awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : Decidable (s.pi (α := α) t).Nonempty
hi : ¬i ∈ s
h :
  ∀ (xᵢ : α i),
    xᵢ ∈ eval (β := α) i '' s.pi (α := α) t ↔
      Membership.mem (γ := Set (α i)) (if (s.pi (α := α) t).Nonempty then univ else ∅) xᵢ
h₁ :
  ∀ (xᵢ : α i),
    (∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) ↔
      ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i
h₂ :
  ∀ (xᵢ : α i),
    (∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) →
      ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i
h₃ h₄ :
  ∀ (xᵢ : α i),
    (∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i) →
      ∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ
⊢ eval (β := α) i '' s.pi (α := α) t = if (s.pi (α := α) t).Nonempty then univ else ∅

Tactic:
classical
  ext xᵢ
  simp only [eval, mem_image, mem_pi, Set.Nonempty, mem_ite_empty_right, mem_univ, and_true]
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨x, hx⟩
  · rintro ⟨x, hx⟩
    refine ⟨Function.update x i xᵢ, ?_⟩
    simpa +contextual [(ne_of_mem_of_not_mem · hi)]

Premises used: and_true, Set.mem_image, Set.mem_ite_empty_right, Set.mem_pi, Function.eval, ne_of_mem_of_not_mem, Set.Nonempty, Set.mem_univ, rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
i : ι
ht : (pi (α := α) univ t).Nonempty
⊢ (fun (f : (i : ι) → α i) ↦ f i) '' pi (α := α) univ t = t i

Tactic:
eval_image_pi (mem_univ i) ht

Premises used: Set.mem_univ, Set.eval_image_pi
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
I : Set ι
f : (i : ι) → α i → β i
s : (i : ι) → Set (α i)
t : (i : ι) → Set (β i)
h : ∀ (i : ι), i ∈ I → MapsTo (f i) (s i) (t i)
⊢ MapsTo (Pi.map (α := α) (β := β) f) (I.pi (α := α) s) (I.pi (α := β) t)

Tactic:
fun _x hx i hi => h i hi (hx i hi)

Premises used: Set.Mem, setOf, Pi.map, Set.MapsTo, Set.pi
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
t : (i : ι) → Set (α i)
⊢ Pi.map (α := α) (β := β) f '' s.pi (α := α) t ⊆ s.pi (α := β) fun (i : ι) ↦ f i '' t i

Tactic:
image_subset_iff.2 <| piMap_mapsTo_pi fun _ _ => mapsTo_image _ _

Premises used: Set.piMap_mapsTo_pi, Iff.mpr, Set.mapsTo_image, Set.image_subset_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
⊢ Pi.map (α := α) (β := β) f '' s.pi (α := α) t = s.pi (α := β) fun (i : ι) ↦ f i '' t i

Tactic:
Subset.antisymm (piMap_image_pi_subset _) fun b hb => ?_

Premises used: Set.Subset.antisymm, Set.piMap_image_pi_subset
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
refine :
  ∀ (b : (i : ι) → β i) (hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b),
    b ∈ Pi.map (α := α) (β := β) f '' s.pi (α := α) t
⊢ Pi.map (α := α) (β := β) f '' s.pi (α := α) t = s.pi (α := β) fun (i : ι) ↦ f i '' t i

Tactic:
refine Subset.antisymm (piMap_image_pi_subset _) fun b hb => ?_

Premises used: Set.Subset.antisymm, Set.piMap_image_pi_subset
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b
i : ι
hi : i ∈ s
⊢ ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)

Tactic:
(hb i hi).imp fun a ⟨hat, hab⟩ ↦ ⟨hab, fun _ ↦ hat⟩

Premises used: Exists.imp
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b
i : ι
hi : i ∈ s
⊢ ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)

Tactic:
exact (hb i hi).imp fun a ⟨hat, hab⟩ ↦ ⟨hab, fun _ ↦ hat⟩

Premises used: Exists.imp
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b
i : ι
hi : ¬i ∈ s
⊢ ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)

Tactic:
(hf i hi (b i)).imp fun a ha ↦ ⟨ha, (absurd · hi)⟩

Premises used: Exists.imp, absurd, And.intro
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b
i : ι
hi : ¬i ∈ s
⊢ ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)

Tactic:
exact (hf i hi (b i)).imp fun a ha ↦ ⟨ha, (absurd · hi)⟩

Premises used: Exists.imp
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b
i : ι
if : ∀ (hi : i ∈ s), ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)
if₁ : ∀ (hi : ¬i ∈ s), ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)
if₂ : ∀ (hi : i ∈ s), ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)
if₃ if₄ : ∀ (hi : ¬i ∈ s), ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)
⊢ ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)

Tactic:
if hi : i ∈ s then
      exact (hb i hi).imp fun a ⟨hat, hab⟩ ↦ ⟨hab, fun _ ↦ hat⟩
    else
      exact (hf i hi (b i)).imp fun a ha ↦ ⟨ha, (absurd · hi)⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b
⊢ ∀ (i : ι), ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)

Tactic:
have (i : ι) : ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i) := by
    if hi : i ∈ s then
      exact (hb i hi).imp fun a ⟨hat, hab⟩ ↦ ⟨hab, fun _ ↦ hat⟩
    else
      exact (hf i hi (b i)).imp fun a ha ↦ ⟨ha, (absurd · hi)⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b
this : ∀ (i : ι), ∃ (a : α i), f i a = b i ∧ (i ∈ s → a ∈ t i)
choose :
  ∀ (a : (i : ι) → α i) (hab : ∀ (i : ι), f i (a i) = b i) (hat : ∀ (i : ι), i ∈ s → a i ∈ t i),
    b ∈ Pi.map (α := α) (β := β) f '' s.pi (α := α) t
⊢ b ∈ Pi.map (α := α) (β := β) f '' s.pi (α := α) t

Tactic:
choose a hab hat using this
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b
a : (i : ι) → α i
hab : ∀ (i : ι), f i (a i) = b i
hat : ∀ (i : ι), i ∈ s → a i ∈ t i
⊢ b ∈ Pi.map (α := α) (β := β) f '' s.pi (α := α) t

Tactic:
⟨a, hat, funext hab⟩

Premises used: Set.Mem, setOf, funext, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : Membership.mem (γ := Set ((i : ι) → β i)) (s.pi (α := β) fun (i : ι) ↦ f i '' t i) b
a : (i : ι) → α i
hab : ∀ (i : ι), f i (a i) = b i
hat : ∀ (i : ι), i ∈ s → a i ∈ t i
⊢ b ∈ Pi.map (α := α) (β := β) f '' s.pi (α := α) t

Tactic:
exact ⟨a, hat, funext hab⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
f : (i : ι) → α i → β i
t : (i : ι) → Set (α i)
⊢ ∀ (i : ι), ¬Membership.mem (γ := Set ι) univ i → Surjective (f i)

Tactic:
simp
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
f : (i : ι) → α i → β i
⊢ range (Pi.map (α := α) (β := β) f) = pi (α := β) univ fun (i : ι) ↦ range (f i)

Tactic:
simp only [← image_univ, ← piMap_image_univ_pi, pi_univ]

Premises used: Set.image_univ, Set.piMap_image_univ_pi, Set.pi_univ
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
s' : Set ((i : ι) → α i)
⊢ s' ⊆ s.pi (α := α) t ↔ ∀ (i : ι), i ∈ s → s' ⊆ (fun (x : (i : ι) → α i) ↦ x i) ⁻¹' t i

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst : DecidableEq ι
a : (i : ι) → α i
i : ι
b : α i
⊢ update (β := α) a i b ∈ s.pi (α := α) t ↔ a ∈ (s \ {i}).pi (α := α) t ∧ (i ∈ s → b ∈ t i)

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst : DecidableEq ι
a : (i : ι) → α i
i : ι
b : α i
ha : a ∈ s.pi (α := α) t
rw : a ∈ (s \ {i}).pi (α := α) t
⊢ update (β := α) a i b ∈ s.pi (α := α) t ↔ i ∈ s → b ∈ t i

Tactic:
rw [update_mem_pi_iff, and_iff_right]

Premises used: Set.update_mem_pi_iff, and_iff_right
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst : DecidableEq ι
a : (i : ι) → α i
i : ι
b : α i
ha : a ∈ s.pi (α := α) t
⊢ a ∈ (s \ {i}).pi (α := α) t

Tactic:
fun j hj => ha j hj.1

Premises used: Set.Mem, setOf, And.left, Set.pi
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst : DecidableEq ι
a : (i : ι) → α i
i : ι
b : α i
ha : a ∈ s.pi (α := α) t
⊢ a ∈ (s \ {i}).pi (α := α) t

Tactic:
exact fun j hj => ha j hj.1
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
simp :
  (a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) ↔
    ∀ (i : ι), a i ∈ t i ∧ ∀ (x : α i), x ∈ t i → x = a i
⊢ pi (α := α) univ t = {a} ↔ ∀ (i : ι), t i = {a i}

Tactic:
simp only [eq_singleton_iff_unique_mem]

Premises used: Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
h : a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a
i : ι
h₁ : a ∈ pi (α := α) univ t
h₂ : ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a
⊢ a i ∈ t i

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ (∀ (i : ι), a i ∈ t i ∧ ∀ (x : α i), x ∈ t i → x = a i) →
    a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
refine :
  (a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) →
    ∀ (i : ι) (h₁ : a ∈ pi (α := α) univ t) (h₂ : ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) (x : α i)
      (hx : x ∈ t i), x = a i
⊢ (a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) ↔
    ∀ (i : ι), a i ∈ t i ∧ ∀ (x : α i), x ∈ t i → x = a i

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ i => ⟨by grind, fun x hx => ?_⟩, by grind⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
h : a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a
i : ι
h₁ : a ∈ pi (α := α) univ t
h₂ : ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a
x : α i
hx : x ∈ t i
rw : x = update (β := α) a i x i
rw₁ rw₂ : x = x
⊢ x = a i

Tactic:
rw [← h₂ _ fun j _ => (update_mem_pi_iff_of_mem h₁).mpr (fun _ => hx) j trivial, update_self]

Premises used: Iff.mpr, trivial, Set.update_mem_pi_iff_of_mem, Function.update_self
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
simp :
  (a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) ↔
    ∀ (i : ι), a i ∈ t i ∧ ∀ (x : α i), x ∈ t i → x = a i
simp₁ :
  (a ∈ pi (α := α) univ t ∧ ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) →
    ∀ (i : ι) (h₁ : a ∈ pi (α := α) univ t) (h₂ : ∀ (x : (i : ι) → α i), x ∈ pi (α := α) univ t → x = a) (x : α i)
      (hx : x ∈ t i), x = a i
⊢ pi (α := α) univ t = {a} ↔ ∀ (i : ι), t i = {a i}

Tactic:
classical
  simp only [eq_singleton_iff_unique_mem]
  refine ⟨fun ⟨h₁, h₂⟩ i => ⟨by grind, fun x hx => ?_⟩, by grind⟩
  rw [← h₂ _ fun j _ => (update_mem_pi_iff_of_mem h₁).mpr (fun _ => hx) j trivial, update_self]

Premises used: Set.eq_singleton_iff_unique_mem, Function.update_self
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ s.pi (α := α) t₁ ⊆ s.pi (α := α) t₂ ↔ (∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i) ∨ s.pi (α := α) t₁ = ∅

Tactic:
⟨fun h => or_iff_not_imp_right.2 ?_, fun h => h.elim pi_mono fun h' => h'.symm ▸ empty_subset _⟩

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, Eq.rec, Iff.intro, Set.empty_subset, Set.pi, Set.pi_mono, Or.elim, Eq.symm
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : ∀ (h : s.pi (α := α) t₁ ⊆ s.pi (α := α) t₂), ¬s.pi (α := α) t₁ = ∅ → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
⊢ s.pi (α := α) t₁ ⊆ s.pi (α := α) t₂ ↔ (∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i) ∨ s.pi (α := α) t₁ = ∅

Tactic:
refine
    ⟨fun h => or_iff_not_imp_right.2 ?_, fun h => h.elim pi_mono fun h' => h'.symm ▸ empty_subset _⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi (α := α) t₁ ⊆ s.pi (α := α) t₂
rw : (s.pi (α := α) t₁).Nonempty → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
⊢ ¬s.pi (α := α) t₁ = ∅ → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i

Tactic:
rw [← Ne, ← nonempty_iff_ne_empty]

Premises used: Ne, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi (α := α) t₁ ⊆ s.pi (α := α) t₂
hne : (s.pi (α := α) t₁).Nonempty
i : ι
hi : i ∈ s
⊢ t₁ i ⊆ t₂ i

Tactic:
simpa only [eval_image_pi hi hne, eval_image_pi hi (hne.mono h)] using
    image_mono (f := fun f : ∀ i, α i => f i) h

Premises used: Set.image_mono, Set.Nonempty.mono, Set.eval_image_pi
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t₁ t₂ : (i : ι) → Set (α i)
⊢ pi (α := α) univ t₁ ⊆ pi (α := α) univ t₂ ↔ (∀ (i : ι), t₁ i ⊆ t₂ i) ∨ ∃ (i : ι), t₁ i = ∅

Tactic:
simp [pi_subset_pi_iff]

Premises used: Set.pi_subset_pi_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
i : ι
inst : DecidableEq ι
s : Set (α i)
h :
  ∀ (x : (x : ι) → α x),
    x ∈ eval (β := α) i ⁻¹' s ↔
      Membership.mem (γ := Set ((x : ι) → α x))
        (pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ univ) i s)) x
⊢ eval (β := α) i ⁻¹' s = pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ univ) i s)

Tactic:
ext x
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
i : ι
inst : DecidableEq ι
s : Set (α i)
x : (x : ι) → α x
⊢ x ∈ eval (β := α) i ⁻¹' s ↔
    Membership.mem (γ := Set ((x : ι) → α x))
      (pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ univ) i s)) x

Tactic:
simp [@forall_update_iff _ (fun i => Set (α i)) _ _ _ _ fun i' y => x i' ∈ y]

Premises used: Membership.mem, Function.forall_update_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
i : ι
inst : DecidableEq ι
s : Set (α i)
h :
  ∀ (x : (x : ι) → α x),
    x ∈ eval (β := α) i ⁻¹' s ↔
      Membership.mem (γ := Set ((x : ι) → α x))
        (pi (α := α) {i} (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ univ) i s)) x
⊢ eval (β := α) i ⁻¹' s = pi (α := α) {i} (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ univ) i s)

Tactic:
ext
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
i : ι
inst : DecidableEq ι
s : Set (α i)
x : (x : ι) → α x
⊢ x ∈ eval (β := α) i ⁻¹' s ↔
    Membership.mem (γ := Set ((x : ι) → α x))
      (pi (α := α) {i} (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ univ) i s)) x

Tactic:
simp
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
h : ∀ (x : α i), x ∈ update (β := α) f i ⁻¹' s.pi (α := α) t ↔ x ∈ t i
⊢ update (β := α) f i ⁻¹' s.pi (α := α) t = t i

Tactic:
ext x
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
⊢ x ∈ update (β := α) f i ⁻¹' s.pi (α := α) t ↔ x ∈ t i

Tactic:
⟨fun h => ?_, fun hx j hj => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
h : ∀ (h : x ∈ update (β := α) f i ⁻¹' s.pi (α := α) t), x ∈ t i
h₁ : ∀ (hx : x ∈ t i) (j : ι) (hj : j ∈ s), update (β := α) f i x j ∈ t j
⊢ x ∈ update (β := α) f i ⁻¹' s.pi (α := α) t ↔ x ∈ t i

Tactic:
refine ⟨fun h => ?_, fun hx j hj => ?_⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
h : x ∈ update (β := α) f i ⁻¹' s.pi (α := α) t
⊢ update (β := α) f i x i ∈ t i

Tactic:
h i hi
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
h : x ∈ update (β := α) f i ⁻¹' s.pi (α := α) t
h₁ : x = update (β := α) f i x i
⊢ x ∈ t i

Tactic:
convert! h i hi
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
h : x ∈ update (β := α) f i ⁻¹' s.pi (α := α) t
⊢ x = update (β := α) f i x i

Tactic:
simp
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h :
  ∀ (hi : j ∈ s) (hf : ∀ (j_1 : ι), j_1 ∈ s → j_1 ≠ j → f j_1 ∈ t j_1) (x : α j) (hx : x ∈ t j),
    update (β := α) f j x j ∈ t j
h₁ : ∀ (h : j ≠ i), update (β := α) f i x j ∈ t j
⊢ update (β := α) f i x j ∈ t j

Tactic:
obtain rfl | h := eq_or_ne j i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst : DecidableEq ι
f : (i : ι) → α i
j : ι
hj hi : j ∈ s
hf : ∀ (j_1 : ι), j_1 ∈ s → j_1 ≠ j → f j_1 ∈ t j_1
x : α j
hx : x ∈ t j
⊢ update (β := α) f j x j ∈ t j

Tactic:
simpa
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
h₁ : f j ∈ t j
⊢ update (β := α) f i x j ∈ t j

Tactic:
rw [update_of_ne h]

Premises used: Function.update_of_ne
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
⊢ f j ∈ t j

Tactic:
hf j hj h
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
⊢ f j ∈ t j

Tactic:
exact hf j hj h
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
β : ι → Type u_3
inst : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
h :
  ∀ (y : (a : ι) → β a),
    y ∈ update (β := β) x i '' s ↔
      Membership.mem (γ := Set ((a : ι) → β a))
        (pi (α := β) univ (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s)) y
⊢ update (β := β) x i '' s = pi (α := β) univ (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s)

Tactic:
ext y
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
β : ι → Type u_3
inst : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
h :
  (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔
    ∀ (i_1 : ι),
      Membership.mem (γ := Set (β i_1))
        (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s i_1 : Set (β i_1)) (y i_1)
⊢ y ∈ update (β := β) x i '' s ↔
    Membership.mem (γ := Set ((a : ι) → β a))
      (pi (α := β) univ (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s)) y

Tactic:
simp only [mem_image, update_eq_iff, ne_eq, and_left_comm (a := _ ∈ s), exists_eq_left, mem_pi,
    mem_univ, true_implies]

Premises used: Function.update_eq_iff, Set.mem_image, and_left_comm, exists_eq_left, Set.mem_pi, ne_eq, true_implies, Set.mem_univ
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
β : ι → Type u_3
inst : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
h :
  (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔
    y i ∈ s ∧ ∀ (x_1 : ι), x_1 ≠ i → Membership.mem (γ := Set (β x_1)) {x x_1} (y x_1)
⊢ (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔
    ∀ (i_1 : ι),
      Membership.mem (γ := Set (β i_1))
        (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s i_1 : Set (β i_1)) (y i_1)

Tactic:
rw [forall_update_iff (p := fun x s => y x ∈ s)]

Premises used: Membership.mem, Function.forall_update_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
β : ι → Type u_3
inst : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔
    y i ∈ s ∧ ∀ (x_1 : ι), x_1 ≠ i → Membership.mem (γ := Set (β x_1)) {x x_1} (y x_1)

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
i : ι
inst : DecidableEq ι
f : (i : ι) → α i
hf : ∀ (j : ι), j ≠ i → f j ∈ t j
⊢ update (β := α) f i ⁻¹' pi (α := α) univ t = t i

Tactic:
update_preimage_pi (mem_univ i) fun j _ => hf j

Premises used: Set.mem_univ, Set.update_preimage_pi
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
u : Set ((i : ι) → α i)
⊢ u ⊆ s.pi (α := α) fun (i : ι) ↦ eval (β := α) i '' u

Tactic:
fun f hf _ _ => ⟨f, hf, rfl⟩

Premises used: Set.Mem, setOf, Set.Subset, And.intro, Exists.intro, Set.image, Set.pi, rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
κ : Type u_4
α : Type u_5
s : Set ι
t : Set κ
u : ι × κ → Set α
⊢ uncurry ⁻¹' (s ×ˢ t).pi (α := fun (a : ι × κ) ↦ α) u =
    s.pi (α := fun (i : ι) ↦ (i : κ) → α) fun (i : ι) ↦ t.pi (α := fun (j : κ) ↦ α) fun (j : κ) ↦ u (i, j)

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
h :
  ∀ (x : (b : ι) → α b),
    Membership.mem (γ := Set ((b : ι) → α b))
        (preimage (β := (a : ι') → α ((f : (a : ι') → ι) a))
          (⇑(piCongrLeft α f).symm : (a : (b : ι) → α b) → (a : ι') → α ((f : (a : ι') → ι) a))
          (s.pi (α := fun (a : ι') ↦ α ((f : (a : ι') → ι) a)) fun (i' : ι') ↦ t ((f : (a : ι') → ι) i')))
        x ↔
      x ∈ pi (α := α) ((⇑f : (a : ι') → ι) '' s) t
⊢ preimage (β := (a : ι') → α ((f : (a : ι') → ι) a))
      (⇑(piCongrLeft α f).symm : (a : (b : ι) → α b) → (a : ι') → α ((f : (a : ι') → ι) a))
      (s.pi (α := fun (a : ι') ↦ α ((f : (a : ι') → ι) a)) fun (i' : ι') ↦ t ((f : (a : ι') → ι) i')) =
    pi (α := α) ((⇑f : (a : ι') → ι) '' s) t

Tactic:
ext