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

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n

Tactic:
have ⟨a_n, b_n, eq⟩ := dvd

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case mp
a b : ℤ
n : ℕ
⊢ a.gcd b ∣ n → ∃ x y, ↑n = a * x + b * y

Tactic:
intro h
    rw [← Nat.mul_div_cancel' h, Int.natCast_mul, gcd_eq_gcd_ab, Int.add_mul, mul_assoc, mul_assoc]
    exact ⟨_, _, rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b = 1
⊢ b * a = a

Tactic:
by rw [h, one_mul]

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

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

Tactic:
← zero_add a

Goal state after:
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
h : ⊤ = 0
a : α
ha : 0 + a ≠ 0
⊢ False
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ 0 ≤ ⌈a⌉

Tactic:
← FloorRing.intCast_strictMono.le_iff_le (β := α),

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ ↑0 ≤ ↑⌈a⌉
Module: Mathlib.Algebra.Order.Floor.Defs

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

Tactic:
← FloorRing.intCast_strictMono.le_iff_le (β := α),

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : a ≤ 0
⊢ ↑⌊a⌋ ≤ ↑0
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
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : 0 ≤ a
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
floor_lt ha

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : 0 ≤ a
⊢ a < ↑⌈b⌉₊
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a b : R
⊢ Nat.cast ⁻¹' Ico a b = Ico ⌈a⌉₊ ⌈b⌉₊

Tactic:
by
  ext
  simp [ceil_le, lt_ceil]

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

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
rw [floor_of_nonpos (tsub_nonpos_of_le h), eq_comm, tsub_eq_zero_iff_le]

Goal state after:
case inr.inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a⌋₊ ≤ n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ |a - ↑⌈a⌉₊| ≤ 1

Tactic:
refine abs_le.mpr ⟨?_, ?_⟩
  · simpa using (ceil_lt_add_one ha).le
  · simpa using (le_ceil a).trans (le_add_of_nonneg_left zero_le_one)

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

Goal state before:
pp: case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ ↑n ≤ a ↔ n ≤ FloorSemiring.floor a

pp: case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ 0 ≤ a

Tactic:
H₂.gc_floor

Goal state after:
case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ ↑n ≤ a ↔ ↑n ≤ a

case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ 0 ≤ a

case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
n : ℕ
⊢ 0 ≤ a
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.bot
α : Type u_1
inst✝ : LE α
⊢ ⊤ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ WithTop.ofDual ⊤

Tactic:
simp [le_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ ⊤ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ WithTop.ofDual ⊤

Tactic:
simp [le_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ ↑a✝ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ WithTop.ofDual ↑a✝

Tactic:
simp [le_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : αᵒᵈ
a✝ : α
⊢ ↑a✝¹ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ WithTop.ofDual ↑a✝¹

Tactic:
simp [le_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.bot
α : Type u_1
inst✝ : LE α
⊢ ⊤ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ WithTop.toDual ⊤

Tactic:
simp [le_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.coe
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ ⊤ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ WithTop.toDual ⊤

Tactic:
simp [le_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ ↑a✝ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ WithTop.toDual ↑a✝

Tactic:
simp [le_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : α
a✝ : αᵒᵈ
⊢ ↑a✝¹ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ WithTop.toDual ↑a✝¹

Tactic:
simp [le_toDual]

Goal state after:
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
h : ⅟(a + b) = ⅟a + ⅟b
h' : -1 = ⅟a * b + ⅟b * a
h_a_binv_a : -(b + a) = a * ⅟b * a
h_b_ainv_b : -(a + b) = b * ⅟a * b
⊢ a * ⅟b * a = b * ⅟a * b

Tactic:
rw [← h_a_binv_a, ← h_b_ainv_b, add_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b - c
⊢ a ∣ b - c + c ↔ a ∣ c

Tactic:
dvd_add_right h

Goal state after:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b - c
⊢ a ∣ c ↔ a ∣ c
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMono (s.domRestrict f) ↔ StrictMonoOn f s

Tactic:
by
  simp [Set.domRestrict, StrictMono, StrictMonoOn]

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ ∀ {a b : Antisymmetrization (α × β) fun x1 x2 ↦ x1 ≤ x2},
    { toFun := Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯, invFun := uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯),
            left_inv := ⋯, right_inv := ⋯ }
          a ≤
        { toFun := Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯,
            invFun := uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯), left_inv := ⋯, right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
by rintro ⟨_⟩ ⟨_⟩; rfl

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
⊢ ⇑(prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u

Tactic:
simpa only [Equiv.image_eq_preimage_symm] using! prod_assoc_preimage

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ↑s ⊕ ↑(t \ s ∪ s ∩ t) ≃ ↑s ⊕ ↑t

Tactic:
by
      { rw [(_ : t \ s ∪ s ∩ t = t)]
        rw [union_comm, inter_comm, inter_union_sdiff] }

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
⊢ BijOn (⇑(swap a b)) s s

Tactic:
grind [Equiv.bijOn]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : ¬b ∈ s
⊢ BijOn (⇑(swap a b)) s (insert b (s \ {a}))

Tactic:
grind [Equiv.bijOn]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : Invertible a
⊢ ⅟a ≤ 0 ↔ a ≤ 0

Tactic:
simp only [← not_lt, invOf_pos]

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

Goal state before:
pp: case pos
α : 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
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

Tactic:
refine Or.inl (Subset.antisymm hc ?_)
    rwa [← Ico_sdiff_left, sdiff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_sdiff_right,
      sdiff_singleton_subset_iff, insert_eq_of_mem hb] at ho

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
⊢ 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:
refine ⟨fun h ↦ ?_, ?_⟩
  · 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⟩
  · rintro (⟨hs, hts⟩ | ⟨ht, hst⟩) x hx y hy
    · obtain ⟨x', hx', hxx'⟩ := hts.union_right hx
      obtain ⟨y', hy', hyy'⟩ := hts.union_right hy
      obtain ⟨z, hz, hx'z, hy'z⟩ := hs x' hx' y' hy'
      exact ⟨z, .inl hz, hxx'.trans hx'z, hyy'.trans hy'z⟩
    · obtain ⟨x', hx', hxx'⟩ := hst.union_left hx
      obtain ⟨y', hy', hyy'⟩ := hst.union_left hy
      obtain ⟨z, hz, hx'z, hy'z⟩ := ht x' hx' y' hy'
      exact ⟨z, .inr hz, hxx'.trans hx'z, hyy'.trans hy'z⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ IsGLB ∅ a ↔ IsTop a

Tactic:
by
  simp [IsGLB]

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 : α
h : a * b / c ≤ d
hc : 0 < c
⊢ b * a ≤ d * c

Tactic:
rwa [mul_comm b, ← div_le_iff₀ hc]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
B ε : α
hε : 0 < ε
n : ℕ
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
wlog! B_pos : 0 < B generalizing B
  · have ⟨δ, δ_pos, cont⟩ := this 1 zero_lt_one
    exact ⟨δ, δ_pos, fun q r hr ↦ cont q r (hr.trans (B_pos.trans zero_le_one))⟩
  have pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1) := zero_lt_one.trans_le <| le_add_of_nonneg_right <|
    mul_nonneg n.cast_nonneg <| (pow_pos (B_pos.trans <| lt_add_of_pos_right _ zero_lt_one) _).le
  refine ⟨min 1 (ε / (1 + n * (B + 1) ^ (n - 1))), lt_min zero_lt_one (div_pos hε pos),
    fun q r hr hqr ↦ (abs_pow_sub_pow_le ..).trans_lt ?_⟩
  rw [le_inf_iff, le_div_iff₀ pos, mul_one_add, ← mul_assoc] at hqr
  obtain h | h := (abs_nonneg (q - r)).eq_or_lt
  · simpa only [← h, zero_mul] using hε
  refine (lt_of_le_of_lt ?_ <| lt_add_of_pos_left _ h).trans_le hqr.2
  gcongr
  · exact mul_nonneg (abs_nonneg _) n.cast_nonneg
  · exact (abs_nonneg _).trans le_sup_left
  refine max_le ?_ (hr.trans <| le_add_of_nonneg_right zero_le_one)
  exact add_sub_cancel r q ▸ (abs_add_le ..).trans (add_le_add hr hqr.1)

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
⊢ zpow' a (-n) = (zpow' a n)⁻¹

Tactic:
simp +contextual [zpow', apply_ite]
  split_ifs with h
  · tauto
  · tauto

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

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
a : α
ha : a ∈ s
a' : α
ha' : a' ∈ t
ha'' : f a' ⋯ = f a ⋯
⊢ False

Tactic:
apply h ha

Goal state after:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
a : α
ha : a ∈ s
a' : α
ha' : a' ∈ t
ha'' : f a' ⋯ = f a ⋯
⊢ a ∈ t
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q : ℚ
hq : 0 ≤ q
hp : 0 ≤ p
⊢ ↑(q + p).toNNRat = ↑(q.toNNRat + p.toNNRat)

Tactic:
simp [toNNRat, hq, hp, add_nonneg]

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

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

Tactic:
← den_coe,

Goal state after:
q : ℚ≥0
⊢ ↑q * ↑↑(↑q).den = ↑q.num
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»
⊢ ((«$r», «$x») ::ᵣ []).eval = «$e»

Tactic:
rw [NF.eval_cons]

Goal state after:
«$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»
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: α β : Type u_2
inst : CSLift α β
a b : α
a' b' : β
h1 : CSLiftVal a a'
h2 : CSLiftVal b b'
h : a' = b'
⊢ a' = CSLift.lift b

Tactic:
← h2.1

Goal state after:
α β : Type u_2
inst : CSLift α β
a b : α
a' b' : β
h1 : CSLiftVal a a'
h2 : CSLiftVal b b'
h : a' = b'
⊢ a' = b'
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋂ i, ⋂ j, s i j) ∪ t = ⋂ i, ⋂ j, s i j ∪ t

Tactic:
by simp_rw [iInter_union]

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

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

Tactic:
by
  simp [nonempty_iff_ne_empty, iInter_eq_empty_iff]

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
    ∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ ∃ c, c ∈ s ∧ a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
by
  simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, and_assoc, exists_and_left,
    not_monotone_not_antitone_iff_exists_lt_lt, @and_left_comm (_ ∈ s)]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ sSup s ∆ a ≤ sSup ((fun x ↦ x ∆ a) '' s)

Tactic:
rw [sSup_image', sSup_eq_iSup']
  have : Nonempty s := Set.nonempty_coe_sort.mpr hs
  exact iSup_symmDiff_le

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
⊢ Frame α

Tactic:
let completeLattice := e.completeLattice

Goal state after:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
⊢ Frame α
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
⊢ Coframe α

Tactic:
let completeLattice := e.completeLattice

Goal state after:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
⊢ Coframe α
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h : a < b ∨ c < d
⊢ Ico a b = Ico c d ↔ a = c ∧ b = d

Tactic:
refine ⟨fun h ↦ ?_, by grind⟩
  have : c ≤ a ∧ b ≤ d := (Ico_subset_Ico_iff (show a < b by grind [Set.nonempty_Ico])).1 h.subset
  have : a ≤ c ∧ d ≤ b := (Ico_subset_Ico_iff (show c < d by grind)).1 h.superset
  grind

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
⊢ CompleteDistribLattice α

Tactic:
let completeLattice := e.completeLattice

Goal state after:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
⊢ CompleteDistribLattice α
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
⊢ CompleteBooleanAlgebra α

Tactic:
let completeLattice := e.completeLattice

Goal state after:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
⊢ CompleteBooleanAlgebra α
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
⊢ CompleteBooleanAlgebra α

Tactic:
apply e.injective.completeBooleanAlgebra <;> intros

Goal state after:
case le
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a

case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a

case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := ⋯
booleanAlgebra : BooleanAlgebra α := ⋯
⊢ e ⊤ = ⊤

case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := ⋯
booleanAlgebra : BooleanAlgebra α := ⋯
⊢ e ⊥ = ⊥

case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b

Tactic:
uIoc_eq_union,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∈ Ioc b c ∪ Ioc c b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (Ι a b).Nonempty ↔ a ≠ b

Tactic:
simp [uIoc, eq_comm]

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

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ {a}.OrdConnected

Tactic:
← Icc_self

Goal state after:
α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ (Icc a a).OrdConnected
Module: Mathlib.Order.Preorder.Chain

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

Tactic:
exact (succChain_spec h).2.1

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

Goal state before:
pp: a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
⊢ a / b = -(a / -b)

Tactic:
← Int.ediv_neg,

Goal state after:
a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
⊢ a / b = a / - -b
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : 0 < n
⊢ (n - 1)! * n.ascFactorial k = (n + k - 1)!

Tactic:
rw [Nat.sub_add_comm h, Nat.sub_one]

Goal state after:
n k : ℕ
h : 0 < n
⊢ n.pred ! * n.ascFactorial k = (n.pred + k)!
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f x ≤ f y + f (y / x)

Tactic:
by
  simpa only [add_comm, map_div_rev, div_mul_cancel] using map_mul_le_add f (x / y) y

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

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
hx' : 2 * x ∉ range Int.cast
⊢ round x = ⌈2 * x⌉ / 2

Tactic:
rw [round_eq_div, (ceil_eq_floor_add_one_iff_notMem _).mpr hx']

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

Goal state before:
pp: a b : ℕ+
⊢ ↑(a - b) ≤ ↑a

Tactic:
sub_coe

Goal state after:
a b : ℕ+
⊢ (if b < a then ↑a - ↑b else 1) ≤ ↑a
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: a b : ℕ+
hab : a < b
⊢ ↑a ≤ ↑(b - 1)

Tactic:
sub_coe

Goal state after:
a b : ℕ+
hab : a < b
⊢ ↑a ≤ if 1 < b then ↑b - ↑1 else 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: 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) = fract a * ↑c - fract (a * ↑c) - ↑y

Tactic:
← hy

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) =
    fract a * ↑c - fract (a * ↑c) - (fract (a * ↑c + a) - fract (a * ↑c) - fract a)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : FloorRing k
a b : k
ha : a ≠ 0
⊢ b / a * a = b

Tactic:
div_mul_cancel₀ b ha

Goal state after:
k : Type u_4
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : FloorRing k
a b : k
ha : a ≠ 0
⊢ b = b