internlm/Lean-Github huggingface dataset:
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₂ : ℕ
⊢ ∀ (m_1 : ℕ), step n₁ ≃ step m_1 → step n₁ + m ≃ step m_1 + m
Tactic:
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 n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ + m ≃ y + m
n₂ : ℕ
⊢ step n₁ ≃ 0 → step n₁ + m ≃ 0 + m
Tactic:
intro (_ : step n₁ ≃ 0)
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁✝ n₂✝ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ + m ≃ y + m
n₂ : ℕ
x✝ : step n₁ ≃ 0
⊢ step n₁ + m ≃ 0 + 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₂ : ℕ
x✝ : step n₁ ≃ 0
⊢ step n₁ + m ≃ 0 + m
Tactic:
exact absurd ‹step n₁ ≃ 0› 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₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ + m ≃ y + m
n₂ : ℕ
⊢ ∀ (m_1 : ℕ), step n₁ ≃ step m_1 → step n₁ + m ≃ step m_1 + m
Tactic:
intro n₂ (_ : step n₁ ≃ step n₂)
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁✝ n₂✝¹ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ + m ≃ y + m
n₂✝ n₂ : ℕ
x✝ : step n₁ ≃ step n₂
⊢ step n₁ + m ≃ step 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₂✝ n₂ : ℕ
x✝ : step n₁ ≃ step n₂
⊢ step n₁ + m ≃ step n₂ + m
Tactic:
have : n₁ ≃ n₂ := AA.inject ‹step n₁ ≃ step n₂›
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁✝ n₂✝¹ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ + m ≃ y + m
n₂✝ n₂ : ℕ
x✝ : step n₁ ≃ step n₂
this : n₁ ≃ n₂
⊢ step n₁ + m ≃ step 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₂✝ n₂ : ℕ
x✝ : step n₁ ≃ step n₂
this : n₁ ≃ n₂
⊢ step n₁ + m ≃ step n₂ + m
Tactic:
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.add_one_step
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n : ℕ
⊢ n + 1 ≃ step n
Tactic:
calc
  n + 1        ≃ _ := AA.substR Literals.literal_step
  n + step 0   ≃ _ := add_step
  step (n + 0) ≃ _ := AA.subst₁ add_zero
  step n       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.cancel_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m k : ℕ
⊢ n + m ≃ n + k → m ≃ k
Tactic:
apply ind_on (motive := λ n => n + m ≃ n + k → m ≃ k) n
Proof state after:
case zero
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m k : ℕ
⊢ 0 + m ≃ 0 + k → m ≃ k

case step
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m k : ℕ
⊢ ∀ (m_1 : ℕ), (m_1 + m ≃ m_1 + k → m ≃ k) → step m_1 + m ≃ step m_1 + k → m ≃ k
Theorem: Lean4Axiomatic.Natural.cancel_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m k : ℕ
⊢ 0 + m ≃ 0 + k → m ≃ k
Tactic:
case zero =>
  intro (_ : 0 + m ≃ 0 + k)
  show m ≃ k
  calc
    m     ≃ _ := Rel.symm Addition.zero_add
    0 + m ≃ _ := ‹0 + m ≃ 0 + k›
    0 + k ≃ _ := Addition.zero_add
    k     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.cancel_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m k : ℕ
⊢ 0 + m ≃ 0 + k → m ≃ k
Tactic:
intro (_ : 0 + m ≃ 0 + k)
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m k : ℕ
x✝ : 0 + m ≃ 0 + k
⊢ m ≃ k
Theorem: Lean4Axiomatic.Natural.cancel_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m k : ℕ
x✝ : 0 + m ≃ 0 + k
⊢ m ≃ k
Tactic:
calc
  m     ≃ _ := Rel.symm Addition.zero_add
  0 + m ≃ _ := ‹0 + m ≃ 0 + k›
  0 + k ≃ _ := Addition.zero_add
  k     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.cancel_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m k : ℕ
⊢ ∀ (m_1 : ℕ), (m_1 + m ≃ m_1 + k → m ≃ k) → step m_1 + m ≃ step m_1 + k → m ≃ k
Tactic:
intro n (ih : n + m ≃ n + k → m ≃ k) (_ : step n + m ≃ step n + k)
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m k n : ℕ
ih : n + m ≃ n + k → m ≃ k
x✝ : step n + m ≃ step n + k
⊢ m ≃ k
Theorem: Lean4Axiomatic.Natural.cancel_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m k n : ℕ
ih : n + m ≃ n + k → m ≃ k
x✝ : step n + m ≃ step n + k
⊢ m ≃ k
Tactic:
apply ih
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m k n : ℕ
ih : n + m ≃ n + k → m ≃ k
x✝ : step n + m ≃ step n + k
⊢ n + m ≃ n + k
Theorem: Lean4Axiomatic.Natural.cancel_add
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m k n : ℕ
ih : n + m ≃ n + k → m ≃ k
x✝ : step n + m ≃ step n + k
⊢ step (n + m) ≃ step (n + k)
Tactic:
calc
  step (n + m) ≃ _ := Rel.symm Addition.step_add
  step n + m   ≃ _ := ‹step n + m ≃ step n + k›
  step n + k   ≃ _ := Addition.step_add
  step (n + k) ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.zero_sum_split
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n + m ≃ 0 → n ≃ 0 ∧ m ≃ 0
Tactic:
apply cases_on (motive := λ n => n + m ≃ 0 → n ≃ 0 ∧ m ≃ 0) n
Proof state after:
case zero
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + m ≃ 0 → 0 ≃ 0 ∧ m ≃ 0

case step
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), step m_1 + m ≃ 0 → step m_1 ≃ 0 ∧ m ≃ 0
Theorem: Lean4Axiomatic.Natural.zero_sum_split
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + m ≃ 0 → 0 ≃ 0 ∧ m ≃ 0
Tactic:
case zero =>
  intro (_ : 0 + m ≃ 0)
  show 0 ≃ 0 ∧ m ≃ 0
  have : m ≃ 0 := Rel.trans (Rel.symm Addition.zero_add) ‹0 + m ≃ 0›
  exact And.intro Rel.refl ‹m ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.zero_sum_split
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), step m_1 + m ≃ 0 → step m_1 ≃ 0 ∧ m ≃ 0
Tactic:
case step =>
  intro n (_ : step n + m ≃ 0)
  show step n ≃ 0 ∧ m ≃ 0
  apply False.elim
  show False
  have : step (n + m) ≃ step n + m := Rel.symm Addition.step_add
  have : step (n + m) ≃ 0 :=
    Rel.trans ‹step (n + m) ≃ step n + m› ‹step n + m ≃ 0›
  exact absurd ‹step (n + m) ≃ 0› step_neqv_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.zero_sum_split
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + m ≃ 0 → 0 ≃ 0 ∧ m ≃ 0
Tactic:
intro (_ : 0 + m ≃ 0)
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
x✝ : 0 + m ≃ 0
⊢ 0 ≃ 0 ∧ m ≃ 0
Theorem: Lean4Axiomatic.Natural.zero_sum_split
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
x✝ : 0 + m ≃ 0
⊢ 0 ≃ 0 ∧ m ≃ 0
Tactic:
have : m ≃ 0 := Rel.trans (Rel.symm Addition.zero_add) ‹0 + m ≃ 0›
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
x✝ : 0 + m ≃ 0
this : m ≃ 0
⊢ 0 ≃ 0 ∧ m ≃ 0
Theorem: Lean4Axiomatic.Natural.zero_sum_split
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
x✝ : 0 + m ≃ 0
this : m ≃ 0
⊢ 0 ≃ 0 ∧ m ≃ 0
Tactic:
exact And.intro Rel.refl ‹m ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.zero_sum_split
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), step m_1 + m ≃ 0 → step m_1 ≃ 0 ∧ m ≃ 0
Tactic:
intro n (_ : step n + m ≃ 0)
Proof state after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
⊢ step n ≃ 0 ∧ m ≃ 0
Theorem: Lean4Axiomatic.Natural.zero_sum_split
Proof state before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
⊢ step n ≃ 0 ∧ m ≃ 0
Tactic:
apply False.elim
Proof state after:
case h
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Natural.zero_sum_split
Proof state before:
case h
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
⊢ False
Tactic:
have : step (n + m) ≃ step n + m := Rel.symm Addition.step_add
Proof state after:
case h
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
this : step (n + m) ≃ step n + m
⊢ False
Theorem: Lean4Axiomatic.Natural.zero_sum_split
Proof state before:
case h
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
this : step (n + m) ≃ step n + m
⊢ False
Tactic:
have : step (n + m) ≃ 0 :=
  Rel.trans ‹step (n + m) ≃ step n + m› ‹step n + m ≃ 0›
Proof state after:
case h
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
this✝ : step (n + m) ≃ step n + m
this : step (n + m) ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Natural.zero_sum_split
Proof state before:
case h
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
this✝ : step (n + m) ≃ step n + m
this : step (n + m) ≃ 0
⊢ False
Tactic:
exact absurd ‹step (n + m) ≃ 0› step_neqv_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.neg_preserves_zero
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
⊢ -p ≃ 0 ↔ p ≃ 0
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
⊢ -p ≃ 0 → p ≃ 0

case mpr
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
⊢ p ≃ 0 → -p ≃ 0
Theorem: Lean4Axiomatic.Rational.neg_preserves_zero
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
⊢ -p ≃ 0 → p ≃ 0
Tactic:
case mp =>
  intro (_ : -p ≃ 0)
  show p ≃ 0
  calc
    p      ≃ _ := eqv_symm add_identR
    p + 0  ≃ _ := add_substR (eqv_symm ‹-p ≃ 0›)
    p + -p ≃ _ := add_inverseR
    0      ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.neg_preserves_zero
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
⊢ p ≃ 0 → -p ≃ 0
Tactic:
case mpr =>
  intro (_ : p ≃ 0)
  show -p ≃ 0
  calc
    -p     ≃ _ := eqv_symm add_identL
    0 + -p ≃ _ := add_substL (eqv_symm ‹p ≃ 0›)
    p + -p ≃ _ := add_inverseR
    0      ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.neg_preserves_zero
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
⊢ -p ≃ 0 → p ≃ 0
Tactic:
intro (_ : -p ≃ 0)
Proof state after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝ : -p ≃ 0
⊢ p ≃ 0
Theorem: Lean4Axiomatic.Rational.neg_preserves_zero
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝ : -p ≃ 0
⊢ p ≃ 0
Tactic:
calc
  p      ≃ _ := eqv_symm add_identR
  p + 0  ≃ _ := add_substR (eqv_symm ‹-p ≃ 0›)
  p + -p ≃ _ := add_inverseR
  0      ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.neg_preserves_zero
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
⊢ p ≃ 0 → -p ≃ 0
Tactic:
intro (_ : p ≃ 0)
Proof state after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝ : p ≃ 0
⊢ -p ≃ 0
Theorem: Lean4Axiomatic.Rational.neg_preserves_zero
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝ : p ≃ 0
⊢ -p ≃ 0
Tactic:
calc
  -p     ≃ _ := eqv_symm add_identL
  0 + -p ≃ _ := add_substL (eqv_symm ‹p ≃ 0›)
  p + -p ≃ _ := add_inverseR
  0      ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.neg_scompatL_mul
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ -(p * q) ≃ -p * q
Tactic:
have : 0 ≃ -p + p := eqv_symm add_inverseL
Proof state after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
this : 0 ≃ -p + p
⊢ -(p * q) ≃ -p * q
Theorem: Lean4Axiomatic.Rational.neg_scompatL_mul
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
this : 0 ≃ -p + p
⊢ -(p * q) ≃ -p * q
Tactic:
calc
  -(p * q)                      ≃ _ := eqv_symm add_identL
  0 + -(p * q)                  ≃ _ := add_substL (eqv_symm mul_absorbL)
  0 * q + -(p * q)              ≃ _ := add_substL (mul_substL ‹0 ≃ -p + p›)
  (-p + p) * q + -(p * q)       ≃ _ := add_substL mul_distribR
  (-p * q + p * q) + -(p * q)   ≃ _ := add_assoc
  (-p) * q + (p * q + -(p * q)) ≃ _ := add_substR add_inverseR
  (-p) * q + 0                  ≃ _ := add_identR
  (-p) * q                      ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sqrt1_nonzero
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
⊢ Sqrt1 p → p ≄ 0
Tactic:
intro (_ : Sqrt1 p) (_ : p ≃ 0)
Proof state after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝¹ : Sqrt1 p
x✝ : p ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.sqrt1_nonzero
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝¹ : Sqrt1 p
x✝ : p ≃ 0
⊢ False
Tactic:
have : (1 : ℚ) ≃ 0 := calc
  (1 : ℚ) ≃ _ := eqv_symm ‹Sqrt1 p›.elim
  p * p   ≃ _ := mul_substL ‹p ≃ 0›
  0 * p   ≃ _ := mul_absorbL
  0       ≃ _ := eqv_refl
Proof state after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝¹ : Sqrt1 p
x✝ : p ≃ 0
this : 1 ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.sqrt1_nonzero
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝¹ : Sqrt1 p
x✝ : p ≃ 0
this : 1 ≃ 0
⊢ False
Tactic:
have : (1 : ℚ) ≄ 0 := nonzero_one
Proof state after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝¹ : Sqrt1 p
x✝ : p ≃ 0
this✝ : 1 ≃ 0
this : 1 ≄ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.sqrt1_nonzero
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝¹ : Sqrt1 p
x✝ : p ≃ 0
this✝ : 1 ≃ 0
this : 1 ≄ 0
⊢ False
Tactic:
exact absurd ‹(1 : ℚ) ≃ 0› ‹(1 : ℚ) ≄ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sub_substL
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p₁ p₂ q : ℚ
⊢ p₁ ≃ p₂ → p₁ - q ≃ p₂ - q
Tactic:
intro (_ : p₁ ≃ p₂)
Proof state after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p₁ p₂ q : ℚ
x✝ : p₁ ≃ p₂
⊢ p₁ - q ≃ p₂ - q
Theorem: Lean4Axiomatic.Rational.sub_substL
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p₁ p₂ q : ℚ
x✝ : p₁ ≃ p₂
⊢ p₁ - q ≃ p₂ - q
Tactic:
calc
  p₁ - q  ≃ _ := sub_add_neg
  p₁ + -q ≃ _ := add_substL ‹p₁ ≃ p₂›
  p₂ + -q ≃ _ := eqv_symm sub_add_neg
  p₂ - q  ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sub_substR
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p₁ p₂ q : ℚ
⊢ p₁ ≃ p₂ → q - p₁ ≃ q - p₂
Tactic:
intro (_ : p₁ ≃ p₂)
Proof state after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p₁ p₂ q : ℚ
x✝ : p₁ ≃ p₂
⊢ q - p₁ ≃ q - p₂
Theorem: Lean4Axiomatic.Rational.sub_substR
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p₁ p₂ q : ℚ
x✝ : p₁ ≃ p₂
⊢ q - p₁ ≃ q - p₂
Tactic:
calc
  q - p₁  ≃ _ := sub_add_neg
  q + -p₁ ≃ _ := add_substR (neg_subst ‹p₁ ≃ p₂›)
  q + -p₂ ≃ _ := eqv_symm sub_add_neg
  q - p₂  ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sub_eqv_zero_iff_eqv
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p - q ≃ 0 ↔ p ≃ q
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p - q ≃ 0 → p ≃ q

case mpr
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p ≃ q → p - q ≃ 0
Theorem: Lean4Axiomatic.Rational.sub_eqv_zero_iff_eqv
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p - q ≃ 0 → p ≃ q
Tactic:
case mp =>
  intro (_ : p - q ≃ 0)
  show p ≃ q
  calc
    p            ≃ _ := eqv_symm add_identR
    p + 0        ≃ _ := add_substR (eqv_symm add_inverseL)
    p + (-q + q) ≃ _ := eqv_symm add_assoc
    (p + -q) + q ≃ _ := add_substL (eqv_symm sub_add_neg)
    (p - q) + q  ≃ _ := add_substL ‹p - q ≃ 0›
    0 + q        ≃ _ := add_identL
    q            ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sub_eqv_zero_iff_eqv
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p ≃ q → p - q ≃ 0
Tactic:
case mpr =>
  intro (_ : p ≃ q)
  show p - q ≃ 0
  calc
    p - q  ≃ _ := sub_add_neg
    p + -q ≃ _ := add_substL ‹p ≃ q›
    q + -q ≃ _ := add_inverseR
    0      ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sub_eqv_zero_iff_eqv
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p - q ≃ 0 → p ≃ q
Tactic:
intro (_ : p - q ≃ 0)
Proof state after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
x✝ : p - q ≃ 0
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.sub_eqv_zero_iff_eqv
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
x✝ : p - q ≃ 0
⊢ p ≃ q
Tactic:
calc
  p            ≃ _ := eqv_symm add_identR
  p + 0        ≃ _ := add_substR (eqv_symm add_inverseL)
  p + (-q + q) ≃ _ := eqv_symm add_assoc
  (p + -q) + q ≃ _ := add_substL (eqv_symm sub_add_neg)
  (p - q) + q  ≃ _ := add_substL ‹p - q ≃ 0›
  0 + q        ≃ _ := add_identL
  q            ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.sub_eqv_zero_iff_eqv
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p ≃ q → p - q ≃ 0
Tactic:
intro (_ : p ≃ q)
Proof state after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
x✝ : p ≃ q
⊢ p - q ≃ 0
Theorem: Lean4Axiomatic.Rational.sub_eqv_zero_iff_eqv
Proof state before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
x✝ : p ≃ q
⊢ p - q ≃ 0
Tactic:
calc
  p - q  ≃ _ := sub_add_neg
  p + -q ≃ _ := add_substL ‹p ≃ q›
  q + -q ≃ _ := add_inverseR
  0      ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_subst
Proof state before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
p₁ p₂ : Fraction ℤ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
⊢ p₁ ≃ p₂ → p₁⁻¹ ≃ p₂⁻¹
Tactic:
revert p₁
Proof state after:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
p₂ : Fraction ℤ
inst✝ : AP (p₂ ≄ 0)
⊢ ∀ {p₁ : Fraction ℤ} [inst : AP (p₁ ≄ 0)], p₁ ≃ p₂ → p₁⁻¹ ≃ p₂⁻¹
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_subst
Proof state before:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
p₂ : Fraction ℤ
inst✝ : AP (p₂ ≄ 0)
⊢ ∀ {p₁ : Fraction ℤ} [inst : AP (p₁ ≄ 0)], p₁ ≃ p₂ → p₁⁻¹ ≃ p₂⁻¹
Tactic:
intro (a//b)
Proof state after:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
p₂ : Fraction ℤ
inst✝ : AP (p₂ ≄ 0)
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ [inst : AP (a//b ≄ 0)], a//b ≃ p₂ → (a//b)⁻¹ ≃ p₂⁻¹