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

Goal state before:
pp: X Y : Stoch
κ : X ⟶ Y
inst✝ : Deterministic κ
this : copy Y.obj.carrier ∘ₖ κ.hom.hom = κ.hom.hom ∥ₖ κ.hom.hom ∘ₖ copy X.obj.carrier
⊢ κ.hom.hom ∥ₖ κ.hom.hom ∘ₖ copy X.obj.carrier = copy Y.obj.carrier ∘ₖ κ.hom.hom

Tactic:
exact this.symm

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndep m' (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) hm' μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']

Tactic:
condIndep_iff _ _ _ _ hf.comap_le hg.comap_le

Goal state after:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']) ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
⊢ ∫ (x : Ω), (⇑f ∘ A.indicator 1 * ∏ t, ⇑(g t) ∘ X t) x ∂P =
    (∫ (x : Ω), (⇑f ∘ A.indicator 1) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ X t) x ∂P

Tactic:
have h1 ω : f (A.indicator 1 ω) * ∏ s, g s (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, g s (X s ω)) ω +
      f 0 * ∏ s, g s (X s ω) - A.indicator (fun ω ↦ f 0 * ∏ s, g s (X s ω)) ω := by
    classical
    rw [Set.indicator_apply]
    split_ifs <;> simp_all

Goal state after:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
⊢ ∫ (x : Ω), (⇑f ∘ A.indicator 1 * ∏ t, ⇑(g t) ∘ X t) x ∂P =
    (∫ (x : Ω), (⇑f ∘ A.indicator 1) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ X t) x ∂P
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case e'_3
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g) =
    ⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ∘ₘ μ.trim hm'

Tactic:
rw [Measure.compProd_eq_comp_prod]

Goal state after:
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
⊢ volume {x_1 | f a x_1 ≤ x} = (κ a) (Iic x)

Tactic:
Iic_to_Icc,

Goal state after:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
⊢ volume {x_1 | f a x_1 ≤ x} = (κ a) (Icc 0 x)
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
ι : Type u_3
inst✝⁶ : LinearOrder ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst✝¹ : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_countable_range : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}
⊢ stoppedValue f τ =ᵐ[μ.restrict (⋃ i ∈ Set.range τ, {x | τ x = i})] μ[f n | hτ.measurableSpace]

Tactic:
ae_eq_restrict_biUnion_iff _ h_countable_range

Goal state after:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
ι : Type u_3
inst✝⁶ : LinearOrder ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst✝¹ : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_countable_range : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}
⊢ ∀ i ∈ Set.range τ, stoppedValue f τ =ᵐ[μ.restrict {x | τ x = i}] μ[f n | hτ.measurableSpace]
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ Integrable (fun a ↦ |X a| ^ ↑p) (μ.tilted fun x ↦ t * X x)

Tactic:
integrable_tilted_iff (interior_subset (s := integrableExpSet X μ) ht),

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ Integrable (fun x ↦ rexp (t * X x) • |X x| ^ ↑p) μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case mgf_le
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
X : Ω → ℝ
c : ℝ≥0
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf X (0 ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
simp [exp_nonneg]

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : ConditionallyCompleteLinearOrderBot ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝² : SecondCountableTopology ι
inst✝¹ : IsFiniteMeasure P
inst✝ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
this : ∑' (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} < ∞
⊢ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x ↦ min (τ x ω) (σ x (nk x) ω)) atTop (𝓝 ⊤)

Tactic:
filter_upwards [ae_eventually_notMem this.ne, hτ.tendsto_top] with ω hω hωτ

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : ConditionallyCompleteLinearOrderBot ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝² : SecondCountableTopology ι
inst✝¹ : IsFiniteMeasure P
inst✝ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
this : ∑' (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, ¬σ n (nk n) ω < min (τ n ω) ↑(T n)
hωτ : Tendsto (fun x ↦ τ x ω) atTop (𝓝 ⊤)
⊢ Tendsto (fun x ↦ min (τ x ω) (σ x (nk x) ω)) atTop (𝓝 ⊤)
Module: Mathlib.RepresentationTheory.Rep.Res

Goal state before:
pp: G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
f : H →* G
k : Type u
inst✝ : CommRing k
S : ShortComplex (Rep k G)
⊢ (S.map (resFunctor f)).Exact ↔ S.Exact

Tactic:
rw [ShortComplex.exact_map_iff_of_faithful]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : CommRing k
inst✝ : Monoid G
A B C : TopRep k G
f : A ⟶ B
r : k
g : B ⟶ C
x✝ : ↑A
⊢ (Hom.hom (f ≫ (r • g))).toContinuousLinearMap x✝ = (Hom.hom (r • f ≫ g)).toContinuousLinearMap x✝

Tactic:
simp [hom_smul, ContIntertwiningMap.smul_comp]

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
f : V →ₗ[k[G]] W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this✝² : Module k W := Module.compHom W (algebraMap k A)
this✝¹ : Module k V := Module.compHom V (algebraMap k A)
this✝ : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V := (↑k f).leftInverse
hφ : ∀ (x : V), φ (f x) = x
x✝ : Fintype G
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Tactic:
refine ⟨φ.equivariantProjection G, LinearMap.ext ?_⟩

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
f : V →ₗ[k[G]] W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this✝² : Module k W := Module.compHom W (algebraMap k A)
this✝¹ : Module k V := Module.compHom V (algebraMap k A)
this✝ : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V := (↑k f).leftInverse
hφ : ∀ (x : V), φ (f x) = x
x✝ : Fintype G
⊢ ∀ (x : V), (LinearMap.equivariantProjection G φ ∘ₗ f) x = LinearMap.id x
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Rep k G
⊢ (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)

Tactic:
ext1; simp [← comm_symm Y.ρ X.ρ, ← toIntertwiningMap_trans,
    trans_symm, toIntertwiningMap_refl]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
⊢ Coinvariants.ker (leftRegular k G) = ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker

Tactic:
have := Fintype.ofFinite G

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
⊢ Coinvariants.ker (leftRegular k G) = ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
A : Rep k G
n : ℕ
r : k
f : (Fin n → G) → ↑A
⊢ (fun g ↦
      (A.ρ (g 0)) ((r • f) fun i ↦ g i.succ) + ∑ j, (-1) ^ (↑j + 1) • (r • f) (j.contractNth (fun x1 x2 ↦ x1 * x2) g)) =
    (RingHom.id k) r • fun g ↦
      (A.ρ (g 0)) (f fun i ↦ g i.succ) + ∑ j, (-1) ^ (↑j + 1) • f (j.contractNth (fun x1 x2 ↦ x1 * x2) g)

Tactic:
by
      ext
      simp [Finset.smul_sum, ← smul_assoc, mul_comm r]

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
s : G
⊢ TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
      (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ s =
    TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)

Tactic:
by
    simp only [MonoidalCategory.curriedTensor_obj_obj, tensor_V, tensor_ρ, tprod_apply,
      MonoidHom.coe_comp, Function.comp_apply]
    ext x y
    simpa [Coinvariants.mk_eq_iff, coinvariantsTensorMk] using
      Coinvariants.mem_ker_of_eq (φ s) (IndV.mk φ A.ρ (1 : H) x ⊗ₜ[k] y) _ <| by
      simp [← Coinvariants.mk_inv_tmul]

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 j : ℕ),
    (ComplexShape.up ℕ).Rel i j →
      A.leftRegularHomEquiv.toModuleIso.hom ≫ (moduleCatCochainComplex A g).d i j =
        ((resolution k g hg).complex.linearYonedaObj k A).d i j ≫ A.leftRegularHomEquiv.toModuleIso.hom

Tactic:
by
    rintro i j ⟨rfl⟩
    ext (x : leftRegular _ _ ⟶ _)
    by_cases hi : Even i
    · have : ¬(Even (i + 1)) := Nat.even_add_one.not_left.mpr hi
      simp [sub_hom, hi, this, homEquiv, ← hom_comm_apply x, Rep.applyAsHom]
    · simp [hi, Nat.even_add_one.2 hi, Representation.norm, homEquiv, Rep.norm, ← hom_comm_apply x]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
m : ℕ
f : Fin m → G
g : G
⊢ ∀ (r : k),
    (Hom.hom (diagonalSuccIsoFree k G m).inv) (single f (MonoidAlgebra.single g r)) =
      MonoidAlgebra.single (g • Fin.partialProd f) r

Tactic:
r

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
m : ℕ
f : Fin m → G
g : G
r : k
⊢ (Hom.hom (diagonalSuccIsoFree k G m).inv) (single f (MonoidAlgebra.single g r)) =
    MonoidAlgebra.single (g • Fin.partialProd f) r
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⁻¹) = -f g

Tactic:
by
  rw [← add_eq_zero_iff_eq_neg, ← cocycles₁_map_one f, ← mul_inv_cancel g,
    (mem_cocycles₁_iff f).1 f.2 g g⁻¹]

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
⊢ toCocycles A 0 1 ≫ (isoCocycles₁ A).hom = (cochainsIso₀ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.f'

Tactic:
simp [← cancel_mono (shortComplexH1 A).moduleCatLeftHomologyData.i, comp_d₀₁_eq,
    shortComplexH1_f]

Goal state after:
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 × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
x✝ : Fin 1 → G
⊢ ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) ((ConcreteCategory.hom (chainsIso₁ X.X₁).inv) x)) x✝ =
    ((ConcreteCategory.hom ((inhomogeneousChains X.X₂).d 2 1)) ((ConcreteCategory.hom (chainsIso₂ X.X₂).inv) y)) x✝

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

Goal state after:
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 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:
induction g using QuotientGroup.induction_on with | @H g =>
    induction h using QuotientGroup.induction_on with | @H h =>
    apply Subtype.ext
    simp [← QuotientGroup.mk_mul, h1 g h, sub_add_eq_add_sub, add_assoc]

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 h : α (α_inv 1) = 1
⊢ α 1 = 1

Tactic:
← one_mul (α_inv 1),

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 : α (1 * α_inv 1) = 1
h : α (α_inv 1) = 1
⊢ α 1 = 1
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)
h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep
⊢ η₁ = η₂

Tactic:
have := Fintype.ofFinite G

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η₁ η₂ : Aut (forget k G)
h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep
this : Fintype G
⊢ η₁ = η₂
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
x✝ : ((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ x✝ ∈ ↑⋯.toFinset →
    ∀ ⦃x₂ : ((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)⦄,
      x₂ ∈ ↑⋯.toFinset →
        ((match x✝ with
            | (fst, b) => (b.1 + b.2, b)) =
            match x₂ with
            | (fst, b) => (b.1 + b.2, b)) →
          x✝ = x₂

Tactic:
simp; grind

Goal state after:
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 : G
a : ↑A
⊢ (ConcreteCategory.hom (d₂₁ A)) (single (g, g⁻¹) ((A.ρ g) a) - single (g⁻¹, g) a) = single 1 a - single 1 ((A.ρ g) a)

Tactic:
simp only [map_sub, d₂₁_single (G := G), inv_self_apply, mul_inv_cancel, inv_inv,
    inv_mul_cancel]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g : G
a : ↑A
⊢ single g⁻¹ a - single 1 ((A.ρ g) a) + single g ((A.ρ g) a) - (single g ((A.ρ g) a) - single 1 a + single g⁻¹ a) =
    single 1 a - single 1 ((A.ρ 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 : G × G × G
a : ↑A
⊢ (ConcreteCategory.hom (d₃₂ A)) (single g a) =
    single (g.2.1, g.2.2) ((A.ρ g.1⁻¹) a) - single (g.1 * g.2.1, g.2.2) a + single (g.1, g.2.1 * g.2.2) a -
      single (g.1, g.2.1) a

Tactic:
by
  simp [d₃₂]

Goal state after:
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 (1, g, h) a) = single (1, g * h) a - single (1, g) a

Tactic:
by
  simp [d₃₂]

Goal state after:
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, 1, h) a) = single (1, h) ((A.ρ g⁻¹) a) - single (g, 1) a

Tactic:
by
  simp [d₃₂]

Goal state after:
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, 1) a) = single (h, 1) ((A.ρ g⁻¹) a) - single (g * h, 1) a

Tactic:
by
  simp [d₃₂]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
w✝ : Ideal R
hI : w✝ ∈ C
⊢ ↑(sSup C) ∩ ↑S = ∅

Tactic:
eq_empty_iff_forall_notMem

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
w✝ : Ideal R
hI : w✝ ∈ C
⊢ ∀ (x : R), x ∉ ↑(sSup C) ∩ ↑S
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
S : Type u_5
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
e✝ e : σ ↪ τ
⊢ ∀ (r : R), killComplFun e ((algebraMap R (MvPowerSeries τ R)) r) = (algebraMap R (MvPowerSeries σ R)) r

Tactic:
by simpa using! killComplFun_monomial_embDomain 0

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ d₃₂ A ≫ d₂₁ A = 0

Tactic:
simp [← cancel_mono (chainsIso₁ A).inv, ← eq_d₂₁_comp_inv, ← eq_d₃₂_comp_inv_assoc,
    ChainComplex.of.d, inhomogeneousChains.d_comp_d]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
hzero : 0 ∉ closure {r | Prime r}
h : span {a} ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : ↑T ∩ ↑(closure {r | Prime r}).toSubsemigroup = ∅
hT₂ : ∀ I ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
Tpri : T.IsPrime
x : R
H₃ : x ∈ T
H₄ : Prime x
⊢ False

Tactic:
eq_empty_iff_forall_notMem

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
hzero : 0 ∉ closure {r | Prime r}
h : span {a} ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : ∀ (x : R), x ∉ ↑T ∩ ↑(closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
Tpri : T.IsPrime
x : R
H₃ : x ∈ T
H₄ : Prime x
⊢ False
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 : σ →₀ ℕ
⊢ (coeff y) ((PowerSeries.coeff n) (optionFunLeft σ R ((monomial x) r))) =
    (coeff y) ((PowerSeries.coeff n) ((PowerSeries.monomial (x none)) ((monomial x.some) r)))

Tactic:
PowerSeries.coeff_monomial,

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