Theorem: succ_plus_eq_succ_plus (meetings/ex5.lean)

State before:
x y : ↑N0
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
let A := {y : N0 | plus ((S x), y) = S (plus (x, y))}
State after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
⊢ plus (S x, y) = S (plus (x, y))

State before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
have hzmem : z ∈ A := by
  simp only [Set.mem_setOf_eq]
  simp [zplus]
State after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
⊢ plus (S x, y) = S (plus (x, y))

State before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
have hind : (∀ n : N0, n ∈ A → (S n) ∈ A) := by
  intros n hel
  simp only [Set.mem_setOf_eq]
  simp only [Set.mem_setOf_eq] at hel
  rw [splus, hel, ←splus]
State after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ plus (S x, y) = S (plus (x, y))

State before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
have heq := p3 A ⟨hzmem, hind⟩
State after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ plus (S x, y) = S (plus (x, y))

State before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
simp [A, Set.ext_iff] at heq
State after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  ∀ (x_1 : α),
    (∃ (x_2 : x_1 ∈ N0),
        plus (S x, { val := x_1, property := (_ : x_1 ∈ N0) }) =
          S (plus (x, { val := x_1, property := (_ : x_1 ∈ N0) }))) ↔
      x_1 ∈ N0
⊢ plus (S x, y) = S (plus (x, y))

State before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  ∀ (x_1 : α),
    (∃ (x_2 : x_1 ∈ N0),
        plus (S x, { val := x_1, property := (_ : x_1 ∈ N0) }) =
          S (plus (x, { val := x_1, property := (_ : x_1 ∈ N0) }))) ↔
      x_1 ∈ N0
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
specialize heq y
State after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x_1 : ↑y ∈ N0),
      plus (S x, { val := ↑y, property := (_ : ↑y ∈ N0) }) = S (plus (x, { val := ↑y, property := (_ : ↑y ∈ N0) }))) ↔
    ↑y ∈ N0
⊢ plus (S x, y) = S (plus (x, y))

State before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x_1 : ↑y ∈ N0),
      plus (S x, { val := ↑y, property := (_ : ↑y ∈ N0) }) = S (plus (x, { val := ↑y, property := (_ : ↑y ∈ N0) }))) ↔
    ↑y ∈ N0
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const, iff_true] at heq
State after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : plus (S x, y) = S (plus (x, y))
⊢ plus (S x, y) = S (plus (x, y))

State before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : plus (S x, y) = S (plus (x, y))
⊢ plus (S x, y) = S (plus (x, y))
Tactic:
exact heq
State after:
no goals

State before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
⊢ z ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
State after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
⊢ plus (S x, z) = S (plus (x, z))

State before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
⊢ plus (S x, z) = S (plus (x, z))
Tactic:
simp [zplus]
State after:
no goals

State before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
⊢ ∀ n ∈ A, S n ∈ A
Tactic:
intros n hel
State after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A

State before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
State after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ plus (S x, S n) = S (plus (x, S n))

State before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ plus (S x, S n) = S (plus (x, S n))
Tactic:
simp only [Set.mem_setOf_eq] at hel
State after:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : plus (S x, n) = S (plus (x, n))
⊢ plus (S x, S n) = S (plus (x, S n))

State before:
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : plus (S x, n) = S (plus (x, n))
⊢ plus (S x, S n) = S (plus (x, S n))
Tactic:
rw [splus, hel, ←splus]
State after:
no goals