mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ 1 < card α ↔ Nontrivial α

Tactic:
by
  contrapose!; exact card_le_one_iff_subsingleton

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
⊢ (∃ i, P i) → P p ∨ ∃ i, P (p.succAbove i)

Tactic:
by
    rintro ⟨i, hi⟩
    induction i using p.succAboveCases
    · exact .inl hi
    · exact .inr ⟨_, hi⟩

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hs : s ⊆ range f
⊢ s.Finite

Tactic:
rw [← image_preimage_eq_of_subset hs]

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hs : s ⊆ range f
⊢ (f '' f ⁻¹' s).Finite
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_2.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
⊢ (replicate 2 x).get ⟨n✝ + 1, hi⟩ =
    l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ⟨n✝ + 1, hi⟩)

Tactic:
· simpa using h'

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

Goal state before:
pp: case cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → c <+ tail✝ → c <+ insertionSort r tail✝
l₁✝ : List α
hr : Pairwise r (head✝ :: l₁✝)
h : l₁✝ <+ tail✝
⊢ head✝ :: l₁✝ <+ insertionSort r (head✝ :: tail✝)

Tactic:
obtain ⟨hr, hp⟩ := pairwise_cons.mp hr
      exact cons_sublist_orderedInsert (ih hp h) hr

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → c <+ tail✝ → c <+ insertionSort r tail✝
c : List α
hr : Pairwise r c
hc : c <+ head✝ :: tail✝
⊢ c <+ insertionSort r (head✝ :: tail✝)

Tactic:
| cons _ _ ih =>

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

Goal state before:
pp: case refine_2.rel
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂

pp: case refine_2.cons
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ r a a ∨ a = a ∧ Lex r l₁ l₂

Tactic:
· exact Or.inl h

Goal state after:
case refine_2.cons
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ r a a ∨ a = a ∧ Lex r l₁ l₂
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun a b ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun a b ↦ R b a) (y :: l)
⊢ IsChain R (a :: b :: l).reverse ↔ IsChain (fun a b ↦ R b a) (a :: b :: l)

Tactic:
rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      isChain_split, ← reverse_cons, IH2, and_comm, isChain_pair]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ l.prod = (map op (map unop l).reverse).reverse.prod

Tactic:
map_reverse,

Goal state after:
M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ l.prod = (map op (map unop l)).reverse.reverse.prod
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → β
a✝ : Multiset α
s✝ : Multiset (Multiset α)
ih : map f s✝.join = (map (map f) s✝).join
⊢ map f (a✝ ::ₘ s✝).join = (map (map f) (a✝ ::ₘ s✝)).join

Tactic:
| cons _ _ ih =>

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : CommMonoid α
a✝ : Multiset α
s✝ : Multiset (Multiset α)
ih : s✝.join.prod = (map prod s✝).prod
⊢ (a✝ ::ₘ s✝).join.prod = (map prod (a✝ ::ₘ s✝)).prod

Tactic:
| cons _ _ ih =>

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

Goal state before:
pp: case cons
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a✝ : Multiset α
s✝ : Multiset (Multiset α)
ih : filter p s✝.join = (map (filter p) s✝).join
⊢ filter p (a✝ ::ₘ s✝).join = (map (filter p) (a✝ ::ₘ s✝)).join

Tactic:
| cons _ _ ih =>

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → Option β
a✝ : Multiset α
s✝ : Multiset (Multiset α)
ih : filterMap f s✝.join = (map (filterMap f) s✝).join
⊢ filterMap f (a✝ ::ₘ s✝).join = (map (filterMap f) (a✝ ::ₘ s✝)).join

Tactic:
| cons _ _ ih =>

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

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
s z : Multiset M
h : s ≤ s + z
⊢ s.prod ∣ (s + z).prod

Tactic:
simp only [prod_add, dvd_mul_right]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b ↦ count a (f b)) S = count a (f x) ::ₘ m'
⊢ count a (f x) ≤ count a (S.bind f)

Tactic:
count_bind,

Goal state after:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b ↦ count a (f b)) S = count a (f x) ::ₘ m'
⊢ count a (f x) ≤ (map (fun b ↦ count a (f b)) S).sum
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
h : 0 < l.cyclicPermutations.length
⊢ l.cyclicPermutations.head ⋯ = l

Tactic:
rw [← get_mk_zero h, get_cyclicPermutations, Fin.val_mk, rotate_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

Tactic:
by
  refine
    ⟨fun H => ?_, fun H =>
      H.elim (and_imp.2 <| @Prod.infinite_of_left α β) (and_imp.2 <| @Prod.infinite_of_right α β)⟩
  rw [and_comm]
  rcases Infinite.nonempty (α × β) with ⟨a, b⟩
  contrapose! H; have := H.1 ⟨b⟩; have := H.2 ⟨a⟩
  infer_instance

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

Goal state before:
pp: i j : ℕ
⊢ (i + j).choose j = (i + j)! / (i ! * j !)

Tactic:
by
  rw [choose_eq_factorial_div_factorial (Nat.le_add_left j i), Nat.add_sub_cancel_right,
    Nat.mul_comm]

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

Goal state before:
pp: E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
x : G
m : F
⊢ ∃ g, g • x = m • x

Tactic:
obtain ⟨e, rfl⟩ : ∃ e, f e = m := hf m

Goal state after:
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
x : G
e : E
⊢ ∃ g, g • x = f e • x
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ kernImage f ∅ = (range f)ᶜ

Tactic:
rw [kernImage_eq_compl, compl_empty, image_univ]

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

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

Tactic:
by
  ext1 x
  simp only [mem_image, mem_iUnion, ← exists_and_right, exists_comm (α := α)]

Goal state after:
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 : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i

Tactic:
intro x hz x' hw

Goal state after:
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
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor
  · contrapose! +distrib
    rintro (hs | rfl)
    · exact hs.pow
    · simp
  · rintro ⟨rfl, hn⟩
    exact empty_pow hn

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ univ * univ = univ

Tactic:
univ_mul_univ

Goal state after:
α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ univ = univ
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a : α
⊢ (fun x ↦ a * x) ⁻¹' 1 = {a⁻¹}

Tactic:
by
  rw [← image_mul_left', image_one, mul_one]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H = ⊥ ∨ Nontrivial ↥H

Tactic:
have := nontrivial_iff_ne_bot H

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : Nontrivial ↥H ↔ H ≠ ⊥
⊢ H = ⊥ ∨ Nontrivial ↥H
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ↑(map K.subtype (H.subgroupOf K)) = ↑(H ⊓ K)

Tactic:
refine Subtype.image_preimage_coe _ _ |>.trans ?_

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ↑K ∩ H.toSubsemigroup.1 = ↑(H ⊓ K)
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
⊢ Injective ⇑f.rangeRestrict ↔ Injective ⇑f

Tactic:
by
  convert! Set.injective_codRestrict _

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

Goal state before:
pp: α : Sort u
⊢ ¬Uncountable α ↔ Countable α

Tactic:
by
  rw [uncountable_iff_not_countable, not_not]

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

Goal state before:
pp: M : Type u_1
inst✝³ : MulOneClass M
N : Type u_5
S : Type u_6
inst✝² : MulOneClass N
f : M →* N
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
s : S
⊢ f.domRestrict s = 1 ↔ ∀ x ∈ s, f x = 1

Tactic:
by
  simp [MonoidHom.ext_iff]

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

Goal state before:
pp: m n : ℕ
⊢ (m * n).bodd = (m.bodd && n.bodd)

Tactic:
by
  induction n with
  | zero => simp
  | succ n IH =>
    simp only [mul_succ, bodd_add, IH, bodd_succ]
    cases bodd m <;> cases bodd n <;> rfl

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

Goal state before:
pp: case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ n.sqrt < n

Tactic:
simp only [not_lt] at h
    have s0 : 0 < s := sqrt_pos.2 n1
    exact lt_of_le_of_lt h (Nat.sub_lt n1 (Nat.mul_pos s0 s0))

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

Goal state before:
pp: n : ℕ
⊢ n.div2.bits = n.bits.tail

Tactic:
by
  induction n using Nat.binaryRec' with
  | zero => simp
  | bit _ _ h => simp [div2_bit, bits_append_bit _ _ h]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Set β
⊢ (fun a ↦ a) '' s = s

Tactic:
image_id'

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsIdempotentElem a
i : ℕ
hn : i + 1 ≠ 0
⊢ a ^ (i + 1) = a

Tactic:
exact h.pow_succ_eq _

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

Goal state before:
pp: case inr.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ * b✝ ∈ {1, b✝}

Tactic:
· rw [ha]; exact .inr rfl

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
    (foldl (argAux r) o (tl ++ [hd]) = none ↔ tl ++ [hd] = [] ∧ o = none)

Tactic:
by
    simp only [foldl_append, foldl_cons, argAux, foldl_nil, append_eq_nil_iff]
    cases foldl (argAux r) o tl
    · simp
    · simp only
      split_ifs <;> simp

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

Goal state before:
pp: case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ foldl (argAux r) o (tl ++ [a])
⊢ ¬r b m

Tactic:
rw [foldl_append, foldl_cons, foldl_nil, argAux] at ho

Goal state after:
case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c ↦ if r a c then some a else some c
⊢ ¬r b m
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
l₂ : List α
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).maximum = max tail✝.maximum l₂.maximum
⊢ (head✝ :: tail✝ ++ l₂).maximum = max (head✝ :: tail✝).maximum l₂.maximum

Tactic:
| cons _ _ ih =>

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
P : β → Prop
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)
this : Lattice { x // P x } := Subtype.lattice Psup Pinf
⊢ ∀ (a b : { x // P x }),
    (SupHom.subtypeVal Psup).toFun (a ⊓ b) = (SupHom.subtypeVal Psup).toFun a ⊓ (SupHom.subtypeVal Psup).toFun b

Tactic:
simp [Subtype.coe_inf Pinf]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ (insert a ∅).max = ↑a

Tactic:
exact max_insert

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ s.min = ⊤ ↔ s = ∅

Tactic:
simp [Finset.min, eq_empty_iff_forall_notMem]

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

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

Tactic:
· exact h.cons_cons _

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

Goal state before:
pp: case cons.mpr.cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s

pp: case cons.mpr.cons_cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
l₁✝ : List α
h : l₁✝ <+ t
⊢ a :: l₁✝ <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: l₁✝

Tactic:
· exact Or.inl h

Goal state after:
case cons.mpr.cons_cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
l₁✝ : List α
h : l₁✝ <+ t
⊢ a :: l₁✝ <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: l₁✝
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case succ.swap.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) (a :: l✝)) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a) (powersetCardAux (n✝ + 1) (b :: l✝))

Tactic:
simp only [powersetCardAux_cons, map_append, List.map_map]

Goal state after:
case succ.swap.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++
      (List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b ∘ cons a) (powersetCardAux n✝ l✝)) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      (List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝))
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case cons
α : Type u_1
a✝ : α
s✝ : Multiset α
ih : powersetCard s✝.card s✝ = {s✝}
⊢ powersetCard (a✝ ::ₘ s✝).card (a✝ ::ₘ s✝) = {a✝ ::ₘ s✝}

Tactic:
| cons _ _ ih =>

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

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (cons a✝ s✝ h✝).sup (f ⊔ g) = (cons a✝ s✝ h✝).sup f ⊔ (cons a✝ s✝ h✝).sup g

Tactic:
rw [sup_cons, sup_cons, sup_cons, ih]

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (f ⊔ g) a✝ ⊔ (s✝.sup f ⊔ s✝.sup g) = f a✝ ⊔ s✝.sup f ⊔ (g a✝ ⊔ s✝.sup g)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : IsEmpty β
f : β → α
S : Finset β
⊢ ∀ s ∈ S, f s = ⊥

Tactic:
exact fun x _ => False.elim <| IsEmpty.false x

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

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

Tactic:
rw [← card_map Function.Embedding.some, map_some_eraseNone]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : p
⊢ ⨆ (h : p), f h = f hp

Tactic:
by
  simp [hp]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow (⋃ i, range (f i))
⊢ BddBelow (range fun i ↦ ⨅ j, f i j)

Tactic:
have ⟨a, h⟩ := H
  refine ⟨a ⊓ (sInf ∅), fun x ⟨i, hx⟩ ↦ hx ▸ ?_⟩
  cases isEmpty_or_nonempty <| κ i
  · exact iInf_of_isEmpty (f i) ▸ inf_le_right
  exact le_ciInf fun j ↦ inf_le_of_left_le <| h ⟨_, ⟨i, rfl⟩, ⟨j, rfl⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
b : β
f : (x : β) → x = b → α
⊢ f b ⋯ ≤ ⨆ x, ⨆ (h : x = b), f x h

Tactic:
refine le_ciSup₂ (f := f) ⟨f b rfl, ?_⟩ b rfl

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
b : β
f : (x : β) → x = b → α
⊢ f b ⋯ ∈ upperBounds (⋃ i, range (f i))
Module: Mathlib.Order.Cover

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
h : (a₁, b₁) ⋖ (a₂, b₂)
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⋖ (a₂, b₂)

Tactic:
· obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h.wcovBy
    · exact Or.inr ⟨mk_covBy_mk_iff_right.1 h, rfl⟩
    · exact Or.inl ⟨mk_covBy_mk_iff_left.1 h, rfl⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⋖ (a₂, b₂)
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ⩿ b
⊢ ∃ i, ∀ (j : ι), j ≠ i → a j = b j

Tactic:
obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h
  exact ⟨i, fun j hj ↦ AntisymmRel.eq (hi _ hj)⟩

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ Nat.find ⋯ ≤ m

Tactic:
exact Nat.find_min' ⟨m, hm⟩ hm

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

Goal state before:
pp: a b c : ℕ
h : c ≤ a
⊢ image (fun x ↦ x - c) (Ico a b) = Ico (a - c) (b - c)

Tactic:
ext x
  simp_rw [mem_image, mem_Ico]
  refine ⟨?_, fun h ↦ ⟨x + c, by lia⟩⟩
  rintro ⟨x, hx, rfl⟩
  lia

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
h : a < b
⊢ Ioi b ⊂ Ioi a

Tactic:
simpa [← coe_ssubset] using Set.Ioi_ssubset_Ioi h

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

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderTop α
inst✝ : Fintype α
a : α
⊢ a ∈ Iic ⊤ ↔ a ∈ univ

Tactic:
simp only [mem_Iic, le_top, mem_univ]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
⊢ (s ∪ t).PartiallyWellOrderedOn r

Tactic:
intro f
  obtain ⟨g, hgs | hgt⟩ := Nat.exists_subseq_of_forall_mem_union _ fun x ↦ (f x).2
  · rcases hs.exists_lt hgs with ⟨m, n, hlt, hr⟩
    exact ⟨g m, g n, g.strictMono hlt, hr⟩
  · rcases ht.exists_lt hgt with ⟨m, n, hlt, hr⟩
    exact ⟨g m, g n, g.strictMono hlt, hr⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_2.inl
α : 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 : ℕ
hf : f (g m) = f (g n)
h : m < n
⊢ m = n

Tactic:
first | rfl | cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_2.inr.inl
α : 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 : ℕ
hf : f (g m) = f (g m)
⊢ m = m

Tactic:
first | rfl | cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_2.inr.inr
α : 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 : ℕ
hf : f (g m) = f (g n)
h : n < m
⊢ m = n

Tactic:
first | rfl | cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst✝ : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
⊢ (s ×ˢ t).PartiallyWellOrderedOn fun x y ↦ r x.1 y.1 ∧ r' x.2 y.2

Tactic:
rw [partiallyWellOrderedOn_iff_exists_lt]
  intro f hf
  obtain ⟨g₁, h₁⟩ := hs.exists_monotone_subseq fun n => (hf n).1
  obtain ⟨m, n, hlt, hle⟩ := ht.exists_lt fun n => (hf _).2
  exact ⟨g₁ m, g₁ n, g₁.strictMono hlt, h₁ _ _ hlt.le, hle⟩

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

Goal state before:
pp: ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (↑univ).Pairwise (Commute on fun i ↦ (MonoidHom.mulSingle M i) (x i))

Tactic:
intro i _ j _ _

Goal state after:
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i✝ i : ι
a✝² : i ∈ ↑univ
j : ι
a✝¹ : j ∈ ↑univ
a✝ : i ≠ j
⊢ (Commute on fun i ↦ (MonoidHom.mulSingle M i) (x i)) i j
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient r × Quotient s
⊢ (fun q ↦ q.liftOn' (fun xy ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯)
      ((fun x ↦
          match x with
          | (x, y) => Quotient.map₂ Prod.mk ⋯ x y)
        q) =
    q

Tactic:
rcases q with ⟨qa, qb⟩
    induction qa, qb using Quotient.inductionOn₂'
    rfl

Goal state after: