awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
    0
hb₂ :
  (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ V
x : E
hx : x ∈ s
⊢ Membership.mem (γ := Set E)
    ((fun (x : E) ↦
        HAdd.hAdd (α := Set E)
          (interior
            ((convexHull ℝ : (a : Set E) → Set E)
              (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
          {x})
      x)
    x

Tactic:
simpa using hb₁
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
    0
hb₂ :
  (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ V
rcases :
  ∀ (u : Set E) (hu₁ : u ⊆ s) (hu₂ : u.Finite)
    (hu₃ :
      s ⊆
        ⋃ i ∈ u,
          HAdd.hAdd (α := Set E)
            (interior
              ((convexHull ℝ : (a : Set E) → Set E)
                (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
            {i}),
    ∃ (u : Finset E),
      s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
        (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
⊢ ∃ (u : Finset E),
    s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
      (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t

Tactic:
rcases hs₂.elim_finite_subcover_image (b := s)
      (c := fun x => interior (convexHull ℝ (Set.range b)) + {x})
      (fun _ _ => isOpen_interior.add_right)
      (fun x hx => Set.mem_iUnion₂_of_mem hx <| by simpa using hb₁)
    with ⟨u, hu₁, hu₂, hu₃⟩

Premises used: isOpen_interior, Set.mem_iUnion₂_of_mem, IsOpen.add_right, IsCompact.elim_finite_subcover_image
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
    0
hb₂ :
  (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ V
u : Set E
hu₁ : u ⊆ s
hu₂ : u.Finite
hu₃ :
  s ⊆
    ⋃ i ∈ u,
      HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i}
⊢ u.Finite

Tactic:
hu₂
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
    0
hb₂ :
  (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ V
u : Set E
hu₁ : u ⊆ s
hu₂ : u.Finite
hu₃ :
  s ⊆
    ⋃ i ∈ u,
      HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i}
lift :
  ∀ (u : Finset E) (hu₁ : (↑u : Set E) ⊆ s)
    (hu₃ :
      s ⊆
        ⋃ i ∈ (↑u : Set E),
          HAdd.hAdd (α := Set E)
            (interior
              ((convexHull ℝ : (a : Set E) → Set E)
                (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
            {i}),
    ∃ (u : Finset E),
      s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
        (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
⊢ ∃ (u : Finset E),
    s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
      (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t

Tactic:
lift u to Finset E using hu₂

Premises used: Finset
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
    0
hb₂ :
  (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ V
u : Finset E
hu₁ : (↑u : Set E) ⊆ s
hu₃ :
  s ⊆
    ⋃ i ∈ (↑u : Set E),
      HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i}
⊢ ∃ (u : Finset E),
    s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
      (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t

Tactic:
⟨Finset.univ.image b + u, ?_, ?_⟩

Premises used: Finset.univ, HAdd.hAdd, And.intro, Exists.intro, DFunLike.coe, Finset.image
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
    0
hb₂ :
  (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ V
u : Finset E
hu₁ : (↑u : Set E) ⊆ s
hu₃ :
  s ⊆
    ⋃ i ∈ (↑u : Set E),
      HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i}
refine_1 :
  s ⊆
    interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (↑(Finset.image (α := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E) Finset.univ + u) : Set E))
refine_2 :
  (convexHull ℝ : (a : Set E) → Set E)
      (↑(Finset.image (α := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E) Finset.univ + u) : Set E) ⊆
    t
⊢ ∃ (u : Finset E),
    s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
      (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t

Tactic:
refine ⟨Finset.univ.image b + u, ?_, ?_⟩
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
    0
hb₂ :
  (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ V
u : Finset E
hu₁ : (↑u : Set E) ⊆ s
hu₃ :
  s ⊆
    ⋃ i ∈ (↑u : Set E),
      HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i}
refine_1 :
  s ⊆
    interior
      (HAdd.hAdd (α := Set E) (β := Set E)
        ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) :
          Set E)
        ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) : Set E))
⊢ s ⊆
    interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (↑(Finset.image (α := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E) Finset.univ + u) : Set E))

Tactic:
rw [Finset.coe_add, Finset.coe_image, Finset.coe_univ, Set.image_univ, convexHull_add]

Premises used: Set.image_univ, Finset.coe_univ, convexHull_add, Finset.coe_image, Finset.coe_add
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
    0
hb₂ :
  (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ V
u : Finset E
hu₁ : (↑u : Set E) ⊆ s
hu₃ :
  s ⊆
    ⋃ i ∈ (↑u : Set E),
      HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i}
refine_2 :
  HAdd.hAdd (α := Set E) (β := Set E)
      ((convexHull ℝ : (a : Set E) → Set E)
          (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) :
        Set E)
      ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) : Set E) ⊆
    t
⊢ (convexHull ℝ : (a : Set E) → Set E)
      (↑(Finset.image (α := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E) Finset.univ + u) : Set E) ⊆
    t

Tactic:
rw [Finset.coe_add, Finset.coe_image, Finset.coe_univ, Set.image_univ, convexHull_add]

Premises used: Set.image_univ, Finset.coe_univ, convexHull_add, Finset.coe_image, Finset.coe_add
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
    0
hb₂ :
  (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ V
u : Finset E
hu₁ : (↑u : Set E) ⊆ s
hu₃ :
  s ⊆
    ⋃ i ∈ (↑u : Set E),
      HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i}
refine_1 :
  ∀ (i : E) (j : i ∈ (↑u : Set E)),
    HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i} ⊆
      interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))) +
        (↑u : Set E)
⊢ s ⊆
    interior
      (HAdd.hAdd (α := Set E) (β := Set E)
        ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) :
          Set E)
        ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) : Set E))

Tactic:
grw [hu₃, ← subset_interior_add_left, Set.iUnion₂_subset_iff, ← subset_convexHull _ (u : Set E)]

Premises used: subset_convexHull, subset_interior_add_left, SetLike.coe, Set.iUnion₂_subset_iff
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
    0
hb₂ :
  (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ V
u : Finset E
hu₁ : (↑u : Set E) ⊆ s
hu₃ :
  s ⊆
    ⋃ i ∈ (↑u : Set E),
      HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i}
i : E
j : i ∈ (↑u : Set E)
refine_1 : {i} ⊆ (↑u : Set E)
⊢ HAdd.hAdd (α := Set E)
      (interior
        ((convexHull ℝ : (a : Set E) → Set E)
          (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
      {i} ⊆
    interior
        ((convexHull ℝ : (a : Set E) → Set E)
          (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))) +
      (↑u : Set E)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
    0
hb₂ :
  (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ V
u : Finset E
hu₁ : (↑u : Set E) ⊆ s
hu₃ :
  s ⊆
    ⋃ i ∈ (↑u : Set E),
      HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i}
i : E
j : i ∈ (↑u : Set E)
⊢ {i} ⊆ (↑u : Set E)

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
    0
hb₂ :
  (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆ V
u : Finset E
hu₁ : (↑u : Set E) ⊆ s
hu₃ :
  s ⊆
    ⋃ i ∈ (↑u : Set E),
      HAdd.hAdd (α := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        {i}
refine_2 :
  HAdd.hAdd (α := Set E) (β := Set E)
      ((convexHull ℝ : (a : Set E) → Set E)
          (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) :
        Set E)
      ((convexHull ℝ : (a : Set E) → Set E) s : Set E) ⊆
    t
refine_2₁ :
  HAdd.hAdd (α := Set E)
      ((convexHull ℝ : (a : Set E) → Set E)
          (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) :
        Set E)
      s ⊆
    t
refine_2₂ : V + s ⊆ t
refine_2₃ : U ⊆ t
refine_2₄ refine_2₅ : t ⊆ t
⊢ HAdd.hAdd (α := Set E) (β := Set E)
      ((convexHull ℝ : (a : Set E) → Set E)
          (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) :
        Set E)
      ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) : Set E) ⊆
    t

Tactic:
grw [hu₁, hs₁.convexHull_eq, hb₂, hV₂, hU₃]

Premises used: Convex.convexHull_eq
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : SeminormedAddCommGroup V₂
inst_6 : NormedSpace 𝕜 V₂
inst_7 : PseudoMetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
h :
  ∀ (x : V),
    Eq.{u_5 + 1} (α := V₂) ((f.linear : (a : V) → V₂) x : V₂) ((f.linearIsometry.toLinearMap : (a : V) → V₂) x : V₂)
⊢ f.linear = f.linearIsometry.toLinearMap

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : SeminormedAddCommGroup V₂
inst_6 : NormedSpace 𝕜 V₂
inst_7 : PseudoMetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
x : V
⊢ Eq.{u_5 + 1} (α := V₂) ((f.linear : (a : V) → V₂) x : V₂) ((f.linearIsometry.toLinearMap : (a : V) → V₂) x : V₂)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₁' : Type u_4
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
P₁ : Type u_8
P₁' : Type u_9
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
P₄ : Type u_13
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : SeminormedAddCommGroup V₁
inst_6 : NormedSpace 𝕜 V₁
inst_7 : PseudoMetricSpace P₁
inst_8 : NormedAddTorsor V₁ P₁
inst_9 : SeminormedAddCommGroup V₁'
inst_10 : NormedSpace 𝕜 V₁'
inst_11 : MetricSpace P₁'
inst_12 : NormedAddTorsor V₁' P₁'
inst_13 : SeminormedAddCommGroup V₂
inst_14 : NormedSpace 𝕜 V₂
inst_15 : PseudoMetricSpace P₂
inst_16 : NormedAddTorsor V₂ P₂
inst_17 : SeminormedAddCommGroup V₃
inst_18 : NormedSpace 𝕜 V₃
inst_19 : PseudoMetricSpace P₃
inst_20 : NormedAddTorsor V₃ P₃
inst_21 : SeminormedAddCommGroup V₄
inst_22 : NormedSpace 𝕜 V₄
inst_23 : PseudoMetricSpace P₄
inst_24 : NormedAddTorsor V₄ P₄
f_1 f g : P →ᵃⁱ[𝕜] P₂
mk :
  ∀ (toAffineMap : P →ᵃ[𝕜] P₂)
    (norm_map : ∀ (x : V), norm.{u_5} (E := V₂) ((toAffineMap.linear : (a : V) → V₂) x : V₂) = ‖x‖),
    Eq (α := (a : P) → P₂) ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) { toAffineMap := toAffineMap, norm_map := norm_map })
        ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) g) →
      { toAffineMap := toAffineMap, norm_map := norm_map : P →ᵃⁱ[𝕜] P₂ } = g
⊢ Eq (α := (a : P) → P₂) ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) f) ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) g) → f = g

Tactic:
cases f
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₁' : Type u_4
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
P₁ : Type u_8
P₁' : Type u_9
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
P₄ : Type u_13
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : SeminormedAddCommGroup V₁
inst_6 : NormedSpace 𝕜 V₁
inst_7 : PseudoMetricSpace P₁
inst_8 : NormedAddTorsor V₁ P₁
inst_9 : SeminormedAddCommGroup V₁'
inst_10 : NormedSpace 𝕜 V₁'
inst_11 : MetricSpace P₁'
inst_12 : NormedAddTorsor V₁' P₁'
inst_13 : SeminormedAddCommGroup V₂
inst_14 : NormedSpace 𝕜 V₂
inst_15 : PseudoMetricSpace P₂
inst_16 : NormedAddTorsor V₂ P₂
inst_17 : SeminormedAddCommGroup V₃
inst_18 : NormedSpace 𝕜 V₃
inst_19 : PseudoMetricSpace P₃
inst_20 : NormedAddTorsor V₃ P₃
inst_21 : SeminormedAddCommGroup V₄
inst_22 : NormedSpace 𝕜 V₄
inst_23 : PseudoMetricSpace P₄
inst_24 : NormedAddTorsor V₄ P₄
f g : P →ᵃⁱ[𝕜] P₂
toAffineMap : P →ᵃ[𝕜] P₂
norm_map : ∀ (x : V), norm.{u_5} (E := V₂) ((toAffineMap.linear : (a : V) → V₂) x : V₂) = ‖x‖
mk :
  ∀ (toAffineMap_1 : P →ᵃ[𝕜] P₂)
    (norm_map_1 : ∀ (x : V), norm.{u_5} (E := V₂) ((toAffineMap_1.linear : (a : V) → V₂) x : V₂) = ‖x‖),
    Eq (α := (a : P) → P₂) ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) { toAffineMap := toAffineMap, norm_map := norm_map })
        ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) { toAffineMap := toAffineMap_1, norm_map := norm_map_1 }) →
      { toAffineMap := toAffineMap, norm_map := norm_map : P →ᵃⁱ[𝕜] P₂ } =
        { toAffineMap := toAffineMap_1, norm_map := norm_map_1 }
⊢ Eq (α := (a : P) → P₂) ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) { toAffineMap := toAffineMap, norm_map := norm_map })
      ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) g) →
    { toAffineMap := toAffineMap, norm_map := norm_map : P →ᵃⁱ[𝕜] P₂ } = g

Tactic:
cases g
-- Module: Mathlib.Analysis.Normed.Affine.Isometry
Goal:
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₁' : Type u_4
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
P₁ : Type u_8
P₁' : Type u_9
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
P₄ : Type u_13
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
inst_5 : SeminormedAddCommGroup V₁
inst_6 : NormedSpace 𝕜 V₁
inst_7 : PseudoMetricSpace P₁
inst_8 : NormedAddTorsor V₁ P₁
inst_9 : SeminormedAddCommGroup V₁'
inst_10 : NormedSpace 𝕜 V₁'
inst_11 : MetricSpace P₁'
inst_12 : NormedAddTorsor V₁' P₁'
inst_13 : SeminormedAddCommGroup V₂
inst_14 : NormedSpace 𝕜 V₂
inst_15 : PseudoMetricSpace P₂
inst_16 : NormedAddTorsor V₂ P₂
inst_17 : SeminormedAddCommGroup V₃
inst_18 : NormedSpace 𝕜 V₃
inst_19 : PseudoMetricSpace P₃
inst_20 : NormedAddTorsor V₃ P₃
inst_21 : SeminormedAddCommGroup V₄
inst_22 : NormedSpace 𝕜 V₄
inst_23 : PseudoMetricSpace P₄
inst_24 : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
toAffineMap : P →ᵃ[𝕜] P₂
norm_map : ∀ (x : V), norm.{u_5} (E := V₂) ((toAffineMap.linear : (a : V) → V₂) x : V₂) = ‖x‖
toAffineMap_1 : P →ᵃ[𝕜] P₂
norm_map_1 : ∀ (x : V), norm.{u_5} (E := V₂) ((toAffineMap_1.linear : (a : V) → V₂) x : V₂) = ‖x‖
⊢ Eq (α := (a : P) → P₂) ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) { toAffineMap := toAffineMap, norm_map := norm_map })
      ((fun (f : P →ᵃⁱ[𝕜] P₂) ↦ f.toFun) { toAffineMap := toAffineMap_1, norm_map := norm_map_1 }) →
    { toAffineMap := toAffineMap, norm_map := norm_map : P →ᵃⁱ[𝕜] P₂ } =
      { toAffineMap := toAffineMap_1, norm_map := norm_map_1 }

Tactic:
simp