internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_subst
Proof state before:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
p₂ : Fraction ℤ
inst✝ : AP (p₂ ≄ 0)
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ [inst : AP (a//b ≄ 0)], a//b ≃ p₂ → (a//b)⁻¹ ≃ p₂⁻¹
Tactic:
revert p₂
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ {p₂ : Fraction ℤ} [inst : AP (p₂ ≄ 0)] [inst_1 : AP (a//b ≄ 0)], a//b ≃ p₂ → (a//b)⁻¹ ≃ p₂⁻¹
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ {p₂ : Fraction ℤ} [inst : AP (p₂ ≄ 0)] [inst_1 : AP (a//b ≄ 0)], a//b ≃ p₂ → (a//b)⁻¹ ≃ 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)
⊢ ∀ [inst : AP (c//d ≄ 0)] [inst_1 : AP (a//b ≄ 0)], a//b ≃ c//d → (a//b)⁻¹ ≃ (c//d)⁻¹
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
⊢ ∀ [inst : AP (c//d ≄ 0)] [inst_1 : AP (a//b ≄ 0)], a//b ≃ c//d → (a//b)⁻¹ ≃ (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)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
⊢ (a//b)⁻¹ ≃ (c//d)⁻¹
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_subst
Proof state before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
⊢ (a//b)⁻¹ ≃ (c//d)⁻¹
Tactic:
have : Integer.Nonzero a := nonzero_numerator (a//b)
Proof state after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this : Integer.Nonzero a
⊢ (a//b)⁻¹ ≃ (c//d)⁻¹
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_subst
Proof state before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this : Integer.Nonzero a
⊢ (a//b)⁻¹ ≃ (c//d)⁻¹
Tactic:
have : Integer.Nonzero c := nonzero_numerator (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)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝ : Integer.Nonzero a
this : Integer.Nonzero c
⊢ (a//b)⁻¹ ≃ (c//d)⁻¹
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_subst
Proof state before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝ : Integer.Nonzero a
this : Integer.Nonzero c
⊢ (a//b)⁻¹ ≃ (c//d)⁻¹
Tactic:
show (b * sgn a)//(a * sgn a) ≃ (d * sgn c)//(c * sgn c)
Proof state after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝ : Integer.Nonzero a
this : Integer.Nonzero c
⊢ (b * sgn a)//(a * sgn a) ≃ (d * sgn c)//(c * sgn c)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_subst
Proof state before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝ : Integer.Nonzero a
this : Integer.Nonzero c
⊢ (b * sgn a)//(a * sgn a) ≃ (d * sgn c)//(c * sgn c)
Tactic:
show (b * sgn a) * (c * sgn c) ≃ (d * sgn c) * (a * sgn a)
Proof state after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝ : Integer.Nonzero a
this : Integer.Nonzero c
⊢ b * sgn a * (c * sgn c) ≃ d * sgn c * (a * sgn a)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_subst
Proof state before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝ : Integer.Nonzero a
this : Integer.Nonzero c
⊢ b * sgn a * (c * sgn c) ≃ d * sgn c * (a * sgn a)
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)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝¹ : Integer.Nonzero a
this✝ : Integer.Nonzero c
this : a * d ≃ c * b
⊢ b * sgn a * (c * sgn c) ≃ d * sgn c * (a * sgn a)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_subst
Proof state before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝¹ : Integer.Nonzero a
this✝ : Integer.Nonzero c
this : a * d ≃ c * b
⊢ b * sgn a * (c * sgn c) ≃ d * sgn c * (a * sgn a)
Tactic:
calc
  (b * sgn a) * (c * sgn c) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (b * c) * (sgn a * sgn c) ≃ _ := AA.substL AA.comm
  (c * b) * (sgn a * sgn c) ≃ _ := AA.substL (Rel.symm ‹a * d ≃ c * b›)
  (a * d) * (sgn a * sgn c) ≃ _ := AA.substL AA.comm
  (d * a) * (sgn a * sgn c) ≃ _ := AA.substR AA.comm
  (d * a) * (sgn c * sgn a) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (d * sgn c) * (a * sgn a) ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_inverseL
Proof state before:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
p : Fraction ℤ
inst✝ : AP (p ≄ 0)
⊢ p⁻¹ * p ≃ 1
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ} [inst : AP (p ≄ 0)], p⁻¹ * p ≃ 1
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_inverseL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ} [inst : AP (p ≄ 0)], p⁻¹ * p ≃ 1
Tactic:
intro (pn//pd) (_ : AP (pn//pd ≄ 0))
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : AP (pn//pd ≄ 0)
⊢ (pn//pd)⁻¹ * pn//pd ≃ 1
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_inverseL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : AP (pn//pd ≄ 0)
⊢ (pn//pd)⁻¹ * pn//pd ≃ 1
Tactic:
have : Integer.Nonzero pn := nonzero_numerator (pn//pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : AP (pn//pd ≄ 0)
this : Integer.Nonzero pn
⊢ (pn//pd)⁻¹ * pn//pd ≃ 1
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_inverseL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : AP (pn//pd ≄ 0)
this : Integer.Nonzero pn
⊢ (pn//pd)⁻¹ * pn//pd ≃ 1
Tactic:
calc
  (pn//pd)⁻¹ * pn//pd
    ≃ _ := eqv_refl
  (pd * sgn pn)//(pn * sgn pn) * pn//pd
    ≃ _ := eqv_refl
  ((pd * sgn pn) * pn)//((pn * sgn pn) * pd)
    ≃ _ := substN AA.assoc
  (pd * (sgn pn * pn))//((pn * sgn pn) * pd)
    ≃ _ := substN (AA.substR AA.comm)
  (pd * (pn * sgn pn))//((pn * sgn pn) * pd)
    ≃ _ := substN AA.comm
  ((pn * sgn pn) * pd)//((pn * sgn pn) * pd)
    ≃ _ := eqv_one_iff_numer_eqv_denom.mpr Rel.refl
  1
    ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.nonzero_from_positive_numer
Proof state before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
⊢ a//b ≄ 0
Tactic:
have : Integer.Nonzero a := Integer.nonzero_from_positive_inst
Proof state after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this : Integer.Nonzero a
⊢ a//b ≄ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.nonzero_from_positive_numer
Proof state before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this : Integer.Nonzero a
⊢ a//b ≄ 0
Tactic:
have : a ≄ 0 := Integer.nonzero_iff_neqv_zero.mp this
Proof state after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this✝ : Integer.Nonzero a
this : a ≄ 0
⊢ a//b ≄ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.nonzero_from_positive_numer
Proof state before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this✝ : Integer.Nonzero a
this : a ≄ 0
⊢ a//b ≄ 0
Tactic:
have : a//b ≄ 0 := mt eqv_zero_iff_numerator_eqv_zero.mp this
Proof state after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this✝¹ : Integer.Nonzero a
this✝ : a ≄ 0
this : a//b ≄ 0
⊢ a//b ≄ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.nonzero_from_positive_numer
Proof state before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this✝¹ : Integer.Nonzero a
this✝ : a ≄ 0
this : a//b ≄ 0
⊢ a//b ≄ 0
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_positive
Proof state before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
⊢ (a//b)⁻¹ ≃ b//a
Tactic:
have : sgn a ≃ 1 := Integer.sgn_positive.mp ‹AP (Positive a)›.ev
Proof state after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this : sgn a ≃ 1
⊢ (a//b)⁻¹ ≃ b//a
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_positive
Proof state before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this : sgn a ≃ 1
⊢ (a//b)⁻¹ ≃ b//a
Tactic:
have x_sgn_a {x : ℤ} : x * sgn a ≃ x := calc
  x * sgn a ≃ _ := AA.substR ‹sgn a ≃ 1›
  x * 1     ≃ _ := AA.identR
  x         ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this : sgn a ≃ 1
x_sgn_a : ∀ {x : ℤ}, x * sgn a ≃ x
⊢ (a//b)⁻¹ ≃ b//a
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_positive
Proof state before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this : sgn a ≃ 1
x_sgn_a : ∀ {x : ℤ}, x * sgn a ≃ x
⊢ (a//b)⁻¹ ≃ b//a
Tactic:
calc
  (a//b)⁻¹                 ≃ _ := eqv_refl
  (b * sgn a)//(a * sgn a) ≃ _ := substN x_sgn_a
  b//(a * sgn a)           ≃ _ := substD x_sgn_a
  b//a                     ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ a > b ↔ Positive (a - b)
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ a > b → Positive (a - b)

case mpr
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ Positive (a - b) → a > b
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ a > b → Positive (a - b)
Tactic:
case mp =>
  intro (_ : b < a)
  show Positive (a - b)
  have (And.intro (_ : b ≤ a) (_ : b ≄ a)) := lt_iff_le_neqv.mp ‹b < a›
  have (Exists.intro (k : ℕ) (_ : a ≃ b + coe k)) :=
    le_iff_add_nat.mp ‹b ≤ a›
  have : a - b ≃ coe k := subR_moveR_addL.mpr ‹a ≃ b + coe k›
  have : a - b ≄ 0 := mt zero_diff_iff_eqv.mp (Rel.symm ‹b ≄ a›)
  have : (k:ℤ) ≄ 0 := AA.neqv_substL ‹a - b ≃ coe k› ‹a - b ≄ 0›
  have : k ≄ 0 := AA.inject ‹coe k ≄ coe (0 : ℕ)›
  have : Positive k := Signed.positive_defn.mpr ‹k ≄ 0›
  have : Positive (a - b) := positive_intro_nat ‹Positive k› ‹a - b ≃ coe k›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ Positive (a - b) → a > b
Tactic:
case mpr =>
  intro (_ : Positive (a - b))
  show b < a
  have
    (Exists.intro (k : ℕ) (And.intro (_ : Positive k) (_ : a - b ≃ coe k)))
      := positive_elim_nat ‹Positive (a - b)›
  apply lt_iff_le_neqv.mpr
  show b ≤ a ∧ b ≄ a
  have : a ≃ b + coe k := subR_moveR_addL.mp ‹a - b ≃ coe k›
  have : b ≤ a := le_iff_add_nat.mpr (Exists.intro k ‹a ≃ b + coe k›)
  have : k ≄ 0 := Signed.positive_defn.mp ‹Positive k›
  have : (k:ℤ) ≄ ((0:ℕ):ℤ) := AA.subst₁ ‹k ≄ 0›
  have : a - b ≄ 0 :=
    AA.neqv_substL (Rel.symm ‹a - b ≃ coe k›) ‹(coe k : ℤ) ≄ 0›
  have : b ≄ a := Rel.symm (mt zero_diff_iff_eqv.mpr ‹a - b ≄ 0›)
  exact And.intro ‹b ≤ a› ‹b ≄ a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ a > b → Positive (a - b)
Tactic:
intro (_ : b < a)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
⊢ Positive (a - b)
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
⊢ Positive (a - b)
Tactic:
have (And.intro (_ : b ≤ a) (_ : b ≄ a)) := lt_iff_le_neqv.mp ‹b < a›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
⊢ Positive (a - b)
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
⊢ Positive (a - b)
Tactic:
have (Exists.intro (k : ℕ) (_ : a ≃ b + coe k)) :=
  le_iff_add_nat.mp ‹b ≤ a›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
⊢ Positive (a - b)
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
⊢ Positive (a - b)
Tactic:
have : a - b ≃ coe k := subR_moveR_addL.mpr ‹a ≃ b + coe k›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this : a - b ≃ coe k
⊢ Positive (a - b)
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this : a - b ≃ coe k
⊢ Positive (a - b)
Tactic:
have : a - b ≄ 0 := mt zero_diff_iff_eqv.mp (Rel.symm ‹b ≄ a›)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝ : a - b ≃ coe k
this : a - b ≄ 0
⊢ Positive (a - b)
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝ : a - b ≃ coe k
this : a - b ≄ 0
⊢ Positive (a - b)
Tactic:
have : (k:ℤ) ≄ 0 := AA.neqv_substL ‹a - b ≃ coe k› ‹a - b ≄ 0›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝¹ : a - b ≃ coe k
this✝ : a - b ≄ 0
this : coe k ≄ 0
⊢ Positive (a - b)
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝¹ : a - b ≃ coe k
this✝ : a - b ≄ 0
this : coe k ≄ 0
⊢ Positive (a - b)
Tactic:
have : k ≄ 0 := AA.inject ‹coe k ≄ coe (0 : ℕ)›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝² : a - b ≃ coe k
this✝¹ : a - b ≄ 0
this✝ : coe k ≄ 0
this : k ≄ 0
⊢ Positive (a - b)
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝² : a - b ≃ coe k
this✝¹ : a - b ≄ 0
this✝ : coe k ≄ 0
this : k ≄ 0
⊢ Positive (a - b)
Tactic:
have : Positive k := Signed.positive_defn.mpr ‹k ≄ 0›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝³ : a - b ≃ coe k
this✝² : a - b ≄ 0
this✝¹ : coe k ≄ 0
this✝ : k ≄ 0
this : Positive k
⊢ Positive (a - b)
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝³ : a - b ≃ coe k
this✝² : a - b ≄ 0
this✝¹ : coe k ≄ 0
this✝ : k ≄ 0
this : Positive k
⊢ Positive (a - b)
Tactic:
have : Positive (a - b) := positive_intro_nat ‹Positive k› ‹a - b ≃ coe k›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝⁴ : a - b ≃ coe k
this✝³ : a - b ≄ 0
this✝² : coe k ≄ 0
this✝¹ : k ≄ 0
this✝ : Positive k
this : Positive (a - b)
⊢ Positive (a - b)
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝⁴ : a - b ≃ coe k
this✝³ : a - b ≄ 0
this✝² : coe k ≄ 0
this✝¹ : k ≄ 0
this✝ : Positive k
this : Positive (a - b)
⊢ Positive (a - b)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ Positive (a - b) → a > b
Tactic:
intro (_ : Positive (a - b))
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
⊢ a > b
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
⊢ a > b
Tactic:
show b < a
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
⊢ b < a
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
⊢ b < a
Tactic:
have
  (Exists.intro (k : ℕ) (And.intro (_ : Positive k) (_ : a - b ≃ coe k)))
    := positive_elim_nat ‹Positive (a - b)›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
⊢ b < a
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
⊢ b < a
Tactic:
apply lt_iff_le_neqv.mpr
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
⊢ b ≤ a ∧ b ≄ a