L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
⊢ (∃ xs,
      BoundedFormula.Realize
        (List.foldr (fun x x_1 => x ⊓ x_1) ⊤
          (List.map (fun ij => ∼((var ∘ Sum.inr) ij.fst =' (var ∘ Sum.inr) ij.snd))
            (List.filter (fun ij => decide (ij.fst ≠ ij.snd)) (List.finRange n ×ˢ List.finRange n))))
        default xs) ↔
    Nonempty (Fin n ↪ M)
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
⊢ M ⊨ Sentence.cardGe L n ↔ ↑n ≤ (#M)
rw [← lift_mk_fin, ← lift_le.{w, 0}, lift_lift, lift_mk_le, Sentence.cardGe, Sentence.Realize,
  BoundedFormula.realize_exs]
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
⊢ (∃ xs,
      ∀ (φ : BoundedFormula L Empty n),
        φ ∈
            List.map (fun ij => ∼((var ∘ Sum.inr) ij.fst =' (var ∘ Sum.inr) ij.snd))
              (List.filter (fun ij => decide (ij.fst ≠ ij.snd)) (List.finRange n ×ˢ List.finRange n)) →
          BoundedFormula.Realize φ default xs) ↔
    Nonempty (Fin n ↪ M)
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
⊢ (∃ xs,
      BoundedFormula.Realize
        (List.foldr (fun x x_1 => x ⊓ x_1) ⊤
          (List.map (fun ij => ∼((var ∘ Sum.inr) ij.fst =' (var ∘ Sum.inr) ij.snd))
            (List.filter (fun ij => decide (ij.fst ≠ ij.snd)) (List.finRange n ×ˢ List.finRange n))))
        default xs) ↔
    Nonempty (Fin n ↪ M)
simp_rw [BoundedFormula.realize_foldr_inf]
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
⊢ (∃ xs,
      ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs) ↔
    Nonempty (Fin n ↪ M)
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
⊢ (∃ xs,
      ∀ (φ : BoundedFormula L Empty n),
        φ ∈
            List.map (fun ij => ∼((var ∘ Sum.inr) ij.fst =' (var ∘ Sum.inr) ij.snd))
              (List.filter (fun ij => decide (ij.fst ≠ ij.snd)) (List.finRange n ×ˢ List.finRange n)) →
          BoundedFormula.Realize φ default xs) ↔
    Nonempty (Fin n ↪ M)
simp only [Function.comp_apply, List.mem_map, Prod.exists, Ne.def, List.mem_product,
  List.mem_finRange, forall_exists_index, and_imp, List.mem_filter, true_and_iff]
case refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
⊢ (∃ xs,
      ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs) →
    Nonempty (Fin n ↪ M)

case refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Nonempty (Fin n ↪ M)
⊢ ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true →
      ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default ↑(Nonempty.some xs)
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
⊢ (∃ xs,
      ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs) ↔
    Nonempty (Fin n ↪ M)
refine' ⟨_, fun xs => ⟨xs.some, _⟩⟩
case refine'_1.intro
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs
⊢ Nonempty (Fin n ↪ M)
case refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
⊢ (∃ xs,
      ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs) →
    Nonempty (Fin n ↪ M)
rintro ⟨xs, h⟩
case refine'_1.intro
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs
i j : Fin n
ij : xs i = xs j
⊢ i = j
case refine'_1.intro
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs
⊢ Nonempty (Fin n ↪ M)
refine' ⟨⟨xs, fun i j ij => _⟩⟩
case refine'_1.intro
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs
i j : Fin n
ij : i ≠ j
⊢ xs i ≠ xs j
case refine'_1.intro
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs
i j : Fin n
ij : xs i = xs j
⊢ i = j
contrapose! ij
case refine'_1.intro
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs
i j : Fin n
ij : i ≠ j
hij : BoundedFormula.Realize (∼(var (Sum.inr i) =' var (Sum.inr j))) default xs
⊢ xs i ≠ xs j
case refine'_1.intro
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs
i j : Fin n
ij : i ≠ j
⊢ xs i ≠ xs j
have hij := h _ i j (by simpa using ij) rfl
case refine'_1.intro
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs
i j : Fin n
ij : i ≠ j
hij : ¬xs i = xs j
⊢ xs i ≠ xs j
case refine'_1.intro
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs
i j : Fin n
ij : i ≠ j
hij : BoundedFormula.Realize (∼(var (Sum.inr i) =' var (Sum.inr j))) default xs
⊢ xs i ≠ xs j
simp only [BoundedFormula.realize_not, Term.realize, BoundedFormula.realize_bdEqual,
  Sum.elim_inr] at hij
no goals
case refine'_1.intro
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs
i j : Fin n
ij : i ≠ j
hij : ¬xs i = xs j
⊢ xs i ≠ xs j
exact hij
no goals
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default xs
i j : Fin n
ij : i ≠ j
⊢ (decide ¬i = j) = true
simpa using ij
case refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Nonempty (Fin n ↪ M)
i j : Fin n
ij : (decide ¬i = j) = true
⊢ BoundedFormula.Realize (∼(var (Sum.inr i) =' var (Sum.inr j))) default ↑(Nonempty.some xs)
case refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Nonempty (Fin n ↪ M)
⊢ ∀ (φ : BoundedFormula L Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true →
      ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → BoundedFormula.Realize φ default ↑(Nonempty.some xs)
rintro _ i j ij rfl
no goals
case refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.762328
P : Type ?u.762331
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
n : ℕ
xs : Nonempty (Fin n ↪ M)
i j : Fin n
ij : (decide ¬i = j) = true
⊢ BoundedFormula.Realize (∼(var (Sum.inr i) =' var (Sum.inr j))) default ↑(Nonempty.some xs)
simpa using ij