awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x y : A₁ ≃ₐ[R] A₁
z : A₁ˣ
huv : (↑((x * y) • z) : A₁) = (↑(x • y • z) : A₁)
⊢ (x * y) • z = x • y • z

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x y : A₁ ≃ₐ[R] A₁
z : A₁ˣ
⊢ (↑((x * y) • z) : A₁) = (↑(x • y • z) : A₁)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ˣ
huv : (↑(HSMul.hSMul (α := A₁ ≃ₐ[R] A₁) 1 x) : A₁) = (↑x : A₁)
⊢ HSMul.hSMul (α := A₁ ≃ₐ[R] A₁) 1 x = x

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ˣ
⊢ (↑(HSMul.hSMul (α := A₁ ≃ₐ[R] A₁) 1 x) : A₁) = (↑x : A₁)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ ≃ₐ[R] A₁
huv : (↑(HSMul.hSMul (β := A₁ˣ) x 1) : A₁) = (↑1 : A₁)
⊢ HSMul.hSMul (β := A₁ˣ) x 1 = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ ≃ₐ[R] A₁
⊢ (↑(HSMul.hSMul (β := A₁ˣ) x 1) : A₁) = (↑1 : A₁)

Tactic:
map_one x

Premises used: map_one
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ ≃ₐ[R] A₁
⊢ (↑(HSMul.hSMul (β := A₁ˣ) x 1) : A₁) = (↑1 : A₁)

Tactic:
exact map_one x

Premises used: map_one
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ ≃ₐ[R] A₁
y z : A₁ˣ
huv : (↑(x • (y * z)) : A₁) = (↑(x • y * x • z) : A₁)
⊢ x • (y * z) = x • y * x • z

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ ≃ₐ[R] A₁
y z : A₁ˣ
⊢ (↑(x • (y * z)) : A₁) = (↑(x • y * x • z) : A₁)

Tactic:
map_mul x _ _

Premises used: map_mul
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ ≃ₐ[R] A₁
y z : A₁ˣ
⊢ (↑(x • (y * z)) : A₁) = (↑(x • y * x • z) : A₁)

Tactic:
exact map_mul x _ _

Premises used: map_mul
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
f : A₁ ≃ₐ[R] A₁
x : A₁ˣ
⊢ f • x = (Units.map (↑f : A₁ →* A₁) : (a : A₁ˣ) → A₁ˣ) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
σ : A₁ ≃ₐ[R] A₁
⊢ MulSemiringAction.toRingEquiv (A₁ ≃ₐ[R] A₁) A₁ σ = σ.toRingEquiv

Tactic:
rfl

Premises used: MulSemiringAction.toRingEquiv, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
y : R
x : A₁
h : Eq.{uA₂ + 1} (α := A₂) ((algebraMap R A₂ : (a : R) → A₂) y : A₂) ((e : (a : A₁) → A₂) x : A₂)
⊢ (algebraMap R A₁ : (a : R) → A₁) y = x

Tactic:
simpa using e.symm.toAlgHom.algebraMap_eq_apply h

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, AlgHom.algebraMap_eq_apply
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
σ : A₁ ≃ₐ[R] A₁
n : ℕ
⊢ (σ ^ n).toLinearMap = σ.toLinearMap ^ n

Tactic:
(AlgEquiv.toLinearMapHom R A₁).map_pow σ n

Premises used: AlgHom.toLinearMap, AlgEquiv.toLinearMapHom, MonoidHom.map_pow
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
⊢ Eq.{uA₁ + 1} (α := A₁ →ₗ[R] A₁) (toLinearMap 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R_1 : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R_1
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R_1 A₁
inst_8 : Algebra R_1 A₂
inst_9 : Algebra R_1 A₃
inst_10 : Algebra R_1 A₁'
inst_11 : Algebra R_1 A₂'
inst_12 : Algebra R_1 A₃'
e : A₁ ≃ₐ[R_1] A₂
R : Type u_1
S : Type u_2
inst_13 : CommSemiring R
inst_14 : Semiring S
inst_15 : Algebra R S
f : (S →ₐ[R] S)ˣ
x : S
rw : ((↑1 : S →ₐ[R] S) : (a : S) → S) x = x
⊢ ((↑(f⁻¹ * f) : S →ₐ[R] S) : (a : S) → S) x = x

Tactic:
rw [inv_mul_cancel]

Premises used: inv_mul_cancel
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R_1 : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R_1
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R_1 A₁
inst_8 : Algebra R_1 A₂
inst_9 : Algebra R_1 A₃
inst_10 : Algebra R_1 A₁'
inst_11 : Algebra R_1 A₂'
inst_12 : Algebra R_1 A₃'
e : A₁ ≃ₐ[R_1] A₂
R : Type u_1
S : Type u_2
inst_13 : CommSemiring R
inst_14 : Semiring S
inst_15 : Algebra R S
f : (S →ₐ[R] S)ˣ
x : S
⊢ ((↑1 : S →ₐ[R] S) : (a : S) → S) x = x

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R_1 : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R_1
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R_1 A₁
inst_8 : Algebra R_1 A₂
inst_9 : Algebra R_1 A₃
inst_10 : Algebra R_1 A₁'
inst_11 : Algebra R_1 A₂'
inst_12 : Algebra R_1 A₃'
e : A₁ ≃ₐ[R_1] A₂
R : Type u_1
S : Type u_2
inst_13 : CommSemiring R
inst_14 : Semiring S
inst_15 : Algebra R S
f : (S →ₐ[R] S)ˣ
x : S
rw : ((↑1 : S →ₐ[R] S) : (a : S) → S) x = x
⊢ ((↑(f * f⁻¹) : S →ₐ[R] S) : (a : S) → S) x = x

Tactic:
rw [mul_inv_cancel]

Premises used: mul_inv_cancel
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
inst_13 : Finite (A₁ →ₐ[R] A₂)
⊢ Finite (A₁ ≃ₐ[R] A₂)

Tactic:
Finite.of_injective _ AlgEquiv.coe_algHom_injective

Premises used: AlgEquiv.coe_algHom_injective, Finite.of_injective
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
G : Type u_2
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Group G
inst_4 : MulSemiringAction G A
inst_5 : SMulCommClass G R A
inst_6 : FaithfulSMul G A
⊢ Function.Injective.{u_2 + 1, u_4 + 1} (α := G) (β := A ≃ₐ[R] A) (toAlgEquiv R A)

Tactic:
fun _ _ h =>
  eq_of_smul_eq_smul fun r => AlgEquiv.ext_iff.1 h r

Premises used: FaithfulSMul.eq_of_smul_eq_smul, AlgEquiv.ext_iff, Iff.mp, Function.Injective
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Subsingleton S
inst_6 : Subsingleton T
x : S
⊢ Eq.{u_3 + 1} (α := T) ((default : (a : S) → T) x : T) (0 : T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
⊢ down.{u_3, u_2} ((AlgEquiv.symm algEquiv.{u_1, u_2, u_3} : (a : A) → ULift.{u_3, u_2} A) a) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra R T
f : S →ₐ[R] T
x : ULift.{u₂, u_1} R
⊢ (↑(↑(comp (↑(AlgEquiv.symm ULift.algEquiv.{u_1, u_3, u₃}) : T →ₐ[R] ULift.{u₃, u_3} T)
                    (f.comp (↑ULift.algEquiv.{u_1, u_2, u₁} : ULift.{u₁, u_2} S →ₐ[R] S))).toRingHom :
              ULift.{u₁, u_2} S →* ULift.{u₃, u_3} T) :
          OneHom (ULift.{u₁, u_2} S) (ULift.{u₃, u_3} T)).toFun
      ((algebraMap (ULift.{u₂, u_1} R) (ULift.{u₁, u_2} S) : (a : ULift.{u₂, u_1} R) → ULift.{u₁, u_2} S) x) =
    (algebraMap (ULift.{u₂, u_1} R) (ULift.{u₃, u_3} T) : (a : ULift.{u₂, u_1} R) → ULift.{u₃, u_3} T) x

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra R T
f : S →ₐ[R] T
x : ULift.{u_4, u_2} S
⊢ Eq.{u_3 + 1} (α := T)
    (ULift.down.{u_5, u_3}
        ((ulift.{u_4, u_6, u_5, u_1, u_2, u_3} f : (a : ULift.{u_4, u_2} S) → ULift.{u_5, u_3} T) x) :
      T)
    ((f : (a : S) → T) x.down : T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra R T
f : S →ₐ[R] T
x : ULift.{u_4, u_2} S
⊢ Eq (α := ULift.{u_5, u_3} T)
    ((ulift.{u_4, u_6, u_5, u_1, u_2, u_3} f : (a : ULift.{u_4, u_2} S) → ULift.{u_5, u_3} T) x : ULift.{u_5, u_3} T)
    ({ down := (f : (a : S) → T) x.down } : ULift.{u_5, u_3} T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
e : R ≃ₗ[R] A
x : R
rw :
  Eq.{u_1 + 1} (α := R)
    ((e.symm : (a : A) → R)
        (HMul.hMul (α := A) (β := A) ((e : (a : R) → A) 1 : A) ((algebraMap R A : (a : R) → A) x : A)) :
      R)
    ((e.symm : (a : A) → R)
        (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A) ((e : (a : R) → A) 1 : A)) :
      R)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := R)
    ((e.symm : (a : A) → R)
        (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A) ((e : (a : R) → A) 1 : A)) :
      R)
    ((e.symm : (a : A) → R)
        (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A) ((e : (a : R) → A) 1 : A)) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((e.symm : (a : A) → R)
        (HMul.hMul (α := A) (β := A) ((e : (a : R) → A) 1 : A) ((algebraMap R A : (a : R) → A) x : A)) :
      R)
    ((e.symm : (a : A) → R) (HSMul.hSMul (β := A) x ((e : (a : R) → A) 1 : A)) : R)

Tactic:
rw [Algebra.smul_def, mul_comm]

Premises used: mul_comm, Algebra.smul_def
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
e : R ≃ₗ[R] A
x : R
rw : HSMul.hSMul (β := R) x ((e.symm : (a : A) → R) ((e : (a : R) → A) 1 : A) : R) = x
rw₁ : HSMul.hSMul (β := R) x 1 = x
rw₂ : x * 1 = x
rw₃ rw₄ : x = x
⊢ (e.symm : (a : A) → R) (HSMul.hSMul (β := A) x ((e : (a : R) → A) 1 : A)) = x

Tactic:
rw [map_smul, e.symm_apply_apply, smul_eq_mul, mul_one]

Premises used: LinearEquiv.symm_apply_apply, LinearEquiv.map_smul, smul_eq_mul, mul_one
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
e : R ≃ₗ[R] A
x : A
rw :
  (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
    HMul.hMul (α := A) (β := A)
      ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
      ((e : (a : R) → A) (HMul.hMul (α := R) (β := R) ((e.symm : (a : A) → R) 1 : R) (1 : R)) : A)
rw₁ :
  (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
    HMul.hMul (α := A) (β := A)
      ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
      ((e : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
rw₂ :
  (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
    HMul.hMul (α := A) (β := A)
      ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
      (1 : A)
rw₃ rw₄ :
  Eq.{u_2 + 1} (α := A)
    ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
    ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
⊢ (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
    HMul.hMul (α := A) (β := A)
      ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
      ((e : (a : R) → A) (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : A) → R) 1 : R) 1) : A)

Tactic:
rw [smul_eq_mul, mul_one, e.apply_symm_apply, mul_one]

Premises used: LinearEquiv.apply_symm_apply, smul_eq_mul, mul_one
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₁
inst_7 : Module S M₂
inst_8 : SMulCommClass S R M₁
inst_9 : SMulCommClass S R M₂
inst_10 : SMul R S
inst_11 : IsScalarTower R S M₁
inst_12 : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
x : R
h :
  ∀ (x_1 : M₂),
    Eq (α := M₂)
      ((e.conjRingEquiv.toFun ((algebraMap R (Module.End S M₁) : (a : R) → Module.End S M₁) x) : (a : M₂) → M₂) x_1 :
        M₂)
      ((((algebraMap R (Module.End S M₂) : (a : R) → Module.End S M₂) x : Module.End S M₂) : (a : M₂) → M₂) x_1 : M₂)
⊢ e.conjRingEquiv.toFun ((algebraMap R (Module.End S M₁) : (a : R) → Module.End S M₁) x) =
    (algebraMap R (Module.End S M₂) : (a : R) → Module.End S M₂) x

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₁
inst_7 : Module S M₂
inst_8 : SMulCommClass S R M₁
inst_9 : SMulCommClass S R M₂
inst_10 : SMul R S
inst_11 : IsScalarTower R S M₁
inst_12 : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
x : R
x_1 : M₂
h :
  Eq.{u_4 + 1} (α := M₂)
    ((restrictScalars R e : (a : M₁) → M₂)
        ((((algebraMap R (Module.End S M₁) : (a : R) → Module.End S M₁) x : Module.End S M₁) : (a : M₁) → M₁)
            (((↑e.symm : M₂ →ₗ[S] M₁) : (a : M₂) → M₁) x_1 : M₁) :
          M₁) :
      M₂)
    ((((algebraMap R (Module.End S M₂) : (a : R) → Module.End S M₂) x : Module.End S M₂) : (a : M₂) → M₂) x_1 : M₂)
⊢ Eq (α := M₂)
    ((e.conjRingEquiv.toFun ((algebraMap R (Module.End S M₁) : (a : R) → Module.End S M₁) x) : (a : M₂) → M₂) x_1 : M₂)
    ((((algebraMap R (Module.End S M₂) : (a : R) → Module.End S M₂) x : Module.End S M₂) : (a : M₂) → M₂) x_1 : M₂)

Tactic:
change e.restrictScalars R _ = _

Premises used: LinearEquiv.restrictScalars, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₁
inst_7 : Module S M₂
inst_8 : SMulCommClass S R M₁
inst_9 : SMulCommClass S R M₂
inst_10 : SMul R S
inst_11 : IsScalarTower R S M₁
inst_12 : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
x : R
x_1 : M₂
⊢ Eq.{u_4 + 1} (α := M₂)
    ((restrictScalars R e : (a : M₁) → M₂)
        ((((algebraMap R (Module.End S M₁) : (a : R) → Module.End S M₁) x : Module.End S M₁) : (a : M₁) → M₁)
            (((↑e.symm : M₂ →ₗ[S] M₁) : (a : M₂) → M₁) x_1 : M₁) :
          M₁) :
      M₂)
    ((((algebraMap R (Module.End S M₂) : (a : R) → Module.End S M₂) x : Module.End S M₂) : (a : M₂) → M₂) x_1 : M₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₁
inst_7 : Module S M₂
inst_8 : SMulCommClass S R M₁
inst_9 : SMulCommClass S R M₂
inst_10 : SMul R S
inst_11 : IsScalarTower R S M₁
inst_12 : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
f : Module.End S M₁
⊢ ((conjAlgEquiv R e : AlgEquiv.{u_1, u_3, u_4} R (Module.End S M₁) (Module.End S M₂)) :
        (a : Module.End S M₁) → Module.End S M₂)
      f =
    (↑e : M₁ →ₗ[S] M₂) ∘ₗ f ∘ₗ (↑e.symm : M₂ →ₗ[S] M₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Semiring S
inst_6 : Module S M₁
inst_7 : Module S M₂
inst_8 : SMulCommClass S R M₁
inst_9 : SMulCommClass S R M₂
inst_10 : SMul R S
inst_11 : IsScalarTower R S M₁
inst_12 : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
⊢ Eq (α := AlgEquiv.{u_1, u_4, u_3} R (Module.End S M₂) (Module.End S M₁)) (AlgEquiv.symm (conjAlgEquiv R e))
    (conjAlgEquiv R e.symm)

Tactic:
rfl

Premises used: AlgEquiv.symm, LinearEquiv.conjAlgEquiv, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Field
Goal:
R : Type u_1
A : Type u_2
inst : Semifield R
inst_1 : DivisionSemiring A
inst_2 : Algebra R A
r : R
⊢ Eq.{u_2 + 1} (α := A) (↑r⁻¹ : A) (↑r : A)⁻¹

Tactic:
map_inv₀ (algebraMap R A) r

Premises used: Algebra.algebraMap, map_inv₀
-- Module: Mathlib.Algebra.Algebra.Field
Goal:
R : Type u_1
A : Type u_2
inst : Semifield R
inst_1 : DivisionSemiring A
inst_2 : Algebra R A
r s : R
⊢ (↑(r / s) : A) = HDiv.hDiv (α := A) (↑r : A) (↑s : A)

Tactic:
map_div₀ (algebraMap R A) r s

Premises used: Algebra.algebraMap, map_div₀
-- Module: Mathlib.Algebra.Algebra.Field
Goal:
R : Type u_1
A : Type u_2
inst : Semifield R
inst_1 : DivisionSemiring A
inst_2 : Algebra R A
r : R
z : ℤ
⊢ (↑(r ^ z) : A) = HPow.hPow (α := A) (↑r : A) z

Tactic:
map_zpow₀ (algebraMap R A) r z

Premises used: Algebra.algebraMap, map_zpow₀
-- Module: Mathlib.Algebra.Algebra.Field
Goal:
R : Type u_1
A : Type u_2
inst : Field R
inst_1 : DivisionRing A
inst_2 : Algebra R A
q : ℚ
⊢ Eq.{u_2 + 1} (α := A) (↑(↑q : R) : A) (↑q : A)

Tactic:
map_ratCast (algebraMap R A) q

Premises used: map_ratCast, Algebra.algebraMap
-- Module: Mathlib.Algebra.Algebra.Hom.Rat
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
inst_2 : Algebra ℚ R
inst_3 : Algebra ℚ S
f : R →+* S
⊢ (↑f.toRatAlgHom : R →+* S) = f

Tactic:
RingHom.ext fun _x => rfl

Premises used: RingHom.ext, rfl
-- Module: Mathlib.Algebra.Algebra.Hom.Rat
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
inst_2 : Algebra ℚ R
inst_3 : Algebra ℚ S
f : R →+* S
x : R
⊢ Eq.{u_2 + 1} (α := S) ((f.toRatAlgHom : (a : R) → S) x : S) ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Hom.Rat
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
inst_2 : Algebra ℚ R
inst_3 : Algebra ℚ S
f : R →ₐ[ℚ] S
⊢ RingHom.toRatAlgHom (↑f : R →+* S) = f

Tactic:
AlgHom.ext fun _x => rfl

Premises used: AlgHom.ext, rfl
-- Module: Mathlib.Algebra.Algebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
F : Type u_4
inst : CommSemiring R
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
f : F
r : R
x : A
⊢ (f : (a : A) → B) (r • x) =
    HSMul.hSMul (α := R) (β := B) ((RingHom.id R : (a : R) → R) r : R) ((f : (a : A) → B) x : B)

Tactic:
simp only [Algebra.smul_def, map_mul, commutes, RingHom.id_apply]

Premises used: RingHom.id_apply, map_mul, AlgHomClass.commutes, Algebra.smul_def