awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
x_in_U : ∃ i ∈ J, x ∈ Es i
obtain : ∀ (j : ι) (j_in_J : j ∈ J) (hjx : x ∈ Es j), i ∈ J
⊢ i ∈ J

Tactic:
obtain ⟨j, j_in_J, hjx⟩ := x_in_U
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
j : ι
j_in_J : j ∈ J
hjx : x ∈ Es j
by_contra : ∀ (i_ne_j : ¬i = j), False
⊢ i = j

Tactic:
by_contra i_ne_j
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
j : ι
j_in_J : j ∈ J
hjx : x ∈ Es j
i_ne_j : ¬i = j
⊢ False

Tactic:
Disjoint.ne_of_mem (Es_disj i_ne_j) hix hjx rfl

Premises used: Disjoint.ne_of_mem, rfl
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
j : ι
j_in_J : j ∈ J
hjx : x ∈ Es j
i_ne_j : ¬i = j
⊢ False

Tactic:
exact Disjoint.ne_of_mem (Es_disj i_ne_j) hix hjx rfl

Premises used: Disjoint.ne_of_mem, rfl
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
j : ι
j_in_J : j ∈ J
hjx : x ∈ Es j
rwa rwa₁ rwa₂ rwa₃ : j ∈ J
⊢ i ∈ J

Tactic:
rwa [show i = j by by_contra i_ne_j; exact Disjoint.ne_of_mem (Es_disj i_ne_j) hix hjx rfl]
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
⊢ ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j) x ↔ i ∈ J

Tactic:
have obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J := by
    refine fun J ↦ ⟨?_, fun i_in_J ↦ by simpa only [mem_iUnion, exists_prop] using ⟨i, i_in_J, hix⟩⟩
    intro x_in_U
    simp only [mem_iUnion, exists_prop] at x_in_U
    obtain ⟨j, j_in_J, hjx⟩ := x_in_U
    rwa [show i = j by by_contra i_ne_j; exact Disjoint.ne_of_mem (Es_disj i_ne_j) hix hjx rfl]
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
obs : ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j) x ↔ i ∈ J
J : Set ι
⊢ Membership.mem (γ := Set α) (⋃ j ∈ J, Es j)ᶜ x ↔ i ∉ J

Tactic:
simpa only [mem_compl_iff, not_iff_not] using obs J

Premises used: not_iff_not, Set.mem_compl_iff
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
obs : ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j) x ↔ i ∈ J
⊢ ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j)ᶜ x ↔ i ∉ J

Tactic:
have obs' : ∀ (J : Set ι), x ∈ (⋃ j ∈ J, Es j)ᶜ ↔ i ∉ J :=
    fun J ↦ by simpa only [mem_compl_iff, not_iff_not] using obs J
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), Es i) univ
Es_disj : Pairwise fun (i j : ι) ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
obs : ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j) x ↔ i ∈ J
obs' : ∀ (J : Set ι), Membership.mem (γ := Set α) (⋃ j ∈ J, Es j)ᶜ x ↔ i ∉ J
h : Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ i ∈ Iᶜ
h₁ : i ∉ I ↔ i ∈ Iᶜ
h₂ h₃ : i ∉ I ↔ i ∉ I
⊢ Membership.mem (γ := Set α) (⋃ i ∈ I, Es i)ᶜ x ↔ Membership.mem (γ := Set α) (⋃ i ∈ Iᶜ, Es i) x

