α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
⊢ (∃ k,
      (∀ {x : β}, k < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)) ∧
        (∀ (x : α), x ∈ A → ¬f x = k) ∧ ∃ a, a ∈ B ∧ f a = k) ↔
    ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
⊢ toColex (image f A) < toColex (image f B) ↔ toColex A < toColex B
simp only [Colex.lt_def, not_exists, mem_image, exists_prop, not_and]
case mp
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
⊢ (∃ k,
      (∀ {x : β}, k < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)) ∧
        (∀ (x : α), x ∈ A → ¬f x = k) ∧ ∃ a, a ∈ B ∧ f a = k) →
    ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B

case mpr
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
⊢ (∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B) →
    ∃ k,
      (∀ {x : β}, k < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)) ∧
        (∀ (x : α), x ∈ A → ¬f x = k) ∧ ∃ a, a ∈ B ∧ f a = k
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
⊢ (∃ k,
      (∀ {x : β}, k < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)) ∧
        (∀ (x : α), x ∈ A → ¬f x = k) ∧ ∃ a, a ∈ B ∧ f a = k) ↔
    ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
constructor
case mpr.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
⊢ ∃ k,
    (∀ {x : β}, k < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)) ∧
      (∀ (x : α), x ∈ A → ¬f x = k) ∧ ∃ a, a ∈ B ∧ f a = k
case mpr
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
⊢ (∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B) →
    ∃ k,
      (∀ {x : β}, k < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)) ∧
        (∀ (x : α), x ∈ A → ¬f x = k) ∧ ∃ a, a ∈ B ∧ f a = k
rintro ⟨k, z, ka, _⟩
case mpr.intro.intro.intro.refine'_1
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x : β
hx : f k < x
⊢ (∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x

case mpr.intro.intro.intro.refine'_2
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
⊢ ∀ (x : α), x ∈ A → ¬f x = f k
case mpr.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
⊢ ∃ k,
    (∀ {x : β}, k < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)) ∧
      (∀ (x : α), x ∈ A → ¬f x = k) ∧ ∃ a, a ∈ B ∧ f a = k
refine' ⟨f k, @fun x hx => _, _, k, ‹k ∈ B›, rfl⟩
case mp.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k' : α
left✝ : k' ∈ B
z : ∀ {x : β}, f k' < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)
q : ∀ (x : α), x ∈ A → ¬f x = f k'
⊢ ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
case mp
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
⊢ (∃ k,
      (∀ {x : β}, k < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)) ∧
        (∀ (x : α), x ∈ A → ¬f x = k) ∧ ∃ a, a ∈ B ∧ f a = k) →
    ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
rintro ⟨k, z, q, k', _, rfl⟩
no goals
case mp.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k' : α
left✝ : k' ∈ B
z : ∀ {x : β}, f k' < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)
q : ∀ (x : α), x ∈ A → ¬f x = f k'
⊢ ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
exact
  ⟨k', @fun x hx => by
    simpa [h₁.injective.eq_iff] using z (h₁ hx), fun t => q _ t rfl, ‹k' ∈ B›⟩
no goals
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k' : α
left✝ : k' ∈ B
z : ∀ {x : β}, f k' < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)
q : ∀ (x : α), x ∈ A → ¬f x = f k'
x : α
hx : k' < x
⊢ x ∈ A ↔ x ∈ B
simpa [h₁.injective.eq_iff] using z (h₁ hx)
case mpr.intro.intro.intro.refine'_1.mp
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x : β
hx : f k < x
⊢ (∃ a, a ∈ A ∧ f a = x) → ∃ a, a ∈ B ∧ f a = x

case mpr.intro.intro.intro.refine'_1.mpr
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x : β
hx : f k < x
⊢ (∃ a, a ∈ B ∧ f a = x) → ∃ a, a ∈ A ∧ f a = x
case mpr.intro.intro.intro.refine'_1
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x : β
hx : f k < x
⊢ (∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x
constructor
no goals
case mpr.intro.intro.intro.refine'_1.mp
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x : β
hx : f k < x
⊢ (∃ a, a ∈ A ∧ f a = x) → ∃ a, a ∈ B ∧ f a = x

case mpr.intro.intro.intro.refine'_1.mpr
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x : β
hx : f k < x
⊢ (∃ a, a ∈ B ∧ f a = x) → ∃ a, a ∈ A ∧ f a = x
any_goals
  rintro ⟨x', hx', rfl⟩
  refine' ⟨x', _, rfl⟩
  first |rwa [← z _]|rwa [z _]
  rwa [StrictMono.lt_iff_lt h₁] at hx
case mpr.intro.intro.intro.refine'_1.mpr.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ ∃ a, a ∈ A ∧ f a = f x'
case mpr.intro.intro.intro.refine'_1.mpr
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x : β
hx : f k < x
⊢ (∃ a, a ∈ B ∧ f a = x) → ∃ a, a ∈ A ∧ f a = x
rintro ⟨x', hx', rfl⟩
case mpr.intro.intro.intro.refine'_1.mpr.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ x' ∈ A
case mpr.intro.intro.intro.refine'_1.mpr.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ ∃ a, a ∈ A ∧ f a = f x'
refine' ⟨x', _, rfl⟩
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ k < x'
case mpr.intro.intro.intro.refine'_1.mpr.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ x' ∈ A
first |rwa [← z _]|rwa [z _]
no goals
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ k < x'
rwa [StrictMono.lt_iff_lt h₁] at hx
case mpr.intro.intro.intro.refine'_1.mpr.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ x' ∈ A
case mpr.intro.intro.intro.refine'_1.mpr.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ x' ∈ A
rwa [← z _]
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ k < x'
case mpr.intro.intro.intro.refine'_1.mpr.intro.intro
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ x' ∈ A
rwa [z _]
case mpr.intro.intro.intro.refine'_2
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
⊢ ∀ (x : α), x ∈ A → ¬x = k
case mpr.intro.intro.intro.refine'_2
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
⊢ ∀ (x : α), x ∈ A → ¬f x = f k
simp only [h₁.injective, Function.Injective.eq_iff]
no goals
case mpr.intro.intro.intro.refine'_2
α : Type u_2
β : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
⊢ ∀ (x : α), x ∈ A → ¬x = k
exact fun x hx => ne_of_mem_of_not_mem hx ka