mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
g : G
x₁ : W
hx₁ : x₁ ∈ ρ₁.toSubmodule
⊢ ∀ x₂ ∈ ρ₂.toSubmodule, (ρ g) x₁ + (ρ g) x₂ ∈ ρ₁.toSubmodule ⊔ ρ₂.toSubmodule

Tactic:
x₂

Goal state after:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
g : G
x₁ : W
hx₁ : x₁ ∈ ρ₁.toSubmodule
x₂ : W
⊢ x₂ ∈ ρ₂.toSubmodule → (ρ g) x₁ + (ρ g) x₂ ∈ ρ₁.toSubmodule ⊔ ρ₂.toSubmodule
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
⊢ ∀ (a b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)

Tactic:
intro a b

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
a b : ℝ
⊢ ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
ht : 0 < t
⊢ mgf X μ t ≤ rexp ((↑‖b - a‖₊ / 2) ^ 2 * t ^ 2 / 2)

Tactic:
have hi (u : ℝ) : Integrable (fun ω ↦ exp (u * X ω)) μ := integrable_exp_mul_of_mem_Icc hm hb

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (fun ω ↦ rexp (u * X ω)) μ
⊢ mgf X μ t ≤ rexp ((↑‖b - a‖₊ / 2) ^ 2 * t ^ 2 / 2)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h.hc
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := ⋯
S : ℕ → Ω → ℝ := ⋯
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := ⋯
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := ⋯
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N i : ℕ
a✝ : i ∈ range N
⊢ 0 < ↑(u i) * ε

Tactic:
· apply mul_pos (Nat.cast_pos.2 _) εpos
          refine zero_lt_one.trans_le ?_
          apply Nat.le_floor
          rw [Nat.cast_one]
          apply one_le_pow₀ c_one.le

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
by_cases h : ∀ᵐ ω, X 0 ω = 0

Goal state after:
case pos
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ∀ᵐ (ω : Ω), X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

case neg
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
⊢ ∀ (hs : MeasurableSet s),
    ∀ᵐ (ω : Ω) ∂μ,
      Tendsto
        (fun n ↦
          (↑n)⁻¹ •
            ∑ i ∈ Finset.range n, (SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) (X i ω))
        atTop (𝓝 (∫ (x : Ω), (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) ∘ X 0) x ∂μ))

Tactic:
hs

Goal state after:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto
      (fun n ↦
        (↑n)⁻¹ •
          ∑ i ∈ Finset.range n, (SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) (X i ω))
      atTop (𝓝 (∫ (x : Ω), (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) ∘ X 0) x ∂μ))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝¹ : SeparableSpace ↑s
this✝ : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
J : ∀ᶠ (n : ℕ) in atTop, ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
n : ℕ
hn : (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
h'n : ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
⊢ ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω - ∫ (x : Ω), X 0 x ∂μ‖ < ε

Tactic:
calc
  ‖(n : ℝ)⁻¹ • ∑ i ∈ Finset.range n, X i ω - μ[X 0]‖
    = ‖(n : ℝ)⁻¹ • ∑ i ∈ Finset.range n, (X i ω - Y k i ω) +
        ((n : ℝ)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - μ[Y k 0]) + (μ[Y k 0] - μ[X 0])‖ := by
      congr
      simp only [sum_sub_distrib, smul_sub]
      abel
  _ ≤ ‖(n : ℝ)⁻¹ • ∑ i ∈ Finset.range n, (X i ω - Y k i ω)‖ +
        ‖(n : ℝ)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - μ[Y k 0]‖ + ‖μ[Y k 0] - μ[X 0]‖ :=
      norm_add₃_le
  _ ≤ (∑ i ∈ Finset.range n, ‖X i ω - Y k i ω‖) / n + δ + δ := by
      gcongr
      simp only [norm_smul, norm_inv, RCLike.norm_natCast,
        div_eq_inv_mul]
      gcongr
      exact norm_sum_le _ _
  _ ≤ δ + δ + δ := by
      gcongr
      exact hn.le
  _ < ε := hδ

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Finite G
inst✝¹ : Group G
inst✝ : NeZero ↑(Nat.card G)
V : Rep k G
⊢ Module.Injective (MonoidAlgebra k G) ↑(equivalenceModuleMonoidAlgebra.functor.1 V)

Tactic:
exact Module.injective_of_isSemisimpleRing _ _

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✝
⊢ (cechNerveTerminalFrom (Action.ofMulAction G G)).map f ≫
      (limit.isoLimitCone (Action.ofMulActionLimitCone G fun x ↦ G)).hom =
    (limit.isoLimitCone (Action.ofMulActionLimitCone G fun x ↦ G)).hom ≫ (classifyingSpaceUniversalCover G).map f

Tactic:
refine IsLimit.hom_ext (Action.ofMulActionLimitCone.{u, 0} G fun _ => G).2 fun j => ?_

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))
⊢ ((cechNerveTerminalFrom (Action.ofMulAction G G)).map f ≫
        (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
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
m : ℕ
key : (barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ (diagonalSuccIsoFree k G m).inv = 0
⊢ (barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ (diagonalSuccIsoFree k G m).inv =
    0 ≫ (diagonalSuccIsoFree k G m).inv

Tactic:
by simpa using key

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
this✝ : Mono X.f := hX.mono_f
i : ℕ
this : (Rep.Hom.hom X.f).range = (Rep.Hom.hom X.g).ker
⊢ ((X.map (chainsFunctor k G)).map (HomologicalComplex.eval (ModuleCat k) (ComplexShape.down ℕ) i)).Exact

Tactic:
simp [moduleCat_exact_iff_range_eq_ker, ker_mapRange,
        range_mapRange_linearMap X.f.hom.toLinearMap (LinearMap.ker_eq_bot.2 <|
        (Rep.mono_iff_injective X.f).1 hX.mono_f), this]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
x✝ : Fin 1 → G
⊢ ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) ((ConcreteCategory.hom (chainsIso₁ X.X₁).inv) x)) x✝ =
    ((ModuleCat.Hom.hom (d₂₁ X.X₂ ≫ (chainsIso₁ X.X₂).inv)) y) x✝

Tactic:
simp [← hx, chainsIso₁]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
⊢ (ConcreteCategory.hom (δ hX 2 1 ⋯)) ((ConcreteCategory.hom (H2π X.X₃)) z) = (ConcreteCategory.hom (H1π X.X₁)) ⟨x, ⋯⟩

Tactic:
by
  simpa only [H2π, ModuleCat.hom_comp, LinearMap.coe_comp, Function.comp_apply, H1π,
    ← cyclesMk₂_eq X.X₃, ← cyclesMk₁_eq X.X₁]
  using! δ_apply hX (i := 2) (j := 1) rfl ((chainsIso₂ X.X₃).inv z.1) (by
    rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₂₁_comp_inv]; simp)
    ((chainsIso₂ X.X₂).inv y) (Finsupp.ext fun _ => by simp [chainsIso₂, ← hy])
    ((chainsIso₁ X.X₁).inv x) (Finsupp.ext fun _ => by
    conv_rhs => rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₂₁_comp_inv]
    simp [← hx, chainsIso₁])

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 : ↑A
⊢ single 1 a ∈ boundaries₁ A

Tactic:
by
  use single (1, 1) a
  simp [d₂₁]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
d : τ →₀ ℕ
x : σ
a✝¹ : x ∉ ⋃ i ∈ ↑d.support, f ⁻¹' {i}
a✝ : x ∈ {s | (coeff d) ((X ∘ f) s) ≠ 0}
⊢ False

Tactic:
simp_all [coeff_X]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬↑(span {a}) ∩ ↑(closure {r | Prime r}).toSubsemigroup = ∅
x : R
hx : x ∈ ↑(span {a})
hx₂ : x ∈ ↑(closure {r | Prime r}).toSubsemigroup
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a

Tactic:
obtain ⟨b, hb⟩ := mem_span_singleton'.1 hx

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬↑(span {a}) ∩ ↑(closure {r | Prime r}).toSubsemigroup = ∅
x : R
hx : x ∈ ↑(span {a})
hx₂ : x ∈ ↑(closure {r | Prime r}).toSubsemigroup
b : R
hb : b * a = x
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mp.right
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
this : TopologicalSpace R := J.adicTopology
s : Set R
⊢ s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s

Tactic:
hs

Goal state after:
case mp.right
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
this : TopologicalSpace R := J.adicTopology
s : Set R
hs : s ∈ 𝓝 0
⊢ ∃ n, ↑(J ^ n) ⊆ s
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : WithIdeal R
a : R
ha : a ∈ i
⊢ IsTopologicallyNilpotent a

Tactic:
by
  suffices ∀ m : ℕ, ∃ n₀, ∀ n, n₀ ≤ n → a ^ n ∈ i ^ m by
    simpa [IsTopologicallyNilpotent, i.hasBasis_nhds_zero_adic.tendsto_right_iff]
  exact fun m ↦ ⟨m, fun n hn ↦ Ideal.pow_le_pow_right hn (Ideal.pow_mem_pow ha _)⟩

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ IsAdicComplete (maximalIdeal (AdicCompletion (maximalIdeal R) R)) (AdicCompletion (maximalIdeal R) R)

Tactic:
AdicCompletion.maximalIdeal_eq_map_of_fg fg

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ IsAdicComplete (Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal R))
    (AdicCompletion (maximalIdeal R) R)
Module: Mathlib.RingTheory.Algebraic.Denominator

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsAlgebraic R x
r : R
hr0 : r ≠ 0
hr : IsIntegral R (r • x)
⊢ Algebra.denominator R x ≠ 0

Tactic:
exact ne_zero_of_dvd_ne_zero hr0 (Algebra.denominator_dvd_iff.mpr hr)

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

Goal state before:
pp: 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
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
⊢ Epi (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)

Tactic:
ModuleCat.epi_iff_surjective

Goal state after:
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
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv))
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
a b c : ℕ
σ : Type u_3
inst✝ : Finite σ
this :
  Ideal.map (toAdicCompletionAlgEquiv σ R).toRingEquiv (Ideal.span (Set.range X)) =
    Ideal.map (algebraMap (MvPolynomial σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R)
⊢ IsAdicComplete
    (Ideal.map (algebraMap (MvPolynomial σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R))
    (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))

Tactic:
IsAdicComplete.map_algebraMap_iff

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
a b c : ℕ
σ : Type u_3
inst✝ : Finite σ
this :
  Ideal.map (toAdicCompletionAlgEquiv σ R).toRingEquiv (Ideal.span (Set.range X)) =
    Ideal.map (algebraMap (MvPolynomial σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R)
⊢ IsAdicComplete (MvPolynomial.idealOfVars σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: 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
⊢ Epi (H1CoresCoinf A S).g

Tactic:
ModuleCat.epi_iff_surjective

Goal state after:
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
⊢ Function.Surjective ⇑(ConcreteCategory.hom (H1CoresCoinf A S).g)
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) (Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal A (FractionRing A)).range)) I) =
    Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal B (FractionRing B)).range))
      ((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) I)

Tactic:
exact extendedHom_quotientMk A B I

Goal state after:
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
⊢ (Finsupp.linearCombination A fun y ↦ single y 1).range = ⊤

Tactic:
exact LinearMap.range_eq_top_of_surjective _ fun x ↦
      ⟨x.coeff, by simp [Finsupp.linearCombination_apply]⟩

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_11
inst✝² : CommSemiring R
A : Type u_12
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
n : ℤ
⊢ comul (T n) = T n ⊗ₜ[R] T n

Tactic:
simp [T, -single_eq_C_mul_T]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_11
inst✝² : CommSemiring R
A : Type u_12
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
n : ℤ
⊢ counit (T n) = 1

Tactic:
simp [T, -single_eq_C_mul_T]

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case h.refine_2.inl
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
t : ↥S
this : IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s)
ht : t • r ^ 0 • x = 0
⊢ ↑t * r ∈ (⊥.colon {x}).radical

Tactic:
exact Ideal.IsTwoSided.mul_mem_of_left _ ⟨1, by simpa using! ht⟩

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
⊢ valuation.ker = selmerGroup.subgroupOf selmerGroup

Tactic:
ext ⟨_, hx⟩
  constructor
  · intro hx' v _
    by_cases hv : v ∈ S
    · exact congr_fun hx' ⟨v, hv⟩
    · exact hx v hv
  · exact fun hx' => funext fun v => hx' v <| Set.notMem_empty v

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case h
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
e : ↥T → ℕ
g : ↥T → ↥S
hg : ∀ (a : ↥T), g a • ↑a ^ e a • m = 0
a : R
ha : a ∈ ↑T
u : ↥S
hu : ∏ a, g a = g ⟨a, ha⟩ * u
⊢ a ^ e ⟨a, ha⟩ • ↑(∏ a, g a) • m = 0

Tactic:
hu,

Goal state after:
case h
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
e : ↥T → ℕ
g : ↥T → ↥S
hg : ∀ (a : ↥T), g a • ↑a ^ e a • m = 0
a : R
ha : a ∈ ↑T
u : ↥S
hu : ∏ a, g a = g ⟨a, ha⟩ * u
⊢ a ^ e ⟨a, ha⟩ • ↑(g ⟨a, ha⟩ * u) • m = 0
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
a b : A
dp : ℕ → A → A
dp_add : ∀ (n : ℕ), dp n (a + b) = ∑ k ∈ antidiagonal n, dp k.1 a * dp k.2 b
⊢ (PowerSeries.mk fun n ↦ dp n (a + b)) = (PowerSeries.mk fun n ↦ dp n a) * PowerSeries.mk fun n ↦ dp n b

Tactic:
by
  ext n
  simp only [PowerSeries.coeff_mk, PowerSeries.coeff_mul, dp_add n,
    sum_antidiagonal_eq_sum_range_succ_mk]

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

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

Tactic:
dp_zero

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