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

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a b : α
⊢ |a| ∣ b ↔ a ∣ b

Tactic:
rcases abs_choice a with h | h <;> simp only [h, neg_dvd]

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
n : ℕ
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n

Tactic:
by
  simp [← pow_eq_pow_iff_of_ne_zero hn]

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst✝³ : EquivLike E { x // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
⊢ (if h : p i then update v j x (e ⟨i, h⟩) else w i) =
    update (fun i ↦ if h : p i then v (e ⟨i, h⟩) else w i) (↑(EquivLike.inv e j)) x i

Tactic:
by_cases h : p i

Goal state after:
case pos
α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst✝³ : EquivLike E { x // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ (if h : p i then update v j x (e ⟨i, h⟩) else w i) =
    update (fun i ↦ if h : p i then v (e ⟨i, h⟩) else w i) (↑(EquivLike.inv e j)) x i

case neg
α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst✝³ : EquivLike E { x // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : ¬p i
⊢ (if h : p i then update v j x (e ⟨i, h⟩) else w i) =
    update (fun i ↦ if h : p i then v (e ⟨i, h⟩) else w i) (↑(EquivLike.inv e j)) x i
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ a
hb : 1 ≤ b
⊢ a / b ≤ a

Tactic:
simpa only [div_one] using div_le_div_of_nonneg_left ha zero_lt_one hb

Goal state after:
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 * e) ≤ c / (d * e)

Tactic:
rw [div_mul_eq_div_mul_one_div, 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
x : List α
m n : ℕ
⊢ take n (drop m x) ++ drop (m + n) x = drop m x

Tactic:
← drop_drop,

Goal state after:
α : Type u
x : List α
m n : ℕ
⊢ take n (drop m x) ++ drop n (drop m x) = drop m x
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
i j : ℕ
xs : List α
⊢ (dropSlice i j xs).length = xs.length - min j (xs.length - i)

Tactic:
induction xs generalizing i j with

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a - a / 2 = a / 2

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a / 2 - a = -(a / 2)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : a * b < c
⊢ ∃ b' > b, a * b' < c

Tactic:
simp_rw [mul_comm a] at hc ⊢; exact exists_mul_left_lt₀ hc

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

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

Tactic:
by
  grind

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂) → ∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂

pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂) → ∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂

Tactic:
· rintro ⟨l1, h1, h2⟩
    obtain ⟨l', hl1, rfl⟩ := sublist_map_iff.mp h2
    use l'
    simpa [hl1] using h1

Goal state after:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂) → ∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ l.concat a = (a :: l.reverse).reverse

Tactic:
by
  grind

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

Goal state before:
pp: M : Type u_1
inst✝ : Div M
l l_n l_d n d : M
h : l = l_n / l_d
hn : l_n = n
hd : l_d = d
⊢ n / l_d = n / d

Tactic:
hd

Goal state after:
M : Type u_1
inst✝ : Div M
l l_n l_d n d : M
h : l = l_n / l_d
hn : l_n = n
hd : l_d = d
⊢ n / d = n / d
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
a b : α
⊢ a :: l₁ <+ b :: l₂ ↔ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

Tactic:
by
  grind

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

Goal state before:
pp: case nil
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a : α
hf : ∀ (a' : α), a' ≠ a → a' ∈ [] → f a' = 1
⊢ 1 = f a ^ count a []

Tactic:
count_nil,

Goal state after:
case nil
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a : α
hf : ∀ (a' : α), a' ≠ a → a' ∈ [] → f a' = 1
⊢ 1 = f a ^ 0
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ idxOf a l = l.length ↔ ¬a ∈ l

Tactic:
by
  grind

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

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

Tactic:
by rwa [take_eraseIdx_eq_take_of_le l i i (Nat.le_refl i)] at a'_mem

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

Goal state before:
pp: case pos
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. d) = n /. d

Tactic:
hd

Goal state after:
case pos
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. 0) = n /. 0
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: case true
m e : ℕ
⊢ 0 ≤ if true = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

Tactic:
grind [normalize_eq_mkRat, Rat.mkRat_nonneg]

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

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

Tactic:
dsimp [div, modDiv]

Goal state after:
m k : ℕ+
⊢ (k.modDivAux (↑m % ↑k) (↑m / ↑k)).snd = if ↑m % ↑k = 0 then ↑m / ↑k - 1 else ↑m / ↑k
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p = ↑q
⊢ p = q

Tactic:
rw [NNRat.cast_def, NNRat.cast_def, Commute.div_eq_div_iff] at hpq

Goal state after:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ p = q

case hbd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ Commute ↑p.den ↑q.den

case hb
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ ↑p.den ≠ 0

case hd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ ↑q.den ≠ 0
Module: Mathlib.Tactic.FieldSimp

Goal state before:
pp: «$v» : Level
«$M» : Type v
«$iM» : CommGroupWithZero «$M»
«$r» : ℤ
«$x» : «$M»
$snd✝ : ℕ
«$e» : «$M»
«$pf» : zpow' «$x» «$r» = «$e»
⊢ NF.eval [] * zpow' («$r», «$x»).2 («$r», «$x»).1 = «$e»

Tactic:
exact Eq.trans (one_mul _) pf

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

Goal state before:
pp: n✝¹ num✝ n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsNNRat (NNRat.divNat ↑n✝¹ ↑n✝) num✝ denom✝

Tactic:
rw [NNRat.divNat_eq_div]

Goal state after:
n✝¹ num✝ n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsNNRat (↑↑n✝¹ / ↑↑n✝) num✝ denom✝
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: m n : ℤ
hn : n ≠ 0
⊢ (↑m / ↑n).den = 1 ↔ n ∣ m

Tactic:
by
  replace hn : (n : ℚ) ≠ 0 := num_ne_zero.mp hn
  constructor
  · rw [Rat.den_eq_one_iff, eq_div_iff hn]
    exact mod_cast (Dvd.intro_left _)
  · exact (intCast_div _ _ · ▸ rfl)

Goal state after:
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:
by
  grind

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

Goal state before:
pp: case inl
R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hbc : b ≤ c
⊢ a * (b - c) = a * b - a * c

Tactic:
rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_right hbc a)]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
a b : α
c d : Set α
hs : ∀ e ∈ c, e ≤ a
ht : ∀ e ∈ d, e ≤ b
hd : Disjoint a b
he : ⊥ ∉ c ∨ ⊥ ∉ d
⊢ Disjoint c d

Tactic:
by
  grind

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

Goal state before:
pp: β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
p : x ∈ ⊤
⊢ ∃ i ∈ t, x ∈ s i

Tactic:
← w,

Goal state after:
β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
p : x ∈ ⋃ i ∈ t, s i
⊢ ∃ i ∈ t, x ∈ s i
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, t ∩ f i = (⋂ i ∈ s, f i) ∩ t

Tactic:
← biInter_inter hs

Goal state after:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, t ∩ f i = ⋂ i ∈ s, f i ∩ t
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : S ⊆ {∅, univ}
⊢ ⋃₀ S ∈ {∅, univ}

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ ⋃ i, f i = univ ↔ ∀ (x : α), ∃ i, x ∈ f i

Tactic:
simp only [eq_univ_iff_forall, mem_iUnion]

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

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
i : ι
hi : f i = ⊥
i₀ : ι
hi₀ : f i₀ ≠ ⊥
⊢ ∃ i', ⊥ ≤ f ↑i'

Tactic:
exact ⟨⟨i₀, hi₀⟩, bot_le⟩

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ (∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x

Tactic:
← exists_prop,

Goal state after:
α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ (∃ x, ∃ (_ : x ∈ ⋃₀ S), p x) ↔ ∃ s, ∃ (_ : s ∈ S), ∃ x, ∃ (_ : x ∈ s), p x
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h2 : ¬BddBelow ((fun a ↦ ↑a) '' s)
⊢ ↑(sInf s) = ⊤

Tactic:
exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi b ⊂ Ioi a ↔ a < b

Tactic:
by
  refine ⟨fun h => ?_, Ioi_ssubset_Ioi⟩
  obtain ⟨_, c, ac, cb⟩ := ssubset_iff_exists.mp h
  exact ac.trans_le (le_of_not_gt cb)

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

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

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : c ≤ max a b
⊢ Ico a b ∪ Ici c = Ici (min a c)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : c ≤ max a b
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : c ≤ max a b
⊢ Icc a b ∪ Ici c = Ici (min a c)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b c d : α
h : min c d ≤ b
⊢ Iio b ∪ Ico c d = Iio (max b d)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b c d : α
h : min c d < b
⊢ Iic b ∪ Ioc c d = Iic (max b d)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b c d : α
h : min c d < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b c d : α
h : min c d ≤ b
⊢ Iic b ∪ Icc c d = Iic (max b d)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : c ≤ b
h₂ : a ≤ d
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : c < b
h₂ : a < d
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ico a₁ b₁ ∩ Ico a₂ b₂ = Ico (max a₁ a₂) (min b₁ b₂)

Tactic:
by
  grind

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

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

Tactic:
by
  grind

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

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

Tactic:
by
  grind

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

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

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₁ < b₂
⊢ Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioc (max a₁ a₂) b₁

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₂ ≤ b₁
⊢ Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (max a₁ a₂) b₂

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₁ ≤ b₂
⊢ Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioo (max a₁ a₂) b₁

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₂ < b₁
⊢ Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (max a₁ a₂) b₂

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ico a b \ Iio c = Ico (max a c) b

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioc a b \ Ioi c = Ioc a (min b c)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioc a b ∩ Ioi c = Ioc (max a c) b

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ico a b ∩ Iio c = Ico a (min b c)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioc a b \ Iic c = Ioc (max a c) b

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (Ioc a b)ᶜ = Iic a ∪ Ioi b

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Iic b \ Ioc a b = Iic (min a b)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi a \ Ioc a b = Ioi (max a b)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
hab : a ≤ b
⊢ Iic b \ Ioc a b = Iic a

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioc a b ∪ Ioc a c = Ioc a (max b c)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioc a c ∪ Ioc b c = Ioc (min a b) c

Tactic:
by
  grind

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

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

Tactic:
by
  grind

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

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

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
ha : a ≤ c
hb : b ≤ c
⊢ a ∉ Ι b c → b ∉ Ι a c → a = b

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxChain r c
t : Set β
ht : IsChain s t
hf : ⇑e '' c ⊆ t
⊢ ⇑e '' c = t

Tactic:
rw [← e.coe_fn_toEquiv, ← e.toEquiv.eq_preimage_iff_image_eq, ← Equiv.image_symm_eq_preimage]
    exact hc.2 (ht.image e.symm) ((e.toEquiv.subset_symm_image _ _).2 hf)

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
⊢ ¬Nonempty α ↔ ¬s.Nonempty

Tactic:
by simpa [Set.not_nonempty_iff_eq_empty] using h.isEmpty_iff

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
⊢ ¬Nonempty α ↔ ¬s.Nonempty

Tactic:
by simpa [Set.not_nonempty_iff_eq_empty] using h.isEmpty_iff

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

Goal state before:
pp: α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
num den : ℕ
ra : IsRat a (Int.negOfNat num) den
⊢ IsNNRat |a| num den

Tactic:
obtain ⟨ha1, rfl⟩ := ra
  simp only [Int.cast_negOfNat, neg_mul, abs_neg]
  refine ⟨ha1, abs_of_nonneg ?_⟩
  apply mul_nonneg
  · exact Nat.cast_nonneg' num
  · simp only [invOf_eq_inv, inv_nonneg, Nat.cast_nonneg]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = if a < 1 then a⁻¹ else 1

Tactic:
grind [leOnePart_eq_ite, inv_one]

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommMonoid β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
a : α
⊢ 0 ≤ f a + f a

Tactic:
← map_one_eq_zero f,

Goal state after:
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommMonoid β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
a : α
⊢ f 1 ≤ f a + f a
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case neg
n k : ℕ
h : ¬n < k
⊢ n.descFactorial k = (n - k + 1).ascFactorialBinary k

Tactic:
· rw [← ascFactorial_eq_ascFactorialBinary, ← add_descFactorial_eq_ascFactorial']
    grind

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

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

Tactic:
rw [add_coe, sub_coe, if_pos h]

Goal state after:
a b : ℕ+
h : a < b
⊢ ↑a + (↑b - ↑a) = ↑b
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑m > 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k

Tactic:
← Nat.mod_add_div (m : ℕ) (k : ℕ),

Goal state after:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑m % ↑k + ↑k * (↑m / ↑k) > 0
⊢ ↑k ≤ ↑m % ↑k + ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
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
⊢ k * ↑n ≤ k * ↑n + 1 ∧ k * ↑n + 1 < k * (↑n + 1)

Tactic:
simp [mul_add, hk]

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

Goal state before:
pp: case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m / ↑n - ↑(m % n) / ↑n = ↑(↑m / ↑n)

Tactic:
· rw [sub_eq_iff_eq_add', ← mul_right_inj' hn'.ne', mul_div_cancel₀ _ hn'.ne', mul_add,
      mul_div_cancel₀ _ hn'.ne']
    norm_cast
    rw [← Nat.cast_add, Nat.mod_add_div m n]

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

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
⊢ q⁻¹ = q_inv

Tactic:
q_inv_def,

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⁻¹ = ↑q.den / ↑q.num
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ count a s = s.card ↔ ∀ (x : α), x ∈ s → a = x

Tactic:
by
  simp [countP_eq_card, count, @eq_comm _ a]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
l : List α
⊢ Quot.mk (⇑(isSetoid α)) l ≤ {a} ↔ Quot.mk (⇑(isSetoid α)) l = 0 ∨ Quot.mk (⇑(isSetoid α)) l = {a}

Tactic:
simp only [← coe_singleton, quot_mk_to_coe'', coe_le,
    coe_eq_zero, coe_eq_coe, perm_singleton, subperm_singleton_iff]

Goal state after: