[GOAL]
x y : ℝ
a b : Cauchy abs
⊢ { cauchy := a } = { cauchy := b } ↔ { cauchy := a }.cauchy = { cauchy := b }.cauchy
[PROOFSTEP]
rw [ofCauchy.injEq]
[GOAL]
x y : ℝ
a b : Cauchy abs
⊢ { cauchy := a - b } = { cauchy := a } - { cauchy := b }
[PROOFSTEP]
rw [sub_eq_add_neg, ofCauchy_add, ofCauchy_neg]
[GOAL]
x y : ℝ
a b : Cauchy abs
⊢ { cauchy := a } + -{ cauchy := b } = { cauchy := a } - { cauchy := b }
[PROOFSTEP]
rfl
[GOAL]
x y : ℝ
f : Cauchy abs
⊢ { cauchy := f⁻¹ } = Real.inv' { cauchy := f }
[PROOFSTEP]
rw [inv']
[GOAL]
x y : ℝ
⊢ Real.zero.cauchy = 0
[PROOFSTEP]
rw [zero_def]
[GOAL]
x y : ℝ
⊢ Real.one.cauchy = 1
[PROOFSTEP]
rw [one_def]
[GOAL]
x y : ℝ
a b : Cauchy abs
⊢ (Real.add { cauchy := a } { cauchy := b }).cauchy = { cauchy := a }.cauchy + { cauchy := b }.cauchy
[PROOFSTEP]
rw [add_def]
[GOAL]
x y : ℝ
a : Cauchy abs
⊢ (Real.neg { cauchy := a }).cauchy = -{ cauchy := a }.cauchy
[PROOFSTEP]
rw [neg_def]
[GOAL]
x y : ℝ
a b : Cauchy abs
⊢ (Real.mul { cauchy := a } { cauchy := b }).cauchy = { cauchy := a }.cauchy * { cauchy := b }.cauchy
[PROOFSTEP]
rw [mul_def]
[GOAL]
x y : ℝ
a b : Cauchy abs
⊢ ({ cauchy := a } - { cauchy := b }).cauchy = { cauchy := a }.cauchy - { cauchy := b }.cauchy
[PROOFSTEP]
rw [sub_eq_add_neg, ← cauchy_neg, ← cauchy_add]
[GOAL]
x y : ℝ
a b : Cauchy abs
⊢ ({ cauchy := a } - { cauchy := b }).cauchy = ({ cauchy := a } + -{ cauchy := b }).cauchy
[PROOFSTEP]
rfl
[GOAL]
x y : ℝ
f : Cauchy abs
⊢ (Real.inv' { cauchy := f }).cauchy = { cauchy := f }.cauchy⁻¹
[PROOFSTEP]
rw [inv']
[GOAL]
x y : ℝ
⊢ CommRing ℝ
[PROOFSTEP]
refine'
  { natCast := fun n => ⟨n⟩
    intCast := fun z => ⟨z⟩
    zero := (0 : ℝ)
    one := (1 : ℝ)
    mul := (· * ·)
    add := (· + ·)
    neg := @Neg.neg ℝ _
    sub := @Sub.sub ℝ _
    npow := @npowRec ℝ ⟨1⟩ ⟨(· * ·)⟩
    nsmul := @nsmulRec ℝ ⟨0⟩ ⟨(· + ·)⟩
    zsmul := @zsmulRec ℝ ⟨0⟩ ⟨(· + ·)⟩ ⟨@Neg.neg ℝ _⟩, .. }
[GOAL]
case refine'_1
x y : ℝ
⊢ ∀ (a b c : ℝ), a + b + c = a + (b + c)
case refine'_2
x y : ℝ
⊢ ∀ (a : ℝ), 0 + a = a
case refine'_3
x y : ℝ
⊢ ∀ (a : ℝ), a + 0 = a
case refine'_4
x y : ℝ
⊢ ∀ (x : ℝ), nsmulRec 0 x = 0
case refine'_5
x y : ℝ
⊢ ∀ (n : ℕ) (x : ℝ), nsmulRec (n + 1) x = x + nsmulRec n x
case refine'_6
x y : ℝ
⊢ ∀ (a b : ℝ), a + b = b + a
case refine'_7
x y : ℝ
⊢ ∀ (a b c : ℝ), a * (b + c) = a * b + a * c
case refine'_8
x y : ℝ
⊢ ∀ (a b c : ℝ), (a + b) * c = a * c + b * c
case refine'_9
x y : ℝ
⊢ ∀ (a : ℝ), 0 * a = 0
case refine'_10
x y : ℝ
⊢ ∀ (a : ℝ), a * 0 = 0
case refine'_11
x y : ℝ
⊢ ∀ (a b c : ℝ), a * b * c = a * (b * c)
case refine'_12
x y : ℝ
⊢ ∀ (a : ℝ), 1 * a = a
case refine'_13
x y : ℝ
⊢ ∀ (a : ℝ), a * 1 = a
case refine'_14
x y : ℝ
⊢ NatCast.natCast 0 = 0
case refine'_15
x y : ℝ
⊢ ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
case refine'_16
x y : ℝ
⊢ ∀ (x : ℝ), npowRec 0 x = 1
case refine'_17
x y : ℝ
⊢ ∀ (n : ℕ) (x : ℝ), npowRec (n + 1) x = x * npowRec n x
case refine'_18
x y : ℝ
⊢ ∀ (a b : ℝ), a - b = a + -b
case refine'_19
x y : ℝ
⊢ ∀ (a : ℝ), zsmulRec 0 a = 0
case refine'_20
x y : ℝ
⊢ ∀ (n : ℕ) (a : ℝ), zsmulRec (Int.ofNat (Nat.succ n)) a = a + zsmulRec (Int.ofNat n) a
case refine'_21
x y : ℝ
⊢ ∀ (n : ℕ) (a : ℝ), zsmulRec (Int.negSucc n) a = -zsmulRec (↑(Nat.succ n)) a
case refine'_22
x y : ℝ
⊢ ∀ (a : ℝ), -a + a = 0
case refine'_23
x y : ℝ
⊢ ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
case refine'_24
x y : ℝ
⊢ ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
case refine'_25 x y : ℝ ⊢ ∀ (a b : ℝ), a * b = b * a
[PROOFSTEP]
all_goals
  intros
  first
  | rfl
  | apply ext_cauchy
    simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
    first
    | done
    | apply add_assoc
    | apply add_comm
    | apply left_distrib
    | apply right_distrib
    | apply mul_assoc
    | apply mul_comm
[GOAL]
case refine'_1
x y : ℝ
⊢ ∀ (a b c : ℝ), a + b + c = a + (b + c)
[PROOFSTEP]
intros
[GOAL]
case refine'_1
x y a✝ b✝ c✝ : ℝ
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_1
x y a✝ b✝ c✝ : ℝ
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
rfl
[GOAL]
case refine'_1
x y a✝ b✝ c✝ : ℝ
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_1.a
x y a✝ b✝ c✝ : ℝ
⊢ (a✝ + b✝ + c✝).cauchy = (a✝ + (b✝ + c✝)).cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]
case refine'_1.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy + b✝.cauchy + c✝.cauchy = a✝.cauchy + (b✝.cauchy + c✝.cauchy)
[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]
case refine'_1.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy + b✝.cauchy + c✝.cauchy = a✝.cauchy + (b✝.cauchy + c✝.cauchy)
[PROOFSTEP]
done
[GOAL]
case refine'_1.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy + b✝.cauchy + c✝.cauchy = a✝.cauchy + (b✝.cauchy + c✝.cauchy)
[PROOFSTEP]
apply add_assoc
[GOAL]
case refine'_2
x y : ℝ
⊢ ∀ (a : ℝ), 0 + a = a
[PROOFSTEP]
intros
[GOAL]
case refine'_2
x y a✝ : ℝ
⊢ 0 + a✝ = a✝
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_2
x y a✝ : ℝ
⊢ 0 + a✝ = a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
x y a✝ : ℝ
⊢ 0 + a✝ = a✝
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_2.a
x y a✝ : ℝ
⊢ (0 + a✝).cauchy = a✝.cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]

[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]

[PROOFSTEP]
done
[GOAL]
case refine'_3
x y : ℝ
⊢ ∀ (a : ℝ), a + 0 = a
[PROOFSTEP]
intros
[GOAL]
case refine'_3
x y a✝ : ℝ
⊢ a✝ + 0 = a✝
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_3
x y a✝ : ℝ
⊢ a✝ + 0 = a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
x y a✝ : ℝ
⊢ a✝ + 0 = a✝
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_3.a
x y a✝ : ℝ
⊢ (a✝ + 0).cauchy = a✝.cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]

[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]

[PROOFSTEP]
done
[GOAL]
case refine'_4
x y : ℝ
⊢ ∀ (x : ℝ), nsmulRec 0 x = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_4
x y x✝ : ℝ
⊢ nsmulRec 0 x✝ = 0
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_4
x y x✝ : ℝ
⊢ nsmulRec 0 x✝ = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_5
x y : ℝ
⊢ ∀ (n : ℕ) (x : ℝ), nsmulRec (n + 1) x = x + nsmulRec n x
[PROOFSTEP]
intros
[GOAL]
case refine'_5
x y : ℝ
n✝ : ℕ
x✝ : ℝ
⊢ nsmulRec (n✝ + 1) x✝ = x✝ + nsmulRec n✝ x✝
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_5
x y : ℝ
n✝ : ℕ
x✝ : ℝ
⊢ nsmulRec (n✝ + 1) x✝ = x✝ + nsmulRec n✝ x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_6
x y : ℝ
⊢ ∀ (a b : ℝ), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
case refine'_6
x y a✝ b✝ : ℝ
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_6
x y a✝ b✝ : ℝ
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_6
x y a✝ b✝ : ℝ
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_6.a
x y a✝ b✝ : ℝ
⊢ (a✝ + b✝).cauchy = (b✝ + a✝).cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]
case refine'_6.a
x y a✝ b✝ : ℝ
⊢ a✝.cauchy + b✝.cauchy = b✝.cauchy + a✝.cauchy
[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]
case refine'_6.a
x y a✝ b✝ : ℝ
⊢ a✝.cauchy + b✝.cauchy = b✝.cauchy + a✝.cauchy
[PROOFSTEP]
done
[GOAL]
case refine'_6.a
x y a✝ b✝ : ℝ
⊢ a✝.cauchy + b✝.cauchy = b✝.cauchy + a✝.cauchy
[PROOFSTEP]
apply add_assoc
[GOAL]
case refine'_6.a
x y a✝ b✝ : ℝ
⊢ a✝.cauchy + b✝.cauchy = b✝.cauchy + a✝.cauchy
[PROOFSTEP]
apply add_comm
[GOAL]
case refine'_7
x y : ℝ
⊢ ∀ (a b c : ℝ), a * (b + c) = a * b + a * c
[PROOFSTEP]
intros
[GOAL]
case refine'_7
x y a✝ b✝ c✝ : ℝ
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_7
x y a✝ b✝ c✝ : ℝ
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_7
x y a✝ b✝ c✝ : ℝ
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_7.a
x y a✝ b✝ c✝ : ℝ
⊢ (a✝ * (b✝ + c✝)).cauchy = (a✝ * b✝ + a✝ * c✝).cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]
case refine'_7.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy * (b✝.cauchy + c✝.cauchy) = a✝.cauchy * b✝.cauchy + a✝.cauchy * c✝.cauchy
[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]
case refine'_7.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy * (b✝.cauchy + c✝.cauchy) = a✝.cauchy * b✝.cauchy + a✝.cauchy * c✝.cauchy
[PROOFSTEP]
done
[GOAL]
case refine'_7.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy * (b✝.cauchy + c✝.cauchy) = a✝.cauchy * b✝.cauchy + a✝.cauchy * c✝.cauchy
[PROOFSTEP]
apply add_assoc
[GOAL]
case refine'_7.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy * (b✝.cauchy + c✝.cauchy) = a✝.cauchy * b✝.cauchy + a✝.cauchy * c✝.cauchy
[PROOFSTEP]
apply add_comm
[GOAL]
case refine'_7.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy * (b✝.cauchy + c✝.cauchy) = a✝.cauchy * b✝.cauchy + a✝.cauchy * c✝.cauchy
[PROOFSTEP]
apply left_distrib
[GOAL]
case refine'_8
x y : ℝ
⊢ ∀ (a b c : ℝ), (a + b) * c = a * c + b * c
[PROOFSTEP]
intros
[GOAL]
case refine'_8
x y a✝ b✝ c✝ : ℝ
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_8
x y a✝ b✝ c✝ : ℝ
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_8
x y a✝ b✝ c✝ : ℝ
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_8.a
x y a✝ b✝ c✝ : ℝ
⊢ ((a✝ + b✝) * c✝).cauchy = (a✝ * c✝ + b✝ * c✝).cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]
case refine'_8.a
x y a✝ b✝ c✝ : ℝ
⊢ (a✝.cauchy + b✝.cauchy) * c✝.cauchy = a✝.cauchy * c✝.cauchy + b✝.cauchy * c✝.cauchy
[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]
case refine'_8.a
x y a✝ b✝ c✝ : ℝ
⊢ (a✝.cauchy + b✝.cauchy) * c✝.cauchy = a✝.cauchy * c✝.cauchy + b✝.cauchy * c✝.cauchy
[PROOFSTEP]
done
[GOAL]
case refine'_8.a
x y a✝ b✝ c✝ : ℝ
⊢ (a✝.cauchy + b✝.cauchy) * c✝.cauchy = a✝.cauchy * c✝.cauchy + b✝.cauchy * c✝.cauchy
[PROOFSTEP]
apply add_assoc
[GOAL]
case refine'_8.a
x y a✝ b✝ c✝ : ℝ
⊢ (a✝.cauchy + b✝.cauchy) * c✝.cauchy = a✝.cauchy * c✝.cauchy + b✝.cauchy * c✝.cauchy
[PROOFSTEP]
apply add_comm
[GOAL]
case refine'_8.a
x y a✝ b✝ c✝ : ℝ
⊢ (a✝.cauchy + b✝.cauchy) * c✝.cauchy = a✝.cauchy * c✝.cauchy + b✝.cauchy * c✝.cauchy
[PROOFSTEP]
apply left_distrib
[GOAL]
case refine'_8.a
x y a✝ b✝ c✝ : ℝ
⊢ (a✝.cauchy + b✝.cauchy) * c✝.cauchy = a✝.cauchy * c✝.cauchy + b✝.cauchy * c✝.cauchy
[PROOFSTEP]
apply right_distrib
[GOAL]
case refine'_9
x y : ℝ
⊢ ∀ (a : ℝ), 0 * a = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_9
x y a✝ : ℝ
⊢ 0 * a✝ = 0
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_9
x y a✝ : ℝ
⊢ 0 * a✝ = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_9
x y a✝ : ℝ
⊢ 0 * a✝ = 0
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_9.a
x y a✝ : ℝ
⊢ (0 * a✝).cauchy = 0.cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]

[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]

[PROOFSTEP]
done
[GOAL]
case refine'_10
x y : ℝ
⊢ ∀ (a : ℝ), a * 0 = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_10
x y a✝ : ℝ
⊢ a✝ * 0 = 0
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_10
x y a✝ : ℝ
⊢ a✝ * 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_10
x y a✝ : ℝ
⊢ a✝ * 0 = 0
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_10.a
x y a✝ : ℝ
⊢ (a✝ * 0).cauchy = 0.cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]

[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]

[PROOFSTEP]
done
[GOAL]
case refine'_11
x y : ℝ
⊢ ∀ (a b c : ℝ), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
case refine'_11
x y a✝ b✝ c✝ : ℝ
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_11
x y a✝ b✝ c✝ : ℝ
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
rfl
[GOAL]
case refine'_11
x y a✝ b✝ c✝ : ℝ
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_11.a
x y a✝ b✝ c✝ : ℝ
⊢ (a✝ * b✝ * c✝).cauchy = (a✝ * (b✝ * c✝)).cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]
case refine'_11.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy * c✝.cauchy = a✝.cauchy * (b✝.cauchy * c✝.cauchy)
[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]
case refine'_11.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy * c✝.cauchy = a✝.cauchy * (b✝.cauchy * c✝.cauchy)
[PROOFSTEP]
done
[GOAL]
case refine'_11.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy * c✝.cauchy = a✝.cauchy * (b✝.cauchy * c✝.cauchy)
[PROOFSTEP]
apply add_assoc
[GOAL]
case refine'_11.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy * c✝.cauchy = a✝.cauchy * (b✝.cauchy * c✝.cauchy)
[PROOFSTEP]
apply add_comm
[GOAL]
case refine'_11.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy * c✝.cauchy = a✝.cauchy * (b✝.cauchy * c✝.cauchy)
[PROOFSTEP]
apply left_distrib
[GOAL]
case refine'_11.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy * c✝.cauchy = a✝.cauchy * (b✝.cauchy * c✝.cauchy)
[PROOFSTEP]
apply right_distrib
[GOAL]
case refine'_11.a
x y a✝ b✝ c✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy * c✝.cauchy = a✝.cauchy * (b✝.cauchy * c✝.cauchy)
[PROOFSTEP]
apply mul_assoc
[GOAL]
case refine'_12
x y : ℝ
⊢ ∀ (a : ℝ), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
case refine'_12
x y a✝ : ℝ
⊢ 1 * a✝ = a✝
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_12
x y a✝ : ℝ
⊢ 1 * a✝ = a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_12
x y a✝ : ℝ
⊢ 1 * a✝ = a✝
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_12.a
x y a✝ : ℝ
⊢ (1 * a✝).cauchy = a✝.cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]

[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]

[PROOFSTEP]
done
[GOAL]
case refine'_13
x y : ℝ
⊢ ∀ (a : ℝ), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
case refine'_13
x y a✝ : ℝ
⊢ a✝ * 1 = a✝
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_13
x y a✝ : ℝ
⊢ a✝ * 1 = a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_13
x y a✝ : ℝ
⊢ a✝ * 1 = a✝
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_13.a
x y a✝ : ℝ
⊢ (a✝ * 1).cauchy = a✝.cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]

[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]

[PROOFSTEP]
done
[GOAL]
case refine'_14
x y : ℝ
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_14
x y : ℝ
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_14
x y : ℝ
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_14
x y : ℝ
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_14.a
x y : ℝ
⊢ (NatCast.natCast 0).cauchy = 0.cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]

[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]

[PROOFSTEP]
done
[GOAL]
case refine'_15
x y : ℝ
⊢ ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
intros
[GOAL]
case refine'_15
x y : ℝ
n✝ : ℕ
⊢ NatCast.natCast (n✝ + 1) = NatCast.natCast n✝ + 1
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_15
x y : ℝ
n✝ : ℕ
⊢ NatCast.natCast (n✝ + 1) = NatCast.natCast n✝ + 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_15
x y : ℝ
n✝ : ℕ
⊢ NatCast.natCast (n✝ + 1) = NatCast.natCast n✝ + 1
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_15.a
x y : ℝ
n✝ : ℕ
⊢ (NatCast.natCast (n✝ + 1)).cauchy = (NatCast.natCast n✝ + 1).cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]

[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]

[PROOFSTEP]
done
[GOAL]
case refine'_16
x y : ℝ
⊢ ∀ (x : ℝ), npowRec 0 x = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_16
x y x✝ : ℝ
⊢ npowRec 0 x✝ = 1
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_16
x y x✝ : ℝ
⊢ npowRec 0 x✝ = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_17
x y : ℝ
⊢ ∀ (n : ℕ) (x : ℝ), npowRec (n + 1) x = x * npowRec n x
[PROOFSTEP]
intros
[GOAL]
case refine'_17
x y : ℝ
n✝ : ℕ
x✝ : ℝ
⊢ npowRec (n✝ + 1) x✝ = x✝ * npowRec n✝ x✝
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_17
x y : ℝ
n✝ : ℕ
x✝ : ℝ
⊢ npowRec (n✝ + 1) x✝ = x✝ * npowRec n✝ x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_18
x y : ℝ
⊢ ∀ (a b : ℝ), a - b = a + -b
[PROOFSTEP]
intros
[GOAL]
case refine'_18
x y a✝ b✝ : ℝ
⊢ a✝ - b✝ = a✝ + -b✝
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_18
x y a✝ b✝ : ℝ
⊢ a✝ - b✝ = a✝ + -b✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_19
x y : ℝ
⊢ ∀ (a : ℝ), zsmulRec 0 a = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_19
x y a✝ : ℝ
⊢ zsmulRec 0 a✝ = 0
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_19
x y a✝ : ℝ
⊢ zsmulRec 0 a✝ = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_20
x y : ℝ
⊢ ∀ (n : ℕ) (a : ℝ), zsmulRec (Int.ofNat (Nat.succ n)) a = a + zsmulRec (Int.ofNat n) a
[PROOFSTEP]
intros
[GOAL]
case refine'_20
x y : ℝ
n✝ : ℕ
a✝ : ℝ
⊢ zsmulRec (Int.ofNat (Nat.succ n✝)) a✝ = a✝ + zsmulRec (Int.ofNat n✝) a✝
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_20
x y : ℝ
n✝ : ℕ
a✝ : ℝ
⊢ zsmulRec (Int.ofNat (Nat.succ n✝)) a✝ = a✝ + zsmulRec (Int.ofNat n✝) a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_21
x y : ℝ
⊢ ∀ (n : ℕ) (a : ℝ), zsmulRec (Int.negSucc n) a = -zsmulRec (↑(Nat.succ n)) a
[PROOFSTEP]
intros
[GOAL]
case refine'_21
x y : ℝ
n✝ : ℕ
a✝ : ℝ
⊢ zsmulRec (Int.negSucc n✝) a✝ = -zsmulRec (↑(Nat.succ n✝)) a✝
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_21
x y : ℝ
n✝ : ℕ
a✝ : ℝ
⊢ zsmulRec (Int.negSucc n✝) a✝ = -zsmulRec (↑(Nat.succ n✝)) a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_22
x y : ℝ
⊢ ∀ (a : ℝ), -a + a = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_22
x y a✝ : ℝ
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_22
x y a✝ : ℝ
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_22
x y a✝ : ℝ
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_22.a
x y a✝ : ℝ
⊢ (-a✝ + a✝).cauchy = 0.cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]

[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]

[PROOFSTEP]
done
[GOAL]
case refine'_23
x y : ℝ
⊢ ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
[PROOFSTEP]
intros
[GOAL]
case refine'_23
x y : ℝ
n✝ : ℕ
⊢ IntCast.intCast ↑n✝ = ↑n✝
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_23
x y : ℝ
n✝ : ℕ
⊢ IntCast.intCast ↑n✝ = ↑n✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_24
x y : ℝ
⊢ ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
[PROOFSTEP]
intros
[GOAL]
case refine'_24
x y : ℝ
n✝ : ℕ
⊢ IntCast.intCast (Int.negSucc n✝) = -↑(n✝ + 1)
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_24
x y : ℝ
n✝ : ℕ
⊢ IntCast.intCast (Int.negSucc n✝) = -↑(n✝ + 1)
[PROOFSTEP]
rfl
[GOAL]
case refine'_24
x y : ℝ
n✝ : ℕ
⊢ IntCast.intCast (Int.negSucc n✝) = -↑(n✝ + 1)
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_24.a
x y : ℝ
n✝ : ℕ
⊢ (IntCast.intCast (Int.negSucc n✝)).cauchy = (-↑(n✝ + 1)).cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]

[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]

[PROOFSTEP]
done
[GOAL]
case refine'_25
x y : ℝ
⊢ ∀ (a b : ℝ), a * b = b * a
[PROOFSTEP]
intros
[GOAL]
case refine'_25
x y a✝ b✝ : ℝ
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
first
| rfl
| apply ext_cauchy
  simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
  first
  | done
  | apply add_assoc
  | apply add_comm
  | apply left_distrib
  | apply right_distrib
  | apply mul_assoc
  | apply mul_comm
[GOAL]
case refine'_25
x y a✝ b✝ : ℝ
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_25
x y a✝ b✝ : ℝ
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
apply ext_cauchy
[GOAL]
case refine'_25.a
x y a✝ b✝ : ℝ
⊢ (a✝ * b✝).cauchy = (b✝ * a✝).cauchy
[PROOFSTEP]
simp [cauchy_add, cauchy_zero, cauchy_one, cauchy_neg, cauchy_mul, cauchy_natCast, cauchy_intCast]
[GOAL]
case refine'_25.a
x y a✝ b✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy = b✝.cauchy * a✝.cauchy
[PROOFSTEP]
first
| done
| apply add_assoc
| apply add_comm
| apply left_distrib
| apply right_distrib
| apply mul_assoc
| apply mul_comm
[GOAL]
case refine'_25.a
x y a✝ b✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy = b✝.cauchy * a✝.cauchy
[PROOFSTEP]
done
[GOAL]
case refine'_25.a
x y a✝ b✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy = b✝.cauchy * a✝.cauchy
[PROOFSTEP]
apply add_assoc
[GOAL]
case refine'_25.a
x y a✝ b✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy = b✝.cauchy * a✝.cauchy
[PROOFSTEP]
apply add_comm
[GOAL]
case refine'_25.a
x y a✝ b✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy = b✝.cauchy * a✝.cauchy
[PROOFSTEP]
apply left_distrib
[GOAL]
case refine'_25.a
x y a✝ b✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy = b✝.cauchy * a✝.cauchy
[PROOFSTEP]
apply right_distrib
[GOAL]
case refine'_25.a
x y a✝ b✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy = b✝.cauchy * a✝.cauchy
[PROOFSTEP]
apply mul_assoc
[GOAL]
case refine'_25.a
x y a✝ b✝ : ℝ
⊢ a✝.cauchy * b✝.cauchy = b✝.cauchy * a✝.cauchy
[PROOFSTEP]
apply mul_comm
[GOAL]
x y : ℝ
⊢ Ring ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ CommSemiring ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ Semiring ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ CommMonoidWithZero ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ MonoidWithZero ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ AddCommGroup ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ AddGroup ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ AddCommMonoid ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ AddMonoid ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ AddLeftCancelSemigroup ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ AddRightCancelSemigroup ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ AddCommSemigroup ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ AddSemigroup ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ CommMonoid ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ Monoid ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ CommSemigroup ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ Semigroup ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
f g : CauSeq ℚ abs
⊢ Real.lt { cauchy := Quotient.mk equiv f } { cauchy := Quotient.mk equiv g } ↔ f < g
[PROOFSTEP]
rw [lt_def]
[GOAL]
x y : ℝ
f g : CauSeq ℚ abs
⊢ (match { cauchy := Quotient.mk equiv f }, { cauchy := Quotient.mk equiv g } with
    | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x x_1 => x < x_1) Real.definition.proof_1✝) ↔
    f < g
[PROOFSTEP]
rfl
[GOAL]
x y : ℝ
⊢ mk 0 = 0
[PROOFSTEP]
rw [← ofCauchy_zero]
[GOAL]
x y : ℝ
⊢ mk 0 = { cauchy := 0 }
[PROOFSTEP]
rfl
[GOAL]
x y : ℝ
⊢ mk 1 = 1
[PROOFSTEP]
rw [← ofCauchy_one]
[GOAL]
x y : ℝ
⊢ mk 1 = { cauchy := 1 }
[PROOFSTEP]
rfl
[GOAL]
x y : ℝ
f g : CauSeq ℚ abs
⊢ mk (f + g) = mk f + mk g
[PROOFSTEP]
simp [mk, ← ofCauchy_add]
[GOAL]
x y : ℝ
f g : CauSeq ℚ abs
⊢ mk (f * g) = mk f * mk g
[PROOFSTEP]
simp [mk, ← ofCauchy_mul]
[GOAL]
x y : ℝ
f : CauSeq ℚ abs
⊢ mk (-f) = -mk f
[PROOFSTEP]
simp [mk, ← ofCauchy_neg]
[GOAL]
x y : ℝ
f : CauSeq ℚ abs
⊢ 0 < mk f ↔ Pos f
[PROOFSTEP]
rw [← mk_zero, mk_lt]
[GOAL]
x y : ℝ
f : CauSeq ℚ abs
⊢ 0 < f ↔ Pos f
[PROOFSTEP]
exact iff_of_eq (congr_arg Pos (sub_zero f))
[GOAL]
x✝ y✝ x y : ℝ
⊢ Real.le x y ↔ x < y ∨ x = y
[PROOFSTEP]
rw [le_def]
[GOAL]
x y : ℝ
f g : CauSeq ℚ abs
⊢ mk f ≤ mk g ↔ f ≤ g
[PROOFSTEP]
simp [le_def', mk_eq]
[GOAL]
x y : ℝ
f g : CauSeq ℚ abs
⊢ f < g ∨ f ≈ g ↔ f ≤ g
[PROOFSTEP]
rfl
[GOAL]
x✝ y : ℝ
C : ℝ → Prop
x : ℝ
h : ∀ (y : CauSeq ℚ abs), C (mk y)
⊢ C x
[PROOFSTEP]
cases' x with x
[GOAL]
case ofCauchy
x✝ y : ℝ
C : ℝ → Prop
h : ∀ (y : CauSeq ℚ abs), C (mk y)
x : Cauchy abs
⊢ C { cauchy := x }
[PROOFSTEP]
induction' x using Quot.induction_on with x
[GOAL]
case ofCauchy.h
x✝ y : ℝ
C : ℝ → Prop
h : ∀ (y : CauSeq ℚ abs), C (mk y)
x : CauSeq ℚ abs
⊢ C { cauchy := Quot.mk Setoid.r x }
[PROOFSTEP]
exact h x
[GOAL]
x y a b c : ℝ
⊢ c + a < c + b ↔ a < b
[PROOFSTEP]
induction a using Real.ind_mk
[GOAL]
case h
x y b c : ℝ
y✝ : CauSeq ℚ abs
⊢ c + mk y✝ < c + b ↔ mk y✝ < b
[PROOFSTEP]
induction b using Real.ind_mk
[GOAL]
case h.h
x y c : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ c + mk y✝¹ < c + mk y✝ ↔ mk y✝¹ < mk y✝
[PROOFSTEP]
induction c using Real.ind_mk
[GOAL]
case h.h.h
x y : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝ + mk y✝² < mk y✝ + mk y✝¹ ↔ mk y✝² < mk y✝¹
[PROOFSTEP]
simp only [mk_lt, ← mk_add]
[GOAL]
case h.h.h
x y : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ y✝ + y✝² < y✝ + y✝¹ ↔ y✝² < y✝¹
[PROOFSTEP]
show Pos _ ↔ Pos _
[GOAL]
case h.h.h
x y : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ Pos (y✝ + y✝¹ - (y✝ + y✝²)) ↔ Pos (y✝¹ - y✝²)
[PROOFSTEP]
rw [add_sub_add_left_eq_sub]
[GOAL]
x y a : ℝ
⊢ a ≤ a
[PROOFSTEP]
induction' a using Real.ind_mk with a
[GOAL]
case h
x y : ℝ
a : CauSeq ℚ abs
⊢ mk a ≤ mk a
[PROOFSTEP]
rw [mk_le]
[GOAL]
x y a b c : ℝ
⊢ a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
induction' a using Real.ind_mk with a
[GOAL]
case h
x y b c : ℝ
a : CauSeq ℚ abs
⊢ mk a ≤ b → b ≤ c → mk a ≤ c
[PROOFSTEP]
induction' b using Real.ind_mk with b
[GOAL]
case h.h
x y c : ℝ
a b : CauSeq ℚ abs
⊢ mk a ≤ mk b → mk b ≤ c → mk a ≤ c
[PROOFSTEP]
induction' c using Real.ind_mk with c
[GOAL]
case h.h.h
x y : ℝ
a b c : CauSeq ℚ abs
⊢ mk a ≤ mk b → mk b ≤ mk c → mk a ≤ mk c
[PROOFSTEP]
simpa using le_trans
[GOAL]
x y a b : ℝ
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
induction' a using Real.ind_mk with a
[GOAL]
case h
x y b : ℝ
a : CauSeq ℚ abs
⊢ mk a < b ↔ mk a ≤ b ∧ ¬b ≤ mk a
[PROOFSTEP]
induction' b using Real.ind_mk with b
[GOAL]
case h.h
x y : ℝ
a b : CauSeq ℚ abs
⊢ mk a < mk b ↔ mk a ≤ mk b ∧ ¬mk b ≤ mk a
[PROOFSTEP]
simpa using lt_iff_le_not_le
[GOAL]
x y a b : ℝ
⊢ a ≤ b → b ≤ a → a = b
[PROOFSTEP]
induction' a using Real.ind_mk with a
[GOAL]
case h
x y b : ℝ
a : CauSeq ℚ abs
⊢ mk a ≤ b → b ≤ mk a → mk a = b
[PROOFSTEP]
induction' b using Real.ind_mk with b
[GOAL]
case h.h
x y : ℝ
a b : CauSeq ℚ abs
⊢ mk a ≤ mk b → mk b ≤ mk a → mk a = mk b
[PROOFSTEP]
simpa [mk_eq] using @CauSeq.le_antisymm _ _ a b
[GOAL]
x y : ℝ
⊢ Preorder ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x✝ y✝ : ℝ
x y : ℚ
⊢ ↑x < ↑y ↔ x < y
[PROOFSTEP]
erw [mk_lt]
[GOAL]
x✝ y✝ : ℝ
x y : ℚ
⊢ const abs ↑x < const abs ↑y ↔ x < y
[PROOFSTEP]
exact const_lt
[GOAL]
x y : ℝ
⊢ 0 < 1
[PROOFSTEP]
convert ratCast_lt.2 zero_lt_one
[GOAL]
case h.e'_3
x y : ℝ
⊢ 0 = ↑0
[PROOFSTEP]
simp [← ofCauchy_ratCast, ofCauchy_one, ofCauchy_zero]
[GOAL]
case h.e'_4
x y : ℝ
⊢ 1 = ↑1
[PROOFSTEP]
simp [← ofCauchy_ratCast, ofCauchy_one, ofCauchy_zero]
[GOAL]
x y a b : ℝ
⊢ 0 < a → 0 < b → 0 < a * b
[PROOFSTEP]
induction' a using Real.ind_mk with a
[GOAL]
case h
x y b : ℝ
a : CauSeq ℚ abs
⊢ 0 < mk a → 0 < b → 0 < mk a * b
[PROOFSTEP]
induction' b using Real.ind_mk with b
[GOAL]
case h.h
x y : ℝ
a b : CauSeq ℚ abs
⊢ 0 < mk a → 0 < mk b → 0 < mk a * mk b
[PROOFSTEP]
simpa only [mk_lt, mk_pos, ← mk_mul] using CauSeq.mul_pos
[GOAL]
x y : ℝ
src✝² : CommRing ℝ := commRing
src✝¹ : PartialOrder ℝ := partialOrder
src✝ : Semiring ℝ := semiring
⊢ ∀ (a b : ℝ), a ≤ b → ∀ (c : ℝ), c + a ≤ c + b
[PROOFSTEP]
simp only [le_iff_eq_or_lt]
[GOAL]
x y : ℝ
src✝² : CommRing ℝ := commRing
src✝¹ : PartialOrder ℝ := partialOrder
src✝ : Semiring ℝ := semiring
⊢ ∀ (a b : ℝ), a = b ∨ a < b → ∀ (c : ℝ), c + a = c + b ∨ c + a < c + b
[PROOFSTEP]
rintro a b ⟨rfl, h⟩
[GOAL]
case inl.refl
x y : ℝ
src✝² : CommRing ℝ := commRing
src✝¹ : PartialOrder ℝ := partialOrder
src✝ : Semiring ℝ := semiring
a : ℝ
⊢ ∀ (c : ℝ), c + a = c + a ∨ c + a < c + a
[PROOFSTEP]
simp only [lt_self_iff_false, or_false, forall_const]
[GOAL]
case inr
x y : ℝ
src✝² : CommRing ℝ := commRing
src✝¹ : PartialOrder ℝ := partialOrder
src✝ : Semiring ℝ := semiring
a b : ℝ
h✝ : a < b
⊢ ∀ (c : ℝ), c + a = c + b ∨ c + a < c + b
[PROOFSTEP]
exact fun c => Or.inr ((add_lt_add_iff_left c).2 ‹_›)
[GOAL]
x y : ℝ
a b : CauSeq ℚ abs
⊢ { cauchy := Quotient.mk equiv (a ⊔ b) } = Real.sup { cauchy := Quotient.mk equiv a } { cauchy := Quotient.mk equiv b }
[PROOFSTEP]
rw [sup_def]
[GOAL]
x y : ℝ
a b : CauSeq ℚ abs
⊢ { cauchy := Quotient.mk equiv (a ⊔ b) } =
    match { cauchy := Quotient.mk equiv a }, { cauchy := Quotient.mk equiv b } with
    | { cauchy := x }, { cauchy := y } =>
      {
        cauchy :=
          Quotient.map₂ (fun x x_1 => x ⊔ x_1)
            (_ : ∀ (x x_1 : CauSeq ℚ abs), x ≈ x_1 → ∀ (x_2 x_3 : CauSeq ℚ abs), x_2 ≈ x_3 → x ⊔ x_2 ≈ x_1 ⊔ x_3) x y }
[PROOFSTEP]
rfl
[GOAL]
x y : ℝ
a b : CauSeq ℚ abs
⊢ { cauchy := Quotient.mk equiv (a ⊓ b) } = Real.inf { cauchy := Quotient.mk equiv a } { cauchy := Quotient.mk equiv b }
[PROOFSTEP]
rw [inf_def]
[GOAL]
x y : ℝ
a b : CauSeq ℚ abs
⊢ { cauchy := Quotient.mk equiv (a ⊓ b) } =
    match { cauchy := Quotient.mk equiv a }, { cauchy := Quotient.mk equiv b } with
    | { cauchy := x }, { cauchy := y } =>
      {
        cauchy :=
          Quotient.map₂ (fun x x_1 => x ⊓ x_1)
            (_ : ∀ (x x_1 : CauSeq ℚ abs), x ≈ x_1 → ∀ (x_2 x_3 : CauSeq ℚ abs), x_2 ≈ x_3 → x ⊓ x_2 ≈ x_1 ⊓ x_3) x y }
[PROOFSTEP]
rfl
[GOAL]
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
⊢ ∀ (a b : ℝ), a ≤ a ⊔ b
[PROOFSTEP]
intros a b
[GOAL]
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b : ℝ
⊢ a ≤ a ⊔ b
[PROOFSTEP]
induction' a using Real.ind_mk with a
[GOAL]
case h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
b : ℝ
a : CauSeq ℚ abs
⊢ mk a ≤ mk a ⊔ b
[PROOFSTEP]
induction' b using Real.ind_mk with b
[GOAL]
case h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b : CauSeq ℚ abs
⊢ mk a ≤ mk a ⊔ mk b
[PROOFSTEP]
rw [← mk_sup, mk_le]
[GOAL]
case h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b : CauSeq ℚ abs
⊢ a ≤ a ⊔ b
[PROOFSTEP]
exact CauSeq.le_sup_left
[GOAL]
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
⊢ ∀ (a b : ℝ), b ≤ a ⊔ b
[PROOFSTEP]
intros a b
[GOAL]
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b : ℝ
⊢ b ≤ a ⊔ b
[PROOFSTEP]
induction' a using Real.ind_mk with a
[GOAL]
case h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
b : ℝ
a : CauSeq ℚ abs
⊢ b ≤ mk a ⊔ b
[PROOFSTEP]
induction' b using Real.ind_mk with b
[GOAL]
case h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b : CauSeq ℚ abs
⊢ mk b ≤ mk a ⊔ mk b
[PROOFSTEP]
rw [← mk_sup, mk_le]
[GOAL]
case h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b : CauSeq ℚ abs
⊢ b ≤ a ⊔ b
[PROOFSTEP]
exact CauSeq.le_sup_right
[GOAL]
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
⊢ ∀ (a b c : ℝ), a ≤ c → b ≤ c → a ⊔ b ≤ c
[PROOFSTEP]
intros a b c
[GOAL]
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b c : ℝ
⊢ a ≤ c → b ≤ c → a ⊔ b ≤ c
[PROOFSTEP]
induction' a using Real.ind_mk with a
[GOAL]
case h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
b c : ℝ
a : CauSeq ℚ abs
⊢ mk a ≤ c → b ≤ c → mk a ⊔ b ≤ c
[PROOFSTEP]
induction' b using Real.ind_mk with b
[GOAL]
case h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
c : ℝ
a b : CauSeq ℚ abs
⊢ mk a ≤ c → mk b ≤ c → mk a ⊔ mk b ≤ c
[PROOFSTEP]
induction' c using Real.ind_mk with c
[GOAL]
case h.h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b c : CauSeq ℚ abs
⊢ mk a ≤ mk c → mk b ≤ mk c → mk a ⊔ mk b ≤ mk c
[PROOFSTEP]
simp_rw [← mk_sup, mk_le]
[GOAL]
case h.h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b c : CauSeq ℚ abs
⊢ a ≤ c → b ≤ c → a ⊔ b ≤ c
[PROOFSTEP]
exact CauSeq.sup_le
[GOAL]
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
⊢ ∀ (a b : ℝ), a ⊓ b ≤ a
[PROOFSTEP]
intros a b
[GOAL]
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b : ℝ
⊢ a ⊓ b ≤ a
[PROOFSTEP]
induction' a using Real.ind_mk with a
[GOAL]
case h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
b : ℝ
a : CauSeq ℚ abs
⊢ mk a ⊓ b ≤ mk a
[PROOFSTEP]
induction' b using Real.ind_mk with b
[GOAL]
case h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b : CauSeq ℚ abs
⊢ mk a ⊓ mk b ≤ mk a
[PROOFSTEP]
rw [← mk_inf, mk_le]
[GOAL]
case h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b : CauSeq ℚ abs
⊢ a ⊓ b ≤ a
[PROOFSTEP]
exact CauSeq.inf_le_left
[GOAL]
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
⊢ ∀ (a b : ℝ), a ⊓ b ≤ b
[PROOFSTEP]
intros a b
[GOAL]
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b : ℝ
⊢ a ⊓ b ≤ b
[PROOFSTEP]
induction' a using Real.ind_mk with a
[GOAL]
case h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
b : ℝ
a : CauSeq ℚ abs
⊢ mk a ⊓ b ≤ b
[PROOFSTEP]
induction' b using Real.ind_mk with b
[GOAL]
case h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b : CauSeq ℚ abs
⊢ mk a ⊓ mk b ≤ mk b
[PROOFSTEP]
rw [← mk_inf, mk_le]
[GOAL]
case h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b : CauSeq ℚ abs
⊢ a ⊓ b ≤ b
[PROOFSTEP]
exact CauSeq.inf_le_right
[GOAL]
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
⊢ ∀ (a b c : ℝ), a ≤ b → a ≤ c → a ≤ b ⊓ c
[PROOFSTEP]
intros a b c
[GOAL]
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b c : ℝ
⊢ a ≤ b → a ≤ c → a ≤ b ⊓ c
[PROOFSTEP]
induction' a using Real.ind_mk with a
[GOAL]
case h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
b c : ℝ
a : CauSeq ℚ abs
⊢ mk a ≤ b → mk a ≤ c → mk a ≤ b ⊓ c
[PROOFSTEP]
induction' b using Real.ind_mk with b
[GOAL]
case h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
c : ℝ
a b : CauSeq ℚ abs
⊢ mk a ≤ mk b → mk a ≤ c → mk a ≤ mk b ⊓ c
[PROOFSTEP]
induction' c using Real.ind_mk with c
[GOAL]
case h.h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b c : CauSeq ℚ abs
⊢ mk a ≤ mk b → mk a ≤ mk c → mk a ≤ mk b ⊓ mk c
[PROOFSTEP]
simp_rw [← mk_inf, mk_le]
[GOAL]
case h.h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b c : CauSeq ℚ abs
⊢ a ≤ b → a ≤ c → a ≤ b ⊓ c
[PROOFSTEP]
exact CauSeq.le_inf
[GOAL]
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
⊢ ∀ (x y z : ℝ), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
[PROOFSTEP]
intros a b c
[GOAL]
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b c : ℝ
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
[PROOFSTEP]
induction' a using Real.ind_mk with a
[GOAL]
case h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
b c : ℝ
a : CauSeq ℚ abs
⊢ (mk a ⊔ b) ⊓ (mk a ⊔ c) ≤ mk a ⊔ b ⊓ c
[PROOFSTEP]
induction' b using Real.ind_mk with b
[GOAL]
case h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
c : ℝ
a b : CauSeq ℚ abs
⊢ (mk a ⊔ mk b) ⊓ (mk a ⊔ c) ≤ mk a ⊔ mk b ⊓ c
[PROOFSTEP]
induction' c using Real.ind_mk with c
[GOAL]
case h.h.h
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b c : CauSeq ℚ abs
⊢ (mk a ⊔ mk b) ⊓ (mk a ⊔ mk c) ≤ mk a ⊔ mk b ⊓ mk c
[PROOFSTEP]
apply Eq.le
[GOAL]
case h.h.h.a
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b c : CauSeq ℚ abs
⊢ (mk a ⊔ mk b) ⊓ (mk a ⊔ mk c) = mk a ⊔ mk b ⊓ mk c
[PROOFSTEP]
simp only [← mk_sup, ← mk_inf]
[GOAL]
case h.h.h.a
x y : ℝ
src✝ : PartialOrder ℝ := partialOrder
a b c : CauSeq ℚ abs
⊢ mk ((a ⊔ b) ⊓ (a ⊔ c)) = mk (a ⊔ b ⊓ c)
[PROOFSTEP]
exact congr_arg mk (CauSeq.sup_inf_distrib_left _ _ _).symm
[GOAL]
x y : ℝ
⊢ ∀ (a b : ℝ), a ≤ b ∨ b ≤ a
[PROOFSTEP]
intros a b
[GOAL]
x y a b : ℝ
⊢ a ≤ b ∨ b ≤ a
[PROOFSTEP]
induction' a using Real.ind_mk with a
[GOAL]
case h
x y b : ℝ
a : CauSeq ℚ abs
⊢ mk a ≤ b ∨ b ≤ mk a
[PROOFSTEP]
induction' b using Real.ind_mk with b
[GOAL]
case h.h
x y : ℝ
a b : CauSeq ℚ abs
⊢ mk a ≤ mk b ∨ mk b ≤ mk a
[PROOFSTEP]
simpa using le_total a b
[GOAL]
x y : ℝ
⊢ LinearOrderedRing ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ LinearOrderedSemiring ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
src✝ : LinearOrderedCommRing ℝ := linearOrderedCommRing
⊢ ∀ (a : ℝ), a ≠ 0 → a * a⁻¹ = 1
[PROOFSTEP]
rintro ⟨a⟩ h
[GOAL]
case ofCauchy
x y : ℝ
src✝ : LinearOrderedCommRing ℝ := linearOrderedCommRing
a : Cauchy abs
h : { cauchy := a } ≠ 0
⊢ { cauchy := a } * { cauchy := a }⁻¹ = 1
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case ofCauchy
x y : ℝ
src✝ : LinearOrderedCommRing ℝ := linearOrderedCommRing
a : Cauchy abs
h : { cauchy := a } ≠ 0
⊢ { cauchy := a }⁻¹ * { cauchy := a } = 1
[PROOFSTEP]
simp only [← ofCauchy_inv, ← ofCauchy_mul, ← ofCauchy_one, ← ofCauchy_zero, Ne.def, ofCauchy.injEq] at *
[GOAL]
case ofCauchy
x y : ℝ
src✝ : LinearOrderedCommRing ℝ := linearOrderedCommRing
a : Cauchy abs
h : ¬a = 0
⊢ a⁻¹ * a = 1
[PROOFSTEP]
exact CauSeq.Completion.inv_mul_cancel h
[GOAL]
x y : ℝ
src✝ : LinearOrderedCommRing ℝ := linearOrderedCommRing
⊢ 0⁻¹ = 0
[PROOFSTEP]
simp [← ofCauchy_zero, ← ofCauchy_inv]
[GOAL]
x y : ℝ
src✝ : LinearOrderedCommRing ℝ := linearOrderedCommRing
n : ℤ
d : ℕ
hd : d ≠ 0
h2 : Nat.coprime (Int.natAbs n) d
⊢ ↑(Rat.mk' n d) = ↑n * (↑d)⁻¹
[PROOFSTEP]
rw [← ofCauchy_ratCast, Rat.cast_mk', ofCauchy_mul, ofCauchy_inv, ofCauchy_natCast, ofCauchy_intCast]
[GOAL]
x y : ℝ
⊢ LinearOrderedAddCommGroup ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ Field ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
⊢ DivisionRing ℝ
[PROOFSTEP]
infer_instance
[GOAL]
x y a b : ℝ
⊢ Decidable (a < b)
[PROOFSTEP]
infer_instance
[GOAL]
x y a b : ℝ
⊢ Decidable (a ≤ b)
[PROOFSTEP]
infer_instance
[GOAL]
x y a b : ℝ
⊢ Decidable (a = b)
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
f : CauSeq ℚ abs
⊢ (∃ i, ∀ (j : ℕ), j ≥ i → x ≤ ↑(↑f j)) → x ≤ mk f
[PROOFSTEP]
intro h
[GOAL]
x y : ℝ
f : CauSeq ℚ abs
h : ∃ i, ∀ (j : ℕ), j ≥ i → x ≤ ↑(↑f j)
⊢ x ≤ mk f
[PROOFSTEP]
induction' x using Real.ind_mk with x
[GOAL]
case h
x✝ y : ℝ
f : CauSeq ℚ abs
h✝ : ∃ i, ∀ (j : ℕ), j ≥ i → x✝ ≤ ↑(↑f j)
x : CauSeq ℚ abs
h : ∃ i, ∀ (j : ℕ), j ≥ i → mk x ≤ ↑(↑f j)
⊢ mk x ≤ mk f
[PROOFSTEP]
apply le_of_not_lt
[GOAL]
case h.h
x✝ y : ℝ
f : CauSeq ℚ abs
h✝ : ∃ i, ∀ (j : ℕ), j ≥ i → x✝ ≤ ↑(↑f j)
x : CauSeq ℚ abs
h : ∃ i, ∀ (j : ℕ), j ≥ i → mk x ≤ ↑(↑f j)
⊢ ¬mk f < mk x
[PROOFSTEP]
rw [mk_lt]
[GOAL]
case h.h
x✝ y : ℝ
f : CauSeq ℚ abs
h✝ : ∃ i, ∀ (j : ℕ), j ≥ i → x✝ ≤ ↑(↑f j)
x : CauSeq ℚ abs
h : ∃ i, ∀ (j : ℕ), j ≥ i → mk x ≤ ↑(↑f j)
⊢ ¬f < x
[PROOFSTEP]
rintro ⟨K, K0, hK⟩
[GOAL]
case h.h.intro.intro
x✝ y : ℝ
f : CauSeq ℚ abs
h✝ : ∃ i, ∀ (j : ℕ), j ≥ i → x✝ ≤ ↑(↑f j)
x : CauSeq ℚ abs
h : ∃ i, ∀ (j : ℕ), j ≥ i → mk x ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ ↑(x - f) j
⊢ False
[PROOFSTEP]
obtain ⟨i, H⟩ := exists_forall_ge_and h (exists_forall_ge_and hK (f.cauchy₃ <| half_pos K0))
[GOAL]
case h.h.intro.intro.intro
x✝ y : ℝ
f : CauSeq ℚ abs
h✝ : ∃ i, ∀ (j : ℕ), j ≥ i → x✝ ≤ ↑(↑f j)
x : CauSeq ℚ abs
h : ∃ i, ∀ (j : ℕ), j ≥ i → mk x ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ ↑(x - f) j
i : ℕ
H : ∀ (j : ℕ), j ≥ i → mk x ≤ ↑(↑f j) ∧ K ≤ ↑(x - f) j ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K / 2
⊢ False
[PROOFSTEP]
apply not_lt_of_le (H _ le_rfl).1
[GOAL]
case h.h.intro.intro.intro
x✝ y : ℝ
f : CauSeq ℚ abs
h✝ : ∃ i, ∀ (j : ℕ), j ≥ i → x✝ ≤ ↑(↑f j)
x : CauSeq ℚ abs
h : ∃ i, ∀ (j : ℕ), j ≥ i → mk x ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ ↑(x - f) j
i : ℕ
H : ∀ (j : ℕ), j ≥ i → mk x ≤ ↑(↑f j) ∧ K ≤ ↑(x - f) j ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K / 2
⊢ ↑(↑f i) < mk x
[PROOFSTEP]
erw [mk_lt]
[GOAL]
case h.h.intro.intro.intro
x✝ y : ℝ
f : CauSeq ℚ abs
h✝ : ∃ i, ∀ (j : ℕ), j ≥ i → x✝ ≤ ↑(↑f j)
x : CauSeq ℚ abs
h : ∃ i, ∀ (j : ℕ), j ≥ i → mk x ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ ↑(x - f) j
i : ℕ
H : ∀ (j : ℕ), j ≥ i → mk x ≤ ↑(↑f j) ∧ K ≤ ↑(x - f) j ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K / 2
⊢ const abs ↑(↑f i) < x
[PROOFSTEP]
refine' ⟨_, half_pos K0, i, fun j ij => _⟩
[GOAL]
case h.h.intro.intro.intro
x✝ y : ℝ
f : CauSeq ℚ abs
h✝ : ∃ i, ∀ (j : ℕ), j ≥ i → x✝ ≤ ↑(↑f j)
x : CauSeq ℚ abs
h : ∃ i, ∀ (j : ℕ), j ≥ i → mk x ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ ↑(x - f) j
i : ℕ
H : ∀ (j : ℕ), j ≥ i → mk x ≤ ↑(↑f j) ∧ K ≤ ↑(x - f) j ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K / 2
j : ℕ
ij : j ≥ i
⊢ K / 2 ≤ ↑(x - const abs ↑(↑f i)) j
[PROOFSTEP]
have := add_le_add (H _ ij).2.1 (le_of_lt (abs_lt.1 <| (H _ le_rfl).2.2 _ ij).1)
[GOAL]
case h.h.intro.intro.intro
x✝ y : ℝ
f : CauSeq ℚ abs
h✝ : ∃ i, ∀ (j : ℕ), j ≥ i → x✝ ≤ ↑(↑f j)
x : CauSeq ℚ abs
h : ∃ i, ∀ (j : ℕ), j ≥ i → mk x ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ (j : ℕ), j ≥ i → K ≤ ↑(x - f) j
i : ℕ
H : ∀ (j : ℕ), j ≥ i → mk x ≤ ↑(↑f j) ∧ K ≤ ↑(x - f) j ∧ ∀ (k : ℕ), k ≥ j → |↑f k - ↑f j| < K / 2
j : ℕ
ij : j ≥ i
this : K + -(K / 2) ≤ ↑(x - f) j + (↑f j - ↑f i)
⊢ K / 2 ≤ ↑(x - const abs ↑(↑f i)) j
[PROOFSTEP]
rwa [← sub_eq_add_neg, sub_self_div_two, sub_apply, sub_add_sub_cancel] at this
[GOAL]
x✝ y : ℝ
f : CauSeq ℚ abs
x : ℝ
h : ∃ i, ∀ (j : ℕ), j ≥ i → ↑(↑f j) ≤ x
⊢ mk f ≤ x
[PROOFSTEP]
cases' h with i H
[GOAL]
case intro
x✝ y : ℝ
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ↑(↑f j) ≤ x
⊢ mk f ≤ x
[PROOFSTEP]
rw [← neg_le_neg_iff, ← mk_neg]
[GOAL]
case intro
x✝ y : ℝ
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ↑(↑f j) ≤ x
⊢ -x ≤ mk (-f)
[PROOFSTEP]
exact le_mk_of_forall_le ⟨i, fun j ij => by simp [H _ ij]⟩
[GOAL]
x✝ y : ℝ
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ↑(↑f j) ≤ x
j : ℕ
ij : j ≥ i
⊢ -x ≤ ↑(↑(-f) j)
[PROOFSTEP]
simp [H _ ij]
[GOAL]
x y : ℝ
f : ℕ → ℚ
H : IsCauSeq abs f
ε : ℝ
ε0 : ε > 0
δ : ℚ
δ0 : 0 < δ
δε : ↑δ < ε
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → |f j - f i| < δ
j : ℕ
ij : j ≥ i
⊢ |(fun i => ↑(f i)) j - (fun i => ↑(f i)) i| < ↑δ
[PROOFSTEP]
simpa using (@Rat.cast_lt ℝ _ _ _).2 (hi _ ij)
[GOAL]
x y : ℝ
f : ℕ → ℚ
H : IsCauSeq abs fun i => ↑(f i)
ε : ℚ
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → |(fun i => ↑(f i)) j - (fun i => ↑(f i)) i| < ↑ε
j : ℕ
ij : j ≥ i
⊢ ↑|f j - f i| < ↑ε
[PROOFSTEP]
simpa using hi _ ij
[GOAL]
x y : ℝ
S : Set ℝ
hne : Set.Nonempty S
hbdd : BddAbove S
⊢ ∃ x, IsLUB S x
[PROOFSTEP]
rcases hne, hbdd with ⟨⟨L, hL⟩, ⟨U, hU⟩⟩
[GOAL]
case intro.intro
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
⊢ ∃ x, IsLUB S x
[PROOFSTEP]
have : ∀ d : ℕ, BddAbove {m : ℤ | ∃ y ∈ S, (m : ℝ) ≤ y * d} :=
  by
  cases' exists_int_gt U with k hk
  refine' fun d => ⟨k * d, fun z h => _⟩
  rcases h with ⟨y, yS, hy⟩
  refine' Int.cast_le.1 (hy.trans _)
  push_cast
  exact mul_le_mul_of_nonneg_right ((hU yS).trans hk.le) d.cast_nonneg
[GOAL]
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
⊢ ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
[PROOFSTEP]
cases' exists_int_gt U with k hk
[GOAL]
case intro
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
k : ℤ
hk : U < ↑k
⊢ ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
[PROOFSTEP]
refine' fun d => ⟨k * d, fun z h => _⟩
[GOAL]
case intro
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
k : ℤ
hk : U < ↑k
d : ℕ
z : ℤ
h : z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
⊢ z ≤ k * ↑d
[PROOFSTEP]
rcases h with ⟨y, yS, hy⟩
[GOAL]
case intro.intro.intro
x y✝ : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
k : ℤ
hk : U < ↑k
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ S
hy : ↑z ≤ y * ↑d
⊢ z ≤ k * ↑d
[PROOFSTEP]
refine' Int.cast_le.1 (hy.trans _)
[GOAL]
case intro.intro.intro
x y✝ : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
k : ℤ
hk : U < ↑k
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ S
hy : ↑z ≤ y * ↑d
⊢ y * ↑d ≤ ↑(k * ↑d)
[PROOFSTEP]
push_cast
[GOAL]
case intro.intro.intro
x y✝ : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
k : ℤ
hk : U < ↑k
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ S
hy : ↑z ≤ y * ↑d
⊢ y * ↑d ≤ ↑k * ↑d
[PROOFSTEP]
exact mul_le_mul_of_nonneg_right ((hU yS).trans hk.le) d.cast_nonneg
[GOAL]
case intro.intro
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
⊢ ∃ x, IsLUB S x
[PROOFSTEP]
choose f hf using fun d : ℕ => Int.exists_greatest_of_bdd (this d) ⟨⌊L * d⌋, L, hL, Int.floor_le _⟩
[GOAL]
case intro.intro
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
⊢ ∃ x, IsLUB S x
[PROOFSTEP]
have hf₁ : ∀ n > 0, ∃ y ∈ S, ((f n / n : ℚ) : ℝ) ≤ y := fun n n0 =>
  let ⟨y, yS, hy⟩ := (hf n).1
  ⟨y, yS, by simpa using (div_le_iff (Nat.cast_pos.2 n0 : (_ : ℝ) < _)).2 hy⟩
[GOAL]
x y✝ : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ S
hy : ↑(f n) ≤ y * ↑n
⊢ ↑(↑(f n) / ↑n) ≤ y
[PROOFSTEP]
simpa using (div_le_iff (Nat.cast_pos.2 n0 : (_ : ℝ) < _)).2 hy
[GOAL]
case intro.intro
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
⊢ ∃ x, IsLUB S x
[PROOFSTEP]
have hf₂ : ∀ n > 0, ∀ y ∈ S, (y - ((n : ℕ) : ℝ)⁻¹) < (f n / n : ℚ) :=
  by
  intro n n0 y yS
  have := (Int.sub_one_lt_floor _).trans_le (Int.cast_le.2 <| (hf n).2 _ ⟨y, yS, Int.floor_le _⟩)
  simp only [Rat.cast_div, Rat.cast_coe_int, Rat.cast_coe_nat, gt_iff_lt]
  rwa [lt_div_iff (Nat.cast_pos.2 n0 : (_ : ℝ) < _), sub_mul, _root_.inv_mul_cancel]
  exact ne_of_gt (Nat.cast_pos.2 n0)
[GOAL]
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
⊢ ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
[PROOFSTEP]
intro n n0 y yS
[GOAL]
x y✝ : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ S
⊢ y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
[PROOFSTEP]
have := (Int.sub_one_lt_floor _).trans_le (Int.cast_le.2 <| (hf n).2 _ ⟨y, yS, Int.floor_le _⟩)
[GOAL]
x y✝ : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this✝ : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ S
this : y * ↑n - 1 < ↑(f n)
⊢ y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
[PROOFSTEP]
simp only [Rat.cast_div, Rat.cast_coe_int, Rat.cast_coe_nat, gt_iff_lt]
[GOAL]
x y✝ : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this✝ : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ S
this : y * ↑n - 1 < ↑(f n)
⊢ y - (↑n)⁻¹ < ↑(f n) / ↑n
[PROOFSTEP]
rwa [lt_div_iff (Nat.cast_pos.2 n0 : (_ : ℝ) < _), sub_mul, _root_.inv_mul_cancel]
[GOAL]
x y✝ : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this✝ : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ S
this : y * ↑n - 1 < ↑(f n)
⊢ ↑n ≠ 0
[PROOFSTEP]
exact ne_of_gt (Nat.cast_pos.2 n0)
[GOAL]
case intro.intro
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
⊢ ∃ x, IsLUB S x
[PROOFSTEP]
have hg : IsCauSeq abs (fun n => f n / n : ℕ → ℚ) := by
  intro ε ε0
  suffices ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, (f j / j - f k / k : ℚ) < ε
    by
    refine' ⟨_, fun j ij => abs_lt.2 ⟨_, this _ ij _ le_rfl⟩⟩
    rw [neg_lt, neg_sub]
    exact this _ le_rfl _ ij
  intro j ij k ik
  replace ij := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ij)
  replace ik := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ik)
  have j0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ij)
  have k0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ik)
  rcases hf₁ _ j0 with ⟨y, yS, hy⟩
  refine' lt_of_lt_of_le ((@Rat.cast_lt ℝ _ _ _).1 _) ((inv_le ε0 (Nat.cast_pos.2 k0)).1 ik)
  simpa using sub_lt_iff_lt_add'.2 (lt_of_le_of_lt hy <| sub_lt_iff_lt_add.1 <| hf₂ _ k0 _ yS)
[GOAL]
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
⊢ IsCauSeq abs fun n => ↑(f n) / ↑n
[PROOFSTEP]
intro ε ε0
[GOAL]
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → |(fun n => ↑(f n) / ↑n) j - (fun n => ↑(f n) / ↑n) i| < ε
[PROOFSTEP]
suffices ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, (f j / j - f k / k : ℚ) < ε
  by
  refine' ⟨_, fun j ij => abs_lt.2 ⟨_, this _ ij _ le_rfl⟩⟩
  rw [neg_lt, neg_sub]
  exact this _ le_rfl _ ij
[GOAL]
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this✝ : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
this : ∀ (j : ℕ), j ≥ ⌈ε⁻¹⌉₊ → ∀ (k : ℕ), k ≥ ⌈ε⁻¹⌉₊ → ↑(f j) / ↑j - ↑(f k) / ↑k < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → |(fun n => ↑(f n) / ↑n) j - (fun n => ↑(f n) / ↑n) i| < ε
[PROOFSTEP]
refine' ⟨_, fun j ij => abs_lt.2 ⟨_, this _ ij _ le_rfl⟩⟩
[GOAL]
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this✝ : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
this : ∀ (j : ℕ), j ≥ ⌈ε⁻¹⌉₊ → ∀ (k : ℕ), k ≥ ⌈ε⁻¹⌉₊ → ↑(f j) / ↑j - ↑(f k) / ↑k < ε
j : ℕ
ij : j ≥ ⌈ε⁻¹⌉₊
⊢ -ε < (fun n => ↑(f n) / ↑n) j - (fun n => ↑(f n) / ↑n) ⌈ε⁻¹⌉₊
[PROOFSTEP]
rw [neg_lt, neg_sub]
[GOAL]
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this✝ : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
this : ∀ (j : ℕ), j ≥ ⌈ε⁻¹⌉₊ → ∀ (k : ℕ), k ≥ ⌈ε⁻¹⌉₊ → ↑(f j) / ↑j - ↑(f k) / ↑k < ε
j : ℕ
ij : j ≥ ⌈ε⁻¹⌉₊
⊢ (fun n => ↑(f n) / ↑n) ⌈ε⁻¹⌉₊ - (fun n => ↑(f n) / ↑n) j < ε
[PROOFSTEP]
exact this _ le_rfl _ ij
[GOAL]
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
⊢ ∀ (j : ℕ), j ≥ ⌈ε⁻¹⌉₊ → ∀ (k : ℕ), k ≥ ⌈ε⁻¹⌉₊ → ↑(f j) / ↑j - ↑(f k) / ↑k < ε
[PROOFSTEP]
intro j ij k ik
[GOAL]
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j : ℕ
ij : j ≥ ⌈ε⁻¹⌉₊
k : ℕ
ik : k ≥ ⌈ε⁻¹⌉₊
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε
[PROOFSTEP]
replace ij := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ij)
[GOAL]
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ik : k ≥ ⌈ε⁻¹⌉₊
ij : ε⁻¹ ≤ ↑j
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε
[PROOFSTEP]
replace ik := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ik)
[GOAL]
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε
[PROOFSTEP]
have j0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ij)
[GOAL]
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
j0 : 0 < j
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε
[PROOFSTEP]
have k0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ik)
[GOAL]
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
j0 : 0 < j
k0 : 0 < k
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε
[PROOFSTEP]
rcases hf₁ _ j0 with ⟨y, yS, hy⟩
[GOAL]
case intro.intro
x y✝ : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
j0 : 0 < j
k0 : 0 < k
y : ℝ
yS : y ∈ S
hy : ↑(↑(f j) / ↑j) ≤ y
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε
[PROOFSTEP]
refine' lt_of_lt_of_le ((@Rat.cast_lt ℝ _ _ _).1 _) ((inv_le ε0 (Nat.cast_pos.2 k0)).1 ik)
[GOAL]
case intro.intro
x y✝ : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
j0 : 0 < j
k0 : 0 < k
y : ℝ
yS : y ∈ S
hy : ↑(↑(f j) / ↑j) ≤ y
⊢ ↑(↑(f j) / ↑j - ↑(f k) / ↑k) < ↑(↑k)⁻¹
[PROOFSTEP]
simpa using sub_lt_iff_lt_add'.2 (lt_of_le_of_lt hy <| sub_lt_iff_lt_add.1 <| hf₂ _ k0 _ yS)
[GOAL]
case intro.intro
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
⊢ ∃ x, IsLUB S x
[PROOFSTEP]
let g : CauSeq ℚ abs := ⟨fun n => f n / n, hg⟩
[GOAL]
case intro.intro
x y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := { val := fun n => ↑(f n) / ↑n, property := hg }
⊢ ∃ x, IsLUB S x
[PROOFSTEP]
refine' ⟨mk g, ⟨fun x xS => _, fun y h => _⟩⟩
[GOAL]
case intro.intro.refine'_1
x✝ y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := { val := fun n => ↑(f n) / ↑n, property := hg }
x : ℝ
xS : x ∈ S
⊢ x ≤ mk g
[PROOFSTEP]
refine' le_of_forall_ge_of_dense fun z xz => _
[GOAL]
case intro.intro.refine'_1
x✝ y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := { val := fun n => ↑(f n) / ↑n, property := hg }
x : ℝ
xS : x ∈ S
z : ℝ
xz : z < x
⊢ z ≤ mk g
[PROOFSTEP]
cases' exists_nat_gt (x - z)⁻¹ with K hK
[GOAL]
case intro.intro.refine'_1.intro
x✝ y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := { val := fun n => ↑(f n) / ↑n, property := hg }
x : ℝ
xS : x ∈ S
z : ℝ
xz : z < x
K : ℕ
hK : (x - z)⁻¹ < ↑K
⊢ z ≤ mk g
[PROOFSTEP]
refine' le_mk_of_forall_le ⟨K, fun n nK => _⟩
[GOAL]
case intro.intro.refine'_1.intro
x✝ y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := { val := fun n => ↑(f n) / ↑n, property := hg }
x : ℝ
xS : x ∈ S
z : ℝ
xz : z < x
K : ℕ
hK : (x - z)⁻¹ < ↑K
n : ℕ
nK : n ≥ K
⊢ z ≤ ↑(↑g n)
[PROOFSTEP]
replace xz := sub_pos.2 xz
[GOAL]
case intro.intro.refine'_1.intro
x✝ y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := { val := fun n => ↑(f n) / ↑n, property := hg }
x : ℝ
xS : x ∈ S
z : ℝ
K : ℕ
hK : (x - z)⁻¹ < ↑K
n : ℕ
nK : n ≥ K
xz : 0 < x - z
⊢ z ≤ ↑(↑g n)
[PROOFSTEP]
replace hK := hK.le.trans (Nat.cast_le.2 nK)
[GOAL]
case intro.intro.refine'_1.intro
x✝ y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := { val := fun n => ↑(f n) / ↑n, property := hg }
x : ℝ
xS : x ∈ S
z : ℝ
K n : ℕ
nK : n ≥ K
xz : 0 < x - z
hK : (x - z)⁻¹ ≤ ↑n
⊢ z ≤ ↑(↑g n)
[PROOFSTEP]
have n0 : 0 < n := Nat.cast_pos.1 ((inv_pos.2 xz).trans_le hK)
[GOAL]
case intro.intro.refine'_1.intro
x✝ y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := { val := fun n => ↑(f n) / ↑n, property := hg }
x : ℝ
xS : x ∈ S
z : ℝ
K n : ℕ
nK : n ≥ K
xz : 0 < x - z
hK : (x - z)⁻¹ ≤ ↑n
n0 : 0 < n
⊢ z ≤ ↑(↑g n)
[PROOFSTEP]
refine' le_trans _ (hf₂ _ n0 _ xS).le
[GOAL]
case intro.intro.refine'_1.intro
x✝ y : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := { val := fun n => ↑(f n) / ↑n, property := hg }
x : ℝ
xS : x ∈ S
z : ℝ
K n : ℕ
nK : n ≥ K
xz : 0 < x - z
hK : (x - z)⁻¹ ≤ ↑n
n0 : 0 < n
⊢ z ≤ x - (↑n)⁻¹
[PROOFSTEP]
rwa [le_sub_comm, inv_le (Nat.cast_pos.2 n0 : (_ : ℝ) < _) xz]
[GOAL]
case intro.intro.refine'_2
x y✝ : ℝ
S : Set ℝ
L : ℝ
hL : L ∈ S
U : ℝ
hU : U ∈ upperBounds S
this : ∀ (d : ℕ), BddAbove {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} ∧ ∀ (z : ℤ), z ∈ {m | ∃ y, y ∈ S ∧ ↑m ≤ y * ↑d} → z ≤ f d
hf₁ : ∀ (n : ℕ), n > 0 → ∃ y, y ∈ S ∧ ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ (n : ℕ), n > 0 → ∀ (y : ℝ), y ∈ S → y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := { val := fun n => ↑(f n) / ↑n, property := hg }
y : ℝ
h : y ∈ upperBounds S
⊢ mk g ≤ y
[PROOFSTEP]
exact
  mk_le_of_forall_le
    ⟨1, fun n n1 =>
      let ⟨x, xS, hx⟩ := hf₁ _ n1
      le_trans hx (h xS)⟩
[GOAL]
x y : ℝ
S : Set ℝ
h₁ : Set.Nonempty S
h₂ : BddAbove S
⊢ IsLUB S (sSup S)
[PROOFSTEP]
simp only [sSup_def, dif_pos (And.intro h₁ h₂)]
[GOAL]
x y : ℝ
S : Set ℝ
h₁ : Set.Nonempty S
h₂ : BddAbove S
⊢ IsLUB S (choose (_ : ∃ x, IsLUB S x))
[PROOFSTEP]
apply Classical.choose_spec
[GOAL]
x y : ℝ
S : Set ℝ
h₁ : Set.Nonempty S
h₂ : BddBelow S
⊢ IsGLB S (sInf S)
[PROOFSTEP]
rw [sInf_def, ← isLUB_neg', neg_neg]
[GOAL]
x y : ℝ
S : Set ℝ
h₁ : Set.Nonempty S
h₂ : BddBelow S
⊢ IsLUB (-S) (sSup (-S))
[PROOFSTEP]
exact Real.isLUB_sSup _ h₁.neg h₂.neg
[GOAL]
x y : ℝ
src✝¹ : LinearOrder ℝ := linearOrder
src✝ : Lattice ℝ := lattice
s : Set ℝ
hs : ¬BddAbove s
⊢ sSup s = sSup Set.univ
[PROOFSTEP]
simp [hs, sSup_def]
[GOAL]
x y : ℝ
src✝¹ : LinearOrder ℝ := linearOrder
src✝ : Lattice ℝ := lattice
s : Set ℝ
hs : ¬BddBelow s
⊢ sInf s = sInf Set.univ
[PROOFSTEP]
simp [hs, sInf_def, sSup_def]
[GOAL]
x y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
⊢ sInf s ≤ a ↔ ∀ (ε : ℝ), 0 < ε → ∃ x, x ∈ s ∧ x < a + ε
[PROOFSTEP]
rw [le_iff_forall_pos_lt_add]
[GOAL]
x y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
⊢ (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) ↔ ∀ (ε : ℝ), 0 < ε → ∃ x, x ∈ s ∧ x < a + ε
[PROOFSTEP]
constructor
[GOAL]
case mp
x y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
⊢ (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) → ∀ (ε : ℝ), 0 < ε → ∃ x, x ∈ s ∧ x < a + ε
[PROOFSTEP]
intro H ε ε_pos
[GOAL]
case mpr
x y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
⊢ (∀ (ε : ℝ), 0 < ε → ∃ x, x ∈ s ∧ x < a + ε) → ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
[PROOFSTEP]
intro H ε ε_pos
[GOAL]
case mp
x y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ x, x ∈ s ∧ x < a + ε
[PROOFSTEP]
exact exists_lt_of_csInf_lt h' (H ε ε_pos)
[GOAL]
case mpr
x y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), 0 < ε → ∃ x, x ∈ s ∧ x < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ sInf s < a + ε
[PROOFSTEP]
rcases H ε ε_pos with ⟨x, x_in, hx⟩
[GOAL]
case mpr.intro.intro
x✝ y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), 0 < ε → ∃ x, x ∈ s ∧ x < a + ε
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : x < a + ε
⊢ sInf s < a + ε
[PROOFSTEP]
exact csInf_lt_of_lt h x_in hx
[GOAL]
x y : ℝ
s : Set ℝ
h : BddAbove s
h' : Set.Nonempty s
a : ℝ
⊢ a ≤ sSup s ↔ ∀ (ε : ℝ), ε < 0 → ∃ x, x ∈ s ∧ a + ε < x
[PROOFSTEP]
rw [le_iff_forall_pos_lt_add]
[GOAL]
x y : ℝ
s : Set ℝ
h : BddAbove s
h' : Set.Nonempty s
a : ℝ
⊢ (∀ (ε : ℝ), 0 < ε → a < sSup s + ε) ↔ ∀ (ε : ℝ), ε < 0 → ∃ x, x ∈ s ∧ a + ε < x
[PROOFSTEP]
refine' ⟨fun H ε ε_neg => _, fun H ε ε_pos => _⟩
[GOAL]
case refine'_1
x y : ℝ
s : Set ℝ
h : BddAbove s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), 0 < ε → a < sSup s + ε
ε : ℝ
ε_neg : ε < 0
⊢ ∃ x, x ∈ s ∧ a + ε < x
[PROOFSTEP]
exact exists_lt_of_lt_csSup h' (lt_sub_iff_add_lt.mp (H _ (neg_pos.mpr ε_neg)))
[GOAL]
case refine'_2
x y : ℝ
s : Set ℝ
h : BddAbove s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), ε < 0 → ∃ x, x ∈ s ∧ a + ε < x
ε : ℝ
ε_pos : 0 < ε
⊢ a < sSup s + ε
[PROOFSTEP]
rcases H _ (neg_lt_zero.mpr ε_pos) with ⟨x, x_in, hx⟩
[GOAL]
case refine'_2.intro.intro
x✝ y : ℝ
s : Set ℝ
h : BddAbove s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), ε < 0 → ∃ x, x ∈ s ∧ a + ε < x
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : a + -ε < x
⊢ a < sSup s + ε
[PROOFSTEP]
exact sub_lt_iff_lt_add.mp (lt_csSup_of_lt h x_in hx)
[GOAL]
x y : ℝ
⊢ ¬(Set.Nonempty ∅ ∧ BddAbove ∅)
[PROOFSTEP]
simp
[GOAL]
x y : ℝ
α : Sort u_1
inst✝ : IsEmpty α
f : α → ℝ
⊢ ⨆ (i : α), f i = 0
[PROOFSTEP]
dsimp [iSup]
[GOAL]
x y : ℝ
α : Sort u_1
inst✝ : IsEmpty α
f : α → ℝ
⊢ sSup (Set.range fun i => f i) = 0
[PROOFSTEP]
convert Real.sSup_empty
[GOAL]
case h.e'_2.h.e'_3
x y : ℝ
α : Sort u_1
inst✝ : IsEmpty α
f : α → ℝ
⊢ (Set.range fun i => f i) = ∅
[PROOFSTEP]
rw [Set.range_eq_empty_iff]
[GOAL]
case h.e'_2.h.e'_3
x y : ℝ
α : Sort u_1
inst✝ : IsEmpty α
f : α → ℝ
⊢ IsEmpty α
[PROOFSTEP]
infer_instance
[GOAL]
x y : ℝ
α : Sort u_1
⊢ ⨆ (x : α), 0 = 0
[PROOFSTEP]
cases isEmpty_or_nonempty α
[GOAL]
case inl
x y : ℝ
α : Sort u_1
h✝ : IsEmpty α
⊢ ⨆ (x : α), 0 = 0
[PROOFSTEP]
exact Real.ciSup_empty _
[GOAL]
case inr
x y : ℝ
α : Sort u_1
h✝ : Nonempty α
⊢ ⨆ (x : α), 0 = 0
[PROOFSTEP]
exact ciSup_const
[GOAL]
x y : ℝ
⊢ sInf ∅ = 0
[PROOFSTEP]
simp [sInf_def, sSup_empty]
[GOAL]
x y : ℝ
α : Sort u_1
inst✝ : IsEmpty α
f : α → ℝ
⊢ ⨅ (i : α), f i = 0
[PROOFSTEP]
rw [iInf_of_empty', sInf_empty]
[GOAL]
x y : ℝ
α : Sort u_1
⊢ ⨅ (x : α), 0 = 0
[PROOFSTEP]
cases isEmpty_or_nonempty α
[GOAL]
case inl
x y : ℝ
α : Sort u_1
h✝ : IsEmpty α
⊢ ⨅ (x : α), 0 = 0
[PROOFSTEP]
exact Real.ciInf_empty _
[GOAL]
case inr
x y : ℝ
α : Sort u_1
h✝ : Nonempty α
⊢ ⨅ (x : α), 0 = 0
[PROOFSTEP]
exact ciInf_const
[GOAL]
x y : ℝ
S : Set ℝ
hS : ∀ (x : ℝ), x ∈ S → 0 ≤ x
⊢ 0 ≤ sSup S
[PROOFSTEP]
rcases S.eq_empty_or_nonempty with (rfl | ⟨y, hy⟩)
[GOAL]
case inl
x y : ℝ
hS : ∀ (x : ℝ), x ∈ ∅ → 0 ≤ x
⊢ 0 ≤ sSup ∅
[PROOFSTEP]
exact sSup_empty.ge
[GOAL]
case inr.intro
x y✝ : ℝ
S : Set ℝ
hS : ∀ (x : ℝ), x ∈ S → 0 ≤ x
y : ℝ
hy : y ∈ S
⊢ 0 ≤ sSup S
[PROOFSTEP]
apply dite _ (fun h => le_csSup_of_le h hy <| hS y hy) fun h => (sSup_of_not_bddAbove h).ge
[GOAL]
x y : ℝ
S : Set ℝ
a : ℝ
hS : ∀ (x : ℝ), x ∈ S → x ≤ a
ha : 0 ≤ a
⊢ sSup S ≤ a
[PROOFSTEP]
rcases S.eq_empty_or_nonempty with (rfl | hS₂)
[GOAL]
case inl
x y a : ℝ
ha : 0 ≤ a
hS : ∀ (x : ℝ), x ∈ ∅ → x ≤ a
⊢ sSup ∅ ≤ a
case inr x y : ℝ S : Set ℝ a : ℝ hS : ∀ (x : ℝ), x ∈ S → x ≤ a ha : 0 ≤ a hS₂ : Set.Nonempty S ⊢ sSup S ≤ a
[PROOFSTEP]
exacts [sSup_empty.trans_le ha, csSup_le hS₂ hS]
[GOAL]
x y : ℝ
S : Set ℝ
hS : ∀ (x : ℝ), x ∈ S → 0 ≤ x
⊢ 0 ≤ sInf S
[PROOFSTEP]
rcases S.eq_empty_or_nonempty with (rfl | hS₂)
[GOAL]
case inl
x y : ℝ
hS : ∀ (x : ℝ), x ∈ ∅ → 0 ≤ x
⊢ 0 ≤ sInf ∅
case inr x y : ℝ S : Set ℝ hS : ∀ (x : ℝ), x ∈ S → 0 ≤ x hS₂ : Set.Nonempty S ⊢ 0 ≤ sInf S
[PROOFSTEP]
exacts [sInf_empty.ge, le_csInf hS₂ hS]
[GOAL]
x y : ℝ
S : Set ℝ
hS : ∀ (x : ℝ), x ∈ S → x ≤ 0
⊢ sInf S ≤ 0
[PROOFSTEP]
rcases S.eq_empty_or_nonempty with (rfl | ⟨y, hy⟩)
[GOAL]
case inl
x y : ℝ
hS : ∀ (x : ℝ), x ∈ ∅ → x ≤ 0
⊢ sInf ∅ ≤ 0
[PROOFSTEP]
exact sInf_empty.le
[GOAL]
case inr.intro
x y✝ : ℝ
S : Set ℝ
hS : ∀ (x : ℝ), x ∈ S → x ≤ 0
y : ℝ
hy : y ∈ S
⊢ sInf S ≤ 0
[PROOFSTEP]
apply dite _ (fun h => csInf_le_of_le h hy <| hS y hy) fun h => (sInf_of_not_bddBelow h).le
[GOAL]
x y : ℝ
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
⊢ sInf s ≤ sSup s
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hne)
[GOAL]
case inl
x y : ℝ
h₁ : BddBelow ∅
h₂ : BddAbove ∅
⊢ sInf ∅ ≤ sSup ∅
[PROOFSTEP]
rw [sInf_empty, sSup_empty]
[GOAL]
case inr
x y : ℝ
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
hne : Set.Nonempty s
⊢ sInf s ≤ sSup s
[PROOFSTEP]
exact csInf_le_csSup h₁ h₂ hne
[GOAL]
x y : ℝ
f : CauSeq ℝ abs
⊢ ∃ x, f ≈ const abs x
[PROOFSTEP]
let S := {x : ℝ | const abs x < f}
[GOAL]
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
⊢ ∃ x, f ≈ const abs x
[PROOFSTEP]
have lb : ∃ x, x ∈ S := exists_lt f
[GOAL]
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
⊢ ∃ x, f ≈ const abs x
[PROOFSTEP]
have ub' : ∀ x, f < const abs x → ∀ y ∈ S, y ≤ x := fun x h y yS => le_of_lt <| const_lt.1 <| CauSeq.lt_trans yS h
[GOAL]
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
⊢ ∃ x, f ≈ const abs x
[PROOFSTEP]
have ub : ∃ x, ∀ y ∈ S, y ≤ x := (exists_gt f).imp ub'
[GOAL]
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
⊢ ∃ x, f ≈ const abs x
[PROOFSTEP]
refine' ⟨sSup S, ((lt_total _ _).resolve_left fun h => _).resolve_right fun h => _⟩
[GOAL]
case refine'_1
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
h : f < const abs (sSup S)
⊢ False
[PROOFSTEP]
rcases h with ⟨ε, ε0, i, ih⟩
[GOAL]
case refine'_1.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(const abs (sSup S) - f) j
⊢ False
[PROOFSTEP]
refine' (csSup_le lb (ub' _ _)).not_lt (sub_lt_self _ (half_pos ε0))
[GOAL]
case refine'_1.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(const abs (sSup S) - f) j
⊢ f < const abs (sSup S - ε / 2)
[PROOFSTEP]
refine' ⟨_, half_pos ε0, i, fun j ij => _⟩
[GOAL]
case refine'_1.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(const abs (sSup S) - f) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ ↑(const abs (sSup S - ε / 2) - f) j
[PROOFSTEP]
rw [sub_apply, const_apply, sub_right_comm, le_sub_iff_add_le, add_halves]
[GOAL]
case refine'_1.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(const abs (sSup S) - f) j
j : ℕ
ij : j ≥ i
⊢ ε ≤ sSup S - ↑f j
[PROOFSTEP]
exact ih _ ij
[GOAL]
case refine'_2
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
h : const abs (sSup S) < f
⊢ False
[PROOFSTEP]
rcases h with ⟨ε, ε0, i, ih⟩
[GOAL]
case refine'_2.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(f - const abs (sSup S)) j
⊢ False
[PROOFSTEP]
refine' (le_csSup ub _).not_lt ((lt_add_iff_pos_left _).2 (half_pos ε0))
[GOAL]
case refine'_2.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(f - const abs (sSup S)) j
⊢ ε / 2 + sSup S ∈ S
[PROOFSTEP]
refine' ⟨_, half_pos ε0, i, fun j ij => _⟩
[GOAL]
case refine'_2.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(f - const abs (sSup S)) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ ↑(f - const abs (ε / 2 + sSup S)) j
[PROOFSTEP]
rw [sub_apply, const_apply, add_comm, ← sub_sub, le_sub_iff_add_le, add_halves]
[GOAL]
case refine'_2.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(f - const abs (sSup S)) j
j : ℕ
ij : j ≥ i
⊢ ε ≤ ↑f j - sSup S
[PROOFSTEP]
exact ih _ ij
[GOAL]
x✝ y : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ (r : ↑(Ioi x)), f ↑r = ⨅ (q : { q' // x < ↑q' }), f ↑↑q
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
x✝ y : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ (r : ↑(Ioi x)), f ↑r ≤ ⨅ (q : { q' // x < ↑q' }), f ↑↑q
[PROOFSTEP]
have : Nonempty { r' : ℚ // x < ↑r' } := by
  obtain ⟨r, hrx⟩ := exists_rat_gt x
  exact ⟨⟨r, hrx⟩⟩
[GOAL]
x✝ y : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ Nonempty { r' // x < ↑r' }
[PROOFSTEP]
obtain ⟨r, hrx⟩ := exists_rat_gt x
[GOAL]
case intro
x✝ y : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
r : ℚ
hrx : x < ↑r
⊢ Nonempty { r' // x < ↑r' }
[PROOFSTEP]
exact ⟨⟨r, hrx⟩⟩
[GOAL]
case refine'_1
x✝ y : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' // x < ↑r' }
⊢ ⨅ (r : ↑(Ioi x)), f ↑r ≤ ⨅ (q : { q' // x < ↑q' }), f ↑↑q
[PROOFSTEP]
refine' le_ciInf fun r => _
[GOAL]
case refine'_1
x✝ y : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' // x < ↑r' }
r : { q' // x < ↑q' }
⊢ ⨅ (r : ↑(Ioi x)), f ↑r ≤ f ↑↑r
[PROOFSTEP]
obtain ⟨y, hxy, hyr⟩ := exists_rat_btwn r.prop
[GOAL]
case refine'_1.intro.intro
x✝ y✝ : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' // x < ↑r' }
r : { q' // x < ↑q' }
y : ℚ
hxy : x < ↑y
hyr : ↑y < ↑↑r
⊢ ⨅ (r : ↑(Ioi x)), f ↑r ≤ f ↑↑r
[PROOFSTEP]
refine' ciInf_set_le hf (hxy.trans _)
[GOAL]
case refine'_1.intro.intro
x✝ y✝ : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' // x < ↑r' }
r : { q' // x < ↑q' }
y : ℚ
hxy : x < ↑y
hyr : ↑y < ↑↑r
⊢ ↑y < ↑↑r
[PROOFSTEP]
exact_mod_cast hyr
[GOAL]
case refine'_2
x✝ y : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ (q : { q' // x < ↑q' }), f ↑↑q ≤ ⨅ (r : ↑(Ioi x)), f ↑r
[PROOFSTEP]
refine' le_ciInf fun q => _
[GOAL]
case refine'_2
x✝ y : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
⊢ ⨅ (q : { q' // x < ↑q' }), f ↑↑q ≤ f ↑q
[PROOFSTEP]
have hq := q.prop
[GOAL]
case refine'_2
x✝ y : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : ↑q ∈ Ioi x
⊢ ⨅ (q : { q' // x < ↑q' }), f ↑↑q ≤ f ↑q
[PROOFSTEP]
rw [mem_Ioi] at hq
[GOAL]
case refine'_2
x✝ y : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
⊢ ⨅ (q : { q' // x < ↑q' }), f ↑↑q ≤ f ↑q
[PROOFSTEP]
obtain ⟨y, hxy, hyq⟩ := exists_rat_btwn hq
[GOAL]
case refine'_2.intro.intro
x✝ y✝ : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ ⨅ (q : { q' // x < ↑q' }), f ↑↑q ≤ f ↑q
[PROOFSTEP]
refine' (ciInf_le _ _).trans _
[GOAL]
case refine'_2.intro.intro.refine'_1
x✝ y✝ : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ BddBelow (range fun q => f ↑↑q)
[PROOFSTEP]
refine' ⟨hf.some, fun z => _⟩
[GOAL]
case refine'_2.intro.intro.refine'_1
x✝ y✝ : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
z : ℝ
⊢ (z ∈ range fun q => f ↑↑q) → Set.Nonempty.some hf ≤ z
[PROOFSTEP]
rintro ⟨u, rfl⟩
[GOAL]
case refine'_2.intro.intro.refine'_1.intro
x✝ y✝ : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
u : { q' // x < ↑q' }
⊢ Set.Nonempty.some hf ≤ (fun q => f ↑↑q) u
[PROOFSTEP]
suffices hfu : f u ∈ f '' Ioi x
[GOAL]
case refine'_2.intro.intro.refine'_1.intro
x✝ y✝ : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
u : { q' // x < ↑q' }
hfu : f ↑↑u ∈ f '' Ioi x
⊢ Set.Nonempty.some hf ≤ (fun q => f ↑↑q) u
case hfu
x✝ y✝ : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
u : { q' // x < ↑q' }
⊢ f ↑↑u ∈ f '' Ioi x
[PROOFSTEP]
exact hf.choose_spec hfu
[GOAL]
case hfu
x✝ y✝ : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
u : { q' // x < ↑q' }
⊢ f ↑↑u ∈ f '' Ioi x
[PROOFSTEP]
exact ⟨u, u.prop, rfl⟩
[GOAL]
case refine'_2.intro.intro.refine'_2
x✝ y✝ : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ { q' // x < ↑q' }
[PROOFSTEP]
exact ⟨y, hxy⟩
[GOAL]
case refine'_2.intro.intro.refine'_3
x✝ y✝ : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ f ↑↑{ val := y, property := hxy } ≤ f ↑q
[PROOFSTEP]
refine' hf_mono (le_trans _ hyq.le)
[GOAL]
case refine'_2.intro.intro.refine'_3
x✝ y✝ : ℝ
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ ↑↑{ val := y, property := hxy } ≤ ↑y
[PROOFSTEP]
norm_cast


[GOAL]
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ Forall P ↔ ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
[PROOFSTEP]
simp only [Forall, FinVec.forall_iff, forall_iff]
[GOAL]
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∀ (x : Fin n → α) (x_1 : Matrix (Fin (Nat.add m 0)) (Fin n) α), P (↑of (vecCons x x_1))) ↔
    ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
[PROOFSTEP]
exact Iff.symm Fin.forall_fin_succ_pi
[GOAL]
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ Exists P ↔ ∃ x, P x
[PROOFSTEP]
simp only [Exists, FinVec.exists_iff, exists_iff]
[GOAL]
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∃ x x_1, P (↑of (vecCons x x_1))) ↔ ∃ x, P x
[PROOFSTEP]
exact Iff.symm Fin.exists_fin_succ_pi
[GOAL]
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ transposeᵣ A i j = Aᵀ i j
[PROOFSTEP]
simp_rw [transposeᵣ, transposeᵣ_eq]
[GOAL]
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ ↑of (vecCons (FinVec.map (fun v => v 0) A) (submatrix A id Fin.succ)ᵀ) i j = Aᵀ i j
[PROOFSTEP]
refine' i.cases _ fun i => _
[GOAL]
case refine'_1
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ ↑of (vecCons (FinVec.map (fun v => v 0) A) (submatrix A id Fin.succ)ᵀ) 0 j = Aᵀ 0 j
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ FinVec.map (fun v => v 0) A j = A j 0
[PROOFSTEP]
rw [FinVec.map_eq, Function.comp_apply]
[GOAL]
case refine'_2
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i✝ : Fin (n + 1)
j : Fin m
i : Fin n
⊢ ↑of (vecCons (FinVec.map (fun v => v 0) A) (submatrix A id Fin.succ)ᵀ) (Fin.succ i) j = Aᵀ (Fin.succ i) j
[PROOFSTEP]
simp only [of_apply, Matrix.cons_val_succ]
[GOAL]
case refine'_2
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i✝ : Fin (n + 1)
j : Fin m
i : Fin n
⊢ (submatrix A id Fin.succ)ᵀ i j = Aᵀ (Fin.succ i) j
[PROOFSTEP]
rfl
[GOAL]
l m✝ n : ℕ
α : Type u_1
β : Type u_2
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
m : ℕ
a b : Fin m → α
⊢ dotProductᵣ a b = a ⬝ᵥ b
[PROOFSTEP]
simp_rw [dotProductᵣ, dotProduct, FinVec.sum_eq, FinVec.seq_eq, FinVec.map_eq, Function.comp_apply]
[GOAL]
l m n : ℕ
α : Type u_1
β : Type u_2
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
A : Matrix (Fin l) (Fin m) α
B : Matrix (Fin m) (Fin n) α
⊢ mulᵣ A B = A * B
[PROOFSTEP]
simp [mulᵣ, Function.comp, Matrix.transpose]
[GOAL]
l m n : ℕ
α : Type u_1
β : Type u_2
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
A : Matrix (Fin l) (Fin m) α
B : Matrix (Fin m) (Fin n) α
⊢ (↑of fun x x_1 => A x ⬝ᵥ ↑of (fun x y => B y x) x_1) = A * B
[PROOFSTEP]
rfl
[GOAL]
l m n : ℕ
α : Type u_1
β : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix (Fin l) (Fin m) α
v : Fin m → α
⊢ mulVecᵣ A v = mulVec A v
[PROOFSTEP]
simp [mulVecᵣ, Function.comp]
[GOAL]
l m n : ℕ
α : Type u_1
β : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix (Fin l) (Fin m) α
v : Fin m → α
⊢ (fun x => A x ⬝ᵥ v) = mulVec A v
[PROOFSTEP]
rfl
[GOAL]
l m n : ℕ
α : Type u_1
β : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
v : Fin l → α
A : Matrix (Fin l) (Fin m) α
⊢ vecMulᵣ v A = vecMul v A
[PROOFSTEP]
simp [vecMulᵣ, Function.comp]
[GOAL]
l m n : ℕ
α : Type u_1
β : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
v : Fin l → α
A : Matrix (Fin l) (Fin m) α
⊢ (fun x => v ⬝ᵥ Aᵀ x) = vecMul v A
[PROOFSTEP]
rfl
[GOAL]
l m✝ n✝ : ℕ
α : Type u_1
β : Type u_2
m n : ℕ
A : Matrix (Fin m) (Fin n) α
⊢ etaExpand A = A
[PROOFSTEP]
simp_rw [etaExpand, FinVec.etaExpand_eq, Matrix.of, Equiv.refl_apply]


[GOAL]
σ : Type u
R : Type v
inst✝² : CommSemiring R
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ max (lift #(σ →₀ ℕ)) (lift #R) = max (max (lift #R) (lift #σ)) ℵ₀
[PROOFSTEP]
rw [mk_finsupp_nat, max_assoc, lift_max, lift_aleph0, max_comm]
[GOAL]
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ #(MvPolynomial σ R) ≤ max (max (lift #R) (lift #σ)) ℵ₀
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝ : Subsingleton R
⊢ #(MvPolynomial σ R) ≤ max (max (lift #R) (lift #σ)) ℵ₀
[PROOFSTEP]
exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)
[GOAL]
case inr
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ #(MvPolynomial σ R) ≤ max (max (lift #R) (lift #σ)) ℵ₀
[PROOFSTEP]
cases isEmpty_or_nonempty σ
[GOAL]
case inr.inl
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝¹ : Nontrivial R
h✝ : IsEmpty σ
⊢ #(MvPolynomial σ R) ≤ max (max (lift #R) (lift #σ)) ℵ₀
[PROOFSTEP]
exact cardinal_mk_eq_lift.trans_le (le_max_of_le_left <| le_max_left _ _)
[GOAL]
case inr.inr
σ✝ : Type u
R✝ : Type v
inst✝¹ : CommSemiring R✝
σ : Type u
R : Type v
inst✝ : CommSemiring R
h✝¹ : Nontrivial R
h✝ : Nonempty σ
⊢ #(MvPolynomial σ R) ≤ max (max (lift #R) (lift #σ)) ℵ₀
[PROOFSTEP]
exact cardinal_mk_eq_max_lift.le
[GOAL]
σ R : Type u
inst✝² : CommSemiring R
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ #(MvPolynomial σ R) = max (max #R #σ) ℵ₀
[PROOFSTEP]
simp
[GOAL]
σ R : Type u
inst✝ : CommSemiring R
⊢ max (max (lift #R) (lift #σ)) ℵ₀ ≤ max (max #R #σ) ℵ₀
[PROOFSTEP]
rw [lift_id, lift_id]


[GOAL]
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ Polynomial.eval x (eval₂ f g p) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) p
[PROOFSTEP]
apply induction_on p
[GOAL]
case h_C
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (a : R),
    Polynomial.eval x (eval₂ f g (↑C a)) =
      eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (↑C a)
[PROOFSTEP]
simp
[GOAL]
case h_add
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    Polynomial.eval x (eval₂ f g p) =
        eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g q) =
          eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) q →
        Polynomial.eval x (eval₂ f g (p + q)) =
          eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (p + q)
[PROOFSTEP]
intro p q hp hq
[GOAL]
case h_add
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p✝ p q : MvPolynomial σ R
hp :
  Polynomial.eval x (eval₂ f g p) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) p
hq :
  Polynomial.eval x (eval₂ f g q) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) q
⊢ Polynomial.eval x (eval₂ f g (p + q)) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (p + q)
[PROOFSTEP]
simp [hp, hq]
[GOAL]
case h_X
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    Polynomial.eval x (eval₂ f g p) =
        eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g (p * X n)) =
        eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (p * X n)
[PROOFSTEP]
intro p n hp
[GOAL]
case h_X
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p✝ p : MvPolynomial σ R
n : σ
hp :
  Polynomial.eval x (eval₂ f g p) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) p
⊢ Polynomial.eval x (eval₂ f g (p * X n)) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (p * X n)
[PROOFSTEP]
simp [hp]
[GOAL]
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ ↑(eval x) (Polynomial.eval q (↑(finSuccEquiv R n) f)) = ↑(eval fun i => Fin.cases (↑(eval x) q) x i) f
[PROOFSTEP]
simp only [finSuccEquiv_apply, coe_eval₂Hom, polynomial_eval_eval₂, eval_eval₂]
[GOAL]
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ eval₂ (RingHom.comp (eval x) (RingHom.comp (Polynomial.evalRingHom q) (RingHom.comp Polynomial.C C)))
      (fun s => ↑(eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) s))) f =
    ↑(eval fun i => Fin.cases (↑(eval x) q) x i) f
[PROOFSTEP]
conv in RingHom.comp _ _ => {
  refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
  simp}
[GOAL]
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
| RingHom.comp (eval x) (RingHom.comp (Polynomial.evalRingHom q) (RingHom.comp Polynomial.C C))
[PROOFSTEP]
{ refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
  simp}
[GOAL]
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
| RingHom.comp (eval x) (RingHom.comp (Polynomial.evalRingHom q) (RingHom.comp Polynomial.C C))
[PROOFSTEP]
{ refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
  simp}
[GOAL]
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
| RingHom.comp (eval x) (RingHom.comp (Polynomial.evalRingHom q) (RingHom.comp Polynomial.C C))
[PROOFSTEP]
refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
[GOAL]
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
r : R
⊢ ↑(RingHom.comp (eval x) (RingHom.comp (Polynomial.evalRingHom q) (RingHom.comp Polynomial.C C))) r = ↑(RingHom.id R) r
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ eval₂ (RingHom.id R)
      (fun s => ↑(eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) s))) f =
    ↑(eval fun i => Fin.cases (↑(eval x) q) x i) f
[PROOFSTEP]
simp only [eval₂_id]
[GOAL]
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ ↑(eval fun s => ↑(eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) s))) f =
    ↑(eval fun i => Fin.cases (↑(eval x) q) x i) f
[PROOFSTEP]
congr
[GOAL]
case e_a.e_f
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ (fun s => ↑(eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) s))) = fun i =>
    Fin.cases (↑(eval x) q) x i
[PROOFSTEP]
funext i
[GOAL]
case e_a.e_f.h
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
i : Fin (n + 1)
⊢ ↑(eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) i)) = Fin.cases (↑(eval x) q) x i
[PROOFSTEP]
refine Fin.cases (by simp) (by simp) i
[GOAL]
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
i : Fin (n + 1)
⊢ ↑(eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) 0)) = Fin.cases (↑(eval x) q) x 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
i : Fin (n + 1)
⊢ ∀ (i : Fin n),
    ↑(eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) (Fin.succ i))) =
      Fin.cases (↑(eval x) q) x (Fin.succ i)
[PROOFSTEP]
simp