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 : ℕ → ℕ
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
n k : ℕ
a✝ : k ∈ range n
⊢ (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • (u (k + 1) - u k) • f (u (k + 1))

Tactic:
rw [smul_smul]

Goal state after:
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
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
n k : ℕ
a✝ : k ∈ range n
⊢ (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ (C * (u (k + 1) - u k)) • f (u (k + 1))
Module: Mathlib.Analysis.PSeries

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

Tactic:
· intro _ _ _ _
    exact antitoneOn_nat_Ici_of_succ_le (k := n + m) (by grind) (by simp) (by simp) (by grind)

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun n ↦ (↑n ^ p)⁻¹) ↔ 1 < p

pp: case inr
p : ℝ
hp : p < 0
⊢ (Summable fun n ↦ (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
· rw [← summable_condensed_iff_of_nonneg]
    · simp_rw [Nat.cast_pow, Nat.cast_two, ← rpow_natCast, ← rpow_mul zero_lt_two.le, mul_comm _ p,
        rpow_mul zero_lt_two.le, rpow_natCast, ← inv_pow, ← mul_pow,
        summable_geometric_iff_norm_lt_one]
      nth_rw 1 [← rpow_one 2]
      rw [← division_def, ← rpow_sub zero_lt_two, norm_eq_abs,
        abs_of_pos (rpow_pos_of_pos zero_lt_two _), rpow_lt_one_iff zero_lt_two.le]
      simp
    · intro n
      positivity
    · intro m n hm hmn
      gcongr

Goal state after:
case inr
p : ℝ
hp : p < 0
⊢ (Summable fun n ↦ (↑n ^ p)⁻¹) ↔ 1 < p
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} ∧ x✝ ∈ ↑L ↔
    (Equiv.smulRight aux₄) ((Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv x✝) ∈
        ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1} ∧
      (Equiv.smulRight aux₄) ((Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv x✝) ∈
        (c ^ (↑(card ι))⁻¹)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
LinearEquiv.coe_toEquiv,

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
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} ∧ x✝ ∈ ↑L ↔
    (Equiv.smulRight aux₄) ((Basis.ofZLatticeBasis ℝ L b).equivFun x✝) ∈
        ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1} ∧
      (Equiv.smulRight aux₄) ((Basis.ofZLatticeBasis ℝ L b).equivFun x✝) ∈
        (c ^ (↑(card ι))⁻¹)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst✝¹ : DecidablePred fun x ↦ l₁.getD x 0 ≠ 0
inst✝ : DecidablePred fun x ↦ l₂.getD x 0 ≠ 0
⊢ (l₁ ++ l₂).toFinsupp = l₁.toFinsupp + Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp

Tactic:
by
  ext n
  simp only [toFinsupp_apply, Finsupp.add_apply]
  cases lt_or_ge n l₁.length with
  | inl h =>
    rw [getD_append _ _ _ _ h, Finsupp.embDomain_of_notMem_range, add_zero]
    rintro ⟨k, rfl : length l₁ + k = n⟩
    lia
  | inr h =>
    rcases Nat.exists_eq_add_of_le h with ⟨k, rfl⟩
    rw [getD_append_right _ _ _ _ h, Nat.add_sub_cancel_left, getD_eq_default _ _ h, zero_add]
    exact Eq.symm (Finsupp.embDomain_apply_self _ _ _)

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

Goal state before:
pp: case neg
α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
ha : a ∉ s
⊢ 0! = ∏ x ∈ s, (Pi.single a n x)!

Tactic:
rw [eq_comm, factorial_zero]

Goal state after:
case neg
α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
ha : a ∉ s
⊢ ∏ x ∈ s, (Pi.single a n x)! = 1
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ m i
⊢ coeff m ((expand p) φ) = 0

Tactic:
contrapose! h

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : coeff m ((expand p) φ) ≠ 0
⊢ p ∣ m i
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ m i
⊢ coeff m ((expand p) φ) = 0

Tactic:
classical
  contrapose! h
  grw [← mem_support_iff, support_expand_subset, Finset.mem_image] at h
  rcases h with ⟨a, -, rfl⟩
  exact ⟨a i, by simp⟩

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

Goal state before:
pp: case insert
α : 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)
⊢ ↑(n.choose (Multiset.count a ↑↑m) * (Multiset.filter (fun x ↦ a ≠ x) ↑↑m).countPerms) *
      ((Multiset.replicate (Multiset.count a ↑↑m) (x a)).noncommProd ⋯ *
        (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 ⋯) *
      ↑(n.choose ↑((symInsertEquiv ha) m).fst)

Tactic:
Multiset.noncommProd_eq_pow_card _ _ _ fun _ => Multiset.eq_of_mem_replicate

Goal state after:
case insert
α : 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)
⊢ ↑(n.choose (Multiset.count a ↑↑m) * (Multiset.filter (fun x ↦ a ≠ x) ↑↑m).countPerms) *
      (x a ^ (Multiset.replicate (Multiset.count a ↑↑m) (x a)).card *
        (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 ⋯) *
      ↑(n.choose ↑((symInsertEquiv ha) m).fst)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case insert
α : 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)
⊢ ↑(n.choose (Multiset.count a ↑↑m) * (Multiset.filter (fun x ↦ a ≠ x) ↑↑m).countPerms) *
      (x a ^ (Multiset.replicate (Multiset.count a ↑↑m) (x a)).card *
        (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 ⋯) *
      ↑(n.choose ↑((symInsertEquiv ha) m).fst)

Tactic:
Multiset.card_replicate,

Goal state after:
case insert
α : 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)
⊢ ↑(n.choose (Multiset.count a ↑↑m) * (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 ⋯) *
      ↑(n.choose ↑((symInsertEquiv ha) m).fst)
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
⊢ ((expand p) f).totalDegree = f.totalDegree * p

Tactic:
classical
  rcases p.eq_zero_or_pos with hp | hp
  · simp [hp]
  by_cases hf : f = 0
  · rw [hf, map_zero, totalDegree_zero, zero_mul]
  simp_rw [totalDegree_eq, support_expand _ (p.ne_zero_iff_zero_lt.mpr hp)]
  simp only [Finsupp.card_toMultiset, Finset.sup_image, Finset.sup_mul₀, Function.comp_def]
  congr! 2 with d
  rw [Finsupp.sum_of_support_subset _ Finsupp.support_smul _ (by simp)]
  simp [Finsupp.sum, Finset.sum_mul, mul_comm p]

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

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g q) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) q →
        Polynomial.eval x (eval₂ f g (p + q)) =
          eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p + q)

pp: case mul_X
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g (p * X n)) =
        eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p * X n)

Tactic:
· intro p q hp hq
    simp [hp, hq]

Goal state after:
case mul_X
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g (p * X n)) =
        eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p * X n)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: k : ℕ
m : Multiset ℕ
⊢ (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k

Tactic:
induction k with

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

Goal state before:
pp: case intro
ι : 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)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
⊢ ∀ (a : α i), Acc (DFinsupp.Lex r s) (single i a)

Tactic:
refine fun a => WellFounded.induction (hs i)
    (C := fun x ↦ Acc (DFinsupp.Lex r s) (single i x)) a fun a ha ↦ ?_

Goal state after:
case intro
ι : 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)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → Acc (DFinsupp.Lex r s) (single i y)
⊢ Acc (DFinsupp.Lex r s) (single i a)
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:
exact Lex.acc hbot hs x fun i _ => hr.apply i

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

Goal state before:
pp: case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ m.leadingCoeff f ≠ 0

Tactic:
rw [leadingCoeff, ← mem_support_iff, degree]

Goal state after:
case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ m.toSyn.symm (f.support.sup ⇑m.toSyn) ∈ f.support
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.toSyn (m.degree f) = 0 ↔ f.totalDegree = 0

Tactic:
← m.bot_eq_zero,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree f) = ⊥ ↔ f.totalDegree = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn d ≤ 0 ↔ ∀ (x : σ), d x = 0

Tactic:
← m.bot_eq_zero,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn d ≤ ⊥ ↔ ∀ (x : σ), d x = 0
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: case e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Sym2 α), x ∈ {x ∈ image (uncurry Sym2.mk) (univ ×ˢ univ) | ¬x.IsDiag} ↔ ¬x.IsDiag

Tactic:
rintro x

Goal state after:
case e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ {x ∈ image (uncurry Sym2.mk) (univ ×ˢ univ) | ¬x.IsDiag} ↔ ¬x.IsDiag
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
hq : q ≠ 0
h : m.toSyn (m.degree p) < m.toSyn (m.degree p')
⊢ p' ≠ 0

Tactic:
contrapose! h

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
hq : q ≠ 0
h : p' = 0
⊢ m.toSyn (m.degree p') ≤ m.toSyn (m.degree p)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
⊢ 0 ∉ s.val

Tactic:
intro con

Goal state after:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
con : 0 ∈ s.val
⊢ False
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : Multiset.Rel Associated (normalizedFactors s.val.prod) s.val
⊢ Squarefree s.val.prod

Tactic:
associated_eq_eq,

Goal state after:
case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : Multiset.Rel Eq (normalizedFactors s.val.prod) s.val
⊢ Squarefree s.val.prod
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : normalizedFactors s.val.prod = s.val
⊢ Squarefree s.val.prod

Tactic:
rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors hs0, h]

Goal state after:
case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : normalizedFactors s.val.prod = s.val
⊢ s.val.Nodup
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
hg : ¬g = 0
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
h' : m.degree (f + g) = m.degree f
⊢ ¬f + g = 0

Tactic:
contrapose! h

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : ¬g = 0
h' : m.degree (f + g) = m.degree f
h : f + g = 0
⊢ 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
hg : ¬g = 0
h' : m.degree (f + g) = m.degree f
h : f + g = 0
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g)

Tactic:
simp [← h', h]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
⊢ (f.ppow k).IsMultiplicative

Tactic:
induction k with

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ coeff (m.degree f ⊔ m.degree g) (m.sPolynomial f g) = 0

Tactic:
rw [sPolynomial_def, coeff_sub]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ coeff (m.degree f ⊔ m.degree g) ((monomial (m.degree f ⊔ m.degree g - m.degree f)) (m.leadingCoeff g) * f) -
      coeff (m.degree f ⊔ m.degree g) ((monomial (m.degree f ⊔ m.degree g - m.degree g)) (m.leadingCoeff f) * g) =
    0
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case mpr.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ p ^ n.factorization p = n

Tactic:
apply Nat.dvd_antisymm (Nat.ordProj_dvd _ _)

Goal state after:
case mpr.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ n ∣ p ^ n.factorization p
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ (σ 0) n = 1 ↔ n = 1

Tactic:
simp [sigma_zero_apply]

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

Goal state before:
pp: case neg
d n : ℕ
f : Fin d → ℕ
h : n = 0
⊢ f ∈ ∅ ↔ ∏ i, f i = n ∧ n ≠ 0

Tactic:
simp only [h, notMem_empty, ne_eq, not_true_eq_false, and_false]

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

Goal state before:
pp: case neg
m k : ℕ
hm : ¬m = 0
⊢ Ω (m ^ k) = k * Ω m

Tactic:
induction k with

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

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
⊢ ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2 = ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n, f x.1 * g x.2

Tactic:
simp only [mem_Ioc] at hn

Goal state after:
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : 0 < n ∧ n ≤ N
⊢ ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2 = ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n, f x.1 * g x.2
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : ↑t ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds ↑t
⊢ n' • r ≤ ∑ k ∈ Finset.range (m + 1), s.indicator (fun x ↦ r) k

Tactic:
← t_s

Goal state after:
case h
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : ↑t ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds ↑t
⊢ n' • r ≤ ∑ k ∈ Finset.range (m + 1), (↑t).indicator (fun x ↦ r) k
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
x y : α
⊢ sSup (cutMap β (x + y)) = inducedMap α β x + inducedMap α β y

Tactic:
cutMap_add

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
x y : α
⊢ sSup (cutMap β x + cutMap β y) = inducedMap α β x + inducedMap α β y
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
this : -∑ i ∈ B, m.leadingCoeff (g i) = m.leadingCoeff (g b)
⊢ ∑ b ∈ B, g b + g b = ∑ x ∈ B, g x + -(((∑ i ∈ B, m.leadingCoeff (g i)) * ↑isunit_gb.unit⁻¹) • g b)

Tactic:
← neg_smul,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
this : -∑ i ∈ B, m.leadingCoeff (g i) = m.leadingCoeff (g b)
⊢ ∑ b ∈ B, g b + g b = ∑ x ∈ B, g x + -((∑ i ∈ B, m.leadingCoeff (g i)) * ↑isunit_gb.unit⁻¹) • g b
Module: Mathlib.Algebra.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
k : ℕ
⊢ p (f (n + 1) \ (partialSups f) k)

Tactic:
induction k with

Goal state after: