-- Mathlib/RingTheory/Unramified/Field.lean
theorem range_eq_top_of_isPurelyInseparable
    [IsPurelyInseparable K L] : (algebraMap K L).range = ⊤

Proof state:
case intro
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
⊢ x ∈ (algebraMap K L).range

Tactic:
have : ExpChar (L ⊗[K] L) (ringExpChar K) := by
  refine expChar_of_injective_ringHom (algebraMap K _).injective (ringExpChar K)

Result:
case intro
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this : ExpChar (L ⊗[K] L) (ringExpChar K)
⊢ x ∈ (algebraMap K L).range

Proof state:
case neg.intro.intro.intro
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
a b : K
e : a • 1 + b • x = 0
hab : a = 0 → ¬b = 0
⊢ x ∈ (algebraMap K L).range

Tactic:
have : IsUnit b := by
  rw [isUnit_iff_ne_zero]
  rintro rfl
  rw [zero_smul, ← algebraMap_eq_smul_one, add_zero,
    (injective_iff_map_eq_zero' _).mp (algebraMap K L).injective] at e
  cases hab e rfl

Result:
case neg.intro.intro.intro
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝² : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝¹ : ExpChar (L ⊗[K] L) (ringExpChar K)
this✝ : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
a b : K
e : a • 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
⊢ x ∈ (algebraMap K L).range

Proof state:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this : ExpChar (L ⊗[K] L) (ringExpChar K)
⊢ (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0

Tactic:
rw [sub_pow_expChar_pow, TensorProduct.tmul_pow, one_pow, TensorProduct.tmul_pow, one_pow]

Result:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this : ExpChar (L ⊗[K] L) (ringExpChar K)
⊢ 1 ⊗ₜ[K] (x ^ ringExpChar K ^ n) - (x ^ ringExpChar K ^ n) ⊗ₜ[K] 1 = 0

Proof state:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
a b : K
e : a • 1 + b • x = 0
hab : a = 0 → ¬b = 0
⊢ b ≠ 0

Tactic:
rintro rfl

Result:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
a : K
e : a • 1 + 0 • x = 0
hab : a = 0 → ¬0 = 0
⊢ False

Proof state:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
inst : IsReduced (L ⊗[K] L)
⊢ 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1

Tactic:
exact sub_eq_zero.mp (IsNilpotent.eq_zero ⟨_, this⟩)

Result:
no goals

Proof state:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
h' : LinearIndependent K ![1, x]
h : LinearIndepOn K _root_.id (Set.range ![1, x])
S : Set L := h.extend ⋯
⊢ 1 ∈ Set.range ![1, x]

Tactic:
simp

Result:
no goals

Proof state:
case neg
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
h' : LinearIndependent K ![1, x]
h : LinearIndepOn K _root_.id (Set.range ![1, x])
S : Set L := h.extend ⋯
a : ↑S := ⟨1, ⋯⟩
ha : (Basis.extend h) a = 1
b : ↑S := ⟨x, ⋯⟩
hb : (Basis.extend h) b = x
e : ¬a = b
⊢ x ∈ (algebraMap K L).range

Tactic:
have := DFunLike.congr_fun
  (DFunLike.congr_arg ((Basis.extend h).tensorProduct (Basis.extend h)).repr H) (a, b)

Result:
case neg
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝² : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝¹ : ExpChar (L ⊗[K] L) (ringExpChar K)
this✝ : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
h' : LinearIndependent K ![1, x]
h : LinearIndepOn K _root_.id (Set.range ![1, x])
S : Set L := h.extend ⋯
a : ↑S := ⟨1, ⋯⟩
ha : (Basis.extend h) a = 1
b : ↑S := ⟨x, ⋯⟩
hb : (Basis.extend h) b = x
e : ¬a = b
this :
  (((Basis.extend h).tensorProduct (Basis.extend h)).repr (1 ⊗ₜ[K] x)) (a, b) =
    (((Basis.extend h).tensorProduct (Basis.extend h)).repr (x ⊗ₜ[K] 1)) (a, b)
⊢ x ∈ (algebraMap K L).range

Proof state:
case pos
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
n : ℕ
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
a✝ : 1 ∈ ⊤
hn : 1 ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this : (1 ⊗ₜ[K] 1 - 1 ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] 1 = 1 ⊗ₜ[K] 1
h' : LinearIndependent K ![1, 1]
h : LinearIndepOn K _root_.id (Set.range ![1, 1])
S : Set L := h.extend ⋯
a : ↑S := ⟨1, ⋯⟩
ha : (Basis.extend h) a = 1
b : ↑S := ⟨1, ⋯⟩
hb : (Basis.extend h) b = 1
e : a = b
⊢ 1 ∈ (algebraMap K L).range

Tactic:
exact ⟨1, map_one _⟩

Result:
no goals