awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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
rw :
  IsSimpleOrder.{u_3} ↥P.weylGroupRootRep.invtSubmodule ↔
    ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤
⊢ IsSimpleModule R[↥P.weylGroup] P.weylGroupRootRep.asModule ↔
    ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤

Tactic:
rw [isSimpleModule_iff, ← P.weylGroupRootRep.mapSubmodule.isSimpleOrder_iff]

Premises used: isSimpleModule_iff, OrderIso.isSimpleOrder_iff, Representation.mapSubmodule, RootPairing.weylGroupRootRep
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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 = ⊤

Tactic:
⟨fun h q hq₁ hq₂ ↦ ?_, fun h ↦ ⟨fun q ↦ ?_⟩⟩

Premises used: IsSimpleOrder.mk, Iff.intro
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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 = ⊤
refine_2 :
  ∀ (h : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤)
    (q : ↥P.weylGroupRootRep.invtSubmodule), q = ⊥ ∨ q = ⊤
⊢ IsSimpleOrder.{u_3} ↥P.weylGroupRootRep.invtSubmodule ↔
    ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) → q ≠ ⊥ → q = ⊤

Tactic:
refine ⟨fun h q hq₁ hq₂ ↦ ?_, fun h ↦ ⟨fun q ↦ ?_⟩⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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_1 :
  ∀ (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 ⋯
this : q' = ⊤
⊢ q = ⊤

Tactic:
simpa [q']
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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 ⋯
suffices : q' = ⊤
⊢ q = ⊤

Tactic:
suffices q' = ⊤ by simpa [q']
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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 ⋯
apply : ¬q' = ⊥
⊢ q' = ⊤

Tactic:
apply (IsSimpleOrder.eq_bot_or_eq_top _).resolve_left

Premises used: Or.resolve_left, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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' = ⊥

Tactic:
simpa [q']
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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 ≠ ⊥
refine_1 :
  ∀ (g : ↥P.weylGroup),
    Membership.mem (γ := Sublattice (Submodule R M))
      (invtSubmodule ((P.weylGroupRootRep : (a : ↥P.weylGroup) → M →ₗ[R] M) g)) q
⊢ 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']
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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
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

Tactic:
hq₁ i

Premises used: Set.Mem, setOf
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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
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

Tactic:
exact hq₁ i
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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
⊢ 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

Tactic:
simp [← Submonoid.one_def]

Premises used: Submonoid.one_def
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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
refine_1₁ : q ∈ invtSubmodule (↑y : 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

Tactic:
apply invtSubmodule.comp

Premises used: Module.End.invtSubmodule.comp
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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
⊢ q ∈ invtSubmodule (↑x : P.Hom P).weightMap

Tactic:
assumption
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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
⊢ q ∈ invtSubmodule (↑y : P.Hom P).weightMap

Tactic:
assumption
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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
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) ⋯)))
      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

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

Premises used: Submonoid.one_def, Module.End.invtSubmodule.comp
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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) ⊥ ⊤
refine_2₁ : ∀ (hq : q ≠ ⊥), q = ⊥ ∨ q = ⊤
⊢ q = ⊥ ∨ q = ⊤

Tactic:
rcases eq_or_ne q ⊥ with rfl | hq

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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 = ⊤
refine_2 refine_2₁ :
  ¬Eq.{u_3 + 1} (α := ↥P.weylGroupRootRep.invtSubmodule) ⊥ ⊥ → Eq.{u_3 + 1} (α := ↥P.weylGroupRootRep.invtSubmodule) ⊥ ⊤
⊢ Eq.{u_3 + 1} (α := ↥P.weylGroupRootRep.invtSubmodule) ⊥ ⊥ ∨ Eq.{u_3 + 1} (α := ↥P.weylGroupRootRep.invtSubmodule) ⊥ ⊤

Tactic:
tauto
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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) = ⊤
h₁ : q = ⊤
⊢ q = ⊥ ∨ q = ⊤

Tactic:
right
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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 = ⊤

Tactic:
simpa using this
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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 ≠ ⊥
refine_2 : (↑q : Submodule R M) = ⊤
⊢ q = ⊥ ∨ q = ⊤

Tactic:
suffices (q : Submodule R M) = ⊤ by right; simpa using this
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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) ≠ ⊥

Tactic:
simpa using hq
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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 ≠ ⊥
refine_2 : ∀ (i : ι), (↑q : Submodule R M) ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
⊢ (↑q : Submodule R M) = ⊤

Tactic:
refine h q (fun i ↦ ?_) (by simpa using hq)

Premises used: Subtype.val
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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 ≠ ⊥
i : ι
⊢ (↑q : Submodule R M) ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)

Tactic:
P.weylGroupRootRep.mem_invtSubmodule.mp q.property ⟨_, P.reflection_mem_weylGroup i⟩

Premises used: Set.Mem, setOf, RootPairing.reflection_mem_weylGroup, Subtype.mk, Iff.mp, Representation.mem_invtSubmodule, Subtype.property, RootPairing.weylGroupRootRep
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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 ≠ ⊥
i : ι
⊢ (↑q : Submodule R M) ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)

Tactic:
exact P.weylGroupRootRep.mem_invtSubmodule.mp q.property ⟨_, P.reflection_mem_weylGroup i⟩

Premises used: RootPairing.reflection_mem_weylGroup, Subtype.mk, Iff.mp, Representation.mem_invtSubmodule, Subtype.property, RootPairing.weylGroupRootRep
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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.IsIrreducible
⊢ IsSimpleModule R[↥P.weylGroup] P.weylGroupRootRep.asModule

Tactic:
have := IsIrreducible.nontrivial P
  P.isSimpleModule_weylGroupRootRep_iff.mpr IsIrreducible.eq_top_of_invtSubmodule_reflection

Premises used: Iff.mpr, RootPairing.IsIrreducible.nontrivial, RootPairing.isSimpleModule_weylGroupRootRep_iff, RootPairing.IsIrreducible.eq_top_of_invtSubmodule_reflection
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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 : Subsingleton M
⊢ ¬P.IsIrreducible

Tactic:
fun contra ↦ not_nontrivial _ contra.nontrivial

Premises used: RootPairing.IsIrreducible.nontrivial, not_nontrivial, Not
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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)
rw : Submodule.map (↑(P.coreflection i) : N →ₗ[R] N).dualMap q.dualAnnihilator ≤ q.dualAnnihilator
⊢ Submodule.map (↑P.toPerfPair.symm : Module.Dual R N →ₗ[R] M) q.dualAnnihilator ∈
    invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)

Tactic:
rw [LinearEquiv.map_mem_invtSubmodule_iff, LinearEquiv.symm_symm, toPerfPair_conj_reflection,
    Module.End.mem_invtSubmodule, ← Submodule.map_le_iff_le_comap]

Premises used: Module.End.mem_invtSubmodule, LinearEquiv.symm_symm, RootPairing.toPerfPair_conj_reflection, Submodule.map_le_iff_le_comap, LinearEquiv.map_mem_invtSubmodule_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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.coreflection i) : N →ₗ[R] N).dualMap q.dualAnnihilator ≤ q.dualAnnihilator

Tactic:
(Submodule.dualAnnihilator_map_dualMap_le _ _).trans <| Submodule.dualAnnihilator_anti hq

Premises used: Submodule.dualAnnihilator_map_dualMap_le, Set.Mem, Submodule.dualAnnihilator_anti, LE.le.trans
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
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.coreflection i) : N →ₗ[R] N).dualMap q.dualAnnihilator ≤ q.dualAnnihilator

Tactic:
exact (Submodule.dualAnnihilator_map_dualMap_le _ _).trans <| Submodule.dualAnnihilator_anti hq

Premises used: Submodule.dualAnnihilator_map_dualMap_le, Submodule.dualAnnihilator_anti, LE.le.trans
-- 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 : 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 ≠ ⊥
⊢ 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)

Premises used: Submodule.dualAnnihilator, Submodule.map
-- 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 : 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.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

Premises used: not_imp_comm, Submodule.map_eq_top_iff