awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : ℤ
⊢ Eq.{u_3 + 1} (α := A) (comp.{1, u_2 + 1, u_3 + 1} (β := R) (⇑(algebraMap R A) : (a : R) → A) Int.cast x) (↑x : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : FaithfulSMul R A
n : ℕ
inst_5 : NeZero.{u_1} (R := R) (↑n : R)
⊢ NeZero.{u_2} (R := A) (↑n : A)

Tactic:
NeZero.nat_of_injective (f := ringHomEquivModuleIsScalarTower.symm ⟨_, ‹_›⟩) <|
    (faithfulSMul_iff_injective_smul_one R A).mp ‹_›

Premises used: NeZero.nat_of_injective, Iff.mp, faithfulSMul_iff_injective_smul_one
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
rw :
  (Injective.{u_1 + 1, u_2 + 1} (β := A) fun (r : R) ↦ HSMul.hSMul (β := A) r 1) ↔
    Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
rw₁ rw₂ :
  (Injective.{u_1 + 1, u_2 + 1} (β := A) fun (r : R) ↦ HSMul.hSMul (β := A) r 1) ↔
    Injective.{u_1 + 1, u_2 + 1} (β := A) fun (r : R) ↦ HSMul.hSMul (β := A) r 1
⊢ FaithfulSMul R A ↔ Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)

Tactic:
rw [faithfulSMul_iff_injective_smul_one, Algebra.algebraMap_eq_smul_one']

Premises used: Algebra.algebraMap_eq_smul_one', faithfulSMul_iff_injective_smul_one
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
⊢ Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)

Tactic:
(faithfulSMul_iff_algebraMap_injective R A).mp inferInstance

Premises used: faithfulSMul_iff_algebraMap_injective, inferInstance, Iff.mp
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
r : R
⊢ Eq.{u_2 + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) (0 : A) ↔ r = 0

Tactic:
map_eq_zero_iff (algebraMap R A) <| algebraMap_injective R A

Premises used: Algebra.algebraMap, map_eq_zero_iff, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
r : R
⊢ Eq.{u_2 + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) (1 : A) ↔ r = 1

Tactic:
map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R A

Premises used: map_eq_one_iff, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
a b : R
⊢ Eq.{u_2 + 1} (α := A) (↑a : A) (↑b : A) ↔ a = b

Tactic:
(FaithfulSMul.algebraMap_injective _ _).eq_iff

Premises used: Function.Injective.eq_iff, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
a : R
⊢ Eq.{u_2 + 1} (α := A) (↑a : A) 0 ↔ a = 0

Tactic:
FaithfulSMul.algebraMap_eq_zero_iff _ _

Premises used: FaithfulSMul.algebraMap_eq_zero_iff
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : CharZero R
⊢ CharZero A

Tactic:
have := algebraMap_comp_natCast R A
  ⟨this ▸ (FaithfulSMul.algebraMap_injective R A).comp CharZero.cast_injective⟩

Premises used: Eq.rec, CharZero.cast_injective, Function.Injective.comp, FaithfulSMul.algebraMap_injective, CharZero.mk, algebraMap_comp_natCast
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : CharZero R
⊢ FaithfulSMul ℕ R

Tactic:
simpa only [faithfulSMul_iff_algebraMap_injective] using (algebraMap ℕ R).injective_nat

Premises used: faithfulSMul_iff_algebraMap_injective, Algebra.algebraMap, RingHom.injective_nat, Nat
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R_1 : Type u_1
A : Type u_2
inst : CommSemiring R_1
inst_1 : Semiring A
inst_2 : Algebra R_1 A
inst_3 : FaithfulSMul R_1 A
R : Type u_3
inst_4 : Ring R
inst_5 : CharZero R
⊢ FaithfulSMul ℤ R

Tactic:
simpa only [faithfulSMul_iff_algebraMap_injective] using (algebraMap ℤ R).injective_int

Premises used: faithfulSMul_iff_algebraMap_injective, Algebra.algebraMap, Int, RingHom.injective_int
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
m : M
rw :
  r • HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
rw₁ :
  HSMul.hSMul (β := A) r 1 • m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
rw₂ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) (1 : A) • m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
rw₃ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := A) 1 m)
rw₄ rw₅ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m
⊢ r • m = HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m

Tactic:
rw [← one_smul A m, ← smul_assoc, Algebra.smul_def, mul_one, one_smul]

Premises used: smul_assoc, one_smul, Algebra.smul_def, mul_one
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
m : M
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m = r • m

Tactic:
(algebra_compatible_smul A r m).symm

Premises used: algebra_compatible_smul, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
⊢ IsSMulRegular.{u_2, u_3} (R := A) M ((algebraMap R A : (a : R) → A) r : A) ↔ IsSMulRegular M r

Tactic:
(Equiv.refl M).isSMulRegular_congr (algebraMap_smul A r)

Premises used: Equiv.isSMulRegular_congr, algebraMap_smul
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
a : A
m : M
rw : HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) (a • m) = a • r • m
rw₁ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a • m = a • r • m
rw₂ : HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A) • m = a • r • m
rw₃ : a • HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) r : A) m = a • r • m
rw₄ rw₅ : a • r • m = a • r • m
⊢ r • a • m = a • r • m

Tactic:
rw [algebra_compatible_smul A r (a • m), smul_smul, Algebra.commutes, mul_smul, ←
      algebra_compatible_smul]

Premises used: algebra_compatible_smul, smul_smul, HSMul.hSMul, SemigroupAction.mul_smul, Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
⊢ SMulCommClass A R M

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
A_1 : Type u_2
inst_1 : Semiring A_1
inst_2 : Algebra R_1 A_1
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A_1 M
inst_5 : Module R_1 M
inst_6 : IsScalarTower R_1 A_1 M
R : Type u_4
A : Type u_5
inst_7 : CommSemiring R
inst_8 : Semiring A
inst_9 : Algebra R A
⊢ SMulCommClass R A A

Tactic:
IsScalarTower.to_smulCommClass

Premises used: IsScalarTower.to_smulCommClass
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
A_1 : Type u_2
inst_1 : Semiring A_1
inst_2 : Algebra R_1 A_1
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A_1 M
inst_5 : Module R_1 M
inst_6 : IsScalarTower R_1 A_1 M
R : Type u_4
S : Type u_5
A : Type u_6
inst_7 : CommSemiring R
inst_8 : CommSemiring S
inst_9 : Semiring A
inst_10 : Algebra R A
inst_11 : Algebra S A
r : R
s : S
a : A
rw : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (s • a) = s • r • a
rw₁ : s • HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a = s • r • a
rw₂ rw₃ : s • r • a = s • r • a
⊢ r • s • a = s • r • a

Tactic:
rw [Algebra.smul_def, mul_smul_comm, ← Algebra.smul_def]

Premises used: mul_smul_comm, Algebra.smul_def
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
a : A
m : M
⊢ a • r • m = r • a • m

Tactic:
smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : NoZeroDivisors A
⊢ Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) 0 : A) (0 : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : NoZeroDivisors A
⊢ ∀ (x y : R),
    (algebraMap R A : (a : R) → A) (x * y) =
      HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A) ((algebraMap R A : (a : R) → A) y : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsCancelMulZero A
⊢ Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) 0 : A) (0 : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsCancelMulZero A
⊢ ∀ (x y : R),
    (algebraMap R A : (a : R) → A) (x * y) =
      HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A) ((algebraMap R A : (a : R) → A) y : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
⊢ IsDomain R

Tactic:
(FaithfulSMul.algebraMap_injective R A).isDomain

Premises used: Function.Injective.isDomain, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : Semiring S
inst_5 : Module S R
inst_6 : Module S A
inst_7 : IsScalarTower S R A
inst_8 : IsTorsionFree S A
⊢ ∀ (r : S) (m : R),
    (algebraMap R A : (a : R) → A) (r • m) = HSMul.hSMul (β := A) r ((algebraMap R A : (a : R) → A) m : A)

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : Nontrivial R
inst_5 : IsCancelMulZero A
inst_6 : AddCommMonoid M
inst_7 : Module A M
inst_8 : Module R M
inst_9 : IsTorsionFree A M
inst_10 : IsScalarTower R A M
r : R
hr : IsRegular r
⊢ Ne.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) (0 : A)

Tactic:
simpa using hr.ne_zero

Premises used: IsRegular.ne_zero
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : Nontrivial R
inst_5 : IsCancelMulZero A
inst_6 : AddCommMonoid M
inst_7 : Module A M
inst_8 : Module R M
inst_9 : IsTorsionFree A M
inst_10 : IsScalarTower R A M
⊢ ∀ (r : R) (m : M), HSMul.hSMul.{u_3, u_4, u_4} (α := A) ((algebraMap R A : (a : R) → A) r : A) m = r • m

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : Nontrivial R
inst_5 : IsCancelMulZero A
⊢ IsTorsionFree R A

Tactic:
.trans_faithfulSMul R A A

Premises used: Module.IsTorsionFree.trans_faithfulSMul
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
inst_4 : IsDomain A
⊢ IsTorsionFree R A ↔ FaithfulSMul R A

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
inst_4 : IsDomain A
rw : FaithfulSMul R A ↔ Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
rw₁ rw₂ :
  Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) ↔
    Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ IsTorsionFree R A ↔ Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)

Tactic:
rw [isTorsionFree_iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective]

Premises used: faithfulSMul_iff_algebraMap_injective, Module.isTorsionFree_iff_faithfulSMul
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
hf : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
r : R
h : Invertible (α := A) ((algebraMap R A : (a : R) → A) r : A)
rw :
  HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B)
      ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B) =
    1
rw₁ :
  HSMul.hSMul (β := B) r
      ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B) =
    1
rw₂ :
  Eq.{u_3 + 1} (α := B)
    ((f : (a : A) → B)
        (HSMul.hSMul (β := A) r
          (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A)) :
      B)
    (1 : B)
rw₃ :
  Eq.{u_3 + 1} (α := B)
    ((f : (a : A) → B)
        (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A)
          (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A)) :
      B)
    (1 : B)
rw₄ : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
rw₅ rw₆ : Eq.{u_3 + 1} (α := B) 1 1
⊢ HMul.hMul (α := B) (β := B)
      ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B)
      ((algebraMap R B : (a : R) → B) r : B) =
    1

Tactic:
rw [← Algebra.commutes, ← Algebra.smul_def, ← map_smul, Algebra.smul_def,
    mul_invOf_self, hf]

Premises used: Invertible.mul_invOf_self, Algebra.smul_def, Algebra.commutes, map_smul
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
hf : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
r : R
h : Invertible (α := A) ((algebraMap R A : (a : R) → A) r : A)
rw :
  HSMul.hSMul (β := B) r
      ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B) =
    1
rw₁ :
  Eq.{u_3 + 1} (α := B)
    ((f : (a : A) → B)
        (HSMul.hSMul (β := A) r
          (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A)) :
      B)
    (1 : B)
rw₂ :
  Eq.{u_3 + 1} (α := B)
    ((f : (a : A) → B)
        (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A)
          (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A)) :
      B)
    (1 : B)
rw₃ : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
rw₄ rw₅ : Eq.{u_3 + 1} (α := B) 1 1
⊢ HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) r : B)
      ((f : (a : A) → B) (@invOf _ Distrib.toMul AddMonoidWithOne.toOne ((algebraMap R A : (a : R) → A) r) _ : A) : B) =
    1

Tactic:
rw [← Algebra.smul_def, ← map_smul, Algebra.smul_def, mul_invOf_self, hf]

Premises used: Invertible.mul_invOf_self, Algebra.smul_def, map_smul
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₗ[R] B
hf : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
r : R
h : IsUnit.{u_2} (M := A) ((algebraMap R A : (a : R) → A) r : A)
⊢ IsUnit.{u_3} (M := B) ((algebraMap R B : (a : R) → B) r : B)

Tactic:
let ⟨i⟩ := nonempty_invertible h
  letI := Invertible.algebraMapOfInvertibleAlgebraMap f hf i
  isUnit_of_invertible _

Premises used: Algebra.algebraMap, isUnit_of_invertible, _private.0.IsUnit.algebraMap_of_algebraMap.match_1, IsUnit, IsUnit.nonempty_invertible, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Injective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y : F
e : Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) x : E) ((algebraMap F E : (a : F) → E) y : E)
rw : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) y : E)
rw₁ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (x * 1) : E) ((b : (a : F) → E) (y * 1) : E)
rw₂ : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E) ((b : (a : F) → E) (y * 1) : E)
rw₃ :
  Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) x 1) : E)
    ((b : (a : F) → E) (HSMul.hSMul (β := F) y 1) : E)
rw₄ : HSMul.hSMul (β := E) x ((b : (a : F) → E) 1 : E) = (b : (a : F) → E) (HSMul.hSMul (β := F) y 1)
rw₅ : HSMul.hSMul (β := E) x ((b : (a : F) → E) 1 : E) = HSMul.hSMul (β := E) y ((b : (a : F) → E) 1 : E)
rw₆ :
  HMul.hMul (α := E) (β := E) ((algebraMap F E : (a : F) → E) x : E) ((b : (a : F) → E) 1 : E) =
    HSMul.hSMul (β := E) y ((b : (a : F) → E) 1 : E)
rw₇ :
  HMul.hMul (α := E) (β := E) ((algebraMap F E : (a : F) → E) x : E) ((b : (a : F) → E) 1 : E) =
    HMul.hMul (α := E) (β := E) ((algebraMap F E : (a : F) → E) y : E) ((b : (a : F) → E) 1 : E)
rw₈ rw₉ :
  HMul.hMul (α := E) (β := E) ((algebraMap F E : (a : F) → E) y : E) ((b : (a : F) → E) 1 : E) =
    HMul.hMul (α := E) (β := E) ((algebraMap F E : (a : F) → E) y : E) ((b : (a : F) → E) 1 : E)
⊢ Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) x : E) ((b : (a : F) → E) y : E)

Tactic:
rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
    map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]

Premises used: Algebra.smul_def, smul_eq_mul, mul_one, map_smul
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x : E
obtain : ∀ (x : F), ∃ (a : F), Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) a : E) ((b : (a : F) → E) x : E)
⊢ ∃ (a : F), (algebraMap F E : (a : F) → E) a = x

Tactic:
obtain ⟨x, rfl⟩ := hb x

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x : F
obtain :
  ∀ (y : F)
    (hy : (b : (a : F) → E) y = HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    ∃ (a : F), Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) a : E) ((b : (a : F) → E) x : E)
⊢ ∃ (a : F), Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) a : E) ((b : (a : F) → E) x : E)

Tactic:
obtain ⟨y, hy⟩ := hb (b 1 * b 1)

Premises used: HMul.hMul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y : F
hy : (b : (a : F) → E) y = HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)
⊢ ∃ (a : F), Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) a : E) ((b : (a : F) → E) x : E)

Tactic:
⟨x * y, ?_⟩

Premises used: HMul.hMul, Exists.intro
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y : F
hy : (b : (a : F) → E) y = HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)
refine : Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
⊢ ∃ (a : F), Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) a : E) ((b : (a : F) → E) x : E)

Tactic:
refine ⟨x * y, ?_⟩
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y : F
hy : (b : (a : F) → E) y = HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)
obtain :
  ∀ (z : F) (hz : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) z : E) (1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
⊢ Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)

Tactic:
obtain ⟨z, hz⟩ := hb 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y : F
hy : (b : (a : F) → E) y = HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)
z : F
hz : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) z : E) (1 : E)
⊢ x • HSMul.hSMul (β := E) z ((b : (a : F) → E) y : E) =
    x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)

Tactic:
apply_fun (x • z • ·) at hy

Premises used: HSMul.hSMul
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Bijective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
⊢ Bijective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)

Tactic:
⟨injective_algebraMap_of_linearMap b hb.1, surjective_algebraMap_of_linearMap b hb.2⟩

Premises used: surjective_algebraMap_of_linearMap, And.right, And.left, And.intro, injective_algebraMap_of_linearMap, Function.Bijective
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F ≃ₗ[F] E
⊢ Bijective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)

Tactic:
bijective_algebraMap_of_linearMap _ b.bijective

Premises used: LinearEquiv.bijective, bijective_algebraMap_of_linearMap