case intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝ : Fintype α
⊢ Definable A L ((fun g => g ∘ f) '' s)
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Definable A L ((fun g => g ∘ f) '' s)
cases nonempty_fintype α
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
⊢ Definable A L ((fun g => g ∘ f) '' s)
case intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝ : Fintype α
⊢ Definable A L ((fun g => g ∘ f) '' s)
cases nonempty_fintype β
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
⊢ Definable A L ((fun g => g ∘ f) '' s)
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
⊢ Definable A L ((fun g => g ∘ f) '' s)
have h :=
  (((h.image_comp_equiv (Equiv.Set.sumCompl (range f))).image_comp_equiv
            (Equiv.sumCongr (_root_.Equiv.refl _)
              (Fintype.equivFin _).symm)).image_comp_sum_inl_fin
        _).preimage_comp
    (rangeSplitting f)
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ Definable A L ((fun g => g ∘ f) '' s)
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
⊢ Definable A L ((fun g => g ∘ f) '' s)
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_finset_biInter h' Finset.univ)
  simp
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ x ∈
      (fun g => g ∘ rangeSplitting f) ⁻¹'
          ((fun g => g ∘ Sum.inl) ''
            ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
              ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))) ∩
        {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))} ↔
    x ∈ (fun g => g ∘ f) '' s
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ Definable A L ((fun g => g ∘ f) '' s)
refine' (congr rfl (ext fun x => _)).mp (h.inter h')
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ ((∃ a,
        a ∈ s ∧
          ((a ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
                ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
              Sum.inl =
            x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))) ↔
    ∃ x_1, x_1 ∈ s ∧ x_1 ∘ f = x
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ x ∈
      (fun g => g ∘ rangeSplitting f) ⁻¹'
          ((fun g => g ∘ Sum.inl) ''
            ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
              ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))) ∩
        {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))} ↔
    x ∈ (fun g => g ∘ f) '' s
simp only [Equiv.coe_trans, mem_inter_iff, mem_preimage, mem_image, exists_exists_and_eq_and,
  mem_setOf_eq]
case intro.intro.mp
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ ((∃ a,
        a ∈ s ∧
          ((a ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
                ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
              Sum.inl =
            x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))) →
    ∃ x_1, x_1 ∈ s ∧ x_1 ∘ f = x

case intro.intro.mpr
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ (∃ x_1, x_1 ∈ s ∧ x_1 ∘ f = x) →
    (∃ a,
        a ∈ s ∧
          ((a ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
                ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
              Sum.inl =
            x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ ((∃ a,
        a ∈ s ∧
          ((a ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
                ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
              Sum.inl =
            x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))) ↔
    ∃ x_1, x_1 ∈ s ∧ x_1 ∘ f = x
constructor
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : ∀ (a : α), Definable A L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
⊢ Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
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
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : ∀ (a : α), Definable A L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ ∀ (x : α → M),
    (x ∈ ⋂ (i : α) (_ : i ∈ Finset.univ), {x | x i = x (rangeSplitting f (rangeFactorization f i))}) ↔
      x ∈ {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : ∀ (a : α), Definable A L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
refine' (congr rfl (ext _)).mp (definable_finset_biInter h' Finset.univ)
no goals
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : ∀ (a : α), Definable A L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ ∀ (x : α → M),
    (x ∈ ⋂ (i : α) (_ : i ∈ Finset.univ), {x | x i = x (rangeSplitting f (rangeFactorization f i))}) ↔
      x ∈ {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
simp
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
a : α
⊢ ∀ (x : α → M),
    x ∈ {x | x a = x (rangeSplitting f (rangeFactorization f a))} ↔
      x ∈ setOf (Formula.Realize (Term.equal (var a) (var (rangeSplitting f (rangeFactorization f a)))))
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
⊢ ∀ (a : α), Definable A L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
refine' fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext _⟩
no goals
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
a : α
⊢ ∀ (x : α → M),
    x ∈ {x | x a = x (rangeSplitting f (rangeFactorization f a))} ↔
      x ∈ setOf (Formula.Realize (Term.equal (var a) (var (rangeSplitting f (rangeFactorization f a)))))
simp
case intro.intro.mp.intro.intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (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 :
  ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
⊢ ∃ x_1, x_1 ∈ s ∧ x_1 ∘ f = x
case intro.intro.mp
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ ((∃ a,
        a ∈ s ∧
          ((a ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
                ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
              Sum.inl =
            x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))) →
    ∃ x_1, x_1 ∈ s ∧ x_1 ∘ f = x
rintro ⟨⟨y, ys, hy⟩, hx⟩
case intro.intro.mp.intro.intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (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 :
  ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
⊢ y ∘ f = x
case intro.intro.mp.intro.intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (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 :
  ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
⊢ ∃ x_1, x_1 ∈ s ∧ x_1 ∘ f = x
refine' ⟨y, ys, _⟩
case intro.intro.mp.intro.intro.intro.h
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (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 :
  ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
a : α
⊢ (y ∘ f) a = x a
case intro.intro.mp.intro.intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (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 :
  ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
⊢ y ∘ f = x
ext a
case intro.intro.mp.intro.intro.intro.h
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (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 :
  ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
a : α
⊢ (y ∘ f) a =
    (((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
          ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
        Sum.inl)
      (rangeFactorization f a)
case intro.intro.mp.intro.intro.intro.h
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (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 :
  ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
a : α
⊢ (y ∘ f) a = x a
rw [hx a, ← Function.comp_apply (f := x), ← hy]
no goals
case intro.intro.mp.intro.intro.intro.h
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (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 :
  ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
a : α
⊢ (y ∘ f) a =
    (((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
          ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
        Sum.inl)
      (rangeFactorization f a)
simp
case intro.intro.mpr.intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
⊢ (∃ a,
      a ∈ s ∧
        ((a ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
              ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
            Sum.inl =
          (y ∘ f) ∘ rangeSplitting f) ∧
    ∀ (a : α), (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
case intro.intro.mpr
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ (∃ x_1, x_1 ∈ s ∧ x_1 ∘ f = x) →
    (∃ a,
        a ∈ s ∧
          ((a ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
                ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
              Sum.inl =
            x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
rintro ⟨y, ys, rfl⟩
case intro.intro.mpr.intro.intro.refine'_1
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
⊢ ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
      Sum.inl =
    (y ∘ f) ∘ rangeSplitting f

case intro.intro.mpr.intro.intro.refine'_2
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (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))
case intro.intro.mpr.intro.intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
⊢ (∃ a,
      a ∈ s ∧
        ((a ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
              ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
            Sum.inl =
          (y ∘ f) ∘ rangeSplitting f) ∧
    ∀ (a : α), (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
refine' ⟨⟨y, ys, _⟩, fun a => _⟩
case intro.intro.mpr.intro.intro.refine'_1.h
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
x✝ : ↑(range f)
⊢ (((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
          ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
        Sum.inl)
      x✝ =
    ((y ∘ f) ∘ rangeSplitting f) x✝
case intro.intro.mpr.intro.intro.refine'_1
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
⊢ ((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
        ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
      Sum.inl =
    (y ∘ f) ∘ rangeSplitting f
ext
no goals
case intro.intro.mpr.intro.intro.refine'_1.h
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
x✝ : ↑(range f)
⊢ (((y ∘ ↑(Equiv.Set.sumCompl (range f))) ∘
          ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ∘
        Sum.inl)
      x✝ =
    ((y ∘ f) ∘ rangeSplitting f) x✝
simp [Set.apply_rangeSplitting f]
no goals
case intro.intro.mpr.intro.intro.refine'_2
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h✝ : Definable A L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  Definable A L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ↑(Equiv.sumCongr (Equiv.refl ↑(range f)) (Fintype.equivFin ↑(range fᶜ)).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range f))) '' s))))
h' : Definable A L {x | ∀ (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))
rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f,
  rangeFactorization_coe]