case nil
ι : Type u_2
α : Type ?u.85857
M : Type u_1
N : Type ?u.85863
P : Type ?u.85866
M₀ : Type ?u.85869
G : Type ?u.85872
R : Type ?u.85875
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 [])

case cons
ι : Type u_2
α : Type ?u.85857
M : Type u_1
N : Type ?u.85863
P : Type ?u.85866
M₀ : Type ?u.85869
G : Type ?u.85872
R : Type ?u.85875
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))
ι : Type u_2
α : Type ?u.85857
M : Type u_1
N : Type ?u.85863
P : Type ?u.85866
M₀ : Type ?u.85869
G : Type ?u.85872
R : Type ?u.85875
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)
induction' l with i l ihl
case cons
ι : Type u_2
α : Type ?u.85857
M : Type u_1
N : Type ?u.85863
P : Type ?u.85866
M₀ : Type ?u.85869
G : Type ?u.85872
R : Type ?u.85875
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)
case cons
ι : Type u_2
α : Type ?u.85857
M : Type u_1
N : Type ?u.85863
P : Type ?u.85866
M₀ : Type ?u.85869
G : Type ?u.85872
R : Type ?u.85875
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))
simp only [forall_mem_cons, exists_mem_cons, map_cons, prod_cons] at h₁ h₂⊢
case cons.inl
ι : Type u_2
α : Type ?u.85857
M : Type u_1
N : Type ?u.85863
P : Type ?u.85866
M₀ : Type ?u.85869
G : Type ?u.85872
R : Type ?u.85875
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)

case cons.inr
ι : Type u_2
α : Type ?u.85857
M : Type u_1
N : Type ?u.85863
P : Type ?u.85866
M₀ : Type ?u.85869
G : Type ?u.85872
R : Type ?u.85875
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)
case cons
ι : Type u_2
α : Type ?u.85857
M : Type u_1
N : Type ?u.85863
P : Type ?u.85866
M₀ : Type ?u.85869
G : Type ?u.85872
R : Type ?u.85875
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)
cases h₂
no goals
case nil
ι : Type u_2
α : Type ?u.85857
M : Type u_1
N : Type ?u.85863
P : Type ?u.85866
M₀ : Type ?u.85869
G : Type ?u.85872
R : Type ?u.85875
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 [])
rcases h₂ with ⟨_, ⟨⟩, _⟩
no goals
case cons.inl
ι : Type u_2
α : Type ?u.85857
M : Type u_1
N : Type ?u.85863
P : Type ?u.85866
M₀ : Type ?u.85869
G : Type ?u.85872
R : Type ?u.85875
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)
exact mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod' h₁.2)
no goals
case cons.inr
ι : Type u_2
α : Type ?u.85857
M : Type u_1
N : Type ?u.85863
P : Type ?u.85866
M₀ : Type ?u.85869
G : Type ?u.85872
R : Type ?u.85875
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)
exact mul_lt_mul_of_le_of_lt h₁.1 <| ihl h₁.2 ‹_›