α : Type u_1
β : Type u_3
γ : Type u_2
ι : Sort ?u.48895
π : α → Type ?u.48900
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b✝ : β
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
b : β
hb : b ∈ t
⊢ g₁ b = g₂ b
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Sort ?u.48895
π : α → Type ?u.48900
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
⊢ EqOn g₁ g₂ t
intro b hb
case intro.intro
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Sort ?u.48895
π : α → Type ?u.48900
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a✝ : α
b : β
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ g₁ (f a) = g₂ (f a)
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Sort ?u.48895
π : α → Type ?u.48900
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b✝ : β
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
b : β
hb : b ∈ t
⊢ g₁ b = g₂ b
obtain ⟨a, ha, rfl⟩ := hf' hb
no goals
case intro.intro
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Sort ?u.48895
π : α → Type ?u.48900
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a✝ : α
b : β
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ g₁ (f a) = g₂ (f a)
exact hf ha