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

Goal state before:
pp: R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₂ T) ↑(y, ⟨(algebraMap R S₂) m, ⋯⟩).2 = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
⊢ ∃ x, a * (algebraMap S₁ T) ↑x.2 = (algebraMap S₁ T) x.1

Tactic:
← IsScalarTower.algebraMap_apply,

Goal state after:
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap R T) m = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
⊢ ∃ x, a * (algebraMap S₁ T) ↑x.2 = (algebraMap S₁ T) x.1
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₁ T) ((algebraMap R S₁) m) = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
z n : R
hn : n ∈ M₂
hz : y * (algebraMap R S₂) ↑(z, ⟨n, hn⟩).2 = (algebraMap R S₂) (z, ⟨n, hn⟩).1
hunit : IsUnit ((algebraMap R S₁) m)
⊢ a * (algebraMap S₁ T) ↑((algebraMap R S₁) z * ↑hunit.unit⁻¹, ⟨(algebraMap R S₁) n, ⋯⟩).2 =
    (algebraMap S₁ T) ((algebraMap R S₁) z) * (algebraMap S₁ T) ↑hunit.unit⁻¹

Tactic:
← IsScalarTower.algebraMap_apply,

Goal state after:
case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₁ T) ((algebraMap R S₁) m) = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
z n : R
hn : n ∈ M₂
hz : y * (algebraMap R S₂) ↑(z, ⟨n, hn⟩).2 = (algebraMap R S₂) (z, ⟨n, hn⟩).1
hunit : IsUnit ((algebraMap R S₁) m)
⊢ a * (algebraMap R T) n = (algebraMap S₁ T) ((algebraMap R S₁) z) * (algebraMap S₁ T) ↑hunit.unit⁻¹
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝¹⁹ : CommRing A
B : Type u_6
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst✝¹⁶ : Field K₁
inst✝¹⁵ : Field K₂
inst✝¹⁴ : Algebra A K₁
inst✝¹³ : Algebra A K₂
inst✝¹² : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst✝¹¹ : Field L₁
inst✝¹⁰ : Field L₂
inst✝⁹ : Algebra B L₁
inst✝⁸ : Algebra B L₂
inst✝⁷ : Algebra K₁ L₁
inst✝⁶ : Algebra K₂ L₂
inst✝⁵ : Algebra A L₁
inst✝⁴ : Algebra A L₂
inst✝³ : IsScalarTower A K₁ L₁
inst✝² : IsScalarTower A K₂ L₂
inst✝¹ : IsScalarTower A B L₁
inst✝ : IsScalarTower A B L₂
e : K₁ →ₐ[A] K₂
f : L₁ →ₐ[B] L₂
r s : A
hs : s ∈ A⁰
⊢ (algebraMap K₂ L₂) ((algebraMap A K₂) r) / (algebraMap K₂ L₂) ((algebraMap A K₂) s) =
    f ((algebraMap K₁ L₁) ((algebraMap A K₁) r)) / f ((algebraMap K₁ L₁) ((algebraMap A K₁) s))

Tactic:
← IsScalarTower.algebraMap_apply,

Goal state after:
A : Type u_4
inst✝¹⁹ : CommRing A
B : Type u_6
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst✝¹⁶ : Field K₁
inst✝¹⁵ : Field K₂
inst✝¹⁴ : Algebra A K₁
inst✝¹³ : Algebra A K₂
inst✝¹² : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst✝¹¹ : Field L₁
inst✝¹⁰ : Field L₂
inst✝⁹ : Algebra B L₁
inst✝⁸ : Algebra B L₂
inst✝⁷ : Algebra K₁ L₁
inst✝⁶ : Algebra K₂ L₂
inst✝⁵ : Algebra A L₁
inst✝⁴ : Algebra A L₂
inst✝³ : IsScalarTower A K₁ L₁
inst✝² : IsScalarTower A K₂ L₂
inst✝¹ : IsScalarTower A B L₁
inst✝ : IsScalarTower A B L₂
e : K₁ →ₐ[A] K₂
f : L₁ →ₐ[B] L₂
r s : A
hs : s ∈ A⁰
⊢ (algebraMap A L₂) r / (algebraMap A L₂) s = f ((algebraMap A L₁) r) / f ((algebraMap A L₁) s)
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝⁴¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴⁰ : CommRing S
inst✝³⁹ : Algebra R S
P : Type u_3
inst✝³⁸ : CommRing P
A✝ : Type u_4
inst✝³⁷ : CommRing A✝
K : Type u_5
B✝ : Type u_6
inst✝³⁶ : CommRing B✝
inst✝³⁵ : IsDomain B✝
inst✝³⁴ : Field K
L : Type u_7
inst✝³³ : Field L
inst✝³² : Algebra A✝ K
inst✝³¹ : IsFractionRing A✝ K
g : A✝ →+* L
A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst✝³⁰ : CommRing A
inst✝²⁹ : CommRing B
inst✝²⁸ : CommRing C
inst✝²⁷ : CommRing D
inst✝²⁶ : Algebra A B
inst✝²⁵ : Algebra A C
inst✝²⁴ : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst✝²³ : Field FA
inst✝²² : Field FB
inst✝²¹ : Field FC
inst✝²⁰ : Field FD
inst✝¹⁹ : Algebra A FA
inst✝¹⁸ : Algebra B FB
inst✝¹⁷ : Algebra C FC
inst✝¹⁶ : Algebra D FD
inst✝¹⁵ : IsFractionRing A FA
inst✝¹⁴ : IsFractionRing B FB
inst✝¹³ : IsFractionRing C FC
inst✝¹² : IsFractionRing D FD
inst✝¹¹ : Algebra A FB
inst✝¹⁰ : IsScalarTower A B FB
inst✝⁹ : Algebra A FC
inst✝⁸ : IsScalarTower A C FC
inst✝⁷ : Algebra A FD
inst✝⁶ : IsScalarTower A D FD
inst✝⁵ : Algebra FA FB
inst✝⁴ : IsScalarTower A FA FB
inst✝³ : Algebra FA FC
inst✝² : IsScalarTower A FA FC
inst✝¹ : Algebra FA FD
inst✝ : IsScalarTower A FA FD
f : B ≃ₐ[A] C
x y : A
⊢ (ringEquivOfRingEquiv f.toRingEquiv).toFun
      ((algebraMap FA FB) ((algebraMap A FA) x) / (algebraMap FA FB) ((algebraMap A FA) y)) =
    (algebraMap FA FC) ((algebraMap A FA) x) / (algebraMap FA FC) ((algebraMap A FA) y)

Tactic:
← IsScalarTower.algebraMap_apply,

Goal state after:
R : Type u_1
inst✝⁴¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴⁰ : CommRing S
inst✝³⁹ : Algebra R S
P : Type u_3
inst✝³⁸ : CommRing P
A✝ : Type u_4
inst✝³⁷ : CommRing A✝
K : Type u_5
B✝ : Type u_6
inst✝³⁶ : CommRing B✝
inst✝³⁵ : IsDomain B✝
inst✝³⁴ : Field K
L : Type u_7
inst✝³³ : Field L
inst✝³² : Algebra A✝ K
inst✝³¹ : IsFractionRing A✝ K
g : A✝ →+* L
A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst✝³⁰ : CommRing A
inst✝²⁹ : CommRing B
inst✝²⁸ : CommRing C
inst✝²⁷ : CommRing D
inst✝²⁶ : Algebra A B
inst✝²⁵ : Algebra A C
inst✝²⁴ : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst✝²³ : Field FA
inst✝²² : Field FB
inst✝²¹ : Field FC
inst✝²⁰ : Field FD
inst✝¹⁹ : Algebra A FA
inst✝¹⁸ : Algebra B FB
inst✝¹⁷ : Algebra C FC
inst✝¹⁶ : Algebra D FD
inst✝¹⁵ : IsFractionRing A FA
inst✝¹⁴ : IsFractionRing B FB
inst✝¹³ : IsFractionRing C FC
inst✝¹² : IsFractionRing D FD
inst✝¹¹ : Algebra A FB
inst✝¹⁰ : IsScalarTower A B FB
inst✝⁹ : Algebra A FC
inst✝⁸ : IsScalarTower A C FC
inst✝⁷ : Algebra A FD
inst✝⁶ : IsScalarTower A D FD
inst✝⁵ : Algebra FA FB
inst✝⁴ : IsScalarTower A FA FB
inst✝³ : Algebra FA FC
inst✝² : IsScalarTower A FA FC
inst✝¹ : Algebra FA FD
inst✝ : IsScalarTower A FA FD
f : B ≃ₐ[A] C
x y : A
⊢ (ringEquivOfRingEquiv f.toRingEquiv).toFun ((algebraMap A FB) x / (algebraMap A FB) y) =
    (algebraMap A FC) x / (algebraMap A FC) y
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₁ T) ((algebraMap R S₁) r) = (algebraMap S₁ T) ((algebraMap R S₁) s)
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
← IsScalarTower.algebraMap_apply,

Goal state after:
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap R T) r = (algebraMap R T) s
⊢ ∃ c, ↑c * x = ↑c * 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
Rₘ : Type u_4
Sₙ : Type u_5
Rₘ' : Type u_6
Sₙ' : Type u_7
inst✝¹⁹ : CommSemiring Rₘ
inst✝¹⁸ : CommSemiring Sₙ
inst✝¹⁷ : CommSemiring Rₘ'
inst✝¹⁶ : CommSemiring Sₙ'
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : Algebra S Sₙ
inst✝¹³ : Algebra R Rₘ'
inst✝¹² : Algebra S Sₙ'
inst✝¹¹ : Algebra R Sₙ
inst✝¹⁰ : Algebra Rₘ Sₙ
inst✝⁹ : Algebra Rₘ' Sₙ'
inst✝⁸ : Algebra R Sₙ'
N : Submonoid S
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization N Sₙ
inst✝⁵ : IsLocalization M Rₘ'
inst✝⁴ : IsLocalization N Sₙ'
inst✝³ : IsScalarTower R Rₘ Sₙ
inst✝² : IsScalarTower R S Sₙ
inst✝¹ : IsScalarTower R Rₘ' Sₙ'
inst✝ : IsScalarTower R S Sₙ'
x : R
⊢ (algEquiv N Sₙ Sₙ') ((algebraMap Rₘ Sₙ) ((algebraMap R Rₘ) x)) = (algebraMap Rₘ' Sₙ') ((algebraMap R Rₘ') x)

Tactic:
← IsScalarTower.algebraMap_apply,

Goal state after:
R : Type u_1
inst✝²² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝²¹ : CommSemiring S
inst✝²⁰ : Algebra R S
Rₘ : Type u_4
Sₙ : Type u_5
Rₘ' : Type u_6
Sₙ' : Type u_7
inst✝¹⁹ : CommSemiring Rₘ
inst✝¹⁸ : CommSemiring Sₙ
inst✝¹⁷ : CommSemiring Rₘ'
inst✝¹⁶ : CommSemiring Sₙ'
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : Algebra S Sₙ
inst✝¹³ : Algebra R Rₘ'
inst✝¹² : Algebra S Sₙ'
inst✝¹¹ : Algebra R Sₙ
inst✝¹⁰ : Algebra Rₘ Sₙ
inst✝⁹ : Algebra Rₘ' Sₙ'
inst✝⁸ : Algebra R Sₙ'
N : Submonoid S
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization N Sₙ
inst✝⁵ : IsLocalization M Rₘ'
inst✝⁴ : IsLocalization N Sₙ'
inst✝³ : IsScalarTower R Rₘ Sₙ
inst✝² : IsScalarTower R S Sₙ
inst✝¹ : IsScalarTower R Rₘ' Sₙ'
inst✝ : IsScalarTower R S Sₙ'
x : R
⊢ (algEquiv N Sₙ Sₙ') ((algebraMap R Sₙ) x) = (algebraMap Rₘ' Sₙ') ((algebraMap R Rₘ') x)
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
Rₘ : Type u_4
Sₙ : Type u_5
Rₘ' : Type u_6
Sₙ' : Type u_7
inst✝¹⁹ : CommSemiring Rₘ
inst✝¹⁸ : CommSemiring Sₙ
inst✝¹⁷ : CommSemiring Rₘ'
inst✝¹⁶ : CommSemiring Sₙ'
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : Algebra S Sₙ
inst✝¹³ : Algebra R Rₘ'
inst✝¹² : Algebra S Sₙ'
inst✝¹¹ : Algebra R Sₙ
inst✝¹⁰ : Algebra Rₘ Sₙ
inst✝⁹ : Algebra Rₘ' Sₙ'
inst✝⁸ : Algebra R Sₙ'
N : Submonoid S
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization N Sₙ
inst✝⁵ : IsLocalization M Rₘ'
inst✝⁴ : IsLocalization N Sₙ'
inst✝³ : IsScalarTower R Rₘ Sₙ
inst✝² : IsScalarTower R S Sₙ
inst✝¹ : IsScalarTower R Rₘ' Sₙ'
inst✝ : IsScalarTower R S Sₙ'
x : R
⊢ (algEquiv N Sₙ Sₙ') ((algebraMap R Sₙ) x) = (algebraMap Rₘ' Sₙ') ((algebraMap R Rₘ') x)

Tactic:
← IsScalarTower.algebraMap_apply,

Goal state after:
R : Type u_1
inst✝²² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝²¹ : CommSemiring S
inst✝²⁰ : Algebra R S
Rₘ : Type u_4
Sₙ : Type u_5
Rₘ' : Type u_6
Sₙ' : Type u_7
inst✝¹⁹ : CommSemiring Rₘ
inst✝¹⁸ : CommSemiring Sₙ
inst✝¹⁷ : CommSemiring Rₘ'
inst✝¹⁶ : CommSemiring Sₙ'
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : Algebra S Sₙ
inst✝¹³ : Algebra R Rₘ'
inst✝¹² : Algebra S Sₙ'
inst✝¹¹ : Algebra R Sₙ
inst✝¹⁰ : Algebra Rₘ Sₙ
inst✝⁹ : Algebra Rₘ' Sₙ'
inst✝⁸ : Algebra R Sₙ'
N : Submonoid S
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization N Sₙ
inst✝⁵ : IsLocalization M Rₘ'
inst✝⁴ : IsLocalization N Sₙ'
inst✝³ : IsScalarTower R Rₘ Sₙ
inst✝² : IsScalarTower R S Sₙ
inst✝¹ : IsScalarTower R Rₘ' Sₙ'
inst✝ : IsScalarTower R S Sₙ'
x : R
⊢ (algEquiv N Sₙ Sₙ') ((algebraMap R Sₙ) x) = (algebraMap R Sₙ') x
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
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) (mk' Rₘ x y) * (algebraMap S Sₘ) ((algebraMap R S) ↑y) = (algebraMap S Sₘ) ((algebraMap R S) x)

Tactic:
← IsScalarTower.algebraMap_apply,

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) (mk' Rₘ x y) * (algebraMap R Sₘ) ↑y = (algebraMap S Sₘ) ((algebraMap R S) 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 f, I ≠ ⊤ ∧ Surjective ⇑f

Tactic:
obtain ⟨N, hN, ⟨x, hx⟩⟩ := Module.exists_isPrincipal_quotient_of_finite R M

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 : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = R ∙ x
⊢ ∃ I f, I ≠ ⊤ ∧ Surjective ⇑f
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ star {c | ∀ m ∈ s, m * c = c * m} = {c | ∀ m ∈ star s, m * c = c * m}

Tactic:
← commute_iff_eq

Goal state after:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ star {c | ∀ m ∈ s, Commute m c} = {c | ∀ m ∈ star s, Commute m c}
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 0 = {0}

Tactic:
refine Set.Subset.antisymm ?_ (by simp [Algebra.algebraMap_eq_smul_one, mem_iff])
  rw [spectrum, Set.compl_subset_comm]
  intro k hk
  rw [Set.mem_compl_singleton_iff] at hk
  have : IsUnit (Units.mk0 k hk • (1 : A)) := IsUnit.smul (Units.mk0 k hk) isUnit_one
  simpa [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one]

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
⊢ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A B) 1) ⊤) ≤
    Subalgebra.toSubmodule (adjoin A ↑includeRight.range)

Tactic:
Submodule.map_top

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
⊢ Submodule.span A ↑((TensorProduct.mk R A B) 1).range ≤ Subalgebra.toSubmodule (adjoin A ↑includeRight.range)
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ (x * y) • m = x • y • m

Tactic:
by
    refine TensorProduct.induction_on x ?_ ?_ ?_ <;> refine TensorProduct.induction_on y ?_ ?_ ?_
    · simp only [(· • ·), mul_zero, map_zero, LinearMap.zero_apply]
    · intro a b
      simp only [(· • ·), zero_mul, map_zero, LinearMap.zero_apply]
    · intro z w _ _
      simp only [(· • ·), zero_mul, map_zero, LinearMap.zero_apply]
    · intro a b
      simp only [(· • ·), mul_zero, map_zero, LinearMap.zero_apply]
    · intro a₁ b₁ a₂ b₂
      -- Porting note: was one `simp only`, not two
      simp only [(· • ·), Algebra.TensorProduct.tmul_mul_tmul]
      simp only [moduleAux_apply, mul_smul, smul_comm a₁ b₂]
    · intro z w hz hw a b
      -- Porting note: was one `simp only`, but random stuff doesn't work
      simp only [(· • ·)] at hz hw ⊢
      simp only [moduleAux_apply, mul_add, map_add,
        LinearMap.add_apply, moduleAux_apply, hz, hw]
    · intro z w _ _
      simp only [(· • ·), mul_zero, map_zero, LinearMap.zero_apply]
    · intro a b z w hz hw
      simp only [(· • ·)] at hz hw ⊢
      simp only [map_add, add_mul, LinearMap.add_apply, hz, hw]
    · intro u v _ _ z w hz hw
      simp only [(· • ·)] at hz hw ⊢
      simp only [add_mul, map_add, LinearMap.add_apply, hz, hw, add_add_add_comm]

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Ring (κ i)
inst✝ : (i : ι) → Algebra R (κ i)
a : (i : ι) → κ i
⊢ {r | ∀ (i : ι), IsUnit (((algebraMap R ((i : ι) → κ i)) r - a) i)} =
    {x | ∀ (i : ι), IsUnit ((algebraMap R (κ i)) x - a i)}

Tactic:
sub_apply,

Goal state after:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Ring (κ i)
inst✝ : (i : ι) → Algebra R (κ i)
a : (i : ι) → κ i
⊢ {r | ∀ (i : ι), IsUnit ((algebraMap R ((i : ι) → κ i)) r i - a i)} =
    {x | ∀ (i : ι), IsUnit ((algebraMap R (κ i)) x - a i)}
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
F : Type u_6
inst✝¹ : FunLike F (Unitization R A) B
inst✝ : AlgHomClass F S (Unitization R A) B
φ ψ : F
h : ∀ (a : A), φ ↑a = ψ ↑a
h' : ∀ (r : R), φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)
x : Unitization R A
⊢ φ x = ψ x

Tactic:
induction x

Goal state after:
case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
F : Type u_6
inst✝¹ : FunLike F (Unitization R A) B
inst✝ : AlgHomClass F S (Unitization R A) B
φ ψ : F
h : ∀ (a : A), φ ↑a = ψ ↑a
h' : ∀ (r : R), φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)
r✝ : R
a✝ : A
⊢ φ (inl r✝ + ↑a✝) = ψ (inl r✝ + ↑a✝)
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : NonUnitalSemiring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
x y : R
inst✝ : IsCancelAdd R
p : R
⊢ x ≠ y ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + p ↔
    p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + p

Tactic:
simp +contextual [← and_assoc]

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * x * c + 0

Tactic:
rw [add_zero]

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * x * c
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : Rᵐᵒᵖ
⊢ (∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), unop y = unop x + p) ↔
    ∃ x_1, op x_1 ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + op x_1

Tactic:
← (AddSubmonoid.closure _).comap_map_eq_of_injective opAddEquiv.injective

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : Rᵐᵒᵖ
⊢ (∃ p ∈ AddSubmonoid.comap opAddEquiv (AddSubmonoid.map opAddEquiv (AddSubmonoid.closure (range fun s ↦ star s * s))),
      unop y = unop x + p) ↔
    ∃ x_1, op x_1 ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + op x_1
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
ι : Type w
fst✝ : Type v
bs : Basis fst✝ R M
⊢ #((_ : ι) × fst✝) = lift.{v, w} #ι * lift.{w, v} #fst✝

Tactic:
Cardinal.mk_sigma,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
ι : Type w
fst✝ : Type v
bs : Basis fst✝ R M
⊢ (sum fun i ↦ #fst✝) = lift.{v, w} #ι * lift.{w, v} #fst✝
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type u_1
b : Basis ι R M
h : lift.{?u.26, v} (Module.rank R M) < lift.{?u.26, v} ℵ₀
⊢ Nonempty (Fintype ι)

Tactic:
← b.mk_eq_rank,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type u_1
b : Basis ι R M
h : lift.{v, u_1} #ι < lift.{u_1, v} ℵ₀
⊢ Nonempty (Fintype ι)