Theorem: every_nonzero_nat_successor (meetings/ex5.lean)

State before:
n : ↑N0
⊢ n ≠ z → ∃ m, n = S m
Tactic:
intro hne
State after:
n : ↑N0
hne : n ≠ z
⊢ ∃ m, n = S m

State before:
n : ↑N0
hne : n ≠ z
⊢ ∃ m, n = S m
Tactic:
let A := {n : N0 | n ≠ z → ∃ m : N0, n = S m}
State after:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
⊢ ∃ m, n = S m

State before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
⊢ ∃ m, n = S m
Tactic:
have hzmem : z ∈ A := by
  simp only [ne_eq, Subtype.exists, Set.mem_setOf_eq, not_true_eq_false, IsEmpty.forall_iff]
State after:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
⊢ ∃ m, n = S m

State before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
⊢ ∃ m, n = S m
Tactic:
have hind : (∀ n : N0, n ∈ A → (S n) ∈ A) := by
  intros n _
  simp only [ne_eq, Subtype.exists, Set.mem_setOf_eq]
  intro _
  use n
  simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const]
State after:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ ∃ m, n = S m

State before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ ∃ m, n = S m
Tactic:
have heq := p3 A ⟨hzmem, hind⟩
State after:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ ∃ m, n = S m

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

State before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  ∀ (x : α),
    (∃ (x_1 : x ∈ N0),
        ¬{ val := x, property := (_ : x ∈ N0) } = z →
          ∃ a, ∃ (b : a ∈ N0), { val := x, property := (_ : x ∈ N0) } = S { val := a, property := b }) ↔
      x ∈ N0
⊢ ∃ m, n = S m
Tactic:
specialize heq n
State after:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x : ↑n ∈ N0),
      ¬{ val := ↑n, property := (_ : ↑n ∈ N0) } = z →
        ∃ a, ∃ (b : a ∈ N0), { val := ↑n, property := (_ : ↑n ∈ N0) } = S { val := a, property := b }) ↔
    ↑n ∈ N0
⊢ ∃ m, n = S m

State before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x : ↑n ∈ N0),
      ¬{ val := ↑n, property := (_ : ↑n ∈ N0) } = z →
        ∃ a, ∃ (b : a ∈ N0), { val := ↑n, property := (_ : ↑n ∈ N0) } = S { val := a, property := b }) ↔
    ↑n ∈ N0
⊢ ∃ m, n = S m
Tactic:
simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const, iff_true] at heq
State after:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : ¬n = z → ∃ a, ∃ (h : a ∈ N0), n = S { val := a, property := (_ : a ∈ N0) }
⊢ ∃ m, n = S m

State before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : ¬n = z → ∃ a, ∃ (h : a ∈ N0), n = S { val := a, property := (_ : a ∈ N0) }
⊢ ∃ m, n = S m
Tactic:
rcases heq hne with ⟨a, ⟨h, heq⟩⟩
State after:
case intro.intro
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq✝ : ¬n = z → ∃ a, ∃ (h : a ∈ N0), n = S { val := a, property := (_ : a ∈ N0) }
a : α
h : a ∈ N0
heq : n = S { val := a, property := (_ : a ∈ N0) }
⊢ ∃ m, n = S m

State before:
case intro.intro
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq✝ : ¬n = z → ∃ a, ∃ (h : a ∈ N0), n = S { val := a, property := (_ : a ∈ N0) }
a : α
h : a ∈ N0
heq : n = S { val := a, property := (_ : a ∈ N0) }
⊢ ∃ m, n = S m
Tactic:
use { val := a, property := h }
State after:
no goals

State before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
⊢ z ∈ A
Tactic:
simp only [ne_eq, Subtype.exists, Set.mem_setOf_eq, not_true_eq_false, IsEmpty.forall_iff]
State after:
no goals

State before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
⊢ ∀ n ∈ A, S n ∈ A
Tactic:
intros n _
State after:
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝ : n ∈ A
⊢ S n ∈ A

State before:
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝ : n ∈ A
⊢ S n ∈ A
Tactic:
simp only [ne_eq, Subtype.exists, Set.mem_setOf_eq]
State after:
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝ : n ∈ A
⊢ ¬S n = z → ∃ a, ∃ (b : a ∈ N0), S n = S { val := a, property := b }

State before:
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝ : n ∈ A
⊢ ¬S n = z → ∃ a, ∃ (b : a ∈ N0), S n = S { val := a, property := b }
Tactic:
intro _
State after:
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝¹ : n ∈ A
a✝ : ¬S n = z
⊢ ∃ a, ∃ (b : a ∈ N0), S n = S { val := a, property := b }

State before:
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝¹ : n ∈ A
a✝ : ¬S n = z
⊢ ∃ a, ∃ (b : a ∈ N0), S n = S { val := a, property := b }
Tactic:
use n
State after:
case h
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝¹ : n ∈ A
a✝ : ¬S n = z
⊢ ∃ (b : ↑n ∈ N0), S n = S { val := ↑n, property := b }

State before:
case h
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝¹ : n ∈ A
a✝ : ¬S n = z
⊢ ∃ (b : ↑n ∈ N0), S n = S { val := ↑n, property := b }
Tactic:
simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const]
State after:
no goals