awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
s t : NonUnitalSubsemiring R
f : F
⊢ Eq (α := NonUnitalSubsemiring S) (map f (s ⊔ t)) (map f s ⊔ map f t)

Tactic:
@GaloisConnection.l_sup _ _ s t _ _ _ _ (gc_map_comap f)

Premises used: NonUnitalSubsemiring.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
ι : Sort u_2
f : F
s : ι → NonUnitalSubsemiring R
⊢ Eq (α := NonUnitalSubsemiring S) (map f (iSup s)) (⨆ (i : ι), map f (s i))

Tactic:
@GaloisConnection.l_iSup _ _ _ _ _ _ _ (gc_map_comap f) s

Premises used: NonUnitalSubsemiring.gc_map_comap, GaloisConnection.l_iSup
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
s t : NonUnitalSubsemiring R
f : F
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq (α := NonUnitalSubsemiring S) (map f (s ⊓ t)) (map f s ⊓ map f t)

Tactic:
SetLike.coe_injective (Set.image_inter hf)

Premises used: Set.image_inter, SetLike.coe_injective
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
ι : Sort u_2
inst_4 : Nonempty ι
f : F
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : ι → NonUnitalSubsemiring R
a : (↑(map f (iInf s)) : Set S) = (↑(⨅ (i : ι), map f (s i)) : Set S)
⊢ Eq (α := NonUnitalSubsemiring S) (map f (iInf s)) (⨅ (i : ι), map f (s i))

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
ι : Sort u_2
inst_4 : Nonempty ι
f : F
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : ι → NonUnitalSubsemiring R
⊢ (↑(map f (iInf s)) : Set S) = (↑(⨅ (i : ι), map f (s i)) : Set S)

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Premises used: Set.InjOn.image_iInter_eq, Set.injOn_of_injective
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
s t : NonUnitalSubsemiring S
f : F
⊢ Eq (α := NonUnitalSubsemiring R) (comap f (s ⊓ t)) (comap f s ⊓ comap f t)

Tactic:
@GaloisConnection.u_inf _ _ s t _ _ _ _ (gc_map_comap f)

Premises used: NonUnitalSubsemiring.gc_map_comap, GaloisConnection.u_inf
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
ι : Sort u_2
f : F
s : ι → NonUnitalSubsemiring S
⊢ Eq (α := NonUnitalSubsemiring R) (comap f (iInf s)) (⨅ (i : ι), comap f (s i))

Tactic:
@GaloisConnection.u_iInf _ _ _ _ _ _ _ (gc_map_comap f) s

Premises used: NonUnitalSubsemiring.gc_map_comap, GaloisConnection.u_iInf
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
⊢ Eq (α := NonUnitalSubsemiring S) (map f ⊥) ⊥

Tactic:
(gc_map_comap f).l_bot

Premises used: NonUnitalSubsemiring.gc_map_comap, GaloisConnection.l_bot
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
⊢ Eq (α := NonUnitalSubsemiring R) (comap f ⊤) ⊤

Tactic:
(gc_map_comap f).u_top

Premises used: NonUnitalSubsemiring.gc_map_comap, GaloisConnection.u_top
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
s : NonUnitalSubsemiring R
t : NonUnitalSubsemiring S
⊢ (↑(s.prod t) : Set (R × S)) = (↑s : Set R) ×ˢ (↑t : Set S)

Tactic:
rfl

Premises used: setOf, Set.prod, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
s : NonUnitalSubsemiring R
t : NonUnitalSubsemiring S
p : R × S
⊢ p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.prod
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
s₁ s₂ : NonUnitalSubsemiring R
hs : s₁ ≤ s₂
t₁ t₂ : NonUnitalSubsemiring S
ht : t₁ ≤ t₂
⊢ s₁.prod t₁ ≤ s₂.prod t₂

Tactic:
Set.prod_mono hs ht

Premises used: Set.Mem, setOf, Set.prod, Set.Subset, Set.prod_mono
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
s : NonUnitalSubsemiring R
⊢ Monotone (β := NonUnitalSubsemiring (R × S)) fun (t : NonUnitalSubsemiring S) ↦ s.prod t

Tactic:
prod_mono (le_refl s)

Premises used: le_refl, Set.Mem, NonUnitalSubsemiring.prod_mono, Monotone
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
t : NonUnitalSubsemiring S
⊢ Monotone (β := NonUnitalSubsemiring (R × S)) fun (s : NonUnitalSubsemiring R) ↦ s.prod t

Tactic:
fun _ _ hs => prod_mono hs (le_refl t)

Premises used: le_refl, Set.Mem, NonUnitalSubsemiring.prod_mono, Monotone
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
s : NonUnitalSubsemiring R
x : R × S
⊢ Membership.mem (γ := NonUnitalSubsemiring (R × S)) (s.prod ⊤) x ↔
    Membership.mem (γ := NonUnitalSubsemiring (R × S)) (comap (F := R × S →ₙ+* R) (NonUnitalRingHom.fst R S) s) x

Tactic:
simp [mem_prod]

Premises used: NonUnitalSubsemiring.mem_prod
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
s : NonUnitalSubsemiring S
x : R × S
⊢ Membership.mem (γ := NonUnitalSubsemiring (R × S)) (prod ⊤ s) x ↔
    Membership.mem (γ := NonUnitalSubsemiring (R × S)) (comap (F := R × S →ₙ+* S) (NonUnitalRingHom.snd R S) s) x

Tactic:
simp [mem_prod]

Premises used: NonUnitalSubsemiring.mem_prod
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
⊢ Eq (α := NonUnitalSubsemiring (R × S)) (prod ⊤ ⊤) ⊤

Tactic:
(top_prod _).trans <| comap_top _

Premises used: NonUnitalSubsemiring.top_prod, NonUnitalSubsemiring.comap_top, Eq.trans
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
x : R
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i

Tactic:
⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Premises used: iSup, Membership.mem, le_iSup, _private.0.NonUnitalSubsemiring.mem_iSup_of_directed.match_1, Iff.intro
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
x : R
refine : Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubsemigroup) ⋯
    (⨆ (i : ι), (S i).toAddSubmonoid) ⋯
this : ⨆ (i : ι), S i ≤ U
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i

Tactic:
simpa [U] using @this x
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubsemigroup) ⋯
    (⨆ (i : ι), (S i).toAddSubmonoid) ⋯
suffices : ⨆ (i : ι), S i ≤ U
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i

Tactic:
suffices ⨆ i, S i ≤ U by simpa [U] using @this x
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubsemigroup) ⋯
    (⨆ (i : ι), (S i).toAddSubmonoid) ⋯
⊢ ⨆ (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.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubsemigroup) ⋯
    (⨆ (i : ι), (S i).toAddSubmonoid) ⋯
⊢ ⨆ (i : ι), S i ≤ U

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

Premises used: iSup_le
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun (x1 x2 : NonUnitalSubsemiring 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: NonUnitalSubsemiring.mem_iSup_of_directed
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
S : Set (NonUnitalSubsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
x : R
⊢ Nonempty.{u + 1} (↑S : Type u)

Tactic:
haveI : Nonempty S := Sne.to_subtype
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
S : Set (NonUnitalSubsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : NonUnitalSubsemiring 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, Subtype.exists, exists_prop]

Premises used: NonUnitalSubsemiring.mem_iSup_of_directed, Subtype.exists, exists_prop, DirectedOn.directed_val, sSup_eq_iSup'
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
S : Set (NonUnitalSubsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : NonUnitalSubsemiring 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: NonUnitalSubsemiring.mem_sSup_of_directedOn
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative.{u} ↥(S i)
dir : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{u} ↥(⨆ (i : ι), S i)

Tactic:
.of_setLike_mul_comm ?_

Premises used: IsMulCommutative.of_setLike_mul_comm
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative.{u} ↥(S i)
dir : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
refine :
  ∀ (a : R),
    Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) a →
      ∀ (b : R), Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) b → a * b = b * a
⊢ IsMulCommutative.{u} ↥(⨆ (i : ι), S i)

Tactic:
refine .of_setLike_mul_comm ?_
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative.{u} ↥(S i)
dir : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
simp_rw : ∀ (a : R) (x : ι) (h : a ∈ S x) (b : R) (x : ι) (h : b ∈ S x), a * b = b * a
⊢ ∀ (a : R),
    Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) a →
      ∀ (b : R), Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) b → a * b = b * a

Tactic:
simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
    SetLike.mem_coe, forall_exists_index]

Premises used: NonUnitalSubsemiring.coe_iSup_of_directed, Set.mem_iUnion, forall_exists_index, SetLike.mem_coe
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative.{u} ↥(S i)
dir : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
a : R
i : ι
ha : a ∈ S i
b : R
j : ι
hb : b ∈ S j
obtain : ∀ (k : ι) (hik : S i ≤ S k) (hjk : S j ≤ S k), a * b = b * a
⊢ a * b = b * a

Tactic:
obtain ⟨k, hik, hjk⟩ := dir i j
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative.{u} ↥(S i)
dir : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
a : R
i : ι
ha : a ∈ S i
b : R
j : ι
hb : b ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ a * b = b * a

Tactic:
setLike_mul_comm (hik ha) (hjk hb)

Premises used: setLike_mul_comm
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative.{u} ↥(S i)
dir : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
a : R
i : ι
ha : a ∈ S i
b : R
j : ι
hb : b ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ a * b = b * a

Tactic:
exact setLike_mul_comm (hik ha) (hjk hb)

Premises used: setLike_mul_comm
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S_1 : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst_1 : NonUnitalNonAssocSemiring S_1
F : Type u_1
inst_2 : FunLike F R S_1
inst_3 : NonUnitalRingHomClass F R S_1
ι : Type u_2
inst_4 : Nonempty ι
inst_5 : Preorder ι
inst_6 : IsDirectedOrder ι
S : OrderHom.{u_2, u} ι (NonUnitalSubsemiring R)
hS : ∀ (i : ι), IsMulCommutative.{u} ↥((S : (a : ι) → NonUnitalSubsemiring R) i : NonUnitalSubsemiring R)
⊢ IsMulCommutative.{u} ↥(⨆ (i : ι), (S : (a : ι) → NonUnitalSubsemiring R) i)

Tactic:
NonUnitalSubsemiring.isMulCommutative_iSup S.monotone.directed_le

Premises used: OrderHom.monotone, NonUnitalSubsemiring.isMulCommutative_iSup, Monotone.directed_le
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
F : Type u_1
inst_1 : FunLike F R S
f g : F
h : Set.EqOn.{u, v} (β := S) (⇑f : (a : R) → S) (⇑g : (a : R) → S) (↑⊤ : Set R)
⊢ f = g

Tactic:
DFunLike.ext _ _ fun _ => h trivial

Premises used: trivial, DFunLike.ext
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
F : Type u_1
inst_1 : FunLike F R S
inst_2 : NonUnitalNonAssocSemiring S
inst_3 : NonUnitalRingHomClass F R S
f : F
x : R
⊢ Eq.{v + 1} (α := S)
    ((↑(((srangeRestrict f : NonUnitalRingHom.{u, v} R ↥(srange f)) : (a : R) → ↥(srange f)) x) : S) : S)
    ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
F : Type u_1
inst_1 : FunLike F R S
inst_2 : NonUnitalNonAssocSemiring S
inst_3 : NonUnitalRingHomClass F R S
f : F
⊢ Function.Surjective.{u + 1, v + 1} (α := R) (β := ↥(srange f)) (⇑(srangeRestrict f) : (a : R) → ↥(srange f))

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

Premises used: NonUnitalRingHom.mem_srange, _private.0.NonUnitalRingHom.srangeRestrict_surjective.match_2, Exists, Subtype.mk, Exists.intro, Iff.mp, NonUnitalRingHom.srangeRestrict, _private.0.NonUnitalRingHom.srangeRestrict_surjective.match_1, Eq, DFunLike.coe, Function.Surjective, Subtype.ext
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
F : Type u_1
inst_1 : FunLike F R S
inst_2 : NonUnitalNonAssocSemiring S
inst_3 : NonUnitalRingHomClass F R S
f : F
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
⊢ (↑(srange f) : Set S) = (↑⊤ : Set S) ↔
    Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ

Tactic:
rw [coe_srange, coe_top]

Premises used: NonUnitalRingHom.coe_srange, NonUnitalSubsemiring.coe_top
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
F : Type u_1
inst_1 : FunLike F R S
inst_2 : NonUnitalNonAssocSemiring S
inst_3 : NonUnitalRingHomClass F R S
f : F
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq (α := NonUnitalSubsemiring S) (srange f) ⊤

Tactic:
srange_eq_top_iff_surjective.2 hf

Premises used: Iff.mpr, NonUnitalRingHom.srange_eq_top_iff_surjective
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
F : Type u_1
inst_1 : FunLike F R S
inst_2 : NonUnitalNonAssocSemiring S
inst_3 : NonUnitalRingHomClass F R S
f g : F
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 ≤ eqSlocus f g from closure_le.2 h

Premises used: Iff.mpr, Set.Mem, setOf, Set.EqOn, NonUnitalSubsemiring.closure_le
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
F : Type u_1
inst_1 : FunLike F R S
inst_2 : NonUnitalNonAssocSemiring S
inst_3 : NonUnitalRingHomClass F R S
s : Set R
hs : Eq (α := NonUnitalSubsemiring R) (closure s) ⊤
f g : F
h : Set.EqOn.{u, v} (β := S) (⇑f : (a : R) → S) (⇑g : (a : R) → S) s
⊢ f = g

Tactic:
eq_of_eqOn_stop <| hs ▸ eqOn_sclosure h

Premises used: NonUnitalRingHom.eq_of_eqOn_stop
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
F : Type u_1
inst_1 : FunLike F R S
inst_2 : NonUnitalNonAssocSemiring S
inst_3 : NonUnitalRingHomClass F R S
f : F
s : Set S
⊢ LE.le (α := NonUnitalSubsemiring R) (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, NonUnitalSubsemiring.subset_closure, SetLike.mem_coe, NonUnitalSubsemiring.closure_le, NonUnitalSubsemiring.mem_comap
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
F : Type u_1
inst_1 : FunLike F R S
inst_2 : NonUnitalNonAssocSemiring S
inst_3 : NonUnitalRingHomClass F R S
f : F
s : Set R
⊢ Eq (α := NonUnitalSubsemiring S) (map f (closure s)) (closure ((⇑f : (a : R) → S) '' s))

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

Premises used: GaloisConnection.l_comm_of_u_comm, NonUnitalSubsemiring.gc_map_comap, Set.image_preimage, NonUnitalSubsemiring.gi, rfl, GaloisInsertion.gc
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : NonUnitalSubsemiring R
⊢ srange (F := ↥s →ₙ+* R) (subtype s) = s

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

Premises used: SetLike.coe_injective, Subtype.range_coe, NonUnitalRingHom.coe_srange, Eq.trans
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
⊢ Eq (α := NonUnitalSubsemiring R) (srange (F := R × S →ₙ+* R) (fst R S)) ⊤

Tactic:
NonUnitalRingHom.srange_eq_top_of_surjective (fst R S) Prod.fst_surjective

Premises used: NonUnitalRingHom.fst, Prod.fst_surjective, NonUnitalRingHom.srange_eq_top_of_surjective
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
⊢ Eq (α := NonUnitalSubsemiring S) (srange (F := R × S →ₙ+* S) (snd R S)) ⊤

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

Premises used: NonUnitalRingHom.srange_eq_top_of_surjective, Prod.snd_surjective, NonUnitalRingHom.snd
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
s t : NonUnitalSubsemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
g : S → R
f : F
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : ↥(srange f)
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.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
g : S → R
f : F
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : R
⊢ Eq.{v + 1} (α := S) ((↑(((sofLeftInverse' h : RingEquiv.{u, v} R ↥(srange f)) : (a : R) → ↥(srange f)) x) : S) : S)
    ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
g : S → R
f : F
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : ↥(srange f)
⊢ (RingEquiv.symm (sofLeftInverse' h) : (a : ↥(srange f)) → R) x = g (↑x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u_1
S : Type u_2
inst : Mul R
inst_1 : HasDistribNeg R
inst_2 : SetLike S R
inst_3 : MulMemClass S R
s : S
x y : R
hx : -x ∈ s
hy : y ∈ s
⊢ -(x * y) ∈ s

Tactic:
simpa using mul_mem hx hy

Premises used: MulMemClass.mul_mem