-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem pairwiseDisjoint_image_right_iff {f : α → β → γ} {s : Set α} {t : Set β}
    (hf : ∀ a ∈ s, Injective (f a)) :
    (s.PairwiseDisjoint fun a => f a '' t) ↔ (s ×ˢ t).InjOn fun p => f p.1 p.2

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : InjOn (fun p => f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
⊢ (Disjoint on fun a => f a '' t) x y

Tactic:
refine disjoint_iff_inf_le.mpr ?_

Result:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : InjOn (fun p => f p.1 p.2) (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 ≤ ⊥

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : s.PairwiseDisjoint fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p => f p.1 p.2) y
this : x.1 = y.1
⊢ (fun p => f p.1 p.2) y = f x.1 y.2

Tactic:
rw [this]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : s.PairwiseDisjoint fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p => f p.1 p.2) y
⊢ x = y

Tactic:
suffices x.1 = y.1 by exact Prod.ext this (hf _ hx.1 <| h.trans <| by rw [this])

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : s.PairwiseDisjoint fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p => f p.1 p.2) y
⊢ x.1 = y.1

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : s.PairwiseDisjoint fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p => f p.1 p.2) y
⊢ f x.1 x.2 ∈ f y.1 '' t

Tactic:
rw [h]

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : s.PairwiseDisjoint fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p => f p.1 p.2) y
⊢ (fun p => f p.1 p.2) y ∈ f y.1 '' t

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : InjOn (fun p => f p.1 p.2) (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 ≤ ⊥

Tactic:
rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩

Result:
case refine_2.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : InjOn (fun p => f p.1 p.2) (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 ∈ ⊥

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : s.PairwiseDisjoint fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p => f p.1 p.2) y
this : x.1 = y.1
⊢ x = y

Tactic:
exact Prod.ext this (hf _ hx.1 <| h.trans <| by rw [this])

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : s.PairwiseDisjoint fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p => f p.1 p.2) y
⊢ (fun p => f p.1 p.2) y ∈ f y.1 '' t

Tactic:
exact mem_image_of_mem _ hy.2

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : s.PairwiseDisjoint fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p => f p.1 p.2) y
⊢ x.1 = y.1

Tactic:
refine hs.elim hx.1 hy.1 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.2, ?_⟩)

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : s.PairwiseDisjoint fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p => f p.1 p.2) y
⊢ f x.1 x.2 ∈ f y.1 '' t

Proof state:
case refine_2.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : InjOn (fun p => f p.1 p.2) (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 ∈ ⊥

Tactic:
exact h (congr_arg Prod.fst <| hs (mk_mem_prod hx ha) (mk_mem_prod hy hb) hab)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
⊢ (s.PairwiseDisjoint fun a => f a '' t) ↔ InjOn (fun p => f p.1 p.2) (s ×ˢ t)

Tactic:
refine ⟨fun hs x hx y hy (h : f _ _ = _) => ?_, fun hs x hx y hy h => ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : s.PairwiseDisjoint fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p => f p.1 p.2) y
⊢ x = y

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ a ∈ s, Injective (f a)
hs : InjOn (fun p => f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
⊢ (Disjoint on fun a => f a '' t) x y