internlm/Lean-Github huggingface dataset:
Theorem: Sinf.succ_ne_zero
Proof state before:
case a
a : String
n : ℕ
⊢ Ø ⋁ (¬ₛ _ a↗ =ₛ O) [a ≔ fromNat n]
Tactic:
induction n <;> simp at *
Proof state after:
case a.zero
a : String
⊢ Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => O
          | isFalse h => _ a)↗ =ₛ
        O

case a.succ
a : String
n✝ : ℕ
n_ih✝ :
  Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => fromNat n✝
          | isFalse h => _ a)↗ =ₛ
        O
⊢ Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => fromNat n✝↗
          | isFalse h => _ a)↗ =ₛ
        O
Theorem: Sinf.succ_ne_zero
Proof state before:
a : String
⊢ Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => O
          | isFalse h => _ a)↗ =ₛ
        O
Tactic:
case a.zero =>
  rw [String.decEq_refl a]; simp
  constructor <;> try constructor <;> try constructor
  intros p
  contradiction
Proof state after:
no goals
Theorem: Sinf.succ_ne_zero
Proof state before:
a : String
n : ℕ
ih :
  Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => fromNat n
          | isFalse h => _ a)↗ =ₛ
        O
⊢ Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => fromNat n↗
          | isFalse h => _ a)↗ =ₛ
        O
Tactic:
case a.succ n ih =>
  rw [String.decEq_refl a] at *; simp at *
  cases ih
  case S_axiom_neg nv1 nv2 e =>
    constructor <;> try constructor <;> try assumption
    intros p
    contradiction
Proof state after:
no goals
Theorem: Sinf.succ_ne_zero
Proof state before:
a : String
⊢ Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => O
          | isFalse h => _ a)↗ =ₛ
        O
Tactic:
rw [String.decEq_refl a]
Proof state after:
a : String
⊢ Ø ⋁
    ¬ₛ
      (match isTrue (_ : a = a) with
          | isTrue h => O
          | isFalse h => _ a)↗ =ₛ
        O
Theorem: Sinf.succ_ne_zero
Proof state before:
a : String
⊢ Ø ⋁
    ¬ₛ
      (match isTrue (_ : a = a) with
          | isTrue h => O
          | isFalse h => _ a)↗ =ₛ
        O
Tactic:
simp
Proof state after:
a : String
⊢ Ø ⋁ ¬ₛ O↗ =ₛ O
Theorem: Sinf.succ_ne_zero
Proof state before:
a : String
⊢ Ø ⋁ ¬ₛ O↗ =ₛ O
Tactic:
constructor <;> try constructor <;> try constructor
Proof state after:
case a
a : String
⊢ Sinf_const.eval (Sinf_const.coerce (O↗) (NoVars.S NoVars.O)) ≠ Sinf_const.eval (Sinf_const.coerce O NoVars.O)
Theorem: Sinf.succ_ne_zero
Proof state before:
case a
a : String
⊢ Sinf_const.eval (Sinf_const.coerce (O↗) (NoVars.S NoVars.O)) ≠ Sinf_const.eval (Sinf_const.coerce O NoVars.O)
Tactic:
intros p
Proof state after:
case a
a : String
p : Sinf_const.eval (Sinf_const.coerce (O↗) (NoVars.S NoVars.O)) = Sinf_const.eval (Sinf_const.coerce O NoVars.O)
⊢ False
Theorem: Sinf.succ_ne_zero
Proof state before:
case a
a : String
p : Sinf_const.eval (Sinf_const.coerce (O↗) (NoVars.S NoVars.O)) = Sinf_const.eval (Sinf_const.coerce O NoVars.O)
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Sinf.succ_ne_zero
Proof state before:
case nv₂
a : String
⊢ NoVars O
Tactic:
constructor <;> try constructor
Proof state after:
no goals
Theorem: Sinf.succ_ne_zero
Proof state before:
case nv₁.a
a : String
⊢ NoVars O
Tactic:
constructor
Proof state after:
no goals
Theorem: Sinf.succ_ne_zero
Proof state before:
a : String
n : ℕ
ih :
  Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => fromNat n
          | isFalse h => _ a)↗ =ₛ
        O
⊢ Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => fromNat n↗
          | isFalse h => _ a)↗ =ₛ
        O
Tactic:
rw [String.decEq_refl a] at *
Proof state after:
a : String
n : ℕ
ih :
  Ø ⋁
    ¬ₛ
      (match isTrue (_ : a = a) with
          | isTrue h => fromNat n
          | isFalse h => _ a)↗ =ₛ
        O
⊢ Ø ⋁
    ¬ₛ
      (match isTrue (_ : a = a) with
          | isTrue h => fromNat n↗
          | isFalse h => _ a)↗ =ₛ
        O
Theorem: Sinf.succ_ne_zero
Proof state before:
a : String
n : ℕ
ih :
  Ø ⋁
    ¬ₛ
      (match isTrue (_ : a = a) with
          | isTrue h => fromNat n
          | isFalse h => _ a)↗ =ₛ
        O
⊢ Ø ⋁
    ¬ₛ
      (match isTrue (_ : a = a) with
          | isTrue h => fromNat n↗
          | isFalse h => _ a)↗ =ₛ
        O
Tactic:
simp at *
Proof state after:
a : String
n : ℕ
ih : Ø ⋁ ¬ₛ fromNat n↗ =ₛ O
⊢ Ø ⋁ ¬ₛ fromNat n↗↗ =ₛ O
Theorem: Sinf.succ_ne_zero
Proof state before:
a : String
n : ℕ
ih : Ø ⋁ ¬ₛ fromNat n↗ =ₛ O
⊢ Ø ⋁ ¬ₛ fromNat n↗↗ =ₛ O
Tactic:
cases ih
Proof state after:
case S_axiom_neg
a : String
n : ℕ
nv₁✝ : NoVars (fromNat n↗)
nv₂✝ : NoVars O
a✝ : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv₁✝) ≠ Sinf_const.eval (Sinf_const.coerce O nv₂✝)
⊢ Ø ⋁ ¬ₛ fromNat n↗↗ =ₛ O
Theorem: Sinf.succ_ne_zero
Proof state before:
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
⊢ Ø ⋁ ¬ₛ fromNat n↗↗ =ₛ O
Tactic:
case S_axiom_neg nv1 nv2 e =>
  constructor <;> try constructor <;> try assumption
  intros p
  contradiction
Proof state after:
no goals
Theorem: Sinf.succ_ne_zero
Proof state before:
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
⊢ Ø ⋁ ¬ₛ fromNat n↗↗ =ₛ O
Tactic:
constructor <;> try constructor <;> try assumption
Proof state after:
case a
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
⊢ Sinf_const.eval (Sinf_const.coerce (fromNat n↗↗) (NoVars.S nv1)) ≠ Sinf_const.eval (Sinf_const.coerce O NoVars.O)
Theorem: Sinf.succ_ne_zero
Proof state before:
case a
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
⊢ Sinf_const.eval (Sinf_const.coerce (fromNat n↗↗) (NoVars.S nv1)) ≠ Sinf_const.eval (Sinf_const.coerce O NoVars.O)
Tactic:
intros p
Proof state after:
case a
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
p : Sinf_const.eval (Sinf_const.coerce (fromNat n↗↗) (NoVars.S nv1)) = Sinf_const.eval (Sinf_const.coerce O NoVars.O)
⊢ False
Theorem: Sinf.succ_ne_zero
Proof state before:
case a
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
p : Sinf_const.eval (Sinf_const.coerce (fromNat n↗↗) (NoVars.S nv1)) = Sinf_const.eval (Sinf_const.coerce O NoVars.O)
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Sinf.succ_ne_zero
Proof state before:
case nv₂
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
⊢ NoVars O
Tactic:
constructor <;> try assumption
Proof state after:
no goals
Theorem: Sinf.succ_ne_zero
Proof state before:
case nv₁.a
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
⊢ NoVars (fromNat n↗)
Tactic:
assumption
Proof state after:
no goals
Theorem: NoVars.fromNat
Proof state before:
n : ℕ
⊢ NoVars (Sinf_term.fromNat n)
Tactic:
induction n <;> try constructor <;> assumption
Proof state after:
no goals
Theorem: NoVars.fromNat
Proof state before:
case succ
n✝ : ℕ
n_ih✝ : NoVars (Sinf_term.fromNat n✝)
⊢ NoVars (Sinf_term.fromNat (Nat.succ n✝))
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
θ : Sinf_term
nv₁ nv₂ : NoVars θ
⊢ nv₁ = nv₂
Tactic:
induction θ <;> try contradiction
Proof state after:
case O
nv₁ nv₂ : NoVars Sinf_term.O
⊢ nv₁ = nv₂

case S
a✝ : Sinf_term
a_ih✝ : ∀ (nv₁ nv₂ : NoVars a✝), nv₁ = nv₂
nv₁ nv₂ : NoVars (a✝↗)
⊢ nv₁ = nv₂

case plus
a✝¹ a✝ : Sinf_term
a_ih✝¹ : ∀ (nv₁ nv₂ : NoVars a✝¹), nv₁ = nv₂
a_ih✝ : ∀ (nv₁ nv₂ : NoVars a✝), nv₁ = nv₂
nv₁ nv₂ : NoVars (a✝¹ +ₛ a✝)
⊢ nv₁ = nv₂

case times
a✝¹ a✝ : Sinf_term
a_ih✝¹ : ∀ (nv₁ nv₂ : NoVars a✝¹), nv₁ = nv₂
a_ih✝ : ∀ (nv₁ nv₂ : NoVars a✝), nv₁ = nv₂
nv₁ nv₂ : NoVars (a✝¹ *ₛ a✝)
⊢ nv₁ = nv₂
Theorem: NoVars.unique
Proof state before:
nv₁ nv₂ : NoVars Sinf_term.O
⊢ nv₁ = nv₂
Tactic:
case O => cases nv₁; cases nv₂; rfl
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₁ nv₂ : NoVars (θ↗)
⊢ nv₁ = nv₂
Tactic:
case S θ ih =>
  cases nv₁; case S nv₁ => cases nv₂; case S nv₂ =>
  apply congrArg; exact (ih nv₁ nv₂)
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁ nv₂ : NoVars (θ₁ +ₛ θ₂)
⊢ nv₁ = nv₂
Tactic:
case plus θ₁ θ₂ ih₁ ih₂ =>
  cases nv₁; case plus nv₁₁ nv₂₁ => cases nv₂; case plus nv₁₂ nv₂₂ =>
  apply congrArg₂; exact (ih₁ nv₁₁ nv₁₂); exact (ih₂ nv₂₁ nv₂₂)
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁ nv₂ : NoVars (θ₁ *ₛ θ₂)
⊢ nv₁ = nv₂
Tactic:
case times θ₁ θ₂ ih₁ ih₂ =>
  cases nv₁; case times nv₁₁ nv₂₁ => cases nv₂; case times nv₁₂ nv₂₂ =>
  apply congrArg₂; exact (ih₁ nv₁₁ nv₁₂); exact (ih₂ nv₂₁ nv₂₂)
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
case var
a✝ : String
nv₁ nv₂ : NoVars _ a✝
⊢ nv₁ = nv₂
Tactic:
contradiction
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
nv₁ nv₂ : NoVars Sinf_term.O
⊢ nv₁ = nv₂
Tactic:
cases nv₁
Proof state after:
case O
nv₂ : NoVars Sinf_term.O
⊢ O = nv₂
Theorem: NoVars.unique
Proof state before:
case O
nv₂ : NoVars Sinf_term.O
⊢ O = nv₂
Tactic:
cases nv₂
Proof state after:
case O.O

⊢ O = O
Theorem: NoVars.unique
Proof state before:
case O.O

⊢ O = O
Tactic:
rfl
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₁ nv₂ : NoVars (θ↗)
⊢ nv₁ = nv₂
Tactic:
cases nv₁
Proof state after:
case S
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₂ : NoVars (θ↗)
a✝ : NoVars θ
⊢ S a✝ = nv₂
Theorem: NoVars.unique
Proof state before:
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₂ : NoVars (θ↗)
nv₁ : NoVars θ
⊢ S nv₁ = nv₂
Tactic:
case S nv₁ => cases nv₂; case S nv₂ =>
apply congrArg; exact (ih nv₁ nv₂)
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₂ : NoVars (θ↗)
nv₁ : NoVars θ
⊢ S nv₁ = nv₂
Tactic:
cases nv₂
Proof state after:
case S
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₁ a✝ : NoVars θ
⊢ S nv₁ = S a✝
Theorem: NoVars.unique
Proof state before:
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₁ nv₂ : NoVars θ
⊢ S nv₁ = S nv₂
Tactic:
case S nv₂ =>
apply congrArg; exact (ih nv₁ nv₂)
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₁ nv₂ : NoVars θ
⊢ S nv₁ = S nv₂
Tactic:
apply congrArg
Proof state after:
case h
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₁ nv₂ : NoVars θ
⊢ nv₁ = nv₂
Theorem: NoVars.unique
Proof state before:
case h
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₁ nv₂ : NoVars θ
⊢ nv₁ = nv₂
Tactic:
exact (ih nv₁ nv₂)
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁ nv₂ : NoVars (θ₁ +ₛ θ₂)
⊢ nv₁ = nv₂
Tactic:
cases nv₁
Proof state after:
case plus
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₂ : NoVars (θ₁ +ₛ θ₂)
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
⊢ plus a✝¹ a✝ = nv₂
Theorem: NoVars.unique
Proof state before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₂ : NoVars (θ₁ +ₛ θ₂)
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
⊢ plus nv₁₁ nv₂₁ = nv₂
Tactic:
case plus nv₁₁ nv₂₁ => cases nv₂; case plus nv₁₂ nv₂₂ =>
apply congrArg₂; exact (ih₁ nv₁₁ nv₁₂); exact (ih₂ nv₂₁ nv₂₂)
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₂ : NoVars (θ₁ +ₛ θ₂)
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
⊢ plus nv₁₁ nv₂₁ = nv₂
Tactic:
cases nv₂
Proof state after:
case plus
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
⊢ plus nv₁₁ nv₂₁ = plus a✝¹ a✝
Theorem: NoVars.unique
Proof state before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ plus nv₁₁ nv₂₁ = plus nv₁₂ nv₂₂
Tactic:
case plus nv₁₂ nv₂₂ =>
apply congrArg₂; exact (ih₁ nv₁₁ nv₁₂); exact (ih₂ nv₂₁ nv₂₂)
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ plus nv₁₁ nv₂₁ = plus nv₁₂ nv₂₂
Tactic:
apply congrArg₂
Proof state after:
case hx
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₁₁ = nv₁₂

case hy
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₂₁ = nv₂₂
Theorem: NoVars.unique
Proof state before:
case hx
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₁₁ = nv₁₂

case hy
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₂₁ = nv₂₂
Tactic:
exact (ih₁ nv₁₁ nv₁₂)
Proof state after:
case hy
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₂₁ = nv₂₂
Theorem: NoVars.unique
Proof state before:
case hy
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₂₁ = nv₂₂
Tactic:
exact (ih₂ nv₂₁ nv₂₂)
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁ nv₂ : NoVars (θ₁ *ₛ θ₂)
⊢ nv₁ = nv₂
Tactic:
cases nv₁
Proof state after:
case times
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₂ : NoVars (θ₁ *ₛ θ₂)
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
⊢ times a✝¹ a✝ = nv₂
Theorem: NoVars.unique
Proof state before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₂ : NoVars (θ₁ *ₛ θ₂)
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
⊢ times nv₁₁ nv₂₁ = nv₂
Tactic:
case times nv₁₁ nv₂₁ => cases nv₂; case times nv₁₂ nv₂₂ =>
apply congrArg₂; exact (ih₁ nv₁₁ nv₁₂); exact (ih₂ nv₂₁ nv₂₂)
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₂ : NoVars (θ₁ *ₛ θ₂)
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
⊢ times nv₁₁ nv₂₁ = nv₂
Tactic:
cases nv₂
Proof state after:
case times
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
⊢ times nv₁₁ nv₂₁ = times a✝¹ a✝
Theorem: NoVars.unique
Proof state before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ times nv₁₁ nv₂₁ = times nv₁₂ nv₂₂
Tactic:
case times nv₁₂ nv₂₂ =>
apply congrArg₂; exact (ih₁ nv₁₁ nv₁₂); exact (ih₂ nv₂₁ nv₂₂)
Proof state after:
no goals
Theorem: NoVars.unique
Proof state before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ times nv₁₁ nv₂₁ = times nv₁₂ nv₂₂
Tactic:
apply congrArg₂
Proof state after:
case hx
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₁₁ = nv₁₂

case hy
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₂₁ = nv₂₂
Theorem: String.decEq_refl
Proof state before:
s : String
⊢ decEq s s = isTrue (_ : s = s)
Tactic:
cases String.decEq s s <;> try contradiction
Proof state after:
case isTrue
s : String
h✝ : s = s
⊢ isTrue h✝ = isTrue (_ : s = s)
Theorem: String.decEq_refl
Proof state before:
case isTrue
s : String
h✝ : s = s
⊢ isTrue h✝ = isTrue (_ : s = s)
Tactic:
simp
Proof state after:
no goals
Theorem: String.decEq_refl
Proof state before:
case isFalse
s : String
h✝ : ¬s = s
⊢ isFalse h✝ = isTrue (_ : s = s)
Tactic:
contradiction
Proof state after:
no goals
Theorem: Option.map_inj
Proof state before:
A B : Type
f : A → B
inj : Injective f
x y : Option A
⊢ Option.map f x = Option.map f y → x = y
Tactic:
intros p
Proof state after:
A B : Type
f : A → B
inj : Injective f
x y : Option A
p : Option.map f x = Option.map f y
⊢ x = y
Theorem: Option.map_inj
Proof state before:
A B : Type
f : A → B
inj : Injective f
x y : Option A
p : Option.map f x = Option.map f y
⊢ x = y
Tactic:
induction x <;> induction y <;> try trivial
Proof state after:
case some.some
A B : Type
f : A → B
inj : Injective f
val✝¹ val✝ : A
p : Option.map f (some val✝¹) = Option.map f (some val✝)
⊢ some val✝¹ = some val✝
Theorem: Option.map_inj
Proof state before:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
⊢ some v = some v'
Tactic:
case some.some v v' =>
  have obvs : ∀ a, Option.map f (some a) = some (f a) := by intros a; rfl
  rw [obvs v, obvs v'] at p
  rw [Option.some_inj] at p
  apply congrArg; apply inj; assumption
Proof state after:
no goals
Theorem: Option.map_inj
Proof state before:
case some.none
A B : Type
f : A → B
inj : Injective f
val✝ : A
p : Option.map f (some val✝) = Option.map f none
⊢ some val✝ = none
Tactic:
trivial
Proof state after:
no goals
Theorem: Option.map_inj
Proof state before:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
⊢ some v = some v'
Tactic:
have obvs : ∀ a, Option.map f (some a) = some (f a) := by intros a; rfl
Proof state after:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ some v = some v'
Theorem: Option.map_inj
Proof state before:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ some v = some v'
Tactic:
rw [obvs v, obvs v'] at p
Proof state after:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : some (f v) = some (f v')
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ some v = some v'
Theorem: Option.map_inj
Proof state before:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : some (f v) = some (f v')
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ some v = some v'
Tactic:
rw [Option.some_inj] at p
Proof state after:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : f v = f v'
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ some v = some v'
Theorem: Option.map_inj
Proof state before:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : f v = f v'
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ some v = some v'
Tactic:
apply congrArg
Proof state after:
case h
A B : Type
f : A → B
inj : Injective f
v v' : A
p : f v = f v'
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ v = v'
Theorem: Option.map_inj
Proof state before:
case h
A B : Type
f : A → B
inj : Injective f
v v' : A
p : f v = f v'
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ v = v'
Tactic:
apply inj
Proof state after:
case h.a
A B : Type
f : A → B
inj : Injective f
v v' : A
p : f v = f v'
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ f v = f v'
Theorem: Option.map_inj
Proof state before:
case h.a
A B : Type
f : A → B
inj : Injective f
v v' : A
p : f v = f v'
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ f v = f v'
Tactic:
assumption
Proof state after:
no goals
Theorem: Option.map_inj
Proof state before:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
⊢ ∀ (a : A), Option.map f (some a) = some (f a)
Tactic:
intros a
Proof state after:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
a : A
⊢ Option.map f (some a) = some (f a)
Theorem: Option.map_inj
Proof state before:
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
a : A
⊢ Option.map f (some a) = some (f a)
Tactic:
rfl
Proof state after:
no goals
Theorem: Network.Graph.Class.reactionInputScheme_type_right
Proof state before:
graph : Graph
cls : Class graph
child : Child cls
childOutput : ((fun child => interface (Child.class child) Reactor.InterfaceKind.outputs) child).vars
⊢ Interface.Scheme.type (reactionInputScheme cls) (Sum.inr { fst := child, snd := childOutput }) =
    Interface.Scheme.type (interface (Child.class child) Reactor.InterfaceKind.outputs) childOutput
Tactic:
simp [Interface.Scheme.bUnion_type]
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.refl
Proof state before:
graph : Graph
start : Class graph
child✝ : Class.Child start
subpath : Path graph (Class.Child.class child✝)
⊢ Path.cons child✝ subpath ≂ Path.cons child✝ subpath
Tactic:
have ⟨_, h⟩ := Succ.cons subpath
Proof state after:
graph : Graph
start : Class graph
child✝ : Class.Child start
subpath : Path graph (Class.Child.class child✝)
w✝ : Path graph start
h : Path.cons child✝ subpath ≻ w✝
⊢ Path.cons child✝ subpath ≂ Path.cons child✝ subpath
Theorem: Network.Graph.Path.Sibling.refl
Proof state before:
graph : Graph
start : Class graph
child✝ : Class.Child start
subpath : Path graph (Class.Child.class child✝)
w✝ : Path graph start
h : Path.cons child✝ subpath ≻ w✝
⊢ Path.cons child✝ subpath ≂ Path.cons child✝ subpath
Tactic:
exact cons h h
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ path₁ ≂ path₂ ↔ prefix? path₁ = prefix? path₂
Tactic:
constructor
Proof state after:
case mp
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ path₁ ≂ path₂ → prefix? path₁ = prefix? path₂

case mpr
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ prefix? path₁ = prefix? path₂ → path₁ ≂ path₂
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ path₁ ≂ path₂ → prefix? path₁ = prefix? path₂
Tactic:
case mp =>
  cases path₁ <;> cases path₂
  case nil.nil => simp
  case cons.cons => intro h; cases h; simp_all [Succ]
  case nil.cons => intro h; cases h; case _ h _ => have := h.isCons; contradiction
  case cons.nil => intro h; cases h; case _ h   => have := h.isCons; contradiction
Proof state after:
no goals