awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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 j : ι
⊢ Eq (α := ι) (((↑(reflection P i)⁻¹ : P.Hom P).indexEquiv : (a : ι) → ι) j : ι)
    (((↑(reflection P i) : P.Hom P).indexEquiv : (a : ι) → ι) j : ι)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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 : ι
⊢ (↑(reflection P i)⁻¹ : P.Hom P).indexEquiv = (↑(reflection P i) : P.Hom P).indexEquiv

Tactic:
exact _root_.Equiv.ext (fun j => by simp)

Premises used: Equiv.ext
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
w : P.Aut
⊢ Eq.{u_3 + 1} (α := M) ((((weightHom P : (a : P.Aut) → M ≃ₗ[R] M) w : M ≃ₗ[R] M) : (a : M) → M) 0 : M) (0 : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
w : P.Aut
x y : M
⊢ (((weightHom P : (a : P.Aut) → M ≃ₗ[R] M) w : M ≃ₗ[R] M) : (a : M) → M) (x + y) =
    HAdd.hAdd (α := M) (β := M) ((((weightHom P : (a : P.Aut) → M ≃ₗ[R] M) w : M ≃ₗ[R] M) : (a : M) → M) x : M)
      ((((weightHom P : (a : P.Aut) → M ≃ₗ[R] M) w : M ≃ₗ[R] M) : (a : M) → M) y : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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 : ι
x : M
⊢ reflection P i • x = (P.reflection i : (a : M) → M) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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 : ι
g : P.Aut
⊢ (P.root : (a : ι) → M) (((↑g : P.Hom P).indexEquiv : (a : ι) → ι) i : ι) =
    HSMul.hSMul (β := M) g ((P.root : (a : ι) → M) i : M)

Tactic:
simpa using (congr_fun g.root_weightMap i).symm

Premises used: RootPairing.Hom.root_weightMap, RootPairing.Equiv.toHom, congr_fun, Eq.symm
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
w : P.Autᵐᵒᵖ
⊢ Eq.{u_4 + 1} (α := N) ((unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) 0 : N) (0 : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
w : P.Autᵐᵒᵖ
x y : N
change :
  (unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) (x + y) =
    HAdd.hAdd (α := N) (β := N) ((unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) x : N)
      ((unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) y : N)
⊢ w • (x + y) = w • x + w • y

Tactic:
change unop (coweightHom P _) (x + y) = unop (coweightHom P _) x + unop (coweightHom P _) y

Premises used: HAdd.hAdd, MulOpposite.unop, DFunLike.coe, RootPairing.Equiv.coweightHom
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
w : P.Autᵐᵒᵖ
x y : N
⊢ (unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) (x + y) =
    HAdd.hAdd (α := N) (β := N) ((unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) x : N)
      ((unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) y : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
w : P.Aut
t : R
x : M
⊢ (((weightHom P : (a : P.Aut) → M ≃ₗ[R] M) w : M ≃ₗ[R] M) : (a : M) → M) (t • x) =
    HSMul.hSMul (β := M) t ((((weightHom P : (a : P.Aut) → M ≃ₗ[R] M) w : M ≃ₗ[R] M) : (a : M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
w : P.Autᵐᵒᵖ
t : R
x : N
change :
  (unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) (t • x) =
    HSMul.hSMul (β := N) t ((unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) x : N)
⊢ w • t • x = t • w • x

Tactic:
change unop (coweightHom P (unop w)) (t • x) = t • unop (coweightHom P (unop w)) x

Premises used: MulOpposite.unop, HSMul.hSMul, DFunLike.coe, RootPairing.Equiv.coweightHom
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
w : P.Autᵐᵒᵖ
t : R
x : N
⊢ (unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) (t • x) =
    HSMul.hSMul (β := N) t ((unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) x : N)

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
q : Submodule R M
⊢ q ∈ P.invtRootSubmodule ↔ ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)

Tactic:
simp [invtRootSubmodule]

Premises used: RootPairing.invtRootSubmodule
-- 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
⊢ ⊤ ∈ P.invtRootSubmodule

Tactic:
simp [invtRootSubmodule]

Premises used: RootPairing.invtRootSubmodule
-- 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
⊢ ⊥ ∈ P.invtRootSubmodule

Tactic:
simp [invtRootSubmodule]

Premises used: RootPairing.invtRootSubmodule
-- 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
x : ↥P.invtRootSubmodule
p : Submodule R M
hp : p ∈ P.invtRootSubmodule
⊢ Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ P.invtRootSubmodule) p hp ≤
    Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ P.invtRootSubmodule) ⊤ ⋯

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
x : ↥P.invtRootSubmodule
p : Submodule R M
hp : p ∈ P.invtRootSubmodule
⊢ Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ P.invtRootSubmodule) ⊥ ⋯ ≤
    Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ P.invtRootSubmodule) p hp

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 : Nontrivial M
rw : ¬Eq.{u_3 + 1} (α := Submodule R M) (↑⊥ : Submodule R M) (↑⊤ : Submodule R M)
⊢ Ne.{u_3 + 1} (α := ↥P.invtRootSubmodule) ⊥ ⊤

Tactic:
rw [ne_eq, Subtype.ext_iff]

Premises used: ne_eq, Subtype.ext_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 : Nontrivial M
⊢ ¬Eq.{u_3 + 1} (α := Submodule R M) (↑⊥ : Submodule R M) (↑⊤ : Submodule R M)

Tactic:
bot_ne_top

Premises used: bot_ne_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
⊢ ¬Eq.{u_3 + 1} (α := Submodule R M) (↑⊥ : Submodule R M) (↑⊤ : Submodule R M)

Tactic:
exact bot_ne_top

Premises used: bot_ne_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
⊢ Eq.{u_3 + 1} (α := Submodule R M) (↑⊥ : Submodule R M) ⊥

Tactic:
rfl

Premises used: 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
⊢ Eq.{u_3 + 1} (α := Submodule R M) (↑⊤ : Submodule R M) ⊤

Tactic:
rfl

Premises used: 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 : P.IsRootSystem
x : M
h : x = 0
⊢ ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((P.coroot' i : (a : M) → R) x : R) (0 : R)

Tactic:
simp [h]
-- 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.IsRootSystem
x : M
refine : ∀ (h : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((P.coroot' i : (a : M) → R) x : R) (0 : R)), x = 0
⊢ x = 0 ↔ ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((P.coroot' i : (a : M) → R) x : R) (0 : R)

Tactic:
refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩
-- 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.IsRootSystem
x : M
h : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((P.coroot' i : (a : M) → R) x : R) (0 : R)
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ι), ker (P.coroot' i)) x

Tactic:
aesop
-- 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.IsRootSystem
x : M
h : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((P.coroot' i : (a : M) → R) x : R) (0 : R)
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ι), ker (P.coroot' i)) x

Tactic:
replace h : x ∈ ⨅ i, ker (P.coroot' i) := by aesop
-- 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.IsRootSystem
x : M
h : Membership.mem (γ := Submodule R M) (⨅ (i : ι), ker (P.coroot' i)) x
⊢ x = 0

Tactic:
simpa [← P.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot'] using h

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
q : ↥P.invtRootSubmodule
k : ι
hk : ((P.root : (a : ι) → M) k : M) ∉ (↑q : Submodule K M)
⊢ (↑q : Submodule K M) ≤ ker (P.coroot' k)

Tactic:
(Submodule.mem_invtSubmodule_reflection_iff (P.flip.root_coroot_two k)
    (Submodule.disjoint_span_singleton_of_notMem hk)).mp
    (P.mem_invtRootSubmodule_iff.mp q.property k)

Premises used: RootPairing.root_coroot_two, Set.Mem, RootPairing.mem_invtRootSubmodule_iff, RootPairing.flip, Submodule.disjoint_span_singleton_of_notMem, Iff.mp, Submodule.mem_invtSubmodule_reflection_iff, Subtype.property
-- 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 : ↥P.invtRootSubmodule
h : q = ⊥
⊢ ∀ (i : ι), ((P.root : (a : ι) → M) i : M) ∉ (↑q : Submodule K M)

Tactic:
simp [h, P.ne_zero]

Premises used: 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 : ↥P.invtRootSubmodule
refine : ∀ (h : ∀ (i : ι), ((P.root : (a : ι) → M) i : M) ∉ (↑q : Submodule K M)), q = ⊥
⊢ q = ⊥ ↔ ∀ (i : ι), ((P.root : (a : ι) → M) i : M) ∉ (↑q : Submodule K M)

Tactic:
refine ⟨fun h ↦ by simp [h, P.ne_zero], fun h ↦ ?_⟩
-- 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 : ↥P.invtRootSubmodule
h : ∀ (i : ι), ((P.root : (a : ι) → M) i : M) ∉ (↑q : Submodule K M)
simp_rw : ∀ x ∈ (↑q : Submodule K M), ∀ (i : ι), x ∈ ker (P.coroot' i)
⊢ q = ⊥

Tactic:
simp_rw [Subtype.mk_eq_bot_iff (invtRootSubmodule.bot_mem P), Submodule.eq_bot_iff,
    P.eq_zero_iff_forall_coroot'_eq_zero, ← LinearMap.mem_ker]

Premises used: RootPairing.invtRootSubmodule.bot_mem, LinearMap.mem_ker, RootPairing.eq_zero_iff_forall_coroot'_eq_zero, Submodule.eq_bot_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 : 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 : ↥P.invtRootSubmodule
h : ∀ (i : ι), ((P.root : (a : ι) → M) i : M) ∉ (↑q : Submodule K M)
⊢ ∀ x ∈ (↑q : Submodule K M), ∀ (i : ι), x ∈ ker (P.coroot' i)

Tactic:
fun x hx i ↦ invtRootSubmodule.le_ker_coroot' q (h i) hx

Premises used: RootPairing.invtRootSubmodule.le_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 : ↥P.invtRootSubmodule
h : ∀ (i : ι), ((P.root : (a : ι) → M) i : M) ∉ (↑q : Submodule K M)
⊢ ∀ x ∈ (↑q : Submodule K M), ∀ (i : ι), x ∈ ker (P.coroot' i)

Tactic:
exact fun x hx i ↦ invtRootSubmodule.le_ker_coroot' q (h i) hx

Premises used: RootPairing.invtRootSubmodule.le_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 : Module K M
inst_4 : Module K N
P : RootPairing ι K M N
inst_5 : P.IsRootSystem
q : ↥P.invtRootSubmodule
h : q = ⊤
⊢ range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M) ⊆ (↑(↑q : Submodule K M) : Set M)

Tactic:
simp [h]
-- 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
P : RootPairing ι K M N
inst_5 : P.IsRootSystem
q : ↥P.invtRootSubmodule
h : range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M) ⊆ (↑(↑q : Submodule K M) : Set M)
⊢ q = ⊤

Tactic:
simpa using Submodule.span_mono h (R := K)

Premises used: Submodule.span_mono
-- 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 : ↥P.invtRootSubmodule
set :
  let Q := (↑q : Submodule K M);
  Q =
    span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
⊢ (↑q : Submodule K M) =
    span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) (↑q : Submodule K M) ((P.root : (a : ι) → M) i : M)})

Tactic:
set Q := (q : Submodule K M)

Premises used: Subtype.val
-- 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 : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
⊢ span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)}) ≤
    Q

Tactic:
have hSQ : span K (P.root '' {i | P.root i ∈ Q}) ≤ Q :=
    span_le.mpr (Set.image_subset_iff.mpr fun _ h => h)
-- 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 : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
hSQ :
  span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)}) ≤
    Q
⊢ Q =
    span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})

Tactic:
le_antisymm ?_ hSQ

Premises used: le_antisymm
-- 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 : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
hSQ :
  span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)}) ≤
    Q
refine :
  Q ≤
    span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
⊢ Q =
    span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})

Tactic:
refine le_antisymm ?_ hSQ

Premises used: le_antisymm
-- 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 : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
hSQ :
  span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)}) ≤
    Q
set :
  let S : Submodule K M :=
    span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)});
  ∀ (hSQ : S ≤ Q), Q ≤ S
⊢ Q ≤
    span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})

Tactic:
set S := span K (P.root '' {i | P.root i ∈ Q})

Premises used: setOf, Membership.mem, RootPairing.root, Submodule.span, Set.image, DFunLike.coe
-- 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 : ↥P.invtRootSubmodule
Q : Submodule K M := (↑q : Submodule K M)
S : Submodule K M :=
  span K
    (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
      {i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)})
hSQ : S ≤ Q
T : Submodule K M :=
  span K (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})
rw :
  Eq.{u_3 + 1} (α := Submodule K M)
    (span K
      (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M)
        ({i : ι | Membership.mem (α := M) Q ((P.root : (a : ι) → M) i : M)} ∪
          {i : ι | ((P.root : (a : ι) → M) i : M) ∉ Q})))
    ⊤
⊢ S ⊔ T = ⊤

Tactic:
rw [← Submodule.span_union, ← Set.image_union]

Premises used: Submodule.span_union, Set.image_union