α : Type u_3
β : Type u_2
γ : Type ?u.301425
ι : Type ?u.301428
M : Type u_1
M' : Type ?u.301434
N : Type ?u.301437
P : Type ?u.301440
G : Type ?u.301443
H : Type ?u.301446
R : Type ?u.301449
S : Type ?u.301452
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ { support := preimage l.support f (_ : Set.InjOn f (f ⁻¹' ↑l.support)), toFun := fun a => ↑l (f a),
          mem_support_toFun :=
            (_ :
              ∀ (a : α),
                a ∈ preimage l.support f (_ : Set.InjOn f (f ⁻¹' ↑l.support)) ↔ (fun a => ↑l (f a)) a ≠ 0) }.support =
      ∅ →
    l.support = ∅
α : Type u_3
β : Type u_2
γ : Type ?u.301425
ι : Type ?u.301428
M : Type u_1
M' : Type ?u.301434
N : Type ?u.301437
P : Type ?u.301440
G : Type ?u.301443
H : Type ?u.301446
R : Type ?u.301449
S : Type ?u.301452
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ comapDomain f l (_ : Set.InjOn f (f ⁻¹' ↑l.support)) = 0 → l = 0
rw [← support_eq_empty, ← support_eq_empty, comapDomain]
α : Type u_3
β : Type u_2
γ : Type ?u.301425
ι : Type ?u.301428
M : Type u_1
M' : Type ?u.301434
N : Type ?u.301437
P : Type ?u.301440
G : Type ?u.301443
H : Type ?u.301446
R : Type ?u.301449
S : Type ?u.301452
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ (∀ (a : α), ¬f a ∈ l.support) → ∀ (a : β), ¬a ∈ l.support
α : Type u_3
β : Type u_2
γ : Type ?u.301425
ι : Type ?u.301428
M : Type u_1
M' : Type ?u.301434
N : Type ?u.301437
P : Type ?u.301440
G : Type ?u.301443
H : Type ?u.301446
R : Type ?u.301449
S : Type ?u.301452
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ { support := preimage l.support f (_ : Set.InjOn f (f ⁻¹' ↑l.support)), toFun := fun a => ↑l (f a),
          mem_support_toFun :=
            (_ :
              ∀ (a : α),
                a ∈ preimage l.support f (_ : Set.InjOn f (f ⁻¹' ↑l.support)) ↔ (fun a => ↑l (f a)) a ≠ 0) }.support =
      ∅ →
    l.support = ∅
simp only [Finset.ext_iff, Finset.not_mem_empty, iff_false_iff, mem_preimage]
α : Type u_3
β : Type u_2
γ : Type ?u.301425
ι : Type ?u.301428
M : Type u_1
M' : Type ?u.301434
N : Type ?u.301437
P : Type ?u.301440
G : Type ?u.301443
H : Type ?u.301446
R : Type ?u.301449
S : Type ?u.301452
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
h : ∀ (a : α), ¬f a ∈ l.support
a : β
ha : a ∈ l.support
⊢ False
α : Type u_3
β : Type u_2
γ : Type ?u.301425
ι : Type ?u.301428
M : Type u_1
M' : Type ?u.301434
N : Type ?u.301437
P : Type ?u.301440
G : Type ?u.301443
H : Type ?u.301446
R : Type ?u.301449
S : Type ?u.301452
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ (∀ (a : α), ¬f a ∈ l.support) → ∀ (a : β), ¬a ∈ l.support
intro h a ha
case intro
α : Type u_3
β : Type u_2
γ : Type ?u.301425
ι : Type ?u.301428
M : Type u_1
M' : Type ?u.301434
N : Type ?u.301437
P : Type ?u.301440
G : Type ?u.301443
H : Type ?u.301446
R : Type ?u.301449
S : Type ?u.301452
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
h : ∀ (a : α), ¬f a ∈ l.support
a : β
ha : a ∈ l.support
b : α
hb : b ∈ f ⁻¹' ↑l.support ∧ f b = a
⊢ False
α : Type u_3
β : Type u_2
γ : Type ?u.301425
ι : Type ?u.301428
M : Type u_1
M' : Type ?u.301434
N : Type ?u.301437
P : Type ?u.301440
G : Type ?u.301443
H : Type ?u.301446
R : Type ?u.301449
S : Type ?u.301452
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
h : ∀ (a : α), ¬f a ∈ l.support
a : β
ha : a ∈ l.support
⊢ False
cases' hf.2.2 ha with b hb
no goals
case intro
α : Type u_3
β : Type u_2
γ : Type ?u.301425
ι : Type ?u.301428
M : Type u_1
M' : Type ?u.301434
N : Type ?u.301437
P : Type ?u.301440
G : Type ?u.301443
H : Type ?u.301446
R : Type ?u.301449
S : Type ?u.301452
inst✝ : AddCommMonoid M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
h : ∀ (a : α), ¬f a ∈ l.support
a : β
ha : a ∈ l.support
b : α
hb : b ∈ f ⁻¹' ↑l.support ∧ f b = a
⊢ False
exact h b (hb.2.symm ▸ ha)