-- Mathlib/ModelTheory/PartialEquiv.lean
@[gcongr] lemma symm_le_symm {f g : M ≃ₚ[L] N} (hfg : f ≤ g) : f.symm ≤ g.symm

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
⊢ ∀ (x : ↥f.symm.dom), (inclusion ⋯) (f.symm.toEquiv x) = g.symm.toEquiv ((inclusion ⋯) x)

Tactic:
intro x

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
x : ↥f.symm.dom
⊢ (inclusion ⋯) (f.symm.toEquiv x) = g.symm.toEquiv ((inclusion ⋯) x)

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
⊢ ∃ (dom_le_dom : f.symm.dom ≤ g.symm.dom) (cod_le_cod : f.symm.cod ≤ g.symm.cod),
    ∀ (x : ↥f.symm.dom), (inclusion cod_le_cod) (f.symm.toEquiv x) = g.symm.toEquiv ((inclusion dom_le_dom) x)

Tactic:
refine ⟨cod_le_cod hfg, dom_le_dom hfg, ?_⟩

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
⊢ ∀ (x : ↥f.symm.dom), (inclusion ⋯) (f.symm.toEquiv x) = g.symm.toEquiv ((inclusion ⋯) x)

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
⊢ f.symm ≤ g.symm

Tactic:
rw [le_iff]

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
⊢ ∃ (dom_le_dom : f.symm.dom ≤ g.symm.dom) (cod_le_cod : f.symm.cod ≤ g.symm.cod),
    ∀ (x : ↥f.symm.dom), (inclusion cod_le_cod) (f.symm.toEquiv x) = g.symm.toEquiv ((inclusion dom_le_dom) x)

Proof state:
case a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
x : ↥f.symm.dom
⊢ g.toEquiv ((inclusion ⋯) (f.toEquiv.symm x)) = g.toEquiv (g.toEquiv.symm ((inclusion ⋯) x))

Tactic:
rw [g.toEquiv.apply_symm_apply, (Equiv.apply_symm_apply f.toEquiv x).symm,
  f.toEquiv.symm_apply_apply]

Result:
case a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
x : ↥f.symm.dom
⊢ g.toEquiv ((inclusion ⋯) (f.toEquiv.symm x)) = (inclusion ⋯) (f.toEquiv (f.toEquiv.symm x))

Proof state:
case a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
x : ↥f.symm.dom
⊢ g.toEquiv ((inclusion ⋯) (f.symm.toEquiv x)) = g.toEquiv (g.symm.toEquiv ((inclusion ⋯) x))

Tactic:
change g.toEquiv (inclusion _ (f.toEquiv.symm x)) = g.toEquiv (g.toEquiv.symm _)

Result:
case a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
x : ↥f.symm.dom
⊢ g.toEquiv ((inclusion ⋯) (f.toEquiv.symm x)) = g.toEquiv (g.toEquiv.symm ((inclusion ⋯) x))

Proof state:
case a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
x : ↥f.symm.dom
⊢ g.toEquiv ((inclusion ⋯) (f.toEquiv.symm x)) = (inclusion ⋯) (f.toEquiv (f.toEquiv.symm x))

Tactic:
exact toEquiv_inclusion_apply hfg _

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
x : ↥f.symm.dom
⊢ (inclusion ⋯) (f.symm.toEquiv x) = g.symm.toEquiv ((inclusion ⋯) x)

Tactic:
apply g.toEquiv.injective

Result:
case a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
x : ↥f.symm.dom
⊢ g.toEquiv ((inclusion ⋯) (f.symm.toEquiv x)) = g.toEquiv (g.symm.toEquiv ((inclusion ⋯) x))