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

Goal state before:
pp: case pos.inr
Ω : 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 κ
hη : IsMarkovKernel η
⊢ Integrable (fun ω ↦ rexp (t * X ω.1) * rexp (t * Y ω.2)) (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
refine MemLp.integrable_mul (p := 2) (q := 2) ?_ ?_

Goal state after:
case pos.inr.refine_1
Ω : 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 κ
hη : IsMarkovKernel η
⊢ MemLp (fun ω ↦ rexp (t * X ω.1)) 2 (⇑(κ ⊗ₖ η) ∘ₘ ν)

case pos.inr.refine_2
Ω : 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 κ
hη : IsMarkovKernel η
⊢ MemLp (fun ω ↦ rexp (t * Y ω.2)) 2 (⇑(κ ⊗ₖ η) ∘ₘ ν)
Module: Mathlib.Probability.Moments.SubGaussian

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

Tactic:
calc
  _ = Var[X; μ.tilted (u * X ·)] := by
    rw [← variance_tilted_mul (hs (Set.mem_Icc_of_Ioo h1))]
  _ ≤ ((b - a) / 2) ^ 2 := by
    convert! variance_le_sq_of_bounded ((tilted_absolutelyContinuous μ (u * X ·)) hb) _
    · exact isProbabilityMeasure_tilted (hi u)
    · exact hm.mono_ac (tilted_absolutelyContinuous μ (u * X ·))
  _ = (‖b - a‖₊ / 2) ^ 2 := by simp [field]

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

Goal state before:
pp: k : Type u
inst✝² : Semiring k
G : Type v1
H : Type v2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : H →* G
M : Rep k G
X✝ Y✝ : Rep k G
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (resFunctor f).map a₁✝ = (resFunctor f).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
simpa [Rep.hom_ext_iff, Representation.IntertwiningMap.ext_iff] using h

Goal state after:
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:
simp only [map_zero]

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁸ : Field k
G : Type u_2
inst✝⁷ : Finite G
inst✝⁶ : NeZero ↑(Nat.card G)
inst✝⁵ : Group G
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module k[G] V
W : Type u_4
inst✝² : AddCommGroup W
inst✝¹ : Module k[G] W
inst✝ : AddGroup G
⊢ NeZero ↑(Nat.card (Multiplicative G))

Tactic:
Nat.card_congr Multiplicative.toAdd

Goal state after:
k : Type u_1
inst✝⁸ : Field k
G : Type u_2
inst✝⁷ : Finite G
inst✝⁶ : NeZero ↑(Nat.card G)
inst✝⁵ : Group G
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module k[G] V
W : Type u_4
inst✝² : AddCommGroup W
inst✝¹ : Module k[G] W
inst✝ : AddGroup G
⊢ NeZero ↑(Nat.card G)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Action (Type u) G
⊢ ofHom (μ X Y) ▷ (linearization k G).obj Z ≫ ofHom (μ (X ⊗ Y) Z) ≫ (linearization k G).map (α_ X Y Z).hom =
    (α_ ((linearization k G).obj X) ((linearization k G).obj Y) ((linearization k G).obj Z)).hom ≫
      (linearization k G).obj X ◁ ofHom (μ Y Z) ≫ ofHom (μ X (Y ⊗ Z))

Tactic:
by ext1; simp [μ_comp_assoc _]

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
x y : ↥(Hom.hom A.norm).ker
⊢ (ConcreteCategory.hom (groupCohomologyπOdd A g hg i hi)) x =
      (ConcreteCategory.hom (groupCohomologyπOdd A g hg i hi)) y ↔
    ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range

Tactic:
by
  rw [← sub_eq_zero, ← map_sub, groupCohomologyπOdd_eq_zero_iff, AddSubgroupClass.coe_sub]

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

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h, ↑(f h) * h z
g : Gal(L/K)
hf : ∀ (g h : Gal(L/K)), ↑(f (g * h)) = g ↑(f h) * ↑(f g)
⊢ ∑ h, ↑(f h) * h z = ∑ x, g ↑(f x) * (↑(f g) * g (x z))

Tactic:
← mul_assoc,

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h, ↑(f h) * h z
g : Gal(L/K)
hf : ∀ (g h : Gal(L/K)), ↑(f (g * h)) = g ↑(f h) * ↑(f g)
⊢ ∑ h, ↑(f h) * h z = ∑ x, g ↑(f x) * ↑(f g) * g (x z)
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝ : CommRing k
n : ℕ
c : Fin (n + 1) → G
r : k
⊢ (d k G n) (MonoidAlgebra.single c r) = ∑ p, MonoidAlgebra.single (c ∘ p.succAbove) (r * (-1) ^ ↑p)

Tactic:
← mul_one r,

Goal state after:
k G : Type u
inst✝ : CommRing k
n : ℕ
c : Fin (n + 1) → G
r : k
⊢ (d k G n) (MonoidAlgebra.single c (r * 1)) = ∑ p, MonoidAlgebra.single (c ∘ p.succAbove) (r * 1 * (-1) ^ ↑p)
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
⊢ (Hom.hom (diagonalSuccIsoFree k G n).inv)
      (single (fun i_1 ↦ i i_1.succ) (MonoidAlgebra.single (i 0) 1) +
        ∑ j, single (j.contractNth (fun x1 x2 ↦ x1 * x2) i) (MonoidAlgebra.single 1 ((-1) ^ (↑j + 1)))) =
    (Hom.hom ((standardComplex k G).d (n + 1) n))
      ((Hom.hom (diagonalSuccIsoFree k G (n + 1)).inv) (single i (MonoidAlgebra.single 1 1)))

Tactic:
map_add,

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 (diagonalSuccIsoFree k G n).inv) (single (fun i_1 ↦ i i_1.succ) (MonoidAlgebra.single (i 0) 1)) +
      (Hom.hom (diagonalSuccIsoFree k G n).inv)
        (∑ j, single (j.contractNth (fun x1 x2 ↦ x1 * x2) i) (MonoidAlgebra.single 1 ((-1) ^ (↑j + 1)))) =
    (Hom.hom ((standardComplex k G).d (n + 1) n))
      ((Hom.hom (diagonalSuccIsoFree k G (n + 1)).inv) (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
x y : G → ↑A
g : G × G
⊢ (A.ρ g.1) (x g.2 + y g.2) - (x (g.1 * g.2) + y (g.1 * g.2)) + (x g.1 + y g.1) =
    (A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1 + ((A.ρ g.1) (y g.2) - y (g.1 * g.2) + y g.1)

Tactic:
map_add,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : G → ↑A
g : G × G
⊢ (A.ρ g.1) (x g.2) + (A.ρ g.1) (y g.2) - (x (g.1 * g.2) + y (g.1 * g.2)) + (x g.1 + y g.1) =
    (A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1 + ((A.ρ g.1) (y g.2) - y (g.1 * g.2) + y g.1)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: case refine_2
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ˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : t • ((algebraMap B L) η * g (IsLocalization.mk' L a b)) = t • IsLocalization.mk' L a b
⊢ η * ((galRestrict A K L B) g) a = a

Tactic:
rw [Algebra.smul_def, mul_left_comm, ← Algebra.smul_def t, ← g.toAlgHom_apply,
        ← AlgHom.map_smul_of_tower, this] at hε

Goal state after:
case refine_2
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ˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η * ↑g ((algebraMap B L) a) = (algebraMap B L) a
⊢ η * ((galRestrict A K L B) g) a = a
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 y : G × G → ↑A
g : G × G × G
⊢ (A.ρ g.1) (x (g.2.1, g.2.2) + y (g.2.1, g.2.2)) - (x (g.1 * g.2.1, g.2.2) + y (g.1 * g.2.1, g.2.2)) +
        (x (g.1, g.2.1 * g.2.2) + y (g.1, g.2.1 * g.2.2)) -
      (x (g.1, g.2.1) + y (g.1, g.2.1)) =
    (A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1) +
      ((A.ρ g.1) (y (g.2.1, g.2.2)) - y (g.1 * g.2.1, g.2.2) + y (g.1, g.2.1 * g.2.2) - y (g.1, g.2.1))

Tactic:
map_add,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : G × G → ↑A
g : G × G × G
⊢ (A.ρ g.1) (x (g.2.1, g.2.2)) + (A.ρ g.1) (y (g.2.1, g.2.2)) - (x (g.1 * g.2.1, g.2.2) + y (g.1 * g.2.1, g.2.2)) +
        (x (g.1, g.2.1 * g.2.2) + y (g.1, g.2.1 * g.2.2)) -
      (x (g.1, g.2.1) + y (g.1, g.2.1)) =
    (A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1) +
      ((A.ρ g.1) (y (g.2.1, g.2.2)) - y (g.1 * g.2.1, g.2.2) + y (g.1, g.2.1 * g.2.2) - y (g.1, g.2.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 : G → ↑A
⊢ f ∈ cocycles₁ A ↔ ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g

Tactic:
by
  simp_rw [mem_cocycles₁_def, sub_add_eq_add_sub, sub_eq_zero, eq_comm]

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
⊢ (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f = iCocycles A 0 ≫ (cochainsIso₀ A).hom

Tactic:
by
  dsimp [cocyclesIso₀]
  apply KernelFork.mapOfIsLimit_ι

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 ≫ η.hom = 𝟙 (forget k G)
⊢ α (α_inv 1) = 1

Tactic:
apply_fun (fun x ↦ (x.hom.app rightFDRep).hom (1 : G → k)) at this

Goal state after:
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 :
  (ConcreteCategory.hom ((η.inv ≫ η.hom).hom.app rightFDRep).hom) 1 =
    (ConcreteCategory.hom ((𝟙 (forget k G)).hom.app rightFDRep).hom) 1
⊢ α (α_inv 1) = 1
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⁻¹ * (MvPolynomial.C (m.leadingCoeff p) * (MvPolynomial.monomial (m.degree p)) 1)

Tactic:
← mul_assoc,

Goal state after:
σ : 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⁻¹ * MvPolynomial.C (m.leadingCoeff p) * (MvPolynomial.monomial (m.degree p)) 1
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_1 : ℕ), G n_1 ∈ I → G n_1 - ∑ i, C (T (G n_1) i) * F i = X * G (n_1 + 1)
⊢ g ∈ Submodule.span R⟦X⟧ (Set.range F)

Tactic:
have hG : ∀ n, G n ∈ I := Nat.rec hg fun n IH ↦
    (‹I.IsPrime›.mul_mem_iff_mem_or_mem.mp (hG' n IH ▸ I.sub_mem IH (I.sum_mem fun i _ ↦
      I.mul_mem_left _ (hJI (subset_span (Set.mem_range_self _)))))).resolve_left hXI

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_1 : ℕ), G n_1 ∈ I → G n_1 - ∑ i, C (T (G n_1) i) * F i = X * G (n_1 + 1)
hG : ∀ (n : ℕ), G n ∈ I
⊢ g ∈ Submodule.span R⟦X⟧ (Set.range F)
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
hfg : I.FG
⊢ spanFinrank I = spanFinrank (Ideal.map constantCoeff I)

Tactic:
refine le_antisymm ?_ ?_
  swap; · exact Ideal.spanFinrank_map_le_of_fg constantCoeff hfg
  have : RingHomSurjective (constantCoeff (R := R)) := ⟨constantCoeff_surj⟩
  obtain ⟨S, rfl, hS, hScard⟩ := exist_eq_span_eq_ncard_of_X_notMem hI
    (I.map constantCoeff).span_generators
    (FG.finite_generators <| map_eq_submodule_map constantCoeff I ▸ Submodule.FG.map _ hfg)
  refine le_trans (spanFinrank_span_le_ncard_of_finite hS) ?_
  rw [hScard, FG.generators_ncard]
  exact map_eq_submodule_map constantCoeff (Ideal.span S) ▸ Submodule.FG.map _ hfg

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

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
hf : Function.Injective ⇑f
inst✝ : Mono φ
i : ℕ
⊢ Mono ((chainsMap f φ).f i)

Tactic:
by
  simpa [ModuleCat.mono_iff_injective] using!
    (mapRange_injective φ.hom (map_zero _) <| (Rep.mono_iff_injective φ).1
    inferInstance).comp (mapDomain_injective hf.comp_left)

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

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

Tactic:
simp [coeff_truncTotal _ hx]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
f : A ⟶ B
⊢ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom = (H0Iso A).hom ≫ (coinvariantsFunctor k G).map f

Tactic:
by
  rw [← cancel_epi (H0π A)]
  ext
  simp

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
a b c n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
i j : ℕ
h : i ≤ j
⊢ (transitionMap I (↥(I ^ n • ⊤)) h) ((fun i ↦ ofValEqZeroAux I ⋯ hxn) j) = (fun i ↦ ofValEqZeroAux I ⋯ hxn) i

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
    rw [← (powSMulQuotInclusion_injective I rfl ⊤).eq_iff, ofValEqZeroAux_prop,
      ← LinearMap.comp_apply, ← factorPow_comp_powSMulQuotInclusion I rfl
      (show i + k + n = k + (i + n) by ring), LinearMap.comp_apply, ofValEqZeroAux_prop]
    exact x.prop (by lia)

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

Goal state before:
pp: case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
he : Function.Injective e
ve : G × G →₀ ↑A := mapDomain e v
hS : ↑(v + (ConcreteCategory.hom (d₂₁ A)) ve).support ⊆ ↑S
this :
  mapDomain Subtype.val (comapDomain Subtype.val (v + (ConcreteCategory.hom (d₂₁ A)) ve) ⋯) =
    v + (ConcreteCategory.hom (d₂₁ A)) ve
⊢ (ModuleCat.Hom.hom (d₂₁ A)) (ve - z) =
    ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype A))))
          ⟨comapDomain Subtype.val (v + (ConcreteCategory.hom (d₂₁ A)) ve) ⋯, ?w✝⟩) -
      ↑⟨x, hxc⟩

Tactic:
simp_all [mapCycles₁_hom, v, add_sub_assoc, sub_add_sub_cancel']

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

Goal state before:
pp: case h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinf A S).f).range

Tactic:
rcases @(ShortComplex.moduleCat_exact_iff_ker_sub_range _).1
    (H1CoresCoinfOfTrivial_exact (toCoinvariants A S) S)
    (H1π _ <| mapCycles₁ (MonoidHom.id G) (Rep.toCoinvariantsMkQ A S) x) (by
    simpa only [H1CoresCoinfOfTrivial_X₂, H1CoresCoinfOfTrivial_X₃, H1CoresCoinfOfTrivial_g,
      Iso.refl_inv, LinearMap.mem_ker, H1π_comp_map_apply (QuotientGroup.mk' S),
      ← mapCycles₁_comp_apply (x := x)] using! hx) with ⟨z, hz⟩

Goal state after:
case h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↑(H1CoresCoinfOfTrivial (A.toCoinvariants S) S).X₁
hz :
  (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial (A.toCoinvariants S) S).f) z =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinf A S).f).range
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.support.gcd p.coeff

Tactic:
Finset.dvd_gcd_iff

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ ∀ b ∈ p.support, Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff b
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
g : G
r : R
⊢ single ((mapDomainOfBialgHom f) g) r = f (single g r)

Tactic:
← mul_one r,

Goal state after:
R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
g : G
r : R
⊢ single ((mapDomainOfBialgHom f) g) (r * 1) = f (single g (r * 1))
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case mpr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range →
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker

Tactic:
· rintro ⟨x, hx⟩
    rw [← hx]
    exact Subtype.mk_eq_mk.mpr <| (QuotientGroup.eq_one_iff _).mpr ⟨Units.map (algebraMap R K) x,
      by simp only [powMonoidHom_apply, RingHom.toMonoidHom_eq_coe, map_pow]⟩

Goal state after: