awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2
x : S
e₁ :
  Eq (α := S)
    ((AlgHom.kerSquareLift (TensorProduct.lmul' R) :
          (a : S ⊗[R] S ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) → S)
        ((f : (a : S) → S ⊗[R] S ⧸ ideal R S ^ 2) x :
          S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) :
      S)
    ((quotientCotangentIdealRingEquiv R S : (a : (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) → S)
        ((Ideal.Quotient.mk (Ideal.cotangentIdeal (ideal R S)) :
              (a : S ⊗[R] S ⧸ ideal R S ^ 2) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
            ((f : (a : S) → S ⊗[R] S ⧸ ideal R S ^ 2) x) :
          HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
            Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
            (Ideal.cotangentIdeal (ideal R S))) :
      S)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have e₂ : x =
  (quotientCotangentIdealRingEquiv R S : (a : (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) → S)
    ((IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
              Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
              (Ideal.cotangentIdeal (ideal R S))) :
          (a : S) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
        x :
      HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
        Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2)) (Ideal.cotangentIdeal (ideal R S)))
Tactic: have e₂ :
    x = KaehlerDifferential.quotientCotangentIdealRingEquiv R S (IsScalarTower.toAlgHom R S _ x) :=
    (mul_one x).symm
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2
x : S
e₁ :
  Eq (α := S)
    ((AlgHom.kerSquareLift (TensorProduct.lmul' R) :
          (a : S ⊗[R] S ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) → S)
        ((f : (a : S) → S ⊗[R] S ⧸ ideal R S ^ 2) x :
          S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) :
      S)
    ((quotientCotangentIdealRingEquiv R S : (a : (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) → S)
        ((Ideal.Quotient.mk (Ideal.cotangentIdeal (ideal R S)) :
              (a : S ⊗[R] S ⧸ ideal R S ^ 2) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
            ((f : (a : S) → S ⊗[R] S ⧸ ideal R S ^ 2) x) :
          HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
            Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
            (Ideal.cotangentIdeal (ideal R S))) :
      S)
e₂ :
  x =
    (quotientCotangentIdealRingEquiv R S : (a : (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) → S)
      ((IsScalarTower.toAlgHom R S
              (HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
                Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
                (Ideal.cotangentIdeal (ideal R S))) :
            (a : S) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
          x :
        HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
          Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
          (Ideal.cotangentIdeal (ideal R S)))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2
x : S
e₁ :
  Eq (α := S)
    ((AlgHom.kerSquareLift (TensorProduct.lmul' R) :
          (a : S ⊗[R] S ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) → S)
        ((f : (a : S) → S ⊗[R] S ⧸ ideal R S ^ 2) x :
          S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) :
      S)
    ((quotientCotangentIdealRingEquiv R S : (a : (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) → S)
        ((Ideal.Quotient.mk (Ideal.cotangentIdeal (ideal R S)) :
              (a : S ⊗[R] S ⧸ ideal R S ^ 2) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
            ((f : (a : S) → S ⊗[R] S ⧸ ideal R S ^ 2) x) :
          HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
            Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
            (Ideal.cotangentIdeal (ideal R S))) :
      S)
e₂ :
  x =
    (quotientCotangentIdealRingEquiv R S : (a : (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) → S)
      ((IsScalarTower.toAlgHom R S
              (HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
                Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
                (Ideal.cotangentIdeal (ideal R S))) :
            (a : S) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
          x :
        HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
          Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
          (Ideal.cotangentIdeal (ideal R S)))
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
⊢ Ideal.FG (R := S ⊗[R] S) (ideal R S)
have h : Ideal.span
    (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
      Set (S ⊗[R] S)) =
  ideal R S
Tactic: use (EssFiniteType.finset R S).image (fun s ↦ (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S))
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
⊢ Ideal.span
      (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
        Set (S ⊗[R] S)) =
    ideal R S
have h : Ideal.span
    (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
      Set (S ⊗[R] S)) ≤
  ideal R S
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
h :
  Ideal.span
      (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
        Set (S ⊗[R] S)) ≤
    ideal R S
⊢ Ideal.span
      (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
        Set (S ⊗[R] S)) =
    ideal R S
have h₁ : ideal R S ≤
  Ideal.span
    (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
      Set (S ⊗[R] S))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
⊢ Ideal.span
      (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
        Set (S ⊗[R] S)) ≤
    ideal R S
have h : (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) '' (↑(EssFiniteType.finset R S) : Set S) ⊆
  (↑(ideal R S) : Set (S ⊗[R] S))
Tactic: rw [Finset.coe_image, Ideal.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
⊢ ideal R S ≤
    Ideal.span
      (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
        Set (S ⊗[R] S))
have h : (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) ⊆
  (↑(Ideal.span
        (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
          Set (S ⊗[R] S))) :
    Set (S ⊗[R] S))
Tactic: rw [← KaehlerDifferential.span_range_eq_ideal, Ideal.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
x : S
I : Ideal (S ⊗[R] S) :=
  Ideal.span
    (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
      Set (S ⊗[R] S))
⊢ (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x ∈
    (↑(Ideal.span
          (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))
                (EssFiniteType.finset R S)) :
            Set (S ⊗[R] S))) :
      Set (S ⊗[R] S))
have h : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] x) (x ⊗ₜ[R] 1) ∈ I
Tactic: change _ - _ ∈ I
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
x : S
I : Ideal (S ⊗[R] S) :=
  Ideal.span
    (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
      Set (S ⊗[R] S))
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] x) (x ⊗ₜ[R] 1) ∈ I
have this : Eq.{v + 1} (α := S →ₐ[R] S ⊗[R] S ⧸ I)
  (AlgHom.comp (B := S ⊗[R] S) (IsScalarTower.toAlgHom.{u, v, v} R (S ⊗[R] S) (S ⊗[R] S ⧸ I))
    TensorProduct.includeRight)
  (AlgHom.comp (B := S ⊗[R] S) (IsScalarTower.toAlgHom.{u, v, v} R (S ⊗[R] S) (S ⊗[R] S ⧸ I)) TensorProduct.includeLeft)
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
⊢ Ideal.FG (R := S ⊗[R] S) (ideal R S)
have w : Finset (S ⊗[R] S)
Tactic: classical
  use (EssFiniteType.finset R S).image (fun s ↦ (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S))
  apply le_antisymm
  · rw [Finset.coe_image, Ideal.span_le]
    rintro _ ⟨x, _, rfl⟩
    exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x
  · rw [← KaehlerDifferential.span_range_eq_ideal, Ideal.span_le]
    rintro _ ⟨x, rfl⟩
    let I : Ideal (S ⊗[R] S) := Ideal.span
      ((EssFiniteType.finset R S).image (fun s ↦ (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)))
    change _ - _ ∈ I
    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⟩
    simpa [Ideal.Quotient.mk_eq_mk_iff_sub_mem] using AlgHom.congr_fun this x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
w : Finset (S ⊗[R] S)
⊢ Ideal.FG (R := S ⊗[R] S) (ideal R S)
have h : Ideal.span
    (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
      Set (S ⊗[R] S)) =
  ideal R S
Tactic: classical
  use (EssFiniteType.finset R S).image (fun s ↦ (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S))
  apply le_antisymm
  · rw [Finset.coe_image, Ideal.span_le]
    rintro _ ⟨x, _, rfl⟩
    exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x
  · rw [← KaehlerDifferential.span_range_eq_ideal, Ideal.span_le]
    rintro _ ⟨x, rfl⟩
    let I : Ideal (S ⊗[R] S) := Ideal.span
      ((EssFiniteType.finset R S).image (fun s ↦ (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)))
    change _ - _ ∈ I
    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⟩
    simpa [Ideal.Quotient.mk_eq_mk_iff_sub_mem] using AlgHom.congr_fun this x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
w : Finset (S ⊗[R] S)
h h₁ :
  Ideal.span
      (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
        Set (S ⊗[R] S)) =
    ideal R S
⊢ Ideal.FG (R := S ⊗[R] S) (ideal R S)
have h₂ : Ideal.span
    (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
      Set (S ⊗[R] S)) ≤
  ideal R S
Tactic: classical
  use (EssFiniteType.finset R S).image (fun s ↦ (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S))
  apply le_antisymm
  · rw [Finset.coe_image, Ideal.span_le]
    rintro _ ⟨x, _, rfl⟩
    exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x
  · rw [← KaehlerDifferential.span_range_eq_ideal, Ideal.span_le]
    rintro _ ⟨x, rfl⟩
    let I : Ideal (S ⊗[R] S) := Ideal.span
      ((EssFiniteType.finset R S).image (fun s ↦ (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)))
    change _ - _ ∈ I
    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⟩
    simpa [Ideal.Quotient.mk_eq_mk_iff_sub_mem] using AlgHom.congr_fun this x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
w : Finset (S ⊗[R] S)
h h₁ :
  Ideal.span
      (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
        Set (S ⊗[R] S)) =
    ideal R S
h₂ :
  Ideal.span
      (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
        Set (S ⊗[R] S)) ≤
    ideal R S
⊢ Ideal.FG (R := S ⊗[R] S) (ideal R S)
have h₃ : ideal R S ≤
  Ideal.span
    (↑(Finset.image (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) (EssFiniteType.finset R S)) :
      Set (S ⊗[R] S))
Tactic: classical
  use (EssFiniteType.finset R S).image (fun s ↦ (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S))
  apply le_antisymm
  · rw [Finset.coe_image, Ideal.span_le]
    rintro _ ⟨x, _, rfl⟩
    exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x
  · rw [← KaehlerDifferential.span_range_eq_ideal, Ideal.span_le]
    rintro _ ⟨x, rfl⟩
    let I : Ideal (S ⊗[R] S) := Ideal.span
      ((EssFiniteType.finset R S).image (fun s ↦ (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)))
    change _ - _ ∈ I
    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⟩
    simpa [Ideal.Quotient.mk_eq_mk_iff_sub_mem] using AlgHom.congr_fun this x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
⊢ Module.Finite S Ω[S⁄R]
have refine : LE.le (α := Submodule S Ω[S⁄R]) ⊤ (Submodule.span S (↑s : Set Ω[S⁄R]))
Tactic: refine ⟨⟨s, top_le_iff.mp ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
⊢ LE.le (α := Submodule S Ω[S⁄R]) ⊤ (Submodule.span S (↑s : Set Ω[S⁄R]))
have rw : Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]) ⊆ (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
Tactic: rw [← span_range_derivation, Submodule.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x_1 x : S
hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x
⊢ Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
have refine_1 : ∀ (x : S) (hx : x ∈ (↑(EssFiniteType.finset R S) : Set S)),
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
Tactic: refine adjoin_induction ?_ ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x_1 x : S
hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x
refine_1 :
  ∀ (x : S) (hx : x ∈ (↑(EssFiniteType.finset R S) : Set S)),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
      ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
⊢ Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
have refine_2 : ∀ (r : R),
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    ((D R S : (a : S) → Ω[S⁄R]) ((algebraMap R S : (a : R) → S) r) : Ω[S⁄R])
Tactic: refine adjoin_induction ?_ ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x_1 x : S
hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x
refine_1 :
  ∀ (x : S) (hx : x ∈ (↑(EssFiniteType.finset R S) : Set S)),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
      ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
refine_2 :
  ∀ (r : R),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
      ((D R S : (a : S) → Ω[S⁄R]) ((algebraMap R S : (a : R) → S) r) : Ω[S⁄R])
⊢ Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
have refine_3 : ∀ (x y : S) (hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x)
  (hy : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) y),
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
      ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]) →
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
        ((D R S : (a : S) → Ω[S⁄R]) y : Ω[S⁄R]) →
      Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
        ((D R S : (a : S) → Ω[S⁄R]) (x + y) : Ω[S⁄R])
Tactic: refine adjoin_induction ?_ ?_ ?_ ?_ hx