mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
s : Multiset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
l : List α
⊢ countP p (Quot.mk (⇑(isSetoid α)) l) =
    countP p (filter q (Quot.mk (⇑(isSetoid α)) l)) + countP p (filter (fun a ↦ ¬q a) (Quot.mk (⇑(isSetoid α)) l))

Tactic:
by
    convert! l.countP_eq_countP_filter_add (p ·) (q ·)
    simp

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

Goal state before:
pp: α : Type u_1
l : Multiset α
a : α
⊢ _root_.Disjoint {a} l ↔ ¬a ∈ l

Tactic:
simp [disjoint_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ _root_.Disjoint (ndinsert a s) t ↔ _root_.Disjoint (a ::ₘ s) t

Tactic:
simp [disjoint_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s ∪ t = s ↔ t ⊆ s

Tactic:
union_eq_left

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ⊆ s ↔ t ⊆ s
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n j : ℕ
hj : j < n + 1
⊢ ↑⟨j, hj⟩ + ↑⟨j, hj⟩.rev = n

Tactic:
simp [Nat.add_sub_cancel' <| le_of_lt_succ hj]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ n ≤ 1 ↔ n = 1

Tactic:
le_one_iff_eq_zero_or_eq_one,

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ n = 0 ∨ n = 1 ↔ n = 1
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
⊢ i.castPred ⋯ ≤ i.pred ⋯

Tactic:
have : b < a := castSucc_lt_castSucc_iff.mpr (hb.trans_le (le_of_not_gt ha))

Goal state after:
case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
this : b < a
⊢ i.castPred ⋯ ≤ i.pred ⋯
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i.predAbove = j.predAbove
⊢ i = j

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_add_one_eq.2 i.size_positive

Goal state after:
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
⊢ i = j
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

Tactic:
· by_cases h1 : 1 ≠ i ∧ 1 ≠ j
    · exact ⟨⟨1, by lia⟩, h1⟩
    · refine ⟨⟨2, by lia⟩, ?_⟩
      dsimp only
      lia

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

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
hb : b ≠ last n
hk : a.succAbove b ≠ last (n + 1)
⊢ (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk

Tactic:
simp_rw [← castSucc_inj (b := (a.succAbove b).castPred hk), ← castSucc_succAbove_castSucc,
    castSucc_castPred]

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)

Tactic:
have : Nonempty α := by
      rcases h ∅ (by simp) with ⟨y, _⟩
      exact ⟨y⟩
    choose! F hF using h
    have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
    set f := seqOfForallFinsetExistsAux P r h' with hf
    have A : ∀ n : ℕ, P (f n) := by
      intro n
      induction n using Nat.strong_induction_on with | _ n IH
      have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
      rw [hf, seqOfForallFinsetExistsAux]
      exact
        (Classical.choose_spec
            (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
            (by simp [IH'])).1
    refine ⟨f, A, fun m n hmn => ?_⟩
    conv_rhs => rw [hf]
    rw [seqOfForallFinsetExistsAux]
    apply
      (Classical.choose_spec
          (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
    exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ Fintype.card ↑s = Fintype.card α ↔ s = Set.univ

Tactic:
by
  rw [← Set.toFinset_card, Finset.card_eq_iff_eq_univ, ← Set.toFinset_univ, Set.toFinset_inj]

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

Goal state before:
pp: case mpr
α : Type u_1
s : Finset α
⊢ (∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d) →
    ∃ b b_1 b_2 b_3, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}

Tactic:
rintro ⟨a, b, c, d, ha, hb, hc, hd, hab, hac, had, hbc, hbd, hcd⟩

Goal state after:
case mpr
α : Type u_1
s : Finset α
a b c d : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
hab : a ≠ b
hac : a ≠ c
had : a ≠ d
hbc : b ≠ c
hbd : b ≠ d
hcd : c ≠ d
⊢ ∃ b b_1 b_2 b_3, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ card { x // ¬p x } = card α - card { x // p x }

Tactic:
classical
    rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype] <;>
    · intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_ofPred]

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

Goal state before:
pp: case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Tactic:
· 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.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_2
f : Fin n → α
x : α
⊢ Set.range (snoc f x) = insert x (Set.range f)

Tactic:
by
  ext; simp [Fin.exists_fin_succ', or_comm, eq_comm]

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

Goal state before:
pp: n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
⊢ g ∘ snoc q y = snoc (g ∘ q) (g y)

Tactic:
by
  ext j
  by_cases h : j.val < n
  · simp [h, snoc, castSucc_castLT]
  · rw [eq_last_of_not_lt h]
    simp

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
⊢ insertionSort r (a :: l) = a :: insertionSort r l

Tactic:
rw [insertionSort_cons]
  cases hi : insertionSort r l with
  | nil => rfl
  | cons b m =>
    rw [orderedInsert_cons_of_le]
    apply h b <| (mem_insertionSort r).1 _
    rw [hi]
    exact mem_cons_self

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hs : s ⊆ range f
⊢ s.Finite

Tactic:
by
  rw [← image_preimage_eq_of_subset hs]
  exact Finite.image f h

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)

Tactic:
simp_rw [@and_comm ((_ : Set _) ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
    Finset.subset_set_image_iff]
  aesop

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
as bs : List α
x : α
hs : as <+ bs
hb : Pairwise r bs
⊢ orderedInsert r x as <+ orderedInsert r x bs

Tactic:
cases as with
  | nil => simp
  | cons a as =>
    cases bs with
    | nil => contradiction
    | cons b bs =>
      unfold orderedInsert
      cases hs <;> split_ifs with hr
      · exact .cons_cons _ <| .cons _ ‹a :: as <+ bs›
      · have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
        simp only [hr, orderedInsert_cons, ite_true] at ih
        exact .trans ih <| .cons _ (.refl _)
      · have hba := pairwise_cons.mp hb |>.left _ (mem_of_cons_sublist ‹a :: as <+ bs›)
        exact absurd (trans_of _ ‹r x b› hba) hr
      · have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
        rw [orderedInsert_cons, if_neg hr] at ih
        exact .cons _ ih
      · simp_all
      · exact .cons_cons _ <| orderedInsert_sublist x ‹as <+ bs› hb.of_cons

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

Goal state before:
pp: case H₂
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
this : Std.Symm fun x y ↦ x ≠ y → R x y
⊢ Pairwise (fun x y ↦ x ≠ y → R x y) l

Tactic:
· exact hl.imp @fun a b h _ ↦ by exact h

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

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : a = b
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
subst b

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂
l₂ : List α
H : (a :: l₁).length ≤ (a :: l₂).length
h : a :: l₁ ≠ a :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (a :: l₁) (a :: l₂)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: α : Type u_2
L : List (List α)
i : ℕ
h : i < L.length
this : take i (map length L) = take i (map length (take (i + 1) L))
⊢ drop (take i (map length L)).sum (take (take (i + 1) (map length L)).sum L.flatten) = L[i]

Tactic:
simp only [this, take_sum_flatten, drop_sum_flatten,
    drop_take_succ_eq_cons_getElem, h, flatten_nil, flatten_cons, append_nil]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ ∀ (a : α) (s : Multiset α), filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)

Tactic:
intro a ha ih
    rw [nsmul_cons, filter_add, ih, filter_cons, nsmul_add]
    congr
    split_ifs with hp <;>
      · simp only [filter_eq_self, nsmul_zero, filter_eq_nil]
        intro b hb
        rwa [mem_singleton.mp (mem_of_mem_nsmul hb)]

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
p : α × ℕ → Prop
⊢ (∀ (x : α × ℕ), x ∈ l.zipIdx n → p x) ↔ ∀ (i : ℕ) (x : i < l.length), p (l[i], n + i)

Tactic:
simp only [forall_mem_iff_getElem, getElem_zipIdx, length_zipIdx]

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

Goal state before:
pp: n : ℕ
⊢ (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n

Tactic:
by
  rw [← add_mul_div_left, Nat.mul_comm 2 n, ← Nat.mul_add, Nat.add_sub_cancel, Nat.mul_comm]
  cases n <;> rfl; apply zero_lt_succ

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

Goal state before:
pp: n : ℕ
⊢ (n + 1 + 1) * (n + 1).choose 0 = (n + 1 + 1).choose (0 + 1) * (0 + 1)

Tactic:
by simp [choose, mul_succ, Nat.add_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ cons (a' ::ₘ m) a b (cons m a' b' f) ≍ cons (a ::ₘ m) a' b' (cons m a b f)

Tactic:
apply hfunext rfl

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ ∀ (a_1 a'_1 : α), a_1 ≍ a'_1 → cons (a' ::ₘ m) a b (cons m a' b' f) a_1 ≍ cons (a ::ₘ m) a' b' (cons m a b f) a'_1
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ Disjoint s.diag s.offDiag

Tactic:
simp [disjoint_left]

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

Goal state before:
pp: case succ
k n✝ : ℕ
⊢ (n✝ + 1).ascFactorial k = k ! * (n✝ + 1 + k - 1).choose k

Tactic:
rw [ascFactorial_eq_factorial_mul_choose]

Goal state after:
case succ
k n✝ : ℕ
⊢ k ! * (n✝ + k).choose k = k ! * (n✝ + 1 + k - 1).choose k
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
x✝ : α
⊢ x✝ ∈ iUnion (Fin.snoc f s) ↔ x✝ ∈ (⋃ i, f i) ∪ s

Tactic:
simp [Fin.exists_iff_castSucc, or_comm]

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅)

Tactic:
contrapose! +distrib

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun x ↦ f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

Tactic:
contrapose! +distrib

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun x ↦ f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (image2 f s t).Infinite ↔ (s.Infinite ∨ t.Infinite) ∧ s.Nonempty ∧ t.Nonempty
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Group α
i : ℤ
a b : α
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹

Tactic:
cases i

Goal state after:
case ofNat
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.ofNat a✝ = a * b ^ Int.ofNat a✝ * a⁻¹

case negSucc
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.negSucc a✝ = a * b ^ Int.negSucc a✝ * a⁻¹
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
b : β
⊢ b ∈ f '' s ↔ b ∈ ⋃ i ∈ s, {f i}

Tactic:
by simp [@eq_comm β b]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ (fun x ↦ f x⁻¹) '' s = g '' s

Tactic:
exact Set.image_congr H

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

Goal state before:
pp: case mp
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

Tactic:
contrapose! +distrib

Goal state after:
case mp
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s.Nonempty ∨ n = 0 → (s ^ n).Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

Tactic:
contrapose! +distrib

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s.Nonempty ∨ n = 0 → (s ^ n).Nonempty
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 N
hH : H ≤ f.range
hK : K ≤ f.range
⊢ map f (comap f H ⊔ comap f K) = map f (comap f (H ⊔ K))

Tactic:
rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
        inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
h : (decode₂ α x).isSome = true
⊢ decode₂ α x = some ((decode₂ α x).get h)

Tactic:
Option.some_get

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
h : (decode₂ α x).isSome = true
⊢ decode₂ α x = decode₂ α x
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: m n : ℕ
⊢ max m n ^ 2 + min m n ≤ pair m n

Tactic:
rw [pair]
  rcases lt_or_ge m n with h | h
  · rw [if_pos h, max_eq_right h.le, min_eq_left h.le, Nat.pow_two]
  rw [if_neg h.not_gt, max_eq_left h, min_eq_right h, Nat.pow_two, Nat.add_assoc,
    Nat.add_le_add_iff_left]
  exact Nat.le_add_left _ _

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
l : List ι
f g : ι → M
h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i
h₂ : ∃ i, i ∈ l ∧ f i < g i
⊢ (map f l).prod < (map g l).prod

Tactic:
induction l with
  | nil => simp at h₂
  | cons i l ihl =>
    simp only [forall_mem_cons, map_cons, prod_cons] at h₁ ⊢
    simp only [mem_cons, exists_eq_or_imp] at h₂
    cases h₂
    · exact mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod' h₁.2)
    · exact mul_lt_mul_of_le_of_lt h₁.1 <| ihl h₁.2 ‹_›

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

Goal state before:
pp: case hS
M : Type u_1
inst✝ : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ Directed (S ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) Subtype.val

Tactic:
exact hS.directed_val

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p 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) ⋯)) x) =
    x

Tactic:
cases x with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : Lex (α × β)
h : x < y
⊢ ∃ a, x < a ∧ a < y

Tactic:
cases x with

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
y : Lex (α × β)
x : α × β
h : toLex x < y
⊢ ∃ a, toLex x < a ∧ a < y
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : Lex (α × β)
h : x < y
⊢ ∃ a, x < a ∧ a < y

Tactic:
cases x with

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
y : Lex (α × β)
x : α × β
h : toLex x < y
⊢ ∃ a, toLex x < a ∧ a < y
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
z : ↥(powers x)
⊢ z ^ 0 = 1

Tactic:
simp_rw [HPow.hPow, Pow.pow]
    simp only [Int.natMod, Int.zero_emod, Int.toNat_zero, pow_zero]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝² : α
a✝¹ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
a✝ : α
⊢ ∀ (m : α),
    m ∈ Option.rec (some a✝²) (fun val ↦ if r a✝² val then some a✝² else some val) (foldl (argAux r) (some a✝) l✝) →
      m ∈ a✝ :: (l✝ ++ [a✝²])

Tactic:
cases _ : foldl _ _ _

Goal state after:
case none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝² : α
a✝¹ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
a✝ : α
h✝ : foldl (argAux r) (some a✝) l✝ = none
⊢ ∀ (m : α),
    m ∈ Option.rec (some a✝²) (fun val ↦ if r a✝² val then some a✝² else some val) none → m ∈ a✝ :: (l✝ ++ [a✝²])

case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝² : α
a✝¹ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
a✝ val✝ : α
h✝ : foldl (argAux r) (some a✝) l✝ = some val✝
⊢ ∀ (m : α),
    m ∈ Option.rec (some a✝²) (fun val ↦ if r a✝² val then some a✝² else some val) (some val✝) → m ∈ a✝ :: (l✝ ++ [a✝²])
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
a : α
l : List α
⊢ argmax f (l ++ [a]) = Option.casesOn (argmax f l) (some a) fun c ↦ if f c < f a then some a else some c

Tactic:
by
  rw [argmax, argmax]; simp [argAux]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
h : u ⊆ v
x✝ : β
⊢ x✝ ∈ u.toRight → x✝ ∈ v.toRight

Tactic:
by simpa only [mem_toRight] using @h _

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

Goal state before:
pp: case cons
α : Type u_1
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
IH : powersetAux' l₁✝ ~ powersetAux' l₂✝
⊢ powersetAux' (x✝ :: l₁✝) ~ powersetAux' (x✝ :: l₂✝)

Tactic:
simp only [powersetAux'_cons]

Goal state after:
case cons
α : Type u_1
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
IH : powersetAux' l₁✝ ~ powersetAux' l₂✝
⊢ powersetAux' l₁✝ ++ List.map (cons x✝) (powersetAux' l₁✝) ~ powersetAux' l₂✝ ++ List.map (cons x✝) (powersetAux' l₂✝)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ List.map (Prod.map ofList ofList) (l.sublists.zip l.sublists.reverse)
⊢ x.1 + x.2 = ↑l

Tactic:
← revzip,

Goal state after:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ List.map (Prod.map ofList ofList) l.sublists.revzip
⊢ x.1 + x.2 = ↑l
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ List.map (Prod.map ofList ofList) (l.sublists'.zip l.sublists'.reverse)
⊢ x.1 + x.2 = ↑l

Tactic:
← revzip,

Goal state after:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ List.map (Prod.map ofList ofList) l.sublists'.revzip
⊢ x.1 + x.2 = ↑l
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) l (g ∘ f) (sublistsLenAux n l ((g ∘ f) ∘ cons a) (map g r ++ s)) =
    map g (sublistsLenAux (n + 1) l f (sublistsLenAux n l (f ∘ cons a) r)) ++ s

Tactic:
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: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n ↦ sublistsLen n tl) (0 :: map succ (range tl.length)) ~ tl.sublists'

Tactic:
← range_succ_eq_map

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ l = l.toFinset.sup id

Tactic:
rw [← coe_fold_r, ← Multiset.fold_dedup_idem, sup_def, ← List.toFinset_coe, toFinset_val,
    Multiset.map_id]
  rfl

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (i, i') ≤ (fun i ↦ ⨆ i' ∈ t, f (i, i')) (i, i').1

Tactic:
convert! le_iSup₂ (α := α) i' hi.2

Goal state after:
case e'_3
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (i, i') = f ((i, i').1, i')