case h
F : Type ?u.8458
α : Type u_1
β : Type ?u.8464
γ : Type ?u.8467
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ a ∈ List.prod (List.ofFn f) ↔
    ∃ l', List.prod (List.map (fun x => ↑x.snd) l') = a ∧ List.map Sigma.fst l' = List.ofFn f
F : Type ?u.8458
α : Type u_1
β : Type ?u.8464
γ : Type ?u.8467
inst✝ : Monoid α
s t : Set α
a✝ : α
m n : ℕ
l : List (Set α)
a : α
⊢ a ∈ List.prod l ↔ ∃ l', List.prod (List.map (fun x => ↑x.snd) l') = a ∧ List.map Sigma.fst l' = l
induction' l using List.ofFnRec with n f
case h
F : Type ?u.8458
α : Type u_1
β : Type ?u.8464
γ : Type ?u.8467
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, List.prod (List.ofFn fun i => ↑(f_1 i)) = a) ↔
    ∃ x, List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = a ∧ (fun x_1 => (x x_1).fst) = f
case h
F : Type ?u.8458
α : Type u_1
β : Type ?u.8464
γ : Type ?u.8467
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ a ∈ List.prod (List.ofFn f) ↔
    ∃ l', List.prod (List.map (fun x => ↑x.snd) l') = a ∧ List.map Sigma.fst l' = List.ofFn f
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]
case h.mp
F : Type ?u.8458
α : Type u_1
β : Type ?u.8464
γ : Type ?u.8467
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, List.prod (List.ofFn fun i => ↑(f_1 i)) = a) →
    ∃ x, List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = a ∧ (fun x_1 => (x x_1).fst) = f

case h.mpr
F : Type ?u.8458
α : Type u_1
β : Type ?u.8464
γ : Type ?u.8467
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ x, List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = a ∧ (fun x_1 => (x x_1).fst) = f) →
    ∃ f_1, List.prod (List.ofFn fun i => ↑(f_1 i)) = a
case h
F : Type ?u.8458
α : Type u_1
β : Type ?u.8464
γ : Type ?u.8467
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, List.prod (List.ofFn fun i => ↑(f_1 i)) = a) ↔
    ∃ x, List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = a ∧ (fun x_1 => (x x_1).fst) = f
constructor
case h.mp.intro
F : Type ?u.8458
α : Type u_1
β : Type ?u.8464
γ : Type ?u.8467
inst✝ : Monoid α
s t : Set α
a : α
m n✝ n : ℕ
f : Fin n → Set α
fi : (i : Fin n) → ↑(f i)
⊢ ∃ x,
    List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = List.prod (List.ofFn fun i => ↑(fi i)) ∧
      (fun x_1 => (x x_1).fst) = f
case h.mp
F : Type ?u.8458
α : Type u_1
β : Type ?u.8464
γ : Type ?u.8467
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, List.prod (List.ofFn fun i => ↑(f_1 i)) = a) →
    ∃ x, List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = a ∧ (fun x_1 => (x x_1).fst) = f
rintro ⟨fi, rfl⟩
no goals
case h.mp.intro
F : Type ?u.8458
α : Type u_1
β : Type ?u.8464
γ : Type ?u.8467
inst✝ : Monoid α
s t : Set α
a : α
m n✝ n : ℕ
f : Fin n → Set α
fi : (i : Fin n) → ↑(f i)
⊢ ∃ x,
    List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = List.prod (List.ofFn fun i => ↑(fi i)) ∧
      (fun x_1 => (x x_1).fst) = f
exact ⟨fun i ↦ ⟨_, fi i⟩, rfl, rfl⟩
case h.mpr.intro.intro
F : Type ?u.8458
α : Type u_1
β : Type ?u.8464
γ : Type ?u.8467
inst✝ : Monoid α
s t : Set α
a : α
m n✝ n : ℕ
fi : Fin n → (s : Set α) × ↑s
⊢ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = List.prod (List.ofFn fun x => ↑(fi x).snd)
case h.mpr
F : Type ?u.8458
α : Type u_1
β : Type ?u.8464
γ : Type ?u.8467
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ x, List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = a ∧ (fun x_1 => (x x_1).fst) = f) →
    ∃ f_1, List.prod (List.ofFn fun i => ↑(f_1 i)) = a
rintro ⟨fi, rfl, rfl⟩
no goals
case h.mpr.intro.intro
F : Type ?u.8458
α : Type u_1
β : Type ?u.8464
γ : Type ?u.8467
inst✝ : Monoid α
s t : Set α
a : α
m n✝ n : ℕ
fi : Fin n → (s : Set α) × ↑s
⊢ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = List.prod (List.ofFn fun x => ↑(fi x).snd)
exact ⟨fun i ↦ _, rfl⟩