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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
⊢ x ∈ s ∪ t ↔ Xor (x ∈ s) (x ∈ t)

Tactic:
by
  rw [Finset.mem_union, Xor]
  have := disjoint_left.1 h
  tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
hf : Injective f
⊢ Injective (image f)

Tactic:
by
  simpa only [funext (map_eq_image _)] using! map_injective ⟨f, hf⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
this : (∃ i, f (i % ↑n) = a) ↔ ∃ i < n, f ↑i = a
⊢ a ∈ Set.range f ↔ a ∈ image (fun i ↦ f ↑i) (range n)

Tactic:
simpa [h]

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

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
ha : a ∉ s
⊢ (cons a s ha).attach = cons ⟨a, ⋯⟩ (map { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ } s.attach) ⋯

Tactic:
by ext ⟨x, hx⟩; simpa using hx

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ (insert a s).attach = insert ⟨a, ⋯⟩ (image (fun x ↦ ⟨↑x, ⋯⟩) s.attach)

Tactic:
by ext ⟨x, hx⟩; simpa using hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Option β
s : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
⊢ ∀ (x : β), x ∈ ↑(filterMap f s f_inj) ↔ x ∈ {b | ∃ a ∈ s, f a = some b}

Tactic:
simp only [mem_coe, mem_filterMap, Set.mem_ofPred_eq, implies_true]

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

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

pp: case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ a.pred ⋯ ≤ b.castPred ⋯

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

pp: case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ a.castPred ⋯ ≤ b.castPred ⋯

Tactic:
all_goals simp only [le_iff_val_le_val, val_pred]

Goal state after:
case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : p.castSucc < b
⊢ ↑a - 1 ≤ ↑b - 1

case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑a - 1 ≤ ↑(b.castPred ⋯)

case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑b - 1

case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
h : i < j
⊢ i = j

Tactic:
replace hij := congr_fun hij i.succ

Goal state after:
n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i.predAbove i.succ = j.predAbove i.succ
⊢ i = j
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ #s = #t

Tactic:
by
  classical
  calc
    #s = #s.attach := card_attach.symm
    _ = #(s.attach.image fun a ↦ i a.1 a.2) := Eq.symm ?_
    _ = #t := ?_
  · apply card_image_of_injective
    intro ⟨_, _⟩ ⟨_, _⟩ h
    simpa using i_inj _ _ _ _ h
  · congr 1
    ext b
    constructor <;> intro h
    · obtain ⟨_, _, rfl⟩ := mem_image.1 h; apply hi
    · obtain ⟨a, ha, rfl⟩ := i_surj b h; exact mem_image.2 ⟨⟨a, ha⟩, by simp⟩

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i ≠ p

Tactic:
by
  rcases p.castSucc_lt_or_lt_succ i with (h | h)
  · rw [succAbove_of_castSucc_lt _ _ h]
    exact Fin.ne_of_lt h
  · rw [succAbove_of_lt_succ _ _ h]
    exact Fin.ne_of_gt h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
e : α ≃ β
⊢ map (⇑e) univ.val = univ.val

Tactic:
rw [← congr_arg Finset.val (Finset.map_univ_equiv e), Finset.map_val, Equiv.coe_toEmbedding]

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
h : ∃ a b, a ∈ s ∧ b ∈ s ∧ ∃ a_1, a a_1 ≠ b a_1
⊢ ∃ i, (∃ a b, a ∈ image (fun x ↦ x i) s ∧ b ∈ image (fun x ↦ x i) s ∧ a ≠ b) ∧ ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s

Tactic:
obtain ⟨a1, a2, h1, h2, i, hne⟩ := h

Goal state after:
ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
⊢ ∃ i, (∃ a b, a ∈ image (fun x ↦ x i) s ∧ b ∈ image (fun x ↦ x i) s ∧ a ≠ b) ∧ ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s
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:
← card_ofFinset s H

Goal state after:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = card ↑p
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α → β
hf : Injective f
h : card β = card α + 1
⊢ ∃! x, x ∉ image f univ

Tactic:
simpa using existsUnique_notMem_image_of_injOn_of_card_eq_add_one
      (s := .univ) (t := .univ) (Set.injOn_of_injective hf) (by simp) (by simpa)

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

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

Tactic:
rintro ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩
      exact ⟨a, b, c, {a, b, c}, by simp_all [insert_subset_iff]⟩

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

Goal state before:
pp: m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
⊢ Injective (append xs ys) ↔ Injective xs ∧ Injective ys ∧ ∀ (i : Fin m) (j : Fin n), xs i ≠ ys j

Tactic:
by
  -- TODO: move things around so we can just import this.
  -- We inline it because it's still shorter than proving from scratch.
  let finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (Fin.castAdd n) (Fin.natAdd m)
    invFun i := @Fin.addCases m n (fun _ => Fin m ⊕ Fin n) Sum.inl Sum.inr i
    left_inv x := by rcases x with y | y <;> simp
    right_inv x := by refine Fin.addCases (fun i => ?_) (fun i => ?_) x <;> simp }
  rw [← Sum.elim_injective, ← append_comp_sumElim, ← finSumFinEquiv.injective_comp,
    Equiv.coe_fn_mk]

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

Goal state before:
pp: case cast
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin n
⊢ snoc (update p i y) x j.castSucc = update (snoc p x) i.castSucc y j.castSucc

Tactic:
rcases eq_or_ne j i with rfl | hne

Goal state after:
case cast.inl
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
j : Fin n
y : α j.castSucc
⊢ snoc (update p j y) x j.castSucc = update (snoc p x) j.castSucc y j.castSucc

case cast.inr
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin n
hne : j ≠ i
⊢ snoc (update p i y) x j.castSucc = update (snoc p x) i.castSucc y j.castSucc
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Fintype ℕ), False

Tactic:
by
    intro h
    exact (Finset.range _).card_le_univ.not_gt ((Nat.lt_succ_self _).trans_eq (card_range _).symm)

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

Goal state before:
pp: case mp
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
⊢ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

Tactic:
have h : ∀ {i : ℕ}, i < l.length → f i < l'.length := by
      intro i hi
      specialize hf i
      rw [getElem?_eq_getElem hi, eq_comm, getElem?_eq_some_iff] at hf
      obtain ⟨h, -⟩ := hf
      exact h

Goal state after:
case mp
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
⊢ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case neg
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : ¬j < l.length
⊢ i + l'.length < j + l'.length

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ (s ∪ sᶜ).Finite

Tactic:
exact hs.union hsc

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

Goal state before:
pp: case mpr.refine_2.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi : 0 < (replicate 2 x).length
⊢ (replicate 2 x).get ⟨0, hi⟩ = l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ⟨0, hi⟩)

Tactic:
simpa using h

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

Goal state before:
pp: 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
⊢ p.removeNth (update f (p.succAbove i) x) j = update (p.removeNth f) i x j

Tactic:
rcases eq_or_ne j i with rfl | hne

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

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
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise (fun a b ↦ decide (r a b) = true) l

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
l₁ l₂ : List α
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
hl₁ : l₁.SortedLT
hl₂ : l₂.SortedGT
⊢ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂.reverse

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
l₁ l₂ : List α
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
hl₁ : l₁.SortedGT
hl₂ : l₂.SortedLT
⊢ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂.reverse

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
l : List (List α)
hl : l ≠ []
hl' : l.getLast hl ≠ []
x✝ : l = [] ∨ ∃ l' b, l = l'.concat b
⊢ (l.getLast hl).getLast hl' = l.flatten.getLast ⋯

Tactic:
cases eq_nil_or_concat l with

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

Goal state before:
pp: α : Type u_1
ai : ℕ
a b : Fin ai → α
h : ⟨ai, a⟩.snd = ⟨ai, b⟩.snd ∘ Fin.cast ⋯
⊢ ⟨ai, a⟩ = ⟨ai, b⟩

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ min y z ≤ x ↔ x ≥ y ∨ x ≥ z

Tactic:
exact min_le_iff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold max b f s < c ↔ b < c ∧ ∀ x ∈ s, f x < c

Tactic:
by
  change _ > _ ↔ _
  apply fold_op_rel_iff_and
  intro x y z
  change _ < _ ↔ _
  exact max_lt_iff

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

Goal state before:
pp: case cons
α : Type u_1
R : α → α → Prop
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
head✝ : α
tail✝ : List α
h : Pairwise R (head✝ :: tail✝)
ha : a ∈ head✝ :: tail✝
⊢ R (head✝ :: tail✝).head! a

Tactic:
cases ha with

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
h✝ : Pairwise R l
a b : α
h : R a b
⊢ Decidable.decide (R a b) = true

Tactic:
simpa using h

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

Goal state before:
pp: case succ.succ
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (m + 1)
⊢ (∀ (m : ℕ), m < n → r m (m + 1)) ∧ r n (n + 1) ↔ ∀ (m : ℕ), m < n + 1 → r m (m + 1)

Tactic:
forall_lt_succ_right

Goal state after:
case succ.succ
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (m + 1)
⊢ (∀ (m : ℕ), m < n → r m (m + 1)) ∧ r n (n + 1) ↔ (∀ (m : ℕ), m < n → r m (m + 1)) ∧ r n (n + 1)
Module: Mathlib.Data.List.Range

Goal state before:
pp: case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise (fun a_1 b ↦ (map (fun x ↦ a + x) a_1).Disjoint (map (fun x ↦ a + x) b)) l.ranges

Tactic:
apply Pairwise.imp _ hl

Goal state after:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ ∀ {a_1 b : List ℕ}, a_1.Disjoint b → (map (fun x ↦ a + x) a_1).Disjoint (map (fun x ↦ a + x) b)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
inst✝ : Trans R R R
hl : IsChain R l₂
h : l₁ <+ l₂
⊢ IsChain R l₁

Tactic:
rw [isChain_iff_pairwise] at hl ⊢
  exact hl.sublist h

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

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
ih : op xs.prod = (map op xs).reverse.prod
⊢ op (x * xs.prod) = (map op xs).reverse.prod * op x

Tactic:
op_mul,

Goal state after:
case cons
M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
ih : op xs.prod = (map op xs).reverse.prod
⊢ op xs.prod * op x = (map op xs).reverse.prod * op x
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
hα : Nonempty α
a : α
l : List α
h : ∀ (n : ℕ), (a :: l).rotate n = a :: l
n : ℕ
h₁ : n < (a :: l).length
h₂ : n < (replicate (a :: l).length a).length
⊢ (a :: l).head? = some a

Tactic:
head?_cons

Goal state after:
α : Type u
hα : Nonempty α
a : α
l : List α
h : ∀ (n : ℕ), (a :: l).rotate n = a :: l
n : ℕ
h₁ : n < (a :: l).length
h₂ : n < (replicate (a :: l).length a).length
⊢ some a = some a
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
⊢ l = l'

Tactic:
obtain ⟨hd, ht⟩ := append_inj h (by simp_all)

Goal state after:
α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
⊢ l = l'
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons.intro.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l✝ : List α
hl' : List.IsChain (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l → ∀ (hl : List.IsChain (flip r) (a :: ↑y)), Acc (List.lex_chains r) ⟨a :: ↑y, hl⟩
⊢ ∀ (hl : List.IsChain (flip r) (a :: ↑l)), Acc (List.lex_chains r) ⟨a :: ↑l, hl⟩

Tactic:
intro hl
      apply Acc.intro
      rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
      · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
      · apply ih b hr
      · apply ihl ⟨m, (List.isChain_cons.1 hm).2⟩ hr

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 : α
⊢ a ∈ m → (if p a then {a} else 0).bind f = if p a then f a else 0

Tactic:
ham

Goal state after:
α : 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
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : α
⊢ a ∈ m → ((Option.map singleton (f a)).getD 0).bind g = (Option.map g (f a)).getD 0

Tactic:
ham

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : α
ham : a ∈ m
⊢ ((Option.map singleton (f a)).getD 0).bind g = (Option.map g (f a)).getD 0
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
h : ∀ (a b : α), (List.count a l * List.count b l - if a = b then List.count a l else 0) ≤ 1
a : α
⊢ List.count a l ≤ 1

Tactic:
specialize h a a

Goal state after:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : (List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1
⊢ List.count a l ≤ 1
Module: Mathlib.Data.Fintype.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
x y : ι
hne : ¬x = y
h : n x = update m y (n y) x ∧ ∀ (x_1 : ι), x_1 ≠ x → m x_1 = update m y (n y) x_1
⊢ False

Tactic:
update_of_ne hne

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
x y : ι
hne : ¬x = y
h : n x = m x ∧ ∀ (x_1 : ι), x_1 ≠ x → m x_1 = update m y (n y) x_1
⊢ False
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((a ::ₘ s.val).pi fun a ↦ (t a).val).dedup =
    ((t a).val.bind fun b ↦
        (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup).dedup

Tactic:
pi_cons

Goal state after:
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((t a).val.bind fun b ↦ Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a ↦ (t a).val)).dedup =
    ((t a).val.bind fun b ↦
        (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup).dedup
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : a = b
⊢ a = b

Tactic:
exact hc

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

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

Tactic:
preimage_iUnion₂

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
⊢ ⋃ i ∈ s, f ⁻¹' i = ⋃ t ∈ s, f ⁻¹' t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i

Tactic:
· intro x hz x' hw
    exact ⟨x ⊔ x', hs le_sup_left hz, ht le_sup_right hw⟩

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
x y : G
h : x ∈ H
hab : x * y ∈ H
⊢ y ∈ H

Tactic:
by simpa using mul_mem (inv_mem h) hab

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_7
inst✝ : Group N
f : G →* N
⊢ ↑f.range = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
rw [coe_range, coe_top]

Goal state after:
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:
by
  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 mpr
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
⊢ (∃ y ∈ s, ∃ z ∈ t, y * z = x) → x ∈ s ⊔ t

Tactic:
· rintro ⟨y, hy, z, hz, rfl⟩; exact mul_mem_sup hy hz

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s : Set M
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Tactic:
congr with a

Goal state after:
M : Type u_2
inst✝ : Mul M
s : Set M
a : Subsemigroup Mᵐᵒᵖ
⊢ s ⊆ MulOpposite.op ⁻¹' ↑a ↔ MulOpposite.unop ⁻¹' s ⊆ ↑a
Module: Mathlib.Algebra.Group.Submonoid.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
s : Set M
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Tactic:
congr with a

Goal state after:
M : Type u_2
inst✝ : MulOneClass M
s : Set M
a : Submonoid Mᵐᵒᵖ
⊢ s ⊆ MulOpposite.op ⁻¹' ↑a ↔ MulOpposite.unop ⁻¹' s ⊆ ↑a
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mpr
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
h1' : (inl M N) x1 ∈ u
h2' : (inr M N) x2 ∈ u
⊢ (x1, x2) ∈ u

Tactic:
simpa using Submonoid.mul_mem _ h1' h2'

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

Goal state before:
pp: m n : ℕ
⊢ m * 2 ^ n * 2 = 2 ^ (n + 1) * m

Tactic:
Nat.mul_assoc,

Goal state after:
m n : ℕ
⊢ m * (2 ^ n * 2) = 2 ^ (n + 1) * m
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ n.boddDiv2 = (n.bodd, n.div2)

Tactic:
induction n with
  | zero => rfl
  | succ n ih =>
    rw [boddDiv2, ih]
    cases hn : n.bodd <;> simp [hn]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {K | MulOpposite.unop ⁻¹' s ⊆ ↑K}

Tactic:
congr with a

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
a : Subgroup Gᵐᵒᵖ
⊢ s ⊆ MulOpposite.op ⁻¹' ↑a ↔ MulOpposite.unop ⁻¹' s ⊆ ↑a
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_3
inst✝ : Group N
f : G →* N
x : G
⊢ Subgroup.map f (Subgroup.zpowers x) = Subgroup.zpowers (f x)

Tactic:
by
  rw [Subgroup.zpowers_eq_closure, Subgroup.zpowers_eq_closure, f.map_closure, Set.image_singleton]

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

Goal state before:
pp: G : Type u_5
inst✝ : CommGroup G
s : Set G
x✝ : G
⊢ x✝ ∈ normalizer s ↔ x✝ ∈ ⊤

Tactic:
simp [mem_set_normalizer_iff]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
T : Set γ
⊢ (a • b) • T = a • b • T

Tactic:
by simp only [← image_smul, image_image, smul_assoc]

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

Goal state before:
pp: case left.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ j✝¹ : ι
a : α i✝
b : α j✝¹
hij : r i✝ j✝¹
j✝ : ι
c : α j✝
hk : r j✝¹ j✝
⊢ Lex r s ⟨i✝, a⟩ ⟨j✝, c⟩

Tactic:
exact Lex.left _ _ (_root_.trans hij hk)

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

Goal state before:
pp: M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
b : M
h : ∀ (x : M), x ∈ [b] → 1 < x
x✝ : [b] ≠ []
⊢ 1 < [b].prod

Tactic:
simpa using h

Goal state after: