mathlib-initiative/mathlib-tactics huggingface dataset:
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
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
⊢ LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ⋯ ∘ₗ
      B.ρ g =
    (Representation.coind φ A.ρ) g ∘ₗ
      LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ⋯

Tactic:
by
    dsimp; ext; simp

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ Tendsto (fun n ↦ eLpNorm (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (x : Ω), X 0 x ∂μ) p μ) atTop (𝓝 0)

Tactic:
refine tendsto_Lp_finite_of_tendstoInMeasure hp hp' havg (memLp_const _) ?_
    (tendstoInMeasure_of_tendsto_ae havg (strong_law_ae _ hint hindep hident))

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ UnifIntegrable (fun n ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) p μ
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ UnifIntegrable (fun n ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) p μ

Tactic:
rw [(_ : (fun (n : ℕ) ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω))
            = fun (n : ℕ) => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i))]

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ UnifIntegrable (fun n ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i) p μ

Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ (fun n ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) = fun n ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i
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
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
S✝ : Type u_6
inst✝⁹ : Monoid S✝
inst✝⁸ : DistribMulAction S✝ W
inst✝⁷ : SMulCommClass R S✝ W
inst✝⁶ : ContinuousConstSMul S✝ W
inst✝⁵ : LinearMap.CompatibleSMul W W S✝ R
S : Type u_7
inst✝⁴ : Ring S
inst✝³ : Module S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝³ x✝² : S
x✝¹ : π₁ →ⁱL π₂
x✝ : V
⊢ ((x✝³ + x✝²) • x✝¹).toContinuousLinearMap x✝ = (x✝³ • x✝¹ + x✝² • x✝¹).toContinuousLinearMap x✝

Tactic:
simp [add_smul]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Basic

Goal state before:
pp: case succ
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι -
      (ofHom (X.resolutionX (n + 1)).ρ.coind₁ι - (coind₁Functor k G).map (X.d n)) ≫
        (coind₁Functor k G).map (X.d (n + 1)) =
    0

Tactic:
rw [Preadditive.sub_comp, ← Functor.map_comp, ih, Functor.map_zero, sub_zero, sub_eq_zero]

Goal state after:
case succ
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι =
    ofHom (X.resolutionX (n + 1)).ρ.coind₁ι ≫ (coind₁Functor k G).map (X.d (n + 1))
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
X✝ Y✝ : Rep k G
f : X✝ ⟶ Y✝
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      f ≫ (HomologicalComplex.alternatingConst Y✝ ⋯ ⋯ ⋯).d i j =
        (HomologicalComplex.alternatingConst X✝ ⋯ ⋯ ⋯).d i j ≫ f

Tactic:
rintro i j ⟨rfl⟩

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
X✝ Y✝ : Rep k G
f : X✝ ⟶ Y✝
j : ℕ
⊢ f ≫ (HomologicalComplex.alternatingConst Y✝ ⋯ ⋯ ⋯).d (j + 1) j =
    (HomologicalComplex.alternatingConst X✝ ⋯ ⋯ ⋯).d (j + 1) j ≫ f
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 j : ℕ),
    (ComplexShape.up ℕ).Rel i j →
      A.leftRegularHomEquiv.toModuleIso.hom ≫ (moduleCatCochainComplex A g).d i j =
        ((resolution k g hg).complex.linearYonedaObj k A).d i j ≫ A.leftRegularHomEquiv.toModuleIso.hom

Tactic:
rintro i j ⟨rfl⟩

Goal state after:
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 : ℕ
⊢ A.leftRegularHomEquiv.toModuleIso.hom ≫ (moduleCatCochainComplex A g).d i (i + 1) =
    ((resolution k g hg).complex.linearYonedaObj k A).d i (i + 1) ≫ A.leftRegularHomEquiv.toModuleIso.hom
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
y : ↑X.X₂
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
⊢ (fun x ↦ ⇑(Rep.Hom.hom X.f) ∘ x) ((ModuleCat.Hom.hom (d₁₂ X.X₁)) x) = (fun x ↦ ⇑(Rep.Hom.hom X.f) ∘ x) 0

Tactic:
have := congr($((mapShortComplexH1 (MonoidHom.id G) X.f).comm₂₃.symm) x)

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
y : ↑X.X₂
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
this :
  (ConcreteCategory.hom ((shortComplexH1 X.1).g ≫ (mapShortComplexH1 (MonoidHom.id G) X.f).τ₃)) x =
    (ConcreteCategory.hom ((mapShortComplexH1 (MonoidHom.id G) X.f).τ₂ ≫ (shortComplexH1 X.X₂).g)) x
⊢ (fun x ↦ ⇑(Rep.Hom.hom X.f) ∘ x) ((ModuleCat.Hom.hom (d₁₂ X.X₁)) x) = (fun x ↦ ⇑(Rep.Hom.hom X.f) ∘ x) 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ cocyclesMk ((ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x) ⋯ = (ConcreteCategory.hom (isoCocycles₂ A).inv) x

Tactic:
by
  apply_fun (forget₂ _ Ab).map ((inhomogeneousCochains A).iCycles 2) using
    (AddCommGrpCat.mono_iff_injective _).1 <| (forget₂ _ _).map_mono _
  rw [HomologicalComplex.i_cyclesMk]
  simp; rfl

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
n : ℕ
⊢ cocyclesMap (MonoidHom.id G) (φ ≫ ψ) n = cocyclesMap (MonoidHom.id G) φ n ≫ cocyclesMap (MonoidHom.id G) ψ n

Tactic:
by
  simp [cocyclesMap, cochainsMap_id_comp, HomologicalComplex.cyclesMap_comp]

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 : ℕ
⊢ ((X.map (chainsFunctor k G)).map (HomologicalComplex.eval (ModuleCat k) (ComplexShape.down ℕ) i)).Exact

Tactic:
have : LinearMap.range X.f.hom.toLinearMap = LinearMap.ker X.g.hom.toLinearMap :=
        (hX.exact.map (forget₂ (Rep k G) (ModuleCat k))).moduleCat_range_eq_ker
      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
y : G × G →₀ ↑X.X₂
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
⊢ (Rep.Hom.hom X.f) ((ModuleCat.Hom.hom (d₁₀ X.X₁)) x) = (Rep.Hom.hom X.f) 0

Tactic:
have := congr($((mapShortComplexH1 (MonoidHom.id G) X.f).comm₂₃.symm) x)

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
y : G × G →₀ ↑X.X₂
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
this :
  (ConcreteCategory.hom ((shortComplexH1 X.X₁).g ≫ (mapShortComplexH1 (MonoidHom.id G) X.f).τ₃)) x =
    (ConcreteCategory.hom ((mapShortComplexH1 (MonoidHom.id G) X.f).τ₂ ≫ (shortComplexH1 X.2).g)) x
⊢ (Rep.Hom.hom X.f) ((ModuleCat.Hom.hom (d₁₀ X.X₁)) x) = (Rep.Hom.hom X.f) 0
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ := fun t ↦ Nat.rec g (fun x G' ↦ mk fun p ↦ (coeff (p + 1)) G' - ∑ i, T G' i * (coeff (p + 1)) (F i)) t
hG : ∀ (n : ℕ), G n ∈ I
hG' : ∀ (n_1 : ℕ), G n_1 - ∑ i, C (T (G n_1) i) * F i = X * G (n_1 + 1)
H : Fin n → R⟦X⟧ := fun i ↦ mk fun n ↦ T (G n) i
h₁ : ∀ (n_1 : ℕ), g - ∑ i, ↑((trunc n_1) (H i)) * F i = X ^ n_1 * G n_1
⊢ g ∈ Submodule.span R⟦X⟧ (Set.range F)

Tactic:
have h₂ : g = ∑ i, H i * F i := by
    ext n; simpa [coeff_trunc, sub_eq_zero] using congr(($(h₁ (n + 1)).trunc (n + 1)).coeff n)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ := fun t ↦ Nat.rec g (fun x G' ↦ mk fun p ↦ (coeff (p + 1)) G' - ∑ i, T G' i * (coeff (p + 1)) (F i)) t
hG : ∀ (n : ℕ), G n ∈ I
hG' : ∀ (n_1 : ℕ), G n_1 - ∑ i, C (T (G n_1) i) * F i = X * G (n_1 + 1)
H : Fin n → R⟦X⟧ := fun i ↦ mk fun n ↦ T (G n) i
h₁ : ∀ (n_1 : ℕ), g - ∑ i, ↑((trunc n_1) (H i)) * F i = X ^ n_1 * G n_1
h₂ : g = ∑ i, H i * F i
⊢ g ∈ Submodule.span R⟦X⟧ (Set.range F)
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
⊢ ∃ T, I = span T ∧ T.Finite ∧ T.ncard = S.ncard

Tactic:
have : SurjOn constantCoeff I S := by
    intro r hr
    simpa [mem_map_iff_of_surjective _ constantCoeff_surj, hSI] using subset_span hr
  obtain ⟨T, hTI, hinj, hT⟩ := this.exists_subset_injOn_image_eq
  refine ⟨T, eq_of_le_of_X_notMem_of_fg_of_isPrime (span_le.2  hTI) hI (Submodule.fg_def.2
    ⟨T, (hT ▸ hS).of_finite_image hinj, rfl⟩) ?_, Finite.of_injOn
    (fun f hf ↦ hT ▸ Set.mem_image_of_mem _ hf) hinj hS, hT ▸ hinj.ncard_image.symm⟩
  rw [map_le_iff_le_comap]
  intro f hf
  rw [mem_comap, mem_map_iff_of_surjective _ constantCoeff_surj]
  replace hf : constantCoeff f ∈ span S := hSI ▸ Ideal.mem_map_of_mem constantCoeff hf
  refine Submodule.span_induction (fun s hs ↦ ?_) ⟨0, zero_mem _, by simp⟩ ?_ ?_ hf
  · obtain ⟨t, htmem, ht⟩ := hT ▸ hs
    exact ⟨t, subset_span htmem, ht⟩
  · intro r₁ r₂ hr₁ hr₂ ⟨s₁, hs₁mem, hs₁⟩ ⟨s₂, hs₂mem, hs₂⟩
    exact ⟨s₁ + s₂, Ideal.add_mem _ hs₁mem hs₂mem, by simp [hs₁, hs₂]⟩
  · intro r₁ r₂ hr₁ ⟨f, hfmem, hf⟩
    exact ⟨r₁ • f, Submodule.smul_of_tower_mem _ _ hfmem, by simp [hf]⟩

Goal state after:
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
mapeq :
  Ideal.map (algebraMap R (AdicCompletion I R)) m = comap (evalOneₐ I).toRingHom (Ideal.map (Ideal.Quotient.mk I) m)
this : (Ideal.map (Ideal.Quotient.mk I) m).IsMaximal
⊢ (Ideal.map (algebraMap R (AdicCompletion I R)) m).IsMaximal

Tactic:
rw [mapeq]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I m : Ideal R
inst✝ : m.IsMaximal
le : I ≤ m
fg : I.FG
mapeq :
  Ideal.map (algebraMap R (AdicCompletion I R)) m = comap (evalOneₐ I).toRingHom (Ideal.map (Ideal.Quotient.mk I) m)
this : (Ideal.map (Ideal.Quotient.mk I) m).IsMaximal
⊢ (comap (evalOneₐ I).toRingHom (Ideal.map (Ideal.Quotient.mk I) m)).IsMaximal
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)) ⋯
m : (maximalIdeal R).Cotangent
m' : ↥(maximalIdeal R)
hm' : (maximalIdeal R).toCotangent m' = m
hm : (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' ∈ (eval (maximalIdeal R) R 2).ker
⊢ m = 0

Tactic:
have : (algebraMap R (AdicCompletion (maximalIdeal R) R)) m'.1 = of _ R m'.1 := rfl

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)) ⋯
m : (maximalIdeal R).Cotangent
m' : ↥(maximalIdeal R)
hm' : (maximalIdeal R).toCotangent m' = m
hm : (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' ∈ (eval (maximalIdeal R) R 2).ker
this : (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' = (of (maximalIdeal R) R) ↑m'
⊢ m = 0
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)) ⋯
m : (maximalIdeal R).Cotangent
m' : ↥(maximalIdeal R)
hm' : (maximalIdeal R).toCotangent m' = m
hm : (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' ∈ (eval (maximalIdeal R) R 2).ker
this : (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' = (of (maximalIdeal R) R) ↑m'
⊢ m = 0

Tactic:
simp only [smul_eq_mul, eval, this, LinearMap.mem_ker, LinearMap.coe_mk, AddHom.coe_mk,
      of_apply, Submodule.mkQ_apply, mk_eq_mk, Ideal.Quotient.eq_zero_iff_mem] at hm

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)) ⋯
m : (maximalIdeal R).Cotangent
m' : ↥(maximalIdeal R)
hm' : (maximalIdeal R).toCotangent m' = m
this : (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' = (of (maximalIdeal R) R) ↑m'
hm : ↑m' ∈ maximalIdeal R ^ 2 * ⊤
⊢ m = 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_2
τ : Type u_3
inst✝¹ : CommSemiring R
f : σ → τ
inst✝ : TendstoCofinite f
a : σ
⊢ (rename f).comp (toMvPowerSeries a) = toMvPowerSeries (f a)

Tactic:
by
  ext
  simp [toMvPowerSeries_apply, comp_def]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Denominator

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
n : ℕ
x : S
⊢ (denominator ℤ x).natAbs ∣ n ↔ IsIntegral ℤ (n • x)

Tactic:
← Int.ofNat_dvd_right,

Goal state after:
S : Type u_2
inst✝ : CommRing S
n : ℕ
x : S
⊢ denominator ℤ x ∣ ↑n ↔ IsIntegral ℤ (n • x)
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)
x : G ⧸ S →₀ ↑(A.ofQuotient S)
hx : x ∈ cycles₁ (A.ofQuotient S)
⊢ ∃ a, (ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) a = ⟨x, hx⟩

Tactic:
choose! s hs using QuotientGroup.mk_surjective (s := S)

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)
x : G ⧸ S →₀ ↑(A.ofQuotient S)
hx : x ∈ cycles₁ (A.ofQuotient S)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), ↑(s b) = b
⊢ ∃ a, (ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) a = ⟨x, hx⟩
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hx : ↑x n = 0
⊢ x ∈ restrictScalars R (ofPowSMul I M n).range

Tactic:
use ofValEqZero I hx

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hx : ↑x n = 0
⊢ (ofPowSMul I M n) (ofValEqZero I hx) = x
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case w
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↥(cycles₁ (res S.subtype (A.toCoinvariants S)))
hz :
  (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
w : ↑(ModuleCat.of k (G × G →₀ ↑(A.toCoinvariants S)))
hzw :
  (ModuleCat.Hom.hom (d₂₁ (A.toCoinvariants S))) w =
    ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) -
      ↑((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
Z : ↥S →₀ ↑A
hZ : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Z = ↑z
W : G × G →₀ ↑A
hW : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ W = w
b : G →₀ ↑A := ↑x + (ConcreteCategory.hom (d₂₁ A)) W - (lmapDomain (↑A) k ⇑S.subtype) Z
hb : ∀ (g : G), b g ∈ Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)
β : G →₀ ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)) :=
  mapRange (Function.invFun ⇑(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype) ⋯ b
hβb : mapRange Subtype.val ⋯ β = b
α : ↥S →₀ ↑A
hα :
  (ModuleCat.Hom.hom (shortComplexH1 A).pOpcycles ∘ₗ
        ModuleCat.Hom.hom (mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂)
      α =
    (ModuleCat.Hom.hom (shortComplexH1 A).pOpcycles ∘ₗ
        ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂)
      β
δ : G × G →₀ ↑A
hβ :
  (ModuleCat.Hom.hom (shortComplexH1 A).f) δ =
    (ModuleCat.Hom.hom (mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂) α -
      (ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂) β
hαZ : (ConcreteCategory.hom (d₂₁ A)) (W + δ) = mapDomain Subtype.val (α + Z) - ↑x
this : ↑x + (ConcreteCategory.hom (d₂₁ A)) (W + δ) ∈ cycles₁ A
⊢ ((α + Z).sum fun g a ↦ ((res S.subtype A).ρ g⁻¹) a) = (α + Z).sum fun x a ↦ a

Tactic:
rwa [eq_sub_iff_add_eq'.1 hαZ, mem_cycles₁_iff, sum_mapDomain_index_inj
      Subtype.val_injective, sum_mapDomain_index_inj Subtype.val_injective] at this

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

Goal state before:
pp: case neg.mpr
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
h : ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1
n : ℕ
⊢ n ∈ p.support → (v.intAdicAbv hb) (p.coeff n) < 1

Tactic:
hn

Goal state after:
case neg.mpr
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
h : ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1
n : ℕ
hn : n ∈ p.support
⊢ (v.intAdicAbv hb) (p.coeff n) < 1