Theorem: uIcc_subsets (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a b c : ℝ
hc : c ∈ Icc a b
⊢ [[a, c]] ⊆ [[a, b]] ∧ [[c, b]] ⊆ [[a, b]]
Tactic:
constructor <;> rw [uIcc_of_le ?_, uIcc_of_le ?_]
State after:
case left
a b c : ℝ
hc : c ∈ Icc a b
⊢ Icc a c ⊆ Icc a b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ c

case right
a b c : ℝ
hc : c ∈ Icc a b
⊢ Icc c b ⊆ Icc a b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ c ≤ b

State before:
case left
a b c : ℝ
hc : c ∈ Icc a b
⊢ Icc a c ⊆ Icc a b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ c

case right
a b c : ℝ
hc : c ∈ Icc a b
⊢ Icc c b ⊆ Icc a b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ c ≤ b
Tactic:
any_goals apply Icc_subset_Icc
State after:
case left.h₁
a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ a

case left.h₂
a b c : ℝ
hc : c ∈ Icc a b
⊢ c ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ c

case right.h₁
a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ c

case right.h₂
a b c : ℝ
hc : c ∈ Icc a b
⊢ b ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ c ≤ b

State before:
case left.h₁
a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ a

case left.h₂
a b c : ℝ
hc : c ∈ Icc a b
⊢ c ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ c

case right.h₁
a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ c

case right.h₂
a b c : ℝ
hc : c ∈ Icc a b
⊢ b ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ b

a b c : ℝ
hc : c ∈ Icc a b
⊢ c ≤ b
Tactic:
all_goals linarith [hc.1, hc.2]
State after:
no goals

State before:
case right
a b c : ℝ
hc : c ∈ Icc a b
⊢ Icc c b ⊆ Icc a b
Tactic:
apply Icc_subset_Icc
State after:
case right.h₁
a b c : ℝ
hc : c ∈ Icc a b
⊢ a ≤ c

case right.h₂
a b c : ℝ
hc : c ∈ Icc a b
⊢ b ≤ b

State before:
a b c : ℝ
hc : c ∈ Icc a b
⊢ c ≤ b
Tactic:
linarith [hc.1, hc.2]
State after:
no goals