mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: ι : Type u_1
I J : Box ι
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
⊢ J ∈ π₁.disjUnion π₂ h ↔ J ∈ π₁ ∨ J ∈ π₂

Tactic:
by
  classical exact Finset.mem_union

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ x_1, (b.repr x).ofLp x_1 • b x_1 = x

Tactic:
← b.coe_toBasis_repr_apply,

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ x_1, (b.toBasis.repr x) x_1 • b x_1 = x
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : EuclideanSpace 𝕜 ι
⊢ ∑ i, v.ofLp i • b i = b.repr.symm v

Tactic:
simpa using (b.toBasis.equivFun_symm_apply v).symm

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
j : (i : η) × ι i
⊢ (Pi.orthonormalBasis B) j = PiLp.single 2 j.fst ((B j.fst) j.snd)

Tactic:
ext k

Goal state after:
η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
j : (i : η) × ι i
k : η
⊢ ((Pi.orthonormalBasis B) j).ofLp k = (PiLp.single 2 j.fst ((B j.fst) j.snd)).ofLp k
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ π₁.compl = π₂.compl

Tactic:
dsimp only [compl]

Goal state after:
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ ⋯.choose = ⋯.choose
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
h : π.IsPartition
⊢ π.compl = ⊥

Tactic:
← iUnion_eq_empty,

Goal state after:
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
h : π.IsPartition
⊢ π.compl.iUnion = ∅
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁶ : RCLike 𝕜
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : Fintype ι
E' : Type u_7
inst✝² : Fintype ι'
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
x : E
⊢ (b.equiv b' e) x = ∑ i, (b.repr x).ofLp i • b' (e i)

Tactic:
nth_rw 1 [← b.sum_repr x, map_sum]

Goal state after:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁶ : RCLike 𝕜
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : Fintype ι
E' : Type u_7
inst✝² : Fintype ι'
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
x : E
⊢ ∑ x_1, (b.equiv b' e) ((b.repr x).ofLp x_1 • b x_1) = ∑ i, (b.repr x).ofLp i • b' (e i)
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = ↑I \ π.iUnion
hc : π₁.distortion ≤ c
⊢ ∃ π', π'.iUnion = ↑I \ (π.filter p).iUnion ∧ π'.distortion ≤ c

Tactic:
set π₂ := π.filter fun J => ¬p J

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = ↑I \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun J ↦ ¬p J
⊢ ∃ π', π'.iUnion = ↑I \ (π.filter p).iUnion ∧ π'.distortion ≤ c
Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
i : ι
x : ℝ
⊢ Option.elim' 0 (⇑f) (I.splitLower i x) + Option.elim' 0 (⇑f) (I.splitUpper i x) = f I

Tactic:
← f.sum_partition_boxes hI (isPartitionSplit I i x),

Goal state after:
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
i : ι
x : ℝ
⊢ Option.elim' 0 (⇑f) (I.splitLower i x) + Option.elim' 0 (⇑f) (I.splitUpper i x) = ∑ J ∈ (split I i x).boxes, f J
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
ν : ι → ℤ
⊢ ν ∈ ⋯.toFinset ↔ box n ν ≤ B

Tactic:
Set.Finite.mem_toFinset,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
ν : ι → ℤ
⊢ ν ∈ {ν | ↑(box n ν) ⊆ ↑B} ↔ box n ν ≤ B
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
⊢ (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then tag n hI.choose else ⋯.choose) ∈ Box.Icc B

Tactic:
by
    by_cases hI : ∃ ν ∈ admissibleIndex n B, I = box n ν
    · simp_rw [dif_pos hI]
      exact Box.coe_subset_Icc <| (mem_admissibleIndex_iff.mp hI.choose_spec.1) (tag_mem n _)
    · simp_rw [dif_neg hI]
      exact Box.coe_subset_Icc B.exists_mem.choose_spec

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
hI : I ∈ (prepartition n B).boxes
⊢ box n (index n ((prepartition n B).tag I)) = I

Tactic:
by
  obtain ⟨ν, hν, rfl⟩ := mem_prepartition_boxes_iff.mp hI
  rw [prepartition_tag n hν, index_tag]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ i ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset, F i / ↑n ^ card ι =
    ∑ x ∈ (prepartition n B).boxes with (prepartition n B).tag x ∈ s, volume.real ↑x * F ((prepartition n B).tag x) +
      ∑ x ∈ (prepartition n B).boxes with (prepartition n B).tag x ∉ s, 0

Tactic:
Finset.sum_const_zero,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ i ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset, F i / ↑n ^ card ι =
    ∑ x ∈ (prepartition n B).boxes with (prepartition n B).tag x ∈ s, volume.real ↑x * F ((prepartition n B).tag x) + 0
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
i j : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i + ∑ x < i, (⟪gramSchmidt 𝕜 f x, f i⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f x‖ ^ 2)) • gramSchmidt 𝕜 f x ∈
    span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)

Tactic:
exact Submodule.add_mem _ (subset_span <| mem_image_of_mem _ hij)
    (Submodule.sum_mem _ fun k hk => smul_mem (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)) _ <|
      subset_span <| mem_image_of_mem (gramSchmidt 𝕜 f) <| (Finset.mem_Iio.1 hk).le.trans hij)

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
n : ℕ
⊢ ∃ U, N ⁻¹' {n} ⊆ U ∧ IsOpen U ∧ (μ.restrict ↑I) U < ↑(δ n) / ↑n

Tactic:
refine (N ⁻¹' {n}).exists_isOpen_lt_of_lt _ ?_

Goal state after:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
hδc : HasSum δ c
hcε : c < ε
this : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
n : ℕ
⊢ (μ.restrict ↑I) (N ⁻¹' {n}) < ↑(δ n) / ↑n
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
s : Set ι
i : ι
hi : i ∈ s
h : ¬gramSchmidt 𝕜 f i = 0
⊢ gramSchmidt 𝕜 f i ∈ 𝕜 ∙ gramSchmidtNormed 𝕜 f i

Tactic:
refine mem_span_singleton.2 ⟨‖gramSchmidt 𝕜 f i‖, smul_inv_smul₀ ?_ _⟩
    exact mod_cast norm_ne_zero_iff.2 h

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hc : ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x
⊢ Integrable I l f μ.toBoxAdditive.toSMul

Tactic:
refine integrable_iff_cauchy_basis.2 fun ε ε0 ↦ ?_

Goal state after:
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hc : ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x
ε : ℝ
ε0 : ε > 0
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: case pos
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable fun n ↦ f (m * n + k.val)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
hl : ↑l.val + ↑m = l
⊢ Summable ({n | ↑n = l}.indicator f)

Tactic:
← hl,

Goal state after:
case pos
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable fun n ↦ f (m * n + k.val)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
hl : ↑l.val + ↑m = l
⊢ Summable ({n | ↑n = ↑l.val + ↑m}.indicator f)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k ∈ Ico 2 (2 ^ n + 1), f k

Tactic:
by
  convert!
    sum_schlomilch_le' hf (fun n => pow_pos zero_lt_two n)
      (fun m n hm => pow_right_mono₀ one_le_two hm) n using 2
  simp [pow_succ, mul_two]

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
b : Basis ι ℤ ↥L
x : ↥L
i : ι
⊢ ↑|(b.repr x) i| ≤ (normBound b)⁻¹ * ‖x‖

Tactic:
by
  rw [le_inv_mul_iff₀ (normBound_pos b)]
  exact normBound_spec b x i

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
⊢ ∀ (f g : M[ι]), to_hom (f * g) = to_hom f * to_hom g

Tactic:
AddMonoidHom.map_mul_iff

Goal state after:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
⊢ AddMonoidHom.mul.compr₂ to_hom = (AddMonoidHom.mul.comp to_hom).compl₂ to_hom
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
⊢ coeff d ((X 0 + X 1) ^ n) = ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)

Tactic:
rw [← Fin.sum_univ_two, coeff_sum_X_pow_of_fintype]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
⊢ ↑(if (d.sum fun x m ↦ m) = n then d.multinomial else 0) =
    ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
⊢ (monomial i) r ∣ (monomial j) s ↔ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Tactic:
constructor
  · rintro ⟨x, hx⟩
    rw [MvPolynomial.ext_iff] at hx
    have hj := hx j
    have hi := hx i
    classical
    simp_rw [coeff_monomial, if_pos] at hj hi
    simp_rw [coeff_monomial_mul'] at hi hj
    split_ifs at hj with hi
    · exact ⟨Or.inr hi, _, hj⟩
    · exact ⟨Or.inl hj, hj.symm ▸ dvd_zero _⟩
  · rintro ⟨h | hij, d, rfl⟩
    · simp_rw [h, monomial_zero, dvd_zero]
    · refine ⟨monomial (j - i) d, ?_⟩
      rw [monomial_mul, add_tsub_cancel_of_le hij]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ (toFinsupp m).multinomial = m.card.choose (count a m) * (toFinsupp (filter (fun x ↦ a ≠ x) m)).multinomial

Tactic:
convert! Finsupp.multinomial_update a _

Goal state after:
case e'_3.e'_5.e'_1
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ m.card = (toFinsupp m).sum fun x ↦ id

case e'_3.e'_6
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ toFinsupp (filter (fun x ↦ a ≠ x) m) = (toFinsupp m).update a 0
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case cons.e_a.e_a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ ↑((p.1 + p.2).choose p.1) = ↑(n.choose p.1)

pp: case cons.e_a.e_a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ ↑(multinomial s (f + fun i ↦ if i = a then p.1 else 0)) = ↑(multinomial s f)

pp: case cons.e_a.e_a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ s.noncommProd (fun i ↦ f✝ i ^ (f i + if i = a then p.1 else 0)) ⋯ = s.noncommProd (fun i ↦ f✝ i ^ f i) ⋯

Tactic:
· rw [mem_antidiagonal.1 hp]

Goal state after:
case cons.e_a.e_a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ ↑(multinomial s (f + fun i ↦ if i = a then p.1 else 0)) = ↑(multinomial s f)

case cons.e_a.e_a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ s.noncommProd (fun i ↦ f✝ i ^ (f i + if i = a then p.1 else 0)) ⋯ = s.noncommProd (fun i ↦ f✝ i ^ f i) ⋯
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case cons
x : ℕ
m : Multiset ℕ
h : 0 < m.multinomial
⊢ 0 < (x ::ₘ m).multinomial

Tactic:
| cons x m h =>

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ StrictAnti fun a ↦ toDegLex (single a 1)

Tactic:
intro _ _ h
  simp only [lt_iff, ofDegLex_toDegLex, degree_single, lt_self_iff_false, Lex.single_lt_iff, h,
    and_self, or_true]

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ
⊢ degLex.toSyn (single a 1) ≤ degLex.toSyn (single b 1) ↔ b ≤ a

Tactic:
by
  rw [MonomialOrder.degLex_le_iff, DegLex.single_le_iff]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l ≤ Henstock
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
H₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x δ →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
H₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x δ →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
A : l.bHenstock = true
⊢ ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x δ →
              (l.bHenstock = true → x ∈ Box.Icc J) →
                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J

Tactic:
simpa only [A, true_imp_iff] using H₂

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ d = 0 ↔ ∀ (x : σ), d x = 0

Tactic:
exact Finsupp.ext_iff

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
⊢ coeff (m.degree (f ^ n)) (f ^ n) = m.leadingCoeff f ^ n

Tactic:
degree_pow,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
⊢ coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
⊢ m.leadingTerm ((monomial s) c) = (monomial s) c

Tactic:
by_cases h : c = 0

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
h : c = 0
⊢ m.leadingTerm ((monomial s) c) = (monomial s) c

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
h : ¬c = 0
⊢ m.leadingTerm ((monomial s) c) = (monomial s) c
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree (p ^ k)
⊢ Prime (p ^ k)

Tactic:
rw [squarefree_pow_iff hp.ne_one hk.ne'] at h

Goal state after:
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
⊢ Prime (p ^ k)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
f : MvPolynomial σ R
inst✝ : Decidable (f = 0)
⊢ m.withBotDegree f = if f = 0 then ⊥ else ↑(m.degree f)

Tactic:
simp [withBotDegree, degree]
  by_cases hf : f = 0
  · simp [hf]
  · simp [hf, Finset.max_eq_sup_coe, ← Finset.coe_sup_of_nonempty _ (⇑m.toSyn)]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n d : ℕ
h : n.minSqFac = some d
⊢ Prime d

Tactic:
have := minSqFac_has_prop n
  rw [h] at this
  exact this.1

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (f - m.leadingTerm f)) ≤ m.toSyn (m.degree f)

Tactic:
apply le_trans degree_sub_le
  simp [degree_leadingTerm]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ∈ n.primeFactors.powerset
⊢ (∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i = f (∏ x ∈ t, x) * g (∏ a ∈ n.primeFactors \ t, a)

Tactic:
hf.map_prod_of_subset_primeFactors n t (mem_powerset.mp ht),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ∈ n.primeFactors.powerset
⊢ (∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i = (∏ a ∈ t, f a) * g (∏ a ∈ n.primeFactors \ t, a)
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
i : Fin d
hd : d ≠ 1
⊢ image (fun f ↦ f i) (d.finMulAntidiag n) = n.divisors

Tactic:
ext k

Goal state after:
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∈ image (fun f ↦ f i) (d.finMulAntidiag n) ↔ k ∈ n.divisors
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ s.Infinite ↔ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k) atTop atTop

Tactic:
by
  constructor
  · have h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun _ ↦ r) k := by
      refine (sum_mono_set_of_nonneg ?_).comp range_mono
      exact (fun _ ↦ indicator_nonneg (fun _ _ ↦ h.le) _)
    rw [h_mono.tendsto_atTop_atTop_iff]
    intro hs n
    obtain ⟨n', hn'⟩ := exists_lt_nsmul h n
    obtain ⟨t, t_s, t_card⟩ := hs.exists_subset_card_eq n'
    obtain ⟨m, hm⟩ := t.bddAbove
    use m + 1
    grw [hn', ← t_s]
    have h : t ⊆ Finset.range (m + 1) := by
      intro i i_t
      rw [Finset.mem_range]
      exact (hm i_t).trans_lt (lt_add_one m)
    rw [sum_indicator_subset (fun _ ↦ r) h, sum_eq_card_nsmul (fun _ _ ↦ rfl), t_card]
  · contrapose!
    intro hs
    rw [tendsto_congr' (sum_indicator_eventually_eq_card r hs), tendsto_atTop_atTop]
    push Not
    obtain ⟨m, hm⟩ := exists_lt_nsmul h (Nat.card s • r)
    exact ⟨m • r, fun n ↦ ⟨n, le_refl n, not_le_of_gt hm⟩⟩

Goal state after: