awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon : TwoSidedIdeal R } ≤ J
have rw : { ringCon := I.ringCon ⊓ J.ringCon : TwoSidedIdeal R }.ringCon ≤ J.ringCon
Tactic: rw [ringCon_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I ≤ J
h2 : I ≤ K
⊢ I ≤ { ringCon := J.ringCon ⊓ K.ringCon }
have rw : ∀ (h1 : I.ringCon ≤ J.ringCon) (h2 : I.ringCon ≤ K.ringCon), I.ringCon ≤ { ringCon := J.ringCon ⊓ K.ringCon }.ringCon
Tactic: rw [ringCon_le_iff] at h1 h2 ⊢
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ Eq.{u_1 + 1} (α := RingCon R) (sSup (ringCon '' Set.range fun (i : ι) ↦ I i))
    (sSup (Set.range fun (i : ι) ↦ (I i).ringCon))
have e_a : Eq.{u_1 + 1} (α := Set (RingCon R)) (ringCon '' Set.range fun (i : ι) ↦ I i) (Set.range fun (i : ι) ↦ (I i).ringCon)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ Eq.{u_1 + 1} (α := Set (RingCon R)) (ringCon '' Set.range fun (i : ι) ↦ I i) (Set.range fun (i : ι) ↦ (I i).ringCon)
have e_a : ∀ (x : RingCon R),
  Membership.mem (γ := Set (RingCon R)) (ringCon '' Set.range fun (i : ι) ↦ I i) x ↔
    Membership.mem (γ := Set (RingCon R)) (Set.range fun (i : ι) ↦ (I i).ringCon) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ Eq.{u_1 + 1} (α := RingCon R) (sInf (ringCon '' Set.range fun (i : ι) ↦ I i))
    (sInf (Set.range fun (i : ι) ↦ (I i).ringCon))
have h : Eq.{u_1 + 1} (α := Set (RingCon R)) (ringCon '' Set.range fun (i : ι) ↦ I i) (Set.range fun (i : ι) ↦ (I i).ringCon)
Tactic: congr!
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ Eq.{u_1 + 1} (α := Set (RingCon R)) (ringCon '' Set.range fun (i : ι) ↦ I i) (Set.range fun (i : ι) ↦ (I i).ringCon)
have h : ∀ (x : RingCon R),
  Membership.mem (γ := Set (RingCon R)) (ringCon '' Set.range fun (i : ι) ↦ I i) x ↔
    Membership.mem (γ := Set (RingCon R)) (Set.range fun (i : ι) ↦ (I i).ringCon) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x : TwoSidedIdeal R
⊢ x ≤ ⊤
have rw : x.ringCon ≤ ringCon ⊤
Tactic: rw [ringCon_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x : TwoSidedIdeal R
⊢ ⊥ ≤ x
have rw : ringCon ⊥ ≤ x.ringCon
Tactic: rw [ringCon_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) x ↔ ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → x ∈ I
have refine : Membership.mem (γ := TwoSidedIdeal R) (span s) x → ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → x ∈ I
Tactic: refine ⟨?_, fun h => h _ subset_span⟩
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ Membership.mem (γ := TwoSidedIdeal R) { ringCon := ringConGen fun (a b : R) ↦ a - b ∈ s } x →
    ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → x ∈ I
have rw : Membership.mem (γ := TwoSidedIdeal R)
    { ringCon := sInf {s_1 : RingCon R | ∀ (x y : R), x - y ∈ s → (s_1 : (a : R) → R → Prop) x y} } x →
  ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → x ∈ I
Tactic: rw [RingCon.ringConGen_eq]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
x : R
h :
  Membership.mem (γ := TwoSidedIdeal R)
    { ringCon := sInf {s_1 : RingCon R | ∀ (x y : R), x - y ∈ s → (s_1 : (a : R) → R → Prop) x y} } x
I : TwoSidedIdeal R
hI : s ⊆ (↑I : Set R)
⊢ x ∈ I
have refine : Membership.mem (γ := Set (RingCon R)) {s_1 : RingCon R | ∀ (x y : R), x - y ∈ s → (s_1 : (a : R) → R → Prop) x y}
  I.ringCon
Tactic: refine sInf_le (α := RingCon R) ?_ h
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
x_1 : R
h :
  Membership.mem (γ := TwoSidedIdeal R)
    { ringCon := sInf {s_1 : RingCon R | ∀ (x y : R), x - y ∈ s → (s_1 : (a : R) → R → Prop) x y} } x_1
I : TwoSidedIdeal R
hI : s ⊆ (↑I : Set R)
x y : R
hxy : x - y ∈ s
⊢ (I.ringCon : (a : R) → R → Prop) x y
have hI₁ : x - y ∈ (↑I : Set R)
Tactic: specialize hI hxy
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
x_1 : R
h :
  Membership.mem (γ := TwoSidedIdeal R)
    { ringCon := sInf {s_1 : RingCon R | ∀ (x y : R), x - y ∈ s → (s_1 : (a : R) → R → Prop) x y} } x_1
I : TwoSidedIdeal R
x y : R
hxy : x - y ∈ s
hI : x - y ∈ (↑I : Set R)
⊢ (I.ringCon : (a : R) → R → Prop) x y
have rwa : ∀ (hI : x - y ∈ I), (I.ringCon : (a : R) → R → Prop) x y
Tactic: rwa [SetLike.mem_coe, ← rel_iff] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
x_1 : R
h :
  Membership.mem (γ := TwoSidedIdeal R)
    { ringCon := sInf {s_1 : RingCon R | ∀ (x y : R), x - y ∈ s → (s_1 : (a : R) → R → Prop) x y} } x_1
I : TwoSidedIdeal R
x y : R
hxy : x - y ∈ s
hI : x - y ∈ (↑I : Set R)
rwa : ∀ (hI : x - y ∈ I), (I.ringCon : (a : R) → R → Prop) x y
⊢ (I.ringCon : (a : R) → R → Prop) x y
have rwa₁ : ∀ (hI : (I.ringCon : (a : R) → R → Prop) x y), (I.ringCon : (a : R) → R → Prop) x y
Tactic: rwa [SetLike.mem_coe, ← rel_iff] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
x : R
hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x
⊢ Membership.mem (γ := TwoSidedIdeal R) (span t) x
have rw : ∀ (hx : ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → x ∈ I) (I : TwoSidedIdeal R), t ⊆ (↑I : Set R) → x ∈ I
Tactic: rw [mem_span_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
I : TwoSidedIdeal R
⊢ span s ≤ I ↔ s ⊆ (↑I : Set R)
have rw : LE.le (α := R → R → Prop) (fun (a b : R) ↦ a - b ∈ s) (⇑I.ringCon : (a : R) → R → Prop) ↔ s ⊆ (↑I : Set R)
Tactic: rw [TwoSidedIdeal.ringCon_le_iff, RingCon.gi _ |>.gc]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
F : Type u_3
inst_2 : FunLike F R S
f : F
inst_3 : NonUnitalRingHomClass F R S
I J : TwoSidedIdeal S
h : I ≤ J
⊢ LE.le.{u_1} (α := TwoSidedIdeal R)
    ((fun (I : TwoSidedIdeal S) ↦ ({ ringCon := I.ringCon.comap f } : TwoSidedIdeal R)) I)
    ((fun (I : TwoSidedIdeal S) ↦ ({ ringCon := I.ringCon.comap f } : TwoSidedIdeal R)) J)
have h₁ : (↑I : Set S) ⊆ (↑J : Set S)
Tactic: rw [le_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
F : Type u_3
inst_2 : FunLike F R S
f : F
inst_3 : NonUnitalRingHomClass F R S
I J : TwoSidedIdeal S
h : (↑I : Set S) ⊆ (↑J : Set S)
x : R
⊢ Membership.mem (γ := TwoSidedIdeal R)
      ((fun (I : TwoSidedIdeal S) ↦ ({ ringCon := I.ringCon.comap f } : TwoSidedIdeal R)) I) x →
    Membership.mem (γ := TwoSidedIdeal R)
      ((fun (I : TwoSidedIdeal S) ↦ ({ ringCon := I.ringCon.comap f } : TwoSidedIdeal R)) J) x
have h₁ : Membership.mem (α := S) (↑I : Set S) ((f : (a : R) → S) x : S) →
  Membership.mem (α := S) (↑J : Set S) ((f : (a : R) → S) x : S)
Tactic: specialize @h (f x)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
F : Type u_3
inst_2 : FunLike F R S
f : F
inst_3 : NonUnitalRingHomClass F R S
e : R ≃+* S
⊢ Eq (α := TwoSidedIdeal S →o TwoSidedIdeal S) (OrderHom.comp (β := TwoSidedIdeal R) (comap e.symm) (comap e))
    OrderHom.id
have h : ∀ (x : TwoSidedIdeal S) (x_1 : S),
  Membership.mem (γ := TwoSidedIdeal S)
      ((OrderHom.comp (β := TwoSidedIdeal R) (comap e.symm) (comap e) : (a : TwoSidedIdeal S) → TwoSidedIdeal S) x :
        TwoSidedIdeal S)
      x_1 ↔
    Membership.mem (γ := TwoSidedIdeal S) ((OrderHom.id : (a : TwoSidedIdeal S) → TwoSidedIdeal S) x : TwoSidedIdeal S)
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
F : Type u_3
inst_2 : FunLike F R S
f : F
inst_3 : NonUnitalRingHomClass F R S
e : R ≃+* S
⊢ Eq (α := TwoSidedIdeal R →o TwoSidedIdeal R) (OrderHom.comp (β := TwoSidedIdeal S) (comap e) (comap e.symm))
    OrderHom.id
have h : ∀ (x : TwoSidedIdeal R) (x_1 : R),
  Membership.mem (γ := TwoSidedIdeal R)
      ((OrderHom.comp (β := TwoSidedIdeal S) (comap e) (comap e.symm) : (a : TwoSidedIdeal R) → TwoSidedIdeal R) x :
        TwoSidedIdeal R)
      x_1 ↔
    Membership.mem (γ := TwoSidedIdeal R) ((OrderHom.id : (a : TwoSidedIdeal R) → TwoSidedIdeal R) x : TwoSidedIdeal R)
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : NonAssocRing T
I : TwoSidedIdeal T
f : R →+* S
g : S →+* T
⊢ Eq.{u_1 + 1} (α := TwoSidedIdeal R)
    (((comap f : OrderHom.{u_2, u_1} (TwoSidedIdeal S) (TwoSidedIdeal R)) : (a : TwoSidedIdeal S) → TwoSidedIdeal R)
        (((comap g : OrderHom.{u_3, u_2} (TwoSidedIdeal T) (TwoSidedIdeal S)) : (a : TwoSidedIdeal T) → TwoSidedIdeal S)
          I) :
      TwoSidedIdeal R)
    (((comap (g.comp f) : OrderHom.{u_3, u_1} (TwoSidedIdeal T) (TwoSidedIdeal R)) :
          (a : TwoSidedIdeal T) → TwoSidedIdeal R)
        I :
      TwoSidedIdeal R)
have h : ∀ (x : R),
  Membership.mem (γ := TwoSidedIdeal R)
      (((comap f : OrderHom.{u_2, u_1} (TwoSidedIdeal S) (TwoSidedIdeal R)) : (a : TwoSidedIdeal S) → TwoSidedIdeal R)
          (((comap g : OrderHom.{u_3, u_2} (TwoSidedIdeal T) (TwoSidedIdeal S)) :
              (a : TwoSidedIdeal T) → TwoSidedIdeal S)
            I) :
        TwoSidedIdeal R)
      x ↔
    Membership.mem (γ := TwoSidedIdeal R)
      (((comap (g.comp f) : OrderHom.{u_3, u_1} (TwoSidedIdeal T) (TwoSidedIdeal R)) :
            (a : TwoSidedIdeal T) → TwoSidedIdeal R)
          I :
        TwoSidedIdeal R)
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (hypothesis)
Goal:
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 : Membership.mem (γ := AddSubgroup R) (closure s) y
⊢ Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
have this : Membership.mem (α := R) (γ := AddSubgroup R) (closure ((⇑(AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) '' s))
  (((AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) y : R)
Tactic: have := (AddMonoidHom.mulLeft x).map_closure s ▸ mem_map_of_mem _ hy
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
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 : Membership.mem (γ := AddSubgroup R) (closure s) y
this :
  Membership.mem (α := R) (γ := AddSubgroup R) (closure ((⇑(AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) '' s))
    (((AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) y : R)
⊢ Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
have refine : (⇑(AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) '' s ⊆ s
Tactic: refine closure_mono ?_ this
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (hypothesis)
Goal:
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
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ Membership.mem (γ := AddSubgroup R) (closure s) z
have h_left' : ∀ {x y : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
  Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
Tactic: have h_left' {x y} (hy : y ∈ closure s) : x * y ∈ closure s := by
    have := (AddMonoidHom.mulLeft x).map_closure s ▸ mem_map_of_mem _ hy
    refine closure_mono ?_ this
    rintro - ⟨y, hy, rfl⟩
    exact h_left x y hy
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (hypothesis)
Goal:
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} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
y x : R
hy : Membership.mem (γ := AddSubgroup R) (closure s) y
⊢ Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
have this : Membership.mem (α := R) (γ := AddSubgroup R) (closure ((⇑(AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) '' s))
  (((AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) y : R)
Tactic: have := (AddMonoidHom.mulRight x).map_closure s ▸ mem_map_of_mem _ hy
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
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} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
y x : R
hy : Membership.mem (γ := AddSubgroup R) (closure s) y
this :
  Membership.mem (α := R) (γ := AddSubgroup R) (closure ((⇑(AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) '' s))
    (((AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) y : R)
⊢ Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
have refine : (⇑(AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) '' s ⊆ s
Tactic: refine closure_mono ?_ this
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (hypothesis)
Goal:
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} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ Membership.mem (γ := AddSubgroup R) (closure s) z
have h_right' : ∀ {y x : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
  Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
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
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
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} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
h_right' :
  ∀ {y x : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
I : TwoSidedIdeal R := mk' (↑(closure s) : Set R) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ Membership.mem (γ := AddSubgroup R) (closure s) z
have suffices : Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ z ∈ I
Tactic: suffices z ∈ span s ↔ z ∈ I by simpa only [I, mem_mk', SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
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} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
h_right' :
  ∀ {y x : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
I : TwoSidedIdeal R := mk' (↑(closure s) : Set R) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ z ∈ I
have rw : (∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → z ∈ I) ↔ z ∈ I
Tactic: rw [mem_span_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
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} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
h_right' :
  ∀ {y x : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
I : TwoSidedIdeal R := mk' (↑(closure s) : Set R) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → z ∈ I) ↔ z ∈ I
have refine : ∀ (h : ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → z ∈ I) (x : R) (hx : x ∈ s), x ∈ (↑I : Set R)
Tactic: refine ⟨fun h ↦ h I fun x hx ↦ ?mem_closure_of_forall, fun hz J hJ ↦ ?mem_ideal_of_subset⟩
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
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} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
h_right' :
  ∀ {y x : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
I : TwoSidedIdeal R := mk' (↑(closure s) : Set R) ⋯ ⋯ ⋯ ⋯ ⋯
refine : ∀ (h : ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → z ∈ I) (x : R) (hx : x ∈ s), x ∈ (↑I : Set R)
⊢ (∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → z ∈ I) ↔ z ∈ I
have refine₁ : ∀ (hz : z ∈ I) (J : TwoSidedIdeal R) (hJ : s ⊆ (↑J : Set R)), z ∈ J
Tactic: refine ⟨fun h ↦ h I fun x hx ↦ ?mem_closure_of_forall, fun hz J hJ ↦ ?mem_ideal_of_subset⟩
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (hypothesis)
Goal:
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} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
h_right' :
  ∀ {y x : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
I : TwoSidedIdeal R := mk' (↑(closure s) : Set R) ⋯ ⋯ ⋯ ⋯ ⋯
hz : z ∈ I
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
⊢ z ∈ J
have hz₁ : Membership.mem (γ := AddSubgroup R) (closure s) z
Tactic: simp only [I, SetLike.mem_coe, mem_mk'] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
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} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
h_right' :
  ∀ {y x : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
I : TwoSidedIdeal R := mk' (↑(closure s) : Set R) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
hz : Membership.mem (γ := AddSubgroup R) (closure s) z
⊢ z ∈ J
have mem : ∀ (x : R) (hx : x ∈ s), x ∈ J
Tactic: induction hz using closure_induction with
    | mem x hx => exact hJ hx
    | zero => exact zero_mem _
    | add x y _ _ hx hy => exact J.add_mem hx hy
    | neg x _ hx => exact J.neg_mem hx
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
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} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
h_right' :
  ∀ {y x : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
I : TwoSidedIdeal R := mk' (↑(closure s) : Set R) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
hz : Membership.mem (γ := AddSubgroup R) (closure s) z
mem : ∀ (x : R) (hx : x ∈ s), x ∈ J
⊢ z ∈ J
have zero : 0 ∈ J
Tactic: induction hz using closure_induction with
    | mem x hx => exact hJ hx
    | zero => exact zero_mem _
    | add x y _ _ hx hy => exact J.add_mem hx hy
    | neg x _ hx => exact J.neg_mem hx
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
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} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
h_right' :
  ∀ {y x : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
I : TwoSidedIdeal R := mk' (↑(closure s) : Set R) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
hz : Membership.mem (γ := AddSubgroup R) (closure s) z
mem : ∀ (x : R) (hx : x ∈ s), x ∈ J
zero : 0 ∈ J
⊢ z ∈ J
have add : ∀ (x y : R),
  Membership.mem (γ := AddSubgroup R) (closure s) x →
    Membership.mem (γ := AddSubgroup R) (closure s) y → ∀ (hx : x ∈ J) (hy : y ∈ J), x + y ∈ J
Tactic: induction hz using closure_induction with
    | mem x hx => exact hJ hx
    | zero => exact zero_mem _
    | add x y _ _ hx hy => exact J.add_mem hx hy
    | neg x _ hx => exact J.neg_mem hx
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
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} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
h_right' :
  ∀ {y x : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
I : TwoSidedIdeal R := mk' (↑(closure s) : Set R) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
hz : Membership.mem (γ := AddSubgroup R) (closure s) z
mem : ∀ (x : R) (hx : x ∈ s), x ∈ J
zero : 0 ∈ J
add :
  ∀ (x y : R),
    Membership.mem (γ := AddSubgroup R) (closure s) x →
      Membership.mem (γ := AddSubgroup R) (closure s) y → ∀ (hx : x ∈ J) (hy : y ∈ J), x + y ∈ J
⊢ z ∈ J
have neg : ∀ (x : R), Membership.mem (γ := AddSubgroup R) (closure s) x → ∀ (hx : x ∈ J), -x ∈ J
Tactic: induction hz using closure_induction with
    | mem x hx => exact hJ hx
    | zero => exact zero_mem _
    | add x y _ _ hx hy => exact J.add_mem hx hy
    | neg x _ hx => exact J.neg_mem hx
Cleared hypotheses: hz