awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
⊢ s.pi (α := α) t₁ ⊆ s.pi (α := α) t₂

Tactic:
pi_mono' h Subset.rfl

Premises used: Set.pi_mono', Set.Subset.rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t t₁ : (i : ι) → Set (α i)
⊢ (s.pi (α := α) fun (i : ι) ↦ t i ∩ t₁ i) = s.pi (α := α) t ∩ s.pi (α := α) t₁

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s₁ = s₂
h' : ∀ (i : ι), i ∈ s₁ → t₁ i = t₂ i
⊢ s₁.pi (α := α) t₁ = s₂.pi (α := α) t₂

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
⊢ s.pi (α := α) t = ∅

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
i : ι
ht : t i = ∅
⊢ pi (α := α) univ t = ∅

Tactic:
pi_eq_empty (mem_univ i) ht

Premises used: Set.mem_univ, Set.pi_eq_empty
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
⊢ (s.pi (α := α) t).Nonempty ↔ ∀ (i : ι), ∃ (x : α i), i ∈ s → x ∈ t i

Tactic:
simp [Classical.skolem, Set.Nonempty]

Premises used: Classical.skolem, Set.Nonempty
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
⊢ (pi (α := α) univ t).Nonempty ↔ ∀ (i : ι), (t i).Nonempty

Tactic:
simp [Classical.skolem, Set.Nonempty]

Premises used: Classical.skolem, Set.Nonempty
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
rw : (¬∀ (i : ι), ∃ (x : α i), i ∈ s → x ∈ t i) ↔ ∃ (i : ι), IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅
⊢ s.pi (α := α) t = ∅ ↔ ∃ (i : ι), IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
rw [← not_nonempty_iff_eq_empty, pi_nonempty_iff]

Premises used: Set.not_nonempty_iff_eq_empty, Set.pi_nonempty_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
push : (∃ (i : ι), ∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ ∃ (i : ι), IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅
⊢ (¬∀ (i : ι), ∃ (x : α i), i ∈ s → x ∈ t i) ↔ ∃ (i : ι), IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
⊢ (∃ (i : ι), ∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ ∃ (i : ι), IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
exists_congr fun i => ?_

Premises used: exists_congr
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
refine : ∀ (i : ι), (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅
⊢ (∃ (i : ι), ∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ ∃ (i : ι), IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
refine exists_congr fun i => ?_

Premises used: exists_congr
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inl : IsEmpty.{u_2 + 1} (α i) → ((∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅)
inr : Nonempty.{u_2 + 1} (α i) → ((∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅)
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
cases isEmpty_or_nonempty (α i)

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
h : IsEmpty.{u_2 + 1} (α i)
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
simp [*, forall_and, eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem, forall_and
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
h : Nonempty.{u_2 + 1} (α i)
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty.{u_2 + 1} (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
simp [*, forall_and, eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem, forall_and
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
⊢ pi (α := α) univ t = ∅ ↔ ∃ (i : ι), t i = ∅

Tactic:
simp [← not_nonempty_iff_eq_empty, univ_pi_nonempty_iff]

Premises used: Set.not_nonempty_iff_eq_empty, Set.univ_pi_nonempty_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
h : Nonempty ι
⊢ Eq (α := Set ((i : ι) → α i)) (pi (α := α) univ fun (x : ι) ↦ ∅) ∅

Tactic:
univ_pi_eq_empty_iff.2 <| h.elim fun x => ⟨x, rfl⟩

Premises used: Iff.mpr, Set.univ_pi_eq_empty_iff, Nonempty.elim, Exists.intro, rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t₁ t₂ : (i : ι) → Set (α i)
⊢ Disjoint (pi (α := α) univ t₁) (pi (α := α) univ t₂) ↔ ∃ (i : ι), Disjoint (t₁ i) (t₂ i)

Tactic:
simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, univ_pi_eq_empty_iff]

Premises used: Set.univ_pi_eq_empty_iff, Set.disjoint_iff_inter_eq_empty, Set.pi_inter_distrib
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
i : ι
hi : i ∈ s
ht : Disjoint (t₁ i) (t₂ i)
⊢ Disjoint (s.pi (α := α) t₁) (s.pi (α := α) t₂)

Tactic:
disjoint_left.2 fun _ h₁ h₂ => disjoint_left.1 ht (h₁ _ hi) (h₂ _ hi)

Premises used: Iff.mpr, Set.disjoint_left, Iff.mp
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Unique ι
t : (i : ι) → Set (α i)
h :
  ∀ (x : α default),
    Membership.mem (γ := Set (α default)) (uniqueElim (α := α) ⁻¹' pi (α := α) univ t) x ↔
      Membership.mem (γ := Set (α default)) (t default) x
⊢ Eq (α := Set (α default)) (uniqueElim (α := α) ⁻¹' pi (α := α) univ t) (t default)

Tactic:
ext
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Unique ι
t : (i : ι) → Set (α i)
x : α default
⊢ Membership.mem (γ := Set (α default)) (uniqueElim (α := α) ⁻¹' pi (α := α) univ t) x ↔
    Membership.mem (γ := Set (α default)) (t default) x

Tactic:
simp [Unique.forall_iff]

Premises used: Unique.forall_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
⊢ s.pi (α := α) t = ∅ ↔ ∃ (i : ι), i ∈ s ∧ t i = ∅

Tactic:
simp [pi_eq_empty_iff]

Premises used: Set.pi_eq_empty_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
inst : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
⊢ Disjoint (s.pi (α := α) t₁) (s.pi (α := α) t₂) ↔ ∃ (i : ι), i ∈ s ∧ Disjoint (t₁ i) (t₂ i)

Tactic:
simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, pi_eq_empty_iff']

Premises used: Set.pi_eq_empty_iff', Set.disjoint_iff_inter_eq_empty, Set.pi_inter_distrib
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
i : ι
s : Set ι
t : (i : ι) → Set (α i)
⊢ (insert i s).pi (α := α) t = eval (β := α) i ⁻¹' t i ∩ s.pi (α := α) t

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
i : ι
t : (i : ι) → Set (α i)
⊢ pi (α := α) {i} t = eval (β := α) i ⁻¹' t i

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
i : ι
t : (i : ι) → Set (α i)
⊢ pi (α := α) {i} t = {x : (i : ι) → α i | x i ∈ t i}

Tactic:
singleton_pi i t

Premises used: Set.singleton_pi, Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
f g : (i : ι) → α i
⊢ Membership.mem (γ := Set ((i : ι) → α i)) (pi (α := α) univ fun (i : ι) ↦ {f i}) g ↔
    Membership.mem (γ := Set ((i : ι) → α i)) {f} g

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
t : (i : ι) → Set (β i)
f : (i : ι) → α i → β i
⊢ Eq (α := Set ((i : ι) → α i)) ((fun (g : (i : ι) → α i) (i : ι) ↦ f i (g i)) ⁻¹' s.pi (α := β) t)
    (s.pi (α := α) fun (i : ι) ↦ f i ⁻¹' t i)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.pi, rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h₁ :
  ∀ (f : (i : ι) → α i),
    Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f ↔
      f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
⊢ (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) =
    pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂

Tactic:
ext f
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f ↔
    f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h₁ :
  ∀ (h : Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f),
    f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
h₂ :
  f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂ →
    Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f
⊢ Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f ↔
    f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h_1 : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f
h₁ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁
h₂ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
⊢ f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁ ∩ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂

Tactic:
constructor
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h_1 : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f
i : ι
his : i ∈ s
hpi : p i
⊢ f i ∈ t₁ i

Tactic:
simpa [*] using h i
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h_1 : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : Membership.mem (γ := Set ((i : ι) → α i)) (s.pi (α := α) fun (i : ι) ↦ if p i then t₁ i else t₂ i) f
i : ι
his : i ∈ s
hpi : ¬p i
⊢ f i ∈ t₂ i

Tactic:
simpa [*] using h i
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁
ht₂ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
i : ι
his : i ∈ s
pos : p i → Membership.mem (γ := Set (α i)) ((fun (i : ι) ↦ if p i then t₁ i else t₂ i) i) (f i)
neg : ¬p i → Membership.mem (γ := Set (α i)) ((fun (i : ι) ↦ if p i then t₁ i else t₂ i) i) (f i)
⊢ Membership.mem (γ := Set (α i)) ((fun (i : ι) ↦ if p i then t₁ i else t₂ i) i) (f i)

Tactic:
by_cases p i
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁
ht₂ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
i : ι
his : i ∈ s
h_1 : p i
⊢ Membership.mem (γ := Set (α i)) ((fun (i : ι) ↦ if p i then t₁ i else t₂ i) i) (f i)

Tactic:
simp_all
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ p i} t₁
ht₂ : f ∈ pi (α := α) {i : ι | i ∈ s ∧ ¬p i} t₂
i : ι
his : i ∈ s
h_1 : ¬p i
⊢ Membership.mem (γ := Set (α i)) ((fun (i : ι) ↦ if p i then t₁ i else t₂ i) i) (f i)

Tactic:
simp_all
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t : (i : ι) → Set (α i)
⊢ (s₁ ∪ s₂).pi (α := α) t = s₁.pi (α := α) t ∩ s₂.pi (α := α) t

Tactic:
simp [pi, or_imp, forall_and, setOf_and]

Premises used: Set.setOf_and, or_imp, Set.pi, forall_and
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ (i : ι), ¬i ∈ s₁ → t₁ i = univ
ht₂ : ∀ (i : ι), ¬i ∈ s₂ → t₂ i = univ
⊢ ((s₁ ∪ s₂).pi (α := α) fun (i : ι) ↦ t₁ i ∩ t₂ i) = s₁.pi (α := α) t₁ ∩ s₂.pi (α := α) t₂

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
s : Set ι
⊢ s.pi (α := α) t ∩ sᶜ.pi (α := α) t = pi (α := α) univ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst : DecidableEq ι
hi : ¬i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
j : ι
hj : j ∈ s
h : j ≠ i
⊢ t j (update (β := α) f i a j) = t j (f j)

Tactic:
rw [update_of_ne]

Premises used: Function.update_of_ne
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst : DecidableEq ι
hi : ¬i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
j : ι
hj : j ∈ s
⊢ j ≠ i

Tactic:
fun h => hi (h ▸ hj)

Premises used: Eq.rec, Not
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst : DecidableEq ι
hi : ¬i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
j : ι
hj : j ∈ s
⊢ j ≠ i

Tactic:
exact fun h => hi (h ▸ hj)
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
rw :
  Eq (α := Set ((i : ι) → β i)) (s.pi (α := β) fun (j : ι) ↦ t j (update (β := α) f i a j))
    (({i} ∪ s).pi (α := β) fun (j : ι) ↦ t j (update (β := α) f i a j))
rw₁ rw₂ :
  Eq (α := Set ((i : ι) → β i)) (s.pi (α := β) fun (j : ι) ↦ t j (update (β := α) f i a j))
    (s.pi (α := β) fun (j : ι) ↦ t j (update (β := α) f i a j))
⊢ Eq (α := Set ((i : ι) → β i)) (s.pi (α := β) fun (j : ι) ↦ t j (update (β := α) f i a j))
    (({i} ∪ s \ {i}).pi (α := β) fun (j : ι) ↦ t j (update (β := α) f i a j))

Tactic:
rw [union_diff_self, union_eq_self_of_subset_left (singleton_subset_iff.2 hi)]

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.union_eq_self_of_subset_left, Set.union_diff_self
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
hi₁ : ¬i ∈ s \ {i}
⊢ Eq (α := Set ((i : ι) → β i)) (({i} ∪ s \ {i}).pi (α := β) fun (j : ι) ↦ t j (update (β := α) f i a j))
    ({x : (i : ι) → β i | x i ∈ t i a} ∩ (s \ {i}).pi (α := β) fun (j : ι) ↦ t j (f j))

Tactic:
rw [union_pi, singleton_pi', update_self, pi_update_of_notMem]

Premises used: Set.singleton_pi', Set.pi_update_of_notMem, Set.union_pi, Function.update_self
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ ¬i ∈ s \ {i}

Tactic:
simp
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
β : ι → Type u_4
i : ι
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
rw :
  Eq (α := Set ((i : ι) → β i)) (pi (α := β) univ fun (j : ι) ↦ t j (update (β := α) f i a j))
    ({x : (i : ι) → β i | x i ∈ t i a} ∩ pi (α := β) (univ \ {i}) fun (j : ι) ↦ t j (f j))
rw₁ rw₂ :
  Eq (α := Set ((i : ι) → β i)) (pi (α := β) univ fun (j : ι) ↦ t j (update (β := α) f i a j))
    (pi (α := β) univ fun (j : ι) ↦ t j (update (β := α) f i a j))
⊢ Eq (α := Set ((i : ι) → β i)) (pi (α := β) univ fun (j : ι) ↦ t j (update (β := α) f i a j))
    ({x : (i : ι) → β i | x i ∈ t i a} ∩ pi (α := β) {i}ᶜ fun (j : ι) ↦ t j (f j))

Tactic:
rw [compl_eq_univ_diff, ← pi_update_of_mem (mem_univ _)]

Premises used: Set.compl_eq_univ_diff, Set.mem_univ, Set.pi_update_of_mem
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
i : ι
s : Set (α i)
rw : ({x : (i : ι) → α i | x i ∈ s} ∩ pi (α := α) {i}ᶜ fun (j : ι) ↦ univ) = eval (β := α) i ⁻¹' s
rw₁ : {x : (i : ι) → α i | x i ∈ s} ∩ univ = eval (β := α) i ⁻¹' s
rw₂ : {x : (i : ι) → α i | x i ∈ s} = eval (β := α) i ⁻¹' s
rw₃ rw₄ : Eq (α := Set ((i : ι) → α i)) {x : (i : ι) → α i | x i ∈ s} {x : (x : ι) → α x | eval (β := α) i x ∈ s}
⊢ pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s) = eval (β := α) i ⁻¹' s

Tactic:
rw [univ_pi_update i (fun j => (univ : Set (α j))) s fun j t => t, pi_univ, inter_univ, preimage]

Premises used: Set.univ, Set.inter_univ, Set.preimage, Set.univ_pi_update, Set.pi_univ
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
⊢ eval (β := α) i '' s.pi (α := α) t ⊆ t i

Tactic:
image_subset_iff.2 fun _ hf => hf i hs

Premises used: Iff.mpr, Set.image_subset_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
i : ι
⊢ eval (β := α) i '' pi (α := α) univ t ⊆ t i

Tactic:
eval_image_pi_subset (mem_univ i)

Premises used: Set.eval_image_pi_subset, Set.mem_univ
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
ht : (s.pi (α := α) t).Nonempty
i : ι
obtain : ∀ (f : (i : ι) → α i) (hf : f ∈ s.pi (α := α) t), t i ⊆ eval (β := α) i '' s.pi (α := α) t
⊢ t i ⊆ eval (β := α) i '' s.pi (α := α) t

Tactic:
obtain ⟨f, hf⟩ := ht
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi (α := α) t
⊢ t i ⊆ eval (β := α) i '' s.pi (α := α) t

Tactic:
fun y hy => ⟨update f i y, fun j hj => ?_, update_self ..⟩

Premises used: Function.update, Set.Mem, setOf, Set.Subset, And.intro, Exists.intro, Set.image, Function.update_self
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi (α := α) t
refine : ∀ (y : α i) (hy : y ∈ t i) (j : ι) (hj : j ∈ s), update (β := α) f i y j ∈ t j
⊢ t i ⊆ eval (β := α) i '' s.pi (α := α) t

Tactic:
refine fun y hy => ⟨update f i y, fun j hj => ?_, update_self ..⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi (α := α) t
y : α i
hy : y ∈ t i
j : ι
hj : j ∈ s
inl : ∀ (y : α j) (hy : y ∈ t j), update (β := α) f j y j ∈ t j
inr : ∀ (hji : j ≠ i), update (β := α) f i y j ∈ t j
⊢ update (β := α) f i y j ∈ t j

Tactic:
obtain rfl | hji := 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)
f : (i : ι) → α i
hf : f ∈ s.pi (α := α) t
j : ι
hj : j ∈ s
y : α j
hy : y ∈ t j
⊢ update (β := α) f j y j ∈ t j

Tactic:
simp [*, hf _ hj]
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi (α := α) t
y : α i
hy : y ∈ t i
j : ι
hj : j ∈ s
hji : j ≠ i
⊢ update (β := α) f i y j ∈ t j

Tactic:
simp [*, hf _ hj]
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
ht : (s.pi (α := α) t).Nonempty
i : ι
obtain : ∀ (f : (i : ι) → α i) (hf : f ∈ s.pi (α := α) t), t i ⊆ eval (β := α) i '' s.pi (α := α) t
obtain₁ :
  ∀ (f : (i : ι) → α i) (hf : f ∈ s.pi (α := α) t) (y : α i) (hy : y ∈ t i) (j : ι) (hj : j ∈ s),
    update (β := α) f i y j ∈ t j
⊢ t i ⊆ eval (β := α) i '' s.pi (α := α) t

Tactic:
classical
  obtain ⟨f, hf⟩ := ht
  refine fun y hy => ⟨update f i y, fun j hj => ?_, update_self ..⟩
  obtain rfl | hji := eq_or_ne j i <;> simp [*, hf _ hj]

Premises used: rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : (s.pi (α := α) t).Nonempty
⊢ eval (β := α) i '' s.pi (α := α) t = t i

Tactic:
(eval_image_pi_subset hs).antisymm (subset_eval_image_pi ht i)

Premises used: Set.eval_image_pi_subset, Set.subset_eval_image_pi, HasSubset.Subset.antisymm
-- 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ᵢ
⊢ eval (β := α) i '' s.pi (α := α) t = if (s.pi (α := α) t).Nonempty then univ else ∅

Tactic:
ext xᵢ
-- 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
xᵢ : α i
h :
  (∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) ↔
    ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i
⊢ xᵢ ∈ eval (β := α) i '' s.pi (α := α) t ↔
    Membership.mem (γ := Set (α i)) (if (s.pi (α := α) t).Nonempty then univ else ∅) xᵢ

Tactic:
simp only [eval, mem_image, mem_pi, Set.Nonempty, mem_ite_empty_right, mem_univ, and_true]

Premises used: and_true, Set.mem_image, Set.mem_ite_empty_right, Set.mem_pi, Function.eval, Set.Nonempty, Set.mem_univ
-- 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
xᵢ : α i
h :
  (∃ (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 : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i) →
    ∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ
⊢ (∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ) ↔
    ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i

Tactic:
constructor
-- 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
x : (x : ι) → α x
hx : ∀ (i : ι), i ∈ s → x i ∈ t i
⊢ ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i

Tactic:
⟨x, hx⟩

Premises used: Exists.intro
-- 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
x : (x : ι) → α x
hx : ∀ (i : ι), i ∈ s → x i ∈ t i
⊢ ∃ (x : (i : ι) → α i), ∀ (i : ι), i ∈ s → x i ∈ t i

Tactic:
exact ⟨x, hx⟩
-- 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
xᵢ : α i
x : (i : ι) → α i
hx : ∀ (i : ι), i ∈ s → x i ∈ t i
⊢ ∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ

Tactic:
⟨Function.update x i xᵢ, ?_⟩

Premises used: Function.update, Exists.intro
-- 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
xᵢ : α i
x : (i : ι) → α i
hx : ∀ (i : ι), i ∈ s → x i ∈ t i
h : (∀ (i_1 : ι), i_1 ∈ s → update (β := α) x i xᵢ i_1 ∈ t i_1) ∧ update (β := α) x i xᵢ i = xᵢ
⊢ ∃ (x : (x : ι) → α x), (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ

Tactic:
refine ⟨Function.update x i xᵢ, ?_⟩
-- 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
xᵢ : α i
x : (i : ι) → α i
hx : ∀ (i : ι), i ∈ s → x i ∈ t i
⊢ (∀ (i_1 : ι), i_1 ∈ s → update (β := α) x i xᵢ i_1 ∈ t i_1) ∧ update (β := α) x i xᵢ i = xᵢ

Tactic:
simpa +contextual [(ne_of_mem_of_not_mem · hi)]

Premises used: ne_of_mem_of_not_mem