case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ x = y

case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (Disjoint on fun b => (fun a => f a b) '' s) x y
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
⊢ (PairwiseDisjoint t fun b => (fun a => f a b) '' s) ↔ InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
refine' ⟨fun ht x hx y hy (h : f _ _ = _) => _, fun ht x hx y hy h => _⟩
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ x.snd = y.snd
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ x = y
suffices x.2 = y.2 by exact Prod.ext (hf _ hx.2 <| h.trans <| by rw [this]) this
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ f x.fst x.snd ∈ (fun a => f a y.snd) '' s
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ x.snd = y.snd
refine' ht.elim hx.2 hy.2 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.1, _⟩)
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ (fun p => f p.fst p.snd) y ∈ (fun a => f a y.snd) '' s
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ f x.fst x.snd ∈ (fun a => f a y.snd) '' s
rw [h]
no goals
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ (fun p => f p.fst p.snd) y ∈ (fun a => f a y.snd) '' s
exact mem_image_of_mem _ hy.1
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
this : x.snd = y.snd
⊢ x = y
exact Prod.ext (hf _ hx.2 <| h.trans <| by rw [this]) this
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
this : x.snd = y.snd
⊢ (fun p => f p.fst p.snd) y = (fun a => f a x.snd) y.fst
rw [this]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (fun b => (fun a => f a b) '' s) x ⊓ (fun b => (fun a => f a b) '' s) y ≤ ⊥
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (Disjoint on fun b => (fun a => f a b) '' s) x y
refine' disjoint_iff_inf_le.mpr _
case refine'_2.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : (fun a => f a x) a = (fun a => f a y) b
⊢ (fun a => f a y) b ∈ ⊥
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (fun b => (fun a => f a b) '' s) x ⊓ (fun b => (fun a => f a b) '' s) y ≤ ⊥
rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩
no goals
case refine'_2.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.41702
ι' : Type ?u.41705
r p q : α → α → Prop
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : (fun a => f a x) a = (fun a => f a y) b
⊢ (fun a => f a y) b ∈ ⊥
exact h (congr_arg Prod.snd <| ht (mk_mem_prod ha hx) (mk_mem_prod hb hy) hab)