mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
a : α
b : β
⊢ (a, b) ∈ s ×ˢ t ↔ (a, b).1 ∈ s ∧ (a, b).2 ∈ t

Tactic:
simp [SProd.sprod, product, and_left_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ ∀ (a_1 a'_1 : α), a_1 ≍ a'_1 → cons (a' ::ₘ m) a b (cons m a' b' f) a_1 ≍ cons (a ::ₘ m) a' b' (cons m a b f) a'_1

Tactic:
simp only [heq_iff_eq]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ ∀ (a_1 a'_1 : α), a_1 = a'_1 → cons (a' ::ₘ m) a b (cons m a' b' f) a_1 ≍ cons (a ::ₘ m) a' b' (cons m a b f) a'_1
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})

Tactic:
by
  classical
  rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]
  · apply congr_arg
    grind
  · apply Finset.disjoint_filter_filter'
    exact (disjoint_compl_right.inf_left _).inf_right _

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

Goal state before:
pp: case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + n.choose k.succ * (n.succ - k.succ)

Tactic:
Nat.mul_sub_left_distrib,

Goal state after:
case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + (n.choose k.succ * n.succ - n.choose k.succ * k.succ)
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑(image2 f s t)

Tactic:
rw [← image_prod]
  infer_instance

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
α : Type u_3
inst✝⁵ : Monoid M✝
inst✝⁴ : MulAction M✝ α
R : Type u_4
S : Type u_5
M : Type u_6
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : Monoid S
inst✝ : SMul S M
f : R →* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
b : M
⊢ 1 • b = b

Tactic:
one_smul

Goal state after:
M✝ : Type u_1
N : Type u_2
α : Type u_3
inst✝⁵ : Monoid M✝
inst✝⁴ : MulAction M✝ α
R : Type u_4
S : Type u_5
M : Type u_6
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : Monoid S
inst✝ : SMul S M
f : R →* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
b : M
⊢ b = b
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: δ : Type u_4
α : Type u_9
β : Type u_10
γ : Type u_11
s : Set α
t : Set β
f : α → Set γ
g : β → Set δ
fst✝ : γ
snd✝ : δ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ fst✝ ∈ f a ∧ snd✝ ∈ g b) ↔ (∃ i ∈ s, fst✝ ∈ f i) ∧ ∃ i ∈ t, snd✝ ∈ g i

Tactic:
tauto

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

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x / y ∈ H

Tactic:
by
  rw [div_eq_mul_inv]; exact mul_mem hx (inv_mem hy)

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

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

Tactic:
tauto

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Nontrivial G
⊢ Nontrivial ↥⊤

Tactic:
rw [nontrivial_iff_ne_bot]
  exact top_ne_bot

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

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
y₁ : C
hy₁ : y₁ ∈ s
z₁ : C
hz₁ : z₁ ∈ t
hx✝ : y₁ * z₁ ∈ closure (↑s ∪ ↑t)
y₂ : C
hy₂ : y₂ ∈ s
z₂ : C
hz₂ : z₂ ∈ t
hy✝ : y₂ * z₂ ∈ closure (↑s ∪ ↑t)
⊢ y₁ * y₂ * (z₁ * z₂) = y₁ * z₁ * (y₂ * z₂)

Tactic:
simp [mul_assoc, mul_left_comm]

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

Goal state before:
pp: n : ℕ
⊢ (n + 2).bodd = (1 &&& n + 2 != 0)

Tactic:
by simpa using bodd_eq_one_and_ne_zero n

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

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
a : α
⊢ decode₂ α (encode a) = some a

Tactic:
by
  simp [decode₂_eq_some]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ decode n = (decode (unpair n).1).bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)

Tactic:
simp only [decode_ofEquiv, Equiv.symm_symm, decode_sigma_val]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β))
      ((decode (unpair n).1).bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    (decode (unpair n).1).bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer ↑H ↔ normalizer ↑H = H → H = ⊤

Tactic:
tauto

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

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_6
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M
he : IsIdempotentElem e
f : F
⊢ IsIdempotentElem (f e)

Tactic:
by
  rw [IsIdempotentElem, ← map_mul, he.eq]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y * x⁻¹ * y⁻¹ = 1
⊢ Commute x y

Tactic:
by
    change x * y = y * x
    · rw [mul_assoc, mul_eq_one_iff_eq_inv] at this
      simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ↔ x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)

Tactic:
tauto

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 β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
v : β
htv : x.2 < v
hvu : v < y.2
⊢ toLex x < toLex (x.1, v) ∧ toLex (x.1, v) < toLex y

Tactic:
simp [Prod.Lex.toLex_lt_toLex, h.1, htv, hvu]

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✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
v : β
htv : x.2 < v
hvu : v < y.2
⊢ toLex x < toLex (x.1, v) ∧ toLex (x.1, v) < toLex y

Tactic:
simp [Prod.Lex.toLex_lt_toLex, h.1, htv, hvu]

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

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
y : N
z : α
⊢ y • z = 1 • y • z

Tactic:
one_smul

Goal state after:
case refine_1
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
y : N
z : α
⊢ y • z = y • z
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
y : N
z : α
⊢ y • z = y • 1 • z

Tactic:
one_smul

Goal state after:
case refine_1
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
y : N
z : α
⊢ y • z = y • z
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: ⊢ AddSubmonoid.closure {1} = ⊤

Tactic:
by
  ext
  simp [AddSubmonoid.mem_closure_singleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
a : α
l : List α
⊢ argmax f (l ++ [a]) = Option.casesOn (argmax f l) (some a) fun c ↦ if f c < f a then some a else some c

Tactic:
rw [argmax, argmax]; simp [argAux]

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
n : α
harg : argmax f l = some n
this : idxOf m l = idxOf n l
⊢ m ∈ some n

Tactic:
rw [(idxOf_inj hml).1 this, Option.mem_def]

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

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
hx : x ∈ []
⊢ a ≤ foldr max ⊥ []

Tactic:
exact absurd hx not_mem_nil

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Max α
inst✝¹ : Max β
inst✝ : Max γ
g : SupHom β γ
f₁ f₂ : SupHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by rw [← SupHom.comp_apply, h, SupHom.comp_apply]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
g : LatticeHom β γ
f₁ f₂ : LatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)

Tactic:
LatticeHom.comp_apply

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
g : LatticeHom β γ
f₁ f₂ : LatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₂ a) = g (f₂ a)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case nil
α : Type u
l₁ l₂ : List α
h : (l₁, l₂) ∈ [].sublists.zip [].sublists.reverse
this : l₁ = [] ∧ l₂ = []
⊢ l₁ ++ l₂ ~ []

Tactic:
simp [this]

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

Goal state before:
pp: case append_singleton.inr
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ [a] ++ id l₂ ~ l' ++ [a]

Tactic:
append_assoc

Goal state after:
case append_singleton.inr
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ ([a] ++ id l₂) ~ l' ++ [a]
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
h : a ∈ none
⊢ a ∈ s

Tactic:
cases h

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:
← card_map Function.Embedding.some,

Goal state after:
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ #(map Embedding.some (eraseNone s)) = #(s.erase none)
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
⊢ (map f s).sup' hs g = s.sup' ⋯ (g ∘ ⇑f)

Tactic:
by
  rw [← WithBot.coe_eq_coe, coe_sup', sup_map, coe_sup']
  rfl

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ s.sup' H f ≤ a ↔ sSup (f '' ↑s) ≤ a

Tactic:
simp [csSup_le_iff (s.finite_toSet.image f).bddAbove (H.to_set.image f)]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
⊢ ⨆ i ∈ s, i = sSup s

Tactic:
rw [← csSup_image (Subtype.range_coe ▸ hs), Set.image_id']

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
⊢ sSup ∅ ≤ ⨆ i, ↑i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = sSup ∅

Tactic:
refine ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j ↦ ?_) ?_

Goal state after:
case inr.refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
j : ι
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅

case inr.refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
⊢ ∀ w < sSup ∅, ∃ i, w < ⨆ (h : p i), f ⟨i, h⟩
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ Ico a b = {a} ↔ a ⋖ b

Tactic:
simp [Ico_eq_singleton_iff]

Goal state after:
Module: Mathlib.Order.Cover

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

Tactic:
exact Or.inr ⟨mk_wcovBy_mk_iff_right.1 h, rfl⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
⊢ a ⋖ b ↔ ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j

Tactic:
simp [covBy_iff_antisymmRel]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ (s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty

Tactic:
by simp [Finset.Nonempty]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
inst✝ : LE α
x : α
hx : Q x
⊢ (P x ∧ ∀ (a : α), Q a → P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Finset.Ico a b = ∅ ↔ ¬a < b

Tactic:
Finset.Ico_eq_empty_iff

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ ¬a < b ↔ ¬a < b
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inl
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hIncreasing : ∀ (m n : ℕ), m < n → f (g m) < f (g n)
⊢ StrictMono (⇑f ∘ ⇑g) ∨ StrictAnti (⇑f ∘ ⇑g)

Tactic:
exact Or.inl hIncreasing

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : a₁ < a₂
⊢ Set.Ico a₂ b ⊆ Set.Ioo a₁ b

Tactic:
exact Set.Ico_subset_Ioo_left h

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

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ (Ioi a).Nonempty ↔ ¬IsMax a

Tactic:
by simp [Finset.Nonempty]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
f : (fun x1 x2 ↦ x1 > x2) ↪r r
hf : ∀ (n : ℕ), f n ∈ s ∪ t
⊢ False

Tactic:
rcases Nat.exists_subseq_of_forall_mem_union f hf with ⟨g, hg | hg⟩

Goal state after:
case inl
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
f : (fun x1 x2 ↦ x1 > x2) ↪r r
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), f (g n) ∈ s
⊢ False

case inr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
f : (fun x1 x2 ↦ x1 > x2) ↪r r
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), f (g n) ∈ t
⊢ False
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ (Iio a).Nonempty ↔ ¬IsMin a

Tactic:
by simp [Finset.Nonempty]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Ioi a) = Ioi ↑a

Tactic:
subtype_Ioi_eq

Goal state after:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioi ↑a)) = Ioi ↑a
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = g' n
⊢ ∃ m n, m < n ∧ r' (g' m) (g' n)

Tactic:
obtain rfl : f ∘ g = g' := funext heq

Goal state after:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a < c → b < c → c ∉ [[a, b]]

Tactic:
rw [mem_uIcc]
  exact Set.notMem_uIcc_of_gt

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ orbit ⟦a⟧
⊢ ↑b ∈ MulAction.orbit ↥H ↑a

Tactic:
by
    rw [orbitRel.Quotient.orbit_eq_orbit_out (⟦a⟧ : orbitRel.Quotient H x.orbit) Quotient.out_eq']
       at hb
    rw [orbitRel.Quotient.mem_subgroup_orbit_iff]
    convert! hb using 1
    rw [orbit_eq_iff, ← orbitRel_apply, ← Quotient.eq'', Quotient.out_eq', @Quotient.mk''_eq_mk]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
⊢ x < y ↔ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
by
  refine ⟨transGen_covBy_of_lt, fun h ↦ ?_⟩
  induction h with
  | single hx => exact hx.1
  | tail _ hb ih => exact ih.trans hb.1

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

Goal state before:
pp: G : Type u_1
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G β
α : Type u_4
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : SMulCommClass G α β
a : α
b : β
⊢ stabilizer G (a⁻¹ • a • b) = stabilizer G b

Tactic:
by
    rw [inv_smul_smul]

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

Goal state before:
pp: G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤

Tactic:
by
  rw [eq_top_iff']
  intro x
  rw [Subgroup.mem_center_iff]
  intro y
  exact mul_comm y x

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Sort u_5
H : ι → Subgroup G
g : G
hg : g ∈ ⨅ i, normalizer ↑(H i)
⊢ g ∈ normalizer ↑(⨆ i, H i)

Tactic:
mem_iInf,

Goal state after:
G : Type u_2
inst✝ : Group G
ι : Sort u_5
H : ι → Subgroup G
g : G
hg : ∀ (i : ι), g ∈ normalizer ↑(H i)
⊢ g ∈ normalizer ↑(⨆ i, H i)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Sort u_5
H : ι → Subgroup G
⊢ ⨅ i, normalizer ↑(H i) ≤ normalizer ↑(⨆ i, H i)

Tactic:
intro g hg
  simp_rw [mem_iInf, mem_normalizer_iff_map_conj_eq, map_iSup, hg] at hg ⊢

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

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ MulAut.conj h • P.subgroupOf H ≤ (MulAut.conj ↑h • P).subgroupOf H

Tactic:
rintro - ⟨g, hg, rfl⟩
    exact ⟨g, hg, rfl⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
m : Multiset M
comm : {x | x ∈ m}.Pairwise Commute
h : ∀ x ∈ m, x ∈ S
⊢ m.noncommProd comm ∈ S

Tactic:
induction m using Quotient.inductionOn with | h l => ?_

Goal state after:
case h
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
l : List M
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
h : ∀ x ∈ ⟦l⟧, x ∈ S
⊢ Multiset.noncommProd ⟦l⟧ comm ∈ S
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

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

Tactic:
exact ⟨0, ∅, by simp⟩

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

Goal state before:
pp: α : Type u_1
s : Setoid α
a b : α
⊢ Quotient.mk' a = Quotient.mk' b ↔ ⊤ → s a b

Tactic:
simp_rw [Prop.top_eq_true, true_implies, Quotient.eq']

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c d : Con M
⊢ ∀ {w x y z : M}, ⊤ w x → ⊤ y z → ⊤ (w * y) (x * z)

Tactic:
tauto

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s).PairwiseDisjoint t
⊢ ∏ x ∈ s.disjiUnion t h, f x =
    fold (fun x1 x2 ↦ x1 * x2) (fold (fun x1 x2 ↦ x1 * x2) 1 (fun i ↦ 1) s) (fun x ↦ f x) (s.disjiUnion t h)

Tactic:
dsimp [Finset.prod, Multiset.prod, Multiset.fold, Finset.disjUnion, Finset.fold]

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s).PairwiseDisjoint t
⊢ Multiset.foldr (fun x1 x2 ↦ x1 * x2) 1 (Multiset.map (fun x ↦ f x) (s.val.bind fun a ↦ (t a).val)) =
    Multiset.foldr (fun x1 x2 ↦ x1 * x2) (Multiset.foldr (fun x1 x2 ↦ x1 * x2) 1 (Multiset.map (fun i ↦ 1) s.val))
      (Multiset.map (fun x ↦ f x) (s.val.bind fun a ↦ (t a).val))
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι → κ
he : Set.InjOn e ↑s
hest : Set.MapsTo e ↑s ↑t
h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ Set.SurjOn e ↑s ↑(image e s)

Tactic:
by simp [Set.surjOn_image]

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ a b : List (α × Bool)
h : Red.Step a b
⊢ Red.Step (invRev a) (invRev b)

Tactic:
cases h

Goal state after:
case not
α : Type u
L L₁ L₂ L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Red.Step (invRev (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝)) (invRev (L₁✝ ++ L₂✝))