mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: case comm₁₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
this✝ : HasDerivedCategory C := ⋯
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₂,
            X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
            X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
            f := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).map hS.singleTriangle.mor₂,
            g :=
              (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯,
            zero := ⋯ }.f)
    ⇑(ConcreteCategory.hom
        { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₂,
            X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
            X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
            f := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).map hS.singleTriangle.mor₂,
            g :=
              (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯,
            zero := ⋯ }.g)
⊢ (ConcreteCategory.hom
          { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₂,
              X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
              X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
              f := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).map hS.singleTriangle.mor₂,
              g :=
                (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁
                  ⋯,
              zero := ⋯ }.f).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (ConcreteCategory.hom
        { X₁ := AddCommGrpCat.of (Ext X S.X₂ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₃ n₀),
            X₃ := AddCommGrpCat.of (Ext X S.X₁ n₁), f := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯),
            g := AddCommGrpCat.ofHom (hS.extClass.postcomp X h), zero := ⋯ }.f)

Tactic:
ext x; apply hom_comp_singleFunctor_map_shift (C := C)

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

Goal state before:
pp: case comm₂₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
this✝ : HasDerivedCategory C := ⋯
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
            X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
            X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₂,
            f :=
              (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯,
            g := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).map hS.singleTriangle.mor₁,
            zero := ⋯ }.f)
    ⇑(ConcreteCategory.hom
        { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
            X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
            X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₂,
            f :=
              (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯,
            g := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).map hS.singleTriangle.mor₁,
            zero := ⋯ }.g)
⊢ (ConcreteCategory.hom
          { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
              X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
              X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₂,
              f :=
                (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁
                  ⋯,
              g := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).map hS.singleTriangle.mor₁,
              zero := ⋯ }.g).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (ConcreteCategory.hom
        { X₁ := AddCommGrpCat.of (Ext X S.X₃ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₁ n₁),
            X₃ := AddCommGrpCat.of (Ext X S.X₂ n₁), f := AddCommGrpCat.ofHom (hS.extClass.postcomp X h),
            g := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), zero := ⋯ }.g)

Tactic:
ext x; apply hom_comp_singleFunctor_map_shift (C := C)

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

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

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

Goal state before:
pp: case mpr
K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h : (B x) y = 0
z : K
⊢ (RingHom.id K) z = 0 ∨ (B x) y = 0

Tactic:
exact Or.intro_right _ h

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
r : relations.R
⊢ (Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)) (relations.relation r) = 0

Tactic:
have : π = Finsupp.linearCombination _ (fun g ↦ π (Finsupp.single g 1)) := by ext; simp

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
r : relations.R
this : π = Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)
⊢ (Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)) (relations.relation r) = 0
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
e : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : ι → M
i✝ j✝ : ι
⊢ e.toMatrix v i✝ j✝ = (LinearMap.toMatrix e e) ((e.constr ℕ) v) i✝ j✝

Tactic:
Basis.toMatrix_apply,

Goal state after:
ι : Type u_1
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
e : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : ι → M
i✝ j✝ : ι
⊢ (e.repr (v j✝)) i✝ = (LinearMap.toMatrix e e) ((e.constr ℕ) v) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
⊢ (e.repr (update v j x k)) i' = if k = j then (e.repr x) i' else (e.repr (v k)) i'

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : k = j
⊢ (e.repr (update v j x k)) i' = (e.repr x) i'

case neg
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : ¬k = j
⊢ (e.repr (update v j x k)) i' = (e.repr (v k)) i'
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst✝⁴ : CommSemiring R₁
inst✝³ : Semiring S
inst✝² : Algebra R₁ S
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
i✝ j✝ : ι
⊢ b.toMatrix (x • w) i✝ j✝ = ((Algebra.leftMulMatrix b) x * b.toMatrix w) i✝ j✝

Tactic:
Basis.toMatrix_apply,

Goal state after:
ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst✝⁴ : CommSemiring R₁
inst✝³ : Semiring S
inst✝² : Algebra R₁ S
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
i✝ j✝ : ι
⊢ (b.repr ((x • w) j✝)) i✝ = ((Algebra.leftMulMatrix b) x * b.toMatrix w) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝¹¹ : CommRing R₂
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
S : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : Algebra R₂ S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R₂ S M₂
inst✝¹ : IsDomain R₂
inst✝ : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range ⇑b))
i✝ j✝ : ι
⊢ (algebraMap R₂ S) ((restrictScalars R₂ b).toMatrix v i✝ j✝) = b.toMatrix (fun i ↦ ↑(v i)) i✝ j✝

Tactic:
Basis.toMatrix_apply,

Goal state after:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝¹¹ : CommRing R₂
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
S : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : Algebra R₂ S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R₂ S M₂
inst✝¹ : IsDomain R₂
inst✝ : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range ⇑b))
i✝ j✝ : ι
⊢ (algebraMap R₂ S) (((restrictScalars R₂ b).repr (v j✝)) i✝) = b.toMatrix (fun i ↦ ↑(v i)) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
N : Type u_9
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
b : Basis ι R M
c : Basis κ R N
f : M →ₗ[R] N
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Finite κ
⊢ (LinearMap.toMatrix b c) f = c.toMatrix (⇑f ∘ ⇑b)

Tactic:
ext; simp [LinearMap.toMatrix_apply, toMatrix_apply]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
⊢ ∑ g, f g = ↑(if f = 1 then Fintype.card G else 0)

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : f = 1
⊢ ∑ g, f g = ↑(Fintype.card G)

case neg
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g, f g = ↑0
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h2 : ∀ (i : n), 0 < ∑ j, A i j
⊢ Aᵀ.det ≠ 0

Tactic:
refine det_ne_zero_of_sum_col_pos ?_ ?_

Goal state after:
case refine_1
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h2 : ∀ (i : n), 0 < ∑ j, A i j
⊢ Pairwise fun i j ↦ Aᵀ i j < 0

case refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h2 : ∀ (i : n), 0 < ∑ j, A i j
⊢ ∀ (j : n), 0 < ∑ i, Aᵀ i j
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x : SpecialLinearGroup n R
x✝ : x ∈ center (SpecialLinearGroup n R)
⊢ x ∈ ⊥

Tactic:
mem_bot,

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x : SpecialLinearGroup n R
x✝ : x ∈ center (SpecialLinearGroup n R)
⊢ x = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hA : A ∈ center (SpecialLinearGroup n R)
i : n
⊢ (scalar n) (↑A i i) = ↑A

Tactic:
obtain ⟨r : R, hr : scalar n r = A⟩ := mem_range_scalar_of_commute_transvectionStruct fun t ↦
    Subtype.ext_iff.mp <| Subgroup.mem_center_iff.mp hA ⟨t.toMatrix, by simp⟩
  simp [← congr_fun₂ hr i i, ← hr]

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

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : ↥(center (SpecialLinearGroup n R))
⊢ ↑↑A =
    (scalar n)
      ↑↑((if hp : IsEmpty n then (fun hn ↦ ⋯.mpr (⋯.mpr (⋯.mpr (⋯.mpr MulEquiv.ofUnique)))) hp
            else (fun x ↦ ⋯ ▸ center_equiv_rootsOfUnity' (Classical.arbitrary n)) ⋯)
            A)

Tactic:
split_ifs with h

Goal state after:
case pos
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : ↥(center (SpecialLinearGroup n R))
h : IsEmpty n
⊢ ↑↑A = (scalar n) ↑↑(((fun hn ↦ ⋯.mpr (⋯.mpr (⋯.mpr (⋯.mpr MulEquiv.ofUnique)))) h) A)

case neg
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : ↥(center (SpecialLinearGroup n R))
h : ¬IsEmpty n
⊢ ↑↑A = (scalar n) ↑↑(((fun x ↦ ⋯ ▸ center_equiv_rootsOfUnity' (Classical.arbitrary n)) ⋯) A)
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
n : ℕ
⊢ (of A 0) (GSemiring.natCast (n + 1)) = (of A 0) (GSemiring.natCast n) + 1

Tactic:
GSemiring.natCast_succ

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
n : ℕ
⊢ (of A 0) (GSemiring.natCast n + GradedMonoid.GOne.one) = (of A 0) (GSemiring.natCast n) + 1
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case e_f.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✝¹ x✝ : ι
⊢ ↑(((of (fun i ↦ ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) =
    if x✝¹ + x✝ = n then ↑(r x✝¹) * ↑(r' x✝) else 0

Tactic:
split_ifs with h

Goal state after:
case pos
ι : 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✝¹ x✝ : ι
h : x✝¹ + x✝ = n
⊢ ↑(((of (fun i ↦ ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) = ↑(r x✝¹) * ↑(r' x✝)

case neg
ι : 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✝¹ x✝ : ι
h : ¬x✝¹ + x✝ = n
⊢ ↑(((of (fun i ↦ ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) = 0
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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (∑ x ∈ DFinsupp.support r', if i + x = n then ↑r * ↑(r' x) else 0) = ↑r * ↑(r' j)

Tactic:
H,

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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (∑ x ∈ DFinsupp.support r', if x = j then ↑r * ↑(r' x) else 0) = ↑r * ↑(r' j)
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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (if j ∈ DFinsupp.support r' then ↑r * ↑(r' j) else 0) = ↑r * ↑(r' j)

Tactic:
split_ifs with h

Goal state after:
case pos
ι : 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : j ∈ DFinsupp.support r'
⊢ ↑r * ↑(r' j) = ↑r * ↑(r' j)

case neg
ι : 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : j ∉ DFinsupp.support r'
⊢ 0 = ↑r * ↑(r' j)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ associated sq = mul R R

Tactic:
by
  rw [sq, associated_linMulLin]
  simp only [smul_add, invOf_two_smul_add_invOf_two_smul]
  rfl

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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (∑ x ∈ DFinsupp.support r, if x + i = n then ↑(r x) * ↑r' else 0) = ↑(r j) * ↑r'

Tactic:
H,

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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (∑ x ∈ DFinsupp.support r, if x = j then ↑(r x) * ↑r' else 0) = ↑(r j) * ↑r'
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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (if j ∈ DFinsupp.support r then ↑(r j) * ↑r' else 0) = ↑(r j) * ↑r'

Tactic:
split_ifs with h

Goal state after:
case pos
ι : 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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
h : j ∈ DFinsupp.support r
⊢ ↑(r j) * ↑r' = ↑(r j) * ↑r'

case neg
ι : 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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
h : j ∉ DFinsupp.support r
⊢ 0 = ↑(r j) * ↑r'
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✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
⊢ ↑((r * (of (fun i ↦ ↥(A i)) i) r') n) = if i ≤ n then ↑(r (n - i)) * ↑r' else 0

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
h : i ≤ n
⊢ ↑((r * (of (fun i ↦ ↥(A i)) i) r') n) = ↑(r (n - i)) * ↑r'

case neg
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
h : ¬i ≤ n
⊢ ↑((r * (of (fun i ↦ ↥(A i)) i) r') n) = 0
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✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
⊢ ↑(((of (fun i ↦ ↥(A i)) i) r * r') n) = if i ≤ n then ↑r * ↑(r' (n - i)) else 0

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
h : i ≤ n
⊢ ↑(((of (fun i ↦ ↥(A i)) i) r * r') n) = ↑r * ↑(r' (n - i))

case neg
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
h : ¬i ≤ n
⊢ ↑(((of (fun i ↦ ↥(A i)) i) r * r') n) = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

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
x : CliffordAlgebra Q
h : x ∈ evenOdd Q 1
⊢ involute x = -x

Tactic:
induction x, h using odd_induction with
  | ι m => exact involute_ι _
  | add x y _hx _hy ihx ihy =>
    rw [map_add, ihx, ihy, neg_add]
  | ι_mul_ι_mul m₁ m₂ x _hx ihx =>
    rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg, mul_neg]

Goal state after: