awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
rw :
  Eq.{u_2 + 1} (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β) (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) 1) : SetSemiring β)
    (1 : SetSemiring β)
rw₁ :
  Eq (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β) (singleton (α := β) ((f : (a : α) → β) 1 : β)) : SetSemiring β)
    (1 : SetSemiring β)
rw₂ : Eq (α := SetSemiring β) ((up : (a : Set β) → SetSemiring β) {1} : SetSemiring β) (1 : SetSemiring β)
rw₃ : Eq.{u_2 + 1} (α := SetSemiring β) ((up : (a : Set β) → SetSemiring β) 1 : SetSemiring β) (1 : SetSemiring β)
rw₄ rw₅ : Eq.{u_2 + 1} (α := SetSemiring β) 1 1
⊢ Eq.{u_2 + 1} (α := SetSemiring β)
    ((up : (a : Set β) → SetSemiring β)
        (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((down : (a : SetSemiring α) → Set α) 1)) :
      SetSemiring β)
    (1 : SetSemiring β)

Tactic:
rw [down_one, image_one, map_one, singleton_one, up_one]

Premises used: SetSemiring.down_one, Set.image_one, map_one, Set.up_one, Set.singleton_one
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
s : SetSemiring α
⊢ Eq (α := SetSemiring β) ((imageHom f : (a : SetSemiring α) → SetSemiring β) s : SetSemiring β)
    ((up : (a : Set β) → SetSemiring β)
        (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((down : (a : SetSemiring α) → Set α) s)) :
      SetSemiring β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
s : SetSemiring α
⊢ Eq.{u_2 + 1} (α := Set β)
    ((down : (a : SetSemiring β) → Set β) ((imageHom f : (a : SetSemiring α) → SetSemiring β) s : SetSemiring β) :
      Set β)
    (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((down : (a : SetSemiring α) → Set α) s) : Set β)

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.Data.Set.Semiring
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
s : Set α
⊢ Eq.{u_2 + 1} (α := SetSemiring β) ((up : (a : Set β) → SetSemiring β) ((⇑f : (a : α) → β) '' s) : SetSemiring β)
    ((imageHom f : (a : SetSemiring α) → SetSemiring β) ((up : (a : Set α) → SetSemiring α) s) : SetSemiring β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
i : ι
⊢ Eq (α := Set (Sigma α)) (range (Sigma.mk (β := α) i)) (Sigma.fst (β := α) ⁻¹' {i})

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
i j : ι
h : i ≠ j
s : Set (α j)
⊢ Sigma.mk (β := α) i ⁻¹' Sigma.mk (β := α) j '' s = ∅

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
⊢ Sigma.mk (β := α) i '' g i ⁻¹' s ⊆ Sigma.map (β₁ := α) (β₂ := β) f g ⁻¹' Sigma.mk (β := β) (f i) '' s

Tactic:
image_subset_iff.2 fun x hx ↦ ⟨g i x, hx, rfl⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Set.image_subset_iff, rfl
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
⊢ Sigma.mk (β := α) i '' g i ⁻¹' s = Sigma.map (β₁ := α) (β₂ := β) f g ⁻¹' Sigma.mk (β := β) (f i) '' s

Tactic:
(image_sigmaMk_preimage_sigmaMap_subset f g i s).antisymm ?_

Premises used: Set.image_sigmaMk_preimage_sigmaMap_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
refine : Sigma.map (β₁ := α) (β₂ := β) f g ⁻¹' Sigma.mk (β := β) (f i) '' s ⊆ Sigma.mk (β := α) i '' g i ⁻¹' s
⊢ Sigma.mk (β := α) i '' g i ⁻¹' s = Sigma.map (β₁ := α) (β₂ := β) f g ⁻¹' Sigma.mk (β := β) (f i) '' s

Tactic:
refine (image_sigmaMk_preimage_sigmaMap_subset f g i s).antisymm ?_

Premises used: Set.image_sigmaMk_preimage_sigmaMap_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
j : ι
x : α j
y : β (f i)
hys : y ∈ s
hxy : Sigma.mk (β := β) (f i) y = Sigma.map (β₁ := α) (β₂ := β) f g (Sigma.mk (β := α) j x)
⊢ i = j ∧ y ≍ g j x

Tactic:
simp only [hf.eq_iff, Sigma.map, Sigma.ext_iff] at hxy

Premises used: Function.Injective.eq_iff, Sigma.ext_iff, Sigma.map
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
j : ι
x : α j
y : β (f i)
hys : y ∈ s
hxy : i = j ∧ y ≍ g j x
⊢ Sigma.mk (β := α) j x ∈ Sigma.mk (β := α) i '' g i ⁻¹' s

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
x : (i : ι) × α i
⊢ x ∈ s.sigma (α := α) t ↔
    x.fst (β := fun (i : ι) ↦ α i) ∈ s ∧
      Membership.mem (γ := Set (α (x.fst (β := fun (i : ι) ↦ α i)))) (t (x.fst (β := fun (i : ι) ↦ α i)))
        (x.snd (β := fun (i : ι) ↦ α i))

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.sigma
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
a : α i
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) i a ∈ s.sigma (α := α) t ↔ i ∈ s ∧ a ∈ t i

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.sigma
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
a : α i
hi : i ∈ s
ha : a ∈ t i
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) i a ∈ s.sigma (α := α) t

Tactic:
⟨hi, ha⟩

Premises used: Set.Mem, setOf, Set.sigma, And.intro
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
hs : s₁ ⊆ s₂
ht : ∀ (i : ι), t₁ i ⊆ t₂ i
⊢ s₁.sigma (α := α) t₁ ⊆ s₂.sigma (α := α) t₂

Tactic:
fun _ hx ↦
  ⟨hs hx.1, ht _ hx.2⟩

Premises used: Set.Mem, setOf, Sigma.fst, Set.Subset, And.right, And.left, Set.sigma, And.intro
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
⊢ s.sigma (α := α) t ⊆ u ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃a : α i⦄, a ∈ t i → Sigma.mk (β := fun (i : ι) ↦ α i) i a ∈ u

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
p : (i : ι) × α i → Prop
⊢ (∀ x ∈ s.sigma (α := α) t, p x) ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃a : α i⦄, a ∈ t i → p (Sigma.mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
p : (i : ι) × α i → Prop
⊢ (∃ x ∈ s.sigma (α := α) t, p x) ↔ ∃ i ∈ s, ∃ a ∈ t i, p (Sigma.mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
⊢ Eq (α := Set ((i : ι) × α i)) (s.sigma (α := α) fun (i : ι) ↦ ∅) ∅

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
⊢ Set.sigma (α := α) ∅ t = ∅

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
i : ι
⊢ Eq (α := Set ((_ : ι) × α i)) (Set.sigma (α := fun (x : ι) ↦ α i) univ fun (x : ι) ↦ univ) univ

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
⊢ Eq (α := Set ((i : ι) × α i)) (s.sigma (α := α) fun (x : ι) ↦ univ) (Sigma.fst (β := fun (i : ι) ↦ α i) ⁻¹' s)

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ((i : ι) × α i)
⊢ (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' s) = s

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
i : ι
⊢ Set.sigma (α := α) {i} t = Sigma.mk (β := α) i '' t i

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
a : (i : ι) → α i
⊢ Eq (α := Set ((i : ι) × α i)) (s.sigma (α := α) fun (i : ι) ↦ {a i}) ((fun (i : ι) ↦ Sigma.mk (β := α) i (a i)) '' s)

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
i : ι
a : (i : ι) → α i
⊢ Eq (α := Set ((i : ι) × α i)) (Set.sigma (α := α) {i} fun (i : ι) ↦ {a i}) {Sigma.mk (β := fun (i : ι) ↦ α i) i (a i)}

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t : (i : ι) → Set (α i)
⊢ (s₁ ∪ s₂).sigma (α := α) t = s₁.sigma (α := α) t ∪ s₂.sigma (α := α) t

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ (s.sigma (α := α) fun (i : ι) ↦ t₁ i ∪ t₂ i) = s.sigma (α := α) t₁ ∪ s.sigma (α := α) t₂

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ s₁.sigma (α := α) t₁ ∩ s₂.sigma (α := α) t₂ = (s₁ ∩ s₂).sigma (α := α) fun (i : ι) ↦ t₁ i ∩ t₂ i

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
β : Type u_4
inst : CompleteLattice β
s : Set ι
t : (i : ι) → Set (α i)
f : Sigma α → β
x : β
⊢ ⨆ ij ∈ s.sigma (α := α) t, f ij ≤ x → ⨆ i ∈ s, ⨆ j ∈ t i, f (Sigma.mk (β := α) i j) ≤ x

Tactic:
simp_all
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
β : Type u_4
inst : CompleteLattice β
s : Set ι
t : (i : ι) → Set (α i)
f : Sigma α → β
x : β
⊢ ⨆ i ∈ s, ⨆ j ∈ t i, f (Sigma.mk (β := α) i j) ≤ x → ⨆ ij ∈ s.sigma (α := α) t, f ij ≤ x

Tactic:
simp_all
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
β : Type u_4
inst : CompleteLattice β
s : Set ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i → β
⊢ Eq.{u_4 + 1} (α := β) (⨆ i ∈ s, ⨆ j ∈ t i, f i j)
    (⨆ ij ∈ s.sigma (α := α) t, f (ij.fst (β := fun (i : ι) ↦ α i)) (ij.snd (β := fun (i : ι) ↦ α i)))

Tactic:
Eq.symm (biSup_sigma _ _ _)

Premises used: biSup_sigma, Eq.symm
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
β : Type u_4
inst : CompleteLattice β
s : Set ι
t : (i : ι) → Set (α i)
f : Sigma α → β
⊢ Eq.{u_4 + 1} (α := β) (⨅ ij ∈ s.sigma (α := α) t, f ij) (⨅ i ∈ s, ⨅ j ∈ t i, f (Sigma.mk (β := α) i j))

Tactic:
biSup_sigma (β := βᵒᵈ) _ _ _

Premises used: iInf, biSup_sigma, OrderDual
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
β : Type u_4
inst : CompleteLattice β
s : Set ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i → β
⊢ Eq.{u_4 + 1} (α := β) (⨅ i ∈ s, ⨅ j ∈ t i, f i j)
    (⨅ ij ∈ s.sigma (α := α) t, f (ij.fst (β := fun (i : ι) ↦ α i)) (ij.snd (β := fun (i : ι) ↦ α i)))

Tactic:
Eq.symm (biInf_sigma _ _ _)

Premises used: biInf_sigma, Eq.symm
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
β : Type u_5
s : Set ι
t : (i : ι) → Set (α i)
f : Sigma α → Set β
⊢ Eq.{u_5 + 1} (α := Set β) (⋃ ij ∈ s.sigma (α := α) t, f ij) (⋃ i ∈ s, ⋃ j ∈ t i, f (Sigma.mk (β := α) i j))

Tactic:
biSup_sigma _ _ _

Premises used: biSup_sigma, Set.iUnion
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
β : Type u_5
s : Set ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i → Set β
⊢ Eq.{u_5 + 1} (α := Set β) (⋃ i ∈ s, ⋃ j ∈ t i, f i j)
    (⋃ ij ∈ s.sigma (α := α) t, f (ij.fst (β := fun (i : ι) ↦ α i)) (ij.snd (β := fun (i : ι) ↦ α i)))

Tactic:
biSup_sigma' _ _ _

Premises used: biSup_sigma', Set.iUnion
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
β : Type u_5
s : Set ι
t : (i : ι) → Set (α i)
f : Sigma α → Set β
⊢ Eq.{u_5 + 1} (α := Set β) (⋂ ij ∈ s.sigma (α := α) t, f ij) (⋂ i ∈ s, ⋂ j ∈ t i, f (Sigma.mk (β := α) i j))

Tactic:
biInf_sigma _ _ _

Premises used: biInf_sigma, Set.iInter
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
β : Type u_5
s : Set ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i → Set β
⊢ Eq.{u_5 + 1} (α := Set β) (⋂ i ∈ s, ⋂ j ∈ t i, f i j)
    (⋂ ij ∈ s.sigma (α := α) t, f (ij.fst (β := fun (i : ι) ↦ α i)) (ij.snd (β := fun (i : ι) ↦ α i)))

Tactic:
biInf_sigma' _ _ _

Premises used: Set.iInter, biInf_sigma'
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
⊢ (insert i s).sigma (α := α) t = Sigma.mk (β := α) i '' t i ∪ s.sigma (α := α) t

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ (s.sigma (α := α) fun (i : ι) ↦ insert (a i) (t i)) =
    (fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i (a i)) '' s ∪ s.sigma (α := α) t

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
β : ι → Type u_6
f : ι' → ι
g : (i : ι) → β i → α i
⊢ Eq (α := Set ((i : ι') × β (f i))) ((f ⁻¹' s).sigma (α := fun (i : ι') ↦ β (f i)) fun (i : ι') ↦ g (f i) ⁻¹' t (f i))
    ((fun (p : (i : ι') × β (f i)) ↦
        Sigma.mk (β := α) (f (p.fst (β := fun (i : ι') ↦ β (f i))))
          (g (f (p.fst (β := fun (i : ι') ↦ β (f i)))) (p.snd (β := fun (i : ι') ↦ β (f i))))) ⁻¹'
      s.sigma (α := α) t)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.sigma, rfl
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
f : ι' → ι
⊢ Eq (α := Set ((i : ι') × α (f i))) ((f ⁻¹' s).sigma (α := fun (i : ι') ↦ α (f i)) fun (i : ι') ↦ t (f i))
    ((fun (p : (i : ι') × α (f i)) ↦
        Sigma.mk (β := α) (f (p.fst (β := fun (i : ι') ↦ α (f i)))) (p.snd (β := fun (i : ι') ↦ α (f i)))) ⁻¹'
      s.sigma (α := α) t)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.sigma, rfl
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
β : ι → Type u_6
g : (i : ι) → β i → α i
⊢ Eq (α := Set ((i : ι) × β i)) (s.sigma (α := β) fun (i : ι) ↦ g i ⁻¹' t i)
    ((fun (p : (i : ι) × β i) ↦
        Sigma.mk (β := α) (p.fst (β := fun (i : ι) ↦ β i))
          (g (p.fst (β := fun (i : ι) ↦ β i)) (p.snd (β := fun (i : ι) ↦ β i)))) ⁻¹'
      s.sigma (α := α) t)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.sigma, rfl
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
α' : ι' → Type u_7
f : ι → ι'
g : (i : ι) → α i → α' (f i)
s : Set ι'
t : (i : ι') → Set (α' i)
⊢ Sigma.map (β₁ := α) (β₂ := α') f g ⁻¹' s.sigma (α := α') t = (f ⁻¹' s).sigma (α := α) fun (i : ι) ↦ g i ⁻¹' t (f i)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.sigma, rfl
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hi : i ∈ s
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' s.sigma (α := α) t = t i

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hi : i ∉ s
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' s.sigma (α := α) t = ∅

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst : DecidablePred fun (x : ι) ↦ x ∈ s
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' s.sigma (α := α) t = if i ∈ s then t i else ∅

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
β : Type u_7
inst : DecidablePred fun (x : ι) ↦ x ∈ s
g : β → α i
⊢ (fun (b : β) ↦ Sigma.mk (β := α) i (g b)) ⁻¹' s.sigma (α := α) t = if i ∈ s then g ⁻¹' t i else ∅

Tactic:
grind
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_6
f : (i : ι) → α i → β i
⊢ ∀ (x : (i : ι) × β i),
    Membership.mem (γ := Set ((i : ι) × β i)) (Set.sigma (α := β) univ fun (i : ι) ↦ range (f i)) x ↔
      Membership.mem (γ := Set ((i : ι) × β i))
        (range fun (x : (i : ι) × α i) ↦
          Sigma.mk (β := fun (i : ι) ↦ β i) (x.fst (β := fun (i : ι) ↦ α i))
            (f (x.fst (β := fun (i : ι) ↦ α i)) (x.snd (β := fun (i : ι) ↦ α i))))
        x

Tactic:
simp [range, Sigma.forall]

Premises used: Sigma.forall, Set.range
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ s.Nonempty → (∀ (i : ι), (t i).Nonempty) → (s.sigma (α := α) t).Nonempty

Tactic:
fun ⟨i, hi⟩ h ↦
  let ⟨a, ha⟩ := h i
  ⟨⟨i, a⟩, hi, ha⟩

Premises used: _private.0.Set.Nonempty.sigma.match_1, _private.0.Set.Nonempty.sigma.match_2, Set.Nonempty, Set.sigma, And.intro, Exists.intro, Sigma.mk
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ (s.sigma (α := α) t).Nonempty → s.Nonempty

Tactic:
fun ⟨x, hx⟩ ↦ ⟨x.1, hx.1⟩

Premises used: Sigma.fst, Set.Nonempty, And.left, Exists.intro, _private.0.Set.Nonempty.sigma_fst.match_1
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ (s.sigma (α := α) t).Nonempty → ∃ i ∈ s, (t i).Nonempty

Tactic:
fun ⟨x, hx⟩ ↦ ⟨x.1, hx.1, x.2, hx.2⟩

Premises used: Membership.mem, Exists, Sigma.fst, And, Set.Nonempty, And.right, And.left, And.intro, Exists.intro, _private.0.Set.Nonempty.sigma_fst.match_1, Sigma.snd
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ (s.sigma (α := α) t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty

Tactic:
⟨Nonempty.sigma_snd, fun ⟨i, hi, a, ha⟩ ↦ ⟨⟨i, a⟩, hi, ha⟩⟩

Premises used: Set.Nonempty.sigma_snd, Set.Nonempty, Set.sigma, And.intro, Iff.intro, Exists.intro, Sigma.mk, _private.0.Set.sigma_nonempty_iff.match_1
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ (¬∃ i ∈ s, (t i).Nonempty) ↔ ∀ i ∈ s, t i = ∅

Tactic:
simp only [not_nonempty_iff_eq_empty, not_and, not_exists]

Premises used: Set.not_nonempty_iff_eq_empty, not_exists, not_and
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
a : (i : ι) → α i
ha : ∀ (i : ι), a i ∈ t i
⊢ (fun (i : ι) ↦ Sigma.mk (β := α) i (a i)) '' s ⊆ s.sigma (α := α) t

Tactic:
image_subset_iff.2 fun _ hi ↦ ⟨hi, ha _⟩

Premises used: Iff.mpr, Sigma.fst, And.intro, Set.image_subset_iff, Sigma.mk
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hi : i ∈ s
⊢ Sigma.mk (β := α) i '' t i ⊆ s.sigma (α := α) t

Tactic:
image_subset_iff.2 fun _ ↦ And.intro hi

Premises used: Iff.mpr, And.intro, Set.image_subset_iff
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ s.sigma (α := α) t ⊆ Sigma.fst (β := fun (i : ι) ↦ α i) ⁻¹' s

Tactic:
fun _ ↦ And.left

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, And.left, Set.sigma
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ Sigma.fst (β := fun (i : ι) ↦ α i) '' s.sigma (α := α) t ⊆ s

Tactic:
image_subset_iff.2 fun _ ↦ And.left

Premises used: Iff.mpr, And.left, Set.image_subset_iff
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
γ : Type u_7
f : (i : ι) × α i → γ
⊢ f '' s.sigma (α := α) t = ⋃ i ∈ s, f ∘ Sigma.mk (β := fun (i : ι) ↦ α i) i '' t i

Tactic:
aesop
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
s : Set ι
ht : ∀ (i : ι), (t i).Nonempty
⊢ Sigma.fst (β := fun (i : ι) ↦ α i) '' s.sigma (α := α) t = s

Tactic:
(fst_image_sigma_subset _ _).antisymm fun i hi ↦
    let ⟨a, ha⟩ := ht i
    ⟨⟨i, a⟩, ⟨hi, ha⟩, rfl⟩

Premises used: Membership.mem, _private.0.Set.Nonempty.sigma.match_1, Sigma.fst, Set.sigma, HasSubset.Subset.antisymm, And.intro, Exists.intro, Set.image, Sigma.mk, Set.fst_image_sigma_subset, rfl
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
pos :
  ∀ (h₁ : x.fst (β := fun (i : ι) ↦ α i) ∈ s₁),
    x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
neg :
  ∀ (h₁ : x.fst (β := fun (i : ι) ↦ α i) ∉ s₁),
    x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
⊢ x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁

Tactic:
by_cases h₁ : x.1 ∈ s₁

Premises used: Sigma.fst
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst (β := fun (i : ι) ↦ α i) ∈ s₁
pos :
  ∀
    (h₂ :
      Membership.mem (γ := Set (α (x.fst (β := fun (i : ι) ↦ α i)))) (t₁ (x.fst (β := fun (i : ι) ↦ α i)))
        (x.snd (β := fun (i : ι) ↦ α i))),
    x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
neg :
  ∀ (h₂ : x.snd (β := fun (i : ι) ↦ α i) ∉ t₁ (x.fst (β := fun (i : ι) ↦ α i))),
    x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
⊢ x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁

Tactic:
by_cases h₂ : x.2 ∈ t₁ x.1

Premises used: Sigma.fst, Sigma.snd
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst (β := fun (i : ι) ↦ α i) ∉ s₁
pos :
  ∀
    (h₂ :
      Membership.mem (γ := Set (α (x.fst (β := fun (i : ι) ↦ α i)))) (t₁ (x.fst (β := fun (i : ι) ↦ α i)))
        (x.snd (β := fun (i : ι) ↦ α i))),
    x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
neg :
  ∀ (h₂ : x.snd (β := fun (i : ι) ↦ α i) ∉ t₁ (x.fst (β := fun (i : ι) ↦ α i))),
    x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁
⊢ x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁

Tactic:
by_cases h₂ : x.2 ∈ t₁ x.1

Premises used: Sigma.fst, Sigma.snd
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst (β := fun (i : ι) ↦ α i) ∈ s₁
h₂ :
  Membership.mem (γ := Set (α (x.fst (β := fun (i : ι) ↦ α i)))) (t₁ (x.fst (β := fun (i : ι) ↦ α i)))
    (x.snd (β := fun (i : ι) ↦ α i))
⊢ x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁

Tactic:
simp [*, ← imp_iff_or_not]

Premises used: imp_iff_or_not
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst (β := fun (i : ι) ↦ α i) ∈ s₁
h₂ : x.snd (β := fun (i : ι) ↦ α i) ∉ t₁ (x.fst (β := fun (i : ι) ↦ α i))
⊢ x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁

Tactic:
simp [*, ← imp_iff_or_not]

Premises used: imp_iff_or_not
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst (β := fun (i : ι) ↦ α i) ∉ s₁
h₂ :
  Membership.mem (γ := Set (α (x.fst (β := fun (i : ι) ↦ α i)))) (t₁ (x.fst (β := fun (i : ι) ↦ α i)))
    (x.snd (β := fun (i : ι) ↦ α i))
⊢ x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁

Tactic:
simp [*, ← imp_iff_or_not]

Premises used: imp_iff_or_not
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst (β := fun (i : ι) ↦ α i) ∉ s₁
h₂ : x.snd (β := fun (i : ι) ↦ α i) ∉ t₁ (x.fst (β := fun (i : ι) ↦ α i))
⊢ x ∈ s₁.sigma (α := α) t₁ \ s₂.sigma (α := α) t₂ ↔ x ∈ s₁.sigma (α := α) (t₁ \ t₂) ∪ (s₁ \ s₂).sigma (α := α) t₁

Tactic:
simp [*, ← imp_iff_or_not]

Premises used: imp_iff_or_not
-- Module: Mathlib.Data.Set.Sigma
Goal:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ s.sigma (α := α) t = ⋃ i ∈ s, Sigma.mk (β := α) i '' t i

Tactic:
aesop