-- Mathlib/Algebra/Group/Pointwise/Set/ListOfFn.lean
theorem mem_list_prod {l : List (Set α)} {a : α} :
    a ∈ l.prod ↔
      ∃ l' : List (Σs : Set α, ↥s),
        List.prod (l'.map fun x ↦ (Sigma.snd x : α)) = a ∧ l'.map Sigma.fst = l

Proof state:
case h.mp.intro
α : Type u_1
inst✝ : Monoid α
n : ℕ
f : Fin n → Set α
fi : (i : Fin n) → ↑(f i)
⊢ ∃ x, (List.ofFn ((fun x => ↑x.snd) ∘ x)).prod = (List.ofFn fun i => ↑(fi i)).prod ∧ Sigma.fst ∘ x = f

Tactic:
exact ⟨fun i ↦ ⟨_, fi i⟩, rfl, rfl⟩

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, (List.ofFn fun i => ↑(f_1 i)).prod = a) ↔
    ∃ x, (List.ofFn ((fun x => ↑x.snd) ∘ x)).prod = a ∧ Sigma.fst ∘ x = f

Tactic:
constructor

Result:
case h.mp
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, (List.ofFn fun i => ↑(f_1 i)).prod = a) →
    ∃ x, (List.ofFn ((fun x => ↑x.snd) ∘ x)).prod = a ∧ Sigma.fst ∘ x = f

case h.mpr
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ x, (List.ofFn ((fun x => ↑x.snd) ∘ x)).prod = a ∧ Sigma.fst ∘ x = f) →
    ∃ f_1, (List.ofFn fun i => ↑(f_1 i)).prod = a

Proof state:
case h
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ a ∈ (List.ofFn f).prod ↔ ∃ l', (List.map (fun x => ↑x.snd) l').prod = a ∧ List.map Sigma.fst l' = List.ofFn f

Tactic:
simp only [mem_prod_list_ofFn, List.exists_iff_exists_tuple, List.map_ofFn, Function.comp,
  List.ofFn_inj', Sigma.mk.inj_iff, and_left_comm, exists_and_left, exists_eq_left, heq_eq_eq]

Result:
case h
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, (List.ofFn fun i => ↑(f_1 i)).prod = a) ↔
    ∃ x, (List.ofFn ((fun x => ↑x.snd) ∘ x)).prod = a ∧ Sigma.fst ∘ x = f

Proof state:
α : Type u_1
inst✝ : Monoid α
l : List (Set α)
a : α
⊢ a ∈ l.prod ↔ ∃ l', (List.map (fun x => ↑x.snd) l').prod = a ∧ List.map Sigma.fst l' = l

Tactic:
induction' l using List.ofFnRec with n f

Result:
case h
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ a ∈ (List.ofFn f).prod ↔ ∃ l', (List.map (fun x => ↑x.snd) l').prod = a ∧ List.map Sigma.fst l' = List.ofFn f

Proof state:
case h.mpr
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ x, (List.ofFn ((fun x => ↑x.snd) ∘ x)).prod = a ∧ Sigma.fst ∘ x = f) →
    ∃ f_1, (List.ofFn fun i => ↑(f_1 i)).prod = a

Tactic:
rintro ⟨fi, rfl, rfl⟩

Result:
case h.mpr.intro.intro
α : Type u_1
inst✝ : Monoid α
n : ℕ
fi : Fin n → (s : Set α) × ↑s
⊢ ∃ f, (List.ofFn fun i => ↑(f i)).prod = (List.ofFn ((fun x => ↑x.snd) ∘ fi)).prod

Proof state:
case h.mpr.intro.intro
α : Type u_1
inst✝ : Monoid α
n : ℕ
fi : Fin n → (s : Set α) × ↑s
⊢ ∃ f, (List.ofFn fun i => ↑(f i)).prod = (List.ofFn ((fun x => ↑x.snd) ∘ fi)).prod

Tactic:
exact ⟨fun i ↦ _, rfl⟩

Result:
no goals

Proof state:
case h.mp
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, (List.ofFn fun i => ↑(f_1 i)).prod = a) →
    ∃ x, (List.ofFn ((fun x => ↑x.snd) ∘ x)).prod = a ∧ Sigma.fst ∘ x = f

Tactic:
rintro ⟨fi, rfl⟩

Result:
case h.mp.intro
α : Type u_1
inst✝ : Monoid α
n : ℕ
f : Fin n → Set α
fi : (i : Fin n) → ↑(f i)
⊢ ∃ x, (List.ofFn ((fun x => ↑x.snd) ∘ x)).prod = (List.ofFn fun i => ↑(fi i)).prod ∧ Sigma.fst ∘ x = f