mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ addOrderOf u = n ↔ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u

Tactic:
refine ⟨QuotientAddGroup.induction_on u ?_, ?_⟩
  · rintro ⟨m, -, h₁, rfl⟩
    exact addOrderOf_div_of_gcd_eq_one h h₁
  rintro k rfl
  obtain ⟨m, hm, hk⟩ := (AddCircle.nsmul_eq_zero_iff h).mp
    (addOrderOf_nsmul_eq_zero (k : AddCircle p))
  refine ⟨m, hm, mul_right_cancel₀ h.ne' ?_, hk⟩
  convert! gcd_mul_addOrderOf_div_eq p m h using 1
  · rw [hk]
  · apply one_mul

Goal state after:
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
⊢ commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X)) ≅
    (F ⋙ forget AddCommGrpCat).mapCommGrp.obj (Preadditive.commGrpEquivalence.functor.obj X)

Tactic:
refine CommGrp.mkIso Multiplicative.toAdd.toIso (by
    rw [Functor.obj.η_def X (F := F ⋙ forget AddCommGrpCat)]
    cat_disch) ?_

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
⊢ μ ≫ Multiplicative.toAdd.toIso.hom = (Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫ μ
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
z₂ z₂' : A ⟶ S.cycles
⊢ z₂ ≫ S.homologyπ = z₂' ≫ S.homologyπ ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ z₂ = π ≫ z₂' + x₁ ≫ S.toCycles

Tactic:
by
  obtain ⟨x₂, hx₂, rfl⟩ : ∃ (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0), z₂ = S.liftCycles x₂ hx₂ :=
    ⟨z₂ ≫ S.iCycles, by simp, by simp [← cancel_mono S.iCycles]⟩
  obtain ⟨x₂', hx₂', rfl⟩ : ∃ (x₂' : A ⟶ S.X₂) (hx₂' : x₂' ≫ S.g = 0), z₂' =
    S.liftCycles x₂' hx₂' := ⟨z₂' ≫ S.iCycles, by simp,
      by simp [← cancel_mono S.iCycles]⟩
  simp [liftCycles_comp_homologyπ_eq_iff_up_to_refinements, ← cancel_mono S.iCycles]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : Mono (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
this : S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f

Tactic:
← S₁.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : Mono (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
this : S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ = 0
⊢ S₁.liftCycles x₂ ?hx₂ ≫ S₁.homologyπ = 0

case hx₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : Mono (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
this : S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ = 0
⊢ x₂ ≫ S₁.g = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case right
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : ↑(I.multicospan ⋙ forget C).sections
b : J.R
⊢ ↑((fun x ↦
            ⟨fun j ↦
              match j with
              | WalkingMulticospan.left a => ↑x a
              | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)),
              ⋯⟩)
          ((fun x ↦ ⟨fun x_1 ↦ ↑x (WalkingMulticospan.left x_1), ⋯⟩) x))
      (WalkingMulticospan.right b) =
    ↑x (WalkingMulticospan.right b)

Tactic:
rw [← x.2 (WalkingMulticospan.Hom.fst b)]

Goal state after:
case right
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : ↑(I.multicospan ⋙ forget C).sections
b : J.R
⊢ ↑((fun x ↦
            ⟨fun j ↦
              match j with
              | WalkingMulticospan.left a => ↑x a
              | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)),
              ⋯⟩)
          ((fun x ↦ ⟨fun x_1 ↦ ↑x (WalkingMulticospan.left x_1), ⋯⟩) x))
      (WalkingMulticospan.right b) =
    (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.fst b))) (↑x (WalkingMulticospan.left (J.fst b)))
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
A : Type uA
M : Type uM
B : Type uB
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : AddCommGroup B
inst✝³ : AddCommGroup M
inst✝² : Module R A
inst✝¹ : Module R B
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : B →ₗ[R] M
hj : Function.Injective ⇑j
exac : j.range = g.ker
h : g ∘ₗ f = LinearMap.id
⊢ Function.Injective ⇑(↑ULift.moduleEquiv.symm ∘ₗ j ∘ₗ ↑ULift.moduleEquiv)

Tactic:
simpa using hj

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
⊢ i.hom ≫ (adj.toMonad.transport i).μ ≫ adj.unit = 𝟙 (L ⋙ R)

Tactic:
← Iso.eq_inv_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
⊢ (adj.toMonad.transport i).μ ≫ adj.unit = i.inv ≫ 𝟙 (L ⋙ R)
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).unit.app ((reflector R ⋙ R).obj X.A) ≫ R.map ((reflector R).map X.a) =
    𝟙 ((reflector R ⋙ R).obj X.A)

Tactic:
dsimp only [Functor.comp_obj, Adjunction.toMonad_coe]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).unit.app (R.obj ((reflector R).obj X.A)) ≫ R.map ((reflector R).map X.a) =
    𝟙 (R.obj ((reflector R).obj X.A))
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ R.map ((coreflector R).map X.a) ≫ (coreflectorAdjunction R).counit.app ((coreflector R ⋙ R).obj X.A) =
    𝟙 ((coreflector R ⋙ R).obj X.A)

Tactic:
dsimp only [Functor.comp_obj, Adjunction.toMonad_coe]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ R.map ((coreflector R).map X.a) ≫ (coreflectorAdjunction R).counit.app (R.obj ((coreflector R).obj X.A)) =
    𝟙 (R.obj ((coreflector R).obj X.A))
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : J.L
⊢ (isoEqualizer I).hom ≫ equalizer.ι I.fstPiMap I.sndPiMap ≫ Pi.π I.left a = ι I a

Tactic:
← Iso.eq_inv_comp,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : J.L
⊢ equalizer.ι I.fstPiMap I.sndPiMap ≫ Pi.π I.left a = (isoEqualizer I).inv ≫ ι I a
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
j : J
⊢ T.μ.app ((D ⋙ T.forget).obj j) ≫ (D.obj j).a ≫ c.ι.app j = T.map (D.obj j).a ≫ (D.obj j).a ≫ c.ι.app j

Tactic:
apply (D.obj j).assoc_assoc _

Goal state after:
Module: Mathlib.RingTheory.Flat.CategoryTheory

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : C.Exact
⊢ (C.map (tensorLeft M)).Exact

Tactic:
moduleCat_exact_iff_function_exact

Goal state after:
R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : Function.Exact ⇑(ConcreteCategory.hom C.f) ⇑(ConcreteCategory.hom C.g)
⊢ Function.Exact ⇑(ConcreteCategory.hom (C.map (tensorLeft M)).f) ⇑(ConcreteCategory.hom (C.map (tensorLeft M)).g)
Module: Mathlib.RingTheory.Flat.CategoryTheory

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : C.Exact
⊢ (C.map (tensorRight M)).Exact

Tactic:
moduleCat_exact_iff_function_exact

Goal state after:
R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : Function.Exact ⇑(ConcreteCategory.hom C.f) ⇑(ConcreteCategory.hom C.g)
⊢ Function.Exact ⇑(ConcreteCategory.hom (C.map (tensorRight M)).f) ⇑(ConcreteCategory.hom (C.map (tensorRight M)).g)
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : ComonadicLeftAdjoint R
inst✝¹ : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst✝ : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
A : D ⥤ (comonadicAdjunction R).toComonad.Coalgebra := Comonad.comparison (comonadicAdjunction R)
B : (comonadicAdjunction R).toComonad.Coalgebra ⥤ C := (comonadicAdjunction R).toComonad.forget
⊢ CreatesLimit K R

Tactic:
let i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ Comonad.forget _ ≅ K ⋙ R :=
    Functor.associator _ _ _ ≪≫
      isoWhiskerLeft K (Comonad.comparisonForget (comonadicAdjunction R))

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : ComonadicLeftAdjoint R
inst✝¹ : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst✝ : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
A : D ⥤ (comonadicAdjunction R).toComonad.Coalgebra := Comonad.comparison (comonadicAdjunction R)
B : (comonadicAdjunction R).toComonad.Coalgebra ⥤ C := (comonadicAdjunction R).toComonad.forget
i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ (comonadicAdjunction R).toComonad.forget ≅ K ⋙ R :=
  K.associator (Comonad.comparison (comonadicAdjunction R)) (comonadicAdjunction R).toComonad.forget ≪≫
    K.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction R))
⊢ CreatesLimit K R
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulLeft R a ^ n = 0
⊢ IsNilpotent a

Tactic:
use n

Goal state after:
case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulLeft R a ^ n = 0
⊢ a ^ n = 0
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ IsNilpotent (mulLeft R a)

Tactic:
use n

Goal state after:
case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ mulLeft R a ^ n = 0
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulRight R a ^ n = 0
⊢ IsNilpotent a

Tactic:
use n

Goal state after:
case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulRight R a ^ n = 0
⊢ a ^ n = 0
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ IsNilpotent (mulRight R a)

Tactic:
use n

Goal state after:
case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ mulRight R a ^ n = 0
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ ⊤.minimalPrimes = ∅

Tactic:
ext p
  simp only [Set.notMem_empty, iff_false]
  intro h
  exact h.isPrime.ne_top (top_le_iff.mp h.le)

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

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid 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
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
⊢ ∀ r ∈ localized' S p (Algebra.linearMap R S) I, ∀ n ∈ N', r • n ∈ I • restrictScalars R N'

Tactic:
rintro _ ⟨r, hr, s, rfl⟩ n hn

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid 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
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
r : R
hr : r ∈ I
s : ↥p
n : N
hn : n ∈ N'
⊢ IsLocalizedModule.mk' (Algebra.linearMap R S) r s • n ∈ I • restrictScalars R N'
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
⊢ IsNilpotent (LinearMap.restrict f hp)

Tactic:
use n

Goal state after:
case h
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
⊢ LinearMap.restrict f hp ^ n = 0
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
I p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ : map (Quotient.mk (map (algebraMap R S) p)) P ∈ (map (Quotient.mk (map (algebraMap R S) p)) J).minimalPrimes
q : Ideal S
x✝ : (fun q ↦ q.IsPrime ∧ map (algebraMap R S) I ⊔ J ≤ q) q
hqle : q ≤ P
left✝ : q.IsPrime
hleq : map (algebraMap R S) I ⊔ J ≤ q
⊢ P ≤ q

Tactic:
simp only [sup_le_iff] at hleq

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
I p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ : map (Quotient.mk (map (algebraMap R S) p)) P ∈ (map (Quotient.mk (map (algebraMap R S) p)) J).minimalPrimes
q : Ideal S
x✝ : (fun q ↦ q.IsPrime ∧ map (algebraMap R S) I ⊔ J ≤ q) q
hqle : q ≤ P
left✝ : q.IsPrime
hleq : map (algebraMap R S) I ≤ q ∧ J ≤ q
⊢ P ≤ q
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))]

Goal state after:
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsUnit ((DoubleQuot.quotQuotEquivQuotOfLE ⋯) ((mk (map (mk (I ^ n)) I)) ((mk (I ^ n)) x))) ↔ IsUnit ((mk I) x)
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

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

Tactic:
use n

Goal state after:
case h
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ map (mk (I ^ n)) I ^ n = 0
Module: Mathlib.RingTheory.Localization.Algebra

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝²⁹ : CommSemiring R✝
inst✝²⁸ : CommSemiring S
inst✝²⁷ : CommSemiring P
inst✝²⁶ : CommSemiring Q
M✝ : Submonoid R✝
T : Submonoid P
inst✝²⁵ : Algebra R✝ S
inst✝²⁴ : Algebra P Q
inst✝²³ : IsLocalization M✝ S
inst✝²² : IsLocalization T Q
g : R✝ →+* P
R : Type u_5
inst✝²¹ : CommSemiring R
M : Submonoid R
A : Type u_6
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
B : Type u_7
inst✝¹⁸ : CommSemiring B
inst✝¹⁷ : Algebra R B
Rₚ : Type u_8
inst✝¹⁶ : CommSemiring Rₚ
inst✝¹⁵ : Algebra R Rₚ
inst✝¹⁴ : IsLocalization M Rₚ
Aₚ : Type u_9
inst✝¹³ : CommSemiring Aₚ
inst✝¹² : Algebra R Aₚ
inst✝¹¹ : Algebra A Aₚ
inst✝¹⁰ : IsScalarTower R A Aₚ
inst✝⁹ : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst✝⁸ : CommSemiring Bₚ
inst✝⁷ : Algebra R Bₚ
inst✝⁶ : Algebra B Bₚ
inst✝⁵ : IsScalarTower R B Bₚ
inst✝⁴ : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst✝³ : Algebra Rₚ Aₚ
inst✝² : Algebra Rₚ Bₚ
inst✝¹ : IsScalarTower R Rₚ Aₚ
inst✝ : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ IsLocalization (Submonoid.map (↑↑f) (algebraMapSubmonoid A M)) Bₚ

