internlm/Lean-Github huggingface dataset:
Theorem: Nat.sqPow_eq_gpow
Proof state before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ (if n % 2 = 1 then a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) else gpow a (n / 2 + 1) * gpow a (n / 2 + 1)) =
    gpow a (n + 2)
Tactic:
case pos hodd =>
  rw [if_pos hodd]
  conv =>
    lhs; change gpow a (n/2 + 2) * gpow a (n/2 + 1)
    rw [←gpow_add one_mul assoc]
  apply congrArg
  conv =>
    lhs; rw [Nat.add_assoc, ←Nat.add_assoc 2 (n/2) 1, Nat.add_comm 2, Nat.add_assoc _ 2 1, ←Nat.add_assoc]
    rw [←Nat.mul_two, Nat.mul_comm, Nat.add_comm 2 1, ←Nat.add_assoc, ←hodd]
    rw [Nat.div_add_mod]
Proof state after:
no goals
Theorem: Nat.sqPow_eq_gpow
Proof state before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
⊢ (if n % 2 = 1 then a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) else gpow a (n / 2 + 1) * gpow a (n / 2 + 1)) =
    gpow a (n + 2)
Tactic:
case neg heven =>
  rw [if_neg heven]
  rw [←gpow_add one_mul assoc]
  have : n % 2 = 0 := Or.resolve_right (Nat.mod_two_eq_zero_or_one n) heven
  apply congrArg
  conv =>
    lhs; rw [Nat.add_assoc, ←Nat.add_assoc 1, Nat.add_comm 1, Nat.add_assoc _ 1 1, ←Nat.add_assoc]
    rw [←Nat.mul_two, Nat.mul_comm, ←Nat.add_zero (2*(n/2)), ←this]
    rw [Nat.div_add_mod]
Proof state after:
no goals
Theorem: Nat.sqPow_eq_gpow
Proof state before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ (if n % 2 = 1 then a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) else gpow a (n / 2 + 1) * gpow a (n / 2 + 1)) =
    gpow a (n + 2)
Tactic:
rw [if_pos hodd]
Proof state after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) = gpow a (n + 2)
Theorem: Nat.sqPow_eq_gpow
Proof state before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) = gpow a (n + 2)
Tactic:
conv =>
  lhs; change gpow a (n/2 + 2) * gpow a (n/2 + 1)
  rw [←gpow_add one_mul assoc]
Proof state after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ gpow a (n / 2 + 2 + (n / 2 + 1)) = gpow a (n + 2)
Theorem: Nat.sqPow_eq_gpow
Proof state before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ gpow a (n / 2 + 2 + (n / 2 + 1)) = gpow a (n + 2)
Tactic:
apply congrArg
Proof state after:
case h
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ n / 2 + 2 + (n / 2 + 1) = n + 2
Theorem: Nat.sqPow_eq_gpow
Proof state before:
case h
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ n / 2 + 2 + (n / 2 + 1) = n + 2
Tactic:
conv =>
  lhs; rw [Nat.add_assoc, ←Nat.add_assoc 2 (n/2) 1, Nat.add_comm 2, Nat.add_assoc _ 2 1, ←Nat.add_assoc]
  rw [←Nat.mul_two, Nat.mul_comm, Nat.add_comm 2 1, ←Nat.add_assoc, ←hodd]
  rw [Nat.div_add_mod]
Proof state after:
no goals
Theorem: Nat.sqPow_eq_gpow
Proof state before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
⊢ (if n % 2 = 1 then a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) else gpow a (n / 2 + 1) * gpow a (n / 2 + 1)) =
    gpow a (n + 2)
Tactic:
rw [if_neg heven]
Proof state after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
⊢ gpow a (n / 2 + 1) * gpow a (n / 2 + 1) = gpow a (n + 2)
Theorem: Nat.sqPow_eq_gpow
Proof state before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
⊢ gpow a (n / 2 + 1) * gpow a (n / 2 + 1) = gpow a (n + 2)
Tactic:
rw [←gpow_add one_mul assoc]
Proof state after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
⊢ gpow a (n / 2 + 1 + (n / 2 + 1)) = gpow a (n + 2)
Theorem: Nat.sqPow_eq_gpow
Proof state before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
⊢ gpow a (n / 2 + 1 + (n / 2 + 1)) = gpow a (n + 2)
Tactic:
have : n % 2 = 0 := Or.resolve_right (Nat.mod_two_eq_zero_or_one n) heven
Proof state after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
this : n % 2 = 0
⊢ gpow a (n / 2 + 1 + (n / 2 + 1)) = gpow a (n + 2)
Theorem: Nat.sqPow_eq_gpow
Proof state before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
this : n % 2 = 0
⊢ gpow a (n / 2 + 1 + (n / 2 + 1)) = gpow a (n + 2)
Tactic:
apply congrArg
Proof state after:
case h
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
this : n % 2 = 0
⊢ n / 2 + 1 + (n / 2 + 1) = n + 2
Theorem: Nat.sqPow_eq_gpow
Proof state before:
case h
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
this : n % 2 = 0
⊢ n / 2 + 1 + (n / 2 + 1) = n + 2
Tactic:
conv =>
  lhs; rw [Nat.add_assoc, ←Nat.add_assoc 1, Nat.add_comm 1, Nat.add_assoc _ 1 1, ←Nat.add_assoc]
  rw [←Nat.mul_two, Nat.mul_comm, ←Nat.add_zero (2*(n/2)), ←this]
  rw [Nat.div_add_mod]
Proof state after:
no goals
Theorem: KVChain.insertWithAux_nil
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
⊢ ∀ {hxnil : hingeable xs KVChain.nil} {a : α} {b : β a} {haxs : boundLeft a xs},
    insertWithAux f xs KVChain.nil hxnil a b haxs =
      { val := (KVChain.cons a b xs haxs, KVChain.nil), property := True.intro }
Tactic:
intros
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
hxnil✝ : hingeable xs KVChain.nil
a✝ : α
b✝ : β a✝
haxs✝ : boundLeft a✝ xs
⊢ insertWithAux f xs KVChain.nil hxnil✝ a✝ b✝ haxs✝ =
    { val := (KVChain.cons a✝ b✝ xs haxs✝, KVChain.nil), property := True.intro }
Theorem: KVChain.insertWithAux_nil
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
hxnil✝ : hingeable xs KVChain.nil
a✝ : α
b✝ : β a✝
haxs✝ : boundLeft a✝ xs
⊢ insertWithAux f xs KVChain.nil hxnil✝ a✝ b✝ haxs✝ =
    { val := (KVChain.cons a✝ b✝ xs haxs✝, KVChain.nil), property := True.intro }
Tactic:
rfl
Proof state after:
no goals
Theorem: KVChain.insertWithAux_cons_rel
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
⊢ ∀ (ha₁a : r a₁ a),
    insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs =
      insertWithAux f (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys
        (_ : hingeable (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys) a b ha₁a
Tactic:
intro hbc
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
hbc : r a₁ a
⊢ insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs =
    insertWithAux f (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys
      (_ : hingeable (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys) a b hbc
Theorem: KVChain.insertWithAux_cons_rel
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
hbc : r a₁ a
⊢ insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs =
    insertWithAux f (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys
      (_ : hingeable (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys) a b hbc
Tactic:
unfold insertWithAux
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
hbc : r a₁ a
⊢ insertWithAux.loop f a b xs (KVChain.cons a₁ b₁ ys ha₁ys).toList
      (_ : List.Ascending (Sigma.relOnFst r) (KVChain.cons a₁ b₁ ys ha₁ys).toList)
      (_ :
        List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
          (KVChain.cons a₁ b₁ ys ha₁ys).toList)
      haxs =
    insertWithAux.loop f a b (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys.toList
      (_ : List.Ascending (Sigma.relOnFst r) ys.toList)
      (_ :
        List.predHead
          (fun b =>
            List.predHead (flip (fun a b => r a.fst b.fst) b) (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)).toList)
          ys.toList)
      hbc
Theorem: KVChain.insertWithAux_cons_rel
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
hbc : r a₁ a
⊢ insertWithAux.loop f a b xs (KVChain.cons a₁ b₁ ys ha₁ys).toList
      (_ : List.Ascending (Sigma.relOnFst r) (KVChain.cons a₁ b₁ ys ha₁ys).toList)
      (_ :
        List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
          (KVChain.cons a₁ b₁ ys ha₁ys).toList)
      haxs =
    insertWithAux.loop f a b (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys.toList
      (_ : List.Ascending (Sigma.relOnFst r) ys.toList)
      (_ :
        List.predHead
          (fun b =>
            List.predHead (flip (fun a b => r a.fst b.fst) b) (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)).toList)
          ys.toList)
      hbc
Tactic:
conv in KVChain.cons a₁ b₁ ys ha₁ys => unfold KVChain.cons
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
hbc : r a₁ a
⊢ insertWithAux.loop f a b xs
      { toList := { fst := a₁, snd := b₁ } :: ys.toList,
          ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }.toList
      (_ :
        List.Ascending (Sigma.relOnFst r)
          { toList := { fst := a₁, snd := b₁ } :: ys.toList,
              ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }.toList)
      (_ :
        List.predHead ((fun a => boundLeft a xs) ∘ Sigma.fst)
          { toList := { fst := a₁, snd := b₁ } :: ys.toList,
              ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }.toList)
      haxs =
    insertWithAux.loop f a b (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys.toList
      (_ : List.Ascending (Sigma.relOnFst r) ys.toList)
      (_ :
        List.predHead
          (fun b =>
            List.predHead (flip (fun a b => r a.fst b.fst) b) (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)).toList)
          ys.toList)
      hbc
Theorem: KVChain.insertWithAux_cons_rel
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
hbc : r a₁ a
⊢ (if hya : r a₁ a then
      insertWithAux.loop f a b
        (KVChain.cons a₁ b₁ xs
          (_ :
            List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
              (KVChain.cons a₁ b₁ ys ha₁ys).toList))
        ys.toList (_ : List.Ascending (Sigma.relOnFst r) ys.toList)
        (_ : List.predHead (Sigma.relOnFst r { fst := a₁, snd := b₁ }) ys.toList) hya
    else
      if hay : r a a₁ then
        {
          val :=
            (KVChain.cons a b xs haxs,
              { toList := { fst := a₁, snd := b₁ } :: ys.toList,
                ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }),
          property :=
            (_ :
              hingeable
                (KVChain.cons a b xs haxs,
                    { toList := { fst := a₁, snd := b₁ } :: ys.toList,
                      ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }).fst
                (KVChain.cons a b xs haxs,
                    { toList := { fst := a₁, snd := b₁ } :: ys.toList,
                      ascend :=
                        (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }).snd) }
      else
        match f a₁ b₁ ((_ : a = { fst := a₁, snd := b₁ }.fst) ▸ b) with
        | none =>
          { val := (xs, { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }),
            property :=
              (_ : hingeable xs { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }) }
        | some z =>
          {
            val :=
              (KVChain.cons a₁ z xs
                  (_ :
                    List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
                      (KVChain.cons a₁ b₁ ys ha₁ys).toList),
                { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }),
            property :=
              (_ :
                hingeable
                  (KVChain.cons a₁ z xs
                    (_ :
                      List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
                        (KVChain.cons a₁ b₁ ys ha₁ys).toList))
                  { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }) }) =
    insertWithAux.loop f a b (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys.toList
      (_ : List.Ascending (Sigma.relOnFst r) ys.toList)
      (_ :
        List.predHead
          (fun b =>
            List.predHead (flip (fun a b => r a.fst b.fst) b) (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)).toList)
          ys.toList)
      hbc
Tactic:
rw [dif_pos hbc]
Proof state after:
no goals
Theorem: KVChain.insertWithAux_cons_flip
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
⊢ ∀ (haa₁ : r a a₁),
    insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs =
      { val := (KVChain.cons a b xs haxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }
Tactic:
intro haa₁
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
haa₁ : r a a₁
⊢ insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs =
    { val := (KVChain.cons a b xs haxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }
Theorem: KVChain.insertWithAux_cons_flip
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
haa₁ : r a a₁
⊢ insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs =
    { val := (KVChain.cons a b xs haxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }
Tactic:
unfold insertWithAux
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
haa₁ : r a a₁
⊢ insertWithAux.loop f a b xs (KVChain.cons a₁ b₁ ys ha₁ys).toList
      (_ : List.Ascending (Sigma.relOnFst r) (KVChain.cons a₁ b₁ ys ha₁ys).toList)
      (_ :
        List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
          (KVChain.cons a₁ b₁ ys ha₁ys).toList)
      haxs =
    { val := (KVChain.cons a b xs haxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }
Theorem: KVChain.insertWithAux_cons_flip
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
haa₁ : r a a₁
⊢ insertWithAux.loop f a b xs (KVChain.cons a₁ b₁ ys ha₁ys).toList
      (_ : List.Ascending (Sigma.relOnFst r) (KVChain.cons a₁ b₁ ys ha₁ys).toList)
      (_ :
        List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
          (KVChain.cons a₁ b₁ ys ha₁ys).toList)
      haxs =
    { val := (KVChain.cons a b xs haxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }
Tactic:
conv in KVChain.cons a₁ b₁ ys ha₁ys => unfold KVChain.cons
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
haa₁ : r a a₁
⊢ insertWithAux.loop f a b xs
      { toList := { fst := a₁, snd := b₁ } :: ys.toList,
          ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }.toList
      (_ :
        List.Ascending (Sigma.relOnFst r)
          { toList := { fst := a₁, snd := b₁ } :: ys.toList,
              ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }.toList)
      (_ :
        List.predHead ((fun a => boundLeft a xs) ∘ Sigma.fst)
          { toList := { fst := a₁, snd := b₁ } :: ys.toList,
              ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }.toList)
      haxs =
    { val := (KVChain.cons a b xs haxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }