mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Icc a b₁ ⊆ Ico a b₂

Tactic:
← coe_subset,

Goal state after:
α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ ↑(Icc a b₁) ⊆ ↑(Ico a b₂)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ico a b

Tactic:
← coe_subset,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ ↑(Ioo a b) ⊆ ↑(Ico a b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ioc a b

Tactic:
← coe_subset,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ ↑(Ioo a b) ⊆ ↑(Ioc a b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b ⊆ Icc a b

Tactic:
← coe_subset,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ ↑(Ico a b) ⊆ ↑(Icc a b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Icc a b

Tactic:
← coe_subset,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ ↑(Ioc a b) ⊆ ↑(Icc a b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
← coe_subset,

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ ↑(Icc a₁ b₁) ⊆ ↑(Icc a₂ b₂) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂

Tactic:
← coe_subset,

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ ↑(Icc a₁ b₁) ⊆ ↑(Ioo a₂ b₂) ↔ a₂ < a₁ ∧ b₁ < b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂

Tactic:
← coe_subset,

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ ↑(Icc a₁ b₁) ⊆ ↑(Ico a₂ b₂) ↔ a₂ ≤ a₁ ∧ b₁ < b₂
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mpr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ (∃ x, ∀ (n : ℕ), x n ∈ s) → Nonempty ((fun x1 x2 ↦ x1 > x2) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s)

Tactic:
rintro ⟨⟨f, hf⟩, hfs : ∀ n, f n ∈ s⟩

Goal state after:
case mpr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b
hfs : ∀ (n : ℕ), f n ∈ s
⊢ Nonempty ((fun x1 x2 ↦ x1 > x2) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → f (g m) > f (g n)
⊢ ∃ m n, m < n ∧ (fun x1 x2 ↦ x1 ≤ x2) (f m) (f n)

Tactic:
exfalso
    apply RelEmbedding.not_wellFounded _ hwf.wf
    exact (RelEmbedding.ofMonotone _ h1).swap

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Set.Icc a a = {a}

Tactic:
Set.Icc_self

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ {a} = {a}
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ x : N
hx : x ∈ s
⊢ (fun x ↦ r • x) x = r ^ 1 • x

Tactic:
by rw [pow_one]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ #(Ioo a b) = #(Icc a b) - 2

Tactic:
rw [card_Ioo_eq_card_Ico_sub_one, card_Ico_eq_card_Icc_sub_one]
  rfl

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
← coe_subset,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
⊢ ↑(Ico a₁ b₁) ⊆ ↑(Ico a₂ b₂) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a c ⊆ Ico a b ∪ Ico b c

Tactic:
← coe_subset,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(Ico a c) ⊆ ↑(Ico a b ∪ Ico b c)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz✝ : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : ¬x < z
⊢ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
simp only [lt_iff_le_not_ge, not_and, not_not] at hxz
    exact .single (hzy.of_le_of_lt (hxz hz.1.1) hxy)

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (¬∃ x, IsBadSeq r s x) ↔ ¬∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
not_congr

Goal state after:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ ¬?m.16 ↔ ¬∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ x, IsBadSeq r s x) ↔ ?m.16

α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ Prop
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case h.left
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
n : ℕ
hn : (ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ g 0 < g n

Tactic:
by_contra hx
      simp_all

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mul_left.inr
G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
x✝ : G
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x⁻¹ * y) ⋯
x y : G
hy : y ∈ Submonoid.closure (s ∪ s⁻¹)
ih : p y ⋯
hx : x ∈ s⁻¹
⊢ p (x * y) ⋯

Tactic:
| inr hx =>

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

Goal state before:
pp: case h.cons.e_a
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * hd = hd * a

Tactic:
apply comm.of_refl <;> simp

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ s.noncommProd f comm = m ^ #s

Tactic:
rw [noncommProd, Multiset.noncommProd_eq_pow_card _ _ m]

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ m ^ (Multiset.map f s.val).card = m ^ #s

α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ ∀ x ∈ Multiset.map f s.val, x = m
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ s.noncommProd f comm = m ^ #s

Tactic:
by
  rw [noncommProd, Multiset.noncommProd_eq_pow_card _ _ m]
  · simp only [Finset.card_def, Multiset.card_map]
  · simpa using h

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
i : Finset ι
f : ι → Multiset α
a : Multiset α
⊢ Disjoint (i.sum f) a ↔ ∀ b ∈ i, Disjoint (f b) a

Tactic:
convert! @disjoint_sum_left _ a (map f i.val)

Goal state after:
case e'_2
ι : Type u_1
α : Type u_6
i : Finset ι
f : ι → Multiset α
a : Multiset α
⊢ (∀ b ∈ i, Disjoint (f b) a) ↔ ∀ b ∈ map f i.val, Disjoint b a
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∀ x ∈ t ∪ u, x ∉ u → x ^ g x = 1

Tactic:
simp +contextual [Function.support_subset_iff'.1 hg]

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

Goal state before:
pp: α : Type u_1
r s : Setoid α
⊢ r ⊔ s = sInf {s_1 | ∀ ⦃x y : α⦄, r x y ∨ s x y → s_1 x y}

Tactic:
apply congr_arg sInf

Goal state after:
α : Type u_1
r s : Setoid α
⊢ {x | r ≤ x ∧ s ≤ x} = {s_1 | ∀ ⦃x y : α⦄, r x y ∨ s x y → s_1 x y}
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
S : Set (Setoid α)
⊢ sSup S = sInf {s | ∀ ⦃x y : α⦄, (∃ r ∈ S, r x y) → s x y}

Tactic:
apply congr_arg sInf

Goal state after:
α : Type u_1
S : Set (Setoid α)
⊢ upperBounds S = {s | ∀ ⦃x y : α⦄, (∃ r ∈ S, r x y) → s x y}
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
⊢ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ∀ h ∈ ↑H₃, ⁅h, ⁅g₁, g₂⁆⁆ = 1

Tactic:
intro x hx y hy z hz

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ ⁅z, ⁅x, y⁆⁆ = 1
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ (map (g ∘ f)) x = (map g) ((map f) x)

Tactic:
rw [map_comp]
  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
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
⊢ g ↑(f.sec z).2 * (f.lift hg) z = g (f.sec z).1

Tactic:
by
  rw [mul_comm, lift_mul_right]

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

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))

Tactic:
rcases oreCondition ra sb with ⟨rc, sc, hc⟩

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

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
a₁ b₁ : M
a₂ b₂ : ↥S
⊢ f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (Localization.r S) (a₁, a₂) (b₁, b₂)

Tactic:
f.eq,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a₁ b₁ : M
a₂ b₂ : ↥S
⊢ (∃ c, ↑c * (↑b₂ * a₁) = ↑c * (↑a₂ * b₁)) ↔ (Localization.r S) (a₁, a₂) (b₁, b₂)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a ≤ b
⊢ ∃ n, pred^[n] b = a

Tactic:
replace hab := eq_or_lt_of_le hab

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a = b ∨ a < b
⊢ ∃ n, pred^[n] b = a
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝⁴ : PartialOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : NeZero 1
inst✝¹ : SuccAddOrder α
inst✝ : IsBotZeroClass α
⊢ 0 < x ↔ x ≠ 0

Tactic:
pos_iff_ne_zero

Goal state after:
α : Type u_1
x : α
inst✝⁴ : PartialOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : NeZero 1
inst✝¹ : SuccAddOrder α
inst✝ : IsBotZeroClass α
⊢ x ≠ 0 ↔ x ≠ 0
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ
α : 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^[n + 1] a ∈ s
⊢ f a ≤ f (succ^[n + 1] a)

Tactic:
| succ n hn =>

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f a < f (a + 1)) → StrictMonoOn f s

Tactic:
simpa [Order.succ_eq_add_one] using strictMonoOn_of_lt_succ hs (f := f)

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n + 1 - 1] i)
⊢ pred^[n + 1] (succ^[n + 1] i) = i

Tactic:
| succ n hn =>

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f a < f (a - 1)) → StrictAntiOn f s

Tactic:
by
  simpa [Order.pred_eq_sub_one] using strictAntiOn_of_lt_pred hs (f := f)

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

Goal state before:
pp: case succ.succ
α : 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^[n + 1 + 1] a ∈ s
⊢ f a < f (succ^[n + 1 + 1] a)

Tactic:
| succ n hn =>

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

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

Tactic:
have : pred^[n] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩

Goal state after:
case succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : pred^[n] b ∈ s → f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
⊢ f (pred (pred^[n] b)) ≤ f b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : pred^[n] b ∈ s → f (pred^[n] b) ≤ f b
ha : pred^[n + 1] b ∈ s
⊢ f (pred^[n + 1] b) ≤ f b

Tactic:
| succ n hn =>

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

Goal state before:
pp: case inl
c : ℕ∞
hc : c ≠ 0
⊢ ⊤ ≤ ⊤ * c

pp: case inr
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
⊢ a ≤ a * c

Tactic:
· simp [top_mul hc]

Goal state after:
case inr
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
⊢ a ≤ a * c
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : WithTop ℕ∞
⊢ n + 1 = ↑⊤ ↔ n = ↑⊤

Tactic:
match n with
  | ⊤ => exact Iff.rfl
  | (⊤ : ℕ∞) => simp
  | (n : ℕ) =>
    norm_cast
    simp only [natCast_ne_top]

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

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

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
⊢ Nonempty (α ≃ ↥t)

