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

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
⊢ p ≃ 0 ↔ p.numerator ≃ 0
Tactic:
revert p
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ 0 ↔ p.numerator ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ 0 ↔ p.numerator ≃ 0
Tactic:
intro (pn//pd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 0 ↔ (pn//pd).numerator ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 0 ↔ (pn//pd).numerator ≃ 0
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 0 → (pn//pd).numerator ≃ 0

case mpr
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ (pn//pd).numerator ≃ 0 → pn//pd ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 0 → (pn//pd).numerator ≃ 0
Tactic:
case mp =>
  intro (_ : pn//pd ≃ 0)
  show pn ≃ 0
  have : pn//pd ≃ 0//1 := ‹pn//pd ≃ 0›
  have : pn * 1 ≃ 0 * pd := ‹pn//pd ≃ 0//1›
  calc
    pn     ≃ _ := Rel.symm AA.identR
    pn * 1 ≃ _ := ‹pn * 1 ≃ 0 * pd›
    0 * pd ≃ _ := AA.absorbL
    0      ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ (pn//pd).numerator ≃ 0 → pn//pd ≃ 0
Tactic:
case mpr =>
  intro (_ : pn ≃ 0)
  show pn//pd ≃ 0
  show pn//pd ≃ 0//1
  show pn * 1 ≃ 0 * pd
  calc
    pn * 1 ≃ _ := AA.identR
    pn     ≃ _ := ‹pn ≃ 0›
    0      ≃ _ := Rel.symm AA.absorbL
    0 * pd ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 0 → (pn//pd).numerator ≃ 0
Tactic:
intro (_ : pn//pd ≃ 0)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
⊢ (pn//pd).numerator ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
⊢ (pn//pd).numerator ≃ 0
Tactic:
show pn ≃ 0
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
⊢ pn ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
⊢ pn ≃ 0
Tactic:
have : pn//pd ≃ 0//1 := ‹pn//pd ≃ 0›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
this : pn//pd ≃ 0//1
⊢ pn ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
this : pn//pd ≃ 0//1
⊢ pn ≃ 0
Tactic:
have : pn * 1 ≃ 0 * pd := ‹pn//pd ≃ 0//1›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
this✝ : pn//pd ≃ 0//1
this : pn * 1 ≃ 0 * pd
⊢ pn ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
this✝ : pn//pd ≃ 0//1
this : pn * 1 ≃ 0 * pd
⊢ pn ≃ 0
Tactic:
calc
  pn     ≃ _ := Rel.symm AA.identR
  pn * 1 ≃ _ := ‹pn * 1 ≃ 0 * pd›
  0 * pd ≃ _ := AA.absorbL
  0      ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ (pn//pd).numerator ≃ 0 → pn//pd ≃ 0
Tactic:
intro (_ : pn ≃ 0)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ 0
⊢ pn//pd ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ 0
⊢ pn//pd ≃ 0
Tactic:
show pn//pd ≃ 0//1
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ 0
⊢ pn//pd ≃ 0//1

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ 0
⊢ pn//pd ≃ 0//1
Tactic:
show pn * 1 ≃ 0 * pd
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ 0
⊢ pn * 1 ≃ 0 * pd

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ 0
⊢ pn * 1 ≃ 0 * pd
Tactic:
calc
  pn * 1 ≃ _ := AA.identR
  pn     ≃ _ := ‹pn ≃ 0›
  0      ≃ _ := Rel.symm AA.absorbL
  0 * pd ≃ _ := Rel.refl
State after:
no goals