awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (intrinsicFrontier 𝕜 ((⇑φ : (a : P) → Q) '' s))
    ((⇑φ : (a : P) → Q) '' intrinsicFrontier 𝕜 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) (intrinsicFrontier 𝕜 ((⇑φ : (a : P) → Q) '' s))
    ((⇑φ : (a : P) → Q) '' intrinsicFrontier 𝕜 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) (intrinsicFrontier 𝕜 ((⇑φ : (a : P) → Q) '' s))
    ((⇑φ : (a : P) → Q) '' intrinsicFrontier 𝕜 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))
    (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)
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]
-- 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)
⊢ 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 (α := ↥(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)))
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]
-- 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) (intrinsicClosure 𝕜 ((⇑φ : (a : P) → Q) '' s)) ((⇑φ : (a : P) → Q) '' intrinsicClosure 𝕜 s)
have inl : Eq.{u_4 + 1} (α := Set Q) (intrinsicClosure 𝕜 (image.{u_5, u_4} (α := P) (⇑φ : (a : P) → Q) ∅))
  (image.{u_5, u_4} (α := P) (⇑φ : (a : P) → Q) (intrinsicClosure 𝕜 ∅))
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) (intrinsicClosure 𝕜 (image.{u_5, u_4} (α := P) (⇑φ : (a : P) → Q) ∅))
    (image.{u_5, u_4} (α := P) (⇑φ : (a : P) → Q) (intrinsicClosure 𝕜 ∅))
⊢ Eq.{u_4 + 1} (α := Set Q) (intrinsicClosure 𝕜 ((⇑φ : (a : P) → Q) '' s)) ((⇑φ : (a : P) → Q) '' intrinsicClosure 𝕜 s)
have inr : ∀ (hs : s.Nonempty),
  Eq.{u_4 + 1} (α := Set Q) (intrinsicClosure 𝕜 ((⇑φ : (a : P) → Q) '' s)) ((⇑φ : (a : P) → Q) '' intrinsicClosure 𝕜 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) (intrinsicClosure 𝕜 ((⇑φ : (a : P) → Q) '' s)) ((⇑φ : (a : P) → Q) '' intrinsicClosure 𝕜 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) (intrinsicClosure 𝕜 ((⇑φ : (a : P) → Q) '' s)) ((⇑φ : (a : P) → Q) '' intrinsicClosure 𝕜 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
P : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace 𝕜 V
inst_4 : FiniteDimensional 𝕜 V
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
s : Set P
⊢ intrinsicClosure 𝕜 s = closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
have h : ∀ (x : P), x ∈ intrinsicClosure 𝕜 s ↔ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace 𝕜 V
inst_4 : FiniteDimensional 𝕜 V
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
s : Set P
x : P
⊢ x ∈ intrinsicClosure 𝕜 s ↔ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
have h : (∃ (y : ↥(affineSpan 𝕜 s)),
    (∀ (o : Set ↥(affineSpan 𝕜 s)),
        IsOpen[instTopologicalSpaceSubtype] o →
          y ∈ o →
            (o ∩
                Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹'
                  s).Nonempty) ∧
      (↑y : P) = x) ↔
  ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
Tactic: simp only [mem_closure_iff, mem_intrinsicClosure]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace 𝕜 V
inst_4 : FiniteDimensional 𝕜 V
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
s : Set P
x : P
⊢ (∃ (y : ↥(affineSpan 𝕜 s)),
      (∀ (o : Set ↥(affineSpan 𝕜 s)),
          IsOpen[instTopologicalSpaceSubtype] o →
            y ∈ o →
              (o ∩
                  Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹'
                    s).Nonempty) ∧
        (↑y : P) = x) ↔
    ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
have h : (∃ (y : ↥(affineSpan 𝕜 s)),
    (∀ (o : Set ↥(affineSpan 𝕜 s)),
        IsOpen[instTopologicalSpaceSubtype] o →
          y ∈ o →
            (o ∩
                Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹'
                  s).Nonempty) ∧
      (↑y : P) = x) →
  ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
Tactic: refine ⟨?_, fun h => ⟨⟨x, _⟩, ?_, Subtype.coe_mk _ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace 𝕜 V
inst_4 : FiniteDimensional 𝕜 V
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
s : Set P
x : P
h :
  (∃ (y : ↥(affineSpan 𝕜 s)),
      (∀ (o : Set ↥(affineSpan 𝕜 s)),
          IsOpen[instTopologicalSpaceSubtype] o →
            y ∈ o →
              (o ∩
                  Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹'
                    s).Nonempty) ∧
        (↑y : P) = x) →
    ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
⊢ (∃ (y : ↥(affineSpan 𝕜 s)),
      (∀ (o : Set ↥(affineSpan 𝕜 s)),
          IsOpen[instTopologicalSpaceSubtype] o →
            y ∈ o →
              (o ∩
                  Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹'
                    s).Nonempty) ∧
        (↑y : P) = x) ↔
    ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
have h₁ : ∀ (h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty)
  (o : Set ↥(affineSpan 𝕜 s)),
  IsOpen[instTopologicalSpaceSubtype] o →
    Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) x sorry ∈ o →
      (o ∩ Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s).Nonempty
Tactic: refine ⟨?_, fun h => ⟨⟨x, _⟩, ?_, Subtype.coe_mk _ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace 𝕜 V
inst_4 : FiniteDimensional 𝕜 V
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
s : Set P
x : P
h :
  (∃ (y : ↥(affineSpan 𝕜 s)),
      (∀ (o : Set ↥(affineSpan 𝕜 s)),
          IsOpen[instTopologicalSpaceSubtype] o →
            y ∈ o →
              (o ∩
                  Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹'
                    s).Nonempty) ∧
        (↑y : P) = x) →
    ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
h₁ :
  ∀ (h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty)
    (o : Set ↥(affineSpan 𝕜 s)),
    IsOpen[instTopologicalSpaceSubtype] o →
      Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) x ⋯ ∈ o →
        (o ∩
            Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s).Nonempty
⊢ (∃ (y : ↥(affineSpan 𝕜 s)),
      (∀ (o : Set ↥(affineSpan 𝕜 s)),
          IsOpen[instTopologicalSpaceSubtype] o →
            y ∈ o →
              (o ∩
                  Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹'
                    s).Nonempty) ∧
        (↑y : P) = x) ↔
    ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
have h₂ : ∀ (h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty),
  Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x
Tactic: refine ⟨?_, fun h => ⟨⟨x, _⟩, ?_, Subtype.coe_mk _ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace 𝕜 V
inst_4 : FiniteDimensional 𝕜 V
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
s : Set P
x : ↥(affineSpan 𝕜 s)
h :
  ∀ (o : Set ↥(affineSpan 𝕜 s)),
    IsOpen[instTopologicalSpaceSubtype] o →
      x ∈ o →
        (o ∩
            Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s).Nonempty
t : Set P
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hx : (↑x : P) ∈ t
⊢ (t ∩ s).Nonempty
have h₁ : ∀ (z : ↥(affineSpan 𝕜 s))
  (hz₁ :
    Membership.mem (γ := Set ↥(affineSpan 𝕜 s))
      (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' t) z)
  (hz₂ :
    Membership.mem (γ := Set ↥(affineSpan 𝕜 s))
      (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s) z),
  (t ∩ s).Nonempty
Tactic: obtain ⟨z, hz₁, hz₂⟩ := h _ (continuous_induced_dom.isOpen_preimage t ht) hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace 𝕜 V
inst_4 : FiniteDimensional 𝕜 V
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
t : Set P
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hx :
  Membership.mem (γ := Set ↥(affineSpan 𝕜 s))
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' t)
    (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) x ⋯)
⊢ Set.Nonempty (α := ↥(affineSpan 𝕜 s))
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' t ∩
      Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)
have h₁ : ∀ (y : P) (hyt : y ∈ t) (hys : y ∈ s),
  Set.Nonempty (α := ↥(affineSpan 𝕜 s))
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' t ∩
      Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)
Tactic: obtain ⟨y, hyt, hys⟩ := h _ ht hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace 𝕜 V
inst_4 : FiniteDimensional 𝕜 V
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
⊢ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x
have h₁ : ∀ (hc : x ∉ affineSpan 𝕜 s), False
Tactic: by_contra hc
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace 𝕜 V
inst_4 : FiniteDimensional 𝕜 V
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
hc : x ∉ affineSpan 𝕜 s
⊢ False
have h₁ : ∀ (z : P) (hz₁ : z ∈ (↑(affineSpan 𝕜 s) : Set P)ᶜ) (hz₂ : z ∈ s), False
Tactic: obtain ⟨z, hz₁, hz₂⟩ := h _ (affineSpan 𝕜 s).closed_of_finiteDimensional.isOpen_compl hc
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : AddCommGroup V
inst_3 : Module 𝕜 V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousConstSMul 𝕜 V
s : Set V
hs : Convex 𝕜 s
⊢ Convex 𝕜 (intrinsicClosure 𝕜 s)
have rw : Convex 𝕜 (closure[inst_4] s ∩ (↑(affineSpan 𝕜 s) : Set V))
Tactic: rw [intrinsicClosure_eq_closure_inter_affineSpan]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
α : Type u_6
β : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
φ : α ≃ₜ β
s : Set β
⊢ (interior s).Nonempty ↔ Set.Nonempty.{u_6} (α := α) (interior ((⇑φ : (a : α) → β) ⁻¹' s))
have rw : (interior s).Nonempty ↔ Set.Nonempty.{u_6} (α := α) (interior ((⇑φ.symm : (a : β) → α) '' s))
Tactic: rw [← φ.image_symm, ← φ.symm.image_interior, image_nonempty]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
α : Type u_6
β : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
φ : α ≃ₜ β
s : Set β
rw : (interior s).Nonempty ↔ Set.Nonempty.{u_6} (α := α) (interior ((⇑φ.symm : (a : β) → α) '' s))
⊢ (interior s).Nonempty ↔ Set.Nonempty.{u_6} (α := α) (interior ((⇑φ : (a : α) → β) ⁻¹' s))
have rw₁ : (interior s).Nonempty ↔ Set.Nonempty.{u_6} (α := α) ((⇑φ.symm : (a : β) → α) '' interior s)
Tactic: rw [← φ.image_symm, ← φ.symm.image_interior, image_nonempty]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
α : Type u_6
β : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
φ : α ≃ₜ β
s : Set β
rw : (interior s).Nonempty ↔ Set.Nonempty.{u_6} (α := α) (interior ((⇑φ.symm : (a : β) → α) '' s))
rw₁ : (interior s).Nonempty ↔ Set.Nonempty.{u_6} (α := α) ((⇑φ.symm : (a : β) → α) '' interior s)
⊢ (interior s).Nonempty ↔ Set.Nonempty.{u_6} (α := α) (interior ((⇑φ : (a : α) → β) ⁻¹' s))
have rw₂ : (interior s).Nonempty ↔ (interior s).Nonempty
Tactic: rw [← φ.image_symm, ← φ.symm.image_interior, image_nonempty]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (hypothesis)
Goal:
V : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
hsne : s.Nonempty
⊢ (intrinsicInterior ℝ s).Nonempty
have this : Nonempty.{u_2 + 1} (↑s : Type u_2)
Tactic: haveI := hsne.coe_sort
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
V : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
hsne : s.Nonempty
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
⊢ (intrinsicInterior ℝ s).Nonempty
have obtain : ∀ (p : V) (hp : p ∈ s), (intrinsicInterior ℝ s).Nonempty
Tactic: obtain ⟨p, hp⟩ := hsne
Cleared hypotheses: hsne
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
V : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) :=
  Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := AffineSubspace ℝ V) (_root_.affineSpan ℝ s) x) p ⋯
⊢ (intrinsicInterior ℝ s).Nonempty
have rw : Convex ℝ (E := ↥(direction (_root_.affineSpan ℝ s)))
  (Set.preimage (β := ↥(_root_.affineSpan ℝ s))
    (⇑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.symm (AffineIsometryEquiv.constVSub ℝ p'))) :
      (a : ↥(_root_.affineSpan ℝ s).direction) → ↥(_root_.affineSpan ℝ s))
    (Subtype.val (p := fun (x : V) ↦ Membership.mem (γ := AffineSubspace ℝ V) (_root_.affineSpan ℝ s) x) ⁻¹' s))
Tactic: rw [intrinsicInterior, image_nonempty,
    aux (AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph,
    Convex.interior_nonempty_iff_affineSpan_eq_top, AffineIsometryEquiv.coe_toHomeomorph, ←
    AffineIsometryEquiv.coe_toAffineEquiv, ← comap_span, affineSpan_coe_preimage_eq_top, comap_top]