internlm/Lean-Github huggingface dataset:
Theorem: Nat.pow_eq_zero
Proof state before:
case left
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m ^ n = 0
⊢ m = 0
Tactic:
rw [ih] at h
Proof state after:
case left
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m = 0 ∧ n ≠ 0
⊢ m = 0
Theorem: Nat.pow_eq_zero
Proof state before:
case left
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m = 0 ∧ n ≠ 0
⊢ m = 0
Tactic:
exact h.1
Proof state after:
no goals
Theorem: Nat.pow_eq_zero
Proof state before:
case right
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m ^ n = 0
⊢ n + 1 ≠ 0
Tactic:
exact Nat.succ_ne_zero _
Proof state after:
no goals
Theorem: Nat.pow_eq_zero
Proof state before:
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m = 0
⊢ m = 0 ∧ n + 1 ≠ 0
Tactic:
constructor
Proof state after:
case left
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m = 0
⊢ m = 0

case right
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m = 0
⊢ n + 1 ≠ 0
Theorem: Nat.pow_eq_zero
Proof state before:
case left
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m = 0
⊢ m = 0
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.pow_eq_zero
Proof state before:
case right
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m = 0
⊢ n + 1 ≠ 0
Tactic:
exact Nat.succ_ne_zero _
Proof state after:
no goals
Theorem: Nat.pow_eq_zero
Proof state before:
case succ.mpr
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m = 0 ∧ n + 1 ≠ 0 → m ^ n = 0 ∨ m = 0
Tactic:
intro ⟨h, _⟩
Proof state after:
case succ.mpr
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
h : m = 0
right✝ : n + 1 ≠ 0
⊢ m ^ n = 0 ∨ m = 0
Theorem: Nat.pow_eq_zero
Proof state before:
case succ.mpr
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
h : m = 0
right✝ : n + 1 ≠ 0
⊢ m ^ n = 0 ∨ m = 0
Tactic:
exact .inr h
Proof state after:
no goals
Theorem: Nat.pow_eq_one
Proof state before:
case zero
m : Nat
⊢ m ^ 0 = 1 ↔ m = 1 ∨ 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.pow_eq_one
Proof state before:
case succ
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
⊢ m ^ (n + 1) = 1 ↔ m = 1 ∨ n + 1 = 0
Tactic:
rw [Nat.pow_succ]
Proof state after:
case succ
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
⊢ m ^ n * m = 1 ↔ m = 1 ∨ n + 1 = 0
Theorem: Nat.pow_eq_one
Proof state before:
case succ
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
⊢ m ^ n * m = 1 ↔ m = 1 ∨ n + 1 = 0
Tactic:
rw [Nat.mul_eq_one]
Proof state after:
case succ
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
⊢ m ^ n = 1 ∧ m = 1 ↔ m = 1 ∨ n + 1 = 0
Theorem: Nat.pow_eq_one
Proof state before:
case succ
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
⊢ m ^ n = 1 ∧ m = 1 ↔ m = 1 ∨ n + 1 = 0
Tactic:
constructor
Proof state after:
case succ.mp
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
⊢ m ^ n = 1 ∧ m = 1 → m = 1 ∨ n + 1 = 0

case succ.mpr
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
⊢ m = 1 ∨ n + 1 = 0 → m ^ n = 1 ∧ m = 1
Theorem: Nat.pow_eq_one
Proof state before:
case succ.mp
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
⊢ m ^ n = 1 ∧ m = 1 → m = 1 ∨ n + 1 = 0
Tactic:
intro ⟨_, h⟩
Proof state after:
case succ.mp
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
left✝ : m ^ n = 1
h : m = 1
⊢ m = 1 ∨ n + 1 = 0
Theorem: Nat.pow_eq_one
Proof state before:
case succ.mp
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
left✝ : m ^ n = 1
h : m = 1
⊢ m = 1 ∨ n + 1 = 0
Tactic:
exact .inl h
Proof state after:
no goals
Theorem: Nat.pow_eq_one
Proof state before:
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
x✝ : m = 1 ∨ n + 1 = 0
h : m = 1
⊢ m ^ n = 1 ∧ m = 1
Tactic:
constructor
Proof state after:
case left
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
x✝ : m = 1 ∨ n + 1 = 0
h : m = 1
⊢ m ^ n = 1

case right
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
x✝ : m = 1 ∨ n + 1 = 0
h : m = 1
⊢ m = 1
Theorem: Nat.pow_eq_one
Proof state before:
case left
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
x✝ : m = 1 ∨ n + 1 = 0
h : m = 1
⊢ m ^ n = 1
Tactic:
rw [ih]
Proof state after:
case left
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
x✝ : m = 1 ∨ n + 1 = 0
h : m = 1
⊢ m = 1 ∨ n = 0
Theorem: Nat.pow_eq_one
Proof state before:
case left
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
x✝ : m = 1 ∨ n + 1 = 0
h : m = 1
⊢ m = 1 ∨ n = 0
Tactic:
exact .inl h
Proof state after:
no goals
Theorem: Nat.pow_eq_one
Proof state before:
case right
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
x✝ : m = 1 ∨ n + 1 = 0
h : m = 1
⊢ m = 1
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.div_le_of_lt_mul_succ
Proof state before:
n k m : Nat
h : n < k * (m + 1)
⊢ n / k ≤ m
Tactic:
have hk : 0 < k := match k with
  | 0 => by rw [Nat.zero_mul] at h; absurd h; exact Nat.not_lt_zero _
  | _+1 => Nat.zero_lt_succ _
Proof state after:
n k m : Nat
h : n < k * (m + 1)
hk : 0 < k
⊢ n / k ≤ m
Theorem: Nat.div_le_of_lt_mul_succ
Proof state before:
n k m : Nat
h : n < k * (m + 1)
hk : 0 < k
⊢ n / k ≤ m
Tactic:
rw [Nat.mul_comm, ←Nat.div_lt_iff_lt_mul hk] at h
Proof state after:
n k m : Nat
h : n / k < m + 1
hk : 0 < k
⊢ n / k ≤ m
Theorem: Nat.div_le_of_lt_mul_succ
Proof state before:
n k m : Nat
h : n / k < m + 1
hk : 0 < k
⊢ n / k ≤ m
Tactic:
exact Nat.le_of_lt_succ h
Proof state after:
no goals
Theorem: Nat.div_le_of_lt_mul_succ
Proof state before:
n k m : Nat
h : n < 0 * (m + 1)
⊢ 0 < 0
Tactic:
rw [Nat.zero_mul] at h
Proof state after:
n k m : Nat
h : n < 0
⊢ 0 < 0
Theorem: Nat.div_le_of_lt_mul_succ
Proof state before:
n k m : Nat
h : n < 0
⊢ 0 < 0
Tactic:
absurd h
Proof state after:
n k m : Nat
h : n < 0
⊢ ¬n < 0
Theorem: Nat.div_le_of_lt_mul_succ
Proof state before:
n k m : Nat
h : n < 0
⊢ ¬n < 0
Tactic:
exact Nat.not_lt_zero _
Proof state after:
no goals
Theorem: Nat.div_le_iff_lt_mul_succ
Proof state before:
k n m : Nat
k0 : 0 < k
h : n / k ≤ m
⊢ n < k * (m + 1)
Tactic:
rw [←Nat.div_add_mod n k, Nat.mul_succ]
Proof state after:
k n m : Nat
k0 : 0 < k
h : n / k ≤ m
⊢ k * (n / k) + n % k < k * m + k
Theorem: Nat.div_le_iff_lt_mul_succ
Proof state before:
k n m : Nat
k0 : 0 < k
h : n / k ≤ m
⊢ k * (n / k) + n % k < k * m + k
Tactic:
apply Nat.lt_of_succ_le
Proof state after:
case h
k n m : Nat
k0 : 0 < k
h : n / k ≤ m
⊢ (k * (n / k) + n % k).succ ≤ k * m + k
Theorem: Nat.div_le_iff_lt_mul_succ
Proof state before:
case h
k n m : Nat
k0 : 0 < k
h : n / k ≤ m
⊢ (k * (n / k) + n % k).succ ≤ k * m + k
Tactic:
apply Nat.add_le_add _ (Nat.mod_lt _ k0)
Proof state after:
k n m : Nat
k0 : 0 < k
h : n / k ≤ m
⊢ k * (n / k) ≤ k * m
Theorem: Nat.div_le_iff_lt_mul_succ
Proof state before:
k n m : Nat
k0 : 0 < k
h : n / k ≤ m
⊢ k * (n / k) ≤ k * m
Tactic:
exact Nat.mul_le_mul_left _ h
Proof state after:
no goals
Theorem: Nat.div_le_iff_lt_mul_succ
Proof state before:
k n m : Nat
k0 : 0 < k
h : n < k * (m + 1)
⊢ n / k ≤ m
Tactic:
rw [Nat.mul_comm, ←Nat.div_lt_iff_lt_mul k0] at h
Proof state after:
k n m : Nat
k0 : 0 < k
h : n / k < m + 1
⊢ n / k ≤ m
Theorem: Nat.div_le_iff_lt_mul_succ
Proof state before:
k n m : Nat
k0 : 0 < k
h : n / k < m + 1
⊢ n / k ≤ m
Tactic:
exact Nat.le_of_lt_succ h
Proof state after:
no goals
Theorem: Nat.div_le_div_right
Proof state before:
m n k : Nat
h : m ≤ n
⊢ m / k ≤ n / k
Tactic:
match k with
| 0 => rw [Nat.div_zero]; exact Nat.zero_le _
| k+1 =>
  apply Nat.div_le_of_lt_mul_succ
  apply Nat.lt_of_le_of_lt h
  conv => lhs; rw [←Nat.div_add_mod n (k+1)]
  rw [Nat.mul_succ, Nat.add_lt_add_iff_left]
  exact Nat.mod_lt _ (Nat.zero_lt_succ _)
Proof state after:
no goals
Theorem: Nat.div_le_div_right
Proof state before:
m n k : Nat
h : m ≤ n
⊢ m / 0 ≤ n / 0
Tactic:
rw [Nat.div_zero]
Proof state after:
m n k : Nat
h : m ≤ n
⊢ 0 ≤ n / 0
Theorem: Nat.div_le_div_right
Proof state before:
m n k : Nat
h : m ≤ n
⊢ 0 ≤ n / 0
Tactic:
exact Nat.zero_le _
Proof state after:
no goals
Theorem: Nat.div_le_div_right
Proof state before:
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ m / (k + 1) ≤ n / (k + 1)
Tactic:
apply Nat.div_le_of_lt_mul_succ
Proof state after:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ m < (k + 1) * (n / (k + 1) + 1)
Theorem: Nat.div_le_div_right
Proof state before:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ m < (k + 1) * (n / (k + 1) + 1)
Tactic:
apply Nat.lt_of_le_of_lt h
Proof state after:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ n < (k + 1) * (n / (k + 1) + 1)
Theorem: Nat.div_le_div_right
Proof state before:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ n < (k + 1) * (n / (k + 1) + 1)
Tactic:
conv => lhs; rw [←Nat.div_add_mod n (k+1)]
Proof state after:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ (k + 1) * (n / (k + 1)) + n % (k + 1) < (k + 1) * (n / (k + 1) + 1)
Theorem: Nat.div_le_div_right
Proof state before:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ (k + 1) * (n / (k + 1)) + n % (k + 1) < (k + 1) * (n / (k + 1) + 1)
Tactic:
rw [Nat.mul_succ, Nat.add_lt_add_iff_left]
Proof state after:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ n % (k + 1) < k + 1
Theorem: Nat.div_le_div_right
Proof state before:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ n % (k + 1) < k + 1
Tactic:
exact Nat.mod_lt _ (Nat.zero_lt_succ _)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.with_addConst
Proof state before:
n : Name
ci : VConstant
f : VEnv → Option VEnv
P : Prop
env env' : VEnv
cis : List VObject
henv : Ordered env
hci : HasObjects env cis → VConstant.WF env ci
IH : ∀ {env1 : VEnv}, Ordered env1 → HasObjects env1 (VObject.const n (some ci) :: cis) → f env1 = some env' → P
hcis : HasObjects env cis
H : addConst env n (some ci) >>= f = some env'
⊢ P
Tactic:
let ⟨env1, h1, henv1⟩ := Option.bind_eq_some.1 H
Proof state after:
n : Name
ci : VConstant
f : VEnv → Option VEnv
P : Prop
env env' : VEnv
cis : List VObject
henv : Ordered env
hci : HasObjects env cis → VConstant.WF env ci
IH : ∀ {env1 : VEnv}, Ordered env1 → HasObjects env1 (VObject.const n (some ci) :: cis) → f env1 = some env' → P
hcis : HasObjects env cis
H : addConst env n (some ci) >>= f = some env'
env1 : VEnv
h1 : addConst env n (some ci) = some env1
henv1 : f env1 = some env'
⊢ P
Theorem: Lean4Lean.VEnv.with_addConst
Proof state before:
n : Name
ci : VConstant
f : VEnv → Option VEnv
P : Prop
env env' : VEnv
cis : List VObject
henv : Ordered env
hci : HasObjects env cis → VConstant.WF env ci
IH : ∀ {env1 : VEnv}, Ordered env1 → HasObjects env1 (VObject.const n (some ci) :: cis) → f env1 = some env' → P
hcis : HasObjects env cis
H : addConst env n (some ci) >>= f = some env'
env1 : VEnv
h1 : addConst env n (some ci) = some env1
henv1 : f env1 = some env'
⊢ P
Tactic:
refine IH (.const henv (by rintro _ ⟨⟩; exact hci hcis) h1) (hcis.const h1) henv1
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.with_addConst
Proof state before:
n : Name
ci : VConstant
f : VEnv → Option VEnv
P : Prop
env env' : VEnv
cis : List VObject
henv : Ordered env
hci : HasObjects env cis → VConstant.WF env ci
IH : ∀ {env1 : VEnv}, Ordered env1 → HasObjects env1 (VObject.const n (some ci) :: cis) → f env1 = some env' → P
hcis : HasObjects env cis
H : addConst env n (some ci) >>= f = some env'
env1 : VEnv
h1 : addConst env n (some ci) = some env1
henv1 : f env1 = some env'
⊢ ∀ (ci_1 : VConstant), some ci = some ci_1 → VConstant.WF env ci_1
Tactic:
rintro _ ⟨⟩
Proof state after:
case refl
n : Name
ci : VConstant
f : VEnv → Option VEnv
P : Prop
env env' : VEnv
cis : List VObject
henv : Ordered env
hci : HasObjects env cis → VConstant.WF env ci
IH : ∀ {env1 : VEnv}, Ordered env1 → HasObjects env1 (VObject.const n (some ci) :: cis) → f env1 = some env' → P
hcis : HasObjects env cis
H : addConst env n (some ci) >>= f = some env'
env1 : VEnv
h1 : addConst env n (some ci) = some env1
henv1 : f env1 = some env'
⊢ VConstant.WF env ci
Theorem: Lean4Lean.VEnv.with_addConst
Proof state before:
case refl
n : Name
ci : VConstant
f : VEnv → Option VEnv
P : Prop
env env' : VEnv
cis : List VObject
henv : Ordered env
hci : HasObjects env cis → VConstant.WF env ci
IH : ∀ {env1 : VEnv}, Ordered env1 → HasObjects env1 (VObject.const n (some ci) :: cis) → f env1 = some env' → P
hcis : HasObjects env cis
H : addConst env n (some ci) >>= f = some env'
env1 : VEnv
h1 : addConst env n (some ci) = some env1
henv1 : f env1 = some env'
⊢ VConstant.WF env ci
Tactic:
exact hci hcis
Proof state after:
no goals
Theorem: Nat.le_iff_exists_add'
Proof state before:
a b : Nat
⊢ a ≤ b ↔ ∃ c, b = c + a
Tactic:
simp [Nat.add_comm, Nat.le_iff_exists_add]
Proof state after:
no goals
Theorem: List.Forall₂.rfl
Proof state before:
α : Type u_1
R : α → α → Prop
l : List α
h : ∀ (a : α), a ∈ l → R a a
⊢ Forall₂ R l l
Tactic:
induction l with
| nil => constructor
| cons _ _ ih => simp at h; exact .cons h.1 (ih h.2)
Proof state after:
no goals
Theorem: List.Forall₂.rfl
Proof state before:
case nil
α : Type u_1
R : α → α → Prop
h : ∀ (a : α), a ∈ [] → R a a
⊢ Forall₂ R [] []
Tactic:
constructor
Proof state after:
no goals
Theorem: List.Forall₂.rfl
Proof state before:
case cons
α : Type u_1
R : α → α → Prop
head✝ : α
tail✝ : List α
ih : (∀ (a : α), a ∈ tail✝ → R a a) → Forall₂ R tail✝ tail✝
h : ∀ (a : α), a ∈ head✝ :: tail✝ → R a a
⊢ Forall₂ R (head✝ :: tail✝) (head✝ :: tail✝)
Tactic:
simp at h
Proof state after:
case cons
α : Type u_1
R : α → α → Prop
head✝ : α
tail✝ : List α
ih : (∀ (a : α), a ∈ tail✝ → R a a) → Forall₂ R tail✝ tail✝
h : R head✝ head✝ ∧ ∀ (a : α), a ∈ tail✝ → R a a
⊢ Forall₂ R (head✝ :: tail✝) (head✝ :: tail✝)
Theorem: List.Forall₂.rfl
Proof state before:
case cons
α : Type u_1
R : α → α → Prop
head✝ : α
tail✝ : List α
ih : (∀ (a : α), a ∈ tail✝ → R a a) → Forall₂ R tail✝ tail✝
h : R head✝ head✝ ∧ ∀ (a : α), a ∈ tail✝ → R a a
⊢ Forall₂ R (head✝ :: tail✝) (head✝ :: tail✝)
Tactic:
exact .cons h.1 (ih h.2)
Proof state after:
no goals
Theorem: List.forall₂_nil_left_iff
Proof state before:
α✝¹ : Type u_1
α✝ : Type u_2
R : α✝¹ → α✝ → Prop
l : List α✝
H : Forall₂ R [] l
⊢ l = []
Tactic:
cases H
Proof state after:
case nil
α✝¹ : Type u_1
α✝ : Type u_2
R : α✝¹ → α✝ → Prop
⊢ [] = []
Theorem: List.forall₂_nil_left_iff
Proof state before:
case nil
α✝¹ : Type u_1
α✝ : Type u_2
R : α✝¹ → α✝ → Prop
⊢ [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: List.forall₂_nil_left_iff
Proof state before:
α✝¹ : Type u_1
α✝ : Type u_2
R : α✝¹ → α✝ → Prop
l : List α✝
⊢ l = [] → Forall₂ R [] l
Tactic:
rintro rfl
Proof state after:
α✝¹ : Type u_1
α✝ : Type u_2
R : α✝¹ → α✝ → Prop
⊢ Forall₂ R [] []
Theorem: List.forall₂_nil_left_iff
Proof state before:
α✝¹ : Type u_1
α✝ : Type u_2
R : α✝¹ → α✝ → Prop
⊢ Forall₂ R [] []
Tactic:
exact Forall₂.nil
Proof state after:
no goals
Theorem: List.forall₂_nil_right_iff
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
R : α✝ → β✝ → Prop
l : List α✝
H : Forall₂ R l []
⊢ l = []
Tactic:
cases H
Proof state after:
case nil
α✝ : Type u_1
β✝ : Type u_2
R : α✝ → β✝ → Prop
⊢ [] = []
Theorem: List.forall₂_nil_right_iff
Proof state before:
case nil
α✝ : Type u_1
β✝ : Type u_2
R : α✝ → β✝ → Prop
⊢ [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: List.forall₂_nil_right_iff
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
R : α✝ → β✝ → Prop
l : List α✝
⊢ l = [] → Forall₂ R l []
Tactic:
rintro rfl
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
R : α✝ → β✝ → Prop
⊢ Forall₂ R [] []
Theorem: List.forall₂_nil_right_iff
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
R : α✝ → β✝ → Prop
⊢ Forall₂ R [] []
Tactic:
exact Forall₂.nil
Proof state after:
no goals
Theorem: List.Forall₂.imp
Proof state before:
α✝¹ : Type u_1
α✝ : Type u_2
R S : α✝¹ → α✝ → Prop
H : ∀ (a : α✝¹) (b : α✝), R a b → S a b
l₁ : List α✝¹
l₂ : List α✝
h : Forall₂ R l₁ l₂
⊢ Forall₂ S l₁ l₂
Tactic:
induction h <;> constructor <;> [(apply H; assumption); assumption]
Proof state after:
no goals
Theorem: List.Forall₂.imp
Proof state before:
case cons.a
α✝¹ : Type u_1
α✝ : Type u_2
R S : α✝¹ → α✝ → Prop
H : ∀ (a : α✝¹) (b : α✝), R a b → S a b
l₁ : List α✝¹
l₂ : List α✝
a✝² : α✝¹
b✝ : α✝
l₁✝ : List α✝¹
l₂✝ : List α✝
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ S a✝² b✝
Tactic:
apply H
Proof state after:
case cons.a.a
α✝¹ : Type u_1
α✝ : Type u_2
R S : α✝¹ → α✝ → Prop
H : ∀ (a : α✝¹) (b : α✝), R a b → S a b
l₁ : List α✝¹
l₂ : List α✝
a✝² : α✝¹
b✝ : α✝
l₁✝ : List α✝¹
l₂✝ : List α✝
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ R a✝² b✝
Theorem: List.Forall₂.imp
Proof state before:
case cons.a.a
α✝¹ : Type u_1
α✝ : Type u_2
R S : α✝¹ → α✝ → Prop
H : ∀ (a : α✝¹) (b : α✝), R a b → S a b
l₁ : List α✝¹
l₂ : List α✝
a✝² : α✝¹
b✝ : α✝
l₁✝ : List α✝¹
l₂✝ : List α✝
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ R a✝² b✝
Tactic:
assumption
Proof state after:
no goals
Theorem: List.forall₂_map_left_iff
Proof state before:
γ : Type u_1
α : Type u_2
α✝ : Type u_3
R : α → α✝ → Prop
f : γ → α
x✝ : List α✝
⊢ Forall₂ R (map f []) x✝ ↔ Forall₂ (fun c b => R (f c) b) [] x✝
Tactic:
simp only [map, forall₂_nil_left_iff]
Proof state after:
no goals
Theorem: List.forall₂_map_left_iff
Proof state before:
γ : Type u_1
α : Type u_2
α✝ : Type u_3
R : α → α✝ → Prop
f : γ → α
a : γ
l : List γ
x✝ : List α✝
⊢ Forall₂ R (map f (a :: l)) x✝ ↔ Forall₂ (fun c b => R (f c) b) (a :: l) x✝
Tactic:
simp only [map, forall₂_cons_left_iff, forall₂_map_left_iff]
Proof state after:
no goals
Theorem: List.forall₂_map_right_iff
Proof state before:
γ : Type u_1
β : Type u_2
α✝ : Type u_3
R : α✝ → β → Prop
f : γ → β
x✝ : List α✝
⊢ Forall₂ R x✝ (map f []) ↔ Forall₂ (fun a c => R a (f c)) x✝ []
Tactic:
simp only [map, forall₂_nil_right_iff]
Proof state after:
no goals
Theorem: List.forall₂_map_right_iff
Proof state before:
γ : Type u_1
β : Type u_2
α✝ : Type u_3
R : α✝ → β → Prop
f : γ → β
x✝ : List α✝
b : γ
u : List γ
⊢ Forall₂ R x✝ (map f (b :: u)) ↔ Forall₂ (fun a c => R a (f c)) x✝ (b :: u)
Tactic:
simp only [map, forall₂_cons_right_iff, forall₂_map_right_iff]
Proof state after:
no goals
Theorem: List.Forall₂.forall_exists_l
Proof state before:
α✝¹ : Type u_1
α✝ : Type u_2
R : α✝¹ → α✝ → Prop
l₁ : List α✝¹
l₂ : List α✝
h : Forall₂ R l₁ l₂
⊢ ∀ (a : α✝¹), a ∈ l₁ → ∃ b, b ∈ l₂ ∧ R a b
Tactic:
induction h with simp [*] | cons _ _ ih => exact fun a h => .inr (ih _ h)
Proof state after:
no goals
Theorem: List.Forall₂.forall_exists_l
Proof state before:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
R : α✝¹ → α✝ → Prop
l₁ : List α✝¹
l₂ : List α✝
a✝² : α✝¹
b✝ : α✝
l₁✝ : List α✝¹
l₂✝ : List α✝
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
ih : ∀ (a : α✝¹), a ∈ l₁✝ → ∃ b, b ∈ l₂✝ ∧ R a b
⊢ ∀ (a : α✝¹), a ∈ l₁✝ → R a b✝ ∨ ∃ a_2, a_2 ∈ l₂✝ ∧ R a a_2
Tactic:
exact fun a h => .inr (ih _ h)
Proof state after:
no goals
Theorem: List.map_id''
Proof state before:
α : Type u_1
f : α → α
l : List α
h : ∀ (x : α), x ∈ l → f x = x
⊢ map f l = l
Tactic:
induction l <;> simp_all
Proof state after:
no goals
Theorem: List.map_fst_lookup
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
inst✝ : BEq β
l : List α
b : β
⊢ lookup b (map (fun a => (f a, a)) l) = find? (fun a => b == f a) l
Tactic:
induction l <;> simp_all [lookup, find?]
Proof state after:
no goals
Theorem: List.append_eq_append_of_length_le
Proof state before:
α : Type u_1
a b c d : List α
h : length a ≤ length c
⊢ a ++ b = c ++ d ↔ ∃ a', c = a ++ a' ∧ b = a' ++ d
Tactic:
rw [append_eq_append_iff, or_iff_left_iff_imp]
Proof state after:
α : Type u_1
a b c d : List α
h : length a ≤ length c
⊢ (∃ c', a = c ++ c' ∧ d = c' ++ b) → ∃ a', c = a ++ a' ∧ b = a' ++ d
Theorem: List.append_eq_append_of_length_le
Proof state before:
α : Type u_1
a b c d : List α
h : length a ≤ length c
⊢ (∃ c', a = c ++ c' ∧ d = c' ++ b) → ∃ a', c = a ++ a' ∧ b = a' ++ d
Tactic:
rintro ⟨c', rfl, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
b c c' : List α
h : length (c ++ c') ≤ length c
⊢ ∃ a', c = c ++ c' ++ a' ∧ b = a' ++ (c' ++ b)
Theorem: List.append_eq_append_of_length_le
Proof state before:
case intro.intro
α : Type u_1
b c c' : List α
h : length (c ++ c') ≤ length c
⊢ ∃ a', c = c ++ c' ++ a' ∧ b = a' ++ (c' ++ b)
Tactic:
rw [← Nat.add_zero c.length, length_append,
  Nat.add_le_add_iff_left, Nat.le_zero, length_eq_zero] at h
Proof state after:
case intro.intro
α : Type u_1
b c c' : List α
h : c' = []
⊢ ∃ a', c = c ++ c' ++ a' ∧ b = a' ++ (c' ++ b)
Theorem: List.append_eq_append_of_length_le
Proof state before:
case intro.intro
α : Type u_1
b c c' : List α
h : c' = []
⊢ ∃ a', c = c ++ c' ++ a' ∧ b = a' ++ (c' ++ b)
Tactic:
subst h
Proof state after:
case intro.intro
α : Type u_1
b c : List α
⊢ ∃ a', c = c ++ [] ++ a' ∧ b = a' ++ ([] ++ b)
Theorem: List.append_eq_append_of_length_le
Proof state before:
case intro.intro
α : Type u_1
b c : List α
⊢ ∃ a', c = c ++ [] ++ a' ∧ b = a' ++ ([] ++ b)
Tactic:
exact ⟨[], by simp⟩
Proof state after:
no goals
Theorem: List.append_eq_append_of_length_le
Proof state before:
α : Type u_1
b c : List α
⊢ c = c ++ [] ++ [] ∧ b = [] ++ ([] ++ b)
Tactic:
simp
Proof state after:
no goals
Theorem: Array.get_modify
Proof state before:
α : Type ?u.21452
f : α → α
arr : Array α
x i : Nat
h : i < size arr
⊢ i < size (modify arr x f)
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Array.get_modify
Proof state before:
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
⊢ get (modify arr x f) { val := i, isLt := ⋯ } =
    if x = i then f (get arr { val := i, isLt := h }) else get arr { val := i, isLt := h }
Tactic:
simp [modify, modifyM, Id.run]
Proof state after:
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
⊢ (if h : x < size arr then set arr { val := x, isLt := h } (f arr[x]) else arr)[i] = if x = i then f arr[i] else arr[i]
Theorem: Array.get_modify
Proof state before:
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
⊢ (if h : x < size arr then set arr { val := x, isLt := h } (f arr[x]) else arr)[i] = if x = i then f arr[i] else arr[i]
Tactic:
split
Proof state after:
case inl
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
h✝ : x < size arr
⊢ (set arr { val := x, isLt := h✝ } (f arr[x]))[i] = if x = i then f arr[i] else arr[i]

case inr
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
h✝ : ¬x < size arr
⊢ arr[i] = if x = i then f arr[i] else arr[i]
Theorem: Array.get_modify
Proof state before:
case inl
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
h✝ : x < size arr
⊢ (set arr { val := x, isLt := h✝ } (f arr[x]))[i] = if x = i then f arr[i] else arr[i]
Tactic:
simp [get_set _ _ _ h]
Proof state after:
case inl
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
h✝ : x < size arr
⊢ (if x = i then f arr[x] else arr[i]) = if x = i then f arr[i] else arr[i]
Theorem: Array.get_modify
Proof state before:
case inl
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
h✝ : x < size arr
⊢ (if x = i then f arr[x] else arr[i]) = if x = i then f arr[i] else arr[i]
Tactic:
split <;> simp [*]
Proof state after:
no goals
Theorem: Array.get_modify
Proof state before:
case inr
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
h✝ : ¬x < size arr
⊢ arr[i] = if x = i then f arr[i] else arr[i]
Tactic:
rw [if_neg (mt (by rintro rfl; exact h) ‹_›)]
Proof state after:
no goals
Theorem: Array.get_modify
Proof state before:
α : Type u_1
f : α → α
arr : Array α
x i : Nat
h : i < size arr
h✝ : ¬x < size arr
⊢ x = i → ?m.24309
Tactic:
rintro rfl
Proof state after:
α : Type u_1
f : α → α
arr : Array α
x : Nat
h✝ : ¬x < size arr
h : x < size arr
⊢ ?m.24496 h
Theorem: Array.get_modify
Proof state before:
α : Type u_1
f : α → α
arr : Array α
x : Nat
h✝ : ¬x < size arr
h : x < size arr
⊢ ?m.24496 h
Tactic:
exact h
Proof state after:
no goals
Theorem: List.mapM_eq_some
Proof state before:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
l' : List β
⊢ mapM f l = some l' ↔ Forall₂ (fun x x_1 => f x = some x_1) l l'
Tactic:
induction l generalizing l' <;>
  simp [List.mapM_nil, List.mapM_cons, bind, List.forall₂_cons_left_iff, *, pure, @eq_comm _ l']
Proof state after:
no goals
Theorem: Option.bind_eq_none''
Proof state before:
α : Type u_1
β : Type u_2
o : Option α
f : α → Option β
⊢ Option.bind o f = none ↔ ∀ (a : α), o = some a → f a = none
Tactic:
cases o <;> simp
Proof state after:
no goals
Theorem: Option.forall_ne_some
Proof state before:
α : Type u_1
o : Option α
⊢ (∀ (a : α), o ≠ some a) ↔ o = none
Tactic:
cases o <;> simp
Proof state after:
no goals
Theorem: Lean4Lean.liftVar_zero
Proof state before:
n k : Nat
⊢ liftVar n 0 (k + 1) = 0
Tactic:
simp [liftVar]
Proof state after:
no goals
Theorem: Lean4Lean.liftVar_succ
Proof state before:
n i k : Nat
⊢ liftVar n (i + 1) (k + 1) = liftVar n i k + 1
Tactic:
simp [liftVar, Nat.succ_lt_succ_iff]
Proof state after:
n i k : Nat
⊢ (if i < k then i + 1 else n + (i + 1)) = (if i < k then i else n + i) + 1