awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
t : T
x : TensorProduct.{u, u_2, u} P.Ring S Ω[P.Ring⁄R]
zero :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] 0) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
⊢ (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] x) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) x :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
have add : ∀ (x y : TensorProduct.{u, u_2, u} P.Ring S Ω[P.Ring⁄R])
  (hx :
    (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] x) =
      HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
        ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) x :
          CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange))
  (hy :
    (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] y) =
      HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
        ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) y :
          CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)),
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] (x + y)) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) (x + y) :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
Tactic: induction x with
  | zero => rw [tmul_zero, LinearEquiv.map_zero, LinearMap.map_zero, smul_zero]
  | add x y hx hy => rw [tmul_add, LinearEquiv.map_add, LinearMap.map_add, smul_add, hx, hy]
  | tmul s y =>
  simp [tensorCotangentSpace_tmul_tmul, CotangentSpace.map_tmul_eq_tmul_map,
    smul_tmul', Algebra.smul_def, RingHom.algebraMap_toAlgebra]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
t : T
x : TensorProduct.{u, u_2, u} P.Ring S Ω[P.Ring⁄R]
zero :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] 0) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
add :
  ∀ (x y : TensorProduct.{u, u_2, u} P.Ring S Ω[P.Ring⁄R])
    (hx :
      (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] x) =
        HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
          ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) x :
            CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange))
    (hy :
      (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] y) =
        HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
          ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) y :
            CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)),
    (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] (x + y)) =
      HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
        ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) (x + y) :
          CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
⊢ (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] x) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) x :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
have tmul : ∀ (s : S) (y : Ω[P.Ring⁄R]),
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] (s ⊗ₜ[P.Ring] y)) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) (s ⊗ₜ[P.Ring] y) :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
Tactic: induction x with
  | zero => rw [tmul_zero, LinearEquiv.map_zero, LinearMap.map_zero, smul_zero]
  | add x y hx hy => rw [tmul_add, LinearEquiv.map_add, LinearMap.map_add, smul_add, hx, hy]
  | tmul s y =>
  simp [tensorCotangentSpace_tmul_tmul, CotangentSpace.map_tmul_eq_tmul_map,
    smul_tmul', Algebra.smul_def, RingHom.algebraMap_toAlgebra]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
t : T
x : P.Cotangent
⊢ (P.tensorCotangentOfFlat T : (a : T ⊗[R] P.Cotangent) → P.baseChange.Cotangent) (t ⊗ₜ[R] x) =
    HSMul.hSMul (β := Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((Cotangent.map (toBaseChange T) : (a : P.Cotangent) → P.baseChange.Cotangent) x :
        Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
have obtain : ∀ (x : ↥P.ker),
  (P.tensorCotangentOfFlat T : (a : T ⊗[R] P.Cotangent) → P.baseChange.Cotangent)
      (t ⊗ₜ[R] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x) =
    HSMul.hSMul (β := Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((Cotangent.map (toBaseChange T) : (a : P.Cotangent) → P.baseChange.Cotangent)
          ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x) :
        Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
Tactic: obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
⊢ Function.Bijective (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) (β :=
    Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
    (⇑(P.tensorToH1Cotangent T) : (a : T ⊗[R] P.H1Cotangent) → P.baseChange.H1Cotangent)
have hc₁ : Eq (α := Unit →ₗ[R] Unit) (0 ∘ₗ 0) (0 ∘ₗ 0)
Tactic: apply LinearMap.bijective_of_surjective_of_bijective_of_bijective_of_injective (M₁ := Unit)
      (N₁ := Unit) (M₂ := Unit) (N₂ := Unit)
    -- The row `0 → 0 → T ⊗ H¹(P) → T ⊗ P.Cotangent → T ⊗ P.CotangentSpace`.
    0 0
    ((P.h1Cotangentι.restrictScalars R).lTensor T)
    ((P.cotangentComplex.restrictScalars R).lTensor T)
    -- The row `0 → 0 → H¹(T ⊗ P) → (T ⊗ P).Cotangent → (T ⊗ P).CotangentSpace`.
    0 0
    (h1Cotangentι.restrictScalars R)
    ((P.baseChange (T := T)).cotangentComplex.restrictScalars R)
    -- The vertical maps induced by base change.
    0 0
    ((P.tensorToH1Cotangent T).restrictScalars R)
    ((P.tensorCotangentOfFlat T).restrictScalars R)
    ((P.tensorCotangentSpace T).restrictScalars R)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
hc₁ : Eq (α := Unit →ₗ[R] Unit) (0 ∘ₗ 0) (0 ∘ₗ 0)
⊢ Function.Bijective (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) (β :=
    Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
    (⇑(P.tensorToH1Cotangent T) : (a : T ⊗[R] P.H1Cotangent) → P.baseChange.H1Cotangent)
have hc₂ : Eq (α := Unit →ₗ[R] Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) (0 ∘ₗ 0)
  ((↑R :
        {S : Type u_3} →
          {M M₂ : Type (max u u_3)} →
            [inst : Semiring R] →
              [inst_6 : Semiring S] →
                [inst_7 : AddCommMonoid M] →
                  [inst_8 : AddCommMonoid M₂] →
                    [inst_9 : Module R M] →
                      [inst_10 : Module R M₂] →
                        [inst_11 : Module S M] →
                          [inst_12 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (P.tensorToH1Cotangent T) ∘ₗ
    0)
Tactic: apply LinearMap.bijective_of_surjective_of_bijective_of_bijective_of_injective (M₁ := Unit)
      (N₁ := Unit) (M₂ := Unit) (N₂ := Unit)
    -- The row `0 → 0 → T ⊗ H¹(P) → T ⊗ P.Cotangent → T ⊗ P.CotangentSpace`.
    0 0
    ((P.h1Cotangentι.restrictScalars R).lTensor T)
    ((P.cotangentComplex.restrictScalars R).lTensor T)
    -- The row `0 → 0 → H¹(T ⊗ P) → (T ⊗ P).Cotangent → (T ⊗ P).CotangentSpace`.
    0 0
    (h1Cotangentι.restrictScalars R)
    ((P.baseChange (T := T)).cotangentComplex.restrictScalars R)
    -- The vertical maps induced by base change.
    0 0
    ((P.tensorToH1Cotangent T).restrictScalars R)
    ((P.tensorCotangentOfFlat T).restrictScalars R)
    ((P.tensorCotangentSpace T).restrictScalars R)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
⊢ 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)
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
⊢ 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)
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
⊢ 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)
have 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)
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
⊢ Function.Exact (M := Unit) (N := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) (P :=
    TensorProduct.{u_1, u_3, u} R T P.Cotangent) (⇑0 : (a : Unit) → T ⊗[R] P.H1Cotangent)
    (⇑(LinearMap.lTensor T
          ((↑R :
              {S : Type u_2} →
                {M M₂ : Type u} →
                  [inst : Semiring R] →
                    [inst_6 : Semiring S] →
                      [inst_7 : AddCommMonoid M] →
                        [inst_8 : AddCommMonoid M₂] →
                          [inst_9 : Module R M] →
                            [inst_10 : Module R M₂] →
                              [inst_11 : Module S M] →
                                [inst_12 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            h1Cotangentι)) :
      (a : T ⊗[R] P.H1Cotangent) → T ⊗[R] P.Cotangent)
have hf₂ : Function.Injective (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) (β :=
  TensorProduct.{u_1, u_3, u} R T P.Cotangent)
  (⇑(LinearMap.lTensor T
          ((↑R :
              {S : Type u_2} →
                {M M₂ : Type u} →
                  [inst : Semiring R] →
                    [inst_6 : Semiring S] →
                      [inst_7 : AddCommMonoid M] →
                        [inst_8 : AddCommMonoid M₂] →
                          [inst_9 : Module R M] →
                            [inst_10 : Module R M₂] →
                              [inst_11 : Module S M] →
                                [inst_12 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            h1Cotangentι) :
        TensorProduct.{u_1, u_3, u} R T P.H1Cotangent →ₗ[R] TensorProduct.{u_1, u_3, u} R T P.Cotangent) :
    (a : T ⊗[R] P.H1Cotangent) → T ⊗[R] P.Cotangent)
Tactic: simp only [LinearMap.exact_zero_iff_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
⊢ Function.Injective (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) (β :=
    TensorProduct.{u_1, u_3, u} R T P.Cotangent)
    (⇑(LinearMap.lTensor T
            ((↑R :
                {S : Type u_2} →
                  {M M₂ : Type u} →
                    [inst : Semiring R] →
                      [inst_6 : Semiring S] →
                        [inst_7 : AddCommMonoid M] →
                          [inst_8 : AddCommMonoid M₂] →
                            [inst_9 : Module R M] →
                              [inst_10 : Module R M₂] →
                                [inst_11 : Module S M] →
                                  [inst_12 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              h1Cotangentι) :
          TensorProduct.{u_1, u_3, u} R T P.H1Cotangent →ₗ[R] TensorProduct.{u_1, u_3, u} R T P.Cotangent) :
      (a : T ⊗[R] P.H1Cotangent) → T ⊗[R] P.Cotangent)
have hf₂ : Function.Injective.{u + 1, u + 1} (α := P.H1Cotangent) (β := P.Cotangent)
  (⇑((↑R :
          {S : Type u_2} →
            {M M₂ : Type u} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        h1Cotangentι) :
    (a : P.H1Cotangent) → P.Cotangent)
Tactic: apply Module.Flat.lTensor_preserves_injective_linearMap
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
⊢ 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)
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
⊢ 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)
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
⊢ 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)
have 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)
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
⊢ Function.Exact (M := Unit) (N := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) (P :=
    Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) (⇑0 : (a : Unit) → P.baseChange.H1Cotangent)
    (⇑((↑R :
            {S : Type (max u_2 u_3)} →
              {M M₂ : Type (max u u_3)} →
                [inst : Semiring R] →
                  [inst_6 : Semiring S] →
                    [inst_7 : AddCommMonoid M] →
                      [inst_8 : AddCommMonoid M₂] →
                        [inst_9 : Module R M] →
                          [inst_10 : Module R M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          h1Cotangentι) :
      (a : P.baseChange.H1Cotangent) → P.baseChange.Cotangent)
have hg₂ : Function.Injective (α := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) (β :=
  Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
  (⇑((↑R :
          {S : Type (max u_2 u_3)} →
            {M M₂ : Type (max u u_3)} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        h1Cotangentι) :
    (a : P.baseChange.H1Cotangent) → P.baseChange.Cotangent)
Tactic: rw [LinearMap.exact_zero_iff_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
⊢ Function.Surjective (α := Unit) (β := Unit) (⇑0 : (a : Unit) → Unit)
have hi₁ : ∀ (b : Unit), ∃ (a : Unit), (0 : (a : Unit) → Unit) a = b
Tactic: tauto