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

Goal state before:
pp: case inl.inl
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

Tactic:
by_cases h : x = y

Goal state after:
case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : ¬x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case inr.inr
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
by_cases h : x = y

Goal state after:
case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : ¬x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case inl.inl
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

Tactic:
by_cases h : x = y

Goal state after:
case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p
h : ¬x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case inr.inr
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
by_cases h : x = y

Goal state after:
case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : ¬x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case inr
R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hn : Nonempty n
⊢ cRank 0 = 0

Tactic:
rw [cRank, col_eq_transpose, transpose_zero, of_symm_zero, range_zero, span_zero_singleton,
    rank_bot]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ 0 = (f Q).toBlocks₁₂ ∧ (f Q).toBlocks₁₂ = 0
⊢ (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0

Tactic:
tauto

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
L : Type u_2
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : ↥(twoCochain R L M)
x y : L
⊢ (a y) x + (a x) y = 0

Tactic:
simpa [map_add, twoCochain_alt a x, twoCochain_alt a y] using twoCochain_alt a (x + y)

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x : ↥(couple R A A')
a : A
⊢ (↑x).1 ((Algebra.ofId A A') a) = (Algebra.ofId A A') ((↑x).2 a)

Tactic:
exact congrArg (· a) x.2

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

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x y : L
m : ⨁ (i : ι), M i
⊢ mapRange (fun x_1 m' ↦ ⁅x + y, m'⁆) ⋯ m = mapRange (fun x_1 m' ↦ ⁅x, m'⁆) ⋯ m + mapRange (fun x m' ↦ ⁅y, m'⁆) ⋯ m

Tactic:
by
    ext
    simp only [mapRange_apply, add_apply, add_lie]

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

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
⊢ LieRing.IsNilpotent ↥(engel K x)

Tactic:
apply isNilpotent_of_forall_le_engel

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
⊢ ∀ x_1 ∈ engel K x, engel K x ≤ engel K x_1
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : M → ι
i : ι
m : M
h : m ∈ (coeff 0).support
⊢ f m = i

Tactic:
cases h

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : x ∉ l'
this : l'.formPerm x = x
⊢ l.formPerm x = x ∨ l'.formPerm x = x

Tactic:
tauto

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∉ l
this : l.formPerm x = x
⊢ l.formPerm x = x ∨ l'.formPerm x = x

Tactic:
tauto

Goal state after:
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
w : A
x : V
hx : x ∈ (⨆ k, U' k).carrier
⊢ (T χ w) x ∈ ⨆ k, U' k

Tactic:
set U := ⨆ k : ℕ, U' k

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
w : A
x : V
U : Submodule R V := ⨆ k, U' k
hx : x ∈ U.carrier
⊢ (T χ w) x ∈ U
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
⊢ l.attach.formPerm.cycleType = {l.length}

Tactic:
rw [cycleType_eq [l.attach.formPerm]]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ↑(map (Finset.card ∘ support) [l.attach.formPerm]) = {l.length}

case h0
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ [l.attach.formPerm].prod = l.attach.formPerm

case h1
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ∀ σ ∈ [l.attach.formPerm], σ.IsCycle

case h2
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ Pairwise Perm.Disjoint [l.attach.formPerm]
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
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
x : E.L
y : M
⊢ ⁅x, E.incl y⁆ ∈ E.proj.ker

Tactic:
LieHom.mem_ker,

Goal state after:
R : Type u_1
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
x : E.L
y : M
⊢ E.proj ⁅x, E.incl y⁆ = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ p.SameCycle x y ∧ x ∈ p.support → ∃ m < (p.cycleOf x).support.card, (p ^ m) x = y

Tactic:
rintro ⟨h, hx⟩

Goal state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
h : p.SameCycle x y
hx : x ∈ p.support
⊢ ∃ m < (p.cycleOf x).support.card, (p ^ m) x = y
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
⊢ x ∈ f.toCycle hf → f x ≠ x

Tactic:
have ⟨l, hl⟩ := exists_toCycle_toList f hf

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
l : α
hl : f.toCycle hf = ↑(f.toList l)
⊢ x ∈ f.toCycle hf → f x ≠ x
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
hx : x ∈ f.toCycle hf
⊢ (f.toCycle hf).next ⋯ x hx = f x

Tactic:
have ⟨l, hl⟩ := exists_toCycle_toList f hf

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
hx : x ∈ f.toCycle hf
l : α
hl : f.toCycle hf = ↑(f.toList l)
⊢ (f.toCycle hf).next ⋯ x hx = f x
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
s : { s // s.Nodup ∧ s.Nontrivial }
⊢ (fun f ↦ ⟨(↑f).toCycle ⋯, ⋯⟩) ((fun s ↦ ⟨(↑s).formPerm ⋯, ⋯⟩) s) = s

Tactic:
rcases s with ⟨⟨s⟩, hn, ht⟩

Goal state after:
case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
val✝ : Cycle α
s : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ (fun f ↦ ⟨(↑f).toCycle ⋯, ⋯⟩) ((fun s ↦ ⟨(↑s).formPerm ⋯, ⋯⟩) ⟨Quot.mk (⇑(IsRotated.setoid α)) s, ⋯⟩) =
    ⟨Quot.mk (⇑(IsRotated.setoid α)) s, ⋯⟩
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).IsCycle
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).SameCycle x y
hx : l.length < 2
this : l.formPerm = 1
⊢ (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) x = x

Tactic:
simp [this]

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

Goal state before:
pp: R : Type u_1
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
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj) s'
⊢ s x - s' x ∈ E.proj.ker

Tactic:
LieHom.mem_ker,

Goal state after:
R : Type u_1
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
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj) s'
⊢ E.proj (s x - s' x) = 0
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
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
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj) s'
⊢ s' y - s y ∈ E.proj.ker

Tactic:
LieHom.mem_ker,

Goal state after:
R : Type u_1
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
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj) s'
⊢ E.proj (s' y - s y) = 0
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case inl.inr
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
H : ↑(derivedSeries k L 1) = ⊤
h✝ : Nontrivial L
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
rw [LieSubmodule.toSubmodule_eq_top] at H

Goal state after:
case inl.inr
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
H : derivedSeries k L 1 = ⊤
h✝ : Nontrivial L
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p✝ p : ℕ
ih : Eq1 A p
⊢ Eq1 A (p + 1)

Tactic:
ext i j
    rw [Matrix.of_apply, paper_eq3 A i j ih, paper_eq5 A, paper_eq3_eq5_off_diag A]

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ.refine_2.succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
hb : c ⟨n✝ + 1, hi⟩ < c 1
⊢ c ⟨n✝ + 1, hi⟩ = ⊥

Tactic:
simpa [Fin.lt_def] using h₁.lt_iff_lt.mp hb

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
⊢ q = c 1 ^ n

Tactic:
convert! hi'

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
⊢ n = ↑i
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R (1 • b)

Tactic:
one_smul

Goal state after:
case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R b
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case pos
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : m = 0
⊢ emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n

pp: case neg
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : ¬m = 0
⊢ emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n

Tactic:
· simp [hm] at hp

Goal state after:
case neg
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : ¬m = 0
⊢ emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n
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
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P'
x : P
⊢ x ∈
      (mapEquiv
            (let __src := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
            { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })).symm
        I ↔
    ∃ y ∈ I, (IsLocalization.map P (RingHom.id R) ⋯) y = x

Tactic:
mapEquiv_symm,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P'
x : P
⊢ x ∈
      (mapEquiv
          (let __src := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
            { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }).symm)
        I ↔
    ∃ y ∈ I, (IsLocalization.map P (RingHom.id R) ⋯) y = x
Module: Mathlib.RingTheory.FractionalIdeal.Operations

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
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ IsInteger R₁ (↑a' • 0)

pp: case refine_3
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (x y : K),
    x ∈ span R₁ (f '' ↑s) →
      y ∈ span R₁ (f '' ↑s) → IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • y) → IsInteger R₁ (↑a' • (x + y))

pp: case refine_4
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (a : R₁), ∀ x ∈ span R₁ (f '' ↑s), IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • a • x)

Tactic:
· rw [smul_zero]
      exact IsLocalization.isInteger_zero

Goal state after:
case refine_3
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (x y : K),
    x ∈ span R₁ (f '' ↑s) →
      y ∈ span R₁ (f '' ↑s) → IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • y) → IsInteger R₁ (↑a' • (x + y))

case refine_4
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (a : R₁), ∀ x ∈ span R₁ (f '' ↑s), IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • a • x)
Module: Mathlib.Algebra.Module.DedekindDomain

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ DirectSum.IsInternal fun p ↦ torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))

Tactic:
by
  have hM' := Module.isTorsionBySet_annihilator_top R M
  have hI := Submodule.annihilator_top_inter_nonZeroDivisors hM
  refine isInternal_prime_power_torsion_of_is_torsion_by_ideal ?_ hM'
  rw [Submodule.ne_bot_iff]
  obtain ⟨x, H, hx⟩ := hI; exact ⟨x, H, nonZeroDivisors.ne_zero hx⟩

Goal state after: