mathlib-initiative/mathlib-tactics huggingface dataset:
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
toAddSubmonoid✝¹ : AddSubmonoid L
smul_mem'✝¹ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
lie_mem'✝¹ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.carrier
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
lie_mem'✝ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier
h :
  (fun L' ↦ L'.carrier) { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹, lie_mem' := lie_mem'✝¹ } =
    (fun L' ↦ L'.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝, lie_mem' := lie_mem'✝ }
⊢ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹, lie_mem' := lie_mem'✝¹ } =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝, lie_mem' := lie_mem'✝ }

Tactic:
congr

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
toAddSubmonoid✝¹ : AddSubmonoid L
smul_mem'✝¹ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
lie_mem'✝¹ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ }.carrier
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
lie_mem'✝ :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier
h :
  (fun L' ↦ L'.carrier) { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹, lie_mem' := lie_mem'✝¹ } =
    (fun L' ↦ L'.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝, lie_mem' := lie_mem'✝ }
⊢ toAddSubmonoid✝¹ = toAddSubmonoid✝
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 : L
⊢ ∀ {y : L}, x ∈ (↑I).carrier → y ∈ (↑I).carrier → ⁅x, y⁆ ∈ (↑I).carrier

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
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
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K
x : L
⊢ ∀ (y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

Tactic:
y

Goal state after:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K
x y : L
⊢ x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
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 : L
⊢ ∀ {y : L}, x ∈ span R s → y ∈ span R s → ⁅x, y⁆ ∈ span R s

Tactic:
y

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 y : L
⊢ x ∈ span R s → y ∈ span R s → ⁅x, y⁆ ∈ span R s
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mk.mk
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
toSubmodule✝¹ : Submodule R M
lie_mem✝¹ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝¹.carrier → ⁅x, m⁆ ∈ toSubmodule✝¹.carrier
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h :
  (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } =
    (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
⊢ { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } = { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }

Tactic:
congr

Goal state after:
case mk.mk
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
toSubmodule✝¹ : Submodule R M
lie_mem✝¹ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝¹.carrier → ⁅x, m⁆ ∈ toSubmodule✝¹.carrier
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h :
  (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } =
    (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
⊢ toSubmodule✝¹ = toSubmodule✝
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mk.mk
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
toSubmodule✝¹ : Submodule R M
lie_mem✝¹ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝¹.carrier → ⁅x, m⁆ ∈ toSubmodule✝¹.carrier
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h : ↑{ toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } = ↑{ toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
⊢ { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } = { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }

Tactic:
congr

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 : L
⊢ ∀ (y : L) (m : ↥N), ⟨⁅x + y, ↑m⁆, ⋯⟩ = ⟨⁅x, ↑m⁆, ⋯⟩ + ⟨⁅y, ↑m⁆, ⋯⟩

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
x y : L
⊢ ∀ (m : ↥N), ⟨⁅x + y, ↑m⁆, ⋯⟩ = ⟨⁅x, ↑m⁆, ⋯⟩ + ⟨⁅y, ↑m⁆, ⋯⟩
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mp
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : ∀ (x m : L') (x_1 : L), f x_1 = m → ∃ y, f y = ⁅x, m⁆
x : L'
⊢ ∀ (y : L), ∃ z, ⁅x, f y⁆ = f z

Tactic:
y

Goal state after:
case mp
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : ∀ (x m : L') (x_1 : L), f x_1 = m → ∃ y, f y = ⁅x, m⁆
x : L'
y : L
⊢ ∃ z, ⁅x, f y⁆ = f z
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mpr
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z
x : L'
⊢ ∀ (m : L') (x_1 : L), f x_1 = m → ∃ y, f y = ⁅x, m⁆

Tactic:
y

Goal state after:
case mpr
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z
x y : L'
⊢ ∀ (x_1 : L), f x_1 = y → ∃ y_1, f y_1 = ⁅x, y⁆
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
⊢ ∀ (y : L) (m : ↥N), ⟨⁅x, ↑⟨⁅y, ↑m⁆, ⋯⟩⁆, ⋯⟩ = ⟨⁅⁅x, y⁆, ↑m⁆, ⋯⟩ + ⟨⁅y, ↑⟨⁅x, ↑m⁆, ⋯⟩⁆, ⋯⟩

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
x 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
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
t : R
x : L
⊢ ∀ (m : ↥N), ⁅t • x, m⁆ = t • ⁅x, m⁆

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
t : R
x : L
y : ↥N
⊢ ⁅t • x, y⁆ = t • ⁅x, y⁆
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
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
t : R
x : L
⊢ ∀ (m : ↥N), ⁅x, t • m⁆ = t • ⁅x, m⁆

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
t : R
x : L
y : ↥N
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆
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
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Tactic:
congr

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 : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ (fun x ↦ ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x) = fun x ↦ ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
int : IsIntegral A x
⊢ (minpoly A x).natDegree = 1 ↔ (minpoly A x).natDegree < 2

Tactic:
exact ⟨fun h ↦ h.trans_lt one_lt_two, fun h ↦ by linarith only [minpoly.natDegree_pos int, h]⟩

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ Submodule.span R (⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}) = Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
congr

Goal state after:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ Submodule.comap (↑f) (Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}) =
    Submodule.comap (↑f) (Submodule.span R (⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}))

Tactic:
congr

Goal state after:
case e_p
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ (fun x ↦ ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x) = fun x ↦ ∃ a ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, ↑f a = x
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
| comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆

Tactic:
congr

Goal state after:
case f
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
| I.incl

case J
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
| ⁅I ⊓ I₁, I ⊓ I₂⁆
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
⊢ ∀ (q : K[X]), q.Monic → (Polynomial.aeval σ.toLinearMap) q = 0 → (X ^ orderOf σ - C 1).degree ≤ q.degree

Tactic:
intro q hq hs

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : (Polynomial.aeval σ.toLinearMap) q = 0
⊢ (X ^ orderOf σ - C 1).degree ≤ q.degree
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
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i < pb.dim
⊢ (f %ₘ minpoly A pb.gen).coeff i • ((pb.basis.constr A) fun i ↦ y ^ ↑i) (pb.gen ^ i) =
    (f %ₘ minpoly A pb.gen).coeff i • y ^ i

Tactic:
congr

Goal state after:
case neg.e_a
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i < pb.dim
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) (pb.gen ^ i) = y ^ i
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
K : Type u_6
inst✝⁴ : Field K
inst✝³ : Algebra A S
S' : Type u_7
inst✝² : Ring S'
inst✝¹ : Algebra A S'
inst✝ : IsDomain B
pb : PowerBasis A S
x : B
⊢ map (algebraMap A B) (minpoly A pb.gen) ≠ 0

Tactic:
exact map_monic_ne_zero (minpoly.monic pb.isIntegral_gen)

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁶ : AddCommGroup M
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type u_6
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ ((toMatrix b b) f).det = ((toMatrix c c) f).det

Tactic:
rw [← linearMap_toMatrix_mul_basis_toMatrix c b c, ← basis_toMatrix_mul_linearMap_toMatrix b c b,
      Matrix.det_conj_of_mul_eq_one] <;>
    rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
x✝ : M →ₗ[A] M
h✝ : ∃ s, Nonempty (Basis (↥s) A M)
⊢ (detAux (Trunc.mk ⋯.some)) x✝ = (detAux (Trunc.mk ⋯.some)) x✝

Tactic:
congr

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
H : ∃ s, Nonempty (Basis (↥s) R M)
⊢ Free R M

Tactic:
rcases H with ⟨s, ⟨hs⟩⟩
    exact Module.Free.of_basis hs

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: M : Type u_1
p : ℕ
inst✝¹ : CommMonoid M
inst✝ : PerfectRing M p
n✝ n : ℕ
ih : powMulEquiv M (p ^ n) = powMulEquiv M p ^ n
⊢ powMulEquiv M (p ^ n.succ) = powMulEquiv M (p * p ^ n)

Tactic:
congr

Goal state after:
M : Type u_1
p : ℕ
inst✝¹ : CommMonoid M
inst✝ : PerfectRing M p
n✝ n : ℕ
ih : powMulEquiv M (p ^ n) = powMulEquiv M p ^ n
⊢ p ^ n.succ = p * p ^ n
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
r : R
⊢ p ^ n * (filter (fun x ↦ r ^ p ^ n = x) f.roots).card =
    p ^ n * (filter (fun a ↦ r = (iterateFrobeniusEquiv R p n).symm a) f.roots).card

Tactic:
congr

Goal state after:
case e_a.e_p
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
r : R
⊢ (fun x ↦ r ^ p ^ n = x) = fun a ↦ r = (iterateFrobeniusEquiv R p n).symm a
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
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ (((Pi.basis fun x ↦ b).reindex
            ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans
              (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))).repr
        ((pi fun i ↦ f i ∘ₗ proj i)
          ((⇑(Pi.basis fun x ↦ b) ∘
              ⇑((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans
                    (Equiv.prodComm ι (Free.ChooseBasisIndex R M))).symm)
            (j₁, j₂))))
      (i₁, i₂) =
    if i₂ = j₂ then (toMatrix b b) (f i₂) i₁ j₁ else 0

Tactic:
Function.comp_apply,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ (((Pi.basis fun x ↦ b).reindex
            ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans
              (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))).repr
        ((pi fun i ↦ f i ∘ₗ proj i)
          ((Pi.basis fun x ↦ b)
            (((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans
                  (Equiv.prodComm ι (Free.ChooseBasisIndex R M))).symm
              (j₁, j₂)))))
      (i₁, i₂) =
    if i₂ = j₂ then (toMatrix b b) (f i₂) i₁ j₁ else 0
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a

Tactic:
rw [annIdealGenerator, Ideal.span_singleton_mul_right_unit, Ideal.span_singleton_generator]

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
⊢ IsUnit (C (IsPrincipal.generator (annIdeal 𝕜 a)).leadingCoeff⁻¹)
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
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ (b.repr ((⇑(f i₂) ∘ ⇑(proj i₂)) (Pi.single j₂ (b j₁)))) i₁ = if i₂ = j₂ then (toMatrix b b) (f i₂) i₁ j₁ else 0

Tactic:
Function.comp_apply,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ (b.repr ((f i₂) ((proj i₂) (Pi.single j₂ (b j₁))))) i₁ = if i₂ = j₂ then (toMatrix b b) (f i₂) i₁ j₁ else 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
k : ι
⊢ e.det v = ↑e.det v

Tactic:
congr

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case e'_3.e'_1
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ ↑(∏ i, w i)⁻¹ = ∏ i, ↑(w i)⁻¹

Tactic:
simp [← Finset.prod_inv_distrib]

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: case mk.mk
R : Type u_1
L : Type u_2
M : Type u_3
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
D D1 D2 : LieDerivation R L M
a b : L
toLinearMap✝¹ : L →ₗ[R] M
leibniz'✝¹ : ∀ (a b : L), toLinearMap✝¹ ⁅a, b⁆ = ⁅a, toLinearMap✝¹ b⁆ - ⁅b, toLinearMap✝¹ a⁆
toLinearMap✝ : L →ₗ[R] M
leibniz'✝ : ∀ (a b : L), toLinearMap✝ ⁅a, b⁆ = ⁅a, toLinearMap✝ b⁆ - ⁅b, toLinearMap✝ a⁆
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝¹, leibniz' := leibniz'✝¹ } =
    (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ }
⊢ { toLinearMap := toLinearMap✝¹, leibniz' := leibniz'✝¹ } = { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ }

Tactic:
congr

Goal state after:
case mk.mk
R : Type u_1
L : Type u_2
M : Type u_3
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
D D1 D2 : LieDerivation R L M
a b : L
toLinearMap✝¹ : L →ₗ[R] M
leibniz'✝¹ : ∀ (a b : L), toLinearMap✝¹ ⁅a, b⁆ = ⁅a, toLinearMap✝¹ b⁆ - ⁅b, toLinearMap✝¹ a⁆
toLinearMap✝ : L →ₗ[R] M
leibniz'✝ : ∀ (a b : L), toLinearMap✝ ⁅a, b⁆ = ⁅a, toLinearMap✝ b⁆ - ⁅b, toLinearMap✝ a⁆
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝¹, leibniz' := leibniz'✝¹ } =
    (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ }
⊢ toLinearMap✝¹ = toLinearMap✝