awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
y : A ⊗[R] M
hy : Membership.mem (γ := Submodule A (A ⊗[R] M)) (baseChange A p) y
⊢ ∃ (x : TensorProduct.{u_1, u_3, u_2} R A ↥p),
    (↑((toBaseChange A p : (a : A ⊗[R] ↥p) → ↥(baseChange A p)) x) : A ⊗[R] M) = y
have obtain : ∀ (x : TensorProduct.{u_1, u_3, u_2} R A ↥p)
  (hx :
    (toBaseChange A p : (a : A ⊗[R] ↥p) → ↥(baseChange A p)) x =
      Subtype.mk (p := fun (x : A ⊗[R] M) ↦ Membership.mem (γ := Submodule A (A ⊗[R] M)) (baseChange A p) x) y hy),
  ∃ (x : TensorProduct.{u_1, u_3, u_2} R A ↥p),
    (↑((toBaseChange A p : (a : A ⊗[R] ↥p) → ↥(baseChange A p)) x) : A ⊗[R] M) = y
Tactic: obtain ⟨x, hx⟩ := toBaseChange_surjective A p ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module A N
f : A ⊗[R] M →ₗ[A] N
⊢ LinearMap.baseChange A f ∘ₗ (↑(LinearEquiv.symm (cancelBaseChange R A A A M)) : A ⊗[R] M →ₗ[A] A ⊗[A] (A ⊗[R] M)) =
    (↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N) ∘ₗ f
have rw : LinearMap.baseChange A f ∘ₗ (↑(LinearEquiv.symm (TensorProduct.lid A (A ⊗[R] M))) : A ⊗[R] M →ₗ[A] A ⊗[A] (A ⊗[R] M)) =
  (↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N) ∘ₗ f
