Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn (Logic/FirstOrder/Basic/Syntax/Rew.lean)

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 p.fvar? (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.hom p = ω₂.hom p
Tactic:
unfold fvar? at*
State after:
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

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
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✝

State before:
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)
Tactic:
case hrel =>
  funext i
  exact Semiterm.rew_eq_of_funEqOn _ _ _ hb
    (hf.of_subset (fun x hx ↦ ⟨i, hx⟩))
State after:
no goals

State before:
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)
Tactic:
case hnrel =>
  funext i
  exact Semiterm.rew_eq_of_funEqOn _ _ _ hb
    (hf.of_subset (fun x hx ↦ ⟨i, hx⟩))
State after:
no goals

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ q✝ : Semiformula L ξ₁ n✝
ihp :
  ∀ {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✝
ihq :
  ∀ {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✝
Tactic:
case hand ihp ihq =>
  exact ⟨ihp hb (hf.of_subset (fun x hx => Or.inl hx)), ihq hb (hf.of_subset (fun x hx => Or.inr hx))⟩
State after:
no goals

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ q✝ : Semiformula L ξ₁ n✝
ihp :
  ∀ {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✝
ihq :
  ∀ {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✝
Tactic:
case hor ihp ihq =>
  exact ⟨ihp hb (hf.of_subset (fun x hx => Or.inl hx)), ihq hb (hf.of_subset (fun x hx => Or.inr hx))⟩
State after:
no goals

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {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✝
Tactic:
case hall ih =>
  exact ih (fun x => by cases x using Fin.cases <;> simp[hb]) (fun x hx => by simp; exact congr_arg _ (hf x hx))
State after:
no goals

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {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✝
Tactic:
case hex ih =>
  exact ih (fun x => by cases x using Fin.cases <;> simp[hb]) (fun x hx => by simp; exact congr_arg _ (hf x hx))
State after:
no goals

State before:
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)
Tactic:
funext i
State after:
case h
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)
i : Fin k✝
⊢ ω₁ (v✝ i) = ω₂ (v✝ i)

State before:
case h
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)
i : Fin k✝
⊢ ω₁ (v✝ i) = ω₂ (v✝ i)
Tactic:
exact Semiterm.rew_eq_of_funEqOn _ _ _ hb
  (hf.of_subset (fun x hx ↦ ⟨i, hx⟩))
State after:
no goals

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ q✝ : Semiformula L ξ₁ n✝
ihp :
  ∀ {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✝
ihq :
  ∀ {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✝
Tactic:
exact ⟨ihp hb (hf.of_subset (fun x hx => Or.inl hx)), ihq hb (hf.of_subset (fun x hx => Or.inr hx))⟩
State after:
no goals

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {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✝
Tactic:
exact ih (fun x => by cases x using Fin.cases <;> simp[hb]) (fun x hx => by simp; exact congr_arg _ (hf x hx))
State after:
no goals

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {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)
x : Fin (n✝ + 1)
⊢ ω₁.q #x = ω₂.q #x
Tactic:
cases x using Fin.cases <;> simp[hb]
State after:
no goals

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {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)
x : ξ₁
hx : (fun x => x ∈ p✝.fvarList) x
⊢ (⇑ω₁.q ∘ Semiterm.fvar) x = (⇑ω₂.q ∘ Semiterm.fvar) x
Tactic:
simp
State after:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {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)
x : ξ₁
hx : (fun x => x ∈ p✝.fvarList) x
⊢ Rew.bShift (ω₁ &x) = Rew.bShift (ω₂ &x)

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {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)
x : ξ₁
hx : (fun x => x ∈ p✝.fvarList) x
⊢ Rew.bShift (ω₁ &x) = Rew.bShift (ω₂ &x)
Tactic:
exact congr_arg _ (hf x hx)
State after:
no goals