[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) ⁻¹' Icc b c = Icc (b - a) (c - a)
[PROOFSTEP]
simp [← Ici_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) ⁻¹' Ico b c = Ico (b - a) (c - a)
[PROOFSTEP]
simp [← Ici_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) ⁻¹' Ioc b c = Ioc (b - a) (c - a)
[PROOFSTEP]
simp [← Ioi_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) ⁻¹' Ioo b c = Ioo (b - a) (c - a)
[PROOFSTEP]
simp [← Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) ⁻¹' Icc b c = Icc (b - a) (c - a)
[PROOFSTEP]
simp [← Ici_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) ⁻¹' Ico b c = Ico (b - a) (c - a)
[PROOFSTEP]
simp [← Ici_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) ⁻¹' Ioc b c = Ioc (b - a) (c - a)
[PROOFSTEP]
simp [← Ioi_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) ⁻¹' Ioo b c = Ioo (b - a) (c - a)
[PROOFSTEP]
simp [← Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ -Icc a b = Icc (-b) (-a)
[PROOFSTEP]
simp [← Ici_inter_Iic, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ -Ico a b = Ioc (-b) (-a)
[PROOFSTEP]
simp [← Ici_inter_Iio, ← Ioi_inter_Iic, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ -Ioc a b = Ico (-b) (-a)
[PROOFSTEP]
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ -Ioo a b = Ioo (-b) (-a)
[PROOFSTEP]
simp [← Ioi_inter_Iio, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Ici b = Ici (b + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Ioi b = Ioi (b + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Iic b = Iic (b + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Iio b = Iio (b + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Icc b c = Icc (b + a) (c + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Ico b c = Ico (b + a) (c + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Ioc b c = Ioc (b + a) (c + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Ioo b c = Ioo (b + a) (c + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) ⁻¹' Icc b c = Icc (a - c) (a - b)
[PROOFSTEP]
simp [← Ici_inter_Iic, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) ⁻¹' Ico b c = Ioc (a - c) (a - b)
[PROOFSTEP]
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) ⁻¹' Ioc b c = Ico (a - c) (a - b)
[PROOFSTEP]
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) ⁻¹' Ioo b c = Ioo (a - c) (a - b)
[PROOFSTEP]
simp [← Ioi_inter_Iio, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) '' Iic b = Iic (a + b)
[PROOFSTEP]
simp [add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) '' Iio b = Iio (a + b)
[PROOFSTEP]
simp [add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) '' Iic b = Iic (b + a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) '' Iio b = Iio (b + a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Ici a = Iic (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Iic a = Ici (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Ioi a = Iio (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Iio a = Ioi (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Icc a b = Icc (-b) (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Ico a b = Ioc (-b) (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Ioc a b = Ico (-b) (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Ioo a b = Ioo (-b) (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Ici b = Iic (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ici b = Iic (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ici b = Iic (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Iic b = Ici (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iic b = Ici (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iic b = Ici (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Ioi b = Iio (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioi b = Iio (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioi b = Iio (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Iio b = Ioi (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iio b = Ioi (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iio b = Ioi (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Icc b c = Icc (a - c) (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Icc b c = Icc (a - c) (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Icc b c = Icc (a - c) (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Ici b = Ici (b - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Iic b = Iic (b - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Ioi b = Ioi (b - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Iio b = Iio (b - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Icc b c = Icc (b - a) (c - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Ico b c = Ico (b - a) (c - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Ioc b c = Ioc (b - a) (c - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Ioo b c = Ioo (b - a) (c - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => a + x) ⁻¹' [[b, c]] = [[b - a, c - a]]
[PROOFSTEP]
simp only [← Icc_min_max, preimage_const_add_Icc, min_sub_sub_right, max_sub_sub_right]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => x + a) ⁻¹' [[b, c]] = [[b - a, c - a]]
[PROOFSTEP]
simpa only [add_comm] using preimage_const_add_uIcc a b c
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ -[[a, b]] = [[-a, -b]]
[PROOFSTEP]
simp only [← Icc_min_max, preimage_neg_Icc, min_neg_neg, max_neg_neg]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => x - a) ⁻¹' [[b, c]] = [[b + a, c + a]]
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => a - x) ⁻¹' [[b, c]] = [[a - b, a - c]]
[PROOFSTEP]
simp_rw [← Icc_min_max, preimage_const_sub_Icc]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ Icc (a - max b c) (a - min b c) = Icc (min (a - b) (a - c)) (max (a - b) (a - c))
[PROOFSTEP]
simp only [sub_eq_add_neg, min_add_add_left, max_add_add_left, min_neg_neg, max_neg_neg]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => a + x) '' [[b, c]] = [[a + b, a + c]]
[PROOFSTEP]
simp [add_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => x + a) '' [[b, c]] = [[b + a, c + a]]
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => a - x) '' [[b, c]] = [[a - b, a - c]]
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' [[b, c]] = [[a - b, a - c]]
[PROOFSTEP]
dsimp [Function.comp] at this
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' [[b, c]] = [[a - b, a - c]]
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => x - a) '' [[b, c]] = [[b - a, c - a]]
[PROOFSTEP]
simp [sub_eq_add_neg, add_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ Neg.neg '' [[a, b]] = [[-a, -b]]
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ |d - c| ≤ |b - a|
[PROOFSTEP]
rw [← max_sub_min_eq_abs, ← max_sub_min_eq_abs]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ max c d - min c d ≤ max a b - min a b
[PROOFSTEP]
rw [uIcc_subset_uIcc_iff_le] at h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : min a b ≤ min c d ∧ max c d ≤ max a b
⊢ max c d - min c d ≤ max a b - min a b
[PROOFSTEP]
exact sub_le_sub h.2 h.1
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x => x * c) ⁻¹' Ioo a b = Ioo (a / c) (b / c)
[PROOFSTEP]
simp [← Ioi_inter_Iio, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x => x * c) ⁻¹' Ioc a b = Ioc (a / c) (b / c)
[PROOFSTEP]
simp [← Ioi_inter_Iic, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x => x * c) ⁻¹' Ico a b = Ico (a / c) (b / c)
[PROOFSTEP]
simp [← Ici_inter_Iio, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x => x * c) ⁻¹' Icc a b = Icc (a / c) (b / c)
[PROOFSTEP]
simp [← Ici_inter_Iic, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x => x * c) ⁻¹' Ioo a b = Ioo (b / c) (a / c)
[PROOFSTEP]
simp [← Ioi_inter_Iio, h, inter_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x => x * c) ⁻¹' Ioc a b = Ico (b / c) (a / c)
[PROOFSTEP]
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, h, inter_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x => x * c) ⁻¹' Ico a b = Ioc (b / c) (a / c)
[PROOFSTEP]
simp [← Ici_inter_Iio, ← Ioi_inter_Iic, h, inter_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x => x * c) ⁻¹' Icc a b = Icc (b / c) (a / c)
[PROOFSTEP]
simp [← Ici_inter_Iic, h, inter_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ioo a b = Ioo (a / c) (b / c)
[PROOFSTEP]
simp [← Ioi_inter_Iio, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ioc a b = Ioc (a / c) (b / c)
[PROOFSTEP]
simp [← Ioi_inter_Iic, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ico a b = Ico (a / c) (b / c)
[PROOFSTEP]
simp [← Ici_inter_Iio, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x x_1 => x * x_1) c ⁻¹' Icc a b = Icc (a / c) (b / c)
[PROOFSTEP]
simp [← Ici_inter_Iic, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Iio a = Ioi (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Iio_of_neg a h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ioi a = Iio (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Ioi_of_neg a h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Iic a = Ici (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Iic_of_neg a h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ici a = Iic (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Ici_of_neg a h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ioo a b = Ioo (b / c) (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Ioo_of_neg a b h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ioc a b = Ico (b / c) (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Ioc_of_neg a b h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ico a b = Ioc (b / c) (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Ico_of_neg a b h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Icc a b = Icc (b / c) (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Icc_of_neg a b h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a ≠ 0
b c : α
h : a < 0
⊢ (fun x => x * a) ⁻¹' [[b, c]] = [[b / a, c / a]]
[PROOFSTEP]
simp [← Icc_min_max, h, h.le, min_div_div_right_of_nonpos, max_div_div_right_of_nonpos]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha✝ : a ≠ 0
b c : α
ha : 0 < a
⊢ (fun x => x * a) ⁻¹' [[b, c]] = [[b / a, c / a]]
[PROOFSTEP]
simp [← Icc_min_max, ha, ha.le, min_div_div_right, max_div_div_right]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a ≠ 0
b c : α
⊢ (fun x => a * x) ⁻¹' [[b, c]] = [[b / a, c / a]]
[PROOFSTEP]
simp only [← preimage_mul_const_uIcc ha, mul_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a ≠ 0
b c : α
⊢ (fun x => x / a) ⁻¹' [[b, c]] = [[b * a, c * a]]
[PROOFSTEP]
simp only [div_eq_mul_inv, preimage_mul_const_uIcc (inv_ne_zero ha), inv_inv]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
ha : a = 0
⊢ (fun x => x * a) '' [[b, c]] = [[b * a, c * a]]
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
ha : ¬a = 0
⊢ (fun x => x * a⁻¹) ⁻¹' [[b, c]] = (fun x => x / a) ⁻¹' [[b, c]]
[PROOFSTEP]
simp only [div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
⊢ (fun x => a * x) '' [[b, c]] = [[a * b, a * c]]
[PROOFSTEP]
simpa only [mul_comm] using image_mul_const_uIcc a b c
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
⊢ (fun x => x / a) '' [[b, c]] = [[b / a, c / a]]
[PROOFSTEP]
simp only [div_eq_mul_inv, image_mul_const_uIcc]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ ↑(Units.mulRight (Units.mk0 c (_ : c ≠ 0))).symm ⁻¹' Icc a b = Icc (a * c) (b * c)
[PROOFSTEP]
simp [h, division_def]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
hab : a ≤ b
hc : 0 ≤ c
⊢ (fun x => x * c) '' Icc a b = Icc (a * c) (b * c)
[PROOFSTEP]
cases eq_or_lt_of_le hc
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
hab : a ≤ b
hc : 0 ≤ c
h✝ : 0 = c
⊢ (fun x => x * c) '' Icc a b = Icc (a * c) (b * c)
[PROOFSTEP]
subst c
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b : α
hab : a ≤ b
hc : 0 ≤ 0
⊢ (fun x => x * 0) '' Icc a b = Icc (a * 0) (b * 0)
[PROOFSTEP]
simp [(nonempty_Icc.2 hab).image_const]
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
hab : a ≤ b
hc : 0 ≤ c
h✝ : 0 < c
⊢ (fun x => x * c) '' Icc a b = Icc (a * c) (b * c)
[PROOFSTEP]
exact image_mul_right_Icc' a b ‹0 < c›
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c : α
⊢ (fun x x_1 => x * x_1) a '' Icc b c = Icc (a * b) (a * c)
[PROOFSTEP]
convert image_mul_right_Icc' b c h using 1
[GOAL]
case h.e'_2
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c : α
⊢ (fun x x_1 => x * x_1) a '' Icc b c = (fun x => x * a) '' Icc b c
[PROOFSTEP]
simp only [mul_comm _ a]
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c : α
⊢ Icc (a * b) (a * c) = Icc (b * a) (c * a)
[PROOFSTEP]
simp only [mul_comm _ a]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
ha : 0 ≤ a
hbc : b ≤ c
⊢ (fun x x_1 => x * x_1) a '' Icc b c = Icc (a * b) (a * c)
[PROOFSTEP]
convert image_mul_right_Icc hbc ha using 1
[GOAL]
case h.e'_2
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
ha : 0 ≤ a
hbc : b ≤ c
⊢ (fun x x_1 => x * x_1) a '' Icc b c = (fun x => x * a) '' Icc b c
[PROOFSTEP]
simp only [mul_comm _ a]
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
ha : 0 ≤ a
hbc : b ≤ c
⊢ Icc (a * b) (a * c) = Icc (b * a) (c * a)
[PROOFSTEP]
simp only [mul_comm _ a]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ ↑(Units.mulRight (Units.mk0 c (_ : c ≠ 0))).symm ⁻¹' Ioo a b = Ioo (a * c) (b * c)
[PROOFSTEP]
simp [h, division_def]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c : α
⊢ (fun x x_1 => x * x_1) a '' Ioo b c = Ioo (a * b) (a * c)
[PROOFSTEP]
convert image_mul_right_Ioo b c h using 1
[GOAL]
case h.e'_2
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c : α
⊢ (fun x x_1 => x * x_1) a '' Ioo b c = (fun x => x * a) '' Ioo b c
[PROOFSTEP]
simp only [mul_comm _ a]
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c : α
⊢ Ioo (a * b) (a * c) = Ioo (b * a) (c * a)
[PROOFSTEP]
simp only [mul_comm _ a]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
ha : 0 < a
⊢ (Ioo 0 a)⁻¹ = Ioi a⁻¹
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
ha : 0 < a
x : α
⊢ x ∈ (Ioo 0 a)⁻¹ ↔ x ∈ Ioi a⁻¹
[PROOFSTEP]
exact
  ⟨fun h => inv_inv x ▸ (inv_lt_inv ha h.1).2 h.2, fun h =>
    ⟨inv_pos.2 <| (inv_pos.2 ha).trans h, inv_inv a ▸ (inv_lt_inv ((inv_pos.2 ha).trans h) (inv_pos.2 ha)).2 h⟩⟩
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
ha : 0 < a
⊢ (Ioi a)⁻¹ = Ioo 0 a⁻¹
[PROOFSTEP]
rw [inv_eq_iff_eq_inv, inv_Ioo_0_left (inv_pos.2 ha), inv_inv]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
a : α
k : Type u_2
inst✝ : LinearOrderedField k
x : k
hx : 0 < x
⊢ (fun y => x * y) '' Ioi 0 = Ioi 0
[PROOFSTEP]
erw [(Units.mk0 x hx.ne').mulLeft.image_eq_preimage, preimage_const_mul_Ioi 0 (inv_pos.mpr hx), zero_div]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c d : α
⊢ (fun x => a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)
[PROOFSTEP]
suffices (fun x => x + b) '' ((fun x => a * x) '' Icc c d) = Icc (a * c + b) (a * d + b) by
  rwa [Set.image_image] at this
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c d : α
this : (fun x => x + b) '' ((fun x => a * x) '' Icc c d) = Icc (a * c + b) (a * d + b)
⊢ (fun x => a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)
[PROOFSTEP]
rwa [Set.image_image] at this
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c d : α
⊢ (fun x => x + b) '' ((fun x => a * x) '' Icc c d) = Icc (a * c + b) (a * d + b)
[PROOFSTEP]
rw [image_mul_left_Icc' h, image_add_const_Icc]


[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
⊢ reverse (reverse f) = f
[PROOFSTEP]
apply h.inv'
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g ↔ f = g
[PROOFSTEP]
constructor
[GOAL]
case mp
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g → f = g
[PROOFSTEP]
rintro h
[GOAL]
case mp
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h✝ : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
h : reverse f = reverse g
⊢ f = g
[PROOFSTEP]
simpa using congr_arg Quiver.reverse h
[GOAL]
case mpr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ f = g → reverse f = reverse g
[PROOFSTEP]
rintro h
[GOAL]
case mpr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h✝ : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
h : f = g
⊢ reverse f = reverse g
[PROOFSTEP]
congr
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
g : b ⟶ a
⊢ f = reverse g ↔ reverse f = g
[PROOFSTEP]
rw [← reverse_inj, reverse_reverse]
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁷ : Quiver U
inst✝⁶ : Quiver V
inst✝⁵ : Quiver W
inst✝⁴ : HasReverse U
inst✝³ : HasReverse V
inst✝² : HasReverse W
φ : U ⥤q V
ψ : V ⥤q W
inst✝¹ : Prefunctor.MapReverse φ
inst✝ : Prefunctor.MapReverse ψ
u✝ v✝ : U
e : u✝ ⟶ v✝
⊢ (φ ⋙q ψ).map (reverse e) = reverse ((φ ⋙q ψ).map e)
[PROOFSTEP]
simp only [Prefunctor.comp_map, Prefunctor.MapReverse.map_reverse']
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
inst✝ : HasReverse V
a b c : V
p : Path a b
q : Path b c
⊢ reverse (comp p q) = comp (reverse q) (reverse p)
[PROOFSTEP]
induction' q with _ _ _ _ h
[GOAL]
case nil
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
inst✝ : HasReverse V
a b c : V
p : Path a b
⊢ reverse (comp p nil) = comp (reverse nil) (reverse p)
[PROOFSTEP]
simp
[GOAL]
case cons
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
inst✝ : HasReverse V
a b c : V
p : Path a b
b✝ c✝ : V
a✝¹ : Path b b✝
a✝ : b✝ ⟶ c✝
h : reverse (comp p a✝¹) = comp (reverse a✝¹) (reverse p)
⊢ reverse (comp p (cons a✝¹ a✝)) = comp (reverse (cons a✝¹ a✝)) (reverse p)
[PROOFSTEP]
simp [h]
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
p : Path a b
⊢ reverse (reverse p) = p
[PROOFSTEP]
induction' p with _ _ _ _ h
[GOAL]
case nil
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
⊢ reverse (reverse nil) = nil
[PROOFSTEP]
simp
[GOAL]
case cons
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : reverse (reverse a✝¹) = a✝¹
⊢ reverse (reverse (cons a✝¹ a✝)) = cons a✝¹ a✝
[PROOFSTEP]
rw [Path.reverse, Path.reverse_comp, h, Path.reverse_toPath, Quiver.reverse_reverse]
[GOAL]
case cons
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : reverse (reverse a✝¹) = a✝¹
⊢ comp a✝¹ (Hom.toPath a✝) = cons a✝¹ a✝
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ of ⋙q lift φ = φ
[PROOFSTEP]
fapply Prefunctor.ext
[GOAL]
case h_obj
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X : V), (of ⋙q lift φ).obj X = φ.obj X
[PROOFSTEP]
rintro X
[GOAL]
case h_obj
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
X : V
⊢ (of ⋙q lift φ).obj X = φ.obj X
[PROOFSTEP]
rfl
[GOAL]
case h_map
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X Y : V) (f : X ⟶ Y),
    (of ⋙q lift φ).map f =
      Eq.recOn (_ : φ.obj Y = (of ⋙q lift φ).obj Y) (Eq.recOn (_ : φ.obj X = (of ⋙q lift φ).obj X) (φ.map f))
[PROOFSTEP]
rintro X Y f
[GOAL]
case h_map
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
X Y : V
f : X ⟶ Y
⊢ (of ⋙q lift φ).map f =
    Eq.recOn (_ : φ.obj Y = (of ⋙q lift φ).obj Y) (Eq.recOn (_ : φ.obj X = (of ⋙q lift φ).obj X) (φ.map f))
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
f : X ⟶ Y
⊢ (lift φ).map (reverse f) = reverse ((lift φ).map f)
[PROOFSTEP]
dsimp [Symmetrify.lift]
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
f : X ⟶ Y
⊢ (match Sum.swap f with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match f with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))
[PROOFSTEP]
cases f
[GOAL]
case inl
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ (match Sum.swap (Sum.inl val✝) with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inl val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))
[PROOFSTEP]
simp only
[GOAL]
case inl
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ (match Sum.swap (Sum.inl val✝) with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse (φ.map val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ (match Sum.swap (Sum.inr val✝) with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inr val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))
[PROOFSTEP]
simp only [reverse_reverse]
[GOAL]
case inr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ (match Sum.swap (Sum.inr val✝) with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    φ.map val✝
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
Φ : Symmetrify V ⥤q V'
hΦ : of ⋙q Φ = φ
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ Φ = lift φ
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ Φ = lift (of ⋙q Φ)
[PROOFSTEP]
fapply Prefunctor.ext
[GOAL]
case h_obj
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X : Symmetrify V), Φ.obj X = (lift (of ⋙q Φ)).obj X
[PROOFSTEP]
rintro X
[GOAL]
case h_obj
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X : Symmetrify V
⊢ Φ.obj X = (lift (of ⋙q Φ)).obj X
[PROOFSTEP]
rfl
[GOAL]
case h_map
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X Y : Symmetrify V) (f : X ⟶ Y),
    Φ.map f =
      Eq.recOn (_ : (lift (of ⋙q Φ)).obj Y = Φ.obj Y)
        (Eq.recOn (_ : (lift (of ⋙q Φ)).obj X = Φ.obj X) ((lift (of ⋙q Φ)).map f))
[PROOFSTEP]
rintro X Y f
[GOAL]
case h_map
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
f : X ⟶ Y
⊢ Φ.map f =
    Eq.recOn (_ : (lift (of ⋙q Φ)).obj Y = Φ.obj Y)
      (Eq.recOn (_ : (lift (of ⋙q Φ)).obj X = Φ.obj X) ((lift (of ⋙q Φ)).map f))
[PROOFSTEP]
cases f
[GOAL]
case h_map.inl
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ Φ.map (Sum.inl val✝) =
    Eq.recOn (_ : (lift (of ⋙q Φ)).obj Y = Φ.obj Y)
      (Eq.recOn (_ : (lift (of ⋙q Φ)).obj X = Φ.obj X) ((lift (of ⋙q Φ)).map (Sum.inl val✝)))
[PROOFSTEP]
rfl
[GOAL]
case h_map.inr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ Φ.map (Sum.inr val✝) =
    Eq.recOn (_ : (lift (of ⋙q Φ)).obj Y = Φ.obj Y)
      (Eq.recOn (_ : (lift (of ⋙q Φ)).obj X = Φ.obj X) ((lift (of ⋙q Φ)).map (Sum.inr val✝)))
[PROOFSTEP]
exact hΦinv (Sum.inl _)
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
e : u✝ ⟶ v✝
⊢ (Prefunctor.symmetrify φ).map (reverse e) = reverse ((Prefunctor.symmetrify φ).map e)
[PROOFSTEP]
cases e
[GOAL]
case inl
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
val✝ : u✝ ⟶ v✝
⊢ (Prefunctor.symmetrify φ).map (reverse (Sum.inl val✝)) = reverse ((Prefunctor.symmetrify φ).map (Sum.inl val✝))
[PROOFSTEP]
rfl
[GOAL]
case inr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
val✝ : v✝ ⟶ u✝
⊢ (Prefunctor.symmetrify φ).map (reverse (Sum.inr val✝)) = reverse ((Prefunctor.symmetrify φ).map (Sum.inr val✝))
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
a✝ b✝ : Push σ
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ reverse (reverse (PushQuiver.arrow f)) = PushQuiver.arrow f
[PROOFSTEP]
dsimp [reverse]
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
a✝ b✝ : Push σ
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ PushQuiver.arrow (HasReverse.reverse' (HasReverse.reverse' f)) = PushQuiver.arrow f
[PROOFSTEP]
congr
[GOAL]
case e_f
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
a✝ b✝ : Push σ
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ HasReverse.reverse' (HasReverse.reverse' f) = f
[PROOFSTEP]
apply h.inv'
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
⊢ ∀ {u v : V} (e : u ⟶ v), (of σ).map (reverse e) = reverse ((of σ).map e)
[PROOFSTEP]
simp [of_reverse]


[GOAL]
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F G : Prefunctor V W
h_obj : ∀ (X : V), F.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))
⊢ F = G
[PROOFSTEP]
cases' F with F_obj _
[GOAL]
case mk
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
G : Prefunctor V W
F_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝ }.obj X = G.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝ }.map f =
      Eq.recOn (_ : G.obj Y = { obj := F_obj, map := map✝ }.obj Y)
        (Eq.recOn (_ : G.obj X = { obj := F_obj, map := map✝ }.obj X) (G.map f))
⊢ { obj := F_obj, map := map✝ } = G
[PROOFSTEP]
cases' G with G_obj _
[GOAL]
case mk.mk
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f =
      Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
        (Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
          ({ obj := G_obj, map := map✝ }.map f))
⊢ { obj := F_obj, map := map✝¹ } = { obj := G_obj, map := map✝ }
[PROOFSTEP]
obtain rfl : F_obj = G_obj := by
  ext X
  apply h_obj
[GOAL]
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f =
      Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
        (Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
          ({ obj := G_obj, map := map✝ }.map f))
⊢ F_obj = G_obj
[PROOFSTEP]
ext X
[GOAL]
case h
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f =
      Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
        (Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
          ({ obj := G_obj, map := map✝ }.map f))
X : V
⊢ F_obj X = G_obj X
[PROOFSTEP]
apply h_obj
[GOAL]
case mk.mk
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := F_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f =
      Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
        (Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
          ({ obj := F_obj, map := map✝ }.map f))
⊢ { obj := F_obj, map := map✝¹ } = { obj := F_obj, map := map✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_map
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := F_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f =
      Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
        (Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
          ({ obj := F_obj, map := map✝ }.map f))
⊢ map✝¹ = map✝
[PROOFSTEP]
funext X Y f
[GOAL]
case mk.mk.e_map.h.h.h
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := F_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f =
      Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
        (Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
          ({ obj := F_obj, map := map✝ }.map f))
X Y : V
f : X ⟶ Y
⊢ map✝¹ f = map✝ f
[PROOFSTEP]
simpa using h_map X Y f


[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
⊢ Intersecting {a} ↔ a ≠ ⊥
[PROOFSTEP]
simp [Intersecting]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
hs : Intersecting s
ha : a ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint a b
⊢ Intersecting (insert a s)
[PROOFSTEP]
rintro b (rfl | hb) c (rfl | hc)
[GOAL]
case inl.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
b c✝ : α
hs : Intersecting s
c : α
ha : c ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint c b
⊢ ¬Disjoint c c
[PROOFSTEP]
rwa [disjoint_self]
[GOAL]
case inl.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
b✝ c✝ : α
hs : Intersecting s
b : α
ha : b ≠ ⊥
h : ∀ (b_1 : α), b_1 ∈ s → ¬Disjoint b b_1
c : α
hc : c ∈ s
⊢ ¬Disjoint b c
[PROOFSTEP]
exact h _ hc
[GOAL]
case inr.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
b✝ c✝ : α
hs : Intersecting s
b : α
hb : b ∈ s
c : α
ha : c ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint c b
⊢ ¬Disjoint b c
[PROOFSTEP]
exact fun H => h _ hb H.symm
[GOAL]
case inr.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b✝ c✝ : α
hs : Intersecting s
ha : a ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
⊢ ¬Disjoint b c
[PROOFSTEP]
exact hs hb hc
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
⊢ Intersecting s ↔ (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
[PROOFSTEP]
refine' ⟨fun h => ⟨fun a ha b hb _ => h ha hb, _⟩, fun h a ha b hb hab => _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
h : Intersecting s
⊢ s ≠ {⊥}
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
t : Set α
a b c : α
h : Intersecting {⊥}
⊢ False
[PROOFSTEP]
exact intersecting_singleton.1 h rfl
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
⊢ False
[PROOFSTEP]
have := h.1.eq ha hb (Classical.not_not.2 hab)
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
this : a = b
⊢ False
[PROOFSTEP]
rw [this, disjoint_self] at hab
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : b = ⊥
this : a = b
⊢ False
[PROOFSTEP]
rw [hab] at hb
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : ⊥ ∈ s
hab : b = ⊥
this : a = b
⊢ False
[PROOFSTEP]
exact h.2 (eq_singleton_iff_unique_mem.2 ⟨hb, fun c hc => not_ne_iff.1 fun H => h.1 hb hc H.symm disjoint_bot_left⟩)
[GOAL]
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
s✝ t : Set α
a b c : α
inst✝ : Subsingleton α
s : Set α
⊢ Intersecting s ↔ s = ∅
[PROOFSTEP]
refine'
  subsingleton_of_subsingleton.intersecting.trans
    ⟨not_imp_comm.2 fun h => subsingleton_of_subsingleton.eq_singleton_of_mem _, _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
s✝ t : Set α
a b c : α
inst✝ : Subsingleton α
s : Set α
h : ¬s = ∅
⊢ ⊥ ∈ s
[PROOFSTEP]
obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 h
[GOAL]
case refine'_1.intro
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
s✝ t : Set α
a✝ b c : α
inst✝ : Subsingleton α
s : Set α
h : ¬s = ∅
a : α
ha : a ∈ s
⊢ ⊥ ∈ s
[PROOFSTEP]
rwa [Subsingleton.elim ⊥ a]
[GOAL]
case refine'_2
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
s✝ t : Set α
a b c : α
inst✝ : Subsingleton α
s : Set α
⊢ s = ∅ → s ≠ {⊥}
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
s t : Set α
a b c : α
inst✝ : Subsingleton α
⊢ ∅ ≠ {⊥}
[PROOFSTEP]
exact (Set.singleton_nonempty _).ne_empty.symm
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
⊢ IsUpperSet s
[PROOFSTEP]
classical
rintro a b hab ha
rw [h (Insert.insert b s) _ (subset_insert _ _)]
· exact mem_insert _ _
exact hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
⊢ IsUpperSet s
[PROOFSTEP]
rintro a b hab ha
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ s
[PROOFSTEP]
rw [h (Insert.insert b s) _ (subset_insert _ _)]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ insert b s
[PROOFSTEP]
exact mem_insert _ _
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ Intersecting (insert b s)
[PROOFSTEP]
exact hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s✝ t : Set α
a b c : α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ IsUpperSet ↑s
[PROOFSTEP]
classical
rintro a b hab ha
rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]
· exact mem_insert_self _ _
rw [coe_insert]
exact hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s✝ t : Set α
a b c : α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ IsUpperSet ↑s
[PROOFSTEP]
rintro a b hab ha
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s✝ t : Set α
a✝ b✝ c : α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ b ∈ ↑s
[PROOFSTEP]
rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s✝ t : Set α
a✝ b✝ c : α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ b ∈ ↑(insert b s)
[PROOFSTEP]
exact mem_insert_self _ _
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s✝ t : Set α
a✝ b✝ c : α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ Intersecting ↑(insert b s)
[PROOFSTEP]
rw [coe_insert]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s✝ t : Set α
a✝ b✝ c : α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ Intersecting (insert b ↑s)
[PROOFSTEP]
exact hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
[GOAL]
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : Intersecting ↑s
⊢ Disjoint s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)
[PROOFSTEP]
rw [Finset.disjoint_left]
[GOAL]
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : Intersecting ↑s
⊢ ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ map { toFun := compl, inj' := (_ : Function.Injective compl) } s
[PROOFSTEP]
rintro x hx hxc
[GOAL]
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : Intersecting ↑s
x : α
hx : x ∈ s
hxc : x ∈ map { toFun := compl, inj' := (_ : Function.Injective compl) } s
⊢ False
[PROOFSTEP]
obtain ⟨x, hx', rfl⟩ := mem_map.mp hxc
[GOAL]
case intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : Intersecting ↑s
x : α
hx' : x ∈ s
hx : ↑{ toFun := compl, inj' := (_ : Function.Injective compl) } x ∈ s
hxc :
  ↑{ toFun := compl, inj' := (_ : Function.Injective compl) } x ∈
    map { toFun := compl, inj' := (_ : Function.Injective compl) } s
⊢ False
[PROOFSTEP]
exact hs.not_compl_mem hx' hx
[GOAL]
α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ 2 * card s ≤ Fintype.card α
[PROOFSTEP]
classical
refine' (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' _
rw [two_mul, card_disjUnion, card_map]
[GOAL]
α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ 2 * card s ≤ Fintype.card α
[PROOFSTEP]
refine' (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' _
[GOAL]
α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ 2 * card s =
    card
      (disjUnion s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)
        (_ : Disjoint s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)))
[PROOFSTEP]
rw [two_mul, card_disjUnion, card_map]
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ (∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t) ↔ 2 * card s = Fintype.card α
[PROOFSTEP]
classical
refine'
  ⟨fun h => _, fun h t ht hst =>
    Finset.eq_of_subset_of_card_le hst <| le_of_mul_le_mul_left (ht.card_le.trans_eq h.symm) two_pos⟩
suffices s.disjUnion (s.map ⟨compl, compl_injective⟩) hs.disjoint_map_compl = Finset.univ by
  rw [Fintype.card, ← this, two_mul, card_disjUnion, card_map]
rw [← coe_eq_univ, disjUnion_eq_union, coe_union, coe_map, Function.Embedding.coeFn_mk,
  image_eq_preimage_of_inverse compl_compl compl_compl]
refine' eq_univ_of_forall fun a => _
simp_rw [mem_union, mem_preimage]
by_contra' ha
refine' s.ne_insert_of_not_mem _ ha.1 (h _ _ <| s.subset_insert _)
rw [coe_insert]
refine' hs.insert _ fun b hb hab => ha.2 <| (hs.isUpperSet' h) hab.le_compl_left hb
rintro rfl
have := h {⊤} (by rw [coe_singleton]; exact intersecting_singleton.2 top_ne_bot)
rw [compl_bot] at ha
rw [coe_eq_empty.1 ((hs.isUpperSet' h).not_top_mem.1 ha.2)] at this
exact Finset.singleton_ne_empty _ (this <| Finset.empty_subset _).symm
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ (∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t) ↔ 2 * card s = Fintype.card α
[PROOFSTEP]
refine'
  ⟨fun h => _, fun h t ht hst =>
    Finset.eq_of_subset_of_card_le hst <| le_of_mul_le_mul_left (ht.card_le.trans_eq h.symm) two_pos⟩
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ 2 * card s = Fintype.card α
[PROOFSTEP]
suffices s.disjUnion (s.map ⟨compl, compl_injective⟩) hs.disjoint_map_compl = Finset.univ by
  rw [Fintype.card, ← this, two_mul, card_disjUnion, card_map]
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
this :
  disjUnion s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)
      (_ : Disjoint s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)) =
    Finset.univ
⊢ 2 * card s = Fintype.card α
[PROOFSTEP]
rw [Fintype.card, ← this, two_mul, card_disjUnion, card_map]
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ disjUnion s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)
      (_ : Disjoint s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)) =
    Finset.univ
[PROOFSTEP]
rw [← coe_eq_univ, disjUnion_eq_union, coe_union, coe_map, Function.Embedding.coeFn_mk,
  image_eq_preimage_of_inverse compl_compl compl_compl]
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ ↑s ∪ compl ⁻¹' ↑s = univ
[PROOFSTEP]
refine' eq_univ_of_forall fun a => _
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a : α
⊢ a ∈ ↑s ∪ compl ⁻¹' ↑s
[PROOFSTEP]
simp_rw [mem_union, mem_preimage]
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a : α
⊢ a ∈ ↑s ∨ aᶜ ∈ ↑s
[PROOFSTEP]
by_contra' ha
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a : α
ha : ¬a ∈ ↑s ∧ ¬aᶜ ∈ ↑s
⊢ False
[PROOFSTEP]
refine' s.ne_insert_of_not_mem _ ha.1 (h _ _ <| s.subset_insert _)
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a : α
ha : ¬a ∈ ↑s ∧ ¬aᶜ ∈ ↑s
⊢ Intersecting ↑(insert a s)
[PROOFSTEP]
rw [coe_insert]
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a : α
ha : ¬a ∈ ↑s ∧ ¬aᶜ ∈ ↑s
⊢ Intersecting (insert a ↑s)
[PROOFSTEP]
refine' hs.insert _ fun b hb hab => ha.2 <| (hs.isUpperSet' h) hab.le_compl_left hb
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a : α
ha : ¬a ∈ ↑s ∧ ¬aᶜ ∈ ↑s
⊢ a ≠ ⊥
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
ha : ¬⊥ ∈ ↑s ∧ ¬⊥ᶜ ∈ ↑s
⊢ False
[PROOFSTEP]
have := h {⊤} (by rw [coe_singleton]; exact intersecting_singleton.2 top_ne_bot)
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
ha : ¬⊥ ∈ ↑s ∧ ¬⊥ᶜ ∈ ↑s
⊢ Intersecting ↑{⊤}
[PROOFSTEP]
rw [coe_singleton]
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
ha : ¬⊥ ∈ ↑s ∧ ¬⊥ᶜ ∈ ↑s
⊢ Intersecting {⊤}
[PROOFSTEP]
exact intersecting_singleton.2 top_ne_bot
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
ha : ¬⊥ ∈ ↑s ∧ ¬⊥ᶜ ∈ ↑s
this : s ⊆ {⊤} → s = {⊤}
⊢ False
[PROOFSTEP]
rw [compl_bot] at ha
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
ha : ¬⊥ ∈ ↑s ∧ ¬⊤ ∈ ↑s
this : s ⊆ {⊤} → s = {⊤}
⊢ False
[PROOFSTEP]
rw [coe_eq_empty.1 ((hs.isUpperSet' h).not_top_mem.1 ha.2)] at this
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
ha : ¬⊥ ∈ ↑s ∧ ¬⊤ ∈ ↑s
this : ∅ ⊆ {⊤} → ∅ = {⊤}
⊢ False
[PROOFSTEP]
exact Finset.singleton_ne_empty _ (this <| Finset.empty_subset _).symm
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
have := hs.card_le
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
this : 2 * card s ≤ Fintype.card α
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
rw [mul_comm, ← Nat.le_div_iff_mul_le' two_pos] at this
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
this : card s ≤ Fintype.card α / 2
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
revert hs
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
this : card s ≤ Fintype.card α / 2
⊢ Intersecting ↑s → ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
refine' s.strongDownwardInductionOn _ this
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
this : card s ≤ Fintype.card α / 2
⊢ ∀ (t₁ : Finset α),
    (∀ {t₂ : Finset α},
        card t₂ ≤ Fintype.card α / 2 →
          t₁ ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t) →
      card t₁ ≤ Fintype.card α / 2 → Intersecting ↑t₁ → ∃ t, t₁ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
rintro s ih _hcard hs
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
by_cases h : ∀ t : Finset α, (t : Set α).Intersecting → s ⊆ t → s = t
[GOAL]
case pos
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
exact ⟨s, Subset.rfl, hs.is_max_iff_card_eq.1 h, hs⟩
[GOAL]
case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
h : ¬∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
push_neg at h
[GOAL]
case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
h : ∃ t, Intersecting ↑t ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
obtain ⟨t, ht, hst⟩ := h
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
t : Finset α
ht : Intersecting ↑t
hst : s ⊆ t ∧ s ≠ t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
refine' (ih _ (_root_.ssubset_iff_subset_ne.2 hst) ht).imp fun u => And.imp_left hst.1.trans
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
t : Finset α
ht : Intersecting ↑t
hst : s ⊆ t ∧ s ≠ t
⊢ card t ≤ Fintype.card α / 2
[PROOFSTEP]
rw [Nat.le_div_iff_mul_le' two_pos, mul_comm]
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
t : Finset α
ht : Intersecting ↑t
hst : s ⊆ t ∧ s ≠ t
⊢ 2 * card t ≤ Fintype.card α
[PROOFSTEP]
exact ht.card_le