-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
/-- If `s : Set R` is absorbing under multiplication, then its `TwoSidedIdeal.span` coincides with
its `AddSubgroup.closure`, as sets. -/
lemma mem_span_iff_mem_addSubgroup_closure_absorbing {s : Set R}
    (h_left : ∀ x y, y ∈ s → x * y ∈ s) (h_right : ∀ y x, y ∈ s → y * x ∈ s) {z : R} :
    z ∈ span s ↔ z ∈ closure s

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (∀ (I : TwoSidedIdeal R), s ⊆ ↑I → z ∈ I) ↔ z ∈ I

Tactic:
refine ⟨fun h ↦ h I fun x hx ↦ ?mem_closure_of_forall, fun hz J hJ ↦ ?mem_ideal_of_subset⟩

Result:
case mem_closure_of_forall
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
h : ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → z ∈ I
x : R
hx : x ∈ s
⊢ x ∈ ↑I

case mem_ideal_of_subset
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
hz : z ∈ I
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
⊢ z ∈ J

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y : R
hy : y ∈ closure s
this : (AddMonoidHom.mulLeft x) y ∈ closure (⇑(AddMonoidHom.mulLeft x) '' s)
⊢ x * y ∈ closure s

Tactic:
refine closure_mono ?_ this

Result:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y : R
hy : y ∈ closure s
this : (AddMonoidHom.mulLeft x) y ∈ closure (⇑(AddMonoidHom.mulLeft x) '' s)
⊢ ⇑(AddMonoidHom.mulLeft x) '' s ⊆ s

Proof state:
case mem_ideal_of_subset
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
hz : z ∈ I
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
⊢ z ∈ J

Tactic:
case mem_ideal_of_subset =>
  simp only [I, SetLike.mem_coe, mem_mk'] at hz
  induction hz using closure_induction with
  | mem x hx => exact hJ hx
  | one => exact zero_mem _
  | mul x y _ _ hx hy => exact J.add_mem hx hy
  | inv x _ hx => exact J.neg_mem hx

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
y x : R
hy : y ∈ closure s
this : (AddMonoidHom.mulRight x) y ∈ closure (⇑(AddMonoidHom.mulRight x) '' s)
⊢ y * x ∈ closure s

Tactic:
refine closure_mono ?_ this

Result:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
y x : R
hy : y ∈ closure s
this : (AddMonoidHom.mulRight x) y ∈ closure (⇑(AddMonoidHom.mulRight x) '' s)
⊢ ⇑(AddMonoidHom.mulRight x) '' s ⊆ s

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
⊢ z ∈ span s ↔ z ∈ closure s

Tactic:
have h_right' {y x} (hy : y ∈ closure s) : y * x ∈ closure s := by
  have := (AddMonoidHom.mulRight x).map_closure s ▸ mem_map_of_mem _ hy
  refine closure_mono ?_ this
  rintro - ⟨y, hy, rfl⟩
  exact h_right y x hy

Result:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
⊢ z ∈ span s ↔ z ∈ closure s

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ z ∈ span s ↔ z ∈ closure s

Tactic:
suffices z ∈ span s ↔ z ∈ I by simpa only [I, mem_mk', SetLike.mem_coe]

Result:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ z ∈ span s ↔ z ∈ I

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
y x : R
hy : y ∈ closure s
this : (AddMonoidHom.mulRight x) y ∈ closure (⇑(AddMonoidHom.mulRight x) '' s)
⊢ ⇑(AddMonoidHom.mulRight x) '' s ⊆ s

Tactic:
rintro - ⟨y, hy, rfl⟩

Result:
case intro.intro
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
y✝ x : R
hy✝ : y✝ ∈ closure s
this : (AddMonoidHom.mulRight x) y✝ ∈ closure (⇑(AddMonoidHom.mulRight x) '' s)
y : R
hy : y ∈ s
⊢ (AddMonoidHom.mulRight x) y ∈ s

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
⊢ z ∈ span s ↔ z ∈ closure s

Tactic:
let I : TwoSidedIdeal R := .mk' (closure s) (AddSubgroup.zero_mem _)
  (AddSubgroup.add_mem _) (AddSubgroup.neg_mem _) h_left' h_right'

Result:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ z ∈ span s ↔ z ∈ closure s

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
hz : z ∈ closure s
⊢ z ∈ J

Tactic:
induction hz using closure_induction with
| mem x hx => exact hJ hx
| one => exact zero_mem _
| mul x y _ _ hx hy => exact J.add_mem hx hy
| inv x _ hx => exact J.neg_mem hx

Result:
no goals

Proof state:
case one
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
⊢ 0 ∈ J

Tactic:
exact zero_mem _

Result:
no goals