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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
e_p :
  ∀ (x : A →₀ A),
    Membership.mem (γ := Submodule A (A →₀ A))
        (Submodule.comap (M₂ := Ω[A⁄R]) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
          (LinearMap.ker (M₂ := Ω[B⁄S]) (map R S A B)))
        x ↔
      Membership.mem (γ := Submodule A (A →₀ A))
        (Submodule.comap (M₂ := B →₀ B)
          (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
          (Submodule.restrictScalars A (kerTotal S B)))
        x
⊢ Eq (α := Submodule A (A →₀ A))
    (Submodule.comap (M₂ := Ω[A⁄R]) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (LinearMap.ker (M₂ := Ω[B⁄S]) (map R S A B)))
    (Submodule.comap (M₂ := B →₀ B)
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
      (Submodule.restrictScalars A (kerTotal S B)))

Tactic:
ext 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
x : A →₀ A
e_p :
  Eq.{u_3 + 1} (α := Ω[B⁄S])
      ((linearCombination A
              (Function.comp (β := Ω[A⁄R]) (⇑(map R S A B) : (a : Ω[A⁄R]) → Ω[B⁄S]) (⇑(D R A) : (a : A) → Ω[A⁄R])) :
            (a : A →₀ A) → Ω[B⁄S])
          x :
        Ω[B⁄S])
      (0 : Ω[B⁄S]) ↔
    Eq (α := Ω[B⁄S])
      ((linearCombination B (⇑(D S B) : (a : B) → Ω[B⁄S]) : (a : B →₀ B) → Ω[B⁄S])
          (((mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B) :
                LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) (A →₀ A) (B →₀ B)) :
              (a : A →₀ A) → B →₀ B)
            x) :
        Ω[B⁄S])
      (0 : Ω[B⁄S])
⊢ Membership.mem (γ := Submodule A (A →₀ A))
      (Submodule.comap (M₂ := Ω[A⁄R]) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
        (LinearMap.ker (M₂ := Ω[B⁄S]) (map R S A B)))
      x ↔
    Membership.mem (γ := Submodule A (A →₀ A))
      (Submodule.comap (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (Submodule.restrictScalars A (kerTotal S B)))
      x

Tactic:
simp only [Submodule.mem_comap, LinearMap.mem_ker, Finsupp.apply_linearCombination, ← kerTotal_eq,
    Submodule.restrictScalars_mem]

Premises used: KaehlerDifferential.kerTotal_eq, Submodule.mem_comap, LinearMap.mem_ker, Finsupp.apply_linearCombination, 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
x : A →₀ A
e_p :
  Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (i a : A) ↦
        HSMul.hSMul (β := Ω[B⁄S]) a
          (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
              ((D R A : (a : A) → Ω[A⁄R]) i) :
            Ω[B⁄S]))
      0 ↔
    Eq (α := Ω[B⁄S])
      (sum (mapRange (⇑(Algebra.linearMap A B) : (a : A) → B) ⋯ (mapDomain (⇑(algebraMap A B) : (a : A) → B) x))
        fun (i a : B) ↦ HSMul.hSMul (β := Ω[B⁄S]) a ((D S B : (a : B) → Ω[B⁄S]) i : Ω[B⁄S]))
      0
⊢ Eq.{u_3 + 1} (α := Ω[B⁄S])
      ((linearCombination A
              (Function.comp (β := Ω[A⁄R]) (⇑(map R S A B) : (a : Ω[A⁄R]) → Ω[B⁄S]) (⇑(D R A) : (a : A) → Ω[A⁄R])) :
            (a : A →₀ A) → Ω[B⁄S])
          x :
        Ω[B⁄S])
      (0 : Ω[B⁄S]) ↔
    Eq (α := Ω[B⁄S])
      ((linearCombination B (⇑(D S B) : (a : B) → Ω[B⁄S]) : (a : B →₀ B) → Ω[B⁄S])
          (((mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B) :
                LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) (A →₀ A) (B →₀ B)) :
              (a : A →₀ A) → B →₀ B)
            x) :
        Ω[B⁄S])
      (0 : Ω[B⁄S])

Tactic:
simp only [linearCombination_apply, Function.comp_apply, LinearMap.coe_comp, lmapDomain_apply,
    Finsupp.mapRange.linearMap_apply]

Premises used: Finsupp.mapRange.linearMap_apply, Finsupp.linearCombination_apply, LinearMap.coe_comp, Function.comp_apply, Finsupp.lmapDomain_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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
x : A →₀ A
e_p :
  Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (i a : A) ↦
        HSMul.hSMul (β := Ω[B⁄S]) a
          (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
              ((D R A : (a : A) → Ω[A⁄R]) i) :
            Ω[B⁄S]))
      0 ↔
    Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (a m : A) ↦
        HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) m : B)
          ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a) : Ω[B⁄S]))
      0
e_p₁ :
  ∀ (b : B),
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) 0 : B)
        ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S]) =
      0
e_p₂ :
  ∀ (b : B) (m₁ m₂ : A),
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) (m₁ + m₂) : B)
        ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S]) =
      HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) m₁ : B)
          ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S]) +
        HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) m₂ : B)
          ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S])
e_p₃ : ∀ (a : B), HSMul.hSMul (α := B) (β := Ω[B⁄S]) 0 ((D S B : (a : B) → Ω[B⁄S]) a : Ω[B⁄S]) = 0
⊢ Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (i a : A) ↦
        HSMul.hSMul (β := Ω[B⁄S]) a
          (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
              ((D R A : (a : A) → Ω[A⁄R]) i) :
            Ω[B⁄S]))
      0 ↔
    Eq (α := Ω[B⁄S])
      (sum (mapRange (⇑(Algebra.linearMap A B) : (a : A) → B) ⋯ (mapDomain (⇑(algebraMap A B) : (a : A) → B) x))
        fun (i a : B) ↦ HSMul.hSMul (β := Ω[B⁄S]) a ((D S B : (a : B) → Ω[B⁄S]) i : Ω[B⁄S]))
      0

Tactic:
rw [Finsupp.sum_mapRange_index, Finsupp.sum_mapDomain_index]

Premises used: Finsupp.sum_mapDomain_index, Finsupp.sum_mapRange_index
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
x : A →₀ A
⊢ Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (i a : A) ↦
        HSMul.hSMul (β := Ω[B⁄S]) a
          (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
              ((D R A : (a : A) → Ω[A⁄R]) i) :
            Ω[B⁄S]))
      0 ↔
    Eq.{u_3 + 1} (α := Ω[B⁄S])
      (x.sum fun (a m : A) ↦
        HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) m : B)
          ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a) : Ω[B⁄S]))
      0

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
x : A →₀ A
⊢ ∀ (b : B),
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) 0 : B)
        ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S]) =
      0

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
x : A →₀ A
⊢ ∀ (b : B) (m₁ m₂ : A),
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) (m₁ + m₂) : B)
        ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S]) =
      HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) m₁ : B)
          ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S]) +
        HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.linearMap A B : (a : A) → B) m₂ : B)
          ((D S B : (a : B) → Ω[B⁄S]) b : Ω[B⁄S])

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
x : A →₀ A
⊢ ∀ (a : B), HSMul.hSMul (α := B) (β := Ω[B⁄S]) 0 ((D S B : (a : B) → Ω[B⁄S]) a : Ω[B⁄S]) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
rw :
  Eq (α := Submodule A Ω[A⁄R])
    (Submodule.span A
        (Set.range.{u_2, u + 1} (ι := R)
          (Function.comp (β := A →₀ A) (⇑(linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R])) : (a : A →₀ A) → Ω[A⁄R])
            fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)) ⊔
      Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
        (LinearMap.ker (M₂ := B →₀ B)
          (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))))
    (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (LinearMap.ker (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))))
⊢ Eq (α := Submodule A Ω[A⁄R]) (LinearMap.ker (M₂ := Ω[B⁄R]) (map R R A B))
    (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (LinearMap.ker (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))))

Tactic:
rw [ker_map, ← kerTotal_map' R A B h, Submodule.comap_map_eq, Submodule.map_sup,
    Submodule.map_sup, ← kerTotal_eq, ← Submodule.comap_bot,
    Submodule.map_comap_eq_of_surjective (linearCombination_surjective _ _),
    bot_sup_eq, Submodule.map_span, ← Set.range_comp]

Premises used: Set.range_comp, KaehlerDifferential.kerTotal_eq, Submodule.map_sup, bot_sup_eq, KaehlerDifferential.ker_map, Submodule.map_comap_eq_of_surjective, Submodule.map_span, Submodule.comap_bot, KaehlerDifferential.kerTotal_map', KaehlerDifferential.linearCombination_surjective, Submodule.comap_map_eq
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Eq (α := Submodule A Ω[A⁄R])
    (⊥ ⊔
      Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
        (LinearMap.ker (M₂ := B →₀ B)
          (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))))
    (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (LinearMap.ker (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))))

Tactic:
bot_sup_eq _

Premises used: bot_sup_eq
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h₁ :
  Eq (α := Submodule A Ω[A⁄R])
    (Submodule.span A
      (Set.range.{u_2, u + 1} (ι := R)
        (Function.comp (β := A →₀ A) (⇑(linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R])) : (a : A →₀ A) → Ω[A⁄R])
          fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)))
    ⊥
convert_3 : OrderBot (Submodule A Ω[A⁄R])
⊢ Eq (α := Submodule A Ω[A⁄R])
    (Submodule.span A
        (Set.range.{u_2, u + 1} (ι := R)
          (Function.comp (β := A →₀ A) (⇑(linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R])) : (a : A →₀ A) → Ω[A⁄R])
            fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)) ⊔
      Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
        (LinearMap.ker (M₂ := B →₀ B)
          (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))))
    (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (LinearMap.ker (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))))

Tactic:
convert! bot_sup_eq _

Premises used: bot_sup_eq
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ ∀ (x : Ω[A⁄R]),
    Membership.mem (γ := Set Ω[A⁄R])
        (Set.range.{u_2, u + 1} (ι := R)
          (Function.comp (β := A →₀ A) (⇑(linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R])) : (a : A →₀ A) → Ω[A⁄R])
            fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1))
        x →
      x = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
rw : Set.range (ι := B) (⇑(D S B) : (a : B) → Ω[B⁄S]) ⊆ (↑(LinearMap.range (M := Ω[A⁄R]) (map R S A B)) : Set Ω[B⁄S])
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := Ω[A⁄R]) (β := Ω[B⁄S]) (⇑(map R S A B) : (a : Ω[A⁄R]) → Ω[B⁄S])

Tactic:
rw [← LinearMap.range_eq_top, _root_.eq_top_iff,
    ← @Submodule.restrictScalars_top A B, ← span_range_derivation,
    Submodule.restrictScalars_span _ _ h, Submodule.span_le]

Premises used: eq_top_iff, Submodule.restrictScalars_top, KaehlerDifferential.span_range_derivation, LinearMap.range_eq_top, Submodule.span_le, Submodule.restrictScalars_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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
x : B
obtain :
  ∀ (y : A),
    Membership.mem (α := Ω[B⁄S]) (↑(LinearMap.range (M := Ω[A⁄R]) (map R S A B)) : Set Ω[B⁄S])
      ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) y) : Ω[B⁄S])
⊢ Membership.mem (α := Ω[B⁄S]) (↑(LinearMap.range (M := Ω[A⁄R]) (map R S A B)) : Set Ω[B⁄S])
    ((D S B : (a : B) → Ω[B⁄S]) x : Ω[B⁄S])

Tactic:
obtain ⟨y, 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
y : A
rw :
  Membership.mem (α := Ω[B⁄S]) (↑(LinearMap.range (M := Ω[A⁄R]) (map R S A B)) : Set Ω[B⁄S])
    (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
        ((D R A : (a : A) → Ω[A⁄R]) y) :
      Ω[B⁄S])
⊢ Membership.mem (α := Ω[B⁄S]) (↑(LinearMap.range (M := Ω[A⁄R]) (map R S A B)) : Set Ω[B⁄S])
    ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) y) : Ω[B⁄S])

Tactic:
rw [← KaehlerDifferential.map_D R S A B]

Premises used: KaehlerDifferential.map_D
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
y : A
⊢ Membership.mem (α := Ω[B⁄S]) (↑(LinearMap.range (M := Ω[A⁄R]) (map R S A B)) : Set Ω[B⁄S])
    (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
        ((D R A : (a : A) → Ω[A⁄R]) y) :
      Ω[B⁄S])

Tactic:
⟨_, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
y : A
⊢ Membership.mem (α := Ω[B⁄S]) (↑(LinearMap.range (M := Ω[A⁄R]) (map R S A B)) : Set Ω[B⁄S])
    (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
        ((D R A : (a : A) → Ω[A⁄R]) y) :
      Ω[B⁄S])

Tactic:
exact ⟨_, 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
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra S B
inst_5 : Algebra R B
inst_6 : IsScalarTower R S B
⊢ Function.Surjective (α := Ω[B⁄R]) (β := Ω[B⁄S]) (⇑(map R S B B) : (a : Ω[B⁄R]) → Ω[B⁄S])

Tactic:
map_surjective_of_surjective R S B B Function.surjective_id

Premises used: KaehlerDifferential.map_surjective_of_surjective, Function.surjective_id
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : B
y : Ω[A⁄R]
rw : HSMul.hSMul (β := Ω[B⁄R]) x ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (1 ⊗ₜ[A] y) : Ω[B⁄R])
| (mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (x ⊗ₜ[A] y)

Tactic:
rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul', map_smul]

Premises used: TensorProduct.smul_tmul', smul_eq_mul, mul_one, map_smul
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : B
y : Ω[A⁄R]
e_a :
  Eq.{u_3 + 1} (α := Ω[B⁄R]) ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (1 ⊗ₜ[A] y) : Ω[B⁄R])
    (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R]) y : Ω[B⁄R])
⊢ HSMul.hSMul (β := Ω[B⁄R]) x ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (1 ⊗ₜ[A] y) : Ω[B⁄R]) =
    HSMul.hSMul (β := Ω[B⁄R]) x
      (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R]) y : Ω[B⁄R])

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : B
y : Ω[A⁄R]
⊢ Eq.{u_3 + 1} (α := Ω[B⁄R]) ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (1 ⊗ₜ[A] y) : Ω[B⁄R])
    (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R]) y : Ω[B⁄R])

Tactic:
IsBaseChange.lift_eq _ _ _

Premises used: TensorProduct.tmul, AddCon.toQuotient, IsBaseChange.lift_eq
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : B
y : Ω[A⁄R]
⊢ Eq.{u_3 + 1} (α := Ω[B⁄R]) ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (1 ⊗ₜ[A] y) : Ω[B⁄R])
    (((map R R A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄R]) : (a : Ω[A⁄R]) → Ω[B⁄R]) y : Ω[B⁄R])

Tactic:
exact IsBaseChange.lift_eq _ _ _

Premises used: IsBaseChange.lift_eq
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
a :
  LE.le (α := Submodule B Ω[B⁄R]) (LinearMap.range (M := B ⊗[A] Ω[A⁄R]) (mapBaseChange R A B))
    (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
a₁ :
  LE.le (α := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    (LinearMap.range (M := B ⊗[A] Ω[A⁄R]) (mapBaseChange R A B))
⊢ Eq (α := Submodule B Ω[B⁄R]) (LinearMap.range (M := B ⊗[A] Ω[A⁄R]) (mapBaseChange R A B))
    (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
⊢ Membership.mem (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
r : B
s : Ω[A⁄R]
a :
  ∀ (x : A →₀ A),
    Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
      ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R])
          (r ⊗ₜ[A] (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]) : (a : A →₀ A) → Ω[A⁄R]) x) :
        Ω[B⁄R])
⊢ Membership.mem (α := Ω[B⁄R]) (γ := Submodule B Ω[B⁄R]) (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
    ((mapBaseChange R A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R]) (r ⊗ₜ[A] s) : Ω[B⁄R])

Tactic:
obtain ⟨x, rfl⟩ := linearCombination_surjective _ _ s

Premises used: rfl, KaehlerDifferential.linearCombination_surjective