mathlib-initiative/mathlib-tactics huggingface dataset:
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ₘ
Iₘ : Ideal Rₘ := Submodule.localized' Rₘ m.primeCompl h I
g : ↥I →ₗ[R] ↥Iₘ := Submodule.toLocalized' Rₘ m.primeCompl h I
gM : (↥I →ₗ[R] M) →ₗ[R] ↥Iₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl g f Rₘ
hM : (R →ₗ[R] M) →ₗ[R] Rₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl h f Rₘ
⊢ ↑R (Submodule.subtype Iₘ) ∘ₗ g = (IsLocalizedModule.map m.primeCompl g h) (Submodule.subtype I) ∘ₗ g

Tactic:
ext

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
g : ↥I →ₗ[R] ↥Iₘ := Submodule.toLocalized' Rₘ m.primeCompl h I
gM : (↥I →ₗ[R] M) →ₗ[R] ↥Iₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl g f Rₘ
hM : (R →ₗ[R] M) →ₗ[R] Rₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl h f Rₘ
x✝ : ↥I
⊢ (↑R (Submodule.subtype Iₘ) ∘ₗ g) x✝ = ((IsLocalizedModule.map m.primeCompl g h) (Submodule.subtype I) ∘ₗ g) x✝
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ₘ
Iₘ : Ideal Rₘ := Submodule.localized' Rₘ m.primeCompl h I
g : ↥I →ₗ[R] ↥Iₘ := Submodule.toLocalized' Rₘ m.primeCompl h I
gM : (↥I →ₗ[R] M) →ₗ[R] ↥Iₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl g f Rₘ
hM : (R →ₗ[R] M) →ₗ[R] Rₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl h f Rₘ
eq'' : ↑R (Submodule.subtype Iₘ) = (IsLocalizedModule.map m.primeCompl g h) (Submodule.subtype I)
l : R →ₗ[R] M
⊢ ↑R ((↑R (LinearMap.lcomp Rₘ Mₘ (Submodule.subtype Iₘ)) ∘ₗ hM) l) ∘ₗ g =
    ↑R (((IsLocalizedModule.map m.primeCompl hM gM) (LinearMap.lcomp R M (Submodule.subtype I)) ∘ₗ hM) l) ∘ₗ g

Tactic:
ext

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
g : ↥I →ₗ[R] ↥Iₘ := Submodule.toLocalized' Rₘ m.primeCompl h I
gM : (↥I →ₗ[R] M) →ₗ[R] ↥Iₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl g f Rₘ
hM : (R →ₗ[R] M) →ₗ[R] Rₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl h f Rₘ
eq'' : ↑R (Submodule.subtype Iₘ) = (IsLocalizedModule.map m.primeCompl g h) (Submodule.subtype I)
l : R →ₗ[R] M
x✝ : ↥I
⊢ (↑R ((↑R (LinearMap.lcomp Rₘ Mₘ (Submodule.subtype Iₘ)) ∘ₗ hM) l) ∘ₗ g) x✝ =
    (↑R (((IsLocalizedModule.map m.primeCompl hM gM) (LinearMap.lcomp R M (Submodule.subtype I)) ∘ₗ hM) l) ∘ₗ g) x✝
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
n : ℕ
⊢ injectiveDimension M ≤ ↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n

Tactic:
simp only [injectiveDimension_le_iff, iSup_le_iff]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
n : ℕ
⊢ HasInjectiveDimensionLE M n ↔
    ∀ (i : PrimeSpectrum R), HasInjectiveDimensionLE (M.localizedModule i.asIdeal.primeCompl) n
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
n : ℕ
⊢ injectiveDimension M ≤ ↑n ↔ ⨆ m, injectiveDimension (M.localizedModule m.asIdeal.primeCompl) ≤ ↑n

Tactic:
simp only [injectiveDimension_le_iff, iSup_le_iff]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
n : ℕ
⊢ HasInjectiveDimensionLE M n ↔
    ∀ (i : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule i.asIdeal.primeCompl) n
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: 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
⊢ (ResidueField R)[(residue S) β] = ⊤ ↔ R[β] = ⊤

Tactic:
constructor

Goal state after:
case mp
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
⊢ (ResidueField R)[(residue S) β] = ⊤ → R[β] = ⊤

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) β] = ⊤
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u
inst✝¹⁰ : Group G
inst✝⁹ : MulSemiringAction G B
inst✝⁸ : SMulCommClass G A B
P✝ : Ideal A
inst✝⁷ : TopologicalSpace G
inst✝⁶ : CompactSpace G
inst✝⁵ : TotallyDisconnectedSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : TopologicalSpace B
inst✝² : DiscreteTopology B
inst✝¹ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝ : Q.LiesOver P
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
N N' : OpenNormalSubgroup G
i : N ⟶ N'
x :
  { σ' //
    (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).subtype ⋯;
          { toRingHom := __RingHom, commutes' := ⋯ }).comp
        ↑((stabilizerHom (under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q) P (G ⧸ ↑N.toOpenSubgroup)) σ') =
      (↑σ).comp
        (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).subtype ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ }) }
⊢ (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup).subtype ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ }).comp
      ↑((stabilizerHom (under (↥(FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup)) Q) P (G ⧸ ↑N'.toOpenSubgroup))
          ⟨(QuotientGroup.map (↑N.toOpenSubgroup) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑x, ⋯⟩) =
    (↑σ).comp
      (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup).subtype ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ })

Tactic:
have h : FixedPoints.subalgebra A B N'.1.1 ≤ FixedPoints.subalgebra A B N.1.1 :=
      fun x hx n ↦ hx ⟨_, i.le n.2⟩
    obtain ⟨⟨x, hx⟩, hx'⟩ := x
    obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x
    ext g
    obtain ⟨g, rfl⟩ := Ideal.Quotient.mk_surjective g
    exact DFunLike.congr_fun hx' (Ideal.Quotient.mk _ (Subalgebra.inclusion h g))

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R✝ : Type u_1
R : Type u_2
V : Type u_3
inst✝² : AddCommGroup V
inst✝¹ : Semiring R
inst✝ : Module R V
k : ℕ
f g : V⸨X⸩
⊢ ofSuppBddBelow (fun n ↦ Ring.choose (n + ↑k) k • (f + g).coeff (n + ↑k)) ⋯ =
    ofSuppBddBelow (fun n ↦ Ring.choose (n + ↑k) k • f.coeff (n + ↑k)) ⋯ +
      ofSuppBddBelow (fun n ↦ Ring.choose (n + ↑k) k • g.coeff (n + ↑k)) ⋯

Tactic:
ext

Goal state after:
R✝ : Type u_1
R : Type u_2
V : Type u_3
inst✝² : AddCommGroup V
inst✝¹ : Semiring R
inst✝ : Module R V
k : ℕ
f g : V⸨X⸩
x✝ : ℤ
⊢ (ofSuppBddBelow (fun n ↦ Ring.choose (n + ↑k) k • (f + g).coeff (n + ↑k)) ⋯).coeff x✝ =
    (ofSuppBddBelow (fun n ↦ Ring.choose (n + ↑k) k • f.coeff (n + ↑k)) ⋯ +
          ofSuppBddBelow (fun n ↦ Ring.choose (n + ↑k) k • g.coeff (n + ↑k)) ⋯).coeff
      x✝
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R✝ : Type u_1
R : Type u_2
V : Type u_3
inst✝² : AddCommGroup V
inst✝¹ : Semiring R
inst✝ : Module R V
k : ℕ
r : R
f : V⸨X⸩
⊢ ofSuppBddBelow (fun n ↦ Ring.choose (n + ↑k) k • (r • f).coeff (n + ↑k)) ⋯ =
    (RingHom.id R) r • ofSuppBddBelow (fun n ↦ Ring.choose (n + ↑k) k • f.coeff (n + ↑k)) ⋯

Tactic:
ext

Goal state after:
R✝ : Type u_1
R : Type u_2
V : Type u_3
inst✝² : AddCommGroup V
inst✝¹ : Semiring R
inst✝ : Module R V
k : ℕ
r : R
f : V⸨X⸩
x✝ : ℤ
⊢ (ofSuppBddBelow (fun n ↦ Ring.choose (n + ↑k) k • (r • f).coeff (n + ↑k)) ⋯).coeff x✝ =
    ((RingHom.id R) r • ofSuppBddBelow (fun n ↦ Ring.choose (n + ↑k) k • f.coeff (n + ↑k)) ⋯).coeff x✝
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
⊢ ((fun i ↦ if i = i₁ then 0 else 1) + fun i ↦ if i = i₁ then 1 else 0) = 1

Tactic:
ext

Goal state after:
ι : 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✝ : ι
⊢ ((fun i ↦ if i = i₁ then 0 else 1) + fun i ↦ if i = i₁ then 1 else 0) x✝ = 1 x✝
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ powerSeriesPart 0 = 0

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
n✝ : ℕ
⊢ (PowerSeries.coeff n✝) (powerSeriesPart 0) = (PowerSeries.coeff n✝) 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x.powerSeriesPart = 0 ↔ x = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x.powerSeriesPart = 0 → x = 0

case mpr
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x = 0 → x.powerSeriesPart = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
S : Type u_3
inst✝¹ : Semiring S
inst✝ : Module R S
r : R
x : S⟦X⟧
⊢ (ofPowerSeries ℤ S) (r • x) = r • (ofPowerSeries ℤ S) x

Tactic:
ext

Goal state after:
R : Type u_1
inst✝² : Semiring R
S : Type u_3
inst✝¹ : Semiring S
inst✝ : Module R S
r : R
x : S⟦X⟧
x✝ : ℤ
⊢ ((ofPowerSeries ℤ S) (r • x)).coeff x✝ = (r • (ofPowerSeries ℤ S) x).coeff x✝
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
⊢ f.coeff n = 0

Tactic:
obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat ord_nonpos
    obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (neg_le_iff_add_nonneg.mp (hs ▸ h_n_ord))
    obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le (a := D + s) (by lia)
    rw [eq_add_neg_of_add_eq hm, add_comm, ← hs, ← powerSeriesPart_coeff]
    apply (intValuation_le_iff_coeff_lt_eq_zero K F).mp _ m (by linarith)
    rw [hF, ofPowerSeries_powerSeriesPart f, hs, neg_neg, ← hd, neg_add_rev, exp_add, map_mul,
      ← ofPowerSeries_X_pow s, PowerSeries.coe_pow, valuation_X_pow K s]
    gcongr

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case refine_4
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h✝ : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
r : R
p : MvPolynomial σ R
x✝ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h : IsWeightedHomogeneous w ((pderiv i) p) n'
⊢ IsWeightedHomogeneous w ((pderiv i) (r • p)) n'

Tactic:
· rw [(pderiv i).map_smul]; exact (weightedHomogeneousSubmodule ..).smul_mem _ h

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : MvPolynomial n R
i : n
hf0 : f ≠ 0
hif : i ∉ f.vars
hig : i ∉ g.vars
h : IsRelPrime f g
S : Type (max u_4 u_3) := MvPolynomial { j // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  (renameEquiv R (Equiv.optionSubtypeNe i).symm).trans (optionEquivLeft R { b // b ≠ i })
⊢ (↑e.symm).comp Polynomial.CAlgHom = rename Subtype.val

Tactic:
ext

Goal state after:
n : Type u_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : MvPolynomial n R
i : n
hf0 : f ≠ 0
hif : i ∉ f.vars
hig : i ∉ g.vars
h : IsRelPrime f g
S : Type (max u_4 u_3) := MvPolynomial { j // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  (renameEquiv R (Equiv.optionSubtypeNe i).symm).trans (optionEquivLeft R { b // b ≠ i })
i✝ : { j // j ≠ i }
m✝ : n →₀ ℕ
⊢ coeff m✝ (((↑e.symm).comp Polynomial.CAlgHom) (X i✝)) = coeff m✝ ((rename Subtype.val) (X i✝))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := max ℓ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
⊢ ⋂ n, ⋂ (_ : n < ℓ), φ n ∈ ℱ ∧ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ

Tactic:
constructor

Goal state after:
case left
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := ⋯
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯
N : ℤ := ⋯
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
⊢ ⋂ n, ⋂ (_ : n < ℓ), φ n ∈ ℱ

case right
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := ⋯
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯
N : ℤ := ⋯
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
⊢ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
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 → ℕ
⊢ {x | i + 1 ≤ ↑x} = {x | i ≤ ↑x}.erase ⟨i, hin⟩

Tactic:
ext

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✝ ∈ {x | i ≤ ↑x}.erase ⟨i, hin⟩
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := max ℓ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
this : {x | ∀ d < ⋯.choose, coeff hℱ d = x.coeff d} ∈ ℱ
⊢ ⋂ n, ⋂ (_ : n < ℓ), φ n = {x | ∀ d < ⋯.choose, coeff hℱ d = x.coeff d}

Tactic:
ext

Goal state after:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := max ℓ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
this : {x | ∀ d < ⋯.choose, coeff hℱ d = x.coeff d} ∈ ℱ
x✝ : K⸨X⸩
⊢ x✝ ∈ ⋂ n, ⋂ (_ : n < ℓ), φ n ↔ x✝ ∈ {x | ∀ d < ⋯.choose, coeff hℱ d = x.coeff d}
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
j : Fin m
⊢ (if j ≤ ⟨↑i, him⟩ then 1 else 0) = (accumulate n m) (⇑fun₀ | i => 1) j

Tactic:
accumulate_apply,

Goal state after:
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
j : Fin m
⊢ (if j ≤ ⟨↑i, him⟩ then 1 else 0) = ∑ i_1 with ↑j ≤ ↑i_1, (fun₀ | i => 1) i_1
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case succ
R : Type u_3
m : ℕ
inst✝ : CommSemiring R
i : ℕ
him : i + 1 ≤ m
⊢ Monic (⇑toLex) (esymm (Fin m) R (i + 1))

Tactic:
| succ i =>

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
⊢ (∃ t,
      (∃ t_1 ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
        (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' t ⊆ S) ↔
    ∃ t ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t ⊆ S

Tactic:
constructor

Goal state after:
case mp
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
⊢ (∃ t,
      (∃ t_1 ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
        (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' t ⊆ S) →
    ∃ t ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t ⊆ S

case mpr
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
⊢ (∃ t ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t ⊆ S) →
    ∃ t,
      (∃ t_1 ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
        (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' t ⊆ S
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.refine_1
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
⊢ ∃ γ, {y | Valued.v.restrict y < ↑γ} ⊆ {P | Valued.v P < embedding ↑d}

Tactic:
obtain ⟨x, hx⟩ := RatFunc.valuation_surjective K (embedding d.1)

Goal state after:
case h.refine_1
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x : K⟮X⟯
hx : Valued.v x = embedding ↑d
⊢ ∃ γ, {y | Valued.v.restrict y < ↑γ} ⊆ {P | Valued.v P < embedding ↑d}
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
⊢ {x ∈ pairs σ k |
      match x with
      | (s, snd) => #s < k} =
    (range k).disjiUnion (fun x ↦ powersetCard x univ) ⋯ ×ˢ univ

Tactic:
ext

Goal state after:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a✝ : Finset σ × σ
⊢ a✝ ∈
      {x ∈ pairs σ k |
        match x with
        | (s, snd) => #s < k} ↔
    a✝ ∈ (range k).disjiUnion (fun x ↦ powersetCard x univ) ⋯ ×ˢ univ
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
⊢ ratfuncAdicComplPkg.compare (LaurentSeriesPkg K)
      { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm RatFunc.X) }.toCompletion =
    (algebraMap K⟮X⟯ K⸨X⸩) RatFunc.X

Tactic:
← LaurentSeries_coe,

Goal state after:
K : Type u_2
inst✝ : Field K
⊢ ratfuncAdicComplPkg.compare (LaurentSeriesPkg K)
      { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm RatFunc.X) }.toCompletion =
    (LaurentSeriesPkg K).coe (WithVal.toVal (polynomialValuationX K) RatFunc.X)
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (expand p hp) φ d ≠ 0
this : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ := Finsupp.mapRange (fun n ↦ n / p) ⋯ d
eq_aux : p • m = d
⊢ d ∈ (fun x ↦ p • x) '' Function.support φ

Tactic:
← eq_aux,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
this : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ := Finsupp.mapRange (fun n ↦ n / p) ⋯ d
hd : (expand p hp) φ (p • m) ≠ 0
eq_aux : p • m = d
⊢ d ∈ (fun x ↦ p • x) '' Function.support φ
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁶ : Ring R
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module (Matrix ι ι R) M
inst✝¹ : Module R M
inst✝ : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
⊢ Commute (diagonal fun x ↦ r) (single i i 1)

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
inst✝⁶ : Ring R
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module (Matrix ι ι R) M
inst✝¹ : Module R M
inst✝ : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
i✝ j✝ : ι
⊢ ((diagonal fun x ↦ r) * single i i 1) i✝ j✝ = (single i i 1 * diagonal fun x ↦ r) i✝ j✝
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ = 0
⊢ ↑p ≠ 0

Tactic:
by norm_cast

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ {t | Valued.v t < γ} ∈ 𝓝 a ∧
    (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) ⁻¹' {t | Valued.v t < γ} ⊆
      ⇑Valued.v ⁻¹' S

Tactic:
constructor

Goal state after:
case h.left
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ {t | Valued.v t < γ} ∈ 𝓝 a

case h.right
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) ⁻¹' {t | Valued.v t < γ} ⊆
    ⇑Valued.v ⁻¹' S