awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
refine_1 :
  ∀ (ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s) (x : α × β)
    (hx : x ∈ s ×ˢ t) (y : α × β) (hy : y ∈ s ×ˢ t) (h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y), x = y
⊢ (PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s) ↔
    InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)
have refine_2 : ∀ (ht : InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)) (x : β) (hx : x ∈ t) (y : β) (hy : y ∈ t) (h : x ≠ y),
  onFun.{u_2 + 1, u_3 + 1, 1} (β := Set γ) Disjoint (fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s) x y
Tactic: refine ⟨fun ht x hx y hy (h : f _ _ = _) => ?_, fun ht x hx y hy h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
this : x.2 = y.2
⊢ Eq.{u_3 + 1} (α := γ) ((fun (p : α × β) ↦ f p.1 p.2) y) ((fun (a : α) ↦ f a x.2) y.1)
have rw : Eq.{u_3 + 1} (α := γ) ((fun (p : α × β) ↦ f p.1 p.2) y) ((fun (a : α) ↦ f a y.2) y.1)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
⊢ x = y
have refine_1 : x.2 = y.2
Tactic: suffices x.2 = y.2 by exact Prod.ext (hf _ hx.2 <| h.trans <| by rw [this]) this
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
⊢ x.2 = y.2
have refine_1 : Membership.mem (γ := Set γ) ((fun (a : α) ↦ f a y.2) '' s) (f x.1 x.2)
Tactic: refine ht.elim hx.2 hy.2 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.1, ?_⟩)
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
⊢ Membership.mem (γ := Set γ) ((fun (a : α) ↦ f a y.2) '' s) (f x.1 x.2)
have refine_1 : Membership.mem (γ := Set γ) ((fun (a : α) ↦ f a y.2) '' s) ((fun (p : α × β) ↦ f p.1 p.2) y)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ onFun.{u_2 + 1, u_3 + 1, 1} (β := Set γ) Disjoint (fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s) x y
have refine_2 : LE.le.{u_3} (α := Set γ)
  ((fun (b : β) ↦ ((fun (a : α) ↦ f a b) '' s : Set γ)) x ⊓ (fun (b : β) ↦ ((fun (a : α) ↦ f a b) '' s : Set γ)) y) ⊥
Tactic: refine disjoint_iff_inf_le.mpr ?_
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (hypothesis)
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
have h₁ : ¬∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ∀ (t : Set α), t ≤ f i → t ≤ f j → t ≤ ⊥
Tactic: change ¬ ∀ i, i ∈ s → ∀ j, j ∈ s → i ≠ j → ∀ t, t ≤ f i → t ≤ f j → t ≤ ⊥ at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (hypothesis)
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ¬∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ∀ (t : Set α), t ≤ f i → t ≤ f j → t ≤ ⊥
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
have h₁ : ∃ (x : ι),
  ∃ (h : x ∈ s),
    ∃ (x_1 : ι), ∃ (h : x_1 ∈ s), ∃ (h : x ≠ x_1), ∃ (x_2 : Set α), ∃ (h : x_2 ≤ f x), ∃ (x : x_2 ≤ f x_1), ¬x_2 ≤ ⊥
Tactic: simp only [not_forall] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h :
  ∃ (x : ι),
    ∃ (h : x ∈ s),
      ∃ (x_1 : ι), ∃ (h : x_1 ∈ s), ∃ (h : x ≠ x_1), ∃ (x_2 : Set α), ∃ (h : x_2 ≤ f x), ∃ (x : x_2 ≤ f x_1), ¬x_2 ≤ ⊥
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
have obtain : ∀ (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (h_ne : i ≠ j) (t : Set α) (hfi : t ≤ f i) (hfj : t ≤ f j) (ht : ¬t ≤ ⊥),
  ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
Tactic: obtain ⟨i, hi, j, hj, h_ne, t, hfi, hfj, ht⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ≤ f i
hfj : t ≤ f j
ht : ¬t ≤ ⊥
⊢ t.Nonempty
have rwa : ∀ (ht : ¬t = ⊥), t.Nonempty
Tactic: rwa [le_bot_iff, bot_eq_empty, ← Ne, ← nonempty_iff_ne_empty] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ≤ f i
hfj : t ≤ f j
ht : ¬t ≤ ⊥
rwa : ∀ (ht : ¬t = ⊥), t.Nonempty
⊢ t.Nonempty
have rwa₁ : ∀ (ht : ¬t = ∅), t.Nonempty
Tactic: rwa [le_bot_iff, bot_eq_empty, ← Ne, ← nonempty_iff_ne_empty] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ≤ f i
hfj : t ≤ f j
ht : ¬t ≤ ⊥
rwa : ∀ (ht : ¬t = ⊥), t.Nonempty
rwa₁ : ∀ (ht : ¬t = ∅), t.Nonempty
⊢ t.Nonempty
have rwa₂ : ∀ (ht : t ≠ ∅), t.Nonempty
Tactic: rwa [le_bot_iff, bot_eq_empty, ← Ne, ← nonempty_iff_ne_empty] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ≤ f i
hfj : t ≤ f j
ht : ¬t ≤ ⊥
rwa : ∀ (ht : ¬t = ⊥), t.Nonempty
rwa₁ : ∀ (ht : ¬t = ∅), t.Nonempty
rwa₂ : ∀ (ht : t ≠ ∅), t.Nonempty
⊢ t.Nonempty
have rwa₃ : ∀ (ht : t.Nonempty), t.Nonempty
Tactic: rwa [le_bot_iff, bot_eq_empty, ← Ne, ← nonempty_iff_ne_empty] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (hypothesis)
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ≤ f i
hfj : t ≤ f j
ht : ¬t ≤ ⊥
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
have ht₁ : t.Nonempty
Tactic: replace ht : t.Nonempty := by
    rwa [le_bot_iff, bot_eq_empty, ← Ne, ← nonempty_iff_ne_empty] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ≤ f i
hfj : t ≤ f j
ht : t.Nonempty
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
have obtain : ∀ (x : α) (hx : x ∈ t), ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
Tactic: obtain ⟨x, hx⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
inst : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
have obtain : ∀ (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hne : i ≠ j) (x : α) (hx₁ : x ∈ f i) (hx₂ : x ∈ f j),
  ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
Tactic: obtain ⟨i, hi, j, hj, hne, x, hx₁, hx₂⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
inst : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
have inl : ∀ (h_lt : i < j), ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
Tactic: rcases lt_or_lt_iff_ne.mpr hne with h_lt | h_lt
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
inst : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
inl : ∀ (h_lt : i < j), ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
have inr : ∀ (h_lt : j < i), ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
Tactic: rcases lt_or_lt_iff_ne.mpr hne with h_lt | h_lt
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (hypothesis)
Goal:
α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ∃ (i : ι), ∃ (j : ι), i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
have h₁ : ¬Set.Pairwise univ (Disjoint on f)
Tactic: rw [← pairwise_univ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬Set.Pairwise univ (Disjoint on f)
⊢ ∃ (i : ι), ∃ (j : ι), i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
have obtain : ∀ (i : ι) (_hi : Membership.mem (γ := Set ι) univ i) (j : ι) (_hj : Membership.mem (γ := Set ι) univ j)
  (h : i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j), ∃ (i : ι), ∃ (j : ι), i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
Tactic: obtain ⟨i, _hi, j, _hj, h⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (hypothesis)
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder ι
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ∃ (i : ι), ∃ (j : ι), i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
have h₁ : ¬Set.Pairwise univ (Disjoint on f)
Tactic: rw [← pairwise_univ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Basic (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder ι
f : ι → Set α
h : ¬Set.Pairwise univ (Disjoint on f)
⊢ ∃ (i : ι), ∃ (j : ι), i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
have obtain : ∀ (i : ι) (_hi : Membership.mem (γ := Set ι) univ i) (j : ι) (_hj : Membership.mem (γ := Set ι) univ j)
  (h : i < j ∧ ∃ (x : α), x ∈ f i ∩ f j), ∃ (i : ι), ∃ (j : ι), i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
Tactic: obtain ⟨i, _hi, j, _hj, h⟩ := exists_lt_mem_inter_of_not_pairwiseDisjoint h
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
⊢ Set.Pairwise (⋃ (n : κ), f n) r ↔ ∀ (n : κ), (f n).Pairwise r
have mp : Set.Pairwise (⋃ (n : κ), f n) r → ∀ (n : κ), (f n).Pairwise r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
mp : Set.Pairwise (⋃ (n : κ), f n) r → ∀ (n : κ), (f n).Pairwise r
⊢ Set.Pairwise (⋃ (n : κ), f n) r ↔ ∀ (n : κ), (f n).Pairwise r
have mpr : (∀ (n : κ), (f n).Pairwise r) → Set.Pairwise (⋃ (n : κ), f n) r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : Membership.mem (γ := Set α) (⋃ (n : κ), f n) i
j : α
hj : Membership.mem (γ := Set α) (⋃ (n : κ), f n) j
hij : i ≠ j
⊢ r i j
have mpr : ∀ (m : κ) (hm : i ∈ f m), r i j
Tactic: rcases mem_iUnion.1 hi with ⟨m, hm⟩
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : Membership.mem (γ := Set α) (⋃ (n : κ), f n) i
j : α
hj : Membership.mem (γ := Set α) (⋃ (n : κ), f n) j
hij : i ≠ j
m : κ
hm : i ∈ f m
⊢ r i j
have mpr : ∀ (n : κ) (hn : j ∈ f n), r i j
Tactic: rcases mem_iUnion.1 hj with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : Membership.mem (γ := Set α) (⋃ (n : κ), f n) i
j : α
hj : Membership.mem (γ := Set α) (⋃ (n : κ), f n) j
hij : i ≠ j
m : κ
hm : i ∈ f m
n : κ
hn : j ∈ f n
⊢ r i j
have mpr : ∀ (p : κ) (mp : f m ⊆ f p) (np : f n ⊆ f p), r i j
Tactic: rcases hd m n with ⟨p, mp, np⟩
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
⊢ Set.Pairwise (⋃ a ∈ s, a) r
have simp : ∀ ⦃x : α⦄, ∀ x_1 ∈ s, x ∈ x_1 → ∀ ⦃y : α⦄, ∀ x_2 ∈ s, y ∈ x_2 → x ≠ y → r x y
Tactic: simp only [Set.Pairwise, mem_iUnion, exists_prop, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
S : Set α
hS : S ∈ s
hx : x ∈ S
y : α
T : Set α
hT : T ∈ s
hy : y ∈ T
hne : x ≠ y
⊢ r x y
have obtain : ∀ (U : Set α) (hU : U ∈ s) (hSU : S ⊆ U) (hTU : T ⊆ U), r x y
Tactic: obtain ⟨U, hU, hSU, hTU⟩ := hd S hS T hT
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set (Set α)
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
⊢ (⋃₀ s).Pairwise r ↔ ∀ a ∈ s, a.Pairwise r
have rw : Set.Pairwise (⋃ (i : (↑s : Type u_1)), (↑i : Set α)) r ↔ ∀ a ∈ s, a.Pairwise r
Tactic: rw [sUnion_eq_iUnion, pairwise_iUnion hd.directed_val, SetCoe.forall]
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set (Set α)
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
rw : Set.Pairwise (⋃ (i : (↑s : Type u_1)), (↑i : Set α)) r ↔ ∀ a ∈ s, a.Pairwise r
⊢ (⋃₀ s).Pairwise r ↔ ∀ a ∈ s, a.Pairwise r
have rw₁ : (∀ (n : { x : Set α // x ∈ s }), (↑n : Set α).Pairwise r) ↔ ∀ a ∈ s, a.Pairwise r
Tactic: rw [sUnion_eq_iUnion, pairwise_iUnion hd.directed_val, SetCoe.forall]
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set (Set α)
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
rw : Set.Pairwise (⋃ (i : (↑s : Type u_1)), (↑i : Set α)) r ↔ ∀ a ∈ s, a.Pairwise r
rw₁ : (∀ (n : { x : Set α // x ∈ s }), (↑n : Set α).Pairwise r) ↔ ∀ a ∈ s, a.Pairwise r
⊢ (⋃₀ s).Pairwise r ↔ ∀ a ∈ s, a.Pairwise r
have rw₂ : (∀ (x : Set α) (h : x ∈ s), (↑(Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) x h) : Set α).Pairwise r) ↔
  ∀ a ∈ s, a.Pairwise r
Tactic: rw [sUnion_eq_iUnion, pairwise_iUnion hd.directed_val, SetCoe.forall]
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a : ι
ha : Membership.mem (γ := Set ι) (⋃ i ∈ s, g i) a
b : ι
hb : Membership.mem (γ := Set ι) (⋃ i ∈ s, g i) b
hab : a ≠ b
⊢ (Disjoint on f) a b
have ha₁ : ∃ (i : ι') (_ : i ∈ s), a ∈ g i
Tactic: simp_rw [Set.mem_iUnion] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a : ι
ha : Membership.mem (γ := Set ι) (⋃ i ∈ s, g i) a
b : ι
hb : Membership.mem (γ := Set ι) (⋃ i ∈ s, g i) b
hab : a ≠ b
ha₁ : ∃ (i : ι') (_ : i ∈ s), a ∈ g i
⊢ (Disjoint on f) a b
have hb₁ : ∃ (i : ι') (_ : i ∈ s), b ∈ g i
Tactic: simp_rw [Set.mem_iUnion] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
ha : ∃ (i : ι') (_ : i ∈ s), a ∈ g i
hb : ∃ (i : ι') (_ : i ∈ s), b ∈ g i
⊢ (Disjoint on f) a b
have obtain : ∀ (c : ι') (hc : c ∈ s) (ha : a ∈ g c), (Disjoint on f) a b
Tactic: obtain ⟨c, hc, ha⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
hb : ∃ (i : ι') (_ : i ∈ s), b ∈ g i
c : ι'
hc : c ∈ s
ha : a ∈ g c
⊢ (Disjoint on f) a b
have obtain : ∀ (d : ι') (hd : d ∈ s) (hb : b ∈ g d), (Disjoint on f) a b
Tactic: obtain ⟨d, hd, hb⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
⊢ (Disjoint on f) a b
have inl : ∀ (hcd : g c = g d), (Disjoint on f) a b
Tactic: obtain hcd | hcd := eq_or_ne (g c) (g d)
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
inl : ∀ (hcd : g c = g d), (Disjoint on f) a b
⊢ (Disjoint on f) a b
have inr : ∀ (hcd : g c ≠ g d), (Disjoint on f) a b
Tactic: obtain hcd | hcd := eq_or_ne (g c) (g d)
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')
ht : PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
j : ι
j' : ι'
hj : (j, j') ∈ s ×ˢ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')
have rw : ∀ (hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t) (j : ι) (j' : ι') (hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t) (h : (i, i') ≠ (j, j')),
  (Disjoint on f) (i, i') (j, j')
Tactic: rw [mem_prod] at hi hj
Cleared hypotheses: hi, j, j', hj, h
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')
ht : PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')
have inl : ∀ (hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t) (h : (i, i') ≠ (i, j')), (Disjoint on f) (i, i') (i, j')
Tactic: obtain rfl | hij := eq_or_ne i j
Cleared hypotheses: j, hj, h
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')
ht : PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
inl : ∀ (hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t) (h : (i, i') ≠ (i, j')), (Disjoint on f) (i, i') (i, j')
⊢ (Disjoint on f) (i, i') (j, j')
have inr : ∀ (hij : i ≠ j), (Disjoint on f) (i, i') (j, j')
Tactic: obtain rfl | hij := eq_or_ne i j
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')
ht : PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ (Disjoint on f) (i, i') (i, j')
have inl : f (i, i') ≤ (fun (i' : ι') ↦ (⨆ i ∈ s, f (i, i') : α)) (i, i').2
Tactic: refine (ht hi.2 hj.2 <| (Prod.mk_right_injective _).ne_iff.1 h).mono ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')
ht : PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
inl : f (i, i') ≤ (fun (i' : ι') ↦ (⨆ i ∈ s, f (i, i') : α)) (i, i').2
⊢ (Disjoint on f) (i, i') (i, j')
have inl₁ : f (i, j') ≤ (fun (i' : ι') ↦ (⨆ i ∈ s, f (i, i') : α)) (i, j').2
Tactic: refine (ht hi.2 hj.2 <| (Prod.mk_right_injective _).ne_iff.1 h).mono ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')
ht : PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, i') ≤ (fun (i' : ι') ↦ (⨆ i ∈ s, f (i, i') : α)) (i, i').2
have h₁ : f (i, i') = f (i, (i, i').2)
Tactic: convert! le_iSup₂ (α := α) i hi.1
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')
ht : PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, j') ≤ (fun (i' : ι') ↦ (⨆ i ∈ s, f (i, i') : α)) (i, j').2
have h₁ : f (i, j') = f (i, (i, j').2)
Tactic: convert! le_iSup₂ (α := α) i hj.1
-- Lean 4 proof step from Mathlib.Data.Set.Pairwise.Lattice (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')
ht : PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ (Disjoint on f) (i, i') (j, j')
have inr : f (i, i') ≤ (fun (i : ι) ↦ (⨆ i' ∈ t, f (i, i') : α)) (i, i').1
Tactic: refine (hs hi.1 hj.1 hij).mono ?_ ?_