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

Goal state before:
pp: case refine_1
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
J : Box ι
x✝ : J ∈ π.boxes
⊢ dist (μ.real ↑J • g (π.tag J)) (μ.real ↑J • (f (Nx (π.tag J))) (π.tag J)) ≤ μ.real ↑J * ↑ε

Tactic:
rw [dist_eq_norm, ← smul_sub, norm_smul, Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]

Goal state after:
case refine_1
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
J : Box ι
x✝ : J ∈ π.boxes
⊢ μ.real ↑J * ‖g (π.tag J) - (f (Nx (π.tag J))) (π.tag J)‖ ≤ μ.real ↑J * ↑ε
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
⊢ volume (parallelepiped ⇑b) = 1

Tactic:
have : Fact (finrank ℝ F = finrank ℝ F) := ⟨rfl⟩
  let o := (stdOrthonormalBasis ℝ F).toBasis.orientation
  rw [← o.measure_eq_volume]
  exact o.measure_orthonormalBasis b

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

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
⊢ MeasurePreserving (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)).symm) volume volume

Tactic:
suffices volume = map (MeasurableEquiv.toLp 2 (ι → ℝ)) volume by
    convert! ((MeasurableEquiv.toLp 2 (ι → ℝ)).measurable.measurePreserving _).symm
  rw [← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar_def,
    MeasurableEquiv.coe_toLp, ← PiLp.coe_symm_continuousLinearEquiv 2 ℝ, Basis.map_addHaar]
  exact (EuclideanSpace.basisFun _ _).addHaar_eq_volume.symm

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

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
⊢ volume = map (fun x ↦ x • v) (map (fun x ↦ ‖v‖⁻¹ • x) volume)

Tactic:
by
    have hv' : Submodule.span ℝ {‖v‖⁻¹ • v} = ⊤ := by
      rw [Submodule.span_singleton_eq_top_iff]
      apply exists_smul_eq_of_finrank_eq_one h
      simpa
    let f : ℝ ≃ₗᵢ[ℝ] E := (LinearIsometryEquiv.toSpanUnitSingleton (‖v‖⁻¹ • v)
      (by simp [norm_smul, hv])).trans (LinearIsometryEquiv.ofTop E _ hv')
    rw [map_map (by fun_prop) (by fun_prop)]
    convert! f.measurePreserving.map_eq.symm
    ext x
    simp [f, mul_comm, smul_smul]

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

Goal state before:
pp: E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
b₀ : Basis ι ℝ E
⊢ covolume L μ = |b₀.det (Subtype.val ∘ ⇑b)| * μ.real (fundamentalDomain b₀)

Tactic:
rw [covolume_eq_measure_fundamentalDomain L μ (isAddFundamentalDomain b μ),
    measureReal_fundamentalDomain _ _ b₀,
    measureReal_congr (fundamentalDomain_ae_parallelepiped b₀ μ)]

Goal state after:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
b₀ : Basis ι ℝ E
⊢ |b₀.det ⇑(Basis.ofZLatticeBasis ℝ L b)| * μ.real (parallelepiped ⇑b₀) =
    |b₀.det (Subtype.val ∘ ⇑b)| * μ.real (parallelepiped ⇑b₀)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case mp
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ∞
⊢ ∑' (b : ℕ), ↑(f b) = ∞

Tactic:
replace hf : ∀ m n, 1 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn =>
      ENNReal.coe_le_coe.2 (hf (zero_lt_one.trans hm) hmn)
    have h_nonneg : ∀ n, 0 ≤ (f n : ℝ≥0∞) := fun n =>
      ENNReal.coe_le_coe.2 (f n).2
    obtain hC := tsum_schlomilch_le hf h_pos h_nonneg hu_strict.monotone h_succ_diff
    simpa [add_eq_top, mul_ne_top, mul_eq_top, hC_nonzero] using eq_top_mono hC h

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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁶ : DiscreteTopology ↥L
inst✝⁵ : IsZLattice ℝ L
ι : Type u_2
inst✝⁴ : Fintype ι
b : Basis ι ℤ ↥L
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nonempty ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0
c : ℝ
hc : 0 < c
aux₁ : ↑(card ι) ≠ 0
⊢ ((fun x ↦
          ↑(Nat.card
                ↑(⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1} ∩
                    x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) /
            x ^ card ι) ∘
        fun x ↦ x ^ (↑(card ι))⁻¹)
      c =
    ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c

Tactic:
have aux₂ : 0 < c ^ (card ι : ℝ)⁻¹ := Real.rpow_pos_of_pos hc _

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁶ : DiscreteTopology ↥L
inst✝⁵ : IsZLattice ℝ L
ι : Type u_2
inst✝⁴ : Fintype ι
b : Basis ι ℤ ↥L
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nonempty ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0
c : ℝ
hc : 0 < c
aux₁ : ↑(card ι) ≠ 0
aux₂ : 0 < c ^ (↑(card ι))⁻¹
⊢ ((fun x ↦
          ↑(Nat.card
                ↑(⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1} ∩
                    x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) /
            x ^ card ι) ∘
        fun x ↦ x ^ (↑(card ι))⁻¹)
      c =
    ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case convert_1
f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
⊢ ∀ (n_1 : ℕ), 0 ≤ f (max n_1 (n + m))

pp: case convert_2
f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
⊢ ∀ ⦃m_1 n_1 : ℕ⦄, 0 < m_1 → m_1 ≤ n_1 → f (max n_1 (n + m)) ≤ f (max m_1 (n + m))

Tactic:
· simp_all

Goal state after:
case convert_2
f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
⊢ ∀ ⦃m_1 n_1 : ℕ⦄, 0 < m_1 → m_1 ≤ n_1 → f (max n_1 (n + m)) ≤ f (max m_1 (n + m))
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : k[G]
⊢ x ∈ Ideal.span (⇑(of k G) '' s) ↔ ∀ m ∈ x.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'

Tactic:
classical
  let RHS : Ideal (MonoidAlgebra k G) :=
    { carrier := { p | ∀ m : G, m ∈ p.coeff.support → ∃ m' ∈ s, ∃ d, m = d * m' }
      add_mem' {x y} hx hy m hm := (Finset.mem_union.1 <| Finsupp.support_add hm).elim (hx m) (hy m)
      zero_mem' := by simp
      smul_mem' x y hy m hm := by
        simp only [smul_eq_mul, mul_def, coeff_finsuppSum] at hm
        obtain ⟨xm, -, hm⟩ := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
        obtain ⟨ym, hym, hm⟩ := Finset.mem_biUnion.mp (Finsupp.support_sum hm)
        obtain rfl := Finset.mem_singleton.mp (Finsupp.support_single_subset hm)
        refine (hy _ hym).imp fun sm p => And.imp_right ?_ p
        rintro ⟨d, rfl⟩
        exact ⟨xm * d, (mul_assoc _ _ _).symm⟩ }
  change _ ↔ x ∈ RHS
  constructor
  · suffices Ideal.span (⇑(of k G) '' s) ≤ RHS from @this x
    rw [Ideal.span_le]
    rintro _ ⟨i, hi, rfl⟩ m hm
    refine ⟨_, hi, 1, ?_⟩
    simpa using Finsupp.support_single_subset hm
  · intro hx
    rw [← x.sum_coeff_single]
    apply Ideal.sum_mem _ fun i hi ↦ ?_
    obtain ⟨d, hd, d2, rfl⟩ := hx _ hi
    simpa using Ideal.mul_mem_left _ (.single d2 <| x.coeff (d2 * d)) (b := of k G d)
      (Ideal.subset_span <| Set.mem_image_of_mem _ hd)

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
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)
ε : ℝ := normBound b
hε : 0 < ε
⊢ 2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range n, ↑(k + 1) ^ (↑d - 1 + r) ≤
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range (n + 1), ↑k ^ (↑d - 1 + r)

Tactic:
Finset.sum_range_succ',

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
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)
ε : ℝ := normBound b
hε : 0 < ε
⊢ 2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range n, ↑(k + 1) ^ (↑d - 1 + r) ≤
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * (∑ k ∈ range n, ↑(k + 1) ^ (↑d - 1 + r) + ↑0 ^ (↑d - 1 + r))
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: case hbc
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := ⋯
this : Fintype I
b : Basis I ℤ ↥L := ⋯
d : ℕ := ⋯
hd : d ≠ 0
ε : ℝ := ⋯
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H : ∀ r < -↑d, ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -↑d
s : Finset ↥L
⊢ A ≤ A⁻¹ ^ r

Tactic:
← Real.rpow_neg_one,

Goal state after:
case hbc
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H : ∀ r < -↑d, ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -↑d
s : Finset ↥L
⊢ A ≤ (A ^ (-1)) ^ r
Module: Mathlib.Data.Nat.Factorial.DoubleFactorial

Goal state before:
pp: n : ℕ
⊢ (n + 1)‼ ≤ (n + 1)!

Tactic:
by
    rw [factorial_eq_mul_doubleFactorial]; exact Nat.le_mul_of_pos_right _ n.doubleFactorial_pos

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

Goal state before:
pp: case mp.inl.h
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
hn : ¬x.1 i = 0
⊢ Finsupp.single i 1 ≤ x.1

Tactic:
simpa [← Nat.one_le_iff_ne_zero] using hn

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

Goal state before:
pp: case mp.inr.h
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
hn : ¬x.2 i = 0
⊢ Finsupp.single i 1 ≤ x.2

Tactic:
simpa [← Nat.one_le_iff_ne_zero] using hn

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

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
⊢ ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r

Tactic:
induction d with
  | zero =>
    intro n hn p
    rw [Finsupp.degree_eq_zero_iff] at hn
    simp only [hn, monomial_zero', C_1, one_mul, nonpos_iff_eq_zero, exists_and_left,
      exists_eq_left, exists_eq_right', implies_true]
  | succ d hd =>
    intro n hn p q
    refine ⟨fun hp ↦ ?_, fun ⟨m, r, hmn, hrq, hp⟩ ↦ ?_⟩
    · obtain ⟨i, hi⟩ : n.support.Nonempty := by
        rw [Finsupp.support_nonempty_iff]
        intro hn'
        simp [hn'] at hn
      let n' := n - Finsupp.single i 1
      have hn' : n' + Finsupp.single i 1 = n := by
        apply Finsupp.sub_add_single_one_cancel
        rwa [← Finsupp.mem_support_iff]
      have hnn' : n' ≤ n := by simp [← hn']
      have hd' : n'.degree = d := by
        rw [← add_left_inj, ← hn, ← hn']
        simp
      rw [← hn', monomial_add_single, pow_one, mul_comm _ (X i), mul_assoc, dvd_X_mul_iff] at hp
      rcases hp with hp | hp
      · obtain ⟨m, r, hm, hr, hp⟩ := (hd n' hd' p q).mp hp
        exact ⟨m, r, le_trans hm hnn', hr, hp⟩
      · obtain ⟨p', rfl⟩ := hp.1
        obtain ⟨m, r, hm, hr, hp⟩ := (hd n' hd' _ _).mp hp.2
        use m + Finsupp.single i 1, r, ?_, hr
        · simp [monomial_add_single, pow_one, mul_comm _ (X i), mul_assoc, ← hp]
        · simpa [← hn'] using hm
    · rw [hp, ← add_tsub_cancel_of_le hmn, ← mul_one 1, ← monomial_mul, mul_one, mul_assoc]
      apply mul_dvd_mul dvd_rfl
      apply dvd_mul_of_dvd_right hrq

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b : β
hb : Acc rβ b
⊢ Acc (Prod.GameAdd rα rβ) (a, b)

Tactic:
induction hb with | _ b hb ihb
   =>  _ 

Goal state after:
case intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b✝ b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
⊢ Acc (Prod.GameAdd rα rβ) (a, b)
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b : α
hb : Acc rα b
⊢ Acc (Sym2.GameAdd rα) s(a, b)

Tactic:
induction hb with | _ b hb ihb
   =>  _ 

Goal state after:
case intro.intro
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
⊢ Acc (Sym2.GameAdd rα) s(a, b)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
i : σ
p : MvPolynomial σ R
n : ℕ
hp : p ≠ 0
⊢ degreeOf i (p ^ n) = n * degreeOf i p

Tactic:
rw [pow_eq_prod_const, degreeOf_prod_eq (range n) (fun _ ↦ p) (fun _ _ ↦ hp)]

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
i : σ
p : MvPolynomial σ R
n : ℕ
hp : p ≠ 0
⊢ ∑ i_1 ∈ range n, degreeOf i p = n * degreeOf i p
Module: Mathlib.Algebra.Order.AbsoluteValue.Euclidean

Goal state before:
pp: x y : ℤ
⊢ ↑x.natAbs < ↑y.natAbs ↔ x.natAbs < y.natAbs

Tactic:
ofNat_lt

Goal state after:
x y : ℤ
⊢ x.natAbs < y.natAbs ↔ x.natAbs < y.natAbs
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
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn d ≤ m.toSyn (m.degree f)
⊢ m.toSyn (m.degree g) < m.toSyn e

Tactic:
apply lt_of_add_lt_add_left (a := m.toSyn d)

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn d ≤ m.toSyn (m.degree f)
⊢ m.toSyn d + m.toSyn (m.degree g) < m.toSyn d + m.toSyn e
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: case e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬a.IsDiag } = #(image (uncurry Sym2.mk) univ.offDiag)

Tactic:
← filter_image_mk_not_isDiag,

Goal state after:
case e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬a.IsDiag } = #({x ∈ image (uncurry Sym2.mk) (univ ×ˢ univ) | ¬x.IsDiag})
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 ∈ Finset.map (consEquiv fun i ↦ R).toEmbedding (S 0 ×ˢ {r ∈ piFinset (tail S) | (eval r) pₖ ≠ 0}) |
        (eval x) p = 0}) =
    #({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}.biUnion fun xₜ ↦
        image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}))

Tactic:
filter_map,

Goal state after:
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
⊢ #(Finset.map (consEquiv fun i ↦ R).toEmbedding
        (filter ((fun x ↦ (eval x) p = 0) ∘ ⇑(consEquiv fun i ↦ R).toEmbedding)
          (S 0 ×ˢ {r ∈ piFinset (tail S) | (eval r) pₖ ≠ 0}))) =
    #({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}.biUnion fun xₜ ↦
        image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}))
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case inl
h : Nat.minFac 0 ^ (Nat.factorization 0) (Nat.minFac 0) = 0
hn : 0 ≠ 1
⊢ IsPrimePow 0

pp: case inr
n : ℕ
h : n.minFac ^ n.factorization n.minFac = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ IsPrimePow n

Tactic:
· simp_all

Goal state after:
case inr
n : ℕ
h : n.minFac ^ n.factorization n.minFac = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ IsPrimePow n
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n

Tactic:
by
  simp [squarefree_mul_iff, Nat.coprime_iff_isRelPrime.mp hmn]

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

Goal state before:
pp: p a m n : ℕ
hp : Prime p
hn : n ≠ 0
h : p ^ m = a ^ n
⊢ ∃ k, a = p ^ k

Tactic:
rcases exponent_dvd_of_prime_pow_eq_pow hp h with ⟨k, m_eq⟩

Goal state after:
p a m n : ℕ
hp : Prime p
hn : n ≠ 0
h : p ^ m = a ^ n
k : ℕ
m_eq : m = n * k
⊢ ∃ k, a = p ^ k
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (if i = i then k else if i = i' then r else 1) *
        ((if i' = i then k else if i' = i' then r else 1) *
          ∏ x ∈ (univ.erase i).erase i', if x = i then k else if x = i' then r else 1) =
      k * r ∧
    k * r ≠ 0

pp: case h.h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ i' ∈ univ.erase i

Tactic:
· simp_all

Goal state after:
case h.h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ i' ∈ univ.erase i