Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.hom p = ω₂.hom p
Tactic:
induction p using rec' generalizing n₂ <;> simp[*, Rew.rel, Rew.nrel] <;> simp[fvarList] at hf
Proof state after:
case hrel
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => ∃ a, x ∈ (v✝ a).fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ (fun i => ω₁ (v✝ i)) = fun i => ω₂ (v✝ i)

case hnrel
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => ∃ a, x ∈ (v✝ a).fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ (fun i => ω₁ (v✝ i)) = fun i => ω₂ (v✝ i)

case hand
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ q✝ : Semiformula L ξ₁ n✝
a✝¹ :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂},
    (∀ (x : Fin n✝), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
a✝ :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂},
    (∀ (x : Fin n✝), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ q✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom q✝ = ω₂.hom q✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList ∨ x ∈ q✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.hom p✝ = ω₂.hom p✝ ∧ ω₁.hom q✝ = ω₂.hom q✝

case hor
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ q✝ : Semiformula L ξ₁ n✝
a✝¹ :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂},
    (∀ (x : Fin n✝), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
a✝ :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂},
    (∀ (x : Fin n✝), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ q✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom q✝ = ω₂.hom q✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList ∨ x ∈ q✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.hom p✝ = ω₂.hom p✝ ∧ ω₁.hom q✝ = ω₂.hom q✝

case hall
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ (n✝ + 1) ξ₂ n₂},
    (∀ (x : Fin (n✝ + 1)), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.q.hom p✝ = ω₂.q.hom p✝

case hex
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ (n✝ + 1) ξ₂ n₂},
    (∀ (x : Fin (n✝ + 1)), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.q.hom p✝ = ω₂.q.hom p✝