internlm/Lean-Github huggingface dataset:
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 * rd ≃ rn * pd :=
  eqv_trans_nonzero_denom
    (q := qn//qd)
    ‹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✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝ : Decidable (qd ≃ 0)
h✝ : qd ≄ 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 * rd ≃ rn * pd
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
Tactic:
exact Or.inl ‹pn * rd ≃ rn * pd›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_zero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ (a//0 + b//0).to_prod ≃ (0//0).to_prod
Tactic:
show ((a * 0 + 0 * b)//(0 * 0)).to_prod ≃ (0//0).to_prod
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ ((a * 0 + 0 * b)//(0 * 0)).to_prod ≃ (0//0).to_prod
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_zero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ ((a * 0 + 0 * b)//(0 * 0)).to_prod ≃ (0//0).to_prod
Tactic:
show (a * 0 + 0 * b, 0 * 0) ≃ (0, 0)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ (a * 0 + 0 * b, 0 * 0) ≃ (0, 0)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_zero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ (a * 0 + 0 * b, 0 * 0) ≃ (0, 0)
Tactic:
apply Relation.Equivalence.Impl.Prod.eqv_defn.mpr
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * 0 + 0 * b ≃ 0 ∧ 0 * 0 ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_zero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * 0 + 0 * b ≃ 0 ∧ 0 * 0 ≃ 0
Tactic:
apply And.intro
Proof state after:
case left
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * 0 + 0 * b ≃ 0

case right
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ 0 * 0 ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_zero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * 0 + 0 * b ≃ 0
Tactic:
case left =>
  show a * 0 + 0 * b ≃ 0
  calc
    a * 0 + 0 * b ≃ _ := AA.substL AA.absorbR
    0 + 0 * b     ≃ _ := AA.identL
    0 * b         ≃ _ := AA.absorbL
    0             ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_zero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ 0 * 0 ≃ 0
Tactic:
case right =>
  show 0 * 0 ≃ 0
  exact AA.absorbL
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_zero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * 0 + 0 * b ≃ 0
Tactic:
calc
  a * 0 + 0 * b ≃ _ := AA.substL AA.absorbR
  0 + 0 * b     ≃ _ := AA.identL
  0 * b         ≃ _ := AA.absorbL
  0             ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_zero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ 0 * 0 ≃ 0
Tactic:
exact AA.absorbL
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_nonzero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q : Fraction ℤ
⊢ Nonzero p.denominator → Nonzero q.denominator → Nonzero (p + q).denominator
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, Nonzero p.denominator → Nonzero q.denominator → Nonzero (p + q).denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_nonzero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, Nonzero p.denominator → Nonzero q.denominator → Nonzero (p + q).denominator
Tactic:
intro (pn//pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
pn pd : ℤ
⊢ Nonzero (pn//pd).denominator → Nonzero q.denominator → Nonzero (pn//pd + q).denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_nonzero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
pn pd : ℤ
⊢ Nonzero (pn//pd).denominator → Nonzero q.denominator → Nonzero (pn//pd + q).denominator
Tactic:
revert q
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
⊢ ∀ {q : Fraction ℤ}, Nonzero (pn//pd).denominator → Nonzero q.denominator → Nonzero (pn//pd + q).denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_nonzero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
⊢ ∀ {q : Fraction ℤ}, Nonzero (pn//pd).denominator → Nonzero q.denominator → Nonzero (pn//pd + q).denominator
Tactic:
intro (qn//qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
⊢ Nonzero (pn//pd).denominator → Nonzero (qn//qd).denominator → Nonzero (pn//pd + qn//qd).denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_nonzero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
⊢ Nonzero (pn//pd).denominator → Nonzero (qn//qd).denominator → Nonzero (pn//pd + qn//qd).denominator
Tactic:
intro (_ : Nonzero pd) (_ : Nonzero qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Nonzero pd
x✝ : Nonzero qd
⊢ Nonzero (pn//pd + qn//qd).denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_nonzero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Nonzero pd
x✝ : Nonzero qd
⊢ Nonzero (pn//pd + qn//qd).denominator
Tactic:
show Nonzero ((pn * qd + pd * qn)//(pd * qd)).denominator
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Nonzero pd
x✝ : Nonzero qd
⊢ Nonzero ((pn * qd + pd * qn)//(pd * qd)).denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_nonzero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Nonzero pd
x✝ : Nonzero qd
⊢ Nonzero ((pn * qd + pd * qn)//(pd * qd)).denominator
Tactic:
show Nonzero (pd * qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Nonzero pd
x✝ : Nonzero qd
⊢ Nonzero (pd * qd)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_nonzero_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Nonzero pd
x✝ : Nonzero qd
⊢ Nonzero (pd * qd)
Tactic:
exact Integer.mul_preserves_nonzero ‹Nonzero pd› ‹Nonzero qd›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_positive_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q : Fraction ℤ
⊢ Positive p.denominator → Positive q.denominator → Positive (p + q).denominator
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, Positive p.denominator → Positive q.denominator → Positive (p + q).denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_positive_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, Positive p.denominator → Positive q.denominator → Positive (p + q).denominator
Tactic:
intro (pn//pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
pn pd : ℤ
⊢ Positive (pn//pd).denominator → Positive q.denominator → Positive (pn//pd + q).denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_positive_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
pn pd : ℤ
⊢ Positive (pn//pd).denominator → Positive q.denominator → Positive (pn//pd + q).denominator
Tactic:
revert q
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
⊢ ∀ {q : Fraction ℤ}, Positive (pn//pd).denominator → Positive q.denominator → Positive (pn//pd + q).denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_positive_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
⊢ ∀ {q : Fraction ℤ}, Positive (pn//pd).denominator → Positive q.denominator → Positive (pn//pd + q).denominator
Tactic:
intro (qn//qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
⊢ Positive (pn//pd).denominator → Positive (qn//qd).denominator → Positive (pn//pd + qn//qd).denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_positive_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
⊢ Positive (pn//pd).denominator → Positive (qn//qd).denominator → Positive (pn//pd + qn//qd).denominator
Tactic:
intro (_ : Positive pd) (_ : Positive qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Positive pd
x✝ : Positive qd
⊢ Positive (pn//pd + qn//qd).denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_positive_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Positive pd
x✝ : Positive qd
⊢ Positive (pn//pd + qn//qd).denominator
Tactic:
show Positive ((pn * qd + pd * qn)//(pd * qd)).denominator
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Positive pd
x✝ : Positive qd
⊢ Positive ((pn * qd + pd * qn)//(pd * qd)).denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_positive_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Positive pd
x✝ : Positive qd
⊢ Positive ((pn * qd + pd * qn)//(pd * qd)).denominator
Tactic:
show Positive (pd * qd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Positive pd
x✝ : Positive qd
⊢ Positive (pd * qd)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_positive_denominators
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Positive pd
x✝ : Positive qd
⊢ Positive (pd * qd)
Tactic:
exact Integer.mul_preserves_positive ‹Positive pd› ‹Positive qd›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_zero
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n * 0 ≃ 0
Tactic:
apply ind_on (motive := λ x => x * 0 ≃ 0) n
Proof state after:
case zero
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ 0 * 0 ≃ 0

case step
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ ∀ (m : ℕ), m * 0 ≃ 0 → step m * 0 ≃ 0
Theorem: Lean4Axiomatic.Natural.mul_zero
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ 0 * 0 ≃ 0
Tactic:
case zero =>
  show 0 * 0 ≃ 0
  exact zero_mul
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_zero
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ ∀ (m : ℕ), m * 0 ≃ 0 → step m * 0 ≃ 0
Tactic:
case step =>
  intro n (ih : n * 0 ≃ 0)
  show step n * 0 ≃ 0
  calc
    step n * 0 ≃ _ := step_mul
    n * 0 + 0  ≃ _ := AA.substL ih
    0 + 0      ≃ _ := Addition.zero_add
    0          ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_zero
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ 0 * 0 ≃ 0
Tactic:
exact zero_mul
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_zero
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ ∀ (m : ℕ), m * 0 ≃ 0 → step m * 0 ≃ 0
Tactic:
intro n (ih : n * 0 ≃ 0)
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ n : ℕ
ih : n * 0 ≃ 0
⊢ step n * 0 ≃ 0
Theorem: Lean4Axiomatic.Natural.mul_zero
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ n : ℕ
ih : n * 0 ≃ 0
⊢ step n * 0 ≃ 0
Tactic:
calc
  step n * 0 ≃ _ := step_mul
  n * 0 + 0  ≃ _ := AA.substL ih
  0 + 0      ≃ _ := Addition.zero_add
  0          ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_step
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n * step m ≃ n * m + n
Tactic:
apply ind_on (motive := λ x => x * step m ≃ x * m + x) n
Proof state after:
case zero
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * step m ≃ 0 * m + 0

case step
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 * step m ≃ m_1 * m + m_1 → step m_1 * step m ≃ step m_1 * m + step m_1
Theorem: Lean4Axiomatic.Natural.mul_step
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * step m ≃ 0 * m + 0
Tactic:
case zero =>
  show 0 * step m ≃ 0 * m + 0
  calc
    0 * step m ≃ _ := zero_mul
    0          ≃ _ := Rel.symm Addition.zero_add
    0 + 0      ≃ _ := AA.substL (Rel.symm zero_mul)
    0 * m + 0  ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_step
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 * step m ≃ m_1 * m + m_1 → step m_1 * step m ≃ step m_1 * m + step m_1
Tactic:
case step =>
  intro n (ih : n * step m ≃ n * m + n)
  show step n * step m ≃ step n * m + step n
  calc
    step n * step m        ≃ _ := step_mul
    n * step m + step m    ≃ _ := AA.substL ih
    (n * m + n) + step m   ≃ _ := add_step
    step ((n * m + n) + m) ≃ _ := AA.subst₁ AA.assoc
    step (n * m + (n + m)) ≃ _ := AA.subst₁ (AA.substR AA.comm)
    step (n * m + (m + n)) ≃ _ := AA.subst₁ (Rel.symm AA.assoc)
    step ((n * m + m) + n) ≃ _ := AA.subst₁ (AA.substL (Rel.symm step_mul))
    step (step n * m + n)  ≃ _ := Rel.symm add_step
    step n * m + step n    ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_step
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * step m ≃ 0 * m + 0
Tactic:
calc
  0 * step m ≃ _ := zero_mul
  0          ≃ _ := Rel.symm Addition.zero_add
  0 + 0      ≃ _ := AA.substL (Rel.symm zero_mul)
  0 * m + 0  ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_step
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 * step m ≃ m_1 * m + m_1 → step m_1 * step m ≃ step m_1 * m + step m_1
Tactic:
intro n (ih : n * step m ≃ n * m + n)
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
ih : n * step m ≃ n * m + n
⊢ step n * step m ≃ step n * m + step n
Theorem: Lean4Axiomatic.Natural.mul_step
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
ih : n * step m ≃ n * m + n
⊢ step n * step m ≃ step n * m + step n
Tactic:
calc
  step n * step m        ≃ _ := step_mul
  n * step m + step m    ≃ _ := AA.substL ih
  (n * m + n) + step m   ≃ _ := add_step
  step ((n * m + n) + m) ≃ _ := AA.subst₁ AA.assoc
  step (n * m + (n + m)) ≃ _ := AA.subst₁ (AA.substR AA.comm)
  step (n * m + (m + n)) ≃ _ := AA.subst₁ (Rel.symm AA.assoc)
  step ((n * m + m) + n) ≃ _ := AA.subst₁ (AA.substL (Rel.symm step_mul))
  step (step n * m + n)  ≃ _ := Rel.symm add_step
  step n * m + step n    ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_comm
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n * m ≃ m * n
Tactic:
apply ind_on (motive := λ x => x * m ≃ m * x) n
Proof state after:
case zero
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * m ≃ m * 0

case step
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 * m ≃ m * m_1 → step m_1 * m ≃ m * step m_1
Theorem: Lean4Axiomatic.Natural.mul_comm
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * m ≃ m * 0
Tactic:
case zero =>
  show 0 * m ≃ m * 0
  calc
    0 * m ≃ _ := zero_mul
    0     ≃ _ := Rel.symm mul_zero
    m * 0 ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_comm
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 * m ≃ m * m_1 → step m_1 * m ≃ m * step m_1
Tactic:
case step =>
  intro n (ih : n * m ≃ m * n)
  show step n * m ≃ m * step n
  calc
    step n * m ≃ _ := step_mul
    n * m + m  ≃ _ := AA.substL ih
    m * n + m  ≃ _ := Rel.symm mul_step
    m * step n ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_comm
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * m ≃ m * 0
Tactic:
calc
  0 * m ≃ _ := zero_mul
  0     ≃ _ := Rel.symm mul_zero
  m * 0 ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_comm
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 * m ≃ m * m_1 → step m_1 * m ≃ m * step m_1
Tactic:
intro n (ih : n * m ≃ m * n)
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
ih : n * m ≃ m * n
⊢ step n * m ≃ m * step n
Theorem: Lean4Axiomatic.Natural.mul_comm
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
ih : n * m ≃ m * n
⊢ step n * m ≃ m * step n
Tactic:
calc
  step n * m ≃ _ := step_mul
  n * m + m  ≃ _ := AA.substL ih
  m * n + m  ≃ _ := Rel.symm mul_step
  m * step n ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
⊢ n₁ ≃ n₂ → n₁ * m ≃ n₂ * m
Tactic:
apply ind_on (motive := λ x => ∀ y, x ≃ y → x * m ≃ y * m) n₁
Proof state after:
case zero
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
⊢ ∀ (y : ℕ), 0 ≃ y → 0 * m ≃ y * m

case step
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
⊢ ∀ (m_1 : ℕ), (∀ (y : ℕ), m_1 ≃ y → m_1 * m ≃ y * m) → ∀ (y : ℕ), step m_1 ≃ y → step m_1 * m ≃ y * m
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
⊢ ∀ (y : ℕ), 0 ≃ y → 0 * m ≃ y * m
Tactic:
case zero =>
  intro n₂
  show 0 ≃ n₂ → 0 * m ≃ n₂ * m
  apply cases_on (motive := λ y => 0 ≃ y → 0 * m ≃ y * m)
  case zero =>
    intro (_ : 0 ≃ (0 : ℕ))
    show 0 * m ≃ 0 * m
    exact Rel.refl
  case step =>
    intro n₂ (_ : 0 ≃ step n₂)
    exact absurd (Rel.symm ‹0 ≃ step n₂›) step_neqv_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
⊢ ∀ (m_1 : ℕ), (∀ (y : ℕ), m_1 ≃ y → m_1 * m ≃ y * m) → ∀ (y : ℕ), step m_1 ≃ y → step m_1 * m ≃ y * m
Tactic:
case step =>
  intro n₁ (ih : ∀ y, n₁ ≃ y → n₁ * m ≃ y * m) n₂
  show step n₁ ≃ n₂ → step n₁ * m ≃ n₂ * m
  apply cases_on (motive := λ y => step n₁ ≃ y → step n₁ * m ≃ y * m)
  case zero =>
    intro (_ : step n₁ ≃ 0)
    exact absurd ‹step n₁ ≃ 0› step_neqv_zero
  case step =>
    intro n₂ (_ : step n₁ ≃ step n₂)
    show step n₁ * m ≃ step n₂ * m
    have : n₁ ≃ n₂ := AA.inject ‹step n₁ ≃ step n₂›
    have : n₁ * m ≃ n₂ * m := ih n₂ ‹n₁ ≃ n₂›
    calc
      step n₁ * m  ≃ _ := step_mul
      (n₁ * m) + m ≃ _ := AA.substL ‹n₁ * m ≃ n₂ * m›
      (n₂ * m) + m ≃ _ := Rel.symm step_mul
      step n₂ * m  ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
⊢ ∀ (y : ℕ), 0 ≃ y → 0 * m ≃ y * m
Tactic:
intro n₂
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂✝ m n₂ : ℕ
⊢ 0 ≃ n₂ → 0 * m ≃ n₂ * m
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂✝ m n₂ : ℕ
⊢ 0 ≃ n₂ → 0 * m ≃ n₂ * m
Tactic:
apply cases_on (motive := λ y => 0 ≃ y → 0 * m ≃ y * m)
Proof state after:
case zero
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂✝ m n₂ : ℕ
⊢ 0 ≃ 0 → 0 * m ≃ 0 * m

case step
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂✝ m n₂ : ℕ
⊢ ∀ (m_1 : ℕ), 0 ≃ step m_1 → 0 * m ≃ step m_1 * m
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂✝ m n₂ : ℕ
⊢ 0 ≃ 0 → 0 * m ≃ 0 * m
Tactic:
case zero =>
  intro (_ : 0 ≃ (0 : ℕ))
  show 0 * m ≃ 0 * m
  exact Rel.refl
Proof state after:
no goals