L : Language
M : Type u_3
N : Type u_4
P : Type ?u.306353
Q : Type ?u.306356
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
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.306353
Q : Type ?u.306356
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
⊢ Function.Injective ↑φ
intro x y
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.306353
Q : Type ?u.306356
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
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.306353
Q : Type ?u.306356
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
have h :=
  φ.map_formula ((var 0).equal (var 1) : L.Formula (Fin 2)) fun i => if i = 0 then x else y
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.306353
Q : Type ?u.306356
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
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.306353
Q : Type ?u.306356
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
rw [Formula.realize_equal, Formula.realize_equal] at h
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.306353
Q : Type ?u.306356
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
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.306353
Q : Type ?u.306356
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
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
no goals
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.306353
Q : Type ?u.306356
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
exact h.1