awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommRing R
I : Ideal R
inst_2 : CharP.{u_1} (R ⧸ I) p
inst_3 : IsAdicComplete I R
x : Perfection (R ⧸ I) p
this :
  SModEq (R := R) (I ^ HAdd.hAdd (α := ℕ) 0 1) ((teichmuller p I : (a : Perfection (R ⧸ I) p) → R) x)
    (HPow.hPow (α := R)
      (Quotient.out (s := Submodule.quotientRel (R := R) I)
        ((coeff (R ⧸ I) p 0 : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
      (HPow.hPow (β := ℕ) p 0))
⊢ Eq (α := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) ((teichmuller p I : (a : Perfection (R ⧸ I) p) → R) x) : R ⧸ I)
    ((coeff (R ⧸ I) p 0 : (a : Perfection (R ⧸ I) p) → R ⧸ I) x : R ⧸ I)
have this₁ : SModEq (R := R) I ((teichmuller p I : (a : Perfection (R ⧸ I) p) → R) x)
  (HPow.hPow (α := R)
    (Quotient.out (s := Submodule.quotientRel (R := R) I) ((coeff (R ⧸ I) p 0 : (a : Perfection (R ⧸ I) p) → R ⧸ I) x))
    (HPow.hPow (β := ℕ) p 0))
Tactic: simp_rw [zero_add, pow_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
R_1 : Type u_1
inst_1 : CommRing R_1
I_1 : Ideal R_1
inst_2 : CharP.{u_1} (R_1 ⧸ I_1) p_1
inst_3 : IsAdicComplete I_1 R_1
p : ℕ
inst_4 : Fact (Nat.Prime p)
R : Type u_2
inst_5 : CommRing R
I : Ideal R
inst_6 : CharP.{u_2} (R ⧸ I) p
inst_7 : IsAdicComplete I R
⊢ Eq (α := Perfection R p →* R)
    ((MulEquiv.symm (liftMonoidHom p (Perfection R p) R) : (a : Perfection R p →* Perfection R p) → Perfection R p →* R)
        (MonoidHom.comp (N := Perfection (R ⧸ I) p)
          ((liftMonoidHom p (Perfection (R ⧸ I) p) R :
              (a : Perfection (R ⧸ I) p →* R) → Perfection (R ⧸ I) p →* Perfection R p)
            (teichmuller p I))
          (mapMonoidHom p (↑(Ideal.Quotient.mk I) : R →* R ⧸ I))) :
      Perfection R p →* R)
    ((MulEquiv.symm (liftMonoidHom p (Perfection R p) R) : (a : Perfection R p →* Perfection R p) → Perfection R p →* R)
        (MonoidHom.id (Perfection R p)) :
      Perfection R p →* R)
have h : ∀ (x : Perfection R p),
  Eq (α := R)
    ((((MulEquiv.symm (liftMonoidHom p (Perfection R p) R) :
                (a : Perfection R p →* Perfection R p) → Perfection R p →* R)
              (MonoidHom.comp (N := Perfection (R ⧸ I) p)
                ((liftMonoidHom p (Perfection (R ⧸ I) p) R :
                    (a : Perfection (R ⧸ I) p →* R) → Perfection (R ⧸ I) p →* Perfection R p)
                  (teichmuller p I))
                (mapMonoidHom p (↑(Ideal.Quotient.mk I) : R →* R ⧸ I))) :
            Perfection R p →* R) :
          (a : Perfection R p) → R)
        x :
      R)
    ((((MulEquiv.symm (liftMonoidHom p (Perfection R p) R) :
                (a : Perfection R p →* Perfection R p) → Perfection R p →* R)
              (MonoidHom.id (Perfection R p)) :
            Perfection R p →* R) :
          (a : Perfection R p) → R)
        x :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Teichmuller (goal)
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
R_1 : Type u_1
inst_1 : CommRing R_1
I_1 : Ideal R_1
inst_2 : CharP.{u_1} (R_1 ⧸ I_1) p_1
inst_3 : IsAdicComplete I_1 R_1
p : ℕ
inst_4 : Fact (Nat.Prime p)
R : Type u_2
inst_5 : CommRing R
I : Ideal R
inst_6 : CharP.{u_2} (R ⧸ I) p
inst_7 : IsAdicComplete I R
⊢ Eq (α := Perfection (R ⧸ I) p →* R ⧸ I)
    ((MulEquiv.symm (liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)) :
          (a : Perfection (R ⧸ I) p →* Perfection (R ⧸ I) p) → Perfection (R ⧸ I) p →* R ⧸ I)
        (MonoidHom.comp (N := Perfection R p)
          (mapMonoidHom p (↑(Ideal.Quotient.mk I) : R →* R ⧸ I) : Perfection R p →* Perfection (R ⧸ I) p)
          ((liftMonoidHom p (Perfection (R ⧸ I) p) R :
              (a : Perfection (R ⧸ I) p →* R) → Perfection (R ⧸ I) p →* Perfection R p)
            (teichmuller p I))) :
      Perfection (R ⧸ I) p →* R ⧸ I)
    ((MulEquiv.symm (liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)) :
          (a : Perfection (R ⧸ I) p →* Perfection (R ⧸ I) p) → Perfection (R ⧸ I) p →* R ⧸ I)
        (MonoidHom.id (Perfection (R ⧸ I) p)) :
      Perfection (R ⧸ I) p →* R ⧸ I)
have h : ∀ (x : Perfection (R ⧸ I) p),
  Eq (α := R ⧸ I)
    ((((MulEquiv.symm (liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)) :
                (a : Perfection (R ⧸ I) p →* Perfection (R ⧸ I) p) → Perfection (R ⧸ I) p →* R ⧸ I)
              (MonoidHom.comp (N := Perfection R p)
                (mapMonoidHom p (↑(Ideal.Quotient.mk I) : R →* R ⧸ I) : Perfection R p →* Perfection (R ⧸ I) p)
                ((liftMonoidHom p (Perfection (R ⧸ I) p) R :
                    (a : Perfection (R ⧸ I) p →* R) → Perfection (R ⧸ I) p →* Perfection R p)
                  (teichmuller p I))) :
            Perfection (R ⧸ I) p →* R ⧸ I) :
          (a : Perfection (R ⧸ I) p) → R ⧸ I)
        x :
      R ⧸ I)
    ((((MulEquiv.symm (liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)) :
                (a : Perfection (R ⧸ I) p →* Perfection (R ⧸ I) p) → Perfection (R ⧸ I) p →* R ⧸ I)
              (MonoidHom.id (Perfection (R ⧸ I) p)) :
            Perfection (R ⧸ I) p →* R ⧸ I) :
          (a : Perfection (R ⧸ I) p) → R ⧸ I)
        x :
      R ⧸ I)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
P : Type u_1
inst_9 : AddCommMonoid P
inst_10 : Module A P
inst_11 : Module R P
inst_12 : IsScalarTower R A P
l : M →ₗ[R] N
l' : N →ₗ[A] P
⊢ Eq (α := A ⊗[R] M →ₗ[A] P) (l' ∘ₗ liftBaseChange A l)
    (liftBaseChange A
      ((↑R :
            {S : Type u_2} →
              {M : Type u_5} →
                {M₂ : Type u_1} →
                  [inst : Semiring R] →
                    [inst_13 : Semiring S] →
                      [inst_14 : AddCommMonoid M] →
                        [inst_15 : AddCommMonoid M₂] →
                          [inst_16 : Module R M] →
                            [inst_17 : Module R M₂] →
                              [inst_18 : Module S M] →
                                [inst_19 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          l' ∘ₗ
        l))
have a : ∀ (x : M),
  Eq.{u_1 + 1} (α := P)
    ((((AlgebraTensorModule.curry (l' ∘ₗ liftBaseChange A l) : A →ₗ[A] M →ₗ[R] P) : (a : A) → M →ₗ[R] P) 1 :
          (a : M) → P)
        x :
      P)
    ((((AlgebraTensorModule.curry
                  (liftBaseChange A
                    ((↑R :
                          {S : Type u_2} →
                            {M : Type u_5} →
                              {M₂ : Type u_1} →
                                [inst : Semiring R] →
                                  [inst_13 : Semiring S] →
                                    [inst_14 : AddCommMonoid M] →
                                      [inst_15 : AddCommMonoid M₂] →
                                        [inst_16 : Module R M] →
                                          [inst_17 : Module R M₂] →
                                            [inst_18 : Module S M] →
                                              [inst_19 : Module S M₂] →
                                                [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                        l' ∘ₗ
                      l)) :
                A →ₗ[A] M →ₗ[R] P) :
              (a : A) → M →ₗ[R] P)
            1 :
          (a : M) → P)
        x :
      P)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
⊢ Eq (α := Submodule A N) (range (M := A ⊗[R] M) (liftBaseChange A l)) (Submodule.span A (↑l.range : Set N))
have a : LE.le (α := Submodule A N) (range (M := A ⊗[R] M) (liftBaseChange A l)) (Submodule.span A (↑l.range : Set N))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
a : LE.le (α := Submodule A N) (range (M := A ⊗[R] M) (liftBaseChange A l)) (Submodule.span A (↑l.range : Set N))
⊢ Eq (α := Submodule A N) (range (M := A ⊗[R] M) (liftBaseChange A l)) (Submodule.span A (↑l.range : Set N))
have a₁ : LE.le (α := Submodule A N) (Submodule.span A (↑l.range : Set N)) (range (M := A ⊗[R] M) (liftBaseChange A l))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x : A ⊗[R] M
⊢ Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) x : N)
have a : Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
  ((liftBaseChange A l : (a : A ⊗[R] M) → N) 0 : N)
Tactic: induction x using TensorProduct.induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x : A ⊗[R] M
a :
  Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) 0 : N)
⊢ Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) x : N)
have a₁ : ∀ (x : A) (y : M),
  Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) (x ⊗ₜ[R] y) : N)
Tactic: induction x using TensorProduct.induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x : A ⊗[R] M
a :
  Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) 0 : N)
a₁ :
  ∀ (x : A) (y : M),
    Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
      ((liftBaseChange A l : (a : A ⊗[R] M) → N) (x ⊗ₜ[R] y) : N)
⊢ Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) x : N)
have a₂ : ∀ (x y : A ⊗[R] M),
  Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
      ((liftBaseChange A l : (a : A ⊗[R] M) → N) x : N) →
    Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
        ((liftBaseChange A l : (a : A ⊗[R] M) → N) y : N) →
      Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
        ((liftBaseChange A l : (a : A ⊗[R] M) → N) (x + y) : N)
Tactic: induction x using TensorProduct.induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x : A
y : M
⊢ Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) (x ⊗ₜ[R] y) : N)
have a : Membership.mem (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
  (HSMul.hSMul (β := N) x ((l : (a : M) → N) y : N))
Tactic: rw [LinearMap.liftBaseChange_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
x y : A ⊗[R] M
h :
  Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) x : N)
h_1 :
  Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) y : N)
⊢ Membership.mem (α := N) (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) (x + y) : N)
have a : Membership.mem (γ := Submodule A N) (Submodule.span A (↑l.range : Set N))
  (HAdd.hAdd (α := N) (β := N) ((liftBaseChange A l : (a : A ⊗[R] M) → N) x : N)
    ((liftBaseChange A l : (a : A ⊗[R] M) → N) y : N))
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module A N
inst_8 : IsScalarTower R A N
l : M →ₗ[R] N
⊢ LE.le (α := Submodule A N) (Submodule.span A (↑l.range : Set N)) (range (M := A ⊗[R] M) (liftBaseChange A l))
have a : (↑l.range : Set N) ⊆ (↑(range (M := A ⊗[R] M) (liftBaseChange A l)) : Set N)
Tactic: rw [Submodule.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : AddCommMonoidWithOne A
inst_2 : Module R A
inst_3 : AddCommMonoidWithOne B
inst_4 : Module R B
n : ℕ
⊢ Eq (α := A ⊗[R] B) (↑n : A ⊗[R] B) (1 ⊗ₜ[R] (↑n : B))
have rw : Eq (α := A ⊗[R] B) ((↑n : A) ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑n : B))
Tactic: rw [natCast_def, ← nsmul_one, smul_tmul, nsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : AddCommMonoidWithOne A
inst_2 : Module R A
inst_3 : AddCommMonoidWithOne B
inst_4 : Module R B
n : ℕ
rw : Eq (α := A ⊗[R] B) ((↑n : A) ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑n : B))
⊢ Eq (α := A ⊗[R] B) (↑n : A ⊗[R] B) (1 ⊗ₜ[R] (↑n : B))
have rw₁ : Eq (α := A ⊗[R] B) (HSMul.hSMul (β := A) n 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑n : B))
Tactic: rw [natCast_def, ← nsmul_one, smul_tmul, nsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : AddCommMonoidWithOne A
inst_2 : Module R A
inst_3 : AddCommMonoidWithOne B
inst_4 : Module R B
n : ℕ
rw : Eq (α := A ⊗[R] B) ((↑n : A) ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑n : B))
rw₁ : Eq (α := A ⊗[R] B) (HSMul.hSMul (β := A) n 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑n : B))
⊢ Eq (α := A ⊗[R] B) (↑n : A ⊗[R] B) (1 ⊗ₜ[R] (↑n : B))
have rw₂ : Eq (α := A ⊗[R] B) (1 ⊗ₜ[R] HSMul.hSMul (β := B) n 1) (1 ⊗ₜ[R] (↑n : B))
Tactic: rw [natCast_def, ← nsmul_one, smul_tmul, nsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : AddCommMonoidWithOne A
inst_2 : Module R A
inst_3 : AddCommMonoidWithOne B
inst_4 : Module R B
n : ℕ
rw : Eq (α := A ⊗[R] B) ((↑n : A) ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑n : B))
rw₁ : Eq (α := A ⊗[R] B) (HSMul.hSMul (β := A) n 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑n : B))
rw₂ : Eq (α := A ⊗[R] B) (1 ⊗ₜ[R] HSMul.hSMul (β := B) n 1) (1 ⊗ₜ[R] (↑n : B))
⊢ Eq (α := A ⊗[R] B) (↑n : A ⊗[R] B) (1 ⊗ₜ[R] (↑n : B))
have rw₃ : Eq (α := A ⊗[R] B) (1 ⊗ₜ[R] (↑n : B)) (1 ⊗ₜ[R] (↑n : B))
Tactic: rw [natCast_def, ← nsmul_one, smul_tmul, nsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
a : A
b : B
a' : A
b' : B
⊢ HSMul.hSMul (β := A ⊗[R] B) r (a' ⊗ₜ[R] b') * a ⊗ₜ[R] b = r • HMul.hMul (α := A ⊗[R] B) (a' ⊗ₜ[R] b') (a ⊗ₜ[R] b)
have tmul : HSMul.hSMul (β := A ⊗[R] B) r (a' ⊗ₜ[R] b') * a ⊗ₜ[R] b = HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
a : A
b : B
a' : A
b' : B
⊢ HSMul.hSMul (β := A ⊗[R] B) r (a' ⊗ₜ[R] b') * a ⊗ₜ[R] b = HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b))
have tmul : HMul.hMul (α := A ⊗[R] B) ((r • a') ⊗ₜ[R] b') (a ⊗ₜ[R] b) = HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b))
Tactic: rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
a : A
b : B
a' : A
b' : B
tmul :
  HMul.hMul (α := A ⊗[R] B) ((r • a') ⊗ₜ[R] b') (a ⊗ₜ[R] b) = HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b))
⊢ HSMul.hSMul (β := A ⊗[R] B) r (a' ⊗ₜ[R] b') * a ⊗ₜ[R] b = HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b))
have tmul₁ : HMul.hMul (α := A ⊗[R] B) ((r • a') ⊗ₜ[R] b') (a ⊗ₜ[R] b) = (r • (a' * a)) ⊗ₜ[R] (b' * b)
Tactic: rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
a : A
b : B
a' : A
b' : B
tmul :
  HMul.hMul (α := A ⊗[R] B) ((r • a') ⊗ₜ[R] b') (a ⊗ₜ[R] b) = HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b))
tmul₁ : HMul.hMul (α := A ⊗[R] B) ((r • a') ⊗ₜ[R] b') (a ⊗ₜ[R] b) = (r • (a' * a)) ⊗ₜ[R] (b' * b)
⊢ HSMul.hSMul (β := A ⊗[R] B) r (a' ⊗ₜ[R] b') * a ⊗ₜ[R] b = HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b))
have tmul₂ : Eq (α := A ⊗[R] B) ((r • a' * a) ⊗ₜ[R] (b' * b)) ((r • (a' * a)) ⊗ₜ[R] (b' * b))
Tactic: rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
a : A
b : B
a' : A
b' : B
tmul :
  HMul.hMul (α := A ⊗[R] B) ((r • a') ⊗ₜ[R] b') (a ⊗ₜ[R] b) = HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b))
tmul₁ : HMul.hMul (α := A ⊗[R] B) ((r • a') ⊗ₜ[R] b') (a ⊗ₜ[R] b) = (r • (a' * a)) ⊗ₜ[R] (b' * b)
tmul₂ : Eq (α := A ⊗[R] B) ((r • a' * a) ⊗ₜ[R] (b' * b)) ((r • (a' * a)) ⊗ₜ[R] (b' * b))
⊢ HSMul.hSMul (β := A ⊗[R] B) r (a' ⊗ₜ[R] b') * a ⊗ₜ[R] b = HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b))
have tmul₃ : Eq (α := A ⊗[R] B) ((r • (a' * a)) ⊗ₜ[R] (b' * b)) ((r • (a' * a)) ⊗ₜ[R] (b' * b))
Tactic: rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
x : A ⊗[R] B
a : A
b : B
⊢ r • x * a ⊗ₜ[R] b = r • (x * a ⊗ₜ[R] b)
have tmul : HSMul.hSMul (β := A ⊗[R] B) r 0 * a ⊗ₜ[R] b = r • HMul.hMul (α := A ⊗[R] B) 0 (a ⊗ₜ[R] b)
Tactic: induction x with
      | zero => simp [smul_zero]
      | tmul a' b' =>
        dsimp
        rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, smul_mul_assoc]
      | add x y hx hy => simp [smul_add, add_mul _, *]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
x : A ⊗[R] B
a : A
b : B
tmul : HSMul.hSMul (β := A ⊗[R] B) r 0 * a ⊗ₜ[R] b = r • HMul.hMul (α := A ⊗[R] B) 0 (a ⊗ₜ[R] b)
⊢ r • x * a ⊗ₜ[R] b = r • (x * a ⊗ₜ[R] b)
have tmul₁ : ∀ (a' : A) (b' : B),
  HSMul.hSMul (β := A ⊗[R] B) r (a' ⊗ₜ[R] b') * a ⊗ₜ[R] b = r • HMul.hMul (α := A ⊗[R] B) (a' ⊗ₜ[R] b') (a ⊗ₜ[R] b)
Tactic: induction x with
      | zero => simp [smul_zero]
      | tmul a' b' =>
        dsimp
        rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, smul_mul_assoc]
      | add x y hx hy => simp [smul_add, add_mul _, *]
Cleared hypotheses: x