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₁
β : 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
⊢ 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
have intro : ((∃ 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
Tactic: simp only [mem_inter_iff, mem_preimage, mem_image, exists_exists_and_eq_and,
      mem_setOf_eq]
-- 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))}
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
have intro : ((∃ 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
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_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
have intro : y ∘ f = x
Tactic: refine ⟨y, ys, ?_⟩
-- 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))}
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
⊢ y ∘ f = x
have intro : ∀ (a : α), (y ∘ f) a = x a
Tactic: ext 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_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 : α
⊢ (y ∘ f) a = x a
have 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)
Tactic: rw [hx a, ← Function.comp_apply (f := x), ← hy]
-- 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))}
y : β → M
ys : y ∈ s
⊢ (∃ 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 =
        (y ∘ f) ∘ rangeSplitting f) ∧
    ∀ (a : α), (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
have intro : 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 =
  (y ∘ f) ∘ rangeSplitting f
Tactic: refine ⟨⟨y, ys, ?_⟩, 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_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))}
y : β → M
ys : y ∈ s
intro :
  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 =
    (y ∘ f) ∘ rangeSplitting f
⊢ (∃ 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 =
        (y ∘ f) ∘ rangeSplitting f) ∧
    ∀ (a : α), (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
have intro₁ : ∀ (a : α), (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
Tactic: refine ⟨⟨y, ys, ?_⟩, 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_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))}
y : β → M
ys : y ∈ 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))
        (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 =
    (y ∘ f) ∘ rangeSplitting f
have intro : ∀ (x : (↑(range f) : Type u_1)),
  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 =
    ((y ∘ f) ∘ rangeSplitting f) x
Tactic: ext
-- 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))}
y : β → M
ys : y ∈ s
a : α
⊢ (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
have intro : y (f a) = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
Tactic: rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f,
          rangeFactorization_coe]
-- 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))}
y : β → M
ys : y ∈ s
a : α
intro : y (f a) = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
⊢ (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
have intro₁ : y (f a) = y (f (rangeSplitting f (rangeFactorization f a)))
Tactic: rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f,
          rangeFactorization_coe]