mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Coeff

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

Tactic:
_

Goal state after:
case h₀
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
b✝ : σ → ℕ
a✝² : a.support.sum b✝ = n
a✝¹ : ∀ (i : σ), ¬b✝ i = 0 → ¬a i = 0
a✝ : ¬b✝ = ⇑s
⊢ (s = indicator a.support fun i x ↦ b✝ i) → ↑(Nat.multinomial a.support b✝) * ∏ x ∈ a.support, a x ^ b✝ x = 0
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ →₀ ℕ
⊢ (False ∨ i ≤ j) ∧ 1 ∣ 1 ↔ i ≤ j

Tactic:
false_or,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ →₀ ℕ
⊢ i ≤ j ∧ 1 ∣ 1 ↔ i ≤ j
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
P : MvPolynomial σ R
inst✝ : Finite σ
this : Fintype σ
α β : Type u_1
⊢ ∀ [Fintype β] (e : α ≃ β),
    (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
      ∀ (x : MvPolynomial β R), IsNilpotent x ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i x)

Tactic:
_

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
P : MvPolynomial σ R
inst✝¹ : Finite σ
this : Fintype σ
α β : Type u_1
inst✝ : Fintype β
⊢ ∀ (e : α ≃ β),
    (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
      ∀ (x : MvPolynomial β R), IsNilpotent x ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i x)
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
P : MvPolynomial σ R
inst✝ : Finite σ
this : Fintype σ
α : Type u_1
⊢ ∀ [Fintype α],
    (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
      ∀ (x : MvPolynomial (Option α) R), IsNilpotent x ↔ ∀ (i : Option α →₀ ℕ), IsNilpotent (coeff i x)

Tactic:
_

Goal state after:
case refine_3
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
P : MvPolynomial σ R
inst✝¹ : Finite σ
this : Fintype σ
α : Type u_1
inst✝ : Fintype α
⊢ (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
    ∀ (x : MvPolynomial (Option α) R), IsNilpotent x ↔ ∀ (i : Option α →₀ ℕ), IsNilpotent (coeff i x)
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
P : MvPolynomial σ R
⊢ IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i P)

Tactic:
obtain ⟨n, f, hf, P, rfl⟩ := P.exists_fin_rename
  rw [IsNilpotent.map_iff (rename_injective _ hf), MvPolynomial.isNilpotent_iff_of_fintype]
  lift f to Fin n ↪ σ using hf
  refine ⟨fun H i ↦ ?_, fun H i ↦ by simpa using H (i.embDomain f)⟩
  by_cases H : i ∈ Set.range (Finsupp.embDomain f)
  · aesop
  · rw [coeff_rename_eq_zero] <;> aesop (add simp Finsupp.embDomain_eq_mapDomain)

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

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
P : MvPolynomial σ R
x✝ : IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
h₁ : IsUnit (coeff 0 P)
h₂ : ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
⊢ IsUnit P

Tactic:
have : IsNilpotent (P - C (P.coeff 0)) := by
      simp +contextual [isNilpotent_iff, apply_ite, eq_comm, h₂]
    simpa using this.isUnit_add_right_of_commute (h₁.map C) (.all _ _)

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
a₁✝ : α
⊢ ∀ {b₁ : β} {a₂ : α} {b₂ : β}, rα a₁✝ a₂ → rβ b₁ b₂ → Relation.TransGen (GameAdd rα rβ) (a₁✝, b₁) (a₂, b₂)

Tactic:
_

Goal state after:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
a₁✝ : α
b₁✝ : β
⊢ ∀ {a₂ : α} {b₂ : β}, rα a₁✝ a₂ → rβ b₁✝ b₂ → Relation.TransGen (GameAdd rα rβ) (a₁✝, b₁✝) (a₂, b₂)
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
a₁✝ : α
b₁✝ : β
⊢ ∀ {a₂ : α} {b₂ : β}, rα a₁✝ a₂ → rβ b₁✝ b₂ → Relation.TransGen (GameAdd rα rβ) (a₁✝, b₁✝) (a₂, b₂)

Tactic:
_

Goal state after:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
a₁✝ : α
b₁✝ : β
a₂✝ : α
⊢ ∀ {b₂ : β}, rα a₁✝ a₂✝ → rβ b₁✝ b₂ → Relation.TransGen (GameAdd rα rβ) (a₁✝, b₁✝) (a₂✝, b₂)
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
a₁✝ : α
b₁✝ : β
a₂✝ : α
⊢ ∀ {b₂ : β}, rα a₁✝ a₂✝ → rβ b₁✝ b₂ → Relation.TransGen (GameAdd rα rβ) (a₁✝, b₁✝) (a₂✝, b₂)

Tactic:
_

Goal state after:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
a₁✝ : α
b₁✝ : β
a₂✝ : α
b₂✝ : β
⊢ rα a₁✝ a₂✝ → rβ b₁✝ b₂✝ → Relation.TransGen (GameAdd rα rβ) (a₁✝, b₁✝) (a₂✝, b₂✝)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: m : Multiset ℕ
l l' : List ℕ
h : (List.isSetoid ℕ) l l'
⊢ l.multinomial = l'.multinomial

Tactic:
by
  induction h with
  | nil => simp
  | @cons x l l' hl hl' => simp [List.multinomial_cons, hl', hl.sum_nat]
  | @swap x y l =>
    simp only [List.multinomial_cons, ← mul_assoc, List.sum_cons]
    rw [← Nat.choose_symm (Nat.le_add_right y _), add_tsub_cancel_left]
    rw [add_left_comm, Nat.choose_mul (Nat.le_add_right _ _), add_tsub_cancel_left]
    simp [← Nat.choose_symm (Nat.le_add_right _ _), add_tsub_cancel_left]
  | @trans l l' l'' h h' ih ih' => rw [ih, ih']

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

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

Tactic:
if_neg hp

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x₂ i) (x₂ i)
hi : r i i
⊢ s i (x₂ i) (x₂ i)
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a✝ : α
⊢ ∀ ⦃b : α⦄, a✝ < b → (fun a ↦ toDegLex (single a 1)) b < (fun a ↦ toDegLex (single a 1)) a✝

Tactic:
_

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ : α
⊢ a✝ < b✝ → (fun a ↦ toDegLex (single a 1)) b✝ < (fun a ↦ toDegLex (single a 1)) a✝
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case mpr.inr
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
hb : b ∣ r
hp : p = b • (monomial (Finsupp.single i 1)) 1
⊢ ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b

Tactic:
use Finsupp.single i 1, le_rfl, hb

Goal state after:
case right
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
hb : b ∣ r
hp : p = b • (monomial (Finsupp.single i 1)) 1
⊢ p = (monomial (Finsupp.single i 1)) b
Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : Sym (↥s) n
a : ↥s
⊢ ↑((s.finsuppAntidiagEquiv n).symm f) ↑a = Multiset.count a ↑f

Tactic:
by
  simp [finsuppAntidiagEquiv]

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : ↥(s.finsuppAntidiag n)
a : ↥s
⊢ Multiset.count a ↑((s.finsuppAntidiagEquiv n) f) = ↑f ↑a

Tactic:
by
  simp [finsuppAntidiagEquiv]

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

Goal state before:
pp: case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)
⊢ m.toSyn (m.degree (f ^ n * f)) ≤ m.toSyn (n • m.degree f + m.degree f)

Tactic:
apply le_trans m.degree_mul_le

Goal state after:
case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)
⊢ m.toSyn (m.degree (f ^ n) + m.degree f) ≤ m.toSyn (n • m.degree f + m.degree f)
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ ↑(#(S 0) * #({r ∈ piFinset (tail S) | (eval r) pₖ = 0})) / (↑(#(S 0)) * ∏ i, ↑(#(S i.succ))) =
    ↑(#(S 0)) * ↑(#({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ = 0})) / (↑(#(S 0)) * ∏ i, ↑(#(S i.succ)))

Tactic:
tail_def

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ ↑(#(S 0) * #({r ∈ piFinset fun k ↦ S k.succ | (eval r) pₖ = 0})) / (↑(#(S 0)) * ∏ i, ↑(#(S i.succ))) =
    ↑(#(S 0)) * ↑(#({xₜ ∈ piFinset fun i ↦ (fun k ↦ S k.succ) i | (eval xₜ) pₖ = 0})) /
      (↑(#(S 0)) * ∏ i, ↑(#(S i.succ)))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
⊢ Squarefree n

Tactic:
rw [squarefree_iff_nodup_primeFactorsList hn, List.nodup_iff_count_le_one]

Goal state after:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
⊢ ∀ (a : ℕ), List.count a n.primeFactorsList ≤ 1
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
⊢ Squarefree n

Tactic:
rw [squarefree_iff_nodup_primeFactorsList hn, List.nodup_iff_count_le_one]
  intro a
  rw [primeFactorsList_count_eq]
  apply hn'

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
hq : q ≠ 0
h : m.toSyn (m.degree p) < m.toSyn (m.degree p')
⊢ m.toSyn (m.degree (p * q)) < m.toSyn (m.degree (p' * q))

Tactic:
simpa [m.degree_mul hp hq, m.degree_mul (show p' ≠ 0 by contrapose! h; simp [h]) hq] using h

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

Goal state before:
pp: case neg
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
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
dk : ¬k ∣ n
⊢ n.MinSqFacProp (n.minSqFacAux (k + 2))

Tactic:
exact IH n (dvd_refl _) dk

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

Goal state before:
pp: case h
a : ℕ
hsq : Squarefree a
b : ℕ
h0✝ h0 : a * b ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a

Tactic:
mul_ne_zero_iff

Goal state after:
case h
a : ℕ
hsq : Squarefree a
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: f : ArithmeticFunction ℕ
⊢ ζ * f = f * ζ

Tactic:
rw [← natCoe_nat ζ, coe_zeta_mul_comm]

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
h₁ : m.degree f = 0
h₂ : m.degree g = 0
this : C (m.leadingCoeff g) * f - C (m.leadingCoeff f) * g = 0
⊢ m.sPolynomial f g = 0

Tactic:
simp_all [sPolynomial_def]

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

Goal state before:
pp: case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ f (g a✝ * ∏ x ∈ s✝, g x) = f (g a✝) * ∏ x ∈ s✝, f (g x)

Tactic:
hf.map_mul_of_coprime,

Goal state after:
case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ f (g a✝) * f (∏ x ∈ s✝, g x) = f (g a✝) * ∏ x ∈ s✝, f (g x)

case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ (g a✝).gcd (∏ x ∈ s✝, g x) = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ Ω (m * n) = Ω m + Ω n

Tactic:
by
  rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
    UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
    Multiset.card_add, Multiset.coe_card, Multiset.coe_card]

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

Goal state before:
pp: d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
⊢ d.primeFactorsPiBij n f hf ∈ d.finMulAntidiag n

Tactic:
rw [mem_finMulAntidiag]
  refine ⟨?_, hn.ne_zero⟩
  unfold Nat.primeFactorsPiBij
  rw [prod_fiberwise_of_maps_to, prod_attach (f := fun x => x)]
  · apply prod_primeFactors_of_squarefree hn
  · apply fun _ _ => mem_univ _

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

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
⊢ ∀ᶠ (n : ℕ) in atTop, ∑ k ∈ Finset.range n, s.indicator (fun x ↦ a) k = Nat.card ↑s • a

Tactic:
Nat.card_eq_card_finite_toFinset hs,

Goal state after:
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
⊢ ∀ᶠ (n : ℕ) in atTop, ∑ k ∈ Finset.range n, s.indicator (fun x ↦ a) k = #hs.toFinset • a
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
ha : a ≠ 1
⊢ mk a ≤ mk b ↔ ∃ n, |b|ₘ < |a|ₘ ^ n

Tactic:
by
  refine ⟨fun ⟨n, hn⟩ ↦ ⟨n + 1, hn.trans_lt ?_⟩, fun ⟨n, hn⟩ ↦ ?_⟩
  · rw [pow_succ]
    exact lt_mul_of_one_lt_right' _ (one_lt_mabs.mpr ha)
  · exact ⟨n, hn.le⟩

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
p : ℕ
⊢ p ∈ x.primeFactors ∪ y.primeFactors →
    f (p ^ (x.lcm y).factorization p) * f (p ^ (x.gcd y).factorization p) =
      f (p ^ x.factorization p) * f (p ^ y.factorization p)

Tactic:
_

Goal state after:
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
p : ℕ
a✝ : p ∈ x.primeFactors ∪ y.primeFactors
⊢ f (p ^ (x.lcm y).factorization p) * f (p ^ (x.gcd y).factorization p) =
    f (p ^ x.factorization p) * f (p ^ y.factorization p)
Module: Mathlib.Algebra.Order.Field.Pi

Goal state before:
pp: case intro
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case intro.inl
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

case intro.inr
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : Nonempty ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ : MulArchimedeanClass M
⊢ ∀ ⦃b : MulArchimedeanClass M⦄, a✝ ≤ b → b.ballSubgroup ≤ a✝.ballSubgroup

Tactic:
_

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : MulArchimedeanClass M
⊢ a✝ ≤ b✝ → b✝.ballSubgroup ≤ a✝.ballSubgroup
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
α : Type u_2
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b
x✝ : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : ¬a = 1
hb : b = 1
⊢ MulArchimedeanClass.mk a = ⊤

Tactic:
apply hb ▸ 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
a b : M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
s : UpperSet (FiniteMulArchimedeanClass M)
⊢ ∀ {x : M},
    x ∈ (MulArchimedeanClass.subsemigroup (toUpperSetMulArchimedeanClass s)).carrier →
      x⁻¹ ∈ (MulArchimedeanClass.subsemigroup (toUpperSetMulArchimedeanClass s)).carrier

Tactic:
by simp [MulArchimedeanClass.subsemigroup]

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

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌈r + ↑n⌉₊ = ⌈r⌉₊ + n

Tactic:
exact Nat.ceil_add_natCast zero_le _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ¬S ⊆ {⊥}
⊢ (⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.1, ⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.2).1 ≤
    (⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.1, ⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.2).2

Tactic:
obtain ⟨s, hs, ha⟩ := not_subset.1 h
          lift s to NonemptyInterval α using ha
          exact iInf₂_le_of_le s hs (le_iSup₂_of_le s hs s.fst_le_snd)

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

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
⊢ (if h : x✝ ⊆ {⊥} then ⊥
    else ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }) ∈
    upperBounds x✝

Tactic:
intro s ha

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ x✝
⊢ s ≤
    if h : x✝ ⊆ {⊥} then ⊥
    else ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
⊢ (if h : x✝ ⊆ {⊥} then ⊥
    else ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }) ∈
    lowerBounds (upperBounds x✝)

Tactic:
intro s ha

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ upperBounds x✝
⊢ (if h : x✝ ⊆ {⊥} then ⊥
    else ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }) ≤
    s
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case none
ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s t : Interval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
⊢ - -none = none

Tactic:
first | rfl | exact congr_arg WithBot.some (neg_neg _)

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

Goal state before:
pp: case some
ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s✝ t : Interval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ - -some s = some s

Tactic:
first | rfl | exact congr_arg WithBot.some (neg_neg _)

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

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
⊢ (if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ }
    else ⊥) ∈
    lowerBounds s₁

Tactic:
intro s ha

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ s₁
⊢ (if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ }
    else ⊥) ≤
    s
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
⊢ (if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ }
    else ⊥) ∈
    upperBounds (lowerBounds s₁)

Tactic:
intro s ha

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ lowerBounds s₁
⊢ s ≤
    if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ }
    else ⊥