-- 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
hf₁ hf₂ :
  ∀ (y : Unit),
    Eq (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        ((0 : (a : Unit) → T ⊗[R] P.H1Cotangent) y : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        (0 : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) ↔
      Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y
hf₃ :
  ∀ (y : Unit),
    Eq (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        ((0 : (a : Unit) → T ⊗[R] P.H1Cotangent) y : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        (0 : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) →
      Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y
hf₄ :
  ∀ (y : Unit),
    Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y →
      Eq (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        ((0 : (a : Unit) → T ⊗[R] P.H1Cotangent) y : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        (0 : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
hf₅ hf₆ hf₇ :
  ∀ (y : Unit),
    Eq (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        ((0 : (a : Unit) → T ⊗[R] P.H1Cotangent) y : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        (0 : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) →
      Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y
hf₈ hf₉ hf₁₀ :
  ∀ (y : Unit),
    Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y →
      Eq (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        ((0 : (a : Unit) → T ⊗[R] P.H1Cotangent) y : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        (0 : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
hf₁₁ hf₁₂ hf₁₃ :
  ∀ (y : Unit),
    Eq (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        ((0 : (a : Unit) → T ⊗[R] P.H1Cotangent) y : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        (0 : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) →
      Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y
hf₁₄ hf₁₅ hf₁₆ :
  ∀ (y : Unit),
    Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y →
      Eq (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        ((0 : (a : Unit) → T ⊗[R] P.H1Cotangent) y : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        (0 : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
hf₁₇ hf₁₈ :
  ∀ (y : Unit),
    Eq (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        ((0 : (a : Unit) → T ⊗[R] P.H1Cotangent) y : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        (0 : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) →
      Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y
hf₁₉ :
  ∀ (y : Unit),
    Membership.mem (γ := Set Unit) (Set.range (ι := Unit) (⇑0 : (a : Unit) → Unit)) y →
      Eq (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        ((0 : (a : Unit) → T ⊗[R] P.H1Cotangent) y : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
        (0 : TensorProduct.{u_1, u_3, u} R T P.H1Cotangent)
⊢ Function.Exact (M := Unit) (N := Unit) (P := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) (⇑0 : (a : Unit) → Unit)
    (⇑0 : (a : Unit) → T ⊗[R] P.H1Cotangent)

Tactic:
tauto