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

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nontrivial
⊢ ∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s

Tactic:
classical
  obtain ⟨a, ha, b, hb, hab⟩ := hs
  have : b ∈ s.erase a := mem_erase.2 ⟨hab.symm, hb⟩
  refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩ <;> simp [insert_erase ha, *]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
x✝ : ↥(map f s)
x : β
hx : x ∈ map f s
⊢ ∃ a, (fun x ↦ ⟨f ↑x, ⋯⟩) a = ⟨x, hx⟩

Tactic:
by
    obtain ⟨x, hxs, rfl⟩ := mem_map.mp hx
    exact ⟨⟨x, hxs⟩, rfl⟩

Goal state after:
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
⊢ #(image (fun i ↦ f ↑i ⋯) (range n).attach) = #(range n).attach

Tactic:
apply card_image_of_injective

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
⊢ Injective fun i ↦ f ↑i ⋯
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case calc_1
α : 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
⊢ #(image (fun a ↦ i ↑a ⋯) s.attach) = #s.attach

Tactic:
apply card_image_of_injective

Goal state after:
case calc_1
α : 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
⊢ Injective fun a ↦ i ↑a ⋯
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.castSucc < p ∨ p < i.succ

Tactic:
by
  simp [Fin.lt_def, -val_fin_lt]
  lia

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

Goal state before:
pp: α : Type u
⊢ ofFn [].get = []

Tactic:
ofFn_zero

Goal state after:
α : Type u
⊢ [] = []
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
rwa [succ_zero_eq_one, zero_succAbove] at this

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ #s + 1 = #t

Tactic:
by
  constructor
  · grind
  · rintro ⟨hst, h⟩
    obtain ⟨a, ha⟩ : ∃ a, t \ s = {a} := card_eq_one.mp (by grind)
    grind =>
      have : a ∈ t \ s
      have h : insert a s ⊆ t
      have := eq_of_subset_of_card_le h
      instantiate

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

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 1) → ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
grind [card_eq_one]

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

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 2) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
grind [card_eq_two]

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

Goal state before:
pp: case refine_1.cons_duplicate
α : Type u_1
l : List α
x y : α
hm : x ∈+ l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
exact Or.inr hm

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

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?
⊢ l'[f 0] ∈ take (f 0 + 1) l'

Tactic:
l'.getElem_take' _ (Nat.lt_succ_self _)

Goal state after:
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?
⊢ (take (f 0).succ l')[f 0] ∈ take (f 0 + 1) l'
Module: Mathlib.Data.Fintype.EquivFin

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

Tactic:
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 α
⊢ l <+ l' → ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?

Tactic:
intro H
    induction H with
    | slnil => simp
    | cons _ _ IH =>
      obtain ⟨f, hf⟩ := IH
      refine ⟨f.trans (OrderEmbedding.ofStrictMono (· + 1) fun _ => by simp), ?_⟩
      simpa using hf
    | cons_cons _ _ IH =>
      obtain ⟨f, hf⟩ := IH
      refine
        ⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) ?_, ?_⟩
      · rintro ⟨_ | a⟩ ⟨_ | b⟩ <;> simp [Nat.succ_le_succ_iff]
      · rintro ⟨_ | i⟩
        · simp
        · simpa using hf _

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ t
h : t ⊆ s
⊢ Fintype ↑t

Tactic:
by
  rw [← inter_eq_self_of_subset_right h]
  apply Set.fintypeInterOfLeft

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

Goal state before:
pp: case cons.cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
hs : a :: as <+ b :: bs
⊢ orderedInsert r x (a :: as) <+ orderedInsert r x (b :: bs)

Tactic:
unfold orderedInsert

Goal state after:
case cons.cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
hs : a :: as <+ b :: bs
⊢ (if r x a then x :: a :: as else a :: orderedInsert r x as) <+
    if r x b then x :: b :: bs else b :: orderedInsert r x bs
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_3
p : Fin (n + 1)
x : α
f : Fin n → α
y : α
⊢ y ∈ range (p.insertNth x f) ↔ y ∈ Set.insert x (range f)

Tactic:
simp [Fin.exists_iff_succAbove p, Set.insert, eq_comm]

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
b₁ b₂ : α
⊢ fold op (op b₁ b₂) (s₁ ∪ s₂ + s₁ ∩ s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)

Tactic:
union_add_inter,

Goal state after:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
b₁ b₂ : α
⊢ fold op (op b₁ b₂) (s₁ + s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)
Module: Mathlib.Data.List.Sort

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

Tactic:
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.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
s : Set α
t : Set β
f : α → β
hs : s.Infinite
hf : MapsTo f s t
ht : t.Finite
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Tactic:
contrapose! ht
  exact infinite_of_injOn_mapsTo (fun x hx y hy => not_imp_not.1 (ht x hx y hy)) hf hs

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₁.val ∪ s₂.val + s₁.val ∩ s₂.val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))

Tactic:
union_add_inter,

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₁.val + s₂.val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
Module: Mathlib.Data.Finset.Fold

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

Tactic:
hr,

Goal state after:
case insert
α : 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 : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ r c (f a) ∧ r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
rcases lt_trichotomy (k : ℕ) j with (h | h | h)
  · rwa [j.succAbove_of_castSucc_lt, contractNth_apply_of_lt]
    · rwa [Fin.lt_def]
  · exact False.elim (hjk h.symm)
  · rwa [j.succAbove_of_le_castSucc, contractNth_apply_of_gt]
    · exact Fin.le_iff_val_le_val.2 (le_of_lt h)

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

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

Tactic:
hr,

Goal state after:
case insert
α : 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 : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ r c (f a) ∨ r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
a : α
n : ℕ
⊢ (a :: l).rotate' n.succ = (l ++ [a]).rotate' n

Tactic:
by simp [rotate']

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

Goal state before:
pp: case cons_cons
α : Type u_1
a b : α
l : List α
IH : IsChain (fun x1 x2 ↦ x1 = x2) l ↔ ∀ (a : α), a ∈ l.head? → l = replicate l.length a
IH2 :
  ∀ (y : α),
    IsChain (fun x1 x2 ↦ x1 = x2) (y :: l) ↔ ∀ (a : α), a ∈ (y :: l).head? → y :: l = replicate (y :: l).length a
⊢ IsChain (fun x1 x2 ↦ x1 = x2) (a :: b :: l) ↔
    ∀ (a_1 : α), a_1 ∈ (a :: b :: l).head? → a :: b :: l = replicate (a :: b :: l).length a_1

Tactic:
simp +contextual [isChain_cons_cons, eq_comm, IH2, replicate_succ]

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

Goal state before:
pp: case cons.intro.intro.cons.rel
α : 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)
b : α
m : List α
hm : List.IsChain (flip r) (b :: m)
hr : r b a
⊢ Acc (List.lex_chains r) ⟨b :: m, hm⟩

Tactic:
apply ih b hr

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: s : Multiset ℕ
n : ℕ
⊢ s.prod % n = (map (fun x ↦ x % n) s).prod % n

Tactic:
by
  induction s using Multiset.induction <;> simp [Nat.mul_mod, *]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : ExistsAddOfLE M
inst✝³ : AddLeftMono M
inst✝² : AddLeftReflectLE M
inst✝¹ : Sub M
inst✝ : OrderedSub M
l : Multiset ι
f g : ι → M
hfg : ∀ (x : ι), x ∈ l → g x ≤ f x
⊢ (map (fun x ↦ f x - g x) l).sum + (map g l).sum = (map f l).sum

Tactic:
← sum_map_add

Goal state after:
ι : Type u_2
M : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : ExistsAddOfLE M
inst✝³ : AddLeftMono M
inst✝² : AddLeftReflectLE M
inst✝¹ : Sub M
inst✝ : OrderedSub M
l : Multiset ι
f g : ι → M
hfg : ∀ (x : ι), x ∈ l → g x ≤ f x
⊢ (map (fun i ↦ f i - g i + g i) l).sum = (map f l).sum
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
a : α
l : List α
| map (fun x ↦ (x, a)) l

Tactic:
rw [← zipIdx_map_fst 0 l, map_map, Function.comp_def]

Goal state after:
α : Type u_1
a : α
l : List α
| map (fun x ↦ (x.fst, a)) l.zipIdx
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n a b : ℕ
h : n = a + b
⊢ n.choose (n - b) = n.choose b

Tactic:
exact choose_symm (h ▸ le_add_left _ _)

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

Goal state before:
pp: α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst✝ : DecidableEq α
⊢ (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty

Tactic:
by
  simp [Finset.Nonempty, Classical.skolem]

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
ht : ∀ (b : α), a ≠ b → (t b).Nonempty
⊢ image (fun f ↦ f a) (piFinset t) = t a

Tactic:
refine (eval_image_piFinset_subset _ _).antisymm fun x h ↦ mem_image.2 ?_
  choose f hf using ht
  exact ⟨fun b ↦ if h : a = b then h ▸ x else f _ h, by aesop, by simp⟩

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

Goal state before:
pp: n : ℕ
⊢ n.multichoose 0 = 1

Tactic:
by cases n <;> simp [multichoose]

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

Goal state before:
pp: case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ v i ⊆ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k

Tactic:
intro y y_in
      simp only [mem_image, mem_iInter, mem_preimage]
      rcases hv with ⟨z, hz⟩
      refine ⟨Function.update z i y, ?_, update_self i y z⟩
      rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]
      exact ⟨y_in, fun j _ => by simpa using hz j⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ i, s i
y : α
hy✝ : y ∈ ⋃ i, s i
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
⊢ x = y

Tactic:
rcases hs i j with ⟨k, hi, hj⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ i, s i
y : α
hy✝ : y ∈ ⋃ i, s i
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hi : s i ⊆ s k
hj : s j ⊆ s k
⊢ x = y
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : ∀ (i : ι), IsMulTorsionFree (M i)
n : ℕ
hn : n ≠ 0
a b : (i : ι) → M i
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a = b

Tactic:
ext i; exact pow_left_injective hn <| congr_fun hab i

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

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

Tactic:
· exact Pi.mulSingle_commute hij _ _

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s / t

Tactic:
rw [div_eq_mul_inv]; exact subset_mul_right _ hs

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H ≠ ⊥ ↔ ∃ a, a ≠ 1

Tactic:
rw [← nontrivial_iff_ne_bot, nontrivial_iff_exists_ne_one]
  simp only [ne_eq, Subtype.exists, mk_eq_one, exists_prop]

Goal state after:
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 G
⊢ map f H ≤ map f K ↔ H ≤ K ⊔ f.ker

Tactic:
rw [map_le_iff_le_comap, comap_map_eq]

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

Goal state before:
pp: m n : ℕ
⊢ (m + n).bodd = (m.bodd ^^ n.bodd)

Tactic:
by
  induction n
  case zero => simp
  case succ n ih => simp [← Nat.add_assoc, ih]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ map f (normalizer ↑(comap f H)) ≤ normalizer ↑H

Tactic:
apply (le_normalizer_map f).trans

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ normalizer ↑(map f (comap f H)) ≤ normalizer ↑H
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
h : IsUnit 1
⊢ IsIdempotentElem 1

Tactic:
exact .one

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✝² : LinearOrder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l : List ι
f g : ι → M
h : (map f l).prod < (map g l).prod
⊢ ∃ i, i ∈ l ∧ f i < g i

Tactic:
contrapose! h
  exact prod_le_prod' h

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

Goal state before:
pp: case of_mul
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : ∀ (h : (FreeMonoid.lift Subtype.val) y ∈ closure s), motive ((FreeMonoid.lift Subtype.val) y) h
h : (FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y) ∈ closure s
⊢ motive ((FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y)) h

Tactic:
simp only [map_mul, FreeMonoid.lift_eval_of]
    refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)
    simp only [closure_eq_mrange, mem_mrange, exists_apply_eq_apply]

Goal state after:
Module: Mathlib.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
⊢ ⟨x, hx⟩ ≤ ofNat s (a + 1)

Tactic:
exact le_succ_of_forall_lt_le fun z hz => List.le_maximum_of_mem (hmt.2 hz) hmax

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a✝ : α
b✝ : β
x : α ⊕ β
u v : Finset (α ⊕ β)
a : α
b : β
f : α ⊕ β ↪ γ
⊢ Disjoint (map (Embedding.inl.trans f) s) (map (Embedding.inr.trans f) t)

Tactic:
as_aux_lemma =>
          simpa only [← map_map]
            using (Finset.disjoint_map f).2 (disjoint_map_inl_map_inr _ _)

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
h : l ≠ []
head✝ : α
tail✝ : List α
x✝ : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝).maximum ≠ ⊥

Tactic:
simp [maximum_cons]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
h : 0 < l.length
head✝ : α
tail✝ : List α
x✝ : 0 < (head✝ :: tail✝).length
⊢ (head✝ :: tail✝).maximum ≠ ⊥

Tactic:
simp [maximum_cons]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
f g : TopHom α β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
g : TopHom α β
toFun✝ : α → β
map_top'✝ : toFun✝ ⊤ = ⊤
h : { toFun := toFun✝, map_top' := map_top'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_top' := map_top'✝ } = g
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f g : SupHom α β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
g : SupHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
h : { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_sup' := map_sup'✝ } = g
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: case pos
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ (s.erase x).max ≠ ↑x

Tactic:
refine ne_of_eq_of_ne (coe_max' s0).symm ?_

Goal state after:
case pos
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ ↑((s.erase x).max' s0) ≠ ↑x
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.mpr.cons_cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
l₁✝ : List α
h : l₁✝ <+ t
⊢ a :: l₁✝ <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: l₁✝

Tactic:
· exact Or.inr ⟨_, h, rfl⟩

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

Goal state before:
pp: case cons
α : Type u
l₂ : List α
a : α
l₁ : List α
ih :
  foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂)
      l₁ =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₁)
⊢ foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂)
      (a :: l₁) =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] (a :: l₁))

Tactic:
rw [foldr_cons, ih]
    simp [List.flatMap, flatten_flatten, Function.comp_def]

Goal state after: