awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
⊢ ∃! y : α, y ∈ Q ∧ x ≤ y
have obtain : ∀ (y : α) (hy : y ∈ Q) (hxy : x ≤ y), ∃! y : α, y ∈ Q ∧ x ≤ y
Tactic: obtain ⟨y, hy, hxy⟩ := h hx
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
⊢ ∃! y : α, y ∈ Q ∧ x ≤ y
have refine : ∀ (z : α), (fun (y : α) ↦ y ∈ Q ∧ x ≤ y) z → ∀ (hz : z ∈ Q) (hxz : x ≤ z), ¬Disjoint z y
Tactic: refine ⟨y, ⟨hy, hxy⟩, fun z ⟨hz, hxz⟩ ↦ Q.eq_of_not_disjoint hz hy ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (hypothesis)
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
z : α
h_1 : (fun (y : α) ↦ y ∈ Q ∧ x ≤ y) z
hz : z ∈ Q
hxz : x ≤ z
⊢ ¬Disjoint z y
have this : x ≠ ⊥
Tactic: have := P.ne_bot_of_mem hx
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
z : α
h_1 : (fun (y : α) ↦ y ∈ Q ∧ x ≤ y) z
hz : z ∈ Q
hxz : x ≤ z
this : x ≠ ⊥
⊢ ¬Disjoint z y
have contrapose : ∀ (this : Disjoint z y), x = ⊥
Tactic: contrapose this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
a : α
⊢ Membership.mem (γ := Partition s) ⊤ a ↔ a = s ∧ a ≠ ⊥
have rw : Membership.mem (γ := Partition s) (removeBot {s} sorry sorry) a ↔ a = s ∧ a ≠ ⊥
Tactic: rw [top_def, mem_removeBot, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
a : α
rw : Membership.mem (γ := Partition s) (removeBot {s} ⋯ ⋯) a ↔ a = s ∧ a ≠ ⊥
⊢ Membership.mem (γ := Partition s) ⊤ a ↔ a = s ∧ a ≠ ⊥
have rw₁ : Membership.mem (γ := Set α) {s} a ∧ a ≠ ⊥ ↔ a = s ∧ a ≠ ⊥
Tactic: rw [top_def, mem_removeBot, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
a : α
rw : Membership.mem (γ := Partition s) (removeBot {s} ⋯ ⋯) a ↔ a = s ∧ a ≠ ⊥
rw₁ : Membership.mem (γ := Set α) {s} a ∧ a ≠ ⊥ ↔ a = s ∧ a ≠ ⊥
⊢ Membership.mem (γ := Partition s) ⊤ a ↔ a = s ∧ a ≠ ⊥
have rw₂ : a = s ∧ a ≠ ⊥ ↔ a = s ∧ a ≠ ⊥
Tactic: rw [top_def, mem_removeBot, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q : Partition s
⊢ _root_.sSupIndep.{u_2} (α := α) {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
have rw : PairwiseDisjoint.{u_2, u_2} (α := α) {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} id
Tactic: rw [sSupIndep_iff_pairwiseDisjoint]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q : Partition s
⊢ sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = s
have suffices : sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = sSup (↑P : Set α) ⊓ sSup (↑Q : Set α)
Tactic: suffices sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = sSup P ⊓ sSup Q by simpa
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q : Partition s
⊢ sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = sSup (↑P : Set α) ⊓ sSup (↑Q : Set α)
have rw : Eq.{u_2 + 1} (α := α) (sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}) (⨆ p ∈ (↑P : Set α) ×ˢ (↑Q : Set α), p.1 ⊓ p.2)
Tactic: rw [sSup_inf_sSup]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q : Partition s
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}) (⨆ p ∈ (↑P : Set α) ×ˢ (↑Q : Set α), p.1 ⊓ p.2)
have refine_1 : LE.le.{u_2} (α := α) (sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}) (⨆ p ∈ (↑P : Set α) ×ˢ (↑Q : Set α), p.1 ⊓ p.2)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q : Partition s
refine_1 :
  LE.le.{u_2} (α := α) (sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}) (⨆ p ∈ (↑P : Set α) ×ˢ (↑Q : Set α), p.1 ⊓ p.2)
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}) (⨆ p ∈ (↑P : Set α) ×ˢ (↑Q : Set α), p.1 ⊓ p.2)
have refine_2 : LE.le.{u_2} (α := α) (⨆ p ∈ (↑P : Set α) ×ˢ (↑Q : Set α), p.1 ⊓ p.2) (sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q})
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q : Partition s
a : α
ha : a ∈ removeBot {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} ⋯ ⋯
⊢ ∃ y ∈ P, a ≤ y
have obtain : ∀ (p : α) (hp : p ∈ P) (q : α) (hq : q ∈ Q) (h : p ⊓ q ∉ {⊥}), ∃ y ∈ P, p ⊓ q ≤ y
Tactic: obtain ⟨⟨p, hp, q, hq, rfl⟩, h⟩ := ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q : Partition s
a : α
ha : a ∈ removeBot {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} ⋯ ⋯
⊢ ∃ y ∈ Q, a ≤ y
have obtain : ∀ (p : α) (hp : p ∈ P) (q : α) (hq : q ∈ Q) (h : p ⊓ q ∉ {⊥}), ∃ y ∈ Q, p ⊓ q ≤ y
Tactic: obtain ⟨⟨p, hp, q, hq, rfl⟩, h⟩ := ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
⊢ ∃ y ∈ removeBot {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y
have have : ∀ (q : α) (hq : q ∈ Q ∧ a ≤ q), ∃ y ∈ removeBot {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} sorry sorry, a ≤ y
Tactic: have ⟨q, hq⟩ := hQ ha
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
⊢ ∃ y ∈ removeBot {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y
have have : ∀ (r : α) (hr : r ∈ R ∧ a ≤ r), ∃ y ∈ removeBot {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} sorry sorry, a ≤ y
Tactic: have ⟨r, hr⟩ := hR ha
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
r : α
hr : r ∈ R ∧ a ≤ r
⊢ ∃ y ∈ removeBot {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y
have refine_1 : Membership.mem (γ := Set α) {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} (q ⊓ r)
Tactic: refine ⟨q ⊓ r, ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
r : α
hr : r ∈ R ∧ a ≤ r
refine_1 : Membership.mem (γ := Set α) {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} (q ⊓ r)
⊢ ∃ y ∈ removeBot {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y
have refine_2 : q ⊓ r ∉ {⊥}
Tactic: refine ⟨q ⊓ r, ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
r : α
hr : r ∈ R ∧ a ≤ r
refine_1 : Membership.mem (γ := Set α) {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} (q ⊓ r)
refine_2 : q ⊓ r ∉ {⊥}
⊢ ∃ y ∈ removeBot {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y
have refine_3 : a ≤ q ⊓ r
Tactic: refine ⟨q ⊓ r, ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
⊢ x ∈ u ↔ ∃ t ∈ P, x ∈ t
have refine : ∀ (hx : x ∈ u), ∃ t ∈ P, x ∈ t
Tactic: refine ⟨fun hx ↦ ?_, fun ⟨t, htP, hxt⟩ ↦ subset_of_mem htP hxt⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
⊢ ∃ t ∈ P, x ∈ t
have rwa : ∀ (hx : x ∈ ⋃₀ (↑P : Set (Set α))), ∃ t ∈ P, x ∈ t
Tactic: rwa [← P.sUnion_eq, mem_sUnion] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
rwa : ∀ (hx : x ∈ ⋃₀ (↑P : Set (Set α))), ∃ t ∈ P, x ∈ t
⊢ ∃ t ∈ P, x ∈ t
have rwa₁ : ∀ (hx : ∃ t ∈ (↑P : Set (Set α)), x ∈ t), ∃ t ∈ P, x ∈ t
Tactic: rwa [← P.sUnion_eq, mem_sUnion] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
⊢ x ∈ u ↔ ∃! t : Set α, t ∈ P ∧ x ∈ t
have refine : ∀ (hx : x ∈ u), ∃! t : Set α, t ∈ P ∧ x ∈ t
Tactic: refine ⟨fun hx ↦ ?_, fun ⟨_, ⟨htP, hxt⟩, _⟩ ↦ subset_of_mem htP hxt⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (hypothesis)
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
⊢ ∃! t : Set α, t ∈ P ∧ x ∈ t
have hx₁ : ∃ t ∈ (↑P : Set (Set α)), x ∈ t
Tactic: rw [← P.sUnion_eq, mem_sUnion] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : ∃ t ∈ (↑P : Set (Set α)), x ∈ t
⊢ ∃! t : Set α, t ∈ P ∧ x ∈ t
have obtain : ∀ (t : Set α) (ht : t ∈ (↑P : Set (Set α))) (hxt : x ∈ t), ∃! t : Set α, t ∈ P ∧ x ∈ t
Tactic: obtain ⟨t, ht, hxt⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
hSP : S ⊆ (↑P : Set (Set α))
⊢ t ⊆ ⋃₀ S ∧ t ∈ P ↔ t ∈ S
have refine : t ⊆ ⋃₀ S ∧ t ∈ P → ∀ (htsu : t ⊆ ⋃₀ S) (htP : t ∈ P), t ∈ S
Tactic: refine ⟨fun ⟨htsu, htP⟩ ↦ ?_, fun htS ↦ ⟨subset_sUnion_of_mem htS, hSP htS⟩⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
hSP : S ⊆ (↑P : Set (Set α))
h : t ⊆ ⋃₀ S ∧ t ∈ P
htsu : t ⊆ ⋃₀ S
htP : t ∈ P
⊢ t ∈ S
have obtain : ∀ (x : α) (hxt : x ∈ t), t ∈ S
Tactic: obtain ⟨x, hxt⟩ := nonempty_of_mem htP
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
hSP : S ⊆ (↑P : Set (Set α))
h : t ⊆ ⋃₀ S ∧ t ∈ P
htsu : t ⊆ ⋃₀ S
htP : t ∈ P
x : α
hxt : x ∈ t
⊢ t ∈ S
have obtain : ∀ (s : Set α) (hsS : s ∈ S) (hxs : x ∈ s), t ∈ S
Tactic: obtain ⟨s, hsS, hxs⟩ := htsu hxt
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
ht : t ∈ P
hSP : S ⊆ P.parts (s := u)
⊢ t ⊆ ⋃₀ S ↔ t ∈ S
have rw : t ⊆ ⋃₀ S ↔ t ⊆ ⋃₀ S ∧ t ∈ P
Tactic: rw [← subset_sUnion_and_mem_iff_mem hSP]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P Q : Partition u
⊢ P.Rel (s := u) ≤ Q.Rel (s := u) ↔ P ≤ Q
have refine_1 : ∀ (h : P.Rel (s := u) ≤ Q.Rel (s := u)) (S : Set α) (hS : S ∈ P), ∃ y ∈ Q, S ≤ y
Tactic: refine ⟨fun h S hS ↦ ?_, fun h a b ⟨t, ht, ha, hb⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P Q : Partition u
refine_1 : ∀ (h : P.Rel (s := u) ≤ Q.Rel (s := u)) (S : Set α) (hS : S ∈ P), ∃ y ∈ Q, S ≤ y
⊢ P.Rel (s := u) ≤ Q.Rel (s := u) ↔ P ≤ Q
have refine_2 : ∀ (h : P ≤ Q) (a b : α), P.Rel (s := u) a b → ∀ (t : Set α) (ht : t ∈ P) (ha : a ∈ t) (hb : b ∈ t), Q.Rel (s := u) a b
Tactic: refine ⟨fun h S hS ↦ ?_, fun h a b ⟨t, ht, ha, hb⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P.Rel (s := u) ≤ Q.Rel (s := u)
S : Set α
hS : S ∈ P
⊢ ∃ y ∈ Q, S ≤ y
have refine_1 : ∀ (x : α) (hxS : x ∈ S), ∃ y ∈ Q, S ≤ y
Tactic: obtain ⟨x, hxS⟩ := nonempty_of_mem hS
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P.Rel (s := u) ≤ Q.Rel (s := u)
S : Set α
hS : S ∈ P
x : α
hxS : x ∈ S
⊢ ∃ y ∈ Q, S ≤ y
have refine_1 : ∀ (T : Set α) (hT : T ∈ Q) (hxT : x ∈ T), ∃ y ∈ Q, S ≤ y
Tactic: obtain ⟨T, hT, hxT, -⟩ := h x x ⟨S, hS, hxS, hxS⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P.Rel (s := u) ≤ Q.Rel (s := u)
S : Set α
hS : S ∈ P
x : α
hxS : x ∈ S
T : Set α
hT : T ∈ Q
hxT : x ∈ T
⊢ ∃ y ∈ Q, S ≤ y
have refine_1 : ∀ (a : α) (haS : a ∈ S), a ∈ T
Tactic: refine ⟨T, hT, fun a haS ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P.Rel (s := u) ≤ Q.Rel (s := u)
S : Set α
hS : S ∈ P
x : α
hxS : x ∈ S
T : Set α
hT : T ∈ Q
hxT : x ∈ T
a : α
haS : a ∈ S
⊢ a ∈ T
have refine_1 : ∀ (T' : Set α) (hT' : T' ∈ Q) (haT' : a ∈ T') (hxT' : x ∈ T'), a ∈ T
Tactic: obtain ⟨T', hT', haT', hxT'⟩ := h a x ⟨S, hS, haS, hxS⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P ≤ Q
a b : α
h_1 : P.Rel (s := u) a b
t : Set α
ht : t ∈ P
ha : a ∈ t
hb : b ∈ t
⊢ Q.Rel (s := u) a b
have refine_2 : ∀ (t' : Set α) (ht' : t' ∈ Q) (htt' : t ≤ t'), Q.Rel (s := u) a b
Tactic: obtain ⟨t', ht', htt'⟩ := h ht
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P ≤ Q
a b : α
h_1 : P.Rel (s := u) a b
t : Set α
ht : t ∈ P
ha : a ∈ t
hb : b ∈ t
t' : Set α
ht' : t' ∈ Q
htt' : t ≤ t'
w : Set α
left : t' ∈ Q
⊢ Q.Rel (s := u) a b
have left₁ : a ∈ t'
Tactic: use t', ht', htt' ha, htt' hb
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P ≤ Q
a b : α
h_1 : P.Rel (s := u) a b
t : Set α
ht : t ∈ P
ha : a ∈ t
hb : b ∈ t
t' : Set α
ht' : t' ∈ Q
htt' : t ≤ t'
w : Set α
left : t' ∈ Q
left₁ : a ∈ t'
⊢ Q.Rel (s := u) a b
have right : b ∈ t'
Tactic: use t', ht', htt' ha, htt' hb
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
x y : α
u t : Set α
P : Partition u
h : P.Rel (s := u) x y
ht : t ∈ P
⊢ x ∈ t ↔ y ∈ t
have obtain : ∀ (t_1 : Set α) (ht' : t_1 ∈ P) (hx : x ∈ t_1) (hy : y ∈ t_1), x ∈ t ↔ y ∈ t
Tactic: obtain ⟨t, ht', hx, hy⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
⊢ P.Rel (s := u) x x ↔ x ∈ u
have refine : ∀ (hx : x ∈ u), P.Rel (s := u) x x
Tactic: refine ⟨fun ⟨t, ht, hxP, _⟩ ↦ subset_of_mem ht hxP, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
⊢ P.Rel (s := u) x x
have obtain : ∀ (t : Set α) (ht : t ∈ P) (hxt : x ∈ t), P.Rel (s := u) x x
Tactic: obtain ⟨t, ⟨ht, hxt⟩, -⟩ := P.mem_iff_unique.mp hx
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
x y : α
u : Set α
P : Partition u
h : P.Rel (s := u) x y
⊢ x ∈ u
have obtain : ∀ (t : Set α) (htP : t ∈ P) (hxt : x ∈ t), x ∈ u
Tactic: obtain ⟨t, htP, hxt, -⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
x : α
u t : Set α
P : Partition u
ht : t ∈ P
hxt : x ∈ t
⊢ t = P.partOf (u := u) x
have h : ∀ (y : α), y ∈ t ↔ y ∈ P.partOf (u := u) x
Tactic: ext y
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
⊢ x ∈ u ↔ x ∈ P.partOf (u := u) x ∧ P.partOf (u := u) x ∈ P
have refine : ∀ (hx : 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⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
⊢ x ∈ P.partOf (u := u) x ∧ P.partOf (u := u) x ∈ P
have obtain : ∀ (t : Set α) (htP : t ∈ P) (hxt : x ∈ t), x ∈ P.partOf (u := u) x ∧ P.partOf (u := u) x ∈ P
Tactic: obtain ⟨t, htP, hxt⟩ := P.mem_iff_exists.mp hx
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
⊢ (P.partOf (u := u) x).Nonempty ↔ x ∈ u
have refine : ∀ (h : x ∈ u), (P.partOf (u := u) x).Nonempty
Tactic: refine ⟨fun ⟨y, hy⟩ ↦ hy.left_mem, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
⊢ P.partOf (u := u) x = ∅ ↔ x ∉ u
have rw : P.partOf (u := u) x = ∅ ↔ ¬(P.partOf (u := u) x).Nonempty
Tactic: rw [← partOf_nonempty_iff, not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ P.partOf (u := u) x = ∅ ↔ x ∉ u
have rw₂ : P.partOf (u := u) x = ∅ ↔ P.partOf (u := u) x = ∅
Tactic: rw [← partOf_nonempty_iff, not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
have refine : P.Rel (s := u) x y → ∀ (t : Set α) (htP : t ∈ P) (hxt : x ∈ t) (hyt : y ∈ t), y ∈ P.partOf (u := u) x
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⟩⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
hs : u ⊆ s
a : α
haS : a ∈ s
⊢ f a ∈ s
have pos : ∀ (ha : a ∈ u), f a ∈ s
Tactic: by_cases ha : a ∈ u
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ f a ∈ s
have neg : ∀ (ha : a ∉ u), f a ∈ s
Tactic: by_cases ha : a ∈ u
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
have refine : ∀ (hab : f a = f b), P.Rel (s := u) (f a) b
Tactic: refine ⟨fun hab ↦ (hf.rel_apply ha).trans ?_, (hf.apply_eq_apply ·)⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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) (f a) b
have rw : P.Rel (s := u) b (f b)
Tactic: rw [hab, P.rel_comm]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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)
have refine : ∀ (hb : b ∉ u), False
Tactic: refine hf.rel_apply <| by_contra fun hb ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (hypothesis)
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
⊢ False
have hab₁ : f a = b
Tactic: rw [hf.apply_of_notMem hb] at hab
Cleared hypotheses: hab, hb
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
have simp : f a = f b ↔ a ≠ b → P.Rel (s := u) a b
Tactic: simp only [or_iff_not_imp_left, ← ne_eq]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
have refine_1 : ∀ (hab : f a = f b) (hne : a ≠ b), P.Rel (s := u) a b
Tactic: refine ⟨fun hab hne ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ f a = f b ↔ a ≠ b → P.Rel (s := u) a b
have refine_2 : ∀ (h : a ≠ b → P.Rel (s := u) a b), f a = f b
Tactic: refine ⟨fun hab hne ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ P.Rel (s := u) a b
have refine_1 : ∀ (ha : a ∈ u), P.Rel (s := u) a b
Tactic: obtain (ha | ha) := em (a ∈ u)
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ P.Rel (s := u) a b
have refine_1₁ : ∀ (ha : a ∉ u), P.Rel (s := u) a b
Tactic: obtain (ha | ha) := em (a ∈ u)
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
have refine_1 : ∀ (hb : b ∈ u), P.Rel (s := u) a b
Tactic: obtain (hb | hb) := em (b ∈ u)
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ P.Rel (s := u) a b
have refine_1₁ : ∀ (hb : b ∉ u), P.Rel (s := u) a b
Tactic: obtain (hb | hb) := em (b ∈ u)
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (hypothesis)
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
have hab₁ : a = b
Tactic: rw [hf.apply_of_notMem ha, hf.apply_of_notMem hb] at hab
Cleared hypotheses: hab, hne, ha, hb
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ f a = f b
have refine_2 : ∀ (h : a ≠ a → P.Rel (s := u) a a), f a = f a
Tactic: obtain rfl | hne := eq_or_ne a b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ f a = f b
have refine_2₁ : ∀ (hne : a ≠ b), f a = f b
Tactic: obtain rfl | hne := eq_or_ne a b
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
have refine_1 : ∀ (ha : a ∈ u) (b : α), f a = f b ↔ P.Rel (s := u) a b
Tactic: refine (em (a ∈ u)).elim (fun ha ↦ Or.inr fun b ↦ ?_) (fun ha ↦ Or.inl fun b ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
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
⊢ (∀ (x : α), f a = f x ↔ a = x) ∨ ∀ (x : α), f a = f x ↔ P.Rel (s := u) a x
have refine_2 : ∀ (ha : a ∉ u) (b : α), f a = f b ↔ a = b
Tactic: refine (em (a ∈ u)).elim (fun ha ↦ Or.inr fun b ↦ ?_) (fun ha ↦ Or.inl fun b ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
a : α
ha : a ∈ u
b : α
⊢ f a = f b ↔ P.Rel (s := u) a b
have refine_1 : P.Rel (s := u) a b ↔ P.Rel (s := u) a b
Tactic: rw [hf.apply_eq_apply_iff_rel ha]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun (u := u) f
a : α
ha : a ∉ u
b : α
⊢ f a = f b ↔ a = b
have refine_2 : a = f b ↔ a = b
Tactic: rw [hf.apply_of_notMem ha]