Tactic:
by rwa [← Fintype.card_eq, Fintype.card_coe]

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

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
inst✝ : Subsingleton α
n✝ : ℕ
⊢ ∀ (a b : Sym α (n✝ + 1)), a = b

Tactic:
intro s s'
      obtain ⟨b, -⟩ := exists_mem s
      rw [eq_replicate_of_subsingleton b s', eq_replicate_of_subsingleton b s]

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
⊢ v.reverse.reverse = v

Tactic:
by
  cases v
  simp [Vector.reverse]

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

Goal state before:
pp: case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (n✝ + 1)
⊢ (scanl f b v).head = b

Tactic:
· rw [← cons_head_tail v]
    simp [← get_zero, get_eq_get_toList]

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

Goal state before:
pp: case succ.succ
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
⊢ #({x ∈ T | x.length = s}) ≤ Fintype.card α ^ s

Tactic:
calc
    _ ≤ (Finset.univ.image List.ofFn).card := by
          apply Finset.card_le_card
          intro a ha
          let hlen := Finset.mem_filter.mp ha
          exact Finset.mem_image.mpr ⟨
              (fun j : Fin s => a.get ⟨j.val, by simp [hlen]⟩),
              by simp,
              List.ext_get (by simp [hlen]) (by simp)⟩
    _ = Fintype.card α ^ s := by
          simp [card_image_of_injective univ List.ofFn_injective]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
x : β
⊢ ScottContinuous (Function.const α x)

Tactic:
by
  simp_rw [← scottContinuousOn_univ, ScottContinuousOn.const]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : ScottContinuous f
hg : ScottContinuous g
⊢ ScottContinuous (g ∘ f)

Tactic:
rw [← scottContinuousOn_univ] at ⊢ hf hg

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ ScottContinuousOn univ (g ∘ f)
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : α → γ
hf : ScottContinuous f
hg : ScottContinuous g
⊢ ScottContinuous fun x ↦ (f x, g x)

Tactic:
rw [← scottContinuousOn_univ] at ⊢ hf hg

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : α → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ ScottContinuousOn univ fun x ↦ (f x, g x)
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
⊢ a < 2 ^ a

Tactic:
induction a using Cardinal.inductionOn with | _ α
  rw [← mk_set]
  refine ⟨⟨⟨singleton, fun a b => singleton_eq_singleton_iff.1⟩⟩, ?_⟩
  rintro ⟨⟨f, hf⟩⟩
  exact cantor_injective f hf

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α β : Type u
a b : ℕ
h : ↑a = ↑b
⊢ a = b

Tactic:
rwa [← lift_mk_fin, ← lift_mk_fin, lift_inj, Cardinal.eq, ← Fintype.card_eq,
    Fintype.card_fin, Fintype.card_fin] at h

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr
n : ℕ∞
x : Cardinal.{u_1}
hx : ℵ₀ ≤ x
⊢ ↑n ≤ x ↔ n ≤ x.toENatAux

Tactic:
| inr hx =>

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr
x : Cardinal.{u_1}
n : ℕ
hx : ℵ₀ ≤ x
⊢ x.toENatAux ≤ ↑n ↔ x ≤ ↑n

Tactic:
| inr hx =>

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

Goal state before:
pp: case succ
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a ^ (n + 1))

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift.{u, w} (f i) ≤ t
⊢ lift.{u, w} (iSup f) ≤ t

Tactic:
rw [lift_iSup hf]

Goal state after:
ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift.{u, w} (f i) ≤ t
⊢ ⨆ i, lift.{u, w} (f i) ≤ t
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ lift.{u, w} (iSup f) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t

Tactic:
rw [lift_iSup hf]

Goal state after:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ ⨆ i, lift.{u, w} (f i) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
⊢ 0 < c ↔ c ≠ 0

Tactic:
pos_iff_ne_zero

Goal state after:
c : Cardinal.{u_1}
⊢ c ≠ 0 ↔ c ≠ 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mpr
α : Type u
n : ℕ
⊢ (∃ h, Fintype.card α = n) → ∃ t, ↑t = univ ∧ t.card = n

Tactic:
rintro ⟨⟨t, ht⟩, hn⟩

Goal state after:
case mpr
α : Type u
n : ℕ
t : Finset α
ht : ∀ (x : α), x ∈ t
hn : Fintype.card α = n
⊢ ∃ t, ↑t = univ ∧ t.card = n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case h
a b c : Cardinal.{u}
⊢ BddAbove (range fun c ↦ a ^ ↑c)

Tactic:
· rw [← image_eq_range]
    exact bddAbove_image.{u, u} _ bddAbove_Iio

Goal state after: