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

Goal state before:
pp: 𝕜 : Type u_7
E : Type u_8
F : Type u_9
ι : Type u_10
ι' : Type u_11
inst✝⁷ : RCLike 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
x : E
y : F
b : Basis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 F
⊢ (toMatrix b'.toBasis b) ↑(((rankOne 𝕜) x) y) = Matrix.vecMulVec (⇑(b.repr x)) (star (b'.repr y).ofLp)

Tactic:
have := Fintype.ofFinite ι

Goal state after:
𝕜 : Type u_7
E : Type u_8
F : Type u_9
ι : Type u_10
ι' : Type u_11
inst✝⁷ : RCLike 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
x : E
y : F
b : Basis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 F
this : Fintype ι
⊢ (toMatrix b'.toBasis b) ↑(((rankOne 𝕜) x) y) = Matrix.vecMulVec (⇑(b.repr x)) (star (b'.repr y).ofLp)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
⊢ ∃ B, hasIntegralVertices B ∧ s ⊆ ↑B

Tactic:
have := Fintype.ofFinite ι

Goal state after:
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
⊢ ∃ B, hasIntegralVertices B ∧ s ⊆ ↑B
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ (↑n)⁻¹ ^ Finset.univ.card = (↑n ^ card ι)⁻¹

Tactic:
ENNReal.inv_pow,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ (↑n)⁻¹ ^ Finset.univ.card = (↑n)⁻¹ ^ card ι
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
v : ι → ℝ
⊢ v ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)) ↔ ∀ (i : ι), ↑n * v i ∈ Set.range ⇑(algebraMap ℤ ℝ)

Tactic:
have := Fintype.ofFinite ι

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
v : ι → ℝ
this : Fintype ι
⊢ v ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)) ↔ ∀ (i : ι), ↑n * v i ∈ Set.range ⇑(algebraMap ℤ ℝ)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Finite ι
hs₁ : IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
⊢ Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) ≤
    Nat.card ↑(s ∩ y⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))

Tactic:
have := Fintype.ofFinite ι

Goal state after:
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Finite ι
hs₁ : IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
this : Fintype ι
⊢ Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) ≤
    Nat.card ↑(s ∩ y⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
n : ℕ
J : Box ι
hJ : J ∈ π.filter fun J ↦ N (π.tag J) = n
⊢ ‖μ.real ↑J • f (π.tag J)‖ ≤ μ.real ↑J * ↑n

Tactic:
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 _

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
⊢ rayOfNeZero R x hx = positiveOrientation ∨ rayOfNeZero R x hx = -positiveOrientation

Tactic:
dsimp [positiveOrientation]

Goal state after:
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
⊢ rayOfNeZero R x hx = rayOfNeZero R (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ ∨
    rayOfNeZero R x hx = rayOfNeZero R (-AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯
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:
by
  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.Analysis.PSeries

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

Tactic:
exact add_le_add ihn this

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

Goal state before:
pp: case mpr.ht
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 : ℝ
t : Set D
hcompact : IsCompact t
h : tᶜ ⊆ {x | ‖f x‖ ≤ c}
x : E
hx : ∃ x_1 ∈ tᶜ, f x_1 = x
⊢ ‖x‖ ≤ c

Tactic:
obtain ⟨y, hy, rfl⟩ := hx

Goal state after:
case mpr.ht
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 : ℝ
t : Set D
hcompact : IsCompact t
h : tᶜ ⊆ {x | ‖f x‖ ≤ c}
y : D
hy : y ∈ tᶜ
⊢ ‖f y‖ ≤ c
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ (↑k.succ)⁻¹ - (↑(max k.succ n))⁻¹ ≤ (↑k + 1)⁻¹

Tactic:
· simp only [Nat.cast_succ, sub_le_self_iff, inv_nonneg, Nat.cast_nonneg]

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

Goal state before:
pp: α : Type u
l : List α
d : α
⊢ (Function.Surjective fun x ↦ l.getD x d) ↔ ∀ (x : α), x = d ∨ x ∈ l

Tactic:
apply forall_congr'
  have : ∃ x, l.length ≤ x := ⟨_, Nat.le_refl _⟩
  simp only [getD_eq_getElem?_getD, getD_getElem?, dite_eq_iff, Nat.not_lt, exists_prop, exists_or,
    exists_and_right, this, mem_iff_getElem?, getElem?_eq_some_iff]
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ (∏ x ∈ t, (g x)!) * multinomial s f = (∑ i ∈ t, g i)!

Tactic:
prod_congr_of_eq_on_inter (g := fun a ↦ (f a)!) (s₂ := s) (by aesop)
    (by aesop) (by aesop),

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ (∏ a ∈ s, (f a)!) * multinomial s f = (∑ i ∈ t, g i)!
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
⊢ IsLocalHom (expand p)

Tactic:
by
  refine ⟨fun f hf => ?_⟩
  rw [MvPolynomial.isUnit_iff] at hf ⊢
  simp only [coeff_expand_zero p hp] at hf
  refine ⟨hf.1, fun i hi ↦ ?_⟩
  rw [← coeff_expand_smul p hp]
  apply hf.2
  simp [hi, hp]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial (Fin 0) R
s : Fin 0 → Set R
hs : ∀ (i : Fin 0), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = 0
⊢ p = 0

Tactic:
apply (MvPolynomial.isEmptyRingEquiv R (Fin 0)).injective

Goal state after:
case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial (Fin 0) R
s : Fin 0 → Set R
hs : ∀ (i : Fin 0), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = 0
⊢ (isEmptyRingEquiv R (Fin 0)) p = (isEmptyRingEquiv R (Fin 0)) 0
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro.intro.h.inr.fst
α : 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)
d : α
rd : rα d a
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(b, d)

pp: case intro.intro.h.inr.snd
α : 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)
c : α
rc : rα c b
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(c, a)

Tactic:
· rw [Sym2.eq_swap]
    exact iha d rd ⟨b, hb⟩

Goal state after:
case intro.intro.h.inr.snd
α : 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)
c : α
rc : rα c b
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(c, a)
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case neg
ι : 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)
j : ι
h₁ : ¬(r j i → j ∈ p)
⊢ x₂ j = x j

Tactic:
rw [Classical.not_imp] at h₁

Goal state after:
case neg
ι : 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)
j : ι
h₁ : r j i ∧ j ∉ p
⊢ x₂ j = x j
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
hr : WellFounded (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2)
x : Π₀ (i : ι), α i
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
classical exact Lex.acc hbot hs x fun i _ => hr.apply i

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

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this : (i : ι) → Zero (α i) := fun i ↦ { zero := ⋯.min ⊤ ⋯ }
⊢ WellFounded (Pi.Lex r fun {i} ↦ s i)

Tactic:
have := Fintype.ofFinite ι

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝ : (i : ι) → Zero (α i) := fun i ↦ { zero := ⋯.min ⊤ ⋯ }
this : Fintype ι
⊢ WellFounded (Pi.Lex r fun {i} ↦ s i)
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : Finite ι
inst✝ : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT (α i)
x : (i : ι) → α i
this : (i : ι) → Zero (α i) := fun i ↦ { zero := ⋯.min ⊤ ⋯ }
⊢ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
have := Fintype.ofFinite ι

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : Finite ι
inst✝ : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT (α i)
x : (i : ι) → α i
this✝ : (i : ι) → Zero (α i) := fun i ↦ { zero := ⋯.min ⊤ ⋯ }
this : Fintype ι
⊢ WellFounded fun x1 x2 ↦ x1 < x2
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case right
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
b : R
hmn : m ≤ n
hb : b ∣ a
h : p = (monomial m) b
⊢ p = (monomial m) 1 * C b

Tactic:
rwa [mul_comm, C_mul_monomial, mul_one]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
c : R
⊢ m.leadingCoeff (C c) = c

Tactic:
by
  simp [leadingCoeff]

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

Goal state before:
pp: σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝² : CommSemiring R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : MvPolynomial σ R
h : p ≠ 0 ∧ q ≠ 0
⊢ m.degree (m.leadingTerm p * q) = m.degree (p * q)

Tactic:
simp [leadingTerm, degree_mul, h, degree_monomial]

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 q : MvPolynomial σ R
⊢ m.leadingTerm (p * q) = m.leadingTerm p * m.leadingTerm q

Tactic:
by_cases! h0 : p * q = 0
  · simp [h0, zero_eq_mul.mp]
  simp [leadingTerm, m.degree_mul' h0]

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

Goal state before:
pp: case cons
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
a : α
s : Finset α
haA : a ∉ s
h : m.toWithBotSyn (m.withBotDegree (∑ x ∈ s, f x)) ≤ s.sup fun x ↦ m.toWithBotSyn (m.withBotDegree (f x))
⊢ m.toWithBotSyn (m.withBotDegree (∑ x ∈ Finset.cons a s haA, f x)) ≤
    (Finset.cons a s haA).sup fun x ↦ m.toWithBotSyn (m.withBotDegree (f x))

Tactic:
rw [Finset.sum_cons, Finset.sup_cons]
    exact le_trans (m.withBotDegree_add_le _ _) (max_le_max le_rfl h)

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

Goal state before:
pp: case inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
rcases em' p.Prime with (pp | pp)

Goal state after:
case inr.inl
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

case inr.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: s : Finset ℕ
hs : ∀ p ∈ s, Prime p
⊢ (∏ p ∈ s, p).primeFactors = s

Tactic:
have hn : ∏ p ∈ s, p ≠ 0 := prod_ne_zero_iff.2 fun p hp ↦ (hs _ hp).ne_zero
  ext p
  rw [mem_primeFactors_of_ne_zero hn, and_congr_right (fun hp ↦ hp.prime.dvd_finsetProd_iff _)]
  refine ⟨?_, fun hp ↦ ⟨hs _ hp, _, hp, dvd_rfl⟩⟩
  rintro ⟨hp, q, hq, hpq⟩
  rwa [← ((hs _ hq).dvd_iff_eq hp.ne_one).1 hpq]

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

Goal state before:
pp: case h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ d.primeFactorsPiBij n f hf (f p hp) ≠ d.primeFactorsPiBij n g hg (f p hp)

Tactic:
dsimp only [Nat.primeFactorsPiBij]

Goal state after:
case h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ∏ p ∈ n.primeFactors.attach with f ↑p ⋯ = f p hp, ↑p ≠ ∏ p ∈ n.primeFactors.attach with g ↑p ⋯ = f p hp, ↑p
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
q : ↥n.primeFactors
hp✝ : ↑q ∈ n.primeFactors
hp : Prime ↑q ∧ ↑q ∣ n ∧ n ≠ 0
hfg : f (↑q) hp✝ ≠ g (↑q) hp✝
hq : q ∈ {p ∈ n.primeFactors.attach | g ↑p ⋯ = f (↑q) hp✝}
⊢ False

Tactic:
rw [(mem_filter.mp hq).2] at hfg

Goal state after:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
q : ↥n.primeFactors
hp✝ : ↑q ∈ n.primeFactors
hp : Prime ↑q ∧ ↑q ∣ n ∧ n ≠ 0
hfg : f (↑q) hp✝ ≠ f (↑q) hp✝
hq : q ∈ {p ∈ n.primeFactors.attach | g ↑p ⋯ = f (↑q) hp✝}
⊢ False
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
⊢ limsup s atTop = {ω | Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (s k).indicator (fun x ↦ r) ω) atTop atTop}

Tactic:
by
  nth_rw 1 [← Nat.cofinite_eq_atTop, cofinite.limsup_set_eq]
  ext ω
  rw [mem_ofPred_eq, mem_ofPred_eq, infinite_iff_tendsto_sum_indicator_atTop h, iff_eq_eq]
  congr

Goal state after:
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Field α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ ∀ (x : α), ∃ n, x < ↑n

Tactic:
by_contra! ⟨x, h⟩
    have := csSup_le (range_nonempty Nat.cast)
      (forall_mem_range.2 fun m =>
        le_sub_iff_add_le.2 <| le_csSup ⟨x, forall_mem_range.2 h⟩ ⟨m+1, Nat.cast_succ m⟩)
    linarith

Goal state after:
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
x : α
hx : 0 < x
⊢ ∀ a ∈ cutMap β (x * x), a ≤ (inducedAddHom α β) x * (inducedAddHom α β) x

Tactic:
exact le_inducedMap_mul_self_of_mem_cutMap hx

Goal state after:
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ 2 / ↑(#s) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / ↑(#s)

Tactic:
div_le_div_iff₀ (by positivity) (by positivity),

Goal state after:
case inr
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ 2 * ↑(#s) ≤ (∑ i ∈ s, f i ^ 2) * ↑(#s) ^ 2
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
A : MulArchimedeanClass M
⊢ A ≤ mk 1

Tactic:
induction A using ind with | mk a
     =>  _ 

Goal state after:
case mk
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b a : M
⊢ mk a ≤ mk 1
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h : mk a < mk b
⊢ mk (a / b) = mk a

Tactic:
by
  simpa [h, div_eq_mul_inv] using mk_mul_eq_mk_left (a := a) (b := b⁻¹)

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

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
m n : ℕ
hn : Squarefree n
hmn : m ∣ n
h_zero : f m = 0
⊢ f n = 0

Tactic:
rcases hmn with ⟨k, rfl⟩
  simp only [zero_mul, hf.map_mul_of_coprime (coprime_of_squarefree_mul hn), h_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → ArithmeticFunction R
s : Finset ι
hf : ∀ i ∈ s, (f i).IsMultiplicative
⊢ (∏ i ∈ s, f i).IsMultiplicative

Tactic:
induction s using Finset.cons_induction

Goal state after:
case empty
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → ArithmeticFunction R
hf : ∀ i ∈ ∅, (f i).IsMultiplicative
⊢ (∏ i ∈ ∅, f i).IsMultiplicative

case cons
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → ArithmeticFunction R
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : (∀ i ∈ s✝, (f i).IsMultiplicative) → (∏ i ∈ s✝, f i).IsMultiplicative
hf : ∀ i ∈ cons a✝¹ s✝ h✝, (f i).IsMultiplicative
⊢ (∏ i ∈ cons a✝¹ s✝ h✝, f i).IsMultiplicative