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 : 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.dualAnnihilator ≠ ⊤

Tactic:
simpa
-- 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 : ¬q.dualAnnihilator = ⊤ → Submodule.map (↑P.toPerfPair.symm : Module.Dual K N →ₗ[K] M) q.dualAnnihilator = ⊥
⊢ q.dualAnnihilator ≠ ⊤

Tactic:
replace ne_bot : q.dualAnnihilator ≠ ⊤ := by simpa
-- 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)
h : ¬q.dualAnnihilator = ⊤ → Submodule.map (↑P.toPerfPair.symm : Module.Dual K N →ₗ[K] M) q.dualAnnihilator = ⊥
ne_bot : q.dualAnnihilator ≠ ⊤
⊢ q = ⊤

Tactic:
simpa using h ne_bot
-- 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
⊢ P.IsIrreducible ↔ IsSimpleOrder.{u_3} ↥P.invtRootSubmodule

Tactic:
⟨fun h ↦ ⟨fun ⟨q, hq⟩ ↦ ?_⟩, fun h ↦ IsIrreducible.mk' P fun q hq hq' ↦ ?_⟩

Premises used: IsSimpleOrder.mk, _private.0.RootPairing.isIrreducible_iff_invtRootSubmodule.match_1, Bot.bot, RootPairing.IsIrreducible.mk', Iff.intro, Or, Top.top, Eq
-- 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
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 = ⊤
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 = ⊤
⊢ P.IsIrreducible ↔ IsSimpleOrder.{u_3} ↥P.invtRootSubmodule

Tactic:
refine ⟨fun h ↦ ⟨fun ⟨q, hq⟩ ↦ ?_⟩, fun h ↦ IsIrreducible.mk' P fun q hq hq' ↦ ?_⟩
-- 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 : P.IsIrreducible
x : ↥P.invtRootSubmodule
q : Submodule K M
hq : q ∈ P.invtRootSubmodule
refine_1 : q = ⊥ ∨ q = ⊤
⊢ 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:
simp only [invtRootSubmodule.bot_mem, invtRootSubmodule.top_mem, Subtype.mk_eq_bot_iff,
      Subtype.mk_eq_top_iff]

Premises used: RootPairing.invtRootSubmodule.bot_mem, RootPairing.invtRootSubmodule.top_mem, Subtype.mk_eq_top_iff, Subtype.mk_eq_bot_iff
-- 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 : P.IsIrreducible
x : ↥P.invtRootSubmodule
q : Submodule K M
hq : q ∈ P.invtRootSubmodule
⊢ ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)

Tactic:
rw [mem_invtRootSubmodule_iff] at hq

Premises used: RootPairing.mem_invtRootSubmodule_iff
-- 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 : P.IsIrreducible
x : ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
⊢ q ≠ ⊥ → q = ⊤

Tactic:
have := IsIrreducible.eq_top_of_invtSubmodule_reflection q hq
-- 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 : 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 = ⊤
refine_1₆ : ∀ (this : q = ⊥), ¬q = ⊥ → q = ⊤
⊢ q = ⊥ ∨ q = ⊤

Tactic:
tauto
-- 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 : 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'

Tactic:
simpa [q', bot_lt_iff_ne_bot, -IsSimpleOrder.bot_lt_iff_eq_top]

Premises used: bot_lt_iff_ne_bot, IsSimpleOrder.bot_lt_iff_eq_top
-- 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 : 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'

Tactic:
replace hq' : ⊥ < q' := by simpa [q', bot_lt_iff_ne_bot, -IsSimpleOrder.bot_lt_iff_eq_top]
-- 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 : 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'
this : q' = ⊤
⊢ q = ⊤

Tactic:
simpa [q'] using this
-- 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 : 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'
refine_2 : q' = ⊤
⊢ q = ⊤

Tactic:
suffices q' = ⊤ by simpa [q'] using this
-- 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 : 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' = ⊤

Tactic:
IsSimpleOrder.eq_top_of_lt hq'

Premises used: IsSimpleOrder.eq_top_of_lt
-- 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 : 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' = ⊤

Tactic:
exact IsSimpleOrder.eq_top_of_lt hq'

Premises used: IsSimpleOrder.eq_top_of_lt
-- 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 : 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 : ι),
    Membership.mem (γ := Set ι) {i : ι | ¬Disjoint q (span R (singleton (α := M) ((P.root : (a : ι) → M) i : M)))} i →
      ¬Disjoint q (span R (singleton (α := M) ((P.root : (a : ι) → M) i : M)))

Tactic:
simp
-- 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 : 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)
refine :
  ∀ (i : ι) (hi : i ∉ {i : ι | ¬Disjoint q (span R (singleton (α := M) ((P.root : (a : ι) → M) i : M)))}),
    q ≤ ker (P.coroot' i)
⊢ ∃ (Φ : Set ι),
    (∀ i ∈ Φ, ¬Disjoint q (span R (singleton (α := M) ((P.root : (a : ι) → M) i : M)))) ∧ ∀ i ∉ Φ, q ≤ ker (P.coroot' i)

Tactic:
refine ⟨{i | ¬ Disjoint q (R ∙ P.root i)}, by simp, fun i hi ↦ ?_⟩
-- 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 : 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)))}
⊢ Disjoint q (span R (singleton (α := M) ((P.root : (a : ι) → M) i : M)))

Tactic:
simp only [mem_setOf_eq, not_not] at hi

Premises used: Classical.not_not, Set.mem_setOf_eq
-- 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 : 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)))
⊢ Eq.{u_2 + 1} (α := R) ((P.coroot' i : (a : M) → R) ((P.root : (a : ι) → M) i : M) : R) (2 : R)

Tactic:
simp
-- 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 : 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)))
rw : q ∈ invtSubmodule (↑(Module.reflection ⋯) : M →ₗ[R] M)
⊢ q ≤ ker (P.coroot' i)

Tactic:
rw [← Submodule.mem_invtSubmodule_reflection_iff (by simp) hi]

Premises used: Submodule.mem_invtSubmodule_reflection_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
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 ∈ invtSubmodule (↑(Module.reflection ⋯) : M →ₗ[R] M)

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 : 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 ∈ invtSubmodule (↑(Module.reflection ⋯) : M →ₗ[R] M)

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 : NeZero.{u_2} (R := R) 2
inst_6 : P.IsIrreducible
i : ι
⊢ Eq.{u_3 + 1} (α := Submodule R M) (span R (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) i)) : Submodule R M)
    (⊤ : Submodule R M)

Tactic:
IsIrreducible.eq_top_of_invtSubmodule_reflection (P := P) _ (fun j ↦ ?_) ?_

Premises used: 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 : NeZero.{u_2} (R := R) 2
inst_6 : P.IsIrreducible
i : ι
refine_1 :
  ∀ (j : ι),
    Membership.mem (α := Submodule R M) (invtSubmodule (↑(P.reflection j) : M →ₗ[R] M))
      (span R (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) i)) : Submodule R M)
refine_2 :
  Ne.{u_3 + 1} (α := Submodule R M) (span R (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) i)) : Submodule R M)
    (⊥ : Submodule R M)
⊢ Eq.{u_3 + 1} (α := Submodule R M) (span R (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) i)) : Submodule R M)
    (⊤ : Submodule R M)

Tactic:
refine IsIrreducible.eq_top_of_invtSubmodule_reflection (P := P) _ (fun j ↦ ?_) ?_

Premises used: 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 : NeZero.{u_2} (R := R) 2
inst_6 : P.IsIrreducible
i j : ι
g : ↥P.weylGroup := Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P j) ⋯
⊢ Membership.mem (α := Submodule R M) (invtSubmodule (↑(P.reflection j) : M →ₗ[R] M))
    (span R (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) i)) : Submodule R M)

Tactic:
Module.End.span_orbit_mem_invtSubmodule R (P.root i) g

Premises used: Set.Mem, setOf, RootPairing.root, Module.End.span_orbit_mem_invtSubmodule, DFunLike.coe
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : P.IsIrreducible
i j : ι
g : ↥P.weylGroup := Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P j) ⋯
⊢ Membership.mem (α := Submodule R M) (invtSubmodule (↑(P.reflection j) : M →ₗ[R] M))
    (span R (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) i)) : Submodule R M)

Tactic:
exact Module.End.span_orbit_mem_invtSubmodule R (P.root i) g

Premises used: RootPairing.root, Module.End.span_orbit_mem_invtSubmodule, DFunLike.coe
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : P.IsIrreducible
i : ι
⊢ Ne.{u_3 + 1} (α := Submodule R M) (span R (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) i)) : Submodule R M)
    (⊥ : Submodule R M)

Tactic:
simpa using ⟨P.root i, mem_orbit_self _, P.ne_zero 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 : NeZero.{u_2} (R := R) 2
inst_6 : P.IsIrreducible
B : P.InvariantForm
i j : ι
by_contra! :
  ∀
    (contra :
      ∀ (k : ι)
        (_ :
          Eq.{u_2 + 1} (α := R)
            ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) k : M) :
              R)
            ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) j : M) :
              R)),
        Eq.{u_2 + 1} (α := R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) k : M) :
            R)
          (0 : R)),
    False
⊢ ∃ (k : ι),
    Eq.{u_2 + 1} (α := R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) k : M) :
          R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R) ∧
      Ne.{u_2 + 1} (α := R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) k : M) :
          R)
        (0 : R)

Tactic:
by_contra! contra
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : P.IsIrreducible
B : P.InvariantForm
i j : ι
contra :
  ∀ (k : ι)
    (_ :
      Eq.{u_2 + 1} (α := R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) k : M) :
          R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) :
        R)
      (0 : R)
this :
  LE.le.{u_3} (α := Submodule R M) (span R (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) j)) : Submodule R M)
    (ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i)) :
      Submodule R M)
⊢ Eq (α := M →ₗ[R] R) ((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) (0 : M →ₗ[R] R)

Tactic:
simpa [span_orbit_eq_top] using this

Premises used: RootPairing.span_orbit_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 : NeZero.{u_2} (R := R) 2
inst_6 : P.IsIrreducible
B : P.InvariantForm
i j : ι
contra :
  ∀ (k : ι)
    (_ :
      Eq.{u_2 + 1} (α := R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) k : M) :
          R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) :
        R)
      (0 : R)
suffices :
  LE.le.{u_3} (α := Submodule R M) (span R (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) j)) : Submodule R M)
    (ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i)) :
      Submodule R M)
⊢ False

Tactic:
suffices span R (orbit P.weylGroup (P.root j)) ≤ ker (B.form (P.root i)) from
    B.apply_root_ne_zero i <| by simpa [span_orbit_eq_top] 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 : NeZero.{u_2} (R := R) 2
inst_6 : P.IsIrreducible
B : P.InvariantForm
i j : ι
contra :
  ∀ (k : ι)
    (_ :
      Eq.{u_2 + 1} (α := R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) k : M) :
          R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) :
        R)
      (0 : R)
⊢ LE.le.{u_3} (α := Submodule R M) (span R (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) j)) : Submodule R M)
    (ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i)) :
      Submodule R M)

Tactic:
span_le.mpr fun v hv ↦ ?_

Premises used: Iff.mpr, Submodule.span_le
-- 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 : NeZero.{u_2} (R := R) 2
inst_6 : P.IsIrreducible
B : P.InvariantForm
i j : ι
contra :
  ∀ (k : ι)
    (_ :
      Eq.{u_2 + 1} (α := R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) k : M) :
          R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) :
        R)
      (0 : R)
refine :
  ∀ (v : M) (hv : Membership.mem (γ := Set M) (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) j) : Set M) v),
    v ∈
      (↑(ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i))) :
        Set M)
⊢ LE.le.{u_3} (α := Submodule R M) (span R (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) j)) : Submodule R M)
    (ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i)) :
      Submodule R M)

Tactic:
refine span_le.mpr fun v hv ↦ ?_

Premises used: Iff.mpr, Submodule.span_le