Theorem: LO.FirstOrder.ElementaryEquiv.ofEquiv (Logic/FirstOrder/Basic/Semantics/Elementary.lean)

State before:
n : ℕ
μ : Sort ?u.123142
N : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Nonempty M
inst✝⁵ : Nonempty M₁
inst✝⁴ : Nonempty M₂
inst✝³ : Nonempty M₃
s✝ : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝² : FunLike F M₁ M₂
inst✝¹ : Structure.EmbeddingClass F L M₁ M₂
φ✝ : F
e₁ : Fin n → M₁
ε₁ : μ → M₁
s : Structure L M
φ : M ≃ N
inst✝ : Nonempty N
σ : Sentence L
⊢ M ⊧ₘ σ ↔ N ⊧ₘ σ
Tactic:
letI : Structure L N := Structure.ofEquiv φ
State after:
n : ℕ
μ : Sort ?u.123142
N : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Nonempty M
inst✝⁵ : Nonempty M₁
inst✝⁴ : Nonempty M₂
inst✝³ : Nonempty M₃
s✝ : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝² : FunLike F M₁ M₂
inst✝¹ : Structure.EmbeddingClass F L M₁ M₂
φ✝ : F
e₁ : Fin n → M₁
ε₁ : μ → M₁
s : Structure L M
φ : M ≃ N
inst✝ : Nonempty N
σ : Sentence L
this : Structure L N := Structure.ofEquiv φ
⊢ M ⊧ₘ σ ↔ N ⊧ₘ σ

State before:
n : ℕ
μ : Sort ?u.123142
N : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Nonempty M
inst✝⁵ : Nonempty M₁
inst✝⁴ : Nonempty M₂
inst✝³ : Nonempty M₃
s✝ : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝² : FunLike F M₁ M₂
inst✝¹ : Structure.EmbeddingClass F L M₁ M₂
φ✝ : F
e₁ : Fin n → M₁
ε₁ : μ → M₁
s : Structure L M
φ : M ≃ N
inst✝ : Nonempty N
σ : Sentence L
this : Structure L N := Structure.ofEquiv φ
⊢ M ⊧ₘ σ ↔ N ⊧ₘ σ
Tactic:
simp [models_iff, Empty.eq_elim, Structure.eval_ofEquiv_iff]
State after:
no goals