case intro.intro.intro.intro
α : Type u_1
α' : Type ?u.898
β : Type u_2
β' : Type ?u.904
γ : Type u_3
γ' : Type ?u.910
δ : Type ?u.913
δ' : Type ?u.916
ε : Type ?u.919
ε' : Type ?u.922
ζ : Type ?u.925
ζ' : Type ?u.928
ν : Type ?u.931
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a'✝ : α
b b'✝ : β
c c' : γ
d d' : δ
hf : Injective2 f
a' : α
b' : β
ha' : a' ∈ s
hb' : b' ∈ t
h : f a' b' = f a b
⊢ a ∈ s ∧ b ∈ t
α : Type u_1
α' : Type ?u.898
β : Type u_2
β' : Type ?u.904
γ : Type u_3
γ' : Type ?u.910
δ : Type ?u.913
δ' : Type ?u.916
ε : Type ?u.919
ε' : Type ?u.922
ζ : Type ?u.925
ζ' : Type ?u.928
ν : Type ?u.931
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c c' : γ
d d' : δ
hf : Injective2 f
⊢ f a b ∈ image2 f s t → a ∈ s ∧ b ∈ t
rintro ⟨a', b', ha', hb', h⟩
case intro.intro.intro.intro.intro
α : Type u_1
α' : Type ?u.898
β : Type u_2
β' : Type ?u.904
γ : Type u_3
γ' : Type ?u.910
δ : Type ?u.913
δ' : Type ?u.916
ε : Type ?u.919
ε' : Type ?u.922
ζ : Type ?u.925
ζ' : Type ?u.928
ν : Type ?u.931
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a'✝ : α
b'✝ : β
c c' : γ
d d' : δ
hf : Injective2 f
a' : α
b' : β
ha' : a' ∈ s
hb' : b' ∈ t
h : f a' b' = f a' b'
⊢ a' ∈ s ∧ b' ∈ t
case intro.intro.intro.intro
α : Type u_1
α' : Type ?u.898
β : Type u_2
β' : Type ?u.904
γ : Type u_3
γ' : Type ?u.910
δ : Type ?u.913
δ' : Type ?u.916
ε : Type ?u.919
ε' : Type ?u.922
ζ : Type ?u.925
ζ' : Type ?u.928
ν : Type ?u.931
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a'✝ : α
b b'✝ : β
c c' : γ
d d' : δ
hf : Injective2 f
a' : α
b' : β
ha' : a' ∈ s
hb' : b' ∈ t
h : f a' b' = f a b
⊢ a ∈ s ∧ b ∈ t
rcases hf h with ⟨rfl, rfl⟩
no goals
case intro.intro.intro.intro.intro
α : Type u_1
α' : Type ?u.898
β : Type u_2
β' : Type ?u.904
γ : Type u_3
γ' : Type ?u.910
δ : Type ?u.913
δ' : Type ?u.916
ε : Type ?u.919
ε' : Type ?u.922
ζ : Type ?u.925
ζ' : Type ?u.928
ν : Type ?u.931
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a'✝ : α
b'✝ : β
c c' : γ
d d' : δ
hf : Injective2 f
a' : α
b' : β
ha' : a' ∈ s
hb' : b' ∈ t
h : f a' b' = f a' b'
⊢ a' ∈ s ∧ b' ∈ t
exact ⟨ha', hb'⟩