internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.mul_preserves_nonzeroWithSign
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝¹ : Positive am
eqv✝¹ : a ≃ as * coe am
bm : ℕ
pos✝ : Positive bm
eqv✝ : b ≃ bs * coe bm
this : Positive (am * bm)
⊢ NonzeroWithSign (a * b) (as * bs)
Tactic:
have : a * b ≃ (as * bs) * coe (am * bm) := calc
  a * b                         ≃ _ := AA.substL ‹a ≃ as * coe am›
  (as * coe am) * b             ≃ _ := AA.substR ‹b ≃ bs * coe bm›
  (as * coe am) * (bs * coe bm) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (as * bs) * (coe am * coe bm) ≃ _ := AA.substR (Rel.symm AA.compat₂)
  (as * bs) * coe (am * bm)     ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝¹ : Positive am
eqv✝¹ : a ≃ as * coe am
bm : ℕ
pos✝ : Positive bm
eqv✝ : b ≃ bs * coe bm
this✝ : Positive (am * bm)
this : a * b ≃ as * bs * coe (am * bm)
⊢ NonzeroWithSign (a * b) (as * bs)
Theorem: Lean4Axiomatic.Integer.mul_preserves_nonzeroWithSign
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝¹ : Positive am
eqv✝¹ : a ≃ as * coe am
bm : ℕ
pos✝ : Positive bm
eqv✝ : b ≃ bs * coe bm
this✝ : Positive (am * bm)
this : a * b ≃ as * bs * coe (am * bm)
⊢ NonzeroWithSign (a * b) (as * bs)
Tactic:
exact NonzeroWithSign.intro
  (am * bm) ‹Positive (am * bm)› ‹a * b ≃ (as * bs) * coe (am * bm)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_swap_neg
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign (-a) s ↔ NonzeroWithSign a (-s)
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign (-a) s → NonzeroWithSign a (-s)

case mpr
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign a (-s) → NonzeroWithSign (-a) s
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_swap_neg
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign (-a) s → NonzeroWithSign a (-s)
Tactic:
case mp =>
  intro (NonzeroWithSign.intro (n : ℕ) (_ : Positive n) (_ : -a ≃ s * coe n))
  show NonzeroWithSign a (-s)
  have : a ≃ -s * coe n := calc
    a              ≃ _ := Rel.symm neg_involutive
    (-(-a))        ≃ _ := AA.subst₁ ‹-a ≃ s * coe n›
    (-(s * coe n)) ≃ _ := AA.scompatL
    (-s) * coe n   ≃ _ := Rel.refl
  exact NonzeroWithSign.intro n ‹Positive n› ‹a ≃ -s * coe n›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_swap_neg
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign a (-s) → NonzeroWithSign (-a) s
Tactic:
case mpr =>
  intro (NonzeroWithSign.intro (n : ℕ) (_ : Positive n) (_ : a ≃ -s * coe n))
  show NonzeroWithSign (-a) s
  have : -a ≃ s * coe n := calc
    (-a)            ≃ _ := AA.subst₁ ‹a ≃ -s * coe n›
    (-(-s * coe n)) ≃ _ := AA.scompatL
    (-(-s)) * coe n ≃ _ := AA.substL neg_involutive
    s * coe n       ≃ _ := Rel.refl
  exact NonzeroWithSign.intro n ‹Positive n› ‹-a ≃ s * coe n›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_swap_neg
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign (-a) s → NonzeroWithSign a (-s)
Tactic:
intro (NonzeroWithSign.intro (n : ℕ) (_ : Positive n) (_ : -a ≃ s * coe n))
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : -a ≃ s * coe n
⊢ NonzeroWithSign a (-s)
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_swap_neg
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : -a ≃ s * coe n
⊢ NonzeroWithSign a (-s)
Tactic:
have : a ≃ -s * coe n := calc
  a              ≃ _ := Rel.symm neg_involutive
  (-(-a))        ≃ _ := AA.subst₁ ‹-a ≃ s * coe n›
  (-(s * coe n)) ≃ _ := AA.scompatL
  (-s) * coe n   ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : -a ≃ s * coe n
this : a ≃ -s * coe n
⊢ NonzeroWithSign a (-s)
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_swap_neg
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : -a ≃ s * coe n
this : a ≃ -s * coe n
⊢ NonzeroWithSign a (-s)
Tactic:
exact NonzeroWithSign.intro n ‹Positive n› ‹a ≃ -s * coe n›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_swap_neg
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign a (-s) → NonzeroWithSign (-a) s
Tactic:
intro (NonzeroWithSign.intro (n : ℕ) (_ : Positive n) (_ : a ≃ -s * coe n))
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ -s * coe n
⊢ NonzeroWithSign (-a) s
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_swap_neg
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ -s * coe n
⊢ NonzeroWithSign (-a) s
Tactic:
have : -a ≃ s * coe n := calc
  (-a)            ≃ _ := AA.subst₁ ‹a ≃ -s * coe n›
  (-(-s * coe n)) ≃ _ := AA.scompatL
  (-(-s)) * coe n ≃ _ := AA.substL neg_involutive
  s * coe n       ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ -s * coe n
this : -a ≃ s * coe n
⊢ NonzeroWithSign (-a) s
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_swap_neg
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ -s * coe n
this : -a ≃ s * coe n
⊢ NonzeroWithSign (-a) s
Tactic:
exact NonzeroWithSign.intro n ‹Positive n› ‹-a ≃ s * coe n›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_subst
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
⊢ a₁ ≃ a₂ → Nonzero a₁ → Nonzero a₂
Tactic:
intro (_ : a₁ ≃ a₂) (Nonzero.intro (s : ℤ) (_ : Sqrt1 s) nws)
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
s : ℤ
sqrt1✝ : Sqrt1 s
nws : NonzeroWithSign a₁ s
⊢ Nonzero a₂
Theorem: Lean4Axiomatic.Integer.nonzero_subst
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
s : ℤ
sqrt1✝ : Sqrt1 s
nws : NonzeroWithSign a₁ s
⊢ Nonzero a₂
Tactic:
have : NonzeroWithSign a₁ s := nws
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
s : ℤ
sqrt1✝ : Sqrt1 s
nws this : NonzeroWithSign a₁ s
⊢ Nonzero a₂
Theorem: Lean4Axiomatic.Integer.nonzero_subst
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
s : ℤ
sqrt1✝ : Sqrt1 s
nws this : NonzeroWithSign a₁ s
⊢ Nonzero a₂
Tactic:
have : NonzeroWithSign a₂ s :=
  NonzeroWithSign.subst_nonzero ‹a₁ ≃ a₂› ‹NonzeroWithSign a₁ s›
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
s : ℤ
sqrt1✝ : Sqrt1 s
nws this✝ : NonzeroWithSign a₁ s
this : NonzeroWithSign a₂ s
⊢ Nonzero a₂
Theorem: Lean4Axiomatic.Integer.nonzero_subst
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
s : ℤ
sqrt1✝ : Sqrt1 s
nws this✝ : NonzeroWithSign a₁ s
this : NonzeroWithSign a₂ s
⊢ Nonzero a₂
Tactic:
exact Nonzero.mk ‹NonzeroWithSign a₂ s›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b : ℤ
⊢ Nonzero a → Nonzero b → Nonzero (a * b)
Tactic:
intro (Nonzero.intro as (_ : Sqrt1 as) nwsa)
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝ : Sqrt1 as
nwsa : NonzeroWithSign a as
⊢ Nonzero b → Nonzero (a * b)
Theorem: Lean4Axiomatic.Integer.mul_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝ : Sqrt1 as
nwsa : NonzeroWithSign a as
⊢ Nonzero b → Nonzero (a * b)
Tactic:
intro (Nonzero.intro bs (_ : Sqrt1 bs) nwsb)
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
⊢ Nonzero (a * b)
Theorem: Lean4Axiomatic.Integer.mul_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
⊢ Nonzero (a * b)
Tactic:
have : NonzeroWithSign a as := nwsa
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
this : NonzeroWithSign a as
⊢ Nonzero (a * b)
Theorem: Lean4Axiomatic.Integer.mul_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
this : NonzeroWithSign a as
⊢ Nonzero (a * b)
Tactic:
have : NonzeroWithSign b bs := nwsb
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
this✝ : NonzeroWithSign a as
this : NonzeroWithSign b bs
⊢ Nonzero (a * b)
Theorem: Lean4Axiomatic.Integer.mul_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
this✝ : NonzeroWithSign a as
this : NonzeroWithSign b bs
⊢ Nonzero (a * b)
Tactic:
have : NonzeroWithSign (a * b) (as * bs) :=
  mul_preserves_nonzeroWithSign ‹NonzeroWithSign a as› ‹NonzeroWithSign b bs›
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
this✝¹ : NonzeroWithSign a as
this✝ : NonzeroWithSign b bs
this : NonzeroWithSign (a * b) (as * bs)
⊢ Nonzero (a * b)
Theorem: Lean4Axiomatic.Integer.mul_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
this✝¹ : NonzeroWithSign a as
this✝ : NonzeroWithSign b bs
this : NonzeroWithSign (a * b) (as * bs)
⊢ Nonzero (a * b)
Tactic:
exact Nonzero.mk ‹NonzeroWithSign (a * b) (as * bs)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.neg_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
⊢ Nonzero a → Nonzero (-a)
Tactic:
intro (_ : Nonzero a)
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
x✝ : Nonzero a
⊢ Nonzero (-a)
Theorem: Lean4Axiomatic.Integer.neg_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
x✝ : Nonzero a
⊢ Nonzero (-a)
Tactic:
have : Nonzero (-1 : ℤ) := nonzero_sqrt1
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
x✝ : Nonzero a
this : Nonzero (-1)
⊢ Nonzero (-a)
Theorem: Lean4Axiomatic.Integer.neg_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
x✝ : Nonzero a
this : Nonzero (-1)
⊢ Nonzero (-a)
Tactic:
have : Nonzero (-1 * a) := mul_preserves_nonzero ‹Nonzero (-1 : ℤ)› ‹Nonzero a›
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
x✝ : Nonzero a
this✝ : Nonzero (-1)
this : Nonzero (-1 * a)
⊢ Nonzero (-a)
Theorem: Lean4Axiomatic.Integer.neg_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
x✝ : Nonzero a
this✝ : Nonzero (-1)
this : Nonzero (-1 * a)
⊢ Nonzero (-a)
Tactic:
have : Nonzero (-a) := nonzero_subst mul_neg_one ‹Nonzero (-1 * a)›
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
x✝ : Nonzero a
this✝¹ : Nonzero (-1)
this✝ : Nonzero (-1 * a)
this : Nonzero (-a)
⊢ Nonzero (-a)
Theorem: Lean4Axiomatic.Integer.neg_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
x✝ : Nonzero a
this✝¹ : Nonzero (-1)
this✝ : Nonzero (-1 * a)
this : Nonzero (-a)
⊢ Nonzero (-a)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.ord_sgn_subst
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
o₁ o₂ : Ordering
⊢ o₁ = o₂ → ord_sgn o₁ ≃ ord_sgn o₂
Tactic:
intro (_ : o₁ = o₂)
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
o₁ o₂ : Ordering
x✝ : o₁ = o₂
⊢ ord_sgn o₁ ≃ ord_sgn o₂
Theorem: Lean4Axiomatic.Integer.ord_sgn_subst
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
o₁ o₂ : Ordering
x✝ : o₁ = o₂
⊢ ord_sgn o₁ ≃ ord_sgn o₂
Tactic:
rw [‹o₁ = o₂›]
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
o₁ o₂ : Ordering
x✝ : o₁ = o₂
⊢ ord_sgn o₂ ≃ ord_sgn o₂
Theorem: Lean4Axiomatic.Integer.ord_sgn_subst
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
o₁ o₂ : Ordering
x✝ : o₁ = o₂
⊢ ord_sgn o₂ ≃ ord_sgn o₂
Tactic:
exact Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.ord_sgn_inject
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 0
⊢ -1 ≃ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.ord_sgn_inject
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
⊢ -1 ≃ 1
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.ord_sgn_inject
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : 0 ≃ -1
⊢ 0 ≃ -1
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.ord_sgn_inject
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : 0 ≃ 1
⊢ 0 ≃ 1
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.ord_sgn_inject
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : 1 ≃ -1
⊢ 1 ≃ -1
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.ord_sgn_inject
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : 1 ≃ 0
⊢ 1 ≃ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.positive_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
⊢ a₁ ≃ a₂ → Positive a₁ → Positive a₂
Tactic:
intro (_ : a₁ ≃ a₂) (_ : Positive a₁)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Positive a₁
⊢ Positive a₂
Theorem: Lean4Axiomatic.Integer.positive_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Positive a₁
⊢ Positive a₂
Tactic:
have (NonzeroWithSign.intro (m : ℕ) (_ : Positive m) (_ : a₁ ≃ 1 * ↑m)) :=
  positive_iff_sign_pos1.mp ‹Positive a₁›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Positive a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ 1 * coe m
⊢ Positive a₂
Theorem: Lean4Axiomatic.Integer.positive_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Positive a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ 1 * coe m
⊢ Positive a₂
Tactic:
have : a₂ ≃ 1 * ↑m := Rel.trans (Rel.symm ‹a₁ ≃ a₂›) ‹a₁ ≃ 1 * ↑m›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Positive a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ 1 * coe m
this : a₂ ≃ 1 * coe m
⊢ Positive a₂
Theorem: Lean4Axiomatic.Integer.positive_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Positive a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ 1 * coe m
this : a₂ ≃ 1 * coe m
⊢ Positive a₂
Tactic:
have : NonzeroWithSign a₂ 1 :=
  NonzeroWithSign.intro m ‹Positive m› ‹a₂ ≃ 1 * ↑m›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Positive a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ 1 * coe m
this✝ : a₂ ≃ 1 * coe m
this : NonzeroWithSign a₂ 1
⊢ Positive a₂
Theorem: Lean4Axiomatic.Integer.positive_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Positive a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ 1 * coe m
this✝ : a₂ ≃ 1 * coe m
this : NonzeroWithSign a₂ 1
⊢ Positive a₂
Tactic:
have : Positive a₂ := positive_iff_sign_pos1.mpr ‹NonzeroWithSign a₂ 1›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Positive a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ 1 * coe m
this✝¹ : a₂ ≃ 1 * coe m
this✝ : NonzeroWithSign a₂ 1
this : Positive a₂
⊢ Positive a₂
Theorem: Lean4Axiomatic.Integer.positive_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Positive a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ 1 * coe m
this✝¹ : a₂ ≃ 1 * coe m
this✝ : NonzeroWithSign a₂ 1
this : Positive a₂
⊢ Positive a₂
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.negative_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
⊢ a₁ ≃ a₂ → Negative a₁ → Negative a₂
Tactic:
intro (_ : a₁ ≃ a₂) (_ : Negative a₁)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Negative a₁
⊢ Negative a₂
Theorem: Lean4Axiomatic.Integer.negative_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Negative a₁
⊢ Negative a₂
Tactic:
have (NonzeroWithSign.intro (m : ℕ) (_ : Positive m) (_ : a₁ ≃ -1 * ↑m)) :=
  negative_iff_sign_neg1.mp ‹Negative a₁›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Negative a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ -1 * coe m
⊢ Negative a₂
Theorem: Lean4Axiomatic.Integer.negative_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Negative a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ -1 * coe m
⊢ Negative a₂
Tactic:
have : a₂ ≃ -1 * ↑m := Rel.trans (Rel.symm ‹a₁ ≃ a₂›) ‹a₁ ≃ -1 * ↑m›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Negative a₁
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ -1 * coe m
this : a₂ ≃ -1 * coe m
⊢ Negative a₂