ι : Type u_2
α : Type ?u.144930
β : Type ?u.144933
M : Type u_1
N : Type ?u.144939
G : Type ?u.144942
k : Type ?u.144945
R : Type ?u.144948
inst✝ : LinearOrderedCancelCommMonoid M
f✝ g : ι → M
s t : Finset ι
f : ι → M
h₂ : ∃ i, i ∈ s ∧ f i ≠ 1
h₁ : ∀ (i : ι), i ∈ s → f i ≤ 1
⊢ ∏ i in s, f i ≠ 1
ι : Type u_2
α : Type ?u.144930
β : Type ?u.144933
M : Type u_1
N : Type ?u.144939
G : Type ?u.144942
k : Type ?u.144945
R : Type ?u.144948
inst✝ : LinearOrderedCancelCommMonoid M
f✝ g : ι → M
s t : Finset ι
f : ι → M
h₁ : ∏ i in s, f i = 1
h₂ : ∃ i, i ∈ s ∧ f i ≠ 1
⊢ ∃ i, i ∈ s ∧ 1 < f i
contrapose! h₁
case intro.intro
ι : Type u_2
α : Type ?u.144930
β : Type ?u.144933
M : Type u_1
N : Type ?u.144939
G : Type ?u.144942
k : Type ?u.144945
R : Type ?u.144948
inst✝ : LinearOrderedCancelCommMonoid M
f✝ g : ι → M
s t : Finset ι
f : ι → M
h₁ : ∀ (i : ι), i ∈ s → f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
⊢ ∏ i in s, f i ≠ 1
ι : Type u_2
α : Type ?u.144930
β : Type ?u.144933
M : Type u_1
N : Type ?u.144939
G : Type ?u.144942
k : Type ?u.144945
R : Type ?u.144948
inst✝ : LinearOrderedCancelCommMonoid M
f✝ g : ι → M
s t : Finset ι
f : ι → M
h₂ : ∃ i, i ∈ s ∧ f i ≠ 1
h₁ : ∀ (i : ι), i ∈ s → f i ≤ 1
⊢ ∏ i in s, f i ≠ 1
obtain ⟨i, m, i_ne⟩ : ∃ i ∈ s, f i ≠ 1 := h₂
case intro.intro.h
ι : Type u_2
α : Type ?u.144930
β : Type ?u.144933
M : Type u_1
N : Type ?u.144939
G : Type ?u.144942
k : Type ?u.144945
R : Type ?u.144948
inst✝ : LinearOrderedCancelCommMonoid M
f✝ g : ι → M
s t : Finset ι
f : ι → M
h₁ : ∀ (i : ι), i ∈ s → f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
⊢ ∏ i in s, f i < 1
case intro.intro
ι : Type u_2
α : Type ?u.144930
β : Type ?u.144933
M : Type u_1
N : Type ?u.144939
G : Type ?u.144942
k : Type ?u.144945
R : Type ?u.144948
inst✝ : LinearOrderedCancelCommMonoid M
f✝ g : ι → M
s t : Finset ι
f : ι → M
h₁ : ∀ (i : ι), i ∈ s → f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
⊢ ∏ i in s, f i ≠ 1
apply ne_of_lt
no goals
case intro.intro.h
ι : Type u_2
α : Type ?u.144930
β : Type ?u.144933
M : Type u_1
N : Type ?u.144939
G : Type ?u.144942
k : Type ?u.144945
R : Type ?u.144948
inst✝ : LinearOrderedCancelCommMonoid M
f✝ g : ι → M
s t : Finset ι
f : ι → M
h₁ : ∀ (i : ι), i ∈ s → f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
⊢ ∏ i in s, f i < 1
calc
  (∏ j in s, f j) < ∏ j in s, 1 := prod_lt_prod' h₁ ⟨i, m, (h₁ i m).lt_of_ne i_ne⟩
  _ = 1 := prod_const_one