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₂
⊢ ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R] 1 *
          ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R] 1 +
        ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R]
          ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2) +
      (1 ᵍ⊗ₜ[R] ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2) *
          ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R] 1 +
        1 ᵍ⊗ₜ[R] ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2) *
          1 ᵍ⊗ₜ[R] ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2)) =
    (algebraMap R (CliffordAlgebra Q₁)) (Q₁ m.1) ᵍ⊗ₜ[R] 1 + (algebraMap R (CliffordAlgebra Q₁)) (Q₂ m.2) ᵍ⊗ₜ[R] 1

Tactic:
GradedTensorProduct.tmul_one_mul_coe_tmul,

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₂
⊢ (↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) *
            ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1)) ᵍ⊗ₜ[R]
          1 +
        ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R]
          ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2) +
      (1 ᵍ⊗ₜ[R] ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2) *
          ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R] 1 +
        1 ᵍ⊗ₜ[R] ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2) *
          1 ᵍ⊗ₜ[R] ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2)) =
    (algebraMap R (CliffordAlgebra Q₁)) (Q₁ m.1) ᵍ⊗ₜ[R] 1 + (algebraMap R (CliffordAlgebra Q₁)) (Q₂ m.2) ᵍ⊗ₜ[R] 1
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case convert_3
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h✝ : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
j : Fin n
h : j ≠ hj.choose
hinj : f j ≠ f hj.choose
⊢ (if i = f j then ⋯.choose • a j else 0) = 0

Tactic:
rw [hj.choose_spec] at hinj

Goal state after:
case convert_3
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h✝ : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
j : Fin n
h : j ≠ hj.choose
hinj : f j ≠ i
⊢ (if i = f j then ⋯.choose • a j else 0) = 0
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : LinearOrder m
inst✝² : LinearOrder n
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
l : m → WithTop n
hA : A.IsPivotedBy l
⊢ A.rank = #{i | l i ≠ ⊤}

Tactic:
refine le_antisymm (A.rank_le_card_of_support_subset _
    (Function.support_subset_iff'.mpr fun i hi => hA.eq_top_iff.mp (by aesop))) ?_

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : LinearOrder m
inst✝² : LinearOrder n
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
l : m → WithTop n
hA : A.IsPivotedBy l
⊢ #{i | l i ≠ ⊤} ≤ A.rank
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.MvPolynomial

Goal state before:
pp: case pos
m : Type u_1
k : Type u_2
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Field k
inst✝ : Infinite k
p q : MvPolynomial (m × m) k
h : ∀ (g : GL m k), (eval fun ij ↦ ↑g ij.1 ij.2) p = (eval fun ij ↦ ↑g ij.1 ij.2) q
s : m × m → k
hs_det : (Matrix.of fun i j ↦ s (i, j)).det = 0
⊢ ((eval s) p - (eval s) q) * (Matrix.of fun i j ↦ s (i, j)).det = 0

Tactic:
rw [hs_det, mul_zero]

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

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3
base : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 = 0 → C A
step : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 ≠ 0 → C (reduceStep A) → C A
A : FixedDetMatrix (Fin 2) ℤ m
⊢ C A

Tactic:
by_cases h : (A.1 1 0) = 0

Goal state after:
case pos
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3
base : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 = 0 → C A
step : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 ≠ 0 → C (reduceStep A) → C A
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
⊢ C A

case neg
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3
base : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 = 0 → C A
step : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 ≠ 0 → C (reduceStep A) → C A
A : FixedDetMatrix (Fin 2) ℤ m
h : ¬↑A 1 0 = 0
⊢ C A
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
⊢ A.num = 0 ↔ A = 0

Tactic:
simp [Matrix.num, ← ext_iff, A.den_ne_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝³ : DecidableEq ι
M : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i₀ : ι
m : (i : ι) → M i
⊢ ((tprod R) fun i ↦ m ((Equiv.subtypeNeSumPUnit i₀).symm.symm i)) =
    (tprod R) fun j ↦ m ((Equiv.subtypeNeSumPUnit i₀) j)

Tactic:
Equiv.symm_symm

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

Goal state before:
pp: case inl.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Infinite V
this : ¬Finite (ℙ k V) ↔ ¬Finite V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
push Not at this

Goal state after:
case inl.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Infinite V
this : Infinite (ℙ k V) ↔ Infinite V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: case inl.inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Finite V
this✝¹ : Fintype V
this✝ : Fintype (ℙ k V)
this : Fintype k
hV : Fintype.card { v // v ≠ 0 } = Fintype.card V - 1
⊢ Fintype.card V - 1 = Fintype.card (ℙ k V) * Fintype.card kˣ

Tactic:
← hV

Goal state after:
case inl.inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Finite V
this✝¹ : Fintype V
this✝ : Fintype (ℙ k V)
this : Fintype k
hV : Fintype.card { v // v ≠ 0 } = Fintype.card V - 1
⊢ Fintype.card { v // v ≠ 0 } = Fintype.card (ℙ k V) * Fintype.card kˣ
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: case refine_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
⊢ Independent f

Tactic:
convert! Independent.mk _ _ h

Goal state after:
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
x✝ : ι
⊢ f x✝ = mk K ((Projectivization.rep ∘ f) x✝) ⋯

case refine_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
⊢ ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0
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 : Subspace K V
c : K
x : V
h₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
h₂ : c • x ≠ 0
⊢ Projectivization.mk K (c • x) h₂ ∈ s.carrier

Tactic:
convert! h₁ (right_ne_zero_of_smul h₂) using 1
      rw [Projectivization.mk_eq_mk_iff']
      exact ⟨c, rfl⟩

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
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ⟨⋯.unit, ⋯⟩ = r

Tactic:
· rw [not_subsingleton_iff_nontrivial] at hV
      have := Module.Free.instFaithfulSMulOfNontrivial R V
      simp only [← Subtype.val_inj, ← Units.val_inj, IsUnit.unit_spec]
      have H := mem_center_iff.mp (Subtype.prop (centerEquivRootsOfUnity_invFun r))
      suffices (H.choose • LinearMap.id : V →ₗ[R] V) = (r.val : R) • LinearMap.id by
        apply FaithfulSMul.eq_of_smul_eq_smul (α := V)
        intro x
        rw [LinearMap.ext_iff] at this
        simp only [LinearMap.smul_apply, LinearMap.id_coe, id_eq] at this
        rw [this x]
      rw [← H.choose_spec.2]
      simp [centerEquivRootsOfUnity_invFun]

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
hgg' : ↑((centerCongr (toLin_equiv b)) g) = (toLin_equiv b) ↑g
⊢ ↑↑(centerEquivRootsOfUnity ((centerCongr (toLin_equiv b)) g)) • LinearMap.id =
    ↑↑(center_equiv_rootsOfUnity g) • LinearMap.id

Tactic:
rw [← Subtype.coe_inj, ← LinearEquiv.toLinearMap_inj, LinearMap.ext_iff] at hgg'

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
hgg' : ∀ (x : V), ↑↑↑((centerCongr (toLin_equiv b)) g) x = ↑↑((toLin_equiv b) ↑g) x
⊢ ↑↑(centerEquivRootsOfUnity ((centerCongr (toLin_equiv b)) g)) • LinearMap.id =
    ↑↑(center_equiv_rootsOfUnity g) • LinearMap.id
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: M : Type u_2
inst✝⁵ : AddCommGroup M
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : FiniteDimensional 𝕜 M
this : Invertible 2
w : Fin (Module.finrank 𝕜 M) → 𝕜
e : Equivalent Q (weightedSumSquares 𝕜 w)
⊢ Module.finrank 𝕜 M = Nat.card (Fin (Module.finrank 𝕜 M))

Tactic:
exact Eq.symm (Nat.card_fin (Module.finrank 𝕜 M))

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 ι
⊢ IsLieAbelian ↥(LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h))

Tactic:
LieSubalgebra.isLieAbelian_lieSpan_iff

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✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ ∀ x ∈ range h, ∀ y ∈ range h, ⁅x, y⁆ = 0
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_2
ι : 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
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * (B.form (P.root i)) (twoShortAddLongRoot P) =
    2 * (2 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P)

Tactic:
twoShortAddLongRoot_eq,

Goal state after:
case calc_2
ι : 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
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * (B.form (P.root i)) (2 • shortRoot P + longRoot P) =
    2 * (2 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P)
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
a b : M
⊢ (B x) x * Exists.choose ⋯ = (B x) x * (Exists.choose ⋯ + Exists.choose ⋯)

Tactic:
rw [← (hx.2 (a + b)).choose_spec, mul_add, ← (hx.2 a).choose_spec, ← (hx.2 b).choose_spec,
      map_add, mul_add]

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 ≠ ⊥
this : ∃ i, v b i ∈ U
⊢ U = ⊤

Tactic:
obtain ⟨i, hi⟩ := this; exact instIsIrreducible_aux₂ hi

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

Goal state before:
pp: M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
⊢ (∀ (x : M), 0 ≤ (B x) x) ↔ ∀ (x : n → R), 0 ≤ star x ⬝ᵥ ((toMatrix₂ b b) B).mulVec x

Tactic:
refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩

Goal state after:
case refine_1
M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : M), 0 ≤ (B x) x
x : n → R
⊢ 0 ≤ star x ⬝ᵥ ((toMatrix₂ b b) B).mulVec x

case refine_2
M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ ((toMatrix₂ b b) B).mulVec x
x : M
⊢ 0 ≤ (B x) x
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)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) := { toSubmodule := ↑U, lie_mem := ⋯ }
hU : ↑U ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
⊢ ∑ k, c k * ↑|b.cartanMatrix j k| = 0

Tactic:
by_contra contra

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 ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
contra : ¬∑ k, c k * ↑|b.cartanMatrix j k| = 0
⊢ False
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : Free R M
κ : Type uM
b : Basis κ R M
this✝ : Nonempty κ
this : Nontrivial R
⊢ Cardinal.lift.{uR, uM} #(κ →₀ ℕ) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)

Tactic:
Cardinal.mk_finsupp_nat,

Goal state after:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : Free R M
κ : Type uM
b : Basis κ R M
this✝ : Nonempty κ
this : Nontrivial R
⊢ Cardinal.lift.{uR, uM} (max #κ ℵ₀) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : 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 l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
⊢ (chainBotCoeff i m + 1) * (chainTopCoeff j k + 1) = (chainTopCoeff j l + 1) * (chainBotCoeff i k + 1)

Tactic:
have := chainBotCoeff_mul_chainTopCoeff.isNotG2 hi hj hij h₁ h₂ h₃
  let := P.indexNeg
  suffices (P.chainBotCoeff i m + 1) * (P.chainBotCoeff j (-k) + 1) =
      (P.chainBotCoeff j (-l) + 1) * (P.chainBotCoeff i k + 1) by simpa
  /- Establish basic relationships about roots and their sums / differences. -/
  have him_mem : P.root i + P.root m ∈ range P.root := by rw [← h₂]; convert! h₃ using 1; abel
  have hik_mem : P.root k + P.root i ∈ range P.root := h₁ ▸ mem_range_self l
  have hjk_mem : P.root j + P.root (-k) ∈ range P.root := by
    convert! mem_range_self (-m) using 1; simpa [sub_eq_add_neg] using congr(-$h₂)
  have hjl_mem : P.root j + P.root (-l) ∈ range P.root := by
    rw [h₁, ← neg_mem_range_root_iff] at h₃; convert! h₃ using 1; simp [sub_eq_add_neg]
  have h₁' : P.root (-k) - P.root i = P.root (-l) := by
    simp only [root_reflectionPerm, reflection_apply_self, indexNeg_neg]; rw [← h₁]; abel
  have h₂' : P.root (-k) + P.root j = P.root (-m) := by
    simp only [root_reflectionPerm, reflection_apply_self, indexNeg_neg]; rw [← h₂]; abel
  have h₃' : P.root (-k) + P.root j - P.root i ∈ range P.root := by grind
  /- Proceed to the main argument, following Geck's case splits. It's all just bookkeeping. -/
  rcases aux_0 hik_mem with hki | ⟨hki, hik⟩
  · /- Geck "Case 1" -/
    exact aux_1 hi hj hij h₁ h₂ h₃ hki him_mem hjl_mem hjk_mem
  rw [add_comm] at hik_mem hjk_mem
  rcases aux_0 hjk_mem with hkj | ⟨hkj, hjk⟩
  · /- Geck "Case 2" -/
    simpa only [neg_neg] using (aux_1 hj hi hij.symm h₂' h₁' h₃' hkj hjl_mem
      (by simpa only [neg_neg]) (by simpa only [neg_neg])).symm
  /- Geck "Case 3" -/
  suffices P.chainBotCoeff i m = P.chainBotCoeff j (-l) by rw [hik, hjk, this]
  have aux₁ : ¬ (P.chainBotCoeff i m = 1 ∧ P.chainBotCoeff j (-l) = 0) :=
    aux_2 hi hj hij h₁ h₂ h₃ hki (by simpa using hkj) him_mem hjl_mem <| by rwa [add_comm]
  have aux₂ : ¬(P.chainBotCoeff j (-l) = 1 ∧ P.chainBotCoeff i m = 0) := by
    simpa using aux_2 hj hi hij.symm h₂' h₁' h₃' hkj (by simpa)
      hjl_mem (by simpa only [neg_neg]) (by simpa only [neg_neg])
  have aux₃ : P.chainBotCoeff i m = 0 ∨ P.chainBotCoeff i m = 1 := by
    have := P.chainBotCoeff_if_one_zero him_mem
    split at this <;> simp [this]
  have aux₄ : P.chainBotCoeff j (-l) = 0 ∨ P.chainBotCoeff j (-l) = 1 := by
    have := P.chainBotCoeff_if_one_zero hjl_mem
    split at this <;> simp only [this, true_or, or_true]
  lia

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e f : V ≃ₗ[K] V
hf : f ∈ dilatransvections K V
this :
  finrank K ↥(↑f).fixedSubmodule + finrank K ↥(↑e).fixedSubmodule ≤
    finrank K ↥((↑f).fixedSubmodule ⊔ (↑e).fixedSubmodule) + finrank K ↥(↑(f * e)).fixedSubmodule
⊢ finrank K ↥(↑e).fixedSubmodule ≤ 1 + finrank K ↥(↑(f * e)).fixedSubmodule

Tactic:
have := finrank_le_one_add_finrank_fixedSubmodule_dilatransvection f hf

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e f : V ≃ₗ[K] V
hf : f ∈ dilatransvections K V
this✝ :
  finrank K ↥(↑f).fixedSubmodule + finrank K ↥(↑e).fixedSubmodule ≤
    finrank K ↥((↑f).fixedSubmodule ⊔ (↑e).fixedSubmodule) + finrank K ↥(↑(f * e)).fixedSubmodule
this : finrank K V ≤ 1 + finrank K ↥(↑f).fixedSubmodule
⊢ finrank K ↥(↑e).fixedSubmodule ≤ 1 + finrank K ↥(↑(f * e)).fixedSubmodule
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e f : V ≃ₗ[K] V
hf : f ∈ dilatransvections K V
this :
  finrank K ↥(↑e).fixedSubmodule + finrank K ↥(↑f).fixedSubmodule ≤
    finrank K ↥((↑e).fixedSubmodule ⊔ (↑f).fixedSubmodule) + finrank K ↥(↑(e * f)).fixedSubmodule
⊢ finrank K ↥(↑e).fixedSubmodule ≤ 1 + finrank K ↥(↑(e * f)).fixedSubmodule

Tactic:
have := finrank_le_one_add_finrank_fixedSubmodule_dilatransvection f hf

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e f : V ≃ₗ[K] V
hf : f ∈ dilatransvections K V
this✝ :
  finrank K ↥(↑e).fixedSubmodule + finrank K ↥(↑f).fixedSubmodule ≤
    finrank K ↥((↑e).fixedSubmodule ⊔ (↑f).fixedSubmodule) + finrank K ↥(↑(e * f)).fixedSubmodule
this : finrank K V ≤ 1 + finrank K ↥(↑f).fixedSubmodule
⊢ finrank K ↥(↑e).fixedSubmodule ≤ 1 + finrank K ↥(↑(e * f)).fixedSubmodule
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
inst✝ : Unique ι
⊢ ∀ (a : ι), Measurable fun x ↦ uniqueElim x a

Tactic:
Unique.forall_iff,

Goal state after:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
inst✝ : Unique ι
⊢ Measurable fun x ↦ uniqueElim x default