awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Intrinsic
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]
    (closure[instTopologicalSpaceSubtype]
      (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s))

Tactic:
exact isClosed_closure

Premises used: isClosed_closure
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
⊢ 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
-- Module: Mathlib.Analysis.Convex.Intrinsic
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))
rw :
  s ⊆
    range (ι := ↥(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)

Tactic:
rw [intrinsicClosure, h.closure_eq_preimage_closure_image, Set.image_preimage_eq_inter_range,
    Set.image_preimage_eq_of_subset ?_, Subtype.range_coe]

Premises used: intrinsicClosure, Subtype.range_coe, Set.image_preimage_eq_inter_range, Set.image_preimage_eq_of_subset, Topology.IsInducing.closure_eq_preimage_closure_image
-- Module: Mathlib.Analysis.Convex.Intrinsic
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))
rw : s ⊆ (↑(affineSpan 𝕜 s) : Set P)
⊢ s ⊆
    range (ι := ↥(affineSpan 𝕜 s))
      (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))

Tactic:
rw [Subtype.range_coe]

Premises used: Subtype.range_coe
-- Module: Mathlib.Analysis.Convex.Intrinsic
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 ⊆ (↑(affineSpan 𝕜 s) : Set P)

Tactic:
apply subset_affineSpan

Premises used: subset_affineSpan
-- Module: Mathlib.Analysis.Convex.Intrinsic
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 𝕜 ∅))
inr :
  ∀ (hs : s.Nonempty),
    Eq.{u_4 + 1} (α := Set Q) (intrinsicInterior 𝕜 ((⇑φ : (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)

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
⊢ 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:
simp only [intrinsicInterior_empty, image_empty]

Premises used: intrinsicInterior_empty, Set.image_empty
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
⊢ Nonempty.{u_5 + 1} (↑s : Type u_5)

Tactic:
haveI : Nonempty s := hs.to_subtype
-- Module: Mathlib.Analysis.Convex.Intrinsic
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} (α := ↥(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
-- Module: Mathlib.Analysis.Convex.Intrinsic
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 𝕜 ∅))
inr :
  ∀ (hs : s.Nonempty),
    Eq.{u_4 + 1} (α := Set Q) (intrinsicFrontier 𝕜 ((⇑φ : (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)

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
⊢ 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:
simp
-- Module: Mathlib.Analysis.Convex.Intrinsic
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 𝕜 ∅))
inr :
  ∀ (hs : s.Nonempty),
    Eq.{u_4 + 1} (α := Set Q) (intrinsicClosure 𝕜 ((⇑φ : (a : P) → Q) '' s))
      ((⇑φ : (a : P) → Q) '' intrinsicClosure 𝕜 s)
⊢ 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

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
⊢ 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:
simp
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
h : ∀ (x : P), x ∈ intrinsicClosure 𝕜 s ↔ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ intrinsicClosure 𝕜 s = closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
ext x
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
⊢ x ∈ intrinsicClosure 𝕜 s ↔ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
simp only [mem_closure_iff, mem_intrinsicClosure]

Premises used: mem_closure_iff, mem_intrinsicClosure
-- Module: Mathlib.Analysis.Convex.Intrinsic
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

Tactic:
⟨?_, fun h => ⟨⟨x, _⟩, ?_, Subtype.coe_mk _ ?_⟩⟩

Premises used: Subtype.coe_mk, Subtype.mk, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
h₂ :
  ∀ (h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty),
    Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x
⊢ (∃ (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 _ ?_⟩⟩
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
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
⊢ (t ∩ s).Nonempty

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h _ (continuous_induced_dom.isOpen_preimage t ht) hx

Premises used: continuous_induced_dom, Continuous.isOpen_preimage
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
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:
⟨z, hz₁, hz₂⟩

Premises used: Set.Nonempty, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
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:
exact ⟨z, hz₁, hz₂⟩
-- Module: Mathlib.Analysis.Convex.Intrinsic
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 ⋯)
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)
⊢ 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
-- Module: Mathlib.Analysis.Convex.Intrinsic
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 ⋯)
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:
⟨⟨_, subset_affineSpan 𝕜 s hys⟩, hyt, hys⟩

Premises used: Subtype.mk, subset_affineSpan, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Intrinsic
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 ⋯)
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:
exact ⟨⟨_, subset_affineSpan 𝕜 s hys⟩, hyt, hys⟩
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
h₁ : ∀ (hc : x ∉ affineSpan 𝕜 s), False
⊢ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x

Tactic:
by_contra hc
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
h₁ : ∀ (z : P) (hz₁ : z ∈ (↑(affineSpan 𝕜 s) : Set P)ᶜ) (hz₂ : z ∈ s), False
⊢ False

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h _ (affineSpan 𝕜 s).closed_of_finiteDimensional.isOpen_compl hc

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
z : P
hz₁ : z ∈ (↑(affineSpan 𝕜 s) : Set P)ᶜ
hz₂ : z ∈ s
⊢ False

Tactic:
hz₁ (subset_affineSpan 𝕜 s hz₂)

Premises used: subset_affineSpan
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
z : P
hz₁ : z ∈ (↑(affineSpan 𝕜 s) : Set P)ᶜ
hz₂ : z ∈ s
⊢ False

Tactic:
exact hz₁ (subset_affineSpan 𝕜 s hz₂)

Premises used: subset_affineSpan
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s \ intrinsicInterior 𝕜 s = intrinsicFrontier 𝕜 s

Tactic:
intrinsicClosure_eq_closure 𝕜 s ▸ intrinsicClosure_diff_intrinsicInterior s

Premises used: Eq.rec, intrinsicClosure_diff_intrinsicInterior, intrinsicClosure_eq_closure
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s \ intrinsicFrontier 𝕜 s = intrinsicInterior 𝕜 s

Tactic:
intrinsicClosure_eq_closure 𝕜 s ▸ intrinsicClosure_diff_intrinsicFrontier s

Premises used: intrinsicClosure_diff_intrinsicFrontier, Eq.rec, intrinsicClosure_eq_closure
-- Module: Mathlib.Analysis.Convex.Intrinsic
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
rw : Convex 𝕜 (closure[inst_4] s ∩ (↑(affineSpan 𝕜 s) : Set V))
⊢ Convex 𝕜 (intrinsicClosure 𝕜 s)

Tactic:
rw [intrinsicClosure_eq_closure_inter_affineSpan]

Premises used: intrinsicClosure_eq_closure_inter_affineSpan