awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsRootSystem
x : M
⊢ x = 0 ↔ ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((P.coroot' i : (a : M) → R) x : R) (0 : R)
have refine : ∀ (h : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((P.coroot' i : (a : M) → R) x : R) (0 : R)), x = 0
Tactic: refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsRootSystem
x : M
h : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((P.coroot' i : (a : M) → R) x : R) (0 : R)
⊢ x = 0
have h₁ : Membership.mem (γ := Submodule R M) (⨅ (i : ι), ker (P.coroot' i)) x
Tactic: replace h : x ∈ ⨅ i, ker (P.coroot' i) := by aesop
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
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 = ⊥ ↔ ∀ (i : ι), ((P.root : (a : ι) → M) i : M) ∉ (↑q : Submodule K M)
have refine : ∀ (h : ∀ (i : ι), ((P.root : (a : ι) → M) i : M) ∉ (↑q : Submodule K M)), q = ⊥
Tactic: refine ⟨fun h ↦ by simp [h, P.ne_zero], fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
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
h : ∀ (i : ι), ((P.root : (a : ι) → M) i : M) ∉ (↑q : Submodule K M)
⊢ q = ⊥
have simp_rw : ∀ x ∈ (↑q : Submodule K M), ∀ (i : ι), x ∈ ker (P.coroot' i)
Tactic: simp_rw [Subtype.mk_eq_bot_iff (invtRootSubmodule.bot_mem P), Submodule.eq_bot_iff,
    P.eq_zero_iff_forall_coroot'_eq_zero, ← LinearMap.mem_ker]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (hypothesis)
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)
⊢ Q =
    span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
have hSQ : span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)}) ≤
  Q
Tactic: have hSQ : span K (P.root '' {i | P.root i ∈ Q}) ≤ Q :=
    span_le.mpr (Set.image_subset_iff.mpr fun _ h => h)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
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)
hSQ :
  span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)}) ≤
    Q
⊢ Q =
    span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
have refine : Q ≤
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
Tactic: refine le_antisymm ?_ hSQ
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
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)
hSQ :
  span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)}) ≤
    Q
⊢ Q ≤
    span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
have set : let 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), Q ≤ S
Tactic: set S := span K (P.root '' {i | P.root i ∈ Q})
Cleared hypotheses: hSQ
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
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 = ⊤
have rw : 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 [← Submodule.span_union, ← Set.image_union]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (hypothesis)
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_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})))
    ⊤
have 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
Tactic: have : {i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q} = Set.univ := by ext; simp [em]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
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
      (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})))
    ⊤
have rw : Eq.{u_3 + 1} (α := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) ⊤
Tactic: rw [this, Set.image_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (hypothesis)
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})
⊢ Q ≤ S
have h_sup : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
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
⊢ v ∈ S
have obtain : ∀ (s : M) (hs : s ∈ S) (t : M) (ht : t ∈ T) (hv : s + t ∈ Q), s + t ∈ S
Tactic: obtain ⟨s, hs, t, ht, rfl⟩ := Submodule.mem_sup.mp (h_sup ▸ Submodule.mem_top (x := v))
Cleared hypotheses: v, hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
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
⊢ s + t ∈ S
have suffices : t = 0
Tactic: suffices t = 0 by rw [this, add_zero]; exact hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (hypothesis)
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 = 0
have htQ : t ∈ Q
Tactic: have htQ : t ∈ Q := by simpa using Q.sub_mem hv (hSQ hs)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
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)
have 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)
Tactic: by_cases hk : P.root k ∈ Q
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
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)
⊢ Eq.{u_5 + 1} (α := K) ((P.coroot' k : (a : M) → K) t : K) (0 : K)
have neg : ∀ (hk : ((P.root : (a : ι) → M) k : M) ∉ Q), Eq.{u_5 + 1} (α := K) ((P.coroot' k : (a : M) → K) t : K) (0 : K)
Tactic: by_cases hk : P.root k ∈ Q
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
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)
have pos : image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q} ⊆
  (↑(ker (P.coroot' k)) : Set M)
Tactic: refine LinearMap.mem_ker.mp (span_le.mpr ?_ ht)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
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
⊢ Membership.mem (α := M) (↑(ker (P.coroot' k)) : Set M) ((P.root : (a : ι) → M) j : M)
have pos : Eq.{u_5 + 1} (α := K) ((P.coroot' j : (a : M) → K) ((P.root : (a : ι) → M) k : M) : K) (0 : K)
Tactic: rw [SetLike.mem_coe, LinearMap.mem_ker, P.root_coroot'_eq_pairing, P.pairing_eq_zero_iff',
        ← P.root_coroot'_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (hypothesis)
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
⊢ t = 0
have h_ker : ∀ (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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Nontrivial M
⊢ IsSimpleModule R[↥P.weylGroup] P.weylGroupRootRep.asModule ↔
    ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤
have rw : IsSimpleOrder.{u_3} ↥P.weylGroupRootRep.invtSubmodule ↔
  ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤
Tactic: rw [isSimpleModule_iff, ← P.weylGroupRootRep.mapSubmodule.isSimpleOrder_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Nontrivial M
⊢ IsSimpleOrder.{u_3} ↥P.weylGroupRootRep.invtSubmodule ↔
    ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤
have refine_1 : ∀ (h : IsSimpleOrder.{u_3} ↥P.weylGroupRootRep.invtSubmodule) (q : Submodule R M)
  (hq₁ : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) (hq₂ : q ≠ ⊥), q = ⊤
Tactic: refine ⟨fun h q hq₁ hq₂ ↦ ?_, fun h ↦ ⟨fun q ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Nontrivial M
refine_1 :
  ∀ (h : IsSimpleOrder.{u_3} ↥P.weylGroupRootRep.invtSubmodule) (q : Submodule R M)
    (hq₁ : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) (hq₂ : q ≠ ⊥), q = ⊤
⊢ IsSimpleOrder.{u_3} ↥P.weylGroupRootRep.invtSubmodule ↔
    ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤
have refine_2 : ∀ (h : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤)
  (q : ↥P.weylGroupRootRep.invtSubmodule), q = ⊥ ∨ q = ⊤
Tactic: refine ⟨fun h q hq₁ hq₂ ↦ ?_, fun h ↦ ⟨fun q ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Nontrivial M
h : IsSimpleOrder.{u_3} ↥P.weylGroupRootRep.invtSubmodule
q : Submodule R M
hq₁ : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
hq₂ : q ≠ ⊥
this :
  ∀ (g : ↥P.weylGroup),
    Membership.mem (γ := Sublattice (Submodule R M))
      (invtSubmodule ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M) g)) q
q' : ↥P.weylGroupRootRep.invtSubmodule :=
  Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ P.weylGroupRootRep.invtSubmodule) q ⋯
⊢ q = ⊤
have suffices : q' = ⊤
Tactic: suffices q' = ⊤ by simpa [q']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Nontrivial M
h : IsSimpleOrder.{u_3} ↥P.weylGroupRootRep.invtSubmodule
q : Submodule R M
hq₁ : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
hq₂ : q ≠ ⊥
this :
  ∀ (g : ↥P.weylGroup),
    Membership.mem (γ := Sublattice (Submodule R M))
      (invtSubmodule ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M) g)) q
q' : ↥P.weylGroupRootRep.invtSubmodule :=
  Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ P.weylGroupRootRep.invtSubmodule) q ⋯
⊢ q' = ⊤
have apply : ¬q' = ⊥
Tactic: apply (IsSimpleOrder.eq_bot_or_eq_top _).resolve_left
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Nontrivial M
h : IsSimpleOrder.{u_3} ↥P.weylGroupRootRep.invtSubmodule
q : Submodule R M
hq₁ : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
hq₂ : q ≠ ⊥
⊢ q = ⊤
have refine_1 : ∀ (g : ↥P.weylGroup),
  Membership.mem (γ := Sublattice (Submodule R M))
    (invtSubmodule ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M) g)) q
Tactic: suffices ∀ g : P.weylGroup, q ∈ invtSubmodule (P.weylGroupRootRep g) by
      let q' : P.weylGroupRootRep.invtSubmodule :=
        ⟨q, (Representation.mem_invtSubmodule P.weylGroupRootRep).mpr this⟩
      suffices q' = ⊤ by simpa [q']
      apply (IsSimpleOrder.eq_bot_or_eq_top _).resolve_left
      simpa [q']