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
carrier : Set A
mul_mem' : ∀ {a b : A}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
toSubsemigroup : Subsemigroup A := { carrier := carrier, mul_mem' := @mul_mem' }
add_mem' : ∀ {a b : A}, a ∈ carrier → b ∈ carrier → a + b ∈ carrier
zero_mem' : 0 ∈ carrier
toAddSubsemigroup : AddSubsemigroup A := { carrier := carrier, add_mem' := @add_mem' }
toAddSubmonoid : AddSubmonoid A := { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' }
algebraMap_mem' : ∀ (r : R), Membership.mem (α := A) carrier ((algebraMap R A : (a : R) → A) r : A)
⊢ 1 ∈ carrier

Tactic:
(algebraMap R A).map_one ▸ algebraMap_mem' 1

Premises used: Algebra.algebraMap, Set.Mem, RingHom.map_one, Eq.rec, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
p q : Subalgebra R A
h : Eq.{v + 1} (α := Set A) ((fun (s : Subalgebra R A) ↦ s.carrier) p) ((fun (s : Subalgebra R A) ↦ s.carrier) q)
mk :
  ∀ (toSubsemiring : Subsemiring A)
    (algebraMap_mem' : ∀ (r : R), Membership.mem (α := A) toSubsemiring.carrier ((algebraMap R A : (a : R) → A) r : A))
    (h :
      Eq.{v + 1} (α := Set A)
        ((fun (s : Subalgebra R A) ↦ s.carrier) { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' })
        ((fun (s : Subalgebra R A) ↦ s.carrier) q)),
    { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' : Subalgebra R A } = q
⊢ p = q

Tactic:
cases p
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
q : Subalgebra R A
toSubsemiring : Subsemiring A
algebraMap_mem' : ∀ (r : R), Membership.mem (α := A) toSubsemiring.carrier ((algebraMap R A : (a : R) → A) r : A)
h :
  Eq.{v + 1} (α := Set A)
    ((fun (s : Subalgebra R A) ↦ s.carrier) { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' })
    ((fun (s : Subalgebra R A) ↦ s.carrier) q)
mk :
  ∀ (toSubsemiring_1 : Subsemiring A)
    (algebraMap_mem'_1 :
      ∀ (r : R), Membership.mem (α := A) toSubsemiring_1.carrier ((algebraMap R A : (a : R) → A) r : A))
    (h :
      Eq.{v + 1} (α := Set A)
        ((fun (s : Subalgebra R A) ↦ s.carrier) { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' })
        ((fun (s : Subalgebra R A) ↦ s.carrier)
          { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1 })),
    { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' : Subalgebra R A } =
      { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1 }
⊢ { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' : Subalgebra R A } = q

Tactic:
cases q
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
toSubsemiring : Subsemiring A
algebraMap_mem' : ∀ (r : R), Membership.mem (α := A) toSubsemiring.carrier ((algebraMap R A : (a : R) → A) r : A)
toSubsemiring_1 : Subsemiring A
algebraMap_mem'_1 : ∀ (r : R), Membership.mem (α := A) toSubsemiring_1.carrier ((algebraMap R A : (a : R) → A) r : A)
h :
  Eq.{v + 1} (α := Set A)
    ((fun (s : Subalgebra R A) ↦ s.carrier) { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' })
    ((fun (s : Subalgebra R A) ↦ s.carrier) { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1 })
mk : toSubsemiring = toSubsemiring_1
⊢ { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' : Subalgebra R A } =
    { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
toSubsemiring : Subsemiring A
algebraMap_mem' : ∀ (r : R), Membership.mem (α := A) toSubsemiring.carrier ((algebraMap R A : (a : R) → A) r : A)
toSubsemiring_1 : Subsemiring A
algebraMap_mem'_1 : ∀ (r : R), Membership.mem (α := A) toSubsemiring_1.carrier ((algebraMap R A : (a : R) → A) r : A)
h :
  Eq.{v + 1} (α := Set A)
    ((fun (s : Subalgebra R A) ↦ s.carrier) { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' })
    ((fun (s : Subalgebra R A) ↦ s.carrier) { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1 })
⊢ toSubsemiring = toSubsemiring_1

Tactic:
SetLike.coe_injective' h

Premises used: SetLike.coe_injective'
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
toSubsemiring : Subsemiring A
algebraMap_mem' : ∀ (r : R), Membership.mem (α := A) toSubsemiring.carrier ((algebraMap R A : (a : R) → A) r : A)
toSubsemiring_1 : Subsemiring A
algebraMap_mem'_1 : ∀ (r : R), Membership.mem (α := A) toSubsemiring_1.carrier ((algebraMap R A : (a : R) → A) r : A)
h :
  Eq.{v + 1} (α := Set A)
    ((fun (s : Subalgebra R A) ↦ s.carrier) { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' })
    ((fun (s : Subalgebra R A) ↦ s.carrier) { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1 })
⊢ toSubsemiring = toSubsemiring_1

Tactic:
exact SetLike.coe_injective' h

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 : Subsemiring A
h : ∀ (r : R), Membership.mem (α := A) s.carrier ((algebraMap R A : (a : R) → A) r : A)
⊢ (↑{ toSubsemiring := s, algebraMap_mem' := h : Subalgebra R A } : Set A) = (↑s : Set A)

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
s : Subsemiring A
h : ∀ (r : R), Membership.mem (α := A) s.carrier ((algebraMap R A : (a : R) → A) r : A)
x : A
⊢ x ∈ { toSubsemiring := s, algebraMap_mem' := h : Subalgebra R A } ↔ x ∈ s

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
s : Set A
h :
  (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
    (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧
      ∀ (r : R), Membership.mem (α := A) s ((algebraMap R A : (a : R) → A) r : A)
⊢ 1 ∈ s

Tactic:
simpa using h.2.2 1

Premises used: And.right, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
s : Set A
h :
  (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
    (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧
      ∀ (r : R), Membership.mem (α := A) s ((algebraMap R A : (a : R) → A) r : A)
⊢ 0 ∈ s

Tactic:
simpa using h.2.2 0

Premises used: And.right, OfNat.ofNat
-- 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
x : A
⊢ x ∈ S.toSubsemiring ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.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
x : A
⊢ x ∈ s.carrier ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.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 : ∀ (x : A), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.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
⊢ (↑S.toSubsemiring : Set A) = (↑S : Set A)

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
S T : Subalgebra R A
h : S.toSubsemiring = T.toSubsemiring
x : A
rw : x ∈ S.toSubsemiring ↔ x ∈ T
rw₁ : x ∈ S.toSubsemiring ↔ x ∈ T.toSubsemiring
rw₂ rw₃ : x ∈ T.toSubsemiring ↔ x ∈ T.toSubsemiring
⊢ x ∈ S ↔ x ∈ T

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

Premises used: Subalgebra.mem_toSubsemiring
-- 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 U : Subalgebra R A
⊢ S.toSubsemiring = U.toSubsemiring ↔ S = U

Tactic:
toSubsemiring_injective.eq_iff

Premises used: Function.Injective.eq_iff, Subalgebra.toSubsemiring_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 : Subalgebra 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.Subalgebra.Basic
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : SetLike S A
inst_4 : OneMemClass S A
inst_5 : SMulMemClass S R A
s : S
r : R
⊢ Membership.mem.{u_3, u_1} (α := A) s ((algebraMap R A : (a : R) → A) r : A)

Tactic:
Algebra.algebraMap_eq_smul_one (A := A) r ▸ SMulMemClass.smul_mem r (one_mem s)

Premises used: SMulMemClass.smul_mem, Eq.rec, Algebra.algebraMap_eq_smul_one, OneMemClass.one_mem, 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 : Subalgebra R A
r : R
⊢ Membership.mem (α := A) S ((algebraMap R A : (a : R) → A) r : A)

Tactic:
algebraMap_mem S r

Premises used: algebraMap_mem
-- 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
⊢ RingHom.rangeS (algebraMap R A) ≤ S.toSubsemiring

Tactic:
fun _x ⟨r, hr⟩ =>
  hr ▸ S.algebraMap_mem r

Premises used: Membership.mem, Eq.rec, Subalgebra.toSubsemiring, _private.0.Subalgebra.rangeS_le.match_1, Subalgebra.algebraMap_mem
-- 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
⊢ Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ⊆ (↑S : Set A)

Tactic:
fun _x ⟨r, hr⟩ => hr ▸ S.algebraMap_mem r

Premises used: Membership.mem, Eq.rec, _private.0.Subalgebra.range_subset.match_1, Set.Subset, SetLike.coe, Subalgebra.algebraMap_mem
-- 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
⊢ Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ≤ (↑S : Set A)

Tactic:
S.range_subset

Premises used: Subalgebra.range_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
S : Subalgebra R A
x : A
hx : x ∈ S
r : R
⊢ r • x ∈ S

Tactic:
SMulMemClass.smul_mem r hx

Premises used: SMulMemClass.smul_mem
-- 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
⊢ 1 ∈ S

Tactic:
one_mem S

Premises used: OneMemClass.one_mem
-- 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
x y : A
hx : x ∈ S
hy : y ∈ S
⊢ x * y ∈ S

Tactic:
mul_mem hx hy

Premises used: MulMemClass.mul_mem
-- 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
x : A
hx : x ∈ S
n : ℕ
⊢ x ^ n ∈ S

Tactic:
pow_mem hx n

Premises used: pow_mem
-- 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
⊢ 0 ∈ S

Tactic:
zero_mem S

Premises used: Set.Mem, ZeroMemClass.zero_mem
-- 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
x y : A
hx : x ∈ S
hy : y ∈ S
⊢ x + y ∈ S

Tactic:
add_mem hx hy

Premises used: AddMemClass.add_mem
-- 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
x : A
hx : x ∈ S
n : ℕ
⊢ n • x ∈ S

Tactic:
nsmul_mem hx n

Premises used: nsmul_mem
-- 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
n : ℕ
⊢ (↑n : A) ∈ S

Tactic:
natCast_mem S n

Premises used: natCast_mem
-- 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
L : List A
h : ∀ x ∈ L, x ∈ S
⊢ L.prod ∈ S

Tactic:
list_prod_mem h

Premises used: list_prod_mem, Set.Mem
-- 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
L : List A
h : ∀ x ∈ L, x ∈ S
⊢ L.sum ∈ S

Tactic:
list_sum_mem h

Premises used: Set.Mem, list_sum_mem
-- 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
m : Multiset A
h : ∀ x ∈ m, x ∈ S
⊢ m.sum ∈ S

Tactic:
multiset_sum_mem m h

Premises used: multiset_sum_mem
-- 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
ι : Type w
t : Finset ι
f : ι → A
h : ∀ x ∈ t, f x ∈ S
⊢ ∑ x ∈ t, f x ∈ S

Tactic:
sum_mem h

Premises used: sum_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
m : Multiset A
h : ∀ x ∈ m, x ∈ S
⊢ m.prod ∈ S

Tactic:
multiset_prod_mem m h

Premises used: multiset_prod_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
ι : Type w
t : Finset ι
f : ι → A
h : ∀ x ∈ t, f x ∈ S
⊢ ∏ x ∈ t, f x ∈ S

Tactic:
prod_mem h

Premises used: prod_mem
-- 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
⊢ 1 ∈ S.toNonUnitalSubalgebra

Tactic:
S.one_mem

Premises used: Set.Mem, Subalgebra.one_mem
-- 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
x : A
⊢ x ∈ S.toNonUnitalSubalgebra ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.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
x x_1 : Subalgebra R A
⊢ x.toNonUnitalSubalgebra = x_1.toNonUnitalSubalgebra → x = x_1

Tactic:
simp [SetLike.ext_iff]

Premises used: SetLike.ext_iff
-- 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 U : Subalgebra R A
⊢ S.toNonUnitalSubalgebra = U.toNonUnitalSubalgebra ↔ S = U

Tactic:
toNonUnitalSubalgebra_injective.eq_iff

Premises used: Function.Injective.eq_iff, Subalgebra.toNonUnitalSubalgebra_injective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R_1 : Type u
A_1 : Type v
B : Type w
C : Type w'
inst : CommSemiring R_1
inst_1 : Semiring A_1
inst_2 : Algebra R_1 A_1
inst_3 : Semiring B
inst_4 : Algebra R_1 B
inst_5 : Semiring C
inst_6 : Algebra R_1 C
S : Subalgebra R_1 A_1
R : Type u_1
A : Type u_2
inst_7 : CommRing R
inst_8 : Ring A
inst_9 : Algebra R A
⊢ SubringClass (Subalgebra R A) A

Tactic:
{ Subalgebra.instSubsemiringClass with
    neg_mem := fun {S x} hx => neg_one_smul R x ▸ S.smul_mem hx _ }

Premises used: SubringClass.mk, Subalgebra.instSubsemiringClass
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : A
hx : x ∈ S
⊢ -x ∈ S

Tactic:
neg_mem hx

Premises used: NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x y : A
hx : x ∈ S
hy : y ∈ S
⊢ x - y ∈ S

Tactic:
sub_mem hx hy

Premises used: sub_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : A
hx : x ∈ S
n : ℤ
⊢ n • x ∈ S

Tactic:
zsmul_mem hx n

Premises used: zsmul_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
n : ℤ
⊢ (↑n : A) ∈ S

Tactic:
intCast_mem S n

Premises used: intCast_mem, Set.Mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : A
⊢ x ∈ S.toSubring ↔ x ∈ S

Tactic:
Iff.rfl

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

Tactic:
rfl

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

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

Premises used: Subalgebra.mem_toSubring
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S U : Subalgebra R A
⊢ S.toSubring = U.toSubring ↔ S = U

Tactic:
toSubring_injective.eq_iff

Premises used: Subalgebra.toSubring_injective, Function.Injective.eq_iff
-- 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
x : A
⊢ Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.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
⊢ (↑((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) : Set A) = (↑S : Set A)

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
⊢ Function.Injective.{v + 1, v + 1} (α := Subalgebra R A) (β := Submodule R A)
    (⇑toSubmodule : (a : Subalgebra R A) → Submodule R A)

Tactic:
fun _S₁ _S₂ h => SetLike.ext (SetLike.ext_iff.mp h :)

Premises used: SetLike.ext_iff, SetLike.ext, Iff.mp, Function.Injective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
S : Subalgebra 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:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
S : Subalgebra R A
inst_7 : CommSemiring R'
inst_8 : SMul R' R
inst_9 : Algebra R' A
inst_10 : IsScalarTower R' R A
x : R'
rw : Membership.mem (α := A) S ((algebraMap R A : (a : R) → A) (HSMul.hSMul (β := R) x 1) : A)
⊢ Membership.mem (α := A) S ((algebraMap R' A : (a : R') → A) x : A)

Tactic:
rw [Algebra.algebraMap_eq_smul_one, ← smul_one_smul R x (1 : A), ←
      Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one, smul_one_smul, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
S : Subalgebra R A
inst_7 : CommSemiring R'
inst_8 : SMul R' R
inst_9 : Algebra R' A
inst_10 : IsScalarTower R' R A
x : R'
⊢ Membership.mem (α := A) S ((algebraMap R A : (a : R) → A) (HSMul.hSMul (β := R) x 1) : A)

Tactic:
algebraMap_mem S _

Premises used: algebraMap_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
S : Subalgebra R A
inst_7 : CommSemiring R'
inst_8 : SMul R' R
inst_9 : Algebra R' A
inst_10 : IsScalarTower R' R A
x : R'
⊢ Membership.mem (α := A) S ((algebraMap R A : (a : R) → A) (HSMul.hSMul (β := R) x 1) : A)

Tactic:
exact algebraMap_mem S _

Premises used: algebraMap_mem
-- 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
r : R
hr : Membership.mem (α := A) S ((algebraMap R A : (a : R) → A) r : A)
⊢ Eq.{v + 1} (α := ↥S) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) ((algebraMap R A : (a : R) → A) r) hr : ↥S)
    ((algebraMap R ↥S : (a : R) → ↥S) r : ↥S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
S : Subalgebra R A
inst_7 : IsTorsionFree R A
⊢ IsTorsionFree.{u, v} R ↥S

Tactic:
S.toSubmodule.instIsTorsionFree

Premises used: Set.Mem, Subalgebra.toSubmodule, Submodule.instIsTorsionFree, DFunLike.coe
-- 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
x y : ↥S
⊢ (↑(x + y) : A) = (↑x : A) + (↑y : A)

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
S : Subalgebra R A
x y : ↥S
⊢ (↑(x * y) : A) = (↑x : A) * (↑y : A)

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
S : Subalgebra R A
⊢ Eq.{v + 1} (α := A) (↑0 : A) 0

Tactic:
rfl

Premises used: rfl