awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
val : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : RingHom.{u_1, u_3} (MvPolynomial (Fin (Fintype.card σ)) R) S :=
  f.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e)))
hf' :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (⇑f' : (a : MvPolynomial (Fin (Fintype.card σ)) R) → S)
this : IsMaximal (ker f')
g : RingHom.{u_1, u_3}
  (HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
    (ker f'))
  S :=
  Ideal.Quotient.lift (ker f') f' ⋯
⊢ (f'.comp C).IsIntegral
have hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
Tactic: have hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f')) = f' :=
      ringHom_ext (fun r => rfl) fun i => rfl
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
val : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : RingHom.{u_1, u_3} (MvPolynomial (Fin (Fintype.card σ)) R) S :=
  f.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e)))
hf' :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (⇑f' : (a : MvPolynomial (Fin (Fintype.card σ)) R) → S)
this : IsMaximal (ker f')
g : RingHom.{u_1, u_3}
  (HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
    (ker f'))
  S :=
  Ideal.Quotient.lift (ker f') f' ⋯
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ (f'.comp C).IsIntegral
have rw : (g.comp (RingHom.comp (Ideal.Quotient.mk (ker f')) C)).IsIntegral
Tactic: rw [← hfg, RingHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
val : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : RingHom.{u_1, u_3} (MvPolynomial (Fin (Fintype.card σ)) R) S :=
  f.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e)))
hf' :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (⇑f' : (a : MvPolynomial (Fin (Fintype.card σ)) R) → S)
this : IsMaximal (ker f')
g : RingHom.{u_1, u_3}
  (HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
    (ker f'))
  S :=
  Ideal.Quotient.lift (ker f') f' ⋯
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ (g.comp (RingHom.comp (Ideal.Quotient.mk (ker f')) C)).IsIntegral
have refine : Function.Surjective.{u_1 + 1, u_3 + 1} (α :=
  HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
    (ker f'))
  (β := S) (⇑g : (a : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f') → S)
Tactic: refine (quotient_mk_comp_C_isIntegral_of_isJacobsonRing (RingHom.ker f')).trans _ g
      (g.isIntegral_of_surjective ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
val : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : RingHom.{u_1, u_3} (MvPolynomial (Fin (Fintype.card σ)) R) S :=
  f.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e)))
hf' :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (⇑f' : (a : MvPolynomial (Fin (Fintype.card σ)) R) → S)
this : IsMaximal (ker f')
g : RingHom.{u_1, u_3}
  (HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
    (ker f'))
  S :=
  Ideal.Quotient.lift (ker f') f' ⋯
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α :=
    HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
      (ker f'))
    (β := S) (⇑g : (a : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f') → S)
have hf'₁ : Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
  (Function.comp (β :=
    HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
      (ker f'))
    (⇑g : (a : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f') → S)
    (⇑(Ideal.Quotient.mk (ker f')) :
      (a : MvPolynomial (Fin (Fintype.card σ)) R) → MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f'))
Tactic: rw [← hfg, coe_comp] at hf'
Cleared hypotheses: hf', hfg
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
val : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : RingHom.{u_1, u_3} (MvPolynomial (Fin (Fintype.card σ)) R) S :=
  f.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e)))
hf' :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (⇑f' : (a : MvPolynomial (Fin (Fintype.card σ)) R) → S)
⊢ (f.comp C).IsIntegral
have this : (f'.comp C).IsIntegral
Tactic: have : (f'.comp C).IsIntegral := by
    have : (RingHom.ker f').IsMaximal := ker_isMaximal_of_surjective f' hf'
    let g : MvPolynomial _ R ⧸ (RingHom.ker f') →+* S :=
      Ideal.Quotient.lift (RingHom.ker f') f' fun _ h => h
    have hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f')) = f' :=
      ringHom_ext (fun r => rfl) fun i => rfl
    rw [← hfg, RingHom.comp_assoc]
    refine (quotient_mk_comp_C_isIntegral_of_isJacobsonRing (RingHom.ker f')).trans _ g
      (g.isIntegral_of_surjective ?_)
    rw [← hfg, coe_comp] at hf'
    exact Function.Surjective.of_comp hf'
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
val : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : RingHom.{u_1, u_3} (MvPolynomial (Fin (Fintype.card σ)) R) S :=
  f.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e)))
hf' :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (⇑f' : (a : MvPolynomial (Fin (Fintype.card σ)) R) → S)
this : (f.comp (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C)).IsIntegral
⊢ (f.comp C).IsIntegral
have h : Eq (α := R →+* MvPolynomial σ R) C (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C)
Tactic: convert! this
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
val : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : RingHom.{u_1, u_3} (MvPolynomial (Fin (Fintype.card σ)) R) S :=
  f.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e)))
hf' :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (⇑f' : (a : MvPolynomial (Fin (Fintype.card σ)) R) → S)
this : (f.comp (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C)).IsIntegral
⊢ Eq (α := R →+* MvPolynomial σ R) C (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C)
have h : ∀ (x : R),
  Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
    ((RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C : (a : R) → MvPolynomial σ R) x :
      MvPolynomial σ R)
Tactic: refine RingHom.ext fun x => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsJacobsonRing A
inst_4 : Algebra.FiniteType A B
⊢ IsJacobsonRing B
have obtain : ∀ (ι : Type u_2) (hι : Fintype ι) (f : MvPolynomial ι A →ₐ[A] B)
  (hf : Function.Surjective (α := MvPolynomial ι A) (β := B) (⇑f : (a : MvPolynomial ι A) → B)), IsJacobsonRing B
Tactic: obtain ⟨ι, hι, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial'.mp ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : Algebra R S
inst_3 : IsJacobsonRing R
inst_4 : Algebra.FiniteType R S
⊢ Module.Finite R S
have obtain : ∀ (ι : Type u_2) (hι : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S)
  (hf : Function.Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)), Module.Finite R S
Tactic: obtain ⟨ι, hι, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial'.mp ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : Algebra R S
inst_3 : IsJacobsonRing R
inst_4 : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
⊢ RingHom.IsIntegral (algebraMap R S)
have rw : RingHom.IsIntegral
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : MvPolynomial ι R →+* S) (algebraMap R (MvPolynomial ι R)))
Tactic: rw [← f.comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : Algebra R S
inst_3 : IsJacobsonRing R
inst_4 : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
⊢ Module.Finite R S
have this : RingHom.IsIntegral (algebraMap R S)
Tactic: have : (algebraMap R S).IsIntegral := by
    rw [← f.comp_algebraMap]
    -- We need to write `f.toRingHom` instead of just `f`, to avoid unification issues.
    exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing f.toRingHom hf
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : Algebra R S
inst_3 : IsJacobsonRing R
inst_4 : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
this : RingHom.IsIntegral (algebraMap R S)
⊢ Module.Finite R S
have this₁ : Algebra.IsIntegral R S
Tactic: have : Algebra.IsIntegral R S := Algebra.isIntegral_def.mpr this
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsJacobsonRing R
inst_2 : Field S
f : R →+* S
h : f.FiniteType
⊢ f.Finite
have algebraizeInst : Algebra.FiniteType R S
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
K : Type u_1
L : Type u_2
A : Type u_3
inst : CommRing K
inst_1 : DivisionRing L
inst_2 : CommRing A
inst_3 : IsJacobsonRing K
inst_4 : IsNoetherianRing K
inst_5 : Nontrivial A
inst_6 : Algebra K L
inst_7 : Algebra K A
inst_8 : Algebra.FiniteType K A
f : L →ₐ[K] A
⊢ Module.Finite K L
have obtain : ∀ (m : Ideal A) (hm : m.IsMaximal), Module.Finite K L
Tactic: obtain ⟨m, hm⟩ := Ideal.exists_maximal A
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
K : Type u_1
L : Type u_2
A : Type u_3
inst : CommRing K
inst_1 : DivisionRing L
inst_2 : CommRing A
inst_3 : IsJacobsonRing K
inst_4 : IsNoetherianRing K
inst_5 : Nontrivial A
inst_6 : Algebra K L
inst_7 : Algebra K A
inst_8 : Algebra.FiniteType K A
f : L →ₐ[K] A
m : Ideal A
hm : m.IsMaximal
this : Field (A ⧸ m) := Quotient.field m
⊢ Module.Finite K L
have this₁ : Module.Finite.{u_1, u_3} K (A ⧸ m)
Tactic: have := finite_of_finite_type_of_isJacobsonRing K (A ⧸ m)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
K : Type u_1
L : Type u_2
A : Type u_3
inst : CommRing K
inst_1 : Field L
inst_2 : CommRing A
inst_3 : IsJacobsonRing K
inst_4 : IsNoetherianRing K
inst_5 : Nontrivial A
f : K →+* L
g : L →+* A
hfg : (g.comp f).FiniteType
⊢ f.Finite
have algebraizeInst : Algebra.FiniteType K A
Tactic: algebraize [f, (g.comp f)]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Semiprimary (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
inst_7 : IsSemisimpleModule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Submodule.comap f (Module.jacobson R₂ M₂) ≤ f.ker
have simp_rw : Submodule.comap f ⊥ ≤ f.ker
Tactic: simp_rw [jacobson_eq_bot, LinearMap.ker, le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Semiprimary (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
inst_7 : IsSemisimpleModule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
simp_rw : Submodule.comap f ⊥ ≤ f.ker
⊢ Submodule.comap f (Module.jacobson R₂ M₂) ≤ f.ker
have simp_rw₁ : Submodule.comap f ⊥ ≤ Submodule.comap f ⊥
Tactic: simp_rw [jacobson_eq_bot, LinearMap.ker, le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Semiprimary (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
r : R
hr : Membership.mem (γ := Submodule R R) (Ring.jacobson R) r
m : M
⊢ r • m = 0
have this : Membership.mem (γ := Submodule R R) (Submodule.comap (LinearMap.toSpanSingleton R M m) (Module.jacobson R M)) r
Tactic: have := Module.le_comap_jacobson (LinearMap.toSpanSingleton R M m) hr
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Semiprimary (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
r : R
hr : Membership.mem (γ := Submodule R R) (Ring.jacobson R) r
m : M
this : Membership.mem (γ := Submodule R R) (Submodule.comap (LinearMap.toSpanSingleton R M m) (Module.jacobson R M)) r
⊢ r • m = 0
have rwa : ∀ (this : Membership.mem (γ := Submodule R R) (Submodule.comap (LinearMap.toSpanSingleton R M m) ⊥) r), r • m = 0
Tactic: rwa [jacobson_eq_bot] 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
D : Derivation R S M
x y : S ⊗[R] S
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (x * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M)
have refine_1 : (D.tensorProductTo : (a : S ⊗[R] S) → M) (0 * y) =
  HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) 0 : M)
Tactic: refine TensorProduct.induction_on 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
D : Derivation R S M
x y : S ⊗[R] S
refine_1 :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (0 * y) =
    HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) 0 : M)
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (x * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M)
have refine_2 : ∀ (x y_1 : S),
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x ⊗ₜ[R] y_1 * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x ⊗ₜ[R] y_1) : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x ⊗ₜ[R] y_1) : M)
Tactic: refine TensorProduct.induction_on 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
D : Derivation R S M
x y : S ⊗[R] S
refine_1 :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (0 * y) =
    HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) 0 : M)
refine_2 :
  ∀ (x y_1 : S),
    (D.tensorProductTo : (a : S ⊗[R] S) → M) (x ⊗ₜ[R] y_1 * y) =
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x ⊗ₜ[R] y_1) : S)
          ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
        HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
          ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x ⊗ₜ[R] y_1) : M)
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (x * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M)
have refine_3 : ∀ (x y_1 : S ⊗[R] S),
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x * y) =
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S)
          ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
        HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
          ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) →
    (D.tensorProductTo : (a : S ⊗[R] S) → M) (y_1 * y) =
        HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y_1 : S)
            ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
          HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
            ((D.tensorProductTo : (a : S ⊗[R] S) → M) y_1 : M) →
      (D.tensorProductTo : (a : S ⊗[R] S) → M) ((x + y_1) * y) =
        HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x + y_1) : S)
            ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
          HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
            ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x + y_1) : M)
Tactic: refine TensorProduct.induction_on 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
D : Derivation R S M
x y : S ⊗[R] S
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (0 * y) =
    HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) 0 : M)
have refine_1 : (D.tensorProductTo : (a : S ⊗[R] S) → M) 0 =
  HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) 0 : M)
Tactic: rw [zero_mul, map_zero, map_zero, zero_smul, smul_zero, add_zero]
-- 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
D : Derivation R S M
x y : S ⊗[R] S
refine_1 :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) 0 =
    HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) 0 : M)
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (0 * y) =
    HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) 0 : M)
have refine_1₁ : 0 =
  HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S) 0
Tactic: rw [zero_mul, map_zero, map_zero, zero_smul, smul_zero, add_zero]