internlm/Lean-Github huggingface dataset:
Theorem: Execution.State.indep_output_disjoint_targets
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
⊢ Disjoint (Reaction.Output.targets (output s i₁)) (Reaction.Output.targets (output s i₂))
Tactic:
cases h₁ : s.rtr[.rcn][i₁] <;> cases h₂ : s.rtr[.rcn][i₂] <;> simp [output, h₁, h₂]
Proof state after:
case none.none
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
h₁ : s.rtr[Component.rcn][i₁] = none
h₂ : s.rtr[Component.rcn][i₂] = none
⊢ Reaction.Output.targets [] = ∅

case none.some
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
h₁ : s.rtr[Component.rcn][i₁] = none
val✝ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some val✝
⊢ Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (val✝.body (input s i₂)))

case some.none
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
val✝ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some val✝
h₂ : s.rtr[Component.rcn][i₂] = none
⊢ Disjoint (Reaction.Output.targets (val✝.body (input s i₁))) (Reaction.Output.targets [])

case some.some
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
val✝¹ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some val✝¹
val✝ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some val✝
⊢ Disjoint (Reaction.Output.targets (val✝¹.body (input s i₁))) (Reaction.Output.targets (val✝.body (input s i₂)))
Theorem: Execution.State.indep_output_disjoint_targets
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
⊢ Disjoint (Reaction.Output.targets (rcn₁.body (input s i₁))) (Reaction.Output.targets (rcn₂.body (input s i₂)))
Tactic:
case some.some rcn₁ rcn₂ =>
  simp [Set.disjoint_iff_forall_ne]
  intro _ _ ⟨_, hc₁, ht₁⟩ _ _ ⟨_, hc₂, ht₂⟩ hc hj
  cases hc; cases hj; cases ht₁; cases ht₂
  replace hc₁ := rcn₁.target_mem_deps hc₁
  replace hc₂ := rcn₂.target_mem_deps hc₂
  cases Dependency.shared_out_dep h₁ h₂ hi.not_eq hc₁ hc₂ <;> simp [hi.left, hi.right] at *
Proof state after:
no goals
Theorem: Execution.State.indep_output_disjoint_targets
Proof state before:
case none.none
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
h₁ : s.rtr[Component.rcn][i₁] = none
h₂ : s.rtr[Component.rcn][i₂] = none
⊢ Reaction.Output.targets [] = ∅

case none.some
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
h₁ : s.rtr[Component.rcn][i₁] = none
val✝ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some val✝
⊢ Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (val✝.body (input s i₂)))

case some.none
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
val✝ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some val✝
h₂ : s.rtr[Component.rcn][i₂] = none
⊢ Disjoint (Reaction.Output.targets (val✝.body (input s i₁))) (Reaction.Output.targets [])
Tactic:
all_goals simp [Reaction.Output.targets]
Proof state after:
no goals
Theorem: Execution.State.indep_output_disjoint_targets
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
⊢ Disjoint (Reaction.Output.targets (rcn₁.body (input s i₁))) (Reaction.Output.targets (rcn₂.body (input s i₂)))
Tactic:
simp [Set.disjoint_iff_forall_ne]
Proof state after:
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
⊢ ∀ (a : Component.Valued) (b : ID),
    (a, b) ∈ Reaction.Output.targets (rcn₁.body (input s i₁)) →
      ∀ (a_2 : Component.Valued) (b_1 : ID),
        (a_2, b_1) ∈ Reaction.Output.targets (rcn₂.body (input s i₂)) → a = a_2 → ¬b = b_1
Theorem: Execution.State.indep_output_disjoint_targets
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
⊢ ∀ (a : Component.Valued) (b : ID),
    (a, b) ∈ Reaction.Output.targets (rcn₁.body (input s i₁)) →
      ∀ (a_2 : Component.Valued) (b_1 : ID),
        (a_2, b_1) ∈ Reaction.Output.targets (rcn₂.body (input s i₂)) → a = a_2 → ¬b = b_1
Tactic:
intro _ _ ⟨_, hc₁, ht₁⟩ _ _ ⟨_, hc₂, ht₂⟩ hc hj
Proof state after:
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝¹ : Component.Valued
b✝¹ : ID
w✝¹ : Change
hc₁ : w✝¹ ∈ rcn₁.body (input s i₁)
ht₁ : Change.Targets w✝¹ (a✝¹, b✝¹).1 (a✝¹, b✝¹).2
a✝ : Component.Valued
b✝ : ID
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
hc : a✝¹ = a✝
hj : b✝¹ = b✝
⊢ False
Theorem: Execution.State.indep_output_disjoint_targets
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝¹ : Component.Valued
b✝¹ : ID
w✝¹ : Change
hc₁ : w✝¹ ∈ rcn₁.body (input s i₁)
ht₁ : Change.Targets w✝¹ (a✝¹, b✝¹).1 (a✝¹, b✝¹).2
a✝ : Component.Valued
b✝ : ID
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
hc : a✝¹ = a✝
hj : b✝¹ = b✝
⊢ False
Tactic:
cases hc
Proof state after:
case refl
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝¹ : ID
w✝¹ : Change
hc₁ : w✝¹ ∈ rcn₁.body (input s i₁)
ht₁ : Change.Targets w✝¹ (a✝, b✝¹).1 (a✝, b✝¹).2
b✝ : ID
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
hj : b✝¹ = b✝
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
⊢ False
Theorem: Execution.State.indep_output_disjoint_targets
Proof state before:
case refl
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝¹ : ID
w✝¹ : Change
hc₁ : w✝¹ ∈ rcn₁.body (input s i₁)
ht₁ : Change.Targets w✝¹ (a✝, b✝¹).1 (a✝, b✝¹).2
b✝ : ID
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
hj : b✝¹ = b✝
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
⊢ False
Tactic:
cases hj
Proof state after:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
w✝¹ : Change
hc₁ : w✝¹ ∈ rcn₁.body (input s i₁)
ht₁ : Change.Targets w✝¹ (a✝, b✝).1 (a✝, b✝).2
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
⊢ False
Theorem: Execution.State.indep_output_disjoint_targets
Proof state before:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
w✝¹ : Change
hc₁ : w✝¹ ∈ rcn₁.body (input s i₁)
ht₁ : Change.Targets w✝¹ (a✝, b✝).1 (a✝, b✝).2
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
⊢ False
Tactic:
cases ht₁
Proof state after:
case refl.refl.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
v✝ : Component.Valued.changeType (a✝, b✝).1
hc₁ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₁.body (input s i₁)
⊢ False
Theorem: Execution.State.indep_output_disjoint_targets
Proof state before:
case refl.refl.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
w✝ : Change
hc₂ : w✝ ∈ rcn₂.body (input s i₂)
ht₂ : Change.Targets w✝ (a✝, b✝).1 (a✝, b✝).2
v✝ : Component.Valued.changeType (a✝, b✝).1
hc₁ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₁.body (input s i₁)
⊢ False
Tactic:
cases ht₂
Proof state after:
case refl.refl.intro.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
v✝¹ : Component.Valued.changeType (a✝, b✝).1
hc₁ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝¹ } ∈ rcn₁.body (input s i₁)
v✝ : Component.Valued.changeType (a✝, b✝).1
hc₂ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₂.body (input s i₂)
⊢ False
Theorem: Execution.State.indep_output_disjoint_targets
Proof state before:
case refl.refl.intro.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
v✝¹ : Component.Valued.changeType (a✝, b✝).1
hc₁ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝¹ } ∈ rcn₁.body (input s i₁)
v✝ : Component.Valued.changeType (a✝, b✝).1
hc₂ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₂.body (input s i₂)
⊢ False
Tactic:
replace hc₁ := rcn₁.target_mem_deps hc₁
Proof state after:
case refl.refl.intro.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
v✝¹ v✝ : Component.Valued.changeType (a✝, b✝).1
hc₂ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₂.body (input s i₂)
hc₁ : Change.Normal.target { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝¹ } ∈ rcn₁.deps Kind.out
⊢ False
Theorem: Execution.State.indep_output_disjoint_targets
Proof state before:
case refl.refl.intro.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
v✝¹ v✝ : Component.Valued.changeType (a✝, b✝).1
hc₂ : Change.norm { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₂.body (input s i₂)
hc₁ : Change.Normal.target { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝¹ } ∈ rcn₁.deps Kind.out
⊢ False
Tactic:
replace hc₂ := rcn₂.target_mem_deps hc₂
Proof state after:
case refl.refl.intro.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
v✝¹ v✝ : Component.Valued.changeType (a✝, b✝).1
hc₁ : Change.Normal.target { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝¹ } ∈ rcn₁.deps Kind.out
hc₂ : Change.Normal.target { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₂.deps Kind.out
⊢ False
Theorem: Execution.State.indep_output_disjoint_targets
Proof state before:
case refl.refl.intro.intro
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
a✝ : Component.Valued
b✝ : ID
v✝¹ v✝ : Component.Valued.changeType (a✝, b✝).1
hc₁ : Change.Normal.target { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝¹ } ∈ rcn₁.deps Kind.out
hc₂ : Change.Normal.target { cpt := (a✝, b✝).1, id := (a✝, b✝).2, value := v✝ } ∈ rcn₂.deps Kind.out
⊢ False
Tactic:
cases Dependency.shared_out_dep h₁ h₂ hi.not_eq hc₁ hc₂ <;> simp [hi.left, hi.right] at *
Proof state after:
no goals
Theorem: Execution.State.indep_output_disjoint_targets
Proof state before:
case some.none
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
val✝ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some val✝
h₂ : s.rtr[Component.rcn][i₂] = none
⊢ Disjoint (Reaction.Output.targets (val✝.body (input s i₁))) (Reaction.Output.targets [])
Tactic:
simp [Reaction.Output.targets]
Proof state after:
no goals
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
⊢ recComplete ind n = recCompleteWF ind n
Tactic:
suffices ∀ k (hk : k ≤ n), recComplete.aux (motive:=motive) ind n k hk = recCompleteWF (motive:=motive) ind k
  from this n n.le_refl
Proof state after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
⊢ ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
⊢ ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
Tactic:
intro k hk
Proof state after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n k : Nat
hk : k ≤ n
⊢ recComplete.aux ind n k hk = recCompleteWF ind k
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n k : Nat
hk : k ≤ n
⊢ recComplete.aux ind n k hk = recCompleteWF ind k
Tactic:
induction n generalizing k
Proof state after:
case zero
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ recComplete.aux ind zero k hk = recCompleteWF ind k

case succ
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n✝ : Nat
n_ih✝ : ∀ (k : Nat) (hk : k ≤ n✝), recComplete.aux ind n✝ k hk = recCompleteWF ind k
k : Nat
hk : k ≤ succ n✝
⊢ recComplete.aux ind (succ n✝) k hk = recCompleteWF ind k
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ recComplete.aux ind zero k hk = recCompleteWF ind k
Tactic:
case zero =>
  dsimp [recComplete.aux]; unfold recCompleteWF
  have : k = 0 := k.eq_zero_of_le_zero hk
  cases this
  apply congrArg; funext k hk; cases hk
Proof state after:
no goals
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : k ≤ succ n
⊢ recComplete.aux ind (succ n) k hk = recCompleteWF ind k
Tactic:
case succ n h_ind =>
  cases k
  case zero =>
    dsimp [recComplete.aux]; unfold recCompleteWF
    apply congrArg; funext k hk; cases hk
  case succ k =>
    dsimp [recComplete.aux]; unfold recCompleteWF
    apply congrArg; funext k hk; rw [h_ind]
Proof state after:
no goals
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ recComplete.aux ind zero k hk = recCompleteWF ind k
Tactic:
dsimp [recComplete.aux]
Proof state after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ (ind k fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = recCompleteWF ind k
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ (ind k fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = recCompleteWF ind k
Tactic:
unfold recCompleteWF
Proof state after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ (ind k fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = ind k fun k_1 x => recCompleteWF ind k_1
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ (ind k fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = ind k fun k_1 x => recCompleteWF ind k_1
Tactic:
have : k = 0 := k.eq_zero_of_le_zero hk
Proof state after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
this : k = 0
⊢ (ind k fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = ind k fun k_1 x => recCompleteWF ind k_1
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
this : k = 0
⊢ (ind k fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = ind k fun k_1 x => recCompleteWF ind k_1
Tactic:
cases this
Proof state after:
case refl
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
hk : 0 ≤ zero
⊢ (ind 0 fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = ind 0 fun k x => recCompleteWF ind k
Theorem: Nat.recComplete_eq
Proof state before:
case refl
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
hk : 0 ≤ zero
⊢ (ind 0 fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = ind 0 fun k x => recCompleteWF ind k
Tactic:
apply congrArg
Proof state after:
case refl.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
hk : 0 ≤ zero
⊢ (fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = fun k x => recCompleteWF ind k
Theorem: Nat.recComplete_eq
Proof state before:
case refl.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
hk : 0 ≤ zero
⊢ (fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = fun k x => recCompleteWF ind k
Tactic:
funext k hk
Proof state after:
case refl.h.h.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
hk✝ : 0 ≤ zero
k : Nat
hk : k < 0
⊢ absurd (_ : k < 0) (_ : ¬k < 0) = recCompleteWF ind k
Theorem: Nat.recComplete_eq
Proof state before:
case refl.h.h.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
hk✝ : 0 ≤ zero
k : Nat
hk : k < 0
⊢ absurd (_ : k < 0) (_ : ¬k < 0) = recCompleteWF ind k
Tactic:
cases hk
Proof state after:
no goals
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : k ≤ succ n
⊢ recComplete.aux ind (succ n) k hk = recCompleteWF ind k
Tactic:
cases k
Proof state after:
case zero
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ recComplete.aux ind (succ n) zero hk = recCompleteWF ind zero

case succ
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
n✝ : Nat
hk : succ n✝ ≤ succ n
⊢ recComplete.aux ind (succ n) (succ n✝) hk = recCompleteWF ind (succ n✝)
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ recComplete.aux ind (succ n) zero hk = recCompleteWF ind zero
Tactic:
case zero =>
  dsimp [recComplete.aux]; unfold recCompleteWF
  apply congrArg; funext k hk; cases hk
Proof state after:
no goals
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ recComplete.aux ind (succ n) (succ k) hk = recCompleteWF ind (succ k)
Tactic:
case succ k =>
  dsimp [recComplete.aux]; unfold recCompleteWF
  apply congrArg; funext k hk; rw [h_ind]
Proof state after:
no goals
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ recComplete.aux ind (succ n) zero hk = recCompleteWF ind zero
Tactic:
dsimp [recComplete.aux]
Proof state after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ (ind 0 fun k hk => absurd hk (_ : ¬k < 0)) = recCompleteWF ind 0
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ (ind 0 fun k hk => absurd hk (_ : ¬k < 0)) = recCompleteWF ind 0
Tactic:
unfold recCompleteWF
Proof state after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ (ind 0 fun k hk => absurd hk (_ : ¬k < 0)) = ind 0 fun k x => recCompleteWF ind k
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ (ind 0 fun k hk => absurd hk (_ : ¬k < 0)) = ind 0 fun k x => recCompleteWF ind k
Tactic:
apply congrArg
Proof state after:
case h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ (fun k hk => absurd hk (_ : ¬k < 0)) = fun k x => recCompleteWF ind k
Theorem: Nat.recComplete_eq
Proof state before:
case h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk : zero ≤ succ n
⊢ (fun k hk => absurd hk (_ : ¬k < 0)) = fun k x => recCompleteWF ind k
Tactic:
funext k hk
Proof state after:
case h.h.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk✝ : zero ≤ succ n
k : Nat
hk : k < 0
⊢ absurd hk (_ : ¬k < 0) = recCompleteWF ind k
Theorem: Nat.recComplete_eq
Proof state before:
case h.h.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
hk✝ : zero ≤ succ n
k : Nat
hk : k < 0
⊢ absurd hk (_ : ¬k < 0) = recCompleteWF ind k
Tactic:
cases hk
Proof state after:
no goals