internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Natural.pow_distribR_mul
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 y : α
n : ℕ
⊢ (x * y) ^ n ≃ x ^ n * y ^ n
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 y : α
n : ℕ
⊢ (x * y) ^ 0 ≃ x ^ 0 * y ^ 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 y : α
n : ℕ
⊢ ∀ (m : ℕ), (x * y) ^ m ≃ x ^ m * y ^ m → (x * y) ^ step m ≃ x ^ step m * y ^ step m
Theorem: Lean4Axiomatic.Natural.pow_distribR_mul
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 y : α
n : ℕ
⊢ (x * y) ^ 0 ≃ x ^ 0 * y ^ 0
Tactic:
case zero =>
  show (x * y)^0 ≃ x^0 * y^0
  calc
    _ ≃ (x * y)^0 := Rel.refl
    _ ≃ 1         := pow_zero
    _ ≃ 1 * 1     := Rel.symm AA.identR
    _ ≃ x^0 * 1   := AA.substL (Rel.symm pow_zero)
    _ ≃ x^0 * y^0 := AA.substR (Rel.symm pow_zero)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_distribR_mul
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 y : α
n : ℕ
⊢ ∀ (m : ℕ), (x * y) ^ m ≃ x ^ m * y ^ m → (x * y) ^ step m ≃ x ^ step m * y ^ step m
Tactic:
case step =>
  intro n' (ih : (x * y)^n' ≃ x^n' * y^n')
  show (x * y)^(step n') ≃ x^(step n') * y^(step n')
  calc
    _ ≃ (x * y)^(step n')         := Rel.refl
    _ ≃ (x * y)^n' * (x * y)      := pow_step
    _ ≃ (x^n' * y^n') * (x * y)   := AA.substL ih
    _ ≃ (x^n' * x) * (y^n' * y)   := AA.expr_xxfxxff_lr_swap_rl
    _ ≃ x^(step n') * (y^n' * y)  := AA.substL (Rel.symm pow_step)
    _ ≃ x^(step n') * y^(step n') := AA.substR (Rel.symm pow_step)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_distribR_mul
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 y : α
n : ℕ
⊢ (x * y) ^ 0 ≃ x ^ 0 * y ^ 0
Tactic:
calc
  _ ≃ (x * y)^0 := Rel.refl
  _ ≃ 1         := pow_zero
  _ ≃ 1 * 1     := Rel.symm AA.identR
  _ ≃ x^0 * 1   := AA.substL (Rel.symm pow_zero)
  _ ≃ x^0 * y^0 := AA.substR (Rel.symm pow_zero)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_distribR_mul
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 y : α
n : ℕ
⊢ ∀ (m : ℕ), (x * y) ^ m ≃ x ^ m * y ^ m → (x * y) ^ step m ≃ x ^ step m * y ^ step m
Tactic:
intro n' (ih : (x * y)^n' ≃ x^n' * y^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
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 y : α
n n' : ℕ
ih : (x * y) ^ n' ≃ x ^ n' * y ^ n'
⊢ (x * y) ^ step n' ≃ x ^ step n' * y ^ step n'
Theorem: Lean4Axiomatic.Natural.pow_distribR_mul
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 y : α
n n' : ℕ
ih : (x * y) ^ n' ≃ x ^ n' * y ^ n'
⊢ (x * y) ^ step n' ≃ x ^ step n' * y ^ step n'
Tactic:
calc
  _ ≃ (x * y)^(step n')         := Rel.refl
  _ ≃ (x * y)^n' * (x * y)      := pow_step
  _ ≃ (x^n' * y^n') * (x * y)   := AA.substL ih
  _ ≃ (x^n' * x) * (y^n' * y)   := AA.expr_xxfxxff_lr_swap_rl
  _ ≃ x^(step n') * (y^n' * y)  := AA.substL (Rel.symm pow_step)
  _ ≃ x^(step n') * y^(step n') := AA.substR (Rel.symm pow_step)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_inputs_for_output_zero
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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n : ℕ
⊢ x ^ n ≃ 0 → x ≃ 0 ∧ n ≄ 0
Tactic:
apply ind_on (motive := λ m => x^m ≃ 0 → x ≃ 0 ∧ m ≄ 0) 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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n : ℕ
⊢ x ^ 0 ≃ 0 → x ≃ 0 ∧ 0 ≄ 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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n : ℕ
⊢ ∀ (m : ℕ), (x ^ m ≃ 0 → x ≃ 0 ∧ m ≄ 0) → x ^ step m ≃ 0 → x ≃ 0 ∧ step m ≄ 0
Theorem: Lean4Axiomatic.Natural.pow_inputs_for_output_zero
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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n : ℕ
⊢ x ^ 0 ≃ 0 → x ≃ 0 ∧ 0 ≄ 0
Tactic:
case zero =>
  intro (_ : x^(0:ℕ) ≃ 0)
  show x ≃ 0 ∧ 0 ≄ 0
  have : (1:α) ≃ 0 := calc
    _ ≃ 1   := Rel.refl
    _ ≃ x^0 := Rel.symm pow_zero
    _ ≃ 0   := ‹x^(0:ℕ) ≃ 0›
  exact absurd ‹(1:α) ≃ 0› ‹AP ((1:α) ≄ 0)›.ev
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_inputs_for_output_zero
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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n : ℕ
⊢ ∀ (m : ℕ), (x ^ m ≃ 0 → x ≃ 0 ∧ m ≄ 0) → x ^ step m ≃ 0 → x ≃ 0 ∧ step m ≄ 0
Tactic:
case step =>
  intro (n' : ℕ) (ih : x^n' ≃ 0 → x ≃ 0 ∧ n' ≄ 0) (_ : x^(step n') ≃ 0)
  show x ≃ 0 ∧ step n' ≄ 0
  have : x^n' * x ≃ 0 := AA.eqv_substL pow_step ‹x^(step n') ≃ 0›
  have : x^n' ≃ 0 ∨ x ≃ 0 := AA.zero_prod this
  have : x ≃ 0 :=
    match this with
    | Or.inl (_ : x^n' ≃ 0) => (ih ‹x^n' ≃ 0›).left
    | Or.inr (_ : x ≃ 0) => ‹x ≃ 0›
  have : step n' ≄ 0 := step_neqv_zero
  exact And.intro ‹x ≃ 0› ‹step n' ≄ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_inputs_for_output_zero
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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n : ℕ
⊢ x ^ 0 ≃ 0 → x ≃ 0 ∧ 0 ≄ 0
Tactic:
intro (_ : x^(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
inst✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n : ℕ
x✝ : x ^ 0 ≃ 0
⊢ x ≃ 0 ∧ 0 ≄ 0
Theorem: Lean4Axiomatic.Natural.pow_inputs_for_output_zero
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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n : ℕ
x✝ : x ^ 0 ≃ 0
⊢ x ≃ 0 ∧ 0 ≄ 0
Tactic:
have : (1:α) ≃ 0 := calc
  _ ≃ 1   := Rel.refl
  _ ≃ x^0 := Rel.symm pow_zero
  _ ≃ 0   := ‹x^(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
inst✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n : ℕ
x✝ : x ^ 0 ≃ 0
this : 1 ≃ 0
⊢ x ≃ 0 ∧ 0 ≄ 0
Theorem: Lean4Axiomatic.Natural.pow_inputs_for_output_zero
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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n : ℕ
x✝ : x ^ 0 ≃ 0
this : 1 ≃ 0
⊢ x ≃ 0 ∧ 0 ≄ 0
Tactic:
exact absurd ‹(1:α) ≃ 0› ‹AP ((1:α) ≄ 0)›.ev
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_inputs_for_output_zero
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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n : ℕ
⊢ ∀ (m : ℕ), (x ^ m ≃ 0 → x ≃ 0 ∧ m ≄ 0) → x ^ step m ≃ 0 → x ≃ 0 ∧ step m ≄ 0
Tactic:
intro (n' : ℕ) (ih : x^n' ≃ 0 → x ≃ 0 ∧ n' ≄ 0) (_ : x^(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
inst✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n n' : ℕ
ih : x ^ n' ≃ 0 → x ≃ 0 ∧ n' ≄ 0
x✝ : x ^ step n' ≃ 0
⊢ x ≃ 0 ∧ step n' ≄ 0
Theorem: Lean4Axiomatic.Natural.pow_inputs_for_output_zero
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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n n' : ℕ
ih : x ^ n' ≃ 0 → x ≃ 0 ∧ n' ≄ 0
x✝ : x ^ step n' ≃ 0
⊢ x ≃ 0 ∧ step n' ≄ 0
Tactic:
have : x^n' * x ≃ 0 := AA.eqv_substL pow_step ‹x^(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
inst✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n n' : ℕ
ih : x ^ n' ≃ 0 → x ≃ 0 ∧ n' ≄ 0
x✝ : x ^ step n' ≃ 0
this : x ^ n' * x ≃ 0
⊢ x ≃ 0 ∧ step n' ≄ 0
Theorem: Lean4Axiomatic.Natural.pow_inputs_for_output_zero
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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n n' : ℕ
ih : x ^ n' ≃ 0 → x ≃ 0 ∧ n' ≄ 0
x✝ : x ^ step n' ≃ 0
this : x ^ n' * x ≃ 0
⊢ x ≃ 0 ∧ step n' ≄ 0
Tactic:
have : x^n' ≃ 0 ∨ x ≃ 0 := AA.zero_prod this
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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n n' : ℕ
ih : x ^ n' ≃ 0 → x ≃ 0 ∧ n' ≄ 0
x✝ : x ^ step n' ≃ 0
this✝ : x ^ n' * x ≃ 0
this : x ^ n' ≃ 0 ∨ x ≃ 0
⊢ x ≃ 0 ∧ step n' ≄ 0
Theorem: Lean4Axiomatic.Natural.pow_inputs_for_output_zero
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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n n' : ℕ
ih : x ^ n' ≃ 0 → x ≃ 0 ∧ n' ≄ 0
x✝ : x ^ step n' ≃ 0
this✝ : x ^ n' * x ≃ 0
this : x ^ n' ≃ 0 ∨ x ≃ 0
⊢ x ≃ 0 ∧ step n' ≄ 0
Tactic:
have : x ≃ 0 :=
  match this with
  | Or.inl (_ : x^n' ≃ 0) => (ih ‹x^n' ≃ 0›).left
  | Or.inr (_ : x ≃ 0) => ‹x ≃ 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
inst✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n n' : ℕ
ih : x ^ n' ≃ 0 → x ≃ 0 ∧ n' ≄ 0
x✝ : x ^ step n' ≃ 0
this✝¹ : x ^ n' * x ≃ 0
this✝ : x ^ n' ≃ 0 ∨ x ≃ 0
this : x ≃ 0
⊢ x ≃ 0 ∧ step n' ≄ 0
Theorem: Lean4Axiomatic.Natural.pow_inputs_for_output_zero
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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n n' : ℕ
ih : x ^ n' ≃ 0 → x ≃ 0 ∧ n' ≄ 0
x✝ : x ^ step n' ≃ 0
this✝¹ : x ^ n' * x ≃ 0
this✝ : x ^ n' ≃ 0 ∨ x ≃ 0
this : x ≃ 0
⊢ x ≃ 0 ∧ step n' ≄ 0
Tactic:
have : step n' ≄ 0 := step_neqv_zero
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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n n' : ℕ
ih : x ^ n' ≃ 0 → x ≃ 0 ∧ n' ≄ 0
x✝ : x ^ step n' ≃ 0
this✝² : x ^ n' * x ≃ 0
this✝¹ : x ^ n' ≃ 0 ∨ x ≃ 0
this✝ : x ≃ 0
this : step n' ≄ 0
⊢ x ≃ 0 ∧ step n' ≄ 0
Theorem: Lean4Axiomatic.Natural.pow_inputs_for_output_zero
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✝² : OfNat α 0
inst✝¹ : AP (1 ≄ 0)
inst✝ : AA.ZeroProduct fun x x_1 => x * x_1
x : α
n n' : ℕ
ih : x ^ n' ≃ 0 → x ≃ 0 ∧ n' ≄ 0
x✝ : x ^ step n' ≃ 0
this✝² : x ^ n' * x ≃ 0
this✝¹ : x ^ n' ≃ 0 ∨ x ≃ 0
this✝ : x ≃ 0
this : step n' ≄ 0
⊢ x ≃ 0 ∧ step n' ≄ 0
Tactic:
exact And.intro ‹x ≃ 0› ‹step n' ≄ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_eqv_zero
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✝³ : OfNat α 0
inst✝² : AP (1 ≄ 0)
inst✝¹ : AA.ZeroProduct fun x x_1 => x * x_1
inst✝ : AA.Absorbing 0 fun x x_1 => x * x_1
x : α
n : ℕ
⊢ x ^ n ≃ 0 ↔ x ≃ 0 ∧ n ≄ 0
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : 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✝³ : OfNat α 0
inst✝² : AP (1 ≄ 0)
inst✝¹ : AA.ZeroProduct fun x x_1 => x * x_1
inst✝ : AA.Absorbing 0 fun x x_1 => x * x_1
x : α
n : ℕ
⊢ x ^ n ≃ 0 → x ≃ 0 ∧ n ≄ 0

case mpr
ℕ : 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✝³ : OfNat α 0
inst✝² : AP (1 ≄ 0)
inst✝¹ : AA.ZeroProduct fun x x_1 => x * x_1
inst✝ : AA.Absorbing 0 fun x x_1 => x * x_1
x : α
n : ℕ
⊢ x ≃ 0 ∧ n ≄ 0 → x ^ n ≃ 0
Theorem: Lean4Axiomatic.Natural.pow_eqv_zero
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✝³ : OfNat α 0
inst✝² : AP (1 ≄ 0)
inst✝¹ : AA.ZeroProduct fun x x_1 => x * x_1
inst✝ : AA.Absorbing 0 fun x x_1 => x * x_1
x : α
n : ℕ
⊢ x ^ n ≃ 0 → x ≃ 0 ∧ n ≄ 0
Tactic:
case mp =>
  show x^n ≃ 0 → x ≃ 0 ∧ n ≄ 0
  exact pow_inputs_for_output_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_eqv_zero
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✝³ : OfNat α 0
inst✝² : AP (1 ≄ 0)
inst✝¹ : AA.ZeroProduct fun x x_1 => x * x_1
inst✝ : AA.Absorbing 0 fun x x_1 => x * x_1
x : α
n : ℕ
⊢ x ≃ 0 ∧ n ≄ 0 → x ^ n ≃ 0
Tactic:
case mpr =>
  intro (And.intro (_ : x ≃ 0) (_ : n ≄ 0))
  show x^n ≃ 0
  have : Positive n := Signed.positive_defn.mpr ‹n ≄ 0›
  have (Exists.intro (n' : ℕ) (_ : step n' ≃ n)) := positive_step this
  calc
    _ ≃ x^n         := Rel.refl
    _ ≃ x^(step n') := pow_substR (Rel.symm ‹step n' ≃ n›)
    _ ≃ x^n' * x    := pow_step
    _ ≃ x^n' * 0    := AA.substR ‹x ≃ 0›
    _ ≃ 0           := AA.absorbR
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_eqv_zero
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✝³ : OfNat α 0
inst✝² : AP (1 ≄ 0)
inst✝¹ : AA.ZeroProduct fun x x_1 => x * x_1
inst✝ : AA.Absorbing 0 fun x x_1 => x * x_1
x : α
n : ℕ
⊢ x ^ n ≃ 0 → x ≃ 0 ∧ n ≄ 0
Tactic:
exact pow_inputs_for_output_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_eqv_zero
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✝³ : OfNat α 0
inst✝² : AP (1 ≄ 0)
inst✝¹ : AA.ZeroProduct fun x x_1 => x * x_1
inst✝ : AA.Absorbing 0 fun x x_1 => x * x_1
x : α
n : ℕ
⊢ x ≃ 0 ∧ n ≄ 0 → x ^ n ≃ 0
Tactic:
intro (And.intro (_ : x ≃ 0) (_ : 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
inst✝³ : OfNat α 0
inst✝² : AP (1 ≄ 0)
inst✝¹ : AA.ZeroProduct fun x x_1 => x * x_1
inst✝ : AA.Absorbing 0 fun x x_1 => x * x_1
x : α
n : ℕ
left✝ : x ≃ 0
right✝ : n ≄ 0
⊢ x ^ n ≃ 0