internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_nonzero_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, q.denominator ≄ 0 → p ≃ q → q ≃ r → p ≃ r
Tactic:
intro (pn//pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
⊢ q.denominator ≄ 0 → pn//pd ≃ q → q ≃ r → pn//pd ≃ r
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_nonzero_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
⊢ q.denominator ≄ 0 → pn//pd ≃ q → q ≃ r → pn//pd ≃ r
Tactic:
revert q
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
⊢ ∀ {q : Fraction ℤ}, q.denominator ≄ 0 → pn//pd ≃ q → q ≃ r → pn//pd ≃ r
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_nonzero_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
⊢ ∀ {q : Fraction ℤ}, q.denominator ≄ 0 → pn//pd ≃ q → q ≃ r → pn//pd ≃ r
Tactic:
intro (qn//qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd qn qd : ℤ
⊢ (qn//qd).denominator ≄ 0 → pn//pd ≃ qn//qd → qn//qd ≃ r → pn//pd ≃ r
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_nonzero_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd qn qd : ℤ
⊢ (qn//qd).denominator ≄ 0 → pn//pd ≃ qn//qd → qn//qd ≃ r → pn//pd ≃ r
Tactic:
revert r
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
⊢ ∀ {r : Fraction ℤ}, (qn//qd).denominator ≄ 0 → pn//pd ≃ qn//qd → qn//qd ≃ r → pn//pd ≃ r
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_nonzero_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
⊢ ∀ {r : Fraction ℤ}, (qn//qd).denominator ≄ 0 → pn//pd ≃ qn//qd → qn//qd ≃ r → pn//pd ≃ r
Tactic:
intro (rn//rd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
⊢ (qn//qd).denominator ≄ 0 → pn//pd ≃ qn//qd → qn//qd ≃ rn//rd → pn//pd ≃ rn//rd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_nonzero_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
⊢ (qn//qd).denominator ≄ 0 → pn//pd ≃ qn//qd → qn//qd ≃ rn//rd → pn//pd ≃ rn//rd
Tactic:
intro (_ : qd ≄ 0) (_ : pn//pd ≃ qn//qd) (_ : qn//qd ≃ rn//rd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝² : qd ≄ 0
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
⊢ pn//pd ≃ rn//rd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_nonzero_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝² : qd ≄ 0
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
⊢ pn//pd ≃ rn//rd
Tactic:
have : (pn * rd) * qd ≃ (rn * pd) * qd := calc
  (pn * rd) * qd ≃ _ := AA.substL AA.comm
  (rd * pn) * qd ≃ _ := AA.assoc
  rd * (pn * qd) ≃ _ := AA.substR ‹pn * qd ≃ qn * pd›
  rd * (qn * pd) ≃ _ := Rel.symm AA.assoc
  (rd * qn) * pd ≃ _ := AA.substL AA.comm
  (qn * rd) * pd ≃ _ := AA.substL ‹qn * rd ≃ rn * qd›
  (rn * qd) * pd ≃ _ := AA.assoc
  rn * (qd * pd) ≃ _ := AA.substR AA.comm
  rn * (pd * qd) ≃ _ := Rel.symm AA.assoc
  (rn * pd) * qd ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝² : qd ≄ 0
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this : pn * rd * qd ≃ rn * pd * qd
⊢ pn//pd ≃ rn//rd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_nonzero_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝² : qd ≄ 0
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this : pn * rd * qd ≃ rn * pd * qd
⊢ pn//pd ≃ rn//rd
Tactic:
have : pn * rd ≃ rn * pd :=
  Integer.mul_cancelR ‹qd ≄ 0› ‹(pn * rd) * qd ≃ (rn * pd) * qd›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝² : qd ≄ 0
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝ : pn * rd * qd ≃ rn * pd * qd
this : pn * rd ≃ rn * pd
⊢ pn//pd ≃ rn//rd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_nonzero_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝² : qd ≄ 0
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝ : pn * rd * qd ≃ rn * pd * qd
this : pn * rd ≃ rn * pd
⊢ pn//pd ≃ rn//rd
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.zero_over_zero_eqv_any
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
⊢ 0//0 ≃ p
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, 0//0 ≃ p
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.zero_over_zero_eqv_any
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, 0//0 ≃ p
Tactic:
intro (pn//pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
⊢ 0//0 ≃ pn//pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.zero_over_zero_eqv_any
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
⊢ 0//0 ≃ pn//pd
Tactic:
show 0 * pd ≃ pn * 0
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
⊢ 0 * pd ≃ pn * 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.zero_over_zero_eqv_any
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
⊢ 0 * pd ≃ pn * 0
Tactic:
calc
  0 * pd ≃ _ := AA.absorbL
  0      ≃ _ := Rel.symm AA.absorbR
  pn * 0 ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q r : Fraction ℤ
⊢ p ≃ q → q ≃ r → p ≃ r ∨ q.to_prod ≃ (0//0).to_prod
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r ∨ q.to_prod ≃ (0//0).to_prod
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r ∨ q.to_prod ≃ (0//0).to_prod
Tactic:
intro (pn//pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
⊢ pn//pd ≃ q → q ≃ r → pn//pd ≃ r ∨ q.to_prod ≃ (0//0).to_prod
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
⊢ pn//pd ≃ q → q ≃ r → pn//pd ≃ r ∨ q.to_prod ≃ (0//0).to_prod
Tactic:
revert q
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
⊢ ∀ {q : Fraction ℤ}, pn//pd ≃ q → q ≃ r → pn//pd ≃ r ∨ q.to_prod ≃ (0//0).to_prod
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
⊢ ∀ {q : Fraction ℤ}, pn//pd ≃ q → q ≃ r → pn//pd ≃ r ∨ q.to_prod ≃ (0//0).to_prod
Tactic:
intro (qn//qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd qn qd : ℤ
⊢ pn//pd ≃ qn//qd → qn//qd ≃ r → pn//pd ≃ r ∨ (qn//qd).to_prod ≃ (0//0).to_prod
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd qn qd : ℤ
⊢ pn//pd ≃ qn//qd → qn//qd ≃ r → pn//pd ≃ r ∨ (qn//qd).to_prod ≃ (0//0).to_prod
Tactic:
revert r
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
⊢ ∀ {r : Fraction ℤ}, pn//pd ≃ qn//qd → qn//qd ≃ r → pn//pd ≃ r ∨ (qn//qd).to_prod ≃ (0//0).to_prod
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
⊢ ∀ {r : Fraction ℤ}, pn//pd ≃ qn//qd → qn//qd ≃ r → pn//pd ≃ r ∨ (qn//qd).to_prod ≃ (0//0).to_prod
Tactic:
intro (rn//rd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
⊢ pn//pd ≃ qn//qd → qn//qd ≃ rn//rd → pn//pd ≃ rn//rd ∨ (qn//qd).to_prod ≃ (0//0).to_prod
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
⊢ pn//pd ≃ qn//qd → qn//qd ≃ rn//rd → pn//pd ≃ rn//rd ∨ (qn//qd).to_prod ≃ (0//0).to_prod
Tactic:
intro (_ : pn//pd ≃ qn//qd) (_ : qn//qd ≃ rn//rd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
⊢ pn//pd ≃ rn//rd ∨ (qn//qd).to_prod ≃ (0//0).to_prod
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
⊢ pn//pd ≃ rn//rd ∨ (qn//qd).to_prod ≃ (0//0).to_prod
Tactic:
show pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
have : Decidable (qd ≃ 0) := Integer.eqv? qd 0
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this : Decidable (qd ≃ 0)
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this : Decidable (qd ≃ 0)
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
match this with
| isTrue (_ : qd ≃ 0) =>
  have : pn * qd ≃ qn * pd := ‹pn//pd ≃ qn//qd›
  have : qn * rd ≃ rn * qd := ‹qn//qd ≃ rn//rd›
  have : qn * pd ≃ 0 := calc
    qn * pd ≃ _ := Rel.symm ‹pn * qd ≃ qn * pd›
    pn * qd ≃ _ := AA.substR ‹qd ≃ 0›
    pn * 0  ≃ _ := AA.absorbR
    0       ≃ _ := Rel.refl
  have : qn * rd ≃ 0 := calc
    qn * rd ≃ _ := ‹qn * rd ≃ rn * qd›
    rn * qd ≃ _ := AA.substR ‹qd ≃ 0›
    rn * 0  ≃ _ := AA.absorbR
    0       ≃ _ := Rel.refl
  have : qn ≃ 0 ∨ pd ≃ 0 := Integer.mul_split_zero.mp ‹qn * pd ≃ 0›
  have : qn ≃ 0 ∨ rd ≃ 0 := Integer.mul_split_zero.mp ‹qn * rd ≃ 0›
  have : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0) :=
    And.intro ‹qn ≃ 0 ∨ pd ≃ 0› ‹qn ≃ 0 ∨ rd ≃ 0›
  have : qn ≃ 0 ∨ (pd ≃ 0 ∧ rd ≃ 0) :=
    Logic.or_distribL_and.mpr ‹(qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)›
  match ‹qn ≃ 0 ∨ (pd ≃ 0 ∧ rd ≃ 0)› with
  | Or.inl (_ : qn ≃ 0) =>
    have : qn ≃ 0 ∧ qd ≃ 0 := And.intro ‹qn ≃ 0› ‹qd ≃ 0›
    have : (qn, qd) ≃ (0, 0) :=
      Relation.Equivalence.Impl.Prod.eqv_defn.mpr ‹qn ≃ 0 ∧ qd ≃ 0›
    exact Or.inr ‹(qn, qd) ≃ (0, 0)›
  | Or.inr (And.intro (_ : pd ≃ 0) (_ : rd ≃ 0)) =>
    have : pn * rd ≃ rn * pd := calc
      pn * rd ≃ _ := AA.substR ‹rd ≃ 0›
      pn * 0  ≃ _ := AA.absorbR
      0       ≃ _ := Rel.symm AA.absorbR
      rn * 0  ≃ _ := AA.substR (Rel.symm ‹pd ≃ 0›)
      rn * pd ≃ _ := Rel.refl
    exact Or.inl ‹pn * rd ≃ rn * pd›
| isFalse (_ : qd ≄ 0) =>
  have : pn * rd ≃ rn * pd :=
    eqv_trans_nonzero_denom
      (q := qn//qd)
      ‹qd ≄ 0›
      ‹pn//pd ≃ qn//qd›
      ‹qn//qd ≃ rn//rd›
  exact Or.inl ‹pn * rd ≃ rn * pd›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
have : pn * qd ≃ qn * pd := ‹pn//pd ≃ qn//qd›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this : pn * qd ≃ qn * pd
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this : pn * qd ≃ qn * pd
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
have : qn * rd ≃ rn * qd := ‹qn//qd ≃ rn//rd›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝¹ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝ : pn * qd ≃ qn * pd
this : qn * rd ≃ rn * qd
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝¹ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝ : pn * qd ≃ qn * pd
this : qn * rd ≃ rn * qd
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
have : qn * pd ≃ 0 := calc
  qn * pd ≃ _ := Rel.symm ‹pn * qd ≃ qn * pd›
  pn * qd ≃ _ := AA.substR ‹qd ≃ 0›
  pn * 0  ≃ _ := AA.absorbR
  0       ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝² : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝¹ : pn * qd ≃ qn * pd
this✝ : qn * rd ≃ rn * qd
this : qn * pd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝² : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝¹ : pn * qd ≃ qn * pd
this✝ : qn * rd ≃ rn * qd
this : qn * pd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
have : qn * rd ≃ 0 := calc
  qn * rd ≃ _ := ‹qn * rd ≃ rn * qd›
  rn * qd ≃ _ := AA.substR ‹qd ≃ 0›
  rn * 0  ≃ _ := AA.absorbR
  0       ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝³ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝² : pn * qd ≃ qn * pd
this✝¹ : qn * rd ≃ rn * qd
this✝ : qn * pd ≃ 0
this : qn * rd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝³ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝² : pn * qd ≃ qn * pd
this✝¹ : qn * rd ≃ rn * qd
this✝ : qn * pd ≃ 0
this : qn * rd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
have : qn ≃ 0 ∨ pd ≃ 0 := Integer.mul_split_zero.mp ‹qn * pd ≃ 0›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁴ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝³ : pn * qd ≃ qn * pd
this✝² : qn * rd ≃ rn * qd
this✝¹ : qn * pd ≃ 0
this✝ : qn * rd ≃ 0
this : qn ≃ 0 ∨ pd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁴ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝³ : pn * qd ≃ qn * pd
this✝² : qn * rd ≃ rn * qd
this✝¹ : qn * pd ≃ 0
this✝ : qn * rd ≃ 0
this : qn ≃ 0 ∨ pd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
have : qn ≃ 0 ∨ rd ≃ 0 := Integer.mul_split_zero.mp ‹qn * rd ≃ 0›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁵ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝⁴ : pn * qd ≃ qn * pd
this✝³ : qn * rd ≃ rn * qd
this✝² : qn * pd ≃ 0
this✝¹ : qn * rd ≃ 0
this✝ : qn ≃ 0 ∨ pd ≃ 0
this : qn ≃ 0 ∨ rd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁵ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝⁴ : pn * qd ≃ qn * pd
this✝³ : qn * rd ≃ rn * qd
this✝² : qn * pd ≃ 0
this✝¹ : qn * rd ≃ 0
this✝ : qn ≃ 0 ∨ pd ≃ 0
this : qn ≃ 0 ∨ rd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
have : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0) :=
  And.intro ‹qn ≃ 0 ∨ pd ≃ 0› ‹qn ≃ 0 ∨ rd ≃ 0›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁶ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝⁵ : pn * qd ≃ qn * pd
this✝⁴ : qn * rd ≃ rn * qd
this✝³ : qn * pd ≃ 0
this✝² : qn * rd ≃ 0
this✝¹ : qn ≃ 0 ∨ pd ≃ 0
this✝ : qn ≃ 0 ∨ rd ≃ 0
this : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁶ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝⁵ : pn * qd ≃ qn * pd
this✝⁴ : qn * rd ≃ rn * qd
this✝³ : qn * pd ≃ 0
this✝² : qn * rd ≃ 0
this✝¹ : qn ≃ 0 ∨ pd ≃ 0
this✝ : qn ≃ 0 ∨ rd ≃ 0
this : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
have : qn ≃ 0 ∨ (pd ≃ 0 ∧ rd ≃ 0) :=
  Logic.or_distribL_and.mpr ‹(qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁷ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝⁶ : pn * qd ≃ qn * pd
this✝⁵ : qn * rd ≃ rn * qd
this✝⁴ : qn * pd ≃ 0
this✝³ : qn * rd ≃ 0
this✝² : qn ≃ 0 ∨ pd ≃ 0
this✝¹ : qn ≃ 0 ∨ rd ≃ 0
this✝ : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)
this : qn ≃ 0 ∨ pd ≃ 0 ∧ rd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁷ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝⁶ : pn * qd ≃ qn * pd
this✝⁵ : qn * rd ≃ rn * qd
this✝⁴ : qn * pd ≃ 0
this✝³ : qn * rd ≃ 0
this✝² : qn ≃ 0 ∨ pd ≃ 0
this✝¹ : qn ≃ 0 ∨ rd ≃ 0
this✝ : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)
this : qn ≃ 0 ∨ pd ≃ 0 ∧ rd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
match ‹qn ≃ 0 ∨ (pd ≃ 0 ∧ rd ≃ 0)› with
| Or.inl (_ : qn ≃ 0) =>
  have : qn ≃ 0 ∧ qd ≃ 0 := And.intro ‹qn ≃ 0› ‹qd ≃ 0›
  have : (qn, qd) ≃ (0, 0) :=
    Relation.Equivalence.Impl.Prod.eqv_defn.mpr ‹qn ≃ 0 ∧ qd ≃ 0›
  exact Or.inr ‹(qn, qd) ≃ (0, 0)›
| Or.inr (And.intro (_ : pd ≃ 0) (_ : rd ≃ 0)) =>
  have : pn * rd ≃ rn * pd := calc
    pn * rd ≃ _ := AA.substR ‹rd ≃ 0›
    pn * 0  ≃ _ := AA.absorbR
    0       ≃ _ := Rel.symm AA.absorbR
    rn * 0  ≃ _ := AA.substR (Rel.symm ‹pd ≃ 0›)
    rn * pd ≃ _ := Rel.refl
  exact Or.inl ‹pn * rd ≃ rn * pd›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁷ : Decidable (qd ≃ 0)
h✝¹ : qd ≃ 0
this✝⁶ : pn * qd ≃ qn * pd
this✝⁵ : qn * rd ≃ rn * qd
this✝⁴ : qn * pd ≃ 0
this✝³ : qn * rd ≃ 0
this✝² : qn ≃ 0 ∨ pd ≃ 0
this✝¹ : qn ≃ 0 ∨ rd ≃ 0
this✝ : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)
this : qn ≃ 0 ∨ pd ≃ 0 ∧ rd ≃ 0
h✝ : qn ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
have : qn ≃ 0 ∧ qd ≃ 0 := And.intro ‹qn ≃ 0› ‹qd ≃ 0›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁸ : Decidable (qd ≃ 0)
h✝¹ : qd ≃ 0
this✝⁷ : pn * qd ≃ qn * pd
this✝⁶ : qn * rd ≃ rn * qd
this✝⁵ : qn * pd ≃ 0
this✝⁴ : qn * rd ≃ 0
this✝³ : qn ≃ 0 ∨ pd ≃ 0
this✝² : qn ≃ 0 ∨ rd ≃ 0
this✝¹ : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)
this✝ : qn ≃ 0 ∨ pd ≃ 0 ∧ rd ≃ 0
h✝ : qn ≃ 0
this : qn ≃ 0 ∧ qd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁸ : Decidable (qd ≃ 0)
h✝¹ : qd ≃ 0
this✝⁷ : pn * qd ≃ qn * pd
this✝⁶ : qn * rd ≃ rn * qd
this✝⁵ : qn * pd ≃ 0
this✝⁴ : qn * rd ≃ 0
this✝³ : qn ≃ 0 ∨ pd ≃ 0
this✝² : qn ≃ 0 ∨ rd ≃ 0
this✝¹ : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)
this✝ : qn ≃ 0 ∨ pd ≃ 0 ∧ rd ≃ 0
h✝ : qn ≃ 0
this : qn ≃ 0 ∧ qd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
have : (qn, qd) ≃ (0, 0) :=
  Relation.Equivalence.Impl.Prod.eqv_defn.mpr ‹qn ≃ 0 ∧ qd ≃ 0›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁹ : Decidable (qd ≃ 0)
h✝¹ : qd ≃ 0
this✝⁸ : pn * qd ≃ qn * pd
this✝⁷ : qn * rd ≃ rn * qd
this✝⁶ : qn * pd ≃ 0
this✝⁵ : qn * rd ≃ 0
this✝⁴ : qn ≃ 0 ∨ pd ≃ 0
this✝³ : qn ≃ 0 ∨ rd ≃ 0
this✝² : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)
this✝¹ : qn ≃ 0 ∨ pd ≃ 0 ∧ rd ≃ 0
h✝ : qn ≃ 0
this✝ : qn ≃ 0 ∧ qd ≃ 0
this : (qn, qd) ≃ (0, 0)
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁹ : Decidable (qd ≃ 0)
h✝¹ : qd ≃ 0
this✝⁸ : pn * qd ≃ qn * pd
this✝⁷ : qn * rd ≃ rn * qd
this✝⁶ : qn * pd ≃ 0
this✝⁵ : qn * rd ≃ 0
this✝⁴ : qn ≃ 0 ∨ pd ≃ 0
this✝³ : qn ≃ 0 ∨ rd ≃ 0
this✝² : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)
this✝¹ : qn ≃ 0 ∨ pd ≃ 0 ∧ rd ≃ 0
h✝ : qn ≃ 0
this✝ : qn ≃ 0 ∧ qd ≃ 0
this : (qn, qd) ≃ (0, 0)
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
exact Or.inr ‹(qn, qd) ≃ (0, 0)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁷ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝⁶ : pn * qd ≃ qn * pd
this✝⁵ : qn * rd ≃ rn * qd
this✝⁴ : qn * pd ≃ 0
this✝³ : qn * rd ≃ 0
this✝² : qn ≃ 0 ∨ pd ≃ 0
this✝¹ : qn ≃ 0 ∨ rd ≃ 0
this✝ : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)
this : qn ≃ 0 ∨ pd ≃ 0 ∧ rd ≃ 0
left✝ : pd ≃ 0
right✝ : rd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
have : pn * rd ≃ rn * pd := calc
  pn * rd ≃ _ := AA.substR ‹rd ≃ 0›
  pn * 0  ≃ _ := AA.absorbR
  0       ≃ _ := Rel.symm AA.absorbR
  rn * 0  ≃ _ := AA.substR (Rel.symm ‹pd ≃ 0›)
  rn * pd ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁸ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝⁷ : pn * qd ≃ qn * pd
this✝⁶ : qn * rd ≃ rn * qd
this✝⁵ : qn * pd ≃ 0
this✝⁴ : qn * rd ≃ 0
this✝³ : qn ≃ 0 ∨ pd ≃ 0
this✝² : qn ≃ 0 ∨ rd ≃ 0
this✝¹ : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)
this✝ : qn ≃ 0 ∨ pd ≃ 0 ∧ rd ≃ 0
left✝ : pd ≃ 0
right✝ : rd ≃ 0
this : pn * rd ≃ rn * pd
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_almost
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝⁸ : Decidable (qd ≃ 0)
h✝ : qd ≃ 0
this✝⁷ : pn * qd ≃ qn * pd
this✝⁶ : qn * rd ≃ rn * qd
this✝⁵ : qn * pd ≃ 0
this✝⁴ : qn * rd ≃ 0
this✝³ : qn ≃ 0 ∨ pd ≃ 0
this✝² : qn ≃ 0 ∨ rd ≃ 0
this✝¹ : (qn ≃ 0 ∨ pd ≃ 0) ∧ (qn ≃ 0 ∨ rd ≃ 0)
this✝ : qn ≃ 0 ∨ pd ≃ 0 ∧ rd ≃ 0
left✝ : pd ≃ 0
right✝ : rd ≃ 0
this : pn * rd ≃ rn * pd
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
exact Or.inl ‹pn * rd ≃ rn * pd›
Proof state after:
no goals