Theorem: Prod.snd.arg_self.isomorph_rule (SciLean/Core/FunctionTransformations/Isomorph/RealToFloat.lean)

State before:
α✝ : Type ?u.9557
α'✝ : Type ?u.9560
β : Type ?u.9563
β' : Type ?u.9566
γ : Type ?u.9569
γ' : Type ?u.9572
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
⊢ (isomorph `RealToFloat fun x => (f x).2) = fun x => (isomorph `RealToFloat f x).2
Tactic:
funext x
State after:
case h
α✝ : Type ?u.9557
α'✝ : Type ?u.9560
β : Type ?u.9563
β' : Type ?u.9566
γ : Type ?u.9569
γ' : Type ?u.9572
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ isomorph `RealToFloat (fun x => (f x).2) x = (isomorph `RealToFloat f x).2

State before:
case h
α✝ : Type ?u.9557
α'✝ : Type ?u.9560
β : Type ?u.9563
β' : Type ?u.9566
γ : Type ?u.9569
γ' : Type ?u.9572
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ isomorph `RealToFloat (fun x => (f x).2) x = (isomorph `RealToFloat f x).2
Tactic:
unfold isomorph
State after:
case h
α✝ : Type ?u.9557
α'✝ : Type ?u.9560
β : Type ?u.9563
β' : Type ?u.9566
γ : Type ?u.9569
γ' : Type ?u.9572
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ (IsomorphicType.equiv `RealToFloat) ((fun x => (f x).2) ((IsomorphicType.equiv `RealToFloat).symm x)) =
    ((IsomorphicType.equiv `RealToFloat) (f ((IsomorphicType.equiv `RealToFloat).symm x))).2

State before:
case h
α✝ : Type ?u.9557
α'✝ : Type ?u.9560
β : Type ?u.9563
β' : Type ?u.9566
γ : Type ?u.9569
γ' : Type ?u.9572
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ (IsomorphicType.equiv `RealToFloat) ((fun x => (f x).2) ((IsomorphicType.equiv `RealToFloat).symm x)) =
    ((IsomorphicType.equiv `RealToFloat) (f ((IsomorphicType.equiv `RealToFloat).symm x))).2
Tactic:
unfold IsomorphicType.equiv
State after:
case h
α✝ : Type ?u.9557
α'✝ : Type ?u.9560
β : Type ?u.9563
β' : Type ?u.9566
γ : Type ?u.9569
γ' : Type ?u.9572
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ inst✝.1 ((fun x => (f x).2) (inst✝².1.symm x)) =
    ({
            equiv :=
              {
                toFun := fun x =>
                  match x with
                  | (a, b) => (inst✝¹.1 a, inst✝.1 b),
                invFun := fun x =>
                  match x with
                  | (a', b') => (inst✝¹.1.symm a', inst✝.1.symm b'),
                left_inv := ⋯, right_inv := ⋯ } }.1
        (f (inst✝².1.symm x))).2

State before:
case h
α✝ : Type ?u.9557
α'✝ : Type ?u.9560
β : Type ?u.9563
β' : Type ?u.9566
γ : Type ?u.9569
γ' : Type ?u.9572
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ inst✝.1 ((fun x => (f x).2) (inst✝².1.symm x)) =
    ({
            equiv :=
              {
                toFun := fun x =>
                  match x with
                  | (a, b) => (inst✝¹.1 a, inst✝.1 b),
                invFun := fun x =>
                  match x with
                  | (a', b') => (inst✝¹.1.symm a', inst✝.1.symm b'),
                left_inv := ⋯, right_inv := ⋯ } }.1
        (f (inst✝².1.symm x))).2
Tactic:
simp
State after:
no goals