[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
s : Set α
⊢ mulSupport f = s ↔ (∀ (x : α), x ∈ s → f x ≠ 1) ∧ ∀ (x : α), ¬x ∈ s → f x = 1
[PROOFSTEP]
simp (config := { contextual := true }) only [ext_iff, mem_mulSupport, ne_eq, iff_def, not_imp_comm, and_comm,
  forall_and]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
s : Set α
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s
[PROOFSTEP]
simp_rw [← subset_compl_iff_disjoint_right, mulSupport_subset_iff', not_mem_compl_iff, EqOn, Pi.one_apply]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
s : Set α
⊢ Disjoint s (mulSupport f) ↔ EqOn f 1 s
[PROOFSTEP]
rw [disjoint_comm, mulSupport_disjoint_iff]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
⊢ mulSupport f = ∅ ↔ f = 1
[PROOFSTEP]
simp_rw [← subset_empty_iff, mulSupport_subset_iff', funext_iff]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
⊢ (∀ (x : α), ¬x ∈ ∅ → f x = 1) ↔ ∀ (a : α), f a = OfNat.ofNat 1 a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
⊢ Set.Nonempty (mulSupport f) ↔ f ≠ 1
[PROOFSTEP]
rw [nonempty_iff_ne_empty, Ne.def, mulSupport_eq_empty_iff]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
⊢ range f ⊆ insert 1 (f '' mulSupport f)
[PROOFSTEP]
simpa only [range_subset_iff, mem_insert_iff, or_iff_not_imp_left] using fun x (hx : x ∈ mulSupport f) =>
  mem_image_of_mem f hx
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
c : M
hc : c ≠ 1
⊢ (mulSupport fun x => c) = univ
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
c : M
hc : c ≠ 1
x : α
⊢ (x ∈ mulSupport fun x => c) ↔ x ∈ univ
[PROOFSTEP]
simp [hc]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
op : M → N → P
op1 : op 1 1 = 1
f : α → M
g : α → N
x : α
hx : x ∈ mulSupport fun x => op (f x) (g x)
hf : f x = 1
hg : g x = 1
⊢ (fun x => op (f x) (g x)) x = 1
[PROOFSTEP]
simp only [hf, hg, op1]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ (mulSupport fun x => ⨆ (i : ι), f i x) ⊆ ⋃ (i : ι), mulSupport (f i)
[PROOFSTEP]
rw [mulSupport_subset_iff']
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ ∀ (x : α), ¬x ∈ ⋃ (i : ι), mulSupport (f i) → ⨆ (i : ι), f i x = 1
[PROOFSTEP]
simp only [mem_iUnion, not_exists, nmem_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ ∀ (x : α), (∀ (x_1 : ι), f x_1 x = 1) → ⨆ (i : ι), f i x = 1
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝⁴ : One M
inst✝³ : One N
inst✝² : One P
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
x : α
hx : ∀ (x_1 : ι), f x_1 x = 1
⊢ ⨆ (i : ι), f i x = 1
[PROOFSTEP]
simp only [hx, ciSup_const]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
g : M → N
hg : g 1 = 1
f : α → M
x : α
h : f x = 1
⊢ (g ∘ f) x = 1
[PROOFSTEP]
simp only [(· ∘ ·), *]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
g : M → N
f : α → M
hg : ∀ {x : M}, x ∈ range f → (g x = 1 ↔ x = 1)
x : α
⊢ (g ∘ f) x = 1 ↔ f x = 1
[PROOFSTEP]
rw [Function.comp, hg (mem_range_self x)]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
g : α → N
x : α
⊢ (x ∈ mulSupport fun x => (f x, g x)) ↔ x ∈ mulSupport f ∪ mulSupport g
[PROOFSTEP]
simp only [mulSupport, not_and_or, mem_union, mem_setOf_eq, Prod.mk_eq_one, Ne.def]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M × N
⊢ mulSupport f = (mulSupport fun x => (f x).fst) ∪ mulSupport fun x => (f x).snd
[PROOFSTEP]
simp only [← mulSupport_prod_mk, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α × β → M
a : α
x : β
hx : x ∈ mulSupport fun b => f (a, b)
⊢ (a, x) ∈ mulSupport f ∧ (a, x).snd = x
[PROOFSTEP]
simpa using hx
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : Monoid M
f : α → M
n : ℕ
⊢ (mulSupport fun x => f x ^ n) ⊆ mulSupport f
[PROOFSTEP]
induction' n with n hfn
[GOAL]
case zero
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : Monoid M
f : α → M
⊢ (mulSupport fun x => f x ^ Nat.zero) ⊆ mulSupport f
[PROOFSTEP]
simp [pow_zero, mulSupport_one]
[GOAL]
case succ
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : Monoid M
f : α → M
n : ℕ
hfn : (mulSupport fun x => f x ^ n) ⊆ mulSupport f
⊢ (mulSupport fun x => f x ^ Nat.succ n) ⊆ mulSupport f
[PROOFSTEP]
simpa only [pow_succ] using (mulSupport_mul f _).trans (union_subset Subset.rfl hfn)
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : DivisionMonoid G
f g : α → G
⊢ (fun a b => a * b⁻¹) 1 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : MulZeroClass R
f g : α → R
x : α
hfg : x ∈ support fun x => f x * g x
hf : f x = 0
⊢ (fun x => f x * g x) x = 0
[PROOFSTEP]
simp only [hf, zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : MulZeroClass R
f g : α → R
x : α
hfg : x ∈ support fun x => f x * g x
hg : g x = 0
⊢ (fun x => f x * g x) x = 0
[PROOFSTEP]
simp only [hg, mul_zero]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : AddMonoid A
inst✝¹ : Monoid B
inst✝ : DistribMulAction B A
b : B
f : α → A
x : α
hbf : x ∈ support (b • f)
hf : f x = 0
⊢ (b • f) x = 0
[PROOFSTEP]
rw [Pi.smul_apply, hf, smul_zero]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : Zero M
inst✝¹ : Zero β
inst✝ : SMulWithZero M β
f : α → M
g : α → β
x : α
hfg : x ∈ support (f • g)
hf : f x = 0
⊢ (f • g) x = 0
[PROOFSTEP]
rw [Pi.smul_apply', hf, zero_smul]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
c : R
g : α → M
hc : c ≠ 0
x : α
⊢ x ∈ support (c • g) ↔ x ∈ support g
[PROOFSTEP]
simp only [hc, mem_support, Pi.smul_apply, Ne.def, smul_eq_zero, false_or_iff]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : GroupWithZero G₀
f g : α → G₀
⊢ (support fun x => f x / g x) = support f ∩ support g
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : CommMonoid M
s : Finset α
f : α → β → M
⊢ (mulSupport fun x => ∏ i in s, f i x) ⊆ ⋃ (i : α) (_ : i ∈ s), mulSupport (f i)
[PROOFSTEP]
rw [mulSupport_subset_iff']
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : CommMonoid M
s : Finset α
f : α → β → M
⊢ ∀ (x : β), ¬x ∈ ⋃ (i : α) (_ : i ∈ s), mulSupport (f i) → ∏ i in s, f i x = 1
[PROOFSTEP]
simp only [mem_iUnion, not_exists, nmem_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝ : CommMonoid M
s : Finset α
f : α → β → M
⊢ ∀ (x : β), (∀ (x_1 : α), x_1 ∈ s → f x_1 x = 1) → ∏ i in s, f i x = 1
[PROOFSTEP]
exact fun x => Finset.prod_eq_one
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝² : CommMonoidWithZero A
inst✝¹ : NoZeroDivisors A
inst✝ : Nontrivial A
s : Finset α
f : α → β → A
x : β
⊢ (x ∈ support fun x => ∏ i in s, f i x) ↔ x ∈ ⋂ (i : α) (_ : i ∈ s), support (f i)
[PROOFSTEP]
simp [support, Ne.def, Finset.prod_eq_zero_iff, mem_setOf_eq, Set.mem_iInter, not_exists]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
R : Type u_8
S : Type u_9
G : Type u_10
M₀ : Type u_11
G₀ : Type u_12
ι : Sort u_13
inst✝¹ : One R
inst✝ : AddGroup R
f : α → R
⊢ mulSupport (1 - f) = support f
[PROOFSTEP]
rw [sub_eq_add_neg, mulSupport_one_add', support_neg']
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
f : α → M
s : Set β
g : β → α
⊢ g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g))
[PROOFSTEP]
rw [mulSupport_comp_eq_preimage f g, image_inter_preimage]
[GOAL]
A : Type u_1
B : Type u_2
inst✝¹ : DecidableEq A
inst✝ : One B
a : A
b : B
⊢ mulSupport (mulSingle a 1) = ∅
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
inst✝¹ : DecidableEq A
inst✝ : One B
a : A
b : B
h : b ≠ 1
x : A
hx : x = a
⊢ x ∈ mulSupport (mulSingle a b)
[PROOFSTEP]
rwa [mem_mulSupport, hx, mulSingle_eq_same]
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : DecidableEq A
inst✝¹ : One B
a : A
b : B
inst✝ : DecidableEq B
⊢ mulSupport (mulSingle a b) = if b = 1 then ∅ else {a}
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
A : Type u_1
B : Type u_2
inst✝² : DecidableEq A
inst✝¹ : One B
a : A
b : B
inst✝ : DecidableEq B
h : b = 1
⊢ mulSupport (mulSingle a b) = ∅
[PROOFSTEP]
simp [h]
[GOAL]
case neg
A : Type u_1
B : Type u_2
inst✝² : DecidableEq A
inst✝¹ : One B
a : A
b : B
inst✝ : DecidableEq B
h : ¬b = 1
⊢ mulSupport (mulSingle a b) = {a}
[PROOFSTEP]
simp [h]
[GOAL]
A : Type u_1
B : Type u_2
inst✝¹ : DecidableEq A
inst✝ : One B
a : A
b b' : B
hb : b ≠ 1
hb' : b' ≠ 1
i j : A
⊢ Disjoint (mulSupport (mulSingle i b)) (mulSupport (mulSingle j b')) ↔ i ≠ j
[PROOFSTEP]
rw [mulSupport_mulSingle_of_ne hb, mulSupport_mulSingle_of_ne hb', disjoint_singleton]
