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 : 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)
have 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)
Tactic: refine IsIrreducible.eq_top_of_invtSubmodule_reflection (P := P) _ (fun j ↦ ?_) ?_
-- 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 : 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)
⊢ Eq.{u_3 + 1} (α := Submodule R M) (span R (orbit (↥P.weylGroup) ((P.root : (a : ι) → M) i)) : Submodule R M)
    (⊤ : Submodule R M)
have 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)
Tactic: refine IsIrreducible.eq_top_of_invtSubmodule_reflection (P := P) _ (fun j ↦ ?_) ?_
-- 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 : P.IsIrreducible
B : P.InvariantForm
i j : ι
⊢ ∃ (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)
have 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
Tactic: by_contra! contra
-- 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 : 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)
⊢ False
have 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)
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
-- 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 : 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)
have 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)
Tactic: refine span_le.mpr fun v hv ↦ ?_
-- 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 : 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
⊢ v ∈
    (↑(ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i))) :
      Set M)
have 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)
Tactic: obtain ⟨g, rfl⟩ := mem_orbit_iff.mp hv
Cleared hypotheses: v, hv
-- 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 : 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))
⊢ 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)
have 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)
Tactic: simp only [P.weylGroup_apply_root, SetLike.mem_coe, LinearMap.mem_ker]
-- 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 : 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) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) ((((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) g : ι ≃ ι) : (a : ι) → ι) j : ι) :
          M) :
      R)
    (0 : R)
have _ : 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: apply contra
-- 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 : 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)
have 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)
Tactic: by_cases hj : P.root j ∈ span R (P.root '' s)
-- 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 : 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)
⊢ span R ((⇑P.root : (a : ι) → M) '' s) ∈ invtSubmodule (↑(P.reflection j) : M →ₗ[R] M)
have 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)
Tactic: by_cases hj : P.root j ∈ span R (P.root '' s)
-- 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 : 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)
have 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))
Tactic: refine (Module.End.mem_invtSubmodule _).mpr fun x hx ↦ ?_
-- 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 : 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
⊢ x ∈ Submodule.comap (↑(P.reflection j) : M →ₗ[R] M) (span R ((⇑P.root : (a : ι) → M) '' s))
have 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)
Tactic: rwa [Submodule.mem_comap, LinearEquiv.coe_coe,
        (isFixedPt_reflection_of_isOrthogonal (h _ hj) hx).eq]
-- 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 : 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)
⊢ x ∈ Submodule.comap (↑(P.reflection j) : M →ₗ[R] M) (span R ((⇑P.root : (a : ι) → M) '' s))
have neg₁ : Membership.mem (α := M) (γ := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s))
  ((P.reflection j : (a : M) → M) x : M)
Tactic: rwa [Submodule.mem_comap, LinearEquiv.coe_coe,
        (isFixedPt_reflection_of_isOrthogonal (h _ hj) hx).eq]
-- 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 : 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
⊢ Eq.{u_3 + 1} (α := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) ⊤
have hq : ∀ (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]
-- 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 : 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)
⊢ Eq.{u_3 + 1} (α := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) ⊤
have apply : Ne.{u_3 + 1} (α := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' s)) ⊥
Tactic: apply IsIrreducible.eq_top_of_invtSubmodule_reflection _ 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 : 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
⊢ q = ⊤
have obtain : ∀ (Φ : Set ι) (b : ∀ i ∈ Φ, ¬Disjoint q (span K (singleton (α := M) ((P.root : (a : ι) → M) i : M))))
  (c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)), q = ⊤
Tactic: obtain ⟨Φ, b, c⟩ := P.exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule q h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : 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)
⊢ q = ⊤
have 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 = ⊤
Tactic: rcases Φ.eq_empty_or_nonempty with rfl | hΦ
Cleared hypotheses: Φ, b, c
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : 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 = ⊤
⊢ q = ⊤
have inr : ∀ (hΦ : Φ.Nonempty), q = ⊤
Tactic: rcases Φ.eq_empty_or_nonempty with rfl | 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 : 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 = ⊤
have c₁ : q ≤ ⨅ (i : ι), ker (P.coroot' i)
Tactic: replace c : q ≤ ⨅ i, LinearMap.ker (P.coroot' i) := by simpa using c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
inst_6 : P.IsRootSystem
q : 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
⊢ q = ⊤
have b₁ : (⇑P.root : (a : ι) → M) '' Φ ⊆ (↑q : Set M)
Tactic: replace b : P.root '' Φ ⊆ q := by
      simpa [Submodule.disjoint_span_singleton' (P.ne_zero _)] using b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
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
⊢ P.flip.IsValuedIn S
have rw : ∀ (b a : ι), ∃ (s : S), (algebraMap S R : (a : S) → R) s = P.flip.pairing a b
Tactic: rw [isValuedIn_iff, forall_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
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
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
i j k l : ι
h : (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) l : M)
⊢ P.pairingIn S k j = P.pairingIn S i j + P.pairingIn S l j
have a : Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S k j) : R)
  ((algebraMap S R : (a : S) → R) (P.pairingIn S i j + P.pairingIn S l j) : R)
Tactic: apply FaithfulSMul.algebraMap_injective S R