Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - refactor: add explicit equation lemmas for comp and flip #8371

Closed
wants to merge 7 commits into from
Closed
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Archive/Wiedijk100Theorems/CubingACube.lean
Original file line number Diff line number Diff line change
@@ -219,7 +219,7 @@ theorem shiftUp_bottom_subset_bottoms (hc : (cs i).xm ≠ 1) :
rw [mem_iUnion]; use i'; refine' ⟨_, fun j => hi' j.succ⟩
have : i ≠ i' := by rintro rfl; apply not_le_of_lt (hi' 0).2; rw [hp0]; rfl
have := h.1 this
rw [onFun, comp, comp, toSet_disjoint, exists_fin_succ] at this
rw [onFun, comp_apply, comp_apply, toSet_disjoint, exists_fin_succ] at this
rcases this with (h0 | ⟨j, hj⟩)
rw [hp0]; symm; apply eq_of_Ico_disjoint h0 (by simp [hw]) _
convert hi' 0; rw [hp0]; rfl
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
Original file line number Diff line number Diff line change
@@ -747,7 +747,7 @@ def counit : restrictScalars.{max v u₂,u₁,u₂} f ⋙ extendScalars f ⟶
induction' z using TensorProduct.induction_on with s' y z₁ z₂ ih₁ ih₂
· rw [map_zero, map_zero]
· dsimp
rw [ModuleCat.coe_comp, ModuleCat.coe_comp,Function.comp,Function.comp,
rw [ModuleCat.coe_comp, ModuleCat.coe_comp, Function.comp_apply, Function.comp_apply,
ExtendScalars.map_tmul, restrictScalars.map_apply]
-- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
erw [Counit.map_apply]
@@ -771,7 +771,7 @@ def extendRestrictScalarsAdj {R : Type u₁} {S : Type u₂} [CommRing R] [CommR
counit := ExtendRestrictScalarsAdj.counit.{v,u₁,u₂} f
homEquiv_unit {X Y g} := LinearMap.ext fun x => by
dsimp
rw [ModuleCat.coe_comp, Function.comp, restrictScalars.map_apply]
rw [ModuleCat.coe_comp, Function.comp_apply, restrictScalars.map_apply]
rfl
homEquiv_counit {X Y g} := LinearMap.ext fun x => by
-- Porting note: once again reminding Lean of the instances
2 changes: 1 addition & 1 deletion Mathlib/Data/Fin/Tuple/Basic.lean
Original file line number Diff line number Diff line change
@@ -242,7 +242,7 @@ theorem comp_cons {α : Type*} {β : Type*} (g : α → β) (y : α) (q : Fin n
rfl
· let j' := pred j h
have : j'.succ = j := succ_pred j h
rw [← this, cons_succ, comp, comp, cons_succ]
rw [← this, cons_succ, comp_apply, comp_apply, cons_succ]
#align fin.comp_cons Fin.comp_cons

theorem comp_tail {α : Type*} {β : Type*} (g : α → β) (q : Fin n.succ → α) :
2 changes: 1 addition & 1 deletion Mathlib/Data/MvPolynomial/Rename.lean
Original file line number Diff line number Diff line change
@@ -85,7 +85,7 @@ theorem rename_rename (f : σ → τ) (g : τ → α) (p : MvPolynomial σ R) :
-- porting note: the Lean 3 proof of this was very fragile and included a nonterminal `simp`.
-- Hopefully this is less prone to breaking
rw [eval₂_comp_left (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C (X ∘ f) p]
simp only [(· ∘ ·), eval₂Hom_X', coe_eval₂Hom]
simp only [(· ∘ ·), eval₂Hom_X']
refine' eval₂Hom_congr _ rfl rfl
ext1; simp only [comp_apply, RingHom.coe_comp, eval₂Hom_C]
#align mv_polynomial.rename_rename MvPolynomial.rename_rename
7 changes: 7 additions & 0 deletions Mathlib/Init/Function.lean
Original file line number Diff line number Diff line change
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Haitao Zhang
import Mathlib.Init.Logic
import Mathlib.Mathport.Rename
import Mathlib.Tactic.Attr.Register
import Mathlib.Tactic.Eqns

#align_import init.function from "leanprover-community/lean"@"03a6a6015c0b12dce7b36b4a1f7205a92dfaa592"

@@ -25,6 +26,12 @@ variable {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ

lemma comp_def {α β δ : Sort _} (f : β → δ) (g : α → β) : f ∘ g = fun x ↦ f (g x) := rfl

attribute [eqns comp_def] comp

lemma flip_def {f : α → β → φ} : flip f = fun b a => f a b := rfl

attribute [eqns flip_def] flip

Comment on lines +29 to +34
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am extremely hesitant to make this change in Mathlib; if we want to change a basic behaviour like this shouldn't we coordinate with Std and Lean? I worry that it introduces a confusing variation in behaviour across the ecosystem.

Copy link
Member Author

@eric-wieser eric-wieser Nov 12, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For other readers, discussion continues on Zulip; the conclusion is that we can live with this in the short term, but should indeed upstream or coordinate.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've been convinved.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Undoability was one of the reasons I decided to go ahead and merge. I was seeing it as a workaround to help get the version bump done sooner rather than a permanent design.

/-- Composition of dependent functions: `(f ∘' g) x = f (g x)`, where type of `g x` depends on `x`
and type of `f (g x)` depends on `x` and `g x`. -/
@[inline, reducible]
4 changes: 2 additions & 2 deletions Mathlib/NumberTheory/NumberField/Discriminant.lean
Original file line number Diff line number Diff line change
@@ -75,8 +75,8 @@ theorem _root_.NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis
← coe_discr, map_intCast, ← Complex.nnnorm_int]
ext : 2
dsimp only
rw [Matrix.map_apply, Basis.toMatrix_apply, Basis.coe_reindex, Function.comp, Equiv.symm_symm,
latticeBasis_apply, ← commMap_canonical_eq_mixed, Complex.ofReal_eq_coe,
rw [Matrix.map_apply, Basis.toMatrix_apply, Basis.coe_reindex, Function.comp_apply,
Equiv.symm_symm, latticeBasis_apply, ← commMap_canonical_eq_mixed, Complex.ofReal_eq_coe,
stdBasis_repr_eq_matrixToStdBasis_mul K _ (fun _ => rfl)]
rfl

2 changes: 1 addition & 1 deletion Mathlib/Topology/UniformSpace/AbstractCompletion.lean
Original file line number Diff line number Diff line change
@@ -208,7 +208,7 @@ theorem map_unique {f : α → β} {g : hatα → hatβ} (hg : UniformContinuous
pkg.funext (pkg.continuous_map _ _) hg.continuous <| by
intro a
change pkg.extend (ι' ∘ f) _ = _
simp only [(· ∘ ·), h, ←comp_apply (f := g)]
simp_rw [(· ∘ ·), h, ←comp_apply (f := g)]
rw [pkg.extend_coe (hg.comp pkg.uniformContinuous_coe)]
#align abstract_completion.map_unique AbstractCompletion.map_unique