Theorem: PropForm.eval_of_not_occurs (LAMR/Examples/using_lean_as_a_proof_assistant/induction.lean)

State before:
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
h : ¬Occurs v A
b : Bool
⊢ eval (fun w => if v = w then b else τ w) A = eval τ A
Tactic:
induction A with
| var s =>
  rw [eval]
  rw [Occurs] at h
  rw [if_neg h, eval]
| tr =>
  rw [eval, eval]
| fls =>
  rw [eval, eval]
| neg A ihA =>
  rw [eval, eval]
  rw [Occurs] at h
  rw [ihA h]
| conj A B ihA ihB =>
  rw [Occurs, not_or] at h
  rcases h with ⟨hA, hB⟩
  rw [eval, eval, ihA hA, ihB hB]
| disj A B ihA ihB =>
  rw [Occurs, not_or] at h
  rcases h with ⟨hA, hB⟩
  rw [eval, eval, ihA hA, ihB hB]
| impl A B ihA ihB =>
  rw [Occurs, not_or] at h
  rcases h with ⟨hA, hB⟩
  rw [eval, eval, ihA hA, ihB hB]
| biImpl A B ihA ihB =>
  rw [Occurs, not_or] at h
  rcases h with ⟨hA, hB⟩
  rw [eval, eval, ihA hA, ihB hB]
State after:
no goals

State before:
case var
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
s : String
h : ¬Occurs v (var s)
⊢ eval (fun w => if v = w then b else τ w) (var s) = eval τ (var s)
Tactic:
rw [eval]
State after:
case var
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
s : String
h : ¬Occurs v (var s)
⊢ (if v = s then b else τ s) = eval τ (var s)

State before:
case var
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
s : String
h : ¬Occurs v (var s)
⊢ (if v = s then b else τ s) = eval τ (var s)
Tactic:
rw [Occurs] at h
State after:
case var
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
s : String
h : ¬v = s
⊢ (if v = s then b else τ s) = eval τ (var s)

State before:
case var
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
s : String
h : ¬v = s
⊢ (if v = s then b else τ s) = eval τ (var s)
Tactic:
rw [if_neg h, eval]
State after:
no goals

State before:
case tr
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
h : ¬Occurs v tr
⊢ eval (fun w => if v = w then b else τ w) tr = eval τ tr
Tactic:
rw [eval, eval]
State after:
no goals

State before:
case fls
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
h : ¬Occurs v fls
⊢ eval (fun w => if v = w then b else τ w) fls = eval τ fls
Tactic:
rw [eval, eval]
State after:
no goals

State before:
case neg
α : Type
as bs cs : List α
a b✝ c : α
A✝ B : PropForm
τ : String → Bool
v : String
b : Bool
A : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
h : ¬Occurs v (neg A)
⊢ eval (fun w => if v = w then b else τ w) (neg A) = eval τ (neg A)
Tactic:
rw [eval, eval]
State after:
case neg
α : Type
as bs cs : List α
a b✝ c : α
A✝ B : PropForm
τ : String → Bool
v : String
b : Bool
A : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
h : ¬Occurs v (neg A)
⊢ (!eval (fun w => if v = w then b else τ w) A) = !eval τ A

State before:
case neg
α : Type
as bs cs : List α
a b✝ c : α
A✝ B : PropForm
τ : String → Bool
v : String
b : Bool
A : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
h : ¬Occurs v (neg A)
⊢ (!eval (fun w => if v = w then b else τ w) A) = !eval τ A
Tactic:
rw [Occurs] at h
State after:
case neg
α : Type
as bs cs : List α
a b✝ c : α
A✝ B : PropForm
τ : String → Bool
v : String
b : Bool
A : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
h : ¬Occurs v A
⊢ (!eval (fun w => if v = w then b else τ w) A) = !eval τ A

State before:
case neg
α : Type
as bs cs : List α
a b✝ c : α
A✝ B : PropForm
τ : String → Bool
v : String
b : Bool
A : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
h : ¬Occurs v A
⊢ (!eval (fun w => if v = w then b else τ w) A) = !eval τ A
Tactic:
rw [ihA h]
State after:
no goals

State before:
case conj
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v (conj A B)
⊢ eval (fun w => if v = w then b else τ w) (conj A B) = eval τ (conj A B)
Tactic:
rw [Occurs, not_or] at h
State after:
case conj
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (conj A B) = eval τ (conj A B)

State before:
case conj
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (conj A B) = eval τ (conj A B)
Tactic:
rcases h with ⟨hA, hB⟩
State after:
case conj.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (conj A B) = eval τ (conj A B)

State before:
case conj.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (conj A B) = eval τ (conj A B)
Tactic:
rw [eval, eval, ihA hA, ihB hB]
State after:
no goals

State before:
case disj
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v (disj A B)
⊢ eval (fun w => if v = w then b else τ w) (disj A B) = eval τ (disj A B)
Tactic:
rw [Occurs, not_or] at h
State after:
case disj
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (disj A B) = eval τ (disj A B)

State before:
case disj
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (disj A B) = eval τ (disj A B)
Tactic:
rcases h with ⟨hA, hB⟩
State after:
case disj.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (disj A B) = eval τ (disj A B)

State before:
case disj.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (disj A B) = eval τ (disj A B)
Tactic:
rw [eval, eval, ihA hA, ihB hB]
State after:
no goals

State before:
case impl
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v (impl A B)
⊢ eval (fun w => if v = w then b else τ w) (impl A B) = eval τ (impl A B)
Tactic:
rw [Occurs, not_or] at h
State after:
case impl
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (impl A B) = eval τ (impl A B)

State before:
case impl
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (impl A B) = eval τ (impl A B)
Tactic:
rcases h with ⟨hA, hB⟩
State after:
case impl.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (impl A B) = eval τ (impl A B)

State before:
case impl.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (impl A B) = eval τ (impl A B)
Tactic:
rw [eval, eval, ihA hA, ihB hB]
State after:
no goals

State before:
case biImpl
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v (biImpl A B)
⊢ eval (fun w => if v = w then b else τ w) (biImpl A B) = eval τ (biImpl A B)
Tactic:
rw [Occurs, not_or] at h
State after:
case biImpl
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (biImpl A B) = eval τ (biImpl A B)

State before:
case biImpl
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (biImpl A B) = eval τ (biImpl A B)
Tactic:
rcases h with ⟨hA, hB⟩
State after:
case biImpl.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (biImpl A B) = eval τ (biImpl A B)

State before:
case biImpl.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (biImpl A B) = eval τ (biImpl A B)
Tactic:
rw [eval, eval, ihA hA, ihB hB]
State after:
no goals