mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
⊢ ∃ a, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
by
  choose next hnext using exists_covBy_of_wellFoundedLT (α := α)
  have hα := Set.nonempty_iff_univ_nonempty.mp ‹_›
  classical
  let a : ℕ → α := Nat.rec (wfl.wf.min _ hα) fun _n a ↦ if ha : IsMax a then a else next ha
  refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ (Set.mem_univ _), ?_⟩
  have cov n (hn : ¬ IsMax (a n)) : a n ⋖ a (n + 1) := by
    change a n ⋖ if ha : IsMax (a n) then a n else _
    rw [dif_neg hn]
    exact hnext hn
  have H : ∃ n, IsMax (a n) := by
    by_contra!
    exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf
  exact ⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ (wellFounded_lt.not_lt_min _ · h)⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case neg
α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : ¬(s ∩ t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
rcases ht with ⟨m, mt⟩
    exact ⟨m, mt, fun x _ ⟨_, _, ms⟩ => hst ⟨m, ⟨ms, mt⟩⟩⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Preorder α
inst✝ : WellQuasiOrderedLE α
⊢ WellFoundedLT α

Tactic:
rw [WellFoundedLT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Preorder α
inst✝ : WellQuasiOrderedLE α
⊢ IsEmpty ((fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x1 < x2)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case H
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a : α
i : Finset α
ih : ∀ t ⊂ i, ∀ (b : α), a < b → Icc a b = t → False
b : α
h : a < b
hs : Icc a b = i
⊢ False

Tactic:
subst hs

Goal state after:
case H
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a b : α
h : a < b
ih : ∀ t ⊂ Icc a b, ∀ (b : α), a < b → Icc a b = t → False
⊢ False
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ Iio a = ∅ ↔ IsMin a

Tactic:
exact Iio_eq_empty

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

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
a✝ b✝ : G
ha : a✝ ∈ (↑S)⁻¹
hb : b✝ ∈ (↑S)⁻¹
⊢ b✝⁻¹ * a✝⁻¹ ∈ ↑S

Tactic:
exact mul_mem hb ha

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

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝³ : Monoid M
inst✝² : AddMonoid A
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α M
S : Submonoid M
⊢ 1 • S = S

Tactic:
change S.map _ = S
    simpa only [map_one] using! S.map_id

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
| x.orbit

Tactic:
rw [← hφ x]

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
| orbit (Quotient.mk' (φ x))
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ center G = ⊤ ↔ IsMulCommutative G

Tactic:
by
  simp [eq_top_iff', isMulCommutative_iff, mem_center_iff, eq_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set M
⊢ S.centralizer.centralizer.centralizer = S.centralizer

Tactic:
refine Set.Subset.antisymm ?_ Set.subset_centralizer_centralizer
  exact fun x hx y hy ↦ hx y <| Set.subset_centralizer_centralizer hy

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case h.right
α : 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
⊢ f (g 0) ≤ f (g n)

Tactic:
exact Prod.Lex.toLex_le_toLex.mpr <| .inl hn

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : closure s = ⊤
⊢ center G = ⨅ g ∈ s, centralizer {g}

Tactic:
by
  rw [← centralizer_univ, ← coe_top, ← hs, centralizer_closure, centralizer_eq_iInf]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → ι → M
hs : {a | σ a ≠ a} ⊆ ↑s
⊢ ∏ x ∈ s, f (σ x) x = ∏ x ∈ s, f x ((Equiv.symm σ) x)

Tactic:
convert! σ.prod_comp s (fun x => f x (σ.symm x)) hs
  rw [Equiv.symm_apply_apply]

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

Goal state before:
pp: α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
S : Subgroup G
⊢ 1 • S = S

Tactic:
change S.map _ = S
    simpa only [map_one] using! S.map_id

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
hx : x ∈ closure s
⊢ ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x

Tactic:
induction hx using closure_induction with
    | one => exact ⟨0, ∅, by simp⟩
    | mem x hx =>
      exact ⟨Pi.single x 1, {x}, by simp [hx, Pi.single_apply]⟩
    | mul x y _ _ hx hy =>
    obtain ⟨f, t, hts, hf, rfl⟩ := hx
    obtain ⟨g, u, hus, hg, rfl⟩ := hy
    refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
    simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
    congr 1 <;> symm
    · refine Finset.prod_subset Finset.subset_union_left ?_
      simp +contextual [Function.support_subset_iff'.1 hf]
    · refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
c : Con M
f : N →* M
x y : N
⊢ c (f x) (f y) ↔ c.mk' (f x) = c.mk' (f y)

Tactic:
rw [← c.eq]

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
c : Con M
f : N →* M
x y : N
⊢ ↑(f x) = ↑(f y) ↔ c.mk' (f x) = c.mk' (f y)
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
a b c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
⊢ c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) = (a * c)⁻¹ * (b * d)

Tactic:
simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ ↑N * s → a ∈ mk ⁻¹' mk '' s

Tactic:
rintro ⟨a, ha, b, hb, rfl⟩
    refine ⟨b, hb, ?_⟩
    simpa only [QuotientGroup.mk_mul, right_eq_mul, QuotientGroup.eq_one_iff]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
⊢ ∏ x ∈ insert a (s.erase a), f x = ∏ x ∈ s, f x

Tactic:
insert_erase h

Goal state after:
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
⊢ ∏ x ∈ s, f x = ∏ x ∈ s, f x
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ s : R
hs✝ : s ∈ ⊥
hs : s = 1
h : x✝¹ * ↑⟨s, hs✝⟩ = x✝ * ↑⟨s, hs✝⟩
⊢ ↑⟨s, hs✝⟩ * x✝¹ = ↑⟨s, hs✝⟩ * x✝

Tactic:
subst hs

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ : R
hs : 1 ∈ ⊥
h : x✝¹ * ↑⟨1, hs⟩ = x✝ * ↑⟨1, hs⟩
⊢ ↑⟨1, hs⟩ * x✝¹ = ↑⟨1, hs⟩ * x✝
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ commutator G = ⊥ ↔ IsMulCommutative G

Tactic:
by
  rw [commutator_eq_bot_iff_center_eq_top, center_eq_top_iff]

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
p q : G
⊢ ↑p * ↑q * (↑p)⁻¹ * (↑q)⁻¹ = 1

Tactic:
← commutatorElement_def,

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
p q : G
⊢ ⁅↑p, ↑q⁆ = 1
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
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
⊢ r₃ * (v * ↑s) = r₃ * ↑u * ↑s'

Tactic:
← hsu,

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
⊢ r₃ * (↑u * ↑s') = r₃ * ↑u * ↑s'
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
x y : OreLocalization S R
z : OreLocalization S X
⊢ (x * y) • z = x • y • z

Tactic:
cases x with | _ r₁ s₁

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
y : OreLocalization S R
z : OreLocalization S X
r₁ : R
s₁ : ↥S
⊢ (r₁ /ₒ s₁ * y) • z = (r₁ /ₒ s₁) • y • z
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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
d : P
hc : k d * k x = k d * k y
hd : k d = ↑c
⊢ ↑⟨d, ⋯⟩ * x = ↑⟨d, ⋯⟩ * y

Tactic:
← map_mul k,

Goal state after:
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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
d : P
hc : k (d * x) = k d * k y
hd : k d = ↑c
⊢ ↑⟨d, ⋯⟩ * x = ↑⟨d, ⋯⟩ * y
Module: Mathlib.Algebra.Order.Hom.Ring

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : NonAssocSemiring α
inst✝² : Preorder α
inst✝¹ : NonAssocSemiring β
inst✝ : Preorder β
f g : α ≃+*o β
h : f.toOrderRingHom = g.toOrderRingHom
⊢ ⇑f = ⇑g

Tactic:
by convert! DFunLike.ext'_iff.1 h using 0

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
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
x y : OreLocalization S R
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (x * y) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ x * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ y

Tactic:
cases x with | _ r₁ s₁

Goal state after:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
y : OreLocalization S R
r₁ : R
s₁ : ↥S
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁ * y) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ y
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : ⊤.LocalizationMap N
⊢ Injective ⇑f ↔ IsCancelMul M

Tactic:
simp [injective_iff, isCancelMul_iff_forall_isRegular]

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
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
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R M M
r : R
x : OreLocalization S M
y : OreLocalization S X
⊢ r • x • y = x • r • y

Tactic:
cases x with | _ r₁ s₁

Goal state after:
case c
R : Type u_1
R' : Type u_2
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
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R M M
r : R
y : OreLocalization S X
r₁ : M
s₁ : ↥S
⊢ r • (r₁ /ₒ s₁) • y = (r₁ /ₒ s₁) • r • y
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
x y : OreLocalization S R
⊢ x * y = y * x

Tactic:
cases x with | _ r₁ s₁

Goal state after:
case c
R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
y : OreLocalization S R
r₁ : R
s₁ : ↥S
⊢ r₁ /ₒ s₁ * y = y * (r₁ /ₒ s₁)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
hS : BddAbove S
hS' : S.Nonempty
⊢ ∃ x, IsGreatest S x

Tactic:
obtain ⟨m, hm⟩ := hS
  obtain ⟨n, hn⟩ := hS'
  by_cases hm' : m ∈ S
  · exact ⟨_, hm', hm⟩
  have hn' := hm hn
  revert hn hm hm'
  refine Succ.rec ?_ ?_ hn'
  · simp +contextual
  intro m _ IH hm hn hm'
  rw [mem_upperBounds] at IH hm
  simp_rw [Order.le_succ_iff_eq_or_le] at hm
  replace hm : ∀ x ∈ S, x ≤ m := by
    intro x hx
    refine (hm x hx).resolve_left ?_
    rintro rfl
    exact hm' hx
  by_cases hmS : m ∈ S
  · exact ⟨m, hmS, hm⟩
  · exact IH hm hn hmS

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
this : pred ⟨c, hc⟩ = ⟨c, hc⟩
⊢ pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
rw [Function.iterate_fixed]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
this : pred ⟨c, hc⟩ = ⟨c, hc⟩
⊢ ⟨c, hc⟩ = ⟨b, hb⟩

case neg.h
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
this : pred ⟨c, hc⟩ = ⟨c, hc⟩
⊢ pred ⟨c, hc⟩ = ⟨c, hc⟩
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : 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)
⊢ MonotoneOn f s

Tactic:
rintro a ha b hb hab

Goal state after:
α : 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
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f a ≤ f b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : 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)
⊢ StrictMonoOn f s

Tactic:
rintro a ha b hb hab

Goal state after:
α : 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
b : α
hb : b ∈ s
hab : a < b
⊢ f a < f b
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 α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f (a + 1) ≤ f a) → Antitone f

Tactic:
by
  simpa [Order.succ_eq_add_one] using antitone_of_succ_le (f := f)

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

Goal state before:
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:
· rw [coe_le_coe, succ_le_iff_isMax, ← succ_eq_iff_isMax] at ha
      exact (ha' ha).elim

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a : WithTop α
ha :
  a ≤
    match a with
    | none => ↑⊤
    | Option.some a => ↑(pred a)
⊢ IsMin a

Tactic:
by
    cases a
    · exact ((coe_lt_top (⊤ : α)).not_ge ha).elim
    · exact (min_of_le_pred <| coe_le_coe.1 ha).withTop

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

Goal state before:
pp: α : 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
⊢ MonotoneOn f s

Tactic:
rintro a ha b hb hab

Goal state after:
α : 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
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f a ≤ f b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : 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
⊢ StrictMonoOn f s

Tactic:
rintro a ha b hb hab

Goal state after:
α : 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
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f a < f b
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Tactic:
by_cases hs : i ∈ s

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∈ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∉ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
f : ι → M
a : ι
s : Finset ι
ha : a ∈ s
⊢ f a ∣ ∏ i ∈ s, f i

Tactic:
classical
    rw [Finset.prod_eq_mul_prod_sdiff_singleton_of_mem ha]
    exact dvd_mul_right _ _

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

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

Tactic:
cases n
  · have : v = nil := by simp only [eq_iff_true_of_subsingleton]
    simp only [this, scanl_nil, head_cons]
  · rw [← cons_head_tail v]
    simp [← get_zero, get_eq_get_toList]

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

Goal state before:
pp: case refine_3
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ (range (Subtype.val ∘ f)).Infinite

Tactic:
exact infinite_range_of_injective <| Injective.comp Subtype.val_injective hf

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∏ a ∈ {x | p x}.toFinset, f a = ∏ a, f ↑a

Tactic:
by
  rw [← Finset.prod_subtype]
  simp_rw [Set.mem_toFinset]; intro; rfl

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
a : α
⊢ inl ⊥ ≤ inl a

Tactic:
exact Lex.inl bot_le

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
i : α
his : i ∈ s
hi : i < y
⊢ sInf s ∈ s

Tactic:
exact eq_of_le_of_not_lt (sInf_le his) (hy.2 · hi) ▸ his

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

Goal state before:
pp: case mpr
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
⊢ ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂

Tactic:
intro n₁

Goal state after:
case mpr
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ : ℕ
⊢ ∀ (n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ f '' {y | IsExtremePt x f y} ⊆ {y | IsExtremePt x f y}

Tactic:
rintro _ ⟨y, hy, rfl⟩
    refine ⟨map_mem_bot le_map hy.mem_bot, ?_⟩
    intro z hz hzy
    have hz' := hz
    rw [← bot_eq_of_le_or_map_le le_map hy] at hz'
    rcases hz' with ⟨_, (hz' | hz')⟩
    · rcases le_iff_lt_or_eq.1 hz' with (hz' | rfl)
      · exact le_trans (hy.map_le_of_mem_of_lt hz hz') (le_map y)
      · exact le_refl (f z)
    · exfalso
      exact lt_irrefl z (lt_of_lt_of_le hzy hz')

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
a✝ : y ≠ z
left✝ : z ∈ bot x f
hz : f y ≤ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y

Tactic:
· left; exact le_trans (le_map y) hz

Goal state after: