internlm/Lean-Github huggingface dataset:
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (fun x => r b x) bs
Tactic:
exact hhook.snd_Ascending.forAll_of_tail
Proof state after:
no goals
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (fun a => forAll (r a) bs) as
Tactic:
exact hlt.right
Proof state after:
no goals
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending (flip r) (a :: as)
Tactic:
apply List.Ascending.cons_of_forAll _ hhook.fst_revAscending
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (flip r a) as
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (flip r a) as
Tactic:
apply List.forAll_of_forAll (λ x (h : r x b) => trans h hba)
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (fun x => r x b) as
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (fun x => r x b) as
Tactic:
exact hlt.left
Proof state after:
no goals
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending r bs
Tactic:
exact hhook.snd_Ascending.tail
Proof state after:
no goals
Theorem: List.HookedAscending.consL
Proof state before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
⊢ forAll (fun x => r x a) as → forAll (r a) bs → HookedAscending r as bs → HookedAscending r (a :: as) bs
Tactic:
intro has hbs hhook
Proof state after:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ HookedAscending r (a :: as) bs
Theorem: List.HookedAscending.consL
Proof state before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ HookedAscending r (a :: as) bs
Tactic:
constructor
Proof state after:
case fst_lt_snd
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ List.forAllRel r (a :: as) bs

case fst_revAscending
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ Ascending (flip r) (a :: as)

case snd_Ascending
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ Ascending r bs
Theorem: List.HookedAscending.consL
Proof state before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ List.forAllRel r (a :: as) bs
Tactic:
case fst_lt_snd =>
  simp [List.forAllRel_cons_left]
  exact And.intro hbs hhook.fst_lt_snd
Proof state after:
no goals
Theorem: List.HookedAscending.consL
Proof state before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ Ascending (flip r) (a :: as)
Tactic:
case fst_revAscending =>
  exact List.Ascending.cons_of_forAll has hhook.fst_revAscending
Proof state after:
no goals
Theorem: List.HookedAscending.consL
Proof state before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ Ascending r bs
Tactic:
case snd_Ascending => exact hhook.snd_Ascending
Proof state after:
no goals
Theorem: List.HookedAscending.consL
Proof state before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ List.forAllRel r (a :: as) bs
Tactic:
simp [List.forAllRel_cons_left]
Proof state after:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ forAll (r a) bs ∧ List.forAllRel r as bs
Theorem: List.HookedAscending.consL
Proof state before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ forAll (r a) bs ∧ List.forAllRel r as bs
Tactic:
exact And.intro hbs hhook.fst_lt_snd
Proof state after:
no goals
Theorem: List.HookedAscending.consL
Proof state before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ Ascending (flip r) (a :: as)
Tactic:
exact List.Ascending.cons_of_forAll has hhook.fst_revAscending
Proof state after:
no goals
Theorem: List.HookedAscending.consL
Proof state before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ Ascending r bs
Tactic:
exact hhook.snd_Ascending
Proof state after:
no goals
Theorem: List.HookedAscending.consR
Proof state before:
α : Type u_1
r : α → α → Prop
as : List α
b : α
bs : List α
⊢ forAll (fun x => r x b) as → forAll (r b) bs → HookedAscending r as bs → HookedAscending r as (b :: bs)
Tactic:
intro has hbs hhook
Proof state after:
α : Type u_1
r : α → α → Prop
as : List α
b : α
bs : List α
has : forAll (fun x => r x b) as
hbs : forAll (r b) bs
hhook : HookedAscending r as bs
⊢ HookedAscending r as (b :: bs)
Theorem: List.HookedAscending.consR
Proof state before:
α : Type u_1
r : α → α → Prop
as : List α
b : α
bs : List α
has : forAll (fun x => r x b) as
hbs : forAll (r b) bs
hhook : HookedAscending r as bs
⊢ HookedAscending r as (b :: bs)
Tactic:
have : ∀ a b, flip (flip r) a b → r a b := λ _ _ => id
Proof state after:
α : Type u_1
r : α → α → Prop
as : List α
b : α
bs : List α
has : forAll (fun x => r x b) as
hbs : forAll (r b) bs
hhook : HookedAscending r as bs
this : ∀ (a b : α), flip (flip r) a b → r a b
⊢ HookedAscending r as (b :: bs)
Theorem: List.HookedAscending.consR
Proof state before:
α : Type u_1
r : α → α → Prop
as : List α
b : α
bs : List α
has : forAll (fun x => r x b) as
hbs : forAll (r b) bs
hhook : HookedAscending r as bs
this : ∀ (a b : α), flip (flip r) a b → r a b
⊢ HookedAscending r as (b :: bs)
Tactic:
exact (hhook.flip.consL hbs has).flip.of_implies this
Proof state after:
no goals
Theorem: List.HookedAscending.tailL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
⊢ HookedAscending r (a :: as) bs → HookedAscending r as bs
Tactic:
intro hhook
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ HookedAscending r as bs
Theorem: List.HookedAscending.tailL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ HookedAscending r as bs
Tactic:
constructor
Proof state after:
case fst_lt_snd
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ List.forAllRel r as bs

case fst_revAscending
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending (flip r) as

case snd_Ascending
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r bs
Theorem: List.HookedAscending.tailL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ List.forAllRel r as bs
Tactic:
case fst_lt_snd =>
  have := hhook.fst_lt_snd
  simp [List.forAllRel_cons_left] at this
  exact this.right
Proof state after:
no goals
Theorem: List.HookedAscending.tailL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending (flip r) as
Tactic:
case fst_revAscending => exact hhook.fst_revAscending.tail
Proof state after:
no goals
Theorem: List.HookedAscending.tailL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r bs
Tactic:
case snd_Ascending => exact hhook.snd_Ascending
Proof state after:
no goals
Theorem: List.HookedAscending.tailL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ List.forAllRel r as bs
Tactic:
have := hhook.fst_lt_snd
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
this : List.forAllRel r (a :: as) bs
⊢ List.forAllRel r as bs
Theorem: List.HookedAscending.tailL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
this : List.forAllRel r (a :: as) bs
⊢ List.forAllRel r as bs
Tactic:
simp [List.forAllRel_cons_left] at this
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
this : forAll (r a) bs ∧ List.forAllRel r as bs
⊢ List.forAllRel r as bs
Theorem: List.HookedAscending.tailL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
this : forAll (r a) bs ∧ List.forAllRel r as bs
⊢ List.forAllRel r as bs
Tactic:
exact this.right
Proof state after:
no goals
Theorem: List.HookedAscending.tailL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending (flip r) as
Tactic:
exact hhook.fst_revAscending.tail
Proof state after:
no goals
Theorem: List.HookedAscending.tailL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r bs
Tactic:
exact hhook.snd_Ascending
Proof state after:
no goals
Theorem: List.HookedAscending.tailR
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
⊢ HookedAscending r as (b :: bs) → HookedAscending r as bs
Tactic:
intro hhook
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
⊢ HookedAscending r as bs
Theorem: List.HookedAscending.tailR
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
⊢ HookedAscending r as bs
Tactic:
have : Trans (flip r) (flip r) (flip r) :=
  Trans.mk (by simp [flip]; exact flip trans)
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
this : Trans (flip r) (flip r) (flip r)
⊢ HookedAscending r as bs
Theorem: List.HookedAscending.tailR
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
this : Trans (flip r) (flip r) (flip r)
⊢ HookedAscending r as bs
Tactic:
exact hhook.flip.tailL.flip
Proof state after:
no goals
Theorem: List.HookedAscending.tailR
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
⊢ ∀ {a b c : α}, flip r a b → flip r b c → flip r a c
Tactic:
simp [flip]
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
⊢ ∀ {a b c : α}, r b a → r c b → r c a
Theorem: List.HookedAscending.tailR
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
⊢ ∀ {a b c : α}, r b a → r c b → r c a
Tactic:
exact flip trans
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)
⊢ ∀ (a : α) (n : Nat), sqPow a n = gpow a n
Tactic:
intro a n
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)
a : α
n : Nat
⊢ sqPow a n = gpow a n
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)
a : α
n : Nat
⊢ sqPow a n = gpow a n
Tactic:
unfold sqPow
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)
a : α
n : Nat
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) n = gpow a n
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)
a : α
n : Nat
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) n = gpow a n
Tactic:
induction n using recBase2 generalizing a
Proof state after:
case zero
α✝ : 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)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) 0 = gpow a 0

case one
α✝ : 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)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) 1 = gpow a 1

case div2
α✝ : 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
a✝ : ∀ (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 : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n✝ + 2) = 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)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) 0 = gpow a 0
Tactic:
case zero => rfl
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)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) 1 = gpow a 1
Tactic:
case one =>
  rw [recBase2_one]
  exact (mul_one a).symm
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 : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n + 2) = gpow a (n + 2)
Tactic:
case div2 n h_ind =>
  rw [recBase2_div2]
  rw [h_ind a]
  by_cases n % 2 = 1
  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]
  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)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) 0 = gpow a 0
Tactic:
rfl
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)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) 1 = gpow a 1
Tactic:
rw [recBase2_one]
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)
a : α
⊢ a = gpow a 1
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)
a : α
⊢ a = gpow a 1
Tactic:
exact (mul_one a).symm
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 : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n + 2) = gpow a (n + 2)
Tactic:
rw [recBase2_div2]
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 : α
⊢ (if n % 2 = 1 then
      a * recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) *
        recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1)
    else
      recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) *
        recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (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 : α
⊢ (if n % 2 = 1 then
      a * recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) *
        recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1)
    else
      recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) *
        recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1)) =
    gpow a (n + 2)
Tactic:
rw [h_ind a]
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 : α
⊢ (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)
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 : α
⊢ (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:
by_cases n % 2 = 1
Proof state after:
case pos
α✝ : 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 : α
h✝ : 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)

case neg
α✝ : 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 : α
h✝ : ¬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)