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

Goal state before:
pp: case refine_1
ι : 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
this : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂.toPrepartition this).iUnion = ↑I \ (π.filter p).iUnion

pp: case refine_2
ι : 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
this : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂.toPrepartition this).distortion ≤ c

Tactic:
· suffices ↑I \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = ↑I \ (π.filter p).iUnion by
      simp [π₂, *]
    have h : (π.filter p).iUnion ⊆ π.iUnion :=
      biUnion_subset_biUnion_left (Finset.filter_subset _ _)
    ext x
    fconstructor
    · rintro (⟨hxI, hxπ⟩ | ⟨hxπ, hxp⟩)
      exacts [⟨hxI, mt (@h x) hxπ⟩, ⟨π.iUnion_subset hxπ, hxp⟩]
    · rintro ⟨hxI, hxp⟩
      by_cases hxπ : x ∈ π.iUnion
      exacts [Or.inr ⟨hxπ, hxp⟩, Or.inl ⟨hxI, hxπ⟩]

Goal state after:
case refine_2
ι : 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
this : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂.toPrepartition this).distortion ≤ c
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: K : Type u_1
inst✝¹⁴ : NormedField K
inst✝¹³ : LinearOrder K
inst✝¹² : IsStrictOrderedRing K
inst✝¹¹ : HasSolidNorm K
inst✝¹⁰ : FloorRing K
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace K E
inst✝⁷ : FiniteDimensional K E
inst✝⁶ : ProperSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace K F
inst✝³ : FiniteDimensional K F
inst✝² : ProperSpace F
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
e : F ≃L[K] E
ι : Type u_4
b : Basis ι ℤ ↥L
⊢ ofZLatticeBasis K (ZLattice.comap K L ↑↑e) (ofZLatticeComap K L (↑e) b) = (ofZLatticeBasis K L b).map ↑e.symm

Tactic:
ext
  simp

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

Goal state before:
pp: case e'_3
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ 1 i j = if i = j then 1 else 0

Tactic:
Matrix.one_apply

Goal state after:
case e'_3
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ (if i = j then 1 else 0) = if i = j then 1 else 0
Module: Mathlib.Analysis.BoxIntegral.Partition.Measure

Goal state before:
pp: ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ (μ π.iUnion).toReal = ∑ J ∈ π.boxes, (μ ↑J).toReal

Tactic:
← ENNReal.toReal_sum (fun J _ => (J.measure_coe_lt_top μ).ne),

Goal state after:
ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ (μ π.iUnion).toReal = (∑ a ∈ π.boxes, μ ↑a).toReal
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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
a : ι
ha : a ∈ Finset.Iio n
⊢ gramSchmidt 𝕜 f a ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)

Tactic:
Finset.mem_Iio

Goal state after:
𝕜 : 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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
a : ι
ha : a < n
⊢ gramSchmidt 𝕜 f a ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio 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.UnitPartition

Goal state before:
pp: case e'_3
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
x✝ : ℕ
⊢ ↑(Nat.card ↑(s ∩ (↑x✝)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) =
    ∑' (x : ↑(s ∩ (↑x✝)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), 1

pp: case e'_5
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ volume.real s = ∫ (x : ι → ℝ) in s, 1

Tactic:
· rw [tsum_const, nsmul_eq_mul, mul_one, Nat.cast_inj]

Goal state after:
case e'_5
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ volume.real s = ∫ (x : ι → ℝ) in s, 1
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : SimpleFunc (ι → ℝ) E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
⊢ HasIntegral I l (⇑f) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) f)

Tactic:
induction f using MeasureTheory.SimpleFunc.induction with

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
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
⊢ dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂

Tactic:
rcases h₁.exists_common_compl h₂ HU with ⟨π, hπU, hπc₁, hπc₂⟩

Goal state after:
ι : 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
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
π : Prepartition I
hπU : π.iUnion = ↑I \ π₁.iUnion
hπc₁ : l.bDistortion = true → π.distortion ≤ c₁
hπc₂ : l.bDistortion = true → π.distortion ≤ c₂
⊢ dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: R : Type u_1
inst✝⁵ : AddCommGroup R
inst✝⁴ : UniformSpace R
inst✝³ : IsUniformAddGroup R
inst✝² : CompleteSpace R
inst✝¹ : T0Space R
f : ℕ → R
hf : Summable f
N : ℕ
inst✝ : NeZero N
⊢ ∑' (n : ℕ), f n = ∑ j, ∑' (m : ℕ), f (j.val + N * m)

Tactic:
rw [← (residueClassesEquiv N).symm.tsum_eq f, Summable.tsum_prod, tsum_fintype,
    residueClassesEquiv, Equiv.coe_fn_symm_mk]

Goal state after:
R : Type u_1
inst✝⁵ : AddCommGroup R
inst✝⁴ : UniformSpace R
inst✝³ : IsUniformAddGroup R
inst✝² : CompleteSpace R
inst✝¹ : T0Space R
f : ℕ → R
hf : Summable f
N : ℕ
inst✝ : NeZero N
⊢ Summable fun c ↦ f (N.residueClassesEquiv.symm c)
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p q : ℕ
hpq : q < p
⊢ 0 < ↑p - ↑q

Tactic:
lia

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ ↑p - ↑q < 0

Tactic:
lia

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case succ
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k
⊢ ∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u (n + 1) + 1), f k

Tactic:
suffices (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k by
      rw [sum_range_succ, ← sum_Ico_consecutive]
      exacts [add_le_add ihn this,
        (add_le_add_left (hu n.zero_le) _ : u 0 + 1 ≤ u n + 1),
        add_le_add_left (hu n.le_succ) _]
    have : ∀ k ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1)) ≤ f k := fun k hk =>
      hf (Nat.lt_of_le_of_lt (Nat.succ_le_of_lt (h_pos n)) <| (Nat.lt_succ_of_le le_rfl).trans_le
        (mem_Ico.mp hk).1) (Nat.le_of_lt_succ <| (mem_Ico.mp hk).2)
    convert! sum_le_sum this
    simp

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inr
p : ℝ
hp : p < 0
h : Summable fun n ↦ (↑n ^ p)⁻¹
⊢ False

Tactic:
obtain ⟨k : ℕ, hk₁ : ((k : ℝ) ^ p)⁻¹ < 1, hk₀ : k ≠ 0⟩ :=
      ((h.tendsto_cofinite_zero.eventually (gt_mem_nhds zero_lt_one)).and
          (eventually_cofinite_ne 0)).exists

Goal state after:
case inr
p : ℝ
hp : p < 0
h : Summable fun n ↦ (↑n ^ p)⁻¹
k : ℕ
hk₁ : (↑k ^ p)⁻¹ < 1
hk₀ : k ≠ 0
⊢ False
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: case mp
k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] := ⋯
⊢ x ∈ Ideal.span (⇑(of k G) '' s) → x ∈ RHS

Tactic:
suffices Ideal.span (⇑(of k G) '' s) ≤ RHS from @this x

Goal state after:
case mp
k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ Ideal.span (⇑(of k G) '' s) ≤ RHS
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
n : ℕ
hxn : ‖x‖ < normBound b * ↑n
i : ι
⊢ |(b.repr x) i| < ↑n

Tactic:
refine Int.cast_lt.mp ((abs_repr_le b x i).trans_lt ?_)

Goal state after:
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
n : ℕ
hxn : ‖x‖ < normBound b * ↑n
i : ι
⊢ (normBound b)⁻¹ * ‖x‖ < ↑↑n
Module: Mathlib.Data.Finset.SMulAntidiagonal

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
⊢ SMulAntidiagonal (hs.min hns • ht.min hnt) ⋯ = {(hs.min hns, ht.min hnt)}

Tactic:
by
  ext ⟨a, b⟩
  simp only [mem_smulAntidiagonal, mem_singleton, Prod.ext_iff]
  constructor
  · rintro ⟨has, hat, hst⟩
    obtain rfl :=
      (hs.min_le hns has).eq_of_not_lt fun hlt =>
        (SMul.smul_lt_smul_of_lt_of_le hlt <| ht.min_le hnt hat).ne' hst
    exact ⟨rfl, IsCancelSMul.left_cancel _ _ _ hst⟩
  · rintro ⟨rfl, rfl⟩
    exact ⟨hs.min_mem _, ht.min_mem _, rfl⟩

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

Goal state before:
pp: case hab
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := ⋯
d : ℕ := ⋯
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := ⋯
hε : 0 < ε
k : ℕ
hk : k ∈ range n
⊢ 2 * k + 3 ≤ 3 * (k + 1)

Tactic:
lia

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : Zero M
inst✝ : DecidablePred fun i ↦ [].getD i 0 ≠ 0
⊢ [].toFinsupp = 0

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: case inl.h
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst✝¹ : DecidablePred fun x ↦ l₁.getD x 0 ≠ 0
inst✝ : DecidablePred fun x ↦ l₂.getD x 0 ≠ 0
k : ℕ
h : l₁.length + k < l₁.length
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
i : σ
hsi : ¬s i = 0
hai : a i = 0
⊢ 0 = ↑s.multinomial * (0 * (erase i s).prod fun r m ↦ a r ^ m)

Tactic:
zero_mul,

Goal state after:
case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
i : σ
hsi : ¬s i = 0
hai : a i = 0
⊢ 0 = ↑s.multinomial * 0
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} (Function.update (Function.update f a (f a).succ) b (f b).succ) =
    multinomial {a, b} (Function.update f a (f a).succ) + multinomial {a, b} (Function.update f b (f b).succ)

Tactic:
by
  simp only [binomial_eq_choose, Function.update_apply,
    h, Ne, ite_true, ite_false, not_false_eq_true]
  rw [if_neg h.symm]
  rw [add_succ, choose_succ_succ, succ_add_eq_add_succ]
  ring

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

Goal state before:
pp: α : 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 : ℕ
this :
  ∀ p ∈ antidiagonal n,
    ∑ g ∈ s.piAntidiag p.2,
        ↑((g a + p.1 + s.sum g).choose (g a + p.1)) * ↑(multinomial s (g + fun i ↦ if i = a then p.1 else 0)) *
          (f a ^ (g a + p.1) * s.noncommProd (fun i ↦ f i ^ (g i + if i = a then p.1 else 0)) ⋯) =
      ∑ g ∈ s.piAntidiag p.2, ↑(n.choose p.1) * ↑(multinomial s g) * (f a ^ p.1 * s.noncommProd (fun i ↦ f i ^ g i) ⋯)
i : ℕ
x✝¹ : i ∈ range (n + 1)
g : α → ℕ
x✝ : g ∈ s.piAntidiag (n - i)
⊢ f a ^ i * (↑(multinomial s g) * s.noncommProd (fun i ↦ f i ^ g i) ⋯) * ↑(n.choose i) =
    ↑(n.choose i) * ↑(multinomial s g) * (f a ^ i * s.noncommProd (fun i ↦ f i ^ g i) ⋯)

Tactic:
rw [← Nat.cast_comm, (Nat.commute_cast (f a ^ i) _).left_comm, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mpr.inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
⊢ p ∣ X i * q

Tactic:
suffices p = X i * p.divMonomial (Finsupp.single i 1) by
        rw [this]
        exact mul_dvd_mul_left (X i) hq
      conv_lhs => rw [← p.modMonomial_add_divMonomial (Finsupp.single i 1)]
      simpa only [← C_mul_X_eq_monomial, C_1, one_mul, add_eq_right,
        ← X_dvd_iff_modMonomial_eq_zero]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
⊢ (eval₂Hom f g).comp ↑(expand p) = eval₂Hom f (g ^ p)

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f r : MvPolynomial σ R
hg : f * r ≠ 0
⊢ f.totalDegree ≤ f.totalDegree + r.totalDegree

Tactic:
lia

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

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : m.toSyn c ≤ m.toSyn (m.degree f)
⊢ ¬m.toSyn d ≤ m.toSyn (m.degree g)

Tactic:
intro hf'

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : m.toSyn c ≤ m.toSyn (m.degree f)
hf' : m.toSyn d ≤ m.toSyn (m.degree g)
⊢ False
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : n.factorization p = 0 ↔ m.factorization p = 0
h₂ : n.factorization p ≤ 1
h₃ : m.factorization p ≤ 1
⊢ n.factorization p = m.factorization p

Tactic:
lia

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

Goal state before:
pp: n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ 2 ≤ k

Tactic:
lia

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

Goal state before:
pp: n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this✝ : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : k.succ = m
d : 2 * (i + 2) ∣ n'
this : 2 * i + 3 ≤ 2
⊢ ¬2 * i + 3 ≤ 2

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
xₜ : Fin n → R
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
hpₓ₀ : pₓ ≠ 0
⊢ Finsupp.cons k (ofLex (AddMonoidAlgebra.supDegree (⇑toLex) p'.leadingCoeff)) ∈ p.support

Tactic:
rwa [← mem_support_coeff_finSuccEquiv, mem_support_iff, ← hp', hk,
                ← Polynomial.leadingCoeff, ← hpₖ, ← leadingCoeff_toLex,
                AddMonoidAlgebra.leadingCoeff_ne_zero toLex.injective]

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 g : MvPolynomial σ R
h : m.toWithBotSyn (m.withBotDegree g) < m.toWithBotSyn (m.withBotDegree f)
⊢ m.withBotDegree (f + g) = m.withBotDegree f

Tactic:
by
  by_cases hg : g = 0
  · simp [hg]
  simp only [withBotDegree_lt_withBotDegree_iff, hg, ne_eq, false_and, or_false] at h
  simp only [withBotDegree_eq_withBotDegree_iff, show f ≠ 0 by contrapose h; simp [h], iff_false]
  apply (show ∀ {p q}, p → (p → q) → (p ∧ q) by tauto) (m.degree_add_of_lt h)
  intro h'
  contrapose! h
  simp [← h', h]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℕ
⊢ ↑↑f = ↑f

Tactic:
ext
  simp

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ { toFun := fun x ↦ if x = 1 then ↑(n + 1) else 0, map_zero' := ⋯ } =
    { toFun := fun x ↦ if x = 1 then ↑n else 0, map_zero' := ⋯ } + 1

Tactic:
by ext x; by_cases h : x = 1 <;> simp [h]

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

Goal state before:
pp: f : ArithmeticFunction ℕ
x : ℕ
⊢ (f * ζ) x = ∑ i ∈ x.divisors, f i

Tactic:
rw [← natCoe_nat ζ, coe_mul_zeta_apply]

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

Goal state before:
pp: case refine_1
n k : ℕ
hk : k ≠ 0
h : ∏ p ∈ n.primeFactors, p ∣ k
⊢ n.primeFactors ⊆ k.primeFactors

Tactic:
grw [← Nat.primeFactors_mono h hk, primeFactors_prod_primeFactors]

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

Goal state before:
pp: case neg.mp
k n : ℕ
hn0 : ¬n = 0
h : (σ k) n = 1
zero_lt_sigma : 0 < (σ 0) n
sigma_zero_le_sigma : (σ 0) n ≤ (σ k) n
⊢ (σ 0) n = 1

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case inr
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hd' : d ≠ 0
⊢ 2 ≤ d

Tactic:
lia

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

Goal state before:
pp: N a✝ : ℕ
⊢ 0 < a✝ → a✝ ≤ N → ¬a✝ = 0

Tactic:
lia

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

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n a✝¹ : ℕ
hn : 0 < n ∧ n ≤ N
a✝ : 0 < a✝¹
left✝ : a✝¹ ≤ N
h : n * a✝¹ ≤ N
⊢ 0 < n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
⊢ a = b

Tactic:
by
  obtain ⟨hfab1, hfab2⟩ := Prod.mk.inj hfab
  have hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2 := by
    rw [finMulAntidiag_three a ha, hfab1, finMulAntidiag_three b hb]
  have hab2 : a 2 = b 2 := by
    rw [← mul_right_inj' <| mul_ne_zero (ne_zero_of_mem_finMulAntidiag ha 0)
      (ne_zero_of_mem_finMulAntidiag ha 1)]
    exact hprods
  have hab0 : a 0 = b 0 := by
    rw [hab2] at hfab2
    exact (mul_left_inj' <| ne_zero_of_mem_finMulAntidiag hb 2).mp hfab2;
  have hab1 : a 1 = b 1 := by
    rw [hab0] at hfab1
    exact (mul_right_inj' <| ne_zero_of_mem_finMulAntidiag hb 0).mp hfab1;
  funext i; fin_cases i <;> assumption

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ s → x ∈ Finset.range n

Tactic:
rw [Finset.mem_range]

Goal state after:
case refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ s → x < n