awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ 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
have 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)
Tactic: simp only [Set.mem_image, mem_setOf_eq, BoundedFormula.realize_exs,
    BoundedFormula.realize_relabel, Function.comp_id, Fin.castAdd_zero, Fin.cast_refl]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ (∃ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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)
⊢ (∃ (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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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 β
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)
have intro : ∀ (val : Fintype β), Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)
Tactic: cases nonempty_fintype β
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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)
have 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 : α) → β) sorry).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: 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
          _)
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ 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
have 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 : α) → β) sorry).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: simp only [mem_image, exists_exists_and_eq_and]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
have 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 : α) → β) sorry).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: refine exists_congr fun y => and_congr_right fun _ => Eq.congr_left (funext fun a => ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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 β
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)
have intro : ∀ (val : Fintype β), Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)
Tactic: 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_sumInl_fin
          _)
    simp only [mem_image, exists_exists_and_eq_and]
    refine exists_congr fun y => and_congr_right fun _ => Eq.congr_left (funext fun a => ?_)
    simp
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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)
have intro₁ : ∀ (val : Fintype β) (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 : α) → β) sorry).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: 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_sumInl_fin
          _)
    simp only [mem_image, exists_exists_and_eq_and]
    refine exists_congr fun y => and_congr_right fun _ => Eq.congr_left (funext fun a => ?_)
    simp
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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 β
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
have intro : ∀ (val : Fintype α), Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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 α
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
have intro : ∀ (val : Fintype β), Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
Tactic: cases nonempty_fintype β
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (hypothesis)
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 (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
have 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))
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)
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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))}
have 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
Tactic: refine fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (hypothesis)
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))}
have h' : ∀ (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
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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))}
have 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
Tactic: refine (congr rfl (ext ?_)).mp (definable_biInter_finset h' Finset.univ)
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (hypothesis)
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 (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
have h' : 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
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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)
have 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
Tactic: refine (congr rfl (ext fun x => ?_)).mp (h.inter h')