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

Proof state:
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))
⊢ (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

Tactic:
apply EssFiniteType.algHom_ext

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))
⊢ ∀ s ∈ EssFiniteType.finset R S,
    ((IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeRight) s =
      ((IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeLeft) s

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
⊢ (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) '' ↑(EssFiniteType.finset R S) ⊆ ↑(ideal R S)

Tactic:
rintro _ ⟨x, _, rfl⟩

Result:
case h.a.intro.intro
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
x : S
left✝ : x ∈ ↑(EssFiniteType.finset R S)
⊢ (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x ∈ ↑(ideal 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
⊢ (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x ∈
    ↑(Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S)))

Tactic:
let I : Ideal (S ⊗[R] S) := Ideal.span
  ((EssFiniteType.finset R S).image (fun s ↦ (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)))

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))
⊢ (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x ∈
    ↑(Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset 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 ∈ I

Tactic:
refine Ideal.subset_span ?_

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
⊢ 1 ⊗ₜ[R] a - a ⊗ₜ[R] 1 ∈ ↑(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))
⊢ (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x ∈
    ↑(Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S)))

Tactic:
show _ - _ ∈ I

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))
⊢ 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
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

Tactic:
exact ⟨a, ha, rfl⟩

Result:
no goals

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

Tactic:
exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x

Result:
no goals

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))
⊢ ∀ s ∈ EssFiniteType.finset R S,
    ((IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeRight) s =
      ((IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeLeft) s

Tactic:
intro a ha

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
⊢ ((IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeRight) a =
    ((IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeLeft) a

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
⊢ ((IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeRight) a =
    ((IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeLeft) a

Tactic:
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]

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
⊢ 1 ⊗ₜ[R] a - a ⊗ₜ[R] 1 ∈ I

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
⊢ (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)))

Tactic:
rintro _ ⟨x, 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
⊢ (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x ∈
    ↑(Ideal.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S)))

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.span ↑(Finset.image (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S)) ≤ ideal R S

Tactic:
rw [Finset.coe_image, 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
⊢ (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) '' ↑(EssFiniteType.finset R S) ⊆ ↑(ideal R S)