Theorem: LO.FirstOrder.Formula.univClosure_rew_eq_of_eq (Logic/FirstOrder/Basic/Syntax/Rew.lean)

State before:
L : Language
ξ₁ : Type ?u.1797290
n₁ : ℕ
ξ₂ : Type ?u.1797295
n₂ n₂' : ℕ
p : Semiformula L ξ₁ n₁
ω : Rew L ξ₁ n₁ ξ₂ n₂
ω' : Rew L ξ₁ n₁ ξ₂ n₂'
eq : n₂ = n₂'
⊢ n₂' ≤ n₂
Tactic:
simp [eq]
State after:
no goals

State before:
L : Language
ξ₁ : Type u_2
n₁ : ℕ
ξ₂ : Type u_3
n₂ n₂' : ℕ
p : Semiformula L ξ₁ n₁
ω : Rew L ξ₁ n₁ ξ₂ n₂
ω' : Rew L ξ₁ n₁ ξ₂ n₂'
eq : n₂ = n₂'
H : ω = (Rew.castLE ⋯).comp ω'
⊢ ∀* ω.hom p = ∀* ω'.hom p
Tactic:
rcases eq with rfl
State after:
L : Language
ξ₁ : Type u_2
n₁ : ℕ
ξ₂ : Type u_3
n₂ : ℕ
p : Semiformula L ξ₁ n₁
ω ω' : Rew L ξ₁ n₁ ξ₂ n₂
H : ω = (Rew.castLE ⋯).comp ω'
⊢ ∀* ω.hom p = ∀* ω'.hom p

State before:
L : Language
ξ₁ : Type u_2
n₁ : ℕ
ξ₂ : Type u_3
n₂ : ℕ
p : Semiformula L ξ₁ n₁
ω ω' : Rew L ξ₁ n₁ ξ₂ n₂
H : ω = (Rew.castLE ⋯).comp ω'
⊢ ∀* ω.hom p = ∀* ω'.hom p
Tactic:
rcases H with rfl
State after:
L : Language
ξ₁ : Type u_2
n₁ : ℕ
ξ₂ : Type u_3
n₂ : ℕ
p : Semiformula L ξ₁ n₁
ω' : Rew L ξ₁ n₁ ξ₂ n₂
⊢ ∀* ((Rew.castLE ⋯).comp ω').hom p = ∀* ω'.hom p

State before:
L : Language
ξ₁ : Type u_2
n₁ : ℕ
ξ₂ : Type u_3
n₂ : ℕ
p : Semiformula L ξ₁ n₁
ω' : Rew L ξ₁ n₁ ξ₂ n₂
⊢ ∀* ((Rew.castLE ⋯).comp ω').hom p = ∀* ω'.hom p
Tactic:
simp
State after:
no goals