mathlib-initiative/mathlib-tactics huggingface dataset:
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₁.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_1.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_1.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.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
⊢ iCycles K i ≫ π.f i =
    cyclesMap π i ≫
      (singleObjCyclesSelfIso (ComplexShape.up ℤ) i P).hom ≫
        (singleObjCyclesSelfIso (ComplexShape.up ℤ) i P).inv ≫ ((single C (ComplexShape.up ℤ) i).obj P).iCycles i

Tactic:
Iso.hom_inv_id_assoc,

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
⊢ iCycles K i ≫ π.f i = cyclesMap π i ≫ ((single C (ComplexShape.up ℤ) i).obj P).iCycles i
Module: Mathlib.CategoryTheory.Shift.Linear

Goal state before:
pp: R : Type u_1
inst✝¹³ : Ring R
C : Type u_4
inst✝¹² : Category.{v_1, u_4} C
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Linear R C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : Linear R D
M : Type u_3
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : ∀ (n : M), Functor.Linear R (shiftFunctor C n)
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
inst✝² : Functor.Linear R L
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
⊢ Functor.Linear R (shiftFunctor D n)

Tactic:
have : Localization.Lifting L W (shiftFunctor C n ⋙ L) (shiftFunctor D n) :=
    ⟨(L.commShiftIso n).symm⟩
  rw [← Localization.functor_linear_iff L W R (shiftFunctor C n ⋙ L) (shiftFunctor D n)]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.CharP.Reduced

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p n : ℕ
inst✝ : ExpChar R p
x y : R
H : (iterateFrobenius R p n) x - (iterateFrobenius R p n) y = 0
⊢ x - y = 0

Tactic:
simp_rw [iterateFrobenius_def, ← sub_pow_expChar_pow] at H

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p n : ℕ
inst✝ : ExpChar R p
x y : R
H : (x - y) ^ p ^ n = 0
⊢ x - y = 0
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : LinearIndependent R v
A : Matrix κ ι R
hA : A.Nondegenerate
⊢ LinearIndependent R fun i ↦ ∑ j, A i j • v j

Tactic:
have : Fintype κ := Fintype.ofFinite _
  rw [Fintype.linearIndependent_iff] at hv ⊢
  intro w hw
  suffices w = 0 by aesop
  simp_rw [Finset.smul_sum, ← smul_assoc] at hw
  rw [Finset.sum_comm] at hw
  simp_rw [← Finset.sum_smul] at hw
  replace hv : w ᵥ* A = 0 := funext <| hv _ hw
  replace hv (w' : ι → R) : w ⬝ᵥ A *ᵥ w' = 0 := by
    simpa [Matrix.dotProduct_mulVec] using congr_arg (fun x ↦ dotProduct x w') hv
  exact hA.eq_zero_of_ortho hv

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

Goal state before:
pp: K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
hv₂ : ∀ (i : Fin (finrank K V)), (((associatedHom K) Q) (v i)) (v i) ≠ 0
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)

Tactic:
simp_rw [associated_eq_self_apply] at hv₂

Goal state after:
K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
hv₂ : ∀ (i : Fin (finrank K V)), Q (v i) ≠ 0
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: ι✝ : Type u_1
R✝ : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : Field K
inst✝⁹ : Invertible 2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
inst✝⁶ : FiniteDimensional K V
ι : Type u_10
S : Type u_11
R : Type u_12
inst✝⁵ : Fintype ι
inst✝⁴ : CommSemiring R
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R R
w w' : ι → S
u : ι → Sˣ
h : ∀ (i : ι), w' i * ↑(u i) ^ 2 = w i
x : ι → R
j : ι
hj : j ∈ Finset.univ
⊢ (w' j * ↑(u j * u j)) • (x j * x j) = w j • (x j * x j)

Tactic:
← pow_two,

Goal state after:
ι✝ : Type u_1
R✝ : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : Field K
inst✝⁹ : Invertible 2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
inst✝⁶ : FiniteDimensional K V
ι : Type u_10
S : Type u_11
R : Type u_12
inst✝⁵ : Fintype ι
inst✝⁴ : CommSemiring R
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R R
w w' : ι → S
u : ι → Sˣ
h : ∀ (i : ι), w' i * ↑(u i) ^ 2 = w i
x : ι → R
j : ι
hj : j ∈ Finset.univ
⊢ (w' j * ↑(u j ^ 2)) • (x j * x j) = w j • (x j * x j)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring S₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring S₂
inst✝¹⁰ : AddCommMonoid N₂
inst✝⁹ : Module R N₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
⊢ (toMatrix₂Aux R (fun i ↦ Pi.single i 1) fun j ↦ Pi.single j 1) (toLinearMap₂'Aux σ₁ σ₂ f) = f

Tactic:
by
  ext i j
  simp_rw [LinearMap.toMatrix₂Aux_apply, Matrix.toLinearMap₂'Aux_single]

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

Goal state before:
pp: case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih : (of A (tail.dProdIndex fι)) (tail.dProd fι fA) = (List.map (fun a ↦ (of A (fι a)) (fA a)) tail).prod
⊢ (of A ((head :: tail).dProdIndex fι)) (GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA)) =
    (of A (fι head)) (fA head) * (of A (tail.dProdIndex fι)) (tail.dProd fι fA)

Tactic:
DirectSum.of_mul_of (fA head)

Goal state after:
case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih : (of A (tail.dProdIndex fι)) (tail.dProd fι fA) = (List.map (fun a ↦ (of A (fι a)) (fA a)) tail).prod
⊢ (of A ((head :: tail).dProdIndex fι)) (GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA)) =
    (of A (fι head + tail.dProdIndex fι)) (GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA))
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
α : Type u_3
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ (of A (l.dProdIndex fι)) (l.dProd fι fA) = (List.map (fun a ↦ (of A (fι a)) (fA a)) l).prod

Tactic:
by
  induction l with
  | nil => simp only [List.map_nil, List.prod_nil, List.dProd_nil]; rfl
  | cons head tail =>
    rename_i ih
    simp only [List.map_cons, List.prod_cons, List.dProd_cons, ← ih]
    rw [DirectSum.of_mul_of (fA head)]
    rfl

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✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ ∀ (i : ι) (y : A i), ((mulHom A) ((of A ai) ax)) ((of A i) y) = ((mulHom A).flip ((of A ai) ax)) ((of A i) y)

Tactic:
intro bi

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
⊢ ∀ (y : A bi), ((mulHom A) ((of A ai) ax)) ((of A bi) y) = ((mulHom A).flip ((of A ai) ax)) ((of A bi) y)
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) +
        (((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))

Tactic:
Sym2.mkEmbedding_apply,

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 ¬s(a, a).IsDiag then polarSym2 (⇑Q) (Sym2.map f s(a, a)) else 0) +
            ∑ x ∈ s, if ¬s(a, x).IsDiag then polarSym2 (⇑Q) (Sym2.map f s(a, x)) else 0) +
          ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0))
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
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✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ (b₁.toMatrix ⇑c₁)ᵀ * (toMatrix₂ b₁ b₂) B * b₂.toMatrix ⇑c₂ = (toMatrix₂ c₁ c₂) B

Tactic:
by
  simp_rw [← LinearMap.toMatrix_id_eq_basis_toMatrix]
  rw [← LinearMap.toMatrix₂_compl₁₂, LinearMap.compl₁₂_id_id]

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

Tactic:
Sym2.mkEmbedding_apply,

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 s(a, a)) + ∑ x ∈ s, polarSym2 (⇑Q) (Sym2.map f s(a, x)) +
        ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) -
      (Q (f a) + ∑ i ∈ s, Q (f i))
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✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
N' : Type u_8
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
B : BilinMap R M N
a : R
x : M
⊢ (B (a • x)) (a • x) = (a * a) • (B x) x

Tactic:
simp only [map_smul, LinearMap.smul_apply, smul_smul]

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✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x : M
⊢ (((associatedHom S) Q) x) x = Q x

Tactic:
rw [associated_apply, map_add_self, ← three_add_one_eq_four, ← two_add_one_eq_three, add_smul,
    add_smul, one_smul, add_sub_cancel_right, add_sub_cancel_right, two_smul, ← two_smul R,
    invOf_smul_eq_iff, two_smul, two_smul]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
Q : QuadraticMap R M N
inst✝ : Invertible 2
x y : M
⊢ ((associated Q) x) y = 0 ↔ Q.IsOrtho x y

Tactic:
simp_rw [isOrtho_def, associated_apply, invOf_smul_eq_iff, smul_zero, sub_sub, sub_eq_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
n : N
m : M
x : CliffordAlgebra Q
⊢ (((foldr'Aux Q f) m) (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x)).2 =
    (f m) (x, (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).2)

Tactic:
foldr'Aux_apply_apply

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
n : N
m : M
x : CliffordAlgebra Q
⊢ ((ι Q) m * (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).1, (f m) (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x)).2 =
    (f m) (x, (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).2)
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
x : ExteriorAlgebra R M
⊢ (liftAlternating f) ((ι R) m * x) = (liftAlternating fun i ↦ (f i.succ).curryLeft m) x

Tactic:
dsimp [liftAlternating]
  rw [foldl_mul, foldl_ι]
  rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
v : ι → ↑S.X₁
hv : LinearIndependent R v
w : ι' → ↑S.X₃
hw : LinearIndependent R w
⊢ LinearIndependent R (Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w))

Tactic:
apply linearIndependent_leftExact hS'.exact hv _ hS'.mono_f rfl

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
v : ι → ↑S.X₁
hv : LinearIndependent R v
w : ι' → ↑S.X₃
hw : LinearIndependent R w
⊢ LinearIndependent R
    (⇑(ConcreteCategory.hom S.g) ∘
      Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w) ∘ Sum.inr)
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
⊢ ⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s} ⊆ ↑(⋀[R]^n M)

Tactic:
rintro - ⟨y, ⟨y_mem, rfl⟩⟩

Goal state after:
case a
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
y : Fin n → M
y_mem : y ∈ {a | range a ⊆ s}
⊢ (ExteriorAlgebra.ιMulti R n) y ∈ ↑(⋀[R]^n M)
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d), d = n + k → e = 0
Y : C
p : ProjectivePresentation Y
h : { X₁ := kernel p.f, X₂ := p.p, X₃ := Y, f := kernel.ι p.f, g := p.f, zero := ⋯ }.ShortExact
e : Ext Y X (n + k + 1)
hd : n + k + 1 = n + (k + 1)
⊢ (Ext.mk₀ { X₁ := kernel p.f, X₂ := p.p, X₃ := Y, f := kernel.ι p.f, g := p.f, zero := ⋯ }.g).comp e ⋯ = 0

Tactic:
apply Ext.eq_zero_of_projective

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X : Cᵒᵖ
⊢ limMap (F.whiskerLeft (restriction R (𝟙 X))) =
    (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (limit (F ⋙ evaluation R X))).inv ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).hom

Tactic:
apply limit.hom_ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X : Cᵒᵖ
⊢ ∀ (j : J),
    limMap (F.whiskerLeft (restriction R (𝟙 X))) ≫
        limit.π (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) j =
      ((ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (limit (F ⋙ evaluation R X))).inv ≫
          (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).hom) ≫
        limit.π (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) j
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ limMap (F.whiskerLeft (restriction R (f ≫ g))) =
    limMap (F.whiskerLeft (restriction R f)) ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (limMap (F.whiskerLeft (restriction R g)) ≫
              (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (limit (F ⋙ evaluation R Z))).inv ≫
            (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)).hom

Tactic:
apply limit.hom_ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (j : J),
    limMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
        limit.π (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j =
      (limMap (F.whiskerLeft (restriction R f)) ≫
          (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                (limMap (F.whiskerLeft (restriction R g)) ≫
                  (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g)))
                      (F ⋙ evaluation R Z)).inv) ≫
              (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                    (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (limit (F ⋙ evaluation R Z))).inv ≫
                (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g))))
                    (F ⋙ evaluation R Z)).hom) ≫
        limit.π (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j