mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin n
⊢ i ≠ 0 → ↑(i - 1) = ↑i - 1

Tactic:
by
  have := i.neZero
  intro hi
  obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne n)
  rw [Fin.sub_val_of_le (one_le_of_ne_zero hi), Fin.val_one', Nat.mod_eq_of_lt
    (Nat.succ_le_iff.mpr (nontrivial_iff_two_le.mp <| nontrivial_of_ne i 0 hi))]

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

Goal state before:
pp: m n : ℕ
a b : Fin n
h : b ≤ a
⊢ castAdd m a - castAdd m b = castAdd m (a - b)

Tactic:
grind [Fin.sub_val_of_le]

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

Goal state before:
pp: n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
hkb : k < ↑b
⊢ ⟨k, ⋯⟩ + 1 ≤ b

Tactic:
by fin_omega

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
⊢ Set.InjOn f ↑s

Tactic:
have : s.image f = t := Finset.coe_injective <| by simp [hsurj.image_eq_of_mapsTo hf]
  have : #(s.image f) = #t := by rw [this]
  have : #(s.image f) ≤ #s := card_image_le
  rw [← card_image_iff]
  lia

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Tactic:
by
  rcases castSucc_lt_or_lt_succ p i with H | H
  · rw [iff_false_right (Fin.not_le.2 H), succAbove_of_castSucc_lt _ _ H]
    exact Fin.not_lt.2 <| Fin.le_of_lt H
  · rwa [succAbove_of_lt_succ _ _ H, iff_true_left H, le_castSucc_iff]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ

Tactic:
by
  obtain h | h := i.lt_or_ge (succ j)
  · rw [succAbove_of_lt_succ _ _ h, succAbove_succ_of_lt _ _ h]
  · rwa [succAbove_of_castSucc_lt _ _ h, succAbove_succ_of_le, succ_castSucc]

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

Goal state before:
pp: case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
x✝ : α
⊢ x✝ ∈ {x | p x}.toFinset ↔ p x✝

Tactic:
simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_ofPred]

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

Goal state before:
pp: case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
x✝ : α
⊢ x✝ ∈ {x | p x}ᶜ.toFinset ↔ ¬p x✝

Tactic:
simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_ofPred]

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

Goal state before:
pp: α : Type u_4
inst✝ : Fintype α
e : α ↪ α
⊢ map e univ = univ

Tactic:
← e.toEmbedding_equivOfFiniteSelfEmbedding,

Goal state after:
α : Type u_4
inst✝ : Fintype α
e : α ↪ α
⊢ map e.equivOfFiniteSelfEmbedding.toEmbedding univ = univ
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ False

Tactic:
classical
      refine lt_irrefl (Fintype.card α) ?_
      calc
        Fintype.card α ≤ Fintype.card s := Fintype.card_le_of_injective f hf
        _ = #s.toFinset := s.toFinset_card.symm
        _ < Fintype.card α :=
          Finset.card_lt_card <| by rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]

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

Goal state before:
pp: α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ hs.toFinset ⊂ ht.toFinset ↔ s ⊂ t

Tactic:
simp only [← Finset.coe_ssubset, Finite.coe_toFinset]

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 : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁ ∪ s₂).val + Multiset.map f (s₁ ∩ s₂).val) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))

Tactic:
← Multiset.map_add,

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ Multiset.fold op (op b₁ b₂) (Multiset.map f ((s₁ ∪ s₂).val + (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case left
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin m
hi : castAdd n i < natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)
⊢ ¬p (castAdd n i)

Tactic:
| left i =>

Goal state after:
case left
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin m
hi : castAdd n i < natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)
⊢ ¬p (castAdd n i)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inr.inr.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j ≤ k.castSucc

Tactic:
· exact Fin.le_iff_val_le_val.2 (le_of_lt h)

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

Goal state before:
pp: M : Type u_8
inst✝ : CommMonoid M
L : List M
⊢ IsUnit L.prod ↔ ∀ (m : M), m ∈ L → IsUnit m

Tactic:
refine ⟨fun h => ?_, prod_isUnit⟩
  induction L with
  | nil => exact fun m' h' => False.elim (not_mem_nil h')
  | cons m L ih =>
    rw [prod_cons, IsUnit.mul_iff] at h
    exact fun m' h' ↦ Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H

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

Goal state before:
pp: case cons
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
⊢ (map (fun x ↦ count x (a :: as)) (filter p (a :: as).dedup)).sum = countP p (a :: as)

Tactic:
simp_rw [List.countP_cons, List.count_cons, List.sum_map_add]

Goal state after:
case cons
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum +
      (map (fun i ↦ if (a == i) = true then 1 else 0) (filter p (a :: as).dedup)).sum =
    countP p as + if p a = true then 1 else 0
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
hf : Function.Injective f
⊢ s.disjiUnion (fun a ↦ {f a}) ⋯ = map { toFun := f, inj' := hf } s

Tactic:
ext; simp [eq_comm]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case succ
n : ℕ
ih : n.choose 2 = n * (n - 1) / 2
⊢ (n + 1).choose 2 = (n + 1) * (n + 1 - 1) / 2

Tactic:
rw [triangle_succ n, choose, ih]

Goal state after:
case succ
n : ℕ
ih : n.choose 2 = n * (n - 1) / 2
⊢ n.choose 1 + n * (n - 1) / 2 = n * (n - 1) / 2 + n
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: i j : ℕ
⊢ i ! * j ! ∣ (i + j)!

Tactic:
by
  suffices i ! * (i + j - i)! ∣ (i + j)! by
    rwa [Nat.add_sub_cancel_left i j] at this
  exact factorial_mul_factorial_dvd_factorial (Nat.le_add_right _ _)

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ f' a' ⋯ ∈ t a'

Tactic:
apply hf'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ sᶜ ⊆ range f ↔ (range f)ᶜ ⊆ s

Tactic:
compl_subset_comm

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ (range f)ᶜ ⊆ s ↔ (range f)ᶜ ⊆ s
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 [sInter_eq_biInter, preimage_iInter₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ ⋂₀ {s} ×ˢ ⋂₀ T = ⋂ t ∈ T, ⋂₀ {s} ×ˢ t

Tactic:
sInter_prod_sInter (singleton_nonempty s) hT,

Goal state after:
α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ ⋂ r ∈ {s} ×ˢ T, r.1 ×ˢ r.2 = ⋂ t ∈ T, ⋂₀ {s} ×ˢ t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t

Tactic:
rw [← sInter_singleton s, sInter_prod_sInter (singleton_nonempty s) hT, sInter_singleton]
  simp_rw [singleton_prod, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = ⋃ i ∈ s, ⋃ j ∈ t, {f i j}

Tactic:
ext; simp [eq_comm]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Set M
motive : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : x ∈ closure s), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : x ∈ closure s), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y : M
hx : x ∈ closure s
hy : y ∈ closure s
⊢ motive x y hx hy

Tactic:
by
  induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem _ _ h hz
    | one => exact one_left _ (subset_closure hz)
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
  | one => exact one_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ hx h₁ h₂

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : g ∈ normalizer S
n : G
⊢ n * g ∈ S ↔ g * n ∈ S

Tactic:
rw [h, mul_assoc, mul_inv_cancel_right]

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
x y✝ : G
hy✝ : y✝ ∈ closure {x}
y : G
hy : y ∈ {x}
⊢ ∃ n, x ^ n = x

Tactic:
exact ⟨1, zpow_one x⟩

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
h : Disjoint H K
⊢ Disjoint (map f H) (map f K)

Tactic:
rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]

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

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

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

pp: case refine_4
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ closure (↑s ∪ ↑t), (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹

Tactic:
· exact ⟨1, s.one_mem, 1, ⟨t.one_mem, mul_one 1⟩⟩

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

case refine_4
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ closure (↑s ∪ ↑t), (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
by
  constructor
  · intro hx; rw [sup_eq_closure] at hx
    refine closure_induction ?_ ?_ ?_ ?_ hx
    · rintro x (hx | hx)
      · exact ⟨x, hx, 1, t.one_mem, by simp⟩
      · exact ⟨1, s.one_mem, x, hx, by simp⟩
    · exact ⟨1, s.one_mem, 1, t.one_mem, by simp⟩
    · rintro _ _ _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
      exact ⟨y₁ * y₂, s.mul_mem hy₁ hy₂,
            (y₂⁻¹ * z₁ * y₂) * z₂, t.mul_mem (ht.conj_mem' z₁ hz₁ y₂) hz₂, by simp [mul_assoc]⟩
    · rintro _ _ ⟨y, hy, z, hz, rfl⟩
      exact ⟨y⁻¹, s.inv_mem hy,
            y * z⁻¹ * y⁻¹, ht.conj_mem z⁻¹ (t.inv_mem hz) y, by simp [mul_assoc]⟩
  · rintro ⟨y, hy, z, hz, rfl⟩; exact mul_mem_sup hy hz

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective ⇑f
H K : Submonoid M
h : Disjoint H K
⊢ Disjoint (map f H) (map f K)

Tactic:
rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]

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

Goal state before:
pp: case succ
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (m * (n + 1)).bodd = (m.bodd && (n + 1).bodd)

Tactic:
simp only [mul_succ, bodd_add, IH, bodd_succ]

Goal state after:
case succ
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (m.bodd && n.bodd ^^ m.bodd) = (m.bodd && !n.bodd)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg.h₁
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ < a₂ * a₂

pp: case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ + b < a₂ + b

Tactic:
· exact Nat.mul_self_lt_mul_self h

Goal state after:
case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ + b < a₂ + b
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
α₁ : Type u_6
g : α₁ → α
x : FreeMonoid α₁
⊢ (map f) ((map g) x) = (map (f ∘ g)) x

Tactic:
by
  unfold map
  simp only [MonoidHom.coe_mk, OneHom.coe_mk, toList_ofList, List.map_map]

Goal state after:
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 ⊔ N)).Normal

Tactic:
by
  rw [normal_subgroupOf_iff_le_normalizer le_sup_right]
  exact sup_le hLE le_normalizer

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 : ℕ
x : ↥(powers x✝)
⊢ ↑(x ^ ↑m.succ) = ↑(x ^ ↑m * x)

Tactic:
simp_rw [HPow.hPow, Pow.pow]
    obtain ⟨_, k, rfl⟩ := x
    simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow, coe_mul]
    norm_cast
    iterate 2 rw [Int.toNat_natCast, mul_comm, pow_mul, ← pow_eq_pow_mod _ hx]
    rw [← pow_mul _ m, mul_comm, pow_mul, ← pow_succ, ← pow_mul, mul_comm, pow_mul]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
n : ℕ
⊢ encode (ofNat α n) = n

Tactic:
obtain ⟨a, h, e⟩ := decode_inv (α := α) n

Goal state after:
α : Type u_1
inst✝ : Denumerable α
n : ℕ
a : α
h : a ∈ decode n
e : encode a = n
⊢ encode (ofNat α n) = n
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
val✝ : α
h : argmax f tl = some val✝
h✝ : ¬f hd < f val✝
ham : f hd ≤ f hd
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ (if hd = val✝ then 0 else idxOf val✝ tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
· rw [if_pos rfl]

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ (if hd = val✝ then 0 else idxOf val✝ tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: case inr
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 : b ≤ a
⊢ f (min a b) = f a ⊓ f b

Tactic:
inf_eq_right.2 h,

Goal state after:
case inr
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 : b ≤ a
⊢ f b = f a ⊓ f b
Module: Mathlib.Data.Finset.Max

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

Tactic:
simp only [max', Finset.max, id_eq, coe_sup', Function.comp_def]

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

Goal state before:
pp: α : Type u
l : List α
⊢ map Prod.fst l.revzip = l

Tactic:
← unzip_fst,

Goal state after:
α : Type u
l : List α
⊢ l.revzip.unzip.fst = l
Module: Mathlib.Data.Multiset.Powerset

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

Tactic:
by
  rw [powersetAux_eq_map_coe]; exact (sublists_perm_sublists' _).map _

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux (n + 1) (a :: l) (g ∘ f) (map g r ++ s) = map g (sublistsLenAux (n + 1) (a :: l) f r) ++ s

Tactic:
by
    unfold sublistsLenAux
    simp only [show (g ∘ f) ∘ List.cons a = g ∘ f ∘ List.cons a by rfl,
      sublistsLenAux_append]

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

Goal state before:
pp: α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.zip l.sublists.reverse
⊢ l₁ ++ l₂ ~ l

Tactic:
induction l using List.reverseRecOn generalizing l₁ l₂ with

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

Goal state before:
pp: case mk
α : Type u_1
t : Finset α
val✝ : Multiset α
nodup✝ : val✝.Nodup
⊢ { val := val✝, nodup := nodup✝ } ∈ t.powerset ↔ { val := val✝, nodup := nodup✝ } ⊆ t

Tactic:
simp [powerset, mem_mk, mem_pmap, mk.injEq, exists_prop, exists_eq_right,
    ← val_le_iff]

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
hs : s.Finite
F : (i : α) → i ∈ s → β
⊢ {y | ∃ x, ∃ (hx : x ∈ s), F x hx = y}.Finite

Tactic:
have := hs.to_subtype
  simpa [range] using finite_range fun x : s => F x x.2

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ (powersetCard n s).Nonempty ↔ n ≤ #s

Tactic:
aesop (add simp [Finset.Nonempty, exists_subset_card_eq, card_le_card])

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

Goal state before:
pp: case empty
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
⊢ ⊥ = a \ ⊤

Tactic:
sdiff_top

Goal state after:
case empty
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
⊢ ⊥ = ⊥
Module: Mathlib.Data.Fintype.Option

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

pp: case intro.refine_2
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ P PEmpty.{u + 1}

pp: case intro.refine_3
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ ∀ (α : Type u) [Fintype α], P α → P (Option α)

Tactic:
exacts [fun α β _ => of_equiv, h_empty, @h_option]

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

Goal state before:
pp: ι : Type u_5
α : Type u_7
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
cases subsingleton_or_nontrivial α
  · simpa [Subsingleton.elim _ (⊤ : α)]
  · exact Finset.sup_eq_top_iff

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Ico ↑a ↑b = Ico a b

Tactic:
simp [← Ici_inter_Iio]

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some ⁻¹' Ico ↑a ⊤ = Ici a

Tactic:
simp [← Ici_inter_Iio]

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Iic a = Iic ↑a

Tactic:
← preimage_coe_Iic,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' some ⁻¹' Iic ↑a = Iic ↑a
Module: Mathlib.Order.Cover

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
fst✝¹ : α
snd✝¹ : β
fst✝ : α
snd✝ : β
⊢ (fst✝¹, snd✝¹) ⩿ (fst✝, snd✝) ↔
    (fst✝¹, snd✝¹).1 ⩿ (fst✝, snd✝).1 ∧ (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2 ∨
      (fst✝¹, snd✝¹).2 ⩿ (fst✝, snd✝).2 ∧ (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1

Tactic:
exact mk_wcovBy_mk_iff

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Ioo a a = 0

Tactic:
by rw [Ioo, Finset.Ioo_self, Finset.empty_val]

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h : b ≤ c
a✝ : α
hab : a✝ ∈ Ico a b
hbc : a✝ ∈ Ico c d
⊢ False

Tactic:
rw [mem_Ico] at hab hbc
    exact hab.2.not_ge (h.trans hbc.1)

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

Goal state before:
pp: a b c : ℕ
⊢ Unique ↥(Iic 0)

Tactic:
by
  rw [← Nat.bot_eq_zero]
  infer_instance

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

Goal state before:
pp: a : ℕ
⊢ Ico 0 a = range a

Tactic:
by
  rw [← Nat.bot_eq_zero, ← Iio_eq_Ico, Iio_eq_range]

Goal state after: