α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : f x ≠ 1
⊢ x ∈ s ↔ x ∈ t
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
⊢ ∀ {x : α}, f x ≠ 1 → (x ∈ s ↔ x ∈ t)
intro x hxf
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
⊢ x ∈ s ↔ x ∈ t
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : f x ≠ 1
⊢ x ∈ s ↔ x ∈ t
rw [← mem_mulSupport] at hxf
case refine_1
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ t

case refine_2
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
⊢ x ∈ s ↔ x ∈ t
refine ⟨fun hx => ?_, fun hx => ?_⟩
case refine_1
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ ↑t ∩ mulSupport f
case refine_1
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ t
refine ((mem_inter_iff x t (mulSupport f)).mp ?_).1
case refine_1
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ s ∧ x ∈ mulSupport f
case refine_1
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ ↑t ∩ mulSupport f
rw [← Set.ext_iff.mp h x, mem_inter_iff]
no goals
case refine_1
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ s ∧ x ∈ mulSupport f
exact ⟨hx, hxf⟩
case refine_2
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s ∩ mulSupport f
case refine_2
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s
refine ((mem_inter_iff x s (mulSupport f)).mp ?_).1
case refine_2
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ ↑t ∧ x ∈ mulSupport f
case refine_2
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s ∩ mulSupport f
rw [Set.ext_iff.mp h x, mem_inter_iff]
no goals
case refine_2
α : Type u_1
β : Type ?u.192527
ι : Type ?u.192530
G : Type ?u.192533
M : Type u_2
N : Type ?u.192539
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ ↑t ∧ x ∈ mulSupport f
exact ⟨hx, hxf⟩