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 : 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 ≠ ⊥
g x y : P.Aut
hx : x ∈ P.weylGroup
hy : y ∈ P.weylGroup
hx' :
  Membership.mem (γ := Sublattice (Submodule R M))
    (invtSubmodule
      ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) x hx)))
    q
hy' :
  Membership.mem (γ := Sublattice (Submodule R M))
    (invtSubmodule
      ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) y hy)))
    q
⊢ Membership.mem (γ := Sublattice (Submodule R M))
    (invtSubmodule
      ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (x * y) ⋯)))
    q
have refine_1 : q ∈ invtSubmodule (↑x : P.Hom P).weightMap
Tactic: apply invtSubmodule.comp
-- 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 ≠ ⊥
g x y : P.Aut
hx : x ∈ P.weylGroup
hy : y ∈ P.weylGroup
hx' :
  Membership.mem (γ := Sublattice (Submodule R M))
    (invtSubmodule
      ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) x hx)))
    q
hy' :
  Membership.mem (γ := Sublattice (Submodule R M))
    (invtSubmodule
      ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) y hy)))
    q
refine_1 : q ∈ invtSubmodule (↑x : P.Hom P).weightMap
⊢ Membership.mem (γ := Sublattice (Submodule R M))
    (invtSubmodule
      ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (x * y) ⋯)))
    q
have refine_1₁ : q ∈ invtSubmodule (↑y : P.Hom P).weightMap
Tactic: apply invtSubmodule.comp
-- 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 ≠ ⊥
g : P.Aut
hg : g ∈ P.weylGroup
⊢ Membership.mem (γ := Sublattice (Submodule R M))
    (invtSubmodule
      ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g hg)))
    q
have refine_1 : ∀ (i : ι),
  Membership.mem (γ := Sublattice (Submodule R M))
    (invtSubmodule
      ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) sorry)))
    q
Tactic: induction hg using weylGroup.induction with
    | mem i => exact hq₁ i
    | one => simp [← Submonoid.one_def]
    | mul x y hx hy hx' hy' => apply invtSubmodule.comp <;> assumption
Cleared hypotheses: hg
-- 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 ≠ ⊥
g : P.Aut
hg : g ∈ P.weylGroup
refine_1 :
  ∀ (i : ι),
    Membership.mem (γ := Sublattice (Submodule R M))
      (invtSubmodule
        ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) ⋯)))
      q
⊢ Membership.mem (γ := Sublattice (Submodule R M))
    (invtSubmodule
      ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g hg)))
    q
have refine_1₁ : Membership.mem (γ := Sublattice (Submodule R M))
  (invtSubmodule
    ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 sorry)))
  q
Tactic: induction hg using weylGroup.induction with
    | mem i => exact hq₁ i
    | one => simp [← Submonoid.one_def]
    | mul x y hx hy hx' hy' => apply invtSubmodule.comp <;> assumption
Cleared hypotheses: hg
-- 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 ≠ ⊥
g : P.Aut
hg : g ∈ P.weylGroup
refine_1 :
  ∀ (i : ι),
    Membership.mem (γ := Sublattice (Submodule R M))
      (invtSubmodule
        ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) ⋯)))
      q
refine_1₁ :
  Membership.mem (γ := Sublattice (Submodule R M))
    (invtSubmodule
      ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 ⋯)))
    q
⊢ Membership.mem (γ := Sublattice (Submodule R M))
    (invtSubmodule
      ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g hg)))
    q
have refine_1₂ : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup)
  (hx' :
    Membership.mem (γ := Sublattice (Submodule R M))
      (invtSubmodule
        ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) x hx)))
      q)
  (hy' :
    Membership.mem (γ := Sublattice (Submodule R M))
      (invtSubmodule
        ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) y hy)))
      q),
  Membership.mem (γ := Sublattice (Submodule R M))
    (invtSubmodule
      ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (x * y) sorry)))
    q
Tactic: induction hg using weylGroup.induction with
    | mem i => exact hq₁ i
    | one => simp [← Submonoid.one_def]
    | mul x y hx hy hx' hy' => apply invtSubmodule.comp <;> assumption
Cleared hypotheses: hg
-- 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 : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤
q : ↥P.weylGroupRootRep.invtSubmodule
⊢ q = ⊥ ∨ q = ⊤
have refine_2 : Eq.{u_3 + 1} (α := ↥P.weylGroupRootRep.invtSubmodule) ⊥ ⊥ ∨ Eq.{u_3 + 1} (α := ↥P.weylGroupRootRep.invtSubmodule) ⊥ ⊤
Tactic: rcases eq_or_ne q ⊥ with rfl | hq
Cleared hypotheses: 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 : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤
q : ↥P.weylGroupRootRep.invtSubmodule
refine_2 :
  Eq.{u_3 + 1} (α := ↥P.weylGroupRootRep.invtSubmodule) ⊥ ⊥ ∨ Eq.{u_3 + 1} (α := ↥P.weylGroupRootRep.invtSubmodule) ⊥ ⊤
⊢ q = ⊥ ∨ q = ⊤
have refine_2₁ : ∀ (hq : q ≠ ⊥), q = ⊥ ∨ q = ⊤
Tactic: rcases eq_or_ne q ⊥ with rfl | hq
-- 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 : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤
⊢ Eq.{u_3 + 1} (α := ↥P.weylGroupRootRep.invtSubmodule) ⊥ ⊥ ∨ Eq.{u_3 + 1} (α := ↥P.weylGroupRootRep.invtSubmodule) ⊥ ⊤
have refine_2 : ¬Eq.{u_3 + 1} (α := ↥P.weylGroupRootRep.invtSubmodule) ⊥ ⊥ → Eq.{u_3 + 1} (α := ↥P.weylGroupRootRep.invtSubmodule) ⊥ ⊤
Tactic: tauto
-- 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 : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤
q : ↥P.weylGroupRootRep.invtSubmodule
hq : q ≠ ⊥
this : (↑q : Submodule R M) = ⊤
⊢ q = ⊥ ∨ q = ⊤
have h₁ : q = ⊤
Tactic: right
-- 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 : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤
q : ↥P.weylGroupRootRep.invtSubmodule
hq : q ≠ ⊥
⊢ q = ⊥ ∨ q = ⊤
have refine_2 : (↑q : Submodule R M) = ⊤
Tactic: suffices (q : Submodule R M) = ⊤ by right; simpa using this
-- 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 : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤
q : ↥P.weylGroupRootRep.invtSubmodule
hq : q ≠ ⊥
⊢ (↑q : Submodule R M) = ⊤
have refine_2 : ∀ (i : ι), (↑q : Submodule R M) ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
Tactic: refine h q (fun i ↦ ?_) (by simpa using hq)
-- 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
i : ι
q : Submodule R N
hq : q ∈ invtSubmodule (↑(P.coreflection i) : N →ₗ[R] N)
⊢ Submodule.map (↑P.toPerfPair.symm : Module.Dual R N →ₗ[R] M) q.dualAnnihilator ∈
    invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
have rw : Submodule.map (↑(P.coreflection i) : N →ₗ[R] N).dualMap q.dualAnnihilator ≤ q.dualAnnihilator
Tactic: rw [LinearEquiv.map_mem_invtSubmodule_iff, LinearEquiv.symm_symm, toPerfPair_conj_reflection,
    Module.End.mem_invtSubmodule, ← Submodule.map_le_iff_le_comap]
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
h : ∀ (q : Submodule K M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)) → q ≠ ⊥ → q = ⊤
q : Submodule K N
stab : ∀ (i : ι), q ∈ invtSubmodule (↑(P.coreflection i) : N →ₗ[K] N)
ne_bot : q ≠ ⊥
⊢ q = ⊤
have h₁ : Submodule.map (↑P.toPerfPair.symm : Module.Dual K N →ₗ[K] M) q.dualAnnihilator ≠ ⊥ →
  Submodule.map (↑P.toPerfPair.symm : Module.Dual K N →ₗ[K] M) q.dualAnnihilator = ⊤
Tactic: specialize h (q.dualAnnihilator.map P.toPerfPair.symm)
      fun i ↦ invtSubmodule_reflection_of_invtSubmodule_coreflection P i q (stab i)
Cleared hypotheses: h
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
q : Submodule K N
stab : ∀ (i : ι), q ∈ invtSubmodule (↑(P.coreflection i) : N →ₗ[K] N)
ne_bot : q ≠ ⊥
h :
  Submodule.map (↑P.toPerfPair.symm : Module.Dual K N →ₗ[K] M) q.dualAnnihilator ≠ ⊥ →
    Submodule.map (↑P.toPerfPair.symm : Module.Dual K N →ₗ[K] M) q.dualAnnihilator = ⊤
⊢ q = ⊤
have h₁ : ¬q.dualAnnihilator = ⊤ → Submodule.map (↑P.toPerfPair.symm : Module.Dual K N →ₗ[K] M) q.dualAnnihilator = ⊥
Tactic: rw [Submodule.map_eq_top_iff, not_imp_comm] at h
Cleared hypotheses: h
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
q : Submodule K N
stab : ∀ (i : ι), q ∈ invtSubmodule (↑(P.coreflection i) : N →ₗ[K] N)
ne_bot : q ≠ ⊥
h : ¬q.dualAnnihilator = ⊤ → Submodule.map (↑P.toPerfPair.symm : Module.Dual K N →ₗ[K] M) q.dualAnnihilator = ⊥
⊢ q = ⊤
have ne_bot₁ : q.dualAnnihilator ≠ ⊤
Tactic: replace ne_bot : q.dualAnnihilator ≠ ⊤ := by simpa
Cleared hypotheses: ne_bot
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
⊢ P.IsIrreducible ↔ IsSimpleOrder.{u_3} ↥P.invtRootSubmodule
have refine_1 : ∀ (h : P.IsIrreducible) (x : ↥P.invtRootSubmodule) (q : Submodule K M) (hq : q ∈ P.invtRootSubmodule),
  Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq = ⊥ ∨
    Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq = ⊤
Tactic: refine ⟨fun h ↦ ⟨fun ⟨q, hq⟩ ↦ ?_⟩, fun h ↦ IsIrreducible.mk' P fun q hq hq' ↦ ?_⟩
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
refine_1 :
  ∀ (h : P.IsIrreducible) (x : ↥P.invtRootSubmodule) (q : Submodule K M) (hq : q ∈ P.invtRootSubmodule),
    Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq = ⊥ ∨
      Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq = ⊤
⊢ P.IsIrreducible ↔ IsSimpleOrder.{u_3} ↥P.invtRootSubmodule
have refine_2 : ∀ (h : IsSimpleOrder.{u_3} ↥P.invtRootSubmodule) (q : Submodule K M)
  (hq : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)) (hq' : q ≠ ⊥), q = ⊤
Tactic: refine ⟨fun h ↦ ⟨fun ⟨q, hq⟩ ↦ ?_⟩, fun h ↦ IsIrreducible.mk' P fun q hq hq' ↦ ?_⟩
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x : ↥P.invtRootSubmodule
q : Submodule K M
hq : q ∈ P.invtRootSubmodule
⊢ Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq = ⊥ ∨
    Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq = ⊤
have refine_1 : q = ⊥ ∨ q = ⊤
Tactic: simp only [invtRootSubmodule.bot_mem, invtRootSubmodule.top_mem, Subtype.mk_eq_bot_iff,
      Subtype.mk_eq_top_iff]
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x : ↥P.invtRootSubmodule
q : Submodule K M
hq : q ∈ P.invtRootSubmodule
⊢ q = ⊥ ∨ q = ⊤
have hq₁ : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
Tactic: rw [mem_invtRootSubmodule_iff] at hq
Cleared hypotheses: hq
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x : ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
⊢ q = ⊥ ∨ q = ⊤
have this : q ≠ ⊥ → q = ⊤
Tactic: have := IsIrreducible.eq_top_of_invtSubmodule_reflection q hq
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x : ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
this : q ≠ ⊥ → q = ⊤
⊢ q = ⊥ ∨ q = ⊤
have refine_1 : ∀ (this : ¬q ≠ ⊥), q = ⊥ ∨ q = ⊤
Tactic: tauto
Cleared hypotheses: this
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x : ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
this : q ≠ ⊥ → q = ⊤
refine_1 : ∀ (this : ¬q ≠ ⊥), q = ⊥ ∨ q = ⊤
⊢ q = ⊥ ∨ q = ⊤
have refine_1₁ : ∀ (this : q = ⊤), q = ⊥ ∨ q = ⊤
Tactic: tauto
Cleared hypotheses: this
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x : ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
this : q ≠ ⊥ → q = ⊤
refine_1 : ∀ (this : ¬q ≠ ⊥), q = ⊥ ∨ q = ⊤
refine_1₁ : ∀ (this : q = ⊤), q = ⊥ ∨ q = ⊤
refine_1₂ : ∀ (this : ¬q ≠ ⊥), q = ⊥ ∨ q = ⊤
refine_1₃ : ∀ (this : q = ⊤), q = ⊥ ∨ q = ⊤
⊢ q = ⊥ ∨ q = ⊤
have refine_1₄ : ∀ (this : ¬q ≠ ⊥), ¬q = ⊥ → q = ⊤
Tactic: tauto
Cleared hypotheses: this
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x : ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
this : q ≠ ⊥ → q = ⊤
refine_1 : ∀ (this : ¬q ≠ ⊥), q = ⊥ ∨ q = ⊤
refine_1₁ : ∀ (this : q = ⊤), q = ⊥ ∨ q = ⊤
refine_1₂ : ∀ (this : ¬q ≠ ⊥), q = ⊥ ∨ q = ⊤
refine_1₃ : ∀ (this : q = ⊤), q = ⊥ ∨ q = ⊤
refine_1₄ : ∀ (this : ¬q ≠ ⊥), ¬q = ⊥ → q = ⊤
⊢ q = ⊥ ∨ q = ⊤
have refine_1₅ : ∀ (this : q = ⊤), ¬q = ⊥ → q = ⊤
Tactic: tauto
Cleared hypotheses: this
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x : ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
this : q ≠ ⊥ → q = ⊤
refine_1 : ∀ (this : ¬q ≠ ⊥), q = ⊥ ∨ q = ⊤
refine_1₁ : ∀ (this : q = ⊤), q = ⊥ ∨ q = ⊤
refine_1₂ : ∀ (this : ¬q ≠ ⊥), q = ⊥ ∨ q = ⊤
refine_1₃ : ∀ (this : q = ⊤), q = ⊥ ∨ q = ⊤
refine_1₄ : ∀ (this : ¬q ≠ ⊥), ¬q = ⊥ → q = ⊤
refine_1₅ : ∀ (this : q = ⊤), ¬q = ⊥ → q = ⊤
⊢ q = ⊥ ∨ q = ⊤
have refine_1₆ : ∀ (this : q = ⊥), ¬q = ⊥ → q = ⊤
Tactic: tauto
Cleared hypotheses: this
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
h : IsSimpleOrder.{u_3} ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
hq' : q ≠ ⊥
q' : ↥P.invtRootSubmodule := Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q ⋯
⊢ q = ⊤
have hq'₁ : ⊥ < q'
Tactic: replace hq' : ⊥ < q' := by simpa [q', bot_lt_iff_ne_bot, -IsSimpleOrder.bot_lt_iff_eq_top]
Cleared hypotheses: hq'
-- 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 : Module K M
inst_4 : Module K N
inst_5 : Nontrivial M
P : RootPairing ι K M N
h : IsSimpleOrder.{u_3} ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
q' : ↥P.invtRootSubmodule := Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q ⋯
hq' : ⊥ < q'
⊢ q = ⊤
have refine_2 : q' = ⊤
Tactic: suffices q' = ⊤ by simpa [q'] using this
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : Module.IsTorsionFree R M
q : Submodule R M
hq : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
⊢ ∃ (Φ : Set ι),
    (∀ i ∈ Φ, ¬Disjoint q (span R (singleton (α := M) ((P.root : (a : ι) → M) i : M)))) ∧ ∀ i ∉ Φ, q ≤ ker (P.coroot' i)
have refine : ∀ (i : ι) (hi : i ∉ {i : ι | ¬Disjoint q (span R (singleton (α := M) ((P.root : (a : ι) → M) i : M)))}),
  q ≤ ker (P.coroot' i)
Tactic: refine ⟨{i | ¬ Disjoint q (R ∙ P.root i)}, by simp, fun i hi ↦ ?_⟩
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : Module.IsTorsionFree R M
q : Submodule R M
hq : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
i : ι
hi : i ∉ {i : ι | ¬Disjoint q (span R (singleton (α := M) ((P.root : (a : ι) → M) i : M)))}
⊢ q ≤ ker (P.coroot' i)
have hi₁ : Disjoint q (span R (singleton (α := M) ((P.root : (a : ι) → M) i : M)))
Tactic: simp only [mem_setOf_eq, not_not] at hi
Cleared hypotheses: hi
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
inst_7 : Module.IsTorsionFree R M
q : Submodule R M
hq : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
i : ι
hi : Disjoint q (span R (singleton (α := M) ((P.root : (a : ι) → M) i : M)))
⊢ q ≤ ker (P.coroot' i)
have rw : q ∈ invtSubmodule (↑(Module.reflection sorry) : M →ₗ[R] M)
Tactic: rw [← Submodule.mem_invtSubmodule_reflection_iff (by simp) hi]