awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 diff_subset diff_subset (ih hu' hv' ?_)

Premises used: Set.diff_subset, 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 diff_subset diff_subset (ih hu' hv' ?_)

Premises used: Set.diff_subset, 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 : ℕ
zero : ∀ {u v : Set α} (hu : u ∈ memPartition f 0) (hv : v ∈ memPartition f 0) (huv : u ≠ v), Disjoint u v
succ :
  ∀ (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), Disjoint u v
⊢ ∀ {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v), Disjoint u v

Tactic:
induction n with
  | zero =>
    intro u v hu hv huv
    simp only [memPartition_zero, mem_singleton_iff] at hu hv
    rw [hu, hv] at huv
    exact absurd rfl huv
  | succ n ih =>
    intro u v hu hv huv
    rw [memPartition_succ] at hu hv
    obtain ⟨u', hu', hu'_eq⟩ := hu
    obtain ⟨v', hv', hv'_eq⟩ := hv
    rcases hu'_eq with rfl | rfl <;> rcases hv'_eq with rfl | rfl
    · refine Disjoint.mono inter_subset_left inter_subset_left (ih hu' hv' ?_)
      exact fun huv' ↦ huv (huv' ▸ rfl)
    · exact Disjoint.mono_left inter_subset_right Set.disjoint_sdiff_right
    · exact Disjoint.mono_right inter_subset_right Set.disjoint_sdiff_left
    · refine Disjoint.mono diff_subset diff_subset (ih hu' hv' ?_)
      exact fun huv' ↦ huv (huv' ▸ rfl)

Premises used: memPartition_zero, Disjoint.mono_left, Set.mem_singleton_iff, Set.disjoint_sdiff_left, Set.disjoint_sdiff_right, memPartition_succ, Disjoint.mono_right, rfl, Set.inter_subset_right
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
⊢ ⋃₀ memPartition f 0 = univ

Tactic:
simp
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
succ :
  ∀ (x : α),
    Membership.mem (γ := Set α) (⋃₀ {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}) x ↔
      Membership.mem (γ := Set α) univ x
⊢ Eq.{u_1 + 1} (α := Set α) (⋃₀ {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}) univ

Tactic:
ext x
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
⊢ x ∈ ⋃₀ memPartition f n

Tactic:
simp [ih]
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
⊢ x ∈ ⋃₀ memPartition f n

Tactic:
have : x ∈ ⋃₀ memPartition f n := by simp [ih]
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
this : x ∈ ⋃₀ memPartition f n
succ :
  ∀ (this : ∃ t ∈ memPartition f n, x ∈ t),
    ∃ (t : Set α),
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t
⊢ Membership.mem (γ := Set α) (⋃₀ {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}) x ↔
    Membership.mem (γ := Set α) univ x

Tactic:
simp only [mem_sUnion, mem_univ,
      iff_true] at this ⊢

Premises used: iff_true, Set.mem_univ, Set.mem_sUnion
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
this : ∃ t ∈ memPartition f n, x ∈ t
succ :
  ∀ (t : Set α) (ht : t ∈ memPartition f n) (hxt : x ∈ t),
    ∃ (t : Set α),
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t
⊢ ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t

Tactic:
obtain ⟨t, ht, hxt⟩ := this
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
pos :
  ∀ (hxf : x ∈ f n),
    ∃ (t : Set α),
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t
neg :
  ∀ (hxf : x ∉ f n),
    ∃ (t : Set α),
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t
⊢ ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t

Tactic:
by_cases hxf : x ∈ f n
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
hxf : x ∈ f n
⊢ ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t

Tactic:
⟨t ∩ f n, ⟨t, ht, Or.inl rfl⟩, hxt, hxf⟩

Premises used: Inter.inter, And.intro, Exists.intro, Or.inl, rfl
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
hxf : x ∈ f n
⊢ ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t

Tactic:
exact ⟨t ∩ f n, ⟨t, ht, Or.inl rfl⟩, hxt, hxf⟩
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
hxf : x ∉ f n
⊢ ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t

Tactic:
⟨t \ f n, ⟨t, ht, Or.inr rfl⟩, hxt, hxf⟩

Premises used: SDiff.sdiff, And.intro, Exists.intro, Or.inr, rfl
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
hxf : x ∉ f n
⊢ ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} t ∧ x ∈ t

Tactic:
exact ⟨t \ f n, ⟨t, ht, Or.inr rfl⟩, hxt, hxf⟩
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
zero : ⋃₀ memPartition f 0 = univ
succ : ∀ (n : ℕ) (ih : ⋃₀ memPartition f n = univ), ⋃₀ memPartition f (n + 1) = univ
⊢ ⋃₀ memPartition f n = univ

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [memPartition_succ]
    ext x
    have : x ∈ ⋃₀ memPartition f n := by simp [ih]
    simp only [mem_sUnion, mem_univ,
      iff_true] at this ⊢
    obtain ⟨t, ht, hxt⟩ := this
    by_cases hxf : x ∈ f n
    · exact ⟨t ∩ f n, ⟨t, ht, Or.inl rfl⟩, hxt, hxf⟩
    · exact ⟨t \ f n, ⟨t, ht, Or.inr rfl⟩, hxt, hxf⟩

Premises used: iff_true, Set.mem_univ, memPartition_succ, Set.mem_sUnion
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
⊢ (memPartition f 0).Finite

Tactic:
simp
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
⊢ Finite.{u_1 + 1} (↑(memPartition f n) : Type u_1)

Tactic:
have : Finite (memPartition f n) := Set.finite_coe_iff.mp ih
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite.{u_1 + 1} (↑(memPartition f n) : Type u_1)
succ : Finite.{u_1 + 1} (↑(⋃ i ∈ memPartition f n, {a : Set α | a = i ∩ f n} ∪ {a : Set α | a = i \ f n}) : Type u_1)
⊢ Finite.{u_1 + 1} (↑{s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} : Type u_1)

Tactic:
simp_rw [setOf_exists, ← exists_prop, setOf_exists, setOf_or]

Premises used: Set.setOf_exists, exists_prop, Set.setOf_or
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite.{u_1 + 1} (↑(memPartition f n) : Type u_1)
⊢ Finite.{u_1 + 1} (↑(⋃ i ∈ memPartition f n, {a : Set α | a = i ∩ f n} ∪ {a : Set α | a = i \ f n}) : Type u_1)

Tactic:
Finite.Set.finite_biUnion (memPartition f n) _ (fun u _ ↦ ?_)

Premises used: memPartition, Finite.Set.finite_biUnion
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite.{u_1 + 1} (↑(memPartition f n) : Type u_1)
succ : ∀ u ∈ memPartition f n, Finite.{u_1 + 1} (↑({a : Set α | a = u ∩ f n} ∪ {a : Set α | a = u \ f n}) : Type u_1)
⊢ Finite.{u_1 + 1} (↑(⋃ i ∈ memPartition f n, {a : Set α | a = i ∩ f n} ∪ {a : Set α | a = i \ f n}) : Type u_1)

Tactic:
refine Finite.Set.finite_biUnion (memPartition f n) _ (fun u _ ↦ ?_)

Premises used: memPartition, Finite.Set.finite_biUnion
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite.{u_1 + 1} (↑(memPartition f n) : Type u_1)
u : Set α
h : u ∈ memPartition f n
⊢ Set.Finite.{u_1} (α := Set α) ({a : Set α | a = u ∩ f n} ∪ {a : Set α | a = u \ f n})

Tactic:
simp
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
zero : (memPartition f 0).Finite
succ : ∀ (n : ℕ) (ih : (memPartition f n).Finite), (memPartition f (n + 1)).Finite
⊢ (memPartition f n).Finite

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [memPartition_succ]
    have : Finite (memPartition f n) := Set.finite_coe_iff.mp ih
    rw [← Set.finite_coe_iff]
    simp_rw [setOf_exists, ← exists_prop, setOf_exists, setOf_or]
    refine Finite.Set.finite_biUnion (memPartition f n) _ (fun u _ ↦ ?_)
    rw [Set.finite_coe_iff]
    simp

Premises used: Set.setOf_exists, exists_prop, Set.finite_coe_iff, memPartition_succ, Set.setOf_or
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
⊢ Finite.{u_1 + 1} (↑(memPartition f n) : Type u_1)

Tactic:
Set.finite_coe_iff.mp (finite_memPartition _ _)

Premises used: finite_memPartition, Set.Finite, Set.finite_coe_iff, Iff.mp
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
⊢ memPartitionSet f 0 a = univ

Tactic:
simp [memPartitionSet]

Premises used: memPartitionSet
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
inst : Decidable (a ∈ f n)
⊢ memPartitionSet f (n + 1) a = if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n

Tactic:
simp [memPartitionSet]

Premises used: memPartitionSet
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
⊢ memPartitionSet f 0 a ∈ memPartition f 0

Tactic:
simp [memPartitionSet]

Premises used: memPartitionSet
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
    (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n)

Tactic:
⟨memPartitionSet f n a, ?_⟩

Premises used: Set.Mem, setOf, memPartitionSet, Exists.intro
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
succ :
  memPartitionSet f n a ∈ memPartition f n ∧
    ((if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a ∩ f n ∨
      (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a \ f n)
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
    (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n)

Tactic:
refine ⟨memPartitionSet f n a, ?_⟩
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
pos :
  a ∈ f n →
    memPartitionSet f n a ∈ memPartition f n ∧
      (memPartitionSet f n a ∩ f n = memPartitionSet f n a ∩ f n ∨
        memPartitionSet f n a ∩ f n = memPartitionSet f n a \ f n)
neg :
  a ∉ f n →
    memPartitionSet f n a ∈ memPartition f n ∧
      (memPartitionSet f n a \ f n = memPartitionSet f n a ∩ f n ∨
        memPartitionSet f n a \ f n = memPartitionSet f n a \ f n)
⊢ memPartitionSet f n a ∈ memPartition f n ∧
    ((if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a ∩ f n ∨
      (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a \ f n)

Tactic:
split_ifs
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
h : a ∈ f n
⊢ memPartitionSet f n a ∈ memPartition f n ∧
    (memPartitionSet f n a ∩ f n = memPartitionSet f n a ∩ f n ∨
      memPartitionSet f n a ∩ f n = memPartitionSet f n a \ f n)

Tactic:
simp [ih]
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
h : a ∉ f n
⊢ memPartitionSet f n a ∈ memPartition f n ∧
    (memPartitionSet f n a \ f n = memPartitionSet f n a ∩ f n ∨
      memPartitionSet f n a \ f n = memPartitionSet f n a \ f n)

Tactic:
simp [ih]
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
succ : (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) ∈ memPartition f (n + 1)
succ₁ succ₂ succ₃ :
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
    (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n)
succ₄ :
  memPartitionSet f n a ∈ memPartition f n ∧
    ((if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a ∩ f n ∨
      (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a \ f n)
⊢ memPartitionSet f (n + 1) a ∈ memPartition f (n + 1)

Tactic:
classical
    rw [memPartitionSet_succ, memPartition_succ]
    refine ⟨memPartitionSet f n a, ?_⟩
    split_ifs <;> simp [ih]

Premises used: memPartitionSet_succ, memPartition_succ
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
zero : memPartitionSet f 0 a ∈ memPartition f 0
succ : ∀ (n : ℕ) (ih : memPartitionSet f n a ∈ memPartition f n), memPartitionSet f (n + 1) a ∈ memPartition f (n + 1)
⊢ memPartitionSet f n a ∈ memPartition f n

Tactic:
induction n with
  | zero => simp [memPartitionSet]
  | succ n ih =>
    classical
    rw [memPartitionSet_succ, memPartition_succ]
    refine ⟨memPartitionSet f n a, ?_⟩
    split_ifs <;> simp [ih]

Premises used: memPartitionSet_succ, memPartitionSet, memPartition_succ
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
⊢ a ∈ memPartitionSet f 0 a

Tactic:
simp [memPartitionSet]

Premises used: memPartitionSet
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
pos : ∀ (h : a ∈ f n), a ∈ memPartitionSet f n a ∩ f n
neg : ∀ (h : a ∉ f n), a ∈ memPartitionSet f n a \ f n
⊢ a ∈ if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
h : a ∈ f n
⊢ a ∈ memPartitionSet f n a ∩ f n

Tactic:
⟨ih, h⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
h : a ∈ f n
⊢ a ∈ memPartitionSet f n a ∩ f n

Tactic:
exact ⟨ih, h⟩
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
h : a ∉ f n
⊢ a ∈ memPartitionSet f n a \ f n

Tactic:
⟨ih, h⟩

Premises used: Set.Mem, Set.diff, setOf, And.intro
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
h : a ∉ f n
⊢ a ∈ memPartitionSet f n a \ f n

Tactic:
exact ⟨ih, h⟩
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
succ succ₁ succ₂ : a ∈ if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n
⊢ a ∈ memPartitionSet f (n + 1) a

Tactic:
classical
    rw [memPartitionSet_succ]
    split_ifs with h <;> exact ⟨ih, h⟩

Premises used: memPartitionSet_succ
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
zero : a ∈ memPartitionSet f 0 a
succ : ∀ (n : ℕ) (ih : a ∈ memPartitionSet f n a), a ∈ memPartitionSet f (n + 1) a
⊢ a ∈ memPartitionSet f n a

Tactic:
induction n with
  | zero => simp [memPartitionSet]
  | succ n ih =>
    classical
    rw [memPartitionSet_succ]
    split_ifs with h <;> exact ⟨ih, h⟩

Premises used: memPartitionSet_succ, memPartitionSet
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
⊢ memPartitionSet f n a = s ↔ a ∈ s

Tactic:
⟨fun h ↦ h ▸ mem_memPartitionSet f n a, fun h ↦ ?_⟩

Premises used: Eq.rec, mem_memPartitionSet, Iff.intro
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
refine : ∀ (h : a ∈ s), memPartitionSet f n a = s
⊢ memPartitionSet f n a = s ↔ a ∈ s

Tactic:
refine ⟨fun h ↦ h ▸ mem_memPartitionSet f n a, fun h ↦ ?_⟩
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
by_contra : ∀ (h_ne : ¬memPartitionSet f n a = s), False
⊢ memPartitionSet f n a = s

Tactic:
by_contra h_ne
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
⊢ Disjoint s (memPartitionSet f n a)

Tactic:
have h_disj : Disjoint s (memPartitionSet f n a) :=
    disjoint_memPartition f n hs (memPartitionSet_mem f n a) (Ne.symm h_ne)
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ False

Tactic:
absurd h_disj ?_

Premises used: absurd
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
refine : ¬Disjoint s (memPartitionSet f n a)
⊢ False

Tactic:
refine absurd h_disj ?_

Premises used: absurd
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
rw : (s ∩ memPartitionSet f n a).Nonempty
⊢ ¬Disjoint s (memPartitionSet f n a)

Tactic:
rw [not_disjoint_iff_nonempty_inter]

Premises used: Set.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ (s ∩ memPartitionSet f n a).Nonempty

Tactic:
⟨a, h, mem_memPartitionSet f n a⟩

Premises used: mem_memPartitionSet, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ (s ∩ memPartitionSet f n a).Nonempty

Tactic:
exact ⟨a, h, mem_memPartitionSet f n a⟩
-- Module: Mathlib.Data.Set.MemPartition
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
ha : a ∈ s
⊢ memPartitionSet f n a = s

Tactic:
(memPartitionSet_eq_iff a hs).mpr ha

Premises used: Iff.mpr, memPartitionSet_eq_iff
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst : Preorder α
inst_1 : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
rw : f₁ a ≤ f₁ b
⊢ f₂ a ≤ f₂ b

Tactic:
rw [← h ha, ← h hb]
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst : Preorder α
inst_1 : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₁ a ≤ f₁ b

Tactic:
h₁ ha hb hab
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst : Preorder α
inst_1 : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₁ a ≤ f₁ b

Tactic:
exact h₁ ha hb hab
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst : Preorder α
inst_1 : Preorder β
h₁ : AntitoneOn f₁ s
h : EqOn f₁ f₂ s
⊢ AntitoneOn f₂ s

Tactic:
h₁.dual_right.congr h

Premises used: MonotoneOn.congr, AntitoneOn.dual_right, AntitoneOn
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst : Preorder α
inst_1 : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
rw : f₁ a < f₁ b
⊢ f₂ a < f₂ b

Tactic:
rw [← h ha, ← h hb]
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst : Preorder α
inst_1 : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₁ a < f₁ b

Tactic:
h₁ ha hb hab
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst : Preorder α
inst_1 : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₁ a < f₁ b

Tactic:
exact h₁ ha hb hab
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst : Preorder α
inst_1 : Preorder β
h₁ : StrictAntiOn f₁ s
h : EqOn f₁ f₂ s
⊢ StrictAntiOn f₂ s

Tactic:
h₁.dual_right.congr h

Premises used: StrictMonoOn.congr, StrictAntiOn, StrictAntiOn.dual_right
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst : Preorder α
inst_1 : Preorder β
h : EqOn f₁ f₂ s
⊢ MonotoneOn f₁ s ↔ MonotoneOn f₂ s

Tactic:
⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩

Premises used: MonotoneOn.congr, Iff.intro, Set.EqOn.symm
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst : Preorder α
inst_1 : Preorder β
h : EqOn f₁ f₂ s
⊢ AntitoneOn f₁ s ↔ AntitoneOn f₂ s

Tactic:
⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩

Premises used: Iff.intro, AntitoneOn.congr, Set.EqOn.symm
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst : Preorder α
inst_1 : Preorder β
h : EqOn f₁ f₂ s
⊢ StrictMonoOn f₁ s ↔ StrictMonoOn f₂ s

Tactic:
⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩

Premises used: StrictMonoOn.congr, Iff.intro, Set.EqOn.symm
-- Module: Mathlib.Data.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst : Preorder α
inst_1 : Preorder β
h : EqOn f₁ f₂ s
⊢ StrictAntiOn f₁ s ↔ StrictAntiOn f₂ s

Tactic:
⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩

Premises used: StrictAntiOn.congr, Iff.intro, Set.EqOn.symm