-- Mathlib/Combinatorics/SetFamily/Shadow.lean
lemma mem_upShadow_iterate_iff_exists_card :
    t ∈ ∂⁺^[k] 𝒜 ↔ ∃ u : Finset α, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Proof state:
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ ^[0] 𝒜 ↔ ∃ u, #u = 0 ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
simp

Result:
no goals

Proof state:
case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ (∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜) →
    ∃ a ∈ t, ∃ u, #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜

Tactic:
rintro ⟨_, ⟨a, u, hau, rfl, rfl⟩, hut, htu⟩

Result:
case succ.mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
u : Finset α
hau : a ∉ u
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ u_1, #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
hut : insert a u ⊆ t
htu : t \ insert a u ∈ 𝒜
⊢ ∃ a ∈ t, ∃ u_1, #u_1 = #u ∧ (u_1 ⊆ t ∧ a ∉ u_1) ∧ t \ insert a u_1 ∈ 𝒜

Proof state:
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
hat : a ∈ t
u : Finset α
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ u_1, #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
htu : t \ insert a u ∈ 𝒜
hut : u ⊆ t
hau : a ∉ u
⊢ ∃ u_1, (∃ a t, a ∉ t ∧ insert a t = u_1 ∧ #t = #u) ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜

Tactic:
exact ⟨_, ⟨_, _, hau, rfl, rfl⟩, insert_subset hat hut, htu⟩

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ (∃ a ∈ t, ∃ u, #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜) ↔
    ∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
constructor

Result:
case succ.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ (∃ a ∈ t, ∃ u, #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜) →
    ∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜

case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ (∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜) →
    ∃ a ∈ t, ∃ u, #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜

Proof state:
case succ.mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
u : Finset α
hau : a ∉ u
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ u_1, #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
hut : insert a u ⊆ t
htu : t \ insert a u ∈ 𝒜
⊢ ∃ a ∈ t, ∃ u_1, #u_1 = #u ∧ (u_1 ⊆ t ∧ a ∉ u_1) ∧ t \ insert a u_1 ∈ 𝒜

Tactic:
rw [insert_subset_iff] at hut

Result:
case succ.mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
u : Finset α
hau : a ∉ u
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ u_1, #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
hut : a ∈ t ∧ u ⊆ t
htu : t \ insert a u ∈ 𝒜
⊢ ∃ a ∈ t, ∃ u_1, #u_1 = #u ∧ (u_1 ⊆ t ∧ a ∉ u_1) ∧ t \ insert a u_1 ∈ 𝒜

Proof state:
case succ.mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
u : Finset α
hau : a ∉ u
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ u_1, #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
hut : a ∈ t ∧ u ⊆ t
htu : t \ insert a u ∈ 𝒜
⊢ ∃ a ∈ t, ∃ u_1, #u_1 = #u ∧ (u_1 ⊆ t ∧ a ∉ u_1) ∧ t \ insert a u_1 ∈ 𝒜

Tactic:
exact ⟨a, hut.1, _, rfl, ⟨hut.2, hau⟩, htu⟩

Result:
no goals

Proof state:
case succ.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ (∃ a ∈ t, ∃ u, #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜) →
    ∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
rintro ⟨a, hat, u, rfl, ⟨hut, hau⟩, htu⟩

Result:
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
hat : a ∈ t
u : Finset α
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ u_1, #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
htu : t \ insert a u ∈ 𝒜
hut : u ⊆ t
hau : a ∉ u
⊢ ∃ u_1, (∃ a t, a ∉ t ∧ insert a t = u_1 ∧ #t = #u) ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜

Proof state:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ t ∈ ∂⁺ ^[k + 1] 𝒜 ↔ ∃ u, #u = k + 1 ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
simp only [mem_upShadow_iff_erase_mem, ih, Function.iterate_succ_apply', card_eq_succ,
  subset_erase, erase_sdiff_comm, ← sdiff_insert]

Result:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ (∃ a ∈ t, ∃ u, #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜) ↔
    ∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