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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.op f.op ⋯ ≫ (kernelSubobject f.op).arrow =
    ((imageSubobjectIso g.op ≪≫ (imageOpOp g).symm).hom ≫
        (cokernel.desc f (factorThruImage g) ⋯).op ≫ (kernelSubobjectIso f.op ≪≫ kernelOpOp f).inv) ≫
      (kernelSubobject f.op).arrow

Tactic:
simp only [Iso.trans_hom, Iso.symm_hom, Iso.trans_inv, kernelOpOp_inv, Category.assoc,
    imageToKernel_arrow, kernelSubobject_arrow', kernel.lift_ι, ← op_comp, cokernel.π_desc,
    ← imageSubobject_arrow, ← imageUnopOp_inv_comp_op_factorThruImage g.op]

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (imageSubobjectIso g.op).hom ≫ (imageUnopOp g.op).inv ≫ (factorThruImage g.op.unop).op =
    (imageSubobjectIso g.op).hom ≫ (imageOpOp g).inv ≫ (factorThruImage g).op
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

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.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryGE i
⊢ (K.restrictionToTruncGE' e).f i = (K.restrictionXIso e hi').hom ≫ (K.truncGE'XIso e hi' hi).inv

Tactic:
apply restrictionToTruncGE'.f_eq_iso_hom_iso_inv

Goal state after:
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))
⊢ 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 s 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)
⊢ 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.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : CochainComplex C ℤ
inst✝¹ : CategoryWithHomology C
n : ℤ
inst✝ : K.IsGE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : i < n'
⊢ IsZero (homology ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) i)

Tactic:
exact IsZero.of_iso (K.isZero_of_isGE n (a + i) (by lia))
    (((homologyFunctor C _ (0 : ℤ)).shiftIso a i _ rfl).app K)

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 : 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

Tactic:
have eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') (zero_add n) := by
    simp [α', β']

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 β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
⊢ (α + β).hom = α.hom + β.hom
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

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

Tactic:
refine exact_of_δ₀ (hR₂.exact 0).exact_toComposableArrows (exact_of_δ₀ ?_ ?_)

Goal state after:
case refine_2.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₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₂ ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
      ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact

case refine_2.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.Exact
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ (m + n)).obj (Opposite.op X)
⊢ (opEquiv' (m + n) a a'' ⋯).symm x =
    (opEquiv' m a' a'' ha'').symm
      (Quiver.Hom.op ((opEquiv' n a a' ha').symm (x ≫ (shiftFunctorAdd Cᵒᵖ m n).hom.app (Opposite.op X))))

Tactic:
by
  simp only [opEquiv'_symm_apply, opEquiv_symm_apply,
    opShiftFunctorEquivalence_add_unitIso_inv_app_eq _ _ _ _ (add_comm n m)]
  dsimp
  simp only [assoc, Functor.map_comp, ← shiftFunctorAdd'_eq_shiftFunctorAdd,
    ← NatTrans.naturality_assoc,
    shiftFunctorAdd'_assoc_inv_app a n m a' (m + n) a'' (by lia) (by lia) (by lia)]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Yoneda

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
B : C
T : Triangle Cᵒᵖ
hT : T ∈ distinguishedTriangles
⊢ ∀ (x₂ : ↑((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).X₂),
    (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).g) x₂ = 0 →
      ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).f) x₁ = x₂

Tactic:
intro (x₂ : T.obj₂.unop ⟶ B) (hx₂ : T.mor₂.unop ≫ x₂ = 0)

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
B : C
T : Triangle Cᵒᵖ
hT : T ∈ distinguishedTriangles
x₂ : unop T.obj₂ ⟶ B
hx₂ : T.mor₂.unop ≫ x₂ = 0
⊢ ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).f) x₁ = x₂
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y : C
n : ℕ
x : Ext X Y n
r : R
this : HasDerivedCategory C := ⋯
⊢ (r • x).hom = (x.comp (mk₀ (r • 𝟙 Y)) ⋯).hom

Tactic:
apply ((Equiv.linearEquiv R homEquiv).map_smul r x).trans

Goal state after:
R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y : C
n : ℕ
x : Ext X Y n
r : R
this : HasDerivedCategory C := ⋯
⊢ r • (Equiv.linearEquiv R homEquiv) x = (x.comp (mk₀ (r • 𝟙 Y)) ⋯).hom
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
⊢ LeftInverse (fun m j ↦ ∑ i, m i j • e i) e.toMatrix

Tactic:
intro v

Goal state after:
ι : 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
v : ι → M
⊢ (fun m j ↦ ∑ i, m i j • e i) (e.toMatrix v) = v
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: 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
hg' : (algebraMap R[X] K) g ≠ 0
⊢ (algebraMap R[X] K) f = (algebraMap R[X] K) g * (algebraMap R[X] K) (f /ₘ g) + (algebraMap R[X] K) (f %ₘ g)

Tactic:
add_comm,

Goal state after:
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
hg' : (algebraMap R[X] K) g ≠ 0
⊢ (algebraMap R[X] K) f = (algebraMap R[X] K) (f %ₘ g) + (algebraMap R[X] K) g * (algebraMap R[X] K) (f /ₘ g)
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Finite ↥(rootsOfUnity k R)

Tactic:
exact .of_equiv { x // x ∈ nthRoots k (1 : R) } (rootsOfUnityEquivNthRoots R k).symm

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

Goal state before:
pp: case mp.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 → A
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
h : (fun i ↦ (algebraMap A K) (v i)) = 0
i : n
⊢ v i = 0 i

Tactic:
exact IsFractionRing.to_map_eq_zero_iff.mp (congr_fun h i)

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
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ det ((map f) g) = (Units.map ↑f) (det g)

Tactic:
ext
  simp only [map,
    Matrix.GeneralLinearGroup.val_det_apply, Units.coe_map, MonoidHom.coe_coe]
  exact Eq.symm (RingHom.map_det f g.1)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
⊢ IsCoprime ((v ᵥ* ↑A) 0) ((v ᵥ* ↑A) 1)

Tactic:
have : v = g 0 := funext fun t ↦ by { fin_cases t <;> tauto }

Goal state after:
R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
this : v = ↑g 0
⊢ IsCoprime ((v ᵥ* ↑A) 0) ((v ᵥ* ↑A) 1)
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
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ x * (ι Q) a * (ι Q) b = -(x * (ι Q) b * (ι Q) a)

Tactic:
by
  rw [mul_assoc, ι_mul_ι_comm_of_isOrtho h, mul_neg, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : CommMonoid R
inst✝¹ : AddCommMonoid ι
A : ι → S
inst✝ : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
j : κ
F' : Finset κ
hF2 : j ∉ F'
h3 : (∀ k ∈ F', g k ∈ A (i k)) → ∏ k ∈ F', g k ∈ A (∑ k ∈ F', i k)
hF : ∀ k ∈ insert j F', g k ∈ A (i k)
⊢ g j * ∏ x ∈ F', g x ∈ A (i j + ∑ x ∈ F', i x)

Tactic:
apply SetLike.mul_mem_graded (by grind)

Goal state after:
ι : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : CommMonoid R
inst✝¹ : AddCommMonoid ι
A : ι → S
inst✝ : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
j : κ
F' : Finset κ
hF2 : j ∉ F'
h3 : (∀ k ∈ F', g k ∈ A (i k)) → ∏ k ∈ F', g k ∈ A (∑ k ∈ F', i k)
hF : ∀ k ∈ insert j F', g k ∈ A (i k)
⊢ ∏ x ∈ F', g x ∈ A (∑ x ∈ F', i x)
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
⊢ associator = 0 ↔ Std.Associative fun x y ↦ x * y

Tactic:
simp [mulLeft₃_eq_mulRight₃_iff_associative, associator, sub_eq_zero]

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

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
⊢ AddMonoidHom.mul ((of A 0) (GAlgebra.toFun r)) = AddMonoidHom.mul.flip ((of A 0) (GAlgebra.toFun r))

Tactic:
ext i xi : 2

Goal state after:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ((AddMonoidHom.mul ((of A 0) (GAlgebra.toFun r))).comp (of A i)) xi =
    ((AddMonoidHom.mul.flip ((of A 0) (GAlgebra.toFun r))).comp (of A i)) xi
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
⊢ DistribSMul.toAddMonoidHom (⨁ (i : ι), A i) r = AddMonoidHom.mul ((of A 0) (GAlgebra.toFun r))

Tactic:
ext i xi : 2

Goal state after:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ((DistribSMul.toAddMonoidHom (⨁ (i : ι), A i) r).comp (of A i)) xi =
    ((AddMonoidHom.mul ((of A 0) (GAlgebra.toFun r))).comp (of A i)) xi
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 : ℕ
fι : Fin n → ι
fA : (a : Fin n) → A (fι a)
⊢ (List.ofFn fun a ↦ (of A (fι a)) (fA a)).prod =
    (of A ((List.finRange n).dProdIndex fι)) ((List.finRange n).dProd fι fA)

Tactic:
by
  rw [List.ofFn_eq_map, ofList_dProd]

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 y : M
⊢ f (x + y) = f x + f y + polar f x y

Tactic:
rw [polar]

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ f (x + y) = f x + f y + (f (x + y) - f x - f y)
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 y : M
⊢ f (x + y) - f x - f y = f (y + x) - f y - f x

Tactic:
add_comm,

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ f (y + x) - f x - f y = f (y + x) - f y - f x
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 ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p q : P
hp : SetLike.IsHomogeneous ℳ p
hq : SetLike.IsHomogeneous ℳ q
hpq : ∀ (i : ι), ∀ m ∈ ℳ i, m ∈ p ↔ m ∈ q
m : M
⊢ (∀ (i : ι), ↑(((decompose ℳ) m) i) ∈ p) ↔ m ∈ q

Tactic:
AddSubmonoidClass.IsHomogeneous.mem_iff ℳ q hq

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 ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p q : P
hp : SetLike.IsHomogeneous ℳ p
hq : SetLike.IsHomogeneous ℳ q
hpq : ∀ (i : ι), ∀ m ∈ ℳ i, m ∈ p ↔ m ∈ q
m : M
⊢ (∀ (i : ι), ↑(((decompose ℳ) m) i) ∈ p) ↔ ∀ (i : ι), ↑(((decompose ℳ) m) i) ∈ q
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Invertible 2
m : M
⊢ ⅟2 • 2 • m = m

Tactic:
rw [← ofNat_smul_eq_nsmul R, invOf_smul_smul (2 : R) m]

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

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
⊢ (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)

Tactic:
let u := P.nonsingInvUnit h'

Goal state after:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
⊢ (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)
Module: Mathlib.Algebra.DirectSum.Internal

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

Tactic:
rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]

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

Goal state before:
pp: case mem.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)
x✝ : CliffordAlgebra Q
i : ℕ
x : CliffordAlgebra Q
r : R
⊢ P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)

Tactic:
exact algebraMap r

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

Goal state before:
pp: case mem.mem_mul.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ 1 + ↑i = ↑(i + 1)

Tactic:
add_comm,

Goal state after:
case mem.mem_mul.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ ↑i + 1 = ↑(i + 1)
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
⊢ ⨆ i, (ι Q).range ^ i = iSup (evenOdd Q)

Tactic:
eq_comm

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
⊢ iSup (evenOdd Q) = ⨆ i, (ι Q).range ^ i
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
a b : α
hα : ↑n < 1 + {b}ᶜ.encard
hab : a ≠ b
⊢ ↑n ≤ {b}ᶜ.encard

Tactic:
add_comm,

Goal state after:
α : Type u_1
n : ℕ
hn : 1 ≤ n
a b : α
hα : ↑n < {b}ᶜ.encard + 1
hab : a ≠ b
⊢ ↑n ≤ {b}ᶜ.encard
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: ι : Type u_8
inst✝⁴ : Fintype ι
R : Type u_9
M : Type u_10
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
w : ι → R
⊢ (basisRepr Q v) w = (weightedSumSquares R fun i ↦ Q (v i)) w

Tactic:
rw [basisRepr_apply, ← @associated_eq_self_apply R, map_sum, weightedSumSquares_apply]

Goal state after:
ι : Type u_8
inst✝⁴ : Fintype ι
R : Type u_9
M : Type u_10
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
w : ι → R
⊢ ∑ x, (((associatedHom R) Q) (∑ i, w i • v i)) (w x • v x) = ∑ i, Q (v i) • (w i * w i)
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
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (CliffordAlgebra Q)) r) ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) (hy : y ∈ evenOdd Q 0),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
r : R
h : (Algebra.algebraMap R (CliffordAlgebra Q)) r ∈ (ι Q).range ^ ZMod.val 0
⊢ motive ((Algebra.algebraMap R (CliffordAlgebra Q)) r) ⋯

Tactic:
exact algebraMap r

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

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ ∀ (y : Fin n → M), (ιMulti R n) y ∈ ↑(⋀[R]^n M)

Tactic:
intro v

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ (ιMulti R n) v ∈ ↑(⋀[R]^n M)