Theorem: Hpolytope_translation (src/Polytope.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
⊢ Hpolytope ⋯ = Hpolytope hH_ + {x}
Tactic:
rw [Hpolytope, Hpolytope, Set.sInter_image, Set.sInter_image]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
⊢ ⋂ x_1 ∈ Halfspace_translation x '' H_, ↑x_1 = (⋂ x ∈ H_, ↑x) + {x}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
⊢ ⋂ x_1 ∈ Halfspace_translation x '' H_, ↑x_1 = (⋂ x ∈ H_, ↑x) + {x}
Tactic:
ext y
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ y ∈ ⋂ x_1 ∈ Halfspace_translation x '' H_, ↑x_1 ↔ y ∈ (⋂ x ∈ H_, ↑x) + {x}

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ y ∈ ⋂ x_1 ∈ Halfspace_translation x '' H_, ↑x_1 ↔ y ∈ (⋂ x ∈ H_, ↑x) + {x}
Tactic:
rw [Set.mem_iInter, Set.add_singleton]
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ (i : Halfspace E), y ∈ ⋂ (_ : i ∈ Halfspace_translation x '' H_), ↑i) ↔ y ∈ (fun x_1 => x_1 + x) '' ⋂ x ∈ H_, ↑x

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ (i : Halfspace E), y ∈ ⋂ (_ : i ∈ Halfspace_translation x '' H_), ↑i) ↔ y ∈ (fun x_1 => x_1 + x) '' ⋂ x ∈ H_, ↑x
Tactic:
simp only [Set.mem_iInter, SetLike.mem_coe, Set.image_add_right, Set.mem_preimage]
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ i ∈ Halfspace_translation x '' H_, y ∈ i) ↔ ∀ i ∈ H_, y + -x ∈ i

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ i ∈ Halfspace_translation x '' H_, y ∈ i) ↔ ∀ i ∈ H_, y + -x ∈ i
Tactic:
constructor
State after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ i ∈ Halfspace_translation x '' H_, y ∈ i) → ∀ i ∈ H_, y + -x ∈ i

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ i ∈ H_, y + -x ∈ i) → ∀ i ∈ Halfspace_translation x '' H_, y ∈ i

State before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ i ∈ Halfspace_translation x '' H_, y ∈ i) → ∀ i ∈ H_, y + -x ∈ i
Tactic:
intro h Hi_ hHi_
State after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ Halfspace_translation x '' H_, y ∈ i
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ y + -x ∈ Hi_

State before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ Halfspace_translation x '' H_, y ∈ i
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ y + -x ∈ Hi_
Tactic:
specialize h (Halfspace_translation x Hi_) (Set.mem_image_of_mem _ hHi_)
State after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : y ∈ Halfspace_translation x Hi_
⊢ y + -x ∈ Hi_

State before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : y ∈ Halfspace_translation x Hi_
⊢ y + -x ∈ Hi_
Tactic:
rw [← SetLike.mem_coe, mem_Halfspace_translation, sub_eq_add_neg] at h
State after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : y + -x ∈ ↑Hi_
⊢ y + -x ∈ Hi_

State before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : y + -x ∈ ↑Hi_
⊢ y + -x ∈ Hi_
Tactic:
exact h
State after:
no goals

State before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
⊢ (∀ i ∈ H_, y + -x ∈ i) → ∀ i ∈ Halfspace_translation x '' H_, y ∈ i
Tactic:
intro h Hi_ hHi_
State after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
⊢ y ∈ Hi_

State before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
⊢ y ∈ Hi_
Tactic:
specialize h (Halfspace_translation (-x) Hi_) (?_)
State after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
⊢ Halfspace_translation (-x) Hi_ ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_

State before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
⊢ Halfspace_translation (-x) Hi_ ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Tactic:
rw [Set.mem_image] at hHi_
State after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_ : Halfspace E
hHi_ : ∃ x_1 ∈ H_, Halfspace_translation x x_1 = Hi_
⊢ Halfspace_translation (-x) Hi_ ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_

State before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_ : Halfspace E
hHi_ : ∃ x_1 ∈ H_, Halfspace_translation x x_1 = Hi_
⊢ Halfspace_translation (-x) Hi_ ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Tactic:
rcases hHi_ with ⟨ Hi_', hHi_', rfl ⟩
State after:
case h.mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
⊢ Halfspace_translation (-x) (Halfspace_translation x Hi_') ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_

State before:
case h.mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
⊢ Halfspace_translation (-x) (Halfspace_translation x Hi_') ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Tactic:
have : Halfspace_translation (-x) (Halfspace_translation x Hi_') = Hi_':= by
  rw [SetLike.ext_iff]
  intro z
  rw [← SetLike.mem_coe, ← SetLike.mem_coe, mem_Halfspace_translation, mem_Halfspace_translation,
    sub_neg_eq_add, add_sub_cancel]
  done
State after:
case h.mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
this : Halfspace_translation (-x) (Halfspace_translation x Hi_') = Hi_'
⊢ Halfspace_translation (-x) (Halfspace_translation x Hi_') ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_

State before:
case h.mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
this : Halfspace_translation (-x) (Halfspace_translation x Hi_') = Hi_'
⊢ Halfspace_translation (-x) (Halfspace_translation x Hi_') ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Tactic:
rw [this]
State after:
case h.mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
this : Halfspace_translation (-x) (Halfspace_translation x Hi_') = Hi_'
⊢ Hi_' ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_

State before:
case h.mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
this : Halfspace_translation (-x) (Halfspace_translation x Hi_') = Hi_'
⊢ Hi_' ∈ H_

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Tactic:
assumption
State after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_

State before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y + -x ∈ Halfspace_translation (-x) Hi_
⊢ y ∈ Hi_
Tactic:
rw [← SetLike.mem_coe, mem_Halfspace_translation, add_sub_cancel, SetLike.mem_coe] at h
State after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y ∈ Hi_
⊢ y ∈ Hi_

State before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Halfspace_translation x '' H_
h : y ∈ Hi_
⊢ y ∈ Hi_
Tactic:
exact h
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
⊢ Halfspace_translation (-x) (Halfspace_translation x Hi_') = Hi_'
Tactic:
rw [SetLike.ext_iff]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
⊢ ∀ (x_1 : E), x_1 ∈ Halfspace_translation (-x) (Halfspace_translation x Hi_') ↔ x_1 ∈ Hi_'

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
⊢ ∀ (x_1 : E), x_1 ∈ Halfspace_translation (-x) (Halfspace_translation x Hi_') ↔ x_1 ∈ Hi_'
Tactic:
intro z
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
z : E
⊢ z ∈ Halfspace_translation (-x) (Halfspace_translation x Hi_') ↔ z ∈ Hi_'

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
h : ∀ i ∈ H_, y + -x ∈ i
Hi_' : Halfspace E
hHi_' : Hi_' ∈ H_
z : E
⊢ z ∈ Halfspace_translation (-x) (Halfspace_translation x Hi_') ↔ z ∈ Hi_'
Tactic:
rw [← SetLike.mem_coe, ← SetLike.mem_coe, mem_Halfspace_translation, mem_Halfspace_translation,
  sub_neg_eq_add, add_sub_cancel]
State after:
no goals