mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case some
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : ToType ((wideSpan B X f).obj (some j))
⊢ (∃ y_1, (hom (head f)) y_1 = (hom (colimit.ι (wideSpan B X f) (some j))) y) ∨
    ∃ i y_1, (hom (ι f i)) y_1 = (hom (colimit.ι (wideSpan B X f) (some j))) y

Tactic:
· right
    use j, y
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: ⊢ ∀ {W X Y Z : WalkingReflexivePair} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
intro _ _ _ _ f g h

Goal state after:
W✝ X✝ Y✝ Z✝ : WalkingReflexivePair
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ (f.comp g).comp h = f.comp (g.comp h)
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ D.map f ≫ { f := c.ι.app B, h := ⋯ } = { f := c.ι.app A, h := ⋯ } ≫ ((const J).obj (coconePoint c t)).map f

Tactic:
ext1
        dsimp
        rw [comp_id]
        apply c.w

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
⊢ (F ⋙ H).map right ≫ H.map e₀ = H.map e₁ ≫ (G ⋙ H).map right

Tactic:
by simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp, h₂]

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

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
R : Type u_2
inst✝¹⁵ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹⁴ : CommRing A
inst✝¹³ : CommRing B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra A C
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : IsScalarTower R A B
P✝ : Ideal B
Q : Ideal C
p✝ : Ideal A
inst✝⁶ : Q.LiesOver p✝
inst✝⁵ : P✝.LiesOver p✝
G : Type u_6
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : SMulCommClass G A B
p : Ideal R
P : Ideal A
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
⊢ (map (mk (map (algebraMap R A) p)) P).IsPrime

Tactic:
by
  apply Ideal.isPrime_map_quotientMk_of_isPrime
  rw [Ideal.map_le_iff_le_comap, Ideal.LiesOver.over (p := p) (P := P)]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
ι : Type u_5
g : ι → Submodule R M
⊢ localized₀ p f (⨆ i, g i) = ⨆ i, localized₀ p f (g i)

Tactic:
let : Module (Localization p) N := IsLocalizedModule.module p f
  have : IsScalarTower R (Localization p) N := IsLocalizedModule.isScalarTower_module p f
  simpa using! congr_arg (restrictScalars R) (localized'_iSup (Localization p) p f g)

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
k : ℕ
hk : f ^ k = 0
⊢ IsNilpotent (p.mapQ p f hp)

Tactic:
use k

Goal state after:
case h
R : Type u_1
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
k : ℕ
hk : f ^ k = 0
⊢ p.mapQ p f hp ^ k = 0
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      if ¬p₂.coeff x.2 = 0 then
        (if ¬p₁.coeff x.1 = 0 then a₁ * (algebraMap R A) (p₁.coeff x.1) else 0) * (a₂ * (algebraMap R A) (p₂.coeff x.2))
      else 0

Tactic:
← mul_ite_zero (¬coeff p₂ _ = 0) _ (_ * _)

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      (if ¬p₁.coeff x.1 = 0 then a₁ * (algebraMap R A) (p₁.coeff x.1) else 0) *
        if ¬p₂.coeff x.2 = 0 then a₂ * (algebraMap R A) (p₂.coeff x.2) else 0
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case neg
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
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯)
      ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m * (Ideal.Quotient.mk (Ideal.under R I)) rn) =
    (Ideal.quotientMap I (algebraMap R S) ⋯) 1
⊢ (Ideal.quotientMap I (algebraMap R S) H) ((Ideal.Quotient.mk J) (r * rn)) = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)

Tactic:
rw [map_one, map_mul] at hn

Goal state after:
case neg
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
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ (Ideal.quotientMap I (algebraMap R S) H) ((Ideal.Quotient.mk J) (r * rn)) = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)
Module: Mathlib.RingTheory.Localization.Ideal

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
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
z : S
r : R
s : ↥M
e : z * (algebraMap R S) ↑(r, s).2 = (algebraMap R S) (r, s).1
⊢ g z * (algebraMap R' S') ↑(f r, ⟨f ↑s, ⋯⟩).2 = (algebraMap R' S') (f r, ⟨f ↑s, ⋯⟩).1

Tactic:
simpa only [map_mul, ← RingHom.comp_apply, H] using DFunLike.congr_arg g e

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
ι : Type u_9
v : ι → M
H : ∀ (P : Ideal R) [inst : P.IsMaximal], LinearIndependent (Rₚ P) (⇑(f P) ∘ v)
P : Ideal R
x✝ : P.IsMaximal
⊢ Function.Injective
    ⇑((IsLocalizedModule.map P.primeCompl (Finsupp.mapRange.linearMap (Algebra.linearMap R (Rₚ P))) (f P))
        (Finsupp.linearCombination R v))

Tactic:
by rw [map_linearCombination]; exact H P

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Injective ⇑(algebraMap (Rₚ p) (Sₚ p))
p : Ideal R
hp : p.IsMaximal
⊢ (IsLocalizedModule.map p.primeCompl (Algebra.linearMap R (Rₚ p)) ↑(IsScalarTower.toAlgHom R S (Sₚ p)))
      (Algebra.linearMap R S) =
    ↑R (Algebra.linearMap (Rₚ p) (Sₚ p))

Tactic:
apply IsLocalizedModule.map_linearMap_of_isLocalization

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Surjective ⇑(algebraMap (Rₚ p) (Sₚ p))
p : Ideal R
hp : p.IsMaximal
⊢ (IsLocalizedModule.map p.primeCompl (Algebra.linearMap R (Rₚ p)) ↑(IsScalarTower.toAlgHom R S (Sₚ p)))
      (Algebra.linearMap R S) =
    ↑R (Algebra.linearMap (Rₚ p) (Sₚ p))

Tactic:
apply IsLocalizedModule.map_linearMap_of_isLocalization

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

Goal state before:
pp: case left
R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
⊢ ∀ a ∈ s,
    ∀ b ∈ s,
      b ∉ P →
        ∀ c ∈ s,
          ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
intro a _ b _ _ c _ d _ _ x hxP e

Goal state after:
case left
R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
a : S
a✝⁵ : a ∈ s
b : S
a✝⁴ : b ∈ s
a✝³ : b ∉ P
c : S
a✝² : c ∈ s
d : S
a✝¹ : d ∈ s
a✝ : d ∉ P
x : S
hxP : x ∉ P
e : x * (a * d) = x * (c * b)
⊢ ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
x✝¹ : A
x✝ : M
⊢ { toFun := fun n ↦ S.mkQ ((x✝¹ • x✝) ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id A) x✝¹ • { toFun := fun n ↦ S.mkQ (x✝ ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by simp; rfl

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

Goal state before:
pp: case refine_2
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ₚ
x : Rₚ ⧸ maximalIdeal Rₚ
⊢ ∃ a, (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) a = x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Goal state after:
case refine_2
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ₚ
x : Rₚ
⊢ ∃ a, (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) a = (Ideal.Quotient.mk (maximalIdeal Rₚ)) x
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp.refine_3.e_a
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S (1 * 1) z • y = (mk' S 1 z * (mk' S 1 z' * (algebraMap R S) ↑z')) • y

Tactic:
mk'_spec,

Goal state after:
case mp.refine_3.e_a
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S (1 * 1) z • y = (mk' S 1 z * (algebraMap R S) 1) • y
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp.refine_3.e_a
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S (1 * 1) z' • y' = (mk' S 1 z * (algebraMap R S) ↑z * mk' S 1 z') • y'

Tactic:
mk'_spec,

Goal state after:
case mp.refine_3.e_a
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S (1 * 1) z' • y' = ((algebraMap R S) 1 * mk' S 1 z') • y'
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: 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ₚ
x : R
s : ↥p.primeCompl
h₁ : (Ideal.Quotient.mk p) ↑s ≠ 0
⊢ (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ↑s) ≠ 0

Tactic:
RingEquiv.map_ne_zero_iff

Goal state after:
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ₚ
x : R
s : ↥p.primeCompl
h₁ : (Ideal.Quotient.mk p) ↑s ≠ 0
⊢ (Ideal.Quotient.mk p) ↑s ≠ 0
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: 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ₚ
x : R
s : ↥p.primeCompl
h₁ : (Ideal.Quotient.mk p) ↑s ≠ 0
h₂ : (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ↑s) ≠ 0
⊢ (Ideal.Quotient.mk (maximalIdeal Rₚ)) (mk' Rₚ x s * (algebraMap R Rₚ) ↑s) =
    (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) x)

Tactic:
mk'_spec,

Goal state after:
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ₚ
x : R
s : ↥p.primeCompl
h₁ : (Ideal.Quotient.mk p) ↑s ≠ 0
h₂ : (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ↑s) ≠ 0
⊢ (Ideal.Quotient.mk (maximalIdeal Rₚ)) ((algebraMap R Rₚ) x) = (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) x)
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
R✝ S T : Type u
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
s : S
inst✝ : IsLocalization.Away s T
f : R✝ →+* S
hf : (fun {R S} [CommRing R] [CommRing S] ↦ P) f
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S T).comp f)

Tactic:
exact hPc _ _ hf (hPl T s)

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
R S Rᵣ Sᵣ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Rᵣ
inst✝⁴ : CommRing Sᵣ
inst✝³ : Algebra R Rᵣ
inst✝² : Algebra S Sᵣ
M : Submonoid R
inst✝¹ : IsLocalization M Rᵣ
f : R →+* S
inst✝ : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra Rᵣ Sᵣ := (IsLocalization.map Sᵣ f ⋯).toAlgebra
algInst✝ : Algebra R Sᵣ := ((IsLocalization.map Sᵣ f ⋯).comp (algebraMap R Rᵣ)).toAlgebra
scalarTowerInst✝ : IsScalarTower R Rᵣ Sᵣ := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R Sᵣ))
this✝ : IsScalarTower R S Sᵣ
this : IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ
⊢ P (IsLocalization.map Sᵣ f ⋯)

Tactic:
apply hP.of_isLocalization M hf

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

Goal state before:
pp: case refine_2
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 : 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:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Goal state after:
case refine_2
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ₚ
⊢ 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.a
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank S N ≤ Module.rank R N

Tactic:
rw [Module.rank]; apply ciSup_le'; intro ⟨s, hs⟩

Goal state after:
case inr.a
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
s : Set N
hs : LinearIndepOn S id s
⊢ #↑↑⟨s, hs⟩ ≤ Module.rank R N