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

Goal state before:
pp: case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
simp at h₁
    simp only [not_lt_of_gt (lt_of_le_of_lt h₁ h), ite_false]
    apply add_lt_add
    · exact Nat.mul_self_lt_mul_self h
    · apply Nat.add_lt_add_right; assumption

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

Goal state before:
pp: a b₁ b₂ : ℕ
h : b₁ < b₂
⊢ pair a b₁ < pair a b₂

Tactic:
by_cases h₁ : a < b₁

Goal state after:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : a < b₁
⊢ pair a b₁ < pair a b₂

case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ pair a b₁ < pair a b₂
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case zero
⊢ bodd 0 = (bits 0).headI

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ (div2 0).bits = (bits 0).tail

Tactic:
| zero =>

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ (H.subgroupOf K).Normal ↔ K ≤ normalizer ↑H

Tactic:
by
  rw [← subgroupOf_eq_top, subgroupOf_normalizer_eq h, normalizer_eq_top_iff]

Goal state after:
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

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
⊢ x ∈ ⨆ (h : p), S h ↔ x = 1 ∨ ∃ (h : p), x ∈ S h

Tactic:
by
  by_cases h : p <;>
  simp +contextual [h]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : M) (x : ι), a ∈ S x → ∀ (b : M) (x : ι), b ∈ S x → a * b = b * a

Tactic:
intro a

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : M
⊢ ∀ (x : ι), a ∈ S x → ∀ (b : M) (x : ι), b ∈ S x → a * b = b * a
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ Lex r s a b ↔ r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

Tactic:
constructor
  · rintro (⟨a, b, hij⟩ | ⟨i, hab⟩)
    · exact Or.inl hij
    · exact Or.inr ⟨rfl, hab⟩
  · obtain ⟨i, a⟩ := a
    dsimp only
    rintro (h | ⟨rfl, h⟩)
    · exact Lex.left _ _ h
    · exact Lex.right _ h

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
i : ι
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S

Tactic:
rw [← SetLike.le_def]
  exact le_iSup _ _

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
y : Lex (α × β)
x : α × β
h : toLex x < y
⊢ ∃ a, toLex x < a ∧ a < y

Tactic:
cases y with

Goal state after:
case h.h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : toLex x < toLex y
⊢ ∃ a, toLex x < a ∧ a < toLex y
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
y : Lex (α × β)
x : α × β
h : toLex x < y
⊢ ∃ a, toLex x < a ∧ a < y

Tactic:
cases y with

Goal state after:
case h.h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : toLex x < toLex y
⊢ ∃ a, toLex x < a ∧ a < toLex y
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
⊢ ∀ (a : α) (b : β), ∃ b_1, toLex (a, b) < b_1

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
a : α
⊢ ∀ (b : β), ∃ b_1, toLex (a, b) < b_1
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
⊢ ∀ (a : α) (b : β), ∃ b_1, toLex (a, b) < b_1

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
a : α
⊢ ∀ (b : β), ∃ b_1, toLex (a, b) < b_1
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ ∀ (l : List α) (a : α),
    (∀ (a m : α), m ∈ foldl (argAux r) (some a) l → m ∈ a :: l) →
      ∀ (a_2 m : α), m ∈ foldl (argAux r) (some a_2) (l ++ [a]) → m ∈ a_2 :: (l ++ [a])

Tactic:
intro _ _ _ _

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝² : α
a✝¹ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
a✝ : α
⊢ ∀ (m : α), m ∈ foldl (argAux r) (some a✝) (l✝ ++ [a✝²]) → m ∈ a✝ :: (l✝ ++ [a✝²])
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a ∈ decode 0, encode a = 0

Tactic:
| zero =>

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
val✝ : α
h : argmax f tl = some val✝
h✝ : ¬f hd < f val✝
ham : f hd ≤ f hd
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

Tactic:
rw [if_pos rfl]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
rw [if_pos rfl]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ 0 ≤ if hd = a then 0 else idxOf a tl + 1
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
⊢ ∀ a ∈ List.filter (fun y ↦ decide (y ∈ s)) (List.range x), a ∈ s

Tactic:
intro a

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
a : ℕ
⊢ a ∈ List.filter (fun y ↦ decide (y ∈ s)) (List.range x) → a ∈ s
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ (map (Equiv.sumComm α β).toEmbedding u).toLeft = u.toRight

Tactic:
by
  ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ (map (Equiv.sumComm α β).toEmbedding u).toRight = u.toLeft

Tactic:
by
  ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (image Sum.swap u).toLeft = u.toRight

Tactic:
by
  ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (image Sum.swap u).toRight = u.toLeft

Tactic:
by
  ext x; simp

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
l✝ : List α
b : WithBot α
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ↑a ≤ b) → l.maximum ≤ b
h : ∀ (a_1 : α), a_1 ∈ a :: l → ↑a_1 ≤ b
⊢ ↑a ≤ b ∧ l.maximum ≤ b

Tactic:
exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩

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

Goal state before:
pp: case zero
α : Type u
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen 0 l₁ <+ sublistsLen 0 l₂

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetCardAux 0 l₁ ~ powersetCardAux 0 l₂

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
n : ℕ
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetCardAux n l₁ ~ powersetCardAux n l₂

Tactic:
induction n generalizing l₁ l₂ with | zero => simp | succ n IHn => ?_
  induction p with
  | nil => rfl
  | cons _ p IH =>
    simp only [powersetCardAux_cons]
    exact IH.append ((IHn p).map _)
  | swap a b =>
    simp only [powersetCardAux_cons, append_assoc]
    apply Perm.append_left
    cases n
    · simp [Perm.swap]
    simp only [powersetCardAux_cons, map_append, List.map_map]
    rw [← append_assoc, ← append_assoc,
      (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
    exact perm_append_comm.append_right _
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂

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

Goal state before:
pp: α : Type u_1
n : ℕ
s t : Multiset α
h✝ : s ≤ t
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ powersetCard n ↑l₁ ≤ powersetCard n ↑l₂

Tactic:
simp only [powersetCard_coe, coe_le]

Goal state after:
α : Type u_1
n : ℕ
s t : Multiset α
h✝ : s ≤ t
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ List.map ofList (sublistsLen n l₁) <+~ List.map ofList (sublistsLen n l₂)
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a : ι
ha : a ∈ ⋃ i ∈ s, g i
b : ι
hb : b ∈ ⋃ i ∈ s, g i
hab : a ≠ b
⊢ (Disjoint on f) a b

Tactic:
simp_rw [Set.mem_iUnion] at ha hb

Goal state after:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
ha : ∃ i, ∃ (_ : i ∈ s), a ∈ g i
hb : ∃ i, ∃ (_ : i ∈ s), b ∈ g i
⊢ (Disjoint on f) a b
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
hcd : g c ≠ g d
⊢ (Disjoint on f) a b

Tactic:
exact (hs hc hd <| ne_of_apply_ne _ hcd).mono
      (le_iSup₂ (f := fun i _ => f i) a ha)
      (le_iSup₂ (f := fun i _ => f i) b hb)

Goal state after:
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'
⊢ sublistsLen 0 tl ++ flatMap (fun a ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
      map (cons h) (flatMap (fun a ↦ sublistsLen a tl) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Tactic:
refine Perm.append ?_ (l_ih.map _)

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

Goal state before:
pp: α : Type u_1
s t : Finset α
a : α
ht : t ∈ s.powerset
h : a ∉ s
⊢ a ∉ t

Tactic:
apply mt _ h

Goal state after:
α : Type u_1
s t : Finset α
a : α
ht : t ∈ s.powerset
h : a ∉ s
⊢ a ∈ t → a ∈ s
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ (↑s.powerset).PairwiseDisjoint fun t ↦ {t, insert a t}

Tactic:
Set.pairwiseDisjoint_iff,

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ ∀ ⦃i : Finset α⦄,
    i ∈ ↑s.powerset → ∀ ⦃j : Finset α⦄, j ∈ ↑s.powerset → ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j
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.sup f = ⊥

Tactic:
rw [Finset.sup_eq_bot_iff]
  exact fun x _ => False.elim <| IsEmpty.false x

Goal state after:
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:
| zero =>

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ (∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t) → t ⊆ map f s ∧ #t = n

Tactic:
rintro ⟨a, ⟨has, rfl⟩, rfl⟩
      simp [has]

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

Goal state before:
pp: ι : Type u_5
α : Type u_7
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
cases subsingleton_or_nontrivial α

Goal state after:
case inl
ι : Type u_5
α : Type u_7
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
h✝ : Subsingleton α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

case inr
ι : Type u_5
α : Type u_7
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
h✝ : Nontrivial α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
⊢ WithBot.recBotCoe True p ↑(s.sup' H f)

Tactic:
coe_sup'

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
⊢ WithBot.recBotCoe True p (s.sup (WithBot.some ∘ f))
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SemilatticeSup α
s : Finset γ
f : γ ↪ β
g : β → α
hs : (map f s).Nonempty
⊢ s.sup ((WithBot.some ∘ g) ∘ ⇑f) = ↑(s.sup' ⋯ (g ∘ ⇑f))

Tactic:
coe_sup'

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SemilatticeSup α
s : Finset γ
f : γ ↪ β
g : β → α
hs : (map f s).Nonempty
⊢ s.sup ((WithBot.some ∘ g) ∘ ⇑f) = s.sup (WithBot.some ∘ g ∘ ⇑f)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i ↦ ⟨Exists.choose ⋯, ⋯⟩
u_inj : Injective u
this : Finite ↑(⋃ i, s i)
⊢ {i | (s i).Nonempty}.Finite

Tactic:
exact .of_injective u u_inj

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s ⋖ insert a s

Tactic:
exact covBy_insert ha

Goal state after:
Module: Mathlib.Order.Cover

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

Tactic:
by
  refine ⟨fun h => ?_, ?_⟩
  · 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⟩
  · rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)
    · exact mk_covBy_mk_iff_left.2 h
    · exact mk_covBy_mk_iff_right.2 h

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
by
  classical
  simp only [CovBy, Pi.lt_def, not_and, and_imp, forall_exists_index, not_exists] at h
  obtain ⟨⟨hab, ⟨i, hi⟩⟩, h⟩ := h
  refine ⟨i, fun j hj ↦ ?_⟩
  let c : (i : ι) → α i := Function.update a i (b i)
  have h₁ : c ≤ b := by simpa [update_le_iff, c] using fun k hk ↦ hab k
  have h₂ : ¬ c j < b j := h (by simp [c, hi.le]) i (by simpa [c]) h₁ j
  exact ⟨hab j, by simpa [lt_iff_le_not_ge, hab j, c, hj] using h₂⟩

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

Goal state before:
pp: case inl.mpr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx : x.snd ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) (⋯ ▸ ⟨x.1, b⟩.snd)
⊢ ∃ a_1 ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) ⟨x.1, b⟩.snd, (Embedding.sigmaMk ⟨x.1, b⟩.fst) a_1 = x

Tactic:
exact ⟨_, hx, by simp⟩

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

Goal state before:
pp: α : Type u
β : Type v
s : Finset (α ⊕ β)
⊢ s.preimage Sum.inl ⋯ = s.toLeft

Tactic:
by
  ext x; simp

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

Goal state before:
pp: α : Type u
β : Type v
s : Finset (α ⊕ β)
⊢ s.preimage Sum.inr ⋯ = s.toRight

Tactic:
by
  ext x; simp

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

Goal state before:
pp: s : Set ℕ
hs : ¬BddAbove s
⊢ (if h : ∃ n, ∀ a ∈ s, a ≤ n then Nat.find h else 0) = Nat.find ⋯

Tactic:
dif_neg

Goal state after:
s : Set ℕ
hs : ¬BddAbove s
⊢ 0 = Nat.find ⋯

case hnc
s : Set ℕ
hs : ¬BddAbove s
⊢ ¬∃ n, ∀ a ∈ s, a ≤ n
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case zero
a : ℕ
⊢ Set.InjOn (fun x ↦ x % a) ↑(Ico 0 (0 + a))

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b x : α × β
⊢ x ∈ Icc a.1 b.1 ×ˢ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b

Tactic:
mem_product,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b x : α × β
⊢ x.1 ∈ Icc a.1 b.1 ∧ x.2 ∈ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : LocallyFiniteOrderTop β
inst✝ : DecidableLE (α × β)
a x : α × β
⊢ x ∈ Ici a.1 ×ˢ Ici a.2 ↔ a ≤ x

Tactic:
mem_product,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : LocallyFiniteOrderTop β
inst✝ : DecidableLE (α × β)
a x : α × β
⊢ x.1 ∈ Ici a.1 ∧ x.2 ∈ Ici a.2 ↔ a ≤ x
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inl.zero
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m : ℕ
mn : m < m.succ + 0
⊢ r (f (g m)) (f (g (m.succ + 0)))

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
⊢ Min.min (hs.min hsn) (ht.min htn) ≤ ⋯.min ⋯

Tactic:
min_le_iff

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
⊢ hs.min hsn ≤ ⋯.min ⋯ ∨ ht.min htn ≤ ⋯.min ⋯
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
⊢ hs.min hsn ≤ ⋯.min ⋯ ∨ ht.min htn ≤ ⋯.min ⋯

Tactic:
exact ((mem_union _ _ _).1 ((hs.union ht).min_mem (union_nonempty.2 (.inl hsn)))).imp
    (hs.min_le _) (ht.min_le _)

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case zero
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
m : ℕ
⊢ ↑(fs m) m = ↑(fs (m + 0)) m

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
m k : ℕ
⊢ ↑(fs m) m = ↑(fs (m + k)) m

Tactic:
induction k with
    | zero => rfl
    | succ k ih =>
      rw [ih, (minBadSeqOfBadSeq r rk s (m + k + 1) (fs (m + k)).1 (fs (m + k)).2.1).2.1 m
        (Nat.lt_succ_iff.2 (Nat.add_le_add_left k.zero_le m))]
      rfl

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
⊢ ∀ (x y : ConjAct Mˣ) (b : M), (x * y) • b = x • y • b

Tactic:
simp [units_smul_def, mul_assoc]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
⊢ ∀ (r : ConjAct Mˣ) (x y : M), r • (x * y) = r • x * r • y

Tactic:
simp [units_smul_def, mul_assoc]

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

Goal state before:
pp: case zero
α : Type u_1
M : Type u_2
inst✝ : Monoid M
f : α → M
⊢ (mulSupport fun x ↦ f x ^ 0) ⊆ mulSupport f

Tactic:
| zero =>

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 = ⊤
⊢ centralizer ↑⊤ = ⨅ g ∈ s, centralizer {g}

Tactic:
← hs,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
hs : closure s = ⊤
⊢ centralizer ↑(closure s) = ⨅ g ∈ s, centralizer {g}
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

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

Tactic:
closure_toSubmonoid

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
x : G
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x⁻¹ * y) ⋯
⊢ ∀ (h : x ∈ Submonoid.closure (s ∪ s⁻¹)), p x ⋯
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
⊢ (List.map f s.toList).prod = (Multiset.map f s.val).prod

Tactic:
← Multiset.prod_coe,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
⊢ (↑(List.map f s.toList)).prod = (Multiset.map f s.val).prod
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (f a ::ₘ Multiset.map f s.val).noncommProd ⋯ = f a * (Multiset.map f s.val).noncommProd ⋯

Tactic:
Multiset.noncommProd_cons

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y✝ : β
h : ∀ x ∈ s, Commute y✝ (f x)
y : β
⊢ y ∈ Multiset.map f s.val → Commute y✝ y

Tactic:
Multiset.mem_map

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y✝ : β
h : ∀ x ∈ s, Commute y✝ (f x)
y : β
⊢ (∃ a ∈ s.val, f a = y) → Commute y✝ y