ι : Type ?u.788537
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel Setoid.r
h : ∀ (x : α), x ∈ s → ∏ a in filter (fun y => y ≈ x) s, f a = 1
⊢ ∀ (x : Quotient R), x ∈ image Quotient.mk'' s → ∏ y in filter (fun x_1 => Quotient.mk R x_1 = x) s, f y = 1
ι : Type ?u.788537
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel Setoid.r
h : ∀ (x : α), x ∈ s → ∏ a in filter (fun y => y ≈ x) s, f a = 1
⊢ ∏ x in s, f x = 1
rw [prod_partition R, ← Finset.prod_eq_one]
ι : Type ?u.788537
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel Setoid.r
h : ∀ (x : α), x ∈ s → ∏ a in filter (fun y => y ≈ x) s, f a = 1
xbar : Quotient R
xbar_in_s : xbar ∈ image Quotient.mk'' s
⊢ ∏ y in filter (fun x => Quotient.mk R x = xbar) s, f y = 1
ι : Type ?u.788537
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel Setoid.r
h : ∀ (x : α), x ∈ s → ∏ a in filter (fun y => y ≈ x) s, f a = 1
⊢ ∀ (x : Quotient R), x ∈ image Quotient.mk'' s → ∏ y in filter (fun x_1 => Quotient.mk R x_1 = x) s, f y = 1
intro xbar xbar_in_s
case intro.intro
ι : Type ?u.788537
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel Setoid.r
h : ∀ (x : α), x ∈ s → ∏ a in filter (fun y => y ≈ x) s, f a = 1
x : α
x_in_s : x ∈ s
xbar_in_s : Quotient.mk'' x ∈ image Quotient.mk'' s
⊢ ∏ y in filter (fun x_1 => Quotient.mk R x_1 = Quotient.mk'' x) s, f y = 1
ι : Type ?u.788537
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel Setoid.r
h : ∀ (x : α), x ∈ s → ∏ a in filter (fun y => y ≈ x) s, f a = 1
xbar : Quotient R
xbar_in_s : xbar ∈ image Quotient.mk'' s
⊢ ∏ y in filter (fun x => Quotient.mk R x = xbar) s, f y = 1
obtain ⟨x, x_in_s, rfl⟩ := mem_image.mp xbar_in_s
case intro.intro
ι : Type ?u.788537
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel Setoid.r
x : α
x_in_s : x ∈ s
xbar_in_s : Quotient.mk'' x ∈ image Quotient.mk'' s
h : ∀ (x : α), x ∈ s → ∏ x in filter (fun y => Quotient.mk R y = Quotient.mk R x) s, f x = 1
⊢ ∏ y in filter (fun x_1 => Quotient.mk R x_1 = Quotient.mk'' x) s, f y = 1
case intro.intro
ι : Type ?u.788537
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel Setoid.r
h : ∀ (x : α), x ∈ s → ∏ a in filter (fun y => y ≈ x) s, f a = 1
x : α
x_in_s : x ∈ s
xbar_in_s : Quotient.mk'' x ∈ image Quotient.mk'' s
⊢ ∏ y in filter (fun x_1 => Quotient.mk R x_1 = Quotient.mk'' x) s, f y = 1
simp only [← Quotient.eq] at h
no goals
case intro.intro
ι : Type ?u.788537
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel Setoid.r
x : α
x_in_s : x ∈ s
xbar_in_s : Quotient.mk'' x ∈ image Quotient.mk'' s
h : ∀ (x : α), x ∈ s → ∏ x in filter (fun y => Quotient.mk R y = Quotient.mk R x) s, f x = 1
⊢ ∏ y in filter (fun x_1 => Quotient.mk R x_1 = Quotient.mk'' x) s, f y = 1
exact h x x_in_s