awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h : Nontrivial S
f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker
hf :
  ∀ (b : P.toExtension.Cotangent),
    (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b
v : (i : σ) → ↥P.ker := fun (i : σ) ↦ f ((b₀ : (a : σ) → P.toExtension.Cotangent) i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ P.ker ≤ J ⊔ P.ker • P.ker
have inr : ⊤ ≤ Submodule.comap (Submodule.subtype P.ker) J ⊔ P.ker • Submodule.comap (Submodule.subtype P.ker) P.ker
Tactic: rw [← Submodule.comap_le_comap_iff_of_le_range (f := P.ker.subtype) (by simp),
    Submodule.comap_subtype_self,
    Submodule.comap_sup_of_injective P.ker.subtype_injective (by simpa using hJ)
    (by simp [Ideal.mul_le_left]),
    Submodule.comap_smul'' P.ker.subtype_injective (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h : Nontrivial S
f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker
hf :
  ∀ (b : P.toExtension.Cotangent),
    (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b
v : (i : σ) → ↥P.ker := fun (i : σ) ↦ f ((b₀ : (a : σ) → P.toExtension.Cotangent) i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ ⊤ ≤ Submodule.comap (Submodule.subtype P.ker) J ⊔ P.ker • Submodule.comap (Submodule.subtype P.ker) P.ker
have inr : ⊤ ≤
  Submodule.comap (Submodule.subtype P.ker)
      (Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))) ⊔
    HSMul.hSMul (β := Submodule P.Ring ↥P.ker) P.ker ⊤
Tactic: simp only [Submodule.comap_subtype_self, J]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h : Nontrivial S
f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker
hf :
  ∀ (b : P.toExtension.Cotangent),
    (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b
v : (i : σ) → ↥P.ker := fun (i : σ) ↦ f ((b₀ : (a : σ) → P.toExtension.Cotangent) i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ ⊤ ≤
    Submodule.comap (Submodule.subtype P.ker)
        (Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))) ⊔
      HSMul.hSMul (β := Submodule P.Ring ↥P.ker) P.ker ⊤
have inr : LE.le (α := Submodule P.Ring ↥P.ker) ⊤ (Submodule.span P.Ring (Set.range v) ⊔ LinearMap.ker Extension.Cotangent.mk)
Tactic: rw [← Submodule.coe_subtype, Ideal.span, Set.range_comp, ← Submodule.map_span,
    Submodule.comap_map_eq_of_injective P.ker.subtype_injective,
    ← Extension.Cotangent.ker_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h : Nontrivial S
f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker
hf :
  ∀ (b : P.toExtension.Cotangent),
    (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b
v : (i : σ) → ↥P.ker := fun (i : σ) ↦ f ((b₀ : (a : σ) → P.toExtension.Cotangent) i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ LE.le (α := Submodule P.Ring ↥P.ker) ⊤
    (Submodule.span P.Ring (Set.range v) ⊔
      LinearMap.ker (R₂ := P.Ring) (M₂ := P.toExtension.Cotangent) (τ₁₂ := RingHom.id P.Ring) Extension.Cotangent.mk)
have inr : LE.le (α := Submodule P.Ring P.toExtension.Cotangent)
  (Submodule.map (R := P.Ring) (M := ↥P.ker) (σ₁₂ := RingHom.id P.Ring) Extension.Cotangent.mk ⊤ :
    Submodule P.Ring P.toExtension.Cotangent)
  (Submodule.restrictScalars P.Ring
      (Submodule.span S
        (Set.range fun (x : σ) ↦
          ((Extension.Cotangent.mk :
                LinearMap (R := P.toExtension.Ring) (RingHom.id P.toExtension.Ring) (↥P.toExtension.ker)
                  P.toExtension.Cotangent) :
              (a : ↥P.ker) → P.toExtension.Cotangent)
            (v x))) :
    Submodule P.Ring P.toExtension.Cotangent)
Tactic: simp only [← LinearMap.map_le_map_iff, Submodule.map_span, ← Set.range_comp,
    Function.comp_def, ← Submodule.restrictScalars_span P.Ring S P.algebraMap_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h : Nontrivial S
f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker
hf :
  ∀ (b : P.toExtension.Cotangent),
    (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b
v : (i : σ) → ↥P.ker := fun (i : σ) ↦ f ((b₀ : (a : σ) → P.toExtension.Cotangent) i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ LE.le (α := Submodule P.Ring P.toExtension.Cotangent)
    (Submodule.map (R := P.Ring) (M := ↥P.ker) (σ₁₂ := RingHom.id P.Ring) Extension.Cotangent.mk ⊤ :
      Submodule P.Ring P.toExtension.Cotangent)
    (Submodule.restrictScalars P.Ring
        (Submodule.span S
          (Set.range fun (x : σ) ↦
            ((Extension.Cotangent.mk :
                  LinearMap (R := P.toExtension.Ring) (RingHom.id P.toExtension.Ring) (↥P.toExtension.ker)
                    P.toExtension.Cotangent) :
                (a : ↥P.ker) → P.toExtension.Cotangent)
              (v x))) :
      Submodule P.Ring P.toExtension.Cotangent)
have inr : Eq (α := Submodule P.Ring P.toExtension.Cotangent)
  (Submodule.restrictScalars P.Ring
    (Submodule.span S
      (Set.range fun (x : σ) ↦
        ((Extension.Cotangent.mk :
              LinearMap (R := P.toExtension.Ring) (RingHom.id P.toExtension.Ring) (↥P.toExtension.ker)
                P.toExtension.Cotangent) :
            (a : ↥P.ker) → P.toExtension.Cotangent)
          (v x))))
  ⊤
Tactic: refine le_trans le_top (top_le_iff.mpr ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h : Nontrivial S
f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker
hf :
  ∀ (b : P.toExtension.Cotangent),
    (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b
v : (i : σ) → ↥P.ker := fun (i : σ) ↦ f ((b₀ : (a : σ) → P.toExtension.Cotangent) i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ Eq (α := Submodule P.Ring P.toExtension.Cotangent)
    (Submodule.restrictScalars P.Ring
      (Submodule.span S
        (Set.range fun (x : σ) ↦
          ((Extension.Cotangent.mk :
                LinearMap (R := P.toExtension.Ring) (RingHom.id P.toExtension.Ring) (↥P.toExtension.ker)
                  P.toExtension.Cotangent) :
              (a : ↥P.ker) → P.toExtension.Cotangent)
            (v x))))
    ⊤
have inr : Eq (α := Submodule S P.toExtension.Cotangent)
  (Submodule.span S
    (Set.range fun (x : σ) ↦
      ((Extension.Cotangent.mk :
            LinearMap (R := P.toExtension.Ring) (RingHom.id P.toExtension.Ring) (↥P.toExtension.ker)
              P.toExtension.Cotangent) :
          (a : ↥P.ker) → P.toExtension.Cotangent)
        (v x)))
  ⊤
Tactic: rw [Submodule.restrictScalars_eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h : Nontrivial S
f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker
hf :
  ∀ (b : P.toExtension.Cotangent),
    (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b
v : (i : σ) → ↥P.ker := fun (i : σ) ↦ f ((b₀ : (a : σ) → P.toExtension.Cotangent) i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ Eq (α := Submodule S P.toExtension.Cotangent)
    (Submodule.span S
      (Set.range fun (x : σ) ↦
        ((Extension.Cotangent.mk :
              LinearMap (R := P.toExtension.Ring) (RingHom.id P.toExtension.Ring) (↥P.toExtension.ker)
                P.toExtension.Cotangent) :
            (a : ↥P.ker) → P.toExtension.Cotangent)
          (v x)))
    ⊤
have h : ∀ (x : σ),
  Eq (α := P.toExtension.Cotangent)
    (((Extension.Cotangent.mk :
            LinearMap (R := P.toExtension.Ring) (RingHom.id P.toExtension.Ring) (↥P.toExtension.ker)
              P.toExtension.Cotangent) :
          (a : ↥P.ker) → P.toExtension.Cotangent)
        (v x) :
      P.toExtension.Cotangent)
    ((b₀ : (a : σ) → P.toExtension.Cotangent) x : P.toExtension.Cotangent)
Tactic: convert! b₀.span_eq
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
inst_5 : Module.Free S P.toExtension.Cotangent
⊢ ∃ (P' : Presentation.{0, u_4, u_1, u_2} R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent))) (b :
    Module.Basis (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) S P'.toExtension.Cotangent),
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)),
        Eq (α := P'.toExtension.Cotangent)
          ((b : (a : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) → P'.toExtension.Cotangent) r :
            P'.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥P'.toExtension.ker) → P'.toExtension.Cotangent)
              (Subtype.mk (p := fun (x : P'.toExtension.Ring) ↦ x ∈ P'.toExtension.ker) (P'.relation r) ⋯) :
            P'.toExtension.Cotangent)
have inl : Subsingleton S →
  ∃ (P' : Presentation.{0, u_4, u_1, u_2} R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent))) (b :
    Module.Basis (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) S P'.toExtension.Cotangent),
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)),
        Eq (α := P'.toExtension.Cotangent)
          ((b : (a : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) → P'.toExtension.Cotangent) r :
            P'.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥P'.toExtension.ker) → P'.toExtension.Cotangent)
              (Subtype.mk (p := fun (x : P'.toExtension.Ring) ↦ x ∈ P'.toExtension.ker) (P'.relation r) sorry) :
            P'.toExtension.Cotangent)
Tactic: cases subsingleton_or_nontrivial S
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
inst_5 : Module.Free S P.toExtension.Cotangent
inl :
  Subsingleton S →
    ∃ (P' : Presentation.{0, u_4, u_1, u_2} R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent))) (b :
      Module.Basis (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) S P'.toExtension.Cotangent),
      P'.val ∘ Sum.inr = P.val ∧
        ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)),
          Eq (α := P'.toExtension.Cotangent)
            ((b : (a : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) → P'.toExtension.Cotangent) r :
              P'.toExtension.Cotangent)
            ((Extension.Cotangent.mk : (a : ↥P'.toExtension.ker) → P'.toExtension.Cotangent)
                (Subtype.mk (p := fun (x : P'.toExtension.Ring) ↦ x ∈ P'.toExtension.ker) (P'.relation r) ⋯) :
              P'.toExtension.Cotangent)
⊢ ∃ (P' : Presentation.{0, u_4, u_1, u_2} R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent))) (b :
    Module.Basis (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) S P'.toExtension.Cotangent),
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)),
        Eq (α := P'.toExtension.Cotangent)
          ((b : (a : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) → P'.toExtension.Cotangent) r :
            P'.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥P'.toExtension.ker) → P'.toExtension.Cotangent)
              (Subtype.mk (p := fun (x : P'.toExtension.Ring) ↦ x ∈ P'.toExtension.ker) (P'.relation r) ⋯) :
            P'.toExtension.Cotangent)
have inr : Nontrivial S →
  ∃ (P' : Presentation.{0, u_4, u_1, u_2} R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent))) (b :
    Module.Basis (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) S P'.toExtension.Cotangent),
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)),
        Eq (α := P'.toExtension.Cotangent)
          ((b : (a : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) → P'.toExtension.Cotangent) r :
            P'.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥P'.toExtension.ker) → P'.toExtension.Cotangent)
              (Subtype.mk (p := fun (x : P'.toExtension.Ring) ↦ x ∈ P'.toExtension.ker) (P'.relation r) sorry) :
            P'.toExtension.Cotangent)
Tactic: cases subsingleton_or_nontrivial S
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
inst_5 : Module.Free S P.toExtension.Cotangent
h : Subsingleton S
P' : Presentation.{0, u_4, u_1, u_2} R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) :=
  let __Generators : Generators.{u_4, u_1, u_2} R S (Unit ⊕ α) := ofSurjective (fun (i : Unit ⊕ α) ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun (x : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) ↦ 1,
    span_range_relation_eq_ker := ⋯ }
⊢ ∃ (P' : Presentation.{0, u_4, u_1, u_2} R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent))) (b :
    Module.Basis (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) S P'.toExtension.Cotangent),
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)),
        Eq (α := P'.toExtension.Cotangent)
          ((b : (a : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) → P'.toExtension.Cotangent) r :
            P'.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥P'.toExtension.ker) → P'.toExtension.Cotangent)
              (Subtype.mk (p := fun (x : P'.toExtension.Ring) ↦ x ∈ P'.toExtension.ker) (P'.relation r) ⋯) :
            P'.toExtension.Cotangent)
have this : Subsingleton P'.toExtension.Cotangent
Tactic: have : Subsingleton P'.toExtension.Cotangent := Module.subsingleton S _
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
inst_5 : Module.Free S P.toExtension.Cotangent
h : Nontrivial S
⊢ ∃ (P' : Presentation.{0, u_4, u_1, u_2} R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent))) (b :
    Module.Basis (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) S P'.toExtension.Cotangent),
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)),
        Eq (α := P'.toExtension.Cotangent)
          ((b : (a : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) → P'.toExtension.Cotangent) r :
            P'.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥P'.toExtension.ker) → P'.toExtension.Cotangent)
              (Subtype.mk (p := fun (x : P'.toExtension.Ring) ↦ x ∈ P'.toExtension.ker) (P'.relation r) ⋯) :
            P'.toExtension.Cotangent)
have this : Module.Finite S P.toExtension.Cotangent
Tactic: have : Module.Finite S P.toExtension.Cotangent :=
    Algebra.Extension.Cotangent.finite P.fg_ker_of_finitePresentation
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm :
  Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v i)))) ⊤
hk :
  Disjoint P.toExtension.toKaehler.ker
    (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))
inst_3 : Subsingleton (H1Cotangent R S)
⊢ Function.Bijective (α := P.toExtension.Cotangent) (β := σ →₀ S)
    (⇑(P.cotangentRestrict hu) : (a : P.toExtension.Cotangent) → σ →₀ S)
have rw : Function.Bijective (α := P.toExtension.Cotangent) (β := σ →₀ S)
  (⇑(LinearMap.linearProjOfIsCompl (E := ι →₀ S) (Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1))
            (F := σ →₀ S) (Finsupp.lmapDomain S S u) sorry sorry ∘ₗ
          (↑P.cotangentSpaceBasis.repr : P.toExtension.CotangentSpace →ₗ[S] ι →₀ S) ∘ₗ P.toExtension.cotangentComplex :
        P.toExtension.Cotangent →ₗ[S] σ →₀ S) :
    (a : P.toExtension.Cotangent) → σ →₀ S)
Tactic: rw [cotangentRestrict, Finsupp.lcomapDomain_eq_linearProjOfIsCompl _ huv.symm]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm :
  Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v i)))) ⊤
hk :
  Disjoint P.toExtension.toKaehler.ker
    (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))
inst_3 : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S :=
  (↑P.cotangentSpaceBasis.repr : P.toExtension.CotangentSpace →ₗ[S] ι →₀ S) ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] :=
  P.toExtension.toKaehler ∘ₗ (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)
⊢ Function.Exact (M := P.toExtension.Cotangent) (N := ι →₀ S) (P := Ω[S⁄R])
    (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S) (⇑g : (a : ι →₀ S) → Ω[S⁄R])
have simp : Function.Exact (M := P.toExtension.Cotangent) (N := P.toExtension.CotangentSpace) (P := Ω[S⁄R])
  (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
  (⇑P.toExtension.toKaehler : (a : P.toExtension.CotangentSpace) → Ω[S⁄R])
Tactic: simp only [f, g, LinearEquiv.conj_exact_iff_exact]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm :
  Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v i)))) ⊤
hk :
  Disjoint P.toExtension.toKaehler.ker
    (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))
inst_3 : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S :=
  (↑P.cotangentSpaceBasis.repr : P.toExtension.CotangentSpace →ₗ[S] ι →₀ S) ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] :=
  P.toExtension.toKaehler ∘ₗ (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)
⊢ Function.Bijective (α := P.toExtension.Cotangent) (β := σ →₀ S)
    (⇑(LinearMap.linearProjOfIsCompl (E := ι →₀ S) (Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1))
              (F := σ →₀ S) (Finsupp.lmapDomain S S u) ⋯ ⋯ ∘ₗ
            f :
          P.toExtension.Cotangent →ₗ[S] σ →₀ S) :
      (a : P.toExtension.Cotangent) → σ →₀ S)
have hfg : Function.Exact (M := P.toExtension.Cotangent) (N := ι →₀ S) (P := Ω[S⁄R]) (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S)
  (⇑g : (a : ι →₀ S) → Ω[S⁄R])
Tactic: have hfg : Function.Exact f g := by
    simp only [f, g, LinearEquiv.conj_exact_iff_exact]
    exact Extension.exact_cotangentComplex_toKaehler
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm :
  Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v i)))) ⊤
hk :
  Disjoint P.toExtension.toKaehler.ker
    (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))
inst_3 : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S :=
  (↑P.cotangentSpaceBasis.repr : P.toExtension.CotangentSpace →ₗ[S] ι →₀ S) ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] :=
  P.toExtension.toKaehler ∘ₗ (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)
hfg :
  Function.Exact (M := P.toExtension.Cotangent) (N := ι →₀ S) (P := Ω[S⁄R])
    (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S) (⇑g : (a : ι →₀ S) → Ω[S⁄R])
⊢ Function.Bijective (α := P.toExtension.Cotangent) (β := σ →₀ S)
    (⇑(LinearMap.linearProjOfIsCompl (E := ι →₀ S) (Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1))
              (F := σ →₀ S) (Finsupp.lmapDomain S S u) ⋯ ⋯ ∘ₗ
            f :
          P.toExtension.Cotangent →ₗ[S] σ →₀ S) :
      (a : P.toExtension.Cotangent) → σ →₀ S)
have hf : Function.Injective (α := P.toExtension.Cotangent) (β := ι →₀ S) (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S)
Tactic: apply LinearMap.linearProjOfIsCompl_comp_bijective_of_exact hfg