internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₂ : ℕ
⊢ 0 ≃ 0 → x ^ 0 ≃ x ^ 0
Tactic:
intro (_ : (0 : ℕ) ≃ 0)
Proof state after:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₂ : ℕ
x✝ : 0 ≃ 0
⊢ x ^ 0 ≃ x ^ 0
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₂ : ℕ
x✝ : 0 ≃ 0
⊢ x ^ 0 ≃ x ^ 0
Tactic:
exact Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₂ : ℕ
⊢ ∀ (m : ℕ), 0 ≃ step m → x ^ 0 ≃ x ^ step m
Tactic:
intro (n₂' : ℕ) (_ : 0 ≃ step n₂')
Proof state after:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₂ n₂' : ℕ
x✝ : 0 ≃ step n₂'
⊢ x ^ 0 ≃ x ^ step n₂'
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₂ n₂' : ℕ
x✝ : 0 ≃ step n₂'
⊢ x ^ 0 ≃ x ^ step n₂'
Tactic:
exact absurd ‹0 ≃ step n₂'› (Rel.symm step_neqv_zero)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂ : ℕ
⊢ ∀ (m : ℕ), (∀ {j : ℕ}, m ≃ j → x ^ m ≃ x ^ j) → ∀ {j : ℕ}, step m ≃ j → x ^ step m ≃ x ^ j
Tactic:
intro (n₁' : ℕ) (ih : ∀ {j}, n₁' ≃ j → x ^ n₁' ≃ x ^ j) (n₂ : ℕ)
Proof state after:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ step n₁' ≃ n₂ → x ^ step n₁' ≃ x ^ n₂
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ step n₁' ≃ n₂ → x ^ step n₁' ≃ x ^ n₂
Tactic:
apply cases_on (motive := λ j => step n₁' ≃ j → x ^ step n₁' ≃ x ^ j) n₂
Proof state after:
case zero
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ step n₁' ≃ 0 → x ^ step n₁' ≃ x ^ 0

case step
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ ∀ (m : ℕ), step n₁' ≃ step m → x ^ step n₁' ≃ x ^ step m
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ step n₁' ≃ 0 → x ^ step n₁' ≃ x ^ 0
Tactic:
case zero =>
  intro (_ : step n₁' ≃ 0)
  show x ^ step n₁' ≃ x ^ 0
  exact absurd ‹step n₁' ≃ 0› step_neqv_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ ∀ (m : ℕ), step n₁' ≃ step m → x ^ step n₁' ≃ x ^ step m
Tactic:
case step =>
  intro (n₂' : ℕ) (_ : step n₁' ≃ step n₂')
  show x ^ step n₁' ≃ x ^ step n₂'
  have : n₁' ≃ n₂' := AA.inject ‹step n₁' ≃ step n₂'›
  calc
    _ ≃ x ^ step n₁' := Rel.refl
    _ ≃ x ^ n₁' * x  := pow_step
    _ ≃ x ^ n₂' * x  := AA.substL (ih ‹n₁' ≃ n₂'›)
    _ ≃ x ^ step n₂' := Rel.symm pow_step
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ step n₁' ≃ 0 → x ^ step n₁' ≃ x ^ 0
Tactic:
intro (_ : step n₁' ≃ 0)
Proof state after:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
x✝ : step n₁' ≃ 0
⊢ x ^ step n₁' ≃ x ^ 0
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
x✝ : step n₁' ≃ 0
⊢ x ^ step n₁' ≃ x ^ 0
Tactic:
exact absurd ‹step n₁' ≃ 0› step_neqv_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ ∀ (m : ℕ), step n₁' ≃ step m → x ^ step n₁' ≃ x ^ step m
Tactic:
intro (n₂' : ℕ) (_ : step n₁' ≃ step n₂')
Proof state after:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ n₂' : ℕ
x✝ : step n₁' ≃ step n₂'
⊢ x ^ step n₁' ≃ x ^ step n₂'
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ n₂' : ℕ
x✝ : step n₁' ≃ step n₂'
⊢ x ^ step n₁' ≃ x ^ step n₂'
Tactic:
have : n₁' ≃ n₂' := AA.inject ‹step n₁' ≃ step n₂'›
Proof state after:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ n₂' : ℕ
x✝ : step n₁' ≃ step n₂'
this : n₁' ≃ n₂'
⊢ x ^ step n₁' ≃ x ^ step n₂'
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ n₂' : ℕ
x✝ : step n₁' ≃ step n₂'
this : n₁' ≃ n₂'
⊢ x ^ step n₁' ≃ x ^ step n₂'
Tactic:
calc
  _ ≃ x ^ step n₁' := Rel.refl
  _ ≃ x ^ n₁' * x  := pow_step
  _ ≃ x ^ n₂' * x  := AA.substL (ih ‹n₁' ≃ n₂'›)
  _ ≃ x ^ step n₂' := Rel.symm pow_step
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_compatL_add
Proof state before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ x ^ (n + m) ≃ x ^ n * x ^ m
Tactic:
apply ind_on n
Proof state after:
case zero
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ x ^ (0 + m) ≃ x ^ 0 * x ^ m

case step
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ ∀ (m_1 : ℕ), x ^ (m_1 + m) ≃ x ^ m_1 * x ^ m → x ^ (step m_1 + m) ≃ x ^ step m_1 * x ^ m
Theorem: Lean4Axiomatic.Natural.pow_compatL_add
Proof state before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ x ^ (0 + m) ≃ x ^ 0 * x ^ m
Tactic:
case zero =>
  show x^(0 + m) ≃ x^(0:ℕ) * x^m
  calc
    _ ≃ x^(0 + m)     := Rel.refl
    _ ≃ x^m           := pow_substR AA.identL
    _ ≃ 1 * x^m       := Rel.symm AA.identL
    _ ≃ x^(0:ℕ) * x^m := AA.substL (Rel.symm pow_zero)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_compatL_add
Proof state before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ ∀ (m_1 : ℕ), x ^ (m_1 + m) ≃ x ^ m_1 * x ^ m → x ^ (step m_1 + m) ≃ x ^ step m_1 * x ^ m
Tactic:
case step =>
  intro n' (ih : x^(n' + m) ≃ x^n' * x^m)
  show x^(step n' + m) ≃ x^(step n') * x^m
  calc
    _ ≃ x^(step n' + m)   := Rel.refl
    _ ≃ x^(step (n' + m)) := pow_substR (Rel.symm AA.scompatL)
    _ ≃ x^(n' + m) * x    := pow_step
    _ ≃ (x^n' * x^m) * x  := AA.substL ih
    _ ≃ x^n' * (x^m * x)  := AA.assoc
    _ ≃ x^n' * (x * x^m)  := AA.substR AA.comm
    _ ≃ (x^n' * x) * x^m  := Rel.symm AA.assoc
    _ ≃ x^(step n') * x^m := AA.substL (Rel.symm pow_step)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_compatL_add
Proof state before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ x ^ (0 + m) ≃ x ^ 0 * x ^ m
Tactic:
calc
  _ ≃ x^(0 + m)     := Rel.refl
  _ ≃ x^m           := pow_substR AA.identL
  _ ≃ 1 * x^m       := Rel.symm AA.identL
  _ ≃ x^(0:ℕ) * x^m := AA.substL (Rel.symm pow_zero)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_compatL_add
Proof state before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ ∀ (m_1 : ℕ), x ^ (m_1 + m) ≃ x ^ m_1 * x ^ m → x ^ (step m_1 + m) ≃ x ^ step m_1 * x ^ m
Tactic:
intro n' (ih : x^(n' + m) ≃ x^n' * x^m)
Proof state after:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m n' : ℕ
ih : x ^ (n' + m) ≃ x ^ n' * x ^ m
⊢ x ^ (step n' + m) ≃ x ^ step n' * x ^ m
Theorem: Lean4Axiomatic.Natural.pow_compatL_add
Proof state before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m n' : ℕ
ih : x ^ (n' + m) ≃ x ^ n' * x ^ m
⊢ x ^ (step n' + m) ≃ x ^ step n' * x ^ m
Tactic:
calc
  _ ≃ x^(step n' + m)   := Rel.refl
  _ ≃ x^(step (n' + m)) := pow_substR (Rel.symm AA.scompatL)
  _ ≃ x^(n' + m) * x    := pow_step
  _ ≃ (x^n' * x^m) * x  := AA.substL ih
  _ ≃ x^n' * (x^m * x)  := AA.assoc
  _ ≃ x^n' * (x * x^m)  := AA.substR AA.comm
  _ ≃ (x^n' * x) * x^m  := Rel.symm AA.assoc
  _ ≃ x^(step n') * x^m := AA.substL (Rel.symm pow_step)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_flatten
Proof state before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ (x ^ n) ^ m ≃ x ^ (n * m)
Tactic:
apply ind_on m
Proof state after:
case zero
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ (x ^ n) ^ 0 ≃ x ^ (n * 0)

case step
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ ∀ (m : ℕ), (x ^ n) ^ m ≃ x ^ (n * m) → (x ^ n) ^ step m ≃ x ^ (n * step m)
Theorem: Lean4Axiomatic.Natural.pow_flatten
Proof state before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ (x ^ n) ^ 0 ≃ x ^ (n * 0)
Tactic:
case zero =>
  show (x^n)^0 ≃ x^(n * 0)
  calc
    _ ≃ (x^n)^0   := Rel.refl
    _ ≃ 1         := pow_zero
    _ ≃ x^0       := Rel.symm pow_zero
    _ ≃ x^(n * 0) := pow_substR (Rel.symm mul_zero)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_flatten
Proof state before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ ∀ (m : ℕ), (x ^ n) ^ m ≃ x ^ (n * m) → (x ^ n) ^ step m ≃ x ^ (n * step m)
Tactic:
case step =>
  intro m' (ih : (x^n)^m' ≃ x^(n * m'))
  show (x^n)^(step m') ≃ x^(n * step m')
  calc
    _ ≃ (x^n)^(step m')  := Rel.refl
    _ ≃ (x^n)^m' * x^n   := pow_step
    _ ≃ x^(n * m') * x^n := AA.substL ih
    _ ≃ x^(n * m' + n)   := Rel.symm pow_compatL_add
    _ ≃ x^(n * step m')  := pow_substR (Rel.symm mul_step)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_flatten
Proof state before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ (x ^ n) ^ 0 ≃ x ^ (n * 0)
Tactic:
calc
  _ ≃ (x^n)^0   := Rel.refl
  _ ≃ 1         := pow_zero
  _ ≃ x^0       := Rel.symm pow_zero
  _ ≃ x^(n * 0) := pow_substR (Rel.symm mul_zero)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_flatten
Proof state before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ ∀ (m : ℕ), (x ^ n) ^ m ≃ x ^ (n * m) → (x ^ n) ^ step m ≃ x ^ (n * step m)
Tactic:
intro m' (ih : (x^n)^m' ≃ x^(n * m'))
Proof state after:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m m' : ℕ
ih : (x ^ n) ^ m' ≃ x ^ (n * m')
⊢ (x ^ n) ^ step m' ≃ x ^ (n * step m')
Theorem: Lean4Axiomatic.Natural.pow_flatten
Proof state before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m m' : ℕ
ih : (x ^ n) ^ m' ≃ x ^ (n * m')
⊢ (x ^ n) ^ step m' ≃ x ^ (n * step m')
Tactic:
calc
  _ ≃ (x^n)^(step m')  := Rel.refl
  _ ≃ (x^n)^m' * x^n   := pow_step
  _ ≃ x^(n * m') * x^n := AA.substL ih
  _ ≃ x^(n * m' + n)   := Rel.symm pow_compatL_add
  _ ≃ x^(n * step m')  := pow_substR (Rel.symm mul_step)
Proof state after:
no goals