α : Type u_4
β : Type u_1
γ : Type u_3
δ : Type u_2
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
b : β
inhabited_h : Inhabited δ
⊢ f₁ (f₂ b) = b
α : Type u_4
β : Type u_1
γ : Type u_3
δ : Type u_2
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
b : β
⊢ f₁ (f₂ b) = b
inhabit δ
no goals
α : Type u_4
β : Type u_1
γ : Type u_3
δ : Type u_2
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
b : β
inhabited_h : Inhabited δ
⊢ f₁ (f₂ b) = b
exact congr_arg Prod.fst (h (b, default))
α : Type u_4
β : Type u_1
γ : Type u_3
δ : Type u_2
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
inhabited_h : Inhabited β
⊢ g₁ (g₂ d) = d
α : Type u_4
β : Type u_1
γ : Type u_3
δ : Type u_2
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
⊢ g₁ (g₂ d) = d
inhabit β
no goals
α : Type u_4
β : Type u_1
γ : Type u_3
δ : Type u_2
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
inhabited_h : Inhabited β
⊢ g₁ (g₂ d) = d
exact congr_arg Prod.snd (h (default, d))