mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V := ⋯
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V := ⋯
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
x : V
hx : x ∈ U
⊢ ↑(((toEnd R A ↥U) ⁅z, a⁆) ⟨x, hx⟩) = ↑(⁅LinearMap.restrict ((toEnd R L V) z) hzU, (toEnd R A ↥U) a⁆ ⟨x, hx⟩)

Tactic:
change ⁅⁅z, a⁆, x⁆ = ⁅z, ⁅a, x⁆⁆ - ⁅a, ⁅z, x⁆⁆

Goal state after:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
x : V
hx : x ∈ U
⊢ ⁅⁅z, a⁆, x⁆ = ⁅z, ⁅a, x⁆⁆ - ⁅a, ⁅z, x⁆⁆
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ iterate (⇑l.formPerm) (l.get ⟨0, ⋯⟩) l.length = l

Tactic:
refine ext_getElem (by simp) fun k hk hk' => ?_
    simp only [get_eq_getElem, getElem_iterate, iterate_eq_pow, formPerm_pow_apply_getElem _ hn,
      zero_add, Nat.mod_eq_of_lt hk']

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate ↑k
⊢ (l.rotate ↑k).formPerm.toList ((l.rotate ↑k).get ⟨(l.length - ↑k % l.length + ↑k) % l.length, ⋯⟩) ~r l

Tactic:
simp only [Nat.mod_eq_of_lt k.2, tsub_add_cancel_of_le (le_of_lt k.2), Nat.mod_self]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate ↑k
⊢ (l.rotate ↑k).formPerm.toList ((l.rotate ↑k).get ⟨0, ⋯⟩) ~r l
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate ↑k
⊢ (l.rotate ↑k).formPerm.toList ((l.rotate ↑k).get ⟨0, ⋯⟩) ~r l

Tactic:
rw [toList_formPerm_nontrivial]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate ↑k
⊢ l.rotate ↑k ~r l

case hl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate ↑k
⊢ 2 ≤ (l.rotate ↑k).length

case hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate ↑k
⊢ (l.rotate ↑k).Nodup
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing M
inst✝ : LieAlgebra R M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x✝¹ : R
x✝ : L
⊢ x✝¹ • s₁ x✝ - s₂ (x✝¹ • x✝) = x✝¹ • (s₁ x✝ - s₂ x✝)

Tactic:
smul_sub,

Goal state after:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing M
inst✝ : LieAlgebra R M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x✝¹ : R
x✝ : L
⊢ x✝¹ • s₁ x✝ - s₂ (x✝¹ • x✝) = x✝¹ • s₁ x✝ - x✝¹ • s₂ x✝
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
β : ↥LieSubalgebra.root
hβ : β ∉ I.rootSet
h_ker : coroot ↑α ∈ Weight.ker
⊢ coroot ↑β ∈ Weight.ker

Tactic:
← orthogonal_span_coroot_eq_ker,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
β : ↥LieSubalgebra.root
hβ : β ∉ I.rootSet
h_ker : coroot ↑α ∈ Weight.ker
⊢ coroot ↑β ∈ (traceForm K (↥H) L).orthogonal (K ∙ coroot ↑α)
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0».«0»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «0».«1»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «0».«2»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «0».«3»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «0».«4»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «0».«5»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «0».«6»
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «1».«0»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «1».«1»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «1».«2»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «1».«3»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «1».«4»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «1».«5»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «1».«6»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «2».«0»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «2».«1»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «2».«2»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «2».«3»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «2».«4»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «2».«5»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «2».«6»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «3».«0»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «3».«1»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «3».«2»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «3».«3»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «3».«4»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «3».«5»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «3».«6»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «4».«0»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «4».«1»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «4».«2»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «4».«3»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «4».«4»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «4».«5»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «4».«6»
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «5».«0»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «5».«1»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «5».«2»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «5».«3»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «5».«4»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «5».«5»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «5».«6»
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «6».«0»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «6».«1»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «6».«2»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «6».«3»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «6».«4»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨4, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «6».«5»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨5, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

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

Goal state before:
pp: case «6».«6»
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ (fun i ↦ i) ⟨6, ⋯⟩
⊢ E₇ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) ≤ 0

Tactic:
simp_all [E₇]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
y : K
hy : y ∈ ↑I
⊢ 1 * y ∈ 1

Tactic:
one_mul

Goal state after:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
y : K
hy : y ∈ ↑I
⊢ y ∈ 1
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥LieSubalgebra.root
hα_span : Weight.toLinear K (↥H) L ↑α ∈ I.rootSpan
hα_not : α ∉ I.rootSet
hα_nz : (↑α).IsNonZero
this : I.rootSpan ≤ LinearMap.ker ((Dual.eval K ↥H) (coroot ↑α))
⊢ False

Tactic:
have := LinearMap.mem_ker.mp (this hα_span)

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥LieSubalgebra.root
hα_span : Weight.toLinear K (↥H) L ↑α ∈ I.rootSpan
hα_not : α ∉ I.rootSet
hα_nz : (↑α).IsNonZero
this✝ : I.rootSpan ≤ LinearMap.ker ((Dual.eval K ↥H) (coroot ↑α))
this : ((Dual.eval K ↥H) (coroot ↑α)) (Weight.toLinear K (↥H) L ↑α) = 0
⊢ False
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : IsLocalization S P
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R P
x y : P
⊢ spanSingleton S x = spanSingleton S y ↔ ∃ z, z • x = y

Tactic:
rw [← Submodule.span_singleton_eq_span_singleton, spanSingleton, spanSingleton]
  exact Subtype.mk_eq_mk

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
le_one : (↑M)⁻¹ * ↑P ≤ 1
y : A
_hy : y ∈ ⊤
hx : (algebraMap A (FractionRing A)) y ∈ (↑M)⁻¹ * ↑P
z : A
hzM : z ∈ M
hzp : z ∉ P
zy_mem : (algebraMap A (FractionRing A)) (z * y) ∈ 1 * ↑P
⊢ (algebraMap A (FractionRing A)) y ∈ ↑P

Tactic:
one_mul

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
le_one : (↑M)⁻¹ * ↑P ≤ 1
y : A
_hy : y ∈ ⊤
hx : (algebraMap A (FractionRing A)) y ∈ (↑M)⁻¹ * ↑P
z : A
hzM : z ∈ M
hzp : z ∉ P
zy_mem : (algebraMap A (FractionRing A)) (z * y) ∈ ↑P
⊢ (algebraMap A (FractionRing A)) y ∈ ↑P
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
n : ℕ
⊢ spanSingleton S x ^ n = spanSingleton S (x ^ n)

Tactic:
by
  induction n with
  | zero => rw [pow_zero, pow_zero, spanSingleton_one]
  | succ n hn => rw [pow_succ, hn, spanSingleton_mul_spanSingleton, pow_succ]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case h
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
this : (↑I)⁻¹ * ↑J ≤ 1
H : Ideal A
hH : ↑H = (↑I)⁻¹ * ↑J
⊢ ↑J = 1 * ↑J

Tactic:
one_mul

Goal state after:
case h
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
this : (↑I)⁻¹ * ↑J ≤ 1
H : Ideal A
hH : ↑H = (↑I)⁻¹ * ↑J
⊢ ↑J = ↑J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : y ∈ R₁⁰
this : spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩) * spanSingleton R₁⁰ ((algebraMap R₁ K) y) = 1
y' : (FractionalIdeal R₁⁰ K)ˣ :=
  Units.mkOfMulEqOne (spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩)) (spanSingleton R₁⁰ ((algebraMap R₁ K) y)) this
coe_y' : ↑y' = spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩)
⊢ spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = ↑J ↔ spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = 1 * ↑J

Tactic:
one_mul

Goal state after:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : y ∈ R₁⁰
this : spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩) * spanSingleton R₁⁰ ((algebraMap R₁ K) y) = 1
y' : (FractionalIdeal R₁⁰ K)ˣ :=
  Units.mkOfMulEqOne (spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩)) (spanSingleton R₁⁰ ((algebraMap R₁ K) y)) this
coe_y' : ↑y' = spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩)
⊢ spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = ↑J ↔ spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = ↑J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_1
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * x
⊢ ∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
    x = ((algebraMap R₁ K) a_inv)⁻¹ * y'

Tactic:
refine ⟨algebraMap R₁ K x', (mem_coeIdeal _).mpr ⟨x', mem_singleton_mul.mpr ?_, rfl⟩, ?_⟩

Goal state after:
case refine_1.refine_1
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * x
⊢ ∃ y' ∈ I, (Algebra.linearMap R₁ K) x' = (algebraMap R₁ K) a_inv * y'

case refine_1.refine_2
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * x
⊢ x = ((algebraMap R₁ K) a_inv)⁻¹ * (algebraMap R₁ K) x'