Tactic:
AlgHom.toRingHom_toMonoidHom,

Goal state after:
R✝ : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝²⁹ : CommSemiring R✝
inst✝²⁸ : CommSemiring S
inst✝²⁷ : CommSemiring P
inst✝²⁶ : CommSemiring Q
M✝ : Submonoid R✝
T : Submonoid P
inst✝²⁵ : Algebra R✝ S
inst✝²⁴ : Algebra P Q
inst✝²³ : IsLocalization M✝ S
inst✝²² : IsLocalization T Q
g : R✝ →+* P
R : Type u_5
inst✝²¹ : CommSemiring R
M : Submonoid R
A : Type u_6
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
B : Type u_7
inst✝¹⁸ : CommSemiring B
inst✝¹⁷ : Algebra R B
Rₚ : Type u_8
inst✝¹⁶ : CommSemiring Rₚ
inst✝¹⁵ : Algebra R Rₚ
inst✝¹⁴ : IsLocalization M Rₚ
Aₚ : Type u_9
inst✝¹³ : CommSemiring Aₚ
inst✝¹² : Algebra R Aₚ
inst✝¹¹ : Algebra A Aₚ
inst✝¹⁰ : IsScalarTower R A Aₚ
inst✝⁹ : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst✝⁸ : CommSemiring Bₚ
inst✝⁷ : Algebra R Bₚ
inst✝⁶ : Algebra B Bₚ
inst✝⁵ : IsScalarTower R B Bₚ
inst✝⁴ : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst✝³ : Algebra Rₚ Aₚ
inst✝² : Algebra Rₚ Bₚ
inst✝¹ : IsScalarTower R Rₚ Aₚ
inst✝ : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ IsLocalization (Submonoid.map (↑f) (algebraMapSubmonoid A M)) Bₚ
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)
⊢ ∀ (y : ↥(Submonoid.map f M)), IsUnit ((algebraMap R' S') ↑y)

Tactic:
by
    rintro ⟨_, y, hy, rfl⟩
    simpa only [← RingHom.comp_apply, H] using (IsLocalization.map_units S ⟨y, hy⟩).map g

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
this :
  (algebraMap R T) (y₁ * ↑s₂) = (algebraMap R T) (y₂ * ↑s₁) →
    ∃ a, (algebraMap R S) (↑a * (y₁ * ↑s₂)) = (algebraMap R S) (↑a * (y₂ * ↑s₁))
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂

Tactic:
have h₁ := @IsUnit.mul_left_inj T _ _ (algebraMap S T x₁) (algebraMap S T x₂)
        (IsLocalization.map_units T ⟨(s₁ : R), h s₁.prop⟩)
      have h₂ := @IsUnit.mul_left_inj T _ _ ((algebraMap S T x₁) * (algebraMap R T s₁))
        ((algebraMap S T x₂) * (algebraMap R T s₁))
        (IsLocalization.map_units T ⟨(s₂ : R), h s₂.prop⟩)
      simp only [IsScalarTower.algebraMap_apply R S T] at h₁ h₂
      simp only [IsScalarTower.algebraMap_apply R S T, map_mul, ← e₁, ← e₂, ← mul_assoc,
        mul_right_comm _ (algebraMap R S s₂),
        (IsLocalization.map_units S s₁).mul_left_inj,
        (IsLocalization.map_units S s₂).mul_left_inj] at this
      rw [h₂, h₁] at this
      simpa only [mul_comm] using! this

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ ∀ (s : S), ∃ t ∈ adjoin R ↑∅, IsUnit t ∧ s * t ∈ adjoin R ↑∅

Tactic:
simp only [Finset.coe_empty, Algebra.adjoin_empty, Algebra.mem_bot,
    Set.mem_range, exists_exists_eq_and]

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ ∀ (s : S), ∃ a, IsUnit ((algebraMap R S) a) ∧ ∃ y, (algebraMap R S) y = s * (algebraMap R S) a
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✝ : 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
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
⊢ (algebraMap R Rₚ) ↑s ∉ maximalIdeal Rₚ

Tactic:
rw [← Ideal.mem_under, IsLocalization.AtPrime.under_maximalIdeal Rₚ p]

Goal state after:
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
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
⊢ ↑s ∉ p