awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
x : P
rw :
  Eq (α := Set P)
    (image (α := ↥(affineSpan 𝕜 {x}))
      (Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {x}) x_1))
      (frontier
        (Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {x}) x_1) ⁻¹' {x})))
    ∅
rw₁ :
  Eq.{u_5 + 1} (α := Set P)
    (image (α := ↥(affineSpan 𝕜 {x}))
      (Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {x}) x_1))
      (frontier univ))
    ∅
⊢ Eq (α := Set P) (intrinsicFrontier 𝕜 {x}) ∅
have rw₂ : Eq.{u_5 + 1} (α := Set P)
  (image (α := ↥(affineSpan 𝕜 {x}))
    (Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {x}) x_1)) ∅)
  ∅
Tactic: rw [intrinsicFrontier, preimage_coe_affineSpan_singleton, frontier_univ, image_empty]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
x : P
rw :
  Eq (α := Set P)
    (image (α := ↥(affineSpan 𝕜 {x}))
      (Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {x}) x_1))
      (frontier
        (Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {x}) x_1) ⁻¹' {x})))
    ∅
rw₁ :
  Eq.{u_5 + 1} (α := Set P)
    (image (α := ↥(affineSpan 𝕜 {x}))
      (Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {x}) x_1))
      (frontier univ))
    ∅
rw₂ :
  Eq.{u_5 + 1} (α := Set P)
    (image (α := ↥(affineSpan 𝕜 {x}))
      (Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {x}) x_1)) ∅)
    ∅
⊢ Eq (α := Set P) (intrinsicFrontier 𝕜 {x}) ∅
have rw₃ : Eq.{u_5 + 1} (α := Set P) ∅ ∅
Tactic: rw [intrinsicFrontier, preimage_coe_affineSpan_singleton, frontier_univ, image_empty]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s t : Set P
h : s ⊆ t
⊢ intrinsicClosure 𝕜 s ⊆ intrinsicClosure 𝕜 t
have refine : ∀ (x : ↥(affineSpan 𝕜 s))
  (hx :
    Membership.mem (γ := Set ↥(affineSpan 𝕜 s))
      (closure[instTopologicalSpaceSubtype]
        (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s))
      x),
  Membership.mem (γ := Set ↥(affineSpan 𝕜 s))
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹'
      intrinsicClosure 𝕜 t)
    x
Tactic: refine image_subset_iff.2 fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s t : Set P
h : s ⊆ t
x : ↥(affineSpan 𝕜 s)
hx :
  Membership.mem (γ := Set ↥(affineSpan 𝕜 s))
    (closure[instTopologicalSpaceSubtype]
      (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s))
    x
⊢ Membership.mem (γ := Set ↥(affineSpan 𝕜 s))
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹'
      intrinsicClosure 𝕜 t)
    x
have refine : Membership.mem (γ := Set ↥(affineSpan 𝕜 t))
  (closure[instTopologicalSpaceSubtype]
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 t) x) ⁻¹' t))
  (Set.inclusion (s := (↑(affineSpan 𝕜 s) : Set P)) (t := (↑(affineSpan 𝕜 t) : Set P)) sorry x)
Tactic: refine ⟨Set.inclusion (affineSpan_mono _ h) x, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s t : Set P
h : s ⊆ t
x : ↥(affineSpan 𝕜 s)
hx :
  Membership.mem (γ := Set ↥(affineSpan 𝕜 s))
    (closure[instTopologicalSpaceSubtype]
      (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s))
    x
⊢ Membership.mem (γ := Set ↥(affineSpan 𝕜 t))
    (closure[instTopologicalSpaceSubtype]
      (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 t) x) ⁻¹' t))
    (Set.inclusion (s := (↑(affineSpan 𝕜 s) : Set P)) (t := (↑(affineSpan 𝕜 t) : Set P)) ⋯ x)
have refine : Subset (α := Set (↑(↑(affineSpan 𝕜 s) : Set P) : Type u_5))
  (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)
  (Set.inclusion (s := (↑(affineSpan 𝕜 s) : Set P)) (t := (↑(affineSpan 𝕜 t) : Set P)) sorry ⁻¹'
    Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 t) x) ⁻¹' t)
