mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
m : M₁ × M₂
⊢ ((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)).toLinearMap
          ((evenOdd Q₁ 1).subtype ((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1)) +
        (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)).toLinearMap
          ((evenOdd Q₂ 1).subtype ((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2))) *
      ((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)).toLinearMap
          ((evenOdd Q₁ 1).subtype ((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1)) +
        (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)).toLinearMap
          ((evenOdd Q₂ 1).subtype ((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2))) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) ((QuadraticMap.prod Q₁ Q₂) m)

Tactic:
AlgHom.toLinearMap_apply,

Goal state after:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
m : M₁ × M₂
⊢ ((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₁ 1).subtype ((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1)) +
        (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₂ 1).subtype ((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2))) *
      ((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₁ 1).subtype ((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1)) +
        (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₂ 1).subtype ((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2))) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) ((QuadraticMap.prod Q₁ Q₂) m)
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : Ring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Module ι (Additive ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)
a₁ : A
j₁ : ι
b₁ : ↥(ℬ j₁)
i₂ : ι
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (-1) ^ (j₁ * i₂) • (f.toLinearMap (a₁ * ↑a₂) * g.toLinearMap (↑b₁ * b₂)) = f a₁ * g ↑b₁ * (f ↑a₂ * g b₂)

Tactic:
AlgHom.toLinearMap_apply,

Goal state after:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : Ring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Module ι (Additive ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)
a₁ : A
j₁ : ι
b₁ : ↥(ℬ j₁)
i₂ : ι
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (-1) ^ (j₁ * i₂) • (f (a₁ * ↑a₂) * g (↑b₁ * b₂)) = f a₁ * g ↑b₁ * (f ↑a₂ * g b₂)
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)

Tactic:
apply GradedAlgebra.liftι R M

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
h : LinearIndependent R v
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
⊢ LinearIndependent K (⇑(Pi.algebraMap ι' R K) ∘ v)

Tactic:
rw [← LinearIndependent.iff_fractionRing (R := R)]

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
h : LinearIndependent R v
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
⊢ LinearIndependent R (⇑(Pi.algebraMap ι' R K) ∘ v)
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : PartialOrder m
hA : A.IsPivotedBy l
i₁ i₂ : m
hlt : i₁ < i₂
⊢ l i₁ ≤ l i₂

Tactic:
by_cases h₁ : l i₁ = ⊤

Goal state after:
case pos
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : PartialOrder m
hA : A.IsPivotedBy l
i₁ i₂ : m
hlt : i₁ < i₂
h₁ : l i₁ = ⊤
⊢ l i₁ ≤ l i₂

case neg
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : PartialOrder m
hA : A.IsPivotedBy l
i₁ i₂ : m
hlt : i₁ < i₂
h₁ : ¬l i₁ = ⊤
⊢ l i₁ ≤ l i₂
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : ¬n = Fintype.card ι
⊢ Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index = 0

Tactic:
have hlt : n < Fintype.card ι :=
      Ne.lt_of_le h (by simpa using Fintype.card_le_of_embedding snf.f)
    simp [hlt]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case inr
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
x✝ :
  Monotone l ∧
    StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
hmono : Monotone l
hstrict : StrictMonoOn l {i | l i ≠ ⊤}
hlead : ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
i₁ i₂ : m
hlt : i₁ < i₂
j₂ : n
hz : ∀ j₁ < j₂, A i₁ j₁ = 0
h₂ : l i₂ ≠ ⊤
⊢ ↑j₂ < l i₂

Tactic:
have h₁ : l i₁ ≠ ⊤ := fun ht => h₂ (top_le_iff.mp (ht.symm.le.trans (hmono hlt.le)))

Goal state after:
case inr
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
x✝ :
  Monotone l ∧
    StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
hmono : Monotone l
hstrict : StrictMonoOn l {i | l i ≠ ⊤}
hlead : ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
i₁ i₂ : m
hlt : i₁ < i₂
j₂ : n
hz : ∀ j₁ < j₂, A i₁ j₁ = 0
h₂ : l i₂ ≠ ⊤
h₁ : l i₁ ≠ ⊤
⊢ ↑j₂ < l i₂
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
⊢ reduce A ∈ reps m

Tactic:
simp only [reduce_of_pos h h1]

Goal state after:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
⊢ T ^ (-(↑A 0 1 / ↑A 1 1)) • A ∈ reps m
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
s : R
hA : A.IsHadamard
hcard : IsRegular ↑(Fintype.card n)
hcol : ∀ (j : n), ∑ i, A i j = s
hvcol : 1 ᵥ* A = s • 1
i : n
⊢ (Aᴴ *ᵥ 1) i = (star s • 1) i

Tactic:
simp [Matrix.mulVec, dotProduct, ← star_sum, hcol i]

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ Aᵀᴴ * Aᵀ = ↑(Fintype.card n) • 1

Tactic:
rw [conjTranspose_transpose_eq_transpose_conjTranspose, ← transpose_mul, hA.mul_conjTranspose,
      transpose_smul, transpose_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
this : ¬Aᵀ.IsIrreducible
⊢ ¬((∀ (i j : n), 0 ≤ A i j) ∧ IsSStronglyConnected n)

Tactic:
simp_all only [not_forall, not_le, isSStronglyConnected_iff,
      not_and, not_exists, not_lt, nonpos_iff_eq_zero, isEmpty_Prop, IsEmpty.forall_iff]

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

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n R
inst✝ : IsCancelAdd R
hA : A.Nonsingular
k : ℕ
⊢ (A ^ (k + 1)).Nonsingular

Tactic:
by simp [pow_succ, (hA.pow k).mul hA]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
⊢ Nat.card (ℙ k V) = (Nat.card V - 1) / (Nat.card k - 1)

Tactic:
by
  have : 1 < Nat.card k := Finite.one_lt_card
  rw [card k, Nat.mul_div_cancel]
  lia

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : ℙ K V
⊢ x ∉ ⊥

Tactic:
induction x using ind with | h v hv =>
  rwa [← Subspace.mem_submodule_iff _ hv, Subspace.submodule.map_bot, Submodule.mem_bot]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Module.Free R V
d1 : Module.finrank R V = 1
u✝ v : SpecialLinearGroup R V
a✝ : Nontrivial R
x✝ : V
hx : ¬x✝ = 0
u : SpecialLinearGroup R V
x : V
c : R := (LinearEquiv.smul_id_of_finrank_eq_one d1).symm ↑↑u
hc : (LinearEquiv.smul_id_of_finrank_eq_one d1) c = ↑↑u
⊢ c = 1

Tactic:
have hu := u.prop

Goal state after:
case neg
R : Type u_1
V : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Module.Free R V
d1 : Module.finrank R V = 1
u✝ v : SpecialLinearGroup R V
a✝ : Nontrivial R
x✝ : V
hx : ¬x✝ = 0
u : SpecialLinearGroup R V
x : V
c : R := (LinearEquiv.smul_id_of_finrank_eq_one d1).symm ↑↑u
hc : (LinearEquiv.smul_id_of_finrank_eq_one d1) c = ↑↑u
hu : LinearEquiv.det ↑u = 1
⊢ c = 1
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : ¬FiniteDimensional K V
⊢ LinearEquiv.det g = 1

Tactic:
← Units.val_inj,

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : ¬FiniteDimensional K V
⊢ ↑(LinearEquiv.det g) = ↑1
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
⊢ IsMultiplyPretransitive (SpecialLinearGroup K V) (ℙ K V) 2

Tactic:
by
  have := linearEquiv_is_two_pretransitive K V
  rw [is_two_pretransitive_iff] at this ⊢
  intro D D' E E' hD hE
  obtain ⟨g, gD, gE⟩ := this hD hE
  by_cases hV : FiniteDimensional K V
  · suffices ∀ a : Kˣ, ∃ h : V ≃ₗ[K] V, h.det = a ∧ h • D = D ∧ h • D' = D' by
      obtain ⟨h, hdet, hD, hE⟩ := this (g.det)⁻¹
      use ⟨g * h, by simp [hdet]⟩
      simp [specialLinearGroup_smul_def, toLinearEquiv_eq_coe, mul_smul, gD, hD, gE, hE]
    intro a
    rw [← linearIndependent_pair_iff_ne] at hD
    have := linearIndepOn_pair D D'
    let s := (linearIndepOn_pair D D').extend (Set.subset_univ _)
    let b : Module.Basis s K V := Module.Basis.extend this
    rw [← mk_rep D, ← mk_rep D']
    have hD_mem : D.rep ∈ s := LinearIndepOn.subset_extend _ _ (by simp)
    have hD'_mem : D'.rep ∈ s := LinearIndepOn.subset_extend _ _ (by simp)
    refine ⟨dilatransvection (f := b.coord ⟨D.rep, hD_mem⟩)
      (v := (a.val - 1) • b ⟨D.rep, hD_mem⟩) (by simp), ?_, ?_, ?_⟩
    · simp [← Units.val_inj, coe_det, LinearMap.transvection.det]
    · rw [smul_mk, mk_eq_mk_iff, LinearEquiv.smul_def]
      use a
      rw [← coe_coe, dilatransvection.coe_toLinearMap,
        LinearMap.transvection.apply, Module.Basis.coord_apply]
      suffices (b.repr D.rep) ⟨D.rep, hD_mem⟩ = 1 by
        rw [this, Module.Basis.extend_apply_self, Units.smul_def]
        module
      nth_rewrite 1 [show D.rep = (⟨D.rep, hD_mem⟩ : s) by rfl]
      rw [← Module.Basis.extend_apply_self, Module.Basis.repr_self]
      simp
    · rw [smul_mk, mk_eq_mk_iff, LinearEquiv.smul_def]
      use 1
      rw [one_smul, ← coe_coe, dilatransvection.coe_toLinearMap,
        LinearMap.transvection.apply, Module.Basis.coord_apply]
      suffices (b.repr D'.rep) ⟨D.rep, hD_mem⟩ = 0 by
        rw [Module.Basis.extend_apply_self]
        simp [this]
      nth_rewrite 1 [show D'.rep = (⟨D'.rep, hD'_mem⟩ : s) by rfl]
      rw [← Module.Basis.extend_apply_self, Module.Basis.repr_self]
      apply Finsupp.single_eq_of_ne
      simp only [ne_eq, ← Subtype.coe_inj]
      intro h
      apply Fin.zero_ne_one
      apply hD.injective
      simp [h]
  use ⟨g, by
    rw [← Units.val_inj, coe_det]
    apply LinearMap.det_eq_one_of_not_module_finite hV⟩
  simp [← gD, ← gE, specialLinearGroup_smul_def, toLinearEquiv_eq_coe]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (∑ x_1 ∈ (bm.repr x).support,
      ∑ x_2 ∈ (bm.repr x).support,
        if x_1 = x_2 then (bm.repr x) x_1 • (bm.repr x) x_2 • Q (bm x_1)
        else
          if x_1 < x_2 then (bm.repr x) x_1 • (bm.repr x) x_2 • polar (⇑Q) (bm x_1) (bm x_2)
          else (bm.repr x) x_1 • (bm.repr x) x_2 • 0) =
    Q (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)

Tactic:
smul_zero,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (∑ x_1 ∈ (bm.repr x).support,
      ∑ x_2 ∈ (bm.repr x).support,
        if x_1 = x_2 then (bm.repr x) x_1 • (bm.repr x) x_2 • Q (bm x_1)
        else if x_1 < x_2 then (bm.repr x) x_1 • (bm.repr x) x_2 • polar (⇑Q) (bm x_1) (bm x_2) else 0) =
    Q (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x y : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : x ∈ (span R (range h)).carrier
hy : y ∈ (span R (range h)).carrier
i j : ↥b.support
⊢ ⁅h i, h j⁆ = 0

Tactic:
exact lie_h_h i j

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairing k i = -1
⊢ 0 < P.pairingIn ℤ l i

Tactic:
have : P.pairingIn ℤ l i = 1 - P.pairingIn ℤ j i := by
    apply algebraMap_injective ℤ R
    simp only [algebraMap_pairingIn, map_sub, map_one, algebraMap_pairingIn]
    convert! (P.coroot' i : M →ₗ[R] R).congr_arg hl using 1
    simp only [map_sub, map_add, LinearMap.flip_apply, root_coroot_eq_pairing, hki, pairing_same,
      sub_left_inj]
    ring

Goal state after:
case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairing k i = -1
this : P.pairingIn ℤ l i = 1 - P.pairingIn ℤ j i
⊢ 0 < P.pairingIn ℤ l i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ span R (range h') = ⊤

Tactic:
rw [eq_top_iff]
  rintro ⟨⟨x, -⟩, hx : x ∈ span R (range h)⟩ -
  let g : cartanSubalgebra' b →ₗ[R] Matrix (b.support ⊕ ι) (b.support ⊕ ι) R :=
    (lieAlgebra b).subtype ∘ₗ (cartanSubalgebra' b).subtype
  suffices x ∈ (span R (range h')).map g by
    rwa [← SetLike.mem_coe, ← (injective_subtype _).mem_set_image,
        ← (injective_subtype _).mem_set_image, ← image_comp]
  rwa [map_span, ← range_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i j : ↥b.support
⊢ ⁅h i, h j⁆ = 0

Tactic:
exact lie_h_h i j

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : ¬j = -↑i
⊢ ∃ n, (e i ^ n).col (Sum.inr j) = 0

Tactic:
use P.chainTopCoeff i j + 1

Goal state after:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := ⋯
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : ¬j = -↑i
⊢ (e i ^ (chainTopCoeff (↑i) j + 1)).col (Sum.inr j) = 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
χ : ↥H → K
hχ : χ ≠ 0
hχ' : genWeightSpace (↥U) χ ≠ ⊥
this : ∀ {w : ↥b.support ⊕ ι → K}, w ≠ 0 → w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ → ∃ i t, t • w = v b i
w : ↥U
hw₀ : w ≠ 0
hw : U.incl w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
i : ι
t : K
hi : t • ↑w = v b i
⊢ ∃ i, v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)

Tactic:
use i

Goal state after:
case h
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
χ : ↥H → K
hχ : χ ≠ 0
hχ' : genWeightSpace (↥U) χ ≠ ⊥
this : ∀ {w : ↥b.support ⊕ ι → K}, w ≠ 0 → w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ → ∃ i t, t • w = v b i
w : ↥U
hw₀ : w ≠ 0
hw : U.incl w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
i : ι
t : K
hi : t • ↑w = v b i
⊢ v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)
Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
⊢ (B x) x • coroot B hx = 2 • B x

Tactic:
by
  ext y
  simp [smul_apply, smul_eq_mul, nsmul_eq_mul, Nat.cast_ofNat, apply_self_mul_coroot_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field K
inst✝¹¹ : CharZero K
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Fintype ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module K M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module K N
P : RootPairing ι K M N
inst✝⁴ : P.IsRootSystem
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : P.IsReduced
inst✝¹ : P.IsIrreducible
inst✝ : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hU : U ≠ ⊥
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) := ⋯
⊢ ¬U' ≤ genWeightSpace (↥b.support ⊕ ι → K) 0

Tactic:
contrapose hU

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field K
inst✝¹¹ : CharZero K
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Fintype ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module K M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module K N
P : RootPairing ι K M N
inst✝⁴ : P.IsRootSystem
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : P.IsReduced
inst✝¹ : P.IsIrreducible
inst✝ : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) := { toSubmodule := ↑U, lie_mem := ⋯ }
hU : U' ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
⊢ U = ⊥
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
t u s x✝¹ : Multiset α
x✝ : α
⊢ s + t + {x✝} = s + u + x✝¹ ↔ t + {x✝} = u + x✝¹

Tactic:
by rw [add_assoc, add_assoc, add_left_cancel_iff]

Goal state after:
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case hC.compl
α : Type u_1
𝒜 : Set (Set α)
s t u : Set α
hs✝ : generateSetAlgebra 𝒜 u
mu : MeasurableSet u
⊢ MeasurableSet uᶜ

Tactic:
| compl u _ mu =>

Goal state after: