mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (truncation f n) μ

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : α) ∂μ, ‖truncation f n a‖ ≤ |f a|

pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (fun x ↦ |f x|) μ

pp: case refine_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ truncation f n a) atTop (𝓝 (f a))

Tactic:
· exact Eventually.of_forall fun A ↦ hf.aestronglyMeasurable.truncation

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : α) ∂μ, ‖truncation f n a‖ ≤ |f a|

case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (fun x ↦ |f x|) μ

case refine_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ truncation f n a) atTop (𝓝 (f a))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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 : ℝ := ⋯
N : ℕ
⊢ 0 ≤ (c - 1)⁻¹ ^ 3

Tactic:
exact pow_nonneg (inv_nonneg.2 (sub_nonneg.2 c_one.le)) _

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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 : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
N : ℕ
⊢ c ^ 5 * (c - 1)⁻¹ ^ 3 * ∑ j ∈ range (u (N - 1)), (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤
    c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)

Tactic:
apply mul_le_mul_of_nonneg_left (I1 _)
        apply mul_nonneg (pow_nonneg c_pos.le _)
        exact pow_nonneg (inv_nonneg.2 (sub_nonneg.2 c_one.le)) _

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : CommRing k
inst✝ : Monoid G
A B C : TopRep k G
r : k
f : A ⟶ B
g : B ⟶ C
x✝ : ↑A
⊢ (Hom.hom ((r • f) ≫ g)).toContinuousLinearMap x✝ = (Hom.hom (r • f ≫ g)).toContinuousLinearMap x✝

Tactic:
simp [hom_smul, ContIntertwiningMap.comp_smul]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
f : k[Fin (n + 1 + 1) → G]
⊢ (Hom.hom ((standardComplex k G).d (n + 1) n)) f = (d k G (n + 1)) f

Tactic:
rw [← Representation.IntertwiningMap.toLinearMap_apply, d_eq]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
f : k[Fin (n + 1 + 1) → G]
⊢ (d k G (n + 1)) f = (d k G (n + 1)) f
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
          (HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)
                  0).hom.app
            (trivial k G k)).f
      0 =
    (forget₂ToModuleCatHomotopyEquiv k G).hom.f 0

Tactic:
simpa using! (forget₂ToModuleCatHomotopyEquiv_f_0_eq k G).symm

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

Goal state before:
pp: case e_a.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
i : Fin 2
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2) i =
    Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) i

Tactic:
fin_cases i

Goal state after:
case e_a.e_a.«_@»._internal._hyg.0.«0»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2) ((fun i ↦ i) ⟨0, ⋯⟩) =
    Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨0, ⋯⟩)

case e_a.e_a.«_@»._internal._hyg.0.«1»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2) ((fun i ↦ i) ⟨1, ⋯⟩) =
    Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: case e_a.e_a.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
i : Fin 2
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2) i =
    Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) i

Tactic:
fin_cases i

Goal state after:
case e_a.e_a.e_a.«_@»._internal._hyg.0.«0»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2) ((fun i ↦ i) ⟨0, ⋯⟩) =
    Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨0, ⋯⟩)

case e_a.e_a.e_a.«_@»._internal._hyg.0.«1»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2) ((fun i ↦ i) ⟨1, ⋯⟩) =
    Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: case e_a.e_a.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
i : Fin 2
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1) i =
    Fin.contractNth 2 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) i

Tactic:
fin_cases i

Goal state after:
case e_a.e_a.e_a.«_@»._internal._hyg.0.«0»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1) ((fun i ↦ i) ⟨0, ⋯⟩) =
    Fin.contractNth 2 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨0, ⋯⟩)

case e_a.e_a.e_a.«_@»._internal._hyg.0.«1»
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1) ((fun i ↦ i) ⟨1, ⋯⟩) =
    Fin.contractNth 2 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) ((fun i ↦ i) ⟨1, ⋯⟩)
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✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map (↑e.symm) (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) n ≫
      map (↑e) (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) n =
    𝟙 (groupCohomology B n)

Tactic:
rw [← groupCohomology.map_comp, ← groupCohomology.map_id]

Goal state after:
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✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e.symm).comp ↑e)
      ((resFunctor ↑e).map (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) ≫
        ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ })
      n =
    map (MonoidHom.id G) (𝟙 B) n
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✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map (↑e) (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) n ≫
      map (↑e.symm) (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) n =
    𝟙 (groupCohomology A n)

Tactic:
rw [← groupCohomology.map_comp, ← groupCohomology.map_id]

Goal state after:
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✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e).comp ↑e.symm)
      ((resFunctor ↑e.symm).map (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) ≫
        ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ })
      n =
    map (MonoidHom.id H) (𝟙 A) n
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun s ↦ (monomial s) 1) '' (fun i ↦ Finsupp.single i 1) '' s) ↔
    ∀ xi ∈ x.support, ∃ si ∈ (fun i ↦ Finsupp.single i 1) '' s, si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0

Tactic:
rw [Set.image_image] at this

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x ↦ (monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ xi ∈ x.support, ∃ si ∈ (fun i ↦ Finsupp.single i 1) '' s, si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ idealOfVars σ R ^ n = Ideal.span ((fun x ↦ (monomial x) 1) '' ⇑degree ⁻¹' {n})

Tactic:
by
  rw [idealOfVars, Ideal.span, Submodule.span_pow, ← Set.image_univ,
    image_pow_eq_finsuppProd_image]
  simp [monomial_eq, Set.preimage, degree]

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

Goal state before:
pp: A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
d : MvPolynomial σ A
⊢ (aeval fun d ↦ (Ideal.Quotient.mk I) (X d)) d =
    eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) (fun d ↦ (aeval fun d ↦ (Ideal.Quotient.mk I) (X d)) (X d)) d

Tactic:
aeval_X,

Goal state after:
A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
d : MvPolynomial σ A
⊢ (aeval fun d ↦ (Ideal.Quotient.mk I) (X d)) d =
    eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) (fun d ↦ (Ideal.Quotient.mk I) (X d)) d
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
y : R
hy : y ∈ I
⊢ y ∈ span (Set.range p) ⊔ span (Set.range fun a_1 ↦ a • i a_1)

Tactic:
Submodule.mem_sup

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
y : R
hy : y ∈ I
⊢ ∃ y_1 ∈ span (Set.range p), ∃ z ∈ span (Set.range fun a_1 ↦ a • i a_1), y_1 + z = y
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I m : Ideal R
inst✝ : m.IsMaximal
le : I ≤ m
fg : I.FG
⊢ Ideal.map (algebraMap R (AdicCompletion I R)) m ⊔ RingHom.ker (evalOneₐ I).toRingHom =
    Ideal.map (algebraMap R (AdicCompletion I R)) m

Tactic:
sup_eq_left,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I m : Ideal R
inst✝ : m.IsMaximal
le : I ≤ m
fg : I.FG
⊢ RingHom.ker (evalOneₐ I).toRingHom ≤ Ideal.map (algebraMap R (AdicCompletion I R)) m
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
inj : Function.Injective ⇑f
m : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
m' : ↥(maximalIdeal (AdicCompletion (maximalIdeal R) R))
hm' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).toCotangent m' = m
⊢ ∃ a, f a = m

Tactic:
rcases Submodule.Quotient.mk_surjective _ (m'.1.1 2) with ⟨l, hl⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
inj : Function.Injective ⇑f
m : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
m' : ↥(maximalIdeal (AdicCompletion (maximalIdeal R) R))
hm' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).toCotangent m' = m
l : R
hl : Submodule.Quotient.mk l = ↑↑m' 2
⊢ ∃ a, f a = m
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
inst✝³ : Module R B
inst✝² : Coalgebra R B
a : A
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
⊢ (TensorProduct.map ↑f ↑f) (comul a) = f a ⊗ₜ[R] f a

Tactic:
ha.comul_eq_tmul_self

Goal state after:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
inst✝³ : Module R B
inst✝² : Coalgebra R B
a : A
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
⊢ (TensorProduct.map ↑f ↑f) (a ⊗ₜ[R] a) = f a ⊗ₜ[R] f a
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
r : R
a✝ : span {Submodule.IsPrincipal.generator p.contentIdeal} ≤ span {r}
⊢ C r ∣ C (Submodule.IsPrincipal.generator p.contentIdeal)

Tactic:
apply _root_.map_dvd C
      rwa [← span_singleton_le_span_singleton]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
⊢ ⊤ = p.contentIdeal * q.contentIdeal

Tactic:
simp [hp, hq]

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

Goal state before:
pp: case single_one_left
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
a : A
⊢ (((Algebra.TensorProduct.map ↑(domCongr R A e) ↑(domCongr R A e)).comp (comulAlgHom R A[M])).comp singleOneAlgHom) a =
    (((comulAlgHom R A[N]).comp ↑(domCongr R A e)).comp singleOneAlgHom) a

Tactic:
simp [← (Coalgebra.Repr.arbitrary R a).eq]

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : (↥(S.integer K))ˣ
v : HeightOneSpectrum R
hv : v ∉ S
⊢ (HeightOneSpectrum.valuation K v) (↑↑x * ↑x.inv) = 1

Tactic:
Subtype.mk_eq_mk.mp x.val_inv,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : (↥(S.integer K))ˣ
v : HeightOneSpectrum R
hv : v ∉ S
⊢ (HeightOneSpectrum.valuation K v) 1 = 1
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case neg.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
x✝ : ℕ
h1 : p.coeff x✝ ≠ 0
h2 : 1 ≤ (v.intAdicAbv hb) (p.coeff x✝)
⊢ 1 ≤ p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)

Tactic:
exact Finset.le_sup'_of_le (fun n ↦ (v.intAdicAbv hb) (p.coeff n)) (by simp [h1]) h2

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

Goal state before:
pp: case single_one_left
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
a : A
⊢ (((Algebra.TensorProduct.map ↑(toAdditiveAlgEquiv R A M) ↑(toAdditiveAlgEquiv R A M)).comp (comulAlgHom R A[M])).comp
        singleOneAlgHom)
      a =
    (((comulAlgHom R (AddMonoidAlgebra A (Additive M))).comp ↑(toAdditiveAlgEquiv R A M)).comp singleOneAlgHom) a

Tactic:
simp [← (Coalgebra.Repr.arbitrary R a).eq]

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

Goal state before:
pp: case single_zero_left
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Bialgebra R A
inst✝² : Bialgebra R B
inst✝¹ : AddMonoid M
inst✝ : AddMonoid N
a : A
⊢ (((Algebra.TensorProduct.map ↑(toMultiplicativeAlgEquiv R A M) ↑(toMultiplicativeAlgEquiv R A M)).comp
            (comulAlgHom R A[M])).comp
        singleZeroAlgHom)
      a =
    (((comulAlgHom R (MonoidAlgebra A (Multiplicative M))).comp ↑(toMultiplicativeAlgEquiv R A M)).comp
        singleZeroAlgHom)
      a

Tactic:
simp [← (Coalgebra.Repr.arbitrary R a).eq]

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

Goal state before:
pp: R : Type u_1
A : Type u_3
M : Type u_8
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Bialgebra R A
inst✝ : AddMonoid M
m : M
a : A
⊢ (toMultiplicativeBialgEquiv R A M) (single m a) = MonoidAlgebra.single (Multiplicative.ofAdd m) a

Tactic:
simp [toMultiplicativeBialgEquiv]

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

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

Tactic:
by
  cases Nat.eq_zero_or_pos n with
  | inl hn =>
    rw [if_pos hn, hn, dp_zero]
  | inr hn =>
    rw [if_neg (ne_of_gt hn), ← zero_smul R (0 : M), dp_smul]
    rw [zero_pow (Nat.pos_iff_ne_zero.mp hn), zero_smul]

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ f = g

Tactic:
DFunLike.ext'_iff

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ ⇑f = ⇑g
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case a
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| IsRegular M (r :: rs)

Tactic:
rw [isRegular_iff, ne_eq]

Goal state after:
case a
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| IsWeaklyRegular M (r :: rs) ∧ ¬⊤ = Ideal.ofList (r :: rs) • ⊤
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case b
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)

Tactic:
rw [isRegular_iff, ne_eq]

Goal state after:
case b
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| IsSMulRegular M r ∧
    IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) ∧
      ¬⊤ = Ideal.ofList (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) • ⊤
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
hlt : ↑(padicValNat p n !) < ↑n
hnorm : 0 < ‖↑n !‖
⊢ ‖(↑n !)⁻¹ʳ * ↑x ^ n‖ ≤ (↑p)⁻¹

Tactic:
← zpow_neg_one,

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
hlt : ↑(padicValNat p n !) < ↑n
hnorm : 0 < ‖↑n !‖
⊢ ‖(↑n !)⁻¹ʳ * ↑x ^ n‖ ≤ ↑p ^ (-1)
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hn : ¬n = 0
⊢ (↑p)⁻¹ ≤ 1

Tactic:
← zpow_neg_one,

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hn : ¬n = 0
⊢ ↑p ^ (-1) ≤ 1
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
p q : hI.SubDPIdeal
h : (fun s ↦ ↑s.carrier) p = (fun s ↦ ↑s.carrier) q
⊢ p = q

Tactic:
by
    rw [SetLike.coe_set_eq] at h
    cases p; cases q; congr

Goal state after: