awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A₁ i)
inst_2 : (i : ι) → Semiring (A₂ i)
inst_3 : (i : ι) → Semiring (A₃ i)
inst_4 : (i : ι) → Algebra.{u_3, u_5} R (A₁ i)
inst_5 : (i : ι) → Algebra.{u_3, u_6} R (A₂ i)
inst_6 : (i : ι) → Algebra.{u_3, u_7} R (A₃ i)
S : Type u_8
inst_7 : Semiring S
inst_8 : Algebra R S
x : R
fst :
  ∀ (x_1 : α),
    Eq.{u_8 + 1} (α := S)
      ((((RingEquiv.sumArrowEquivProdArrow α β S : (α ⊕ β → S) ≃+* (α → S) × (β → S)) :
              (a : α ⊕ β → S) → (α → S) × (β → S))
            ((algebraMap R (α ⊕ β → S) : (a : R) → α ⊕ β → S) x)).1
        x_1)
      (((algebraMap R ((α → S) × (β → S)) : (a : R) → (α → S) × (β → S)) x).1 x_1)
snd :
  ∀ (x_1 : β),
    Eq.{u_8 + 1} (α := S)
      ((((RingEquiv.sumArrowEquivProdArrow α β S : (α ⊕ β → S) ≃+* (α → S) × (β → S)) :
              (a : α ⊕ β → S) → (α → S) × (β → S))
            ((algebraMap R (α ⊕ β → S) : (a : R) → α ⊕ β → S) x)).2
        x_1)
      (((algebraMap R ((α → S) × (β → S)) : (a : R) → (α → S) × (β → S)) x).2 x_1)
⊢ Eq (α := (α → S) × (β → S))
    (((RingEquiv.sumArrowEquivProdArrow α β S : (α ⊕ β → S) ≃+* (α → S) × (β → S)) :
          (a : α ⊕ β → S) → (α → S) × (β → S))
        ((algebraMap R (α ⊕ β → S) : (a : R) → α ⊕ β → S) x) :
      (α → S) × (β → S))
    ((algebraMap R ((α → S) × (β → S)) : (a : R) → (α → S) × (β → S)) x : (α → S) × (β → S))

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A₁ i)
inst_2 : (i : ι) → Semiring (A₂ i)
inst_3 : (i : ι) → Semiring (A₃ i)
inst_4 : (i : ι) → Algebra.{u_3, u_5} R (A₁ i)
inst_5 : (i : ι) → Algebra.{u_3, u_6} R (A₂ i)
inst_6 : (i : ι) → Algebra.{u_3, u_7} R (A₃ i)
S : Type u_8
inst_7 : Semiring S
inst_8 : Algebra R S
x : R
x_1 : α
⊢ Eq.{u_8 + 1} (α := S)
    ((((RingEquiv.sumArrowEquivProdArrow α β S : (α ⊕ β → S) ≃+* (α → S) × (β → S)) :
            (a : α ⊕ β → S) → (α → S) × (β → S))
          ((algebraMap R (α ⊕ β → S) : (a : R) → α ⊕ β → S) x)).1
      x_1)
    (((algebraMap R ((α → S) × (β → S)) : (a : R) → (α → S) × (β → S)) x).1 x_1)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A₁ i)
inst_2 : (i : ι) → Semiring (A₂ i)
inst_3 : (i : ι) → Semiring (A₃ i)
inst_4 : (i : ι) → Algebra.{u_3, u_5} R (A₁ i)
inst_5 : (i : ι) → Algebra.{u_3, u_6} R (A₂ i)
inst_6 : (i : ι) → Algebra.{u_3, u_7} R (A₃ i)
S : Type u_8
inst_7 : Semiring S
inst_8 : Algebra R S
x : R
x_1 : β
⊢ Eq.{u_8 + 1} (α := S)
    ((((RingEquiv.sumArrowEquivProdArrow α β S : (α ⊕ β → S) ≃+* (α → S) × (β → S)) :
            (a : α ⊕ β → S) → (α → S) × (β → S))
          ((algebraMap R (α ⊕ β → S) : (a : R) → α ⊕ β → S) x)).2
      x_1)
    (((algebraMap R ((α → S) × (β → S)) : (a : R) → (α → S) × (β → S)) x).2 x_1)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : CommSemiring R
S : Type u_8
inst_1 : Semiring S
inst_2 : Algebra R S
x : α ⊕ β → S
⊢ Eq (α := (α → S) × (β → S))
    ((sumArrowEquivProdArrow α β R S : (a : α ⊕ β → S) → (α → S) × (β → S)) x : (α → S) × (β → S))
    ((Equiv.sumArrowEquivProdArrow α β S : (a : α ⊕ β → S) → (α → S) × (β → S)) x : (α → S) × (β → S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : CommSemiring R
S : Type u_8
inst_1 : Semiring S
inst_2 : Algebra R S
x : (α → S) × (β → S)
⊢ Eq (α := α ⊕ β → S) ((symm (sumArrowEquivProdArrow α β R S) : (a : (α → S) × (β → S)) → α ⊕ β → S) x : α ⊕ β → S)
    (((Equiv.sumArrowEquivProdArrow α β S).symm : (a : (α → S) × (β → S)) → α ⊕ β → S) x : α ⊕ β → S)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
v w : ι → R
⊢ (⇑(algebraMap R A) : (a : R) → A) ∘ (v + w) =
    HAdd.hAdd (α := ι → A) ((⇑(algebraMap R A) : (a : R) → A) ∘ v) ((⇑(algebraMap R A) : (a : R) → A) ∘ w)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
t : R
v : ι → R
h :
  ∀ (x : ι),
    ((⇑(algebraMap R A) : (a : R) → A) ∘ (t • v)) x =
      HSMul.hSMul (α := R) (β := ι → A) ((RingHom.id R : (a : R) → R) t : R) ((⇑(algebraMap R A) : (a : R) → A) ∘ v) x
⊢ (⇑(algebraMap R A) : (a : R) → A) ∘ (t • v) =
    HSMul.hSMul (α := R) (β := ι → A) ((RingHom.id R : (a : R) → R) t : R) ((⇑(algebraMap R A) : (a : R) → A) ∘ v)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
t : R
v : ι → R
x : ι
⊢ ((⇑(algebraMap R A) : (a : R) → A) ∘ (t • v)) x =
    HSMul.hSMul (α := R) (β := ι → A) ((RingHom.id R : (a : R) → R) t : R) ((⇑(algebraMap R A) : (a : R) → A) ∘ v) x

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
r : R
a : A
b : B
dsimp :
  (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b) =
    (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
      HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) r : B))
⊢ HMul.hMul (α := A × B) ((RingHom.prod (algebraMap R A) (algebraMap R B) : (a : R) → A × B) r : A × B) (a, b) =
    HMul.hMul (β := A × B) (a, b) ((RingHom.prod (algebraMap R A) (algebraMap R B) : (a : R) → A × B) r : A × B)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
r : R
a : A
b : B
rw :
  (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b) =
    (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
      HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) r : B))
rw₁ rw₂ :
  (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
      HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) r : B)) =
    (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
      HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) r : B))
⊢ (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b) =
    (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
      HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) r : B))

Tactic:
rw [commutes r a, commutes r b]

Premises used: Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
r : R
a : A
b : B
dsimp :
  (r • a, r • b) =
    (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b)
⊢ r • (a, b) =
    HMul.hMul (α := A × B) ((RingHom.prod (algebraMap R A) (algebraMap R B) : (a : R) → A × B) r : A × B) (a, b)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
r : R
a : A
b : B
rw :
  (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a, r • b) =
    (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b)
rw₁ rw₂ :
  (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b) =
    (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b)
⊢ (r • a, r • b) =
    (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b)

Tactic:
rw [Algebra.smul_def r a, Algebra.smul_def r b]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
r : R
⊢ Eq (α := A × B) ((algebraMap R (A × B) : (a : R) → A × B) r : A × B)
    (((algebraMap R A : (a : R) → A) r, (algebraMap R B : (a : R) → B) r) : A × B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
a : A × B
⊢ (fst R A B : (a : A × B) → A) a = a.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
a : A × B
⊢ (snd R A B : (a : A × B) → B) a = a.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
r : R
⊢ (↑(↑(f.prod g.toRingHom) : A →* B × C) : OneHom A (B × C)).toFun ((algebraMap R A : (a : R) → A) r) =
    (algebraMap R (B × C) : (a : R) → B × C) r

Tactic:
simp only [toRingHom_eq_coe, RingHom.toFun_eq_coe, RingHom.prod_apply, coe_toRingHom,
        commutes, Prod.algebraMap_apply]

Premises used: AlgHom.coe_toRingHom, RingHom.toFun_eq_coe, Prod.algebraMap_apply, AlgHom.toRingHom_eq_coe, AlgHom.commutes, RingHom.prod_apply
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
⊢ Eq (α := (a : A) → B × C) (⇑(f.prod g) : (a : A) → B × C)
    (Function.prod (α := fun (a : A) ↦ B) (β := fun (a : A) ↦ C) (⇑f : (a : A) → B) (⇑g : (a : A) → C))

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
H : ∀ (x : A), Eq.{u_3 + 1} (α := B) ((comp (fst R B C) (f.prod g) : (a : A) → B) x : B) ((f : (a : A) → B) x : B)
⊢ comp (fst R B C) (f.prod g) = f

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
x : A
⊢ Eq.{u_3 + 1} (α := B) ((comp (fst R B C) (f.prod g) : (a : A) → B) x : B) ((f : (a : A) → B) x : B)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
H : ∀ (x : A), Eq.{u_4 + 1} (α := C) ((comp (snd R B C) (f.prod g) : (a : A) → C) x : C) ((g : (a : A) → C) x : C)
⊢ comp (snd R B C) (f.prod g) = g

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
x : A
⊢ Eq.{u_4 + 1} (α := C) ((comp (snd R B C) (f.prod g) : (a : A) → C) x : C) ((g : (a : A) → C) x : C)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
⊢ Eq (α := A × B →ₐ[R] A × B) (prod (fst R A B) (snd R A B)) (AlgHom.id R (A × B))

Tactic:
rfl

Premises used: AlgHom.id, RingHom.prod, rfl, AlgHom.prod
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
C' : Type u_5
inst_7 : Semiring C'
inst_8 : Algebra R C'
f : A →ₐ[R] B
g : B →ₐ[R] C
g' : B →ₐ[R] C'
⊢ (g.prod g').comp f = (g.comp f).prod (g'.comp f)

Tactic:
rfl

Premises used: AlgHom.comp, RingHom.prod, rfl, AlgHom.prod
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
D : Type u_5
inst_7 : Semiring D
inst_8 : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
r : R
⊢ (↑(↑(f.prodMap g.toRingHom) : A × C →* B × D) : OneHom (A × C) (B × D)).toFun
      ((algebraMap R (A × C) : (a : R) → A × C) r) =
    (algebraMap R (B × D) : (a : R) → B × D) r

Tactic:
simp [commutes]

Premises used: AlgHom.commutes
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
A_1 : Type u_2
B_1 : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A_1
inst_2 : Algebra R A_1
inst_3 : Semiring B_1
inst_4 : Algebra R B_1
inst_5 : Semiring C
inst_6 : Algebra R C
S : Type u_5
T : Type u_6
A : Type u_7
B : Type u_8
inst_7 : Semiring A
inst_8 : Semiring B
inst_9 : Semiring S
inst_10 : Semiring T
inst_11 : Algebra R S
inst_12 : Algebra R T
inst_13 : Algebra R A
inst_14 : Algebra R B
l : S ≃ₐ[R] A
r : T ≃ₐ[R] B
⊢ ∀ (x : R),
    Eq (α := A × B)
      ((l.toRingEquiv.prodCongr r.toRingEquiv : (a : S × T) → A × B) ((algebraMap R (S × T) : (a : R) → S × T) x) :
        A × B)
      ((algebraMap R (A × B) : (a : R) → A × B) x : A × B)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_5
T : Type u_6
A : Type u_7
B : Type u_8
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring S
inst_4 : Semiring T
inst_5 : Algebra R S
inst_6 : Algebra R T
inst_7 : Algebra R A
inst_8 : Algebra R B
l : S ≃ₐ[R] A
r : T ≃ₐ[R] B
x : S × T
⊢ Eq (α := A × B) ((l.prodCongr r : (a : S × T) → A × B) x : A × B)
    (((↑l : S ≃ A).prodCongr (↑r : T ≃ B) : (a : S × T) → A × B) x : A × B)

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Algebra.Algebra.Prod
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_5
T : Type u_6
A : Type u_7
B : Type u_8
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring S
inst_4 : Semiring T
inst_5 : Algebra R S
inst_6 : Algebra R T
inst_7 : Algebra R A
inst_8 : Algebra R B
l : S ≃ₐ[R] A
r : T ≃ₐ[R] B
x : A × B
⊢ Eq (α := S × T) (((l.prodCongr r).symm : (a : A × B) → S × T) x : S × T)
    ((((↑l : S ≃ A).prodCongr (↑r : T ≃ B)).symm : (a : A × B) → S × T) x : S × T)

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Algebra.Algebra.Rat
Goal:
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : Algebra ℚ R
inst_3 : Algebra ℚ S
f : R →+* S
r : ℚ
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((algebraMap ℚ R : (a : ℚ) → R) r : R) : S)
    ((algebraMap ℚ S : (a : ℚ) → S) r : S)

Tactic:
RingHom.ext_iff.1 (Subsingleton.elim (f.comp (algebraMap ℚ R)) (algebraMap ℚ S)) r

Premises used: Algebra.algebraMap, Rat, RingHom.ext_iff, RingHom.comp, Iff.mp, Subsingleton.elim
-- Module: Mathlib.Algebra.Algebra.Rat
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : DivisionSemiring R
inst_1 : CharZero R
inst_2 : DivisionSemiring S
inst_3 : CharZero S
inst_4 : FunLike F R S
inst_5 : RingHomClass F R S
f : F
q : ℚ≥0
a : R
⊢ (f : (a : R) → S) (q • a) =
    HSMul.hSMul (α := ℚ≥0) (β := S) ((RingHom.id ℚ≥0 : (a : ℚ≥0) → ℚ≥0) q : ℚ≥0) ((f : (a : R) → S) a : S)

Tactic:
simp [smul_def, cast_id]

Premises used: NNRat.cast_id, NNRat.smul_def
-- Module: Mathlib.Algebra.Algebra.Rat
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : DivisionSemiring R
inst_1 : CharZero R
inst_2 : DivisionSemiring S
inst_3 : CharZero S
inst_4 : SMul R S
inst_5 : SMulCommClass R S S
q : ℚ≥0
a : R
b : S
⊢ q • a • b = a • q • b

Tactic:
simp [smul_def, mul_smul_comm]

Premises used: mul_smul_comm, NNRat.smul_def
-- Module: Mathlib.Algebra.Algebra.Rat
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : DivisionSemiring R
inst_1 : CharZero R
inst_2 : DivisionSemiring S
inst_3 : CharZero S
inst_4 : SMul R S
inst_5 : SMulCommClass S R S
⊢ SMulCommClass R ℚ≥0 S

Tactic:
have := SMulCommClass.symm S R S; SMulCommClass.symm _ _ _

Premises used: NNRat, SMulCommClass.symm
-- Module: Mathlib.Algebra.Algebra.Rat
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : DivisionRing R
inst_1 : CharZero R
inst_2 : DivisionRing S
inst_3 : CharZero S
inst_4 : FunLike F R S
inst_5 : RingHomClass F R S
f : F
q : ℚ
a : R
⊢ (f : (a : R) → S) (q • a) =
    HSMul.hSMul (α := ℚ) (β := S) ((RingHom.id ℚ : (a : ℚ) → ℚ) q : ℚ) ((f : (a : R) → S) a : S)

Tactic:
simp [smul_def, cast_id]

Premises used: Rat.smul_def, Rat.cast_id
-- Module: Mathlib.Algebra.Algebra.Rat
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : DivisionRing R
inst_1 : CharZero R
inst_2 : DivisionRing S
inst_3 : CharZero S
inst_4 : EquivLike F R S
inst_5 : RingEquivClass F R S
f : F
c : ℚ
x : R
⊢ (f : (a : R) → S) (c • x) =
    HSMul.hSMul (α := ℚ) (β := S) ((RingHom.id ℚ : (a : ℚ) → ℚ) c : ℚ) ((f : (a : R) → S) x : S)

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.Algebra.Rat
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : DivisionRing R
inst_1 : CharZero R
inst_2 : DivisionRing S
inst_3 : CharZero S
inst_4 : SMul R S
inst_5 : SMulCommClass R S S
q : ℚ
a : R
b : S
⊢ q • a • b = a • q • b

Tactic:
simp [smul_def, mul_smul_comm]

Premises used: mul_smul_comm, Rat.smul_def
-- Module: Mathlib.Algebra.Algebra.Rat
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : DivisionRing R
inst_1 : CharZero R
inst_2 : DivisionRing S
inst_3 : CharZero S
inst_4 : SMul R S
inst_5 : SMulCommClass S R S
⊢ SMulCommClass R ℚ S

Tactic:
have := SMulCommClass.symm S R S; SMulCommClass.symm _ _ _

Premises used: Rat, SMulCommClass.symm
-- Module: Mathlib.Algebra.Algebra.Rat
Goal:
F : Type u_1
R_1 : Type u_2
S : Type u_3
inst : DivisionRing R_1
inst_1 : CharZero R_1
inst_2 : DivisionRing S
inst_3 : CharZero S
inst_4 : SMul R_1 S
R : Type u_4
inst_5 : Semiring R
⊢ Subsingleton.{u_4 + 1} (Algebra ℚ R)

Tactic:
⟨fun x y => Algebra.algebra_ext x y <| RingHom.congr_fun <| Subsingleton.elim _ _⟩

Premises used: Algebra.algebraMap, RingHom.congr_fun, Rat, Subsingleton.intro, Algebra.algebra_ext, Subsingleton.elim
-- Module: Mathlib.Algebra.Algebra.RestrictScalars
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring S
inst_1 : AddCommMonoid M
inst_2 : CommSemiring R
inst_3 : Algebra R S
inst_4 : Module S M
⊢ IsScalarTower R S M

Tactic:
IsScalarTower.of_compHom R S M

Premises used: SMul.comp.smul, IsScalarTower.of_compHom
-- Module: Mathlib.Algebra.Algebra.RestrictScalars
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
A : Type u_4
inst : Semiring S
inst_1 : AddCommMonoid M
inst_2 : CommSemiring R
inst_3 : Algebra R S
inst_4 : Module S M
⊢ IsScalarTower.{u_1, u_2, u_3} R S (RestrictScalars R S M)

Tactic:
IsScalarTower.restrictScalars R S M

Premises used: RestrictScalars, IsScalarTower.restrictScalars
-- Module: Mathlib.Algebra.Algebra.RestrictScalars
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Semiring S
inst_3 : Algebra R S
inst_4 : Module S M
c : R
x : RestrictScalars R S M
⊢ c • x =
    (AddEquiv.symm (addEquiv R S M) : (a : M) → RestrictScalars R S M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M) ((algebraMap R S : (a : R) → S) c : S)
        ((addEquiv R S M : (a : RestrictScalars R S M) → M) x : M))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.RestrictScalars
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Semiring S
inst_3 : Algebra R S
inst_4 : Module S M
c : R
x : RestrictScalars R S M
⊢ (addEquiv R S M : (a : RestrictScalars R S M) → M) (c • x) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M) ((algebraMap R S : (a : R) → S) c : S)
      ((addEquiv R S M : (a : RestrictScalars R S M) → M) x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.RestrictScalars
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Semiring S
inst_3 : Algebra R S
inst_4 : Module S M
r : R
x : M
⊢ (AddEquiv.symm (addEquiv R S M) : (a : M) → RestrictScalars R S M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) x) =
    HSMul.hSMul (β := RestrictScalars R S M) r
      ((AddEquiv.symm (addEquiv R S M) : (a : M) → RestrictScalars R S M) x : RestrictScalars R S M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.RestrictScalars
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Semiring S
inst_3 : Algebra R S
inst_4 : Module S M
r : R
s : S
x : M
rw :
  (AddEquiv.symm (addEquiv R S M) : (a : M) → RestrictScalars R S M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) (s • x)) =
    HSMul.hSMul (β := RestrictScalars R S M) r
      ((AddEquiv.symm (addEquiv R S M) : (a : M) → RestrictScalars R S M) (s • x) : RestrictScalars R S M)
⊢ (AddEquiv.symm (addEquiv R S M) : (a : M) → RestrictScalars R S M) ((r • s) • x) =
    HSMul.hSMul (β := RestrictScalars R S M) r
      ((AddEquiv.symm (addEquiv R S M) : (a : M) → RestrictScalars R S M) (s • x) : RestrictScalars R S M)

Tactic:
rw [Algebra.smul_def, mul_smul]

Premises used: Algebra.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Algebra.RestrictScalars
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Semiring S
inst_3 : Algebra R S
inst_4 : Module S M
r : R
s : S
x : M
⊢ (AddEquiv.symm (addEquiv R S M) : (a : M) → RestrictScalars R S M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) (s • x)) =
    HSMul.hSMul (β := RestrictScalars R S M) r
      ((AddEquiv.symm (addEquiv R S M) : (a : M) → RestrictScalars R S M) (s • x) : RestrictScalars R S M)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.RestrictScalars
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Semiring S
inst_3 : Algebra R S
inst_4 : Module S M
s : S
x : RestrictScalars R S M
⊢ Eq (α := RestrictScalars R S M)
    (((((lsmul R S M : AlgHom.{u_1, u_2, u_3} R S (Module.End R (RestrictScalars R S M))) :
                (a : S) → Module.End R (RestrictScalars R S M))
              s :
            Module.End R (RestrictScalars R S M)) :
          (a : RestrictScalars R S M) → RestrictScalars R S M)
        x :
      RestrictScalars R S M)
    ((AddEquiv.symm (addEquiv R S M) : (a : M) → RestrictScalars R S M)
        (HSMul.hSMul (β := M) s ((addEquiv R S M : (a : RestrictScalars R S M) → M) x : M)) :
      RestrictScalars R S M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.RestrictScalars
Goal:
R : Type u_1
S : Type u_2
A : Type u_4
inst : Semiring A
inst_1 : CommSemiring S
inst_2 : Algebra S A
inst_3 : CommSemiring R
inst_4 : Algebra R S
r : R
x : RestrictScalars R S A
⊢ (ringEquiv R S A : (a : RestrictScalars R S A) → A) (r • x) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := S) (β := A) ((algebraMap R S : (a : R) → S) r : S)
      ((ringEquiv R S A : (a : RestrictScalars R S A) → A) x : A)

Tactic:
rfl

Premises used: rfl