mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddRightReflectLE R
h : b * a < c * a
hbc : b ≤ c
⊢ 0 < a

Tactic:
by_cases! ha : 0 < a
  · exact ha
  · grind [mul_le_mul_of_nonpos_right hbc ha]

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ 2 * 2 * r ^ 2 ≤ (a + b) * (a + b)

Tactic:
two_mul,

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ (2 + 2) * r ^ 2 ≤ (a + b) * (a + b)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x

Tactic:
mul_nonneg_iff,

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ 0 ≤ x - a ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
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✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : (fun x1 x2 ↦ x1 < x2) ≃r fun x1 x2 ↦ x1 < x2
⊢ ∀ {a b : α}, e.toEquiv a ≤ e.toEquiv b ↔ a ≤ b

Tactic:
by simp [le_iff_eq_or_lt, e.map_rel_iff, e.injective.eq_iff]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
a✝ : ComplementedLattice α
⊢ ComplementedLattice β

Tactic:
exact f.complementedLattice

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

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ |a ^ n|ₘ = a⁻¹ ^ n

Tactic:
← mabs_inv,

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ |(a ^ n)⁻¹|ₘ = a⁻¹ ^ n
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
a b : α
⊢ |a / b|ₘ = |b / a|ₘ

Tactic:
← mabs_inv,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
a b : α
⊢ |(a / b)⁻¹|ₘ = |b / a|ₘ
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: b p : ℕ
w : 0 < b
⊢ ↑(b ^ p - 1) = ↑b ^ p - 1

Tactic:
have : 1 ≤ b ^ p := Nat.one_le_pow p b w

Goal state after:
b p : ℕ
w : 0 < b
this : 1 ≤ b ^ p
⊢ ↑(b ^ p - 1) = ↑b ^ p - 1
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑1 ≤ ↑n ↔ 1 ≤ n

Tactic:
cast_le

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ 1 ≤ n ↔ 1 ≤ n
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑n ≤ ↑1 ↔ n ≤ 1

Tactic:
cast_le

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ n ≤ 1 ↔ n ≤ 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
h : s.succ ≠ 0
⊢ s.succ.gcdB 0 = 0

Tactic:
simp [gcdB, xgcd, xgcdAux, Nat.strongRec_eq]

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

Goal state before:
pp: m n : ℕ
⊢ ↑((↑m).gcd -[n+1]) = ↑m * (↑m).gcdA -[n+1] + -(↑n + 1) * -(↑m).natAbs.gcdB n.succ

Tactic:
rw [Int.neg_mul_neg]; apply Nat.gcd_eq_gcd_ab

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

Goal state before:
pp: m n : ℕ
⊢ ↑(-[m+1].gcd ↑n) = -(↑m + 1) * -m.succ.gcdA (↑n).natAbs + ↑n * -[m+1].gcdB ↑n

Tactic:
rw [Int.neg_mul_neg]; apply Nat.gcd_eq_gcd_ab

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

Goal state before:
pp: case mpr
a b : ℤ
n : ℕ
x y : ℤ
h : ↑n = a * x + b * y
⊢ ↑(a.gcd b) ∣ a * x + b * y

Tactic:
exact Int.dvd_add (dvd_mul_of_dvd_left (gcd_dvd_left ..))
      (dvd_mul_of_dvd_left (gcd_dvd_right ..))

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
⊢ a < b ↔ ∃ c, c > 1 ∧ b = a * c

Tactic:
by
  rw [lt_iff_le_and_ne, le_iff_exists_mul, ← exists_and_right]
  apply exists_congr
  intro c
  rw [and_comm, and_congr_left_iff, gt_iff_lt]
  rintro rfl
  constructor
  · rw [one_lt_iff_ne_one]
    apply mt
    rintro rfl
    rw [mul_one]
  · rw [← (self_le_mul_right a c).lt_iff_ne]
    apply lt_mul_of_one_lt_right'

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
⊢ ¬IsLeftRegular 0 ↔ Nontrivial R

Tactic:
nontrivial_iff,

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
⊢ ¬IsLeftRegular 0 ↔ ∃ x y, x ≠ y
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
⊢ ¬IsRightRegular 0 ↔ Nontrivial R

Tactic:
nontrivial_iff,

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
⊢ ¬IsRightRegular 0 ↔ ∃ x y, x ≠ y
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
h : ⊤ = 0
a : α
ha : 0 + a ≠ 0
⊢ False

Tactic:
simp [LinearOrderedAddCommGroupWithTop.top_add', -zero_add, ← h] at ha

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝ : WithZero α ≃* WithZero β
⊢ (fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
      ((fun e ↦ { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
        x✝) =
    x✝

Tactic:
ext x; cases x <;> simp

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a b : WithTop G
⊢ a - b = a + -b

Tactic:
cases a <;> cases b

Goal state after:
case top.top
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
⊢ ⊤ - ⊤ = ⊤ + -⊤

case top.coe
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝ : G
⊢ ⊤ - ↑a✝ = ⊤ + -↑a✝

case coe.top
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝ : G
⊢ ↑a✝ - ⊤ = ↑a✝ + -⊤

case coe.coe
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝¹ a✝ : G
⊢ ↑a✝¹ - ↑a✝ = ↑a✝¹ + -↑a✝
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℤ
⊢ ↑n ≤ ↑0 ↔ n ≤ 0

Tactic:
cast_le

Goal state after:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℤ
⊢ n ≤ 0 ↔ n ≤ 0
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℤ
h : a < 0
⊢ ↑a ≤ ↑(-1)

Tactic:
cast_le

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℤ
h : a < 0
⊢ a ≤ -1
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case neg
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
findGreatest_of_not hk,

Goal state after:
case neg
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ findGreatest P k = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n a : ℕ
⊢ ↑n ≤ ↑a ↔ n ≤ a

Tactic:
cast_le

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n a : ℕ
⊢ n ≤ a ↔ n ≤ a
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n

Tactic:
obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_comm n, add_comm (n : R), add_le_add_iff_right, add_le_add_iff_right,
        le_floor_iff ha]

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Preorder α
f : α → β
inst✝ : IsDirectedOrder α
hf : Monotone f
hf' : Antitone f
a b : α
⊢ f a = f b

Tactic:
have := hf.forall_le_of_antitone hf' le_rfl
  exact le_antisymm (this a b) (this b a)

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hf : Injective2 f
a' : α
ha' : a' ∈ s
b' : β
hb' : b' ∈ t
h : f a' b' = f a b
⊢ a ∈ s ∧ b ∈ t

Tactic:
rcases hf h with ⟨rfl, rfl⟩

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
hf : Injective2 f
a' : α
ha' : a' ∈ s
b' : β
hb' : b' ∈ t
h : f a' b' = f a' b'
⊢ a' ∈ s ∧ b' ∈ t
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|

Tactic:
← mabs_inv,

Goal state after:
case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ |(a ^ n)⁻¹|ₘ = |a|ₘ ^ |n|
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
s : Set α
⊢ image2 f s {b} = s

Tactic:
rw [image2_singleton_right, funext h, image_id']

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ IsCofinalFor s t

Tactic:
rcases isCofinalFor_or_isCofinalFor_of_directedOn_union h with hts | hst
    · exact .inl ⟨DirectedOn.of_isCofinalFor h subset_union_left hts.union_right, hts⟩
    · exact .inr ⟨DirectedOn.of_isCofinalFor h subset_union_right hst.union_left, hst⟩

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n d : ℕ
inst✝¹ : Semiring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ e

Tactic:
rw [eq, of_decide_eq_true h]; simp

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝¹ : Ring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ e

Tactic:
rw [eq, of_decide_eq_true h]; simp

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
⊢ a ≤ a + a ↔ 0 ≤ a

Tactic:
le_add_iff_nonneg_left

Goal state after:
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
⊢ 0 ≤ a ↔ 0 ≤ a
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
inst✝ : IsStrictOrderedRing α
h : a / b ≤ c / d
he : 0 ≤ e
⊢ a / b * (1 / e) ≤ c / (d * e)

Tactic:
div_mul_eq_div_mul_one_div

Goal state after:
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
inst✝ : IsStrictOrderedRing α
h : a / b ≤ c / d
he : 0 ≤ e
⊢ a / b * (1 / e) ≤ c / d * (1 / e)
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ tail^[n] l = drop n l

Tactic:
induction n generalizing l with
  | zero => rfl
  | succ n ih => cases l <;> simp [*]

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

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
l₁ l₂ : List α
⊢ l₁.length ≤ (l₁ ++ l₂).length

Tactic:
simp only [length_append, Nat.le_add_right]

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
a : α
⊢ l₁.length ≤ (l₁ ++ l₂).length

Tactic:
simp only [length_append, Nat.le_add_right]

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

Goal state before:
pp: α : Type u
β : Type v
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
⊢ n + k + 1 < (l.insertIdx n x).length

Tactic:
rwa [length_insertIdx_of_le_length (by lia), Nat.succ_lt_succ_iff]

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 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 2 * a * b = 2 * a * b * (ε * ε⁻¹)

Tactic:
by rw [mul_inv_cancel₀ hε.ne', mul_one]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
l : List α
i✝ : ℕ
a✝ : γ
⊢ ((map g ∘ map f) l)[i✝]? = some a✝ ↔ (map g (map f l))[i✝]? = some a✝

Tactic:
Function.comp_apply

Goal state after:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
l : List α
i✝ : ℕ
a✝ : γ
⊢ (map g (map f l))[i✝]? = some a✝ ↔ (map g (map f l))[i✝]? = some a✝
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ (j :: L).length ≤ (j :: L).sum

Tactic:
sum_cons,

Goal state after:
case cons
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ (j :: L).length ≤ j + L.sum
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: r : ℚ
⊢ ↑r.num / ↑↑r.den = r

Tactic:
← divInt_eq_div,

Goal state after:
r : ℚ
⊢ r.num /. ↑r.den = r
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ ↑a.den /. a.num

Tactic:
exact divInt_nonneg (Int.natCast_nonneg a.den) (num_nonneg.mpr ha)

Goal state after:
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: n : ℕ
a : ℚ≥0
⊢ ↑(a ^ Int.negSucc n) = ↑(a ^ ↑n.succ)⁻¹

Tactic:
apply Field.zpow_neg'

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

Goal state before:
pp: m : ℕ
⊢ ↑(m + 1).toPNat' = if 0 < m + 1 then m + 1 else 1

Tactic:
if_pos (succ_pos m)

Goal state after:
m : ℕ
⊢ ↑(m + 1).toPNat' = m + 1
Module: Mathlib.Data.Rat.Lemmas

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

Tactic:
rw [← Int.natCast_dvd_natCast, Int.dvd_natAbs]

Goal state after:
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₁.num * ↑q₂.den + q₂.num * ↑q₁.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mpr
q : ℚ
⊢ IsSquare q.num ∧ IsSquare q.den → IsSquare q

Tactic:
rintro ⟨⟨nr, hnr⟩, ⟨dr, hdr⟩⟩

Goal state after:
case mpr
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ IsSquare q
Module: Mathlib.Data.Rat.Cast.Defs

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

Tactic:
simp [cast_def]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) = OfNat.ofNat n

Tactic:
simp [cast_def]

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

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.ofNat a ^ (2 * b') = Int.ofNat c

Tactic:
two_mul,

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.ofNat a ^ (b' + b') = Int.ofNat c
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ Int.ofNat a ^ (2 * b') * -Int.ofNat a = -Int.ofNat c

Tactic:
two_mul,

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ Int.ofNat a ^ (b' + b') * -Int.ofNat a = -Int.ofNat c
Module: Mathlib.Data.Tree.Basic

Goal state before:
pp: case node
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
v : α
l r : BinaryTree α
hl : map (g ∘ f) l = map g (map f l)
hr : map (g ∘ f) r = map g (map f r)
⊢ node ((g ∘ f) v) (map g (map f l)) (map g (map f r)) = node (g (f v)) (map g (map f l)) (map g (map f r))

Tactic:
Function.comp_apply

Goal state after:
case node
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
v : α
l r : BinaryTree α
hl : map (g ∘ f) l = map g (map f l)
hr : map (g ∘ f) r = map g (map f r)
⊢ node (g (f v)) (map g (map f l)) (map g (map f r)) = node (g (f v)) (map g (map f l)) (map g (map f r))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set (WithTop α)
h : ¬BddAbove (some ⁻¹' s)
hmem : ⊤ ∉ s
⊢ sSup s = ⊤

Tactic:
· exact if_neg hmem |>.trans <| if_neg h

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
s : Set α
b : α
⊢ sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

Tactic:
simpa only [inf_comm] using @inf_sSup_eq α _ s b

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : OrderBot α
x y : ↑(Iic a)
⊢ Disjoint ↑x ↑y ∧ Codisjoint x y ↔ Disjoint ↑x ↑y ∧ ↑x ⊔ ↑y = a

Tactic:
Iic.codisjoint_iff

Goal state after:
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : OrderBot α
x y : ↑(Iic a)
⊢ Disjoint ↑x ↑y ∧ ↑x ⊔ ↑y = a ↔ Disjoint ↑x ↑y ∧ ↑x ⊔ ↑y = a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.some.refine_1.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb✝ : Option.some b ∈ upperBounds s
hb : none ∈ s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty

Tactic:
exact absurd hb h₁

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

Goal state before:
pp: case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ∀ b_1 ∈ (fun a ↦ ↑a) ⁻¹' s, b_1 ≤ b

Tactic:
· intro a ha
        exact coe_le_coe.1 (hb ha)

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

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

Tactic:
· refine coe_le_coe.2 (le_csInf ?_ ?_)
        · classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim
        · intro b hb
          rw [← coe_le_coe]
          exact ha hb

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ Monotone f ∨ Antitone f → ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
rintro (hf | hf) a b c <;> simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]
    exacts [fun hc => ⟨hf hc.1, hf hc.2⟩, fun hc => ⟨hf hc.2, hf hc.1⟩]

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
by
  obtain ⟨i, hi, j, hj, hne, x, hx₁, hx₂⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h
  rcases lt_or_lt_iff_ne.mpr hne with h_lt | h_lt
  · exact ⟨i, hi, j, hj, h_lt, x, hx₁, hx₂⟩
  · exact ⟨j, hj, i, hi, h_lt, x, hx₂, hx₁⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
h : (s ∩ Icc x y).OrdConnected
z : α
hz : z ∈ Icc x y
⊢ z ∈ s

Tactic:
have hxy : x ≤ y := hz.1.trans hz.2

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
h : (s ∩ Icc x y).OrdConnected
z : α
hz : z ∈ Icc x y
hxy : x ≤ y
⊢ z ∈ s
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
by
  cases n with
  | zero =>
    cases l
    · simp only [ascFactorial_zero, Nat.add_zero, Nat.one_mul, Nat.zero_add]
    · simp only [Nat.add_right_comm, zero_ascFactorial, Nat.zero_add, Nat.zero_mul]
  | succ n' =>
    apply Nat.mul_left_cancel (factorial_pos n')
    simp only [Nat.add_assoc, ← Nat.mul_assoc, factorial_mul_ascFactorial]
    rw [Nat.add_comm 1 l, ← Nat.add_assoc, factorial_mul_ascFactorial, Nat.add_assoc]

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

Goal state before:
pp: k : ℕ
⊢ (0 - k) * descFactorial 0 k = 0

Tactic:
Nat.zero_sub,

Goal state after:
k : ℕ
⊢ 0 * descFactorial 0 k = 0
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : ↑(m + m) = 2 * x
⊢ 2 * ↑m = 2 * x

Tactic:
by simp [← hm, ← two_mul]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x

Tactic:
two_mul,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(if fract x + fract x < 1 then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x
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
n : ℕ
a : ℤ
⊢ ↑a ≤ ↑↑n ↔ a ≤ ↑n

Tactic:
cast_le

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
n : ℕ
a : ℤ
⊢ a ≤ ↑n ↔ a ≤ ↑n
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:
rw [floor_eq_iff, ← mul_le_mul_iff_right₀ hk0, ← mul_lt_mul_iff_right₀ hk0, hn]

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
⊢ k * ↑n ≤ k * ↑n + 1 ∧ k * ↑n + 1 < k * (↑n + 1)