-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.ideal_fg [EssFiniteType R S] :
    (KaehlerDifferential.ideal R S).FG

Proof state:
case h.a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ ideal R S ≤ Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S))

Tactic:
rw [← KaehlerDifferential.span_range_eq_ideal, Ideal.span_le]

Result:
case h.a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ⊆
    ↑(Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S)))

Proof state:
case h.a.intro
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
x : S
I : Ideal (S ⊗[R] S) := Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S))
⊢ 1 ⊗ₜ[R] x - x ⊗ₜ[R] 1 ∈ I

Tactic:
have : (IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeRight =
    (IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeLeft := by
  apply EssFiniteType.algHom_ext
  intro a ha
  simp only [AlgHom.coe_comp, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq,
    Function.comp_apply, TensorProduct.includeLeft_apply, TensorProduct.includeRight_apply,
    Ideal.Quotient.mk_eq_mk_iff_sub_mem]
  refine Ideal.subset_span ?_
  simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe]
  exact ⟨a, ha, rfl⟩

Result:
case h.a.intro
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
x : S
I : Ideal (S ⊗[R] S) := Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S))
this :
  (IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeRight =
    (IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeLeft
⊢ 1 ⊗ₜ[R] x - x ⊗ₜ[R] 1 ∈ I

Proof state:
case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S)) = ideal R S

Tactic:
apply le_antisymm

Result:
case h.a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S)) ≤ ideal R S

case h.a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ ideal R S ≤ Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S))

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ (ideal R S).FG

Tactic:
use (EssFiniteType.finset R S).image (fun s ↦ (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S))

Result:
case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S)) = ideal R S

Proof state:
case H
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
x : S
I : Ideal (S ⊗[R] S) := Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S))
a : S
ha : a ∈ EssFiniteType.finset R S
⊢ 1 ⊗ₜ[R] a - a ⊗ₜ[R] 1 ∈ ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S))

Tactic:
simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe]

Result:
case H
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
x : S
I : Ideal (S ⊗[R] S) := Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S))
a : S
ha : a ∈ EssFiniteType.finset R S
⊢ ∃ x ∈ EssFiniteType.finset R S, 1 ⊗ₜ[R] x - x ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a - a ⊗ₜ[R] 1

Proof state:
case h.a.intro
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
x : S
I : Ideal (S ⊗[R] S) := Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S))
this :
  (IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeRight =
    (IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeLeft
⊢ 1 ⊗ₜ[R] x - x ⊗ₜ[R] 1 ∈ I

Tactic:
simpa [Ideal.Quotient.mk_eq_mk_iff_sub_mem] using AlgHom.congr_fun this x

Result:
no goals