Theorem: exists_eq_image_subset_of_subset_image (Matroid/ForMathlib/Other.lean)

State before:
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
⊢ ∃ t₀ ⊆ s, t = f '' t₀
Tactic:
refine ⟨f ⁻¹' t ∩ s, inter_subset_right, subset_antisymm (fun x hxt ↦ ?_) ?_⟩
State after:
case refine_1
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
x : β
hxt : x ∈ t
⊢ x ∈ f '' (f ⁻¹' t ∩ s)

case refine_2
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
⊢ f '' (f ⁻¹' t ∩ s) ⊆ t

State before:
case refine_2
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
⊢ f '' (f ⁻¹' t ∩ s) ⊆ t
Tactic:
simp [image_subset_iff, inter_subset_left]
State after:
no goals

State before:
case refine_1
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
x : β
hxt : x ∈ t
⊢ x ∈ f '' (f ⁻¹' t ∩ s)
Tactic:
obtain ⟨a, ha, rfl⟩ := hst hxt
State after:
case refine_1.intro.intro
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
a : α
ha : a ∈ s
hxt : f a ∈ t
⊢ f a ∈ f '' (f ⁻¹' t ∩ s)

State before:
case refine_1.intro.intro
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
a : α
ha : a ∈ s
hxt : f a ∈ t
⊢ f a ∈ f '' (f ⁻¹' t ∩ s)
Tactic:
exact ⟨a, mem_inter hxt ha, rfl⟩
State after:
no goals