awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
inst_11 : DistribMulAction R B
inst_12 : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
⊢ Eq (α := B × C)
    (Function.prod (α := fun (a : A) ↦ B) (β := fun (a : A) ↦ C) (⇑f : (a : A) → B) (⇑g : (a : A) → C) 0 : B × C)
    (0 : B × C)

Tactic:
simp only [Function.prod_apply, Prod.mk_zero_zero, map_zero]

Premises used: Prod.mk_zero_zero, map_zero, Function.prod_apply
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
inst_11 : DistribMulAction R B
inst_12 : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
x y : A
⊢ Function.prod (α := fun (a : A) ↦ B) (β := fun (a : A) ↦ C) (⇑f : (a : A) → B) (⇑g : (a : A) → C) (x + y) =
    HAdd.hAdd (α := B × C) (β := B × C)
      (Function.prod (α := fun (a : A) ↦ B) (β := fun (a : A) ↦ C) (⇑f : (a : A) → B) (⇑g : (a : A) → C) x : B × C)
      (Function.prod (α := fun (a : A) ↦ B) (β := fun (a : A) ↦ C) (⇑f : (a : A) → B) (⇑g : (a : A) → C) y : B × C)

Tactic:
simp only [Function.prod_apply, Prod.mk_add_mk, map_add]

Premises used: Prod.mk_add_mk, map_add, Function.prod_apply
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
inst_11 : DistribMulAction R B
inst_12 : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
x y : A
⊢ Function.prod (α := fun (a : A) ↦ B) (β := fun (a : A) ↦ C) (⇑f : (a : A) → B) (⇑g : (a : A) → C) (x * y) =
    HMul.hMul (α := B × C) (β := B × C)
      (Function.prod (α := fun (a : A) ↦ B) (β := fun (a : A) ↦ C) (⇑f : (a : A) → B) (⇑g : (a : A) → C) x : B × C)
      (Function.prod (α := fun (a : A) ↦ B) (β := fun (a : A) ↦ C) (⇑f : (a : A) → B) (⇑g : (a : A) → C) y : B × C)

Tactic:
simp only [Function.prod_apply, Prod.mk_mul_mk, map_mul]

Premises used: map_mul, Prod.mk_mul_mk, Function.prod_apply
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
inst : Monoid R
A : Type v
B : Type w
C : Type w₁
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : NonUnitalNonAssocSemiring C
inst_5 : DistribMulAction R B
inst_6 : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
⊢ Eq (α := (a : A) → B × C) (⇑(f.prod g) : (a : A) → B × C)
    (Function.prod (α := fun (a : A) ↦ B) (β := fun (a : A) ↦ C) (⇑f : (a : A) → B) (⇑g : (a : A) → C))

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
inst : Monoid R
A : Type v
B : Type w
C : Type w₁
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : NonUnitalNonAssocSemiring C
inst_5 : DistribMulAction R B
inst_6 : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
⊢ comp (fst R B C) (f.prod g) = f

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
inst : Monoid R
A : Type v
B : Type w
C : Type w₁
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : NonUnitalNonAssocSemiring C
inst_5 : DistribMulAction R B
inst_6 : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
⊢ comp (snd R B C) (f.prod g) = g

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
inst : Monoid R
A : Type v
B : Type w
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : DistribMulAction R B
⊢ Eq (α := A × B →ₙₐ[R] A × B) (prod (fst R A B) (snd R A B)) 1

Tactic:
coe_injective Function.prod_fst_snd

Premises used: Function.prod_fst_snd, NonUnitalAlgHom.coe_injective
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
inst : Monoid R
A : Type v
B : Type w
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : DistribMulAction R B
⊢ Eq (α := (a : A) → A × B) (⇑(inl R A B) : (a : A) → A × B) fun (x : A) ↦ (x, 0)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
inst : Monoid R
A : Type v
B : Type w
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : DistribMulAction R B
x : A
⊢ Eq (α := A × B) ((inl R A B : (a : A) → A × B) x : A × B) ((x, 0) : A × B)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
inst : Monoid R
A : Type v
B : Type w
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : DistribMulAction R B
⊢ Eq (α := (a : B) → A × B) (⇑(inr R A B) : (a : B) → A × B) (Prod.mk 0)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
inst : Monoid R
A : Type v
B : Type w
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : DistribMulAction R B
x : B
⊢ Eq (α := A × B) ((inr R A B : (a : B) → A × B) x : A × B) ((0, x) : A × B)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R_1 : Type u
S : Type u₁
F : Type u_1
R : Type u_2
inst : CommSemiring R
A : Type u_3
B : Type u_4
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
⊢ NonUnitalAlgHomClass F R A B

Tactic:
{ ‹AlgHomClass F R A B› with map_smulₛₗ := map_smul }

Premises used: NonUnitalAlgSemiHomClass.mk
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
B : Type u_4
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ (↑f : A →ₙₐ[R] B) = NonUnitalAlgHomClass.toNonUnitalAlgHom f

Tactic:
rfl

Premises used: AlgHom.toNonUnitalAlgHom, rfl, NonUnitalAlgHomClass.toNonUnitalAlgHom
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R_1 : Type u
S_1 : Type u₁
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : Monoid R
inst_1 : Monoid S
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : MulAction R S
inst_5 : DistribMulAction S A
inst_6 : DistribMulAction S B
inst_7 : DistribMulAction R A
inst_8 : DistribMulAction R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₙₐ[S] B
r : R
x : A
⊢ (f : (a : A) → B) (HSMul.hSMul (β := S) r 1 • x) =
    HSMul.hSMul (β := B) (HSMul.hSMul (β := S) r 1) ((f : (a : A) → B) x : B)

Tactic:
have := map_smul f (r • 1) x
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R_1 : Type u
S_1 : Type u₁
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : Monoid R
inst_1 : Monoid S
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : MulAction R S
inst_5 : DistribMulAction S A
inst_6 : DistribMulAction S B
inst_7 : DistribMulAction R A
inst_8 : DistribMulAction R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₙₐ[S] B
r : R
x : A
this :
  (f : (a : A) → B) (HSMul.hSMul (β := S) r 1 • x) =
    HSMul.hSMul (β := B) (HSMul.hSMul (β := S) r 1) ((f : (a : A) → B) x : B)
⊢ MulHom.toFun (NonUnitalRingHom.toMulHom (↑f : A →ₙ+* B)) (r • x) =
    HSMul.hSMul (α := R) ((MonoidHom.id R : (a : R) → R) r : R)
      (MulHom.toFun (NonUnitalRingHom.toMulHom (↑f : A →ₙ+* B)) x)

Tactic:
simpa
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : Monoid R
inst_1 : Monoid S
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : MulAction R S
inst_5 : DistribMulAction S A
inst_6 : DistribMulAction S B
inst_7 : DistribMulAction R A
inst_8 : DistribMulAction R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₙₐ[S] B
x : A
⊢ Eq.{u_4 + 1} (α := B) ((restrictScalars R f : (a : A) → B) x : B) ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : Monoid R
inst_1 : Monoid S
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : MulAction R S
inst_5 : DistribMulAction S A
inst_6 : DistribMulAction S B
inst_7 : DistribMulAction R A
inst_8 : DistribMulAction R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₙₐ[S] B
⊢ Eq (α := A →ₙ+* B) (↑(restrictScalars R f) : A →ₙ+* B) (↑f : A →ₙ+* B)

Tactic:
rfl

Premises used: NonUnitalAlgHom.restrictScalars, MulHomClass.toMulHom, NonUnitalRingHomClass.toNonUnitalRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : Monoid R
inst_1 : Monoid S
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : MulAction R S
inst_5 : DistribMulAction S A
inst_6 : DistribMulAction S B
inst_7 : DistribMulAction R A
inst_8 : DistribMulAction R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₙₐ[S] B
⊢ Eq (α := (a : A) → B) (⇑(restrictScalars R f) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : Monoid R
inst_1 : Monoid S
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : MulAction R S
inst_5 : DistribMulAction S A
inst_6 : DistribMulAction S B
inst_7 : DistribMulAction R A
inst_8 : DistribMulAction R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
⊢ Function.Injective (α := A →ₙₐ[S] B) (β := A →ₙₐ[R] B) (restrictScalars R)

Tactic:
fun _ _ h ↦ ext (congr_fun h :)

Premises used: NonUnitalAlgHom.congr_fun, Function.Injective, NonUnitalAlgHom.ext
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SetLike S A
inst_4 : NonUnitalSubsemiringClass S A
hSR : SMulMemClass S R A
s : S
x : ↥s
⊢ (subtype s : (a : ↥s) → A) x = (↑x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SetLike S A
inst_4 : NonUnitalSubsemiringClass S A
hSR : SMulMemClass S R A
s : S
⊢ Function.Injective (α := ↥s) (β := A) (⇑(subtype s) : (a : ↥s) → A)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SetLike S A
inst_4 : NonUnitalSubsemiringClass S A
hSR : SMulMemClass S R A
s : S
⊢ Eq (α := (a : ↥s) → A) (⇑(subtype s) : (a : ↥s) → A) (Subtype.val (p := fun (x : A) ↦ x ∈ s))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
x t : NonUnitalSubalgebra R A
s : NonUnitalSubsemiring A
hs : ∀ (c : R) {x : A}, x ∈ s.carrier → c • x ∈ s.carrier
⊢ { toNonUnitalSubsemiring := s, smul_mem' := hs : NonUnitalSubalgebra R A }.toNonUnitalSubsemiring =
      t.toNonUnitalSubsemiring →
    { toNonUnitalSubsemiring := s, smul_mem' := hs : NonUnitalSubalgebra R A } = t

Tactic:
congr!
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
s t : NonUnitalSubalgebra R A
⊢ s.toNonUnitalSubsemiring = t.toNonUnitalSubsemiring ↔ s = t

Tactic:
toNonUnitalSubsemiring_injective.eq_iff

Premises used: Function.Injective.eq_iff, NonUnitalSubalgebra.toNonUnitalSubsemiring_injective
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
⊢ Function.Injective.{v + 1, v + 1} (α := NonUnitalSubalgebra R A) toSubmodule

Tactic:
fun _ _ h ↦ SetLike.ext (SetLike.ext_iff.mp h :)

Premises used: SetLike.ext_iff, SetLike.ext, Iff.mp, Function.Injective
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
s t : NonUnitalSubalgebra R A
⊢ s.toSubmodule = t.toSubmodule ↔ s = t

Tactic:
toSubmodule_injective.eq_iff

Premises used: NonUnitalSubalgebra.toSubmodule_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
s : NonUnitalSubalgebra R A
x : A
⊢ x ∈ s.carrier ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S T : NonUnitalSubalgebra R A
h : ∀ (x : A), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
x : A
⊢ x ∈ S.toNonUnitalSubsemiring ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
⊢ (↑S.toNonUnitalSubsemiring : Set A) = (↑S : Set A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
x : A
⊢ x ∈ S.toSubmodule ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
⊢ (↑S.toSubmodule : Set A) = (↑S : Set A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : NonUnitalNonAssocSemiring C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
S : NonUnitalSubalgebra R A
s : Set A
hs : s = (↑S : Set A)
r : R
a : A
⊢ a ∈ (S.copy s hs).carrier → r • a ∈ (S.copy s hs).carrier

Tactic:
simpa [hs] using S.smul_mem r

Premises used: NonUnitalSubalgebra.toSubmodule, Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
s : Set A
hs : s = (↑S : Set A)
⊢ (↑(S.copy s hs) : Set A) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
s : Set A
hs : s = (↑S : Set A)
⊢ S.copy s hs = S

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommRing R
inst_1 : NonUnitalNonAssocRing A
inst_2 : NonUnitalNonAssocRing B
inst_3 : NonUnitalNonAssocRing C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
⊢ NonUnitalSubringClass (NonUnitalSubalgebra R A) A

Tactic:
{ NonUnitalSubalgebra.instNonUnitalSubsemiringClass with
    neg_mem {_ x} hx := neg_one_smul R x ▸ SMulMemClass.smul_mem _ hx }

Premises used: NonUnitalSubalgebra.instNonUnitalSubsemiringClass, NonUnitalSubringClass.mk
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalNonAssocRing A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
x : A
⊢ x ∈ S.toNonUnitalSubring ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalNonAssocRing A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
⊢ (↑S.toNonUnitalSubring : Set A) = (↑S : Set A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalNonAssocRing A
inst_2 : Module R A
S T : NonUnitalSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
rw : x ∈ S.toNonUnitalSubring ↔ x ∈ T
rw₁ : x ∈ S.toNonUnitalSubring ↔ x ∈ T.toNonUnitalSubring
rw₂ rw₃ : x ∈ T.toNonUnitalSubring ↔ x ∈ T.toNonUnitalSubring
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]

Premises used: NonUnitalSubalgebra.mem_toNonUnitalSubring
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalNonAssocRing A
inst_2 : Module R A
S U : NonUnitalSubalgebra R A
⊢ S.toNonUnitalSubring = U.toNonUnitalSubring ↔ S = U

Tactic:
toNonUnitalSubring_injective.eq_iff

Premises used: Function.Injective.eq_iff, NonUnitalSubalgebra.toNonUnitalSubring_injective
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S T : NonUnitalSubalgebra R A
h :
  Eq.{v + 1} (α := Submodule R A) ((fun (S : NonUnitalSubalgebra R A) ↦ S.toSubmodule) S)
    ((fun (S : NonUnitalSubalgebra R A) ↦ S.toSubmodule) T)
⊢ ∀ (x : A), x ∈ S ↔ x ∈ T

Tactic:
apply SetLike.ext_iff.1 h

Premises used: SetLike.ext_iff, Iff.mp
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S T : NonUnitalSubalgebra R A
h :
  Eq.{v + 1} (α := NonUnitalSubsemiring A) ((fun (S : NonUnitalSubalgebra R A) ↦ S.toNonUnitalSubsemiring) S)
    ((fun (S : NonUnitalSubalgebra R A) ↦ S.toNonUnitalSubsemiring) T)
⊢ ∀ (x : A), x ∈ S ↔ x ∈ T

Tactic:
apply SetLike.ext_iff.1 h

Premises used: SetLike.ext_iff, Iff.mp
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommRing R
inst_1 : NonUnitalNonAssocRing A
inst_2 : Module R A
S T : NonUnitalSubalgebra R A
h :
  Eq.{v + 1} (α := NonUnitalSubring A) ((fun (S : NonUnitalSubalgebra R A) ↦ S.toNonUnitalSubring) S)
    ((fun (S : NonUnitalSubalgebra R A) ↦ S.toNonUnitalSubring) T)
⊢ ∀ (x : A), x ∈ S ↔ x ∈ T

Tactic:
apply SetLike.ext_iff.1 h

Premises used: SetLike.ext_iff, Iff.mp
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : NonUnitalNonAssocSemiring C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
S : NonUnitalSubalgebra R A
inst_7 : Semiring R'
inst_8 : SMul R' R
inst_9 : Module R' A
inst_10 : IsScalarTower R' R A
⊢ IsScalarTower.{u', u, v} R' R ↥S

Tactic:
S.toSubmodule.isScalarTower

Premises used: Submodule.isScalarTower, Set.Mem, NonUnitalSubalgebra.toSubmodule
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : NonUnitalNonAssocSemiring C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
S : NonUnitalSubalgebra R A
inst_7 : Module.IsTorsionFree R A
⊢ Module.IsTorsionFree.{u, v} R ↥S

Tactic:
S.toSubmodule.instIsTorsionFree

Premises used: Set.Mem, NonUnitalSubalgebra.toSubmodule, Submodule.instIsTorsionFree
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
x y : ↥S
⊢ (↑(x + y) : A) = (↑x : A) + (↑y : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
x y : ↥S
⊢ (↑(x * y) : A) = (↑x : A) * (↑y : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
⊢ Eq.{v + 1} (α := A) (↑0 : A) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : NonUnitalSubalgebra R A
x : ↥S
⊢ (↑(-x) : A) = -(↑x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : NonUnitalSubalgebra R A
x y : ↥S
⊢ (↑(x - y) : A) = (↑x : A) - (↑y : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R' : Type u'
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : SMul R' R
inst_4 : SMul R' A
inst_5 : IsScalarTower R' R A
r : R'
x : ↥S
⊢ (↑(r • x) : A) = r • (↑x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
x : ↥S
⊢ (↑x : A) = 0 ↔ x = 0

Tactic:
ZeroMemClass.coe_eq_zero

Premises used: ZeroMemClass.coe_eq_zero
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
⊢ Eq (α := ↥S →ₙ+* A) (NonUnitalSubsemiringClass.subtype S) (↑(NonUnitalSubalgebraClass.subtype S) : ↥S →ₙ+* A)

Tactic:
rfl

Premises used: MulHomClass.toMulHom, NonUnitalSubsemiringClass.subtype, NonUnitalRingHomClass.toNonUnitalRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : NonUnitalSubalgebra R A
⊢ Eq (α := ↥S →ₙ+* A) (NonUnitalSubringClass.subtype S) (↑(NonUnitalSubalgebraClass.subtype S) : ↥S →ₙ+* A)

Tactic:
rfl

Premises used: MulHomClass.toMulHom, NonUnitalSubringClass.subtype, NonUnitalRingHomClass.toNonUnitalRingHom, rfl