mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
h : n < k
⊢ 0 = k ! * n.choose k

Tactic:
choose_eq_zero_of_lt h,

Goal state after:
case inl
n k : ℕ
h : n < k
⊢ 0 = k ! * 0
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n - r ≤ n / 2

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr
r n : ℕ
b : n < r
⊢ 0 ≤ n.choose (n / 2)

Tactic:
apply zero_le

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
this : (t.Nonempty → s.Finite) ∧ (s.Nonempty → t.Finite)
⊢ False

Tactic:
exact h ((this.1 h.nonempty.snd).prod <| this.2 h.nonempty.fst)

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ ∅ ^ k
k : ℕ
hk : Fintype.card G ≤ k
⊢ ↑(∅ ^ k) ≃ ↑(∅ ^ Fintype.card G)

Tactic:
empty_pow (hG.trans_le hk).ne',

Goal state after:
case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ ∅ ^ k
k : ℕ
hk : Fintype.card G ≤ k
⊢ ↑∅ ≃ ↑(∅ ^ Fintype.card G)
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set β
⊢ f ⁻¹' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f ⁻¹' s i j

Tactic:
preimage_iUnion

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
⊢ s ×ˢ ⋃ i, t i = ⋃ i, s ×ˢ t i

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : Set β
⊢ (⋃ i, s i) ×ˢ t = ⋃ i, s i ×ˢ t

Tactic:
ext
  simp

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

Goal state before:
pp: ι : Type u_9
ι' : Type u_10
α : Type u_11
β : Type u_12
s : ι → Set α
t : ι' → Set β
⊢ ⋃ x, s x.1 ×ˢ t x.2 = (⋃ i, s i) ×ˢ ⋃ i, t i

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ a⁻¹ * x) '' s ∩ t).Nonempty ↔ ((fun x ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
by
  rw [← nonempty_inv, inter_inv]; simp_rw [← image_inv_eq_inv, image_image, mul_inv_rev, inv_inv]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ x * a⁻¹) '' s ∩ t).Nonempty ↔ ((fun x ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
by
  rw [← nonempty_inv, inter_inv]; simp_rw [← image_inv_eq_inv, image_image, mul_inv_rev, inv_inv]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit {a}

Tactic:
exact ha.set

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ Nontrivial ↥H

Tactic:
nontrivial_iff_exists_ne_one

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ ∃ x ∈ H, x ≠ 1
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nontrivial ↥H ↔ ∃ a, a ≠ 1

Tactic:
nontrivial_iff_exists_ne_one

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ ∃ a, a ≠ 1
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
⊢ comap f f.range = ⊤

Tactic:
ext
  simp

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

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
H : (↑e).comp (powMonoidHom n) = (powMonoidHom n).comp ↑e
⊢ ((powMonoidHom n).comp ↑e).range = (powMonoidHom n).range

Tactic:
range_comp,

Goal state after:
M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
H : (↑e).comp (powMonoidHom n) = (powMonoidHom n).comp ↑e
⊢ Subgroup.map (powMonoidHom n) (↑e).range = (powMonoidHom n).range
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n : ℕ
⊢ (unpair n).2 ≤ n

Tactic:
simpa using right_le_pair n.unpair.1 n.unpair.2

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) + 1 = 2 * x✝¹ + (2 * x✝ + 1)

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) = 2 * x✝¹ + 2 * x✝

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) + 1 = 2 * x✝¹ + 1 + 2 * x✝

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case false
n : ℕ
h : n ≠ 0
⊢ ¬2 * n = 0

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case true
n : ℕ
h : n ≠ 0
⊢ ¬2 * n + 1 = 0

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ 2 * x✝¹ + 1 ≤ 2 * x✝ + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ 2 * x✝¹ ≤ 2 * x✝

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case false
m n : ℕ
b : Bool
h : m < n
⊢ 2 * m < 2 * n

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case true
m n : ℕ
b : Bool
h : m < n
⊢ 2 * m + 1 < 2 * n

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case false
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ 2 * n

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case true
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ 2 * n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
m n : ℕ
h✝ : m < n
⊢ m < n + (n + 1)

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
m n : ℕ
h✝ : ¬m < n
⊢ n < m + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
m n : ℕ
h✝ : m < n
this : n ≤ n * n
⊢ m + n ≤ n * n + m

Tactic:
lia

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
⊢ r (f a) (f (Directed.sequence f hf (encode a + 1)))

Tactic:
by
  simp only [Directed.sequence, encodek]
  exact (Classical.choose_spec (hf _ a)).2

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
⊢ (∀ (h : G), h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ∀ (x : G), (∃ x_1 ∈ s, (MulAut.conj g) x_1 = x) ↔ x ∈ s

Tactic:
MulAut.conj_apply

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
⊢ (∀ (h : G), h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ∀ (x : G), (∃ x_1 ∈ s, g * x_1 * g⁻¹ = x) ↔ x ∈ s
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
g : M →* N
f : α → M
⊢ g.comp (lift f) = lift (⇑g ∘ f)

Tactic:
ext
  simp

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

Goal state before:
pp: G✝ : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁷ : Group G✝
inst✝⁶ : Group G'
inst✝⁵ : Group G''
A : Type u_4
inst✝⁴ : AddGroup A
N : Type u_5
inst✝³ : Group N
M : Type u_6
inst✝² : AddGroup M
I : AddSubgroup M
G : Type u_7
inst✝¹ : Group G
inst✝ : MulAction G M
a b : G
ha : a ∈ {σ | ∀ (x : M), σ • x - x ∈ I}
hb : b ∈ {σ | ∀ (x : M), σ • x - x ∈ I}
x : M
⊢ (a * b) • x - x ∈ I

Tactic:
simpa [mul_smul] using add_mem (ha (b • x)) (hb x)

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

Goal state before:
pp: α : Type ?u.8
β : Type ?u.9
x✝ : (f : α ↪ β) × ↑(range ⇑f)ᶜ
f : α ↪ β
y : β
hy : y ∈ (range ⇑f)ᶜ
⊢ (fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ⟨f, ⟨y, hy⟩⟩) = ⟨f, ⟨y, hy⟩⟩

Tactic:
ext <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ (∃ b_1, b_1 ∈ t ∧ inr b_1 = inr b) ↔ b ∈ t

pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ ¬∃ a, a ∈ s ∧ inl a = inr b

Tactic:
· simp only [inr.injEq, exists_eq_right]

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ ¬∃ a, a ∈ s ∧ inl a = inr b
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : ↑s
h : y < x
hx : ∃ m, ↑y + m + 1 ∈ s
k : ℕ
hk : ↑x = ↑y + k + 1
this : Nat.find hx ≤ k
⊢ ↑y + Nat.find hx + 1 ≤ ↑x

Tactic:
lia

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : ↑s
h : ∀ z < x, z ≤ y
hx : ∃ m, ↑y + m + 1 ∈ s
hxy : ↑y + Nat.find hx + 1 < ↑x
⊢ ↑y < ↑y + Nat.find hx + 1

Tactic:
lia

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
⊢ s = ∅

Tactic:
obtain ⟨a, ha⟩ := max_of_nonempty H

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
a : α
ha : s.max = ↑a
⊢ s = ∅
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
H : s.Nonempty
x : α
h₂ : 1 < #s
⊢ 0 < #s

Tactic:
lia

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

Goal state before:
pp: case cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ s ∈ (a :: t).sublists' ↔ s <+ a :: t

Tactic:
| cons a t IH =>

Goal state after:
case cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ s ∈ (a :: t).sublists' ↔ s <+ a :: t
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ l.sublists' ++ map (cons a) l.sublists' ~ l.sublists ++ map (cons a) l.sublists

Tactic:
exact Perm.append (sublists_perm_sublists' _).symm (Perm.map _ (sublists_perm_sublists' _).symm)

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
⊢ (s.erase ⊥).sup id = s.sup id

Tactic:
refine (sup_mono (s.erase_subset _)).antisymm (Finset.sup_le_iff.2 fun a ha => ?_)
  obtain rfl | ha' := eq_or_ne a ⊥
  · exact bot_le
  · exact le_sup (mem_erase.2 ⟨ha', ha⟩)

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ↑s.powerset = SetLike.coe ⁻¹' 𝒫 ↑s

Tactic:
ext
  simp

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
y : Finset α
hyt : y ⊆ t \ s
hyn : #y = n - #s
⊢ n - #s + #s = n

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset (Option α)
⊢ eraseNone s = s.biUnion Option.toFinset

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ eraseNone (map Embedding.some s) = s

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
⊢ eraseNone (s ∪ t) = eraseNone s ∪ eraseNone t

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
⊢ eraseNone (s ∩ t) = eraseNone s ∩ eraseNone t

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
⊢ eraseNone ∅ = ∅

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
⊢ eraseNone {none} = ∅

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ eraseNone (insertNone s) = s

Tactic:
ext
  simp

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

Goal state before:
pp: P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
⊢ P α

Tactic:
cases nonempty_fintype α

Goal state after:
case intro
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ P α
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hne : s.Nonempty
hbdd : BddAbove s
⊢ l (sSup s) = ⨆ x, l ↑x

Tactic:
by
  simpa only [← comp_def, ← sSup_range, range_comp, Subtype.range_coe_subtype, ofPred_mem_eq]
    using gc.l_csSup_of_directedOn' hd hne hbdd

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ⨆ i ∈ s, f i = (image f s).max' h'

Tactic:
by
  classical
  rw [iSup, ← h'.csSup_eq_max', coe_image]
  refine csSup_eq_csSup_of_forall_exists_le ?_ ?_
  · simp only [ciSup_eq_ite, dite_eq_ite, Set.mem_range, Set.mem_image, mem_coe,
      exists_exists_and_eq_and, forall_exists_index, forall_apply_eq_imp_iff]
    intro i
    split_ifs
    · exact ⟨_, by assumption, le_rfl⟩
    · assumption
  · simp only [Set.mem_image, mem_coe, ciSup_eq_ite, dite_eq_ite, Set.mem_range,
      exists_exists_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    intro i hi
    refine ⟨i, ?_⟩
    simp [hi]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
s : Finset α
hs : ↑s ⊆ ⋃ i, f i
⊢ ∃ i, ↑s ⊆ f i

Tactic:
by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons b t hbt iht =>
    simp only [Finset.coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢
    rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩
    rcases h i j with ⟨k, hik, hjk⟩
    exact ⟨k, hik hi, hj.trans hjk⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case refine_2.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⋖ b₂
⊢ (a₁, b₁) ⋖ (a₁, b₂)

Tactic:
· exact mk_covBy_mk_iff_right.2 h

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

Goal state before:
pp: case cons
ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih : ∃ i, MaximalFor (fun x ↦ x ∈ s) f i
⊢ ∃ i_1, MaximalFor (fun x ↦ x ∈ cons i s hi) f i_1

Tactic:
obtain ⟨j, hj⟩ := ih

Goal state after:
case cons
ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun x ↦ x ∈ s) f j
⊢ ∃ i_1, MaximalFor (fun x ↦ x ∈ cons i s hi) f i_1
Module: Mathlib.Order.Minimal

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : LE α
f : ι → α
i j : ι
⊢ MinimalFor (fun x ↦ x = j) f i ↔ i = j

Tactic:
by simp +contextual [MinimalFor]

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Finset.Iio b ↔ x < b

Tactic:
Finset.mem_Iio

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x < b ↔ x < b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b

Tactic:
lia

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

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b

Tactic:
lia

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

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b

Tactic:
lia

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

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a - 1) ↔ a < x ∧ x < b

Tactic:
lia

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

Goal state before:
pp: a : ℕ
h : 0 < a
x : ℕ
⊢ a - 1 ≤ x ∧ x < a ↔ x = a - 1

Tactic:
lia

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

Goal state before:
pp: a✝ b c : ℕ
a : ↥(Ioc b (b + 1))
⊢ b < b + 1 ∧ b + 1 ≤ b + 1

Tactic:
lia

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

Goal state before:
pp: a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : a - c ≤ x ∧ x < b - c
⊢ (a ≤ x + c ∧ x + c < b) ∧ x + c - c = x

Tactic:
lia

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

Goal state before:
pp: a b c : ℕ
h : c ≤ a
x : ℕ
hx : a ≤ x ∧ x < b
⊢ a - c ≤ x - c ∧ x - c < b - c

Tactic:
lia

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

Goal state before:
pp: a b c : ℕ
hac : a ≤ c
x : ℕ
h : c + 1 - b ≤ x ∧ x < c + 1 - a
⊢ (a ≤ c - x ∧ c - x < b) ∧ c - (c - x) = x

Tactic:
lia

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

Goal state before:
pp: a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
⊢ c + 1 - b ≤ c - x ∧ c - x < c + 1 - a

Tactic:
lia

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

Goal state before:
pp: a b x : ℕ
⊢ a.succ ≤ x ∧ x < b ↔ x ≠ a ∧ a ≤ x ∧ x < b

Tactic:
lia

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

Goal state before:
pp: a b : ℕ
h : a ≤ b
x : ℕ
⊢ a ≤ x ∧ x < b.succ ↔ x = b ∨ a ≤ x ∧ x < b

Tactic:
lia

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

Goal state before:
pp: a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
⊢ n ≤ n + a

Tactic:
lia

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
⊢ n < n + n' - n - m

Tactic:
lia

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
⊢ n + n' - n - m + m = n'

Tactic:
lia

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

Goal state before:
pp: case inr.mpr.inr.refine_1
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ n ≤ i + a * (n / a)

Tactic:
lia

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

Goal state before:
pp: case inr.mpr.inr.refine_2
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < n + a

Tactic:
lia

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

Goal state before:
pp: case mp
a b x : ℕ
⊢ (∃ a_1 < b, a + a_1 = x) → a ≤ x ∧ x < a + b

Tactic:
lia

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

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

Tactic:
lia

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
⊢ Set.Ioo a b = ∅ ↔ ¬a < b

Tactic:
Set.Ioo_eq_empty_iff

Goal state after:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
⊢ ¬a < b ↔ ¬a < b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ b : ℕ
hb : b ∈ upperBounds {x | ∀ m ≥ x, P m}
n : ℕ
hn : ∀ m > n, P m
m : ℕ
hm : m ≥ n + b + 1
⊢ m > n

Tactic:
lia

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

Goal state before:
pp: P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ b n : ℕ
hb : n + b + 1 ≤ b
hn : ∀ m > n, P m
⊢ False

Tactic:
lia

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

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Set.Ioi a = ∅ ↔ IsMax a

Tactic:
Set.Ioi_eq_empty_iff

Goal state after:
α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ IsMax a ↔ IsMax a
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ r (f m) (f n)

Tactic:
rw [hmn]

Goal state after:
case refine_1.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ r (f n) (f n)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1.inr.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ r (f n) (f m)

Tactic:
rw [hmn]

Goal state after:
case refine_1.inr.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ r (f n) (f n)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a < b
⊢ #(Ioo a b) = #(Ico a b) - 1

Tactic:
Ioo_eq_empty h,

Goal state after:
case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a < b
⊢ #∅ = #(Ico a b) - 1
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ico a b ∪ Ico b c = Ico a c

Tactic:
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico_eq_Ico hab hbc]

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

Goal state before:
pp: case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : Quot.mk (⇑(IsConj.setoid G)) g ∈ (noncenter G)ᶜ
⊢ g ∈ ↑(Subgroup.center G)

Tactic:
simp only [mem_noncenter, Set.compl_def, Set.mem_ofPred, Set.not_nontrivial_iff] at hg

Goal state after:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ g ∈ ↑(Subgroup.center G)