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

Goal state before:
pp: case refine_1
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ (resFunctor f).map ψ)).τ₁ = (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁

Tactic:
{ simp only [shortComplexH2]
    ext
    simp [Prod.map] }

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

Goal state before:
pp: case refine_2
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ (resFunctor f).map ψ)).τ₂ = (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂

Tactic:
{ simp only [shortComplexH2]
    ext
    simp [Prod.map] }

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

Goal state before:
pp: case refine_3
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ (resFunctor f).map ψ)).τ₃ = (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃

Tactic:
{ simp only [shortComplexH2]
    ext
    simp [Prod.map] }

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

Goal state before:
pp: case mpr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
⊢ ⟨val✝, hx⟩ ∈ selmerGroup.subgroupOf selmerGroup → ⟨val✝, hx⟩ ∈ valuation.ker

Tactic:
· exact fun hx' => funext fun v => hx' v <| Set.notMem_empty v

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

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
hn : n = 0
⊢ 1 = if n = 0 then x✝¹ ^ n else 0

Tactic:
hn,

Goal state after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
hn : n = 0
⊢ 1 = if 0 = 0 then x✝¹ ^ 0 else 0
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
⊢ a ^ n = 0

Tactic:
have h_fac : (n ! : A) * hI.dpow n a = n • ((n - 1)! : A) * hI.dpow n a := by
    rw [nsmul_eq_mul, ← cast_mul, mul_factorial_pred hn]
  rw [← hI.factorial_mul_dpow_eq_pow ha, h_fac, smul_mul_assoc]
  exact hnI (I.mul_mem_left ((n - 1)! : A) (hI.dpow_mem hn ha))

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

Goal state before:
pp: case inl
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n = 0
⊢ dp R n 0 = 1

Tactic:
hn,

Goal state after:
case inl
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n = 0
⊢ dp R 0 0 = 1
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
hn : n = 0
a✝ : A
ha : a✝ ∈ I
⊢ hJ.dpow n (f a✝) = f (hI.dpow n a✝)

Tactic:
hn,

Goal state after:
case pos
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
hn : n = 0
a✝ : A
ha : a✝ ∈ I
⊢ hJ.dpow 0 (f a✝) = f (hI.dpow 0 a✝)
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)
n : ℕ
a : A
ha : a ∈ J
⊢ (if a ∈ J then hI.dpow n a else 0) = hI.dpow n a

Tactic:
if_pos ha

Goal state after:
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)
n : ℕ
a : A
ha : a ∈ J
⊢ hI.dpow n a = hI.dpow n a
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hm : n ≠ 0
hx : x ∈ Ideal.span {↑p}
⊢ ⟨dpow' p n ↑x, ⋯⟩ ∈ Ideal.span {↑p}

Tactic:
have hiff := PadicInt.norm_le_pow_iff_mem_span_pow ⟨dpow' p n x, dpow'_int p n hx⟩ 1
  rw [pow_one] at hiff
  rw [← hiff]
  simp only [cast_one, zpow_neg_one]
  exact dpow'_norm_le_of_ne_zero p hm hx

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
I : Ideal R
inst✝¹ : DecidablePred fun x ↦ x ∈ I
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ x ^ n = ↑n ! * hI.dpow n x

Tactic:
factorial_mul_dpow_eq_pow _ hx

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
I : Ideal R
inst✝¹ : DecidablePred fun x ↦ x ∈ I
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ x ^ n = x ^ n
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x ^ n = 0
⊢ (x ^ n).fst = 0

Tactic:
hn,

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x ^ n = 0
⊢ fst 0 = 0
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case mpr.h1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ (x.fst ^ n) ^ 2 = fst 0

Tactic:
hn,

Goal state after:
case mpr.h1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ 0 ^ 2 = fst 0
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case mpr.h2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ x.fst ^ n • (x ^ n).snd + MulOpposite.op (x.fst ^ n) • (x ^ n).snd = snd 0

Tactic:
hn,

Goal state after:
case mpr.h2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ 0 • (x ^ n).snd + MulOpposite.op 0 • (x ^ n).snd = snd 0
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∉ S
⊢ ↑(⨆ (_ : J ∈ S), ⟨J.carrier, ⋯⟩) = ⨆ (_ : J ∈ S), ↑⟨J.carrier, ⋯⟩

Tactic:
simp [hJ, not_false_eq_true, iSup_neg, Set.Iic.coe_bot]

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

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n = 0
⊢ hI.dpow n 0 = hI'.dpow n 0

Tactic:
hn,

Goal state after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n = 0
⊢ hI.dpow 0 0 = hI'.dpow 0 0
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 : ℕ
a b : A
hb : b ∈ I
hy : f b ∈ J
⊢ dpow hI f n (f a * f b) = f a ^ n * f (hI.dpow n b)

Tactic:
← _root_.map_mul,

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 : ℕ
a b : A
hb : b ∈ I
hy : f b ∈ J
⊢ dpow hI f n (f (a * b)) = f a ^ n * f (hI.dpow n b)
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)
m✝ n✝ : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ f (hI.dpow m✝ a) * f (hI.dpow n✝ a) = ↑((m✝ + n✝).choose m✝) * f (hI.dpow (m✝ + n✝) a)

Tactic:
← _root_.map_mul,

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)
m✝ n✝ : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ f (hI.dpow m✝ a * hI.dpow n✝ a) = ↑((m✝ + n✝).choose m✝) * f (hI.dpow (m✝ + n✝) a)
Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
i j : ι
⊢ Submodule.map₂ (↑(Algebra.lmul S (S ⊗[R] A))) (Submodule.baseChange S (𝒜 i)) (Submodule.baseChange S (𝒜 j)) ≤
    Submodule.baseChange S (𝒜 (i + j))

Tactic:
simp_rw [baseChange_eq_span, map₂_span_span, span_le, Set.image2_subset_iff]

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
i j : ι
⊢ ∀ x ∈ ↑(Submodule.map ((TensorProduct.mk R S A) 1) (𝒜 i)),
    ∀ y ∈ ↑(Submodule.map ((TensorProduct.mk R S A) 1) (𝒜 j)),
      (↑(Algebra.lmul S (S ⊗[R] A)) x) y ∈ ↑(span S ↑(Submodule.map ((TensorProduct.mk R S A) 1) (𝒜 (i + j))))
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d e : ℕ
⊢ (1 - X) ^ (d + e) * ↑(invOneSubPow S e) = (1 - X) ^ d

Tactic:
simp [pow_add, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow S e]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
⊢ ∑ x ∈ VAddAntidiagonal g ⋯, (s a.1).coeff x.1 • (t a.2).coeff x.2 =
    ∑ x ∈ VAddAntidiagonal g ⋯, (s a.1).coeff x.1 • (t a.2).coeff x.2

Tactic:
by
  refine sum_subset (fun gh hgh => ?_) fun gh hgh h => ?_
  · simp_all only [mem_vaddAntidiagonal, Function.mem_support, Set.mem_iUnion, mem_support]
    exact ⟨Exists.intro a.1 hgh.1, Exists.intro a.2 hgh.2.1, trivial⟩
  · by_cases hs : (s a.1).coeff gh.1 = 0
    · exact smul_eq_zero_of_left hs ((t a.2).coeff gh.2)
    · simp_all

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
α : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
x : R⟦Γ⟧
s : SummableFamily Γ' V α
⊢ (x • s).hsum = (of R).symm (x • (of R) s.hsum)

Tactic:
by
  rw [smul_eq, hsum_equiv, smul_hsum, hsum_unique, const_toFun]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
x : PowerSeries R
n : ℕ
⊢ ((ofPowerSeries Γ R) x).coeff ↑n = (PowerSeries.coeff n) x

Tactic:
trans (embDomain (Nat.castOrderEmbedding (α := Γ)) (toPowerSeries.symm x)).coeff
    (Nat.castOrderEmbedding n)

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
x : PowerSeries R
n : ℕ
⊢ ((ofPowerSeries Γ R) x).coeff ↑n =
    (embDomain Nat.castOrderEmbedding (toPowerSeries.symm x)).coeff (Nat.castOrderEmbedding n)

Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
x : PowerSeries R
n : ℕ
⊢ (embDomain Nat.castOrderEmbedding (toPowerSeries.symm x)).coeff (Nat.castOrderEmbedding n) = (PowerSeries.coeff n) x
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h✝ : Nontrivial R
⊢ IsUnit x

Tactic:
· refine isUnit_of_isUnit_leadingCoeff_AddUnitOrder ?_ ?_
    · rw [(x.orderTop_self_sub_one_pos_iff.mp h).2]
      exact isUnit_one
    · have := (x.orderTop_self_sub_one_pos_iff.mp h).1
      rw [← order_eq_orderTop_of_ne_zero
        (fun h ↦ WithTop.top_ne_zero (orderTop_eq_top.mpr h ▸ this)), WithTop.coe_eq_zero] at this
      rw [this]
      exact isAddUnit_zero

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : Ideal R[X]
ism : (comap C p).IsMaximal
ne : p ≠ Ideal.map C (comap C p)
q : Ideal R := ⋯
this✝ : Field (R ⧸ q) := ⋯
ne' : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p ≠ ⊥
y : (R ⧸ q)[X]
mony : y.Monic
hy : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p = span {y}
this : y ∈ lifts (Ideal.Quotient.mk q)
f : R[X]
hf : map (Ideal.Quotient.mk q) f = y
deg : f.natDegree = y.natDegree
monf : f.Monic
⊢ p = comap (mapRingHom (Ideal.Quotient.mk q)) (Ideal.map (mapRingHom (Ideal.Quotient.mk q)) (span {f}))

Tactic:
rw [Ideal.map_span, coe_mapRingHom, Set.image_singleton, hf, ← hy,
      Ideal.comap_map_of_surjective' _ (map_surjective _ Ideal.Quotient.mk_surjective)]
    simpa [Polynomial.ker_mapRingHom, q] using Ideal.map_comap_le

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : Ideal R[X]
ism : (comap C p).IsMaximal
ne : p ≠ Ideal.map C (comap C p)
q : Ideal R := comap C p
this✝ : Field (R ⧸ q) := Quotient.field q
ne' : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p ≠ ⊥
y : (R ⧸ q)[X]
mony : y.Monic
hy : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p = span {y}
this : y ∈ lifts (Ideal.Quotient.mk q)
f : R[X]
hf : map (Ideal.Quotient.mk q) f = y
deg : f.natDegree = y.natDegree
monf : f.Monic
⊢ span {f} ⊔ RingHom.ker (mapRingHom (Ideal.Quotient.mk q)) = Ideal.map C (comap C p) ⊔ span {f}

Tactic:
sup_comm,

Goal state after:
R : Type u_1
inst✝ : CommRing R
p : Ideal R[X]
ism : (comap C p).IsMaximal
ne : p ≠ Ideal.map C (comap C p)
q : Ideal R := comap C p
this✝ : Field (R ⧸ q) := Quotient.field q
ne' : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p ≠ ⊥
y : (R ⧸ q)[X]
mony : y.Monic
hy : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p = span {y}
this : y ∈ lifts (Ideal.Quotient.mk q)
f : R[X]
hf : map (Ideal.Quotient.mk q) f = y
deg : f.natDegree = y.natDegree
monf : f.Monic
⊢ RingHom.ker (mapRingHom (Ideal.Quotient.mk q)) ⊔ span {f} = Ideal.map C (comap C p) ⊔ span {f}
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝³ : p.IsPrime
this✝² : (map f p).IsPrime
h : (map f p).height ≤ 1
h_lt : map f q < map f p
this✝¹ : (map f q).IsPrime
this✝ : (map f p).FiniteHeight
this : (map f q).height < 1
⊢ q ∈ (span t).minimalPrimes

Tactic:
Order.lt_one_iff,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝³ : p.IsPrime
this✝² : (map f p).IsPrime
h : (map f p).height ≤ 1
h_lt : map f q < map f p
this✝¹ : (map f q).IsPrime
this✝ : (map f p).FiniteHeight
this : (map f q).height = 0
⊢ q ∈ (span t).minimalPrimes
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case h.zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
this : p.IsPrime
H :
  ∀ m < 0,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
hn : s.card ≤ 0
⊢ p.height ≤ ↑0

Tactic:
rw [ENat.natCast_zero, nonpos_iff_eq_zero, height_eq_zero_iff, minimalPrimes]

Goal state after:
case h.zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
this : p.IsPrime
H :
  ∀ m < 0,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
hn : s.card ≤ 0
⊢ p ∈ {p | IsMinimalPrime p}
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑(P.diagram.obj H).toProfinite.toTop
a✝ : IsOpen s
⊢ IsOpen (⋃ y ∈ s, QuotientGroup.mk ⁻¹' {y})

Tactic:
refine isOpen_iUnion (fun i ↦ isOpen_iUnion (fun _ ↦ ?_))

Goal state after:
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑(P.diagram.obj H).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
⊢ IsOpen (QuotientGroup.mk ⁻¹' {i})
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case e'_4
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ ↑p.height
hs : (Submodule.generators I).Finite
⊢ ↑(Submodule.spanFinrank I) = Cardinal.toENat (Submodule.spanRank I)

pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ ↑p.height
hs : (Submodule.generators I).Finite
⊢ p.height ≤ Cardinal.toENat (Submodule.spanRank I)

Tactic:
· symm
      simpa [Submodule.fg_iff_spanRank_eq_spanFinrank] using (IsNoetherian.noetherian I)

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ ↑p.height
hs : (Submodule.generators I).Finite
⊢ p.height ≤ Cardinal.toENat (Submodule.spanRank I)
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this✝ : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset
⊢ p ∈ (span ↑o ⊔ span (Submodule.generators I)).minimalPrimes

Tactic:
sup_comm,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this✝ : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset
⊢ p ∈ (span (Submodule.generators I) ⊔ span ↑o).minimalPrimes
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
this✝³ : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (algebraMap R Rₚ) p
this✝² : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (algebraMap R[X] Rₚ[X]) P
disj : Disjoint ↑(Submonoid.map C p.primeCompl) ↑P
eq : under R[X] (Ideal.map (algebraMap R[X] Rₚ[X]) P) = P
this✝¹ : (under R[X] P').IsMaximal
this✝ : P'.IsMaximal
this : P'.LiesOver p'
eq1 : p.height = p'.height
eq2 : P.height = P'.height
⊢ P.height = p'.height + 1

Tactic:
eq2

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
this✝³ : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (algebraMap R Rₚ) p
this✝² : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (algebraMap R[X] Rₚ[X]) P
disj : Disjoint ↑(Submonoid.map C p.primeCompl) ↑P
eq : under R[X] (Ideal.map (algebraMap R[X] Rₚ[X]) P) = P
this✝¹ : (under R[X] P').IsMaximal
this✝ : P'.IsMaximal
this : P'.LiesOver p'
eq1 : p.height = p'.height
eq2 : P.height = P'.height
⊢ P'.height = p'.height + 1
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
ei : EnoughInjectives (ModuleCat R)
I : ModuleCat R
inj : Injective I
f : M ⟶ I
monof : Mono f
S : ShortComplex (ModuleCat R) := { X₁ := M, X₂ := I, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
⊢ HasInjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)

Tactic:
have S_exact : S.ShortExact := { exact := ShortComplex.exact_cokernel f }

Goal state after:
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
ei : EnoughInjectives (ModuleCat R)
I : ModuleCat R
inj : Injective I
f : M ⟶ I
monof : Mono f
S : ShortComplex (ModuleCat R) := { X₁ := M, X₂ := I, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
S_exact : S.ShortExact
⊢ HasInjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: ι : Type u_1
inst✝² : Nontrivial ι
R : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit fun i ↦ if i = i₁ then 0 else 1
hb : ¬IsUnit fun i ↦ if i = i₁ then 1 else 0
x✝ : ι
⊢ ((if x✝ = i₁ then 0 else 1) + if x✝ = i₁ then 1 else 0) = 1

Tactic:
split

Goal state after:
case isTrue
ι : Type u_1
inst✝² : Nontrivial ι
R : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit fun i ↦ if i = i₁ then 0 else 1
hb : ¬IsUnit fun i ↦ if i = i₁ then 1 else 0
x✝ : ι
h✝ : x✝ = i₁
⊢ 0 + 1 = 1

case isFalse
ι : Type u_1
inst✝² : Nontrivial ι
R : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit fun i ↦ if i = i₁ then 0 else 1
hb : ¬IsUnit fun i ↦ if i = i₁ then 1 else 0
x✝ : ι
h✝ : ¬x✝ = i₁
⊢ 1 + 0 = 1