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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
⊢ ∃ f, Measurable (uncurry f) ∧ ∀ (a : X), Measure.map (f a) volume = κ a

Tactic:
let f := fun s (t : I) ↦ sSup {x | (κ s).real (Icc 0 x) < t}
  have measurable_f : Measurable (uncurry f) := by
    refine measurable_of_Ioi fun a ↦ ?_
    simp only [preimage, uncurry, mem_Ioi]
    have h_monotone s : Monotone (fun x ↦ (κ s).real (Icc 0 x)) :=
      fun x y hxy ↦ measureReal_mono (by gcongr)
    have sSup_eq_iUnion_rat : {x : X × I | a < f x.1 x.2} =
        ⋃ (q : ℚ) (hqI : ↑q ∈ I) (_ : a < (q : ℝ)), {e | (κ e.1).real (Icc 0 ⟨q, hqI⟩) < e.2} := by
      ext e
      simp_all only [lt_sSup_iff, mem_ofPred_eq, Subtype.exists, mem_Icc, Rat.cast_nonneg,
        mem_iUnion, exists_prop, exists_and_left, f]
      constructor
      · rintro ⟨y, hyI, y_mem, (hy : a.1 < y)⟩
        obtain ⟨q, hqa, hqy⟩ := exists_rat_btwn hy
        refine ⟨q, hqa, ⟨?_, hqy.le.trans hyI.2⟩, lt_of_lt_of_le' y_mem (h_monotone e.1 hqy.le)⟩
        simp [← Rat.cast_nonneg (K := ℝ), a.2.1.trans hqa.le]
      · intro he
        obtain ⟨q, hqa, hqI, h⟩ := he
        refine ⟨q, ⟨by simp [hqI.1], hqI.2⟩, h, ?_⟩
        change a.1 < q
        simp [hqa]
    rw [sSup_eq_iUnion_rat]
    refine MeasurableSet.iUnion (fun b ↦ MeasurableSet.iUnion
      (fun bI ↦ MeasurableSet.iUnion (fun _ ↦ ?_)))
    refine measurableSet_lt ?_ measurable_snd.subtype_val
    simp_rw [measureReal_def]
    have hκ := κ.measurable_coe (s := Icc 0 ⟨b, bI⟩) measurableSet_Icc
    fun_prop
  refine ⟨f, measurable_f, fun a ↦ (volume.map (f a)).ext_of_Iic (κ a) fun x ↦ ?_⟩
  have Iic_to_Icc : Iic x = Icc 0 x := by ext; simp
  have κ_in_I : ((κ a).real (Icc 0 x)) ∈ I := ⟨measureReal_nonneg, measureReal_le_one⟩
  simp_rw [volume.map_apply measurable_f.of_uncurry_left measurableSet_Iic, preimage,
    mem_Iic, Iic_to_Icc, ← ofReal_measureReal (measure_ne_top (κ a) _), ← volume_Iic ⟨_, κ_in_I⟩]
  congr with ξ
  constructor
  · intro (hξ : f a ξ ≤ x)
    change ξ ≤ (κ a).real (Icc 0 x)
    by_cases hx : x = 1
    · simp [hx, ← univ_eq_Icc, ξ.2.2]
    let g := fun y ↦ (κ a).real (Icc 0 y)
    let nebot : NeBot (𝓝[>] x) := by
      refine nhdsGT_neBot_of_exists_gt ?_
      use 1
      exact lt_of_le_of_ne x.2.2 hx
    refine le_of_tendsto_of_tendsto (b := 𝓝[>] x) (g := g) continuousWithinAt_const ?_ ?_
    · let h := cdf ((κ a).map Subtype.val)
      have h_continuousWithinAt := continuousWithinAt_Ioi_iff_Ici.mpr (h.right_continuous x)
      simp_rw [g, ← unitInterval.cdf_eq_real (κ a)]
      exact h_continuousWithinAt.comp (Continuous.continuousWithinAt (by fun_prop)) (fun y hy ↦ hy)
    · refine eventually_nhdsWithin_of_forall fun y hy ↦ ?_
      by_contra! h
      simp only [sSup_le_iff, f] at hξ
      specialize hξ y h
      grind
  · intro (hξ : ξ ≤ (κ a).real (Icc 0 x))
    simp only [sSup_le_iff, f]
    intro c hc
    by_contra! h
    have h_lt : ¬ (κ a).real (Icc 0 x) ≤ (κ a).real (Icc 0 c) := not_le.mpr (lt_of_le_of_lt' hξ hc)
    refine h_lt ?_
    gcongr
    simp

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

Goal state before:
pp: case neg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : ¬IsSFiniteKernel κ
⊢ Integrable (fun ω ↦ rexp (t * (X ω.1 + Y ω.2))) (⇑(κ ⊗ₖ η) ∘ₘ ν)

pp: case pos
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
⊢ Integrable (fun ω ↦ rexp (t * (X ω.1 + Y ω.2))) (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
· simp [FunLike.coe_zero, hκ]

Goal state after:
case pos
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
⊢ Integrable (fun ω ↦ rexp (t * (X ω.1 + Y ω.2))) (⇑(κ ⊗ₖ η) ∘ₘ ν)
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
σ : Representation k G W
g : G
⊢ (ρ g) 0 = 0

Tactic:
by simp only [map_zero]

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
inst✝ : Fintype G
g : G
v : W
⊢ (sumOfConjugates G π) (MonoidAlgebra.single g 1 • v) = MonoidAlgebra.single g 1 • (sumOfConjugates G π) v

Tactic:
simp only [sumOfConjugates_apply, Finset.smul_sum, conjugate_apply]
    refine Fintype.sum_bijective (· * g) (Group.mulRight_bijective g) _ _ fun i ↦ ?_
    simp only [smul_smul, single_mul_single, mul_inv_rev, mul_inv_cancel_left, one_mul]

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 : Rep k G
f : trivial k G PUnit.{w + 1} ⟶ X
x : ↑(trivial k G PUnit.{w + 1})
this : x = 0
⊢ (Hom.hom f).toLinearMap x = (Hom.hom default).toLinearMap x

Tactic:
subst this

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X : Rep k G
f : trivial k G PUnit.{w + 1} ⟶ X
⊢ (Hom.hom f).toLinearMap 0 = (Hom.hom default).toLinearMap 0
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
M : Rep k G
⊢ Limits.IsZero M ↔ Subsingleton ↑M

Tactic:
simp [Limits.IsZero.iff_id_eq_zero, Rep.hom_ext_iff, Representation.IntertwiningMap.ext_iff,
    ← ModuleCat.isZero_of_iff_subsingleton (R := k), ModuleCat.hom_ext_iff]

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

Goal state before:
pp: R : Type u_1
G✝ : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²³ : Monoid G✝
inst✝²² : Ring R
inst✝²¹ : AddCommGroup V
inst✝²⁰ : TopologicalSpace V
inst✝¹⁹ : IsTopologicalAddGroup V
inst✝¹⁸ : Module R V
inst✝¹⁷ : AddCommGroup W
inst✝¹⁶ : TopologicalSpace W
inst✝¹⁵ : IsTopologicalAddGroup W
inst✝¹⁴ : Module R W
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
g : ↥⊥
⊢ ↑(Submodule.topContEquiv.symm.trans (ContinuousLinearEquiv.ofEq ⊤ (coindV 1 (trivial R G V)) ⋯)) ∘SL
      (trivial R (↥⊥) V).coind₁ g =
    (coind 1 (trivial R G V)) g ∘SL
      ↑(Submodule.topContEquiv.symm.trans (ContinuousLinearEquiv.ofEq ⊤ (coindV 1 (trivial R G V)) ⋯))

Tactic:
by
    simp [Subsingleton.elim g 1, ContinuousLinearMap.one_def]

Goal state after:
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
n : ℕ
⊢ X.d n ≫ X.d (n + 1) = 0

Tactic:
induction n with
  | zero =>
    ext
    simp [d_succ, ContIntertwiningMap.toContinuousLinearMap_apply, d_zero, hom_sub]
  | succ n ih =>
    rw [d_succ _ (n + 1), Preadditive.comp_sub]
    nth_rw 2 [d_succ]
    rw [Preadditive.sub_comp, ← Functor.map_comp, ih, Functor.map_zero, sub_zero, sub_eq_zero]
    rfl

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
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
⊢ ∑ c, ↑(A.indToCoind (c.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = ↑g a

Tactic:
rw [Finset.sum_eq_single ⟦a⟧]

Goal state after:
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
⊢ ↑(A.indToCoind (⟦a⟧.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = ↑g a

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

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
⊢ ⟦a⟧ ∉ Finset.univ → ↑(A.indToCoind (⟦a⟧.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case hx
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 : G
a : ↑A
x : G
hx : x ∉ MulAction.orbit (↥S) g
⊢ x ∉
    Function.support
      ↑(A.indToCoind
          ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a)))

Tactic:
simpa using indToCoindAux_of_not_rel g x a hx

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
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
⊢ A.coindToInd ∘ₗ A.indToCoind = LinearMap.id

Tactic:
by
  ext g a
  simp only [LinearMap.comp_apply, AlgebraTensorModule.curry_apply,
    TensorProduct.curry_apply, LinearMap.coe_restrictScalars, LinearMap.id_apply]
  rw [coindToInd_of_support_subset_orbit g]
  · simp
  · intro x hx
    contrapose hx
    simpa using indToCoindAux_of_not_rel g x a hx

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : ind φ A ⟶ B
h : H
a : ↑A
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom
                  ((fun f ↦
                      ofHom
                        {
                          toLinearMap :=
                            Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                              (TensorProduct.lift
                                (((lift (↑A →ₗ[k] ↑B) k H) fun h ↦ B.ρ h⁻¹ ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ
                                  ↑(MonoidAlgebra.coeffLinearEquiv k)))
                              ⋯,
                          isIntertwining' := ⋯ })
                    ((fun f ↦ ofHom { toLinearMap := (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1, isIntertwining' := ⋯ })
                      f))).toLinearMap ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle h)
        1)
      a =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom f).toLinearMap ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle h)
        1)
      a

Tactic:
simpa using (hom_comm_apply f h⁻¹ (IndV.mk φ A.ρ 1 a)).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
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
m : ℕ
f : Fin m → G
g : G
r : k
⊢ (Hom.hom (linearizationOfMulActionIso k G (Fin (m + 1) → G)).inv)
      ((Hom.hom ((linearization k G).mapIso (Action.diagonalSuccIsoTensorTrivial G m)).inv)
        ((Hom.hom
            (Functor.Monoidal.μIso (linearization k G) (Action.leftRegular G) (Action.trivial G (Fin m → G))).symm.inv)
          ((Hom.hom
              (MonoidalCategory.tensorIso (linearizationOfMulActionIso k G G)
                  (linearizationTrivialIso k G (Fin m → G))).inv)
            ((Hom.hom (leftRegularTensorTrivialIsoFree k G (Fin m → G)).inv) (single f (MonoidAlgebra.single g r)))))) =
    MonoidAlgebra.single (g • Fin.partialProd f) r

Tactic:
have step1 : (Hom.hom (leftRegularTensorTrivialIsoFree k G (Fin m → G)).inv)
          (single f (.single g r)) = .single g 1 ⊗ₜ[k] .single f r :=
        Representation.leftRegularTensorTrivialIsoFree_symm_apply_single_single f g r

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
m : ℕ
f : Fin m → G
g : G
r : k
step1 :
  (Hom.hom (leftRegularTensorTrivialIsoFree k G (Fin m → G)).inv) (single f (MonoidAlgebra.single g r)) =
    MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single f r
⊢ (Hom.hom (linearizationOfMulActionIso k G (Fin (m + 1) → G)).inv)
      ((Hom.hom ((linearization k G).mapIso (Action.diagonalSuccIsoTensorTrivial G m)).inv)
        ((Hom.hom
            (Functor.Monoidal.μIso (linearization k G) (Action.leftRegular G) (Action.trivial G (Fin m → G))).symm.inv)
          ((Hom.hom
              (MonoidalCategory.tensorIso (linearizationOfMulActionIso k G G)
                  (linearizationTrivialIso k G (Fin m → G))).inv)
            ((Hom.hom (leftRegularTensorTrivialIsoFree k G (Fin m → G)).inv) (single f (MonoidAlgebra.single g r)))))) =
    MonoidAlgebra.single (g • Fin.partialProd f) r
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
S : Subgroup G
A✝ : Rep.{?u.12, u, u} k ↥S
P : ProjectiveResolution (Rep.trivial k G k)
A : Rep.{u, u, u} k ↥S
x✝⁴ x✝³ : ℕ
x✝² : (ComplexShape.up ℕ).Rel x✝⁴ x✝³
f : ↑((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).X x✝⁴)
x✝¹ : ↑(Opposite.unop (Opposite.op (P.complex.X x✝³)))
x✝ : G
⊢ ↑((Hom.hom
              ((ModuleCat.Hom.hom
                  ((resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x✝⁴) A).toModuleIso.hom ≫
                    (P.complex.linearYonedaObj k (coind.{u, u, u, u} S.subtype A)).d x✝⁴ x✝³))
                f)).toLinearMap
          x✝¹)
      x✝ =
    ↑((Hom.hom
              ((ModuleCat.Hom.hom
                  ((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).d x✝⁴ x✝³ ≫
                    (resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x✝³) A).toModuleIso.hom))
                f)).toLinearMap
          x✝¹)
      x✝

Tactic:
simp [← ModuleCat.ofHom_comp, resCoindHomEquiv, hom_comm_apply]

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

Goal state before:
pp: k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
⊢ inhomogeneousChains.d A (n + 1) ≫ inhomogeneousChains.d A n = 0

Tactic:
inhomogeneousChains.d_eq,

Goal state after:
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
⊢ ((A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G)).toModuleIso.inv ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
          (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.hom) ≫
      inhomogeneousChains.d A n =
    0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G M : Type
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulDistribMulAction G M
f : G × G → M
hf : f ∈ coboundaries₂ (Rep.ofMulDistribMulAction G M)
⊢ IsMulCoboundary₂ (⇑Additive.toMul ∘ f)

Tactic:
by
  rcases hf with ⟨x, rfl⟩
  exact ⟨x, fun _ _ => rfl⟩

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
x : ↥(cocycles₁ A)
⊢ cocyclesMk ((ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x) ⋯ = (ConcreteCategory.hom (isoCocycles₁ A).inv) x

Tactic:
apply_fun (forget₂ _ Ab).map ((inhomogeneousCochains A).iCycles 1) using
    (AddCommGrpCat.mono_iff_injective _).1 <| (forget₂ _ _).map_mono _

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
⊢ (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map (HomologicalComplex.iCycles (inhomogeneousCochains A) 1)))
      (cocyclesMk ((ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x) ⋯) =
    (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map (HomologicalComplex.iCycles (inhomogeneousCochains A) 1)))
      ((ConcreteCategory.hom (isoCocycles₁ A).inv) x)
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
⊢ (cochainsMap f φ).f 2 ≫ (cochainsIso₂ B).hom = (cochainsIso₂ A).hom ≫ cochainsMap₂ f φ

Tactic:
by
  ext x g
  change φ.hom (x _) = φ.hom (x _)
  rcongr x
  fin_cases x <;> rfl

Goal state after:
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
⊢ (cochainsMap f φ).f 3 ≫ (cochainsIso₃ B).hom = (cochainsIso₃ A).hom ≫ cochainsMap₃ f φ

Tactic:
by
  ext x g
  change φ.hom (x _) = φ.hom (x _)
  rcongr x
  fin_cases x <;> rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
α : (G → k) →ₗ[k] G → k := Hom.hom (η.hom.hom.app rightFDRep).hom
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (η.inv.hom.app rightFDRep).hom
this : α (α_inv 1) = 1
⊢ α 1 = 1

Tactic:
by
    have h := this
    rwa [← one_mul (α_inv 1), map_mul_toRightFDRepComp, h, mul_one] at this

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

Goal state before:
pp: case mpr.h.mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen[top] ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n ↦ J ^ n • ⊤ := Ideal.adic_basis J
H : s ∈ 𝓝 0
n : ℕ
h : ↑(J ^ n) ⊆ s
⊢ ∃ i, True ∧ ↑(J ^ i) ⊆ s

Tactic:
exact ⟨n, trivial, h⟩

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : optionElim n y = x
h2 : ¬n = x none
⊢ r = (coeff y) 0

Tactic:
absurd h2

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : optionElim n y = x
h2 : ¬n = x none
⊢ n = x none
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : optionElim n y = x
h2 : ¬n = x none
⊢ n = x none

Tactic:
rw [← optionElim_apply_none n, h1]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h3 : n = x none
h1 : ¬y = x.some
⊢ 0 = (coeff y) ((monomial x.some) r)

Tactic:
coeff_monomial,

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h3 : n = x none
h1 : ¬y = x.some
⊢ 0 = if y = x.some then r else 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
p q : MvPowerSeries σ R
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) (p * q)) =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) p) *
      (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) q)

Tactic:
by
    rw [← map_mul, Ideal.Quotient.mk_eq_mk_iff_sub_mem]
    exact truncTotal_mul_sub_mul_truncTotal_mem_pow_idealOfVars p q

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
I : Submodule R C
⊢ I.IsCoideal ↔ (∀ x ∈ I, counit x = 0) ∧ ∀ x ∈ I, comul x ∈ (lTensor C I.subtype).range ⊔ (rTensor C I.subtype).range

Tactic:
isCoideal_iff,

Goal state after:
R : Type u_1
C : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
I : Submodule R C
⊢ ((∀ ⦃x : C⦄, x ∈ I → counit x = 0) ∧ ∀ ⦃x : C⦄, x ∈ I → (TensorProduct.map I.mkQ I.mkQ) (comul x) = 0) ↔
    (∀ ⦃x : C⦄, x ∈ I → counit x = 0) ∧ ∀ x ∈ I, comul x ∈ (lTensor C I.subtype).range ⊔ (rTensor C I.subtype).range
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ ↑(v.valuationOfNeZeroToFun 1) = ↑1

Tactic:
valuationOfNeZeroToFun_eq

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ (valuation K v) ↑1 = ↑1
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
a : A
ha : a ∉ ⊥
⊢ (if a = 0 ∧ n = 0 then 1 else 0) = 0

Tactic:
simp only [mem_bot] at ha
    rw [if_neg]
    exact not_and_of_not_left (n = 0) ha

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑(multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) = ↑(multinomial (insert a✝ s✝) n)

Tactic:
multinomial_insert hi,

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑(multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) =
    ↑((n a✝ + ∑ i ∈ s✝, n i).choose (n a✝) * multinomial s✝ n)