awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Eq (α := (S →₀ S) →ₗ[S] HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
      linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]))
    (Submodule.mkQ (kerTotal R S))
have h : ∀ (a b : S),
  Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
            linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) :
          (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
        (single a b) :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (b𝖣a : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
Tactic: apply Finsupp.lhom_ext
-- 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
a b : S
| b𝖣a
have rw : HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) b
  (1𝖣a : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
Tactic: rw [← Finsupp.smul_single_one a b, map_smul]
-- 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
a b : S
⊢ Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
            linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) :
          (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
        (single a b) :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (b𝖣a : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
have h : (Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) :
      (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
    (single a b) =
  HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) b
    (1𝖣a : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
Tactic: conv_rhs => rw [← Finsupp.smul_single_one a b, map_smul]
-- 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
⊢ Eq (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (kerTotal R S)
have a : LE.le (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
  (kerTotal 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
a :
  LE.le (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (kerTotal R S)
⊢ Eq (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (kerTotal R S)
have a₁ : LE.le (α := Submodule S (S →₀ S)) (kerTotal R S)
  (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
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
| kerTotal R S
have rw : (LinearMap.ker (R₂ := S) (M₂ := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) (τ₁₂ :=
    RingHom.id S) (Submodule.mkQ (kerTotal R S)) :
  Submodule S (S →₀ S))
Tactic: rw [← (KaehlerDifferential.kerTotal R S).ker_mkQ]
-- 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
⊢ LE.le (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (kerTotal R S)
have a : LE.le (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
  (LinearMap.ker (R₂ := S) (M₂ := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) (τ₁₂ :=
    RingHom.id S) (Submodule.mkQ (kerTotal R S)))
Tactic: conv_rhs => rw [← (KaehlerDifferential.kerTotal R S).ker_mkQ]
-- 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
⊢ LE.le (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (LinearMap.ker (R₂ := S) (M₂ := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) (τ₁₂ :=
      RingHom.id S) (Submodule.mkQ (kerTotal R S)))
have a : LE.le (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
  (LinearMap.ker (M₂ := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
      linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
Tactic: rw [← KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination]
-- 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
⊢ LE.le (α := Submodule S (S →₀ S)) (kerTotal R S)
    (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
have a : (((Set.range fun (x : S × S) ↦ HAdd.hAdd (α := S →₀ S) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) ∪
      Set.range fun (x : S × S) ↦ HAdd.hAdd (α := S →₀ S) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) ∪
    Set.range fun (x : R) ↦ single ((algebraMap R S : (a : R) → S) x) 1) ⊆
  (↑(LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]))) : Set (S →₀ S))
Tactic: rw [KaehlerDifferential.kerTotal, 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
⊢ Function.Surjective (α := S →₀ S) (β := Ω[S⁄R])
    (⇑(linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) : (a : S →₀ S) → Ω[S⁄R])
have rw : Eq (α := Submodule S Ω[S⁄R]) (LinearMap.range (M := S →₀ S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]))) ⊤
Tactic: rw [← LinearMap.range_eq_top, range_linearCombination, span_range_derivation]
-- 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
rw : Eq (α := Submodule S Ω[S⁄R]) (LinearMap.range (M := S →₀ S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]))) ⊤
⊢ Function.Surjective (α := S →₀ S) (β := Ω[S⁄R])
    (⇑(linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) : (a : S →₀ S) → Ω[S⁄R])
have rw₁ : Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))) ⊤
Tactic: rw [← LinearMap.range_eq_top, range_linearCombination, span_range_derivation]
-- 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
rw : Eq (α := Submodule S Ω[S⁄R]) (LinearMap.range (M := S →₀ S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]))) ⊤
rw₁ : Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))) ⊤
⊢ Function.Surjective (α := S →₀ S) (β := Ω[S⁄R])
    (⇑(linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) : (a : S →₀ S) → Ω[S⁄R])
have rw₂ : Eq.{v + 1} (α := Submodule S Ω[S⁄R]) ⊤ ⊤
Tactic: rw [← LinearMap.range_eq_top, range_linearCombination, span_range_derivation]
-- 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
x : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)
⊢ (Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S)
      (AddHom.toFun
        (LinearMap.toAddHom (S := S) (σ := RingHom.id S)
          (Submodule.liftQ (kerTotal R S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) ⋯))
        x) =
    x
have obtain : ∀ (x : S →₀ S),
  Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S)
        (AddHom.toFun (M := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
          (LinearMap.toAddHom (S := S) (σ := RingHom.id S)
            (Submodule.liftQ (kerTotal R S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) sorry))
          ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x)) :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
Tactic: obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
Cleared hypotheses: 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
x : Ω[S⁄R]
⊢ AddHom.toFun (M := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      (LinearMap.toAddHom (S := S) (σ := RingHom.id S)
        (Submodule.liftQ (kerTotal R S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) ⋯))
      ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S) x) =
    x
have obtain : ∀ (x : S →₀ S),
  Eq (α := Ω[S⁄R])
    (AddHom.toFun (M := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
        (LinearMap.toAddHom (S := S) (σ := RingHom.id S)
          (Submodule.liftQ (kerTotal R S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) sorry))
        ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S)
          ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x)) :
      Ω[S⁄R])
    ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x : Ω[S⁄R])
Tactic: obtain ⟨x, rfl⟩ := KaehlerDifferential.linearCombination_surjective R S x
Cleared hypotheses: x
-- 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
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
x : S →₀ S
⊢ Eq (α := Ω[S⁄R])
    (AddHom.toFun (M := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
        (LinearMap.toAddHom (S := S) (σ := RingHom.id S)
          (Submodule.liftQ (kerTotal R S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) ⋯))
        ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S)
          ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x)) :
      Ω[S⁄R])
    ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x : Ω[S⁄R])
have this : Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
  ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
          linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) :
        (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
      x :
    HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
  ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x :
    HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
Tactic: have := LinearMap.congr_fun
        (KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination R S) x
-- 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
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
x : S →₀ S
this :
  Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
            linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) :
          (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
        x :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
⊢ Eq (α := Ω[S⁄R])
    (AddHom.toFun (M := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
        (LinearMap.toAddHom (S := S) (σ := RingHom.id S)
          (Submodule.liftQ (kerTotal R S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) ⋯))
        ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S)
          ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x)) :
      Ω[S⁄R])
    ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x : Ω[S⁄R])
have this₁ : Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
  ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S)
      ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x) :
    HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
  ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x :
    HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
Tactic: rw [LinearMap.comp_apply] at this
Cleared hypotheses: this
-- 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
x : S →₀ S
this :
  Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S)
        ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x) :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
⊢ Eq (α := Ω[S⁄R])
    (AddHom.toFun (M := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
        (LinearMap.toAddHom (S := S) (σ := RingHom.id S)
          (Submodule.liftQ (kerTotal R S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) ⋯))
        ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S)
          ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x)) :
      Ω[S⁄R])
    ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x : Ω[S⁄R])
have rw : Eq (α := Ω[S⁄R])
  (AddHom.toFun (M := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      (LinearMap.toAddHom (S := S) (σ := RingHom.id S)
        (Submodule.liftQ (kerTotal R S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) sorry))
      ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x) :
    Ω[S⁄R])
  ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x : Ω[S⁄R])
Tactic: rw [this]
-- 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
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
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Eq (α := Submodule A (B →₀ B))
    (Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (kerTotal R A) ⊔
      Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
    (Submodule.restrictScalars A (kerTotal S B))
have rw : Eq.{u_3 + 1} (α := Submodule A (B →₀ B))
  (Submodule.span A
      (Set.image.{u_2, u_3} (α := A →₀ A)
        (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B)) :
          (a : A →₀ A) → B →₀ B)
        (((Set.range fun (x : A × A) ↦ HAdd.hAdd (α := A →₀ A) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) ∪
            Set.range fun (x : A × A) ↦
              HAdd.hAdd (α := A →₀ A) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) ∪
          Set.range fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)) ⊔
    Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
  (Submodule.span A
    (((Set.range fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) ∪
        Set.range fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) ∪
      Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
Tactic: rw [KaehlerDifferential.kerTotal, Submodule.map_span, KaehlerDifferential.kerTotal,
    Submodule.restrictScalars_span _ _ h]
-- 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
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
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Eq.{u_3 + 1} (α := Submodule A (B →₀ B))
    (Submodule.span A
        (Set.range fun (x : A × A) ↦
          HAdd.hAdd (α := B →₀ B) (β := B →₀ B) (single ((algebraMap A B : (a : A) → B) x.1) 1 : B →₀ B)
              (single ((algebraMap A B : (a : A) → B) x.2) 1 : B →₀ B) -
            single
              (HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) x.1 : B)
                ((algebraMap A B : (a : A) → B) x.2 : B))
              1) ⊔
      (Submodule.span A
          (Set.range fun (x : A × A) ↦
            HAdd.hAdd (α := B →₀ B) (β := B →₀ B)
                (single ((algebraMap A B : (a : A) → B) x.2) ((algebraMap A B : (a : A) → B) x.1) : B →₀ B)
                (single ((algebraMap A B : (a : A) → B) x.1) ((algebraMap A B : (a : A) → B) x.2) : B →₀ B) -
              single
                (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x.1 : B)
                  ((algebraMap A B : (a : A) → B) x.2 : B))
                1) ⊔
        (Submodule.span A
            (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1) ⊔
          Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))))
    (Submodule.span A
        (Set.range.{u_3, u_2 + 1} (ι := A × A)
          ((fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) ∘
            Prod.map (⇑(algebraMap A B) : (a : A) → B) (⇑(algebraMap A B) : (a : A) → B))) ⊔
      (Submodule.span A
          (Set.range.{u_3, u_2 + 1} (ι := A × A)
            ((fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) ∘
              Prod.map (⇑(algebraMap A B) : (a : A) → B) (⇑(algebraMap A B) : (a : A) → B))) ⊔
        Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1)))
have h₁ : Eq.{u_3 + 1} (α := Submodule A (B →₀ B))
  (Submodule.span A
      (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1) ⊔
    Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
  (Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
Tactic: congr!
-- 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
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
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Eq.{u_3 + 1} (α := Submodule A (B →₀ B))
    (Submodule.span A
        (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1) ⊔
      Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
    (Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
have h₁ : LE.le.{u_3} (α := Submodule A (B →₀ B))
  (Submodule.span A
    (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1))
  (Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
Tactic: rw [sup_eq_right]
-- 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
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
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ LE.le.{u_3} (α := Submodule A (B →₀ B))
    (Submodule.span A
      (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1))
    (Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
have h₁ : Subset.{u_3} (α := Set (B →₀ B))
  (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1)
  (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1)
Tactic: apply Submodule.span_mono
-- 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
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
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Subset.{u_3} (α := Set (B →₀ B))
    (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1)
    (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1)
have h₁ : Subset.{u_3} (α := Set (B →₀ B))
  (Set.range fun (x : R) ↦ single ((algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) x : S)) 1)
  (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1)
Tactic: simp_rw [← IsScalarTower.algebraMap_apply R A B, IsScalarTower.algebraMap_apply R S B]