internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_compat_from_integer
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ from_integer (a * b) ≃ from_integer a * from_integer b
Tactic:
show (a * b)//1 ≃ a//1 * b//1
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ (a * b)//1 ≃ a//1 * b//1
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_compat_from_integer
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ (a * b)//1 ≃ a//1 * b//1
Tactic:
have : a//1 * b//1 ≃ (a * b)//1 := calc
  a//1 * b//1      ≃ _ := eqv_refl
  (a * b)//(1 * 1) ≃ _ := substD AA.identL
  (a * b)//1       ≃ _ := eqv_refl
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
this : a//1 * b//1 ≃ (a * b)//1
⊢ (a * b)//1 ≃ a//1 * b//1
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_compat_from_integer
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
this : a//1 * b//1 ≃ (a * b)//1
⊢ (a * b)//1 ≃ a//1 * b//1
Tactic:
exact eqv_symm this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_comm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q : Fraction ℤ
⊢ p * q ≃ q * p
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p * q ≃ q * p
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_comm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p * q ≃ q * p
Tactic:
intro (pn//pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd * q ≃ q * pn//pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_comm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd * q ≃ q * pn//pd
Tactic:
revert q
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ ∀ {q : Fraction ℤ}, pn//pd * q ≃ q * pn//pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_comm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ ∀ {q : Fraction ℤ}, pn//pd * q ≃ q * pn//pd
Tactic:
intro (qn//qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝¹ : AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ pn//pd * qn//qd ≃ qn//qd * pn//pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_comm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝¹ : AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ pn//pd * qn//qd ≃ qn//qd * pn//pd
Tactic:
calc
  pn//pd * qn//qd      ≃ _ := eqv_refl
  (pn * qn)//(pd * qd) ≃ _ := substN AA.comm
  (qn * pn)//(pd * qd) ≃ _ := substD AA.comm
  (qn * pn)//(qd * pd) ≃ _ := eqv_refl
  qn//qd * pn//pd      ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁ p₂ q : Fraction ℤ
⊢ p₁ ≃ p₂ → p₁ * q ≃ p₂ * q
Tactic:
revert p₁
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ q : Fraction ℤ
⊢ ∀ {p₁ : Fraction ℤ}, p₁ ≃ p₂ → p₁ * q ≃ p₂ * q
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ q : Fraction ℤ
⊢ ∀ {p₁ : Fraction ℤ}, p₁ ≃ p₂ → p₁ * q ≃ p₂ * q
Tactic:
intro (p₁n//p₁d)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : AP (Positive p₁d)
⊢ p₁n//p₁d ≃ p₂ → p₁n//p₁d * q ≃ p₂ * q
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : AP (Positive p₁d)
⊢ p₁n//p₁d ≃ p₂ → p₁n//p₁d * q ≃ p₂ * q
Tactic:
revert p₂
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : AP (Positive p₁d)
⊢ ∀ {p₂ : Fraction ℤ}, p₁n//p₁d ≃ p₂ → p₁n//p₁d * q ≃ p₂ * q
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : AP (Positive p₁d)
⊢ ∀ {p₂ : Fraction ℤ}, p₁n//p₁d ≃ p₂ → p₁n//p₁d * q ≃ p₂ * q
Tactic:
intro (p₂n//p₂d)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : AP (Positive p₂d)
⊢ p₁n//p₁d ≃ p₂n//p₂d → p₁n//p₁d * q ≃ p₂n//p₂d * q
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : AP (Positive p₂d)
⊢ p₁n//p₁d ≃ p₂n//p₂d → p₁n//p₁d * q ≃ p₂n//p₂d * q
Tactic:
revert q
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : AP (Positive p₂d)
⊢ ∀ {q : Fraction ℤ}, p₁n//p₁d ≃ p₂n//p₂d → p₁n//p₁d * q ≃ p₂n//p₂d * q
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : AP (Positive p₂d)
⊢ ∀ {q : Fraction ℤ}, p₁n//p₁d ≃ p₂n//p₂d → p₁n//p₁d * q ≃ p₂n//p₂d * q
Tactic:
intro (qn//qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ p₁n//p₁d ≃ p₂n//p₂d → p₁n//p₁d * qn//qd ≃ p₂n//p₂d * qn//qd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ p₁n//p₁d ≃ p₂n//p₂d → p₁n//p₁d * qn//qd ≃ p₂n//p₂d * qn//qd
Tactic:
intro (_ : p₁n//p₁d ≃ p₂n//p₂d)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ p₁n//p₁d * qn//qd ≃ p₂n//p₂d * qn//qd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ p₁n//p₁d * qn//qd ≃ p₂n//p₂d * qn//qd
Tactic:
show (p₁n * qn)//(p₁d * qd) ≃ (p₂n * qn)//(p₂d * qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ (p₁n * qn)//(p₁d * qd) ≃ (p₂n * qn)//(p₂d * qd)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ (p₁n * qn)//(p₁d * qd) ≃ (p₂n * qn)//(p₂d * qd)
Tactic:
show (p₁n * qn) * (p₂d * qd) ≃ (p₂n * qn) * (p₁d * qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ p₁n * qn * (p₂d * qd) ≃ p₂n * qn * (p₁d * qd)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ p₁n * qn * (p₂d * qd) ≃ p₂n * qn * (p₁d * qd)
Tactic:
have : p₁n * p₂d ≃ p₂n * p₁d := ‹p₁n//p₁d ≃ p₂n//p₂d›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
this : p₁n * p₂d ≃ p₂n * p₁d
⊢ p₁n * qn * (p₂d * qd) ≃ p₂n * qn * (p₁d * qd)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
this : p₁n * p₂d ≃ p₂n * p₁d
⊢ p₁n * qn * (p₂d * qd) ≃ p₂n * qn * (p₁d * qd)
Tactic:
calc
  (p₁n * qn) * (p₂d * qd) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (p₁n * p₂d) * (qn * qd) ≃ _ := AA.substL ‹p₁n * p₂d ≃ p₂n * p₁d›
  (p₂n * p₁d) * (qn * qd) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (p₂n * qn) * (p₁d * qd) ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_substR
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q₁ q₂ : Fraction ℤ
⊢ q₁ ≃ q₂ → p * q₁ ≃ p * q₂
Tactic:
intro (_ : q₁ ≃ q₂)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q₁ q₂ : Fraction ℤ
x✝ : q₁ ≃ q₂
⊢ p * q₁ ≃ p * q₂
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_substR
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q₁ q₂ : Fraction ℤ
x✝ : q₁ ≃ q₂
⊢ p * q₁ ≃ p * q₂
Tactic:
calc
  p * q₁ ≃ _ := mul_comm
  q₁ * p ≃ _ := mul_substL ‹q₁ ≃ q₂›
  q₂ * p ≃ _ := mul_comm
  p * q₂ ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_assoc
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q r : Fraction ℤ
⊢ p * q * r ≃ p * (q * r)
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p * q * r ≃ p * (q * r)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_assoc
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p * q * r ≃ p * (q * r)
Tactic:
intro (pn//pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd * q * r ≃ pn//pd * (q * r)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_assoc
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd * q * r ≃ pn//pd * (q * r)
Tactic:
revert q
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ ∀ {q : Fraction ℤ}, pn//pd * q * r ≃ pn//pd * (q * r)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_assoc
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ ∀ {q : Fraction ℤ}, pn//pd * q * r ≃ pn//pd * (q * r)
Tactic:
intro (qn//qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝¹ : AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ pn//pd * qn//qd * r ≃ pn//pd * (qn//qd * r)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_assoc
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝¹ : AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ pn//pd * qn//qd * r ≃ pn//pd * (qn//qd * r)
Tactic:
revert r
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝¹ : AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ ∀ {r : Fraction ℤ}, pn//pd * qn//qd * r ≃ pn//pd * (qn//qd * r)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_assoc
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝¹ : AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ ∀ {r : Fraction ℤ}, pn//pd * qn//qd * r ≃ pn//pd * (qn//qd * r)
Tactic:
intro (rn//rd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝² : AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : AP (Positive rd)
⊢ pn//pd * qn//qd * rn//rd ≃ pn//pd * (qn//qd * rn//rd)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_assoc
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝² : AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : AP (Positive rd)
⊢ pn//pd * qn//qd * rn//rd ≃ pn//pd * (qn//qd * rn//rd)
Tactic:
calc
  (pn//pd * qn//qd) * rn//rd         ≃ _ := eqv_refl
  (pn * qn)//(pd * qd) * rn//rd      ≃ _ := eqv_refl
  ((pn * qn) * rn)//((pd * qd) * rd) ≃ _ := substN AA.assoc
  (pn * (qn * rn))//((pd * qd) * rd) ≃ _ := substD AA.assoc
  (pn * (qn * rn))//(pd * (qd * rd)) ≃ _ := eqv_refl
  pn//pd * (qn * rn)//(qd * rd)      ≃ _ := eqv_refl
  pn//pd * (qn//qd * rn//rd)         ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_identL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
⊢ 1 * p ≃ p
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, 1 * p ≃ p
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_identL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, 1 * p ≃ p
Tactic:
intro (pn//pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ 1 * pn//pd ≃ pn//pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_identL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ 1 * pn//pd ≃ pn//pd
Tactic:
calc
  1 * pn//pd         ≃ _ := eqv_refl
  1//1 * pn//pd      ≃ _ := eqv_refl
  (1 * pn)//(1 * pd) ≃ _ := substN AA.identL
  pn//(1 * pd)       ≃ _ := substD AA.identL
  pn//pd             ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_distribL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q r : Fraction ℤ
⊢ p * (q + r) ≃ p * q + p * r
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p * (q + r) ≃ p * q + p * r
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_distribL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p * (q + r) ≃ p * q + p * r
Tactic:
intro (pn//pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd * (q + r) ≃ pn//pd * q + pn//pd * r
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_distribL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd * (q + r) ≃ pn//pd * q + pn//pd * r
Tactic:
revert q
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ ∀ {q : Fraction ℤ}, pn//pd * (q + r) ≃ pn//pd * q + pn//pd * r
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_distribL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ ∀ {q : Fraction ℤ}, pn//pd * (q + r) ≃ pn//pd * q + pn//pd * r
Tactic:
intro (qn//qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝¹ : AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ pn//pd * (qn//qd + r) ≃ pn//pd * qn//qd + pn//pd * r
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_distribL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝¹ : AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ pn//pd * (qn//qd + r) ≃ pn//pd * qn//qd + pn//pd * r
Tactic:
revert r
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝¹ : AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ ∀ {r : Fraction ℤ}, pn//pd * (qn//qd + r) ≃ pn//pd * qn//qd + pn//pd * r
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_distribL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝¹ : AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : AP (Positive qd)
⊢ ∀ {r : Fraction ℤ}, pn//pd * (qn//qd + r) ≃ pn//pd * qn//qd + pn//pd * r
Tactic:
intro (rn//rd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝² : AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : AP (Positive rd)
⊢ pn//pd * (qn//qd + rn//rd) ≃ pn//pd * qn//qd + pn//pd * rn//rd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_distribL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝² : AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : AP (Positive rd)
⊢ pn//pd * (qn//qd + rn//rd) ≃ pn//pd * qn//qd + pn//pd * rn//rd
Tactic:
have pos_mul_denom_prq : AP (Positive (pd * (rd * qd))) := inferInstance
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝² : AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : AP (Positive rd)
pos_mul_denom_prq : AP (Positive (pd * (rd * qd)))
⊢ pn//pd * (qn//qd + rn//rd) ≃ pn//pd * qn//qd + pn//pd * rn//rd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_distribL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝² : AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : AP (Positive rd)
pos_mul_denom_prq : AP (Positive (pd * (rd * qd)))
⊢ pn//pd * (qn//qd + rn//rd) ≃ pn//pd * qn//qd + pn//pd * rn//rd
Tactic:
calc
  pn//pd * (qn//qd + rn//rd)
    ≃ _ := eqv_refl
  pn//pd * (qn * rd + qd * rn)//(qd * rd)
    ≃ _ := eqv_refl
  (pn * (qn * rd + qd * rn))//(pd * (qd * rd))
    ≃ _ := substN AA.distribL
  (pn * (qn * rd) + pn * (qd * rn))//(pd * (qd * rd))
    ≃ _ := eqv_symm add_eqv_denominators
  (pn * (qn * rd))//(pd * (qd * rd)) + (pn * (qd * rn))//(pd * (qd * rd))
    ≃ _ := add_substL (substN (Rel.symm AA.assoc))
  ((pn * qn) * rd)//(pd * (qd * rd)) + (pn * (qd * rn))//(pd * (qd * rd))
    ≃ _ := add_substL (substD (Rel.symm AA.assoc))
  ((pn * qn) * rd)//((pd * qd) * rd) + (pn * (qd * rn))//(pd * (qd * rd))
    ≃ _ := add_substL cancelR
  (pn * qn)//(pd * qd) + (pn * (qd * rn))//(pd * (qd * rd))
    ≃ _ := add_substR (substN (AA.substR AA.comm))
  (pn * qn)//(pd * qd) + (pn * (rn * qd))//(pd * (qd * rd))
    ≃ _ := add_substR (substD (pb₂ := pos_mul_denom_prq) (AA.substR AA.comm))
  (pn * qn)//(pd * qd) + (pn * (rn * qd))//(pd * (rd * qd))
    ≃ _ := add_substR (substN (Rel.symm AA.assoc))
  (pn * qn)//(pd * qd) + ((pn * rn) * qd)//(pd * (rd * qd))
    ≃ _ := add_substR (substD (Rel.symm AA.assoc))
  (pn * qn)//(pd * qd) + ((pn * rn) * qd)//((pd * rd) * qd)
    ≃ _ := add_substR cancelR
  (pn * qn)//(pd * qd) + (pn * rn)//(pd * rd)
    ≃ _ := eqv_refl
  pn//pd * qn//qd + (pn * rn)//(pd * rd)
    ≃ _ := eqv_refl
  pn//pd * qn//qd + pn//pd * rn//rd
    ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Relation.trans_failL
Proof state before:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
⊢ ¬R x y → R y z → ¬R x z
Tactic:
intro (_ : ¬ R x y) (_ : R y z) (_ : R x z)
Proof state after:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
x✝² : ¬R x y
x✝¹ : R y z
x✝ : R x z
⊢ False
Theorem: Lean4Axiomatic.Relation.trans_failL
Proof state before:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
x✝² : ¬R x y
x✝¹ : R y z
x✝ : R x z
⊢ False
Tactic:
have : R x y := trans ‹R x z› (symm ‹R y z›)
Proof state after:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
x✝² : ¬R x y
x✝¹ : R y z
x✝ : R x z
this : R x y
⊢ False
Theorem: Lean4Axiomatic.Relation.trans_failL
Proof state before:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
x✝² : ¬R x y
x✝¹ : R y z
x✝ : R x z
this : R x y
⊢ False
Tactic:
exact ‹¬ R x y› ‹R x y›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Relation.trans_failR
Proof state before:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
⊢ R x y → ¬R y z → ¬R x z
Tactic:
intro (_ : R x y) (_ : ¬ R y z) (_ : R x z)
Proof state after:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
x✝² : R x y
x✝¹ : ¬R y z
x✝ : R x z
⊢ False
Theorem: Lean4Axiomatic.Relation.trans_failR
Proof state before:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
x✝² : R x y
x✝¹ : ¬R y z
x✝ : R x z
⊢ False
Tactic:
have : R y z := trans (symm ‹R x y›) ‹R x z›
Proof state after:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
x✝² : R x y
x✝¹ : ¬R y z
x✝ : R x z
this : R y z
⊢ False
Theorem: Lean4Axiomatic.Relation.trans_failR
Proof state before:
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
x✝² : R x y
x✝¹ : ¬R y z
x✝ : R x z
this : R y z
⊢ False
Tactic:
exact ‹¬ R y z› ‹R y z›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Relation.Equivalence.iff_subst_eqv
Proof state before:
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
⊢ x₁ ≃ x₂ → (P x₁ ↔ P x₂)
Tactic:
intro (_ : x₁ ≃ x₂)
Proof state after:
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
x✝ : x₁ ≃ x₂
⊢ P x₁ ↔ P x₂
Theorem: Lean4Axiomatic.Relation.Equivalence.iff_subst_eqv
Proof state before:
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
x✝ : x₁ ≃ x₂
⊢ P x₁ ↔ P x₂
Tactic:
have : P x₁ → P x₂ := P_subst ‹x₁ ≃ x₂›
Proof state after:
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
x✝ : x₁ ≃ x₂
this : P x₁ → P x₂
⊢ P x₁ ↔ P x₂
Theorem: Lean4Axiomatic.Relation.Equivalence.iff_subst_eqv
Proof state before:
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
x✝ : x₁ ≃ x₂
this : P x₁ → P x₂
⊢ P x₁ ↔ P x₂
Tactic:
have : P x₂ → P x₁ := P_subst (symm ‹x₁ ≃ x₂›)
Proof state after:
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
x✝ : x₁ ≃ x₂
this✝ : P x₁ → P x₂
this : P x₂ → P x₁
⊢ P x₁ ↔ P x₂
Theorem: Lean4Axiomatic.Relation.Equivalence.iff_subst_eqv
Proof state before:
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
x✝ : x₁ ≃ x₂
this✝ : P x₁ → P x₂
this : P x₂ → P x₁
⊢ P x₁ ↔ P x₂
Tactic:
exact Iff.intro ‹P x₁ → P x₂› ‹P x₂ → P x₁›
Proof state after:
no goals