Theorem: Finset.Ioc_diff_Ioc (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
⊢ Ioc a b = Ioc a c \ Ioc b c
Tactic:
ext x
State after:
case a
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ x ∈ Ioc a b ↔ x ∈ Ioc a c \ Ioc b c

State before:
case a
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ x ∈ Ioc a b ↔ x ∈ Ioc a c \ Ioc b c
Tactic:
simp only [mem_Ioc, mem_sdiff, not_and, not_le]
State after:
case a
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ a < x ∧ x ≤ b ↔ (a < x ∧ x ≤ c) ∧ (b < x → c < x)

State before:
case a
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ a < x ∧ x ≤ b ↔ (a < x ∧ x ≤ c) ∧ (b < x → c < x)
Tactic:
constructor
State after:
case a.mp
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ a < x ∧ x ≤ b → (a < x ∧ x ≤ c) ∧ (b < x → c < x)

case a.mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ (a < x ∧ x ≤ c) ∧ (b < x → c < x) → a < x ∧ x ≤ b

State before:
case a.mp
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ a < x ∧ x ≤ b → (a < x ∧ x ≤ c) ∧ (b < x → c < x)
Tactic:
refine fun ⟨h₁, h₂⟩ ↦ ⟨⟨h₁, le_trans h₂ (mem_Icc.mp hb).2⟩, by contrapose! h₂; exact h₂.1⟩
State after:
no goals

State before:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : a < x ∧ x ≤ b
h₁ : a < x
h₂ : x ≤ b
⊢ b < x → c < x
Tactic:
contrapose! h₂
State after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : a < x ∧ x ≤ b
h₁ : a < x
h₂ : b < x ∧ x ≤ c
⊢ b < x

State before:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : a < x ∧ x ≤ b
h₁ : a < x
h₂ : b < x ∧ x ≤ c
⊢ b < x
Tactic:
exact h₂.1
State after:
no goals

State before:
case a.mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ (a < x ∧ x ≤ c) ∧ (b < x → c < x) → a < x ∧ x ≤ b
Tactic:
exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.1, by contrapose! h₂; exact ⟨h₂, h₁.2⟩⟩
State after:
no goals

State before:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : (a < x ∧ x ≤ c) ∧ (b < x → c < x)
h₁ : a < x ∧ x ≤ c
h₂ : b < x → c < x
⊢ x ≤ b
Tactic:
contrapose! h₂
State after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : (a < x ∧ x ≤ c) ∧ (b < x → c < x)
h₁ : a < x ∧ x ≤ c
h₂ : b < x
⊢ b < x ∧ x ≤ c

State before:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : (a < x ∧ x ≤ c) ∧ (b < x → c < x)
h₁ : a < x ∧ x ≤ c
h₂ : b < x
⊢ b < x ∧ x ≤ c
Tactic:
exact ⟨h₂, h₁.2⟩
State after:
no goals