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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a

Tactic:
constructor
  · rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Set.mul_eq_one_iff.1 u.mul_inv
    refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩
    rw [← singleton_mul_singleton, ← ha, ← hb]
    exact u.inv_mul
  · rintro ⟨a, rfl, ha⟩
    exact ha.set

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

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

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

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

Goal state before:
pp: case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ ↑(closure s) ⊆ {1} ∪ ↑(Subsemigroup.closure s)

pp: case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ {1} ∪ ↑(Subsemigroup.closure s) ⊆ ↑(closure s)

Tactic:
· intro x hx
    induction hx using closure_induction with
    | mem x hx => exact Or.inr <| Subsemigroup.subset_closure hx
    | one => exact Or.inl <| by simp
    | mul x hx y hy hx hy =>
      push _ ∈ _ at hx hy
      obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
      all_goals simp_all [mul_mem]

Goal state after:
case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ {1} ∪ ↑(Subsemigroup.closure s) ⊆ ↑(closure s)
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : ↑p = ↑q
⊢ p = q

Tactic:
exact SetLike.ext'_iff.2 this

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ⊓ K = ⊥ ⊓ K ↔ H ⊓ K = ⊥

Tactic:
bot_inf_eq

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ⊓ K = ⊥ ↔ H ⊓ K = ⊥
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : map f H = map f K
⊢ H = K

Tactic:
apply_fun comap f at hf
  rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf

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

Goal state before:
pp: case mpr
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t → u ≤ s.prod t

Tactic:
· rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
    exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : α
⊢ (fun n ↦ (decode₂ α ↑n).get ⋯) ((fun a ↦ ⟨encode a, ⋯⟩) x✝) = x✝

Tactic:
by dsimp; rw [← Option.some_inj, Option.some_get, encodek₂]

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

Goal state before:
pp: case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hba : s i✝ b a
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩

Tactic:
exact congr_arg (Sigma.mk _ ·) <| antisymm hab hba

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

Goal state before:
pp: M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ l.length = l.length

Tactic:
· rfl

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type u_1
ι : Type u_2
s✝ t r : Set α
s : ι → Set α
h : Pairwise (Disjoint on s)
⊢ Injective fun x ↦ ↑x.snd

Tactic:
by
    rintro ⟨i, x, hx⟩ ⟨j, -, hx'⟩ rfl
    obtain rfl : i = j := h.eq (not_disjoint_iff.2 ⟨_, hx, hx'⟩)
    rfl

Goal state after:
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
⊢ ∃ n, ¬p n ∧ p (n + 1)

Tactic:
by
  classical
  let k := Nat.find H
  have hk : p k := Nat.find_spec H
  suffices 0 < k from
    ⟨k - 1, Nat.find_min H <| Nat.pred_lt this.ne', by rwa [Nat.sub_add_cancel this]⟩
  by_contra! contra
  rw [le_zero_eq] at contra
  exact H' (contra ▸ hk)

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

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

Tactic:
by_cases h : tl = []

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

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.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGreatest (lowerBounds ↑s) i
⊢ i = s.min' hs

Tactic:
IsGreatest,

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : i ∈ lowerBounds ↑s ∧ i ∈ upperBounds (lowerBounds ↑s)
⊢ i = s.min' hs
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
⊢ l'.revzip = List.map (fun x ↦ (x, ↑l - x)) l'

Tactic:
by
  have :
    Forall₂ (fun (p : Multiset α × Multiset α) (s : Multiset α) => p = (s, ↑l - s)) (revzip l')
      ((revzip l').map Prod.fst) := by
    rw [forall₂_map_right_iff, forall₂_same]
    rintro ⟨s, t⟩ h
    dsimp
    rw [← H h, add_tsub_cancel_left]
  rw [← forall₂_eq_eq_eq, forall₂_map_right_iff]
  simpa using this

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
f : List α → β
r : List β
⊢ sublistsLenAux 0 l f r = f [] :: r

Tactic:
by cases l <;> rfl

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ (map f (a :: l)).sublists = map (map f) (a :: l).sublists

Tactic:
by
    rw [map_cons, sublists_cons, bind_eq_flatMap, sublists_map f l, sublists_cons,
      bind_eq_flatMap, map_eq_flatMap, map_eq_flatMap]
    induction sublists l <;> simp [*]

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

Goal state before:
pp: α : Type u_1
a b : Finset α
r : ℕ
hab : #a = #b
hr₀ : r ≠ 0
hra : r ≤ #a
h : powersetCard r a = powersetCard r b
⊢ a = b

Tactic:
simpa [powersetCard_biUnion hr₀, ← hab, hra] using congr(($h).biUnion id)

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

Tactic:
rcases le_or_gt (sSup ∅) (iSup f) with le | gt

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
x : α i
h : a i ⩿ x
⊢ a i ⩿ Function.update a i x i ∧ ∀ (j : ι), j ≠ i → a j = Function.update a i x j

Tactic:
by simpa +contextual

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
p : (i : ι) × α i → Prop
inst✝ : DecidablePred p
⊢ filter p (s.sigma t) = s.sigma fun i ↦ {x ∈ t i | p ⟨i, x⟩}

Tactic:
ext ⟨i, a⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
p : (i : ι) × α i → Prop
inst✝ : DecidablePred p
i : ι
a : α i
⊢ ⟨i, a⟩ ∈ filter p (s.sigma t) ↔ ⟨i, a⟩ ∈ s.sigma fun i ↦ {x ∈ t i | p ⟨i, x⟩}
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
x : α i
h : a i ⋖ x
⊢ a i ⋖ Function.update a i x i ∧ ∀ (j : ι), j ≠ i → a j = Function.update a i x j

Tactic:
by simpa +contextual

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
x : α i
h : x ⩿ b i
⊢ Function.update b i x i ⩿ b i ∧ ∀ (j : ι), j ≠ i → Function.update b i x j = b j

Tactic:
by simpa +contextual

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
b : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
x : α i
h : x ⋖ b i
⊢ Function.update b i x i ⋖ b i ∧ ∀ (j : ι), j ≠ i → Function.update b i x j = b j

Tactic:
by simpa +contextual

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

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨i, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨i, b⟩.snd)

Tactic:
constructor
    · simp_rw [sigmaLift]
      simp only [dite_eq_ite, ite_true, mem_map, Embedding.sigmaMk_apply, forall_exists_index,
        and_imp]
      rintro x hx rfl
      exact ⟨rfl, rfl, hx⟩
    · rintro ⟨⟨⟩, ⟨⟩, hx⟩
      rw [sigmaLift, dif_pos rfl, mem_map]
      exact ⟨_, hx, by simp⟩

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:
rw [mem_sigmaLift]

Goal state after:
ι : 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
⊢ ¬∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
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 : b.fst ≠ x.fst
⊢ x ∉ sigmaLift f a b

Tactic:
rw [mem_sigmaLift]

Goal state after:
ι : 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 : b.fst ≠ x.fst
⊢ ¬∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ ⇑f '' s
⊢ x ∈ s ∧ x ∈ ⇑f ⁻¹' {y | Minimal (fun x ↦ x ∈ t) y} ↔ Minimal (fun x ↦ x ∈ s ∧ x ∈ ⇑f ⁻¹' t) x

Tactic:
preimage_ofPred_eq,

Goal state after:
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ ⇑f '' s
⊢ x ∈ s ∧ x ∈ {a | Minimal (fun x ↦ x ∈ t) (f a)} ↔ Minimal (fun x ↦ x ∈ s ∧ x ∈ ⇑f ⁻¹' t) x
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ioi a ↔ a < x

Tactic:
Ioi,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ (Finset.Ioi a).val ↔ a < x
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Finset.Iic b ↔ x ≤ b

Tactic:
Finset.mem_Iic

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ≤ b ↔ x ≤ b
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ b ≤ x
⊢ filter (fun x ↦ b ≤ x) (Ico a b) = ∅

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_right_le]

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ b ≤ x
⊢ ∅.val = ∅
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inl
s : Set ℕ
h : s = ∅
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

Tactic:
subst h

Goal state after:
case inl
⊢ sInf ∅ = 0 ↔ 0 ∈ ∅ ∨ ∅ = ∅
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inl
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s = ∅
⊢ m ∉ s

Tactic:
subst h

Goal state after:
case inl
m : ℕ
hm : m < sInf ∅
⊢ m ∉ ∅
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b : ℕ
⊢ max a b + 1 - min a b = (↑b - ↑a).natAbs + 1

Tactic:
rw [← Int.natCast_inj, Int.ofNat_sub] <;> omega

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

Goal state before:
pp: case succ.inl.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
ha : 0 < a
hkn : n + a ≠ n
hkl : (n + a) % a = (n + a) % a
hln : n + a ≠ n
⊢ n + a = n + a

pp: case succ.inl.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l

pp: case succ.inr.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = (n + a) % a
hln : n + a ≠ n
⊢ k = n + a

pp: case succ.inr.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k = l

Tactic:
· rfl

Goal state after:
case succ.inl.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l

case succ.inr.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = (n + a) % a
hln : n + a ≠ n
⊢ k = n + a

case succ.inr.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k = l
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
⊢ WellFounded fun x1 x2 ↦ x2 < x1

Tactic:
RelEmbedding.wellFounded_iff_isEmpty

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
⊢ IsEmpty ((fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x2 < x1)
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
⊢ ∃ a, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
choose next hnext using exists_covBy_of_wellFoundedLT (α := α)
  have hα := Set.nonempty_iff_univ_nonempty.mp ‹_›
  classical
  let a : ℕ → α := Nat.rec (wfl.wf.min _ hα) fun _n a ↦ if ha : IsMax a then a else next ha
  refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ (Set.mem_univ _), ?_⟩
  have cov n (hn : ¬ IsMax (a n)) : a n ⋖ a (n + 1) := by
    change a n ⋖ if ha : IsMax (a n) then a n else _
    rw [dif_neg hn]
    exact hnext hn
  have H : ∃ n, IsMax (a n) := by
    by_contra!
    exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf
  exact ⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ (wellFounded_lt.not_lt_min _ · h)⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
by
  obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq r f
  · refine ⟨g, fun m n hle => ?_⟩
    obtain hlt | rfl := hle.lt_or_eq
    exacts [h1 m n hlt, refl_of r _]
  · obtain ⟨m, n, hlt, hle⟩ := h (f ∘ g)
    cases h2 m n hlt hle

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Preorder α
inst✝ : WellQuasiOrderedLE α
⊢ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
RelEmbedding.wellFounded_iff_isEmpty

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Preorder α
inst✝ : WellQuasiOrderedLE α
⊢ IsEmpty ((fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x1 < x2)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Preorder α
inst✝ : WellQuasiOrderedLE α
f : (fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x1 < x2
⊢ False

Tactic:
obtain ⟨a, b, h, hf⟩ := wellQuasiOrdered_le f

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Preorder α
inst✝ : WellQuasiOrderedLE α
f : (fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x1 < x2
a b : ℕ
h : a < b
hf : f a ≤ f b
⊢ False
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h : a ≤ b
⊢ Iio a ⊆ Iio b

Tactic:
by
  simpa [← coe_subset] using Set.Iio_subset_Iio h

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 α
a₁ a₂ : α
⊢ a₁ ∈ orbit G a₂ ↔ a₂ ∈ orbit G a₁

Tactic:
← orbit_eq_iff,

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a₁ a₂ : α
⊢ orbit G a₁ = orbit G a₂ ↔ orbit G a₂ = orbit G a₁
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:
subst h

Goal state after:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
b : ↑(orbit G x)
g : ↥H
⊢ ↑g • b ∈ orbit (↥H) b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a

Tactic:
exact Set.uIcc_eq_union

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:
subst h

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 α
b : ↑x.orbit
g : ↥H
⊢ ↑g • b ∈ MulAction.orbit (↥H) b
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.inl
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
x : α
hx hy : x ∈ l
⊢ x * x = x * x

pp: case h.inr
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
x : α
hx : x ∈ l
y : α
hy : y ∈ l
hxy : x ≠ y
⊢ x * y = y * x

Tactic:
· rfl

Goal state after:
case h.inr
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
x : α
hx : x ∈ l
y : α
hy : y ∈ l
hxy : x ≠ y
⊢ x * y = y * x
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case inl
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
hb : a ∈ s.erase a
⊢ Commute a a

pp: case inr
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
b : α
hb : b ∈ s.erase a
hab : a ≠ b
⊢ Commute a b

Tactic:
· rfl

Goal state after:
case inr
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
b : α
hb : b ∈ s.erase a
hab : a ≠ b
⊢ Commute a b
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 = ∏ i ∈ s, ∏ x ∈ t i, f x

Tactic:
by
  refine Eq.trans ?_ (fold_disjiUnion h)
  dsimp [Finset.prod, Multiset.prod, Multiset.fold, Finset.disjUnion, Finset.fold]
  congr
  exact prod_const_one.symm

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
H : Step L₁ L₂
⊢ L₂ <+ L₁

Tactic:
cases H; simp

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

Goal state before:
pp: α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
L₁ L₂ : List (α × Bool)
H : Red.Step L₁ L₂
⊢ Red.Step (List.map (fun x ↦ (f x.1, x.2)) L₁) (List.map (fun x ↦ (f x.1, x.2)) L₂)

Tactic:
cases H; simp

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

Goal state before:
pp: α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) tl).sum = mk tl
b : Bool
⊢ of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) ((PUnit.unit, b) :: tl)).sum =
    mk ((PUnit.unit, b) :: tl)

Tactic:
cases b <;> simp [zpow_add, ih] <;> rfl

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ : Type u
x✝ x y : FreeGroup α✝
ihx : id <$> x = x
ihy : id <$> y = y
⊢ x * id <$> y = x * y

Tactic:
ihy

Goal state after:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ : Type u
x✝ x y : FreeGroup α✝
ihx : id <$> x = x
ihy : id <$> y = y
⊢ x * y = x * y
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ : Type u
x✝ x y : FreeGroup α✝
ihx : id <$> x = x
ihy : id <$> y = y
⊢ id <$> (x * y) = x * y

Tactic:
rw [map_mul, ihx, ihy]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
⊢ rightRel N = ⊤ ↔ N = ⊤

Tactic:
by
  simpa [rightRel, MulAction.orbitRel, funext_iff, MulAction.mem_orbit_iff,
    MulAction.subgroup_smul_def, ← eq_mul_inv_iff_mul_eq]
    using ⟨fun h ↦ by ext; simpa using h _ 1, fun h ↦ by simp [h]⟩

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure ↑(s i) = P i
⊢ (Submonoid.pi Set.univ P).FG

Tactic:
refine ⟨Finset.univ.biUnion fun i => (s i).image (MonoidHom.mulSingle M i), ?_⟩

Goal state after:
ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure ↑(s i) = P i
⊢ closure ↑(Finset.univ.biUnion fun i ↦ Finset.image (⇑(MonoidHom.mulSingle M i)) (s i)) = Submonoid.pi Set.univ P