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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i✝ : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
hf₀ : ∀ (i : ι), f (P.root i) ≠ 0
i : ι
⊢ ∃ q, 0 < q ∧ ↑q = 2 / (P.RootForm (P.root i)) (P.root i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: a b : Cauchy abs
⊢ { cauchy := a } = { cauchy := b } ↔ { cauchy := a }.cauchy = { cauchy := b }.cauchy

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: a b : Cauchy abs
⊢ { cauchy := a - b } = { cauchy := a } - { cauchy := b }

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: a b : Cauchy abs
⊢ ({ cauchy := a } - { cauchy := b }).cauchy = { cauchy := a }.cauchy - { cauchy := b }.cauchy

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ a + b + c = a + (b + c)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ 0 + a = a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i✝ : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
hf₀ : ∀ (i : ι), f (P.root i) ≠ 0
aux : ∀ (i : ι), ∃ q, 0 < q ∧ ↑q = 2 / (P.RootForm (P.root i)) (P.root i)
g : Dual ℚ N := f ∘ₗ ↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm)
i : ι
⊢ g (P.coroot i) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ a + 0 = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ a + b = b + a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ a * b * c = a * (b * c)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ 1 * a = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ a * 1 = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ 0 * a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ a * 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ a * (b + c) = a * b + a * c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ (a + b) * c = a * c + b * c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ { cauchy := ↑0 } = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
n : ℕ
⊢ { cauchy := ↑(n + 1) } = { cauchy := ↑n } + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ -a + a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
z : ℕ
⊢ { cauchy := ↑(Int.negSucc z) } = -↑(z + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ a * b = b * a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ Ring ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ CommSemiring ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ Semiring ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ CommMonoidWithZero ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ MonoidWithZero ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ AddCommGroup ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ AddGroup ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ AddCommMonoid ℝ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i✝ : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
hf₀ : ∀ (i : ι), f (P.root i) ≠ 0
aux : ∀ (i : ι), ∃ q, 0 < q ∧ ↑q = 2 / (P.RootForm (P.root i)) (P.root i)
g : Dual ℚ N := f ∘ₗ ↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm)
hg₀ : ∀ (i : ι), g (P.coroot i) ≠ 0
i : ι
⊢ 0 < g (P.coroot i) ↔ 0 < f (P.root i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ AddMonoid ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
⊢ f.Pos ∨ f.LimZero ∨ (-f).Pos

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ AddLeftCancelSemigroup ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ AddRightCancelSemigroup ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ AddCommSemigroup ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ AddSemigroup ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ CommMonoid ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ Monoid ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ CommSemigroup ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ Semigroup ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
⊢ f < h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
x✝ : f < f
h : f < f := x✝
⊢ (f - f).LimZero

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g : CauSeq α abs
h✝ : (g - f).LimZero ∨ (-(g - f)).Pos
h : (-(g - f)).Pos
⊢ g < f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: ⊢ mk 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: ⊢ mk 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f g : CauSeq ℚ abs
⊢ mk (f + g) = mk f + mk g

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f g : CauSeq ℚ abs
⊢ mk (f * g) = mk f * mk g

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f : CauSeq ℚ abs
⊢ mk (-f) = -mk f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
⊢ const x ≤ const y ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f : CauSeq ℚ abs
⊢ 0 < mk f ↔ f.Pos

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f g : CauSeq ℚ abs
⊢ mk f ≤ mk g ↔ f ≤ g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |↑f i| < K
i : ℕ
x✝ : i ≥ 0
⊢ 1 ≤ ↑(const (K + 1) - f) i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: C : ℝ → Prop
x : ℝ
h : ∀ (y : CauSeq ℚ abs), C (mk y)
⊢ C x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ a ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
⊢ mk (if h : f.LimZero then 0 else f.inv h) = mk (if h : g.LimZero then 0 else g.inv h)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
hf₀ : ∀ (i : ι), f (P.root i) ≠ 0
aux : ∀ (i : ι), ∃ q, 0 < q ∧ ↑q = 2 / (P.RootForm (P.root i)) (P.root i)
g : Dual ℚ N := f ∘ₗ ↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm)
hg₀ : ∀ (i : ι), g (P.coroot i) ≠ 0
hg : ∀ (i : ι), 0 < g (P.coroot i) ↔ 0 < f (P.root i)
⊢ P.coroot (-i) = -P.coroot i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ a ≤ b → b ≤ a → a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ Preorder ℝ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i : ι
⊢ P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' s) ∨ -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' s)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
⊢ LinearIndepOn R ⇑P.root ↑⋯.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x y : ℚ
⊢ ↑x < ↑y ↔ x < y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: ⊢ 0 < 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
⊢ LinearIndepOn R ⇑P.coroot ↑⋯.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ x✝
⊢ |↑(f ⊔ g) j| < ε

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ (if h : (const abv 0).LimZero then 0 else (const abv 0).inv h) = const abv 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i : ι
⊢ P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑⋯.toFinset) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑⋯.toFinset)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i : ι
⊢ P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑⋯.toFinset) ∨
    -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑⋯.toFinset)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
_i : Module ℚ M := compHom M (algebraMap ℚ R)
⊢ ∀ (i : ι), P.root i ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ (if h : f.LimZero then 0 else f.inv h) = f.inv hf

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
_i : Module ℚ M := compHom M (algebraMap ℚ R)
f : Dual ℚ M
hf : ∀ (i : ι), f (P.root i) ≠ 0
this : InvolutiveNeg ι := P.indexNeg
i : ι
⊢ P.root (-i) = -P.root i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
⊢ Nonempty P.Base

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
h : 0 ≈ 1
this : (1 - 0).LimZero
⊢ LimZero 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ x✝
⊢ |↑(f ⊓ g) j| < ε

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ⟦f⟧ ≠ 0
⊢ (⟦f⟧)⁻¹ * ⟦f⟧ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (a b : ℝ), a ≤ b → ∀ (c : ℝ), a + c ≤ b + c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ 0 < a → 0 < b → 0 < a * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ⟦f⟧ ≠ 0
⊢ ⟦f⟧ * (⟦f⟧)⁻¹ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Pi

Goal state before:
pp: I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst✝ : Star α
⊢ star (Sum.elim x y) = Sum.elim (star x) (star y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
⊢ const abv x⁻¹ = if h : (const abv x).LimZero then 0 else (const abv x).inv h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x y : β
⊢ ofRat (x / y) = ofRat x / ofRat y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
⊢ a₁ ⊔ b₁ ≈ a₂ ⊔ b₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
⊢ const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
⊢ a₁ ⊓ b₁ ≈ a₂ ⊓ b₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (a b : ℝ), a ≤ a ⊔ b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
x : β
⊢ f.lim * x = (f * const abv x).lim

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a < c
hb : b < c
⊢ a ⊔ b < c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (a b : ℝ), b ≤ a ⊔ b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
⊢ f.lim - g.lim = (f - g).lim

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
⊢ f.LimZero

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
⊢ f.LimZero

Tactic:
by
    have hf := equiv_lim f
    rw [h] at hf
    exact (limZero_congr hf).mpr (const_limZero.mpr rfl)

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.LimZero
n : ℕ
⊢ ↑f n = ↑(f - const abv 0) n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : a < b
hc : a < c
⊢ a < b ⊓ c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (a b c : ℝ), a ≤ c → b ≤ c → a ⊔ b ≤ c

Tactic:
by

Goal state after: