mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
h : p.Separable
x : S
hx : eval₂ f x p = 0
⊢ eval₂ f x (derivative p) ≠ 0

Tactic:
intro hx'

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
h : p.Separable
x : S
hx : eval₂ f x p = 0
hx' : eval₂ f x (derivative p) = 0
⊢ False
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : R
⊢ (X - C x).Separable

Tactic:
simpa only [sub_eq_add_neg, C_neg] using separable_X_add_C (-x)

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
hs : (Multiset.map (fun a ↦ X - C a) s).prod.Separable
⊢ s.Nodup

Tactic:
rw [Multiset.nodup_iff_ne_cons_cons]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
hs : (Multiset.map (fun a ↦ X - C a) s).prod.Separable
⊢ ∀ (a : R) (t : Multiset R), s ≠ a ::ₘ a ::ₘ t
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case hMM'
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
⊢ c.toMatrix ⇑b * b.toMatrix ⇑c = 1

pp: case hM'M
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
⊢ b.toMatrix ⇑c * c.toMatrix ⇑b = 1

Tactic:
<;>

Goal state after:
case hMM'
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
⊢ c.toMatrix ⇑b * b.toMatrix ⇑c = 1

case hM'M
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
⊢ b.toMatrix ⇑c * c.toMatrix ⇑b = 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case h.inr.zero
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.coeff 0 ≠ 0
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
ih : ∀ m < 0, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f = C (f.coeff 0)
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f

Tactic:
Classical.not_not

Goal state after:
case h.inr.zero
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : f.coeff 0 = 0
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
ih : ∀ m < 0, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f = C (f.coeff 0)
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Finite K
⊢ PerfectField K

Tactic:
obtain ⟨p, _instP⟩ := CharP.exists K

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Finite K
p : ℕ
_instP : CharP K p
⊢ PerfectField K
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]
⊢ Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots ≤ p ^ n • f.roots

Tactic:
refine le_iff_count.2 fun r ↦ ?_
  by_cases h : ∃ s, r = s ^ p ^ n
  · obtain ⟨s, rfl⟩ := h
    simp_rw [count_nsmul, count_roots, ← rootMultiplicity_expand_pow, ← count_roots, count_map,
      count_eq_card_filter_eq]
    exact card_le_card (monotone_filter_right _ fun _ h ↦ iterateFrobenius_inj R p n h)
  convert! Nat.zero_le _
  simp_rw [count_map, card_eq_zero]
  exact ext' fun t ↦ count_zero t ▸ count_filter_of_neg fun h' ↦ h ⟨t, h'⟩

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case e'_3.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ p ^ 1 = p

pp: case e'_4
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ p ^ 1 = p

Tactic:
<;>

Goal state after:
case e'_3.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ p ^ 1 = p

case e'_4
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ p ^ 1 = p
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case mp
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ LinearMap.det f = 0 → f.ker ≠ ⊥

pp: case mpr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ f.ker ≠ ⊥ → LinearMap.det f = 0

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ LinearMap.det f = 0 → f.ker ≠ ⊥

case mpr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ f.ker ≠ ⊥ → LinearMap.det f = 0
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hgf₂ : (expand F (p ^ n₁)) ((expand F (p ^ k)) g₂) = (expand F (p ^ n₁)) g₁
⊢ n₁ = n₁ + k ∧ g₁ = g₂

Tactic:
expand_inj (pow_pos hp n₁)

Goal state after:
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hgf₂ : (expand F (p ^ k)) g₂ = g₁
⊢ n₁ = n₁ + k ∧ g₁ = g₂
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inr.left
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
⊢ n₁ = n₁

pp: case inr.right
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
⊢ g₂ = g₂

Tactic:
<;>

Goal state after:
case inr.left
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
⊢ n₁ = n₁

case inr.right
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
⊢ g₂ = g₂
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
⊢ Multiset.map (fun x ↦ (iterateFrobeniusEquiv R p n) x)
      (p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots) =
    p ^ n • f.roots

