case mp
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)

case mpr
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)
constructor
case mp
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
⊢ x ≤ ⊥
case mp
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)
intro h i x hf hg
case mp.refine'_1
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
x✝¹ : ι
x✝ : x✝¹ ≠ i
⊢ ?mp.refine'_2 x✝¹ ≤ f x✝¹

case mp.refine'_2
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
⊢ (i : ι) → α' i

case mp.refine'_3
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
x✝¹ : ι
x✝ : x✝¹ ≠ i
⊢ ?mp.refine'_2 x✝¹ ≤ g x✝¹
case mp
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
⊢ x ≤ ⊥
refine' (update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => _⟩)
  (update_le_iff.mpr ⟨hg, fun _ _ => _⟩)).1
no goals
case mp.refine'_1
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
x✝¹ : ι
x✝ : x✝¹ ≠ i
⊢ ?mp.refine'_2 x✝¹ ≤ f x✝¹
exact bot_le
no goals
case mp.refine'_3
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
x✝¹ : ι
x✝ : x✝¹ ≠ i
⊢ ⊥ ≤ g x✝¹
exact bot_le
case mpr
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : ∀ (i : ι), Disjoint (f i) (g i)
x : (i : ι) → α' i
hf : x ≤ f
hg : x ≤ g
i : ι
⊢ x i ≤ ⊥ i
case mpr
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g
intro h x hf hg i
no goals
case mpr
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : ∀ (i : ι), Disjoint (f i) (g i)
x : (i : ι) → α' i
hf : x ≤ f
hg : x ≤ g
i : ι
⊢ x i ≤ ⊥ i
apply h i (hf i) (hg i)