mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f (f_inv (x * y)) * f (f_inv x * f_inv y)⁻¹ = 1

Tactic:
f.map_inv,

Goal state after:
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
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f (f_inv (x * y)) * (f (f_inv x * f_inv y))⁻¹ = 1
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f (f_inv (f x)) * f x⁻¹ = 1

Tactic:
f.map_inv,

Goal state after:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f (f_inv (f x)) * (f x)⁻¹ = 1
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type ?u.8
β : Type ?u.9
f : Option α ↪ β
⊢ ∀ (x : Option α), ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) f)) x = f x

Tactic:
rintro (_ | _)

Goal state after:
case none
α : Type ?u.8
β : Type ?u.9
f : Option α ↪ β
⊢ ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) f)) none = f none

case some
α : Type ?u.8
β : Type ?u.9
f : Option α ↪ β
val✝ : α
⊢ ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) f)) (some val✝) = f (some val✝)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case of_mul
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : ∀ (h : (FreeMonoid.lift Subtype.val) y ∈ closure s), motive ((FreeMonoid.lift Subtype.val) y) h
h : (FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y) ∈ closure s
⊢ motive ((FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y)) h

Tactic:
simp only [map_mul, FreeMonoid.lift_eval_of]

Goal state after:
case of_mul
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : ∀ (h : (FreeMonoid.lift Subtype.val) y ∈ closure s), motive ((FreeMonoid.lift Subtype.val) y) h
h : (FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y) ∈ closure s
⊢ motive (↑x * (FreeMonoid.lift Subtype.val) y) ⋯
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
l : List α
⊢ argmax f l = none ↔ l = []

Tactic:
by simp [argmax]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) tl.maximum

pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : ¬tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) tl.maximum

Tactic:
· simp [h]

Goal state after:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : ¬tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) tl.maximum
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✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
f : F
inst✝ : InfHomClass F α β
hf : Injective ⇑f
x y : α
h : f x ≤ f y
⊢ f x ⊓ f y = f x

Tactic:
inf_eq_left

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
f : F
inst✝ : InfHomClass F α β
hf : Injective ⇑f
x y : α
h : f x ≤ f y
⊢ f x ≤ f y
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✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ (⇑f ∘ ⇑g) (a ⊔ b) = (⇑f ∘ ⇑g) a ⊔ (⇑f ∘ ⇑g) b

Tactic:
by rw [comp_apply, map_sup, map_sup]; rfl

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetAux' l₁ ~ powersetAux' l₂

Tactic:
induction p with

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

Goal state before:
pp: case succ
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂

Tactic:
induction p with

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

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x ↦ x.sup f, ¬(fun x ↦ x.sup f) t < x
a : α
this : ¬¬f a ≤ (fun x ↦ x.sup f) t
⊢ f a ≤ t.sup f

Tactic:
not_not

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x ↦ x.sup f, ¬(fun x ↦ x.sup f) t < x
a : α
this : f a ≤ (fun x ↦ x.sup f) t
⊢ f a ≤ t.sup f
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq (Finset α)
s : Finset α
⊢ s.powerset = (range (#s + 1)).biUnion fun i ↦ powersetCard i s

Tactic:
by
  simpa only [disjiUnion_eq_biUnion] using powerset_card_disjiUnion s

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

Goal state before:
pp: α✝ : 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 α
this : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
h : P (ULift.{u, 0} (Fin (card α)))
e : α ≃ Fin (card α)
⊢ P α

Tactic:
exact of_equiv (Equiv.ulift.trans e.symm) h

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ Disjoint (s.sup f) a ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint (f i) a

Tactic:
by
  simp only [disjoint_iff, sup_inf_distrib_right, Finset.sup_eq_bot_iff]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
r : ℕ
hr : r ≠ 0
hrs : r ≤ #s
⊢ (powersetCard r s).biUnion id = s

Tactic:
by
  obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hr
  rw [← sup_eq_biUnion]
  exact powersetCard_sup _ _ hrs

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ g (s.sup' H f) = s.sup' H (g ∘ f)

Tactic:
refine H.cons_induction ?_ ?_

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ ∀ (a : β), g ({a}.sup' ⋯ f) = {a}.sup' ⋯ (g ∘ f)

case refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ ∀ (a : β) (s : Finset β) (h : a ∉ s) (hs : s.Nonempty),
    g (s.sup' hs f) = s.sup' hs (g ∘ f) → g ((cons a s h).sup' ⋯ f) = (cons a s h).sup' ⋯ (g ∘ f)
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

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

Tactic:
rw [iSup]

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
⊢ sSup (range fun h ↦ f h) = sSup ∅
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Finite ι
f : ι → Set α
inst✝ : ∀ (i : ι), Finite ↑(f i)
this✝ : Fintype (PLift ι)
this : (i : ι) → Fintype ↑(f i)
⊢ Finite ↑(⋃ i, f i)

Tactic:
apply (fintypeiUnion _).finite

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

Goal state before:
pp: G : Type u_1
inst✝¹ : CommMagma G
inst✝ : IsCancelMul G
g : G
⊢ mulLeftEmbedding g = mulRightEmbedding g

Tactic:
ext
  exact mul_comm _ _

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

Goal state before:
pp: case mp
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
x_in : x ∈ t
⊢ ∃ i, x ∈ s ↑i ∩ t

Tactic:
rcases mem_iUnion.mp (hI x_in) with ⟨i, _, ⟨hi, rfl⟩, H⟩

Goal state after:
case mp
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
x_in : x ∈ t
i : ι
hi : i ∈ I
H : x ∈ (fun h ↦ s i) hi
⊢ ∃ i, x ∈ s ↑i ∩ t
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ Iio ↑a ∩ Iio ⊤ = Iio ↑a

Tactic:
inter_eq_self_of_subset_left (Iio_subset_Iio le_top)

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ Iio ↑a = Iio ↑a
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : a ≤ b
⊢ (∃ x, a < x ∧ ¬¬x < b) ↔ ∃ c, a < c ∧ c < b

Tactic:
not_not

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

Goal state before:
pp: 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 ∅

Tactic:
by_cases hj : p j

Goal state after:
case pos
α : 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 : ι
hj : p j
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅

case neg
α : 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 : ι
hj : ¬p j
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2 : a ≤ c
h3 : c ≤ b
⊢ c = a ∨ c = b

Tactic:
rcases h2.eq_or_lt with (h2 | h2); · exact Or.inl h2.symm
  rcases h3.eq_or_lt with (h3 | h3); · exact Or.inr h3
  exact (h.2 h2 h3).elim

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
h : a < b
⊢ (∃ x, a < x ∧ ¬¬x < b) ↔ ∃ c, a < c ∧ c < b

Tactic:
not_not

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

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
h₂ : x.snd ∈ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

Tactic:
simp [*, ← imp_iff_or_not]

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

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
h₂ : x.snd ∉ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

Tactic:
simp [*, ← imp_iff_or_not]

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

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∉ s₁
h₂ : x.snd ∈ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

Tactic:
simp [*, ← imp_iff_or_not]

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

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∉ s₁
h₂ : x.snd ∉ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

Tactic:
simp [*, ← imp_iff_or_not]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (range fun x ↦ f ↑x)
hne : s.Nonempty
this : Nonempty ↑s
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)

Tactic:
exact gc.l_ciSup hf

Goal state after:
Module: Mathlib.Order.Cover

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

Tactic:
by
  simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_left, mk_lt_mk_iff_left]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : a.fst ≠ x.fst
⊢ x ∉ sigmaLift f a b

Tactic:
by
  rw [mem_sigmaLift]
  exact fun H => h H.fst

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

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

pp: case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ ∅ = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

Tactic:
· simp [h]

Goal state after:
case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ ∅ = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ ∅ = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

Tactic:
· simp [h]

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

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a : α
s : Finset α
ha : a ∈ s
⊢ ∃ b, a ≤ b ∧ Maximal (fun x ↦ x ∈ s) b

Tactic:
obtain ⟨b, hb, hab, hbmin⟩ : ∃ b ∈ s, a ≤ b ∧ _ := by
    simpa [Maximal, and_assoc] using {x ∈ s | a ≤ x}.exists_maximal ⟨a, mem_filter.2 ⟨ha, le_rfl⟩⟩

Goal state after:
α : Type u_2
inst✝ : Preorder α
a : α
s : Finset α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
hbmin : ∀ ⦃y : α⦄, y ∈ s → a ≤ y → b ≤ y → y ≤ b
⊢ ∃ b, a ≤ b ∧ Maximal (fun x ↦ x ∈ s) b
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n ↦ Nat.recOn n ⋯.choose fun x a ↦ ⋯.choose
⊢ ∀ (n : ℕ), f n ∈ s

Tactic:
rintro (_ | _)

Goal state after:
case zero
α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n ↦ Nat.recOn n ⋯.choose fun x a ↦ ⋯.choose
⊢ f 0 ∈ s

case succ
α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n ↦ Nat.recOn n ⋯.choose fun x a ↦ ⋯.choose
n✝ : ℕ
⊢ f (n✝ + 1) ∈ s
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t

Tactic:
obtain rfl | hn := s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_2
inst✝ : LinearOrder α
hs : ∅.Finite
hs' : IsCofinal ∅
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t

case inr
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ False

Tactic:
apply h'

Goal state after:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ sInf s = 0
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: b : ℕ
⊢ b + 1 - 0 = b + 1

Tactic:
Nat.sub_zero

Goal state after:
b : ℕ
⊢ b + 1 = b + 1
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: b : ℕ
⊢ b - 0 = b

Tactic:
Nat.sub_zero

Goal state after:
b : ℕ
⊢ b = b
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : ¬¬bad.Finite
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
not_not

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : s.PartiallyWellOrderedOn r
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
⊢ (f '' s).PartiallyWellOrderedOn r'

Tactic:
by
  rw [partiallyWellOrderedOn_iff_exists_lt] at *
  intro g' hg'
  choose g hgs heq using hg'
  obtain rfl : f ∘ g = g' := funext heq
  obtain ⟨m, n, hlt, hmn⟩ := hs g hgs
  exact ⟨m, n, hlt, hf _ (hgs m) _ (hgs n) hmn⟩

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

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
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
⊢ ∀ {x y z : α}, x ∈ orbit G y → y ∈ orbit G z → x ∈ orbit G z

Tactic:
by grind [orbit_eq_iff]

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

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

Tactic:
subgroup_smul_def,

Goal state after:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
g : ↥H
h : ↑g • ↑b = ↑a
⊢ a ∈ MulAction.orbit (↥H) b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
⊢ s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), ¬IsBadSeq r s f

Tactic:
by
  rw [partiallyWellOrderedOn_iff_exists_lt]
  exact forall_congr' fun f => by simp [IsBadSeq]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
x y : α
⊢ x ≤ y ↔ ReflTransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
rw [le_iff_transGen_wcovBy, wcovBy_eq_reflGen_covBy, transGen_reflGen]

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

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
⊢ ConjClasses.mk g ∈ (noncenter G)ᶜ

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

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
⊢ (ConjClasses.mk g).carrier.Subsingleton
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
N H : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ ↑(N ⊔ H) = ↑N * ↑H

Tactic:
← set_mul_normalizer_comm _ _ hLE,

Goal state after:
G : Type u_2
inst✝ : Group G
N H : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ ↑(N ⊔ H) = ↑H * ↑N
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_2
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 p ⟨g, hg, hp⟩
    exact ⟨⟨g, hP hg⟩, hg, Subtype.ext hp⟩

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s).Pairwise (Commute on f)
comm' : ∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → (Commute on f) x x_1
⊢ (s.erase a).noncommProd f comm' * f a = s.noncommProd f comm

Tactic:
by
  classical
  simpa only [← Multiset.map_erase_of_mem _ _ h] using!
    Multiset.noncommProd_erase_mul (s.1.map f) (Multiset.mem_map_of_mem f h) _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
⊢ Quotient.lift f H = g

Tactic:
ext ⟨x⟩

Goal state after:
case mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x✝ : Quotient r
x : α
⊢ Quotient.lift f H (Quot.mk (⇑r) x) = g (Quot.mk (⇑r) x)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x✝⁵ : List (α × Bool)
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = (x3, b3) :: (x4, b4) :: tl ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [] ++ x✝⁵ = (x3, b3) :: (x4, b4) :: tl ++ x✝⁴ ∨
    ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ((x3, b3) :: (x4, b4) :: tl ++ x✝⁴) L₅

Tactic:
injections; subst_vars; right; exact ⟨_, Red.Step.not, Red.Step.cons_not⟩

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

Goal state before:
pp: case tail.inl
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
this : L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)

Tactic:
rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩

Goal state after:
case tail.inl
α : Type u
L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
this : L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
w₁ w₂ : List (α × Bool)
hLL' : ReflTransGen Step (w₁ ++ w₂) (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
h₁ : Red w₁ L₁
h₂ : Red w₂ (s' ++ (a, b) :: (a, !b) :: e)
⊢ ∃ L₃ L₄, w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)