awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
rw :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s : S ⊗[R] A)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])
⊢ (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] 1)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])
have rw₁ : (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
  HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s : S ⊗[R] A)
    ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
Tactic: rw [show s ⊗ₜ 1 = algebraMap S (S ⊗ A) s by simp, Algebra.TensorProduct.right_algebraMap_apply,
    algebraMap_smul, ← Derivation.map_smul, smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
rw :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s : S ⊗[R] A)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])
rw₁ :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s : S ⊗[R] A)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
⊢ (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] 1)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])
have rw₂ : (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
  HSMul.hSMul (β := Ω[S ⊗[R] A⁄S]) s ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
Tactic: rw [show s ⊗ₜ 1 = algebraMap S (S ⊗ A) s by simp, Algebra.TensorProduct.right_algebraMap_apply,
    algebraMap_smul, ← Derivation.map_smul, smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
rw :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s : S ⊗[R] A)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])
rw₁ :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s : S ⊗[R] A)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
rw₂ :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (β := Ω[S ⊗[R] A⁄S]) s ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
⊢ (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] 1)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])
have rw₃ : Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
  ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (HSMul.hSMul (β := S ⊗[R] A) s (1 ⊗ₜ[R] a)) : Ω[S ⊗[R] A⁄S])
Tactic: rw [show s ⊗ₜ 1 = algebraMap S (S ⊗ A) s by simp, Algebra.TensorProduct.right_algebraMap_apply,
    algebraMap_smul, ← Derivation.map_smul, smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
rw :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s : S ⊗[R] A)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])
rw₁ :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s : S ⊗[R] A)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
rw₂ :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (β := Ω[S ⊗[R] A⁄S]) s ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
rw₃ :
  Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
    ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (HSMul.hSMul (β := S ⊗[R] A) s (1 ⊗ₜ[R] a)) : Ω[S ⊗[R] A⁄S])
⊢ (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] 1)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])
have rw₄ : Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
  ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (HSMul.hSMul (β := S) s 1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
Tactic: rw [show s ⊗ₜ 1 = algebraMap S (S ⊗ A) s by simp, Algebra.TensorProduct.right_algebraMap_apply,
    algebraMap_smul, ← Derivation.map_smul, smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
rw :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s : S ⊗[R] A)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])
rw₁ :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s : S ⊗[R] A)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
rw₂ :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (β := Ω[S ⊗[R] A⁄S]) s ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
rw₃ :
  Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
    ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (HSMul.hSMul (β := S ⊗[R] A) s (1 ⊗ₜ[R] a)) : Ω[S ⊗[R] A⁄S])
rw₄ :
  Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
    ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (HSMul.hSMul (β := S) s 1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
⊢ (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] 1)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])
have rw₅ : Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
  ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((s * 1) ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
Tactic: rw [show s ⊗ₜ 1 = algebraMap S (S ⊗ A) s by simp, Algebra.TensorProduct.right_algebraMap_apply,
    algebraMap_smul, ← Derivation.map_smul, smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
rw :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s : S ⊗[R] A)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])
rw₁ :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s : S ⊗[R] A)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
rw₂ :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (β := Ω[S ⊗[R] A⁄S]) s ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
rw₃ :
  Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
    ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (HSMul.hSMul (β := S ⊗[R] A) s (1 ⊗ₜ[R] a)) : Ω[S ⊗[R] A⁄S])
rw₄ :
  Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
    ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (HSMul.hSMul (β := S) s 1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
rw₅ :
  Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
    ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((s * 1) ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
⊢ (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] 1)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])
have rw₆ : Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
  ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
Tactic: rw [show s ⊗ₜ 1 = algebraMap S (S ⊗ A) s by simp, Algebra.TensorProduct.right_algebraMap_apply,
    algebraMap_smul, ← Derivation.map_smul, smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
⊢ Eq (α := A ⊗[R] S ⊗[A] Ω[A⁄R])
    ((LinearEquiv.symm (tensorKaehlerEquiv R S A (A ⊗[R] S)) : (a : Ω[A ⊗[R] S⁄S]) → A ⊗[R] S ⊗[A] Ω[A⁄R])
        ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] s)) :
      A ⊗[R] S ⊗[A] Ω[A⁄R])
    ((algebraMap S (A ⊗[R] S) : (a : S) → A ⊗[R] S) s ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a : A ⊗[R] S ⊗[A] Ω[A⁄R])
have apply : Eq (α := Ω[A ⊗[R] S⁄S]) ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] s) : Ω[A ⊗[R] S⁄S])
  ((tensorKaehlerEquiv R S A (A ⊗[R] S) : (a : A ⊗[R] S ⊗[A] Ω[A⁄R]) → Ω[A ⊗[R] S⁄S])
      ((algebraMap S (A ⊗[R] S) : (a : S) → A ⊗[R] S) s ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) :
    Ω[A ⊗[R] S⁄S])
Tactic: apply (tensorKaehlerEquiv R S A _).symm_apply_eq.mpr ?_
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
⊢ Eq (α := Ω[A ⊗[R] S⁄S]) ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] s) : Ω[A ⊗[R] S⁄S])
    ((tensorKaehlerEquiv R S A (A ⊗[R] S) : (a : A ⊗[R] S ⊗[A] Ω[A⁄R]) → Ω[A ⊗[R] S⁄S])
        ((algebraMap S (A ⊗[R] S) : (a : S) → A ⊗[R] S) s ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) :
      Ω[A ⊗[R] S⁄S])
have simp : (D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] s) =
  HSMul.hSMul (α := A ⊗[R] S) (β := Ω[A ⊗[R] S⁄S]) ((algebraMap S (A ⊗[R] S) : (a : S) → A ⊗[R] S) s : A ⊗[R] S)
    ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] 1) : Ω[A ⊗[R] S⁄S])
Tactic: simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    tensorKaehlerEquiv_tmul_D]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
⊢ (D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] s) =
    HSMul.hSMul (α := A ⊗[R] S) (β := Ω[A ⊗[R] S⁄S]) ((algebraMap S (A ⊗[R] S) : (a : S) → A ⊗[R] S) s : A ⊗[R] S)
      ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] 1) : Ω[A ⊗[R] S⁄S])
have rw : Eq (α := Ω[A ⊗[R] S⁄S]) ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] s) : Ω[A ⊗[R] S⁄S])
  ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (HMul.hMul (α := A ⊗[R] S) (1 ⊗ₜ[R] s) (a ⊗ₜ[R] 1)) :
    Ω[A ⊗[R] S⁄S])
Tactic: rw [algebraMap_smul, ← Derivation.map_smul, Algebra.smul_def,
    Algebra.TensorProduct.right_algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : FiniteRingKrullDim R
⊢ Nontrivial R
have rw : Nonempty.{u_1 + 1} (PrimeSpectrum R)
Tactic: rw [← PrimeSpectrum.nonempty_iff_nontrivial]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ KrullDimLE 0 R ↔ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
have simp_rw : (∀ (a : Ideal R) (b : a.IsPrime),
    Ideal.IsMaximal.{u_1} (α := R)
      (PrimeSpectrum.asIdeal
        ((Equiv.symm
              (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
            (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
          (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b)))) ↔
  ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
Tactic: simp_rw [Ring.KrullDimLE, Order.krullDimLE_iff, Nat.cast_zero,
    Order.krullDim_nonpos_iff_forall_isMax,
    (PrimeSpectrum.equivSubtype R).forall_congr_left, Subtype.forall, PrimeSpectrum.isMax_iff]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I.IsPrime → Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I ∨ I.IsMaximal
have simp_rw : (∀ (a : Ideal R) (b : a.IsPrime),
    Membership.mem (γ := Set (Ideal R)) (minimalPrimes R)
        (PrimeSpectrum.asIdeal
          ((Equiv.symm
                (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
              (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
            (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b))) ∨
      Ideal.IsMaximal.{u_1} (α := R)
        (PrimeSpectrum.asIdeal
          ((Equiv.symm
                (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
              (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
            (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b)))) ↔
  ∀ (I : Ideal R), I.IsPrime → Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I ∨ I.IsMaximal
Tactic: simp_rw [Ring.KrullDimLE, Order.krullDimLE_iff, Nat.cast_one,
    Order.krullDim_le_one_iff, (PrimeSpectrum.equivSubtype R).forall_congr_left,
    Subtype.forall, PrimeSpectrum.isMax_iff, PrimeSpectrum.isMin_iff]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Ideal.IsPrime.{u_1} (α := R) ⊥
this : OrderBot (PrimeSpectrum R) := { bot := { asIdeal := ⊥, isPrime := inst_1 }, bot_le := ⋯ }
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
have simp_rw : (∀ (a : Ideal R) (b : a.IsPrime),
    ¬Eq.{u_1 + 1} (α := Ideal R)
          (PrimeSpectrum.asIdeal
            ((Equiv.symm
                  (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
              (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b)))
          (PrimeSpectrum.asIdeal ⊥) →
      Ideal.IsMaximal.{u_1} (α := R)
        (PrimeSpectrum.asIdeal
          ((Equiv.symm
                (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
              (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
            (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b)))) ↔
  ∀ (I : Ideal R) (b : I.IsPrime) (a : ¬I = ⊥), I.IsMaximal
Tactic: simp_rw [Ring.KrullDimLE, Order.krullDimLE_iff, Nat.cast_one,
    Order.krullDim_le_one_iff_forall_isMax, (PrimeSpectrum.equivSubtype R).forall_congr_left,
    Subtype.forall, PrimeSpectrum.isMax_iff, forall_comm (α := _ ≠ ⊥),
    ne_eq, PrimeSpectrum.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
have inl : Subsingleton R → (KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inl : Subsingleton R → (KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal)
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
have inr : Nontrivial R → (KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
⊢ KrullDimLE 1 R
have pos : ∀ (hR : Ideal.IsPrime.{u_1} (α := R) ⊥), KrullDimLE 1 R
Tactic: by_cases hR : (⊥ : Ideal R).IsPrime
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
pos : ∀ (hR : Ideal.IsPrime.{u_1} (α := R) ⊥), KrullDimLE 1 R
⊢ KrullDimLE 1 R
have neg : ∀ (hR : ¬Ideal.IsPrime.{u_1} (α := R) ⊥), KrullDimLE 1 R
Tactic: by_cases hR : (⊥ : Ideal R).IsPrime
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ¬Ideal.IsPrime.{u_1} (α := R) ⊥
⊢ KrullDimLE 1 R
have neg : KrullDimLE 0 R
Tactic: suffices Ring.KrullDimLE 0 R from inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : NoZeroDivisors R
inst_3 : Ring.KrullDimLE 1 R
inst_4 : Algebra R S
P : Ideal S
p : R
hP : P ≠ ⊤
hp : Prime p
⊢ P.LiesOver (A := R) (span {p}) ↔ Membership.mem (α := S) P ((algebraMap R S : (a : R) → S) p : S)
have hP₁ : Ne (α := Ideal R) (under R P) ⊤
Tactic: have hP : P.under R ≠ ⊤ := Ideal.comap_ne_top _ hP
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
⊢ ringKrullDim R = 1 ↔
    ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
have refine_1 : ∀ (h : ringKrullDim R = 1) (h' : IsField R), False
Tactic: refine ⟨fun h ↦ ⟨fun h' ↦ ?_, ?_⟩, fun ⟨hn, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
refine_1 : ∀ (h : ringKrullDim R = 1) (h' : IsField R), False
⊢ ringKrullDim R = 1 ↔
    ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
have refine_2 : ∀ (h : ringKrullDim R = 1) (x : R),
  x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
Tactic: refine ⟨fun h ↦ ⟨fun h' ↦ ?_, ?_⟩, fun ⟨hn, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
refine_1 : ∀ (h : ringKrullDim R = 1) (h' : IsField R), False
refine_2 :
  ∀ (h : ringKrullDim R = 1) (x : R),
    x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
⊢ ringKrullDim R = 1 ↔
    ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
have refine_3 : (¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))) →
  ∀ (hn : ¬IsField R)
    (h : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))),
    ringKrullDim R = 1
Tactic: refine ⟨fun h ↦ ⟨fun h' ↦ ?_, ?_⟩, fun ⟨hn, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
⊢ LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
have refine_2 : LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (sInf {J : Ideal R | Ideal.span {x} ≤ J ∧ J.IsPrime})
Tactic: rw [Ideal.radical_eq_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
⊢ LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (sInf {J : Ideal R | Ideal.span {x} ≤ J ∧ J.IsPrime})
have refine_2 : ∀ (J : Ideal R),
  Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.span {x} ≤ J ∧ J.IsPrime} J →
    ∀ (hJ1 : Ideal.span {x} ≤ J) (hJ2 : J.IsPrime), IsLocalRing.maximalIdeal R ≤ J
Tactic: refine le_sInf (fun J ⟨hJ1, hJ2⟩ ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
J : Ideal R
h_1 : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.span {x} ≤ J ∧ J.IsPrime} J
hJ1 : Ideal.span {x} ≤ J
hJ2 : J.IsPrime
⊢ IsLocalRing.maximalIdeal R ≤ J
have this : J.IsMaximal
Tactic: have : J.IsMaximal :=
      Ring.krullDimLE_one_iff_of_noZeroDivisors.mp (Ring.krullDimLE_iff.mpr (by simp [h]))
        J (fun hJ3 ↦ hx (by simp_all)) hJ2
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h_2 : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
h : ringKrullDim R ≤ 0
⊢ False
have this : Ring.KrullDimLE 0 R
Tactic: have : Ring.KrullDimLE 0 R := Ring.krullDimLE_iff.mpr h