mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case w
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↥(cycles₁ (res S.subtype (A.toCoinvariants S)))
hz :
  (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
w : ↑(ModuleCat.of k (G × G →₀ ↑(A.toCoinvariants S)))
hzw :
  (ModuleCat.Hom.hom (d₂₁ (A.toCoinvariants S))) w =
    ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) -
      ↑((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
Z : ↥S →₀ ↑A
hZ : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Z = ↑z
W : G × G →₀ ↑A
hW : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ W = w
b : G →₀ ↑A := ↑x + (ConcreteCategory.hom (d₂₁ A)) W - (lmapDomain (↑A) k ⇑S.subtype) Z
hb : ∀ (g : G), b g ∈ Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)
β : G →₀ ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)) :=
  mapRange (Function.invFun ⇑(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype) ⋯ b
hβb : mapRange Subtype.val ⋯ β = b
α : ↥S →₀ ↑A
hα :
  (ModuleCat.Hom.hom (shortComplexH1 A).pOpcycles ∘ₗ
        ModuleCat.Hom.hom (mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂)
      α =
    (ModuleCat.Hom.hom (shortComplexH1 A).pOpcycles ∘ₗ
        ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂)
      β
δ : G × G →₀ ↑A
hβ :
  (ModuleCat.Hom.hom (shortComplexH1 A).f) δ =
    (ModuleCat.Hom.hom (mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂) α -
      (ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂) β
hαZ : (ConcreteCategory.hom (d₂₁ A)) (W + δ) = mapDomain Subtype.val (α + Z) - ↑x
⊢ α + Z ∈ cycles₁ (res S.subtype A)

Tactic:
· rw [mem_cycles₁_iff]
    have : x + d₂₁ A (W + δ) ∈ cycles₁ A := Submodule.add_mem _ x.2 (d₂₁_apply_mem_cycles₁ _)
    rwa [eq_sub_iff_add_eq'.1 hαZ, mem_cycles₁_iff, sum_mapDomain_index_inj
      Subtype.val_injective, sum_mapDomain_index_inj Subtype.val_injective] at this

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
⊢ cyclesMap f φ 2 ≫ (isoCycles₂ B).hom = (isoCycles₂ A).hom ≫ mapCycles₂ f φ

Tactic:
by
  simp [← cancel_mono (moduleCatLeftHomologyData (shortComplexH2 B)).i, mapShortComplexH2,
    chainsMap_f_2_comp_chainsIso₂ f]

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

Goal state before:
pp: case h.refine_1
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t
h : IsLocalization.mk' R' r s ∈ p
⊢ r ∈ Ideal.comap (algebraMap R R') p

Tactic:
exact hSR'.mk'_mem_iff.mp h

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
a✝ b✝ : Kˣ ⧸ (powMonoidHom n).range
hx : a✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
hy : b✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
v : HeightOneSpectrum R
hv : v ∉ S
⊢ (v.valuationOfNeZeroMod n) (a✝ * b✝) = 1

Tactic:
rw [map_mul, hx v hv, hy v hv, one_mul]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
a✝ b✝ : Kˣ ⧸ (powMonoidHom n).range
hx : a✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
hy : b✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
v : HeightOneSpectrum R
hv : v ∉ S
⊢ (v.valuationOfNeZeroMod n) (a✝ * b✝) = 1

Tactic:
by rw [map_mul, hx v hv, hy v hv, one_mul]

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

Goal state before:
pp: case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ hI.dpow n (x + y) = hJ.dpow n (x + y)

Tactic:
rw [hI.dpow_add (mul_le_left hx) (mul_le_left hy),
      hJ.dpow_add (mul_le_right hx) (mul_le_right hy)]
    apply sum_congr rfl
    intro k _
    rw [hx', hy']

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.mem.mem
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x✝ : DividedPowerAlgebra R M
k : ℕ
i : ι
x : DividedPowerAlgebra R M
hx : x ∈ Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)
⊢ x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
| mem x hx =>

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
m✝ n✝ : ℕ
x✝ : A
hn : n✝ ≠ 0
hx : x✝ ∈ J
⊢ (if (if x✝ ∈ J then hI.dpow n✝ x✝ else 0) ∈ J then hI.dpow m✝ (if x✝ ∈ J then hI.dpow n✝ x✝ else 0) else 0) =
    ↑(m✝.uniformBell n✝) * if x✝ ∈ J then hI.dpow (m✝ * n✝) x✝ else 0

Tactic:
simp [if_pos hx, if_pos (hJ.dpow_mem _ hn hx), hI.dpow_comp hn (hJ.isSubideal hx)]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.IsSubDPIdeal J
hK : hI.IsSubDPIdeal K
⊢ hI.IsSubDPIdeal (J ⊔ K)

Tactic:
by
  rw [← J.span_eq, ← K.span_eq, ← span_union,
    span_isSubDPIdeal_iff (Set.union_subset_iff.mpr ⟨hJ.1, hK.1⟩)]
  intro n hn a ha
  rcases ha with ha | ha
  · exact span_mono Set.subset_union_left (subset_span (hJ.2 n hn ha))
  · exact span_mono Set.subset_union_right (subset_span (hK.2 n hn ha))

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case inr
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
hx : IsNilpotent x
⊢ ε ∣ x

Tactic:
← isNilpotent_iff_eps_dvd

Goal state after:
case inr
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
x : K[ε]
hxI : x ∈ I
hx : IsNilpotent x
⊢ IsNilpotent x
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: case intro
k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
ι : Type u_4
inst✝ : Finite ι
val✝ : Fintype ι
⊢ ∃ n, Nonempty ((ι → R) ≃ₐ[R] Fin n → R)

Tactic:
exact ⟨_, ⟨AlgEquiv.piCongrLeft' _ _ (Fintype.equivFin ι)⟩⟩

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: case succ.inr.refine_4
n✝ : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n✝ →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n✝ + 1)
h✝ : Nontrivial R
this✝⁴ : Nontrivial S
U : Type u
w✝⁶ : CommRing U
w✝⁵ : Algebra S U
e✝ : S ⊗[R] S ≃ₐ[S] S × U
algInst✝¹ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝³ : IsScalarTower S (S × U) U
this✝² : Etale S U
this✝¹ : Module.Finite S U
this✝ : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n✝ + 1
this : Module.rankAtStalk U = ↑n✝
V : Type u
w✝⁴ : CommRing V
w✝³ : Algebra S V
w✝² : Module.FaithfullyFlat S V
w✝¹ : Module.Finite S V
w✝ : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst✝ : Algebra R V := ((algebraMap S V).comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S V := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R V))
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  (TensorProduct.cancelBaseChange R S V V S).symm.trans
    ((TensorProduct.congr AlgEquiv.refl e✝).trans
      ((TensorProduct.prodRight S V V S U).trans
        (((TensorProduct.rid S V V).prodCongr f).trans
          (((AlgEquiv.funUnique V Unit V).symm.prodCongr AlgEquiv.refl).trans
            (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V).symm))))
⊢ IsFiniteSplit V (V ⊗[R] S)

Tactic:
exact .of_algEquiv e.symm

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ Ideal.map f I
⊢ dpow hI f n x ∈ Ideal.map f I

Tactic:
obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp hx

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
hx : f a ∈ Ideal.map f I
⊢ dpow hI f n (f a) ∈ Ideal.map f I
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
Q : Ideal S
σ : G
inst✝ : Q.IsPrime
h : IsArithFrobAt R σ Q
⊢ σ ∈ MulAction.stabilizer G Q

Tactic:
MulAction.mem_stabilizer_iff

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
Q : Ideal S
σ : G
inst✝ : Q.IsPrime
h : IsArithFrobAt R σ Q
⊢ σ • Q = Q
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
inst✝¹ : Finite G
inst✝ : Algebra.IsInvariant R S G
P : Ideal R
hP : ∃ Q, Finite (S ⧸ ↑Q)
⊢ ∃ σ, (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)

Tactic:
by
  obtain ⟨⟨Q, hQ₁, hQ₂⟩, hQ₃⟩ := hP
  have (Q' : Ideal.primesOver P S) : ∃ σ : G, Q'.1 = σ • Q :=
    Algebra.IsInvariant.exists_smul_of_under_eq R S G _ _ (hQ₂.over.symm.trans Q'.2.2.over)
  choose τ hτ using this
  obtain ⟨σ, hσ⟩ := exists_of_isInvariant R G Q
  refine ⟨fun Q' ↦ τ Q' * σ * (τ Q')⁻¹, fun Q' ↦ hτ Q' ▸ hσ.conj (τ Q'), fun Q₁ Q₂ ↦
    .trans (.symm (isConj_iff.mpr ⟨τ Q₁, rfl⟩)) (isConj_iff.mpr ⟨τ Q₂, rfl⟩)⟩

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
⊢ (powerSeriesFamily x (C r)).hsum.coeff g = ((algebraMap R R⟦Γ⟧) r).coeff g

Tactic:
simp only [coeff_hsum, smulFamily_toFun, coeff_C, powers_toFun, ite_smul, zero_smul]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
⊢ ∑ᶠ (i : ℕ), (if i = 0 then r • (if 0 < x.orderTop then x else 0) ^ i else 0).coeff g = ((algebraMap R R⟦Γ⟧) r).coeff g
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
⊢ x.order < y.order

Tactic:
exact order_lt_order_of_eq_add_single (sub_add_cancel x _).symm hy

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
⊢ IsUnit x

Tactic:
by
  let ⟨⟨u, i, ui, iu⟩, h⟩ := hx
  rw [Units.val_mk] at h
  rw [h] at iu
  have h' := SummableFamily.one_sub_self_mul_hsum_powers (unit_aux x iu _ hxo.addUnit.neg_add)
  rw [sub_sub_cancel] at h'
  exact isUnit_of_mul_isUnit_right (.of_mul_eq_one _ h')

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal R
h₂ : (Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f)) = 0
⊢ ¬IsUnit ((Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f)))

Tactic:
rw [h₂]

Goal state after:
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal R
h₂ : (Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f)) = 0
⊢ ¬IsUnit 0
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
⊢ p.height ≤ 1

Tactic:
let f := algebraMap R (Localization.AtPrime p)

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
⊢ p.height ≤ 1
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: case h
P : ProfiniteGrp.{u}
U : Set ↑(limit P.diagram).toProfinite.toTop
s : Set ((j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux P.diagram
uDefaultSpec : spc ∈ s
J : Finset (OpenNormalSubgroup ↑P.toProfinite.toTop)
fJ : (a : OpenNormalSubgroup ↑P.toProfinite.toTop) → Set ↑(P.diagram.obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ spc a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑P.toProfinite.toTop := ⨅ j, ↑(↑j).toOpenSubgroup
hM : M.Normal
hMOpen : IsOpen ↑M
m : OpenNormalSubgroup ↑P.toProfinite.toTop := { toSubgroup := M, isOpen' := hMOpen, isNormal' := ⋯ }
origin : ↑P.toProfinite.toTop
horigin : (QuotientGroup.mk' M) origin = spc m
a : OpenNormalSubgroup ↑P.toProfinite.toTop
a_in_J : a ∈ ↑J
M_to_Na : m ⟶ a := ⋯.hom
⊢ (ConcreteCategory.hom (P.toFiniteQuotientFunctor.map M_to_Na)) ((QuotientGroup.mk' M) origin) ∈ fJ a

Tactic:
rw [horigin]

Goal state after:
case h
P : ProfiniteGrp.{u}
U : Set ↑(limit P.diagram).toProfinite.toTop
s : Set ((j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux P.diagram
uDefaultSpec : spc ∈ s
J : Finset (OpenNormalSubgroup ↑P.toProfinite.toTop)
fJ : (a : OpenNormalSubgroup ↑P.toProfinite.toTop) → Set ↑(P.diagram.obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ spc a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑P.toProfinite.toTop := ⨅ j, ↑(↑j).toOpenSubgroup
hM : M.Normal
hMOpen : IsOpen ↑M
m : OpenNormalSubgroup ↑P.toProfinite.toTop := { toSubgroup := M, isOpen' := hMOpen, isNormal' := ⋯ }
origin : ↑P.toProfinite.toTop
horigin : (QuotientGroup.mk' M) origin = spc m
a : OpenNormalSubgroup ↑P.toProfinite.toTop
a_in_J : a ∈ ↑J
M_to_Na : m ⟶ a := ⋯.hom
⊢ (ConcreteCategory.hom (P.toFiniteQuotientFunctor.map M_to_Na)) (spc m) ∈ fJ a
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsMaximal
⊢ (Ideal.map C p).height = p.height

Tactic:
by
  have : (p.map C).LiesOver p := ⟨IsMaximal.eq_of_le inferInstance IsPrime.ne_top' le_comap_map⟩
  simp [height_eq_height_add_of_liesOver_of_hasGoingDown p]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
h : I ≤ Ring.jacobson R
a✝ : Nontrivial R
⊢ ringKrullDim R ≤ ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)

Tactic:
ringKrullDim_le_iff_isMaximal_height_le

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
h : I ≤ Ring.jacobson R
a✝ : Nontrivial R
⊢ ∀ ⦃m : Ideal R⦄, m.IsMaximal → ↑m.height ≤ ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
x : M
hx : x ∈ N
y : M
x✝ : x + a ^ n • y ∈ f n ⊓ (N + a ^ n • ⊤)
h1 : x + a ^ n • y ∈ ↑(f n)
⊢ x + a ^ n • y ∈ N

Tactic:
have h : (a ^ n • y ∈ N) = (a ^ (n + n) • y ∈ N) := congr_arg (y ∈ ·) (hn (n + n) le_add_self)

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h✝ : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
x : M
hx : x ∈ N
y : M
x✝ : x + a ^ n • y ∈ f n ⊓ (N + a ^ n • ⊤)
h1 : x + a ^ n • y ∈ ↑(f n)
h : (a ^ n • y ∈ N) = (a ^ (n + n) • y ∈ N)
⊢ x + a ^ n • y ∈ N
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalIso R S
hne : ¬Ideal.span {g | IsStandardOpenImmersion R (Localization.Away g)} = ⊤
⊢ False

Tactic:
obtain ⟨m, hm, hms⟩ := Ideal.exists_le_maximal _ hne

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalIso R S
hne : ¬Ideal.span {g | IsStandardOpenImmersion R (Localization.Away g)} = ⊤
m : Ideal S
hm : m.IsMaximal
hms : Ideal.span {g | IsStandardOpenImmersion R (Localization.Away g)} ≤ m
⊢ False
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h : Ideal.span (Set.range f) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
⊢ IsLocalIso R S

Tactic:
refine ⟨fun q hq ↦ ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h : Ideal.span (Set.range f) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
⊢ ∃ g ∉ q, IsStandardOpenImmersion R (Localization.Away g)
Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
I : Ideal R
x✝¹ : FinitePresentation R ↥I := finitePresentation_of_finite R ↥I
m : Ideal R
x✝ : m.IsMaximal
Rₘ : Type u := Localization.AtPrime m
Mₘ : Type (max u v) := LocalizedModule m.primeCompl M
f : M →ₗ[R] LocalizedModule m.primeCompl M := LocalizedModule.mkLinearMap m.primeCompl M
h : R →ₗ[R] Rₘ := Algebra.linearMap R Rₘ
⊢ Function.Surjective ⇑((LocalizedModule.map m.primeCompl) (LinearMap.lcomp R M (Submodule.subtype I)))

Tactic:
let Iₘ : Ideal Rₘ := Submodule.localized' Rₘ m.primeCompl h I

Goal state after:
R : Type u
inst✝⁴ : CommRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
I : Ideal R
x✝¹ : FinitePresentation R ↥I := finitePresentation_of_finite R ↥I
m : Ideal R
x✝ : m.IsMaximal
Rₘ : Type u := Localization.AtPrime m
Mₘ : Type (max u v) := LocalizedModule m.primeCompl M
f : M →ₗ[R] LocalizedModule m.primeCompl M := LocalizedModule.mkLinearMap m.primeCompl M
h : R →ₗ[R] Rₘ := Algebra.linearMap R Rₘ
Iₘ : Ideal Rₘ := Submodule.localized' Rₘ m.primeCompl h I
⊢ Function.Surjective ⇑((LocalizedModule.map m.primeCompl) (LinearMap.lcomp R M (Submodule.subtype I)))