internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.sgn_compat_mul
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
this : a * b ≃ 0 ∨ Nonzero (a * b)
h✝ : Nonzero (a * b)
⊢ sgn (a * b) ≃ sgn a * sgn b
Tactic:
have (And.intro (_ : Sqrt1 (sgn a)) (_ : Sqrt1 (sgn b))) :=
  sqrt1_sgn_split_nonzero_mul ‹Nonzero (a * b)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
this : a * b ≃ 0 ∨ Nonzero (a * b)
h✝ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
⊢ sgn (a * b) ≃ sgn a * sgn b
Theorem: Lean4Axiomatic.Integer.sgn_compat_mul
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
this : a * b ≃ 0 ∨ Nonzero (a * b)
h✝ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
⊢ sgn (a * b) ≃ sgn a * sgn b
Tactic:
have : Positive (a * b) ∨ Negative (a * b) :=
  nonzero_iff_pos_or_neg.mp ‹Nonzero (a * b)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
this✝ : a * b ≃ 0 ∨ Nonzero (a * b)
h✝ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
this : Positive (a * b) ∨ Negative (a * b)
⊢ sgn (a * b) ≃ sgn a * sgn b
Theorem: Lean4Axiomatic.Integer.sgn_compat_mul
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
this✝ : a * b ≃ 0 ∨ Nonzero (a * b)
h✝ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
this : Positive (a * b) ∨ Negative (a * b)
⊢ sgn (a * b) ≃ sgn a * sgn b
Tactic:
match this with
| Or.inl (_ : Positive (a * b)) =>
  have : sgn a ≃ sgn b := positive_mul_iff_sgn_eqv.mp ‹Positive (a * b)›
  have : Sqrt1 (sgn b) ∧ sgn a ≃ sgn b := And.intro ‹Sqrt1 (sgn b)› this
  calc
    sgn (a * b)   ≃ _ := sgn_positive.mp ‹Positive (a * b)›
    1             ≃ _ := Rel.symm (mul_sqrt1_eqv.mpr this)
    sgn a * sgn b ≃ _ := Rel.refl
| Or.inr (_ : Negative (a * b)) =>
  have : sgn a ≄ sgn b := negative_mul_iff_sgn_neqv.mp ‹Negative (a * b)›
  calc
    sgn (a * b)   ≃ _ := sgn_negative.mp ‹Negative (a * b)›
    (-1)          ≃ _ := Rel.symm (mul_sqrt1_neqv.mpr ‹sgn a ≄ sgn b›)
    sgn a * sgn b ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_compat_mul
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
this✝ : a * b ≃ 0 ∨ Nonzero (a * b)
h✝¹ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
this : Positive (a * b) ∨ Negative (a * b)
h✝ : Positive (a * b)
⊢ sgn (a * b) ≃ sgn a * sgn b
Tactic:
have : sgn a ≃ sgn b := positive_mul_iff_sgn_eqv.mp ‹Positive (a * b)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
this✝¹ : a * b ≃ 0 ∨ Nonzero (a * b)
h✝¹ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
this✝ : Positive (a * b) ∨ Negative (a * b)
h✝ : Positive (a * b)
this : sgn a ≃ sgn b
⊢ sgn (a * b) ≃ sgn a * sgn b
Theorem: Lean4Axiomatic.Integer.sgn_compat_mul
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
this✝¹ : a * b ≃ 0 ∨ Nonzero (a * b)
h✝¹ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
this✝ : Positive (a * b) ∨ Negative (a * b)
h✝ : Positive (a * b)
this : sgn a ≃ sgn b
⊢ sgn (a * b) ≃ sgn a * sgn b
Tactic:
have : Sqrt1 (sgn b) ∧ sgn a ≃ sgn b := And.intro ‹Sqrt1 (sgn b)› this
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
this✝² : a * b ≃ 0 ∨ Nonzero (a * b)
h✝¹ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
this✝¹ : Positive (a * b) ∨ Negative (a * b)
h✝ : Positive (a * b)
this✝ : sgn a ≃ sgn b
this : Sqrt1 (sgn b) ∧ sgn a ≃ sgn b
⊢ sgn (a * b) ≃ sgn a * sgn b
Theorem: Lean4Axiomatic.Integer.sgn_compat_mul
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
this✝² : a * b ≃ 0 ∨ Nonzero (a * b)
h✝¹ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
this✝¹ : Positive (a * b) ∨ Negative (a * b)
h✝ : Positive (a * b)
this✝ : sgn a ≃ sgn b
this : Sqrt1 (sgn b) ∧ sgn a ≃ sgn b
⊢ sgn (a * b) ≃ sgn a * sgn b
Tactic:
calc
  sgn (a * b)   ≃ _ := sgn_positive.mp ‹Positive (a * b)›
  1             ≃ _ := Rel.symm (mul_sqrt1_eqv.mpr this)
  sgn a * sgn b ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_compat_mul
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
this✝ : a * b ≃ 0 ∨ Nonzero (a * b)
h✝¹ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
this : Positive (a * b) ∨ Negative (a * b)
h✝ : Negative (a * b)
⊢ sgn (a * b) ≃ sgn a * sgn b
Tactic:
have : sgn a ≄ sgn b := negative_mul_iff_sgn_neqv.mp ‹Negative (a * b)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
this✝¹ : a * b ≃ 0 ∨ Nonzero (a * b)
h✝¹ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
this✝ : Positive (a * b) ∨ Negative (a * b)
h✝ : Negative (a * b)
this : sgn a ≄ sgn b
⊢ sgn (a * b) ≃ sgn a * sgn b
Theorem: Lean4Axiomatic.Integer.sgn_compat_mul
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
this✝¹ : a * b ≃ 0 ∨ Nonzero (a * b)
h✝¹ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
this✝ : Positive (a * b) ∨ Negative (a * b)
h✝ : Negative (a * b)
this : sgn a ≄ sgn b
⊢ sgn (a * b) ≃ sgn a * sgn b
Tactic:
calc
  sgn (a * b)   ≃ _ := sgn_negative.mp ‹Negative (a * b)›
  (-1)          ≃ _ := Rel.symm (mul_sqrt1_neqv.mpr ‹sgn a ≄ sgn b›)
  sgn a * sgn b ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.positive_mul_sgn_self
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Nonzero a → Positive (a * sgn a)
Tactic:
intro (_ : Nonzero a)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
⊢ Positive (a * sgn a)
Theorem: Lean4Axiomatic.Integer.positive_mul_sgn_self
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
⊢ Positive (a * sgn a)
Tactic:
have : Sqrt1 (sgn a) := sgn_nonzero.mp ‹Nonzero a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this : Sqrt1 (sgn a)
⊢ Positive (a * sgn a)
Theorem: Lean4Axiomatic.Integer.positive_mul_sgn_self
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this : Sqrt1 (sgn a)
⊢ Positive (a * sgn a)
Tactic:
have : sgn a * sgn a ≃ 1 := this.elim
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝ : Sqrt1 (sgn a)
this : sgn a * sgn a ≃ 1
⊢ Positive (a * sgn a)
Theorem: Lean4Axiomatic.Integer.positive_mul_sgn_self
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝ : Sqrt1 (sgn a)
this : sgn a * sgn a ≃ 1
⊢ Positive (a * sgn a)
Tactic:
have : sgn (a * sgn a) ≃ 1 := calc
  sgn (a * sgn a)     ≃ _ := sgn_compat_mul
  sgn a * sgn (sgn a) ≃ _ := AA.substR sgn_idemp
  sgn a * sgn a       ≃ _ := ‹sgn a * sgn a ≃ 1›
  1                   ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝¹ : Sqrt1 (sgn a)
this✝ : sgn a * sgn a ≃ 1
this : sgn (a * sgn a) ≃ 1
⊢ Positive (a * sgn a)
Theorem: Lean4Axiomatic.Integer.positive_mul_sgn_self
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝¹ : Sqrt1 (sgn a)
this✝ : sgn a * sgn a ≃ 1
this : sgn (a * sgn a) ≃ 1
⊢ Positive (a * sgn a)
Tactic:
have : Positive (a * sgn a) := sgn_positive.mpr ‹sgn (a * sgn a) ≃ 1›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝² : Sqrt1 (sgn a)
this✝¹ : sgn a * sgn a ≃ 1
this✝ : sgn (a * sgn a) ≃ 1
this : Positive (a * sgn a)
⊢ Positive (a * sgn a)
Theorem: Lean4Axiomatic.Integer.positive_mul_sgn_self
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝² : Sqrt1 (sgn a)
this✝¹ : sgn a * sgn a ≃ 1
this✝ : sgn (a * sgn a) ≃ 1
this : Positive (a * sgn a)
⊢ Positive (a * sgn a)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_two_eqv_one
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
⊢ sgn 2 ≃ 1
Tactic:
have : sgn (1:ℤ) ≃ 1 := sgn_positive.mp one_positive
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
this : sgn 1 ≃ 1
⊢ sgn 2 ≃ 1
Theorem: Lean4Axiomatic.Integer.sgn_two_eqv_one
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
this : sgn 1 ≃ 1
⊢ sgn 2 ≃ 1
Tactic:
calc
  _ ≃ sgn (2:ℤ)       := Rel.refl
  _ ≃ sgn (1 + 1 : ℤ) := sgn_subst (Rel.symm add_one_one)
  _ ≃ 1               := add_preserves_sign ‹sgn (1:ℤ) ≃ 1› ‹sgn (1:ℤ) ≃ 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁ p₂ : Fraction ℤ
⊢ p₁ ≃ p₂ → sgn p₁ ≃ sgn p₂
Tactic:
revert p₁
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ : Fraction ℤ
⊢ ∀ {p₁ : Fraction ℤ}, p₁ ≃ p₂ → sgn p₁ ≃ sgn p₂
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ : Fraction ℤ
⊢ ∀ {p₁ : Fraction ℤ}, p₁ ≃ p₂ → sgn p₁ ≃ sgn p₂
Tactic:
intro (a//b)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ : Fraction ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ a//b ≃ p₂ → sgn (a//b) ≃ sgn p₂
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ : Fraction ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ a//b ≃ p₂ → sgn (a//b) ≃ sgn p₂
Tactic:
revert p₂
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ {p₂ : Fraction ℤ}, a//b ≃ p₂ → sgn (a//b) ≃ sgn p₂
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ {p₂ : Fraction ℤ}, a//b ≃ p₂ → sgn (a//b) ≃ sgn p₂
Tactic:
intro (c//d)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
⊢ a//b ≃ c//d → sgn (a//b) ≃ sgn (c//d)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
⊢ a//b ≃ c//d → sgn (a//b) ≃ sgn (c//d)
Tactic:
intro (_ : a//b ≃ c//d)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
⊢ sgn (a//b) ≃ sgn (c//d)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
⊢ sgn (a//b) ≃ sgn (c//d)
Tactic:
have : a * d ≃ c * b := ‹a//b ≃ c//d›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this : a * d ≃ c * b
⊢ sgn (a//b) ≃ sgn (c//d)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this : a * d ≃ c * b
⊢ sgn (a//b) ≃ sgn (c//d)
Tactic:
have : Positive b := ‹AP (Positive b)›.ev
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this✝ : a * d ≃ c * b
this : Positive b
⊢ sgn (a//b) ≃ sgn (c//d)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this✝ : a * d ≃ c * b
this : Positive b
⊢ sgn (a//b) ≃ sgn (c//d)
Tactic:
have : sgn b ≃ 1 := Integer.sgn_positive.mp this
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this✝¹ : a * d ≃ c * b
this✝ : Positive b
this : sgn b ≃ 1
⊢ sgn (a//b) ≃ sgn (c//d)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this✝¹ : a * d ≃ c * b
this✝ : Positive b
this : sgn b ≃ 1
⊢ sgn (a//b) ≃ sgn (c//d)
Tactic:
have : Positive d := ‹AP (Positive d)›.ev
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this✝² : a * d ≃ c * b
this✝¹ : Positive b
this✝ : sgn b ≃ 1
this : Positive d
⊢ sgn (a//b) ≃ sgn (c//d)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this✝² : a * d ≃ c * b
this✝¹ : Positive b
this✝ : sgn b ≃ 1
this : Positive d
⊢ sgn (a//b) ≃ sgn (c//d)
Tactic:
have : 1 ≃ sgn d := Rel.symm (Integer.sgn_positive.mp this)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this✝³ : a * d ≃ c * b
this✝² : Positive b
this✝¹ : sgn b ≃ 1
this✝ : Positive d
this : 1 ≃ sgn d
⊢ sgn (a//b) ≃ sgn (c//d)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this✝³ : a * d ≃ c * b
this✝² : Positive b
this✝¹ : sgn b ≃ 1
this✝ : Positive d
this : 1 ≃ sgn d
⊢ sgn (a//b) ≃ sgn (c//d)
Tactic:
calc
  sgn (a//b)    ≃ _ := Rel.refl
  sgn a         ≃ _ := Rel.symm AA.identR
  sgn a * 1     ≃ _ := AA.substR ‹1 ≃ sgn d›
  sgn a * sgn d ≃ _ := Rel.symm Integer.sgn_compat_mul
  sgn (a * d)   ≃ _ := Integer.sgn_subst ‹a * d ≃ c * b›
  sgn (c * b)   ≃ _ := Integer.sgn_compat_mul
  sgn c * sgn b ≃ _ := AA.substR ‹sgn b ≃ 1›
  sgn c * 1     ≃ _ := AA.identR
  sgn c         ≃ _ := Rel.refl
  sgn (c//d)    ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_zero_only_for_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
⊢ sgn p ≃ 0 → p ≃ 0
Tactic:
intro (_ : sgn p ≃ 0)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
⊢ p ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_zero_only_for_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
⊢ p ≃ 0
Tactic:
have : sgn p.numerator ≃ 0 := ‹sgn p ≃ 0›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this : sgn p.numerator ≃ 0
⊢ p ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_zero_only_for_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this : sgn p.numerator ≃ 0
⊢ p ≃ 0
Tactic:
have : p.numerator ≃ 0 := Integer.sgn_zero.mpr this
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this✝ : sgn p.numerator ≃ 0
this : p.numerator ≃ 0
⊢ p ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_zero_only_for_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this✝ : sgn p.numerator ≃ 0
this : p.numerator ≃ 0
⊢ p ≃ 0
Tactic:
have : p ≃ 0 := eqv_zero_iff_numerator_eqv_zero.mpr this
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this✝¹ : sgn p.numerator ≃ 0
this✝ : p.numerator ≃ 0
this : p ≃ 0
⊢ p ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_zero_only_for_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this✝¹ : sgn p.numerator ≃ 0
this✝ : p.numerator ≃ 0
this : p ≃ 0
⊢ p ≃ 0
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_compat_mul
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q : Fraction ℤ
⊢ sgn (p * q) ≃ sgn p * sgn q
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, sgn (p * q) ≃ sgn p * sgn q
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_compat_mul
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, sgn (p * q) ≃ sgn p * sgn q
Tactic:
intro (a//b)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ sgn (a//b * q) ≃ sgn (a//b) * sgn q
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_compat_mul
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ sgn (a//b * q) ≃ sgn (a//b) * sgn q
Tactic:
revert q
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ {q : Fraction ℤ}, sgn (a//b * q) ≃ sgn (a//b) * sgn q
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_compat_mul
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ {q : Fraction ℤ}, sgn (a//b * q) ≃ sgn (a//b) * sgn q
Tactic:
intro (c//d)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
⊢ sgn (a//b * c//d) ≃ sgn (a//b) * sgn (c//d)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_compat_mul
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
⊢ sgn (a//b * c//d) ≃ sgn (a//b) * sgn (c//d)
Tactic:
calc
  sgn (a//b * c//d)       ≃ _ := sgn_subst eqv_refl
  sgn ((a * c)//(b * d))  ≃ _ := Rel.refl
  sgn (a * c)             ≃ _ := Integer.sgn_compat_mul
  sgn a * sgn c           ≃ _ := Rel.refl
  sgn (a//b) * sgn (c//d) ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_trichotomy
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
have
  : AA.OneOfThree
    (p.numerator ≃ 0)
    (Positive p.numerator)
    (Negative p.numerator)
  := (Integer.sign_trichotomy p.numerator).atLeastOne
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_trichotomy
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
match this with
| AA.OneOfThree.first (_ : p.numerator ≃ 0) =>
  have : sgn p ≃ 0 := calc
    sgn p           ≃ _ := Rel.refl
    sgn p.numerator ≃ _ := Integer.sgn_zero.mp ‹p.numerator ≃ 0›
    0               ≃ _ := Rel.refl
  exact AA.OneOfThree.first this
| AA.OneOfThree.second (_ : Positive p.numerator) =>
  have : sgn p ≃ 1 := calc
    sgn p           ≃ _ := Rel.refl
    sgn p.numerator ≃ _ := Integer.sgn_positive.mp ‹Positive p.numerator›
    1               ≃ _ := Rel.refl
  exact AA.OneOfThree.second this
| AA.OneOfThree.third (_ : Negative p.numerator) =>
  have : sgn p ≃ -1 := calc
    sgn p           ≃ _ := Rel.refl
    sgn p.numerator ≃ _ := Integer.sgn_negative.mp ‹Negative p.numerator›
    (-1)            ≃ _ := Rel.refl
  exact AA.OneOfThree.third this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_trichotomy
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
a✝ : p.numerator ≃ 0
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
have : sgn p ≃ 0 := calc
  sgn p           ≃ _ := Rel.refl
  sgn p.numerator ≃ _ := Integer.sgn_zero.mp ‹p.numerator ≃ 0›
  0               ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this✝ : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
a✝ : p.numerator ≃ 0
this : sgn p ≃ 0
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_trichotomy
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this✝ : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
a✝ : p.numerator ≃ 0
this : sgn p ≃ 0
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
exact AA.OneOfThree.first this
Proof state after:
no goals