[GOAL]
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ GameAdd rα rβ x y ↔ rα x.fst y.fst ∧ x.snd = y.snd ∨ rβ x.snd y.snd ∧ x.fst = y.fst
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ GameAdd rα rβ x y → rα x.fst y.fst ∧ x.snd = y.snd ∨ rβ x.snd y.snd ∧ x.fst = y.fst
[PROOFSTEP]
rintro (@⟨a₁, a₂, b, h⟩ | @⟨a, b₁, b₂, h⟩)
[GOAL]
case mp.fst
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ : α
b : β
h : rα a₁ a₂
⊢ rα (a₁, b).fst (a₂, b).fst ∧ (a₁, b).snd = (a₂, b).snd ∨ rβ (a₁, b).snd (a₂, b).snd ∧ (a₁, b).fst = (a₂, b).fst
case mp.snd
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
a : α
b₁ b₂ : β
h : rβ b₁ b₂
⊢ rα (a, b₁).fst (a, b₂).fst ∧ (a, b₁).snd = (a, b₂).snd ∨ rβ (a, b₁).snd (a, b₂).snd ∧ (a, b₁).fst = (a, b₂).fst
[PROOFSTEP]
exacts [Or.inl ⟨h, rfl⟩, Or.inr ⟨h, rfl⟩]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ rα x.fst y.fst ∧ x.snd = y.snd ∨ rβ x.snd y.snd ∧ x.fst = y.fst → GameAdd rα rβ x y
[PROOFSTEP]
revert x y
[GOAL]
case mpr
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
⊢ ∀ {x y : α × β}, rα x.fst y.fst ∧ x.snd = y.snd ∨ rβ x.snd y.snd ∧ x.fst = y.fst → GameAdd rα rβ x y
[PROOFSTEP]
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (⟨h, rfl : b₁ = b₂⟩ | ⟨h, rfl : a₁ = a₂⟩)
[GOAL]
case mpr.mk.mk.inl.intro
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
a₁ : α
b₁ : β
a₂ : α
h : rα (a₁, b₁).fst (a₂, b₁).fst
⊢ GameAdd rα rβ (a₁, b₁) (a₂, b₁)
case mpr.mk.mk.inr.intro
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ✝ : β → β → Prop
rα : α → α → Prop
rβ : β → β → Prop
a₁ : α
b₁ b₂ : β
h : rβ (a₁, b₁).snd (a₁, b₂).snd
⊢ GameAdd rα rβ (a₁, b₁) (a₁, b₂)
[PROOFSTEP]
exacts [GameAdd.fst h, GameAdd.snd h]
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ GameAdd rβ rα (swap (a₁, b₁)) (swap (a₂, b₂)) ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
rw [Prod.swap, Prod.swap, gameAdd_mk_iff, gameAdd_mk_iff, or_comm]
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
⊢ ∀ {a₁ : α} {b₁ : β} {a₂ : α} {b₂ : β}, rα a₁ a₂ → rβ b₁ b₂ → Relation.TransGen (GameAdd rα rβ) (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
intro _ _ _ _ hα hβ
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
a₁✝ : α
b₁✝ : β
a₂✝ : α
b₂✝ : β
hα : rα a₁✝ a₂✝
hβ : rβ b₁✝ b₂✝
⊢ Relation.TransGen (GameAdd rα rβ) (a₁✝, b₁✝) (a₂✝, b₂✝)
[PROOFSTEP]
exact Relation.TransGen.tail (Relation.TransGen.single $ GameAdd.fst hα) (GameAdd.snd hβ)
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a : α
b : β
ha : Acc rα a
hb : Acc rβ b
⊢ Acc (Prod.GameAdd rα rβ) (a, b)
[PROOFSTEP]
induction' ha with a _ iha generalizing b
[GOAL]
case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ : α
b✝ : β
hb✝ : Acc rβ b✝
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b : β
hb : Acc rβ b
⊢ Acc (Prod.GameAdd rα rβ) (a, b)
[PROOFSTEP]
induction' hb with b hb ihb
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ : α
b✝¹ : β
hb✝ : Acc rβ b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b✝ b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
⊢ Acc (Prod.GameAdd rα rβ) (a, b)
[PROOFSTEP]
refine' Acc.intro _ fun h => _
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ : α
b✝¹ : β
hb✝ : Acc rβ b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b✝ b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
h : α × β
⊢ Prod.GameAdd rα rβ h (a, b) → Acc (Prod.GameAdd rα rβ) h
[PROOFSTEP]
rintro (⟨ra⟩ | ⟨rb⟩)
[GOAL]
case intro.intro.fst
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ : α
b✝¹ : β
hb✝ : Acc rβ b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b✝ b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
a₁✝ : α
ra : rα a₁✝ a
⊢ Acc (Prod.GameAdd rα rβ) (a₁✝, b)
case intro.intro.snd
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ : α
b✝¹ : β
hb✝ : Acc rβ b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b✝ b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
b₁✝ : β
rb : rβ b₁✝ b
⊢ Acc (Prod.GameAdd rα rβ) (a, b₁✝)
[PROOFSTEP]
exacts [iha _ ra (Acc.intro b hb), ihb _ rb]
[GOAL]
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ : β → β → Prop
rα : α → α → Prop
a₁ b₁ a₂ b₂ : α
⊢ (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂ b₂ =
      (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁ a₂ b₂ ∧
    (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂ b₂ =
      (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ b₂ a₂
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ : β → β → Prop
rα : α → α → Prop
a₁ b₁ a₂ b₂ : α
⊢ (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) ∧
    (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (a₁, b₁) (b₂, a₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (b₂, a₂))
[PROOFSTEP]
rw [Prod.gameAdd_swap_swap_mk _ _ b₁ b₂ a₁ a₂, Prod.gameAdd_swap_swap_mk _ _ a₁ b₂ b₁ a₂]
[GOAL]
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ : β → β → Prop
rα : α → α → Prop
a₁ b₁ a₂ b₂ : α
⊢ (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) ∧
    (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂))
[PROOFSTEP]
simp [or_comm]
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
⊢ ∀ {x y : α × α},
    GameAdd rα (Quotient.mk (Rel.setoid α) x) (Quotient.mk (Rel.setoid α) y) ↔
      Prod.GameAdd rα rα x y ∨ Prod.GameAdd rα rα (Prod.swap x) y
[PROOFSTEP]
rintro ⟨_, _⟩ ⟨_, _⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
fst✝¹ snd✝¹ fst✝ snd✝ : α
⊢ GameAdd rα (Quotient.mk (Rel.setoid α) (fst✝¹, snd✝¹)) (Quotient.mk (Rel.setoid α) (fst✝, snd✝)) ↔
    Prod.GameAdd rα rα (fst✝¹, snd✝¹) (fst✝, snd✝) ∨ Prod.GameAdd rα rα (Prod.swap (fst✝¹, snd✝¹)) (fst✝, snd✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα (Quotient.mk (Rel.setoid α) (a₁, b)) (Quotient.mk (Rel.setoid α) (b, a₂))
[PROOFSTEP]
rw [Sym2.eq_swap]
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα (Quotient.mk (Rel.setoid α) (b, a₁)) (Quotient.mk (Rel.setoid α) (b, a₂))
[PROOFSTEP]
exact GameAdd.snd h
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα (Quotient.mk (Rel.setoid α) (b, a₁)) (Quotient.mk (Rel.setoid α) (a₂, b))
[PROOFSTEP]
rw [Sym2.eq_swap]
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα (Quotient.mk (Rel.setoid α) (a₁, b)) (Quotient.mk (Rel.setoid α) (a₂, b))
[PROOFSTEP]
exact GameAdd.fst h
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a b : α
ha : Acc rα a
hb : Acc rα b
⊢ Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, b))
[PROOFSTEP]
induction' ha with a _ iha generalizing b
[GOAL]
case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝ : α
hb✝ : Acc rα b✝
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b : α
hb : Acc rα b
⊢ Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, b))
[PROOFSTEP]
induction' hb with b hb ihb
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
⊢ Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, b))
[PROOFSTEP]
refine' Acc.intro _ fun s => _
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
s : Sym2 α
⊢ Sym2.GameAdd rα s (Quotient.mk (Sym2.Rel.setoid α) (a, b)) → Acc (Sym2.GameAdd rα) s
[PROOFSTEP]
induction' s using Sym2.inductionOn with c d
[GOAL]
case intro.intro.hf
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
c d : α
⊢ Sym2.GameAdd rα (Quotient.mk (Sym2.Rel.setoid α) (c, d)) (Quotient.mk (Sym2.Rel.setoid α) (a, b)) →
    Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (c, d))
[PROOFSTEP]
rw [Sym2.GameAdd]
[GOAL]
case intro.intro.hf
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
c d : α
⊢ ↑Sym2.lift₂
      { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
        property :=
          (_ :
            ∀ (a₁ b₁ a₂ b₂ : α),
              (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂
                    b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁
                    a₂ b₂ ∧
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    a₂ b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    b₂ a₂) }
      (Quotient.mk (Sym2.Rel.setoid α) (c, d)) (Quotient.mk (Sym2.Rel.setoid α) (a, b)) →
    Acc
      (↑Sym2.lift₂
        { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
          property :=
            (_ :
              ∀ (a₁ b₁ a₂ b₂ : α),
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                      a₂ b₂ =
                    (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁
                      a₁ a₂ b₂ ∧
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                      a₂ b₂ =
                    (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁
                      b₁ b₂ a₂) })
      (Quotient.mk (Sym2.Rel.setoid α) (c, d))
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.hf
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
c d : α
⊢ Prod.GameAdd rα rα (c, d) (a, b) ∨ Prod.GameAdd rα rα (d, c) (a, b) →
    Acc
      (↑Sym2.lift₂
        { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
          property :=
            (_ :
              ∀ (a₁ b₁ a₂ b₂ : α),
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                      a₂ b₂ =
                    (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁
                      a₁ a₂ b₂ ∧
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                      a₂ b₂ =
                    (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁
                      b₁ b₂ a₂) })
      (Quotient.mk (Sym2.Rel.setoid α) (c, d))
[PROOFSTEP]
rintro ((rc | rd) | (rd | rc))
[GOAL]
case intro.intro.hf.inl.fst
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
c : α
rc : rα c a
⊢ Acc
    (↑Sym2.lift₂
      { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
        property :=
          (_ :
            ∀ (a₁ b₁ a₂ b₂ : α),
              (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂
                    b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁
                    a₂ b₂ ∧
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    a₂ b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    b₂ a₂) })
    (Quotient.mk (Sym2.Rel.setoid α) (c, b))
[PROOFSTEP]
exact iha c rc ⟨b, hb⟩
[GOAL]
case intro.intro.hf.inl.snd
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
d : α
rd : rα d b
⊢ Acc
    (↑Sym2.lift₂
      { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
        property :=
          (_ :
            ∀ (a₁ b₁ a₂ b₂ : α),
              (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂
                    b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁
                    a₂ b₂ ∧
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    a₂ b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    b₂ a₂) })
    (Quotient.mk (Sym2.Rel.setoid α) (a, d))
[PROOFSTEP]
exact ihb d rd
[GOAL]
case intro.intro.hf.inr.fst
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
d : α
rd : rα d a
⊢ Acc
    (↑Sym2.lift₂
      { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
        property :=
          (_ :
            ∀ (a₁ b₁ a₂ b₂ : α),
              (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂
                    b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁
                    a₂ b₂ ∧
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    a₂ b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    b₂ a₂) })
    (Quotient.mk (Sym2.Rel.setoid α) (b, d))
[PROOFSTEP]
rw [Sym2.eq_swap]
[GOAL]
case intro.intro.hf.inr.fst
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
d : α
rd : rα d a
⊢ Acc
    (↑Sym2.lift₂
      { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
        property :=
          (_ :
            ∀ (a₁ b₁ a₂ b₂ : α),
              (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂
                    b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁
                    a₂ b₂ ∧
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    a₂ b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    b₂ a₂) })
    (Quotient.mk (Sym2.Rel.setoid α) (d, b))
[PROOFSTEP]
exact iha d rd ⟨b, hb⟩
[GOAL]
case intro.intro.hf.inr.snd
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
c : α
rc : rα c b
⊢ Acc
    (↑Sym2.lift₂
      { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
        property :=
          (_ :
            ∀ (a₁ b₁ a₂ b₂ : α),
              (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂
                    b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁
                    a₂ b₂ ∧
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    a₂ b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    b₂ a₂) })
    (Quotient.mk (Sym2.Rel.setoid α) (c, a))
[PROOFSTEP]
rw [Sym2.eq_swap]
[GOAL]
case intro.intro.hf.inr.snd
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ b✝¹ : α
hb✝ : Acc rα b✝¹
a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (y, b))
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) (Quotient.mk (Sym2.Rel.setoid α) (a, y))
c : α
rc : rα c b
⊢ Acc
    (↑Sym2.lift₂
      { val := fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
        property :=
          (_ :
            ∀ (a₁ b₁ a₂ b₂ : α),
              (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂
                    b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁
                    a₂ b₂ ∧
                (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    a₂ b₂ =
                  (fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁
                    b₂ a₂) })
    (Quotient.mk (Sym2.Rel.setoid α) (a, c))
[PROOFSTEP]
exact ihb c rc
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
C : α → α → Sort u_3
hr : WellFounded rα
IH :
  (a₁ b₁ : α) →
    ((a₂ b₂ : α) → GameAdd rα (Quotient.mk (Rel.setoid α) (a₂, b₂)) (Quotient.mk (Rel.setoid α) (a₁, b₁)) → C a₂ b₂) →
      C a₁ b₁
a b : α
⊢ C a b
[PROOFSTEP]
have := hr.sym2_gameAdd
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
C : α → α → Sort u_3
hr : WellFounded rα
IH :
  (a₁ b₁ : α) →
    ((a₂ b₂ : α) → GameAdd rα (Quotient.mk (Rel.setoid α) (a₂, b₂)) (Quotient.mk (Rel.setoid α) (a₁, b₁)) → C a₂ b₂) →
      C a₁ b₁
a b : α
this : WellFounded (GameAdd rα)
⊢ C a b
[PROOFSTEP]
dsimp only [GameAdd, lift₂, FunLike.coe, EquivLike.coe] at this
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
C : α → α → Sort u_3
hr : WellFounded rα
IH :
  (a₁ b₁ : α) →
    ((a₂ b₂ : α) → GameAdd rα (Quotient.mk (Rel.setoid α) (a₂, b₂)) (Quotient.mk (Rel.setoid α) (a₁, b₁)) → C a₂ b₂) →
      C a₁ b₁
a b : α
this :
  WellFounded
    (Quotient.lift₂
      (fun a b => Prod.GameAdd rα rα (a.fst, a.snd) (b.fst, b.snd) ∨ Prod.GameAdd rα rα (a.snd, a.fst) (b.fst, b.snd))
      (_ :
        ∀ (a₁ b₁ a₂ b₂ : α × α),
          a₁ ≈ a₂ →
            b₁ ≈ b₂ →
              (fun a b =>
                    ↑{
                          val := fun a₁ b₁ a₂ b₂ =>
                            Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
                          property :=
                            (_ :
                              ∀ (a₁ b₁ a₂ b₂ : α),
                                (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      a₁ b₁ a₂ b₂ =
                                    (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      b₁ a₁ a₂ b₂ ∧
                                  (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      a₁ b₁ a₂ b₂ =
                                    (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      a₁ b₁ b₂ a₂) }
                      a.fst a.snd b.fst b.snd)
                  a₁ b₁ =
                (fun a b =>
                    ↑{
                          val := fun a₁ b₁ a₂ b₂ =>
                            Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂),
                          property :=
                            (_ :
                              ∀ (a₁ b₁ a₂ b₂ : α),
                                (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      a₁ b₁ a₂ b₂ =
                                    (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      b₁ a₁ a₂ b₂ ∧
                                  (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      a₁ b₁ a₂ b₂ =
                                    (fun a₁ b₁ a₂ b₂ =>
                                        Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂))
                                      a₁ b₁ b₂ a₂) }
                      a.fst a.snd b.fst b.snd)
                  a₂ b₂))
⊢ C a b
[PROOFSTEP]
exact
  @WellFounded.fix (α × α) (fun x => C x.1 x.2) _ this.of_quotient_lift₂
    (fun ⟨x₁, x₂⟩ IH' => IH x₁ x₂ fun a' b' => IH' ⟨a', b'⟩) (a, b)
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
C : α → α → Sort u_3
hr : WellFounded rα
IH :
  (a₁ b₁ : α) →
    ((a₂ b₂ : α) → GameAdd rα (Quotient.mk (Rel.setoid α) (a₂, b₂)) (Quotient.mk (Rel.setoid α) (a₁, b₁)) → C a₂ b₂) →
      C a₁ b₁
a b : α
⊢ fix hr IH a b = IH a b fun a' b' x => fix hr IH a' b'
[PROOFSTEP]
dsimp [GameAdd.fix]
[GOAL]
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
C : α → α → Sort u_3
hr : WellFounded rα
IH :
  (a₁ b₁ : α) →
    ((a₂ b₂ : α) → GameAdd rα (Quotient.mk (Rel.setoid α) (a₂, b₂)) (Quotient.mk (Rel.setoid α) (a₁, b₁)) → C a₂ b₂) →
      C a₁ b₁
a b : α
⊢ WellFounded.fix
      (_ :
        WellFounded fun a b =>
          Prod.GameAdd rα rα (a.fst, a.snd) (b.fst, b.snd) ∨ Prod.GameAdd rα rα (a.snd, a.fst) (b.fst, b.snd))
      (fun x IH' => IH x.fst x.snd fun a' b' => IH' (a', b')) (a, b) =
    IH a b fun a' b' x =>
      WellFounded.fix
        (_ :
          WellFounded fun a b =>
            Prod.GameAdd rα rα (a.fst, a.snd) (b.fst, b.snd) ∨ Prod.GameAdd rα rα (a.snd, a.fst) (b.fst, b.snd))
        (fun x IH' => IH x.fst x.snd fun a' b' => IH' (a', b')) (a', b')
[PROOFSTEP]
exact WellFounded.fix_eq _ _ _


[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
⊢ min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a
[PROOFSTEP]
by_cases h : a ≤ b
[GOAL]
case pos
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a
[PROOFSTEP]
left
[GOAL]
case pos.h
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ min a b = a ∧ a ≤ b
[PROOFSTEP]
exact ⟨min_eq_left h, h⟩
[GOAL]
case neg
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : ¬a ≤ b
⊢ min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a
[PROOFSTEP]
right
[GOAL]
case neg.h
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : ¬a ≤ b
⊢ min a b = b ∧ b < a
[PROOFSTEP]
exact ⟨min_eq_right (le_of_lt (not_le.mp h)), not_le.mp h⟩
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ min a b = c ↔ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ min a b = c → a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
h : min a b = c
⊢ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a
[PROOFSTEP]
refine' Or.imp (fun h' => _) (fun h' => _) (le_total a b)
[GOAL]
case mp.refine'_1
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
h : min a b = c
h' : a ≤ b
⊢ a = c ∧ a ≤ b
[PROOFSTEP]
exact ⟨by simpa [h'] using h, h'⟩
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
h : min a b = c
h' : a ≤ b
⊢ a = c
[PROOFSTEP]
simpa [h'] using h
[GOAL]
case mp.refine'_2
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
h : min a b = c
h' : b ≤ a
⊢ b = c ∧ b ≤ a
[PROOFSTEP]
exact ⟨by simpa [h'] using h, h'⟩
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
h : min a b = c
h' : b ≤ a
⊢ b = c
[PROOFSTEP]
simpa [h'] using h
[GOAL]
case mpr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a → min a b = c
[PROOFSTEP]
rintro (⟨rfl, h⟩ | ⟨rfl, h⟩)
[GOAL]
case mpr.inl.intro
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b d : α
h : a ≤ b
⊢ min a b = a
[PROOFSTEP]
simp [h]
[GOAL]
case mpr.inr.intro
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b d : α
h : b ≤ a
⊢ min a b = b
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ min a c < min b c ↔ a < b ∧ a < c
[PROOFSTEP]
simp_rw [lt_min_iff, min_lt_iff, or_iff_left (lt_irrefl _)]
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ (a < b ∨ c < b) ∧ a < c ↔ a < b ∧ a < c
[PROOFSTEP]
exact and_congr_left fun h => or_iff_left_of_imp h.trans
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ min a b < min a c ↔ b < c ∧ b < a
[PROOFSTEP]
simp_rw [min_comm a, min_lt_min_left_iff]
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ ∀ (a : α), max a a = a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ ∀ (a : α), min a a = a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
⊢ f (max a b) = max (f a) (f b)
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
h : a ≤ b
⊢ f (max a b) = max (f a) (f b)
[PROOFSTEP]
simp only [max_eq_right, max_eq_left, hf ha hb, hf hb ha, h]
[GOAL]
case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
h : b ≤ a
⊢ f (max a b) = max (f a) (f b)
[PROOFSTEP]
simp only [max_eq_right, max_eq_left, hf ha hb, hf hb ha, h]
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : Monotone f
⊢ f (max a b) = max (f a) (f b)
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : Monotone f
h : a ≤ b
⊢ f (max a b) = max (f a) (f b)
[PROOFSTEP]
simp [h, hf h]
[GOAL]
case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : Monotone f
h : b ≤ a
⊢ f (max a b) = max (f a) (f b)
[PROOFSTEP]
simp [h, hf h]
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : Antitone f
⊢ f (max a b) = min (f a) (f b)
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : Antitone f
h : a ≤ b
⊢ f (max a b) = min (f a) (f b)
[PROOFSTEP]
simp [h, hf h]
[GOAL]
case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : Antitone f
h : b ≤ a
⊢ f (max a b) = min (f a) (f b)
[PROOFSTEP]
simp [h, hf h]
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
⊢ min a b = a ∨ min a b = b
[PROOFSTEP]
cases le_total a b
[GOAL]
case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h✝ : a ≤ b
⊢ min a b = a ∨ min a b = b
[PROOFSTEP]
simp [*]
[GOAL]
case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h✝ : b ≤ a
⊢ min a b = a ∨ min a b = b
[PROOFSTEP]
simp [*]


[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f g : M ↪ₑ[L] N
h : (fun f => ↑f) f = (fun f => ↑f) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
g : M ↪ₑ[L] N
toFun✝ : M → N
map_formula'✝ : ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝ ∘ x) ↔ Formula.Realize φ x
h : (fun f => ↑f) (mk toFun✝) = (fun f => ↑f) g
⊢ mk toFun✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
toFun✝¹ : M → N
map_formula'✝¹ :
  ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝¹ ∘ x) ↔ Formula.Realize φ x
toFun✝ : M → N
map_formula'✝ : ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝ ∘ x) ↔ Formula.Realize φ x
h : (fun f => ↑f) (mk toFun✝¹) = (fun f => ↑f) (mk toFun✝)
⊢ mk toFun✝¹ = mk toFun✝
[PROOFSTEP]
simp only [ElementaryEmbedding.mk.injEq]
[GOAL]
case mk.mk
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
toFun✝¹ : M → N
map_formula'✝¹ :
  ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝¹ ∘ x) ↔ Formula.Realize φ x
toFun✝ : M → N
map_formula'✝ : ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝ ∘ x) ↔ Formula.Realize φ x
h : (fun f => ↑f) (mk toFun✝¹) = (fun f => ↑f) (mk toFun✝)
⊢ toFun✝¹ = toFun✝
[PROOFSTEP]
ext x
[GOAL]
case mk.mk.h
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
toFun✝¹ : M → N
map_formula'✝¹ :
  ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝¹ ∘ x) ↔ Formula.Realize φ x
toFun✝ : M → N
map_formula'✝ : ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝ ∘ x) ↔ Formula.Realize φ x
h : (fun f => ↑f) (mk toFun✝¹) = (fun f => ↑f) (mk toFun✝)
x : M
⊢ toFun✝¹ x = toFun✝ x
[PROOFSTEP]
exact Function.funext_iff.1 h x
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize φ (↑f ∘ v) (↑f ∘ xs) ↔ BoundedFormula.Realize φ v xs
[PROOFSTEP]
classical
rw [← BoundedFormula.realize_restrictFreeVar Set.Subset.rfl, Set.inclusion_eq_id, iff_eq_eq]
have h :=
  f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _))
    (Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm)
simp only [Formula.realize_relabel, BoundedFormula.realize_toFormula, iff_eq_eq] at h
rw [← Function.comp.assoc _ _ (Fintype.equivFin _).symm,
  Function.comp.assoc _ (Fintype.equivFin _).symm (Fintype.equivFin _), Equiv.symm_comp_self, Function.comp.right_id,
  Function.comp.assoc, Sum.elim_comp_inl, Function.comp.assoc _ _ Sum.inr, Sum.elim_comp_inr, ← Function.comp.assoc] at
  h
refine' h.trans _
erw [Function.comp.assoc _ _ (Fintype.equivFin _), Equiv.symm_comp_self, Function.comp.right_id, Sum.elim_comp_inl,
  Sum.elim_comp_inr (v ∘ Subtype.val) xs, ←
  Set.inclusion_eq_id (s := (BoundedFormula.freeVarFinset φ : Set α)) Set.Subset.rfl,
  BoundedFormula.realize_restrictFreeVar Set.Subset.rfl]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize φ (↑f ∘ v) (↑f ∘ xs) ↔ BoundedFormula.Realize φ v xs
[PROOFSTEP]
rw [← BoundedFormula.realize_restrictFreeVar Set.Subset.rfl, Set.inclusion_eq_id, iff_eq_eq]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id) ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    BoundedFormula.Realize φ v xs
[PROOFSTEP]
have h :=
  f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _))
    (Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm)
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
h :
  Formula.Realize
      (Formula.relabel (↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)))
        (BoundedFormula.toFormula (BoundedFormula.restrictFreeVar φ id)))
      (↑f ∘
        Sum.elim (v ∘ Subtype.val) xs ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ↔
    Formula.Realize
      (Formula.relabel (↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)))
        (BoundedFormula.toFormula (BoundedFormula.restrictFreeVar φ id)))
      (Sum.elim (v ∘ Subtype.val) xs ∘ ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm)
⊢ BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id) ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    BoundedFormula.Realize φ v xs
[PROOFSTEP]
simp only [Formula.realize_relabel, BoundedFormula.realize_toFormula, iff_eq_eq] at h
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
h :
  BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id)
      (((↑f ∘
            Sum.elim (v ∘ Subtype.val) xs ∘
              ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inl)
      (((↑f ∘
            Sum.elim (v ∘ Subtype.val) xs ∘
              ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inr) =
    BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inr)
⊢ BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id) ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    BoundedFormula.Realize φ v xs
[PROOFSTEP]
rw [← Function.comp.assoc _ _ (Fintype.equivFin _).symm,
  Function.comp.assoc _ (Fintype.equivFin _).symm (Fintype.equivFin _), Equiv.symm_comp_self, Function.comp.right_id,
  Function.comp.assoc, Sum.elim_comp_inl, Function.comp.assoc _ _ Sum.inr, Sum.elim_comp_inr, ← Function.comp.assoc] at
  h
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
h :
  BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id) ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inr)
⊢ BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id) ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    BoundedFormula.Realize φ v xs
[PROOFSTEP]
refine' h.trans _
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
h :
  BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id) ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inr)
⊢ BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inr) =
    BoundedFormula.Realize φ v xs
[PROOFSTEP]
erw [Function.comp.assoc _ _ (Fintype.equivFin _), Equiv.symm_comp_self, Function.comp.right_id, Sum.elim_comp_inl,
  Sum.elim_comp_inr (v ∘ Subtype.val) xs, ←
  Set.inclusion_eq_id (s := (BoundedFormula.freeVarFinset φ : Set α)) Set.Subset.rfl,
  BoundedFormula.realize_restrictFreeVar Set.Subset.rfl]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
φ : Formula L α
x : α → M
⊢ Formula.Realize φ (↑f ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
rw [Formula.Realize, Formula.Realize, ← f.map_boundedFormula, Unique.eq_default (f ∘ default)]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
φ : Sentence L
⊢ M ⊨ φ ↔ N ⊨ φ
[PROOFSTEP]
rw [Sentence.Realize, Sentence.Realize, ← f.map_formula, Unique.eq_default (f ∘ default)]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
T : Theory L
⊢ M ⊨ T ↔ N ⊨ T
[PROOFSTEP]
simp only [Theory.model_iff, f.map_sentence]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
⊢ Function.Injective ↑φ
[PROOFSTEP]
intro x y
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
x y : M
⊢ ↑φ x = ↑φ y → x = y
[PROOFSTEP]
have h := φ.map_formula ((var 0).equal (var 1) : L.Formula (Fin 2)) fun i => if i = 0 then x else y
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
x y : M
h :
  Formula.Realize (Term.equal (var 0) (var 1)) (↑φ ∘ fun i => if i = 0 then x else y) ↔
    Formula.Realize (Term.equal (var 0) (var 1)) fun i => if i = 0 then x else y
⊢ ↑φ x = ↑φ y → x = y
[PROOFSTEP]
rw [Formula.realize_equal, Formula.realize_equal] at h
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
x y : M
h :
  Term.realize (↑φ ∘ fun i => if i = 0 then x else y) (var 0) =
      Term.realize (↑φ ∘ fun i => if i = 0 then x else y) (var 1) ↔
    Term.realize (fun i => if i = 0 then x else y) (var 0) = Term.realize (fun i => if i = 0 then x else y) (var 1)
⊢ ↑φ x = ↑φ y → x = y
[PROOFSTEP]
simp only [Nat.one_ne_zero, Term.realize, Fin.one_eq_zero_iff, if_true, eq_self_iff_true, Function.comp_apply,
  if_false] at h
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
x y : M
h : ↑φ x = ↑φ y ↔ x = y
⊢ ↑φ x = ↑φ y → x = y
[PROOFSTEP]
exact h.1
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
n : ℕ
f : Functions L n
x : Fin n → M
⊢ ↑φ (funMap f x) = funMap f (↑φ ∘ x)
[PROOFSTEP]
have h := φ.map_formula (Formula.graph f) (Fin.cons (funMap f x) x)
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
n : ℕ
f : Functions L n
x : Fin n → M
h :
  Formula.Realize (Formula.graph f) (↑φ ∘ Fin.cons (funMap f x) x) ↔
    Formula.Realize (Formula.graph f) (Fin.cons (funMap f x) x)
⊢ ↑φ (funMap f x) = funMap f (↑φ ∘ x)
[PROOFSTEP]
rw [Formula.realize_graph, Fin.comp_cons, Formula.realize_graph] at h
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
n : ℕ
f : Functions L n
x : Fin n → M
h : funMap f (↑φ ∘ x) = ↑φ (funMap f x) ↔ funMap f x = funMap f x
⊢ ↑φ (funMap f x) = funMap f (↑φ ∘ x)
[PROOFSTEP]
rw [eq_comm, h]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f✝ : M ↪ₑ[L] N
x✝ : ℕ
f : Functions L x✝
x : Fin x✝ → M
⊢ Function.Embedding.toFun { toFun := ↑f✝, inj' := (_ : Function.Injective ↑f✝) } (funMap f x) =
    funMap f ({ toFun := ↑f✝, inj' := (_ : Function.Injective ↑f✝) }.toFun ∘ x)
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
x✝ : ℕ
R : Relations L x✝
x : Fin x✝ → M
⊢ RelMap R ({ toFun := ↑f, inj' := (_ : Function.Injective ↑f) }.toFun ∘ x) ↔ RelMap R x
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f✝ : M ↪ₑ[L] N
x✝ : ℕ
f : Functions L x✝
x : Fin x✝ → M
⊢ ↑f✝ (funMap f x) = funMap f (↑f✝ ∘ x)
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
x✝ : ℕ
R : Relations L x✝
x : Fin x✝ → M
⊢ RelMap R x → RelMap R (↑f ∘ x)
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
hnp : N ↪ₑ[L] P
hmn : M ↪ₑ[L] N
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
⊢ Formula.Realize φ ((↑hnp ∘ ↑hmn) ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
cases' hnp with _ hhnp
[GOAL]
case mk
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
hmn : M ↪ₑ[L] N
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
toFun✝ : N → P
hhnp : ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → N), Formula.Realize φ (toFun✝ ∘ x) ↔ Formula.Realize φ x
⊢ Formula.Realize φ ((↑(mk toFun✝) ∘ ↑hmn) ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
cases' hmn with _ hhmn
[GOAL]
case mk.mk
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
toFun✝¹ : N → P
hhnp : ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → N), Formula.Realize φ (toFun✝¹ ∘ x) ↔ Formula.Realize φ x
toFun✝ : M → N
hhmn : ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝ ∘ x) ↔ Formula.Realize φ x
⊢ Formula.Realize φ ((↑(mk toFun✝¹) ∘ ↑(mk toFun✝)) ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
erw [hhnp, hhmn]
[GOAL]
L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : Structure L M
inst✝⁶ : Structure L N✝
inst✝⁵ : Structure L P
inst✝⁴ : Structure L Q
N : Type u_5
inst✝³ : Structure L N
inst✝² : Structure (L[[M]]) N
inst✝¹ : LHom.IsExpansionOn (lhomWithConstants L M) N
inst✝ : N ⊨ elementaryDiagram L M
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
⊢ Formula.Realize φ ((constantMap ∘ Sum.inr) ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
refine'
  _root_.trans _
    ((realize_iff_of_model_completeTheory M N
          (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)).alls).trans
      _)
[GOAL]
case refine'_1
L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : Structure L M
inst✝⁶ : Structure L N✝
inst✝⁵ : Structure L P
inst✝⁴ : Structure L Q
N : Type u_5
inst✝³ : Structure L N
inst✝² : Structure (L[[M]]) N
inst✝¹ : LHom.IsExpansionOn (lhomWithConstants L M) N
inst✝ : N ⊨ elementaryDiagram L M
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
⊢ Formula.Realize φ ((constantMap ∘ Sum.inr) ∘ x) ↔
    N ⊨
      BoundedFormula.alls
        (BoundedFormula.subst (LHom.onBoundedFormula (lhomWithConstants L M) φ) (Constants.term ∘ Sum.inr ∘ x))
[PROOFSTEP]
simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst, LHom.realize_onBoundedFormula,
  Formula.Realize, Unique.forall_iff, Function.comp, Term.realize_constants]
[GOAL]
case refine'_2
L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : Structure L M
inst✝⁶ : Structure L N✝
inst✝⁵ : Structure L P
inst✝⁴ : Structure L Q
N : Type u_5
inst✝³ : Structure L N
inst✝² : Structure (L[[M]]) N
inst✝¹ : LHom.IsExpansionOn (lhomWithConstants L M) N
inst✝ : N ⊨ elementaryDiagram L M
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
⊢ M ⊨
      BoundedFormula.alls
        (BoundedFormula.subst (LHom.onBoundedFormula (lhomWithConstants L M) φ) (Constants.term ∘ Sum.inr ∘ x)) ↔
    Formula.Realize φ x
[PROOFSTEP]
simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst, LHom.realize_onBoundedFormula,
  Formula.Realize, Unique.forall_iff]
[GOAL]
case refine'_2
L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : Structure L M
inst✝⁶ : Structure L N✝
inst✝⁵ : Structure L P
inst✝⁴ : Structure L Q
N : Type u_5
inst✝³ : Structure L N
inst✝² : Structure (L[[M]]) N
inst✝¹ : LHom.IsExpansionOn (lhomWithConstants L M) N
inst✝ : N ⊨ elementaryDiagram L M
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
⊢ BoundedFormula.Realize φ (fun a => Term.realize default ((Constants.term ∘ Sum.inr ∘ x) a)) default ↔
    BoundedFormula.Realize φ x default
[PROOFSTEP]
rfl
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
⊢ ∀ {n : ℕ} (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (↑f ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
suffices h :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M), φ.Realize (f ∘ default) (f ∘ xs) ↔ φ.Realize default xs
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
h :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty n) (xs : Fin n → M),
    BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
⊢ ∀ {n : ℕ} (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (↑f ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
intro n φ x
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
h :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty n) (xs : Fin n → M),
    BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
⊢ Formula.Realize φ (↑f ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
refine' φ.realize_relabel_sum_inr.symm.trans (_root_.trans (h n _ _) φ.realize_relabel_sum_inr)
[GOAL]
case h
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
⊢ ∀ (n : ℕ) (φ : BoundedFormula L Empty n) (xs : Fin n → M),
    BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
[PROOFSTEP]
refine' fun n φ => φ.recOn _ _ _ _ _
[GOAL]
case h.refine'_1
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
⊢ ∀ {n : ℕ} (xs : Fin n → M),
    BoundedFormula.Realize BoundedFormula.falsum (↑f ∘ default) (↑f ∘ xs) ↔
      BoundedFormula.Realize BoundedFormula.falsum default xs
[PROOFSTEP]
exact fun {_} _ => Iff.rfl
[GOAL]
case h.refine'_2
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
⊢ ∀ {n : ℕ} (t₁ t₂ : Term L (Empty ⊕ Fin n)) (xs : Fin n → M),
    BoundedFormula.Realize (BoundedFormula.equal t₁ t₂) (↑f ∘ default) (↑f ∘ xs) ↔
      BoundedFormula.Realize (BoundedFormula.equal t₁ t₂) default xs
[PROOFSTEP]
intros
[GOAL]
case h.refine'_2
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
n✝ : ℕ
t₁✝ t₂✝ : Term L (Empty ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ BoundedFormula.Realize (BoundedFormula.equal t₁✝ t₂✝) (↑f ∘ default) (↑f ∘ xs✝) ↔
    BoundedFormula.Realize (BoundedFormula.equal t₁✝ t₂✝) default xs✝
[PROOFSTEP]
simp [BoundedFormula.Realize, ← Sum.comp_elim, Embedding.realize_term]
[GOAL]
case h.refine'_3
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
⊢ ∀ {n l : ℕ} (R : Relations L l) (ts : Fin l → Term L (Empty ⊕ Fin n)) (xs : Fin n → M),
    BoundedFormula.Realize (BoundedFormula.rel R ts) (↑f ∘ default) (↑f ∘ xs) ↔
      BoundedFormula.Realize (BoundedFormula.rel R ts) default xs
[PROOFSTEP]
intros
[GOAL]
case h.refine'_3
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (Empty ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ BoundedFormula.Realize (BoundedFormula.rel R✝ ts✝) (↑f ∘ default) (↑f ∘ xs✝) ↔
    BoundedFormula.Realize (BoundedFormula.rel R✝ ts✝) default xs✝
[PROOFSTEP]
simp [BoundedFormula.Realize, ← Sum.comp_elim, Embedding.realize_term]
[GOAL]
case h.refine'_3
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (Empty ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ (RelMap R✝ fun i => ↑f (Term.realize (Sum.elim default xs✝) (ts✝ i))) ↔
    RelMap R✝ fun i => Term.realize (Sum.elim default xs✝) (ts✝ i)
[PROOFSTEP]
erw [map_rel f]
[GOAL]
case h.refine'_4
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
⊢ ∀ {n : ℕ} (f₁ f₂ : BoundedFormula L Empty n),
    (∀ (xs : Fin n → M), BoundedFormula.Realize f₁ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize f₁ default xs) →
      (∀ (xs : Fin n → M), BoundedFormula.Realize f₂ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize f₂ default xs) →
        ∀ (xs : Fin n → M),
          BoundedFormula.Realize (f₁ ⟹ f₂) (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize (f₁ ⟹ f₂) default xs
[PROOFSTEP]
intro _ _ _ ih1 ih2 _
[GOAL]
case h.refine'_4
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L Empty n✝
ih1 : ∀ (xs : Fin n✝ → M), BoundedFormula.Realize f₁✝ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize f₁✝ default xs
ih2 : ∀ (xs : Fin n✝ → M), BoundedFormula.Realize f₂✝ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize f₂✝ default xs
xs✝ : Fin n✝ → M
⊢ BoundedFormula.Realize (f₁✝ ⟹ f₂✝) (↑f ∘ default) (↑f ∘ xs✝) ↔ BoundedFormula.Realize (f₁✝ ⟹ f₂✝) default xs✝
[PROOFSTEP]
simp [ih1, ih2]
[GOAL]
case h.refine'_5
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
⊢ ∀ {n : ℕ} (f_1 : BoundedFormula L Empty (n + 1)),
    (∀ (xs : Fin (n + 1) → M),
        BoundedFormula.Realize f_1 (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize f_1 default xs) →
      ∀ (xs : Fin n → M),
        BoundedFormula.Realize (∀'f_1) (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize (∀'f_1) default xs
[PROOFSTEP]
intro n φ ih xs
[GOAL]
case h.refine'_5
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
⊢ BoundedFormula.Realize (∀'φ) (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize (∀'φ) default xs
[PROOFSTEP]
simp only [BoundedFormula.realize_all]
[GOAL]
case h.refine'_5
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
⊢ (∀ (a : N), BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)) ↔
    ∀ (a : M), BoundedFormula.Realize φ default (Fin.snoc xs a)
[PROOFSTEP]
refine' ⟨fun h a => _, _⟩
[GOAL]
case h.refine'_5.refine'_1
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
h : ∀ (a : N), BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
a : M
⊢ BoundedFormula.Realize φ default (Fin.snoc xs a)
[PROOFSTEP]
rw [← ih, Fin.comp_snoc]
[GOAL]
case h.refine'_5.refine'_1
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
h : ∀ (a : N), BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
a : M
⊢ BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) (↑f a))
[PROOFSTEP]
exact h (f a)
[GOAL]
case h.refine'_5.refine'_2
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
⊢ (∀ (a : M), BoundedFormula.Realize φ default (Fin.snoc xs a)) →
    ∀ (a : N), BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
[PROOFSTEP]
contrapose!
[GOAL]
case h.refine'_5.refine'_2
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
⊢ (∃ a, ¬BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)) →
    ∃ a, ¬BoundedFormula.Realize φ default (Fin.snoc xs a)
[PROOFSTEP]
rintro ⟨a, ha⟩
[GOAL]
case h.refine'_5.refine'_2.intro
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
a : N
ha : ¬BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
⊢ ∃ a, ¬BoundedFormula.Realize φ default (Fin.snoc xs a)
[PROOFSTEP]
obtain ⟨b, hb⟩ :=
  htv n φ.not xs a
    (by
      rw [BoundedFormula.realize_not, ← Unique.eq_default (f ∘ default)]
      exact ha)
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
a : N
ha : ¬BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
⊢ BoundedFormula.Realize (∼φ) default (Fin.snoc (↑f ∘ xs) a)
[PROOFSTEP]
rw [BoundedFormula.realize_not, ← Unique.eq_default (f ∘ default)]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
a : N
ha : ¬BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
⊢ ¬BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
[PROOFSTEP]
exact ha
[GOAL]
case h.refine'_5.refine'_2.intro.intro
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
a : N
ha : ¬BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
b : M
hb : BoundedFormula.Realize (∼φ) default (Fin.snoc (↑f ∘ xs) (↑f b))
⊢ ∃ a, ¬BoundedFormula.Realize φ default (Fin.snoc xs a)
[PROOFSTEP]
refine' ⟨b, fun h => hb (Eq.mp _ ((ih _).2 h))⟩
[GOAL]
case h.refine'_5.refine'_2.intro.intro
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
a : N
ha : ¬BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
b : M
hb : BoundedFormula.Realize (∼φ) default (Fin.snoc (↑f ∘ xs) (↑f b))
h : BoundedFormula.Realize φ default (Fin.snoc xs b)
⊢ BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ Fin.snoc xs b) =
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ xs) (↑f b))
[PROOFSTEP]
rw [Unique.eq_default (f ∘ default), Fin.comp_snoc]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ≃[L] N
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
⊢ Formula.Realize φ (↑f ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → { x // x ∈ ⊤ }
xs : Fin n → { x // x ∈ ⊤ }
⊢ BoundedFormula.Realize φ v xs ↔ BoundedFormula.Realize φ (Subtype.val ∘ v) (Subtype.val ∘ xs)
[PROOFSTEP]
rw [← Substructure.topEquiv.realize_boundedFormula φ]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → { x // x ∈ ⊤ }
xs : Fin n → { x // x ∈ ⊤ }
⊢ BoundedFormula.Realize φ (↑topEquiv ∘ v) (↑topEquiv ∘ xs) ↔
    BoundedFormula.Realize φ (Subtype.val ∘ v) (Subtype.val ∘ xs)
[PROOFSTEP]
simp
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
α : Type u_5
φ : Formula L α
v : α → { x // x ∈ ⊤ }
⊢ Formula.Realize φ v ↔ Formula.Realize φ (Subtype.val ∘ v)
[PROOFSTEP]
rw [← Substructure.topEquiv.realize_formula φ]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
α : Type u_5
φ : Formula L α
v : α → { x // x ∈ ⊤ }
⊢ Formula.Realize φ (↑topEquiv ∘ v) ↔ Formula.Realize φ (Subtype.val ∘ v)
[PROOFSTEP]
simp
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
x✝² x✝¹ : ElementarySubstructure L M
s : Set M
hs1 : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f s
hs2 : Substructure.IsElementary { carrier := s, fun_mem := hs1 }
t : Set M
ht1 : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f t
isElementary'✝ : Substructure.IsElementary { carrier := t, fun_mem := ht1 }
x✝ :
  (fun x => ↑↑x) { toSubstructure := { carrier := s, fun_mem := hs1 }, isElementary' := hs2 } =
    (fun x => ↑↑x) { toSubstructure := { carrier := t, fun_mem := ht1 }, isElementary' := isElementary'✝ }
⊢ { toSubstructure := { carrier := s, fun_mem := hs1 }, isElementary' := hs2 } =
    { toSubstructure := { carrier := t, fun_mem := ht1 }, isElementary' := isElementary'✝ }
[PROOFSTEP]
congr
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
S : ElementarySubstructure L M
T : Theory L
⊢ { x // x ∈ S } ⊨ T ↔ M ⊨ T
[PROOFSTEP]
simp only [Theory.model_iff, realize_sentence]


[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
m n : ℕ
h : m ≤ n
⊢ f m ≤ ↑(partialSups f) n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
m n : ℕ
h✝ : m ≤ n
h : m ≤ Nat.zero
⊢ f m ≤ ↑(partialSups f) Nat.zero
[PROOFSTEP]
rw [nonpos_iff_eq_zero.mp h, partialSups_zero]
[GOAL]
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
ih : m ≤ n → f m ≤ ↑(partialSups f) n
h : m ≤ Nat.succ n
⊢ f m ≤ ↑(partialSups f) (Nat.succ n)
[PROOFSTEP]
cases' h with h h
[GOAL]
case succ.refl
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n✝ n : ℕ
h : Nat.succ n ≤ n✝
ih : Nat.succ n ≤ n → f (Nat.succ n) ≤ ↑(partialSups f) n
⊢ f (Nat.succ n) ≤ ↑(partialSups f) (Nat.succ n)
[PROOFSTEP]
exact le_sup_right
[GOAL]
case succ.step
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
ih : m ≤ n → f m ≤ ↑(partialSups f) n
h : Nat.le m n
⊢ f m ≤ ↑(partialSups f) (Nat.succ n)
[PROOFSTEP]
exact (ih h).trans le_sup_left
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
a : α
w : ∀ (m : ℕ), m ≤ n → f m ≤ a
⊢ ↑(partialSups f) n ≤ a
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
a : α
w✝ : ∀ (m : ℕ), m ≤ n → f m ≤ a
w : ∀ (m : ℕ), m ≤ Nat.zero → f m ≤ a
⊢ ↑(partialSups f) Nat.zero ≤ a
[PROOFSTEP]
apply w 0 le_rfl
[GOAL]
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n✝ : ℕ
a : α
w✝ : ∀ (m : ℕ), m ≤ n✝ → f m ≤ a
n : ℕ
ih : (∀ (m : ℕ), m ≤ n → f m ≤ a) → ↑(partialSups f) n ≤ a
w : ∀ (m : ℕ), m ≤ Nat.succ n → f m ≤ a
⊢ ↑(partialSups f) (Nat.succ n) ≤ a
[PROOFSTEP]
exact sup_le (ih fun m p => w m (Nat.le_succ_of_le p)) (w (n + 1) le_rfl)
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
⊢ BddAbove (Set.range ↑(partialSups f)) ↔ BddAbove (Set.range f)
[PROOFSTEP]
apply exists_congr fun a => _
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
⊢ ∀ (a : α), a ∈ upperBounds (Set.range ↑(partialSups f)) ↔ a ∈ upperBounds (Set.range f)
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
⊢ a ∈ upperBounds (Set.range ↑(partialSups f)) ↔ a ∈ upperBounds (Set.range f)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
⊢ a ∈ upperBounds (Set.range ↑(partialSups f)) → a ∈ upperBounds (Set.range f)
[PROOFSTEP]
rintro h b ⟨i, rfl⟩
[GOAL]
case mp.intro
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
h : a ∈ upperBounds (Set.range ↑(partialSups f))
i : ℕ
⊢ f i ≤ a
[PROOFSTEP]
exact (le_partialSups _ _).trans (h (Set.mem_range_self i))
[GOAL]
case mpr
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
⊢ a ∈ upperBounds (Set.range f) → a ∈ upperBounds (Set.range ↑(partialSups f))
[PROOFSTEP]
rintro h b ⟨i, rfl⟩
[GOAL]
case mpr.intro
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
h : a ∈ upperBounds (Set.range f)
i : ℕ
⊢ ↑(partialSups f) i ≤ a
[PROOFSTEP]
exact partialSups_le _ _ _ fun _ _ => h (Set.mem_range_self _)
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
hf : Monotone f
⊢ ↑(partialSups f) = f
[PROOFSTEP]
ext n
[GOAL]
case h
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
hf : Monotone f
n : ℕ
⊢ ↑(partialSups f) n = f n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case h.zero
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
hf : Monotone f
⊢ ↑(partialSups f) Nat.zero = f Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case h.succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
hf : Monotone f
n : ℕ
ih : ↑(partialSups f) n = f n
⊢ ↑(partialSups f) (Nat.succ n) = f (Nat.succ n)
[PROOFSTEP]
rw [partialSups_succ, ih, sup_eq_right.2 (hf (Nat.le_succ _))]
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
⊢ Monotone partialSups
[PROOFSTEP]
rintro f g h n
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f g : ℕ → α
h : f ≤ g
n : ℕ
⊢ OrderHom.toFun (partialSups f) n ≤ OrderHom.toFun (partialSups g) n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
inst✝ : SemilatticeSup α
f g : ℕ → α
h : f ≤ g
⊢ OrderHom.toFun (partialSups f) Nat.zero ≤ OrderHom.toFun (partialSups g) Nat.zero
[PROOFSTEP]
exact h 0
[GOAL]
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f g : ℕ → α
h : f ≤ g
n : ℕ
ih : OrderHom.toFun (partialSups f) n ≤ OrderHom.toFun (partialSups g) n
⊢ OrderHom.toFun (partialSups f) (Nat.succ n) ≤ OrderHom.toFun (partialSups g) (Nat.succ n)
[PROOFSTEP]
exact sup_le_sup ih (h _)
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
h : ↑(partialSups f) ≤ f
⊢ Monotone f
[PROOFSTEP]
convert (partialSups f).monotone using 1
[GOAL]
case h.e'_5
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
h : ↑(partialSups f) ≤ f
⊢ f = ↑(partialSups f)
[PROOFSTEP]
exact (le_partialSups f).antisymm h
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
g : ℕ →o α
⊢ partialSups f ≤ g ↔ f ≤ ↑g
[PROOFSTEP]
refine' ⟨(le_partialSups f).trans, fun h => _⟩
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
g : ℕ →o α
h : f ≤ ↑g
⊢ partialSups f ≤ g
[PROOFSTEP]
convert partialSups_mono h
[GOAL]
case h.e'_4
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
g : ℕ →o α
h : f ≤ ↑g
⊢ g = partialSups ↑g
[PROOFSTEP]
exact OrderHom.ext _ _ g.monotone.partialSups_eq.symm
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups f) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ Finset.range (n + 1)) f
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
⊢ ↑(partialSups f) Nat.zero = Finset.sup' (Finset.range (Nat.zero + 1)) (_ : ∃ x, x ∈ Finset.range (Nat.zero + 1)) f
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
ih : ↑(partialSups f) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ Finset.range (n + 1)) f
⊢ ↑(partialSups f) (Nat.succ n) =
    Finset.sup' (Finset.range (Nat.succ n + 1)) (_ : ∃ x, x ∈ Finset.range (Nat.succ n + 1)) f
[PROOFSTEP]
dsimp [partialSups] at ih ⊢
[GOAL]
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
ih :
  Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ Finset.range (n + 1)) f
⊢ Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n ⊔ f (n + 1) =
    Finset.sup' (Finset.range (Nat.succ n + 1)) (_ : ∃ x, x ∈ Finset.range (Nat.succ n + 1)) f
[PROOFSTEP]
simp_rw [@Finset.range_succ n.succ]
[GOAL]
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
ih :
  Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ Finset.range (n + 1)) f
⊢ Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n ⊔ f (n + 1) =
    Finset.sup' (insert (Nat.succ n) (Finset.range (Nat.succ n)))
      (_ : Finset.Nonempty (insert (Nat.succ n) (Finset.range (Nat.succ n)))) fun x => f x
[PROOFSTEP]
rw [ih, Finset.sup'_insert, sup_comm]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups f) n = Finset.sup (Finset.range (n + 1)) f
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
⊢ ↑(partialSups f) Nat.zero = Finset.sup (Finset.range (Nat.zero + 1)) f
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
n : ℕ
ih : ↑(partialSups f) n = Finset.sup (Finset.range (n + 1)) f
⊢ ↑(partialSups f) (Nat.succ n) = Finset.sup (Finset.range (Nat.succ n + 1)) f
[PROOFSTEP]
dsimp [partialSups] at ih ⊢
[GOAL]
case succ
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
n : ℕ
ih : Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n = Finset.sup (Finset.range (n + 1)) f
⊢ Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n ⊔ f (n + 1) = Finset.sup (Finset.range (Nat.succ n + 1)) f
[PROOFSTEP]
rw [Finset.range_succ, Finset.sup_insert, sup_comm, ih]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m n : ℕ
hmn : m < n
⊢ Disjoint (↑(partialSups f) m) (f n)
[PROOFSTEP]
induction' m with m ih
[GOAL]
case zero
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m n : ℕ
hmn✝ : m < n
hmn : Nat.zero < n
⊢ Disjoint (↑(partialSups f) Nat.zero) (f n)
[PROOFSTEP]
exact h hmn.ne
[GOAL]
case succ
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m✝ n : ℕ
hmn✝ : m✝ < n
m : ℕ
ih : m < n → Disjoint (↑(partialSups f) m) (f n)
hmn : Nat.succ m < n
⊢ Disjoint (↑(partialSups f) (Nat.succ m)) (f n)
[PROOFSTEP]
rw [partialSups_succ, disjoint_sup_left]
[GOAL]
case succ
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m✝ n : ℕ
hmn✝ : m✝ < n
m : ℕ
ih : m < n → Disjoint (↑(partialSups f) m) (f n)
hmn : Nat.succ m < n
⊢ Disjoint (↑(partialSups f) m) (f n) ∧ Disjoint (f (m + 1)) (f n)
[PROOFSTEP]
exact ⟨ih (Nat.lt_of_succ_lt hmn), h hmn.ne⟩
[GOAL]
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups f) n = ⨆ (i : ↑(Set.Iic n)), f ↑i
[PROOFSTEP]
have : Set.Iio (n + 1) = Set.Iic n := Set.ext fun _ => Nat.lt_succ_iff
[GOAL]
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
n : ℕ
this : Set.Iio (n + 1) = Set.Iic n
⊢ ↑(partialSups f) n = ⨆ (i : ↑(Set.Iic n)), f ↑i
[PROOFSTEP]
rw [partialSups_eq_sup'_range, Finset.sup'_eq_csSup_image, Finset.coe_range, iSup, this]
[GOAL]
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
n : ℕ
this : Set.Iio (n + 1) = Set.Iic n
⊢ sSup (f '' Set.Iic n) = sSup (Set.range fun i => f ↑i)
[PROOFSTEP]
simp only [Set.range, Subtype.exists, Set.mem_Iic, exists_prop, (· '' ·)]
[GOAL]
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
⊢ ⨆ (n : ℕ), ↑(partialSups f) n = ⨆ (n : ℕ), f n
[PROOFSTEP]
refine' (ciSup_le fun n => _).antisymm (ciSup_mono _ <| le_partialSups f)
[GOAL]
case refine'_1
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
n : ℕ
⊢ ↑(partialSups f) n ≤ ⨆ (n : ℕ), f n
[PROOFSTEP]
rw [partialSups_eq_ciSup_Iic]
[GOAL]
case refine'_1
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
n : ℕ
⊢ ⨆ (i : ↑(Set.Iic n)), f ↑i ≤ ⨆ (n : ℕ), f n
[PROOFSTEP]
exact ciSup_le fun i => le_ciSup h _
[GOAL]
case refine'_2
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
⊢ BddAbove (Set.range fun n => ↑(partialSups f) n)
[PROOFSTEP]
rwa [bddAbove_range_partialSups]
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups f) n = ⨆ (i : ℕ) (_ : i ≤ n), f i
[PROOFSTEP]
simpa only [iSup_subtype] using partialSups_eq_ciSup_Iic f n
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
f g : ℕ → α
h : partialSups f ≤ partialSups g
⊢ ⨆ (n : ℕ), f n ≤ ⨆ (n : ℕ), g n
[PROOFSTEP]
rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g]
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
f g : ℕ → α
h : partialSups f ≤ partialSups g
⊢ ⨆ (n : ℕ), ↑(partialSups f) n ≤ ⨆ (n : ℕ), ↑(partialSups g) n
[PROOFSTEP]
exact iSup_mono h
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
f g : ℕ → α
h : partialSups f = partialSups g
⊢ ⨆ (n : ℕ), f n = ⨆ (n : ℕ), g n
[PROOFSTEP]
simp_rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g, h]