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

Goal state before:
pp: Ω : 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 ∂ρ
k : ℕ
a✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
x : ℝ
hx : x ∈ Set.Ioc ↑k ↑(k + 1)
this : 0 < x
⊢ x / (↑k + 1) * (2 * x) ≤ 1 * (2 * x)

Tactic:
gcongr

Goal state after:
case hbc
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := ⋯
ρ : Measure ℝ := ⋯
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
x : ℝ
hx : x ∈ Set.Ioc ↑k ↑(k + 1)
this : 0 < x
⊢ x / (↑k + 1) ≤ 1
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
⊢ HasSubgaussianMGF (-X) c μ

Tactic:
simpa [HasSubgaussianMGF_iff_kernel] using (HasSubgaussianMGF_iff_kernel.1 h).neg

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ mgf X μ t * mgf Y μ t ≤ rexp (↑cX * t ^ 2 / 2) * rexp (↑cY * t ^ 2 / 2)

Tactic:
gcongr

Goal state after:
case c0
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ 0 ≤ mgf Y μ t

case h₁
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ mgf X μ t ≤ rexp (↑cX * t ^ 2 / 2)

case h₂
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ mgf Y μ t ≤ rexp (↑cY * t ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (fun ω ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * t ^ 2 / 2
⊢ iteratedDeriv 2 (cgf X μ) u * t ^ 2 / 2 ≤ (↑‖b - a‖₊ / 2) ^ 2 * t ^ 2 / 2

Tactic:
gcongr

Goal state after:
case hbc
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (fun ω ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * t ^ 2 / 2
⊢ iteratedDeriv 2 (cgf X μ) u ≤ (↑‖b - a‖₊ / 2) ^ 2
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f : ρ.IntertwiningMap σ
m : A[G]
v : ρ.asModule
⊢ f.toLinearMap (m • v) = (RingHom.id A[G]) m • f.toLinearMap v

Tactic:
by
        induction m using MonoidAlgebra.induction_linear with
          | zero => simp [f.toLinearMap.map_zero]
          | add x y hx hy => simp [add_smul, map_add, hx, hy]
          | single g a => simp [f.isIntertwining]; rfl

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝¹ : StandardBorelSpace Ω
inst✝ : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : HasSubgaussianMGF X cX (μ.trim hm)
hY : HasCondSubgaussianMGF m hm Y cY μ
this : HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (cX + cY) (Measure.map Function.diag μ)
h_eq : X + Y = (fun p ↦ X p.1 + Y p.2) ∘ Function.diag
⊢ AEMeasurable Function.diag μ

Tactic:
exact @Measurable.aemeasurable _ _ _ (m.prod mΩ) _ _
      ((measurable_id'' hm).prodMk measurable_id)

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f₁ f₂ : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
⊢ (f₁ + f₂).tensor g = f₁.tensor g + f₂.tensor g

Tactic:
ext; simp [TensorProduct.add_tmul]

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)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N : ℕ
⊢ ε⁻¹ ^ 2 * ∑ i ∈ range N, (↑(u i))⁻¹ ^ 2 * Var[S (u i); ℙ] ≤ ε⁻¹ ^ 2 * C

Tactic:
gcongr

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

Tactic:
simp only [Nat.one_le_cast, Nat.one_le_floor_iff, one_le_pow₀ c_one.le]

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Group G
X Y : FDRep k G
⊢ ↥(linHom X.ρ Y.ρ).invariants ≃ₗ[k] X ⟶ Y

Tactic:
rw [← FDRep.forget₂_ρ, ← FDRep.forget₂_ρ]

Goal state after:
k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Group G
X Y : FDRep k G
⊢ ↥(((forget₂ (FDRep k G) (Rep k G)).obj X).ρ.linHom ((forget₂ (FDRep k G) (Rep k G)).obj Y).ρ).invariants ≃ₗ[k] X ⟶ Y
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S✝ : Subgroup G
inst✝¹ : S✝.Normal
S : Subgroup G
inst✝ : S.Normal
X Y : Rep k G
f : X ⟶ Y
g✝ : G ⧸ S
g : G
x✝ : ↥(invariants (MonoidHom.comp X.ρ S.subtype))
⊢ ↑((ModuleCat.Hom.hom ((invariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)) ∘ₗ (X.ρ.quotientToInvariants S) ↑g)
        x✝) =
    ↑(((Y.ρ.quotientToInvariants S) ↑g ∘ₗ
          ModuleCat.Hom.hom ((invariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)))
        x✝)

Tactic:
simp [hom_comm_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Field k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : FiniteDimensional k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
this : Invertible ↑(Fintype.card G)
⊢ (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g = ↑(finrank k ↥ρ.invariants)

Tactic:
rw [← (isProj_averageMap ρ).trace]

Goal state after:
G : Type u_1
k : Type u_2
V : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Field k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : FiniteDimensional k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
this : Invertible ↑(Fintype.card G)
⊢ (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g = (trace k V) ρ.averageMap
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Monoid G✝
A B : Rep k✝ G✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X Y : Rep k G
f : X ⟶ Y
g✝ : G ⧸ S
g : G
x✝ : ↑X
⊢ ((ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)) ∘ₗ
          ((X.toCoinvariants S).ρ.ofQuotient S) ↑g) ∘ₗ
        Coinvariants.mk (MonoidHom.comp X.ρ S.subtype))
      x✝ =
    ((((Y.toCoinvariants S).ρ.ofQuotient S) ↑g ∘ₗ
          ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f))) ∘ₗ
        Coinvariants.mk (MonoidHom.comp X.ρ S.subtype))
      x✝

Tactic:
simp [hom_comm_apply]

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

Goal state before:
pp: k : Type u
inst✝¹ : Semiring k
G : Type v
inst✝ : CommMonoid G
A B : Rep k G
f : A ⟶ B
g : G
x✝ : ↑A
⊢ (Hom.hom (A.applyAsHom g ≫ f)).toLinearMap x✝ = (Hom.hom (f ≫ B.applyAsHom g)).toLinearMap x✝

Tactic:
simp [hom_comm_apply]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X✝ Y✝ : Rep k G
f : X✝ ⟶ Y✝
g : G
⊢ ModuleCat.Hom.hom
      ({ V := ModuleCat.of k ↑X✝, ρ := (ModuleCat.of k ↑X✝).endRingEquiv.symm.toMonoidHom.comp X✝.ρ }.ρ g ≫
        Hom.toModuleCatHom f) =
    ModuleCat.Hom.hom
      (Hom.toModuleCatHom f ≫
        { V := ModuleCat.of k ↑Y✝, ρ := (ModuleCat.of k ↑Y✝).endRingEquiv.symm.toMonoidHom.comp Y✝.ρ }.ρ g)

Tactic:
by
    simp [ModuleCat.endRingEquiv, f.hom.2]

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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ✝ φ : ρ.Equiv σ
ψ : σ.Equiv τ
g : G
⊢ (↑ψ.toContinuousLinearEquiv ∘SL σ g) ∘SL ↑φ.toContinuousLinearEquiv =
    τ g ∘SL ↑ψ.toContinuousLinearEquiv ∘SL ↑φ.toContinuousLinearEquiv

Tactic:
ψ.isIntertwining,

Goal state after:
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
φ✝ φ : ρ.Equiv σ
ψ : σ.Equiv τ
g : G
⊢ (τ g ∘SL ↑ψ.toContinuousLinearEquiv) ∘SL ↑φ.toContinuousLinearEquiv =
    τ g ∘SL ↑ψ.toContinuousLinearEquiv ∘SL ↑φ.toContinuousLinearEquiv
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Basic

Goal state before:
pp: 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
i : ℕ
⊢ X.homogeneousCochains.d i (i + 1) = (invariantsFunctor k G).map (X.d (i + 1))

Tactic:
dsimp only
  rw [← resolution'd_eq, CochainComplex.of_d]

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

Goal state before:
pp: k : Type u
G H K : 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
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : IsTopologicalGroup K
X : TopRep k G
Y : TopRep k H
Z : TopRep k K
φ : H →ₜ* G
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
i : ℕ
⊢ resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i =
    (resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i

Tactic:
by
  induction i with
  | zero => rfl
  | succ i ih =>
    rw [resolutionMap_succ, resolutionMap_succ, resolutionMap_succ, ih]
    ext F x
    rfl

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

Goal state before:
pp: 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
n : ℕ
⊢ π X n ≫ map φ f n = cocyclesMap φ f n ≫ π Y n

Tactic:
simp [map, cocyclesMap]

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 = ↑ε
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) g) ε = ε

Tactic:
obtain ⟨t, ht, ht'⟩ := b.prop

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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) 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
x : ↑A
hx : x ∈ A.ρ.invariants
g : G
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom A.ρ.invariants.subtype ≫ d₀₁ A)) ⟨x, hx⟩ g = (ModuleCat.Hom.hom 0) ⟨x, hx⟩ g

Tactic:
replace hx := hx g

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
⊢ (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.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 : ℕ
⊢ π A n ≫ map f φ n = cocyclesMap f φ n ≫ π B n

Tactic:
simp [map, cocyclesMap]

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

Goal state before:
pp: case h.refine_2
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g : G ⧸ S
⊢ ∀ (a b : G), (QuotientGroup.leftRel S) a b → ⟨↑x a - (A.ρ a) y + y, ⋯⟩ = ⟨↑x b - (A.ρ b) y + y, ⋯⟩

Tactic:
intro g h hgh

Goal state after:
case h.refine_2
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g✝ : G ⧸ S
g h : G
hgh : (QuotientGroup.leftRel S) g h
⊢ ⟨↑x g - (A.ρ g) y + y, ⋯⟩ = ⟨↑x h - (A.ρ h) y + y, ⋯⟩
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case h₁
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (Set.range fun gv ↦ (A.ρ gv.1) gv.2 - gv.2) ⊆ ↑(ModuleCat.Hom.hom (d₁₀ A)).range

pp: case h₂
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ModuleCat.Hom.hom (d₁₀ A)).range ≤ Submodule.span k (Set.range fun gv ↦ (A.ρ gv.1) gv.2 - gv.2)

Tactic:
· rintro _ ⟨x, rfl⟩
    use single x.1⁻¹ x.2
    simp [d₁₀]

Goal state after:
case h₂
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ModuleCat.Hom.hom (d₁₀ A)).range ≤ Submodule.span k (Set.range fun gv ↦ (A.ρ gv.1) gv.2 - gv.2)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
x : A
hx : x ∈ Coinvariants.ker (Representation.ofDistribMulAction k G A)
r : k
x✝² : A
x✝¹ : x✝² ∈ Submodule.span k (Set.range fun gv ↦ ((Representation.ofDistribMulAction k G A) gv.1) gv.2 - gv.2)
x✝ : IsBoundary₀ G x✝²
X : G →₀ A
hX : (X.sum fun g z ↦ g⁻¹ • z - z) = x✝²
⊢ ((r • X).sum fun g z ↦ g⁻¹ • z - z) = r • x✝²

Tactic:
simp [← hX, sum_smul_index', smul_comm, smul_sub, smul_sum]

Goal state after:
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
⊢ g ∈ Submodule.span R⟦X⟧ (Set.range F)

Tactic:
have h₁ (n : ℕ) : g - ∑ i, trunc n (H i) * F i = X ^ n * G n := by
    induction n with
    | zero => simp [G]
    | succ n IH =>
      simp [trunc_succ, add_mul, sum_add_distrib, ← sub_sub, IH, pow_succ, mul_assoc, ← hG',
        mul_sub, H, mul_sum, monomial_eq_C_mul_X_pow, mul_left_comm (C _)]

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
⊢ g ∈ Submodule.span R⟦X⟧ (Set.range F)
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
I : Ideal R⟦X⟧
S : Set R
P✝ : Ideal R⟦X⟧
inst✝² : P✝.IsPrime
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
P : Ideal R⟦X⟧
h₁ : P ≠ ⊥
h₂ : P.IsPrime
hXP : X ∈ P
⊢ ∃ x ∈ P, Prime x

pp: case neg
R : Type u_1
inst✝³ : CommRing R
I : Ideal R⟦X⟧
S : Set R
P✝ : Ideal R⟦X⟧
inst✝² : P✝.IsPrime
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
P : Ideal R⟦X⟧
h₁ : P ≠ ⊥
h₂ : P.IsPrime
hXP : X ∉ P
⊢ ∃ x ∈ P, Prime x

Tactic:
· exact ⟨X, hXP, X_prime⟩

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
I : Ideal R⟦X⟧
S : Set R
P✝ : Ideal R⟦X⟧
inst✝² : P✝.IsPrime
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
P : Ideal R⟦X⟧
h₁ : P ≠ ⊥
h₂ : P.IsPrime
hXP : X ∉ P
⊢ ∃ x ∈ P, Prime x
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

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

Tactic:
by tauto

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

Goal state before:
pp: 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
⊢ ¬x = single j 1

Tactic:
by tauto

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(k = 0 ∧ x = 0)
h3 : k = 0
⊢ ¬x = 0

Tactic:
by tauto

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : CommRing R
inst✝ : Finite σ
p q : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) (p * q)) = MvPolynomial.coeff x ((truncTotal n) p * (truncTotal n) q)

Tactic:
coeff_truncTotal _ hx,

Goal state after:
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : CommRing R
inst✝ : Finite σ
p q : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < n
⊢ (coeff x) (p * q) = MvPolynomial.coeff x ((truncTotal n) p * (truncTotal n) q)
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c : ℕ
h : c = b + a
x : AdicCompletion I ↥(I ^ a • ⊤)
⊢ ↑((ofPowSMul I M a) x) c = (powSMulQuotInclusion I M h ⊤) (↑x b)

Tactic:
by
  rw [← x.prop (show b ≤ c by lia), map_val_apply]
  refine Quotient.induction_on _ (x.val c) fun z ↦ ?_
  simp [powSMulQuotInclusion]

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ (toMvPowerSeries i) X = MvPowerSeries.X i

Tactic:
rw [toMvPowerSeries_apply, X_apply, MvPowerSeries.rename_X]

Goal state after: