Theorem: SciLean.parametric_inverse_bijection (SciLean/Core/Integral/ParametricInverse.lean)

State before:
R : Type ?u.275
inst✝¹ : RealScalar R
X Y : Type
inst✝ : Nonempty X
f : X → Y
hf : Function.Bijective f
y : Y
⊢ ParametricInverseAt f y (fun x x x => x) (fun x x => Function.invFun f y) fun x => univ
Tactic:
intro i x _
State after:
R : Type ?u.275
inst✝¹ : RealScalar R
X Y : Type
inst✝ : Nonempty X
f : X → Y
hf : Function.Bijective f
y : Y
i x : Unit
a✝ : x ∈ (fun x => univ) i
⊢ f ((fun x x x => x) i x ((fun x x => Function.invFun f y) i x)) = y

State before:
R : Type ?u.275
inst✝¹ : RealScalar R
X Y : Type
inst✝ : Nonempty X
f : X → Y
hf : Function.Bijective f
y : Y
i x : Unit
a✝ : x ∈ (fun x => univ) i
⊢ f ((fun x x x => x) i x ((fun x x => Function.invFun f y) i x)) = y
Tactic:
simp only
State after:
R : Type ?u.275
inst✝¹ : RealScalar R
X Y : Type
inst✝ : Nonempty X
f : X → Y
hf : Function.Bijective f
y : Y
i x : Unit
a✝ : x ∈ (fun x => univ) i
⊢ f (Function.invFun f y) = y

State before:
R : Type ?u.275
inst✝¹ : RealScalar R
X Y : Type
inst✝ : Nonempty X
f : X → Y
hf : Function.Bijective f
y : Y
i x : Unit
a✝ : x ∈ (fun x => univ) i
⊢ f (Function.invFun f y) = y
Tactic:
sorry_proof
State after:
no goals