awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun (x1 x2 : Subring R) ↦ x1 ≤ x2) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), (S i).toAddSubgroup) ⋯ ⋯
suffices : ⨆ (i : ι), S i ≤ U
⊢ Membership.mem (γ := Subring R) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i

Tactic:
suffices ⨆ i, S i ≤ U by simpa [U] using @this x
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun (x1 x2 : Subring R) ↦ x1 ≤ x2) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), (S i).toAddSubgroup) ⋯ ⋯
⊢ ⨆ (i : ι), S i ≤ U

Tactic:
iSup_le fun i x hx ↦ Set.mem_iUnion.2 ⟨i, hx⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro, iSup_le
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun (x1 x2 : Subring R) ↦ x1 ≤ x2) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), (S i).toAddSubgroup) ⋯ ⋯
⊢ ⨆ (i : ι), S i ≤ U

Tactic:
exact iSup_le fun i x hx ↦ Set.mem_iUnion.2 ⟨i, hx⟩

Premises used: iSup_le
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun (x1 x2 : Subring R) ↦ x1 ≤ x2) S
x : R
⊢ x ∈ (↑(⨆ (i : ι), S i) : Set R) ↔ Membership.mem (γ := Set R) (⋃ (i : ι), (↑(S i) : Set R)) x

Tactic:
simp [mem_iSup_of_directed hS]

Premises used: Subring.mem_iSup_of_directed
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
S : Set (Subring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Subring R) ↦ x1 ≤ x2) S
x : R
⊢ Nonempty.{u + 1} (↑S : Type u)

Tactic:
haveI : Nonempty S := Sne.to_subtype
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
S : Set (Subring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Subring R) ↦ x1 ≤ x2) S
x : R
this : Nonempty.{u + 1} (↑S : Type u)
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, exists_prop]

Premises used: SetCoe.exists, exists_prop, DirectedOn.directed_val, Subring.mem_iSup_of_directed, sSup_eq_iSup'
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
S : Set (Subring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Subring R) ↦ x1 ≤ x2) S
x : R
⊢ x ∈ (↑(sSup S) : Set R) ↔ Membership.mem (γ := Set R) (⋃ s ∈ S, (↑s : Set R)) x

Tactic:
simp [mem_sSup_of_directedOn Sne hS]

Premises used: Subring.mem_sSup_of_directedOn
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
ι : Sort u_1
inst_1 : Nonempty ι
S : ι → Subring R
hS : ∀ (i : ι), IsMulCommutative.{u} ↥(S i)
dir : Directed (fun (x1 x2 : Subring R) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{u} ↥(⨆ (i : ι), S i)

Tactic:
simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
    Subsemigroup.coe_iSup_of_directed dir] using Subsemigroup.isMulCommutative_iSup dir

Premises used: Subring.coe_iSup_of_directed, SetLike.mem_coe, Subsemigroup.isMulCommutative_iSup, Subsemigroup.coe_iSup_of_directed, isMulCommutative_iff
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
ι : Type u_1
inst_3 : Nonempty ι
inst_4 : Preorder ι
inst_5 : IsDirectedOrder ι
S : OrderHom.{u_1, u} ι (Subring R)
hS : ∀ (i : ι), IsMulCommutative.{u} ↥((S : (a : ι) → Subring R) i : Subring R)
⊢ IsMulCommutative.{u} ↥(⨆ (i : ι), (S : (a : ι) → Subring R) i)

Tactic:
Subring.isMulCommutative_iSup S.monotone.directed_le

Premises used: OrderHom.monotone, Subring.isMulCommutative_iSup, Monotone.directed_le
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R ≃+* S
K : Subring R
x : S
⊢ Membership.mem (γ := Subring S) (map (↑f : R →+* S) K) x ↔ Membership.mem (α := R) K ((f.symm : (a : S) → R) x : R)

Tactic:
@Set.mem_image_equiv _ _ (K : Set R) f.toEquiv x

Premises used: Set.Mem, setOf, Set.image, Set.mem_image_equiv
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R ≃+* S
K : Subring R
⊢ Eq (α := Subring S) (map (↑f : R →+* S) K) (comap (↑f.symm : S →+* R) K)

Tactic:
SetLike.coe_injective (f.toEquiv.image_eq_preimage_symm K)

Premises used: RingEquiv.toEquiv, SetLike.coe_injective, Equiv.image_eq_preimage_symm, SetLike.coe
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R ≃+* S
K : Subring S
⊢ Eq (α := Subring R) (comap (↑f : R →+* S) K) (map (↑f.symm : S →+* R) K)

Tactic:
(map_equiv_eq_comap_symm f.symm K).symm

Premises used: Subring.map_equiv_eq_comap_symm, Equiv.symm, Eq.symm, RingEquiv.symm
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
x : R
⊢ Eq.{v + 1} (α := S) ((↑((f.rangeRestrict : (a : R) → ↥f.range) x) : S) : S) ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
⊢ Function.Surjective.{u + 1, v + 1} (α := R) (β := ↥f.range) (⇑f.rangeRestrict : (a : R) → ↥f.range)

Tactic:
fun ⟨_y, hy⟩ =>
  let ⟨x, hx⟩ := mem_range.mp hy
  ⟨x, Subtype.ext hx⟩

Premises used: RingHom.mem_range, Exists, _private.0.RingHom.rangeRestrict_surjective.match_2, _private.0.RingHom.rangeRestrict_surjective.match_1, RingHom.rangeRestrict, Subtype.mk, Exists.intro, Iff.mp, Eq, DFunLike.coe, Function.Surjective, Subtype.ext
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
rw :
  Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S) = (↑⊤ : Set S) ↔
    Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ
rw₁ rw₂ :
  Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ ↔
    Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ
⊢ (↑f.range : Set S) = (↑⊤ : Set S) ↔
    Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ

Tactic:
rw [coe_range, coe_top]

Premises used: Subring.coe_top, RingHom.coe_range
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ f.range = ⊤

Tactic:
range_eq_top.2 hf

Premises used: Iff.mpr, RingHom.range_eq_top
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : NonAssocRing T
g : S →+* T
f : R →+* S
⊢ comp (g.domRestrict f.range) f.rangeRestrict = g.comp f

Tactic:
rfl

Premises used: RingHom.domRestrict, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
S : Type v
inst_1 : Semiring S
f g : R →+* S
x : R
⊢ x ∈ f.eqLocus g ↔ Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((g : (a : R) → S) x : S)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
S : Type v
inst_1 : Semiring S
f : R →+* S
⊢ f.eqLocus f = ⊤

Tactic:
SetLike.ext fun _ => eq_self_iff_true _

Premises used: SetLike.ext, DFunLike.coe, eq_self_iff_true
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
S : Type v
inst_1 : Semiring S
f g : R →+* S
s : Set R
h : Set.EqOn.{u, v} (β := S) (⇑f : (a : R) → S) (⇑g : (a : R) → S) s
⊢ Set.EqOn.{u, v} (β := S) (⇑f : (a : R) → S) (⇑g : (a : R) → S) (↑(closure s) : Set R)

Tactic:
show closure s ≤ f.eqLocus g from closure_le.2 h

Premises used: Iff.mpr, Set.Mem, setOf, Set.EqOn, Subring.closure_le
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
S : Type v
inst_1 : Semiring S
f g : R →+* S
h : Set.EqOn.{u, v} (β := S) (⇑f : (a : R) → S) (⇑g : (a : R) → S) (↑⊤ : Set R)
⊢ f = g

Tactic:
ext fun _x => h trivial

Premises used: trivial, RingHom.ext
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
S : Type v
inst_1 : Semiring S
s : Set R
hs : Eq (α := Subring R) (closure s) ⊤
f g : R →+* S
h : Set.EqOn.{u, v} (β := S) (⇑f : (a : R) → S) (⇑g : (a : R) → S) s
⊢ f = g

Tactic:
eq_of_eqOn_set_top <| hs ▸ eqOn_set_closure h

Premises used: Eq.rec, RingHom.eqOn_set_closure, RingHom.eq_of_eqOn_set_top
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Set S
⊢ closure ((⇑f : (a : R) → S) ⁻¹' s) ≤ comap f (closure s)

Tactic:
closure_le.2 fun _ hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx

Premises used: Iff.mpr, Subring.subset_closure, Subring.mem_comap, SetLike.mem_coe, Subring.closure_le
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Set R
⊢ map f (closure s) = closure ((⇑f : (a : R) → S) '' s)

Tactic:
Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Subring.gi S).gc (Subring.gi R).gc
    fun _ ↦ rfl

Premises used: GaloisConnection.l_comm_of_u_comm, Set.image_preimage, Subring.gc_map_comap, Subring.gi, rfl, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Set R
x : R
hx : Membership.mem (γ := Subring R) (closure s) x
rw :
  ∃ (x_1 : R),
    Membership.mem (γ := Subring R) (closure s) x_1 ∧
      Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)
⊢ Membership.mem.{v, v} (α := S) (γ := Subring S) (closure ((⇑f : (a : R) → S) '' s)) ((f : (a : R) → S) x : S)

Tactic:
rw [← f.map_closure, Subring.mem_map]

Premises used: Subring.mem_map, RingHom.map_closure
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Set R
x : R
hx : Membership.mem (γ := Subring R) (closure s) x
⊢ ∃ (x_1 : R),
    Membership.mem (γ := Subring R) (closure s) x_1 ∧
      Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)

Tactic:
⟨x, hx, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Set R
x : R
hx : Membership.mem (γ := Subring R) (closure s) x
⊢ ∃ (x_1 : R),
    Membership.mem (γ := Subring R) (closure s) x_1 ∧
      Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)

Tactic:
exact ⟨x, hx, rfl⟩
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
S T : Subring R
h : S ≤ T
x : ↥S
⊢ (↑((inclusion h : (a : ↥S) → ↥T) x) : R) = (↑x : R)

Tactic:
simp [Subring.inclusion]

Premises used: Subring.inclusion
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
S T : Subring R
h : S ≤ T
⊢ Function.Injective (α := ↥S) (β := ↥T) (⇑(inclusion h) : (a : ↥S) → ↥T)

Tactic:
RingHom.injective_codRestrict.mpr S.subtype_injective

Premises used: Iff.mpr, RingHom.injective_codRestrict, Subring.subtype_injective
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
⊢ s.subtype.range = s

Tactic:
SetLike.coe_injective <| (coe_rangeS _).trans Subtype.range_coe

Premises used: SetLike.coe_injective, Subtype.range_coe, Eq.trans, RingHom.coe_rangeS
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
⊢ Eq (α := Subsemiring R) (rangeS (fst R S)) ⊤

Tactic:
(fst R S).rangeS_top_of_surjective <| Prod.fst_surjective

Premises used: Prod.fst_surjective, RingHom.rangeS_top_of_surjective, RingHom.fst
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
⊢ Eq (α := Subsemiring S) (rangeS (snd R S)) ⊤

Tactic:
(snd R S).rangeS_top_of_surjective <| Prod.snd_surjective

Premises used: RingHom.snd, RingHom.rangeS_top_of_surjective, Prod.snd_surjective
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
s : Subring R
t : Subring S
⊢ s.prod ⊥ ⊔ prod ⊥ t = s.prod t

Tactic:
le_antisymm (sup_le (prod_mono_right s bot_le) (prod_mono_left t bot_le)) fun p hp =>
    Prod.fst_mul_snd p ▸
      mul_mem
        ((le_sup_left : s.prod ⊥ ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨hp.1, SetLike.mem_coe.2 <| one_mem ⊥⟩)
        ((le_sup_right : prod ⊥ t ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨SetLike.mem_coe.2 <| one_mem ⊥, hp.2⟩)

Premises used: Iff.mpr, Prod.fst_mul_snd, le_sup_left, Eq.rec, Subring.prod_mono_left, le_sup_right, Bot.bot, le_antisymm, And.right, And.left, SetLike.mem_coe, And.intro, sup_le, OneMemClass.one_mem, bot_le, Subring.prod_mono_right, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s t : Subring R
h : s = t
⊢ (subringCongr h).symm = subringCongr ⋯

Tactic:
rfl

Premises used: Equiv.setCongr, Equiv.subtypeEquiv, RingEquiv.subringCongr, Equiv.subtypeEquivProp, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s t : Subring R
h : s = t
x : ↥s
⊢ (↑((subringCongr h : (a : ↥s) → ↥t) x) : R) = (↑x : R)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : NonAssocRing T
s t : Subring R
g : S → R
f : R →+* S
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : ↥f.range
x' : R
hx' : (f : (a : R) → S) x' = (↑x : S)
rw : Eq.{v + 1} (α := S) ((f : (a : R) → S) (g ((f : (a : R) → S) x')) : S) ((f : (a : R) → S) x' : S)
rw₁ rw₂ : Eq.{v + 1} (α := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x' : S)
⊢ (f : (a : R) → S) (g (↑x : S)) = (↑x : S)

Tactic:
rw [← hx', h x']
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
g : S → R
f : R →+* S
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : R
⊢ Eq.{v + 1} (α := S) ((↑((ofLeftInverse h : (a : R) → ↥f.range) x) : S) : S) ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
g : S → R
f : R →+* S
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : ↥f.range
⊢ ((ofLeftInverse h).symm : (a : ↥f.range) → R) x = g (↑x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
s_1 t : Subring R_1
R : Type u
S : Type v
inst_3 : NonAssocSemiring R
inst_4 : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst_5 : SetLike σR R
inst_6 : SetLike σS S
inst_7 : SubsemiringClass σR R
inst_8 : SubsemiringClass σS S
e : R ≃+* S
s' : σR
s : σS
h : ∀ (x : R), x ∈ s' ↔ Membership.mem.{v, u_2} (α := S) s ((e : (a : R) → S) x : S)
y : S
hy : y ∈ s
obtain :
  ∀ (x : R) (hy : Membership.mem.{v, u_2} (α := S) s ((e : (a : R) → S) x : S)),
    Membership.mem.{u, u_1} (α := R) s' (((↑e.symm : S →+* R) : (a : S) → R) ((e : (a : R) → S) x : S) : R)
⊢ Membership.mem.{u, u_1} (α := R) s' (((↑e.symm : S →+* R) : (a : S) → R) y : R)

Tactic:
obtain ⟨x, rfl⟩ := e.surjective y

Premises used: RingEquiv.surjective, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
s_1 t : Subring R_1
R : Type u
S : Type v
inst_3 : NonAssocSemiring R
inst_4 : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst_5 : SetLike σR R
inst_6 : SetLike σS S
inst_7 : SubsemiringClass σR R
inst_8 : SubsemiringClass σS S
e : R ≃+* S
s' : σR
s : σS
h : ∀ (x : R), x ∈ s' ↔ Membership.mem.{v, u_2} (α := S) s ((e : (a : R) → S) x : S)
x : R
hy : Membership.mem.{v, u_2} (α := S) s ((e : (a : R) → S) x : S)
⊢ Membership.mem.{u, u_1} (α := R) s' (((↑e.symm : S →+* R) : (a : S) → R) ((e : (a : R) → S) x : S) : R)

Tactic:
simp [(h _).2 hy]

Premises used: Iff.mpr
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
s_1 t : Subring R_1
R : Type u
S : Type v
inst_3 : NonAssocSemiring R
inst_4 : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst_5 : SetLike σR R
inst_6 : SetLike σS S
inst_7 : SubsemiringClass σR R
inst_8 : SubsemiringClass σS S
e : R ≃+* S
s' : σR
s : σS
h : ∀ (x : R), x ∈ s' ↔ Membership.mem.{v, u_2} (α := S) s ((e : (a : R) → S) x : S)
y : ↥s'
⊢ ((RingHom.restrict (↑e.symm : S →+* R) s s' ⋯ : RingHom.{v, u} ↥s ↥s') : (a : ↥s) → ↥s')
      (OneHom.toFun (↑(↑(RingHom.restrict (↑e : R →+* S) s' s ⋯) : ↥s' →* ↥s) : OneHom ↥s' ↥s) y) =
    y

Tactic:
simp [← Subtype.val_inj]

Premises used: Subtype.val_inj
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
s_1 t : Subring R_1
R : Type u
S : Type v
inst_3 : NonAssocSemiring R
inst_4 : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst_5 : SetLike σR R
inst_6 : SetLike σS S
inst_7 : SubsemiringClass σR R
inst_8 : SubsemiringClass σS S
e : R ≃+* S
s' : σR
s : σS
h : ∀ (x : R), x ∈ s' ↔ Membership.mem.{v, u_2} (α := S) s ((e : (a : R) → S) x : S)
x : ↥s
⊢ OneHom.toFun (M := ↥s') (↑(↑(RingHom.restrict (↑e : R →+* S) s' s ⋯) : ↥s' →* ↥s) : OneHom ↥s' ↥s)
      (((RingHom.restrict (↑e.symm : S →+* R) s s' ⋯ : RingHom.{v, u} ↥s ↥s') : (a : ↥s) → ↥s') x) =
    x

Tactic:
simp [← Subtype.val_inj]

Premises used: Subtype.val_inj
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
x : R
hx : Membership.mem (γ := Subring R) (closure s) x
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
have : ∀ (h0 : C 0), C x
⊢ C x

Tactic:
have h0 : C 0 := add_neg_cancel (1 : R) ▸ ha h1 hneg1
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
x : R
hx : Membership.mem (γ := Subring R) (closure s) x
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
rcases :
  ∀ (L : List (List R)) (HL : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1)
    (hx : Membership.mem (γ := Subring R) (closure s) (List.map List.prod L).sum), C (List.map List.prod L).sum
⊢ C x

Tactic:
rcases exists_list_of_mem_closure hx with ⟨L, HL, rfl⟩

Premises used: Subring.exists_list_of_mem_closure, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
HL : ∀ (t : List R), Membership.mem (γ := List (List R)) [] t → ∀ y ∈ t, y ∈ s ∨ y = -1
⊢ C (List.sum (List.map List.prod []))

Tactic:
h0

Premises used: List.sum, List.foldr
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
HL : ∀ (t : List R), Membership.mem (γ := List (List R)) [] t → ∀ y ∈ t, y ∈ s ∨ y = -1
⊢ C (List.sum (List.map List.prod []))

Tactic:
exact h0
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod tl).sum
HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ s ∨ y = -1
⊢ C (List.map List.prod (hd :: tl)).sum

Tactic:
?_
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1
cons :
  ∀ (hd : List R) (tl : List (List R)) (ih : ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod tl).sum)
    (HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod (hd :: tl)).sum
⊢ C (List.map List.prod L).sum

Tactic:
induction L with
  | nil => exact h0
  | cons hd tl ih => ?_
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod tl).sum
HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ s ∨ y = -1
⊢ (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1

Tactic:
rw [List.forall_mem_cons] at HL

Premises used: List.forall_mem_cons
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
this : C hd.prod
rw : C (hd.prod + (List.map List.prod tl).sum)
⊢ C (List.map List.prod (hd :: tl)).sum

Tactic:
rw [List.map_cons, List.sum_cons]

Premises used: List.map_cons, List.sum_cons
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
this : C hd.prod
⊢ C (hd.prod + (List.map List.prod tl).sum)

Tactic:
ha this (ih HL.2)

Premises used: And.right
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
this : C hd.prod
⊢ C (hd.prod + (List.map List.prod tl).sum)

Tactic:
exact ha this (ih HL.2)

Premises used: And.right
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
cons : C hd.prod
⊢ C (List.map List.prod (hd :: tl)).sum

Tactic:
suffices C (List.prod hd) by
    rw [List.map_cons, List.sum_cons]
    exact ha this (ih HL.2)
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
cons : ∀ (HL : ∀ y ∈ hd, y ∈ s ∨ y = -1), C hd.prod
⊢ C hd.prod

Tactic:
replace HL := HL.1