-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero S
inst_2 : EquivLike F M₀ S
inst_3 : MulEquivClass F M₀ S
h_1 : F
h : M₀ ≃* S := (↑h_1 : M₀ ≃* S)
x : S
h₁ : Membership.mem (γ := Submonoid S) (Submonoid.comap h.symm M₀⁰) x ↔ Membership.mem (γ := Submonoid S) S⁰ x
h₂ :
  Membership.mem (α := M₀) (γ := Submonoid M₀) M₀⁰ ((h.symm : (a : S) → M₀) x : M₀) ↔
    Membership.mem (γ := Submonoid S) S⁰ x
h₃ :
  ((∀ (x_1 : M₀), HMul.hMul (α := M₀) ((h.symm : (a : S) → M₀) x : M₀) x_1 = 0 → x_1 = 0) ∧
      ∀ (x_1 : M₀), HMul.hMul (β := M₀) x_1 ((h.symm : (a : S) → M₀) x : M₀) = 0 → x_1 = 0) ↔
    (∀ (x_1 : S), x * x_1 = 0 → x_1 = 0) ∧ ∀ (x_1 : S), x_1 * x = 0 → x_1 = 0
h₄ :
  ((∀ (a : S),
        HMul.hMul (α := M₀) (β := M₀) ((h.symm : (a : S) → M₀) x : M₀) ((h.symm.toEquiv : (a : S) → M₀) a : M₀) = 0 →
          Eq.{u_4 + 1} (α := M₀) ((h.symm.toEquiv : (a : S) → M₀) a : M₀) (0 : M₀)) ∧
      ∀ (a : S),
        HMul.hMul (α := M₀) (β := M₀) ((h.symm.toEquiv : (a : S) → M₀) a : M₀) ((h.symm : (a : S) → M₀) x : M₀) = 0 →
          Eq.{u_4 + 1} (α := M₀) ((h.symm.toEquiv : (a : S) → M₀) a : M₀) (0 : M₀)) ↔
    (∀ (x_1 : S), x * x_1 = 0 → x_1 = 0) ∧ ∀ (x_1 : S), x_1 * x = 0 → x_1 = 0
h₅ :
  ((∀ (a : S),
        HMul.hMul (α := M₀) (β := M₀) ((h.symm : (a : S) → M₀) x : M₀) (((↑h.symm : S ≃ M₀) : (a : S) → M₀) a : M₀) =
            0 →
          Eq.{u_4 + 1} (α := M₀) (((↑h.symm : S ≃ M₀) : (a : S) → M₀) a : M₀) (0 : M₀)) ∧
      ∀ (a : S),
        HMul.hMul (α := M₀) (β := M₀) (((↑h.symm : S ≃ M₀) : (a : S) → M₀) a : M₀) ((h.symm : (a : S) → M₀) x : M₀) =
            0 →
          Eq.{u_4 + 1} (α := M₀) (((↑h.symm : S ≃ M₀) : (a : S) → M₀) a : M₀) (0 : M₀)) ↔
    (∀ (x_1 : S), x * x_1 = 0 → x_1 = 0) ∧ ∀ (x_1 : S), x_1 * x = 0 → x_1 = 0
h₆ :
  ((∀ (a : S),
        HMul.hMul (α := M₀) (β := M₀) ((h.symm : (a : S) → M₀) x : M₀) ((h.symm : (a : S) → M₀) a : M₀) = 0 →
          Eq.{u_4 + 1} (α := M₀) ((h.symm : (a : S) → M₀) a : M₀) (0 : M₀)) ∧
      ∀ (a : S),
        HMul.hMul (α := M₀) (β := M₀) ((h.symm : (a : S) → M₀) a : M₀) ((h.symm : (a : S) → M₀) x : M₀) = 0 →
          Eq.{u_4 + 1} (α := M₀) ((h.symm : (a : S) → M₀) a : M₀) (0 : M₀)) ↔
    (∀ (x_1 : S), x * x_1 = 0 → x_1 = 0) ∧ ∀ (x_1 : S), x_1 * x = 0 → x_1 = 0
h₇ :
  ((∀ (a : S),
        Eq.{u_4 + 1} (α := M₀) ((h.symm : (a : S) → M₀) (x * a) : M₀) (0 : M₀) →
          Eq.{u_4 + 1} (α := M₀) ((h.symm : (a : S) → M₀) a : M₀) (0 : M₀)) ∧
      ∀ (a : S),
        Eq.{u_4 + 1} (α := M₀) ((h.symm : (a : S) → M₀) (a * x) : M₀) (0 : M₀) →
          Eq.{u_4 + 1} (α := M₀) ((h.symm : (a : S) → M₀) a : M₀) (0 : M₀)) ↔
    (∀ (x_1 : S), x * x_1 = 0 → x_1 = 0) ∧ ∀ (x_1 : S), x_1 * x = 0 → x_1 = 0
⊢ Membership.mem (γ := Submonoid S) (Submonoid.map h M₀⁰) x ↔ Membership.mem (γ := Submonoid S) S⁰ x

Tactic:
simp_rw [Submonoid.map_equiv_eq_comap_symm, Submonoid.mem_comap, mem_nonZeroDivisors_iff,
    ← h.symm.forall_congr_right, h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv, ← map_mul,
    map_eq_zero_iff _ h.symm.injective]

Premises used: MulEquivClass.map_mul, mem_nonZeroDivisors_iff, Submonoid.mem_comap, MulEquiv.toEquiv, MulEquiv.toEquiv_eq_coe, Submonoid.map_equiv_eq_comap_symm, map_eq_zero_iff, MulEquiv.coe_toEquiv, Equiv.forall_congr_right, MulEquiv.symm, MulEquiv.injective