mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ : ↥S
⊢ (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = oreNum r₁ s₂ * r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : MulAction R X
inst✝ : One X
⊢ 1 = 1 /ₒ 1

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x✝ : M
⊢ (f.ofMulEquivOfLocalizations (MulEquiv.refl N)) x✝ = f x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
Q : Type u_4
inst✝ : CommMonoid Q
k : N ≃* P
j : P ≃* Q
x✝ : M
⊢ (f.ofMulEquivOfLocalizations (k.trans j)).toMonoidHom x✝ =
    (j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMonoidHom) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x✝ : M
⊢ (f.ofMulEquivOfDom ⋯) x✝ = f x✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LE α
x : α
⊢ (OrderRingIso.refl α) x = x

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
⊢ 1 /ₒ 1 = 1

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊤ = Option.bind ⊤ fun a ↦ Option.some (a * b)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : α
ha : a ≠ 0
⊢ ⊤ = Option.bind ⊤ fun b ↦ Option.some (a * b)

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mk.mk.succ
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
c : M
hc : c ∈ S
n : ℕ
hn : n + 1 ≠ 0
hab : c * (↑b.2 ^ (n + 1) * a.1 ^ (n + 1)) = c * (↑a.2 ^ (n + 1) * b.1 ^ (n + 1))
⊢ (fun a ↦ a ^ (n + 1)) (c * (↑b.2 * a.1)) = (fun a ↦ a ^ (n + 1)) (c * (↑a.2 * b.1))

Tactic:
simp [mul_pow, pow_succ c, mul_assoc, hab]

Goal state after:
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: case top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
⊢ ⊤ - ⊤ = ↑⊥

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: case coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝ : α
⊢ ↑a✝ - ⊤ = ↑⊥

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
x : X
s : ↥S
⊢ r • (x /ₒ s) = oreNum (r • 1) s • x /ₒ oreDenom (r • 1) s

Tactic:
rfl

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

Goal state before:
pp: case neg.top.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
⊢ (Option.bind (⊤ + ⊤) fun b ↦ Option.some (c * b)) =
    (Option.bind ⊤ fun b ↦ Option.some (c * b)) + Option.bind ⊤ fun b ↦ Option.some (c * b)

Tactic:
rfl

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

Goal state before:
pp: case neg.top.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (⊤ + ↑a✝) fun b ↦ Option.some (c * b)) =
    (Option.bind ⊤ fun b ↦ Option.some (c * b)) + Option.bind ↑a✝ fun b ↦ Option.some (c * b)

Tactic:
rfl

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

Goal state before:
pp: case neg.coe.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (↑a✝ + ⊤) fun b ↦ Option.some (c * b)) =
    (Option.bind ↑a✝ fun b ↦ Option.some (c * b)) + Option.bind ⊤ fun b ↦ Option.some (c * b)

Tactic:
rfl

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

Goal state before:
pp: case neg.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝¹ a✝ : α
⊢ (Option.bind (↑a✝¹ + ↑a✝) fun b ↦ Option.some (c * b)) =
    (Option.bind ↑a✝¹ fun b ↦ Option.some (c * b)) + Option.bind ↑a✝ fun b ↦ Option.some (c * b)

Tactic:
rfl

Goal state after:
case neg.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝¹ a✝ : α
⊢ (Option.bind (↑a✝¹ + ↑a✝) fun b ↦ Option.some (c * b)) =
    (Option.bind ↑a✝¹ fun b ↦ Option.some (c * b)) + Option.bind ↑a✝ fun b ↦ Option.some (c * b)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.top.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
⊢ (Option.bind (⊤ + ⊤) fun a ↦ Option.some (a * c)) =
    (Option.bind ⊤ fun a ↦ Option.some (a * c)) + Option.bind ⊤ fun a ↦ Option.some (a * c)

Tactic:
rfl

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

Goal state before:
pp: case neg.top.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (⊤ + ↑a✝) fun a ↦ Option.some (a * c)) =
    (Option.bind ⊤ fun a ↦ Option.some (a * c)) + Option.bind ↑a✝ fun a ↦ Option.some (a * c)

Tactic:
rfl

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

Goal state before:
pp: case neg.coe.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (↑a✝ + ⊤) fun a ↦ Option.some (a * c)) =
    (Option.bind ↑a✝ fun a ↦ Option.some (a * c)) + Option.bind ⊤ fun a ↦ Option.some (a * c)

Tactic:
rfl

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

Goal state before:
pp: case neg.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝¹ a✝ : α
⊢ (Option.bind (↑a✝¹ + ↑a✝) fun a ↦ Option.some (a * c)) =
    (Option.bind ↑a✝¹ fun a ↦ Option.some (a * c)) + Option.bind ↑a✝ fun a ↦ Option.some (a * c)

Tactic:
rfl

Goal state after:
case neg.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝¹ a✝ : α
⊢ (Option.bind (↑a✝¹ + ↑a✝) fun a ↦ Option.some (a * c)) =
    (Option.bind ↑a✝¹ fun a ↦ Option.some (a * c)) + Option.bind ↑a✝ fun a ↦ Option.some (a * c)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : Zero X
inst✝ : MulAction R X
⊢ 0 = 0 /ₒ 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[0] x ≤ g^[0] x

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ f^[0] x ≤ g^[0] x

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊥ = Option.bind ⊥ fun a ↦ Option.some (a * b)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : α
ha : a ≠ 0
⊢ ⊥ = Option.bind ⊥ fun b ↦ Option.some (a * b)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
⊢ a * x ≤ b * x

Tactic:
rcases eq_or_ne x 0 with rfl | x0'
    · simp
    lift x to α
    · rintro rfl
      exact (WithBot.bot_lt_coe (0 : α)).not_ge x0
    cases a
    · simp_rw [bot_mul x0', bot_le]
    cases b
    · exact absurd h (bot_lt_coe _).not_ge
    simp only [← coe_mul, coe_le_coe] at *
    norm_cast at x0
    exact mul_le_mul_of_nonneg_right h x0

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
⊢ Contravariant { x // 0 ≤ x } (WithBot α) (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 < x2

Tactic:
intro ⟨x, x0⟩ a b h
    simp only at h
    rcases eq_or_ne x 0 with rfl | x0'
    · simp at h
    lift x to α
    · rintro rfl
      exact (WithBot.bot_lt_coe (0 : α)).not_ge x0
    cases b
    · rw [bot_mul x0'] at h
      exact absurd h bot_le.not_gt
    cases a
    · exact WithBot.bot_lt_coe _
    simp only [← coe_mul, coe_lt_coe] at *
    norm_cast at x0
    exact lt_of_mul_lt_mul_right h x0

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccPrelimit b
⊢ (isSuccPrelimit b hb fun y x ↦
      ⋯.fix
        (fun a IH ↦
          if h : IsSuccPrelimit a then isSuccPrelimit a h IH
          else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
        y) =
    isSuccPrelimit b hb fun x x_1 ↦ prelimitRecOn x succ isSuccPrelimit

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
a : α
ha : ¬IsMax a
x : (a : α) → motive a
hc : ¬IsMax a
⊢ cast ⋯ (succ a ha (x a)) = succ a hc (x a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsMin b
⊢ limitRecOn b isMin succ isSuccLimit = isMin b hb

Tactic:
by
  rw [limitRecOn, prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccLimit b
⊢ (isSuccLimit b ⋯ fun x x_1 ↦
      prelimitRecOn x succ fun a ha IH ↦ if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) =
    isSuccLimit b hb fun x x_1 ↦ limitRecOn x isMin succ isSuccLimit

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
⊢ succ b ?hb (prelimitRecOn b succ fun a ha IH ↦ if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) =
    succ b hb (limitRecOn b isMin succ isSuccLimit)

pp: case hb
α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
⊢ ¬IsMax b

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < y
⊢ x + 1 ≤ y

Tactic:
rw [← succ_eq_add_one]

Goal state after:
α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < y
⊢ succ x ≤ y
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
x : α
⊢ x ⩿ x + 1

Tactic:
rw [← succ_eq_add_one]

Goal state after:
α : Type u_1
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
x : α
⊢ x ⩿ succ x
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
x : α
⊢ x ⋖ x + 1

Tactic:
rw [← succ_eq_add_one]

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
x : α
⊢ x ⋖ succ x
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ succ^[n] (EquivLike.inv f a) = EquivLike.inv f b → succ^[n] a = b

Tactic:
rw [← f.apply_eq_iff_eq, EquivLike.apply_inv_apply]

Goal state after:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ f (succ^[n] (EquivLike.inv f a)) = b → succ^[n] a = b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
n : ℕ
IH : ∀ {a : Y}, succ^[n] a = f (succ^[n] (EquivLike.inv f a))
a : Y
⊢ succ^[n + 1] a = f (succ^[n + 1] (EquivLike.inv f a))

Tactic:
simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_succ]

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∃ n, succ^[n] a = b

Tactic:
by
    refine (exists_succ_iterate_of_le ((map_inv_le_map_inv_iff f).mpr h)).imp ?_
    intro n
    rw [← f.apply_eq_iff_eq, EquivLike.apply_inv_apply]
    rintro rfl
    clear h
    induction n generalizing a with
    | zero => simp
    | succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_succ]

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ pred^[n] (EquivLike.inv f b) = EquivLike.inv f a → pred^[n] b = a

Tactic:
rw [← f.apply_eq_iff_eq, EquivLike.apply_inv_apply]

Goal state after:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ f (pred^[n] (EquivLike.inv f b)) = a → pred^[n] b = a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
⊢ sInf (Ioi ⊤) ≤ succ ⊤

Tactic:
succ_top

Goal state after:
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
⊢ sInf (Ioi ⊤) ≤ ⊤
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝⁴ : PartialOrder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x ⋖ y ↔ x + 1 = y

Tactic:
rw [← succ_eq_add_one]

Goal state after:
α : Type u_1
x y : α
inst✝⁴ : PartialOrder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x ⋖ y ↔ succ x = y
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : PartialOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ y + 1 < x

Tactic:
rw [← succ_eq_add_one]

Goal state after:
α : Type u_1
x y : α
inst✝³ : PartialOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ succ y < x
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : succ^[n] a ∈ s → f a ≤ f (succ^[n] a)
hb : succ (succ^[n] a) ∈ s
this : succ^[n] a ∈ s
hb' : IsMax (succ^[n] a)
⊢ f a ≤ f (succ (succ^[n] a))

Tactic:
rw [succ_eq_iff_isMax.2 hb']
      exact hn this

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha' : succ a✝ = a✝
ha : ⊤ ≤ ↑a✝
⊢ IsMax ↑a✝

pp: case neg
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha' : ¬succ a✝ = a✝
ha : ↑(succ a✝) ≤ ↑a✝
⊢ IsMax ↑a✝

Tactic:
· exact (not_top_le_coe _ ha).elim

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha' : ¬succ a✝ = a✝
ha : ↑(succ a✝) ≤ ↑a✝
⊢ IsMax ↑a✝
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : succ^[n + 1] a ∈ s → f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
this : succ^[n + 1] a ∈ s
hb' : IsMax (succ^[n + 1] a)
⊢ f a < f (succ (succ^[n + 1] a))

Tactic:
rw [succ_eq_iff_isMax.2 hb']
      exact hn this

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

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝¹ a✝ : α
h : ↑a✝ < ↑a✝¹
⊢ (match ↑a✝ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ↑a✝¹

Tactic:
rw [coe_lt_coe] at h

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝¹ a✝ : α
h : a✝ < a✝¹
⊢ (match ↑a✝ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ↑a✝¹
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ∞
hn0 : n ≠ 0
hxt : n ≠ ⊤
⊢ 0 < n.toNat

Tactic:
rw [pos_iff_ne_zero, ne_eq, ENat.toNat_eq_zero, not_or]

Goal state after:
n : ℕ∞
hn0 : n ≠ 0
hxt : n ≠ ⊤
⊢ ¬n = 0 ∧ ¬n = ⊤
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case some
x : ℕ
hx : some x < ⊤
⊢ lift (some x) hx = toNat (some x)

Tactic:
rfl

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

Goal state before:
pp: m n : ℕ
⊢ (↑m + ↑n).toNat = (↑m).toNat + (↑n).toNat

Tactic:
rfl

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

Goal state before:
pp: n : ℕ∞
hn : n ≠ ⊤
⊢ Injective fun x ↦ x + n

Tactic:
by
  intro a b e
  exact le_antisymm
    ((WithTop.add_le_add_iff_right hn).mp e.le)
    ((WithTop.add_le_add_iff_right hn).mp e.ge)

Goal state after:
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g j = f j

Tactic:
by simp [piecewise]

Goal state after:
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f g : (i : ι) → π i
⊢ {i}ᶜ.piecewise f g = update f i (g i)

Tactic:
piecewise_compl,

Goal state after:
ι : Type u_1
π : ι → Sort u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f g : (i : ι) → π i
⊢ {i}.piecewise g f = update f i (g i)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s), ⟨a, ha⟩ ∈ univ

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ a ∈ univ, ↑a ∈ s

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case refine_3
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s), ↑⟨a, ha⟩ = a

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case refine_4
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ↥s) (ha : a ∈ univ), ⟨↑a, ⋯⟩ = a

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case refine_5
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s), (if hi : p a then f a hi else g a hi) = f ↑⟨a, ha⟩ ⋯

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∉ s
⊢ ∀ x ∈ s, (if h : a = x then b x h else 1) = 1

Tactic:
grind

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

Goal state before:
pp: case mk
α : Type u_1
n : ℕ
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ (cons a ⟨val✝, property✝⟩).toList = a :: toList ⟨val✝, property✝⟩

Tactic:
rfl

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

Goal state before:
pp: case mk
α : Type u_1
n m : ℕ
val✝ : List α
property✝ : val✝.length = m
⊢ (drop n ⟨val✝, property✝⟩).toList = List.drop n (toList ⟨val✝, property✝⟩)

Tactic:
rfl

Goal state after: