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))}
y : β → M
ys : y ∈ s
a : α
intro : y (f a) = (y ∘ f) (rangeSplitting f (rangeFactorization f 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 (↑(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))
intro₁ : y (f a) = y (f (rangeSplitting f (rangeFactorization f a)))
intro₂ : y (f a) = y (↑(rangeFactorization f a) : β)
⊢ (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
have intro₃ : y (f a) = y (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 : 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: classical
    cases nonempty_fintype α
    cases nonempty_fintype β
    have h :=
      (((h.image_comp_equiv (Equiv.Set.sumCompl (range f))).image_comp_equiv
                (Equiv.sumCongr (_root_.Equiv.refl _)
                  (Fintype.equivFin _).symm)).image_comp_sumInl_fin
            _).preimage_comp
        (rangeSplitting f)
    have h' :
      A.Definable L { x : α → M | ∀ a, x a = x (rangeSplitting f (rangeFactorization f a)) } := by
      have h' : ∀ a,
        A.Definable L { x : α → M | x a = x (rangeSplitting f (rangeFactorization f a)) } := by
          refine fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext ?_⟩
          simp
      refine (congr rfl (ext ?_)).mp (definable_biInter_finset h' Finset.univ)
      simp
    refine (congr rfl (ext fun x => ?_)).mp (h.inter h')
    simp only [mem_inter_iff, mem_preimage, mem_image, exists_exists_and_eq_and,
      mem_setOf_eq]
    constructor
    · rintro ⟨⟨y, ys, hy⟩, hx⟩
      refine ⟨y, ys, ?_⟩
      ext a
      rw [hx a, ← Function.comp_apply (f := x), ← hy]
      simp
    · rintro ⟨y, ys, rfl⟩
      refine ⟨⟨y, ys, ?_⟩, fun a => ?_⟩
      · ext
        simp [Set.apply_rangeSplitting f]
      · rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f,
          rangeFactorization_coe]
-- 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 β
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)
have intro₁ : ∀ (val : Fintype α) (val : Fintype β), Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
Tactic: classical
    cases nonempty_fintype α
    cases nonempty_fintype β
    have h :=
      (((h.image_comp_equiv (Equiv.Set.sumCompl (range f))).image_comp_equiv
                (Equiv.sumCongr (_root_.Equiv.refl _)
                  (Fintype.equivFin _).symm)).image_comp_sumInl_fin
            _).preimage_comp
        (rangeSplitting f)
    have h' :
      A.Definable L { x : α → M | ∀ a, x a = x (rangeSplitting f (rangeFactorization f a)) } := by
      have h' : ∀ a,
        A.Definable L { x : α → M | x a = x (rangeSplitting f (rangeFactorization f a)) } := by
          refine fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext ?_⟩
          simp
      refine (congr rfl (ext ?_)).mp (definable_biInter_finset h' Finset.univ)
      simp
    refine (congr rfl (ext fun x => ?_)).mp (h.inter h')
    simp only [mem_inter_iff, mem_preimage, mem_image, exists_exists_and_eq_and,
      mem_setOf_eq]
    constructor
    · rintro ⟨⟨y, ys, hy⟩, hx⟩
      refine ⟨y, ys, ?_⟩
      ext a
      rw [hx a, ← Function.comp_apply (f := x), ← hy]
      simp
    · rintro ⟨y, ys, rfl⟩
      refine ⟨⟨y, ys, ?_⟩, fun a => ?_⟩
      · ext
        simp [Set.apply_rangeSplitting f]
      · rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f,
          rangeFactorization_coe]
-- 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 β
intro : ∀ (val : Fintype α), Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
intro₁ : ∀ (val : Fintype α) (val : Fintype β), Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
have intro₂ : ∀ (val : Fintype α) (val_1 : Fintype β)
  (h :
    Definable.{u, v, w, u₁} A L (α := α)
      (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
        ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
          (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
              g ∘
                (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                      (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                  (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                    (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
            (fun (g : β → M) ↦
                g ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
              s))),
  Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
Tactic: classical
    cases nonempty_fintype α
    cases nonempty_fintype β
    have h :=
      (((h.image_comp_equiv (Equiv.Set.sumCompl (range f))).image_comp_equiv
                (Equiv.sumCongr (_root_.Equiv.refl _)
                  (Fintype.equivFin _).symm)).image_comp_sumInl_fin
            _).preimage_comp
        (rangeSplitting f)
    have h' :
      A.Definable L { x : α → M | ∀ a, x a = x (rangeSplitting f (rangeFactorization f a)) } := by
      have h' : ∀ a,
        A.Definable L { x : α → M | x a = x (rangeSplitting f (rangeFactorization f a)) } := by
          refine fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext ?_⟩
          simp
      refine (congr rfl (ext ?_)).mp (definable_biInter_finset h' Finset.univ)
      simp
    refine (congr rfl (ext fun x => ?_)).mp (h.inter h')
    simp only [mem_inter_iff, mem_preimage, mem_image, exists_exists_and_eq_and,
      mem_setOf_eq]
    constructor
    · rintro ⟨⟨y, ys, hy⟩, hx⟩
      refine ⟨y, ys, ?_⟩
      ext a
      rw [hx a, ← Function.comp_apply (f := x), ← hy]
      simp
    · rintro ⟨y, ys, rfl⟩
      refine ⟨⟨y, ys, ?_⟩, fun a => ?_⟩
      · ext
        simp [Set.apply_rangeSplitting f]
      · rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f,
          rangeFactorization_coe]
-- 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
inst_1 : Finite β
S : Set (α ⊕ β → M)
hS : A.Definable L S
⊢ Definable.{u, v, w, u₁} A L (α := α) {v : α → M | ∃ (u : β → M), Sum.elim v u ∈ S}
have obtain : ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ β)) (hφ : S = setOf φ.Realize),
  Definable.{u, v, w, u₁} A L (α := α) {v : α → M | ∃ (u : β → M), Sum.elim v u ∈ S}
Tactic: obtain ⟨φ, hφ⟩ := hS
Cleared hypotheses: hS
-- 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
inst_1 : Finite β
S : Set (α ⊕ β → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ β)
hφ : S = setOf φ.Realize
⊢ Definable.{u, v, w, u₁} A L (α := α) {v : α → M | ∃ (u : β → M), Sum.elim v u ∈ S}
have exists : Eq (α := Set (α → M)) {v : α → M | ∃ (u : β → M), Sum.elim v u ∈ S} (setOf (Formula.iExs β φ).Realize)
Tactic: exists φ.iExs β
-- 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
inst_1 : Finite β
S : Set (α ⊕ β → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ β)
hφ : S = setOf φ.Realize
⊢ Eq (α := Set (α → M)) {v : α → M | ∃ (u : β → M), Sum.elim v u ∈ S} (setOf (Formula.iExs β φ).Realize)
have h : ∀ (v : α → M),
  Membership.mem (γ := Set (α → M)) {v : α → M | ∃ (u : β → M), Sum.elim v u ∈ S} v ↔
    Membership.mem (γ := Set (α → M)) (setOf (Formula.iExs β φ).Realize) v
Tactic: ext v
-- 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
inst_1 : Finite β
S : Set (α ⊕ β → M)
hS : A.Definable L S
⊢ Definable.{u, v, w, u₁} A L (α := α) {v : α → M | ∀ (u : β → M), Sum.elim v u ∈ S}
have obtain : ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ β)) (hφ : S = setOf φ.Realize),
  Definable.{u, v, w, u₁} A L (α := α) {v : α → M | ∀ (u : β → M), Sum.elim v u ∈ S}
Tactic: obtain ⟨φ, hφ⟩ := hS
Cleared hypotheses: hS
-- 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
inst_1 : Finite β
S : Set (α ⊕ β → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ β)
hφ : S = setOf φ.Realize
⊢ Definable.{u, v, w, u₁} A L (α := α) {v : α → M | ∀ (u : β → M), Sum.elim v u ∈ S}
have exists : Eq (α := Set (α → M)) {v : α → M | ∀ (u : β → M), Sum.elim v u ∈ S} (setOf (Formula.iAlls β φ).Realize)
Tactic: exists φ.iAlls β
-- 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
inst_1 : Finite β
S : Set (α ⊕ β → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ β)
hφ : S = setOf φ.Realize
⊢ Eq (α := Set (α → M)) {v : α → M | ∀ (u : β → M), Sum.elim v u ∈ S} (setOf (Formula.iAlls β φ).Realize)
have h : ∀ (v : α → M),
  Membership.mem (γ := Set (α → M)) {v : α → M | ∀ (u : β → M), Sum.elim v u ∈ S} v ↔
    Membership.mem (γ := Set (α → M)) (setOf (Formula.iAlls β φ).Realize) v
Tactic: ext v
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
L : Language
inst : L.Structure M
a : M
⊢ Definable₁ (M := M) {a} L {a}
have exists : Eq.{w + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | Membership.mem (γ := Set M) {a} (x 0)}
  (setOf
    (Formula.Realize
      (Term.equal (var 0) (L.con (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) {a} x) a sorry)).term)))
Tactic: exists (Term.var 0).equal (L.con (⟨a, rfl⟩ : ↑({a} : Set M))).term
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
L : Language
inst : L.Structure M
A : Set M
⊢ A.Definable₂ L (Set.diagonal M)
have exists : Eq.{w + 1} (α := Set (Fin 2 → M)) {x : Fin 2 → M | (x 0, x 1) ∈ Set.diagonal M}
  (setOf (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w)) (Term.equal (var 0) (var 1))))
Tactic: exists (Term.var 0).equal (Term.var 1)
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
t : L.Term α
⊢ DefinableFun.{u_1, u_2, u_4, u_5} (M := M) L (α := α) ∅ fun (v : α → M) ↦ Term.realize v t
have rw : ∃ (φ : Formula.{u_4, u_5, u_2} L (Option α)),
  Eq (α := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ Term.realize v t) (setOf φ.Realize)
Tactic: rw [empty_definableFun_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
t : L.Term α
⊢ ∃ (φ : Formula.{u_4, u_5, u_2} L (Option α)),
    Eq (α := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ Term.realize v t) (setOf φ.Realize)
have refine : Eq (α := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ Term.realize v t)
  (setOf ((Term.relabel some t).equal (var none)).Realize)
Tactic: refine ⟨(t.relabel some).equal (Term.var none), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
t : L.Term α
⊢ Eq (α := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ Term.realize v t)
    (setOf ((Term.relabel some t).equal (var none)).Realize)
have h : ∀ (v : Option α → M),
  Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ Term.realize v t) v ↔
    Membership.mem (γ := Set (Option α → M)) (setOf ((Term.relabel some t).equal (var none)).Realize) v
Tactic: ext v
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
a : M
γ : Type u_4
ha : a ∈ A
⊢ DefinableFun.{u_1, u_4, u_5, u_6} L (α := γ) A fun (x : γ → M) ↦ a
have rw : DefinableFun (M := M) (withConstants.{u_5, u_6, u_1} L (↑A : Type u_1)) (α := γ) ∅ fun (x : γ → M) ↦ a
Tactic: rw [definableFun_iff_empty_definableFun_with_params]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
⊢ A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
have rw : A.Definable L (α := α ⊕ β) (⋂ (i : β), {x : α ⊕ β → M | F (x ∘ Sum.inl) i = x (Sum.inr i)})
Tactic: rw [setOf_forall]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
⊢ A.Definable L (α := α ⊕ β) (⋂ (i : β), {x : α ⊕ β → M | F (x ∘ Sum.inl) i = x (Sum.inr i)})
have refine : ∀ (i : β), A.Definable L (α := α ⊕ β) {x : α ⊕ β → M | F (x ∘ Sum.inl) i = x (Sum.inr i)}
Tactic: refine definable_iInter_of_finite fun i => ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (hypothesis)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
⊢ A.Definable L (F ⁻¹' S)
have h_graph : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
Tactic: have h_graph : A.Definable L { w : α ⊕ β → M | ∀ i, F (w ∘ Sum.inl) i = w (Sum.inr i) } := by
    rw [setOf_forall]
    refine definable_iInter_of_finite fun i => ?_
    simpa [tupleGraph] using
      (hF i).preimage_comp (fun | none => Sum.inr i | some j => Sum.inl j)
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (hypothesis)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
h_graph : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
⊢ A.Definable L (F ⁻¹' S)
have h_cyl : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | w ∘ Sum.inr ∈ S}
Tactic: have h_cyl : A.Definable L { w : α ⊕ β → M | w ∘ Sum.inr ∈ S } :=
    hS.preimage_comp Sum.inr
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
h_graph : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
h_cyl : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | w ∘ Sum.inr ∈ S}
⊢ A.Definable L (F ⁻¹' S)
have h : F ⁻¹' S =
  {v : α → M |
    ∃ (u : β → M),
      Membership.mem (γ := Set (α ⊕ β → M))
        ({w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)} ∩ {w : α ⊕ β → M | w ∘ Sum.inr ∈ S})
        (Sum.elim v u)}
Tactic: convert! Definable.exists_of_finite (Definable.inter h_graph h_cyl) using 1
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
h_graph : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
h_cyl : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | w ∘ Sum.inr ∈ S}
⊢ F ⁻¹' S =
    {v : α → M |
      ∃ (u : β → M),
        Membership.mem (γ := Set (α ⊕ β → M))
          ({w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)} ∩ {w : α ⊕ β → M | w ∘ Sum.inr ∈ S})
          (Sum.elim v u)}
have h : ∀ (v : α → M),
  v ∈ F ⁻¹' S ↔
    Membership.mem (γ := Set (α → M))
      {v : α → M |
        ∃ (u : β → M),
          Membership.mem (γ := Set (α ⊕ β → M))
            ({w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)} ∩ {w : α ⊕ β → M | w ∘ Sum.inr ∈ S})
            (Sum.elim v u)}
      v
Tactic: ext v
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
β : Type u_3
A : Set M
f : (α → M) → M
inst_1 : Finite α
g : (β → M) → α → M
hg : DefinableMap L A g
hf : DefinableFun L A f
G : (Option β → M) → Option α → M :=
  fun (w : Option β → M) (j : Option α) ↦
    match (motive := Option α → M) j with
    | none => w none
    | some i => g (w ∘ some) i
i : Option α
⊢ DefinableFun.{u_1, u_3, u_4, u_5} L (α := Option β) A fun (x : Option β → M) ↦ G x i
have none : DefinableFun.{u_1, u_3, u_4, u_5} L (α := Option β) A fun (x : Option β → M) ↦ G x none
Tactic: cases i with
    | none => fun_prop
    | some j =>
      simpa [tupleGraph] using
        ((hg j).preimage_comp fun | none => none | some i => some (some i))
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
β : Type u_3
A : Set M
f : (α → M) → M
inst_1 : Finite α
g : (β → M) → α → M
hg : DefinableMap L A g
hf : DefinableFun L A f
G : (Option β → M) → Option α → M :=
  fun (w : Option β → M) (j : Option α) ↦
    match (motive := Option α → M) j with
    | Option.none => w Option.none
    | some i => g (w ∘ some) i
i : Option α
none : DefinableFun.{u_1, u_3, u_4, u_5} L (α := Option β) A fun (x : Option β → M) ↦ G x Option.none
⊢ DefinableFun.{u_1, u_3, u_4, u_5} L (α := Option β) A fun (x : Option β → M) ↦ G x i
have some : ∀ (j : α), DefinableFun.{u_1, u_3, u_4, u_5} L (α := Option β) A fun (x : Option β → M) ↦ G x (some j)
Tactic: cases i with
    | none => fun_prop
    | some j =>
      simpa [tupleGraph] using
        ((hg j).preimage_comp fun | none => none | some i => some (some i))
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (hypothesis)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
β : Type u_3
A : Set M
f : (α → M) → M
inst_1 : Finite α
g : (β → M) → α → M
hg : DefinableMap L A g
hf : DefinableFun L A f
G : (Option β → M) → Option α → M :=
  fun (w : Option β → M) (j : Option α) ↦
    match (motive := Option α → M) j with
    | none => w none
    | some i => g (w ∘ some) i
⊢ DefinableFun.{u_1, u_3, u_4, u_5} L (α := β) A fun (v : β → M) ↦ f (g v)
have hG : DefinableMap L A G
Tactic: have hG : A.DefinableMap L G := by
    intro i
    cases i with
    | none => fun_prop
    | some j =>
      simpa [tupleGraph] using
        ((hg j).preimage_comp fun | none => none | some i => some (some i))
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (hypothesis)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst_1 : DecidablePred p
hp : A.Definable L (setOf p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w : Option α → M | p (w ∘ some)}
⊢ DefinableFun.{u_1, u_2, u_4, u_5} L (α := α) A fun (v : α → M) ↦ if p v then f v else g v
have hP : A.Definable L P
Tactic: have hP : A.Definable L P := hp.preimage_comp some
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst_1 : DecidablePred p
hp : A.Definable L (setOf p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w : Option α → M | p (w ∘ some)}
hP : A.Definable L P
⊢ Definable.{u_4, u_5, u_1, u_2} A L (α := Option α) (tupleGraph fun (v : α → M) ↦ if p v then f v else g v)
have h : (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) = P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g
Tactic: convert! (hP.inter hf).union (hP.compl.inter hg)
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst_1 : DecidablePred p
hp : A.Definable L (setOf p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w : Option α → M | p (w ∘ some)}
hP : A.Definable L P
⊢ (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) = P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g
have h : ∀ (w : Option α → M),
  Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) w ↔
    w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g
Tactic: ext w