awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T U : Subalgebra R A
hst : S ≤ T
htu : T ≤ U
x : ↥S
⊢ Eq (α := ↥U) ((inclusion htu : (a : ↥T) → ↥U) ((inclusion hst : (a : ↥S) → ↥T) x) : ↥U)
    ((inclusion ⋯ : (a : ↥S) → ↥U) x : ↥U)

Tactic:
Subtype.ext rfl

Premises used: rfl, Subtype.ext
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
hst : S ≤ T
⊢ T.val.comp (inclusion hst) = S.val

Tactic:
rfl

Premises used: Set.Mem, Subalgebra.val, AlgHom.comp, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
h : S ≤ T
s : ↥S
⊢ (↑((inclusion h : (a : ↥S) → ↥T) s) : A) = (↑s : A)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
X : Type u_1
inst_5 : SMul X R
inst_6 : SMul X A
inst_7 : IsScalarTower X R A
this : Module ↥S ↥T := (inclusion h).toModule
x : X
s : ↥S
t : ↥T
rw :
  (↑(HMul.hMul (α := ↥S) ((algebraMap R ↥S : (a : R) → ↥S) (HSMul.hSMul (β := R) x 1) : ↥S) s • t) : A) =
    (↑(HMul.hMul (α := ↥T) ((algebraMap R ↥T : (a : R) → ↥T) (HSMul.hSMul (β := R) x 1) : ↥T) (s • t)) : A)
⊢ (↑((x • s) • t) : A) = (↑(x • s • t) : A)

Tactic:
rw [← one_smul R s, ← smul_assoc, one_smul, ← one_smul R (s • t), ← smul_assoc,
      Algebra.smul_def, Algebra.smul_def]

Premises used: smul_assoc, one_smul, HSMul.hSMul, Algebra.smul_def
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
X : Type u_1
inst_5 : SMul X R
inst_6 : SMul X A
inst_7 : IsScalarTower X R A
this : Module ↥S ↥T := (inclusion h).toModule
x : X
s : ↥S
t : ↥T
⊢ (↑(HMul.hMul (α := ↥S) ((algebraMap R ↥S : (a : R) → ↥S) (HSMul.hSMul (β := R) x 1) : ↥S) s • t) : A) =
    (↑(HMul.hMul (α := ↥T) ((algebraMap R ↥T : (a : R) → ↥T) (HSMul.hSMul (β := R) x 1) : ↥T) (s • t)) : A)

Tactic:
apply mul_assoc

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
X : Type u_1
inst_5 : MulAction A X
⊢ IsScalarTower.{v, v, u_1} (↥S) (↥T) X

Tactic:
letI := (inclusion h).toModule; ⟨fun _ ↦ mul_smul _⟩

Premises used: RingHom.toMonoidWithZeroHom, MonoidWithZeroHom.toZeroHom, Subalgebra.inclusion, AlgHom.toRingHom, IsScalarTower.mk, DFunLike.coe, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S T U : Subalgebra R A
h_1 : S ≤ T
this : Module ↥S ↥T := (inclusion h_1).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ (↑(HSMul.hSMul (β := ↥T) x 1) : A) = (↑(HSMul.hSMul (β := ↥T) y 1) : A)

Tactic:
Subtype.ext_iff.mp (h 1)

Premises used: Subtype.ext_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S T U : Subalgebra R A
h_1 : S ≤ T
this : Module ↥S ↥T := (inclusion h_1).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
h₁ : (↑x : A) = (↑(HSMul.hSMul (β := ↥T) x 1) : A)
h₂ : (↑y : A) = (↑(HSMul.hSMul (β := ↥T) y 1) : A)
⊢ (↑x : A) = (↑y : A)

Tactic:
convert! Subtype.ext_iff.mp (h 1) using 1

Premises used: Subtype.ext_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S T U : Subalgebra R A
h_1 : S ≤ T
this : Module ↥S ↥T := (inclusion h_1).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ (↑x : A) = (↑(HSMul.hSMul (β := ↥T) x 1) : A)

Tactic:
(mul_one _).symm

Premises used: Set.Mem, mul_one, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S T U : Subalgebra R A
h_1 : S ≤ T
this : Module ↥S ↥T := (inclusion h_1).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ (↑x : A) = (↑(HSMul.hSMul (β := ↥T) x 1) : A)

Tactic:
exact (mul_one _).symm

Premises used: mul_one, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S T U : Subalgebra R A
h_1 : S ≤ T
this : Module ↥S ↥T := (inclusion h_1).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ (↑y : A) = (↑(HSMul.hSMul (β := ↥T) y 1) : A)

Tactic:
(mul_one _).symm

Premises used: Set.Mem, mul_one, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S T U : Subalgebra R A
h_1 : S ≤ T
this : Module ↥S ↥T := (inclusion h_1).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ (↑y : A) = (↑(HSMul.hSMul (β := ↥T) y 1) : A)

Tactic:
exact (mul_one _).symm

Premises used: mul_one, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
h : S = T
⊢ (S.equivOfEq T h).symm = T.equivOfEq S ⋯

Tactic:
rfl

Premises used: AlgEquiv.symm, Subalgebra.equivOfEq, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h :
  ∀ (a : ↥S),
    Eq.{v + 1} (α := A) (↑((S.equivOfEq S ⋯ : (a : ↥S) → ↥S) a) : A) (↑((AlgEquiv.refl : (a : ↥S) → ↥S) a) : A)
⊢ S.equivOfEq S ⋯ = AlgEquiv.refl

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
a : ↥S
⊢ Eq.{v + 1} (α := A) (↑((S.equivOfEq S ⋯ : (a : ↥S) → ↥S) a) : A) (↑((AlgEquiv.refl : (a : ↥S) → ↥S) a) : A)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T U : Subalgebra R A
hST : S = T
hTU : T = U
⊢ (S.equivOfEq T hST).trans (T.equivOfEq U hTU) = S.equivOfEq U ⋯

Tactic:
rfl

Premises used: Set.Mem, Equiv.trans, Subalgebra.equivOfEq, AlgEquiv.trans, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
rw : map f S.val.range = map f S
rw₁ rw₂ : map f S = map f S
⊢ (f.comp S.val).range = map f S

Tactic:
rw [AlgHom.range_comp, range_val]

Premises used: Subalgebra.range_val, AlgHom.range_comp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
x : ↥S
⊢ Eq.{w + 1} (α := B) ((↑((AlgHom.subalgebraMap S f : (a : ↥S) → ↥(map f S)) x) : B) : B)
    ((f : (a : A) → B) (↑x : A) : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
⊢ Function.Surjective.{v + 1, w + 1} (α := ↥S) (β := ↥(map f S)) (⇑(AlgHom.subalgebraMap S f) : (a : ↥S) → ↥(map f S))

Tactic:
f.toAddMonoidHom.addSubmonoidMap_surjective S.toAddSubmonoid

Premises used: Set.Mem, AddMonoidHom.addSubmonoidMap_surjective, Subalgebra.toAddSubmonoid, RingHom.toAddMonoidHom, AlgHom.toRingHom
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
x : ↥S
⊢ Eq.{w + 1} (α := B) ((↑((S.equivMapOfInjective f hf : (a : ↥S) → ↥(map f S)) x) : B) : B)
    ((f : (a : A) → B) (↑x : A) : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
α : Type u_1
inst_3 : SMul A α
S : Subalgebra R A
g : ↥S
m : α
⊢ g • m = (↑g : A) • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S_1 T U : Subalgebra R A
h : S_1 ≤ T
α : Type u_1
β : Type u_2
inst_5 : SMul A β
inst_6 : SMul α β
inst_7 : SMulCommClass A α β
S : Subalgebra R A
⊢ SMulCommClass.{v, u_1, u_2} (↥S) α β

Tactic:
S.toSubsemiring.smulCommClass_left

Premises used: Set.Mem, Subalgebra.toSubsemiring, Subsemiring.smulCommClass_left
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S_1 T U : Subalgebra R A
h : S_1 ≤ T
α : Type u_1
β : Type u_2
inst_5 : SMul α β
inst_6 : SMul A β
inst_7 : SMulCommClass α A β
S : Subalgebra R A
⊢ SMulCommClass.{u_1, v, u_2} α (↥S) β

Tactic:
S.toSubsemiring.smulCommClass_right

Premises used: Set.Mem, Subalgebra.toSubsemiring, Subsemiring.smulCommClass_right
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
α : Type u_1
β : Type u_2
inst_5 : SMul α β
inst_6 : SMul A α
inst_7 : SMul A β
inst_8 : IsScalarTower A α β
⊢ IsScalarTower.{v, u_1, u_2} (↥S) α β

Tactic:
inferInstanceAs (IsScalarTower S.toSubsemiring α β)

Premises used: _private.0.Subalgebra.isScalarTower_left._proof_1
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
α : Type u_1
β : Type u_2
inst_5 : SMul α R
inst_6 : SMul α A
inst_7 : IsScalarTower α R A
inst_8 : SMul A β
inst_9 : SMul α β
inst_10 : IsScalarTower α A β
⊢ IsScalarTower.{u_1, v, u_2} α (↥S) β

Tactic:
⟨fun a b c ↦ smul_assoc a b.1 c⟩

Premises used: smul_assoc, IsScalarTower.mk, Subtype.val
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
α : Type u_1
β : Type u_2
inst_5 : SMul α R
inst_6 : SMul α A
inst_7 : IsScalarTower α R A
inst_8 : SMul β R
inst_9 : SMul β A
inst_10 : IsScalarTower β R A
inst_11 : SMul α β
inst_12 : IsScalarTower α β A
⊢ IsScalarTower.{u_1, u_2, v} α β ↥S

Tactic:
⟨fun a b c ↦ Subtype.ext (smul_assoc a b c.1)⟩

Premises used: smul_assoc, IsScalarTower.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S_1 T U : Subalgebra R A
h : S_1 ≤ T
α : Type u_1
β : Type u_2
inst_5 : SMul A α
inst_6 : FaithfulSMul A α
S : Subalgebra R A
⊢ FaithfulSMul.{v, u_1} (↥S) α

Tactic:
inferInstanceAs (FaithfulSMul S.toSubsemiring α)

Premises used: _private.0.Subalgebra.instFaithfulSMulSubtypeMem._proof_1
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
α : Type u_1
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring α
inst_3 : Algebra R A
inst_4 : Algebra A α
S : Subalgebra R A
⊢ Eq (α := RingHom.{u_4, u_1} (↥S) α) (algebraMap (↥S) α)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A α) (↑S.val : ↥S →+* A))

Tactic:
rfl

Premises used: Subsemiring.subtype, Set.Mem, Subsemiring.ofClass, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
α : Type u_1
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring α
inst_3 : Algebra R A
inst_4 : Algebra A α
S : Subalgebra R A
s : ↥S
⊢ Eq.{u_1 + 1} (α := α) ((algebraMap (↥S) α : (a : ↥S) → α) s : α) ((algebraMap A α : (a : A) → α) (↑s : A) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
α : Type u_1
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring α
inst_3 : Algebra R A
inst_4 : Algebra A α
S : Subalgebra R A
a : A
ha : a ∈ S
⊢ Eq.{u_1 + 1} (α := α) ((algebraMap (↥S) α : (a : ↥S) → α) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) a ha) : α)
    ((algebraMap A α : (a : A) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
⊢ (algebraMap (↥S) A : (a : ↥S) → A) x = (↑x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
rw :
  RingHom.rangeS (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A A) (↑S.val : ↥S →+* A)) =
    S.toSubsemiring
rw₁ : RingHom.rangeS (RingHom.comp (RingHom.id A) (↑S.val : ↥S →+* A)) = S.toSubsemiring
rw₂ : RingHom.rangeS (↑S.val : ↥S →+* A) = S.toSubsemiring
rw₃ : S.subtype.rangeS = S.toSubsemiring
rw₄ rw₅ : S.toSubsemiring = S.toSubsemiring
⊢ RingHom.rangeS (R := ↥S) (algebraMap (↥S) A) = S.toSubsemiring

Tactic:
rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubsemiring_subtype,
    Subsemiring.rangeS_subtype]

Premises used: Algebra.algebraMap_self, Subsemiring.rangeS_subtype, Subalgebra.algebraMap_eq, Subalgebra.toSubsemiring_subtype, RingHom.id_comp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Subalgebra R A
rw :
  RingHom.range (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A A) (↑S.val : ↥S →+* A)) = S.toSubring
