awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : Membership.mem (γ := Filter E) (𝓝 0) t
htb : IsVonNBounded ℝ t
⊢ (⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb).symm : (a : E) → E) '' closure[inst_2] t ⊆ closure[inst_2] s

Tactic:
exact (mapsTo_gaugeRescale_closure htc ht₀ hsc
    (mem_of_mem_nhds hs₀) (absorbent_nhds_zero hs₀)).image_subset

Premises used: mapsTo_gaugeRescale_closure, absorbent_nhds_zero, mem_of_mem_nhds, Set.MapsTo.image_subset
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsne : (interior s).Nonempty
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htne : (interior t).Nonempty
htb : IsVonNBounded ℝ t
rsuffices :
  ∀ (e : E ≃ₜ E) (h₁ : (⇑e : (a : E) → E) '' interior s = interior t)
    (h₂ : (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t),
    ∃ (e : E ≃ₜ E),
      (⇑e : (a : E) → E) '' interior s = interior t ∧
        (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t ∧ (⇑e : (a : E) → E) '' frontier s = frontier t
rsuffices₁ :
  ∃ (e : E ≃ₜ E),
    (⇑e : (a : E) → E) '' interior s = interior t ∧ (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t
⊢ ∃ (e : E ≃ₜ E),
    (⇑e : (a : E) → E) '' interior s = interior t ∧
      (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t ∧ (⇑e : (a : E) → E) '' frontier s = frontier t

Tactic:
rsuffices ⟨e, h₁, h₂⟩ : ∃ e : E ≃ₜ E, e '' interior s = interior t ∧ e '' closure s = closure t

Premises used: closure, interior
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsne : (interior s).Nonempty
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htne : (interior t).Nonempty
htb : IsVonNBounded ℝ t
e : E ≃ₜ E
h₁ : (⇑e : (a : E) → E) '' interior s = interior t
h₂ : (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t
⊢ ∃ (e : E ≃ₜ E),
    (⇑e : (a : E) → E) '' interior s = interior t ∧
      (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t ∧ (⇑e : (a : E) → E) '' frontier s = frontier t

Tactic:
⟨e, h₁, h₂, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsne : (interior s).Nonempty
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htne : (interior t).Nonempty
htb : IsVonNBounded ℝ t
e : E ≃ₜ E
h₁ : (⇑e : (a : E) → E) '' interior s = interior t
h₂ : (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t
refine : (⇑e : (a : E) → E) '' frontier s = frontier t
⊢ ∃ (e : E ≃ₜ E),
    (⇑e : (a : E) → E) '' interior s = interior t ∧
      (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t ∧ (⇑e : (a : E) → E) '' frontier s = frontier t

Tactic:
refine ⟨e, h₁, h₂, ?_⟩
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsne : (interior s).Nonempty
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htne : (interior t).Nonempty
htb : IsVonNBounded ℝ t
e : E ≃ₜ E
h₁ : (⇑e : (a : E) → E) '' interior s = interior t
h₂ : (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t
simp_rw : (⇑e : (a : E) → E) '' (closure[inst_2] s \ interior s) = closure[inst_2] t \ interior t
simp_rw₁ : (⇑e : (a : E) → E) '' closure[inst_2] s \ (⇑e : (a : E) → E) '' interior s = closure[inst_2] t \ interior t
simp_rw₂ : (⇑e : (a : E) → E) '' closure[inst_2] s \ interior t = closure[inst_2] t \ interior t
⊢ (⇑e : (a : E) → E) '' frontier s = frontier t

Tactic:
simp_rw [← closure_diff_interior, image_diff e.injective, h₁, h₂]

Premises used: Set.image_diff, Homeomorph.injective, closure_diff_interior
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsne : (interior s).Nonempty
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htne : (interior t).Nonempty
htb : IsVonNBounded ℝ t
rcases :
  ∀ (x : E) (hx : x ∈ interior s),
    ∃ (e : E ≃ₜ E),
      (⇑e : (a : E) → E) '' interior s = interior t ∧ (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t
⊢ ∃ (e : E ≃ₜ E),
    (⇑e : (a : E) → E) '' interior s = interior t ∧ (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t

Tactic:
rcases hsne with ⟨x, hx⟩
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htne : (interior t).Nonempty
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
rcases :
  ∀ (y : E) (hy : y ∈ interior t),
    ∃ (e : E ≃ₜ E),
      (⇑e : (a : E) → E) '' interior s = interior t ∧ (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t
⊢ ∃ (e : E ≃ₜ E),
    (⇑e : (a : E) → E) '' interior s = interior t ∧ (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t

Tactic:
rcases htne with ⟨y, hy⟩
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
hsc₁ : Convex ℝ (-x +ᵥ s)
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) (-x +ᵥ s)
hsb₁ : IsVonNBounded ℝ (-x +ᵥ s)
htc : Convex ℝ (-y +ᵥ t)
ht₀ : Membership.mem (γ := Filter E) (𝓝 0) (-y +ᵥ t)
htb₁ : IsVonNBounded ℝ (-y +ᵥ t)
⊢ E ≃ₜ E

Tactic:
apply gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t)

Premises used: HVAdd.hVAdd, gaugeRescaleHomeomorph, Neg.neg
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
⊢ Convex ℝ (-x +ᵥ s)

Tactic:
simp [← mem_interior_iff_mem_nhds, interior_vadd, mem_vadd_set_iff_neg_vadd_mem, *]

Premises used: mem_interior_iff_mem_nhds, interior_vadd, Set.mem_vadd_set_iff_neg_vadd_mem
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
⊢ Membership.mem (γ := Filter E) (𝓝 0) (-x +ᵥ s)

Tactic:
simp [← mem_interior_iff_mem_nhds, interior_vadd, mem_vadd_set_iff_neg_vadd_mem, *]

Premises used: mem_interior_iff_mem_nhds, interior_vadd, Set.mem_vadd_set_iff_neg_vadd_mem
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
⊢ IsVonNBounded ℝ (-x +ᵥ s)

Tactic:
simp [← mem_interior_iff_mem_nhds, interior_vadd, mem_vadd_set_iff_neg_vadd_mem, *]

Premises used: mem_interior_iff_mem_nhds, interior_vadd, Set.mem_vadd_set_iff_neg_vadd_mem
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
⊢ Convex ℝ (-y +ᵥ t)

Tactic:
simp [← mem_interior_iff_mem_nhds, interior_vadd, mem_vadd_set_iff_neg_vadd_mem, *]

Premises used: mem_interior_iff_mem_nhds, interior_vadd, Set.mem_vadd_set_iff_neg_vadd_mem
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
⊢ Membership.mem (γ := Filter E) (𝓝 0) (-y +ᵥ t)

Tactic:
simp [← mem_interior_iff_mem_nhds, interior_vadd, mem_vadd_set_iff_neg_vadd_mem, *]

Premises used: mem_interior_iff_mem_nhds, interior_vadd, Set.mem_vadd_set_iff_neg_vadd_mem
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
⊢ IsVonNBounded ℝ (-y +ᵥ t)

Tactic:
simp [← mem_interior_iff_mem_nhds, interior_vadd, mem_vadd_set_iff_neg_vadd_mem, *]

Premises used: mem_interior_iff_mem_nhds, interior_vadd, Set.mem_vadd_set_iff_neg_vadd_mem
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ ∃ (e : E ≃ₜ E),
    (⇑e : (a : E) → E) '' interior s = interior t ∧ (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t

Tactic:
⟨.trans (.addLeft (-x)) <| h.trans <| .addLeft y, ?_, ?_⟩

Premises used: Homeomorph.addLeft, And.intro, Exists.intro, Homeomorph.trans, Neg.neg
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
refine_1 :
  (⇑(Homeomorph.trans (Homeomorph.addLeft (-x)) (h.trans (Homeomorph.addLeft y))) : (a : E) → E) '' interior s =
    interior t
refine_2 :
  (⇑(Homeomorph.trans (Homeomorph.addLeft (-x)) (h.trans (Homeomorph.addLeft y))) : (a : E) → E) '' closure[inst_2] s =
    closure[inst_2] t
⊢ ∃ (e : E ≃ₜ E),
    (⇑e : (a : E) → E) '' interior s = interior t ∧ (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t

Tactic:
refine ⟨.trans (.addLeft (-x)) <| h.trans <| .addLeft y, ?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
simp_rw :
  (fun (a : E) ↦ HAdd.hAdd (β := E) y ((h : (a : E) → E) (-x + a) : E)) '' interior s =
    HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' (-x +ᵥ interior s))
simp_rw₁ :
  Eq (α := Set E) ((fun (a : E) ↦ HAdd.hAdd (β := E) y ((h : (a : E) → E) (-x + a) : E)) '' interior s)
    ((fun (x : E) ↦ y +ᵥ x) '' image (α := E) (⇑h : (a : E) → E) ((fun (x_1 : E) ↦ -x +ᵥ x_1) '' interior s))
simp_rw₂ :
  Eq (α := Set E) ((fun (a : E) ↦ HAdd.hAdd (β := E) y ((h : (a : E) → E) (-x + a) : E)) '' interior s)
    ((fun (x_1 : E) ↦ HVAdd.hVAdd (β := E) y ((h : (a : E) → E) (-x +ᵥ x_1) : E)) '' interior s)
⊢ (fun (a : E) ↦ HAdd.hAdd (β := E) y ((h : (a : E) → E) (-x + a) : E)) '' interior s =
    HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' interior (-x +ᵥ s))

Tactic:
simp_rw [interior_vadd, ← image_vadd, image_image, vadd_eq_add]

Premises used: Set.image_image, Set.image_vadd, interior_vadd, vadd_eq_add
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
rw : y +ᵥ interior (-y +ᵥ t) = interior t
rw₁ : y +ᵥ -y +ᵥ interior t = interior t
rw₂ rw₃ : interior t = interior t
⊢ HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' interior (-x +ᵥ s)) = interior t

Tactic:
rw [image_gaugeRescaleHomeomorph_interior, interior_vadd, vadd_neg_vadd]

Premises used: image_gaugeRescaleHomeomorph_interior, interior_vadd, vadd_neg_vadd
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
a :
  (fun (a : E) ↦ HAdd.hAdd (β := E) y ((h : (a : E) → E) (-x + a) : E)) '' interior s =
    HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' interior (-x +ᵥ s))
a₁ : HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' interior (-x +ᵥ s)) = interior t
⊢ (⇑(Homeomorph.trans (Homeomorph.addLeft (-x)) (h.trans (Homeomorph.addLeft y))) : (a : E) → E) '' interior s =
    interior t

Tactic:
calc
      (fun a ↦ y + h (-x + a)) '' interior s = y +ᵥ h '' interior (-x +ᵥ s) := by
        simp_rw [interior_vadd, ← image_vadd, image_image, vadd_eq_add]
      _ = _ := by rw [image_gaugeRescaleHomeomorph_interior, interior_vadd, vadd_neg_vadd]

Premises used: HVAdd.hVAdd, HAdd.hAdd, interior, DFunLike.coe, Neg.neg
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
simp_rw :
  (fun (a : E) ↦ HAdd.hAdd (β := E) y ((h : (a : E) → E) (-x + a) : E)) '' closure[inst_2] s =
    HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' (-x +ᵥ closure[inst_2] s))
simp_rw₁ :
  Eq (α := Set E) ((fun (a : E) ↦ HAdd.hAdd (β := E) y ((h : (a : E) → E) (-x + a) : E)) '' closure[inst_2] s)
    ((fun (x : E) ↦ y +ᵥ x) '' image (α := E) (⇑h : (a : E) → E) ((fun (x_1 : E) ↦ -x +ᵥ x_1) '' closure[inst_2] s))
simp_rw₂ :
  Eq (α := Set E) ((fun (a : E) ↦ HAdd.hAdd (β := E) y ((h : (a : E) → E) (-x + a) : E)) '' closure[inst_2] s)
    ((fun (x_1 : E) ↦ HVAdd.hVAdd (β := E) y ((h : (a : E) → E) (-x +ᵥ x_1) : E)) '' closure[inst_2] s)
⊢ (fun (a : E) ↦ HAdd.hAdd (β := E) y ((h : (a : E) → E) (-x + a) : E)) '' closure[inst_2] s =
    HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' closure[inst_2] (-x +ᵥ s))

Tactic:
simp_rw [closure_vadd, ← image_vadd, image_image, vadd_eq_add]

Premises used: Set.image_image, Set.image_vadd, vadd_eq_add, closure_vadd
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
rw : y +ᵥ closure[inst_2] (-y +ᵥ t) = closure[inst_2] t
rw₁ : y +ᵥ -y +ᵥ closure[inst_2] t = closure[inst_2] t
rw₂ rw₃ : closure[inst_2] t = closure[inst_2] t
⊢ HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' closure[inst_2] (-x +ᵥ s)) = closure[inst_2] t

Tactic:
rw [image_gaugeRescaleHomeomorph_closure, closure_vadd, vadd_neg_vadd]

Premises used: vadd_neg_vadd, image_gaugeRescaleHomeomorph_closure, closure_vadd
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
a :
  (fun (a : E) ↦ HAdd.hAdd (β := E) y ((h : (a : E) → E) (-x + a) : E)) '' closure[inst_2] s =
    HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' closure[inst_2] (-x +ᵥ s))
a₁ : HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' closure[inst_2] (-x +ᵥ s)) = closure[inst_2] t
⊢ (⇑(Homeomorph.trans (Homeomorph.addLeft (-x)) (h.trans (Homeomorph.addLeft y))) : (a : E) → E) '' closure[inst_2] s =
    closure[inst_2] t

Tactic:
calc
      (fun a ↦ y + h (-x + a)) '' closure s = y +ᵥ h '' closure (-x +ᵥ s) := by
        simp_rw [closure_vadd, ← image_vadd, image_image, vadd_eq_add]
      _ = _ := by rw [image_gaugeRescaleHomeomorph_closure, closure_vadd, vadd_neg_vadd]

Premises used: HVAdd.hVAdd, closure, HAdd.hAdd, DFunLike.coe, Neg.neg
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hc : Convex ℝ s
hne : (interior s).Nonempty
hb : Bornology.IsBounded s
⊢ Set.Nonempty.{u_1} (α := E) (interior (ball 0 1))

Tactic:
simp [isOpen_ball.interior_eq]

Premises used: Metric.isOpen_ball, IsOpen.interior_eq
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hc : Convex ℝ s
hne : (interior s).Nonempty
hb : Bornology.IsBounded s
⊢ ∃ (h : E ≃ₜ E),
    Eq (α := Set E) ((⇑h : (a : E) → E) '' interior s) (ball 0 1) ∧
      Eq (α := Set E) ((⇑h : (a : E) → E) '' closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
          (closedBall 0 1) ∧
        Eq (α := Set E) ((⇑h : (a : E) → E) '' frontier s) (sphere 0 1)

Tactic:
simpa [isOpen_ball.interior_eq, closure_ball, frontier_ball]
    using exists_homeomorph_image_eq hc hne (NormedSpace.isVonNBounded_of_isBounded _ hb)
    (convex_ball 0 1) (by simp [isOpen_ball.interior_eq]) (NormedSpace.isVonNBounded_ball _ _ _)

Premises used: NormedSpace.isVonNBounded_ball, NormedSpace.isVonNBounded_of_isBounded, convex_ball, Metric.isOpen_ball, exists_homeomorph_image_eq, frontier_ball, closure_ball, IsOpen.interior_eq, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
⊢ s ⊆ (convexHull 𝕜 : (a : Set E) → Set E) s

Tactic:
(convexHull 𝕜).le_closure s

Premises used: ClosureOperator.le_closure, convexHull
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
⊢ Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
(convexHull 𝕜).isClosed_closure s

Premises used: convexHull, Convex, ClosureOperator.isClosed_closure
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E)
    (⋂ (t : Set E), ⋂ (_ : s ⊆ t), ⋂ (_ : Convex 𝕜 t), t : Set E)

Tactic:
simp [convexHull, iInter_subtype, iInter_and]

Premises used: convexHull, Set.iInter_subtype, Set.iInter_and
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
x : E
simp_rw :
  Membership.mem (γ := Set E) (⋂ (t : Set E), ⋂ (_ : s ⊆ t), ⋂ (_ : Convex 𝕜 t), t) x ↔
    ∀ (t : Set E), s ⊆ t → Convex 𝕜 t → x ∈ t
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x ↔
    ∀ (t : Set E), s ⊆ t → Convex 𝕜 t → x ∈ t

Tactic:
simp_rw [convexHull_eq_iInter, mem_iInter]

Premises used: convexHull_eq_iInter, Set.mem_iInter
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t : Set E
⊢ s ⊆ t → Convex 𝕜 t → (convexHull 𝕜 : (a : Set E) → Set E) s ⊆ t

Tactic:
(convexHull 𝕜).closure_min

Premises used: ClosureOperator.closure_min, Convex
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t : Set E
ht : Convex 𝕜 t
⊢ (convexHull 𝕜 : (a : Set E) → Set E) s ⊆ t ↔ s ⊆ t

Tactic:
(show (convexHull 𝕜).IsClosed t from ht).closure_le_iff

Premises used: ClosureOperator.IsClosed.closure_le_iff
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t : Set E
hst : s ⊆ t
⊢ Subset (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) ((convexHull 𝕜 : (a : Set E) → Set E) t : Set E)

Tactic:
(convexHull 𝕜).monotone hst

Premises used: convexHull, ClosureOperator.monotone
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜 : (a : Set E) → Set E) s = s ↔ Convex 𝕜 s

Tactic:
(convexHull 𝕜).isClosed_iff.symm

Premises used: convexHull, ClosureOperator.isClosed_iff, Convex, Iff.symm
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
⊢ Eq.{u_2 + 1} (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) univ : Set E) (univ : Set E)

Tactic:
ClosureOperator.closure_top (convexHull 𝕜)

Premises used: convexHull, ClosureOperator.closure_top
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
⊢ Eq.{u_2 + 1} (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ∅ : Set E) (∅ : Set E)

Tactic:
convex_empty.convexHull_eq

Premises used: convex_empty, Convex.convexHull_eq
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
mp : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) → s = ∅
mpr : s = ∅ → Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E)
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) ↔ s = ∅

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
h : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E)
mp : s ⊆ (convexHull 𝕜 : (a : Set E) → Set E) s
⊢ s = ∅

Tactic:
rw [← Set.subset_empty_iff, ← h]

Premises used: Set.subset_empty_iff