Theorem: LO.FirstOrder.Semiterm.Operator.bv_operator (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
⊢ (o.operator v).bv = o.term.bv.biUnion fun i => (v i).bv
Tactic:
simp [operator]
State after:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
⊢ ((Rew.substs v) (Rew.emb o.term)).bv = o.term.bv.biUnion fun i => (v i).bv

State before:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
⊢ ((Rew.substs v) (Rew.emb o.term)).bv = o.term.bv.biUnion fun i => (v i).bv
Tactic:
generalize o.term = s
State after:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
s : Semiterm L Empty k
⊢ ((Rew.substs v) (Rew.emb s)).bv = s.bv.biUnion fun i => (v i).bv

State before:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
s : Semiterm L Empty k
⊢ ((Rew.substs v) (Rew.emb s)).bv = s.bv.biUnion fun i => (v i).bv
Tactic:
induction s <;> try simp [Rew.func, bv_func, Finset.biUnion_biUnion, *]
State after:
case fvar
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
a✝ : Empty
⊢ ((Rew.substs v) (Rew.emb &a✝)).bv = ∅

State before:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
a✝ : Empty
⊢ ((Rew.substs v) (Rew.emb &a✝)).bv = ∅
Tactic:
case fvar => contradiction
State after:
no goals

State before:
case func
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L Empty k
a_ih✝ : ∀ (a : Fin arity✝), ((Rew.substs v) (Rew.emb (a✝ a))).bv = (a✝ a).bv.biUnion fun i => (v i).bv
⊢ ((Rew.substs v) (Rew.emb (func a✝¹ a✝))).bv = (func a✝¹ a✝).bv.biUnion fun i => (v i).bv
Tactic:
simp [Rew.func, bv_func, Finset.biUnion_biUnion, *]
State after:
no goals

State before:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
a✝ : Empty
⊢ ((Rew.substs v) (Rew.emb &a✝)).bv = ∅
Tactic:
contradiction
State after:
no goals