internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.recip_preserves_nonzero
Proof state before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
x✝ : p⁻¹ ≃ 0
⊢ False
Tactic:
have : p ≃ 0 := calc
  _ ≃ p             := eqv_refl
  _ ≃ p * 1         := eqv_symm mul_identR
  _ ≃ p * (p * p⁻¹) := mul_substR (eqv_symm mul_inverseR)
  _ ≃ p * (p * 0)   := mul_substR (mul_substR ‹p⁻¹ ≃ 0›)
  _ ≃ p * 0         := mul_substR mul_absorbR
  _ ≃ 0             := mul_absorbR
Proof state after:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
x✝ : p⁻¹ ≃ 0
this : p ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.recip_preserves_nonzero
Proof state before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
x✝ : p⁻¹ ≃ 0
this : p ≃ 0
⊢ False
Tactic:
exact absurd ‹p ≃ 0› ‹AP (p ≄ 0)›.ev
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Sqrt1.elim
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p : ℚ
⊢ Sqrt1 p → p * p ≃ 1
Tactic:
intro (_ : Sqrt1 p)
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p : ℚ
x✝ : Sqrt1 p
⊢ p * p ≃ 1
Theorem: Lean4Axiomatic.Rational.Sqrt1.elim
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p : ℚ
x✝ : Sqrt1 p
⊢ p * p ≃ 1
Tactic:
have (Sqrt1.from_integer_intro (a : ℤ) (_ : Integer.Sqrt1 a) eqv) :=
  ‹Sqrt1 p›
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p : ℚ
x✝ : Sqrt1 p
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv : p ≃ Rational.from_integer a
⊢ p * p ≃ 1
Theorem: Lean4Axiomatic.Rational.Sqrt1.elim
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p : ℚ
x✝ : Sqrt1 p
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv : p ≃ Rational.from_integer a
⊢ p * p ≃ 1
Tactic:
have : p ≃ (a : ℚ) := eqv
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p : ℚ
x✝ : Sqrt1 p
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this : p ≃ Rational.from_integer a
⊢ p * p ≃ 1
Theorem: Lean4Axiomatic.Rational.Sqrt1.elim
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p : ℚ
x✝ : Sqrt1 p
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this : p ≃ Rational.from_integer a
⊢ p * p ≃ 1
Tactic:
have : p * p ≃ 1 := calc
  p * p             ≃ _ := mul_substL ‹p ≃ (a : ℚ)›
  (a : ℚ) * p       ≃ _ := mul_substR ‹p ≃ (a : ℚ)›
  (a : ℚ) * (a : ℚ) ≃ _ := eqv_symm mul_compat_from_integer
  ((a * a : ℤ) : ℚ) ≃ _ := from_integer_subst ‹Integer.Sqrt1 a›.elim
  (1 : ℚ)           ≃ _ := eqv_refl
  1                 ≃ _ := eqv_refl
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p : ℚ
x✝ : Sqrt1 p
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this✝ : p ≃ Rational.from_integer a
this : p * p ≃ 1
⊢ p * p ≃ 1
Theorem: Lean4Axiomatic.Rational.Sqrt1.elim
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p : ℚ
x✝ : Sqrt1 p
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this✝ : p ≃ Rational.from_integer a
this : p * p ≃ 1
⊢ p * p ≃ 1
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sqrt1_subst
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p₁ p₂ : ℚ
⊢ p₁ ≃ p₂ → Sqrt1 p₁ → Sqrt1 p₂
Tactic:
intro (_ : p₁ ≃ p₂) (_ : Sqrt1 p₁)
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p₁ p₂ : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : Sqrt1 p₁
⊢ Sqrt1 p₂
Theorem: Lean4Axiomatic.Rational.sqrt1_subst
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p₁ p₂ : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : Sqrt1 p₁
⊢ Sqrt1 p₂
Tactic:
have (Sqrt1.from_integer_intro (a : ℤ) (_ : Integer.Sqrt1 a) eqv) :=
  ‹Sqrt1 p₁›
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p₁ p₂ : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : Sqrt1 p₁
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv : p₁ ≃ from_integer a
⊢ Sqrt1 p₂
Theorem: Lean4Axiomatic.Rational.sqrt1_subst
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p₁ p₂ : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : Sqrt1 p₁
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv : p₁ ≃ from_integer a
⊢ Sqrt1 p₂
Tactic:
have : p₁ ≃ (a : ℚ) := eqv
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p₁ p₂ : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : Sqrt1 p₁
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this : p₁ ≃ from_integer a
⊢ Sqrt1 p₂
Theorem: Lean4Axiomatic.Rational.sqrt1_subst
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p₁ p₂ : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : Sqrt1 p₁
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this : p₁ ≃ from_integer a
⊢ Sqrt1 p₂
Tactic:
have : p₂ ≃ (a : ℚ) := AA.substLFn ‹p₁ ≃ p₂› this
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p₁ p₂ : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : Sqrt1 p₁
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this✝ : p₁ ≃ from_integer a
this : p₂ ≃ from_integer a
⊢ Sqrt1 p₂
Theorem: Lean4Axiomatic.Rational.sqrt1_subst
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p₁ p₂ : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : Sqrt1 p₁
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this✝ : p₁ ≃ from_integer a
this : p₂ ≃ from_integer a
⊢ Sqrt1 p₂
Tactic:
have : Sqrt1 p₂ := Sqrt1.from_integer_intro a ‹Integer.Sqrt1 a› this
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p₁ p₂ : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : Sqrt1 p₁
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this✝¹ : p₁ ≃ from_integer a
this✝ : p₂ ≃ from_integer a
this : Sqrt1 p₂
⊢ Sqrt1 p₂
Theorem: Lean4Axiomatic.Rational.sqrt1_subst
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p₁ p₂ : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : Sqrt1 p₁
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this✝¹ : p₁ ≃ from_integer a
this✝ : p₂ ≃ from_integer a
this : Sqrt1 p₂
⊢ Sqrt1 p₂
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_sqrt1
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Sqrt1 (from_integer a) ↔ Integer.Sqrt1 a
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Sqrt1 (from_integer a) → Integer.Sqrt1 a

case mpr
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Integer.Sqrt1 a → Sqrt1 (from_integer a)
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_sqrt1
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Sqrt1 (from_integer a) → Integer.Sqrt1 a
Tactic:
case mp =>
  intro (_ : Sqrt1 (a : ℚ))
  show Integer.Sqrt1 a
  have (Sqrt1.from_integer_intro (b : ℤ) (_ : Integer.Sqrt1 b) eqv) :=
    ‹Sqrt1 (a : ℚ)›
  have : (b : ℚ) ≃ (a : ℚ) := eqv_symm eqv
  have : b ≃ a := from_integer_inject this
  have : Integer.Sqrt1 a := Integer.sqrt1_subst this ‹Integer.Sqrt1 b›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_sqrt1
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Integer.Sqrt1 a → Sqrt1 (from_integer a)
Tactic:
case mpr =>
  intro (_ : Integer.Sqrt1 a)
  show Sqrt1 (a : ℚ)
  exact Sqrt1.from_integer eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_sqrt1
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Sqrt1 (from_integer a) → Integer.Sqrt1 a
Tactic:
intro (_ : Sqrt1 (a : ℚ))
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
⊢ Integer.Sqrt1 a
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_sqrt1
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
⊢ Integer.Sqrt1 a
Tactic:
have (Sqrt1.from_integer_intro (b : ℤ) (_ : Integer.Sqrt1 b) eqv) :=
  ‹Sqrt1 (a : ℚ)›
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
⊢ Integer.Sqrt1 a
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_sqrt1
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
⊢ Integer.Sqrt1 a
Tactic:
have : (b : ℚ) ≃ (a : ℚ) := eqv_symm eqv
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
this : from_integer b ≃ from_integer a
⊢ Integer.Sqrt1 a
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_sqrt1
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
this : from_integer b ≃ from_integer a
⊢ Integer.Sqrt1 a
Tactic:
have : b ≃ a := from_integer_inject this
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
this✝ : from_integer b ≃ from_integer a
this : b ≃ a
⊢ Integer.Sqrt1 a
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_sqrt1
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
this✝ : from_integer b ≃ from_integer a
this : b ≃ a
⊢ Integer.Sqrt1 a
Tactic:
have : Integer.Sqrt1 a := Integer.sqrt1_subst this ‹Integer.Sqrt1 b›
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
this✝¹ : from_integer b ≃ from_integer a
this✝ : b ≃ a
this : Integer.Sqrt1 a
⊢ Integer.Sqrt1 a
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_sqrt1
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
this✝¹ : from_integer b ≃ from_integer a
this✝ : b ≃ a
this : Integer.Sqrt1 a
⊢ Integer.Sqrt1 a
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_sqrt1
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Integer.Sqrt1 a → Sqrt1 (from_integer a)
Tactic:
intro (_ : Integer.Sqrt1 a)
Proof state after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Integer.Sqrt1 a
⊢ Sqrt1 (from_integer a)
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_sqrt1
Proof state before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Integer.Sqrt1 a
⊢ Sqrt1 (from_integer a)
Tactic:
exact Sqrt1.from_integer eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_nonzero
Proof state before:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
⊢ Integer.Nonzero a → from_integer a ≄ 0
Tactic:
intro (_ : Integer.Nonzero a) (_ : (a : ℚ) ≃ 0)
Proof state after:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_nonzero
Proof state before:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
⊢ False
Tactic:
have : a ≄ 0 := Integer.nonzero_iff_neqv_zero.mp ‹Integer.Nonzero a›
Proof state after:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
this : a ≄ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_nonzero
Proof state before:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
this : a ≄ 0
⊢ False
Tactic:
have : (a : ℚ) ≃ (0 : ℚ) := ‹(a : ℚ) ≃ 0›
Proof state after:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
this✝ : a ≄ 0
this : from_integer a ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_nonzero
Proof state before:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
this✝ : a ≄ 0
this : from_integer a ≃ 0
⊢ False
Tactic:
have : a ≃ 0 := from_integer_inject this
Proof state after:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
this✝¹ : a ≄ 0
this✝ : from_integer a ≃ 0
this : a ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.from_integer_preserves_nonzero
Proof state before:
ℕ ℤ : Type
inst✝² : Natural ℕ
inst✝¹ : Integer ℤ
ℚ : Type
inst✝ : Core ℚ
a : ℤ
x✝¹ : Integer.Nonzero a
x✝ : from_integer a ≃ 0
this✝¹ : a ≄ 0
this✝ : from_integer a ≃ 0
this : a ≃ 0
⊢ False
Tactic:
exact absurd ‹a ≃ 0› ‹a ≄ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_comm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a b : Difference ℕ
⊢ a + b ≃ b + a
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a + b ≃ b + a
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_comm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a + b ≃ b + a
Tactic:
intro (a₁——a₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
a₁ a₂ : ℕ
⊢ a₁——a₂ + b ≃ b + a₁——a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_comm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
a₁ a₂ : ℕ
⊢ a₁——a₂ + b ≃ b + a₁——a₂
Tactic:
revert b
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ : ℕ
⊢ ∀ {b : Difference ℕ}, a₁——a₂ + b ≃ b + a₁——a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_comm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ : ℕ
⊢ ∀ {b : Difference ℕ}, a₁——a₂ + b ≃ b + a₁——a₂
Tactic:
intro (b₁——b₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ a₁——a₂ + b₁——b₂ ≃ b₁——b₂ + a₁——a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_comm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ a₁——a₂ + b₁——b₂ ≃ b₁——b₂ + a₁——a₂
Tactic:
show (a₁ + b₁)——(a₂ + b₂) ≃ (b₁ + a₁)——(b₂ + a₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ (a₁ + b₁)——(a₂ + b₂) ≃ (b₁ + a₁)——(b₂ + a₂)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_comm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ (a₁ + b₁)——(a₂ + b₂) ≃ (b₁ + a₁)——(b₂ + a₂)
Tactic:
show from_prod (a₁ + b₁, a₂ + b₂) ≃ from_prod (b₁ + a₁, b₂ + a₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ from_prod (a₁ + b₁, a₂ + b₂) ≃ from_prod (b₁ + a₁, b₂ + a₂)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_comm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ from_prod (a₁ + b₁, a₂ + b₂) ≃ from_prod (b₁ + a₁, b₂ + a₂)
Tactic:
apply AA.subst₁
Proof state after:
case a
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ (a₁ + b₁, a₂ + b₂) ≃ (b₁ + a₁, b₂ + a₂)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_comm
Proof state before:
case a
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ (a₁ + b₁, a₂ + b₂) ≃ (b₁ + a₁, b₂ + a₂)
Tactic:
calc
  (a₁ + b₁, a₂ + b₂) ≃ _ := AA.substL AA.comm
  (b₁ + a₁, a₂ + b₂) ≃ _ := AA.substR AA.comm
  (b₁ + a₁, b₂ + a₂) ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b : Difference ℕ
⊢ a₁ ≃ a₂ → a₁ + b ≃ a₂ + b
Tactic:
revert a₁
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₂ b : Difference ℕ
⊢ ∀ {a₁ : Difference ℕ}, a₁ ≃ a₂ → a₁ + b ≃ a₂ + b
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₂ b : Difference ℕ
⊢ ∀ {a₁ : Difference ℕ}, a₁ ≃ a₂ → a₁ + b ≃ a₂ + b
Tactic:
intro (n——m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₂ b : Difference ℕ
n m : ℕ
⊢ n——m ≃ a₂ → n——m + b ≃ a₂ + b
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₂ b : Difference ℕ
n m : ℕ
⊢ n——m ≃ a₂ → n——m + b ≃ a₂ + b
Tactic:
revert a₂
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m : ℕ
⊢ ∀ {a₂ : Difference ℕ}, n——m ≃ a₂ → n——m + b ≃ a₂ + b
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m : ℕ
⊢ ∀ {a₂ : Difference ℕ}, n——m ≃ a₂ → n——m + b ≃ a₂ + b
Tactic:
intro (k——j)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m k j : ℕ
⊢ n——m ≃ k——j → n——m + b ≃ k——j + b
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m k j : ℕ
⊢ n——m ≃ k——j → n——m + b ≃ k——j + b
Tactic:
revert b
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ ∀ {b : Difference ℕ}, n——m ≃ k——j → n——m + b ≃ k——j + b
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ ∀ {b : Difference ℕ}, n——m ≃ k——j → n——m + b ≃ k——j + b
Tactic:
intro (p——q)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
⊢ n——m ≃ k——j → n——m + p——q ≃ k——j + p——q
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
⊢ n——m ≃ k——j → n——m + p——q ≃ k——j + p——q
Tactic:
intro (_ : n——m ≃ k——j)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
⊢ n——m + p——q ≃ k——j + p——q
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
⊢ n——m + p——q ≃ k——j + p——q
Tactic:
have : n + j ≃ k + m := ‹n——m ≃ k——j›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ n——m + p——q ≃ k——j + p——q
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ n——m + p——q ≃ k——j + p——q
Tactic:
show (n + p)——(m + q) ≃ (k + p)——(j + q)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ (n + p)——(m + q) ≃ (k + p)——(j + q)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ (n + p)——(m + q) ≃ (k + p)——(j + q)
Tactic:
show (n + p) + (j + q) ≃ (k + p) + (m + q)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ n + p + (j + q) ≃ k + p + (m + q)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ n + p + (j + q) ≃ k + p + (m + q)
Tactic:
calc
  (n + p) + (j + q) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (n + j) + (p + q) ≃ _ := AA.substL ‹n + j ≃ k + m›
  (k + m) + (p + q) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (k + p) + (m + q) ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_identL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a : Difference ℕ
⊢ 0 + a ≃ a
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, 0 + a ≃ a
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_identL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, 0 + a ≃ a
Tactic:
intro (n——m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ 0 + n——m ≃ n——m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_identL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ 0 + n——m ≃ n——m
Tactic:
show 0——0 + n——m ≃ n——m
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ 0——0 + n——m ≃ n——m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_identL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ 0——0 + n——m ≃ n——m
Tactic:
show (0 + n)——(0 + m) ≃ n——m
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (0 + n)——(0 + m) ≃ n——m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_identL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (0 + n)——(0 + m) ≃ n——m
Tactic:
show from_prod (0 + n, 0 + m) ≃ from_prod (n, m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ from_prod (0 + n, 0 + m) ≃ from_prod (n, m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_identL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ from_prod (0 + n, 0 + m) ≃ from_prod (n, m)
Tactic:
apply AA.subst₁
Proof state after:
case a
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (0 + n, 0 + m) ≃ (n, m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_identL
Proof state before:
case a
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (0 + n, 0 + m) ≃ (n, m)
Tactic:
calc
  (0 + n, 0 + m) ≃ _ := AA.substL AA.identL
  (n, 0 + m)     ≃ _ := AA.substR AA.identL
  (n, m)         ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_compat_natural
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n + m)——0 ≃ n——0 + m——0
Tactic:
show (n + m)——0 ≃ (n + m)——(0 + 0)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n + m)——0 ≃ (n + m)——(0 + 0)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_compat_natural
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n + m)——0 ≃ (n + m)——(0 + 0)
Tactic:
show (n + m) + (0 + 0) ≃ (n + m) + 0
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n + m + (0 + 0) ≃ n + m + 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_compat_natural
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n + m + (0 + 0) ≃ n + m + 0
Tactic:
exact AA.substR AA.identR
Proof state after:
no goals