mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
⊢ ∑ k ∈ range (u n), f k ≤ ∑ k ∈ range (u 0), f k + ∑ k ∈ Ico (u 0) (u n), f k

Tactic:
← sum_range_add_sum_Ico _ (hu n.zero_le)

Goal state after:
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 : ℕ
⊢ ∑ k ∈ range (u 0), f k + ∑ k ∈ Ico (u 0) (u n), f k ≤ ∑ k ∈ range (u 0), f k + ∑ k ∈ Ico (u 0) (u n), f k
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
x : E
⊢ x ∈ s → True

Tactic:
implies_true

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ Bornology.IsBounded (range f) ↔ f =O[cocompact D] 1

Tactic:
constructor <;> intro h

Goal state after:
case mp
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h : Bornology.IsBounded (range f)
⊢ f =O[cocompact D] 1

case mpr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h : f =O[cocompact D] 1
⊢ Bornology.IsBounded (range f)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
⊢ ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k) ≤ (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑' (k : ℕ), f k

Tactic:
ENNReal.tsum_eq_iSup_nat' (tendsto_atTop_mono Nat.le_succ tendsto_id)

Goal state after:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
⊢ ⨆ i, ∑ a ∈ range i.succ, (↑(u (a + 1)) - ↑(u a)) * f (u a) ≤ (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑' (k : ℕ), f k
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: 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
⊢ ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ∞ ↔ ∑' (b : ℕ), ↑(f b) = ∞

Tactic:
constructor <;> intro h

Goal state after:
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) = ∞

case mpr
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 : ℕ), ↑(f b) = ∞
⊢ ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ∞
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
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
⊢ (Summable fun k ↦ (↑(u (k + 1)) - ↑(u k)) * f (u k)) ↔ Summable f

Tactic:
lift f to ℕ → ℝ≥0 using h_nonneg
  simp only [NNReal.coe_le_coe] at *
  have (k : ℕ) : (u (k + 1) - (u k : ℝ)) = ((u (k + 1) : ℝ≥0) - (u k : ℝ≥0) : ℝ≥0) := by
    have := Nat.cast_le (α := ℝ≥0).mpr <| (hu_strict k.lt_succ_self).le
    simp [NNReal.coe_sub this]
  simp_rw [this]
  exact_mod_cast NNReal.summable_schlomilch_iff hf h_pos hu_strict hC_nonzero h_succ_diff

Goal state after:
Module: Mathlib.Analysis.PSeries

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

Tactic:
rw [Filter.eventually_atTop] at h_mono

Goal state after:
f : ℕ → ℝ
h_nonneg : ∃ a, ∀ (b : ℕ), a ≤ b → 0 b ≤ f b
h_mono : ∃ a, ∀ (b : ℕ), a ≤ b → f (b + 1) ≤ f b
⊢ (Summable fun k ↦ 2 ^ k * f (2 ^ k)) ↔ Summable f
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
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 ι))⁻¹
aux₃ : (c ^ (↑(card ι))⁻¹)⁻¹ ≠ 0
aux₄ : c ^ (-(↑(card ι))⁻¹) ≠ 0
hc₁ : 0 ≤ c
hc₂ : 0 ≠ c
x✝ : E
⊢ x✝ ∈ {x | x ∈ X ∧ F x ≤ c} → True

Tactic:
implies_true

Goal state after:
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 ι
⊢ finrank ℝ (ι → ℝ) = card ι

Tactic:
finrank_fintype_fun_eq_card

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 ι
⊢ card ι = card ι
Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul

Goal state before:
pp: G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
x✝¹ : G × P
h₁ : x✝¹ ∈ s
x✝ : G × P
h₂ : x✝ ∈ s
h : x✝¹.1 = x✝.1
⊢ x✝¹ = x✝

Tactic:
rw [Finset.mem_coe, mem_smulAntidiagonal_of_group] at h₁ h₂
    aesop

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
xi : ι
xv : M
yi : ι
yv : M
⊢ ((((AddMonoidHom.mul.compr₂ to_hom).comp (singleAddHom xi)) xv).comp (singleAddHom yi)) yv =
    (((((AddMonoidHom.mul.comp to_hom).compl₂ to_hom).comp (singleAddHom xi)) xv).comp (singleAddHom yi)) yv

Tactic:
simp [to_hom, AddMonoidAlgebra.single_mul_single, DirectSum.of_mul_of]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsLeftCancelAdd R
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, n i = 0
⊢ q = p.divMonomial (Finsupp.single i 1)

Tactic:
ext n
  rw [coeff_divMonomial, h, coeff_add, coeff_X_mul, left_eq_add, ← notMem_support_iff]
  intro hn
  simpa using hr _ hn

Goal state after:
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
⊢ X i ∣
    X i * p.divMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) +
      (p.modMonomial (Finsupp.single i 1) * (X i * q.divMonomial (Finsupp.single i 1)) +
        X i * p.divMonomial (Finsupp.single i 1) * (X i * q.divMonomial (Finsupp.single i 1)))

Tactic:
simp only [← mul_assoc, mul_comm _ (X i)]

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

Goal state before:
pp: case cons
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : f ∈ s.piAntidiag p.2
⊢ ↑((f a + p.1 + s.sum f).choose (f a + p.1)) * ↑(multinomial s (f + fun i ↦ if i = a then p.1 else 0)) *
      (f✝ a ^ (f a + p.1) * s.noncommProd (fun i ↦ f✝ i ^ (f i + if i = a then p.1 else 0)) ⋯) =
    ↑(n.choose p.1) * ↑(multinomial s f) * (f✝ a ^ p.1 * s.noncommProd (fun i ↦ f✝ i ^ f i) ⋯)

Tactic:
mem_piAntidiag

Goal state after:
case cons
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ ↑((f a + p.1 + s.sum f).choose (f a + p.1)) * ↑(multinomial s (f + fun i ↦ if i = a then p.1 else 0)) *
      (f✝ a ^ (f a + p.1) * s.noncommProd (fun i ↦ f✝ i ^ (f i + if i = a then p.1 else 0)) ⋯) =
    ↑(n.choose p.1) * ↑(multinomial s f) * (f✝ a ^ p.1 * s.noncommProd (fun i ↦ f✝ i ^ f i) ⋯)
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
⊢ p ∣ X i * q → p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q

pp: case mpr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
⊢ p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q → p ∣ X i * q

Tactic:
· rintro ⟨r, hp⟩
    have : X i ∣ p ∨ X i ∣ r := by simp [← X_dvd_mul_iff, ← hp]
    apply this.symm.imp
    · rintro ⟨r, rfl⟩
      obtain rfl : q = p * r := by rw [← X_mul_cancel_left_iff (i := i), hp, mul_left_comm]
      exact dvd_mul_right p r
    · intro hip
      refine ⟨hip, ?_⟩
      rw [X_dvd_iff_modMonomial_eq_zero] at hip
      rw [← p.modMonomial_add_divMonomial_single i, hip,
        zero_add, mul_assoc, X_mul_cancel_left_iff] at hp
      use r

Goal state after:
case mpr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
⊢ p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q → p ∣ X i * q
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case empty.zero.a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
⊢ ↥(∅.sym 0)

Tactic:
exact ⟨0, by simp [eq_iff_true_of_subsingleton]⟩

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

Goal state before:
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_succ, mul_zero]

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 = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
Module: Mathlib.Data.Nat.Choose.Multinomial

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

Tactic:
simp_rw [← mul_assoc, Nat.cast_comm]

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

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

Tactic:
by rintro rfl _ _; rfl

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
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(a, c)

Tactic:
exact ihb c rc

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

Goal state before:
pp: case insert
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i), x.support = t → (∀ i ∈ t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : x.support = insert b t
h : ∀ i ∈ insert b t, Acc (DFinsupp.Lex r s) (single i (x i))
a : ι
ha : a ∈ t
⊢ Acc (DFinsupp.Lex r s) (single a (x a))

Tactic:
exact h a (Finset.mem_insert_of_mem ha)

Goal state after:
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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
⊢ (∀ i ∈ x.support, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x

Tactic:
by
  generalize ht : x.support = t; revert x
  classical
    induction t using Finset.induction with
    | empty =>
      intro x ht
      rw [support_eq_empty.1 ht]
      exact fun _ => Lex.acc_zero hbot
    | insert b t hb ih =>
      refine fun x ht h => Lex.acc_of_single_erase b (h b <| t.mem_insert_self b) ?_
      refine ih _ (by rw [support_erase, ht, Finset.erase_insert hb]) fun a ha => ?_
      rw [erase_ne (ha.ne_of_notMem hb)]
      exact h a (Finset.mem_insert_of_mem ha)

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
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)]
  simp

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
h : m.toSyn (m.degree (p * q)) < m.toSyn (m.degree (p' * q))
⊢ m.toSyn (m.degree p) < m.toSyn (m.degree p')

Tactic:
wlog! hq : q ≠ 0
  · simp [hq] at h
  apply lt_of_le_of_lt' m.degree_mul_le at h
  simpa [m.degree_mul hp hq] using h

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
⊢ y ∈ (normalizedFactors n).toFinset.powerset.val → x.val.prod = y.val.prod → x = y

Tactic:
hy

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset.val
⊢ x.val.prod = y.val.prod → x = y
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f g : ArithmeticFunction R
⊢ f.pmul g = g.pmul f

Tactic:
ext
  simp [mul_comm]

Goal state after:
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 = n

Tactic:
rw [Nat.eq_pow_of_factorization_eq_single hn0 hn]

Goal state after:
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
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case h
n : ℕ
S : Finset ℕ := ⋯
hSne : S.Nonempty
s : ℕ := ⋯
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * a = (b * x) ^ 2 * y

Tactic:
hy

Goal state after:
case h
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * (x * x * y) = (b * x) ^ 2 * y
Module: Mathlib.Data.Nat.Squarefree

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

Tactic:
by
  rw [_root_.squarefree_mul_iff, Nat.coprime_iff_isRelPrime]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
x y : ℕ
hx : ¬x = 0
⊢ ¬y = 0 →
    x.Coprime y →
      (ArithmeticFunction.prodPrimeFactors f) (x * y) =
        (ArithmeticFunction.prodPrimeFactors f) x * (ArithmeticFunction.prodPrimeFactors f) y

Tactic:
hy

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
⊢ x.Coprime y →
    (ArithmeticFunction.prodPrimeFactors f) (x * y) =
      (ArithmeticFunction.prodPrimeFactors f) x * (ArithmeticFunction.prodPrimeFactors f) y
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

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

Tactic:
simp only [sigma_apply, pow_succ']
  refine (Finset.sum_le_sum fun d hd ↦ Nat.pow_le_pow_left (Nat.divisor_le hd) k).trans ?_
  simpa [Finset.sum_const] using Nat.mul_le_mul_right (n ^ k) (Nat.card_divisors_le_self n)

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ n.primeFactorsList.dedup.length = Ω n ↔ n.primeFactorsList.Nodup

Tactic:
constructor <;> intro h

Goal state after:
case mp
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.dedup.length = Ω n
⊢ n.primeFactorsList.Nodup

case mpr
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.Nodup
⊢ n.primeFactorsList.dedup.length = Ω n
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case mp
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.dedup.length = Ω n
⊢ n.primeFactorsList.Nodup

pp: case mpr
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.Nodup
⊢ n.primeFactorsList.dedup.length = Ω n

Tactic:
· rw [← n.primeFactorsList.dedup_sublist.eq_of_length h]
    apply List.nodup_dedup

Goal state after:
case mpr
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.Nodup
⊢ n.primeFactorsList.dedup.length = Ω n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
⊢ f = g ↔ ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)

Tactic:
constructor <;> intro h

Goal state after:
case mp
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : f = g
⊢ ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)

case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
⊢ f = g
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
⊢ mk a = ⊤ ↔ a = 1

Tactic:
mk_eq_top_iff

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

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
⊢ MonotoneOn mk (Set.Iic 1)

Tactic:
intro a ha b hb hab
  contrapose! hab
  rw [mk_lt_mk] at hab
  obtain h := hab 1
  rw [mabs_eq_inv_self.mpr ha, mabs_eq_inv_self.mpr hb] at h
  simpa using h

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
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (a i) < mk (∏ i ∈ s, a i)
y : ι
⊢ y ∈ Finset.cons i s hi → i ≤ y

Tactic:
hy

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
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
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (a i) < mk (∏ i ∈ s, a i)
y : ι
hy : y ∈ Finset.cons i s hi
⊢ i ≤ y