awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Noetherian.Orzech
Goal:
R : Type u_1
M : Type u_2
N : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective.{w + 1, u_2 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
this : IsNoetherian R N
n : ℕ
H :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R N)
        (({ toFun := fun (n : ℕ) ↦ f.iterateMapComap i n ⊥, monotone' := ⋯ : ℕ →o Submodule R N } :
              (a : ℕ) → Submodule R N)
            n :
          Submodule R N)
        (({ toFun := fun (n : ℕ) ↦ f.iterateMapComap i n ⊥, monotone' := ⋯ : ℕ →o Submodule R N } :
              (a : ℕ) → Submodule R N)
            m :
          Submodule R N)
⊢ Injective.{w + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)

Tactic:
exact LinearMap.ker_eq_bot.1 <| bot_unique <|
    f.ker_le_of_iterateMapComap_eq_succ i ⊥ n (H _ (Nat.le_succ _)) hf hi

Premises used: LinearMap.ker_le_of_iterateMapComap_eq_succ, LinearMap.ker_eq_bot, Nat.le_succ, Bot.bot, Iff.mp, bot_unique
-- Module: Mathlib.RingTheory.Noetherian.Orzech
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
⊢ Injective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)

Tactic:
IsNoetherian.injective_of_surjective_of_injective N.subtype f N.injective_subtype hf

Premises used: IsNoetherian.injective_of_surjective_of_injective, Submodule.injective_subtype, Submodule.subtype
-- Module: Mathlib.RingTheory.Noetherian.Orzech
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : M →ₗ[R] M
s : Surjective (α := M) (β := M) (⇑f : (a : M) → M)
⊢ Injective (α := M) (β := M) (⇑f : (a : M) → M)

Tactic:
IsNoetherian.injective_of_surjective_of_injective _ f (LinearEquiv.refl _ _).injective s

Premises used: IsNoetherian.injective_of_surjective_of_injective, LinearEquiv.refl, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Noetherian.Orzech
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : M →ₗ[R] M
s : Surjective (α := M) (β := M) (⇑f : (a : M) → M)
⊢ Bijective (α := M) (β := M) (⇑f : (a : M) → M)

Tactic:
⟨IsNoetherian.injective_of_surjective_endomorphism f s, s⟩

Premises used: IsNoetherian.injective_of_surjective_endomorphism, And.intro, Function.Bijective
-- Module: Mathlib.RingTheory.Noetherian.Orzech
Goal:
R : Type u_1
M : Type u_2
N : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherian R M
f : M × N →ₗ[R] M
i : Injective (α := M × N) (β := M) (⇑f : (a : M × N) → M)
x y : N
⊢ Injective (α := M × N) (β := M) (⇑(LinearMap.fst R M N : M × N →ₗ[R] M) : (a : M × N) → M)

Tactic:
have h := IsNoetherian.injective_of_surjective_of_injective f _ i LinearMap.fst_surjective
-- Module: Mathlib.RingTheory.Noetherian.Orzech
Goal:
R : Type u_1
M : Type u_2
N : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherian R M
f : M × N →ₗ[R] M
i : Injective (α := M × N) (β := M) (⇑f : (a : M × N) → M)
x y : N
h : Injective (α := M × N) (β := M) (⇑(LinearMap.fst R M N : M × N →ₗ[R] M) : (a : M × N) → M)
⊢ x = y

Tactic:
simpa using h (show LinearMap.fst R M N (0, x) = LinearMap.fst R M N (0, y) from rfl)

Premises used: rfl
-- Module: Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
h : IsNoetherianRing R
⊢ WfDvdMonoid R

Tactic:
WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt h.wf.wellFoundedOn

Premises used: WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt, WellFounded.wellFoundedOn, IsNoetherian.wf
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
l : List R
⊢ (∀ x ∈ l, x ∈ s) → l.sum ∈ s

Tactic:
list_sum_mem

Premises used: Set.Mem, list_sum_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
m : Multiset R
⊢ (∀ a ∈ m, a ∈ s) → m.sum ∈ s

Tactic:
multiset_sum_mem _

Premises used: multiset_sum_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
ι : Type u_2
t : Finset ι
f : ι → R
h : ∀ c ∈ t, f c ∈ s
⊢ ∑ i ∈ t, f i ∈ s

Tactic:
sum_mem h

Premises used: sum_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
x : R
⊢ Membership.mem (γ := NonUnitalSubring R) ⊤ x

Tactic:
Set.mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
⊢ (↑⊤ : Set R) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
⊢ Eq.{u + 1} (α := NonUnitalSubsemiring R) (toNonUnitalSubsemiring ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
⊢ Eq.{u + 1} (α := AddSubgroup R) (toAddSubgroup ⊤) ⊤

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
S : NonUnitalSubring R
⊢ S.toNonUnitalSubsemiring = ⊤ ↔ S = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
S : NonUnitalSubring R
⊢ S.toAddSubgroup = ⊤ ↔ S = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
s : NonUnitalSubring S
f : F
⊢ (↑(comap f s) : Set R) = (⇑f : (a : R) → S) ⁻¹' (↑s : Set S)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
s : NonUnitalSubring S
f : F
x : R
⊢ Membership.mem (γ := NonUnitalSubring R) (comap f s) x ↔ Membership.mem (α := S) s ((f : (a : R) → S) x : S)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
T : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : NonUnitalNonAssocRing T
s : NonUnitalSubring T
g : S →ₙ+* T
f : R →ₙ+* S
⊢ Eq (α := NonUnitalSubring R) (comap f (comap g s)) (comap (g.comp f) s)

Tactic:
rfl

Premises used: Set.Mem, setOf, NonUnitalSubring.comap, Set.preimage, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
s : NonUnitalSubring R
⊢ (↑(map f s) : Set S) = (⇑f : (a : R) → S) '' (↑s : Set R)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
s : NonUnitalSubring R
y : S
⊢ Membership.mem (γ := NonUnitalSubring S) (map f s) y ↔ ∃ x ∈ s, (f : (a : R) → S) x = y

Tactic:
Set.mem_image _ _ _

Premises used: Set.Mem, setOf, Set.mem_image, Set.image
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
⊢ map (F := R →ₙ+* R) (NonUnitalRingHom.id R) s = s

Tactic:
SetLike.coe_injective <| Set.image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
T : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : NonUnitalNonAssocRing T
s : NonUnitalSubring R
g : S →ₙ+* T
f : R →ₙ+* S
⊢ Eq (α := NonUnitalSubring T) (map g (map f s)) (map (g.comp f) s)

Tactic:
SetLike.coe_injective <| Set.image_image _ _ _

Premises used: Set.image_image, SetLike.coe_injective
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
s : NonUnitalSubring R
t : NonUnitalSubring S
⊢ map f s ≤ t ↔ s ≤ comap f t

Tactic:
Set.image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
⊢ GaloisConnection (α := NonUnitalSubring R) (β := NonUnitalSubring S) (map f) (comap f)

Tactic:
fun _S _T =>
  map_le_iff_le_comap

Premises used: NonUnitalSubring.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
s : NonUnitalSubring R
f : F
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : ↥s
⊢ Eq.{v + 1} (α := S)
    ((↑(((s.equivMapOfInjective f hf : RingEquiv.{u, v} ↥s ↥(map f s)) : (a : ↥s) → ↥(map f s)) x) : S) : S)
    ((f : (a : R) → S) (↑x : R) : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R →ₙ+* S
⊢ (↑f.range : Set S) = Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R →ₙ+* S
y : S
⊢ y ∈ f.range ↔ ∃ (x : R), (f : (a : R) → S) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R →ₙ+* S
h : ∀ (x : S), x ∈ f.range ↔ Membership.mem (γ := NonUnitalSubring S) (NonUnitalSubring.map f ⊤) x
⊢ f.range = NonUnitalSubring.map f ⊤

Tactic:
ext
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R →ₙ+* S
x : S
⊢ x ∈ f.range ↔ Membership.mem (γ := NonUnitalSubring S) (NonUnitalSubring.map f ⊤) x

Tactic:
simp
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R →ₙ+* S
x : R
⊢ Membership.mem (α := S) f.range ((f : (a : R) → S) x : S)

Tactic:
mem_range.mpr ⟨x, rfl⟩

Premises used: Iff.mpr, NonUnitalRingHom.mem_range, Exists.intro, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
T : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : NonUnitalNonAssocRing T
g : S →ₙ+* T
f : R →ₙ+* S
⊢ NonUnitalSubring.map g f.range = (g.comp f).range

Tactic:
simpa only [range_eq_map] using (⊤ : NonUnitalSubring R).map_map g f

Premises used: NonUnitalSubring.map_map, Top.top, NonUnitalRingHom.range_eq_map
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
⊢ (↑⊥ : Set R) = {0}

Tactic:
(NonUnitalRingHom.coe_range (0 : R →ₙ+* R)).trans (@Set.range_const R R _ 0)

Premises used: NonUnitalRingHom.coe_range, Set.range_const, OfNat.ofNat, Eq.trans
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
x : R
rw : Membership.mem (γ := Set R) {0} x ↔ x = 0
rw₁ rw₂ : x = 0 ↔ x = 0
⊢ x ∈ (↑⊥ : Set R) ↔ x = 0

Tactic:
rw [coe_bot, Set.mem_singleton_iff]

Premises used: NonUnitalSubring.coe_bot, Set.mem_singleton_iff
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
p p' : NonUnitalSubring R
⊢ (↑(p ⊓ p') : Set R) = (↑p : Set R) ∩ (↑p' : Set R)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
p p' : NonUnitalSubring R
x : R
⊢ x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set (NonUnitalSubring R)
⊢ (↑(⨅ t ∈ s, t.toSubsemigroup) : Set R) = ⋂ t ∈ s, (↑t : Set R)

Tactic:
simp
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set (NonUnitalSubring R)
⊢ (↑(⨅ t ∈ s, t.toAddSubgroup) : Set R) = ⋂ t ∈ s, (↑t : Set R)

Tactic:
simp
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
S : Set (NonUnitalSubring R)
⊢ (↑(sInf S) : Set R) = ⋂ s ∈ S, (↑s : Set R)

Tactic:
rfl

Premises used: iInf, Set.iInter, setOf, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
S : Set (NonUnitalSubring R)
x : R
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
Set.mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
ι : Sort u_1
S : ι → NonUnitalSubring R
⊢ (↑(⨅ (i : ι), S i) : Set R) = ⋂ (i : ι), (↑(S i) : Set R)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Premises used: NonUnitalSubring.coe_sInf, iInf, Set.biInter_range
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
ι : Sort u_1
S : ι → NonUnitalSubring R
x : R
⊢ Membership.mem (γ := NonUnitalSubring R) (⨅ (i : ι), S i) x ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Premises used: iInf, Set.forall_mem_range, NonUnitalSubring.mem_sInf
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set (NonUnitalSubring R)
⊢ (sInf s).toSubsemigroup = ⨅ t ∈ s, t.toSubsemigroup

Tactic:
mk'_toSubsemigroup _ _

Premises used: NonUnitalSubring.mk'_toSubsemigroup
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set (NonUnitalSubring R)
⊢ (sInf s).toAddSubgroup = ⨅ t ∈ s, t.toAddSubgroup

Tactic:
mk'_toAddSubgroup _ _

Premises used: NonUnitalSubring.mk'_toAddSubgroup
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
A : NonUnitalSubring R
⊢ A = ⊤ ↔ ∀ (x : R), x ∈ A

Tactic:
eq_top_iff.trans ⟨fun h m => h <| mem_top m, fun h m _ => h m⟩

Premises used: eq_top_iff, NonUnitalSubring.mem_top, Iff.intro, Iff.trans
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
⊢ (↑(center R) : Set R) = Set.center R

Tactic:
rfl

Premises used: setOf, Set.center, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
⊢ Eq (α := NonUnitalSubsemiring R) (toNonUnitalSubsemiring (center R)) (NonUnitalSubsemiring.center R)

Tactic:
rfl

Premises used: NonUnitalSubsemiring.center, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalRing R
⊢ Eq (α := NonUnitalRing ↥(center R)) NonUnitalCommRing.toNonUnitalRing
    (NonUnitalSubringClass.toNonUnitalRing (center R))

Tactic:
rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalRing R
⊢ Eq (α := NonUnitalRing ↥(center R)) NonUnitalCommRing.toNonUnitalRing
    (NonUnitalSubringClass.toNonUnitalRing (center R))

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalRing R
z : R
⊢ Membership.mem (γ := NonUnitalSubring R) (center R) z ↔ ∀ (g : R), g * z = z * g

Tactic:
Subsemigroup.mem_center_iff

Premises used: Set.Mem, setOf, Subsemigroup.mem_center_iff, Set.center
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u_1
inst : NonUnitalCommRing R
⊢ Eq (α := NonUnitalSubring R) (center R) ⊤

Tactic:
SetLike.coe_injective (Set.center_eq_univ R)

Premises used: Set.center_eq_univ, SetLike.coe_injective
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
⊢ (↑(centralizer s) : Set R) = s.centralizer

Tactic:
rfl

Premises used: setOf, Set.centralizer, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
⊢ Eq (α := NonUnitalSubsemiring R) (toNonUnitalSubsemiring (centralizer s)) (NonUnitalSubsemiring.centralizer s)

Tactic:
rfl

Premises used: NonUnitalSubsemiring.centralizer, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
⊢ Membership.mem (γ := NonUnitalSubring R) (centralizer s) z ↔ ∀ g ∈ s, g * z = z * g

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.centralizer
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
⊢ LE.le (α := NonUnitalSubring R) (center R) (centralizer s)

Tactic:
s.center_subset_centralizer

Premises used: Set.Mem, setOf, Set.center, Set.centralizer, Set.Subset, Set.center_subset_centralizer
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u_1
inst : NonUnitalRing R
s t : Set R
h : s ⊆ t
⊢ LE.le (α := NonUnitalSubring R) (centralizer t) (centralizer s)

Tactic:
Set.centralizer_subset h

Premises used: Set.Mem, setOf, Set.centralizer, Set.Subset, Set.centralizer_subset
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
⊢ Eq (α := NonUnitalSubring R) (centralizer s) ⊤ ↔ s ⊆ (↑(center R) : Set R)

Tactic:
SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset

Premises used: Set.centralizer_eq_top_iff_subset, SetLike.ext'_iff, Iff.trans
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u_1
inst : NonUnitalRing R
⊢ Eq (α := NonUnitalSubring R) (centralizer Set.univ) (center R)

Tactic:
SetLike.ext' (Set.centralizer_univ R)

Premises used: SetLike.ext', Set.centralizer_univ
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
x : R
s : Set R
⊢ Membership.mem (γ := NonUnitalSubring R) (closure s) x ↔ ∀ (S : NonUnitalSubring R), s ⊆ (↑S : Set R) → x ∈ S

Tactic:
mem_sInf

Premises used: Set.Mem, setOf, NonUnitalSubring.mem_sInf
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
⊢ s ⊆ (↑(closure s) : Set R)

Tactic:
fun _x hx => mem_closure.2 fun _S hS => hS hx

Premises used: Iff.mpr, Set.Subset, NonUnitalSubring.mem_closure
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x : R
hx : x ∈ s
⊢ Membership.mem (γ := NonUnitalSubring R) (closure s) x

Tactic:
subset_closure hx

Premises used: NonUnitalSubring.subset_closure
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
P : R
hP : P ∉ closure s
⊢ P ∉ s

Tactic:
fun h =>
  hP (subset_closure h)

Premises used: NonUnitalSubring.subset_closure, Not
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
t : NonUnitalSubring R
⊢ closure s ≤ t ↔ s ⊆ (↑t : Set R)

Tactic:
⟨Set.Subset.trans subset_closure, fun h => sInf_le h⟩

Premises used: Set.Subset.trans, sInf_le, Iff.intro, NonUnitalSubring.subset_closure
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
⊢ LE.le (α := NonUnitalSubring R) (closure s) (closure t)

Tactic:
closure_le.2 <| Set.Subset.trans h subset_closure

Premises used: Iff.mpr, Set.Subset.trans, NonUnitalSubring.subset_closure, NonUnitalSubring.closure_le
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
t : NonUnitalSubring R
h₁ : s ⊆ (↑t : Set R)
h₂ : t ≤ closure s
⊢ closure s = t

Tactic:
le_antisymm (closure_le.2 h₁) h₂

Premises used: Iff.mpr, le_antisymm, NonUnitalSubring.closure_le
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
p : (x : R) → Membership.mem (γ := NonUnitalSubring R) (closure s) x → Prop
mem : ∀ (x : R) (hx : x ∈ s), p x ⋯
zero : p 0 ⋯
add :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p x hx → p (-x) ⋯
mul :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : R
hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x
⊢ p x hx

Tactic:
let K : NonUnitalSubring R :=
    { carrier := { x | ∃ hx, p x hx }
      mul_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, mul _ _ _ _ hpx hpy⟩
      add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
      neg_mem' := fun ⟨_, hpx⟩ ↦ ⟨_, neg _ _ hpx⟩
      zero_mem' := ⟨_, zero⟩ }
  closure_le (t := K) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Premises used: Iff.mpr, HMul.hMul, setOf, Membership.mem, Exists, id, NonUnitalSubsemiring.mk, AddSubmonoid.mk, AddSubsemigroup.mk, NonUnitalSubring.closure, HAdd.hAdd, Exists.intro, AddMemClass.add_mem, ZeroMemClass.zero_mem, NonUnitalSubring.subset_closure, _private.0.NonUnitalSubring.closure_induction.match_1, Neg.neg, NonUnitalSubring.mk, Exists.elim, NegMemClass.neg_mem, NonUnitalSubring.closure_le, MulMemClass.mul_mem