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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
f : M →ₗ⁅R,L⁆ N
g : N → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
⊢ ∀ {x : L} {m : N}, ((↑f).inverse g h₁ h₂).toFun ⁅x, m⁆ = ⁅x, ((↑f).inverse g h₁ h₂).toFun m⁆

Tactic:
intro x

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
f : M →ₗ⁅R,L⁆ N
g : N → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x : L
⊢ ∀ {m : N}, ((↑f).inverse g h₁ h₂).toFun ⁅x, m⁆ = ⁅x, ((↑f).inverse g h₁ h₂).toFun m⁆
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
m : ℕ
hm : n ≤ m
⊢ ∀ (x : M), ∃ y ∈ (f ^ m).ker, ∃ z ∈ range (f ^ n), y + z = x

Tactic:
intro x

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
m : ℕ
hm : n ≤ m
x : M
⊢ ∃ y ∈ (f ^ m).ker, ∃ z ∈ range (f ^ n), y + z = x
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
⊢ { toFun := fun m ↦ ⁅x + y, m⁆, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun m ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun m ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext m; apply add_lie

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
y : ↥N
n : ℕ
⊢ ↑(((toEnd R L ↥N) x ^ n) y) = ((toEnd R L M) x ^ n) ↑y

Tactic:
induction n generalizing y with

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

Goal state before:
pp: case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
⊢ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

Tactic:
intro x

Goal state after:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
x : L
⊢ ∀ (y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I : LieIdeal R L
⊢ ∀ {x y : L}, x ∈ (↑I).carrier → y ∈ (↑I).carrier → ⁅x, y⁆ ∈ (↑I).carrier

Tactic:
intro x

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
⊢ ∀ {y : L}, x ∈ (↑I).carrier → y ∈ (↑I).carrier → ⁅x, y⁆ ∈ (↑I).carrier
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
⊢ ∀ {x y : L}, x ∈ span R s → y ∈ span R s → ⁅x, y⁆ ∈ span R s

Tactic:
intro x

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x : L
⊢ ∀ {y : L}, x ∈ span R s → y ∈ span R s → ⁅x, y⁆ ∈ span R s
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
s : Set M
hs : s = ↑N
⊢ ∀ {x : L} {m : M}, m ∈ s → ⁅x, m⁆ ∈ s

Tactic:
exact hs.symm ▸ N.lie_mem

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
⊢ ∀ (x y : L) (m : ↥N), ⟨⁅x + y, ↑m⁆, ⋯⟩ = ⟨⁅x, ↑m⁆, ⋯⟩ + ⟨⁅y, ↑m⁆, ⋯⟩

Tactic:
intro x

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x : L
⊢ ∀ (y : L) (m : ↥N), ⟨⁅x + y, ↑m⁆, ⋯⟩ = ⟨⁅x, ↑m⁆, ⋯⟩ + ⟨⁅y, ↑m⁆, ⋯⟩
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
⊢ ∀ (x : L) (m n : ↥N), ⟨⁅x, ↑(m + n)⁆, ⋯⟩ = ⟨⁅x, ↑m⁆, ⋯⟩ + ⟨⁅x, ↑n⁆, ⋯⟩

Tactic:
intro x

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x : L
⊢ ∀ (m n : ↥N), ⟨⁅x, ↑(m + n)⁆, ⋯⟩ = ⟨⁅x, ↑m⁆, ⋯⟩ + ⟨⁅x, ↑n⁆, ⋯⟩
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
⊢ ∀ (x y : L) (m : ↥N), ⟨⁅x, ↑⟨⁅y, ↑m⁆, ⋯⟩⁆, ⋯⟩ = ⟨⁅⁅x, y⁆, ↑m⁆, ⋯⟩ + ⟨⁅y, ↑⟨⁅x, ↑m⁆, ⋯⟩⁆, ⋯⟩

Tactic:
intro x

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x : L
⊢ ∀ (y : L) (m : ↥N), ⟨⁅x, ↑⟨⁅y, ↑m⁆, ⋯⟩⁆, ⋯⟩ = ⟨⁅⁅x, y⁆, ↑m⁆, ⋯⟩ + ⟨⁅y, ↑⟨⁅x, ↑m⁆, ⋯⟩⁆, ⋯⟩
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
S : Set (LieSubmodule R L M)
⊢ ∀ {x : L} {m : M}, m ∈ (sSup {x | ∃ p ∈ S, ↑p = x}).carrier → ⁅x, m⁆ ∈ (sSup {x | ∃ p ∈ S, ↑p = x}).carrier

Tactic:
intro x

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
S : Set (LieSubmodule R L M)
x : L
⊢ ∀ {m : M}, m ∈ (sSup {x | ∃ p ∈ S, ↑p = x}).carrier → ⁅x, m⁆ ∈ (sSup {x | ∃ p ∈ S, ↑p = x}).carrier
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ ↑⁅I, N⁆ = Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
apply le_antisymm
  · let s := { ⁅(x : L), (n : M)⁆ | (x : I) (n : N) }
    have aux : ∀ (y : L), ∀ m' ∈ Submodule.span R s, ⁅y, m'⁆ ∈ Submodule.span R s := by
      intro y m' hm'
      refine Submodule.span_induction (R := R) (M := M) (s := s)
        (p := fun m' _ ↦ ⁅y, m'⁆ ∈ Submodule.span R s) ?_ ?_ ?_ ?_ hm'
      · rintro m'' ⟨x, n, hm''⟩; rw [← hm'', leibniz_lie]
        refine Submodule.add_mem _ ?_ ?_ <;> apply Submodule.subset_span
        · use ⟨⁅y, ↑x⁆, I.lie_mem x.property⟩, n
        · use x, ⟨⁅y, ↑n⁆, N.lie_mem n.property⟩
      · simp
      · intro m₁ m₂ _ _ hm₁ hm₂; rw [lie_add]; exact Submodule.add_mem _ hm₁ hm₂
      · intro t m'' _ hm''; rw [lie_smul]; exact Submodule.smul_mem _ t hm''
    change _ ≤ ({ Submodule.span R s with lie_mem := fun hm' => aux _ _ hm' } : LieSubmodule R L M)
    rw [lieIdeal_oper_eq_span, lieSpan_le]
    exact Submodule.subset_span
  · rw [lieIdeal_oper_eq_span]; apply submodule_span_le_lieSpan

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

Goal state before:
pp: case refine_2.mem.lie
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
hu : ⁅⟨w, ⋯⟩, ⟨u, hx✝⟩⁆ = 0
hv : ⁅⟨w, ⋯⟩, ⟨v, hy✝⟩⁆ = 0
⊢ ⁅⟨w, ⋯⟩, ⟨⁅u, v⁆, ⋯⟩⁆ = 0

Tactic:
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu hv ⊢
        rw [leibniz_lie]
        simp [hu, hv]

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

Goal state before:
pp: case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ↑(lieSpan R L ↑p) = p
⊢ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p

Tactic:
intro x

Goal state after:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ↑(lieSpan R L ↑p) = p
x : L
⊢ ∀ m ∈ p, ⁅x, m⁆ ∈ p
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: case mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : maxTrivSubmodule R L M = ⊤
⊢ ∀ (x : L) (m : M), ⁅x, m⁆ = 0

Tactic:
intro x

Goal state after:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : maxTrivSubmodule R L M = ⊤
x : L
⊢ ∀ (m : M), ⁅x, m⁆ = 0
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ Set.range ⇑f = Set.univ ↔ Function.Surjective ⇑f

Tactic:
Set.range_eq_univ

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ Function.Surjective ⇑f ↔ Function.Surjective ⇑f
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑(comap f ⁅map f I₁, map f I₂⁆)

Tactic:
intro x

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
x : L
⊢ x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → x ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
y : A
h : (minpoly A x).IsRoot y
key : minpoly A x = X - C y
⊢ (algebraMap A B) y = x

Tactic:
have := aeval A x

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
y : A
h : (minpoly A x).IsRoot y
key : minpoly A x = X - C y
this : (Polynomial.aeval x) (minpoly A x) = 0
⊢ (algebraMap A B) y = x
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ f ∈ map C I, (eval₂RingHom (C.comp (Quotient.mk I)) X) f = 0

Tactic:
intro a ha
  rw [← sum_monomial_eq a]
  dsimp
  rw [eval₂_sum]
  refine Finset.sum_eq_zero fun n _ => ?_
  dsimp
  rw [eval₂_monomial (C.comp (Quotient.mk I)) X]
  refine mul_eq_zero_of_left (Polynomial.ext fun m => ?_) (X ^ n)
  rw [RingHom.comp_apply, coeff_C]
  by_cases h : m = 0
  · simpa [h] using Quotient.eq_zero_iff_mem.2 ((mem_map_C_iff.1 ha) n)
  · simp [h]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ∀ (x : Fin pb.dim), x ≠ ⟨↑k + 1, ⋯⟩ → (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0

Tactic:
intro x

Goal state after:
case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
x : Fin pb.dim
⊢ x ≠ ⟨↑k + 1, ⋯⟩ → (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) (∑ v ∈ a.support, (monomial v) (coeff v a)) = 0

Tactic:
rw [coe_eval₂Hom, eval₂_sum]

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ ∑ x ∈ a.support, eval₂ (C.comp (Ideal.Quotient.mk I)) X ((monomial x) (coeff x a)) = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p q : MvPolynomial σ R
hp :
  eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
      ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
    (Ideal.Quotient.mk (Ideal.map C I)) p
hq :
  eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
      ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        ((Ideal.Quotient.mk (Ideal.map C I)) q)) =
    (Ideal.Quotient.mk (Ideal.map C I)) q
⊢ eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
      ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        ((Ideal.Quotient.mk (Ideal.map C I)) (p + q))) =
    (Ideal.Quotient.mk (Ideal.map C I)) (p + q)

Tactic:
Ideal.Quotient.lift_mk

Goal state after:
case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p q : MvPolynomial σ R
hp :
  eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) p) =
    (Ideal.Quotient.mk (Ideal.map C I)) p
hq :
  eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) q) =
    (Ideal.Quotient.mk (Ideal.map C I)) q
⊢ eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) (p + q)) =
    (Ideal.Quotient.mk (Ideal.map C I)) (p + q)
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case refine_2.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : Squarefree r
⊢ ∀ (x : R), Irreducible x → ¬x * x ∣ r

Tactic:
intro x

Goal state after:
case refine_2.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : Squarefree r
x : R
⊢ Irreducible x → ¬x * x ∣ r
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
z w : R
h0 : z ≠ 0 ∧ z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ z * w ≠ 0

Tactic:
exact h0.2

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inl
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ k : ℕ
r : F
hr : IsUnit r
hg₂ : (C r).Separable
hg₁ : ((expand F (p ^ k)) (C r)).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ k)) (C r)))
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) (C r) = C r

Tactic:
expand_C

Goal state after:
case inl
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ k : ℕ
r : F
hr : IsUnit r
hg₂ : (C r).Separable
hg₁ : ((expand F (p ^ k)) (C r)).Separable
hf : Irreducible (C r)
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) (C r) = C r
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : (X ^ p ^ n - (expand R (p ^ n)) (C y)).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
⊢ (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}

Tactic:
expand_C

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
⊢ (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case neg.h2
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ IsUnit (IsPrincipal.generator (annIdeal 𝕜 a)).leadingCoeff⁻¹

Tactic:
apply IsUnit.mk0

Goal state after:
case neg.h2
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ (IsPrincipal.generator (annIdeal 𝕜 a)).leadingCoeff⁻¹ ≠ 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
⊢ ∀ (x : M), (f ∘ₗ ↑e) x = (f ∘ₗ ↑e') ((e ≪≫ₗ e'.symm) x)

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
x : M
⊢ (f ∘ₗ ↑e) x = (f ∘ₗ ↑e') ((e ≪≫ₗ e'.symm) x)
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S →ₐ[R] T
g : T →ₐ[R] U
p : S[X]
q : T[X]
r : U[X]
hf : q ∣ Polynomial.map (↑f) p
hg : r ∣ Polynomial.map (↑g) q
⊢ (mapAlgHom g q r hg).comp (mapAlgHom f p q hf) = mapAlgHom (g.comp f) p r ⋯

Tactic:
by
  aesop

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ ⊤ ≤ (toAdjoin R x).range

Tactic:
← adjoin_adjoin_coe_preimage

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ adjoin R (Subtype.val ⁻¹' {x}) ≤ (toAdjoin R x).range
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ∀ {x y : L}, (-inner R L L).toFun ⁅x, y⁆ = ⁅(-inner R L L).toFun x, (-inner R L L).toFun y⁆

Tactic:
intro x

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ ∀ {y : L}, (-inner R L L).toFun ⁅x, y⁆ = ⁅(-inner R L L).toFun x, (-inner R L L).toFun y⁆
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ : ∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₂ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
restrict :
  ∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
x✝¹ x✝ : (_ : ℕ) × ℕ
i j i' j' : ℕ
h :
  (fun x ↦
        match x with
        | ⟨i, j⟩ => (i, j))
      ⟨i, j⟩ =
    (fun x ↦
        match x with
        | ⟨i, j⟩ => (i, j))
      ⟨i', j'⟩
⊢ ⟨i, j⟩ = ⟨i', j'⟩

Tactic:
by cases h; rfl

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
⊢ L ⧸ I → L ⧸ I → L ⧸ I

Tactic:
intro x

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x : L ⧸ I
⊢ L ⧸ I → L ⧸ I
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y : L ⧸ I
x₁ x₂ : L
⊢ ∀ (b₁ b₂ : L), (↑I).quotientRel x₁ b₁ → (↑I).quotientRel x₂ b₂ → mk ⁅x₁, x₂⁆ = mk ⁅b₁, b₂⁆

Tactic:
y₁

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y : L ⧸ I
x₁ x₂ y₁ : L
⊢ ∀ (b₂ : L), (↑I).quotientRel x₁ y₁ → (↑I).quotientRel x₂ b₂ → mk ⁅x₁, x₂⁆ = mk ⁅y₁, b₂⁆
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
⊢ H.normalizer ≤ H

Tactic:
intro x

Goal state after:
case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
⊢ x ∈ H.normalizer → x ∈ H
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : derivedSeries A (A ⊗[R] L) k ≤ ⊥
⊢ derivedSeries R L k ≤ ⊥

Tactic:
intro x

Goal state after:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : derivedSeries A (A ⊗[R] L) k ≤ ⊥
x : L
⊢ x ∈ derivedSeries R L k → x ∈ ⊥