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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
r : ℝ
ω : Ω'
hω : ∀ (t : ℝ), mgf X (κ ω) t ≤ rexp (↑c * t ^ 2 / 2)
t : ℝ
⊢ mgf (fun ω ↦ r * X ω) (κ ω) t ≤ rexp (↑(NNReal.mk (r ^ 2) ⋯ * c) * t ^ 2 / 2)

Tactic:
mgf_const_mul,

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
r : ℝ
ω : Ω'
hω : ∀ (t : ℝ), mgf X (κ ω) t ≤ rexp (↑c * t ^ 2 / 2)
t : ℝ
⊢ mgf X (κ ω) (r * t) ≤ rexp (↑(NNReal.mk (r ^ 2) ⋯ * c) * t ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

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

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

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
x : α
⊢ 0 x ≤ truncation f A x

Tactic:
exact truncation_nonneg _ (h'f x)

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

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

Tactic:
by
  by_cases hX0 : cX = 0
  · simp only [hX0, NNReal.sqrt_zero, zero_add, NNReal.sq_sqrt] at hX ⊢
    refine hY.congr ?_
    filter_upwards [ae_eq_zero_of_hasSubgaussianMGF_zero' hX] with ω hX0 using by simp [hX0]
  by_cases hY0 : cY = 0
  · simp only [hY0, NNReal.sqrt_zero, add_zero, NNReal.sq_sqrt] at hY ⊢
    refine hX.congr ?_
    filter_upwards [ae_eq_zero_of_hasSubgaussianMGF_zero' hY] with ω hY0 using by simp [hY0]
  exact
  { integrable_exp_mul t := by
      simp_rw [mul_add, exp_add]
      convert! MemLp.integrable_mul (hX.memLp_exp_mul t 2) (hY.memLp_exp_mul t 2)
      norm_cast
      infer_instance
    mgf_le := by
      let p := (cX.sqrt + cY.sqrt) / cX.sqrt
      let q := (cX.sqrt + cY.sqrt) / cY.sqrt
      filter_upwards [hX.mgf_le, hY.mgf_le, hX.ae_forall_memLp_exp_mul p,
        hY.ae_forall_memLp_exp_mul q] with ω' hmX hmY hlX hlY t
      calc (κ ω')[fun ω ↦ exp (t * (X ω + Y ω))]
      _ ≤ (κ ω')[fun ω ↦ exp (t * X ω) ^ (p : ℝ)] ^ (1 / (p : ℝ)) *
          (κ ω')[fun ω ↦ exp (t * Y ω) ^ (q : ℝ)] ^ (1 / (q : ℝ)) := by
        simp_rw [mul_add, exp_add]
        apply integral_mul_le_Lp_mul_Lq_of_nonneg
        · exact ⟨by simp [field, p, q], by positivity, by positivity⟩
        · exact ae_of_all _ fun _ ↦ exp_nonneg _
        · exact ae_of_all _ fun _ ↦ exp_nonneg _
        · simpa using (hlX t)
        · simpa using (hlY t)
      _ ≤ exp (cX * (t * p) ^ 2 / 2) ^ (1 / (p : ℝ)) *
          exp (cY * (t * q) ^ 2 / 2) ^ (1 / (q : ℝ)) := by
        simp_rw [← exp_mul _ p, ← exp_mul _ q, mul_right_comm t _ p, mul_right_comm t _ q]
        gcongr
        · exact hmX (t * p)
        · exact hmY (t * q)
      _ = exp ((cX.sqrt + cY.sqrt) ^ 2 * t ^ 2 / 2) := by
        simp_rw [← exp_mul, ← exp_add]
        simp only [NNReal.coe_div, NNReal.coe_add, coe_sqrt, one_div, inv_div, exp_eq_exp, p, q]
        field_simp
        linear_combination t ^ 2 * (-√↑cY * Real.sq_sqrt cX.coe_nonneg
            -√↑cX * Real.sq_sqrt cY.coe_nonneg) }

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

Goal state before:
pp: A : Type u_1
V : Type u_2
k : Type u_3
inst✝⁹ : Field k
inst✝⁸ : Ring A
inst✝⁷ : Algebra k A
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k V
inst✝⁴ : Module A V
inst✝³ : IsScalarTower k A V
inst✝² : IsSimpleModule A V
inst✝¹ : FiniteDimensional k V
inst✝ : IsAlgClosed k
this : Module.Finite k (Module.End A V)
⊢ Function.Bijective ⇑(algebraMap k (Module.End A V))

Tactic:
classical exact IsAlgClosed.algebraMap_bijective_of_isIntegral (k := k)

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 : ρ.IntertwiningMap σ
g₁ g₂ : τ.IntertwiningMap π
x✝¹ : V
x✝ : U
⊢ ((TensorProduct.AlgebraTensorModule.curry (f.tensor (g₁ + g₂)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (f.tensor g₁ + f.tensor g₂).toLinearMap) x✝¹) x✝

Tactic:
simp [TensorProduct.tmul_add]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
let pos : ℝ → ℝ := fun x => max x 0

Goal state after:
case neg
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x ↦ max x 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
α : Type u
inst✝ : DecidableEq α
i : α
x : ↑A
⊢ (A.finsuppToCoinvariantsTensorFree α) (single i x) =
    (Coinvariants.mk (A.ρ.tprod (Representation.free k G α))) (x ⊗ₜ[k] single i (MonoidAlgebra.single 1 1))

Tactic:
by
  simp [finsuppToCoinvariantsTensorFree, Representation.finsuppTensorRight, Equiv.mk_symm]

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
π : ContRepresentation R G V
h : H
⊢ Continuous
    (Subtype.val ∘ fun x ↦
      match x with
      | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h), ⋯⟩)

Tactic:
by
      simpa using! (ContinuousMap.mulRight h).continuous_precomp.comp continuous_subtype_val

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
g : G
inst✝ : Finite G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ (Hom.hom ((leftRegular k G).applyAsHom g - 𝟙 (leftRegular k G))).range =
    ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker

Tactic:
simp [sub_hom, applyAsHom, FiniteCyclicGroup.coinvariantsKer_eq_range
    (Representation.leftRegular k G) _ hg,
    ← FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker]

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

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
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
g : G
hσ : ↑σ g⁻¹ = ↑σ 1
⊢ (X.ρ g) (↑σ 1) = ↑σ 1

Tactic:
simpa [hσ] using DFunLike.ext_iff.1 (σ.2 g) 1

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✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
h : H
a : ↑A
b : ↑B
⊢ (((TensorProduct.AlgebraTensorModule.curry
              (((ind φ A).coinvariantsTensorMk B).compr₂
                  (ModuleCat.Hom.hom (coinvariantsTensorIndHom φ A B ≫ coinvariantsTensorIndInv φ A B)) ∘ₗ
                Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
            MonoidAlgebra.lsingle h)
          1)
        a)
      b =
    (((TensorProduct.AlgebraTensorModule.curry
              (((ind φ A).coinvariantsTensorMk B).compr₂
                  (ModuleCat.Hom.hom (𝟙 (((coinvariantsTensor k H).obj (ind φ A)).obj B))) ∘ₗ
                Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
            MonoidAlgebra.lsingle h)
          1)
        a)
      b

Tactic:
simpa [coinvariantsTensorIndInv, coinvariantsTensorMk,
      coinvariantsTensorIndHom, Coinvariants.mk_eq_iff] using
        Coinvariants.mem_ker_of_eq h (IndV.mk φ _ h a ⊗ₜ[k] b) _ <| by simp

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (standardComplex k G).d 1 0 ≫ ε k G = 0

Tactic:
ext : 3
  have : (forget₂ToModuleCat k G).d 1 0
      ≫ (forget₂ (Rep k G) (ModuleCat.{u} k)).map (ε k G) = 0 := by
    rw [← forget₂ToModuleCatHomotopyEquiv_f_0_eq,
      ← (forget₂ToModuleCatHomotopyEquiv k G).1.2 1 0 rfl]
    exact comp_zero
  exact LinearMap.ext_iff.1 (ModuleCat.hom_ext_iff.mp this) _

Goal state after:
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
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
⊢ (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f 0)) ((ConcreteCategory.hom (cochainsIso₀ X.X₂).inv) y) =
    (ConcreteCategory.hom (cochainsIso₀ X.X₃).inv) ↑z

Tactic:
ext; simp [← hy, cochainsIso₀]

Goal state after:
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
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
⊢ (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d 1 (1 + 1)))
      ((ConcreteCategory.hom (cochainsIso₁ X.X₃).inv) ⇑z) =
    0

Tactic:
by
      rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₂_comp_inv]
      simp [cocycles₁.d₁₂_apply z]

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 : ↑((inhomogeneousCochains A).X 1)
y : G × G
⊢ (A.ρ y.1) (x ((Equiv.funUnique (Fin 1) G).symm y.2)) +
      (-x ((Equiv.funUnique (Fin 1) G).symm (y.1 * y.2)) + x ((Equiv.funUnique (Fin 1) G).symm y.1)) =
    (A.ρ ((piFinTwoEquiv fun x ↦ G).symm y 0)) (x fun i ↦ (piFinTwoEquiv fun x ↦ G).symm y i.succ) +
      (-x (Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y)) +
        x (Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y)))

Tactic:
rcongr i

Goal state after:
case e_a.e_6
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
i : Fin 1
⊢ (Equiv.funUnique (Fin 1) G).symm y.2 i = (piFinTwoEquiv fun x ↦ G).symm y i.succ

case e_a.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
i : Fin 1
⊢ (Equiv.funUnique (Fin 1) G).symm (y.1 * y.2) i =
    Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y) i

case e_a.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
i : Fin 1
⊢ (Equiv.funUnique (Fin 1) G).symm y.1 i = Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y) i
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

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

Tactic:
simp [inhomogeneousChains]

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 : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x ((piFinTwoEquiv fun x ↦ G).symm (y.2.1, y.2.2))) +
      (-x ((piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2)) +
        (x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2)) + -x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1)))) =
    (A.ρ ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y) 0))
        (x fun i ↦ (Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y) i.succ) +
      (-x
            (Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2)
              ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))) +
        (x
            (Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2)
              ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))) +
          -x
              (Fin.contractNth 2 (fun x1 x2 ↦ x1 * x2)
                ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)))))

Tactic:
rcongr i

Goal state after:
case e_a.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
i : Fin 2
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2) i =
    Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) i

case e_a.e_a.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
i : Fin 2
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2) i =
    Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) i

case e_a.e_a.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
i : Fin 2
⊢ (piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1) i =
    Fin.contractNth 2 (fun x1 x2 ↦ x1 * x2)
      ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)) i
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 : ↥(cocycles₂ A)
g : G
⊢ (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
have := (mem_cocycles₂_iff f).1 f.2 g g⁻¹ g
  simp only [mul_inv_cancel, inv_mul_cancel, cocycles₂_map_one_fst _ g]
    at this
  exact sub_eq_sub_iff_add_eq_add.2 this.symm

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
this : f (g * g⁻¹, g) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, g⁻¹ * g)
⊢ g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)

Tactic:
simp only [mul_inv_cancel, inv_mul_cancel, map_one_fst_of_isMulCocycle₂ hf g] at this

Goal state after:
G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
this : f (1, 1) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, 1)
⊢ g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)
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
x✝ : Fin 0 → G
⊢ ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) ((ConcreteCategory.hom (chainsIso₀ X.X₁).inv) x)) x✝ =
    ((ConcreteCategory.hom ((inhomogeneousChains X.X₂).d 1 0)) ((ConcreteCategory.hom (chainsIso₁ X.X₂).inv) y)) x✝

Tactic:
by
      conv_rhs => rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]
      simp [chainsIso₀, ← hx]

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✝ : Fintype G
X : FDRep k G
v : ↑X.V
t : G
⊢ rightFDRep.ρ t ≫ InducedCategory.homMk (↟(sumSMulInv v)) = InducedCategory.homMk (↟(sumSMulInv v)) ≫ X.ρ t

Tactic:
by
    ext f
    let φ_term (X : FDRep k G) (f : G → k) v s := (f s) • (X.ρ s⁻¹ v)
    have := sum_map univ (mulRightEmbedding t⁻¹) (φ_term X (rightRegular t f) v)
    simpa [φ_term] using! this

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

Goal state before:
pp: case a
σ : 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
⊢ m.leadingTerm p ∈ ↑(span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B))

Tactic:
SetLike.mem_coe,

Goal state after:
case a
σ : 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
⊢ m.leadingTerm p ∈ span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B)
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : Submodule.span R (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
⊢ I.FG

Tactic:
submodule_span_eq

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
⊢ I.FG
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
⊢ (ConcreteCategory.hom (d₂₁ A)) (single (g, h) ((A.ρ g) a) + single (g⁻¹, g * h) a) =
    single g ((A.ρ g) a) + single g⁻¹ a

Tactic:
simp only [map_add, d₂₁_single (G := G), inv_self_apply, inv_inv, inv_mul_cancel_left]

Goal state after:
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
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x : R
_hx : x ∈ ↑(I ^ n)
b : R
hb : b ∈ ↑(I ^ n)
⊢ (fun x1 x2 ↦ x1 * x2) x b ∈ ↑(I ^ n)

Tactic:
exact (I ^ n).smul_mem x hb

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
S : Finset R
hS : span ↑S = Ideal.map constantCoeff P
hX : X ∉ P
T : Set R⟦X⟧
hT : P = span T
hT₂ : T.Finite
right✝ : T.ncard = (↑S).ncard
⊢ P.FG

Tactic:
lift T to Finset R⟦X⟧ using hT₂

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
S : Finset R
hS : span ↑S = Ideal.map constantCoeff P
hX : X ∉ P
T : Finset R⟦X⟧
hT : P = span ↑T
right✝ : (↑T).ncard = (↑S).ncard
⊢ P.FG
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
⊢ ∃ i, True ∧ ↑(J ^ i) ⊆ s

pp: case mpr.h.mpr
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 : ∃ i, True ∧ ↑(J ^ i) ⊆ s
⊢ s ∈ 𝓝 0

Tactic:
· rcases H₂ s H with ⟨n, h⟩
        exact ⟨n, trivial, h⟩

Goal state after:
case mpr.h.mpr
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 : ∃ i, True ∧ ↑(J ^ i) ⊆ s
⊢ s ∈ 𝓝 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
⊢ (if optionElim n y = x then r else 0) = (coeff y) (if n = x none then (monomial x.some) r else 0)

Tactic:
split_ifs with h1 h2 h3

Goal state after:
case pos
σ : 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) ((monomial x.some) r)

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

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

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : ¬n = x none
⊢ 0 = (coeff y) 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
⊢ (if x = 0 ∧ k = 1 then 1 else 0) = (coeff x) (if k = 1 then 1 else 0)

Tactic:
split_ifs with h1 h2 h3

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : x = 0 ∧ k = 1
h2 : k = 1
⊢ 1 = (coeff x) 1

case neg
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : x = 0 ∧ k = 1
h2 : ¬k = 1
⊢ 1 = (coeff x) 0

case pos
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = 0 ∧ k = 1)
h3 : k = 1
⊢ 0 = (coeff x) 1

case neg
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = 0 ∧ k = 1)
h3 : ¬k = 1
⊢ 0 = (coeff x) 0