-- Mathlib/Order/Filter/Cofinite.lean
theorem map_piMap_pi {α β : ι → Type*} {f : ∀ i, α i → β i}
    (hf : ∀ᶠ i in cofinite, Surjective (f i)) (l : ∀ i, Filter (α i)) :
    map (Pi.map f) (pi l) = pi fun i ↦ map (f i) (l i)

Proof state:
case mk.intro
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ (Pi.map f '' (I, s).1.pi fun i => id ((I, s).2 i)) ∈ pi fun i => map (f i) (l i)

Tactic:
rw [← univ_pi_piecewise_univ, piMap_image_univ_pi]

Result:
case mk.intro
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ (univ.pi fun i => f i '' (I, s).1.piecewise (fun i => id ((I, s).2 i)) (fun x => univ) i) ∈
    pi fun i => map (f i) (l i)

Proof state:
case pos
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hi : i ∈ I
⊢ f i '' (I, s).1.piecewise (fun i => id ((I, s).2 i)) (fun x => univ) i ∈ map (f i) (l i)

Tactic:
simpa [hi] using image_mem_map (hs i hi)

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
⊢ map (Pi.map f) (pi l) = pi fun i => map (f i) (l i)

Tactic:
refine le_antisymm (tendsto_piMap_pi fun _ ↦ tendsto_map) ?_

Result:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
⊢ (pi fun i => map (f i) (l i)) ≤ map (Pi.map f) (pi l)

Proof state:
case h
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hsurj : Surjective (f i)
hiI : i ∉ I
⊢ f i '' I.piecewise (fun i => id (s i)) (fun x => univ) i = univ

Tactic:
simp [hiI, hsurj.range_eq]

Result:
no goals

Proof state:
case mk.intro
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ (univ.pi fun i => f i '' (I, s).1.piecewise (fun i => id ((I, s).2 i)) (fun x => univ) i) ∈
    pi fun i => map (f i) (l i)

Tactic:
refine univ_pi_mem_pi (fun i ↦ ?_) ?_

Result:
case mk.intro.refine_1
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
⊢ f i '' (I, s).1.piecewise (fun i => id ((I, s).2 i)) (fun x => univ) i ∈ map (f i) (l i)

case mk.intro.refine_2
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ ∀ᶠ (i : ι) in cofinite, f i '' (I, s).1.piecewise (fun i => id ((I, s).2 i)) (fun x => univ) i = univ

Proof state:
case neg
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hi : i ∉ I
⊢ f i '' (I, s).1.piecewise (fun i => id ((I, s).2 i)) (fun x => univ) i ∈ map (f i) (l i)

Tactic:
simp [hi]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
⊢ ∀ (i' : Set ι × ((i : ι) → Set (α i))),
    (i'.1.Finite ∧ ∀ i ∈ i'.1, i'.2 i ∈ l i) → (Pi.map f '' i'.1.pi fun i => id (i'.2 i)) ∈ pi fun i => map (f i) (l i)

Tactic:
rintro ⟨I, s⟩ ⟨hI : I.Finite, hs : ∀ i ∈ I, s i ∈ l i⟩

Result:
case mk.intro
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ (Pi.map f '' (I, s).1.pi fun i => id ((I, s).2 i)) ∈ pi fun i => map (f i) (l i)

Proof state:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
⊢ (pi fun i => map (f i) (l i)) ≤ map (Pi.map f) (pi l)

Tactic:
refine ((hasBasis_pi fun i ↦ (l i).basis_sets).map _).ge_iff.2 ?_

Result:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
⊢ ∀ (i' : Set ι × ((i : ι) → Set (α i))),
    (i'.1.Finite ∧ ∀ i ∈ i'.1, i'.2 i ∈ l i) → (Pi.map f '' i'.1.pi fun i => id (i'.2 i)) ∈ pi fun i => map (f i) (l i)

Proof state:
case mk.intro.refine_2
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ ∀ᶠ (i : ι) in cofinite, f i '' (I, s).1.piecewise (fun i => id ((I, s).2 i)) (fun x => univ) i = univ

Tactic:
filter_upwards [hf, hI.compl_mem_cofinite] with i hsurj (hiI : i ∉ I)

Result:
case h
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hsurj : Surjective (f i)
hiI : i ∉ I
⊢ f i '' I.piecewise (fun i => id (s i)) (fun x => univ) i = univ

Proof state:
case mk.intro.refine_1
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
⊢ f i '' (I, s).1.piecewise (fun i => id ((I, s).2 i)) (fun x => univ) i ∈ map (f i) (l i)

Tactic:
by_cases hi : i ∈ I

Result:
case pos
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hi : i ∈ I
⊢ f i '' (I, s).1.piecewise (fun i => id ((I, s).2 i)) (fun x => univ) i ∈ map (f i) (l i)

case neg
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hi : i ∉ I
⊢ f i '' (I, s).1.piecewise (fun i => id ((I, s).2 i)) (fun x => univ) i ∈ map (f i) (l i)