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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
⊢ f.comp id = f

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
⊢ id.comp f = f

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
f : α ↪o β
⊢ (id α).comp f = f

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
f : α ↪o β
⊢ f.comp (id β) = f

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℕ
h : x < ↑n
⊢ x < ↑↑n

Tactic:
Int.cast_natCast

Goal state after:
R : Type u_1
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℕ
h : x < ↑n
⊢ x < ↑n
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ Codisjoint (f a) (f b)

Tactic:
codisjoint_iff_le_sup,

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ ⊤ ≤ f a ⊔ f b
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ x * (y ⊓ z)

Tactic:
← inv_mul_le_iff_le_mul,

Goal state after:
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y ⊓ z
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

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

Tactic:
apply pow_two_semiclosed _
  rw [mabs, pow_two, mul_sup, sup_mul, ← pow_two, inv_mul_cancel, sup_comm, ← sup_assoc]
  apply le_sup_right

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑n.natAbs = ↑↑n.natAbs

Tactic:
Int.cast_natCast

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑n.natAbs = ↑n.natAbs
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: x y : ℤ
hc : x = 0 ∧ y = 0
⊢ gcd 0 y = 0

Tactic:
hc.right,

Goal state after:
x y : ℤ
hc : x = 0 ∧ y = 0
⊢ gcd 0 0 = 0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
x y : WithTop α
⊢ x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
x y : WithTop α
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
x y : WithTop α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z : α
⊢ x + ↑z ≤ y + ↑z → x ≤ y

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Goal state after:
case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝¹ a✝ : α
⊢ a✝¹ + z ≤ a✝ + z → a✝¹ ≤ a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
x y : WithTop α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ x < y → x + ↑z < y + ↑z

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Goal state after:
case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝¹ a✝ : α
⊢ a✝¹ < a✝ → a✝¹ + z < a✝ + z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
x : WithTop α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : AddLeftReflectLE α
⊢ AddLECancellable x → x ≠ ⊤

Tactic:
by rintro h rfl; exact (coe_lt_top <| Classical.arbitrary _).not_ge <| h <| by simp

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
⊢ a - (a - min a b) = min a b

Tactic:
tsub_tsub_cancel_of_le (min_le_left a _)

Goal state after:
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
⊢ min a b = min a b
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b + b = max a b

Tactic:
rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
x y : WithBot α
⊢ x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
x y : WithBot α
⊢ x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y : WithBot α
inst✝ : IsRightCancelAdd α
z : α
⊢ x + ↑z = y + ↑z ↔ x = y

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
x y : WithBot α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z : α
⊢ x + ↑z ≤ y + ↑z → x ≤ y

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Goal state after:
case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝¹ a✝ : α
⊢ a✝¹ + z ≤ a✝ + z → a✝¹ ≤ a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
x y : WithBot α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ x < y → x + ↑z < y + ↑z

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Goal state after:
case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝¹ a✝ : α
⊢ a✝¹ < a✝ → a✝¹ + z < a✝ + z
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑a✝¹ * ↑a✝ ≤ ↑a✝¹ * ↑c

Tactic:
← coe_mul _ c,

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑a✝¹ * ↑a✝ ≤ ↑(a✝¹ * c)
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n

Tactic:
simp [findGreatest_eq_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
hf : StrictMono ⇑f
⊢ StrictMono ⇑(map' f)

Tactic:
simpa [StrictMono, WithZero.forall]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : unzero ha < ofAdd b
⊢ toAdd (unzero ha) < b

Tactic:
← toAdd_lt,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) < toAdd (ofAdd b)
⊢ toAdd (unzero ha) < b
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
bounded : ∀ (x : α), ∃ n, x ≤ ↑n
below : ∀ (x : α), ∃ n, ↑n ≤ x
x : α
n : ℕ
hn : x ≤ ↑n
⊢ ∃ n, x ≤ ↑n

Tactic:
use n

Goal state after:
case h
F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
bounded : ∀ (x : α), ∃ n, x ≤ ↑n
below : ∀ (x : α), ∃ n, ↑n ≤ x
x : α
n : ℕ
hn : x ≤ ↑n
⊢ x ≤ ↑↑n
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ↑↑n ≤ a ↔ ↑n ≤ a

Tactic:
Int.cast_natCast

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ↑n ≤ a ↔ ↑n ≤ a
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ a ≤ ↑↑n ↔ a ≤ ↑n

Tactic:
Int.cast_natCast

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ a ≤ ↑n ↔ a ≤ ↑n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ a < ↑1 ↔ a < 1

Tactic:
rw [Nat.cast_one]

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

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
x : R
h : IsSquare x
⊢ 0 ≤ x

Tactic:
by
  rcases h with ⟨y, rfl⟩
  exact mul_self_nonneg y

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Units

Goal state before:
pp: u : ℤˣ
⊢ u = 1 ∨ u = -1

Tactic:
simpa only [Units.ext_iff] using! isUnit_eq_one_or u.isUnit

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a ≤ b
⊢ Icc a b = Ioc a b

Tactic:
rw [Icc_eq_empty h, Ioc_eq_empty (mt le_of_lt h)]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a < b
⊢ Ioo a b = Ioc a b

Tactic:
rw [Ioo_eq_empty h, Ioc_eq_empty h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
⊢ ↑(Int.negOfNat n) = -↑n

Tactic:
simp [Int.negOfNat_eq, Int.cast_neg]

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
⊢ f = HAdd.hAdd →
    IsRat a na da →
      IsRat b nb db → (na.mul ↑db).add (nb.mul ↑da) = (↑k).mul nc → da.mul db = k.mul dc → IsRat (f a b) nc dc

Tactic:
by
  rintro rfl ⟨_, rfl⟩ ⟨_, rfl⟩ (h₁ : na * db + nb * da = k * nc) (h₂ : da * db = k * dc)
  have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da:α) db
  have := invertibleOfMul' (α := α) h₂
  use this
  have H := (Nat.cast_commute (α := α) da db).invOf_left.invOf_right.right_comm
  have h₁ := congr_arg (↑· * (⅟↑da * ⅟↑db : α)) h₁
  simp only [Int.cast_add, Int.cast_mul, Int.cast_natCast, ← mul_assoc,
    add_mul, mul_invOf_cancel_right] at h₁
  have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
  simp only [H, mul_invOf_cancel_right', Nat.cast_mul, ← mul_assoc] at h₁ h₂
  rw [h₁, h₂, Nat.cast_commute]
  simp only [mul_invOf_cancel_right,
    (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
    (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]

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

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

Tactic:
have h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2 := two_mul_le_add_sq (ε * a) b
  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.Basic

Goal state before:
pp: α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ (a :: b :: l).dropLast ++ [(a :: b :: l).getLast h] = a :: b :: l

Tactic:
rw [dropLast_cons_cons, cons_append, getLast_cons (cons_ne_nil _ _)]

Goal state after:
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ a :: ((b :: l).dropLast ++ [(b :: l).getLast ⋯]) = a :: b :: l
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩

Tactic:
constructor
  · rintro rfl
    exact ⟨rfl, fun _ _ _ ↦ rfl⟩
  · intro ⟨h₁, h₂⟩
    exact ext_get h₁ h₂

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ x ^ r = (l ^ r).eval

Tactic:
← zpow'_of_ne_zero_right x r hr,

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ zpow' x r = (l ^ r).eval
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
i j : ℕ
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ j < l.length

Tactic:
simpa using hj

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

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
⊢ ∀ (a : α), foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)

Tactic:
induction l <;> intros <;> [rfl; simp only [*, foldr]]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: a : ℤ
b : ℕ
hb : b ≠ 0
⊢ 0 < mkRat a b ↔ 0 < a

Tactic:
grind [mkRat_nonneg_iff, Rat.mkRat_eq_zero]

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

Goal state before:
pp: q : ℚ≥0
⊢ 0 < q.num ↔ 0 < q

Tactic:
simpa [num, -nonpos_iff_eq_zero] using nonpos_iff_eq_zero _ |>.not.symm

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
Int.cast_natCast

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
n : ℕ
⊢ ↑n = ↑n
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
⊢ ↑↑d * ↑k = ↑d * ↑k

Tactic:
Int.cast_natCast

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
⊢ ↑d * ↑k = ↑d * ↑k
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑↑d = ↑n * ↑b
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b

Tactic:
Int.cast_natCast

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑a / ↑↑b = ↑a / ↑b

pp: case b0
α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑↑b ≠ 0

Tactic:
Int.cast_natCast

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑a / ↑b = ↑a / ↑b

case b0
α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑↑b ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: case b0
α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑↑b ≠ 0

Tactic:
Int.cast_natCast

Goal state after:
case b0
α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑b ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
q : ℚ
hq : ↑q.num ≠ 0
⊢ ↑↑q.den / ↑q.num = ↑q.den / ↑q.num

Tactic:
Int.cast_natCast

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
q : ℚ
hq : ↑q.num ≠ 0
⊢ ↑q.den / ↑q.num = ↑q.den / ↑q.num
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j ≤ i), f j = ⨆ i, f i

Tactic:
by
  apply le_antisymm
  · exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _
  · exact iSup_le fun j ↦ le_iSup_of_le j (le_iSup₂_of_le j le_rfl le_rfl)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j ≥ i), f j = ⨆ i, f i

Tactic:
by
  apply le_antisymm
  · exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _
  · exact iSup_le fun j ↦ le_iSup_of_le j (le_iSup₂_of_le j le_rfl le_rfl)

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
x : β
t : ι → Set β
⊢ insert x (⋂ i, t i) = ⋂ i, insert x (t i)

Tactic:
by
  simp_rw [← union_singleton, iInter_union]

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a b : α
inst✝¹ : Lattice α
inst✝ : Fact (a ≤ b)
x y : ↑(Icc a b)
⊢ IsCompl x y ↔ ↑x ⊓ ↑y = a ∧ ↑x ⊔ ↑y = b

Tactic:
by
  rw [_root_.isCompl_iff, Icc.disjoint_iff, Icc.codisjoint_iff]

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

Goal state before:
pp: case neg.some.refine_1.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a : β
ha✝ : Option.some a ∈ lowerBounds s
h : (fun a ↦ ↑a) ⁻¹' s = ∅
ha : none ∈ s
⊢ none ∈ {⊤}

Tactic:
exact mem_singleton ⊤

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ {a, b}.Pairwise r ↔ a ≠ b → r a b ∧ r b a

Tactic:
simp [pairwise_insert]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ uIoo a a = ∅

Tactic:
by simp [uIoo]

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : One M
f : ι × κ → M
i : ι
j : κ
hj : j ∈ mulSupport fun j ↦ f (i, j)
⊢ (i, j) ∈ mulSupport f ∧ (i, j).2 = j

Tactic:
simpa using hj

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inl
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : n < m
⊢ n = m

Tactic:
rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm

Goal state after:
case inl
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m ! < m !
⊢ n = m
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m < n
⊢ n = m

Tactic:
rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm

Goal state after:
case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m ! < m !
⊢ n = m
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n * n.succ.ascFactorial (k + 1) = (n + (k + 1)) * n.ascFactorial (k + 1)

Tactic:
ascFactorial,

Goal state after:
n k : ℕ
⊢ n * ((n.succ + k) * n.succ.ascFactorial k) = (n + (k + 1)) * n.ascFactorial (k + 1)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n.succ + k) * ((n + k) * n.ascFactorial k) = (n + (k + 1)) * n.ascFactorial (k + 1)

Tactic:
ascFactorial,

Goal state after:
n k : ℕ
⊢ (n.succ + k) * ((n + k) * n.ascFactorial k) = (n + (k + 1)) * ((n + k) * n.ascFactorial k)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1) ^ (k + 1) * (n + 1) < (n + 1).ascFactorial (k + 2)

Tactic:
ascFactorial,

Goal state after:
n k : ℕ
⊢ (n + 1) ^ (k + 1) * (n + 1) < (n + 1 + (k + 1)) * (n + 1).ascFactorial (k + 1)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

pp: case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Tactic:
· apply Nat.mul_left_cancel (n - m).factorial_pos
    rw [factorial_mul_descFactorial hmn, show n - m = (n - k) - (m - k) by lia, ← Nat.mul_assoc,
      factorial_mul_descFactorial (show m - k ≤ n - k by lia),
      factorial_mul_descFactorial (le_trans hkm hmn)]

Goal state after:
case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
hn : (↑q.num / ↑q.den).num = ↑q.num
hd : (↑q.num / ↑q.den).den = q.den
⊢ ↑↑q.num / ↑q.den = ↑q.num / ↑q.den

Tactic:
Int.cast_natCast

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
hn : (↑q.num / ↑q.den).num = ↑q.num
hd : (↑q.num / ↑q.den).den = q.den
⊢ ↑q.num / ↑q.den = ↑q.num / ↑q.den
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ ↑(round x) ≤ x + 1 / 2

Tactic:
rw [round_eq x]

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = negOfNat ⌈↑↑n / ↑d⌉.toNat

Tactic:
Int.cast_natCast

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = negOfNat ⌈↑n / ↑d⌉.toNat
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
ε : K
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ ∃ n, 1 / (↑n + 1) < ε

Tactic:
use n

Goal state after:
case h
K : Type u_4
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
ε : K
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / (↑n + 1) < ε
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.den / ↑q.num = ↑q.den / ↑q.num

Tactic:
Int.cast_natCast

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.den / ↑q.num = ↑q.den / ↑q.num
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉ < b * a

Tactic:
rw [← sub_pos] at hb

Goal state after:
case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉ < b * a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ ↑⌊a⌋₊ = ↑↑⌊a⌋₊

Tactic:
Int.cast_natCast

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ ↑⌊a⌋₊ = ↑⌊a⌋₊