-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem generateMeasurableRec_induction {s : Set (Set α)} {i : Ordinal} {t : Set α}
    {p : Set α → Prop} (hs : ∀ t ∈ s, p t) (h0 : p ∅)
    (hc : ∀ u, p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ)
    (hn : ∀ f : ℕ → Set α,
      (∀ n, p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)) :
    t ∈ generateMeasurableRec s i → p t

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t✝ : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
hk : k ≤ i
t : Set α
IH : ∀ j < k, ∀ t ∈ generateMeasurableRec s j, p t
⊢ t ∈ generateMeasurableRec s k → p t

Tactic:
unfold generateMeasurableRec

Result:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t✝ : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
hk : k ≤ i
t : Set α
IH : ∀ j < k, ∀ t ∈ generateMeasurableRec s j, p t
⊢ (t ∈
      let S := ⋃ j, ⋃ (_ : j < k), generateMeasurableRec s j;
      s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ n, ↑(f n)) →
    p t

Proof state:
case inl.inl.inl
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t✝ : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
hk : k ≤ i
t : Set α
IH : ∀ j < k, ∀ t ∈ generateMeasurableRec s j, p t
ht : t ∈ s
⊢ p t

Tactic:
exact hs t ht

Result:
no goals

Proof state:
case inr.intro.a
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
hk : k ≤ i
IH : ∀ j < k, ∀ t ∈ generateMeasurableRec s j, p t
f : ℕ → ↑(⋃ j, ⋃ (_ : j < k), generateMeasurableRec s j)
n : ℕ
⊢ p ↑(f n) ∧ ∃ j < i, ↑(f n) ∈ generateMeasurableRec s j

Tactic:
obtain ⟨j, hj, hj'⟩ := mem_iUnion₂.1 (f n).2

Result:
case inr.intro.a.intro.intro
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
hk : k ≤ i
IH : ∀ j < k, ∀ t ∈ generateMeasurableRec s j, p t
f : ℕ → ↑(⋃ j, ⋃ (_ : j < k), generateMeasurableRec s j)
n : ℕ
j : Ordinal.{u_1}
hj : j < k
hj' : ↑(f n) ∈ generateMeasurableRec s j
⊢ p ↑(f n) ∧ ∃ j < i, ↑(f n) ∈ generateMeasurableRec s j

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t✝ : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
IH : ∀ y < k, y ≤ i → ∀ t ∈ generateMeasurableRec s y, p t
hk : k ≤ i
t : Set α
⊢ t ∈ generateMeasurableRec s k → p t

Tactic:
replace IH := fun j hj => IH j hj (hj.le.trans hk)

Result:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t✝ : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
hk : k ≤ i
t : Set α
IH : ∀ j < k, ∀ t ∈ generateMeasurableRec s j, p t
⊢ t ∈ generateMeasurableRec s k → p t

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k : Ordinal.{u_1}
⊢ ∀ (x : Ordinal.{u_1}),
    (∀ y < x, y ≤ i → ∀ t ∈ generateMeasurableRec s y, p t) → x ≤ i → ∀ t ∈ generateMeasurableRec s x, p t

Tactic:
intro k IH hk t

Result:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t✝ : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
IH : ∀ y < k, y ≤ i → ∀ t ∈ generateMeasurableRec s y, p t
hk : k ≤ i
t : Set α
⊢ t ∈ generateMeasurableRec s k → p t

Proof state:
case inr.intro.a
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
hk : k ≤ i
IH : ∀ j < k, ∀ t ∈ generateMeasurableRec s j, p t
f : ℕ → ↑(⋃ j, ⋃ (_ : j < k), generateMeasurableRec s j)
⊢ ∀ (n : ℕ), p ↑(f n) ∧ ∃ j < i, ↑(f n) ∈ generateMeasurableRec s j

Tactic:
intro n

Result:
case inr.intro.a
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
hk : k ≤ i
IH : ∀ j < k, ∀ t ∈ generateMeasurableRec s j, p t
f : ℕ → ↑(⋃ j, ⋃ (_ : j < k), generateMeasurableRec s j)
n : ℕ
⊢ p ↑(f n) ∧ ∃ j < i, ↑(f n) ∈ generateMeasurableRec s j