mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
i : Fin 3
⊢ a i = b i

Tactic:
;

Goal state after:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
i : Fin 3
⊢ a i = b i
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := ⋯
a : Fin (succ 0).succ.succ → ℕ := ⋯
ha : a ∈ finMulAntidiag 3 n
⊢ ∃ (ha : a ∈ finMulAntidiag 3 n), f a ha = b

Tactic:
;

Goal state after:
case h
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := ⋯
a : Fin (succ 0).succ.succ → ℕ := ⋯
ha : a ∈ finMulAntidiag 3 n
⊢ ∃ (ha : a ∈ finMulAntidiag 3 n), f a ha = b
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ #({p ∈ n.divisors ×ˢ n.divisors | p.1.lcm p.2 = n}) = 3 ^ ω n

Tactic:
by
  rw [← card_finMulAntidiag_of_squarefree hn, eq_comm]
  apply Finset.card_bij f (f_img hn) f_inj (f_surj hn.ne_zero)

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁹ : Field α✝
inst✝⁸ : LinearOrder α✝
inst✝⁷ : Field β✝
inst✝⁶ : LinearOrder β✝
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : f x ≠ g x
h : f x < g x
q : ℚ
hf : f x < f ↑q
hg : ↑q < g x
⊢ False

Tactic:
← map_ratCast g

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
inst✝⁹ : Field α✝
inst✝⁸ : LinearOrder α✝
inst✝⁷ : Field β✝
inst✝⁶ : LinearOrder β✝
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : f x ≠ g x
h : f x < g x
q : ℚ
hf : f x < f ↑q
hg : g ↑q < g x
⊢ False
Module: Mathlib.Algebra.Order.Archimedean.Hom

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : α →+*o α
x : α
⊢ (OrderRingHom.id α) x = x

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : α →+*o α
x : α
⊢ (OrderRingHom.id α) x = x
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 = #hs.toFinset • a

Tactic:
← sum_eq_card_nsmul key,

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 = ∑ a_1 ∈ hs.toFinset, s.indicator (fun x ↦ a) a_1
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

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

Tactic:
tendsto_congr' (sum_indicator_eventually_eq_card r hs),

Goal state after:
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 ℕ
hs : s.Finite
⊢ ¬Tendsto (fun x ↦ Nat.card ↑s • r) atTop atTop
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ ↑(qa + qb) = ↑qa + ↑qb

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ ↑(qa + qb) = ↑qa + ↑qb
Module: Mathlib.Algebra.Order.CompleteField

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

Tactic:
by
  refine (image_subset_iff.2 fun q hq => ?_).antisymm ?_
  · rw [mem_ofPred_eq, ← sub_lt_iff_lt_add] at hq
    obtain ⟨q₁, hq₁q, hq₁ab⟩ := exists_rat_btwn hq
    refine ⟨q₁, by rwa [coe_mem_cutMap_iff], q - q₁, ?_, add_sub_cancel _ _⟩
    norm_cast
    rw [coe_mem_cutMap_iff]
    exact mod_cast sub_lt_comm.mp hq₁q
  · rintro _ ⟨_, ⟨qa, ha, rfl⟩, _, ⟨qb, hb, rfl⟩, rfl⟩
    -- After https://github.com/leanprover/lean4/pull/2734, `norm_cast` needs help with beta reduction.
    refine ⟨qa + qb, ?_, by beta_reduce; norm_cast⟩
    rw [mem_ofPred_eq, cast_add]
    exact add_lt_add ha hb

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Hom

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedAddMonoid R
inst✝³ : Ring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedAddMonoid S
inst✝ : PosMulMono S
hR : ∀ (r : R), 0 ≤ r → IsSquare r
f : R →+* S
s : R
h : 0 ≤ s * s
⊢ 0 ≤ f (s * s)

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedAddMonoid R
inst✝³ : Ring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedAddMonoid S
inst✝ : PosMulMono S
hR : ∀ (r : R), 0 ≤ r → IsSquare r
f : R →+* S
s : R
h : 0 ≤ s * s
⊢ 0 ≤ f (s * s)
Module: Mathlib.Algebra.Order.Archimedean.Real.Hom

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedAddMonoid R
inst✝³ : Ring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedAddMonoid S
inst✝ : PosMulMono S
hR : ∀ (r : R), 0 ≤ r → IsSquare r
f : R →+* S
s : R
h : 0 ≤ s * s
⊢ 0 ≤ f s * f s

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedAddMonoid R
inst✝³ : Ring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedAddMonoid S
inst✝ : PosMulMono S
hR : ∀ (r : R), 0 ≤ r → IsSquare r
f : R →+* S
s : R
h : 0 ≤ s * s
⊢ 0 ≤ f s * f s
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: 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
i : ℕ
⊢ f (i ^ 0) = 1

Tactic:
;

Goal state after:
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
i : ℕ
⊢ f (i ^ 0) = 1
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
N : Type u_3
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
⊢ Monotone fun a ↦ of (f (val a))

Tactic:
rintro a b ⟨n, hn⟩
    simp_rw [le_def, val_of, ← map_mabs, ← map_pow]
    exact ⟨n, OrderHomClass.monotone f hn⟩

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

Goal state before:
pp: case 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✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ⇑σ) x < (g ∘ ⇑σ) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
hτs : {x | τ x ≠ x} ⊆ ↑s
hxy : x ≠ y
z : ι
hz : z ≠ y ∧ z ≠ x ∧ z ∈ s
⊢ f z • g (σ z) = f z • g (σ ((Equiv.swap x y) z))

Tactic:
rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]

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

Goal state before:
pp: case refine_3
ι : 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✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ⇑σ) g ↑s
⊢ MonovaryOn f (g ∘ ⇑σ⁻¹) ↑s

Tactic:
convert! h.comp_right σ.symm

Goal state after:
case e'_6
ι : 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✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ⇑σ) g ↑s
⊢ f = (f ∘ ⇑σ) ∘ ⇑(Equiv.symm σ)

case e'_8
ι : 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✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ⇑σ) g ↑s
⊢ ↑s = ⇑(Equiv.symm σ) ⁻¹' ↑s
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 : ι) → FloorDiv α (π i)
a : α
ha : a ≤ 0
f : (i : ι) → π i
i : ι
⊢ f i ⌊/⌋ a = 0 i

Tactic:
;

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 : ι) → FloorDiv α (π i)
a : α
ha : a ≤ 0
f : (i : ι) → π i
i : ι
⊢ f i ⌊/⌋ a = 0 i
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 : ι) → FloorDiv α (π i)
a : α
i : ι
⊢ 0 i ⌊/⌋ a = 0 i

Tactic:
;

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 : ι) → FloorDiv α (π i)
a : α
i : ι
⊢ 0 i ⌊/⌋ a = 0 i
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 : α
ha : a ≤ 0
f : (i : ι) → π i
i : ι
⊢ f i ⌈/⌉ a = 0 i

Tactic:
;

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 : α
ha : a ≤ 0
f : (i : ι) → π i
i : ι
⊢ f i ⌈/⌉ a = 0 i
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 : α
x✝ : ι
⊢ 0 x✝ ⌈/⌉ a = 0 x✝

Tactic:
;

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.Semifield

Goal state before:
pp: case hbc
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ a < ↑⌊a⌋₊ + 1

Tactic:
;

Goal state after:
case hbc
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ a < ↑⌊a⌋₊ + 1
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 : α
ha : a ≤ 0
f : ι →₀ β
i : ι
⊢ (mapRange (fun x ↦ x ⌊/⌋ a) ⋯ f) i = 0 i

Tactic:
;

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 : α
ha : a ≤ 0
f : ι →₀ β
i : ι
⊢ (mapRange (fun x ↦ x ⌊/⌋ a) ⋯ f) i = 0 i
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 : α
a✝ : ι
⊢ (mapRange (fun x ↦ x ⌊/⌋ a) ⋯ 0) a✝ = 0 a✝

Tactic:
;

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 : α
ha : a ≤ 0
f : ι →₀ β
i : ι
⊢ (mapRange (fun x ↦ x ⌈/⌉ a) ⋯ f) i = 0 i

Tactic:
;

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 : α
ha : a ≤ 0
f : ι →₀ β
i : ι
⊢ (mapRange (fun x ↦ x ⌈/⌉ a) ⋯ f) i = 0 i
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 : α
a✝ : ι
⊢ (mapRange (fun x ↦ x ⌈/⌉ a) ⋯ 0) a✝ = 0 a✝

Tactic:
;

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.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ 0 < b

Tactic:
;

Goal state after:
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ 0 < b
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ b - 1 ≠ 0

Tactic:
;

Goal state after:
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ b - 1 ≠ 0
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ 2⁻¹ * a < ↑⌊a⌋₊

Tactic:
;

Goal state after:
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ 2⁻¹ * a < ↑⌊a⌋₊
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x✝ : M
⊢ x✝ ∈ subgroup ⊤ ↔ x✝ ∈ ⊥

Tactic:
;

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: case refine_3
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ 1 ≤ a

Tactic:
;

Goal state after:
case refine_3
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ 1 ≤ a
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 2⁻¹ < a
⊢ ↑⌈(2 - 1)⁻¹⌉₊ / 2 < a

Tactic:
norm_num at ha ⊢

Goal state after:
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 / 2 < a
⊢ 1 / 2 < a
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 / 2 < a
⊢ 1 / 2 < a

Tactic:
;

Goal state after:
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 / 2 < a
⊢ 1 / 2 < 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 : M
s : UpperSet (FiniteMulArchimedeanClass M)
⊢ a ∈ subgroup s ↔ ∀ (h : ¬MulArchimedeanClass.mk a = ⊤), ⟨MulArchimedeanClass.mk a, ⋯⟩ ∈ s

Tactic:
;

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
s : UpperSet (FiniteMulArchimedeanClass M)
⊢ a ∈ subgroup s ↔ ∀ (h : ¬MulArchimedeanClass.mk a = ⊤), ⟨MulArchimedeanClass.mk a, ⋯⟩ ∈ s
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 2⁻¹ ≤ a
⊢ ↑⌈(2 - 1)⁻¹⌉₊ / 2 ≤ a

Tactic:
norm_num at ha ⊢

Goal state after:
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a

Tactic:
;

Goal state after:
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌊↑r + ↑n⌋ₑ = ↑(⌊r⌋₊ + n)

Tactic:
;

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌊↑r + ↑n⌋ₑ = ↑(⌊r⌋₊ + n)
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌊↑(r + ↑n)⌋ₑ = ↑(⌊r⌋₊ + n)

Tactic:
;

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌊↑(r + ↑n)⌋ₑ = ↑(⌊r⌋₊ + n)
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
;

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌊r + ↑n⌋₊ = ⌊r⌋₊ + n
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
;

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌈↑r + ↑n⌉ₑ = ↑(⌈r⌉₊ + n)
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
;

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌈↑(r + ↑n)⌉ₑ = ↑(⌈r⌉₊ + n)
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
;

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌈r + ↑n⌉₊ = ⌈r⌉₊ + n
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌊↑r - ↑n⌋ₑ = ↑(⌊r⌋₊ - n)

Tactic:
;

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌊↑r - ↑n⌋ₑ = ↑(⌊r⌋₊ - n)
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌊↑(r - ↑n)⌋ₑ = ↑(⌊r⌋₊ - n)

Tactic:
;

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌊↑(r - ↑n)⌋ₑ = ↑(⌊r⌋₊ - n)
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌊r - ↑n⌋₊ = ⌊r⌋₊ - n

Tactic:
;

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌊r - ↑n⌋₊ = ⌊r⌋₊ - n
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌈↑r - ↑n⌉ₑ = ↑(⌈r⌉₊ - n)

Tactic:
;

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌈↑r - ↑n⌉ₑ = ↑(⌈r⌉₊ - n)
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌈↑(r - ↑n)⌉ₑ = ↑(⌈r⌉₊ - n)

Tactic:
;

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌈↑(r - ↑n)⌉ₑ = ↑(⌈r⌉₊ - n)
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
;

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌈r - ↑n⌉₊ = ⌈r⌉₊ - n
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
⊢ ↑⌈↑r⌉ₑ < ↑r + 1

Tactic:
;

Goal state after:
r : ℝ≥0
⊢ ↑⌈↑r⌉ₑ < ↑r + 1
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: a : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ioi a ↔ x✝ ∈ Ioi ⌊a⌋ₑ

Tactic:
;

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∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Iio a ↔ x✝ ∈ Iio ⌈a⌉ₑ

Tactic:
;

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∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Iic a ↔ x✝ ∈ Iic ⌊a⌋ₑ

Tactic:
;

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∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ici a ↔ x✝ ∈ Ici ⌈a⌉ₑ

Tactic:
;

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∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Icc a b ↔ x✝ ∈ Icc ⌈a⌉ₑ ⌊b⌋ₑ

Tactic:
;

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∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ico a b ↔ x✝ ∈ Ico ⌈a⌉ₑ ⌈b⌉ₑ

Tactic:
;

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∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ioc a b ↔ x✝ ∈ Ioc ⌊a⌋ₑ ⌊b⌋ₑ

Tactic:
;

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∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ioo a b ↔ x✝ ∈ Ioo ⌊a⌋ₑ ⌈b⌉ₑ

Tactic:
;

Goal state after:
a b : ℝ≥0∞
x✝ : ℕ∞
⊢ x✝ ∈ toENNReal ⁻¹' Ioo a b ↔ x✝ ∈ Ioo ⌊a⌋ₑ ⌈b⌉ₑ