-- Mathlib/ModelTheory/Semantics.lean
theorem Sentence.realize_cardGe (n) : M ⊨ Sentence.cardGe L n ↔ ↑n ≤ #M

Proof state:
case refine_1.intro
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : i ≠ j
hij : (∼(var (Sum.inr i) =' var (Sum.inr j))).Realize default xs
⊢ xs i ≠ xs j

Tactic:
simp only [BoundedFormula.realize_not, Term.realize, BoundedFormula.realize_bdEqual,
  Sum.elim_inr] at hij

Result:
case refine_1.intro
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : i ≠ j
hij : ¬xs i = xs j
⊢ xs i ≠ xs j

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) ↔
    Nonempty (Fin n ↪ M)

Tactic:
refine ⟨?_, fun xs => ⟨xs.some, ?_⟩⟩

Result:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) →
    Nonempty (Fin n ↪ M)

case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Nonempty (Fin n ↪ M)
⊢ ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default ⇑xs.some

Proof state:
case refine_1.intro
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : i ≠ j
⊢ xs i ≠ xs j

Tactic:
have hij := h _ i j (by simpa using ij) rfl

Result:
case refine_1.intro
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : i ≠ j
hij : (∼(var (Sum.inr i) =' var (Sum.inr j))).Realize default xs
⊢ xs i ≠ xs j

Proof state:
case refine_1.intro
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : xs i = xs j
⊢ i = j

Tactic:
contrapose! ij

Result:
case refine_1.intro
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : i ≠ j
⊢ xs i ≠ xs j

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      ∀
        φ ∈
          List.map (fun ij => ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
            (List.filter (fun ij => decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)),
        φ.Realize default xs) ↔
    Nonempty (Fin n ↪ M)

Tactic:
simp only [Function.comp_apply, List.mem_map, Prod.exists, Ne, List.mem_product,
  List.mem_finRange, forall_exists_index, and_imp, List.mem_filter, true_and]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) ↔
    Nonempty (Fin n ↪ M)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      (List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤
            (List.map (fun ij => ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
              (List.filter (fun ij => decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)))).Realize
        default xs) ↔
    Nonempty (Fin n ↪ M)

Tactic:
simp_rw [BoundedFormula.realize_foldr_inf]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      ∀
        φ ∈
          List.map (fun ij => ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
            (List.filter (fun ij => decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)),
        φ.Realize default xs) ↔
    Nonempty (Fin n ↪ M)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : i ≠ j
⊢ (decide ¬i = j) = true

Tactic:
simpa using ij

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ M ⊨ Sentence.cardGe L n ↔ ↑n ≤ #M

Tactic:
rw [← lift_mk_fin, ← lift_le.{0}, lift_lift, lift_mk_le, Sentence.cardGe, Sentence.Realize,
  BoundedFormula.realize_exs]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      (List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤
            (List.map (fun ij => ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
              (List.filter (fun ij => decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)))).Realize
        default xs) ↔
    Nonempty (Fin n ↪ M)

Proof state:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Nonempty (Fin n ↪ M)
i j : Fin n
ij : (decide ¬i = j) = true
⊢ (∼(var (Sum.inr i) =' var (Sum.inr j))).Realize default ⇑xs.some

Tactic:
simpa using ij

Result:
no goals

Proof state:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Nonempty (Fin n ↪ M)
⊢ ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default ⇑xs.some

Tactic:
rintro _ i j ij rfl

Result:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Nonempty (Fin n ↪ M)
i j : Fin n
ij : (decide ¬i = j) = true
⊢ (∼(var (Sum.inr i) =' var (Sum.inr j))).Realize default ⇑xs.some

Proof state:
case refine_1.intro
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
⊢ Nonempty (Fin n ↪ M)

Tactic:
refine ⟨⟨xs, fun i j ij => ?_⟩⟩

Result:
case refine_1.intro
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : xs i = xs j
⊢ i = j

Proof state:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) →
    Nonempty (Fin n ↪ M)

Tactic:
rintro ⟨xs, h⟩

Result:
case refine_1.intro
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
⊢ Nonempty (Fin n ↪ M)

Proof state:
case refine_1.intro
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : i ≠ j
hij : ¬xs i = xs j
⊢ xs i ≠ xs j

Tactic:
exact hij

Result:
no goals