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