-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
lemma mem_span_iff {s : Set R} {x} :
    x ∈ span s ↔ ∀ (I : TwoSidedIdeal R), s ⊆ I → x ∈ I

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
h : x ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} }
I : TwoSidedIdeal R
hI : s ⊆ ↑I
⊢ x ∈ I

Tactic:
refine sInf_le (α := RingCon R) ?_ h

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
h : x ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} }
I : TwoSidedIdeal R
hI : s ⊆ ↑I
⊢ I.ringCon ∈ {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y}

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
h : x ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} }
I : TwoSidedIdeal R
hI : s ⊆ ↑I
⊢ I.ringCon ∈ {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y}

Tactic:
intro x y hxy

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x✝ : R
h : x✝ ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} }
I : TwoSidedIdeal R
hI : s ⊆ ↑I
x y : R
hxy : x - y ∈ s
⊢ I.ringCon x y

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ x ∈ span s → ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I

Tactic:
delta span

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ x ∈ { ringCon := ringConGen fun a b => a - b ∈ s } → ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x✝ : R
h : x✝ ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} }
I : TwoSidedIdeal R
hI : s ⊆ ↑I
x y : R
hxy : x - y ∈ s
⊢ I.ringCon x y

Tactic:
specialize hI hxy

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x✝ : R
h : x✝ ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} }
I : TwoSidedIdeal R
x y : R
hxy : x - y ∈ s
hI : x - y ∈ ↑I
⊢ I.ringCon x y

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x✝ : R
h : x✝ ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} }
I : TwoSidedIdeal R
x y : R
hxy : x - y ∈ s
hI : x - y ∈ ↑I
⊢ I.ringCon x y

Tactic:
rwa [SetLike.mem_coe, ← rel_iff] at hI

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ x ∈ { ringCon := ringConGen fun a b => a - b ∈ s } → ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I

Tactic:
rw [RingCon.ringConGen_eq]

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ x ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} } → ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ x ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} } → ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I

Tactic:
intro h I hI

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
h : x ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} }
I : TwoSidedIdeal R
hI : s ⊆ ↑I
⊢ x ∈ I

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ x ∈ span s ↔ ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I

Tactic:
refine ⟨?_, fun h => h _ subset_span⟩

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ x ∈ span s → ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I