mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
⊢ √((‖x‖ + x.re) / 2) = √((‖x‖ + x.re) / 2)

pp: case hx
x : ℂ
⊢ 0 ≤ ‖x‖

pp: case hl
x : ℂ
⊢ -π ≤ x.arg

pp: case hr
x : ℂ
⊢ x.arg ≤ π

Tactic:
]

Goal state after:
case hx
x : ℂ
⊢ 0 ≤ ‖x‖

case hl
x : ℂ
⊢ -π ≤ x.arg

case hr
x : ℂ
⊢ x.arg ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : x ≤ 1
h : ¬x = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
]

Goal state after:
case neg
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : x ≤ 1
h : ¬x = 0
⊢ ↑x ^ y ≤ ↑x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
⊢ √((‖x‖ - x.re) / 2) = √((‖x‖ - x.re) / 2)

pp: case hl
x : ℂ
hx : 0 ≤ x.im
⊢ 0 ≤ x.arg

pp: case hr
x : ℂ
hx : 0 ≤ x.im
⊢ x.arg ≤ 2 * π

Tactic:
]

Goal state after:
case hl
x : ℂ
hx : 0 ≤ x.im
⊢ 0 ≤ x.arg

case hr
x : ℂ
hx : 0 ≤ x.im
⊢ x.arg ≤ 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x ^ 1

Tactic:
]

Goal state after:
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x ^ 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case hl
x : ℂ
hx : 0 ≤ x.im
⊢ 0 ≤ x.im

Tactic:
]

Goal state after:
case hl
x : ℂ
hx : 0 ≤ x.im
⊢ 0 ≤ x.im
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
⊢ x ^ 1 ≤ x ^ z

Tactic:
]

Goal state after:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
⊢ x ^ 1 ≤ x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
⊢ 0 < x ^ p

Tactic:
]

Goal state after:
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
⊢ 0 < x ^ p
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 ^ p < x ^ p

Tactic:
]

Goal state after:
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 ^ p < x ^ p
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_nonpos : p ≤ 0
⊢ x ^ (-p) ≠ ∞

Tactic:
]

Goal state after:
case inr
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_nonpos : p ≤ 0
⊢ x ^ (-p) ≠ ∞
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
hx : x.im < 0
⊢ -√((‖x‖ - x.re) / 2) = -√((‖x‖ - x.re) / 2)

pp: case hl
x : ℂ
hx : x.im < 0
⊢ -(2 * π) ≤ x.arg

pp: case hr
x : ℂ
hx : x.im < 0
⊢ x.arg ≤ 0

Tactic:
]

Goal state after:
case hl
x : ℂ
hx : x.im < 0
⊢ -(2 * π) ≤ x.arg

case hr
x : ℂ
hx : x.im < 0
⊢ x.arg ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
⊢ ↑(x.toNNReal ^ z) = ↑(x.toNNReal ^ z)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x p : ℝ
hx_pos : 0 < x
⊢ x.toNNReal ^ p = x.toNNReal ^ p

pp: case h
x p : ℝ
hx_pos : 0 < x
⊢ x.toNNReal ≠ 0

Tactic:
]

Goal state after:
case h
x p : ℝ
hx_pos : 0 < x
⊢ x.toNNReal ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
]

Goal state after:
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
⊢ √((‖x‖ - x.re) / 2) = √((‖x‖ - x.re) / 2)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x ≠ 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
]

Goal state after:
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x ≠ 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
hy : y ≠ 0
x : ℝ≥0∞
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < ↑(↑n ^ x)

Tactic:
]

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < ↑(↑n ^ x)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: b : ℝ
n : ℕ
h : IsNat b n
a : ℝ
⊢ a ^ n = a ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
n : ℕ
z : ℝ
⊢ (x ^ n) ^ z = (x ^ n) ^ z

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
n : ℕ
⊢ (x ^ y) ^ n = (x ^ y) ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
n : ℤ
z : ℝ
⊢ (x ^ n) ^ z = (x ^ n) ^ z

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
n : ℤ
⊢ (x ^ y) ^ n = (x ^ y) ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ
⊢ (a ^ n)⁻¹ = (a ^ n)⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ (a + b) ^ p ≤ (max a b + max a b) ^ p

Tactic:
]

Goal state after:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ (a + b) ^ p ≤ (max a b + max a b) ^ p
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ 2 ^ p * max (a ^ p) (b ^ p) = 2 ^ p * max (a ^ p) (b ^ p)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ ↑(m ^ n) ^ (↑d)⁻¹ = ↑r

pp: case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑m

Tactic:
hm,

Goal state after:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ ↑l ^ (↑d)⁻¹ = ↑r

case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑m
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: b : ℝ
n : ℕ
h : IsNat b n
a : ℝ≥0
⊢ a ^ n = a ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
⊢ (a ^ n)⁻¹ = (a ^ n)⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ ↑r = ↑r

pp: case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑r

pp: case hn
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ d ≠ 0

pp: case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑m

Tactic:
]

Goal state after:
case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑r

case hn
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ d ≠ 0

case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑m
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ ↑(m ^ n) ^ (↑d)⁻¹ = ↑r

Tactic:
hm,

Goal state after:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ ↑l ^ (↑d)⁻¹ = ↑r
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: a b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (↑na ^ b) nr
hden : IsNat (↑da ^ b) dr
⊢ ↑da ^ b ≠ 0

Tactic:
]

Goal state after:
a b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (↑na ^ b) nr
hden : IsNat (↑da ^ b) dr
⊢ ↑da ^ b ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ ↑r = ↑r

pp: case hn
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ d ≠ 0

Tactic:
]

Goal state after:
case hn
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ d ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: a b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
⊢ a ^ (-(↑n / ↑d)) = a ^ (-(↑n / ↑d))

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: a : ℝ≥0
b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
⊢ a ^ (-(↑n / ↑d)) = a ^ (-(↑n / ↑d))

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ y = y

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ (lineMap y x) ⅟2 = (lineMap y x) ⅟2

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R 0 y

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R 0 y
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ : P
⊢ ⅟2 • (p₁ -ᵥ p₂) = ⅟2 • (p₁ -ᵥ p₂)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ : P
⊢ ⅟2 • (p₂ -ᵥ p₁) = ⅟2 • (p₂ -ᵥ p₁)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
⊢ r₂ • r₃ • y = r₂ • r₃ • y

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inl
R : Type u_1
inst✝¹⁰ : CommSemiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_5
inst✝⁵ : CommSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : (algebraMap S R) a = 0
⊢ SameRay R v 0

Tactic:
]

Goal state after:
case inl
R : Type u_1
inst✝¹⁰ : CommSemiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_5
inst✝⁵ : CommSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : (algebraMap S R) a = 0
⊢ SameRay R v 0
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ (⅟2 • (p₁ -ᵥ p₂) +ᵥ p₂) -ᵥ p = (⅟2 • (p₁ -ᵥ p₂) +ᵥ p₂) -ᵥ p

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ p₂) = ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ p₂)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x y : M
S : Type u_5
inst✝⁵ : CommSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
h : SameRay R x y
ha : 0 ≤ a
hy : y = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ x = y ↔ x = y

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
x y : M
f : M →ₗ[R] N
h : SameRay R x y
hx : x = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
x y : M
f : M →ₗ[R] N
h : SameRay R x y
hy : y = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
x y : M
f : M →ₗ[R] N
h✝ : SameRay R x y
x✝ : ∃ r₁ r₂, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ f (r₂ • y) = f (r₂ • y)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y z : M
hy : SameRay R y z
hx : SameRay R 0 z
⊢ SameRay R y z

Tactic:
]

Goal state after:
case inl
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y z : M
hy : SameRay R y z
hx : SameRay R 0 z
⊢ SameRay R y z
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x z : M
hx : SameRay R x z
hx₀ : x ≠ 0
hy : SameRay R 0 z
⊢ SameRay R x z

Tactic:
]

Goal state after:
case inr.inl
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x z : M
hx : SameRay R x z
hx₀ : x ≠ 0
hy : SameRay R 0 z
⊢ SameRay R x z
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x x' y y' : P
⊢ x -ᵥ x' = y' -ᵥ y ↔ x -ᵥ x' = y' -ᵥ y

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R y x +ᵥ midpoint R y x = midpoint R y x +ᵥ midpoint R y x

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ y + x = y + x

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ y = y

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x : V
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R x x +ᵥ midpoint R (-y) y = x

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R x x +ᵥ midpoint R (-y) y = x
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R (x - y) (x + y) = x

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R (x - y) (x + y) = x
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p₃ : P
⊢ ⅟2 • (p₂ -ᵥ p₃) = ⅟2 • (p₂ -ᵥ p₃)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ SameRay R (u • v✝) v✝

Tactic:
]

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ SameRay R (u • v✝) v✝
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ SameRay R x (-y) ↔ SameRay R x (-y)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p₃ : P
⊢ ⅟2 • (p₁ -ᵥ p₂) = ⅟2 • (p₁ -ᵥ p₂)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Invertible 2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
inst✝³ : Ring R'
inst✝² : Invertible 2
inst✝¹ : AddCommGroup F
inst✝ : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
⊢ f (x + y) = f (x + y)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Invertible 2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
inst✝³ : Ring R'
inst✝² : Invertible 2
inst✝¹ : AddCommGroup F
inst✝ : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
⊢ f (midpoint R x y) + f (midpoint R x y) = f (midpoint R x y) + f (midpoint R x y)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ x = 0

Tactic:
]

Goal state after:
case inr.inr
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ x = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Invertible 2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
inst✝³ : Ring R'
inst✝² : Invertible 2
inst✝¹ : AddCommGroup F
inst✝ : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
⊢ f (midpoint R x y) + f (midpoint R x y) = f x + f y

Tactic:
hm,

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Invertible 2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
inst✝³ : Ring R'
inst✝² : Invertible 2
inst✝¹ : AddCommGroup F
inst✝ : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
⊢ midpoint R' (f x) (f y) + midpoint R' (f x) (f y) = f x + f y
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Invertible 2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
inst✝³ : Ring R'
inst✝² : Invertible 2
inst✝¹ : AddCommGroup F
inst✝ : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
⊢ f x + f y = f x + f y

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : SameRay R x (-x)
⊢ SameRay R x (-x)

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : SameRay R x (-x)
⊢ SameRay R x (-x)
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R✝ : Type u_1
inst✝⁶ : CommRing R✝
inst✝⁵ : PartialOrder R✝
inst✝⁴ : IsStrictOrderedRing R✝
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ M
inst✝ : Module R✝ N
x y : M
R : Type u_4
v : RayVector R M
⊢ ↑((equiv R M) v) = ↑((equiv R M) v)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
⊢ ¬SameRay R x (-x)

Tactic:
]

Goal state after:
case h
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
⊢ ¬SameRay R x (-x)