mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
⊢ (⇑b = fun x ↦ 1) ∨ ⇑b = fun x ↦ -1

Tactic:
have : Unique ι := b.toBasis.unique

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this : Unique ι
⊢ (⇑b = fun x ↦ 1) ∨ ⇑b = fun x ↦ -1
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 + ∑ i_1 < i, (𝕜 ∙ gramSchmidt 𝕜 f i_1).starProjection (f i) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)

Tactic:
starProjection_singleton

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
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)
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
j i : ι
hij : i ≤ j
⊢ f i - ∑ i_1 < i, (𝕜 ∙ gramSchmidt 𝕜 f i_1).starProjection (f i) ∈ span 𝕜 (f '' Set.Iic j)

Tactic:
starProjection_singleton

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
j i : ι
hij : i ≤ j
⊢ f i - ∑ x < i, (⟪gramSchmidt 𝕜 f x, f i⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f x‖ ^ 2)) • gramSchmidt 𝕜 f x ∈ span 𝕜 (f '' Set.Iic j)
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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsPartition
h₂ : π₂.IsPartition
⊢ integralSum f vol π₁ - integralSum f vol π₂ =
    ∑ J ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
      ((vol J) (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) -
        (vol J) (f ((π₂.infPrepartition π₁.toPrepartition).tag J)))

Tactic:
rw [← integralSum_inf_partition f vol π₁ h₂, ← integralSum_inf_partition f vol π₂ h₁,
    integralSum, integralSum, Finset.sum_sub_distrib]

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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsPartition
h₂ : π₂.IsPartition
⊢ ∑ J ∈ (π₁.infPrepartition π₂.toPrepartition).boxes, (vol J) (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) -
      ∑ J ∈ (π₂.infPrepartition π₁.toPrepartition).boxes, (vol J) (f ((π₂.infPrepartition π₁.toPrepartition).tag J)) =
    ∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, (vol x) (f ((π₁.infPrepartition π₂.toPrepartition).tag x)) -
      ∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, (vol x) (f ((π₂.infPrepartition π₁.toPrepartition).tag 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 ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y : F
a : ℝ
h :
  ∀ (ε : ℝ),
    0 < ε →
      ∃ r,
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
            l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε
⊢ HasIntegral I l f vol y

Tactic:
refine hasIntegral_iff.2 fun ε hε => ?_
  rcases exists_pos_mul_lt hε a with ⟨ε', hε', ha⟩
  rcases h ε' hε' with ⟨r, hr, H⟩
  exact ⟨r, hr, fun c π hπ hπp => (H c π hπ hπp).trans ha.le⟩

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 ι
y : E
f g : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hf : HasIntegral I l f μ.toBoxAdditive.toSMul y
hfg : f =ᵐ[μ.restrict ↑I] g
hl : l.bRiemann = false
this : g - f =ᵐ[μ.restrict ↑I] 0
⊢ HasIntegral I l g μ.toBoxAdditive.toSMul y

Tactic:
simpa using hf.add (HasIntegral.of_aeEq_zero this hl)

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
h : ¬Integrable I l f vol
⊢ (if h : Integrable I l (-f) vol then Exists.choose h else 0) =
    -if h : Integrable I l f vol then Exists.choose h else 0

Tactic:
dif_neg h,

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
h : ¬Integrable I l f vol
⊢ (if h : Integrable I l (-f) vol then Exists.choose h else 0) = -0
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.det ⇑f ≠ -1
⊢ e.toBasis.orientation = f.toBasis.orientation

Tactic:
simp [e.toBasis.orientation_eq_iff_det_pos,
    (e.det_to_matrix_orthonormalBasis_real f).resolve_right h]

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

Goal state before:
pp: α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
⊢ u ^ r ~[l] v ^ r

Tactic:
isEquivalent_iff_exists_eq_mul

Goal state after:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
⊢ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u ^ r =ᶠ[l] φ * v ^ r
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: case e_a
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
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0
n : ℕ
hn : 0 < n
⊢ Nat.card ↑(⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) =
    Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)

Tactic:
refine Nat.card_congr <| ((b.ofZLatticeBasis ℝ).equivFun.toEquiv.subtypeEquiv fun x ↦ ?_).symm

Goal state after:
case e_a
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
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0
n : ℕ
hn : 0 < n
x : E
⊢ x ∈ s ∩ (↑n)⁻¹ • ↑L ↔
    (Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv x ∈
      ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: case h₁
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
⊢ ⇑s ∉ a.support.piAntidiag n →
    (if s = indicator a.support fun i x ↦ s i then ↑(Nat.multinomial a.support ⇑s) * ∏ x ∈ a.support, a x ^ s x
      else 0) =
      0

Tactic:
ite_eq_right_iff

Goal state after:
case h₁
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
⊢ ⇑s ∉ a.support.piAntidiag n →
    (s = indicator a.support fun i x ↦ s i) → ↑(Nat.multinomial a.support ⇑s) * ∏ x ∈ a.support, a x ^ s x = 0
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
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hc : ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : 2 * μ.toBoxAdditive I * ε₁ < ε
C : ℝ
hC : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) := ⋯
μ' : Measure (ι → ℝ) := ⋯
μ'D : μ' D = 0
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : μ' U < ENNReal.ofReal ε₂
comp : IsCompact (Box.Icc I \ U)
this✝ : ∀ x ∈ Box.Icc I \ U, oscillationWithin f (Box.Icc I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr : ∀ x ∈ Box.Icc I \ U, ediam (f '' (eball x (ENNReal.ofReal r) ∩ Box.Icc I)) ≤ ENNReal.ofReal ε₁
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₁) π₁
h₁p : π₁.IsPartition
h₂ : l.MemBaseSet I c₂ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₂) π₂
h₂p : π₂.IsPartition
μI : μ ↑I < ∞
t₁ : Box ι → ι → ℝ := ⋯
t₂ : Box ι → ι → ℝ := ⋯
B : Finset (Box ι) := ⋯
B' : Finset (Box ι) := ⋯
hB' : B' ⊆ B
μJ_ne_top : ∀ J ∈ B, μ ↑J ≠ ∞
un : ∀ S ⊆ B, ⋃ J ∈ S, ↑J ⊆ ↑I
this : ∀ J ∈ B', ‖μ.toBoxAdditive J • (f (t₁ J) - f (t₂ J))‖ ≤ μ.toBoxAdditive J * (2 * C)
⊢ μ' (⋃ J ∈ B', ↑J) ≤ μ' U

Tactic:
apply μ'.mono
      simp_rw [iUnion_subset_iff]
      exact fun J hJ ↦ (mem_filter.1 hJ).2

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ ((expand p) φ).support ⊆ Finset.image (fun x ↦ p • x) φ.support

Tactic:
conv_lhs => rw [φ.as_sum]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ ((expand p) (∑ v ∈ φ.support, (monomial v) (coeff v φ))).support ⊆ Finset.image (fun x ↦ p • x) φ.support
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ∀ a ∈ ↑s, x ≠ a

Tactic:
exact fun j hj h ↦ hx <| by simpa [h] using hj

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

Goal state before:
pp: k n : ℕ
⊢ (k • {n}).multinomial = Nat.multinomial (Finset.range k) fun x ↦ n

Tactic:
simp [multinomial_nsmul]

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
hi : r i i
⊢ s i (x₁ i) (x₁ i)

Tactic:
rwa [hr i hi, if_pos hp] at hs

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 * r).totalDegree

Tactic:
totalDegree_mul_of_isDomain (by aesop) (by aesop)

Goal state after:
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
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.degree f ≠ m.degree g
⊢ m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
by_cases h' : m.degree g ≺[m] m.degree f

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))
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
h : m.degree f ≠ m.degree g
h' : ¬m.degree f = m.degree g → m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree (g + f)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
degree_add_of_lt (h' h),

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.degree f = m.degree g → m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree g) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n m : ℕ
hn : Squarefree n
hm : Squarefree m
⊢ n = m → ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)

Tactic:
by rintro rfl; simp

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
h : pₓ = 0
⊢ (eval xₜ) (p'.coeff p'.natDegree) = 0

Tactic:
← hk,

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
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
h : pₓ = 0
⊢ (eval xₜ) (p'.coeff k) = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ (f * ↑ζ) x = ∑ i ∈ x.divisors, f i

Tactic:
rw [← coe_zeta_mul_comm, coe_zeta_mul_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
h0 : ¬k = 0
⊢ f 0 ^ k = 0

Tactic:
simp_rw [map_zero, zero_pow h0]

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

Goal state before:
pp: case mp
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃! p, Nat.Prime p ∧ p ∣ n

Tactic:
rintro ⟨p, k, hp, hk, rfl⟩
    refine ⟨p, ⟨hp, dvd_pow_self _ hk.ne'⟩, ?_⟩
    rintro q ⟨hq, hq'⟩
    exact (Nat.prime_dvd_prime_iff_eq hq hp).1 (hq.dvd_of_dvd_pow hq')

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

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
hs : ¬m.sPolynomial f g = 0
⊢ m.toSyn (m.degree (m.sPolynomial f g)) ≠ m.toSyn (m.degree f ⊔ m.degree g)

Tactic:
apply m.toSyn.injective.ne

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
hs : ¬m.sPolynomial f g = 0
⊢ m.degree (m.sPolynomial f g) ≠ m.degree f ⊔ m.degree g
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
⊢ (pow k) n = if k = 0 ∧ n = 0 then 0 else n ^ k

Tactic:
by
  cases k <;> simp [pow]

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

Goal state before:
pp: k n : ℕ
⊢ (σ k) n ≤ n ^ (k + 1)

Tactic:
simp only [sigma_apply, pow_succ']

Goal state after:
k n : ℕ
⊢ ∑ d ∈ n.divisors, d ^ k ≤ n * n ^ k
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case cons
ih : ℕ
s✝ : Multiset ℕ
a✝ : s✝.prod ≠ 0 → Ω s✝.prod = (Multiset.map (⇑Ω) s✝).sum
h0 : (ih ::ₘ s✝).prod ≠ 0
⊢ Ω (ih ::ₘ s✝).prod = (Multiset.map (⇑Ω) (ih ::ₘ s✝)).sum

Tactic:
| cons ih =>

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

Goal state before:
pp: d n : ℕ
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag n ↔ ∏ i, f i = n ∧ n ≠ 0

Tactic:
unfold finMulAntidiag
  split_ifs with h
  · simp_rw [mem_map, mem_finAntidiagonal, Function.Embedding.arrowCongrRight_apply,
      Function.comp_def, Function.Embedding.trans_apply, Equiv.coe_toEmbedding,
      Function.Embedding.coeFn_mk, ← Additive.ofMul.symm_apply_eq, Additive.ofMul_symm_eq,
      toMul_sum, (Equiv.piCongrRight fun _ => Additive.ofMul).surjective.exists,
      Equiv.piCongrRight_apply, Pi.map_apply, toMul_ofMul, ← PNat.coe_inj, PNat.mk_coe,
      PNat.coe_prod]
    constructor
    · rintro ⟨a, ha_mem, rfl⟩
      exact ⟨ha_mem, h.ne.symm⟩
    · rintro ⟨rfl, _⟩
      refine ⟨fun i ↦ ⟨f i, ?_⟩, rfl, funext fun _ => rfl⟩
      apply Nat.pos_of_ne_zero
      exact Finset.prod_ne_zero_iff.mp h.ne.symm _ (mem_univ _)
  · simp only [not_lt, nonpos_iff_eq_zero] at h
    simp only [h, notMem_empty, ne_eq, not_true_eq_false, and_false]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).1.1 = (a1 * a2).gcd (a1 * b1)

Tactic:
rw [gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one, mul_one]

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

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ n ∈ Ioc 0 N, (f * ↑zeta) n = ∑ n ∈ Ioc 0 N, f n * ↑(N / n)

Tactic:
by
  rw [sum_Ioc_mul_eq_sum_sum]
  refine sum_congr rfl fun n hn ↦ ?_
  simp_rw [natCoe_apply]
  rw_mod_cast [sum_Ioc_zeta]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.degree (X i) = single i 1

pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.toSyn (m.degree (C r)) < m.toSyn (m.degree (X i))

Tactic:
degree_X

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ single i 1 = single i 1

R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.toSyn (m.degree (C r)) < m.toSyn (m.degree (X i))
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
⊢ min (mk y) (mk z) ≤ mk x

Tactic:
have H := mabs_le_max_mabs_mabs hy hz
  rw [← mabs_of_one_le (le_max_of_le_left (one_le_mabs y))] at H
  apply (mk_le_mk_of_mabs H).trans'
  obtain h | h := le_total |y|ₘ |z|ₘ
  · rw [max_eq_right h, min_eq_right, mk_mabs]
    exact mk_le_mk_of_mabs h
  · rw [max_eq_left h, min_eq_left, mk_mabs]
    exact mk_le_mk_of_mabs h

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : (i : ι) → AddCommMonoid (π i)
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → SMulZeroClass α (π i)
inst✝ : (i : ι) → FloorDiv α (π i)
a : α
⊢ (fun i ↦ 0 i ⌊/⌋ a) = 0

Tactic:
ext i; exact zero_floorDiv a

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:

Tactic:
b * a < b * (⌊a⌋₊ + 1) := by gcongr; apply lt_floor_add_one
    _ ≤ ⌊a⌋₊ := by
      rw [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
        ← ceil_le]
      exact le_floor hba

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
m : ℕ
⊢ IsNat ⌊↑(Int.negOfNat m)⌋₊ 0

Tactic:
exact ⟨Nat.floor_of_nonpos <| by simp⟩

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Icc a b) = Icc (a + c) (b + c)

Tactic:
simp_rw [add_comm _ c]
  exact map_add_left_Icc _ _ _

Goal state after:
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s : NonemptyInterval α
⊢ ↑(↑s ⊓ ⊥) = ↑↑s ∩ ↑⊥

Tactic:
inf_bot_eq

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s : NonemptyInterval α
⊢ ↑⊥ = ↑↑s ∩ ↑⊥
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ ↑⊥ = ⋂ s ∈ S, ↑s

Tactic:
refine (not_nonempty_iff_eq_empty.1 ?_).symm
    rintro ⟨x, hx⟩
    rw [mem_iInter₂] at hx
    exact h fun s ha t hb => (hx _ ha).1.trans (hx _ hb).2

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
hx✝ : x.orderTop ≠ ⊤
hx : x ≠ 0
⊢ x.coeff (x.orderTop.untop hx✝) = x.leadingCoeff

Tactic:
rw [leadingCoeff_of_ne_zero hx, (WithTop.untop_eq_iff _).mpr (orderTop_of_ne_zero hx)]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
⊢ BddBelow (Function.support f)

Tactic:
by
  refine ⟨n, fun _ ↦ ?_⟩
  contrapose
  simp_all

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case mpr
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
a1 : Γ
a2 : Γ'
⊢ a1 = b ∧ a2 = a → a1 = b ∧ a2 ∈ ((of R).symm x).support ∧ a1 +ᵥ a2 = b +ᵥ a

Tactic:
· rintro ⟨rfl, rfl⟩
      exact ⟨rfl, by exact hx, rfl⟩

Goal state after: