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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω' : Ω'
h1 : (κ ω') {ω | 0 < (-X) ω} = 0
h2 : (κ ω') {ω | 0 < X ω} = 0
⊢ X =ᵐ[κ ω'] 0

Tactic:
Pi.neg_apply,

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω' : Ω'
h1 : (κ ω') {ω | 0 < -X ω} = 0
h2 : (κ ω') {ω | 0 < X ω} = 0
⊢ X =ᵐ[κ ω'] 0
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : cX = 0
⊢ HasSubgaussianMGF (fun ω ↦ X ω + Y ω) ((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) κ ν

Tactic:
simp only [hX0, NNReal.sqrt_zero, zero_add, NNReal.sq_sqrt] at hX ⊢
    refine hY.congr ?_
    filter_upwards [ae_eq_zero_of_hasSubgaussianMGF_zero' hX] with ω hX0 using by simp [hX0]

Goal state after:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁴ : Zero E
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable 𝓕 p
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))
n : ℕ
⊢ p fun i ↦
    {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator
      (stoppedProcess (stoppedProcess X fun ω ↦ τ n ω) (fun x ↦ ⨅ j, ⨅ (_ : j ≥ n), τ j x) i)

Tactic:
← stoppedProcess_indicator_comm'

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁴ : Zero E
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable 𝓕 p
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))
n : ℕ
⊢ p
    (stoppedProcess (fun i ↦ {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (stoppedProcess X (fun ω ↦ τ n ω) i)) fun x ↦
      ⨅ j, ⨅ (_ : j ≥ n), τ j x)
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 ρ
⊢ ∫ (x : ℝ) in 0..↑N, x + 1 ∂ρ = ∫ (x : ℝ) in 0..↑N, x ∂ρ + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ

Tactic:
intervalIntegral.integral_add

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 ρ
⊢ ∫ (x : ℝ) in 0..↑N, x ∂ρ + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ = ∫ (x : ℝ) in 0..↑N, x ∂ρ + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ

case hf
Ω : 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 ρ
⊢ IntervalIntegrable (fun x ↦ x) ρ 0 ↑N

case hg
Ω : 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 ρ
⊢ IntervalIntegrable (fun x ↦ 1) ρ 0 ↑N
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e_f.e_a
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
j : ℕ
⊢ ∫ (x : ℝ) in 0..↑j, x ^ 2 ∂ρ = ∑ k ∈ range j, ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

Tactic:
intervalIntegral.sum_integral_adjacent_intervals

Goal state after:
case e_f.e_a
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
j : ℕ
⊢ ∫ (x : ℝ) in 0..↑j, x ^ 2 ∂ρ = ∫ (x : ℝ) in ↑0..↑j, x ^ 2 ∂ρ

case e_f.e_a
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
j : ℕ
⊢ ∀ k < j, IntervalIntegrable (fun x ↦ x ^ 2) ρ ↑k ↑(k + 1)
Module: Mathlib.Probability.Moments.SubGaussian

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

Tactic:
simp [mgf]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Res

Goal state before:
pp: k✝ : Type u
inst✝³ : Semiring k✝
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
f : H →* G
M : Rep k✝ G
k : Type u
inst✝ : CommSemiring k
x✝³ x✝² : Rep k G
x✝¹ : x✝³ ⟶ x✝²
x✝ : k
⊢ (Hom.hom ((resFunctor f).map (x✝ • x✝¹))).toLinearMap = (Hom.hom (x✝ • (resFunctor f).map x✝¹)).toLinearMap

Tactic:
simp [smul_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G✝ : Type v
H : Type w
inst✝⁴ : CommRing k
inst✝³ : Monoid G✝
inst✝² : Monoid H
φ : G✝ →* H
A : Rep k G✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
this : Setoid G := QuotientGroup.rightRel S
s : ↑Y → ↑X
hs : ∀ (b : ↑Y), (Hom.hom f) (s b) = b
⊢ ∃ a, (Hom.hom ((coindFunctor k S.subtype).map f)) a = y

Tactic:
choose! i hi using Quotient.mk'_surjective (α := G)

Goal state after:
k : Type u
G✝ : Type v
H : Type w
inst✝⁴ : CommRing k
inst✝³ : Monoid G✝
inst✝² : Monoid H
φ : G✝ →* H
A : Rep k G✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
this : Setoid G := QuotientGroup.rightRel S
s : ↑Y → ↑X
hs : ∀ (b : ↑Y), (Hom.hom f) (s b) = b
i : Quotient this → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
⊢ ∃ a, (Hom.hom ((coindFunctor k S.subtype).map f)) a = y
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
x✝¹ : k
x✝ : ↥(Representation.coindV φ A.ρ)
⊢ ∀ (h : H),
    (Hom.hom
            (ofHom
              { toLinearMap := linearCombination k ↑(x✝¹ • x✝) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k),
                isIntertwining' := ⋯ })).toLinearMap
        (MonoidAlgebra.single h 1) =
      (Hom.hom
            ((RingHom.id k) x✝¹ •
              ofHom
                { toLinearMap := linearCombination k ↑x✝ ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k),
                  isIntertwining' := ⋯ })).toLinearMap
        (MonoidAlgebra.single h 1)

Tactic:
simp [smul_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁹ : CommRing k
G : Type u_2
inst✝⁸ : Group G
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module k[G] V
inst✝⁴ : IsScalarTower k k[G] V
W : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module k[G] W
inst✝ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
h : ∀ (v : V), π (i v) = v
g : G
v : V
⊢ (MonoidAlgebra.single g⁻¹ 1 * MonoidAlgebra.single g 1) • v = v

Tactic:
single_mul_single,

Goal state after:
k : Type u_1
inst✝⁹ : CommRing k
G : Type u_2
inst✝⁸ : Group G
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module k[G] V
inst✝⁴ : IsScalarTower k k[G] V
W : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module k[G] W
inst✝ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
h : ∀ (v : V), π (i v) = v
g : G
v : V
⊢ MonoidAlgebra.single (g⁻¹ * g) (1 * 1) • v = v
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommSemiring k
inst✝ : Monoid G
M N : Rep k G
⊢ ∀ (c : k) (x : M ⟶ N),
    { toFun := Hom.hom, map_zero' := ⋯, map_add' := ⋯ } (c • x) =
      c • { toFun := Hom.hom, map_zero' := ⋯, map_add' := ⋯ } x

Tactic:
simp [smul_hom]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Rep k G
f : X ⟶ Y
r : k
x✝ : ↑((forget₂ (Rep k G) (ModuleCat k)).obj X)
⊢ (ModuleCat.Hom.hom ((forget₂ (Rep k G) (ModuleCat k)).map (r • f))) x✝ =
    (ModuleCat.Hom.hom (r • (forget₂ (Rep k G) (ModuleCat k)).map f)) x✝

Tactic:
simp [smul_hom]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝⁴ x✝³ x✝² : Rep k G
x✝¹ : k
x✝ : x✝³ ⟶ x✝²
⊢ Hom.hom (x✝⁴ ◁ (x✝¹ • x✝)) = Hom.hom (x✝¹ • x✝⁴ ◁ x✝)

Tactic:
simp [smul_hom]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝⁴ : k
x✝³ x✝² : Rep k G
x✝¹ : x✝³ ⟶ x✝²
x✝ : Rep k G
⊢ Hom.hom ((x✝⁴ • x✝¹) ▷ x✝) = Hom.hom (x✝⁴ • x✝¹ ▷ x✝)

Tactic:
simp [smul_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inl
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ : G
a : ↑A
s : ↥S
⊢ (B.indToCoindAux g₁) ((Hom.hom f) a) ((fun m ↦ m • g₁) s) = (Hom.hom f) ((A.indToCoindAux g₁) a ((fun m ↦ m • g₁) s))

pp: case inr
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ g₂ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) g₂ g₁
⊢ (B.indToCoindAux g₁) ((Hom.hom f) a) g₂ = (Hom.hom f) ((A.indToCoindAux g₁) a g₂)

Tactic:
· simp [S.1.smul_def, hom_comm_apply]

Goal state after:
case inr
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ g₂ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) g₂ g₁
⊢ (B.indToCoindAux g₁) ((Hom.hom f) a) g₂ = (Hom.hom f) ((A.indToCoindAux g₁) a g₂)
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

Goal state before:
pp: case succ
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
i : ℕ
ih :
  (Hom.hom (Y.d i)).comp (Hom.hom (resolutionMap φ f i)) =
    (coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i)))
⊢ (Y.resolutionX i).ρ.coind₁.coind₁ι.comp (coind₁ResMap φ (Hom.hom (resolutionMap φ f i))) -
      coind₁ResMap φ ((Hom.hom (Y.d i)).comp (Hom.hom (resolutionMap φ f i))) =
    (coind₁ResMap φ (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))).comp
        (ContIntertwiningMap.restrict (↑φ) (X.resolutionX i).ρ.coind₁.coind₁ι) -
      coind₁ResMap φ
        ((coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i))))

Tactic:
rw [ih, ← coind₁ResMap_comp_coind₁ι_restrict]

Goal state after:
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
⊢ cochainsMap (ContinuousMonoidHom.id G) (𝟙 X) = 𝟙 X.homogeneousCochains

Tactic:
ext i : 1
  rw [cochainsMap_f, resolutionMap_id]
  ext v
  rfl

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

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
inst✝ : NeZero i
hi : Even i
x : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupCohomologyπEven A g hg i hi)) x = 0 ↔ ↑x ∈ (Hom.hom A.norm).range

Tactic:
simp [groupCohomologyπEven, map_eq_zero_iff _ ((ModuleCat.mono_iff_injective _).1 inferInstance),
    moduleCatToCycles, -LinearMap.mem_range, LinearMap.range_codRestrict]

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

Goal state before:
pp: k G✝ : Type u
inst✝² : CommRing k
n✝ : ℕ
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Group G
n : ℕ
⊢ Projective ((standardComplex k G).X n)

Tactic:
exact inferInstanceAs <| Projective (Rep.diagonal k G (n + 1))

Goal state after:
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
⊢ H1π A ≫ (H1IsoOfIsTrivial A).hom = (cocycles₁IsoOfIsTrivial A).hom

Tactic:
by
  simp [H1IsoOfIsTrivial, H1π]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
⊢ (killCompl e).comp (rename ⇑e) = AlgHom.id R (MvPowerSeries σ R)

Tactic:
ext; simp [coeff_killCompl]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
e : σ ↪ τ
φ : R →+* S
p : MvPowerSeries τ R
⊢ (killCompl e) ((map φ) p) = (map φ) ((killCompl e) p)

Tactic:
ext; simp [coeff_killCompl]

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

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

Tactic:
replace hfg : (Ideal.map constantCoeff I).FG := by
    have : RingHomSurjective (constantCoeff (R := R)) := ⟨constantCoeff_surj⟩
    exact map_eq_submodule_map constantCoeff I ▸ Submodule.FG.map _ hfg

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I) + 1
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
i j : ℕ
⊢ ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j

Tactic:
exact ⟨max i j, pow_le_pow_right (le_max_left i j), pow_le_pow_right (le_max_right i j)⟩

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

Goal state before:
pp: case mp
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
⊢ ((∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s) → DiscreteTopology A

pp: case mpr
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
⊢ DiscreteTopology A → (∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s

Tactic:
· rintro ⟨h, _h'⟩
    rw [discreteTopology_iff_isOpen_singleton_zero]
    simpa using h 1

Goal state after:
case mpr
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
⊢ DiscreteTopology A → (∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPowerSeries (Fin (n + 1)) R
k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff x) ((PowerSeries.coeff k) ((optionEquivLeft (Fin n) R) ((rename ⇑(_root_.finSuccEquiv n)) p))) =
    (coeff (Finsupp.cons k x)) p

Tactic:
← Equiv.coe_toEmbedding,

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPowerSeries (Fin (n + 1)) R
k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff x) ((PowerSeries.coeff k) ((optionEquivLeft (Fin n) R) ((rename ⇑(_root_.finSuccEquiv n).toEmbedding) p))) =
    (coeff (Finsupp.cons k x)) p
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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e.symm).comp ↑e)
      (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ } ≫
        (resFunctor ↑e).map (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }))
      n =
    𝟙 (groupHomology A n)

Tactic:
← groupHomology.map_id

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

Tactic:
← groupHomology.map_id

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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e).comp ↑e.symm)
      (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ } ≫
        (resFunctor ↑e.symm).map (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }))
      n =
    map (MonoidHom.id H) (𝟙 B) n
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ᵐᵒᵖ
⊢ (map (counit ∘ₗ ↑(opLinearEquiv R).symm ∘ₗ ↑(opLinearEquiv R)) ↑(opLinearEquiv R))
      (comul (↑(opLinearEquiv R).symm x✝)) =
    ((TensorProduct.mk R R Aᵐᵒᵖ) 1) x✝

Tactic:
simp [← lTensor_comp_rTensor]

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
⊢ mapShortComplexH2 f 0 = 0

Tactic:
refine ShortComplex.hom_ext _ _ ?_ ?_ ?_
  all_goals
  { simp only [shortComplexH2]
    ext
    simp }

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
r : R
reg : IsSMulRegular (↑M) r
⊢ Mono (M.smulShortComplex r).f

Tactic:
by simpa [ModuleCat.smulShortComplex, ModuleCat.mono_iff_injective] using! reg

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ mapShortComplexH2 (MonoidHom.id G) (𝟙 A) = 𝟙 (shortComplexH2 A)

Tactic:
refine ShortComplex.hom_ext _ _ ?_ ?_ ?_
  all_goals
  { simp only [shortComplexH2]
    ext
    simp }

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

Goal state before:
pp: case dp.mem
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 y : M
hy : y ∈ Set.range v
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 y ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
obtain ⟨i, rfl⟩ := hy

Goal state after:
case dp.mem
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
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
i : ι
⊢ x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ k ! * (m ! * (m + k).choose k) = k ! * (m ! * (m + k).choose m)

Tactic:
Nat.choose_symm_add

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ k ! * (m ! * (m + k).choose k) = k ! * (m ! * (m + k).choose k)
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case mpr.h1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ ((x ^ n) ^ 2).fst = fst 0

pp: case mpr.h2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ ((x ^ n) ^ 2).snd = snd 0

Tactic:
· rw [fst_pow, fst_pow, hn, zero_pow two_ne_zero, fst_zero]

Goal state after:
case mpr.h2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ ((x ^ n) ^ 2).snd = snd 0
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J

Tactic:
rintro y ⟨x, hx, rfl⟩
    exact hf.1 (mem_map_of_mem f (hK.1 hx))

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Field k
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra k R
inst✝³ : Algebra R S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : IsFiniteSplit R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ IsFiniteSplit T (T ⊗[R] S)

Tactic:
refine ⟨n, ⟨?_⟩⟩

Goal state after:
k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Field k
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra k R
inst✝³ : Algebra R S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : IsFiniteSplit R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ T ⊗[R] S ≃ₐ[T] Fin n → T
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit R S
⊢ Module.Free R S

Tactic:
by
  obtain ⟨n, ⟨e⟩⟩ := nonempty_algEquiv_fun R S
  exact Module.Free.of_equiv e.symm.toLinearEquiv

Goal state after: