mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case refine_2
Ω : 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✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ ∀ᵐ (x : Ω) ∂μ.restrict {x | σ x ≤ τ x}ᶜ,
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

Tactic:
suffices μ[stoppedValue f τ | (hσ.min hτ).measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}]
        μ[stoppedValue f τ | hσ.measurableSpace] by
      rw [ae_restrict_iff' (hσ.measurableSpace_le _ (hσ.measurableSet_le_stopping_time hτ).compl)]
      rw [Filter.EventuallyEq, ae_restrict_iff'] at this
      swap; · exact hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ)
      filter_upwards [this] with x hx hx_mem
      simp only [Set.mem_compl_iff, Set.mem_ofPred_eq, not_le] at hx_mem
      exact hx hx_mem.le
    apply Filter.EventuallyEq.trans _ ((condExp_min_stopping_time_ae_eq_restrict_le hτ hσ).trans _)
    · exact stoppedValue f τ
    · rw [IsStoppingTime.measurableSpace_min hσ hτ,
        IsStoppingTime.measurableSpace_min hτ hσ, inf_comm]
    · have h1 : μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ := by
        apply condExp_of_stronglyMeasurable hτ.measurableSpace_le
        · exact Measurable.stronglyMeasurable <|
            measurable_stoppedValue h.stronglyAdapted.isStronglyProgressive_of_discrete hτ
        · exact integrable_stoppedValue ι hτ h.integrable hτ_le
      rw [h1]
      exact (condExp_stoppedValue_stopping_time_ae_eq_restrict_le h hτ hσ hτ_le).symm

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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')

Tactic:
by
  have h_int (n : ℤ) : ∀ᵐ ω' ∂ν, Integrable (fun ω ↦ exp (n * X ω)) (κ ω') :=
    h.ae_integrable_exp_mul _
  rw [← ae_all_iff] at h_int
  filter_upwards [h_int] with ω' h_int t
  exact integrable_exp_mul_of_le_of_le (h_int _) (h_int _) (Int.floor_le t) (Int.le_ceil t)

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

Goal state before:
pp: case integrable_exp_mul
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
X : Ω → ℝ
c : ℝ≥0
⊢ ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑0 ∘ₘ ν)

Tactic:
simp [FunLike.coe_zero]

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 κ ν
ω' : Ω'
h2 : (κ ω') {ω | 0 < X ω} = 0
h1 : (κ ω') {ω | X ω < 0} = 0
⊢ (κ ω') {ω | X ω < 0} + (κ ω') {ω | 0 < X ω} = 0

Tactic:
simp [h1, h2]

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✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
ω : Ω
hω : liminf (fun x ↦ τ x ω) atTop = ⊤
⊢ Tendsto (fun x ↦ ⨅ j, ⨅ (_ : j ≥ x), τ j ω) atTop (𝓝 ⊤)

Tactic:
liminf_eq_iSup_iInf_of_nat

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁶ : ConditionallyCompleteLinearOrderBot ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
ω : Ω
hω : ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), τ i ω = ⊤
⊢ Tendsto (fun x ↦ ⨅ j, ⨅ (_ : j ≥ x), τ j ω) atTop (𝓝 ⊤)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos.inl
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
hX : HasSubgaussianMGF X c κ ν
t : ℝ
hκ : IsSFiniteKernel κ
inst✝ : IsZeroOrMarkovKernel 0
hY : HasSubgaussianMGF Y cY 0 (ν ⊗ₘ κ)
⊢ Integrable (fun ω ↦ rexp (t * (X ω.1 + Y ω.2))) (⇑(κ ⊗ₖ 0) ∘ₘ ν)

Tactic:
simp [FunLike.coe_zero]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∫ (x : ℝ) in 0..↑N, x + 1 ∂ρ = ∫ (x : ℝ) in 0..↑N, x ∂ρ + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ

Tactic:
by
        rw [intervalIntegral.integral_add]
        · exact continuous_id.intervalIntegrable _ _
        · exact continuous_const.intervalIntegrable _ _

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:

Tactic:
∑ j ∈ range K, ((j : ℝ) ^ 2)⁻¹ * Var[Y j] ≤
          ∑ j ∈ range K, ((j : ℝ) ^ 2)⁻¹ * 𝔼[truncation (X 0) j ^ 2] := by
        gcongr with j
        rw [(hident j).truncation.variance_eq]
        exact variance_le_expectation_sq (hX 0).truncation
      _ ≤ 2 * 𝔼[X 0] := sum_variance_truncation_le hint (hnonneg 0) K

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h : (∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ) → HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
h_indep' : X i ⟂ᵢ[μ] ∑ j ∈ s, X j
x✝ : Ω
⊢ ∑ c ∈ s, X c x✝ = (∑ j ∈ s, X j) x✝

Tactic:
rw [Finset.sum_apply]

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

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) cX μ
hY : HasSubgaussianMGF (fun ω ↦ Y ω - ∫ (x : Ω), Y x ∂μ) cY μ
hindep : X ⟂ᵢ[μ] Y
h_le : ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ
⊢ HasSubgaussianMGF (fun ω ↦ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)) (cX + cY) μ

Tactic:
rw [add_comm cX]

Goal state after:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) cX μ
hY : HasSubgaussianMGF (fun ω ↦ Y ω - ∫ (x : Ω), Y x ∂μ) cY μ
hindep : X ⟂ᵢ[μ] Y
h_le : ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ
⊢ HasSubgaussianMGF (fun ω ↦ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)) (cY + cX) μ
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case single
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 σ
v : ρ.asModule
g : G
a : A
⊢ f.toLinearMap (MonoidAlgebra.single g a • v) = (RingHom.id A[G]) (MonoidAlgebra.single g a) • f.toLinearMap v

Tactic:
simp [f.isIntertwining]; rfl

Goal state after:
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) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
n : ℕ
hn : X n ω ∉ Set.Ioi ↑n
npos : n ∈ Set.Ioi 0
⊢ 0 = truncation (X n) (↑n) ω - X n ω

Tactic:
simp only [truncation, indicator, Set.mem_Ioc, id, Function.comp_apply]

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
n : ℕ
hn : X n ω ∉ Set.Ioi ↑n
npos : n ∈ Set.Ioi 0
⊢ 0 = (if -↑n < X n ω ∧ X n ω ≤ ↑n then X n ω else 0) - X n ω
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
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ (fun n ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) = fun n ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i

Tactic:
ext n ω

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
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
n : ℕ
ω : Ω
⊢ (↑n)⁻¹ • ∑ i ∈ range n, X i ω = ((↑n)⁻¹ • ∑ i ∈ range n, X i) ω
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:
by
  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.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
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝² x✝¹ : S
x✝ : π₁ →ⁱL π₂
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
ext; simp [mul_smul]

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Group G
inst✝² : IsAlgClosed k
inst✝¹ : CharZero k
inst✝ : Fintype G
V : FDRep k G
this : Invertible ↑(Nat.card G)
⊢ Simple V ↔ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)

Tactic:
constructor <;> intro h

Goal state after:
case mp
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Group G
inst✝² : IsAlgClosed k
inst✝¹ : CharZero k
inst✝ : Fintype G
V : FDRep k G
this : Invertible ↑(Nat.card G)
h : Simple V
⊢ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)

case mpr
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Group G
inst✝² : IsAlgClosed k
inst✝¹ : CharZero k
inst✝ : Fintype G
V : FDRep k G
this : Invertible ↑(Nat.card G)
h : ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)
⊢ Simple V
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inl
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ : G
a : ↑A
s : ↥S
⊢ (B.indToCoindAux g₁) ((Hom.hom f) a) ((fun m ↦ m • g₁) s) = (Hom.hom f) ((A.indToCoindAux g₁) a ((fun m ↦ m • g₁) s))

Tactic:
simp [S.1.smul_def, hom_comm_apply]

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

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

Tactic:
groupCohomologyπOdd_eq_zero_iff,

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
x y : ↥(Hom.hom A.norm).ker
⊢ ↑(x - y) ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range ↔ ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: case h
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)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
H : ∀ (x : L), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x
hxinv : (Algebra.norm K) x⁻¹ = 1
y : Lˣ
hy : g ↑y = x⁻¹ * ↑y
⊢ ↑y / g ↑y = x

Tactic:
hy

Goal state after:
case h
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)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
H : ∀ (x : L), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x
hxinv : (Algebra.norm K) x⁻¹ = 1
y : Lˣ
hy : g ↑y = x⁻¹ * ↑y
⊢ ↑y / (x⁻¹ * ↑y) = x
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : ↑A
g : G
⊢ (A.ρ g) (r • x) - r • x = r • ((A.ρ g) x - x)

Tactic:
rw [map_smul, smul_sub]

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 B L) η = 0 / g 0
e : g (IsLocalization.mk' L a b) = 0
⊢ False

Tactic:
zero_div

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) η = 0
e : g (IsLocalization.mk' L a b) = 0
⊢ False
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 : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(LinearMap.ker A.ρ.norm)
⊢ (ConcreteCategory.hom (groupHomologyπEven A g hg i hi)) (x - y) = 0 ↔ ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range

Tactic:
groupHomologyπEven_eq_zero_iff,

Goal state after:
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 : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(LinearMap.ker A.ρ.norm)
⊢ ↑(x - y) ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range ↔ ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝³ : CommRing R
inst✝² : Group G
inst✝¹ : Fintype G
M : Rep R G
X✝ : Rep R G
Y✝ : Rep R G
m : ℤ
n : ℕ
hmn : m = -(↑n + 1)
inst✝ : NeZero n
X Y : Rep R G
f : X ⟶ Y
⊢ (tateCohomologyFunctor m).map f ≫ ((tateComplexConnectData Y).homologyIsoNeg n m hmn).hom =
    ((tateComplexConnectData X).homologyIsoNeg n m hmn).hom ≫ (groupHomology.functor R G n).map f

Tactic:
by
    simp [tateCohomologyFunctor,
      CochainComplex.ConnectData.homologyMap_map_of_eq_neg_succ (hmn := hmn)]

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 : σ ↪ τ
⊢ Function.Injective ⇑(rename ⇑e)

Tactic:
by
  intro _ _ h; ext x
  simpa using MvPowerSeries.ext_iff.mp h (embDomain e x)

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
⊢ single (1, g * h) a - single (1, g) a ∈ boundaries₂ A

Tactic:
use single (1, g, h) a

Goal state after:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g h : G
a : ↑A
⊢ (ModuleCat.Hom.hom (d₃₂ A)) (single (1, g, h) a) = single (1, g * h) a - single (1, g) a
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 : ℕ
x : Fin n → G
a : ↑A
⊢ (ConcreteCategory.hom ((chainsMap f φ).f n)) (single x a) = single (⇑f ∘ x) ((Hom.hom φ) a)

Tactic:
by
  simp [chainsMap_f]

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
⊢ Submodule.spanFinrank (maximalIdeal (AdicCompletion (maximalIdeal R) R)) = Submodule.spanFinrank (maximalIdeal R)

Tactic:
have fg : (maximalIdeal R).FG := fg_of_isNoetherianRing (maximalIdeal R)
  have comapeq := IsLocalRing.maximalIdeal_comap (algebraMap R (AdicCompletion (maximalIdeal R) R))
  let f := Ideal.mapCotangent _ _ (Algebra.ofId R (AdicCompletion (maximalIdeal R) R))
    (le_of_eq comapeq.symm)
  have inj : Function.Injective f := by
    rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
    intro m hm
    rcases Ideal.toCotangent_surjective _ m with ⟨m', hm'⟩
    simp only [← hm', mapCotangent_toCotangent, Algebra.ofId_apply, toCotangent_eq_zero,
      maximalIdeal_eq_map, ← Ideal.map_pow, f] at hm
    rw [← Submodule.restrictScalars_mem R, ← Ideal.smul_top_eq_map,
      pow_smul_top_eq_ker_eval fg] at hm
    have : (algebraMap R (AdicCompletion (maximalIdeal R) R)) m'.1 = of _ R m'.1 := rfl
    simp only [smul_eq_mul, eval, this, LinearMap.mem_ker, LinearMap.coe_mk, AddHom.coe_mk,
      of_apply, Submodule.mkQ_apply, mk_eq_mk, Ideal.Quotient.eq_zero_iff_mem] at hm
    simpa [← hm', toCotangent_eq_zero] using hm
  have surj : Function.Surjective f := by
    intro m
    rcases Ideal.toCotangent_surjective _ m with ⟨m', hm'⟩
    rcases Submodule.Quotient.mk_surjective _ (m'.1.1 2) with ⟨l, hl⟩
    have lmem : (transitionMap _ R (Nat.le_succ 1)) (m'.1.1 2) = m'.1.1 1 := m'.1.2 (Nat.le_succ 1)
    simp only [smul_eq_mul, Nat.succ_eq_add_one, Nat.reduceAdd, transitionMap, Submodule.factorPow,
      Submodule.mapQ_eq_factor, Submodule.factor_eq_factor, ← hl, mk_eq_mk, factor_mk, pow_one,
      (mem_maximalIdeal_iff_eval_one_eq_zero m'.1).mp m'.2, eq_zero_iff_mem, mul_top] at lmem
    use (maximalIdeal R).toCotangent ⟨l, lmem⟩
    simp only [mapCotangent_toCotangent, Algebra.ofId_apply, ← hm', toCotangent_eq, f]
    change (of (maximalIdeal R) R l) - m' ∈ _
    simp only [maximalIdeal_eq_map, ← Ideal.map_pow]
    rw [← Submodule.restrictScalars_mem R, ← Ideal.smul_top_eq_map]
    simpa [pow_smul_top_eq_ker_eval (maximalIdeal R).fg_of_isNoetherianRing, eval, sub_eq_zero]
      using hl
  have rkeq := rank_eq_of_equiv_equiv _
    (LinearEquiv.ofBijective f ⟨inj, surj⟩).toAddEquiv
    (residueField_map_bijective R) (fun r m ↦ by
      rcases IsLocalRing.residue_surjective r with ⟨s, rfl⟩
      exact map_smul f s m )
  have fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG := by
    simpa [AdicCompletion.maximalIdeal_eq_map] using fg.map _
  rw [IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg fg,
    IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg fg', eq_comm]
  simp [Module.finrank, CotangentSpace, rkeq]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
n : ℕ
hn : maximalIdeal A ^ n = 0
m : ℕ
h : m ≤ n
⊢ f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]

Tactic:
exact hf h

Goal state after: