mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
m n : ℕ
I : Type u_3
inst✝³ : LinearOrder I
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis I R M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : ¬Disjoint ↑s ↑t
⊢ b.ExteriorAlgebra ↑s * b.ExteriorAlgebra ↑t = 0

Tactic:
by
  simpa only [basis_apply_powersetCard] using ιMulti_family_mul_of_not_disjoint R b s t h

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

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v w : n → α
⊢ circulant v = circulant w → v = w

Tactic:
h

Goal state after:
α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v w : n → α
h : circulant v = circulant w
⊢ v = w
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v w : n → α
h : circulant v = circulant w
k : n
⊢ circulant v k 0 = circulant w k 0

Tactic:
h

Goal state after:
α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v w : n → α
h : circulant v = circulant w
k : n
⊢ circulant w k 0 = circulant w k 0
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case top
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✝¹ : LT m
inst✝ : LT n
i : m
hA : A.IsPivotedBy l
hc : l i = ⊤
⊢ ⊤ = ⊤ ↔ A i = 0

Tactic:
have h := (hA.isPivotEntry i).1

Goal state after:
case top
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✝¹ : LT m
inst✝ : LT n
i : m
hA : A.IsPivotedBy l
hc : l i = ⊤
h : ∀ (j : n), ↑j < l i → A i j = 0
⊢ ⊤ = ⊤ ↔ A i = 0
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : A ∈ reps m
i j : Fin 2
⊢ ↑A i j ∈ Finset.Icc (-|m|) |m|

Tactic:
by
  suffices |A.1 i j| ≤ |m| from Finset.mem_Icc.mpr <| abs_le.mp this
  obtain ⟨h10, h00, h01, h11⟩ := h
  have h1 : 0 < |A.1 1 1| := (abs_nonneg _).trans_lt h11
  have h2 : 0 < |A.1 0 0| := abs_pos.mpr h00.ne'
  fin_cases i <;> fin_cases j
  · simpa only [← abs_mul, A_c_eq_zero h10] using! (le_mul_iff_one_le_right h2).mpr h1
  · simpa only [← abs_mul, A_c_eq_zero h10] using! h11.le.trans (le_mul_of_one_le_left h1.le h2)
  · simp_all
  · simpa only [← abs_mul, A_c_eq_zero h10] using! (le_mul_iff_one_le_left h1).mpr h2

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 k : ℤ
H : Finset ℤ := Finset.Icc (-|k|) |k|
H4 : Type := Fin 2 → Fin 2 → ↥H
M N : ↑(reps k)
⊢ (fun M i j ↦ ⟨↑↑M i j, ⋯⟩) M = (fun M i j ↦ ⟨↑↑M i j, ⋯⟩) N → M = N

Tactic:
h

Goal state after:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m k : ℤ
H : Finset ℤ := Finset.Icc (-|k|) |k|
H4 : Type := Fin 2 → Fin 2 → ↥H
M N : ↑(reps k)
h : (fun M i j ↦ ⟨↑↑M i j, ⋯⟩) M = (fun M i j ↦ ⟨↑↑M i j, ⋯⟩) N
⊢ M = N
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case succ.mp
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
h_pos : 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
l : n
hl_mem : l ∈ Finset.univ
hl_pos : 0 < (A ^ m) i l * A l j
⊢ Nonempty { p // p.length = m + 1 }

Tactic:
have hAm_nonneg : 0 ≤ (A ^ m) i l := pow_apply_nonneg hA m i l

Goal state after:
case succ.mp
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
h_pos : 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
l : n
hl_mem : l ∈ Finset.univ
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
⊢ Nonempty { p // p.length = m + 1 }
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
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
h_pos : 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
l : n
hl_mem : l ∈ Finset.univ
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
h : (A ^ m) i l ≤ 0
⊢ False

Tactic:
simp [le_antisymm h hAm_nonneg] at hl_pos

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

Goal state before:
pp: case succ.mp
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
h_pos : 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
l : n
hl_mem : l ∈ Finset.univ
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
h_Am : 0 < (A ^ m) i l
h_A : 0 < A l j
⊢ Nonempty { p // p.length = m + 1 }

Tactic:
obtain ⟨⟨p, rfl⟩⟩ := (ih i l).mp h_Am

Goal state after:
case succ.mp
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
i j l : n
hl_mem : l ∈ Finset.univ
hA_nonneg' : 0 ≤ A l j
h_A : 0 < A l j
p : Path i l
ih : ∀ (i_1 j : n), 0 < (A ^ p.length) i_1 j ↔ Nonempty { p_1 // p_1.length = p.length }
h_pos : 0 < ∑ j_1, (A ^ p.length) i j_1 * A j_1 j
hl_pos : 0 < (A ^ p.length) i l * A l j
hAm_nonneg : 0 ≤ (A ^ p.length) i l
h_Am : 0 < (A ^ p.length) i l
⊢ Nonempty { p_1 // p_1.length = p.length + 1 }
Module: Mathlib.LinearAlgebra.Matrix.Gershgorin

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖(∑ j ∈ Finset.univ.erase i, A i j * v j) * (v i)⁻¹‖ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ * ‖v j * (v i)⁻¹‖

Tactic:
by
                rw [Finset.sum_mul]
                exact (norm_sum_le _ _).trans (le_of_eq (by simp_rw [mul_assoc, norm_mul]))

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

Goal state before:
pp: case base
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A✝ : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A✝)
A : FixedDetMatrix (Fin 2) ℤ m
⊢ ↑A 1 0 = 0 → C (reduce A) → C A

Tactic:
h

Goal state after:
case base
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A✝ : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A✝)
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
⊢ C (reduce A) → C A
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Zero α
inst✝ : Zero β
A : Matrix n n α
ha : A.IsDiag
f : α → β
hf : f 0 = 0
i j : n
⊢ i ≠ j → (fun i j ↦ A.map f i j = 0) i j

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Zero α
inst✝ : Zero β
A : Matrix n n α
ha : A.IsDiag
f : α → β
hf : f 0 = 0
i j : n
h : i ≠ j
⊢ A.map f i j = 0
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
⊢ i ≠ j → (fun i j ↦ (-A) i j = 0) i j

Tactic:
h

Goal state after:
α : 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
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : AddZeroClass α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i j : n
⊢ i ≠ j → (fun i j ↦ (A + B) i j = 0) i j

Tactic:
h

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : AddZeroClass α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i j : n
h : i ≠ j
⊢ (A + B) i j = 0
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

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

Tactic:
h

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : SubtractionMonoid α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i j : n
h : i ≠ j
⊢ (A - B) i j = 0
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
⊢ i ≠ j → (fun i j ↦ (k • A) i j = 0) i j

Tactic:
h

Goal state after:
α : 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
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case cons
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this : Quiver n := A.toQuiver
b : n
q : Path j b
e : b ⟶ i
hp_pos : 0 < (q.cons e).length
⊢ ∃ p, 0 < p.length

Tactic:
let qT := transposePath (A := A) (q.cons e)
    let : Quiver n := toQuiver Aᵀ
    use qT
    simp [qT, transposePath, Quiver.Path.length_comp, Quiver.Path.length_toPath]

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

Goal state before:
pp: case mp
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ (fromBlocks A B C D).IsDiag → A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag

pp: case mpr
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag → (fromBlocks A B C D).IsDiag

Tactic:
· intro h
    refine ⟨fun i j hij => ?_, ext fun i j => ?_, ext fun i j => ?_, fun i j hij => ?_⟩
    · exact h (Sum.inl_injective.ne hij)
    · exact h Sum.inl_ne_inr
    · exact h Sum.inr_ne_inl
    · exact h (Sum.inr_injective.ne hij)

Goal state after:
case mpr
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag → (fromBlocks A B C D).IsDiag
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
h : Module.finrank k V = 2
⊢ Nat.card (ℙ k V) = Nat.card k + 1

Tactic:
by
  simp [card_of_finrank k V h]

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 : R
hc : c • v = A v
⊢ ∃ c, A v = c • v ∧ ∃ (hcomap : R ∙ v ≤ Submodule.comap A (R ∙ v)), A.restrict hcomap = c • id

Tactic:
refine ⟨c, hc.symm, fun w hw ↦ ?_, LinearMap.ext fun ⟨w, hw⟩ ↦ ?_⟩
  <;> obtain ⟨a, rfl⟩ := Submodule.mem_span_singleton.1 hw

Goal state after:
case refine_1
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
a : R
hw : a • v ∈ R ∙ v
⊢ a • v ∈ Submodule.comap A (R ∙ v)

case refine_2
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
x✝ : ↥(R ∙ v)
a : R
hw : a • v ∈ R ∙ v
⊢ (A.restrict ⋯) ⟨a • v, hw⟩ = (c • id) ⟨a • v, hw⟩
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
β : F
hβ : β • v = B • w - w
⊢ A • β • v + α • v = B • α • v + β • v

Tactic:
smul_comm,

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
β : F
hβ : β • v = B • w - w
⊢ β • A • v + α • v = B • α • v + β • v
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
β : F
hβ : β • v = B • w - w
⊢ β • v + α • v = B • α • v + β • v

Tactic:
smul_comm,

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
β : F
hβ : β • v = B • w - w
⊢ β • v + α • v = α • B • v + β • v
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
h : Module.finrank R V ≤ 1
a✝ : Nontrivial R
⊢ Subgroup.center (SpecialLinearGroup R V) = ⊥

Tactic:
let b := Module.Free.chooseBasis R V

Goal state after:
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
h : Module.finrank R V ≤ 1
a✝ : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
⊢ Subgroup.center (SpecialLinearGroup R V) = ⊥
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case inr
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
g : SpecialLinearGroup R V
hR : Nontrivial R
⊢ g ∈ Subgroup.center (SpecialLinearGroup R V) ↔ ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑g = r • LinearMap.id

Tactic:
let b := Module.Free.chooseBasis R V

Goal state after:
case inr
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
g : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
⊢ g ∈ Subgroup.center (SpecialLinearGroup R V) ↔ ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑g = r • LinearMap.id
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case inl
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)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = Module.finrank R V
h' : 1 ≤ Module.finrank R V
⊢ ↑↑r ^ Module.finrank R V = 1

Tactic:
h

Goal state after:
case inl
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)
h : max (Module.finrank R V) 1 = Module.finrank R V
h' : 1 ≤ Module.finrank R V
this : ↑↑r ^ Module.finrank R V = 1
⊢ ↑↑r ^ Module.finrank R V = 1
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: case h
ι : 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 : ι × ι
hx : x.1 ∈ (bm.repr x✝).support ∧ x.2 ∈ (bm.repr x✝).support ∧ x.1 ≠ x.2
⊢ ¬x.1 = x.2

Tactic:
simpa using hx.2.2

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

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
h : Q.radical = ⊥
⊢ Module.rank R ↥Q.radical ≤ 1

Tactic:
h

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
h : Q.radical = ⊥
⊢ Module.rank R ↥⊥ ≤ 1
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 ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu : e i ∈ range h ∪ range e ∪ range f
⊢ (ωConj b) (e i) ∈ range h ∪ range e ∪ range f

Tactic:
by simp [ω_mul_e, mul_assoc]

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

Goal state before:
pp: case inr.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 l : ι
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)

Tactic:
rcases eq_or_ne k i with rfl | hki

Goal state after:
case inr.inr.inl
ι : 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
l : ι
⊢ ⁅e i, f i⁆ (Sum.inr ↑i) (Sum.inr l) = h i (Sum.inr ↑i) (Sum.inr l)

case inr.inr.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 l : ι
hki : k ≠ ↑i
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr.inr.inr.inr.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 l : ι
hki : k ≠ ↑i
hki' : k ≠ -↑i
hkl : k ≠ l
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)

Tactic:
simp_all [h, e, f]

Goal state after:
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
hki : P.pairingIn ℤ k i = 0
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hnk_notMem : P.root n - P.root k ∉ range ⇑P.root
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
key₂ : P.pairingIn ℤ i m = 0
key₃ : P.pairingIn ℤ j k = 2
hij : P.pairing i j = 0
hkj : P.pairing k j = 1
⊢ (P.toLinearMap (P.root k + P.root i)) (P.coroot j) = (algebraMap ℤ R) 1

Tactic:
simp [hkj, hij]

Goal state after:
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.IsG2
b : P.Base
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
⊢ Submodule.span ℤ {P.root i, P.root j} = P.rootSpan ℤ

Tactic:
have : {i, j} ⊆ b.support := by grind
  rw [← image_pair, ← Finset.coe_pair, Finset.eq_of_subset_of_card_le this (by aesop),
    b.span_int_root_support]

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

Goal state before:
pp: 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.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i✝ : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
i : ι
⊢ (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U) →
    ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b ((P.reflectionPerm i) i) ∈ U → ∃ j, u j ∈ U

Tactic:
h

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.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i✝ : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
i : ι
h : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U
⊢ ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b ((P.reflectionPerm i) i) ∈ U → ∃ j, u j ∈ U