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

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

Tactic:
← exp_cgf (hi t),

Goal state after:
Ω : 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
⊢ rexp (cgf X μ t) ≤ rexp ((↑‖b - a‖₊ / 2) ^ 2 * t ^ 2 / 2)
Module: Mathlib.RepresentationTheory.Rep.Res

Goal state before:
pp: case mp
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
h : (S.map (resFunctor φ)).ShortExact
h₁ : (S.map (resFunctor φ)).Exact
⊢ S.ShortExact

Tactic:
have h₂ := h.2

Goal state after:
case mp
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
h : (S.map (resFunctor φ)).ShortExact
h₁ : (S.map (resFunctor φ)).Exact
h₂ : Mono (S.map (resFunctor φ)).f
⊢ S.ShortExact
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
⊢ (fun i ↦ ∫ (a : Ω), truncation (X i) (↑i) a) = (fun A ↦ ∫ (x : Ω), truncation (X 0) A x) ∘ Nat.cast

Tactic:
ext i

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
i : ℕ
⊢ ∫ (a : Ω), truncation (X i) (↑i) a = ((fun A ↦ ∫ (x : Ω), truncation (X 0) A x) ∘ Nat.cast) i
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V : FDRep k G
⊢ (↑(Nat.card G))⁻¹ * ∑ g, V.character g = ↑(finrank k ↥(invariants V.ρ))

Tactic:
have : Invertible (Fintype.card G : k) := by
    rwa [Fintype.card_eq_nat_card]

Goal state after:
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V : FDRep k G
this : Invertible ↑(Fintype.card G)
⊢ (↑(Nat.card G))⁻¹ * ∑ g, V.character g = ↑(finrank k ↥(invariants V.ρ))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case hident
Ω : 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 ∂μ))
k : ℕ
G : ℕ → E → ℝ := fun k x ↦ ‖x - (φ k) x‖
G_meas : ∀ (k : ℕ), Measurable (G k)
I : ∀ (k i : ℕ), (fun ω ↦ ‖(X i - Y k i) ω‖) = G k ∘ X i
i : ℕ
⊢ IdentDistrib (G k ∘ X i) (G k ∘ X 0) μ μ

Tactic:
apply (hident i).comp (G_meas k)

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep.{?u.16, u, v} k G
⊢ ∀ {X : Rep.{max w t, u, w} k H} {Y Y' : Rep.{max w t, u, v} k G} (f : (resFunctor φ).obj X ⟶ Y) (g : Y ⟶ Y'),
    (resCoindHomEquiv.{t, u, v, w} φ X Y').toEquiv (f ≫ g) =
      (resCoindHomEquiv.{t, u, v, w} φ X Y).toEquiv f ≫ (coindFunctor k φ).map g

Tactic:
by intros; ext; rfl

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
p : Submodule k[G] V
⊢ ∃ q, IsCompl p q

Tactic:
rcases MonoidAlgebra.exists_leftInverse_of_injective p.subtype p.ker_subtype with ⟨f, hf⟩
  exact ⟨LinearMap.ker f, LinearMap.isCompl_of_proj <| DFunLike.congr_fun hf⟩

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case refine_1
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
x✝ : Mono f
hf : IsIso 0
habs : f = 0
⊢ False

Tactic:
isIsoZero_iff_source_target_isZero

Goal state after:
case refine_1
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
x✝ : Mono f
hf : IsZero W ∧ IsZero V
habs : f = 0
⊢ False
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case succ
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
⊢ HomologicalComplex.ExactAt ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 1)

Tactic:
HomologicalComplex.exactAt_iff' _ (m + 2) (m + 1) m (by simp) (by simp)

Goal state after:
case succ
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
⊢ (HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).Exact
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
⊢ coinvariantsTensorIndInv φ A B ≫ coinvariantsTensorIndHom φ A B = 𝟙 (((coinvariantsTensor k G).obj A).obj (res φ B))

Tactic:
by
    ext
    simp [coinvariantsTensorIndInv, coinvariantsTensorMk, coinvariantsTensorIndHom]

Goal state after:
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ε : (algebraMap A L) 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:
mul_left_comm,

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) η * ((algebraMap A L) t * g (IsLocalization.mk' L a b)) = t • IsLocalization.mk' L a b
⊢ η * ((galRestrict A K L B) g) a = a
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ε : (algebraMap B L) η * ↑g ((algebraMap B L) a) = (algebraMap B L) a
⊢ η * ((galRestrict A K L B) g) a = a

Tactic:
apply IsIntegralClosure.algebraMap_injective B A L

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ˣ := ⋯
ε : 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
⊢ (algebraMap B L) (η * ((galRestrict A K L B) g) a) = (algebraMap B L) a
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
⊢ (G → k) →ₐ[k] G → k

Tactic:
refine AlgHom.ofLinearMap α ?_ (map_mul_toRightFDRepComp η)

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
⊢ α 1 = 1
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
s x✝¹ : G
f : ↑rightFDRep.V.obj
x✝ : G
⊢ (Hom.hom (rightFDRep.ρ x✝¹ ≫ InducedCategory.homMk (↟(leftRegular s))).hom) f x✝ =
    (Hom.hom (InducedCategory.homMk (↟(leftRegular s)) ≫ rightFDRep.ρ x✝¹).hom) f x✝

Tactic:
apply congrArg f

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
s x✝¹ : G
f : ↑rightFDRep.V.obj
x✝ : G
⊢ s⁻¹ * x✝ * x✝¹ = s⁻¹ * (x✝ * x✝¹)
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (t : Set R), t ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ t

Tactic:
intro U

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ U ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
⊢ optionFunLeft σ R ((monomial x) r) = (PowerSeries.monomial (x none)) ((monomial x.some) r)

Tactic:
ext n y
  rw [PowerSeries.coeff_monomial, coeff_coeff_optionFunLeft, coeff_monomial]
  split_ifs with h1 h2 h3
  · simp [← h1]
  · absurd h2
    rw [← optionElim_apply_none n, h1]
  · replace h1 : ¬ y = x.some := fun h ↦ by
      absurd h1; ext u
      cases u <;> simp_all
    rw [coeff_monomial, if_neg h1]
  · rw [coeff_zero]

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

Goal state before:
pp: case mpr.right
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
a✝ : DiscreteTopology A
⊢ ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s

Tactic:
intro U

Goal state after:
case mpr.right
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
a✝ : DiscreteTopology A
U : Set A
⊢ U ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ U
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ map (MonoidHom.id G) (𝟙 A) n = 𝟙 (groupHomology A n)

Tactic:
simp [map, groupHomology]

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
⊢ x = 0

Tactic:
ext i

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 • ⊤)
hx : (ofPowSMul I M n) x = 0
i : ℕ
⊢ ↑x i = ↑0 i
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 M
hxn : ↑x n = 0
⊢ (ofPowSMul I M n) (ofValEqZero I hxn) = x

Tactic:
ext i

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 M
hxn : ↑x n = 0
i : ℕ
⊢ ↑((ofPowSMul I M n) (ofValEqZero I hxn)) i = ↑x i
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
n : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ ↑(A.ofQuotient S)
hx : x ∈ cycles₁ (A.ofQuotient S)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), ↑(s b) = b
⊢ ∃ a, (ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) a = ⟨x, hx⟩

Tactic:
have hs₁ : QuotientGroup.mk ∘ s = id := funext hs

Goal state after:
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
n : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ ↑(A.ofQuotient S)
hx : x ∈ cycles₁ (A.ofQuotient S)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), ↑(s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
⊢ ∃ a, (ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) a = ⟨x, hx⟩
Module: Mathlib.RingTheory.Flat.Domain

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ (Finsupp.linearCombination R fun i ↦ v i.1 ⊗ₜ[R] w i.2) =
    TensorProduct.map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
      ↑(finsuppTensorFinsupp' R ι κ).symm

Tactic:
ext i

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
hv : LinearIndependent R v
hw : LinearIndependent R w
i : ι × κ
⊢ ((Finsupp.linearCombination R fun i ↦ v i.1 ⊗ₜ[R] w i.2) ∘ₗ Finsupp.lsingle i) 1 =
    ((TensorProduct.map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
          ↑(finsuppTensorFinsupp' R ι κ).symm) ∘ₗ
        Finsupp.lsingle i)
      1
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).contentIdeal ≤ p.contentIdeal * q.contentIdeal

Tactic:
contentIdeal_def,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ span ↑(p * q).coeffs ≤ p.contentIdeal * q.contentIdeal
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.contentIdeal ≤ span {p.content}

Tactic:
contentIdeal_def,

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ span ↑p.coeffs ≤ span {p.content}
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
n : ℕ
⊢ chainsMap₃ f φ ≫ (shortComplexH2 B).f = (shortComplexH2 A).f ≫ chainsMap₂ f φ

Tactic:
simp only [shortComplexH2]

Goal state after:
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
n : ℕ
⊢ chainsMap₃ f φ ≫ d₃₂ B = d₃₂ A ≫ chainsMap₂ f φ
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
n : ℕ
⊢ chainsMap₂ f φ ≫ (shortComplexH2 B).g = (shortComplexH2 A).g ≫ chainsMap₁ f φ

Tactic:
simp only [shortComplexH2]

Goal state after:
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
n : ℕ
⊢ chainsMap₂ f φ ≫ d₂₁ B = d₂₁ A ≫ chainsMap₁ f φ
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_1
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
⊢ (mapShortComplexH2 f 0).τ₁ = Hom.τ₁ 0

Tactic:
simp only [shortComplexH2]

Goal state after:
case refine_1
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
⊢ (mapShortComplexH2 f 0).τ₁ = Hom.τ₁ 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_2
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
⊢ (mapShortComplexH2 f 0).τ₂ = Hom.τ₂ 0

Tactic:
simp only [shortComplexH2]

Goal state after:
case refine_2
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
⊢ (mapShortComplexH2 f 0).τ₂ = Hom.τ₂ 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_3
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
⊢ (mapShortComplexH2 f 0).τ₃ = Hom.τ₃ 0

Tactic:
simp only [shortComplexH2]

Goal state after:
case refine_3
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
⊢ (mapShortComplexH2 f 0).τ₃ = Hom.τ₃ 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_1
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₁ = (𝟙 (shortComplexH2 A)).τ₁

Tactic:
simp only [shortComplexH2]

Goal state after:
case refine_1
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₁ =
    (𝟙
        { X₁ := ModuleCat.of k (G × G × G →₀ ↑A), X₂ := ModuleCat.of k (G × G →₀ ↑A), X₃ := ModuleCat.of k (G →₀ ↑A),
          f := d₃₂ A, g := d₂₁ A, zero := ⋯ }).τ₁
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_2
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₂ = (𝟙 (shortComplexH2 A)).τ₂

Tactic:
simp only [shortComplexH2]

Goal state after:
case refine_2
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₂ =
    (𝟙
        { X₁ := ModuleCat.of k (G × G × G →₀ ↑A), X₂ := ModuleCat.of k (G × G →₀ ↑A), X₃ := ModuleCat.of k (G →₀ ↑A),
          f := d₃₂ A, g := d₂₁ A, zero := ⋯ }).τ₂
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_3
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₃ = (𝟙 (shortComplexH2 A)).τ₃

Tactic:
simp only [shortComplexH2]

Goal state after:
case refine_3
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₃ =
    (𝟙
        { X₁ := ModuleCat.of k (G × G × G →₀ ↑A), X₂ := ModuleCat.of k (G × G →₀ ↑A), X₃ := ModuleCat.of k (G →₀ ↑A),
          f := d₃₂ A, g := d₂₁ A, zero := ⋯ }).τ₃
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_1
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ (resFunctor f).map ψ)).τ₁ = (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁

Tactic:
simp only [shortComplexH2]

Goal state after:
case refine_1
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ resMap f ψ)).τ₁ = (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_2
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ (resFunctor f).map ψ)).τ₂ = (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂

Tactic:
simp only [shortComplexH2]

Goal state after:
case refine_2
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ resMap f ψ)).τ₂ = (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_3
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ (resFunctor f).map ψ)).τ₃ = (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃

Tactic:
simp only [shortComplexH2]

Goal state after:
case refine_3
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ resMap f ψ)).τ₃ = (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