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

Goal state before:
pp: case refine_2
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g₁ g₂ : X → ℝ≥0∞
a✝ : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂π x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂π x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ ∫⁻ (a : X), g₁ a * f a ∂π x₀ + ∫⁻ (a : X), g₂ a * f a ∂π x₀ =
    g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀ + g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀

pp: case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g₁ g₂ : X → ℝ≥0∞
a✝ : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂π x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂π x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ Measurable fun x ↦ g₂ x * f x

Tactic:
hg₁,

Goal state after:
case refine_2
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g₁ g₂ : X → ℝ≥0∞
a✝ : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂π x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂π x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀ + ∫⁻ (a : X), g₂ a * f a ∂π x₀ =
    g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀ + g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀

case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g₁ g₂ : X → ℝ≥0∞
a✝ : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂π x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂π x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ Measurable fun x ↦ g₂ x * f x
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g₁ g₂ : X → ℝ≥0∞
a✝ : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂π x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂π x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ Measurable fun x ↦ g₂ x * f x

Tactic:
· exact (hg₂_meas.mono h𝓑𝓧 le_rfl).mul hf

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
n : ℕ
i : Fin (n + 1)
⊢ (binomial p h n) i = ↑p ^ ↑i * (1 - ↑p) ^ (↑(Fin.last n) - ↑i) * ↑(n.choose ↑i)

Tactic:
by
  simp [binomial]

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

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
⊢ g ⟂ᵢ[k, hk; μ] f ↔
    ⇑(condDistrib f (fun ω ↦ (k ω, g ω)) μ) =ᵐ[Measure.map (fun ω ↦ (k ω, g ω)) μ]
      ⇑(Kernel.prodMkRight β' (condDistrib f k μ))

Tactic:
by
  rw [condDistrib_ae_eq_iff_measure_eq_compProd (μ := μ) _ hf.aemeasurable,
    condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib hg hf hk,
    Measure.compProd_eq_comp_prod]
  let e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
  have h_eq : ((Kernel.id ×ₖ condDistrib g k μ) ×ₖ condDistrib f k μ) ∘ₘ μ.map k =
      (Kernel.id ×ₖ (condDistrib f k μ).prodMkRight _) ∘ₘ μ.map (fun a ↦ (k a, g a)) := by
    calc ((Kernel.id ×ₖ condDistrib g k μ) ×ₖ condDistrib f k μ) ∘ₘ μ.map k
    _ = (Kernel.id ×ₖ (condDistrib f k μ).prodMkRight _) ∘ₘ (μ.map k ⊗ₘ condDistrib g k μ) := by
      rw [Measure.compProd_eq_comp_prod, Measure.comp_assoc]
      congr 2
      have h := Kernel.prod_prodMkRight_comp_deterministic_prod (condDistrib g k μ)
        (condDistrib f k μ) Kernel.id measurable_id
      rw [← Kernel.id] at h
      simpa using h.symm
    _ = (Kernel.id ×ₖ (condDistrib f k μ).prodMkRight _) ∘ₘ μ.map (fun a ↦ (k a, g a)) := by
      rw [compProd_map_condDistrib hg.aemeasurable]
  rw [← h_eq]
  have h1 : μ.map (fun x ↦ ((k x, g x), f x)) = (μ.map (fun a ↦ (k a, g a, f a))).map e := by
    rw [Measure.map_map (by fun_prop) (by fun_prop)]
    rfl
  have h1_symm : μ.map (fun a ↦ (k a, g a, f a)) =
      (μ.map (fun x ↦ ((k x, g x), f x))).map e.symm := by
    rw [h1, Measure.map_map (by fun_prop) (by fun_prop), MeasurableEquiv.symm_comp_self,
      Measure.map_id]
  have h2 : ((Kernel.id ×ₖ condDistrib g k μ) ×ₖ condDistrib f k μ) ∘ₘ μ.map k =
      ((Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ μ.map k).map e := by
    rw [← Measure.deterministic_comp_eq_map e.measurable, Measure.comp_assoc]
    congr 2
    unfold e
    rw [Kernel.deterministic_comp_eq_map, Kernel.prodAssoc_symm_prod]
  have h2_symm : (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ μ.map k =
      (((Kernel.id ×ₖ condDistrib g k μ) ×ₖ condDistrib f k μ) ∘ₘ μ.map k).map e.symm := by
    rw [h2, Measure.map_map (by fun_prop) (by fun_prop), MeasurableEquiv.symm_comp_self,
      Measure.map_id]
  rw [h1, h2]
  exact ⟨fun h ↦ by rw [h], fun h ↦ by rw [h1_symm, h1, h2_symm, h2, h]⟩

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

Goal state before:
pp: case pos.mgf_le
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
h2 : ∀ᵐ (ω' : Ω) ∂Measure.map Prod.snd (ν ⊗ₘ κ), ∀ (t : ℝ), mgf Y (η ω') t ≤ rexp (↑cY * t ^ 2 / 2)
⊢ ∀ᵐ (ω' : Ω' × Ω) ∂ν ⊗ₘ κ, ∀ (t : ℝ), mgf Y ((prodMkLeft Ω' η) ω') t ≤ rexp (↑cY * t ^ 2 / 2)

Tactic:
exact ae_of_ae_map (by fun_prop) h2

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h
Ω : 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 ρ
i : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
x : ℝ
hx : ↑i < x ∧ x ≤ ↑i + 1
⊢ (↑i + 1) * 1 ≤ x + 1

Tactic:
simp [hx.1.le]

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S✝ : Subgroup G
inst✝¹ : S✝.Normal
S : Subgroup G
inst✝ : S.Normal
X Y : Rep k G
f : X ⟶ Y
g✝ : G ⧸ S
g : G
⊢ ModuleCat.Hom.hom ((invariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)) ∘ₗ (X.ρ.quotientToInvariants S) ↑g =
    (Y.ρ.quotientToInvariants S) ↑g ∘ₗ ModuleCat.Hom.hom ((invariantsFunctor k ↥S).map ((resFunctor S.subtype).map f))

Tactic:
by ext; simp [hom_comm_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
f : σ.IntertwiningMap ρ
x : H → A
h : ∀ (g : G) (h : H), x (φ g * h) = (σ g) (x h)
⊢ ∀ (g : G) (h : H), f (x (φ g * h)) = (ρ g) (f (x h))

Tactic:
intro g h0

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
f : σ.IntertwiningMap ρ
x : H → A
h : ∀ (g : G) (h : H), x (φ g * h) = (σ g) (x h)
g : G
h0 : H
⊢ f (x (φ g * h0)) = (ρ g) (f (x h0))
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
f : res φ (leftRegular k H) ⟶ A
g : G
h : H
⊢ ?m.240

Tactic:
simpa using (hom_comm_apply f g (.single h 1)).symm

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
x✝² : ↑B
x✝¹ : G
x✝ : H
⊢ (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) x✝² (φ x✝¹ * x✝) =
    (A.ρ x✝¹) ((LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) x✝² x✝)

Tactic:
simpa using hom_comm_apply f _ _

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Monoid G✝
A B : Rep k✝ G✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X Y : Rep k G
f : X ⟶ Y
g✝ : G ⧸ S
g : G
⊢ ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)) ∘ₗ
      ((X.toCoinvariants S).ρ.ofQuotient S) ↑g =
    ((Y.toCoinvariants S).ρ.ofQuotient S) ↑g ∘ₗ
      ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f))

Tactic:
by ext; simp [hom_comm_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: 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)
eq : (↑(Nat.card G))⁻¹ * ∑ g, V.character g * V.character g⁻¹ = ↑(Module.finrank k (V ⟶ V))
⊢ Simple V

Tactic:
rw [h, inv_mul_cancel_of_invertible] at eq

Goal state after:
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)
eq : 1 = ↑(Module.finrank k (V ⟶ V))
⊢ Simple V
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: 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

Tactic:
· have eq := V.scalar_product_char_eq_finrank_equivariant V
    rw [h, inv_mul_cancel_of_invertible] at eq
    rw [simple_iff_end_is_rank_one, ← Nat.cast_inj (R := k), ← eq, Nat.cast_one]

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
⊢ Simple V ↔ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)

Tactic:
have := invertibleOfNonzero (NeZero.ne (Nat.card G : k))
  constructor <;> intro h
  · symm; simpa [Nonempty.intro (Iso.refl V), inv_mul_eq_one₀] using char_orthonormal V V
  · have eq := V.scalar_product_char_eq_finrank_equivariant V
    rw [h, inv_mul_cancel_of_invertible] at eq
    rw [simple_iff_end_is_rank_one, ← Nat.cast_inj (R := k), ← eq, Nat.cast_one]

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σ : (X.resolutionX (0 + 1)).ρ.coind₁ι ↑σ = (Hom.hom ((coind₁Functor k G).map (ofHom X.ρ.coind₁ι))) ↑σ
g : G
⊢ (X.ρ g) (↑σ 1) = ↑σ 1

Tactic:
replace hσ := DFunLike.ext_iff.1 (DFunLike.ext_iff.1 hσ 1) g⁻¹

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
g : G
hσ :
  (((X.resolutionX (0 + 1)).ρ.coind₁ι ↑σ) 1) g⁻¹ = (((Hom.hom ((coind₁Functor k G).map (ofHom X.ρ.coind₁ι))) ↑σ) 1) g⁻¹
⊢ (X.ρ g) (↑σ 1) = ↑σ 1
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
i j : ℕ
y : (Fin i → G) →₀ ↑X.X₂
x : (Fin j → G) →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom ((inhomogeneousChains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom ((inhomogeneousChains X.X₁).d j ((ComplexShape.down ℕ).next j))) x = 0

Tactic:
simpa using! (map_chainsFunctor_shortExact hX).d_eq_zero_of_f_eq_d_apply i j y x
      (by simpa using! hx) _

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
⊢ map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1 ≫ map S.subtype (𝟙 (res S.subtype A)) 1 = 0

Tactic:
rw [← map_comp, Category.comp_id, congr (QuotientGroup.mk'_comp_subtype S)
    (fun f φ => map f φ 1), map₁_one]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ p ∈ idealOfVars σ R ^ n ↔ ∀ (x : σ →₀ ℕ), degree x < n → coeff x p = 0

Tactic:
grind only [mem_pow_idealOfVars_iff, mem_support_iff]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝² : TendstoCofinite f
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
x : τ →₀ ℕ
fst✝¹ fst✝ snd✝ : σ →₀ ℕ
⊢ fst✝ + snd✝ = fst✝¹ → (mapDomain f fst✝ + mapDomain f snd✝ = x ↔ mapDomain f fst✝¹ = x)

Tactic:
grind [Finsupp.mapDomain_add]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
⊢ IsHausdorff I R ∧ IsPrecomplete I R ↔ CompleteSpace R ∧ T2Space R

Tactic:
hI.isHausdorff_iff,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
⊢ T2Space R ∧ IsPrecomplete I R ↔ CompleteSpace R ∧ T2Space R
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
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n))
      ((truncTotal n) ((algebraMap (MvPolynomial σ R) (MvPowerSeries σ R)) p)) =
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n)) p

Tactic:
by
    change (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) (truncTotal n p) =
      (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) p
    rw [Ideal.Quotient.eq, MvPolynomial.mem_pow_idealOfVars_iff']
    intro x h
    rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ h, MvPolynomial.coeff_coe]

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

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

Tactic:
refine ShortComplex.hom_ext _ _ ?_ ?_ rfl
  all_goals
  { simp only [shortComplexH1]
    ext
    simp [Prod.map]}

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Pi

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : CommSemiring T
inst✝¹ : Algebra R S
inst✝ : Algebra S T
x✝¹ : R[X]
x✝ : S → T
z : S
⊢ (x✝¹ • x✝) z =
    ({ toFun := fun p z ↦ (algebraMap S T) ((aeval z) p), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
          x✝¹ *
        x✝)
      z

Tactic:
by
    simp only [polynomial_smul_apply', Algebra.algebraMap_eq_smul_one, RingHom.coe_mk,
      MonoidHom.coe_mk, OneHom.coe_mk, Pi.mul_apply, Algebra.smul_mul_assoc, one_mul]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
r : R
⊢ IsGroupLikeElem R r ↔ r = 1

Tactic:
simp +contextual [isGroupLikeElem_iff]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
g : G
r : R
⊢ single ((mapDomainOfBialgHom f) g) r = f (single g r)

Tactic:
by
  rw [← mul_one r, ← smul_eq_mul, ← smul_single, ← smul_single, map_smul]
  exact congr(r • $(single_mapDomainOfBialgHomFun_one f g))

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
⊢ IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s)

Tactic:
← hSR'.mk'_mul,

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
⊢ IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r * 1) (1 * (t * s))
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
p : MvPolynomial (ℕ × M) R
⊢ (lift hI g hg) ↑p = (aeval fun nm ↦ hI.dpow nm.1 (g nm.2)) p

Tactic:
rw [lift, lift'_apply]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
⊢ hI.IsSubDPIdeal (I ⊓ ⨅ i, J i)

Tactic:
by
  cases isEmpty_or_nonempty ι with
  | inr _ =>
    refine ⟨fun _ hx ↦ hx.1, ?_⟩
    intro n hn x hx
    simp only [Ideal.mem_inf, mem_iInf] at hx ⊢
    exact ⟨hI.dpow_mem hn hx.1, fun i ↦  IsSubDPIdeal.dpow_mem (hJ i) n hn (hx.2 i)⟩
  | inl _ =>
    simp only [iInf_of_empty, le_top, inf_of_le_left]
    exact IsSubDPIdeal.self hI

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit R S
⊢ Etale R S

Tactic:
by
  obtain ⟨n, ⟨e⟩⟩ := nonempty_algEquiv_fun R S
  exact .of_equiv e.symm

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case refine_3
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
x y : A
hx : x ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy : y ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hx_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
n : ℕ
hn : n ≠ 0
⊢ ∑ k ∈ Finset.range (n + 1), hI.dpow k x * hI.dpow (n - k) y ∈
    span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
apply Submodule.sum_mem (span _)

Goal state after:
case refine_3
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := ⋯
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
x y : A
hx : x ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy : y ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hx_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
n : ℕ
hn : n ≠ 0
⊢ ∀ c ∈ Finset.range (n + 1),
    hI.dpow c x * hI.dpow (n - c) y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a x : A
hx : x ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
⊢ a • x ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}

Tactic:
rw [smul_eq_mul]
    exact ⟨I.mul_mem_left a hx.1, (fun n ↦ by rw [hI.dpow_mul hx.1, hI'.dpow_mul hx.1, hx.2])⟩

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
a : A
ha : a ∈ ↑I
n : ℕ
⊢ hK.dpow n (f a) = hK'.dpow n (f a)

Tactic:
by rw [hIK.2 a ha, hIK'.2 a ha]

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this✝ : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : (∑ i_1 ∈ Finset.range k, (ζ ^ (q + k - i)) ^ i_1) * (ζ ^ (q + k - i) - 1) = 0
⊢ φ ζ = ζ ^ q

Tactic:
mul_eq_zero,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this✝ : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ∑ i_1 ∈ Finset.range k, (ζ ^ (q + k - i)) ^ i_1 = 0 ∨ ζ ^ (q + k - i) - 1 = 0
⊢ φ ζ = ζ ^ q
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
n : ℕ
⊢ (coeff n) ((1 - X) * mk 1) = (coeff n) 1

Tactic:
cases n with

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Binomial

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
d n : ℕ
⊢ ↑(↑n).negOnePow • (coeff n) ↑(invOneSubPow A d) = Ring.choose (-↑d) n • 1

Tactic:
cases d with

Goal state after: