awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
⊢ HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
      (((lof.{u_1, u_2, u_4} R ι (fun (x : ι) ↦ ↥(ℬ x)) j : ↥(ℬ j) →ₗ[R] ⨁ (i : ι), ↥(ℬ i)) :
              (a : ↥(ℬ j)) → ⨁ (i : ι), ↥(ℬ i))
            b ⊗ₜ[R]
          ((lof.{u_1, u_2, u_3} R ι (fun (x : ι) ↦ ↥(𝒜 x)) i : ↥(𝒜 i) →ₗ[R] ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            a :
        (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) =
    HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
      ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) (↑b : B) ⊗ₜ[R] (decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑a : A) :
        (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
have simp_rw : HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
    (((lof.{u_1, u_2, u_4} R ι (fun (x : ι) ↦ ↥(ℬ x)) j : ↥(ℬ j) →ₗ[R] ⨁ (i : ι), ↥(ℬ i)) :
            (a : ↥(ℬ j)) → ⨁ (i : ι), ↥(ℬ i))
          b ⊗ₜ[R]
        ((lof.{u_1, u_2, u_3} R ι (fun (x : ι) ↦ ↥(𝒜 x)) i : ↥(𝒜 i) →ₗ[R] ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
          a :
      (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) =
  HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
    (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
    (((DirectSum.of.{u_2, u_4} (fun (i : ι) ↦ ↥(ℬ i)) j : ↥(ℬ j) →+ ⨁ (i : ι), ↥(ℬ i)) :
            (a : ↥(ℬ j)) → ⨁ (i : ι), ↥(ℬ i))
          b ⊗ₜ[R]
        ((DirectSum.of.{u_2, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
          a :
      (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
Tactic: simp_rw [decompose_coe, lof_eq_of]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ (map f g).range = Submodule.map₂ (mk R P Q) f.range g.range
have simp_rw : Submodule.map₂ (compr₂ (mk R M N) (map f g)) ⊤ ⊤ = Submodule.map₂ (compl₁₂ (mk R P Q) f g) ⊤ ⊤
Tactic: simp_rw [← Submodule.map_top, Submodule.map₂_map_map, ← map₂_mk_top_top_eq_top,
    Submodule.map_map₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ (map f g).range =
    Submodule.span R {t : P ⊗[R] Q | ∃ (m : M) (n : N), (f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n = t}
have simp : Eq (α := Submodule R (P ⊗[R] Q))
  (Submodule.span R
    (Set.image (α := M ⊗[R] N) (⇑(map f g) : (a : M ⊗[R] N) → P ⊗[R] Q)
      {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}))
  (Submodule.span R {t : P ⊗[R] Q | ∃ (m : M) (n : N), (f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n = t})
Tactic: simp only [← Submodule.map_top, ← span_tmul_eq_top, Submodule.map_span]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ Eq (α := Submodule R (P ⊗[R] Q))
    (Submodule.span R
      (Set.image (α := M ⊗[R] N) (⇑(map f g) : (a : M ⊗[R] N) → P ⊗[R] Q)
        {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}))
    (Submodule.span R {t : P ⊗[R] Q | ∃ (m : M) (n : N), (f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n = t})
have e_s : Eq (α := Set (P ⊗[R] Q))
  (Set.image (α := M ⊗[R] N) (⇑(map f g) : (a : M ⊗[R] N) → P ⊗[R] Q) {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
  {t : P ⊗[R] Q | ∃ (m : M) (n : N), (f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n = t}
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ Eq (α := Set (P ⊗[R] Q))
    (Set.image (α := M ⊗[R] N) (⇑(map f g) : (a : M ⊗[R] N) → P ⊗[R] Q)
      {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
    {t : P ⊗[R] Q | ∃ (m : M) (n : N), (f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n = t}
have e_s : ∀ (t : P ⊗[R] Q),
  Membership.mem (γ := Set (P ⊗[R] Q))
      (Set.image (α := M ⊗[R] N) (⇑(map f g) : (a : M ⊗[R] N) → P ⊗[R] Q)
        {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
      t ↔
    Membership.mem (γ := Set (P ⊗[R] Q))
      {t : P ⊗[R] Q | ∃ (m : M) (n : N), (f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n = t} t
Tactic: ext t
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid P
inst_2 : AddCommMonoid Q
inst_3 : Module R P
inst_4 : Module R Q
p : Submodule R P
q : Submodule R Q
⊢ (mapIncl p q).range = Submodule.map₂ (mk R P Q) p q
have simp_rw : (map p.subtype q.subtype).range = Submodule.map₂ (mk R P Q) p q
Tactic: simp_rw [mapIncl, range_map, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid P
inst_2 : AddCommMonoid Q
inst_3 : Module R P
inst_4 : Module R Q
p : Submodule R P
q : Submodule R Q
simp_rw : (map p.subtype q.subtype).range = Submodule.map₂ (mk R P Q) p q
⊢ (mapIncl p q).range = Submodule.map₂ (mk R P Q) p q
have simp_rw₁ : Submodule.map₂ (mk R P Q) p.subtype.range q.subtype.range = Submodule.map₂ (mk R P Q) p q
Tactic: simp_rw [mapIncl, range_map, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
f : P →ₗ[R] Q →ₗ[R] M
p : Submodule R P
q : Submodule R Q
⊢ Submodule.map₂ f p q = (lift f ∘ₗ mapIncl p q).range
have simp_rw : Submodule.map₂ f p q = Submodule.map₂ (compr₂ (mk R P Q) (lift f)) p q
Tactic: simp_rw [LinearMap.range_comp, range_mapIncl, Submodule.map_map₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₃
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R N₂
inst_12 : Module R N₃
a : M →ₗ[R] M₂
b : M₃ →ₗ[R] M₂
c : N →ₗ[R] N₂
d : N₃ →ₗ[R] N₂
hab : a.range ≤ b.range
hcd : c.range ≤ d.range
⊢ (map a c).range ≤ (map b d).range
have simp_rw : Submodule.map₂ (mk R M₂ N₂) a.range c.range ≤ Submodule.map₂ (mk R M₂ N₂) b.range d.range
Tactic: simp_rw [range_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (map LinearMap.id LinearMap.id) LinearMap.id
have H : ∀ (x : M) (x_1 : N),
  Eq (α := M ⊗[R] N)
    ((((compr₂ₛₗ (mk R M N) (map LinearMap.id LinearMap.id) : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
          (a : N) → M ⊗[R] N)
        x_1 :
      M ⊗[R] N)
    ((((compr₂ₛₗ (mk R M N) LinearMap.id : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) : (a : N) → M ⊗[R] N) x_1 :
      M ⊗[R] N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M →ₗ[R] M
g : N →ₗ[R] N
n : ℕ
⊢ map f g ^ n = map (f ^ n) (g ^ n)
have zero : HPow.hPow (β := ℕ) (map f g) 0 = map (HPow.hPow (β := ℕ) f 0) (HPow.hPow (β := ℕ) g 0)
Tactic: induction n with
  | zero => simp only [pow_zero, TensorProduct.map_one]
  | succ n ih => simp only [pow_succ', ih, TensorProduct.map_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M →ₗ[R] M
g : N →ₗ[R] N
n : ℕ
zero : HPow.hPow (β := ℕ) (map f g) 0 = map (HPow.hPow (β := ℕ) f 0) (HPow.hPow (β := ℕ) g 0)
⊢ map f g ^ n = map (f ^ n) (g ^ n)
have succ : ∀ (n : ℕ) (ih : map f g ^ n = map (f ^ n) (g ^ n)), map f g ^ (n + 1) = map (f ^ (n + 1)) (g ^ (n + 1))
Tactic: induction n with
  | zero => simp only [pow_zero, TensorProduct.map_one]
  | succ n ih => simp only [pow_succ', ih, TensorProduct.map_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
f₁ f₂ : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
⊢ map (f₁ + f₂) g = map f₁ g + map f₂ g
have H : ∀ (x : M) (x_1 : N),
  Eq (α := M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (map (f₁ + f₂) g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (map f₁ g + map f₂ g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
f : M →ₛₗ[σ₁₂] M₂
g₁ g₂ : N →ₛₗ[σ₁₂] N₂
⊢ map f (g₁ + g₂) = map f g₁ + map f g₂
have H : ∀ (x : M) (x_1 : N),
  Eq (α := M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (map f (g₁ + g₂)) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (map f g₁ + map f g₂) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
r : R₂
f : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
⊢ map (r • f) g = r • map f g
have H : ∀ (x : M) (x_1 : N),
  Eq (α := M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (map (r • f) g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (r • map f g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
r : R₂
f : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
⊢ map f (r • g) = r • map f g
have H : ∀ (x : M) (x_1 : N),
  Eq (α := M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (map f (r • g)) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (r • map f g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
ih : congr f g ^ n = congr (f ^ n) (g ^ n)
⊢ congr f g ^ (n + 1) = congr (f ^ (n + 1)) (g ^ (n + 1))
have succ : congr f g ^ n * congr f g = congr (f ^ n * f) (g ^ n * g)
Tactic: simp_rw [pow_succ, ih, congr_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
ih : congr f g ^ n = congr (f ^ n) (g ^ n)
succ : congr f g ^ n * congr f g = congr (f ^ n * f) (g ^ n * g)
⊢ congr f g ^ (n + 1) = congr (f ^ (n + 1)) (g ^ (n + 1))
have succ₁ : congr (f ^ n) (g ^ n) * congr f g = congr (f ^ n * f) (g ^ n * g)
Tactic: simp_rw [pow_succ, ih, congr_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ congr f g ^ n = congr (f ^ n) (g ^ n)
have zero : HPow.hPow (β := ℕ) (congr f g) 0 = congr (HPow.hPow (β := ℕ) f 0) (HPow.hPow (β := ℕ) g 0)
Tactic: induction n with
  | zero => exact congr_refl_refl.symm
  | succ n ih => simp_rw [pow_succ, ih, congr_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
zero : HPow.hPow (β := ℕ) (congr f g) 0 = congr (HPow.hPow (β := ℕ) f 0) (HPow.hPow (β := ℕ) g 0)
⊢ congr f g ^ n = congr (f ^ n) (g ^ n)
have succ : ∀ (n : ℕ) (ih : congr f g ^ n = congr (f ^ n) (g ^ n)), congr f g ^ (n + 1) = congr (f ^ (n + 1)) (g ^ (n + 1))
Tactic: induction n with
  | zero => exact congr_refl_refl.symm
  | succ n ih => simp_rw [pow_succ, ih, congr_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ congr f g ^ Int.negSucc n = congr (f ^ Int.negSucc n) (g ^ Int.negSucc n)
have negSucc : (congr (f ^ (n + 1)) (g ^ (n + 1)))⁻¹ = congr (f ^ (n + 1))⁻¹ (g ^ (n + 1))⁻¹
Tactic: simp_rw [zpow_negSucc, congr_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℤ
⊢ congr f g ^ n = congr (f ^ n) (g ^ n)
have ofNat : ∀ (n : ℕ), congr f g ^ Int.ofNat n = congr (f ^ Int.ofNat n) (g ^ Int.ofNat n)
Tactic: cases n with
  | ofNat n => exact congr_pow _ _ _
  | negSucc n => simp_rw [zpow_negSucc, congr_pow]; exact congr_symm _ _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℤ
ofNat : ∀ (n : ℕ), congr f g ^ Int.ofNat n = congr (f ^ Int.ofNat n) (g ^ Int.ofNat n)
⊢ congr f g ^ n = congr (f ^ n) (g ^ n)
have negSucc : ∀ (n : ℕ), congr f g ^ Int.negSucc n = congr (f ^ Int.negSucc n) (g ^ Int.negSucc n)
Tactic: cases n with
  | ofNat n => exact congr_pow _ _ _
  | negSucc n => simp_rw [zpow_negSucc, congr_pow]; exact congr_symm _ _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (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₃
inst_35 : Module R P
inst_36 : Module R Q
g_1 : P →ₗ[R] Q
f_1 f g : N →ₗ[R] P
⊢ lTensor M (f + g) = HAdd.hAdd (α := M ⊗[R] N →ₗ[R] M ⊗[R] P) (lTensor M f) (lTensor M g)
have H : ∀ (x : M) (y : N),
  Eq (α := M ⊗[R] P)
    ((((compr₂ₛₗ (TensorProduct.mk R M N) (lTensor M (f + g)) : (a : M) → N →ₗ[R] M ⊗[R] P) x : N →ₗ[R] M ⊗[R] P) :
          (a : N) → M ⊗[R] P)
        y :
      M ⊗[R] P)
    ((((compr₂ₛₗ (TensorProduct.mk R M N) (HAdd.hAdd (α := M ⊗[R] N →ₗ[R] M ⊗[R] P) (lTensor M f) (lTensor M g)) :
                (a : M) → N →ₗ[R] M ⊗[R] P)
              x :
            N →ₗ[R] M ⊗[R] P) :
          (a : N) → M ⊗[R] P)
        y :
      M ⊗[R] P)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (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₃
inst_35 : Module R P
inst_36 : Module R Q
g : P →ₗ[R] Q
f_1 : N →ₗ[R] P
r : R
f : N →ₗ[R] P
⊢ lTensor M (r • f) =
    HSMul.hSMul (α := R) (β := M ⊗[R] N →ₗ[R] M ⊗[R] P) ((RingHom.id R : (a : R) → R) r : R) (lTensor M f)
have dsimp : lTensor M (r • f) = HSMul.hSMul (β := M ⊗[R] N →ₗ[R] M ⊗[R] P) r (lTensor M f)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (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₃
inst_35 : Module R P
inst_36 : Module R Q
g : P →ₗ[R] Q
f_1 : N →ₗ[R] P
r : R
f : N →ₗ[R] P
⊢ lTensor M (r • f) = HSMul.hSMul (β := M ⊗[R] N →ₗ[R] M ⊗[R] P) r (lTensor M f)
have H : ∀ (x : M) (y : N),
  Eq (α := M ⊗[R] P)
    ((((compr₂ₛₗ (TensorProduct.mk R M N) (lTensor M (r • f)) : (a : M) → N →ₗ[R] M ⊗[R] P) x : N →ₗ[R] M ⊗[R] P) :
          (a : N) → M ⊗[R] P)
        y :
      M ⊗[R] P)
    ((((compr₂ₛₗ (TensorProduct.mk R M N) (HSMul.hSMul (β := M ⊗[R] N →ₗ[R] M ⊗[R] P) r (lTensor M f)) :
                (a : M) → N →ₗ[R] M ⊗[R] P)
              x :
            N →ₗ[R] M ⊗[R] P) :
          (a : N) → M ⊗[R] P)
        y :
      M ⊗[R] P)
Tactic: ext x y