Theorem: Lean4Axiomatic.Rational.Impl.Fraction.nonzero_from_positive_numer (Lean4Axiomatic/Rational/Impl/Fraction/Reciprocation.lean)

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
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

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
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

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
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

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
State after:
no goals