internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.le_diff_lower
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
⊢ p - ε ≤ q → -ε ≤ q - p
Tactic:
case mpr =>
  intro (_ : p - ε ≤ q)
  show -ε ≤ q - p
  calc
    _ ≃ -ε              := eqv_refl
    _ ≃ 0 + (-ε)        := eqv_symm add_identL
    _ ≃ (-p + p) + (-ε) := add_substL (eqv_symm add_inverseL)
    _ ≃ -p + (p + (-ε)) := add_assoc
    _ ≃ -p + (p - ε)    := add_substR (eqv_symm sub_add_neg)
    _ ≤ -p + q          := le_substR_add ‹p-ε ≤ q›
    _ ≃ q + (-p)        := add_comm
    _ ≃ q - p           := eqv_symm sub_add_neg
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_diff_lower
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
⊢ -ε ≤ q - p → p - ε ≤ q
Tactic:
intro (_ : -ε ≤ q - p)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
x✝ : -ε ≤ q - p
⊢ p - ε ≤ q
Theorem: Lean4Axiomatic.Rational.le_diff_lower
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
x✝ : -ε ≤ q - p
⊢ p - ε ≤ q
Tactic:
calc
  _ ≃ p - ε          := eqv_refl
  _ ≃ p + (-ε)       := sub_add_neg
  _ ≤ p + (q - p)    := le_substR_add ‹-ε ≤ q - p›
  _ ≃ p + (q + (-p)) := add_substR sub_add_neg
  _ ≃ p + ((-p) + q) := add_substR add_comm
  _ ≃ (p + (-p)) + q := eqv_symm add_assoc
  _ ≃ 0 + q          := add_substL add_inverseR
  _ ≃ q              := add_identL
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_diff_lower
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
⊢ p - ε ≤ q → -ε ≤ q - p
Tactic:
intro (_ : p - ε ≤ q)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
x✝ : p - ε ≤ q
⊢ -ε ≤ q - p
Theorem: Lean4Axiomatic.Rational.le_diff_lower
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
x✝ : p - ε ≤ q
⊢ -ε ≤ q - p
Tactic:
calc
  _ ≃ -ε              := eqv_refl
  _ ≃ 0 + (-ε)        := eqv_symm add_identL
  _ ≃ (-p + p) + (-ε) := add_substL (eqv_symm add_inverseL)
  _ ≃ -p + (p + (-ε)) := add_assoc
  _ ≃ -p + (p - ε)    := add_substR (eqv_symm sub_add_neg)
  _ ≤ -p + q          := le_substR_add ‹p-ε ≤ q›
  _ ≃ q + (-p)        := add_comm
  _ ≃ q - p           := eqv_symm sub_add_neg
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_diff_upper
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
⊢ q - p ≤ ε ↔ q ≤ p + ε
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
⊢ q - p ≤ ε → q ≤ p + ε

case mpr
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
⊢ q ≤ p + ε → q - p ≤ ε
Theorem: Lean4Axiomatic.Rational.le_diff_upper
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
⊢ q - p ≤ ε → q ≤ p + ε
Tactic:
case mp =>
  intro (_ : q - p ≤ ε)
  show q ≤ p + ε
  calc
    _ ≃ q              := eqv_refl
    _ ≃ q + 0          := eqv_symm add_identR
    _ ≃ q + ((-p) + p) := add_substR (eqv_symm add_inverseL)
    _ ≃ (q + (-p)) + p := eqv_symm add_assoc
    _ ≃ (q - p) + p    := add_substL (eqv_symm sub_add_neg)
    _ ≤ ε + p          := le_substL_add ‹q - p ≤ ε›
    _ ≃ p + ε          := add_comm
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_diff_upper
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
⊢ q ≤ p + ε → q - p ≤ ε
Tactic:
case mpr =>
  intro (_ : q ≤ p + ε)
  show q - p ≤ ε
  calc
    _ ≃ q - p          := eqv_refl
    _ ≃ q + (-p)       := sub_add_neg
    _ ≤ (p + ε) + (-p) := le_substL_add ‹q ≤ p+ε›
    _ ≃ (ε + p) + (-p) := add_substL add_comm
    _ ≃ ε + (p + (-p)) := add_assoc
    _ ≃ ε + 0          := add_substR add_inverseR
    _ ≃ ε              := add_identR
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_diff_upper
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
⊢ q - p ≤ ε → q ≤ p + ε
Tactic:
intro (_ : q - p ≤ ε)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
x✝ : q - p ≤ ε
⊢ q ≤ p + ε
Theorem: Lean4Axiomatic.Rational.le_diff_upper
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
x✝ : q - p ≤ ε
⊢ q ≤ p + ε
Tactic:
calc
  _ ≃ q              := eqv_refl
  _ ≃ q + 0          := eqv_symm add_identR
  _ ≃ q + ((-p) + p) := add_substR (eqv_symm add_inverseL)
  _ ≃ (q + (-p)) + p := eqv_symm add_assoc
  _ ≃ (q - p) + p    := add_substL (eqv_symm sub_add_neg)
  _ ≤ ε + p          := le_substL_add ‹q - p ≤ ε›
  _ ≃ p + ε          := add_comm
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_diff_upper
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
⊢ q ≤ p + ε → q - p ≤ ε
Tactic:
intro (_ : q ≤ p + ε)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
x✝ : q ≤ p + ε
⊢ q - p ≤ ε
Theorem: Lean4Axiomatic.Rational.le_diff_upper
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
ε p q : ℚ
x✝ : q ≤ p + ε
⊢ q - p ≤ ε
Tactic:
calc
  _ ≃ q - p          := eqv_refl
  _ ≃ q + (-p)       := sub_add_neg
  _ ≤ (p + ε) + (-p) := le_substL_add ‹q ≤ p+ε›
  _ ≃ (ε + p) + (-p) := add_substL add_comm
  _ ≃ ε + (p + (-p)) := add_assoc
  _ ≃ ε + 0          := add_substR add_inverseR
  _ ≃ ε              := add_identR
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_zero
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n : ℕ
⊢ n + 0 ≃ n
Tactic:
apply ind_on (motive := λ n => n + 0 ≃ n) n
Proof state after:
case zero
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n : ℕ
⊢ 0 + 0 ≃ 0

case step
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n : ℕ
⊢ ∀ (m : ℕ), m + 0 ≃ m → step m + 0 ≃ step m
Theorem: Lean4Axiomatic.Natural.add_zero
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n : ℕ
⊢ 0 + 0 ≃ 0
Tactic:
case zero =>
  show 0 + 0 ≃ 0
  calc
    0 + (0 : ℕ) ≃ _ := Addition.zero_add
    0           ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_zero
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n : ℕ
⊢ ∀ (m : ℕ), m + 0 ≃ m → step m + 0 ≃ step m
Tactic:
case step =>
  intro n (ih : n + 0 ≃ n)
  show step n + 0 ≃ step n
  calc
    step n + 0   ≃ _ := Addition.step_add
    step (n + 0) ≃ _ := AA.subst₁ ih
    step n       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_zero
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n : ℕ
⊢ 0 + 0 ≃ 0
Tactic:
calc
  0 + (0 : ℕ) ≃ _ := Addition.zero_add
  0           ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_zero
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n : ℕ
⊢ ∀ (m : ℕ), m + 0 ≃ m → step m + 0 ≃ step m
Tactic:
intro n (ih : n + 0 ≃ n)
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ n : ℕ
ih : n + 0 ≃ n
⊢ step n + 0 ≃ step n
Theorem: Lean4Axiomatic.Natural.add_zero
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ n : ℕ
ih : n + 0 ≃ n
⊢ step n + 0 ≃ step n
Tactic:
calc
  step n + 0   ≃ _ := Addition.step_add
  step (n + 0) ≃ _ := AA.subst₁ ih
  step n       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_swapped_zeros_eqv
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n + 0 ≃ 0 + m ↔ n ≃ m
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n + 0 ≃ 0 + m → n ≃ m

case mpr
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n ≃ m → n + 0 ≃ 0 + m
Theorem: Lean4Axiomatic.Natural.add_swapped_zeros_eqv
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n + 0 ≃ 0 + m → n ≃ m
Tactic:
case mp =>
  intro (_ : n + 0 ≃ 0 + m)
  show n ≃ m
  calc
    n     ≃ _ := Rel.symm AA.identR
    n + 0 ≃ _ := ‹n + 0 ≃ 0 + m›
    0 + m ≃ _ := AA.identL
    m     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_swapped_zeros_eqv
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n ≃ m → n + 0 ≃ 0 + m
Tactic:
case mpr =>
  intro (_ : n ≃ m)
  show n + 0 ≃ 0 + m
  calc
    n + 0 ≃ _ := AA.identR
    n     ≃ _ := ‹n ≃ m›
    m     ≃ _ := Rel.symm AA.identL
    0 + m ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_swapped_zeros_eqv
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n + 0 ≃ 0 + m → n ≃ m
Tactic:
intro (_ : n + 0 ≃ 0 + m)
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
x✝ : n + 0 ≃ 0 + m
⊢ n ≃ m
Theorem: Lean4Axiomatic.Natural.add_swapped_zeros_eqv
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
x✝ : n + 0 ≃ 0 + m
⊢ n ≃ m
Tactic:
calc
  n     ≃ _ := Rel.symm AA.identR
  n + 0 ≃ _ := ‹n + 0 ≃ 0 + m›
  0 + m ≃ _ := AA.identL
  m     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_swapped_zeros_eqv
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n ≃ m → n + 0 ≃ 0 + m
Tactic:
intro (_ : n ≃ m)
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n + 0 ≃ 0 + m
Theorem: Lean4Axiomatic.Natural.add_swapped_zeros_eqv
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n + 0 ≃ 0 + m
Tactic:
calc
  n + 0 ≃ _ := AA.identR
  n     ≃ _ := ‹n ≃ m›
  m     ≃ _ := Rel.symm AA.identL
  0 + m ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_step
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n + step m ≃ step (n + m)
Tactic:
apply ind_on (motive := λ n => n + step m ≃ step (n + m)) n
Proof state after:
case zero
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + step m ≃ step (0 + m)

case step
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 + step m ≃ step (m_1 + m) → step m_1 + step m ≃ step (step m_1 + m)
Theorem: Lean4Axiomatic.Natural.add_step
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + step m ≃ step (0 + m)
Tactic:
case zero =>
  show 0 + step m ≃ step (0 + m)
  calc
    0 + step m   ≃ _ := Addition.zero_add
    step m       ≃ _ := AA.subst₁ (Rel.symm Addition.zero_add)
    step (0 + m) ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_step
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 + step m ≃ step (m_1 + m) → step m_1 + step m ≃ step (step m_1 + m)
Tactic:
case step =>
  intro n (ih : n + step m ≃ step (n + m))
  show step n + step m ≃ step (step n + m)
  calc
    step n + step m     ≃ _ := Addition.step_add
    step (n + step m)   ≃ _ := AA.subst₁ ih
    step (step (n + m)) ≃ _ := AA.subst₁ (Rel.symm Addition.step_add)
    step (step n + m)   ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_step
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + step m ≃ step (0 + m)
Tactic:
calc
  0 + step m   ≃ _ := Addition.zero_add
  step m       ≃ _ := AA.subst₁ (Rel.symm Addition.zero_add)
  step (0 + m) ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_step
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 + step m ≃ step (m_1 + m) → step m_1 + step m ≃ step (step m_1 + m)
Tactic:
intro n (ih : n + step m ≃ step (n + m))
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
ih : n + step m ≃ step (n + m)
⊢ step n + step m ≃ step (step n + m)
Theorem: Lean4Axiomatic.Natural.add_step
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
ih : n + step m ≃ step (n + m)
⊢ step n + step m ≃ step (step n + m)
Tactic:
calc
  step n + step m     ≃ _ := Addition.step_add
  step (n + step m)   ≃ _ := AA.subst₁ ih
  step (step (n + m)) ≃ _ := AA.subst₁ (Rel.symm Addition.step_add)
  step (step n + m)   ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_comm
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n + m ≃ m + n
Tactic:
apply ind_on (motive := λ n => n + m ≃ m + n) n
Proof state after:
case zero
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + m ≃ m + 0

case step
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 + m ≃ m + m_1 → step m_1 + m ≃ m + step m_1
Theorem: Lean4Axiomatic.Natural.add_comm
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + m ≃ m + 0
Tactic:
case zero =>
  show 0 + m ≃ m + 0
  calc
    0 + m ≃ _ := Addition.zero_add
    m     ≃ _ := Rel.symm add_zero
    m + 0 ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_comm
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
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   ≃ _ := Addition.step_add
    step (n + m) ≃ _ := AA.subst₁ ih
    step (m + n) ≃ _ := Rel.symm add_step
    m + step n   ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_comm
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + m ≃ m + 0
Tactic:
calc
  0 + m ≃ _ := Addition.zero_add
  m     ≃ _ := Rel.symm add_zero
  m + 0 ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_comm
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
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 ℕ
n✝ m n : ℕ
ih : n + m ≃ m + n
⊢ step n + m ≃ m + step n
Theorem: Lean4Axiomatic.Natural.add_comm
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
ih : n + m ≃ m + n
⊢ step n + m ≃ m + step n
Tactic:
calc
  step n + m   ≃ _ := Addition.step_add
  step (n + m) ≃ _ := AA.subst₁ ih
  step (m + n) ≃ _ := Rel.symm add_step
  m + step n   ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.subst_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
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 ℕ
n₁ n₂ m : ℕ
⊢ ∀ (y : ℕ), 0 ≃ y → 0 + m ≃ y + m

case step
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
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_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
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_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
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)
    show step n₁ + m ≃ 0 + m
    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₂›
    calc
      step n₁ + m   ≃ _ := Addition.step_add
      step (n₁ + m) ≃ _ := AA.subst₁ (ih _ ‹n₁ ≃ n₂›)
      step (n₂ + m) ≃ _ := Rel.symm Addition.step_add
      step n₂ + m   ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.subst_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂ m : ℕ
⊢ ∀ (y : ℕ), 0 ≃ y → 0 + m ≃ y + m
Tactic:
intro n₂
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂✝ m n₂ : ℕ
⊢ 0 ≃ n₂ → 0 + m ≃ n₂ + m
Theorem: Lean4Axiomatic.Natural.subst_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
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 ℕ
n₁ n₂✝ m n₂ : ℕ
⊢ 0 ≃ 0 → 0 + m ≃ 0 + m

case step
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂✝ m n₂ : ℕ
⊢ ∀ (m_1 : ℕ), 0 ≃ step m_1 → 0 + m ≃ step m_1 + m
Theorem: Lean4Axiomatic.Natural.subst_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
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
Theorem: Lean4Axiomatic.Natural.subst_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂✝ m n₂ : ℕ
⊢ ∀ (m_1 : ℕ), 0 ≃ step m_1 → 0 + m ≃ step m_1 + m
Tactic:
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_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂✝ m n₂ : ℕ
⊢ 0 ≃ 0 → 0 + m ≃ 0 + m
Tactic:
intro (_ : 0 ≃ (0 : ℕ))
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂✝ m n₂ : ℕ
x✝ : 0 ≃ 0
⊢ 0 + m ≃ 0 + m
Theorem: Lean4Axiomatic.Natural.subst_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂✝ m n₂ : ℕ
x✝ : 0 ≃ 0
⊢ 0 + m ≃ 0 + m
Tactic:
exact Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.subst_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂✝ m n₂ : ℕ
⊢ ∀ (m_1 : ℕ), 0 ≃ step m_1 → 0 + m ≃ step m_1 + m
Tactic:
intro n₂ (_ : 0 ≃ step n₂)
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂✝¹ m n₂✝ n₂ : ℕ
x✝ : 0 ≃ step n₂
⊢ 0 + m ≃ step n₂ + m
Theorem: Lean4Axiomatic.Natural.subst_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂✝¹ m n₂✝ n₂ : ℕ
x✝ : 0 ≃ step n₂
⊢ 0 + m ≃ step n₂ + m
Tactic:
exact absurd (Rel.symm ‹0 ≃ step n₂›) step_neqv_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.subst_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
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:
intro n₁ (ih : ∀ y, n₁ ≃ y → n₁ + m ≃ y + m) n₂
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁✝ n₂✝ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ + m ≃ y + m
n₂ : ℕ
⊢ step n₁ ≃ n₂ → step n₁ + m ≃ n₂ + m
Theorem: Lean4Axiomatic.Natural.subst_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁✝ n₂✝ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ + m ≃ y + m
n₂ : ℕ
⊢ step n₁ ≃ n₂ → step n₁ + m ≃ n₂ + m
Tactic:
apply cases_on (motive := λ y => step n₁ ≃ y → step n₁ + m ≃ y + m)
Proof state after:
case zero
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁✝ n₂✝ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ + m ≃ y + m
n₂ : ℕ
⊢ step n₁ ≃ 0 → step n₁ + m ≃ 0 + m

case step
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁✝ n₂✝ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ + m ≃ y + m
n₂ : ℕ
⊢ ∀ (m_1 : ℕ), step n₁ ≃ step m_1 → step n₁ + m ≃ step m_1 + m
Theorem: Lean4Axiomatic.Natural.subst_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁✝ n₂✝ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ + m ≃ y + m
n₂ : ℕ
⊢ step n₁ ≃ 0 → step n₁ + m ≃ 0 + m
Tactic:
case zero =>
  intro (_ : step n₁ ≃ 0)
  show step n₁ + m ≃ 0 + m
  exact absurd ‹step n₁ ≃ 0› step_neqv_zero
Proof state after:
no goals