[GOAL]
p q : Prop
⊢ p ≤ q ∨ q ≤ p
[PROOFSTEP]
by_cases h : q
[GOAL]
case pos
p q : Prop
h : q
⊢ p ≤ q ∨ q ≤ p
[PROOFSTEP]
simp [h]
[GOAL]
case neg
p q : Prop
h : ¬q
⊢ p ≤ q ∨ q ≤ p
[PROOFSTEP]
simp [h]
[GOAL]
⊢ LinearOrder Prop
[PROOFSTEP]
classical exact Lattice.toLinearOrder Prop
[GOAL]
⊢ LinearOrder Prop
[PROOFSTEP]
exact Lattice.toLinearOrder Prop
[GOAL]
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)
[PROOFSTEP]
classical
constructor
· intro h i x hf hg
  refine' (update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => _⟩) (update_le_iff.mpr ⟨hg, fun _ _ => _⟩)).1
  · exact bot_le
  · exact bot_le
· intro h x hf hg i
  apply h i (hf i) (hg i)
[GOAL]
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)
[PROOFSTEP]
intro h i x hf hg
[GOAL]
case mp
ι : Type u_1
α' : ι → Type u_2
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 ≤ ⊥
[PROOFSTEP]
refine' (update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => _⟩) (update_le_iff.mpr ⟨hg, fun _ _ => _⟩)).1
[GOAL]
case mp.refine'_1
ι : Type u_1
α' : ι → Type u_2
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✝¹
[PROOFSTEP]
exact bot_le
[GOAL]
case mp.refine'_3
ι : Type u_1
α' : ι → Type u_2
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✝¹
[PROOFSTEP]
exact bot_le
[GOAL]
case mpr
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g
[PROOFSTEP]
intro h x hf hg i
[GOAL]
case mpr
ι : Type u_1
α' : ι → Type u_2
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
[PROOFSTEP]
apply h i (hf i) (hg i)
[GOAL]
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)
[PROOFSTEP]
simp_rw [_root_.isCompl_iff, disjoint_iff, codisjoint_iff, forall_and]
[GOAL]
P Q : Prop
⊢ IsCompl P Q ↔ ¬(P ↔ Q)
[PROOFSTEP]
rw [_root_.isCompl_iff, Prop.disjoint_iff, Prop.codisjoint_iff, not_iff]
[GOAL]
P Q : Prop
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
by_cases P
[GOAL]
P Q : Prop
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
by_cases P
[GOAL]
case pos
P Q : Prop
h : P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
by_cases Q
[GOAL]
case pos
P Q : Prop
h : P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
by_cases Q
[GOAL]
case neg
P Q : Prop
h : ¬P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
by_cases Q
[GOAL]
case neg
P Q : Prop
h : ¬P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
by_cases Q
[GOAL]
case pos
P Q : Prop
h✝ : P
h : Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
P Q : Prop
h✝ : P
h : ¬Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
simp [*]
[GOAL]
case pos
P Q : Prop
h✝ : ¬P
h : Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
P Q : Prop
h✝ : ¬P
h : ¬Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
simp [*]