Tactic:
Multiset.map_nsmul,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
⊢ p ^ n •
      Multiset.map (fun x ↦ (iterateFrobeniusEquiv R p n) x)
        (Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots) =
    p ^ n • f.roots
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
f g : R[X]
inst✝³ : CommRing S
i✝ : R →+* S
a : S
h✝ : eval₂ i✝ a f = 0
inst✝² : CommRing T
inst✝¹ : Algebra S R
inst✝ : Algebra S T
p : R[X]
i : R →ₐ[S] T
x : T
h : eval₂ (↑i) x p = 0
r : S
⊢ (↑↑(lift i.toRingHom x h)).toFun ((algebraMap S (AdjoinRoot p)) r) = (algebraMap S T) r

Tactic:
simp [lift_of h, AdjoinRoot.algebraMap_eq']

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case e'_2
R : Type u_1
inst✝ : CommRing R
r : R
⊢ (of (C r * X - 1)) r * root (C r * X - 1) = eval₂ (of (C r * X - 1)) (root (C r * X - 1)) (C r * X)

pp: case e'_3
R : Type u_1
inst✝ : CommRing R
r : R
⊢ 1 = eval₂ (of (C r * X - 1)) (root (C r * X - 1)) 1

Tactic:
<;>

Goal state after:
case e'_2
R : Type u_1
inst✝ : CommRing R
r : R
⊢ (of (C r * X - 1)) r * root (C r * X - 1) = eval₂ (of (C r * X - 1)) (root (C r * X - 1)) (C r * X)

case e'_3
R : Type u_1
inst✝ : CommRing R
r : R
⊢ 1 = eval₂ (of (C r * X - 1)) (root (C r * X - 1)) 1
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hAlg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
x✝ : R
⊢ (((map g q r hg).comp (map f p q hf)).comp (of p)) x✝ = ((map (g.comp f) p r ⋯).comp (of p)) x✝

pp: case hRoot
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
⊢ ((map g q r hg).comp (map f p q hf)) (root p) = (map (g.comp f) p r ⋯) (root p)

Tactic:
<;>

Goal state after:
case hAlg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
x✝ : R
⊢ (((map g q r hg).comp (map f p q hf)).comp (of p)) x✝ = ((map (g.comp f) p r ⋯).comp (of p)) x✝

case hRoot
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
⊢ ((map g q r hg).comp (map f p q hf)) (root p) = (map (g.comp f) p r ⋯) (root p)
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hAlg
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
x✝ : S
⊢ (((map (↑f) p q ⋯).comp (map (↑f.symm) q p ⋯)).comp (of q)) x✝ = ((RingHom.id (AdjoinRoot q)).comp (of q)) x✝

pp: case hRoot
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ ((map (↑f) p q ⋯).comp (map (↑f.symm) q p ⋯)) (root q) = (RingHom.id (AdjoinRoot q)) (root q)

Tactic:
<;>

Goal state after:
case hAlg
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
x✝ : S
⊢ (((map (↑f) p q ⋯).comp (map (↑f.symm) q p ⋯)).comp (of q)) x✝ = ((RingHom.id (AdjoinRoot q)).comp (of q)) x✝

case hRoot
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ ((map (↑f) p q ⋯).comp (map (↑f.symm) q p ⋯)) (root q) = (RingHom.id (AdjoinRoot q)) (root q)
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hAlg
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
x✝ : R
⊢ (((map (↑f.symm) q p ⋯).comp (map (↑f) p q ⋯)).comp (of p)) x✝ = ((RingHom.id (AdjoinRoot p)).comp (of p)) x✝

pp: case hRoot
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ ((map (↑f.symm) q p ⋯).comp (map (↑f) p q ⋯)) (root p) = (RingHom.id (AdjoinRoot p)) (root p)

Tactic:
<;>

Goal state after:
case hAlg
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
x✝ : R
⊢ (((map (↑f.symm) q p ⋯).comp (map (↑f) p q ⋯)).comp (of p)) x✝ = ((RingHom.id (AdjoinRoot p)).comp (of p)) x✝

case hRoot
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ ((map (↑f.symm) q p ⋯).comp (map (↑f) p q ⋯)) (root p) = (RingHom.id (AdjoinRoot p)) (root p)
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✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit ((LinearMap.toMatrix e e) ((e.constr ℕ) v)).det
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
i : ι
⊢ ((e.constr ℕ) v) (e i) = v i

Tactic:
e.constr_basis

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✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit ((LinearMap.toMatrix e e) ((e.constr ℕ) v)).det
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
i : ι
⊢ v i = v i
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hAlg
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
x✝ : T
⊢ (((mapAlgHom (↑f) p q ⋯).comp (mapAlgHom (↑f.symm) q p ⋯)).comp (ofAlgHom R q)) x✝ =
    ((AlgHom.id R (AdjoinRoot q)).comp (ofAlgHom R q)) x✝

pp: case hRoot
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ ((mapAlgHom (↑f) p q ⋯).comp (mapAlgHom (↑f.symm) q p ⋯)) (root q) = (AlgHom.id R (AdjoinRoot q)) (root q)

Tactic:
<;>

Goal state after:
case hAlg
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
x✝ : T
⊢ (((mapAlgHom (↑f) p q ⋯).comp (mapAlgHom (↑f.symm) q p ⋯)).comp (ofAlgHom R q)) x✝ =
    ((AlgHom.id R (AdjoinRoot q)).comp (ofAlgHom R q)) x✝

case hRoot
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ ((mapAlgHom (↑f) p q ⋯).comp (mapAlgHom (↑f.symm) q p ⋯)) (root q) = (AlgHom.id R (AdjoinRoot q)) (root q)
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hAlg
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
x✝ : S
⊢ (((mapAlgHom (↑f.symm) q p ⋯).comp (mapAlgHom (↑f) p q ⋯)).comp (ofAlgHom R p)) x✝ =
    ((AlgHom.id R (AdjoinRoot p)).comp (ofAlgHom R p)) x✝

pp: case hRoot
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ ((mapAlgHom (↑f.symm) q p ⋯).comp (mapAlgHom (↑f) p q ⋯)) (root p) = (AlgHom.id R (AdjoinRoot p)) (root p)

Tactic:
<;>

Goal state after:
case hAlg
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
x✝ : S
⊢ (((mapAlgHom (↑f.symm) q p ⋯).comp (mapAlgHom (↑f) p q ⋯)).comp (ofAlgHom R p)) x✝ =
    ((AlgHom.id R (AdjoinRoot p)).comp (ofAlgHom R p)) x✝

case hRoot
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ ((mapAlgHom (↑f.symm) q p ⋯).comp (mapAlgHom (↑f) p q ⋯)) (root p) = (AlgHom.id R (AdjoinRoot p)) (root p)
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✝³ : DecidableEq ι
inst✝² : Fintype ι
ι' : Type u_6
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ (b.toMatrix (v ∘ ⇑e)).det = b.det (v ∘ ⇑e)

Tactic:
det_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✝³ : DecidableEq ι
inst✝² : Fintype ι
ι' : Type u_6
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ (b.toMatrix (v ∘ ⇑e)).det = (b.toMatrix (v ∘ ⇑e)).det
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
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : M ≃ₗ[R] M'
v : ι → M'
⊢ (b.toMatrix (⇑f.symm ∘ v)).det = b.det (⇑f.symm ∘ v)

Tactic:
det_apply

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : M ≃ₗ[R] M'
v : ι → M'
⊢ (b.toMatrix (⇑f.symm ∘ v)).det = (b.toMatrix (⇑f.symm ∘ v)).det
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 • (Basis.mk hli hsp).coord k) ((Basis.mk hli hsp) k) = ((↑e.det).toLinearMap v k) ((Basis.mk hli hsp) k)

pp: case inr
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)
i k : ι
hik : k ≠ i
⊢ (e.det v • (Basis.mk hli hsp).coord i) ((Basis.mk hli hsp) k) = ((↑e.det).toLinearMap v i) ((Basis.mk hli hsp) k)

Tactic:
<;>

Goal state after:
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 • (Basis.mk hli hsp).coord k) ((Basis.mk hli hsp) k) = ((↑e.det).toLinearMap v k) ((Basis.mk hli hsp) k)

case inr
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)
i k : ι
hik : k ≠ i
⊢ (e.det v • (Basis.mk hli hsp).coord i) ((Basis.mk hli hsp) k) = ((↑e.det).toLinearMap v i) ((Basis.mk hli hsp) k)
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inr
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)
i k : ι
hik : k ≠ i
⊢ e.det v * ((Basis.mk hli hsp).coord i) (v k) = ↑e.det (update v i (v k))

Tactic:
mk_coord_apply_ne hik,

Goal state after:
case inr
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)
i k : ι
hik : k ≠ i
⊢ e.det v * 0 = ↑e.det (update v i (v k))