[GOAL]
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
L' : Language
inst✝¹ : Structure L' M
h : Definable A L s
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
⊢ Definable A L' s
[PROOFSTEP]
obtain ⟨ψ, rfl⟩ := h
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
ψ : Formula (L[[↑A]]) α
⊢ Definable A L' (setOf (Formula.Realize ψ))
[PROOFSTEP]
refine' ⟨(φ.addConstants A).onFormula ψ, _⟩
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
ψ : Formula (L[[↑A]]) α
⊢ setOf (Formula.Realize ψ) = setOf (Formula.Realize (LHom.onFormula (LHom.addConstants (↑A) φ) ψ))
[PROOFSTEP]
ext x
[GOAL]
case intro.h
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
ψ : Formula (L[[↑A]]) α
x : α → M
⊢ x ∈ setOf (Formula.Realize ψ) ↔ x ∈ setOf (Formula.Realize (LHom.onFormula (LHom.addConstants (↑A) φ) ψ))
[PROOFSTEP]
simp only [mem_setOf_eq, LHom.realize_onFormula]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
⊢ Definable ∅ L s ↔ ∃ φ, s = setOf (Formula.Realize φ)
[PROOFSTEP]
rw [Definable, Equiv.exists_congr_left (LEquiv.addEmptyConstants L (∅ : Set M)).onFormula]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
⊢ (∃ φ, s = setOf (Formula.Realize φ)) ↔
    ∃ b, s = setOf (Formula.Realize (↑(LEquiv.onFormula (LEquiv.addEmptyConstants L ↑∅)).symm b))
[PROOFSTEP]
simp [-constantsOn]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
hAs : Definable A L s
hAB : A ⊆ B
⊢ Definable B L s
[PROOFSTEP]
rw [definable_iff_empty_definable_with_params] at *
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
hAs : Definable ∅ (L[[↑A]]) s
hAB : A ⊆ B
⊢ Definable ∅ (L[[↑B]]) s
[PROOFSTEP]
exact hAs.map_expansion (L.lhomWithConstantsMap (Set.inclusion hAB))
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
⊢ ∅ = setOf (Formula.Realize ⊥)
[PROOFSTEP]
ext
[GOAL]
case h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
x✝ : α → M
⊢ x✝ ∈ ∅ ↔ x✝ ∈ setOf (Formula.Realize ⊥)
[PROOFSTEP]
simp
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
⊢ univ = setOf (Formula.Realize ⊤)
[PROOFSTEP]
ext
[GOAL]
case h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
x✝ : α → M
⊢ x✝ ∈ univ ↔ x✝ ∈ setOf (Formula.Realize ⊤)
[PROOFSTEP]
simp
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s f g : Set (α → M)
hf : Definable A L f
hg : Definable A L g
⊢ Definable A L (f ∩ g)
[PROOFSTEP]
rcases hf with ⟨φ, rfl⟩
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s g : Set (α → M)
hg : Definable A L g
φ : Formula (L[[↑A]]) α
⊢ Definable A L (setOf (Formula.Realize φ) ∩ g)
[PROOFSTEP]
rcases hg with ⟨θ, rfl⟩
[GOAL]
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
φ θ : Formula (L[[↑A]]) α
⊢ Definable A L (setOf (Formula.Realize φ) ∩ setOf (Formula.Realize θ))
[PROOFSTEP]
refine' ⟨φ ⊓ θ, _⟩
[GOAL]
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
φ θ : Formula (L[[↑A]]) α
⊢ setOf (Formula.Realize φ) ∩ setOf (Formula.Realize θ) = setOf (Formula.Realize (φ ⊓ θ))
[PROOFSTEP]
ext
[GOAL]
case intro.intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
φ θ : Formula (L[[↑A]]) α
x✝ : α → M
⊢ x✝ ∈ setOf (Formula.Realize φ) ∩ setOf (Formula.Realize θ) ↔ x✝ ∈ setOf (Formula.Realize (φ ⊓ θ))
[PROOFSTEP]
simp
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s f g : Set (α → M)
hf : Definable A L f
hg : Definable A L g
⊢ Definable A L (f ∪ g)
[PROOFSTEP]
rcases hf with ⟨φ, hφ⟩
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s f g : Set (α → M)
hg : Definable A L g
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
⊢ Definable A L (f ∪ g)
[PROOFSTEP]
rcases hg with ⟨θ, hθ⟩
[GOAL]
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s f g : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
θ : Formula (L[[↑A]]) α
hθ : g = setOf (Formula.Realize θ)
⊢ Definable A L (f ∪ g)
[PROOFSTEP]
refine' ⟨φ ⊔ θ, _⟩
[GOAL]
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s f g : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
θ : Formula (L[[↑A]]) α
hθ : g = setOf (Formula.Realize θ)
⊢ f ∪ g = setOf (Formula.Realize (φ ⊔ θ))
[PROOFSTEP]
ext
[GOAL]
case intro.intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s f g : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
θ : Formula (L[[↑A]]) α
hθ : g = setOf (Formula.Realize θ)
x✝ : α → M
⊢ x✝ ∈ f ∪ g ↔ x✝ ∈ setOf (Formula.Realize (φ ⊔ θ))
[PROOFSTEP]
rw [hφ, hθ, mem_setOf_eq, Formula.realize_sup, mem_union, mem_setOf_eq, mem_setOf_eq]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (Finset.inf s f)
[PROOFSTEP]
classical
refine' Finset.induction definable_univ (fun i s _ h => _) s
rw [Finset.inf_insert]
exact (hf i).inter h
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (Finset.inf s f)
[PROOFSTEP]
refine' Finset.induction definable_univ (fun i s _ h => _) s
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝¹ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : Definable A L (Finset.inf s f)
⊢ Definable A L (Finset.inf (insert i s) f)
[PROOFSTEP]
rw [Finset.inf_insert]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝¹ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : Definable A L (Finset.inf s f)
⊢ Definable A L (f i ⊓ Finset.inf s f)
[PROOFSTEP]
exact (hf i).inter h
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (Finset.sup s f)
[PROOFSTEP]
classical
refine' Finset.induction definable_empty (fun i s _ h => _) s
rw [Finset.sup_insert]
exact (hf i).union h
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (Finset.sup s f)
[PROOFSTEP]
refine' Finset.induction definable_empty (fun i s _ h => _) s
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝¹ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : Definable A L (Finset.sup s f)
⊢ Definable A L (Finset.sup (insert i s) f)
[PROOFSTEP]
rw [Finset.sup_insert]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝¹ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : Definable A L (Finset.sup s f)
⊢ Definable A L (f i ⊔ Finset.sup s f)
[PROOFSTEP]
exact (hf i).union h
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (⋂ (i : ι) (_ : i ∈ s), f i)
[PROOFSTEP]
rw [← Finset.inf_set_eq_iInter]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (Finset.inf s fun i => f i)
[PROOFSTEP]
exact definable_finset_inf hf s
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (⋃ (i : ι) (_ : i ∈ s), f i)
[PROOFSTEP]
rw [← Finset.sup_set_eq_biUnion]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (Finset.sup s fun i => f i)
[PROOFSTEP]
exact definable_finset_sup hf s
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ s : Set (α → M)
hf : Definable A L s
⊢ Definable A L sᶜ
[PROOFSTEP]
rcases hf with ⟨φ, hφ⟩
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ s : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : s = setOf (Formula.Realize φ)
⊢ Definable A L sᶜ
[PROOFSTEP]
refine' ⟨φ.not, _⟩
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ s : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : s = setOf (Formula.Realize φ)
⊢ sᶜ = setOf (Formula.Realize (Formula.not φ))
[PROOFSTEP]
ext v
[GOAL]
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ s : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : s = setOf (Formula.Realize φ)
v : α → M
⊢ v ∈ sᶜ ↔ v ∈ setOf (Formula.Realize (Formula.not φ))
[PROOFSTEP]
rw [hφ, compl_setOf, mem_setOf, mem_setOf, Formula.realize_not]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
f : α → β
s : Set (α → M)
h : Definable A L s
⊢ Definable A L ((fun g => g ∘ f) ⁻¹' s)
[PROOFSTEP]
obtain ⟨φ, rfl⟩ := h
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
f : α → β
φ : Formula (L[[↑A]]) α
⊢ Definable A L ((fun g => g ∘ f) ⁻¹' setOf (Formula.Realize φ))
[PROOFSTEP]
refine' ⟨φ.relabel f, _⟩
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
f : α → β
φ : Formula (L[[↑A]]) α
⊢ (fun g => g ∘ f) ⁻¹' setOf (Formula.Realize φ) = setOf (Formula.Realize (Formula.relabel f φ))
[PROOFSTEP]
ext
[GOAL]
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
f : α → β
φ : Formula (L[[↑A]]) α
x✝ : β → M
⊢ x✝ ∈ (fun g => g ∘ f) ⁻¹' setOf (Formula.Realize φ) ↔ x✝ ∈ setOf (Formula.Realize (Formula.relabel f φ))
[PROOFSTEP]
simp only [Set.preimage_setOf_eq, mem_setOf_eq, Formula.realize_relabel]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
⊢ Definable A L ((fun g => g ∘ ↑f) '' s)
[PROOFSTEP]
refine' (congr rfl _).mp (h.preimage_comp f.symm)
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
⊢ (fun g => g ∘ ↑f.symm) ⁻¹' s = (fun g => g ∘ ↑f) '' s
[PROOFSTEP]
rw [image_eq_preimage_of_inverse]
[GOAL]
case h₁
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
⊢ Function.LeftInverse (fun g => g ∘ ↑f.symm) fun g => g ∘ ↑f
[PROOFSTEP]
intro i
[GOAL]
case h₁
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
i : β → M
⊢ (fun g => g ∘ ↑f.symm) ((fun g => g ∘ ↑f) i) = i
[PROOFSTEP]
ext b
[GOAL]
case h₁.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
i : β → M
b : β
⊢ (fun g => g ∘ ↑f.symm) ((fun g => g ∘ ↑f) i) b = i b
[PROOFSTEP]
simp only [Function.comp_apply, Equiv.apply_symm_apply]
[GOAL]
case h₂
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
⊢ Function.RightInverse (fun g => g ∘ ↑f.symm) fun g => g ∘ ↑f
[PROOFSTEP]
intro i
[GOAL]
case h₂
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
i : α → M
⊢ (fun g => g ∘ ↑f) ((fun g => g ∘ ↑f.symm) i) = i
[PROOFSTEP]
ext a
[GOAL]
case h₂.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
i : α → M
a : α
⊢ (fun g => g ∘ ↑f) ((fun g => g ∘ ↑f.symm) i) a = i a
[PROOFSTEP]
simp
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
m : ℕ
s : Set (α ⊕ Fin m → M)
h : Definable A L s
⊢ Definable A L ((fun g => g ∘ Sum.inl) '' s)
[PROOFSTEP]
obtain ⟨φ, rfl⟩ := h
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
⊢ Definable A L ((fun g => g ∘ Sum.inl) '' setOf (Formula.Realize φ))
[PROOFSTEP]
refine' ⟨(BoundedFormula.relabel id φ).exs, _⟩
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
⊢ (fun g => g ∘ Sum.inl) '' setOf (Formula.Realize φ) =
    setOf (Formula.Realize (BoundedFormula.exs (BoundedFormula.relabel id φ)))
[PROOFSTEP]
ext x
[GOAL]
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
x : α → M
⊢ x ∈ (fun g => g ∘ Sum.inl) '' setOf (Formula.Realize φ) ↔
    x ∈ setOf (Formula.Realize (BoundedFormula.exs (BoundedFormula.relabel id φ)))
[PROOFSTEP]
simp only [Set.mem_image, mem_setOf_eq, BoundedFormula.realize_exs, BoundedFormula.realize_relabel,
  Function.comp.right_id, Fin.castAdd_zero, Fin.castIso_refl]
[GOAL]
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
x : α → M
⊢ (∃ x_1, Formula.Realize φ x_1 ∧ x_1 ∘ Sum.inl = x) ↔
    ∃ xs, BoundedFormula.Realize φ (Sum.elim x (xs ∘ Fin.cast (_ : m = m))) (xs ∘ Fin.natAdd m)
[PROOFSTEP]
constructor
[GOAL]
case intro.h.mp
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
x : α → M
⊢ (∃ x_1, Formula.Realize φ x_1 ∧ x_1 ∘ Sum.inl = x) →
    ∃ xs, BoundedFormula.Realize φ (Sum.elim x (xs ∘ Fin.cast (_ : m = m))) (xs ∘ Fin.natAdd m)
[PROOFSTEP]
rintro ⟨y, hy, rfl⟩
[GOAL]
case intro.h.mp.intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
y : α ⊕ Fin m → M
hy : Formula.Realize φ y
⊢ ∃ xs, BoundedFormula.Realize φ (Sum.elim (y ∘ Sum.inl) (xs ∘ Fin.cast (_ : m = m))) (xs ∘ Fin.natAdd m)
[PROOFSTEP]
exact ⟨y ∘ Sum.inr, (congr (congr rfl (Sum.elim_comp_inl_inr y).symm) (funext finZeroElim)).mp hy⟩
[GOAL]
case intro.h.mpr
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
x : α → M
⊢ (∃ xs, BoundedFormula.Realize φ (Sum.elim x (xs ∘ Fin.cast (_ : m = m))) (xs ∘ Fin.natAdd m)) →
    ∃ x_1, Formula.Realize φ x_1 ∧ x_1 ∘ Sum.inl = x
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case intro.h.mpr.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
x : α → M
y : Fin (m + 0) → M
hy : BoundedFormula.Realize φ (Sum.elim x (y ∘ Fin.cast (_ : m = m))) (y ∘ Fin.natAdd m)
⊢ ∃ x_1, Formula.Realize φ x_1 ∧ x_1 ∘ Sum.inl = x
[PROOFSTEP]
exact ⟨Sum.elim x y, (congr rfl (funext finZeroElim)).mp hy, Sum.elim_comp_inl _ _⟩
[GOAL]
M : Type w
A : Set M
L : Language
inst✝¹ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ↪ β
inst✝ : Finite β
⊢ Definable A L ((fun g => g ∘ ↑f) '' s)
[PROOFSTEP]
classical
cases nonempty_fintype β
refine'
  (congr rfl (ext fun x => _)).mp
    (((h.image_comp_equiv (Equiv.Set.sumCompl (range f))).image_comp_equiv
          (Equiv.sumCongr (Equiv.ofInjective f f.injective)
            (Fintype.equivFin (↥(range f)ᶜ)).symm)).image_comp_sum_inl_fin
      _)
simp only [mem_preimage, mem_image, exists_exists_and_eq_and]
refine' exists_congr fun y => and_congr_right fun _ => Eq.congr_left (funext fun a => _)
simp
[GOAL]
M : Type w
A : Set M
L : Language
inst✝¹ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ↪ β
inst✝ : Finite β
⊢ Definable A L ((fun g => g ∘ ↑f) '' s)
[PROOFSTEP]
cases nonempty_fintype β
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝¹ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ↪ β
inst✝ : Finite β
val✝ : Fintype β
⊢ Definable A L ((fun g => g ∘ ↑f) '' s)
[PROOFSTEP]
refine'
  (congr rfl (ext fun x => _)).mp
    (((h.image_comp_equiv (Equiv.Set.sumCompl (range f))).image_comp_equiv
          (Equiv.sumCongr (Equiv.ofInjective f f.injective)
            (Fintype.equivFin (↥(range f)ᶜ)).symm)).image_comp_sum_inl_fin
      _)
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝¹ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ↪ β
inst✝ : Finite β
val✝ : Fintype β
x : α → M
⊢ x ∈
      (fun g => g ∘ Sum.inl) ''
        ((fun g =>
            g ∘
              ↑(Equiv.sumCongr (Equiv.ofInjective ↑f (_ : Function.Injective ↑f))
                  (Fintype.equivFin ↑(range ↑f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range ↑f))) '' s)) ↔
    x ∈ (fun g => g ∘ ↑f) '' s
[PROOFSTEP]
simp only [mem_preimage, mem_image, exists_exists_and_eq_and]
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝¹ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ↪ β
inst✝ : Finite β
val✝ : Fintype β
x : α → M
⊢ (∃ a,
      a ∈ s ∧
        ((a ∘ ↑(Equiv.Set.sumCompl (range ↑f))) ∘
              ↑(Equiv.sumCongr (Equiv.ofInjective ↑f (_ : Function.Injective ↑f))
                  (Fintype.equivFin ↑(range ↑f)ᶜ).symm)) ∘
            Sum.inl =
          x) ↔
    ∃ x_1, x_1 ∈ s ∧ x_1 ∘ ↑f = x
[PROOFSTEP]
refine' exists_congr fun y => and_congr_right fun _ => Eq.congr_left (funext fun a => _)
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝¹ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ↪ β
inst✝ : Finite β
val✝ : Fintype β
x : α → M
y : β → M
x✝ : y ∈ s
a : α
⊢ (((y ∘ ↑(Equiv.Set.sumCompl (range ↑f))) ∘
          ↑(Equiv.sumCongr (Equiv.ofInjective ↑f (_ : Function.Injective ↑f)) (Fintype.equivFin ↑(range ↑f)ᶜ).symm)) ∘
        Sum.inl)
      a =
    (y ∘ ↑f) a
[PROOFSTEP]
simp
[GOAL]
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Definable A L ((fun g => g ∘ f) '' s)
[PROOFSTEP]
classical
cases nonempty_fintype α
cases nonempty_fintype β
have h :=
  (((h.image_comp_equiv (Equiv.Set.sumCompl (range f))).image_comp_equiv
            (Equiv.sumCongr (_root_.Equiv.refl _) (Fintype.equivFin _).symm)).image_comp_sum_inl_fin
        _).preimage_comp
    (rangeSplitting f)
have h' : A.Definable L {x : α → M | ∀ a, x a = x (rangeSplitting f (rangeFactorization f a))} :=
  by
  have h' : ∀ a, A.Definable L {x : α → M | x a = x (rangeSplitting f (rangeFactorization f a))} :=
    by
    refine' fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext _⟩
    simp
  refine' (congr rfl (ext _)).mp (definable_finset_biInter h' Finset.univ)
  simp
refine' (congr rfl (ext fun x => _)).mp (h.inter h')
simp only [Equiv.coe_trans, mem_inter_iff, mem_preimage, mem_image, exists_exists_and_eq_and, mem_setOf_eq]
constructor
· rintro ⟨⟨y, ys, hy⟩, hx⟩
  refine' ⟨y, ys, _⟩
  ext a
  rw [hx a, ← Function.comp_apply (f := x), ← hy]
  simp
· rintro ⟨y, ys, rfl⟩
  refine' ⟨⟨y, ys, _⟩, fun a => _⟩
  · ext
    simp [Set.apply_rangeSplitting f]
  · rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f, rangeFactorization_coe]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Definable A L ((fun g => g ∘ f) '' s)
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝ : Fintype α
⊢ Definable A L ((fun g => g ∘ f) '' s)
[PROOFSTEP]
cases nonempty_fintype β
[GOAL]
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
⊢ Definable A L ((fun g => g ∘ f) '' s)
[PROOFSTEP]
have h :=
  (((h.image_comp_equiv (Equiv.Set.sumCompl (range f))).image_comp_equiv
            (Equiv.sumCongr (_root_.Equiv.refl _) (Fintype.equivFin _).symm)).image_comp_sum_inl_fin
        _).preimage_comp
    (rangeSplitting f)
[GOAL]
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
⊢ Definable A L ((fun g => g ∘ f) '' s)
[PROOFSTEP]
have h' : A.Definable L {x : α → M | ∀ a, x a = x (rangeSplitting f (rangeFactorization f a))} :=
  by
  have h' : ∀ a, A.Definable L {x : α → M | x a = x (rangeSplitting f (rangeFactorization f a))} :=
    by
    refine' fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext _⟩
    simp
  refine' (congr rfl (ext _)).mp (definable_finset_biInter h' Finset.univ)
  simp
[GOAL]
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
⊢ Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
[PROOFSTEP]
have h' : ∀ a, A.Definable L {x : α → M | x a = x (rangeSplitting f (rangeFactorization f a))} :=
  by
  refine' fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext _⟩
  simp
[GOAL]
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
⊢ ∀ (a : α), Definable A L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
[PROOFSTEP]
refine' fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext _⟩
[GOAL]
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
a : α
⊢ ∀ (x : α → M),
    x ∈ {x | x a = x (rangeSplitting f (rangeFactorization f a))} ↔
      x ∈ setOf (Formula.Realize (Term.equal (var a) (var (rangeSplitting f (rangeFactorization f a)))))
[PROOFSTEP]
simp
[GOAL]
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : ∀ (a : α), Definable A L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
[PROOFSTEP]
refine' (congr rfl (ext _)).mp (definable_finset_biInter h' Finset.univ)
[GOAL]
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : ∀ (a : α), Definable A L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ ∀ (x : α → M),
    x ∈ ⋂ (i : α) (_ : i ∈ Finset.univ), {x | x i = x (rangeSplitting f (rangeFactorization f i))} ↔
      x ∈ {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
[PROOFSTEP]
simp
[GOAL]
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ Definable A L ((fun g => g ∘ f) '' s)
[PROOFSTEP]
refine' (congr rfl (ext fun x => _)).mp (h.inter h')
[GOAL]
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ x ∈
      (fun g => g ∘ rangeSplitting f) ⁻¹'
          ((fun g => g ∘ Sum.inl) ''
            ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
              ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))) ∩
        {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))} ↔
    x ∈ (fun g => g ∘ f) '' s
