α : Type u_1
β : Type ?u.366
γ : Type ?u.369
ι : Type ?u.372
M : Type u_2
M' : Type ?u.378
N : Type ?u.381
P : Type ?u.384
G : Type ?u.387
H : Type ?u.390
R : Type ?u.393
S : Type ?u.396
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ a_1,
      ↑f a_1 ≠ 0 ∧
        ↑{ toFun := fun a => (a, ↑f a),
                inj' := (_ : ∀ (x x_1 : α), (fun a => (a, ↑f a)) x = (fun a => (a, ↑f a)) x_1 → x = x_1) }
            a_1 =
          (a, m)) ↔
    ↑f a = m ∧ m ≠ 0
α : Type u_1
β : Type ?u.366
γ : Type ?u.369
ι : Type ?u.372
M : Type u_2
M' : Type ?u.378
N : Type ?u.381
P : Type ?u.384
G : Type ?u.387
H : Type ?u.390
R : Type ?u.393
S : Type ?u.396
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (a, m) ∈ graph f ↔ ↑f a = m ∧ m ≠ 0
simp_rw [graph, mem_map, mem_support_iff]
case mp
α : Type u_1
β : Type ?u.366
γ : Type ?u.369
ι : Type ?u.372
M : Type u_2
M' : Type ?u.378
N : Type ?u.381
P : Type ?u.384
G : Type ?u.387
H : Type ?u.390
R : Type ?u.393
S : Type ?u.396
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ a_1,
      ↑f a_1 ≠ 0 ∧
        ↑{ toFun := fun a => (a, ↑f a),
                inj' := (_ : ∀ (x x_1 : α), (fun a => (a, ↑f a)) x = (fun a => (a, ↑f a)) x_1 → x = x_1) }
            a_1 =
          (a, m)) →
    ↑f a = m ∧ m ≠ 0

case mpr
α : Type u_1
β : Type ?u.366
γ : Type ?u.369
ι : Type ?u.372
M : Type u_2
M' : Type ?u.378
N : Type ?u.381
P : Type ?u.384
G : Type ?u.387
H : Type ?u.390
R : Type ?u.393
S : Type ?u.396
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ ↑f a = m ∧ m ≠ 0 →
    ∃ a_2,
      ↑f a_2 ≠ 0 ∧
        ↑{ toFun := fun a => (a, ↑f a),
                inj' := (_ : ∀ (x x_1 : α), (fun a => (a, ↑f a)) x = (fun a => (a, ↑f a)) x_1 → x = x_1) }
            a_2 =
          (a, m)
α : Type u_1
β : Type ?u.366
γ : Type ?u.369
ι : Type ?u.372
M : Type u_2
M' : Type ?u.378
N : Type ?u.381
P : Type ?u.384
G : Type ?u.387
H : Type ?u.390
R : Type ?u.393
S : Type ?u.396
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ a_1,
      ↑f a_1 ≠ 0 ∧
        ↑{ toFun := fun a => (a, ↑f a),
                inj' := (_ : ∀ (x x_1 : α), (fun a => (a, ↑f a)) x = (fun a => (a, ↑f a)) x_1 → x = x_1) }
            a_1 =
          (a, m)) ↔
    ↑f a = m ∧ m ≠ 0
constructor
case mp.intro.intro.refl
α : Type u_1
β : Type ?u.366
γ : Type ?u.369
ι : Type ?u.372
M : Type u_2
M' : Type ?u.378
N : Type ?u.381
P : Type ?u.384
G : Type ?u.387
H : Type ?u.390
R : Type ?u.393
S : Type ?u.396
inst✝ : Zero M
a : α
f : α →₀ M
ha : ↑f a ≠ 0
⊢ ↑f a = ↑f a ∧ ↑f a ≠ 0
case mp
α : Type u_1
β : Type ?u.366
γ : Type ?u.369
ι : Type ?u.372
M : Type u_2
M' : Type ?u.378
N : Type ?u.381
P : Type ?u.384
G : Type ?u.387
H : Type ?u.390
R : Type ?u.393
S : Type ?u.396
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ a_1,
      ↑f a_1 ≠ 0 ∧
        ↑{ toFun := fun a => (a, ↑f a),
                inj' := (_ : ∀ (x x_1 : α), (fun a => (a, ↑f a)) x = (fun a => (a, ↑f a)) x_1 → x = x_1) }
            a_1 =
          (a, m)) →
    ↑f a = m ∧ m ≠ 0
rintro ⟨b, ha, rfl, -⟩
no goals
case mp.intro.intro.refl
α : Type u_1
β : Type ?u.366
γ : Type ?u.369
ι : Type ?u.372
M : Type u_2
M' : Type ?u.378
N : Type ?u.381
P : Type ?u.384
G : Type ?u.387
H : Type ?u.390
R : Type ?u.393
S : Type ?u.396
inst✝ : Zero M
a : α
f : α →₀ M
ha : ↑f a ≠ 0
⊢ ↑f a = ↑f a ∧ ↑f a ≠ 0
exact ⟨rfl, ha⟩
case mpr.intro
α : Type u_1
β : Type ?u.366
γ : Type ?u.369
ι : Type ?u.372
M : Type u_2
M' : Type ?u.378
N : Type ?u.381
P : Type ?u.384
G : Type ?u.387
H : Type ?u.390
R : Type ?u.393
S : Type ?u.396
inst✝ : Zero M
a : α
f : α →₀ M
ha : ↑f a ≠ 0
⊢ ∃ a_1,
    ↑f a_1 ≠ 0 ∧
      ↑{ toFun := fun a => (a, ↑f a),
              inj' := (_ : ∀ (x x_1 : α), (fun a => (a, ↑f a)) x = (fun a => (a, ↑f a)) x_1 → x = x_1) }
          a_1 =
        (a, ↑f a)
case mpr
α : Type u_1
β : Type ?u.366
γ : Type ?u.369
ι : Type ?u.372
M : Type u_2
M' : Type ?u.378
N : Type ?u.381
P : Type ?u.384
G : Type ?u.387
H : Type ?u.390
R : Type ?u.393
S : Type ?u.396
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ ↑f a = m ∧ m ≠ 0 →
    ∃ a_2,
      ↑f a_2 ≠ 0 ∧
        ↑{ toFun := fun a => (a, ↑f a),
                inj' := (_ : ∀ (x x_1 : α), (fun a => (a, ↑f a)) x = (fun a => (a, ↑f a)) x_1 → x = x_1) }
            a_2 =
          (a, m)
rintro ⟨rfl, ha⟩
no goals
case mpr.intro
α : Type u_1
β : Type ?u.366
γ : Type ?u.369
ι : Type ?u.372
M : Type u_2
M' : Type ?u.378
N : Type ?u.381
P : Type ?u.384
G : Type ?u.387
H : Type ?u.390
R : Type ?u.393
S : Type ?u.396
inst✝ : Zero M
a : α
f : α →₀ M
ha : ↑f a ≠ 0
⊢ ∃ a_1,
    ↑f a_1 ≠ 0 ∧
      ↑{ toFun := fun a => (a, ↑f a),
              inj' := (_ : ∀ (x x_1 : α), (fun a => (a, ↑f a)) x = (fun a => (a, ↑f a)) x_1 → x = x_1) }
          a_1 =
        (a, ↑f a)
exact ⟨a, ha, rfl⟩