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 κ ν
ω' : Ω'
⊢ Integrable (fun y ↦ rexp (0 * X y)) (κ ω') →
    (∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)) → IsFiniteMeasure (κ ω')

Tactic:
h

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : Integrable (fun y ↦ rexp (0 * X y)) (κ ω')
⊢ (∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)) → IsFiniteMeasure (κ ω')
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 κ ν
ω' : Ω'
⊢ IsFiniteMeasure (κ ω') → (∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)) → (κ ω') Set.univ ≤ 1

Tactic:
h

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : IsFiniteMeasure (κ ω')
⊢ (∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)) → (κ ω') Set.univ ≤ 1
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 κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : c = 0
ω' : Ω'
⊢ (κ ω') Set.univ ≤ 1 → (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-ε ^ 2 / (2 * ↑c))

Tactic:
h

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : c = 0
ω' : Ω'
h : (κ ω') Set.univ ≤ 1
⊢ (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-ε ^ 2 / (2 * ↑c))
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 κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : ¬c = 0
ω' : Ω'
⊢ (∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-t * ε + ↑c * t ^ 2 / 2)) →
    (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-ε ^ 2 / (2 * ↑c))

Tactic:
h

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : ¬c = 0
ω' : Ω'
h : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-t * ε + ↑c * t ^ 2 / 2)
⊢ (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-ε ^ 2 / (2 * ↑c))
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: x : ℕ → ℕ
n : ℕ
⊢ mkStrictMonoAux x n < mkStrictMonoAux x (n + 1)

Tactic:
grind [mkStrictMonoAux]

Goal state after:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: x : ℕ → ℕ
n : ℕ
⊢ x (n + 1) ≤ mkStrictMonoAux x (n + 1)

Tactic:
grind [mkStrictMonoAux]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h.hs
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
⊢ MeasurableSet (Set.Ioc ↑i ↑(i + 1))

Tactic:
exact measurableSet_Ioc

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
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
f g : ρ.IntertwiningMap σ
⊢ (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g → f = g

Tactic:
h

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
f g : ρ.IntertwiningMap σ
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
⊢ ∀ (g_1 : G) (v : V), (f.toLinearMap ∘ₗ g.toLinearMap) ((ρ g_1) v) = (τ g_1) ((f.toLinearMap ∘ₗ g.toLinearMap) v)

Tactic:
intro γ

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
γ : G
⊢ ∀ (v : V), (f.toLinearMap ∘ₗ g.toLinearMap) ((ρ γ) v) = (τ γ) ((f.toLinearMap ∘ₗ g.toLinearMap) v)
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module A V
ρ : Representation A G V
g : G
hg : g ∈ Submonoid.center G
⊢ ρ.IsIntertwiningMap ρ (ρ g)

Tactic:
rw [isIntertwiningMap_iff]

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module A V
ρ : Representation A G V
g : G
hg : g ∈ Submonoid.center G
⊢ ∀ (g_1 : G) (v : V), (ρ g) ((ρ g_1) v) = (ρ g_1) ((ρ g) v)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N : ℕ
⊢ ∑ x ∈ range N, (ε⁻¹ * (↑(u x))⁻¹) ^ 2 * Var[S (u x); ℙ] ≤ ε⁻¹ ^ 2 * C

Tactic:
mul_pow,

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N : ℕ
⊢ ∑ x ∈ range N, ε⁻¹ ^ 2 * (↑(u x))⁻¹ ^ 2 * Var[S (u x); ℙ] ≤ ε⁻¹ ^ 2 * C
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FDRep R G
f : (forget₂ (FDRep R G) (Rep R G)).obj X ⟶ (forget₂ (FDRep R G) (Rep R G)).obj Y
g : G
⊢ ModuleCat.Hom.hom (X.ρ g ≫ InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap)).hom =
    ModuleCat.Hom.hom (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap) ≫ Y.ρ g).hom

Tactic:
exact f.hom.2 g

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

Goal state before:
pp: case add
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : k[G]
x : V
g : k[G]
⊢ ∀ (y : k[G]),
    f ((((lift k (V →ₗ[k] V) G) ρ) g) x) = (((lift k (W →ₗ[k] W) G) σ) g) (f x) →
      f ((((lift k (V →ₗ[k] V) G) ρ) y) x) = (((lift k (W →ₗ[k] W) G) σ) y) (f x) →
        f ((((lift k (V →ₗ[k] V) G) ρ) (g + y)) x) = (((lift k (W →ₗ[k] W) G) σ) (g + y)) (f x)

Tactic:
h

Goal state after:
case add
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : k[G]
x : V
g h : k[G]
⊢ f ((((lift k (V →ₗ[k] V) G) ρ) g) x) = (((lift k (W →ₗ[k] W) G) σ) g) (f x) →
    f ((((lift k (V →ₗ[k] V) G) ρ) h) x) = (((lift k (W →ₗ[k] W) G) σ) h) (f x) →
      f ((((lift k (V →ₗ[k] V) G) ρ) (g + h)) x) = (((lift k (W →ₗ[k] W) G) σ) (g + h)) (f x)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ) = 0

Tactic:
by ext1; simp [zero_hom]

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 A B : Rep k G
⊢ ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ) = 0

Tactic:
by ext1; simp [zero_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
inst✝² : CommRing k
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
h : H
x : ↑A
y : ↑B
⊢ (ConcreteCategory.hom (coinvariantsTensorIndHom φ A B))
      ((((ind φ A).coinvariantsTensorMk B) ((IndV.mk φ A.ρ h) x)) y) =
    ((A.coinvariantsTensorMk (res φ B)) x) ((B.ρ h) y)

Tactic:
simp [coinvariantsTensorIndHom, coinvariantsTensorMk]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
h : QuasiIso (forget₂ToModuleCatHomotopyEquiv k G).hom
⊢ QuasiIso (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G))

Tactic:
← εToSingle₀_comp_eq k G

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
h :
  QuasiIso
    (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
      (HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ) 0).hom.app
        (trivial k G k))
⊢ QuasiIso (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G))
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
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)
            (MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single f r)))) =
    MonoidAlgebra.single (g • Fin.partialProd f) r

Tactic:
simp only [mkIso_inv, Representation.linearizeOfMulActionIso, Representation.Equiv.mk_symm,
        LinearEquiv.refl_symm, ConcreteCategory.hom_ofHom, Action.tensorObj_V, Action.trivial_V,
        Functor.mapIso_inv, tensor_V, tensor_ρ, Iso.symm_inv, Functor.Monoidal.μIso_hom, μ_hom,
        MonoidalCategory.tensorIso_inv, Representation.linearizeTrivialIso, hom_tensorHom,
        Representation.IntertwiningMap.tensor_apply, Representation.Equiv.coe_toIntertwiningMap,
        Representation.Equiv.mk_apply, LinearEquiv.refl_apply]

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
⊢ (Representation.linearizeMap (Action.diagonalSuccIsoTensorTrivial G m).inv)
      ((Representation.LinearizeMonoidal.μ (Action.leftRegular G) (Action.trivial G (Fin m → G)))
        ((LinearEquiv.refl k k[(Action.ofMulAction G G).V]) (MonoidAlgebra.single g 1) ⊗ₜ[k]
          MonoidAlgebra.single f r)) =
    MonoidAlgebra.single (g • Fin.partialProd f) r
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
m : ℕ
key : (barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ (diagonalSuccIsoFree k G m).inv = 0
⊢ barComplex.d k G (m + 1) ≫ barComplex.d k G m = 0

Tactic:
exact (cancel_mono (diagonalSuccIsoFree k G m).inv).mp (by simpa using key)

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
f : ↥(cocycles₂ A)
g : G
⊢ f (1, g) = f (1, 1)

Tactic:
have := ((mem_cocycles₂_iff f).1 f.2 1 1 g).symm
  simpa only [map_one, Module.End.one_apply, one_mul, add_right_inj, this]

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 : G →* H
φ : res f A ⟶ B
ψ : res g A ⟶ B
hfg : f = g
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ cochainsMap f φ = cochainsMap g ψ

Tactic:
subst hfg; congr; ext; simp [hφψ]

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 : G →* H
φ : res f A ⟶ B
ψ : res g A ⟶ B
hfg : f = g
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
n : ℕ
⊢ map f φ n = map g ψ n

Tactic:
subst hfg; congr; ext; simp [hφψ]

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
n : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↑(H1InfRes A S).X₁
hx : (ConcreteCategory.hom (H1InfRes A S).f) x = 0
⊢ x = 0

Tactic:
induction x using H1_induction_on with

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

Goal state before:
pp: case h.refine_2
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g✝ : G ⧸ S
g : G
⊢ ∀ (b : G), (QuotientGroup.leftRel S) g b → ⟨↑x g - (A.ρ g) y + y, ⋯⟩ = ⟨↑x b - (A.ρ b) y + y, ⋯⟩

Tactic:
h

Goal state after:
case h.refine_2
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g✝ : G ⧸ S
g h : G
⊢ (QuotientGroup.leftRel S) g h → ⟨↑x g - (A.ρ g) y + y, ⋯⟩ = ⟨↑x h - (A.ρ h) y + y, ⋯⟩
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: case h.refine_3
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g : G ⧸ S
⊢ ∀ (h : G ⧸ S),
    Quotient.liftOn' (g * h) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯ =
      ((A.quotientToInvariants S).ρ g) (Quotient.liftOn' h (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) +
        Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯

Tactic:
h

Goal state after:
case h.refine_3
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g h : G ⧸ S
⊢ Quotient.liftOn' (g * h) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯ =
    ((A.quotientToInvariants S).ρ g) (Quotient.liftOn' h (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) +
      Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Nontrivial k
s t : G
⊢ (equivHom k G) s = (equivHom k G) t → s = t

Tactic:
h

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Nontrivial k
s t : G
h : (equivHom k G) s = (equivHom k G) t
⊢ s = t
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↑(H1InfRes A S).X₂
hx : x ∈ (ModuleCat.Hom.hom (H1InfRes A S).g).ker
⊢ x ∈ (ModuleCat.Hom.hom (H1InfRes A S).f).range

Tactic:
induction x using H1_induction_on with

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsDomain k
η : Aut (forget k G)
⊢ ∃ a, (equivHom k G) a = η

Tactic:
obtain ⟨s, h⟩ := toRightFDRepComp_in_rightRegular η

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsDomain k
η : Aut (forget k G)
s : G
h : Hom.hom (η.hom.hom.app rightFDRep).hom = rightRegular s
⊢ ∃ a, (equivHom k G) a = η
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:
by
  simp only [map_add, d₂₁_single (G := G), inv_self_apply, inv_inv, inv_mul_cancel_left]
  abel

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
a₁✝ a₂✝ : MvPowerSeries σ R
⊢ (rename ⇑e) a₁✝ = (rename ⇑e) a₂✝ → a₁✝ = a₂✝

Tactic:
h

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
a₁✝ a₂✝ : MvPowerSeries σ R
h : (rename ⇑e) a₁✝ = (rename ⇑e) a₂✝
⊢ a₁✝ = a₂✝
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
this : ∀ x ∈ I, C (constantCoeff x) ∈ I
⊢ Ideal.map (C.comp constantCoeff) I ≤ I

Tactic:
simpa [Ideal.map_le_iff_le_comap]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : WithIdeal S
e : R ≃+* S
h : Ideal.map e.toRingHom i = i
⊢ Ideal.map e.toRingHom i ≤ i

Tactic:
h

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : WithIdeal S
e : R ≃+* S
h : Ideal.map e.toRingHom i = i
⊢ i ≤ i
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : WithIdeal S
e : R ≃+* S
h : Ideal.map e.toRingHom i = i
⊢ Ideal.map e.symm.toRingHom i ≤ i

Tactic:
by simp [← h]

Goal state after:
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 : MvPolynomial σ R
x : σ →₀ ℕ
⊢ degree x < n → MvPolynomial.coeff x ((truncTotal n) ↑p - p) = 0

Tactic:
h

Goal state after:
σ✝ : 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 : MvPolynomial σ R
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) ↑p - p) = 0
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 : G →* H
φ : A ⟶ res f B
ψ : A ⟶ res g B
hfg : f = g
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ chainsMap f φ = chainsMap g ψ

Tactic:
subst hfg; congr; ext; simp [hφψ]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
m : (maximalIdeal R).Cotangent
hm : f m = 0
m' : ↥(maximalIdeal R)
hm' : (maximalIdeal R).toCotangent m' = m
⊢ m = 0

Tactic:
simp only [← hm', mapCotangent_toCotangent, Algebra.ofId_apply, toCotangent_eq_zero,
      maximalIdeal_eq_map, ← Ideal.map_pow, f] at hm

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
m : (maximalIdeal R).Cotangent
m' : ↥(maximalIdeal R)
hm' : (maximalIdeal R).toCotangent m' = m
hm :
  (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' ∈
    Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal R ^ 2)
⊢ m = 0