[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
⊢ prod (a :: l) = foldl (fun x x_1 => x * x_1) (a * 1) l
[PROOFSTEP]
simp only [List.prod, foldl_cons, one_mul, mul_one]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
⊢ prod (l₁ ++ l₂) = foldl (fun x x_1 => x * x_1) (foldl (fun x x_1 => x * x_1) 1 l₁ * 1) l₂
[PROOFSTEP]
simp [List.prod]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
⊢ prod (concat l a) = prod l * a
[PROOFSTEP]
rw [concat_eq_append, prod_append, prod_singleton]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List (List M)
⊢ prod (join l) = prod (map prod l)
[PROOFSTEP]
induction l <;> [rfl; simp only [*, List.join, map, prod_append, prod_cons]]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List (List M)
⊢ prod (join l) = prod (map prod l)
[PROOFSTEP]
induction l
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
⊢ prod (join []) = prod (map prod [])
[PROOFSTEP]
rfl
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
head✝ : List M
tail✝ : List (List M)
tail_ih✝ : prod (join tail✝) = prod (map prod tail✝)
⊢ prod (join (head✝ :: tail✝)) = prod (map prod (head✝ :: tail✝))
[PROOFSTEP]
simp only [*, List.join, map, prod_append, prod_cons]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a✝ a : M
l : List M
⊢ prod (a :: l) = foldr (fun x x_1 => x * x_1) 1 (a :: l)
[PROOFSTEP]
rw [prod_cons, foldr_cons, prod_eq_foldr]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ : M
n : ℕ
a : M
⊢ prod (replicate n a) = a ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ a : M
⊢ prod (replicate Nat.zero a) = a ^ Nat.zero
[PROOFSTEP]
rw [pow_zero]
[GOAL]
case zero
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ a : M
⊢ prod (replicate Nat.zero a) = 1
[PROOFSTEP]
rfl
[GOAL]
case succ
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ a : M
n : ℕ
ih : prod (replicate n a) = a ^ n
⊢ prod (replicate (Nat.succ n) a) = a ^ Nat.succ n
[PROOFSTEP]
rw [replicate_succ, prod_cons, ih, pow_succ]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List M
m : M
h : ∀ (x : M), x ∈ l → x = m
⊢ prod l = m ^ length l
[PROOFSTEP]
rw [← prod_replicate, ← List.eq_replicate.mpr ⟨rfl, h⟩]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝¹ l₁ l₂ : List M
a✝ : M
l✝ : List ι
r : M → N → Prop
f : ι → M
g : ι → N
h₁ : r 1 1
h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i * a) (g i * b)
a : ι
l : List ι
hl : r (prod (map f l)) (prod (map g l))
⊢ r (prod (map f (a :: l))) (prod (map g (a :: l)))
[PROOFSTEP]
simp only [map_cons, prod_cons, h₂ hl]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List M
F : Type u_9
inst✝ : MonoidHomClass F M N
f : F
⊢ prod (map (↑f) l) = ↑f (prod l)
[PROOFSTEP]
simp only [prod, foldl_map, ← map_one f]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List M
F : Type u_9
inst✝ : MonoidHomClass F M N
f : F
⊢ foldl (fun x y => x * ↑f y) (↑f 1) l = ↑f (foldl (fun x x_1 => x * x_1) 1 l)
[PROOFSTEP]
exact l.foldl_hom f (· * ·) (· * f ·) 1 (fun x y => (map_mul f x y).symm)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ prod (map (fun i => f (f₁ i) (f₂ i)) l) = f (prod (map f₁ l)) (prod (map f₂ l))
[PROOFSTEP]
simp only [prod, foldl_map]
  -- Porting note: next 3 lines used to be
    -- convert l.foldl_hom₂ (fun a b => f a b) _ _ _ _ _ fun a b i => _
    -- · exact hf'.symm
    -- · exact hf _ _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ foldl (fun x y => x * f (f₁ y) (f₂ y)) 1 l = f (foldl (fun x y => x * f₁ y) 1 l) (foldl (fun x y => x * f₂ y) 1 l)
[PROOFSTEP]
rw [← l.foldl_hom₂ (fun a b => f a b), hf']
[GOAL]
case h
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ ∀ (a : M) (b : N) (i : ι), f (a * f₁ i) (b * f₂ i) = f a b * f (f₁ i) (f₂ i)
[PROOFSTEP]
intros
[GOAL]
case h
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
a✝ : M
b✝ : N
i✝ : ι
⊢ f (a✝ * f₁ i✝) (b✝ * f₂ i✝) = f a✝ b✝ * f (f₁ i✝) (f₂ i✝)
[PROOFSTEP]
exact hf _ _ _ _
[GOAL]
ι : Type u_1
α✝ : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : Monoid P
l✝ l₁ l₂ : List M
a : M
α : Type u_9
inst✝¹ : CommMonoid α
inst✝ : HasDistribNeg α
l : List α
⊢ prod (map Neg.neg l) = (-1) ^ length l * prod l
[PROOFSTEP]
simpa only [id_eq, neg_mul, one_mul, map_const', prod_replicate, map_id] using @prod_map_mul α α _ l (fun _ => -1) id
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G✝ : Type u_7
R : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
L : List ι
f : ι → M
G : Type u_9
inst✝ : MonoidHomClass G M N
g : G
⊢ prod (map (↑g ∘ f) L) = ↑g (prod (map f L))
[PROOFSTEP]
rw [← prod_hom, map_map]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
x✝ : ∀ (m : M), m ∈ [] → IsUnit m
⊢ IsUnit (prod [])
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
u : ∀ (m : M), m ∈ h :: t → IsUnit m
⊢ IsUnit (prod (h :: t))
[PROOFSTEP]
simp only [List.prod_cons]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
u : ∀ (m : M), m ∈ h :: t → IsUnit m
⊢ IsUnit (h * prod t)
[PROOFSTEP]
exact IsUnit.mul (u h (mem_cons_self h t)) (prod_isUnit fun m mt => u m (mem_cons_of_mem h mt))
[GOAL]
ι : Type u_1
α✝ : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
α : Type u_9
inst✝ : CommMonoid α
L : List α
⊢ IsUnit (prod L) ↔ ∀ (m : α), m ∈ L → IsUnit m
[PROOFSTEP]
refine' ⟨fun h => _, prod_isUnit⟩
[GOAL]
ι : Type u_1
α✝ : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
α : Type u_9
inst✝ : CommMonoid α
L : List α
h : IsUnit (prod L)
⊢ ∀ (m : α), m ∈ L → IsUnit m
[PROOFSTEP]
induction' L with m L ih
[GOAL]
case nil
ι : Type u_1
α✝ : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
α : Type u_9
inst✝ : CommMonoid α
L : List α
h✝ : IsUnit (prod L)
h : IsUnit (prod [])
⊢ ∀ (m : α), m ∈ [] → IsUnit m
[PROOFSTEP]
exact fun m' h' => False.elim (not_mem_nil m' h')
[GOAL]
case cons
ι : Type u_1
α✝ : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
α : Type u_9
inst✝ : CommMonoid α
L✝ : List α
h✝ : IsUnit (prod L✝)
m : α
L : List α
ih : IsUnit (prod L) → ∀ (m : α), m ∈ L → IsUnit m
h : IsUnit (prod (m :: L))
⊢ ∀ (m_1 : α), m_1 ∈ m :: L → IsUnit m_1
[PROOFSTEP]
rw [prod_cons, IsUnit.mul_iff] at h
[GOAL]
case cons
ι : Type u_1
α✝ : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
α : Type u_9
inst✝ : CommMonoid α
L✝ : List α
h✝ : IsUnit (prod L✝)
m : α
L : List α
ih : IsUnit (prod L) → ∀ (m : α), m ∈ L → IsUnit m
h : IsUnit m ∧ IsUnit (prod L)
⊢ ∀ (m_1 : α), m_1 ∈ m :: L → IsUnit m_1
[PROOFSTEP]
exact fun m' h' => Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
i : ℕ
⊢ prod (take i []) * prod (drop i []) = prod []
[PROOFSTEP]
simp [Nat.zero_le]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
L : List M
⊢ prod (take 0 L) * prod (drop 0 L) = prod L
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
n : ℕ
⊢ prod (take (n + 1) (h :: t)) * prod (drop (n + 1) (h :: t)) = prod (h :: t)
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
n : ℕ
⊢ prod (h :: take n t) * prod (drop n t) = prod (h :: t)
[PROOFSTEP]
rw [prod_cons, prod_cons, mul_assoc, prod_take_mul_prod_drop t]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
i : ℕ
p : i < length []
⊢ prod (take (i + 1) []) = prod (take i []) * nthLe [] i p
[PROOFSTEP]
cases p
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
n : ℕ
p : n + 1 < length (h :: t)
⊢ prod (take (n + 1 + 1) (h :: t)) = prod (take (n + 1) (h :: t)) * nthLe (h :: t) (n + 1) p
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
n : ℕ
p : n + 1 < length (h :: t)
⊢ prod (h :: take (n + 1) t) = prod (h :: take n t) * nthLe (h :: t) (n + 1) p
[PROOFSTEP]
rw [prod_cons, prod_cons, prod_take_succ t n (Nat.lt_of_succ_lt_succ p), mul_assoc, nthLe_cons,
  dif_neg (Nat.add_one_ne_zero _)]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
n : ℕ
p : n + 1 < length (h :: t)
⊢ h * (prod (take n t) * nthLe t n (_ : n < length t)) =
    h * (prod (take n t) * nthLe t (n + 1 - 1) (_ : n + 1 - 1 < length t))
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
L : List M
h : prod L ≠ 1
⊢ 0 < length L
[PROOFSTEP]
cases L
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
h : prod [] ≠ 1
⊢ 0 < length []
[PROOFSTEP]
contrapose h
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
h : ¬0 < length []
⊢ ¬prod [] ≠ 1
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a head✝ : M
tail✝ : List M
h : prod (head✝ :: tail✝) ≠ 1
⊢ 0 < length (head✝ :: tail✝)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ x : M
xs : List M
a : M
⊢ prod (set (x :: xs) 0 a) =
    (prod (take 0 (x :: xs)) * if 0 < length (x :: xs) then a else 1) * prod (drop (0 + 1) (x :: xs))
[PROOFSTEP]
simp [set]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ x : M
xs : List M
i : ℕ
a : M
⊢ prod (set (x :: xs) (i + 1) a) =
    (prod (take (i + 1) (x :: xs)) * if i + 1 < length (x :: xs) then a else 1) * prod (drop (i + 1 + 1) (x :: xs))
[PROOFSTEP]
simp [set, prod_set xs i a, mul_assoc, Nat.succ_eq_add_one]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
x✝¹ : ℕ
x✝ : M
⊢ prod (set [] x✝¹ x✝) = (prod (take x✝¹ []) * if x✝¹ < length [] then x✝ else 1) * prod (drop (x✝¹ + 1) [])
[PROOFSTEP]
simp [set, (Nat.zero_le _).not_lt, Nat.zero_le]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List M
⊢ Option.getD (get? l 0) 1 * prod (tail l) = prod l
[PROOFSTEP]
cases l
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
⊢ Option.getD (get? [] 0) 1 * prod (tail []) = prod []
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a head✝ : M
tail✝ : List M
⊢ Option.getD (get? (head✝ :: tail✝) 0) 1 * prod (tail (head✝ :: tail✝)) = prod (head✝ :: tail✝)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝ : Inhabited M
l : List M
h : l ≠ []
⊢ headI l * prod (tail l) = prod l
[PROOFSTEP]
cases l <;> [contradiction; simp]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝ : Inhabited M
l : List M
h : l ≠ []
⊢ headI l * prod (tail l) = prod l
[PROOFSTEP]
cases l
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
inst✝ : Inhabited M
h : [] ≠ []
⊢ headI [] * prod (tail []) = prod []
[PROOFSTEP]
contradiction
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
inst✝ : Inhabited M
head✝ : M
tail✝ : List M
h : head✝ :: tail✝ ≠ []
⊢ headI (head✝ :: tail✝) * prod (tail (head✝ :: tail✝)) = prod (head✝ :: tail✝)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List M
y : M
h : ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (prod l)
[PROOFSTEP]
induction' l with z l IH
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List M
y : M
h✝ : ∀ (x : M), x ∈ l → Commute y x
h : ∀ (x : M), x ∈ [] → Commute y x
⊢ Commute y (prod [])
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝¹ l₁ l₂ : List M
a : M
l✝ : List M
y : M
h✝ : ∀ (x : M), x ∈ l✝ → Commute y x
z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y (prod l)
h : ∀ (x : M), x ∈ z :: l → Commute y x
⊢ Commute y (prod (z :: l))
[PROOFSTEP]
rw [List.forall_mem_cons] at h
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝¹ l₁ l₂ : List M
a : M
l✝ : List M
y : M
h✝ : ∀ (x : M), x ∈ l✝ → Commute y x
z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y (prod l)
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (prod (z :: l))
[PROOFSTEP]
rw [List.prod_cons]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝¹ l₁ l₂ : List M
a : M
l✝ : List M
y : M
h✝ : ∀ (x : M), x ∈ l✝ → Commute y x
z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y (prod l)
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z * prod l)
[PROOFSTEP]
exact Commute.mul_right h.1 (IH h.2)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝ l₂✝ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ : List M
h : Forall₂ (fun x x_1 => x ≤ x_1) l₁ l₂
⊢ prod l₁ ≤ prod l₂
[PROOFSTEP]
induction' h with a b la lb hab ih ih'
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝ l₂✝ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ : List M
⊢ prod [] ≤ prod []
[PROOFSTEP]
rfl
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝ l₂✝ : List M
a✝ : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ : List M
a b : M
la lb : List M
hab : a ≤ b
ih : Forall₂ (fun x x_1 => x ≤ x_1) la lb
ih' : prod la ≤ prod lb
⊢ prod (a :: la) ≤ prod (b :: lb)
[PROOFSTEP]
simpa only [prod_cons] using mul_le_mul' hab ih'
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝ l₂✝ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ : List M
h : l₁ <+ l₂
h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a
⊢ prod l₁ ≤ prod l₂
[PROOFSTEP]
induction h
[GOAL]
case slnil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝ l₂✝ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ : List M
h₁ : ∀ (a : M), a ∈ [] → 1 ≤ a
⊢ prod [] ≤ prod []
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝¹ l₂✝¹ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod l₁✝ ≤ prod (a✝¹ :: l₂✝)
case cons₂
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝¹ l₂✝¹ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod (a✝¹ :: l₁✝) ≤ prod (a✝¹ :: l₂✝)
[PROOFSTEP]
case slnil => rfl
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝ l₂✝ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ : List M
h₁ : ∀ (a : M), a ∈ [] → 1 ≤ a
⊢ prod [] ≤ prod []
[PROOFSTEP]
case slnil => rfl
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝ l₂✝ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ : List M
h₁ : ∀ (a : M), a ∈ [] → 1 ≤ a
⊢ prod [] ≤ prod []
[PROOFSTEP]
rfl
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝¹ l₂✝¹ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod l₁✝ ≤ prod (a✝¹ :: l₂✝)
case cons₂
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝¹ l₂✝¹ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod (a✝¹ :: l₁✝) ≤ prod (a✝¹ :: l₂✝)
[PROOFSTEP]
case cons l₁ l₂ a _ ih' =>
  simp only [prod_cons, forall_mem_cons] at h₁ ⊢
  exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝¹ l₂✝¹ : List M
a✝¹ : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁✝ l₂✝ l₁ l₂ : List M
a : M
a✝ : l₁ <+ l₂
ih' : (∀ (a : M), a ∈ l₂ → 1 ≤ a) → prod l₁ ≤ prod l₂
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂ → 1 ≤ a_1
⊢ prod l₁ ≤ prod (a :: l₂)
[PROOFSTEP]
case cons l₁ l₂ a _ ih' =>
  simp only [prod_cons, forall_mem_cons] at h₁ ⊢
  exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝¹ l₂✝¹ : List M
a✝¹ : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁✝ l₂✝ l₁ l₂ : List M
a : M
a✝ : l₁ <+ l₂
ih' : (∀ (a : M), a ∈ l₂ → 1 ≤ a) → prod l₁ ≤ prod l₂
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂ → 1 ≤ a_1
⊢ prod l₁ ≤ prod (a :: l₂)
[PROOFSTEP]
simp only [prod_cons, forall_mem_cons] at h₁ ⊢
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝¹ l₂✝¹ : List M
a✝¹ : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁✝ l₂✝ l₁ l₂ : List M
a : M
a✝ : l₁ <+ l₂
ih' : (∀ (a : M), a ∈ l₂ → 1 ≤ a) → prod l₁ ≤ prod l₂
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂ → 1 ≤ x
⊢ prod l₁ ≤ a * prod l₂
[PROOFSTEP]
exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
[GOAL]
case cons₂
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝¹ l₂✝¹ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod (a✝¹ :: l₁✝) ≤ prod (a✝¹ :: l₂✝)
[PROOFSTEP]
case cons₂ l₁ l₂ a _ ih' =>
  simp only [prod_cons, forall_mem_cons] at h₁ ⊢
  exact mul_le_mul_left' (ih' h₁.2) _
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝¹ l₂✝¹ : List M
a✝¹ : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁✝ l₂✝ l₁ l₂ : List M
a : M
a✝ : l₁ <+ l₂
ih' : (∀ (a : M), a ∈ l₂ → 1 ≤ a) → prod l₁ ≤ prod l₂
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂ → 1 ≤ a_1
⊢ prod (a :: l₁) ≤ prod (a :: l₂)
[PROOFSTEP]
case cons₂ l₁ l₂ a _ ih' =>
  simp only [prod_cons, forall_mem_cons] at h₁ ⊢
  exact mul_le_mul_left' (ih' h₁.2) _
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝¹ l₂✝¹ : List M
a✝¹ : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁✝ l₂✝ l₁ l₂ : List M
a : M
a✝ : l₁ <+ l₂
ih' : (∀ (a : M), a ∈ l₂ → 1 ≤ a) → prod l₁ ≤ prod l₂
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂ → 1 ≤ a_1
⊢ prod (a :: l₁) ≤ prod (a :: l₂)
[PROOFSTEP]
simp only [prod_cons, forall_mem_cons] at h₁ ⊢
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝¹ l₂✝¹ : List M
a✝¹ : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁✝ l₂✝ l₁ l₂ : List M
a : M
a✝ : l₁ <+ l₂
ih' : (∀ (a : M), a ∈ l₂ → 1 ≤ a) → prod l₁ ≤ prod l₂
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂ → 1 ≤ x
⊢ a * prod l₁ ≤ a * prod l₂
[PROOFSTEP]
exact mul_le_mul_left' (ih' h₁.2) _
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List ι
f g : ι → M
h : ∀ (i : ι), i ∈ l → f i ≤ g i
⊢ Forall₂ (fun x x_1 => x ≤ x_1) (map f l) (map g l)
[PROOFSTEP]
simpa
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁷ : Monoid M
inst✝⁶ : Monoid N
inst✝⁵ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝⁴ : Preorder M
inst✝³ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝² : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List ι
f g : ι → M
h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i
h₂ : ∃ i, i ∈ l ∧ f i < g i
⊢ prod (map f l) < prod (map g l)
[PROOFSTEP]
induction' l with i l ihl
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁷ : Monoid M
inst✝⁶ : Monoid N
inst✝⁵ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝⁴ : Preorder M
inst✝³ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝² : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List ι
f g : ι → M
h₁✝ : ∀ (i : ι), i ∈ l → f i ≤ g i
h₂✝ : ∃ i, i ∈ l ∧ f i < g i
h₁ : ∀ (i : ι), i ∈ [] → f i ≤ g i
h₂ : ∃ i, i ∈ [] ∧ f i < g i
⊢ prod (map f []) < prod (map g [])
[PROOFSTEP]
rcases h₂ with ⟨_, ⟨⟩, _⟩
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁷ : Monoid M
inst✝⁶ : Monoid N
inst✝⁵ : Monoid P
l✝¹ l₁ l₂ : List M
a : M
inst✝⁴ : Preorder M
inst✝³ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝² : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l✝ : List ι
f g : ι → M
h₁✝ : ∀ (i : ι), i ∈ l✝ → f i ≤ g i
h₂✝ : ∃ i, i ∈ l✝ ∧ f i < g i
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → prod (map f l) < prod (map g l)
h₁ : ∀ (i_1 : ι), i_1 ∈ i :: l → f i_1 ≤ g i_1
h₂ : ∃ i_1, i_1 ∈ i :: l ∧ f i_1 < g i_1
⊢ prod (map f (i :: l)) < prod (map g (i :: l))
[PROOFSTEP]
simp only [forall_mem_cons, exists_mem_cons, map_cons, prod_cons] at h₁ h₂ ⊢
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁷ : Monoid M
inst✝⁶ : Monoid N
inst✝⁵ : Monoid P
l✝¹ l₁ l₂ : List M
a : M
inst✝⁴ : Preorder M
inst✝³ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝² : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l✝ : List ι
f g : ι → M
h₁✝ : ∀ (i : ι), i ∈ l✝ → f i ≤ g i
h₂✝ : ∃ i, i ∈ l✝ ∧ f i < g i
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → prod (map f l) < prod (map g l)
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h₂ : f i < g i ∨ ∃ x, x ∈ l ∧ f x < g x
⊢ f i * prod (map f l) < g i * prod (map g l)
[PROOFSTEP]
cases h₂
[GOAL]
case cons.inl
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁷ : Monoid M
inst✝⁶ : Monoid N
inst✝⁵ : Monoid P
l✝¹ l₁ l₂ : List M
a : M
inst✝⁴ : Preorder M
inst✝³ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝² : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l✝ : List ι
f g : ι → M
h₁✝ : ∀ (i : ι), i ∈ l✝ → f i ≤ g i
h₂ : ∃ i, i ∈ l✝ ∧ f i < g i
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → prod (map f l) < prod (map g l)
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h✝ : f i < g i
⊢ f i * prod (map f l) < g i * prod (map g l)
[PROOFSTEP]
exact mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod' h₁.2)
[GOAL]
case cons.inr
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁷ : Monoid M
inst✝⁶ : Monoid N
inst✝⁵ : Monoid P
l✝¹ l₁ l₂ : List M
a : M
inst✝⁴ : Preorder M
inst✝³ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝² : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l✝ : List ι
f g : ι → M
h₁✝ : ∀ (i : ι), i ∈ l✝ → f i ≤ g i
h₂ : ∃ i, i ∈ l✝ ∧ f i < g i
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → prod (map f l) < prod (map g l)
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h✝ : ∃ x, x ∈ l ∧ f x < g x
⊢ f i * prod (map f l) < g i * prod (map g l)
[PROOFSTEP]
exact mul_lt_mul_of_le_of_lt h₁.1 <| ihl h₁.2 ‹_›
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List M
n : M
h : ∀ (x : M), x ∈ l → x ≤ n
⊢ prod l ≤ n ^ length l
[PROOFSTEP]
simpa only [map_id'', map_const', prod_replicate] using prod_le_prod' h
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝² : LinearOrder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List ι
f g : ι → M
h : prod (map f l) < prod (map g l)
⊢ ∃ i, i ∈ l ∧ f i < g i
[PROOFSTEP]
contrapose! h
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝² : LinearOrder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List ι
f g : ι → M
h : ∀ (i : ι), i ∈ l → g i ≤ f i
⊢ prod (map g l) ≤ prod (map f l)
[PROOFSTEP]
exact prod_le_prod' h
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁷ : Monoid M
inst✝⁶ : Monoid N
inst✝⁵ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝⁴ : LinearOrder M
inst✝³ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝² : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List ι
hl : l ≠ []
f g : ι → M
h : prod (map f l) ≤ prod (map g l)
⊢ ∃ x, x ∈ l ∧ f x ≤ g x
[PROOFSTEP]
contrapose! h
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁷ : Monoid M
inst✝⁶ : Monoid N
inst✝⁵ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝⁴ : LinearOrder M
inst✝³ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝² : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List ι
hl : l ≠ []
f g : ι → M
h : ∀ (x : ι), x ∈ l → g x < f x
⊢ prod (map g l) < prod (map f l)
[PROOFSTEP]
exact prod_lt_prod_of_ne_nil hl _ _ h
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List M
hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x
⊢ 1 ≤ prod l
[PROOFSTEP]
induction' l with hd tl ih
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List M
hl₁✝ : ∀ (x : M), x ∈ l → 1 ≤ x
hl₁ : ∀ (x : M), x ∈ [] → 1 ≤ x
⊢ 1 ≤ prod []
[PROOFSTEP]
rfl
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List M
hl₁✝ : ∀ (x : M), x ∈ l → 1 ≤ x
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ prod tl
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ prod (hd :: tl)
[PROOFSTEP]
rw [prod_cons]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List M
hl₁✝ : ∀ (x : M), x ∈ l → 1 ≤ x
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ prod tl
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ hd * prod tl
[PROOFSTEP]
exact one_le_mul (hl₁ hd (mem_cons_self hd tl)) (ih fun x h => hl₁ x (mem_cons_of_mem hd h))
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : MonoidWithZero M₀
L : List M₀
h : 0 ∈ L
⊢ prod L = 0
[PROOFSTEP]
induction' L with a L ihL
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : MonoidWithZero M₀
L : List M₀
h✝ : 0 ∈ L
h : 0 ∈ []
⊢ prod [] = 0
[PROOFSTEP]
exact absurd h (not_mem_nil _)
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : MonoidWithZero M₀
L✝ : List M₀
h✝ : 0 ∈ L✝
a : M₀
L : List M₀
ihL : 0 ∈ L → prod L = 0
h : 0 ∈ a :: L
⊢ prod (a :: L) = 0
[PROOFSTEP]
rw [prod_cons]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : MonoidWithZero M₀
L✝ : List M₀
h✝ : 0 ∈ L✝
a : M₀
L : List M₀
ihL : 0 ∈ L → prod L = 0
h : 0 ∈ a :: L
⊢ a * prod L = 0
[PROOFSTEP]
cases' mem_cons.1 h with ha hL
[GOAL]
case cons.inl
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : MonoidWithZero M₀
L✝ : List M₀
h✝ : 0 ∈ L✝
a : M₀
L : List M₀
ihL : 0 ∈ L → prod L = 0
h : 0 ∈ a :: L
ha : 0 = a
⊢ a * prod L = 0
case cons.inr
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : MonoidWithZero M₀
L✝ : List M₀
h✝ : 0 ∈ L✝
a : M₀
L : List M₀
ihL : 0 ∈ L → prod L = 0
h : 0 ∈ a :: L
hL : 0 ∈ L
⊢ a * prod L = 0
[PROOFSTEP]
exacts [mul_eq_zero_of_left ha.symm _, mul_eq_zero_of_right _ (ihL hL)]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
L : List M₀
⊢ prod L = 0 ↔ 0 ∈ L
[PROOFSTEP]
induction' L with a L ihL
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ prod [] = 0 ↔ 0 ∈ []
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a : M₀
L : List M₀
ihL : prod L = 0 ↔ 0 ∈ L
⊢ prod (a :: L) = 0 ↔ 0 ∈ a :: L
[PROOFSTEP]
rw [prod_cons, mul_eq_zero, ihL, mem_cons, eq_comm]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Group G
⊢ (prod [])⁻¹ = prod (reverse (map (fun x => x⁻¹) []))
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Group G
x : G
xs : List G
⊢ (prod (x :: xs))⁻¹ = prod (reverse (map (fun x => x⁻¹) (x :: xs)))
[PROOFSTEP]
simp [prod_inv_reverse xs]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Group G
⊢ ∀ (L : List G), prod (reverse L) = (prod (map (fun x => x⁻¹) L))⁻¹
[PROOFSTEP]
simp [prod_inv_reverse]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Group G
x : G
xs : List G
x✝ : 0 < length (x :: xs)
⊢ prod (drop (0 + 1) (x :: xs)) = (nthLe (x :: xs) 0 x✝)⁻¹ * prod (drop 0 (x :: xs))
[PROOFSTEP]
simp [nthLe]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup G
⊢ (prod [])⁻¹ = prod (map (fun x => x⁻¹) [])
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup G
x : G
xs : List G
⊢ (prod (x :: xs))⁻¹ = prod (map (fun x => x⁻¹) (x :: xs))
[PROOFSTEP]
simp [mul_comm, prod_inv xs]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
⊢ prod (set L n a) = prod L * if hn : n < length L then (nthLe L n hn)⁻¹ * a else 1
[PROOFSTEP]
refine (prod_set L n a).trans ?_
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
⊢ (prod (take n L) * if n < length L then a else 1) * prod (drop (n + 1) L) =
    prod L * if hn : n < length L then (nthLe L n hn)⁻¹ * a else 1
[PROOFSTEP]
split_ifs with hn
[GOAL]
case pos
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : n < length L
⊢ prod (take n L) * a * prod (drop (n + 1) L) = prod L * ((nthLe L n hn)⁻¹ * a)
[PROOFSTEP]
rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ← mul_assoc (take n L).prod,
  prod_take_mul_prod_drop, mul_comm a, mul_assoc]
[GOAL]
case neg
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : ¬n < length L
⊢ prod (take n L) * 1 * prod (drop (n + 1) L) = prod L * 1
[PROOFSTEP]
simp only [take_all_of_le (le_of_not_lt hn), prod_nil, mul_one, drop_eq_nil_of_le ((le_of_not_lt hn).trans n.le_succ)]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : LeftCancelMonoid M
L L' : List M
h : length L = length L'
h' : ∀ (i : ℕ), i ≤ length L → prod (take i L) = prod (take i L')
⊢ L = L'
[PROOFSTEP]
refine ext_get h fun i h₁ h₂ => ?_
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : LeftCancelMonoid M
L L' : List M
h : length L = length L'
h' : ∀ (i : ℕ), i ≤ length L → prod (take i L) = prod (take i L')
i : ℕ
h₁ : i < length L
h₂ : i < length L'
⊢ get L { val := i, isLt := h₁ } = get L' { val := i, isLt := h₂ }
[PROOFSTEP]
have : (L.take (i + 1)).prod = (L'.take (i + 1)).prod := h' _ (Nat.succ_le_of_lt h₁)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : LeftCancelMonoid M
L L' : List M
h : length L = length L'
h' : ∀ (i : ℕ), i ≤ length L → prod (take i L) = prod (take i L')
i : ℕ
h₁ : i < length L
h₂ : i < length L'
this : prod (take (i + 1) L) = prod (take (i + 1) L')
⊢ get L { val := i, isLt := h₁ } = get L' { val := i, isLt := h₂ }
[PROOFSTEP]
rw [prod_take_succ L i h₁, prod_take_succ L' i h₂, h' i (le_of_lt h₁)] at this
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : LeftCancelMonoid M
L L' : List M
h : length L = length L'
h' : ∀ (i : ℕ), i ≤ length L → prod (take i L) = prod (take i L')
i : ℕ
h₁ : i < length L
h₂ : i < length L'
this : prod (take i L') * nthLe L i h₁ = prod (take i L') * nthLe L' i h₂
⊢ get L { val := i, isLt := h₁ } = get L' { val := i, isLt := h₂ }
[PROOFSTEP]
convert mul_left_cancel this
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
L : List M
⊢ Monotone fun i => prod (take i L)
[PROOFSTEP]
refine' monotone_nat_of_le_succ fun n => _
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
L : List M
n : ℕ
⊢ prod (take n L) ≤ prod (take (n + 1) L)
[PROOFSTEP]
cases' lt_or_le n L.length with h h
[GOAL]
case inl
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
L : List M
n : ℕ
h : n < length L
⊢ prod (take n L) ≤ prod (take (n + 1) L)
[PROOFSTEP]
rw [prod_take_succ _ _ h]
[GOAL]
case inl
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
L : List M
n : ℕ
h : n < length L
⊢ prod (take n L) ≤ prod (take n L) * nthLe L n h
[PROOFSTEP]
exact le_self_mul
[GOAL]
case inr
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
L : List M
n : ℕ
h : length L ≤ n
⊢ prod (take n L) ≤ prod (take (n + 1) L)
[PROOFSTEP]
simp [take_all_of_le h, take_all_of_le (le_trans h (Nat.le_succ _))]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
b : M
h : ∀ (x : M), x ∈ [b] → 1 < x
x✝ : [b] ≠ []
⊢ 1 < prod [b]
[PROOFSTEP]
simpa using h
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
a b : M
l : List M
hl₁ : ∀ (x : M), x ∈ a :: b :: l → 1 < x
x✝ : a :: b :: l ≠ []
⊢ 1 < prod (a :: b :: l)
[PROOFSTEP]
simp only [forall_eq_or_imp, List.mem_cons] at hl₁
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 < prod (a :: b :: l)
[PROOFSTEP]
rw [List.prod_cons]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 < a * prod (b :: l)
[PROOFSTEP]
apply one_lt_mul_of_lt_of_le' hl₁.1
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 ≤ prod (b :: l)
[PROOFSTEP]
apply le_of_lt ((b :: l).one_lt_prod_of_one_lt _ (l.cons_ne_nil b))
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ ∀ (x : M), x ∈ b :: l → 1 < x
[PROOFSTEP]
intro x hx
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
x : M
hx : x ∈ b :: l
⊢ 1 < x
[PROOFSTEP]
cases hx
[GOAL]
case head
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 < b
[PROOFSTEP]
exact hl₁.2.1
[GOAL]
case tail
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
x : M
a✝ : Mem x l
⊢ 1 < x
[PROOFSTEP]
exact hl₁.2.2 _ ‹_›
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
l : List M
hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x
⊢ ∀ (x : M), x ∈ l → x ≤ prod l
[PROOFSTEP]
induction l
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
hl₁ : ∀ (x : M), x ∈ [] → 1 ≤ x
⊢ ∀ (x : M), x ∈ [] → x ≤ prod []
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : ∀ (x : M), x ∈ head✝ :: tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ head✝ :: tail✝ → x ≤ prod (head✝ :: tail✝)
[PROOFSTEP]
simp_rw [prod_cons, forall_mem_cons] at hl₁ ⊢
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * prod tail✝ ∧ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * prod tail✝
[PROOFSTEP]
constructor
[GOAL]
case cons.left
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * prod tail✝
case cons.right
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * prod tail✝
[PROOFSTEP]
case cons.left => exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * prod tail✝
[PROOFSTEP]
case cons.left => exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * prod tail✝
[PROOFSTEP]
exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)
[GOAL]
case cons.right
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * prod tail✝
[PROOFSTEP]
case cons.right hd tl ih => exact fun x H => le_mul_of_one_le_of_le hl₁.1 (ih hl₁.right x H)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → ∀ (x : M), x ∈ tl → x ≤ prod tl
hl₁ : 1 ≤ hd ∧ ∀ (x : M), x ∈ tl → 1 ≤ x
⊢ ∀ (x : M), x ∈ tl → x ≤ hd * prod tl
[PROOFSTEP]
case cons.right hd tl ih => exact fun x H => le_mul_of_one_le_of_le hl₁.1 (ih hl₁.right x H)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : OrderedCommMonoid M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → ∀ (x : M), x ∈ tl → x ≤ prod tl
hl₁ : 1 ≤ hd ∧ ∀ (x : M), x ∈ tl → 1 ≤ x
⊢ ∀ (x : M), x ∈ tl → x ≤ hd * prod tl
[PROOFSTEP]
exact fun x H => le_mul_of_one_le_of_le hl₁.1 (ih hl₁.right x H)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
l : List M
hl : ∀ (x : M), x ∈ l → x = 1
⊢ prod l = 1
[PROOFSTEP]
induction' l with i l hil
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
l : List M
hl✝ : ∀ (x : M), x ∈ l → x = 1
hl : ∀ (x : M), x ∈ [] → x = 1
⊢ prod [] = 1
[PROOFSTEP]
rfl
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
l✝ : List M
hl✝ : ∀ (x : M), x ∈ l✝ → x = 1
i : M
l : List M
hil : (∀ (x : M), x ∈ l → x = 1) → prod l = 1
hl : ∀ (x : M), x ∈ i :: l → x = 1
⊢ prod (i :: l) = 1
[PROOFSTEP]
rw [List.prod_cons, hil fun x hx => hl _ (mem_cons_of_mem i hx), hl _ (mem_cons_self i l), one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
l : List M
h : prod l ≠ 1
⊢ ∃ x, x ∈ l ∧ x ≠ 1
[PROOFSTEP]
simpa only [not_forall, exists_prop] using mt prod_eq_one h
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
l : List M
⊢ f (sum l) ≤ foldr max 0 (map f l)
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
⊢ f (sum []) ≤ foldr max 0 (map f [])
[PROOFSTEP]
simpa using h0
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
hd : M
tl : List M
IH : f (sum tl) ≤ foldr max 0 (map f tl)
⊢ f (sum (hd :: tl)) ≤ foldr max 0 (map f (hd :: tl))
[PROOFSTEP]
simp only [List.sum_cons, List.foldr_map, List.foldr] at IH ⊢
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
hd : M
tl : List M
IH : f (sum tl) ≤ foldr (fun x y => max (f x) y) 0 tl
⊢ f (hd + sum tl) ≤ max (f hd) (foldr (fun x y => max (f x) y) 0 tl)
[PROOFSTEP]
exact (hadd _ _).trans (max_le_max le_rfl IH)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
a b : M
l : List M
h : a ∈ b :: l
⊢ a * prod (List.erase (b :: l) a) = prod (b :: l)
[PROOFSTEP]
obtain rfl | ⟨ne, h⟩ := Decidable.List.eq_or_ne_mem_of_mem h
[GOAL]
case inl
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
a : M
l : List M
h : a ∈ a :: l
⊢ a * prod (List.erase (a :: l) a) = prod (a :: l)
[PROOFSTEP]
simp only [List.erase, if_pos, prod_cons, beq_self_eq_true]
[GOAL]
case inr.intro
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
a b : M
l : List M
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ a * prod (List.erase (b :: l) a) = prod (b :: l)
[PROOFSTEP]
simp only [List.erase, beq_false_of_ne ne.symm, prod_cons, prod_erase h, mul_left_comm a b]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝¹ : DecidableEq ι
inst✝ : CommMonoid M
f : ι → M
a b : ι
l : List ι
h : a ∈ b :: l
⊢ f a * prod (map f (List.erase (b :: l) a)) = prod (map f (b :: l))
[PROOFSTEP]
obtain rfl | ⟨ne, h⟩ := Decidable.List.eq_or_ne_mem_of_mem h
[GOAL]
case inl
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝¹ : DecidableEq ι
inst✝ : CommMonoid M
f : ι → M
a : ι
l : List ι
h : a ∈ a :: l
⊢ f a * prod (map f (List.erase (a :: l) a)) = prod (map f (a :: l))
[PROOFSTEP]
simp only [map, erase_cons_head, prod_cons]
[GOAL]
case inr.intro
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝¹ : DecidableEq ι
inst✝ : CommMonoid M
f : ι → M
a b : ι
l : List ι
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ f a * prod (map f (List.erase (b :: l) a)) = prod (map f (b :: l))
[PROOFSTEP]
simp only [map, erase_cons_tail _ ne.symm, prod_cons, prod_map_erase _ h, mul_left_comm (f a) (f b)]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : StrictOrderedSemiring R
l : List R
h : ∀ (a : R), a ∈ l → 0 < a
⊢ 0 < prod l
[PROOFSTEP]
induction' l with a l ih
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : StrictOrderedSemiring R
l : List R
h✝ : ∀ (a : R), a ∈ l → 0 < a
h : ∀ (a : R), a ∈ [] → 0 < a
⊢ 0 < prod []
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : StrictOrderedSemiring R
l✝ : List R
h✝ : ∀ (a : R), a ∈ l✝ → 0 < a
a : R
l : List R
ih : (∀ (a : R), a ∈ l → 0 < a) → 0 < prod l
h : ∀ (a_1 : R), a_1 ∈ a :: l → 0 < a_1
⊢ 0 < prod (a :: l)
[PROOFSTEP]
rw [prod_cons]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : StrictOrderedSemiring R
l✝ : List R
h✝ : ∀ (a : R), a ∈ l✝ → 0 < a
a : R
l : List R
ih : (∀ (a : R), a ∈ l → 0 < a) → 0 < prod l
h : ∀ (a_1 : R), a_1 ∈ a :: l → 0 < a_1
⊢ 0 < a * prod l
[PROOFSTEP]
exact mul_pos (h _ <| mem_cons_self _ _) (ih fun a ha => h a <| mem_cons_of_mem _ ha)
[GOAL]
ι : Type u_1
α✝ : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
α : Type u_9
inst✝¹ : CanonicallyOrderedCommSemiring α
inst✝ : Nontrivial α
⊢ 0 < prod [] ↔ ∀ (x : α), x ∈ [] → 0 < x
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α✝ : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
α : Type u_9
inst✝¹ : CanonicallyOrderedCommSemiring α
inst✝ : Nontrivial α
x : α
xs : List α
⊢ 0 < prod (x :: xs) ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → 0 < x_1
[PROOFSTEP]
simp_rw [prod_cons, forall_mem_cons, CanonicallyOrderedCommSemiring.mul_pos, list_prod_pos]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
L : List ℕ
⊢ headI L + sum (tail L) = sum L
[PROOFSTEP]
cases L
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
⊢ headI [] + sum (tail []) = sum []
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
head✝ : ℕ
tail✝ : List ℕ
⊢ headI (head✝ :: tail✝) + sum (tail (head✝ :: tail✝)) = sum (head✝ :: tail✝)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
L : List ℕ
⊢ sum (tail L) = sum L - headI L
[PROOFSTEP]
rw [← headI_add_tail_sum L, add_comm, @add_tsub_cancel_right]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : DivInvMonoid α
a b : α
l : List α
⊢ alternatingProd (a :: b :: l) = a / b * alternatingProd l
[PROOFSTEP]
rw [div_eq_mul_inv, alternatingProd_cons_cons']
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup α
a : α
⊢ alternatingProd [a] = a * (alternatingProd [])⁻¹
[PROOFSTEP]
rw [alternatingProd_nil, inv_one, mul_one, alternatingProd_singleton]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup α
a b : α
l : List α
⊢ alternatingProd (a :: b :: l) = a * (alternatingProd (b :: l))⁻¹
[PROOFSTEP]
rw [alternatingProd_cons_cons', alternatingProd_cons' b l, mul_inv, inv_inv, mul_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup α
a : α
l : List α
⊢ alternatingProd (a :: l) = a / alternatingProd l
[PROOFSTEP]
rw [div_eq_mul_inv, alternatingProd_cons']
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
l : List ℕ
n : ℕ
⊢ sum l % n = sum (map (fun x => x % n) l) % n
[PROOFSTEP]
induction l
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
n : ℕ
⊢ sum [] % n = sum (map (fun x => x % n) []) % n
[PROOFSTEP]
simp [Nat.add_mod, *]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
n head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : sum tail✝ % n = sum (map (fun x => x % n) tail✝) % n
⊢ sum (head✝ :: tail✝) % n = sum (map (fun x => x % n) (head✝ :: tail✝)) % n
[PROOFSTEP]
simp [Nat.add_mod, *]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
l : List ℕ
n : ℕ
⊢ prod l % n = prod (map (fun x => x % n) l) % n
[PROOFSTEP]
induction l
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
n : ℕ
⊢ prod [] % n = prod (map (fun x => x % n) []) % n
[PROOFSTEP]
simp [Nat.mul_mod, *]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
n head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : prod tail✝ % n = prod (map (fun x => x % n) tail✝) % n
⊢ prod (head✝ :: tail✝) % n = prod (map (fun x => x % n) (head✝ :: tail✝)) % n
[PROOFSTEP]
simp [Nat.mul_mod, *]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
l : List ℤ
n : ℤ
⊢ sum l % n = sum (map (fun x => x % n) l) % n
[PROOFSTEP]
induction l
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
n : ℤ
⊢ sum [] % n = sum (map (fun x => x % n) []) % n
[PROOFSTEP]
simp [Int.add_emod, *]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
n head✝ : ℤ
tail✝ : List ℤ
tail_ih✝ : sum tail✝ % n = sum (map (fun x => x % n) tail✝) % n
⊢ sum (head✝ :: tail✝) % n = sum (map (fun x => x % n) (head✝ :: tail✝)) % n
[PROOFSTEP]
simp [Int.add_emod, *]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
l : List ℤ
n : ℤ
⊢ prod l % n = prod (map (fun x => x % n) l) % n
[PROOFSTEP]
induction l
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
n : ℤ
⊢ prod [] % n = prod (map (fun x => x % n) []) % n
[PROOFSTEP]
simp [Int.mul_emod, *]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
n head✝ : ℤ
tail✝ : List ℤ
tail_ih✝ : prod tail✝ % n = prod (map (fun x => x % n) tail✝) % n
⊢ prod (head✝ :: tail✝) % n = prod (map (fun x => x % n) (head✝ :: tail✝)) % n
[PROOFSTEP]
simp [Int.mul_emod, *]


[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
⊢ p fab
[PROOFSTEP]
have h1 : fab = Sum.rec (fun a => fab (Sum.inl a)) (fun b => fab (Sum.inr b)) := by ext ab; cases ab <;> rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
⊢ fab = fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t
[PROOFSTEP]
ext ab
[GOAL]
case h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
ab : α ⊕ β
⊢ fab ab = rec (fun a => fab (inl a)) (fun b => fab (inr b)) ab
[PROOFSTEP]
cases ab
[GOAL]
case h.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
val✝ : α
⊢ fab (inl val✝) = rec (fun a => fab (inl a)) (fun b => fab (inr b)) (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case h.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
val✝ : β
⊢ fab (inr val✝) = rec (fun a => fab (inl a)) (fun b => fab (inr b)) (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
h1 : fab = fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t
⊢ p fab
[PROOFSTEP]
rw [h1]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
h1 : fab = fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t
⊢ p fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t
[PROOFSTEP]
exact h _ _
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (∃ fab, p fab) ↔ ∃ fa fb, p fun t => rec fa fb t
[PROOFSTEP]
rw [← not_forall_not, forall_sum_pi]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (¬∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), ¬p fun t => rec fa fb t) ↔
    ∃ fa fb, p fun t => rec fa fb t
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ getLeft? x = none ↔ isRight x = true
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : α
⊢ getLeft? (inl val✝) = none ↔ isRight (inl val✝) = true
[PROOFSTEP]
simp only [getLeft?, isRight, eq_self_iff_true]
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : β
⊢ getLeft? (inr val✝) = none ↔ isRight (inr val✝) = true
[PROOFSTEP]
simp only [getLeft?, isRight, eq_self_iff_true]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ getRight? x = none ↔ isLeft x = true
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : α
⊢ getRight? (inl val✝) = none ↔ isLeft (inl val✝) = true
[PROOFSTEP]
simp only [getRight?, isLeft, eq_self_iff_true]
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : β
⊢ getRight? (inr val✝) = none ↔ isLeft (inr val✝) = true
[PROOFSTEP]
simp only [getRight?, isLeft, eq_self_iff_true]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
a : α
⊢ getLeft? x = some a ↔ x = inl a
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
a val✝ : α
⊢ getLeft? (inl val✝) = some a ↔ inl val✝ = inl a
[PROOFSTEP]
simp only [getLeft?, Option.some.injEq, inl.injEq]
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
a : α
val✝ : β
⊢ getLeft? (inr val✝) = some a ↔ inr val✝ = inl a
[PROOFSTEP]
simp only [getLeft?, Option.some.injEq, inl.injEq]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
b : β
⊢ getRight? x = some b ↔ x = inr b
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
b : β
val✝ : α
⊢ getRight? (inl val✝) = some b ↔ inl val✝ = inr b
[PROOFSTEP]
simp only [getRight?, Option.some.injEq, inr.injEq]
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
b val✝ : β
⊢ getRight? (inr val✝) = some b ↔ inr val✝ = inr b
[PROOFSTEP]
simp only [getRight?, Option.some.injEq, inr.injEq]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x✝ y x : α ⊕ β
⊢ (!isLeft x) = isRight x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
val✝ : α
⊢ (!isLeft (inl val✝)) = isRight (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
val✝ : β
⊢ (!isLeft (inr val✝)) = isRight (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ isLeft x = false ↔ isRight x = true
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : α
⊢ isLeft (inl val✝) = false ↔ isRight (inl val✝) = true
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : β
⊢ isLeft (inr val✝) = false ↔ isRight (inr val✝) = true
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ ¬isLeft x = true ↔ isRight x = true
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x✝ y x : α ⊕ β
⊢ (!decide (isRight x = isLeft x)) = true
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
val✝ : α
⊢ (!decide (isRight (inl val✝) = isLeft (inl val✝))) = true
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
val✝ : β
⊢ (!decide (isRight (inr val✝) = isLeft (inr val✝))) = true
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ isRight x = false ↔ isLeft x = true
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : α
⊢ isRight (inl val✝) = false ↔ isLeft (inl val✝) = true
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : β
⊢ isRight (inr val✝) = false ↔ isLeft (inr val✝) = true
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ ¬isRight x = true ↔ isLeft x = true
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ isLeft x = true ↔ ∃ y, x = inl y
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : α
⊢ isLeft (inl val✝) = true ↔ ∃ y, inl val✝ = inl y
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : β
⊢ isLeft (inr val✝) = true ↔ ∃ y, inr val✝ = inl y
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ isRight x = true ↔ ∃ y, x = inr y
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : α
⊢ isRight (inl val✝) = true ↔ ∃ y, inl val✝ = inr y
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : β
⊢ isRight (inr val✝) = true ↔ ∃ y, inr val✝ = inr y
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
α' : Type w
β✝ : Type v
β' : Type x
γ✝ : Type u_1
δ✝ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
ε : Sort u_7
f₁ : α → β
f₂ : β → ε
g₁ : γ → δ
g₂ : δ → ε
x : α ⊕ γ
⊢ Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x
[PROOFSTEP]
cases x
[GOAL]
case inl
α✝ : Type u
α' : Type w
β✝ : Type v
β' : Type x
γ✝ : Type u_1
δ✝ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
ε : Sort u_7
f₁ : α → β
f₂ : β → ε
g₁ : γ → δ
g₂ : δ → ε
val✝ : α
⊢ Sum.elim f₂ g₂ (Sum.map f₁ g₁ (inl val✝)) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α✝ : Type u
α' : Type w
β✝ : Type v
β' : Type x
γ✝ : Type u_1
δ✝ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
ε : Sort u_7
f₁ : α → β
f₂ : β → ε
g₁ : γ → δ
g₂ : δ → ε
val✝ : γ
⊢ Sum.elim f₂ g₂ (Sum.map f₁ g₁ (inr val✝)) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
x : α ⊕ γ
⊢ isLeft (Sum.map f g x) = isLeft x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : α
⊢ isLeft (Sum.map f g (inl val✝)) = isLeft (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : γ
⊢ isLeft (Sum.map f g (inr val✝)) = isLeft (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
x : α ⊕ γ
⊢ isRight (Sum.map f g x) = isRight x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : α
⊢ isRight (Sum.map f g (inl val✝)) = isRight (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : γ
⊢ isRight (Sum.map f g (inr val✝)) = isRight (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
x : α ⊕ γ
⊢ getLeft? (Sum.map f g x) = Option.map f (getLeft? x)
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : α
⊢ getLeft? (Sum.map f g (inl val✝)) = Option.map f (getLeft? (inl val✝))
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : γ
⊢ getLeft? (Sum.map f g (inr val✝)) = Option.map f (getLeft? (inr val✝))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
x : α ⊕ γ
⊢ getRight? (Sum.map f g x) = Option.map g (getRight? x)
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : α
⊢ getRight? (Sum.map f g (inl val✝)) = Option.map g (getRight? (inl val✝))
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : γ
⊢ getRight? (Sum.map f g (inr val✝)) = Option.map g (getRight? (inr val✝))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : α
x : γ
⊢ x = Sum.elim (update f i x) g (inl i)
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : α
x : γ
⊢ ∀ (x_1 : α ⊕ β), x_1 ≠ inl i → Sum.elim f g x_1 = Sum.elim (update f i x) g x_1
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : β
x : γ
⊢ x = Sum.elim f (update g i x) (inr i)
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : β
x : γ
⊢ ∀ (x_1 : α ⊕ β), x_1 ≠ inr i → Sum.elim f g x_1 = Sum.elim f (update g i x) x_1
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : α
x : γ
⊢ update f (inl i) x (inl j) = update (f ∘ inl) i x j
[PROOFSTEP]
rw [← update_inl_comp_inl, Function.comp_apply]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : β
x : γ
⊢ update f (inr i) x (inr j) = update (f ∘ inr) i x j
[PROOFSTEP]
rw [← update_inr_comp_inr, Function.comp_apply]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x : α ⊕ β
⊢ swap (swap x) = x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : α
⊢ swap (swap (inl val✝)) = inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : β
⊢ swap (swap (inr val✝)) = inr val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x : α ⊕ β
⊢ isLeft (swap x) = isRight x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : α
⊢ isLeft (swap (inl val✝)) = isRight (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : β
⊢ isLeft (swap (inr val✝)) = isRight (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x : α ⊕ β
⊢ isRight (swap x) = isLeft x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : α
⊢ isRight (swap (inl val✝)) = isLeft (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : β
⊢ isRight (swap (inr val✝)) = isLeft (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x : α ⊕ β
⊢ getLeft? (swap x) = getRight? x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : α
⊢ getLeft? (swap (inl val✝)) = getRight? (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : β
⊢ getLeft? (swap (inr val✝)) = getRight? (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x : α ⊕ β
⊢ getRight? (swap x) = getLeft? x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : α
⊢ getRight? (swap (inl val✝)) = getLeft? (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : β
⊢ getRight? (swap (inr val✝)) = getLeft? (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s (inl a) (inl c)
⊢ r a c
[PROOFSTEP]
cases h
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
a✝ : r a c
⊢ r a c
[PROOFSTEP]
assumption
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s (inr b) (inr d)
⊢ s b d
[PROOFSTEP]
cases h
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
a✝ : s b d
⊢ s b d
[PROOFSTEP]
assumption
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
hr : ∀ (a : α) (b : γ), r₁ a b → r₂ a b
hs : ∀ (a : β) (b : δ), s₁ a b → s₂ a b
h : LiftRel r₁ s₁ x y
⊢ LiftRel r₂ s₂ x y
[PROOFSTEP]
cases h
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
hr : ∀ (a : α) (b : γ), r₁ a b → r₂ a b
hs : ∀ (a : β) (b : δ), s₁ a b → s₂ a b
a✝¹ : α
c✝ : γ
a✝ : r₁ a✝¹ c✝
⊢ LiftRel r₂ s₂ (inl a✝¹) (inl c✝)
[PROOFSTEP]
exact LiftRel.inl (hr _ _ ‹_›)
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
hr : ∀ (a : α) (b : γ), r₁ a b → r₂ a b
hs : ∀ (a : β) (b : δ), s₁ a b → s₂ a b
b✝ : β
d✝ : δ
a✝ : s₁ b✝ d✝
⊢ LiftRel r₂ s₂ (inr b✝) (inr d✝)
[PROOFSTEP]
exact LiftRel.inr (hs _ _ ‹_›)
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s x y
⊢ LiftRel s r (swap x) (swap y)
[PROOFSTEP]
cases h
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
a✝¹ : α
c✝ : γ
a✝ : r a✝¹ c✝
⊢ LiftRel s r (swap (inl a✝¹)) (swap (inl c✝))
[PROOFSTEP]
exact LiftRel.inr ‹_›
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
b✝ : β
d✝ : δ
a✝ : s b✝ d✝
⊢ LiftRel s r (swap (inr b✝)) (swap (inr d✝))
[PROOFSTEP]
exact LiftRel.inl ‹_›
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel s r (swap x) (swap y)
⊢ LiftRel r s x y
[PROOFSTEP]
rw [← swap_swap x, ← swap_swap y]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel s r (swap x) (swap y)
⊢ LiftRel r s (swap (swap x)) (swap (swap y))
[PROOFSTEP]
exact h.swap
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
h : Lex r s (inl a₁) (inl a₂)
⊢ r a₁ a₂
[PROOFSTEP]
cases h
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
h✝ : r a₁ a₂
⊢ r a₁ a₂
[PROOFSTEP]
assumption
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
h : Lex r s (inr b₁) (inr b₂)
⊢ s b₁ b₂
[PROOFSTEP]
cases h
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
h✝ : s b₁ b₂
⊢ s b₁ b₂
[PROOFSTEP]
assumption
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
x y a b : α ⊕ β
h : LiftRel r s a b
⊢ Lex r s a b
[PROOFSTEP]
cases h
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
a✝¹ c✝ : α
a✝ : r a✝¹ c✝
⊢ Lex r s (inl a✝¹) (inl c✝)
[PROOFSTEP]
exact Lex.inl ‹_›
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
b✝ d✝ : β
a✝ : s b✝ d✝
⊢ Lex r s (inr b✝) (inr d✝)
[PROOFSTEP]
exact Lex.inr ‹_›
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
h : Lex r₁ s₁ x y
⊢ Lex r₂ s₂ x y
[PROOFSTEP]
cases h
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
a₁✝ a₂✝ : α
h✝ : r₁ a₁✝ a₂✝
⊢ Lex r₂ s₂ (inl a₁✝) (inl a₂✝)
[PROOFSTEP]
exact Lex.inl (hr _ _ ‹_›)
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
b₁✝ b₂✝ : β
h✝ : s₁ b₁✝ b₂✝
⊢ Lex r₂ s₂ (inr b₁✝) (inr b₂✝)
[PROOFSTEP]
exact Lex.inr (hs _ _ ‹_›)
[GOAL]
case sep
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
a✝ : α
b✝ : β
⊢ Lex r₂ s₂ (inl a✝) (inr b✝)
[PROOFSTEP]
exact Lex.sep _ _
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝ a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
a : α
aca : Acc r a
⊢ Acc (Lex r s) (inl a)
[PROOFSTEP]
induction' aca with a _ IH
[GOAL]
case intro
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝¹ a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α), r y a → Acc (Lex r s) (inl y)
⊢ Acc (Lex r s) (inl a)
[PROOFSTEP]
constructor
[GOAL]
case intro.h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝¹ a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α), r y a → Acc (Lex r s) (inl y)
⊢ ∀ (y : α ⊕ β), Lex r s y (inl a) → Acc (Lex r s) y
[PROOFSTEP]
intro y h
[GOAL]
case intro.h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝¹ a₁ a₂ : α
b b₁ b₂ : β
x y✝ : α ⊕ β
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α), r y a → Acc (Lex r s) (inl y)
y : α ⊕ β
h : Lex r s y (inl a)
⊢ Acc (Lex r s) y
[PROOFSTEP]
cases' h with a' _ h'
[GOAL]
case intro.h.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝¹ a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α), r y a → Acc (Lex r s) (inl y)
a' : α
h' : r a' a
⊢ Acc (Lex r s) (inl a')
[PROOFSTEP]
exact IH _ h'
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b : β
acb : Acc s b
⊢ Acc (Lex r s) (inr b)
[PROOFSTEP]
induction' acb with b _ IH
[GOAL]
case intro
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
⊢ Acc (Lex r s) (inr b)
[PROOFSTEP]
constructor
[GOAL]
case intro.h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
⊢ ∀ (y : α ⊕ β), Lex r s y (inr b) → Acc (Lex r s) y
[PROOFSTEP]
intro y h
[GOAL]
case intro.h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y✝ : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
y : α ⊕ β
h : Lex r s y (inr b)
⊢ Acc (Lex r s) y
[PROOFSTEP]
cases' h with _ _ _ b' _ h' a
[GOAL]
case intro.h.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
b' : β
h' : s b' b
⊢ Acc (Lex r s) (inr b')
[PROOFSTEP]
exact IH _ h'
[GOAL]
case intro.h.sep
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝ a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
a : α
⊢ Acc (Lex r s) (inl a)
[PROOFSTEP]
exact aca _
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
c : γ
⊢ ∃ a, f a = c
[PROOFSTEP]
obtain ⟨a | b, h⟩ := h (inl c)
[GOAL]
case intro.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
a : α
h : Sum.map f g (inl a) = inl c
⊢ ∃ a, f a = c
[PROOFSTEP]
exact ⟨a, inl_injective h⟩
[GOAL]
case intro.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
b : β
h : Sum.map f g (inr b) = inl c
⊢ ∃ a, f a = c
[PROOFSTEP]
cases h
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
d : δ
⊢ ∃ a, g a = d
[PROOFSTEP]
obtain ⟨a | b, h⟩ := h (inr d)
[GOAL]
case intro.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
a : α
h : Sum.map f g (inl a) = inr d
⊢ ∃ a, g a = d
[PROOFSTEP]
cases h
[GOAL]
case intro.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ a, g a = d
[PROOFSTEP]
exact ⟨b, inr_injective h⟩
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
c : γ
⊢ Sum.elim (const α c) (const β c) = const (α ⊕ β) c
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
c : γ
x : α ⊕ β
⊢ Sum.elim (const α c) (const β c) x = const (α ⊕ β) c x
[PROOFSTEP]
cases x
[GOAL]
case h.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
c : γ
val✝ : α
⊢ Sum.elim (const α c) (const β c) (inl val✝) = const (α ⊕ β) c (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case h.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
c : γ
val✝ : β
⊢ Sum.elim (const α c) (const β c) (inr val✝) = const (α ⊕ β) c (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
⊢ Sum.elim (update f i c) g = update (Sum.elim f g) (inl i) c
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α ⊕ β
⊢ Sum.elim (update f i c) g x = update (Sum.elim f g) (inl i) c x
[PROOFSTEP]
rcases x with x | x
[GOAL]
case h.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)
[PROOFSTEP]
by_cases h : x = i
[GOAL]
case pos
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
h : x = i
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)
[PROOFSTEP]
subst h
[GOAL]
case pos
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
c : γ
x : α
⊢ Sum.elim (update f x c) g (inl x) = update (Sum.elim f g) (inl x) c (inl x)
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
h : ¬x = i
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)
[PROOFSTEP]
simp [h]
[GOAL]
case h.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : β
⊢ Sum.elim (update f i c) g (inr x) = update (Sum.elim f g) (inl i) c (inr x)
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
⊢ Sum.elim f (update g i c) = update (Sum.elim f g) (inr i) c
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : α ⊕ β
⊢ Sum.elim f (update g i c) x = update (Sum.elim f g) (inr i) c x
[PROOFSTEP]
rcases x with x | x
[GOAL]
case h.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : α
⊢ Sum.elim f (update g i c) (inl x) = update (Sum.elim f g) (inr i) c (inl x)
[PROOFSTEP]
simp
[GOAL]
case h.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : β
⊢ Sum.elim f (update g i c) (inr x) = update (Sum.elim f g) (inr i) c (inr x)
[PROOFSTEP]
by_cases h : x = i
[GOAL]
case pos
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : β
h : x = i
⊢ Sum.elim f (update g i c) (inr x) = update (Sum.elim f g) (inr i) c (inr x)
[PROOFSTEP]
subst h
[GOAL]
case pos
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
c : γ
x : β
⊢ Sum.elim f (update g x c) (inr x) = update (Sum.elim f g) (inr x) c (inr x)
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : β
h : ¬x = i
⊢ Sum.elim f (update g i c) (inr x) = update (Sum.elim f g) (inr i) c (inr x)
[PROOFSTEP]
simp [h]