internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.sub_substR
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a₁ a₂ b : ℤ
x✝ : a₁ ≃ a₂
⊢ b - a₁ ≃ b - a₂
Tactic:
calc
  b - a₁    ≃ _ := sub_defn
  b + (-a₁) ≃ _ := AA.substR (AA.subst₁ ‹a₁ ≃ a₂›)
  b + (-a₂) ≃ _ := Rel.symm sub_defn
  b - a₂    ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.zero_diff_iff_eqv
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
⊢ a - b ≃ 0 ↔ a ≃ b
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
⊢ a - b ≃ 0 → a ≃ b

case mpr
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
⊢ a ≃ b → a - b ≃ 0
Theorem: Lean4Axiomatic.Integer.zero_diff_iff_eqv
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
⊢ a - b ≃ 0 → a ≃ b
Tactic:
case mp =>
  intro (_ : a - b ≃ 0)
  show a ≃ b
  calc
    a            ≃ _ := Rel.symm AA.identR
    a + 0        ≃ _ := AA.substR (Rel.symm AA.inverseL)
    a + (-b + b) ≃ _ := Rel.symm AA.assoc
    (a + -b) + b ≃ _ := AA.substL (Rel.symm sub_defn)
    (a - b) + b  ≃ _ := AA.substL ‹a - b ≃ 0›
    0 + b        ≃ _ := AA.identL
    b            ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.zero_diff_iff_eqv
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
⊢ a ≃ b → a - b ≃ 0
Tactic:
case mpr =>
  intro (_ : a ≃ b)
  show a - b ≃ 0
  calc
    a - b  ≃ _ := AA.substL ‹a ≃ b›
    b - b  ≃ _ := sub_same
    0      ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.zero_diff_iff_eqv
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
⊢ a - b ≃ 0 → a ≃ b
Tactic:
intro (_ : a - b ≃ 0)
Proof state after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
x✝ : a - b ≃ 0
⊢ a ≃ b
Theorem: Lean4Axiomatic.Integer.zero_diff_iff_eqv
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
x✝ : a - b ≃ 0
⊢ a ≃ b
Tactic:
calc
  a            ≃ _ := Rel.symm AA.identR
  a + 0        ≃ _ := AA.substR (Rel.symm AA.inverseL)
  a + (-b + b) ≃ _ := Rel.symm AA.assoc
  (a + -b) + b ≃ _ := AA.substL (Rel.symm sub_defn)
  (a - b) + b  ≃ _ := AA.substL ‹a - b ≃ 0›
  0 + b        ≃ _ := AA.identL
  b            ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.zero_diff_iff_eqv
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
⊢ a ≃ b → a - b ≃ 0
Tactic:
intro (_ : a ≃ b)
Proof state after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
x✝ : a ≃ b
⊢ a - b ≃ 0
Theorem: Lean4Axiomatic.Integer.zero_diff_iff_eqv
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
x✝ : a ≃ b
⊢ a - b ≃ 0
Tactic:
calc
  a - b  ≃ _ := AA.substL ‹a ≃ b›
  b - b  ≃ _ := sub_same
  0      ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_cancelL
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
⊢ a ≄ 0 → a * b ≃ a * c → b ≃ c
Tactic:
intro (_ : a ≄ 0) (_ : a * b ≃ a * c)
Proof state after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
⊢ b ≃ c
Theorem: Lean4Axiomatic.Integer.mul_cancelL
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
⊢ b ≃ c
Tactic:
have : a * b - a * c ≃ 0 := zero_diff_iff_eqv.mpr ‹a * b ≃ a * c›
Proof state after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this : a * b - a * c ≃ 0
⊢ b ≃ c
Theorem: Lean4Axiomatic.Integer.mul_cancelL
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this : a * b - a * c ≃ 0
⊢ b ≃ c
Tactic:
have : a * (b - c) ≃ 0 := Rel.trans AA.distribL ‹a * b - a * c ≃ 0›
Proof state after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this✝ : a * b - a * c ≃ 0
this : a * (b - c) ≃ 0
⊢ b ≃ c
Theorem: Lean4Axiomatic.Integer.mul_cancelL
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this✝ : a * b - a * c ≃ 0
this : a * (b - c) ≃ 0
⊢ b ≃ c
Tactic:
have : a ≃ 0 ∨ b - c ≃ 0 := mul_split_zero.mp ‹a * (b - c) ≃ 0›
Proof state after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this✝¹ : a * b - a * c ≃ 0
this✝ : a * (b - c) ≃ 0
this : a ≃ 0 ∨ b - c ≃ 0
⊢ b ≃ c
Theorem: Lean4Axiomatic.Integer.mul_cancelL
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this✝¹ : a * b - a * c ≃ 0
this✝ : a * (b - c) ≃ 0
this : a ≃ 0 ∨ b - c ≃ 0
⊢ b ≃ c
Tactic:
match ‹a ≃ 0 ∨ b - c ≃ 0› with
| Or.inl (_ : a ≃ 0) =>
  show b ≃ c
  exact absurd ‹a ≃ 0› ‹a ≄ 0›
| Or.inr (_ : b - c ≃ 0) =>
  show b ≃ c
  exact zero_diff_iff_eqv.mp ‹b - c ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_cancelL
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this✝¹ : a * b - a * c ≃ 0
this✝ : a * (b - c) ≃ 0
this : a ≃ 0 ∨ b - c ≃ 0
h✝ : a ≃ 0
⊢ b ≃ c
Tactic:
exact absurd ‹a ≃ 0› ‹a ≄ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_cancelL
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this✝¹ : a * b - a * c ≃ 0
this✝ : a * (b - c) ≃ 0
this : a ≃ 0 ∨ b - c ≃ 0
h✝ : b - c ≃ 0
⊢ b ≃ c
Tactic:
exact zero_diff_iff_eqv.mp ‹b - c ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.neg_compat_from_integer
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a : ℤ
⊢ from_integer (-a) ≃ -from_integer a
Tactic:
show (-a)//1 ≃ -(a//1)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a : ℤ
⊢ (-a)//1 ≃ -a//1
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.neg_compat_from_integer
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a : ℤ
⊢ (-a)//1 ≃ -a//1
Tactic:
exact eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.neg_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁ p₂ : Fraction ℤ
⊢ p₁ ≃ p₂ → -p₁ ≃ -p₂
Tactic:
revert p₁
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ : Fraction ℤ
⊢ ∀ {p₁ : Fraction ℤ}, p₁ ≃ p₂ → -p₁ ≃ -p₂
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.neg_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ : Fraction ℤ
⊢ ∀ {p₁ : Fraction ℤ}, p₁ ≃ p₂ → -p₁ ≃ -p₂
Tactic:
intro (p₁n//p₁d)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₁d)
⊢ p₁n//p₁d ≃ p₂ → -p₁n//p₁d ≃ -p₂
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.neg_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₁d)
⊢ p₁n//p₁d ≃ p₂ → -p₁n//p₁d ≃ -p₂
Tactic:
revert p₂
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₁d)
⊢ ∀ {p₂ : Fraction ℤ}, p₁n//p₁d ≃ p₂ → -p₁n//p₁d ≃ -p₂
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.neg_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₁d)
⊢ ∀ {p₂ : Fraction ℤ}, p₁n//p₁d ≃ p₂ → -p₁n//p₁d ≃ -p₂
Tactic:
intro (p₂n//p₂d)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
⊢ p₁n//p₁d ≃ p₂n//p₂d → -p₁n//p₁d ≃ -p₂n//p₂d
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.neg_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
⊢ p₁n//p₁d ≃ p₂n//p₂d → -p₁n//p₁d ≃ -p₂n//p₂d
Tactic:
intro (_ : p₁n//p₁d ≃ p₂n//p₂d)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ -p₁n//p₁d ≃ -p₂n//p₂d
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.neg_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ -p₁n//p₁d ≃ -p₂n//p₂d
Tactic:
show -p₁n * p₂d ≃ -p₂n * p₁d
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ -p₁n * p₂d ≃ -p₂n * p₁d
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.neg_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ -p₁n * p₂d ≃ -p₂n * p₁d
Tactic:
have : p₁n * p₂d ≃ p₂n * p₁d := ‹p₁n//p₁d ≃ p₂n//p₂d›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
this : p₁n * p₂d ≃ p₂n * p₁d
⊢ -p₁n * p₂d ≃ -p₂n * p₁d
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.neg_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
this : p₁n * p₂d ≃ p₂n * p₁d
⊢ -p₁n * p₂d ≃ -p₂n * p₁d
Tactic:
calc
  (-p₁n) * p₂d   ≃ _ := Rel.symm AA.scompatL
  (-(p₁n * p₂d)) ≃ _ := AA.subst₁ ‹p₁n * p₂d ≃ p₂n * p₁d›
  (-(p₂n * p₁d)) ≃ _ := AA.scompatL
  (-p₂n) * p₁d   ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_inverseL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
⊢ -p + p ≃ 0
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, -p + p ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_inverseL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, -p + p ≃ 0
Tactic:
intro (pn//pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive pd)
⊢ -pn//pd + pn//pd ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_inverseL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive pd)
⊢ -pn//pd + pn//pd ≃ 0
Tactic:
calc
  -(pn//pd) + pn//pd ≃ _ := eqv_refl
  (-pn)//pd + pn//pd ≃ _ := add_eqv_denominators
  (-pn + pn)//pd     ≃ _ := substN AA.inverseL
  0//pd              ≃ _ := eqv_zero_iff_numerator_eqv_zero.mpr Rel.refl
  0                  ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
⊢ p ≃ 0 ↔ sgn p ≃ 0
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
⊢ p ≃ 0 → sgn p ≃ 0

case mpr
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
⊢ sgn p ≃ 0 → p ≃ 0
Theorem: Lean4Axiomatic.Rational.sgn_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
⊢ p ≃ 0 → sgn p ≃ 0
Tactic:
case mp =>
  intro (_ : p ≃ 0)
  show sgn p ≃ 0
  calc
    sgn p             ≃ _ := sgn_subst ‹p ≃ 0›
    sgn ((0 : ℤ) : ℚ) ≃ _ := sgn_from_integer
    sgn (0 : ℤ)       ≃ _ := Integer.sgn_zero.mp Rel.refl
    0                 ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
⊢ sgn p ≃ 0 → p ≃ 0
Tactic:
case mpr =>
  exact Sign.Props.sgn_zero_only_for_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
⊢ p ≃ 0 → sgn p ≃ 0
Tactic:
intro (_ : p ≃ 0)
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : p ≃ 0
⊢ sgn p ≃ 0
Theorem: Lean4Axiomatic.Rational.sgn_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : p ≃ 0
⊢ sgn p ≃ 0
Tactic:
calc
  sgn p             ≃ _ := sgn_subst ‹p ≃ 0›
  sgn ((0 : ℤ) : ℚ) ≃ _ := sgn_from_integer
  sgn (0 : ℤ)       ≃ _ := Integer.sgn_zero.mp Rel.refl
  0                 ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
⊢ sgn p ≃ 0 → p ≃ 0
Tactic:
exact Sign.Props.sgn_zero_only_for_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelL_mul_pos
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
⊢ sgn r ≃ 1 → sgn (r * p - r * q) ≃ sgn (p - q)
Tactic:
intro (_ : sgn r ≃ 1)
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
x✝ : sgn r ≃ 1
⊢ sgn (r * p - r * q) ≃ sgn (p - q)
Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelL_mul_pos
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
x✝ : sgn r ≃ 1
⊢ sgn (r * p - r * q) ≃ sgn (p - q)
Tactic:
calc
  _ ≃ sgn (r * p - r * q) := Rel.refl
  _ ≃ sgn (r * (p - q))   := sgn_subst (eqv_symm mul_distribL_sub)
  _ ≃ sgn r * sgn (p - q) := sgn_compat_mul
  _ ≃ 1 * sgn (p - q)     := AA.substL ‹sgn r ≃ 1›
  _ ≃ sgn (p - q)         := AA.identL
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelR_mul_pos
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
⊢ sgn r ≃ 1 → sgn (p * r - q * r) ≃ sgn (p - q)
Tactic:
intro (_ : sgn r ≃ 1)
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
x✝ : sgn r ≃ 1
⊢ sgn (p * r - q * r) ≃ sgn (p - q)
Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelR_mul_pos
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
x✝ : sgn r ≃ 1
⊢ sgn (p * r - q * r) ≃ sgn (p - q)
Tactic:
calc
  _ ≃ sgn (p * r - q * r) := Rel.refl
  _ ≃ sgn (r * p - q * r) := sgn_subst (sub_substL mul_comm)
  _ ≃ sgn (r * p - r * q) := sgn_subst (sub_substR mul_comm)
  _ ≃ sgn (p - q)         := sgn_sub_cancelL_mul_pos ‹sgn r ≃ 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelL_mul_neg
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
⊢ sgn r ≃ -1 → sgn (r * p - r * q) ≃ sgn (q - p)
Tactic:
intro (_ : sgn r ≃ -1)
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
x✝ : sgn r ≃ -1
⊢ sgn (r * p - r * q) ≃ sgn (q - p)
Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelL_mul_neg
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
x✝ : sgn r ≃ -1
⊢ sgn (r * p - r * q) ≃ sgn (q - p)
Tactic:
calc
  _ ≃ sgn (r * p - r * q) := Rel.refl
  _ ≃ sgn (r * (p - q))   := sgn_subst (eqv_symm mul_distribL_sub)
  _ ≃ sgn r * sgn (p - q) := sgn_compat_mul
  _ ≃ -1 * sgn (p - q)    := AA.substL ‹sgn r ≃ -1›
  _ ≃ -sgn (p - q)        := Integer.mul_neg_one
  _ ≃ sgn (-(p - q))      := Rel.symm sgn_compat_neg
  _ ≃ sgn (q - p)         := sgn_subst neg_sub
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelR_mul_neg
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
⊢ sgn r ≃ -1 → sgn (p * r - q * r) ≃ sgn (q - p)
Tactic:
intro (_ : sgn r ≃ -1)
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
x✝ : sgn r ≃ -1
⊢ sgn (p * r - q * r) ≃ sgn (q - p)
Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelR_mul_neg
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
x✝ : sgn r ≃ -1
⊢ sgn (p * r - q * r) ≃ sgn (q - p)
Tactic:
calc
  _ ≃ sgn (p * r - q * r) := Rel.refl
  _ ≃ sgn (r * p - q * r) := sgn_subst (sub_substL mul_comm)
  _ ≃ sgn (r * p - r * q) := sgn_subst (sub_substR mul_comm)
  _ ≃ sgn (q - p)         := sgn_sub_cancelL_mul_neg ‹sgn r ≃ -1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sqrt1_sgn_nonzero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
⊢ Integer.Sqrt1 (sgn p)
Tactic:
have : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1) := sgn_trichotomy p
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
this : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
⊢ Integer.Sqrt1 (sgn p)