rw₁ : RingHom.range (RingHom.comp (RingHom.id A) (↑S.val : ↥S →+* A)) = S.toSubring
rw₂ : RingHom.range (↑S.val : ↥S →+* A) = S.toSubring
rw₃ : S.toSubring.subtype.range = S.toSubring
rw₄ rw₅ : S.toSubring = S.toSubring
⊢ RingHom.range (R := ↥S) (algebraMap (↥S) A) = S.toSubring

Tactic:
rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubring_subtype,
    Subring.range_subtype]

Premises used: Algebra.algebraMap_self, Subalgebra.algebraMap_eq, Subalgebra.toSubring_subtype, Subring.range_subtype, RingHom.id_comp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ Set.range (ι := ↥S) (⇑(algebraMap (↥S) A) : (a : ↥S) → A) = (↑S : Set A)

Tactic:
SetLike.ext'_iff.mp S.rangeS_algebraMap

Premises used: setOf, Subalgebra.rangeS_algebraMap, Iff.mp, SetLike.ext'_iff, Set.range
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S_1 T U : Subalgebra R A
h : S_1 ≤ T
α : Type u_1
β : Type u_2
inst_5 : IsDomain A
S : Subalgebra R A
r : ↥S
hr : IsRegular r
⊢ IsRegular (↑r : A)

Tactic:
simpa [isRegular_iff_ne_zero] using hr.ne_zero

Premises used: isRegular_iff_ne_zero, IsRegular.ne_zero
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S_1 T U : Subalgebra R A
h : S_1 ≤ T
α : Type u_1
β : Type u_2
inst_5 : IsDomain A
S : Subalgebra R A
⊢ ∀ (r : ↥S) (m : A), (↑r : A) • m = r • m

Tactic:
simp [smul_def]

Premises used: Subalgebra.smul_def
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ Membership.mem (α := A) (Set.center A) ((algebraMap R A : (a : R) → A) r : A)

Tactic:
simp only [Semigroup.mem_center_iff, commutes, forall_const]

Premises used: Semigroup.mem_center_iff, forall_const, Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
⊢ Eq (α := Subring A) (toSubring (center R A)) (Subring.center A)

Tactic:
rfl

Premises used: Subring.center, setOf, Set.center, Subsemiring.center, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
⊢ Membership.mem (γ := Subalgebra R A) (center R A) a ↔ ∀ (b : A), b * a = a * b

Tactic:
Subsemigroup.mem_center_iff

Premises used: Set.Mem, setOf, Subsemigroup.mem_center_iff, Set.center
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
r : R
⊢ Membership.mem (α := A) s.centralizer ((algebraMap R A : (a : R) → A) r : A)

Tactic:
fun _a _h => (Algebra.commutes _ _).symm

Premises used: Set.Mem, setOf, Set.centralizer, Eq.symm, Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ (↑(centralizer R s) : Set A) = s.centralizer

Tactic:
rfl

Premises used: setOf, Set.centralizer, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
z : A
⊢ Membership.mem (γ := Subalgebra R A) (centralizer R s) z ↔ ∀ g ∈ s, g * z = z * g

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.centralizer
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ LE.le (α := Subalgebra R A) (center R A) (centralizer R s)

Tactic:
s.center_subset_centralizer

Premises used: Set.Mem, setOf, Set.center, Set.centralizer, Set.Subset, Set.center_subset_centralizer
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s t : Set A
h : s ⊆ t
⊢ LE.le (α := Subalgebra R A) (centralizer R t) (centralizer R s)

Tactic:
Set.centralizer_subset h

Premises used: Set.Mem, setOf, Set.centralizer, Set.Subset, Set.centralizer_subset
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := Subalgebra R A) (centralizer R Set.univ) (center R A)

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

Premises used: SetLike.ext', Set.centralizer_univ
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Subalgebra R A
⊢ s ≤ centralizer R (↑(centralizer R (↑s : Set A)) : Set A)

Tactic:
Set.subset_centralizer_centralizer

Premises used: Set.Mem, setOf, Set.centralizer, Set.Subset, Set.subset_centralizer_centralizer
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
a : (↑(centralizer R s.centralizer.centralizer) : Set A) = (↑(centralizer R s) : Set A)
⊢ Eq (α := Subalgebra R A) (centralizer R s.centralizer.centralizer) (centralizer R s)

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ (↑(centralizer R s.centralizer.centralizer) : Set A) = (↑(centralizer R s) : Set A)

Tactic:
simp only [coe_centralizer, Set.centralizer_centralizer_centralizer]

Premises used: Set.centralizer_centralizer_centralizer, Subalgebra.coe_centralizer
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
inst : Semiring R
x : R
S : Subsemiring R
⊢ x ∈ subalgebraOfSubsemiring S ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
inst : Ring R
S : Subring R
i : ℤ
⊢ Membership.mem (α := R) S.carrier ((algebraMap ℤ R : (a : ℤ) → R) 0 : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
inst : Ring R
S : Subring R
i_1 : ℤ
i : ℕ
ih : Membership.mem (α := R) S.carrier ((algebraMap ℤ R : (a : ℤ) → R) (↑i : ℤ) : R)
⊢ Membership.mem (α := R) S.carrier ((algebraMap ℤ R : (a : ℤ) → R) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : R)

Tactic:
simpa using S.add_mem ih S.one_mem

Premises used: Subring.add_mem, Subring.one_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
inst : Ring R
S : Subring R
i_1 : ℤ
i : ℕ
ih : Membership.mem (α := R) S.carrier ((algebraMap ℤ R : (a : ℤ) → R) (-(↑i : ℤ)) : R)
rw : HSub.hSub (α := R) (↑(-(↑i : ℤ)) : R) 1 ∈ S
⊢ (↑(HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1) : R) ∈ S

Tactic:
rw [Int.cast_sub, Int.cast_one]

Premises used: Int.cast_sub, Int.cast_one
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
inst : Ring R
S : Subring R
i_1 : ℤ
i : ℕ
ih : Membership.mem (α := R) S.carrier ((algebraMap ℤ R : (a : ℤ) → R) (-(↑i : ℤ)) : R)
⊢ HSub.hSub (α := R) (↑(-(↑i : ℤ)) : R) 1 ∈ S

Tactic:
S.sub_mem ih S.one_mem

Premises used: Set.Mem, Subring.sub_mem, Subring.one_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
inst : Ring R
S : Subring R
i_1 : ℤ
i : ℕ
ih : Membership.mem (α := R) S.carrier ((algebraMap ℤ R : (a : ℤ) → R) (-(↑i : ℤ)) : R)
⊢ HSub.hSub (α := R) (↑(-(↑i : ℤ)) : R) 1 ∈ S

Tactic:
exact S.sub_mem ih S.one_mem

Premises used: Subring.sub_mem, Subring.one_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
inst : Ring R
x : R
S : Subring R
⊢ x ∈ subalgebraOfSubring S ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
x y : A
hx : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) (x * y) : B) ((ψ : (a : A) → B) (x * y) : B)
rw₁ : HMul.hMul (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x * y)
rw₂ :
  HMul.hMul (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
rw₃ :
  HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
rw₄ rw₅ :
  HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B) =
    HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)}
    (x * y)

Tactic:
rw [Set.mem_setOf_eq, map_mul, map_mul, hx, hy]

Premises used: Set.mem_setOf_eq, map_mul