Theorem: Lean4Axiomatic.Natural.subst_add (Lean4Axiomatic/Natural/Addition.lean)

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₁
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

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
State after:
no goals

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
State after:
no goals

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂ m : ℕ
⊢ ∀ (y : ℕ), 0 ≃ y → 0 + m ≃ y + m
Tactic:
intro n₂
State after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂✝ m n₂ : ℕ
⊢ 0 ≃ n₂ → 0 + m ≃ n₂ + m

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)
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

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
State after:
no goals

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
State after:
no goals

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂✝ m n₂ : ℕ
⊢ 0 ≃ 0 → 0 + m ≃ 0 + m
Tactic:
intro (_ : 0 ≃ (0 : ℕ))
State after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂✝ m n₂ : ℕ
x✝ : 0 ≃ 0
⊢ 0 + m ≃ 0 + m

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂✝ m n₂ : ℕ
x✝ : 0 ≃ 0
⊢ 0 + m ≃ 0 + m
Tactic:
exact Rel.refl
State after:
no goals

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₂)
State after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂✝¹ m n₂✝ n₂ : ℕ
x✝ : 0 ≃ step n₂
⊢ 0 + m ≃ step n₂ + m

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
State after:
no goals

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₂
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

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)
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

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
State after:
no goals

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
State after:
no goals

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)
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

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
State after:
no goals

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₂)
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

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₂›
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

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
State after:
no goals