awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
set :
  let f := (↑P.cotangentSpaceBasis.repr : P.toExtension.CotangentSpace →ₗ[S] ι →₀ S) ∘ₗ P.toExtension.cotangentComplex;
  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)
⊢ 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)

Tactic:
set f : _ →ₗ[S] (ι →₀ S) := P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex

Premises used: Algebra.Extension.cotangentComplex, Algebra.Generators.cotangentSpaceBasis, Module.Basis.repr, Algebra.Generators.toExtension, Finsupp
-- 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)
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)
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])
⊢ Function.Exact (M := P.toExtension.Cotangent) (N := ι →₀ S) (P := Ω[S⁄R])
    (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S) (⇑g : (a : ι →₀ S) → Ω[S⁄R])

Tactic:
simp only [f, g, LinearEquiv.conj_exact_iff_exact]

Premises used: LinearEquiv.conj_exact_iff_exact
-- 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)
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 := 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:
Extension.exact_cotangentComplex_toKaehler

Premises used: Algebra.Extension.exact_cotangentComplex_toKaehler
-- 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)
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 := 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:
exact Extension.exact_cotangentComplex_toKaehler

Premises used: Algebra.Extension.exact_cotangentComplex_toKaehler
-- 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)
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])

Tactic:
have hfg : Function.Exact f g := by
    simp only [f, g, LinearEquiv.conj_exact_iff_exact]
    exact Extension.exact_cotangentComplex_toKaehler
-- 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)
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])
hf : Function.Injective (α := P.toExtension.Cotangent) (β := ι →₀ S) (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S)
hker : Disjoint g.ker (Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1))
hmap : Submodule.map g (Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1)) = ⊤
⊢ 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)

Tactic:
apply LinearMap.linearProjOfIsCompl_comp_bijective_of_exact hfg

Premises used: LinearMap.linearProjOfIsCompl_comp_bijective_of_exact
-- 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)
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.Injective (α := P.toExtension.Cotangent) (β := ι →₀ S) (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S)

Tactic:
P.cotangentSpaceBasis.repr.injective.comp <|
      (Extension.subsingleton_h1Cotangent P.toExtension).mp P.equivH1Cotangent.subsingleton

Premises used: Algebra.Extension.subsingleton_h1Cotangent, Finsupp.equivMapDomain, LinearEquiv.toAddEquiv, Algebra.Generators.cotangentSpaceBasis, Module.Basis.repr, Function.Injective.comp, Algebra.Generators.equivH1Cotangent, Iff.mp, Algebra.Generators.toExtension, AddEquiv.toEquiv, LinearEquiv.injective, Equiv.subsingleton
-- 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)
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.Injective (α := P.toExtension.Cotangent) (β := ι →₀ S) (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S)

Tactic:
exact P.cotangentSpaceBasis.repr.injective.comp <|
      (Extension.subsingleton_h1Cotangent P.toExtension).mp P.equivH1Cotangent.subsingleton

Premises used: Algebra.Extension.subsingleton_h1Cotangent, LinearEquiv.toAddEquiv, Algebra.Generators.cotangentSpaceBasis, Module.Basis.repr, Function.Injective.comp, Algebra.Generators.equivH1Cotangent, Iff.mp, Algebra.Generators.toExtension, AddEquiv.toEquiv, LinearEquiv.injective, Equiv.subsingleton
-- 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)
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])
hker :
  (P.toExtension.toKaehler ∘ₗ (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)).ker ⊓
      Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1) =
    ⊥
⊢ Disjoint g.ker (Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1))

Tactic:
simp only [disjoint_iff, g]

Premises used: disjoint_iff
-- 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)
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])
hker :
  Submodule.map (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)
      ((P.toExtension.toKaehler ∘ₗ
            (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)).ker ⊓
        Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1)) =
    Submodule.map (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) ⊥
⊢ (P.toExtension.toKaehler ∘ₗ (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)).ker ⊓
      Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1) =
    ⊥

Tactic:
apply Submodule.map_injective_of_injective (f := P.cotangentSpaceBasis.repr.symm.toLinearMap)
      P.cotangentSpaceBasis.repr.symm.injective

Premises used: LinearEquiv.symm, Algebra.Generators.cotangentSpaceBasis, Module.Basis.repr, LinearEquiv.injective, Submodule.map_injective_of_injective
-- 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)
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])
hker :
  P.toExtension.toKaehler.ker ⊓
      Submodule.span S
        (Set.range fun (x : κ) ↦
          ((↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) :
              (a : ι →₀ S) → P.toExtension.CotangentSpace)
            (Finsupp.single (v x) 1)) =
    Submodule.map (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) ⊥
hker₁ :
  Function.Surjective (α := ι →₀ S) (β := P.toExtension.CotangentSpace)
    (⇑(↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) :
      (a : ι →₀ S) → P.toExtension.CotangentSpace)
⊢ Submodule.map (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)
      ((P.toExtension.toKaehler ∘ₗ
            (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)).ker ⊓
        Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1)) =
    Submodule.map (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) ⊥

Tactic:
rw [Submodule.map_inf P.cotangentSpaceBasis.repr.symm.toLinearMap
        P.cotangentSpaceBasis.repr.symm.injective, Submodule.map_span, ← Set.range_comp,
        Function.comp_def, LinearMap.ker_comp, Submodule.map_comap_eq_of_surjective]

Premises used: Set.range_comp, LinearEquiv.symm, LinearMap.ker_comp, Algebra.Generators.cotangentSpaceBasis, Module.Basis.repr, Function.comp_def, LinearEquiv.toLinearMap, Submodule.map_inf, Submodule.map_comap_eq_of_surjective, Submodule.map_span, LinearEquiv.injective
-- 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)
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])
⊢ P.toExtension.toKaehler.ker ⊓
      Submodule.span S
        (Set.range fun (x : κ) ↦
          ((↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) :
              (a : ι →₀ S) → P.toExtension.CotangentSpace)
            (Finsupp.single (v x) 1)) =
    Submodule.map (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) ⊥

Tactic:
simpa [← disjoint_iff]

Premises used: disjoint_iff
-- 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)
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.Surjective (α := ι →₀ S) (β := P.toExtension.CotangentSpace)
    (⇑(↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) :
      (a : ι →₀ S) → P.toExtension.CotangentSpace)

Tactic:
P.cotangentSpaceBasis.repr.symm.surjective

Premises used: LinearEquiv.symm, LinearEquiv.surjective, Algebra.Generators.cotangentSpaceBasis, Module.Basis.repr
-- 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)
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.Surjective (α := ι →₀ S) (β := P.toExtension.CotangentSpace)
    (⇑(↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) :
      (a : ι →₀ S) → P.toExtension.CotangentSpace)

Tactic:
exact P.cotangentSpaceBasis.repr.symm.surjective

Premises used: LinearEquiv.symm, LinearEquiv.surjective, Algebra.Generators.cotangentSpaceBasis, Module.Basis.repr
-- 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)
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])
⊢ Submodule.map g (Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1)) = ⊤

Tactic:
simpa [g, Submodule.map_comp, Submodule.map_span, ← Set.range_comp, Function.comp_def]

Premises used: Set.range_comp, Submodule.map_comp, Function.comp_def, Submodule.map_span