mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
p : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp : IsStable 𝓕 p
⊢ IsStable 𝓕 fun Y ↦ Locally p 𝓕 Y P

Tactic:
by
  refine fun X hX τ hτ ↦ ⟨hX.localSeq, hX.isLocalizingSequence_localSeq, fun n ↦ ?_⟩
  simp_rw [← stoppedProcess_indicator_comm', Set.indicator_indicator, Set.inter_comm,
    ← Set.indicator_indicator, stoppedProcess_stoppedProcess, inf_comm,
    stoppedProcess_indicator_comm', ← stoppedProcess_stoppedProcess]
  exact hp _ (hX.stoppedProcess_localSeq n) τ hτ

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
ε : ℚ
ω' : Ω'
a✝ : IsFiniteMeasure (κ ω')
hε : 0 < ε
hm : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ↑ε ≤ X ω} ≤ rexp (-(t * ↑ε))
this : (κ ω').real {ω | ↑ε ≤ X ω} = 0
⊢ (κ ω') {ω | ↑ε ≤ X ω} = 0

Tactic:
by simpa [Measure.real, ENNReal.toReal_eq_zero_iff]

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp : IsStable 𝓕 p✝
hq : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX : Locally p✝ 𝓕 X P
hqX : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
⊢ IsStable 𝓕 p →
    IsStable 𝓕 q →
      ∀ (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P),
        p
          (stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i))
            ((hpX.localSeq ⊓ hqX.localSeq) n))

Tactic:
hp

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp✝ : IsStable 𝓕 p✝
hq : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX : Locally p✝ 𝓕 X P
hqX : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
⊢ IsStable 𝓕 q →
    ∀ (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P),
      p
        (stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i))
          ((hpX.localSeq ⊓ hqX.localSeq) n))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |truncation f A x| ≤ |f x|

Tactic:
by
  simp only [truncation, indicator, id, Function.comp_apply]
  split_ifs
  · exact le_rfl
  · simp [abs_nonneg]

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁸ : ConditionallyCompleteLinearOrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : IsFiniteMeasure P
inst✝³ : DenselyOrdered ι
inst✝² : NoMaxOrder ι
inst✝¹ : Zero E
inst✝ : 𝓕.IsRightContinuous
hp : IsStable 𝓕 p
hL : Locally (fun Y ↦ Locally p 𝓕 Y P) 𝓕 X P
⊢ Locally p 𝓕 X P

Tactic:
choose τ hτ₁ hτ₂ using hL.stoppedProcess_localSeq

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁸ : ConditionallyCompleteLinearOrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : IsFiniteMeasure P
inst✝³ : DenselyOrdered ι
inst✝² : NoMaxOrder ι
inst✝¹ : Zero E
inst✝ : 𝓕.IsRightContinuous
hp : IsStable 𝓕 p
hL : Locally (fun Y ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : ℕ → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun i ↦
          {ω | ⊥ < τ n n_1 ω}.indicator
            (stoppedProcess (fun i ↦ {ω | ⊥ < hL.localSeq n ω}.indicator (X i)) (hL.localSeq n) i))
        (τ n n_1))
⊢ Locally p 𝓕 X P
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case hc
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ ∫ (x : Ω), (-X) x ∂μ = 0

pp: case ht
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ 0 < -t

Tactic:
· simp only [Pi.neg_apply]; rw [integral_neg, hc, neg_zero]

Goal state after:
case ht
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ 0 < -t
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → k[G] := fun x ↦ single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x, single (x * g) 1 = ⅟↑(Fintype.card G) • Finset.univ.sum f

Tactic:
change ⅟(Fintype.card G : k) • ∑ x : G, f (x * g) = ⅟(Fintype.card G : k) • ∑ x : G, f x

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → k[G] := fun x ↦ single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x, f (x * g) = ⅟↑(Fintype.card G) • ∑ x, f x
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Group G
X Y : FDRep k G
⊢ ↥(linHom X.ρ Y.ρ).invariants ≃ₗ[k] X ⟶ Y

Tactic:
by
  rw [← FDRep.forget₂_ρ, ← FDRep.forget₂_ρ]
  -- Porting note: The original version used `linHom.invariantsEquivRepHom _ _ ≪≫ₗ`
  exact linHom.invariantsEquivRepHom
    ((forget₂ (FDRep k G) (Rep k G)).obj X) ((forget₂ (FDRep k G) (Rep k G)).obj Y) ≪≫ₗ
    FDRep.forget₂HomLinearEquiv X Y

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_5
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ✝ φ ψ : SimpleFunc E E
hφ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hψ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
ω : Ω
hωφ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hωψ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
⊢ 𝓝 (∫ (x : Ω), (⇑(φ + ψ) ∘ X 0) x ∂μ) = 𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ + ∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ)

Tactic:
congr 1
      rw [← integral_add]
      · rfl
      · exact (φ.comp (X 0) h').integrable_of_isFiniteMeasure
      · exact (ψ.comp (X 0) h').integrable_of_isFiniteMeasure

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u_6
G : Type u_7
V : Type u_8
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
α : Type u_9
a : α
x : V
⊢ (ρ.finsuppToCoinvariants α) (single a ((Coinvariants.mk ρ) x)) = (Coinvariants.mk (ρ.finsupp α)) (single a x)

Tactic:
by
  simp [finsuppToCoinvariants]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
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) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun i ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
Yint : Integrable (Y 0) μ
C : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
⊢ (∀ (n : ℕ), X n ω = Y n ω) →
    Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ)) →
      Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
h₁

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
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) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun i ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
Yint : Integrable (Y 0) μ
C : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
h₁ : ∀ (n : ℕ), X n ω = Y n ω
⊢ Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ)) →
    Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f : π₁ →ⁱL π₂
⊢ ∀ (g : G), (-f.toContinuousLinearMap) ∘SL π₁ g = π₂ g ∘SL (-f.toContinuousLinearMap)

Tactic:
simp [f.2]

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: 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 : f ≠ 0
this : Epi (Abelian.image.ι f)
⊢ Epi (Abelian.factorThruImage f ≫ Abelian.image.ι f)

Tactic:
exact epi_comp _ _

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
hσ : (Hom.hom (X.d 1)) ↑σ = ↑0
g : G
⊢ (X.ρ g) (↑σ 1) = ↑σ 1

Tactic:
rw [d_succ, hom_sub, hom_ofHom, ContIntertwiningMap.sub_apply, d_zero,
    ZeroMemClass.coe_zero, sub_eq_zero] at hσ

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
hσ : (X.resolutionX (0 + 1)).ρ.coind₁ι ↑σ = (Hom.hom ((coind₁Functor k G).map (ofHom X.ρ.coind₁ι))) ↑σ
g : G
⊢ (X.ρ g) (↑σ 1) = ↑σ 1
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
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : ind φ A ⟶ B
⊢ (fun f ↦
        ofHom
          {
            toLinearMap :=
              Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                (TensorProduct.lift
                  (((lift (↑A →ₗ[k] ↑B) k H) fun h ↦ B.ρ h⁻¹ ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ
                    ↑(MonoidAlgebra.coeffLinearEquiv k)))
                ⋯,
            isIntertwining' := ⋯ })
      ((fun f ↦ ofHom { toLinearMap := (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1, isIntertwining' := ⋯ }) f) =
    f

Tactic:
by
    ext h a
    simpa using (hom_comm_apply f h⁻¹ (IndV.mk φ A.ρ 1 a)).symm

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
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev i) i

Tactic:
rcases hi with ⟨j, rfl⟩; simp

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

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
⊢ (ComplexShape.down ℕ).Rel i ((ComplexShape.down ℕ).next i)

Tactic:
rcases hi with ⟨j, rfl⟩; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
S : ShortComplex (Rep R G)
hS : S.ShortExact
⊢ ∀ (i : ℤ), (S.map (tateComplexFunctor R G ⋙ HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) i)).ShortExact

Tactic:
rintro (_ | _)

Goal state after:
case ofNat
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
S : ShortComplex (Rep R G)
hS : S.ShortExact
a✝ : ℕ
⊢ (S.map (tateComplexFunctor R G ⋙ HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) (Int.ofNat a✝))).ShortExact

case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
S : ShortComplex (Rep R G)
hS : S.ShortExact
a✝ : ℕ
⊢ (S.map
      (tateComplexFunctor R G ⋙ HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) (Int.negSucc a✝))).ShortExact
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 : ℕ
⊢ cochainsMap₁ f φ ≫ (shortComplexH2 B).f = (shortComplexH2 A).f ≫ cochainsMap₂ f φ

Tactic:
ext x
    funext g
    simp [shortComplexH2, ← hom_comm_apply φ]

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 : ℕ
⊢ cochainsMap₂ f φ ≫ (shortComplexH2 B).g = (shortComplexH2 A).g ≫ cochainsMap₃ f φ

Tactic:
ext x
    funext g
    simp [shortComplexH2, ← hom_comm_apply φ]

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)
⊢ ∃ s, Hom.hom (η.hom.hom.app rightFDRep).hom = rightRegular s

Tactic:
classical
  obtain ⟨s, hs⟩ := ((evalAlgHom _ _ 1).comp (algHomOfRightFDRepComp η)).eq_piEvalAlgHom
  refine ⟨s, (basisFun k G).ext fun u ↦ ?_⟩
  simp only [rightFDRep, forget_obj]
  ext t
  have nat := η.hom.hom.naturality (leftRegularFDRepHom t⁻¹)
  calc
    _ = leftRegular t⁻¹ ((η.hom.hom.app rightFDRep).hom (single u 1)) 1 := by simp
    _ = (η.hom.hom.app rightFDRep).hom (leftRegular t⁻¹ (single u 1)) 1 :=
      congrFun congr(($nat.symm).hom (single u 1)) 1
    _ = evalAlgHom _ _ s (leftRegular t⁻¹ (single u 1)) :=
      congr($hs (leftRegular t⁻¹ (single u 1)))
    _ = _ := by by_cases u = t * s <;> simp_all

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
hn : ¬n = 0
⊢ Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯) ^ n =
    Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯)

Tactic:
simp [← restrictSupport_nsmul, ← degree_preimage_nsmul, hn, Set.Ici_nsmul_eq]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
h : r = 0
⊢ C r ∈ idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
h : ¬r = 0
⊢ C r ∈ idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0

Tactic:
· simp [h]

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
h : ¬r = 0
⊢ C r ∈ idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
⊢ p ∈ B → p ∈ m.leadingTerm ⁻¹' ↑(span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B))

Tactic:
hp

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ p ∈ m.leadingTerm ⁻¹' ↑(span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B))
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
⊢ p ∈ B → p ∈ (fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) ⁻¹' ↑(span (m.leadingTerm '' B))

Tactic:
hp

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ p ∈ (fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) ⁻¹' ↑(span (m.leadingTerm '' B))
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq τ
x : τ →₀ ℕ
⊢ {p | p.1 ∈ Finset.antidiagonal x ∧ p.2 ∈ ⋯.toFinset ×ˢ ⋯.toFinset}.Finite

Tactic:
apply Set.Finite.subset (s := ↑((Finset.antidiagonal x).sup (fun q ↦ Finset.product {q}
    ((TendstoCofinite.finite_preimage_singleton (Finsupp.mapDomain f) q.1).toFinset ×ˢ
      (TendstoCofinite.finite_preimage_singleton (Finsupp.mapDomain f) q.2).toFinset))))
  · exact Finset.finite_toSet ..
  · intro; simp
    grind

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 : σ ↪ τ
t : τ
h : t ∉ Set.range ⇑e
⊢ single t 1 ∉ Set.range (embDomain e)

Tactic:
mem_range_embDomain_iff,

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
t : τ
h : t ∉ Set.range ⇑e
⊢ ¬↑(single t 1).support ⊆ Set.range ⇑e
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 : ℕ), G n ∈ I
hG' : ∀ (n_1 : ℕ), G n_1 - ∑ i, C (T (G n_1) i) * F i = X * G (n_1 + 1)
H : Fin n → R⟦X⟧ := fun i ↦ mk fun n ↦ T (G n) i
h₁ : ∀ (n_1 : ℕ), g - ∑ i, ↑((trunc n_1) (H i)) * F i = X ^ n_1 * G n_1
h₂ : g = ∑ i, H i * F i
⊢ ∑ i, H i * F i ∈ Submodule.span R⟦X⟧ (Set.range F)

Tactic:
exact Ideal.sum_mem _ fun i _ ↦ Ideal.mul_mem_left _ _ (subset_span (Set.mem_range_self _))

Goal state after:
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
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
⊢ ∃ T, I = span T ∧ T.Finite ∧ T.ncard = S.ncard

Tactic:
obtain ⟨T, hTI, hinj, hT⟩ := this.exists_subset_injOn_image_eq

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
⊢ ∃ T, I = span T ∧ T.Finite ∧ T.ncard = S.ncard
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : ¬n = x none
⊢ 0 = (coeff y) 0

Tactic:
rw [coeff_zero]

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

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

Tactic:
rw [coeff_zero]

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

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

Tactic:
rw [coeff_zero]

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

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

Tactic:
rw [coeff_zero]

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
m' : ↥(maximalIdeal R)
hm' : (maximalIdeal R).toCotangent m' = m
this : (algebraMap R (AdicCompletion (maximalIdeal R) R)) ↑m' = (of (maximalIdeal R) R) ↑m'
hm : ↑m' ∈ maximalIdeal R ^ 2 * ⊤
⊢ m = 0

Tactic:
simpa [← hm', toCotangent_eq_zero] using hm

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I : ↥(Ideal A)⁰
⊢ (extendedHom A B) (mk0 I) = mk0 (extendedIdeal A B I)

Tactic:
by
  rw [mk0_eq_quotientMk, mk0_eq_quotientMk, extendedHom_quotientMk]
  congr; ext : 1
  exact FractionalIdeal.extendedHom_coeIdeal_eq_map (L := FractionRing B) (B := B) _

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.coeff n ∈ p.contentIdeal

pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ p.coeff n ∈ p.contentIdeal

Tactic:
· simp [h]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ p.coeff n ∈ p.contentIdeal
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: 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
x : Rˣ
hx : (powMonoidHom n) x = { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ (powMonoidHom n) ((Units.map ↑(algebraMap R K)) x) = (Units.map ↑(algebraMap R K)) ((powMonoidHom n) x)

Tactic:
by simp only [powMonoidHom_apply, RingHom.toMonoidHom_eq_coe, map_pow]

Goal state after: