awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb :
  Eq (α := B →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f) includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R g) includeRight)
a : A
b : B
this :
  HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C) ((f : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C) =
    HMul.hMul (α := C) (β := C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C) ((g : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C)
⊢ Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
have a₁ : ∀
  (this :
    (f : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) =
      HMul.hMul (α := C) (β := C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C)
        ((g : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C)),
  Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
Tactic: rwa [← map_mul, ← map_mul, tmul_mul_tmul, one_mul, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb :
  Eq (α := B →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f) includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R g) includeRight)
a : A
b : B
this :
  HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C) ((f : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C) =
    HMul.hMul (α := C) (β := C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C) ((g : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C)
a₁ :
  ∀
    (this :
      (f : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) =
        HMul.hMul (α := C) (β := C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C)
          ((g : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
⊢ Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
have a₂ : ∀
  (this :
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) : C)
      ((g : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) : C)),
  Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
Tactic: rwa [← map_mul, ← map_mul, tmul_mul_tmul, one_mul, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb :
  Eq (α := B →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f) includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R g) includeRight)
a : A
b : B
this :
  HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C) ((f : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C) =
    HMul.hMul (α := C) (β := C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C) ((g : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C)
a₁ :
  ∀
    (this :
      (f : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) =
        HMul.hMul (α := C) (β := C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C)
          ((g : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
a₂ :
  ∀
    (this :
      Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) : C)
        ((g : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
⊢ Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
have a₃ : ∀
  (this :
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) ((a * 1) ⊗ₜ[R] (1 * b)) : C)
      ((g : (a : A ⊗[R] B) → C) ((a * 1) ⊗ₜ[R] (1 * b)) : C)),
  Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
Tactic: rwa [← map_mul, ← map_mul, tmul_mul_tmul, one_mul, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb :
  Eq (α := B →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f) includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R g) includeRight)
a : A
b : B
this :
  HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C) ((f : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C) =
    HMul.hMul (α := C) (β := C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C) ((g : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C)
a₁ :
  ∀
    (this :
      (f : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) =
        HMul.hMul (α := C) (β := C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C)
          ((g : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
a₂ :
  ∀
    (this :
      Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) : C)
        ((g : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
a₃ :
  ∀
    (this :
      Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) ((a * 1) ⊗ₜ[R] (1 * b)) : C)
        ((g : (a : A ⊗[R] B) → C) ((a * 1) ⊗ₜ[R] (1 * b)) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
⊢ Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
have a₄ : ∀
  (this :
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) ((a * 1) ⊗ₜ[R] b) : C)
      ((g : (a : A ⊗[R] B) → C) ((a * 1) ⊗ₜ[R] b) : C)),
  Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
Tactic: rwa [← map_mul, ← map_mul, tmul_mul_tmul, one_mul, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
inst_7 : CommSemiring S
inst_8 : Algebra S A
inst_9 : Algebra R S
inst_10 : Algebra S C
inst_11 : IsScalarTower R S A
inst_12 : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb :
  Eq (α := B →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f) includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R g) includeRight)
a : A
b : B
this :
  HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C) ((f : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C) =
    HMul.hMul (α := C) (β := C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C) ((g : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C)
a₁ :
  ∀
    (this :
      (f : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) =
        HMul.hMul (α := C) (β := C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] 1) : C)
          ((g : (a : A ⊗[R] B) → C) (1 ⊗ₜ[R] b) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
a₂ :
  ∀
    (this :
      Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) : C)
        ((g : (a : A ⊗[R] B) → C) (HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] b)) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
a₃ :
  ∀
    (this :
      Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) ((a * 1) ⊗ₜ[R] (1 * b)) : C)
        ((g : (a : A ⊗[R] B) → C) ((a * 1) ⊗ₜ[R] (1 * b)) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
a₄ :
  ∀
    (this :
      Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) ((a * 1) ⊗ₜ[R] b) : C)
        ((g : (a : A ⊗[R] B) → C) ((a * 1) ⊗ₜ[R] b) : C)),
    Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
⊢ Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
have a₅ : ∀ (this : Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)),
  Eq.{uC + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C) ((g : (a : A ⊗[R] B) → C) (a ⊗ₜ[R] b) : C)
Tactic: rwa [← map_mul, ← map_mul, tmul_mul_tmul, one_mul, mul_one] at this
Cleared hypotheses: this
-- 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 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
C : Type u_3
inst_5 : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp (AlgHom.toRingHom includeRight) = g.comp (AlgHom.toRingHom includeRight)
⊢ f = g
have a : ∀ (x : A ⊗[R] B), Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) x : C) ((g : (a : A ⊗[R] B) → C) x : C)
Tactic: ext x
-- 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 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
C : Type u_3
inst_5 : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp (AlgHom.toRingHom includeRight) = g.comp (AlgHom.toRingHom includeRight)
x : A ⊗[R] B
⊢ Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) x : C) ((g : (a : A ⊗[R] B) → C) x : C)
have a : Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) 0 : C) ((g : (a : A ⊗[R] B) → C) 0 : C)
Tactic: induction x with
  | zero => simp
  | add x y _ _ => simp_all
  | tmul x y => simpa [← map_mul] using congr($h₁ x * $h₂ y)
Cleared hypotheses: x
-- 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 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
C : Type u_3
inst_5 : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp (AlgHom.toRingHom includeRight) = g.comp (AlgHom.toRingHom includeRight)
x : A ⊗[R] B
a : Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) 0 : C) ((g : (a : A ⊗[R] B) → C) 0 : C)
⊢ Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) x : C) ((g : (a : A ⊗[R] B) → C) x : C)
have a₁ : ∀ (x y : A ⊗[R] B),
  Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) x : C) ((g : (a : A ⊗[R] B) → C) x : C) →
    Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) y : C) ((g : (a : A ⊗[R] B) → C) y : C) →
      Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (x + y) : C) ((g : (a : A ⊗[R] B) → C) (x + y) : C)
Tactic: induction x with
  | zero => simp
  | add x y _ _ => simp_all
  | tmul x y => simpa [← map_mul] using congr($h₁ x * $h₂ y)
Cleared hypotheses: x
-- 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 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
C : Type u_3
inst_5 : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp (AlgHom.toRingHom includeRight) = g.comp (AlgHom.toRingHom includeRight)
x : A ⊗[R] B
a : Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) 0 : C) ((g : (a : A ⊗[R] B) → C) 0 : C)
a₁ :
  ∀ (x y : A ⊗[R] B),
    Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) x : C) ((g : (a : A ⊗[R] B) → C) x : C) →
      Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) y : C) ((g : (a : A ⊗[R] B) → C) y : C) →
        Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (x + y) : C) ((g : (a : A ⊗[R] B) → C) (x + y) : C)
⊢ Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) x : C) ((g : (a : A ⊗[R] B) → C) x : C)
have a₂ : ∀ (x : A) (y : B),
  Eq.{u_3 + 1} (α := C) ((f : (a : A ⊗[R] B) → C) (x ⊗ₜ[R] y) : C) ((g : (a : A ⊗[R] B) → C) (x ⊗ₜ[R] y) : C)
Tactic: induction x with
  | zero => simp
  | add x y _ _ => simp_all
  | tmul x y => simpa [← map_mul] using congr($h₁ x * $h₂ y)
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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y : A ⊗[R] B
⊢ x * y = y * x
have refine_1 : 0 * y = y * 0
Tactic: refine TensorProduct.induction_on 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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y : A ⊗[R] B
refine_1 : 0 * y = y * 0
⊢ x * y = y * x
have refine_2 : ∀ (x : A) (y_1 : B), x ⊗ₜ[R] y_1 * y = y * x ⊗ₜ[R] y_1
Tactic: refine TensorProduct.induction_on 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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y : A ⊗[R] B
refine_1 : 0 * y = y * 0
refine_2 : ∀ (x : A) (y_1 : B), x ⊗ₜ[R] y_1 * y = y * x ⊗ₜ[R] y_1
⊢ x * y = y * x
have refine_3 : ∀ (x y_1 : A ⊗[R] B), x * y = y * x → y_1 * y = y * y_1 → (x + y_1) * y = y * (x + y_1)
Tactic: refine TensorProduct.induction_on 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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y : A ⊗[R] B
a₁ : A
b₁ : B
⊢ a₁ ⊗ₜ[R] b₁ * y = y * a₁ ⊗ₜ[R] b₁
have refine_2 : HMul.hMul (α := A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) 0 = HMul.hMul (α := A ⊗[R] B) 0 (a₁ ⊗ₜ[R] b₁)
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- 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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y : A ⊗[R] B
a₁ : A
b₁ : B
refine_2 : HMul.hMul (α := A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) 0 = HMul.hMul (α := A ⊗[R] B) 0 (a₁ ⊗ₜ[R] b₁)
⊢ a₁ ⊗ₜ[R] b₁ * y = y * a₁ ⊗ₜ[R] b₁
have refine_2₁ : ∀ (x : A) (y : B),
  HMul.hMul (α := A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) (x ⊗ₜ[R] y) = HMul.hMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) (a₁ ⊗ₜ[R] b₁)
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- 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 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
x y : A ⊗[R] B
a₁ : A
b₁ : B
refine_2 : HMul.hMul (α := A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) 0 = HMul.hMul (α := A ⊗[R] B) 0 (a₁ ⊗ₜ[R] b₁)
refine_2₁ :
  ∀ (x : A) (y : B),
    HMul.hMul (α := A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) (x ⊗ₜ[R] y) = HMul.hMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) (a₁ ⊗ₜ[R] b₁)
⊢ a₁ ⊗ₜ[R] b₁ * y = y * a₁ ⊗ₜ[R] b₁
have refine_2₂ : ∀ (x y : A ⊗[R] B),
  a₁ ⊗ₜ[R] b₁ * x = x * a₁ ⊗ₜ[R] b₁ → a₁ ⊗ₜ[R] b₁ * y = y * a₁ ⊗ₜ[R] b₁ → a₁ ⊗ₜ[R] b₁ * (x + y) = (x + y) * a₁ ⊗ₜ[R] b₁
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Ring B
inst_4 : Algebra R B
z : ℤ
⊢ Eq (α := A ⊗[R] B) (↑z : A ⊗[R] B) (1 ⊗ₜ[R] (↑z : B))
have rw : Eq (α := A ⊗[R] B) ((↑z : A) ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑z : B))
Tactic: rw [intCast_def, ← zsmul_one, smul_tmul, zsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Ring B
inst_4 : Algebra R B
z : ℤ
rw : Eq (α := A ⊗[R] B) ((↑z : A) ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑z : B))
⊢ Eq (α := A ⊗[R] B) (↑z : A ⊗[R] B) (1 ⊗ₜ[R] (↑z : B))
have rw₁ : Eq (α := A ⊗[R] B) (HSMul.hSMul (β := A) z 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑z : B))
Tactic: rw [intCast_def, ← zsmul_one, smul_tmul, zsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Ring B
inst_4 : Algebra R B
z : ℤ
rw : Eq (α := A ⊗[R] B) ((↑z : A) ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑z : B))
rw₁ : Eq (α := A ⊗[R] B) (HSMul.hSMul (β := A) z 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑z : B))
⊢ Eq (α := A ⊗[R] B) (↑z : A ⊗[R] B) (1 ⊗ₜ[R] (↑z : B))
have rw₂ : Eq (α := A ⊗[R] B) (1 ⊗ₜ[R] HSMul.hSMul (β := B) z 1) (1 ⊗ₜ[R] (↑z : B))
Tactic: rw [intCast_def, ← zsmul_one, smul_tmul, zsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Ring B
inst_4 : Algebra R B
z : ℤ
rw : Eq (α := A ⊗[R] B) ((↑z : A) ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑z : B))
rw₁ : Eq (α := A ⊗[R] B) (HSMul.hSMul (β := A) z 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑z : B))
rw₂ : Eq (α := A ⊗[R] B) (1 ⊗ₜ[R] HSMul.hSMul (β := B) z 1) (1 ⊗ₜ[R] (↑z : B))
⊢ Eq (α := A ⊗[R] B) (↑z : A ⊗[R] B) (1 ⊗ₜ[R] (↑z : B))
have rw₃ : Eq (α := A ⊗[R] B) (1 ⊗ₜ[R] (↑z : B)) (1 ⊗ₜ[R] (↑z : B))
Tactic: rw [intCast_def, ← zsmul_one, smul_tmul, zsmul_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 : Semiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
b : B
x : A ⊗[R] B
⊢ HMul.hMul (α := A ⊗[R] B) ((AlgHom.toRingHom includeRight : (a : B) → A ⊗[R] B) b : A ⊗[R] B) x =
    HMul.hMul (β := A ⊗[R] B) x ((AlgHom.toRingHom includeRight : (a : B) → A ⊗[R] B) b : A ⊗[R] B)
have suffices : Eq (α := A ⊗[R] B →ₗ[R] A ⊗[R] B)
  (LinearMap.mulLeft R ((includeRight : (a : B) → A ⊗[R] B) b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)
  (LinearMap.mulRight R ((includeRight : (a : B) → A ⊗[R] B) b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)
Tactic: suffices LinearMap.mulLeft R (includeRight b) = LinearMap.mulRight R (includeRight b) from
      congr($this 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 : Semiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
b : B
x : A ⊗[R] B
⊢ Eq (α := A ⊗[R] B →ₗ[R] A ⊗[R] B)
    (LinearMap.mulLeft R ((includeRight : (a : B) → A ⊗[R] B) b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)
    (LinearMap.mulRight R ((includeRight : (a : B) → A ⊗[R] B) b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)
have a : ∀ (xa : A) (xb : B),
  Eq (α := A ⊗[R] B)
    (((((AlgebraTensorModule.curry (LinearMap.mulLeft R ((includeRight : (a : B) → A ⊗[R] B) b)) :
                  A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              xa :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        xb :
      A ⊗[R] B)
    (((((AlgebraTensorModule.curry (LinearMap.mulRight R ((includeRight : (a : B) → A ⊗[R] B) b)) :
                  A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              xa :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        xb :
      A ⊗[R] B)
Tactic: ext xa xb
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Eq (α := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    ⊤
have rw : LE.le (α := Subring (A ⊗[R] B)) ⊤
  (Subring.closure
    (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪ Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
Tactic: rw [← top_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A
y : B
⊢ Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    (x ⊗ₜ[R] y)
have h : x ⊗ₜ[R] y =
  HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeftRingHom : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
    ((includeRight : (a : B) → A ⊗[R] B) y : A ⊗[R] B)
Tactic: convert_to (Algebra.TensorProduct.includeLeftRingHom (R := R) x) *
      (Algebra.TensorProduct.includeRight y) ∈ _
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A
y : B
h :
  x ⊗ₜ[R] y =
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeftRingHom : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
      ((includeRight : (a : B) → A ⊗[R] B) y : A ⊗[R] B)
⊢ Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    (x ⊗ₜ[R] y)
have tmul : Membership.mem (γ := Subring (A ⊗[R] B))
  (Subring.closure
    (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪ Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
  (HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeftRingHom : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
    ((includeRight : (a : B) → A ⊗[R] B) y : A ⊗[R] B))
Tactic: convert_to (Algebra.TensorProduct.includeLeftRingHom (R := R) x) *
      (Algebra.TensorProduct.includeRight y) ∈ _