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

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : DistribMulAction R X
x y : OreLocalization S X
⊢ x + y = y + x

Tactic:
induction x with

Goal state after:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : DistribMulAction R X
y : OreLocalization S X
r : X
s : ↥S
⊢ r /ₒ s + y = y + r /ₒ s
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
x : OreLocalization S X
⊢ -x + x = 0

Tactic:
induction x with

Goal state after:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
r : X
s : ↥S
⊢ -(r /ₒ s) + r /ₒ s = 0
Module: Mathlib.GroupTheory.MonoidLocalization.Divisibility

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m₁ m₂ : M
x✝ : f m₁ ∣ f m₂
n : N
eq : f m₂ = f m₁ * n
m : M
s : ↥S
hn : f (m₂ * ↑(m, s).2) = f (m₁ * (m, s).1)
s' : ↥S
hs' : ↑s' * (m₂ * ↑(m, s).2) = ↑s' * (m₁ * (m, s).1)
⊢ ↑s' * ↑s * m₂ = m₁ * (↑s' * m)

Tactic:
mul_left_comm,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m₁ m₂ : M
x✝ : f m₁ ∣ f m₂
n : N
eq : f m₂ = f m₁ * n
m : M
s : ↥S
hn : f (m₂ * ↑(m, s).2) = f (m₁ * (m, s).1)
s' : ↥S
hs' : ↑s' * (m₂ * ↑(m, s).2) = ↑s' * (m₁ * (m, s).1)
⊢ ↑s' * ↑s * m₂ = ↑s' * (m₁ * m)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
x : OreLocalization S X
⊢ 0 • x = 0

Tactic:
induction x with

Goal state after:
case c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r : X
s : ↥S
⊢ 0 • (r /ₒ s) = 0
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
y z : OreLocalization S R
x : OreLocalization S X
⊢ (y + z) • x = y • x + z • x

Tactic:
induction x with

Goal state after:
case c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
y z : OreLocalization S R
r₁ : X
s₁ : ↥S
⊢ (y + z) • (r₁ /ₒ s₁) = y • (r₁ /ₒ s₁) + z • (r₁ /ₒ s₁)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
y z : OreLocalization S R
r₁ : X
s₁ : ↥S
⊢ (y + z) • (r₁ /ₒ s₁) = y • (r₁ /ₒ s₁) + z • (r₁ /ₒ s₁)

Tactic:
induction y with | _ r₂ s₂
   =>  _ 

Goal state after:
case c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
z : OreLocalization S R
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (r₂ /ₒ s₂ + z) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + z • (r₁ /ₒ s₁)
Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R⁰ R
h : x ≠ 0
⊢ x * x⁻¹ = 1

Tactic:
induction x with

Goal state after:
case c
R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
⊢ r /ₒ s * (r /ₒ s)⁻¹ = 1
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₂
⊢ ((toLin v₁ v₂) M) (((toLin v₂ v₁) M') x) = x

Tactic:
by
      rw [← Matrix.toLin_mul_apply, hMM', Matrix.toLin_one, id_apply]

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
x y : OreLocalization S R
⊢ (universalMulHom (↑f) fS ⋯) (x + y) = (universalMulHom (↑f) fS ⋯) x + (universalMulHom (↑f) fS ⋯) y

Tactic:
induction x with

Goal state after:
case c
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
y : OreLocalization S R
r₁ : R
s₁ : ↥S
⊢ (universalMulHom (↑f) fS ⋯) (r₁ /ₒ s₁ + y) = (universalMulHom (↑f) fS ⋯) (r₁ /ₒ s₁) + (universalMulHom (↑f) fS ⋯) y
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * (f r₃ * f r₂) = ↑(fS s₂)⁻¹ * f r₂

Tactic:
rw [← mul_assoc]

Goal state after:
case c.c.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * f r₃ * f r₂ = ↑(fS s₂)⁻¹ * f r₂
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
⊢ ⇑(snf.bM.repr ↑m) ∘ ⇑snf.f = snf.a • ⇑(snf.bN.repr m)

Tactic:
ext i

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
i : Fin n
⊢ (⇑(snf.bM.repr ↑m) ∘ ⇑snf.f) i = (snf.a • ⇑(snf.bN.repr m)) i
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁹ : CommSemiring R✝
M✝ N : Submonoid R✝
S✝ : Type u_2
inst✝¹⁸ : CommSemiring S✝
inst✝¹⁷ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁶ : CommSemiring P✝
inst✝¹⁵ : IsLocalization M✝ S✝
g : R✝ →+* P✝
hg : ∀ (y : ↥M✝), IsUnit (g ↑y)
A : Type u_4
inst✝¹⁴ : CommSemiring A
R : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : Algebra A R
M : Submonoid R
S : Type u_6
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra A S
inst✝⁹ : Algebra R S
inst✝⁸ : IsScalarTower A R S
inst✝⁷ : IsLocalization M S
P : Type u_7
inst✝⁶ : CommSemiring P
inst✝⁵ : Algebra A P
T : Submonoid P
Q : Type u_8
inst✝⁴ : CommSemiring Q
inst✝³ : Algebra A Q
inst✝² : Algebra P Q
inst✝¹ : IsScalarTower A P Q
inst✝ : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x✝ : A
⊢ (ringEquivOfRingEquiv S Q h.toRingEquiv H).toFun ((algebraMap A S) x✝) = (algebraMap A Q) x✝

Tactic:
by dsimp; rw [IsScalarTower.algebraMap_apply A R S, map_eq,
    RingHom.coe_coe, AlgEquiv.commutes, IsScalarTower.algebraMap_apply A P Q]

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : y * (algebraMap R S) ↑(x, s).2 = (algebraMap R S) (x, s).1
u : Rˣ
hu : ↑u = ↑s
⊢ (Algebra.ofId R S) (x * u.inv) = y

Tactic:
dsimp [Algebra.ofId, RingHom.toFun_eq_coe, AlgHom.coe_mks]

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : y * (algebraMap R S) ↑(x, s).2 = (algebraMap R S) (x, s).1
u : Rˣ
hu : ↑u = ↑s
⊢ (algebraMap R S) (x * ↑u⁻¹) = y
Module: Mathlib.RingTheory.Localization.Defs

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
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
⊢ Submonoid.map h.symm.toMonoidHom T = M

Tactic:
rw [← M.map_id, ← H, Submonoid.map_map]

Goal state after:
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
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
⊢ Submonoid.map (h.symm.toMonoidHom.comp h.toMonoidHom) M = Submonoid.map (MonoidHom.id R) M
Module: Mathlib.RingTheory.Localization.Defs

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
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
H' : Submonoid.map h.symm.toMonoidHom T = M
x : S
⊢ (map S ↑h.symm ⋯) ((map Q ↑h ⋯) x) = x

Tactic:
by
      rw [map_map, map_unique _ (RingHom.id _), RingHom.id_apply]
      simp

Goal state after:
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 : R
ha : a ∈ ↑M₂
⊢ IsUnit ((algebraMap R T) a)

Tactic:
IsScalarTower.algebraMap_apply R S₂ T

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 : R
ha : a ∈ ↑M₂
⊢ IsUnit ((algebraMap S₂ T) ((algebraMap R S₂) a))
Module: Mathlib.RingTheory.Localization.Defs

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
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
H' : Submonoid.map h.symm.toMonoidHom T = M
x : Q
⊢ (map Q ↑h ⋯) ((map S ↑h.symm ⋯) x) = x

Tactic:
by
      rw [map_map, map_unique _ (RingHom.id _), RingHom.id_apply]
      simp

Goal state after:
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 R T) n = (algebraMap S₁ T) ((algebraMap R S₁) z) * (algebraMap S₁ T) ↑hunit.unit⁻¹

Tactic:
IsScalarTower.algebraMap_apply R S₂ T

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 S₂ T) ((algebraMap R S₂) n) =
    (algebraMap S₁ T) ((algebraMap R S₁) z) * (algebraMap S₁ T) ↑hunit.unit⁻¹
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
d : ↥M
⊢ mk a b + mk c d = mk (↑b * c + ↑d * a) (b * d)

Tactic:
by
  rw [add_comm (b * c) (d * a), mul_comm b d]
  exact OreLocalization.oreDiv_add_oreDiv

Goal state after:
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 R T) r = (algebraMap R T) s
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
IsScalarTower.algebraMap_apply R S₂ T

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 S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
⊢ ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: case add
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
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : ↥J₂ ⊗[R] M
⊢ (rTensor M J₁.subtype) y₁ + (rTensor M J₂.subtype) y₂ =
    (rTensor M (J₁ ⊔ J₂).subtype) ((rTensor M (inclusion ⋯)) y₁ + (rTensor M (inclusion ⋯)) y₂)

Tactic:
rw [map_add, ← rTensor_comp_apply, ← rTensor_comp_apply]

Goal state after:
case add
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
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : ↥J₂ ⊗[R] M
⊢ (rTensor M J₁.subtype) y₁ + (rTensor M J₂.subtype) y₂ =
    (rTensor M ((J₁ ⊔ J₂).subtype ∘ₗ inclusion ⋯)) y₁ + (rTensor M ((J₁ ⊔ J₂).subtype ∘ₗ inclusion ⋯)) 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
x : N ⊗[R] M
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, x = (rTensor M J.subtype) y

Tactic:
induction x with

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
x : TensorProduct R A M
⊢ x ∈ Submodule.span A ↑(Finset.image (⇑((TensorProduct.mk R A M) 1)) s)

Tactic:
induction x with

Goal state after:
Module: Mathlib.Algebra.Algebra.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
b : β
⊢ Sort ?u.18

Tactic:
letI := Equiv.semiring e

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
b : β
this : Semiring α := e.semiring
⊢ Sort ?u.18
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : InvolutiveStar α
⊢ star '' s = star ⁻¹' s

Tactic:
rw [image_eq_preimage_of_inverse] <;> intro

Goal state after:
case h₁
α : Type u_1
s : Set α
inst✝ : InvolutiveStar α
x✝ : α
⊢ x✝⋆⋆ = x✝

case h₂
α : Type u_1
s : Set α
inst✝ : InvolutiveStar α
x✝ : α
⊢ x✝⋆⋆ = x✝
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case tmul
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : IsScalarTower S A A
inst✝ : SMulCommClass R S A
r : S
x : A ⊗[R] B
a : A
b : B
⊢ r • x * a ⊗ₜ[R] b = r • (x * a ⊗ₜ[R] b)

Tactic:
induction x with

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

Goal state before:
pp: case tmul
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass S A A
inst✝ : SMulCommClass R S A
r : S
x : A ⊗[R] B
a : A
b : B
⊢ r • (x * a ⊗ₜ[R] b) = x * r • a ⊗ₜ[R] b

Tactic:
induction x with

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : CommSemiring S
inst✝ : Algebra S A
r : R
⊢ (↑((AlgebraTensorModule.mk R R A B) 1).toAddMonoidHom).toFun ((algebraMap R B) r) = (algebraMap R (A ⊗[R] B)) r

Tactic:
simp [algebraMap_eq_smul_one', smul_tmul]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

Tactic:
by_cases h : s ∈ spectrum R a
  · rw [mem_iff] at h
    simp only [resolvent, Algebra.algebraMap_eq_smul_one] at *
    rw [smul_assoc, ← smul_sub]
    have h' : ¬IsUnit (r⁻¹ • (s • (1 : A) - a)) := fun hu =>
      h (by simpa only [smul_inv_smul] using IsUnit.smul r hu)
    simp only [Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ h', smul_zero]
  · simp only [resolvent]
    have h' : IsUnit (r • algebraMap R A (r⁻¹ • s) - a) := by
      simpa [Algebra.algebraMap_eq_smul_one, smul_assoc] using notMem_iff.mp h
    rw [← h'.val_subInvSMul, ← (notMem_iff.mp h).unit_spec, Ring.inverse_unit, Ring.inverse_unit,
      h'.val_inv_subInvSMul]
    simp only [Algebra.algebraMap_eq_smul_one, smul_assoc, smul_inv_smul]

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✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
C : Type u_3
inst✝ : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp includeRight.toRingHom = g.comp includeRight.toRingHom
x : A ⊗[R] B
⊢ f x = g x

Tactic:
induction x with

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A ⊗[R] B
⊢ x ∈ Subring.closure (Set.range ⇑includeLeft ∪ Set.range ⇑includeRight)

Tactic:
induction x with

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

Goal state before:
pp: R : Type u_1
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring B
inst✝² : Algebra R B
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : B
⊢ LinearMap.baseChange A ((lmul R B) f) = (lmul A (A ⊗[R] B)) (1 ⊗ₜ[R] f)

Tactic:
ext i

Goal state after:
R : Type u_1
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring B
inst✝² : Algebra R B
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f i : B
⊢ ((AlgebraTensorModule.curry (LinearMap.baseChange A ((lmul R B) f))) 1) i =
    ((AlgebraTensorModule.curry ((lmul A (A ⊗[R] B)) (1 ⊗ₜ[R] f))) 1) i
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : (PreQuasiregular A)ˣ
⊢ (1 + ↑(PreQuasiregular.equiv.symm ↑x⁻¹)) * (1 + ↑(PreQuasiregular.equiv.symm ↑x)) = 1

Tactic:
convert congr((1 + $(add_inv_add_mul_eq_zero x) : Unitization R A))
          · simp only [mul_one, PreQuasiregular.equiv_symm_apply, one_mul, mul_add,
              add_mul, inr_add, inr_mul]
            abel
          · simp only [inr_zero, add_zero]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Algebra R S
a : A
f : S → R
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ ⇑(algebraMap R S) '' quasispectrum R a = quasispectrum S a

Tactic:
refine Set.eq_of_subset_of_subset ?_ fun s hs => ⟨f s, ?_⟩
  · simpa only [quasispectrum.preimage_algebraMap] using
      (quasispectrum S a).image_preimage_subset (algebraMap R S)
  exact ⟨quasispectrum.of_algebraMap_mem S ((h.rightInvOn hs).symm ▸ hs), h.rightInvOn hs⟩

Goal state after: