mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
key₀ : ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
φ : ℕ → ℕ := fun n ↦ Nat.recOn n (Classical.choose ⋯) fun k yk ↦ Classical.choose ⋯
⊢ ∃ a, Tendsto x atTop (𝓝 a)

Tactic:
have hφ :
    ∀ n : ℕ,
      φ n < φ (n + 1) ∧
        ∀ a b : ℕ,
          φ (n + 1) ≤ a →
            φ (n + 1) ≤ b → ∀ g : G, x b = g → ∃ g' : G, g / g' ∈ u (n + 1) ∧ x a = g' :=
    fun n => Classical.choose_spec (key₀ (n + 1) (φ n))

Goal state after:
G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
key₀ : ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
φ : ℕ → ℕ := fun n ↦ Nat.recOn n (Classical.choose ⋯) fun k yk ↦ Classical.choose ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ), φ (n + 1) ≤ a → φ (n + 1) ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u (n + 1) ∧ x a = ↑g'
⊢ ∃ a, Tendsto x atTop (𝓝 a)
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : c < 0
this : Tendsto (fun x ↦ c * x ^ n) atTop atBot
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

Tactic:
simp [not_tendsto_nhds_of_tendsto_atBot this, hc.ne, hn]

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s

Tactic:
by
  rw [inter_comm, e.leftInvOn.image_inter', image_source_eq_target, inter_comm]

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : OrderTopology α
⊢ 𝓝 ⊤ = ⨅ l, ⨅ (_ : l < ⊤), 𝓟 (Ioi l)

Tactic:
simp [nhds_eq_order (⊤ : α)]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
a✝ : Nontrivial 𝕜
hn : IsSMulRegular 𝕜 0
⊢ {x | 0 • x = 0}.Finite

pp: case inr
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
hn : IsSMulRegular 𝕜 n
a✝ : Nontrivial 𝕜
h0 : n ≠ 0
⊢ {x | n • x = 0}.Finite

Tactic:
exacts [hn.not_zero.elim, ENat.card_lt_top.mp <|
    (card_torsion_le_of_isSMulRegular p n h0 hn).trans_lt <| ENat.natCast_lt_top n]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
⊢ Bijective fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩

Tactic:
by
        refine ⟨fun m₁ m₂ h => Subtype.ext ?_, fun u => ?_⟩
        · simp_rw [Subtype.mk_eq_mk, natCast_div_mul_eq_nsmul] at h
          refine nsmul_injOn_Iio_addOrderOf ?_ ?_ h <;> rw [addOrderOf_period_div hn]
          exacts [m₁.2.1, m₂.2.1]
        · obtain ⟨m, hmn, hg, he⟩ := (addOrderOf_eq_pos_iff hn).mp u.2
          exact ⟨⟨m, hmn, hg⟩, Subtype.ext he⟩

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inl.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
this : Infinite { u // ¬IsOfFinAddOrder u }
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

Tactic:
exact Nat.card_eq_zero_of_infinite

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
h : x ≠ a + p
⊢ (fun x ↦ Quot.mk (EndpointIdent p a) (Set.inclusion ⋯ ((equivIco p a) x)))
      ((fun x ↦ x.liftOn (fun x ↦ ↑↑x) ⋯) (Quot.mk (EndpointIdent p a) ⟨x, hx⟩)) =
    Quot.mk (EndpointIdent p a) ⟨x, hx⟩

pp: case inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ (fun x ↦ Quot.mk (EndpointIdent p a) (Set.inclusion ⋯ ((equivIco p a) x)))
      ((fun x ↦ x.liftOn (fun x ↦ ↑↑x) ⋯) (Quot.mk (EndpointIdent p a) ⟨a + p, hx⟩)) =
    Quot.mk (EndpointIdent p a) ⟨a + p, hx⟩

Tactic:
· revert x
        dsimp only
        intro x hx h
        congr
        ext1
        apply congr_arg Subtype.val ((equivIco p a).right_inv ⟨x, hx.1, hx.2.lt_of_ne h⟩)

Goal state after:
case inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ (fun x ↦ Quot.mk (EndpointIdent p a) (Set.inclusion ⋯ ((equivIco p a) x)))
      ((fun x ↦ x.liftOn (fun x ↦ ↑↑x) ⋯) (Quot.mk (EndpointIdent p a) ⟨a + p, hx⟩)) =
    Quot.mk (EndpointIdent p a) ⟨a + p, hx⟩
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ (Finsupp.sum (freeMk x) fun x r ↦ r • (ConcreteCategory.hom f) x) = (ConcreteCategory.hom f) x

Tactic:
Finsupp.sum_single_index

Goal state after:
R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ 1 • (ConcreteCategory.hom f) x = (ConcreteCategory.hom f) x

R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ 0 • (ConcreteCategory.hom f) x = 0
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
⊢ S.toComposableArrows.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.toComposableArrows.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0

Tactic:
simp [-Fin.reduceFinMk]

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h₁ : S.δlast.Exact
h₂ : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.Exact

Tactic:
rw [exact_iff_δlast]
  constructor <;> assumption

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ Epi S.L₂.op.g

Tactic:
by dsimp; infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ Mono S.L₁.op.f

Tactic:
by dsimp; infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pushout.inr S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.op.δ.unop ≫ (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op).unop =
    (pushout.inl S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.v₁₂.τ₂ ≫ (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op).unop

Tactic:
apply Quiver.Hom.op_inj

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ ((pushout.inr S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.op.δ.unop ≫ (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op).unop).op =
    ((pushout.inl S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.v₁₂.τ₂ ≫ (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op).unop).op
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoPullback f g).inv ≫ pullback.snd f g = ↾fun p ↦ (↑p).2

Tactic:
ext
  exact PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd (pullbackIsPullback f g) _

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝¹² : Ring R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type v
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
L : Type v
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup L'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
eq0 : g ∘ₗ f = 0
⊢ (↑eL.symm ∘ₗ g ∘ₗ ↑eN) ∘ₗ (↑eN.symm ∘ₗ f) ∘ₗ ↑eM = 0

Tactic:
by
      ext x
      simpa using LinearMap.congr_fun eq0 (eM x)

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.inv 0 ⋯ = α.inv ≫ F.map' 0 1 homMk₁._proof_4 ⋯

Tactic:
rw [← cancel_epi α.hom, ← reassoc_of% w, α.hom_inv_id_assoc, β.hom_inv_id_app]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ F.map' 0 1 homMk₁._proof_4 ⋯ ≫ 𝟙 (F.δ₀.obj ⟨0, ⋯⟩) = F.map' 0 1 homMk₁._proof_4 ⋯
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ adj.unit.app (G.obj (F.obj Y)) ≫ G.map (adj.counit.app (F.1 ((𝟭 C).obj Y))) =
    𝟙 (G.obj ((𝟭 D).obj (F.1 ((𝟭 C).obj Y))))

Tactic:
· rw [← G.map_id]
          simp

Goal state after:
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
inst✝¹ : ComonadicLeftAdjoint R
inst✝ : PreservesLimitsOfShape J R
⊢ PreservesLimitsOfShape J (comonadicRightAdjoint R)

Tactic:
by
    apply (Adjunction.rightAdjoint_preservesLimits (comonadicAdjunction R)).1

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

Goal state before:
pp: A : Type u_2
inst✝⁵ : CommSemiring A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
P : Ideal B
G : Type u_5
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
g : G
inst✝ : SMulCommClass G A B
⊢ under A (g • P) = under A P

Tactic:
by
  ext a
  rw [mem_comap, mem_comap, mem_pointwise_smul_iff_inv_smul_mem, smul_algebraMap]

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

Goal state before:
pp: case mk
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
a✝ : B ⧸ P
x : B
⊢ (algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B 1) ⋯) (Quot.mk (⇑(quotientRel P)) x) =
    1 (Quot.mk (⇑(quotientRel P)) x)

Tactic:
exact congrArg (Ideal.Quotient.mk P) (one_smul G x)

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
⊢ S.IsPrimary ↔ S ≠ ⊤ ∧ ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ n, r ^ n • ⊤ = ⊥

Tactic:
by
  refine (and_congr_right fun _ ↦ ?_)
  simp_rw [S.mkQ_surjective.forall, ← map_smul, ne_eq, ← LinearMap.mem_ker, ker_mkQ]
  congr! 2
  rw [forall_comm, ← or_iff_not_imp_left,
    ← LinearMap.range_eq_top.mpr S.mkQ_surjective, ← map_top]
  simp_rw [eq_bot_iff, ← map_pointwise_smul, map_le_iff_le_comap, comap_bot, ker_mkQ]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N✝ N₁ N₂ : Submodule R M
S✝ S₁ S₂ : Set M
N : Submodule R M
S : Set M
r : R
⊢ ∀ {x : R}, x ∈ {r | r • S ⊆ ↑N} → r • x ∈ {r | r • S ⊆ ↑N}

Tactic:
simp only [Set.mem_ofPred_eq, smul_eq_mul, mul_smul, Set.smul_set_subset_iff]
    intro x hx y hy
    exact N.smul_mem _ (hx hy)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
s : Set (Submodule R M)
⊢ ⨆ i, localized₀ p f ↑i = sSup (localized₀ p f '' s)

Tactic:
sSup_image'

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
s : Set (Submodule R M)
⊢ ⨆ i, localized₀ p f ↑i = ⨆ a, localized₀ p f ↑a
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
s : Set (Submodule R M)
⊢ ⨆ i, localized' S p f ↑i = sSup (localized' S p f '' s)

Tactic:
sSup_image'

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
s : Set (Submodule R M)
⊢ ⨆ i, localized' S p f ↑i = ⨆ a, localized' S p f ↑a
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.minimalPrimes ⊆ {J | I ≤ J ∧ J.IsPrime}

Tactic:
intro I hI

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I✝ I : Ideal R
hI : I ∈ I✝.minimalPrimes
⊢ I ∈ {J | I✝ ≤ J ∧ J.IsPrime}
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case h
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI : I ^ n = ⊥
⊢ P I

Tactic:
by_cases hI' : I = ⊥

Goal state after:
case pos
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI : I ^ n = ⊥
hI' : I = ⊥
⊢ P I

case neg
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI : I ^ n = ⊥
hI' : ¬I = ⊥
⊢ P I
Module: Mathlib.RingTheory.Localization.Ideal

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
I I' : { p // p.IsPrime }
⊢ I ≤ I' →
    { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I'

Tactic:
exact fun h x hx => h hx

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
s : Set R
spn : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝⁸ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝⁷ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝⁶ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
Nₚ : ↑s → Type u_6
inst✝⁵ : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝⁴ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)
Lₚ : ↑s → Type u_7
inst✝² : (r : ↑s) → AddCommMonoid (Lₚ r)
inst✝¹ : (r : ↑s) → Module R (Lₚ r)
h : (r : ↑s) → L →ₗ[R] Lₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : ↑s),
    ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G).ker =
      ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F).range
r : ↑s
this :
  ∀ (x : Nₚ r),
    x ∈ ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G).ker ↔
      x ∈ ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F).range
x : Nₚ r
⊢ x ∈ ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G).ker ↔
    x ∈ ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F).range

Tactic:
simp only [mem_range, mem_ker] at this ⊢

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
s : Set R
spn : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝⁸ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝⁷ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝⁶ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
Nₚ : ↑s → Type u_6
inst✝⁵ : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝⁴ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)
Lₚ : ↑s → Type u_7
inst✝² : (r : ↑s) → AddCommMonoid (Lₚ r)
inst✝¹ : (r : ↑s) → Module R (Lₚ r)
h : (r : ↑s) → L →ₗ[R] Lₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : ↑s),
    ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G).ker =
      ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F).range
r : ↑s
x : Nₚ r
this :
  ∀ (x : Nₚ r),
    ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) x = 0 ↔
      ∃ y, ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F) y = x
⊢ ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) x = 0 ↔
    ∃ y, ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F) y = x
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: 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✝ : FiniteType R S
⊢ EssFiniteType R S

Tactic:
by
  obtain ⟨s, hs⟩ := ‹FiniteType R S›
  rw [essFiniteType_iff]
  exact ⟨s, fun _ ↦ by simpa only [hs, mem_top, and_true, true_and] using ⟨1, isUnit_one⟩⟩

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 = RingHom.ker ((algebraMap Rₚ (Rₚ ⧸ maximalIdeal Rₚ)).comp (algebraMap R Rₚ))

Tactic:
← RingHom.comap_ker,

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 = comap (algebraMap R Rₚ) (RingHom.ker (algebraMap Rₚ (Rₚ ⧸ maximalIdeal Rₚ)))