-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α → β
inst_1 : Finite α
inst_2 : Finite β
intro : ∀ (val : Fintype α), Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
intro₁ : ∀ (val : Fintype α) (val : Fintype β), Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
intro₂ :
  ∀ (val : Fintype α) (val_1 : Fintype β)
    (h :
      Definable.{u, v, w, u₁} A L (α := α)
        (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
          ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
            (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
                g ∘
                  (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                        (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                    (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                      (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
              (fun (g : β → M) ↦
                  g ∘
                    (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
                s))),
    Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
intro₃ :
  ∀ (val : Fintype α) (val_1 : Fintype β)
    (h :
      Definable.{u, v, w, u₁} A L (α := α)
        (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
          ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
            (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
                g ∘
                  (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                        (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                    (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                      (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
              (fun (g : β → M) ↦
                  g ∘
                    (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
                s)))
    (h' :
      Definable.{u, v, w, u₁} A L (α := α)
        {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}),
    Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
intro₄ :
  ∀ (val : Fintype α) (val_1 : Fintype β)
    (h :
      Definable.{u, v, w, u₁} A L (α := α)
        (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
          ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
            (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
                g ∘
                  (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                        (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                    (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                      (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
              (fun (g : β → M) ↦
                  g ∘
                    (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
                s)))
    (h' :
      Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))})
    (x : α → M),
    Membership.mem (γ := Set (α → M))
        (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
            ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦
                g ∘ Sum.inl) ''
              (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
                  g ∘
                    (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                          (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                      (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                        (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
                (fun (g : β → M) ↦
                    g ∘
                      (⇑(Equiv.Set.sumCompl (range f)) :
                        (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
                  s) ∩
          {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))})
        x ↔
      Membership.mem (γ := Set (α → M)) ((fun (g : β → M) ↦ g ∘ f) '' s) x
intro₅ :
  ∀ (val : Fintype α) (val_1 : Fintype β)
    (h :
      Definable.{u, v, w, u₁} A L (α := α)
        (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
          ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
            (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
                g ∘
                  (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                        (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                    (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                      (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
              (fun (g : β → M) ↦
                  g ∘
                    (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
                s)))
    (h' :
      Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))})
    (x : α → M),
    ((∃ a ∈ s,
          Function.comp (β := (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)))
              (Function.comp (β := (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))
                (a ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β))
                (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                      (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                  (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                    (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)))
              Sum.inl =
            x ∘ rangeSplitting f) ∧
        ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))) ↔
      ∃ x_1 ∈ s, x_1 ∘ f = x
intro₆ :
  ∀ (val : Fintype α) (val_1 : Fintype β)
    (h :
      Definable.{u, v, w, u₁} A L (α := α)
        (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
          ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
            (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
                g ∘
                  (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                        (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                    (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                      (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
              (fun (g : β → M) ↦
                  g ∘
                    (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
                s)))
    (h' :
      Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))})
    (x : α → M),
    ((∃ a ∈ s,
          Function.comp (β := (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)))
              (Function.comp (β := (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))
                (a ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β))
                (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                      (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                  (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                    (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)))
              Sum.inl =
            x ∘ rangeSplitting f) ∧
        ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))) →
      ∃ x_1 ∈ s, x_1 ∘ f = x
intro₇ intro₈ :
  ∀ (val : Fintype α) (val_1 : Fintype β)
    (h :
      Definable.{u, v, w, u₁} A L (α := α)
        (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
          ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
            (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
                g ∘
                  (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                        (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                    (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                      (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
              (fun (g : β → M) ↦
                  g ∘
                    (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
                s)))
    (h' :
      Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))})
    (x : α → M),
    (∃ x_1 ∈ s, x_1 ∘ f = x) →
      (∃ a ∈ s,
          Function.comp (β := (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)))
              (Function.comp (β := (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))
                (a ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β))
                (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                      (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                  (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                    (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)))
              Sum.inl =
            x ∘ rangeSplitting f) ∧
        ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)

Tactic:
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_sumInl_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_biInter_finset h' Finset.univ)
      simp
    refine (congr rfl (ext fun x => ?_)).mp (h.inter h')
    simp only [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]

Premises used: Set.rangeFactorization_coe, Set.mem_inter_iff, Set.mem_image, Set.mem_setOf_eq, nonempty_fintype, exists_exists_and_eq_and, Function.comp_apply, Set.apply_rangeSplitting, rfl, Set.mem_preimage