mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.SingleFunctors

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : Category.{v_4, u_4} E'
A : Type u_5
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift D A
inst✝⁴ : HasShift E A
inst✝³ : HasShift E' A
F G✝ H : SingleFunctors C D A
G G' : D ⥤ E
e : G ≅ G'
inst✝² : G.CommShift A
inst✝¹ : G'.CommShift A
inst✝ : NatTrans.CommShift e.hom A
n a a' : A
ha' : n + a = a'
⊢ ((F.postcomp G).shiftIso n a a' ha').hom ≫ ((F.functor a).isoWhiskerLeft e).hom =
    whiskerRight ((F.functor a').isoWhiskerLeft e).hom (shiftFunctor E n) ≫ ((F.postcomp G').shiftIso n a a' ha').hom

Tactic:
ext X
    simp [NatTrans.shift_app e.hom n]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst✝² : AddCommSemigroup A
inst✝¹ : IsRightCancelAdd A
inst✝ : One A
a b : A
⊢ ∀ (i₁ i₂ : A), (up' a).Rel i₁ i₂ ↔ (up' a).Rel (i₁ + b) (i₂ + b)

Tactic:
dsimp; simp_rw [add_right_comm _ b a, add_right_cancel_iff, implies_true]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst✝² : AddCommSemigroup A
inst✝¹ : IsRightCancelAdd A
inst✝ : One A
a b : A
⊢ ∀ (i₁ i₂ : A), (down' a).Rel i₁ i₂ ↔ (down' a).Rel (i₁ + b) (i₂ + b)

Tactic:
dsimp; simp_rw [add_right_comm _ b a, add_right_cancel_iff, implies_true]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
a✝ : c'.Rel (e.f i) (c'.next (e.f i))
⊢ ∃ x, c'.Rel (e.f i) (e.f x)

Tactic:
exact ⟨j, by simpa only [e.rel_iff] using hi⟩

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ¬∃ j, e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

Tactic:
· have hj' := e.r_eq_none j' (fun j'' hj'' => hj ⟨j'', hj''⟩)
        dsimp [extend]
        rw [extend.d_none_eq_zero' _ _ _ hj', extend.d_none_eq_zero' _ _ _ hj',
          comp_zero, zero_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (φ ≫ φ') e).f i' = (extendMap φ e ≫ extendMap φ' e).f i'

Tactic:
· simp [extendMap_f_eq_zero _ e i' (fun i hi => hi' ⟨i, hi⟩)]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
⊢ (extendSingleIso e X i i' h).hom.f i' =
    (((single C c i).obj X).extendXIso e h).hom ≫ (singleObjXSelf c i X).hom ≫ (singleObjXSelf c' i' X).inv

Tactic:
simp [extendSingleIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
⊢ (extendSingleIso e X i i' h).inv.f i' =
    (singleObjXSelf c' i' X).hom ≫ (singleObjXSelf c i X).inv ≫ (((single C c i).obj X).extendXIso e h).inv

Tactic:
simp [extendSingleIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
i : ι
⊢ (e.liftExtend (e.homRestrict ψ) ⋯).f (e.f i) = ψ.f (e.f i)

Tactic:
simp [e.homRestrict_f _ rfl, e.liftExtend_f _ _ rfl]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i : ι
⊢ (e.homRestrict (e.liftExtend φ hφ)).f i = φ.f i

Tactic:
simp [e.homRestrict_f _ rfl, e.liftExtend_f _ _ rfl]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i : ι
hi : ∀ (i₂ : ι₂), e₂.f i₂ ≠ i
⊢ ∃ i₁, i = e₁.f i₁

Tactic:
by
  obtain ⟨i₁, rfl⟩ | ⟨i₂, rfl⟩ := ac.union i
  · exact ⟨_, rfl⟩
  · exfalso
    exact hi i₂ rfl

Goal state after:
Module: Mathlib.CategoryTheory.Localization.HomEquiv

Goal state before:
pp: C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{v_2, u_2} C₁
inst✝⁴ : Category.{v_3, u_3} C₂
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y Z : C₁
f : L₁.obj X ⟶ L₁.obj Y
g : L₁.obj Y ⟶ L₁.obj Z
⊢ Φ.homMap L₁ L₂ (f ≫ g) = Φ.homMap L₁ L₂ f ≫ Φ.homMap L₁ L₂ g

Tactic:
by
  simp [homMap]

Goal state after:
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ (singleObjHomologySelfIso c j A).inv ≫ ((single C c j).obj A).homologyι j = (singleObjOpcyclesSelfIso c j A).hom

Tactic:
rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, homology_π_ι,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ HasExt C

Tactic:
let := HasDerivedCategory.standard

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : (C : Type ?u.11) → [inst : Category.{?u.12, ?u.11} C] → [inst_1 : Abelian C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
⊢ HasExt C
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₂ : ((mk₀ biprod.inr).comp α ⋯).hom = ((mk₀ biprod.inr).comp β ⋯).hom
h₁ : ((mk₀ biprod.inl).comp α ⋯).hom = ((mk₀ biprod.inl).comp β ⋯).hom
⊢ α.hom = β.hom

Tactic:
simp only [comp_hom, mk₀_hom, ShiftedHom.mk₀_comp] at h₁ h₂

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ : (singleFunctor C 0).map biprod.inl ≫ α.hom = (singleFunctor C 0).map biprod.inl ≫ β.hom
h₂ : (singleFunctor C 0).map biprod.inr ≫ α.hom = (singleFunctor C 0).map biprod.inr ≫ β.hom
⊢ α.hom = β.hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
⊢ (α + β).hom = α.hom + β.hom

Tactic:
let β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β (zero_add n)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
⊢ (α + β).hom = α.hom + β.hom
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a b : A
⊢ iso adj (a + b) = Functor.CommShift.isoAdd (iso adj a) (iso adj b)

Tactic:
refine CommShift.compatibilityUnit_unique_right adj (F.commShiftIso (a + b)) _ _
      (compatibilityUnit_iso adj (a + b)) ?_

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a b : A
⊢ CommShift.CompatibilityUnit adj (Functor.commShiftIso F (a + b)) (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
E : C ≌ D
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : E.inverse.CommShift A
⊢ E.CommShift A

Tactic:
let := E.commShiftFunctor A
  have := E.symm.commShift_of_functor A
  exact inferInstanceAs (E.symm.symm.CommShift A)

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: case zero
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughProjectives C
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
⊢ Small.{w, max u v} (Ext X Y 0)

Tactic:
rw [small_congr Ext.homEquiv₀]

Goal state after:
case zero
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughProjectives C
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
⊢ Small.{w, v} (X ⟶ Y)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i : ℤ
φ : Q.obj K ⟶ Q.obj ((CochainComplex.singleFunctor C i).obj I)
n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
⊢ φ = 0

Tactic:
by
  obtain ⟨L, _, g, ι, h, rfl⟩ := left_fac_of_isStrictlyGE φ i
  have hπ : IsSplitMono ι := by
    rw [isIso_Q_map_iff_quasiIso] at h
    exact CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective ι
  have h₁ : inv (Q.map ι) = Q.map (retraction ι) := by
    rw [← cancel_epi (Q.map ι), IsIso.hom_inv_id, ← Q.map_comp, IsSplitMono.id, Q.map_id]
  have h₂ : g ≫ retraction ι = 0 := by
    apply HomologicalComplex.to_single_hom_ext
    apply (K.isZero_of_isStrictlyGE n i hn).eq_of_src
  rw [h₁, ← Q.map_comp, h₂, Q.map_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: case zero
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughInjectives C
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
⊢ Small.{w, max u v} (Ext X Y 0)

Tactic:
rw [small_congr Ext.homEquiv₀]

Goal state after:
case zero
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughInjectives C
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
⊢ Small.{w, v} (X ⟶ Y)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
g : M ⟶ N
hg : Epi g
f : N ⟶ L
hx : addEquiv₀.symm f ∈ ((mk₀ g).precomp L ⋯).ker
⊢ addEquiv₀.symm f = 0

Tactic:
simpa [← cancel_epi g] using hx

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mpr.refine_1
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
h : (fun i ↦ f (v i) ⋯) = 0
i : n
⊢ v i = 0 i

Tactic:
have := congr_arg (algebraMap A K) (congr_fun h i)

Goal state after:
case mpr.refine_1
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝¹ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this✝ : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
h : (fun i ↦ f (v i) ⋯) = 0
i : n
this : (algebraMap A K) (f (v i) ⋯) = (algebraMap A K) (0 i)
⊢ v i = 0 i
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
R : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
⊢ 0 < ↑(GeneralLinearGroup.det (-↑g))

Tactic:
GeneralLinearGroup.val_det_apply,

Goal state after:
n : Type u
R : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
⊢ 0 < (↑(-↑g)).det
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Algebra.adjoin R (Set.range ⇑(ι Q)) = ⊤

Tactic:
refine top_unique fun x hx => ?_; clear hx
  induction x using induction with
  | algebraMap => exact algebraMap_mem _ _
  | add x y hx hy => exact add_mem hx hy
  | mul x y hx hy => exact mul_mem hx hy
  | ι x => exact Algebra.subset_adjoin (Set.mem_range_self _)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case convert_3
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ (diagonalRingHom ι F) D = (diagonalRingHom ι F) ({i | i ≠ i₀}.noncommProd g ⋯)

Tactic:
Finset.noncommProd_eq_prod

Goal state after:
case convert_3
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ (diagonalRingHom ι F) D = (diagonalRingHom ι F) ({i | i ≠ i₀}.prod g)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
⊢ ⟨diagonal D, hD⟩ = {i | i ≠ i₀}.noncommProd (fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1) ⋯

Tactic:
set g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1 with hg_def
  apply coeMonoidHom_injective
  rw [Finset.map_noncommProd]
  simp_rw [coeMonoidHom_apply, apply_dite, coe_one]
  rw [Finset.noncommProd_congr (s₂ := {i | i ≠ i₀}) rfl (fun i hi ↦
      (dif_pos (Finset.mem_filter.1 hi).2 : _ = (diag2n (Finset.mem_filter.1 hi).2 _ _).1))]
  convert_to! _ = Finset.noncommProd {i | i ≠ i₀} (fun x ↦ diagonal (g x)) _
  simp_rw [← diagonalRingHom_apply]
  rw [← Finset.map_noncommProd _ _ (fun _ _ _ _ _ ↦ Commute.all _ _), Finset.noncommProd_eq_prod]
  rw [diag_decompose i₀ D hD]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case nil
F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
i₀ j₀ : ι
hij₀ : i₀ ≠ j₀
hP1 : P 1
hdiagonal : ∀ (D : ι → F) (hD : (diagonal D).det = 1), P ⟨diagonal D, hD⟩
⊢ P (List.map TransvectionStruct.toSpecialLinearGroup []).prod

Tactic:
| nil =>

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «0».refine_1
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ 1
⊢ P (SpecialLinearGroup.transvection ⋯ c)

pp: case «0».refine_2
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ 1
⊢ P (SpecialLinearGroup.transvection ⋯ (-c⁻¹))

pp: case «0».refine_3
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ 1
⊢ P (SpecialLinearGroup.transvection ⋯ c)

pp: case «0».refine_4
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ 1
⊢ P (SpecialLinearGroup.transvection ⋯ (-1))

pp: case «0».refine_5
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ 1
⊢ P (SpecialLinearGroup.transvection ⋯ 1)

pp: case «0».refine_6
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ 1
⊢ P (SpecialLinearGroup.transvection ⋯ (-1))

Tactic:
all_goals exact htransvec _ _ _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «1».refine_1
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
⊢ P (SpecialLinearGroup.transvection ⋯ c⁻¹)

pp: case «1».refine_2
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
⊢ P (SpecialLinearGroup.transvection ⋯ (-c⁻¹⁻¹))

pp: case «1».refine_3
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
⊢ P (SpecialLinearGroup.transvection ⋯ c⁻¹)

pp: case «1».refine_4
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
⊢ P (SpecialLinearGroup.transvection ⋯ (-1))

pp: case «1».refine_5
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
⊢ P (SpecialLinearGroup.transvection ⋯ 1)

pp: case «1».refine_6
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
⊢ P (SpecialLinearGroup.transvection ⋯ (-1))

Tactic:
all_goals exact htransvec _ _ _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
j' : m
⊢ ((Pi.basisFun R n).repr (l (Pi.single i 1))) i' •>
      ((Pi.basisFun R m).repr (r (Pi.single j 1))) j' •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) j') =
    of (fun i j ↦ l (Pi.single j 1) i) i' i * (B (Pi.single i' 1)) (Pi.single j' 1) *
      of (fun i j ↦ r (Pi.single j 1) i) j' j

Tactic:
simp only [smul_eq_mul, Pi.basisFun_repr, mul_assoc, mul_comm, mul_left_comm,
        Pi.basisFun_apply, of_apply]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: case nil
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
⊢ (of A ([].dProdIndex fι)) ([].dProd fι fA) = (List.map (fun a ↦ (of A (fι a)) (fA a)) []).prod

Tactic:
| nil =>

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x x' y : M
⊢ f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x + x') + f (x' + y) + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y)

Tactic:
add_left_inj

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x x' y : M
⊢ f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y) ↔
    f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y)
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
| (decompose ℳ).symm ((decompose ℳ) r)

Tactic:
← sum_support_of (decompose ℳ r)

Goal state after:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
| (decompose ℳ).symm (∑ i ∈ DFinsupp.support ((decompose ℳ) r), (of (fun i ↦ ↥(ℳ i)) i) (((decompose ℳ) r) i))