Theorem: Set.Nonempty.sInter_inter_comm (src/Pre.lean)

State before:
α : Type u_1
s : Set (Set α)
hs : Set.Nonempty s
t : Set α
⊢ ⋂₀ ((fun x => x ∩ t) '' s) = ⋂₀ s ∩ t
Tactic:
ext x
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

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]
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

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
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

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
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

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⟩
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

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⟩
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

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
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

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⟩
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

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
State after:
no goals

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]
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

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⟩
State after:
no goals

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]
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

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⟩
State after:
no goals

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 ⟩
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

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
State after:
no goals