awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(K i)
hx : (↑x : A) ∈ iSup K
dsimp :
  Eq.{w + 1} (α := B)
    (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (Subtype.mk (p := fun (x : A) ↦ x ∈ iSup K) (↑x : A) hx) :
      B)
    ((f i : (a : ↥(K i)) → B) x : B)
⊢ Eq.{w + 1} (α := B)
    ((iSupLift K dir f hf (iSup K) ⋯ : (a : ↥(iSup K)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ iSup K) (↑x : A) hx) :
      B)
    ((f i : (a : ↥(K i)) → B) x : B)

Tactic:
dsimp [iSupLift]

Premises used: NonUnitalSubalgebra.iSupLift
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(K i)
hx : (↑x : A) ∈ iSup K
⊢ Eq.{w + 1} (α := B)
    (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (Subtype.mk (p := fun (x : A) ↦ x ∈ iSup K) (↑x : A) hx) :
      B)
    ((f i : (a : ↥(K i)) → B) x : B)

Tactic:
apply Set.iUnionLift_mk

Premises used: Set.iUnionLift_mk
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
x : ↥T
hx : (↑x : A) ∈ K i
subst :
  ∀ (x : ↥(iSup K)) (hx : (↑x : A) ∈ K i),
    Eq.{w + 1} (α := B) ((iSupLift K dir f hf (iSup K) ⋯ : (a : ↥(iSup K)) → B) x : B)
      ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)
⊢ Eq.{w + 1} (α := B) ((iSupLift K dir f hf T hT : (a : ↥T) → B) x : B)
    ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)

Tactic:
subst hT
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(iSup K)
hx : (↑x : A) ∈ K i
dsimp :
  Eq.{w + 1} (α := B)
    (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ x :
      B)
    ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)
⊢ Eq.{w + 1} (α := B) ((iSupLift K dir f hf (iSup K) ⋯ : (a : ↥(iSup K)) → B) x : B)
    ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)

Tactic:
dsimp [iSupLift]

Premises used: NonUnitalSubalgebra.iSupLift
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(iSup K)
hx : (↑x : A) ∈ K i
⊢ Eq.{w + 1} (α := B)
    (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ x :
      B)
    ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)

Tactic:
apply Set.iUnionLift_of_mem

Premises used: Set.iUnionLift_of_mem
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b : A
rw : r • a * b = b * r • a
rw₁ : r • a * b = r • (b * a)
rw₂ : r • (a * b) = r • (b * a)
rw₃ rw₄ : r • (b * a) = r • (b * a)
⊢ Commute (r • a) b

Tactic:
rw [commute_iff_eq, mul_smul_comm, smul_mul_assoc, ha.comm]

Premises used: commute_iff_eq, IsMulCentral.comm, smul_mul_assoc, mul_smul_comm
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
rw : r • (a * (b * c)) = r • a * b * c
rw₁ : r • (a * (b * c)) = r • (a * b) * c
rw₂ : r • (a * (b * c)) = r • (a * b * c)
rw₃ rw₄ : r • (a * b * c) = r • (a * b * c)
⊢ r • a * (b * c) = r • a * b * c

Tactic:
rw [smul_mul_assoc, smul_mul_assoc, smul_mul_assoc, ha.left_assoc]

Premises used: smul_mul_assoc, IsMulCentral.left_assoc
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
rw : r • (b * c * a) = b * (c * r • a)
rw₁ : r • (b * c * a) = b * r • (c * a)
rw₂ : r • (b * c * a) = r • (b * (c * a))
rw₃ rw₄ : r • (b * (c * a)) = r • (b * (c * a))
⊢ b * c * r • a = b * (c * r • a)

Tactic:
rw [mul_smul_comm, mul_smul_comm, mul_smul_comm, ha.right_assoc]

Premises used: mul_smul_comm, IsMulCentral.right_assoc
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ (↑(center R A) : Set A) = Set.center A

Tactic:
rfl

Premises used: setOf, Set.center, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq (α := NonUnitalSubsemiring A) (toNonUnitalSubsemiring (center R A)) (NonUnitalSubsemiring.center A)

Tactic:
rfl

Premises used: NonUnitalSubsemiring.center, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalNonAssocRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq (α := NonUnitalSubring A) (toNonUnitalSubring (center R A)) (NonUnitalSubring.center A)

Tactic:
rfl

Premises used: NonUnitalSubsemiring.center, NonUnitalSubring.center, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq (α := NonUnitalSemiring ↥(center R A)) NonUnitalCommSemiring.toNonUnitalSemiring
    (NonUnitalSubsemiringClass.toNonUnitalSemiring (center R A))

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq (α := NonUnitalSemiring ↥(center R A)) NonUnitalCommSemiring.toNonUnitalSemiring
    (NonUnitalSubsemiringClass.toNonUnitalSemiring (center R A))

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : NonUnitalCommSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq (α := NonUnitalSubalgebra R A) (center R A) ⊤

Tactic:
SetLike.coe_injective (Set.center_eq_univ A)

Premises used: Set.center_eq_univ, SetLike.coe_injective
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a : A
⊢ Membership.mem (γ := NonUnitalSubalgebra 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.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
r : R
a : A
ha : a ∈ s.centralizer
x : A
hx : x ∈ s
rw : r • (x * a) = r • a * x
rw₁ : r • (x * a) = r • (a * x)
rw₂ rw₃ : r • (a * x) = r • (a * x)
⊢ x * r • a = r • a * x

Tactic:
rw [mul_smul_comm, smul_mul_assoc, ha x hx]

Premises used: smul_mul_assoc, mul_smul_comm
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
⊢ (↑(centralizer R s) : Set A) = s.centralizer

Tactic:
rfl

Premises used: setOf, Set.centralizer, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
z : A
⊢ Membership.mem (γ := NonUnitalSubalgebra 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.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s t : Set A
h : s ⊆ t
⊢ LE.le (α := NonUnitalSubalgebra 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.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq (α := NonUnitalSubalgebra 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.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
⊢ LE.le (α := NonUnitalSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))

Tactic:
adjoin_le Set.subset_centralizer_centralizer

Premises used: NonUnitalAlgebra.adjoin_le, Set.subset_centralizer_centralizer
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b : A
s : Set A
hb : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) b
h : ∀ b ∈ s, Commute a b
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) (centralizer R s) a

Tactic:
simpa only [Commute.symm_iff (a := a)] using h

Premises used: Commute.symm_iff
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b : A
s : Set A
hb : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) b
h : ∀ b ∈ s, Commute a b
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) (centralizer R s) a

Tactic:
have : a ∈ centralizer R s := by simpa only [Commute.symm_iff (a := a)] using h
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b : A
s : Set A
hb : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) b
h : ∀ b ∈ s, Commute a b
this : Membership.mem (γ := NonUnitalSubalgebra R A) (centralizer R s) a
⊢ Commute a b

Tactic:
adjoin_le_centralizer_centralizer R s hb a this

Premises used: NonUnitalAlgebra.adjoin_le_centralizer_centralizer, SemiconjBy, Commute
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b : A
s : Set A
hb : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) b
h : ∀ b ∈ s, Commute a b
this : Membership.mem (γ := NonUnitalSubalgebra R A) (centralizer R s) a
⊢ Commute a b

Tactic:
exact adjoin_le_centralizer_centralizer R s hb a this

Premises used: NonUnitalAlgebra.adjoin_le_centralizer_centralizer
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b c : A
hc : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R {b}) c
h : Commute a b
⊢ ∀ (b_1 : A), Membership.mem (γ := Set A) {b} b_1 → Commute a b_1

Tactic:
simpa
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b : A
hb : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R {a}) b
⊢ Commute a b

Tactic:
commute_of_mem_adjoin_singleton_of_commute hb rfl

Premises used: NonUnitalAlgebra.commute_of_mem_adjoin_singleton_of_commute, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
⊢ IsMulCommutative.{u_2} ↥(adjoin R s)

Tactic:
have := adjoin_le_centralizer_centralizer R s
  .of_setLike_mul_comm fun _ h₁ _ h₂ ↦
    Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂)

Premises used: NonUnitalAlgebra.adjoin_le_centralizer_centralizer, IsMulCommutative.of_setLike_mul_comm, Set.centralizer_centralizer_comm_of_comm
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x : A
⊢ ∀ (x_1 : A), Membership.mem (γ := Set A) {x} x_1 → ∀ (y : A), Membership.mem (γ := Set A) {x} y → x_1 * y = y * x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : Type u_3
inst_5 : SetLike S A
inst_6 : MulMemClass S A
s : S
inst_7 : IsMulCommutative.{u_2} ↥s
⊢ IsMulCommutative.{u_2} ↥(adjoin R (↑s : Set A))

Tactic:
isMulCommutative_adjoin R fun _ h₁ _ h₂ => setLike_mul_comm h₁ h₂

Premises used: setLike_mul_comm, NonUnitalAlgebra.isMulCommutative_adjoin
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x : R
S : NonUnitalSubsemiring R
⊢ x ∈ nonUnitalSubalgebraOfNonUnitalSubsemiring S ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x : R
S : NonUnitalSubring R
⊢ x ∈ nonUnitalSubalgebraOfNonUnitalSubring S ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ Membership.mem.{v, v} (α := A) (γ := SubMulAction R A) 1 ((algebraMap R A : (a : R) → A) r : A)

Tactic:
⟨r, (algebraMap_eq_smul_one r).symm⟩

Premises used: Set.Mem, setOf, Algebra.algebraMap_eq_smul_one, Exists.intro, Set.range, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
r : R
rw rw₁ : (fun (r : R) ↦ HSMul.hSMul (β := A) r 1) r = x ↔ HSMul.hSMul (β := A) r 1 = x
⊢ (fun (r : R) ↦ HSMul.hSMul (β := A) r 1) r = x ↔ (algebraMap R A : (a : R) → A) r = x

Tactic:
rw [algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
⊢ Eq (α := Submodule R A) 1 (R ∙ 1)

Tactic:
(LinearMap.span_singleton_eq_range _ _ _).symm

Premises used: Eq.symm, LinearMap.span_singleton_eq_range
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
n : ℕ
rw : HSMul.hSMul (β := A) n 1 = (↑n : A)
rw₁ rw₂ : Eq.{v + 1} (α := A) (↑n : A) (↑n : A)
⊢ HSMul.hSMul.{u, v, v} (α := R) (β := A) (↑n : R) 1 = (↑n : A)

Tactic:
rw [Nat.cast_smul_eq_nsmul, nsmul_one]

Premises used: Nat.cast_smul_eq_nsmul, nsmul_one
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
n : ℕ
⊢ Membership.mem (α := A) (γ := AddSubmonoid A) (toAddSubmonoid.{u, v} (R := R) 1)
    ((Nat.castAddMonoidHom A : (a : ℕ) → A) n : A)

Tactic:
exact ⟨n, show (n : R) • (1 : A) = n by rw [Nat.cast_smul_eq_nsmul, nsmul_one]⟩
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
x : A
rw : Membership.mem (γ := SubMulAction R A) (toSubMulAction (R ∙ 1)) x ↔ ∃ (r : R), HSMul.hSMul (β := A) r 1 = x
⊢ Membership.mem (γ := SubMulAction R A) (toSubMulAction 1) x ↔ Membership.mem (γ := SubMulAction R A) 1 x

Tactic:
rw [one_eq_span, SubMulAction.mem_one]

Premises used: SubMulAction.mem_one, Submodule.one_eq_span
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
x : A
⊢ Membership.mem (γ := SubMulAction R A) (toSubMulAction (R ∙ 1)) x ↔ ∃ (r : R), HSMul.hSMul (β := A) r 1 = x

Tactic:
mem_span_singleton

Premises used: iInf, Set.Mem, Set.iInter, Submodule.mem_span_singleton
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
x : A
⊢ Membership.mem (γ := SubMulAction R A) (toSubMulAction (R ∙ 1)) x ↔ ∃ (r : R), HSMul.hSMul (β := A) r 1 = x

Tactic:
exact mem_span_singleton

Premises used: Submodule.mem_span_singleton
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
⊢ Eq.{v + 1} (α := Submodule R A) 1 (span R 1)

Tactic:
one_eq_span

Premises used: Submodule.one_eq_span
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
P : Submodule R A
⊢ 1 ≤ P ↔ 1 ∈ P

Tactic:
simp [one_eq_span]

Premises used: Submodule.one_eq_span
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
A' : Submodule R A
M' : Submodule R M
r : R
m_1 : M
hm_1 : m_1 ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
a : A
ha : a ∈ A'.toAddSubmonoid
m : M
hm : m ∈ M'.toAddSubmonoid
rw : (r • a) • m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
⊢ r • a • m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier

Tactic:
rw [← smul_assoc]

Premises used: smul_assoc
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
A' : Submodule R A
M' : Submodule R M
r : R
m_1 : M
hm_1 : m_1 ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
a : A
ha : a ∈ A'.toAddSubmonoid
m : M
hm : m ∈ M'.toAddSubmonoid
⊢ (r • a) • m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier

Tactic:
AddSubmonoid.smul_mem_smul (A'.smul_mem r ha) hm

Premises used: AddSubmonoid.smul_mem_smul, Set.Mem, Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
A' : Submodule R A
M' : Submodule R M
r : R
m_1 : M
hm_1 : m_1 ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
a : A
ha : a ∈ A'.toAddSubmonoid
m : M
hm : m ∈ M'.toAddSubmonoid
⊢ (r • a) • m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier

Tactic:
exact AddSubmonoid.smul_mem_smul (A'.smul_mem r ha) hm

Premises used: AddSubmonoid.smul_mem_smul, Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
A' : Submodule R A
M' : Submodule R M
r : R
m : M
hm : m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
m₁ m₂ : M
h₁ : r • m₁ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
h₂ : r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
rw : r • m₁ + r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
⊢ r • (m₁ + m₂) ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier

Tactic:
rw [smul_add]

Premises used: smul_add
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
A' : Submodule R A
M' : Submodule R M
r : R
m : M
hm : m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
m₁ m₂ : M
h₁ : r • m₁ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
h₂ : r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
⊢ r • m₁ + r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier

Tactic:
(A'.1 • M'.1).add_mem h₁ h₂

Premises used: AddSubmonoid.add_mem, Submodule.toAddSubmonoid, Set.Mem, HSMul.hSMul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
A' : Submodule R A
M' : Submodule R M
r : R
m : M
hm : m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
m₁ m₂ : M
h₁ : r • m₁ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
h₂ : r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
⊢ r • m₁ + r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier

Tactic:
exact (A'.1 • M'.1).add_mem h₁ h₂

Premises used: AddSubmonoid.add_mem, Submodule.toAddSubmonoid, HSMul.hSMul