mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : LT m
i₁ i₂ : m
hA : A.IsPivotedBy l
hlt : i₁ < i₂
h₁ : l i₁ ≠ ⊤
hle : l i₂ ≤ l i₁
⊢ False

Tactic:
obtain ⟨c₂, hc₂⟩ := WithTop.ne_top_iff_exists.mp (hle.trans_lt h₁.lt_top).ne

Goal state after:
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✝ : LT m
i₁ i₂ : m
hA : A.IsPivotedBy l
hlt : i₁ < i₂
h₁ : l i₁ ≠ ⊤
hle : l i₂ ≤ l i₁
c₂ : n
hc₂ : ↑c₂ = l i₂
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : ¬a = i
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b

Tactic:
obtain h | h := ne_iff_lt_or_gt.mp h
        · rw [Fin.succAbove_castSucc_of_lt _ _ h,
            Fin.succAbove_of_succ_le _ _ (Fin.succ_lt_succ_iff.mpr h).le]
        · rw [Fin.succAbove_succ_of_lt _ _ h, Fin.succAbove_castSucc_of_le _ _ h.le]

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

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
this : ↑(reduceStep A) 1 0 = ↑A 0 0 % ↑A 1 0
⊢ |↑(reduceStep A) 1 0| < |↑A 1 0|

Tactic:
this,

Goal state after:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
this : ↑(reduceStep A) 1 0 = ↑A 0 0 % ↑A 1 0
⊢ |↑A 0 0 % ↑A 1 0| < |↑A 1 0|
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
hcard : IsRegular ↑(Fintype.card n)
⊢ IsRegular A.det

Tactic:
have : IsRegular (A.det * star A.det) := by
    rw [hA.det_mul_star_det]
    exact hcard.pow _

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
hcard : IsRegular ↑(Fintype.card n)
this : IsRegular (A.det * star A.det)
⊢ IsRegular A.det
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : SubtractionMonoid α
A : Matrix n n α
ha : A.IsDiag
i j : n
h : i ≠ j
⊢ (-A) i j = 0

Tactic:
simp [ha h]

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

Goal state before:
pp: α : Type u_1
R : Type u_3
n : Type u_4
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
k : R
A : Matrix n n α
ha : A.IsDiag
i j : n
h : i ≠ j
⊢ (k • A) i j = 0

Tactic:
simp [ha h]

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

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
A : Matrix n n α
ha : Aᴴ.IsDiag
⊢ A.IsDiag

Tactic:
by
    convert! ha.conjTranspose
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional

Goal state before:
pp: case intro
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
inst✝³ : (i : ι) → AddCommGroup (M₁ i)
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)
inst✝ : ∀ (i : ι), Module.Free R (M₁ i)
val✝ : Fintype ι
this :
  ∀ [inst : (i : Fin (Fintype.card ι)) → AddCommGroup (M₁ ((Fintype.equivFin ι).symm i))]
    [inst_1 : (i : Fin (Fintype.card ι)) → Module R (M₁ ((Fintype.equivFin ι).symm i))]
    [∀ (i : Fin (Fintype.card ι)), Module.Finite R (M₁ ((Fintype.equivFin ι).symm i))]
    [∀ (i : Fin (Fintype.card ι)), Module.Free R (M₁ ((Fintype.equivFin ι).symm i))],
    Module.Free R (MultilinearMap R (fun x ↦ M₁ ((Fintype.equivFin ι).symm x)) M₂) ∧
      Module.Finite R (MultilinearMap R (fun x ↦ M₁ ((Fintype.equivFin ι).symm x)) M₂)
l : Module.Free R (MultilinearMap R (fun x ↦ M₁ ((Fintype.equivFin ι).symm x)) M₂)
r : Module.Finite R (MultilinearMap R (fun x ↦ M₁ ((Fintype.equivFin ι).symm x)) M₂)
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)

Tactic:
have e := domDomCongrLinearEquiv' R R M₁ M₂ (Fintype.equivFin ι)

Goal state after:
case intro
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
inst✝³ : (i : ι) → AddCommGroup (M₁ i)
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)
inst✝ : ∀ (i : ι), Module.Free R (M₁ i)
val✝ : Fintype ι
this :
  ∀ [inst : (i : Fin (Fintype.card ι)) → AddCommGroup (M₁ ((Fintype.equivFin ι).symm i))]
    [inst_1 : (i : Fin (Fintype.card ι)) → Module R (M₁ ((Fintype.equivFin ι).symm i))]
    [∀ (i : Fin (Fintype.card ι)), Module.Finite R (M₁ ((Fintype.equivFin ι).symm i))]
    [∀ (i : Fin (Fintype.card ι)), Module.Free R (M₁ ((Fintype.equivFin ι).symm i))],
    Module.Free R (MultilinearMap R (fun x ↦ M₁ ((Fintype.equivFin ι).symm x)) M₂) ∧
      Module.Finite R (MultilinearMap R (fun x ↦ M₁ ((Fintype.equivFin ι).symm x)) M₂)
l : Module.Free R (MultilinearMap R (fun x ↦ M₁ ((Fintype.equivFin ι).symm x)) M₂)
r : Module.Finite R (MultilinearMap R (fun x ↦ M₁ ((Fintype.equivFin ι).symm x)) M₂)
e : MultilinearMap R M₁ M₂ ≃ₗ[R] MultilinearMap R (fun i ↦ M₁ ((Fintype.equivFin ι).symm i)) M₂
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
Module: Mathlib.LinearAlgebra.Multilinear.DirectSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁶ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) M'
x : ⨁ (i : ι) (j : κ i), M i j
⊢ (fromDirectSumEquiv f) ⇑x = ∑ p ∈ Fintype.piFinset fun i ↦ DFinsupp.support (x i), (f p) fun i ↦ (x i) (p i)

Tactic:
rw [fromDirectSumEquiv, ← fromDFinsuppEquiv_apply]
  convert! rfl

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (A i)
inst✝⁴ : Algebra R' R
inst✝³ : (i : ι) → Algebra R (A i)
inst✝² : (i : ι) → Algebra R' (A i)
inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
i : ι
inst✝ : DecidableEq ι
this : Pi.mulSingle i ((algebraMap R' (A i)) r) = update (fun i ↦ 1) i (r • 1)
⊢ r • (tprod R) 1 = (tprod R) (Pi.mulSingle i ((algebraMap R' (A i)) r))

Tactic:
this,

Goal state after:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (A i)
inst✝⁴ : Algebra R' R
inst✝³ : (i : ι) → Algebra R (A i)
inst✝² : (i : ι) → Algebra R' (A i)
inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
i : ι
inst✝ : DecidableEq ι
this : Pi.mulSingle i ((algebraMap R' (A i)) r) = update (fun i ↦ 1) i (r • 1)
⊢ r • (tprod R) 1 = (tprod R) (update (fun i ↦ 1) i (r • 1))
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
A B : Subspace K V
⊢ A.carrier = B.carrier → A = B

Tactic:
by
    cases A
    cases B
    simp

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
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), S ⊆ ↑W → u ∈ W

Tactic:
simp_rw [← span_le_subspace_iff]
  exact ⟨fun hu W hW => hW hu, fun W => W (span S) (le_refl _)⟩

Goal state after:
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 : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this✝ : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this✝
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
this : (b.repr D.rep) ⟨D.rep, hD_mem⟩ = 1
⊢ a • D.rep = D.rep + (b.repr D.rep) ⟨D.rep, hD_mem⟩ • (↑a - 1) • b ⟨D.rep, hD_mem⟩

Tactic:
this,

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 : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this✝ : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this✝
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
this : (b.repr D.rep) ⟨D.rep, hD_mem⟩ = 1
⊢ a • D.rep = D.rep + 1 • (↑a - 1) • b ⟨D.rep, hD_mem⟩
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : SpecialLinearGroup ι F
L : Submodule F (ι → F)
⊢ lineStab (g • L) = MulAut.conj g • lineStab L

Tactic:
ext A
  rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem]
  simp only [mem_lineStab_iff, Submodule.mem_smul_pointwise_iff_exists, MulAut.smul_def,
    MulAut.inv_apply, MulAut.conj_symm_apply]
  refine ⟨fun hA w ↦ ?_, fun hA w ↦ ⟨g⁻¹ • (A • w - w), ?_, by simp⟩⟩
  · obtain ⟨v, hv, hvw⟩ := hA (g • w)
    simp_all [eq_comm (a := g • v), sub_eq_iff_eq_add, mul_smul]
  · simpa [mul_smul, smul_sub] using hA (g⁻¹ • w)

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v : V
A : V →ₗ[R] V
hAv : A v ∈ R ∙ v
⊢ ∃ c, A v = c • v ∧ ∃ (hcomap : R ∙ v ≤ Submodule.comap A (R ∙ v)), A.restrict hcomap = c • id

Tactic:
obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.1 hAv

Goal state after:
R : Type u_3
V : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v : V
A : V →ₗ[R] V
hAv : A v ∈ R ∙ v
c : R
hc : c • v = A v
⊢ ∃ c, A v = c • v ∧ ∃ (hcomap : R ∙ v ≤ Submodule.comap A (R ∙ v)), A.restrict hcomap = c • id
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ LinearEquiv.det (LinearMap.equivOfIsUnitDet ⋯) = 1

Tactic:
simp only [← Units.val_inj, LinearEquiv.coe_det, LinearMap.coe_equivOfIsUnitDet,
      LinearMap.det_smul, LinearMap.det_id, mul_one, Units.val_one]
    have := (mem_rootsOfUnity' _ _).mp r.prop
    rcases max_cases (Module.finrank R V) 1 with ⟨h, h'⟩ |  ⟨h, h'⟩
    · simp_rw [h] at this
      exact this
    · simp_rw [h, pow_one] at this
      simp [this]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Nontrivial V
hι : ¬IsEmpty ι
this✝ : FaithfulSMul R V
g' : ↥(center (_root_.SpecialLinearGroup R V)) := (centerCongr (toLin_equiv b)) g
hgg' : ∀ (x : V), ↑↑↑g' x = ↑↑((toLin_equiv b) ↑g) x
x : V
this : ↑↑(centerEquivRootsOfUnity g') • x = ↑↑g' x
⊢ ↑↑(centerEquivRootsOfUnity g') • x = ↑↑(center_equiv_rootsOfUnity g) • x

Tactic:
this,

Goal state after:
case neg
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Nontrivial V
hι : ¬IsEmpty ι
this✝ : FaithfulSMul R V
g' : ↥(center (_root_.SpecialLinearGroup R V)) := (centerCongr (toLin_equiv b)) g
hgg' : ∀ (x : V), ↑↑↑g' x = ↑↑((toLin_equiv b) ↑g) x
x : V
this : ↑↑(centerEquivRootsOfUnity g') • x = ↑↑g' x
⊢ ↑↑g' x = ↑↑(center_equiv_rootsOfUnity g) • x
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
x y : M
hx : x ∈ {x | Q x = 0 ∧ Q.polarBilin x = 0}
hy : y ∈ {x | Q x = 0 ∧ Q.polarBilin x = 0}
this : Q (x + y) = Q x + Q y
⊢ Q (x + y) = 0

Tactic:
this,

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
x y : M
hx : x ∈ {x | Q x = 0 ∧ Q.polarBilin x = 0}
hy : y ∈ {x | Q x = 0 ∧ Q.polarBilin x = 0}
this : Q (x + y) = Q x + Q y
⊢ Q x + Q y = 0
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✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsRootSystem
this :
  ⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) ∘ h =
    ⇑Sum.elimZeroLeft ∘ fun i ↦ ⇑(algebraMap ℤ R) ∘ fun x ↦ P.pairingIn ℤ x ↑i
⊢ LinearIndependent R (⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) ∘ h)

Tactic:
this,

Goal state after:
ι : 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✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsRootSystem
this :
  ⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) ∘ h =
    ⇑Sum.elimZeroLeft ∘ fun i ↦ ⇑(algebraMap ℤ R) ∘ fun x ↦ P.pairingIn ℤ x ↑i
⊢ LinearIndependent R (⇑Sum.elimZeroLeft ∘ fun i ↦ ⇑(algebraMap ℤ R) ∘ fun x ↦ P.pairingIn ℤ x ↑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✝ : Fintype ι
i j : ↥b.support
⊢ ⁅h i, h j⁆ = 0

Tactic:
by
  classical
  simpa only [h_eq_diagonal, ← commute_iff_lie_eq] using Matrix.commute_diagonal _ _

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case inl
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
this : Module.IsReflexive R M
aux₁ : LinearIndependent R ![P.root i, P.root j]
aux₂ : chainBotCoeff i j + chainTopCoeff i j ≤ 2
aux₃ : 1 ≤ chainTopCoeff i j
aux₄ : chainBotCoeff i j = chainTopCoeff i j
⊢ chainTopCoeff i j = if True then 1 else 0

Tactic:
reduceIte

Goal state after:
case inl
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
this : Module.IsReflexive R M
aux₁ : LinearIndependent R ![P.root i, P.root j]
aux₂ : chainBotCoeff i j + chainTopCoeff i j ≤ 2
aux₃ : 1 ≤ chainTopCoeff i j
aux₄ : chainBotCoeff i j = chainTopCoeff i j
⊢ chainTopCoeff i j = 1
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

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✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
this : Module.IsReflexive R M
aux₁ : LinearIndependent R ![P.root i, P.root j]
aux₂ : chainBotCoeff i j + chainTopCoeff i j ≤ 2
aux₃ : 1 ≤ chainTopCoeff i j
aux₄ : chainBotCoeff i j ≠ chainTopCoeff i j
⊢ chainBotCoeff i j = if False then 1 else 0

Tactic:
reduceIte

Goal state after:
case inr
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
this : Module.IsReflexive R M
aux₁ : LinearIndependent R ![P.root i, P.root j]
aux₂ : chainBotCoeff i j + chainTopCoeff i j ≤ 2
aux₃ : 1 ≤ chainTopCoeff i j
aux₄ : chainBotCoeff i j ≠ chainTopCoeff i j
⊢ chainBotCoeff i j = 0
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

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.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
x : M
hx : x ∈ allRoots P
this : {longRoot P, shortRoot P} = Set.range ![shortRoot P, longRoot P]
⊢ x ∈ Submodule.span ℤ {longRoot P, shortRoot P}

Tactic:
this,

Goal state after:
ι : 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.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
x : M
hx : x ∈ allRoots P
this : {longRoot P, shortRoot P} = Set.range ![shortRoot P, longRoot P]
⊢ x ∈ Submodule.span ℤ (Set.range ![shortRoot P, longRoot P])
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
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
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
x : ι
hx : P.root k = P.root ↑i + P.root x
y : ι
hy : P.root k = P.root y - P.root ↑i
h_lin_ind_x : LinearIndependent R ![P.root ↑i, P.root x]
⊢ LinearIndependent R ![P.root ↑i, P.root y]

Tactic:
← add_eq_of_eq_sub hy,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
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
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
x : ι
hx : P.root k = P.root ↑i + P.root x
y : ι
hy : P.root k = P.root y - P.root ↑i
h_lin_ind_x : LinearIndependent R ![P.root ↑i, P.root x]
⊢ LinearIndependent R ![P.root ↑i, P.root k + P.root ↑i]
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
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
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
y : ι
hy : P.root k = P.root y - P.root ↑i
h₁ : chainBotCoeff (↑i) k = 0
⊢ LinearIndependent R ![P.root ↑i, P.root y]

Tactic:
← add_eq_of_eq_sub hy,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
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
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
y : ι
hy : P.root k = P.root y - P.root ↑i
h₁ : chainBotCoeff (↑i) k = 0
⊢ LinearIndependent R ![P.root ↑i, P.root k + P.root ↑i]
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inl.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
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
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ↥b.support
l : ι
h₁ : ∀ (x : ι), ¬(P.root x = P.root l - P.root ↑i ∧ k = i ∧ x = -↑i)
⊢ ⁅e i, f i⁆ (Sum.inl k) (Sum.inr l) = h i (Sum.inl k) (Sum.inr l)

Tactic:
have h₂ (x : ι) : ¬ (P.root x = P.root i + P.root l ∧ k = i ∧ x = i) := by
      simp only [not_and]
      rintro contra rfl rfl
      simp [P.ne_zero] at contra

Goal state after:
case inl.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
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
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ↥b.support
l : ι
h₁ : ∀ (x : ι), ¬(P.root x = P.root l - P.root ↑i ∧ k = i ∧ x = -↑i)
h₂ : ∀ (x : ι), ¬(P.root x = P.root ↑i + P.root l ∧ k = i ∧ x = ↑i)
⊢ ⁅e i, f i⁆ (Sum.inl k) (Sum.inr l) = h i (Sum.inl k) (Sum.inr l)
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)
hU : ∀ (χ : ↥H → K), χ ≠ 0 → genWeightSpace (↥U) χ = ⊥
this : ⨆ χ, ⨆ (_ : χ ≠ 0), ⊥ = ⊥
⊢ genWeightSpace (↥U) 0 = genWeightSpace (↥U) 0 ⊔ ⨆ i, ⨆ (_ : i ≠ 0), ⊥

Tactic:
this,

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
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K), χ ≠ 0 → genWeightSpace (↥U) χ = ⊥
this : ⨆ χ, ⨆ (_ : χ ≠ 0), ⊥ = ⊥
⊢ genWeightSpace (↥U) 0 = genWeightSpace (↥U) 0 ⊔ ⊥