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✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.leadingCoeff g * coeff (m.degree f) f -
      coeff (m.degree f ⊔ m.degree g) ((monomial (m.degree f ⊔ m.degree g - m.degree g)) (m.leadingCoeff f) * g) =
    0

Tactic:
nth_rewrite 1 [← tsub_add_cancel_of_le le_sup_right, coeff_monomial_mul]

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

Goal state before:
pp: n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃! p, Nat.Prime p ∧ p ∣ n

Tactic:
constructor

Goal state after:
case mp
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃! p, Nat.Prime p ∧ p ∣ n

case mpr
n : ℕ
⊢ (∃! p, Nat.Prime p ∧ p ∣ n) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
⊢ IsUnit f ↔ IsUnit (f 1)

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
⊢ IsUnit f → IsUnit (f 1)

case mpr
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
⊢ IsUnit (f 1) → IsUnit f
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k : ℕ
⊢ ζ * pow k = σ k

Tactic:
ext

Goal state after:
k x✝ : ℕ
⊢ (ζ * pow k) x✝ = (σ k) x✝
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag n ↔ ∏ i, f i = n ∧ n ≠ 0

Tactic:
unfold finMulAntidiag

Goal state after:
d n : ℕ
f : Fin d → ℕ
⊢ (f ∈
      if hn : 0 < n then
        map (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }).arrowCongrRight
          (finAntidiagonal d (Additive.ofMul ⟨n, hn⟩))
      else ∅) ↔
    ∏ i, f i = n ∧ n ≠ 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case neg
k n : ℕ
hn0 : ¬n = 0
⊢ (σ k) n = 1 ↔ n = 1

Tactic:
constructor

Goal state after:
case neg.mp
k n : ℕ
hn0 : ¬n = 0
⊢ (σ k) n = 1 → n = 1

case neg.mpr
k n : ℕ
hn0 : ¬n = 0
⊢ n = 1 → (σ k) n = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

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

Tactic:
by
  by_cases hn0 : n = 0
  · aesop
  constructor
  · intro h
    rw [← sigma_zero_eq_one_iff]
    have zero_lt_sigma := sigma_pos 0 n hn0
    have sigma_zero_le_sigma := sigma_mono 0 k n k.zero_le
    lia
  · simp +contextual

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

Goal state before:
pp: case hi
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2) ∧ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)

Tactic:
constructor

Goal state after:
case hi.left
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2)

case hi.right
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x, ∏ i, ↑(x i) = n ∧ (fun i ↦ ↑(x i)) = f) ↔ ∏ i, f i = n ∧ n ≠ 0

Tactic:
constructor

Goal state after:
case pos.mp
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x, ∏ i, ↑(x i) = n ∧ (fun i ↦ ↑(x i)) = f) → ∏ i, f i = n ∧ n ≠ 0

case pos.mpr
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ ∏ i, f i = n ∧ n ≠ 0 → ∃ x, ∏ i, ↑(x i) = n ∧ (fun i ↦ ↑(x i)) = f
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d : ℕ
⊢ d.finMulAntidiag 1 = {fun x ↦ 1}

Tactic:
ext

Goal state after:
d : ℕ
a✝ : Fin d → ℕ
⊢ a✝ ∈ d.finMulAntidiag 1 ↔ a✝ ∈ {fun x ↦ 1}
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
hn : n ≠ 1
⊢ finMulAntidiag 0 n = ∅

Tactic:
ext

Goal state after:
n : ℕ
hn : n ≠ 1
a✝ : Fin 0 → ℕ
⊢ a✝ ∈ finMulAntidiag 0 n ↔ a✝ ∈ ∅
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

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

Tactic:
constructor

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

case mpr
n : ℕ
h0 : n ≠ 0
⊢ n.primeFactorsList.Nodup → n.primeFactorsList.dedup.length = Ω n
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag m ↔ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i, f i = m

Tactic:
constructor

Goal state after:
case mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag m → (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i, f i = m

case mpr
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i, f i = m → f ∈ d.finMulAntidiag m
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ d.finMulAntidiag m = {f ∈ Fintype.piFinset fun x ↦ n.divisors | ∏ i, f i = m}

Tactic:
ext f
  simp only [ne_eq,
    Fintype.mem_piFinset, mem_divisors, mem_filter]
  constructor
  · intro hf
    refine ⟨?_, prod_eq_of_mem_finMulAntidiag hf⟩
    exact fun i => ⟨(dvd_of_mem_finMulAntidiag hf i).trans hmn, hn⟩
  · rw [mem_finMulAntidiag]
    exact fun ⟨_, hprod⟩ => ⟨hprod, ne_zero_of_dvd_ne_zero hn hmn⟩

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

Goal state before:
pp: d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiag n, a i = k) ↔ k ∣ n ∧ ¬n = 0

Tactic:
constructor

Goal state after:
case mp
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiag n, a i = k) → k ∣ n ∧ ¬n = 0

case mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a ∈ d.finMulAntidiag n, a i = k
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: N : ℕ
⊢ {x ∈ Ioc 0 N | ¬x = 0} = Ioc 0 N

Tactic:
ext

Goal state after:
N a✝ : ℕ
⊢ a✝ ∈ {x ∈ Ioc 0 N | ¬x = 0} ↔ a✝ ∈ Ioc 0 N
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case e_s
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
⊢ {x ∈ Ioc 0 N | n * x ≤ N} = Ioc 0 (N / n)

Tactic:
ext

Goal state after:
case e_s
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
a✝ : ℕ
⊢ a✝ ∈ {x ∈ Ioc 0 N | n * x ≤ N} ↔ a✝ ∈ Ioc 0 (N / n)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case e_s
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n a✝¹ : ℕ
hn : 0 < n ∧ n ≤ N
a✝ : 0 < a✝¹
⊢ a✝¹ ≤ N ∧ n * a✝¹ ≤ N ↔ a✝¹ ≤ N / n

Tactic:
constructor

Goal state after:
case e_s.mp
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n a✝¹ : ℕ
hn : 0 < n ∧ n ≤ N
a✝ : 0 < a✝¹
⊢ a✝¹ ≤ N ∧ n * a✝¹ ≤ N → a✝¹ ≤ N / n

case e_s.mpr
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n a✝¹ : ℕ
hn : 0 < n ∧ n ≤ N
a✝ : 0 < a✝¹
⊢ a✝¹ ≤ N / n → a✝¹ ≤ N ∧ n * a✝¹ ≤ N
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: 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 ℕ
⊢ s.Infinite ↔ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k) atTop atTop

Tactic:
constructor

Goal state after:
case mp
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 ℕ
⊢ s.Infinite → Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k) atTop atTop

case mpr
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 ℕ
⊢ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k) atTop atTop → s.Infinite
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
h : ↑q < inducedMap α β a
⊢ ↑q < a

Tactic:
rw [← inducedMap_rat α] at h
    exact (inducedMap_mono α β).reflect_lt h

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_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
⊢ coeff (m.degree (g b)) (g b) + ∑ i ∈ B, coeff (m.degree (g b)) (g i) = 0

Tactic:
rw [← coeff_sum, ← coeff_add, ← notMem_support_iff]

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
⊢ m.degree (g b) ∉ (g b + ∑ x ∈ B, g x).support
Module: Mathlib.Algebra.Order.Archimedean.Submonoid

Goal state before:
pp: M : Type u_1
S : Type u_2
inst✝⁴ : SetLike S M
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : SubmonoidClass S M
inst✝ : MulArchimedean M
H : S
⊢ MulArchimedean ↥H

Tactic:
constructor

Goal state after:
M : Type u_1
S : Type u_2
inst✝⁴ : SetLike S M
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : SubmonoidClass S M
inst✝ : MulArchimedean M
H : S
⊢ ∀ (x : ↥H) {y : ↥H}, 1 < y → ∃ n, x ≤ y ^ 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

Goal state after:
case mp
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)

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

Goal state before:
pp: case insert.inr.refine_2.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 (σ a), f (σ a)).1 = (g a, f a).1 ∧ (g (σ a), f (σ a)).2 ≤ (g a, f a).2
⊢ g (σ a) ≤ g a

Tactic:
· exact hamax.1.le

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → ArithmeticFunction R
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, (f i).IsMultiplicative) → (∏ i ∈ s, f i).IsMultiplicative
hf : ∀ i ∈ cons a s ha, (f i).IsMultiplicative
⊢ (f a * ∏ x ∈ s, f x).IsMultiplicative

Tactic:
exact (hf a (by grind)).mul (by grind)

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

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

Tactic:
exact hk.mul hf

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
⊢ ⊤.closedBallSubgroup = ⊥

Tactic:
ext

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x✝ : M
⊢ x✝ ∈ ⊤.closedBallSubgroup ↔ x✝ ∈ ⊥
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: case inr
K : Type u_2
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a : K
n : ℕ
hn : n > 0
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

Tactic:
nth_rw 2 [← div_mul_cancel₀ (a := a) (b := ↑n) (by positivity)]

Goal state after:
case inr
K : Type u_2
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a : K
n : ℕ
hn : n > 0
⊢ ⌊a / ↑n⌋₊ = ⌊a / ↑n * ↑n⌋₊ / n
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : (i : ι) → AddCommMonoid (π i)
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → SMulZeroClass α (π i)
inst✝ : (i : ι) → CeilDiv α (π i)
a : α
⊢ (fun i ↦ 0 i ⌈/⌉ a) = 0

Tactic:
ext

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : (i : ι) → AddCommMonoid (π i)
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → SMulZeroClass α (π i)
inst✝ : (i : ι) → CeilDiv α (π i)
a : α
x✝ : ι
⊢ 0 x✝ ⌈/⌉ a = 0 x✝
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : FloorDiv α β
f : ι →₀ β
a✝ a : α
⊢ mapRange (fun x ↦ x ⌊/⌋ a) ⋯ 0 = 0

Tactic:
ext

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : FloorDiv α β
f : ι →₀ β
a✝¹ a : α
a✝ : ι
⊢ (mapRange (fun x ↦ x ⌊/⌋ a) ⋯ 0) a✝ = 0 a✝
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : CeilDiv α β
f : ι →₀ β
a✝ a : α
⊢ mapRange (fun x ↦ x ⌈/⌉ a) ⋯ 0 = 0

Tactic:
ext

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : CeilDiv α β
f : ι →₀ β
a✝¹ a : α
a✝ : ι
⊢ (mapRange (fun x ↦ x ⌈/⌉ a) ⋯ 0) a✝ = 0 a✝
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
⊢ ⌊r⌋ₑ = ⊤ ↔ r = ∞

Tactic:
by cases r <;> simp

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

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

Tactic:
by cases r <;> simp

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

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

Tactic:
by cases r <;> simp

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

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

Tactic:
by cases r <;> 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
⊢ subgroup ⊤ = ⊥

Tactic:
ext

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x✝ : M
⊢ x✝ ∈ subgroup ⊤ ↔ x✝ ∈ ⊥
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: R : Type u_3
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : n / d = res
⊢ IsNat ⌊r⌋₊ res

Tactic:
constructor

Goal state after:
R : Type u_3
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : n / d = res
⊢ ⌊r⌋₊ = ↑res
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: R : Type u_3
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
n d : ℕ
hd : Invertible ↑d
⊢ IsNat ⌊↑(Int.negOfNat n) * ⅟↑d⌋₊ 0

Tactic:
constructor

Goal state after:
R : Type u_3
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
n d : ℕ
hd : Invertible ↑d
⊢ ⌊↑(Int.negOfNat n) * ⅟↑d⌋₊ = ↑0
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a : ℝ≥0∞
⊢ toENNReal ⁻¹' Ioi a = Ioi ⌊a⌋ₑ

Tactic:
ext

Goal state after:
a : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ioi a ↔ x✝ ∈ Ioi ⌊a⌋ₑ
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a : ℝ≥0∞
⊢ toENNReal ⁻¹' Iio a = Iio ⌈a⌉ₑ

Tactic:
ext

Goal state after:
a : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Iio a ↔ x✝ ∈ Iio ⌈a⌉ₑ
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a : ℝ≥0∞
⊢ toENNReal ⁻¹' Iic a = Iic ⌊a⌋ₑ

Tactic:
ext

Goal state after:
a : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Iic a ↔ x✝ ∈ Iic ⌊a⌋ₑ
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a : ℝ≥0∞
⊢ toENNReal ⁻¹' Ici a = Ici ⌈a⌉ₑ

Tactic:
ext

Goal state after:
a : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ici a ↔ x✝ ∈ Ici ⌈a⌉ₑ
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Icc a b = Icc ⌈a⌉ₑ ⌊b⌋ₑ

Tactic:
ext

Goal state after:
a b : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Icc a b ↔ x✝ ∈ Icc ⌈a⌉ₑ ⌊b⌋ₑ
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Ico a b = Ico ⌈a⌉ₑ ⌈b⌉ₑ

Tactic:
ext

Goal state after:
a b : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ico a b ↔ x✝ ∈ Ico ⌈a⌉ₑ ⌈b⌉ₑ
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Ioc a b = Ioc ⌊a⌋ₑ ⌊b⌋ₑ

Tactic:
ext

Goal state after:
a b : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ioc a b ↔ x✝ ∈ Ioc ⌊a⌋ₑ ⌊b⌋ₑ
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Ioo a b = Ioo ⌊a⌋ₑ ⌈b⌉ₑ

Tactic:
ext

Goal state after:
a b : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ioo a b ↔ x✝ ∈ Ioo ⌊a⌋ₑ ⌈b⌉ₑ
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Subgroup.zpowers g2 = ⊥
⊢ g1 = g2

Tactic:
rw [h'] at h
    simp_all only [Subgroup.zpowers_eq_bot]

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
x : M
⊢ x ∈ I ↔ ∃ y z, Minimal (fun x ↦ x ∈ I) z ∧ y * z = x

Tactic:
constructor

Goal state after:
case mp
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
x : M
⊢ x ∈ I → ∃ y z, Minimal (fun x ↦ x ∈ I) z ∧ y * z = x

case mpr
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
x : M
⊢ (∃ y z, Minimal (fun x ↦ x ∈ I) z ∧ y * z = x) → x ∈ I
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ range #s
⊢ c - ↑(#s) < c - ↑x ∧ c - ↑x ≤ c

Tactic:
rw [mem_range] at mx

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x < #s
⊢ c - ↑(#s) < c - ↑x ∧ c - ↑x ≤ c
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
⊢ c ≤ c + ↑x ∧ c + ↑x < c + ↑(#s)

Tactic:
rw [mem_range] at mx

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x < #s
⊢ c ≤ c + ↑x ∧ c + ↑x < c + ↑(#s)
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Icc a b) = Icc (a + c) (b + c)

Tactic:
add_comm _ c

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Icc a b) = Icc (c + a) (c + b)
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Ico a b) = Ico (a + c) (b + c)

Tactic:
add_comm _ c

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Ico a b) = Ico (c + a) (c + b)
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Ioc a b) = Ioc (a + c) (b + c)

Tactic:
add_comm _ c

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Ioo a b) = Ioo (a + c) (b + c)

Tactic:
add_comm _ c

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a < b
⊢ insert b (Ioc a (b - 1)) = Ioc a b

Tactic:
simpa [pred_eq_sub_one] using insert_Ioc_pred_right_eq_Ioc h

Goal state after: