mathlib-initiative/mathlib-tactics huggingface dataset:
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‖ ∂μ))
⊢ Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
tendsto_iff_norm_sub_tendsto_zero,

Goal state after:
Ω : 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‖ ∂μ))
⊢ Tendsto (fun e ↦ ‖(↑e)⁻¹ • ∑ i ∈ Finset.range e, X i ω - ∫ (x : Ω), X 0 x ∂μ‖) atTop (𝓝 0)
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
X Y : Type w
inst✝¹² : TopologicalSpace k
inst✝¹¹ : Ring k
inst✝¹⁰ : Monoid G
inst✝⁹ : AddCommGroup X
inst✝⁸ : Module k X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : IsTopologicalAddGroup X
inst✝⁵ : ContinuousSMul k X
inst✝⁴ : AddCommGroup Y
inst✝³ : Module k Y
inst✝² : TopologicalSpace Y
inst✝¹ : IsTopologicalAddGroup Y
inst✝ : ContinuousSMul k Y
ρ : ContRepresentation k G X
σ : ContRepresentation k G Y
A B C : TopRep k G
X✝ Y✝ : TopRep k G
f : X✝ ⟶ Y✝
g : G
⊢ { V := TopModuleCat.of k ↑X✝, ρ := (TopModuleCat.of k ↑X✝).endRingEquiv.symm.toMonoidHom.comp ↑X✝.ρ }.ρ g ≫
      Hom.toTopModuleCatHom f =
    Hom.toTopModuleCatHom f ≫
      { V := TopModuleCat.of k ↑Y✝, ρ := (TopModuleCat.of k ↑Y✝).endRingEquiv.symm.toMonoidHom.comp ↑Y✝.ρ }.ρ g

Tactic:
by ext1; simp [TopModuleCat.endRingEquiv, f.hom.2 g]

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

Goal state before:
pp: R : Type u_1
G✝ : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²¹ : Monoid G✝
inst✝²⁰ : Ring R
inst✝¹⁹ : AddCommGroup V
inst✝¹⁸ : TopologicalSpace V
inst✝¹⁷ : IsTopologicalAddGroup V
inst✝¹⁶ : Module R V
inst✝¹⁵ : AddCommGroup W
inst✝¹⁴ : TopologicalSpace W
inst✝¹³ : IsTopologicalAddGroup W
inst✝¹² : Module R W
inst✝¹¹ : AddCommGroup U
inst✝¹⁰ : Module R U
inst✝⁹ : TopologicalSpace U
inst✝⁸ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁷ : Monoid H✝
π✝ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace R
inst✝³ : ContinuousSMul R V
inst✝² : ContinuousSMul R W
inst✝¹ : Group H
inst✝ : TopologicalSpace H
φ : G →ₜ* H
π : ContRepresentation R G V
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
by continuity

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

Goal state before:
pp: K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝ : Module.IsTorsionFree A L
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
hε : ↑ε / g ↑ε = (algebraMap B L) η
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
⊢ t • IsLocalization.mk' L a b = (algebraMap B L) a

Tactic:
Algebra.smul_def,

Goal state after:
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝ : Module.IsTorsionFree A L
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
hε : ↑ε / g ↑ε = (algebraMap B L) η
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
⊢ (algebraMap A L) t * IsLocalization.mk' L a b = (algebraMap B L) a
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: case refine_2
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : t • ((algebraMap B L) η * g (IsLocalization.mk' L a b)) = t • IsLocalization.mk' L a b
⊢ η * ((galRestrict A K L B) g) a = a

Tactic:
Algebra.smul_def,

Goal state after:
case refine_2
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap A L) t * ((algebraMap B L) η * g (IsLocalization.mk' L a b)) = t • IsLocalization.mk' L a b
⊢ η * ((galRestrict A K L B) g) a = a
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 : ↑A
hx✝ : x ∈ A.ρ.invariants
g : G
hx : (A.ρ g) x = x
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom A.ρ.invariants.subtype ≫ d₀₁ A)) ⟨x, hx✝⟩ g = (ModuleCat.Hom.hom 0) ⟨x, hx✝⟩ g

Tactic:
rw [← sub_eq_zero] at hx

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A
hx✝ : x ∈ A.ρ.invariants
g : G
hx : (A.ρ g) x - x = 0
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom A.ρ.invariants.subtype ≫ d₀₁ A)) ⟨x, hx✝⟩ g = (ModuleCat.Hom.hom 0) ⟨x, hx✝⟩ g
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ coboundaries₁ A = ⊥

Tactic:
coboundaries₁,

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ (ModuleCat.Hom.hom (d₀₁ A)).range = ⊥
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : span S = Ideal.map constantCoeff I
⊢ I = span {X} ⊔ Ideal.map C (span S)

Tactic:
hSI,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : span S = Ideal.map constantCoeff I
⊢ I = span {X} ⊔ Ideal.map C (Ideal.map constantCoeff I)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g : G
a : ↑A
⊢ (⇑(QuotientAddGroup.lift (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup
            ((Finsupp.liftAddHom fun g ↦
                  ↑((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A) (Additive.ofMul (Abelianization.of g)))).comp
              (cycles₁ A).toAddSubgroup.subtype)
            ⋯) ∘
        ⇑↑(ModuleCat.Hom.hom (H1Iso A).hom))
      ((ConcreteCategory.hom ((isoCycles₁ A).inv ≫ π A 1))
        ((ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (single g a))) =
    Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a

Tactic:
change QuotientAddGroup.lift _ _ _ ((H1Iso A).hom _) = _

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g : G
a : ↑A
⊢ (QuotientAddGroup.lift (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup
        ((Finsupp.liftAddHom fun g ↦
              ↑((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A) (Additive.ofMul (Abelianization.of g)))).comp
          (cycles₁ A).toAddSubgroup.subtype)
        ⋯)
      ((ConcreteCategory.hom (H1Iso A).hom)
        ((ConcreteCategory.hom ((isoCycles₁ A).inv ≫ π A 1))
          ((ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (single g a)))) =
    Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
⊢ IsAdicComplete (Ideal.map e I) S ↔ IsAdicComplete I R

Tactic:
by
  simp [isAdicComplete_iff, IsHausdorff.congr_ringEquiv, IsPrecomplete.congr_ringEquiv]

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

Goal state before:
pp: case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < n✝ + 1
⊢ ↑((J ^ (n✝ + 1)) ^ m) ⊆ ↑(J ^ m)

Tactic:
rw [← pow_mul, Nat.succ_mul]

Goal state after:
case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < n✝ + 1
⊢ ↑(J ^ (n✝ * m + m)) ⊆ ↑(J ^ m)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : x = 0 ∧ k = 1
h2 : k = 1
⊢ 1 = (coeff x) 1

pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : x = 0 ∧ k = 1
h2 : ¬k = 1
⊢ 1 = (coeff x) 0

pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = 0 ∧ k = 1)
h3 : k = 1
⊢ 0 = (coeff x) 1

pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = 0 ∧ k = 1)
h3 : ¬k = 1
⊢ 0 = (coeff x) 0

Tactic:
· simp [h1.left]

Goal state after:
case neg
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : x = 0 ∧ k = 1
h2 : ¬k = 1
⊢ 1 = (coeff x) 0

case pos
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = 0 ∧ k = 1)
h3 : k = 1
⊢ 0 = (coeff x) 1

case neg
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = 0 ∧ k = 1)
h3 : ¬k = 1
⊢ 0 = (coeff x) 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
h1 : x = single j 1 ∧ k = 0
h2 : k = 0
⊢ 1 = (coeff x) (X j)

pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
h1 : x = single j 1 ∧ k = 0
h2 : ¬k = 0
⊢ 1 = (coeff x) 0

pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = single j 1 ∧ k = 0)
h3 : k = 0
⊢ 0 = (coeff x) (X j)

pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = single j 1 ∧ k = 0)
h3 : ¬k = 0
⊢ 0 = (coeff x) 0

Tactic:
· simp [h1.left]

Goal state after:
case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
h1 : x = single j 1 ∧ k = 0
h2 : ¬k = 0
⊢ 1 = (coeff x) 0

case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = single j 1 ∧ k = 0)
h3 : k = 0
⊢ 0 = (coeff x) (X j)

case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = single j 1 ∧ k = 0)
h3 : ¬k = 0
⊢ 0 = (coeff x) 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range

Tactic:
have he : e.Injective := fun x y hxy => by
    obtain ⟨(h₁ : s _ = s _), (h₂ : _ * _ = _ * _)⟩ := Prod.ext_iff.1 hxy
    exact (mul_right_inj _).1 (h₁ ▸ h₂)

Goal state after:
case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
he : Function.Injective e
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range
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ᵐᵒᵖ
⊢ (↑(TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ) ∘ₗ
        (rTensor Aᵐᵒᵖ (map ↑(opLinearEquiv R) ↑(opLinearEquiv R)) ∘ₗ
            rTensor Aᵐᵒᵖ comul ∘ₗ rTensor Aᵐᵒᵖ ↑(opLinearEquiv R).symm) ∘ₗ
          map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm)
      x✝ =
    (lTensor Aᵐᵒᵖ (map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm) ∘ₗ
        map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm)
      x✝

Tactic:
simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, lTensor_map, rTensor_def]

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ᵐᵒᵖ
⊢ (TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ)
      ((map (map ↑(opLinearEquiv R) ↑(opLinearEquiv R)) LinearMap.id)
        ((map comul LinearMap.id)
          ((map (↑(opLinearEquiv R).symm) LinearMap.id)
            ((map ↑(opLinearEquiv R) ↑(opLinearEquiv R)) (comul ((opLinearEquiv R).symm x✝)))))) =
    (map (↑(opLinearEquiv R))
        ((map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm) ∘ₗ ↑(opLinearEquiv R)))
      (comul ((opLinearEquiv R).symm x✝))
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : R
h1 : ∃ n ∈ p.support, a✝ = p.coeff n
⊢ a✝ ∈ ↑(span {p.content})

Tactic:
obtain ⟨n, _, h2⟩ := h1

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : R
n : ℕ
left✝ : n ∈ p.support
h2 : a✝ = p.coeff n
⊢ a✝ ∈ ↑(span {p.content})
Module: Mathlib.RingTheory.DedekindDomain.SInteger

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
x : K
⊢ x ∈ ∅.integer K ↔ x ∈ ⊥

Tactic:
simp only [Set.integer, Set.mem_empty_iff_false, not_false_eq_true, true_implies]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈
      {
        toSubsemiring :=
          ((⨅ v, ⨅ (_ : True), (HeightOneSpectrum.valuation K v).valuationSubring.toSubring).copy
              {x | ∀ (v : HeightOneSpectrum R), (HeightOneSpectrum.valuation K v) x ≤ 1} ⋯).toSubsemiring,
        algebraMap_mem' := ⋯ } ↔
    x ∈ ⊥
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M''
M''' : Type u_6
inst✝¹ : AddCommGroup M'''
inst✝ : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h : IsSMulRegular M''' r
this : IsSMulRegular (M'' ⧸ f₂.range) r
⊢ Exact ⇑((r • ⊤).mapQ (r • ⊤) f₁ ⋯) ⇑((r • ⊤).mapQ (r • ⊤) f₂ ⋯)

Tactic:
rw [Exact.exact_mapQ_iff h₁₂, map_pointwise_smul, Submodule.map_top, inf_comm]

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M''
M''' : Type u_6
inst✝¹ : AddCommGroup M'''
inst✝ : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h : IsSMulRegular M''' r
this : IsSMulRegular (M'' ⧸ f₂.range) r
⊢ r • ⊤ ⊓ f₂.range ≤ r • f₂.range
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
ι : Type u_4
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
a : ι → R
x : ι → M
⊢ ∑ x_1 ∈ s.sym q, ∏ x_2 ∈ s, a x_2 ^ Multiset.count x_2 ↑x_1 • dp R (Multiset.count x_2 ↑x_1) (x x_2) =
    ∑ k ∈ s.sym q, (∏ i ∈ s, a i ^ Multiset.count i ↑k) • ∏ i ∈ s, dp R (Multiset.count i ↑k) (x i)

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
a : ι → R
x : ι → M
⊢ ∑ x_1 ∈ s.sym q,
      ∏ x_2 ∈ s,
        (algebraMap R (DividedPowerAlgebra R M)) (a x_2 ^ Multiset.count x_2 ↑x_1) *
          dp R (Multiset.count x_2 ↑x_1) (x x_2) =
    ∑ x_1 ∈ s.sym q,
      (algebraMap R (DividedPowerAlgebra R M)) (∏ i ∈ s, a i ^ Multiset.count i ↑x_1) *
        ∏ i ∈ s, dp R (Multiset.count i ↑x_1) (x i)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.add
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m✝ m n : M
hm_mem : m ∈ Submodule.span R (Set.range v)
hn_mem : n ∈ Submodule.span R (Set.range v)
hm :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k m ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hn :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k n ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ x * dp R k (m + n) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
| add m n hm_mem hn_mem hm hn =>

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

Goal state before:
pp: A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
x : ι → M
hx : ∀ i ∈ s, x i ∈ I
n : ℕ
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
⊢ dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)

Tactic:
induction s using Finset.induction generalizing n with

Goal state after: