-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x :
  HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
    (Ideal.span
      (Set.range (ι := σ)
        (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
          D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
pos :
  x = 0 →
    (Ideal.Quotient.mk
            (Ideal.span
              (Set.range (ι := σ)
                (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                  D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
          (a : MvPolynomial ι R) →
            MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
        0 =
      x
pos₁ :
  ¬x = 0 →
    x = -1 →
      (Ideal.Quotient.mk
              (Ideal.span
                (Set.range (ι := σ)
                  (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                    D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
            (a : MvPolynomial ι R) →
              MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
          (-1) =
        x
neg :
  ¬x = 0 →
    ¬x = -1 →
      (Ideal.Quotient.mk
              (Ideal.span
                (Set.range (ι := σ)
                  (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                    D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
            (a : MvPolynomial ι R) →
              MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
          (Function.surjInv (f :=
            (⇑(Ideal.Quotient.mk
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                        D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))) :
              (a : MvPolynomial ι R) →
                MvPolynomial ι R ⧸
                  Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
            ⋯ x) =
        x
⊢ (Ideal.Quotient.mk
          (Ideal.span
            (Set.range (ι := σ)
              (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
        (a : MvPolynomial ι R) →
          MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
      (if x = 0 then 0
      else
        if x = -1 then -1
        else
          Function.surjInv (f :=
            (⇑(Ideal.Quotient.mk
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                        D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))) :
              (a : MvPolynomial ι R) →
                MvPolynomial ι R ⧸
                  Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
            ⋯ x) =
    x

Tactic:
split_ifs