no goals
ι : Type u_1
α : Type ?u.27020
β : Type ?u.27023
M : Type ?u.27026
N : Type u_2
G : Type ?u.27032
k : Type ?u.27035
R : Type ?u.27038
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
⊢ (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
classical
  refine Finset.induction_on s
    (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.not_mem_empty _ h), fun _ ↦ rfl⟩) ?_
  intro a s ha ih H
  have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
  rw [prod_insert ha, mul_eq_one_iff' (H _ <| mem_insert_self _ _) (one_le_prod' this),
    forall_mem_insert, ih this]
ι : Type u_1
α : Type ?u.27020
β : Type ?u.27023
M : Type ?u.27026
N : Type u_2
G : Type ?u.27032
k : Type ?u.27035
R : Type ?u.27038
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)) →
        (∀ (i : ι), i ∈ insert a s → 1 ≤ f i) → (∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1)
ι : Type u_1
α : Type ?u.27020
β : Type ?u.27023
M : Type ?u.27026
N : Type u_2
G : Type ?u.27032
k : Type ?u.27035
R : Type ?u.27038
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
⊢ (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
refine Finset.induction_on s
  (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.not_mem_empty _ h), fun _ ↦ rfl⟩) ?_
ι : Type u_1
α : Type ?u.27020
β : Type ?u.27023
M : Type ?u.27026
N : Type u_2
G : Type ?u.27032
k : Type ?u.27035
R : Type ?u.27038
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s✝ t : Finset ι
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
H : ∀ (i : ι), i ∈ insert a s → 1 ≤ f i
⊢ ∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
ι : Type u_1
α : Type ?u.27020
β : Type ?u.27023
M : Type ?u.27026
N : Type u_2
G : Type ?u.27032
k : Type ?u.27035
R : Type ?u.27038
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)) →
        (∀ (i : ι), i ∈ insert a s → 1 ≤ f i) → (∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1)
intro a s ha ih H
ι : Type u_1
α : Type ?u.27020
β : Type ?u.27023
M : Type ?u.27026
N : Type u_2
G : Type ?u.27032
k : Type ?u.27035
R : Type ?u.27038
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s✝ t : Finset ι
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
H : ∀ (i : ι), i ∈ insert a s → 1 ≤ f i
this : ∀ (i : ι), i ∈ s → 1 ≤ f i
⊢ ∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
ι : Type u_1
α : Type ?u.27020
β : Type ?u.27023
M : Type ?u.27026
N : Type u_2
G : Type ?u.27032
k : Type ?u.27035
R : Type ?u.27038
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s✝ t : Finset ι
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
H : ∀ (i : ι), i ∈ insert a s → 1 ≤ f i
⊢ ∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
no goals
ι : Type u_1
α : Type ?u.27020
β : Type ?u.27023
M : Type ?u.27026
N : Type u_2
G : Type ?u.27032
k : Type ?u.27035
R : Type ?u.27038
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s✝ t : Finset ι
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
H : ∀ (i : ι), i ∈ insert a s → 1 ≤ f i
this : ∀ (i : ι), i ∈ s → 1 ≤ f i
⊢ ∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
rw [prod_insert ha, mul_eq_one_iff' (H _ <| mem_insert_self _ _) (one_le_prod' this),
  forall_mem_insert, ih this]