mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x✝ : ↥P.invtRootSubmodule
q : Submodule K M
hq : q ∈ P.invtRootSubmodule
⊢ ⟨q, hq⟩ = ⊥ ∨ ⟨q, hq⟩ = ⊤

pp: case refine_2
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : IsSimpleOrder ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq' : q ≠ ⊥
⊢ q = ⊤

Tactic:
·

Goal state after:
case refine_1
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x✝ : ↥P.invtRootSubmodule
q : Submodule K M
hq : q ∈ P.invtRootSubmodule
⊢ ⟨q, hq⟩ = ⊥ ∨ ⟨q, hq⟩ = ⊤
Module: Mathlib.Data.Int.ConditionallyCompleteOrder

Goal state before:
pp: s : Set ℤ
inst✝ : DecidablePred fun x ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ z, z ∈ s
⊢ sInf s = ↑(b.leastOfBdd Hb Hinh)

Tactic:
have : s.Nonempty ∧ BddBelow s := ⟨Hinh, b, Hb⟩

Goal state after:
s : Set ℤ
inst✝ : DecidablePred fun x ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ z, z ∈ s
this : s.Nonempty ∧ BddBelow s
⊢ sInf s = ↑(b.leastOfBdd Hb Hinh)
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : IsSimpleOrder ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq' : q ≠ ⊥
⊢ q = ⊤

Tactic:
·

Goal state after:
case refine_2
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : IsSimpleOrder ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq' : q ≠ ⊥
⊢ q = ⊤
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : IsSimpleOrder ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq' : q ≠ ⊥
⊢ q = ⊤

Tactic:
let q' : P.invtRootSubmodule := ⟨q, P.mem_invtRootSubmodule_iff.mpr hq⟩

Goal state after:
case refine_2
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : IsSimpleOrder ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq' : q ≠ ⊥
q' : ↥P.invtRootSubmodule := ⟨q, ⋯⟩
⊢ q = ⊤
Module: Mathlib.Order.Interval.Set.OrdConnectedLinear

Goal state before:
pp: case refine_1
α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
h' : I.OrdConnected
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : Ioo x y ⊆ Iᶜ
⊢ Ioo x y = ∅

pp: case refine_2
α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : x < y
z : α
hz : z ∈ Ioo x y
⊢ z ∈ I

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
h' : I.OrdConnected
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : Ioo x y ⊆ Iᶜ
⊢ Ioo x y = ∅
Module: Mathlib.Order.Interval.Set.OrdConnectedLinear

Goal state before:
pp: case refine_2
α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : x < y
z : α
hz : z ∈ Ioo x y
⊢ z ∈ I

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : x < y
z : α
hz : z ∈ Ioo x y
⊢ z ∈ I
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : NeZero 2
inst✝ : P.IsIrreducible
i j : ι
⊢ span R (orbit (↥P.weylGroup) (P.root i)) ∈ invtSubmodule ↑(P.reflection j)

pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : NeZero 2
inst✝ : P.IsIrreducible
i : ι
⊢ span R (orbit (↥P.weylGroup) (P.root i)) ≠ ⊥

Tactic:
·

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : NeZero 2
inst✝ : P.IsIrreducible
i j : ι
⊢ span R (orbit (↥P.weylGroup) (P.root i)) ∈ invtSubmodule ↑(P.reflection j)
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : NeZero 2
inst✝ : P.IsIrreducible
i : ι
⊢ span R (orbit (↥P.weylGroup) (P.root i)) ≠ ⊥

Tactic:
·

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : NeZero 2
inst✝ : P.IsIrreducible
i : ι
⊢ span R (orbit (↥P.weylGroup) (P.root i)) ≠ ⊥
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case he
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁴ : CommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : Module R N₂
P✝ : RootPairing ι R M N
Q✝ : RootPairing ι₂ R M₂ N₂
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Module.IsTorsionFree R M₂
inst✝² : Finite ι₂
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst✝ : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf : ∀ (i : ι), f (P.root i) = Q.root (e i)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
x✝¹ : M₂
x✝ : N₂
⊢ (Q.toLinearMap x✝¹) x✝ = ((RootPairing.map e f g).toLinearMap x✝¹) x✝

pp: case hr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁴ : CommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : Module R N₂
P✝ : RootPairing ι R M N
Q✝ : RootPairing ι₂ R M₂ N₂
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Module.IsTorsionFree R M₂
inst✝² : Finite ι₂
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst✝ : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf : ∀ (i : ι), f (P.root i) = Q.root (e i)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
x✝ : ι₂
⊢ Q.root x✝ = (RootPairing.map e f g).root x✝

Tactic:
·

Goal state after:
case he
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁴ : CommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : Module R N₂
P✝ : RootPairing ι R M N
Q✝ : RootPairing ι₂ R M₂ N₂
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Module.IsTorsionFree R M₂
inst✝² : Finite ι₂
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst✝ : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf : ∀ (i : ι), f (P.root i) = Q.root (e i)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
x✝¹ : M₂
x✝ : N₂
⊢ (Q.toLinearMap x✝¹) x✝ = ((RootPairing.map e f g).toLinearMap x✝¹) x✝
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case hr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁴ : CommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : Module R N₂
P✝ : RootPairing ι R M N
Q✝ : RootPairing ι₂ R M₂ N₂
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Module.IsTorsionFree R M₂
inst✝² : Finite ι₂
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst✝ : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf : ∀ (i : ι), f (P.root i) = Q.root (e i)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
x✝ : ι₂
⊢ Q.root x✝ = (RootPairing.map e f g).root x✝

Tactic:
·

Goal state after:
case hr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁴ : CommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : Module R N₂
P✝ : RootPairing ι R M N
Q✝ : RootPairing ι₂ R M₂ N₂
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Module.IsTorsionFree R M₂
inst✝² : Finite ι₂
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst✝ : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf : ∀ (i : ι), f (P.root i) = Q.root (e i)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
x✝ : ι₂
⊢ Q.root x✝ = (RootPairing.map e f g).root x✝
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : NeZero 2
inst✝ : P.IsIrreducible
s : Set ι
hne : s.Nonempty
h : ∀ (j : ι), P.root j ∉ span R (⇑P.root '' s) → ∀ i ∈ s, P.IsOrthogonal j i
j : ι
hj : P.root j ∈ span R (⇑P.root '' s)
⊢ span R (⇑P.root '' s) ∈ invtSubmodule ↑(P.reflection j)

pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : NeZero 2
inst✝ : P.IsIrreducible
s : Set ι
hne : s.Nonempty
h : ∀ (j : ι), P.root j ∉ span R (⇑P.root '' s) → ∀ i ∈ s, P.IsOrthogonal j i
j : ι
hj : P.root j ∉ span R (⇑P.root '' s)
⊢ span R (⇑P.root '' s) ∈ invtSubmodule ↑(P.reflection j)

Tactic:
·

Goal state after:
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : NeZero 2
inst✝ : P.IsIrreducible
s : Set ι
hne : s.Nonempty
h : ∀ (j : ι), P.root j ∉ span R (⇑P.root '' s) → ∀ i ∈ s, P.IsOrthogonal j i
j : ι
hj : P.root j ∈ span R (⇑P.root '' s)
⊢ span R (⇑P.root '' s) ∈ invtSubmodule ↑(P.reflection j)
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : NeZero 2
inst✝ : P.IsIrreducible
s : Set ι
hne : s.Nonempty
h : ∀ (j : ι), P.root j ∉ span R (⇑P.root '' s) → ∀ i ∈ s, P.IsOrthogonal j i
j : ι
hj : P.root j ∉ span R (⇑P.root '' s)
⊢ span R (⇑P.root '' s) ∈ invtSubmodule ↑(P.reflection j)

Tactic:
·

Goal state after:
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : NeZero 2
inst✝ : P.IsIrreducible
s : Set ι
hne : s.Nonempty
h : ∀ (j : ι), P.root j ∉ span R (⇑P.root '' s) → ∀ i ∈ s, P.IsOrthogonal j i
j : ι
hj : P.root j ∉ span R (⇑P.root '' s)
⊢ span R (⇑P.root '' s) ∈ invtSubmodule ↑(P.reflection j)
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case h.left
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ LeftInverse ⇑f.inv.weightMap ⇑(↑f).weightMap

pp: case h.right
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ RightInverse ⇑f.inv.weightMap ⇑(↑f).weightMap

Tactic:
·

Goal state after:
case h.left
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ LeftInverse ⇑f.inv.weightMap ⇑(↑f).weightMap
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case h.right
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ RightInverse ⇑f.inv.weightMap ⇑(↑f).weightMap

Tactic:
·

Goal state after:
case h.right
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ RightInverse ⇑f.inv.weightMap ⇑(↑f).weightMap
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
h₂ : ∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
b : ∀ i ∈ ∅, ¬Disjoint q (K ∙ P.root i)
c : ∀ i ∉ ∅, q ≤ ker (P.coroot' i)
⊢ q = ⊤

pp: case inr
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
h₂ : ∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
Φ : Set ι
b : ∀ i ∈ Φ, ¬Disjoint q (K ∙ P.root i)
c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)
hΦ : Φ.Nonempty
⊢ q = ⊤

Tactic:
·

Goal state after:
case inl
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
h₂ : ∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
b : ∀ i ∈ ∅, ¬Disjoint q (K ∙ P.root i)
c : ∀ i ∉ ∅, q ≤ ker (P.coroot' i)
⊢ q = ⊤
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case h.left
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ LeftInverse ⇑f.inv.coweightMap ⇑(↑f).coweightMap

pp: case h.right
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ RightInverse ⇑f.inv.coweightMap ⇑(↑f).coweightMap

Tactic:
·

Goal state after:
case h.left
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ LeftInverse ⇑f.inv.coweightMap ⇑(↑f).coweightMap
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case h.right
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ RightInverse ⇑f.inv.coweightMap ⇑(↑f).coweightMap

Tactic:
·

Goal state after:
case h.right
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ RightInverse ⇑f.inv.coweightMap ⇑(↑f).coweightMap
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
h₂ : ∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
Φ : Set ι
b : ∀ i ∈ Φ, ¬Disjoint q (K ∙ P.root i)
c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)
hΦ : Φ.Nonempty
⊢ q = ⊤

Tactic:
·

Goal state after:
case inr
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
h₂ : ∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
Φ : Set ι
b : ∀ i ∈ Φ, ¬Disjoint q (K ∙ P.root i)
c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)
hΦ : Φ.Nonempty
⊢ q = ⊤
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ (↑(reflection P i)⁻¹).weightMap = (↑(reflection P i)).weightMap

pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ (↑(reflection P i)⁻¹).coweightMap = (↑(reflection P i)).coweightMap

pp: case refine_3
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ (↑(reflection P i)⁻¹).indexEquiv = (↑(reflection P i)).indexEquiv

Tactic:
·

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ (↑(reflection P i)⁻¹).weightMap = (↑(reflection P i)).weightMap
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ (↑(reflection P i)⁻¹).coweightMap = (↑(reflection P i)).coweightMap

pp: case refine_3
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ (↑(reflection P i)⁻¹).indexEquiv = (↑(reflection P i)).indexEquiv

Tactic:
·

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ (↑(reflection P i)⁻¹).coweightMap = (↑(reflection P i)).coweightMap
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case refine_3
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ (↑(reflection P i)⁻¹).indexEquiv = (↑(reflection P i)).indexEquiv

Tactic:
·

Goal state after:
case refine_3
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ (↑(reflection P i)⁻¹).indexEquiv = (↑(reflection P i)).indexEquiv