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

Goal state before:
pp: k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
i : ℕ
⊢ (cochainsMap (ContinuousMonoidHom.id G) (𝟙 X)).f i = (𝟙 X.homogeneousCochains).f i

Tactic:
rw [cochainsMap_f, resolutionMap_id]

Goal state after:
k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
i : ℕ
⊢ invariantsResMap (↑(ContinuousMonoidHom.id G)) (𝟙 (X.resolutionX (i + 1))) = (𝟙 X.homogeneousCochains).f i
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

Goal state before:
pp: k : Type u
G H : Type v
inst✝⁷ : Ring k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
X : TopRep k G
Y : TopRep k H
φ : H →ₜ* G
f : res (↑φ) X ⟶ Y
n : ℕ
⊢ π X n ≫ map φ f n = cocyclesMap φ f n ≫ π Y n

Tactic:
by
  simp [map, cocyclesMap]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ (Hom.hom ((leftRegular k G).applyAsHom g - 𝟙 (leftRegular k G))).range = (Hom.hom (leftRegular k G).norm).ker

Tactic:
simp [norm, ker_leftRegular_norm_eq, range_applyAsHom_sub_eq_ker_linearCombination k g hg]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
X✝ Y✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
j : Discrete (Fin ((Opposite.unop Y✝).len + 1))
⊢ limit.lift (Discrete.functor fun x ↦ Action.ofMulAction G G)
        (Fan.mk (∏ᶜ fun x ↦ Action.ofMulAction G G) fun i ↦
          Pi.π (fun x ↦ Action.ofMulAction G G) ((SimplexCategory.Hom.toOrderHom f.unop) i)) ≫
      (limit.isoLimitCone (Action.ofMulActionLimitCone G fun x ↦ G)).hom ≫
        (Action.ofMulActionLimitCone G fun x ↦ G).cone.π.app j =
    ((limit.isoLimitCone (Action.ofMulActionLimitCone G fun x ↦ G)).hom ≫ (classifyingSpaceUniversalCover G).map f) ≫
      (Action.ofMulActionLimitCone G fun x ↦ G).cone.π.app j

Tactic:
limit.isoLimitCone_hom_π,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
X✝ Y✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
j : Discrete (Fin ((Opposite.unop Y✝).len + 1))
⊢ limit.lift (Discrete.functor fun x ↦ Action.ofMulAction G G)
        (Fan.mk (∏ᶜ fun x ↦ Action.ofMulAction G G) fun i ↦
          Pi.π (fun x ↦ Action.ofMulAction G G) ((SimplexCategory.Hom.toOrderHom f.unop) i)) ≫
      limit.π (Discrete.functor fun i ↦ Action.ofMulAction G G) j =
    ((limit.isoLimitCone (Action.ofMulActionLimitCone G fun x ↦ G)).hom ≫ (classifyingSpaceUniversalCover G).map f) ≫
      (Action.ofMulActionLimitCone G fun x ↦ G).cone.π.app j
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) x = 0 ↔ ⇑x ∈ coboundaries₁ A

Tactic:
by
  have h := leftHomologyπ_naturality'_assoc (isoShortComplexH1 A).inv
    (shortComplexH1 A).moduleCatLeftHomologyData (leftHomologyData _)
    ((inhomogeneousCochains A).sc 1).leftHomologyIso.hom
  simp only [H1π, isoCocycles₁, π, HomologicalComplex.homologyπ, homologyπ,
    cyclesMapIso'_inv, leftHomologyπ, ← h, ← leftHomologyMapIso'_inv, ModuleCat.hom_comp,
    LinearMap.coe_comp, Function.comp_apply, map_eq_zero_iff _
    ((ModuleCat.mono_iff_injective <| _).1 inferInstance)]
  simp [LinearMap.range_codRestrict, coboundaries₁, shortComplexH1, cocycles₁]

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
⊢ π A n ≫ map f φ n = cocyclesMap f φ n ≫ π B n

Tactic:
by
  simp [map, cocyclesMap]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fintype G
X : FDRep k G
v : ↑X.V
x✝¹ : k
x✝ : G → k
⊢ ∑ s, (x✝¹ • x✝) s • (X.ρ s⁻¹) v = (RingHom.id k) x✝¹ • ∑ s, x✝ s • (X.ρ s⁻¹) v

Tactic:
simp [smul_sum, smul_smul]

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

Goal state before:
pp: case pos.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ (generators (Ideal.map constantCoeff I)).ncard ≤ spanFinrank (Ideal.map constantCoeff I)

Tactic:
rw [FG.generators_ncard hfg]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ π A 0 ≫ (H0Iso A).hom = (cyclesIso₀ A).hom ≫ (coinvariantsMk k G).app A

Tactic:
by
  simp [H0Iso, cyclesIso₀]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: case mul
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z₁ z₂ : R
hz₁ : z₁ ∈ closure {r | IsUnit r ∨ Prime r}
hz₂ : z₂ ∈ closure {r | IsUnit r ∨ Prime r}
h₁ : ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z₁
h₂ : ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z₂
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod (z₁ * z₂)

Tactic:
| mul z₁ z₂ hz₁ hz₂ h₁ h₂ =>

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
this : ∀ (i j : ℕ), ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j
⊢ ∀ (i j : ℕ), ∃ k, I ^ k • ⊤ ≤ I ^ i • ⊤ ⊓ I ^ j • ⊤

Tactic:
simpa only [smul_eq_mul, mul_top, Algebra.algebraMap_self, map_id, le_inf_iff] using! this

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff x) ((PowerSeries.coeff k) ((finSuccEquiv R n) (X 0))) = (coeff x) ((PowerSeries.coeff k) PowerSeries.X)

Tactic:
simp_rw [coeff_coeff_finSuccEquiv, PowerSeries.coeff_X, coeff_X, cons_eq_single_zero_iff]

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
⊢ (if x = 0 ∧ k = 1 then 1 else 0) = (coeff x) (if k = 1 then 1 else 0)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
l m n : ℕ
h : l ≤ m
h' : l ≤ n
p : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < l
⊢ MvPolynomial.coeff x ((truncTotal m) p - (truncTotal n) p) = 0

Tactic:
rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ (by lia),
    coeff_truncTotal _ (by lia)]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
x✝ : ℕ
a : d = single i x✝
⊢ (coeff x✝) f = 0

Tactic:
subst a

Goal state after:
σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
hf : constantCoeff f = 0
x✝ : ℕ
hd : (single i x✝) i = 0
⊢ (coeff x✝) f = 0
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD I ^ m • ⊤]
m n : ℕ
h' : m ≤ n
⊢ ↑(x n) m = ↑(x m) m

Tactic:
specialize hx h'

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
m n : ℕ
hx : x m ≡ x n [SMOD I ^ m • ⊤]
h' : m ≤ n
⊢ ↑(x n) m = ↑(x m) m
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h
k G H✝ : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H✝
A : Rep k G
B : Rep k H✝
f : G →* H✝
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ (A.quotientToCoinvariants S))
y : ↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S)))
hy : (ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) ((A.toCoinvariants S).resOfQuotientIso S).inv)) y = x
Y : G →₀ ↑A
hY : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Y = ↑y
this : (ConcreteCategory.hom (d₁₀ A)) Y ∈ Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)
Z : ↥S →₀ ↑A
hZ : (ConcreteCategory.hom (chains₁ToCoinvariantsKer (res S.subtype A))) Z = ⟨(ConcreteCategory.hom (d₁₀ A)) Y, this⟩
H : (ConcreteCategory.hom (d₁₀ A)) (Y - mapDomain (⇑S.subtype) Z) = 0
⊢ ∃ a, (ConcreteCategory.hom (H1CoresCoinf A S).g) a = (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S))) x

Tactic:
use H1π A ⟨Y - mapDomain S.subtype Z, H⟩

Goal state after:
case h
k G H✝ : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H✝
A : Rep k G
B : Rep k H✝
f : G →* H✝
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ (A.quotientToCoinvariants S))
y : ↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S)))
hy : (ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) ((A.toCoinvariants S).resOfQuotientIso S).inv)) y = x
Y : G →₀ ↑A
hY : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Y = ↑y
this : (ConcreteCategory.hom (d₁₀ A)) Y ∈ Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)
Z : ↥S →₀ ↑A
hZ : (ConcreteCategory.hom (chains₁ToCoinvariantsKer (res S.subtype A))) Z = ⟨(ConcreteCategory.hom (d₁₀ A)) Y, this⟩
H : (ConcreteCategory.hom (d₁₀ A)) (Y - mapDomain (⇑S.subtype) Z) = 0
⊢ (ConcreteCategory.hom (H1CoresCoinf A S).g) ((ConcreteCategory.hom (H1π A)) ⟨Y - mapDomain (⇑S.subtype) Z, H⟩) =
    (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S))) x
Module: Mathlib.RingTheory.Coalgebra.MulOpposite

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x✝ : Aᵐᵒᵖ
⊢ (lTensor Aᵐᵒᵖ counit ∘ₗ comul) x✝ = ((TensorProduct.mk R Aᵐᵒᵖ R).flip 1) x✝

Tactic:
simp only [counit_def, comul_def, coe_comp, Function.comp_apply, lTensor_map, comp_assoc]

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x✝ : Aᵐᵒᵖ
⊢ (map (↑(opLinearEquiv R)) (counit ∘ₗ ↑(opLinearEquiv R).symm ∘ₗ ↑(opLinearEquiv R)))
      (comul (↑(opLinearEquiv R).symm x✝)) =
    ((TensorProduct.mk R Aᵐᵒᵖ R).flip 1) x✝
Module: Mathlib.RingTheory.Congruence.Star

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : R
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star (w✝ * y✝)) (Star.star (x✝ * z✝))

Tactic:
rw [star_mul, star_mul]

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : R
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star y✝ * Star.star w✝) (Star.star z✝ * Star.star x✝)
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
I : (FractionalIdeal A⁰ (FractionRing A))ˣ
⊢ (extendedHom A B) ((mk (FractionRing A)) I) =
    (mk (FractionRing B)) ((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) I)

Tactic:
rw [← ClassGroup.Quot_mk_eq_mk, ← ClassGroup.Quot_mk_eq_mk]
  exact extendedHom_quotientMk A B I

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
this : p.coeff n ∈ p.contentIdeal
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n

Tactic:
rw [Submodule.IsPrincipal.mem_iff_eq_smul_generator] at this

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
this : ∃ s, p.coeff n = s • Submodule.IsPrincipal.generator p.contentIdeal
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
G : Type u_5
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
x : A[G]
⊢ (Finsupp.linearCombination A fun y ↦ single y 1) x.coeff = x

Tactic:
by simp [Finsupp.linearCombination_apply]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribSMul.toLinearMap R M r)
⊢ comap ((LinearMap.lsmul R M) r) N ≤ N ↔ r • ⊤ ⊓ N ≤ r • N

Tactic:
← map_le_map_iff_of_injective h,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribSMul.toLinearMap R M r)
⊢ map (DistribSMul.toLinearMap R M r) (comap ((LinearMap.lsmul R M) r) N) ≤ map (DistribSMul.toLinearMap R M r) N ↔
    r • ⊤ ⊓ N ≤ r • N
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case neg.hnc
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
hn : ¬n = 0
⊢ ¬(m = 0 ∧ n = 0)

Tactic:
exact not_and_of_not_right (m = 0) hn

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

Goal state before:
pp: case h.add
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
g1 g2 : MvPolynomial (ℕ × M) R
hg1 : P ↑g1
hg2 : P ↑g2
⊢ P ↑(g1 + g2)

Tactic:
rw [RingCon.coe_add]
    exact h_add _ _ hg1 hg2

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec : s.Nonempty → (∀ i ∈ s, r i ∈ I) → hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
this : #s = #s - 1 + 1
⊢ r a ∈ I

Tactic:
exact hs' a (mem_insert_self a s)

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

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

Tactic:
· have hxmk : x ^ (m + k) = 0 := Ideal.pow_eq_zero_of_mem hnI hkm hx
    rw [dpow_eq_of_mem hx, dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_assoc, ← mul_assoc (x ^ m), mul_comm (x ^ m), mul_assoc _ (x ^ m), ← pow_add, hxmk,
      mul_zero, mul_zero, mul_zero, mul_zero]

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherian R M
rs rs' : List R
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
h4 : ⊤ ≠ Ideal.ofList rs • ⊤
⊢ ⊤ ≠ Ideal.ofList rs' • ⊤

Tactic:
· refine ne_of_ne_of_eq h4 (congrArg (Ideal.span · • ⊤) ?_)
    exact Set.ext fun _ => h2.mem_iff

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: case succ.inr
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
this✝¹ : Nontrivial S
U : Type u
w✝¹ : CommRing U
w✝ : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst✝ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝ : IsScalarTower S (S × U) U
this : Etale S U
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
have : Module.Finite S U := by
      have : Module.Finite S (S × U) := Module.Finite.equiv e.toLinearEquiv
      have : Module.Finite (S × U) U :=
        Module.Finite.of_surjective (Algebra.linearMap (S × U) U) (RingHom.snd S U).surjective
      exact Module.Finite.trans (S × U) _

Goal state after:
case succ.inr
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
this✝² : Nontrivial S
U : Type u
w✝¹ : CommRing U
w✝ : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst✝ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝¹ : IsScalarTower S (S × U) U
this✝ : Etale S U
this : Module.Finite S U
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
⊢ Ideal.map f I ≤ hK.dpEqualizer hK'

Tactic:
rw [Ideal.map, span_le]
  rintro b ⟨a, ha, rfl⟩
  exact ⟨hI_le_K (mem_map_of_mem f ha), fun n ↦ by rw [hIK.2 a ha, hIK'.2 a ha]⟩

Goal state after:
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:
decompose_mul,

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 : ι
⊢ ↑(((decompose 𝒜) x * (decompose 𝒜) y) i) ∈ Subsemiring.closure s
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : 0 < x.orderTop
⊢ ↑0 < ((powers x) n).orderTop

Tactic:
refine (lt_of_lt_of_le ((nsmul_pos_iff hn).mpr h) ?_)

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : 0 < x.orderTop
⊢ n • x.orderTop ≤ ((powers x) n).orderTop
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:
by
  trans (embDomain (Nat.castOrderEmbedding (α := Γ)) (toPowerSeries.symm x)).coeff
    (Nat.castOrderEmbedding n)
  · simp [ofPowerSeries_apply]
  rw [embDomain_coeff]
  simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
⊢ (x ^ n).cardSupp ≤ x.cardSupp ^ n

Tactic:
by
  induction n with
  | zero => simp
  | succ n IH =>
    simpa [pow_succ] using (cardSupp_mul_le ..).trans <| mul_le_mul_left IH _

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

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
a : Γ
⊢ ((single a) 0)⁻¹ = (single (-a)) 0⁻¹

pp: case inr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
a : Γ
r : R
hr : r ≠ 0
⊢ ((single a) r)⁻¹ = (single (-a)) r⁻¹

Tactic:
· simp [inv_def]

Goal state after:
case inr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
a : Γ
r : R
hr : r ≠ 0
⊢ ((single a) r)⁻¹ = (single (-a)) r⁻¹
Module: Mathlib.RingTheory.Ideal.UFD

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : WfDvdMonoid R
x : R
hx : Prime x
p : Ideal R
inst✝³ : p.IsPrime
hxp : x ∉ p
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
this : Disjoint ↑(Submonoid.powers x) ↑p
hpbot : ¬p = ⊥
hi : Function.Injective ⇑(algebraMap R S)
hpb : map (algebraMap R S) p ≠ ⊥
g : S
hg : map (algebraMap R S) p = S ∙ g
hg0 : g ≠ 0
a : R
n : ℤ
hxa : ¬x ∣ a
hag : selfZPow x S n * (algebraMap R S) a = g
hu : IsUnit (selfZPow x S n)
y : R
hy : x * y ∈ R ∙ a
⊢ y ∈ R ∙ a

Tactic:
rw [mem_span_singleton] at hy ⊢

Goal state after:
case neg.refine_2
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : WfDvdMonoid R
x : R
hx : Prime x
p : Ideal R
inst✝³ : p.IsPrime
hxp : x ∉ p
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
this : Disjoint ↑(Submonoid.powers x) ↑p
hpbot : ¬p = ⊥
hi : Function.Injective ⇑(algebraMap R S)
hpb : map (algebraMap R S) p ≠ ⊥
g : S
hg : map (algebraMap R S) p = S ∙ g
hg0 : g ≠ 0
a : R
n : ℤ
hxa : ¬x ∣ a
hag : selfZPow x S n * (algebraMap R S) a = g
hu : IsUnit (selfZPow x S n)
y : R
hy : a ∣ x * y
⊢ a ∣ y
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
hF : F.IsGabriel
⊢ F.IsUniform ∧ F • F = F

Tactic:
refine ⟨hF.toIsUniform, ?_⟩

Goal state after:
case mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
hF : F.IsGabriel
⊢ F • F = F
Module: Mathlib.RingTheory.KrullDimension.Module

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : _root_.Ideal R
⊢ supportDim R (R ⧸ I) = ringKrullDim (R ⧸ I)

Tactic:
by
  rw [supportDim_eq_ringKrullDim_quotient_annihilator, Ideal.annihilator_quotient]

Goal state after: