internlm/Lean-Github huggingface dataset:
Theorem: Hpolytope_translation
Proof 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
Proof 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_
Theorem: Hpolytope_translation
Proof 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
Proof state after:
no goals
Theorem: Hpolytope_translation
Proof 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]
Proof 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_'
Theorem: Hpolytope_translation
Proof 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
Proof 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_'
Theorem: Hpolytope_translation
Proof 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]
Proof state after:
no goals
Theorem: Set.Finite.translation
Proof state before:
α : Type
inst✝ : AddGroup α
S : Set α
hS : Set.Finite S
x : α
⊢ Set.Finite (S + {x})
Tactic:
rw [Set.add_singleton]
Proof state after:
α : Type
inst✝ : AddGroup α
S : Set α
hS : Set.Finite S
x : α
⊢ Set.Finite ((fun x_1 => x_1 + x) '' S)
Theorem: Set.Finite.translation
Proof state before:
α : Type
inst✝ : AddGroup α
S : Set α
hS : Set.Finite S
x : α
⊢ Set.Finite ((fun x_1 => x_1 + x) '' S)
Tactic:
exact Set.Finite.image _ hS
Proof state after:
no goals
Theorem: Set.mem_translation
Proof state before:
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
⊢ s ∈ S + {x} ↔ s - x ∈ S
Tactic:
rw [Set.add_singleton, Set.mem_image]
Proof state after:
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
⊢ (∃ x_1 ∈ S, x_1 + x = s) ↔ s - x ∈ S
Theorem: Set.mem_translation
Proof state before:
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
⊢ (∃ x_1 ∈ S, x_1 + x = s) ↔ s - x ∈ S
Tactic:
constructor
Proof state after:
case mp
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
⊢ (∃ x_1 ∈ S, x_1 + x = s) → s - x ∈ S

case mpr
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
⊢ s - x ∈ S → ∃ x_1 ∈ S, x_1 + x = s
Theorem: Set.mem_translation
Proof state before:
case mp
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
⊢ (∃ x_1 ∈ S, x_1 + x = s) → s - x ∈ S
Tactic:
rintro ⟨y, hy, rfl⟩
Proof state after:
case mp.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
hy : y ∈ S
⊢ y + x - x ∈ S
Theorem: Set.mem_translation
Proof state before:
case mp.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
hy : y ∈ S
⊢ y + x - x ∈ S
Tactic:
rw [add_sub_cancel]
Proof state after:
case mp.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
hy : y ∈ S
⊢ y ∈ S
Theorem: Set.mem_translation
Proof state before:
case mp.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
hy : y ∈ S
⊢ y ∈ S
Tactic:
exact hy
Proof state after:
no goals
Theorem: Set.mem_translation
Proof state before:
case mpr
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
⊢ s - x ∈ S → ∃ x_1 ∈ S, x_1 + x = s
Tactic:
intro h
Proof state after:
case mpr
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
h : s - x ∈ S
⊢ ∃ x_1 ∈ S, x_1 + x = s
Theorem: Set.mem_translation
Proof state before:
case mpr
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
h : s - x ∈ S
⊢ ∃ x_1 ∈ S, x_1 + x = s
Tactic:
exact ⟨s - x, h, by rw [sub_add_cancel]⟩
Proof state after:
no goals
Theorem: Set.mem_translation
Proof state before:
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
h : s - x ∈ S
⊢ s - x + x = s
Tactic:
rw [sub_add_cancel]
Proof state after:
no goals
Theorem: Set.sub_eq_neg_add
Proof state before:
α : Type
inst✝ : AddGroup α
S : Set α
x : α
⊢ S - {x} = S + {-x}
Tactic:
ext y
Proof state after:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ y ∈ S - {x} ↔ y ∈ S + {-x}
Theorem: Set.sub_eq_neg_add
Proof state before:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ y ∈ S - {x} ↔ y ∈ S + {-x}
Tactic:
simp only [sub_singleton, mem_image, add_singleton, image_add_right, neg_neg, mem_preimage]
Proof state after:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ (∃ x_1 ∈ S, x_1 - x = y) ↔ y + x ∈ S
Theorem: Set.sub_eq_neg_add
Proof state before:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ (∃ x_1 ∈ S, x_1 - x = y) ↔ y + x ∈ S
Tactic:
refine ⟨ ?_, fun h => ⟨y + x, h, by rw [add_sub_cancel]⟩ ⟩
Proof state after:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ (∃ x_1 ∈ S, x_1 - x = y) → y + x ∈ S
Theorem: Set.sub_eq_neg_add
Proof state before:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ (∃ x_1 ∈ S, x_1 - x = y) → y + x ∈ S
Tactic:
rintro ⟨z, hz, rfl⟩
Proof state after:
case h.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x z : α
hz : z ∈ S
⊢ z - x + x ∈ S
Theorem: Set.sub_eq_neg_add
Proof state before:
case h.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x z : α
hz : z ∈ S
⊢ z - x + x ∈ S
Tactic:
rw [sub_add_cancel]
Proof state after:
case h.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x z : α
hz : z ∈ S
⊢ z ∈ S
Theorem: Set.sub_eq_neg_add
Proof state before:
case h.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x z : α
hz : z ∈ S
⊢ z ∈ S
Tactic:
exact hz
Proof state after:
no goals
Theorem: Set.sub_eq_neg_add
Proof state before:
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
h : y + x ∈ S
⊢ y + x - x = y
Tactic:
rw [add_sub_cancel]
Proof state after:
no goals
Theorem: Set.neg_add_cancel_right'
Proof state before:
α : Type
inst✝ : AddGroup α
S : Set α
x : α
⊢ S - {x} + {x} = S
Tactic:
ext y
Proof state after:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ y ∈ S - {x} + {x} ↔ y ∈ S
Theorem: Set.neg_add_cancel_right'
Proof state before:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ y ∈ S - {x} + {x} ↔ y ∈ S
Tactic:
simp only [sub_singleton, add_singleton, mem_image, exists_exists_and_eq_and, sub_add_cancel, exists_eq_right]
Proof state after:
no goals
Theorem: interior_eq_compl_closure_compl
Proof state before:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ interior s = (closure sᶜ)ᶜ
Tactic:
rw [← compl_compl s, compl_compl sᶜ, interior_compl]
Proof state after:
no goals
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
⊢ ⋂₀ ((fun x => x ∩ t) '' s) = ⋂₀ s ∩ t
Tactic:
ext x
Proof state after:
case h
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
⊢ x ∈ ⋂₀ ((fun x => x ∩ t) '' s) ↔ x ∈ ⋂₀ s ∩ t
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
case h
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
⊢ x ∈ ⋂₀ ((fun x => x ∩ t) '' s) ↔ x ∈ ⋂₀ s ∩ t
Tactic:
simp only [mem_sInter, mem_inter_iff, mem_singleton_iff, and_imp]
Proof state after:
case h
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
⊢ (∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1) ↔ (∀ t ∈ s, x ∈ t) ∧ x ∈ t
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
case h
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
⊢ (∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1) ↔ (∀ t ∈ s, x ∈ t) ∧ x ∈ t
Tactic:
constructor
Proof state after:
case h.mp
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
⊢ (∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1) → (∀ t ∈ s, x ∈ t) ∧ x ∈ t

case h.mpr
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
⊢ (∀ t ∈ s, x ∈ t) ∧ x ∈ t → ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
case h.mp
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
⊢ (∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1) → (∀ t ∈ s, x ∈ t) ∧ x ∈ t
Tactic:
intro h
Proof state after:
case h.mp
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
⊢ (∀ t ∈ s, x ∈ t) ∧ x ∈ t
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
case h.mp
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
⊢ (∀ t ∈ s, x ∈ t) ∧ x ∈ t
Tactic:
have : Nonempty.some hs ∩ t ∈ (fun x => x ∩ t) '' s := by
  rw [mem_image]
  exact ⟨Nonempty.some hs, hs.some_mem, rfl⟩
Proof state after:
case h.mp
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
this : Nonempty.some hs ∩ t ∈ (fun x => x ∩ t) '' s
⊢ (∀ t ∈ s, x ∈ t) ∧ x ∈ t
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
case h.mp
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
this : Nonempty.some hs ∩ t ∈ (fun x => x ∩ t) '' s
⊢ (∀ t ∈ s, x ∈ t) ∧ x ∈ t
Tactic:
refine ⟨ ?_, (h (hs.some ∩ t) this).2⟩
Proof state after:
case h.mp
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
this : Nonempty.some hs ∩ t ∈ (fun x => x ∩ t) '' s
⊢ ∀ t ∈ s, x ∈ t
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
case h.mp
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
this : Nonempty.some hs ∩ t ∈ (fun x => x ∩ t) '' s
⊢ ∀ t ∈ s, x ∈ t
Tactic:
intro y hy
Proof state after:
case h.mp
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
this : Nonempty.some hs ∩ t ∈ (fun x => x ∩ t) '' s
y : Set α
hy : y ∈ s
⊢ x ∈ y
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
case h.mp
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
this : Nonempty.some hs ∩ t ∈ (fun x => x ∩ t) '' s
y : Set α
hy : y ∈ s
⊢ x ∈ y
Tactic:
have : y ∩ t ∈ (fun x => x ∩ t) '' s := by
  rw [mem_image]
  exact ⟨y, hy, rfl⟩
Proof state after:
case h.mp
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
this✝ : Nonempty.some hs ∩ t ∈ (fun x => x ∩ t) '' s
y : Set α
hy : y ∈ s
this : y ∩ t ∈ (fun x => x ∩ t) '' s
⊢ x ∈ y
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
case h.mp
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
this✝ : Nonempty.some hs ∩ t ∈ (fun x => x ∩ t) '' s
y : Set α
hy : y ∈ s
this : y ∩ t ∈ (fun x => x ∩ t) '' s
⊢ x ∈ y
Tactic:
exact (h (y ∩ t) this).1
Proof state after:
no goals
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
⊢ Nonempty.some hs ∩ t ∈ (fun x => x ∩ t) '' s
Tactic:
rw [mem_image]
Proof state after:
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
⊢ ∃ x ∈ s, x ∩ t = Nonempty.some hs ∩ t
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
⊢ ∃ x ∈ s, x ∩ t = Nonempty.some hs ∩ t
Tactic:
exact ⟨Nonempty.some hs, hs.some_mem, rfl⟩
Proof state after:
no goals
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
this : Nonempty.some hs ∩ t ∈ (fun x => x ∩ t) '' s
y : Set α
hy : y ∈ s
⊢ y ∩ t ∈ (fun x => x ∩ t) '' s
Tactic:
rw [mem_image]
Proof state after:
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
this : Nonempty.some hs ∩ t ∈ (fun x => x ∩ t) '' s
y : Set α
hy : y ∈ s
⊢ ∃ x ∈ s, x ∩ t = y ∩ t
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
this : Nonempty.some hs ∩ t ∈ (fun x => x ∩ t) '' s
y : Set α
hy : y ∈ s
⊢ ∃ x ∈ s, x ∩ t = y ∩ t
Tactic:
exact ⟨y, hy, rfl⟩
Proof state after:
no goals
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
case h.mpr
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
⊢ (∀ t ∈ s, x ∈ t) ∧ x ∈ t → ∀ t_1 ∈ (fun x => x ∩ t) '' s, x ∈ t_1
Tactic:
rintro h y ⟨ z, hz, rfl ⟩
Proof state after:
case h.mpr.intro.intro
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : (∀ t ∈ s, x ∈ t) ∧ x ∈ t
z : Set α
hz : z ∈ s
⊢ x ∈ (fun x => x ∩ t) z
Theorem: Set.Nonempty.sInter_inter_comm
Proof state before:
case h.mpr.intro.intro
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
x : α
h : (∀ t ∈ s, x ∈ t) ∧ x ∈ t
z : Set α
hz : z ∈ s
⊢ x ∈ (fun x => x ∩ t) z
Tactic:
exact mem_inter (h.1 z hz) h.2
Proof state after:
no goals
Theorem: Set.Nonempty.image_sInter
Proof state before:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
⊢ f '' ⋂₀ S = ⋂ s ∈ S, f '' s
Tactic:
refine subset_antisymm (image_sInter_subset S f) ?_
Proof state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
⊢ ⋂ s ∈ S, f '' s ⊆ f '' ⋂₀ S
Theorem: Set.Nonempty.image_sInter
Proof state before:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
⊢ ⋂ s ∈ S, f '' s ⊆ f '' ⋂₀ S
Tactic:
intro y hy
Proof state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
y : β
hy : y ∈ ⋂ s ∈ S, f '' s
⊢ y ∈ f '' ⋂₀ S
Theorem: Set.Nonempty.image_sInter
Proof state before:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
y : β
hy : y ∈ ⋂ s ∈ S, f '' s
⊢ y ∈ f '' ⋂₀ S
Tactic:
simp_all
Proof state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
y : β
hy : ∀ i ∈ S, ∃ x ∈ i, f x = y
⊢ ∃ x, (∀ t ∈ S, x ∈ t) ∧ f x = y
Theorem: Set.Nonempty.image_sInter
Proof state before:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
y : β
hy : ∀ i ∈ S, ∃ x ∈ i, f x = y
⊢ ∃ x, (∀ t ∈ S, x ∈ t) ∧ f x = y
Tactic:
rcases hy hS.some hS.some_mem with ⟨x, _hxInhSsome_, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
x : α
_hxInhSsome_ : x ∈ Nonempty.some hS
hy : ∀ i ∈ S, ∃ x_1 ∈ i, f x_1 = f x
⊢ ∃ x_1, (∀ t ∈ S, x_1 ∈ t) ∧ f x_1 = f x
Theorem: Set.Nonempty.image_sInter
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
x : α
_hxInhSsome_ : x ∈ Nonempty.some hS
hy : ∀ i ∈ S, ∃ x_1 ∈ i, f x_1 = f x
⊢ ∃ x_1, (∀ t ∈ S, x_1 ∈ t) ∧ f x_1 = f x
Tactic:
refine ⟨x, ?_, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
x : α
_hxInhSsome_ : x ∈ Nonempty.some hS
hy : ∀ i ∈ S, ∃ x_1 ∈ i, f x_1 = f x
⊢ ∀ t ∈ S, x ∈ t
Theorem: Set.Nonempty.image_sInter
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
x : α
_hxInhSsome_ : x ∈ Nonempty.some hS
hy : ∀ i ∈ S, ∃ x_1 ∈ i, f x_1 = f x
⊢ ∀ t ∈ S, x ∈ t
Tactic:
intro s hsInS
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
x : α
_hxInhSsome_ : x ∈ Nonempty.some hS
hy : ∀ i ∈ S, ∃ x_1 ∈ i, f x_1 = f x
s : Set α
hsInS : s ∈ S
⊢ x ∈ s
Theorem: Set.Nonempty.image_sInter
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
x : α
_hxInhSsome_ : x ∈ Nonempty.some hS
hy : ∀ i ∈ S, ∃ x_1 ∈ i, f x_1 = f x
s : Set α
hsInS : s ∈ S
⊢ x ∈ s
Tactic:
rcases hy s hsInS with ⟨z, hzIns, hfzEqfx⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
x : α
_hxInhSsome_ : x ∈ Nonempty.some hS
hy : ∀ i ∈ S, ∃ x_1 ∈ i, f x_1 = f x
s : Set α
hsInS : s ∈ S
z : α
hzIns : z ∈ s
hfzEqfx : f z = f x
⊢ x ∈ s
Theorem: Set.Nonempty.image_sInter
Proof state before:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
x : α
_hxInhSsome_ : x ∈ Nonempty.some hS
hy : ∀ i ∈ S, ∃ x_1 ∈ i, f x_1 = f x
s : Set α
hsInS : s ∈ S
z : α
hzIns : z ∈ s
hfzEqfx : f z = f x
⊢ x ∈ s
Tactic:
convert hzIns
Proof state after:
case h.e'_4
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
x : α
_hxInhSsome_ : x ∈ Nonempty.some hS
hy : ∀ i ∈ S, ∃ x_1 ∈ i, f x_1 = f x
s : Set α
hsInS : s ∈ S
z : α
hzIns : z ∈ s
hfzEqfx : f z = f x
⊢ x = z
Theorem: Set.Nonempty.image_sInter
Proof state before:
case h.e'_4
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : Set.Nonempty S
f : α → β
hf : Function.Injective f
x : α
_hxInhSsome_ : x ∈ Nonempty.some hS
hy : ∀ i ∈ S, ∃ x_1 ∈ i, f x_1 = f x
s : Set α
hsInS : s ∈ S
z : α
hzIns : z ∈ s
hfzEqfx : f z = f x
⊢ x = z
Tactic:
exact hf hfzEqfx.symm
Proof state after:
no goals
Theorem: AffineEquiv.coe_VSubconst
Proof state before:
𝕜 E P : Type
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : AddTorsor E P
x : P
⊢ ⇑(VSubconst 𝕜 x) = fun x_1 => x_1 -ᵥ x
Tactic:
rfl
Proof state after:
no goals
Theorem: Submodule.mem_orthogonal_Basis
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
⊢ v ∈ Kᗮ ↔ ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
Tactic:
rw [Submodule.mem_orthogonal]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
⊢ (∀ u ∈ K, ⟪u, v⟫_𝕜 = 0) ↔ ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
Theorem: Submodule.mem_orthogonal_Basis
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
⊢ (∀ u ∈ K, ⟪u, v⟫_𝕜 = 0) ↔ ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
Tactic:
constructor
Proof state after:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
⊢ (∀ u ∈ K, ⟪u, v⟫_𝕜 = 0) → ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0

case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
⊢ (∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0) → ∀ u ∈ K, ⟪u, v⟫_𝕜 = 0
Theorem: Submodule.mem_orthogonal_Basis
Proof state before:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
⊢ (∀ u ∈ K, ⟪u, v⟫_𝕜 = 0) → ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
Tactic:
intro h i
Proof state after:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ u ∈ K, ⟪u, v⟫_𝕜 = 0
i : ι
⊢ ⟪↑(b i), v⟫_𝕜 = 0
Theorem: Submodule.mem_orthogonal_Basis
Proof state before:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ u ∈ K, ⟪u, v⟫_𝕜 = 0
i : ι
⊢ ⟪↑(b i), v⟫_𝕜 = 0
Tactic:
exact h _ (Submodule.coe_mem (b i))
Proof state after:
no goals
Theorem: Submodule.mem_orthogonal_Basis
Proof state before:
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
⊢ (∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0) → ∀ u ∈ K, ⟪u, v⟫_𝕜 = 0
Tactic:
intro h x hx
Proof state after:
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
x : E
hx : x ∈ K
⊢ ⟪x, v⟫_𝕜 = 0
Theorem: Submodule.mem_orthogonal_Basis
Proof state before:
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
x : E
hx : x ∈ K
⊢ ⟪x, v⟫_𝕜 = 0
Tactic:
rw [Basis.mem_submodule_iff b] at hx
Proof state after:
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
x : E
hx : ∃ c, x = Finsupp.sum c fun i x => x • ↑(b i)
⊢ ⟪x, v⟫_𝕜 = 0
Theorem: Submodule.mem_orthogonal_Basis
Proof state before:
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
x : E
hx : ∃ c, x = Finsupp.sum c fun i x => x • ↑(b i)
⊢ ⟪x, v⟫_𝕜 = 0
Tactic:
rcases hx with ⟨ a, rfl ⟩
Proof state after:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
⊢ ⟪Finsupp.sum a fun i x => x • ↑(b i), v⟫_𝕜 = 0
Theorem: Submodule.mem_orthogonal_Basis
Proof state before:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
⊢ ⟪Finsupp.sum a fun i x => x • ↑(b i), v⟫_𝕜 = 0
Tactic:
rw [Finsupp.sum_inner]
Proof state after:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
⊢ (Finsupp.sum a fun i a => (starRingEnd 𝕜) a • ⟪↑(b i), v⟫_𝕜) = 0
Theorem: Submodule.mem_orthogonal_Basis
Proof state before:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
⊢ (Finsupp.sum a fun i a => (starRingEnd 𝕜) a • ⟪↑(b i), v⟫_𝕜) = 0
Tactic:
apply Finset.sum_eq_zero
Proof state after:
case mpr.intro.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
⊢ ∀ x ∈ a.support, (fun i a => (starRingEnd 𝕜) a • ⟪↑(b i), v⟫_𝕜) x (a x) = 0