awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ ∃ (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
have rsuffices₁ : ∃ (e : E ≃ₜ E),
  (⇑e : (a : E) → E) '' interior s = interior t ∧ (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t
Tactic: rsuffices ⟨e, h₁, h₂⟩ : ∃ e : E ≃ₜ E, e '' interior s = interior t ∧ e '' closure s = closure t
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
have refine : (⇑e : (a : E) → E) '' frontier s = frontier t
Tactic: refine ⟨e, h₁, h₂, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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 : (a : E) → E) '' frontier s = frontier t
have simp_rw : (⇑e : (a : E) → E) '' (closure[inst_2] s \ interior s) = closure[inst_2] t \ interior t
Tactic: simp_rw [← closure_diff_interior, image_diff e.injective, h₁, h₂]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ (⇑e : (a : E) → E) '' frontier s = frontier t
have simp_rw₁ : (⇑e : (a : E) → E) '' closure[inst_2] s \ (⇑e : (a : E) → E) '' interior s = closure[inst_2] t \ interior t
Tactic: simp_rw [← closure_diff_interior, image_diff e.injective, h₁, h₂]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ (⇑e : (a : E) → E) '' frontier s = frontier t
have simp_rw₂ : (⇑e : (a : E) → E) '' closure[inst_2] s \ interior t = closure[inst_2] t \ interior t
Tactic: simp_rw [← closure_diff_interior, image_diff e.injective, h₁, h₂]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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),
    (⇑e : (a : E) → E) '' interior s = interior t ∧ (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t
have 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
Tactic: rcases hsne with ⟨x, hx⟩
Cleared hypotheses: hsne
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ ∃ (e : E ≃ₜ E),
    (⇑e : (a : E) → E) '' interior s = interior t ∧ (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t
have 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
Tactic: rcases htne with ⟨y, hy⟩
Cleared hypotheses: htne
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ E ≃ₜ E
have hsc₁ : Convex ℝ (-x +ᵥ s)
Tactic: apply gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t)
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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)
⊢ E ≃ₜ E
have hs₀ : Membership.mem (γ := Filter E) (𝓝 0) (-x +ᵥ s)
Tactic: apply gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t)
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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)
⊢ E ≃ₜ E
have hsb₁ : IsVonNBounded ℝ (-x +ᵥ s)
Tactic: apply gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t)
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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)
⊢ E ≃ₜ E
have htc : Convex ℝ (-y +ᵥ t)
Tactic: apply gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t)
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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)
⊢ E ≃ₜ E
have ht₀ : Membership.mem (γ := Filter E) (𝓝 0) (-y +ᵥ t)
Tactic: apply gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t)
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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)
⊢ E ≃ₜ E
have htb₁ : IsVonNBounded ℝ (-y +ᵥ t)
Tactic: apply gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t)
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
have refine_1 : (⇑(Homeomorph.trans (Homeomorph.addLeft (-x)) (h.trans (Homeomorph.addLeft y))) : (a : E) → E) '' interior s =
  interior t
Tactic: refine ⟨.trans (.addLeft (-x)) <| h.trans <| .addLeft y, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ ∃ (e : E ≃ₜ E),
    (⇑e : (a : E) → E) '' interior s = interior t ∧ (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t
have refine_2 : (⇑(Homeomorph.trans (Homeomorph.addLeft (-x)) (h.trans (Homeomorph.addLeft y))) : (a : E) → E) '' closure[inst_2] s =
  closure[inst_2] t
Tactic: refine ⟨.trans (.addLeft (-x)) <| h.trans <| .addLeft y, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (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))
have 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))
Tactic: simp_rw [interior_vadd, ← image_vadd, image_image, vadd_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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))
⊢ (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))
have 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))
Tactic: simp_rw [interior_vadd, ← image_vadd, image_image, vadd_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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))
⊢ (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))
have 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)
Tactic: simp_rw [interior_vadd, ← image_vadd, image_image, vadd_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' interior (-x +ᵥ s)) = interior t
have rw : y +ᵥ interior (-y +ᵥ t) = interior t
Tactic: rw [image_gaugeRescaleHomeomorph_interior, interior_vadd, vadd_neg_vadd]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' interior (-x +ᵥ s)) = interior t
have rw₁ : y +ᵥ -y +ᵥ interior t = interior t
Tactic: rw [image_gaugeRescaleHomeomorph_interior, interior_vadd, vadd_neg_vadd]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' interior (-x +ᵥ s)) = interior t
have rw₂ : interior t = interior t
Tactic: rw [image_gaugeRescaleHomeomorph_interior, interior_vadd, vadd_neg_vadd]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (⇑(Homeomorph.trans (Homeomorph.addLeft (-x)) (h.trans (Homeomorph.addLeft y))) : (a : E) → E) '' interior s =
    interior t
have 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))
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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))
⊢ (⇑(Homeomorph.trans (Homeomorph.addLeft (-x)) (h.trans (Homeomorph.addLeft y))) : (a : E) → E) '' interior s =
    interior t
have a₁ : HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' interior (-x +ᵥ 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (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))
have 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))
Tactic: simp_rw [closure_vadd, ← image_vadd, image_image, vadd_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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))
⊢ (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))
have 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))
Tactic: simp_rw [closure_vadd, ← image_vadd, image_image, vadd_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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))
⊢ (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))
have 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)
Tactic: simp_rw [closure_vadd, ← image_vadd, image_image, vadd_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' closure[inst_2] (-x +ᵥ s)) = closure[inst_2] t
have rw : y +ᵥ closure[inst_2] (-y +ᵥ t) = closure[inst_2] t
Tactic: rw [image_gaugeRescaleHomeomorph_closure, closure_vadd, vadd_neg_vadd]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' closure[inst_2] (-x +ᵥ s)) = closure[inst_2] t
have rw₁ : y +ᵥ -y +ᵥ closure[inst_2] t = closure[inst_2] t
Tactic: rw [image_gaugeRescaleHomeomorph_closure, closure_vadd, vadd_neg_vadd]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' closure[inst_2] (-x +ᵥ s)) = closure[inst_2] t
have rw₂ : closure[inst_2] t = closure[inst_2] t
Tactic: rw [image_gaugeRescaleHomeomorph_closure, closure_vadd, vadd_neg_vadd]