Tactic: rw [cancelBaseChange_self_eq_lid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module A N
f : A ⊗[R] M →ₗ[A] N
⊢ LinearMap.baseChange A f ∘ₗ
      (↑(LinearEquiv.symm (TensorProduct.lid A (A ⊗[R] M))) : A ⊗[R] M →ₗ[A] A ⊗[A] (A ⊗[R] M)) =
    (↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N) ∘ₗ f
have a : ∀ (x : M),
  Eq (α := A ⊗[A] N)
    ((((curry
                  (LinearMap.baseChange A f ∘ₗ
                    (↑(LinearEquiv.symm (TensorProduct.lid A (A ⊗[R] M))) : A ⊗[R] M →ₗ[A] A ⊗[A] (A ⊗[R] M))) :
                A →ₗ[A] M →ₗ[R] A ⊗[A] N) :
              (a : A) → M →ₗ[R] A ⊗[A] N)
            1 :
          (a : M) → A ⊗[A] N)
        x :
      A ⊗[A] N)
    ((((curry ((↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N) ∘ₗ f) : A →ₗ[A] M →ₗ[R] A ⊗[A] N) :
              (a : A) → M →ₗ[R] A ⊗[A] N)
            1 :
          (a : M) → A ⊗[A] N)
        x :
      A ⊗[A] N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module A N
f : A ⊗[R] M →ₗ[A] N
⊢ LinearMap.ker
      (LinearMap.baseChange A f ∘ₗ
        (↑(LinearEquiv.symm (cancelBaseChange R A A A M)) : A ⊗[R] M →ₗ[A] A ⊗[A] (A ⊗[R] M))) =
    f.ker
have rw : ((↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N) ∘ₗ f).ker = f.ker
Tactic: rw [baseChange_comp_cancelBaseChange_symm_self, LinearMap.ker_comp,
    LinearEquiv.ker, Submodule.comap_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module A N
f : A ⊗[R] M →ₗ[A] N
rw : ((↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N) ∘ₗ f).ker = f.ker
⊢ LinearMap.ker
      (LinearMap.baseChange A f ∘ₗ
        (↑(LinearEquiv.symm (cancelBaseChange R A A A M)) : A ⊗[R] M →ₗ[A] A ⊗[A] (A ⊗[R] M))) =
    f.ker
have rw₁ : Submodule.comap f (LinearMap.ker (↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N)) = f.ker
Tactic: rw [baseChange_comp_cancelBaseChange_symm_self, LinearMap.ker_comp,
    LinearEquiv.ker, Submodule.comap_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module A N
f : A ⊗[R] M →ₗ[A] N
rw : ((↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N) ∘ₗ f).ker = f.ker
rw₁ : Submodule.comap f (LinearMap.ker (↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N)) = f.ker
⊢ LinearMap.ker
      (LinearMap.baseChange A f ∘ₗ
        (↑(LinearEquiv.symm (cancelBaseChange R A A A M)) : A ⊗[R] M →ₗ[A] A ⊗[A] (A ⊗[R] M))) =
    f.ker
have rw₂ : Submodule.comap f ⊥ = f.ker
Tactic: rw [baseChange_comp_cancelBaseChange_symm_self, LinearMap.ker_comp,
    LinearEquiv.ker, Submodule.comap_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module A N
f : A ⊗[R] M →ₗ[A] N
rw : ((↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N) ∘ₗ f).ker = f.ker
rw₁ : Submodule.comap f (LinearMap.ker (↑(LinearEquiv.symm (TensorProduct.lid A N)) : N →ₗ[A] A ⊗[A] N)) = f.ker
rw₂ : Submodule.comap f ⊥ = f.ker
⊢ LinearMap.ker
      (LinearMap.baseChange A f ∘ₗ
        (↑(LinearEquiv.symm (cancelBaseChange R A A A M)) : A ⊗[R] M →ₗ[A] A ⊗[A] (A ⊗[R] M))) =
    f.ker
have rw₃ : f.ker = f.ker
Tactic: rw [baseChange_comp_cancelBaseChange_symm_self, LinearMap.ker_comp,
    LinearEquiv.ker, Submodule.comap_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
κ : Type u_5
inst_6 : Fintype κ
a : ι → κ → R
y : κ → N
hay : ∀ (i : ι), n i = ∑ j : κ, a i j • y j
ham : ∀ (j : κ), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0
e : Fin (Fintype.card κ) ≃ κ
⊢ ∀ (j : Fin (Fintype.card κ)),
    Eq.{u_2 + 1} (α := M)
      (∑ i : ι,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R)
          ((fun (x : ι) ↦ (a x ∘ (⇑e : (a : Fin (Fintype.card κ)) → κ) : Fin (Fintype.card κ) → R)) i j) (m i))
      0
have rwa : ∀
  (ham :
    ∀ (a_1 : Fin (Fintype.card κ)),
      Eq.{u_2 + 1} (α := M) (∑ i : ι, a i ((e : (a : Fin (Fintype.card κ)) → κ) a_1) • m i) 0)
  (j : Fin (Fintype.card κ)),
  Eq.{u_2 + 1} (α := M)
    (∑ i : ι,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((fun (x : ι) ↦ (a x ∘ (⇑e : (a : Fin (Fintype.card κ)) → κ) : Fin (Fintype.card κ) → R)) i j) (m i))
    0
Tactic: rwa [← e.forall_congr_right] at ham
Cleared hypotheses: ham
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hmn : VanishesTrivially R m n
⊢ Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
have obtain : ∀ (k : ℕ) (a : ι → Fin k → R) (y : Fin k → N) (h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j)
  (h₂ : ∀ (j : Fin k), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0), Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
Tactic: obtain ⟨k, a, y, h₁, h₂⟩ := hmn
Cleared hypotheses: hmn
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0
⊢ Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
have simp_rw : Eq (α := M ⊗[R] N) (∑ x : ι, ∑ x_1 : Fin k, HSMul.hSMul (β := M ⊗[R] N) (a x x_1) (m x ⊗ₜ[R] y x_1)) 0
Tactic: simp_rw [h₁, tmul_sum, tmul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0
⊢ Eq (α := M ⊗[R] N) (∑ x : ι, ∑ x_1 : Fin k, HSMul.hSMul (β := M ⊗[R] N) (a x x_1) (m x ⊗ₜ[R] y x_1)) 0
have rw : Eq (α := M ⊗[R] N) (∑ y_1 : Fin k, ∑ x : ι, HSMul.hSMul (β := M ⊗[R] N) (a x y_1) (m x ⊗ₜ[R] y y_1)) 0
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0
⊢ Eq (α := M ⊗[R] N) (∑ y_1 : Fin k, ∑ x : ι, HSMul.hSMul (β := M ⊗[R] N) (a x y_1) (m x ⊗ₜ[R] y y_1)) 0
have simp_rw : Eq (α := M ⊗[R] N) (∑ x : Fin k, ∑ x_1 : ι, m x_1 ⊗ₜ[R] (a x_1 x • y x)) 0
Tactic: simp_rw [← tmul_smul, ← smul_tmul, ← sum_tmul, h₂, zero_tmul, Finset.sum_const_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0
simp_rw : Eq (α := M ⊗[R] N) (∑ x : Fin k, ∑ x_1 : ι, m x_1 ⊗ₜ[R] (a x_1 x • y x)) 0
⊢ Eq (α := M ⊗[R] N) (∑ y_1 : Fin k, ∑ x : ι, HSMul.hSMul (β := M ⊗[R] N) (a x y_1) (m x ⊗ₜ[R] y y_1)) 0
have simp_rw₁ : Eq (α := M ⊗[R] N) (∑ x : Fin k, ∑ x_1 : ι, (a x_1 x • m x_1) ⊗ₜ[R] y x) 0
Tactic: simp_rw [← tmul_smul, ← smul_tmul, ← sum_tmul, h₂, zero_tmul, Finset.sum_const_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0
simp_rw : Eq (α := M ⊗[R] N) (∑ x : Fin k, ∑ x_1 : ι, m x_1 ⊗ₜ[R] (a x_1 x • y x)) 0
simp_rw₁ : Eq (α := M ⊗[R] N) (∑ x : Fin k, ∑ x_1 : ι, (a x_1 x • m x_1) ⊗ₜ[R] y x) 0
⊢ Eq (α := M ⊗[R] N) (∑ y_1 : Fin k, ∑ x : ι, HSMul.hSMul (β := M ⊗[R] N) (a x y_1) (m x ⊗ₜ[R] y y_1)) 0
have simp_rw₂ : Eq (α := M ⊗[R] N) (∑ x : Fin k, (∑ a_1 : ι, a a_1 x • m a_1) ⊗ₜ[R] y x) 0
Tactic: simp_rw [← tmul_smul, ← smul_tmul, ← sum_tmul, h₂, zero_tmul, Finset.sum_const_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0
simp_rw : Eq (α := M ⊗[R] N) (∑ x : Fin k, ∑ x_1 : ι, m x_1 ⊗ₜ[R] (a x_1 x • y x)) 0
simp_rw₁ : Eq (α := M ⊗[R] N) (∑ x : Fin k, ∑ x_1 : ι, (a x_1 x • m x_1) ⊗ₜ[R] y x) 0
simp_rw₂ : Eq (α := M ⊗[R] N) (∑ x : Fin k, (∑ a_1 : ι, a a_1 x • m a_1) ⊗ₜ[R] y x) 0
⊢ Eq (α := M ⊗[R] N) (∑ y_1 : Fin k, ∑ x : ι, HSMul.hSMul (β := M ⊗[R] N) (a x y_1) (m x ⊗ₜ[R] y y_1)) 0
have simp_rw₃ : Eq (α := M ⊗[R] N) (∑ x : Fin k, 0 ⊗ₜ[R] y x) 0
Tactic: simp_rw [← tmul_smul, ← smul_tmul, ← sum_tmul, h₂, zero_tmul, Finset.sum_const_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0
simp_rw : Eq (α := M ⊗[R] N) (∑ x : Fin k, ∑ x_1 : ι, m x_1 ⊗ₜ[R] (a x_1 x • y x)) 0
simp_rw₁ : Eq (α := M ⊗[R] N) (∑ x : Fin k, ∑ x_1 : ι, (a x_1 x • m x_1) ⊗ₜ[R] y x) 0
simp_rw₂ : Eq (α := M ⊗[R] N) (∑ x : Fin k, (∑ a_1 : ι, a a_1 x • m a_1) ⊗ₜ[R] y x) 0
simp_rw₃ : Eq (α := M ⊗[R] N) (∑ x : Fin k, 0 ⊗ₜ[R] y x) 0
⊢ Eq (α := M ⊗[R] N) (∑ y_1 : Fin k, ∑ x : ι, HSMul.hSMul (β := M ⊗[R] N) (a x y_1) (m x ⊗ₜ[R] y y_1)) 0
have simp_rw₄ : Eq (α := M ⊗[R] N) (∑ x : Fin k, 0) 0
Tactic: simp_rw [← tmul_smul, ← smul_tmul, ← sum_tmul, h₂, zero_tmul, Finset.sum_const_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
⊢ VanishesTrivially R m n
have hG : let G : (ι →₀ R) →ₗ[R] M := linearCombination R m;
G = linearCombination R m
Tactic: set G : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R m with hG
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
⊢ VanishesTrivially R m n
have G_basis_eq : ∀ (i : ι), (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
Tactic: have G_basis_eq (i : ι) : G (Finsupp.single i 1) = m i := by simp [hG]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
⊢ Surjective (α := ι →₀ R) (β := M) (⇑G : (a : ι →₀ R) → M)
have apply : G.range = ⊤
Tactic: apply LinearMap.range_eq_top.mp
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
⊢ G.range = ⊤
have apply : ⊤ ≤ G.range
Tactic: apply top_le_iff.mp
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
⊢ ⊤ ≤ G.range
have rw : span R (Set.range m) ≤ G.range
Tactic: rw [← hm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
⊢ span R (Set.range m) ≤ G.range
have apply : Set.range m ⊆ (↑G.range : Set M)
Tactic: apply Submodule.span_le.mpr
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
i : ι
⊢ m i ∈ (↑G.range : Set M)
have w : ι →₀ R
Tactic: use Finsupp.single i 1, G_basis_eq i
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
i : ι
w : ι →₀ R
⊢ m i ∈ (↑G.range : Set M)
have h : (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
Tactic: use Finsupp.single i 1, G_basis_eq i
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
⊢ VanishesTrivially R m n
have G_surjective : Surjective (α := ι →₀ R) (β := M) (⇑G : (a : ι →₀ R) → M)
Tactic: have G_surjective : Surjective G := by
    apply LinearMap.range_eq_top.mp
    apply top_le_iff.mp
    rw [← hm]
    apply Submodule.span_le.mpr
    rintro _ ⟨i, rfl⟩
    use Finsupp.single i 1, G_basis_eq i
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
G_surjective : Surjective (α := ι →₀ R) (β := M) (⇑G : (a : ι →₀ R) → M)
⊢ VanishesTrivially R m n
have hen : let en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i;
en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
Tactic: set en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ n i with hen
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
G_surjective : Surjective (α := ι →₀ R) (β := M) (⇑G : (a : ι →₀ R) → M)
en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
⊢ VanishesTrivially R m n
have en_mem_ker : Membership.mem (γ := Submodule R ((ι →₀ R) ⊗[R] N)) (ker (rTensor N G)) en
Tactic: have en_mem_ker : en ∈ ker (rTensor N G) := by simp [hen, G_basis_eq, hmn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
G_surjective : Surjective (α := ι →₀ R) (β := M) (⇑G : (a : ι →₀ R) → M)
en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : Membership.mem (γ := Submodule R ((ι →₀ R) ⊗[R] N)) (ker (rTensor N G)) en
⊢ VanishesTrivially R m n
have exact_ker_subtype : Exact (M := ↥G.ker) (N := ι →₀ R) (P := M) (⇑G.ker.subtype : (a : ↥G.ker) → ι →₀ R) (⇑G : (a : ι →₀ R) → M)
Tactic: have exact_ker_subtype : Exact (ker G).subtype G := G.exact_subtype_ker_map
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
G_surjective : Surjective (α := ι →₀ R) (β := M) (⇑G : (a : ι →₀ R) → M)
en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : Membership.mem (γ := Submodule R ((ι →₀ R) ⊗[R] N)) (ker (rTensor N G)) en
exact_ker_subtype :
  Exact (M := ↥G.ker) (N := ι →₀ R) (P := M) (⇑G.ker.subtype : (a : ↥G.ker) → ι →₀ R) (⇑G : (a : ι →₀ R) → M)
⊢ VanishesTrivially R m n
have exact_rTensor_ker_subtype : Exact (M := ↥G.ker ⊗[R] N) (N := (ι →₀ R) ⊗[R] N) (P := M ⊗[R] N)
  (⇑(rTensor N G.ker.subtype) : (a : ↥G.ker ⊗[R] N) → (ι →₀ R) ⊗[R] N)
  (⇑(rTensor N G) : (a : (ι →₀ R) ⊗[R] N) → M ⊗[R] N)
Tactic: have exact_rTensor_ker_subtype : Exact (rTensor N (ker G).subtype) (rTensor N G) :=
    rTensor_exact (M := ↥(ker G)) N exact_ker_subtype G_surjective