mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'

Tactic:
by
  by_cases h : j' = j
  · rw [h, updateCol_self, if_pos rfl]
  · rw [updateCol_ne h, if_neg h]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
⊢ span R {a, ψ ⟨y, ⋯⟩} = Ideal.span {generator (ϕ.submoduleImage N)}

pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
⊢ generator (ϕ.submoduleImage N) ∈ span R {a, ψ ⟨y, ⋯⟩}

Tactic:
Ideal.span,

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
⊢ span R {a, ψ ⟨y, ⋯⟩} = R ∙ generator (ϕ.submoduleImage N)

R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
⊢ generator (ϕ.submoduleImage N) ∈ span R {a, ψ ⟨y, ⋯⟩}
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
hrS : 1 ∈ ↑S
hrirred : 1 ∉ {p | Irreducible p}
⊢ False

Tactic:
simpa using hSmax (y := S \ {1}) (by simpa) Finset.sdiff_subset hrS

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m : M → ℕ
hm : ∏ a ∈ S, a ^ m a = a
n : M → ℕ
hn : ∏ a ∈ S, a ^ n a = b
⊢ ∏ a ∈ S, a ^ m a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s

Tactic:
Finset.sdiff_singleton_eq_erase,

Goal state after:
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m : M → ℕ
hm : ∏ a ∈ S, a ^ m a = a
n : M → ℕ
hn : ∏ a ∈ S, a ^ n a = b
⊢ ∏ a ∈ S, a ^ m a = r ^ m r * ∏ s ∈ S.erase r, s ^ m s
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hn : ∏ a ∈ S, a ^ n a = b
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
⊢ ∏ a ∈ S, a ^ n a = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s

Tactic:
Finset.sdiff_singleton_eq_erase,

Goal state after:
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hn : ∏ a ∈ S, a ^ n a = b
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
⊢ ∏ a ∈ S, a ^ n a = r ^ n r * ∏ s ∈ S.erase r, s ^ n s
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c✝ : ι → R
hc✝ : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c✝ i
val✝ : Fintype ι
y' : O := ∑ i, c✝ i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c✝ i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
c : R
x : O
xM : x ∈ M
hx' : ϕ ⟨x, xM⟩ = 0
xM' : M.subtype ⟨x, xM⟩ ∈ M'
hc : c • y' + M.subtype ⟨x, xM⟩ = 0
hc' : c • ⟨y', y'M⟩ + ⟨x, xM⟩ = 0
⊢ c = 0

Tactic:
simpa only [map_add, map_zero, map_smul, smul_eq_mul, add_zero, mul_eq_zero, ϕy'_ne_zero, hx',
      or_false] using congr_arg ϕ hc'

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ ⨆ i, Submodule.map M.vecMulLinear (Submodule.map (LinearMap.single R (fun i ↦ R) i) (Ideal.span {1})) =
    span R (Set.range M.row)

Tactic:
Ideal.span,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ ⨆ i, Submodule.map M.vecMulLinear (Submodule.map (LinearMap.single R (fun i ↦ R) i) (R ∙ 1)) =
    span R (Set.range M.row)
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✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
x✝ : OreLocalization S X
⊢ 0 • x✝ = 0

Tactic:
by with_unfolding_all rfl

Goal state after:
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✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
x✝¹ : ℕ
x✝ : OreLocalization S X
⊢ (x✝¹ + 1) • x✝ = x✝¹ • x✝ + x✝

Tactic:
by with_unfolding_all rfl

Goal state after:
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
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a b ↦ b • snf.bM.repr ↑(snf.bN a)) (snf.f i) = (snf.a i • c.sum fun a b ↦ b • snf.bN.repr (snf.bN a)) i

Tactic:
repr_self,

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
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a b ↦ b • snf.bM.repr ↑(snf.bN a)) (snf.f i) = (snf.a i • c.sum fun a b ↦ b • Finsupp.single a 1) i
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
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a b ↦ b • snf.a a • snf.bM.repr (snf.bM (snf.f a))) (snf.f i) = snf.a i • c i

Tactic:
repr_self,

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
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a b ↦ b • snf.a a • Finsupp.single (snf.f a) 1) (snf.f i) = snf.a i • c i
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
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
⊢ IsFractionRing.inv A 0 = 0

Tactic:
rw [IsFractionRing.inv]; exact dif_pos rfl

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 S₁ T) (x * (algebraMap R S₁) ↑d) = (algebraMap S₁ T) (y * (algebraMap R S₁) ↑d)
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
hr,

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) (y * (algebraMap R S₁) ↑d)
⊢ ∃ c, ↑c * x = ↑c * y
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
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 : R
hmc : c ∈ ↑M₁
hc : (algebraMap R S₂) (c * r) = (algebraMap R S₂) (c * s)
a : ↥M₂
ha : ↑a * (c * r) = ↑a * (c * s)
⊢ ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * (x * (algebraMap R S₁) ↑d) = ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * y * (algebraMap R S₁) ↑d

Tactic:
hr,

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
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 : R
hmc : c ∈ ↑M₁
hc : (algebraMap R S₂) (c * r) = (algebraMap R S₂) (c * s)
a : ↥M₂
ha : ↑a * (c * r) = ↑a * (c * s)
⊢ ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * (algebraMap R S₁) r = ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * y * (algebraMap R S₁) ↑d
Module: Mathlib.RingTheory.Localization.Defs

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
inst✝¹ : IsLocalization M S
T : Type u_4
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
x y : R
hz : f ((algebraMap R S) x - (algebraMap R S) y) = 0
⊢ (algebraMap R S) x = (algebraMap R S) y

Tactic:
← map_sub

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_4
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
x y : R
hz : f ((algebraMap R S) (x - y)) = 0
⊢ (algebraMap R S) x = (algebraMap R S) y
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : Surjective ⇑(algebraMap R A)
a : A
⊢ 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1

Tactic:
obtain ⟨r, rfl⟩ := h a

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : Surjective ⇑(algebraMap R A)
r : R
⊢ 1 ⊗ₜ[R] (algebraMap R A) r = (algebraMap R A) r ⊗ₜ[R] 1
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
T' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.Finite
g : T →ₐ[R] T'
Hg : g.Finite
⊢ (Algebra.TensorProduct.map f g).toRingHom =
    (Algebra.TensorProduct.map f (AlgHom.id R T')).comp
      ((Algebra.TensorProduct.comm R T' S).toRingEquiv.toRingHom.comp
        ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp (Algebra.TensorProduct.comm R S T).toRingEquiv.toRingHom))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, ← AlgEquiv.toAlgHom_toRingHom, ← AlgHom.comp_toRingHom]

Goal state after:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
T' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.Finite
g : T →ₐ[R] T'
Hg : g.Finite
⊢ ↑(Algebra.TensorProduct.map f g) =
    ↑((Algebra.TensorProduct.map f (AlgHom.id R T')).comp
        ((↑(Algebra.TensorProduct.comm R T' S)).comp
          ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp ↑(Algebra.TensorProduct.comm R S T))))
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
x : S
y : M
⊢ x ⊗ₜ[R] y ∈ ↑((mk R S M) 1).range

Tactic:
obtain ⟨x, rfl⟩ := h x

Goal state after:
R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
y : M
x : R
⊢ (algebraMap R S) x ⊗ₜ[R] y ∈ ↑((mk R S M) 1).range
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case h.right
R : Type u_1
inst✝ : Ring R
x : R
hx : IsUnit (1 + x)
this : ↑hx.unit⁻¹ * (1 + x) - 1 = 1 - 1
⊢ x + (↑hx.unit⁻¹ - 1) + (↑hx.unit⁻¹ - 1) * x = 0

Tactic:
rw [← sub_add_cancel (↑hx.unit⁻¹ : R) 1, sub_self] at this
    convert this
    noncomm_ring

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

Goal state before:
pp: case h.left
R : Type u_1
inst✝ : Ring R
x : R
hx : IsUnit (1 + x)
this : (1 + x) * ↑hx.unit⁻¹ - 1 = 1 - 1
⊢ ↑hx.unit⁻¹ - 1 + x + x * (↑hx.unit⁻¹ - 1) = 0

Tactic:
rw [← sub_add_cancel (↑hx.unit⁻¹ : R) 1, sub_self] at this
    convert this
    noncomm_ring

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

Goal state before:
pp: case refine_1
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 : R
⊢ 0 ≤ star c * (fun s ↦ star s * s) x * c

Tactic:
convert! star_mul_self_nonneg (x * c) using 1

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 : R
⊢ star c * (fun s ↦ star s * s) x * c = star (x * c) * (x * c)
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 c p : R
hp : 0 ≤ p
⊢ star c * (a + p) * c = star c * a * c + star c * p * c

Tactic:
simp only [add_mul, mul_add]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module R A
inst✝⁵ : StarModule R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : IsDomain R
inst✝¹ : IsCancelAdd A
inst✝ : Module.IsTorsionFree R A
r : R
hr : r ≠ 0 ∧ r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : a < b
⊢ r • a < r • b

Tactic:
StarOrderedRing.lt_iff

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module R A
inst✝⁵ : StarModule R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : IsDomain R
inst✝¹ : IsCancelAdd A
inst✝ : Module.IsTorsionFree R A
r : R
hr : r ≠ 0 ∧ r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ b = a + p
⊢ ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ r • b = r • a + p
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁵ : Semiring R
inst✝¹⁴ : PartialOrder R
inst✝¹³ : StarRing R
inst✝¹² : StarOrderedRing R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarOrderedRing A
inst✝⁷ : Module R A
inst✝⁶ : StarModule R A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsDomain R
inst✝² : IsCancelAdd A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : IsCancelAdd R
a : A
ha : a ≠ 0 ∧ a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : r < s
⊢ r • a < s • a

Tactic:
StarOrderedRing.lt_iff

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹⁵ : Semiring R
inst✝¹⁴ : PartialOrder R
inst✝¹³ : StarRing R
inst✝¹² : StarOrderedRing R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarOrderedRing A
inst✝⁷ : Module R A
inst✝⁶ : StarModule R A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsDomain R
inst✝² : IsCancelAdd A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : IsCancelAdd R
a : A
ha : a ≠ 0 ∧ a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ s = r + p
⊢ ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ s • a = r • a + p
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : NonUnitalSemiring A
inst✝³ : StarRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
z : A
⊢ z ∈ centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

Tactic:
change (∀ g ∈ s ∪ star s, g * z = z * g) ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g
  simp only [Set.mem_union, or_imp, forall_and, and_congr_right_iff]
  exact fun _ =>
    ⟨fun hz a ha => hz _ (Set.star_mem_star.mpr ha), fun hz a ha => star_star a ▸ hz _ ha⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_2
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n
⊢ f ((Basis.mk H₁ ⋯) i) = (Finsupp.single i 1) ⟨w, ⋯⟩

Tactic:
rcases i with ⟨x, rfl | ⟨x, hx, rfl⟩⟩

Goal state after:
case refine_2.inl
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
x : V
hw : f x = 1
n : Set V := insert x s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
⊢ f ((Basis.mk H₁ ⋯) ⟨x, ⋯⟩) = (Finsupp.single ⟨x, ⋯⟩ 1) ⟨x, ⋯⟩

case refine_2.inr
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
x : ↥f.ker
hx : x ∈ Set.range ⇑b₁
⊢ f ((Basis.mk H₁ ⋯) ⟨f.ker.subtype x, ⋯⟩) = (Finsupp.single ⟨f.ker.subtype x, ⋯⟩ 1) ⟨w, ⋯⟩