awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
mpr : ∀ (p : κ) (mp : f m ⊆ f p) (np : f n ⊆ f p), r i j
⊢ r i j

Tactic:
rcases hd m n with ⟨p, mp, np⟩
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
p : κ
mp : f m ⊆ f p
np : f n ⊆ f p
⊢ r i j

Tactic:
H p (mp hm) (np hn) hij
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
p : κ
mp : f m ⊆ f p
np : f n ⊆ f p
⊢ r i j

Tactic:
exact H p (mp hm) (np hn) hij
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
simp : ∀ ⦃x : α⦄, ∀ x_1 ∈ s, x ∈ x_1 → ∀ ⦃y : α⦄, ∀ x_2 ∈ s, y ∈ x_2 → x ≠ y → r x y
⊢ Set.Pairwise (⋃ a ∈ s, a) r

Tactic:
simp only [Set.Pairwise, mem_iUnion, exists_prop, forall_exists_index, and_imp]

Premises used: and_imp, Set.mem_iUnion, forall_exists_index, exists_prop, Set.Pairwise
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
obtain : ∀ (U : Set α) (hU : U ∈ s) (hSU : S ⊆ U) (hTU : T ⊆ U), r x y
⊢ r x y

Tactic:
obtain ⟨U, hU, hSU, hTU⟩ := hd S hS T hT
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
U : Set α
hU : U ∈ s
hSU : S ⊆ U
hTU : T ⊆ U
⊢ r x y

Tactic:
h U hU (hSU hx) (hTU hy) hne
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
U : Set α
hU : U ∈ s
hSU : S ⊆ U
hTU : T ⊆ U
⊢ r x y

Tactic:
exact h U hU (hSU hx) (hTU hy) hne
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
r : α → α → Prop
s : Set (Set α)
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : Set.Pairwise (⋃ a ∈ s, a) r
a : Set α
ha : a ∈ s
⊢ a ⊆ a

Tactic:
rfl
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
rw₂ rw₃ :
  (∀ (x : Set α) (h : x ∈ s), (↑(Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) x h) : Set α).Pairwise r) ↔
    ∀ a ∈ s, a.Pairwise r
⊢ (⋃₀ s).Pairwise r ↔ ∀ a ∈ s, a.Pairwise r

Tactic:
rw [sUnion_eq_iUnion, pairwise_iUnion hd.directed_val, SetCoe.forall]

Premises used: Set.pairwise_iUnion, Set.sUnion_eq_iUnion, DirectedOn.directed_val, SetCoe.forall
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
f : ι → α
g : ι' → Set ι
h : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) g
⊢ PairwiseDisjoint (⋃ (n : ι'), g n) f ↔ ∀ ⦃n : ι'⦄, (g n).PairwiseDisjoint f

Tactic:
pairwise_iUnion h

Premises used: Set.pairwise_iUnion, Set.PairwiseDisjoint
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
f : ι → α
s : Set (Set ι)
h : DirectedOn (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
⊢ (⋃₀ s).PairwiseDisjoint f ↔ ∀ ⦃a : Set ι⦄, a ∈ s → a.PairwiseDisjoint f

Tactic:
pairwise_sUnion h

Premises used: Set.pairwise_sUnion, Set.PairwiseDisjoint
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
⊢ ∃ (i : ι') (_ : i ∈ s), a ∈ g i

Tactic:
simp_rw [Set.mem_iUnion] at ha hb

Premises used: Set.mem_iUnion
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
⊢ ∃ (i : ι') (_ : i ∈ s), b ∈ g i

Tactic:
simp_rw [Set.mem_iUnion] at ha hb

Premises used: Set.mem_iUnion
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
obtain : ∀ (c : ι') (hc : c ∈ s) (ha : a ∈ g c), (Disjoint on f) a b
⊢ (Disjoint on f) a b

Tactic:
obtain ⟨c, hc, ha⟩ := ha
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
obtain : ∀ (d : ι') (hd : d ∈ s) (hb : b ∈ g d), (Disjoint on f) a b
⊢ (Disjoint on f) a b

Tactic:
obtain ⟨d, hd, hb⟩ := hb
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
inr : ∀ (hcd : g c ≠ g d), (Disjoint on f) a b
⊢ (Disjoint on f) a b

Tactic:
obtain hcd | hcd := eq_or_ne (g c) (g d)

Premises used: eq_or_ne
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
hcd : g c = g d
⊢ (Disjoint on f) a b

Tactic:
hg d hd (hcd ▸ ha) hb hab
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
hcd : g c = g d
⊢ (Disjoint on f) a b

Tactic:
exact hg d hd (hcd ▸ ha) hb hab
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
hcd : g c ≠ g d
⊢ (Disjoint on f) a b

Tactic:
(hs hc hd <| ne_of_apply_ne _ hcd).mono
      (le_iSup₂ (f := fun i _ => f i) a ha)
      (le_iSup₂ (f := fun i _ => f i) b hb)

Premises used: le_iSup₂, ne_of_apply_ne, Disjoint.mono
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
hcd : g c ≠ g d
⊢ (Disjoint on f) a b

Tactic:
exact (hs hc hd <| ne_of_apply_ne _ hcd).mono
      (le_iSup₂ (f := fun i _ => f i) a ha)
      (le_iSup₂ (f := fun i _ => f i) b hb)

Premises used: le_iSup₂, ne_of_apply_ne, Disjoint.mono
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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')
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')
⊢ (Disjoint on f) (i, i') (j, j')

Tactic:
rw [mem_prod] at hi hj

Premises used: Set.mem_prod
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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')
inr : ∀ (hij : i ≠ j), (Disjoint on f) (i, i') (j, j')
⊢ (Disjoint on f) (i, i') (j, j')

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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')

Tactic:
(ht hi.2 hj.2 <| (Prod.mk_right_injective _).ne_iff.1 h).mono ?_ ?_

Premises used: Function.Injective.ne_iff, And.right, Iff.mp, Prod.mk_right_injective, Disjoint.mono
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
inl₁ : f (i, j') ≤ (fun (i' : ι') ↦ (⨆ i ∈ s, f (i, i') : α)) (i, j').2
⊢ (Disjoint on f) (i, i') (i, j')

Tactic:
refine (ht hi.2 hj.2 <| (Prod.mk_right_injective _).ne_iff.1 h).mono ?_ ?_

Premises used: Function.Injective.ne_iff, And.right, Iff.mp, Prod.mk_right_injective, Disjoint.mono
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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, i').2) ≤ ⨆ i_1 ∈ s, f (i_1, (i, i').2)

Tactic:
le_iSup₂ (α := α) i hi.1

Premises used: le_iSup₂, And.left
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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')
h₁ : f (i, i') = f (i, (i, i').2)
⊢ f (i, i') ≤ (fun (i' : ι') ↦ (⨆ i ∈ s, f (i, i') : α)) (i, i').2

Tactic:
convert! le_iSup₂ (α := α) i hi.1

Premises used: le_iSup₂, And.left
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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') = f (i, (i, i').2)

Tactic:
rfl
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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, j').2) ≤ ⨆ i_1 ∈ s, f (i_1, (i, j').2)

Tactic:
le_iSup₂ (α := α) i hj.1

Premises used: le_iSup₂, And.left
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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')
h₁ : f (i, j') = f (i, (i, j').2)
⊢ f (i, j') ≤ (fun (i' : ι') ↦ (⨆ i ∈ s, f (i, i') : α)) (i, j').2

Tactic:
convert! le_iSup₂ (α := α) i hj.1

Premises used: le_iSup₂, And.left
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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') = f (i, (i, j').2)

Tactic:
rfl
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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')

Tactic:
(hs hi.1 hj.1 hij).mono ?_ ?_

Premises used: And.left, Disjoint.mono
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
inr : f (i, i') ≤ (fun (i : ι) ↦ (⨆ i' ∈ t, f (i, i') : α)) (i, i').1
inr₁ : f (j, j') ≤ (fun (i : ι) ↦ (⨆ i' ∈ t, f (i, i') : α)) (j, j').1
⊢ (Disjoint on f) (i, i') (j, j')

Tactic:
refine (hs hi.1 hj.1 hij).mono ?_ ?_

Premises used: And.left, Disjoint.mono
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
⊢ f ((i, i').1, i') ≤ ⨆ i_1 ∈ t, f ((i, i').1, i_1)

Tactic:
le_iSup₂ (α := α) i' hi.2

Premises used: le_iSup₂, And.right
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
h₁ : f (i, i') = f ((i, i').1, i')
⊢ f (i, i') ≤ (fun (i : ι) ↦ (⨆ i' ∈ t, f (i, i') : α)) (i, i').1

Tactic:
convert! le_iSup₂ (α := α) i' hi.2

Premises used: le_iSup₂, And.right
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
⊢ f (i, i') = f ((i, i').1, i')

Tactic:
rfl
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
⊢ f ((j, j').1, j') ≤ ⨆ i ∈ t, f ((j, j').1, i)

Tactic:
le_iSup₂ (α := α) j' hj.2

Premises used: le_iSup₂, And.right
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
h₁ : f (j, j') = f ((j, j').1, j')
⊢ f (j, j') ≤ (fun (i : ι) ↦ (⨆ i' ∈ t, f (i, i') : α)) (j, j').1

Tactic:
convert! le_iSup₂ (α := α) j' hj.2

Premises used: le_iSup₂, And.right
-- Module: Mathlib.Data.Set.Pairwise.Lattice
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
⊢ f (j, j') = f ((j, j').1, j')

Tactic:
rfl
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
⊢ (s ×ˢ t).PairwiseDisjoint f ↔
    (PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')) ∧
      PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')

Tactic:
⟨fun h => ⟨fun i hi j hj hij => ?_, fun i hi j hj hij => ?_⟩, fun h => h.1.prod_left h.2⟩

Premises used: Set.PairwiseDisjoint.prod_left, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
refine_1 :
  ∀ (h : (s ×ˢ t).PairwiseDisjoint f) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i ≠ j),
    onFun.{u_2 + 1, u_1 + 1, 1} (β := α) Disjoint (fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')) i j
refine_2 :
  ∀ (h : (s ×ˢ t).PairwiseDisjoint f) (i : ι') (hi : i ∈ t) (j : ι') (hj : j ∈ t) (hij : i ≠ j),
    onFun.{u_3 + 1, u_1 + 1, 1} (β := α) Disjoint (fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')) i j
⊢ (s ×ˢ t).PairwiseDisjoint f ↔
    (PairwiseDisjoint.{u_1, u_2} (α := α) s fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')) ∧
      PairwiseDisjoint.{u_1, u_3} (α := α) t fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')

Tactic:
refine
      ⟨fun h => ⟨fun i hi j hj hij => ?_, fun i hi j hj hij => ?_⟩, fun h => h.1.prod_left h.2⟩
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
refine_1 : ∀ (i_1 : ι') (i_2 : i_1 ∈ t) (i_3 : ι') (i_4 : i_3 ∈ t), Disjoint (f (i, i_1)) (f (j, i_3))
⊢ onFun.{u_2 + 1, u_1 + 1, 1} (β := α) Disjoint (fun (i : ι) ↦ ⨆ i' ∈ t, f (i, i')) i j

Tactic:
simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff]

Premises used: Function.onFun, disjoint_iSup_iff, iSup_disjoint_iff
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
refine_2 : ∀ (i_1 : ι) (i_2 : i_1 ∈ s) (i_3 : ι) (i_4 : i_3 ∈ s), Disjoint (f (i_1, i)) (f (i_3, j))
⊢ onFun.{u_3 + 1, u_1 + 1, 1} (β := α) Disjoint (fun (i' : ι') ↦ ⨆ i ∈ s, f (i, i')) i j

Tactic:
simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff]

Premises used: Function.onFun, disjoint_iSup_iff, iSup_disjoint_iff
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
i' : ι'
hi' : i' ∈ t
j' : ι'
hj' : j' ∈ t
⊢ Disjoint (f (i, i')) (f (j, j'))

Tactic:
h (mk_mem_prod hi hi') (mk_mem_prod hj hj') (ne_of_apply_ne Prod.fst hij)

Premises used: ne_of_apply_ne, Prod.fst, Set.mk_mem_prod
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
i' : ι'
hi' : i' ∈ t
j' : ι'
hj' : j' ∈ t
⊢ Disjoint (f (i, i')) (f (j, j'))

Tactic:
exact h (mk_mem_prod hi hi') (mk_mem_prod hj hj') (ne_of_apply_ne Prod.fst hij)

Premises used: ne_of_apply_ne, Prod.fst, Set.mk_mem_prod
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
i' : ι
hi' : i' ∈ s
j' : ι
hj' : j' ∈ s
⊢ Disjoint (f (i', i)) (f (j', j))

Tactic:
h (mk_mem_prod hi' hi) (mk_mem_prod hj' hj) (ne_of_apply_ne Prod.snd hij)

Premises used: ne_of_apply_ne, Set.mk_mem_prod, Prod.snd
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
i' : ι
hi' : i' ∈ s
j' : ι
hj' : j' ∈ s
⊢ Disjoint (f (i', i)) (f (j', j))

Tactic:
exact h (mk_mem_prod hi' hi) (mk_mem_prod hj' hj) (ne_of_apply_ne Prod.snd hij)

Premises used: ne_of_apply_ne, Set.mk_mem_prod, Prod.snd
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
⊢ Eq.{u_1 + 1} (α := Set α) ((⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i) (⋃ i ∈ s \ t, f i)

Tactic:
(biUnion_diff_biUnion_subset f s t).antisymm
      (iUnion₂_subset fun i hi a ha => (mem_diff _).2 ⟨mem_biUnion hi.1 ha, ?_⟩)

Premises used: Iff.mpr, Set.biUnion_diff_biUnion_subset, Set.iUnion₂_subset, Set.mem_biUnion, And.left, Set.mem_diff, HasSubset.Subset.antisymm, And.intro