Theorem: Lean4Axiomatic.Rational.average (Lean4Axiomatic/Rational/Order.lean)

State before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p < q → p < (p + q) / 2 ∧ (p + q) / 2 < q
Tactic:
intro (_ : p < q)
State after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q

State before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q
Tactic:
have : p < (p + q)/2 := calc
  _ ≃ p         := eqv_refl
  _ ≃ (2 * p)/2 := eqv_symm mulL_div_same
  _ ≃ (p + p)/2 := div_substL mul_two_add
  _ < (p + q)/2 := lt_substN_div_pos (lt_substR_add ‹p < q›)
State after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q
this : p < (p + q) / 2
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q

State before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q
this : p < (p + q) / 2
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q
Tactic:
have : (p + q)/2 < q := calc
  _ ≃ (p + q)/2 := eqv_refl
  _ < (q + q)/2 := lt_substN_div_pos (lt_substL_add ‹p < q›)
  _ ≃ (2 * q)/2 := div_substL (eqv_symm mul_two_add)
  _ ≃ q         := mulL_div_same
State after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q
this✝ : p < (p + q) / 2
this : (p + q) / 2 < q
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q

State before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q
this✝ : p < (p + q) / 2
this : (p + q) / 2 < q
⊢ p < (p + q) / 2 ∧ (p + q) / 2 < q
Tactic:
exact And.intro ‹p < (p + q)/2› ‹(p + q)/2 < q›
State after:
no goals