mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this✝ : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
N : ℕ
this : ⋃ n, s n = (⋃ n ∈ Finset.range N, s n) ∪ ⋃ n, s (n + N)
⊢ ⋃ n, s (n + N) ⊆ ⋃ b, s b

Tactic:
by simp [subset_iUnion s]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this✝ : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
N : ℕ
this : ⋃ n, s n = (⋃ n ∈ Finset.range N, s n) ∪ ⋃ n, s (n + N)
i : ℕ
hi : i ∈ Finset.range N
⊢ s i ⊆ ⋃ b, s b

Tactic:
by simp [subset_iUnion s]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
inst✝ : Countable ι
s : ι → Set X
hm : ∀ (i : ι), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hι : Finite ι
this : Fintype ι := Fintype.ofFinite ι
i : ι
⊢ s i ⊆ ⋃ b, s b

Tactic:
by simp [subset_iUnion s]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case e_f
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : Unique X
inst✝ : CompleteSpace G
x : X
⊢ f x = f default

Tactic:
;

Goal state after:
case e_f
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : Unique X
inst✝ : CompleteSpace G
x : X
⊢ f x = f default
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case e_f
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : Unique X
inst✝ : CompleteSpace G
x : X
⊢ x = default

Tactic:
;

Goal state after:
case e_f
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : Unique X
inst✝ : CompleteSpace G
x : X
⊢ x = default
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case pos
X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : VectorMeasure X F
β : Type u_10
inst✝ : MeasurableSpace β
φ : X → β
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
h : μ.Integrable (f ∘ φ)
hφ : Measurable φ
⊢ (μ.map φ).Integrable f

pp: case neg
X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : VectorMeasure X F
β : Type u_10
inst✝ : MeasurableSpace β
φ : X → β
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
h : μ.Integrable (f ∘ φ)
hφ : ¬Measurable φ
⊢ (μ.map φ).Integrable f

Tactic:
;

Goal state after:
case pos
X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : VectorMeasure X F
β : Type u_10
inst✝ : MeasurableSpace β
φ : X → β
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
h : μ.Integrable (f ∘ φ)
hφ : Measurable φ
⊢ (μ.map φ).Integrable f

case neg
X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : VectorMeasure X F
β : Type u_10
inst✝ : MeasurableSpace β
φ : X → β
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
h : μ.Integrable (f ∘ φ)
hφ : ¬Measurable φ
⊢ (μ.map φ).Integrable f
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case pos
X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : VectorMeasure X F
β : Type u_10
inst✝ : MeasurableSpace β
φ : X → β
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
h : μ.Integrable (f ∘ φ)
hφ : Measurable φ
⊢ (μ.map φ).Integrable f

Tactic:
VectorMeasure.Integrable

Goal state after:
case pos
X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : VectorMeasure X F
β : Type u_10
inst✝ : MeasurableSpace β
φ : X → β
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
h : Integrable (f ∘ φ) μ.variation
hφ : Measurable φ
⊢ Integrable f (μ.map φ).variation
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case of_isQF
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hψ : φ✝.IsQF
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
⊢ (φ ⟹ φ✝).IsPrenex

Tactic:
;

Goal state after:
case of_isQF
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hψ : φ✝.IsQF
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
⊢ (φ ⟹ φ✝).IsPrenex
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case of_isQF
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hφ : φ✝.IsQF
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ (φ✝.toPrenexImpRight ψ).IsPrenex

Tactic:
;

Goal state after:
case of_isQF
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hφ : φ✝.IsQF
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ (φ✝.toPrenexImpRight ψ).IsPrenex
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : IsDirectedOrder ι
x✝⁴ x✝³ x✝² : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ι
x : G i
j : ι
y : G j
x✝¹ :
  match ⟨i, x⟩ with
  | ⟨i, x⟩ =>
    match ⟨j, y⟩ with
    | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x = (f j k jk) y
k : ι
z : G k
x✝ :
  match ⟨j, y⟩ with
  | ⟨i, x⟩ =>
    match ⟨k, z⟩ with
    | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x = (f j k jk) y
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : (f i ij hiij) x = (f j ij hjij) y
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : (f j jk hjjk) y = (f k jk hkjk) z
ijk : ι
hijijk : ij ≤ ijk
hjkijk : jk ≤ ijk
⊢ (f ij ijk hijijk) ((f i ij hiij) x) = (f k ijk ⋯) z

Tactic:
hij,

Goal state after:
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : IsDirectedOrder ι
x✝⁴ x✝³ x✝² : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ι
x : G i
j : ι
y : G j
x✝¹ :
  match ⟨i, x⟩ with
  | ⟨i, x⟩ =>
    match ⟨j, y⟩ with
    | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x = (f j k jk) y
k : ι
z : G k
x✝ :
  match ⟨j, y⟩ with
  | ⟨i, x⟩ =>
    match ⟨k, z⟩ with
    | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x = (f j k jk) y
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : (f i ij hiij) x = (f j ij hjij) y
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : (f j jk hjjk) y = (f k jk hkjk) z
ijk : ι
hijijk : ij ≤ ijk
hjkijk : jk ≤ ijk
⊢ (f ij ijk hijijk) ((f j ij hjij) y) = (f k ijk ⋯) z
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
w✝ : f.dom ≤ g.dom
eq : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w✝)) = f.cod.subtype.comp f.toEquiv.toEmbedding
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) = f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
;

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
w✝ : f.dom ≤ g.dom
eq : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w✝)) = f.cod.subtype.comp f.toEquiv.toEmbedding
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) = f.cod.subtype.comp f.toEquiv.toEmbedding
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: 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:
;

Goal state after:
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)
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: 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:
;

Goal state after:
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))
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: 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:
;

Goal state after:
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✝
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: 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:
;

Goal state after:
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✝
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: 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:
;

Goal state after:
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✝
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: 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⟩
    rw [le_def]
    exact ⟨dom_le_dom, by ext; change subtype _ (g.toEquiv _) = _; rw [← h_eq]; rfl⟩

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f.symm ≤ g
⊢ f ≤ g.symm

Tactic:
;

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f.symm ≤ g
⊢ f ≤ g.symm
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f.symm ≤ g
⊢ f.symm.symm ≤ g.symm

Tactic:
;

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f.symm ≤ g
⊢ f.symm.symm ≤ g.symm
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g

Tactic:
;

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g.symm.symm

Tactic:
;

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g.symm.symm
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl.le_fg
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ ∃ (h : { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom ≤ g.dom),
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion h)) =
      { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding

Tactic:
;

Goal state after:
case refl.le_fg
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ ∃ (h : { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom ≤ g.dom),
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion h)) =
      { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
      { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding

Tactic:
;

Goal state after:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
      { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl.le_gf
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ ∃ (h : g.dom ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding.comp (inclusion h)) =
      g.cod.subtype.comp g.toEquiv.toEmbedding

Tactic:
;

Goal state after:
case refl.le_gf
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ ∃ (h : g.dom ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding.comp (inclusion h)) =
      g.cod.subtype.comp g.toEquiv.toEmbedding
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
      ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    g.cod.subtype.comp g.toEquiv.toEmbedding

Tactic:
;

Goal state after:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
      ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    g.cod.subtype.comp g.toEquiv.toEmbedding
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case mpr
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f.dom = g.dom
H : ∀ (x : M) (h_1 : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h_1⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ f = g

Tactic:
;

Goal state after:
case mpr
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f.dom = g.dom
H : ∀ (x : M) (h_1 : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h_1⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ f = g
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
A : L.Substructure M
hf : f.dom ≤ A
hg : A ≤ g.dom
hfg : f ≤ g
⊢ (g.domRestrict hg).cod.subtype.comp ((g.domRestrict hg).toEquiv.toEmbedding.comp (inclusion hf)) =
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯))

Tactic:
;

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
A : L.Substructure M
hf : f.dom ≤ A
hg : A ≤ g.dom
hfg : f ≤ g
⊢ (g.domRestrict hg).cod.subtype.comp ((g.domRestrict hg).toEquiv.toEmbedding.comp (inclusion hf)) =
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯))
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
h : f.dom = ⊤
⊢ (PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = f

Tactic:
rcases f with ⟨_, _, _⟩

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
dom✝ : L.Substructure M
cod✝ : L.Substructure N
toEquiv✝ : ↥dom✝ ≃[L] ↥cod✝
h : { dom := dom✝, cod := cod✝, toEquiv := toEquiv✝ }.dom = ⊤
⊢ (PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = { dom := dom✝, cod := cod✝, toEquiv := toEquiv✝ }
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
x y : DirectLimit G f
i : ι
hx : (Quotient.out x).fst ≤ i
hy : (Quotient.out y).fst ≤ i
xy :
  (g i) ((f (Quotient.out x).fst i hx) (Quotient.out x).snd) =
    (g i) ((f (Quotient.out y).fst i hy) (Quotient.out y).snd)
⊢ Quotient.out x ≈ Quotient.out y

Tactic:
equiv_iff G f hx hy

Goal state after:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
x y : DirectLimit G f
i : ι
hx : (Quotient.out x).fst ≤ i
hy : (Quotient.out y).fst ≤ i
xy :
  (g i) ((f (Quotient.out x).fst i hx) (Quotient.out x).snd) =
    (g i) ((f (Quotient.out y).fst i hy) (Quotient.out y).snd)
⊢ (f (Quotient.out x).fst i hx) (Quotient.out x).snd = (f (Quotient.out y).fst i hy) (Quotient.out y).snd