Tactic:
rw [obs, obs', mem_compl_iff]

Premises used: Set.mem_compl_iff
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
inst : Preorder α
f : ι → α
h : ∀ (c : α), Membership.mem (γ := Set α) (⋂ (i : ι), Iic (f i)) c ↔ c ∈ lowerBounds (range f)
⊢ ⋂ (i : ι), Iic (f i) = lowerBounds (range f)

Tactic:
ext c
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
inst : Preorder α
f : ι → α
c : α
⊢ Membership.mem (γ := Set α) (⋂ (i : ι), Iic (f i)) c ↔ c ∈ lowerBounds (range f)

Tactic:
simp [lowerBounds]

Premises used: lowerBounds
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
inst : Preorder α
f : ι → α
⊢ ⋂ (i : ι), Iic (f i) = lowerBounds (range f)

Tactic:
have : (⋂ (i : ι), Iic (f i)) = lowerBounds (range f) := by
    ext c; simp [lowerBounds]
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
inst : Preorder α
f : ι → α
this : ⋂ (i : ι), Iic (f i) = lowerBounds (range f)
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (i : ι), Iic (f i)) ↔ BddBelow (range f)

Tactic:
simp [this, BddBelow]

Premises used: BddBelow
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
inst : Preorder α
f : ι → α
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (i : ι), Ici (f i)) ↔ BddAbove (range f)

Tactic:
nonempty_iInter_Iic_iff (α := αᵒᵈ)

Premises used: Set.Ici, Set.nonempty_iInter_Iic_iff, Set.Mem, setOf, upperBounds, BddAbove, OrderDual
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
inst : CompleteLattice α
f : ι → α
x : α
⊢ Membership.mem (γ := Set α) (Ici (⨆ (i : ι), f i)) x ↔ Membership.mem (γ := Set α) (⋂ (i : ι), Ici (f i)) x

Tactic:
simp only [mem_Ici, iSup_le_iff, mem_iInter]

Premises used: Set.mem_iInter, Set.mem_Ici, iSup_le_iff
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
inst : CompleteLattice α
f : ι → α
x : α
⊢ Membership.mem (γ := Set α) (Iic (⨅ (i : ι), f i)) x ↔ Membership.mem (γ := Set α) (⋂ (i : ι), Iic (f i)) x

Tactic:
simp only [mem_Iic, le_iInf_iff, mem_iInter]

Premises used: le_iInf_iff, Set.mem_iInter, Set.mem_Iic
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
inst : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Eq.{u_1 + 1} (α := Set α) (Ici (⨆ (i : ι), ⨆ (j : κ i), f i j)) (⋂ (i : ι), ⋂ (j : κ i), Ici (f i j))

Tactic:
simp_rw [Ici_iSup]

Premises used: Set.Ici_iSup
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
inst : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Eq.{u_1 + 1} (α := Set α) (Iic (⨅ (i : ι), ⨅ (j : κ i), f i j)) (⋂ (i : ι), ⋂ (j : κ i), Iic (f i j))

Tactic:
simp_rw [Iic_iInf]

Premises used: Set.Iic_iInf
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
rw : Eq.{u_1 + 1} (α := Set α) (Ici (⨆ a ∈ s, a)) (⋂ a ∈ s, Ici a)
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ s, Ici i) (⋂ a ∈ s, Ici a)
⊢ Ici (sSup s) = ⋂ a ∈ s, Ici a

Tactic:
rw [sSup_eq_iSup, Ici_iSup₂]

Premises used: Set.Ici_iSup₂, sSup_eq_iSup
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
rw : Eq.{u_1 + 1} (α := Set α) (Iic (⨅ a ∈ s, a)) (⋂ a ∈ s, Iic a)
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ s, Iic i) (⋂ a ∈ s, Iic a)
⊢ Iic (sInf s) = ⋂ a ∈ s, Iic a

Tactic:
rw [sInf_eq_iInf, Iic_iInf₂]

Premises used: Set.Iic_iInf₂, sInf_eq_iInf
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
simp : Subset.{u_2} (α := Set β) (⋃ x ∈ s₁, t x) (⋃ x ∈ s₂ ∪ s₁ \ s₂, t x)
⊢ Subset.{u_2} (α := Set β) ((⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x) (⋃ x ∈ s₁ \ s₂, t x)

Tactic:
simp only [diff_subset_iff, ← biUnion_union]

Premises used: Set.diff_subset_iff, Set.biUnion_union
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
h : s₁ ⊆ s₂ ∪ s₁ \ s₂
⊢ Subset.{u_2} (α := Set β) (⋃ x ∈ s₁, t x) (⋃ x ∈ s₂ ∪ s₁ \ s₂, t x)

Tactic:
apply biUnion_subset_biUnion_left

Premises used: Set.biUnion_subset_biUnion_left
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
h : s₁ ⊆ s₂ ∪ s₁
⊢ s₁ ⊆ s₂ ∪ s₁ \ s₂

Tactic:
rw [union_diff_self]

Premises used: Set.union_diff_self
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁

Tactic:
apply subset_union_right

Premises used: Set.subset_union_right
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
t : α → Set β
b : β
hb : Membership.mem (γ := Set β) (⋃ (i : α), t i) b
⊢ ∃ (a : α), b ∈ t a

Tactic:
simpa using hb
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
b₂ : β
h₂ : b₂ ∈ t a₂
eq :
  sigmaToiUnion t
      (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
    sigmaToiUnion t
      (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₂ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₂) b₂ h₂))
b_eq : b₁ = b₂
a_eq : a₁ = a₂
subst :
  ∀ (h₂ : b₁ ∈ t a₂)
    (eq :
      sigmaToiUnion t
          (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
        sigmaToiUnion t
          (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₂ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₂) b₁ h₂))),
    Eq.{u_2 + 1} (α := β)
      (↑(Eq.recOn (motive :=
            fun (x : α)
              (x_1 :
                Sigma.fst (β := fun (a : α) ↦ (↑(t a) : Type u_2))
                    (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁
                      (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
                  x) ↦
            (↑(t x) : Type u_2)) a_eq
            (Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
              (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁
                (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)))) :
        β)
      (↑(Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
            (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₂ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₂) b₁ h₂))) :
        β)
⊢ Eq.{u_2 + 1} (α := β)
    (↑(Eq.recOn (motive :=
          fun (x : α)
            (x_1 :
              Sigma.fst (β := fun (a : α) ↦ (↑(t a) : Type u_2))
                  (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁
                    (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
                x) ↦
          (↑(t x) : Type u_2)) a_eq
          (Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
            (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)))) :
      β)
    (↑(Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
          (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₂ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₂) b₂ h₂))) :
      β)

Tactic:
subst b_eq
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
a_eq : a₁ = a₂
h₂ : b₁ ∈ t a₂
eq :
  sigmaToiUnion t
      (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
    sigmaToiUnion t
      (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₂ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₂) b₁ h₂))
subst :
  ∀ (h₂ : b₁ ∈ t a₁)
    (eq :
      sigmaToiUnion t
          (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
        sigmaToiUnion t
          (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₂))),
    Eq.{u_2 + 1} (α := β)
      (↑(Eq.recOn (motive :=
            fun (x : α)
              (x_1 :
                Sigma.fst (β := fun (a : α) ↦ (↑(t a) : Type u_2))
                    (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁
                      (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
                  x) ↦
            (↑(t x) : Type u_2)) ⋯
            (Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
              (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁
                (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)))) :
        β)
      (↑(Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
            (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₂))) :
        β)
⊢ Eq.{u_2 + 1} (α := β)
    (↑(Eq.recOn (motive :=
          fun (x : α)
            (x_1 :
              Sigma.fst (β := fun (a : α) ↦ (↑(t a) : Type u_2))
                  (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁
                    (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
                x) ↦
          (↑(t x) : Type u_2)) a_eq
          (Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
            (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)))) :
      β)
    (↑(Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
          (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₂ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₂) b₁ h₂))) :
      β)

Tactic:
subst a_eq
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ h₂ : b₁ ∈ t a₁
eq :
  sigmaToiUnion t
      (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
    sigmaToiUnion t
      (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₂))
⊢ Eq.{u_2 + 1} (α := β)
    (↑(Eq.recOn (motive :=
          fun (x : α)
            (x_1 :
              Sigma.fst (β := fun (a : α) ↦ (↑(t a) : Type u_2))
                  (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁
                    (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)) =
                x) ↦
          (↑(t x) : Type u_2)) ⋯
          (Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
            (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₁)))) :
      β)
    (↑(Sigma.snd (β := fun (a : α) ↦ (↑(t a) : Type u_2))
          (Sigma.mk (β := fun (i : α) ↦ (↑(t i) : Type u_2)) a₁ (Subtype.mk (p := fun (x : β) ↦ x ∈ t a₁) b₁ h₂))) :
      β)

Tactic:
rfl
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
⊢ Bijective (sigmaToiUnion t)

Tactic:
⟨sigmaToiUnion_injective t h, sigmaToiUnion_surjective t⟩

Premises used: And.intro, Set.sigmaToiUnion_injective, Function.Bijective, Set.sigmaToiUnion_surjective
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : (i : α) × (↑(t i) : Type u_13)
⊢ (↑(((unionEqSigmaOfDisjoint (t := t) h).symm : (a : (i : α) × (↑(t i) : Type u_13)) → (↑(⋃ (i : α), t i) : Type u_13))
          x) :
      β) =
    (↑(x.snd (β := fun (i : α) ↦ (↑(t i) : Type u_13))) : β)

Tactic:
rfl
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : (↑(⋃ (i : α), t i) : Type u_13)
right : (↑x : β)
| (↑(Sigma.snd (β := fun (i : α) ↦ (↑(t i) : Type u_13))
            ((unionEqSigmaOfDisjoint (t := t) h :
                (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
              x) :
          (↑(t
                (Sigma.fst (β := fun (i : α) ↦ (↑(t i) : Type u_13))
                  ((unionEqSigmaOfDisjoint (t := t) h :
                      (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
                    x))) :
            Type u_13)) :
      β) =
    (↑x : β)

Tactic:
right
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : (↑(⋃ (i : α), t i) : Type u_13)
rw :
  (↑(((unionEqSigmaOfDisjoint (t := t) h).symm : (a : (i : α) × (↑(t i) : Type u_13)) → (↑(⋃ (i : α), t i) : Type u_13))
        ((unionEqSigmaOfDisjoint (t := t) h : (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
          x)) :
    β)
| (↑x : β)

Tactic:
rw [← unionEqSigmaOfDisjoint h |>.symm_apply_apply x]

Premises used: Equiv.symm_apply_apply, Set.unionEqSigmaOfDisjoint
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : (↑(⋃ (i : α), t i) : Type u_13)
rw :
  (↑(((unionEqSigmaOfDisjoint (t := t) h).symm : (a : (i : α) × (↑(t i) : Type u_13)) → (↑(⋃ (i : α), t i) : Type u_13))
        ((unionEqSigmaOfDisjoint (t := t) h : (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
          x)) :
    β)
| (↑(Sigma.snd (β := fun (i : α) ↦ (↑(t i) : Type u_13))
            ((unionEqSigmaOfDisjoint (t := t) h :
                (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
              x) :
          (↑(t
                (Sigma.fst (β := fun (i : α) ↦ (↑(t i) : Type u_13))
                  ((unionEqSigmaOfDisjoint (t := t) h :
                      (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
                    x))) :
            Type u_13)) :
      β) =
    (↑x : β)

Tactic:
right; rw [← unionEqSigmaOfDisjoint h |>.symm_apply_apply x]

Premises used: Equiv.symm_apply_apply, Set.unionEqSigmaOfDisjoint
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : (↑(⋃ (i : α), t i) : Type u_13)
conv :
  Eq.{u_13 + 1} (α := β)
    (↑(Sigma.snd (β := fun (i : α) ↦ (↑(t i) : Type u_13))
            ((unionEqSigmaOfDisjoint (t := t) h :
                (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
              x) :
          (↑(t
                (Sigma.fst (β := fun (i : α) ↦ (↑(t i) : Type u_13))
                  ((unionEqSigmaOfDisjoint (t := t) h :
                      (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
                    x))) :
            Type u_13)) :
      β)
    (↑(((unionEqSigmaOfDisjoint (t := t) h).symm :
            (a : (i : α) × (↑(t i) : Type u_13)) → (↑(⋃ (i : α), t i) : Type u_13))
          ((unionEqSigmaOfDisjoint (t := t) h : (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
            x)) :
      β)
⊢ (↑(Sigma.snd (β := fun (i : α) ↦ (↑(t i) : Type u_13))
            ((unionEqSigmaOfDisjoint (t := t) h :
                (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
              x) :
          (↑(t
                (Sigma.fst (β := fun (i : α) ↦ (↑(t i) : Type u_13))
                  ((unionEqSigmaOfDisjoint (t := t) h :
                      (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
                    x))) :
            Type u_13)) :
      β) =
    (↑x : β)

Tactic:
conv => right; rw [← unionEqSigmaOfDisjoint h |>.symm_apply_apply x]

Premises used: Equiv.symm_apply_apply, Set.unionEqSigmaOfDisjoint
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : (↑(⋃ (i : α), t i) : Type u_13)
⊢ Eq.{u_13 + 1} (α := β)
    (↑(Sigma.snd (β := fun (i : α) ↦ (↑(t i) : Type u_13))
            ((unionEqSigmaOfDisjoint (t := t) h :
                (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
              x) :
          (↑(t
                (Sigma.fst (β := fun (i : α) ↦ (↑(t i) : Type u_13))
                  ((unionEqSigmaOfDisjoint (t := t) h :
                      (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
                    x))) :
            Type u_13)) :
      β)
    (↑(((unionEqSigmaOfDisjoint (t := t) h).symm :
            (a : (i : α) × (↑(t i) : Type u_13)) → (↑(⋃ (i : α), t i) : Type u_13))
          ((unionEqSigmaOfDisjoint (t := t) h : (a : (↑(⋃ (i : α), t i) : Type u_13)) → (i : α) × (↑(t i) : Type u_13))
            x)) :
      β)

Tactic:
rfl
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
u : ℕ → Set α
n : ℕ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), ⋃ (_ : i ≥ n), u i) (⋃ (i : ℕ), u (i + n))

Tactic:
iSup_ge_eq_iSup_nat_add u n

Premises used: iSup_ge_eq_iSup_nat_add, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
u : ℕ → Set α
n : ℕ
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), ⋂ (_ : i ≥ n), u i) (⋂ (i : ℕ), u (i + n))

Tactic:
iInf_ge_eq_iInf_nat_add u n

Premises used: Set.iInter, iInf_ge_eq_iInf_nat_add
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
f : ℕ → Set α
hf : Monotone f
k : ℕ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), f (n + k)) (⋃ (n : ℕ), f n)

Tactic:
hf.iSup_nat_add k

Premises used: Set.iUnion, Monotone.iSup_nat_add
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
f : ℕ → Set α
hf : Antitone f
k : ℕ
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), f (n + k)) (⋂ (n : ℕ), f n)

Tactic:
hf.iInf_nat_add k

Premises used: Antitone.iInf_nat_add, Set.iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
f : ℕ → Set α
k : ℕ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), ⋂ (i : ℕ), ⋂ (_ : i ≥ n), f (i + k)) (⋃ (n : ℕ), ⋂ (i : ℕ), ⋂ (_ : i ≥ n), f i)

Tactic:
iSup_iInf_ge_nat_add f k

Premises used: Set.iInter, iSup_iInf_ge_nat_add, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
u : ℕ → Set α
⊢ u 0 ∪ ⋃ (i : ℕ), u (i + 1) = ⋃ (i : ℕ), u i

Tactic:
sup_iSup_nat_succ u

Premises used: sup_iSup_nat_succ, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
u : ℕ → Set α
⊢ u 0 ∩ ⋂ (i : ℕ), u (i + 1) = ⋂ (i : ℕ), u i

Tactic:
inf_iInf_nat_succ u

Premises used: inf_iInf_nat_succ, Set.iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
⊢ Eq (α := Set ℕ) (⋃ (n : ℕ), {i : ℕ | i ≤ n}) univ

Tactic:
subset_antisymm (Set.subset_univ _)
    (fun i _ ↦ Set.mem_iUnion_of_mem i (Set.mem_setOf.mpr (le_refl _)))

Premises used: Iff.mpr, le_refl, Set.subset_univ, subset_antisymm, Set.mem_setOf, Set.mem_iUnion_of_mem
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : CompleteLattice β
s : ι → Set α
f : α → β
rw :
  Eq.{u_2 + 1} (α := β) (⨆ (a : α), ⨆ (_ : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a), f a)
    (⨆ (j : α), ⨆ (i : ι), ⨆ (_ : j ∈ s i), f j)
⊢ Eq.{u_2 + 1} (α := β) (⨆ (a : α), ⨆ (_ : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a), f a)
    (⨆ (i : ι), ⨆ a ∈ s i, f a)

Tactic:
rw [iSup_comm]

Premises used: iSup_comm
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : CompleteLattice β
s : ι → Set α
f : α → β
simp_rw :
  Eq.{u_2 + 1} (α := β) (⨆ (a : α), ⨆ (_ : ∃ (i : ι), a ∈ s i), f a) (⨆ (j : α), ⨆ (i : ι), ⨆ (_ : j ∈ s i), f j)
⊢ Eq.{u_2 + 1} (α := β) (⨆ (a : α), ⨆ (_ : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a), f a)
    (⨆ (j : α), ⨆ (i : ι), ⨆ (_ : j ∈ s i), f j)

Tactic:
simp_rw [mem_iUnion, iSup_exists]

Premises used: iSup_exists, Set.mem_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : CompleteLattice β
s : ι → Set α
f : α → β
⊢ Eq.{u_2 + 1} (α := β) (⨅ (a : α), ⨅ (_ : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a), f a)
    (⨅ (i : ι), ⨅ a ∈ s i, f a)

Tactic:
iSup_iUnion (β := βᵒᵈ) s f

Premises used: iInf, iSup_iUnion, OrderDual
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
inst : CompleteLattice β
t : ι → Set β
simp_rw :
  Eq.{u_2 + 1} (α := β) (⨆ (a : β), ⨆ (_ : Membership.mem (γ := Set β) (⋃ (i : ι), t i) a), a) (⨆ (i : ι), ⨆ a ∈ t i, a)
⊢ Eq.{u_2 + 1} (α := β) (sSup (⋃ (i : ι), t i)) (⨆ (i : ι), sSup (t i))

Tactic:
simp_rw [sSup_eq_iSup, iSup_iUnion]

Premises used: iSup_iUnion, sSup_eq_iSup
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
inst : CompleteLattice β
s : Set (Set β)
⊢ sSup (⋃₀ s) = ⨆ t ∈ s, sSup t

Tactic:
simp only [sUnion_eq_biUnion, sSup_eq_iSup, iSup_iUnion]

Premises used: Set.sUnion_eq_biUnion, iSup_iUnion, sSup_eq_iSup
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
inst : CompleteLattice β
s : Set (Set β)
⊢ sInf (⋃₀ s) = ⨅ t ∈ s, sInf t

Tactic:
sSup_sUnion (β := βᵒᵈ) s

Premises used: iInf, Set.Mem, sSup_sUnion, OrderDual