-- Mathlib/ModelTheory/PartialEquiv.lean
theorem le_iff {f g : M ≃ₚ[L] N} : f ≤ g ↔
    ∃ dom_le_dom : f.dom ≤ g.dom,
    ∃ cod_le_cod : f.cod ≤ g.cod,
    ∀ x, inclusion cod_le_cod (f.toEquiv x) = g.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
h : f ≤ g
x : ↥f.dom
⊢ g.cod.subtype.toFun ((inclusion ⋯) (f.toEquiv x)) = g.cod.subtype.toFun (g.toEquiv ((inclusion ⋯) x))

Tactic:
rwa [toEquiv_inclusion_apply]

Result:
no goals

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

Tactic:
exact fun h ↦ ⟨dom_le_dom h, cod_le_cod h,
  by intro x; apply (subtype _).inj'; rwa [toEquiv_inclusion_apply]⟩

Result:
no goals

Proof state:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
x✝ : ↥f.dom
⊢ g.cod.subtype ((inclusion le_cod) (f.toEquiv x✝)) = (f.cod.subtype.comp f.toEquiv.toEmbedding) x✝

Tactic:
rfl

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
⊢ f ≤ g ↔
    ∃ (dom_le_dom : f.dom ≤ g.dom) (cod_le_cod : f.cod ≤ g.cod),
      ∀ (x : ↥f.dom), (inclusion cod_le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)

Tactic:
constructor

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

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

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

Tactic:
apply (subtype _).inj'

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

Proof state:
case mpr.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
⊢ ∃ (h : f.dom ≤ g.dom),
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion h)) = f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
exact ⟨dom_le_dom, by ext; change subtype _ (g.toEquiv _) = _; rw [← h_eq]; rfl⟩

Result:
no goals

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

Tactic:
rintro ⟨dom_le_dom, le_cod, h_eq⟩

Result:
case mpr.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
⊢ f ≤ g

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
⊢ ∀ (x : ↥f.dom), (inclusion ⋯) (f.toEquiv x) = g.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
h : f ≤ g
x : ↥f.dom
⊢ (inclusion ⋯) (f.toEquiv x) = g.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
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion dom_le_dom)) = f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
ext

Result:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
x✝ : ↥f.dom
⊢ (g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion dom_le_dom))) x✝ =
    (f.cod.subtype.comp f.toEquiv.toEmbedding) x✝

Proof state:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
x✝ : ↥f.dom
⊢ g.cod.subtype (g.toEquiv ((inclusion dom_le_dom) x✝)) = (f.cod.subtype.comp f.toEquiv.toEmbedding) x✝

Tactic:
rw [← h_eq]

Result:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
x✝ : ↥f.dom
⊢ g.cod.subtype ((inclusion le_cod) (f.toEquiv x✝)) = (f.cod.subtype.comp f.toEquiv.toEmbedding) x✝

Proof state:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
x✝ : ↥f.dom
⊢ (g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion dom_le_dom))) x✝ =
    (f.cod.subtype.comp f.toEquiv.toEmbedding) x✝

Tactic:
change subtype _ (g.toEquiv _) = _

Result:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
x✝ : ↥f.dom
⊢ g.cod.subtype (g.toEquiv ((inclusion dom_le_dom) x✝)) = (f.cod.subtype.comp f.toEquiv.toEmbedding) x✝

Proof state:
case mpr.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
⊢ f ≤ g

Tactic:
rw [le_def]

Result:
case mpr.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
⊢ ∃ (h : f.dom ≤ g.dom),
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion h)) = f.cod.subtype.comp f.toEquiv.toEmbedding