mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
⊢ ∀ {a b : α},
    { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
intro a b

Goal state after:
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a b : α
⊢ { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a ≤
      { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b ↔
    a ≤ b
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: case refine_1
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
⊢ ∀ (a a_1 : X), f a ≤ f a_1 ↔ a_1 ≤ a

Tactic:
intro a b

Goal state after:
case refine_1
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
a b : X
⊢ f a ≤ f b ↔ b ≤ a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:

Tactic:
a ^ (n + 2) = a ^ (n + 1) * a := by rw [pow_succ]
      _ ≤ b ^ n * a * a := by grw [pow_le_pow_mul_of_sq_le_mul hab (by lia)]; simp
      _ = b ^ n * a ^ 2 := by rw [mul_assoc, sq]
      _ ≤ b ^ n * (b * a) := by grw [hab]
      _ = b ^ (n + 1) * a := by rw [← mul_assoc, ← pow_succ]

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
⊢ |a|ₘ ≤ |b|ₘ * |b * a|ₘ

Tactic:
simpa using mabs_mul_le b⁻¹ (b * a)

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) * c / ((b ⊓ a ⊓ c) * (b ⊓ a ⊔ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)

Tactic:
inf_mul_sup

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) * c / ((b ⊓ a) * c) = (b ⊔ a) * c / ((b ⊓ a) * c)
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ 1 ≤ a * |a|ₘ

Tactic:
grw [← mul_inv_cancel a, inv_le_mabs a]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
⊢ max a b / min a b = |a / b|ₘ

Tactic:
rcases le_total a b with ab | ba
  · rw [max_eq_right ab, min_eq_left ab, mabs_of_le_one, inv_div]
    rwa [div_le_one']
  · rw [max_eq_left ba, min_eq_right ba, mabs_of_one_le]
    rwa [one_le_div']

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : (↑(n.gcd k % k)).toNat = (↑n * n.gcdA k % ↑k).toNat
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k

Tactic:
Int.toNat_natCast,

Goal state after:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k % k = (↑n * n.gcdA k % ↑k).toNat
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
h2 : a < b
⊢ a - c < b - c

Tactic:
apply hc.lt_tsub_of_add_lt_left

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
h2 : a < b
⊢ c + (a - c) < b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : WithTop α
⊢ map (⇑f) (a + b) = map (⇑f) a + map (⇑f) b

Tactic:
induction a
  · exact (top_add _).symm
  · induction b
    · exact (add_top _).symm
    · rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
      rfl

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrderedCommMonoidWithZero α
a : α
n : ℕ
inst✝ : IsReduced α
hn : n ≠ 0
⊢ 0 < a ^ n ↔ 0 < a

Tactic:
simp_rw [pos_iff_ne_zero, pow_ne_zero_iff hn]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : Nonempty α
inst✝ : NoTopOrder α
x : WithBot (WithTop α)
⊢ x = ⊤ ↔ ∀ (a : α), ↑↑a ≤ x

Tactic:
refine ⟨by simp_all, fun H ↦ ?_⟩
  induction x
  · simp at H
  · simpa [WithTop.eq_top_iff_forall_ge] using H

Goal state after:
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
lb : ℤ
H : P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z

Tactic:
exact ⟨lb, H⟩

Goal state after:
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
lb : ℤ
H : P lb ∧ ∀ (z : ℤ), P z → z ≤ lb
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

Tactic:
exact ⟨lb, H⟩

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ ⌈a⌉ ≤ 0 ↔ a ≤ 0

Tactic:
rw [ceil_le, cast_zero]

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥)

Tactic:
intro a b

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
a b : β
⊢ ∃ z, (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible (a * b)
⊢ ⅟(a * b) * a * b = 1

Tactic:
rw [mul_assoc, invOf_mul_self]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: case inr
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
a : G₀
h✝ : IsUnit (f a)
h : a ≠ 0
⊢ IsUnit a

Tactic:
· exact ⟨⟨a, a⁻¹, mul_inv_cancel₀ h, inv_mul_cancel₀ h⟩, rfl⟩

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a : β
⊢ ∀ (x : β), (∀ (y : β), y < x → f y = g y) → f x = g x

Tactic:
intro a IH

Goal state after:
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
⊢ f a = g a
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 2 * a * b ≤ ε * a ^ 2 + ε⁻¹ * b ^ 2

Tactic:
calc 2 * a * b
  _ = 2 * a * b * (ε * ε⁻¹) := by rw [mul_inv_cancel₀ hε.ne', mul_one]
  _ = (2 * (ε * a) * b) * ε⁻¹ := by simp_rw [mul_assoc, mul_comm ε, mul_assoc]
  _ ≤ ((ε * a) ^ 2 + b ^ 2) * ε⁻¹ := by gcongr; exact inv_nonneg.mpr hε.le
  _ = ε * a ^ 2 + ε⁻¹ * b ^ 2 := by
    rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]

Goal state after:
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ⊆ [a, b] ↔ ∀ (c : α), c ∈ l → c = b ∨ c = a

Tactic:
simp [subset_def, or_comm]

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ {x, y} = [x, y]

Tactic:
by
  rw [insert_neg, singleton_eq]
  rwa [singleton_eq, mem_singleton]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
L : List M
h : L.prod ≠ 1
⊢ 0 < L.length

Tactic:
cases L
  · simp at h
  · simp

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < max l₁.length l₂.length → l₁[n]? = l₂[n]?
⊢ l₁ = l₂

Tactic:
apply ext_getElem?
  grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
i : ℕ
hlen : i < l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute l[i] a'
a' : M
a'_mem : a' ∈ take i (l.eraseIdx i)
⊢ a' ∈ take i l

Tactic:
take_eraseIdx_eq_take_of_le l i i (Nat.le_refl i)

Goal state after:
M : Type u_4
inst✝ : Monoid M
l : List M
i : ℕ
hlen : i < l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute l[i] a'
a' : M
a'_mem : a' ∈ take i l
⊢ a' ∈ take i l
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a b : G
l : List G
⊢ (a :: b :: l).alternatingProd = a * (b :: l).alternatingProd⁻¹

Tactic:
by
    rw [alternatingProd_cons_cons', alternatingProd_cons' b l, mul_inv, inv_inv, mul_assoc]

Goal state after:
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
hq : q.den = 1
| q.num /. ↑q.den

Tactic:
hq

Goal state after:
q : ℚ
hq : q.den = 1
| q.num /. ↑1
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
l₁ l₂ : List α
⊢ map f (foldl List.erase l₁ l₂) = foldl (fun l a ↦ l.erase (f a)) (map f l₁) l₂

Tactic:
induction l₂ generalizing l₁ <;> [rfl; simp only [foldl_cons, map_erase finj, *]]

Goal state after:
Module: Mathlib.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a x y : G
⊢ SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x

Tactic:
by
  simp_rw [SemiconjBy, ← mul_inv_rev, inv_inj, eq_comm]

Goal state after:
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ / ↑d₁ = ↑n₂ / ↑d₂
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂

Tactic:
rwa [eq_div_iff_mul_eq d₂a, division_def, mul_assoc, (d₁.cast_commute (d₂ : α)).inv_left₀.eq,
      ← mul_assoc, ← division_def, eq_comm, eq_div_iff_mul_eq d₁a, eq_comm, ← Int.cast_natCast d₁,
      ← Int.cast_mul, ← Int.cast_natCast d₂, ← Int.cast_mul, Int.cast_inj, ← mkRat_eq_iff d₁0 d₂0]
      at h

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: n : ℤ
q : ℚ
⊢ (-q).den = q.den

Tactic:
neg_den

Goal state after:
n : ℤ
q : ℚ
⊢ q.den = q.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) ∣ q₁.num * q₂.num

Tactic:
rw [← Int.dvd_natAbs]

Goal state after:
q₁ q₂ : ℚ
⊢ ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) ∣ ↑(q₁.num * q₂.num).natAbs
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b : R
⊢ (a₁ + a₂) * b = a₁ * b + a₂ * b

Tactic:
simp [_root_.add_mul]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
x✝ : BddAbove (l '' s)
x : β
hx : x ∈ upperBounds (l '' s)
⊢ u x ∈ upperBounds s

Tactic:
rwa [gc.upperBounds_l_image] at hx

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
Bs : BddAbove s
b : α
hb : b ∈ upperBounds s
⊢ BddAbove t

Tactic:
refine ⟨b, fun y hy ↦ ?_⟩
        rcases ht y hy with ⟨x, hx, hyx⟩
        exact hyx.trans (hb hx)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' t) ≤ sInf (f '' s)

Tactic:
gcongr; exacts [ht, hs.image f]

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f [[a, b]] [[f a, f b]]

Tactic:
by
  rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf] <;>
    apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
h : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ i = j ∨ Disjoint (f i) (f j)

Tactic:
by
  rw [or_iff_not_imp_right]
  exact h.elim hi hj

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f [[a, b]] [[f a, f b]]

Tactic:
by
  rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf] <;>
    apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
⊢ (Disjoint on fun a ↦ f a '' t) x y

Tactic:
refine disjoint_iff_inf_le.mpr ?_
    rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩
    exact h (congr_arg Prod.fst <| hs (mk_mem_prod hx ha) (mk_mem_prod hy hb) hab)

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
⊢ (uIoo a b).Nonempty ↔ a ≠ b

Tactic:
by
  simp [uIoo, eq_comm]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
⊢ ↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)

Tactic:
by
  cases isEmpty_or_nonempty ι
  · simp
  · simp_rw [coe_iInf, ← inf_iInf, ← inf_assoc, inf_idem]

Goal state after:
Module: Mathlib.Tactic.NormNum.Eq

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul (Int.ofNat denom✝) = num✝.mul (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ⅟↑denom✝¹ = ↑num✝ * ⅟↑denom✝

Tactic:
Rat.invOf_denom_swap

Goal state after:
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul (Int.ofNat denom✝) = num✝.mul (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ↑denom✝ = ↑num✝ * ↑denom✝¹
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
a : α
⊢ round (a - 1) = round a - 1

Tactic:
rw [← round_sub_intCast a 1, cast_one]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
n : ℤ
⊢ round x = n ↔ x ∈ Ico (↑n - 1 / 2) (↑n + 1 / 2)

Tactic:
by
  norm_num [round_eq, floor_eq_iff, ← lt_sub_iff_add_lt, add_sub_assoc]

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

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * ↑n + 1
hk0 : 0 < k
⊢ ⌊x⌋ = n

Tactic:
floor_eq_iff,

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * ↑n + 1
hk0 : 0 < k
⊢ ↑n ≤ x ∧ x < ↑n + 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ ⌊fract a⌋ = 0

Tactic:
floor_eq_iff,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ ↑0 ≤ fract a ∧ fract a < ↑0 + 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ ⌊a⌋ = z

Tactic:
floor_eq_iff,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ ↑z ≤ a ∧ a < ↑z + 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case mp
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
x : R
⊢ (∃ x_1 ∈ s, fract x_1 = x) → ∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1

Tactic:
rintro ⟨y, hy, rfl⟩
    exact ⟨⌊y⌋, ⟨y, hy, rfl⟩, fract_nonneg y, fract_lt_one y⟩

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
⊢ (q_inv - ↑⌊q_inv⌋).num < q.num

Tactic:
simp only [gt_iff_lt, q_inv]

Goal state after:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
⊢ (↑q.den / ↑q.num - ↑⌊↑q.den / ↑q.num⌋).num < q.num
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ a / 2 < ↑⌊a⌋

Tactic:
by
  rw [div_eq_inv_mul]; refine mul_lt_floor ?_ ?_ ?_ <;> norm_num; assumption

Goal state after:
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: M : Type u_6
inst✝ : CommMonoid M
u₁ u₂ : Mˣ
⊢ u₁ • u₂ = u₁ * u₂

Tactic:
ext
  rfl

Goal state after:
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : t ≤ s
⊢ {a} + s - t = {a} + (s - t)

Tactic:
Multiset.add_sub_assoc h

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : t ≤ s
⊢ {a} + (s - t) = {a} + (s - t)
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case isTrue
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h✝ : a ∈ l.dedup
⊢ (a :: l).dedup = l.dedup

Tactic:
simp [dedup_cons_of_mem', dedup_cons_of_notMem', *]

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case isFalse
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h✝ : ¬a ∈ l.dedup
⊢ (a :: l).dedup = a :: l.dedup

Tactic:
simp [dedup_cons_of_mem', dedup_cons_of_notMem', *]

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ min (if x = y then n else 0) (count y s) = count y (replicate (min n (count x s)) x)

Tactic:
count_replicate

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
⊢ ∀ (a b : Finset α), P a b

Tactic:
intro a b

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
⊢ P a b
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
h : (image f s).Nontrivial
⊢ s.Nontrivial

Tactic:
simp only [Finset.Nontrivial, coe_image] at h ⊢

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
h : (f '' ↑s).Nontrivial
⊢ (↑s).Nontrivial
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
⊢ p.predAbove a ≤ p.predAbove b

Tactic:
dsimp [predAbove]

Goal state after:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
⊢ (if h : p.castSucc < a then a.pred ⋯ else a.castPred ⋯) ≤ if h : p.castSucc < b then b.pred ⋯ else b.castPred ⋯
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
⊢ (fun p ↦ p.predAbove i) a ≤ (fun p ↦ p.predAbove i) b

Tactic:
dsimp [predAbove]

Goal state after:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
⊢ (if h : a.castSucc < i then i.pred ⋯ else i.castPred ⋯) ≤ if h : b.castSucc < i then i.pred ⋯ else i.castPred ⋯
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
h : 1 ≠ 0
⊢ ↑(pred 1 h) = ↑0

Tactic:
val_pred,

Goal state after:
n : ℕ
inst✝ : NeZero n
h : 1 ≠ 0
⊢ ↑1 - 1 = ↑0
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
i j : Fin (n + 1)
h : i ≤ j
hj : j ≠ last n
⊢ i ≠ last n

Tactic:
← lt_last_iff_ne_last

Goal state after:
n m : ℕ
i j : Fin (n + 1)
h : i ≤ j
hj : j < last n
⊢ i < last n
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ b < a.succ.castPred ha ↔ b ≤ a

Tactic:
by
  rw [lt_castPred_iff, castSucc_lt_succ_iff]

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ¬Nontrivial ↑↑s

Tactic:
not_nontrivial_iff_subsingleton,

Goal state after:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ Subsingleton ↑↑s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.succ
i : Fin n
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ m + n = n

Tactic:
hu,

Goal state after:
m n : ℕ
α✝ : Fin (n + 1) → Sort u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.succ
i : Fin n
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ 0 + n = n
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i < n + 1 + m
⊢ append (cons a as) bs ⟨i, isLt✝⟩ = (cons a (append as bs) ∘ Fin.cast ⋯) ⟨i, isLt✝⟩

Tactic:
simp only [append, addCases, cons, castLT, comp_apply]

Goal state after:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i < n + 1 + m
⊢ (if h : i < n + 1 then cases a as ⟨i, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i, isLt✝⟩) ⋯)) =
    cases a (addCases as bs) (Fin.cast ⋯ ⟨i, isLt✝⟩)