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

Goal state before:
pp: case mp.of_mul
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
⊢ ∃ a, f a = d

Tactic:
use head

Goal state after:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
⊢ f head = d
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x y : α × β
⊢ toLex y < toLex x ↔ y.1 < x.1 ∨ y.1 = x.1 ∧ y.2 < x.2

Tactic:
toLex_lt_toLex

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x y : α × β
⊢ y.1 < x.1 ∨ y.1 = x.1 ∧ y.2 < x.2 ↔ y.1 < x.1 ∨ y.1 = x.1 ∧ y.2 < x.2
Module: Mathlib.Data.Prod.Lex

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

Tactic:
toLex_lt_toLex

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)
Module: Mathlib.Algebra.Group.Submonoid.Membership

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

Tactic:
by
    obtain ⟨_, k, rfl⟩ := y
    simp only [coe_one, coe_mul, SubmonoidClass.coe_pow]
    rw [← pow_succ, Nat.sub_add_cancel hpos, ← pow_mul, mul_comm, pow_mul, hx, one_pow]

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

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
x y : A
⊢ y ∈ closure {x} ↔ ∃ n, n • x = y

Tactic:
by
  rw [closure_singleton_eq, AddMonoidHom.mem_mrange]; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ (s.disjSum t).Nodup

Tactic:
refine ((hs.map inl_injective).add_iff <| ht.map inr_injective).2 ?_
  rw [disjoint_map_map]
  exact fun _ _ _ _ ↦ inr_ne_inl.symm

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
h₂ : {x ∈ range ↑(succ (ofNat s n)) | x ∈ s} = insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s})
ih : #({y ∈ range ↑(ofNat s n) | y ∈ s}) = n
| #({y ∈ range ↑(ofNat s n) | y ∈ s}) + 1

Tactic:
← card_insert_of_notMem h₁,

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
h₂ : {x ∈ range ↑(succ (ofNat s n)) | x ∈ s} = insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s})
ih : #({y ∈ range ↑(ofNat s n) | y ∈ s}) = n
| #(insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s}))
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z
this : Std.Antisymm fun x1 x2 ↦ x1 ≤ x2
⊢ (some z).getD d = y

Tactic:
rw [Option.getD_some]

Goal state after:
case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z
this : Std.Antisymm fun x1 x2 ↦ x1 ≤ x2
⊢ z = y
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : Top α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ (⇑f ⊔ ⇑g) ⊤ = ⊤

Tactic:
Pi.sup_apply,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : Top α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ f ⊤ ⊔ g ⊤ = ⊤
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✝ : SemilatticeSup β
f g : SupHom α β
a b : α
⊢ (⇑f ⊔ ⇑g) (a ⊔ b) = (⇑f ⊔ ⇑g) a ⊔ (⇑f ⊔ ⇑g) b

Tactic:
Pi.sup_apply,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : Max α
inst✝ : SemilatticeSup β
f g : SupHom α β
a b : α
⊢ f (a ⊔ b) ⊔ g (a ⊔ b) = (⇑f ⊔ ⇑g) a ⊔ (⇑f ⊔ ⇑g) b
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: case H.inl
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
ih : ∀ s ∈ ∅, motive (∅.erase s)
⊢ motive ∅

Tactic:
exact empty

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

Goal state before:
pp: case append_singleton
α : Type u
l✝ : List α
a✝¹ : α
a✝ : map pure l✝ <+ l✝.sublists
⊢ map pure l✝ ++ [pure a✝¹] <+ l✝.sublists ++ map (fun x ↦ x ++ [a✝¹]) l✝.sublists

Tactic:
case append_singleton l a ih =>
    exact ((append_sublist_append_left _).2 <|
              singleton_sublist.2 <| mem_map.2 ⟨[], mem_sublists.2 (nil_sublist _), by rfl⟩).trans
          ((append_sublist_append_right _).2 ih)

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

Goal state before:
pp: α : Type u
n : ℕ
l : List α
h✝ : l.Nodup
a✝ b✝ : List α
h : Lex (Function.swap fun x1 x2 ↦ x1 ≠ x2) a✝ b✝
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) a✝ b✝

Tactic:
by convert! h using 3; simp [eq_comm]

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

Goal state before:
pp: case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
⊢ i ≠ j → r i j

Tactic:
hij

Goal state after:
case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
⊢ r i j
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
s : Finset α
⊢ s.sup id = sSup ↑s

Tactic:
by
  simp [sSup_eq_iSup, sup_eq_iSup]

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 α
this : card PEmpty.{?u.57 + 1} = card (ULift.{?u.61, 0} (Fin 0))
e : PEmpty.{?u.57 + 1} ≃ ULift.{?u.61, 0} (Fin 0)
⊢ Trunc (P (ULift.{u, 0} (Fin 0)))

Tactic:
apply Trunc.mk

Goal state after:
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 α
this : card PEmpty.{?u.57 + 1} = card (ULift.{?u.61, 0} (Fin 0))
e : PEmpty.{?u.57 + 1} ≃ ULift.{?u.61, 0} (Fin 0)
⊢ P (ULift.{u, 0} (Fin 0))
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 ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ↑(u ⟨i, hi⟩) ∈ s ↑⟨j, hj⟩

Tactic:
hij

Goal state after:
α : 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 ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ↑(u ⟨j, hj⟩) ∈ s ↑⟨j, hj⟩
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
| ∀ (i : β), ⨆ c, f (i, c) ≤ c

Tactic:
enter [b]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
b : β
| ⨆ c, f (b, c) ≤ c
Module: Mathlib.Order.Cover

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

Tactic:
mk_lt_mk_iff_right

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
⊢ a ⋖ b ↔ ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
by
  constructor
  · intro h
    obtain ⟨j, hj⟩ := (Pi.lt_def.1 h.1).2
    have : Nonempty ι := ⟨j⟩
    obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h.wcovBy
    obtain rfl : i = j := by_contra fun this ↦ (hi j (Ne.symm this)).2.not_gt hj
    exact ⟨i, covBy_iff_wcovBy_and_lt.2 ⟨h.wcovBy.eval i, hj⟩, hi⟩
  rintro ⟨i, hi, h⟩
  have : Nonempty ι := ⟨i⟩
  refine covBy_iff_wcovBy_and_lt.2 ⟨wcovBy_iff_antisymmRel.2 ⟨i, hi.wcovBy, h⟩, ?_⟩
  exact Pi.lt_def.2 ⟨fun j ↦ (eq_or_ne j i).elim (· ▸ hi.1.le) (h j · |>.1), i, hi.1⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
⊢ i ≠ j → (Disjoint on fun i ↦ map (Embedding.sigmaMk i) (t i)) i j

Tactic:
hij

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ (Disjoint on fun i ↦ map (Embedding.sigmaMk i) (t i)) i j
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
⊢ f '' {x | Minimal P x} = {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}

Tactic:
by
  refine Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩
  · rintro ⟨x, (hx : Minimal _ x), rfl⟩
    exact (minimal_mem_image_monotone_iff hx.prop hf).2 hx
  obtain ⟨y, hy, rfl⟩ := (mem_ofPred_eq ▸ h).prop
  exact mem_image_of_mem _ <| (minimal_mem_image_monotone_iff (s := Set.ofPred P) hy hf).1 h

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x ↦ x ∈ t ∩ range ⇑f) (f x)
y : α
hy : (fun x ↦ f x ∈ t) y
⊢ f y ≤ f x → x ≤ y

Tactic:
← f.le_iff_le

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x ↦ x ∈ t ∩ range ⇑f) (f x)
y : α
hy : (fun x ↦ f x ∈ t) y
⊢ f y ≤ f x → f x ≤ f y
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: s : Set ℕ
inst✝ : Infinite ↑s
dP : DecidablePred fun x ↦ x ∈ s
n : ℕ
⊢ (orderIsoOfNat s) n = ofNat s n

Tactic:
by
  simp only [orderIsoOfNat, RelIso.ofSurjective_apply,
    RelEmbedding.orderEmbeddingOfLTEmbedding_apply, RelEmbedding.coe_natLT]
  congr!

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

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

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

Tactic:
· exfalso
    apply RelEmbedding.not_wellFounded _ hwf.wf
    exact (RelEmbedding.ofMonotone _ h1).swap

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
⊢ ∃ m n, m < n ∧ (fun x1 x2 ↦ x1 ≤ x2) (f m) (f n)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mpr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
⊢ (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))) → s.PartiallyWellOrderedOn r

Tactic:
PartiallyWellOrderedOn,

Goal state after:
case mpr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
⊢ (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))) →
    WellQuasiOrdered (Subrel r fun x ↦ x ∈ s)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
h : s.IsPWO
a : α
ha : a ∈ s
⊢ ∃ a, Minimal (fun x ↦ x ∈ s) a

Tactic:
obtain ⟨b, _, hb⟩ := h.exists_le_minimal ha

Goal state after:
α : Type u_2
inst✝ : Preorder α
s : Set α
h : s.IsPWO
a : α
ha : a ∈ s
b : α
left✝ : b ≤ a
hb : Minimal (fun x ↦ x ∈ s) b
⊢ ∃ a, Minimal (fun x ↦ x ∈ s) a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

Tactic:
by_cases hxy' : y ≤ x

Goal state after:
case pos
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : y ≤ x
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
hhc : ∀ (n : ℕ), (ofLex f (g 0)).1 = (ofLex f (g n)).1
hβ : ∀ (a : α) (f : ℕ → β), (∀ (n : ℕ), f n ∈ {y | toLex (a, y) ∈ s}) → ∃ g, Monotone (f ∘ ⇑g)
⊢ ∃ g', Monotone fun n ↦ (ofLex f (g (g' n))).2

Tactic:
apply hβ (ofLex f (g 0)).1 fun n ↦ (ofLex f (g n)).2

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
hhc : ∀ (n : ℕ), (ofLex f (g 0)).1 = (ofLex f (g n)).1
hβ : ∀ (a : α) (f : ℕ → β), (∀ (n : ℕ), f n ∈ {y | toLex (a, y) ∈ s}) → ∃ g, Monotone (f ∘ ⇑g)
⊢ ∀ (n : ℕ), (ofLex f (g n)).2 ∈ {y | toLex ((ofLex f (g 0)).1, y) ∈ s}
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c ↦ (f c, g c)) c c'
h' :
  ((fun c ↦ (f c, g c)) c).1 = ((fun c ↦ (f c, g c)) c').1 ∧ rβ ((fun c ↦ (f c, g c)) c).2 ((fun c ↦ (f c, g c)) c').2
⊢ ((PSigma.Lex (Subrel rα fun x ↦ x ∈ range f) fun a ↦ Subrel (rβ on g) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'

Tactic:
· dsimp only [InvImage, (· on ·)] at h' ⊢
    convert! PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1; swap
    exacts [⟨c, h'.1⟩, PSigma.subtype_ext (Subtype.ext h'.1) rfl, h'.2]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ = closure s

Tactic:
simp only [← toSubmonoid_inj, closure_toSubmonoid, inv_inv, union_comm]

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

Goal state before:
pp: case mul
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x x'✝ x' : G
hx✝ : x'✝ ∈ closure (↑H * ↑N)
hy✝ : x' ∈ closure (↑H * ↑N)
hx : x'✝ ∈ ↑H * ↑N
hx' : x' ∈ ↑H * ↑N
⊢ x'✝ * x' ∈ ↑H * ↑N

Tactic:
| mul x' x' _ _ hx hx' =>

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
h : a ∉ s
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1

Tactic:
· replace h₀ : ∀ b ∈ s, f b = 1 := by grind
    simp +contextual [h₀]

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

Goal state before:
pp: α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f (of x)⁻¹ * f (of x) * g (of x)⁻¹ = g (of x)⁻¹

Tactic:
· simp_rw [← _root_.map_mul, inv_mul_cancel, _root_.map_one, one_mul]

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

Goal state before:
pp: α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x : FreeGroup α
this : ∀ (x : α), f (of x)⁻¹ = g (of x)⁻¹
⊢ f x = g x

Tactic:
induction x <;> simp [*]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Function.Surjective f
⊢ Function.Surjective ⇑(map f)

Tactic:
by
  rw [← MonoidHom.range_eq_top, range_map, hf.range_eq, Set.image_univ, closure_range_of]

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

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)

Tactic:
by_cases has : a ∈ s.toFinset

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)

case neg
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
N : Submonoid M
| N.FG

Tactic:
rw [← N.mrange_subtype, MonoidHom.mrange_eq_map]

Goal state after:
M : Type u_1
inst✝ : Monoid M
N : Submonoid M
| (Submonoid.map N.subtype ⊤).FG
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
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ ↑s
j : κ
hj : j ∈ ↑s
⊢ i ≠ j → (_root_.Disjoint on t') i j

Tactic:
hij

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ ↑s
j : κ
hj : j ∈ ↑s
hij : i ≠ j
⊢ (_root_.Disjoint on t') i j
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
x : ι
hx : x ∈ s.toFinset
⊢ (k * (count x s / k)) • {x} = count x s • {x}

Tactic:
Nat.mul_div_cancel' (h x (mem_toFinset.mp hx))

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
x : ι
hx : x ∈ s.toFinset
⊢ count x s • {x} = count x s • {x}
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Mul α
x y z : FreeAbelianGroup α
⊢ (x + y) * z = x * z + y * z

Tactic:
simp [mul_def, ← Pi.add_def]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
hg : IsConj g (g ^ 2)
⊢ g ∈ commutatorSet G

Tactic:
obtain ⟨h, hg⟩ := hg

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ∈ commutatorSet G
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case hx
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⊤ = f.range

Tactic:
· rw [Subgroup.map_eq_range_iff]
    rw [codisjoint_iff, top_sup_eq]

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

Goal state before:
pp: case hy
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⊤ = f.range

Tactic:
· rw [Subgroup.map_eq_range_iff]
    rw [codisjoint_iff, top_sup_eq]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
⊢ ∀ {x y z : X × ↥S},
    (∃ u v, u • y.fst = v • x.fst ∧ ↑u * ↑y.snd = v * ↑x.snd) →
      (∃ u v, u • z.fst = v • y.fst ∧ ↑u * ↑z.snd = v * ↑y.snd) →
        ∃ u v, u • z.fst = v • x.fst ∧ ↑u * ↑z.snd = v * ↑x.snd

Tactic:
· rintro ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨r₃, s₃⟩ ⟨u, v, hur₁, hs₁u⟩ ⟨u', v', hur₂, hs₂u⟩
      rcases oreCondition v' u with ⟨r', s', h⟩; dsimp only at *
      refine ⟨s' * u', r' * v, ?_, ?_⟩ <;>
        simp only [Submonoid.smul_def, Submonoid.coe_mul, mul_smul, mul_assoc] at *
      · rw [hur₂, smul_smul, h, mul_smul, hur₁]
      · rw [hs₂u, ← mul_assoc, h, mul_assoc, hs₁u]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥S
h : ↑c * x = ↑c * y
⊢ f x = f y

Tactic:
by
    replace h := congr_arg f h
    rw [map_mul, map_mul] at h
    exact (f.map_units c).mul_right_inj.mp h

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
ha : ↑a₁ < ⊤
⊢ b₂ ≠ 0

Tactic:
simpa [bot_eq_zero] using hb.bot_lt.ne'

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
p : α → Prop
hsucc : ∀ (a : α), p a ↔ p (succ a)
a b : α
h : a ≤ b
⊢ p a ↔ p b

Tactic:
obtain ⟨n, rfl⟩ := h.exists_succ_iterate

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
p : α → Prop
hsucc : ∀ (a : α), p a ↔ p (succ a)
a : α
n : ℕ
h : a ≤ succ^[n] a
⊢ p a ↔ p (succ^[n] a)