awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
y : S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2
obtain :
  ∀ (y : S ⊗[R] S),
    Eq (α := S)
      ((AlgHom.kerSquareLift (TensorProduct.lmul' R) :
            (a : S ⊗[R] S ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) → S)
          ((Ideal.Quotient.mk (HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) :
                (a : S ⊗[R] S) → S ⊗[R] S ⧸ ideal R S ^ 2)
              y :
            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)
              ((Ideal.Quotient.mk (HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) :
                  (a : S ⊗[R] S) → S ⊗[R] S ⧸ ideal R S ^ 2)
                y) :
            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)
⊢ Eq (α := S)
    ((AlgHom.kerSquareLift (TensorProduct.lmul' R) :
          (a : S ⊗[R] S ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) → S)
        y :
      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)
            y :
          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)

Tactic:
obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
y : S ⊗[R] S
⊢ Eq (α := S)
    ((AlgHom.kerSquareLift (TensorProduct.lmul' R) :
          (a : S ⊗[R] S ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) → S)
        ((Ideal.Quotient.mk (HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) :
              (a : S ⊗[R] S) → S ⊗[R] S ⧸ ideal R S ^ 2)
            y :
          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)
            ((Ideal.Quotient.mk (HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) :
                (a : S ⊗[R] S) → S ⊗[R] S ⧸ ideal R S ^ 2)
              y) :
          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)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
⊢ 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)

Tactic:
have e₁ : (TensorProduct.lmul' R : S ⊗[R] S →ₐ[R] S).kerSquareLift (f x) =
      KaehlerDifferential.quotientCotangentIdealRingEquiv R S
        (Ideal.Quotient.mk (KaehlerDifferential.ideal R S).cotangentIdeal <| f x) := by
    generalize f x = y; obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y; rfl
-- Module: Mathlib.RingTheory.Kaehler.Basic
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)
⊢ 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
-- Module: Mathlib.RingTheory.Kaehler.Basic
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)
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)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Kaehler.Basic
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.FG (R := S ⊗[R] S) (ideal R S)

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

Premises used: HSub.hSub, Algebra.EssFiniteType.finset, TensorProduct.tmul, OfNat.ofNat, Finset.image
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
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))
⊢ 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

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Kaehler.Basic
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 :
  (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))
⊢ 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:
rw [Finset.coe_image, Ideal.span_le]

Premises used: Ideal.span_le, Finset.coe_image
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
left : x ∈ (↑(EssFiniteType.finset R S) : Set S)
⊢ (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x ∈ (↑(ideal R S) : Set (S ⊗[R] S))

Tactic:
KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x

Premises used: Set.Mem, KaehlerDifferential.one_smul_sub_smul_one_mem_ideal
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
left : x ∈ (↑(EssFiniteType.finset R S) : Set S)
⊢ (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x ∈ (↑(ideal R S) : Set (S ⊗[R] S))

Tactic:
exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x

Premises used: KaehlerDifferential.one_smul_sub_smul_one_mem_ideal
-- Module: Mathlib.RingTheory.Kaehler.Basic
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 :
  (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))
⊢ 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:
rw [← KaehlerDifferential.span_range_eq_ideal, Ideal.span_le]

Premises used: Ideal.span_le, KaehlerDifferential.span_range_eq_ideal
-- Module: Mathlib.RingTheory.Kaehler.Basic
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))
h : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] x) (x ⊗ₜ[R] 1) ∈ I
⊢ (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))

Tactic:
change _ - _ ∈ I
-- Module: Mathlib.RingTheory.Kaehler.Basic
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))
⊢ 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⟩
-- Module: Mathlib.RingTheory.Kaehler.Basic
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))
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)
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] x) (x ⊗ₜ[R] 1) ∈ I

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

Premises used: Ideal.Quotient.mk_eq_mk_iff_sub_mem, AlgHom.congr_fun
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
h₃ 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))
⊢ Ideal.FG (R := 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

Premises used: Ideal.span_le, HSub.hSub, Finset.coe_image, Algebra.EssFiniteType.finset, le_antisymm, Ideal.Quotient.mk_eq_mk_iff_sub_mem, KaehlerDifferential.span_range_eq_ideal, TensorProduct.tmul, OfNat.ofNat, Finset.image, rfl
-- Module: Mathlib.RingTheory.Kaehler.Basic
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]

Tactic:
⟨⟨s, top_le_iff.mp ?_⟩⟩

Premises used: Module.Finite.of_fg_top, top_le_iff, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.Kaehler.Basic
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)
refine : LE.le (α := Submodule S Ω[S⁄R]) ⊤ (Submodule.span S (↑s : Set Ω[S⁄R]))
⊢ Module.Finite S Ω[S⁄R]

Tactic:
refine ⟨⟨s, top_le_iff.mp ?_⟩⟩
-- Module: Mathlib.RingTheory.Kaehler.Basic
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)
rw : Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]) ⊆ (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
⊢ LE.le (α := Submodule S Ω[S⁄R]) ⊤ (Submodule.span S (↑s : Set Ω[S⁄R]))

Tactic:
rw [← span_range_derivation, Submodule.span_le]

Premises used: KaehlerDifferential.span_range_derivation, Submodule.span_le
-- Module: Mathlib.RingTheory.Kaehler.Basic
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])

Tactic:
adjoin_induction ?_ ?_ ?_ ?_ hx

Premises used: Algebra.adjoin_induction
-- Module: Mathlib.RingTheory.Kaehler.Basic
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])
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])
refine_4 :
  ∀ (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])
⊢ 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
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
⊢ ∀ (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:
fun x hx ↦ Submodule.subset_span (Finset.mem_image_of_mem _ hx)

Premises used: KaehlerDifferential.D, Submodule.subset_span, Finset.mem_image_of_mem, DFunLike.coe
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
⊢ ∀ (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:
exact fun x hx ↦ Submodule.subset_span (Finset.mem_image_of_mem _ hx)

Premises used: Submodule.subset_span, Finset.mem_image_of_mem