mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case h₂
R : Type u_2
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
I J : Ideal S
e : I ≤ J
h₁ : ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x
h₂ : ∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x
x : S
h₃ : IsUnit ((Ideal.Quotient.mk J) x)
⊢ IsUnit x

Tactic:
apply h₁

Goal state after:
case h₂
R : Type u_2
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
I J : Ideal S
e : I ≤ J
h₁ : ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x
h₂ : ∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x
x : S
h₃ : IsUnit ((Ideal.Quotient.mk J) x)
⊢ IsUnit ((Ideal.Quotient.mk I) x)
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsUnit ((mk (map (mk (I ^ n)) I)) ((mk (I ^ n)) x)) ↔ IsUnit ((mk I) x)

Tactic:
rw [← isUnit_map_iff (DoubleQuot.quotQuotEquivQuotOfLE (Ideal.pow_le_self hn))]
    rfl

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

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
J : Ideal S
x : S
hJ : x ∈ J
r : R
s : ↥M
hx : mk' S r s = x
⊢ x ∈ Ideal.map (algebraMap R S) (Ideal.under R J)

Tactic:
← hx

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
J : Ideal S
x : S
r : R
s : ↥M
hJ : mk' S r s ∈ J
hx : mk' S r s = x
⊢ mk' S r s ∈ Ideal.map (algebraMap R S) (Ideal.under R J)
Module: Mathlib.RingTheory.Localization.Ideal

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
I : Ideal R
hI : I.IsPrimary
hM : Disjoint ↑M ↑I
key : Disjoint ↑M ↑I.radical
a : R
b : ↥I
s : ↥M
h : (algebraMap R S) (↑s * a) = (algebraMap R S) ↑b
c : ↥M
hc : ↑c * (↑s * a) = ↑c * ↑b
⊢ ↑c * (↑s * a) ∈ I

Tactic:
hc

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
I : Ideal R
hI : I.IsPrimary
hM : Disjoint ↑M ↑I
key : Disjoint ↑M ↑I.radical
a : R
b : ↥I
s : ↥M
h : (algebraMap R S) (↑s * a) = (algebraMap R S) ↑b
c : ↥M
hc : ↑c * (↑s * a) = ↑c * ↑b
⊢ ↑c * ↑b ∈ I
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ (algebraMap R S) ↑c * (algebraMap R S) z' = ↑z * (algebraMap R S) ↑(c * s)

Tactic:
← eq₂,

Goal state after:
case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ (algebraMap R S) ↑c * (↑z * (algebraMap R S) ↑s) = ↑z * (algebraMap R S) ↑(c * s)
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

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
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
⊢ (algebraMap R S) x * (algebraMap R S) z' = (algebraMap R S) y * (algebraMap R S) z'

Tactic:
← eq₂,

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
⊢ (algebraMap R S) x * (↑z * (algebraMap R S) ↑s) = (algebraMap R S) y * (↑z * (algebraMap R S) ↑s)
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case h
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
left✝ : x ∈ ↑(nonZeroDivisorsLeft S)
hx : x ∈ ↑(nonZeroDivisorsRight S)
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
z : R
hz : z * (y, s).1 = 0
⊢ (algebraMap R S) (z * (y, s).1) = 0 * (algebraMap R S) ↑s

Tactic:
hz,

Goal state after:
case h
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
left✝ : x ∈ ↑(nonZeroDivisorsLeft S)
hx : x ∈ ↑(nonZeroDivisorsRight S)
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
z : R
hz : z * (y, s).1 = 0
⊢ (algebraMap R S) 0 = 0 * (algebraMap R S) ↑s
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : 0 = (algebraMap R S) 1
⊢ False

Tactic:
← (algebraMap R S).map_zero

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : (algebraMap R S) 0 = (algebraMap R S) 1
⊢ False
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
I : Ideal R
⊢ Submodule.map (↑(TensorProduct.lid R M)) (map (Submodule.subtype I) LinearMap.id).range = I • ⊤

Tactic:
rw [← LinearMap.range_comp, ← (Submodule.topEquiv.lTensor I).range_comp, Submodule.smul_eq_map₂,
      map₂_eq_range_lift_comp_mapIncl]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
I : Ideal R
⊢ ((↑(TensorProduct.lid R M) ∘ₗ map (Submodule.subtype I) LinearMap.id) ∘ₗ
        ↑(LinearEquiv.lTensor (↥I) Submodule.topEquiv)).range =
    (lift (LinearMap.lsmul R M) ∘ₗ mapIncl I ⊤).range
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ (sx • x) • sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
smul_eq_mul

Goal state after:
case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ sx • x * sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
p : Ideal R
inst✝⁵ : p.IsPrime
Rₚ : Type u_4
inst✝⁴ : CommSemiring Rₚ
inst✝³ : Algebra R Rₚ
inst✝² : IsLocalization.AtPrime Rₚ p
inst✝¹ : IsLocalRing Rₚ
inst✝ : p.IsMaximal
n : ℕ
⊢ under R (maximalIdeal Rₚ ^ n) = p ^ n

Tactic:
by
  ext
  rw [mem_comap, ← map_eq_maximalIdeal p Rₚ, ← Ideal.map_pow,
    algebraMap_mem_map_algebraMap_iff p.primeCompl Rₚ]
  refine ⟨fun ⟨m, hm, h⟩ ↦ ?_, fun h ↦ ⟨1, by simp, by simp [h]⟩⟩
  exact (IsMaximal.mul_mem_pow _ h).resolve_left (mem_primeCompl_iff.mp hm)

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

Goal state before:
pp: case refine_1
R✝ : Type u_1
inst✝¹⁸ : CommSemiring R✝
S✝ : Type u_2
inst✝¹⁷ : CommSemiring S✝
inst✝¹⁶ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁵ : CommSemiring P✝
p✝ : Ideal R✝
inst✝¹⁴ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝¹³ : CommSemiring Rₚ✝
inst✝¹² : Algebra R✝ Rₚ✝
inst✝¹¹ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁰ : IsLocalRing Rₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
⊢ p = under R (RingHom.ker (algebraMap Rₚ (Rₚ ⧸ maximalIdeal Rₚ)))

Tactic:
Ideal.Quotient.algebraMap_eq,

Goal state after:
case refine_1
R✝ : Type u_1
inst✝¹⁸ : CommSemiring R✝
S✝ : Type u_2
inst✝¹⁷ : CommSemiring S✝
inst✝¹⁶ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁵ : CommSemiring P✝
p✝ : Ideal R✝
inst✝¹⁴ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝¹³ : CommSemiring Rₚ✝
inst✝¹² : Algebra R✝ Rₚ✝
inst✝¹¹ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁰ : IsLocalRing Rₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
⊢ p = under R (RingHom.ker (Ideal.Quotient.mk (maximalIdeal Rₚ)))
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp
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 : S
a : Set R
y : R
hy : y ∈ ↑(Ideal.span a)
z : ↥M
hz : x = mk' S 1 z • (Algebra.linearMap R S) y
⊢ x = mk' S y z

Tactic:
hz,

Goal state after:
case mp
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 : S
a : Set R
y : R
hy : y ∈ ↑(Ideal.span a)
z : ↥M
hz : x = mk' S 1 z • (Algebra.linearMap R S) y
⊢ mk' S 1 z • (Algebra.linearMap R S) y = mk' S y z
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mpr
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 : S
a : Set R
y : R
hy : y ∈ Ideal.span a
z : ↥M
hz : x = mk' S y z
⊢ x = mk' S 1 z • (algebraMap R S) y

Tactic:
hz,

Goal state after:
case mpr
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 : S
a : Set R
y : R
hy : y ∈ Ideal.span a
z : ↥M
hz : x = mk' S y z
⊢ mk' S y z = mk' S 1 z • (algebraMap R S) y
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
y : ↥pS
s c : ↥(algebraMapSubmonoid S p.primeCompl)
hc : ↑c * (x * ↑(y, s).2) = ↑c * ↑(y, s).1
α : R
hα : α ∈ ↑p.primeCompl
e : (algebraMap R S) α = ↑(c * s)
⊢ ↑c * (x * ↑s) ∈ pS

Tactic:
hc

Goal state after:
S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
y : ↥pS
s c : ↥(algebraMapSubmonoid S p.primeCompl)
hc : ↑c * (x * ↑(y, s).2) = ↑c * ↑(y, s).1
α : R
hα : α ∈ ↑p.primeCompl
e : (algebraMap R S) α = ↑(c * s)
⊢ ↑c * ↑(y, s).1 ∈ pS
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case refine_1
R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Type u_2
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : Algebra R✝ S✝
P✝ : Type u_3
inst✝²⁴ : CommSemiring P✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
Ideal.Quotient.algebraMap_eq,

Goal state after:
case refine_1
R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Type u_2
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : Algebra R✝ S✝
P✝ : Type u_3
inst✝²⁴ : CommSemiring P✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case h
R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Type u_2
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : Algebra R✝ S✝
P✝ : Type u_3
inst✝²⁴ : CommSemiring P✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S) α = ↑s
β γ : R
hγ : γ ∈ p
hβ : α * β = 1 + γ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
Ideal.Quotient.algebraMap_eq,

Goal state after:
case h
R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Type u_2
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : Algebra R✝ S✝
P✝ : Type u_3
inst✝²⁴ : CommSemiring P✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S) α = ↑s
β γ : R
hγ : γ ∈ p
hβ : α * β = 1 + γ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)

Tactic:
apply le_antisymm <;>
    rw [Module.rank_def, lift_iSup bddAbove_of_small] <;>
    apply ciSup_le'

Goal state after:
case inr.a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ ∀ (i : { s // LinearIndepOn R id s }), Cardinal.lift.{uM, uN} #↑↑i ≤ Cardinal.lift.{uN, uM} (Module.rank R M)

case a
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ ∀ (i : { s // LinearIndepOn R id s }), Cardinal.lift.{uN, uM} #↑↑i ≤ Cardinal.lift.{uM, uN} (Module.rank R N)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ (1 * T n).degree = ↑n

Tactic:
← map_one C

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ (C 1 * T n).degree = ↑n
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case cons
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
head✝ : TransvectionStruct n R
tail✝ : List (TransvectionStruct n R)
IH : (List.map toMatrix tail✝).prod.det = 1
⊢ (List.map toMatrix (head✝ :: tail✝)).prod.det = 1

Tactic:
simp [IH]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
n : ℤ
r : R
⊢ smeval (AddMonoidAlgebra.single n r) x = r • ↑(x ^ n)

Tactic:
simp [smeval, -single_eq_C_mul_T]

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

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝² : Fintype n
ι : Type u_8
inst✝¹ : Unique ι
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ ∀ x ∈ Finset.univ, (replicateCol ι a * replicateRow ι b).diag x = a x * b x

Tactic:
simp [mul_apply]

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

Goal state before:
pp: case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
⊢ IsRightRegular A

Tactic:
· intro B C (h : B * A = C * A)
    refine hA.matrix ?_
    simp only
    rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ←
      mul_adjugate, ← Matrix.mul_assoc, ← Matrix.mul_assoc, h]

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

Goal state before:
pp: m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ LinearIndependent K Aᵀ.col ↔ IsUnit A

Tactic:
← mulVec_injective_iff,

Goal state after:
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ Function.Injective Aᵀ.mulVec ↔ IsUnit A
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
⊢ (M⁻¹.toBlock (fun i ↦ k ≤ b i) fun i ↦ b i < k) = 0

Tactic:
have h_zero : M.toBlock q p = 0 := by
    ext i j
    simpa using hM (lt_of_lt_of_le j.2 <| le_of_not_gt i.2)

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
⊢ (M⁻¹.toBlock (fun i ↦ k ≤ b i) fun i ↦ b i < k) = 0