mathlib-initiative/mathlib-tactics huggingface dataset:
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₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ { 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 := ⋯ }.Exact

Tactic:
let := HasDerivedCategory.standard C

Goal state after:
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 := HasDerivedCategory.standard C
⊢ { 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 := ⋯ }.Exact
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
⊢ r • x = x.comp (mk₀ (r • 𝟙 Y)) ⋯

Tactic:
let := HasDerivedCategory.standard C

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 := HasDerivedCategory.standard C
⊢ r • x = x.comp (mk₀ (r • 𝟙 Y)) ⋯
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 Z : C
a b : ℕ
α : Ext X Y a
β : Ext Y Z b
c : ℕ
h : a + b = c
r : R
⊢ α.comp (r • β) h = r • α.comp β h

Tactic:
let := HasDerivedCategory.standard C

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 Z : C
a b : ℕ
α : Ext X Y a
β : Ext Y Z b
c : ℕ
h : a + b = c
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp (r • β) h = r • α.comp β h
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 Z : C
a b : ℕ
α : Ext X Y a
β : Ext Y Z b
c : ℕ
h : a + b = c
r : R
⊢ (r • α).comp β h = r • α.comp β h

Tactic:
let := HasDerivedCategory.standard C

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 Z : C
a b : ℕ
α : Ext X Y a
β : Ext Y Z b
c : ℕ
h : a + b = c
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (r • α).comp β h = r • α.comp β h
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
r : R
f : X ⟶ Y
⊢ mk₀ (r • f) = r • mk₀ f

Tactic:
let := HasDerivedCategory.standard C

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
r : R
f : X ⟶ Y
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ mk₀ (r • f) = r • mk₀ f
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M N : ModuleCat R
r : R
mem_ann : r ∈ Module.annihilator R ↑N
n : ℕ
⊢ AddCommGrpCat.ofHom ((mk₀ (r • 𝟙 M)).postcomp N ⋯) = 0

Tactic:
ext h
  have : r • 𝟙 N = 0 := by
    simp [← ModuleCat.lsmul_eq_smul_id, Module.mem_annihilator_iff_lsmul_eq_zero.mp mem_ann]
  have smul_eq : r • h = (Ext.mk₀ (r • 𝟙 N)).comp h (zero_add n) := by simp [Ext.mk₀_smul]
  simp [Ext.mk₀_smul, this, smul_eq]

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₁ := AddCommGrpCat.of (Ext S.X₃ Y n), X₂ := AddCommGrpCat.of (Ext S.X₂ Y n), X₃ := AddCommGrpCat.of (Ext S.X₁ Y n),
      f := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
      zero := ⋯ }.Exact

Tactic:
let := HasDerivedCategory.standard C

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 : ℕ
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ { X₁ := AddCommGrpCat.of (Ext S.X₃ Y n), X₂ := AddCommGrpCat.of (Ext S.X₂ Y n), X₃ := AddCommGrpCat.of (Ext S.X₁ Y n),
      f := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
      zero := ⋯ }.Exact
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

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

Tactic:
let := HasDerivedCategory.standard C

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughInjectives C
⊢ HasExt C

Tactic:
let := HasDerivedCategory.standard C

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughInjectives C
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ HasExt C
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₀ n₁ : ℕ
h : 1 + n₀ = n₁
⊢ { X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
      X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp Y h), zero := ⋯ }.Exact

Tactic:
let := HasDerivedCategory.standard C

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₀ n₁ : ℕ
h : 1 + n₀ = n₁
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ { X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
      X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp Y h), zero := ⋯ }.Exact
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: case refine_1
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Finite n
this : Fintype n
h : ∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
v : m → R
hv : v ᵥ* M = 0
w : n → R
⊢ v ⬝ᵥ M *ᵥ w = 0

pp: case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Finite n
this : Fintype n
h : ∀ (v : m → R), v ᵥ* M = 0 → v = 0
w : m → R
hw : ∀ (w_1 : n → R), w ⬝ᵥ M *ᵥ w_1 = 0
i : n
⊢ (w ᵥ* M) i = 0 i

Tactic:
· simp [dotProduct_mulVec, hv]

Goal state after:
case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Finite n
this : Fintype n
h : ∀ (v : m → R), v ᵥ* M = 0 → v = 0
w : m → R
hw : ∀ (w_1 : n → R), w ⬝ᵥ M *ᵥ w_1 = 0
i : n
⊢ (w ᵥ* M) i = 0 i
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✝ : Fintype n
this : Fintype m
⊢ M.SeparatingRight ↔ ∀ (v : n → R), M *ᵥ v = 0 → v = 0

Tactic:
rw [separatingRight_def]

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Fintype n
this : Fintype m
⊢ (∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0) ↔ ∀ (v : n → R), M *ᵥ v = 0 → v = 0
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₀ n₁ : ℕ
h : 1 + n₀ = n₁
⊢ { X₁ := AddCommGrpCat.of (Ext S.X₁ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₃ Y n₁),
      X₃ := AddCommGrpCat.of (Ext S.X₂ Y n₁), f := AddCommGrpCat.ofHom (hS.extClass.precomp Y h),
      g := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.Exact

Tactic:
let := HasDerivedCategory.standard C

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₀ n₁ : ℕ
h : 1 + n₀ = n₁
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ { X₁ := AddCommGrpCat.of (Ext S.X₁ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₃ Y n₁),
      X₃ := AddCommGrpCat.of (Ext S.X₂ Y n₁), f := AddCommGrpCat.ofHom (hS.extClass.precomp Y h),
      g := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.Exact
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
b : Basis ι R M
b' : Basis ι' R M
inst✝¹ : Fintype ι
inst✝ : Finite ι'
m : M
⊢ b'.toMatrix ⇑b *ᵥ ⇑(b.repr m) = ⇑(b'.repr m)

Tactic:
classical
  cases nonempty_fintype ι'
  simp [← LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrix_mulVec_repr]

Goal state after:
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
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
⊢ b.toMatrix ⇑b' * b'.toMatrix b'' = b.toMatrix b''

Tactic:
have := Classical.decEq ι

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
this : DecidableEq ι
⊢ b.toMatrix ⇑b' * b'.toMatrix b'' = b.toMatrix b''
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
m n : ℕ
h : m.Coprime n
⊢ Disjoint (rootsOfUnity m M) (rootsOfUnity n M)

Tactic:
simp [disjoint_iff_inf_le, rootsOfUnity_inf_rootsOfUnity, Nat.coprime_iff_gcd_eq_one.mp h]

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

Goal state before:
pp: R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m, σ ↑↑ζ = ↑↑ζ ^ m

Tactic:
← restrictRootsOfUnity_coe_apply,

Goal state after:
R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m, ↑↑((restrictRootsOfUnity σ k) ζ) = ↑↑ζ ^ m
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : Basis n R M
inst✝ : DecidableEq n
A : Matrix n n R
hA : IsUnit A.det
x : M
⊢ ((toLin b b) 1) x = x

Tactic:
toLin_one,

Goal state after:
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : Basis n R M
inst✝ : DecidableEq n
A : Matrix n n R
hA : IsUnit A.det
x : M
⊢ LinearMap.id x = x
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mpr
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 → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
⊢ ∃ v, v ≠ 0 ∧ M *ᵥ v = 0

Tactic:
· let := Classical.decEq K
    obtain ⟨⟨b, hb⟩, ba_eq⟩ :=
      IsLocalization.exist_integer_multiples_of_finset (nonZeroDivisors A) (Finset.univ.image v)
    choose f hf using ba_eq
    refine
      ⟨fun i => f _ (Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩),
        mt (fun h => funext fun i => ?_) hv, ?_⟩
    · have := congr_arg (algebraMap A K) (congr_fun h i)
      rw [hf, Subtype.coe_mk, Pi.zero_apply, map_zero, Algebra.smul_def, mul_eq_zero,
        IsFractionRing.to_map_eq_zero_iff] at this
      exact this.resolve_left (nonZeroDivisors.ne_zero hb)
    · ext i
      refine IsFractionRing.injective A K ?_
      calc
        algebraMap A K ((M *ᵥ (fun i : n => f (v i) _)) i) =
            ((algebraMap A K).mapMatrix M *ᵥ algebraMap _ K b • v) i := ?_
        _ = 0 := ?_
        _ = algebraMap A K 0 := (map_zero _).symm
      · simp_rw [RingHom.map_mulVec, mulVec, dotProduct, Function.comp_apply, hf,
          RingHom.mapMatrix_apply, Pi.smul_apply, smul_eq_mul, Algebra.smul_def]
      · rw [mulVec_smul, mul_eq, Pi.smul_apply, Pi.zero_apply, smul_zero]

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * (SpecialLinearGroup.transvection ⋯ b)⁻¹ =
    SpecialLinearGroup.transvection ⋯ c

Tactic:
SpecialLinearGroup.transvection_inv zero_ne_one b

Goal state after:
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b) =
    SpecialLinearGroup.transvection ⋯ c
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ⊢ ↑S * ↑S = -1

Tactic:
simp only [S, Int.reduceNeg, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd,
    vecMul_cons, head_cons, zero_smul, tail_cons, neg_smul, one_smul, neg_cons, neg_zero, neg_empty,
    empty_vecMul, add_zero, zero_add, empty_mul, Equiv.symm_apply_apply]
  exact Eq.symm (eta_fin_two (-1))

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

Goal state before:
pp: R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
B : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂
i✝ : n
j✝ : m
⊢ (toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m)) B i✝ j✝ = (toMatrix₂' R) B i✝ j✝

Tactic:
rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂'_apply, Pi.basisFun_apply, Pi.basisFun_apply]

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✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x)

Tactic:
rw [add_comm z x]

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (x + z)
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✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
Q : QuadraticMap R M N
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x✝² : R
x✝¹ x✝ : M
⊢ polar toFun x✝¹ (x✝² • x✝) = x✝² • polar toFun x✝¹ x✝

Tactic:
polar_comm,

Goal state after:
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✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
Q : QuadraticMap R M N
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x✝² : R
x✝¹ x✝ : M
⊢ polar toFun (x✝² • x✝) x✝¹ = x✝² • polar toFun x✝¹ x✝
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✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
B : BilinMap R M N
x y : M
⊢ polar (⇑B.toQuadraticMap) x y = (B x) y + (B y) x

Tactic:
simp only [polar, toQuadraticMap_apply, map_add, add_apply, add_assoc, add_comm (B y x) _,
    add_sub_cancel_left, sub_eq_add_neg _ (B y y), add_neg_cancel_left]

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

Goal state before:
pp: case negSucc
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.negSucc a✝) ∈ A 0

Tactic:
rw [Int.cast_negSucc]

Goal state after:
case negSucc
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ -↑(a✝ + 1) ∈ A 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case succ.inr
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = d + 1
hB₁ : B ≠ 0
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
obtain ⟨x, hx⟩ := exists_bilinForm_self_ne_zero hB₁ hB₂

Goal state after:
case succ.inr
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = d + 1
hB₁ : B ≠ 0
x : V
hx : (B x) x ≠ 0
⊢ ∃ v, IsOrthoᵢ B ⇑v
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case nil
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : SetLike.GradedMonoid A
inst✝ : CanonicallyOrderedAdd ι
hl : ∀ xn ∈ [], ∀ k < xn.2, xn.1 k = 0
n : ι
hn : n < (List.map Prod.snd []).sum
⊢ (List.map Prod.fst []).prod n = 0

Tactic:
simp at hn

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

Goal state before:
pp: case nil
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : SetLike.GradedMonoid A
inst✝ : CanonicallyOrderedAdd ι
m : ι
hl : ∀ x ∈ [], ∀ k < m, x k = 0
n : ι
hn : n < [].length • m
⊢ [].prod n = 0

Tactic:
simp at hn

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

Goal state before:
pp: K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
c : K
y : V
hy : c • x ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : -(c • x) = y
this : ∀ x_1 ∈ K ∙ x, x_1 ∈ Submodule.orthogonalBilin B (K ∙ x) → x_1 = 0
⊢ c = 0

Tactic:
have := this (c • x) (Submodule.smul_mem _ _ <| Submodule.mem_span_singleton_self _) hy

Goal state after:
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
c : K
y : V
hy : c • x ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : -(c • x) = y
this✝ : ∀ x_1 ∈ K ∙ x, x_1 ∈ Submodule.orthogonalBilin B (K ∙ x) → x_1 = 0
this : c • x = 0
⊢ c = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case succ
R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
⊢ (List.ofFn fun i ↦ (ι R) (f i)).prod = 0

Tactic:
rw [List.ofFn_succ, List.prod_cons]

Goal state after:
case succ
R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
⊢ (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0
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
⊢ (((foldl 0 (LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) f) 1 0) 0 = (f 0) 0

Tactic:
rw [foldl_one]

Goal state after: