mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a|ₘ = a⁻¹ ↔ a ≤ 1

Tactic:
mabs_eq_max_inv,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ max a a⁻¹ = a⁻¹ ↔ a ≤ 1
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 = |b / a|ₘ

Tactic:
mabs_div_comm,

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
⊢ max a b / min a b = |a / b|ₘ
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: x y : ℕ
⊢ x.P y (x, 1, 0)

Tactic:
by simp [P]

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

Goal state before:
pp: x y : ℕ
⊢ x.P y (y, 0, 1)

Tactic:
by simp [P]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semigroup R
a b : R
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a * b) ∧ IsRegular (b * a)

Tactic:
exact ⟨ha.mul hb, hb.mul ha⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ Function.Injective fun x ↦ b - x

Tactic:
simpa [sub_eq_add_neg] using! (add_right_injective_of_ne_top b h).comp neg_injective

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a + -a = 0 → a ≠ ⊤

Tactic:
contrapose; simp +contextual

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

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝¹ a✝ : α
⊢ x + a✝¹ ≤ x + a✝ → a✝¹ ≤ a✝

Tactic:
simpa using le_of_add_le_add_left

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

Goal state before:
pp: α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
⊢ ↑(f 1) = 1

Tactic:
map_one,

Goal state after:
α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
⊢ ↑1 = 1
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
ha : a ≠ 0
⊢ b < d

Tactic:
rw [← inv_le_inv₀ ha.pos hc] at hh

Goal state after:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : a⁻¹ ≤ c⁻¹
ha : a ≠ 0
⊢ b < d
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ x.log < y.log ↔ x < y

Tactic:
by
  rw [log_lt_iff_lt_exp hx, exp_log hy]

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

Goal state before:
pp: case inr
y x : Multiplicative ℤ
⊢ ↑x < ↑y * exp 1 ↔ ↑x ≤ ↑y

Tactic:
← log_le_log,

Goal state after:
case inr
y x : Multiplicative ℤ
⊢ ↑x < ↑y * exp 1 ↔ (↑x).log ≤ (↑y).log

case inr.hx
y x : Multiplicative ℤ
⊢ ↑x ≠ 0

case inr.hy
y x : Multiplicative ℤ
⊢ ↑y ≠ 0
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case succ
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)

