[GOAL]
x : ℝ
⊢ Irrational x ↔ ∀ (a b : ℤ), x ≠ ↑a / ↑b
[PROOFSTEP]
simp only [Irrational, Rat.forall, cast_mk, not_exists, Set.mem_range, cast_coe_int, cast_div, eq_comm]
[GOAL]
r : ℝ
tr : Transcendental ℚ r
⊢ Irrational r
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro
a : ℚ
tr : Transcendental ℚ ↑a
⊢ False
[PROOFSTEP]
exact tr (isAlgebraic_algebraMap a)
[GOAL]
x : ℝ
n : ℕ
m : ℤ
hxr : x ^ n = ↑m
hv : ¬∃ y, x = ↑y
hnpos : 0 < n
⊢ Irrational x
[PROOFSTEP]
rintro ⟨⟨N, D, P, C⟩, rfl⟩
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D) ^ n = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ False
[PROOFSTEP]
rw [← cast_pow] at hxr
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ False
[PROOFSTEP]
have c1 : ((D : ℤ) : ℝ) ≠ 0 := by
  rw [Int.cast_ne_zero, Int.coe_nat_ne_zero]
  exact P
[GOAL]
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ ↑↑D ≠ 0
[PROOFSTEP]
rw [Int.cast_ne_zero, Int.coe_nat_ne_zero]
[GOAL]
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
⊢ D ≠ 0
[PROOFSTEP]
exact P
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
⊢ False
[PROOFSTEP]
have c2 : ((D : ℤ) : ℝ) ^ n ≠ 0 := pow_ne_zero _ c1
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : ↑(mk' N D ^ n) = ↑m
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False
[PROOFSTEP]
rw [num_den', cast_pow, cast_mk, div_pow, div_eq_iff_mul_eq c2, ← Int.cast_pow, ← Int.cast_pow, ← Int.cast_mul,
  Int.cast_inj] at hxr
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False
[PROOFSTEP]
have hdivn : (D : ℤ) ^ n ∣ N ^ n := Dvd.intro_left m hxr
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : ↑D ^ n ∣ N ^ n
⊢ False
[PROOFSTEP]
rw [← Int.dvd_natAbs, ← Int.coe_nat_pow, Int.coe_nat_dvd, Int.natAbs_pow, Nat.pow_dvd_pow_iff hnpos] at hdivn
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : D ∣ Int.natAbs N
⊢ False
[PROOFSTEP]
obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
[GOAL]
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : Nat.coprime (Int.natAbs N) D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N D) = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : D ∣ Int.natAbs N
⊢ D = 1
[PROOFSTEP]
rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : 1 ≠ 0
C : Nat.coprime (Int.natAbs N) 1
hxr : m * ↑1 ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N 1) = ↑y
c1 : ↑↑1 ≠ 0
c2 : ↑↑1 ^ n ≠ 0
hdivn : 1 ∣ Int.natAbs N
⊢ False
[PROOFSTEP]
refine' hv ⟨N, _⟩
[GOAL]
case intro.mk'
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : 1 ≠ 0
C : Nat.coprime (Int.natAbs N) 1
hxr : m * ↑1 ^ n = N ^ n
hv : ¬∃ y, ↑(mk' N 1) = ↑y
c1 : ↑↑1 ≠ 0
c2 : ↑↑1 ^ n ≠ 0
hdivn : 1 ∣ Int.natAbs N
⊢ ↑(mk' N 1) = ↑N
[PROOFSTEP]
rw [num_den', Int.ofNat_one, divInt_one, cast_coe_int]
[GOAL]
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
⊢ Irrational x
[PROOFSTEP]
rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
[GOAL]
case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ 0 = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 0 ≠ 0
⊢ Irrational x
[PROOFSTEP]
rw [eq_comm, pow_zero, ← Int.cast_one, Int.cast_inj] at hxr
[GOAL]
case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : m = 1
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 0 ≠ 0
⊢ Irrational x
[PROOFSTEP]
simp [hxr, multiplicity.one_right (mt isUnit_iff_dvd_one.1 (mt Int.coe_nat_dvd.1 hp.1.not_dvd_one)), Nat.zero_mod] at hv
[GOAL]
case inr
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
⊢ Irrational x
[PROOFSTEP]
refine' irrational_nrt_of_notint_nrt _ _ hxr _ hnpos
[GOAL]
case inr
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
⊢ ¬∃ y, x = ↑y
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case inr.intro
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : ↑y ^ n = ↑m
⊢ False
[PROOFSTEP]
rw [← Int.cast_pow, Int.cast_inj] at hxr
[GOAL]
case inr.intro
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : y ^ n = m
⊢ False
[PROOFSTEP]
subst m
[GOAL]
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (y ^ n)) (_ : multiplicity.Finite (↑p) (y ^ n)) % n ≠ 0
⊢ False
[PROOFSTEP]
have : y ≠ 0 := by
  rintro rfl
  rw [zero_pow hnpos] at hm
  exact hm rfl
[GOAL]
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (y ^ n)) (_ : multiplicity.Finite (↑p) (y ^ n)) % n ≠ 0
⊢ y ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm : 0 ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (0 ^ n)) (_ : multiplicity.Finite (↑p) (0 ^ n)) % n ≠ 0
⊢ False
[PROOFSTEP]
rw [zero_pow hnpos] at hm
[GOAL]
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
hm✝ : 0 ^ n ≠ 0
hm : 0 ≠ 0
hv : Part.get (multiplicity (↑p) (0 ^ n)) (_ : multiplicity.Finite (↑p) (0 ^ n)) % n ≠ 0
⊢ False
[PROOFSTEP]
exact hm rfl
[GOAL]
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : Part.get (multiplicity (↑p) (y ^ n)) (_ : multiplicity.Finite (↑p) (y ^ n)) % n ≠ 0
this : y ≠ 0
⊢ False
[PROOFSTEP]
erw [multiplicity.pow' (Nat.prime_iff_prime_int.1 hp.1) (finite_int_iff.2 ⟨hp.1.ne_one, this⟩), Nat.mul_mod_right] at hv
[GOAL]
case inr.intro
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
this : y ≠ 0
hv : 0 ≠ 0
⊢ False
[PROOFSTEP]
exact hv rfl
[GOAL]
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 2 = 1
⊢ Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 2 ≠ 0
[PROOFSTEP]
rw [Hpv]
[GOAL]
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 2 = 1
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
p : ℕ
hp : Prime p
⊢ Part.get (multiplicity ↑p ↑p) (_ : multiplicity.Finite ↑p ↑p) % 2 = 1
[PROOFSTEP]
simp [multiplicity.multiplicity_self (mt isUnit_iff_dvd_one.1 (mt Int.coe_nat_dvd.1 hp.not_dvd_one))]
[GOAL]
⊢ Irrational (Real.sqrt 2)
[PROOFSTEP]
simpa using Nat.prime_two.irrational_sqrt
[GOAL]
q : ℚ
H1 : Rat.sqrt q * Rat.sqrt q = q
⊢ ↑(Rat.sqrt q) = Real.sqrt ↑q
[PROOFSTEP]
rw [← H1, cast_mul, sqrt_mul_self (cast_nonneg.2 <| Rat.sqrt_nonneg q), sqrt_eq, abs_of_nonneg (Rat.sqrt_nonneg q)]
[GOAL]
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : 0 ≤ q
x✝ : Real.sqrt ↑q ∈ Set.range Rat.cast
r : ℚ
hr : ↑r = Real.sqrt ↑q
⊢ r * r = q
[PROOFSTEP]
rwa [eq_comm, sqrt_eq_iff_mul_self_eq (cast_nonneg.2 H2), ← cast_mul, Rat.cast_inj] at hr
[GOAL]
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : 0 ≤ q
x✝ : Real.sqrt ↑q ∈ Set.range Rat.cast
r : ℚ
hr : Real.sqrt ↑q = ↑r
⊢ 0 ≤ ↑r
[PROOFSTEP]
rw [← hr]
[GOAL]
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : 0 ≤ q
x✝ : Real.sqrt ↑q ∈ Set.range Rat.cast
r : ℚ
hr : Real.sqrt ↑q = ↑r
⊢ 0 ≤ Real.sqrt ↑q
[PROOFSTEP]
exact Real.sqrt_nonneg _
[GOAL]
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : ¬0 ≤ q
⊢ ↑0 = Real.sqrt ↑q
[PROOFSTEP]
rw [cast_zero]
[GOAL]
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : ¬0 ≤ q
⊢ 0 = Real.sqrt ↑q
[PROOFSTEP]
exact (sqrt_eq_zero_of_nonpos (Rat.cast_nonpos.2 <| le_of_not_le H2)).symm
[GOAL]
x : ℝ
h : Irrational x
m : ℤ
⊢ x ≠ ↑m
[PROOFSTEP]
rw [← Rat.cast_coe_int]
[GOAL]
x : ℝ
h : Irrational x
m : ℤ
⊢ x ≠ ↑↑m
[PROOFSTEP]
exact h.ne_rat _
[GOAL]
x : ℝ
h : Irrational x
⊢ x ≠ 0
[PROOFSTEP]
exact_mod_cast h.ne_nat 0
[GOAL]
x : ℝ
h : Irrational x
⊢ x ≠ 1
[PROOFSTEP]
simpa only [Nat.cast_one] using h.ne_nat 1
[GOAL]
q : ℚ
x y : ℝ
⊢ Irrational (x + y) → Irrational x ∨ Irrational y
[PROOFSTEP]
delta Irrational
[GOAL]
q : ℚ
x y : ℝ
⊢ ¬x + y ∈ Set.range Rat.cast → ¬x ∈ Set.range Rat.cast ∨ ¬y ∈ Set.range Rat.cast
[PROOFSTEP]
contrapose!
[GOAL]
q : ℚ
x y : ℝ
⊢ x ∈ Set.range Rat.cast ∧ y ∈ Set.range Rat.cast → x + y ∈ Set.range Rat.cast
[PROOFSTEP]
rintro ⟨⟨rx, rfl⟩, ⟨ry, rfl⟩⟩
[GOAL]
case intro.intro.intro
q rx ry : ℚ
⊢ ↑rx + ↑ry ∈ Set.range Rat.cast
[PROOFSTEP]
exact ⟨rx + ry, cast_add rx ry⟩
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
⊢ Irrational (↑(-q) + (↑q + x))
[PROOFSTEP]
rwa [cast_neg, neg_add_cancel_left]
[GOAL]
q : ℚ
x y : ℝ
m : ℤ
h : Irrational (↑m + x)
⊢ Irrational x
[PROOFSTEP]
rw [← cast_coe_int] at h
[GOAL]
q : ℚ
x y : ℝ
m : ℤ
h : Irrational (↑↑m + x)
⊢ Irrational x
[PROOFSTEP]
exact h.of_rat_add m
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m + x)
[PROOFSTEP]
rw [← cast_coe_int]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑↑m + x)
[PROOFSTEP]
exact h.rat_add m
[GOAL]
q✝ : ℚ
x y : ℝ
h : Irrational (-x)
x✝ : x ∈ Set.range Rat.cast
q : ℚ
hx : ↑q = x
⊢ ↑(-q) = -x
[PROOFSTEP]
rw [cast_neg, hx]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
⊢ Irrational (- -x)
[PROOFSTEP]
rwa [neg_neg]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
⊢ Irrational (x - ↑q)
[PROOFSTEP]
simpa only [sub_eq_add_neg, cast_neg] using h.add_rat (-q)
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
⊢ Irrational (↑q - x)
[PROOFSTEP]
simpa only [sub_eq_add_neg] using h.neg.rat_add q
[GOAL]
q : ℚ
x y : ℝ
h : Irrational (x - ↑q)
⊢ Irrational (x + ↑(-q))
[PROOFSTEP]
simpa only [cast_neg, sub_eq_add_neg] using h
[GOAL]
q : ℚ
x y : ℝ
h : Irrational (↑q - x)
⊢ Irrational (↑q + -x)
[PROOFSTEP]
simpa only [sub_eq_add_neg] using h
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (x - ↑m)
[PROOFSTEP]
simpa only [Rat.cast_coe_int] using h.sub_rat m
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m - x)
[PROOFSTEP]
simpa only [Rat.cast_coe_int] using h.rat_sub m
[GOAL]
q : ℚ
x y : ℝ
m : ℤ
h : Irrational (x - ↑m)
⊢ Irrational (x - ↑↑m)
[PROOFSTEP]
rwa [Rat.cast_coe_int]
[GOAL]
q : ℚ
x y : ℝ
m : ℤ
h : Irrational (↑m - x)
⊢ Irrational (↑↑m - x)
[PROOFSTEP]
rwa [Rat.cast_coe_int]
[GOAL]
q : ℚ
x y : ℝ
⊢ Irrational (x * y) → Irrational x ∨ Irrational y
[PROOFSTEP]
delta Irrational
[GOAL]
q : ℚ
x y : ℝ
⊢ ¬x * y ∈ Set.range Rat.cast → ¬x ∈ Set.range Rat.cast ∨ ¬y ∈ Set.range Rat.cast
[PROOFSTEP]
contrapose!
[GOAL]
q : ℚ
x y : ℝ
⊢ x ∈ Set.range Rat.cast ∧ y ∈ Set.range Rat.cast → x * y ∈ Set.range Rat.cast
[PROOFSTEP]
rintro ⟨⟨rx, rfl⟩, ⟨ry, rfl⟩⟩
[GOAL]
case intro.intro.intro
q rx ry : ℚ
⊢ ↑rx * ↑ry ∈ Set.range Rat.cast
[PROOFSTEP]
exact ⟨rx * ry, cast_mul rx ry⟩
[GOAL]
q✝ : ℚ
x y : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * ↑q * ↑q⁻¹)
[PROOFSTEP]
rwa [mul_assoc, ← cast_mul, mul_inv_cancel hq, cast_one, mul_one]
[GOAL]
q : ℚ
x y : ℝ
m : ℤ
h : Irrational (x * ↑m)
⊢ Irrational (x * ↑↑m)
[PROOFSTEP]
rwa [cast_coe_int]
[GOAL]
q : ℚ
x y : ℝ
m : ℤ
h : Irrational (↑m * x)
⊢ Irrational (↑↑m * x)
[PROOFSTEP]
rwa [cast_coe_int]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑m)
[PROOFSTEP]
rw [← cast_coe_int]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑↑m)
[PROOFSTEP]
refine' h.mul_rat _
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ ↑m ≠ 0
[PROOFSTEP]
rwa [Int.cast_ne_zero]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
⊢ Irrational x⁻¹⁻¹
[PROOFSTEP]
rwa [inv_inv]
[GOAL]
q✝ : ℚ
x y : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x / ↑q)
[PROOFSTEP]
rw [div_eq_mul_inv, ← cast_inv]
[GOAL]
q✝ : ℚ
x y : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * ↑q⁻¹)
[PROOFSTEP]
exact h.mul_rat (inv_ne_zero hq)
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / ↑m)
[PROOFSTEP]
rw [← cast_coe_int]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / ↑↑m)
[PROOFSTEP]
refine' h.div_rat _
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ ↑m ≠ 0
[PROOFSTEP]
rwa [Int.cast_ne_zero]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational x
m : ℕ
hm : m ≠ 0
⊢ ↑m ≠ 0
[PROOFSTEP]
rwa [Int.coe_nat_ne_zero]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational (1 / x)
⊢ Irrational (↑1 / x)
[PROOFSTEP]
rwa [cast_one]
[GOAL]
q : ℚ
x y : ℝ
h : Irrational (x ^ 0)
⊢ Irrational x
[PROOFSTEP]
rw [pow_zero] at h
[GOAL]
q : ℚ
x y : ℝ
h : Irrational 1
⊢ Irrational x
[PROOFSTEP]
exact (h ⟨1, cast_one⟩).elim
[GOAL]
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))
⊢ Irrational x
[PROOFSTEP]
rw [pow_succ] at h
[GOAL]
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x * x ^ n)
⊢ Irrational x
[PROOFSTEP]
exact h.mul_cases.elim id (of_pow n)
[GOAL]
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ ↑n)
⊢ Irrational x
[PROOFSTEP]
rw [zpow_ofNat] at h
[GOAL]
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ n)
⊢ Irrational x
[PROOFSTEP]
exact h.of_pow _
[GOAL]
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ -[n+1])
⊢ Irrational x
[PROOFSTEP]
rw [zpow_negSucc] at h
[GOAL]
q : ℚ
x y : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))⁻¹
⊢ Irrational x
[PROOFSTEP]
exact h.of_inv.of_pow _
[GOAL]
x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : ↑(aeval x) p = 0
⊢ 1 < natDegree p
[PROOFSTEP]
by_contra rid
[GOAL]
x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : ↑(aeval x) p = 0
rid : ¬1 < natDegree p
⊢ False
[PROOFSTEP]
rcases exists_eq_X_add_C_of_natDegree_le_one (not_lt.1 rid) with ⟨a, b, rfl⟩
[GOAL]
case intro.intro
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
rid : ¬1 < natDegree (↑C a * X + ↑C b)
⊢ False
[PROOFSTEP]
clear rid
[GOAL]
case intro.intro
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
⊢ False
[PROOFSTEP]
have : (a : ℝ) * x = -b := by simpa [eq_neg_iff_add_eq_zero] using x_is_root
[GOAL]
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
⊢ ↑a * x = -↑b
[PROOFSTEP]
simpa [eq_neg_iff_add_eq_zero] using x_is_root
[GOAL]
case intro.intro
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : ↑a * x = -↑b
⊢ False
[PROOFSTEP]
rcases em (a = 0) with (rfl | ha)
[GOAL]
case intro.intro.inl
x : ℝ
hx : Irrational x
b : ℤ
p_nonzero : ↑C 0 * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C 0 * X + ↑C b) = 0
this : ↑0 * x = -↑b
⊢ False
[PROOFSTEP]
obtain rfl : b = 0 := by simpa
[GOAL]
x : ℝ
hx : Irrational x
b : ℤ
p_nonzero : ↑C 0 * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C 0 * X + ↑C b) = 0
this : ↑0 * x = -↑b
⊢ b = 0
[PROOFSTEP]
simpa
[GOAL]
case intro.intro.inl
x : ℝ
hx : Irrational x
p_nonzero : ↑C 0 * X + ↑C 0 ≠ 0
x_is_root : ↑(aeval x) (↑C 0 * X + ↑C 0) = 0
this : ↑0 * x = -↑0
⊢ False
[PROOFSTEP]
simp at p_nonzero
[GOAL]
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : ↑a * x = -↑b
ha : ¬a = 0
⊢ False
[PROOFSTEP]
rw [mul_comm, ← eq_div_iff_mul_eq, eq_comm] at this
[GOAL]
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : -↑b / ↑a = x
ha : ¬a = 0
⊢ False
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
[PROOFSTEP]
refine' hx ⟨-b / a, _⟩
[GOAL]
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : -↑b / ↑a = x
ha : ¬a = 0
⊢ ↑(-↑b / ↑a) = x
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
[PROOFSTEP]
assumption_mod_cast
[GOAL]
case intro.intro.inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : ↑C a * X + ↑C b ≠ 0
x_is_root : ↑(aeval x) (↑C a * X + ↑C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
[PROOFSTEP]
assumption_mod_cast
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (x * ↑q) ↔ q ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [mul_comm, irrational_rat_mul_iff]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (↑m * x) ↔ m ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [← cast_coe_int, irrational_rat_mul_iff, Int.cast_ne_zero]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (x * ↑m) ↔ m ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [← cast_coe_int, irrational_mul_rat_iff, Int.cast_ne_zero]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (↑n * x) ↔ n ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [← cast_coe_nat, irrational_rat_mul_iff, Nat.cast_ne_zero]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (x * ↑n) ↔ n ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [← cast_coe_nat, irrational_mul_rat_iff, Nat.cast_ne_zero]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (↑q / x) ↔ q ≠ 0 ∧ Irrational x
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (x / ↑q) ↔ q ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [div_eq_mul_inv, ← cast_inv, irrational_mul_rat_iff, Ne.def, inv_eq_zero]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (↑m / x) ↔ m ≠ 0 ∧ Irrational x
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (x / ↑m) ↔ m ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [← cast_coe_int, irrational_div_rat_iff, Int.cast_ne_zero]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (↑n / x) ↔ n ≠ 0 ∧ Irrational x
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
q : ℚ
m : ℤ
n : ℕ
x : ℝ
⊢ Irrational (x / ↑n) ↔ n ≠ 0 ∧ Irrational x
[PROOFSTEP]
rw [← cast_coe_nat, irrational_div_rat_iff, Nat.cast_ne_zero]


[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n = c ^ n
[PROOFSTEP]
simp [cantorFunctionAux, h]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n = 0
[PROOFSTEP]
simp [cantorFunctionAux, h]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
h : 0 ≤ c
⊢ 0 ≤ cantorFunctionAux c f n
[PROOFSTEP]
cases h' : f n
[GOAL]
case false
c : ℝ
f g : ℕ → Bool
n : ℕ
h : 0 ≤ c
h' : f n = false
⊢ 0 ≤ cantorFunctionAux c f n
[PROOFSTEP]
simp [h']
[GOAL]
case true
c : ℝ
f g : ℕ → Bool
n : ℕ
h : 0 ≤ c
h' : f n = true
⊢ 0 ≤ cantorFunctionAux c f n
[PROOFSTEP]
simp [h']
[GOAL]
case true
c : ℝ
f g : ℕ → Bool
n : ℕ
h : 0 ≤ c
h' : f n = true
⊢ 0 ≤ c ^ n
[PROOFSTEP]
apply pow_nonneg h
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
h : f n = g n
⊢ cantorFunctionAux c f n = cantorFunctionAux c g n
[PROOFSTEP]
simp [cantorFunctionAux, h]
[GOAL]
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
⊢ cantorFunctionAux c f 0 = bif f 0 then 1 else 0
[PROOFSTEP]
cases h : f 0
[GOAL]
case false
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h : f 0 = false
⊢ cantorFunctionAux c f 0 = bif false then 1 else 0
[PROOFSTEP]
simp [h]
[GOAL]
case true
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h : f 0 = true
⊢ cantorFunctionAux c f 0 = bif true then 1 else 0
[PROOFSTEP]
simp [h]
[GOAL]
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
⊢ (fun n => cantorFunctionAux c f (n + 1)) = fun n => c * cantorFunctionAux c (fun n => f (n + 1)) n
[PROOFSTEP]
ext n
[GOAL]
case h
c : ℝ
f✝ g : ℕ → Bool
n✝ : ℕ
f : ℕ → Bool
n : ℕ
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n => f (n + 1)) n
[PROOFSTEP]
cases h : f (n + 1)
[GOAL]
case h.false
c : ℝ
f✝ g : ℕ → Bool
n✝ : ℕ
f : ℕ → Bool
n : ℕ
h : f (n + 1) = false
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n => f (n + 1)) n
[PROOFSTEP]
simp [h, _root_.pow_succ]
[GOAL]
case h.true
c : ℝ
f✝ g : ℕ → Bool
n✝ : ℕ
f : ℕ → Bool
n : ℕ
h : f (n + 1) = true
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n => f (n + 1)) n
[PROOFSTEP]
simp [h, _root_.pow_succ]
[GOAL]
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ Summable (cantorFunctionAux c f)
[PROOFSTEP]
apply (summable_geometric_of_lt_1 h1 h2).summable_of_eq_zero_or_self
[GOAL]
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ ∀ (b : ℕ), cantorFunctionAux c f b = 0 ∨ cantorFunctionAux c f b = c ^ b
[PROOFSTEP]
intro n
[GOAL]
c : ℝ
f✝ g : ℕ → Bool
n✝ : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
[PROOFSTEP]
cases h : f n
[GOAL]
case false
c : ℝ
f✝ g : ℕ → Bool
n✝ : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
[PROOFSTEP]
simp [h]
[GOAL]
case true
c : ℝ
f✝ g : ℕ → Bool
n✝ : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
[PROOFSTEP]
simp [h]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
⊢ cantorFunction c f ≤ cantorFunction c g
[PROOFSTEP]
apply tsum_le_tsum _ (summable_cantor_function f h1 h2) (summable_cantor_function g h1 h2)
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
⊢ ∀ (i : ℕ), cantorFunctionAux c f i ≤ cantorFunctionAux c g i
[PROOFSTEP]
intro n
[GOAL]
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
[PROOFSTEP]
cases h : f n
[GOAL]
case false
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
case true
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
[PROOFSTEP]
simp [h, cantorFunctionAux_nonneg h1]
[GOAL]
case true
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
[PROOFSTEP]
replace h3 : g n = true := h3 n h
[GOAL]
case true
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = true
h3 : g n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
[PROOFSTEP]
simp [h, h3]
[GOAL]
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ cantorFunction c f = (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)
[PROOFSTEP]
rw [cantorFunction, tsum_eq_zero_add (summable_cantor_function f h1 h2)]
[GOAL]
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ cantorFunctionAux c f 0 + ∑' (b : ℕ), cantorFunctionAux c f (b + 1) =
    (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)
[PROOFSTEP]
rw [cantorFunctionAux_succ, tsum_mul_left, cantorFunctionAux, _root_.pow_zero]
[GOAL]
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ (bif f 0 then 1 else 0) + c * ∑' (x : ℕ), cantorFunctionAux c (fun n => f (n + 1)) x =
    (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)
[PROOFSTEP]
rfl
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
gn : g n = true
⊢ cantorFunction c f < cantorFunction c g
[PROOFSTEP]
have h3 : c < 1 := by
  apply h2.trans
  norm_num
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
gn : g n = true
⊢ c < 1
[PROOFSTEP]
apply h2.trans
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
gn : g n = true
⊢ 1 / 2 < 1
[PROOFSTEP]
norm_num
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
gn : g n = true
h3 : c < 1
⊢ cantorFunction c f < cantorFunction c g
[PROOFSTEP]
induction' n with n ih generalizing f g
[GOAL]
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
⊢ cantorFunction c f < cantorFunction c g
[PROOFSTEP]
let f_max : ℕ → Bool := fun n => Nat.rec false (fun _ _ => true) n
[GOAL]
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
⊢ cantorFunction c f < cantorFunction c g
[PROOFSTEP]
have hf_max : ∀ n, f n → f_max n := by
  intro n hn
  cases n
  rw [fn] at hn
  contradiction
  apply rfl
[GOAL]
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
⊢ ∀ (n : ℕ), f n = true → f_max n = true
[PROOFSTEP]
intro n hn
[GOAL]
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
n : ℕ
hn : f n = true
⊢ f_max n = true
[PROOFSTEP]
cases n
[GOAL]
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hn : f zero = true
⊢ f_max zero = true
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
n✝ : ℕ
hn : f (succ n✝) = true
⊢ f_max (succ n✝) = true
[PROOFSTEP]
rw [fn] at hn
[GOAL]
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hn : false = true
⊢ f_max zero = true
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
n✝ : ℕ
hn : f (succ n✝) = true
⊢ f_max (succ n✝) = true
[PROOFSTEP]
contradiction
[GOAL]
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
n✝ : ℕ
hn : f (succ n✝) = true
⊢ f_max (succ n✝) = true
[PROOFSTEP]
apply rfl
[GOAL]
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
⊢ cantorFunction c f < cantorFunction c g
[PROOFSTEP]
let g_min : ℕ → Bool := fun n => Nat.rec true (fun _ _ => false) n
[GOAL]
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
⊢ cantorFunction c f < cantorFunction c g
[PROOFSTEP]
have hg_min : ∀ n, g_min n → g n := by
  intro n hn
  cases n
  rw [gn]
  simp at hn
[GOAL]
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
⊢ ∀ (n : ℕ), g_min n = true → g n = true
[PROOFSTEP]
intro n hn
[GOAL]
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
n : ℕ
hn : g_min n = true
⊢ g n = true
[PROOFSTEP]
cases n
[GOAL]
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hn : g_min zero = true
⊢ g zero = true
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
n✝ : ℕ
hn : g_min (succ n✝) = true
⊢ g (succ n✝) = true
[PROOFSTEP]
rw [gn]
[GOAL]
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
n✝ : ℕ
hn : g_min (succ n✝) = true
⊢ g (succ n✝) = true
[PROOFSTEP]
simp at hn
[GOAL]
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ cantorFunction c f < cantorFunction c g
[PROOFSTEP]
apply (cantorFunction_le (le_of_lt h1) h3 hf_max).trans_lt
[GOAL]
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ (cantorFunction c fun n => f_max n) < cantorFunction c g
[PROOFSTEP]
refine' lt_of_lt_of_le _ (cantorFunction_le (le_of_lt h1) h3 hg_min)
[GOAL]
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ (cantorFunction c fun n => f_max n) < cantorFunction c fun n => g_min n
[PROOFSTEP]
have : c / (1 - c) < 1 := by
  rw [div_lt_one, lt_sub_iff_add_lt]
  · convert _root_.add_lt_add h2 h2
    norm_num
  rwa [sub_pos]
[GOAL]
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ c / (1 - c) < 1
[PROOFSTEP]
rw [div_lt_one, lt_sub_iff_add_lt]
[GOAL]
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ c + c < 1
[PROOFSTEP]
convert _root_.add_lt_add h2 h2
[GOAL]
case h.e'_4
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ 1 = 1 / 2 + 1 / 2
[PROOFSTEP]
norm_num
[GOAL]
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ 0 < 1 - c
[PROOFSTEP]
rwa [sub_pos]
[GOAL]
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ (cantorFunction c fun n => f_max n) < cantorFunction c fun n => g_min n
[PROOFSTEP]
convert this
[GOAL]
case h.e'_3
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ (cantorFunction c fun n => f_max n) = c / (1 - c)
[PROOFSTEP]
rw [cantorFunction_succ _ (le_of_lt h1) h3, div_eq_mul_inv, ← tsum_geometric_of_lt_1 (le_of_lt h1) h3]
[GOAL]
case h.e'_3
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ ((bif f_max 0 then 1 else 0) + c * cantorFunction c fun n => f_max (n + 1)) = c * ∑' (n : ℕ), c ^ n
[PROOFSTEP]
apply zero_add
[GOAL]
case h.e'_4
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ (cantorFunction c fun n => g_min n) = 1
[PROOFSTEP]
refine' (tsum_eq_single 0 _).trans _
[GOAL]
case h.e'_4.refine'_1
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ ∀ (b' : ℕ), b' ≠ 0 → cantorFunctionAux c (fun n => g_min n) b' = 0
[PROOFSTEP]
intro n hn
[GOAL]
case h.e'_4.refine'_1
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
n : ℕ
hn : n ≠ 0
⊢ cantorFunctionAux c (fun n => g_min n) n = 0
[PROOFSTEP]
cases n
[GOAL]
case h.e'_4.refine'_1.zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
hn : zero ≠ 0
⊢ cantorFunctionAux c (fun n => g_min n) zero = 0
case h.e'_4.refine'_1.succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
n✝ : ℕ
hn : succ n✝ ≠ 0
⊢ cantorFunctionAux c (fun n => g_min n) (succ n✝) = 0
[PROOFSTEP]
contradiction
[GOAL]
case h.e'_4.refine'_1.succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
n✝ : ℕ
hn : succ n✝ ≠ 0
⊢ cantorFunctionAux c (fun n => g_min n) (succ n✝) = 0
[PROOFSTEP]
rfl
[GOAL]
case h.e'_4.refine'_2
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ cantorFunctionAux c (fun n => g_min n) 0 = 1
[PROOFSTEP]
exact cantorFunctionAux_zero _
[GOAL]
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ cantorFunction c f < cantorFunction c g
[PROOFSTEP]
rw [cantorFunction_succ f (le_of_lt h1) h3, cantorFunction_succ g (le_of_lt h1) h3]
[GOAL]
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ ((bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)) <
    (bif g 0 then 1 else 0) + c * cantorFunction c fun n => g (n + 1)
[PROOFSTEP]
rw [hn 0 <| zero_lt_succ n]
[GOAL]
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ ((bif g 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)) <
    (bif g 0 then 1 else 0) + c * cantorFunction c fun n => g (n + 1)
[PROOFSTEP]
apply add_lt_add_left
[GOAL]
case succ.bc
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ (c * cantorFunction c fun n => f (n + 1)) < c * cantorFunction c fun n => g (n + 1)
[PROOFSTEP]
rw [mul_lt_mul_left h1]
[GOAL]
case succ.bc
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ (cantorFunction c fun n => f (n + 1)) < cantorFunction c fun n => g (n + 1)
[PROOFSTEP]
exact ih (fun k hk => hn _ <| Nat.succ_lt_succ hk) fn gn
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
⊢ Function.Injective (cantorFunction c)
[PROOFSTEP]
intro f g hfg
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
⊢ f = g
[PROOFSTEP]
classical
by_contra h
revert hfg
have : ∃ n, f n ≠ g n := by
  rw [← not_forall]
  intro h'
  apply h
  ext
  apply h'
let n := Nat.find this
have hn : ∀ k : ℕ, k < n → f k = g k := by
  intro k hk
  apply of_not_not
  exact Nat.find_min this hk
cases fn : f n
· apply _root_.ne_of_lt
  refine' increasing_cantorFunction h1 h2 hn fn _
  apply Bool.eq_true_of_not_eq_false
  rw [← fn]
  apply Ne.symm
  exact Nat.find_spec this
· apply _root_.ne_of_gt
  refine' increasing_cantorFunction h1 h2 (fun k hk => (hn k hk).symm) _ fn
  apply Bool.eq_false_of_not_eq_true
  rw [← fn]
  apply Ne.symm
  exact Nat.find_spec this
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
⊢ f = g
[PROOFSTEP]
by_contra h
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
h : ¬f = g
⊢ False
[PROOFSTEP]
revert hfg
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
⊢ cantorFunction c f = cantorFunction c g → False
[PROOFSTEP]
have : ∃ n, f n ≠ g n := by
  rw [← not_forall]
  intro h'
  apply h
  ext
  apply h'
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
⊢ ∃ n, f n ≠ g n
[PROOFSTEP]
rw [← not_forall]
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
⊢ ¬∀ (x : ℕ), f x = g x
[PROOFSTEP]
intro h'
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
h' : ∀ (x : ℕ), f x = g x
⊢ False
[PROOFSTEP]
apply h
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
h' : ∀ (x : ℕ), f x = g x
⊢ f = g
[PROOFSTEP]
ext
[GOAL]
case h
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
h' : ∀ (x : ℕ), f x = g x
x✝ : ℕ
⊢ f x✝ = g x✝
[PROOFSTEP]
apply h'
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
⊢ cantorFunction c f = cantorFunction c g → False
[PROOFSTEP]
let n := Nat.find this
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
⊢ cantorFunction c f = cantorFunction c g → False
[PROOFSTEP]
have hn : ∀ k : ℕ, k < n → f k = g k := by
  intro k hk
  apply of_not_not
  exact Nat.find_min this hk
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
⊢ ∀ (k : ℕ), k < n → f k = g k
[PROOFSTEP]
intro k hk
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
k : ℕ
hk : k < n
⊢ f k = g k
[PROOFSTEP]
apply of_not_not
[GOAL]
case a
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
k : ℕ
hk : k < n
⊢ ¬¬f k = g k
[PROOFSTEP]
exact Nat.find_min this hk
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
⊢ cantorFunction c f = cantorFunction c g → False
[PROOFSTEP]
cases fn : f n
[GOAL]
case false
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
⊢ cantorFunction c f = cantorFunction c g → False
[PROOFSTEP]
apply _root_.ne_of_lt
[GOAL]
case false.h
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
⊢ cantorFunction c f < cantorFunction c g
[PROOFSTEP]
refine' increasing_cantorFunction h1 h2 hn fn _
[GOAL]
case false.h
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
⊢ g n = true
[PROOFSTEP]
apply Bool.eq_true_of_not_eq_false
[GOAL]
case false.h.a
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
⊢ ¬g n = false
[PROOFSTEP]
rw [← fn]
[GOAL]
case false.h.a
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
⊢ ¬g n = f n
[PROOFSTEP]
apply Ne.symm
[GOAL]
case false.h.a.h
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
⊢ f n ≠ g n
[PROOFSTEP]
exact Nat.find_spec this
[GOAL]
case true
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = true
⊢ cantorFunction c f = cantorFunction c g → False
[PROOFSTEP]
apply _root_.ne_of_gt
[GOAL]
case true.h
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = true
⊢ cantorFunction c g < cantorFunction c f
[PROOFSTEP]
refine' increasing_cantorFunction h1 h2 (fun k hk => (hn k hk).symm) _ fn
[GOAL]
case true.h
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = true
⊢ g n = false
[PROOFSTEP]
apply Bool.eq_false_of_not_eq_true
[GOAL]
case true.h.a
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = true
⊢ ¬g n = true
[PROOFSTEP]
rw [← fn]
[GOAL]
case true.h.a
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = true
⊢ ¬g n = f n
[PROOFSTEP]
apply Ne.symm
[GOAL]
case true.h.a.h
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = true
⊢ f n ≠ g n
[PROOFSTEP]
exact Nat.find_spec this
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ #ℝ = 𝔠
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ #ℝ ≤ 𝔠
[PROOFSTEP]
rw [Real.equivCauchy.cardinal_eq]
[GOAL]
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ #(CauSeq.Completion.Cauchy abs) ≤ 𝔠
[PROOFSTEP]
apply mk_quotient_le.trans
[GOAL]
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ #(CauSeq ℚ abs) ≤ 𝔠
[PROOFSTEP]
apply (mk_subtype_le _).trans_eq
[GOAL]
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ #(ℕ → ℚ) = 𝔠
[PROOFSTEP]
rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]
[GOAL]
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 𝔠 ≤ #ℝ
[PROOFSTEP]
convert mk_le_of_injective (cantorFunction_injective _ _)
[GOAL]
case h.e'_3
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 𝔠 = #(ℕ → Bool)
case a.convert_1
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℝ
case a.convert_2
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 0 < ?a.convert_1✝
case a.convert_3 c : ℝ f g : ℕ → Bool n : ℕ ⊢ ?a.convert_1✝ < 1 / 2
[PROOFSTEP]
rw [← power_def, mk_bool, mk_nat, two_power_aleph0]
[GOAL]
case a.convert_1
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℝ
case a.convert_2
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 0 < ?a.convert_1✝
case a.convert_3 c : ℝ f g : ℕ → Bool n : ℕ ⊢ ?a.convert_1✝ < 1 / 2
[PROOFSTEP]
exact 1 / 3
[GOAL]
case a.convert_2
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 0 < 1 / 3
case a.convert_3 c : ℝ f g : ℕ → Bool n : ℕ ⊢ 1 / 3 < 1 / 2
[PROOFSTEP]
norm_num
[GOAL]
case a.convert_3
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 1 / 3 < 1 / 2
[PROOFSTEP]
norm_num
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ #↑Set.univ = 𝔠
[PROOFSTEP]
rw [mk_univ, mk_real]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ¬Set.Countable Set.univ
[PROOFSTEP]
rw [← le_aleph0_iff_set_countable, not_le, mk_univ_real]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℵ₀ < 𝔠
[PROOFSTEP]
apply cantor
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ #↑(Ioi a) = 𝔠
[PROOFSTEP]
refine' le_antisymm (mk_real ▸ mk_set_le _) _
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ 𝔠 ≤ #↑(Ioi a)
[PROOFSTEP]
rw [← not_lt]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ ¬#↑(Ioi a) < 𝔠
[PROOFSTEP]
intro h
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ False
[PROOFSTEP]
refine' _root_.ne_of_lt _ mk_univ_real
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ #↑Set.univ < 𝔠
[PROOFSTEP]
have hu : Iio a ∪ { a } ∪ Ioi a = Set.univ :=
  by
  convert @Iic_union_Ioi ℝ _ _
  exact Iio_union_right
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ Iio a ∪ {a} ∪ Ioi a = Set.univ
[PROOFSTEP]
convert @Iic_union_Ioi ℝ _ _
[GOAL]
case h.e'_2.h.e'_3
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ Iio a ∪ {a} = Iic a
[PROOFSTEP]
exact Iio_union_right
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑Set.univ < 𝔠
[PROOFSTEP]
rw [← hu]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a ∪ {a} ∪ Ioi a) < 𝔠
[PROOFSTEP]
refine' lt_of_le_of_lt (mk_union_le _ _) _
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a ∪ {a}) + #↑(Ioi a) < 𝔠
[PROOFSTEP]
refine' lt_of_le_of_lt (add_le_add_right (mk_union_le _ _) _) _
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a) + #↑{a} + #↑(Ioi a) < 𝔠
[PROOFSTEP]
have h2 : (fun x => a + a - x) '' Ioi a = Iio a :=
  by
  convert @image_const_sub_Ioi ℝ _ _ _
  simp
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (fun x => a + a - x) '' Ioi a = Iio a
[PROOFSTEP]
convert @image_const_sub_Ioi ℝ _ _ _
[GOAL]
case h.e'_3.h.e'_3
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ a = a + a - a
[PROOFSTEP]
simp
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑(Iio a) + #↑{a} + #↑(Ioi a) < 𝔠
[PROOFSTEP]
rw [← h2]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑((fun x => a + a - x) '' Ioi a) + #↑{a} + #↑(Ioi a) < 𝔠
[PROOFSTEP]
refine' add_lt_of_lt (cantor _).le _ h
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑((fun x => a + a - x) '' Ioi a) + #↑{a} < 𝔠
[PROOFSTEP]
refine' add_lt_of_lt (cantor _).le (mk_image_le.trans_lt h) _
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑{a} < 𝔠
[PROOFSTEP]
rw [mk_singleton]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ 1 < 𝔠
[PROOFSTEP]
exact one_lt_aleph0.trans (cantor _)
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ #↑(Iio a) = 𝔠
[PROOFSTEP]
refine' le_antisymm (mk_real ▸ mk_set_le _) _
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ 𝔠 ≤ #↑(Iio a)
[PROOFSTEP]
have h2 : (fun x => a + a - x) '' Iio a = Ioi a := by simp only [image_const_sub_Iio, add_sub_cancel]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ (fun x => a + a - x) '' Iio a = Ioi a
[PROOFSTEP]
simp only [image_const_sub_Iio, add_sub_cancel]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h2 : (fun x => a + a - x) '' Iio a = Ioi a
⊢ 𝔠 ≤ #↑(Iio a)
[PROOFSTEP]
exact mk_Ioi_real a ▸ h2 ▸ mk_image_le
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h : a < b
⊢ #↑(Ioo a b) = 𝔠
[PROOFSTEP]
refine' le_antisymm (mk_real ▸ mk_set_le _) _
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h : a < b
⊢ 𝔠 ≤ #↑(Ioo a b)
[PROOFSTEP]
have h1 : #((fun x => x - a) '' Ioo a b) ≤ #(Ioo a b) := mk_image_le
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h : a < b
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
⊢ 𝔠 ≤ #↑(Ioo a b)
[PROOFSTEP]
refine' le_trans _ h1
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h : a < b
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
⊢ 𝔠 ≤ #↑((fun x => x - a) '' Ioo a b)
[PROOFSTEP]
rw [image_sub_const_Ioo, sub_self]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h : a < b
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))
[PROOFSTEP]
replace h := sub_pos_of_lt h
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))
[PROOFSTEP]
have h2 : #(Inv.inv '' Ioo 0 (b - a)) ≤ #(Ioo 0 (b - a)) := mk_image_le
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
h2 : #↑(Inv.inv '' Ioo 0 (b - a)) ≤ #↑(Ioo 0 (b - a))
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))
[PROOFSTEP]
refine' le_trans _ h2
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
h2 : #↑(Inv.inv '' Ioo 0 (b - a)) ≤ #↑(Ioo 0 (b - a))
⊢ 𝔠 ≤ #↑(Inv.inv '' Ioo 0 (b - a))
[PROOFSTEP]
rw [image_inv, inv_Ioo_0_left h, mk_Ioi_real]


[GOAL]
α : Type u_1
inst✝ : Fintype α
⊢ ↑(powerset univ) = ↑univ
[PROOFSTEP]
simp [-coe_eq_univ]
[GOAL]
α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ powerset s = univ ↔ s = univ
[PROOFSTEP]
rw [← Finset.powerset_univ, powerset_inj]
[GOAL]
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
k : ℕ
⊢ filter (fun s => card s = k) univ = powersetLen k univ
[PROOFSTEP]
ext
[GOAL]
case a
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
k : ℕ
a✝ : Finset α
⊢ a✝ ∈ filter (fun s => card s = k) univ ↔ a✝ ∈ powersetLen k univ
[PROOFSTEP]
simp [Finset.mem_powersetLen]
[GOAL]
α : Type u_1
inst✝ : Fintype α
k : ℕ
⊢ card { s // Finset.card s = k } = Nat.choose (card α) k
[PROOFSTEP]
simp [Fintype.subtype_card, Finset.card_univ]
[GOAL]
α : Type u_1
inst✝ : Fintype α
s : Set α
⊢ s ∈ map { toFun := toSet, inj' := (_ : Function.Injective toSet) } (Finset.powerset Finset.univ)
[PROOFSTEP]
classical
refine' mem_map.2 ⟨Finset.univ.filter s, Finset.mem_powerset.2 (Finset.subset_univ _), _⟩
apply (coe_filter _ _).trans
simp
rfl
[GOAL]
α : Type u_1
inst✝ : Fintype α
s : Set α
⊢ s ∈ map { toFun := toSet, inj' := (_ : Function.Injective toSet) } (Finset.powerset Finset.univ)
[PROOFSTEP]
refine' mem_map.2 ⟨Finset.univ.filter s, Finset.mem_powerset.2 (Finset.subset_univ _), _⟩
[GOAL]
α : Type u_1
inst✝ : Fintype α
s : Set α
⊢ ↑{ toFun := toSet, inj' := (_ : Function.Injective toSet) } (filter s Finset.univ) = s
[PROOFSTEP]
apply (coe_filter _ _).trans
[GOAL]
α : Type u_1
inst✝ : Fintype α
s : Set α
⊢ {x | x ∈ Finset.univ ∧ s x} = s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Fintype α
s : Set α
⊢ {x | s x} = s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : Finite α
⊢ Finite (Set α)
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type u_1
inst✝ : Finite α
val✝ : Fintype α
⊢ Finite (Set α)
[PROOFSTEP]
infer_instance


[GOAL]
R : Type u
inst✝ : Ring R
M : FGModuleCat R
⊢ AddCommGroup ↑M
[PROOFSTEP]
change AddCommGroup M.obj
[GOAL]
R : Type u
inst✝ : Ring R
M : FGModuleCat R
⊢ AddCommGroup ↑M.obj
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : Ring R
M : FGModuleCat R
⊢ Module R ↑M
[PROOFSTEP]
change Module R M.obj
[GOAL]
R : Type u
inst✝ : Ring R
M : FGModuleCat R
⊢ Module R ↑M.obj
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : Ring R
⊢ LargeCategory (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : Ring R
⊢ LargeCategory (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : Ring R
⊢ ConcreteCategory (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : Ring R
⊢ ConcreteCategory (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : Ring R
⊢ Preadditive (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : Ring R
⊢ Preadditive (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝³ : Ring R
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Module.Finite R V
⊢ Module.Finite R ↑(ModuleCat.of R V)
[PROOFSTEP]
change Module.Finite R V
[GOAL]
R : Type u
inst✝³ : Ring R
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Module.Finite R V
⊢ Module.Finite R V
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : Ring R
⊢ HasForget₂ (FGModuleCat R) (ModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : Ring R
⊢ HasForget₂ (FullSubcategory fun V => Module.Finite R ↑V) (ModuleCat R)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝⁶ : Ring R
V W : Type u
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
⊢ ↑e ≫ ↑(LinearEquiv.symm e) = 𝟙 (of R V)
[PROOFSTEP]
ext x
[GOAL]
case w
R : Type u
inst✝⁶ : Ring R
V W : Type u
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
x : (forget (FGModuleCat R)).obj (of R V)
⊢ ↑(↑e ≫ ↑(LinearEquiv.symm e)) x = ↑(𝟙 (of R V)) x
[PROOFSTEP]
exact e.left_inv x
[GOAL]
R : Type u
inst✝⁶ : Ring R
V W : Type u
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
⊢ ↑(LinearEquiv.symm e) ≫ ↑e = 𝟙 (of R W)
[PROOFSTEP]
ext x
[GOAL]
case w
R : Type u
inst✝⁶ : Ring R
V W : Type u
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
x : (forget (FGModuleCat R)).obj (of R W)
⊢ ↑(↑(LinearEquiv.symm e) ≫ ↑e) x = ↑(𝟙 (of R W)) x
[PROOFSTEP]
exact e.right_inv x
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Linear R (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Linear R (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalCategory (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalCategory (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ SymmetricCategory (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ SymmetricCategory (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalPreadditive (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalPreadditive (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalLinear R (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalLinear R (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Faithful (forget₂Monoidal R).toLaxMonoidalFunctor.toFunctor
[PROOFSTEP]
dsimp [forget₂Monoidal]
  -- Porting note: was `infer_instance`
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Faithful (fullSubcategoryInclusion fun V => Module.Finite R ↑V)
[PROOFSTEP]
exact FullSubcategory.faithful _
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Functor.Additive (forget₂Monoidal R).toLaxMonoidalFunctor.toFunctor
[PROOFSTEP]
dsimp [forget₂Monoidal]
  -- Porting note: was `infer_instance`
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Functor.Additive (fullSubcategoryInclusion fun V => Module.Finite R ↑V)
[PROOFSTEP]
exact Functor.fullSubcategoryInclusion_additive _
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Functor.Linear R (forget₂Monoidal R).toLaxMonoidalFunctor.toFunctor
[PROOFSTEP]
dsimp [forget₂Monoidal]
  -- Porting note: was `infer_instance`
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Functor.Linear R (fullSubcategoryInclusion fun V => Module.Finite R ↑V)
[PROOFSTEP]
exact Functor.fullSubcategoryInclusionLinear _ _
[GOAL]
K : Type u
inst✝ : Field K
V W : FGModuleCat K
⊢ Module.Finite K (↑V →ₗ[K] ↑W)
[PROOFSTEP]
infer_instance
[GOAL]
K : Type u
inst✝ : Field K
⊢ MonoidalClosed (FGModuleCat K)
[PROOFSTEP]
dsimp [FGModuleCat]
  -- Porting note: was `infer_instance`
[GOAL]
K : Type u
inst✝ : Field K
⊢ MonoidalClosed (FullSubcategory fun V => Module.Finite K ↑V)
[PROOFSTEP]
exact MonoidalCategory.fullMonoidalClosedSubcategory _
[GOAL]
K : Type u
inst✝ : Field K
V W : FGModuleCat K
⊢ (𝟙 (FGModuleCatDual K V) ⊗ FGModuleCatCoevaluation K V) ≫
      (α_ (FGModuleCatDual K V) V (FGModuleCatDual K V)).inv ≫ (FGModuleCatEvaluation K V ⊗ 𝟙 (FGModuleCatDual K V)) =
    (ρ_ (FGModuleCatDual K V)).hom ≫ (λ_ (FGModuleCatDual K V)).inv
[PROOFSTEP]
apply contractLeft_assoc_coevaluation K V
[GOAL]
K : Type u
inst✝ : Field K
V W : FGModuleCat K
⊢ (FGModuleCatCoevaluation K V ⊗ 𝟙 V) ≫ (α_ V (FGModuleCatDual K V) V).hom ≫ (𝟙 V ⊗ FGModuleCatEvaluation K V) =
    (λ_ V).hom ≫ (ρ_ V).inv
[PROOFSTEP]
apply contractLeft_assoc_coevaluation' K V


[GOAL]
α : Type u_1
x : ℤˣ
⊢ x ∈ {1, -1}
[PROOFSTEP]
cases Int.units_eq_one_or x
[GOAL]
case inl
α : Type u_1
x : ℤˣ
h✝ : x = 1
⊢ x ∈ {1, -1}
[PROOFSTEP]
simp [*]
[GOAL]
case inr
α : Type u_1
x : ℤˣ
h✝ : x = -1
⊢ x ∈ {1, -1}
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card α = card αˣ + 1
[PROOFSTEP]
rw [eq_comm, Fintype.card_congr (unitsEquivNeZero α)]
[GOAL]
α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card { a // a ≠ 0 } + 1 = card α
[PROOFSTEP]
have := Fintype.card_congr (Equiv.sumCompl (· = (0 : α)))
[GOAL]
α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) = card α
⊢ card { a // a ≠ 0 } + 1 = card α
[PROOFSTEP]
rwa [Fintype.card_sum, add_comm, Fintype.card_subtype_eq] at this
[GOAL]
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : Finite α
⊢ Nat.card α = Nat.card αˣ + 1
[PROOFSTEP]
have : Fintype α := Fintype.ofFinite α
[GOAL]
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α = Nat.card αˣ + 1
[PROOFSTEP]
classical rw [Nat.card_eq_fintype_card, Nat.card_eq_fintype_card, Fintype.card_eq_card_units_add_one]
[GOAL]
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α = Nat.card αˣ + 1
[PROOFSTEP]
rw [Nat.card_eq_fintype_card, Nat.card_eq_fintype_card, Fintype.card_eq_card_units_add_one]
[GOAL]
α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card αˣ = card α - 1
[PROOFSTEP]
rw [@Fintype.card_eq_card_units_add_one α, Nat.add_sub_cancel]


[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
⊢ sInf (a • s) = a • sInf s
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
⊢ sInf (a • ∅) = a • sInf ∅
[PROOFSTEP]
rw [smul_set_empty, Real.sInf_empty, smul_zero]
[GOAL]
case inr
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
⊢ sInf (a • s) = a • sInf s
[PROOFSTEP]
obtain rfl | ha' := ha.eq_or_lt
[GOAL]
case inr.inl
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sInf (0 • s) = 0 • sInf s
[PROOFSTEP]
rw [zero_smul_set hs, zero_smul]
[GOAL]
case inr.inl
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sInf 0 = 0
[PROOFSTEP]
exact csInf_singleton 0
[GOAL]
case inr.inr
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
⊢ sInf (a • s) = a • sInf s
[PROOFSTEP]
by_cases h : BddBelow s
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
h : BddBelow s
⊢ sInf (a • s) = a • sInf s
[PROOFSTEP]
exact ((OrderIso.smulLeft ℝ ha').map_csInf' hs h).symm
[GOAL]
case neg
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
h : ¬BddBelow s
⊢ sInf (a • s) = a • sInf s
[PROOFSTEP]
rw [Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_pos ha').1 h), Real.sInf_of_not_bddBelow h, smul_zero]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
⊢ sSup (a • s) = a • sSup s
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
⊢ sSup (a • ∅) = a • sSup ∅
[PROOFSTEP]
rw [smul_set_empty, Real.sSup_empty, smul_zero]
[GOAL]
case inr
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
⊢ sSup (a • s) = a • sSup s
[PROOFSTEP]
obtain rfl | ha' := ha.eq_or_lt
[GOAL]
case inr.inl
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sSup (0 • s) = 0 • sSup s
[PROOFSTEP]
rw [zero_smul_set hs, zero_smul]
[GOAL]
case inr.inl
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sSup 0 = 0
[PROOFSTEP]
exact csSup_singleton 0
[GOAL]
case inr.inr
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
⊢ sSup (a • s) = a • sSup s
[PROOFSTEP]
by_cases h : BddAbove s
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
h : BddAbove s
⊢ sSup (a • s) = a • sSup s
[PROOFSTEP]
exact ((OrderIso.smulLeft ℝ ha').map_csSup' hs h).symm
[GOAL]
case neg
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
h : ¬BddAbove s
⊢ sSup (a • s) = a • sSup s
[PROOFSTEP]
rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_pos ha').1 h), Real.sSup_of_not_bddAbove h, smul_zero]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
⊢ sInf (a • s) = a • sSup s
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : a ≤ 0
⊢ sInf (a • ∅) = a • sSup ∅
[PROOFSTEP]
rw [smul_set_empty, Real.sInf_empty, Real.sSup_empty, smul_zero]
[GOAL]
case inr
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : Set.Nonempty s
⊢ sInf (a • s) = a • sSup s
[PROOFSTEP]
obtain rfl | ha' := ha.eq_or_lt
[GOAL]
case inr.inl
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sInf (0 • s) = 0 • sSup s
[PROOFSTEP]
rw [zero_smul_set hs, zero_smul]
[GOAL]
case inr.inl
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sInf 0 = 0
[PROOFSTEP]
exact csInf_singleton 0
[GOAL]
case inr.inr
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : Set.Nonempty s
ha' : a < 0
⊢ sInf (a • s) = a • sSup s
[PROOFSTEP]
by_cases h : BddAbove s
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : Set.Nonempty s
ha' : a < 0
h : BddAbove s
⊢ sInf (a • s) = a • sSup s
[PROOFSTEP]
exact ((OrderIso.smulLeftDual ℝ ha').map_csSup' hs h).symm
[GOAL]
case neg
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : Set.Nonempty s
ha' : a < 0
h : ¬BddAbove s
⊢ sInf (a • s) = a • sSup s
[PROOFSTEP]
rw [Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_neg ha').1 h), Real.sSup_of_not_bddAbove h, smul_zero]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
⊢ sSup (a • s) = a • sInf s
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : a ≤ 0
⊢ sSup (a • ∅) = a • sInf ∅
[PROOFSTEP]
rw [smul_set_empty, Real.sSup_empty, Real.sInf_empty, smul_zero]
[GOAL]
case inr
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : Set.Nonempty s
⊢ sSup (a • s) = a • sInf s
[PROOFSTEP]
obtain rfl | ha' := ha.eq_or_lt
[GOAL]
case inr.inl
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sSup (0 • s) = 0 • sInf s
[PROOFSTEP]
rw [zero_smul_set hs, zero_smul]
[GOAL]
case inr.inl
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sSup 0 = 0
[PROOFSTEP]
exact csSup_singleton 0
[GOAL]
case inr.inr
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : Set.Nonempty s
ha' : a < 0
⊢ sSup (a • s) = a • sInf s
[PROOFSTEP]
by_cases h : BddBelow s
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : Set.Nonempty s
ha' : a < 0
h : BddBelow s
⊢ sSup (a • s) = a • sInf s
[PROOFSTEP]
exact ((OrderIso.smulLeftDual ℝ ha').map_csInf' hs h).symm
[GOAL]
case neg
ι : Sort u_1
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Module α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : Set.Nonempty s
ha' : a < 0
h : ¬BddBelow s
⊢ sSup (a • s) = a • sInf s
[PROOFSTEP]
rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_neg ha').1 h), Real.sInf_of_not_bddBelow h, smul_zero]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : LinearOrderedField α
r : ℝ
ha : 0 ≤ r
f : ι → ℝ
⊢ (⨅ (i : ι), f i) * r = ⨅ (i : ι), f i * r
[PROOFSTEP]
simp only [Real.mul_iInf_of_nonneg ha, mul_comm]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : LinearOrderedField α
r : ℝ
ha : 0 ≤ r
f : ι → ℝ
⊢ (⨆ (i : ι), f i) * r = ⨆ (i : ι), f i * r
[PROOFSTEP]
simp only [Real.mul_iSup_of_nonneg ha, mul_comm]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : LinearOrderedField α
r : ℝ
ha : r ≤ 0
f : ι → ℝ
⊢ (⨅ (i : ι), f i) * r = ⨆ (i : ι), f i * r
[PROOFSTEP]
simp only [Real.mul_iInf_of_nonpos ha, mul_comm]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : LinearOrderedField α
r : ℝ
ha : r ≤ 0
f : ι → ℝ
⊢ (⨆ (i : ι), f i) * r = ⨅ (i : ι), f i * r
[PROOFSTEP]
simp only [Real.mul_iSup_of_nonpos ha, mul_comm]


[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r✝ : ℝ
hr : 0 < r✝
hg : Tendsto (fun x => -f x) atTop (𝓝 (-0))
⊢ -ofSeq f < ↑r✝
[PROOFSTEP]
rw [neg_zero] at hg
[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r✝ : ℝ
hr : 0 < r✝
hg : Tendsto (fun x => -f x) atTop (𝓝 0)
⊢ -ofSeq f < ↑r✝
[PROOFSTEP]
exact lt_of_tendsto_zero_of_pos hg hr
[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : r < 0
⊢ ↑r < ofSeq f
[PROOFSTEP]
rw [← neg_neg r, coe_neg]
[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : r < 0
⊢ -↑(-r) < ofSeq f
[PROOFSTEP]
exact neg_lt_of_tendsto_zero_of_pos hf (neg_pos.mpr hr)
[GOAL]
x : ℝ*
r : ℝ
⊢ IsSt x r ↔ Germ.Tendsto x (𝓝 r)
[PROOFSTEP]
rcases ofSeq_surjective x with ⟨f, rfl⟩
[GOAL]
case intro
r : ℝ
f : ℕ → ℝ
⊢ IsSt (ofSeq f) r ↔ Germ.Tendsto (ofSeq f) (𝓝 r)
[PROOFSTEP]
exact isSt_ofSeq_iff_tendsto
[GOAL]
x y : ℝ*
r s : ℝ
hxr : IsSt x r
hys : IsSt y s
hrs : r < s
⊢ x < y
[PROOFSTEP]
rcases ofSeq_surjective x with ⟨f, rfl⟩
[GOAL]
case intro
y : ℝ*
r s : ℝ
hys : IsSt y s
hrs : r < s
f : ℕ → ℝ
hxr : IsSt (ofSeq f) r
⊢ ofSeq f < y
[PROOFSTEP]
rcases ofSeq_surjective y with ⟨g, rfl⟩
[GOAL]
case intro.intro
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : IsSt (ofSeq f) r
g : ℕ → ℝ
hys : IsSt (ofSeq g) s
⊢ ofSeq f < ofSeq g
[PROOFSTEP]
rw [isSt_ofSeq_iff_tendsto] at hxr hys
[GOAL]
case intro.intro
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
g : ℕ → ℝ
hys : Tendsto g (↑(hyperfilter ℕ)) (𝓝 s)
⊢ ofSeq f < ofSeq g
[PROOFSTEP]
exact ofSeq_lt_ofSeq.2 <| hxr.eventually_lt hys hrs
[GOAL]
x : ℝ*
r s : ℝ
hr : IsSt x r
hs : IsSt x s
⊢ r = s
[PROOFSTEP]
rcases ofSeq_surjective x with ⟨f, rfl⟩
[GOAL]
case intro
r s : ℝ
f : ℕ → ℝ
hr : IsSt (ofSeq f) r
hs : IsSt (ofSeq f) s
⊢ r = s
[PROOFSTEP]
rw [isSt_ofSeq_iff_tendsto] at hr hs
[GOAL]
case intro
r s : ℝ
f : ℕ → ℝ
hr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
hs : Tendsto f (↑(hyperfilter ℕ)) (𝓝 s)
⊢ r = s
[PROOFSTEP]
exact tendsto_nhds_unique hr hs
[GOAL]
x : ℝ*
r : ℝ
hxr : IsSt x r
⊢ st x = r
[PROOFSTEP]
have h : ∃ r, IsSt x r := ⟨r, hxr⟩
[GOAL]
x : ℝ*
r : ℝ
hxr : IsSt x r
h : ∃ r, IsSt x r
⊢ st x = r
[PROOFSTEP]
rw [st, dif_pos h]
[GOAL]
x : ℝ*
r : ℝ
hxr : IsSt x r
h : ∃ r, IsSt x r
⊢ choose h = r
[PROOFSTEP]
exact (Classical.choose_spec h).unique hxr
[GOAL]
x : ℝ*
⊢ st x = sSup {y | ↑y < x}
[PROOFSTEP]
rcases _root_.em (Infinite x) with (hx | hx)
[GOAL]
case inl
x : ℝ*
hx : Infinite x
⊢ st x = sSup {y | ↑y < x}
[PROOFSTEP]
rw [hx.st_eq]
[GOAL]
case inl
x : ℝ*
hx : Infinite x
⊢ 0 = sSup {y | ↑y < x}
[PROOFSTEP]
cases hx with
| inl hx =>
  convert Real.sSup_univ.symm
  exact Set.eq_univ_of_forall hx
| inr hx =>
  convert Real.sSup_empty.symm
  exact Set.eq_empty_of_forall_not_mem fun y hy ↦ hy.out.not_lt (hx _)
[GOAL]
case inl
x : ℝ*
hx : Infinite x
⊢ 0 = sSup {y | ↑y < x}
[PROOFSTEP]
cases hx with
| inl hx =>
  convert Real.sSup_univ.symm
  exact Set.eq_univ_of_forall hx
| inr hx =>
  convert Real.sSup_empty.symm
  exact Set.eq_empty_of_forall_not_mem fun y hy ↦ hy.out.not_lt (hx _)
[GOAL]
case inl.inl
x : ℝ*
hx : InfinitePos x
⊢ 0 = sSup {y | ↑y < x}
[PROOFSTEP]

| inl hx =>
  convert Real.sSup_univ.symm
  exact Set.eq_univ_of_forall hx
[GOAL]
case inl.inl
x : ℝ*
hx : InfinitePos x
⊢ 0 = sSup {y | ↑y < x}
[PROOFSTEP]
convert Real.sSup_univ.symm
[GOAL]
case h.e'_3.h.e'_3
x : ℝ*
hx : InfinitePos x
⊢ {y | ↑y < x} = Set.univ
[PROOFSTEP]
exact Set.eq_univ_of_forall hx
[GOAL]
case inl.inr
x : ℝ*
hx : InfiniteNeg x
⊢ 0 = sSup {y | ↑y < x}
[PROOFSTEP]

| inr hx =>
  convert Real.sSup_empty.symm
  exact Set.eq_empty_of_forall_not_mem fun y hy ↦ hy.out.not_lt (hx _)
[GOAL]
case inl.inr
x : ℝ*
hx : InfiniteNeg x
⊢ 0 = sSup {y | ↑y < x}
[PROOFSTEP]
convert Real.sSup_empty.symm
[GOAL]
case h.e'_3.h.e'_3
x : ℝ*
hx : InfiniteNeg x
⊢ {y | ↑y < x} = ∅
[PROOFSTEP]
exact Set.eq_empty_of_forall_not_mem fun y hy ↦ hy.out.not_lt (hx _)
[GOAL]
case inr
x : ℝ*
hx : ¬Infinite x
⊢ st x = sSup {y | ↑y < x}
[PROOFSTEP]
exact (isSt_sSup hx).st_eq
[GOAL]
x : ℝ*
r : ℝ
hxr : IsSt x r
⊢ IsSt x (st x)
[PROOFSTEP]
rwa [hxr.st_eq]
[GOAL]
r s : ℝ
⊢ IsSt (↑r) s ↔ IsSt (↑s) r
[PROOFSTEP]
rw [isSt_real_iff_eq, isSt_real_iff_eq, eq_comm]
[GOAL]
r s t : ℝ
⊢ IsSt (↑r) s → IsSt (↑s) t → IsSt (↑r) t
[PROOFSTEP]
rw [isSt_real_iff_eq, isSt_real_iff_eq, isSt_real_iff_eq]
[GOAL]
r s t : ℝ
⊢ r = s → s = t → r = t
[PROOFSTEP]
exact Eq.trans
[GOAL]
x : ℝ*
r : ℝ
⊢ IsSt x r ↔ ∀ (δ : ℝ), 0 < δ → |x - ↑r| < ↑δ
[PROOFSTEP]
simp only [abs_sub_lt_iff, sub_lt_iff_lt_add, IsSt, and_comm, add_comm]
[GOAL]
x : ℝ*
r : ℝ
hxr : IsSt x r
f : ℝ → ℝ
hf : ContinuousAt f r
⊢ IsSt (Germ.map f x) (f r)
[PROOFSTEP]
rcases ofSeq_surjective x with ⟨g, rfl⟩
[GOAL]
case intro
r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
g : ℕ → ℝ
hxr : IsSt (ofSeq g) r
⊢ IsSt (Germ.map f (ofSeq g)) (f r)
[PROOFSTEP]
exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (isSt_ofSeq_iff_tendsto.1 hxr)
[GOAL]
x y : ℝ*
r s : ℝ
hxr : IsSt x r
hys : IsSt y s
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
⊢ IsSt (Germ.map₂ f x y) (f r s)
[PROOFSTEP]
rcases ofSeq_surjective x with ⟨x, rfl⟩
[GOAL]
case intro
y : ℝ*
r s : ℝ
hys : IsSt y s
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : IsSt (ofSeq x) r
⊢ IsSt (Germ.map₂ f (ofSeq x) y) (f r s)
[PROOFSTEP]
rcases ofSeq_surjective y with ⟨y, rfl⟩
[GOAL]
case intro.intro
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : IsSt (ofSeq x) r
y : ℕ → ℝ
hys : IsSt (ofSeq y) s
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
[PROOFSTEP]
rw [isSt_ofSeq_iff_tendsto] at hxr hys
[GOAL]
case intro.intro
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Tendsto x (↑(hyperfilter ℕ)) (𝓝 r)
y : ℕ → ℝ
hys : Tendsto y (↑(hyperfilter ℕ)) (𝓝 s)
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
[PROOFSTEP]
exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (hxr.prod_mk_nhds hys)
[GOAL]
x : ℝ*
⊢ Infinite |x| ↔ Infinite x
[PROOFSTEP]
cases le_total 0 x
[GOAL]
case inl
x : ℝ*
h✝ : 0 ≤ x
⊢ Infinite |x| ↔ Infinite x
[PROOFSTEP]
simp [*, abs_of_nonneg, abs_of_nonpos, infinite_neg]
[GOAL]
case inr
x : ℝ*
h✝ : x ≤ 0
⊢ Infinite |x| ↔ Infinite x
[PROOFSTEP]
simp [*, abs_of_nonneg, abs_of_nonpos, infinite_neg]
[GOAL]
x y : ℝ*
⊢ InfinitePos x → ¬InfiniteNeg y → InfinitePos (x + y)
[PROOFSTEP]
intro hip hnin r
[GOAL]
x y : ℝ*
hip : InfinitePos x
hnin : ¬InfiniteNeg y
r : ℝ
⊢ ↑r < x + y
[PROOFSTEP]
cases' not_forall.mp hnin with r₂ hr₂
[GOAL]
case intro
x y : ℝ*
hip : InfinitePos x
hnin : ¬InfiniteNeg y
r r₂ : ℝ
hr₂ : ¬y < ↑r₂
⊢ ↑r < x + y
[PROOFSTEP]
convert add_lt_add_of_lt_of_le (hip (r + -r₂)) (not_lt.mp hr₂) using 1
[GOAL]
case h.e'_3
x y : ℝ*
hip : InfinitePos x
hnin : ¬InfiniteNeg y
r r₂ : ℝ
hr₂ : ¬y < ↑r₂
⊢ ↑r = ↑(r + -r₂) + ↑r₂
[PROOFSTEP]
simp
[GOAL]
x y : ℝ*
⊢ InfiniteNeg x → ¬InfinitePos y → InfiniteNeg (x + y)
[PROOFSTEP]
rw [← infinitePos_neg, ← infinitePos_neg, ← @infiniteNeg_neg y, neg_add]
[GOAL]
x y : ℝ*
⊢ InfinitePos (-x) → ¬InfiniteNeg (-y) → InfinitePos (-x + -y)
[PROOFSTEP]
exact infinitePos_add_not_infiniteNeg
[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop atTop
r : ℝ
hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ f a
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → r + 1 ≤ f a
hi' : ∀ (a : ℕ), f a < r + 1 → a < i
⊢ {a | r < f a}ᶜ ⊆ {a | a ≤ i}
[PROOFSTEP]
simp only [Set.compl_setOf, not_lt]
[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop atTop
r : ℝ
hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ f a
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → r + 1 ≤ f a
hi' : ∀ (a : ℕ), f a < r + 1 → a < i
⊢ {a | f a ≤ r} ⊆ {a | a ≤ i}
[PROOFSTEP]
exact fun a har => le_of_lt (hi' a (lt_of_le_of_lt har (lt_add_one _)))
[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop atBot
r : ℝ
hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → f a ≤ b
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → f a ≤ r - 1
hi' : ∀ (a : ℕ), r - 1 < f a → a < i
⊢ {a | f a < r}ᶜ ⊆ {a | a ≤ i}
[PROOFSTEP]
simp only [Set.compl_setOf, not_lt]
[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop atBot
r : ℝ
hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → f a ≤ b
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → f a ≤ r - 1
hi' : ∀ (a : ℕ), r - 1 < f a → a < i
⊢ {a | r ≤ f a} ⊆ {a | a ≤ i}
[PROOFSTEP]
exact fun a har => le_of_lt (hi' a (lt_of_lt_of_le (sub_one_lt _) har))
[GOAL]
r : ℝ
⊢ ¬Infinite ↑r
[PROOFSTEP]
rw [not_infinite_iff_exist_lt_gt]
[GOAL]
r : ℝ
⊢ ∃ r_1 s, ↑r_1 < ↑r ∧ ↑r < ↑s
[PROOFSTEP]
exact ⟨r - 1, r + 1, coe_lt_coe.2 <| sub_one_lt r, coe_lt_coe.2 <| lt_add_one r⟩
[GOAL]
x : ℝ*
h : Infinite x
⊢ st (-x) = -st x
[PROOFSTEP]
rw [h.st_eq, (infinite_neg.2 h).st_eq, neg_zero]
[GOAL]
x : ℝ*
⊢ Infinitesimal x ↔ ∀ (r : ℝ), 0 < r → -↑r < x ∧ x < ↑r
[PROOFSTEP]
simp [Infinitesimal, IsSt]
[GOAL]
x y : ℝ*
hx : Infinitesimal x
hy : Infinitesimal y
⊢ Infinitesimal (x + y)
[PROOFSTEP]
simpa only [add_zero] using hx.add hy
[GOAL]
x : ℝ*
hx : Infinitesimal x
⊢ Infinitesimal (-x)
[PROOFSTEP]
simpa only [neg_zero] using hx.neg
[GOAL]
x y : ℝ*
hx : Infinitesimal x
hy : Infinitesimal y
⊢ Infinitesimal (x * y)
[PROOFSTEP]
simpa only [mul_zero] using hx.mul hy
[GOAL]
x : ℝ*
r : ℝ
hxr : IsSt x r
⊢ Infinitesimal (x - ↑r)
[PROOFSTEP]
simpa only [sub_self] using hxr.sub (isSt_refl_real r)
[GOAL]
x : ℝ*
hip : InfinitePos x
r : ℝ
hr : 0 < r
⊢ (↑r)⁻¹ < x
[PROOFSTEP]
convert hip r⁻¹
[GOAL]
x : ℝ*
⊢ InfiniteNeg x ↔ Infinitesimal x⁻¹ ∧ x⁻¹ < 0
[PROOFSTEP]
rw [← infinitePos_neg, infinitePos_iff_infinitesimal_inv_pos, inv_neg, neg_pos, infinitesimal_neg]
[GOAL]
x : ℝ*
h0 : x ≠ 0
hi : Infinitesimal x⁻¹
⊢ Infinite x
[PROOFSTEP]
cases' lt_or_gt_of_ne h0 with hn hp
[GOAL]
case inl
x : ℝ*
h0 : x ≠ 0
hi : Infinitesimal x⁻¹
hn : x < 0
⊢ Infinite x
[PROOFSTEP]
exact Or.inr (infiniteNeg_iff_infinitesimal_inv_neg.mpr ⟨hi, inv_lt_zero.mpr hn⟩)
[GOAL]
case inr
x : ℝ*
h0 : x ≠ 0
hi : Infinitesimal x⁻¹
hp : x > 0
⊢ Infinite x
[PROOFSTEP]
exact Or.inl (infinitePos_iff_infinitesimal_inv_pos.mpr ⟨hi, inv_pos.mpr hp⟩)
[GOAL]
x : ℝ*
⊢ Infinitesimal x⁻¹⁻¹ ∧ 0 < x⁻¹⁻¹ ↔ Infinitesimal x ∧ 0 < x
[PROOFSTEP]
rw [inv_inv]
[GOAL]
x : ℝ*
⊢ Infinitesimal x⁻¹⁻¹ ∧ x⁻¹⁻¹ < 0 ↔ Infinitesimal x ∧ x < 0
[PROOFSTEP]
rw [inv_inv]
[GOAL]
x : ℝ*
h : x ≠ 0
⊢ Infinitesimal x ↔ Infinitesimal x⁻¹⁻¹
[PROOFSTEP]
rw [inv_inv]
[GOAL]
x : ℝ*
r : ℝ
hi : ¬Infinitesimal x
hr : IsSt x r
⊢ r ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
x : ℝ*
hi : ¬Infinitesimal x
hr : IsSt x 0
⊢ False
[PROOFSTEP]
exact hi hr
[GOAL]
x : ℝ*
⊢ st x⁻¹ = (st x)⁻¹
[PROOFSTEP]
by_cases h0 : x = 0
[GOAL]
case pos
x : ℝ*
h0 : x = 0
⊢ st x⁻¹ = (st x)⁻¹
case neg x : ℝ* h0 : ¬x = 0 ⊢ st x⁻¹ = (st x)⁻¹
[PROOFSTEP]
rw [h0, inv_zero, ← coe_zero, st_id_real, inv_zero]
[GOAL]
case neg
x : ℝ*
h0 : ¬x = 0
⊢ st x⁻¹ = (st x)⁻¹
[PROOFSTEP]
by_cases h1 : Infinitesimal x
[GOAL]
case pos
x : ℝ*
h0 : ¬x = 0
h1 : Infinitesimal x
⊢ st x⁻¹ = (st x)⁻¹
case neg x : ℝ* h0 : ¬x = 0 h1 : ¬Infinitesimal x ⊢ st x⁻¹ = (st x)⁻¹
[PROOFSTEP]
rw [((infinitesimal_iff_infinite_inv h0).mp h1).st_eq, h1.st_eq, inv_zero]
[GOAL]
case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
⊢ st x⁻¹ = (st x)⁻¹
[PROOFSTEP]
by_cases h2 : Infinite x
[GOAL]
case pos
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
h2 : Infinite x
⊢ st x⁻¹ = (st x)⁻¹
case neg x : ℝ* h0 : ¬x = 0 h1 : ¬Infinitesimal x h2 : ¬Infinite x ⊢ st x⁻¹ = (st x)⁻¹
[PROOFSTEP]
rw [(infinitesimal_inv_of_infinite h2).st_eq, h2.st_eq, inv_zero]
[GOAL]
case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
h2 : ¬Infinite x
⊢ st x⁻¹ = (st x)⁻¹
[PROOFSTEP]
exact ((isSt_st' h2).inv h1).st_eq
[GOAL]
x y : ℝ*
hx : InfinitePos x
hy₁ : ¬Infinitesimal y
hy₂ : 0 < y
r : ℝ
⊢ ↑r < x * y
[PROOFSTEP]
have hy₁' := not_forall.mp (mt infinitesimal_def.2 hy₁)
[GOAL]
x y : ℝ*
hx : InfinitePos x
hy₁ : ¬Infinitesimal y
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
⊢ ↑r < x * y
[PROOFSTEP]
let ⟨r₁, hy₁''⟩ := hy₁'
[GOAL]
x y : ℝ*
hx : InfinitePos x
hy₁ : ¬Infinitesimal y
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
⊢ ↑r < x * y
[PROOFSTEP]
have hyr : 0 < r₁ ∧ ↑r₁ ≤ y := by rwa [not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁''
[GOAL]
x y : ℝ*
hx : InfinitePos x
hy₁ : ¬Infinitesimal y
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
⊢ 0 < r₁ ∧ ↑r₁ ≤ y
[PROOFSTEP]
rwa [not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁''
[GOAL]
x y : ℝ*
hx : InfinitePos x
hy₁ : ¬Infinitesimal y
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
hyr : 0 < r₁ ∧ ↑r₁ ≤ y
⊢ ↑r < x * y
[PROOFSTEP]
rw [← div_mul_cancel r (ne_of_gt hyr.1), coe_mul]
[GOAL]
x y : ℝ*
hx : InfinitePos x
hy₁ : ¬Infinitesimal y
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
hyr : 0 < r₁ ∧ ↑r₁ ≤ y
⊢ ↑(r / r₁) * ↑r₁ < x * y
[PROOFSTEP]
exact mul_lt_mul (hx (r / r₁)) hyr.2 (coe_lt_coe.2 hyr.1) (le_of_lt (hx 0))
[GOAL]
x y : ℝ*
⊢ InfiniteNeg x → ¬Infinitesimal y → y < 0 → InfinitePos (x * y)
[PROOFSTEP]
rw [← infinitePos_neg, ← neg_pos, ← neg_mul_neg, ← infinitesimal_neg]
[GOAL]
x y : ℝ*
⊢ InfinitePos (-x) → ¬Infinitesimal (-y) → 0 < -y → InfinitePos (-x * -y)
[PROOFSTEP]
exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos
[GOAL]
x y : ℝ*
⊢ InfinitePos x → ¬Infinitesimal y → y < 0 → InfiniteNeg (x * y)
[PROOFSTEP]
rw [← infinitePos_neg, ← neg_pos, neg_mul_eq_mul_neg, ← infinitesimal_neg]
[GOAL]
x y : ℝ*
⊢ InfinitePos x → ¬Infinitesimal (-y) → 0 < -y → InfinitePos (x * -y)
[PROOFSTEP]
exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos
[GOAL]
x y : ℝ*
⊢ InfiniteNeg x → ¬Infinitesimal y → 0 < y → InfiniteNeg (x * y)
[PROOFSTEP]
rw [← infinitePos_neg, ← infinitePos_neg, neg_mul_eq_neg_mul]
[GOAL]
x y : ℝ*
⊢ InfinitePos (-x) → ¬Infinitesimal y → 0 < y → InfinitePos (-x * y)
[PROOFSTEP]
exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos
[GOAL]
x y : ℝ*
hx : ¬Infinitesimal x
hp : 0 < x
hy : InfiniteNeg y
⊢ InfiniteNeg (x * y)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
x y : ℝ*
hx : ¬Infinitesimal x
hp : 0 < x
hy : InfiniteNeg y
⊢ InfiniteNeg (y * x)
[PROOFSTEP]
exact infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos hy hx hp
[GOAL]
x y : ℝ*
hx : ¬Infinitesimal x
hy : Infinite y
⊢ Infinite (x * y)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
x y : ℝ*
hx : ¬Infinitesimal x
hy : Infinite y
⊢ Infinite (y * x)
[PROOFSTEP]
exact infinite_mul_of_infinite_not_infinitesimal hy hx


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
⊢ List.length (List.zipWith f ↑x ↑y) = n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
i : Fin n
⊢ get (zipWith f x y) i = f (get x i) (get y i)
[PROOFSTEP]
dsimp only [Vector.zipWith, Vector.get]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
i : Fin n
⊢ List.nthLe (List.zipWith f ↑x ↑y) ↑i (_ : ↑i < List.length (List.zipWith f ↑x ↑y)) =
    f
      (match x, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
      (match y, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
y : Vector β n
i : Fin n
val✝ : List α
property✝ : List.length val✝ = n
⊢ List.nthLe (List.zipWith f ↑{ val := val✝, property := property✝ } ↑y) ↑i
      (_ : ↑i < List.length (List.zipWith f ↑{ val := val✝, property := property✝ } ↑y)) =
    f
      (match { val := val✝, property := property✝ }, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
      (match y, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
i : Fin n
val✝¹ : List α
property✝¹ : List.length val✝¹ = n
val✝ : List β
property✝ : List.length val✝ = n
⊢ List.nthLe (List.zipWith f ↑{ val := val✝¹, property := property✝¹ } ↑{ val := val✝, property := property✝ }) ↑i
      (_ :
        ↑i <
          List.length
            (List.zipWith f ↑{ val := val✝¹, property := property✝¹ } ↑{ val := val✝, property := property✝ })) =
    f
      (match { val := val✝¹, property := property✝¹ }, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
      (match { val := val✝, property := property✝ }, i with
      | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l))
[PROOFSTEP]
simp only [List.nthLe_zipWith]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
⊢ tail (zipWith f x y) = zipWith f (tail x) (tail y)
[PROOFSTEP]
ext
[GOAL]
case x
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
m✝ : Fin (n - 1)
⊢ get (tail (zipWith f x y)) m✝ = get (zipWith f (tail x) (tail y)) m✝
[PROOFSTEP]
simp [get_tail]