case mp
E : Type ?u.34598
F : Type ?u.34601
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]]

case mpr
E : Type ?u.34598
F : Type ?u.34601
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
E : Type ?u.34598
F : Type ?u.34601
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]]
constructor
case mp
E : Type ?u.34598
F : Type ?u.34601
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
case mp
E : Type ?u.34598
F : Type ?u.34601
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]]
refine' fun h => or_iff_not_imp_left.2 fun hne hc => _
no goals
case mp
E : Type ?u.34598
F : Type ?u.34601
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
exact not_intervalIntegrable_of_sub_inv_isBigO_punctured (isBigO_refl _ _) hne hc h
case mpr.inl
E : Type ?u.34598
F : Type ?u.34601
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

case mpr.inr
E : Type ?u.34598
F : Type ?u.34601
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
case mpr
E : Type ?u.34598
F : Type ?u.34601
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
rintro (rfl | h₀)
case mpr.inr
E : Type ?u.34598
F : Type ?u.34601
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
case mpr.inr
E : Type ?u.34598
F : Type ?u.34601
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
refine' ((continuous_sub_right c).continuousOn.inv₀ _).intervalIntegrable
no goals
case mpr.inr
E : Type ?u.34598
F : Type ?u.34601
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
exact fun x hx => sub_ne_zero.2 <| ne_of_mem_of_not_mem hx h₀
no goals
case mpr.inl
E : Type ?u.34598
F : Type ?u.34601
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
exact IntervalIntegrable.refl