awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice β
S : Set (Set α)
f : α → β
rw :
  Eq.{u_2 + 1} (α := β) (⨆ (x : α), ⨆ (_ : Membership.mem (γ := Set α) (⋃ (i : (↑S : Type u_1)), (↑i : Set α)) x), f x)
    (⨆ s ∈ S, ⨆ x ∈ s, f x)
rw₁ : Eq.{u_2 + 1} (α := β) (⨆ (i : (↑S : Type u_1)), ⨆ a ∈ (↑i : Set α), f a) (⨆ s ∈ S, ⨆ x ∈ s, f x)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := β) (⨆ (i : (↑S : Type u_1)), ⨆ a ∈ (↑i : Set α), f a)
    (⨆ (i : (↑S : Type u_1)), ⨆ x ∈ (↑i : Set α), f x)
⊢ Eq.{u_2 + 1} (α := β) (⨆ x ∈ ⋃₀ S, f x) (⨆ s ∈ S, ⨆ x ∈ s, f x)

Tactic:
rw [sUnion_eq_iUnion, iSup_iUnion, ← iSup_subtype'']

Premises used: Set.sUnion_eq_iUnion, iSup_subtype'', iSup_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice β
S : Set (Set α)
f : α → β
rw :
  Eq.{u_2 + 1} (α := β) (⨅ (x : α), ⨅ (_ : Membership.mem (γ := Set α) (⋃ (i : (↑S : Type u_1)), (↑i : Set α)) x), f x)
    (⨅ s ∈ S, ⨅ x ∈ s, f x)
rw₁ : Eq.{u_2 + 1} (α := β) (⨅ (i : (↑S : Type u_1)), ⨅ a ∈ (↑i : Set α), f a) (⨅ s ∈ S, ⨅ x ∈ s, f x)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := β) (⨅ (i : (↑S : Type u_1)), ⨅ a ∈ (↑i : Set α), f a)
    (⨅ (i : (↑S : Type u_1)), ⨅ x ∈ (↑i : Set α), f x)
⊢ Eq.{u_2 + 1} (α := β) (⨅ x ∈ ⋃₀ S, f x) (⨅ s ∈ S, ⨅ x ∈ s, f x)

Tactic:
rw [sUnion_eq_iUnion, iInf_iUnion, ← iInf_subtype'']

Premises used: Set.sUnion_eq_iUnion, iInf_subtype'', iInf_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
p : α → Prop
simp_rw : ⨅ i ∈ ⋃₀ S, p i ↔ ⨅ i ∈ S, ⨅ i_2 ∈ i, p i_2
⊢ (∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x

Tactic:
simp_rw [← iInf_Prop_eq, iInf_sUnion]

Premises used: iInf_Prop_eq, iInf_sUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
p : α → Prop
simp_rw : (∃ (x : α) (_ : x ∈ ⋃₀ S), p x) ↔ ∃ (s : Set α) (_ : s ∈ S) (x : α) (_ : x ∈ s), p x
simp_rw₁ : ⨆ x ∈ ⋃₀ S, p x ↔ ⨆ s ∈ S, ⨆ x ∈ s, p x
⊢ (∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x

Tactic:
simp_rw [← exists_prop, ← iSup_Prop_eq, iSup_sUnion]

Premises used: exists_prop, iSup_Prop_eq, iSup_sUnion
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ range (map f) = {l : List β | ∀ (x : β), x ∈ l → x ∈ range f}

Tactic:
antisymm (range_subset_iff.2 fun l => forall_mem_map.2 fun y _ => mem_range_self _)
      fun l hl => ?_

Premises used: Set.mem_range_self, Iff.mpr, List.forall_mem_map, antisymm, Set.range_subset_iff
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
β : Type u_2
f : α → β
refine :
  ∀ (l : List β) (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} l),
    l ∈ range (map f)
⊢ range (map f) = {l : List β | ∀ (x : β), x ∈ l → x ∈ range f}

Tactic:
refine antisymm (range_subset_iff.2 fun l => forall_mem_map.2 fun y _ => mem_range_self _)
      fun l hl => ?_
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
β : Type u_2
f : α → β
hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} []
⊢ [] ∈ range (map f)

Tactic:
⟨[], rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl, List.nil
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
β : Type u_2
f : α → β
hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} []
⊢ [] ∈ range (map f)

Tactic:
exact ⟨[], rfl⟩
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : β
l : List β
ihl : ∀ (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} l), l ∈ range (map f)
hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (a :: l)
cons :
  ∀ (l : List α)
    (ihl :
      ∀ (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (map f l)),
        map f l ∈ range (map f))
    (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (a :: map f l)),
    a :: map f l ∈ range (map f)
⊢ a :: l ∈ range (map f)

Tactic:
rcases ihl fun x hx => hl x <| subset_cons_self _ _ hx with ⟨l, rfl⟩

Premises used: rfl, List.subset_cons_self
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : β
l : List α
ihl :
  ∀ (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (map f l)),
    map f l ∈ range (map f)
hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (a :: map f l)
cons :
  ∀ (a : α) (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (f a :: map f l)),
    f a :: map f l ∈ range (map f)
⊢ a :: map f l ∈ range (map f)

Tactic:
rcases hl a mem_cons_self with ⟨a, rfl⟩

Premises used: List.mem_cons_self, rfl
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : List α
ihl :
  ∀ (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (map f l)),
    map f l ∈ range (map f)
a : α
hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (f a :: map f l)
⊢ f a :: map f l ∈ range (map f)

Tactic:
⟨a :: l, map_cons⟩

Premises used: List.map_cons, Set.Mem, setOf, List.cons, Exists.intro, Set.range
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : List α
ihl :
  ∀ (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (map f l)),
    map f l ∈ range (map f)
a : α
hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (f a :: map f l)
⊢ f a :: map f l ∈ range (map f)

Tactic:
exact ⟨a :: l, map_cons⟩
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : List β
hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} l
nil : ∀ (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} []), [] ∈ range (map f)
cons :
  ∀ (a : β) (l : List β)
    (ihl :
      ∀ (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} l), l ∈ range (map f))
    (hl : Membership.mem (γ := Set (List β)) {l : List β | ∀ (x : β), x ∈ l → x ∈ range f} (a :: l)),
    a :: l ∈ range (map f)
⊢ l ∈ range (map f)

Tactic:
induction l with
  | nil => exact ⟨[], rfl⟩
  | cons a l ihl =>
    rcases ihl fun x hx => hl x <| subset_cons_self _ _ hx with ⟨l, rfl⟩
    rcases hl a mem_cons_self with ⟨a, rfl⟩
    exact ⟨a :: l, map_cons⟩

Premises used: List.cons, rfl, List.nil
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
s : Set α
rw :
  Eq.{u_1 + 1} (α := Set (List α))
    {l : List α |
      ∀ (x : α),
        x ∈ l →
          Membership.mem (γ := Set α) (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) x}
    {l : List α | ∀ (x : α), x ∈ l → x ∈ s}
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := Set (List α)) {l : List α | ∀ (x : α), x ∈ l → x ∈ s} {l : List α | ∀ (x : α), x ∈ l → x ∈ s}
⊢ Eq.{u_1 + 1} (α := Set (List α)) (range (ι := List { x : α // x ∈ s }) (map (Subtype.val (p := fun (x : α) ↦ x ∈ s))))
    {l : List α | ∀ (x : α), x ∈ l → x ∈ s}

Tactic:
rw [range_list_map, Subtype.range_coe]

Premises used: Subtype.range_coe, Set.range_list_map
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
l : List α
h : ∀ (x : α), x ∈ range l.get ↔ Membership.mem (γ := Set α) {x : α | x ∈ l} x
⊢ range l.get = {x : α | x ∈ l}

Tactic:
ext x
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
l : List α
x : α
h : x ∈ range l.get ↔ x ∈ l
h₁ : x ∈ range l.get ↔ ∃ (n : Fin l.length), l.get n = x
h₂ h₃ : (∃ (y : Fin l.length), l.get y = x) ↔ ∃ (n : Fin l.length), l.get n = x
⊢ x ∈ range l.get ↔ Membership.mem (γ := Set α) {x : α | x ∈ l} x

Tactic:
rw [mem_setOf_eq, mem_iff_get, mem_range]

Premises used: Set.mem_range, List.mem_iff_get, Set.mem_setOf_eq
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
l : List α
rw :
  (range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) =
    insert none (range (some ∘ l.get))
⊢ Eq (α := Set (Option α)) (range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x)
    (insert none (some '' {x : α | x ∈ l}))

Tactic:
rw [← range_list_get, ← range_comp]

Premises used: Set.range_comp, Set.range_list_get
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
l : List α
⊢ (range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) =
    insert none (range (some ∘ l.get))

Tactic:
(range_subset_iff.2 fun n => ?_).antisymm (insert_subset_iff.2 ⟨?_, ?_⟩)

Premises used: Iff.mpr, Set.insert_subset_iff, HasSubset.Subset.antisymm, And.intro, Set.range_subset_iff
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
l : List α
refine_1 :
  ∀ (n : ℕ), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ∈ insert none (range (some ∘ l.get))
refine_2 :
  Membership.mem (γ := Set (Option α))
    (range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) none
refine_3 : range (some ∘ l.get) ⊆ range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x
⊢ (range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) =
    insert none (range (some ∘ l.get))

Tactic:
refine (range_subset_iff.2 fun n => ?_).antisymm (insert_subset_iff.2 ⟨?_, ?_⟩)

Premises used: Iff.mpr, Set.insert_subset_iff, HasSubset.Subset.antisymm, And.intro, Set.range_subset_iff
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
l : List α
n : ℕ
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ∈ insert none (range (some ∘ l.get))

Tactic:
(le_or_gt l.length n).imp getElem?_eq_none_iff.mpr
      (fun hlt => ⟨⟨_, hlt⟩, (getElem?_eq_getElem hlt).symm⟩)

Premises used: Iff.mpr, Set.insert, Set.Mem, setOf, Fin.mk, le_or_gt, List.getElem?_eq_getElem, Exists.intro, List.getElem?_eq_none_iff, Or.imp, Eq.symm, List.length
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
l : List α
n : ℕ
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ∈ insert none (range (some ∘ l.get))

Tactic:
exact (le_or_gt l.length n).imp getElem?_eq_none_iff.mpr
      (fun hlt => ⟨⟨_, hlt⟩, (getElem?_eq_getElem hlt).symm⟩)

Premises used: Iff.mpr, le_or_gt, List.getElem?_eq_none_iff, Or.imp, List.length
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
l : List α
⊢ Membership.mem (γ := Set (Option α))
    (range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) none

Tactic:
⟨_, getElem?_eq_none_iff.mpr le_rfl⟩

Premises used: Iff.mpr, le_rfl, Set.Mem, setOf, Exists.intro, List.getElem?_eq_none_iff, Set.range
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
l : List α
⊢ Membership.mem (γ := Set (Option α))
    (range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) none

Tactic:
exact ⟨_, getElem?_eq_none_iff.mpr le_rfl⟩
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
l : List α
⊢ range (some ∘ l.get) ⊆ range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x

Tactic:
range_subset_iff.2 fun k => ⟨_, getElem?_eq_getElem _⟩

Premises used: Iff.mpr, Fin.isLt, Fin.val, List.getElem?_eq_getElem, Exists.intro, Set.range_subset_iff
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
l : List α
⊢ range (some ∘ l.get) ⊆ range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x

Tactic:
exact range_subset_iff.2 fun k => ⟨_, getElem?_eq_getElem _⟩
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
l : List α
d : α
simp :
  Eq.{u_1 + 1} (α := Set α)
    (range fun (n : ℕ) ↦ (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD d)
    (range fun (x : ℕ) ↦ (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x).getD d)
⊢ Eq.{u_1 + 1} (α := Set α)
    (range fun (n : ℕ) ↦ (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD d)
    ((fun (o : Option α) ↦ o.getD d) ''
      range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x)

Tactic:
simp only [← range_comp, Function.comp_def]

Premises used: Set.range_comp, Function.comp_def
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
l : List α
d : α
⊢ Eq.{u_1 + 1} (α := Set α)
    (range fun (n : ℕ) ↦ (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD d)
    (range fun (x : ℕ) ↦ (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x).getD d)

Tactic:
rfl
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
l : List α
d : α
⊢ Eq (α := Set α)
    ((fun (o : Option α) ↦ o.getD d) ''
      range fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x)
    (insert d {x : α | x ∈ l})

Tactic:
simp only [Option.getD, range_list_getElem?, image_insert_eq, image_image, image_id']

Premises used: Set.image_image, Set.range_list_getElem?, Set.image_id', Option.getD, Set.image_insert_eq
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
inst : Inhabited α
l : List α
⊢ Eq (α := Set α) (range fun (n : ℕ) ↦ l.getD n default) (insert default {x : α | x ∈ l})

Tactic:
simp
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
β : Type u_2
l_1 : List α
c : β → α
p : α → Prop
inst : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
rw : Membership.mem (γ := Set (List α)) {l : List α | ∀ (x : α), x ∈ l → x ∈ Set.range c} l
⊢ ∃ (y : List β), map c y = l

Tactic:
rw [← Set.mem_range, Set.range_list_map]

Premises used: Set.mem_range, Set.range_list_map
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
β : Type u_2
l_1 : List α
c : β → α
p : α → Prop
inst : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
⊢ Membership.mem (γ := Set (List α)) {l : List α | ∀ (x : α), x ∈ l → x ∈ Set.range c} l

Tactic:
fun a ha => CanLift.prf a (H a ha)

Premises used: Set.Mem, setOf, Set.range, CanLift.prf
-- Module: Mathlib.Data.Set.List
Goal:
α : Type u_1
β : Type u_2
l_1 : List α
c : β → α
p : α → Prop
inst : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
⊢ Membership.mem (γ := Set (List α)) {l : List α | ∀ (x : α), x ∈ l → x ∈ Set.range c} l

Tactic:
exact fun a ha => CanLift.prf a (H a ha)

Premises used: CanLift.prf
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
⊢ memPartition f 0 = {univ}

Tactic:
rfl

Premises used: memPartition, rfl
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
⊢ memPartition f (n + 1) = {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}

Tactic:
rfl

Premises used: memPartition, rfl
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
u v : Set α
hu : u ∈ memPartition f n
hv : v ∈ memPartition f n
huv : u ≠ v
revert : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
⊢ Disjoint u v

Tactic:
revert u v
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
u v : Set α
hu : u ∈ memPartition f 0
hv : v ∈ memPartition f 0
huv : u ≠ v
⊢ u = univ

Tactic:
simp only [memPartition_zero, mem_singleton_iff] at hu hv

Premises used: memPartition_zero, Set.mem_singleton_iff
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
u v : Set α
hu : u ∈ memPartition f 0
hv : v ∈ memPartition f 0
huv : u ≠ v
hu₁ : u = univ
⊢ v = univ

Tactic:
simp only [memPartition_zero, mem_singleton_iff] at hu hv

Premises used: memPartition_zero, Set.mem_singleton_iff
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : u ≠ v
hu : u = univ
hv : v = univ
⊢ Ne.{u_1 + 1} (α := Set α) univ univ

Tactic:
rw [hu, hv] at huv
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : u ≠ v
hu : u = univ
hv : v = univ
huv₁ : Ne.{u_1 + 1} (α := Set α) univ univ
⊢ u = univ

Tactic:
rw [hu, hv] at huv
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : u ≠ v
hu : u = univ
hv : v = univ
huv₁ : Ne.{u_1 + 1} (α := Set α) univ univ
hu₁ : u = univ
⊢ v = univ

Tactic:
rw [hu, hv] at huv
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : Ne.{u_1 + 1} (α := Set α) univ univ
hu : u = univ
hv : v = univ
⊢ Disjoint u v

Tactic:
absurd rfl huv

Premises used: absurd, rfl
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : Ne.{u_1 + 1} (α := Set α) univ univ
hu : u = univ
hv : v = univ
⊢ Disjoint u v

Tactic:
exact absurd rfl huv

Premises used: absurd, rfl
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u v : Set α
hu : u ∈ memPartition f (n + 1)
hv : v ∈ memPartition f (n + 1)
huv : u ≠ v
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} u

Tactic:
rw [memPartition_succ] at hu hv

Premises used: memPartition_succ
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u v : Set α
hu : u ∈ memPartition f (n + 1)
hv : v ∈ memPartition f (n + 1)
huv : u ≠ v
hu₁ : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} u
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} v

Tactic:
rw [memPartition_succ] at hu hv

Premises used: memPartition_succ
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u v : Set α
hu : u ∈ memPartition f (n + 1)
hv : v ∈ memPartition f (n + 1)
huv : u ≠ v
hu₁ : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} u
hv₁ : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} v
⊢ u ≠ v

Tactic:
rw [memPartition_succ] at hu hv

Premises used: memPartition_succ
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u v : Set α
hu : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} u
hv : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} v
huv : u ≠ v
succ : ∀ (u' : Set α) (hu' : u' ∈ memPartition f n) (hu'_eq : u = u' ∩ f n ∨ u = u' \ f n), Disjoint u v
⊢ Disjoint u v

Tactic:
obtain ⟨u', hu', hu'_eq⟩ := hu
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u v : Set α
hv : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} v
huv : u ≠ v
u' : Set α
hu' : u' ∈ memPartition f n
hu'_eq : u = u' ∩ f n ∨ u = u' \ f n
succ : ∀ (v' : Set α) (hv' : v' ∈ memPartition f n) (hv'_eq : v = v' ∩ f n ∨ v = v' \ f n), Disjoint u v
⊢ Disjoint u v

Tactic:
obtain ⟨v', hv', hv'_eq⟩ := hv
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u v : Set α
huv : u ≠ v
u' : Set α
hu' : u' ∈ memPartition f n
hu'_eq : u = u' ∩ f n ∨ u = u' \ f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
succ : ∀ (huv : u' ∩ f n ≠ v), Disjoint (u' ∩ f n) v
succ₁ : ∀ (huv : u' \ f n ≠ v), Disjoint (u' \ f n) v
⊢ Disjoint u v

Tactic:
rcases hu'_eq with rfl | rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
v u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
huv : u' ∩ f n ≠ v
succ : ∀ (huv : u' ∩ f n ≠ v' ∩ f n), Disjoint (u' ∩ f n) (v' ∩ f n)
succ₁ : ∀ (huv : u' ∩ f n ≠ v' \ f n), Disjoint (u' ∩ f n) (v' \ f n)
⊢ Disjoint (u' ∩ f n) v

Tactic:
rcases hv'_eq with rfl | rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
v u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
huv : u' \ f n ≠ v
succ : ∀ (huv : u' \ f n ≠ v' ∩ f n), Disjoint (u' \ f n) (v' ∩ f n)
succ₁ : ∀ (huv : u' \ f n ≠ v' \ f n), Disjoint (u' \ f n) (v' \ f n)
⊢ Disjoint (u' \ f n) v

Tactic:
rcases hv'_eq with rfl | rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' ∩ f n
⊢ Disjoint (u' ∩ f n) (v' ∩ f n)

Tactic:
Disjoint.mono inter_subset_left inter_subset_left (ih hu' hv' ?_)

Premises used: Set.inter_subset_left, Disjoint.mono
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' ∩ f n
succ : u' ≠ v'
⊢ Disjoint (u' ∩ f n) (v' ∩ f n)

Tactic:
refine Disjoint.mono inter_subset_left inter_subset_left (ih hu' hv' ?_)

Premises used: Set.inter_subset_left, Disjoint.mono
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' ∩ f n
⊢ u' ≠ v'

Tactic:
fun huv' ↦ huv (huv' ▸ rfl)

Premises used: Eq.rec, Not, rfl
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' ∩ f n
⊢ u' ≠ v'

Tactic:
exact fun huv' ↦ huv (huv' ▸ rfl)
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' \ f n
⊢ Disjoint (u' ∩ f n) (v' \ f n)

Tactic:
Disjoint.mono_left inter_subset_right Set.disjoint_sdiff_right

Premises used: Disjoint.mono_left, Set.disjoint_sdiff_right, Set.inter_subset_right
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' \ f n
⊢ Disjoint (u' ∩ f n) (v' \ f n)

Tactic:
exact Disjoint.mono_left inter_subset_right Set.disjoint_sdiff_right

Premises used: Disjoint.mono_left, Set.disjoint_sdiff_right, Set.inter_subset_right
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' \ f n ≠ v' ∩ f n
⊢ Disjoint (u' \ f n) (v' ∩ f n)

Tactic:
Disjoint.mono_right inter_subset_right Set.disjoint_sdiff_left

Premises used: Set.disjoint_sdiff_left, Disjoint.mono_right, Set.inter_subset_right
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' \ f n ≠ v' ∩ f n
⊢ Disjoint (u' \ f n) (v' ∩ f n)

Tactic:
exact Disjoint.mono_right inter_subset_right Set.disjoint_sdiff_left

Premises used: Set.disjoint_sdiff_left, Disjoint.mono_right, Set.inter_subset_right