mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
⊢ f ∈ (MvPolynomial σ R)⁰

Tactic:
rw [← nonZeroDivisorsLeft_eq_nonZeroDivisors, mem_nonZeroDivisorsLeft_iff]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
⊢ ∀ (y : MvPolynomial σ R), f * y = 0 → y = 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case pos
n : ℕ
d2 : 2 ∣ n
d4 : 2 ∣ n / 2
⊢ n.MinSqFacProp (some 2)

Tactic:
exact ⟨prime_two, (dvd_div_iff_mul_dvd d2).1 d4, fun p pp _ => pp.two_le⟩

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

Goal state before:
pp: n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp (some d)
fd : m.minFac ∣ m
⊢ d ≤ m

Tactic:
exact
    le_trans (this.2.2 _ (minFac_prime <| ne_of_gt m2) (dvd_trans (mul_dvd_mul fd fd) md))
      (minFac_le <| lt_of_lt_of_le (by decide) m2)

Goal state after:
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) R
hp : p ≠ 0
S : Finset R
⊢ ↑(#({f ∈ piFinset fun x ↦ S | (eval f) p = 0})) / ↑(#S) ^ n =
    ↑(#({f ∈ piFinset fun x ↦ S | (eval f) p = 0})) / ∏ i, ↑(#S)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
f : ArithmeticFunction ℕ
⊢ ↑(f 0) = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℤ
⊢ ↑(f 0) = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoid R
f g : ArithmeticFunction R
⊢ (⇑f + ⇑g) 0 = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ (if 0 = 1 then ↑n else 0) = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : NegZeroClass R
f : ArithmeticFunction R
⊢ (-⇑f) 0 = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Zero R
inst✝¹ : AddCommMonoid M
inst✝ : SMul R M
f : ArithmeticFunction R
g : ArithmeticFunction M
⊢ ∑ x ∈ divisorsAntidiagonal 0, f x.1 • g x.2 = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction R
⊢ (f * g) 1 = f 1 * g 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
f g : ArithmeticFunction R
⊢ f 0 * g 0 = 0

Tactic:
by simp

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

Goal state before:
pp: ⊢ ζ 1 = 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid S
inst✝ : Module R S
x : R
f : ArithmeticFunction S
⊢ (x • ⇑f) 0 = 0

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ 1 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: n p : ℕ
hn : p ^ n.factorization p ≠ 1
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ p ^ n.factorization p = p ^ n.factorization p

Tactic:
by simp

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

Goal state before:
pp: ⊢ 0 ^ 2 * 1 = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
k : ℕ
⊢ ∑ d ∈ divisors 0, d ^ k = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
⊢ (primeFactorsList 0).length = 0

Tactic:
by simp

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

Goal state before:
pp: ⊢ Ω 0 = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
⊢ (primeFactorsList 0).dedup.length = 0

Tactic:
by simp

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

Goal state before:
pp: ⊢ ω 0 = 0

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (Coprime on f) → ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)
h : (↑(cons a s ha)).Pairwise (Coprime on f)
i : ι
hi : i ∈ s
⊢ a ∈ ↑(cons a s ha)

Tactic:
by simp

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

Goal state before:
pp: d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
⊢ ∃ g, ∃ (hg : g ∈ n.primeFactors.pi fun x ↦ univ), d.primeFactorsPiBij n g hg = t

Tactic:
by
  have existsUnique := fun (p : ℕ) (hp : p ∈ n.primeFactors) =>
    (finMulAntidiag_existsUnique_prime_dvd hn
      (mem_primeFactors_iff_mem_primeFactorsList.mp hp) t ht)
  choose f hf hf_unique using existsUnique
  refine ⟨f, ?_, ?_⟩
  · simp only [mem_pi, mem_univ, forall_true_iff]
  funext i
  have : t i ∣ n := dvd_of_mem_finMulAntidiag ht _
  trans (∏ p ∈ n.primeFactors.attach, if p.1 ∣ t i then p else 1)
  · rw [Nat.primeFactorsPiBij, ← prod_filter]
    congr
    grind
  rw [prod_attach (f := fun p => if p ∣ t i then p else 1), ← Finset.prod_filter]
  rw [primeFactors_filter_dvd_of_dvd hn.ne_zero this]
  exact prod_primeFactors_of_squarefree <| hn.squarefree_of_dvd this

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

Goal state before:
pp: σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝² : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : p₂ ≠ 0
hm1 : ¬(monomial d₁) c₁ = 0
hm2 : ¬(monomial d₂) c₂ = 0
⊢ m.degree p₁ ≤ m.degree p₁ ⊔ m.degree p₂

Tactic:
by simp

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

Goal state before:
pp: σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝² : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : p₂ ≠ 0
hm1 : ¬(monomial d₁) c₁ = 0
hm2 : ¬(monomial d₂) c₂ = 0
⊢ m.degree p₂ ≤ m.degree p₁ ⊔ m.degree p₂

Tactic:
by simp

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

Goal state before:
pp: case e'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) (x * x) = (inducedAddHom α β) (-x * -x)

Tactic:
neg_mul,

Goal state after:
case e'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) (x * x) = (inducedAddHom α β) (-(x * -x))
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) x * (inducedAddHom α β) x = -(inducedAddHom α β) x * -(inducedAddHom α β) x

Tactic:
neg_mul,

Goal state after:
case e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) x * (inducedAddHom α β) x = -((inducedAddHom α β) x * -(inducedAddHom α β) x)
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
⊢ (∑ i ∈ s, f i) ^ (0 + 1) ≤ ↑(#s) ^ 0 * ∑ i ∈ s, f i ^ (0 + 1)

Tactic:
by simp

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

Goal state before:
pp: M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b : M
a : MulArchimedeanOrder M
⊢ |val a|ₘ ≤ |val a|ₘ ^ 1

Tactic:
by simp

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 : M
⊢ |a|ₘ ≤ |a⁻¹|ₘ ^ 1

Tactic:
by simp

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 : M
⊢ |a⁻¹|ₘ ≤ |a|ₘ ^ 1

Tactic:
by simp

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 : M
⊢ |a|ₘ ≤ |(|a|ₘ)|ₘ ^ 1

Tactic:
by simp

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 : M
⊢ |(|a|ₘ)|ₘ ≤ |a|ₘ ^ 1

Tactic:
by simp

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 a : M
⊢ |1|ₘ ≤ |a|ₘ ^ 1

Tactic:
by simp

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
h : |a|ₘ ≤ |b|ₘ
ha : 1 ≤ |a|ₘ
⊢ mk |b|ₘ ≤ mk |a|ₘ

Tactic:
exact mk_antitoneOn ha (ha.trans h) h

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

Goal state before:
pp: case insert.inr.refine_1.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 : ι → β
a : ι
s : Finset ι
has : a ∉ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
hamax : (g ((Equiv.symm σ) a), f ((Equiv.symm σ) a)).1 < (g a, f a).1
⊢ f ((Equiv.symm σ) a) ≤ f a

pp: case insert.inr.refine_1.inr
ι : 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 : ι → β
a : ι
s : Finset ι
has : a ∉ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
hamax :
  (g ((Equiv.symm σ) a), f ((Equiv.symm σ) a)).1 = (g a, f a).1 ∧
    (g ((Equiv.symm σ) a), f ((Equiv.symm σ) a)).2 ≤ (g a, f a).2
⊢ f ((Equiv.symm σ) a) ≤ f a

Tactic:
· exact hfg (mem_insert_of_mem h1s) (mem_insert_self _ _) hamax

Goal state after:
case insert.inr.refine_1.inr
ι : 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 : ι → β
a : ι
s : Finset ι
has : a ∉ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
hamax :
  (g ((Equiv.symm σ) a), f ((Equiv.symm σ) a)).1 = (g a, f a).1 ∧
    (g ((Equiv.symm σ) a), f ((Equiv.symm σ) a)).2 ≤ (g a, f a).2
⊢ f ((Equiv.symm σ) a) ≤ f a
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |y|ₘ ≤ |z|ₘ
⊢ min (mk y) (mk z) ≤ mk (max |y|ₘ |z|ₘ)

pp: case inr
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |z|ₘ ≤ |y|ₘ
⊢ min (mk y) (mk z) ≤ mk (max |y|ₘ |z|ₘ)

Tactic:
· rw [max_eq_right h, min_eq_right, mk_mabs]
    exact mk_le_mk_of_mabs h

Goal state after:
case inr
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |z|ₘ ≤ |y|ₘ
⊢ min (mk y) (mk z) ≤ mk (max |y|ₘ |z|ₘ)
Module: Mathlib.Algebra.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁶ : GeneralizedBooleanAlgebra α
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : Add ι
inst✝² : One ι
inst✝¹ : SuccAddOrder ι
inst✝ : NoMaxOrder ι
f : ι → α
hf : Monotone f
i : ι
⊢ disjointed f (i + 1) = f (i + 1) \ f i

Tactic:
by
  rw [← succ_eq_add_one, hf.disjointed_succ]
  exact not_isMax i

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

Goal state before:
pp: case succ
α : 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 : ℕ
ih : p (f (n + 1) \ (partialSups f) k)
⊢ p (f (n + 1) \ (partialSups f) (k + 1))

Tactic:
| succ k ih =>

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)
⊢ ↑s ⊆ ↑(Finset.cons i s hi)

Tactic:
by simp

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))
⊢ i ∈ ↑(Finset.cons i s hi)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
⊢ 1 1 = 1

Tactic:
by simp

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)
⊢ i ∈ Finset.cons i s hi

Tactic:
by simp

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 : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ i ∈ ↑(Finset.cons i s hi)

Tactic:
by simp

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
s : Finset ι
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
y : ι
hi : y ∉ s
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons y s hi)
hminmem : s.min' hs ∈ Finset.cons y s hi
hne : mk (a y) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a y)
hy : y ∈ Finset.cons y s hi
⊢ y ∈ ↑(Finset.cons y s hi)

Tactic:
by simp

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
s : UpperSet (MulArchimedeanClass M)
⊢ ∀ ⦃b : UpperSet (MulArchimedeanClass M)⦄, s < b → subsemigroup b < subsemigroup s

Tactic:
t

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
⊢ s < t → subsemigroup t < subsemigroup s
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
s : UpperSet (MulArchimedeanClass M)
hs : ¬s = ⊤
⊢ mk 1 ∈ ↑s

Tactic:
obtain ⟨u, hu⟩ := UpperSet.coe_nonempty.mpr hs

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
s : UpperSet (MulArchimedeanClass M)
hs : ¬s = ⊤
u : MulArchimedeanClass M
hu : u ∈ ↑s
⊢ mk 1 ∈ ↑s
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
s : UpperSet (MulArchimedeanClass M)
hs : ¬s = ⊤
u : MulArchimedeanClass M
hu : u ∈ ↑s
⊢ u ≤ ⊤

Tactic:
by simp

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
s : UpperSet (MulArchimedeanClass M)
hs : s ∈ Set.Iio ⊤
⊢ ∀ ⦃b : UpperSet (MulArchimedeanClass M)⦄, b ∈ Set.Iio ⊤ → s < b → subgroup b < subgroup s

Tactic:
t

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : s ∈ Set.Iio ⊤
t : UpperSet (MulArchimedeanClass M)
⊢ t ∈ Set.Iio ⊤ → s < t → subgroup t < subgroup s
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
⊢ ∀ ⦃b : UpperSet (MulArchimedeanClass M)⦄, s ≤ b → subgroup b ≤ subgroup s

Tactic:
t

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
⊢ s ≤ t → subgroup t ≤ subgroup s
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : FloorDiv α β
b : β
⊢ b ⌊/⌋ 0 = 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : CeilDiv α β
b : β
⊢ b ⌈/⌉ 0 = 0

Tactic:
by simp

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
e : MulArchimedeanClass M ≃o MulArchimedeanClass N
⊢ ∀ (a : MulArchimedeanClass M), a ≠ ⊤ ↔ ↑e a ≠ ⊤

Tactic:
by simp

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
e : MulArchimedeanClass M ≃o MulArchimedeanClass N
⊢ ∀ {a b : FiniteMulArchimedeanClass M}, ((↑e).subtypeEquiv ⋯) a ≤ ((↑e).subtypeEquiv ⋯) b ↔ a ≤ b

Tactic:
by simp

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

Goal state before:
pp: n r : ℕ∞
⊢ r ≤ ⌊↑n⌋ₑ ↔ r ≤ n

Tactic:
by simp

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

Goal state before:
pp: n r : ℕ∞
⊢ ⌈↑n⌉ₑ ≤ r ↔ n ≤ r

Tactic:
by simp

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

Goal state before:
pp: r : ℝ≥0∞
⊢ 0 < ⌊r⌋ₑ ↔ 1 ≤ r

Tactic:
by simp

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

Goal state before:
pp: r : ℝ≥0∞
⊢ 0 < ⌈r⌉ₑ ↔ 0 < r

Tactic:
by simp

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
m : ℕ
⊢ ⌊↑m⌋₊ = ↑m

Tactic:
by simp

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
m : ℕ
⊢ ↑(Int.negOfNat m) ≤ 0

Tactic:
by simp

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

Goal state before:
pp: x✝ : ℕ∞
⊢ ⌊∞ + ↑x✝⌋ₑ = ⌊∞⌋ₑ + x✝

Tactic:
by simp

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

Goal state before:
pp: x✝ : ℝ≥0∞
⊢ ⌊x✝ + ↑⊤⌋ₑ = ⌊x✝⌋ₑ + ⊤

Tactic:
by simp

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

Goal state before:
pp: x✝ : ℕ∞
⊢ ⌈∞ + ↑x✝⌉ₑ = ⌈∞⌉ₑ + x✝

Tactic:
by simp

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

Goal state before:
pp: x✝ : ℝ≥0∞
⊢ ⌈x✝ + ↑⊤⌉ₑ = ⌈x✝⌉ₑ + ⊤

Tactic:
by simp

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

Goal state before:
pp: ⊢ ⌊∞ - ↑⊤⌋ₑ = ⌊∞⌋ₑ - ⊤

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ ⌊∞ - ↑↑n⌋ₑ = ⌊∞⌋ₑ - ↑n

Tactic:
by simp

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

Goal state before:
pp: r : ℝ≥0
⊢ ⌊↑r - ↑⊤⌋ₑ = ⌊↑r⌋ₑ - ⊤

Tactic:
by simp

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

Goal state before:
pp: ⊢ ⌈∞ - ↑⊤⌉ₑ = ⌈∞⌉ₑ - ⊤

Tactic:
by simp

Goal state after: