Theorem: generic_recursor (meetings/ex6.lean)

State before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
⊢ motive x
Tactic:
let A := {x : N0 | motive x}
State after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
⊢ motive x

State before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
⊢ motive x
Tactic:
have hzmem : z ∈ A := by
  simp only [Set.mem_setOf_eq]
  exact hz
State after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
⊢ motive x

State before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
⊢ motive x
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
  specialize hs n
  exact hs hel
State after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ motive x

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

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

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

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

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

State before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
⊢ z ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
State after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
⊢ motive z

State before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
⊢ motive z
Tactic:
exact hz
State after:
no goals

State before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
⊢ ∀ n ∈ A, S n ∈ A
Tactic:
intros n hel
State after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A

State before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
State after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ motive (S n)

State before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ motive (S n)
Tactic:
simp only [Set.mem_setOf_eq] at hel
State after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : motive n
⊢ motive (S n)

State before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : motive n
⊢ motive (S n)
Tactic:
specialize hs n
State after:
motive : ↑N0 → Prop
hz : motive z
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : motive n
hs : motive n → motive (S n)
⊢ motive (S n)

State before:
motive : ↑N0 → Prop
hz : motive z
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : motive n
hs : motive n → motive (S n)
⊢ motive (S n)
Tactic:
exact hs hel
State after:
no goals