mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ι
⊢ ↑(((decompose 𝒜) (x * y)) i) ∈ Subsemiring.closure s

Tactic:
rw [decompose_mul, DirectSum.mul_eq_dfinsuppSum]

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 : ι
⊢ ↑((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
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 : ι
⊢ ∀ {gi gj : S ⊗[R] A},
    gi ∈ Submodule.baseChange S (𝒜 i) → gj ∈ Submodule.baseChange S (𝒜 j) → gi * gj ∈ Submodule.baseChange S (𝒜 (i + j))

Tactic:
suffices h : ((𝒜 i).baseChange S).map₂ (Algebra.lmul S (S ⊗[R] A)) ((𝒜 j).baseChange S) ≤
      (𝒜 (i + j)).baseChange S from fun xi xj ↦ (h <| apply_mem_map₂ _ · ·)
    simp_rw [baseChange_eq_span, map₂_span_span, span_le, Set.image2_subset_iff]
    rintro - ⟨x, hx, rfl⟩ - ⟨y, hy, rfl⟩
    simpa using subset_span <| Set.mem_image_of_mem _ <| mul_mem_graded hx hy

Goal state after:
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
H : IsArithFrobAt R σ Q
τ : G
x : S
⊢ Ideal.comap ((↑((MulSemiringAction.toRingEquiv G S) τ).symm).comp (algebraMap R S)) Q = Ideal.under R Q

Tactic:
congr 1

Goal state after:
case e_f
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
H : IsArithFrobAt R σ Q
τ : G
x : S
⊢ (↑((MulSemiringAction.toRingEquiv G S) τ).symm).comp (algebraMap R S) = algebraMap R S
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: R : Type u
inst✝² : CommRing R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
k : ℕ
N₁ N₂ : G(k, M; R)
h : N₁.toSubmodule = N₂.toSubmodule
⊢ N₁ = N₂

Tactic:
cases N₁

Goal state after:
case mk
R : Type u
inst✝² : CommRing R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
k : ℕ
N₂ : G(k, M; R)
toSubmodule✝ : Submodule R M
finite_quotient✝ : Module.Finite R (M ⧸ toSubmodule✝)
projective_quotient✝ : Projective R (M ⧸ toSubmodule✝)
rankAtStalk_eq✝ : ∀ (p : PrimeSpectrum R), rankAtStalk (M ⧸ toSubmodule✝) p = k
h :
  { toSubmodule := toSubmodule✝, finite_quotient := finite_quotient✝, projective_quotient := projective_quotient✝,
        rankAtStalk_eq := rankAtStalk_eq✝ }.toSubmodule =
    N₂.toSubmodule
⊢ { toSubmodule := toSubmodule✝, finite_quotient := finite_quotient✝, projective_quotient := projective_quotient✝,
      rankAtStalk_eq := rankAtStalk_eq✝ } =
    N₂
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: case mk.mk
R : Type u
inst✝² : CommRing R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
k : ℕ
toSubmodule✝¹ : Submodule R M
finite_quotient✝¹ : Module.Finite R (M ⧸ toSubmodule✝¹)
projective_quotient✝¹ : Projective R (M ⧸ toSubmodule✝¹)
rankAtStalk_eq✝¹ : ∀ (p : PrimeSpectrum R), rankAtStalk (M ⧸ toSubmodule✝¹) p = k
toSubmodule✝ : Submodule R M
finite_quotient✝ : Module.Finite R (M ⧸ toSubmodule✝)
projective_quotient✝ : Projective R (M ⧸ toSubmodule✝)
rankAtStalk_eq✝ : ∀ (p : PrimeSpectrum R), rankAtStalk (M ⧸ toSubmodule✝) p = k
h :
  { toSubmodule := toSubmodule✝¹, finite_quotient := finite_quotient✝¹, projective_quotient := projective_quotient✝¹,
        rankAtStalk_eq := rankAtStalk_eq✝¹ }.toSubmodule =
    { toSubmodule := toSubmodule✝, finite_quotient := finite_quotient✝, projective_quotient := projective_quotient✝,
        rankAtStalk_eq := rankAtStalk_eq✝ }.toSubmodule
⊢ { toSubmodule := toSubmodule✝¹, finite_quotient := finite_quotient✝¹, projective_quotient := projective_quotient✝¹,
      rankAtStalk_eq := rankAtStalk_eq✝¹ } =
    { toSubmodule := toSubmodule✝, finite_quotient := finite_quotient✝, projective_quotient := projective_quotient✝,
      rankAtStalk_eq := rankAtStalk_eq✝ }

Tactic:
congr 1

Goal state after:
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: case add
R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB : Function.Surjective ⇑fAB
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x✝ : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
hfBC_ker_eq : (map g (map f N)).toSubmodule = fBC.ker
x y : C ⊗[R] M
hx : fAC x = (↑e ∘ₗ fBC) x
hy : fAC y = (↑e ∘ₗ fBC) y
⊢ fAC (x + y) = (↑e ∘ₗ fBC) (x + y)

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d : ℕ
h : 0 < d
⊢ ↑{ val := mk fun n ↦ ↑((d - 1 + n).choose (d - 1)), inv := (1 - X) ^ (d - 1 + 1), val_inv := ⋯, inv_val := ⋯ } =
    mk fun n ↦ ↑((d - 1 + 1 - 1 + n).choose (d - 1 + 1 - 1))

Tactic:
add_tsub_cancel_right

Goal state after:
S : Type u_1
inst✝ : CommRing S
d : ℕ
h : 0 < d
⊢ ↑{ val := mk fun n ↦ ↑((d - 1 + n).choose (d - 1)), inv := (1 - X) ^ (d - 1 + 1), val_inv := ⋯, inv_val := ⋯ } =
    mk fun n ↦ ↑((d - 1 + n).choose (d - 1))
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
hx : 0 < x.orderTop
f : PowerSeries R
n : ℕ
⊢ (powerSeriesFamily x f) n = (PowerSeries.coeff n) f • x ^ n

Tactic:
by
  simp [hx]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
aux₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain aux₂ := HasSubst.cons_subst_zero_right (f := X₀ + X₁) (0 : Fin 3) 1 2 (by simp)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
aux₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
aux₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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✝ : AddCommMonoid R
x y : SummableFamily Γ R α
g : Γ
a : α
ha : (x a).coeff g = 0 ∧ (y a).coeff g = 0
⊢ 0 + 0 = 0

Tactic:
add_zero

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x y : SummableFamily Γ R α
g : Γ
a : α
ha : (x a).coeff g = 0 ∧ (y a).coeff g = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding

Goal state before:
pp: M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective ⇑f₁
hf₁class :
  ∀ (a : M), ArchimedeanClass.mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (f₁ a))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' : StrictMono ⇑f₂'
hf₂class' :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂' a)).orderTop
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
hf₂ : Function.Injective ⇑f₂
hf₂class :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂ a)).orderTop
f₃ : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ →+o Lex ℝ⟦FiniteArchimedeanClass M⟧ :=
  embDomainOrderAddMonoidHom
    (RelIso.toRelEmbedding (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M).symm))
