Theorem: Function.invFun_comp' (SciLean/Core/FunctionPropositions/Bijective.lean)

State before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
hf : Injective f
x : α
⊢ invFun f (f x) = x
Tactic:
suffices (f.invFun ∘ f) x = x by assumption
State after:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
hf : Injective f
x : α
⊢ (invFun f ∘ f) x = x

State before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
hf : Injective f
x : α
⊢ (invFun f ∘ f) x = x
Tactic:
rw[Function.invFun_comp hf]
State after:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
hf : Injective f
x : α
⊢ id x = x

State before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
hf : Injective f
x : α
⊢ id x = x
Tactic:
rfl
State after:
no goals

State before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
hf : Injective f
x : α
this : (invFun f ∘ f) x = x
⊢ invFun f (f x) = x
Tactic:
assumption
State after:
no goals