awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h :
  ∀ (x : ι),
    Membership.mem (γ := Set ι)
        ({i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)} ∪
          {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
        x ↔
      Membership.mem (γ := Set ι) univ x
⊢ Eq.{u_1 + 1} (α := Set ι)
    ({i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)} ∪ {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
    univ

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
x : ι
⊢ Membership.mem (γ := Set ι)
      ({i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)} ∪
        {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
      x ↔
    Membership.mem (γ := Set ι) univ x

Tactic:
simp [em]

Premises used: em
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
⊢ Eq.{u_1 + 1} (α := Set ι)
    ({i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)} ∪ {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
    univ

Tactic:
have : {i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q} = Set.univ := by ext; simp [em]
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
this :
  Eq.{u_1 + 1} (α := Set ι)
    ({i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)} ∪ {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
    univ
rw : Eq.{u_3 + 1} (α := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) ⊤
⊢ Eq.{u_3 + 1} (α := Submodule K M)
    (span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        ({i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)} ∪
          {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})))
    ⊤

Tactic:
rw [this, Set.image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
this :
  Eq.{u_1 + 1} (α := Set ι)
    ({i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)} ∪ {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
    univ
⊢ Eq.{u_3 + 1} (α := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) ⊤

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
⊢ S ⊔ T = ⊤

Tactic:
have h_sup : S ⊔ T = ⊤ := by
    rw [← Submodule.span_union, ← Set.image_union]
    have : {i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q} = Set.univ := by ext; simp [em]
    rw [this, Set.image_univ]
    simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
v : M
hv : v ∈ Q
obtain : ∀ (s : M) (hs : s ∈ S) (t : M) (ht : t ∈ T) (hv : s + t ∈ Q), s + t ∈ S
⊢ v ∈ S

Tactic:
obtain ⟨s, hs, t, ht, rfl⟩ := Submodule.mem_sup.mp (h_sup ▸ Submodule.mem_top (x := v))

Premises used: Iff.mp, Submodule.mem_sup, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
this : t = 0
rw : s ∈ S
⊢ s + t ∈ S

Tactic:
rw [this, add_zero]

Premises used: add_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
this : t = 0
⊢ s ∈ S

Tactic:
hs

Premises used: Set.Mem
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
this : t = 0
⊢ s ∈ S

Tactic:
exact hs
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
suffices : t = 0
⊢ s + t ∈ S

Tactic:
suffices t = 0 by rw [this, add_zero]; exact hs
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
⊢ t ∈ Q

Tactic:
simpa using Q.sub_mem hv (hSQ hs)

Premises used: Submodule.sub_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
⊢ t ∈ Q

Tactic:
have htQ : t ∈ Q := by simpa using Q.sub_mem hv (hSQ hs)
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
pos :
  ∀ (hk : Membership.mem (α := M) Q ((P.root : (a : ι) → M) k : M)),
    Eq.{u_5 + 1} (α := K) ((P.coroot' k : (a : M) → K) t : K) (0 : K)
neg : ∀ (hk : ((P.root : (a : ι) → M) k : M) ∉ Q), Eq.{u_5 + 1} (α := K) ((P.coroot' k : (a : M) → K) t : K) (0 : K)
⊢ Eq.{u_5 + 1} (α := K) ((P.coroot' k : (a : M) → K) t : K) (0 : K)

Tactic:
by_cases hk : P.root k ∈ Q

Premises used: RootPairing.root, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
hk : Membership.mem (α := M) Q ((P.root : (a : ι) → M) k : M)
⊢ Eq.{u_5 + 1} (α := K) ((P.coroot' k : (a : M) → K) t : K) (0 : K)

Tactic:
LinearMap.mem_ker.mp (span_le.mpr ?_ ht)

Premises used: Iff.mpr, LinearMap.mem_ker, Iff.mp, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
hk : Membership.mem (α := M) Q ((P.root : (a : ι) → M) k : M)
pos :
  image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q} ⊆
    (↑(ker (P.coroot' k)) : Set M)
⊢ Eq.{u_5 + 1} (α := K) ((P.coroot' k : (a : M) → K) t : K) (0 : K)

Tactic:
refine LinearMap.mem_ker.mp (span_le.mpr ?_ ht)

Premises used: Iff.mpr, LinearMap.mem_ker, Iff.mp, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
hk : Membership.mem (α := M) Q ((P.root : (a : ι) → M) k : M)
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q} j
pos : Eq.{u_5 + 1} (α := K) ((P.coroot' j : (a : M) → K) ((P.root : (a : ι) → M) k : M) : K) (0 : K)
⊢ Membership.mem (α := M) (↑(ker (P.coroot' k)) : Set M) ((P.root : (a : ι) → M) j : M)

Tactic:
rw [SetLike.mem_coe, LinearMap.mem_ker, P.root_coroot'_eq_pairing, P.pairing_eq_zero_iff',
        ← P.root_coroot'_eq_pairing]

Premises used: RootPairing.pairing_eq_zero_iff', LinearMap.mem_ker, SetLike.mem_coe, RootPairing.root_coroot'_eq_pairing
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
hk : Membership.mem (α := M) Q ((P.root : (a : ι) → M) k : M)
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q} j
⊢ Eq.{u_5 + 1} (α := K) ((P.coroot' j : (a : M) → K) ((P.root : (a : ι) → M) k : M) : K) (0 : K)

Tactic:
LinearMap.mem_ker.mp (invtRootSubmodule.le_ker_coroot' q hj hk)

Premises used: RootPairing.invtRootSubmodule.le_ker_coroot', LinearMap.mem_ker, Iff.mp
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
hk : Membership.mem (α := M) Q ((P.root : (a : ι) → M) k : M)
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q} j
⊢ Eq.{u_5 + 1} (α := K) ((P.coroot' j : (a : M) → K) ((P.root : (a : ι) → M) k : M) : K) (0 : K)

Tactic:
exact LinearMap.mem_ker.mp (invtRootSubmodule.le_ker_coroot' q hj hk)

Premises used: RootPairing.invtRootSubmodule.le_ker_coroot', LinearMap.mem_ker, Iff.mp
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
hk : ((P.root : (a : ι) → M) k : M) ∉ Q
⊢ Eq.{u_5 + 1} (α := K) ((P.coroot' k : (a : M) → K) t : K) (0 : K)

Tactic:
LinearMap.mem_ker.mp (invtRootSubmodule.le_ker_coroot' q hk htQ)

Premises used: RootPairing.invtRootSubmodule.le_ker_coroot', LinearMap.mem_ker, Iff.mp
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
hk : ((P.root : (a : ι) → M) k : M) ∉ Q
⊢ Eq.{u_5 + 1} (α := K) ((P.coroot' k : (a : M) → K) t : K) (0 : K)

Tactic:
exact LinearMap.mem_ker.mp (invtRootSubmodule.le_ker_coroot' q hk htQ)

Premises used: RootPairing.invtRootSubmodule.le_ker_coroot', LinearMap.mem_ker, Iff.mp
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
⊢ ∀ (k : ι), Eq.{u_5 + 1} (α := K) ((P.coroot' k : (a : M) → K) t : K) (0 : K)

Tactic:
have h_ker : ∀ k, P.coroot' k t = 0 := by
    intro k
    by_cases hk : P.root k ∈ Q
    · refine LinearMap.mem_ker.mp (span_le.mpr ?_ ht)
      rintro _ ⟨j, hj, rfl⟩
      rw [SetLike.mem_coe, LinearMap.mem_ker, P.root_coroot'_eq_pairing, P.pairing_eq_zero_iff',
        ← P.root_coroot'_eq_pairing]
      exact LinearMap.mem_ker.mp (invtRootSubmodule.le_ker_coroot' q hj hk)
    · exact LinearMap.mem_ker.mp (invtRootSubmodule.le_ker_coroot' q hk htQ)
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
h_ker : ∀ (k : ι), Eq.{u_5 + 1} (α := K) ((P.coroot' k : (a : M) → K) t : K) (0 : K)
⊢ t = 0

Tactic:
P.eq_zero_iff_forall_coroot'_eq_zero.mpr h_ker

Premises used: Iff.mpr, RootPairing.eq_zero_iff_forall_coroot'_eq_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
h_ker : ∀ (k : ι), Eq.{u_5 + 1} (α := K) ((P.coroot' k : (a : M) → K) t : K) (0 : K)
⊢ t = 0

Tactic:
exact P.eq_zero_iff_forall_coroot'_eq_zero.mpr h_ker

Premises used: Iff.mpr, RootPairing.eq_zero_iff_forall_coroot'_eq_zero