[GOAL]
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
L' : Language
inst✝¹ : Structure L' M
h : Definable A L s
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
⊢ Definable A L' s
[PROOFSTEP]
obtain ⟨ψ, rfl⟩ := h
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
ψ : Formula (L[[↑A]]) α
⊢ Definable A L' (setOf (Formula.Realize ψ))
[PROOFSTEP]
refine' ⟨(φ.addConstants A).onFormula ψ, _⟩
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
ψ : Formula (L[[↑A]]) α
⊢ setOf (Formula.Realize ψ) = setOf (Formula.Realize (LHom.onFormula (LHom.addConstants (↑A) φ) ψ))
[PROOFSTEP]
ext x
[GOAL]
case intro.h
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type u_1
B : Set M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
ψ : Formula (L[[↑A]]) α
x : α → M
⊢ x ∈ setOf (Formula.Realize ψ) ↔ x ∈ setOf (Formula.Realize (LHom.onFormula (LHom.addConstants (↑A) φ) ψ))
[PROOFSTEP]
simp only [mem_setOf_eq, LHom.realize_onFormula]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
⊢ Definable ∅ L s ↔ ∃ φ, s = setOf (Formula.Realize φ)
[PROOFSTEP]
rw [Definable, Equiv.exists_congr_left (LEquiv.addEmptyConstants L (∅ : Set M)).onFormula]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
⊢ (∃ φ, s = setOf (Formula.Realize φ)) ↔
    ∃ b, s = setOf (Formula.Realize (↑(LEquiv.onFormula (LEquiv.addEmptyConstants L ↑∅)).symm b))
[PROOFSTEP]
simp [-constantsOn]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
hAs : Definable A L s
hAB : A ⊆ B
⊢ Definable B L s
[PROOFSTEP]
rw [definable_iff_empty_definable_with_params] at *
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
hAs : Definable ∅ (L[[↑A]]) s
hAB : A ⊆ B
⊢ Definable ∅ (L[[↑B]]) s
[PROOFSTEP]
exact hAs.map_expansion (L.lhomWithConstantsMap (Set.inclusion hAB))
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
⊢ ∅ = setOf (Formula.Realize ⊥)
[PROOFSTEP]
ext
[GOAL]
case h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
x✝ : α → M
⊢ x✝ ∈ ∅ ↔ x✝ ∈ setOf (Formula.Realize ⊥)
[PROOFSTEP]
simp
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
⊢ univ = setOf (Formula.Realize ⊤)
[PROOFSTEP]
ext
[GOAL]
case h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
x✝ : α → M
⊢ x✝ ∈ univ ↔ x✝ ∈ setOf (Formula.Realize ⊤)
[PROOFSTEP]
simp
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s f g : Set (α → M)
hf : Definable A L f
hg : Definable A L g
⊢ Definable A L (f ∩ g)
[PROOFSTEP]
rcases hf with ⟨φ, rfl⟩
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s g : Set (α → M)
hg : Definable A L g
φ : Formula (L[[↑A]]) α
⊢ Definable A L (setOf (Formula.Realize φ) ∩ g)
[PROOFSTEP]
rcases hg with ⟨θ, rfl⟩
[GOAL]
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)
φ θ : Formula (L[[↑A]]) α
⊢ Definable A L (setOf (Formula.Realize φ) ∩ setOf (Formula.Realize θ))
[PROOFSTEP]
refine' ⟨φ ⊓ θ, _⟩
[GOAL]
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)
φ θ : Formula (L[[↑A]]) α
⊢ setOf (Formula.Realize φ) ∩ setOf (Formula.Realize θ) = setOf (Formula.Realize (φ ⊓ θ))
[PROOFSTEP]
ext
[GOAL]
case 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)
φ θ : Formula (L[[↑A]]) α
x✝ : α → M
⊢ x✝ ∈ setOf (Formula.Realize φ) ∩ setOf (Formula.Realize θ) ↔ x✝ ∈ setOf (Formula.Realize (φ ⊓ θ))
[PROOFSTEP]
simp
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s f g : Set (α → M)
hf : Definable A L f
hg : Definable A L g
⊢ Definable A L (f ∪ g)
[PROOFSTEP]
rcases hf with ⟨φ, hφ⟩
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s f g : Set (α → M)
hg : Definable A L g
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
⊢ Definable A L (f ∪ g)
[PROOFSTEP]
rcases hg with ⟨θ, hθ⟩
[GOAL]
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s f g : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
θ : Formula (L[[↑A]]) α
hθ : g = setOf (Formula.Realize θ)
⊢ Definable A L (f ∪ g)
[PROOFSTEP]
refine' ⟨φ ⊔ θ, _⟩
[GOAL]
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s f g : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
θ : Formula (L[[↑A]]) α
hθ : g = setOf (Formula.Realize θ)
⊢ f ∪ g = setOf (Formula.Realize (φ ⊔ θ))
[PROOFSTEP]
ext
[GOAL]
case intro.intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s f g : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : f = setOf (Formula.Realize φ)
θ : Formula (L[[↑A]]) α
hθ : g = setOf (Formula.Realize θ)
x✝ : α → M
⊢ x✝ ∈ f ∪ g ↔ x✝ ∈ setOf (Formula.Realize (φ ⊔ θ))
[PROOFSTEP]
rw [hφ, hθ, mem_setOf_eq, Formula.realize_sup, mem_union, mem_setOf_eq, mem_setOf_eq]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (Finset.inf s f)
[PROOFSTEP]
classical
refine' Finset.induction definable_univ (fun i s _ h => _) s
rw [Finset.inf_insert]
exact (hf i).inter h
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (Finset.inf s f)
[PROOFSTEP]
refine' Finset.induction definable_univ (fun i s _ h => _) s
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝¹ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : Definable A L (Finset.inf s f)
⊢ Definable A L (Finset.inf (insert i s) f)
[PROOFSTEP]
rw [Finset.inf_insert]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝¹ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : Definable A L (Finset.inf s f)
⊢ Definable A L (f i ⊓ Finset.inf s f)
[PROOFSTEP]
exact (hf i).inter h
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (Finset.sup s f)
[PROOFSTEP]
classical
refine' Finset.induction definable_empty (fun i s _ h => _) s
rw [Finset.sup_insert]
exact (hf i).union h
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (Finset.sup s f)
[PROOFSTEP]
refine' Finset.induction definable_empty (fun i s _ h => _) s
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝¹ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : Definable A L (Finset.sup s f)
⊢ Definable A L (Finset.sup (insert i s) f)
[PROOFSTEP]
rw [Finset.sup_insert]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝¹ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : Definable A L (Finset.sup s f)
⊢ Definable A L (f i ⊔ Finset.sup s f)
[PROOFSTEP]
exact (hf i).union h
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (⋂ (i : ι) (_ : i ∈ s), f i)
[PROOFSTEP]
rw [← Finset.inf_set_eq_iInter]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (Finset.inf s fun i => f i)
[PROOFSTEP]
exact definable_finset_inf hf s
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (⋃ (i : ι) (_ : i ∈ s), f i)
[PROOFSTEP]
rw [← Finset.sup_set_eq_biUnion]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (Finset.sup s fun i => f i)
[PROOFSTEP]
exact definable_finset_sup hf s
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ s : Set (α → M)
hf : Definable A L s
⊢ Definable A L sᶜ
[PROOFSTEP]
rcases hf with ⟨φ, hφ⟩
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ s : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : s = setOf (Formula.Realize φ)
⊢ Definable A L sᶜ
[PROOFSTEP]
refine' ⟨φ.not, _⟩
[GOAL]
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ s : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : s = setOf (Formula.Realize φ)
⊢ sᶜ = setOf (Formula.Realize (Formula.not φ))
[PROOFSTEP]
ext v
[GOAL]
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ s : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : s = setOf (Formula.Realize φ)
v : α → M
⊢ v ∈ sᶜ ↔ v ∈ setOf (Formula.Realize (Formula.not φ))
[PROOFSTEP]
rw [hφ, compl_setOf, mem_setOf, mem_setOf, Formula.realize_not]
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
f : α → β
s : Set (α → M)
h : Definable A L s
⊢ Definable A L ((fun g => g ∘ f) ⁻¹' s)
[PROOFSTEP]
obtain ⟨φ, rfl⟩ := h
[GOAL]
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)
f : α → β
φ : Formula (L[[↑A]]) α
⊢ Definable A L ((fun g => g ∘ f) ⁻¹' setOf (Formula.Realize φ))
[PROOFSTEP]
refine' ⟨φ.relabel f, _⟩
[GOAL]
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)
f : α → β
φ : Formula (L[[↑A]]) α
⊢ (fun g => g ∘ f) ⁻¹' setOf (Formula.Realize φ) = setOf (Formula.Realize (Formula.relabel f φ))
[PROOFSTEP]
ext
[GOAL]
case 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)
f : α → β
φ : Formula (L[[↑A]]) α
x✝ : β → M
⊢ x✝ ∈ (fun g => g ∘ f) ⁻¹' setOf (Formula.Realize φ) ↔ x✝ ∈ setOf (Formula.Realize (Formula.relabel f φ))
[PROOFSTEP]
simp only [Set.preimage_setOf_eq, mem_setOf_eq, Formula.realize_relabel]
[GOAL]
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 : α ≃ β
⊢ Definable A L ((fun g => g ∘ ↑f) '' s)
[PROOFSTEP]
refine' (congr rfl _).mp (h.preimage_comp f.symm)
[GOAL]
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 : α ≃ β
⊢ (fun g => g ∘ ↑f.symm) ⁻¹' s = (fun g => g ∘ ↑f) '' s
[PROOFSTEP]
rw [image_eq_preimage_of_inverse]
[GOAL]
case 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 : α ≃ β
⊢ Function.LeftInverse (fun g => g ∘ ↑f.symm) fun g => g ∘ ↑f
[PROOFSTEP]
intro i
[GOAL]
case 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 : α ≃ β
i : β → M
⊢ (fun g => g ∘ ↑f.symm) ((fun g => g ∘ ↑f) i) = i
[PROOFSTEP]
ext b
[GOAL]
case h₁.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 : α ≃ β
i : β → M
b : β
⊢ (fun g => g ∘ ↑f.symm) ((fun g => g ∘ ↑f) i) b = i b
[PROOFSTEP]
simp only [Function.comp_apply, Equiv.apply_symm_apply]
[GOAL]
case 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 : α ≃ β
⊢ Function.RightInverse (fun g => g ∘ ↑f.symm) fun g => g ∘ ↑f
[PROOFSTEP]
intro i
[GOAL]
case 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 : α ≃ β
i : α → M
⊢ (fun g => g ∘ ↑f) ((fun g => g ∘ ↑f.symm) i) = i
[PROOFSTEP]
ext a
[GOAL]
case h₂.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 : α ≃ β
i : α → M
a : α
⊢ (fun g => g ∘ ↑f) ((fun g => g ∘ ↑f.symm) i) a = i a
[PROOFSTEP]
simp
[GOAL]
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
m : ℕ
s : Set (α ⊕ Fin m → M)
h : Definable A L s
⊢ Definable A L ((fun g => g ∘ Sum.inl) '' s)
[PROOFSTEP]
obtain ⟨φ, rfl⟩ := h
[GOAL]
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)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
⊢ Definable A L ((fun g => g ∘ Sum.inl) '' setOf (Formula.Realize φ))
[PROOFSTEP]
refine' ⟨(BoundedFormula.relabel id φ).exs, _⟩
[GOAL]
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)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
⊢ (fun g => g ∘ Sum.inl) '' setOf (Formula.Realize φ) =
    setOf (Formula.Realize (BoundedFormula.exs (BoundedFormula.relabel id φ)))
[PROOFSTEP]
ext x
[GOAL]
case 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)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
x : α → M
⊢ x ∈ (fun g => g ∘ Sum.inl) '' setOf (Formula.Realize φ) ↔
    x ∈ setOf (Formula.Realize (BoundedFormula.exs (BoundedFormula.relabel id φ)))
[PROOFSTEP]
simp only [Set.mem_image, mem_setOf_eq, BoundedFormula.realize_exs, BoundedFormula.realize_relabel,
  Function.comp.right_id, Fin.castAdd_zero, Fin.castIso_refl]
[GOAL]
case 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)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
x : α → M
⊢ (∃ x_1, Formula.Realize φ x_1 ∧ x_1 ∘ Sum.inl = x) ↔
    ∃ xs, BoundedFormula.Realize φ (Sum.elim x (xs ∘ Fin.cast (_ : m = m))) (xs ∘ Fin.natAdd m)
[PROOFSTEP]
constructor
[GOAL]
case intro.h.mp
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
x : α → M
⊢ (∃ x_1, Formula.Realize φ x_1 ∧ x_1 ∘ Sum.inl = x) →
    ∃ xs, BoundedFormula.Realize φ (Sum.elim x (xs ∘ Fin.cast (_ : m = m))) (xs ∘ Fin.natAdd m)
[PROOFSTEP]
rintro ⟨y, hy, rfl⟩
[GOAL]
case intro.h.mp.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)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
y : α ⊕ Fin m → M
hy : Formula.Realize φ y
⊢ ∃ xs, BoundedFormula.Realize φ (Sum.elim (y ∘ Sum.inl) (xs ∘ Fin.cast (_ : m = m))) (xs ∘ Fin.natAdd m)
[PROOFSTEP]
exact ⟨y ∘ Sum.inr, (congr (congr rfl (Sum.elim_comp_inl_inr y).symm) (funext finZeroElim)).mp hy⟩
[GOAL]
case intro.h.mpr
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
x : α → M
⊢ (∃ xs, BoundedFormula.Realize φ (Sum.elim x (xs ∘ Fin.cast (_ : m = m))) (xs ∘ Fin.natAdd m)) →
    ∃ x_1, Formula.Realize φ x_1 ∧ x_1 ∘ Sum.inl = x
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case intro.h.mpr.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
m : ℕ
φ : Formula (L[[↑A]]) (α ⊕ Fin m)
x : α → M
y : Fin (m + 0) → M
hy : BoundedFormula.Realize φ (Sum.elim x (y ∘ Fin.cast (_ : m = m))) (y ∘ Fin.natAdd m)
⊢ ∃ x_1, Formula.Realize φ x_1 ∧ x_1 ∘ Sum.inl = x
[PROOFSTEP]
exact ⟨Sum.elim x y, (congr rfl (funext finZeroElim)).mp hy, Sum.elim_comp_inl _ _⟩
[GOAL]
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 β
⊢ Definable A L ((fun g => g ∘ ↑f) '' s)
[PROOFSTEP]
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_sum_inl_fin
      _)
simp only [mem_preimage, mem_image, exists_exists_and_eq_and]
refine' exists_congr fun y => and_congr_right fun _ => Eq.congr_left (funext fun a => _)
simp
[GOAL]
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 β
⊢ Definable A L ((fun g => g ∘ ↑f) '' s)
[PROOFSTEP]
cases nonempty_fintype β
[GOAL]
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 β
val✝ : Fintype β
⊢ Definable A L ((fun g => g ∘ ↑f) '' s)
[PROOFSTEP]
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_sum_inl_fin
      _)
[GOAL]
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 β
val✝ : Fintype β
x : α → M
⊢ x ∈
      (fun g => g ∘ Sum.inl) ''
        ((fun g =>
            g ∘
              ↑(Equiv.sumCongr (Equiv.ofInjective ↑f (_ : Function.Injective ↑f))
                  (Fintype.equivFin ↑(range ↑f)ᶜ).symm)) ''
          ((fun g => g ∘ ↑(Equiv.Set.sumCompl (range ↑f))) '' s)) ↔
    x ∈ (fun g => g ∘ ↑f) '' s
[PROOFSTEP]
simp only [mem_preimage, mem_image, exists_exists_and_eq_and]
[GOAL]
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 β
val✝ : Fintype β
x : α → M
⊢ (∃ a,
      a ∈ s ∧
        ((a ∘ ↑(Equiv.Set.sumCompl (range ↑f))) ∘
              ↑(Equiv.sumCongr (Equiv.ofInjective ↑f (_ : Function.Injective ↑f))
                  (Fintype.equivFin ↑(range ↑f)ᶜ).symm)) ∘
            Sum.inl =
          x) ↔
    ∃ x_1, x_1 ∈ s ∧ x_1 ∘ ↑f = x
[PROOFSTEP]
refine' exists_congr fun y => and_congr_right fun _ => Eq.congr_left (funext fun a => _)
[GOAL]
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 β
val✝ : Fintype β
x : α → M
y : β → M
x✝ : y ∈ s
a : α
⊢ (((y ∘ ↑(Equiv.Set.sumCompl (range ↑f))) ∘
          ↑(Equiv.sumCongr (Equiv.ofInjective ↑f (_ : Function.Injective ↑f)) (Fintype.equivFin ↑(range ↑f)ᶜ).symm)) ∘
        Sum.inl)
      a =
    (y ∘ ↑f) a
[PROOFSTEP]
simp
[GOAL]
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)
[PROOFSTEP]
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_sum_inl_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_finset_biInter h' Finset.univ)
  simp
refine' (congr rfl (ext fun x => _)).mp (h.inter h')
simp only [Equiv.coe_trans, 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]
[GOAL]
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)
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
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)
[PROOFSTEP]
cases nonempty_fintype β
[GOAL]
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)
[PROOFSTEP]
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)
[GOAL]
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)
[PROOFSTEP]
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
[GOAL]
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))}
[PROOFSTEP]
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
[GOAL]
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))}
[PROOFSTEP]
refine' fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext _⟩
[GOAL]
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)))))
[PROOFSTEP]
simp
[GOAL]
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))}
[PROOFSTEP]
refine' (congr rfl (ext _)).mp (definable_finset_biInter h' Finset.univ)
[GOAL]
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))}
[PROOFSTEP]
simp
[GOAL]
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)
[PROOFSTEP]
refine' (congr rfl (ext fun x => _)).mp (h.inter h')
[GOAL]
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
[PROOFSTEP]
simp only [Equiv.coe_trans, mem_inter_iff, mem_preimage, mem_image, exists_exists_and_eq_and, mem_setOf_eq]
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
rintro ⟨⟨y, ys, hy⟩, hx⟩
[GOAL]
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
[PROOFSTEP]
refine' ⟨y, ys, _⟩
[GOAL]
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
[PROOFSTEP]
ext a
[GOAL]
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
[PROOFSTEP]
rw [hx a, ← Function.comp_apply (f := x), ← hy]
[GOAL]
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)
[PROOFSTEP]
simp
[GOAL]
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))
[PROOFSTEP]
rintro ⟨y, ys, rfl⟩
[GOAL]
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))
[PROOFSTEP]
refine' ⟨⟨y, ys, _⟩, fun a => _⟩
[GOAL]
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
[PROOFSTEP]
ext
[GOAL]
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✝
[PROOFSTEP]
simp [Set.apply_rangeSplitting f]
[GOAL]
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))
[PROOFSTEP]
rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f, rangeFactorization_coe]


[GOAL]
L : Language
α : Type w
V : Type w'
n : ℕ
inst✝ : Structure Language.graph V
⊢ V ⊨ Theory.simpleGraph ↔ (Irreflexive fun x y => RelMap adj ![x, y]) ∧ Symmetric fun x y => RelMap adj ![x, y]
[PROOFSTEP]
simp [Theory.simpleGraph]
[GOAL]
L : Language
α : Type w
V : Type w'
n : ℕ
G : SimpleGraph V
⊢ V ⊨ Theory.simpleGraph
[PROOFSTEP]
simp only [@Theory.simpleGraph_model_iff _ G.structure, relMap_apply₂]
[GOAL]
L : Language
α : Type w
V : Type w'
n : ℕ
G : SimpleGraph V
⊢ (Irreflexive fun x y => SimpleGraph.Adj G x y) ∧ Symmetric fun x y => SimpleGraph.Adj G x y
[PROOFSTEP]
exact ⟨G.loopless, G.symm⟩
[GOAL]
L : Language
α : Type w
V : Type w'
n : ℕ
G : SimpleGraph V
⊢ FirstOrder.Language.simpleGraphOfStructure V = G
[PROOFSTEP]
ext
[GOAL]
case Adj.h.h.a
L : Language
α : Type w
V : Type w'
n : ℕ
G : SimpleGraph V
x✝¹ x✝ : V
⊢ SimpleGraph.Adj (FirstOrder.Language.simpleGraphOfStructure V) x✝¹ x✝ ↔ SimpleGraph.Adj G x✝¹ x✝
[PROOFSTEP]
rfl
[GOAL]
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
⊢ SimpleGraph.structure (simpleGraphOfStructure V) = S
[PROOFSTEP]
ext
[GOAL]
case funMap.h.h.h
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
x✝² : ℕ
x✝¹ : Functions Language.graph x✝²
x✝ : Fin x✝² → V
⊢ funMap x✝¹ x✝ = funMap x✝¹ x✝
case RelMap.h.h.h.a
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
x✝² : ℕ
x✝¹ : Relations Language.graph x✝²
x✝ : Fin x✝² → V
⊢ RelMap x✝¹ x✝ ↔ RelMap x✝¹ x✝
[PROOFSTEP]
case funMap n f xs => exact (IsRelational.empty_functions n).elim f
[GOAL]
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
f : Functions Language.graph n
xs : Fin n → V
⊢ funMap f xs = funMap f xs
[PROOFSTEP]
case funMap n f xs => exact (IsRelational.empty_functions n).elim f
[GOAL]
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
f : Functions Language.graph n
xs : Fin n → V
⊢ funMap f xs = funMap f xs
[PROOFSTEP]
exact (IsRelational.empty_functions n).elim f
[GOAL]
case RelMap.h.h.h.a
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
x✝² : ℕ
x✝¹ : Relations Language.graph x✝²
x✝ : Fin x✝² → V
⊢ RelMap x✝¹ x✝ ↔ RelMap x✝¹ x✝
[PROOFSTEP]
case RelMap n r xs =>
  rw [iff_eq_eq]
  cases' n with n
  · exact r.elim
  · cases' n with n
    · exact r.elim
    · cases' n with n
      · cases r
        change RelMap adj ![xs 0, xs 1] = _
        refine' congr rfl (funext _)
        simp [Fin.forall_fin_two]
      · exact r.elim
[GOAL]
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Relations Language.graph n
xs : Fin n → V
⊢ RelMap r xs ↔ RelMap r xs
[PROOFSTEP]
case RelMap n r xs =>
  rw [iff_eq_eq]
  cases' n with n
  · exact r.elim
  · cases' n with n
    · exact r.elim
    · cases' n with n
      · cases r
        change RelMap adj ![xs 0, xs 1] = _
        refine' congr rfl (funext _)
        simp [Fin.forall_fin_two]
      · exact r.elim
[GOAL]
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Relations Language.graph n
xs : Fin n → V
⊢ RelMap r xs ↔ RelMap r xs
[PROOFSTEP]
rw [iff_eq_eq]
[GOAL]
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Relations Language.graph n
xs : Fin n → V
⊢ RelMap r xs = RelMap r xs
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
r : Relations Language.graph Nat.zero
xs : Fin Nat.zero → V
⊢ RelMap r xs = RelMap r xs
[PROOFSTEP]
exact r.elim
[GOAL]
case succ
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Relations Language.graph (Nat.succ n)
xs : Fin (Nat.succ n) → V
⊢ RelMap r xs = RelMap r xs
[PROOFSTEP]
cases' n with n
[GOAL]
case succ.zero
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
r : Relations Language.graph (Nat.succ Nat.zero)
xs : Fin (Nat.succ Nat.zero) → V
⊢ RelMap r xs = RelMap r xs
[PROOFSTEP]
exact r.elim
[GOAL]
case succ.succ
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Relations Language.graph (Nat.succ (Nat.succ n))
xs : Fin (Nat.succ (Nat.succ n)) → V
⊢ RelMap r xs = RelMap r xs
[PROOFSTEP]
cases' n with n
[GOAL]
case succ.succ.zero
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
r : Relations Language.graph (Nat.succ (Nat.succ Nat.zero))
xs : Fin (Nat.succ (Nat.succ Nat.zero)) → V
⊢ RelMap r xs = RelMap r xs
[PROOFSTEP]
cases r
[GOAL]
case succ.succ.zero.unit
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
xs : Fin (Nat.succ (Nat.succ Nat.zero)) → V
⊢ RelMap PUnit.unit xs = RelMap PUnit.unit xs
[PROOFSTEP]
change RelMap adj ![xs 0, xs 1] = _
[GOAL]
case succ.succ.zero.unit
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
xs : Fin (Nat.succ (Nat.succ Nat.zero)) → V
⊢ RelMap adj ![xs 0, xs 1] = RelMap PUnit.unit xs
[PROOFSTEP]
refine' congr rfl (funext _)
[GOAL]
case succ.succ.zero.unit
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
xs : Fin (Nat.succ (Nat.succ Nat.zero)) → V
⊢ ∀ (x : Fin (Nat.succ 1)), Matrix.vecCons (xs 0) ![xs 1] x = xs x
[PROOFSTEP]
simp [Fin.forall_fin_two]
[GOAL]
case succ.succ.succ
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Relations Language.graph (Nat.succ (Nat.succ (Nat.succ n)))
xs : Fin (Nat.succ (Nat.succ (Nat.succ n))) → V
⊢ RelMap r xs = RelMap r xs
[PROOFSTEP]
exact r.elim


[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ OrderedStructure Language.order M
[PROOFSTEP]
rw [orderedStructure_iff, orderLHom_order]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ LHom.IsExpansionOn (LHom.id Language.order) M
[PROOFSTEP]
exact LHom.id_isExpansionOn M
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
⊢ M ⊨ preorderTheory Language.order
[PROOFSTEP]
simp only [preorderTheory, Theory.model_iff, Set.mem_insert_iff, Set.mem_singleton_iff, forall_eq_or_imp,
  Relations.realize_reflexive, relMap_apply₂, forall_eq, Relations.realize_transitive]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
⊢ (Reflexive fun x y => x ≤ y) ∧ Transitive fun x y => x ≤ y
[PROOFSTEP]
exact ⟨le_refl, fun _ _ _ => le_trans⟩
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : PartialOrder M
⊢ M ⊨ partialOrderTheory Language.order
[PROOFSTEP]
simp only [partialOrderTheory, Theory.model_iff, Set.mem_insert_iff, Set.mem_singleton_iff, forall_eq_or_imp,
  Relations.realize_reflexive, relMap_apply₂, Relations.realize_antisymmetric, forall_eq, Relations.realize_transitive]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : PartialOrder M
⊢ (Reflexive fun x y => x ≤ y) ∧ (AntiSymmetric fun x y => x ≤ y) ∧ Transitive fun x y => x ≤ y
[PROOFSTEP]
exact ⟨le_refl, fun _ _ => le_antisymm, fun _ _ _ => le_trans⟩
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LinearOrder M
⊢ M ⊨ linearOrderTheory Language.order
[PROOFSTEP]
simp only [linearOrderTheory, Theory.model_iff, Set.mem_insert_iff, Set.mem_singleton_iff, forall_eq_or_imp,
  Relations.realize_reflexive, relMap_apply₂, Relations.realize_antisymmetric, Relations.realize_transitive, forall_eq,
  Relations.realize_total]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LinearOrder M
⊢ (Reflexive fun x y => x ≤ y) ∧
    (AntiSymmetric fun x y => x ≤ y) ∧ (Transitive fun x y => x ≤ y) ∧ Total fun x y => x ≤ y
[PROOFSTEP]
exact ⟨le_refl, fun _ _ => le_antisymm, fun _ _ _ => le_trans, le_total⟩
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : IsOrdered L
inst✝² : Structure L M
inst✝¹ : LE M
inst✝ : OrderedStructure L M
a b : M
⊢ RelMap leSymb ![a, b] ↔ a ≤ b
[PROOFSTEP]
rw [← orderLHom_leSymb, LHom.map_onRelation]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : IsOrdered L
inst✝² : Structure L M
inst✝¹ : LE M
inst✝ : OrderedStructure L M
a b : M
⊢ RelMap leSymb ![a, b] ↔ a ≤ b
[PROOFSTEP]
rfl
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : IsOrdered L
inst✝² : Structure L M
inst✝¹ : LE M
inst✝ : OrderedStructure L M
t₁ t₂ : Term L (α ⊕ Fin n)
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize (le t₁ t₂) v xs ↔ realize (Sum.elim v xs) t₁ ≤ realize (Sum.elim v xs) t₂
[PROOFSTEP]
simp [Term.le]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : IsOrdered L
inst✝² : Structure L M
inst✝¹ : Preorder M
inst✝ : OrderedStructure L M
t₁ t₂ : Term L (α ⊕ Fin n)
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize (lt t₁ t₂) v xs ↔ realize (Sum.elim v xs) t₁ < realize (Sum.elim v xs) t₂
[PROOFSTEP]
simp [Term.lt, lt_iff_le_not_le]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ M ⊨ noTopOrderSentence Language.order ↔ NoTopOrder M
[PROOFSTEP]
simp only [noTopOrderSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_all, BoundedFormula.realize_ex,
  BoundedFormula.realize_not, Term.realize, Term.realize_le, Sum.elim_inr]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ (∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 1 ≤ Fin.snoc (Fin.snoc default a) a_1 0) ↔ NoTopOrder M
[PROOFSTEP]
refine' ⟨fun h => ⟨fun a => h a⟩, _⟩
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ NoTopOrder M → ∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 1 ≤ Fin.snoc (Fin.snoc default a) a_1 0
[PROOFSTEP]
intro h a
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
h : NoTopOrder M
a : M
⊢ ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 1 ≤ Fin.snoc (Fin.snoc default a) a_1 0
[PROOFSTEP]
exact exists_not_le a
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ M ⊨ noBotOrderSentence Language.order ↔ NoBotOrder M
[PROOFSTEP]
simp only [noBotOrderSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_all, BoundedFormula.realize_ex,
  BoundedFormula.realize_not, Term.realize, Term.realize_le, Sum.elim_inr]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ (∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 0 ≤ Fin.snoc (Fin.snoc default a) a_1 1) ↔ NoBotOrder M
[PROOFSTEP]
refine' ⟨fun h => ⟨fun a => h a⟩, _⟩
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ NoBotOrder M → ∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 0 ≤ Fin.snoc (Fin.snoc default a) a_1 1
[PROOFSTEP]
intro h a
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
h : NoBotOrder M
a : M
⊢ ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 0 ≤ Fin.snoc (Fin.snoc default a) a_1 1
[PROOFSTEP]
exact exists_not_ge a
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
⊢ M ⊨ denselyOrderedSentence Language.order ↔ DenselyOrdered M
[PROOFSTEP]
simp only [denselyOrderedSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_imp,
  BoundedFormula.realize_all, Term.realize, Term.realize_lt, Sum.elim_inr, BoundedFormula.realize_ex,
  BoundedFormula.realize_inf]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
⊢ (∀ (a a_1 : M),
      Fin.snoc (Fin.snoc default a) a_1 0 < Fin.snoc (Fin.snoc default a) a_1 1 →
        ∃ a_3,
          Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 0 < Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 2 ∧
            Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 2 < Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 1) ↔
    DenselyOrdered M
[PROOFSTEP]
refine' ⟨fun h => ⟨fun a b ab => h a b ab⟩, _⟩
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
⊢ DenselyOrdered M →
    ∀ (a a_1 : M),
      Fin.snoc (Fin.snoc default a) a_1 0 < Fin.snoc (Fin.snoc default a) a_1 1 →
        ∃ a_3,
          Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 0 < Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 2 ∧
            Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 2 < Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 1
[PROOFSTEP]
intro h a b ab
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
h : DenselyOrdered M
a b : M
ab : Fin.snoc (Fin.snoc default a) b 0 < Fin.snoc (Fin.snoc default a) b 1
⊢ ∃ a_1,
    Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 0 < Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 2 ∧
      Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 2 < Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 1
[PROOFSTEP]
exact exists_between ab
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : LinearOrder M
inst✝² : DenselyOrdered M
inst✝¹ : NoTopOrder M
inst✝ : NoBotOrder M
⊢ M ⊨ dlo Language.order
[PROOFSTEP]
simp only [dlo, Set.union_insert, Set.union_singleton, Theory.model_iff, Set.mem_insert_iff, forall_eq_or_imp,
  realize_noTopOrder, realize_noBotOrder, realize_denselyOrdered, true_and_iff]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : LinearOrder M
inst✝² : DenselyOrdered M
inst✝¹ : NoTopOrder M
inst✝ : NoBotOrder M
⊢ ∀ (a : Sentence Language.order), a ∈ linearOrderTheory Language.order → M ⊨ a
[PROOFSTEP]
rw [← Theory.model_iff]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : LinearOrder M
inst✝² : DenselyOrdered M
inst✝¹ : NoTopOrder M
inst✝ : NoBotOrder M
⊢ M ⊨ linearOrderTheory Language.order
[PROOFSTEP]
infer_instance


[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ Finsupp.single g 1 * average k G = average k G
[PROOFSTEP]
simp only [mul_one, Finset.mul_sum, Algebra.mul_smul_comm, average, MonoidAlgebra.of_apply, Finset.sum_congr,
  MonoidAlgebra.single_mul_single]
[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (g * x) 1 = ⅟↑(Fintype.card G) • ∑ x : G, single x 1
[PROOFSTEP]
set f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (g * x) 1 = ⅟↑(Fintype.card G) • Finset.sum Finset.univ f
[PROOFSTEP]
show ⅟(Fintype.card G : k) • ∑ x : G, f (g * x) = ⅟(Fintype.card G : k) • ∑ x : G, f x
[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, f (g * x) = ⅟↑(Fintype.card G) • ∑ x : G, f x
[PROOFSTEP]
rw [Function.Bijective.sum_comp (Group.mulLeft_bijective g) _]
[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ average k G * Finsupp.single g 1 = average k G
[PROOFSTEP]
simp only [mul_one, Finset.sum_mul, Algebra.smul_mul_assoc, average, MonoidAlgebra.of_apply, Finset.sum_congr,
  MonoidAlgebra.single_mul_single]
[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (x * g) 1 = ⅟↑(Fintype.card G) • ∑ x : G, single x 1
[PROOFSTEP]
set f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (x * g) 1 = ⅟↑(Fintype.card G) • Finset.sum Finset.univ f
[PROOFSTEP]
show ⅟(Fintype.card G : k) • ∑ x : G, f (x * g) = ⅟(Fintype.card G : k) • ∑ x : G, f x
[GOAL]
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, f (x * g) = ⅟↑(Fintype.card G) • ∑ x : G, f x
[PROOFSTEP]
rw [Function.Bijective.sum_comp (Group.mulRight_bijective g) _]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
a✝ b✝ : V
hv : a✝ ∈ {v | ∀ (g : G), ↑(↑ρ g) v = v}
hw : b✝ ∈ {v | ∀ (g : G), ↑(↑ρ g) v = v}
g : G
⊢ ↑(↑ρ g) (a✝ + b✝) = a✝ + b✝
[PROOFSTEP]
simp only [hv g, hw g, map_add]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
⊢ ↑(↑ρ g) 0 = 0
[PROOFSTEP]
simp only [map_zero]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
r : k
v : V
hv :
  v ∈
    {
          toAddSubsemigroup :=
            { carrier := {v | ∀ (g : G), ↑(↑ρ g) v = v},
              add_mem' :=
                (_ :
                  ∀ {a b : V},
                    a ∈ {v | ∀ (g : G), ↑(↑ρ g) v = v} →
                      b ∈ {v | ∀ (g : G), ↑(↑ρ g) v = v} → ∀ (g : G), ↑(↑ρ g) (a + b) = a + b) },
          zero_mem' := (_ : ∀ (g : G), ↑(↑ρ g) 0 = 0) }.toAddSubsemigroup.carrier
g : G
⊢ ↑(↑ρ g) (r • v) = r • v
[PROOFSTEP]
simp only [hv g, LinearMap.map_smulₛₗ, RingHom.id_apply]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
v : V
⊢ v ∈ invariants ρ ↔ ∀ (g : G), ↑(↑ρ g) v = v
[PROOFSTEP]
rfl
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
⊢ (invariants ρ).toAddSubmonoid.toAddSubsemigroup.carrier = ⋂ (g : G), Function.fixedPoints ↑(↑ρ g)
[PROOFSTEP]
ext
[GOAL]
case h
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : V
⊢ x✝ ∈ (invariants ρ).toAddSubmonoid.toAddSubsemigroup.carrier ↔ x✝ ∈ ⋂ (g : G), Function.fixedPoints ↑(↑ρ g)
[PROOFSTEP]
simp [Function.IsFixedPt]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
g : G
⊢ ↑(↑ρ g) (↑(averageMap ρ) v) = ↑(averageMap ρ) v
[PROOFSTEP]
rw [averageMap, ← asAlgebraHom_single_one, ← LinearMap.mul_apply, ← map_mul (asAlgebraHom ρ), mul_average_left]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
hv : v ∈ invariants ρ
⊢ ↑(averageMap ρ) v = v
[PROOFSTEP]
rw [mem_invariants] at hv
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
hv : ∀ (g : G), ↑(↑ρ g) v = v
⊢ ↑(averageMap ρ) v = v
[PROOFSTEP]
simp [average, map_sum, hv, Finset.card_univ, nsmul_eq_smul_cast k _ v, smul_smul]
[GOAL]
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
f : ↑X.V →ₗ[k] ↑Y.V
g : ↑G
⊢ ↑(↑(linHom (Rep.ρ X) (Rep.ρ Y)) g) f = f ↔ LinearMap.comp f (↑(Rep.ρ X) g) = LinearMap.comp (↑(Rep.ρ Y) g) f
[PROOFSTEP]
dsimp
[GOAL]
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
f : ↑X.V →ₗ[k] ↑Y.V
g : ↑G
⊢ LinearMap.comp (↑(Rep.ρ Y) g) (LinearMap.comp f (↑(Rep.ρ X) g⁻¹)) = f ↔
    LinearMap.comp f (↑(Rep.ρ X) g) = LinearMap.comp (↑(Rep.ρ Y) g) f
[PROOFSTEP]
erw [← ρAut_apply_inv]
[GOAL]
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
f : ↑X.V →ₗ[k] ↑Y.V
g : ↑G
⊢ LinearMap.comp (↑(Rep.ρ Y) g) (LinearMap.comp f (↑(ρAut X) g).inv) = f ↔
    LinearMap.comp f (↑(Rep.ρ X) g) = LinearMap.comp (↑(Rep.ρ Y) g) f
[PROOFSTEP]
rw [← LinearMap.comp_assoc, ← ModuleCat.comp_def, ← ModuleCat.comp_def, Iso.inv_comp_eq, ρAut_apply_hom]
[GOAL]
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
f : ↑X.V →ₗ[k] ↑Y.V
g : ↑G
⊢ f ≫ ↑(Rep.ρ Y) g = ↑X.ρ g ≫ f ↔ LinearMap.comp f (↑(Rep.ρ X) g) = f ≫ ↑(Rep.ρ Y) g
[PROOFSTEP]
exact comm
[GOAL]
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
x✝ : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }
⊢ (fun f => { val := f.hom, property := (_ : ∀ (g : ↑G), ↑(↑(linHom (Rep.ρ X) (Rep.ρ Y)) g) f.hom = f.hom) })
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f => Hom.mk ↑f,
                map_add' :=
                  (_ :
                    ∀ (x x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                      (fun f => Hom.mk ↑f) (x + x_1) = (fun f => Hom.mk ↑f) (x + x_1)) },
            map_smul' :=
              (_ :
                ∀ (x : k) (x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                  AddHom.toFun
                      { toFun := fun f => Hom.mk ↑f,
                        map_add' :=
                          (_ :
                            ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                              (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                      (x • x_1) =
                    AddHom.toFun
                      { toFun := fun f => Hom.mk ↑f,
                        map_add' :=
                          (_ :
                            ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                              (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                      (x • x_1)) }.toAddHom
        x✝) =
    x✝
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case a
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
x✝ : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }
⊢ ↑((fun f => { val := f.hom, property := (_ : ∀ (g : ↑G), ↑(↑(linHom (Rep.ρ X) (Rep.ρ Y)) g) f.hom = f.hom) })
        (AddHom.toFun
          {
              toAddHom :=
                { toFun := fun f => Hom.mk ↑f,
                  map_add' :=
                    (_ :
                      ∀ (x x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                        (fun f => Hom.mk ↑f) (x + x_1) = (fun f => Hom.mk ↑f) (x + x_1)) },
              map_smul' :=
                (_ :
                  ∀ (x : k) (x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                    AddHom.toFun
                        { toFun := fun f => Hom.mk ↑f,
                          map_add' :=
                            (_ :
                              ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                                (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                        (x • x_1) =
                      AddHom.toFun
                        { toFun := fun f => Hom.mk ↑f,
                          map_add' :=
                            (_ :
                              ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                                (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                        (x • x_1)) }.toAddHom
          x✝)) =
    ↑x✝
[PROOFSTEP]
ext
[GOAL]
case a.h
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
x✝¹ : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }
x✝ : CoeSort.coe X
⊢ ↑↑((fun f => { val := f.hom, property := (_ : ∀ (g : ↑G), ↑(↑(linHom (Rep.ρ X) (Rep.ρ Y)) g) f.hom = f.hom) })
            (AddHom.toFun
              {
                  toAddHom :=
                    { toFun := fun f => Hom.mk ↑f,
                      map_add' :=
                        (_ :
                          ∀ (x x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                            (fun f => Hom.mk ↑f) (x + x_1) = (fun f => Hom.mk ↑f) (x + x_1)) },
                  map_smul' :=
                    (_ :
                      ∀ (x : k) (x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                        AddHom.toFun
                            { toFun := fun f => Hom.mk ↑f,
                              map_add' :=
                                (_ :
                                  ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                                    (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                            (x • x_1) =
                          AddHom.toFun
                            { toFun := fun f => Hom.mk ↑f,
                              map_add' :=
                                (_ :
                                  ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                                    (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                            (x • x_1)) }.toAddHom
              x✝¹))
      x✝ =
    ↑↑x✝¹ x✝
[PROOFSTEP]
rfl
  -- Porting note: Added `apply Subtype.ext`
[GOAL]
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
x✝ : X ⟶ Y
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f => Hom.mk ↑f,
              map_add' :=
                (_ :
                  ∀ (x x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                    (fun f => Hom.mk ↑f) (x + x_1) = (fun f => Hom.mk ↑f) (x + x_1)) },
          map_smul' :=
            (_ :
              ∀ (x : k) (x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                AddHom.toFun
                    { toFun := fun f => Hom.mk ↑f,
                      map_add' :=
                        (_ :
                          ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                            (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                    (x • x_1) =
                  AddHom.toFun
                    { toFun := fun f => Hom.mk ↑f,
                      map_add' :=
                        (_ :
                          ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                            (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                    (x • x_1)) }.toAddHom
      ((fun f => { val := f.hom, property := (_ : ∀ (g : ↑G), ↑(↑(linHom (Rep.ρ X) (Rep.ρ Y)) g) f.hom = f.hom) }) x✝) =
    x✝
[PROOFSTEP]
ext
[GOAL]
case h.h
k : Type u
inst✝ : CommRing k
G : GroupCat
X Y : Rep k ↑G
x✝¹ : X ⟶ Y
x✝ : ↑X.V
⊢ ↑(AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => Hom.mk ↑f,
                    map_add' :=
                      (_ :
                        ∀ (x x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                          (fun f => Hom.mk ↑f) (x + x_1) = (fun f => Hom.mk ↑f) (x + x_1)) },
                map_smul' :=
                  (_ :
                    ∀ (x : k) (x_1 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                      AddHom.toFun
                          { toFun := fun f => Hom.mk ↑f,
                            map_add' :=
                              (_ :
                                ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                                  (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                          (x • x_1) =
                        AddHom.toFun
                          { toFun := fun f => Hom.mk ↑f,
                            map_add' :=
                              (_ :
                                ∀ (x x_2 : { x // x ∈ invariants (linHom (Rep.ρ X) (Rep.ρ Y)) }),
                                  (fun f => Hom.mk ↑f) (x + x_2) = (fun f => Hom.mk ↑f) (x + x_2)) }
                          (x • x_1)) }.toAddHom
            ((fun f => { val := f.hom, property := (_ : ∀ (g : ↑G), ↑(↑(linHom (Rep.ρ X) (Rep.ρ Y)) g) f.hom = f.hom) })
              x✝¹)).hom
      x✝ =
    ↑x✝¹.hom x✝
[PROOFSTEP]
rfl
[GOAL]
k : Type u
inst✝ : Field k
G : GroupCat
X Y : FdRep k ↑G
⊢ { x // x ∈ invariants (linHom (FdRep.ρ X) (FdRep.ρ Y)) } ≃ₗ[k] X ⟶ Y
[PROOFSTEP]
rw [← FdRep.forget₂_ρ, ← FdRep.forget₂_ρ]
  -- Porting note: The original version used `linHom.invariantsEquivRepHom _ _ ≪≫ₗ`
[GOAL]
k : Type u
inst✝ : Field k
G : GroupCat
X Y : FdRep k ↑G
⊢ { x //
      x ∈
        invariants
          (linHom (Rep.ρ ((forget₂ (FdRep k ↑G) (Rep k ↑G)).obj X))
            (Rep.ρ ((forget₂ (FdRep k ↑G) (Rep k ↑G)).obj Y))) } ≃ₗ[k]
    X ⟶ Y
[PROOFSTEP]
exact
  linHom.invariantsEquivRepHom ((forget₂ (FdRep k G) (Rep k G)).obj X) ((forget₂ (FdRep k G) (Rep k G)).obj Y) ≪≫ₗ
    FdRep.forget₂HomLinearEquiv X Y


[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
⊢ IsChain r univ ↔ IsTrichotomous α r
[PROOFSTEP]
refine' ⟨fun h => ⟨fun a b => _⟩, fun h => @isChain_of_trichotomous _ _ h univ⟩
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a✝ b✝ x y : α
h : IsChain r univ
a b : α
⊢ r a b ∨ a = b ∨ r b a
[PROOFSTEP]
rw [or_left_comm, or_iff_not_imp_left]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a✝ b✝ x y : α
h : IsChain r univ
a b : α
⊢ ¬a = b → r a b ∨ r b a
[PROOFSTEP]
exact h trivial trivial
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun x x_1 => x ≤ x_1) (range f)
[PROOFSTEP]
rw [← image_univ]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun x x_1 => x ≤ x_1) (f '' univ)
[PROOFSTEP]
exact (isChain_of_trichotomous _).image (· ≤ ·) _ _ hf
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ c₁ c₂ c₃ s t : Set α
a✝ b✝ x y : α
inst✝ : IsRefl α r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x✝¹ x✝ : { a // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
⊢ ∃ z,
    r ((fun x => f ↑x) { val := a, property := ha }) ((fun x => f ↑x) z) ∧
      r ((fun x => f ↑x) { val := b, property := hb }) ((fun x => f ↑x) z)
[PROOFSTEP]
simp only [hab, exists_prop, and_self_iff, Subtype.exists]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ c₁ c₂ c₃ s t : Set α
a✝ b✝ x y : α
inst✝ : IsRefl α r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x✝¹ x✝ : { a // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
⊢ ∃ a, a ∈ c ∧ r (f b) (f a)
[PROOFSTEP]
exact ⟨b, hb, refl _⟩
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ c₁ c₂ c₃ s t : Set α
a✝ b✝ x y : α
inst✝¹ : IsRefl α r
hchain : IsChain r s
inst✝ : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
⊢ ∃ z x, r a z ∧ r b z ∧ r c z
[PROOFSTEP]
rcases directedOn_iff_directed.mpr (IsChain.directed hchain) a mem1 b mem2 with ⟨z, mem4, H1, H2⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ c₁ c₂ c₃ s t : Set α
a✝ b✝ x y : α
inst✝¹ : IsRefl α r
hchain : IsChain r s
inst✝ : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
z : α
mem4 : z ∈ s
H1 : r a z
H2 : r b z
⊢ ∃ z x, r a z ∧ r b z ∧ r c z
[PROOFSTEP]
rcases directedOn_iff_directed.mpr (IsChain.directed hchain) z mem4 c mem3 with ⟨z', mem5, H3, H4⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ c₁ c₂ c₃ s t : Set α
a✝ b✝ x y : α
inst✝¹ : IsRefl α r
hchain : IsChain r s
inst✝ : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
z : α
mem4 : z ∈ s
H1 : r a z
H2 : r b z
z' : α
mem5 : z' ∈ s
H3 : r z z'
H4 : r c z'
⊢ ∃ z x, r a z ∧ r b z ∧ r c z
[PROOFSTEP]
exact ⟨z', mem5, _root_.trans H1 H3, _root_.trans H2 H3, H4⟩
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ∃ t, IsChain r s ∧ SuperChain r s t
⊢ SuperChain r s (SuccChain r s)
[PROOFSTEP]
have : IsChain r s ∧ SuperChain r s (choose h) := @choose_spec _ (fun t => IsChain r s ∧ SuperChain r s t) _
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ∃ t, IsChain r s ∧ SuperChain r s t
this : IsChain r s ∧ SuperChain r s (choose h)
⊢ SuperChain r s (SuccChain r s)
[PROOFSTEP]
simpa [SuccChain, dif_pos, exists_and_left.mp h] using this.2
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hs : IsChain r s
h : ¬∃ t, IsChain r s ∧ SuperChain r s t
⊢ IsChain r (SuccChain r s)
[PROOFSTEP]
rw [exists_and_left] at h
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hs : IsChain r s
h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)
⊢ IsChain r (SuccChain r s)
[PROOFSTEP]
simpa [SuccChain, dif_neg, h] using hs
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hs₁ : IsChain r s
hs₂ : ¬IsMaxChain r s
⊢ SuperChain r s (SuccChain r s)
[PROOFSTEP]
simp only [IsMaxChain, not_and, not_forall, exists_prop, exists_and_left] at hs₂
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
⊢ SuperChain r s (SuccChain r s)
[PROOFSTEP]
obtain ⟨t, ht, hst⟩ := hs₂ hs₁
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t✝ : Set α
a b x y : α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
t : Set α
ht : IsChain r t
hst : s ⊆ t ∧ ¬s = t
⊢ SuperChain r s (SuccChain r s)
[PROOFSTEP]
exact succChain_spec ⟨t, hs₁, ht, ssubset_iff_subset_ne.2 hst⟩
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ¬∃ t, IsChain r s ∧ SuperChain r s t
⊢ s ⊆ SuccChain r s
[PROOFSTEP]
rw [exists_and_left] at h
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)
⊢ s ⊆ SuccChain r s
[PROOFSTEP]
simp [SuccChain, dif_neg, h, Subset.rfl]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
⊢ ChainClosure r ∅
[PROOFSTEP]
have : ChainClosure r (⋃₀ ∅) := ChainClosure.union fun a h => False.rec h
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
this : ChainClosure r (⋃₀ ∅)
⊢ ChainClosure r ∅
[PROOFSTEP]
simpa using this
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₁ : ChainClosure r c₁
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ c₁ ∨ c₁ ⊆ c₂
[PROOFSTEP]
induction hc₁
[GOAL]
case succ
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s✝ : Set α
a✝ : ChainClosure r s✝
a_ih✝ : SuccChain r c₂ ⊆ s✝ ∨ s✝ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r s✝ ∨ SuccChain r s✝ ⊆ c₂
case union
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
⊢ SuccChain r c₂ ⊆ ⋃₀ s✝ ∨ ⋃₀ s✝ ⊆ c₂
[PROOFSTEP]
case succ c₃ hc₃ ih =>
  cases' ih with ih ih
  · exact Or.inl (ih.trans subset_succChain)
  · exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃✝ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃ ∨ c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
[PROOFSTEP]
case succ c₃ hc₃ ih =>
  cases' ih with ih ih
  · exact Or.inl (ih.trans subset_succChain)
  · exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃✝ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃ ∨ c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
[PROOFSTEP]
cases' ih with ih ih
[GOAL]
case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃✝ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
[PROOFSTEP]
exact Or.inl (ih.trans subset_succChain)
[GOAL]
case inr
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃✝ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
[PROOFSTEP]
exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl
[GOAL]
case union
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
⊢ SuccChain r c₂ ⊆ ⋃₀ s✝ ∨ ⋃₀ s✝ ⊆ c₂
[PROOFSTEP]
case union s _ ih =>
  refine' or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => _
  exact (ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s✝ t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
⊢ SuccChain r c₂ ⊆ ⋃₀ s ∨ ⋃₀ s ⊆ c₂
[PROOFSTEP]
case union s _ ih =>
  refine' or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => _
  exact (ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s✝ t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
⊢ SuccChain r c₂ ⊆ ⋃₀ s ∨ ⋃₀ s ⊆ c₂
[PROOFSTEP]
refine' or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => _
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s✝ t : Set α
a✝¹ b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
hn : ¬SuccChain r c₂ ⊆ ⋃₀ s
a : Set α
ha : a ∈ s
⊢ a ⊆ c₂
[PROOFSTEP]
exact (ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
h : c₁ ⊆ c₂
⊢ c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
[PROOFSTEP]
induction hc₂ generalizing c₁ hc₁
[GOAL]
case succ
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂ c₃ s t : Set α
a b x y : α
s✝ : Set α
a✝ : ChainClosure r s✝
a_ih✝ : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ s✝ → s✝ = c₁ ∨ SuccChain r c₁ ⊆ s✝
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r s✝
⊢ SuccChain r s✝ = c₁ ∨ SuccChain r c₁ ⊆ SuccChain r s✝
case union
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂ c₃ s t : Set α
a b x y : α
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
⊢ ⋃₀ s✝ = c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s✝
[PROOFSTEP]
case succ c₂ _
  ih =>
  refine' ((chainClosure_succ_total_aux hc₁) fun c₁ => ih).imp h.antisymm' fun h₁ => _
  obtain rfl | h₂ := ih hc₁ h₁
  · exact Subset.rfl
  · exact h₂.trans subset_succChain
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂✝ c₃ s t : Set α
a b x y : α
c₂ : Set α
a✝ : ChainClosure r c₂
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ c₂ → c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r c₂
⊢ SuccChain r c₂ = c₁ ∨ SuccChain r c₁ ⊆ SuccChain r c₂
[PROOFSTEP]
case succ c₂ _
  ih =>
  refine' ((chainClosure_succ_total_aux hc₁) fun c₁ => ih).imp h.antisymm' fun h₁ => _
  obtain rfl | h₂ := ih hc₁ h₁
  · exact Subset.rfl
  · exact h₂.trans subset_succChain
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂✝ c₃ s t : Set α
a b x y : α
c₂ : Set α
a✝ : ChainClosure r c₂
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ c₂ → c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r c₂
⊢ SuccChain r c₂ = c₁ ∨ SuccChain r c₁ ⊆ SuccChain r c₂
[PROOFSTEP]
refine' ((chainClosure_succ_total_aux hc₁) fun c₁ => ih).imp h.antisymm' fun h₁ => _
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂✝ c₃ s t : Set α
a b x y : α
c₂ : Set α
a✝ : ChainClosure r c₂
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ c₂ → c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r c₂
h₁ : c₁ ⊆ c₂
⊢ SuccChain r c₁ ⊆ SuccChain r c₂
[PROOFSTEP]
obtain rfl | h₂ := ih hc₁ h₁
[GOAL]
case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂✝ c₃ s t : Set α
a b x y : α
c₂ : Set α
a✝ : ChainClosure r c₂
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ c₂ → c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
hc₁ : ChainClosure r c₂
h : c₂ ⊆ SuccChain r c₂
h₁ : c₂ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₂
[PROOFSTEP]
exact Subset.rfl
[GOAL]
case inr
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂✝ c₃ s t : Set α
a b x y : α
c₂ : Set α
a✝ : ChainClosure r c₂
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ c₂ → c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r c₂
h₁ : c₁ ⊆ c₂
h₂ : SuccChain r c₁ ⊆ c₂
⊢ SuccChain r c₁ ⊆ SuccChain r c₂
[PROOFSTEP]
exact h₂.trans subset_succChain
[GOAL]
case union
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂ c₃ s t : Set α
a b x y : α
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
⊢ ⋃₀ s✝ = c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s✝
[PROOFSTEP]
case union s _ ih =>
  apply Or.imp_left h.antisymm'
  apply by_contradiction
  simp only [sUnion_subset_iff, not_or, not_forall, exists_prop, and_imp, forall_exists_index]
  intro c₃ hc₃ h₁ h₂
  obtain h | h := chainClosure_succ_total_aux hc₁ fun c₄ => ih _ hc₃
  · exact h₁ (subset_succChain.trans h)
  obtain h' | h' := ih c₃ hc₃ hc₁ h
  · exact h₁ h'.subset
  · exact h₂ (h'.trans <| subset_sUnion_of_mem hc₃)
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
⊢ ⋃₀ s = c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s
[PROOFSTEP]
case union s _ ih =>
  apply Or.imp_left h.antisymm'
  apply by_contradiction
  simp only [sUnion_subset_iff, not_or, not_forall, exists_prop, and_imp, forall_exists_index]
  intro c₃ hc₃ h₁ h₂
  obtain h | h := chainClosure_succ_total_aux hc₁ fun c₄ => ih _ hc₃
  · exact h₁ (subset_succChain.trans h)
  obtain h' | h' := ih c₃ hc₃ hc₁ h
  · exact h₁ h'.subset
  · exact h₂ (h'.trans <| subset_sUnion_of_mem hc₃)
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
⊢ ⋃₀ s = c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s
[PROOFSTEP]
apply Or.imp_left h.antisymm'
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
⊢ ⋃₀ s ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s
[PROOFSTEP]
apply by_contradiction
[GOAL]
case a
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
⊢ ¬(⋃₀ s ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s) → False
[PROOFSTEP]
simp only [sUnion_subset_iff, not_or, not_forall, exists_prop, and_imp, forall_exists_index]
[GOAL]
case a
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
⊢ ∀ (x : Set α), x ∈ s → ¬x ⊆ c₁ → ¬SuccChain r c₁ ⊆ ⋃₀ s → False
[PROOFSTEP]
intro c₃ hc₃ h₁ h₂
[GOAL]
case a
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
⊢ False
[PROOFSTEP]
obtain h | h := chainClosure_succ_total_aux hc₁ fun c₄ => ih _ hc₃
[GOAL]
case a.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : SuccChain r c₃ ⊆ c₁
⊢ False
[PROOFSTEP]
exact h₁ (subset_succChain.trans h)
[GOAL]
case a.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : c₁ ⊆ c₃
⊢ False
[PROOFSTEP]
obtain h' | h' := ih c₃ hc₃ hc₁ h
[GOAL]
case a.inr.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : c₁ ⊆ c₃
h' : c₃ = c₁
⊢ False
[PROOFSTEP]
exact h₁ h'.subset
[GOAL]
case a.inr.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : c₁ ⊆ c₃
h' : SuccChain r c₁ ⊆ c₃
⊢ False
[PROOFSTEP]
exact h₂ (h'.trans <| subset_sUnion_of_mem hc₃)
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
⊢ c₁ ⊆ c₂
[PROOFSTEP]
induction hc₁
[GOAL]
case succ
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s✝ : Set α
a✝ : ChainClosure r s✝
a_ih✝ : s✝ ⊆ c₂
⊢ SuccChain r s✝ ⊆ c₂
case union
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → a ⊆ c₂
⊢ ⋃₀ s✝ ⊆ c₂
[PROOFSTEP]
case succ s₁ hc₁ h => exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s₁ : Set α
hc₁ : ChainClosure r s₁
h : s₁ ⊆ c₂
⊢ SuccChain r s₁ ⊆ c₂
[PROOFSTEP]
case succ s₁ hc₁ h => exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s₁ : Set α
hc₁ : ChainClosure r s₁
h : s₁ ⊆ c₂
⊢ SuccChain r s₁ ⊆ c₂
[PROOFSTEP]
exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id
[GOAL]
case union
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → a ⊆ c₂
⊢ ⋃₀ s✝ ⊆ c₂
[PROOFSTEP]
case union s _ ih => exact sUnion_subset ih
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s✝ t : Set α
a b x y : α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → a ⊆ c₂
⊢ ⋃₀ s ⊆ c₂
[PROOFSTEP]
case union s _ ih => exact sUnion_subset ih
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s✝ t : Set α
a b x y : α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → a ⊆ c₂
⊢ ⋃₀ s ⊆ c₂
[PROOFSTEP]
exact sUnion_subset ih
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc : ChainClosure r c
⊢ IsChain r c
[PROOFSTEP]
induction hc
[GOAL]
case succ
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
s✝ : Set α
a✝ : ChainClosure r s✝
a_ih✝ : IsChain r s✝
⊢ IsChain r (SuccChain r s✝)
case union
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → IsChain r a
⊢ IsChain r (⋃₀ s✝)
[PROOFSTEP]
case succ c _ h => exact h.succ
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ c₁ c₂ c₃ s t : Set α
a b x y : α
c : Set α
a✝ : ChainClosure r c
h : IsChain r c
⊢ IsChain r (SuccChain r c)
[PROOFSTEP]
case succ c _ h => exact h.succ
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ c₁ c₂ c₃ s t : Set α
a b x y : α
c : Set α
a✝ : ChainClosure r c
h : IsChain r c
⊢ IsChain r (SuccChain r c)
[PROOFSTEP]
exact h.succ
[GOAL]
case union
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → IsChain r a
⊢ IsChain r (⋃₀ s✝)
[PROOFSTEP]
case union s hs h =>
  exact fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq =>
    ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht => h t₁ ht₁ hc₁ (ht hc₂) hneq
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
hs : ∀ (a : Set α), a ∈ s → ChainClosure r a
h : ∀ (a : Set α), a ∈ s → IsChain r a
⊢ IsChain r (⋃₀ s)
[PROOFSTEP]
case union s hs h =>
  exact fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq =>
    ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht => h t₁ ht₁ hc₁ (ht hc₂) hneq
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
hs : ∀ (a : Set α), a ∈ s → ChainClosure r a
h : ∀ (a : Set α), a ∈ s → IsChain r a
⊢ IsChain r (⋃₀ s)
[PROOFSTEP]
exact fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq =>
  ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht => h t₁ ht₁ hc₁ (ht hc₂) hneq
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LE α
s✝ t✝ : Flag α
a : α
s t : Flag α
h : s.carrier = t.carrier
⊢ s = t
[PROOFSTEP]
cases s
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝ : LE α
s t✝ : Flag α
a : α
t : Flag α
carrier✝ : Set α
Chain'✝ : IsChain (fun x x_1 => x ≤ x_1) carrier✝
max_chain'✝ : ∀ ⦃s : Set α⦄, IsChain (fun x x_1 => x ≤ x_1) s → carrier✝ ⊆ s → carrier✝ = s
h : { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ } = t
[PROOFSTEP]
cases t
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝ : LE α
s t : Flag α
a : α
carrier✝¹ : Set α
Chain'✝¹ : IsChain (fun x x_1 => x ≤ x_1) carrier✝¹
max_chain'✝¹ : ∀ ⦃s : Set α⦄, IsChain (fun x x_1 => x ≤ x_1) s → carrier✝¹ ⊆ s → carrier✝¹ = s
carrier✝ : Set α
Chain'✝ : IsChain (fun x x_1 => x ≤ x_1) carrier✝
max_chain'✝ : ∀ ⦃s : Set α⦄, IsChain (fun x x_1 => x ≤ x_1) s → carrier✝ ⊆ s → carrier✝ = s
h :
  { carrier := carrier✝¹, Chain' := Chain'✝¹, max_chain' := max_chain'✝¹ }.carrier =
    { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ }.carrier
⊢ { carrier := carrier✝¹, Chain' := Chain'✝¹, max_chain' := max_chain'✝¹ } =
    { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ }
[PROOFSTEP]
congr