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

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

Tactic:
rw [← choose_symm b]
      apply choose_le_middle_of_le_half_left
      lia

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pretransitive

Goal state before:
pp: G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
x y : X
⊢ ∃ g, g • x = y

Tactic:
rcases ha x with ⟨g, rfl⟩

Goal state after:
G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
y : X
g : G
⊢ ∃ g_1, g_1 • g • x₀ = y
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype ↑s
ht : Fintype ↑t
⊢ Fintype ↑((fun x ↦ f x.1 x.2) '' s ×ˢ t)

Tactic:
apply Set.fintypeImage

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
⊢ IsConj 1 a ↔ a = 1

Tactic:
refine ⟨fun ⟨c, h⟩ => ?_, fun h => by rw [h]⟩

Goal state after:
α : Type u
inst✝ : Monoid α
a : α
x✝ : IsConj 1 a
c : αˣ
h : SemiconjBy (↑c) 1 a
⊢ a = 1
Module: Mathlib.Algebra.Group.Submonoid.Defs

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝¹ x✝ : Submonoid M
s : Subsemigroup M
hs : 1 ∈ s.carrier
t : Subsemigroup M
ht : 1 ∈ t.carrier
⊢ { toSubsemigroup := s, one_mem' := hs }.toSubsemigroup = { toSubsemigroup := t, one_mem' := ht }.toSubsemigroup →
    { toSubsemigroup := s, one_mem' := hs } = { toSubsemigroup := t, one_mem' := ht }

Tactic:
by congr!

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
x✝ : β
⊢ x✝ ∈ f '' ⋃₀ s ↔ x✝ ∈ ⋃₀ (image f '' s)

Tactic:
simp only [Set.mem_iUnion, Set.sUnion_image]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
x✝ : β
⊢ x✝ ∈ f '' ⋃₀ s ↔ ∃ i, ∃ (_ : i ∈ s), x✝ ∈ f '' i
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
x' : α
hw : w ∈ t x'
⊢ ∃ i, z ∈ s i ∧ w ∈ t i

Tactic:
exact ⟨x ⊔ x', hs le_sup_left hz, ht le_sup_right hw⟩

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

Goal state before:
pp: case neg
M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
hxt : x ∉ t
⊢ x ∈ ↑(closure (s \ t))

Tactic:
rw [SetLike.mem_coe, Submonoid.mem_closure]
    exact fun N hN ↦ hN <| Set.mem_sdiff_of_mem hxs hxt

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : ↑p.toSubmonoid = ↑q.toSubmonoid
⊢ p = q

Tactic:
rw [coe_toSubmonoid, coe_toSubmonoid] at this

Goal state after:
G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : ↑p = ↑q
⊢ p = q
Module: Mathlib.Algebra.Group.Subgroup.Lattice

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

Tactic:
by
  rwa [← Subgroup.nontrivial_iff_exists_ne_one]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
⊢ x ∈ iSup K ↔ ∃ i, x ∈ K i

Tactic:
have : iSup K = ⨆ i : PLift ι, ⨆ (_ : True), K i.down := by simp [iSup_plift_down]

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
⊢ x ∈ iSup K ↔ ∃ i, x ∈ K i
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case mp.refine_1.inr
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x✝ : G
hx✝ : x✝ ∈ closure (↑s ∪ ↑t)
x : G
hx : x ∈ ↑t
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
· exact ⟨1, s.one_mem, x, hx, by simp⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
hs : s.Normal
x : G
h : x ∈ s ⊔ t ↔ ∃ y ∈ t, ∃ z ∈ s, y * z = x
x✝ : ∃ y ∈ s, ∃ z ∈ t, y * z = x
y : G
hy : y ∈ s
z : G
hz : z ∈ t
hp : y * z = x
⊢ z * (z⁻¹ * y * z) = x

Tactic:
simp [mul_assoc, hp]

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

Goal state before:
pp: A : Type u_2
inst✝ : AddGroup A
x : A
⊢ ↑(Subgroup.zpowers (Multiplicative.ofAdd x)) = ⇑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x)

Tactic:
Equiv.eq_image_iff_symm_image_eq

Goal state after:
A : Type u_2
inst✝ : AddGroup A
x : A
⊢ ⇑Multiplicative.ofAdd.symm '' ↑(Subgroup.zpowers (Multiplicative.ofAdd x)) = ↑(AddSubgroup.zmultiples x)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ normalizer s ≤ normalizer ↑(closure s)

Tactic:
by
  intro g hg
  rw [mem_normalizer_iff_conj_image_eq] at hg
  rw [mem_normalizer_iff_map_conj_eq, MonoidHom.map_closure, MonoidHom.coe_coe, hg]

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

Goal state before:
pp: case refine_4
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
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ g * x⁻¹ * g⁻¹ ∈ normalClosure s

Tactic:
rw [← conj_inv]

Goal state after:
case refine_4
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
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ (g * x * g⁻¹)⁻¹ ∈ normalClosure s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
⊢ normalClosure s ≤ N

Tactic:
intro a w

Goal state after:
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
⊢ a ∈ N
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
⊢ map f (normalClosure s) ≤ normalClosure (⇑f '' s)

Tactic:
simp [map_le_iff_le_comap, comap_normalClosure_image_ge]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
h₁ : ∀ (i : ι), i ∈ [] → f i ≤ g i
h₂ : ∃ i, i ∈ [] ∧ f i < g i
⊢ (map f []).prod < (map g []).prod

Tactic:
simp at h₂

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

Goal state before:
pp: α : Type u_1
s t r : Set α
h : Disjoint s t
⊢ Subtype.val '' Sum.inl ⁻¹' ⇑(sumSet h) ⁻¹' r = r ∩ s

Tactic:
by
  simp [Set.ext_iff]

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

Goal state before:
pp: α : Type u_1
s t r : Set α
h : Disjoint s t
⊢ Subtype.val '' Sum.inr ⁻¹' ⇑(sumSet h) ⁻¹' r = r ∩ t

Tactic:
by
  simp [Set.ext_iff]

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
⊢ range ⇑(sumSet h) = s ∪ t

Tactic:
by
  simp [Set.ext_iff]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
s : ι → Set α
h : Pairwise (Disjoint on s)
i : ι
r : Set α
⊢ Subtype.val '' Sigma.mk i ⁻¹' ⇑(sigmaSet h) ⁻¹' r = r ∩ s i

Tactic:
by
  simp [Set.ext_iff]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
s : ι → Set α
h : Pairwise (Disjoint on s)
⊢ range ⇑(sigmaSet h) = ⋃ i, s i

Tactic:
by
  simp [Set.ext_iff]

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

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x✝ : M
n : ℕ
hpos : 0 < n
hx : x✝ ^ n = 1
m : ℕ
x : ↥(powers x✝)
⊢ x ^ Int.negSucc m = (x ^ ↑m.succ) ^ (n - 1)

Tactic:
by
    change x ^ (Int.natMod _ n) = (x ^ (Int.natMod _ n)) ^ (n - 1)
    ext
    obtain ⟨_, k, rfl⟩ := x
    simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow]
    rw [Int.negSucc_eq, ← Int.natCast_succ, ← Int.add_mul_emod_self_right (b := (m + 1 : ℕ))]
    nth_rw 1 [← mul_one ((m + 1 : ℕ) : ℤ)]
    rw [← sub_eq_neg_add, ← Int.mul_sub, ← Int.natCast_pred_of_pos hpos]; norm_cast
    simp only [Int.toNat_natCast]
    rw [mul_comm, pow_mul, ← pow_eq_pow_mod _ hx, mul_comm k, mul_assoc, pow_mul _ (_ % _),
      ← pow_eq_pow_mod _ hx, pow_mul, pow_mul]

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

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ↑(Submonoid.powers (Multiplicative.ofAdd x)) = ⇑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x)

Tactic:
Equiv.eq_image_iff_symm_image_eq

Goal state after:
A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ⇑Multiplicative.ofAdd.symm '' ↑(Submonoid.powers (Multiplicative.ofAdd x)) = ↑(AddSubmonoid.multiples x)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
hd : α
tl : List α
m : α
⊢ m ∈ argmax f (hd :: tl) → m ∈ hd :: tl

Tactic:
by simpa [argmax, argAux] using foldl_argAux_mem _ tl hd m

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
n : ℕ
a : α
h : a ∈ decode n
e : encode a = n
⊢ encode (ofNat α n) = n

Tactic:
ofNat_of_decode h

Goal state after:
α : Type u_1
inst✝ : Denumerable α
n : ℕ
a : α
h : a ∈ decode n
e : encode a = n
⊢ encode a = n
Module: Mathlib.Data.Multiset.Sum

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

Tactic:
rintro ⟨b, _, hb⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
b : β
left✝ : b ∈ t
hb : inr b = inl a
⊢ False
Module: Mathlib.Data.List.Zip

Goal state before:
pp: α : Type u
l : List α
⊢ l.revzip.reverse = l.reverse.revzip

Tactic:
rw [← zip_unzip (revzip l).reverse]
  simp [unzip_eq_map, revzip, map_reverse, map_fst_zip, map_snd_zip]

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

Goal state before:
pp: case mp
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) = ([], hd :: tl) ∨ (init, tail) ∈ (map (fun t ↦ hd :: t) tl.inits).zip tl.tails → init ++ tail = hd :: tl

Tactic:
zip_map_left,

Goal state after:
case mp
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) = ([], hd :: tl) ∨ (init, tail) ∈ map (Prod.map (fun t ↦ hd :: t) id) (tl.inits.zip tl.tails) →
    init ++ tail = hd :: tl
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case mpr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl → (init, tail) = ([], hd :: tl) ∨ (init, tail) ∈ (map (fun t ↦ hd :: t) tl.inits).zip tl.tails

Tactic:
zip_map_left,

Goal state after:
case mpr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl →
    (init, tail) = ([], hd :: tl) ∨ (init, tail) ∈ map (Prod.map (fun t ↦ hd :: t) id) (tl.inits.zip tl.tails)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l : List α
s : Multiset α
⊢ ∀ (a : List α), ⟦a⟧ ∈ powersetAux l ↔ ⟦a⟧ ≤ ↑l

Tactic:
simp [powersetAux_eq_map_coe, Subperm, and_comm]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ List.map ofList l.sublists ~ powersetAux' l

Tactic:
exact (sublists_perm_sublists' _).map _

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

Goal state before:
pp: case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (b :: l₁).length (a :: l₂)

Tactic:
length,

Goal state after:
case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (l₁.length + 1) (a :: l₂)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons_cons
α : Type u
l l' l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
IH : l₁✝ ∈ sublistsLen l₁✝.length l₂✝
⊢ a :: l₁✝ ∈ sublistsLen (a :: l₁✝).length (a :: l₂✝)

Tactic:
length,

Goal state after:
case cons_cons
α : Type u
l l' l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
IH : l₁✝ ∈ sublistsLen l₁✝.length l₂✝
⊢ a :: l₁✝ ∈ sublistsLen (l₁✝.length + 1) (a :: l₂✝)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n ↦ sublistsLen n (h :: tl)) (0 :: map succ (range (h :: tl).length)) ~ (h :: tl).sublists'

Tactic:
length,

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n ↦ sublistsLen n (h :: tl)) (0 :: map succ (range (tl.length + 1))) ~ (h :: tl).sublists'
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: case zero
α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Trunc (P (ULift.{u, 0} (Fin 0)))

Tactic:
have : card PEmpty = card (ULift (Fin 0)) := by
      simp only [card_fin, card_pempty, card_ulift]
    apply Trunc.bind (truncEquivOfCardEq this)
    intro e
    apply Trunc.mk
    exact of_equiv e h_empty

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ (s.inf fun b ↦ a \ f b) = a \ s.sup f

Tactic:
by
  induction hs using Finset.Nonempty.cons_induction with
  | singleton => rw [sup_singleton, inf_singleton]
  | cons _ _ _ _ ih => rw [sup_cons, inf_cons, ih, sdiff_sup]

Goal state after:
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : ConditionallyCompletePartialOrderSup α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this : Nonempty β
h₁ : ∀ (m : β), f m ≤ g n
⊢ ⨆ n, f n ∈ Icc (f n) (g n)

Tactic:
have h₂ : Directed (· ≤ ·) f := hf.directed_le

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : ConditionallyCompletePartialOrderSup α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this : Nonempty β
h₁ : ∀ (m : β), f m ≤ g n
h₂ : Directed (fun x1 x2 ↦ x1 ≤ x2) f
⊢ ⨆ n, f n ∈ Icc (f n) (g n)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
⊢ ⋃ i, s i ⊆ ⋃ i ∈ t, s i

Tactic:
refine iUnion_subset fun i x hx => ?_

Goal state after:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
⊢ x ∈ ⋃ i ∈ t, s i
Module: Mathlib.Order.Cover

Goal state before:
pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
i : ι
hab : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
c : (i : ι) → α i
hac : a < c
hcb : c < b
haci : a i < c i
hcbi : c i < b i
⊢ False

Tactic:
exact hab.2 haci hcbi

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
t : Set β
f : α → β
inst✝ : Infinite α
hf : MapsTo f univ t
ht : t.Finite
a b : α
h : a < b ∧ f a = f b
⊢ ∃ a b, a < b ∧ f a = f b

Tactic:
exact ⟨a, b, h⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ a ≤ x ∧ x ≤ b ∧ x ≠ b ↔ a ≤ x ∧ x < b

Tactic:
lt_iff_le_and_ne

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ a ≤ x ∧ x ≤ b ∧ x ≠ b ↔ a ≤ x ∧ x ≤ b ∧ x ≠ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ (a ≤ x ∧ a ≠ x) ∧ x ≤ b ↔ a < x ∧ x ≤ b

Tactic:
lt_iff_le_and_ne

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ (a ≤ x ∧ a ≠ x) ∧ x ≤ b ↔ (a ≤ x ∧ a ≠ x) ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ (a ≤ x ∧ a ≠ x) ∧ x ≤ b ∧ x ≠ b ↔ (a ≤ x ∧ a ≠ x) ∧ x < b

Tactic:
lt_iff_le_and_ne

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ (a ≤ x ∧ a ≠ x) ∧ x ≤ b ∧ x ≠ b ↔ (a ≤ x ∧ a ≠ x) ∧ x ≤ b ∧ x ≠ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
⊢ a ≤ x ∧ a ≠ x ↔ a < x

Tactic:
lt_iff_le_and_ne

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
⊢ a ≤ x ∧ a ≠ x ↔ a ≤ x ∧ a ≠ x
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
hIoc : h₀_finset_Ioc = h₁_finset_Ioc
a b x : α
⊢ x ∈ h₀_finset_Ioo a b ↔ x ∈ h₁_finset_Ioo a b

Tactic:
h₀_finset_mem_Ioo,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
hIoc : h₀_finset_Ioc = h₁_finset_Ioc
a b x : α
⊢ a < x ∧ x < b ↔ x ∈ h₁_finset_Ioo a b
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : ℕ → α
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
by
  classical
    let bad : Set ℕ := { m | ∀ n, m < n → ¬r (f m) (f n) }
    by_cases hbad : Infinite bad
    · refine ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => ?_⟩
      have h := @Set.mem_range_self _ _ ↑(Nat.orderEmbeddingOfSet bad) m
      rw [Nat.orderEmbeddingOfSet_range bad] at h
      exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn)
    · rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad
      obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → n ∉ bad := by
        by_cases he : hbad.toFinset.Nonempty
        · refine
            ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
              Nat.not_succ_le_self _
                (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
        · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
      have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) := by
        intro n
        have h := hm _ (Nat.le_add_left m n)
        simp only [bad, exists_prop, not_not, Set.mem_ofPred_eq, not_forall] at h
        obtain ⟨n', hn1, hn2⟩ := h
        refine ⟨n + n' - n - m, by lia, ?_⟩
        convert! hn2
        lia
      let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn)
      exact
        ⟨(RelEmbedding.natLT (fun n => g' n + m) fun n =>
              Nat.add_lt_add_right (Nat.find_spec (h (g' n))).1 m).orderEmbeddingOfLTEmbedding,
          Or.intro_left _ fun n => (Nat.find_spec (h (g' n))).2⟩

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : ℕ →o α
n m : ℕ
h : n ≤ m
⊢ ¬a n < a m ↔ a n = a m

Tactic:
lt_iff_le_and_ne

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : ℕ →o α
n m : ℕ
h : n ≤ m
⊢ ¬(a n ≤ a m ∧ a n ≠ a m) ↔ a n = a m
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
⊢ WellQuasiOrdered fun a b ↦ r a.1 b.1 ∧ s a.2 b.2

Tactic:
by
  intro f
  obtain ⟨g, h₁⟩ := hr.exists_monotone_subseq (Prod.fst ∘ f)
  obtain ⟨m, n, h, hf⟩ := hs (Prod.snd ∘ f ∘ g)
  exact ⟨g m, g n, g.strictMono h, h₁ _ _ h.le, hf⟩

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

Goal state before:
pp: P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ ¬BddAbove {x | ∀ m ≥ x, P m}

Tactic:
· rintro ⟨b, hb⟩
    rcases base with ⟨n, hn⟩
    specialize @hb (n + b + 1) (fun m hm ↦ hn _ _)
    all_goals lia

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

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

Tactic:
rintro _ ⟨m, rfl⟩ _ ⟨n, rfl⟩ _ hf

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
a✝ : (f ∘ ⇑g) m ≠ (f ∘ ⇑g) n
hf : (f ∘ ⇑g) m ≤ (f ∘ ⇑g) n
⊢ False
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
g : ↥H
h : ↑g • ↑b = ↑a
⊢ a ∈ orbit (↥H) b

Tactic:
← orbit.coe_smul,

Goal state after:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
g : ↥H
h : ↑(↑g • b) = ↑a
⊢ a ∈ orbit (↥H) b