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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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