Theorem: Set.BijOn.exists_extend_of_subset (Matroid/ForMathlib/Function.lean)

State before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
Tactic:
obtain ⟨r, hrss, hbij⟩ := exists_subset_bijOn ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t) f
State after:
case intro.intro
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r (f '' ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t))
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'

State before:
case intro.intro
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r (f '' ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t))
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
Tactic:
rw [image_diff_preimage, image_inter_preimage] at hbij
State after:
case intro.intro
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'

State before:
case intro.intro
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
Tactic:
refine ⟨s ∪ r, subset_union_left, ?_, ?_, ?_, fun y hyt' ↦ ?_⟩
State after:
case intro.intro.refine_1
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ s ∪ r ⊆ s₁

case intro.intro.refine_2
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ MapsTo f (s ∪ r) t'

case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ InjOn f (s ∪ r)

case intro.intro.refine_4
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ f '' (s ∪ r)

State before:
case intro.intro.refine_4
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ f '' (s ∪ r)
Tactic:
rw [image_union, h.image_eq, hbij.image_eq, union_diff_self]
State after:
case intro.intro.refine_4
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ t ∪ f '' s₁ ∩ t'

State before:
case intro.intro.refine_4
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ t ∪ f '' s₁ ∩ t'
Tactic:
exact .inr ⟨ht' hyt', hyt'⟩
State after:
no goals

State before:
case intro.intro.refine_1
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ s ∪ r ⊆ s₁
Tactic:
exact union_subset hss₁ <| hrss.trans <| diff_subset.trans inter_subset_left
State after:
no goals

State before:
case intro.intro.refine_2
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ MapsTo f (s ∪ r) t'
Tactic:
rw [mapsTo', image_union, hbij.image_eq, h.image_eq, union_subset_iff]
State after:
case intro.intro.refine_2
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ t ⊆ t' ∧ (f '' s₁ ∩ t') \ t ⊆ t'

State before:
case intro.intro.refine_2
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ t ⊆ t' ∧ (f '' s₁ ∩ t') \ t ⊆ t'
Tactic:
exact ⟨htt', diff_subset.trans inter_subset_right⟩
State after:
no goals

State before:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ InjOn f (s ∪ r)
Tactic:
rw [injOn_union, and_iff_right h.injOn, and_iff_right hbij.injOn]
State after:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∀ x ∈ s, ∀ y ∈ r, f x ≠ f y

case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ Disjoint s r

State before:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ Disjoint s r
Tactic:
exact (subset_diff.1 hrss).2.symm.mono_left h.mapsTo
State after:
no goals

State before:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∀ x ∈ s, ∀ y ∈ r, f x ≠ f y
Tactic:
refine fun x hxs y hyr hxy ↦ (hrss hyr).2 ?_
State after:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' t

State before:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' t
Tactic:
rw [← h.image_eq]
State after:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' (f '' s)

State before:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' (f '' s)
Tactic:
exact ⟨x, hxs, hxy⟩
State after:
no goals