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
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
a b : S
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
h :
  (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
            (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) ((a * b) ⊗ₜ[R] 1)) ⋯) :
        S ⊗[R] S) -
      (↑(a •
              Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
                (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)) ⋯ +
            b •
              Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
                (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
        S ⊗[R] S) =
    HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1) * HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)
⊢ (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
            (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) ((a * b) ⊗ₜ[R] 1)) ⋯) :
        S ⊗[R] S) -
      (↑(a •
              Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
                (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)) ⋯ +
            b •
              Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
                (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
        S ⊗[R] S) ∈
    HMul.hMul (α := Ideal (S ⊗[R] S)) (ideal R S) (ideal R S)

Tactic:
convert!
        Submodule.mul_mem_mul (KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R a :)
          (KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R b :) using 1

Premises used: Submodule.mul_mem_mul, 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
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
a b : S
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
h :
  HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) ((a * b) ⊗ₜ[R] 1) -
      (HSub.hSub (α := S ⊗[R] S) (a ⊗ₜ[R] b) ((a * b) ⊗ₜ[R] 1) +
        HSub.hSub (α := S ⊗[R] S) ((1 * b) ⊗ₜ[R] a) ((a * b) ⊗ₜ[R] 1)) =
    HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) (a ⊗ₜ[R] (1 * b)) -
      HSub.hSub (α := S ⊗[R] S) ((1 * b) ⊗ₜ[R] a) ((a * b) ⊗ₜ[R] 1)
⊢ (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
            (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) ((a * b) ⊗ₜ[R] 1)) ⋯) :
        S ⊗[R] S) -
      (↑(a •
              Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
                (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)) ⋯ +
            b •
              Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
                (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
        S ⊗[R] S) =
    HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1) * HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)

Tactic:
simp only [Submodule.coe_add,
        TensorProduct.tmul_mul_tmul, mul_sub, sub_mul, mul_comm b, Submodule.coe_smul_of_tower,
        smul_sub, TensorProduct.smul_tmul', smul_eq_mul, mul_one]

Premises used: Submodule.coe_add, mul_sub, Algebra.TensorProduct.tmul_mul_tmul, sub_mul, smul_sub, TensorProduct.smul_tmul', Submodule.coe_smul_of_tower, mul_comm, smul_eq_mul, mul_one
-- 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
a b : S
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) ((a * b) ⊗ₜ[R] 1) -
      (HSub.hSub (α := S ⊗[R] S) (a ⊗ₜ[R] b) ((a * b) ⊗ₜ[R] 1) +
        HSub.hSub (α := S ⊗[R] S) ((1 * b) ⊗ₜ[R] a) ((a * b) ⊗ₜ[R] 1)) =
    HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) (a ⊗ₜ[R] (1 * b)) -
      HSub.hSub (α := S ⊗[R] S) ((1 * b) ⊗ₜ[R] a) ((a * b) ⊗ₜ[R] 1)

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
⊢ Eq (α := Ω[S⁄R]) ((D R S : (a : S) → Ω[S⁄R]) s : Ω[S⁄R])
    ((Ideal.toCotangent (ideal R S) : (a : ↥(ideal R S)) → (ideal R S).Cotangent)
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
          (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) ⋯) :
      Ideal.Cotangent (R := S ⊗[R] S) (ideal R S))

Tactic:
rfl

Premises used: Set.Mem, Submodule.Quotient.mk, setOf, Set.preimage, Set.singleton, TensorProduct.tmul, AddCon.toQuotient, 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
rw : LE.le (α := Submodule S Ω[S⁄R]) ⊤ (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
⊢ Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))) ⊤

Tactic:
rw [_root_.eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : Ω[S⁄R]
obtain :
  ∀ (x : S ⊗[R] S) (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx) :
        Ω[S⁄R])
⊢ Membership.mem (γ := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))) x

Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := fromIdeal_surjective R S x

Premises used: KaehlerDifferential.fromIdeal_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
x : S ⊗[R] S
hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x
⊢ Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x

Tactic:
rw [← Submodule.restrictScalars_mem S, ← KaehlerDifferential.submodule_span_range_eq_ideal] at hx

Premises used: KaehlerDifferential.submodule_span_range_eq_ideal, Submodule.restrictScalars_mem
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x
suffices :
  ∃ (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx) :
        Ω[S⁄R])
⊢ Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx_1) :
      Ω[S⁄R])

Tactic:
suffices ∃ hx,
      fromIdeal R S ⟨x, hx⟩ ∈ Submodule.span S (Set.range <| KaehlerDifferential.D R S) from
    this.snd
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x
⊢ ∃ (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx) :
        Ω[S⁄R])

Tactic:
Submodule.span_induction ?_ ?_ ?_ ?_ hx

Premises used: Submodule.span_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
x_1 : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x_1
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x_1
x : S
⊢ ∃ (hx :
    Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S)
      ((fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x)),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
            ((fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x) hx) :
        Ω[S⁄R])

Tactic:
⟨KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x, ?_⟩

Premises used: KaehlerDifferential.one_smul_sub_smul_one_mem_ideal, Exists.intro
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x_1 : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x_1
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x_1
x : S
refine_1 :
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
          ((fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x) ⋯) :
      Ω[S⁄R])
⊢ ∃ (hx :
    Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S)
      ((fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x)),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
            ((fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x) hx) :
        Ω[S⁄R])

Tactic:
refine ⟨KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x, ?_⟩
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x_1 : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x_1
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x_1
x : S
refine_1 :
  Membership.mem (α := Ω[S⁄R]) (γ := Set Ω[S⁄R]) (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
          ((fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x) ⋯) :
      Ω[S⁄R])
⊢ Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
          ((fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x) ⋯) :
      Ω[S⁄R])

Tactic:
apply Submodule.subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x_1 : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x_1
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x_1
x : S
⊢ Membership.mem (α := Ω[S⁄R]) (γ := Set Ω[S⁄R]) (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
          ((fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x) ⋯) :
      Ω[S⁄R])

Tactic:
⟨x, KaehlerDifferential.DLinearMap_apply R S x⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, KaehlerDifferential.DLinearMap_apply
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x_1 : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x_1
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x_1
x : S
⊢ Membership.mem (α := Ω[S⁄R]) (γ := Set Ω[S⁄R]) (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
          ((fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x) ⋯) :
      Ω[S⁄R])

Tactic:
exact ⟨x, KaehlerDifferential.DLinearMap_apply R S x⟩
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x
⊢ ∃ (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) 0),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) 0 hx) :
        Ω[S⁄R])

Tactic:
⟨zero_mem _, Submodule.zero_mem _⟩

Premises used: Submodule.zero_mem, Exists.intro, ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x
⊢ ∃ (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) 0),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) 0 hx) :
        Ω[S⁄R])

Tactic:
exact ⟨zero_mem _, Submodule.zero_mem _⟩
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x_1 : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x_1
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x_1
x y : S ⊗[R] S
hx₁ : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x
hx₂ :
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx₁) :
      Ω[S⁄R])
hy₁ : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) y
hy₂ :
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) y hy₁) :
      Ω[S⁄R])
⊢ ∃ (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) (x + y)),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) (x + y) hx) :
        Ω[S⁄R])

Tactic:
⟨add_mem hx₁ hy₁, Submodule.add_mem _ hx₂ hy₂⟩

Premises used: Exists.intro, AddMemClass.add_mem, Submodule.add_mem
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x_1 : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x_1
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x_1
x y : S ⊗[R] S
hx₁ : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x
hx₂ :
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx₁) :
      Ω[S⁄R])
hy₁ : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) y
hy₂ :
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) y hy₁) :
      Ω[S⁄R])
⊢ ∃ (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) (x + y)),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) (x + y) hx) :
        Ω[S⁄R])

Tactic:
exact ⟨add_mem hx₁ hy₁, Submodule.add_mem _ hx₂ hy₂⟩
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x_1 : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x_1
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x_1
r : S
x : S ⊗[R] S
hx₁ : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x
hx₂ :
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx₁) :
      Ω[S⁄R])
⊢ ∃ (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) (r • x)),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) (r • x) hx) :
        Ω[S⁄R])

Tactic:
⟨((KaehlerDifferential.ideal R S).restrictScalars S).smul_mem r hx₁,
      Submodule.smul_mem _ r hx₂⟩

Premises used: Submodule.restrictScalars, KaehlerDifferential.ideal, Exists.intro, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x_1 : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x_1
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x_1
r : S
x : S ⊗[R] S
hx₁ : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x
hx₂ :
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx₁) :
      Ω[S⁄R])
⊢ ∃ (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) (r • x)),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) (r • x) hx) :
        Ω[S⁄R])

Tactic:
exact ⟨((KaehlerDifferential.ideal R S).restrictScalars S).smul_mem r hx₁,
      Submodule.smul_mem _ r 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
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
suffices : LE.le.{v} (α := Submodule S Ω[S⁄R]) ⊤ ⊥
⊢ Subsingleton.{v + 1} Ω[S⁄R]

Tactic:
suffices (⊤ : Submodule S Ω[S⁄R]) ≤ ⊥ from
    (subsingleton_iff_forall_eq 0).mpr fun y ↦ this trivial
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
rw : Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]) ⊆ (↑⊥ : Set Ω[S⁄R])
⊢ LE.le.{v} (α := Submodule S Ω[S⁄R]) ⊤ ⊥

Tactic:
rw [← KaehlerDifferential.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
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x : S
obtain :
  ∀ (x : R),
    Membership.mem (α := Ω[S⁄R]) (↑⊥ : Set Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) ((algebraMap R S : (a : R) → S) x) : Ω[S⁄R])
⊢ Membership.mem (α := Ω[S⁄R]) (↑⊥ : Set Ω[S⁄R]) ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])

Tactic:
obtain ⟨x, rfl⟩ := h x

Premises used: 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
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x : R
⊢ Membership.mem (α := Ω[S⁄R]) (↑⊥ : Set Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) ((algebraMap R S : (a : R) → S) x) : Ω[S⁄R])

Tactic:
simp