mathlib-initiative/mathlib-tactics huggingface dataset:
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
i' : ι'
i : ι
hi : e.f i = i'
⊢ f φ i' = (K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv

Tactic:
have hi' : ∃ k, e.f k = i' := ⟨i, hi⟩

Goal state after:
ι : 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
i' : ι'
i : ι
hi : e.f i = i'
hi' : ∃ k, e.f k = i'
⊢ f φ i' = (K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv
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₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
⊢ ac.desc x₁ x₂ (e₂.f i₂) = x₂ i₂

Tactic:
by
  dsimp [desc]
  rw [ac.desc'_inr _ _ _ i₂ (ac.equiv.injective (by simp)), desc.aux_trans]
  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 : C₁
f : X ⟶ Y
⊢ Φ.homMap L₁ L₂ (L₁.map f) = L₂.map (Φ.functor.map f)

Tactic:
dsimp [homMap]

Goal state after:
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 : C₁
f : X ⟶ Y
⊢ (((CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).symm.app X).homCongr
        ((CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).symm.app Y))
      ((Φ.localizedFunctor L₁ L₂).map (L₁.map f)) =
    L₂.map (Φ.functor.map f)
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
this : IsIso (Q.map (CochainComplex.truncGEMap s n))
eq : Q.map (Y.πTruncGE n ≫ CochainComplex.truncGEMap s n) = Q.map (s ≫ Y'.πTruncGE n)
⊢ Q.map g ≫ inv (Q.map s) =
    Q.map (X.πTruncGE n ≫ CochainComplex.truncGEMap g n) ≫ inv (Q.map (Y.πTruncGE n ≫ CochainComplex.truncGEMap s n))

Tactic:
have eq' := Q.congr_map (CochainComplex.πTruncGE_naturality g n)

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
this : IsIso (Q.map (CochainComplex.truncGEMap s n))
eq : Q.map (Y.πTruncGE n ≫ CochainComplex.truncGEMap s n) = Q.map (s ≫ Y'.πTruncGE n)
eq' : Q.map (X.πTruncGE n ≫ CochainComplex.truncGEMap g n) = Q.map (g ≫ Y'.πTruncGE n)
⊢ Q.map g ≫ inv (Q.map s) =
    Q.map (X.πTruncGE n ≫ CochainComplex.truncGEMap g n) ≫ inv (Q.map (Y.πTruncGE n ≫ CochainComplex.truncGEMap s n))
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 Z : C
n : ℕ
α₁ α₂ : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
⊢ (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h

Tactic:
by
  let := HasDerivedCategory.standard C; ext; simp [this, add_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
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β₁ β₂ : Ext Y Z m
p : ℕ
h : n + m = p
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h

Tactic:
by
  let := HasDerivedCategory.standard C; ext; simp [this, add_hom']

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hi : c.prev j = i
A : C
z₂ : A ⟶ K.cycles j
⊢ z₂ ≫ K.homologyπ j = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ z₂ = x₁ ≫ K.toCycles i j

Tactic:
by
  subst hi
  exact (K.sc j).comp_homologyπ_eq_zero_iff_up_to_refinements z₂

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

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := ⋯
⊢ (∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w', max u v}
          ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))) →
    ∀ (X Y : C) (n : ℕ), Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)

Tactic:
intro h X Y n

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := HasDerivedCategory.standard C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w', max u v}
        ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
n : ℕ
⊢ Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂ : R₂.Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 _proof_300✝)) ⋯ ⋯
    ⋯
⊢ (mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2
      mono_of_epi_of_mono_of_mono'._proof_4 =
    0

Tactic:
dsimp
    rw [← Functor.map_comp]
    exact hR₁

Goal state after:
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✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
x✝¹ : NatTrans.CommShift adj.unit A
a : A
x✝ : D
⊢ ((Functor.commShiftIso (G ⋙ F) a).hom ≫ Functor.whiskerRight adj.counit (shiftFunctor D a)).app x✝ =
    ((shiftFunctor D a).whiskerLeft adj.counit ≫ (Functor.commShiftIso (𝟭 D) a).hom).app x✝

Tactic:
simp only [Functor.comp_obj, Functor.id_obj, NatTrans.comp_app,
      Functor.commShiftIso_comp_hom_app, Functor.whiskerRight_app, assoc, Functor.whiskerLeft_app,
      Functor.commShiftIso_id_hom_app, comp_id]

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✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
x✝¹ : NatTrans.CommShift adj.unit A
a : A
x✝ : D
⊢ F.map ((Functor.commShiftIso G a).hom.app x✝) ≫
      (Functor.commShiftIso F a).hom.app (G.obj x✝) ≫ (shiftFunctor D a).map (adj.counit.app x✝) =
    adj.counit.app ((shiftFunctor D a).obj x✝)
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 : A
X✝ : C
⊢ F.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
      (shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj (F.obj X✝)))) ≫
        (shiftFunctor D a).map ((shiftFunctor D (-a)).map ((Functor.commShiftIso F a).hom.app (G.obj (F.obj X✝)))) ≫
          (shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝)))) ≫
            (shiftFunctor D a).map (adj.counit.app (F.obj X✝)) =
    (Functor.commShiftIso F a).hom.app X✝

Tactic:
← NatTrans.naturality_assoc

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 : A
X✝ : C
⊢ F.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
      (𝟭 D).map ((Functor.commShiftIso F a).hom.app (G.obj (F.obj X✝))) ≫
        (shiftFunctorCompIsoId D (-a) a ⋯).inv.app ((shiftFunctor D a).obj (F.obj (G.obj (F.obj X✝)))) ≫
          (shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝)))) ≫
            (shiftFunctor D a).map (adj.counit.app (F.obj X✝)) =
    (Functor.commShiftIso F a).hom.app X✝
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: R : Type w
inst✝⁷ : Ring R
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : L.Additive
inst✝ : Linear R C
⊢ Functor.Linear R L

Tactic:
let := linear R L W

Goal state after:
R : Type w
inst✝⁷ : Ring R
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : L.Additive
inst✝ : Linear R C
this : Linear R D := linear R L W
⊢ Functor.Linear R L
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
K : CochainComplex C ℤ
w✝ : K.IsStrictlyLE i
π : K ⟶ (CochainComplex.singleFunctor C i).obj P
h : IsIso (Q.map π)
g : K ⟶ L
hπ : IsSplitEpi π
h₁ : inv (Q.map π) = Q.map (section_ π)
⊢ inv (Q.map π) ≫ Q.map g = 0

Tactic:
have h₂ : section_ π ≫ g = 0 := by
    apply HomologicalComplex.from_single_hom_ext
    apply (L.isZero_of_isStrictlyLE n i hn).eq_of_tgt

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
K : CochainComplex C ℤ
w✝ : K.IsStrictlyLE i
π : K ⟶ (CochainComplex.singleFunctor C i).obj P
h : IsIso (Q.map π)
g : K ⟶ L
hπ : IsSplitEpi π
h₁ : inv (Q.map π) = Q.map (section_ π)
h₂ : section_ π ≫ g = 0
⊢ inv (Q.map π) ≫ Q.map g = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X I : C
n : ℕ
inst✝ : Injective I
e : Ext X I (n + 1)
K : CochainComplex C ℤ := (CochainComplex.singleFunctor C 0).obj X
⊢ e = 0

Tactic:
have := K.isStrictlyGE_of_ge (-n) 0 (by lia)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X I : C
n : ℕ
inst✝ : Injective I
e : Ext X I (n + 1)
K : CochainComplex C ℤ := (CochainComplex.singleFunctor C 0).obj X
this : K.IsStrictlyGE (-↑n)
⊢ e = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: case succ
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
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex C :=
  { X₁ := Y, X₂ := Injective.under Y, X₃ := cokernel (Injective.ι Y), f := Injective.ι Y,
    g := cokernel.π (Injective.ι Y), zero := ⋯ }
hS : S.ShortExact
⊢ Small.{w, max u v} (Ext X Y (n + 1))

Tactic:
have : Function.Surjective (Ext.postcomp hS.extClass X (rfl : n + 1 = _)) :=
        fun y₁ ↦ Ext.covariant_sequence_exact₁ X hS y₁ (Ext.eq_zero_of_injective _) rfl

Goal state after:
case succ
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
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex C :=
  { X₁ := Y, X₂ := Injective.under Y, X₃ := cokernel (Injective.ι Y), f := Injective.ι Y,
    g := cokernel.π (Injective.ι Y), zero := ⋯ }
hS : S.ShortExact
this : Function.Surjective ⇑(hS.extClass.postcomp X ⋯)
⊢ Small.{w, max u v} (Ext X Y (n + 1))
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : g.Monic
⊢ ∃ q r,
    r.degree < g.degree ∧
      (algebraMap R[X] K) f / (algebraMap R[X] K) g =
        (algebraMap R[X] K) q + (algebraMap R[X] K) r / (algebraMap R[X] K) g

Tactic:
refine ⟨f /ₘ g, f %ₘ g, ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : g.Monic
⊢ (f %ₘ g).degree < g.degree

case refine_2
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : g.Monic
⊢ (algebraMap R[X] K) f / (algebraMap R[X] K) g =
    (algebraMap R[X] K) (f /ₘ g) + (algebraMap R[X] K) (f %ₘ g) / (algebraMap R[X] K) g
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
i j : ι
⊢ (b.repr (A.col j)) i = of (fun i j ↦ (b.repr (A.col j)) i) i j

Tactic:
Matrix.of_apply

Goal state after:
ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
i j : ι
⊢ (b.repr (A.col j)) i = (b.repr (A.col j)) i
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_7
inst✝ : CommMonoid M
⊢ rootsOfUnity 0 M = ⊤

Tactic:
ext1
  simp only [mem_rootsOfUnity, pow_zero, Subgroup.mem_top]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
m n : ℕ
⊢ rootsOfUnity m M ⊓ rootsOfUnity n M = rootsOfUnity (m.gcd n) M

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Bilinear

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ ((b₁.repr x).sum fun i xi ↦ (b₂.repr y).sum fun j yj ↦ ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) = (B x) y

Tactic:
conv_rhs => rw [← b₁.linearCombination_repr x, ← b₂.linearCombination_repr y]
  simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂, map_sum, map_smulₛₗ₂, map_smulₛₗ]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
u : Rˣ
⊢ det ((scalar n) u) = u ^ Fintype.card n

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type u_2
inst✝ : Field R
g : SL(2, R)
hg : ↑g 1 0 = 0
⊢ ∃ a b, ∃ (h : a ≠ 0), g = ⟨!![a, b; 0, a⁻¹], ⋯⟩

Tactic:
induction g using Matrix.SpecialLinearGroup.fin_two_induction with | h a b c d h_det =>
  replace hg : c = 0 := by simpa using hg
  have had : a * d = 1 := by rwa [hg, mul_zero, sub_zero] at h_det
  refine ⟨a, b, left_ne_zero_of_mul_eq_one had, ?_⟩
  simp_rw [eq_inv_of_mul_eq_one_right had, hg]

Goal state after:
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
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
⊢ f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q → f = g

Tactic:
intro h
  apply (lift Q).symm.injective
  rw [lift_symm_apply, lift_symm_apply]
  simp only [h]

Goal state after:
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
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
⊢ Algebra.adjoin R (Set.range (⇑((lift Q) ⟨f, cond⟩) ∘ ⇑(ι Q))) = Algebra.adjoin R (Set.range ⇑f)

Tactic:
Function.comp_def,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
⊢ Algebra.adjoin R (Set.range fun x ↦ ((lift Q) ⟨f, cond⟩) ((ι Q) x)) = Algebra.adjoin R (Set.range ⇑f)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : SpecialLinearGroup ι F
L L' : List (TransvectionStruct ι F)
D : ι → F
hM : ↑M = (List.map TransvectionStruct.toMatrix L).prod * diagonal D * (List.map TransvectionStruct.toMatrix L').prod
⊢ coeMonoidHom M =
    (List.map (⇑coeMonoidHom ∘ TransvectionStruct.toSpecialLinearGroup) L).prod * diagonal D *
      (List.map (⇑coeMonoidHom ∘ TransvectionStruct.toSpecialLinearGroup) L').prod

Tactic:
Function.comp_def,

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : SpecialLinearGroup ι F
L L' : List (TransvectionStruct ι F)
D : ι → F
hM : ↑M = (List.map TransvectionStruct.toMatrix L).prod * diagonal D * (List.map TransvectionStruct.toMatrix L').prod
⊢ coeMonoidHom M =
    (List.map (fun x ↦ coeMonoidHom x.toSpecialLinearGroup) L).prod * diagonal D *
      (List.map (fun x ↦ coeMonoidHom x.toSpecialLinearGroup) L').prod
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: 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)
⊢ P A

Tactic:
refine diagonal_transvection_induction' P _ (fun i j hij c hc ↦ ?_) htransvec hmul
  fin_cases i
  · obtain rfl : j = 1 := by fin_cases j <;> tauto
    change P (diag2 c hc)
    rw [diag2_decompose c hc]
    refine hmul _ _ (hmul _ _ (hmul _ _ (hmul _ _ (hmul _ _ ?_ ?_) ?_) ?_) ?_) ?_
    all_goals exact htransvec _ _ _ _
  · obtain rfl : j = 0 := by fin_cases j <;> tauto
    rw [show diag2n hij c hc = diag2 c⁻¹ (inv_ne_zero hc) by
      ext; simp [diag2n_coe, diagonal_apply]; grind, diag2_decompose c⁻¹ (inv_ne_zero hc)]
    refine hmul _ _ (hmul _ _ (hmul _ _ (hmul _ _ (hmul _ _ ?_ ?_) ?_) ?_) ?_) ?_
    all_goals exact htransvec _ _ _ _

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
⊢ a * b * c = a * (b * c)

Tactic:
by
  -- (`fun a b c => a * b * c` as a bundled hom) = (`fun a b c => a * (b * c)` as a bundled hom)
  suffices AddMonoidHom.mulLeft₃ = AddMonoidHom.mulRight₃ by
      simpa only [AddMonoidHom.mulLeft₃_apply, AddMonoidHom.mulRight₃_apply] using
        DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this a) b) c
  ext ai ax bi bx ci cx : 6
  dsimp only [coe_comp, Function.comp_apply, AddMonoidHom.mulLeft₃_apply,
    AddMonoidHom.mulRight₃_apply]
  simp_rw [of_mul_of]
  exact of_eq_of_gradedMonoid_eq (_root_.mul_assoc (GradedMonoid.mk ai ax) ⟨bi, bx⟩ ⟨ci, cx⟩)

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

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
Q : QuadraticMap R M N
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : SMul S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
a : S
x : M
⊢ Q (a • x) = (a * a) • Q x

Tactic:
rw [← IsScalarTower.algebraMap_smul R a x, Q.map_smul, ← map_mul, algebraMap_smul]

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ↑((DFinsupp.sum r fun x ai ↦
          DFinsupp.sum r' fun x_1 aj ↦ (of (fun i ↦ ↥(A i)) (x + x_1)) (GradedMonoid.GMul.mul ai aj))
        n) =
    DFinsupp.sum r fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0

Tactic:
DFinsupp.sum_apply,

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ↑(DFinsupp.sum r fun i₁ b ↦
        (DFinsupp.sum r' fun x aj ↦ (of (fun i ↦ ↥(A i)) (i₁ + x)) (GradedMonoid.GMul.mul b aj)) n) =
    DFinsupp.sum r fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case e_f
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝ : ι
⊢ ↑((DFinsupp.sum r' fun x aj ↦ (of (fun i ↦ ↥(A i)) (x✝ + x)) (GradedMonoid.GMul.mul (r x✝) aj)) n) =
    (fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0) x✝ (r x✝)

Tactic:
DFinsupp.sum_apply,

Goal state after:
case e_f
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝ : ι
⊢ ↑(DFinsupp.sum r' fun i₁ b ↦ ((of (fun i ↦ ↥(A i)) (x✝ + i₁)) (GradedMonoid.GMul.mul (r x✝) b)) n) =
    (fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0) x✝ (r x✝)