-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this_2 : Module.Finite K L
B : Type (max u_1 u_2)
x_1 : CommRing B
x_2 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I) ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)
helper :
  ∀ (x : B),
    Eq (α := B ⧸ I) ((IsScalarTower.toAlgHom K B (B ⧸ I) : (a : B) → B ⧸ I) x : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I)
hx' :
  Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I)
    (0 : B ⧸ I)
this :
  IsUnit (M := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
        ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
      B ⧸ I)
u : B
hu : (Ideal.Quotient.mk I : (a : B) → B ⧸ I) u = -(↑this.unit⁻¹ : B ⧸ I)
h₁ :
  Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
        (HMul.hMul (α := B)
            ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : B) u +
          1) :
      B ⧸ I)
    (0 : B ⧸ I)
h₂ :
  HAdd.hAdd (α := B ⧸ I) (β := B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
          (HMul.hMul (α := B)
            ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : B) u) :
        B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 : B ⧸ I) =
    0
h₃ :
  HMul.hMul (α := B ⧸ I) (β := B ⧸ I)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
            ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
          B ⧸ I)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) +
      (Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 =
    0
h₄ :
  HMul.hMul (α := B ⧸ I) (β := B ⧸ I)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
            ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
          B ⧸ I)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) +
      1 =
    0
h₅ :
  HMul.hMul (α := B ⧸ I)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
            ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
          B ⧸ I)
        (-(↑this.unit⁻¹ : B ⧸ I)) +
      1 =
    0
h₆ :
  -HMul.hMul (α := B ⧸ I)
          ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
              ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
            B ⧸ I)
          (↑this.unit⁻¹ : B ⧸ I) +
      1 =
    0
h₇ : HAdd.hAdd (α := B ⧸ I) (-1) 1 = 0
h₈ h₉ : Eq (α := B ⧸ I) 0 0
⊢ HMul.hMul (α := B) ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : B) u +
      1 ∈
    I

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, map_add, map_mul, map_one, hu, mul_neg,
      IsUnit.mul_val_inv, neg_add_cancel]

Premises used: IsUnit.mul_val_inv, map_add, Ideal.Quotient.eq_zero_iff_mem, map_mul, neg_add_cancel, map_one, mul_neg