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

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
⊢ φ.symm ≤ φ'.symm
Tactic:
refine ⟨target_subset h, fun {i} hi ↦ φ'.injOn ?_ ?_ ?_⟩
State after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ'.symm i ∈ φ'.source

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ.symm i ∈ φ'.source

case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ' (↑φ'.symm i) = ↑φ' (↑φ.symm i)

State before:
case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ' (↑φ'.symm i) = ↑φ' (↑φ.symm i)
Tactic:
rw [eq_comm, h.2 (φ.map_target hi), φ.right_inv hi, φ'.right_inv (target_subset h hi)]
State after:
no goals

State before:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ'.symm i ∈ φ'.source
Tactic:
exact φ'.map_target (target_subset h hi)
State after:
no goals

State before:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ.symm i ∈ φ'.source
Tactic:
exact h.1 <| φ.map_target hi
State after:
no goals