mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : (Q₁.prod Q₂).Anisotropic
⊢ Q₁.Anisotropic ∧ Q₂.Anisotropic

Tactic:
[

Goal state after:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : (Q₁.prod Q₂).Anisotropic
⊢ Q₁.Anisotropic ∧ Q₂.Anisotropic
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : Preorder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ (∀ (x : M₁ × M₂), 0 ≤ (Q₁.prod Q₂) x) ↔ (∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x

Tactic:
[

Goal state after:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : Preorder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ (∀ (x : M₁ × M₂), 0 ≤ (Q₁.prod Q₂) x) ↔ (∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ (Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef

Tactic:
[

Goal state after:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ (Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : (pi Q).Anisotropic
⊢ ∀ (i : ι), (Q i).Anisotropic

Tactic:
[

Goal state after:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : (pi Q).Anisotropic
⊢ ∀ (i : ι), (Q i).Anisotropic
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (∀ (x : (i : ι) → Mᵢ i), 0 ≤ (pi Q) x) ↔ ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x

Tactic:
[

Goal state after:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (∀ (x : (i : ι) → Mᵢ i), 0 ≤ (pi Q) x) ↔ ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (pi Q).PosDef ↔ ∀ (i : ι), (Q i).PosDef

Tactic:
[

Goal state after:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (pi Q).PosDef ↔ ∀ (i : ι), (Q i).PosDef
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
s : Finset ι
c : ι → R
hc : ∑ i ∈ s, c i • v i = 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
⊢ x = y

Tactic:
[

Goal state after:
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
s : Finset ι
c : ι → R
hc : ∑ i ∈ s, c i • v i = 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
⊢ x = y
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case mpr
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ (Q i) x) ∧ (Q i).Anisotropic) →
    (∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x) ∧ (pi Q).Anisotropic

Tactic:
· intro h
    refine ⟨fun i => (h i).1, fun x hx => funext fun i => (h i).2 _ ?_⟩
    rw [pi_apply, Finset.sum_eq_zero_iff_of_nonneg fun j _ => ?_] at hx
    · exact hx _ (Finset.mem_univ _)
    exact (h j).1 _

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝³ : AddCommGroup P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
x y : (i : ι) → Mᵢ i
⊢ (pi Q) (x + y) - (pi Q) x - (pi Q) y = ∑ i, ((Q i) (x i + y i) - (Q i) (x i) - (Q i) (y i))

Tactic:
[

Goal state after:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝³ : AddCommGroup P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
x y : (i : ι) → Mᵢ i
⊢ (pi Q) (x + y) - (pi Q) x - (pi Q) y = ∑ i, ((Q i) (x i + y i) - (Q i) (x i) - (Q i) (y i))
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
⊢ chainLength α β' = chainLength α β

Tactic:
by_cases hα : α.IsZero

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
hα : α.IsZero
⊢ chainLength α β' = chainLength α β

case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
hα : ¬α.IsZero
⊢ chainLength α β' = chainLength α β
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

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
⊢ range P.reflection ⊆ ↑((Equiv.weightHom P).domRestrict P.weylGroup).range

Tactic:
rintro - ⟨i, rfl⟩
    simp only [MonoidHom.domRestrict_range, Subgroup.coe_map, Equiv.weightHom_apply, mem_image,
      SetLike.mem_coe]
    use Equiv.reflection P i
    exact ⟨reflection_mem_weylGroup P i, Equiv.reflection_weightEquiv P i⟩

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
k : K
h : ⇑β = k • ⇑α
⊢ β = -α ∨ β = α

Tactic:
by_cases hα : α.IsZero

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
k : K
h : ⇑β = k • ⇑α
hα : α.IsZero
⊢ β = -α ∨ β = α

case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
k : K
h : ⇑β = k • ⇑α
hα : ¬α.IsZero
⊢ β = -α ∨ β = α
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ β✝ α β : Weight K (↥H) L
⊢ genWeightSpace L (⇑β - β (coroot α) • ⇑α) ≠ ⊥

Tactic:
by_cases hα : α.IsZero

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ β✝ α β : Weight K (↥H) L
hα : α.IsZero
⊢ genWeightSpace L (⇑β - β (coroot α) • ⇑α) ≠ ⊥

case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ β✝ α β : Weight K (↥H) L
hα : ¬α.IsZero
⊢ genWeightSpace L (⇑β - β (coroot α) • ⇑α) ≠ ⊥
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case coweightMap
ι : 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
f g : P.End
hfg : (weightHom P) f = (weightHom P) g
x : N
⊢ P.flip.toPerfPair (f.coweightMap x) = P.flip.toPerfPair (g.coweightMap x)

Tactic:
[

Goal state after:
case coweightMap
ι : 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
f g : P.End
hfg : (weightHom P) f = (weightHom P) g
x : N
⊢ P.flip.toPerfPair (f.coweightMap x) = P.flip.toPerfPair (g.coweightMap x)
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case indexEquiv
ι : 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
f g : P.End
hfg : (weightHom P) f = (weightHom P) g
x : ι
⊢ P.root (f.indexEquiv x) = P.root (g.indexEquiv x)

Tactic:
[

Goal state after:
case indexEquiv
ι : 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
f g : P.End
hfg : (weightHom P) f = (weightHom P) g
x : ι
⊢ P.root (f.indexEquiv x) = P.root (g.indexEquiv x)
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
e : (reflectRoot α β).IsZero
⊢ β (coroot α) = 0

Tactic:
by_cases hα : α.IsZero

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
e : (reflectRoot α β).IsZero
hα : α.IsZero
⊢ β (coroot α) = 0

case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
e : (reflectRoot α β).IsZero
hα : ¬α.IsZero
⊢ β (coroot α) = 0
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: ι : 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 : ↥P.invtRootSubmodule
h : ∀ (i : ι), P.root i ∉ ↑q
⊢ q = ⊥

Tactic:
[

Goal state after:
ι : 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 : ↥P.invtRootSubmodule
h : ∀ (i : ι), P.root i ∉ ↑q
⊢ q = ⊥
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
f₁ f₂ : V →ₗ[k] W
⊢ ρW g ∘ₗ (f₁ + f₂) ∘ₗ ρV g⁻¹ = ρW g ∘ₗ f₁ ∘ₗ ρV g⁻¹ + ρW g ∘ₗ f₂ ∘ₗ ρV g⁻¹

Tactic:
[

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
f₁ f₂ : V →ₗ[k] W
⊢ ρW g ∘ₗ (f₁ + f₂) ∘ₗ ρV g⁻¹ = ρW g ∘ₗ f₁ ∘ₗ ρV g⁻¹ + ρW g ∘ₗ f₂ ∘ₗ ρV g⁻¹
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
r : k
f : V →ₗ[k] W
⊢ ρW g ∘ₗ (r • f) ∘ₗ ρV g⁻¹ = (RingHom.id k) r • ρW g ∘ₗ f ∘ₗ ρV g⁻¹

Tactic:
[

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
r : k
f : V →ₗ[k] W
⊢ ρW g ∘ₗ (r • f) ∘ₗ ρV g⁻¹ = (RingHom.id k) r • ρW g ∘ₗ f ∘ₗ ρV g⁻¹
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: ι : 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)
this : Q = RootPairing.map e f g
i : ι₂
| Q.coroot i

Tactic:
this

Goal state after:
ι : 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)
this : Q = RootPairing.map e f g
i : ι₂
| (RootPairing.map e f g).coroot i
Module: Mathlib.Order.Interval.Set.OrdConnectedLinear

Goal state before:
pp: α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
⊢ I.OrdConnected ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Ioo x y) I → Ioo x y = ∅

Tactic:
[

Goal state after:
α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
⊢ I.OrdConnected ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Ioo x y) I → Ioo x y = ∅
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: ι : 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
B : P.InvariantForm
i j : ι
contra : ∀ (k : ι), (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j) → (B.form (P.root i)) (P.root k) = 0
⊢ span R (orbit (↥P.weylGroup) (P.root j)) ≤ (B.form (P.root i)).ker

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

Goal state after:
ι : 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
B : P.InvariantForm
i j : ι
contra : ∀ (k : ι), (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j) → (B.form (P.root i)) (P.root k) = 0
v : M
hv : v ∈ orbit (↥P.weylGroup) (P.root j)
⊢ v ∈ ↑(B.form (P.root i)).ker
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : 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
b : P.Base
inst✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : P.root j = t • P.root i
this : ∃ c, ∑ i, c i • P.coroot ↑i = P.coroot j
f : ↥b.support → ℤ
hf : ∑ i, f i • P.coroot ↑i = P.coroot j
⊢ P.coroot i = ∑ i, (t * ↑(f i)) • P.coroot ↑i

Tactic:
[

Goal state after:
ι : 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
b : P.Base
inst✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : P.root j = t • P.root i
this : ∃ c, ∑ i, c i • P.coroot ↑i = P.coroot j
f : ↥b.support → ℤ
hf : ∑ i, f i • P.coroot ↑i = P.coroot j
⊢ P.coroot i = ∑ i, (t * ↑(f i)) • P.coroot ↑i
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : 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
b : P.Base
inst✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : P.root j = t • P.root i
f : ↥b.support → ℤ
hf : P.coroot i = ∑ i, (t * ↑(f i)) • P.coroot ↑i
⊢ ∑ i, (t * ↑(f i)) • P.coroot ↑i = t • ∑ i, ↑(f i) • P.coroot ↑i

Tactic:
[

Goal state after:
ι : 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
b : P.Base
inst✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : P.root j = t • P.root i
f : ↥b.support → ℤ
hf : P.coroot i = ∑ i, (t * ↑(f i)) • P.coroot ↑i
⊢ ∑ i, (t * ↑(f i)) • P.coroot ↑i = t • ∑ i, ↑(f i) • P.coroot ↑i
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : 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
b : P.Base
inst✝ : CharZero R
f✝ : ι → ℤ
hf✝ : ∑ j ∈ b.support, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ ↑b.support
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
hf₀ : Function.support f ⊆ ↑b.support
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun i ↦ f ↑i
this : ∑ j, f' j • P.root ↑j = ∑ j ∈ b.support, f j • P.root j
⊢ ∑ j, f' j • P.root ↑j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)

Tactic:
this

Goal state after:
ι : 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
b : P.Base
inst✝ : CharZero R
f✝ : ι → ℤ
hf✝ : ∑ j ∈ b.support, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ ↑b.support
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
hf₀ : Function.support f ⊆ ↑b.support
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun i ↦ f ↑i
this : ∑ j, f' j • P.root ↑j = ∑ j ∈ b.support, f j • P.root j
⊢ ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : 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
b : P.Base
inst✝ : CharZero R
f✝ : ι → ℤ
hf✝ : ∑ j ∈ b.support, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ ↑b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun i ↦ f ↑i
hf : ∑ j, f' j • P.root ↑j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
⊢ 0 < f

Tactic:
← span_nat_eq_addSubmonoidClosure,

Goal state after:
ι : 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
b : P.Base
inst✝ : CharZero R
f✝ : ι → ℤ
hf✝ : ∑ j ∈ b.support, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ ↑b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun i ↦ f ↑i
hf : ∑ j, f' j • P.root ↑j ∈ (span ℕ (⇑P.root '' ↑b.support)).toAddSubmonoid
⊢ 0 < f