mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ x ∈+ l ↔ [x, x] <+ l

Tactic:
induction l with
  | nil => simp
  | cons y l IH =>
    by_cases hx : x = y
    · simp [hx, cons_sublist_cons, singleton_sublist]
    · rw [duplicate_cons_iff_of_ne hx, IH]
      refine ⟨sublist_cons_of_sublist y, fun h => ?_⟩
      cases h
      · assumption
      · contradiction

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
⊢ m = n

Tactic:
let := Classical.decEq α

Goal state after:
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
⊢ m = n
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
val✝ : Fintype ↑s
⊢ Finite ↑(s ∪ t)

Tactic:
cases nonempty_fintype t

Goal state after:
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
val✝¹ : Fintype ↑s
val✝ : Fintype ↑t
⊢ Finite ↑(s ∪ t)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : x ∉ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x ↦ c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
⊢ op c (if s = ∅ then b else op b c) = op b c

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : x ∉ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x ↦ c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : s = ∅
⊢ op c b = op b c

case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : x ∉ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x ↦ c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : ¬s = ∅
⊢ op c (op b c) = op b c
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ Fin.find p h = if h0 : p 0 then 0 else (Fin.find (fun k ↦ p k.succ) ⋯).succ

Tactic:
split_ifs

Goal state after:
case pos
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h✝ : p 0
⊢ Fin.find p h = 0

case neg
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h✝ : ¬p 0
⊢ Fin.find p h = (Fin.find (fun k ↦ p k.succ) ⋯).succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Bool
⊢ find? p = if h : ∃ i, p i = true then some (Fin.find (fun x ↦ p x = true) h) else none

Tactic:
split_ifs

Goal state after:
case pos
n : ℕ
p : Fin n → Bool
h✝ : ∃ i, p i = true
⊢ find? p = some (Fin.find (fun x ↦ p x = true) h✝)

case neg
n : ℕ
p : Fin n → Bool
h✝ : ¬∃ i, p i = true
⊢ find? p = none
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
m : Multiset ι
⊢ 1 ^ m.card = 1

Tactic:
one_pow

Goal state after:
ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
m : Multiset ι
⊢ 1 = 1
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
n : ℕ
⊢ a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s

Tactic:
by
  refine ⟨fun ha ↦ ⟨?_, mem_of_mem_nsmul ha⟩, fun h ↦ ?_⟩
  · rintro rfl
    simp [zero_nsmul] at ha
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero h.1
  rw [succ_nsmul, mem_add]
  exact Or.inr h.2

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

Goal state before:
pp: case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse =
    (x :: l).reverse.rotate
      ((x :: l).reverse.length - ((x :: l).reverse.length - n % (x :: l).reverse.length) % (x :: l).reverse.length +
        ((x :: l).reverse.length - n % (x :: l).reverse.length))

Tactic:
· rw [Nat.mod_eq_of_lt, Nat.sub_add_cancel, rotate_length]
      · exact Nat.sub_le _ _
      · exact Nat.sub_lt (by simp) (by simp_all! [k])

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

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
a : α
ham : a ∈ m
⊢ (if p a then {a} else 0).bind f = if p a then f a else 0

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
a : α
ham : a ∈ m
h✝ : p a
⊢ {a}.bind f = f a

case neg
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
a : α
ham : a ∈ m
h✝ : ¬p a
⊢ bind 0 f = 0
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → Finset β
hf : (↑s).PairwiseDisjoint f
t : Finset β
⊢ Disjoint (s.disjiUnion f hf) t ↔ ∀ i ∈ s, Disjoint (f i) t

Tactic:
by
  induction s using Finset.cons_induction <;> simp_all

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
s : Multiset ι
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b s)) (s.bind t) = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) s)

Tactic:
by
  induction s using Multiset.induction_on with
  | empty => rw [zero_bind, map_zero, map_zero, fold_zero]
  | cons a ha ih => rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
⊢ l.offDiag.Nodup

Tactic:
let := Classical.decEq α

Goal state after:
α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
⊢ l.offDiag.Nodup
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
h : l.offDiag.Nodup
⊢ l.Nodup

Tactic:
let := Classical.decEq α

Goal state after:
α : Type u_1
l : List α
h : l.offDiag.Nodup
this : DecidableEq α := Classical.decEq α
⊢ l.Nodup
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ k * n ! + (1 + n) * n ! - k * n ! = (n + 1) * n !

Tactic:
Nat.add_sub_cancel_left,

Goal state after:
case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ (1 + n) * n ! = (n + 1) * n !
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ (a a' : α) (m : Multiset α) (b : Multiset ((a : α) → a ∈ m → β a)),
    ((t a).bind fun b_1 ↦ map (Pi.cons (a' ::ₘ m) a b_1) ((t a').bind fun b_2 ↦ map (Pi.cons m a' b_2) b)) ≍
      (t a').bind fun b_1 ↦ map (Pi.cons (a ::ₘ m) a' b_1) ((t a).bind fun b_2 ↦ map (Pi.cons m a b_2) b)

Tactic:
by
      intro a a' m n
      by_cases eq : a = a'
      · subst eq; rfl
      · simp only [map_bind, map_map, comp_apply, bind_bind (t a') (t a)]
        apply bind_hcongr
        · rw [cons_swap a a']
        intro b _
        apply bind_hcongr
        · rw [cons_swap a a']
        intro b' _
        apply map_hcongr
        · rw [cons_swap a a']
        intro f _
        exact Pi.cons_swap eq

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : CommMonoid α
⊢ Function.RightInverse (Quotient.lift id ⋯) ConjClasses.mk

Tactic:
rw [Function.RightInverse, Function.LeftInverse, forall_isConj]
    solve_by_elim

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
⊢ Commute (mulSingle i (x i)) (mulSingle j (x j))

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Goal state after:
case inl
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i : I
⊢ Commute (mulSingle i (x i)) (mulSingle i (x i))

case inr
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
hij : i ≠ j
⊢ Commute (mulSingle i (x i)) (mulSingle j (x j))
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ univ ^ (n + 2) = univ

Tactic:
rw [pow_succ, univ_pow n.succ_ne_zero, univ_mul_univ]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
⊢ x ∈ closure {x}

Tactic:
simpa [-subset_closure] using subset_closure (k := {x})

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

Goal state before:
pp: case hK
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
⊢ DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on fun i ↦ K i.down) {i | True}

Tactic:
simp only [ofPred_true]

Goal state after:
case hK
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
⊢ DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on fun i ↦ K i.down) univ
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : Set (Subgroup G)
Kne : K.Nonempty
hK : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) K
x : G
⊢ x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s

Tactic:
have : Nonempty K := Kne.to_subtype
  simp only [sSup_eq_iSup', mem_iSup_of_directed hK.directed_val, SetCoe.exists, exists_prop]

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

Goal state before:
pp: case refine_3
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ (x y : C),
    x ∈ closure (↑s ∪ ↑t) →
      y ∈ closure (↑s ∪ ↑t) →
        (∃ y ∈ s, ∃ z ∈ t, y * z = x) → (∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y) → ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = x * y

Tactic:
rintro _ _ _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩

Goal state after:
case refine_3
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 ∈ s, ∃ z ∈ t, y * z = y₁ * z₁ * (y₂ * z₂)
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 : Subgroup G
h : f.ker ≤ H
⊢ comap f (map f H) = H

Tactic:
rwa [comap_map_eq, sup_eq_left]

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

Goal state before:
pp: case mp.refine_3
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ (x y : G),
    x ∈ closure (↑s ∪ ↑t) →
      y ∈ closure (↑s ∪ ↑t) →
        (∃ y ∈ s, ∃ z ∈ t, y * z = x) → (∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y) → ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = x * y

Tactic:
rintro _ _ _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩

Goal state after:
case mp.refine_3
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
y₁ : G
hy₁ : y₁ ∈ s
z₁ : G
hz₁ : z₁ ∈ t
hx✝ : y₁ * z₁ ∈ closure (↑s ∪ ↑t)
y₂ : G
hy₂ : y₂ ∈ s
z₂ : G
hz₂ : z₂ ∈ t
hy✝ : y₂ * z₂ ∈ closure (↑s ∪ ↑t)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = y₁ * z₁ * (y₂ * z₂)
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ n % 2 = n.bodd.toNat

Tactic:
by
  cases n using bitCasesOn with
  | bit b n => cases b <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ decode₂ α n ≠ none ↔ n ∈ Set.range encode

Tactic:
simp_rw [Set.range, Set.mem_ofPred_eq, Ne, Option.eq_none_iff_forall_not_mem,
    Encodable.mem_decode₂, not_forall, not_not]

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

Goal state before:
pp: m n : ℕ
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + (max m n + 1))

Tactic:
split_ifs

Goal state after:
case pos
m n : ℕ
h✝ : m < n
⊢ n * n + m < max m n * max m n + (max m n + (max m n + 1))

case neg
m n : ℕ
h✝ : ¬m < n
⊢ m * m + (m + n) < max m n * max m n + (max m n + (max m n + 1))
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: m n : ℕ
⊢ m + n ≤ if m < n then n * n + m else m * m + (m + n)

Tactic:
split_ifs

Goal state after:
case pos
m n : ℕ
h✝ : m < n
⊢ m + n ≤ n * n + m

case neg
m n : ℕ
h✝ : ¬m < n
⊢ m + n ≤ m * m + (m + n)
Module: Mathlib.Algebra.Group.Subgroup.Basic

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

Tactic:
rw [normal_subgroupOf_iff_le_normalizer_inf]

Goal state after:
G : Type u_1
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ H ≤ normalizer ↑(N ⊓ H)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x✝ : M
hx : x✝ ∈ closure (⋃ i, ↑(S i))
x y : M
hx✝ : x ∈ closure (⋃ i, ↑(S i))
hy✝ : y ∈ closure (⋃ i, ↑(S i))
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x * y ∈ S i

Tactic:
obtain ⟨k, hik, hjk⟩ := hS i j

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x✝ : M
hx : x✝ ∈ closure (⋃ i, ↑(S i))
x y : M
hx✝ : x ∈ closure (⋃ i, ↑(S i))
hy✝ : y ∈ closure (⋃ i, ↑(S i))
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ ∃ i, x * y ∈ S i
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
⊢ 1 ^ ?n = 1

pp: case n
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
⊢ ℕ

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 = ?n

Tactic:
one_pow

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

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
⊢ ℕ

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 = ?m.52
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: 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 : M
h : x ∈ closure s
⊢ motive x h

Tactic:
simp_rw [closure_eq_mrange] at h
  obtain ⟨l, rfl⟩ := h
  induction l using FreeMonoid.inductionOn' with
  | one => exact one
  | of_mul x y ih =>
    simp only [map_mul, FreeMonoid.lift_eval_of]
    refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)
    simp only [closure_eq_mrange, mem_mrange, exists_apply_eq_apply]

Goal state after:
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
k : ℕ
⊢ 1 ^ k = 1

Tactic:
one_pow

Goal state after:
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
k : ℕ
⊢ 1 = 1
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
⊢ (some val✝ = none ↔ tl = [] ∧ o = none) →
    ((if r hd val✝ then some hd else some val✝) = none ↔ (tl = [] ∧ [hd] = []) ∧ o = none)

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
h✝ : r hd val✝
⊢ (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)

case neg
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
h✝ : ¬r hd val✝
⊢ (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
    (foldl (argAux r) o (tl ++ [hd]) = none ↔ tl ++ [hd] = [] ∧ o = none)

Tactic:
simp only [foldl_append, foldl_cons, argAux, foldl_nil, append_eq_nil_iff]
    cases foldl (argAux r) o tl
    · simp
    · simp only
      split_ifs <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a
⊢ (Option.casesOn (Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a) (some tl) fun c ↦
      if f c < f tl then some tl else some c) =
    Option.casesOn (Option.casesOn (argmax f hd) (some tl) fun c ↦ if f c < f tl then some tl else some c) (some a)
      fun c ↦ if f a < f c then some c else some a

Tactic:
rcases h : argmax f hd with - | m

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a
h : argmax f hd = none
⊢ (Option.casesOn (Option.casesOn none (some a) fun c ↦ if f a < f c then some c else some a) (some tl) fun c ↦
      if f c < f tl then some tl else some c) =
    Option.casesOn (Option.casesOn none (some tl) fun c ↦ if f c < f tl then some tl else some c) (some a) fun c ↦
      if f a < f c then some c else some a

case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ (Option.casesOn (Option.casesOn (some m) (some a) fun c ↦ if f a < f c then some c else some a) (some tl) fun c ↦
      if f c < f tl then some tl else some c) =
    Option.casesOn (Option.casesOn (some m) (some tl) fun c ↦ if f c < f tl then some tl else some c) (some a) fun c ↦
      if f a < f c then some c else some a
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a y : α
l : List α
IH : (∀ (x : α), x ∈ l → x ≤ a) → foldr max ⊥ l ≤ a
h : ∀ (x : α), x ∈ y :: l → x ≤ a
⊢ foldr max ⊥ (y :: l) ≤ a

Tactic:
simpa [h y mem_cons_self] using IH fun x hx => h x <| mem_cons_of_mem _ hx

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
H : s.Nonempty
⊢ s.min = ↑(s.min' H)

Tactic:
by simp only [Finset.min, min', id_eq, coe_inf', Function.comp_def]

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

Goal state before:
pp: α : Type u
β : Type u_1
l : List (α × β)
⊢ (map Prod.swap l).unzip = l.unzip.swap

Tactic:
by
  simp only [unzip_eq_map, map_map]
  rfl

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

Goal state before:

Tactic:
s.card = (s.image f).card := (card_image_of_injOn f_mono.injOn).symm
    _ ≤ (insert ⊤ (t.image (↑)) : Finset (WithTop α)).card :=
      card_mono <| image_subset_iff.2 fun x _ =>
          insert_subset_insert _ (image_subset_image <| filter_subset _ _)
            (min_mem_insert_top_image_coe _)
    _ ≤ t.card + 1 := (card_insert_le _ _).trans (Nat.add_le_add_right card_image_le _)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : s.Nonempty
x : β
hx : x ∈ s
hy : (image f s).max = ↑(f x)
⊢ ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

Tactic:
exact ⟨x, hx, fun x' hx' => le_max_of_eq (mem_image_of_mem f hx') hy⟩

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

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset α
⊢ IsLUB (↑s) (s.sup id)

Tactic:
by simpa using isLUB_sup (f := id)

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

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : (∀ b ∈ s✝, p (f b)) → p (s✝.sup f)
hs : ∀ b ∈ cons a✝ s✝ h✝, p (f b)
⊢ p ((cons a✝ s✝ h✝).sup f)

Tactic:
simp only [sup_cons, forall_mem_cons] at hs ⊢
    exact hp _ hs.1 _ (ih hs.2)

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

Goal state before:
pp: case singleton
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
⊢ ({a✝}.inf fun b ↦ f b \ a) = {a✝}.inf f \ a

Tactic:
rw [inf_singleton, inf_singleton]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
⊢ ↑(s.sup' H f) = s.sup (WithBot.some ∘ f)

Tactic:
by
  rw [sup', WithBot.coe_unbot]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
⊢ count b (s.sup f) = s.sup fun a ↦ count b (f a)

Tactic:
let := Classical.decEq α

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (s.sup f) = s.sup fun a ↦ count b (f a)
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
⊢ IsEmpty p

Tactic:
isEmpty_Prop

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
⊢ ¬p
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
⊢ ∃ a ∈ s, (if i ∈ s then f i else sSup ∅) ≤ f a

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
h✝ : i ∈ s
⊢ ∃ a ∈ s, f i ≤ f a

case neg
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
h✝ : i ∉ s
⊢ ∃ a ∈ s, sSup ∅ ≤ f a