-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
hg₁ hg₂ :
  ∀ (y : Unit),
    Eq (α := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        ((0 : (a : Unit) → P.baseChange.H1Cotangent) y : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        (0 : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) ↔
      Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y
hg₃ :
  ∀ (y : Unit),
    Eq (α := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        ((0 : (a : Unit) → P.baseChange.H1Cotangent) y : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        (0 : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) →
      Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y
hg₄ :
  ∀ (y : Unit),
    Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y →
      Eq (α := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        ((0 : (a : Unit) → P.baseChange.H1Cotangent) y : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        (0 : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
hg₅ hg₆ hg₇ :
  ∀ (y : Unit),
    Eq (α := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        ((0 : (a : Unit) → P.baseChange.H1Cotangent) y : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        (0 : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) →
      Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y
hg₈ hg₉ hg₁₀ :
  ∀ (y : Unit),
    Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y →
      Eq (α := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        ((0 : (a : Unit) → P.baseChange.H1Cotangent) y : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        (0 : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
hg₁₁ hg₁₂ hg₁₃ :
  ∀ (y : Unit),
    Eq (α := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        ((0 : (a : Unit) → P.baseChange.H1Cotangent) y : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        (0 : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) →
      Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y
hg₁₄ hg₁₅ hg₁₆ :
  ∀ (y : Unit),
    Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y →
      Eq (α := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        ((0 : (a : Unit) → P.baseChange.H1Cotangent) y : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        (0 : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
hg₁₇ hg₁₈ :
  ∀ (y : Unit),
    Eq (α := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        ((0 : (a : Unit) → P.baseChange.H1Cotangent) y : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        (0 : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) →
      Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y
hg₁₉ :
  ∀ (y : Unit),
    Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y →
      Eq (α := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        ((0 : (a : Unit) → P.baseChange.H1Cotangent) y : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
        (0 : Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
⊢ Function.Exact (M := Unit) (N := Unit) (P := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
    (⇑0 : (a : Unit) → Unit) (⇑0 : (a : Unit) → P.baseChange.H1Cotangent)

Tactic:
tauto