awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring 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 :
  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)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := LinearEquiv.symm (finsuppTensorFinsupp' R κ ι)
i1 : ↥M ⊗[R] ↥N ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := TensorProduct.congr m.repr n.repr
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ (↑(i0 ≪≫ₗ i1.symm) : (κ × ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N)
this :
  i =
    Finsupp.linearCombination R fun (i : κ × ι) ↦
      HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)
⊢ M.LinearDisjoint N
have H₁ : Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
Tactic: simp_rw [← this, i, LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.injective_comp] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
N : Submodule R S
⊢ Submodule.LinearDisjoint 1 N
have rw : Function.Injective (α := ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) ⊗[R] ↥N)
  (β := S)
  (⇑(N.subtype ∘ₗ (↑N.lTensorOne : ↥⊥ ⊗[R] ↥N →ₗ[R] ↥N)) :
    (a : ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥) ⊗[R] ↥N) → S)
Tactic: rw [linearDisjoint_iff, ← Algebra.toSubmodule_bot, mulMap_one_left_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Submodule R S
⊢ M.LinearDisjoint 1
have rw : Function.Injective (α := ↥M ⊗[R] ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S))
  (β := S)
  (⇑(M.subtype ∘ₗ (↑M.rTensorOne : ↥M ⊗[R] ↥⊥ →ₗ[R] ↥M)) :
    (a : ↥M ⊗[R] ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥)) → S)
Tactic: rw [linearDisjoint_iff, ← Algebra.toSubmodule_bot, mulMap_one_right_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
⊢ x = y
have obtain : ∀ (M' : Submodule R S) (hM : M' ≤ M) (hFG : Module.Finite.{u, v} R ↥M')
  (h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))), x = y
Tactic: obtain ⟨M', hM, hFG, h⟩ :=
    TensorProduct.exists_finite_submodule_left_of_setFinite' {x, y} (Set.toFinite _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : Module.Finite.{u, v} R ↥M'
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
⊢ x = y
have hFG₁ : M'.FG
Tactic: rw [Module.Finite.iff_fg] at hFG
Cleared hypotheses: hFG, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
⊢ x = y
have obtain : ∀ (x' : ↥M' ⊗[R] ↥N) (hx' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' = x), x = y
Tactic: obtain ⟨x', hx'⟩ := h (show x ∈ {x, y} by simp)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' = x
⊢ x = y
have obtain : ∀ (y' : ↥M' ⊗[R] ↥N) (hy' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) y' = y), x = y
Tactic: obtain ⟨y', hy'⟩ := h (show y ∈ {x, y} by simp)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' = x
y' : ↥M' ⊗[R] ↥N
hy' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) y' = y
⊢ x = y
have rw : Eq (α := ↥M ⊗[R] ↥N) ((LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' : ↥M ⊗[R] ↥N)
  ((LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) y' : ↥M ⊗[R] ↥N)
Tactic: rw [← hx', ← hy']
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM))) : Set (↥M ⊗[R] ↥N))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' = x
y' : ↥M' ⊗[R] ↥N
hy' : (LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) y' = y
⊢ Eq (α := ↥M ⊗[R] ↥N) ((LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) x' : ↥M ⊗[R] ↥N)
    ((LinearMap.rTensor (↥N) (inclusion hM) : (a : ↥M' ⊗[R] ↥N) → ↥M ⊗[R] ↥N) y' : ↥M ⊗[R] ↥N)
have h₁ : x' = y'
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
⊢ x = y
have obtain : ∀ (N' : Submodule R S) (hN : N' ≤ N) (hFG : Module.Finite.{u, v} R ↥N')
  (h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))), x = y
Tactic: obtain ⟨N', hN, hFG, h⟩ :=
    TensorProduct.exists_finite_submodule_right_of_setFinite' {x, y} (Set.toFinite _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : Module.Finite.{u, v} R ↥N'
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
⊢ x = y
have hFG₁ : N'.FG
Tactic: rw [Module.Finite.iff_fg] at hFG
Cleared hypotheses: hFG, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
⊢ x = y
have obtain : ∀ (x' : ↥M ⊗[R] ↥N') (hx' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' = x), x = y
Tactic: obtain ⟨x', hx'⟩ := h (show x ∈ {x, y} by simp)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' = x
⊢ x = y
have obtain : ∀ (y' : ↥M ⊗[R] ↥N') (hy' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) y' = y), x = y
Tactic: obtain ⟨y', hy'⟩ := h (show y ∈ {x, y} by simp)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) y' = y
⊢ x = y
have rw : Eq (α := ↥M ⊗[R] ↥N) ((LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' : ↥M ⊗[R] ↥N)
  ((LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) y' : ↥M ⊗[R] ↥N)
Tactic: rw [← hx', ← hy']
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : Eq (α := S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) x : S) ((M.mulMap N : (a : ↥M ⊗[R] ↥N) → S) y : S)
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN))) : Set (↥M ⊗[R] ↥N))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) y' = y
⊢ Eq (α := ↥M ⊗[R] ↥N) ((LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) x' : ↥M ⊗[R] ↥N)
    ((LinearMap.lTensor (↥M) (inclusion hN) : (a : ↥M ⊗[R] ↥N') → ↥M ⊗[R] ↥N) y' : ↥M ⊗[R] ↥N)
have h₁ : x' = y'
Tactic: congr
-- 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
m : ι → ↥M
hm : LinearIndependent R m
⊢ (mulLeftMap N m).ker = ⊥
have refine : Function.Injective (α := Finsupp.{u_1, v} ι ↥N) (β := S) (⇑(mulLeftMap N m) : (a : ι →₀ ↥N) → S)
Tactic: refine LinearMap.ker_eq_bot_of_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
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective (α := Finsupp.{u_1, v} ι ↥N) (β := S) (⇑(mulLeftMap N m) : (a : ι →₀ ↥N) → S)
have simp_rw : Function.Injective (α := (ι →₀ R) ⊗[R] ↥N) (β := S)
  (Function.comp (β := ↥M ⊗[R] ↥N) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
    (⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)) : (a : (ι →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N))
Tactic: simp_rw [mulLeftMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe,
    ← Function.comp_assoc, EquivLike.injective_comp]
-- 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
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective (α := Finsupp.{u_1, v} ι ↥N) (β := S) (⇑(mulLeftMap N m) : (a : ι →₀ ↥N) → S)
have classical : Function.Injective (α := (ι →₀ R) ⊗[R] ↥N) (β := S)
  (Function.comp (β := ↥M ⊗[R] ↥N) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
    (⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)) : (a : (ι →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N))
Tactic: classical simp_rw [mulLeftMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe,
    ← Function.comp_assoc, EquivLike.injective_comp]
-- 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
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective (α := (ι →₀ R) ⊗[R] ↥N) (β := S)
    (Function.comp (β := ↥M ⊗[R] ↥N) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
      (⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)) : (a : (ι →₀ R) ⊗[R] ↥N) → ↥M ⊗[R] ↥N))
have hm₁ : Function.Injective (α := ι →₀ R) (β := ↥M) (⇑(Finsupp.linearCombination R m) : (a : ι →₀ R) → ↥M)
Tactic: rw [LinearIndependent] at hm
Cleared hypotheses: hm
-- 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
n : ι → ↥N
hn : LinearIndependent R n
⊢ (M.mulRightMap n).ker = ⊥
have refine : Function.Injective (α := Finsupp.{u_1, v} ι ↥M) (β := S) (⇑(M.mulRightMap n) : (a : ι →₀ ↥M) → S)
Tactic: refine LinearMap.ker_eq_bot_of_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 ↥M
ι : Type u_1
n : ι → ↥N
hn : LinearIndependent R n
⊢ Function.Injective (α := Finsupp.{u_1, v} ι ↥M) (β := S) (⇑(M.mulRightMap n) : (a : ι →₀ ↥M) → S)
have simp_rw : Function.Injective (α := ↥M ⊗[R] (ι →₀ R)) (β := S)
  (Function.comp (β := ↥M ⊗[R] ↥N) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
    (⇑(LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)) : (a : ↥M ⊗[R] (ι →₀ R)) → ↥M ⊗[R] ↥N))
Tactic: simp_rw [mulRightMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe,
    ← Function.comp_assoc, EquivLike.injective_comp]
-- 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
n : ι → ↥N
hn : LinearIndependent R n
⊢ Function.Injective (α := Finsupp.{u_1, v} ι ↥M) (β := S) (⇑(M.mulRightMap n) : (a : ι →₀ ↥M) → S)
have classical : Function.Injective (α := ↥M ⊗[R] (ι →₀ R)) (β := S)
  (Function.comp (β := ↥M ⊗[R] ↥N) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
    (⇑(LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)) : (a : ↥M ⊗[R] (ι →₀ R)) → ↥M ⊗[R] ↥N))
Tactic: classical simp_rw [mulRightMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe,
    ← Function.comp_assoc, EquivLike.injective_comp]
-- 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
n : ι → ↥N
hn : LinearIndependent R n
⊢ Function.Injective (α := ↥M ⊗[R] (ι →₀ R)) (β := S)
    (Function.comp (β := ↥M ⊗[R] ↥N) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
      (⇑(LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)) : (a : ↥M ⊗[R] (ι →₀ R)) → ↥M ⊗[R] ↥N))
have hn₁ : Function.Injective (α := ι →₀ R) (β := ↥N) (⇑(Finsupp.linearCombination R n) : (a : ι →₀ R) → ↥N)
Tactic: rw [LinearIndependent] at hn
Cleared hypotheses: 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 ↥M
κ : 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 ↥M
κ : 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 ↥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))
⊢ 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)) (β := ↥M ⊗[R] (ι →₀ R))
  (⇑i1 : (a : (κ →₀ R) ⊗[R] (ι →₀ R)) → ↥M ⊗[R] (ι →₀ R))
Tactic: have h1 : Function.Injective i1 := 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 ↥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))
⊢ Function.Injective (α := κ × ι →₀ R) (β := S)
    (⇑(Finsupp.linearCombination R fun (i : κ × ι) ↦ (↑(m i.1) : S) * (↑(n i.2) : S)) : (a : κ × ι →₀ R) → S)
have h2 : Function.Injective (α := ↥M ⊗[R] (ι →₀ R)) (β := ↥M ⊗[R] ↥N) (⇑i2 : (a : ↥M ⊗[R] (ι →₀ R)) → ↥M ⊗[R] ↥N)
Tactic: have h2 : Function.Injective i2 := 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 ↥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)
⊢ 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 ↥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)
⊢ 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