mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: 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
C : Type u_3
inst✝ : CommSemiring C
K : Ideal C
hK : DividedPowers K
f : A →+* B
g : B →+* C
hg : hJ.IsDPMorphism hK g
hf : hI.IsDPMorphism hJ f
⊢ hI.IsDPMorphism hK (g.comp f)

Tactic:
refine ⟨le_trans (map_map f g ▸ map_mono hf.1) hg.1, fun a ha ↦ ?_⟩
  simp only [RingHom.coe_comp, Function.comp_apply]
  rw [← hf.2 a ha, hg.2]
  exact hf.1 (mem_map_of_mem f ha)

Goal state after:
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
| IsWeaklyRegular M as

Tactic:
rw [isWeaklyRegular_iff_Fin]

Goal state after:
case a
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
| ∀ (i : Fin as.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take (↑i) as) • ⊤) as[i]
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case b
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
| IsWeaklyRegular M₂ bs

Tactic:
rw [isWeaklyRegular_iff_Fin]

Goal state after:
case b
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
| ∀ (i : Fin bs.length), IsSMulRegular (M₂ ⧸ Ideal.ofList (List.take (↑i) bs) • ⊤) bs[i]
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
n : ℕ
u v : M
⊢ hI.dpow (n, u + v).1 (g (n, u + v).2) =
    ∑ x ∈ antidiagonal n,
      match x with
      | (k, l) => hI.dpow (k, u).1 (g (k, u).2) * hI.dpow (l, v).1 (g (l, v).2)

Tactic:
by simp [hI.dpow_add (hg u) (hg v)]

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(map R f)

Tactic:
by
  rw [← AlgHom.range_eq_top, ← Algebra.map_top (map R f), eq_top_iff,
    ← (AlgHom.range_eq_top (RingCon.mkₐ R (ringCon R N))).mpr mkAlgHom_surjective,
    ← Algebra.map_top, (Subalgebra.gc_map_comap _).le_iff_le, ← MvPolynomial.adjoin_range_X,
    Algebra.adjoin_le_iff]
  intro
  simp only [Set.mem_range, Prod.exists]
  rintro ⟨n, m, rfl⟩
  obtain ⟨l, rfl⟩ := hf m
  simp only [Algebra.map_top, Subalgebra.coe_comap, AlgHom.coe_range, Set.mem_preimage,
    Set.mem_range, RingCon.mkₐ_apply]
  use dp R n l
  rw [map_apply_dp, dp]

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

Goal state before:
pp: case hS'
A : Type u_3
B : Type u_4
C : Type u_5
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
⊢ ∀ s ∈ ⇑f '' ↑I, g s ∈ K

Tactic:
rintro b ⟨a, ha, rfl⟩
    rw [← RingHom.comp_apply]
    exact hh.1 (mem_map_of_mem _ ha)

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n✝ : ℕ
x✝ : B
hx : x✝ ∉ J
⊢ e (hI.dpow n✝ (e.symm x✝)) = 0

Tactic:
rw [EmbeddingLike.map_eq_zero_iff, hI.dpow_null]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n✝ : ℕ
x✝ : B
hx : x✝ ∉ J
⊢ e.symm x✝ ∉ I
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case pos
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ ha : a ∈ I
⊢ hI'.dpow n a = hI.dpow n a

Tactic:
refine hI.dpow_comp_from_gens hI' (f := RingHom.id A) hS ?_ ?_ a ha

Goal state after:
case pos.refine_1
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ ha : a ∈ I
⊢ ∀ s ∈ S, (RingHom.id A) s ∈ I

case pos.refine_2
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ ha : a ∈ I
⊢ ∀ {n : ℕ}, ∀ a ∈ S, (RingHom.id A) (hI.dpow n a) = hI'.dpow n ((RingHom.id A) a)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n✝ : ℕ
a✝ x✝ : B
hx : x✝ ∈ J
⊢ e (hI.dpow n✝ (e.symm (a✝ * x✝))) = a✝ ^ n✝ * e (hI.dpow n✝ (e.symm x✝))

Tactic:
by
    simp only [map_mul]
    rw [hI.dpow_mul (symm_apply_mem_of_equiv_iff.mpr (h ▸ hx))]
    rw [map_mul, map_pow]
    simp only [RingEquiv.apply_symm_apply]

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

Goal state before:
pp: case hc
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n m : ℕ
x : A
hm : m ≠ 0
hx : x ∈ I
⊢ ⋯.choose ∈ I

Tactic:
exact (Exists.choose_spec (hmem m hx)).1 hm

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
⊢ hJ.IsSubDPIdeal (Ideal.map f K)

Tactic:
by
  rw [Ideal.map, span_isSubDPIdeal_iff]
  · rintro n hn y ⟨x, hx, rfl⟩
    exact hf.2 x (hK.1 hx) ▸ mem_map_of_mem _ (hK.2 _ hn hx)
  · rintro y ⟨x, hx, rfl⟩
    exact hf.1 (mem_map_of_mem f (hK.1 hx))

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
⊢ ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x

Tactic:
intro x hxI hx0

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
x : K[ε]
hxI : x ∈ I
hx0 : x ≠ 0
⊢ ∃ r, ε = r * x
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
h : (fun J ↦ ⟨J.carrier, ⋯⟩) J = (fun J ↦ ⟨J.carrier, ⋯⟩) J'
⊢ J = J'

Tactic:
by simpa only [SubDPIdeal.ext_iff, Subtype.mk.injEq] using h

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: 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
inst✝ : IsFiniteSplit k R
p : PrimeSpectrum R
⊢ Ideal.comap (Ideal.Quotient.mkₐ k p.asIdeal) (RingHom.ker ↑↑(AlgEquiv.ofBijective (ofId k (R ⧸ p.asIdeal)) ⋯).symm) =
    p.asIdeal

Tactic:
AlgEquiv.toAlgHom_toRingHom,

Goal state after:
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
inst✝ : IsFiniteSplit k R
p : PrimeSpectrum R
⊢ Ideal.comap (Ideal.Quotient.mkₐ k p.asIdeal) (RingHom.ker ↑(AlgEquiv.ofBijective (ofId k (R ⧸ p.asIdeal)) ⋯).symm) =
    p.asIdeal
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case mul
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x✝ x y : A
hx✝ : x ∈ Subsemiring.closure s
hy✝ : y ∈ Subsemiring.closure s
h₁ : ∀ (i : ι), ↑(((decompose 𝒜) x) i) ∈ Subsemiring.closure s
h₂ : ∀ (i : ι), ↑(((decompose 𝒜) y) i) ∈ Subsemiring.closure s
i : ι
⊢ ↑((DFinsupp.sum ((decompose 𝒜) x) fun x ai ↦
          DFinsupp.sum ((decompose 𝒜) y) fun x_1 aj ↦ (of (fun i ↦ ↥(𝒜 i)) (x + x_1)) (GradedMonoid.GMul.mul ai aj))
        i) ∈
    Subsemiring.closure s

Tactic:
rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]

Goal state after:
case mul
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x✝ x y : A
hx✝ : x ∈ Subsemiring.closure s
hy✝ : y ∈ Subsemiring.closure s
h₁ : ∀ (i : ι), ↑(((decompose 𝒜) x) i) ∈ Subsemiring.closure s
h₂ : ∀ (i : ι), ↑(((decompose 𝒜) y) i) ∈ Subsemiring.closure s
i : ι
⊢ ∑ i_1 ∈ DFinsupp.support ((decompose 𝒜) x),
      ↑((DFinsupp.sum ((decompose 𝒜) y) fun x_1 aj ↦
            (of (fun i ↦ ↥(𝒜 i)) (i_1 + x_1)) (GradedMonoid.GMul.mul (((decompose 𝒜) x) i_1) aj))
          i) ∈
    Subsemiring.closure s
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case mul
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x✝¹ x y : A
hx✝ : x ∈ Subsemiring.closure s
hy✝ : y ∈ Subsemiring.closure s
h₁ : ∀ (i : ι), ↑(((decompose 𝒜) x) i) ∈ Subsemiring.closure s
h₂ : ∀ (i : ι), ↑(((decompose 𝒜) y) i) ∈ Subsemiring.closure s
i j : ι
x✝ : j ∈ DFinsupp.support ((decompose 𝒜) x)
⊢ ↑((DFinsupp.sum ((decompose 𝒜) y) fun x_1 aj ↦
          (of (fun i ↦ ↥(𝒜 i)) (j + x_1)) (GradedMonoid.GMul.mul (((decompose 𝒜) x) j) aj))
        i) ∈
    Subsemiring.closure s

Tactic:
rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]

Goal state after:
case mul
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x✝¹ x y : A
hx✝ : x ∈ Subsemiring.closure s
hy✝ : y ∈ Subsemiring.closure s
h₁ : ∀ (i : ι), ↑(((decompose 𝒜) x) i) ∈ Subsemiring.closure s
h₂ : ∀ (i : ι), ↑(((decompose 𝒜) y) i) ∈ Subsemiring.closure s
i j : ι
x✝ : j ∈ DFinsupp.support ((decompose 𝒜) x)
⊢ ∑ i_1 ∈ DFinsupp.support ((decompose 𝒜) y),
      ↑(((of (fun i ↦ ↥(𝒜 i)) (j + i_1)) (GradedMonoid.GMul.mul (((decompose 𝒜) x) j) (((decompose 𝒜) y) i_1))) i) ∈
    Subsemiring.closure s
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
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
x : Localization.AtPrime Q
⊢ (Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q))) (H.localize x) =
    (Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q))) (H'.localize x)

Tactic:
rw [H.isArithFrobAt_localize.mk_apply, H'.isArithFrobAt_localize.mk_apply]

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

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ Units.mkOfMulEqOne (1 - X) (mk 1) ⋯ ^ (d + 1) * invOneSubPow S (d + 1) = 1

Tactic:
rw [← Units.val_eq_one, Units.val_mul, Units.val_pow_eq_pow_val]
        exact (invOneSubPow S (d + 1)).inv_val

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

Goal state before:
pp: case succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑↑(↑n).negOnePow * ↑((d + n).choose n) = ↑((↑n).negOnePow • Ring.choose (↑d + 1 + ↑n - 1) n)

Tactic:
Units.smul_def,

Goal state after:
case succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑↑(↑n).negOnePow * ↑((d + n).choose n) = ↑(↑(↑n).negOnePow • Ring.choose (↑d + 1 + ↑n - 1) n)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case refine_2
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
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
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal g ⋯
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

Tactic:
by_cases h : s.hsum.coeff gh.1 = 0

Goal state after:
case pos
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
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
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal g ⋯
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
h : s.hsum.coeff gh.1 = 0
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

case neg
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
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
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal g ⋯
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
h : ¬s.hsum.coeff gh.1 = 0
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
a : α
⊢ (s.embDomain f) (f a) = s a

Tactic:
by
  rw [embDomain_apply, dif_pos (Set.mem_range_self a)]
  exact congr rfl (f.injective (Classical.choose_spec (Set.mem_range_self a)))

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingUp R S
l : LTSeries (PrimeSpectrum R)
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver (RelSeries.head l).asIdeal
⊢ ∃ L,
    L.length = l.length ∧
      RelSeries.head L = { asIdeal := P, isPrime := ⋯ } ∧
        List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = RelSeries.toList l

Tactic:
induction l using RelSeries.inductionOn generalizing P with

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.Pure
inst✝ : J.Pure
⊢ zeroLocus ↑I = zeroLocus ↑J ↔ I = J

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ rfl⟩
  rw [← I.ker_piRingHom_atPrime_eq_of_pure, ← J.ker_piRingHom_atPrime_eq_of_pure]
  generalize hs : zeroLocus (I : Set R) = s
  generalize ht : zeroLocus (J : Set R) = t
  obtain rfl : s = t := by rw [← hs, ← ht, h]
  rfl

Goal state after:
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
h : p.height ≤ ↑t.card
⊢ p.height ≤ (map (Quotient.mk I) p).height + ↑(Submodule.spanFinrank I)

Tactic:
refine le_trans h (hs ▸ ?_)

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
h : p.height ≤ ↑t.card
⊢ ↑t.card ≤ ↑s.card + ↑(Submodule.spanFinrank I)
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
⊢ P.height = p.height + 1

Tactic:
have : (P'.under R[X]).IsMaximal := eq.symm ▸ ‹P.IsMaximal›

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
⊢ P.height = p.height + 1
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
⊢ False

Tactic:
have h : (e ⟨q, le_sup_left.trans hq.1.2⟩).1.height ≤ 1 :=
    map_height_le_one_of_mem_minimalPrimes hq

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
h : (e ⟨q, ⋯⟩).asIdeal.height ≤ 1
⊢ False
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
h : x ∈ (annihilator R M).jacobson
a✝ : Nontrivial M
p : LTSeries ↑(support R M)
hxp : x ∈ (↑(RelSeries.last p)).asIdeal
q : LTSeries (PrimeSpectrum R)
hxq : x ∈ (q.toFun 1).asIdeal
hq : (p.map Subtype.val ⋯).length = q.length
h0 : ↑(RelSeries.head p) = RelSeries.head q
right✝ : RelSeries.last (p.map Subtype.val ⋯) = RelSeries.last q
hp0 : ¬p.length = 0
⊢ Fin (p.length - 1 + 1) → ↑(support R (QuotSMulTop x M))

Tactic:
intro ⟨i, hi⟩

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
h : x ∈ (annihilator R M).jacobson
a✝ : Nontrivial M
p : LTSeries ↑(support R M)
hxp : x ∈ (↑(RelSeries.last p)).asIdeal
q : LTSeries (PrimeSpectrum R)
hxq : x ∈ (q.toFun 1).asIdeal
hq : (p.map Subtype.val ⋯).length = q.length
h0 : ↑(RelSeries.head p) = RelSeries.head q
right✝ : RelSeries.last (p.map Subtype.val ⋯) = RelSeries.last q
hp0 : ¬p.length = 0
i : ℕ
hi : i < p.length - 1 + 1
⊢ ↑(support R (QuotSMulTop x M))
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → CommRing (S i)
inst✝² : (i : ι) → Algebra R (S i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsLocalIso R (S i)
⊢ IsLocalIso R ((i : ι) → S i)

Tactic:
let (i : ι) : Algebra (∀ i, S i) (S i) := (Pi.evalAlgHom R S i).toAlgebra

Goal state after:
ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → CommRing (S i)
inst✝² : (i : ι) → Algebra R (S i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsLocalIso R (S i)
this : (i : ι) → Algebra ((i : ι) → S i) (S i) := fun i ↦ (Pi.evalAlgHom R S i).toAlgebra
⊢ IsLocalIso R ((i : ι) → S i)
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case zero
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
⊢ HasProjectiveDimensionLE M 0 ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) 0

Tactic:
simp only [HasProjectiveDimensionLE, zero_add, ← projective_iff_hasProjectiveDimensionLT_one]

Goal state after:
case zero
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
⊢ Projective M ↔ ∀ (m : MaximalSpectrum R), Projective (M.localizedModule m.asIdeal.primeCompl)
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

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) [Module.Finite R ↑M],
    HasProjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
inst✝ : Module.Finite R ↑M
P : Type v
w✝³ : AddCommGroup P
w✝² : Module R P
w✝¹ : Module.Free R P
w✝ : Module.Finite R P
f : P →ₗ[R] ↑M
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
⊢ HasProjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)

Tactic:
have S_exact := LinearMap.shortExact_shortComplexKer surjf

Goal state after:
case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    HasProjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
inst✝ : Module.Finite R ↑M
P : Type v
w✝³ : AddCommGroup P
w✝² : Module R P
w✝¹ : Module.Free R P
w✝ : Module.Finite R P
f : P →ₗ[R] ↑M
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
S_exact : f.shortComplexKer.ShortExact
⊢ HasProjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)