Theorem: Function.support_of_along_fiber_subset_subset (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
⊢ support f ⊆ s ×ˢ t
Tactic:
intro ⟨x, y⟩ hxy
State after:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y) ∈ s ×ˢ t

State before:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y) ∈ s ×ˢ t
Tactic:
constructor
State after:
case left
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y).1 ∈ s

case right
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y).2 ∈ t

State before:
case left
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y).1 ∈ s
Tactic:
exact hx y (by simp only [Function.mem_support, ne_eq] at hxy ⊢; exact hxy)
State after:
no goals

State before:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y).1 ∈ support fun x => f (x, y)
Tactic:
simp only [Function.mem_support, ne_eq] at hxy ⊢
State after:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : ¬f (x, y) = 0
⊢ ¬f (x, y) = 0

State before:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : ¬f (x, y) = 0
⊢ ¬f (x, y) = 0
Tactic:
exact hxy
State after:
no goals

State before:
case right
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y).2 ∈ t
Tactic:
exact hy x (by simp only [Function.mem_support, ne_eq] at hxy ⊢; exact hxy)
State after:
no goals

State before:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y).2 ∈ support fun y => f (x, y)
Tactic:
simp only [Function.mem_support, ne_eq] at hxy ⊢
State after:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : ¬f (x, y) = 0
⊢ ¬f (x, y) = 0