mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case neg
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsStrictOrderedRing R
a : R
ha : -1 < a
h : a < 0
⊢ ↑⌈a⌉₊ < a + 1

Tactic:
rw [ceil_eq_zero.mpr h.le, cast_zero]

Goal state after:
case neg
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsStrictOrderedRing R
a : R
ha : -1 < a
h : a < 0
⊢ 0 < a + 1
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
l : List α
⊢ Quot.mk (⇑(isSetoid α)) l ≤ {a} ↔ Quot.mk (⇑(isSetoid α)) l = 0 ∨ Quot.mk (⇑(isSetoid α)) l = {a}

Tactic:
by simp only [← coe_singleton, quot_mk_to_coe'', coe_le,
    coe_eq_zero, coe_eq_coe, perm_singleton, subperm_singleton_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = n

Tactic:
convert! List.count_replicate_self (a := a)

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = List.count a (List.replicate n a)
Module: Mathlib.Data.Set.List

Goal state before:
pp: α : Type u_1
l : List α
d : α
⊢ (range fun n ↦ l[n]?.getD d) = (fun o ↦ o.getD d) '' range fun x ↦ l[x]?

Tactic:
simp only [← range_comp, Function.comp_def]
      rfl

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ (∃ bs₀_1 bs₁_1, Rel (flip r) bs₀ bs₀_1 ∧ Rel (flip r) bs₁ bs₁_1 ∧ as = bs₀_1 + bs₁_1) ↔
    ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

Tactic:
simp [rel_flip]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : ¬a ∈ l₁ ∪ l₂
⊢ a :: t ++ l₂ = a :: l₁ ∪ l₂

Tactic:
simp only [cons_append, cons_union, e, insert_of_not_mem h]

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

Goal state before:
pp: α : Type u_1
a : α
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p {a} = if p a then {a} else ∅

Tactic:
simp only [singleton, filter_cons, filter_zero, Multiset.add_zero, empty_eq_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t ⊆ 0 ↔ _root_.Disjoint s t

Tactic:
simp [subset_iff, disjoint_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ≤ t.ndinter u ↔ s ≤ t ∧ s ⊆ u

Tactic:
simp [ndinter, le_filter, subset_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.ndinter t ⊆ 0 ↔ _root_.Disjoint s t

Tactic:
simp [subset_iff, disjoint_left]

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

Goal state before:
pp: a b : ℕ
⊢ range (a + b) = range a ∪ map (fun x ↦ a + x) (range b)

Tactic:
rw [range_add, add_eq_union_iff_disjoint]
  apply range_disjoint_map_add

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

Goal state before:
pp: α : Type u_2
s : Finset α
a : α
h : Disjoint s {a}
⊢ s.disjUnion {a} h = cons a s ⋯

Tactic:
rw [disjUnion_comm, singleton_disjUnion]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
x : α
⊢ x ∈ s ∪ t ∪ u ↔ x ∈ s ∪ u ∪ t

Tactic:
by simp only [mem_union, or_assoc, @or_comm (x ∈ t)]

Goal state after:
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h : i ≠ last n
h' : i.rev ≠ 0
⊢ (i.castPred h).rev = i.rev.pred h'

Tactic:
← succ_inj,

Goal state after:
n : ℕ
i : Fin (n + 1)
h : i ≠ last n
h' : i.rev ≠ 0
⊢ (i.castPred h).rev.succ = (i.rev.pred h').succ
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun i ↦ f ↑i ⋯) (range n).attach
⊢ #s = n

Tactic:
calc
    #s = #((range n).attach.image fun i => f i.1 (mem_range.1 i.2)) := by rw [this]
    _ = #(range n).attach := ?_
    _ = #(range n) := card_attach
    _ = n := card_range n

Goal state after:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun i ↦ f ↑i ⋯) (range n).attach
⊢ #(image (fun i ↦ f ↑i ⋯) (range n).attach) = #(range n).attach
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case succ
n : ℕ
k : Fin (n + 1).succ
this : NeZero (n + 1).succ
hk : k ≠ 0
⊢ 1 ≤ ↑k

Tactic:
Nat.one_le_iff_ne_zero,

Goal state after:
case succ
n : ℕ
k : Fin (n + 1).succ
this : NeZero (n + 1).succ
hk : k ≠ 0
⊢ ↑k ≠ 0
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ s ⊆ t ∧ t ⊆ t ∧ #t = #t

Tactic:
simp [hst]

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

Goal state before:
pp: α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = #s

Tactic:
rw [← card_ofFinset s H]; congr!

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

Goal state before:
pp: α : Type u
s : Finset α
⊢ (↑s).toFinset = s

Tactic:
toFinset_coe

Goal state after:
α : Type u
s : Finset α
⊢ s = s
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑t

Tactic:
rw [← sep_eq_of_subset h]
  infer_instance

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inl
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
f : (j : Fin (n + 1)) → α j
j : Fin n
x : α (p.succAbove j)
⊢ p.removeNth (update f (p.succAbove j) x) j = update (p.removeNth f) j x j

Tactic:
simp [removeNth, *]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inr
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
i : Fin n
x : α (p.succAbove i)
f : (j : Fin (n + 1)) → α j
j : Fin n
hne : j ≠ i
⊢ p.removeNth (update f (p.succAbove i) x) j = update (p.removeNth f) i x j

Tactic:
simp [removeNth, *]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ k, k < n ∧ p k
⊢ Nat.find ⋯ = ↑(Fin.find (fun x ↦ p ↑x) ⋯)

Tactic:
by
  rw [val_find]
  have := h.choose_spec; exact Nat.find_congr (x := h.choose) (by grind) (by grind)

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Bool
h : (find? p).isSome = true
⊢ find? p = some (Fin.find (fun x ↦ p x = true) ⋯)

Tactic:
by
  simp_rw [find?_eq_dite, exists_eq_true_of_isSome_find? h, dite_true]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)

Tactic:
classical
    induction s using Finset.induction_on with
    | empty => simp
    | insert a s ha IH =>
      rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]
      simp

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
x : α
l : List α
h : IsChain R (x :: l)
y : α
hy : y ∈ l.head?
⊢ R x y

Tactic:
← cons_head?_tail hy

Goal state after:
α : Type u_1
R : α → α → Prop
x : α
l : List α
y : α
h : IsChain R (x :: y :: l.tail)
hy : y ∈ l.head?
⊢ R x y
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
l : List α
hl₁ : IsChain r (d :: l)
hl₂ : (d :: l).getLast ⋯ = b
⊢ ∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b

Tactic:
refine ⟨d :: l, .cons_cons e hl₁, ?_⟩

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
l : List α
hl₁ : IsChain r (d :: l)
hl₂ : (d :: l).getLast ⋯ = b
⊢ (c :: d :: l).getLast ⋯ = b
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate n = [] ↔ [] = l

Tactic:
rotate_eq_nil_iff,

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l = [] ↔ [] = l
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: l : List ℤ
h : l.prod = -1
x : ℤ
h₁ : x ∈ l
h₂ : x ≠ 1
⊢ -1 ∈ l

Tactic:
exact Or.resolve_left
    (Int.isUnit_iff.mp (prod_isUnit_iff.mp
      (h.symm ▸ ⟨⟨-1, -1, by decide, by decide⟩, rfl⟩ : IsUnit l.prod) x h₁)) h₂ ▸ h₁

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

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ (l.rotate n)[k] = l[(k + n) % l.length]

Tactic:
rw [← Option.some_inj, ← getElem?_eq_getElem, ← getElem?_eq_getElem, getElem?_rotate]
  exact h.trans_eq (length_rotate _ _)

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

Goal state before:
pp: α : Type u
l : List α
⊢ l ∈ l.cyclicPermutations

Tactic:
by
  simpa using head_mem (cyclicPermutations_ne_nil l)

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y) → (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y

pp: case mpr
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y → ∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y

Tactic:
· rintro ⟨i, hi, j, hj, hne, rfl, rfl⟩
    exact ⟨⟨i, hi, rfl⟩, ⟨j, hj, rfl⟩, mt h.getElem_inj_iff.1 hne⟩

Goal state after:
case mpr
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y → ∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ 0 → β a
this : f = Pi.empty β
⊢ ∀ (a : α) (h : a ∈ 0), Pi.empty β a h ∈ t a

Tactic:
intro _ h

Goal state after:
case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ 0 → β a
this : f = Pi.empty β
a✝ : α
h : a✝ ∈ 0
⊢ Pi.empty β a✝ h ∈ t a✝
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
⊢ f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t

Tactic:
by
  rw [sUnion_eq_biUnion, preimage_iUnion₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
C : Set (Set β)
⊢ s ×ˢ ⋃₀ C = ⋃₀ ((fun t ↦ s ×ˢ t) '' C)

Tactic:
by
  simp_rw [sUnion_eq_biUnion, biUnion_image, prod_iUnion₂]

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

Goal state before:
pp: case refine_2
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n →
    mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v

Tactic:
aesop (add simp [mulSingle_apply])

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
⊢ s ×ˢ ⋂ i, t i = ⋂ i, s ×ˢ t i

Tactic:
by
  ext x
  simp only [mem_prod, mem_iInter]
  exact ⟨fun h i => ⟨h.1, h.2 i⟩, fun h => ⟨(h hι.some).1, fun i => (h i).2⟩⟩

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

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x y : M
⊢ ∀ (x : M), f (x * 1) = f x * f 1

Tactic:
simp [h1]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 1

Tactic:
by
  rw [Subtype.nontrivial_iff_exists_ne (fun x => x ∈ H) (1 : H)]
  simp

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

Goal state before:
pp: 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
⊢ PLift ι

Tactic:
· exact PLift.up hι.some

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

Goal state before:
pp: n : ℕ
s : ℕ := n.sqrt
⊢ pair
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt)
        else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).2 =
    n

Tactic:
have sm : s * s + (n - s * s) = n := Nat.add_sub_cancel' (sqrt_le _)

Goal state after:
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
⊢ pair
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt)
        else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).2 =
    n
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ map ϕ.toMonoidHom H

Tactic:
by
  simp_rw [map_equiv_eq_comap_symm']
  exact characteristic_iff_le_comap.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mpr.of_mul
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
head : β
tail : FreeMonoid β
ih : ∃ a, (map f) a = tail
⊢ ∃ a, (map f) a = of head * tail

Tactic:
specialize fs head
    rcases fs with ⟨a, rfl⟩
    rcases ih with ⟨b, rfl⟩
    use FreeMonoid.of a * b
    rfl

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

Goal state before:
pp: case cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ l₁✝ l₂✝ : List M
a : M
a✝ : l₁✝ <+ l₂✝
ih' : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → l₁✝.prod ≤ l₂✝.prod
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂✝ → 1 ≤ x
⊢ l₁✝.prod ≤ a * l₂✝.prod

Tactic:
exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)

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

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

Tactic:
· rw [mul_assoc, mul_eq_one_iff_eq_inv] at this
      simpa

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

Goal state before:
pp: case inr
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ (subtypeOrLeftEmbedding p q)
      (Sum.elim (⇑(Subtype.impEmbedding p (fun x ↦ p x ∨ q x) ⋯)) (⇑(Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯))
        (Sum.inr x)) =
    Sum.inr x

Tactic:
simp only [Sum.elim_inr]
      rw [subtypeOrLeftEmbedding_apply_right]
      · grind
      · suffices ¬p x by simpa
        intro hp
        simpa using h.le_bot x ⟨hp, x.prop⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
motive : M → Prop
hs : closure s = ⊤
x : M
one : motive 1
mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
this : x ∈ closure s
⊢ motive x

Tactic:
induction this using closure_induction_left with
  | one => exact one
  | mul_left x hx y _ ih => exact mul_left x hx y ih

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
m k : ℕ
⊢ ↑(⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ ^ (↑m.succ).natMod ↑n) =
    ↑(⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ ^ (↑m).natMod ↑n * ⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩)

Tactic:
simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow, coe_mul]

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
m k : ℕ
⊢ x ^ (k * (↑m.succ % ↑n).toNat) = x ^ (k * (↑m % ↑n).toNat) * x ^ k
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
m k : ℕ
⊢ x ^ (k * ((-(↑(m + 1) * 1) + ↑(m + 1) * ↑n) % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))

Tactic:
← sub_eq_neg_add,

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
m k : ℕ
⊢ x ^ (k * ((↑(m + 1) * ↑n - ↑(m + 1) * 1) % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = mrange s.subtype ⊔ mrange t.subtype

Tactic:
mrange_subtype,

Goal state after:
N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = s ⊔ mrange t.subtype
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case coe
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
a : ℕ
hmax : t.maximum = ↑(ofNat s a)
wf : ↑(ofNat s a) < x
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
refine ⟨a + 1, le_antisymm (succ_le_of_lt wf) ?_⟩

Goal state after:
case coe
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
a : ℕ
hmax : t.maximum = ↑(ofNat s a)
wf : ↑(ofNat s a) < x
⊢ ⟨x, hx⟩ ≤ ofNat s (a + 1)
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
⊢ Denumerable α

Tactic:
letI := @decidableRangeEncode α _
  letI : Infinite (Set.range (@encode α _)) :=
    Infinite.of_injective _ (Equiv.ofInjective _ encode_injective).injective
  letI := Nat.Subtype.denumerable (Set.range (@encode α _))
  exact Denumerable.ofEquiv (Set.range (@encode α _)) (equivRangeEncode α)

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

Goal state before:
pp: case coe
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : l.maximum = ↑y
⊢ l.max?.getD d = WithBot.unbotD d ↑y

Tactic:
rw [List.maximum_eq_coe_iff] at hy
    simp only [WithBot.unbotD_coe]
    cases hz : l.max? with
    | none => simp [List.max?_eq_none_iff.mp hz] at hy
    | some z =>
      have : Std.Antisymm (α := α) (· ≤ ·) := ⟨fun _ _ => _root_.le_antisymm⟩
      rw [List.max?_eq_some_iff] at hz
      · rw [Option.getD_some]
        exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left)

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

Goal state before:
pp: case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f (max a b) = f a ⊔ f b

Tactic:
rw [sup_eq_right.2 h, sup_eq_right.2 (OrderHomClass.mono f h : f a ≤ f b)]

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

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

Tactic:
induction s using Finset.eraseInduction with

Goal state after:
case H
α : 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)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
⊢ motive s
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
s : Finset ι
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
⊢ motive s

Tactic:
induction s using Finset.eraseInduction with

Goal state after:
case H
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
⊢ motive s
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ (finRange l.length).sublists.Nodup

pp: α : Type u
l : List α
⊢ (finRange l.length).sublists'.Nodup

Tactic:
· exact nodup_sublists.mpr (nodup_finRange _)

Goal state after:
α : Type u
l : List α
⊢ (finRange l.length).sublists'.Nodup
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
⊢ (⋃ n, f n).Pairwise r ↔ ∀ (n : κ), (f n).Pairwise r

Tactic:
by
  constructor
  · intro H n
    exact Pairwise.mono (subset_iUnion _ _) H
  · intro H i hi j hj hij
    rcases mem_iUnion.1 hi with ⟨m, hm⟩
    rcases mem_iUnion.1 hj with ⟨n, hn⟩
    rcases hd m n with ⟨p, mp, np⟩
    exact H p (mp hm) (np hn) hij

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
⊢ IsLUB (f '' ↑s) (s.sup f)

Tactic:
by
  simp +contextual [IsLUB, IsLeast, upperBounds, lowerBounds, le_sup]

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

Goal state before:
pp: P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
⊢ P α

Tactic:
by
  obtain ⟨p⟩ :=
    let f_empty := fun i => by convert! h_empty
    let h_option : ∀ {α : Type u} [Fintype α] [DecidableEq α],
          (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α) := by
      rintro α hα - Pα hα'
      convert! h_option α (Pα _)
    @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _))
      f_empty h_option α _ (Classical.decEq α)
  exact p _

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⋖ b
⊢ ∅ ∪ {a} = {a}

Tactic:
empty_union

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⋖ b
⊢ {a} = {a}
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ ∅ ∪ Ici b = Ici b

Tactic:
empty_union

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Ici b = Ici b
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update a i (b i)
h₁ : c ≤ b
h₂ : ¬c j < b j
⊢ (fun x1 x2 ↦ x1 ≤ x2) (b j) (a j)

Tactic:
simpa [lt_iff_le_not_ge, hab j, c, hj] using h₂

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

Goal state before:
pp: case inl.mp
ι : 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⟩ → ∃ (h : i = x.fst) (h_1 : i = x.fst), x.snd ∈ f (⋯ ▸ a) (⋯ ▸ b)

Tactic:
sigmaLift

Goal state after:
case inl.mp
ι : 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 ∈ if h : True then map (Embedding.sigmaMk i) (f a b) else ∅) →
    ∃ (h : i = x.fst) (h_1 : i = x.fst), x.snd ∈ f (⋯ ▸ a) (⋯ ▸ b)