[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α × α
⊢ Rel α x y → Rel α y x
[PROOFSTEP]
aesop (rule_sets [Sym2])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : α × α
a : Rel α x y
b : Rel α y z
⊢ Rel α x z
[PROOFSTEP]
aesop (rule_sets [Sym2])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x y z w : α
⊢ Rel α (x, y) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
[PROOFSTEP]
aesop (rule_sets [Sym2])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : Sym2 α → Sym2 β → Prop
i : Sym2 α
j : Sym2 β
hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))
⊢ ∀ (a : α × α) (b : β × β), f (Quotient.mk (Rel.setoid α) a) (Quotient.mk (Rel.setoid β) b)
[PROOFSTEP]
intro ⟨a₁, a₂⟩ ⟨b₁, b₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : Sym2 α → Sym2 β → Prop
i : Sym2 α
j : Sym2 β
hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))
a₁ a₂ : α
b₁ b₂ : β
⊢ f (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))
[PROOFSTEP]
exact hf _ _ _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (b, a)
[PROOFSTEP]
rw [Quotient.eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ (a, b) ≈ (b, a)
[PROOFSTEP]
apply Rel.swap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α × α
⊢ Quotient.mk (Rel.setoid α) (Prod.swap p) = Quotient.mk (Rel.setoid α) p
[PROOFSTEP]
cases p
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
fst✝ snd✝ : α
⊢ Quotient.mk (Rel.setoid α) (Prod.swap (fst✝, snd✝)) = Quotient.mk (Rel.setoid α) (fst✝, snd✝)
[PROOFSTEP]
exact eq_swap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (a, c) ↔ b = c
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (a, c) → b = c
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ b = c → Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (a, c)
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (a, c)
⊢ b = c
[PROOFSTEP]
rw [Quotient.eq] at h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
h : (a, b) ≈ (a, c)
⊢ b = c
[PROOFSTEP]
cases h
[GOAL]
case mp.refl
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ b = b
[PROOFSTEP]
rfl
[GOAL]
case mp.swap
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
h : b = c
⊢ Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (a, c)
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a) ↔ b = c
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a) → b = c
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ b = c → Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a)
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
h : Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a)
⊢ b = c
[PROOFSTEP]
rw [Quotient.eq] at h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
h : (b, a) ≈ (c, a)
⊢ b = c
[PROOFSTEP]
cases h
[GOAL]
case mp.refl
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ b = b
[PROOFSTEP]
rfl
[GOAL]
case mp.swap
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
h : b = c
⊢ Quotient.mk (Rel.setoid α) (b, a) = Quotient.mk (Rel.setoid α) (c, a)
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x y z w : α
⊢ Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α × α
⊢ Quotient.mk (Rel.setoid α) p = Quotient.mk (Rel.setoid α) q ↔ p = q ∨ p = Prod.swap q
[PROOFSTEP]
cases p
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
q : α × α
fst✝ snd✝ : α
⊢ Quotient.mk (Rel.setoid α) (fst✝, snd✝) = Quotient.mk (Rel.setoid α) q ↔ (fst✝, snd✝) = q ∨ (fst✝, snd✝) = Prod.swap q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
fst✝¹ snd✝¹ fst✝ snd✝ : α
⊢ Quotient.mk (Rel.setoid α) (fst✝¹, snd✝¹) = Quotient.mk (Rel.setoid α) (fst✝, snd✝) ↔
    (fst✝¹, snd✝¹) = (fst✝, snd✝) ∨ (fst✝¹, snd✝¹) = Prod.swap (fst✝, snd✝)
[PROOFSTEP]
simp only [eq_iff, Prod.mk.inj_iff, Prod.swap_prod_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
⊢ ∀ (a b : α × α), a ≈ b → uncurry (↑f) a = uncurry (↑f) b
[PROOFSTEP]
rintro _ _ ⟨⟩
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
x✝ y✝ : α
⊢ uncurry ↑f (x✝, y✝) = uncurry ↑f (x✝, y✝)
case swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
x✝ y✝ : α
⊢ uncurry ↑f (x✝, y✝) = uncurry ↑f (y✝, x✝)
[PROOFSTEP]
exacts [rfl, f.prop _ _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
⊢ ∀ (a₁ : α × α) (b₁ : β × β) (a₂ : α × α) (b₂ : β × β),
    a₁ ≈ a₂ → b₁ ≈ b₂ → (fun a b => ↑f a.fst a.snd b.fst b.snd) a₁ b₁ = (fun a b => ↑f a.fst a.snd b.fst b.snd) a₂ b₂
[PROOFSTEP]
rintro _ _ _ _ ⟨⟩ ⟨⟩
[GOAL]
case refl.refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ (fun a b => ↑f a.fst a.snd b.fst b.snd) (x✝¹, y✝¹) (x✝, y✝) =
    (fun a b => ↑f a.fst a.snd b.fst b.snd) (x✝¹, y✝¹) (x✝, y✝)
case refl.swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ (fun a b => ↑f a.fst a.snd b.fst b.snd) (x✝¹, y✝¹) (x✝, y✝) =
    (fun a b => ↑f a.fst a.snd b.fst b.snd) (x✝¹, y✝¹) (y✝, x✝)
case swap.refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ (fun a b => ↑f a.fst a.snd b.fst b.snd) (x✝¹, y✝¹) (x✝, y✝) =
    (fun a b => ↑f a.fst a.snd b.fst b.snd) (y✝¹, x✝¹) (x✝, y✝)
case swap.swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x✝¹ y✝¹ : α
x✝ y✝ : β
⊢ (fun a b => ↑f a.fst a.snd b.fst b.snd) (x✝¹, y✝¹) (x✝, y✝) =
    (fun a b => ↑f a.fst a.snd b.fst b.snd) (y✝¹, x✝¹) (y✝, x✝)
[PROOFSTEP]
exacts [rfl, (f.2 _ _ _ _).2, (f.2 _ _ _ _).1, (f.2 _ _ _ _).1.trans (f.2 _ _ _ _).2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₁ a₂ b₁ b₂ =
      (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₂ a₁ b₁ b₂ ∧
    (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₁ a₂ b₁ b₂ =
      (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₁ a₂ b₂ b₁
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₁ a₂ b₁ b₂ =
    (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₂ a₁ b₁ b₂
case right
α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₁ a₂ b₁ b₂ =
    (fun a₁ a₂ b₁ b₂ => F (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid β) (b₁, b₂))) a₁ a₂ b₂ b₁
[PROOFSTEP]
exacts [congr_arg₂ F eq_swap rfl, congr_arg₂ F rfl eq_swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
⊢ ((fun x x_1 => x ≈ x_1) ⇒ fun x x_1 => x ≈ x_1) (Prod.map f f) (Prod.map f f)
[PROOFSTEP]
intro _ _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a✝ b✝ : α × α
h : a✝ ≈ b✝
⊢ Prod.map f f a✝ ≈ Prod.map f f b✝
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x✝ y✝ : α
⊢ Prod.map f f (x✝, y✝) ≈ Prod.map f f (x✝, y✝)
[PROOFSTEP]
constructor
[GOAL]
case swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x✝ y✝ : α
⊢ Prod.map f f (x✝, y✝) ≈ Prod.map f f (y✝, x✝)
[PROOFSTEP]
apply Rel.swap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ map id = id
[PROOFSTEP]
ext ⟨⟨x, y⟩⟩
[GOAL]
case h.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym2 α
x y : α
⊢ map id (Quot.mk Setoid.r (x, y)) = id (Quot.mk Setoid.r (x, y))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
⊢ map (g ∘ f) = map g ∘ map f
[PROOFSTEP]
ext ⟨⟨x, y⟩⟩
[GOAL]
case h.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x✝ : Sym2 α
x y : α
⊢ map (g ∘ f) (Quot.mk Setoid.r (x, y)) = (map g ∘ map f) (Quot.mk Setoid.r (x, y))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x : Sym2 α
⊢ map g (map f x) = map (g ∘ f) x
[PROOFSTEP]
revert x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
⊢ ∀ (x : Sym2 α), map g (map f x) = map (g ∘ f) x
[PROOFSTEP]
apply Sym2.ind
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
⊢ ∀ (x y : α), map g (map f (Quotient.mk (Rel.setoid α) (x, y))) = map (g ∘ f) (Quotient.mk (Rel.setoid α) (x, y))
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
⊢ Injective (map f)
[PROOFSTEP]
intro z z'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
z z' : Sym2 α
⊢ map f z = map f z' → z = z'
[PROOFSTEP]
refine' Quotient.ind₂ (fun z z' => _) z z'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
z✝ z'✝ : Sym2 α
z z' : α × α
⊢ map f (Quotient.mk (Rel.setoid α) z) = map f (Quotient.mk (Rel.setoid α) z') →
    Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) z'
[PROOFSTEP]
cases' z with x y
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
z z'✝ : Sym2 α
z' : α × α
x y : α
⊢ map f (Quotient.mk (Rel.setoid α) (x, y)) = map f (Quotient.mk (Rel.setoid α) z') →
    Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) z'
[PROOFSTEP]
cases' z' with x' y'
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ map f (Quotient.mk (Rel.setoid α) (x, y)) = map f (Quotient.mk (Rel.setoid α) (x', y')) →
    Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
[PROOFSTEP]
repeat' rw [map_pair_eq, eq_iff]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ map f (Quotient.mk (Rel.setoid α) (x, y)) = map f (Quotient.mk (Rel.setoid α) (x', y')) →
    Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
[PROOFSTEP]
rw [map_pair_eq, eq_iff]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ Quotient.mk (Rel.setoid β) (f x, f y) = map f (Quotient.mk (Rel.setoid α) (x', y')) →
    x = x' ∧ y = y' ∨ x = y' ∧ y = x'
[PROOFSTEP]
rw [map_pair_eq, eq_iff]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ f x = f x' ∧ f y = f y' ∨ f x = f y' ∧ f y = f x' → x = x' ∧ y = y' ∨ x = y' ∧ y = x'
[PROOFSTEP]
rw [map_pair_eq, eq_iff]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ f x = f x' ∧ f y = f y' ∨ f x = f y' ∧ f y = f x' → x = x' ∧ y = y' ∨ x = y' ∧ y = x'
[PROOFSTEP]
rintro (h | h)
[GOAL]
case mk.mk.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
h : f x = f x' ∧ f y = f y'
⊢ x = x' ∧ y = y' ∨ x = y' ∧ y = x'
[PROOFSTEP]
simp [hinj h.1, hinj h.2]
[GOAL]
case mk.mk.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
h : f x = f y' ∧ f y = f x'
⊢ x = x' ∧ y = y' ∨ x = y' ∧ y = x'
[PROOFSTEP]
simp [hinj h.1, hinj h.2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (b, c)) → a = b ∨ a = c
[PROOFSTEP]
rintro ⟨_, h⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
a b c w✝ : α
h : Quotient.mk (Rel.setoid α) (b, c) = Quotient.mk (Rel.setoid α) (a, w✝)
⊢ a = b ∨ a = c
[PROOFSTEP]
rw [eq_iff] at h
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
a b c w✝ : α
h : b = a ∧ c = w✝ ∨ b = w✝ ∧ c = a
⊢ a = b ∨ a = c
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b c : α
⊢ a = b ∨ a = c → Sym2.Mem a (Quotient.mk (Rel.setoid α) (b, c))
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
a c : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (a, c))
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (b, a))
[PROOFSTEP]
rw [eq_swap]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ Sym2.Mem a (Quotient.mk (Rel.setoid α) (a, b))
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h : (fun z => {x | Sym2.Mem x z}) z = (fun z => {x | Sym2.Mem x z}) z'
⊢ z = z'
[PROOFSTEP]
simp only [Set.ext_iff, Set.mem_setOf_eq] at h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
⊢ z = z'
[PROOFSTEP]
induction' z using Sym2.ind with x y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h✝ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
x y : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 z'
⊢ Quotient.mk (Rel.setoid α) (x, y) = z'
[PROOFSTEP]
induction' z' using Sym2.ind with x' y'
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h✝² : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
x y : α
h✝¹ : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 z'
x' y' : α
h✝ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x', y'))
⊢ Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
[PROOFSTEP]
have hx := h x
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h✝² : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
x y : α
h✝¹ : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 z'
x' y' : α
h✝ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x', y'))
hx : Sym2.Mem x (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
⊢ Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
[PROOFSTEP]
have hy := h y
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h✝² : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
x y : α
h✝¹ : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 z'
x' y' : α
h✝ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x', y'))
hx : Sym2.Mem x (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
hy : Sym2.Mem y (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem y (Quotient.mk (Rel.setoid α) (x', y'))
⊢ Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
[PROOFSTEP]
have hx' := h x'
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h✝² : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
x y : α
h✝¹ : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 z'
x' y' : α
h✝ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x', y'))
hx : Sym2.Mem x (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
hy : Sym2.Mem y (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem y (Quotient.mk (Rel.setoid α) (x', y'))
hx' : Sym2.Mem x' (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x' (Quotient.mk (Rel.setoid α) (x', y'))
⊢ Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
[PROOFSTEP]
have hy' := h y'
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h✝² : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
x y : α
h✝¹ : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 z'
x' y' : α
h✝ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x', y'))
hx : Sym2.Mem x (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
hy : Sym2.Mem y (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem y (Quotient.mk (Rel.setoid α) (x', y'))
hx' : Sym2.Mem x' (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x' (Quotient.mk (Rel.setoid α) (x', y'))
hy' : Sym2.Mem y' (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem y' (Quotient.mk (Rel.setoid α) (x', y'))
⊢ Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
[PROOFSTEP]
simp only [mem_iff', eq_self_iff_true, or_true_iff, iff_true_iff, true_or_iff, true_iff_iff] at hx hy hx' hy'
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h✝² : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
x y : α
h✝¹ : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 z'
x' y' : α
h✝ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x (Quotient.mk (Rel.setoid α) (x', y'))
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x, y)) ↔ Sym2.Mem x_1 (Quotient.mk (Rel.setoid α) (x', y'))
hx : x = x' ∨ x = y'
hy : y = x' ∨ y = y'
hx' : x' = x ∨ x' = y
hy' : y' = x ∨ y' = y
⊢ Quotient.mk (Rel.setoid α) (x, y) = Quotient.mk (Rel.setoid α) (x', y')
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : Sym2 α
⊢ e = Quotient.mk (Rel.setoid α) ((Quotient.out e).fst, (Quotient.out e).snd)
[PROOFSTEP]
rw [Prod.mk.eta, e.out_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : Sym2 α
⊢ e = Quotient.mk (Rel.setoid α) ((Quotient.out e).snd, (Quotient.out e).fst)
[PROOFSTEP]
rw [eq_swap, Prod.mk.eta, e.out_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
a b : α
⊢ (∀ (c : α), c ∈ Quotient.mk (Rel.setoid α) (a, b) → p c) ↔ p a ∧ p b
[PROOFSTEP]
refine' ⟨fun h => ⟨h _ <| mem_mk''_left _ _, h _ <| mem_mk''_right _ _⟩, fun h c hc => _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
a b : α
h : p a ∧ p b
c : α
hc : c ∈ Quotient.mk (Rel.setoid α) (a, b)
⊢ p c
[PROOFSTEP]
obtain rfl | rfl := Sym2.mem_iff.1 hc
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
b c : α
h : p c ∧ p b
hc : c ∈ Quotient.mk (Rel.setoid α) (c, b)
⊢ p c
[PROOFSTEP]
exact h.1
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
a c : α
h : p a ∧ p c
hc : c ∈ Quotient.mk (Rel.setoid α) (a, c)
⊢ p c
[PROOFSTEP]
exact h.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
h : a ∈ z
⊢ Quotient.mk (Rel.setoid α) (a, Mem.other h) = z
[PROOFSTEP]
erw [← Classical.choose_spec h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z
[PROOFSTEP]
convert mem_mk''_right a <| Mem.other h
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
h : a ∈ z
⊢ z = Quotient.mk (Rel.setoid α) (a, Mem.other h)
[PROOFSTEP]
rw [other_spec h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z ↔ z = Quotient.mk (Rel.setoid α) (x, y)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z → z = Quotient.mk (Rel.setoid α) (x, y)
[PROOFSTEP]
induction' z using Sym2.ind with x' y'
[GOAL]
case mp.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
hne : x ≠ y
x' y' : α
⊢ x ∈ Quotient.mk (Rel.setoid α) (x', y') ∧ y ∈ Quotient.mk (Rel.setoid α) (x', y') →
    Quotient.mk (Rel.setoid α) (x', y') = Quotient.mk (Rel.setoid α) (x, y)
[PROOFSTEP]
rw [mem_iff, mem_iff]
[GOAL]
case mp.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
hne : x ≠ y
x' y' : α
⊢ (x = x' ∨ x = y') ∧ (y = x' ∨ y = y') → Quotient.mk (Rel.setoid α) (x', y') = Quotient.mk (Rel.setoid α) (x, y)
[PROOFSTEP]
aesop
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
z : Sym2 α
hne : x ≠ y
⊢ z = Quotient.mk (Rel.setoid α) (x, y) → x ∈ z ∧ y ∈ z
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
hne : x ≠ y
⊢ x ∈ Quotient.mk (Rel.setoid α) (x, y) ∧ y ∈ Quotient.mk (Rel.setoid α) (x, y)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
b : β
z : Sym2 α
⊢ b ∈ map f z ↔ ∃ a, a ∈ z ∧ f a = b
[PROOFSTEP]
induction' z using Sym2.ind with x y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
b : β
x y : α
⊢ b ∈ map f (Quotient.mk (Rel.setoid α) (x, y)) ↔ ∃ a, a ∈ Quotient.mk (Rel.setoid α) (x, y) ∧ f a = b
[PROOFSTEP]
simp only [map, Quotient.map_mk, Prod.map_mk, mem_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
b : β
x y : α
⊢ b = f x ∨ b = f y ↔ ∃ a, (a = x ∨ a = y) ∧ f a = b
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
b : β
x y : α
⊢ b = f x ∨ b = f y → ∃ a, (a = x ∨ a = y) ∧ f a = b
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case h.mp.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x y : α
⊢ ∃ a, (a = x ∨ a = y) ∧ f a = f x
[PROOFSTEP]
exact ⟨x, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x y : α
⊢ (x = x ∨ x = y) ∧ f x = f x
[PROOFSTEP]
simp
[GOAL]
case h.mp.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x y : α
⊢ ∃ a, (a = x ∨ a = y) ∧ f a = f y
[PROOFSTEP]
exact ⟨y, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x y : α
⊢ (y = x ∨ y = y) ∧ f y = f y
[PROOFSTEP]
simp
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
b : β
x y : α
⊢ (∃ a, (a = x ∨ a = y) ∧ f a = b) → b = f x ∨ b = f y
[PROOFSTEP]
rintro ⟨w, rfl | rfl, rfl⟩
[GOAL]
case h.mpr.intro.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
y w : α
⊢ f w = f w ∨ f w = f y
[PROOFSTEP]
simp
[GOAL]
case h.mpr.intro.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x w : α
⊢ f w = f x ∨ f w = f w
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
⊢ map f s = map g s
[PROOFSTEP]
ext y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
y : β
⊢ y ∈ map f s ↔ y ∈ map g s
[PROOFSTEP]
simp only [mem_map]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
y : β
⊢ (∃ a, a ∈ s ∧ f a = y) ↔ ∃ a, a ∈ s ∧ g a = y
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
y : β
⊢ (∃ a, a ∈ s ∧ f a = y) → ∃ a, a ∈ s ∧ g a = y
[PROOFSTEP]
rintro ⟨w, hw, rfl⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
w : α
hw : w ∈ s
⊢ ∃ a, a ∈ s ∧ g a = f w
[PROOFSTEP]
exact ⟨w, hw, by simp [hw, h]⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
w : α
hw : w ∈ s
⊢ g w = f w
[PROOFSTEP]
simp [hw, h]
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
y : β
⊢ (∃ a, a ∈ s ∧ g a = y) → ∃ a, a ∈ s ∧ f a = y
[PROOFSTEP]
rintro ⟨w, hw, rfl⟩
[GOAL]
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
w : α
hw : w ∈ s
⊢ ∃ a, a ∈ s ∧ f a = g w
[PROOFSTEP]
exact ⟨w, hw, by simp [hw, h]⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Sym2 α
h : ∀ (x : α), x ∈ s → f x = g x
w : α
hw : w ∈ s
⊢ f w = g w
[PROOFSTEP]
simp [hw, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
h : diag x = diag y
⊢ x = y
[PROOFSTEP]
cases Quotient.exact h
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
x : α
h : diag x = diag x
⊢ x = x
[PROOFSTEP]
rfl
[GOAL]
case swap
α : Type u_1
β : Type u_2
γ : Type u_3
x : α
h : diag x = diag x
⊢ x = x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
⊢ IsDiag z → z ∈ Set.range diag
[PROOFSTEP]
induction' z using Sym2.ind with x y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
⊢ IsDiag (Quotient.mk (Rel.setoid α) (x, y)) → Quotient.mk (Rel.setoid α) (x, y) ∈ Set.range diag
[PROOFSTEP]
rintro (rfl : x = y)
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
x : α
⊢ Quotient.mk (Rel.setoid α) (x, x) ∈ Set.range diag
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝ : DecidableEq α
⊢ DecidablePred IsDiag
[PROOFSTEP]
refine' fun z => Quotient.recOnSubsingleton z fun a => _
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝ : DecidableEq α
z : Sym2 α
a : α × α
⊢ Decidable (IsDiag (Quotient.mk (Rel.setoid α) a))
[PROOFSTEP]
erw [isDiag_iff_proj_eq]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝ : DecidableEq α
z : Sym2 α
a : α × α
⊢ Decidable (a.fst = a.snd)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
hd : ¬IsDiag z
h : a ∈ z
⊢ Mem.other h ≠ a
[PROOFSTEP]
contrapose! hd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
⊢ IsDiag z
[PROOFSTEP]
have h' := Sym2.other_spec h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : Quotient.mk (Rel.setoid α) (a, Mem.other h) = z
⊢ IsDiag z
[PROOFSTEP]
rw [hd] at h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : Quotient.mk (Rel.setoid α) (a, a) = z
⊢ IsDiag z
[PROOFSTEP]
rw [← h']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : Quotient.mk (Rel.setoid α) (a, a) = z
⊢ IsDiag (Quotient.mk (Rel.setoid α) (a, a))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
⊢ fromRel (_ : ∀ (x y : α), ⊥ x y → ⊥ x y) = ∅
[PROOFSTEP]
apply Set.eq_empty_of_forall_not_mem fun e => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
⊢ ∀ (e : Sym2 α), ¬e ∈ fromRel (_ : ∀ (x y : α), ⊥ x y → ⊥ x y)
[PROOFSTEP]
apply Sym2.ind
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
⊢ ∀ (x y : α), ¬Quotient.mk (Rel.setoid α) (x, y) ∈ fromRel (_ : ∀ (x y : α), ⊥ x y → ⊥ x y)
[PROOFSTEP]
simp [-Set.bot_eq_empty, Prop.bot_eq_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
⊢ fromRel (_ : ∀ (x y : α), ⊤ x y → ⊤ x y) = Set.univ
[PROOFSTEP]
apply Set.eq_univ_of_forall fun e => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
⊢ ∀ (e : Sym2 α), e ∈ fromRel (_ : ∀ (x y : α), ⊤ x y → ⊤ x y)
[PROOFSTEP]
apply Sym2.ind
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
⊢ ∀ (x y : α), Quotient.mk (Rel.setoid α) (x, y) ∈ fromRel (_ : ∀ (x y : α), ⊤ x y → ⊤ x y)
[PROOFSTEP]
simp [-Set.top_eq_univ, Prop.top_eq_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
sym : Symmetric r
⊢ Irreflexive r → ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬IsDiag z
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
sym : Symmetric r
h : Irreflexive r
⊢ ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬IsDiag z
[PROOFSTEP]
apply Sym2.ind
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
sym : Symmetric r
h : Irreflexive r
⊢ ∀ (x y : α), Quotient.mk (Rel.setoid α) (x, y) ∈ fromRel sym → ¬IsDiag (Quotient.mk (Rel.setoid α) (x, y))
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : Set (Sym2 α)
x y : α
⊢ ToRel s x y → ToRel s y x
[PROOFSTEP]
simp [eq_swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
⊢ [a₁, b₁] ~ [a₂, b₂] → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
[PROOFSTEP]
simp [← Multiset.coe_eq_coe, ← Multiset.cons_coe, Multiset.cons_eq_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = a₂
h₂ : b₁ = b₂
⊢ [a₁, b₁] ~ [a₂, b₂]
[PROOFSTEP]
rw [h₁, h₂]
[GOAL]

[PROOFSTEP]
first
| done
| apply List.Perm.swap'; rfl
[GOAL]

[PROOFSTEP]
done
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [a₁, b₁] ~ [a₂, b₂]
[PROOFSTEP]
rw [h₁, h₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂] ~ [a₂, b₂]
[PROOFSTEP]
first
| done
| apply List.Perm.swap'; rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂] ~ [a₂, b₂]
[PROOFSTEP]
done
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂] ~ [a₂, b₂]
[PROOFSTEP]
apply List.Perm.swap'
[GOAL]
case p
α : Type u_1
β : Type u_2
γ : Type u_3
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [] ~ []
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ((fun x x_1 => x ≈ x_1) ⇒ fun x x_1 => x ≈ x_1)
    (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
    fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) }
[PROOFSTEP]
rintro _ _ ⟨_⟩
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ y✝ : α
⊢ (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (x✝, y✝) ≈
    (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (x✝, y✝)
[PROOFSTEP]
constructor
[GOAL]
case refl.a
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ y✝ : α
⊢ [(x✝, y✝).snd] ~ [(x✝, y✝).snd]
[PROOFSTEP]
apply List.Perm.refl
[GOAL]
case swap
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ y✝ : α
⊢ (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (x✝, y✝) ≈
    (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (y✝, x✝)
[PROOFSTEP]
apply List.Perm.swap'
[GOAL]
case swap.p
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ y✝ : α
⊢ [] ~ []
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ((fun x x_1 => x ≈ x_1) ⇒ fun x x_1 => x ≈ x_1) Sym2.fromVector Sym2.fromVector
[PROOFSTEP]
rintro ⟨x, hx⟩ ⟨y, hy⟩ h
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
x : List α
hx : List.length x = 2
y : List α
hy : List.length y = 2
h : { val := x, property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := x, property := hx } ≈ Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
cases' x with _ x
[GOAL]
case mk.mk.nil
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
hx : List.length [] = 2
h : { val := [], property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := [], property := hx } ≈ Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
simp at hx
[GOAL]
case mk.mk.cons
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝ : α
x : List α
hx : List.length (head✝ :: x) = 2
h : { val := head✝ :: x, property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := head✝ :: x, property := hx } ≈ Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
cases' x with _ x
[GOAL]
case mk.mk.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝ : α
hx : List.length [head✝] = 2
h : { val := [head✝], property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := [head✝], property := hx } ≈ Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
simp at hx
[GOAL]
case mk.mk.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝¹ head✝ : α
x : List α
hx : List.length (head✝¹ :: head✝ :: x) = 2
h : { val := head✝¹ :: head✝ :: x, property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := head✝¹ :: head✝ :: x, property := hx } ≈ Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
cases' x with _ x
[GOAL]
case mk.mk.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝¹ head✝ : α
hx : List.length [head✝¹, head✝] = 2
h : { val := [head✝¹, head✝], property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := [head✝¹, head✝], property := hx } ≈ Sym2.fromVector { val := y, property := hy }
case mk.mk.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝² head✝¹ head✝ : α
x : List α
hx : List.length (head✝² :: head✝¹ :: head✝ :: x) = 2
h : { val := head✝² :: head✝¹ :: head✝ :: x, property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := head✝² :: head✝¹ :: head✝ :: x, property := hx } ≈
    Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
swap
[GOAL]
case mk.mk.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝² head✝¹ head✝ : α
x : List α
hx : List.length (head✝² :: head✝¹ :: head✝ :: x) = 2
h : { val := head✝² :: head✝¹ :: head✝ :: x, property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := head✝² :: head✝¹ :: head✝ :: x, property := hx } ≈
    Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
exfalso
[GOAL]
case mk.mk.cons.cons.cons.h
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝² head✝¹ head✝ : α
x : List α
hx : List.length (head✝² :: head✝¹ :: head✝ :: x) = 2
h : { val := head✝² :: head✝¹ :: head✝ :: x, property := hx } ≈ { val := y, property := hy }
⊢ False
[PROOFSTEP]
simp at hx
[GOAL]
case mk.mk.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
y : List α
hy : List.length y = 2
head✝¹ head✝ : α
hx : List.length [head✝¹, head✝] = 2
h : { val := [head✝¹, head✝], property := hx } ≈ { val := y, property := hy }
⊢ Sym2.fromVector { val := [head✝¹, head✝], property := hx } ≈ Sym2.fromVector { val := y, property := hy }
[PROOFSTEP]
cases' y with _ y
[GOAL]
case mk.mk.cons.cons.nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
head✝¹ head✝ : α
hx : List.length [head✝¹, head✝] = 2
hy : List.length [] = 2
h : { val := [head✝¹, head✝], property := hx } ≈ { val := [], property := hy }
⊢ Sym2.fromVector { val := [head✝¹, head✝], property := hx } ≈ Sym2.fromVector { val := [], property := hy }
[PROOFSTEP]
simp at hy
[GOAL]
case mk.mk.cons.cons.nil.cons
α : Type u_1
β : Type u_2
γ : Type u_3
head✝² head✝¹ : α
hx : List.length [head✝², head✝¹] = 2
head✝ : α
y : List α
hy : List.length (head✝ :: y) = 2
h : { val := [head✝², head✝¹], property := hx } ≈ { val := head✝ :: y, property := hy }
⊢ Sym2.fromVector { val := [head✝², head✝¹], property := hx } ≈ Sym2.fromVector { val := head✝ :: y, property := hy }
[PROOFSTEP]
cases' y with _ y
[GOAL]
case mk.mk.cons.cons.nil.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
head✝² head✝¹ : α
hx : List.length [head✝², head✝¹] = 2
head✝ : α
hy : List.length [head✝] = 2
h : { val := [head✝², head✝¹], property := hx } ≈ { val := [head✝], property := hy }
⊢ Sym2.fromVector { val := [head✝², head✝¹], property := hx } ≈ Sym2.fromVector { val := [head✝], property := hy }
[PROOFSTEP]
simp at hy
[GOAL]
case mk.mk.cons.cons.nil.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
head✝³ head✝² : α
hx : List.length [head✝³, head✝²] = 2
head✝¹ head✝ : α
y : List α
hy : List.length (head✝¹ :: head✝ :: y) = 2
h : { val := [head✝³, head✝²], property := hx } ≈ { val := head✝¹ :: head✝ :: y, property := hy }
⊢ Sym2.fromVector { val := [head✝³, head✝²], property := hx } ≈
    Sym2.fromVector { val := head✝¹ :: head✝ :: y, property := hy }
[PROOFSTEP]
cases' y with _ y
[GOAL]
case mk.mk.cons.cons.nil.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
head✝³ head✝² : α
hx : List.length [head✝³, head✝²] = 2
head✝¹ head✝ : α
hy : List.length [head✝¹, head✝] = 2
h : { val := [head✝³, head✝²], property := hx } ≈ { val := [head✝¹, head✝], property := hy }
⊢ Sym2.fromVector { val := [head✝³, head✝²], property := hx } ≈
    Sym2.fromVector { val := [head✝¹, head✝], property := hy }
case mk.mk.cons.cons.nil.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
head✝⁴ head✝³ : α
hx : List.length [head✝⁴, head✝³] = 2
head✝² head✝¹ head✝ : α
y : List α
hy : List.length (head✝² :: head✝¹ :: head✝ :: y) = 2
h : { val := [head✝⁴, head✝³], property := hx } ≈ { val := head✝² :: head✝¹ :: head✝ :: y, property := hy }
⊢ Sym2.fromVector { val := [head✝⁴, head✝³], property := hx } ≈
    Sym2.fromVector { val := head✝² :: head✝¹ :: head✝ :: y, property := hy }
[PROOFSTEP]
swap
[GOAL]
case mk.mk.cons.cons.nil.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
head✝⁴ head✝³ : α
hx : List.length [head✝⁴, head✝³] = 2
head✝² head✝¹ head✝ : α
y : List α
hy : List.length (head✝² :: head✝¹ :: head✝ :: y) = 2
h : { val := [head✝⁴, head✝³], property := hx } ≈ { val := head✝² :: head✝¹ :: head✝ :: y, property := hy }
⊢ Sym2.fromVector { val := [head✝⁴, head✝³], property := hx } ≈
    Sym2.fromVector { val := head✝² :: head✝¹ :: head✝ :: y, property := hy }
[PROOFSTEP]
exfalso
[GOAL]
case mk.mk.cons.cons.nil.cons.cons.cons.h
α : Type u_1
β : Type u_2
γ : Type u_3
head✝⁴ head✝³ : α
hx : List.length [head✝⁴, head✝³] = 2
head✝² head✝¹ head✝ : α
y : List α
hy : List.length (head✝² :: head✝¹ :: head✝ :: y) = 2
h : { val := [head✝⁴, head✝³], property := hx } ≈ { val := head✝² :: head✝¹ :: head✝ :: y, property := hy }
⊢ False
[PROOFSTEP]
simp at hy
[GOAL]
case mk.mk.cons.cons.nil.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
head✝³ head✝² : α
hx : List.length [head✝³, head✝²] = 2
head✝¹ head✝ : α
hy : List.length [head✝¹, head✝] = 2
h : { val := [head✝³, head✝²], property := hx } ≈ { val := [head✝¹, head✝], property := hy }
⊢ Sym2.fromVector { val := [head✝³, head✝²], property := hx } ≈
    Sym2.fromVector { val := [head✝¹, head✝], property := hy }
[PROOFSTEP]
rcases perm_card_two_iff.mp h with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
[GOAL]
case mk.mk.cons.cons.nil.cons.cons.nil.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
head✝¹ head✝ : α
hx hy : List.length [head✝¹, head✝] = 2
h : { val := [head✝¹, head✝], property := hx } ≈ { val := [head✝¹, head✝], property := hy }
⊢ Sym2.fromVector { val := [head✝¹, head✝], property := hx } ≈
    Sym2.fromVector { val := [head✝¹, head✝], property := hy }
[PROOFSTEP]
constructor
[GOAL]
case mk.mk.cons.cons.nil.cons.cons.nil.inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
head✝¹ head✝ : α
hx : List.length [head✝¹, head✝] = 2
hy : List.length [head✝, head✝¹] = 2
h : { val := [head✝¹, head✝], property := hx } ≈ { val := [head✝, head✝¹], property := hy }
⊢ Sym2.fromVector { val := [head✝¹, head✝], property := hx } ≈
    Sym2.fromVector { val := [head✝, head✝¹], property := hy }
[PROOFSTEP]
apply Sym2.Rel.swap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ LeftInverse
    (Quotient.map Sym2.fromVector
      (_ :
        ∀ ⦃a b : Vector α 2⦄,
          (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b)))
    (Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b))
[PROOFSTEP]
apply Sym2.ind
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (x y : α),
    Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.map
          (fun x =>
            { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
          (_ :
            ∀ ⦃a b : α × α⦄,
              a ≈ b →
                (fun x =>
                      { val := [x.fst, x.snd],
                        property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                    a ≈
                  (fun x =>
                      { val := [x.fst, x.snd],
                        property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                    b)
          (Quotient.mk (Rel.setoid α) (x, y))) =
      Quotient.mk (Rel.setoid α) (x, y)
[PROOFSTEP]
aesop (add norm unfold [Sym2.fromVector])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : Sym' α 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        x) =
    x
[PROOFSTEP]
refine' Quotient.recOnSubsingleton x fun x => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym' α 2
x : Vector α 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) x)) =
    Quotient.mk (Vector.Perm.isSetoid α 2) x
[PROOFSTEP]
cases' x with x hx
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym' α 2
x : List α
hx : List.length x = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := x, property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := x, property := hx }
[PROOFSTEP]
cases' x with _ x
[GOAL]
case mk.nil
α : Type u_1
β : Type u_2
γ : Type u_3
x : Sym' α 2
hx : List.length [] = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := [], property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := [], property := hx }
[PROOFSTEP]
simp at hx
[GOAL]
case mk.cons
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym' α 2
head✝ : α
x : List α
hx : List.length (head✝ :: x) = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝ :: x, property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝ :: x, property := hx }
[PROOFSTEP]
cases' x with _ x
[GOAL]
case mk.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
x : Sym' α 2
head✝ : α
hx : List.length [head✝] = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := [head✝], property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := [head✝], property := hx }
[PROOFSTEP]
simp at hx
[GOAL]
case mk.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym' α 2
head✝¹ head✝ : α
x : List α
hx : List.length (head✝¹ :: head✝ :: x) = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝¹ :: head✝ :: x, property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝¹ :: head✝ :: x, property := hx }
[PROOFSTEP]
cases' x with _ x
[GOAL]
case mk.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
x : Sym' α 2
head✝¹ head✝ : α
hx : List.length [head✝¹, head✝] = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := [head✝¹, head✝], property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := [head✝¹, head✝], property := hx }
case mk.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym' α 2
head✝² head✝¹ head✝ : α
x : List α
hx : List.length (head✝² :: head✝¹ :: head✝ :: x) = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝² :: head✝¹ :: head✝ :: x, property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝² :: head✝¹ :: head✝ :: x, property := hx }
[PROOFSTEP]
swap
[GOAL]
case mk.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym' α 2
head✝² head✝¹ head✝ : α
x : List α
hx : List.length (head✝² :: head✝¹ :: head✝ :: x) = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝² :: head✝¹ :: head✝ :: x, property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := head✝² :: head✝¹ :: head✝ :: x, property := hx }
[PROOFSTEP]
exfalso
[GOAL]
case mk.cons.cons.cons.h
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Sym' α 2
head✝² head✝¹ head✝ : α
x : List α
hx : List.length (head✝² :: head✝¹ :: head✝ :: x) = 2
⊢ False
[PROOFSTEP]
simp at hx
[GOAL]
case mk.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
x : Sym' α 2
head✝¹ head✝ : α
hx : List.length [head✝¹, head✝] = 2
⊢ Quotient.map
      (fun x => { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
      (_ :
        ∀ ⦃a b : α × α⦄,
          a ≈ b →
            (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                a ≈
              (fun x =>
                  { val := [x.fst, x.snd], property := (_ : List.length [x.fst, x.snd] = List.length [x.fst, x.snd]) })
                b)
      (Quotient.map Sym2.fromVector
        (_ :
          ∀ ⦃a b : Vector α 2⦄,
            (fun x x_1 => x ≈ x_1) a b → (fun x x_1 => x ≈ x_1) (Sym2.fromVector a) (Sym2.fromVector b))
        (Quotient.mk (Vector.Perm.isSetoid α 2) { val := [head✝¹, head✝], property := hx })) =
    Quotient.mk (Vector.Perm.isSetoid α 2) { val := [head✝¹, head✝], property := hx }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
x y : α × α
⊢ relBool x y = true ↔ Rel α x y
[PROOFSTEP]
cases' x with x₁ x₂
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
y : α × α
x₁ x₂ : α
⊢ relBool (x₁, x₂) y = true ↔ Rel α (x₁, x₂) y
[PROOFSTEP]
cases' y with y₁ y₂
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
x₁ x₂ y₁ y₂ : α
⊢ relBool (x₁, x₂) (y₁, y₂) = true ↔ Rel α (x₁, x₂) (y₁, y₂)
[PROOFSTEP]
aesop (rule_sets [Sym2]) (add norm unfold [relBool])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
⊢ ∀ (a₁ a₂ b₁ b₂ : α),
    (fun x₁ x₂ y₁ y₂ => relBool (x₁, x₂) (y₁, y₂)) a₁ a₂ b₁ b₂ =
        (fun x₁ x₂ y₁ y₂ => relBool (x₁, x₂) (y₁, y₂)) a₂ a₁ b₁ b₂ ∧
      (fun x₁ x₂ y₁ y₂ => relBool (x₁, x₂) (y₁, y₂)) a₁ a₂ b₁ b₂ =
        (fun x₁ x₂ y₁ y₂ => relBool (x₁, x₂) (y₁, y₂)) a₁ a₂ b₂ b₁
[PROOFSTEP]
aesop (add norm unfold [relBool])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a b : Sym2 α
⊢ ∀ (a₁ a₂ b₁ b₂ : α),
    eqBool (Quotient.mk (Rel.setoid α) (a₁, a₂)) (Quotient.mk (Rel.setoid α) (b₁, b₂)) = true ↔
      Quotient.mk (Rel.setoid α) (a₁, a₂) = Quotient.mk (Rel.setoid α) (b₁, b₂)
[PROOFSTEP]
aesop (rule_sets [Sym2])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ ∀ (a_1 b : α × α) (p : a_1 ≈ b),
    Eq.ndrec (motive := fun x => a ∈ x → α) (fun x => Sym2.pairOther a a_1)
        (_ : Quotient.mk (Rel.setoid α) a_1 = Quotient.mk (Rel.setoid α) b) =
      fun x => Sym2.pairOther a b
[PROOFSTEP]
clear h z
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
⊢ ∀ (a_1 b : α × α) (p : a_1 ≈ b),
    Eq.ndrec (motive := fun x => a ∈ x → α) (fun x => Sym2.pairOther a a_1)
        (_ : Quotient.mk (Rel.setoid α) a_1 = Quotient.mk (Rel.setoid α) b) =
      fun x => Sym2.pairOther a b
[PROOFSTEP]
intro x y h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
⊢ Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x)
      (_ : Quotient.mk (Rel.setoid α) x = Quotient.mk (Rel.setoid α) y) =
    fun x => Sym2.pairOther a y
[PROOFSTEP]
ext hy
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a ∈ Quotient.mk (Rel.setoid α) y
⊢ Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x)
      (_ : Quotient.mk (Rel.setoid α) x = Quotient.mk (Rel.setoid α) y) hy =
    Sym2.pairOther a y
[PROOFSTEP]
convert_to Sym2.pairOther a x = _
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a ∈ Quotient.mk (Rel.setoid α) y
⊢ Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x)
      (_ : Quotient.mk (Rel.setoid α) x = Quotient.mk (Rel.setoid α) y) hy =
    Sym2.pairOther a x
[PROOFSTEP]
have :
  ∀ {c e h},
    @Eq.ndrec (Quotient (Rel.setoid α)) (Quotient.mk (Rel.setoid α) x) (fun x => a ∈ x → α)
        (fun _ => Sym2.pairOther a x) c e h =
      Sym2.pairOther a x :=
  by intro _ e _; subst e; rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a ∈ Quotient.mk (Rel.setoid α) y
⊢ ∀ {c : Quotient (Rel.setoid α)} {e : Quotient.mk (Rel.setoid α) x = c} {h : a ∈ c},
    Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x) e h = Sym2.pairOther a x
[PROOFSTEP]
intro _ e _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a ∈ Quotient.mk (Rel.setoid α) y
c✝ : Quotient (Rel.setoid α)
e : Quotient.mk (Rel.setoid α) x = c✝
h✝ : a ∈ c✝
⊢ Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x) e h✝ = Sym2.pairOther a x
[PROOFSTEP]
subst e
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a ∈ Quotient.mk (Rel.setoid α) y
h✝ : a ∈ Quotient.mk (Rel.setoid α) x
⊢ Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x)
      (_ : Quotient.mk (Rel.setoid α) x = Quotient.mk (Rel.setoid α) x) h✝ =
    Sym2.pairOther a x
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a ∈ Quotient.mk (Rel.setoid α) y
this :
  ∀ {c : Quotient (Rel.setoid α)} {e : Quotient.mk (Rel.setoid α) x = c} {h : a ∈ c},
    Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x) e h = Sym2.pairOther a x
⊢ Eq.ndrec (motive := fun x => a ∈ x → α) (fun x_1 => Sym2.pairOther a x)
      (_ : Quotient.mk (Rel.setoid α) x = Quotient.mk (Rel.setoid α) y) hy =
    Sym2.pairOther a x
[PROOFSTEP]
apply this
[GOAL]
case h.convert_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a ∈ Quotient.mk (Rel.setoid α) y
⊢ Sym2.pairOther a x = Sym2.pairOther a y
[PROOFSTEP]
rw [mem_iff] at hy
[GOAL]
case h.convert_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a = y.fst ∨ a = y.snd
⊢ Sym2.pairOther a x = Sym2.pairOther a y
[PROOFSTEP]
have : relBool x y := (relBool_spec x y).mpr h
[GOAL]
case h.convert_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
x y : α × α
h : x ≈ y
hy : a = y.fst ∨ a = y.snd
this : relBool x y = true
⊢ Sym2.pairOther a x = Sym2.pairOther a y
[PROOFSTEP]
aesop (add norm unfold [pairOther, relBool])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Quotient.mk (Rel.setoid α) (a, Mem.other' h) = z
[PROOFSTEP]
induction z using Sym2.ind
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a x✝ y✝ : α
h : a ∈ Quotient.mk (Rel.setoid α) (x✝, y✝)
⊢ Quotient.mk (Rel.setoid α) (a, Mem.other' h) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
have h' := mem_iff.mp h
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a x✝ y✝ : α
h : a ∈ Quotient.mk (Rel.setoid α) (x✝, y✝)
h' : a = x✝ ∨ a = y✝
⊢ Quotient.mk (Rel.setoid α) (a, Mem.other' h) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
aesop (add norm unfold [Quotient.rec, Quot.rec]) (rule_sets [Sym2])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h = Mem.other' h
[PROOFSTEP]
rw [← congr_right, other_spec' h, other_spec]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other' h ∈ z
[PROOFSTEP]
rw [← other_eq_other']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z
[PROOFSTEP]
exact other_mem h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb = a
[PROOFSTEP]
induction z using Sym2.ind
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a x✝ y✝ : α
ha : a ∈ Quotient.mk (Rel.setoid α) (x✝, y✝)
hb : Mem.other' ha ∈ Quotient.mk (Rel.setoid α) (x✝, y✝)
⊢ Mem.other' hb = a
[PROOFSTEP]
aesop (rule_sets [Sym2]) (add norm unfold [Quotient.rec, Quot.rec])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
⊢ Mem.other hb = a
[PROOFSTEP]
classical
rw [other_eq_other'] at hb ⊢
convert other_invol' ha hb using 2
apply other_eq_other'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
⊢ Mem.other hb = a
[PROOFSTEP]
rw [other_eq_other'] at hb ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb✝ = a
[PROOFSTEP]
convert other_invol' ha hb using 2
[GOAL]
case h.e'_2.h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other ha = Mem.other' ha
[PROOFSTEP]
apply other_eq_other'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
⊢ filter IsDiag (image Quotient.mk'' (s ×ˢ s)) = image Quotient.mk'' (Finset.diag s)
[PROOFSTEP]
ext z
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
z : Sym2 α
⊢ z ∈ filter IsDiag (image Quotient.mk'' (s ×ˢ s)) ↔ z ∈ image Quotient.mk'' (Finset.diag s)
[PROOFSTEP]
induction' z using Sym2.inductionOn
[GOAL]
case a.hf
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ Quotient.mk (Rel.setoid α) (x✝, y✝) ∈ filter IsDiag (image Quotient.mk'' (s ×ˢ s)) ↔
    Quotient.mk (Rel.setoid α) (x✝, y✝) ∈ image Quotient.mk'' (Finset.diag s)
[PROOFSTEP]
simp only [mem_image, mem_diag, exists_prop, mem_filter, Prod.exists, mem_product]
[GOAL]
case a.hf
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝)) ↔
    ∃ a b, (a ∈ s ∧ a = b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
constructor
[GOAL]
case a.hf.mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝)) →
    ∃ a b, (a ∈ s ∧ a = b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
rintro ⟨⟨a, b, ⟨ha, hb⟩, (h : Quotient.mk _ _ = _)⟩, hab⟩
[GOAL]
case a.hf.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
hab : IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
a b : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ a = b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
rw [← h, Sym2.mk''_isDiag_iff] at hab
[GOAL]
case a.hf.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
hab : a = b
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ a = b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
exact ⟨a, b, ⟨ha, hab⟩, h⟩
[GOAL]
case a.hf.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ a = b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) →
    (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
[PROOFSTEP]
rintro ⟨a, b, ⟨ha, rfl⟩, h⟩
[GOAL]
case a.hf.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a : α
ha : a ∈ s
h : Quotient.mk'' (a, a) = Quotient.mk (Rel.setoid α) (x✝, y✝)
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
    IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
[PROOFSTEP]
rw [← h]
[GOAL]
case a.hf.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a : α
ha : a ∈ s
h : Quotient.mk'' (a, a) = Quotient.mk (Rel.setoid α) (x✝, y✝)
⊢ (∃ a_1 b, (a_1 ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a_1, b) = Quotient.mk'' (a, a)) ∧ IsDiag (Quotient.mk'' (a, a))
[PROOFSTEP]
exact ⟨⟨a, a, ⟨ha, ha⟩, rfl⟩, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
⊢ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (s ×ˢ s)) = image Quotient.mk'' (offDiag s)
[PROOFSTEP]
ext z
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
z : Sym2 α
⊢ z ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (s ×ˢ s)) ↔ z ∈ image Quotient.mk'' (offDiag s)
[PROOFSTEP]
induction z using Sym2.inductionOn
[GOAL]
case a.hf
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ Quotient.mk (Rel.setoid α) (x✝, y✝) ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (s ×ˢ s)) ↔
    Quotient.mk (Rel.setoid α) (x✝, y✝) ∈ image Quotient.mk'' (offDiag s)
[PROOFSTEP]
simp only [mem_image, mem_offDiag, mem_filter, Prod.exists, mem_product]
[GOAL]
case a.hf
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝)) ↔
    ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
constructor
[GOAL]
case a.hf.mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝)) →
    ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
rintro ⟨⟨a, b, ⟨ha, hb⟩, (h : Quotient.mk _ _ = _)⟩, hab⟩
[GOAL]
case a.hf.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
hab : ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
a b : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
rw [← h, Sym2.mk''_isDiag_iff] at hab
[GOAL]
case a.hf.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
hab : ¬a = b
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
[PROOFSTEP]
exact ⟨a, b, ⟨ha, hb, hab⟩, h⟩
[GOAL]
case a.hf.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) →
    (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
[PROOFSTEP]
rintro ⟨a, b, ⟨ha, hb, hab⟩, (h : Quotient.mk _ _ = _)⟩
[GOAL]
case a.hf.mpr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
    ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
[PROOFSTEP]
rw [Ne.def, ← Sym2.mk''_isDiag_iff, h] at hab
[GOAL]
case a.hf.mpr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
hab : ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
    ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
[PROOFSTEP]
exact ⟨⟨a, b, ⟨ha, hb⟩, h⟩, hab⟩


[GOAL]
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
⊢ Rat.Nonneg (a /. b) ↔ 0 ≤ a
[PROOFSTEP]
generalize ha : a /. b = x
[GOAL]
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
x : ℚ
ha : a /. b = x
⊢ Rat.Nonneg x ↔ 0 ≤ a
[PROOFSTEP]
cases' x with n₁ d₁ h₁ c₁
[GOAL]
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = mk' n₁ d₁
⊢ Rat.Nonneg (mk' n₁ d₁) ↔ 0 ≤ a
[PROOFSTEP]
rw [num_den'] at ha
[GOAL]
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
⊢ Rat.Nonneg (mk' n₁ d₁) ↔ 0 ≤ a
[PROOFSTEP]
simp [Rat.Nonneg]
[GOAL]
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
⊢ 0 ≤ n₁ ↔ 0 ≤ a
[PROOFSTEP]
have d0 := Int.ofNat_lt.2 (Nat.pos_of_ne_zero h₁)
[GOAL]
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
⊢ 0 ≤ n₁ ↔ 0 ≤ a
[PROOFSTEP]
have := (divInt_eq_iff (ne_of_gt h) (ne_of_gt d0)).1 ha
[GOAL]
case mk'
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
⊢ 0 ≤ n₁ ↔ 0 ≤ a
[PROOFSTEP]
constructor
[GOAL]
case mk'.mp
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
⊢ 0 ≤ n₁ → 0 ≤ a
[PROOFSTEP]
intro h₂
[GOAL]
case mk'.mpr
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
⊢ 0 ≤ a → 0 ≤ n₁
[PROOFSTEP]
intro h₂
[GOAL]
case mk'.mp
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ n₁
⊢ 0 ≤ a
[PROOFSTEP]
apply nonneg_of_mul_nonneg_left _ d0
[GOAL]
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ n₁
⊢ 0 ≤ a * ↑d₁
[PROOFSTEP]
rw [this]
[GOAL]
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ n₁
⊢ 0 ≤ n₁ * b
[PROOFSTEP]
exact mul_nonneg h₂ (le_of_lt h)
[GOAL]
case mk'.mpr
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ a
⊢ 0 ≤ n₁
[PROOFSTEP]
apply nonneg_of_mul_nonneg_left _ h
[GOAL]
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ a
⊢ 0 ≤ n₁ * b
[PROOFSTEP]
rw [← this]
[GOAL]
a✝ b✝ c : ℚ
a b : ℤ
h : 0 < b
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
d0 : ↑0 < ↑d₁
this : a * ↑d₁ = n₁ * b
h₂ : 0 ≤ a
⊢ 0 ≤ a * ↑d₁
[PROOFSTEP]
exact mul_nonneg h₂ (Int.ofNat_zero_le _)
[GOAL]
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
⊢ Rat.Nonneg (n₁ /. ↑d₁) → Rat.Nonneg (n₂ /. ↑d₂) → Rat.Nonneg (n₁ /. ↑d₁ + n₂ /. ↑d₂)
[PROOFSTEP]
have d₁0 : 0 < (d₁ : ℤ) := Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h₁)
[GOAL]
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
⊢ Rat.Nonneg (n₁ /. ↑d₁) → Rat.Nonneg (n₂ /. ↑d₂) → Rat.Nonneg (n₁ /. ↑d₁ + n₂ /. ↑d₂)
[PROOFSTEP]
have d₂0 : 0 < (d₂ : ℤ) := Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h₂)
[GOAL]
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ Rat.Nonneg (n₁ /. ↑d₁) → Rat.Nonneg (n₂ /. ↑d₂) → Rat.Nonneg (n₁ /. ↑d₁ + n₂ /. ↑d₂)
[PROOFSTEP]
simp only [d₁0, d₂0, h₁, h₂, mul_pos, divInt_nonneg, add_def'', Ne.def, Nat.cast_eq_zero, not_false_iff]
[GOAL]
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ 0 ≤ n₁ → 0 ≤ n₂ → 0 ≤ n₁ * ↑d₂ + n₂ * ↑d₁
[PROOFSTEP]
intro n₁0 n₂0
[GOAL]
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ n₁ * ↑d₂ + n₂ * ↑d₁
[PROOFSTEP]
apply add_nonneg
[GOAL]
case ha
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ n₁ * ↑d₂
[PROOFSTEP]
apply mul_nonneg
[GOAL]
case hb
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ n₂ * ↑d₁
[PROOFSTEP]
apply mul_nonneg
[GOAL]
case ha.ha
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ n₁
[PROOFSTEP]
first
| assumption
| apply Int.ofNat_zero_le
[GOAL]
case ha.ha
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ n₁
[PROOFSTEP]
assumption
[GOAL]
case ha.hb
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ ↑d₂
[PROOFSTEP]
first
| assumption
| apply Int.ofNat_zero_le
[GOAL]
case ha.hb
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ ↑d₂
[PROOFSTEP]
assumption
[GOAL]
case ha.hb
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ ↑d₂
[PROOFSTEP]
apply Int.ofNat_zero_le
[GOAL]
case hb.ha
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ n₂
[PROOFSTEP]
first
| assumption
| apply Int.ofNat_zero_le
[GOAL]
case hb.ha
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ n₂
[PROOFSTEP]
assumption
[GOAL]
case hb.hb
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ ↑d₁
[PROOFSTEP]
first
| assumption
| apply Int.ofNat_zero_le
[GOAL]
case hb.hb
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ ↑d₁
[PROOFSTEP]
assumption
[GOAL]
case hb.hb
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ ↑d₁
[PROOFSTEP]
apply Int.ofNat_zero_le
[GOAL]
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
⊢ Rat.Nonneg (n₁ /. ↑d₁) → Rat.Nonneg (n₂ /. ↑d₂) → Rat.Nonneg (n₁ /. ↑d₁ * (n₂ /. ↑d₂))
[PROOFSTEP]
have d₁0 : 0 < (d₁ : ℤ) := Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h₁)
[GOAL]
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
⊢ Rat.Nonneg (n₁ /. ↑d₁) → Rat.Nonneg (n₂ /. ↑d₂) → Rat.Nonneg (n₁ /. ↑d₁ * (n₂ /. ↑d₂))
[PROOFSTEP]
have d₂0 : 0 < (d₂ : ℤ) := Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h₂)
[GOAL]
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ Rat.Nonneg (n₁ /. ↑d₁) → Rat.Nonneg (n₂ /. ↑d₂) → Rat.Nonneg (n₁ /. ↑d₁ * (n₂ /. ↑d₂))
[PROOFSTEP]
rw [mul_def' d₁0.ne.symm d₂0.ne.symm, divInt_nonneg _ d₁0, divInt_nonneg _ d₂0, divInt_nonneg _ (mul_pos d₁0 d₂0)]
[GOAL]
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ 0 ≤ n₁ → 0 ≤ n₂ → 0 ≤ n₁ * n₂
[PROOFSTEP]
apply mul_nonneg
[GOAL]
a✝ b c a : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ Rat.Nonneg (n /. ↑d) → Rat.Nonneg (-(n /. ↑d)) → n /. ↑d = 0
[PROOFSTEP]
have d0 : 0 < (d : ℤ) := Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h)
[GOAL]
a✝ b c a : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
d0 : 0 < ↑d
⊢ Rat.Nonneg (n /. ↑d) → Rat.Nonneg (-(n /. ↑d)) → n /. ↑d = 0
[PROOFSTEP]
rw [divInt_nonneg _ d0, neg_def, divInt_nonneg _ d0, Right.nonneg_neg_iff, divInt_eq_zero d0.ne.symm]
[GOAL]
a✝ b c a : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
d0 : 0 < ↑d
⊢ 0 ≤ n → n ≤ 0 → n = 0
[PROOFSTEP]
exact fun h₁ h₂ => le_antisymm h₂ h₁
[GOAL]
a b c : ℚ
⊢ Rat.Nonneg a ∨ Rat.Nonneg (-a)
[PROOFSTEP]
cases' a with n
[GOAL]
case mk'
b c : ℚ
n : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs n) den✝
⊢ Rat.Nonneg (mk' n den✝) ∨ Rat.Nonneg (-mk' n den✝)
[PROOFSTEP]
exact Or.imp_right neg_nonneg_of_nonpos (le_total 0 n)
[GOAL]
a b c : ℚ
⊢ Decidable (Rat.Nonneg a)
[PROOFSTEP]
cases a
[GOAL]
case mk'
b c : ℚ
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
⊢ Decidable (Rat.Nonneg (mk' num✝ den✝))
[PROOFSTEP]
unfold Rat.Nonneg
[GOAL]
case mk'
b c : ℚ
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
⊢ Decidable (0 ≤ (mk' num✝ den✝).num)
[PROOFSTEP]
infer_instance
[GOAL]
a✝ b c : ℚ
C : ℚ → Sort u
a : ℚ
H : (n : ℤ) → (d : ℕ) → (nz : d ≠ 0) → (red : Nat.coprime (Int.natAbs n) d) → C (mk' n d)
n : ℤ
d : ℕ
h : 0 < d
h' : Nat.coprime (Int.natAbs n) d
⊢ C (n /. ↑d)
[PROOFSTEP]
rw [← mk_eq_divInt _ _ h.ne' h']
[GOAL]
a✝ b c : ℚ
C : ℚ → Sort u
a : ℚ
H : (n : ℤ) → (d : ℕ) → (nz : d ≠ 0) → (red : Nat.coprime (Int.natAbs n) d) → C (mk' n d)
n : ℤ
d : ℕ
h : 0 < d
h' : Nat.coprime (Int.natAbs n) d
⊢ C (mk' n d)
[PROOFSTEP]
exact
  H n d h.ne'
    _
      -- Porting note: TODO can this be shortened?
[GOAL]
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
⊢ mk' na da ≤ mk' nb db ↔ Rat.Nonneg (mk' nb db - mk' na da)
[PROOFSTEP]
change Rat.blt _ _ = false ↔ _
[GOAL]
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
⊢ Rat.blt (mk' nb db) (mk' na da) = false ↔ Rat.Nonneg (mk' nb db - mk' na da)
[PROOFSTEP]
unfold Rat.blt
[GOAL]
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
⊢ (if (decide ((mk' nb db).num < 0) && decide (0 ≤ (mk' na da).num)) = true then true
      else
        if (mk' nb db).num = 0 then decide (0 < (mk' na da).num)
        else
          if (decide (0 < (mk' nb db).num) && decide ((mk' na da).num ≤ 0)) = true then false
          else decide ((mk' nb db).num * ↑(mk' na da).den < (mk' na da).num * ↑(mk' nb db).den)) =
      false ↔
    Rat.Nonneg (mk' nb db - mk' na da)
[PROOFSTEP]
simp [-divInt_ofNat, mkRat_eq]
[GOAL]
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
⊢ (if nb < 0 ∧ 0 ≤ na then False else if nb = 0 then na ≤ 0 else (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da) ↔
    Rat.Nonneg (mk' nb db - mk' na da)
[PROOFSTEP]
split_ifs with h h'
[GOAL]
case pos
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ False ↔ Rat.Nonneg (mk' nb db - mk' na da)
[PROOFSTEP]
rw [Rat.sub_def]
[GOAL]
case pos
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ False ↔
    Rat.Nonneg
      (normalize ((mk' nb db).num * ↑(mk' na da).den - (mk' na da).num * ↑(mk' nb db).den)
        ((mk' nb db).den * (mk' na da).den))
[PROOFSTEP]
simp [Rat.Nonneg]
[GOAL]
case pos
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ (normalize (nb * ↑da - na * ↑db) (db * da)).num < 0
[PROOFSTEP]
simp [normalize_eq]
[GOAL]
case pos
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da)) < 0
[PROOFSTEP]
apply Int.ediv_neg'
[GOAL]
case pos.Ha
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ nb * ↑da - na * ↑db < 0
[PROOFSTEP]
rw [sub_neg]
[GOAL]
case pos.Ha
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ nb * ↑da < na * ↑db
[PROOFSTEP]
apply lt_of_lt_of_le
[GOAL]
case pos.Ha.a
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ nb * ↑da < ?pos.Ha.b✝
[PROOFSTEP]
apply mul_neg_of_neg_of_pos h.1
[GOAL]
case pos.Ha.a
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 < ↑da
[PROOFSTEP]
rwa [Nat.cast_pos, pos_iff_ne_zero]
[GOAL]
case pos.Ha.a
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 ≤ na * ↑db
[PROOFSTEP]
apply mul_nonneg h.2 (Nat.cast_nonneg _)
[GOAL]
case pos.Hb
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 < ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
[PROOFSTEP]
simp only [Nat.cast_pos]
[GOAL]
case pos.Hb
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 < Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da)
[PROOFSTEP]
apply Nat.gcd_pos_of_pos_right
[GOAL]
case pos.Hb.npos
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 < db * da
[PROOFSTEP]
apply mul_pos
[GOAL]
case pos.Hb.npos.ha
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 < db
[PROOFSTEP]
rwa [pos_iff_ne_zero]
[GOAL]
case pos.Hb.npos.hb
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 < da
[PROOFSTEP]
rwa [pos_iff_ne_zero]
[GOAL]
case pos
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : nb = 0
⊢ na ≤ 0 ↔ Rat.Nonneg (mk' nb db - mk' na da)
[PROOFSTEP]
simp only [divInt_ofNat, ← zero_iff_num_zero, mkRat_eq_zero hb] at h'
[GOAL]
case pos
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : nb = 0
⊢ na ≤ 0 ↔ Rat.Nonneg (mk' nb db - mk' na da)
[PROOFSTEP]
simp [h', Rat.Nonneg]
[GOAL]
case neg
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
⊢ (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da ↔ Rat.Nonneg (mk' nb db - mk' na da)
[PROOFSTEP]
simp [Rat.Nonneg, Rat.sub_def, normalize_eq]
[GOAL]
case neg
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
⊢ (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da ↔
    0 ≤ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
[PROOFSTEP]
refine ⟨fun H => ?_, fun H _ => ?_⟩
[GOAL]
case neg.refine_1
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
⊢ 0 ≤ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
[PROOFSTEP]
refine Int.ediv_nonneg ?_ (Nat.cast_nonneg _)
[GOAL]
case neg.refine_1
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
⊢ 0 ≤ nb * ↑da - na * ↑db
[PROOFSTEP]
rw [sub_nonneg]
[GOAL]
case neg.refine_1
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
⊢ na * ↑db ≤ nb * ↑da
[PROOFSTEP]
push_neg at h
[GOAL]
case neg.refine_1
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
⊢ na * ↑db ≤ nb * ↑da
[PROOFSTEP]
obtain hb | hb := Ne.lt_or_lt h'
[GOAL]
case neg.refine_1.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : nb < 0
⊢ na * ↑db ≤ nb * ↑da
[PROOFSTEP]
apply H
[GOAL]
case neg.refine_1.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : nb < 0
⊢ 0 < nb → 0 < na
[PROOFSTEP]
intro H'
[GOAL]
case neg.refine_1.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : nb < 0
H' : 0 < nb
⊢ 0 < na
[PROOFSTEP]
exact (hb.trans H').false.elim
[GOAL]
case neg.refine_1.inr
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : 0 < nb
⊢ na * ↑db ≤ nb * ↑da
[PROOFSTEP]
obtain ha | ha := le_or_lt na 0
[GOAL]
case neg.refine_1.inr.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha✝ : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : 0 < nb
ha : na ≤ 0
⊢ na * ↑db ≤ nb * ↑da
[PROOFSTEP]
apply le_trans <| mul_nonpos_of_nonpos_of_nonneg ha (Nat.cast_nonneg _)
[GOAL]
case neg.refine_1.inr.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha✝ : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : 0 < nb
ha : na ≤ 0
⊢ 0 ≤ nb * ↑da
[PROOFSTEP]
exact mul_nonneg hb.le (Nat.cast_nonneg _)
[GOAL]
case neg.refine_1.inr.inr
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha✝ : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : 0 < nb
ha : 0 < na
⊢ na * ↑db ≤ nb * ↑da
[PROOFSTEP]
exact H (fun _ => ha)
[GOAL]
case neg.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : 0 ≤ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
x✝ : 0 < nb → 0 < na
⊢ na * ↑db ≤ nb * ↑da
[PROOFSTEP]
rw [← sub_nonneg]
[GOAL]
case neg.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : 0 ≤ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
x✝ : 0 < nb → 0 < na
⊢ 0 ≤ nb * ↑da - na * ↑db
[PROOFSTEP]
contrapose! H
[GOAL]
case neg.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
x✝ : 0 < nb → 0 < na
H : nb * ↑da - na * ↑db < 0
⊢ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da)) < 0
[PROOFSTEP]
apply Int.ediv_neg' H
[GOAL]
case neg.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
x✝ : 0 < nb → 0 < na
H : nb * ↑da - na * ↑db < 0
⊢ 0 < ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
[PROOFSTEP]
simp only [Nat.cast_pos]
[GOAL]
case neg.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
x✝ : 0 < nb → 0 < na
H : nb * ↑da - na * ↑db < 0
⊢ 0 < Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da)
[PROOFSTEP]
apply Nat.gcd_pos_of_pos_right
[GOAL]
case neg.refine_2.npos
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
x✝ : 0 < nb → 0 < na
H : nb * ↑da - na * ↑db < 0
⊢ 0 < db * da
[PROOFSTEP]
apply mul_pos
[GOAL]
case neg.refine_2.npos.ha
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
x✝ : 0 < nb → 0 < na
H : nb * ↑da - na * ↑db < 0
⊢ 0 < db
[PROOFSTEP]
rwa [pos_iff_ne_zero]
[GOAL]
case neg.refine_2.npos.hb
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
x✝ : 0 < nb → 0 < na
H : nb * ↑da - na * ↑db < 0
⊢ 0 < da
[PROOFSTEP]
rwa [pos_iff_ne_zero]
[GOAL]
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ a /. b ≤ c /. d ↔ a * d ≤ c * b
[PROOFSTEP]
rw [Rat.le_iff_Nonneg]
[GOAL]
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ Rat.Nonneg (c /. d - a /. b) ↔ a * d ≤ c * b
[PROOFSTEP]
show Rat.Nonneg _ ↔ _
[GOAL]
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ Rat.Nonneg (c /. d - a /. b) ↔ a * d ≤ c * b
[PROOFSTEP]
rw [← sub_nonneg]
[GOAL]
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ Rat.Nonneg (c /. d - a /. b) ↔ 0 ≤ c * b - a * d
[PROOFSTEP]
simp [sub_eq_add_neg, ne_of_gt b0, ne_of_gt d0, mul_pos d0 b0]
[GOAL]
a b c : ℚ
⊢ a ≤ a
[PROOFSTEP]
rw [Rat.le_iff_Nonneg]
[GOAL]
a b c : ℚ
⊢ Rat.Nonneg (a - a)
[PROOFSTEP]
show Rat.Nonneg (a - a)
[GOAL]
a b c : ℚ
⊢ Rat.Nonneg (a - a)
[PROOFSTEP]
rw [sub_self]
[GOAL]
a b c : ℚ
⊢ Rat.Nonneg 0
[PROOFSTEP]
exact le_refl (0 : ℤ)
[GOAL]
a b c : ℚ
⊢ a ≤ b ∨ b ≤ a
[PROOFSTEP]
have := Rat.nonneg_total (b - a)
[GOAL]
a b c : ℚ
this : Rat.Nonneg (b - a) ∨ Rat.Nonneg (-(b - a))
⊢ a ≤ b ∨ b ≤ a
[PROOFSTEP]
rw [Rat.le_iff_Nonneg, Rat.le_iff_Nonneg]
[GOAL]
a b c : ℚ
this : Rat.Nonneg (b - a) ∨ Rat.Nonneg (-(b - a))
⊢ Rat.Nonneg (b - a) ∨ Rat.Nonneg (a - b)
[PROOFSTEP]
rwa [neg_sub] at this
[GOAL]
a✝ b✝ c a b : ℚ
hab : a ≤ b
hba : b ≤ a
⊢ a = b
[PROOFSTEP]
rw [Rat.le_iff_Nonneg] at hab hba
[GOAL]
a✝ b✝ c a b : ℚ
hab : Rat.Nonneg (b - a)
hba : Rat.Nonneg (a - b)
⊢ a = b
[PROOFSTEP]
rw [sub_eq_add_neg] at hba
[GOAL]
a✝ b✝ c a b : ℚ
hab : Rat.Nonneg (b - a)
hba : Rat.Nonneg (a + -b)
⊢ a = b
[PROOFSTEP]
rw [← neg_sub, sub_eq_add_neg] at hab
[GOAL]
a✝ b✝ c a b : ℚ
hab : Rat.Nonneg (-(a + -b))
hba : Rat.Nonneg (a + -b)
⊢ a = b
[PROOFSTEP]
have := eq_neg_of_add_eq_zero_left (Rat.nonneg_antisymm hba hab)
[GOAL]
a✝ b✝ c a b : ℚ
hab : Rat.Nonneg (-(a + -b))
hba : Rat.Nonneg (a + -b)
this : a = - -b
⊢ a = b
[PROOFSTEP]
rwa [neg_neg] at this
[GOAL]
a✝ b✝ c✝ a b c : ℚ
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c
[PROOFSTEP]
rw [Rat.le_iff_Nonneg] at hab hbc
[GOAL]
a✝ b✝ c✝ a b c : ℚ
hab : Rat.Nonneg (b - a)
hbc : Rat.Nonneg (c - b)
⊢ a ≤ c
[PROOFSTEP]
have : Rat.Nonneg (b - a + (c - b)) := Rat.nonneg_add hab hbc
[GOAL]
a✝ b✝ c✝ a b c : ℚ
hab : Rat.Nonneg (b - a)
hbc : Rat.Nonneg (c - b)
this : Rat.Nonneg (b - a + (c - b))
⊢ a ≤ c
[PROOFSTEP]
simp_rw [sub_eq_add_neg, add_left_comm (b + -a) c (-b), add_comm (b + -a) (-b), add_left_comm (-b) b (-a),
  add_comm (-b) (-a), add_neg_cancel_comm_assoc, ← sub_eq_add_neg] at this
[GOAL]
a✝ b✝ c✝ a b c : ℚ
hab : Rat.Nonneg (b - a)
hbc : Rat.Nonneg (c - b)
this : Rat.Nonneg (c - a)
⊢ a ≤ c
[PROOFSTEP]
rw [Rat.le_iff_Nonneg]
[GOAL]
a✝ b✝ c✝ a b c : ℚ
hab : Rat.Nonneg (b - a)
hbc : Rat.Nonneg (c - b)
this : Rat.Nonneg (c - a)
⊢ Rat.Nonneg (c - a)
[PROOFSTEP]
exact this
[GOAL]
a b c x✝¹ x✝ : ℚ
⊢ x✝¹ < x✝ ↔ x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹
[PROOFSTEP]
rw [← Rat.not_le, and_iff_right_of_imp (Rat.le_total _ _).resolve_left]
  -- Extra instances to short-circuit type class resolution
[GOAL]
a b c x✝¹ x✝ : ℚ
⊢ Decidable ((fun x x_1 => x ≤ x_1) x✝¹ x✝)
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ LT ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ DistribLattice ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ Lattice ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ SemilatticeInf ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ SemilatticeSup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ Inf ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ Sup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ PartialOrder ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ Preorder ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c p q : ℚ
⊢ p ≤ q ↔ p.num * ↑q.den ≤ q.num * ↑p.den
[PROOFSTEP]
rw [← @num_den q, ← @num_den p]
[GOAL]
a b c p q : ℚ
⊢ p.num /. ↑p.den ≤ q.num /. ↑q.den ↔
    (p.num /. ↑p.den).num * ↑(q.num /. ↑q.den).den ≤ (q.num /. ↑q.den).num * ↑(p.num /. ↑p.den).den
[PROOFSTEP]
conv_rhs => simp only [num_den]
[GOAL]
a b c p q : ℚ
| (p.num /. ↑p.den).num * ↑(q.num /. ↑q.den).den ≤ (q.num /. ↑q.den).num * ↑(p.num /. ↑p.den).den
[PROOFSTEP]
simp only [num_den]
[GOAL]
a b c p q : ℚ
| (p.num /. ↑p.den).num * ↑(q.num /. ↑q.den).den ≤ (q.num /. ↑q.den).num * ↑(p.num /. ↑p.den).den
[PROOFSTEP]
simp only [num_den]
[GOAL]
a b c p q : ℚ
| (p.num /. ↑p.den).num * ↑(q.num /. ↑q.den).den ≤ (q.num /. ↑q.den).num * ↑(p.num /. ↑p.den).den
[PROOFSTEP]
simp only [num_den]
[GOAL]
a b c p q : ℚ
⊢ p.num /. ↑p.den ≤ q.num /. ↑q.den ↔ p.num * ↑q.den ≤ q.num * ↑p.den
[PROOFSTEP]
exact Rat.le_def (by exact_mod_cast p.pos) (by exact_mod_cast q.pos)
[GOAL]
a b c p q : ℚ
⊢ 0 < ↑p.den
[PROOFSTEP]
exact_mod_cast p.pos
[GOAL]
a b c p q : ℚ
⊢ 0 < ↑q.den
[PROOFSTEP]
exact_mod_cast q.pos
[GOAL]
a b c p q : ℚ
⊢ p < q ↔ p.num * ↑q.den < q.num * ↑p.den
[PROOFSTEP]
rw [lt_iff_le_and_ne, Rat.le_def']
[GOAL]
a b c p q : ℚ
⊢ p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q ↔ p.num * ↑q.den < q.num * ↑p.den
[PROOFSTEP]
suffices p ≠ q ↔ p.num * q.den ≠ q.num * p.den by
  constructor <;> intro h
  · exact lt_iff_le_and_ne.mpr ⟨h.left, this.mp h.right⟩
  · have tmp := lt_iff_le_and_ne.mp h
    exact ⟨tmp.left, this.mpr tmp.right⟩
[GOAL]
a b c p q : ℚ
this : p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
⊢ p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q ↔ p.num * ↑q.den < q.num * ↑p.den
[PROOFSTEP]
constructor
[GOAL]
case mp
a b c p q : ℚ
this : p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
⊢ p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q → p.num * ↑q.den < q.num * ↑p.den
[PROOFSTEP]
intro h
[GOAL]
case mpr
a b c p q : ℚ
this : p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
⊢ p.num * ↑q.den < q.num * ↑p.den → p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q
[PROOFSTEP]
intro h
[GOAL]
case mp
a b c p q : ℚ
this : p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
h : p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q
⊢ p.num * ↑q.den < q.num * ↑p.den
[PROOFSTEP]
exact lt_iff_le_and_ne.mpr ⟨h.left, this.mp h.right⟩
[GOAL]
case mpr
a b c p q : ℚ
this : p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
h : p.num * ↑q.den < q.num * ↑p.den
⊢ p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q
[PROOFSTEP]
have tmp := lt_iff_le_and_ne.mp h
[GOAL]
case mpr
a b c p q : ℚ
this : p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
h : p.num * ↑q.den < q.num * ↑p.den
tmp : p.num * ↑q.den ≤ q.num * ↑p.den ∧ p.num * ↑q.den ≠ q.num * ↑p.den
⊢ p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q
[PROOFSTEP]
exact ⟨tmp.left, this.mpr tmp.right⟩
[GOAL]
a b c p q : ℚ
⊢ p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
[PROOFSTEP]
exact not_iff_not.mpr eq_iff_mul_eq_mul
[GOAL]
a✝ b c a : ℚ
⊢ Rat.Nonneg a ↔ 0 ≤ a
[PROOFSTEP]
rw [Rat.le_iff_Nonneg]
[GOAL]
a✝ b c a : ℚ
⊢ Rat.Nonneg a ↔ Rat.Nonneg (a - 0)
[PROOFSTEP]
show Rat.Nonneg a ↔ Rat.Nonneg (a - 0)
[GOAL]
a✝ b c a : ℚ
⊢ Rat.Nonneg a ↔ Rat.Nonneg (a - 0)
[PROOFSTEP]
simp
[GOAL]
a✝ b✝ c✝ a b c : ℚ
⊢ c + a ≤ c + b ↔ a ≤ b
[PROOFSTEP]
rw [Rat.le_iff_Nonneg, add_sub_add_left_eq_sub, Rat.le_iff_Nonneg]
[GOAL]
a✝ b✝ c a b : ℚ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b
[PROOFSTEP]
rw [← nonneg_iff_zero_le] at ha hb ⊢
[GOAL]
a✝ b✝ c a b : ℚ
ha : Rat.Nonneg a
hb : Rat.Nonneg b
⊢ Rat.Nonneg (a * b)
[PROOFSTEP]
exact Rat.nonneg_mul ha hb
[GOAL]
a b c : ℚ
src✝² : Field ℚ := field
src✝¹ : LinearOrder ℚ := linearOrder
src✝ : Semiring ℚ := semiring
⊢ 0 ≤ 1
[PROOFSTEP]
decide
[GOAL]
a b c : ℚ
⊢ LinearOrderedCommRing ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ LinearOrderedRing ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ OrderedRing ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ LinearOrderedSemiring ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ OrderedSemiring ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ LinearOrderedAddCommGroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ OrderedAddCommGroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ OrderedCancelAddCommMonoid ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ OrderedAddCommMonoid ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a✝ b c a : ℚ
⊢ a.num ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
simpa [(by cases a; rfl : (-a).num = -a.num)] using @num_nonneg_iff_zero_le (-a)
[GOAL]
a✝ b c a : ℚ
⊢ (-a).num = -a.num
[PROOFSTEP]
cases a
[GOAL]
case mk'
a b c : ℚ
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
⊢ (-mk' num✝ den✝).num = -(mk' num✝ den✝).num
[PROOFSTEP]
rfl
[GOAL]
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b < ↑c / ↑d ↔ a * d < c * b
[PROOFSTEP]
simp only [lt_iff_le_not_le]
[GOAL]
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ∧ ¬↑c / ↑d ≤ ↑a / ↑b ↔ a * d ≤ c * b ∧ ¬c * b ≤ a * d
[PROOFSTEP]
apply and_congr
[GOAL]
case h₁
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ↔ a * d ≤ c * b
[PROOFSTEP]
simp [div_num_den, Rat.le_def b_pos d_pos]
[GOAL]
case h₂
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ¬↑c / ↑d ≤ ↑a / ↑b ↔ ¬c * b ≤ a * d
[PROOFSTEP]
apply not_congr
[GOAL]
case h₂.h
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑c / ↑d ≤ ↑a / ↑b ↔ c * b ≤ a * d
[PROOFSTEP]
simp [div_num_den, Rat.le_def d_pos b_pos]
[GOAL]
a b c q : ℚ
⊢ q < 1 ↔ q.num < ↑q.den
[PROOFSTEP]
simp [Rat.lt_def]
[GOAL]
a b c q : ℚ
⊢ |q| = ↑(Int.natAbs q.num) /. ↑q.den
[PROOFSTEP]
cases' le_total q 0 with hq hq
[GOAL]
case inl
a b c q : ℚ
hq : q ≤ 0
⊢ |q| = ↑(Int.natAbs q.num) /. ↑q.den
[PROOFSTEP]
rw [abs_of_nonpos hq]
[GOAL]
case inl
a b c q : ℚ
hq : q ≤ 0
⊢ -q = ↑(Int.natAbs q.num) /. ↑q.den
[PROOFSTEP]
rw [← @num_den q, ← divInt_zero_one, Rat.le_def (Int.coe_nat_pos.2 q.pos) zero_lt_one, mul_one, zero_mul] at hq
[GOAL]
case inl
a b c q : ℚ
hq : q.num ≤ 0
⊢ -q = ↑(Int.natAbs q.num) /. ↑q.den
[PROOFSTEP]
rw [Int.ofNat_natAbs_of_nonpos hq, ← neg_def, num_den]
[GOAL]
case inr
a b c q : ℚ
hq : 0 ≤ q
⊢ |q| = ↑(Int.natAbs q.num) /. ↑q.den
[PROOFSTEP]
rw [abs_of_nonneg hq]
[GOAL]
case inr
a b c q : ℚ
hq : 0 ≤ q
⊢ q = ↑(Int.natAbs q.num) /. ↑q.den
[PROOFSTEP]
rw [← @num_den q, ← divInt_zero_one, Rat.le_def zero_lt_one (Int.coe_nat_pos.2 q.pos), mul_one, zero_mul] at hq
[GOAL]
case inr
a b c q : ℚ
hq : 0 ≤ q.num
⊢ q = ↑(Int.natAbs q.num) /. ↑q.den
[PROOFSTEP]
rw [Int.natAbs_of_nonneg hq, num_den]