awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u t : Set α
P : Partition u
ht : t ∈ P
hxt : x ∈ t
y : α
⊢ y ∈ t ↔ y ∈ P.partOf (u := u) x

Tactic:
⟨(⟨t, ht, hxt, ·⟩), fun ⟨s, hsP, hxs, hys⟩ ↦ (P.eq_of_mem_of_mem ht hsP hxt hxs) ▸ hys⟩

Premises used: _private.0.Partition.eq_partOf_of_mem.match_1, Partition.eq_of_mem_of_mem, Membership.mem, Eq.rec, And.intro, Iff.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u t : Set α
P : Partition u
ht : t ∈ P
hxt : x ∈ t
y : α
⊢ y ∈ t ↔ y ∈ P.partOf (u := u) x

Tactic:
exact ⟨(⟨t, ht, hxt, ·⟩), fun ⟨s, hsP, hxs, hys⟩ ↦ (P.eq_of_mem_of_mem ht hsP hxt hxs) ▸ hys⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
⊢ x ∈ u ↔ x ∈ P.partOf (u := u) x ∧ P.partOf (u := u) x ∈ P

Tactic:
⟨fun hx ↦ ?_, fun ⟨hx, hP⟩ ↦ subset_of_mem hP hx⟩

Premises used: Partition.subset_of_mem, Membership.mem, _private.0.Partition.mem_iff_mem_partOf_mem.match_1, Iff.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
refine : ∀ (hx : x ∈ u), x ∈ P.partOf (u := u) x ∧ P.partOf (u := u) x ∈ P
⊢ x ∈ u ↔ x ∈ P.partOf (u := u) x ∧ P.partOf (u := u) x ∈ P

Tactic:
refine ⟨fun hx ↦ ?_, fun ⟨hx, hP⟩ ↦ subset_of_mem hP hx⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
obtain : ∀ (t : Set α) (htP : t ∈ P) (hxt : x ∈ t), x ∈ P.partOf (u := u) x ∧ P.partOf (u := u) x ∈ P
⊢ x ∈ P.partOf (u := u) x ∧ P.partOf (u := u) x ∈ P

Tactic:
obtain ⟨t, htP, hxt⟩ := P.mem_iff_exists.mp hx

Premises used: Iff.mp, Partition.mem_iff_exists
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
t : Set α
htP : t ∈ P
hxt : x ∈ t
⊢ x ∈ P.partOf (u := u) x ∧ P.partOf (u := u) x ∈ P

Tactic:
P.eq_partOf_of_mem htP hxt ▸ ⟨hxt, htP⟩

Premises used: Eq.rec, And.intro, Partition.eq_partOf_of_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
t : Set α
htP : t ∈ P
hxt : x ∈ t
⊢ x ∈ P.partOf (u := u) x ∧ P.partOf (u := u) x ∈ P

Tactic:
exact P.eq_partOf_of_mem htP hxt ▸ ⟨hxt, htP⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hxu : x ∈ u
⊢ x ∈ P.partOf (u := u) x

Tactic:
(P.mem_iff_mem_partOf_mem.mp hxu).1

Premises used: And.left, Partition.mem_iff_mem_partOf_mem, Iff.mp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hxu : x ∈ u
⊢ P.partOf (u := u) x ∈ P

Tactic:
(P.mem_iff_mem_partOf_mem.mp hxu).2

Premises used: And.right, Partition.mem_iff_mem_partOf_mem, Iff.mp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u s : Set α
P : Partition u
hs : s ∈ P
⊢ P.partOf (u := u) (P.rep (u := u) (t := s) hs) = s

Tactic:
eq_partOf_of_mem hs (rep_mem hs) |>.symm

Premises used: Partition.rep_mem, Partition.eq_partOf_of_mem, Eq.symm
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u s : Set α
P : Partition u
⊢ s ∈ P ↔ ∃ x ∈ u, P.partOf (u := u) x = s

Tactic:
⟨fun hs ↦ ⟨P.rep hs, rep_mem_supp hs, partOf_rep hs⟩, fun ⟨_, hxu, h⟩ ↦ h ▸ partOf_mem hxu⟩

Premises used: Membership.mem, Eq.rec, And.intro, Partition.partOf_mem, Iff.intro, Exists.intro, Partition.rep_mem_supp, Partition.rep, _private.0.Partition.mem_iff_exists_partOf.match_1, Partition.partOf_rep
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
⊢ (P.partOf (u := u) x).Nonempty ↔ x ∈ u

Tactic:
⟨fun ⟨y, hy⟩ ↦ hy.left_mem, fun h ↦ ?_⟩

Premises used: _private.0.Partition.partOf_nonempty_iff.match_1, Membership.mem, Partition.Rel.left_mem, Iff.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
refine : ∀ (h : x ∈ u), (P.partOf (u := u) x).Nonempty
⊢ (P.partOf (u := u) x).Nonempty ↔ x ∈ u

Tactic:
refine ⟨fun ⟨y, hy⟩ ↦ hy.left_mem, fun h ↦ ?_⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
h : x ∈ u
⊢ (P.partOf (u := u) x).Nonempty

Tactic:
simpa [nonempty_iff_ne_empty] using P.ne_bot_of_mem (partOf_mem h)

Premises used: Partition.ne_bot_of_mem, Partition.partOf_mem, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
rw : P.partOf (u := u) x = ∅ ↔ ¬(P.partOf (u := u) x).Nonempty
rw₁ : Partition u
rw₂ : P.partOf (u := u) x = ∅ ↔ P.partOf (u := u) x = ∅
rw₃ : Partition u
rw₄ : P.partOf (u := u) x = ∅ ↔ P.partOf (u := u) x = ∅
rw₅ : Partition u
⊢ P.partOf (u := u) x = ∅ ↔ x ∉ u

Tactic:
rw [← partOf_nonempty_iff, not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty, Partition.partOf_nonempty_iff
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u : Set α
P : Partition u
hx : x ∈ u
hy : y ∈ u
⊢ P.Rel (s := u) x y ↔ P.partOf (u := u) x = P.partOf (u := u) y

Tactic:
⟨fun ⟨t, htP, hxt, hyt⟩ ↦ eq_partOf_of_mem (P.partOf_mem hx) ?_,
    fun h ↦ ⟨P.partOf x, P.partOf_mem hx, P.mem_partOf hx, h ▸ mem_partOf hy⟩⟩

Premises used: _private.0.Partition.rel_iff_partOf_eq_partOf_of_mem.match_1, Eq.rec, Partition.partOf, And.intro, Partition.partOf_mem, Iff.intro, Exists.intro, Partition.mem_partOf, Partition.eq_partOf_of_mem, Eq.symm, Eq
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u : Set α
P : Partition u
hx : x ∈ u
hy : y ∈ u
refine : P.Rel (s := u) x y → ∀ (t : Set α) (htP : t ∈ P) (hxt : x ∈ t) (hyt : y ∈ t), y ∈ P.partOf (u := u) x
⊢ P.Rel (s := u) x y ↔ P.partOf (u := u) x = P.partOf (u := u) y

Tactic:
refine ⟨fun ⟨t, htP, hxt, hyt⟩ ↦ eq_partOf_of_mem (P.partOf_mem hx) ?_,
    fun h ↦ ⟨P.partOf x, P.partOf_mem hx, P.mem_partOf hx, h ▸ mem_partOf hy⟩⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u : Set α
P : Partition u
hx : x ∈ u
hy : y ∈ u
h : P.Rel (s := u) x y
t : Set α
htP : t ∈ P
hxt : x ∈ t
hyt rwa rwa₁ rwa₂ rwa₃ : y ∈ t
⊢ y ∈ P.partOf (u := u) x

Tactic:
rwa [← eq_partOf_of_mem htP hxt]

Premises used: Partition.eq_partOf_of_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u : Set α
P : Partition u
⊢ P.Rel (s := u) x y ↔ ∃ (_ : x ∈ u) (_ : y ∈ u), P.partOf (u := u) x = P.partOf (u := u) y

Tactic:
grind [rel_iff_partOf_eq_partOf_of_mem, Rel.left_mem, Rel.right_mem]

Premises used: Partition.Rel.right_mem, Partition.Rel.left_mem, Partition.rel_iff_partOf_eq_partOf_of_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun (u := u) f
ha : a ∈ u
⊢ f a ∈ u

Tactic:
(hf.rel_apply ha).right_mem

Premises used: Partition.Rel.right_mem, Partition.IsRepFun.rel_apply
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
hs : u ⊆ s
a : α
haS : a ∈ s
pos : ∀ (ha : a ∈ u), f a ∈ s
neg : ∀ (ha : a ∉ u), f a ∈ s
⊢ f a ∈ s

Tactic:
by_cases ha : a ∈ u
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
hs : u ⊆ s
a : α
haS : a ∈ s
ha : a ∈ u
⊢ f a ∈ s

Tactic:
hs <| hf.apply_mem ha

Premises used: Partition.IsRepFun.apply_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
hs : u ⊆ s
a : α
haS : a ∈ s
ha : a ∈ u
⊢ f a ∈ s

Tactic:
exact hs <| hf.apply_mem ha

Premises used: Partition.IsRepFun.apply_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
hs : u ⊆ s
a : α
haS : a ∈ s
ha : a ∉ u
⊢ f a ∈ s

Tactic:
(hf.apply_of_notMem ha).symm ▸ haS

Premises used: Eq.rec, Partition.IsRepFun.apply_of_notMem, Eq.symm
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
hs : u ⊆ s
a : α
haS : a ∈ s
ha : a ∉ u
⊢ f a ∈ s

Tactic:
exact (hf.apply_of_notMem ha).symm ▸ haS
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
hs : u ⊆ s
⊢ MapsTo f s s

Tactic:
fun x h ↦ hf.image_subset hs ⟨x, h, rfl⟩

Premises used: Set.MapsTo, And.intro, Exists.intro, rfl, Partition.IsRepFun.image_subset
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
hs : Disjoint u s
⊢ MapsTo f s s

Tactic:
fun _ h ↦ (hf.apply_of_notMem <| hs.notMem_of_mem_right h).symm ▸ h

Premises used: Eq.rec, Partition.IsRepFun.apply_of_notMem, Set.MapsTo, Eq.symm, Disjoint.notMem_of_mem_right
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun (u := u) f
hs : u ⊆ s
⊢ f a ∈ s ↔ a ∈ s

Tactic:
hf.mapsTo hs |>.mem_iff <| mapsTo_of_disjoint hf hs.disjoint_compl_right

Premises used: HasSubset.Subset.disjoint_compl_right, Partition.IsRepFun.mapsTo, Set.MapsTo.mem_iff, Partition.IsRepFun.mapsTo_of_disjoint
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
ha : a ∈ u
⊢ f a = f b ↔ P.Rel (s := u) a b

Tactic:
⟨fun hab ↦ (hf.rel_apply ha).trans ?_, (hf.apply_eq_apply ·)⟩

Premises used: Partition.IsRepFun.apply_eq_apply, Partition.IsRepFun.rel_apply, Partition.Rel.trans, Iff.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
ha : a ∈ u
refine : ∀ (hab : f a = f b), P.Rel (s := u) (f a) b
⊢ f a = f b ↔ P.Rel (s := u) a b

Tactic:
refine ⟨fun hab ↦ (hf.rel_apply ha).trans ?_, (hf.apply_eq_apply ·)⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
ha : a ∈ u
hab : f a = f b
rw : P.Rel (s := u) b (f b)
⊢ P.Rel (s := u) (f a) b

Tactic:
rw [hab, P.rel_comm]

Premises used: Partition.rel_comm
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
ha : a ∈ u
hab : f a = f b
⊢ P.Rel (s := u) b (f b)

Tactic:
hf.rel_apply <| by_contra fun hb ↦ ?_

Premises used: Partition.IsRepFun.rel_apply, by_contra
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
ha : a ∈ u
hab : f a = f b
refine : ∀ (hb : b ∉ u), False
⊢ P.Rel (s := u) b (f b)

Tactic:
refine hf.rel_apply <| by_contra fun hb ↦ ?_

Premises used: Partition.IsRepFun.rel_apply, by_contra
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
ha : a ∈ u
hab : f a = f b
hb : b ∉ u
⊢ f a = b

Tactic:
rw [hf.apply_of_notMem hb] at hab

Premises used: Partition.IsRepFun.apply_of_notMem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
ha : a ∈ u
hab : f a = f b
hb : b ∉ u
hab₁ : f a = b
⊢ b ∉ u

Tactic:
rw [hf.apply_of_notMem hb] at hab

Premises used: Partition.IsRepFun.apply_of_notMem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
ha : a ∈ u
hab : f a = b
hb : b ∉ u
⊢ False

Tactic:
exact hab ▸ hb <| hf.apply_mem ha

Premises used: Partition.IsRepFun.apply_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
simp : f a = f b ↔ a ≠ b → P.Rel (s := u) a b
⊢ f a = f b ↔ a = b ∨ P.Rel (s := u) a b

Tactic:
simp only [or_iff_not_imp_left, ← ne_eq]

Premises used: ne_eq, Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
⊢ f a = f b ↔ a ≠ b → P.Rel (s := u) a b

Tactic:
⟨fun hab hne ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
refine_1 : ∀ (hab : f a = f b) (hne : a ≠ b), P.Rel (s := u) a b
refine_2 : ∀ (h : a ≠ b → P.Rel (s := u) a b), f a = f b
⊢ f a = f b ↔ a ≠ b → P.Rel (s := u) a b

Tactic:
refine ⟨fun hab hne ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
hab : f a = f b
hne : a ≠ b
refine_1 : ∀ (ha : a ∈ u), P.Rel (s := u) a b
refine_1₁ : ∀ (ha : a ∉ u), P.Rel (s := u) a b
⊢ P.Rel (s := u) a b

Tactic:
obtain (ha | ha) := em (a ∈ u)

Premises used: Membership.mem, em
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
hab : f a = f b
hne : a ≠ b
ha : a ∈ u
⊢ P.Rel (s := u) a b

Tactic:
hf.apply_eq_apply_iff_rel ha |>.mp hab

Premises used: Partition.IsRepFun.apply_eq_apply_iff_rel, Iff.mp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
hab : f a = f b
hne : a ≠ b
ha : a ∈ u
⊢ P.Rel (s := u) a b

Tactic:
exact hf.apply_eq_apply_iff_rel ha |>.mp hab

Premises used: Partition.IsRepFun.apply_eq_apply_iff_rel, Iff.mp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
hab : f a = f b
hne : a ≠ b
ha : a ∉ u
refine_1 : ∀ (hb : b ∈ u), P.Rel (s := u) a b
refine_1₁ : ∀ (hb : b ∉ u), P.Rel (s := u) a b
⊢ P.Rel (s := u) a b

Tactic:
obtain (hb | hb) := em (b ∈ u)

Premises used: Membership.mem, em
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
hab : f a = f b
hne : a ≠ b
ha : a ∉ u
hb : b ∈ u
⊢ P.Rel (s := u) a b

Tactic:
(hf.apply_eq_apply_iff_rel hb |>.mp hab.symm).symm

Premises used: Partition.Rel.symm, Partition.IsRepFun.apply_eq_apply_iff_rel, Iff.mp, Eq.symm
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
hab : f a = f b
hne : a ≠ b
ha : a ∉ u
hb : b ∈ u
⊢ P.Rel (s := u) a b

Tactic:
exact (hf.apply_eq_apply_iff_rel hb |>.mp hab.symm).symm

Premises used: Partition.Rel.symm, Partition.IsRepFun.apply_eq_apply_iff_rel, Iff.mp, Eq.symm
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
hab : f a = f b
hne : a ≠ b
ha : a ∉ u
hb : b ∉ u
⊢ a = b

Tactic:
rw [hf.apply_of_notMem ha, hf.apply_of_notMem hb] at hab

Premises used: Partition.IsRepFun.apply_of_notMem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
hab : f a = f b
hne : a ≠ b
ha : a ∉ u
hb : b ∉ u
hab₁ : a = b
⊢ a ≠ b

Tactic:
rw [hf.apply_of_notMem ha, hf.apply_of_notMem hb] at hab

Premises used: Partition.IsRepFun.apply_of_notMem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
hab : f a = f b
hne : a ≠ b
ha : a ∉ u
hb : b ∉ u
hab₁ : a = b
hne₁ : a ≠ b
⊢ a ∉ u

Tactic:
rw [hf.apply_of_notMem ha, hf.apply_of_notMem hb] at hab

Premises used: Partition.IsRepFun.apply_of_notMem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
hab : f a = f b
hne : a ≠ b
ha : a ∉ u
hb : b ∉ u
hab₁ : a = b
hne₁ : a ≠ b
ha₁ : a ∉ u
⊢ b ∉ u

Tactic:
rw [hf.apply_of_notMem ha, hf.apply_of_notMem hb] at hab

Premises used: Partition.IsRepFun.apply_of_notMem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
hab : a = b
hne : a ≠ b
ha : a ∉ u
hb : b ∉ u
⊢ P.Rel (s := u) a b

Tactic:
contradiction
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
h : a ≠ b → P.Rel (s := u) a b
refine_2 : ∀ (h : a ≠ a → P.Rel (s := u) a a), f a = f a
refine_2₁ : ∀ (hne : a ≠ b), f a = f b
⊢ f a = f b

Tactic:
obtain rfl | hne := eq_or_ne a b

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun (u := u) f
h : a ≠ a → P.Rel (s := u) a a
⊢ f a = f a

Tactic:
rfl
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
h : a ≠ b → P.Rel (s := u) a b
hne : a ≠ b
⊢ f a = f b

Tactic:
hf.apply_eq_apply (h hne)

Premises used: Partition.IsRepFun.apply_eq_apply
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
h : a ≠ b → P.Rel (s := u) a b
hne : a ≠ b
⊢ f a = f b

Tactic:
exact hf.apply_eq_apply (h hne)

Premises used: Partition.IsRepFun.apply_eq_apply
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
a : α
⊢ (∀ (x : α), f a = f x ↔ a = x) ∨ ∀ (x : α), f a = f x ↔ P.Rel (s := u) a x

Tactic:
(em (a ∈ u)).elim (fun ha ↦ Or.inr fun b ↦ ?_) (fun ha ↦ Or.inl fun b ↦ ?_)

Premises used: Membership.mem, em, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
a : α
refine_1 : ∀ (ha : a ∈ u) (b : α), f a = f b ↔ P.Rel (s := u) a b
refine_2 : ∀ (ha : a ∉ u) (b : α), f a = f b ↔ a = b
⊢ (∀ (x : α), f a = f x ↔ a = x) ∨ ∀ (x : α), f a = f x ↔ P.Rel (s := u) a x

Tactic:
refine (em (a ∈ u)).elim (fun ha ↦ Or.inr fun b ↦ ?_) (fun ha ↦ Or.inl fun b ↦ ?_)

Premises used: Membership.mem, em, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
a : α
ha : a ∈ u
b : α
refine_1 refine_1₁ : P.Rel (s := u) a b ↔ P.Rel (s := u) a b
⊢ f a = f b ↔ P.Rel (s := u) a b

Tactic:
rw [hf.apply_eq_apply_iff_rel ha]

Premises used: Partition.IsRepFun.apply_eq_apply_iff_rel
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
a : α
ha : a ∉ u
b : α
refine_2 : a = f b ↔ a = b
⊢ f a = f b ↔ a = b

Tactic:
rw [hf.apply_of_notMem ha]

Premises used: Partition.IsRepFun.apply_of_notMem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
a : α
ha : a ∉ u
b : α
refine_2 : a = f b → a = b
refine_2₁ : a = b → a = f b
⊢ a = f b ↔ a = b

Tactic:
constructor
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
b : α
ha : f b ∉ u
⊢ f b = b

Tactic:
hf.apply_of_notMem <| hf.apply_mem_iff le_rfl |>.not.mp ha

Premises used: le_rfl, Iff.not, Partition.IsRepFun.apply_mem_iff, Partition.IsRepFun.apply_of_notMem, Iff.mp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
b : α
ha : f b ∉ u
⊢ f b = b

Tactic:
exact hf.apply_of_notMem <| hf.apply_mem_iff le_rfl |>.not.mp ha

Premises used: le_rfl, Iff.not, Partition.IsRepFun.apply_mem_iff, Partition.IsRepFun.apply_of_notMem, Iff.mp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
a : α
ha : a ∉ u
⊢ a = f a

Tactic:
hf.apply_of_notMem ha |>.symm

Premises used: Partition.IsRepFun.apply_of_notMem, Eq.symm
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
a : α
ha : a ∉ u
⊢ a = f a

Tactic:
exact hf.apply_of_notMem ha |>.symm

Premises used: Partition.IsRepFun.apply_of_notMem, Eq.symm
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
inl : ∀ (h1 : ∀ (x : α), f a = f x ↔ a = x), f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel (s := u) a b
inr :
  ∀ (h2 : ∀ (x : α), f a = f x ↔ P.Rel (s := u) a x),
    f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel (s := u) a b
⊢ f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel (s := u) a b

Tactic:
obtain h1 | h2 := hf.forall_apply_eq_apply_iff a

Premises used: Partition.IsRepFun.forall_apply_eq_apply_iff
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
h1 : ∀ (x : α), f a = f x ↔ a = x
⊢ f a = f b → (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel (s := u) a b

Tactic:
grind
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
h1 : ∀ (x : α), f a = f x ↔ a = x
inl : (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel (s := u) a b → f a = f b
⊢ f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel (s := u) a b

Tactic:
refine ⟨by grind, ?_⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
h1 : ∀ (x : α), f a = f x ↔ a = x
h : a = b ∧ ∀ (c : α), f a = f c ↔ a = c
⊢ f a = f b

Tactic:
congrArg _ h.1

Premises used: congrArg, And.left
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
h1 : ∀ (x : α), f a = f x ↔ a = x
h : a = b ∧ ∀ (c : α), f a = f c ↔ a = c
⊢ f a = f b

Tactic:
exact congrArg _ h.1

Premises used: congrArg, And.left
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
h1 : ∀ (x : α), f a = f x ↔ a = x
h : P.Rel (s := u) a b
⊢ f a = f b

Tactic:
hf.apply_eq_apply h

Premises used: Partition.IsRepFun.apply_eq_apply
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
h1 : ∀ (x : α), f a = f x ↔ a = x
h : P.Rel (s := u) a b
⊢ f a = f b

Tactic:
exact hf.apply_eq_apply h

Premises used: Partition.IsRepFun.apply_eq_apply
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun (u := u) f
h2 : ∀ (x : α), f a = f x ↔ P.Rel (s := u) a x
⊢ f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel (s := u) a b

Tactic:
grind
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun (u := u) f
inl : ∀ (ha : a ∈ u), f (f a) = f a
inr : ∀ (ha : a ∉ u), f (f a) = f a
⊢ f (f a) = f a

Tactic:
obtain (ha | ha) := em (a ∈ u)

Premises used: Membership.mem, em
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun (u := u) f
ha : a ∈ u
inl : P.Rel (s := u) a (f a)
⊢ f (f a) = f a

Tactic:
rw [eq_comm, hf.apply_eq_apply_iff_rel ha]

Premises used: eq_comm, Partition.IsRepFun.apply_eq_apply_iff_rel
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun (u := u) f
ha : a ∈ u
⊢ P.Rel (s := u) a (f a)

Tactic:
hf.rel_apply ha

Premises used: Partition.IsRepFun.rel_apply
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun (u := u) f
ha : a ∈ u
⊢ P.Rel (s := u) a (f a)

Tactic:
exact hf.rel_apply ha

Premises used: Partition.IsRepFun.rel_apply
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun (u := u) f
ha : a ∉ u
⊢ f (f a) = f a

Tactic:
simp_rw [hf.apply_of_notMem ha]

Premises used: Partition.IsRepFun.apply_of_notMem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f g : α → α
hf : P.IsRepFun (u := u) f
hg : P.IsRepFun (u := u) g
x : α
inl : ∀ (hx : x ∈ u), f (g x) = f x
inr : ∀ (hx : x ∉ u), f (g x) = f x
⊢ f (g x) = f x

Tactic:
obtain (hx | hx) := em (x ∈ u)

Premises used: Membership.mem, em
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
f g : α → α
hf : P.IsRepFun (u := u) f
hg : P.IsRepFun (u := u) g
x : α
hx : x ∈ u
⊢ f (g x) = f x

Tactic:
hf.apply_eq_apply (hg.rel_apply hx).symm

Premises used: Partition.IsRepFun.apply_eq_apply, Partition.IsRepFun.rel_apply, Partition.Rel.symm