case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.111902
ι : Sort ?u.111905
π : α → Type ?u.111910
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : fb (f x) = fb (f y)
⊢ f x = f y
α : Type u_1
β : Type u_2
γ : Type ?u.111902
ι : Sort ?u.111905
π : α → Type ?u.111910
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
⊢ InjOn fb (f '' s)
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ H
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.111902
ι : Sort ?u.111905
π : α → Type ?u.111910
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : f (fa x) = f (fa y)
⊢ f x = f y
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.111902
ι : Sort ?u.111905
π : α → Type ?u.111910
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : fb (f x) = fb (f y)
⊢ f x = f y
simp only [← h.eq] at H
no goals
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.111902
ι : Sort ?u.111905
π : α → Type ?u.111910
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : f (fa x) = f (fa y)
⊢ f x = f y
exact congr_arg f (ha hx hy <| hf (mem_image_of_mem fa hx) (mem_image_of_mem fa hy) H)