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

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

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

Tactic:
· simp_rw [dif_pos hI]
      exact Box.coe_subset_Icc <| (mem_admissibleIndex_iff.mp hI.choose_spec.1) (tag_mem n _)

Goal state after:
case neg
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
hI : ¬∃ ν ∈ admissibleIndex n B, I = box n ν
⊢ (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then tag n hI.choose else ⋯.choose) ∈ Box.Icc B
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
x : ι → ℝ
hx : x ∈ B
⊢ box n (index n x) ∈ (prepartition n B).toPrepartition

Tactic:
rw [TaggedPrepartition.mem_toPrepartition, mem_prepartition_iff]

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
x : ι → ℝ
hx : x ∈ B
⊢ ∃ ν ∈ admissibleIndex n B, box n ν = box n (index n x)
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
b✝ b : ι
ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
h : ¬gramSchmidt 𝕜 f a = 0
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f a‖ ^ 2) * ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0

Tactic:
rw [RCLike.ofReal_pow, ← inner_self_eq_norm_sq_to_K, div_mul_cancel₀, sub_self]
      rwa [inner_self_ne_zero]

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 μ
hf : f =ᵐ[μ.restrict ↑I] 0
hl : l.bRiemann = false
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul 0

Tactic:
by
  /- Each set `{x | n < ‖f x‖ ≤ n + 1}`, `n : ℕ`, has measure zero. We cover it by an open set of
    measure less than `ε / 2 ^ n / (n + 1)`. Then the norm of the integral sum is less than `ε`. -/
  refine hasIntegral_iff.2 fun ε ε0 => ?_
  lift ε to ℝ≥0 using ε0.lt.le; rw [gt_iff_lt, NNReal.coe_pos] at ε0
  rcases NNReal.exists_pos_sum_of_countable ε0.ne' ℕ with ⟨δ, δ0, c, hδc, hcε⟩
  have := Fact.mk (I.measure_coe_lt_top μ)
  change μ.restrict I {x | f x ≠ 0} = 0 at hf
  set N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊
  have N0 : ∀ {x}, N x = 0 ↔ f x = 0 := by simp [N]
  have : ∀ n, ∃ U, N ⁻¹' {n} ⊆ U ∧ IsOpen U ∧ μ.restrict I U < δ n / n := fun n ↦ by
    refine (N ⁻¹' {n}).exists_isOpen_lt_of_lt _ ?_
    rcases n with - | n
    · simp [ENNReal.div_zero (ENNReal.coe_pos.2 (δ0 _)).ne']
    · refine (measure_mono_null ?_ hf).le.trans_lt ?_
      · exact fun x hxN hxf => n.succ_ne_zero ((Eq.symm hxN).trans <| N0.2 hxf)
      · simp [(δ0 _).ne']
  choose U hNU hUo hμU using this
  have : ∀ x, ∃ r : Ioi (0 : ℝ), closedBall x r ⊆ U (N x) := fun x => by
    obtain ⟨r, hr₀, hr⟩ := nhds_basis_closedBall.mem_iff.1 ((hUo _).mem_nhds (hNU _ rfl))
    exact ⟨⟨r, hr₀⟩, hr⟩
  choose r hrU using this
  refine ⟨fun _ => r, fun c => l.rCond_of_bRiemann_eq_false hl, fun c π hπ _ => ?_⟩
  rw [dist_eq_norm, sub_zero, ← integralSum_fiberwise fun J => N (π.tag J)]
  grw [← hcε, ← sum_le_hasSum _ (fun n _ => (δ n).2) (NNReal.hasSum_coe.2 hδc)]
  apply norm_sum_le_of_le
  rintro n -
  dsimp [integralSum]
  have : ∀ J ∈ π.filter fun J => N (π.tag J) = n,
      ‖μ.real ↑J • f (π.tag J)‖ ≤ μ.real J * n := fun J hJ ↦ by
    rw [TaggedPrepartition.mem_filter] at hJ
    rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
    gcongr
    exact hJ.2 ▸ Nat.le_ceil _
  refine (norm_sum_le_of_le _ this).trans ?_; clear this
  rw [← sum_mul, ← Prepartition.measure_iUnion_toReal]
  let m := μ (π.filter fun J => N (π.tag J) = n).iUnion
  change m.toReal * ↑n ≤ ↑(δ n)
  have : m < δ n / n := by
    simp only [Measure.restrict_apply (hUo _).measurableSet] at hμU
    refine (measure_mono ?_).trans_lt (hμU _)
    simp only [Set.subset_def, TaggedPrepartition.mem_iUnion, TaggedPrepartition.mem_filter]
    rintro x ⟨J, ⟨hJ, rfl⟩, hx⟩
    exact ⟨hrU _ (hπ.1 _ hJ (Box.coe_subset_Icc hx)), π.le_of_mem' J hJ hx⟩
  clear_value m
  lift m to ℝ≥0 using ne_top_of_lt this
  grw [ENNReal.coe_toReal, ← NNReal.coe_natCast, ← NNReal.coe_mul, NNReal.coe_le_coe, ←
    ENNReal.coe_le_coe, ENNReal.coe_mul, ENNReal.coe_natCast, mul_comm, this, ENNReal.mul_div_le]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
⊢ (Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x

Tactic:
have := Fin.pos_iff_nonempty.1 hn

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this : Nonempty (Fin n)
⊢ (Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x
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 ι
π : TaggedPrepartition I
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
h : Integrable I l f vol
h₀ : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
hπp : π.IsPartition
⊢ dist (integralSum f vol π) (integral I l f vol) ≤ ε

Tactic:
rw [convergenceR, dif_pos h₀] at hπ
  exact (hasIntegral_iff.1 h.hasIntegral ε h₀).choose_spec.2 c _ hπ hπp

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 ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst✝ : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / (↑(#π₀.boxes) + 1)
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ

Tactic:
have H0 : 0 < (#π₀.boxes + 1 : ℝ) := Nat.cast_add_one_pos _

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 ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst✝ : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / (↑(#π₀.boxes) + 1)
H0 : 0 < ↑(#π₀.boxes) + 1
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
⊢ MeasurePreserving (⇑b.measurableEquiv) volume volume

Tactic:
convert! (b.measurableEquiv.symm.measurable.measurePreserving _).symm
  rw [← (EuclideanSpace.basisFun ι ℝ).addHaar_eq_volume]
  erw [MeasurableEquiv.coe_toEquiv_symm, Basis.map_addHaar _ b.repr.symm.toContinuousLinearEquiv]
  exact b.addHaar_eq_volume.symm

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: U : Type u_4
V : Type u_5
inst✝⁹ : NormedAddCommGroup U
inst✝⁸ : InnerProductSpace ℝ U
inst✝⁷ : MeasurableSpace U
inst✝⁶ : BorelSpace U
inst✝⁵ : FiniteDimensional ℝ U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
⊢ MeasurePreserving (⇑(MeasurableEquiv.toLp 2 (U × V)).symm) volume volume

Tactic:
suffices MeasurePreserving (volumePreservingSymmMeasurableEquivToLpProdAux U V) by
    convert! this
    ext uv
    <;> simp [volumePreservingSymmMeasurableEquivToLpProdAux, MeasurableEquiv.coe_sumPiEquivProdPi,
      MeasurableEquiv.prodCongr]

Goal state after:
U : Type u_4
V : Type u_5
inst✝⁹ : NormedAddCommGroup U
inst✝⁸ : InnerProductSpace ℝ U
inst✝⁷ : MeasurableSpace U
inst✝⁶ : BorelSpace U
inst✝⁵ : FiniteDimensional ℝ U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
⊢ MeasurePreserving (⇑(volumePreservingSymmMeasurableEquivToLpProdAux U V)) volume volume
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
⊢ covolume L₁ volume / covolume L₂ volume = ↑|b₂.det fun i ↦ ⟨↑(b₁ i), ⋯⟩|

Tactic:
Int.cast_abs

Goal state after:
ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
⊢ covolume L₁ volume / covolume L₂ volume = |↑(b₂.det fun i ↦ ⟨↑(b₁ i), ⋯⟩)|
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, g i) atTop atTop
⊢ (fun n ↦ ∑ i ∈ Finset.range n, f i) =o[atTop] fun n ↦ ∑ i ∈ Finset.range n, g i

Tactic:
have A : ∀ i, ‖g i‖ = g i := fun i => Real.norm_of_nonneg (hg i)

Goal state after:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
⊢ (fun n ↦ ∑ i ∈ Finset.range n, f i) =o[atTop] fun n ↦ ∑ i ∈ Finset.range n, g i
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
L₁ L₂ : Submodule ℤ E
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
f : (Fin (finrank ℝ E) → ℝ) ≃L[ℝ] E :=
  (EuclideanSpace.equiv (Fin (finrank ℝ E)) ℝ).symm.trans (↑(stdOrthonormalBasis ℝ E).repr).symm
hf : MeasurePreserving (⇑f) volume volume
⊢ ↑((ZLattice.comap ℝ L₁ ↑↑f).toAddSubgroup.relIndex (ZLattice.comap ℝ L₂ ↑↑f).toAddSubgroup) =
    ↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup)

Tactic:
ZLattice.comap_toAddSubgroup,

Goal state after:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
L₁ L₂ : Submodule ℤ E
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
f : (Fin (finrank ℝ E) → ℝ) ≃L[ℝ] E :=
  (EuclideanSpace.equiv (Fin (finrank ℝ E)) ℝ).symm.trans (↑(stdOrthonormalBasis ℝ E).repr).symm
hf : MeasurePreserving (⇑f) volume volume
⊢ ↑((AddSubgroup.comap (↑↑f).toAddMonoidHom L₁.toAddSubgroup).relIndex (ZLattice.comap ℝ L₂ ↑↑f).toAddSubgroup) =
    ↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup)
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
L₁ L₂ : Submodule ℤ E
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
f : (Fin (finrank ℝ E) → ℝ) ≃L[ℝ] E :=
  (EuclideanSpace.equiv (Fin (finrank ℝ E)) ℝ).symm.trans (↑(stdOrthonormalBasis ℝ E).repr).symm
hf : MeasurePreserving (⇑f) volume volume
⊢ ↑((AddSubgroup.comap (↑↑f).toAddMonoidHom L₁.toAddSubgroup).relIndex (ZLattice.comap ℝ L₂ ↑↑f).toAddSubgroup) =
    ↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup)

Tactic:
ZLattice.comap_toAddSubgroup,

Goal state after:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
L₁ L₂ : Submodule ℤ E
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
f : (Fin (finrank ℝ E) → ℝ) ≃L[ℝ] E :=
  (EuclideanSpace.equiv (Fin (finrank ℝ E)) ℝ).symm.trans (↑(stdOrthonormalBasis ℝ E).repr).symm
hf : MeasurePreserving (⇑f) volume volume
⊢ ↑((AddSubgroup.comap (↑↑f).toAddMonoidHom L₁.toAddSubgroup).relIndex
        (AddSubgroup.comap (↑↑f).toAddMonoidHom L₂.toAddSubgroup)) =
    ↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup)
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: case mp
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : ℝ
hc : ∀ (a : D), ‖f a‖ ≤ c
⊢ f =O[cocompact D] 1

Tactic:
isBigO_iff

Goal state after:
case mp
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : ℝ
hc : ∀ (a : D), ‖f a‖ ≤ c
⊢ ∃ c, ∀ᶠ (x : D) in cocompact D, ‖f x‖ ≤ c * ‖1 x‖
Module: Mathlib.Data.Set.SMulAntidiagonal

Goal state before:
pp: G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst✝¹ : SMul G P
x y : ↑(s.smulAntidiagonal t a)
inst✝ : IsLeftCancelSMul G P
h : (↑x).1 = (↑y).1
⊢ a = (↑y).1 • (↑x).2

Tactic:
rw [← h]; exact x.2.2.2.symm

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

Goal state before:
pp: case inl
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
n : ℕ
h : n < l₁.length
⊢ l₁.getD n 0 = l₁.getD n 0 + (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp) n

Tactic:
Finsupp.embDomain_of_notMem_range,

Goal state after:
case inl
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
n : ℕ
h : n < l₁.length
⊢ l₁.getD n 0 = l₁.getD n 0 + 0

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
n : ℕ
h : n < l₁.length
⊢ n ∉ Set.range ⇑(addLeftEmbedding l₁.length)
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun i ↦ (xs ++ [x]).getD i 0 ≠ 0
inst✝ : DecidablePred fun i ↦ xs.getD i 0 ≠ 0
⊢ xs.toFinsupp + Finsupp.embDomain (addLeftEmbedding xs.length) [x].toFinsupp =
    xs.toFinsupp + Finsupp.single xs.length x

Tactic:
toFinsupp_singleton,

Goal state after:
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun i ↦ (xs ++ [x]).getD i 0 ≠ 0
inst✝ : DecidablePred fun i ↦ xs.getD i 0 ≠ 0
⊢ xs.toFinsupp + Finsupp.embDomain (addLeftEmbedding xs.length) (Finsupp.single 0 x) =
    xs.toFinsupp + Finsupp.single xs.length x
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: case hnc.e_f
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hs : ((indicator a.support fun i x_1 ↦ x i).sum fun x m ↦ m) ≠ n
hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
i : σ
⊢ (indicator a.support fun i x_1 ↦ x i) i = x i

Tactic:
by_cases hi : i ∈ a.support

Goal state after:
case pos
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hs : ((indicator a.support fun i x_1 ↦ x i).sum fun x m ↦ m) ≠ n
hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
i : σ
hi : i ∈ a.support
⊢ (indicator a.support fun i x_1 ↦ x i) i = x i

case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hs : ((indicator a.support fun i x_1 ↦ x i).sum fun x m ↦ m) ≠ n
hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
i : σ
hi : i ∉ a.support
⊢ (indicator a.support fun i x_1 ↦ x i) i = x i
Module: Mathlib.Algebra.MvPolynomial.Division

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

Tactic:
← p.modMonomial_add_divMonomial (Finsupp.single i 1)

Goal state after:
σ : 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.modMonomial (Finsupp.single i 1) + (monomial (Finsupp.single i 1)) 1 * p.divMonomial (Finsupp.single i 1)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
m : ↥((insert a s).sym n)
⊢ ↑((↑↑m).card.choose (Multiset.count a ↑↑m) * (Multiset.filter (fun x ↦ a ≠ x) ↑↑m).countPerms) *
      (Multiset.map x (Multiset.filter (fun x ↦ a = x) ↑↑m) +
            Multiset.map x (Multiset.filter (fun a_1 ↦ ¬a = a_1) ↑↑m)).noncommProd
        ⋯ =
    x a ^ ↑((symInsertEquiv ha) m).fst *
        (↑(↑↑((symInsertEquiv ha) m).snd).countPerms * (Multiset.map x ↑↑((symInsertEquiv ha) m).snd).noncommProd ⋯) *
      ↑(n.choose ↑((symInsertEquiv ha) m).fst)

Tactic:
simp_rw [Multiset.noncommProd_add, m.1.1.filter_eq, Multiset.map_replicate, m.1.2]

Goal state after:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
m : ↥((insert a s).sym n)
⊢ ↑(n.choose (Multiset.count a ↑↑m) * (Multiset.filter (fun x ↦ a ≠ x) ↑↑m).countPerms) *
      ((Multiset.replicate (Multiset.count a ↑↑m) (x a)).noncommProd ⋯ *
        (Multiset.map x (Multiset.filter (fun a_1 ↦ ¬a = a_1) ↑↑m)).noncommProd ⋯) =
    x a ^ ↑((symInsertEquiv ha) m).fst *
        (↑(↑↑((symInsertEquiv ha) m).snd).countPerms * (Multiset.map x ↑↑((symInsertEquiv ha) m).snd).noncommProd ⋯) *
      ↑(n.choose ↑((symInsertEquiv ha) m).fst)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
j : α
hj : j ∈ ↑s
h : x = j
⊢ x ∈ ↑s

Tactic:
simpa [h] using hj

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a b : σ →₀ ℕ
⊢ m.toSyn a ≤ m.toSyn a + m.toSyn b

Tactic:
← map_add

Goal state after:
σ : Type u_1
m : MonomialOrder σ
a b : σ →₀ ℕ
⊢ m.toSyn a ≤ m.toSyn (a + b)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case inr.insert
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : (∀ i ∈ s, f i ≠ 0) → degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
h : ¬f a = 0 ∧ ∀ a ∈ s, ¬f a = 0
⊢ degreeOf n (∏ i ∈ insert a s, f i) = ∑ i ∈ insert a s, degreeOf n (f i)

Tactic:
obtain ⟨ha, hs⟩ := h

Goal state after:
case inr.insert
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : (∀ i ∈ s, f i ≠ 0) → degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
ha : ¬f a = 0
hs : ∀ a ∈ s, ¬f a = 0
⊢ degreeOf n (∏ i ∈ insert a s, f i) = ∑ i ∈ insert a s, degreeOf n (f i)
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
⊢ x = y ∨
      degree (ofDegLex x) < degree (ofDegLex y) ∨
        degree (ofDegLex x) = degree (ofDegLex y) ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    degree (ofDegLex x) < degree (ofDegLex y) ∨
      degree (ofDegLex x) = degree (ofDegLex y) ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

Tactic:
by_cases k : (ofDegLex x).degree < (ofDegLex y).degree
    · simp [k]
    · simp only [h, k, false_or]

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
hg : m.leadingCoeff g ∈ R⁰
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
by
  by_cases hf : f = 0
  · simp [hf]
  · simp only [leadingCoeff, degree_mul_of_right_mem_nonZeroDivisors hf hg, coeff_mul_of_degree_add]

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✝ : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
hq : q ≠ 0
⊢ m.toSyn (m.degree (p * q)) < m.toSyn (m.degree (p' * q)) ↔ m.toSyn (m.degree p) < m.toSyn (m.degree p')

Tactic:
refine ⟨m.degree_lt_of_left_ne_zero_of_degree_mul_lt hp, ?_⟩
  intro h
  simpa [m.degree_mul hp hq, m.degree_mul (show p' ≠ 0 by contrapose! h; simp [h]) hq] using h

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'
⊢ pₓ.natDegree = k

Tactic:
rw [hpₓ, hk, Polynomial.natDegree_map_of_leadingCoeff_ne_zero _ (mem_filter.1 hxₜ).2]

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

Goal state before:
pp: case neg.inl
d2 : 2 ∣ 0
d4 : ¬2 ∣ 0 / 2
⊢ MinSqFacProp 0 ((0 / 2).minSqFacAux 3)

pp: case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)

Tactic:
· cases d4 (by decide)

Goal state after:
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n p : ℕ
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
hn : n.factorization p ≤ 0
⊢ p ^ n.factorization p = 1

Tactic:
simp [Nat.le_zero.1 hn]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case mpr.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ ∀ x ∈ n.primeFactorsList, List.count x n.primeFactorsList ≤ List.count x (List.replicate (n.factorization p) p)

Tactic:
intro q hq'

Goal state after:
case mpr.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : q ∈ n.primeFactorsList
⊢ List.count q n.primeFactorsList ≤ List.count q (List.replicate (n.factorization p) p)