Theorem: Lean4Axiomatic.Rational.Impl.Fraction.nonzero_numerator (Lean4Axiomatic/Rational/Impl/Fraction/Core.lean)

State before:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
p : Fraction ℤ
inst✝ : AP (p ≄ 0)
⊢ Integer.Nonzero p.numerator
Tactic:
revert p
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ (p : Fraction ℤ) [inst : AP (p ≄ 0)], Integer.Nonzero p.numerator

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ (p : Fraction ℤ) [inst : AP (p ≄ 0)], Integer.Nonzero p.numerator
Tactic:
intro (a//b) (_ : AP (a//b ≄ 0))
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
⊢ Integer.Nonzero (a//b).numerator

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
⊢ Integer.Nonzero (a//b).numerator
Tactic:
have : a ≃ 0 → a//b ≃ 0 := (eqv_zero_iff_numerator_eqv_zero (p := a//b)).mpr
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
this : a ≃ 0 → a//b ≃ 0
⊢ Integer.Nonzero (a//b).numerator

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
this : a ≃ 0 → a//b ≃ 0
⊢ Integer.Nonzero (a//b).numerator
Tactic:
have : a ≄ 0 := mt this ‹AP (a//b ≄ 0)›.ev
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
this✝ : a ≃ 0 → a//b ≃ 0
this : a ≄ 0
⊢ Integer.Nonzero (a//b).numerator

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
this✝ : a ≃ 0 → a//b ≃ 0
this : a ≄ 0
⊢ Integer.Nonzero (a//b).numerator
Tactic:
have : Integer.Nonzero a := Integer.nonzero_iff_neqv_zero.mpr this
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
this✝¹ : a ≃ 0 → a//b ≃ 0
this✝ : a ≄ 0
this : Integer.Nonzero a
⊢ Integer.Nonzero (a//b).numerator

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
this✝¹ : a ≃ 0 → a//b ≃ 0
this✝ : a ≄ 0
this : Integer.Nonzero a
⊢ Integer.Nonzero (a//b).numerator
Tactic:
exact this
State after:
no goals