Theorem: FOL.NV.aux_1 (FOL/NV/Alpha.lean)

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvVar binders x y
⊢ V x = V' y
Tactic:
induction h1
State after:
case nil
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' V✝ : VarAssignment D
h2 : isAlphaEqvVar [] x y
⊢ V✝ x = V✝ y

case cons
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
binders✝ : List (VarName × VarName)
x✝ y✝ : VarName
V✝ V'✝ : VarAssignment D
d✝ : D
a✝ : AlphaEqvVarAssignment D binders✝ V✝ V'✝
a_ih✝ : isAlphaEqvVar binders✝ x y → V✝ x = V'✝ y
h2 : isAlphaEqvVar ((x✝, y✝) :: binders✝) x y
⊢ Function.updateITE V✝ x✝ d✝ x = Function.updateITE V'✝ y✝ d✝ y

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' h1_V : VarAssignment D
h2 : isAlphaEqvVar [] x y
⊢ h1_V x = h1_V y
Tactic:
case nil h1_V =>
  simp only [isAlphaEqvVar] at h2
  subst h2
  rfl
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : isAlphaEqvVar ((h1_x, h1_y) :: h1_l) x y
⊢ Function.updateITE h1_V h1_x h1_d x = Function.updateITE h1_V' h1_y h1_d y
Tactic:
case cons h1_l h1_x h1_y h1_V h1_V' h1_d _ h1_ih =>
  simp only [isAlphaEqvVar] at h2
  simp only [Function.updateITE]
  cases h2
  case inl h2 =>
    cases h2
    case intro h2_left h2_right =>
      simp only [if_pos h2_left, if_pos h2_right]
  case inr h2 =>
    cases h2
    case intro h2_left h2_right =>
      cases h2_left
      case intro h2_left_left h2_left_right =>
        simp only [if_neg h2_left_left, if_neg h2_left_right]
        exact h1_ih h2_right
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' h1_V : VarAssignment D
h2 : isAlphaEqvVar [] x y
⊢ h1_V x = h1_V y
Tactic:
simp only [isAlphaEqvVar] at h2
State after:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' h1_V : VarAssignment D
h2 : x = y
⊢ h1_V x = h1_V y

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' h1_V : VarAssignment D
h2 : x = y
⊢ h1_V x = h1_V y
Tactic:
subst h2
State after:
D : Type
binders : List (VarName × VarName)
x : VarName
V V' h1_V : VarAssignment D
⊢ h1_V x = h1_V x

State before:
D : Type
binders : List (VarName × VarName)
x : VarName
V V' h1_V : VarAssignment D
⊢ h1_V x = h1_V x
Tactic:
rfl
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : isAlphaEqvVar ((h1_x, h1_y) :: h1_l) x y
⊢ Function.updateITE h1_V h1_x h1_d x = Function.updateITE h1_V' h1_y h1_d y
Tactic:
simp only [isAlphaEqvVar] at h2
State after:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : x = h1_x ∧ y = h1_y ∨ (¬x = h1_x ∧ ¬y = h1_y) ∧ isAlphaEqvVar h1_l x y
⊢ Function.updateITE h1_V h1_x h1_d x = Function.updateITE h1_V' h1_y h1_d y

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : x = h1_x ∧ y = h1_y ∨ (¬x = h1_x ∧ ¬y = h1_y) ∧ isAlphaEqvVar h1_l x y
⊢ Function.updateITE h1_V h1_x h1_d x = Function.updateITE h1_V' h1_y h1_d y
Tactic:
simp only [Function.updateITE]
State after:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : x = h1_x ∧ y = h1_y ∨ (¬x = h1_x ∧ ¬y = h1_y) ∧ isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : x = h1_x ∧ y = h1_y ∨ (¬x = h1_x ∧ ¬y = h1_y) ∧ isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
cases h2
State after:
case inl
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h✝ : x = h1_x ∧ y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y

case inr
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h✝ : (¬x = h1_x ∧ ¬y = h1_y) ∧ isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : x = h1_x ∧ y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
case inl h2 =>
  cases h2
  case intro h2_left h2_right =>
    simp only [if_pos h2_left, if_pos h2_right]
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : (¬x = h1_x ∧ ¬y = h1_y) ∧ isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
case inr h2 =>
  cases h2
  case intro h2_left h2_right =>
    cases h2_left
    case intro h2_left_left h2_left_right =>
      simp only [if_neg h2_left_left, if_neg h2_left_right]
      exact h1_ih h2_right
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : x = h1_x ∧ y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
cases h2
State after:
case intro
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
left✝ : x = h1_x
right✝ : y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_left : x = h1_x
h2_right : y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
case intro h2_left h2_right =>
  simp only [if_pos h2_left, if_pos h2_right]
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_left : x = h1_x
h2_right : y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
simp only [if_pos h2_left, if_pos h2_right]
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : (¬x = h1_x ∧ ¬y = h1_y) ∧ isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
cases h2
State after:
case intro
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
left✝ : ¬x = h1_x ∧ ¬y = h1_y
right✝ : isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_left : ¬x = h1_x ∧ ¬y = h1_y
h2_right : isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
case intro h2_left h2_right =>
  cases h2_left
  case intro h2_left_left h2_left_right =>
    simp only [if_neg h2_left_left, if_neg h2_left_right]
    exact h1_ih h2_right
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_left : ¬x = h1_x ∧ ¬y = h1_y
h2_right : isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
cases h2_left
State after:
case intro
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_right : isAlphaEqvVar h1_l x y
left✝ : ¬x = h1_x
right✝ : ¬y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_right : isAlphaEqvVar h1_l x y
h2_left_left : ¬x = h1_x
h2_left_right : ¬y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
case intro h2_left_left h2_left_right =>
  simp only [if_neg h2_left_left, if_neg h2_left_right]
  exact h1_ih h2_right
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_right : isAlphaEqvVar h1_l x y
h2_left_left : ¬x = h1_x
h2_left_right : ¬y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
simp only [if_neg h2_left_left, if_neg h2_left_right]
State after:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_right : isAlphaEqvVar h1_l x y
h2_left_left : ¬x = h1_x
h2_left_right : ¬y = h1_y
⊢ h1_V x = h1_V' y

State before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_right : isAlphaEqvVar h1_l x y
h2_left_left : ¬x = h1_x
h2_left_right : ¬y = h1_y
⊢ h1_V x = h1_V' y
Tactic:
exact h1_ih h2_right
State after:
no goals