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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
⊢ c + (a - c) < b ↔ a < b

Tactic:
add_tsub_cancel_of_le h

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
⊢ a < b ↔ a < b
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
m n : ℤ
h : 0 ≤ n - m
⊢ ↑m ≤ ↑n

Tactic:
lift n - m to ℕ using h with k hk

Goal state after:
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
k : ℕ
hk : ↑k = n - m
⊢ ↑m ≤ ↑n
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝ : LT α
⊢ ⊥ < ⊥ ↔ ∃ b, ⊥ = ↑b ∧ ∀ (a : α), ⊥ = ↑a → a < b

Tactic:
simp [lt_def]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ⊥ < ↑a✝ ↔ ∃ b, ↑a✝ = ↑b ∧ ∀ (a : α), ⊥ = ↑a → a < b

Tactic:
simp [lt_def]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ↑a✝ < ⊥ ↔ ∃ b, ⊥ = ↑b ∧ ∀ (a : α), ↑a✝ = ↑a → a < b

Tactic:
simp [lt_def]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ ↔ ∃ b, ↑a✝ = ↑b ∧ ∀ (a : α), ↑a✝¹ = ↑a → a < b

Tactic:
simp [lt_def]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : LT α
⊢ ↑a < ↑b ↔ a < b

Tactic:
simp [lt_def]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a : α
⊢ ⊥ < ↑a

Tactic:
simp [lt_def]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a : WithBot α
⊢ ¬a < ⊥

Tactic:
simp [lt_def]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
y : αˣ
h : 0 < ↑y
z : αˣ
hz : 1 < z
⊢ y * z⁻¹ < y

Tactic:
by simp [hz]

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

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
⊢ ↑a < ↑b ↔ a < b

Tactic:
simp [lt_def]

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

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a : α
⊢ 0 < ↑a

Tactic:
simp [lt_def]

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

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a : WithZero α
⊢ ¬a < 0

Tactic:
simp [lt_def]

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:
coe_le_coe,

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

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

Tactic:
coe_le_coe,

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

Goal state before:
pp: x y : WithZero (Multiplicative ℤ)
hy : y ≠ 0
⊢ x < y * exp 1 ↔ x ≤ y

Tactic:
by
  lift y to Multiplicative ℤ using hy
  obtain rfl | hx := eq_or_ne x 0
  · simp
  lift x to Multiplicative ℤ using hx
  rw [← log_le_log, ← log_lt_log] <;> simp [log_mul, Int.lt_add_one_iff]

Goal state after:
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
inst✝ : IsStrictOrderedRing R
ha : a ≤ 0
⊢ a = 0 → ⌊a⌋₊ = 0

Tactic:
rintro rfl
    exact floor_zero

Goal state after:
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
inst✝ : IsStrictOrderedRing R
⊢ ↑1 ≤ a ↔ 1 ≤ a

Tactic:
cast_one

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

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ ↑b + (a + ↑d)

Tactic:
exact le_add_of_nonneg_right <| ha.trans <| le_add_of_nonneg_right d.cast_nonneg

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
⊢ DirectedOn r s ↔ Directed r Subtype.val

Tactic:
by
  simp only [DirectedOn, Directed, Subtype.exists, exists_and_left, exists_prop, Subtype.forall]
  exact forall₂_congr fun x _ => by simp [And.comm, and_assoc]

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hac : a ≤ c
hbc : b ≤ c
⊢ f a = f b

Tactic:
exact le_antisymm ((hf ha hc hac).trans <| hf' hb hc hbc) ((hf hb hc hbc).trans <| hf' ha hc hac)

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

Goal state before:
pp: G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
a : G₀
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f a = g a
⊢ f a⁻¹ = g a⁻¹

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Goal state after:
case inl
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f 0 = g 0
⊢ f 0⁻¹ = g 0⁻¹

case inr
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
a : G₀
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f a = g a
ha : a ≠ 0
⊢ f a⁻¹ = g a⁻¹
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hc : IsCofinalFor s t
⊢ IsCofinalFor (s ∪ t) t

Tactic:
rintro a (has | hat)

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
hc : IsCofinalFor s t
a : α
has : a ∈ s
⊢ ∃ b ∈ t, a ≤ b

case inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
hc : IsCofinalFor s t
a : α
hat : a ∈ t
⊢ ∃ b ∈ t, a ≤ b
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hc : IsCofinalFor s t
⊢ IsCofinalFor (t ∪ s) t

Tactic:
by
  rw [union_comm]
  exact hc.union_left

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

Goal state before:
pp: γ : Type u_3
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ (∃ x, ∀ y ∈ s, y ≤ x) ↔ ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x

Tactic:
exists_ge_and_iff_exists

Goal state after:
γ : Type u_3
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ (∃ x, ∀ y ∈ s, y ≤ x) ↔ ∃ x, ∀ y ∈ s, y ≤ x

γ : Type u_3
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ Monotone fun x ↦ ∀ y ∈ s, y ≤ x
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝³ : Semiring A
inst✝² : PartialOrder A
inst✝¹ : IsOrderedRing A
inst✝ : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < e

Tactic:
NormNum.IsNat.to_eq h rfl

Goal state after:
A : Type u_1
e : A
n : ℕ
inst✝³ : Semiring A
inst✝² : PartialOrder A
inst✝¹ : IsOrderedRing A
inst✝ : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < ↑n
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝³ : AddMonoidWithOne A
inst✝² : PartialOrder A
inst✝¹ : AddLeftMono A
inst✝ : ZeroLEOneClass A
h'' : NeZero 1
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < e

Tactic:
NormNum.IsNat.to_eq h rfl

Goal state after:
A : Type u_1
e : A
n : ℕ
inst✝³ : AddMonoidWithOne A
inst✝² : PartialOrder A
inst✝¹ : AddLeftMono A
inst✝ : ZeroLEOneClass A
h'' : NeZero 1
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < ↑n
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝² : Semiring A
inst✝¹ : PartialOrder A
inst✝ : IsOrderedRing A
h : NormNum.IsNat e n
⊢ 0 ≤ e

Tactic:
NormNum.IsNat.to_eq h rfl

Goal state after:
A : Type u_1
e : A
n : ℕ
inst✝² : Semiring A
inst✝¹ : PartialOrder A
inst✝ : IsOrderedRing A
h : NormNum.IsNat e n
⊢ 0 ≤ ↑n
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝³ : AddMonoidWithOne A
inst✝² : PartialOrder A
inst✝¹ : AddLeftMono A
inst✝ : ZeroLEOneClass A
h : NormNum.IsNat e n
⊢ 0 ≤ e

Tactic:
NormNum.IsNat.to_eq h rfl

Goal state after:
A : Type u_1
e : A
n : ℕ
inst✝³ : AddMonoidWithOne A
inst✝² : PartialOrder A
inst✝¹ : AddLeftMono A
inst✝ : ZeroLEOneClass A
h : NormNum.IsNat e n
⊢ 0 ≤ ↑n
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
x a : α
⊢ termg 0 x a = a

Tactic:
simp [termg, zero_zsmul]

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

Goal state before:
pp: α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
⊢ a ≤ b

Tactic:
obtain rfl | hb := hb.eq_or_lt

Goal state after:
case inl
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : 0 ≤ 0
h : ∀ (ε : α), 1 < ε → a ≤ 0 * ε
⊢ a ≤ 0

case inr
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
⊢ a ≤ b
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: α : Type u
β : Type v
a : α
l : List α
x : α
n : ℕ
hn : n ≤ l.length
⊢ n < (l.insertIdx n x).length

Tactic:
by rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff]

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

Goal state before:
pp: case inr
α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
this : ∀ {l₁ l₂ : List α}, l₁.length ≤ l₂.length → (l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂)
hle : ¬l₁.length ≤ l₂.length
⊢ l₂.insertIdx n a ~ l₁.insertIdx n a ↔ l₁ ~ l₂

Tactic:
this (Nat.le_of_not_ge hle),

Goal state after:
case inr
α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
this : ∀ {l₁ l₂ : List α}, l₁.length ≤ l₂.length → (l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂)
hle : ¬l₁.length ≤ l₂.length
⊢ l₂ ~ l₁ ↔ l₁ ~ l₂
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
⊢ (map (⇑f) l).prod = f l.prod

Tactic:
simp only [prod, foldr_map, ← map_one f]
  exact l.foldr_hom f (fun x y => (map_mul f x y).symm)

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
a : M
⊢ ((x :: xs).set 0 a).prod =
    ((take 0 (x :: xs)).prod * if 0 < (x :: xs).length then a else 1) * (drop (0 + 1) (x :: xs)).prod

Tactic:
simp [set]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
x✝¹ : ℕ
x✝ : M
⊢ ([].set x✝¹ x✝).prod = ((take x✝¹ []).prod * if x✝¹ < [].length then x✝ else 1) * (drop (x✝¹ + 1) []).prod

Tactic:
simp [set]

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
x✝ : b = a
e : b = a := x✝
⊢ idxOf a (b :: l) = 0

Tactic:
by rw [← e]; exact idxOf_cons_self

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

Goal state before:
pp: case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a ↦ if p a then f a else g a) xs).prod =
    (map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod
⊢ (map (fun a ↦ if p a then f a else g a) (x :: xs)).prod =
    (map f (filter (fun b ↦ decide (p b)) (x :: xs))).prod * (map g (filter (fun a ↦ decide ¬p a) (x :: xs))).prod

Tactic:
| cons x xs ih =>

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

Goal state before:
pp: case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
ih : (map (fun x ↦ if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (map (fun x ↦ if x = a then f x else g x) (x :: xs)).prod = (f a / g a) ^ count a (x :: xs) * (map g (x :: xs)).prod

Tactic:
| cons x xs ih =>

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

Goal state before:
pp: m k : ℕ+
⊢ ↑(m.mod k) = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k

Tactic:
by
  dsimp [mod, modDiv]
  cases (m : ℕ) % (k : ℕ) with
  | zero =>
    rw [if_pos rfl]
    rfl
  | succ n =>
    rw [if_neg n.succ_ne_zero]
    rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑n.succ
⊢ IsNNRat (↑n.succ * ⅟↑d)⁻¹ d n.succ

Tactic:
exact ⟨this, by simp⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑n.succ
⊢ IsRat (↑(Int.ofNat n.succ) * ⅟↑d)⁻¹ (Int.ofNat d) n.succ

Tactic:
exact ⟨this, by simp⟩

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

Goal state before:
pp: a : ℕ
ha0 : 0 < a
⊢ (↑a)⁻¹.den = a

Tactic:
← Int.ofNat_inj,

Goal state after:
a : ℕ
ha0 : 0 < a
⊢ ↑(↑a)⁻¹.den = ↑a
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: $u✝ «$u» : Lean.Level
«$α» : Type u
«$sα» : CommSemiring «$α»
«$a» : «$α»
«$b» : ℕ
$expr✝ : «$α»
«$pf» : Nat.rawCast 1 = $expr✝
⊢ «$a» ^ «$b» * Nat.rawCast 1 = «$a» ^ «$b» * $expr✝

Tactic:
rw [← pf]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

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

Tactic:
h.1,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ : R
h : IsNat (a₁ + b₁) 0
⊢ ↑0 + (a₂ + b₂) = a₂ + b₂
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ a ≠ b ↔ 1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b')

Tactic:
not_iff_not,

Goal state after:
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ a = b ↔ 1 / gcd * (bd * a') = 1 / gcd * (ad * b')
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ b * a ≤ (b + c) * a

Tactic:
rw [add_mul]

Goal state after:
R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ b * a ≤ b * a + c * a
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : Bool → α
⊢ f false ⊔ f true = f true ⊔ f false

Tactic:
sup_comm

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : Bool → α
⊢ f true ⊔ f false = f true ⊔ f false
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ ∀ (b : γ), a₀ ≤ u₁ b₀ b ↔ ∀ x ∈ s, x ≤ u₁ b₀ b

Tactic:
← ha₀,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ ∀ (b : γ), True
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), l (u a ⊓ u b) ≤ a

Tactic:
exact fun a b => gi.gc.l_le inf_le_left

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
g : β → α
f : ι → β
⊢ ⨆ b ∈ range f, g b = ⨆ i, g (f i)

Tactic:
by
  rw [← iSup_subtype'', iSup_range']

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

Goal state before:
pp: α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
i_in_J : i ∈ J
⊢ x ∈ ⋃ j ∈ J, Es j

Tactic:
simpa only [mem_iUnion, exists_prop] using ⟨i, i_in_J, hix⟩

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

Goal state before:
pp: α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J
obs' : ∀ (J : Set ι), x ∈ (⋃ j ∈ J, Es j)ᶜ ↔ i ∉ J
⊢ x ∈ (⋃ i ∈ I, Es i)ᶜ ↔ x ∈ ⋃ i ∈ Iᶜ, Es i

Tactic:
obs,

Goal state after:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J
obs' : ∀ (J : Set ι), x ∈ (⋃ j ∈ J, Es j)ᶜ ↔ i ∉ J
⊢ x ∈ (⋃ i ∈ I, Es i)ᶜ ↔ i ∈ Iᶜ
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
⊢ sSup s = sSup t

Tactic:
rcases eq_empty_or_nonempty s with rfl | s_ne

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ x ∈ ∅, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ ∅, y ≤ x
⊢ sSup ∅ = sSup t

case inr
α : 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
⊢ sSup s = sSup t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

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

Tactic:
exact ha hb

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

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a b : α
⊢ Icc (a ⊓ b) (a ⊔ b) = Icc (a ⊓ b) (b ⊔ a)

Tactic:
sup_comm

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

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

Tactic:
by
  change ¬ ∀ i, i ∈ s → ∀ j, j ∈ s → i ≠ j → ∀ t, t ≤ f i → t ≤ f j → t ≤ ⊥ at h
  simp only [not_forall] at h
  obtain ⟨i, hi, j, hj, h_ne, t, hfi, hfj, ht⟩ := h
  replace ht : t.Nonempty := by
    rwa [le_bot_iff, bot_eq_empty, ← Ne, ← nonempty_iff_ne_empty] at ht
  obtain ⟨x, hx⟩ := ht
  exact ⟨i, hi, j, hj, h_ne, x, hfi hx, hfj hx⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioo (min a b) (max a b) = Ioo (min a b) (max b a)

Tactic:
sup_comm

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ (∀ (x : ι), x ∈ s → f x = 1) ↔ ∀ ⦃x : ι⦄, x ∈ s → f x = 1 x

Tactic:
Pi.one_apply

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ max a 1 = max 1 a

Tactic:
sup_comm

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ max a⁻¹ 1 = max 1 a⁻¹

Tactic:
sup_comm

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

Goal state before:
pp: n k : ℕ
x✝ : 2 ≤ k + 2
h : k + 2 ≤ n
⊢ (n + 1 - (k + 2)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
rw [succ_sub_succ]
    exact pow_sub_lt_descFactorial' h

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

Goal state before:
pp: p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
⊢ p a

Tactic:
by
  apply strongInductionOn a
  rintro ⟨k, kprop⟩ hk
  rcases k with - | k
  · exact (lt_irrefl 0 kprop).elim
  rcases k with - | k
  · exact hz
  exact hi ⟨k.succ, Nat.succ_pos _⟩ fun m hm => hk _ (Nat.lt_succ_iff.2 hm)

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

Goal state before:
pp: case succ
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
IH : (h : 0 < n) → p ⟨n, h⟩
h : 0 < n + 1
⊢ p ⟨n + 1, h⟩

Tactic:
| succ n IH =>

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

Goal state before:
pp: a b : ℕ+
h : a < b
⊢ ↑a + ↑(b - a) = ↑b

Tactic:
sub_coe,

Goal state after:
a b : ℕ+
h : a < b
⊢ (↑a + if a < b then ↑b - ↑a else 1) = ↑b
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:
cast_one

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
a : α
⊢ round (a + 1) = round (a + 1)
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:
cast_one

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
a : α
⊢ round (a - 1) = round (a - 1)
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
⊢ ↑1 ≤ a ↔ 1 ≤ a

Tactic:
cast_one

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ 1 ≤ a ↔ 1 ≤ a
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
⊢ ⌊a + ↑1⌋ = ⌊a⌋ + 1

Tactic:
floor_add_intCast

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ ⌊a⌋ + 1 = ⌊a⌋ + 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
n : ℕ
⊢ ⌊a + ↑↑n⌋ = ⌊a⌋ + ↑n

Tactic:
floor_add_intCast

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ⌊a⌋ + ↑n = ⌊a⌋ + ↑n
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 : ⌊a⌋ = ⌊b⌋
⊢ |a - b| < 1

Tactic:
wlog h0 : b ≤ a generalizing a b
  · rw [abs_sub_comm]
    exact this h.symm (le_of_not_ge h0)
  calc |a - b|
    _ = a - b := abs_of_nonneg (sub_nonneg_of_le h0)
    _ < ⌊a⌋ + 1 - b := sub_lt_sub_right (lt_floor_add_one a) _
    _ ≤ ⌊a⌋ + 1 - ⌊b⌋ := sub_le_sub_left (floor_le b) _
    _ = 1 := by rw [h, add_sub_cancel_left]

Goal state after: