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
⊢ Eq.{u_5 + 1} (α := Set P) (intrinsicInterior 𝕜 ∅) ∅

Tactic:
simp [intrinsicInterior]

Premises used: intrinsicInterior
-- 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
⊢ Eq.{u_5 + 1} (α := Set P) (intrinsicFrontier 𝕜 ∅) ∅

Tactic:
simp [intrinsicFrontier]

Premises used: intrinsicFrontier
-- 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
⊢ Eq.{u_5 + 1} (α := Set P) (intrinsicClosure 𝕜 ∅) ∅

Tactic:
simp [intrinsicClosure]

Premises used: intrinsicClosure
-- 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
simp_rw : intrinsicClosure 𝕜 s ≠ ∅ → s ≠ ∅
⊢ (intrinsicClosure 𝕜 s).Nonempty → s.Nonempty

Tactic:
simp_rw [nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty
-- 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
h : Ne.{u_5 + 1} (α := Set P) (intrinsicClosure 𝕜 ∅) ∅
⊢ False

Tactic:
h intrinsicClosure_empty

Premises used: intrinsicClosure_empty
-- 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
h : Ne.{u_5 + 1} (α := Set P) (intrinsicClosure 𝕜 ∅) ∅
⊢ False

Tactic:
exact h intrinsicClosure_empty

Premises used: intrinsicClosure_empty
-- 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
x : P
⊢ Eq (α := Set P) (intrinsicInterior 𝕜 {x}) {x}

Tactic:
simp only [intrinsicInterior, preimage_coe_affineSpan_singleton, interior_univ, image_univ,
    Subtype.range_coe_subtype, mem_affineSpan_singleton, setOf_eq_eq_singleton]

Premises used: Set.setOf_eq_eq_singleton, Set.image_univ, interior_univ, intrinsicInterior, Subtype.range_coe_subtype, AffineSubspace.preimage_coe_affineSpan_singleton, AffineSubspace.mem_affineSpan_singleton
-- 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
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)) ∅)
    ∅
rw₃ rw₄ : Eq.{u_5 + 1} (α := Set P) ∅ ∅
⊢ Eq (α := Set P) (intrinsicFrontier 𝕜 {x}) ∅

Tactic:
rw [intrinsicFrontier, preimage_coe_affineSpan_singleton, frontier_univ, image_empty]

Premises used: intrinsicFrontier, AffineSubspace.preimage_coe_affineSpan_singleton, frontier_univ, Set.image_empty
-- 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
x : P
⊢ Eq (α := Set P) (intrinsicClosure 𝕜 {x}) {x}

Tactic:
simp only [intrinsicClosure, preimage_coe_affineSpan_singleton, closure_univ, image_univ,
    Subtype.range_coe_subtype, mem_affineSpan_singleton, setOf_eq_eq_singleton]

Premises used: Set.setOf_eq_eq_singleton, Set.image_univ, intrinsicClosure, Subtype.range_coe_subtype, AffineSubspace.preimage_coe_affineSpan_singleton, AffineSubspace.mem_affineSpan_singleton, closure_univ
-- 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 t : Set P
h : s ⊆ t
⊢ intrinsicClosure 𝕜 s ⊆ intrinsicClosure 𝕜 t

Tactic:
image_subset_iff.2 fun x hx => ?_

Premises used: Iff.mpr, intrinsicClosure, Set.image_subset_iff
-- 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 t : Set P
h : s ⊆ t
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
⊢ intrinsicClosure 𝕜 s ⊆ intrinsicClosure 𝕜 t

Tactic:
refine image_subset_iff.2 fun x hx => ?_

Premises used: Iff.mpr, Set.image_subset_iff
-- 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 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

Tactic:
⟨Set.inclusion (affineSpan_mono _ h) x, ?_, rfl⟩

Premises used: intrinsicClosure, Set.Mem, setOf, Set.preimage, And.intro, Exists.intro, Set.inclusion, Set.image, affineSpan_mono, rfl
-- 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 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
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)) ⋯ x)
⊢ Membership.mem (γ := Set ↥(affineSpan 𝕜 s))
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹'
      intrinsicClosure 𝕜 t)
    x

Tactic:
refine ⟨Set.inclusion (affineSpan_mono _ h) x, ?_, rfl⟩
-- 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 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)

Tactic:
(continuous_inclusion (affineSpan_mono _ h)).closure_preimage_subset _ (closure_mono ?_ hx)

Premises used: Set.Mem, setOf, closure_mono, continuous_inclusion, closure, Set.preimage, affineSpan_mono, Set.sInter, Continuous.closure_preimage_subset
-- 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 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
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)) ⋯ ⁻¹'
      Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 t) x) ⁻¹' t)
⊢ 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)

Tactic:
refine (continuous_inclusion (affineSpan_mono _ h)).closure_preimage_subset _ (closure_mono ?_ hx)

Premises used: closure_mono, continuous_inclusion, affineSpan_mono, Continuous.closure_preimage_subset
-- 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 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
⊢ 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)) ⋯ ⁻¹'
      Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 t) x) ⁻¹' t)

Tactic:
fun y hy => h hy

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage
-- 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 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
⊢ 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)) ⋯ ⁻¹'
      Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 t) x) ⁻¹' t)

Tactic:
exact fun y hy => h hy
-- 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
⊢ interior s ⊆ intrinsicInterior 𝕜 s

Tactic:
fun x hx => ⟨⟨x, subset_affineSpan _ _ <| interior_subset hx⟩,
    preimage_interior_subset_interior_preimage continuous_subtype_val hx, rfl⟩

Premises used: interior_subset, continuous_subtype_val, Set.Mem, intrinsicInterior, setOf, preimage_interior_subset_interior_preimage, Set.Subset, Subtype.mk, subset_affineSpan, And.intro, Exists.intro, Set.image, rfl
-- 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
⊢ intrinsicClosure 𝕜 s ⊆ closure[inst_3] s

Tactic:
image_subset_iff.2 <| continuous_subtype_val.closure_preimage_subset _

Premises used: Iff.mpr, intrinsicClosure, continuous_subtype_val, Set.image_subset_iff, Continuous.closure_preimage_subset
-- 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
⊢ intrinsicFrontier 𝕜 s ⊆ frontier s

Tactic:
image_subset_iff.2 <| continuous_subtype_val.frontier_preimage_subset _

Premises used: Iff.mpr, intrinsicFrontier, continuous_subtype_val, Continuous.frontier_preimage_subset, Set.image_subset_iff
-- 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
⊢ intrinsicClosure 𝕜 s ⊆ (↑(affineSpan 𝕜 s) : Set P)

Tactic:
(image_subset_range _ _).trans Subtype.range_coe.subset

Premises used: intrinsicClosure, HasSubset.Subset.trans, Set.image_subset_range, Subtype.range_coe, Eq.subset
-- 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
rw :
  (fun (a : ↥(affineSpan 𝕜 s)) ↦ (↑a : P)) ''
      interior (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s) =
    intrinsicInterior 𝕜 s
rw₁ 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))
⊢ (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

Tactic:
rw [closure_diff_frontier, intrinsicInterior]

Premises used: intrinsicInterior, closure_diff_frontier
-- 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
⊢ intrinsicClosure 𝕜 s \ intrinsicInterior 𝕜 s = intrinsicFrontier 𝕜 s

Tactic:
(image_diff Subtype.coe_injective _ _).symm

Premises used: frontier, intrinsicFrontier, intrinsicClosure, intrinsicInterior, Set.image_diff, Subtype.coe_injective, Eq.symm
-- 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
⊢ intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s

Tactic:
simp [intrinsicClosure, intrinsicInterior, intrinsicFrontier, closure_eq_interior_union_frontier,
    image_union]

Premises used: intrinsicFrontier, intrinsicClosure, intrinsicInterior, closure_eq_interior_union_frontier, Set.image_union
-- 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
rw : intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s
rw₁ rw₂ : intrinsicClosure 𝕜 s = intrinsicClosure 𝕜 s
⊢ intrinsicFrontier 𝕜 s ∪ intrinsicInterior 𝕜 s = intrinsicClosure 𝕜 s

Tactic:
rw [union_comm, intrinsicInterior_union_intrinsicFrontier]

Premises used: intrinsicInterior_union_intrinsicFrontier, Set.union_comm
-- 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
hs : IsClosed[inst_3] (↑(affineSpan 𝕜 s) : Set P)
⊢ IsClosed[inst_3] (intrinsicClosure 𝕜 s)

Tactic:
hs.isClosedEmbedding_subtypeVal.isClosedMap _ isClosed_closure

Premises used: intrinsicClosure, Topology.IsClosedEmbedding.isClosedMap, IsClosed.isClosedEmbedding_subtypeVal, 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
hs : IsClosed[inst_3] (↑(affineSpan 𝕜 s) : Set P)
⊢ IsClosed[inst_3] (intrinsicFrontier 𝕜 s)

Tactic:
hs.isClosedEmbedding_subtypeVal.isClosedMap _ isClosed_frontier

Premises used: isClosed_frontier, intrinsicFrontier, Topology.IsClosedEmbedding.isClosedMap, IsClosed.isClosedEmbedding_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
⊢ Eq (α := AffineSubspace 𝕜 P) (affineSpan 𝕜 (intrinsicClosure 𝕜 s)) (affineSpan 𝕜 s)

Tactic:
(affineSpan_le.2 intrinsicClosure_subset_affineSpan).antisymm <|
    affineSpan_mono _ subset_intrinsicClosure

Premises used: Iff.mpr, subset_intrinsicClosure, LE.le.antisymm, affineSpan_le, affineSpan_mono, intrinsicClosure_subset_affineSpan
-- 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
hs :
  IsClosed[instTopologicalSpaceSubtype]
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)
rw :
  s ⊆
    range (ι := ↥(affineSpan 𝕜 s))
      (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))
⊢ intrinsicClosure 𝕜 s = s

Tactic:
rw [intrinsicClosure, hs.closure_eq, image_preimage_eq_of_subset]

Premises used: intrinsicClosure, IsClosed.closure_eq, Set.image_preimage_eq_of_subset
-- 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
hs :
  IsClosed[instTopologicalSpaceSubtype]
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)
⊢ s ⊆
    range (ι := ↥(affineSpan 𝕜 s))
      (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))

Tactic:
(subset_affineSpan _ _).trans Subtype.range_coe.superset

Premises used: HasSubset.Subset.trans, Subtype.range_coe, subset_affineSpan, Eq.superset
-- 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
hs :
  IsClosed[instTopologicalSpaceSubtype]
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s)
⊢ s ⊆
    range (ι := ↥(affineSpan 𝕜 s))
      (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x))

Tactic:
exact (subset_affineSpan _ _).trans Subtype.range_coe.superset

Premises used: HasSubset.Subset.trans, Subtype.range_coe, subset_affineSpan, Eq.superset
-- 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
⊢ intrinsicClosure 𝕜 (intrinsicClosure 𝕜 s) = intrinsicClosure 𝕜 s

Tactic:
IsClosed.intrinsicClosure ?_

Premises used: IsClosed.intrinsicClosure
-- 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
refine :
  IsClosed[instTopologicalSpaceSubtype]
    (Subtype.val (p := fun (x : P) ↦
        Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 (intrinsicClosure 𝕜 s)) x) ⁻¹'
      intrinsicClosure 𝕜 s)
⊢ intrinsicClosure 𝕜 (intrinsicClosure 𝕜 s) = intrinsicClosure 𝕜 s

Tactic:
refine IsClosed.intrinsicClosure ?_

Premises used: IsClosed.intrinsicClosure
-- 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
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)
⊢ IsClosed[instTopologicalSpaceSubtype]
    (Subtype.val (p := fun (x : P) ↦
        Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 (intrinsicClosure 𝕜 s)) x) ⁻¹'
      intrinsicClosure 𝕜 s)

Tactic:
set t := affineSpan 𝕜 (intrinsicClosure 𝕜 s) with ht

Premises used: intrinsicClosure, affineSpan
-- 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
t : AffineSubspace 𝕜 P := affineSpan 𝕜 (intrinsicClosure 𝕜 s)
ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
clear_value :
  ∀ (t : AffineSubspace 𝕜 P) (ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)),
    IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : P) ↦ x ∈ t) ⁻¹' intrinsicClosure 𝕜 s)
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : P) ↦ x ∈ t) ⁻¹' intrinsicClosure 𝕜 s)

Tactic:
clear_value t
-- 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
t : AffineSubspace 𝕜 P
ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
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)
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : P) ↦ x ∈ t) ⁻¹' intrinsicClosure 𝕜 s)

Tactic:
obtain rfl := ht.trans (affineSpan_intrinsicClosure _)

Premises used: affineSpan_intrinsicClosure, rfl, Eq.trans
-- 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))
rw :
  IsClosed[instTopologicalSpaceSubtype]
    (closure[instTopologicalSpaceSubtype]
      (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s))
⊢ IsClosed[instTopologicalSpaceSubtype]
    (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹'
      intrinsicClosure 𝕜 s)

Tactic:
rw [intrinsicClosure, preimage_image_eq _ Subtype.coe_injective]

Premises used: intrinsicClosure, Subtype.coe_injective, Set.preimage_image_eq
-- 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:
isClosed_closure

Premises used: isClosed_closure