awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
⊢ n₁ = n₂ ∧ s₁ = s₂
have obtain : ∀ (n₀ : End K V) (hn₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] n₀) (s₀ : End K V)
  (hs₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] s₀) (hn₀_nil : IsNilpotent n₀)
  (hs₀_ss : s₀.IsSemisimple) (h₀ : n₁ + s₁ = n₀ + s₀), n₁ = n₂ ∧ s₁ = s₂
Tactic: obtain ⟨n₀, hn₀, s₀, hs₀, hn₀_nil, hs₀_ss, h₀⟩ := (n₁ + s₁).exists_isNilpotent_isSemisimple
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
n₀ : End K V
hn₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] n₀
s₀ : End K V
hs₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] s₀
hn₀_nil : IsNilpotent n₀
hs₀_ss : s₀.IsSemisimple
h₀ : n₁ + s₁ = n₀ + s₀
⊢ n₁ = n₂ ∧ s₁ = s₂
have suffices : ∀ {n s : End K V}, IsNilpotent n → s.IsSemisimple → Commute n s → n₁ + s₁ = n + s → s = s₀
Tactic: suffices ∀ {n s}, IsNilpotent n → s.IsSemisimple → Commute n s → n₁ + s₁ = n + s → s = s₀ by grind
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
n₀ : End K V
hn₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] n₀
s₀ : End K V
hs₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] s₀
hn₀_nil : IsNilpotent n₀
hs₀_ss : s₀.IsSemisimple
h₀ : n₁ + s₁ = n₀ + s₀
n s : End K V
hn : IsNilpotent n
hs : s.IsSemisimple
hc : Commute n s
heq : n₁ + s₁ = n + s
⊢ s = s₀
have hsf : Commute s (n₁ + s₁)
Tactic: have hsf : Commute s (n₁ + s₁) := heq ▸ hc.symm.add_right (Commute.refl s)
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
n₀ : End K V
hn₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] n₀
s₀ : End K V
hs₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] s₀
hn₀_nil : IsNilpotent n₀
hs₀_ss : s₀.IsSemisimple
h₀ : n₁ + s₁ = n₀ + s₀
n s : End K V
hn : IsNilpotent n
hs : s.IsSemisimple
hc : Commute n s
heq : n₁ + s₁ = n + s
hsf : Commute s (n₁ + s₁)
⊢ s = s₀
have hnf : Commute n (n₁ + s₁)
Tactic: have hnf : Commute n (n₁ + s₁) := heq ▸ (Commute.refl n).add_right hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
n₀ : End K V
hn₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] n₀
s₀ : End K V
hs₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] s₀
hn₀_nil : IsNilpotent n₀
hs₀_ss : s₀.IsSemisimple
h₀ : n₁ + s₁ = n₀ + s₀
n s : End K V
hn : IsNilpotent n
hs : s.IsSemisimple
hc : Commute n s
heq : n₁ + s₁ = n + s
hsf : Commute s (n₁ + s₁)
hnf : Commute n (n₁ + s₁)
⊢ IsNilpotent (s - s₀)
have rw : IsNilpotent (n₀ - n)
Tactic: rw [show s - s₀ = n₀ - n from by grind]
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
n₀ : End K V
hn₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] n₀
s₀ : End K V
hs₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] s₀
hn₀_nil : IsNilpotent n₀
hs₀_ss : s₀.IsSemisimple
h₀ : n₁ + s₁ = n₀ + s₀
n s : End K V
hn : IsNilpotent n
hs : s.IsSemisimple
hc : Commute n s
heq : n₁ + s₁ = n + s
hsf : Commute s (n₁ + s₁)
hnf : Commute n (n₁ + s₁)
⊢ s = s₀
have hnil : IsNilpotent (s - s₀)
Tactic: have hnil : IsNilpotent (s - s₀) := by
    rw [show s - s₀ = n₀ - n from by grind]
    exact (commute_of_mem_adjoin_singleton_of_commute hn₀ hnf).symm.isNilpotent_sub hn₀_nil hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.JordanChevalley (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
inst_4 : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
n₀ : End K V
hn₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] n₀
s₀ : End K V
hs₀ : Membership.mem (γ := Subalgebra K (End K V)) K[n₁ + s₁] s₀
hn₀_nil : IsNilpotent n₀
hs₀_ss : s₀.IsSemisimple
h₀ : n₁ + s₁ = n₀ + s₀
n s : End K V
hn : IsNilpotent n
hs : s.IsSemisimple
hc : Commute n s
heq : n₁ + s₁ = n + s
hsf : Commute s (n₁ + s₁)
hnf : Commute n (n₁ + s₁)
hnil : IsNilpotent (s - s₀)
⊢ s = s₀
have hss : (s - s₀).IsSemisimple
Tactic: have hss : (s - s₀).IsSemisimple :=
    hs.sub_of_commute (commute_of_mem_adjoin_singleton_of_commute hs₀ hsf) hs₀_ss
-- Lean 4 proof step from Mathlib.LinearAlgebra.LeftExact (goal)
Goal:
R : Type u_1
inst : CommRing R
M1 : Type u_2
M2 : Type u_3
M3 : Type u_4
N : Type u_5
inst_1 : AddCommGroup M1
inst_2 : AddCommGroup M2
inst_3 : AddCommGroup M3
inst_4 : AddCommGroup N
inst_5 : Module R M1
inst_6 : Module R M2
inst_7 : Module R M3
inst_8 : Module R N
f : M1 →ₗ[R] M2
g : M2 →ₗ[R] M3
exac : Function.Exact.{u_2, u_3, u_4} (M := M1) (N := M2) (P := M3) (⇑f : (a : M1) → M2) (⇑g : (a : M2) → M3)
surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M2) (β := M3) (⇑g : (a : M2) → M3)
h : M2 →ₗ[R] N
⊢ Eq (α := M1 →ₗ[R] N) ((lcomp R N f : (a : M2 →ₗ[R] N) → M1 →ₗ[R] N) h : M1 →ₗ[R] N) (0 : M1 →ₗ[R] N) ↔
    Membership.mem (γ := Set (M2 →ₗ[R] N))
      (Set.range (ι := M3 →ₗ[R] N) (⇑(lcomp R N g) : (a : M3 →ₗ[R] N) → M2 →ₗ[R] N)) h
have simp : h ∘ₗ f = 0 ↔ ∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h
Tactic: simp only [LinearMap.lcomp_apply', Set.mem_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LeftExact (goal)
Goal:
R : Type u_1
inst : CommRing R
M1 : Type u_2
M2 : Type u_3
M3 : Type u_4
N : Type u_5
inst_1 : AddCommGroup M1
inst_2 : AddCommGroup M2
inst_3 : AddCommGroup M3
inst_4 : AddCommGroup N
inst_5 : Module R M1
inst_6 : Module R M2
inst_7 : Module R M3
inst_8 : Module R N
f : M1 →ₗ[R] M2
g : M2 →ₗ[R] M3
exac : Function.Exact.{u_2, u_3, u_4} (M := M1) (N := M2) (P := M3) (⇑f : (a : M1) → M2) (⇑g : (a : M2) → M3)
surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M2) (β := M3) (⇑g : (a : M2) → M3)
h : M2 →ₗ[R] N
⊢ h ∘ₗ f = 0 ↔ ∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h
have refine_1 : ∀ (hh : h ∘ₗ f = 0), ∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h
Tactic: refine ⟨fun hh ↦ ?_, fun ⟨y, hy⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LeftExact (goal)
Goal:
R : Type u_1
inst : CommRing R
M1 : Type u_2
M2 : Type u_3
M3 : Type u_4
N : Type u_5
inst_1 : AddCommGroup M1
inst_2 : AddCommGroup M2
inst_3 : AddCommGroup M3
inst_4 : AddCommGroup N
inst_5 : Module R M1
inst_6 : Module R M2
inst_7 : Module R M3
inst_8 : Module R N
f : M1 →ₗ[R] M2
g : M2 →ₗ[R] M3
exac : Function.Exact.{u_2, u_3, u_4} (M := M1) (N := M2) (P := M3) (⇑f : (a : M1) → M2) (⇑g : (a : M2) → M3)
surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M2) (β := M3) (⇑g : (a : M2) → M3)
h : M2 →ₗ[R] N
refine_1 : ∀ (hh : h ∘ₗ f = 0), ∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h
⊢ h ∘ₗ f = 0 ↔ ∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h
have refine_2 : (∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h) → ∀ (y : M3 →ₗ[R] N) (hy : y ∘ₗ g = h), h ∘ₗ f = 0
Tactic: refine ⟨fun hh ↦ ?_, fun ⟨y, hy⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LeftExact (goal)
Goal:
R : Type u_1
inst : CommRing R
M1 : Type u_2
M2 : Type u_3
M3 : Type u_4
N : Type u_5
inst_1 : AddCommGroup M1
inst_2 : AddCommGroup M2
inst_3 : AddCommGroup M3
inst_4 : AddCommGroup N
inst_5 : Module R M1
inst_6 : Module R M2
inst_7 : Module R M3
inst_8 : Module R N
f : M1 →ₗ[R] M2
g : M2 →ₗ[R] M3
exac : Function.Exact.{u_2, u_3, u_4} (M := M1) (N := M2) (P := M3) (⇑f : (a : M1) → M2) (⇑g : (a : M2) → M3)
surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M2) (β := M3) (⇑g : (a : M2) → M3)
h : M2 →ₗ[R] N
hh : h ∘ₗ f = 0
⊢ ∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h
have h₁ : (f.range.liftQ h sorry ∘ₗ (↑(exac.linearEquivOfSurjective surj).symm : M3 →ₗ[R] M2 ⧸ f.range)) ∘ₗ g = h
Tactic: use ((LinearMap.range f).liftQ h (LinearMap.range_le_ker_iff.mpr hh)).comp
      (exac.linearEquivOfSurjective surj).symm.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.LeftExact (goal)
Goal:
R : Type u_1
inst : CommRing R
M1 : Type u_2
M2 : Type u_3
M3 : Type u_4
N : Type u_5
inst_1 : AddCommGroup M1
inst_2 : AddCommGroup M2
inst_3 : AddCommGroup M3
inst_4 : AddCommGroup N
inst_5 : Module R M1
inst_6 : Module R M2
inst_7 : Module R M3
inst_8 : Module R N
f : M1 →ₗ[R] M2
g : M2 →ₗ[R] M3
exac : Function.Exact.{u_2, u_3, u_4} (M := M1) (N := M2) (P := M3) (⇑f : (a : M1) → M2) (⇑g : (a : M2) → M3)
surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M2) (β := M3) (⇑g : (a : M2) → M3)
h : M2 →ₗ[R] N
hh : h ∘ₗ f = 0
⊢ (f.range.liftQ h ⋯ ∘ₗ (↑(exac.linearEquivOfSurjective surj).symm : M3 →ₗ[R] M2 ⧸ f.range)) ∘ₗ g = h
have h₁ : ∀ (x : M2),
  Eq.{u_5 + 1} (α := N)
    (((f.range.liftQ h sorry ∘ₗ (↑(exac.linearEquivOfSurjective surj).symm : M3 →ₗ[R] M2 ⧸ f.range)) ∘ₗ g : (a : M2) → N)
        x :
      N)
    ((h : (a : M2) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.LeftExact (goal)
Goal:
R : Type u_1
inst : CommRing R
M1 : Type u_2
M2 : Type u_3
M3 : Type u_4
N : Type u_5
inst_1 : AddCommGroup M1
inst_2 : AddCommGroup M2
inst_3 : AddCommGroup M3
inst_4 : AddCommGroup N
inst_5 : Module R M1
inst_6 : Module R M2
inst_7 : Module R M3
inst_8 : Module R N
f : M1 →ₗ[R] M2
g : M2 →ₗ[R] M3
exac : Function.Exact.{u_2, u_3, u_4} (M := M1) (N := M2) (P := M3) (⇑f : (a : M1) → M2) (⇑g : (a : M2) → M3)
surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M2) (β := M3) (⇑g : (a : M2) → M3)
h : M2 →ₗ[R] N
h_1 : ∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h
y : M3 →ₗ[R] N
hy : y ∘ₗ g = h
⊢ h ∘ₗ f = 0
have refine_2 : (y ∘ₗ g) ∘ₗ f = 0
Tactic: rw [← hy, LinearMap.comp_assoc, exac.linearMap_comp_eq_zero, LinearMap.comp_zero y]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LeftExact (goal)
Goal:
R : Type u_1
inst : CommRing R
M1 : Type u_2
M2 : Type u_3
M3 : Type u_4
N : Type u_5
inst_1 : AddCommGroup M1
inst_2 : AddCommGroup M2
inst_3 : AddCommGroup M3
inst_4 : AddCommGroup N
inst_5 : Module R M1
inst_6 : Module R M2
inst_7 : Module R M3
inst_8 : Module R N
f : M1 →ₗ[R] M2
g : M2 →ₗ[R] M3
exac : Function.Exact.{u_2, u_3, u_4} (M := M1) (N := M2) (P := M3) (⇑f : (a : M1) → M2) (⇑g : (a : M2) → M3)
surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M2) (β := M3) (⇑g : (a : M2) → M3)
h : M2 →ₗ[R] N
h_1 : ∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h
y : M3 →ₗ[R] N
hy : y ∘ₗ g = h
refine_2 : (y ∘ₗ g) ∘ₗ f = 0
⊢ h ∘ₗ f = 0
have refine_2₁ : y ∘ₗ g ∘ₗ f = 0
Tactic: rw [← hy, LinearMap.comp_assoc, exac.linearMap_comp_eq_zero, LinearMap.comp_zero y]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LeftExact (goal)
Goal:
R : Type u_1
inst : CommRing R
M1 : Type u_2
M2 : Type u_3
M3 : Type u_4
N : Type u_5
inst_1 : AddCommGroup M1
inst_2 : AddCommGroup M2
inst_3 : AddCommGroup M3
inst_4 : AddCommGroup N
inst_5 : Module R M1
inst_6 : Module R M2
inst_7 : Module R M3
inst_8 : Module R N
f : M1 →ₗ[R] M2
g : M2 →ₗ[R] M3
exac : Function.Exact.{u_2, u_3, u_4} (M := M1) (N := M2) (P := M3) (⇑f : (a : M1) → M2) (⇑g : (a : M2) → M3)
surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M2) (β := M3) (⇑g : (a : M2) → M3)
h : M2 →ₗ[R] N
h_1 : ∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h
y : M3 →ₗ[R] N
hy : y ∘ₗ g = h
refine_2 : (y ∘ₗ g) ∘ₗ f = 0
refine_2₁ : y ∘ₗ g ∘ₗ f = 0
⊢ h ∘ₗ f = 0
have refine_2₂ : Eq (α := M1 →ₗ[R] N) (y ∘ₗ 0) 0
Tactic: rw [← hy, LinearMap.comp_assoc, exac.linearMap_comp_eq_zero, LinearMap.comp_zero y]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LeftExact (goal)
Goal:
R : Type u_1
inst : CommRing R
M1 : Type u_2
M2 : Type u_3
M3 : Type u_4
N : Type u_5
inst_1 : AddCommGroup M1
inst_2 : AddCommGroup M2
inst_3 : AddCommGroup M3
inst_4 : AddCommGroup N
inst_5 : Module R M1
inst_6 : Module R M2
inst_7 : Module R M3
inst_8 : Module R N
f : M1 →ₗ[R] M2
g : M2 →ₗ[R] M3
exac : Function.Exact.{u_2, u_3, u_4} (M := M1) (N := M2) (P := M3) (⇑f : (a : M1) → M2) (⇑g : (a : M2) → M3)
surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M2) (β := M3) (⇑g : (a : M2) → M3)
h : M2 →ₗ[R] N
h_1 : ∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h
y : M3 →ₗ[R] N
hy : y ∘ₗ g = h
refine_2 : (y ∘ₗ g) ∘ₗ f = 0
refine_2₁ : y ∘ₗ g ∘ₗ f = 0
refine_2₂ : Eq (α := M1 →ₗ[R] N) (y ∘ₗ 0) 0
⊢ h ∘ₗ f = 0
have refine_2₃ : Eq (α := M1 →ₗ[R] N) 0 0
Tactic: rw [← hy, LinearMap.comp_assoc, exac.linearMap_comp_eq_zero, LinearMap.comp_zero y]
-- 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.LinearDisjoint N
hc : ∀ (m : ↥M) (n : ↥N), Commute (↑m : S) (↑n : S)
⊢ N.LinearDisjoint M
have rw : Function.Injective (α := ↥N ⊗[R] ↥M) (β := S)
  (⇑(M.mulMap N ∘ₗ (↑(TensorProduct.comm R ↥N ↥M) : ↥N ⊗[R] ↥M →ₗ[R] ↥M ⊗[R] ↥N)) : (a : ↥N ⊗[R] ↥M) → S)
Tactic: rw [linearDisjoint_iff, mulMap_comm_of_commute M N hc]
-- 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.LinearDisjoint N
T : Type w
inst_3 : Semiring T
inst_4 : Algebra R T
f : S →ₐ[R] T
hf : Function.Injective.{v + 1, w + 1} (α := S) (β := T) (⇑f : (a : S) → T)
⊢ Submodule.LinearDisjoint.{u, w} (R := R) (S := T)
    (Submodule.map (σ₁₂ := RingHom.id R)
      (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T) M)
    (Submodule.map (σ₁₂ := RingHom.id R)
      (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T) N)
have rw : ∀ (H : Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)) {T : Type w}
  [inst_5 : Semiring T] [inst_6 : Algebra R T] (f : S →ₐ[R] T)
  (hf : Function.Injective.{v + 1, w + 1} (α := S) (β := T) (⇑f : (a : S) → T)),
  Function.Injective.{w + 1, w + 1} (α :=
    ↥(Submodule.map (σ₁₂ := RingHom.id R)
          (↑f : [inst_7 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
          M) ⊗[R]
      ↥(Submodule.map (σ₁₂ := RingHom.id R)
          (↑f : [inst_7 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
          N))
    (β := T)
    (⇑(mulMap
          (Submodule.map (σ₁₂ := RingHom.id R)
            (↑f : [inst_7 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
            M)
          (Submodule.map (σ₁₂ := RingHom.id R)
            (↑f : [inst_7 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
            N)) :
      (a :
          ↥(Submodule.map
                (↑f :
                  [inst_7 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                M) ⊗[R]
            ↥(Submodule.map
                (↑f :
                  [inst_7 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                N)) →
        T)
Tactic: rw [linearDisjoint_iff] at H ⊢
Cleared hypotheses: H, T, inst_3, inst_4, f, hf
-- 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 : Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
T : Type w
inst_3 : Semiring T
inst_4 : Algebra R T
f : S →ₐ[R] T
hf : Function.Injective.{v + 1, w + 1} (α := S) (β := T) (⇑f : (a : S) → T)
⊢ Function.Injective.{w + 1, w + 1} (α :=
    ↥(Submodule.map (σ₁₂ := RingHom.id R)
          (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
          M) ⊗[R]
      ↥(Submodule.map (σ₁₂ := RingHom.id R)
          (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
          N))
    (β := T)
    (⇑(mulMap
          (Submodule.map (σ₁₂ := RingHom.id R)
            (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
            M)
          (Submodule.map (σ₁₂ := RingHom.id R)
            (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
            N)) :
      (a :
          ↥(Submodule.map
                (↑f :
                  [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                M) ⊗[R]
            ↥(Submodule.map
                (↑f :
                  [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                N)) →
        T)
have this : Function.Injective.{v + 1, w + 1} (α := ↥M ⊗[R] ↥N) (β := T)
  (Function.comp (β := S) (⇑f : (a : S) → T) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S))
Tactic: have := hf.comp H
-- 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
m : Basis.{u_1, u, v} ι R ↥M
H :
  Function.Injective (α := Finsupp.{u_1, v} ι ↥N) (β := S)
    (⇑(mulLeftMap (M := M) N (⇑m : (a : ι) → ↥M)) : (a : ι →₀ ↥N) → S)
⊢ M.LinearDisjoint N
have H₁ : Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
Tactic: simp_rw [mulLeftMap_eq_mulMap_comp, ← Basis.coe_repr_symm,
    ← LinearEquiv.coe_rTensor, LinearEquiv.comp_coe, LinearMap.coe_comp,
    LinearEquiv.coe_coe, EquivLike.injective_comp] at H
Cleared hypotheses: H
-- 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
m : Basis.{u_1, u, v} ι R ↥M
H :
  Function.Injective (α := Finsupp.{u_1, v} ι ↥N) (β := S)
    (⇑(mulLeftMap (M := M) N (⇑m : (a : ι) → ↥M)) : (a : ι →₀ ↥N) → S)
⊢ M.LinearDisjoint N
have H₁ : Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
Tactic: classical simp_rw [mulLeftMap_eq_mulMap_comp, ← Basis.coe_repr_symm,
    ← LinearEquiv.coe_rTensor, LinearEquiv.comp_coe, LinearMap.coe_comp,
    LinearEquiv.coe_coe, EquivLike.injective_comp] at H
Cleared hypotheses: H
-- 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
n : Basis.{u_1, u, v} ι R ↥N
H :
  Function.Injective (α := Finsupp.{u_1, v} ι ↥M) (β := S)
    (⇑(M.mulRightMap (N := N) (⇑n : (a : ι) → ↥N)) : (a : ι →₀ ↥M) → S)
⊢ M.LinearDisjoint N
have H₁ : Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
Tactic: simp_rw [mulRightMap_eq_mulMap_comp, ← Basis.coe_repr_symm,
    ← LinearEquiv.coe_lTensor, LinearEquiv.comp_coe, LinearMap.coe_comp,
    LinearEquiv.coe_coe, EquivLike.injective_comp] at H
Cleared hypotheses: H
-- 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
n : Basis.{u_1, u, v} ι R ↥N
H :
  Function.Injective (α := Finsupp.{u_1, v} ι ↥M) (β := S)
    (⇑(M.mulRightMap (N := N) (⇑n : (a : ι) → ↥N)) : (a : ι →₀ ↥M) → S)
⊢ M.LinearDisjoint N
have H₁ : Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
Tactic: classical simp_rw [mulRightMap_eq_mulMap_comp, ← Basis.coe_repr_symm,
    ← LinearEquiv.coe_lTensor, LinearEquiv.comp_coe, 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
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)
⊢ i =
    Finsupp.linearCombination R fun (i : κ × ι) ↦
      HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥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 : κ × ι) ↦
              HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥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 : 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)
⊢ M.LinearDisjoint N
have this : i =
  Finsupp.linearCombination R fun (i : κ × ι) ↦
    HMul.hMul (α := S) (↑((m : (a : κ) → ↥M) i.1) : S) (↑((n : (a : ι) → ↥N) i.2) : S)
Tactic: have : i = Finsupp.linearCombination R fun i : κ × ι ↦ (m i.1 * n i.2 : S) := by
    ext x
    simp [i, i0, i1, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]