[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b x : (i : ι) → α i
⊢ x ∈ (fun a b => piFinset fun i => Icc (a i) (b i)) a b ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
simp_rw [mem_piFinset, mem_Icc, le_def, forall_and]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ Finset.card (Ico a b) = ∏ i : ι, Finset.card (Icc (a i) (b i)) - 1
[PROOFSTEP]
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ Finset.card (Ioc a b) = ∏ i : ι, Finset.card (Icc (a i) (b i)) - 1
[PROOFSTEP]
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ Finset.card (Ioo a b) = ∏ i : ι, Finset.card (Icc (a i) (b i)) - 2
[PROOFSTEP]
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
b✝ b x : (i : ι) → α i
⊢ x ∈ (fun b => piFinset fun i => Iic (b i)) b ↔ x ≤ b
[PROOFSTEP]
simp_rw [mem_piFinset, mem_Iic, le_def]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
b : (i : ι) → α i
⊢ Finset.card (Iio b) = ∏ i : ι, Finset.card (Iic (b i)) - 1
[PROOFSTEP]
rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a✝ a x : (i : ι) → α i
⊢ x ∈ (fun a => piFinset fun i => Ici (a i)) a ↔ a ≤ x
[PROOFSTEP]
simp_rw [mem_piFinset, mem_Ici, le_def]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a : (i : ι) → α i
⊢ Finset.card (Ioi a) = ∏ i : ι, Finset.card (Ici (a i)) - 1
[PROOFSTEP]
rw [card_Ioi_eq_card_Ici_sub_one, card_Ici]


[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f i
i✝ : I
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → One (f i)
inst✝² : (i : I) → One (g i)
inst✝¹ : (i : I) → One (h i)
inst✝ : One β
i : I
x : β
i' : I
⊢ mulSingle i x i' = mulSingle i' x i
[PROOFSTEP]
simp [mulSingle_apply, eq_comm]
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f i
i✝ : I
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h i)
f' : (i : I) → f i → g i
hf' : ∀ (i : I), f' i 1 = 1
i : I
x : f i
j : I
⊢ f' j (mulSingle i x j) = mulSingle i (f' i x) j
[PROOFSTEP]
simpa only [Pi.one_apply, hf', mulSingle] using Function.apply_update f' 1 i x j
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y✝ : (i : I) → f i
i✝ : I
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h i)
f' : (i : I) → f i → g i → h i
hf' : ∀ (i : I), f' i 1 1 = 1
i : I
x : f i
y : g i
j : I
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h✝ : I → Type v₃
x✝ y✝ : (i : I) → f i
i✝ : I
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h✝ i)
f' : (i : I) → f i → g i → h✝ i
hf' : ∀ (i : I), f' i 1 1 = 1
i : I
x : f i
y : g i
j : I
h : j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j
[PROOFSTEP]
subst h
[GOAL]
case pos
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y✝ : (i : I) → f i
i : I
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h i)
f' : (i : I) → f i → g i → h i
hf' : ∀ (i : I), f' i 1 1 = 1
j : I
x : f j
y : g j
⊢ f' j (mulSingle j x j) (mulSingle j y j) = mulSingle j (f' j x y) j
[PROOFSTEP]
simp only [mulSingle_eq_same]
[GOAL]
case neg
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h✝ : I → Type v₃
x✝ y✝ : (i : I) → f i
i✝ : I
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h✝ i)
f' : (i : I) → f i → g i → h✝ i
hf' : ∀ (i : I), f' i 1 1 = 1
i : I
x : f i
y : g i
j : I
h : ¬j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j
[PROOFSTEP]
simp only [mulSingle_eq_of_ne h, hf']
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f✝ i
i : I
inst✝ : One γ
f : α → β
x✝ : β
⊢ extend f 1 1 x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
apply ite_self
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f✝ i
i : I
inst✝ : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ * g₂) (e₁ * e₂) = extend f g₁ e₁ * extend f g₂ e₂
[PROOFSTEP]
classical
funext x
simp only [not_exists, extend_def, Pi.mul_apply, apply_dite₂, dite_eq_ite, ite_self]
  -- Porting note: The Lean3 statement was
  -- `funext $ λ _, by convert (apply_dite2 (*) _ _ _ _ _).symm`
  -- which converts to
  -- `funext fun _ => by convert (apply_dite₂ (· * ·) _ _ _ _ _).symm`
  -- However this does not work, and we're not sure why.
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f✝ i
i : I
inst✝ : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ * g₂) (e₁ * e₂) = extend f g₁ e₁ * extend f g₂ e₂
[PROOFSTEP]
funext x
[GOAL]
case h
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f✝ i
i : I
inst✝ : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
x : β
⊢ extend f (g₁ * g₂) (e₁ * e₂) x = (extend f g₁ e₁ * extend f g₂ e₂) x
[PROOFSTEP]
simp only [not_exists, extend_def, Pi.mul_apply, apply_dite₂, dite_eq_ite, ite_self]
  -- Porting note: The Lean3 statement was
  -- `funext $ λ _, by convert (apply_dite2 (*) _ _ _ _ _).symm`
  -- which converts to
  -- `funext fun _ => by convert (apply_dite₂ (· * ·) _ _ _ _ _).symm`
  -- However this does not work, and we're not sure why.
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : I → Type v₁
g✝ : I → Type v₂
h : I → Type v₃
x y : (i : I) → f✝ i
i : I
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
⊢ extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹
[PROOFSTEP]
classical
funext x
simp only [not_exists, extend_def, Pi.inv_apply, apply_dite Inv.inv]
  -- Porting note: The Lean3 statement was
  -- `funext $ λ _, by convert (apply_dite has_inv.inv _ _ _).symm`
  -- which converts to
  -- `funext fun _ => by convert (apply_dite Inv.inv _ _ _).symm`
  -- However this does not work, and we're not sure why.
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : I → Type v₁
g✝ : I → Type v₂
h : I → Type v₃
x y : (i : I) → f✝ i
i : I
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
⊢ extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹
[PROOFSTEP]
funext x
[GOAL]
case h
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : I → Type v₁
g✝ : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f✝ i
i : I
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
x : β
⊢ extend f g⁻¹ e⁻¹ x = (extend f g e)⁻¹ x
[PROOFSTEP]
simp only [not_exists, extend_def, Pi.inv_apply, apply_dite Inv.inv]
  -- Porting note: The Lean3 statement was
  -- `funext $ λ _, by convert (apply_dite has_inv.inv _ _ _).symm`
  -- which converts to
  -- `funext fun _ => by convert (apply_dite Inv.inv _ _ _).symm`
  -- However this does not work, and we're not sure why.
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f✝ i
i : I
inst✝ : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ / g₂) (e₁ / e₂) = extend f g₁ e₁ / extend f g₂ e₂
[PROOFSTEP]
classical
funext x
simp [Function.extend_def, apply_dite₂]
  -- Porting note: The Lean3 statement was
  -- `funext $ λ _, by convert (apply_dite2 (/) _ _ _ _ _).symm`
  -- which converts to
  -- `funext fun _ => by convert (apply_dite₂ (· / ·) _ _ _ _ _).symm`
  -- However this does not work, and we're not sure why.
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f✝ i
i : I
inst✝ : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ / g₂) (e₁ / e₂) = extend f g₁ e₁ / extend f g₂ e₂
[PROOFSTEP]
funext x
[GOAL]
case h
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f✝ i
i : I
inst✝ : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
x : β
⊢ extend f (g₁ / g₂) (e₁ / e₂) x = (extend f g₁ e₁ / extend f g₂ e₂) x
[PROOFSTEP]
simp [Function.extend_def, apply_dite₂]
  -- Porting note: The Lean3 statement was
  -- `funext $ λ _, by convert (apply_dite2 (/) _ _ _ _ _).symm`
  -- which converts to
  -- `funext fun _ => by convert (apply_dite₂ (· / ·) _ _ _ _ _).symm`
  -- However this does not work, and we're not sure why.
[GOAL]
I : Type u
α✝ : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f i
i✝ : I
α : Type u_4
inst✝² : DecidableEq I
inst✝¹ : Subsingleton I
inst✝ : One α
i : I
x : α
j : I
⊢ Pi.mulSingle i x j = x
[PROOFSTEP]
rw [Subsingleton.elim j i, Pi.mulSingle_eq_same]
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i✝ : I
a a' : α → γ
b b' : β → γ
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : One γ
i : α
c : γ
⊢ Sum.elim (Pi.mulSingle i c) 1 = Pi.mulSingle (inl i) c
[PROOFSTEP]
simp only [Pi.mulSingle, Sum.elim_update_left, elim_one_one]
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i✝ : I
a a' : α → γ
b b' : β → γ
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : One γ
i : β
c : γ
⊢ Sum.elim 1 (Pi.mulSingle i c) = Pi.mulSingle (inr i) c
[PROOFSTEP]
simp only [Pi.mulSingle, Sum.elim_update_right, elim_one_one]
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
⊢ Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'
[PROOFSTEP]
ext x
[GOAL]
case h
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
x : α ⊕ β
⊢ Sum.elim (a * a') (b * b') x = (Sum.elim a b * Sum.elim a' b') x
[PROOFSTEP]
cases x
[GOAL]
case h.inl
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
val✝ : α
⊢ Sum.elim (a * a') (b * b') (inl val✝) = (Sum.elim a b * Sum.elim a' b') (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case h.inr
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
val✝ : β
⊢ Sum.elim (a * a') (b * b') (inr val✝) = (Sum.elim a b * Sum.elim a' b') (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
⊢ Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'
[PROOFSTEP]
ext x
[GOAL]
case h
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
x : α ⊕ β
⊢ Sum.elim (a / a') (b / b') x = (Sum.elim a b / Sum.elim a' b') x
[PROOFSTEP]
cases x
[GOAL]
case h.inl
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
val✝ : α
⊢ Sum.elim (a / a') (b / b') (inl val✝) = (Sum.elim a b / Sum.elim a' b') (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case h.inr
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
val✝ : β
⊢ Sum.elim (a / a') (b / b') (inr val✝) = (Sum.elim a b / Sum.elim a' b') (inr val✝)
[PROOFSTEP]
rfl


[GOAL]
ι : Type u_1
β : ι → Type u_2
r✝ : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : (i : ι) → PartialOrder (β i)
r : ι → ι → Prop
hwf : WellFounded r
x y : (i : ι) → β i
hlt : x < y
⊢ Pi.Lex r (fun i x x_1 => x < x_1) x y
[PROOFSTEP]
simp_rw [Pi.Lex, le_antisymm_iff]
[GOAL]
ι : Type u_1
β : ι → Type u_2
r✝ : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : (i : ι) → PartialOrder (β i)
r : ι → ι → Prop
hwf : WellFounded r
x y : (i : ι) → β i
hlt : x < y
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
[PROOFSTEP]
exact lex_lt_of_lt_of_preorder hwf hlt
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
[PROOFSTEP]
cases' eq_or_ne a b with hab hab
[GOAL]
case inl
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : a = b
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
[PROOFSTEP]
exact Or.inr (Or.inl hab)
[GOAL]
case inr
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : a ≠ b
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
[PROOFSTEP]
rw [Function.ne_iff] at hab
[GOAL]
case inr
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
[PROOFSTEP]
let i := wf.min _ hab
[GOAL]
case inr
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
[PROOFSTEP]
have hri : ∀ j, r j i → a j = b j := by
  intro j
  rw [← not_imp_not]
  exact fun h' => wf.not_lt_min _ _ h'
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
⊢ ∀ (j : ι), r j i → a j = b j
[PROOFSTEP]
intro j
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
j : ι
⊢ r j i → a j = b j
[PROOFSTEP]
rw [← not_imp_not]
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
j : ι
⊢ ¬a j = b j → ¬r j i
[PROOFSTEP]
exact fun h' => wf.not_lt_min _ _ h'
[GOAL]
case inr
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
hri : ∀ (j : ι), r j i → a j = b j
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
[PROOFSTEP]
have hne : a i ≠ b i := wf.min_mem _ hab
[GOAL]
case inr
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
hri : ∀ (j : ι), r j i → a j = b j
hne : a i ≠ b i
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
[PROOFSTEP]
cases' trichotomous_of s (a i) (b i) with hi hi
[GOAL]
case inr.inl
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
hri : ∀ (j : ι), r j i → a j = b j
hne : a i ≠ b i
hi : s (a i) (b i)
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
case inr.inr
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
hri : ∀ (j : ι), r j i → a j = b j
hne : a i ≠ b i
hi : a i = b i ∨ s (b i) (a i)
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
[PROOFSTEP]
exacts [Or.inl ⟨i, hri, hi⟩, Or.inr <| Or.inr <| ⟨i, fun j hj => (hri j hj).symm, hi.resolve_left hne⟩]
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝¹ : LinearOrder ι
inst✝ : (a : ι) → PartialOrder (β a)
⊢ ∀ (a b c : Lex ((i : ι) → β i)), a < b → b < c → a < c
[PROOFSTEP]
rintro a b c ⟨N₁, lt_N₁, a_lt_b⟩ ⟨N₂, lt_N₂, b_lt_c⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝¹ : LinearOrder ι
inst✝ : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun x x_1 => x < x_1) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun x x_1 => x < x_1) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
⊢ a < c
[PROOFSTEP]
rcases lt_trichotomy N₁ N₂ with (H | rfl | H)
[GOAL]
case intro.intro.intro.intro.inl
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝¹ : LinearOrder ι
inst✝ : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun x x_1 => x < x_1) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun x x_1 => x < x_1) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
H : N₁ < N₂
⊢ a < c
case intro.intro.intro.intro.inr.inl
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝¹ : LinearOrder ι
inst✝ : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun x x_1 => x < x_1) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
lt_N₂ : ∀ (j : ι), (fun x x_1 => x < x_1) j N₁ → b j = c j
b_lt_c : b N₁ < c N₁
⊢ a < c
case intro.intro.intro.intro.inr.inr
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝¹ : LinearOrder ι
inst✝ : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun x x_1 => x < x_1) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun x x_1 => x < x_1) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
H : N₂ < N₁
⊢ a < c
[PROOFSTEP]
exacts [⟨N₁, fun j hj => (lt_N₁ _ hj).trans (lt_N₂ _ <| hj.trans H), lt_N₂ _ H ▸ a_lt_b⟩,
  ⟨N₁, fun j hj => (lt_N₁ _ hj).trans (lt_N₂ _ hj), a_lt_b.trans b_lt_c⟩,
  ⟨N₂, fun j hj => (lt_N₁ _ (hj.trans H)).trans (lt_N₂ _ hj), (lt_N₁ _ H).symm ▸ b_lt_c⟩]
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i✝ : ι
a✝ : β i✝
a b : (i : ι) → β i
h : a ≤ b
hne : ¬↑toLex a = ↑toLex b
i : ι
hi : i ∈ {i | a i ≠ b i}
hl : ∀ (x : ι), x ∈ {i | a i ≠ b i} → ¬x < i
j : ι
hj : (fun x x_1 => x < x_1) j i
⊢ ↑toLex a j = ↑toLex b j
[PROOFSTEP]
contrapose! hl
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i✝ : ι
a✝ : β i✝
a b : (i : ι) → β i
h : a ≤ b
hne : ¬↑toLex a = ↑toLex b
i : ι
hi : i ∈ {i | a i ≠ b i}
j : ι
hj : (fun x x_1 => x < x_1) j i
hl : ↑toLex a j ≠ ↑toLex b j
⊢ ∃ x, x ∈ {i | a i ≠ b i} ∧ x < i
[PROOFSTEP]
exact ⟨j, hl, hj⟩
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i✝ : ι
a✝ : β i✝
a b : (i : ι) → β i
h : a < b
i : ι
hi : i ∈ {i | a i ≠ b i}
hl : ∀ (x : ι), x ∈ {i | a i ≠ b i} → ¬x < i
j : ι
hj : (fun x x_1 => x < x_1) j i
⊢ ↑toLex a j = ↑toLex b j
[PROOFSTEP]
contrapose! hl
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i✝ : ι
a✝ : β i✝
a b : (i : ι) → β i
h : a < b
i : ι
hi : i ∈ {i | a i ≠ b i}
j : ι
hj : (fun x x_1 => x < x_1) j i
hl : ↑toLex a j ≠ ↑toLex b j
⊢ ∃ x, x ∈ {i | a i ≠ b i} ∧ x < i
[PROOFSTEP]
exact ⟨j, hl, hj⟩
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
⊢ ↑toLex x < ↑toLex (update x i a) ↔ x i < a
[PROOFSTEP]
refine' ⟨_, fun h => toLex_strictMono <| lt_update_self_iff.2 h⟩
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
⊢ ↑toLex x < ↑toLex (update x i a) → x i < a
[PROOFSTEP]
rintro ⟨j, hj, h⟩
[GOAL]
case intro.intro
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → ↑toLex x j_1 = ↑toLex (update x i a) j_1
h : ↑toLex x j < ↑toLex (update x i a) j
⊢ x i < a
[PROOFSTEP]
dsimp at h
[GOAL]
case intro.intro
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → ↑toLex x j_1 = ↑toLex (update x i a) j_1
h : x j < update x i a j
⊢ x i < a
[PROOFSTEP]
obtain rfl : j = i := by
  by_contra H
  rw [update_noteq H] at h
  exact h.false
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → ↑toLex x j_1 = ↑toLex (update x i a) j_1
h : x j < update x i a j
⊢ j = i
[PROOFSTEP]
by_contra H
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → ↑toLex x j_1 = ↑toLex (update x i a) j_1
h : x j < update x i a j
H : ¬j = i
⊢ False
[PROOFSTEP]
rw [update_noteq H] at h
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → ↑toLex x j_1 = ↑toLex (update x i a) j_1
h : x j < x j
H : ¬j = i
⊢ False
[PROOFSTEP]
exact h.false
[GOAL]
case intro.intro
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
j : ι
a : β j
hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → ↑toLex x j_1 = ↑toLex (update x j a) j_1
h : x j < update x j a j
⊢ x j < a
[PROOFSTEP]
rwa [update_same] at h
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
⊢ ↑toLex (update x i a) < ↑toLex x ↔ a < x i
[PROOFSTEP]
refine' ⟨_, fun h => toLex_strictMono <| update_lt_self_iff.2 h⟩
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
⊢ ↑toLex (update x i a) < ↑toLex x → a < x i
[PROOFSTEP]
rintro ⟨j, hj, h⟩
[GOAL]
case intro.intro
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → ↑toLex (update x i a) j_1 = ↑toLex x j_1
h : ↑toLex (update x i a) j < ↑toLex x j
⊢ a < x i
[PROOFSTEP]
dsimp at h
[GOAL]
case intro.intro
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → ↑toLex (update x i a) j_1 = ↑toLex x j_1
h : update x i a j < x j
⊢ a < x i
[PROOFSTEP]
obtain rfl : j = i := by
  by_contra H
  rw [update_noteq H] at h
  exact h.false
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → ↑toLex (update x i a) j_1 = ↑toLex x j_1
h : update x i a j < x j
⊢ j = i
[PROOFSTEP]
by_contra H
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → ↑toLex (update x i a) j_1 = ↑toLex x j_1
h : update x i a j < x j
H : ¬j = i
⊢ False
[PROOFSTEP]
rw [update_noteq H] at h
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
j : ι
hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → ↑toLex (update x i a) j_1 = ↑toLex x j_1
h : x j < x j
H : ¬j = i
⊢ False
[PROOFSTEP]
exact h.false
[GOAL]
case intro.intro
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
j : ι
a : β j
hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → ↑toLex (update x j a) j_1 = ↑toLex x j_1
h : update x j a j < x j
⊢ a < x j
[PROOFSTEP]
rwa [update_same] at h
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
⊢ ↑toLex x ≤ ↑toLex (update x i a) ↔ x i ≤ a
[PROOFSTEP]
simp_rw [le_iff_lt_or_eq, lt_toLex_update_self_iff, toLex_inj, eq_update_self_iff]
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
⊢ ↑toLex (update x i a) ≤ ↑toLex x ↔ a ≤ x i
[PROOFSTEP]
simp_rw [le_iff_lt_or_eq, toLex_update_lt_self_iff, toLex_inj, update_eq_self_iff]
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
⊢ ∀ (a₁ a₂ : Lex ((i : ι) → β i)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro _ a₂ ⟨i, h, hi⟩
[GOAL]
case intro.intro
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
⊢ ∃ a, a₁✝ < a ∧ a < a₂
[PROOFSTEP]
obtain ⟨a, ha₁, ha₂⟩ := exists_between hi
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
⊢ ∃ a, a₁✝ < a ∧ a < a₂
[PROOFSTEP]
classical
refine' ⟨Function.update a₂ _ a, ⟨i, fun j hj => _, _⟩, i, fun j hj => _, _⟩
rw [h j hj]
dsimp only at hj
· rw [Function.update_noteq hj.ne a]
· rwa [Function.update_same i a]
· rw [Function.update_noteq hj.ne a]
· rwa [Function.update_same i a]
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
⊢ ∃ a, a₁✝ < a ∧ a < a₂
[PROOFSTEP]
refine' ⟨Function.update a₂ _ a, ⟨i, fun j hj => _, _⟩, i, fun j hj => _, _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
j : ι
hj : (fun x x_1 => x < x_1) j i
⊢ a₁✝ j = Function.update a₂ i a j
case intro.intro.intro.intro.refine'_2
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
⊢ (fun x x_1 x_2 => x_1 < x_2) i (a₁✝ i) (Function.update a₂ i a i)
case intro.intro.intro.intro.refine'_3
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
j : ι
hj : (fun x x_1 => x < x_1) j i
⊢ Function.update a₂ i a j = a₂ j
case intro.intro.intro.intro.refine'_4
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
⊢ (fun x x_1 x_2 => x_1 < x_2) i (Function.update a₂ i a i) (a₂ i)
[PROOFSTEP]
rw [h j hj]
[GOAL]
case intro.intro.intro.intro.refine'_1
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
j : ι
hj : (fun x x_1 => x < x_1) j i
⊢ a₂ j = Function.update a₂ i a j
case intro.intro.intro.intro.refine'_2
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
⊢ (fun x x_1 x_2 => x_1 < x_2) i (a₁✝ i) (Function.update a₂ i a i)
case intro.intro.intro.intro.refine'_3
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
j : ι
hj : (fun x x_1 => x < x_1) j i
⊢ Function.update a₂ i a j = a₂ j
case intro.intro.intro.intro.refine'_4
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
⊢ (fun x x_1 x_2 => x_1 < x_2) i (Function.update a₂ i a i) (a₂ i)
[PROOFSTEP]
dsimp only at hj
[GOAL]
case intro.intro.intro.intro.refine'_1
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
j : ι
hj : j < i
⊢ a₂ j = Function.update a₂ i a j
[PROOFSTEP]
rw [Function.update_noteq hj.ne a]
[GOAL]
case intro.intro.intro.intro.refine'_2
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
⊢ (fun x x_1 x_2 => x_1 < x_2) i (a₁✝ i) (Function.update a₂ i a i)
[PROOFSTEP]
rwa [Function.update_same i a]
[GOAL]
case intro.intro.intro.intro.refine'_3
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
j : ι
hj : (fun x x_1 => x < x_1) j i
⊢ Function.update a₂ i a j = a₂ j
[PROOFSTEP]
rw [Function.update_noteq hj.ne a]
[GOAL]
case intro.intro.intro.intro.refine'_4
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x x_1 => x < x_1) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
⊢ (fun x x_1 x_2 => x_1 < x_2) i (Function.update a₂ i a i) (a₂ i)
[PROOFSTEP]
rwa [Function.update_same i a]
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
⊢ ∃ b, a < b
[PROOFSTEP]
let ⟨b, hb⟩ := exists_gt (a i)
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ ∃ b, a < b
[PROOFSTEP]
classical exact
  ⟨Function.update a i b, i, fun j hj => (Function.update_noteq hj.ne b a).symm, by rwa [Function.update_same i b]⟩
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ ∃ b, a < b
[PROOFSTEP]
exact ⟨Function.update a i b, i, fun j hj => (Function.update_noteq hj.ne b a).symm, by rwa [Function.update_same i b]⟩
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ (fun x x_1 x_2 => x_1 < x_2) i (a i) (Function.update a i b i)
[PROOFSTEP]
rwa [Function.update_same i b]
[GOAL]
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
α : Type u_3
inst✝² : Preorder ι
inst✝¹ : DecidableEq ι
inst✝ : Preorder α
f : ι → α
i j : ι
h₁ : i ≤ j
h₂ : f j < f i
⊢ (fun x x_1 x_2 => x_1 < x_2) i (↑toLex (f ∘ ↑(Equiv.swap i j)) i) (↑toLex f i)
[PROOFSTEP]
simpa only [Pi.toLex_apply, Function.comp_apply, Equiv.swap_apply_left] using h₂


[GOAL]
q : ℚ
⊢ sqrt (q * q) = |q|
[PROOFSTEP]
rw [sqrt, mul_self_num, mul_self_den, Int.sqrt_eq, Nat.sqrt_eq, abs_def, divInt_ofNat]
[GOAL]
x : ℚ
x✝ : ∃ q, q * q = x
n : ℚ
hn : n * n = x
⊢ sqrt x * sqrt x = x
[PROOFSTEP]
rw [← hn, sqrt_eq, abs_mul_abs_self]


[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
s : { s // 0 ∈ s }
⊢ (fun s => { val := 0 ::ₛ s, property := (_ : 0 ∈ 0 ::ₛ s) }) ((fun s => erase (↑s) 0 (_ : 0 ∈ ↑s)) s) = s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
s : Sym (Fin (succ n)) k
⊢ (fun s => erase (↑s) 0 (_ : 0 ∈ ↑s)) ((fun s => { val := 0 ::ₛ s, property := (_ : 0 ∈ 0 ::ₛ s) }) s) = s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
s : { s // ¬0 ∈ s }
⊢ (fun s => { val := map (Fin.succAbove 0) s, property := (_ : ¬0 ∈ map (Fin.succAbove 0) s) })
      ((fun s => map (Fin.predAbove 0) ↑s) s) =
    s
[PROOFSTEP]
ext1
[GOAL]
case a
α : Type u_1
β : Type u_2
n✝ n k : ℕ
s : { s // ¬0 ∈ s }
⊢ ↑((fun s => { val := map (Fin.succAbove 0) s, property := (_ : ¬0 ∈ map (Fin.succAbove 0) s) })
        ((fun s => map (Fin.predAbove 0) ↑s) s)) =
    ↑s
[PROOFSTEP]
simp only [map_map]
[GOAL]
case a
α : Type u_1
β : Type u_2
n✝ n k : ℕ
s : { s // ¬0 ∈ s }
⊢ map (Fin.succAbove 0 ∘ Fin.predAbove 0) ↑s = ↑s
[PROOFSTEP]
refine (Sym.map_congr fun v hv ↦ ?_).trans (map_id' _)
[GOAL]
case a
α : Type u_1
β : Type u_2
n✝ n k : ℕ
s : { s // ¬0 ∈ s }
v : Fin (succ n + 1)
hv : v ∈ ↑s
⊢ (Fin.succAbove 0 ∘ Fin.predAbove 0) v = v
[PROOFSTEP]
exact Fin.succAbove_predAbove (ne_of_mem_of_not_mem hv s.2)
[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
s : Sym (Fin (succ n)) k
⊢ (fun s => map (Fin.predAbove 0) ↑s)
      ((fun s => { val := map (Fin.succAbove 0) s, property := (_ : ¬0 ∈ map (Fin.succAbove 0) s) }) s) =
    s
[PROOFSTEP]
simp only [map_map, comp_apply, ← Fin.castSucc_zero, Fin.predAbove_succAbove, map_id']
[GOAL]
α : Type u_1
β : Type u_2
n✝ n : ℕ
⊢ Fintype.card (Sym (Fin n) 0) = multichoose n 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
n k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = multichoose 0 (k + 1)
[PROOFSTEP]
rw [multichoose_zero_succ]
[GOAL]
α : Type u_1
β : Type u_2
n k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = 0
[PROOFSTEP]
exact card_eq_zero
[GOAL]
α : Type u_1
β : Type u_2
n k : ℕ
⊢ Fintype.card (Sym (Fin 1) (k + 1)) = multichoose 1 (k + 1)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = multichoose (n + 2) (k + 1)
[PROOFSTEP]
rw [multichoose_succ_succ, ← card_sym_fin_eq_multichoose (n + 1) (k + 1), ← card_sym_fin_eq_multichoose (n + 2) k,
  add_comm (Fintype.card _), ← card_sum]
[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))
[PROOFSTEP]
refine Fintype.card_congr (Equiv.symm ?_)
[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
⊢ Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1) ≃ Sym (Fin (n + 2)) (k + 1)
[PROOFSTEP]
apply (Sym.e1.symm.sumCongr Sym.e2.symm).trans
[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
⊢ { s // 0 ∈ s } ⊕ { s // ¬0 ∈ s } ≃ Sym (Fin (n + 2)) (k + 1)
[PROOFSTEP]
apply Equiv.sumCompl
[GOAL]
α✝ : Type u_1
β : Type u_2
n : ℕ
α : Type u_3
k : ℕ
inst✝¹ : Fintype α
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = multichoose (Fintype.card α) k
[PROOFSTEP]
rw [← card_sym_fin_eq_multichoose]
[GOAL]
α✝ : Type u_1
β : Type u_2
n : ℕ
α : Type u_3
k : ℕ
inst✝¹ : Fintype α
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = Fintype.card (Sym (Fin (Fintype.card α)) k)
[PROOFSTEP]
exact card_congr (equivCongr (equivFin α))
[GOAL]
α✝ : Type u_1
β : Type u_2
n : ℕ
α : Type u_3
inst✝¹ : Fintype α
k : ℕ
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = Nat.choose (Fintype.card α + k - 1) k
[PROOFSTEP]
rw [card_sym_eq_multichoose, Nat.multichoose_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ Finset.card (image Quotient.mk' (Finset.diag s)) = Finset.card s
[PROOFSTEP]
rw [card_image_of_injOn, diag_card]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn Quotient.mk' ↑(Finset.diag s)
[PROOFSTEP]
rintro ⟨x₀, x₁⟩ hx _ _ h
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx : (x₀, x₁) ∈ ↑(Finset.diag s)
x₂✝ : α × α
a✝ : x₂✝ ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' x₂✝
⊢ (x₀, x₁) = x₂✝
[PROOFSTEP]
cases Quotient.eq'.1 h
[GOAL]
case mk.refl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx a✝ : (x₀, x₁) ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' (x₀, x₁)
⊢ (x₀, x₁) = (x₀, x₁)
[PROOFSTEP]
rfl
[GOAL]
case mk.swap
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx : (x₀, x₁) ∈ ↑(Finset.diag s)
a✝ : (x₁, x₀) ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' (x₁, x₀)
⊢ (x₀, x₁) = (x₁, x₀)
[PROOFSTEP]
simp only [mem_coe, mem_diag] at hx
[GOAL]
case mk.swap
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
a✝ : (x₁, x₀) ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' (x₁, x₀)
hx : x₀ ∈ s ∧ x₀ = x₁
⊢ (x₀, x₁) = (x₁, x₀)
[PROOFSTEP]
rw [hx.2]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ 2 * Finset.card (image Quotient.mk' (offDiag s)) = Finset.card (offDiag s)
[PROOFSTEP]
rw [card_eq_sum_card_image (Quotient.mk' : α × α → _), sum_const_nat (Quotient.ind' _), mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ ∀ (a : α × α),
    Quotient.mk'' a ∈ image Quotient.mk' (offDiag s) →
      Finset.card (filter (fun x => Quotient.mk' x = Quotient.mk'' a) (offDiag s)) = 2
[PROOFSTEP]
rintro ⟨x, y⟩ hxy
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
hxy : Quotient.mk'' (x, y) ∈ image Quotient.mk' (offDiag s)
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
[PROOFSTEP]
simp_rw [mem_image, mem_offDiag] at hxy
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
hxy : ∃ a, (a.fst ∈ s ∧ a.snd ∈ s ∧ a.fst ≠ a.snd) ∧ Quotient.mk' a = Quotient.mk'' (x, y)
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
[PROOFSTEP]
obtain ⟨a, ⟨ha₁, ha₂, ha⟩, h⟩ := hxy
[GOAL]
case mk.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
h : Quotient.mk' a = Quotient.mk'' (x, y)
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
[PROOFSTEP]
replace h := Quotient.eq.1 h
[GOAL]
case mk.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
[PROOFSTEP]
obtain ⟨hx, hy, hxy⟩ : x ∈ s ∧ y ∈ s ∧ x ≠ y := by cases h <;> refine' ⟨‹_›, ‹_›, _⟩ <;> [exact ha; exact ha.symm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
⊢ x ∈ s ∧ y ∈ s ∧ x ≠ y
[PROOFSTEP]
cases h <;> refine' ⟨‹_›, ‹_›, _⟩ <;> [exact ha; exact ha.symm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
⊢ x ∈ s ∧ y ∈ s ∧ x ≠ y
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
ha₁ : (x, y).fst ∈ s
ha₂ : (x, y).snd ∈ s
ha : (x, y).fst ≠ (x, y).snd
⊢ x ∈ s ∧ y ∈ s ∧ x ≠ y
[PROOFSTEP]
refine' ⟨‹_›, ‹_›, _⟩
[GOAL]
case swap
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
ha₁ : (y, x).fst ∈ s
ha₂ : (y, x).snd ∈ s
ha : (y, x).fst ≠ (y, x).snd
⊢ x ∈ s ∧ y ∈ s ∧ x ≠ y
[PROOFSTEP]
refine' ⟨‹_›, ‹_›, _⟩
[GOAL]
case refl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
ha₁ : (x, y).fst ∈ s
ha₂ : (x, y).snd ∈ s
ha : (x, y).fst ≠ (x, y).snd
⊢ x ≠ y
[PROOFSTEP]
exact ha
[GOAL]
case swap
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
ha₁ : (y, x).fst ∈ s
ha₂ : (y, x).snd ∈ s
ha : (y, x).fst ≠ (y, x).snd
⊢ x ≠ y
[PROOFSTEP]
exact ha.symm
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
[PROOFSTEP]
have hxy' : y ≠ x := hxy.symm
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
[PROOFSTEP]
have : (s.offDiag.filter fun z => ⟦z⟧ = ⟦(x, y)⟧) = ({(x, y), (y, x)} : Finset _) :=
  by
  ext ⟨x₁, y₁⟩
  rw [mem_filter, mem_insert, mem_singleton, Sym2.eq_iff, Prod.mk.inj_iff, Prod.mk.inj_iff, and_iff_right_iff_imp]
    -- `hxy'` is used in `exact`
  rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;> rw [mem_offDiag] <;> exact ⟨‹_›, ‹_›, ‹_›⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
⊢ filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) = {(x, y), (y, x)}
[PROOFSTEP]
ext ⟨x₁, y₁⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
x₁ y₁ : α
⊢ (x₁, y₁) ∈ filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) ↔
    (x₁, y₁) ∈ {(x, y), (y, x)}
[PROOFSTEP]
rw [mem_filter, mem_insert, mem_singleton, Sym2.eq_iff, Prod.mk.inj_iff, Prod.mk.inj_iff, and_iff_right_iff_imp]
  -- `hxy'` is used in `exact`
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
x₁ y₁ : α
⊢ x₁ = x ∧ y₁ = y ∨ x₁ = y ∧ y₁ = x → (x₁, y₁) ∈ offDiag s
[PROOFSTEP]
rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
[GOAL]
case a.mk.inl.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
x₁ y₁ : α
hx : x₁ ∈ s
hy : y₁ ∈ s
h : a ≈ (x₁, y₁)
hxy : x₁ ≠ y₁
hxy' : y₁ ≠ x₁
⊢ (x₁, y₁) ∈ offDiag s
[PROOFSTEP]
rw [mem_offDiag]
[GOAL]
case a.mk.inr.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
x₁ y₁ : α
hy : x₁ ∈ s
hx : y₁ ∈ s
h : a ≈ (y₁, x₁)
hxy : y₁ ≠ x₁
hxy' : x₁ ≠ y₁
⊢ (x₁, y₁) ∈ offDiag s
[PROOFSTEP]
rw [mem_offDiag]
[GOAL]
case a.mk.inl.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
x₁ y₁ : α
hx : x₁ ∈ s
hy : y₁ ∈ s
h : a ≈ (x₁, y₁)
hxy : x₁ ≠ y₁
hxy' : y₁ ≠ x₁
⊢ (x₁, y₁).fst ∈ s ∧ (x₁, y₁).snd ∈ s ∧ (x₁, y₁).fst ≠ (x₁, y₁).snd
[PROOFSTEP]
exact ⟨‹_›, ‹_›, ‹_›⟩
[GOAL]
case a.mk.inr.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
x₁ y₁ : α
hy : x₁ ∈ s
hx : y₁ ∈ s
h : a ≈ (y₁, x₁)
hxy : y₁ ≠ x₁
hxy' : x₁ ≠ y₁
⊢ (x₁, y₁).fst ∈ s ∧ (x₁, y₁).snd ∈ s ∧ (x₁, y₁).fst ≠ (x₁, y₁).snd
[PROOFSTEP]
exact ⟨‹_›, ‹_›, ‹_›⟩
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) = {(x, y), (y, x)}
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
[PROOFSTEP]
dsimp [Quotient.mk', Quotient.mk''_eq_mk]
  -- Porting note: Added `dsimp`
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) = {(x, y), (y, x)}
⊢ Finset.card (filter (fun x_1 => Quotient.mk (Rel.setoid α) x_1 = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s)) = 2
[PROOFSTEP]
rw [this, card_insert_of_not_mem, card_singleton]
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) = {(x, y), (y, x)}
⊢ ¬(x, y) ∈ {(y, x)}
[PROOFSTEP]
simp only [not_and, Prod.mk.inj_iff, mem_singleton]
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) = {(x, y), (y, x)}
⊢ x = y → ¬y = x
[PROOFSTEP]
exact fun _ => hxy'
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ Finset.card (image Quotient.mk' (offDiag s)) = Nat.choose (Finset.card s) 2
[PROOFSTEP]
rw [Nat.choose_two_right, mul_tsub, mul_one, ← offDiag_card,
  Nat.div_eq_of_eq_mul_right zero_lt_two (two_mul_card_image_offDiag s).symm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // IsDiag a } = Fintype.card α
[PROOFSTEP]
convert card_image_diag (univ : Finset α)
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // IsDiag a } = Finset.card (image Quotient.mk' (Finset.diag univ))
[PROOFSTEP]
simp_rw [Quotient.mk', ← Quotient.mk''_eq_mk]
  -- Porting note: Added `simp_rw`
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // IsDiag a } = Finset.card (image (fun a => Quotient.mk'' a) (Finset.diag univ))
[PROOFSTEP]
rw [Fintype.card_of_subtype, ← filter_image_quotient_mk''_isDiag]
[GOAL]
case h.e'_2.H
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Sym2 α), x ∈ filter IsDiag (image Quotient.mk'' (univ ×ˢ univ)) ↔ IsDiag x
[PROOFSTEP]
rintro x
[GOAL]
case h.e'_2.H
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ filter IsDiag (image Quotient.mk'' (univ ×ˢ univ)) ↔ IsDiag x
[PROOFSTEP]
rw [mem_filter, univ_product_univ, mem_image]
[GOAL]
case h.e'_2.H
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ (∃ a, a ∈ univ ∧ Quotient.mk'' a = x) ∧ IsDiag x ↔ IsDiag x
[PROOFSTEP]
obtain ⟨a, ha⟩ := Quotient.exists_rep x
[GOAL]
case h.e'_2.H.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
a : α × α
ha : Quotient.mk (Rel.setoid α) a = x
⊢ (∃ a, a ∈ univ ∧ Quotient.mk'' a = x) ∧ IsDiag x ↔ IsDiag x
[PROOFSTEP]
exact and_iff_right ⟨a, mem_univ _, ha⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬IsDiag a } = Nat.choose (Fintype.card α) 2
[PROOFSTEP]
convert card_image_offDiag (univ : Finset α)
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬IsDiag a } = Finset.card (image Quotient.mk' (offDiag univ))
[PROOFSTEP]
simp_rw [Quotient.mk', ← Quotient.mk''_eq_mk]
  -- Porting note: Added `simp_rw`
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬IsDiag a } = Finset.card (image (fun a => Quotient.mk'' a) (offDiag univ))
[PROOFSTEP]
rw [Fintype.card_of_subtype, ← filter_image_quotient_mk''_not_isDiag]
[GOAL]
case h.e'_2.H
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Sym2 α), x ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (univ ×ˢ univ)) ↔ ¬IsDiag x
[PROOFSTEP]
rintro x
[GOAL]
case h.e'_2.H
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (univ ×ˢ univ)) ↔ ¬IsDiag x
[PROOFSTEP]
rw [mem_filter, univ_product_univ, mem_image]
[GOAL]
case h.e'_2.H
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ (∃ a, a ∈ univ ∧ Quotient.mk'' a = x) ∧ ¬IsDiag x ↔ ¬IsDiag x
[PROOFSTEP]
obtain ⟨a, ha⟩ := Quotient.exists_rep x
[GOAL]
case h.e'_2.H.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
a : α × α
ha : Quotient.mk (Rel.setoid α) a = x
⊢ (∃ a, a ∈ univ ∧ Quotient.mk'' a = x) ∧ ¬IsDiag x ↔ ¬IsDiag x
[PROOFSTEP]
exact and_iff_right ⟨a, mem_univ _, ha⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ Finset.card (Finset.sym2 s) = Finset.card s * (Finset.card s + 1) / 2
[PROOFSTEP]
rw [← image_diag_union_image_offDiag, card_union_eq, Sym2.card_image_diag, Sym2.card_image_offDiag,
  Nat.choose_two_right, add_comm, ← Nat.triangle_succ, Nat.succ_sub_one, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ Disjoint (image Quotient.mk' (Finset.diag s)) (image Quotient.mk' (offDiag s))
[PROOFSTEP]
rw [disjoint_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ ∀ ⦃a : Quotient (Rel.setoid α)⦄, a ∈ image Quotient.mk' (Finset.diag s) → ¬a ∈ image Quotient.mk' (offDiag s)
[PROOFSTEP]
rintro m ha hb
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
m : Quotient (Rel.setoid α)
ha : m ∈ image Quotient.mk' (Finset.diag s)
hb : m ∈ image Quotient.mk' (offDiag s)
⊢ False
[PROOFSTEP]
rw [mem_image] at ha hb
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
m : Quotient (Rel.setoid α)
ha : ∃ a, a ∈ Finset.diag s ∧ Quotient.mk' a = m
hb : ∃ a, a ∈ offDiag s ∧ Quotient.mk' a = m
⊢ False
[PROOFSTEP]
obtain ⟨⟨a, ha, rfl⟩, ⟨b, hb, hab⟩⟩ := ha, hb
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha : a ∈ Finset.diag s
b : α × α
hb : b ∈ offDiag s
hab : Quotient.mk' b = Quotient.mk' a
⊢ False
[PROOFSTEP]
refine' not_isDiag_mk'_of_mem_offDiag hb _
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha : a ∈ Finset.diag s
b : α × α
hb : b ∈ offDiag s
hab : Quotient.mk' b = Quotient.mk' a
⊢ IsDiag (Quotient.mk (Rel.setoid α) b)
[PROOFSTEP]
dsimp [Quotient.mk'] at hab
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha : a ∈ Finset.diag s
b : α × α
hb : b ∈ offDiag s
hab : Quotient.mk (Rel.setoid α) b = Quotient.mk (Rel.setoid α) a
⊢ IsDiag (Quotient.mk (Rel.setoid α) b)
[PROOFSTEP]
rw [hab]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha : a ∈ Finset.diag s
b : α × α
hb : b ∈ offDiag s
hab : Quotient.mk (Rel.setoid α) b = Quotient.mk (Rel.setoid α) a
⊢ IsDiag (Quotient.mk (Rel.setoid α) a)
[PROOFSTEP]
exact isDiag_mk'_of_mem_diag ha


[GOAL]
⊢ Denumerable ℚ
[PROOFSTEP]
let T := { x : ℤ × ℕ // 0 < x.2 ∧ x.1.natAbs.coprime x.2 }
[GOAL]
T : Type := { x // 0 < x.snd ∧ Nat.coprime (Int.natAbs x.fst) x.snd }
⊢ Denumerable ℚ
[PROOFSTEP]
letI : Infinite T := Infinite.of_injective _ denumerable_aux.injective
[GOAL]
T : Type := { x // 0 < x.snd ∧ Nat.coprime (Int.natAbs x.fst) x.snd }
this : Infinite T := Infinite.of_injective (↑Rat.denumerable_aux) (Equiv.injective Rat.denumerable_aux)
⊢ Denumerable ℚ
[PROOFSTEP]
letI : Encodable T := Subtype.encodable
[GOAL]
T : Type := { x // 0 < x.snd ∧ Nat.coprime (Int.natAbs x.fst) x.snd }
this✝ : Infinite T := Infinite.of_injective (↑Rat.denumerable_aux) (Equiv.injective Rat.denumerable_aux)
this : Encodable T := Subtype.encodable
⊢ Denumerable ℚ
[PROOFSTEP]
letI : Denumerable T := ofEncodableOfInfinite T
[GOAL]
T : Type := { x // 0 < x.snd ∧ Nat.coprime (Int.natAbs x.fst) x.snd }
this✝¹ : Infinite T := Infinite.of_injective (↑Rat.denumerable_aux) (Equiv.injective Rat.denumerable_aux)
this✝ : Encodable T := Subtype.encodable
this : Denumerable T := ofEncodableOfInfinite T
⊢ Denumerable ℚ
[PROOFSTEP]
exact Denumerable.ofEquiv T denumerable_aux
[GOAL]
⊢ #ℚ = ℵ₀
[PROOFSTEP]
simp only [mk_eq_aleph0]