-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubring.Basic (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 y : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x_1
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) y
mul :
  ∀ (x y : R) (hx : x ∈ (↑(Subsemigroup.closure s) : Set R)) (hy : y ∈ (↑(Subsemigroup.closure s) : Set R)),
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x * y)
mul₁ :
  ∀ (x : R),
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x →
      Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (0 * x)
mul₂ :
  ∀ (x : R),
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x →
      Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x * 0)
mul₃ :
  ∀ (x y z : R),
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x →
      Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) y →
        Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) z →
          ∀ (h₁ : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x * z))
            (h₂ :
              Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (y * z)),
            Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) ((x + y) * z)
mul₄ :
  ∀ (y z x : R),
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) y →
      Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) z →
        Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x →
          ∀ (h₁ : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x * y))
            (h₂ :
              Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x * z)),
            Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x * (y + z))
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x_1 * y)
have mul₅ : ∀ (x y : R),
  Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x →
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) y →
      ∀ (h : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x * y)),
        Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (-x * y)
Tactic: induction hx, hy using AddSubgroup.closure_induction₂ with
      | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
      | zero_left => simp
      | zero_right => simp
      | add_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
      | add_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
      | neg_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
      | neg_right _ _ _ _ h => simpa [mul_neg] using neg_mem h
Cleared hypotheses: hx, hy