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

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)

Tactic:
obtain ⟨y, hy⟩ := integrable_of_bounded_and_ae_continuous l hb μ hc
  convert! hy
  refine HasIntegral.unique (IntegrableOn.hasBoxIntegral ?_ ⊥ rfl) (HasIntegral.mono hy bot_le)
  constructor
  · let v := {x : (ι → ℝ) | ContinuousAt f x}
    have : AEStronglyMeasurable f (μ.restrict v) :=
      (continuousOn_of_forall_continuousAt fun _ h ↦ h).aestronglyMeasurable
      (measurableSet_of_continuousAt f)
    refine this.mono_measure (Measure.le_iff.2 fun s hs ↦ ?_)
    repeat rw [μ.restrict_apply hs]
    apply le_of_le_of_eq <| μ.mono s.inter_subset_left
    refine measure_eq_measure_of_null_sdiff s.inter_subset_left ?_ |>.symm
    rw [sdiff_self_inter, Set.sdiff_eq, ← nonpos_iff_eq_zero]
    grw [s.inter_subset_right]
    exact hc.le
  · have : IsFiniteMeasure (μ.restrict (Box.Icc I)) :=
      { measure_univ_lt_top := by simp [I.isCompact_Icc.measure_lt_top (μ := μ)] }
    have : IsFiniteMeasure (μ.restrict I) :=
      isFiniteMeasure_of_le _ (μ.restrict_mono Box.coe_subset_Icc le_rfl)
    obtain ⟨C, hC⟩ := hb
    refine .of_bounded (C := C) (Filter.eventually_iff_exists_mem.2 ?_)
    use I, self_mem_ae_restrict I.measurableSet_coe, fun y hy ↦ hC y (I.coe_subset_Icc hy)

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
h_nonneg : 0 ≤ᶠ[Filter.atTop] f
h_mono : ∀ᶠ (k : ℕ) in Filter.atTop, f (k + 1) ≤ f k
⊢ (Summable fun k ↦ 2 ^ k * f (2 ^ k)) ↔ Summable f

Tactic:
rw [Filter.EventuallyLE, Filter.eventually_atTop] at h_nonneg

Goal state after:
f : ℕ → ℝ
h_nonneg : ∃ a, ∀ (b : ℕ), a ≤ b → 0 b ≤ f b
h_mono : ∀ᶠ (k : ℕ) in Filter.atTop, f (k + 1) ≤ f k
⊢ (Summable fun k ↦ 2 ^ k * f (2 ^ k)) ↔ Summable f
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
⊢ ¬Summable ({n | ↑n = k}.indicator fun n ↦ 1 / ↑n)

Tactic:
← summable_nat_add_iff 1

Goal state after:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
⊢ ¬Summable fun n ↦ {n | ↑n = k}.indicator (fun n ↦ 1 / ↑n) (n + 1)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
⊢ ((Summable fun n ↦ 1 / |↑↑n + a| ^ s) ∧ Summable fun n ↦ 1 / |(-(↑(-↑n) + a))| ^ s) ↔ 1 < s

Tactic:
neg_add,

Goal state after:
a s : ℝ
⊢ ((Summable fun n ↦ 1 / |↑↑n + a| ^ s) ∧ Summable fun n ↦ 1 / |-↑(-↑n) + -a| ^ s) ↔ 1 < s
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: case refine_4
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
x y : ℝ
hx : 0 < x
hy : x ≤ y
⊢ ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' (x • {x | x ∈ X ∧ F x ≤ 1}) ⊆
    ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' (y • {x | x ∈ X ∧ F x ≤ 1})

Tactic:
apply Set.image_mono

Goal state after:
case refine_4
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
x y : ℝ
hx : 0 < x
hy : x ≤ y
⊢ x • {x | x ∈ X ∧ F x ≤ 1} ⊆ y • {x | x ∈ X ∧ F x ≤ 1}
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
X : Set (ι → ℝ)
hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : (ι → ℝ) → ℝ
h₁ : ∀ (x : ι → ℝ) ⦃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 {x | x ∈ X ∧ F x ≤ 1}) = 0
inst✝ : Nonempty ι
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq ⋯
b : Basis ι ℤ ↥L := (Free.chooseBasis ℤ ↥L).reindex e
⊢ Tendsto (fun c ↦ ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) atTop
    (𝓝 (volume.real {x | x ∈ X ∧ F x ≤ 1} / covolume L volume))

Tactic:
convert! tendsto_card_le_div'' b hX h₁ h₂ h₃ ?_

Goal state after:
ι : Type u_1
inst✝³ : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
X : Set (ι → ℝ)
hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : (ι → ℝ) → ℝ
h₁ : ∀ (x : ι → ℝ) ⦃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 {x | x ∈ X ∧ F x ≤ 1}) = 0
inst✝ : Nonempty ι
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq ⋯
b : Basis ι ℤ ↥L := (Free.chooseBasis ℤ ↥L).reindex e
⊢ volume.real {x | x ∈ X ∧ F x ≤ 1} / covolume L volume =
    volume.real (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})

ι : Type u_1
inst✝³ : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
X : Set (ι → ℝ)
hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : (ι → ℝ) → ℝ
h₁ : ∀ (x : ι → ℝ) ⦃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 {x | x ∈ X ∧ F x ≤ 1}) = 0
inst✝ : Nonempty ι
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq ⋯
b : Basis ι ℤ ↥L := (Free.chooseBasis ℤ ↥L).reindex e
⊢ volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0
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
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
r : ℝ
hr : r < -↑d
e : (I → ℤ) ≃ₗ[ℤ] ↥L := (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I).symm
u : Finset (I → ℤ)
⊢ ∑ x ∈ u, ‖↑(e x)‖ ^ r ≤ 2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, u ⊆ Fintype.piFinset fun _ : I ↦ Finset.Icc (-n : ℤ) n := by
      obtain ⟨r, hr, hr'⟩ := u.finite_toSet.isCompact.isBounded.subset_closedBall_lt 0 0
      refine ⟨⌊r⌋.toNat, fun x hx ↦ ?_⟩
      have hr'' : ⌊r⌋ ⊔ 0 = ⌊r⌋ := by rw [sup_eq_left]; positivity
      have := hr' hx
      simp only [Metric.mem_closedBall, dist_zero_right, pi_norm_le_iff_of_nonneg hr.le,
        Int.norm_eq_abs, ← Int.cast_abs, ← Int.le_floor] at this
      simpa only [Int.ofNat_toNat, Fintype.mem_piFinset, Finset.mem_Icc, ← abs_le, hr'']

Goal state after:
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
r : ℝ
hr : r < -↑d
e : (I → ℤ) ≃ₗ[ℤ] ↥L := (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I).symm
u : Finset (I → ℤ)
n : ℕ
hn : u ⊆ Fintype.piFinset fun x ↦ Finset.Icc (-↑n) ↑n
⊢ ∑ x ∈ u, ‖↑(e x)‖ ^ r ≤ 2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑' (k : ℕ), ↑k ^ (↑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 := 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
⊢ 1 ≤ -1 * r

Tactic:
simp only [neg_mul, one_mul, le_neg (b := r)]

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
⊢ r ≤ -1
Module: Mathlib.Algebra.MvPolynomial.Coeff

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

Tactic:
zero_pow hsi,

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst✝ : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ (∑ x ∈ s, f x + 1) * (∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)! = (s.sum f + 1) * ((∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)!)

Tactic:
Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum _ _)

Goal state after:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst✝ : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ (∑ x ∈ s, f x + 1) * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!) = (s.sum f + 1) * ((∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)!)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case e'_3.e'_6
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
⊢ (if a✝ ≠ a then count a m else 0) = ((toFinsupp m).update a✝ 0) a

Tactic:
Finsupp.coe_update

Goal state after:
case e'_3.e'_6
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
⊢ (if a✝ ≠ a then count a m else 0) = Function.update (⇑(toFinsupp m)) a✝ 0 a
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mp
σ : 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 ∈ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support, n i = 0

Tactic:
intro n
      contrapose
      intro hn
      classical
      rw [notMem_support_iff, coeff_mul]
      apply Finset.sum_eq_zero
      intro x hx
      simp only [Finset.mem_antidiagonal] at hx
      simp only [← hx, Finsupp.coe_add, Pi.add_apply, Nat.add_eq_zero_iff, not_and_or] at hn
      rcases hn with hn | hn
      · rw [coeff_modMonomial_of_le, zero_mul]
        simpa [← Nat.one_le_iff_ne_zero] using hn
      · rw [mul_comm, coeff_modMonomial_of_le, zero_mul]
        simpa [← Nat.one_le_iff_ne_zero] using hn

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
d : σ →₀ ℕ
r : R
⊢ (expand p) ((monomial d) r) = (monomial (p • d)) r

Tactic:
by
  rw [expand, bind₁_monomial, monomial_eq, Finsupp.prod_of_support_subset _ Finsupp.support_smul]
  · simp [pow_mul]
  · simp

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

Goal state before:
pp: case empty.zero
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
⊢ 0 ^ 0 = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

pp: case empty.succ
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
n : ℕ
⊢ 0 ^ (n + 1) = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
· rw [_root_.pow_zero, Fintype.sum_subsingleton]
      swap
      · exact ⟨0, by simp [eq_iff_true_of_subsingleton]⟩
      convert! (@one_mul R _ _).symm
      convert! @Nat.cast_one R _
      simp

Goal state after:
case empty.succ
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
n : ℕ
⊢ 0 ^ (n + 1) = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
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 ⊤ ⋯ }
this : Fintype ι
⊢ WellFounded (Pi.Lex r fun {i} ↦ s i)

Tactic:
refine InvImage.wf equivFunOnFintype.symm (Lex.wellFounded' (fun i a => ?_) hs ?_)

Goal state after:
case inr.refine_1
ι : 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 ι
i : ι
a : α i
⊢ ¬s i a 0

case inr.refine_2
ι : 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 (Function.swap r)
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
⊢ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
set β := fun i ↦ Antisymmetrization (α i) (· ≤ ·)
    set e : (i : ι) → α i → β i := fun i ↦ toAntisymmetrization (· ≤ ·)
    let _ : ∀ i, Zero (β i) := fun i ↦ ⟨e i 0⟩
    have : WellFounded (DFinsupp.Lex (Function.swap <| @WellOrderingRel ι)
        (fun _ ↦ (· < ·) : (i : ι) → β i → β i → Prop)) := by
      refine Lex.wellFounded' ?_ (fun i ↦ IsWellFounded.wf) ?_
      · rintro i ⟨a⟩
        apply hbot
      · simp +unfoldPartialApp only [Function.swap]
        exact IsWellFounded.wf
    refine Subrelation.wf (fun h => ?_) <| InvImage.wf (mapRange e fun _ ↦ rfl) this
    obtain ⟨i, he, hl⟩ := lex_lt_of_lt_of_preorder (Function.swap WellOrderingRel) h
    exact ⟨i, fun j hj ↦ Quot.sound (he j hj), hl⟩

Goal state after:
Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : LieAdmissibleRing L
⊢ ∀ (x : L), ⁅x, x⁆ = 0

Tactic:
by simp [Ring.lie_def]

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
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ m.Monic (f * g)

Tactic:
by
    rw [Monic, MonomialOrder.leadingCoeff,
      degree_mul_of_mul_leadingCoeff_ne_zero, coeff_mul_of_degree_add, this]
    rw [this]
    exact one_ne_zero

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (r • f)) ≤ m.toSyn (m.degree f)

Tactic:
smul_eq_C_mul

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (C r * f)) ≤ m.toSyn (m.degree f)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : (n / k).MinSqFacProp o
pp : Prime k
dp : k * k ∣ n
⊢ False

Tactic:
contradiction

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

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

Tactic:
contradiction

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 : MvPolynomial σ R
⊢ m.degree f = WithBot.unbotD 0 (m.withBotDegree f)

Tactic:
by_cases h : f = 0 <;> simp [withBotDegree_eq, h]

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

Goal state before:
pp: case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n / 2
⊢ False

Tactic:
contradiction

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

Goal state before:
pp: case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n
⊢ False

Tactic:
contradiction

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

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h0 : f ≠ 0 ∧ g ≠ 0
hf : f ∈ (MvPolynomial σ R)⁰
⊢ f * g ≠ 0

Tactic:
rw [mem_nonZeroDivisors_iff_left] at hf

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h0 : f ≠ 0 ∧ g ≠ 0
hf : ∀ (x : MvPolynomial σ R), f * x = 0 → x = 0
⊢ f * g ≠ 0
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case mpr
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
hn0 : n ≠ 0
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = p ^ k

Tactic:
exact ⟨Nat.prime_of_mem_primeFactors <|
      Finsupp.mem_support_iff.2 (by simp [hn, hk.ne'] : n.factorization p ≠ 0), hk, rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
⊢ dirichletInverseFun f hf 0 = 0

Tactic:
rw [dirichletInverseFun, if_pos rfl]

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

Goal state before:
pp: n : { n // IsPrimePow n }
⊢ (↑n).minFac ^ (↑n).factorization (↑n).minFac = ↑n

Tactic:
n.prop.minFac_pow_factorization_eq

Goal state after:
n : { n // IsPrimePow n }
⊢ ↑n = ↑n
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case pos.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
f : ι → α
g : ι → β
s : Finset ι
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
x : ι
has : x ∉ s
hamax : ∀ x_1 ∈ s, toLex (g x_1, f x_1) ≤ toLex (g x, f x)
hfg : MonovaryOn f g ↑(insert x s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert x s)
τ : Perm ι := Equiv.trans σ (Equiv.swap x (σ x))
hτ : τ = Equiv.trans σ (Equiv.swap x (σ x))
h₁ : σ x = x
hx : ¬σ x = x
⊢ x ∈ ↑s

Tactic:
contradiction

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
h : mk (a i) = mk (a (s.min' hs))
eq : i = s.min' hs
⊢ False

Tactic:
rw [eq] at hi

Goal state after:
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi✝ : i ∉ s
hs : s.Nonempty
hi : s.min' hs ∉ s
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi✝)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi✝
h : mk (a i) = mk (a (s.min' hs))
eq : i = s.min' hs
⊢ False
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
α : Type u_2
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b
a : M
ha : a ≠ 1
⊢ lift f h (mk a ha) = f ⟨a, ha⟩

Tactic:
by simp [lift, mk, ha]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: S : Type u_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : SetLike S G
C : S
inst✝ : GroupConeClass S G
x✝ : PartialOrder G := PartialOrder.mkOfGroupCone C
a b : G
nab : a ≤ b
c : G
⊢ a * c ≤ b * c

Tactic:
by simpa [· ≤ ·] using nab

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
h1 : IsCyclic ↥(Subgroup.zpowers g2)
⊢ Nontrivial ↥(Subgroup.zpowers g2)

Tactic:
exact h'

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ioo_succ_right_eq_Ioc a b

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

Goal state before:
pp: case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ (Function.support fun g ↦ (x.coeff g.1).coeff g.2) ⊆ (fun x ↦ (ofLex x).1) ⁻¹' Function.support x.coeff

Tactic:
support_subset_iff,

Goal state after:
case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ∀ (x_1 : Lex (Γ × Γ')), (x.coeff x_1.1).coeff x_1.2 ≠ 0 → x_1 ∈ (fun x ↦ (ofLex x).1) ⁻¹' Function.support x.coeff
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a b : Γ
r : R
⊢ ((single a) r).coeff b = if b = a then r else 0

Tactic:
split_ifs with h <;> simp [h]

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

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
i : Γ
hi : ↑i < orderTop 0
⊢ coeff 0 i = 0

pp: case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
i : Γ
hi : ↑i < x.orderTop
hx : x ≠ 0
⊢ x.coeff i = 0

Tactic:
· exact coeff_zero

Goal state after:
case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
i : Γ
hi : ↑i < x.orderTop
hx : x ≠ 0
⊢ x.coeff i = 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
⊢ x.leadingCoeff = 0 ↔ x = 0

Tactic:
obtain rfl | hx := eq_or_ne x 0

Goal state after:
case inl
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
⊢ leadingCoeff 0 = 0 ↔ 0 = 0

case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
hx : x ≠ 0
⊢ x.leadingCoeff = 0 ↔ x = 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : 0 < x.order
h : ¬x = 0
⊢ 0 < x.orderTop

Tactic:
exact (zero_lt_orderTop_iff h).mpr hx

Goal state after: