mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

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✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso ((opFunctor C c').map (K.ιTruncLE e).op) ↔ K.op.IsSupported e.op

Tactic:
exact K.op.quasiIso_πTruncGE_iff_isSupported e.op

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
S₁ S₂ : ShortComplex C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ ((singleFunctorsPostcompQIso C).hom.hom 0).app S₁.X₃ ≫
      triangleOfSESδ ⋯ ≫
        (shiftFunctor (DerivedCategory C) 1).map
            (Q.map ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map f.τ₁)) ≫
          (shiftFunctor (DerivedCategory C) 1).map (((singleFunctorsPostcompQIso C).inv.hom 0).app S₂.X₁) =
    (singleFunctor C 0).map f.τ₃ ≫
      ((singleFunctorsPostcompQIso C).hom.hom 0).app S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          (shiftFunctor (DerivedCategory C) 1).map (((singleFunctorsPostcompQIso C).inv.hom 0).app S₂.X₁)

Tactic:
rw [reassoc_of% dsimp% ((triangleOfSES.map (h₁.map_of_exact _) (h₂.map_of_exact _))
      ((HomologicalComplex.single C (.up ℤ) 0).mapShortComplex.map f)).comm₃]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
S₁ S₂ : ShortComplex C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ ((singleFunctorsPostcompQIso C).hom.hom 0).app S₁.X₃ ≫
      Q.map ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map f.τ₃) ≫
        triangleOfSESδ ⋯ ≫
          (shiftFunctor (DerivedCategory C) 1).map (((singleFunctorsPostcompQIso C).inv.hom 0).app S₂.X₁) =
    (singleFunctor C 0).map f.τ₃ ≫
      ((singleFunctorsPostcompQIso C).hom.hom 0).app S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          (shiftFunctor (DerivedCategory C) 1).map (((singleFunctorsPostcompQIso C).inv.hom 0).app S₂.X₁)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ Ext.comp 0 γ ⋯ = 0

Tactic:
Ext.zero_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ 0 = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₂ Y n
n' : ℕ
h : 1 + n = n'
⊢ Ext.comp 0 γ ⋯ = 0

Tactic:
Ext.zero_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₂ Y n
n' : ℕ
h : 1 + n = n'
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
m n : ℤ
hmn : m + n = 0
⊢ (shiftFunctor Cᵒᵖ m).map ((opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op X)) =
    (opShiftFunctorEquivalence C n).counitIso.inv.app ((shiftFunctor Cᵒᵖ m).obj (Opposite.op X)) ≫
      (shiftFunctor Cᵒᵖ n).map
          ((shiftFunctor C n).map ((shiftFunctorOpIso C m n hmn).hom.app (Opposite.op X)).unop).op ≫
        (shiftFunctor Cᵒᵖ n).map ((shiftFunctorOpIso C m n hmn).inv.app (Opposite.op ((shiftFunctor C n).obj X))) ≫
          (shiftFunctorComm Cᵒᵖ n m).inv.app (Opposite.op ((shiftFunctor C n).obj X))

Tactic:
obtain rfl : m = -n := by lia
  dsimp [opShiftFunctorEquivalence]
  simp only [shiftFunctor_op_map _ (-n) n, shiftFunctor_op_map _ n (-n),
    shiftFunctorComm_inv_app_of_add_eq_zero n (-n) (by lia), assoc,
    shiftFunctorCompIsoId_op_inv_app, shiftFunctorCompIsoId_op_hom_app,
    shift_shiftFunctorCompIsoId_hom_app, op_comp, unop_comp, Quiver.Hom.unop_op,
    Functor.map_comp, Iso.inv_hom_id_app_assoc, Functor.op_obj]
  apply Quiver.Hom.unop_inj
  simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ IsSplitEpi π

Tactic:
have : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv := by
    rw [← cancel_epi e.hom]
    dsimp [α, e]
    rw [assoc, assoc, assoc, iCyclesIso_hom_inv_id_assoc,
      homologyπ_naturality_assoc]
    dsimp [singleFunctor, singleFunctors]
    rw [homologyπ_singleObjHomologySelfIso_hom_assoc,
      ← singleObjCyclesSelfIso_inv_iCycles, Iso.hom_inv_id_assoc, ← cyclesMap_i]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ IsSplitEpi π
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
x : relations.R →₀ A
⊢ relations.toQuotient (relations.map x) ∈ ⊥

Tactic:
simp only [toQuotient_map_apply, Submodule.zero_mem]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Finite n
this✝ : Fintype m
this : Fintype n
⊢ Mᵀ.SeparatingRight ↔ M.SeparatingLeft

Tactic:
simp_rw [separatingRight_def, separatingLeft_def, dotProduct_transpose_mulVec]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
e : Basis ι R M
⊢ RightInverse (fun m j ↦ ∑ i, m i j • e i) e.toMatrix

Tactic:
by
    intro m
    ext k l
    simp only [e.toMatrix_apply, ← e.equivFun_apply, ← e.equivFun_symm_apply,
      LinearEquiv.apply_symm_apply]

Goal state after:
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
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
x₂ : Ext S.X₂ Y n
hx₂ : (mk₀ S.f).comp x₂ ⋯ = 0
⊢ ∃ x₁, (mk₀ S.g).comp x₁ ⋯ = x₂

Tactic:
have := contravariant_sequence_exact₂' hS Y n
  rw [ShortComplex.ab_exact_iff] at this
  exact this x₂ hx₂

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

Tactic:
simp_rw [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, lift_ι_apply]

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∑ i_1, (b₁.repr (l (b₁' i))) i' •> (b₂.repr (r (b₂' j))) i_1 •> (B (b₁ i')) (b₂ i_1) =
    ∑ x, (b₁.repr (l (b₁' i))) i' * (B (b₁ i')) (b₂ x) * (b₂.repr (r (b₂' j))) x

Tactic:
apply sum_congr rfl
      rintro j' -
      simp only [smul_eq_mul, mul_assoc, mul_comm,
        mul_left_comm]

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

Goal state before:
pp: case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (∑ i ∈ Finset.cons a s ha, f i) =
    ∑ i ∈ Finset.cons a s ha, Q (f i) + ∑ ij ∈ (Finset.cons a s ha).sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)

Tactic:
Finset.sum_cons,

Goal state after:
case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (f a + ∑ i ∈ s, f i) =
    Q (f a) + ∑ i ∈ s, Q (f i) + ∑ ij ∈ (Finset.cons a s ha).sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) + polar (⇑Q) (f a) (∑ i ∈ s, f i))) =
    Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ x ∈ Finset.cons a s ha,
            if ¬((Sym2.mkEmbedding a) x).IsDiag then polarSym2 (⇑Q) (Sym2.map f ((Sym2.mkEmbedding a) x)) else 0) +
          ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0))

Tactic:
Finset.sum_cons,

Goal state after:
case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) + polar (⇑Q) (f a) (∑ i ∈ s, f i))) =
    Q (f a) +
      (∑ i ∈ s, Q (f i) +
        (((if ¬((Sym2.mkEmbedding a) a).IsDiag then polarSym2 (⇑Q) (Sym2.map f ((Sym2.mkEmbedding a) a)) else 0) +
            ∑ x ∈ s,
              if ¬((Sym2.mkEmbedding a) x).IsDiag then polarSym2 (⇑Q) (Sym2.map f ((Sym2.mkEmbedding a) x)) else 0) +
          ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0))
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
ι : Type u_8
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
⊢ Q (∑ i ∈ Finset.cons a s ha, f i) =
    ∑ ij ∈ (Finset.cons a s ha).sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ Finset.cons a s ha, Q (f i)

Tactic:
Finset.sum_cons,

Goal state after:
case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
ι : Type u_8
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
⊢ Q (f a + ∑ i ∈ s, f i) =
    ∑ ij ∈ (Finset.cons a s ha).sym2, polarSym2 (⇑Q) (Sym2.map f ij) - (Q (f a) + ∑ i ∈ s, Q (f i))
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
ι : Type u_8
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
⊢ Q (f a) + (∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i) + polar (⇑Q) (f a) (∑ i ∈ s, f i)) =
    ∑ x ∈ Finset.cons a s ha, polarSym2 (⇑Q) (Sym2.map f ((Sym2.mkEmbedding a) x)) +
        ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) -
      (Q (f a) + ∑ i ∈ s, Q (f i))

Tactic:
Finset.sum_cons,

Goal state after:
case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
ι : Type u_8
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
⊢ Q (f a) + (∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i) + polar (⇑Q) (f a) (∑ i ∈ s, f i)) =
    polarSym2 (⇑Q) (Sym2.map f ((Sym2.mkEmbedding a) a)) +
          ∑ x ∈ s, polarSym2 (⇑Q) (Sym2.map f ((Sym2.mkEmbedding a) x)) +
        ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) -
      (Q (f a) + ∑ i ∈ s, Q (f i))
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ∀ {i : ι} (m : ↥(𝒜 i)) (y : A), ↑(((decompose 𝒜) (↑m * y)) 0) = ↑(((decompose 𝒜) ↑m) 0) * ↑(((decompose 𝒜) y) 0)

Tactic:
rintro i ⟨c, hc⟩
      refine DirectSum.Decomposition.inductionOn 𝒜 ?_ ?_ ?_
      · simp only [mul_zero, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
      · rintro j ⟨c', hc'⟩
        simp only
        by_cases h : i + j = 0
        · rw [decompose_of_mem_same 𝒜
              (show c * c' ∈ 𝒜 0 from h ▸ SetLike.GradedMul.mul_mem hc hc'),
            decompose_of_mem_same 𝒜 (show c ∈ 𝒜 0 from (add_eq_zero.mp h).1 ▸ hc),
            decompose_of_mem_same 𝒜 (show c' ∈ 𝒜 0 from (add_eq_zero.mp h).2 ▸ hc')]
        · rw [decompose_of_mem_ne 𝒜 (SetLike.GradedMul.mul_mem hc hc') h]
          rcases show i ≠ 0 ∨ j ≠ 0 by rwa [add_eq_zero, not_and_or] at h with h' | h'
          · simp only [decompose_of_mem_ne 𝒜 hc h', zero_mul]
          · simp only [decompose_of_mem_ne 𝒜 hc' h', mul_zero]
      · intro _ _ hd he
        simp only [mul_add, decompose_add, add_apply, AddMemClass.coe_add, hd, he]

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

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : A
n i : ι
h : ¬i ≤ n
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (a * ↑b)) n) = 0

Tactic:
rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_not_le]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ associated (linMulLin LinearMap.id LinearMap.id) = mul R R

Tactic:
associated_linMulLin

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ ⅟2 • ((mul R R).compl₁₂ LinearMap.id LinearMap.id + (mul R R).compl₁₂ LinearMap.id LinearMap.id) = mul R R
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
⊢ (LinearMap.toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R n)) (QuadraticMap.associated Q) =
    (LinearMap.toMatrix₂' R) (QuadraticMap.associated Q)

Tactic:
exact LinearEquiv.congr_arg rfl

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
Q : QuadraticMap R M R
hB₁ : (QuadraticMap.associatedHom ℕ) Q ≠ 0
⊢ ∃ x, (((QuadraticMap.associatedHom ℕ) Q) x) x ≠ 0

Tactic:
obtain ⟨x, hx⟩ := QuadraticMap.exists_quadraticMap_ne_zero hB₁

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
Q : QuadraticMap R M R
hB₁ : (QuadraticMap.associatedHom ℕ) Q ≠ 0
x : M
hx : Q x ≠ 0
⊢ ∃ x, (((QuadraticMap.associatedHom ℕ) Q) x) x ≠ 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
Q : QuadraticMap R M R
hB₁ : (QuadraticMap.associatedHom ℕ) Q ≠ 0
x : M
hx : Q x ≠ 0
⊢ ∃ x, (((QuadraticMap.associatedHom ℕ) Q) x) x ≠ 0

Tactic:
exact ⟨x, fun h => hx (Q.associated_eq_self_apply ℕ x ▸ h)⟩

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ 1 ≤ evenOdd Q 0

Tactic:
refine le_trans ?_ (le_iSup _ ⟨0, Nat.cast_zero⟩)

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ 1 ≤ (ι Q).range ^ ↑⟨0, ⋯⟩
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
⊢ ∀ (val : ℕ) (property : ↑val = n) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ ↑⟨val, property⟩), motive x ⋯

Tactic:
simp_rw [ZMod.natCast_eq_iff, add_comm n.val]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
⊢ ∀ (val : ℕ) (property : ∃ k, val = 2 * k + n.val) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ val), motive x ⋯
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
h1 : 0 < n
val✝ : Fintype α
this : (Nat.card α).choose n = 0 ∨ (Nat.card α).choose n = 1
h2 : n < Nat.card α
⊢ False

Tactic:
rcases this with h | h

Goal state after:
case inl.inl
α : Type u_1
n : ℕ
h1 : 0 < n
val✝ : Fintype α
h2 : n < Nat.card α
h : (Nat.card α).choose n = 0
⊢ False

case inl.inr
α : Type u_1
n : ℕ
h1 : 0 < n
val✝ : Fintype α
h2 : n < Nat.card α
h : (Nat.card α).choose n = 1
⊢ False
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
hx2 : x ∈ (ι Q).range * (ι Q).range
⊢ motive (x * y * b) ⋯

Tactic:
induction hx2 using Submodule.mul_induction_on' with

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
ι : ∀ (v : M), P ((CliffordAlgebra.ι Q) v) ⋯
add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) (hy : y ∈ evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1),
    P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
⊢ P x hx

Tactic:
by
  refine evenOdd_induction _ _ (motive := P) (fun ιv => ?_) add ι_mul_ι_mul x hx
  simp_rw [ZMod.val_one, pow_one]
  rintro ⟨v, rfl⟩
  exact ι v

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

Goal state before:
pp: case refine_2
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
⊢ x = 0 ∧ r = 0 → (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r

Tactic:
rintro ⟨rfl, rfl⟩
    rw [map_zero, map_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : HasInjectiveDimensionLT X n
i : ℕ
hi : n ≤ i
Y : C
⊢ Subsingleton (Ext Y X i)

Tactic:
by
  let := HasExt.standard C
  have := hX.subsingleton' i hi
  exact Ext.chgUniv.{w, max u v}.symm.subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext Y X i
⊢ e.comp (Ext.mk₀ (𝟙 X)) ⋯ = 0

Tactic:
hX.eq_zero_of_tgt (𝟙 X),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext Y X i
⊢ e.comp (Ext.mk₀ 0) ⋯ = 0