awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
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)
⊢ 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)

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]

Premises used: LinearMap.map_le_map_iff, Set.range_comp, Algebra.Generators.Ring, Algebra.Generators.algebraMap_surjective, Function.comp_def, Submodule.map_span, Submodule.restrictScalars_span
-- 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
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)

Tactic:
le_trans le_top (top_le_iff.mpr ?_)

Premises used: Iff.mpr, le_top, top_le_iff, le_trans
-- 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
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
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))))
    ⊤
⊢ 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:
refine le_trans le_top (top_le_iff.mpr ?_)

Premises used: Iff.mpr, le_top, top_le_iff, le_trans
-- 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
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
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)))
    ⊤
⊢ 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:
rw [Submodule.restrictScalars_eq_top_iff]

Premises used: Submodule.restrictScalars_eq_top_iff
-- 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
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 (ι := σ) (⇑b₀ : (a : σ) → P.toExtension.Cotangent))) ⊤

Tactic:
b₀.span_eq

Premises used: Module.Basis.span_eq
-- 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
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_1 : 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
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)
⊢ 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:
convert! b₀.span_eq

Premises used: Module.Basis.span_eq
-- 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
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
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:
hf _
-- 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
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
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:
exact hf _
-- 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
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)
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) ⋯) :
              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)

Tactic:
cases subsingleton_or_nontrivial S

Premises used: subsingleton_or_nontrivial
-- 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
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
⊢ Eq (α :=
    Ideal (Generators.Ring.{u_4, u_1, u_2} (R := R) (S := S) (ι := Unit ⊕ α) (ofSurjective (fun (i : Unit ⊕ α) ↦ 0) ⋯)))
    (Ideal.span (Set.range fun (x : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) ↦ 1))
    (ker (ofSurjective (fun (i : Unit ⊕ α) ↦ 0) ⋯))

Tactic:
simpa using (RingHom.ker_eq_top_of_subsingleton _).symm

Premises used: RingHom.ker_eq_top_of_subsingleton, Eq.symm
-- 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
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 := ⋯ }
⊢ Subsingleton P'.toExtension.Cotangent

Tactic:
have : Subsingleton P'.toExtension.Cotangent := Module.subsingleton S _
-- 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
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 := ⋯ }
this : Subsingleton P'.toExtension.Cotangent
⊢ P'.val ∘ Sum.inr = P.val

Tactic:
subsingleton
-- 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
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 := ⋯ }
this : Subsingleton P'.toExtension.Cotangent
⊢ ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)),
    Eq (α := P'.toExtension.Cotangent)
      ((default : (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)

Tactic:
subsingleton
-- 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
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 := ⋯ }
this : Subsingleton 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)

Tactic:
exact ⟨P', default, by subsingleton, by subsingleton⟩
-- 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
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
⊢ Module.Finite S P.toExtension.Cotangent

Tactic:
have : Module.Finite S P.toExtension.Cotangent :=
    Algebra.Extension.Cotangent.finite P.fg_ker_of_finitePresentation
-- 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
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
this : Module.Finite 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)

Tactic:
exists_presentation_of_basis_cotangent _ <| Module.finBasis S P.toExtension.Cotangent

Premises used: Algebra.Generators.exists_presentation_of_basis_cotangent, Module.finBasis, Algebra.Generators.toExtension, Algebra.Extension.Cotangent
-- 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
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
this : Module.Finite 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)

Tactic:
exact exists_presentation_of_basis_cotangent _ <| Module.finBasis S P.toExtension.Cotangent

Premises used: Algebra.Generators.exists_presentation_of_basis_cotangent, Module.finBasis, Algebra.Generators.toExtension, Algebra.Extension.Cotangent
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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)
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) ⋯ ⋯ ∘ₗ
            (↑P.cotangentSpaceBasis.repr : P.toExtension.CotangentSpace →ₗ[S] ι →₀ S) ∘ₗ
              P.toExtension.cotangentComplex :
          P.toExtension.Cotangent →ₗ[S] σ →₀ S) :
      (a : P.toExtension.Cotangent) → σ →₀ S)
⊢ Function.Bijective (α := P.toExtension.Cotangent) (β := σ →₀ S)
    (⇑(P.cotangentRestrict hu) : (a : P.toExtension.Cotangent) → σ →₀ S)

Tactic:
rw [cotangentRestrict, Finsupp.lcomapDomain_eq_linearProjOfIsCompl _ huv.symm]

Premises used: Finsupp.lcomapDomain_eq_linearProjOfIsCompl, Algebra.Generators.cotangentRestrict, IsCompl.symm