[PROOFSTEP]
simp only [Equiv.coe_trans, mem_inter_iff, mem_preimage, mem_image, exists_exists_and_eq_and, mem_setOf_eq]
[GOAL]
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ ((∃ a,
        a ∈ s ∧
          ((a ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
                ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
              Sum.inl =
            x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))) ↔
    ∃ x_1, x_1 ∈ s ∧ x_1 ∘ f = x
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.mp
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ ((∃ a,
        a ∈ s ∧
          ((a ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
                ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
              Sum.inl =
            x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))) →
    ∃ x_1, x_1 ∈ s ∧ x_1 ∘ f = x
[PROOFSTEP]
rintro ⟨⟨y, ys, hy⟩, hx⟩
[GOAL]
case intro.intro.mp.intro.intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
⊢ ∃ x_1, x_1 ∈ s ∧ x_1 ∘ f = x
[PROOFSTEP]
refine' ⟨y, ys, _⟩
[GOAL]
case intro.intro.mp.intro.intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
⊢ y ∘ f = x
[PROOFSTEP]
ext a
[GOAL]
case intro.intro.mp.intro.intro.intro.h
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
a : α
⊢ (y ∘ f) a = x a
[PROOFSTEP]
rw [hx a, ← Function.comp_apply (f := x), ← hy]
[GOAL]
case intro.intro.mp.intro.intro.intro.h
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
a : α
⊢ (y ∘ f) a =
    (((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
          ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
        Sum.inl)
      (rangeFactorization f a)
[PROOFSTEP]
simp
[GOAL]
case intro.intro.mpr
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ (∃ x_1, x_1 ∈ s ∧ x_1 ∘ f = x) →
    (∃ a,
        a ∈ s ∧
          ((a ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
                ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
              Sum.inl =
            x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
[PROOFSTEP]
rintro ⟨y, ys, rfl⟩
[GOAL]
case intro.intro.mpr.intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
⊢ (∃ a,
      a ∈ s ∧
        ((a ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
              ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
            Sum.inl =
          (y ∘ f) ∘ rangeSplitting f) ∧
    ∀ (a : α), (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
[PROOFSTEP]
refine' ⟨⟨y, ys, _⟩, fun a => _⟩
[GOAL]
case intro.intro.mpr.intro.intro.refine'_1
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
⊢ ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    (y ∘ f) ∘ rangeSplitting f
[PROOFSTEP]
ext
[GOAL]
case intro.intro.mpr.intro.intro.refine'_1.h
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
x✝ : ↑(range f)
⊢ (((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
          ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
        Sum.inl)
      x✝ =
    ((y ∘ f) ∘ rangeSplitting f) x✝
[PROOFSTEP]
simp [Set.apply_rangeSplitting f]
[GOAL]
case intro.intro.mpr.intro.intro.refine'_2
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
a : α
⊢ (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
[PROOFSTEP]
rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f, rangeFactorization_coe]
