Theorem: Hyperplane_affineClosed (src/Halfspace.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
⊢ ∀ (s : Fin n → E),
    Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α} →
      ∀ (a : Fin n → ℝ),
        Finset.sum Finset.univ a = 1 → (Finset.affineCombination ℝ Finset.univ s) a ∈ {x | ↑Hi_.f x = Hi_.α}
Tactic:
intro s hs a ha
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
⊢ (Finset.affineCombination ℝ Finset.univ s) a ∈ {x | ↑Hi_.f x = Hi_.α}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
⊢ (Finset.affineCombination ℝ Finset.univ s) a ∈ {x | ↑Hi_.f x = Hi_.α}
Tactic:
rw [Finset.affineCombination_eq_linear_combination _ _ _ ha, Set.mem_setOf, map_sum]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
⊢ (Finset.sum Finset.univ fun x => ↑Hi_.f (a x • s x)) = Hi_.α

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
⊢ (Finset.sum Finset.univ fun x => ↑Hi_.f (a x • s x)) = Hi_.α
Tactic:
have hg : (fun i => Hi_.f.1 (a i • s i)) = fun i => a i * Hi_.α := by
  ext i
  rw [Set.range_subset_iff] at hs
  specialize hs i
  rw [Set.mem_setOf] at hs
  rw [ContinuousLinearMap.map_smulₛₗ, smul_eq_mul, RingHom.id_apply, hs]
  done
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
hg : (fun i => ↑Hi_.f (a i • s i)) = fun i => a i * Hi_.α
⊢ (Finset.sum Finset.univ fun x => ↑Hi_.f (a x • s x)) = Hi_.α

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
hg : (fun i => ↑Hi_.f (a i • s i)) = fun i => a i * Hi_.α
⊢ (Finset.sum Finset.univ fun x => ↑Hi_.f (a x • s x)) = Hi_.α
Tactic:
rw [hg, ←Finset.sum_mul, ha, one_mul]
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
⊢ (fun i => ↑Hi_.f (a i • s i)) = fun i => a i * Hi_.α
Tactic:
ext i
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α
Tactic:
rw [Set.range_subset_iff] at hs
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : ∀ (y : Fin n), s y ∈ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : ∀ (y : Fin n), s y ∈ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α
Tactic:
specialize hs i
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
hs : s i ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
hs : s i ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α
Tactic:
rw [Set.mem_setOf] at hs
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
hs : ↑Hi_.f (s i) = Hi_.α
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
hs : ↑Hi_.f (s i) = Hi_.α
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α
Tactic:
rw [ContinuousLinearMap.map_smulₛₗ, smul_eq_mul, RingHom.id_apply, hs]
State after:
no goals