[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Icc a b = 0 ↔ ¬a ≤ b
[PROOFSTEP]
rw [Icc, Finset.val_eq_zero, Finset.Icc_eq_empty_iff]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b = 0 ↔ ¬a < b
[PROOFSTEP]
rw [Ico, Finset.val_eq_zero, Finset.Ico_eq_empty_iff]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ioc a b = 0 ↔ ¬a < b
[PROOFSTEP]
rw [Ioc, Finset.val_eq_zero, Finset.Ioc_eq_empty_iff]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DenselyOrdered α
⊢ Ioo a b = 0 ↔ ¬a < b
[PROOFSTEP]
rw [Ioo, Finset.val_eq_zero, Finset.Ioo_eq_empty_iff]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a a = 0
[PROOFSTEP]
rw [Ico, Finset.Ico_self, Finset.empty_val]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ioc a a = 0
[PROOFSTEP]
rw [Ioc, Finset.Ioc_self, Finset.empty_val]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ioo a a = 0
[PROOFSTEP]
rw [Ioo, Finset.Ioo_self, Finset.empty_val]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hca : c ≤ a
⊢ filter (fun x => x < c) (Ico a b) = ∅
[PROOFSTEP]
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_left hca]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hca : c ≤ a
⊢ ∅.val = ∅
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hbc : b ≤ c
⊢ filter (fun x => x < c) (Ico a b) = Ico a b
[PROOFSTEP]
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_right_le hbc]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
⊢ filter (fun x => x < c) (Ico a b) = Ico a c
[PROOFSTEP]
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_right hcb]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
⊢ (Finset.Ico a c).val = Ico a c
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) c)
hca : c ≤ a
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico a b
[PROOFSTEP]
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_le_left hca]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) b)
⊢ filter (fun x => b ≤ x) (Ico a b) = ∅
[PROOFSTEP]
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_right_le]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) b)
⊢ ∅.val = ∅
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) c)
hac : a ≤ c
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico c b
[PROOFSTEP]
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_left_le hac]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) c)
hac : a ≤ c
⊢ (Finset.Ico c b).val = Ico c b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b a : α
⊢ Icc a a = {a}
[PROOFSTEP]
rw [Icc, Finset.Icc_self, Finset.singleton_val]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ b ::ₘ Ico a b = Icc a b
[PROOFSTEP]
classical
rw [Ico, ← Finset.insert_val_of_not_mem right_not_mem_Ico, Finset.Ico_insert_right h]
rfl
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ b ::ₘ Ico a b = Icc a b
[PROOFSTEP]
rw [Ico, ← Finset.insert_val_of_not_mem right_not_mem_Ico, Finset.Ico_insert_right h]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ (Finset.Icc a b).val = Icc a b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ a ::ₘ Ioo a b = Ico a b
[PROOFSTEP]
classical
rw [Ioo, ← Finset.insert_val_of_not_mem left_not_mem_Ioo, Finset.Ioo_insert_left h]
rfl
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ a ::ₘ Ioo a b = Ico a b
[PROOFSTEP]
rw [Ioo, ← Finset.insert_val_of_not_mem left_not_mem_Ioo, Finset.Ioo_insert_left h]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ (Finset.Ico a b).val = Ico a b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c d : α
h : b ≤ c
x : α
hab : x ∈ Ico a b
hbc : x ∈ Ico c d
⊢ False
[PROOFSTEP]
rw [mem_Ico] at hab hbc
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c d : α
h : b ≤ c
x : α
hab : a ≤ x ∧ x < b
hbc : c ≤ x ∧ x < d
⊢ False
[PROOFSTEP]
exact hab.2.not_le (h.trans hbc.1)
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
⊢ filter (fun x => x ≤ a) (Ico a b) = {a}
[PROOFSTEP]
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_left hab]
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
⊢ {a}.val = {a}
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c✝ d a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ico a b + Ico b c = Ico a c
[PROOFSTEP]
rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ← Finset.union_val,
  Finset.Ico_union_Ico_eq_Ico hab hbc]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
[PROOFSTEP]
rw [Ico, Ico, Ico, ← Finset.inter_val, Finset.Ico_inter_Ico]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c✝ d a b c : α
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
[PROOFSTEP]
rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_lt]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c✝ d a b c : α
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
[PROOFSTEP]
rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_le]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c✝ d a b c : α
⊢ Ico a b - Ico a c = Ico (max a c) b
[PROOFSTEP]
rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_left]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c✝ d a b c : α
⊢ Ico a b - Ico c b = Ico a (min b c)
[PROOFSTEP]
rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_right]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Icc a b) = Icc (c + a) (c + b)
[PROOFSTEP]
classical rw [Icc, Icc, ← Finset.image_add_left_Icc, Finset.image_val,
  ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Icc a b) = Icc (c + a) (c + b)
[PROOFSTEP]
rw [Icc, Icc, ← Finset.image_add_left_Icc, Finset.image_val, ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Ico a b) = Ico (c + a) (c + b)
[PROOFSTEP]
classical rw [Ico, Ico, ← Finset.image_add_left_Ico, Finset.image_val,
  ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Ico a b) = Ico (c + a) (c + b)
[PROOFSTEP]
rw [Ico, Ico, ← Finset.image_add_left_Ico, Finset.image_val, ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Ioc a b) = Ioc (c + a) (c + b)
[PROOFSTEP]
classical rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
  ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Ioc a b) = Ioc (c + a) (c + b)
[PROOFSTEP]
rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val, ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Ioo a b) = Ioo (c + a) (c + b)
[PROOFSTEP]
classical rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val,
  ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Ioo a b) = Ioo (c + a) (c + b)
[PROOFSTEP]
rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val, ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => x + c) (Icc a b) = Icc (a + c) (b + c)
[PROOFSTEP]
simp_rw [add_comm _ c]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Icc a b) = Icc (c + a) (c + b)
[PROOFSTEP]
exact map_add_left_Icc _ _ _
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => x + c) (Ico a b) = Ico (a + c) (b + c)
[PROOFSTEP]
simp_rw [add_comm _ c]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ico a b) = Ico (c + a) (c + b)
[PROOFSTEP]
exact map_add_left_Ico _ _ _
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => x + c) (Ioc a b) = Ioc (a + c) (b + c)
[PROOFSTEP]
simp_rw [add_comm _ c]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ioc a b) = Ioc (c + a) (c + b)
[PROOFSTEP]
exact map_add_left_Ioc _ _ _
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => x + c) (Ioo a b) = Ioo (a + c) (b + c)
[PROOFSTEP]
simp_rw [add_comm _ c]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ioo a b) = Ioo (c + a) (c + b)
[PROOFSTEP]
exact map_add_left_Ioo _ _ _


[GOAL]
n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.fst + x.snd = n
[PROOFSTEP]
rw [antidiagonal, mem_coe, List.Nat.mem_antidiagonal]
[GOAL]
n : ℕ
⊢ ↑card (antidiagonal n) = n + 1
[PROOFSTEP]
rw [antidiagonal, coe_card, List.Nat.length_antidiagonal]
[GOAL]
n : ℕ
⊢ antidiagonal (n + 1) = (0, n + 1) ::ₘ map (Prod.map Nat.succ id) (antidiagonal n)
[PROOFSTEP]
simp only [antidiagonal, List.Nat.antidiagonal_succ, coe_map, cons_coe]
[GOAL]
n : ℕ
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
[PROOFSTEP]
rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, add_comm, antidiagonal, coe_map, coe_add,
  List.singleton_append, cons_coe]
[GOAL]
n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
[PROOFSTEP]
rw [antidiagonal_succ, antidiagonal_succ', map_cons, map_map, Prod_map]
[GOAL]
n : ℕ
⊢ (0, n + 1 + 1) ::ₘ
      (Nat.succ (n + 1, 0).fst, id (n + 1, 0).snd) ::ₘ
        map (Prod.map Nat.succ id ∘ Prod.map id Nat.succ) (antidiagonal n) =
    (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ map Prod.swap (antidiagonal n) = antidiagonal n
[PROOFSTEP]
rw [antidiagonal, coe_map, List.Nat.map_swap_antidiagonal, coe_reverse]


[GOAL]
⊢ LawfulFunctor Multiset
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
⊢ ∀ {α β : Type ?u.250}, Functor.mapConst = Functor.map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
case refine'_2
⊢ ∀ {α : Type ?u.250} (x : Multiset α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_3
⊢ ∀ {α β γ : Type ?u.250} (g : α → β) (h : β → γ) (x : Multiset α), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α✝ β✝ : Type ?u.250
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
try simp
[GOAL]
case refine'_1
α✝ β✝ : Type ?u.250
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α✝ : Type ?u.250
x✝ : Multiset α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
try simp
[GOAL]
case refine'_2
α✝ : Type ?u.250
x✝ : Multiset α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
simp
[GOAL]
case refine'_3
α✝ β✝ γ✝ : Type ?u.250
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Multiset α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
try simp
[GOAL]
case refine'_3
α✝ β✝ γ✝ : Type ?u.250
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Multiset α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
simp
[GOAL]
case refine'_1
α✝ β✝ : Type ?u.250
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
⊢ Multiset α' → F (Multiset β')
[PROOFSTEP]
refine' Quotient.lift (Functor.map Coe.coe ∘ Traversable.traverse f) _
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
⊢ ∀ (a b : List α'),
    a ≈ b → (Functor.map Coe.coe ∘ Traversable.traverse f) a = (Functor.map Coe.coe ∘ Traversable.traverse f) b
[PROOFSTEP]
introv p
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
p : a ≈ b
⊢ (Functor.map Coe.coe ∘ Traversable.traverse f) a = (Functor.map Coe.coe ∘ Traversable.traverse f) b
[PROOFSTEP]
unfold Function.comp
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
p : a ≈ b
⊢ Coe.coe <$> Traversable.traverse f a = Coe.coe <$> Traversable.traverse f b
[PROOFSTEP]
induction p
[GOAL]
case nil
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
⊢ Coe.coe <$> Traversable.traverse f [] = Coe.coe <$> Traversable.traverse f []
case cons
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x✝ : α'
l₁✝ l₂✝ : List α'
a✝ : l₁✝ ~ l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
⊢ Coe.coe <$> Traversable.traverse f (x✝ :: l₁✝) = Coe.coe <$> Traversable.traverse f (x✝ :: l₂✝)
case swap
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x✝ y✝ : α'
l✝ : List α'
⊢ Coe.coe <$> Traversable.traverse f (y✝ :: x✝ :: l✝) = Coe.coe <$> Traversable.traverse f (x✝ :: y✝ :: l✝)
case trans
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁✝ l₂✝ l₃✝ : List α'
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₂✝ = Coe.coe <$> Traversable.traverse f l₃✝
⊢ Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₃✝
[PROOFSTEP]
case nil => rfl
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
⊢ Coe.coe <$> Traversable.traverse f [] = Coe.coe <$> Traversable.traverse f []
[PROOFSTEP]
case nil => rfl
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
⊢ Coe.coe <$> Traversable.traverse f [] = Coe.coe <$> Traversable.traverse f []
[PROOFSTEP]
rfl
[GOAL]
case cons
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x✝ : α'
l₁✝ l₂✝ : List α'
a✝ : l₁✝ ~ l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
⊢ Coe.coe <$> Traversable.traverse f (x✝ :: l₁✝) = Coe.coe <$> Traversable.traverse f (x✝ :: l₂✝)
case swap
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x✝ y✝ : α'
l✝ : List α'
⊢ Coe.coe <$> Traversable.traverse f (y✝ :: x✝ :: l✝) = Coe.coe <$> Traversable.traverse f (x✝ :: y✝ :: l✝)
case trans
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁✝ l₂✝ l₃✝ : List α'
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₂✝ = Coe.coe <$> Traversable.traverse f l₃✝
⊢ Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₃✝
[PROOFSTEP]
case cons x l₁ l₂ _
  h =>
  have :
    Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₁ =
      Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₂ :=
    by rw [h]
  simpa [functor_norm] using this
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
a✝ : l₁ ~ l₂
h : Coe.coe <$> Traversable.traverse f l₁ = Coe.coe <$> Traversable.traverse f l₂
⊢ Coe.coe <$> Traversable.traverse f (x :: l₁) = Coe.coe <$> Traversable.traverse f (x :: l₂)
[PROOFSTEP]
case cons x l₁ l₂ _
  h =>
  have :
    Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₁ =
      Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₂ :=
    by rw [h]
  simpa [functor_norm] using this
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
a✝ : l₁ ~ l₂
h : Coe.coe <$> Traversable.traverse f l₁ = Coe.coe <$> Traversable.traverse f l₂
⊢ Coe.coe <$> Traversable.traverse f (x :: l₁) = Coe.coe <$> Traversable.traverse f (x :: l₂)
[PROOFSTEP]
have :
  Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₁ =
    Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₂ :=
  by rw [h]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
a✝ : l₁ ~ l₂
h : Coe.coe <$> Traversable.traverse f l₁ = Coe.coe <$> Traversable.traverse f l₂
⊢ (Seq.seq (cons <$> f x) fun x => Coe.coe <$> Traversable.traverse f l₁) =
    Seq.seq (cons <$> f x) fun x => Coe.coe <$> Traversable.traverse f l₂
[PROOFSTEP]
rw [h]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
a✝ : l₁ ~ l₂
h : Coe.coe <$> Traversable.traverse f l₁ = Coe.coe <$> Traversable.traverse f l₂
this :
  (Seq.seq (cons <$> f x) fun x => Coe.coe <$> Traversable.traverse f l₁) =
    Seq.seq (cons <$> f x) fun x => Coe.coe <$> Traversable.traverse f l₂
⊢ Coe.coe <$> Traversable.traverse f (x :: l₁) = Coe.coe <$> Traversable.traverse f (x :: l₂)
[PROOFSTEP]
simpa [functor_norm] using this
[GOAL]
case swap
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x✝ y✝ : α'
l✝ : List α'
⊢ Coe.coe <$> Traversable.traverse f (y✝ :: x✝ :: l✝) = Coe.coe <$> Traversable.traverse f (x✝ :: y✝ :: l✝)
case trans
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁✝ l₂✝ l₃✝ : List α'
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₂✝ = Coe.coe <$> Traversable.traverse f l₃✝
⊢ Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₃✝
[PROOFSTEP]
case swap x y
  l =>
  have :
    (fun a b (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x =
      (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y :=
    by
    rw [CommApplicative.commutative_map]
    congr
    funext a b l
    simpa [flip] using Perm.swap a b l
  simp [(· ∘ ·), this, functor_norm, Coe.coe]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ Coe.coe <$> Traversable.traverse f (y :: x :: l) = Coe.coe <$> Traversable.traverse f (x :: y :: l)
[PROOFSTEP]
case swap x y
  l =>
  have :
    (fun a b (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x =
      (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y :=
    by
    rw [CommApplicative.commutative_map]
    congr
    funext a b l
    simpa [flip] using Perm.swap a b l
  simp [(· ∘ ·), this, functor_norm, Coe.coe]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ Coe.coe <$> Traversable.traverse f (y :: x :: l) = Coe.coe <$> Traversable.traverse f (x :: y :: l)
[PROOFSTEP]
have :
  (fun a b (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x =
    (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y :=
  by
  rw [CommApplicative.commutative_map]
  congr
  funext a b l
  simpa [flip] using Perm.swap a b l
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ (Seq.seq ((fun a b l => ↑(a :: b :: l)) <$> f y) fun x_1 => f x) =
    Seq.seq ((fun a b l => ↑(a :: b :: l)) <$> f x) fun x => f y
[PROOFSTEP]
rw [CommApplicative.commutative_map]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ (Seq.seq ((flip fun a b l => ↑(a :: b :: l)) <$> f x) fun x => f y) =
    Seq.seq ((fun a b l => ↑(a :: b :: l)) <$> f x) fun x => f y
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ (flip fun a b l => ↑(a :: b :: l)) = fun a b l => ↑(a :: b :: l)
[PROOFSTEP]
funext a b l
[GOAL]
case e_a.e_a.h.h.h
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a✝ b✝ : List α'
x y : α'
l✝ : List α'
a b : β'
l : List β'
⊢ flip (fun a b l => ↑(a :: b :: l)) a b l = ↑(a :: b :: l)
[PROOFSTEP]
simpa [flip] using Perm.swap a b l
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
this :
  (Seq.seq ((fun a b l => ↑(a :: b :: l)) <$> f y) fun x_1 => f x) =
    Seq.seq ((fun a b l => ↑(a :: b :: l)) <$> f x) fun x => f y
⊢ Coe.coe <$> Traversable.traverse f (y :: x :: l) = Coe.coe <$> Traversable.traverse f (x :: y :: l)
[PROOFSTEP]
simp [(· ∘ ·), this, functor_norm, Coe.coe]
[GOAL]
case trans
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁✝ l₂✝ l₃✝ : List α'
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₂✝ = Coe.coe <$> Traversable.traverse f l₃✝
⊢ Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₃✝
[PROOFSTEP]
case trans => simp [*]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁✝ l₂✝ l₃✝ : List α'
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₂✝ = Coe.coe <$> Traversable.traverse f l₃✝
⊢ Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₃✝
[PROOFSTEP]
case trans => simp [*]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁✝ l₂✝ l₃✝ : List α'
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₂✝ = Coe.coe <$> Traversable.traverse f l₃✝
⊢ Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₃✝
[PROOFSTEP]
simp [*]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α✝ : Type ?u.36389
x✝ : Multiset α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
simp only [fmap_def, id_eq, map_id']
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α✝ β✝ : Type ?u.36389
x✝¹ : α✝
x✝ : α✝ → Multiset β✝
⊢ pure x✝¹ >>= x✝ = x✝ x✝¹
[PROOFSTEP]
simp only [pure_def, bind_def, singleton_bind]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α✝ β✝ : Type ?u.36389
x✝¹ : α✝ → β✝
x✝ : Multiset α✝
⊢ (do
      let y ← x✝
      pure (x✝¹ y)) =
    x✝¹ <$> x✝
[PROOFSTEP]
simp only [pure_def, bind_def, bind_singleton, fmap_def]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α β : Type u_1
h : α → β
⊢ Functor.map h ∘ Coe.coe = Coe.coe ∘ Functor.map h
[PROOFSTEP]
funext
[GOAL]
case h
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α β : Type u_1
h : α → β
x✝ : List α
⊢ (Functor.map h ∘ Coe.coe) x✝ = (Coe.coe ∘ Functor.map h) x✝
[PROOFSTEP]
simp only [Function.comp_apply, Coe.coe, fmap_def, coe_map, List.map_eq_map]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α : Type u_1
x : Multiset α
⊢ traverse pure x = x
[PROOFSTEP]
refine' Quotient.inductionOn x _
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α : Type u_1
x : Multiset α
⊢ ∀ (a : List α), traverse pure (Quotient.mk (isSetoid α) a) = Quotient.mk (isSetoid α) a
[PROOFSTEP]
intro
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α : Type u_1
x : Multiset α
a✝ : List α
⊢ traverse pure (Quotient.mk (isSetoid α) a✝) = Quotient.mk (isSetoid α) a✝
[PROOFSTEP]
simp [traverse, Coe.coe]
[GOAL]
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : CommApplicative F
α' β' : Type u
f : α' → F β'
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) x = Comp.mk (traverse h <$> traverse g x)
[PROOFSTEP]
refine' Quotient.inductionOn x _
[GOAL]
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : CommApplicative F
α' β' : Type u
f : α' → F β'
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
⊢ ∀ (a : List α),
    traverse (Comp.mk ∘ Functor.map h ∘ g) (Quotient.mk (isSetoid α) a) =
      Comp.mk (traverse h <$> traverse g (Quotient.mk (isSetoid α) a))
[PROOFSTEP]
intro
[GOAL]
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : CommApplicative F
α' β' : Type u
f : α' → F β'
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
a✝ : List α
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) (Quotient.mk (isSetoid α) a✝) =
    Comp.mk (traverse h <$> traverse g (Quotient.mk (isSetoid α) a✝))
[PROOFSTEP]
simp only [traverse, quot_mk_to_coe, lift_coe, Coe.coe, Function.comp_apply, Functor.map_map, functor_norm]
[GOAL]
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : CommApplicative F
α' β' : Type u
f : α' → F β'
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
a✝ : List α
⊢ Comp.mk (((fun x => ofList <$> x) ∘ Traversable.traverse h) <$> Traversable.traverse g a✝) =
    Comp.mk
      ((Quotient.lift (Functor.map ofList ∘ Traversable.traverse h)
            (_ :
              ∀ (a b : List β),
                a ≈ b →
                  (Functor.map Coe.coe ∘ Traversable.traverse h) a = (Functor.map Coe.coe ∘ Traversable.traverse h) b) ∘
          ofList) <$>
        Traversable.traverse g a✝)
[PROOFSTEP]
simp only [Function.comp, lift_coe]
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
⊢ Functor.map h <$> traverse g x = traverse (Functor.map h ∘ g) x
[PROOFSTEP]
refine' Quotient.inductionOn x _
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
⊢ ∀ (a : List α),
    Functor.map h <$> traverse g (Quotient.mk (isSetoid α) a) =
      traverse (Functor.map h ∘ g) (Quotient.mk (isSetoid α) a)
[PROOFSTEP]
intro
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
a✝ : List α
⊢ Functor.map h <$> traverse g (Quotient.mk (isSetoid α) a✝) =
    traverse (Functor.map h ∘ g) (Quotient.mk (isSetoid α) a✝)
[PROOFSTEP]
simp only [traverse, quot_mk_to_coe, lift_coe, Function.comp_apply, Functor.map_map, map_comp_coe]
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
a✝ : List α
⊢ (Coe.coe ∘ Functor.map h) <$> Traversable.traverse g a✝ = Coe.coe <$> Traversable.traverse (Functor.map h ∘ g) a✝
[PROOFSTEP]
rw [LawfulFunctor.comp_map, Traversable.map_traverse']
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
a✝ : List α
⊢ Coe.coe <$> Functor.map h <$> Traversable.traverse g a✝ =
    Coe.coe <$> (Functor.map (Functor.map h) ∘ Traversable.traverse g) a✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
⊢ traverse h (map g x) = traverse (h ∘ g) x
[PROOFSTEP]
refine' Quotient.inductionOn x _
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
⊢ ∀ (a : List α), traverse h (map g (Quotient.mk (isSetoid α) a)) = traverse (h ∘ g) (Quotient.mk (isSetoid α) a)
[PROOFSTEP]
intro
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
a✝ : List α
⊢ traverse h (map g (Quotient.mk (isSetoid α) a✝)) = traverse (h ∘ g) (Quotient.mk (isSetoid α) a✝)
[PROOFSTEP]
simp only [traverse, quot_mk_to_coe, coe_map, lift_coe, Function.comp_apply]
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
a✝ : List α
⊢ Coe.coe <$> Traversable.traverse h (List.map g a✝) = Coe.coe <$> Traversable.traverse (h ∘ g) a✝
[PROOFSTEP]
rw [← Traversable.traverse_map h g, List.map_eq_map]
[GOAL]
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : CommApplicative F
α' β' : Type u
f✝ : α' → F β'
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
⊢ (fun {α} => ApplicativeTransformation.app eta α) (traverse f x) =
    traverse ((fun {α} => ApplicativeTransformation.app eta α) ∘ f) x
[PROOFSTEP]
refine' Quotient.inductionOn x _
[GOAL]
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : CommApplicative F
α' β' : Type u
f✝ : α' → F β'
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
⊢ ∀ (a : List α),
    (fun {α} => ApplicativeTransformation.app eta α) (traverse f (Quotient.mk (isSetoid α) a)) =
      traverse ((fun {α} => ApplicativeTransformation.app eta α) ∘ f) (Quotient.mk (isSetoid α) a)
[PROOFSTEP]
intro
[GOAL]
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : CommApplicative F
α' β' : Type u
f✝ : α' → F β'
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
a✝ : List α
⊢ (fun {α} => ApplicativeTransformation.app eta α) (traverse f (Quotient.mk (isSetoid α) a✝)) =
    traverse ((fun {α} => ApplicativeTransformation.app eta α) ∘ f) (Quotient.mk (isSetoid α) a✝)
[PROOFSTEP]
simp only [quot_mk_to_coe, traverse, lift_coe, Function.comp_apply, ApplicativeTransformation.preserves_map,
  LawfulTraversable.naturality]


[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b : α
l : List α
⊢ List.foldl (fun x y => op y x) b l = List.foldl op b l
[PROOFSTEP]
simp [hc.comm]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = op (fold op b s) a
[PROOFSTEP]
simp [hc.comm]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op b a) s
[PROOFSTEP]
rw [fold_eq_foldl, foldl_cons, ← fold_eq_foldl]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op a b) s
[PROOFSTEP]
rw [fold_cons'_right, hc.comm]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b₁ b₂ : α
s₁ s₂ : Multiset α
⊢ fold op (op b₁ b₂) (s₁ + 0) = op (fold op b₁ s₁) (fold op b₂ 0)
[PROOFSTEP]
rw [add_zero, fold_zero, ← fold_cons'_right, ← fold_cons_right op]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))
[PROOFSTEP]
rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm a, ha.assoc]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
ι : Type u_3
s : Multiset ι
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b s)) (bind s t) = fold op b₀ (map (fun i => fold op (b i) (t i)) s)
[PROOFSTEP]
induction' s using Multiset.induction_on with a ha ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
ι : Type u_3
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i => fold op (b i) (t i)) 0)
[PROOFSTEP]
rw [zero_bind, map_zero, map_zero, fold_zero]
[GOAL]
case cons
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha✝ : IsAssociative α op
ι : Type u_3
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (bind ha t) = fold op b₀ (map (fun i => fold op (b i) (t i)) ha)
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) (bind (a ::ₘ ha) t) =
    fold op b₀ (map (fun i => fold op (b i) (t i)) (a ::ₘ ha))
[PROOFSTEP]
rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
f g : β → α
u₁ u₂ : α
s : Multiset β
⊢ fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) 0) = op (fold op u₁ (map f 0)) (fold op u₂ (map g 0))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) (a ::ₘ b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
[PROOFSTEP]
rw [map_cons, fold_cons_left, h, map_cons, fold_cons_left, map_cons, fold_cons_right, ha.assoc, ← ha.assoc (g a),
  hc.comm (g a), ha.assoc, hc.comm (g a), ha.assoc]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
op' : β → β → β
inst✝¹ : IsCommutative β op'
inst✝ : IsAssociative β op'
m : α → β
hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)
b : α
s : Multiset α
⊢ fold op' (m b) (map m 0) = m (fold op b 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
op' : β → β → β
inst✝¹ : IsCommutative β op'
inst✝ : IsAssociative β op'
m : α → β
hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)
b : α
s : Multiset α
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    fold op' (m b) (map m s) = m (fold op b s) → fold op' (m b) (map m (a ::ₘ s)) = m (fold op b (a ::ₘ s))
[PROOFSTEP]
simp (config := { contextual := true }) [hm]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
b₁ b₂ : α
⊢ op (fold op b₁ (s₁ ∪ s₂)) (fold op b₂ (s₁ ∩ s₂)) = op (fold op b₁ s₁) (fold op b₂ s₂)
[PROOFSTEP]
rw [← fold_add op, union_add_inter, fold_add op]
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
hi : IsIdempotent α op
s : Multiset α
b : α
⊢ fold op b (dedup 0) = fold op b 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
hi : IsIdempotent α op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b (dedup s) = fold op b s
⊢ fold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
hi : IsIdempotent α op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b (dedup s) = fold op b s
h : a ∈ s
⊢ fold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s)
[PROOFSTEP]
simp [IH, h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
hi : IsIdempotent α op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b (dedup s) = fold op b s
h : ¬a ∈ s
⊢ fold op b (dedup (a ::ₘ s)) = fold op b (a ::ₘ s)
[PROOFSTEP]
simp [IH, h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
hi : IsIdempotent α op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b (dedup s) = fold op b s
h : a ∈ s
⊢ fold op b s = op a (fold op b s)
[PROOFSTEP]
show fold op b s = op a (fold op b s)
[GOAL]
case pos
α : Type u_1
β : Type u_2
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
hi : IsIdempotent α op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b (dedup s) = fold op b s
h : a ∈ s
⊢ fold op b s = op a (fold op b s)
[PROOFSTEP]
rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : CanonicallyLinearOrderedAddMonoid α
l : Multiset α
n : α
h : ∀ (x : α), x ∈ l → x ≤ n
⊢ fold max ⊥ l ≤ n
[PROOFSTEP]
induction l using Quotient.inductionOn
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : CanonicallyLinearOrderedAddMonoid α
n : α
a✝ : List α
h : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a✝ → x ≤ n
⊢ fold max ⊥ (Quotient.mk (List.isSetoid α) a✝) ≤ n
[PROOFSTEP]
simpa using List.max_le_of_forall_le _ _ h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ count a s ≤ count a (fold max 0 (map (fun a => count a s) s) • dedup s)
[PROOFSTEP]
rw [count_nsmul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a (dedup s)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a (dedup s)
[PROOFSTEP]
refine' le_trans _ (Nat.mul_le_mul_left _ <| count_pos.2 <| mem_dedup.2 h)
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * succ 0
[PROOFSTEP]
have : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a)) := by simp [le_max_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a))
[PROOFSTEP]
simp [le_max_left]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
this : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a))
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * succ 0
[PROOFSTEP]
rw [cons_erase h] at this
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
this : count a s ≤ fold max 0 (map (fun a => count a s) s)
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * succ 0
[PROOFSTEP]
simpa [mul_succ] using this
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ count a s ≤ fold max 0 (map (fun a => count a s) s) * count a (dedup s)
[PROOFSTEP]
simp [count_eq_zero.2 h, Nat.zero_le]


[GOAL]
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Multiset α
a : α
⊢ a ∈ sort r s ↔ a ∈ s
[PROOFSTEP]
rw [← mem_coe, sort_eq]


[GOAL]
α : Type u_1
s : Multiset (Multiset α)
a₀ a₁ : Multiset α
x✝ pi : Multiset (Multiset α)
⊢ HEq (bind a₀ fun a => map (cons a) (bind a₁ fun a => map (cons a) pi))
    (bind a₁ fun a => map (cons a) (bind a₀ fun a => map (cons a) pi))
[PROOFSTEP]
simp [map_bind, bind_bind a₀ a₁, cons_swap]
[GOAL]
α : Type u_1
a : List α
l : List (List α)
⊢ Sections ↑(List.map (fun l => ↑l) (a :: l)) = ↑(List.map (fun l => ↑l) (List.sections (a :: l)))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
a : List α
l : List (List α)
⊢ Sections ↑(↑a :: List.map (fun l => ↑l) l) =
    ↑(List.map (fun l => ↑l) (List.bind (List.sections l) fun s => List.map (fun a => a :: s) a))
[PROOFSTEP]
rw [← cons_coe, sections_cons, bind_map_comm, coe_sections l]
[GOAL]
α : Type u_1
a : List α
l : List (List α)
⊢ (bind ↑(List.map (fun l => ↑l) (List.sections l)) fun b => map (fun a => a ::ₘ b) ↑a) =
    ↑(List.map (fun l => ↑l) (List.bind (List.sections l) fun s => List.map (fun a => a :: s) a))
[PROOFSTEP]
simp [List.sections, (· ∘ ·), List.bind]
[GOAL]
α : Type u_1
s t : Multiset (Multiset α)
⊢ Sections (0 + t) = bind (Sections 0) fun m => map ((fun x x_1 => x + x_1) m) (Sections t)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s✝ t : Multiset (Multiset α)
a : Multiset α
s : Multiset (Multiset α)
ih : Sections (s + t) = bind (Sections s) fun m => map ((fun x x_1 => x + x_1) m) (Sections t)
⊢ Sections (a ::ₘ s + t) = bind (Sections (a ::ₘ s)) fun m => map ((fun x x_1 => x + x_1) m) (Sections t)
[PROOFSTEP]
simp [ih, bind_assoc, map_bind, bind_map]
[GOAL]
α : Type u_1
s : Multiset (Multiset α)
⊢ ∀ {a : Multiset α}, a ∈ Sections s ↔ Rel (fun s a => a ∈ s) s a
[PROOFSTEP]
induction s using Multiset.induction_on
[GOAL]
case empty
α : Type u_1
⊢ ∀ {a : Multiset α}, a ∈ Sections 0 ↔ Rel (fun s a => a ∈ s) 0 a
case cons
α : Type u_1
a✝¹ : Multiset α
s✝ : Multiset (Multiset α)
a✝ : ∀ {a : Multiset α}, a ∈ Sections s✝ ↔ Rel (fun s a => a ∈ s) s✝ a
⊢ ∀ {a : Multiset α}, a ∈ Sections (a✝¹ ::ₘ s✝) ↔ Rel (fun s a => a ∈ s) (a✝¹ ::ₘ s✝) a
[PROOFSTEP]
case empty => simp
[GOAL]
α : Type u_1
⊢ ∀ {a : Multiset α}, a ∈ Sections 0 ↔ Rel (fun s a => a ∈ s) 0 a
[PROOFSTEP]
case empty => simp
[GOAL]
α : Type u_1
⊢ ∀ {a : Multiset α}, a ∈ Sections 0 ↔ Rel (fun s a => a ∈ s) 0 a
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
a✝¹ : Multiset α
s✝ : Multiset (Multiset α)
a✝ : ∀ {a : Multiset α}, a ∈ Sections s✝ ↔ Rel (fun s a => a ∈ s) s✝ a
⊢ ∀ {a : Multiset α}, a ∈ Sections (a✝¹ ::ₘ s✝) ↔ Rel (fun s a => a ∈ s) (a✝¹ ::ₘ s✝) a
[PROOFSTEP]
case cons a a' ih => simp [ih, rel_cons_left, eq_comm]
[GOAL]
α : Type u_1
a : Multiset α
a' : Multiset (Multiset α)
ih : ∀ {a : Multiset α}, a ∈ Sections a' ↔ Rel (fun s a => a ∈ s) a' a
⊢ ∀ {a_1 : Multiset α}, a_1 ∈ Sections (a ::ₘ a') ↔ Rel (fun s a => a ∈ s) (a ::ₘ a') a_1
[PROOFSTEP]
case cons a a' ih => simp [ih, rel_cons_left, eq_comm]
[GOAL]
α : Type u_1
a : Multiset α
a' : Multiset (Multiset α)
ih : ∀ {a : Multiset α}, a ∈ Sections a' ↔ Rel (fun s a => a ∈ s) a' a
⊢ ∀ {a_1 : Multiset α}, a_1 ∈ Sections (a ::ₘ a') ↔ Rel (fun s a => a ∈ s) (a ::ₘ a') a_1
[PROOFSTEP]
simp [ih, rel_cons_left, eq_comm]
[GOAL]
α : Type u_1
s : Multiset (Multiset α)
⊢ ↑card (Sections 0) = prod (map (↑card) 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s : Multiset (Multiset α)
⊢ ∀ ⦃a : Multiset α⦄ {s : Multiset (Multiset α)},
    ↑card (Sections s) = prod (map (↑card) s) → ↑card (Sections (a ::ₘ s)) = prod (map (↑card) (a ::ₘ s))
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
s : Multiset (Multiset α)
⊢ prod (map sum 0) = sum (map prod (Sections 0))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
s✝ : Multiset (Multiset α)
a : Multiset α
s : Multiset (Multiset α)
ih : prod (map sum s) = sum (map prod (Sections s))
⊢ prod (map sum (a ::ₘ s)) = sum (map prod (Sections (a ::ₘ s)))
[PROOFSTEP]
simp [ih, map_bind, sum_map_mul_left, sum_map_mul_right]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : List α
L : List (List α)
⊢ join ↑(List.map ofList (l :: L)) = ↑(List.join (l :: L))
[PROOFSTEP]
simp only [join, List.map, coe_sum, List.sum_cons, List.join, ← coe_add, ← coe_join L]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
S : Multiset (Multiset α)
⊢ a ∈ join 0 ↔ ∃ s, s ∈ 0 ∧ a ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
S : Multiset (Multiset α)
⊢ ∀ ⦃a_1 : Multiset α⦄ {s : Multiset (Multiset α)},
    (a ∈ join s ↔ ∃ s_1, s_1 ∈ s ∧ a ∈ s_1) → (a ∈ join (a_1 ::ₘ s) ↔ ∃ s_1, s_1 ∈ a_1 ::ₘ s ∧ a ∈ s_1)
[PROOFSTEP]
simp (config := { contextual := true }) [or_and_right, exists_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
S : Multiset (Multiset α)
⊢ ↑card (join 0) = sum (map (↑card) 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
S : Multiset (Multiset α)
⊢ ∀ ⦃a : Multiset α⦄ {s : Multiset (Multiset α)},
    ↑card (join s) = sum (map (↑card) s) → ↑card (join (a ::ₘ s)) = sum (map (↑card) (a ::ₘ s))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
h : Rel (Rel r) s t
⊢ Rel r (join s) (join t)
[PROOFSTEP]
induction h
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
⊢ Rel r (join 0) (join 0)
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
a✝² : Multiset α
b✝ : Multiset β
as✝ : Multiset (Multiset α)
bs✝ : Multiset (Multiset β)
a✝¹ : Rel r a✝² b✝
a✝ : Rel (Rel r) as✝ bs✝
a_ih✝ : Rel r (join as✝) (join bs✝)
⊢ Rel r (join (a✝² ::ₘ as✝)) (join (b✝ ::ₘ bs✝))
[PROOFSTEP]
case zero => simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
⊢ Rel r (join 0) (join 0)
[PROOFSTEP]
case zero => simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
⊢ Rel r (join 0) (join 0)
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
a✝² : Multiset α
b✝ : Multiset β
as✝ : Multiset (Multiset α)
bs✝ : Multiset (Multiset β)
a✝¹ : Rel r a✝² b✝
a✝ : Rel (Rel r) as✝ bs✝
a_ih✝ : Rel r (join as✝) (join bs✝)
⊢ Rel r (join (a✝² ::ₘ as✝)) (join (b✝ ::ₘ bs✝))
[PROOFSTEP]
case cons a b s t hab hst ih => simpa using hab.add ih
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s✝ : Multiset (Multiset α)
t✝ : Multiset (Multiset β)
a : Multiset α
b : Multiset β
s : Multiset (Multiset α)
t : Multiset (Multiset β)
hab : Rel r a b
hst : Rel (Rel r) s t
ih : Rel r (join s) (join t)
⊢ Rel r (join (a ::ₘ s)) (join (b ::ₘ t))
[PROOFSTEP]
case cons a b s t hab hst ih => simpa using hab.add ih
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
s✝ : Multiset (Multiset α)
t✝ : Multiset (Multiset β)
a : Multiset α
b : Multiset β
s : Multiset (Multiset α)
t : Multiset (Multiset β)
hab : Rel r a b
hst : Rel (Rel r) s t
ih : Rel r (join s) (join t)
⊢ Rel r (join (a ::ₘ s)) (join (b ::ₘ t))
[PROOFSTEP]
simpa using hab.add ih
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
l : List α
f : α → List β
⊢ (bind ↑l fun a => ↑(f a)) = ↑(List.bind l f)
[PROOFSTEP]
rw [List.bind, ← coe_join, List.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
l : List α
f : α → List β
⊢ (bind ↑l fun a => ↑(f a)) = join ↑(List.map (ofList ∘ f) l)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f g : α → Multiset β
⊢ bind (a ::ₘ s) f = f a + bind s f
[PROOFSTEP]
simp [bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f g : α → Multiset β
⊢ bind {a} f = f a
[PROOFSTEP]
simp [bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f g : α → Multiset β
⊢ bind (s + t) f = bind s f + bind t f
[PROOFSTEP]
simp [bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f g : α → Multiset β
⊢ (bind s fun x => 0) = 0
[PROOFSTEP]
simp [bind, join, nsmul_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f g : α → Multiset β
⊢ (bind s fun a => f a + g a) = bind s f + bind s g
[PROOFSTEP]
simp [bind, join]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g✝ : α → Multiset β
f : α → β
g : α → Multiset β
⊢ (bind 0 fun a => f a ::ₘ g a) = map f 0 + bind 0 g
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g✝ : α → Multiset β
f : α → β
g : α → Multiset β
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (bind s fun a => f a ::ₘ g a) = map f s + bind s g →
      (bind (a ::ₘ s) fun a => f a ::ₘ g a) = map f (a ::ₘ s) + bind (a ::ₘ s) g
[PROOFSTEP]
simp (config := { contextual := true }) [add_comm, add_left_comm, add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
f : α → β
⊢ (bind 0 fun x => {f x}) = map f 0
[PROOFSTEP]
rw [zero_bind, map_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
f : α → β
⊢ ∀ ⦃a : α⦄ {s : Multiset α}, (bind s fun x => {f x}) = map f s → (bind (a ::ₘ s) fun x => {f x}) = map f (a ::ₘ s)
[PROOFSTEP]
simp [singleton_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t : Multiset α
f✝ g : α → Multiset β
b : β
s : Multiset α
f : α → Multiset β
⊢ b ∈ bind s f ↔ ∃ a, a ∈ s ∧ b ∈ f a
[PROOFSTEP]
simp [bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f g : α → Multiset β
⊢ ↑card (bind s f) = sum (map (↑card ∘ f) s)
[PROOFSTEP]
simp [bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g✝ f g : α → Multiset β
m : Multiset α
⊢ (∀ (a : α), a ∈ m → f a = g a) → bind m f = bind m g
[PROOFSTEP]
simp (config := { contextual := true }) [bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
β' : Type u_2
m : Multiset α
f : α → Multiset β
f' : α → Multiset β'
h : β = β'
hf : ∀ (a : α), a ∈ m → HEq (f a) (f' a)
⊢ HEq (bind m f) (bind m f')
[PROOFSTEP]
subst h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
f f' : α → Multiset β
hf : ∀ (a : α), a ∈ m → HEq (f a) (f' a)
⊢ HEq (bind m f) (bind m f')
[PROOFSTEP]
simp only [heq_eq_eq] at hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
f f' : α → Multiset β
hf : ∀ (a : α), a ∈ m → f a = f' a
⊢ HEq (bind m f) (bind m f')
[PROOFSTEP]
simp [bind_congr hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : α → Multiset β
f : β → γ
⊢ map f (bind 0 n) = bind 0 fun a => map f (n a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : α → Multiset β
f : β → γ
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (map f (bind s n) = bind s fun a => map f (n a)) → map f (bind (a ::ₘ s) n) = bind (a ::ₘ s) fun a => map f (n a)
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : β → Multiset γ
f : α → β
⊢ bind (map f 0) n = bind 0 fun a => n (f a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : β → Multiset γ
f : α → β
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (bind (map f s) n = bind s fun a => n (f a)) → bind (map f (a ::ₘ s)) n = bind (a ::ₘ s) fun a => n (f a)
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t : Multiset α
f✝ g✝ : α → Multiset β
s : Multiset α
f : α → Multiset β
g : β → Multiset γ
⊢ bind (bind 0 f) g = bind 0 fun a => bind (f a) g
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t : Multiset α
f✝ g✝ : α → Multiset β
s : Multiset α
f : α → Multiset β
g : β → Multiset γ
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (bind (bind s f) g = bind s fun a => bind (f a) g) →
      bind (bind (a ::ₘ s) f) g = bind (a ::ₘ s) fun a => bind (f a) g
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : Multiset β
f : α → β → Multiset γ
⊢ (bind 0 fun a => bind n fun b => f a b) = bind n fun b => bind 0 fun a => f a b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : Multiset β
f : α → β → Multiset γ
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((bind s fun a => bind n fun b => f a b) = bind n fun b => bind s fun a => f a b) →
      (bind (a ::ₘ s) fun a => bind n fun b => f a b) = bind n fun b => bind (a ::ₘ s) fun a => f a b
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : Multiset β
f : α → β → γ
⊢ (bind 0 fun a => map (fun b => f a b) n) = bind n fun b => map (fun a => f a b) 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : Multiset β
f : α → β → γ
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((bind s fun a => map (fun b => f a b) n) = bind n fun b => map (fun a => f a b) s) →
      (bind (a ::ₘ s) fun a => map (fun b => f a b) n) = bind n fun b => map (fun a => f a b) (a ::ₘ s)
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t✝ : Multiset α
f g : α → Multiset β
inst✝ : CommMonoid β
s : Multiset α
t : α → Multiset β
⊢ prod (bind 0 t) = prod (map (fun a => prod (t a)) 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α
s✝¹ t✝ : Multiset α
f g : α → Multiset β
inst✝ : CommMonoid β
s✝ : Multiset α
t : α → Multiset β
a : α
s : Multiset α
ih : prod (bind s t) = prod (map (fun a => prod (t a)) s)
⊢ prod (bind (a ::ₘ s) t) = prod (map (fun a => prod (t a)) (a ::ₘ s))
[PROOFSTEP]
simp [ih, cons_bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t✝ : Multiset α
f✝ g✝ : α → Multiset β
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel p (bind s f) (bind t g)
[PROOFSTEP]
apply rel_join
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t✝ : Multiset α
f✝ g✝ : α → Multiset β
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (Rel p) (map f s) (map g t)
[PROOFSTEP]
rw [rel_map]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
s✝ t✝ : Multiset α
f✝ g✝ : α → Multiset β
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (fun a b => Rel p (f a) (g b)) s t
[PROOFSTEP]
exact hst.mono fun a _ b _ hr => h hr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α
s t : Multiset α
f✝ g : α → Multiset β
inst✝ : DecidableEq α
m : Multiset β
f : β → Multiset α
a : α
⊢ count a (sum (map f 0)) = sum (map (fun b => count a (f b)) 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α
s t : Multiset α
f✝ g : α → Multiset β
inst✝ : DecidableEq α
m : Multiset β
f : β → Multiset α
a : α
⊢ ∀ ⦃a_1 : β⦄ {s : Multiset β},
    count a (sum (map f s)) = sum (map (fun b => count a (f b)) s) →
      count a (sum (map f (a_1 ::ₘ s))) = sum (map (fun b => count a (f b)) (a_1 ::ₘ s))
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
a : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_5
β : Type u_6
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ bind S f
[PROOFSTEP]
classical
rw [le_iff_count]
intro a
rw [count_bind]
apply le_sum_of_mem
rw [mem_map]
exact ⟨x, hx, rfl⟩
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
a : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_5
β : Type u_6
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ bind S f
[PROOFSTEP]
rw [le_iff_count]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
a : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_5
β : Type u_6
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ ∀ (a : β), count a (f x) ≤ count a (bind S f)
[PROOFSTEP]
intro a
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_5
β : Type u_6
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ≤ count a (bind S f)
[PROOFSTEP]
rw [count_bind]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_5
β : Type u_6
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ≤ sum (map (fun b => count a (f b)) S)
[PROOFSTEP]
apply le_sum_of_mem
[GOAL]
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_5
β : Type u_6
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ∈ map (fun b => count a (f b)) S
[PROOFSTEP]
rw [mem_map]
[GOAL]
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_5
β : Type u_6
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ ∃ a_1, a_1 ∈ S ∧ count a (f a_1) = count a (f x)
[PROOFSTEP]
exact ⟨x, hx, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
l₁ : List α
l₂ : List β
⊢ ↑l₁ ×ˢ ↑l₂ = ↑(l₁ ×ˢ l₂)
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
l₁ : List α
l₂ : List β
⊢ product ↑l₁ ↑l₂ = ↑(List.product l₁ l₂)
[PROOFSTEP]
rw [product, List.product, ← coe_bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
l₁ : List α
l₂ : List β
⊢ (bind ↑l₁ fun a => map (Prod.mk a) ↑l₂) = bind ↑l₁ fun a => ↑(List.map (Prod.mk a) l₂)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
⊢ (a ::ₘ s) ×ˢ t = map (Prod.mk a) t + s ×ˢ t
[PROOFSTEP]
simp [SProd.sprod, product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
⊢ s ×ˢ 0 = 0
[PROOFSTEP]
simp [SProd.sprod, product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
⊢ s ×ˢ (b ::ₘ t) = map (fun a => (a, b)) s + s ×ˢ t
[PROOFSTEP]
simp [SProd.sprod, product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
⊢ {a} ×ˢ {b} = {(a, b)}
[PROOFSTEP]
simp only [SProd.sprod, product, bind_singleton, map_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s✝ : Multiset α
t✝ : Multiset β
s t : Multiset α
u : Multiset β
⊢ (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u
[PROOFSTEP]
simp [SProd.sprod, product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α
b : β
s✝¹ : Multiset α
t✝ : Multiset β
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ (a ::ₘ s) ×ˢ (t + u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
[PROOFSTEP]
rw [cons_product, IH]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α
b : β
s✝¹ : Multiset α
t✝ : Multiset β
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ map (Prod.mk a) (t + u) + (s ×ˢ t + s ×ˢ u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
[PROOFSTEP]
simp [add_comm, add_left_comm, add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ : α
b✝ : β
s✝ : Multiset α
t✝ : Multiset β
s : Multiset α
t : Multiset β
a : α
b : β
⊢ (a, b) ∈ product s t ↔ (a, b).fst ∈ s ∧ (a, b).snd ∈ t
[PROOFSTEP]
simp [product, and_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
s : Multiset α
t : Multiset β
⊢ ↑card (s ×ˢ t) = ↑card s * ↑card t
[PROOFSTEP]
simp [SProd.sprod, product]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a : α
s : Multiset α
t : (a : α) → Multiset (σ a)
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ (Multiset.sigma ↑l₁ fun a => ↑(l₂ a)) = ↑(List.sigma l₁ l₂)
[PROOFSTEP]
rw [Multiset.sigma, List.sigma, ← coe_bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a : α
s : Multiset α
t : (a : α) → Multiset (σ a)
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ (bind ↑l₁ fun a => map (Sigma.mk a) ↑(l₂ a)) = bind ↑l₁ fun a => ↑(List.map (Sigma.mk a) (l₂ a))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a : α
s : Multiset α
t : (a : α) → Multiset (σ a)
⊢ Multiset.sigma (a ::ₘ s) t = map (Sigma.mk a) (t a) + Multiset.sigma s t
[PROOFSTEP]
simp [Multiset.sigma]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a : α
s✝ : Multiset α
t✝ : (a : α) → Multiset (σ a)
s t : Multiset α
u : (a : α) → Multiset (σ a)
⊢ Multiset.sigma (s + t) u = Multiset.sigma s u + Multiset.sigma t u
[PROOFSTEP]
simp [Multiset.sigma]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a✝ : α
s✝ : Multiset α
t✝ : (a : α) → Multiset (σ a)
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (Multiset.sigma s fun a => t a + u a) = Multiset.sigma s t + Multiset.sigma s u
t u : (a : α) → Multiset (σ a)
⊢ (Multiset.sigma (a ::ₘ s) fun a => t a + u a) = Multiset.sigma (a ::ₘ s) t + Multiset.sigma (a ::ₘ s) u
[PROOFSTEP]
rw [cons_sigma, IH]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a✝ : α
s✝ : Multiset α
t✝ : (a : α) → Multiset (σ a)
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (Multiset.sigma s fun a => t a + u a) = Multiset.sigma s t + Multiset.sigma s u
t u : (a : α) → Multiset (σ a)
⊢ map (Sigma.mk a) (t a + u a) + ((Multiset.sigma s fun a => t a) + Multiset.sigma s fun a => u a) =
    Multiset.sigma (a ::ₘ s) t + Multiset.sigma (a ::ₘ s) u
[PROOFSTEP]
simp [add_comm, add_left_comm, add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a✝ : α
s✝ : Multiset α
t✝ : (a : α) → Multiset (σ a)
s : Multiset α
t : (a : α) → Multiset (σ a)
a : α
b : σ a
⊢ { fst := a, snd := b } ∈ Multiset.sigma s t ↔
    { fst := a, snd := b }.fst ∈ s ∧ { fst := a, snd := b }.snd ∈ t { fst := a, snd := b }.fst
[PROOFSTEP]
simp [Multiset.sigma, and_assoc, and_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : α → Type u_5
a : α
s : Multiset α
t : (a : α) → Multiset (σ a)
⊢ ↑card (Multiset.sigma s t) = sum (map (fun a => ↑card (t a)) s)
[PROOFSTEP]
simp [Multiset.sigma, (· ∘ ·)]


[GOAL]
fuel : ℕ
n k : PosNum
h : Nat.sqrt ↑n < fuel + ↑(bit1 k)
⊢ ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
[PROOFSTEP]
induction' fuel with fuel ih generalizing k
[GOAL]
case zero
fuel : ℕ
n k✝ : PosNum
h✝ : Nat.sqrt ↑n < fuel + ↑(bit1 k✝)
k : PosNum
h : Nat.sqrt ↑n < Nat.zero + ↑(bit1 k)
⊢ ↑(minFacAux n Nat.zero k) = Nat.minFacAux ↑n ↑(bit1 k)
[PROOFSTEP]
rw [minFacAux, Nat.minFacAux]
[GOAL]
case succ
fuel✝ : ℕ
n k✝ : PosNum
h✝ : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
⊢ ↑(minFacAux n (Nat.succ fuel) k) = Nat.minFacAux ↑n ↑(bit1 k)
[PROOFSTEP]
rw [minFacAux, Nat.minFacAux]
[GOAL]
case zero
fuel : ℕ
n k✝ : PosNum
h✝ : Nat.sqrt ↑n < fuel + ↑(bit1 k✝)
k : PosNum
h : Nat.sqrt ↑n < Nat.zero + ↑(bit1 k)
⊢ ↑n =
    if h : ↑n < ↑(bit1 k) * ↑(bit1 k) then ↑n
    else
      if ↑(bit1 k) ∣ ↑n then ↑(bit1 k)
      else
        let_fun this := (_ : Nat.sqrt ↑n - ↑(bit1 k) < Nat.sqrt ↑n + 2 - ↑(bit1 k));
        Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
rw [Nat.zero_add, Nat.sqrt_lt] at h
[GOAL]
case zero
fuel : ℕ
n k✝ : PosNum
h✝ : Nat.sqrt ↑n < fuel + ↑(bit1 k✝)
k : PosNum
h : ↑n < ↑(bit1 k) * ↑(bit1 k)
⊢ ↑n =
    if h : ↑n < ↑(bit1 k) * ↑(bit1 k) then ↑n
    else
      if ↑(bit1 k) ∣ ↑n then ↑(bit1 k)
      else
        let_fun this := (_ : Nat.sqrt ↑n - ↑(bit1 k) < Nat.sqrt ↑n + 2 - ↑(bit1 k));
        Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
simp only [h, dite_true]
[GOAL]
case succ
fuel✝ : ℕ
n k✝ : PosNum
h✝ : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
⊢ ↑(if n < bit1 k * bit1 k then n else if bit1 k ∣ n then bit1 k else minFacAux n fuel (succ k)) =
    if h : ↑n < ↑(bit1 k) * ↑(bit1 k) then ↑n
    else
      if ↑(bit1 k) ∣ ↑n then ↑(bit1 k)
      else
        let_fun this := (_ : Nat.sqrt ↑n - ↑(bit1 k) < Nat.sqrt ↑n + 2 - ↑(bit1 k));
        Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
simp_rw [← mul_to_nat]
[GOAL]
case succ
fuel✝ : ℕ
n k✝ : PosNum
h✝ : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
⊢ ↑(if n < bit1 k * bit1 k then n else if bit1 k ∣ n then bit1 k else minFacAux n fuel (succ k)) =
    if h : ↑n < ↑(bit1 k * bit1 k) then ↑n else if ↑(bit1 k) ∣ ↑n then ↑(bit1 k) else Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
simp only [cast_lt, dvd_to_nat]
[GOAL]
case succ
fuel✝ : ℕ
n k✝ : PosNum
h✝ : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
⊢ ↑(if n < bit1 k * bit1 k then n else if bit1 k ∣ n then bit1 k else minFacAux n fuel (succ k)) =
    if h : n < bit1 k * bit1 k then ↑n else if bit1 k ∣ n then ↑(bit1 k) else Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
fuel✝ : ℕ
n k✝ : PosNum
h✝¹ : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝ : n < bit1 k * bit1 k
⊢ ↑n = ↑n
[PROOFSTEP]
try rfl
[GOAL]
case pos
fuel✝ : ℕ
n k✝ : PosNum
h✝¹ : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝ : n < bit1 k * bit1 k
⊢ ↑n = ↑n
[PROOFSTEP]
rfl
[GOAL]
case pos
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : bit1 k ∣ n
⊢ ↑(bit1 k) = ↑(bit1 k)
[PROOFSTEP]
try rfl
[GOAL]
case pos
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : bit1 k ∣ n
⊢ ↑(bit1 k) = ↑(bit1 k)
[PROOFSTEP]
rfl
[GOAL]
case neg
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ ↑(minFacAux n fuel (succ k)) = Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
try rfl
[GOAL]
case neg
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ ↑(minFacAux n fuel (succ k)) = Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
rfl
[GOAL]
case neg
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ ↑(minFacAux n fuel (succ k)) = Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
rw [ih] <;> [congr; convert Nat.lt_succ_of_lt h using 1]
[GOAL]
case neg
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ ↑(minFacAux n fuel (succ k)) = Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
rw [ih]
[GOAL]
case neg
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ Nat.minFacAux ↑n ↑(bit1 (succ k)) = Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
congr
[GOAL]
case neg
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ Nat.sqrt ↑n < fuel + ↑(bit1 (succ k))
[PROOFSTEP]
convert Nat.lt_succ_of_lt h using 1
[GOAL]
case neg.e_a
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ ↑(bit1 (succ k)) = ↑(bit1 k) + 2
[PROOFSTEP]
simp only [_root_.bit1, _root_.bit0, cast_bit1, cast_succ, Nat.succ_eq_add_one, add_assoc, add_left_comm, ←
  one_add_one_eq_two]
[GOAL]
case h.e'_4
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ fuel + ↑(bit1 (succ k)) = Nat.succ (Nat.succ fuel + ↑(bit1 k))
[PROOFSTEP]
simp only [_root_.bit1, _root_.bit0, cast_bit1, cast_succ, Nat.succ_eq_add_one, add_assoc, add_left_comm, ←
  one_add_one_eq_two]
[GOAL]
n : PosNum
⊢ ↑(minFac n) = Nat.minFac ↑n
[PROOFSTEP]
cases' n with n
[GOAL]
case one
⊢ ↑(minFac one) = Nat.minFac ↑one
[PROOFSTEP]
rfl
[GOAL]
case bit1
n : PosNum
⊢ ↑(minFac (bit1 n)) = Nat.minFac ↑(bit1 n)
[PROOFSTEP]
rw [minFac, Nat.minFac_eq, if_neg]
[GOAL]
case bit1
n : PosNum
⊢ ↑(match bit1 n with
      | one => 1
      | bit0 a => 2
      | bit1 n => minFacAux (bit1 n) (↑n) 1) =
    Nat.minFacAux (↑(bit1 n)) 3
case bit1.hnc n : PosNum ⊢ ¬2 ∣ ↑(bit1 n)
[PROOFSTEP]
swap
[GOAL]
case bit1.hnc
n : PosNum
⊢ ¬2 ∣ ↑(bit1 n)
[PROOFSTEP]
simp
[GOAL]
case bit1
n : PosNum
⊢ ↑(match bit1 n with
      | one => 1
      | bit0 a => 2
      | bit1 n => minFacAux (bit1 n) (↑n) 1) =
    Nat.minFacAux (↑(bit1 n)) 3
[PROOFSTEP]
rw [minFacAux_to_nat]
[GOAL]
case bit1
n : PosNum
⊢ Nat.minFacAux ↑(bit1 n) ↑(bit1 1) = Nat.minFacAux (↑(bit1 n)) 3
[PROOFSTEP]
rfl
[GOAL]
case bit1
n : PosNum
⊢ Nat.sqrt ↑(bit1 n) < ↑n + ↑(bit1 1)
[PROOFSTEP]
simp only [cast_one, cast_bit1]
[GOAL]
case bit1
n : PosNum
⊢ Nat.sqrt (_root_.bit1 ↑n) < ↑n + _root_.bit1 1
[PROOFSTEP]
unfold _root_.bit1 _root_.bit0
[GOAL]
case bit1
n : PosNum
⊢ Nat.sqrt (↑n + ↑n + 1) < ↑n + (1 + 1 + 1)
[PROOFSTEP]
rw [Nat.sqrt_lt]
[GOAL]
case bit1
n : PosNum
⊢ ↑n + ↑n + 1 < (↑n + (1 + 1 + 1)) * (↑n + (1 + 1 + 1))
[PROOFSTEP]
calc
  (n : ℕ) + (n : ℕ) + 1 ≤ (n : ℕ) + (n : ℕ) + (n : ℕ) := by simp
  _ = (n : ℕ) * (1 + 1 + 1) := by simp only [mul_add, mul_one]
  _ < _ := by simp [mul_lt_mul]
[GOAL]
n : PosNum
⊢ ↑n + ↑n + 1 ≤ ↑n + ↑n + ↑n
[PROOFSTEP]
simp
[GOAL]
n : PosNum
⊢ ↑n + ↑n + ↑n = ↑n * (1 + 1 + 1)
[PROOFSTEP]
simp only [mul_add, mul_one]
[GOAL]
n : PosNum
⊢ ↑n * (1 + 1 + 1) < (↑n + (1 + 1 + 1)) * (↑n + (1 + 1 + 1))
[PROOFSTEP]
simp [mul_lt_mul]
[GOAL]
case bit0
a✝ : PosNum
⊢ ↑(minFac (bit0 a✝)) = Nat.minFac ↑(bit0 a✝)
[PROOFSTEP]
rw [minFac, Nat.minFac_eq, if_pos]
[GOAL]
case bit0
a✝ : PosNum
⊢ ↑(match bit0 a✝ with
      | one => 1
      | bit0 a => 2
      | bit1 n => minFacAux (bit1 n) (↑n) 1) =
    2
[PROOFSTEP]
rfl
[GOAL]
case bit0.hc
a✝ : PosNum
⊢ 2 ∣ ↑(bit0 a✝)
[PROOFSTEP]
simp
[GOAL]
n : PosNum
⊢ Prime (bit0 n) ↔ n = 1
[PROOFSTEP]
refine' Nat.prime_def_minFac.trans ((and_iff_right _).trans <| eq_comm.trans _)
[GOAL]
case refine'_1
n : PosNum
⊢ 2 ≤ ↑(bit0 n)
[PROOFSTEP]
exact bit0_le_bit0.2 (Nat.succ_le_of_lt (to_nat_pos _))
[GOAL]
case refine'_2
n : PosNum
⊢ ↑(bit0 n) = Nat.minFac ↑(bit0 n) ↔ n = 1
[PROOFSTEP]
rw [← minFac_to_nat, to_nat_inj]
[GOAL]
case refine'_2
n : PosNum
⊢ bit0 n = minFac (bit0 n) ↔ n = 1
[PROOFSTEP]
exact ⟨bit0.inj, congr_arg _⟩
[GOAL]
n : PosNum
⊢ Prime (bit1 n) ↔ minFacAux (bit1 n) (↑n) 1 = bit1 n
[PROOFSTEP]
refine' Nat.prime_def_minFac.trans ((and_iff_right _).trans _)
[GOAL]
case refine'_1
n : PosNum
⊢ 2 ≤ ↑(bit1 n)
[PROOFSTEP]
exact Nat.bit0_le_bit1_iff.2 (to_nat_pos _)
[GOAL]
case refine'_2
n : PosNum
⊢ Nat.minFac ↑(bit1 n) = ↑(bit1 n) ↔ minFacAux (bit1 n) (↑n) 1 = bit1 n
[PROOFSTEP]
rw [← minFac_to_nat, to_nat_inj]
[GOAL]
case refine'_2
n : PosNum
⊢ minFac (bit1 n) = bit1 n ↔ minFacAux (bit1 n) (↑n) 1 = bit1 n
[PROOFSTEP]
rfl


[GOAL]
m k : ℕ
⊢ hyperoperation 0 m k = Nat.succ k
[PROOFSTEP]
rw [hyperoperation, Nat.succ_eq_add_one]
[GOAL]
n m : ℕ
⊢ hyperoperation (n + 3) m 0 = 1
[PROOFSTEP]
rw [hyperoperation]
[GOAL]
n m k : ℕ
⊢ hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k)
[PROOFSTEP]
rw [hyperoperation]
[GOAL]
⊢ hyperoperation 1 = fun x x_1 => x + x_1
[PROOFSTEP]
ext m k
[GOAL]
case h.h
m k : ℕ
⊢ hyperoperation 1 m k = m + k
[PROOFSTEP]
induction' k with bn bih
[GOAL]
case h.h.zero
m : ℕ
⊢ hyperoperation 1 m Nat.zero = m + Nat.zero
[PROOFSTEP]
rw [Nat.add_zero m, hyperoperation]
[GOAL]
case h.h.succ
m bn : ℕ
bih : hyperoperation 1 m bn = m + bn
⊢ hyperoperation 1 m (Nat.succ bn) = m + Nat.succ bn
[PROOFSTEP]
rw [hyperoperation_recursion, bih, hyperoperation_zero]
[GOAL]
case h.h.succ
m bn : ℕ
bih : hyperoperation 1 m bn = m + bn
⊢ Nat.succ (m + bn) = m + Nat.succ bn
[PROOFSTEP]
exact Nat.add_assoc m bn 1
[GOAL]
⊢ hyperoperation 2 = fun x x_1 => x * x_1
[PROOFSTEP]
ext m k
[GOAL]
case h.h
m k : ℕ
⊢ hyperoperation 2 m k = m * k
[PROOFSTEP]
induction' k with bn bih
[GOAL]
case h.h.zero
m : ℕ
⊢ hyperoperation 2 m Nat.zero = m * Nat.zero
[PROOFSTEP]
rw [hyperoperation]
[GOAL]
case h.h.zero
m : ℕ
⊢ 0 = m * Nat.zero
[PROOFSTEP]
exact (Nat.mul_zero m).symm
[GOAL]
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ hyperoperation 2 m (Nat.succ bn) = m * Nat.succ bn
[PROOFSTEP]
rw [hyperoperation_recursion, hyperoperation_one, bih]
  -- porting note: was `ring`
[GOAL]
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ (fun x x_1 => x + x_1) m (m * bn) = m * Nat.succ bn
[PROOFSTEP]
dsimp only
[GOAL]
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ m + m * bn = m * Nat.succ bn
[PROOFSTEP]
nth_rewrite 1 [← mul_one m]
[GOAL]
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ m * 1 + m * bn = m * Nat.succ bn
[PROOFSTEP]
rw [← mul_add, add_comm, Nat.succ_eq_add_one]
[GOAL]
⊢ hyperoperation 3 = fun x x_1 => x ^ x_1
[PROOFSTEP]
ext m k
[GOAL]
case h.h
m k : ℕ
⊢ hyperoperation 3 m k = m ^ k
[PROOFSTEP]
induction' k with bn bih
[GOAL]
case h.h.zero
m : ℕ
⊢ hyperoperation 3 m Nat.zero = m ^ Nat.zero
[PROOFSTEP]
rw [hyperoperation_ge_three_eq_one]
[GOAL]
case h.h.zero
m : ℕ
⊢ 1 = m ^ Nat.zero
[PROOFSTEP]
exact (pow_zero m).symm
[GOAL]
case h.h.succ
m bn : ℕ
bih : hyperoperation 3 m bn = m ^ bn
⊢ hyperoperation 3 m (Nat.succ bn) = m ^ Nat.succ bn
[PROOFSTEP]
rw [hyperoperation_recursion, hyperoperation_two, bih]
[GOAL]
case h.h.succ
m bn : ℕ
bih : hyperoperation 3 m bn = m ^ bn
⊢ (fun x x_1 => x * x_1) m (m ^ bn) = m ^ Nat.succ bn
[PROOFSTEP]
exact (pow_succ m bn).symm
[GOAL]
n m : ℕ
⊢ hyperoperation (n + 2) m 1 = m
[PROOFSTEP]
induction' n with nn nih
[GOAL]
case zero
m : ℕ
⊢ hyperoperation (Nat.zero + 2) m 1 = m
[PROOFSTEP]
rw [hyperoperation_two]
[GOAL]
case zero
m : ℕ
⊢ (fun x x_1 => x * x_1) m 1 = m
[PROOFSTEP]
ring
[GOAL]
case succ
m nn : ℕ
nih : hyperoperation (nn + 2) m 1 = m
⊢ hyperoperation (Nat.succ nn + 2) m 1 = m
[PROOFSTEP]
rw [hyperoperation_recursion, hyperoperation_ge_three_eq_one, nih]
[GOAL]
n : ℕ
⊢ hyperoperation (n + 1) 2 2 = 4
[PROOFSTEP]
induction' n with nn nih
[GOAL]
case zero
⊢ hyperoperation (Nat.zero + 1) 2 2 = 4
[PROOFSTEP]
rw [hyperoperation_one]
[GOAL]
case succ
nn : ℕ
nih : hyperoperation (nn + 1) 2 2 = 4
⊢ hyperoperation (Nat.succ nn + 1) 2 2 = 4
[PROOFSTEP]
rw [hyperoperation_recursion, hyperoperation_ge_two_eq_self, nih]
[GOAL]
n : ℕ
⊢ ∀ (k : ℕ), hyperoperation (n + 3) 1 k = 1
[PROOFSTEP]
induction' n with nn nih
[GOAL]
case zero
⊢ ∀ (k : ℕ), hyperoperation (Nat.zero + 3) 1 k = 1
[PROOFSTEP]
intro k
[GOAL]
case zero
k : ℕ
⊢ hyperoperation (Nat.zero + 3) 1 k = 1
[PROOFSTEP]
rw [hyperoperation_three]
[GOAL]
case zero
k : ℕ
⊢ (fun x x_1 => x ^ x_1) 1 k = 1
[PROOFSTEP]
dsimp
[GOAL]
case zero
k : ℕ
⊢ 1 ^ k = 1
[PROOFSTEP]
rw [one_pow]
[GOAL]
case succ
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
⊢ ∀ (k : ℕ), hyperoperation (Nat.succ nn + 3) 1 k = 1
[PROOFSTEP]
intro k
[GOAL]
case succ
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
k : ℕ
⊢ hyperoperation (Nat.succ nn + 3) 1 k = 1
[PROOFSTEP]
cases k
[GOAL]
case succ.zero
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
⊢ hyperoperation (Nat.succ nn + 3) 1 Nat.zero = 1
[PROOFSTEP]
rw [hyperoperation_ge_three_eq_one]
[GOAL]
case succ.succ
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
n✝ : ℕ
⊢ hyperoperation (Nat.succ nn + 3) 1 (Nat.succ n✝) = 1
[PROOFSTEP]
rw [hyperoperation_recursion, nih]
[GOAL]
n k : ℕ
⊢ hyperoperation (n + 4) 0 k = if Even k then 1 else 0
[PROOFSTEP]
induction' k with kk kih
[GOAL]
case zero
n : ℕ
⊢ hyperoperation (n + 4) 0 Nat.zero = if Even Nat.zero then 1 else 0
[PROOFSTEP]
rw [hyperoperation_ge_three_eq_one]
[GOAL]
case zero
n : ℕ
⊢ 1 = if Even Nat.zero then 1 else 0
[PROOFSTEP]
simp only [even_zero, if_true]
[GOAL]
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 4) 0 (Nat.succ kk) = if Even (Nat.succ kk) then 1 else 0
[PROOFSTEP]
rw [hyperoperation_recursion]
[GOAL]
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (hyperoperation (n + 3 + 1) 0 kk) = if Even (Nat.succ kk) then 1 else 0
[PROOFSTEP]
rw [kih]
[GOAL]
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (if Even kk then 1 else 0) = if Even (Nat.succ kk) then 1 else 0
[PROOFSTEP]
simp_rw [Nat.even_add_one]
[GOAL]
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (if Even kk then 1 else 0) = if ¬Even kk then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
h✝ : Even kk
⊢ hyperoperation (n + 3) 0 1 = 0
[PROOFSTEP]
exact hyperoperation_ge_two_eq_self (n + 1) 0
[GOAL]
case neg
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
h✝ : ¬Even kk
⊢ hyperoperation (n + 3) 0 0 = 1
[PROOFSTEP]
exact hyperoperation_ge_three_eq_one n 0