-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubring R) (closure s) y → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p x 0 hx ⋯
neg_left :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p (-x) y ⋯ hy
neg_right :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x
hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y
mem : ∀ (z : R) (hz : z ∈ s), p x z hx ⋯
zero : p x 0 hx ⋯
mul :
  ∀ (x_1 y : R) (hx_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) x_1)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y) (h₁ : p x x_1 hx hx_1) (h₂ : p x y hx hy),
    p x (x_1 * y) hx ⋯
add :
  ∀ (x_1 y : R) (hx_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) x_1)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y) (h₁ : p x x_1 hx hx_1) (h₂ : p x y hx hy),
    p x (x_1 + y) hx ⋯
neg :
  ∀ (x_1 : R) (hx_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) x_1) (h : p x x_1 hx hx_1), p x (-x_1) hx ⋯
⊢ p x y hx hy

Tactic:
induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | zero => exact zero_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | neg _ _ h => exact neg_left _ _ _ _ h
  | zero => exact zero_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
  | neg _ _ h => exact neg_right _ _ _ _ h