Tactic:
let n := k.succ
    have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))
    have h2 := add_nonneg hx hy
    calc
      x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := by
        rw [pow_succ' _ n, pow_succ' _ n]
        exact le_add_of_nonneg_right h1
      _ = (x + y) * (x ^ n + y ^ n) := by
        rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
          add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
      _ ≤ (x + y) ^ (n + 1) := by
        rw [pow_succ' _ n]
        gcongr; exact ih (Nat.succ_ne_zero k)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s

Tactic:
have : ∀ b ∈ s, b < a → f a < f b := by
    intro b hb hab
    cases (ha _ hb).not_gt hab

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f a < f b
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
⊢ image2 (fun b a ↦ f a b) t s ∪ image2 (fun b a ↦ f a b) t' s = image2 f s t ∪ image2 f s t'

Tactic:
image2_swap f,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
⊢ image2 (fun b a ↦ f a b) t s ∪ image2 (fun b a ↦ f a b) t' s = image2 (fun a b ↦ f b a) t s ∪ image2 f s t'
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 α
⊢ (fun a ↦ f a b) '' s = s

Tactic:
funext h,

Goal state after:
α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
s : Set α
⊢ (fun x ↦ x) '' s = s
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hg : Monotone g
⊢ BddAbove (range fun x ↦ g (f x))

Tactic:
change BddAbove (range (g ∘ f))
  simpa only [Set.range_comp] using hg.map_bddAbove hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : α
⊢ IsLUB (⇑f ⁻¹' s) x ↔ IsLUB s (f x)

Tactic:
rw [← f.symm_symm, ← image_eq_preimage_symm, isLUB_image]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ t
hxz : x ≤ z
hyz : y ≤ z
w : α
hw : w ∈ s
hzw : z ≤ w
⊢ ∃ z ∈ s, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
exact ⟨w, hw, hxz.trans hzw, hyz.trans hzw⟩

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

Goal state before:
pp: case pos.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ Ioc a b ⊆ s

Tactic:
← Ioc_sdiff_right,

Goal state after:
case pos.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioc a b \ {b} ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ Ioc a b ⊆ s
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionSemiring α
x✝³ x✝² : α
x✝¹ x✝ : ℕ
h : IsNNRat (x✝³ * x✝²⁻¹) x✝¹ x✝
⊢ IsNNRat (x✝³ / x✝²) x✝¹ x✝

Tactic:
simpa [div_eq_mul_inv] using h

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

Goal state before:
pp: α : Type u
inst✝ : DivisionRing α
x✝³ x✝² : α
x✝¹ : ℤ
x✝ : ℕ
h : IsRat (x✝³ * x✝²⁻¹) x✝¹ x✝
⊢ IsRat (x✝³ / x✝²) x✝¹ x✝

Tactic:
simpa [div_eq_mul_inv] using h

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

Goal state before:
pp: α : Type u
x y : List α
n : ℕ
⊢ take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length

Tactic:
by
  simp [take_append, Nat.sub_eq_zero_iff_le, Or.comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (a✝ :: l₁✝).reverse (b✝ :: l₂✝).reverse

Tactic:
by
    simp only [reverse_cons]
    exact rel_append (rel_reverse h₂) (Forall₂.cons h₁ Forall₂.nil)

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

Goal state before:
pp: case inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 = |q - r|
⊢ |q - r| * ↑n * max |q| |r| ^ (n - 1) < ε

pp: case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q - r| * ↑n * max |q| |r| ^ (n - 1) < ε

Tactic:
· simpa only [← h, zero_mul] using hε

Goal state after:
case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q - r| * ↑n * max |q| |r| ^ (n - 1) < ε
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons.inl
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ a :: l
comm : ∀ (x : M), x ∈ a :: l → ∀ (y : M), y ∈ a :: l → x * y = y * x
⊢ a * ((a :: l).erase a).prod = (a :: l).prod

pp: case cons.inr
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
⊢ a * ((b :: l).erase a).prod = (b :: l).prod

Tactic:
· simp only [erase_cons_head, prod_cons]

Goal state after:
case cons.inr
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
⊢ a * ((b :: l).erase a).prod = (b :: l).prod
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q r : ℚ
⊢ q / r = q.num * ↑r.den /. (↑q.den * r.num)

Tactic:
← divInt_div_divInt,

Goal state after:
q r : ℚ
⊢ q / r = q.num /. ↑q.den / (r.num /. ↑r.den)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
p q : α → Bool
l : List α
⊢ filter p (filter q l) = filter q (filter p l)

Tactic:
by
  simp [Bool.and_comm]

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

Goal state before:
pp: a : ℤ
ha : 0 ≤ a
b : ℕ
⊢ 0 ≤ mkRat a b

Tactic:
simpa using divInt_nonneg ha (Int.natCast_nonneg _)

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

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ (divNat q.den q.num).num = q.den

Tactic:
divNat,

Goal state after:
q : ℚ≥0
hq : q ≠ 0
⊢ num ⟨Rat.divInt ↑q.den ↑q.num, ⋯⟩ = q.den
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ (divNat q.den q.num).den = q.num

Tactic:
divNat,

Goal state after:
q : ℚ≥0
hq : q ≠ 0
⊢ den ⟨Rat.divInt ↑q.den ↑q.num, ⋯⟩ = q.num
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
⊢ ↑q.num / ↑q.den = q

Tactic:
ext1

Goal state after:
q : ℚ≥0
⊢ ↑(↑q.num / ↑q.den) = ↑q
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
x y : α
inst✝ : Nontrivial α
h : IsRelPrime x y
⊢ x = 0 → y ≠ 0

Tactic:
rintro rfl rfl; exact not_isRelPrime_zero_zero h

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:
by
    rw [if_pos (succ_pos m)]
    rfl

Goal state after:
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:
rwa [Int.cast_natCast]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ k * (e1 * e2) = t1 * t2

Tactic:
rw [← h3, mul_comm n1, mul_assoc n2, ← mul_assoc n1, h1,
      ← mul_assoc n2, mul_comm n2, mul_assoc, h2]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b✝ b : ℕ
x✝ : 0 < b + 1
⊢ 0 ^ (b + 1) = 0

Tactic:
simp [pow_succ]

Goal state after:
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 : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, ∀ y ∈ t, y ≤ u₂ x b

Tactic:
← hb₀,

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 : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, b₀ ≤ u₂ x b
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
⊢ (⋃ y, range fun s ↦ ↑(f s y)) = ⋃₀ C

Tactic:
ext x; constructor
  · rintro ⟨s, ⟨y, rfl⟩, ⟨s, hs⟩, rfl⟩
    refine ⟨_, hs, ?_⟩
    exact (f ⟨s, hs⟩ y).2
  · rintro ⟨s, hs, hx⟩
    obtain ⟨y, hy⟩ := hf ⟨s, hs⟩ ⟨x, hx⟩
    refine ⟨_, ⟨y, rfl⟩, ⟨s, hs⟩, ?_⟩
    exact congr_arg Subtype.val hy

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a : α
inst✝ : SemilatticeSup α
x y : ↑(Iic a)
⊢ Codisjoint x y ↔ ↑x ⊔ ↑y = a

Tactic:
by
  simpa only [_root_.codisjoint_iff] using! Iic.eq_top_iff

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ ↑(sInf s) = sInf ((fun a ↦ ↑a) '' s)

Tactic:
obtain ⟨x, hx⟩ := hs
  change _ = ite _ _ _
  split_ifs with h
  · rcases h with h1 | h2
    · cases h1 (mem_image_of_mem _ hx)
    · exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim
  · rw [preimage_image_eq]
    exact Option.some_injective _

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ (n ∈ s ∧ ∀ a ∈ s, n ≤ a) → sInf s = n

Tactic:
· intro ⟨hn, hle⟩
    exact le_antisymm (csInf_le (OrderBot.bddBelow s) hn) (le_csInf hs hle)

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

Goal state before:
pp: case left
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
⊢ False

Tactic:
have ab := (h ⟨xa, xb⟩).1.trans xb

Goal state after:
case left
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
ab : a₂ < b₁
⊢ False
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
⊢ (s.PairwiseDisjoint fun a ↦ f a '' t) ↔ InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)

Tactic:
refine ⟨fun hs x hx y hy (h : f _ _ = _) => ?_, fun hs x hx y hy h => ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : s.PairwiseDisjoint fun a ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ x = y

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
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ Injective (Ι a)

Tactic:
simpa only [uIoc_comm] using uIoc_injective_right a

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
⊢ ∀ ⦃x : β⦄, x ∈ u → ∀ ⦃y : β⦄, y ∈ u → Icc x y ⊆ u

Tactic:
rintro x ⟨⟨y, yt, yx, ys⟩, -⟩ x' ⟨-, ⟨z, zt, x'z, zs⟩⟩ a ha
    exact ⟨⟨y, yt, yx.trans ha.1, ys⟩, ⟨z, zt, ha.2.trans x'z, zs⟩⟩

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
⊢ IsAntichain r' (⇑φ '' s)

Tactic:
intro b hb b' hb' h₁ h₂

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : b ∈ ⇑φ '' s
b' : β
hb' : b' ∈ ⇑φ '' s
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ¬∃ t, IsChain r s ∧ SuperChain r s t
⊢ IsChain r (SuccChain r s)

Tactic:
rw [exists_and_left] at h

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)
⊢ IsChain r (SuccChain r s)
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : ¬IsMaxChain r s
⊢ SuperChain r s (SuccChain r s)

Tactic:
simp only [IsMaxChain, _root_.not_and, not_forall, exists_prop] at hs₂

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
⊢ SuperChain r s (SuccChain r s)
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ range f ⊆ insert 1 (f '' mulSupport f)

Tactic:
by
  simpa only [range_subset_iff, mem_insert_iff, or_iff_not_imp_left] using!
    fun x (hx : x ∈ mulSupport f) ↦ mem_image_of_mem f hx

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1 - (k + 1)) ^ (k + 1) ≤ n.descFactorial (k + 1)

Tactic:
rw [descFactorial_succ, Nat.pow_succ, succ_sub_succ, Nat.mul_comm]

Goal state after:
n k : ℕ
⊢ (n - k) * (n - k) ^ k ≤ (n - k) * n.descFactorial k
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 1 - fract x ≤ fract x
this : 0 < fract x
⊢ |↑⌈x⌉ - x| = 1 - fract x

Tactic:
ceil_sub_self_eq this.ne.symm,

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 1 - fract x ≤ fract x
this : 0 < fract x
⊢ |1 - fract x| = 1 - fract x
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case mpr
k m : ℕ+
n : ℕ
h : ↑m = ↑k * n.succ
⊢ k ∣ m

Tactic:
use ⟨n.succ, n.succ_pos⟩

Goal state after:
case h
k m : ℕ+
n : ℕ
h : ↑m = ↑k * n.succ
⊢ m = k * ⟨n.succ, ⋯⟩
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ ⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1

Tactic:
by
  rw [le_antisymm_iff, le_floor, ← Int.lt_add_one_iff, floor_lt, Int.cast_add, Int.cast_one,
    and_comm]

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

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ ∃ z, fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z

Tactic:
use z - y

Goal state after:
case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) = ↑(z - y)
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:
simp only [invOf_eq_inv, ← div_eq_mul_inv, Int.cast_id]

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

Tactic:
simp only [invOf_eq_inv, ← div_eq_mul_inv, Int.cast_id]

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)
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddCommMonoidWithOne G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H 1 b
f : F
n : ℕ
x : G
⊢ f (↑n + x) = f x + n • b

Tactic:
simpa using map_nsmul_add f n x

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

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
⊢ ∃! k, 1 ≤ g / a ^ k ∧ g / a ^ k < a

Tactic:
simpa only [one_le_div', zpow_add_one, div_lt_iff_lt_mul'] using
    existsUnique_zpow_near_of_one_lt ha g

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

Goal state before:
pp: case h
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ y ^ (-↑N) ≤ x

Tactic:
rw [zpow_neg y ↑N, zpow_natCast]

Goal state after:
case h
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ (y ^ N)⁻¹ ≤ x