internlm/Lean-Github huggingface dataset:
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 : ℕ
left✝ : x ≃ 0
right✝ : n ≄ 0
⊢ x ^ n ≃ 0
Tactic:
have : Positive n := Signed.positive_defn.mpr ‹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
this : Positive n
⊢ 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 : ℕ
left✝ : x ≃ 0
right✝ : n ≄ 0
this : Positive n
⊢ x ^ n ≃ 0
Tactic:
have (Exists.intro (n' : ℕ) (_ : step n' ≃ n)) := positive_step 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
inst✝ : AA.Absorbing 0 fun x x_1 => x * x_1
x : α
n : ℕ
left✝ : x ≃ 0
right✝ : n ≄ 0
this : Positive n
n' : ℕ
h✝ : step n' ≃ n
⊢ 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 : ℕ
left✝ : x ≃ 0
right✝ : n ≄ 0
this : Positive n
n' : ℕ
h✝ : step n' ≃ n
⊢ x ^ n ≃ 0
Tactic:
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_preserves_nonzero_base
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 → x ^ n ≄ 0
Tactic:
intro (_ : 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 : ℕ
x✝ : x ≄ 0
⊢ x ^ n ≄ 0
Theorem: Lean4Axiomatic.Natural.pow_preserves_nonzero_base
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
⊢ 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›
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
this : ¬(x ≃ 0 ∧ n ≄ 0)
⊢ x ^ n ≄ 0
Theorem: Lean4Axiomatic.Natural.pow_preserves_nonzero_base
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
this : ¬(x ≃ 0 ∧ n ≄ 0)
⊢ x ^ n ≄ 0
Tactic:
have : x^n ≄ 0 := mt pow_inputs_for_output_zero 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 : ℕ
x✝ : x ≄ 0
this✝ : ¬(x ≃ 0 ∧ n ≄ 0)
this : x ^ n ≄ 0
⊢ x ^ n ≄ 0
Theorem: Lean4Axiomatic.Natural.pow_preserves_nonzero_base
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
this✝ : ¬(x ≃ 0 ∧ n ≄ 0)
this : x ^ n ≄ 0
⊢ x ^ n ≄ 0
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_preserves_nonzero_base
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
⊢ ¬(x ≃ 0 ∧ 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
x : α
n : ℕ
x✝ : x ≄ 0
left✝ : x ≃ 0
right✝ : n ≄ 0
⊢ False
Theorem: Lean4Axiomatic.Natural.pow_preserves_nonzero_base
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
left✝ : x ≃ 0
right✝ : n ≄ 0
⊢ False
Tactic:
exact absurd ‹x ≃ 0› ‹x ≄ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_refl
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
⊢ p ≃ p
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ p
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_refl
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ p
Tactic:
intro (a//b)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a//b ≃ a//b
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_refl
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a//b ≃ a//b
Tactic:
show a * b ≃ a * b
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * b ≃ a * b
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_refl
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * b ≃ a * b
Tactic:
exact Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_symm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q : Fraction ℤ
⊢ p ≃ q → q ≃ p
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ q → q ≃ p
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_symm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ q → q ≃ p
Tactic:
intro (a//b)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
a b : ℤ
⊢ a//b ≃ q → q ≃ a//b
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_symm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
a b : ℤ
⊢ a//b ≃ q → q ≃ a//b
Tactic:
revert q
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ ∀ {q : Fraction ℤ}, a//b ≃ q → q ≃ a//b
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_symm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ ∀ {q : Fraction ℤ}, a//b ≃ q → q ≃ a//b
Tactic:
intro (c//d)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
⊢ a//b ≃ c//d → c//d ≃ a//b
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_symm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
⊢ a//b ≃ c//d → c//d ≃ a//b
Tactic:
intro (_ : a//b ≃ c//d)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
x✝ : a//b ≃ c//d
⊢ c//d ≃ a//b
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_symm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
x✝ : a//b ≃ c//d
⊢ c//d ≃ a//b
Tactic:
have : a * d ≃ c * b := ‹a//b ≃ c//d›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
x✝ : a//b ≃ c//d
this : a * d ≃ c * b
⊢ c//d ≃ a//b
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_symm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
x✝ : a//b ≃ c//d
this : a * d ≃ c * b
⊢ c//d ≃ a//b
Tactic:
show c * b ≃ a * d
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
x✝ : a//b ≃ c//d
this : a * d ≃ c * b
⊢ c * b ≃ a * d
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_symm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
x✝ : a//b ≃ c//d
this : a * d ≃ c * b
⊢ c * b ≃ a * d
Tactic:
exact Rel.symm ‹a * d ≃ c * b›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ¬∀ (p q r : Fraction ℤ), p ≃ q → q ≃ r → p ≃ r
Tactic:
intro (trans : {p q r : Naive.Fraction ℤ} → p ≃ q → q ≃ r → p ≃ r)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
⊢ False
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
⊢ False
Tactic:
let p : Naive.Fraction ℤ := 1//0
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
⊢ False
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
⊢ False
Tactic:
let q : Naive.Fraction ℤ := 0//0
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
⊢ False
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
⊢ False
Tactic:
let r : Naive.Fraction ℤ := 1//1
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
⊢ False
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
⊢ False
Tactic:
have : p ≃ q := by
  show 1//0 ≃ 0//0
  show 1 * 0 ≃ 0 * 0
  calc
    (1 : ℤ) * 0 ≃ _ := AA.absorbR
    0           ≃ _ := Rel.symm AA.absorbR
    0 * 0       ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this : p ≃ q
⊢ False
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this : p ≃ q
⊢ False
Tactic:
have : q ≃ r := by
  show 0//0 ≃ 1//1
  show 0 * 1 ≃ 1 * 0
  exact AA.comm
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝ : p ≃ q
this : q ≃ r
⊢ False
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝ : p ≃ q
this : q ≃ r
⊢ False
Tactic:
have : p ≄ r := by
  intro (_ : p ≃ r)
  show False
  have : (1 : ℤ)//0 ≃ 1//1 := ‹p ≃ r›
  have : (1 : ℤ) * 1 ≃ 1 * 0 := ‹(1 : ℤ)//0 ≃ 1//1›
  have : (1 : ℤ) ≃ 0 := calc
    (1 : ℤ) ≃ _ := Rel.symm AA.identR
    1 * 1   ≃ _ := ‹(1 : ℤ) * 1 ≃ 1 * 0›
    1 * 0   ≃ _ := AA.absorbR
    0       ≃ _ := Rel.refl
  have : (1 : ℤ) ≄ 0 := Integer.one_neqv_zero
  exact absurd ‹(1 : ℤ) ≃ 0› ‹(1 : ℤ) ≄ 0›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝¹ : p ≃ q
this✝ : q ≃ r
this : p ≄ r
⊢ False
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝¹ : p ≃ q
this✝ : q ≃ r
this : p ≄ r
⊢ False
Tactic:
have : p ≃ r := trans ‹p ≃ q› ‹q ≃ r›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝² : p ≃ q
this✝¹ : q ≃ r
this✝ : p ≄ r
this : p ≃ r
⊢ False
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝² : p ≃ q
this✝¹ : q ≃ r
this✝ : p ≄ r
this : p ≃ r
⊢ False
Tactic:
exact absurd ‹p ≃ r› ‹p ≄ r›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
⊢ p ≃ q
Tactic:
show 1//0 ≃ 0//0
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
⊢ 1//0 ≃ 0//0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
⊢ 1//0 ≃ 0//0
Tactic:
show 1 * 0 ≃ 0 * 0
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
⊢ 1 * 0 ≃ 0 * 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
⊢ 1 * 0 ≃ 0 * 0
Tactic:
calc
  (1 : ℤ) * 0 ≃ _ := AA.absorbR
  0           ≃ _ := Rel.symm AA.absorbR
  0 * 0       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this : p ≃ q
⊢ q ≃ r
Tactic:
show 0//0 ≃ 1//1
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this : p ≃ q
⊢ 0//0 ≃ 1//1
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this : p ≃ q
⊢ 0//0 ≃ 1//1
Tactic:
show 0 * 1 ≃ 1 * 0
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this : p ≃ q
⊢ 0 * 1 ≃ 1 * 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this : p ≃ q
⊢ 0 * 1 ≃ 1 * 0
Tactic:
exact AA.comm
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝ : p ≃ q
this : q ≃ r
⊢ p ≄ r
Tactic:
intro (_ : p ≃ r)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝ : p ≃ q
this : q ≃ r
x✝ : p ≃ r
⊢ False
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝ : p ≃ q
this : q ≃ r
x✝ : p ≃ r
⊢ False
Tactic:
have : (1 : ℤ)//0 ≃ 1//1 := ‹p ≃ r›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝¹ : p ≃ q
this✝ : q ≃ r
x✝ : p ≃ r
this : 1//0 ≃ 1//1
⊢ False
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝¹ : p ≃ q
this✝ : q ≃ r
x✝ : p ≃ r
this : 1//0 ≃ 1//1
⊢ False
Tactic:
have : (1 : ℤ) * 1 ≃ 1 * 0 := ‹(1 : ℤ)//0 ≃ 1//1›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝² : p ≃ q
this✝¹ : q ≃ r
x✝ : p ≃ r
this✝ : 1//0 ≃ 1//1
this : 1 * 1 ≃ 1 * 0
⊢ False
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝² : p ≃ q
this✝¹ : q ≃ r
x✝ : p ≃ r
this✝ : 1//0 ≃ 1//1
this : 1 * 1 ≃ 1 * 0
⊢ False
Tactic:
have : (1 : ℤ) ≃ 0 := calc
  (1 : ℤ) ≃ _ := Rel.symm AA.identR
  1 * 1   ≃ _ := ‹(1 : ℤ) * 1 ≃ 1 * 0›
  1 * 0   ≃ _ := AA.absorbR
  0       ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝³ : p ≃ q
this✝² : q ≃ r
x✝ : p ≃ r
this✝¹ : 1//0 ≃ 1//1
this✝ : 1 * 1 ≃ 1 * 0
this : 1 ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝³ : p ≃ q
this✝² : q ≃ r
x✝ : p ≃ r
this✝¹ : 1//0 ≃ 1//1
this✝ : 1 * 1 ≃ 1 * 0
this : 1 ≃ 0
⊢ False
Tactic:
have : (1 : ℤ) ≄ 0 := Integer.one_neqv_zero
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝⁴ : p ≃ q
this✝³ : q ≃ r
x✝ : p ≃ r
this✝² : 1//0 ≃ 1//1
this✝¹ : 1 * 1 ≃ 1 * 0
this✝ : 1 ≃ 0
this : 1 ≄ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝⁴ : p ≃ q
this✝³ : q ≃ r
x✝ : p ≃ r
this✝² : 1//0 ≃ 1//1
this✝¹ : 1 * 1 ≃ 1 * 0
this✝ : 1 ≃ 0
this : 1 ≄ 0
⊢ False
Tactic:
exact absurd ‹(1 : ℤ) ≃ 0› ‹(1 : ℤ) ≄ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_nonzero_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q r : Fraction ℤ
⊢ q.denominator ≄ 0 → p ≃ q → q ≃ r → p ≃ r
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, q.denominator ≄ 0 → p ≃ q → q ≃ r → p ≃ r