[GOAL]
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
⊢ ¬IntervalIntegrable g volume a b
[PROOFSTEP]
intro hgi
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
⊢ False
[PROOFSTEP]
obtain ⟨C, hC₀, s, hsl, hsub, hfd, hg⟩ :
  ∃ (C : ℝ) (_ : 0 ≤ C),
    ∃ s ∈ l,
      (∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ [[a, b]]) ∧
        (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z) ∧
          ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖ :=
  by
  rcases hfg.exists_nonneg with ⟨C, C₀, hC⟩
  have h :
    ∀ᶠ x : ℝ × ℝ in l.prod l, ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ [[a, b]] :=
    (tendsto_fst.uIcc tendsto_snd).eventually ((hd.and hC.bound).and hl).smallSets
  rcases mem_prod_self_iff.1 h with ⟨s, hsl, hs⟩
  simp only [prod_subset_iff, mem_setOf_eq] at hs
  exact
    ⟨C, C₀, s, hsl, fun x hx y hy z hz => (hs x hx y hy z hz).2, fun x hx y hy z hz => (hs x hx y hy z hz).1.1,
      fun x hx y hy z hz => (hs x hx y hy z hz).1.2⟩
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
⊢ ∃ C x s,
    s ∈ l ∧
      (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]) ∧
        (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z) ∧
          ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
[PROOFSTEP]
rcases hfg.exists_nonneg with ⟨C, C₀, hC⟩
[GOAL]
case intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
C : ℝ
C₀ : 0 ≤ C
hC : IsBigOWith C l (deriv f) g
⊢ ∃ C x s,
    s ∈ l ∧
      (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]) ∧
        (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z) ∧
          ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
[PROOFSTEP]
have h :
  ∀ᶠ x : ℝ × ℝ in l.prod l, ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ [[a, b]] :=
  (tendsto_fst.uIcc tendsto_snd).eventually ((hd.and hC.bound).and hl).smallSets
[GOAL]
case intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
C : ℝ
C₀ : 0 ≤ C
hC : IsBigOWith C l (deriv f) g
h :
  ∀ᶠ (x : ℝ × ℝ) in Filter.prod l l,
    ∀ (y : ℝ), y ∈ [[x.fst, x.snd]] → (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ [[a, b]]
⊢ ∃ C x s,
    s ∈ l ∧
      (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]) ∧
        (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z) ∧
          ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
[PROOFSTEP]
rcases mem_prod_self_iff.1 h with ⟨s, hsl, hs⟩
[GOAL]
case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
C : ℝ
C₀ : 0 ≤ C
hC : IsBigOWith C l (deriv f) g
h :
  ∀ᶠ (x : ℝ × ℝ) in Filter.prod l l,
    ∀ (y : ℝ), y ∈ [[x.fst, x.snd]] → (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ [[a, b]]
s : Set ℝ
hsl : s ∈ l
hs :
  s ×ˢ s ⊆
    {x |
      (fun x => ∀ (y : ℝ), y ∈ [[x.fst, x.snd]] → (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ [[a, b]]) x}
⊢ ∃ C x s,
    s ∈ l ∧
      (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]) ∧
        (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z) ∧
          ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
[PROOFSTEP]
simp only [prod_subset_iff, mem_setOf_eq] at hs
[GOAL]
case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
C : ℝ
C₀ : 0 ≤ C
hC : IsBigOWith C l (deriv f) g
h :
  ∀ᶠ (x : ℝ × ℝ) in Filter.prod l l,
    ∀ (y : ℝ), y ∈ [[x.fst, x.snd]] → (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ [[a, b]]
s : Set ℝ
hsl : s ∈ l
hs :
  ∀ (x : ℝ),
    x ∈ s →
      ∀ (y : ℝ),
        y ∈ s → ∀ (y_1 : ℝ), y_1 ∈ [[x, y]] → (DifferentiableAt ℝ f y_1 ∧ ‖deriv f y_1‖ ≤ C * ‖g y_1‖) ∧ y_1 ∈ [[a, b]]
⊢ ∃ C x s,
    s ∈ l ∧
      (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]) ∧
        (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z) ∧
          ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
[PROOFSTEP]
exact
  ⟨C, C₀, s, hsl, fun x hx y hy z hz => (hs x hx y hy z hz).2, fun x hx y hy z hz => (hs x hx y hy z hz).1.1,
    fun x hx y hy z hz => (hs x hx y hy z hz).1.2⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
⊢ False
[PROOFSTEP]
replace hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
[GOAL]
case hgi
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
⊢ IntervalIntegrable (fun x => C * ‖g x‖) volume a b
[PROOFSTEP]
convert hgi.norm.smul C using 1
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
⊢ False
[PROOFSTEP]
obtain ⟨c, hc, d, hd, hlt⟩ : ∃ c ∈ s, ∃ d ∈ s, (‖f c‖ + ∫ y in Ι a b, C * ‖g y‖) < ‖f d‖ :=
  by
  rcases Filter.nonempty_of_mem hsl with ⟨c, hc⟩
  have : ∀ᶠ x in l, (‖f c‖ + ∫ y in Ι a b, C * ‖g y‖) < ‖f x‖ := hf.eventually (eventually_gt_atTop _)
  exact ⟨c, hc, (this.and hsl).exists.imp fun d hd => ⟨hd.2, hd.1⟩⟩
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
⊢ ∃ c, c ∈ s ∧ ∃ d, d ∈ s ∧ ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
[PROOFSTEP]
rcases Filter.nonempty_of_mem hsl with ⟨c, hc⟩
[GOAL]
case intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
⊢ ∃ c, c ∈ s ∧ ∃ d, d ∈ s ∧ ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
[PROOFSTEP]
have : ∀ᶠ x in l, (‖f c‖ + ∫ y in Ι a b, C * ‖g y‖) < ‖f x‖ := hf.eventually (eventually_gt_atTop _)
[GOAL]
case intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
this : ∀ᶠ (x : ℝ) in l, ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f x‖
⊢ ∃ c, c ∈ s ∧ ∃ d, d ∈ s ∧ ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
[PROOFSTEP]
exact ⟨c, hc, (this.and hsl).exists.imp fun d hd => ⟨hd.2, hd.1⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
⊢ False
[PROOFSTEP]
specialize hsub c hc d hd
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
⊢ False
[PROOFSTEP]
specialize hfd c hc d hd
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
⊢ False
[PROOFSTEP]
replace hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
[GOAL]
case hg
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
⊢ ∀ (x : ℝ), x ∈ Ι c d → ‖deriv f x‖ ≤ C * ‖g x‖
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ Ι c d → ‖deriv f x‖ ≤ C * ‖g x‖
⊢ False
[PROOFSTEP]
exact fun z hz => hg c hc d hd z ⟨hz.1.le, hz.2⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ Ι c d → ‖deriv f x‖ ≤ C * ‖g x‖
⊢ False
[PROOFSTEP]
have hg_ae : ∀ᵐ x ∂volume.restrict (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖ := (ae_restrict_mem measurableSet_uIoc).mono hg
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ Ι c d → ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
⊢ False
[PROOFSTEP]
have hsub' : Ι c d ⊆ Ι a b := uIoc_subset_uIoc_of_uIcc_subset_uIcc hsub
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ Ι c d → ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ Ι a b
⊢ False
[PROOFSTEP]
have hfi : IntervalIntegrable (deriv f) volume c d :=
  (hgi.mono_set hsub).mono_fun' (aestronglyMeasurable_deriv _ _) hg_ae
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ Ι c d → ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ Ι a b
hfi : IntervalIntegrable (deriv f) volume c d
⊢ False
[PROOFSTEP]
refine' hlt.not_le (sub_le_iff_le_add'.1 _)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ Ι c d → ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ Ι a b
hfi : IntervalIntegrable (deriv f) volume c d
⊢ ‖f d‖ - ‖f c‖ ≤ ∫ (y : ℝ) in Ι a b, C * ‖g y‖
[PROOFSTEP]
calc
  ‖f d‖ - ‖f c‖ ≤ ‖f d - f c‖ := norm_sub_norm_le _ _
  _ = ‖∫ x in c..d, deriv f x‖ := (congr_arg _ (integral_deriv_eq_sub hfd hfi).symm)
  _ = ‖∫ x in Ι c d, deriv f x‖ := (norm_integral_eq_norm_integral_Ioc _)
  _ ≤ ∫ x in Ι c d, ‖deriv f x‖ := (norm_integral_le_integral_norm _)
  _ ≤ ∫ x in Ι c d, C * ‖g x‖ := (set_integral_mono_on hfi.norm.def (hgi.def.mono_set hsub') measurableSet_uIoc hg)
  _ ≤ ∫ x in Ι a b, C * ‖g x‖ :=
    set_integral_mono_set hgi.def (ae_of_all _ fun x => mul_nonneg hC₀ (norm_nonneg _)) hsub'.eventuallyLE
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
⊢ ¬IntervalIntegrable g volume a b
[PROOFSTEP]
obtain ⟨l, hl, hl', hle, hmem⟩ : ∃ l : Filter ℝ, TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ { c } ∈ l :=
  by
  cases' (min_lt_max.2 hne).lt_or_lt c with hlt hlt
  · refine' ⟨𝓝[<] c, inferInstance, inferInstance, inf_le_left, _⟩
    rw [← Iic_diff_right]
    exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsWithin_Iic ⟨hlt, hc.2⟩) _
  · refine' ⟨𝓝[>] c, inferInstance, inferInstance, inf_le_left, _⟩
    rw [← Ici_diff_left]
    exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsWithin_Ici ⟨hc.1, hlt⟩) _
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
⊢ ∃ l, TendstoIxxClass Icc l l ∧ NeBot l ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
[PROOFSTEP]
cases' (min_lt_max.2 hne).lt_or_lt c with hlt hlt
[GOAL]
case inl
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
⊢ ∃ l, TendstoIxxClass Icc l l ∧ NeBot l ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
[PROOFSTEP]
refine' ⟨𝓝[<] c, inferInstance, inferInstance, inf_le_left, _⟩
[GOAL]
case inl
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
⊢ [[a, b]] \ {c} ∈ 𝓝[Iio c] c
[PROOFSTEP]
rw [← Iic_diff_right]
[GOAL]
case inl
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
⊢ [[a, b]] \ {c} ∈ 𝓝[Iic c \ {c}] c
[PROOFSTEP]
exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsWithin_Iic ⟨hlt, hc.2⟩) _
[GOAL]
case inr
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
⊢ ∃ l, TendstoIxxClass Icc l l ∧ NeBot l ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
[PROOFSTEP]
refine' ⟨𝓝[>] c, inferInstance, inferInstance, inf_le_left, _⟩
[GOAL]
case inr
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
⊢ [[a, b]] \ {c} ∈ 𝓝[Ioi c] c
[PROOFSTEP]
rw [← Ici_diff_left]
[GOAL]
case inr
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
⊢ [[a, b]] \ {c} ∈ 𝓝[Ici c \ {c}] c
[PROOFSTEP]
exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsWithin_Ici ⟨hc.1, hlt⟩) _
[GOAL]
case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
l : Filter ℝ
hl : TendstoIxxClass Icc l l
hl' : NeBot l
hle : l ≤ 𝓝 c
hmem : [[a, b]] \ {c} ∈ l
⊢ ¬IntervalIntegrable g volume a b
[PROOFSTEP]
have : l ≤ 𝓝[[[a, b]] \ { c }] c := le_inf hle (le_principal_iff.2 hmem)
[GOAL]
case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
l : Filter ℝ
hl : TendstoIxxClass Icc l l
hl' : NeBot l
hle : l ≤ 𝓝 c
hmem : [[a, b]] \ {c} ∈ l
this : l ≤ 𝓝[[[a, b]] \ {c}] c
⊢ ¬IntervalIntegrable g volume a b
[PROOFSTEP]
exact
  not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter l (mem_of_superset hmem (diff_subset _ _))
    (h_deriv.filter_mono this) (h_infty.mono_left this) (hg.mono this)
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
⊢ ¬IntervalIntegrable f volume a b
[PROOFSTEP]
have A : ∀ᶠ x in 𝓝[≠] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x :=
  by
  filter_upwards [self_mem_nhdsWithin] with x hx
  simpa using ((hasDerivAt_id x).sub_const c).log (sub_ne_zero.2 hx)
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
⊢ ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin] with x hx
[GOAL]
case h
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
x : ℝ
hx : x ∈ {c}ᶜ
⊢ HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
[PROOFSTEP]
simpa using ((hasDerivAt_id x).sub_const c).log (sub_ne_zero.2 hx)
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
⊢ ¬IntervalIntegrable f volume a b
[PROOFSTEP]
have B : Tendsto (fun x => ‖Real.log (x - c)‖) (𝓝[≠] c) atTop :=
  by
  refine' tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsWithin_zero.comp _)
  rw [← sub_self c]
  exact ((hasDerivAt_id c).sub_const c).tendsto_punctured_nhds one_ne_zero
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (fun x => ‖Real.log (x - c)‖) (𝓝[{c}ᶜ] c) atTop
[PROOFSTEP]
refine' tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsWithin_zero.comp _)
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (fun x => x - c) (𝓝[{c}ᶜ] c) (𝓝[{0}ᶜ] 0)
[PROOFSTEP]
rw [← sub_self c]
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (fun x => x - c) (𝓝[{c}ᶜ] c) (𝓝[{c - c}ᶜ] (c - c))
[PROOFSTEP]
exact ((hasDerivAt_id c).sub_const c).tendsto_punctured_nhds one_ne_zero
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
B : Tendsto (fun x => ‖Real.log (x - c)‖) (𝓝[{c}ᶜ] c) atTop
⊢ ¬IntervalIntegrable f volume a b
[PROOFSTEP]
exact
  not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured (A.mono fun x hx => hx.differentiableAt) B
    (hf.congr' (A.mono fun x hx => hx.deriv.symm) EventuallyEq.rfl) hne hc
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b c : ℝ
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a b ↔ a = b ∨ ¬c ∈ [[a, b]]
[PROOFSTEP]
constructor
[GOAL]
case mp
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b c : ℝ
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a b → a = b ∨ ¬c ∈ [[a, b]]
[PROOFSTEP]
refine' fun h => or_iff_not_imp_left.2 fun hne hc => _
[GOAL]
case mp
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b c : ℝ
h : IntervalIntegrable (fun x => (x - c)⁻¹) volume a b
hne : ¬a = b
hc : c ∈ [[a, b]]
⊢ False
[PROOFSTEP]
exact not_intervalIntegrable_of_sub_inv_isBigO_punctured (isBigO_refl _ _) hne hc h
[GOAL]
case mpr
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b c : ℝ
⊢ a = b ∨ ¬c ∈ [[a, b]] → IntervalIntegrable (fun x => (x - c)⁻¹) volume a b
[PROOFSTEP]
rintro (rfl | h₀)
[GOAL]
case mpr.inl
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a c : ℝ
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a a
[PROOFSTEP]
exact IntervalIntegrable.refl
[GOAL]
case mpr.inr
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b c : ℝ
h₀ : ¬c ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a b
[PROOFSTEP]
refine' ((continuous_sub_right c).continuousOn.inv₀ _).intervalIntegrable
[GOAL]
case mpr.inr
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b c : ℝ
h₀ : ¬c ∈ [[a, b]]
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → x - c ≠ 0
[PROOFSTEP]
exact fun x hx => sub_ne_zero.2 <| ne_of_mem_of_not_mem hx h₀
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b : ℝ
⊢ IntervalIntegrable (fun x => x⁻¹) volume a b ↔ a = b ∨ ¬0 ∈ [[a, b]]
[PROOFSTEP]
simp only [← intervalIntegrable_sub_inv_iff, sub_zero]


[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
⊢ ↑(convexHull 𝕜) ↑s ⊆ space K
[PROOFSTEP]
convert subset_biUnion_of_mem hs
[GOAL]
case h.e'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
⊢ ↑(convexHull 𝕜) ↑s = ↑(convexHull 𝕜) ↑s
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
⊢ Disjoint (↑(convexHull 𝕜) ↑s) (↑(convexHull 𝕜) ↑t) ∨
    ∃ u, u ∈ K.faces ∧ ↑(convexHull 𝕜) ↑s ∩ ↑(convexHull 𝕜) ↑t = ↑(convexHull 𝕜) ↑u
[PROOFSTEP]
classical
by_contra' h
refine'
  h.2 (s ∩ t)
    (K.down_closed hs (inter_subset_left _ _) fun hst =>
      h.1 <| disjoint_iff_inf_le.mpr <| (K.inter_subset_convexHull hs ht).trans _)
    _
· rw [← coe_inter, hst, coe_empty, convexHull_empty]
  rfl
· rw [coe_inter, convexHull_inter_convexHull hs ht]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
⊢ Disjoint (↑(convexHull 𝕜) ↑s) (↑(convexHull 𝕜) ↑t) ∨
    ∃ u, u ∈ K.faces ∧ ↑(convexHull 𝕜) ↑s ∩ ↑(convexHull 𝕜) ↑t = ↑(convexHull 𝕜) ↑u
[PROOFSTEP]
by_contra' h
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint (↑(convexHull 𝕜) ↑s) (↑(convexHull 𝕜) ↑t) ∧
    ∀ (u : Finset E), u ∈ K.faces → ↑(convexHull 𝕜) ↑s ∩ ↑(convexHull 𝕜) ↑t ≠ ↑(convexHull 𝕜) ↑u
⊢ False
[PROOFSTEP]
refine'
  h.2 (s ∩ t)
    (K.down_closed hs (inter_subset_left _ _) fun hst =>
      h.1 <| disjoint_iff_inf_le.mpr <| (K.inter_subset_convexHull hs ht).trans _)
    _
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint (↑(convexHull 𝕜) ↑s) (↑(convexHull 𝕜) ↑t) ∧
    ∀ (u : Finset E), u ∈ K.faces → ↑(convexHull 𝕜) ↑s ∩ ↑(convexHull 𝕜) ↑t ≠ ↑(convexHull 𝕜) ↑u
hst : s ∩ t = ∅
⊢ ↑(convexHull 𝕜) (↑s ∩ ↑t) ⊆ ⊥
[PROOFSTEP]
rw [← coe_inter, hst, coe_empty, convexHull_empty]
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint (↑(convexHull 𝕜) ↑s) (↑(convexHull 𝕜) ↑t) ∧
    ∀ (u : Finset E), u ∈ K.faces → ↑(convexHull 𝕜) ↑s ∩ ↑(convexHull 𝕜) ↑t ≠ ↑(convexHull 𝕜) ↑u
hst : s ∩ t = ∅
⊢ ∅ ⊆ ⊥
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint (↑(convexHull 𝕜) ↑s) (↑(convexHull 𝕜) ↑t) ∧
    ∀ (u : Finset E), u ∈ K.faces → ↑(convexHull 𝕜) ↑s ∩ ↑(convexHull 𝕜) ↑t ≠ ↑(convexHull 𝕜) ↑u
⊢ ↑(convexHull 𝕜) ↑s ∩ ↑(convexHull 𝕜) ↑t = ↑(convexHull 𝕜) ↑(s ∩ t)
[PROOFSTEP]
rw [coe_inter, convexHull_inter_convexHull hs ht]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
⊢ vertices K = ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x✝ x : E
⊢ x ∈ vertices K ↔ x ∈ ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
[PROOFSTEP]
refine' ⟨fun h => mem_biUnion h <| mem_coe.2 <| mem_singleton_self x, fun h => _⟩
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x✝ x : E
h : x ∈ ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
⊢ x ∈ vertices K
[PROOFSTEP]
obtain ⟨s, hs, hx⟩ := mem_iUnion₂.1 h
[GOAL]
case h.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
x✝ x : E
h : x ∈ ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
s : Finset E
hs : s ∈ K.faces
hx : x ∈ ↑s
⊢ x ∈ vertices K
[PROOFSTEP]
exact K.down_closed hs (Finset.singleton_subset_iff.2 <| mem_coe.1 hx) (singleton_ne_empty _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
⊢ x ∈ ↑(convexHull 𝕜) ↑s ↔ x ∈ s
[PROOFSTEP]
refine' ⟨fun h => _, fun h => subset_convexHull 𝕜 _ h⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h : x ∈ ↑(convexHull 𝕜) ↑s
⊢ x ∈ s
[PROOFSTEP]
classical
have h := K.inter_subset_convexHull hx hs ⟨by simp, h⟩
by_contra H
rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm, coe_empty,
  convexHull_empty] at h
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h : x ∈ ↑(convexHull 𝕜) ↑s
⊢ x ∈ s
[PROOFSTEP]
have h := K.inter_subset_convexHull hx hs ⟨by simp, h⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h : x ∈ ↑(convexHull 𝕜) ↑s
⊢ x ∈ ↑(convexHull 𝕜) ↑{x}
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h✝ : x ∈ ↑(convexHull 𝕜) ↑s
h : x ∈ ↑(convexHull 𝕜) (↑{x} ∩ ↑s)
⊢ x ∈ s
[PROOFSTEP]
by_contra H
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h✝ : x ∈ ↑(convexHull 𝕜) ↑s
h : x ∈ ↑(convexHull 𝕜) (↑{x} ∩ ↑s)
H : ¬x ∈ s
⊢ False
[PROOFSTEP]
rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm, coe_empty,
  convexHull_empty] at h
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
⊢ ¬s ∈ facets K ↔ ∃ t, t ∈ K.faces ∧ s ⊂ t
[PROOFSTEP]
refine' ⟨fun hs' : ¬(_ ∧ _) => _, _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
hs' : ¬(s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t)
⊢ ∃ t, t ∈ K.faces ∧ s ⊂ t
[PROOFSTEP]
push_neg at hs'
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
hs' : s ∈ K.faces → Exists fun ⦃t⦄ => t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, t ∈ K.faces ∧ s ⊂ t
[PROOFSTEP]
obtain ⟨t, ht⟩ := hs' hs
[GOAL]
case refine'_1.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs : s ∈ K.faces
hs' : s ∈ K.faces → Exists fun ⦃t⦄ => t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
t : Finset E
ht : t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, t ∈ K.faces ∧ s ⊂ t
[PROOFSTEP]
exact ⟨t, ht.1, ⟨ht.2.1, fun hts => ht.2.2 (Subset.antisymm ht.2.1 hts)⟩⟩
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
⊢ (∃ t, t ∈ K.faces ∧ s ⊂ t) → ¬s ∈ facets K
[PROOFSTEP]
rintro ⟨t, ht⟩ ⟨hs, hs'⟩
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs✝ : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ s ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
⊢ False
[PROOFSTEP]
have := hs' ht.1 ht.2.1
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs✝ : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ s ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
this : s = t
⊢ False
[PROOFSTEP]
rw [this] at ht
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs✝ : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ t ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
this : s = t
⊢ False
[PROOFSTEP]
exact ht.2.2 (Subset.refl t)