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

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) ?_
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

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

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

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

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

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

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

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

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