mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝² : IsLieAbelian M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
⊢ Injective ⇑{ toFun := fun x ↦ (ofProd c) (0, x), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

Tactic:
intro x

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
inst✝² : IsLieAbelian M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x : M
⊢ ∀ ⦃a₂ : M⦄,
    { toFun := fun x ↦ (ofProd c) (0, x), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } x =
        { toFun := fun x ↦ (ofProd c) (0, x), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } a₂ →
      x = a₂
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
inst✝² : IsLieAbelian M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
⊢ Surjective ⇑{ toFun := fun x ↦ ((ofProd c).symm x).1, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

Tactic:
intro x

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
inst✝² : IsLieAbelian M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x : L
⊢ ∃ a, { toFun := fun x ↦ ((ofProd c).symm x).1, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } a = x
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 :=
  { 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)
n : ℕ
hn :
  ∀ (w : A),
    ∀ a < n + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}
w : A
⊢ ∀ a < n + 1 + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n + 1, ((toEnd R L V) z ^ i) v = x}

Tactic:
intro m hm
      obtain (hm | rfl) : m < n + 1 ∨ m = n + 1 := by lia
      · exact U'.mono (Nat.le_succ n) (hn w m hm)
      have H : ∀ w, ⁅w, (π z ^ n) v⁆ = (T χ w) ((π z ^ n) v) + χ w • ((π z ^ n) v) := by simp
      rw [T, LinearMap.sub_apply, pow_succ', Module.End.mul_apply, LieModule.toEnd_apply_apply,
        LieModule.toEnd_apply_apply, LinearMap.smul_apply, Module.End.one_apply, leibniz_lie,
        lie_swap_lie w z, H, H, lie_add, lie_smul, add_sub_assoc, add_sub_assoc, sub_self, add_zero]
      refine add_mem (neg_mem <| add_mem ?_ ?_) ?_
      · exact U'.mono n.le_succ (hn _ n n.lt_succ_self)
      · exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨n, n.lt_succ_self, rfl⟩)
      · exact map_U'_le _ <| Submodule.mem_map_of_mem <| hn w n n.lt_succ_self

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ∀ (x : { x // x ∈ l }), l.attach ≠ [x]

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
x : { x // x ∈ l }
⊢ l.attach ≠ [x]
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
⊢ (p.toList x).Nodup

Tactic:
by_cases hx : p x = x

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : p x = x
⊢ (p.toList x).Nodup

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : ¬p x = x
⊢ (p.toList x).Nodup
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 :=
  { 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
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
w : A
key : ∀ (i : ℕ), i ≠ 0 → ∃ j < i, Submodule.map (T χ w) (U' i) ≤ U' j
this : ⨆ i, U' i ≤ (T χ w).maxGenEigenspace 0
⊢ ∀ (m : ↥U), ∃ n, (T χ w ^ n) m = 0

Tactic:
intro 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
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
w : A
key : ∀ (i : ℕ), i ≠ 0 → ∃ j < i, Submodule.map (T χ w) (U' i) ≤ U' j
this : ⨆ i, U' i ≤ (T χ w).maxGenEigenspace 0
x : ↥U
⊢ ∃ n, (T χ w ^ n) x = 0
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
xi xj : AddMonoidAlgebra R A ⊗[R] L
hi : xi ∈ (LinearMap.rTensor L (AddMonoidAlgebra.grade R i).subtype).range
hj : xj ∈ (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype).range
⊢ ⁅xi, xj⁆ ∈ (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range

Tactic:
obtain ⟨xi, rfl⟩ := hi

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
xj : AddMonoidAlgebra R A ⊗[R] L
hj : xj ∈ (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype).range
xi : ↥(AddMonoidAlgebra.grade R i) ⊗[R] L
⊢ ⁅(LinearMap.rTensor L (AddMonoidAlgebra.grade R i).subtype) xi, xj⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
f : Perm α
hf : f.IsCycle
⊢ ∀ (a a' : α) (m : Multiset α) (b : Cycle α),
    (if f a = a then if f a' = a' then b else ↑(f.toList a') else ↑(f.toList a)) ≍
      if f a' = a' then if f a = a then b else ↑(f.toList a) else ↑(f.toList a')

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x : α
⊢ ∀ (a' : α) (m : Multiset α) (b : Cycle α),
    (if f x = x then if f a' = a' then b else ↑(f.toList a') else ↑(f.toList x)) ≍
      if f a' = a' then if f x = x then b else ↑(f.toList x) else ↑(f.toList a')
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
f : Perm α
hf : f.IsCycle
⊢ ∀ (a a' : α) (m : Multiset α) (b : Cycle α),
    (if f a = a then if f a' = a' then b else ↑(f.toList a') else ↑(f.toList a)) ≍
      if f a' = a' then if f a = a then b else ↑(f.toList a) else ↑(f.toList a')

Tactic:
by
      intro x y _ s
      refine heq_of_eq ?_
      split_ifs with hx hy hy <;> try rfl
      have hc : SameCycle f x y := IsCycle.sameCycle hf hx hy
      exact Quotient.sound' hc.toList_isRotated

Goal state after:
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A := (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs : s = (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs' : (F f).support ⊆ s
⊢ Finset.map (Equiv.toEmbedding (Equiv.neg A)) s ⊆ s

Tactic:
intro x

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A := (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs : s = (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs' : (F f).support ⊆ s
x : A
⊢ x ∈ Finset.map (Equiv.toEmbedding (Equiv.neg A)) s → x ∈ s
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
hA : A.size = n * n
t : ℕ
i j : Fin n
⊢ (stepEntry n A)^[t] (BirdDet.get n A) ↑i ↑j = (Spec.stepEntry (Matrix.ofArray A hA))^[t] (Matrix.ofArray A hA) i j

Tactic:
rw [Matrix.ofArray_eq_of_getD]
  induction t generalizing i j with
  | zero => simp [get_eq]
  | succ t ih =>
    simp_rw [iterate_succ_apply', stepEntry_eq, Spec.stepEntry_eq, sumFrom_fin_tail, ih,
      Matrix.of_apply, get_eq]

Goal state after:
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case h.refine_1
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
⊢ ∀ (x : L), ⁅x, v⁆ = (χ₀ ∘ₗ π₁ + c • ↑e ∘ₗ π₂) x • v

Tactic:
intro x

Goal state after:
case h.refine_1
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
⊢ ⁅x, v⁆ = (χ₀ ∘ₗ π₁ + c • ↑e ∘ₗ π₂) x • v
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ e (π₂ x) • ↑(c • ⟨v, hv⟩) = (c • e (π₂ x)) • v

Tactic:
rw [smul_assoc, smul_comm]

Goal state after:
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ e (π₂ x) • ↑(c • ⟨v, hv⟩) = e (π₂ x) • c • v
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case h.refine_1
k : Type u_1
inst✝¹¹ : Field k
L : Type u_2
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : LieRingModule L V
inst✝⁵ : LieModule k L V
inst✝⁴ : CharZero k
inst✝³ : Module.Finite k V
inst✝² : Nontrivial V
inst✝¹ : IsSolvable L
inst✝ : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := (toEnd k L V).range
toEndo : L →ₗ[k] ↥imL := LinearMap.codRestrict imL.toSubmodule ↑(toEnd k L V) ⋯
χ : Module.Dual k ↥imL
h : Nontrivial ↥(weightSpace V ⇑χ)
v : V
hv✝ : v ∈ weightSpace V ⇑χ
hv : ∀ (x : ↥imL), ⁅x, v⁆ = χ x • v
hv0 : ⟨v, hv✝⟩ ≠ 0
⊢ ∀ (x : L), ⁅x, v⁆ = (χ ∘ₗ toEndo) x • v

Tactic:
intro x

Goal state after:
case h.refine_1
k : Type u_1
inst✝¹¹ : Field k
L : Type u_2
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : LieRingModule L V
inst✝⁵ : LieModule k L V
inst✝⁴ : CharZero k
inst✝³ : Module.Finite k V
inst✝² : Nontrivial V
inst✝¹ : IsSolvable L
inst✝ : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := (toEnd k L V).range
toEndo : L →ₗ[k] ↥imL := LinearMap.codRestrict imL.toSubmodule ↑(toEnd k L V) ⋯
χ : Module.Dual k ↥imL
h : Nontrivial ↥(weightSpace V ⇑χ)
v : V
hv✝ : v ∈ weightSpace V ⇑χ
hv : ∀ (x : ↥imL), ⁅x, v⁆ = χ x • v
hv0 : ⟨v, hv✝⟩ ≠ 0
x : L
⊢ ⁅x, v⁆ = (χ ∘ₗ toEndo) x • v
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
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
⊢ corootSubmodule α ≤ LieSubmodule.restr I H

Tactic:
intro x

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
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
x : L
⊢ x ∈ corootSubmodule α → x ∈ LieSubmodule.restr I H
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_4
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
⊢ (∃ i, y = (fun i ↦ p ^ ↑i) i) → y ≤ p ^ n

Tactic:
rintro ⟨i, rfl⟩
    exact ⟨p ^ (n - i : ℕ), (pow_mul_pow_sub p (Nat.succ_le_succ_iff.mp i.2)).symm⟩

Goal state after:
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
⊢ LieSubmodule.restr I H ⊓ H.toLieSubmodule ≤ ⨆ α ∈ I.rootSet, corootSubmodule ↑α

Tactic:
intro x

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
x : L
⊢ x ∈ LieSubmodule.restr I H ⊓ H.toLieSubmodule → x ∈ ⨆ α ∈ I.rootSet, corootSubmodule ↑α
Module: Mathlib.RingTheory.FractionalIdeal.Basic

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✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
⊢ ↑I ≤ ⊥

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
⊢ x ∈ ↑I → x ∈ ⊥
Module: Mathlib.RingTheory.FractionalIdeal.Basic

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
I : FractionalIdeal S P
⊢ 0 ≤ I

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
x : P
⊢ x ∈ 0 → x ∈ I
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
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
μ : ↥LieSubalgebra.root
hμ : μ ∈ I.rootSet
this : ↑span_compl_roots = ⨆ β, ⨆ (_ : β ∉ I.rootSet), ↑(f β)
γ : ↥LieSubalgebra.root
hγ : γ ∉ I.rootSet
⊢ (Weight.toLinear K (↥H) L ↑μ) (coroot ↑γ) = 0

Tactic:
exact I.rootSet_apply_coroot_eq_zero_of_notMem_rootSet hμ hγ

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ b ∈ J, IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
⊢ ∀ (x y : P), IsInteger R ((aI * aJ) • x) → IsInteger R ((aI * aJ) • y) → IsInteger R ((aI * aJ) • (x + y))

Tactic:
intro x

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ b ∈ J, IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
x : P
⊢ ∀ (y : P), IsInteger R ((aI * aJ) • x) → IsInteger R ((aI * aJ) • y) → IsInteger R ((aI * aJ) • (x + y))
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : Subsingleton Mˣ
inst✝ : Subsingleton Nˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
⊢ ∀ {a b : ↑(Set.Iic (Associates.mk m))},
    { toFun := fun l ↦ ⟨Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩), ⋯⟩,
            invFun := fun l ↦ ⟨Associates.mk ↑(d.symm ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩), ⋯⟩, left_inv := ⋯,
            right_inv := ⋯ }
          a ≤
        { toFun := fun l ↦ ⟨Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩), ⋯⟩,
            invFun := fun l ↦ ⟨Associates.mk ↑(d.symm ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩), ⋯⟩, left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩
    simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, Associates.mk_le_mk_iff_dvd, hd,
        associatesEquivOfUniqueUnits_apply, out_dvd_iff, mk_out]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : FractionalIdeal R₁⁰ K
hI : I ≠ 0
hJ : J ≠ 0
hIJ : I ≤ J
⊢ J⁻¹ ≤ I⁻¹

Tactic:
intro x

Goal state after:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : FractionalIdeal R₁⁰ K
hI : I ≠ 0
hJ : J ≠ 0
hIJ : I ≤ J
x : K
⊢ x ∈ J⁻¹ → x ∈ I⁻¹
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁷ : Field K
R₁ : Type u_4
inst✝⁶ : CommRing R₁
inst✝⁵ : IsDomain R₁
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
⊢ map (↑h) I⁻¹ = (map (↑h) I)⁻¹

Tactic:
by
  rw [inv_eq, FractionalIdeal.map_div, FractionalIdeal.map_one, inv_eq]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
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
x✝ : K
h : x✝ ∈ I
⊢ ∀ y ∈ ↑1, x✝ * y ∈ ↑I

Tactic:
rintro y ⟨y', _, rfl⟩

Goal state after:
case mpr
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
x✝ : K
h : x✝ ∈ I
y' : R₁
left✝ : y' ∈ ↑⊤
⊢ x✝ * (Algebra.linearMap R₁ K) y' ∈ ↑I