Tactic: refine (continuous_inclusion (affineSpan_mono _ h)).closure_preimage_subset _ (closure_mono ?_ hx)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
⊢ (fun (a : ↥(affineSpan 𝕜 s)) ↦ (↑a : P)) ''
      (closure[instTopologicalSpaceSubtype]
          (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s) \
        frontier (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)) =
    intrinsicInterior 𝕜 s
have rw : (fun (a : ↥(affineSpan 𝕜 s)) ↦ (↑a : P)) ''
    interior (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s) =
  intrinsicInterior 𝕜 s
Tactic: rw [closure_diff_frontier, intrinsicInterior]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
rw :
  (fun (a : ↥(affineSpan 𝕜 s)) ↦ (↑a : P)) ''
      interior (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s) =
    intrinsicInterior 𝕜 s
⊢ (fun (a : ↥(affineSpan 𝕜 s)) ↦ (↑a : P)) ''
      (closure[instTopologicalSpaceSubtype]
          (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s) \
        frontier (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)) =
    intrinsicInterior 𝕜 s
have rw₁ : (fun (a : ↥(affineSpan 𝕜 s)) ↦ (↑a : P)) ''
    interior (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s) =
  image (α := ↥(affineSpan 𝕜 s))
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
    (interior (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s))
Tactic: rw [closure_diff_frontier, intrinsicInterior]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
⊢ intrinsicFrontier 𝕜 s ∪ intrinsicInterior 𝕜 s = intrinsicClosure 𝕜 s
have rw : intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s
Tactic: rw [union_comm, intrinsicInterior_union_intrinsicFrontier]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
rw : intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s
⊢ intrinsicFrontier 𝕜 s ∪ intrinsicInterior 𝕜 s = intrinsicClosure 𝕜 s
have rw₁ : intrinsicClosure 𝕜 s = intrinsicClosure 𝕜 s
Tactic: rw [union_comm, intrinsicInterior_union_intrinsicFrontier]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
hs :
  IsClosed[instTopologicalSpaceSubtype]
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)
⊢ intrinsicClosure 𝕜 s = s
have rw : s ⊆
  range (ι := ↥(affineSpan 𝕜 s))
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
Tactic: rw [intrinsicClosure, hs.closure_eq, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
⊢ intrinsicClosure 𝕜 (intrinsicClosure 𝕜 s) = intrinsicClosure 𝕜 s
have refine : IsClosed[instTopologicalSpaceSubtype]
  (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 (intrinsicClosure 𝕜 s)) x) ⁻¹'
    intrinsicClosure 𝕜 s)
Tactic: refine IsClosed.intrinsicClosure ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
⊢ IsClosed[instTopologicalSpaceSubtype]
    (Subtype.val (p := fun (x : P) ↦
        Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 (intrinsicClosure 𝕜 s)) x) ⁻¹'
      intrinsicClosure 𝕜 s)
have set : let t : AffineSubspace 𝕜 P := affineSpan 𝕜 (intrinsicClosure 𝕜 s);
∀ (ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)),
  IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : P) ↦ x ∈ t) ⁻¹' intrinsicClosure 𝕜 s)
Tactic: set t := affineSpan 𝕜 (intrinsicClosure 𝕜 s) with ht
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
t : AffineSubspace 𝕜 P := affineSpan 𝕜 (intrinsicClosure 𝕜 s)
ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : P) ↦ x ∈ t) ⁻¹' intrinsicClosure 𝕜 s)
have clear_value : ∀ (t : AffineSubspace 𝕜 P) (ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)),
  IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : P) ↦ x ∈ t) ⁻¹' intrinsicClosure 𝕜 s)
Tactic: clear_value t
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
t : AffineSubspace 𝕜 P
ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : P) ↦ x ∈ t) ⁻¹' intrinsicClosure 𝕜 s)
have obtain : ∀ (ht : Eq (α := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) (affineSpan 𝕜 (intrinsicClosure 𝕜 s))),
  IsClosed[instTopologicalSpaceSubtype]
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹'
      intrinsicClosure 𝕜 s)
Tactic: obtain rfl := ht.trans (affineSpan_intrinsicClosure _)
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
ht : Eq (α := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) (affineSpan 𝕜 (intrinsicClosure 𝕜 s))
⊢ IsClosed[instTopologicalSpaceSubtype]
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹'
      intrinsicClosure 𝕜 s)
have rw : IsClosed[instTopologicalSpaceSubtype]
  (closure[instTopologicalSpaceSubtype]
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s))
Tactic: rw [intrinsicClosure, preimage_image_eq _ Subtype.coe_injective]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
⊢ intrinsicClosure 𝕜 s = closure[inst_3] s ∩ (↑(affineSpan 𝕜 s) : Set P)
have h : IsInducing.{u_5, u_5} (X := ↥(affineSpan 𝕜 s))
  (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
Tactic: have h : Topology.IsInducing ((↑) : affineSpan 𝕜 s → P) := .subtypeVal
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
h :
  IsInducing.{u_5, u_5} (X := ↥(affineSpan 𝕜 s))
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
⊢ intrinsicClosure 𝕜 s = closure[inst_3] s ∩ (↑(affineSpan 𝕜 s) : Set P)
have rw : s ⊆
  range (ι := ↥(affineSpan 𝕜 s))
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
Tactic: rw [intrinsicClosure, h.closure_eq_preimage_closure_image, Set.image_preimage_eq_inter_range,
    Set.image_preimage_eq_of_subset ?_, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
h :
  IsInducing.{u_5, u_5} (X := ↥(affineSpan 𝕜 s))
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
⊢ s ⊆
    range (ι := ↥(affineSpan 𝕜 s))
      (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
have rw : s ⊆ (↑(affineSpan 𝕜 s) : Set P)
Tactic: rw [Subtype.range_coe]
-- 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
⊢ Eq.{u_4 + 1} (α := Set Q) (intrinsicInterior 𝕜 ((⇑φ : (a : P) → Q) '' s))
    ((⇑φ : (a : P) → Q) '' intrinsicInterior 𝕜 s)
have inl : Eq.{u_4 + 1} (α := Set Q) (intrinsicInterior 𝕜 (image.{u_5, u_4} (α := P) (⇑φ : (a : P) → Q) ∅))
  (image.{u_5, u_4} (α := P) (⇑φ : (a : P) → Q) (intrinsicInterior 𝕜 ∅))
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- 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
inl :
  Eq.{u_4 + 1} (α := Set Q) (intrinsicInterior 𝕜 (image.{u_5, u_4} (α := P) (⇑φ : (a : P) → Q) ∅))
    (image.{u_5, u_4} (α := P) (⇑φ : (a : P) → Q) (intrinsicInterior 𝕜 ∅))
⊢ Eq.{u_4 + 1} (α := Set Q) (intrinsicInterior 𝕜 ((⇑φ : (a : P) → Q) '' s))
    ((⇑φ : (a : P) → Q) '' intrinsicInterior 𝕜 s)
have inr : ∀ (hs : s.Nonempty),
  Eq.{u_4 + 1} (α := Set Q) (intrinsicInterior 𝕜 ((⇑φ : (a : P) → Q) '' s))
    ((⇑φ : (a : P) → Q) '' intrinsicInterior 𝕜 s)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (hypothesis)
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
⊢ Eq.{u_4 + 1} (α := Set Q) (intrinsicInterior 𝕜 ((⇑φ : (a : P) → Q) '' s))
    ((⇑φ : (a : P) → Q) '' intrinsicInterior 𝕜 s)
have this : Nonempty.{u_5 + 1} (↑s : Type u_5)
Tactic: haveI : Nonempty s := hs.to_subtype
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (hypothesis)
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 : 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))
⊢ Eq.{u_4 + 1} (α := Set Q) (intrinsicInterior 𝕜 ((⇑φ : (a : P) → Q) '' s))
    ((⇑φ : (a : P) → Q) '' intrinsicInterior 𝕜 s)
have 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)))
Tactic: have : φ.toAffineMap ∘ (↑) ∘ f.symm = (↑) := funext isometryEquivMap.apply_symm_apply
-- 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)))
⊢ Eq.{u_4 + 1} (α := Set Q) (intrinsicInterior 𝕜 ((⇑φ : (a : P) → Q) '' s))
    ((⇑φ : (a : P) → Q) '' intrinsicInterior 𝕜 s)
have 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))
    (interior
      (Subtype.val (p := fun (x : Q) ↦
          Membership.mem (γ := AffineSubspace 𝕜 Q) (affineSpan 𝕜 ((⇑φ : (a : P) → Q) '' s)) x) ⁻¹'
        (⇑φ : (a : P) → Q) '' s)))
  ((⇑φ : (a : P) → Q) '' intrinsicInterior 𝕜 s)
Tactic: rw [intrinsicInterior, intrinsicInterior, ← φ.coe_toAffineMap, ← map_span φ.toAffineMap s, ← this,
    ← Function.comp_assoc, image_comp, image_comp, f.symm.image_interior, f.image_symm,
    ← preimage_comp, Function.comp_assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap,
    Function.comp_id, preimage_comp, φ.injective.preimage_image]
-- 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))
      (interior
        (Subtype.val (p := fun (x : Q) ↦
            Membership.mem (γ := AffineSubspace 𝕜 Q) (affineSpan 𝕜 ((⇑φ : (a : P) → Q) '' s)) x) ⁻¹'
          (⇑φ : (a : P) → Q) '' s)))
    ((⇑φ : (a : P) → Q) '' intrinsicInterior 𝕜 s)
⊢ Eq.{u_4 + 1} (α := Set Q) (intrinsicInterior 𝕜 ((⇑φ : (a : P) → Q) '' s))
    ((⇑φ : (a : P) → Q) '' intrinsicInterior 𝕜 s)
have 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))
    (interior
      (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))
      (interior (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)))
Tactic: rw [intrinsicInterior, intrinsicInterior, ← φ.coe_toAffineMap, ← map_span φ.toAffineMap s, ← this,
    ← Function.comp_assoc, image_comp, image_comp, f.symm.image_interior, f.image_symm,
    ← preimage_comp, Function.comp_assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap,
    Function.comp_id, preimage_comp, φ.injective.preimage_image]
-- 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
⊢ Eq.{u_4 + 1} (α := Set Q) (intrinsicFrontier 𝕜 ((⇑φ : (a : P) → Q) '' s))
    ((⇑φ : (a : P) → Q) '' intrinsicFrontier 𝕜 s)
have inl : Eq.{u_4 + 1} (α := Set Q) (intrinsicFrontier 𝕜 (image.{u_5, u_4} (α := P) (⇑φ : (a : P) → Q) ∅))
  (image.{u_5, u_4} (α := P) (⇑φ : (a : P) → Q) (intrinsicFrontier 𝕜 ∅))
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- 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
inl :
  Eq.{u_4 + 1} (α := Set Q) (intrinsicFrontier 𝕜 (image.{u_5, u_4} (α := P) (⇑φ : (a : P) → Q) ∅))
    (image.{u_5, u_4} (α := P) (⇑φ : (a : P) → Q) (intrinsicFrontier 𝕜 ∅))
⊢ Eq.{u_4 + 1} (α := Set Q) (intrinsicFrontier 𝕜 ((⇑φ : (a : P) → Q) '' s))
    ((⇑φ : (a : P) → Q) '' intrinsicFrontier 𝕜 s)
have inr : ∀ (hs : s.Nonempty),
  Eq.{u_4 + 1} (α := Set Q) (intrinsicFrontier 𝕜 ((⇑φ : (a : P) → Q) '' s))
    ((⇑φ : (a : P) → Q) '' intrinsicFrontier 𝕜 s)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty