awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)
hn : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] (ι →₀ R) := LinearMap.rTensor (ι →₀ R) (Finsupp.linearCombination R m)
i2 : ↥M ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := ↥M ⊗[R] (ι →₀ R))
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → ↥M ⊗[R] (ι →₀ R))
h2 : Function.Injective (α := ↥M ⊗[R] (ι →₀ R)) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : ↥M ⊗[R] (ι →₀ R)) → ↥M ⊗[R] ↥N)
h : Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)
⊢ Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S)
have this : i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
Tactic: have : i = Finsupp.linearCombination R fun i ↦ (m i.1).1 * (n i.2).1 := by
    ext x
    simp [i, i0, i1, i2, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥M
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)
hn : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] (ι →₀ R) := LinearMap.rTensor (ι →₀ R) (Finsupp.linearCombination R m)
i2 : ↥M ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := ↥M ⊗[R] (ι →₀ R))
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → ↥M ⊗[R] (ι →₀ R))
h2 : Function.Injective (α := ↥M ⊗[R] (ι →₀ R)) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : ↥M ⊗[R] (ι →₀ R)) → ↥M ⊗[R] ↥N)
h : Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)
this : i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
⊢ Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S)
have rwa : ∀
  (h :
    Function.Injective (α := κ × ι →₀ R) (β := S)
      (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S))
  (this : i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)),
  Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S)
Tactic: rwa [this] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
⊢ LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
have hm₁ : Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)
Tactic: rw [LinearIndependent] at hm hn ⊢
Cleared hypotheses: hm, hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
hm₁ : Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)
⊢ LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
have hn₁ : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
Tactic: rw [LinearIndependent] at hm hn ⊢
Cleared hypotheses: hm, hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)
hn : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
⊢ Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S)
have h1 : Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := (κ →₀ R) ⊗[R] ↥N)
  (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → (κ →₀ R) ⊗[R] ↥N)
Tactic: have h1 : Function.Injective i1 := Module.Flat.lTensor_preserves_injective_linearMap _ hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)
hn : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := (κ →₀ R) ⊗[R] ↥N)
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → (κ →₀ R) ⊗[R] ↥N)
⊢ Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S)
have h2 : Function.Injective (α := (κ →₀ R) ⊗[R] ↥N) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : (κ →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N)
Tactic: have h2 : Function.Injective i2 := Module.Flat.rTensor_preserves_injective_linearMap _ hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)
hn : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := (κ →₀ R) ⊗[R] ↥N)
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → (κ →₀ R) ⊗[R] ↥N)
h2 : Function.Injective (α := (κ →₀ R) ⊗[R] ↥N) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : (κ →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N)
⊢ Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S)
have h : Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)
Tactic: have h : Function.Injective i := H.injective.comp h2 |>.comp h1 |>.comp i0.injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)
hn : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := (κ →₀ R) ⊗[R] ↥N)
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → (κ →₀ R) ⊗[R] ↥N)
h2 : Function.Injective (α := (κ →₀ R) ⊗[R] ↥N) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : (κ →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N)
h : Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)
⊢ i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
have h₁ : ∀ (x : κ × ι),
  Eq.{v + 1} (α := S) ((i ∘ₗ Finsupp.lsingle x : (a : R) → S) 1 : S)
    (((Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) ∘ₗ Finsupp.lsingle x :
          (a : R) → S)
        1 :
      S)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)
hn : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := (κ →₀ R) ⊗[R] ↥N)
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → (κ →₀ R) ⊗[R] ↥N)
h2 : Function.Injective (α := (κ →₀ R) ⊗[R] ↥N) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : (κ →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N)
h : Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)
⊢ Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S)
have this : i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
Tactic: have : i = Finsupp.linearCombination R fun i ↦ (m i.1).1 * (n i.2).1 := by
    ext x
    simp [i, i0, i1, i2, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Flat.{u, v} R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective (α := κ →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : κ →₀ R) → ↥M)
hn : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ (↑i0 : (κ × ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R))
h1 :
  Function.Injective (α := (κ →₀ R) ⊗[R] (ι →₀ R)) (β := (κ →₀ R) ⊗[R] ↥N)
    (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → (κ →₀ R) ⊗[R] ↥N)
h2 : Function.Injective (α := (κ →₀ R) ⊗[R] ↥N) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : (κ →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N)
h : Function.Injective (α := κ × ι →₀ R) (β := S) (⇑i : (a : κ × ι →₀ R) → S)
this : i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
⊢ Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S)
have rwa : ∀
  (h :
    Function.Injective (α := κ × ι →₀ R) (β := S)
      (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S))
  (this : i = Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)),
  Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S)
Tactic: rwa [this] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
⊢ LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
have inl : Flat.{u, v} R ↥M → LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
Tactic: rcases hf with _ | _
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat.{u, v} R ↥M ∨ Flat.{u, v} R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
inl : Flat.{u, v} R ↥M → LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
⊢ LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
have inr : Flat.{u, v} R ↥N → LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)
Tactic: rcases hf with _ | _
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
κ : Type u_1
ι : Type u_2
m : Basis.{u_1, u, v} κ R ↥M
n : Basis.{u_2, u, v} ι R ↥N
H :
  LinearIndependent R (M := S) fun (i : κ × ι) ↦
    HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)
⊢ M.LinearDisjoint N
have H₁ : Function.Injective (α := κ × ι →₀ R) (β := S)
  (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦
        HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)) :
    (a : κ × ι →₀ R) → S)
Tactic: rw [LinearIndependent] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
M' : Submodule R S
h : M' ≤ M
inst_3 : Flat.{u, v} R ↥N
i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)
⊢ M'.LinearDisjoint N
have hi : Function.Injective (α := ↥M' ⊗[R] ↥N) (β := S) (⇑i : (a : ↥M' ⊗[R] ↥N) → S)
Tactic: have hi : Function.Injective i := H.injective.comp <|
    Module.Flat.rTensor_preserves_injective_linearMap _ <| inclusion_injective h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
M' : Submodule R S
h : M' ≤ M
inst_3 : Flat.{u, v} R ↥N
i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)
hi : Function.Injective (α := ↥M' ⊗[R] ↥N) (β := S) (⇑i : (a : ↥M' ⊗[R] ↥N) → S)
⊢ i = M'.mulMap N
have a : ∀ (x : ↥M') (x_1 : ↥N),
  Eq (α := S)
    (((((TensorProduct.AlgebraTensorModule.curry i : ↥M' →ₗ[R] ↥N →ₗ[R] S) : (a : ↥M') → ↥N →ₗ[R] S) x : ↥N →ₗ[R] S) :
          (a : ↥N) → S)
        x_1 :
      S)
    (((((TensorProduct.AlgebraTensorModule.curry (M'.mulMap N) : ↥M' →ₗ[R] ↥N →ₗ[R] S) : (a : ↥M') → ↥N →ₗ[R] S) x :
            ↥N →ₗ[R] S) :
          (a : ↥N) → S)
        x_1 :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
M' : Submodule R S
h : M' ≤ M
inst_3 : Flat.{u, v} R ↥N
i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)
hi : Function.Injective (α := ↥M' ⊗[R] ↥N) (β := S) (⇑i : (a : ↥M' ⊗[R] ↥N) → S)
⊢ M'.LinearDisjoint N
have this : i = M'.mulMap N
Tactic: have : i = mulMap M' N := by ext; simp [i]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
N' : Submodule R S
h : N' ≤ N
inst_3 : Flat.{u, v} R ↥M
i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)
⊢ M.LinearDisjoint N'
have hi : Function.Injective (α := ↥M ⊗[R] ↥N') (β := S) (⇑i : (a : ↥M ⊗[R] ↥N') → S)
Tactic: have hi : Function.Injective i := H.injective.comp <|
    Module.Flat.lTensor_preserves_injective_linearMap _ <| inclusion_injective h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
N' : Submodule R S
h : N' ≤ N
inst_3 : Flat.{u, v} R ↥M
i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)
hi : Function.Injective (α := ↥M ⊗[R] ↥N') (β := S) (⇑i : (a : ↥M ⊗[R] ↥N') → S)
⊢ i = M.mulMap N'
have a : ∀ (x : ↥M) (x_1 : ↥N'),
  Eq (α := S)
    (((((TensorProduct.AlgebraTensorModule.curry i : ↥M →ₗ[R] ↥N' →ₗ[R] S) : (a : ↥M) → ↥N' →ₗ[R] S) x : ↥N' →ₗ[R] S) :
          (a : ↥N') → S)
        x_1 :
      S)
    (((((TensorProduct.AlgebraTensorModule.curry (M.mulMap N') : ↥M →ₗ[R] ↥N' →ₗ[R] S) : (a : ↥M) → ↥N' →ₗ[R] S) x :
            ↥N' →ₗ[R] S) :
          (a : ↥N') → S)
        x_1 :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
N' : Submodule R S
h : N' ≤ N
inst_3 : Flat.{u, v} R ↥M
i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)
hi : Function.Injective (α := ↥M ⊗[R] ↥N') (β := S) (⇑i : (a : ↥M ⊗[R] ↥N') → S)
⊢ M.LinearDisjoint N'
have this : i = M.mulMap N'
Tactic: have : i = mulMap M N' := by ext; simp [i]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
⊢ False
have hn : LinearIndependent R n
Tactic: have hn : LinearIndependent R n := h.map' _ (ker_inclusion _ _ _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
⊢ False
have hm : Eq (α := S) ((M.mulRightMap n : (a : Fin 2 →₀ ↥M) → S) m : S) (0 : S)
Tactic: have hm : mulRightMap M n m = 0 := by simp [m, n, show _ * _ = _ * _ from hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
hm : Eq (α := S) ((M.mulRightMap n : (a : Fin 2 →₀ ↥M) → S) m : S) (0 : S)
⊢ False
have hm₁ : m = 0
Tactic: rw [← LinearMap.mem_ker, H.linearIndependent_right_of_flat hn, mem_bot] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
hm : m = 0
⊢ False
have hm₁ : Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) sorry = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) sorry = 0
Tactic: simp only [Fin.isValue, sub_eq_zero, Finsupp.single_eq_single_iff, zero_ne_one, Subtype.mk.injEq,
    SetLike.coe_eq_coe, false_and, false_or, m] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst_3 : Nontrivial R
inst_4 : Flat.{u, v} R ↥M
a b : ↥(M ⊓ N)
hc : Commute (↑a : S) (↑b : S)
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := (⇑(inclusion ⋯) : (a : ↥(M ⊓ N)) → ↥N) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M :=
  HSub.hSub (α := Fin 2 →₀ ↥M) (Finsupp.single 0 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯))
    (Finsupp.single 1 (Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯))
hm : Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑b : S) ⋯ = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) ⋯ = 0
⊢ False
have hm₁ : b = 0 ∧ Subtype.mk (p := fun (x : S) ↦ x ∈ M) (↑a : S) sorry = 0
Tactic: rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hm
Cleared hypotheses: hm