awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Subring.IntPolynomial
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
⊢ (↑(int R P hP).leadingCoeff : K) = P.leadingCoeff

Tactic:
rfl

Premises used: Polynomial.int, Polynomial.leadingCoeff, Polynomial.degree, Polynomial.coeff, Polynomial.natDegree, Polynomial.support, rfl
-- Module: Mathlib.Algebra.Ring.Subring.IntPolynomial
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
rw : (int R P hP).leadingCoeff = 1 ↔ P.Monic
rw₁ : (int R P hP).leadingCoeff = 1 ↔ P.leadingCoeff = 1
rw₂ : (int R P hP).leadingCoeff = 1 ↔ (↑(int R P hP).leadingCoeff : K) = 1
R₁ : Subring K
hP₁ : ∀ (n : ℕ), P.coeff n ∈ R
rw₃ : (int R P hP).leadingCoeff = 1 ↔ (int R P hP).leadingCoeff = 1
R₂ : Subring K
hP₂ : ∀ (n : ℕ), P.coeff n ∈ R
rw₄ : (int R P hP).leadingCoeff = 1 ↔ (int R P hP).leadingCoeff = 1
R₃ : Subring K
hP₃ : ∀ (n : ℕ), P.coeff n ∈ R
⊢ (int R P hP).Monic ↔ P.Monic

Tactic:
rw [Monic, Monic, ← int_leadingCoeff_eq, OneMemClass.coe_eq_one]

Premises used: OneMemClass.coe_eq_one, Polynomial.Monic, Polynomial.int_leadingCoeff_eq
-- Module: Mathlib.Algebra.Ring.Subring.IntPolynomial
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
⊢ (int R P hP).natDegree = P.natDegree

Tactic:
rfl

Premises used: Polynomial.int, Polynomial.degree, Polynomial.natDegree, Polynomial.support, rfl
-- Module: Mathlib.Algebra.Ring.Subring.IntPolynomial
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
x : L
rw :
  Eq.{u_2 + 1} (α := L)
    (∑ i ∈ Finset.range ((int R P hP).natDegree + 1),
      HMul.hMul (α := L) ((algebraMap (↥R) L : (a : ↥R) → L) ((int R P hP).coeff i) : L) (x ^ i))
    (∑ i ∈ Finset.range (P.natDegree + 1), P.coeff i • x ^ i)
⊢ eval₂ (algebraMap (↥R) L) x (int R P hP) = (aeval x : (a : K[X]) → L) P

Tactic:
rw [aeval_eq_sum_range, eval₂_eq_sum_range]

Premises used: Polynomial.aeval_eq_sum_range, Polynomial.eval₂_eq_sum_range
-- Module: Mathlib.Algebra.Ring.Subring.IntPolynomial
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
x : L
n : ℕ
h : n ∈ Finset.range (P.natDegree + 1)
rw :
  HMul.hMul (α := L) ((algebraMap (↥R) L : (a : ↥R) → L) ((int R P hP).coeff n) : L) (x ^ n) =
    HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) (P.coeff n) : L) (x ^ n)
⊢ HMul.hMul (α := L) ((algebraMap (↥R) L : (a : ↥R) → L) ((int R P hP).coeff n) : L) (x ^ n) = P.coeff n • x ^ n

Tactic:
rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.Ring.Subring.IntPolynomial
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
x : L
n : ℕ
h : n ∈ Finset.range (P.natDegree + 1)
⊢ HMul.hMul (α := L) ((algebraMap (↥R) L : (a : ↥R) → L) ((int R P hP).coeff n) : L) (x ^ n) =
    HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) (P.coeff n) : L) (x ^ n)

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.Subring.IntPolynomial
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
x : L
⊢ Eq.{u_2 + 1} (α := L)
    (∑ i ∈ Finset.range ((int R P hP).natDegree + 1),
      HMul.hMul (α := L) ((algebraMap (↥R) L : (a : ↥R) → L) ((int R P hP).coeff i) : L) (x ^ i))
    (∑ i ∈ Finset.range (P.natDegree + 1), P.coeff i • x ^ i)

Tactic:
exact Finset.sum_congr rfl (fun n _ => by rw [Algebra.smul_def]; rfl)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
inst : NonAssocRing R
S : Subring R
⊢ ∀ {x : Rᵐᵒᵖ}, x ∈ S.op.carrier → -x ∈ S.op.carrier

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
x : Rᵐᵒᵖ
S : Subring R
⊢ x ∈ S.op ↔ MulOpposite.unop x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
inst : NonAssocRing R
S : Subring Rᵐᵒᵖ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
x : R
S : Subring Rᵐᵒᵖ
⊢ x ∈ S.unop ↔ MulOpposite.op x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S : Subring R
⊢ S.op.unop = S

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Subring.unop, MulOpposite.unop, Subsemiring.unop, Submonoid.unop, rfl
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S : Subring Rᵐᵒᵖ
⊢ S.unop.op = S

Tactic:
rfl

Premises used: Set.Mem, Submonoid.op, MulOpposite, setOf, Set.preimage, Subring.op, Subsemiring.op, MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S₁ : Subring R
S₂ : Subring Rᵐᵒᵖ
⊢ S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S₁ : Subring Rᵐᵒᵖ
S₂ : Subring R
⊢ S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S₁ S₂ : Subring R
⊢ S₁.op ≤ S₂.op ↔ S₁ ≤ S₂

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S₁ S₂ : Subring Rᵐᵒᵖ
⊢ S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂

Tactic:
MulOpposite.unop_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, MulOpposite, setOf, Set.preimage, MulOpposite.unop, MulOpposite.unop_surjective, MulOpposite.op
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := Subring R) Subring.op

Tactic:
opEquiv.injective

Premises used: OrderIso.injective, Subring.op, Subring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := Subring Rᵐᵒᵖ) Subring.unop

Tactic:
opEquiv.symm.injective

Premises used: OrderIso.symm, OrderIso.injective, Subring.unop, Subring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S T : Subring R
⊢ S.op = T.op ↔ S = T

Tactic:
opEquiv.eq_iff_eq

Premises used: RelIso.eq_iff_eq, Subring.op, Subring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S T : Subring Rᵐᵒᵖ
⊢ S.unop = T.unop ↔ S = T

Tactic:
opEquiv.symm.eq_iff_eq

Premises used: RelIso.eq_iff_eq, OrderIso.symm, Subring.unop, Subring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
⊢ Eq.{u_2 + 1} (α := Subring Rᵐᵒᵖ) (Subring.op ⊥) ⊥

Tactic:
opEquiv.map_bot

Premises used: Subring.op, Subring.opEquiv, OrderIso.map_bot
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S : Subring R
⊢ S.op = ⊥ ↔ S = ⊥

Tactic:
op_injective.eq_iff' op_bot

Premises used: Subring.op_injective, Subring.op_bot, Function.Injective.eq_iff'
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
⊢ Eq.{u_2 + 1} (α := Subring R) (Subring.unop ⊥) ⊥

Tactic:
opEquiv.symm.map_bot

Premises used: OrderIso.symm, Subring.unop, Subring.opEquiv, OrderIso.map_bot
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S : Subring Rᵐᵒᵖ
⊢ S.unop = ⊥ ↔ S = ⊥

Tactic:
unop_injective.eq_iff' unop_bot

Premises used: Subring.unop_injective, Function.Injective.eq_iff', Subring.unop_bot
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
⊢ Eq.{u_2 + 1} (α := Subring Rᵐᵒᵖ) (Subring.op ⊤) ⊤

Tactic:
rfl

Premises used: Set.Mem, Submonoid.op, Set.univ, setOf, Set.preimage, Subring.op, Subsemiring.op, rfl
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S : Subring R
⊢ S.op = ⊤ ↔ S = ⊤

Tactic:
op_injective.eq_iff' op_top

Premises used: Subring.op_injective, Subring.op_top, Function.Injective.eq_iff'
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
⊢ Eq.{u_2 + 1} (α := Subring R) (Subring.unop ⊤) ⊤

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, Subring.unop, Subsemiring.unop, Submonoid.unop, rfl
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S : Subring Rᵐᵒᵖ
⊢ S.unop = ⊤ ↔ S = ⊤

Tactic:
unop_injective.eq_iff' unop_top

Premises used: Subring.unop_injective, Subring.unop_top, Function.Injective.eq_iff'
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S₁ S₂ : Subring R
⊢ (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op

Tactic:
opEquiv.map_sup _ _

Premises used: Set.Mem, setOf, Subring.op, OrderIso.map_sup, Subring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S₁ S₂ : Subring Rᵐᵒᵖ
⊢ (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop

Tactic:
opEquiv.symm.map_sup _ _

Premises used: Set.Mem, setOf, OrderIso.symm, OrderIso.map_sup, Subring.unop, Subring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S₁ S₂ : Subring R
⊢ (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op

Tactic:
rfl

Premises used: Set.Mem, Submonoid.op, setOf, Set.inter, Set.preimage, Subring.op, Subsemiring.op, rfl
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S₁ S₂ : Subring Rᵐᵒᵖ
⊢ (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, Set.preimage, Subring.unop, Subsemiring.unop, Submonoid.unop, rfl
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S : Set (Subring R)
⊢ (sSup S).op = sSup (Subring.unop ⁻¹' S)

Tactic:
opEquiv.map_sSup_eq_sSup_symm_preimage _

Premises used: Set.Mem, OrderIso.map_sSup_eq_sSup_symm_preimage, Subring.op, Subring.unop, Subring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S : Set (Subring Rᵐᵒᵖ)
⊢ (sSup S).unop = sSup (Subring.op ⁻¹' S)

Tactic:
opEquiv.symm.map_sSup_eq_sSup_symm_preimage _

Premises used: Set.Mem, OrderIso.map_sSup_eq_sSup_symm_preimage, OrderIso.symm, Subring.op, Subring.unop, Subring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S : Set (Subring R)
⊢ (sInf S).op = sInf (Subring.unop ⁻¹' S)

Tactic:
opEquiv.map_sInf_eq_sInf_symm_preimage _

Premises used: Set.Mem, OrderIso.map_sInf_eq_sInf_symm_preimage, Subring.op, Subring.unop, Subring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
S : Set (Subring Rᵐᵒᵖ)
⊢ (sInf S).unop = sInf (Subring.op ⁻¹' S)

Tactic:
opEquiv.symm.map_sInf_eq_sInf_symm_preimage _

Premises used: Set.Mem, OrderIso.map_sInf_eq_sInf_symm_preimage, OrderIso.symm, Subring.op, Subring.unop, Subring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
inst : NonAssocRing R
S : ι → Subring R
⊢ (iSup S).op = ⨆ (i : ι), (S i).op

Tactic:
opEquiv.map_iSup _

Premises used: OrderIso.map_iSup, Subring.op, Subring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
inst : NonAssocRing R
S : ι → Subring Rᵐᵒᵖ
⊢ (iSup S).unop = ⨆ (i : ι), (S i).unop

Tactic:
opEquiv.symm.map_iSup _

Premises used: OrderIso.map_iSup, OrderIso.symm, Subring.unop, Subring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
inst : NonAssocRing R
S : ι → Subring R
⊢ (iInf S).op = ⨅ (i : ι), (S i).op

Tactic:
opEquiv.map_iInf _

Premises used: OrderIso.map_iInf, Subring.op, Subring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
inst : NonAssocRing R
S : ι → Subring Rᵐᵒᵖ
⊢ (iInf S).unop = ⨅ (i : ι), (S i).unop

Tactic:
opEquiv.symm.map_iInf _

Premises used: OrderIso.map_iInf, OrderIso.symm, Subring.unop, Subring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
s : Set R
simp_rw :
  Eq.{u_2 + 1} (α := Subring Rᵐᵒᵖ) (sInf {a : Subring Rᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Rᵐᵒᵖ)})
    (sInf {S : Subring Rᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑S : Set Rᵐᵒᵖ)})
⊢ Eq (α := Subring Rᵐᵒᵖ) (Subring.op (closure s)) (closure (MulOpposite.unop ⁻¹' s))

Tactic:
simp_rw [closure, op_sInf, Set.preimage_setOf_eq, coe_unop]

Premises used: Subring.coe_unop, Subring.op_sInf, Set.preimage_setOf_eq, Subring.closure
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
s : Set R
e_a : ∀ (a : Subring Rᵐᵒᵖ), s ⊆ MulOpposite.op ⁻¹' (↑a : Set Rᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Rᵐᵒᵖ)
⊢ Eq.{u_2 + 1} (α := Subring Rᵐᵒᵖ) (sInf {a : Subring Rᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Rᵐᵒᵖ)})
    (sInf {S : Subring Rᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑S : Set Rᵐᵒᵖ)})

Tactic:
congr with a
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
s : Set R
a : Subring Rᵐᵒᵖ
⊢ s ⊆ MulOpposite.op ⁻¹' (↑a : Set Rᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Rᵐᵒᵖ)

Tactic:
MulOpposite.unop_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, MulOpposite, setOf, Set.Subset, Set.preimage, MulOpposite.unop, MulOpposite.unop_surjective, MulOpposite.op
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
s : Set R
a : Subring Rᵐᵒᵖ
⊢ s ⊆ MulOpposite.op ⁻¹' (↑a : Set Rᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Rᵐᵒᵖ)

Tactic:
exact MulOpposite.unop_surjective.forall

Premises used: Function.Surjective.forall, MulOpposite.unop_surjective
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
s : Set Rᵐᵒᵖ
rw : Eq (α := Subring Rᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
⊢ Eq (α := Subring R) (Subring.unop (closure s)) (closure (MulOpposite.op ⁻¹' s))

Tactic:
rw [← op_inj, op_unop, op_closure]

Premises used: Subring.op_inj, Subring.op_closure, Subring.op_unop
-- Module: Mathlib.Algebra.Ring.Subring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocRing R
s : Set Rᵐᵒᵖ
simp_rw : Eq (α := Subring Rᵐᵒᵖ) (closure s) (closure ((fun (x : Rᵐᵒᵖ) ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s))
simp_rw₁ : Eq (α := Subring Rᵐᵒᵖ) (closure s) (closure ((fun (x : Rᵐᵒᵖ) ↦ x) ⁻¹' s))
⊢ Eq (α := Subring Rᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))

Tactic:
simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

Premises used: Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id'
-- Module: Mathlib.Algebra.Ring.Subring.Order
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : SetLike S R
inst_3 : SubringClass S R
inst_4 : IsOrderedRing R
s : S
⊢ IsOrderedRing.{u_1} ↥s

Tactic:
Function.Injective.isOrderedRing Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) .rfl

Premises used: Iff.rfl, Function.Injective.isOrderedRing, Subtype.val, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Order
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : SetLike S R
inst_3 : SubringClass S R
inst_4 : IsStrictOrderedRing R
s : S
⊢ IsStrictOrderedRing.{u_1} ↥s

Tactic:
Function.Injective.isStrictOrderedRing Subtype.val
    rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) .rfl .rfl

Premises used: Iff.rfl, Function.Injective.isStrictOrderedRing, Subtype.val, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Order
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
s : Subring R
⊢ (↑s.orderedSubtype : ↥s →+* R) = s.subtype

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, Subring.subtype, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
S : Subring R
⊢ a • S = map (MulSemiringAction.toRingHom M R a) S

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
m : M
S : Subring R
⊢ (↑(m • S) : Set R) = m • (↑S : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
m : M
S : Subring R
⊢ (m • S).toAddSubgroup = m • S.toAddSubgroup

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl, AddSubgroup.map
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
m : M
S : Subring R
⊢ (m • S).toSubsemiring = m • S.toSubsemiring

Tactic:
rfl

Premises used: Subsemiring.map, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
m : M
r : R
S : Subring R
⊢ r ∈ S → m • r ∈ m • S

Tactic:
(Set.smul_mem_smul_set : _ → _ ∈ m • (S : Set R))

Premises used: Set.Mem, Set.smul_mem_smul_set
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
⊢ CovariantClass M (Subring R) HSMul.hSMul LE.le

Tactic:
⟨fun _ _ => image_mono⟩

Premises used: CovariantClass.mk, Set.image_mono
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
m : M
r : R
S : Subring R
⊢ r ∈ m • S ↔ ∃ s ∈ S, m • s = r

Tactic:
(Set.mem_smul_set : r ∈ m • (S : Set R) ↔ _)

Premises used: Set.Mem, Set.mem_smul_set
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
⊢ HSMul.hSMul (β := Subring R) a ⊥ = ⊥

Tactic:
map_bot _

Premises used: Subring.map_bot
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
S T : Subring R
⊢ a • (S ⊔ T) = a • S ⊔ a • T

Tactic:
map_sup _ _ _

Premises used: Set.Mem, setOf, Subring.map_sup
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
s : Set R
⊢ HSMul.hSMul (β := Subring R) a (closure s) = closure (a • s)

Tactic:
RingHom.map_closure _ _

Premises used: RingHom.map_closure
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
inst_3 : MulSemiringAction.{u_1, u_2} Mᵐᵒᵖ R
inst_4 : IsCentralScalar M R
⊢ IsCentralScalar.{u_1, u_2} M (Subring R)

Tactic:
⟨fun _ S => (congr_arg fun f => S.map f) <| RingHom.ext <| op_smul_eq_smul _⟩

Premises used: Subring.map, RingHom.ext, congr_arg, IsCentralScalar.mk, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
S : Subring R
x : R
⊢ a • x ∈ a • S ↔ x ∈ S

Tactic:
smul_mem_smul_set_iff

Premises used: Set.Mem, Set.smul_mem_smul_set_iff
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
S : Subring R
x : R
⊢ x ∈ a • S ↔ a⁻¹ • x ∈ S

Tactic:
mem_smul_set_iff_inv_smul_mem

Premises used: Set.Mem, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
S : Subring R
x : R
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

Tactic:
mem_inv_smul_set_iff

Premises used: Set.Mem, Set.mem_inv_smul_set_iff
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
S T : Subring R
⊢ a • S ≤ a • T ↔ S ≤ T

Tactic:
smul_set_subset_smul_set_iff

Premises used: Set.Mem, Set.Subset, Set.smul_set_subset_smul_set_iff
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
S T : Subring R
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T

Tactic:
smul_set_subset_iff_subset_inv_smul_set

Premises used: Set.Mem, Set.Subset, Set.smul_set_subset_iff_subset_inv_smul_set
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
S T : Subring R
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T

Tactic:
subset_smul_set_iff

Premises used: Set.Mem, Set.subset_smul_set_iff, Set.Subset
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : GroupWithZero M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
ha : a ≠ 0
S : Subring R
x : R
⊢ a • x ∈ a • S ↔ x ∈ S

Tactic:
smul_mem_smul_set_iff₀ ha (S : Set R) x

Premises used: Set.Mem, Set.smul_mem_smul_set_iff₀, SetLike.coe
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : GroupWithZero M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
ha : a ≠ 0
S : Subring R
x : R
⊢ x ∈ a • S ↔ a⁻¹ • x ∈ S

Tactic:
mem_smul_set_iff_inv_smul_mem₀ ha (S : Set R) x

Premises used: Set.Mem, SetLike.coe, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : GroupWithZero M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
ha : a ≠ 0
S : Subring R
x : R
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

Tactic:
mem_inv_smul_set_iff₀ ha (S : Set R) x

Premises used: Set.mem_inv_smul_set_iff₀, Set.Mem, SetLike.coe
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : GroupWithZero M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
ha : a ≠ 0
S T : Subring R
⊢ a • S ≤ a • T ↔ S ≤ T

Tactic:
smul_set_subset_smul_set_iff₀ ha

Premises used: Set.smul_set_subset_smul_set_iff₀, Set.Mem, Set.Subset
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : GroupWithZero M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
ha : a ≠ 0
S T : Subring R
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T

Tactic:
smul_set_subset_iff₀ ha

Premises used: Set.Mem, Set.Subset, Set.smul_set_subset_iff₀
-- Module: Mathlib.Algebra.Ring.Subring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : GroupWithZero M
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
ha : a ≠ 0
S T : Subring R
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T

Tactic:
subset_smul_set_iff₀ ha

Premises used: Set.Mem, Set.Subset, Set.subset_smul_set_iff₀
-- Module: Mathlib.Algebra.Ring.Subring.Units
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
u : Rˣ
⊢ Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) u ↔ 0 < (↑u : R)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocSemiring R
M : Submonoid R
inst_1 : SetLike S R
hSR : SubsemiringClass S R
s : S
inst_2 : CharZero R
⊢ CharZero.{u} ↥s

Tactic:
⟨Function.Injective.of_comp (f := Subtype.val) (g := Nat.cast (R := s)) Nat.cast_injective⟩

Premises used: CharZero.mk, Nat.cast_injective, Function.Injective.of_comp
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
⊢ StrictMono.{u, u} (α := Subsemiring R) toSubmonoid

Tactic:
fun _ _ => id

Premises used: StrictMono, id
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
⊢ Monotone.{u, u} (α := Subsemiring R) toSubmonoid

Tactic:
toSubmonoid_strictMono.monotone

Premises used: StrictMono.monotone, Subsemiring.toSubmonoid_strictMono