-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FormallyUnramified K L
inst_4 : EssFiniteType K L
inst_5 : IsPurelyInseparable K L
have : Nontrivial.{u_3} (L ⊗[K] L)
have₁ :
  ∀ (this : Nontrivial.{u_3} (L ⊗[K] L)),
    Eq.{u_3 + 1} (α := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) ⊤
have₂ : Nontrivial.{u_3} (L ⊗[K] L)
have₃ have₄ :
  ∀ (this : Nontrivial.{u_3} (L ⊗[K] L)),
    Eq.{u_3 + 1} (α := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) ⊤
have₅ :
  ∀ (this : Nontrivial.{u_3} (L ⊗[K] L)),
    LE.le.{u_3} (α := Subring L) ⊤ (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L))
have₆ :
  ∀ (this : Nontrivial.{u_3} (L ⊗[K] L)) ⦃x : L⦄,
    Membership.mem (γ := Subring L) ⊤ x →
      Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
⊢ Eq.{u_3 + 1} (α := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) ⊤
have have₇ : ∀ (this : Nontrivial.{u_3} (L ⊗[K] L)) ⦃x : L⦄,
  Membership.mem (γ := Subring L) ⊤ x →
    ∀ (n : ℕ)
      (hn :
        Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) (x ^ ringExpChar K ^ n)),
      Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
Tactic: classical
  have : Nontrivial (L ⊗[K] L) := by
    rw [← not_subsingleton_iff_nontrivial, ← rank_zero_iff (R := K), rank_tensorProduct',
      mul_eq_zero, or_self, rank_zero_iff, not_subsingleton_iff_nontrivial]
    infer_instance
  rw [← top_le_iff]
  intro x _
  obtain ⟨n, hn⟩ := IsPurelyInseparable.pow_mem K (ringExpChar K) x
  have : ExpChar (L ⊗[K] L) (ringExpChar K) := by
    refine expChar_of_injective_ringHom (algebraMap K _).injective (ringExpChar K)
  have : (1 ⊗ₜ x - x ⊗ₜ 1 : L ⊗[K] L) ^ (ringExpChar K) ^ n = 0 := by
    rw [sub_pow_expChar_pow, TensorProduct.tmul_pow, one_pow, TensorProduct.tmul_pow, one_pow]
    obtain ⟨r, hr⟩ := hn
    rw [← hr, algebraMap_eq_smul_one, TensorProduct.smul_tmul, sub_self]
  have H : (1 ⊗ₜ x : L ⊗[K] L) = x ⊗ₜ 1 := by
    have inst : IsReduced (L ⊗[K] L) := isReduced_of_field L _
    exact sub_eq_zero.mp (IsNilpotent.eq_zero ⟨_, this⟩)
  by_cases h' : LinearIndependent K ![1, x]
  · have h := h'.linearIndepOn_id
    let S := h.extend (Set.subset_univ _)
    let a : S := ⟨1, h.subset_extend _ (by simp)⟩
    have ha : Basis.extend h a = 1 := by simp [a]
    let b : S := ⟨x, h.subset_extend _ (by simp)⟩
    have hb : Basis.extend h b = x := by simp [b]
    by_cases e : a = b
    · obtain rfl : 1 = x := congr_arg Subtype.val e
      exact ⟨1, map_one _⟩
    have := DFunLike.congr_fun
      (DFunLike.congr_arg ((Basis.extend h).tensorProduct (Basis.extend h)).repr H) (a, b)
    simp only [Basis.tensorProduct_repr_tmul_apply, ← ha, ← hb, Basis.repr_self, smul_eq_mul,
      Finsupp.single_apply, e, Ne.symm e, ↓reduceIte, mul_one, mul_zero, one_ne_zero] at this
  · rw [LinearIndependent.pair_iff] at h'
    simp only [not_forall, not_and, exists_prop] at h'
    obtain ⟨a, b, e, hab⟩ := h'
    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
    use (-this.unit⁻¹ * a)
    rw [map_mul, ← Algebra.smul_def, algebraMap_eq_smul_one, eq_neg_iff_add_eq_zero.mpr e,
      smul_neg, neg_smul, neg_neg, smul_smul, this.val_inv_mul, one_smul]