mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
x✝ : A
⊢ ((lift hg).comp (algebraMap A K)) x✝ = g x✝

Tactic:
;

Goal state after:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
x✝ : A
⊢ ((lift hg).comp (algebraMap A K)) x✝ = g x✝
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
s : Set L
hs : g.range = Subring.closure s
x✝ : A
⊢ ((lift hg).comp (algebraMap A K)) x✝ = g x✝

Tactic:
;

Goal state after:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
s : Set L
hs : g.range = Subring.closure s
x✝ : A
⊢ ((lift hg).comp (algebraMap A K)) x✝ = g x✝
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
K : Type u_9
inst✝³ : CommRing A
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : K
⊢ (ringEquivOfRingEquiv (RingEquiv.refl A)) x✝ = (RingEquiv.refl K) x✝

Tactic:
;

Goal state after:
A : Type u_8
K : Type u_9
inst✝³ : CommRing A
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : K
⊢ (ringEquivOfRingEquiv (RingEquiv.refl A)) x✝ = (RingEquiv.refl K) x✝
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := ⋯
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ ∀ (r : R), (algebraMap R S) r = (algebraMap R S) r

Tactic:
intro r

Goal state after:
case e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
r : R
⊢ (algebraMap R S) r = (algebraMap R S) r
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
B : Type u_9
C : Type u_10
inst✝²¹ : CommRing A
inst✝²⁰ : CommRing B
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A B
inst✝¹⁷ : Algebra A C
FA : Type u_12
FB : Type u_13
FC : Type u_14
inst✝¹⁶ : Field FA
inst✝¹⁵ : Field FB
inst✝¹⁴ : Field FC
inst✝¹³ : Algebra A FA
inst✝¹² : Algebra B FB
inst✝¹¹ : Algebra C FC
inst✝¹⁰ : IsFractionRing A FA
inst✝⁹ : IsFractionRing B FB
inst✝⁸ : IsFractionRing C FC
inst✝⁷ : Algebra A FB
inst✝⁶ : IsScalarTower A B FB
inst✝⁵ : Algebra A FC
inst✝⁴ : IsScalarTower A C FC
inst✝³ : Algebra FA FB
inst✝² : IsScalarTower A FA FB
inst✝¹ : Algebra FA FC
inst✝ : IsScalarTower A FA FC
f : B ≃ₐ[A] C
a✝ : FB
⊢ (AlgEquiv.restrictScalars A (fieldEquivOfAlgEquiv FA FB FC f)) a✝ = (algEquivOfAlgEquiv f) a✝

Tactic:
;

Goal state after:
A : Type u_8
B : Type u_9
C : Type u_10
inst✝²¹ : CommRing A
inst✝²⁰ : CommRing B
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A B
inst✝¹⁷ : Algebra A C
FA : Type u_12
FB : Type u_13
FC : Type u_14
inst✝¹⁶ : Field FA
inst✝¹⁵ : Field FB
inst✝¹⁴ : Field FC
inst✝¹³ : Algebra A FA
inst✝¹² : Algebra B FB
inst✝¹¹ : Algebra C FC
inst✝¹⁰ : IsFractionRing A FA
inst✝⁹ : IsFractionRing B FB
inst✝⁸ : IsFractionRing C FC
inst✝⁷ : Algebra A FB
inst✝⁶ : IsScalarTower A B FB
inst✝⁵ : Algebra A FC
inst✝⁴ : IsScalarTower A C FC
inst✝³ : Algebra FA FB
inst✝² : IsScalarTower A FA FB
inst✝¹ : Algebra FA FC
inst✝ : IsScalarTower A FA FC
f : B ≃ₐ[A] C
a✝ : FB
⊢ (AlgEquiv.restrictScalars A (fieldEquivOfAlgEquiv FA FB FC f)) a✝ = (algEquivOfAlgEquiv f) a✝
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ (algebraMap R (Localization M)) ((algebraMap A R) m) = (algebraMap A (Localization M)) m

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ (algebraMap R (Localization M)) ((algebraMap A R) m) = (algebraMap A (Localization M)) m
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
⊢ Injective ⇑(fieldEquivOfAlgEquivHom K L)

Tactic:
by
  intro f g h
  ext b
  simpa using AlgEquiv.ext_iff.mp h (algebraMap B L b)

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (N ⊗[R] M)
hs : Finite ↑s
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
x : N ⊗[R] M
hx : x ∈ s
⊢ (rTensor M ((⨆ x, J ↑x).subtype ∘ₗ inclusion ⋯)) (y x) = (rTensor M (J x).subtype) (y x)

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (N ⊗[R] M)
hs : Finite ↑s
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
x : N ⊗[R] M
hx : x ∈ s
⊢ (rTensor M ((⨆ x, J ↑x).subtype ∘ₗ inclusion ⋯)) (y x) = (rTensor M (J x).subtype) (y x)
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
J : Submodule R ↥I
fg : J.FG
y : ↥J ⊗[R] M
⊢ (rTensor M J.subtype) y = (rTensor M (inclusion ⋯ ∘ₗ I.subtype.submoduleMap J)) y

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
J : Submodule R ↥I
fg : J.FG
y : ↥J ⊗[R] M
⊢ (rTensor M J.subtype) y = (rTensor M (inclusion ⋯ ∘ₗ I.subtype.submoduleMap J)) y
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
⊢ (algEquiv M S) (mk' (Localization M) x y) = mk' S x y

Tactic:
algEquiv_mk'

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
⊢ mk' S x y = mk' S x y
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
s : Set (↥I ⊗[R] M)
hs : Finite ↑s
J : ↥I ⊗[R] M → Submodule R N
fg : ∀ (x : ↥I ⊗[R] M), (J x).FG
hle : ∀ (x : ↥I ⊗[R] M), J x ≤ I
y : (x : ↥I ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : ↥I ⊗[R] M), x = (rTensor M (inclusion ⋯)) (y x)
x : ↥I ⊗[R] M
hx : x ∈ s
⊢ (rTensor M (inclusion ⋯ ∘ₗ inclusion ⋯)) (y x) = (rTensor M (inclusion ⋯)) (y x)

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
s : Set (↥I ⊗[R] M)
hs : Finite ↑s
J : ↥I ⊗[R] M → Submodule R N
fg : ∀ (x : ↥I ⊗[R] M), (J x).FG
hle : ∀ (x : ↥I ⊗[R] M), J x ≤ I
y : (x : ↥I ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : ↥I ⊗[R] M), x = (rTensor M (inclusion ⋯)) (y x)
x : ↥I ⊗[R] M
hx : x ∈ s
⊢ (rTensor M (inclusion ⋯ ∘ₗ inclusion ⋯)) (y x) = (rTensor M (inclusion ⋯)) (y x)
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
x : ℕ
hx : x ∈ s
e : n ≤ x
y : Fin n
⊢ y ∈ Fin.val ⁻¹' Set.Iio x ↔ y ∈ Set.univ

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
x : ℕ
hx : x ∈ s
e : n ≤ x
y : Fin n
⊢ y ∈ Fin.val ⁻¹' Set.Iio x ↔ y ∈ Set.univ
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommRing S
f : R →+* S
Rₘ : Type u_3
inst✝⁶ : CommRing Rₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
Sₘ : Type u_4
N : Submonoid S
inst✝³ : CommRing Sₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization N Sₘ
hf : M ≤ Submonoid.comap f N
hN : 0 ∉ N
inst✝ : IsDomain S
hf' : Injective ⇑f
⊢ Injective ⇑(map Sₘ f hf)

Tactic:
refine (injective_iff_map_eq_zero (map Sₘ f hf)).mpr fun x h ↦ ?_
  obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M x
  aesop (add simp [map_mk', mk'_eq_zero_iff])

Goal state after:
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
x✝ : ∃ a_1 ∈ M, a_1 * (↑d * a) = a_1 * (↑b * c)
u : R
hu : u ∈ M
h : u * (↑d * a) = u * (↑b * c)
⊢ a * ↑d = ↑b * c

Tactic:
have hu' : u ∈ nonZeroDivisors R := hM hu

Goal state after:
R : Type u_1
inst✝ : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
x✝ : ∃ a_1 ∈ M, a_1 * (↑d * a) = a_1 * (↑b * c)
u : R
hu : u ∈ M
h : u * (↑d * a) = u * (↑b * c)
hu' : u ∈ nonZeroDivisors R
⊢ a * ↑d = ↑b * c
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s))) = ⊤
⊢ ⊤ = Submodule.span R (⇑(Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))).mkQ '' {f ⟨sSup s, ⋯⟩})

Tactic:
← Submodule.map_span,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s))) = ⊤
⊢ ⊤ = Submodule.map (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))).mkQ (R ∙ f ⟨sSup s, ⋯⟩)
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective ⇑ϕ
ψ : M ⊗[R] M →ₗ[R] R ⧸ I := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial (R ⧸ I)
x : R ⧸ I
⊢ ∃ a, ψ a = x

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective ⇑ϕ
ψ : M ⊗[R] M →ₗ[R] R ⧸ I := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial (R ⧸ I)
x : R ⧸ I
⊢ ∃ a, ψ a = x
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective ⇑ϕ
ψ : M ⊗[R] M →ₗ[R] R ⧸ I := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial (R ⧸ I)
x : M
⊢ ∃ a, ψ a = ϕ x

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective ⇑ϕ
ψ : M ⊗[R] M →ₗ[R] R ⧸ I := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial (R ⧸ I)
x : M
⊢ ∃ a, ψ a = ϕ x
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective ⇑ϕ
ψ : M ⊗[R] M →ₗ[R] R ⧸ I := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial (R ⧸ I)
x y : M
hy : ϕ y = 1
⊢ ∃ a, ψ a = ϕ x

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective ⇑ϕ
ψ : M ⊗[R] M →ₗ[R] R ⧸ I := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial (R ⧸ I)
x y : M
hy : ϕ y = 1
⊢ ∃ a, ψ a = ϕ x
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this✝¹ : Algebra S S' := f.toAlgebra
this✝ : IsScalarTower R S S'
this : Module.Finite S S'
x✝ : T
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((↑((Algebra.TensorProduct.comm S (TensorProduct R S T) S').trans
                    (Algebra.TensorProduct.cancelBaseChange R S S S' T))).comp
              Algebra.TensorProduct.includeLeft)).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this✝¹ : Algebra S S' := f.toAlgebra
this✝ : IsScalarTower R S S'
this : Module.Finite S S'
x✝ : T
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((↑((Algebra.TensorProduct.comm S (TensorProduct R S T) S').trans
                    (Algebra.TensorProduct.cancelBaseChange R S S S' T))).comp
              Algebra.TensorProduct.includeLeft)).comp
        Algebra.TensorProduct.includeRight)
      x✝
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
this : ∀ (a : A) (m : M), 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m
f : M →ₗ[R] A ⊗[R] M := { toFun := fun m ↦ 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
a : A
m : M
⊢ ((AlgebraTensorModule.curry (f ∘ₗ lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)))) a) m =
    ((AlgebraTensorModule.curry LinearMap.id) a) m

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
this : ∀ (a : A) (m : M), 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m
f : M →ₗ[R] A ⊗[R] M := { toFun := fun m ↦ 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
a : A
m : M
⊢ ((AlgebraTensorModule.curry (f ∘ₗ lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)))) a) m =
    ((AlgebraTensorModule.curry LinearMap.id) a) m
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
x✝ y✝ : A
⊢ { toFun := fun y ↦ (x✝ + y✝) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun y ↦ x✝ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun y ↦ y✝ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
x✝ y✝ : A
⊢ { toFun := fun y ↦ (x✝ + y✝) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun y ↦ x✝ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun y ↦ y✝ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ }
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
x✝¹ y✝ x✝ : A
⊢ { toFun := fun y ↦ (x✝¹ + y✝) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } x✝ =
    ({ toFun := fun y ↦ x✝¹ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun y ↦ y✝ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ })
      x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
x✝¹ y✝ x✝ : A
⊢ { toFun := fun y ↦ (x✝¹ + y✝) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } x✝ =
    ({ toFun := fun y ↦ x✝¹ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun y ↦ y✝ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ })
      x✝
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
m✝ : R
x✝ : A
⊢ { toFun := fun y ↦ (m✝ • x✝) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) m✝ • { toFun := fun y ↦ x✝ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
m✝ : R
x✝ : A
⊢ { toFun := fun y ↦ (m✝ • x✝) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) m✝ • { toFun := fun y ↦ x✝ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ }
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
m✝ : R
x✝¹ x✝ : A
⊢ { toFun := fun y ↦ (m✝ • x✝¹) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } x✝ =
    ((RingHom.id R) m✝ • { toFun := fun y ↦ x✝¹ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ }) x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
m✝ : R
x✝¹ x✝ : A
⊢ { toFun := fun y ↦ (m✝ • x✝¹) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } x✝ =
    ((RingHom.id R) m✝ • { toFun := fun y ↦ x✝¹ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ }) x✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : AddGroupWithOne β
n : ℕ
⊢ e.invFun ↑n = ↑n

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : AddGroupWithOne β
n : ℕ
⊢ e.invFun ↑n = ↑n
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : NonUnitalNonAssocSemiring B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : SMulCommClass R A A
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R A A
inst✝ : IsScalarTower R B B
a : A
b : B
x✝¹ : A
x✝ : B
⊢ ((AlgebraTensorModule.curry (mulLeft R (a ⊗ₜ[R] b))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (map (mulLeft R a) (mulLeft R b))) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : NonUnitalNonAssocSemiring B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : SMulCommClass R A A
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R A A
inst✝ : IsScalarTower R B B
a : A
b : B
x✝¹ : A
x✝ : B
⊢ ((AlgebraTensorModule.curry (mulLeft R (a ⊗ₜ[R] b))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (map (mulLeft R a) (mulLeft R b))) x✝¹) x✝
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : NonUnitalNonAssocSemiring B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : SMulCommClass R A A
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R A A
inst✝ : IsScalarTower R B B
a : A
b : B
x✝¹ : A
x✝ : B
⊢ ((AlgebraTensorModule.curry (mulRight R (a ⊗ₜ[R] b))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (map (mulRight R a) (mulRight R b))) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : NonUnitalNonAssocSemiring B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : SMulCommClass R A A
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R A A
inst✝ : IsScalarTower R B B
a : A
b : B
x✝¹ : A
x✝ : B
⊢ ((AlgebraTensorModule.curry (mulRight R (a ⊗ₜ[R] b))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (map (mulRight R a) (mulRight R b))) x✝¹) x✝