awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
h :
  ∀ (x : R),
    Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
      ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
x : R
y : S
z : A
simp_rw :
  HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) y) : A)
      z =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A)
      (HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) y : A) z)
simp_rw₁ :
  HMul.hMul (α := A) (β := A) ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
        ((algebraMap S A : (a : S) → A) y : A) *
      z =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A)
      (HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) y : A) z)
simp_rw₂ :
  HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
      (HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) y : A) z) =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A)
      (HMul.hMul (α := A) ((algebraMap S A : (a : S) → A) y : A) z)
⊢ (x • y) • z = x • y • z

Tactic:
simp_rw [Algebra.smul_def, map_mul, mul_assoc, h]

Premises used: mul_assoc, map_mul, Algebra.smul_def
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
h :
  Eq (α := R →+* A) (algebraMap R A)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A) (algebraMap R S))
⊢ IsScalarTower R S A

Tactic:
of_algebraMap_eq <| RingHom.ext_iff.1 h

Premises used: RingHom.ext_iff, IsScalarTower.of_algebraMap_eq, Iff.mp
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
x : R
simp_rw :
  Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
    ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
simp_rw₁ : HSMul.hSMul (β := A) x 1 = HSMul.hSMul (β := A) (HSMul.hSMul (β := S) x 1) 1
simp_rw₂ : HSMul.hSMul (β := A) x 1 = x • HSMul.hSMul.{v, w, w} (α := S) (β := A) 1 1
⊢ Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A) (algebraMap R S) : (a : R) → A) x : A)

Tactic:
simp_rw [RingHom.comp_apply, Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

Premises used: one_smul, Algebra.algebraMap_eq_smul_one, RingHom.comp_apply, IsScalarTower.smul_assoc
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
x : R
rw :
  Eq.{w + 1} (α := A)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A) (algebraMap R S) : (a : R) → A) x : A)
    ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
rw₁ rw₂ :
  Eq.{w + 1} (α := A) ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
    ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
⊢ Eq.{w + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
    ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)

Tactic:
rw [algebraMap_eq R S A, RingHom.comp_apply]

Premises used: IsScalarTower.algebraMap_eq, RingHom.comp_apply
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S_1 : Type v
A_1 : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Semiring A_1
inst_3 : Semiring B
inst_4 : Algebra R S_1
inst_5 : Algebra S_1 A_1
inst_6 : Algebra S_1 B
inst_7 : Algebra R A_1
inst_8 : Algebra R B
inst_9 : IsScalarTower R S_1 A_1
inst_10 : IsScalarTower R S_1 B
S : Type u
A : Type v
inst_11 : CommSemiring S
inst_12 : Semiring A
h1 h2 : Algebra S A
r : S
x : A
have : (I : Algebra S A) → A
⊢ A

Tactic:
have I := h1
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S_1 : Type v
A_1 : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Semiring A_1
inst_3 : Semiring B
inst_4 : Algebra R S_1
inst_5 : Algebra S_1 A_1
inst_6 : Algebra S_1 B
inst_7 : Algebra R A_1
inst_8 : Algebra R B
inst_9 : IsScalarTower R S_1 A_1
inst_10 : IsScalarTower R S_1 B
S : Type u
A : Type v
inst_11 : CommSemiring S
inst_12 : Semiring A
h1 h2 : Algebra S A
r : S
x : A
I : Algebra S A
⊢ A

Tactic:
exact r • x
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
S : Type u
A : Type v
inst : CommSemiring S
inst_1 : Semiring A
h1 h2 : Algebra S A
h :
  ∀ (r : S) (x : A),
    (have I := h1;
      r • x) =
      r • x
r : S
⊢ Eq.{v + 1} (α := A) ((algebraMap S A : (a : S) → A) r : A) ((algebraMap S A : (a : S) → A) r : A)

Tactic:
simpa only [@Algebra.smul_def _ _ _ _ h1, @Algebra.smul_def _ _ _ _ h2, mul_one] using h r 1

Premises used: Algebra.smul_def, mul_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
r : R
rw :
  Eq.{u₁ + 1} (α := B)
    ((f : (a : A) → B) ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S) : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)
rw₁ :
  Eq.{u₁ + 1} (α := B) ((algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) r : S) : B)
    ((algebraMap R B : (a : R) → B) r : B)
rw₂ rw₃ : Eq.{u₁ + 1} (α := B) ((algebraMap R B : (a : R) → B) r : B) ((algebraMap R B : (a : R) → B) r : B)
⊢ Eq.{u₁ + 1} (α := B) ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)

Tactic:
rw [algebraMap_apply R S A r, f.commutes, ← algebraMap_apply R S B]

Premises used: AlgHom.commutes, IsScalarTower.algebraMap_apply
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
⊢ Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : A →+* B) (algebraMap R A))
    (algebraMap R B)

Tactic:
RingHom.ext (AlgHom.map_algebraMap f)

Premises used: RingHom.ext, AlgHom.map_algebraMap
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
U : Subsemiring S
⊢ IsScalarTower (↥U) S A

Tactic:
of_algebraMap_eq fun _x => rfl

Premises used: IsScalarTower.of_algebraMap_eq, rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R_1 : Type u
S : Type v
A_1 : Type w
B_1 : Type u₁
M : Type v₁
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : Semiring A_1
inst_3 : Semiring B_1
inst_4 : Algebra R_1 S
inst_5 : Algebra S A_1
inst_6 : Algebra S B_1
inst_7 : Algebra R_1 A_1
inst_8 : Algebra R_1 B_1
inst_9 : IsScalarTower R_1 S A_1
inst_10 : IsScalarTower R_1 S B_1
R : Type u_1
A : Type u_2
B : Type u_3
inst_11 : CommSemiring R
inst_12 : CommSemiring A
inst_13 : CommSemiring B
inst_14 : Algebra R A
inst_15 : Algebra R B
f : A →ₐ[R] B
⊢ IsScalarTower R A B

Tactic:
letI := (f : A →+* B).toAlgebra
  of_algebraMap_eq fun x => (f.commutes x).symm

Premises used: IsScalarTower.of_algebraMap_eq, AlgHom.commutes, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
r : R
rw :
  OneHom.toFun (↑(↑(↑f : A →+* B) : A →* B) : OneHom A B)
      ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S)) =
    (algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) r : S)
⊢ OneHom.toFun (↑(↑(↑f : A →+* B) : A →* B) : OneHom A B) ((algebraMap R A : (a : R) → A) r) =
    (algebraMap R B : (a : R) → B) r

Tactic:
rw [algebraMap_apply R S A, algebraMap_apply R S B]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
r : R
⊢ OneHom.toFun (↑(↑(↑f : A →+* B) : A →* B) : OneHom A B)
      ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S)) =
    (algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) r : S)

Tactic:
f.commutes (algebraMap R S r)

Premises used: Algebra.algebraMap, AlgHom.commutes, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
r : R
⊢ OneHom.toFun (↑(↑(↑f : A →+* B) : A →* B) : OneHom A B)
      ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S)) =
    (algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) r : S)

Tactic:
exact f.commutes (algebraMap R S r)

Premises used: Algebra.algebraMap, AlgHom.commutes, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
x : A
⊢ Eq.{u₁ + 1} (α := B) ((restrictScalars R f : (a : A) → B) x : B) ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
⊢ Eq (α := A →ₗ[R] B) (toLinearMap (restrictScalars R f))
    ((↑R :
        {S : Type v} →
          {M : Type w} →
            {M₂ : Type u₁} →
              [inst : Semiring R] →
                [inst_11 : Semiring S] →
                  [inst_12 : AddCommMonoid M] →
                    [inst_13 : AddCommMonoid M₂] →
                      [inst_14 : Module R M] →
                        [inst_15 : Module R M₂] →
                          [inst_16 : Module S M] →
                            [inst_17 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f.toLinearMap)

Tactic:
rfl

Premises used: LinearMap.restrictScalars, rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
⊢ Eq (α := A →+* B) (↑(restrictScalars R f) : A →+* B) (↑f : A →+* B)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, AlgHom.restrictScalars, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
⊢ Eq (α := (a : A) → B) (⇑(restrictScalars R f) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
⊢ Function.Injective (α := A →ₐ[S] B) (β := A →ₐ[R] B) (restrictScalars R)

Tactic:
fun _ _ h =>
  AlgHom.ext (AlgHom.congr_fun h :)

Premises used: AlgHom.ext, AlgHom.congr_fun, Function.Injective
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
f : A →ₐ[R] B
⊢ ∀ (r : S),
    OneHom.toFun (↑(↑(↑f : A →+* B) : A →* B) : OneHom A B) ((algebraMap S A : (a : S) → A) r) =
      (algebraMap S B : (a : S) → B) r

Tactic:
simp [h.forall, ← IsScalarTower.algebraMap_apply]

Premises used: Function.Surjective.forall, IsScalarTower.algebraMap_apply
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
f : A →ₐ[R] B
⊢ restrictScalars R (extendScalarsOfSurjective h f) = f

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, AlgHom.restrictScalars, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A ≃ₐ[S] B
r : R
rw :
  f.toRingEquiv.toFun ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S)) =
    (algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) r : S)
⊢ f.toRingEquiv.toFun ((algebraMap R A : (a : R) → A) r) = (algebraMap R B : (a : R) → B) r

Tactic:
rw [algebraMap_apply R S A, algebraMap_apply R S B]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A ≃ₐ[S] B
r : R
⊢ f.toRingEquiv.toFun ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S)) =
    (algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) r : S)

Tactic:
f.commutes (algebraMap R S r)

Premises used: Algebra.algebraMap, AlgEquiv.commutes, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A ≃ₐ[S] B
r : R
⊢ f.toRingEquiv.toFun ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S)) =
    (algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) r : S)

Tactic:
exact f.commutes (algebraMap R S r)

Premises used: Algebra.algebraMap, AlgEquiv.commutes, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A ≃ₐ[S] B
x : A
⊢ Eq.{u₁ + 1} (α := B) ((restrictScalars R f : (a : A) → B) x : B) ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A ≃ₐ[S] B
⊢ Eq (α := A →ₐ[R] B) (↑(restrictScalars R f) : A →ₐ[R] B) (AlgHom.restrictScalars R (↑f : A →ₐ[S] B))

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, MonoidHomClass.toMonoidHom, AlgHom.restrictScalars, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A ≃ₐ[S] B
⊢ Eq (α := A ≃ₗ[R] B) (↑(restrictScalars R f) : A ≃ₗ[R] B) (LinearEquiv.restrictScalars R (↑f : A ≃ₗ[S] B))

Tactic:
rfl

Premises used: LinearMap.restrictScalars, LinearEquiv.restrictScalars, AlgEquiv.toLinearEquiv, rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A ≃ₐ[S] B
⊢ toRingEquiv (restrictScalars R f) = f.toRingEquiv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A ≃ₐ[S] B
⊢ Eq (α := (a : A) → B) (⇑(restrictScalars R f) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
⊢ Function.Injective (α := A ≃ₐ[S] B) (β := A ≃ₐ[R] B) (restrictScalars R)

Tactic:
fun _ _ h =>
  AlgEquiv.ext (AlgEquiv.congr_fun h :)

Premises used: AlgEquiv.ext, Function.Injective, AlgEquiv.congr_fun
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A ≃ₐ[S] B
x : B
⊢ Eq.{w + 1} (α := A) ((symm (restrictScalars R f) : (a : B) → A) x : A) ((f.symm : (a : B) → A) x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A ≃ₐ[S] B
⊢ toRingEquiv (symm (restrictScalars R f)) = f.symm.toRingEquiv

Tactic:
rfl

Premises used: AlgEquiv.restrictScalars, rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A ≃ₐ[S] B
⊢ Eq (α := (a : B) → A) (⇑(symm (restrictScalars R f)) : (a : B) → A) (⇑f.symm : (a : B) → A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
f : A ≃ₐ[R] B
⊢ Eq (α := (a : A) → B) (⇑(extendScalarsOfSurjective h f) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
f : A ≃ₐ[R] B
⊢ restrictScalars R (extendScalarsOfSurjective h f) = f

Tactic:
rfl

Premises used: AlgEquiv.restrictScalars, rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
f : A ≃ₐ[R] B
⊢ Eq (α := B ≃ₐ[S] A) (symm (extendScalarsOfSurjective h f)) (extendScalarsOfSurjective h f.symm)

Tactic:
rfl

Premises used: AlgEquiv.symm, AlgEquiv.extendScalarsOfSurjective, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
A : Type w
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
hsur : Function.Surjective.{u + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
X : Set M
⊢ Eq (α := Submodule R M) (restrictScalars R (span A X)) (span R X)

Tactic:
((span_le_restrictScalars R A X).antisymm fun m hm => ?_).symm

Premises used: Submodule.span_le_restrictScalars, LE.le.antisymm, Eq.symm