internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_subst
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ : Difference ℕ
⊢ a₁ ≃ a₂ → -a₁ ≃ -a₂
Tactic:
revert a₁
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₂ : Difference ℕ
⊢ ∀ {a₁ : Difference ℕ}, a₁ ≃ a₂ → -a₁ ≃ -a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_subst
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₂ : Difference ℕ
⊢ ∀ {a₁ : Difference ℕ}, a₁ ≃ a₂ → -a₁ ≃ -a₂
Tactic:
intro (n——m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₂ : Difference ℕ
n m : ℕ
⊢ n——m ≃ a₂ → -n——m ≃ -a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_subst
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₂ : Difference ℕ
n m : ℕ
⊢ n——m ≃ a₂ → -n——m ≃ -a₂
Tactic:
revert a₂
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ ∀ {a₂ : Difference ℕ}, n——m ≃ a₂ → -n——m ≃ -a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_subst
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ ∀ {a₂ : Difference ℕ}, n——m ≃ a₂ → -n——m ≃ -a₂
Tactic:
intro (k——j)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ n——m ≃ k——j → -n——m ≃ -k——j
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_subst
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ n——m ≃ k——j → -n——m ≃ -k——j
Tactic:
intro (_ : n——m ≃ k——j)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
⊢ -n——m ≃ -k——j
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_subst
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
⊢ -n——m ≃ -k——j
Tactic:
have : n + j ≃ k + m := ‹n——m ≃ k——j›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ -n——m ≃ -k——j
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_subst
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ -n——m ≃ -k——j
Tactic:
show m——n ≃ j——k
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ m——n ≃ j——k
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_subst
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ m——n ≃ j——k
Tactic:
show m + k ≃ j + n
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ m + k ≃ j + n
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_subst
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ m + k ≃ j + n
Tactic:
calc
  m + k ≃ _ := AA.comm
  k + m ≃ _ := Rel.symm ‹n + j ≃ k + m›
  n + j ≃ _ := AA.comm
  j + n ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_invL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a : Difference ℕ
⊢ -a + a ≃ 0
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, -a + a ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_invL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, -a + a ≃ 0
Tactic:
intro (n——m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ -n——m + n——m ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_invL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ -n——m + n——m ≃ 0
Tactic:
show -(n——m) + n——m ≃ 0——0
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ -n——m + n——m ≃ 0——0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_invL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ -n——m + n——m ≃ 0——0
Tactic:
show m——n + n——m ≃ 0——0
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ m——n + n——m ≃ 0——0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_invL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ m——n + n——m ≃ 0——0
Tactic:
show (m + n)——(n + m) ≃ 0——0
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (m + n)——(n + m) ≃ 0——0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_invL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (m + n)——(n + m) ≃ 0——0
Tactic:
show (m + n) + 0 ≃ 0 + (n + m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ m + n + 0 ≃ 0 + (n + m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_invL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ m + n + 0 ≃ 0 + (n + m)
Tactic:
apply Natural.add_swapped_zeros_eqv.mpr
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ m + n ≃ n + m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_invL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ m + n ≃ n + m
Tactic:
exact AA.comm
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_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.add_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 * 1 + 1 * b)//(1 * 1) ≃ _ := substN (AA.substL AA.identR)
  (a + 1 * b)//(1 * 1)     ≃ _ := substN (AA.substR AA.identL)
  (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.add_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.add_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.add_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✝ : Logic.AP (Positive pd)
⊢ pn//pd + q ≃ q + pn//pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_comm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : Logic.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✝ : Logic.AP (Positive pd)
⊢ ∀ {q : Fraction ℤ}, pn//pd + q ≃ q + pn//pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_comm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : Logic.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✝¹ : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
⊢ pn//pd + qn//qd ≃ qn//qd + pn//pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_comm
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝¹ : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
⊢ pn//pd + qn//qd ≃ qn//qd + pn//pd
Tactic:
calc
  pn//pd + qn//qd                ≃ _ := eqv_refl
  (pn * qd + pd * qn)//(pd * qd) ≃ _ := substN (AA.substL AA.comm)
  (qd * pn + pd * qn)//(pd * qd) ≃ _ := substN (AA.substR AA.comm)
  (qd * pn + qn * pd)//(pd * qd) ≃ _ := substN AA.comm
  (qn * pd + qd * pn)//(pd * qd) ≃ _ := substD AA.comm
  (qn * pd + qd * pn)//(qd * pd) ≃ _ := eqv_refl
  qn//qd + pn//pd                ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_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.add_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✝ : Logic.AP (Positive p₁d)
⊢ p₁n//p₁d ≃ p₂ → p₁n//p₁d + q ≃ p₂ + q
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : Logic.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✝ : Logic.AP (Positive p₁d)
⊢ ∀ {p₂ : Fraction ℤ}, p₁n//p₁d ≃ p₂ → p₁n//p₁d + q ≃ p₂ + q
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : Logic.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✝¹ : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.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.add_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.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✝¹ : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.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.add_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.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✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.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.add_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.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✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.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.add_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.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 * qd + p₁d * qn)//(p₁d * qd) ≃ (p₂n * qd + p₂d * qn)//(p₂d * qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ (p₁n * qd + p₁d * qn)//(p₁d * qd) ≃ (p₂n * qd + p₂d * qn)//(p₂d * qd)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ (p₁n * qd + p₁d * qn)//(p₁d * qd) ≃ (p₂n * qd + p₂d * qn)//(p₂d * qd)
Tactic:
show (p₁n * qd + p₁d * qn) * (p₂d * qd) ≃ (p₂n * qd + p₂d * qn) * (p₁d * qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ (p₁n * qd + p₁d * qn) * (p₂d * qd) ≃ (p₂n * qd + p₂d * qn) * (p₁d * qd)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ (p₁n * qd + p₁d * qn) * (p₂d * qd) ≃ (p₂n * qd + p₂d * 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✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
this : p₁n * p₂d ≃ p₂n * p₁d
⊢ (p₁n * qd + p₁d * qn) * (p₂d * qd) ≃ (p₂n * qd + p₂d * qn) * (p₁d * qd)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_substL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝² : Logic.AP (Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝¹ : Logic.AP (Positive p₂d)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
this : p₁n * p₂d ≃ p₂n * p₁d
⊢ (p₁n * qd + p₁d * qn) * (p₂d * qd) ≃ (p₂n * qd + p₂d * qn) * (p₁d * qd)
Tactic:
calc
  (p₁n * qd + p₁d * qn) * (p₂d * qd)
    ≃ _ := Rel.symm AA.assoc
  ((p₁n * qd + p₁d * qn) * p₂d) * qd
    ≃ _ := AA.substL AA.distribR
  ((p₁n * qd) * p₂d + (p₁d * qn) * p₂d) * qd
    ≃ _ := AA.substL (AA.substL (AA.substL AA.comm))
  ((qd * p₁n) * p₂d + (p₁d * qn) * p₂d) * qd
    ≃ _ := AA.substL (AA.substL AA.assoc)
  (qd * (p₁n * p₂d) + (p₁d * qn) * p₂d) * qd
    ≃ _ := AA.substL (AA.substL (AA.substR ‹p₁n * p₂d ≃ p₂n * p₁d›))
  (qd * (p₂n * p₁d) + (p₁d * qn) * p₂d) * qd
    ≃ _ := AA.substL (AA.substL (Rel.symm AA.assoc))
  ((qd * p₂n) * p₁d + (p₁d * qn) * p₂d) * qd
    ≃ _ := AA.substL (AA.substR AA.assoc)
  ((qd * p₂n) * p₁d + p₁d * (qn * p₂d)) * qd
    ≃ _ := AA.substL (AA.substR AA.comm)
  ((qd * p₂n) * p₁d + (qn * p₂d) * p₁d) * qd
    ≃ _ := AA.substL (Rel.symm AA.distribR)
  ((qd * p₂n + qn * p₂d) * p₁d) * qd
    ≃ _ := AA.assoc
  (qd * p₂n + qn * p₂d) * (p₁d * qd)
    ≃ _ := AA.substL (AA.substL AA.comm)
  (p₂n * qd + qn * p₂d) * (p₁d * qd)
    ≃ _ := AA.substL (AA.substR AA.comm)
  (p₂n * qd + p₂d * qn) * (p₁d * qd)
    ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_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.add_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₁ ≃ _ := add_comm
  q₁ + p ≃ _ := add_substL ‹q₁ ≃ q₂›
  q₂ + p ≃ _ := add_comm
  p + q₂ ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_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.add_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✝ : Logic.AP (Positive pd)
⊢ pn//pd + q + r ≃ pn//pd + (q + r)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_assoc
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : Logic.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✝ : Logic.AP (Positive pd)
⊢ ∀ {q : Fraction ℤ}, pn//pd + q + r ≃ pn//pd + (q + r)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_assoc
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : Logic.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✝¹ : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
⊢ pn//pd + qn//qd + r ≃ pn//pd + (qn//qd + r)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_assoc
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝¹ : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : Logic.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✝¹ : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
⊢ ∀ {r : Fraction ℤ}, pn//pd + qn//qd + r ≃ pn//pd + (qn//qd + r)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_assoc
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝¹ : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : Logic.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✝² : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : Logic.AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : Logic.AP (Positive rd)
⊢ pn//pd + qn//qd + rn//rd ≃ pn//pd + (qn//qd + rn//rd)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_assoc
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝² : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : Logic.AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : Logic.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 * qd + pd * qn)//(pd * qd) + rn//rd
    ≃ _ := eqv_refl
  ((pn * qd + pd * qn) * rd + (pd * qd) * rn)//((pd * qd) * rd)
    ≃ _ := substN (AA.substL AA.distribR)
  (((pn * qd) * rd + (pd * qn) * rd) + (pd * qd) * rn)//((pd * qd) * rd)
    ≃ _ := substN (AA.substL (AA.substL AA.assoc))
  ((pn * (qd * rd) + (pd * qn) * rd) + (pd * qd) * rn)//((pd * qd) * rd)
    ≃ _ := substN (AA.substL (AA.substR AA.assoc))
  ((pn * (qd * rd) + pd * (qn * rd)) + (pd * qd) * rn)//((pd * qd) * rd)
    ≃ _ := substN (AA.substR AA.assoc)
  ((pn * (qd * rd) + pd * (qn * rd)) + pd * (qd * rn))//((pd * qd) * rd)
    ≃ _ := substN AA.assoc
  (pn * (qd * rd) + (pd * (qn * rd) + pd * (qd * rn)))//((pd * qd) * rd)
    ≃ _ := substN (AA.substR (Rel.symm AA.distribL))
  (pn * (qd * rd) + pd * (qn * rd + qd * rn))//((pd * qd) * rd)
    ≃ _ := substD AA.assoc
  (pn * (qd * rd) + pd * (qn * rd + qd * rn))//(pd * (qd * rd))
    ≃ _ := eqv_refl
  pn//pd + (qn * rd + qd * rn)//(qd * rd)
    ≃ _ := eqv_refl
  pn//pd + (qn//qd + rn//rd)
    ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_identL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
⊢ 0 + p ≃ p
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, 0 + p ≃ p
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_identL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, 0 + p ≃ p
Tactic:
intro (pn//pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Positive pd)
⊢ 0 + pn//pd ≃ pn//pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_identL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Positive pd)
⊢ 0 + pn//pd ≃ pn//pd
Tactic:
show 0//1 + pn//pd ≃ pn//pd
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Positive pd)
⊢ 0//1 + pn//pd ≃ pn//pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_identL
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Positive pd)
⊢ 0//1 + pn//pd ≃ pn//pd
Tactic:
calc
  (0 : ℤ)//1 + pn//pd         ≃ _ := eqv_refl
  (0 * pd + 1 * pn)//(1 * pd) ≃ _ := substN (AA.substL AA.absorbL)
  (0 + 1 * pn)//(1 * pd)      ≃ _ := substN AA.identL
  (1 * pn)//(1 * pd)          ≃ _ := substN AA.identL
  pn//(1 * pd)                ≃ _ := substD AA.identL
  pn//pd                      ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sub_substL
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a₁ a₂ b : ℤ
⊢ a₁ ≃ a₂ → a₁ - b ≃ a₂ - b
Tactic:
intro (_ : a₁ ≃ a₂)
Proof state after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a₁ a₂ b : ℤ
x✝ : a₁ ≃ a₂
⊢ a₁ - b ≃ a₂ - b
Theorem: Lean4Axiomatic.Integer.sub_substL
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a₁ a₂ b : ℤ
x✝ : a₁ ≃ a₂
⊢ a₁ - b ≃ a₂ - b
Tactic:
calc
  a₁ - b    ≃ _ := sub_defn
  a₁ + (-b) ≃ _ := AA.substL ‹a₁ ≃ a₂›
  a₂ + (-b) ≃ _ := Rel.symm sub_defn
  a₂ - b    ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sub_substR
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a₁ a₂ b : ℤ
⊢ a₁ ≃ a₂ → b - a₁ ≃ b - a₂
Tactic:
intro (_ : a₁ ≃ a₂)
Proof state after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a₁ a₂ b : ℤ
x✝ : a₁ ≃ a₂
⊢ b - a₁ ≃ b - a₂