hf₃ : Function.Injective ⇑f₃
a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
⊢ (ofLex a).orderTop =
    (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M)).withTopCongr
      (ofLex (f₃ a)).orderTop

Tactic:
← OrderIso.symm_apply_eq

Goal state after:
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective ⇑f₁
hf₁class :
  ∀ (a : M), ArchimedeanClass.mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (f₁ a))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' : StrictMono ⇑f₂'
hf₂class' :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂' a)).orderTop
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
hf₂ : Function.Injective ⇑f₂
hf₂class :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂ a)).orderTop
f₃ : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ →+o Lex ℝ⟦FiniteArchimedeanClass M⟧ :=
  embDomainOrderAddMonoidHom
    (RelIso.toRelEmbedding (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M).symm))
hf₃ : Function.Injective ⇑f₃
a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
⊢ (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M)).withTopCongr.symm
      (ofLex a).orderTop =
    (ofLex (f₃ a)).orderTop
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : x = 0
⊢ {a | ((fun n ↦ x ^ n) a).coeff g ≠ 0}.Finite

Tactic:
exact h0 ▸ Set.Finite.subset (Set.finite_singleton 0) (co_support_zero g)

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 : 0 < x.orderTop
n : ℕ
⊢ (powers x) n = x ^ n

Tactic:
by
  simp [hx]

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m : ℕ
⊢ c m ≡ c (m + 0) [SMOD I ^ m]

Tactic:
add_zero

Goal state after:
case zero
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m : ℕ
⊢ c m ≡ c m [SMOD I ^ m]
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
⊢ a = b

Tactic:
obtain ⟨c, _⟩ := exists_mul_sq_add_linear_part_eq_eval_add f a (b - a)
  have hc : (c * (b - a) + eval a (derivative f)) * (b - a) = 0 := by grind
  suffices (c * (b - a) + eval a (derivative f)) ∉ maximalIdeal R by
    rw [notMem_maximalIdeal, isUnit_iff_exists] at this
    grind
  by_contra!
  replace this := (maximalIdeal R).add_mem this ((maximalIdeal R).mul_mem_left c h)
  ring_nf at this
  contradiction

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

Goal state before:
pp: case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsNoetherianRing R
x : R
hx : Prime x
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
this✝ : IsDomain S
x✝ : UniqueFactorizationMonoid S
p : Ideal R
hp : p.IsPrime
h1 : p.height = 1
hxp : x ∉ p
hd : Disjoint ↑(Submonoid.powers x) ↑p
this : (Ideal.map (algebraMap R S) p).IsPrime
⊢ (Ideal.under R (Ideal.map (algebraMap R S) p)).height = 1

Tactic:
IsLocalization.under_map_of_isPrime_disjoint (Submonoid.powers x) S hp hd,

Goal state after:
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsNoetherianRing R
x : R
hx : Prime x
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
this✝ : IsDomain S
x✝ : UniqueFactorizationMonoid S
p : Ideal R
hp : p.IsPrime
h1 : p.height = 1
hxp : x ∉ p
hd : Disjoint ↑(Submonoid.powers x) ↑p
this : (Ideal.map (algebraMap R S) p).IsPrime
⊢ p.height = 1
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
⊢ ↑(Submodule.spanFinrank I) = Cardinal.toENat (Submodule.spanRank I)

Tactic:
Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I),

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
⊢ ↑(Submodule.spanFinrank I) = Cardinal.toENat ↑(Submodule.spanFinrank 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'
x : R
hx : (Quotient.mk I) x ∈ ↑p'
⊢ x ∈ ↑p ∧ (Quotient.mk I) x = (Quotient.mk I) x

Tactic:
simpa [hrp, sup_of_le_left, p'] using hx

Goal state after:
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
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
n : ℕ
a✝ b✝ : M
hx : a✝ ∈ {x | a ^ n • x ∈ N}
hy : b✝ ∈ {x | a ^ n • x ∈ N}
⊢ a✝ + b✝ ∈ {x | a ^ n • x ∈ N}

Tactic:
by simp [N.add_mem hx hy]

Goal state after:
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro.h
n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ ⟨y, hy⟩ ∈ ⊤

pp: n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ card ↥R < n

Tactic:
· trivial

Goal state after:
n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ card ↥R < n
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
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
a : ↥S
g' : R →ₗ[R] M
e :
  ↑a • g =
    (mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
      ((LinearMap.lcomp R M I.subtype) g', a).1
⊢ ((algebraMap Rₛ (End Rₛ (↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ))) ((algebraMap R Rₛ) ↑a))
      ((LinearMap.lcomp Rₛ Mₛ (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I).subtype)
        (IsLocalization.mk' Rₛ 1 a • (mapExtendScalars S (Algebra.linearMap R Rₛ) f Rₛ) g')) =
    ((algebraMap Rₛ (End Rₛ (↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)))
        ((algebraMap R Rₛ) ↑a))
      g

Tactic:
algebraMap_end_apply,

Goal state after:
R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
a : ↥S
g' : R →ₗ[R] M
e :
  ↑a • g =
    (mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
      ((LinearMap.lcomp R M I.subtype) g', a).1
⊢ (algebraMap R Rₛ) ↑a •
      (LinearMap.lcomp Rₛ Mₛ (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I).subtype)
        (IsLocalization.mk' Rₛ 1 a • (mapExtendScalars S (Algebra.linearMap R Rₛ) f Rₛ) g') =
    (algebraMap R Rₛ) ↑a • g
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
⊢ R[β] = ⊤ → (ResidueField R)[(residue S) β] = ⊤

Tactic:
· intro hβ_gen
    rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
    intro x
    obtain ⟨s, rfl⟩ := residue_surjective (R := S) x
    obtain ⟨p, rfl⟩ := hβ_gen s
    exact ⟨p.map (residue R), by
      rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl p β]⟩

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
⊢ ((single (order x)) 1 * (ofPowerSeries ℤ R) x.powerSeriesPart).coeff n = x.coeff n

Tactic:
rw [← sub_add_cancel n x.order, coeff_single_mul_add, sub_add_cancel, one_mul]

Goal state after:
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
⊢ ((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff n
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R⟦X⟧
⊢ (algebraMap R⟦X⟧ R⸨X⸩) x = (algebraMap R⟦X⟧ R⸨X⸩) y → ∃ c, ↑c * x = ↑c * y

Tactic:
coe_algebraMap,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R⟦X⟧
⊢ (ofPowerSeries ℤ R) x = (ofPowerSeries ℤ R) y → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
i : ℤ
⊢ ((ofPowerSeries ℤ R) f).coeff i = if i < 0 then 0 else (coeff i.natAbs) f

Tactic:
cases i
  · rw [Int.ofNat_eq_natCast, coeff_coe_powerSeries, if_neg (Int.natCast_nonneg _).not_gt,
      Int.natAbs_natCast]
  · rw [ofPowerSeries_apply, embDomain_notin_image_support, if_pos (Int.negSucc_lt_zero _)]
    simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⟮X⟯
⊢ Valued.v ((algebraMap K⟮X⟯ K⸨X⸩) f) = Valued.v f

Tactic:
simp [adicValued_apply, ← valuation_eq_LaurentSeries_valuation]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case e'_3.e'_6.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a✝ : Fin n
⊢ a✝ ∈ {x | i + 1 ≤ ↑x} ↔ a✝ ∈ {x | i ≤ ↑x}.erase ⟨i, hin⟩

Tactic:
rw [mem_erase]

Goal state after:
case e'_3.e'_6.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a✝ : Fin n
⊢ a✝ ∈ {x | i + 1 ≤ ↑x} ↔ a✝ ≠ ⟨i, hin⟩ ∧ a✝ ∈ {x | i ≤ ↑x}
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
⊢ Antitone ⇑(ofLex (supDegree (⇑toLex) p))

Tactic:
rw [Antitone]

Goal state after:
case inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
⊢ ∀ ⦃a b : σ⦄, a ≤ b → (ofLex (supDegree (⇑toLex) p)) b ≤ (ofLex (supDegree (⇑toLex) p)) a