awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.JordanChevalley
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
⊢ Commute s (n₁ + s₁)

Tactic:
have hsf : Commute s (n₁ + s₁) := heq ▸ hc.symm.add_right (Commute.refl s)
-- Module: Mathlib.LinearAlgebra.JordanChevalley
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₁)
⊢ Commute n (n₁ + s₁)

Tactic:
have hnf : Commute n (n₁ + s₁) := heq ▸ (Commute.refl n).add_right hc
-- Module: Mathlib.LinearAlgebra.JordanChevalley
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₀ = n₀ - n

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.JordanChevalley
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₁)
rw : IsNilpotent (n₀ - n)
⊢ IsNilpotent (s - s₀)

Tactic:
rw [show s - s₀ = n₀ - n from by grind]
-- Module: Mathlib.LinearAlgebra.JordanChevalley
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 (n₀ - n)

Tactic:
(commute_of_mem_adjoin_singleton_of_commute hn₀ hnf).symm.isNilpotent_sub hn₀_nil hn

Premises used: Algebra.commute_of_mem_adjoin_singleton_of_commute, Commute.symm, Commute.isNilpotent_sub
-- Module: Mathlib.LinearAlgebra.JordanChevalley
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 (n₀ - n)

Tactic:
exact (commute_of_mem_adjoin_singleton_of_commute hn₀ hnf).symm.isNilpotent_sub hn₀_nil hn

Premises used: Algebra.commute_of_mem_adjoin_singleton_of_commute, Commute.symm, Commute.isNilpotent_sub
-- Module: Mathlib.LinearAlgebra.JordanChevalley
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₀)

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
-- Module: Mathlib.LinearAlgebra.JordanChevalley
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₀).IsSemisimple

Tactic:
have hss : (s - s₀).IsSemisimple :=
    hs.sub_of_commute (commute_of_mem_adjoin_singleton_of_commute hs₀ hsf) hs₀_ss
-- Module: Mathlib.LinearAlgebra.JordanChevalley
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₀)
hss : (s - s₀).IsSemisimple
⊢ s = s₀

Tactic:
grind [eq_zero_of_isNilpotent_isSemisimple hnil hss]

Premises used: Module.End.eq_zero_of_isNilpotent_isSemisimple
-- Module: Mathlib.LinearAlgebra.LeftExact
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
simp : h ∘ₗ f = 0 ↔ ∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h
⊢ 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

Tactic:
simp only [LinearMap.lcomp_apply', Set.mem_range]

Premises used: Set.mem_range, LinearMap.lcomp_apply'
-- Module: Mathlib.LinearAlgebra.LeftExact
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

Tactic:
⟨fun hh ↦ ?_, fun ⟨y, hy⟩ ↦ ?_⟩

Premises used: LinearMap.comp, Iff.intro, OfNat.ofNat, Eq, _private.0.LinearMap.exact_lcomp_of_exact_of_surjective.match_1
-- Module: Mathlib.LinearAlgebra.LeftExact
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
refine_2 : (∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h) → ∀ (y : M3 →ₗ[R] N) (hy : y ∘ₗ g = h), h ∘ₗ f = 0
⊢ h ∘ₗ f = 0 ↔ ∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h

Tactic:
refine ⟨fun hh ↦ ?_, fun ⟨y, hy⟩ ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.LeftExact
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
h₁ : (f.range.liftQ h ⋯ ∘ₗ (↑(exac.linearEquivOfSurjective surj).symm : M3 →ₗ[R] M2 ⧸ f.range)) ∘ₗ g = h
⊢ ∃ (y : M3 →ₗ[R] N), y ∘ₗ g = h

Tactic:
use ((LinearMap.range f).liftQ h (LinearMap.range_le_ker_iff.mpr hh)).comp
      (exac.linearEquivOfSurjective surj).symm.toLinearMap

Premises used: Iff.mpr, LinearEquiv.symm, LinearMap.range, Function.Exact.linearEquivOfSurjective, LinearMap.comp, LinearEquiv.toLinearMap, Submodule.liftQ, LinearMap.range_le_ker_iff
-- Module: Mathlib.LinearAlgebra.LeftExact
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
h₁ :
  ∀ (x : M2),
    Eq.{u_5 + 1} (α := N)
      (((f.range.liftQ h ⋯ ∘ₗ (↑(exac.linearEquivOfSurjective surj).symm : M3 →ₗ[R] M2 ⧸ f.range)) ∘ₗ g : (a : M2) → N)
          x :
        N)
      ((h : (a : M2) → N) x : N)
⊢ (f.range.liftQ h ⋯ ∘ₗ (↑(exac.linearEquivOfSurjective surj).symm : M3 →ₗ[R] M2 ⧸ f.range)) ∘ₗ g = h

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.LeftExact
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
x : M2
⊢ Eq.{u_5 + 1} (α := N)
    (((f.range.liftQ h ⋯ ∘ₗ (↑(exac.linearEquivOfSurjective surj).symm : M3 →ₗ[R] M2 ⧸ f.range)) ∘ₗ g : (a : M2) → N)
        x :
      N)
    ((h : (a : M2) → N) x : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LeftExact
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
refine_2₃ refine_2₄ : Eq (α := M1 →ₗ[R] N) 0 0
⊢ h ∘ₗ f = 0

Tactic:
rw [← hy, LinearMap.comp_assoc, exac.linearMap_comp_eq_zero, LinearMap.comp_zero y]

Premises used: LinearMap.comp_assoc, LinearMap.comp_zero, Function.Exact.linearMap_comp_eq_zero
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
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
m : ↥M
n : ↥N
⊢ (↑((H.mulMap : (a : ↥M ⊗[R] ↥N) → ↥(M * N)) (m ⊗ₜ[R] n)) : S) = (↑m : S) * (↑n : S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
inst_3 : Subsingleton R
⊢ M.LinearDisjoint N

Tactic:
haveI : Subsingleton S := Module.subsingleton R S
  ⟨Function.injective_of_subsingleton _⟩

Premises used: Submodule.mulMap, Submodule.LinearDisjoint.mk, Function.injective_of_subsingleton, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
inst_3 : Subsingleton S
⊢ M.LinearDisjoint N

Tactic:
⟨Function.injective_of_subsingleton _⟩

Premises used: Submodule.LinearDisjoint.mk, Function.injective_of_subsingleton
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
⊢ M.LinearDisjoint N ↔
    Submodule.LinearDisjoint.{u, v} (R := R) (S := Sᵐᵒᵖ)
      ((RingEquiv.symm equivOpposite : (a : (Submodule R S)ᵐᵒᵖ) → Submodule R Sᵐᵒᵖ) (MulOpposite.op N))
      ((RingEquiv.symm equivOpposite : (a : (Submodule R S)ᵐᵒᵖ) → Submodule R Sᵐᵒᵖ) (MulOpposite.op M))

Tactic:
simp only [linearDisjoint_iff, mulMap_op, LinearMap.coe_comp,
    LinearEquiv.coe_coe, EquivLike.comp_injective, EquivLike.injective_comp]

Premises used: Submodule.linearDisjoint_iff, EquivLike.injective_comp, EquivLike.comp_injective, LinearMap.coe_comp, Submodule.mulMap_op, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
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)
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)
⊢ N.LinearDisjoint M

Tactic:
rw [linearDisjoint_iff, mulMap_comm_of_commute M N hc]

Premises used: Submodule.linearDisjoint_iff, Submodule.mulMap_comm_of_commute
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
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)
⊢ 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:
((TensorProduct.comm R N M).toEquiv.injective_comp _).2 H.injective

Premises used: Iff.mpr, TensorProduct.comm, Quotient.liftOn', AddCon.liftOn, Membership.mem, Subtype, Equiv.injective_comp, Submodule.LinearDisjoint.injective, LinearEquiv.toEquiv
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
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)
⊢ 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:
exact ((TensorProduct.comm R N M).toEquiv.injective_comp _).2 H.injective

Premises used: Iff.mpr, TensorProduct.comm, Membership.mem, Subtype, Equiv.injective_comp, Submodule.LinearDisjoint.injective, LinearEquiv.toEquiv
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
hc : ∀ (m : ↥M) (n : ↥N), Commute (↑m : S) (↑n : S)
⊢ M.LinearDisjoint N ↔ N.LinearDisjoint M

Tactic:
⟨fun H ↦ H.symm_of_commute hc, fun H ↦ H.symm_of_commute fun _ _ ↦ (hc _ _).symm⟩

Premises used: Submodule.LinearDisjoint.symm_of_commute, Commute.symm, Iff.intro
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
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)
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)
⊢ 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)

Tactic:
rw [linearDisjoint_iff] at H ⊢

Premises used: Submodule.linearDisjoint_iff
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
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.{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
-- Module: Mathlib.LinearAlgebra.LinearDisjoint
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)
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))
⊢ Function.Injective.{v + 1, w + 1} (α := ↥M ⊗[R] ↥N) (β := T)
    (Function.comp (β :=
      ↥(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))
      (⇑(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)
      (⇑(TensorProduct.map
            (LinearMap.submoduleMap
              (↑f :
                [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
              M)
            (LinearMap.submoduleMap
              (↑f :
                [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
              N)) :
        (a : ↥M ⊗[R] ↥N) →
          ↥(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)))

Tactic:
rw [← coe_mulMap_comp_eq] at this

Premises used: Submodule.coe_mulMap_comp_eq