awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)
A0 : Finset M := Finset.image (Subtype.val (p := fun (x : M) ↦ x ∈ A)) (BoundedFormula.freeVarFinset φ).toLeft
x : α → M
⊢ BoundedFormula.Realize φ (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) default ↔
    BoundedFormula.Realize (α := Sum.{w, u₁} (↥A0) α)
      (BoundedFormula.restrictFreeVar φ fun (x : ↥(BoundedFormula.freeVarFinset φ)) ↦
        Sum.rec (motive := fun (x : Sum.{w, u₁} (↑A : Type w) α) ↦
          x ∈ BoundedFormula.freeVarFinset φ → Sum.{w, u₁} (↥A0) α)
          (fun (val : (↑A : Type w)) (hx : Sum.inl val ∈ BoundedFormula.freeVarFinset φ) ↦
            Sum.inl (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑A0 : Set M)) (↑val : M) ⋯))
          (fun (val : α) (x : Sum.inr val ∈ BoundedFormula.freeVarFinset φ) ↦ Sum.inr val) (↑x : (↑A : Type w) ⊕ α) ⋯)
      (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) x) default

Tactic:
exact iff_comm.1 <| BoundedFormula.realize_restrictFreeVar _ (by simp)

Premises used: iff_comm, Iff.mp, FirstOrder.Language.BoundedFormula.realize_restrictFreeVar
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
A0 : Finset M
hA0 : (↑A0 : Set M) ⊆ A
hd : (↑A0 : Set M).Definable L s
⊢ A.Definable L s

Tactic:
Definable.mono hd hA0

Premises used: Set.Definable.mono
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
A0 : Finset M
hA0 : (↑A0 : Set M) ⊆ A
hd : (↑A0 : Set M).Definable L s
⊢ A.Definable L s

Tactic:
exact Definable.mono hd hA0

Premises used: Set.Definable.mono
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
mp : A.Definable L s → ∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s
mpr mpr₁ : (∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s) → A.Definable L s
⊢ A.Definable L s ↔ ∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s

Tactic:
classical
  constructor
  · simp only [definable_iff_exists_formula_sum]
    rintro ⟨φ, rfl⟩
    let A0 := (φ.freeVarFinset.toLeft).image Subtype.val
    refine ⟨A0, by simp [A0], (φ.restrictFreeVar <| fun x => Sum.casesOn x.1
        (fun x hx => Sum.inl ⟨x, by simp [A0, hx]⟩) (fun x _ => Sum.inr x) x.2), ?_⟩
    ext
    simp only [Formula.Realize, mem_setOf_eq, Finset.coe_sort_coe]
    exact iff_comm.1 <| BoundedFormula.realize_restrictFreeVar _ (by simp)
  · rintro ⟨A0, hA0, hd⟩
    exact Definable.mono hd hA0

Premises used: Finset.coe_sort_coe, Set.definable_iff_exists_formula_sum, iff_comm, Set.mem_setOf_eq, Iff.mp, rfl, FirstOrder.Language.Formula.Realize, FirstOrder.Language.BoundedFormula.realize_restrictFreeVar
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
m : ℕ
s : Set (α ⊕ Fin m → M)
h : A.Definable L s
obtain :
  ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ Fin m)),
    Definable.{u, v, w, u₁} A L (α := α) ((fun (g : α ⊕ Fin m → M) ↦ g ∘ Sum.inl) '' setOf φ.Realize)
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : α ⊕ Fin m → M) ↦ g ∘ Sum.inl) '' s)

Tactic:
obtain ⟨φ, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
m : ℕ
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ Fin m)
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : α ⊕ Fin m → M) ↦ g ∘ Sum.inl) '' setOf φ.Realize)

Tactic:
⟨(BoundedFormula.relabel id φ).exs, ?_⟩

Premises used: Set.Definable, FirstOrder.Language.BoundedFormula.exs, FirstOrder.Language.BoundedFormula.relabel, id, Exists.intro
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
m : ℕ
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ Fin m)
refine :
  Eq (α := Set (α → M)) ((fun (g : α ⊕ Fin m → M) ↦ g ∘ Sum.inl) '' setOf φ.Realize)
    (setOf (BoundedFormula.relabel id φ).exs.Realize)
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : α ⊕ Fin m → M) ↦ g ∘ Sum.inl) '' setOf φ.Realize)

Tactic:
refine ⟨(BoundedFormula.relabel id φ).exs, ?_⟩
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
m : ℕ
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ Fin m)
h :
  ∀ (x : α → M),
    Membership.mem (γ := Set (α → M)) ((fun (g : α ⊕ Fin m → M) ↦ g ∘ Sum.inl) '' setOf φ.Realize) x ↔
      Membership.mem (γ := Set (α → M)) (setOf (BoundedFormula.relabel id φ).exs.Realize) x
⊢ Eq (α := Set (α → M)) ((fun (g : α ⊕ Fin m → M) ↦ g ∘ Sum.inl) '' setOf φ.Realize)
    (setOf (BoundedFormula.relabel id φ).exs.Realize)

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
m : ℕ
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ Fin m)
x : α → M
h :
  (∃ (x_1 : α ⊕ Fin m → M), φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x) ↔
    ∃ (xs : Fin (m + 0) → M), BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)
⊢ Membership.mem (γ := Set (α → M)) ((fun (g : α ⊕ Fin m → M) ↦ g ∘ Sum.inl) '' setOf φ.Realize) x ↔
    Membership.mem (γ := Set (α → M)) (setOf (BoundedFormula.relabel id φ).exs.Realize) x

Tactic:
simp only [Set.mem_image, mem_setOf_eq, BoundedFormula.realize_exs,
    BoundedFormula.realize_relabel, Function.comp_id, Fin.castAdd_zero, Fin.cast_refl]

Premises used: Function.comp_id, Set.mem_image, Fin.castAdd_zero, Set.mem_setOf_eq, FirstOrder.Language.BoundedFormula.realize_relabel, FirstOrder.Language.BoundedFormula.realize_exs, Fin.cast_refl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
m : ℕ
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ Fin m)
x : α → M
h :
  (∃ (x_1 : α ⊕ Fin m → M), φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x) →
    ∃ (xs : Fin (m + 0) → M), BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)
h₁ :
  (∃ (xs : Fin (m + 0) → M), BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)) →
    ∃ (x_1 : α ⊕ Fin m → M), φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x
⊢ (∃ (x_1 : α ⊕ Fin m → M), φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x) ↔
    ∃ (xs : Fin (m + 0) → M), BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
m : ℕ
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ Fin m)
y : α ⊕ Fin m → M
hy : φ.Realize y
⊢ ∃ (xs : Fin (m + 0) → M), BoundedFormula.Realize φ (Sum.elim (y ∘ Sum.inl) xs) (xs ∘ Fin.natAdd m)

Tactic:
⟨y ∘ Sum.inr, (congr (congr rfl (Sum.elim_comp_inl_inr y).symm) (funext finZeroElim)).mp hy⟩

Premises used: finZeroElim, Function.comp, Eq.mp, funext, Sum.inr, congr, Exists.intro, Eq.symm, Sum.elim_comp_inl_inr, rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
m : ℕ
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ Fin m)
y : α ⊕ Fin m → M
hy : φ.Realize y
⊢ ∃ (xs : Fin (m + 0) → M), BoundedFormula.Realize φ (Sum.elim (y ∘ Sum.inl) xs) (xs ∘ Fin.natAdd m)

Tactic:
exact
      ⟨y ∘ Sum.inr, (congr (congr rfl (Sum.elim_comp_inl_inr y).symm) (funext finZeroElim)).mp hy⟩
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
m : ℕ
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ Fin m)
x : α → M
y : Fin (m + 0) → M
hy : BoundedFormula.Realize φ (Sum.elim x y) (y ∘ Fin.natAdd m)
⊢ ∃ (x_1 : α ⊕ Fin m → M), φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x

Tactic:
⟨Sum.elim x y, (congr rfl (funext finZeroElim)).mp hy, Sum.elim_comp_inl _ _⟩

Premises used: finZeroElim, Sum.elim_comp_inl, Eq.mp, funext, And.intro, congr, Exists.intro, rfl, Sum.elim
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
m : ℕ
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ Fin m)
x : α → M
y : Fin (m + 0) → M
hy : BoundedFormula.Realize φ (Sum.elim x y) (y ∘ Fin.natAdd m)
⊢ ∃ (x_1 : α ⊕ Fin m → M), φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x

Tactic:
exact ⟨Sum.elim x y, (congr rfl (funext finZeroElim)).mp hy, Sum.elim_comp_inl _ _⟩
-- 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 β
intro : ∀ (val : Fintype β), Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)

Tactic:
cases nonempty_fintype β

Premises used: nonempty_fintype
-- 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 β
val : Fintype β
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)

Tactic:
(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_sumInl_fin
          _)

Premises used: Set.ext, Compl.compl, Equiv.Set.sumCompl, Eq.mp, Set.Elem, Fintype.equivFin, Equiv.ofInjective, Equiv.sumCongr, congr, Function.Embedding.injective, Set.range, Equiv.symm, DFunLike.coe, rfl, Set.Definable.image_comp_sumInl_fin, Set.Definable.image_comp_equiv
-- 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 β
val : Fintype β
intro :
  ∀ (x : α → M),
    Membership.mem (γ := Set (α → M))
        ((fun (g : α ⊕ Fin (Fintype.card.{u_1} (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)) → M) ↦
            g ∘ Sum.inl) ''
          (fun
                (g :
                  (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_1) ⊕
                      (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1) →
                    M) ↦
              g ∘
                (⇑((Equiv.ofInjective (⇑f : (a : α) → β) ⋯).sumCongr
                      (Equiv.symm
                        (Fintype.equivFin (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))) :
                  (a : α ⊕ Fin (Fintype.card (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1))) →
                    (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1))) ''
            (fun (g : β → M) ↦
                g ∘
                  (⇑(Equiv.Set.sumCompl (range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))) :
                    (a : (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)) → β)) ''
              s)
        x ↔
      Membership.mem (γ := Set (α → M)) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s) x
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)

Tactic:
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_sumInl_fin
          _)

Premises used: Set.ext, Compl.compl, Equiv.Set.sumCompl, Eq.mp, Set.Elem, Fintype.equivFin, Equiv.ofInjective, Equiv.sumCongr, congr, Function.Embedding.injective, Set.range, Equiv.symm, DFunLike.coe, rfl, Set.Definable.image_comp_sumInl_fin, Set.Definable.image_comp_equiv
-- 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 β
val : Fintype β
x : α → M
intro :
  (∃ a ∈ s,
      Function.comp (β := α ⊕ Fin (Fintype.card.{u_1} (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))
          (Function.comp (β :=
            (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_1) ⊕
              (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1))
            (a ∘
              (⇑(Equiv.Set.sumCompl (range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))) :
                (a : (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)) → β))
            (⇑((Equiv.ofInjective (⇑f : (a : α) → β) ⋯).sumCongr
                  (Equiv.symm (Fintype.equivFin (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))) :
              (a : α ⊕ Fin (Fintype.card (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1))) →
                (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)))
          Sum.inl =
        x) ↔
    ∃ x_1 ∈ s, x_1 ∘ (⇑f : (a : α) → β) = x
⊢ Membership.mem (γ := Set (α → M))
      ((fun (g : α ⊕ Fin (Fintype.card.{u_1} (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)) → M) ↦
          g ∘ Sum.inl) ''
        (fun
              (g :
                (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_1) ⊕
                    (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1) →
                  M) ↦
            g ∘
              (⇑((Equiv.ofInjective (⇑f : (a : α) → β) ⋯).sumCongr
                    (Equiv.symm (Fintype.equivFin (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))) :
                (a : α ⊕ Fin (Fintype.card (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1))) →
                  (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1))) ''
          (fun (g : β → M) ↦
              g ∘
                (⇑(Equiv.Set.sumCompl (range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))) :
                  (a : (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)) → β)) ''
            s)
      x ↔
    Membership.mem (γ := Set (α → M)) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s) x

Tactic:
simp only [mem_image, exists_exists_and_eq_and]

Premises used: Set.mem_image, exists_exists_and_eq_and
-- 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 β
val : Fintype β
x : α → M
⊢ (∃ a ∈ s,
      Function.comp (β := α ⊕ Fin (Fintype.card.{u_1} (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))
          (Function.comp (β :=
            (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_1) ⊕
              (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1))
            (a ∘
              (⇑(Equiv.Set.sumCompl (range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))) :
                (a : (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)) → β))
            (⇑((Equiv.ofInjective (⇑f : (a : α) → β) ⋯).sumCongr
                  (Equiv.symm (Fintype.equivFin (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))) :
              (a : α ⊕ Fin (Fintype.card (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1))) →
                (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)))
          Sum.inl =
        x) ↔
    ∃ x_1 ∈ s, x_1 ∘ (⇑f : (a : α) → β) = x

Tactic:
exists_congr fun y => and_congr_right fun _ => Eq.congr_left (funext fun a => ?_)

Premises used: Eq.congr_left, and_congr_right, funext, exists_congr
-- 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 β
val : Fintype β
x : α → M
intro :
  ∀ y ∈ s,
    ∀ (a : α),
      Function.comp (β := α ⊕ Fin (Fintype.card.{u_1} (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))
          (Function.comp (β :=
            (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_1) ⊕
              (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1))
            (y ∘
              (⇑(Equiv.Set.sumCompl (range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))) :
                (a : (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)) → β))
            (⇑((Equiv.ofInjective (⇑f : (a : α) → β) ⋯).sumCongr
                  (Equiv.symm (Fintype.equivFin (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))) :
              (a : α ⊕ Fin (Fintype.card (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1))) →
                (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)))
          Sum.inl a =
        (y ∘ (⇑f : (a : α) → β)) a
⊢ (∃ a ∈ s,
      Function.comp (β := α ⊕ Fin (Fintype.card.{u_1} (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))
          (Function.comp (β :=
            (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_1) ⊕
              (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1))
            (a ∘
              (⇑(Equiv.Set.sumCompl (range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))) :
                (a : (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)) → β))
            (⇑((Equiv.ofInjective (⇑f : (a : α) → β) ⋯).sumCongr
                  (Equiv.symm (Fintype.equivFin (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))) :
              (a : α ⊕ Fin (Fintype.card (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1))) →
                (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)))
          Sum.inl =
        x) ↔
    ∃ x_1 ∈ s, x_1 ∘ (⇑f : (a : α) → β) = x

Tactic:
refine exists_congr fun y => and_congr_right fun _ => Eq.congr_left (funext fun a => ?_)

Premises used: Eq.congr_left, and_congr_right, funext, exists_congr
-- 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 β
val : Fintype β
x : α → M
y : β → M
h_1 : y ∈ s
a : α
⊢ Function.comp (β := α ⊕ Fin (Fintype.card.{u_1} (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))
      (Function.comp (β :=
        (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_1) ⊕
          (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1))
        (y ∘
          (⇑(Equiv.Set.sumCompl (range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))) :
            (a : (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)) → β))
        (⇑((Equiv.ofInjective (⇑f : (a : α) → β) ⋯).sumCongr
              (Equiv.symm (Fintype.equivFin (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))) :
          (a : α ⊕ Fin (Fintype.card (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1))) →
            (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)))
      Sum.inl a =
    (y ∘ (⇑f : (a : α) → β)) a

Tactic:
simp
-- 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)
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- 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 β
val : Fintype α
intro : ∀ (val : Fintype β), Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)

Tactic:
cases nonempty_fintype β

Premises used: nonempty_fintype
-- 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 β
val : Fintype α
val_1 : Fintype β
⊢ 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))

Tactic:
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)
-- 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_1 : A.Definable L s
f : α → β
inst_1 : Finite α
inst_2 : Finite β
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))
⊢ ∀ (a : α), Definable.{u, v, w, u₁} A L (α := α) {x : α → M | x a = x (rangeSplitting f (rangeFactorization f a))}

Tactic:
fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext ?_⟩

Premises used: Set.ext, Set.Definable, FirstOrder.Language.Term.equal, FirstOrder.Language.Term.var, Exists.intro, Set.rangeSplitting, Set.rangeFactorization