mathlib-initiative/mathlib-tactics huggingface dataset:
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 ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
B : ∀ (a b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
⊢ ∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc ↑j ↑N, 1 ∂ρ = ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ

Tactic:
refine sum_congr rfl fun j hj => ?_

Goal state after:
Ω : 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 ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
B : ∀ (a b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
j : ℕ
hj : j ∈ range K
⊢ ∫ (x : ℝ) in Set.Ioc ↑j ↑N, 1 ∂ρ = ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
⊢ {ω | X ω ∈ Set.Ioi ↑i} ⊆ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}

Tactic:
intro ω hω

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
ω : Ω
hω : ω ∈ {ω | X ω ∈ Set.Ioi ↑i}
⊢ ω ∈ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
xy : (X ⊗ Y).V
⊢ (δ X Y) (MonoidAlgebra.single xy 1) = MonoidAlgebra.single xy.1 1 ⊗ₜ[k] MonoidAlgebra.single xy.2 1

Tactic:
by
  simp [δ, MonoidAlgebra.tensorEquiv_symm_single_eq_single_one_tmul]

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 : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
x✝ : k < K
⊢ IntervalIntegrable (HMul.hMul 2) ρ ↑k ↑(k + 1)

Tactic:
exact (continuous_const.mul continuous_id').intervalIntegrable _ _

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

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

Tactic:
exact congrFun h x

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : V
hx : (ρ g) x = x
γ : G
⊢ (ρ γ) x = x

Tactic:
rcases hg γ with ⟨i, rfl⟩

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : V
hx : (ρ g) x = x
i : ℤ
⊢ (ρ ((fun x ↦ g ^ x) i)) x = x
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: case mpr
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
⊢ f ∘ₗ X.ρ (g * g⁻¹) = f

Tactic:
mul_inv_cancel,

Goal state after:
case mpr
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
⊢ f ∘ₗ X.ρ 1 = f
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✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
α : Type u
inst✝ : DecidableEq α
a : ↑A
i : α
g : G
r : k
⊢ ((((TensorProduct.mk k ↑A ↑(free k G α)).compr₂ₛₗ
              ((A.finsuppToCoinvariantsTensorFree α ∘ₗ A.coinvariantsTensorFreeToFinsupp α) ∘ₗ
                Coinvariants.mk (A ⊗ free k G α).ρ))
            a ∘ₗ
          lsingle i) ∘ₗ
        MonoidAlgebra.lsingle g)
      r =
    ((((TensorProduct.mk k ↑A ↑(free k G α)).compr₂ₛₗ (LinearMap.id ∘ₗ Coinvariants.mk (A ⊗ free k G α).ρ)) a ∘ₗ
          lsingle i) ∘ₗ
        MonoidAlgebra.lsingle g)
      r

Tactic:
by
        simp [coinvariantsTensorFreeToFinsupp_mk_tmul_single _,
          finsuppToCoinvariantsTensorFree_single (A := A) i, TensorProduct.smul_tmul]

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

Goal state before:
pp: case refine_1
k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
g : G
y : MonoidAlgebra k G
⊢ (fun gv ↦ ((leftRegular k G) gv.1) gv.2 - gv.2) (g, y) ∈
    ↑((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker

Tactic:
simpa [linearCombination, sub_eq_zero, sum_fintype]
      using Finset.sum_bijective _ (Group.mulLeft_bijective g⁻¹) (by simp) (by lia)

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

Goal state before:
pp: 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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) g) ε = ε

Tactic:
by
  have : Module.IsTorsionFree A L := by
    rw [Module.isTorsionFree_iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K L]
    exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
  have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L :=
    IsIntegralClosure.isLocalization A K L B
  let η' : Lˣ := Units.mk0 (algebraMap B L η) (fun h ↦ by simp [h] at hη)
  obtain ⟨ε, hε⟩ := exists_div_of_norm_eq_one hg hη
  obtain ⟨a, b, h⟩ := IsLocalization.exists_mk'_eq (Algebra.algebraMapSubmonoid B A⁰) ε.1
  obtain ⟨t, ht, ht'⟩ := b.prop
  have : t • IsLocalization.mk' L a b = algebraMap _ _ a := by
    rw [Algebra.smul_def, IsScalarTower.algebraMap_apply A B L, ht', IsLocalization.mk'_spec']
  refine ⟨a, ?_, ?_⟩
  · rintro rfl
    simp only [IsLocalization.mk'_zero, _root_.map_zero, div_zero, ← h] at hε
    rw [← hε, Algebra.norm_zero] at hη
    exact zero_ne_one hη
  · replace hε := hε.symm
    rw [← h, eq_div_iff_mul_eq] at hε
    · replace hε := congr_arg (t • ·) hε
      rw [Algebra.smul_def, mul_left_comm, ← Algebra.smul_def t, ← g.toAlgHom_apply,
        ← AlgHom.map_smul_of_tower, this] at hε
      apply IsIntegralClosure.algebraMap_injective B A L
      rw [map_mul, ← hε]
      congr 1
      exact algebraMap_galRestrictHom_apply A K L B g a
    · intro e
      rw [(map_eq_zero _).mp e, zero_div] at hε
      rw [hε, Algebra.norm_zero] at hη
      exact zero_ne_one hη

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : Monoid G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
⊢ f (g, 1) = g • f (1, 1)

Tactic:
by
  simpa only [mul_one, mul_left_inj] using hf g 1 1

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
M : Rep R G
X : Rep R G
Y : Rep R G
X✝ Y✝ Z✝ : Rep R G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ tateComplex.map (f ≫ g) = tateComplex.map f ≫ tateComplex.map g

Tactic:
by
    simp [tateComplex.map, CochainComplex.ConnectData.map_comp_map, ← chainsMap_comp]
    rfl

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

Goal state before:
pp: case h.refine_3.H
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
h : G ⧸ S
g : G
⊢ 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 h using QuotientGroup.induction_on with

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

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

Tactic:
apply_fun (fun x ↦ (x.hom.hom.app rightFDRep).hom (single t 1) 1) at h

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Nontrivial k
s t : G
h :
  (ConcreteCategory.hom (((equivHom k G) s).hom.hom.app rightFDRep).hom) (single t 1) 1 =
    (ConcreteCategory.hom (((equivHom k G) t).hom.hom.app rightFDRep).hom) (single t 1) 1
⊢ s = t
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
⊢ Ideal.Quotient.mkₐ A I = aeval fun d ↦ (Ideal.Quotient.mk I) (X d)

Tactic:
ext d

Goal state after:
A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
d : σ
⊢ (Ideal.Quotient.mkₐ A I) (X d) = (aeval fun d ↦ (Ideal.Quotient.mk I) (X d)) (X d)
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
⊢ (↑↑(Ideal.Quotient.mk I)).toFun = eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) fun d ↦ (Ideal.Quotient.mk I) (X d)

Tactic:
ext d

Goal state after:
A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
d : MvPolynomial σ A
⊢ (↑↑(Ideal.Quotient.mk I)).toFun d =
    eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) (fun d ↦ (Ideal.Quotient.mk I) (X d)) d
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (isoCycles₂ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.i = iCycles A 2 ≫ (chainsIso₂ A).hom

Tactic:
simp [isoCycles₂, iCycles, HomologicalComplex.iCycles, ShortComplex.iCycles]

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
J : Ideal R⟦X⟧
hJI : J ≤ I
hXI : X ∉ I
hJ : J.FG
h' : Ideal.map constantCoeff I ≤ Ideal.map constantCoeff J
⊢ I = J

Tactic:
by
  refine hJI.antisymm' ?_
  replace h' := h'.antisymm (Ideal.map_mono hJI)
  obtain ⟨n, F, rfl⟩ := Submodule.fg_iff_exists_fin_generating_family.mp hJ
  rw [submodule_span_eq, map_span, ← Set.range_comp] at h'
  choose! T hT using fun g (hg : g ∈ I) ↦
    mem_span_range_iff_exists_fun.mp (h'.le (Ideal.mem_map_of_mem _ hg))
  dsimp at hT
  intro g hg
  let G : ℕ → R⟦X⟧ :=
    Nat.rec g fun _ G' ↦ mk fun p ↦ coeff (p + 1) G' - ∑ i, T G' i * coeff (p + 1) (F i)
  have hG' (n : ℕ) (H : G n ∈ I) : G n - ∑ i, C (T (G n) i) * F i = X * G (n + 1) := by
    simpa [hT _ H] using sub_const_eq_X_mul_shift (G n - ∑ i, C (T (G n) i) * F i)
  have hG : ∀ n, G n ∈ I := Nat.rec hg fun n IH ↦
    (‹I.IsPrime›.mul_mem_iff_mem_or_mem.mp (hG' n IH ▸ I.sub_mem IH (I.sum_mem fun i _ ↦
      I.mul_mem_left _ (hJI (subset_span (Set.mem_range_self _)))))).resolve_left hXI
  replace hG' := fun n ↦ hG' n (hG n)
  let H (i : Fin n) : R⟦X⟧ := mk fun n ↦ T (G n) i
  have h₁ (n : ℕ) : g - ∑ i, trunc n (H i) * F i = X ^ n * G n := by
    induction n with
    | zero => simp [G]
    | succ n IH =>
      simp [trunc_succ, add_mul, sum_add_distrib, ← sub_sub, IH, pow_succ, mul_assoc, ← hG',
        mul_sub, H, mul_sum, monomial_eq_C_mul_X_pow, mul_left_comm (C _)]
  have h₂ : g = ∑ i, H i * F i := by
    ext n; simpa [coeff_trunc, sub_eq_zero] using congr(($(h₁ (n + 1)).trunc (n + 1)).coeff n)
  rw [h₂]
  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: case refine_3
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
f : R⟦X⟧
hf : constantCoeff f ∈ span S
⊢ ∀ (a x : R),
    x ∈ Submodule.span R S → (∃ x_1 ∈ span T, constantCoeff x_1 = x) → ∃ x_1 ∈ span T, constantCoeff x_1 = a • x

Tactic:
intro r₁ r₂ hr₁ ⟨f, hfmem, hf⟩
    exact ⟨r₁ • f, Submodule.smul_of_tower_mem _ _ hfmem, by simp [hf]⟩

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

Goal state before:
pp: case refine_3
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
f : R⟦X⟧
hf : constantCoeff f ∈ span S
⊢ ∀ (a x : R),
    x ∈ Submodule.span R S → (∃ x_1 ∈ span T, constantCoeff x_1 = x) → ∃ x_1 ∈ span T, constantCoeff x_1 = a • x

Tactic:
· intro r₁ r₂ hr₁ ⟨f, hfmem, hf⟩
    exact ⟨r₁ • f, Submodule.smul_of_tower_mem _ _ hfmem, by simp [hf]⟩

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

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ a₁ ∈ antidiagonal (optionElim k x),
    ∀ a₂ ∈ antidiagonal (optionElim k x),
      ⟨(a₁.1 none, a₁.2 none), (a₁.1.some, a₁.2.some)⟩ = ⟨(a₂.1 none, a₂.2 none), (a₂.1.some, a₂.2.some)⟩ → a₁ = a₂

pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ b ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x,
    ∃ a, ∃ (_ : a ∈ antidiagonal (optionElim k x)), ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩ = b

pp: case refine_4
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ a ∈ antidiagonal (optionElim k x),
    (coeff a.1) p * (coeff a.2) q =
      (coeff
            (optionElim ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.fst.1
              ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.snd.1))
          p *
        (coeff
            (optionElim ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.fst.2
              ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.snd.2))
          q

Tactic:
· intros; ext t <;> cases t
    all_goals simp_all [Finsupp.ext_iff]

Goal state after:
case refine_3
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ b ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x,
    ∃ a, ∃ (_ : a ∈ antidiagonal (optionElim k x)), ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩ = b

case refine_4
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ a ∈ antidiagonal (optionElim k x),
    (coeff a.1) p * (coeff a.2) q =
      (coeff
            (optionElim ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.fst.1
              ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.snd.1))
          p *
        (coeff
            (optionElim ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.fst.2
              ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.snd.2))
          q
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
n : ℕ
i : M
x : Fin n →₀ M
⊢ embDomain (finSuccEquiv n).toEmbedding (Finsupp.cons i x) = optionElim i x

Tactic:
by
  ext a; cases a <;> simp [embDomain_eq_mapDomain]

Goal state after:
Module: Mathlib.RingTheory.Flat.Domain

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁴ : AddCommGroup P
inst✝³ : Module R P
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst✝ : Module.Flat R Q
hf : Injective ⇑f
hg : Injective ⇑g
K : Type u_1 := FractionRing R
H₁ : Injective ⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g))
H₂ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm
H₃ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N)
H₄ : Injective ⇑(AlgebraTensorModule.assoc R R K K P Q).symm
H₅ : Injective ⇑(AlgebraTensorModule.assoc R R K K M N)
H₆ : Injective ⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K))
H₇ : Injective ⇑(TensorProduct.lid R (P ⊗[R] Q)).symm
⊢ (mk R K (M ⊗[R] N)) 1 ∘ₗ map f g =
    ↑R ↑(AlgebraTensorModule.assoc R R K K M N) ∘ₗ
      ↑R ↑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N) ∘ₗ
        ↑R (map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) ∘ₗ
          ↑R ↑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm ∘ₗ
            ↑R ↑(AlgebraTensorModule.assoc R R K K P Q).symm ∘ₗ
              LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K) ∘ₗ ↑(TensorProduct.lid R (P ⊗[R] Q)).symm

Tactic:
ext p q

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁴ : AddCommGroup P
inst✝³ : Module R P
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst✝ : Module.Flat R Q
hf : Injective ⇑f
hg : Injective ⇑g
K : Type u_1 := FractionRing R
H₁ : Injective ⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g))
H₂ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm
H₃ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N)
H₄ : Injective ⇑(AlgebraTensorModule.assoc R R K K P Q).symm
H₅ : Injective ⇑(AlgebraTensorModule.assoc R R K K M N)
H₆ : Injective ⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K))
H₇ : Injective ⇑(TensorProduct.lid R (P ⊗[R] Q)).symm
p : P
q : Q
⊢ ((AlgebraTensorModule.curry ((mk R K (M ⊗[R] N)) 1 ∘ₗ map f g)) p) q =
    ((AlgebraTensorModule.curry
          (↑R ↑(AlgebraTensorModule.assoc R R K K M N) ∘ₗ
            ↑R ↑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N) ∘ₗ
              ↑R (map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) ∘ₗ
                ↑R ↑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm ∘ₗ
                  ↑R ↑(AlgebraTensorModule.assoc R R K K P Q).symm ∘ₗ
                    LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K) ∘ₗ ↑(TensorProduct.lid R (P ⊗[R] Q)).symm))
        p)
      q
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↑(H1CoresCoinfOfTrivial (A.toCoinvariants S) S).X₁
hz :
  (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial (A.toCoinvariants S) S).f) z =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinf A S).f).range

Tactic:
induction z using H1_induction_on with

Goal state after:
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
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x y : ↥selmerGroup
⊢ (fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑(x * y)) =
    (fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑x) * fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑y

Tactic:
by simp only [Subgroup.coe_mul, map_mul]; rfl

Goal state after:
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M''
M''' : Type u_6
inst✝¹ : AddCommGroup M'''
inst✝ : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h : IsSMulRegular M''' r
this : IsSMulRegular (M'' ⧸ f₂.range) r
⊢ Exact ⇑((r • ⊤).mapQ (r • ⊤) f₁ ⋯) ⇑((r • ⊤).mapQ (r • ⊤) f₂ ⋯)

Tactic:
Exact.exact_mapQ_iff h₁₂,

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M''
M''' : Type u_6
inst✝¹ : AddCommGroup M'''
inst✝ : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h : IsSMulRegular M''' r
this : IsSMulRegular (M'' ⧸ f₂.range) r
⊢ f₂.range ⊓ r • ⊤ ≤ Submodule.map f₂ (r • ⊤)
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
ι : Type u_4
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
a : ι → R
x : ι → M
⊢ dp R q (∑ i ∈ s, a i • x i) =
    ∑ k ∈ s.sym q, (∏ i ∈ s, a i ^ Multiset.count i ↑k) • ∏ i ∈ s, dp R (Multiset.count i ↑k) (x i)

Tactic:
by
  simp_rw [dp_sum, dp_smul, Algebra.smul_def, map_prod, ← Finset.prod_mul_distrib]

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

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ n ≠ 0 ∧ ∅ = ∅

Tactic:
exact ⟨hn, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ ⊤ = Ideal.ofList (r :: rs) • ⊤ ↔ ⊤ = Ideal.ofList rs • ⊤

Tactic:
conv => congr <;> rw [eq_comm, ← Quotient.subsingleton_iff]

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ Subsingleton (M ⧸ Ideal.ofList (r :: rs) • ⊤) ↔ Subsingleton (QuotSMulTop r M ⧸ Ideal.ofList rs • ⊤)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m : M
k : ℕ
⊢ dp R n m ^ k = ↑(k • {n}).multinomial * dp R (k * n) m

Tactic:
by
  rw [Multiset.multinomial_nsmul_singleton, ← Fin.prod_const, prod_dp]
  simp [Nat.multinomial]

Goal state after: