Theorem: Lean4Axiomatic.Natural.pow_preserves_nonzero_base (Lean4Axiomatic/Natural/Exponentiation.lean)

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 → x ^ n ≄ 0
Tactic:
intro (_ : x ≄ 0)
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
⊢ x ^ n ≄ 0

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
⊢ x ^ n ≄ 0
Tactic:
have : ¬(x ≃ 0 ∧ n ≄ 0) := by
  intro (And.intro (_ : x ≃ 0) (_ : n ≄ 0))
  show False
  exact absurd ‹x ≃ 0› ‹x ≄ 0›
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
this : ¬(x ≃ 0 ∧ n ≄ 0)
⊢ x ^ n ≄ 0

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
this : ¬(x ≃ 0 ∧ n ≄ 0)
⊢ x ^ n ≄ 0
Tactic:
have : x^n ≄ 0 := mt pow_inputs_for_output_zero this
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
this✝ : ¬(x ≃ 0 ∧ n ≄ 0)
this : x ^ n ≄ 0
⊢ x ^ n ≄ 0

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
this✝ : ¬(x ≃ 0 ∧ n ≄ 0)
this : x ^ n ≄ 0
⊢ x ^ n ≄ 0
Tactic:
exact this
State after:
no goals

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
⊢ ¬(x ≃ 0 ∧ n ≄ 0)
Tactic:
intro (And.intro (_ : x ≃ 0) (_ : n ≄ 0))
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
left✝ : x ≃ 0
right✝ : n ≄ 0
⊢ False

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
left✝ : x ≃ 0
right✝ : n ≄ 0
⊢ False
Tactic:
exact absurd ‹x ≃ 0› ‹x ≄ 0›
State after:
no goals