case intro.intro
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Sort ?u.34009
π : α → Type ?u.34014
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Injective (g ∘ f)
x y : α
H : g (f x) = g (f y)
⊢ f x = f y
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Sort ?u.34009
π : α → Type ?u.34014
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Injective (g ∘ f)
⊢ InjOn g (range f)
rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ H
no goals
case intro.intro
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Sort ?u.34009
π : α → Type ?u.34014
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : Injective (g ∘ f)
x y : α
H : g (f x) = g (f y)
⊢ f x = f y
exact congr_arg f (h H)