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₁
β : 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))
refine :
  ∀ (a : α) (x : α → M),
    Membership.mem (γ := Set (α → M)) {x : α → M | x a = x (rangeSplitting f (rangeFactorization f a))} x ↔
      Membership.mem (γ := Set (α → M))
        (setOf
          (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w))
            (Term.equal (var a) (var (rangeSplitting f (rangeFactorization f a))))))
        x
⊢ ∀ (a : α), Definable.{u, v, w, u₁} A L (α := α) {x : α → M | x a = x (rangeSplitting f (rangeFactorization f a))}

Tactic:
refine fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext ?_⟩
-- 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 : α
⊢ ∀ (x : α → M),
    Membership.mem (γ := Set (α → M)) {x : α → M | x a = x (rangeSplitting f (rangeFactorization f a))} x ↔
      Membership.mem (γ := Set (α → M))
        (setOf
          (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w))
            (Term.equal (var a) (var (rangeSplitting f (rangeFactorization f a))))))
        x

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_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:
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
-- 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))
h' : ∀ (a : α), Definable.{u, v, w, u₁} A L (α := α) {x : α → M | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}

Tactic:
(congr rfl (ext ?_)).mp (definable_biInter_finset h' Finset.univ)

Premises used: Set.ext, Finset.univ, Eq.mp, Set.definable_biInter_finset, congr, rfl
-- 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))
h' : ∀ (a : α), Definable.{u, v, w, u₁} A L (α := α) {x : α → M | x a = x (rangeSplitting f (rangeFactorization f a))}
refine :
  ∀ (x : α → M),
    Membership.mem (γ := Set (α → M))
        (⋂ (i : α),
          ⋂ (_ : Membership.mem (γ := Finset α) Finset.univ i),
            {x : α → M | x i = x (rangeSplitting f (rangeFactorization f i))})
        x ↔
      Membership.mem (γ := Set (α → M)) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))} x
⊢ Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}

Tactic:
refine (congr rfl (ext ?_)).mp (definable_biInter_finset h' Finset.univ)

Premises used: Set.ext, Finset.univ, Eq.mp, Set.definable_biInter_finset, congr, rfl
-- 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))
h' : ∀ (a : α), Definable.{u, v, w, u₁} A L (α := α) {x : α → M | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ ∀ (x : α → M),
    Membership.mem (γ := Set (α → M))
        (⋂ (i : α),
          ⋂ (_ : Membership.mem (γ := Finset α) Finset.univ i),
            {x : α → M | x i = x (rangeSplitting f (rangeFactorization f i))})
        x ↔
      Membership.mem (γ := Set (α → M)) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))} x

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

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

Tactic:
(congr rfl (ext fun x => ?_)).mp (h.inter h')

Premises used: Set.ext, Set.Definable.inter, Eq.mp, congr, rfl
-- 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))
h' : Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
intro :
  ∀ (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
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)

Tactic:
refine (congr rfl (ext fun x => ?_)).mp (h.inter h')

Premises used: Set.ext, Set.Definable.inter, Eq.mp, congr, rfl
-- 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))
h' : Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (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 :
  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))
        (y ∘ (⇑(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
⊢ ∃ x_1 ∈ s, x_1 ∘ f = x

Tactic:
⟨y, ys, ?_⟩

Premises used: And.intro, Exists.intro
-- 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))
h' : Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (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 :
  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))
        (y ∘ (⇑(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
intro : y ∘ f = x
⊢ ∃ x_1 ∈ s, x_1 ∘ f = x

Tactic:
refine ⟨y, ys, ?_⟩
-- 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))
h' : Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (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 :
  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))
        (y ∘ (⇑(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
intro : ∀ (a : α), (y ∘ f) a = x a
⊢ y ∘ f = x

Tactic:
ext a
-- 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))
h' : Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (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 :
  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))
        (y ∘ (⇑(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 : α
intro :
  (y ∘ f) a =
    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))
        (y ∘ (⇑(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 (rangeFactorization f a)
⊢ (y ∘ f) a = x a

Tactic:
rw [hx a, ← Function.comp_apply (f := x), ← hy]

Premises used: Function.comp_apply