-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : MetricSpace P
inst_6 : PseudoMetricSpace Q
inst_7 : NormedAddTorsor V P
inst_8 : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : s.Nonempty
this_1 : Nonempty.{u_5 + 1} (↑s : Type u_5)
f : Homeomorph.{u_5, u_4} ↥(affineSpan 𝕜 s) ↥(map φ.toAffineMap (affineSpan 𝕜 s)) :=
  AffineIsometryEquiv.toHomeomorph (isometryEquivMap φ (affineSpan 𝕜 s))
this :
  Eq.{u_4 + 1} (α := ↥(map φ.toAffineMap (affineSpan 𝕜 s)) → Q)
    (Function.comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := P) (⇑φ.toAffineMap : (a : P) → Q)
      (Function.comp (β := ↥(affineSpan 𝕜 s))
        (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
        (⇑f.symm : (a : ↥(map φ.toAffineMap (affineSpan 𝕜 s))) → ↥(affineSpan 𝕜 s))))
    (Subtype.val (p := fun (x : Q) ↦ x ∈ map φ.toAffineMap (affineSpan 𝕜 s)))
inr :
  Eq.{u_4 + 1} (α := Set Q)
    (image (α := ↥(affineSpan 𝕜 ((⇑φ : (a : P) → Q) '' s)))
      (Subtype.val (p := fun (x : Q) ↦
        Membership.mem (γ := AffineSubspace 𝕜 Q) (affineSpan 𝕜 ((⇑φ : (a : P) → Q) '' s)) x))
      (frontier
        (Subtype.val (p := fun (x : Q) ↦
            Membership.mem (γ := AffineSubspace 𝕜 Q) (affineSpan 𝕜 ((⇑φ : (a : P) → Q) '' s)) x) ⁻¹'
          (⇑φ : (a : P) → Q) '' s)))
    ((⇑φ : (a : P) → Q) '' intrinsicFrontier 𝕜 s)
inr₁ :
  Eq.{u_4 + 1} (α := Set Q)
    (image (α := ↥(affineSpan 𝕜 ((⇑φ : (a : P) → Q) '' s)))
      (Subtype.val (p := fun (x : Q) ↦
        Membership.mem (γ := AffineSubspace 𝕜 Q) (affineSpan 𝕜 ((⇑φ : (a : P) → Q) '' s)) x))
      (frontier
        (Subtype.val (p := fun (x : Q) ↦
            Membership.mem (γ := AffineSubspace 𝕜 Q) (affineSpan 𝕜 ((⇑φ : (a : P) → Q) '' s)) x) ⁻¹'
          (⇑φ : (a : P) → Q) '' s)))
    ((⇑φ : (a : P) → Q) ''
      image (α := ↥(affineSpan 𝕜 s))
        (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
        (frontier (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)))
inr₂ :
  Eq.{u_4 + 1} (α := Set Q)
    (image (α := ↥(affineSpan 𝕜 ((⇑φ.toAffineMap : (a : P) → Q) '' s)))
      (Subtype.val (p := fun (x : Q) ↦
        Membership.mem (γ := AffineSubspace 𝕜 Q) (affineSpan 𝕜 ((⇑φ.toAffineMap : (a : P) → Q) '' s)) x))
      (frontier
        (Subtype.val (p := fun (x : Q) ↦
            Membership.mem (γ := AffineSubspace 𝕜 Q) (affineSpan 𝕜 ((⇑φ.toAffineMap : (a : P) → Q) '' s)) x) ⁻¹'
          (⇑φ.toAffineMap : (a : P) → Q) '' s)))
    ((⇑φ.toAffineMap : (a : P) → Q) ''
      image (α := ↥(affineSpan 𝕜 s))
        (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
        (frontier (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)))
inr₃ :
  Eq.{u_4 + 1} (α := Set Q)
    (image (α := ↥(map φ.toAffineMap (affineSpan 𝕜 s)))
      (Subtype.val (p := fun (x : Q) ↦ x ∈ map φ.toAffineMap (affineSpan 𝕜 s)))
      (frontier
        (Subtype.val (p := fun (x : Q) ↦ x ∈ map φ.toAffineMap (affineSpan 𝕜 s)) ⁻¹'
          (⇑φ.toAffineMap : (a : P) → Q) '' s)))
    ((⇑φ.toAffineMap : (a : P) → Q) ''
      image (α := ↥(affineSpan 𝕜 s))
        (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
        (frontier (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)))
inr₄ :
  Eq.{u_4 + 1} (α := Set Q)
    (image (α := ↥(map φ.toAffineMap (affineSpan 𝕜 s)))
      (Function.comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := P) (⇑φ.toAffineMap : (a : P) → Q)
        (Function.comp (β := ↥(affineSpan 𝕜 s))
          (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
          (⇑f.symm : (a : ↥(map φ.toAffineMap (affineSpan 𝕜 s))) → ↥(affineSpan 𝕜 s))))
      (frontier
        (preimage (β := Q)
          (Function.comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := P) (⇑φ.toAffineMap : (a : P) → Q)
            (Function.comp (β := ↥(affineSpan 𝕜 s))
              (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
              (⇑f.symm : (a : ↥(map φ.toAffineMap (affineSpan 𝕜 s))) → ↥(affineSpan 𝕜 s))))
          ((⇑φ.toAffineMap : (a : P) → Q) '' s))))
    ((⇑φ.toAffineMap : (a : P) → Q) ''
      image (α := ↥(affineSpan 𝕜 s))
        (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
        (frontier (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)))
inr₅ :
  Eq.{u_4 + 1} (α := Set Q)
    (image (α := ↥(map φ.toAffineMap (affineSpan 𝕜 s)))
      (Function.comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := ↥(affineSpan 𝕜 s))
        ((⇑φ.toAffineMap : (a : P) → Q) ∘
          Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
        (⇑f.symm : (a : ↥(map φ.toAffineMap (affineSpan 𝕜 s))) → ↥(affineSpan 𝕜 s)))
      (frontier
        (preimage (β := Q)
          (Function.comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := ↥(affineSpan 𝕜 s))
            ((⇑φ.toAffineMap : (a : P) → Q) ∘
              Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
            (⇑f.symm : (a : ↥(map φ.toAffineMap (affineSpan 𝕜 s))) → ↥(affineSpan 𝕜 s)))
          ((⇑φ.toAffineMap : (a : P) → Q) '' s))))
    ((⇑φ.toAffineMap : (a : P) → Q) ''
      image (α := ↥(affineSpan 𝕜 s))
        (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
        (frontier (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)))
inr₆ :
  Eq.{u_4 + 1} (α := Set Q)
    (image.{u_5, u_4} (α := ↥(affineSpan 𝕜 s))
      ((⇑φ.toAffineMap : (a : P) → Q) ∘
        Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
      (image.{u_4, u_5} (α := ↥(map φ.toAffineMap (affineSpan 𝕜 s)))
        (⇑f.symm : (a : ↥(map φ.toAffineMap (affineSpan 𝕜 s))) → ↥(affineSpan 𝕜 s))
        (frontier
          (preimage (β := Q)
            (Function.comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := ↥(affineSpan 𝕜 s))
              ((⇑φ.toAffineMap : (a : P) → Q) ∘
                Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
              (⇑f.symm : (a : ↥(map φ.toAffineMap (affineSpan 𝕜 s))) → ↥(affineSpan 𝕜 s)))
            ((⇑φ.toAffineMap : (a : P) → Q) '' s)))))
    ((⇑φ.toAffineMap : (a : P) → Q) ''
      image (α := ↥(affineSpan 𝕜 s))
        (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
        (frontier (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)))
inr₇ :
  Eq.{u_4 + 1} (α := Set Q)
    (image.{u_5, u_4} (α := P) (⇑φ.toAffineMap : (a : P) → Q)
      (image (α := ↥(affineSpan 𝕜 s))
        (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
        (image.{u_4, u_5} (α := ↥(map φ.toAffineMap (affineSpan 𝕜 s)))
          (⇑f.symm : (a : ↥(map φ.toAffineMap (affineSpan 𝕜 s))) → ↥(affineSpan 𝕜 s))
          (frontier
            (preimage (β := Q)
              (Function.comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := ↥(affineSpan 𝕜 s))
                ((⇑φ.toAffineMap : (a : P) → Q) ∘
                  Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
                (⇑f.symm : (a : ↥(map φ.toAffineMap (affineSpan 𝕜 s))) → ↥(affineSpan 𝕜 s)))
              ((⇑φ.toAffineMap : (a : P) → Q) '' s))))))
    ((⇑φ.toAffineMap : (a : P) → Q) ''
      image (α := ↥(affineSpan 𝕜 s))
        (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
        (frontier (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)))
⊢ Eq.{u_4 + 1} (α := Set Q) (intrinsicFrontier 𝕜 ((⇑φ : (a : P) → Q) '' s))
    ((⇑φ : (a : P) → Q) '' intrinsicFrontier 𝕜 s)
have inr₈ : Eq.{u_4 + 1} (α := Set Q)
  (image.{u_5, u_4} (α := P) (⇑φ.toAffineMap : (a : P) → Q)
    (image (α := ↥(affineSpan 𝕜 s))
      (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
      (frontier
        (image.{u_4, u_5} (α := ↥(map φ.toAffineMap (affineSpan 𝕜 s)))
          (⇑f.symm : (a : ↥(map φ.toAffineMap (affineSpan 𝕜 s))) → ↥(affineSpan 𝕜 s))
          (preimage (β := Q)
            (Function.comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := ↥(affineSpan 𝕜 s))
              ((⇑φ.toAffineMap : (a : P) → Q) ∘
                Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
              (⇑f.symm : (a : ↥(map φ.toAffineMap (affineSpan 𝕜 s))) → ↥(affineSpan 𝕜 s)))
            ((⇑φ.toAffineMap : (a : P) → Q) '' s))))))
  ((⇑φ.toAffineMap : (a : P) → Q) ''
    image (α := ↥(affineSpan 𝕜 s))
      (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
      (frontier (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)))
Tactic: rw [intrinsicFrontier, intrinsicFrontier, ← φ.coe_toAffineMap, ← map_span φ.toAffineMap s, ← this,
    ← Function.comp_assoc, image_comp, image_comp, f.symm.image_frontier, f.image_symm,
    ← preimage_comp, Function.comp_assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap,
    Function.comp_id, preimage_comp, φ.injective.preimage_image]