Theorem: PartialEquiv.target_subset (Matroid/ForMathlib/PartialEquiv.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
⊢ φ.target ⊆ φ'.target
Tactic:
rw [← φ.image_source_eq_target, ← φ'.image_source_eq_target]
State after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
⊢ ↑φ '' φ.source ⊆ ↑φ' '' φ'.source

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
⊢ ↑φ '' φ.source ⊆ ↑φ' '' φ'.source
Tactic:
rintro _ ⟨x,hx,rfl⟩
State after:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
x : α
hx : x ∈ φ.source
⊢ ↑φ x ∈ ↑φ' '' φ'.source

State before:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
x : α
hx : x ∈ φ.source
⊢ ↑φ x ∈ ↑φ' '' φ'.source
Tactic:
rw [← PartialEquiv.eq_of_mem_source h hx]
State after:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
x : α
hx : x ∈ φ.source
⊢ ↑φ' x ∈ ↑φ' '' φ'.source

State before:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
x : α
hx : x ∈ φ.source
⊢ ↑φ' x ∈ ↑φ' '' φ'.source
Tactic:
exact mem_image_of_mem _ (source_subset h hx)
State after:
no goals