-- Mathlib/ModelTheory/Semantics.lean
theorem _root_.FirstOrder.Language.Formula.realize_iExsUnique [Finite γ]
    {φ : L.Formula (α ⊕ γ)} {v : α → M} : (φ.iExsUnique γ).Realize v ↔
      ∃! (i : γ → M), φ.Realize (Sum.elim v i)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (Formula.iExs γ
          (φ ⊓
            Formula.iAlls γ
              ((Formula.relabel (fun a => Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) φ).imp
                (iInf fun g => (var (Sum.inr g)).equal (var (Sum.inl (Sum.inr g))))))).Realize
      v ↔
    ∃ x, φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x

Tactic:
simp only [Formula.realize_iExs, Formula.realize_inf, Formula.realize_iAlls, Formula.realize_imp,
  Formula.realize_relabel]

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (∃ i,
      φ.Realize (Sum.elim v i) ∧
        ∀ (i_1 : γ → M),
          φ.Realize ((fun a => Sum.elim (Sum.elim v i) i_1 a) ∘ fun a => Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) →
            Formula.Realize (iInf fun g => (var (Sum.inr g)).equal (var (Sum.inl (Sum.inr g)))) fun a =>
              Sum.elim (Sum.elim v i) i_1 a) ↔
    ∃ x, φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
⊢ (Realize φ (fun x => Sum.elim (Sum.elim v i) y (Sum.elim (fun x => Sum.inl (Sum.inl x)) Sum.inr x)) default →
      ∀ (b : γ), y b = i b) ↔
    Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x

Tactic:
rw [iff_iff_eq]

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
⊢ (Realize φ (fun x => Sum.elim (Sum.elim v i) y (Sum.elim (fun x => Sum.inl (Sum.inl x)) Sum.inr x)) default →
      ∀ (b : γ), y b = i b) =
    (Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (∃ i,
      Realize φ (Sum.elim v i) default ∧
        ∀ (i_1 : γ → M),
          Realize φ (fun x => Sum.elim (Sum.elim v i) i_1 (Sum.elim (fun x => Sum.inl (Sum.inl x)) Sum.inr x)) default →
            ∀ (b : γ), i_1 b = i b) ↔
    ∃ x, Realize φ (Sum.elim v x) default ∧ ∀ (y : γ → M), Realize φ (Sum.elim v y) default → ∀ (x_1 : γ), y x_1 = x x_1

Tactic:
refine exists_congr (fun i => and_congr_right' (forall_congr' (fun y => ?_)))

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
⊢ (Realize φ (fun x => Sum.elim (Sum.elim v i) y (Sum.elim (fun x => Sum.inl (Sum.inl x)) Sum.inr x)) default →
      ∀ (b : γ), y b = i b) ↔
    Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
⊢ (Realize φ (fun x => Sum.elim (Sum.elim v i) y (Sum.elim (fun x => Sum.inl (Sum.inl x)) Sum.inr x)) default →
      ∀ (b : γ), y b = i b) =
    (Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x)

Tactic:
congr with x

Result:
case h₁.e__v.h
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
x : α ⊕ γ
⊢ Sum.elim (Sum.elim v i) y (Sum.elim (fun x => Sum.inl (Sum.inl x)) Sum.inr x) = Sum.elim v y x

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (Formula.iExsUnique γ φ).Realize v ↔ ∃! i, φ.Realize (Sum.elim v i)

Tactic:
rw [Formula.iExsUnique, ExistsUnique]

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (Formula.iExs γ
          (φ ⊓
            Formula.iAlls γ
              ((Formula.relabel (fun a => Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) φ).imp
                (iInf fun g => (var (Sum.inr g)).equal (var (Sum.inl (Sum.inr g))))))).Realize
      v ↔
    ∃ x, φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (∃ i,
      φ.Realize (Sum.elim v i) ∧
        ∀ (i_1 : γ → M),
          φ.Realize ((fun a => Sum.elim (Sum.elim v i) i_1 a) ∘ fun a => Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) →
            Formula.Realize (iInf fun g => (var (Sum.inr g)).equal (var (Sum.inl (Sum.inr g)))) fun a =>
              Sum.elim (Sum.elim v i) i_1 a) ↔
    ∃ x, φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x

Tactic:
simp only [Formula.Realize, Function.comp_def, Term.equal, Term.relabel, realize_iInf,
  realize_bdEqual, Term.realize_var, Sum.elim_inl, Sum.elim_inr, funext_iff]

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (∃ i,
      Realize φ (Sum.elim v i) default ∧
        ∀ (i_1 : γ → M),
          Realize φ (fun x => Sum.elim (Sum.elim v i) i_1 (Sum.elim (fun x => Sum.inl (Sum.inl x)) Sum.inr x)) default →
            ∀ (b : γ), i_1 b = i b) ↔
    ∃ x, Realize φ (Sum.elim v x) default ∧ ∀ (y : γ → M), Realize φ (Sum.elim v y) default → ∀ (x_1 : γ), y x_1 = x x_1

Proof state:
case h₁.e__v.h
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
x : α ⊕ γ
⊢ Sum.elim (Sum.elim v i) y (Sum.elim (fun x => Sum.inl (Sum.inl x)) Sum.inr x) = Sum.elim v y x

Tactic:
cases x <;> simp

Result:
no goals