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

Goal state before:
pp: X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
κ : Kernel X Y
inst✝ : IsMarkovKernel κ
g : Y → ↑I := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (κ.map g)
hg'κ : κ = (κ.map g).map hg.invFun
f' : X → ↑I → ↑I
hf' : Measurable (uncurry f')
hf'κ : ∀ (a : X), Measure.map (f' a) volume = (κ.map g) a
a : X
⊢ Measure.map ((fun a u ↦ hg.invFun (f' a u)) a) volume = ((κ.map g).map hg.invFun) a

Tactic:
map_apply _ (by fun_prop),

Goal state after:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
κ : Kernel X Y
inst✝ : IsMarkovKernel κ
g : Y → ↑I := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (κ.map g)
hg'κ : κ = (κ.map g).map hg.invFun
f' : X → ↑I → ↑I
hf' : Measurable (uncurry f')
hf'κ : ∀ (a : X), Measure.map (f' a) volume = (κ.map g) a
a : X
⊢ Measure.map ((fun a u ↦ hg.invFun (f' a u)) a) volume = Measure.map hg.invFun ((κ.map g) a)
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ.tilted fun x ↦ t * X x) ^ 2 ∂μ.tilted fun x ↦ t * X x) =
    iteratedDeriv 2 (cgf X μ) t

Tactic:
rw [integral_tilted_mul_self ht, iteratedDeriv_two_cgf_eq_integral ht, integral_tilted_mul_eq_mgf,
    ← integral_div]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • (X ω - deriv (cgf X μ) t) ^ 2 ∂μ =
    ∫ (a : Ω), (X a - deriv (cgf X μ) t) ^ 2 * rexp (t * X a) / mgf X μ t ∂μ
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : f x ∉ Set.Ioc (-A) A
⊢ |0| ≤ |A|

Tactic:
· simp [abs_nonneg]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h✝ : f x ∉ Set.Ioc (-A) A
⊢ |0| ≤ |f x|

Tactic:
· simp [abs_nonneg]

Goal state after:
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 ∂ρ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (Y j ^ 2) a = ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (x : ℝ) in 0..↑j, x ^ 2 ∂ρ

Tactic:
Y2

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

Goal state before:
pp: 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

pp: 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)

pp: 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)

Tactic:
· exact mgf_nonneg

Goal state after:
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 Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
⊢ HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ

Tactic:
have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
this : IsProbabilityMeasure μ
⊢ HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
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 : ρ.asModule →ₗ[A[G]] σ.asModule
g : G
⊢ { toAddHom := f.toAddHom, map_smul' := ⋯ } ∘ₗ ρ g = σ g ∘ₗ { toAddHom := f.toAddHom, map_smul' := ⋯ }

Tactic:
by ext v; simpa using! f.map_smul' (MonoidAlgebra.single g 1) v

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

Goal state before:
pp: case succ
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst✝ : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
hn :
  (∀ i < n - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ) →
    HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ
h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
⊢ HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
f : σ.IntertwiningMap ρ
x : H → A
h : ∀ (g : G) (h : H), x (φ g * h) = (σ g) (x h)
g : G
h0 : H
⊢ f (x (φ g * h0)) = (ρ g) (f (x h0))

Tactic:
simpa [h] using LinearMap.ext_iff.1 (f.2 g) (x h0)

Goal state after:
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‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
J : ∀ᶠ (n : ℕ) in atTop, ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
n : ℕ
hn : (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
h'n : ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
⊢ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω - ∫ (x : Ω), X 0 x ∂μ =
    (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω - (↑n)⁻¹ • ∑ x ∈ Finset.range n, Y k x ω +
        ((↑n)⁻¹ • ∑ x ∈ Finset.range n, Y k x ω - ∫ (x : Ω), Y k 0 x ∂μ) +
      (∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ)

Tactic:
abel

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
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
h : G
⊢ (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap) ∘SL π₁ h =
    π₃ h ∘SL f.toContinuousLinearMap ∘SL g.toContinuousLinearMap

Tactic:
rw [comp_assoc, g.2, ← comp_assoc, f.2, comp_assoc]

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✝² x✝¹ x✝).hom ≫ (mkIso (Representation.TensorProduct.comm x✝².ρ (x✝¹ ⊗ x✝).ρ)).hom ≫ (α_ x✝¹ x✝ x✝²).hom =
    (mkIso (Representation.TensorProduct.comm x✝².ρ x✝¹.ρ)).hom ▷ x✝ ≫
      (α_ x✝¹ x✝² x✝).hom ≫ x✝¹ ◁ (mkIso (Representation.TensorProduct.comm x✝².ρ x✝.ρ)).hom

Tactic:
by
    ext : 2
    exact TensorProduct.ext_threefold <| fun _ _ _ ↦ by simp

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
b : G
hx : ∀ (x : G), ¬↑f x = 0 → x ∈ MulAction.orbit (↥S) g
a✝ : ⟦b⟧ ∈ Finset.univ
hb : ¬(QuotientGroup.rightRel S) b g
⊢ ↑f b = 0

Tactic:
contrapose! hx

Goal state after:
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
b : G
a✝ : ⟦b⟧ ∈ Finset.univ
hb : ¬(QuotientGroup.rightRel S) b g
hx : ↑f b ≠ 0
⊢ ∃ x, ↑f x ≠ 0 ∧ x ∉ MulAction.orbit (↥S) g
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₀
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
⊢ ∀ b ∈ Finset.univ, b ≠ ⟦a⟧ → ↑(A.indToCoind (b.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0

Tactic:
intro b _ hb
    induction b using Quotient.inductionOn with | h b =>
    simpa using indToCoindAux_of_not_rel b a (g.1 b) (mt Quotient.sound hb.symm)

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
⊢ (Hom.hom (d k G n ≫ (diagonalSuccIsoFree k G n).inv)) (single i (MonoidAlgebra.single 1 1)) =
    (Hom.hom ((diagonalSuccIsoFree k G (n + 1)).inv ≫ (standardComplex k G).d (n + 1) n))
      (single i (MonoidAlgebra.single 1 1))

Tactic:
have eq3 : MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) (1 : k) =
        MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1 := by
      congr; exact funext fun j ↦ Fin.partialProd_succ' i j |>.symm

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
⊢ (Hom.hom (d k G n ≫ (diagonalSuccIsoFree k G n).inv)) (single i (MonoidAlgebra.single 1 1)) =
    (Hom.hom ((diagonalSuccIsoFree k G (n + 1)).inv ≫ (standardComplex k G).d (n + 1) n))
      (single i (MonoidAlgebra.single 1 1))
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↑(ModuleCat.of k (G → ↑A))
g : G × G × G
⊢ (A.ρ g.1) ((A.ρ g.2.1) (f g.2.2)) - (A.ρ g.1) (f (g.2.1 * g.2.2)) + (A.ρ g.1) (f g.2.1) -
          ((A.ρ g.1) ((A.ρ g.2.1) (f g.2.2)) - f (g.1 * (g.2.1 * g.2.2)) + f (g.1 * g.2.1)) +
        ((A.ρ g.1) (f (g.2.1 * g.2.2)) - f (g.1 * (g.2.1 * g.2.2)) + f g.1) -
      ((A.ρ g.1) (f g.2.1) - f (g.1 * g.2.1) + f g.1) =
    0

Tactic:
abel

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
i j : ℕ
hij : j + 1 = i
z : (Fin i → G) →₀ ↑X.X₃
hz : (ConcreteCategory.hom ((inhomogeneousChains X.X₃).d i j)) z = 0
y : (Fin i → G) →₀ ↑X.X₂
hy : (ConcreteCategory.hom ((chainsMap (MonoidHom.id G) X.g).f i)) y = z
x : (Fin j → G) →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom ((inhomogeneousChains X.X₂).d i j)) y
⊢ (ComplexShape.down ℕ).next i = j

Tactic:
by simp [← hij]

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
z : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
⊢ (ConcreteCategory.hom (δ hX 1 0 ⋯)) ((ConcreteCategory.hom (H1π X.X₃)) z) = (ConcreteCategory.hom (H0π X.X₁)) x

Tactic:
by
  simpa only [H1π, ModuleCat.hom_comp, LinearMap.coe_comp, Function.comp_apply, H0π,
    ← cyclesMk₀_eq X.X₁, ← cyclesMk₁_eq X.X₃]
  using! δ_apply hX (i := 1) (j := 0) rfl ((chainsIso₁ X.X₃).inv z.1) (by
    rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]; simp)
    ((chainsIso₁ X.X₂).inv y) (Finsupp.ext fun _ => by simp [chainsIso₁, ← hy])
    ((chainsIso₀ X.X₁).inv x) (Finsupp.ext fun _ => by
      conv_rhs => rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]
      simp [chainsIso₀, ← hx])

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
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

Tactic:
simp_all [shortComplexH1]

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

Goal state before:
pp: 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 : G
s : ↥S
⊢ x (↑s * g) - x ↑s - (A.ρ ↑s) ((A.ρ g) y) + (x ↑s + y) =
    x (↑s * g) - ((A.ρ ↑s) ((A.ρ g) y) - (A.ρ g) y) - (A.ρ g) y + y

Tactic:
abel

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsDomain k
η : Aut (forget k G)
⊢ ∃ s, Hom.hom (η.hom.hom.app rightFDRep).hom = rightRegular s

Tactic:
obtain ⟨s, hs⟩ := ((evalAlgHom _ _ 1).comp (algHomOfRightFDRepComp η)).eq_piEvalAlgHom
  refine ⟨s, (basisFun k G).ext fun u ↦ ?_⟩
  simp only [rightFDRep, forget_obj]
  ext t
  have nat := η.hom.hom.naturality (leftRegularFDRepHom t⁻¹)
  calc
    _ = leftRegular t⁻¹ ((η.hom.hom.app rightFDRep).hom (single u 1)) 1 := by simp
    _ = (η.hom.hom.app rightFDRep).hom (leftRegular t⁻¹ (single u 1)) 1 :=
      congrFun congr(($nat.symm).hom (single u 1)) 1
    _ = evalAlgHom _ _ s (leftRegular t⁻¹ (single u 1)) :=
      congr($hs (leftRegular t⁻¹ (single u 1)))
    _ = _ := by by_cases u = t * s <;> simp_all

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ (MvPolynomial.monomial (m.degree p)) 1 = MvPolynomial.C ↑⋯.unit⁻¹ * m.leadingTerm p

Tactic:
rw [← C_mul_leadingCoeff_monomial_degree, ← mul_assoc, ← map_mul,
      IsUnit.val_inv_mul, MvPolynomial.C_1, one_mul]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g : G
a : ↑A
⊢ single g a - single 1 ((A.ρ g⁻¹) a) + single g⁻¹ ((A.ρ g⁻¹) a) -
      (single g⁻¹ ((A.ρ g⁻¹) a) - single 1 a + single g a) =
    single 1 a - single 1 ((A.ρ g⁻¹) a)

Tactic:
abel

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g : G
a : ↑A
⊢ single g⁻¹ a - single 1 ((A.ρ g) a) + single g ((A.ρ g) a) - (single g ((A.ρ g) a) - single 1 a + single g⁻¹ a) =
    single 1 a - single 1 ((A.ρ g) a)

Tactic:
abel

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g h : G
a : ↑A
⊢ single h a - single (g * h) ((A.ρ g) a) + single g ((A.ρ g) a) +
      (single (g * h) ((A.ρ g) a) - single h a + single g⁻¹ a) =
    single g ((A.ρ g) a) + single g⁻¹ a

Tactic:
abel

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g h : G
a : ↑A
⊢ single (g * h) a - single h ((A.ρ g⁻¹) a) + single g⁻¹ ((A.ρ g⁻¹) a) +
      (single h ((A.ρ g⁻¹) a) - single (g * h) a + single g a) =
    single g⁻¹ ((A.ρ g⁻¹) a) + single g a

Tactic:
abel

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

Goal state before:
pp: case left
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
n : ℕ
hn : 0 < n
m : ℕ
⊢ IsOpen[inst✝¹] ↑((J ^ n) ^ m)

Tactic:
rw [← pow_mul]

Goal state after:
case left
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
n : ℕ
hn : 0 < n
m : ℕ
⊢ IsOpen[inst✝¹] ↑(J ^ (n * m))
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : AdicCompletion (maximalIdeal R) R
this : (eval (maximalIdeal R) R 1).ker = maximalIdeal R • ⊤
⊢ x ∈ maximalIdeal (AdicCompletion (maximalIdeal R) R) ↔ ↑x 1 = 0

Tactic:
rw [maximalIdeal_eq_map, ← Submodule.restrictScalars_mem R, ← Ideal.smul_top_eq_map]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : AdicCompletion (maximalIdeal R) R
this : (eval (maximalIdeal R) R 1).ker = maximalIdeal R • ⊤
⊢ x ∈ maximalIdeal R • ⊤ ↔ ↑x 1 = 0
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ Submodule.spanFinrank (maximalIdeal (AdicCompletion (maximalIdeal R) R)) = Submodule.spanFinrank (maximalIdeal R)

Tactic:
by
  have fg : (maximalIdeal R).FG := fg_of_isNoetherianRing (maximalIdeal R)
  have comapeq := IsLocalRing.maximalIdeal_comap (algebraMap R (AdicCompletion (maximalIdeal R) R))
  let f := Ideal.mapCotangent _ _ (Algebra.ofId R (AdicCompletion (maximalIdeal R) R))
    (le_of_eq comapeq.symm)
  have inj : Function.Injective f := by
    rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
    intro m hm
    rcases Ideal.toCotangent_surjective _ m with ⟨m', hm'⟩
    simp only [← hm', mapCotangent_toCotangent, Algebra.ofId_apply, toCotangent_eq_zero,
      maximalIdeal_eq_map, ← Ideal.map_pow, f] at hm
    rw [← Submodule.restrictScalars_mem R, ← Ideal.smul_top_eq_map,
      pow_smul_top_eq_ker_eval fg] at hm
    have : (algebraMap R (AdicCompletion (maximalIdeal R) R)) m'.1 = of _ R m'.1 := rfl
    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
    simpa [← hm', toCotangent_eq_zero] using hm
  have surj : Function.Surjective f := by
    intro m
    rcases Ideal.toCotangent_surjective _ m with ⟨m', hm'⟩
    rcases Submodule.Quotient.mk_surjective _ (m'.1.1 2) with ⟨l, hl⟩
    have lmem : (transitionMap _ R (Nat.le_succ 1)) (m'.1.1 2) = m'.1.1 1 := m'.1.2 (Nat.le_succ 1)
    simp only [smul_eq_mul, Nat.succ_eq_add_one, Nat.reduceAdd, transitionMap, Submodule.factorPow,
      Submodule.mapQ_eq_factor, Submodule.factor_eq_factor, ← hl, mk_eq_mk, factor_mk, pow_one,
      (mem_maximalIdeal_iff_eval_one_eq_zero m'.1).mp m'.2, eq_zero_iff_mem, mul_top] at lmem
    use (maximalIdeal R).toCotangent ⟨l, lmem⟩
    simp only [mapCotangent_toCotangent, Algebra.ofId_apply, ← hm', toCotangent_eq, f]
    change (of (maximalIdeal R) R l) - m' ∈ _
    simp only [maximalIdeal_eq_map, ← Ideal.map_pow]
    rw [← Submodule.restrictScalars_mem R, ← Ideal.smul_top_eq_map]
    simpa [pow_smul_top_eq_ker_eval (maximalIdeal R).fg_of_isNoetherianRing, eval, sub_eq_zero]
      using hl
  have rkeq := rank_eq_of_equiv_equiv _
    (LinearEquiv.ofBijective f ⟨inj, surj⟩).toAddEquiv
    (residueField_map_bijective R) (fun r m ↦ by
      rcases IsLocalRing.residue_surjective r with ⟨s, rfl⟩
      exact map_smul f s m )
  have fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG := by
    simpa [AdicCompletion.maximalIdeal_eq_map] using fg.map _
  rw [IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg fg,
    IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg fg', eq_comm]
  simp [Module.finrank, CotangentSpace, rkeq]

Goal state after:
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
n : ℕ
x : AdicCompletion I ↥(I ^ n • ⊤)
hx : (ofPowSMul I M n) x = 0
i : ℕ
⊢ ↑x i = ↑0 i

Tactic:
simp only [AdicCompletion.ext_iff, val_zero, Pi.zero_apply] at hx

Goal state after:
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 ↥(I ^ n • ⊤)
i : ℕ
hx : ∀ (n_1 : ℕ), ↑((ofPowSMul I M n) x) n_1 = 0
⊢ ↑x i = ↑0 i