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

Goal state before:

Tactic:
∑ i ∈ range N, ((u i : ℝ) ^ 2)⁻¹ * Var[S (u i)] =
          ∑ i ∈ range N, ((u i : ℝ) ^ 2)⁻¹ * ∑ j ∈ range (u i), Var[Y j] := by
        congr 1 with i
        congr 1
        rw [hS, IndepFun.variance_sum]
        · intro j _
          exact (hident j).aestronglyMeasurable_fst.memLp_truncation
        · intro k _ l _ hkl
          exact (hindep hkl).comp (A k).measurable (A l).measurable
      _ = ∑ j ∈ range (u (N - 1)), (∑ i ∈ range N with j < u i, ((u i : ℝ) ^ 2)⁻¹) * Var[Y j] := by
        simp_rw [mul_sum, sum_mul, sum_sigma']
        refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_
        · simp only [mem_sigma, mem_range, mem_filter, and_imp,
            Sigma.forall]
          exact fun a b haN hb ↦ ⟨hb.trans_le <| u_mono <| Nat.le_pred_of_lt haN, haN, hb⟩
        all_goals simp
      _ ≤ ∑ j ∈ range (u (N - 1)), c ^ 5 * (c - 1)⁻¹ ^ 3 / ↑j ^ 2 * Var[Y j] := by
        gcongr ∑ _ ∈ _, ?_ with j
        rcases eq_zero_or_pos j with (rfl | hj)
        · simp only [Nat.cast_zero]
          simp only [Y, Nat.cast_zero, truncation_zero, variance_zero, mul_zero, le_rfl]
        apply mul_le_mul_of_nonneg_right _ (variance_nonneg _ _)
        convert! sum_div_nat_floor_pow_sq_le_div_sq N (Nat.cast_pos.2 hj) c_one using 2
        · simp only [u, Nat.cast_lt]
        · simp only [u, one_div]
      _ = c ^ 5 * (c - 1)⁻¹ ^ 3 * ∑ j ∈ range (u (N - 1)), ((j : ℝ) ^ 2)⁻¹ * Var[Y j] := by
        simp_rw [mul_sum, div_eq_mul_inv, mul_assoc]
      _ ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * 𝔼[X 0]) := by
        apply mul_le_mul_of_nonneg_left (I1 _)
        apply mul_nonneg (pow_nonneg c_pos.le _)
        exact pow_nonneg (inv_nonneg.2 (sub_nonneg.2 c_one.le)) _

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
x : α
a : V
⊢ (ρ.coinvariantsToFinsupp α) ((Coinvariants.mk (ρ.finsupp α)) (single x a)) = single x ((Coinvariants.mk ρ) a)

Tactic:
by
  simp [coinvariantsToFinsupp]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
Ω : 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) μ
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
have C : ∀ᵐ ω ∂μ,
      Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, Y i ω)) atTop (𝓝 μ[Y 0]) := by
    apply strong_law_ae_of_measurable Y Yint ((A 0).1.stronglyMeasurable_mk)
      (fun i j hij ↦ IndepFun.congr (hindep hij) (A i).1.ae_eq_mk (A j).1.ae_eq_mk)
      (fun i ↦ ((A i).1.identDistrib_mk.symm.trans (hident i)).trans (A 0).1.identDistrib_mk)

Goal state after:
case neg
Ω : 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 ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: case mk
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
g : π₁ →ⁱL π₂
toContinuousLinearMap✝ : V →L[R] W
isIntertwining'✝ : ∀ (g : G), toContinuousLinearMap✝ ∘SL π₁ g = π₂ g ∘SL toContinuousLinearMap✝
h :
  { toContinuousLinearMap := toContinuousLinearMap✝, isIntertwining' := isIntertwining'✝ }.toContinuousLinearMap =
    g.toContinuousLinearMap
⊢ { toContinuousLinearMap := toContinuousLinearMap✝, isIntertwining' := isIntertwining'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
toContinuousLinearMap✝¹ : V →L[R] W
isIntertwining'✝¹ : ∀ (g : G), toContinuousLinearMap✝¹ ∘SL π₁ g = π₂ g ∘SL toContinuousLinearMap✝¹
toContinuousLinearMap✝ : V →L[R] W
isIntertwining'✝ : ∀ (g : G), toContinuousLinearMap✝ ∘SL π₁ g = π₂ g ∘SL toContinuousLinearMap✝
h :
  { toContinuousLinearMap := toContinuousLinearMap✝¹, isIntertwining' := isIntertwining'✝¹ }.toContinuousLinearMap =
    { toContinuousLinearMap := toContinuousLinearMap✝, isIntertwining' := isIntertwining'✝ }.toContinuousLinearMap
⊢ { toContinuousLinearMap := toContinuousLinearMap✝¹, isIntertwining' := isIntertwining'✝¹ } =
    { toContinuousLinearMap := toContinuousLinearMap✝, isIntertwining' := isIntertwining'✝ }
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : Rep k G
x✝ : X✝ ⟶ Y✝
⊢ ofHom (lTensor (trivial k G k).ρ (Hom.hom x✝)) ≫ (mkIso (lid k Y✝.ρ)).hom = (mkIso (lid k X✝.ρ)).hom ≫ x✝

Tactic:
by ext; simp [trivial_V]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : Rep k G
x✝ : X✝ ⟶ Y✝
⊢ ofHom (rTensor (trivial k G k).ρ (Hom.hom x✝)) ≫ (mkIso (rid k Y✝.ρ)).hom = (mkIso (rid k X✝.ρ)).hom ≫ x✝

Tactic:
by ext; simp [trivial_V]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝⁴ x✝³ x✝² : Rep k G
x✝¹ : k
x✝ : x✝³ ⟶ x✝²
⊢ x✝⁴ ◁ (x✝¹ • x✝) = x✝¹ • x✝⁴ ◁ x✝

Tactic:
ext1; simp [smul_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝⁴ : k
x✝³ x✝² : Rep k G
x✝¹ : x✝³ ⟶ x✝²
x✝ : Rep k G
⊢ (x✝⁴ • x✝¹) ▷ x✝ = x✝⁴ • x✝¹ ▷ x✝

Tactic:
ext1; simp [smul_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A✝ B✝ C✝ : Rep k G
A B C : Rep k G
f : A ⊗ B ⟶ C
g : G
⊢ (TensorProduct.curry (Hom.hom f).toLinearMap).flip ∘ₗ B.ρ g =
    (A.ρ.linHom C.ρ) g ∘ₗ (TensorProduct.curry (Hom.hom f).toLinearMap).flip

Tactic:
by
    ext x y
    simp only [tensor_V, tensor_ρ, LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply,
      TensorProduct.curry_apply, Representation.IntertwiningMap.toLinearMap_apply,
      Representation.linHom_apply]
    have := by simpa using (hom_comm_apply f g (A.ρ g⁻¹ y ⊗ₜ[k] x)).symm
    simp [this]

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₀.h
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
b : G
a✝ : ⟦b⟧ ∈ Finset.univ
hb : ⟦b⟧ ≠ ⟦g⟧
⊢ ⟦b⟧.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0

Tactic:
have : f.1 b = 0 := by
      simp_all only [Function.support_subset_iff, ne_eq, Quotient.eq]
      contrapose! hx
      use b, hx, hb

Goal state after:
case h₀.h
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
b : G
a✝ : ⟦b⟧ ∈ Finset.univ
hb : ⟦b⟧ ≠ ⟦g⟧
this : ↑f b = 0
⊢ ⟦b⟧.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0
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 B : Rep k G
f : A ⟶ B
inst✝ : Mono f
Z✝ : ModuleCat k
g h : Z✝ ⟶ groupCohomology A 0
hgh : g ≫ map (MonoidHom.id G) f 0 = h ≫ map (MonoidHom.id G) f 0
⊢ g = h

Tactic:
simp only [← cancel_mono (H0Iso B).hom, Category.assoc, map_id_comp_H0Iso_hom] at hgh
    simp_all [cancel_mono]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
⊢ (rename f) p = subst (X ∘ f) p

Tactic:
by
  classical
  ext n
  rw [coeff_rename, coeff_subst (HasSubst.X_comp _) p n, finsum_eq_sum _
    (coeff_subst_finite (HasSubst.X_comp _) p n)]
  have (d : σ →₀ ℕ) (hd : (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0) :
      mapDomain f d = n := by
    simp_rw [← monomial_mapDomain_apply_one] at hd
    exact (eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hd)).symm
  refine (Finset.sum_subset_zero_on_sdiff ?_ ?_ (fun x hx => ?_)).symm
  · exact Set.Finite.toFinset_mono this
  · simp +contextual [← monomial_mapDomain_apply_one]
  · simp only [Set.Finite.mem_toFinset] at hx
    simp [← this _ hx, ← monomial_mapDomain_apply_one, coeff_monomial_same]

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

Goal state before:
pp: case mul
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z₁ z₂ : R
hz₁ : z₁ ∈ closure {r | IsUnit r ∨ Prime r}
hz₂ : z₂ ∈ closure {r | IsUnit r ∨ Prime r}
S₁ : Multiset R
hS₁pri : ∀ b ∈ S₁, Prime b
hS₁ : Associated S₁.prod z₁
S₂ : Multiset R
hS₂pri : ∀ b ∈ S₂, Prime b
hS₂ : Associated S₂.prod z₂
⊢ Associated (S₁ + S₂).prod (z₁ * z₂)

Tactic:
Multiset.prod_add

Goal state after:
case mul
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z₁ z₂ : R
hz₁ : z₁ ∈ closure {r | IsUnit r ∨ Prime r}
hz₂ : z₂ ∈ closure {r | IsUnit r ∨ Prime r}
S₁ : Multiset R
hS₁pri : ∀ b ∈ S₁, Prime b
hS₁ : Associated S₁.prod z₁
S₂ : Multiset R
hS₂pri : ∀ b ∈ S₂, Prime b
hS₂ : Associated S₂.prod z₂
⊢ Associated (S₁.prod * S₂.prod) (z₁ * z₂)
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 : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : f ∈ I
⊢ constantCoeff f ∈ Ideal.map constantCoeff (span T)

Tactic:
mem_map_iff_of_surjective _ constantCoeff_surj

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
f : R⟦X⟧
hf : f ∈ I
⊢ ∃ x ∈ span T, constantCoeff x = constantCoeff f
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mpr.h.mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen[top] ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n ↦ J ^ n • ⊤ := Ideal.adic_basis J
H : ∃ i, True ∧ ↑(J ^ i) ⊆ s
⊢ s ∈ 𝓝 0

Tactic:
· rcases H with ⟨n, -, hn⟩
        rw [mem_nhds_iff]
        exact ⟨_, hn, H₁ n, (J ^ n).zero_mem⟩

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₁✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₁✝ : a₁✝ ∈ antidiagonal (optionElim k x)
a₂✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₂✝ : a₂✝ ∈ antidiagonal (optionElim k x)
a✝ : ⟨(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₂✝

Tactic:
ext t <;> cases t

Goal state after:
case refine_2.fst.none
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a₁✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₁✝ : a₁✝ ∈ antidiagonal (optionElim k x)
a₂✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₂✝ : a₂✝ ∈ antidiagonal (optionElim k x)
a✝ : ⟨(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₁✝.1 none = a₂✝.1 none

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

case refine_2.snd.none
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a₁✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₁✝ : a₁✝ ∈ antidiagonal (optionElim k x)
a₂✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₂✝ : a₂✝ ∈ antidiagonal (optionElim k x)
a✝ : ⟨(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₁✝.2 none = a₂✝.2 none

case refine_2.snd.some
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a₁✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₁✝ : a₁✝ ∈ antidiagonal (optionElim k x)
a₂✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₂✝ : a₂✝ ∈ antidiagonal (optionElim k x)
a✝ : ⟨(a₁✝.1 none, a₁✝.2 none), (a₁✝.1.some, a₁✝.2.some)⟩ = ⟨(a₂✝.1 none, a₂✝.2 none), (a₂✝.1.some, a₂✝.2.some)⟩
val✝ : σ
⊢ a₁✝.2 (Option.some val✝) = a₂✝.2 (Option.some val✝)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
p : MvPolynomial σ R
⊢ (toAdicCompletion σ R) ↑p = (AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) p

Tactic:
by
  symm; ext n
  suffices p - (truncTotal n) p ∈ MvPolynomial.idealOfVars σ R ^ n by
    simpa [toAdicCompletion, AdicCompletion.liftAlgHom, AdicCompletion.liftRingHom,
      Ideal.Quotient.mk_eq_mk_iff_sub_mem]
  exact (MvPolynomial.mem_pow_idealOfVars_iff' ..).mpr fun x hx ↦ by simp [coeff_truncTotal _ hx]

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)) ⋯
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑f
rkeq :
  Module.rank (IsLocalRing.ResidueField R) (maximalIdeal R).Cotangent =
    Module.rank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG
⊢ Module.finrank (IsLocalRing.ResidueField R) (CotangentSpace R) =
    Module.finrank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (CotangentSpace (AdicCompletion (maximalIdeal R) R))

Tactic:
simp [Module.finrank, CotangentSpace, rkeq]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x✝ : Aᵐᵒᵖ
⊢ (↑(TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ) ∘ₗ
        (rTensor Aᵐᵒᵖ (map ↑(opLinearEquiv R) ↑(opLinearEquiv R)) ∘ₗ rTensor Aᵐᵒᵖ (comul ∘ₗ ↑(opLinearEquiv R).symm)) ∘ₗ
          map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm)
      x✝ =
    (lTensor Aᵐᵒᵖ (map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm) ∘ₗ
        map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm)
      x✝

Tactic:
rTensor_comp

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x✝ : Aᵐᵒᵖ
⊢ (↑(TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ) ∘ₗ
        (rTensor Aᵐᵒᵖ (map ↑(opLinearEquiv R) ↑(opLinearEquiv R)) ∘ₗ
            rTensor Aᵐᵒᵖ comul ∘ₗ rTensor Aᵐᵒᵖ ↑(opLinearEquiv R).symm) ∘ₗ
          map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm)
      x✝ =
    (lTensor Aᵐᵒᵖ (map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm) ∘ₗ
        map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm)
      x✝
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
⊢ (p * q).contentIdeal = ⊤

Tactic:
← Ideal.radical_eq_top

Goal state after:
R : Type u_3
inst✝ : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
⊢ (p * q).contentIdeal.radical = ⊤
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
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) = (valuation K v) ↑x

Tactic:
rw [show v.valuation K x = _ * _ by rw [valuation_def]; rfl]
  rw [Units.val_inv_eq_inv_val]
  change _ = ite _ _ _ * (ite _ _ _)⁻¹
  simp_rw [IsLocalization.toLocalizationMap_sec, SubmonoidClass.coe_subtype,
    if_neg <| IsLocalization.sec_fst_ne_zero x.ne_zero,
    if_neg (nonZeroDivisors.coe_ne_zero _),
    ← exp_neg, ← exp_add, valuationOfNeZeroToFun, ← sub_eq_add_neg, exp]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case right
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
x inv✝ : R
hx : x * inv✝ = 1
inv_val✝ : inv✝ * x = 1
⊢ ¬(valuation K v) ((algebraMap R K) x) < 1

Tactic:
apply_fun v.intValuation at hx

Goal state after:
case right
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
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : v.intValuation (x * inv✝) = v.intValuation 1
⊢ ¬(valuation K v) ((algebraMap R K) x) < 1
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
n : ℕ
x : Kˣ
⊢ (powMonoidHom n) x ∈ Subgroup.comap v.valuationOfNeZero (AddSubgroup.toSubgroup (AddSubgroup.zmultiples ↑n))

Tactic:
exact
          ⟨v.valuationOfNeZero x, by simp only [powMonoidHom_apply, map_pow, Int.toAdd_pow]; rfl⟩

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 : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
mem : ∀ (a : ↥T), (algebraMap R R') ↑a ∈ p
⊢ Ideal.comap (algebraMap R R') p ∈ associatedPrimes R M

Tactic:
simp only [hx, Ideal.mem_radical_iff, mem_bot, mem_colon_singleton, ← map_pow, algebraMap_smul,
    ← IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_eq_zero' f] at mem

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 : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
mem : ∀ (a : ↥T), ∃ n s', s' • ↑a ^ n • m = 0
⊢ Ideal.comap (algebraMap R R') p ∈ associatedPrimes R M
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case insert
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
n : ι → ℕ
m : M
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, dp R (n i) m = ↑(multinomial s✝ n) * dp R (s✝.sum n) m
⊢ dp R (n a✝) m * ↑(multinomial s✝ n) * dp R (s✝.sum n) m =
    ↑(multinomial (insert a✝ s✝) n) * dp R ((insert a✝ s✝).sum n) m

Tactic:
mul_comm (dp R (n _) m),

Goal state after:
case insert
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
n : ι → ℕ
m : M
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, dp R (n i) m = ↑(multinomial s✝ n) * dp R (s✝.sum n) m
⊢ ↑(multinomial s✝ n) * dp R (n a✝) m * dp R (s✝.sum n) m =
    ↑(multinomial (insert a✝ s✝) n) * dp R ((insert a✝ s✝).sum n) m
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n✝ : ℕ
x✝ y✝ : B
hx : x✝ ∈ J
hy : y✝ ∈ J
⊢ e (hI.dpow n✝ (e.symm x✝ + e.symm y✝)) =
    ∑ k ∈ antidiagonal n✝, e (hI.dpow k.1 (e.symm x✝)) * e (hI.dpow k.2 (e.symm y✝))

Tactic:
rw [hI.dpow_add (symm_apply_mem_of_equiv_iff.mpr (h ▸ hx))
        (symm_apply_mem_of_equiv_iff.mpr (h ▸ hy))]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n✝ : ℕ
x✝ y✝ : B
hx : x✝ ∈ J
hy : y✝ ∈ J
⊢ e (∑ k ∈ antidiagonal n✝, hI.dpow k.1 (e.symm x✝) * hI.dpow k.2 (e.symm y✝)) =
    ∑ k ∈ antidiagonal n✝, e (hI.dpow k.1 (e.symm x✝)) * e (hI.dpow k.2 (e.symm y✝))
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hm : n ≠ 0
hx : x ∈ Ideal.span {↑p}
⊢ ⟨dpow' p n ↑x, ⋯⟩ ∈ Ideal.span {↑p}

Tactic:
by
  have hiff := PadicInt.norm_le_pow_iff_mem_span_pow ⟨dpow' p n x, dpow'_int p n hx⟩ 1
  rw [pow_one] at hiff
  rw [← hiff]
  simp only [cast_one, zpow_neg_one]
  exact dpow'_norm_le_of_ne_zero p hm hx

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
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ Etale R S

Tactic:
exact .of_equiv e.symm

Goal state after: