awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
f : M →+ N →+ P
hf :
  ∀ (r : R) (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (r • m) : N →+ P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (r • n) : P)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
n : N
simp_rw :
  Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (0, n)) :
      P)
    (0 : P)
⊢ Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (0, n)) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        0 :
      P)
have simp_rw₁ : Eq.{u_9 + 1} (α := P) (((f : (a : M) → N →+ P) 0 : (a : N) → P) n : P) (0 : P)
Tactic: simp_rw [map_zero, FreeAddMonoid.lift_eval_of, map_zero,
          AddMonoidHom.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
f : M →+ N →+ P
hf :
  ∀ (r : R) (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (r • m) : N →+ P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (r • n) : P)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
n : N
simp_rw :
  Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (0, n)) :
      P)
    (0 : P)
simp_rw₁ : Eq.{u_9 + 1} (α := P) (((f : (a : M) → N →+ P) 0 : (a : N) → P) n : P) (0 : P)
⊢ Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (0, n)) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        0 :
      P)
have simp_rw₂ : Eq.{u_9 + 1} (α := P) ((0 : (a : N) → P) n : P) (0 : P)
Tactic: simp_rw [map_zero, FreeAddMonoid.lift_eval_of, map_zero,
          AddMonoidHom.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
f : M →+ N →+ P
hf :
  ∀ (r : R) (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (r • m) : N →+ P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (r • n) : P)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m : M
⊢ Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, 0)) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        0 :
      P)
have simp_rw : Eq.{u_9 + 1} (α := P)
  (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
          (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
        (a : FreeAddMonoid (M × N)) → P)
      (FreeAddMonoid.of (m, 0)) :
    P)
  (0 : P)
Tactic: simp_rw [map_zero, FreeAddMonoid.lift_eval_of, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
f : M →+ N →+ P
hf :
  ∀ (r : R) (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (r • m) : N →+ P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (r • n) : P)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m : M
simp_rw :
  Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, 0)) :
      P)
    (0 : P)
⊢ Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, 0)) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        0 :
      P)
have simp_rw₁ : Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) 0 : P) (0 : P)
Tactic: simp_rw [map_zero, FreeAddMonoid.lift_eval_of, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
f : M →+ N →+ P
hf :
  ∀ (r : R) (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (r • m) : N →+ P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (r • n) : P)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m₁ m₂ : M
n : N
⊢ Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m₁, n) + FreeAddMonoid.of (m₂, n)) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m₁ + m₂, n)) :
      P)
have simp_rw : HAdd.hAdd (α := P) (β := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m₁, n)) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m₂, n)) :
      P) =
  ((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
        (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
      (a : FreeAddMonoid (M × N)) → P)
    (FreeAddMonoid.of (m₁ + m₂, n))
Tactic: simp_rw [map_add, FreeAddMonoid.lift_eval_of, map_add,
          AddMonoidHom.add_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
f : M →+ N →+ P
hf :
  ∀ (r : R) (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (r • m) : N →+ P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (r • n) : P)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m : M
n₁ n₂ : N
⊢ Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, n₁) + FreeAddMonoid.of (m, n₂)) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, n₁ + n₂)) :
      P)
have simp_rw : HAdd.hAdd (α := P) (β := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, n₁)) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, n₂)) :
      P) =
  ((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
        (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
      (a : FreeAddMonoid (M × N)) → P)
    (FreeAddMonoid.of (m, n₁ + n₂))
Tactic: simp_rw [map_add, FreeAddMonoid.lift_eval_of, map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
f : M →+ N →+ P
hf :
  ∀ (r : R) (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (r • m) : N →+ P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (r • n) : P)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
s : R
m : M
n : N
⊢ Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (s • m, n)) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, s • n)) :
      P)
have rw : Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (s • m, n).1 : N →+ P) : (a : N) → P) (s • m, n).2 : P)
  (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
          (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
        (a : FreeAddMonoid (M × N)) → P)
      (FreeAddMonoid.of (m, s • n)) :
    P)
Tactic: rw [FreeAddMonoid.lift_eval_of, FreeAddMonoid.lift_eval_of, hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
f : M →+ N →+ P
hf :
  ∀ (r : R) (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (r • m) : N →+ P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (r • n) : P)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
s : R
m : M
n : N
rw :
  Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (s • m, n).1 : N →+ P) : (a : N) → P) (s • m, n).2 : P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, s • n)) :
      P)
⊢ Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (s • m, n)) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, s • n)) :
      P)
have rw₁ : Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (s • m, n).1 : N →+ P) : (a : N) → P) (s • m, n).2 : P)
  ((((f : (a : M) → N →+ P) (m, s • n).1 : N →+ P) : (a : N) → P) (m, s • n).2 : P)
Tactic: rw [FreeAddMonoid.lift_eval_of, FreeAddMonoid.lift_eval_of, hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
f : M →+ N →+ P
hf :
  ∀ (r : R) (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (r • m) : N →+ P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (r • n) : P)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
s : R
m : M
n : N
rw :
  Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (s • m, n).1 : N →+ P) : (a : N) → P) (s • m, n).2 : P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, s • n)) :
      P)
rw₁ :
  Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (s • m, n).1 : N →+ P) : (a : N) → P) (s • m, n).2 : P)
    ((((f : (a : M) → N →+ P) (m, s • n).1 : N →+ P) : (a : N) → P) (m, s • n).2 : P)
⊢ Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (s • m, n)) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, s • n)) :
      P)
have rw₂ : Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (s • (s • m, n).2) : P)
  ((((f : (a : M) → N →+ P) (m, s • n).1 : N →+ P) : (a : N) → P) (m, s • n).2 : P)
Tactic: rw [FreeAddMonoid.lift_eval_of, FreeAddMonoid.lift_eval_of, hf]