Skip to content

Commit

Permalink
chore: classify simp cannot prove porting notes (#10960)
Browse files Browse the repository at this point in the history
Classifies by adding issue number #10959 porting notes claiming anything semantically equivalent to: 

- "`simp` cannot prove this"
- "`simp` used to be able to close this goal"
- "`simp` can't handle this"
- "`simp` used to work here"
  • Loading branch information
pitmonticone committed Feb 27, 2024
1 parent 1ea8344 commit c70ed95
Show file tree
Hide file tree
Showing 9 changed files with 19 additions and 19 deletions.
12 changes: 6 additions & 6 deletions Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
Expand Up @@ -200,7 +200,7 @@ instance : IsIso (@LaxMonoidal.ε _ _ _ _ _ _ (free R).obj _ _) := by
refine' ⟨⟨Finsupp.lapply PUnit.unit, ⟨_, _⟩⟩⟩
· -- Porting note: broken ext
apply LinearMap.ext_ring
-- Porting note: simp used to be able to close this goal
-- Porting note (#10959): simp used to be able to close this goal
dsimp
erw [ModuleCat.comp_def, LinearMap.comp_apply, ε_apply, Finsupp.lapply_apply,
Finsupp.single_eq_same, id_apply]
Expand All @@ -210,7 +210,7 @@ instance : IsIso (@LaxMonoidal.ε _ _ _ _ _ _ (free R).obj _ _) := by
apply LinearMap.ext_ring
apply Finsupp.ext
intro ⟨⟩
-- Porting note: simp used to be able to close this goal
-- Porting note (#10959): simp used to be able to close this goal
dsimp
erw [ModuleCat.comp_def, LinearMap.comp_apply, ε_apply, Finsupp.lapply_apply,
Finsupp.single_eq_same]
Expand Down Expand Up @@ -323,7 +323,7 @@ def embedding : C ⥤ Free R C where
map {X Y} f := Finsupp.single f 1
map_id X := rfl
map_comp {X Y Z} f g := by
-- Porting note: simp used to be able to close this goal
-- Porting note (#10959): simp used to be able to close this goal
dsimp only []
rw [single_comp_single, one_mul]
#align category_theory.Free.embedding CategoryTheory.Free.embedding
Expand All @@ -341,7 +341,7 @@ def lift (F : C ⥤ D) : Free R C ⥤ D where
map_id := by dsimp [CategoryTheory.categoryFree]; simp
map_comp {X Y Z} f g := by
apply Finsupp.induction_linear f
· -- Porting note: simp used to be able to close this goal
· -- Porting note (#10959): simp used to be able to close this goal
dsimp
rw [Limits.zero_comp, sum_zero_index, Limits.zero_comp]
· intro f₁ f₂ w₁ w₂
Expand All @@ -355,7 +355,7 @@ def lift (F : C ⥤ D) : Free R C ⥤ D where
· intros; simp only [add_smul]
· intro f' r
apply Finsupp.induction_linear g
· -- Porting note: simp used to be able to close this goal
· -- Porting note (#10959): simp used to be able to close this goal
dsimp
rw [Limits.comp_zero, sum_zero_index, Limits.comp_zero]
· intro f₁ f₂ w₁ w₂
Expand Down Expand Up @@ -405,7 +405,7 @@ def ext {F G : Free R C ⥤ D} [F.Additive] [F.Linear R] [G.Additive] [G.Linear
(by
intro X Y f
apply Finsupp.induction_linear f
· -- Porting note: simp used to be able to close this goal
· -- Porting note (#10959): simp used to be able to close this goal
rw [Functor.map_zero, Limits.zero_comp, Functor.map_zero, Limits.comp_zero]
· intro f₁ f₂ w₁ w₂
-- Porting note: Using rw instead of simp
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/ContinuedFractions/Translations.lean
Expand Up @@ -154,7 +154,7 @@ theorem second_continuant_aux_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some
theorem first_continuant_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
g.continuants 1 = ⟨gp.b * g.h + gp.a, gp.b⟩ := by
simp [nth_cont_eq_succ_nth_cont_aux]
-- porting note: simp used to work here, but now it can't figure out that 1 + 1 = 2
-- Porting note (#10959): simp used to work here, but now it can't figure out that 1 + 1 = 2
convert second_continuant_aux_eq zeroth_s_eq
#align generalized_continued_fraction.first_continuant_eq GeneralizedContinuedFraction.first_continuant_eq

Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Homology/Augment.lean
Expand Up @@ -334,14 +334,14 @@ def augmentTruncate (C : CochainComplex V ℕ) :
comm' := fun i j => by
rcases j with (_ | _ | j) <;> cases i <;>
· dsimp
-- Porting note: simp can't handle this now but aesop does
-- Porting note (#10959): simp can't handle this now but aesop does
aesop }
inv :=
{ f := fun i => by cases i <;> exact 𝟙 _
comm' := fun i j => by
rcases j with (_ | _ | j) <;> cases' i with i <;>
· dsimp
-- Porting note: simp can't handle this now but aesop does
-- Porting note (#10959): simp can't handle this now but aesop does
aesop }
hom_inv_id := by
ext i
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Analysis/NormedSpace/Star/Basic.lean
Expand Up @@ -202,7 +202,7 @@ section Unital

variable [NormedRing E] [StarRing E] [CstarRing E]

@[simp, nolint simpNF] -- Porting note: simp cannot prove this
@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove this
theorem norm_one [Nontrivial E] : ‖(1 : E)‖ = 1 := by
have : 0 < ‖(1 : E)‖ := norm_pos_iff.mpr one_ne_zero
rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]
Expand Down
6 changes: 3 additions & 3 deletions Mathlib/Analysis/Quaternion.lean
Expand Up @@ -80,12 +80,12 @@ theorem nnnorm_coe (a : ℝ) : ‖(a : ℍ)‖₊ = ‖a‖₊ :=
Subtype.ext <| norm_coe a
#align quaternion.nnnorm_coe Quaternion.nnnorm_coe

@[simp, nolint simpNF] -- Porting note: simp cannot prove this
@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove this
theorem norm_star (a : ℍ) : ‖star a‖ = ‖a‖ := by
simp_rw [norm_eq_sqrt_real_inner, inner_self, normSq_star]
#align quaternion.norm_star Quaternion.norm_star

@[simp, nolint simpNF] -- Porting note: simp cannot prove this
@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove this
theorem nnnorm_star (a : ℍ) : ‖star a‖₊ = ‖a‖₊ :=
Subtype.ext <| norm_star a
#align quaternion.nnnorm_star Quaternion.nnnorm_star
Expand Down Expand Up @@ -147,7 +147,7 @@ theorem coeComplex_one : ((1 : ℂ) : ℍ) = 1 :=
rfl
#align quaternion.coe_complex_one Quaternion.coeComplex_one

@[simp, norm_cast, nolint simpNF] -- Porting note: simp cannot prove this
@[simp, norm_cast, nolint simpNF] -- Porting note (#10959): simp cannot prove this
theorem coe_real_complex_mul (r : ℝ) (z : ℂ) : (r • z : ℍ) = ↑r * ↑z := by ext <;> simp
#align quaternion.coe_real_complex_mul Quaternion.coe_real_complex_mul

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Data/List/Basic.lean
Expand Up @@ -3007,7 +3007,7 @@ theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) :
rw [attach, map_pmap]; exact pmap_congr l fun _ _ _ _ => rfl
#align list.pmap_eq_map_attach List.pmap_eq_map_attach

-- @[simp] -- Porting note: lean 4 simp can't rewrite with this
-- @[simp] -- Porting note (#10959): lean 4 simp can't rewrite with this
theorem attach_map_coe' (l : List α) (f : α → β) :
(l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
rw [attach, map_pmap]; exact pmap_eq_map _ _ _ _
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Order/Filter/Germ.lean
Expand Up @@ -267,7 +267,7 @@ theorem coe_compTendsto (f : α → β) {lc : Filter γ} {g : γ → α} (hg : T
rfl
#align filter.germ.coe_comp_tendsto Filter.Germ.coe_compTendsto

@[simp, nolint simpNF] -- Porting note: simp cannot prove this
@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove this
theorem compTendsto'_coe (f : Germ l β) {lc : Filter γ} {g : γ → α} (hg : Tendsto g lc l) :
f.compTendsto' _ hg.germ_tendsto = f.compTendsto g hg :=
rfl
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/RingTheory/Valuation/ValuationSubring.lean
Expand Up @@ -47,7 +47,7 @@ instance : SetLike (ValuationSubring K) K where
replace h := SetLike.coe_injective' h
congr

@[simp, nolint simpNF] -- Porting note: simp cannot prove that
@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove that
theorem mem_carrier (x : K) : x ∈ A.carrier ↔ x ∈ A := Iff.refl _
#align valuation_subring.mem_carrier ValuationSubring.mem_carrier

Expand Down
6 changes: 3 additions & 3 deletions Mathlib/SetTheory/Ordinal/Arithmetic.lean
Expand Up @@ -1148,14 +1148,14 @@ theorem bfamilyOfFamily_typein {ι} (f : ι → α) (i) :
bfamilyOfFamily'_typein _ f i
#align ordinal.bfamily_of_family_typein Ordinal.bfamilyOfFamily_typein

@[simp, nolint simpNF] -- Porting note: simp cannot prove this
@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove this
theorem familyOfBFamily'_enum {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o}
(ho : type r = o) (f : ∀ a < o, α) (i hi) :
familyOfBFamily' r ho f (enum r i (by rwa [ho])) = f i hi := by
simp only [familyOfBFamily', typein_enum]
#align ordinal.family_of_bfamily'_enum Ordinal.familyOfBFamily'_enum

@[simp, nolint simpNF] -- Porting note: simp cannot prove this
@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove this
theorem familyOfBFamily_enum (o : Ordinal) (f : ∀ a < o, α) (i hi) :
familyOfBFamily o f
(enum (· < ·) i
Expand Down Expand Up @@ -1450,7 +1450,7 @@ theorem sup_eq_bsup' {o : Ordinal.{u}} {ι} (r : ι → ι → Prop) [IsWellOrde
sup_eq_sup r _ ho _ f
#align ordinal.sup_eq_bsup' Ordinal.sup_eq_bsup'

@[simp, nolint simpNF] -- Porting note: simp cannot prove this
@[simp, nolint simpNF] -- Porting note (#10959): simp cannot prove this
theorem sSup_eq_bsup {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
sSup (brange o f) = bsup.{_, v} o f := by
congr
Expand Down

0 comments on commit c70ed95

Please sign in to comment.