-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
h₁ :
  (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (a_2 : ↥(s.finsuppAntidiag a_1.2)),
        Membership.mem (γ := Finset ↥(s.finsuppAntidiag a_1.2)) (attach (s.finsuppAntidiag a_1.2)) a_2 ∧
          ({ toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ } :
                (a : ↥(s.finsuppAntidiag a_1.2)) → ι →₀ μ)
              a_2 =
            f
h₂ :
  (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (a_2 : ↥(s.finsuppAntidiag a_1.2)),
        True ∧
          ({ toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ } :
                (a : ↥(s.finsuppAntidiag a_1.2)) → ι →₀ μ)
              a_2 =
            f
h₃ :
  (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (a_2 : ↥(s.finsuppAntidiag a_1.2)),
        ({ toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ } :
              (a : ↥(s.finsuppAntidiag a_1.2)) → ι →₀ μ)
            a_2 =
          f
h₄ :
  (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (a_2 : ι →₀ μ) (b : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag a_1.2) a_2),
        ({ toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ } :
              (a : ↥(s.finsuppAntidiag a_1.2)) → ι →₀ μ)
            (Subtype.mk (p := fun (a : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag a_1.2) a) a_2
              b) =
          f
h₅ :
  (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (a_2 : ι →₀ μ) (_ : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag a_1.2) a_2), a_2.update a a_1.1 = f
h₆ :
  (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (a_2 : ι →₀ μ), Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag a_1.2) a_2 ∧ a_2.update a a_1.1 = f
h₇ :
  (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (a_2 : ι →₀ μ), a_2.update a a_1.1 = f ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag a_1.2) a_2
⊢ (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      Membership.mem (γ := Finset (ι →₀ μ))
        (map (α := ↥(s.finsuppAntidiag a_1.2))
          { toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ }
          (attach (s.finsuppAntidiag a_1.2)))
        f

Tactic:
simp_rw [mem_map, mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk, exists_prop, and_comm,
    eq_comm]

Premises used: Finset.mem_attach, Subtype.exists, and_comm, exists_prop, eq_comm, Function.Embedding.coeFn_mk, Finset.mem_map, true_and