Theorem: Lean4Axiomatic.Integer.same_sign_positive (Lean4Axiomatic/Integer/Sign.lean)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ SameSign a b → Positive a → Positive b
Tactic:
intro (SameSign.intro (s : ℤ) (_ : Sqrt1 s) nwsa nwsb)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
⊢ Positive a → Positive b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
⊢ Positive a → Positive b
Tactic:
have : NonzeroWithSign a s := nwsa
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this : NonzeroWithSign a s
⊢ Positive a → Positive b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this : NonzeroWithSign a s
⊢ Positive a → Positive b
Tactic:
have : NonzeroWithSign b s := nwsb
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝ : NonzeroWithSign a s
this : NonzeroWithSign b s
⊢ Positive a → Positive b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝ : NonzeroWithSign a s
this : NonzeroWithSign b s
⊢ Positive a → Positive b
Tactic:
intro (_ : Positive a)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝ : NonzeroWithSign a s
this : NonzeroWithSign b s
x✝ : Positive a
⊢ Positive b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝ : NonzeroWithSign a s
this : NonzeroWithSign b s
x✝ : Positive a
⊢ Positive b
Tactic:
have : NonzeroWithSign a 1 := positive_iff_sign_pos1.mp ‹Positive a›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝¹ : NonzeroWithSign a s
this✝ : NonzeroWithSign b s
x✝ : Positive a
this : NonzeroWithSign a 1
⊢ Positive b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝¹ : NonzeroWithSign a s
this✝ : NonzeroWithSign b s
x✝ : Positive a
this : NonzeroWithSign a 1
⊢ Positive b
Tactic:
have : s ≃ 1 :=
  nonzeroWithSign_sign_inject ‹NonzeroWithSign a s› ‹NonzeroWithSign a 1›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝² : NonzeroWithSign a s
this✝¹ : NonzeroWithSign b s
x✝ : Positive a
this✝ : NonzeroWithSign a 1
this : s ≃ 1
⊢ Positive b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝² : NonzeroWithSign a s
this✝¹ : NonzeroWithSign b s
x✝ : Positive a
this✝ : NonzeroWithSign a 1
this : s ≃ 1
⊢ Positive b
Tactic:
have : NonzeroWithSign b 1 :=
  NonzeroWithSign.subst_sign ‹s ≃ 1› ‹NonzeroWithSign b s›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝³ : NonzeroWithSign a s
this✝² : NonzeroWithSign b s
x✝ : Positive a
this✝¹ : NonzeroWithSign a 1
this✝ : s ≃ 1
this : NonzeroWithSign b 1
⊢ Positive b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝³ : NonzeroWithSign a s
this✝² : NonzeroWithSign b s
x✝ : Positive a
this✝¹ : NonzeroWithSign a 1
this✝ : s ≃ 1
this : NonzeroWithSign b 1
⊢ Positive b
Tactic:
have : Positive b := positive_iff_sign_pos1.mpr ‹NonzeroWithSign b 1›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝⁴ : NonzeroWithSign a s
this✝³ : NonzeroWithSign b s
x✝ : Positive a
this✝² : NonzeroWithSign a 1
this✝¹ : s ≃ 1
this✝ : NonzeroWithSign b 1
this : Positive b
⊢ Positive b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝⁴ : NonzeroWithSign a s
this✝³ : NonzeroWithSign b s
x✝ : Positive a
this✝² : NonzeroWithSign a 1
this✝¹ : s ≃ 1
this✝ : NonzeroWithSign b 1
this : Positive b
⊢ Positive b
Tactic:
exact this
State after:
no goals