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 : 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)
v : M
hv : Membership.mem (γ := Set M) (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) j) : Set M) v
obtain :
  ∀ (g : ↥P.weylGroup)
    (hv :
      Membership.mem (γ := Set M) (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) j) : Set M)
        (HSMul.hSMul (β := M) g ((P.root : (a : ι) → M) j : M))),
    HSMul.hSMul (β := M) g ((P.root : (a : ι) → M) j : M) ∈
      (↑(ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i))) :
        Set M)
⊢ v ∈
    (↑(ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i))) :
      Set M)

Tactic:
obtain ⟨g, rfl⟩ := mem_orbit_iff.mp hv

Premises used: MulAction.mem_orbit_iff, Iff.mp, 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 : 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)
g : ↥P.weylGroup
hv :
  Membership.mem (γ := Set M) (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) j) : Set M)
    (HSMul.hSMul (β := M) g ((P.root : (a : ι) → M) j : M))
simp :
  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) ((((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) g : ι ≃ ι) : (a : ι) → ι) j : ι) :
          M) :
      R)
    (0 : R)
⊢ HSMul.hSMul (β := M) g ((P.root : (a : ι) → M) j : M) ∈
    (↑(ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i))) :
      Set M)

Tactic:
simp only [P.weylGroup_apply_root, SetLike.mem_coe, LinearMap.mem_ker]

Premises used: RootPairing.weylGroup_apply_root, LinearMap.mem_ker, SetLike.mem_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
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)
g : ↥P.weylGroup
hv :
  Membership.mem (γ := Set M) (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) j) : Set M)
    (HSMul.hSMul (β := M) g ((P.root : (a : ι) → M) j : M))
_ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R)
              ((P.root : (a : ι) → M)
                ((((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) g : ι ≃ ι) : (a : ι) → ι) j : ι)) :
            M →ₗ[R] R) :
          (a : M) → R)
        ((P.root : (a : ι) → M) ((((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) g : ι ≃ ι) : (a : ι) → ι) j : ι) :
          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) ((((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) g : ι ≃ ι) : (a : ι) → ι) j : ι) :
          M) :
      R)
    (0 : R)

Tactic:
apply 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)
g : ↥P.weylGroup
hv :
  Membership.mem (γ := Set M) (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) j) : Set M)
    (HSMul.hSMul (β := M) g ((P.root : (a : ι) → M) j : M))
⊢ Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R)
              ((P.root : (a : ι) → M)
                ((((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) g : ι ≃ ι) : (a : ι) → ι) j : ι)) :
            M →ₗ[R] R) :
          (a : M) → R)
        ((P.root : (a : ι) → M) ((((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) g : ι ≃ ι) : (a : ι) → ι) j : ι) :
          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)

Tactic:
simp [← Subgroup.smul_def g]

Premises used: Subgroup.smul_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 : NeZero.{u_2} (R := R) 2
inst_6 : P.IsIrreducible
s : Set ι
hne : s.Nonempty
h : ∀ (j : ι), ((P.root : (a : ι) → M) j : M) ∉ span R ((⇑P.root : (a : ι) → M) '' s) → ∀ i ∈ s, P.IsOrthogonal j i
j : ι
pos :
  ∀
    (hj :
      Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) j : M)),
    span R ((⇑P.root : (a : ι) → M) '' s) ∈ invtSubmodule (↑(P.reflection j) : M →ₗ[R] M)
neg :
  ∀ (hj : ((P.root : (a : ι) → M) j : M) ∉ span R ((⇑P.root : (a : ι) → M) '' s)),
    span R ((⇑P.root : (a : ι) → M) '' s) ∈ invtSubmodule (↑(P.reflection j) : M →ₗ[R] M)
⊢ span R ((⇑P.root : (a : ι) → M) '' s) ∈ invtSubmodule (↑(P.reflection j) : M →ₗ[R] M)

Tactic:
by_cases hj : P.root j ∈ span R (P.root '' s)

Premises used: RootPairing.root, Submodule.span, Set.image, 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
s : Set ι
hne : s.Nonempty
h : ∀ (j : ι), ((P.root : (a : ι) → M) j : M) ∉ span R ((⇑P.root : (a : ι) → M) '' s) → ∀ i ∈ s, P.IsOrthogonal j i
j : ι
hj :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s))
    ((P.root : (a : ι) → M) j : M)
⊢ span R ((⇑P.root : (a : ι) → M) '' s) ∈ invtSubmodule (↑(P.reflection j) : M →ₗ[R] M)

Tactic:
Submodule.mem_invtSubmodule_reflection_of_mem _ _ hj

Premises used: Submodule.mem_invtSubmodule_reflection_of_mem, 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 : P.IsIrreducible
s : Set ι
hne : s.Nonempty
h : ∀ (j : ι), ((P.root : (a : ι) → M) j : M) ∉ span R ((⇑P.root : (a : ι) → M) '' s) → ∀ i ∈ s, P.IsOrthogonal j i
j : ι
hj :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s))
    ((P.root : (a : ι) → M) j : M)
⊢ span R ((⇑P.root : (a : ι) → M) '' s) ∈ invtSubmodule (↑(P.reflection j) : M →ₗ[R] M)

Tactic:
exact Submodule.mem_invtSubmodule_reflection_of_mem _ _ hj

Premises used: Submodule.mem_invtSubmodule_reflection_of_mem
-- 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
s : Set ι
hne : s.Nonempty
h : ∀ (j : ι), ((P.root : (a : ι) → M) j : M) ∉ span R ((⇑P.root : (a : ι) → M) '' s) → ∀ i ∈ s, P.IsOrthogonal j i
j : ι
hj : ((P.root : (a : ι) → M) j : M) ∉ span R ((⇑P.root : (a : ι) → M) '' s)
⊢ span R ((⇑P.root : (a : ι) → M) '' s) ∈ invtSubmodule (↑(P.reflection j) : M →ₗ[R] M)

Tactic:
(Module.End.mem_invtSubmodule _).mpr fun x hx ↦ ?_

Premises used: Iff.mpr, Module.End.mem_invtSubmodule
-- 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
s : Set ι
hne : s.Nonempty
h : ∀ (j : ι), ((P.root : (a : ι) → M) j : M) ∉ span R ((⇑P.root : (a : ι) → M) '' s) → ∀ i ∈ s, P.IsOrthogonal j i
j : ι
hj : ((P.root : (a : ι) → M) j : M) ∉ span R ((⇑P.root : (a : ι) → M) '' s)
neg :
  ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) x),
    x ∈ Submodule.comap (↑(P.reflection j) : M →ₗ[R] M) (span R ((⇑P.root : (a : ι) → M) '' s))
⊢ span R ((⇑P.root : (a : ι) → M) '' s) ∈ invtSubmodule (↑(P.reflection j) : M →ₗ[R] M)

Tactic:
refine (Module.End.mem_invtSubmodule _).mpr fun x hx ↦ ?_

Premises used: Iff.mpr, Module.End.mem_invtSubmodule
-- 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
s : Set ι
hne : s.Nonempty
h : ∀ (j : ι), ((P.root : (a : ι) → M) j : M) ∉ span R ((⇑P.root : (a : ι) → M) '' s) → ∀ i ∈ s, P.IsOrthogonal j i
j : ι
hj : ((P.root : (a : ι) → M) j : M) ∉ span R ((⇑P.root : (a : ι) → M) '' s)
x : M
hx : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) x
neg :
  Membership.mem (α := M) (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s))
    (((↑(P.reflection j) : M →ₗ[R] M) : (a : M) → M) x : M)
neg₁ :
  Membership.mem (α := M) (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s))
    ((P.reflection j : (a : M) → M) x : M)
neg₂ neg₃ neg₄ neg₅ : Membership.mem (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) x
⊢ x ∈ Submodule.comap (↑(P.reflection j) : M →ₗ[R] M) (span R ((⇑P.root : (a : ι) → M) '' s))

Tactic:
rwa [Submodule.mem_comap, LinearEquiv.coe_coe,
        (isFixedPt_reflection_of_isOrthogonal (h _ hj) hx).eq]

Premises used: Submodule.mem_comap, Function.IsFixedPt.eq, RootPairing.isFixedPt_reflection_of_isOrthogonal, LinearEquiv.coe_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
s : Set ι
hne : s.Nonempty
h : ∀ (j : ι), ((P.root : (a : ι) → M) j : M) ∉ span R ((⇑P.root : (a : ι) → M) '' s) → ∀ i ∈ s, P.IsOrthogonal j i
⊢ ∀ (j : ι), span R ((⇑P.root : (a : ι) → M) '' s) ∈ invtSubmodule (↑(P.reflection j) : M →ₗ[R] M)

Tactic:
have hq (j : ι) : span R (P.root '' s) ∈ Module.End.invtSubmodule (P.reflection j) := by
    by_cases hj : P.root j ∈ span R (P.root '' s)
    · exact Submodule.mem_invtSubmodule_reflection_of_mem _ _ hj
    · refine (Module.End.mem_invtSubmodule _).mpr fun x hx ↦ ?_
      rwa [Submodule.mem_comap, LinearEquiv.coe_coe,
        (isFixedPt_reflection_of_isOrthogonal (h _ hj) hx).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 : P.IsIrreducible
s : Set ι
hne : s.Nonempty
h : ∀ (j : ι), ((P.root : (a : ι) → M) j : M) ∉ span R ((⇑P.root : (a : ι) → M) '' s) → ∀ i ∈ s, P.IsOrthogonal j i
hq : ∀ (j : ι), span R ((⇑P.root : (a : ι) → M) '' s) ∈ invtSubmodule (↑(P.reflection j) : M →ₗ[R] M)
apply : Ne.{u_3 + 1} (α := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) ⊥
⊢ Eq.{u_3 + 1} (α := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) ⊤

Tactic:
apply IsIrreducible.eq_top_of_invtSubmodule_reflection _ hq

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
s : Set ι
hne : s.Nonempty
h : ∀ (j : ι), ((P.root : (a : ι) → M) j : M) ∉ span R ((⇑P.root : (a : ι) → M) '' s) → ∀ i ∈ s, P.IsOrthogonal j i
hq : ∀ (j : ι), span R ((⇑P.root : (a : ι) → M) '' s) ∈ invtSubmodule (↑(P.reflection j) : M →ₗ[R] M)
⊢ Ne.{u_3 + 1} (α := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) ⊥

Tactic:
simpa using ⟨hne.choose, hne.choose_spec, P.ne_zero _⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
h₂ :
  ∀ (Φ : Set ι), Φ.Nonempty → (⇑P.root : (a : ι) → M) '' Φ ⊆ (↑q : Set M) → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
obtain :
  ∀ (Φ : Set ι) (b : ∀ i ∈ Φ, ¬Disjoint q (span K (singleton (α := M) ((P.root : (a : ι) → M) i : M))))
    (c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)), q = ⊤
⊢ q = ⊤

Tactic:
obtain ⟨Φ, b, c⟩ := P.exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule q h₁

Premises used: RootPairing.exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
h₂ :
  ∀ (Φ : Set ι), Φ.Nonempty → (⇑P.root : (a : ι) → M) '' Φ ⊆ (↑q : Set M) → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
Φ : Set ι
b : ∀ i ∈ Φ, ¬Disjoint q (span K (singleton (α := M) ((P.root : (a : ι) → M) i : M)))
c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)
inl :
  ∀
    (b :
      ∀ (i : ι),
        Membership.mem (γ := Set ι) ∅ i → ¬Disjoint q (span K (singleton (α := M) ((P.root : (a : ι) → M) i : M))))
    (c : ∀ i ∉ ∅, q ≤ ker (P.coroot' i)), q = ⊤
inr : ∀ (hΦ : Φ.Nonempty), q = ⊤
⊢ q = ⊤

Tactic:
rcases Φ.eq_empty_or_nonempty with rfl | hΦ

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
h₂ :
  ∀ (Φ : Set ι), Φ.Nonempty → (⇑P.root : (a : ι) → M) '' Φ ⊆ (↑q : Set M) → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
b :
  ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ¬Disjoint q (span K (singleton (α := M) ((P.root : (a : ι) → M) i : M)))
c : ∀ i ∉ ∅, q ≤ ker (P.coroot' i)
⊢ q ≤ ⨅ (i : ι), ker (P.coroot' i)

Tactic:
simpa using c
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
h₂ :
  ∀ (Φ : Set ι), Φ.Nonempty → (⇑P.root : (a : ι) → M) '' Φ ⊆ (↑q : Set M) → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
b :
  ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ¬Disjoint q (span K (singleton (α := M) ((P.root : (a : ι) → M) i : M)))
c : ∀ i ∉ ∅, q ≤ ker (P.coroot' i)
⊢ q ≤ ⨅ (i : ι), ker (P.coroot' i)

Tactic:
replace c : q ≤ ⨅ i, LinearMap.ker (P.coroot' i) := by simpa using c
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
h₂ :
  ∀ (Φ : Set ι), Φ.Nonempty → (⇑P.root : (a : ι) → M) '' Φ ⊆ (↑q : Set M) → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
b :
  ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ¬Disjoint q (span K (singleton (α := M) ((P.root : (a : ι) → M) i : M)))
c : q ≤ ⨅ (i : ι), ker (P.coroot' i)
⊢ q = ⊤

Tactic:
simp [h₀, ← P.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot'] at c

Premises used: RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot'
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
h₂ :
  ∀ (Φ : Set ι), Φ.Nonempty → (⇑P.root : (a : ι) → M) '' Φ ⊆ (↑q : Set M) → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
Φ : Set ι
b : ∀ i ∈ Φ, ¬Disjoint q (span K (singleton (α := M) ((P.root : (a : ι) → M) i : M)))
c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)
hΦ : Φ.Nonempty
⊢ (⇑P.root : (a : ι) → M) '' Φ ⊆ (↑q : Set M)

Tactic:
simpa [Submodule.disjoint_span_singleton' (P.ne_zero _)] using b

Premises used: Submodule.disjoint_span_singleton', RootPairing.ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
h₂ :
  ∀ (Φ : Set ι), Φ.Nonempty → (⇑P.root : (a : ι) → M) '' Φ ⊆ (↑q : Set M) → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
Φ : Set ι
b : ∀ i ∈ Φ, ¬Disjoint q (span K (singleton (α := M) ((P.root : (a : ι) → M) i : M)))
c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)
hΦ : Φ.Nonempty
⊢ (⇑P.root : (a : ι) → M) '' Φ ⊆ (↑q : Set M)

Tactic:
replace b : P.root '' Φ ⊆ q := by
      simpa [Submodule.disjoint_span_singleton' (P.ne_zero _)] using b
-- Module: Mathlib.LinearAlgebra.RootSystem.Irreducible
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
h₂ :
  ∀ (Φ : Set ι), Φ.Nonempty → (⇑P.root : (a : ι) → M) '' Φ ⊆ (↑q : Set M) → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
Φ : Set ι
c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)
hΦ : Φ.Nonempty
b : (⇑P.root : (a : ι) → M) '' Φ ⊆ (↑q : Set M)
⊢ q = ⊤

Tactic:
simpa [h₂ Φ hΦ b c, ← span_le] using b

Premises used: Submodule.span_le
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
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_1 j_1 i j : ι
⊢ ∃ (s : R), (algebraMap R R : (a : R) → R) s = P.pairing i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
⊢ P.IsValuedIn S ↔
    ∀ (i j : ι),
      Membership.mem (γ := Set R) (range.{u_2, u_6 + 1} (ι := S) (⇑(algebraMap S R) : (a : S) → R)) (P.pairing i j)

Tactic:
simp only [isValuedIn_iff, mem_range]

Premises used: Set.mem_range, RootPairing.isValuedIn_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
S_1 : Type u_3
M : Type u_4
N : Type u_5
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 j : ι
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : P.IsValuedIn S
rw : ∀ (b a : ι), ∃ (s : S), (algebraMap S R : (a : S) → R) s = P.flip.pairing a b
⊢ P.flip.IsValuedIn S

Tactic:
rw [isValuedIn_iff, forall_comm]

Premises used: forall_comm, RootPairing.isValuedIn_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
S_1 : Type u_3
M : Type u_4
N : Type u_5
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 j : ι
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : P.IsValuedIn S
⊢ ∀ (b a : ι), ∃ (s : S), (algebraMap S R : (a : S) → R) s = P.flip.pairing a b

Tactic:
P.exists_value

Premises used: RootPairing.pairing, RootPairing.flip, RootPairing.exists_value
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
S_1 : Type u_3
M : Type u_4
N : Type u_5
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 j : ι
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : P.IsValuedIn S
⊢ ∀ (b a : ι), ∃ (s : S), (algebraMap S R : (a : S) → R) s = P.flip.pairing a b

Tactic:
exact P.exists_value

Premises used: RootPairing.exists_value