mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
⊢ l₁ <+~ l₂ ↔ ∃ l, l ~ l₂ ∧ l₁ <+ l

Tactic:
refine ⟨?_, fun ⟨l, h₁, h₂⟩ ↦ h₂.subperm.trans h₁.subperm⟩

Goal state after:
α : Type u_1
l₁ l₂ : List α
⊢ l₁ <+~ l₂ → ∃ l, l ~ l₂ ∧ l₁ <+ l
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
s : Multiset α
n : ℕ
⊢ s.card = n + 1 → ∃ a t, a ::ₘ t = s ∧ t.card = n

Tactic:
induction s using Multiset.induction generalizing n with

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

Goal state before:
pp: case neg
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

Tactic:
rw [← Ne, hl] at hx

Goal state after:
case neg
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ xs.Disjoint ys.dedup

Tactic:
intro a hx hy

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
a : α
hx : a ∈ xs
hy : a ∈ ys.dedup
⊢ False
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x ++ [y.get ⟨x.length, hl⟩] <+: y

Tactic:
use y.drop (x.length + 1)
  nth_rw 1 [List.prefix_iff_eq_take.mp h]
  convert! List.take_append_drop (x.length + 1) y using 2
  rw [← List.take_concat_get, List.concat_eq_append]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ (s.ndinter t).Nodup

Tactic:
exact d.filter _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ IsDirectedOrder (Finset α)

Tactic:
infer_instance

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

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

Tactic:
have : b ∈ s.erase a := mem_erase.2 ⟨hab.symm, hb⟩

Goal state after:
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ ∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
⊢ a * (b / c) ≤ a * b / c

Tactic:
by
  obtain rfl | hlt : c = 0 ∨ 0 < c := by lia
  · simp
  · rw [Int.le_ediv_iff_mul_le hlt, Int.mul_assoc]
    exact Int.mul_le_mul_of_nonneg_left (Int.ediv_mul_le b (Int.ne_of_gt hlt)) ha

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

Goal state before:
pp: n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
⊢ p.predAbove a ≤ p.predAbove b

Tactic:
dsimp [predAbove]
  split_ifs with ha hb hb
  all_goals simp only [le_iff_val_le_val, val_pred]
  · exact pred_le_pred H
  · calc
      _ ≤ _ := Nat.pred_le _
      _ ≤ _ := H
  · exact le_pred_of_lt ((not_lt.mp ha).trans_lt hb)
  · exact H

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
i : ℕ
hi : i ∈ range n
⊢ ∀ ⦃a₂ : ↥(range n)⦄, (fun i ↦ f ↑i ⋯) ⟨i, hi⟩ = (fun i ↦ f ↑i ⋯) a₂ → ⟨i, hi⟩ = a₂

Tactic:
⟨j, hj⟩

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
i : ℕ
hi : i ∈ range n
j : ℕ
hj : j ∈ range n
⊢ (fun i ↦ f ↑i ⋯) ⟨i, hi⟩ = (fun i ↦ f ↑i ⋯) ⟨j, hj⟩ → ⟨i, hi⟩ = ⟨j, hj⟩
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n✝ m n : ℕ
⊢ NeZero (n + 1)

Tactic:
infer_instance

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ i ≤ ↑n

Tactic:
rw [Fin.natCast_eq_last]
  exact Fin.le_last i

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ a.castSucc < b.succ ↔ a ≤ b

Tactic:
castSucc_lt_succ_iff

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f ↔ ∀ (i : Fin n), r (f i.castSucc) (f i.succ)

Tactic:
constructor
  · intro H i
    exact H i.castSucc_lt_succ
  · refine fun H i => Fin.induction (fun h ↦ ?_) ?_
    · simp at h
    · intro j ihj hij
      rw [← le_castSucc_iff] at hij
      obtain hij | hij := (le_def.1 hij).eq_or_lt
      · obtain rfl := Fin.ext hij
        exact H _
      · exact _root_.trans (ihj hij) (H j)

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ b.castSucc < a.succ ↔ b ≤ a

Tactic:
castSucc_lt_succ_iff

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ b ≤ a ↔ b ≤ a
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Fin 0 → Sort u
⊢ Unique ((i : Fin 0) → α i)

Tactic:
infer_instance

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

Goal state before:
pp: case inl.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc ≤ (i.pred ⋯).castSucc

Tactic:
rwa [le_castSucc_iff, succ_pred]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ 2 < #univ ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
two_lt_card_iff,

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ (∃ a b c, a ∈ univ ∧ b ∈ univ ∧ c ∈ univ ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 2 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
two_lt_card_iff,

Goal state after:
α : Type u_1
s : Finset α
⊢ (∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c
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:
intro

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

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

Goal state before:
pp: case cons_cons.inl
α : Type u_1
l l' l₁✝ l₂✝ : List α
y : α
h : l₁✝ <+ l₂✝
IH : y ∈+ l₁✝ → y ∈+ l₂✝
hx : y ∈ l₁✝
⊢ y = y ∧ y ∈ l₂✝ ∨ y ∈+ l₂✝

pp: case cons_cons.inr
α : Type u_1
l : List α
x : α
l' l₁✝ l₂✝ : List α
y : α
h : l₁✝ <+ l₂✝
IH : x ∈+ l₁✝ → x ∈+ l₂✝
hx : x ∈+ l₁✝
⊢ y = x ∧ x ∈ l₂✝ ∨ x ∈+ l₂✝

Tactic:
· simp [h.subset hx]

Goal state after:
case cons_cons.inr
α : Type u_1
l : List α
x : α
l' l₁✝ l₂✝ : List α
y : α
h : l₁✝ <+ l₂✝
IH : x ∈+ l₁✝ → x ∈+ l₂✝
hx : x ∈+ l₁✝
⊢ y = x ∧ x ∈ l₂✝ ∨ x ∈+ l₂✝
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
i j : ℕ
⊢ #(g i) - 1 = #(g j) - 1 ↔ g i = g j

Tactic:
wlog hij : j ≤ i generalizing i j

Goal state after:
case inr
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this✝ : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
i j : ℕ
this : ∀ (i j : ℕ), j ≤ i → (#(g i) - 1 = #(g j) - 1 ↔ g i = g j)
hij : ¬j ≤ i
⊢ #(g i) - 1 = #(g j) - 1 ↔ g i = g j

α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
i j : ℕ
hij : j ≤ i
⊢ #(g i) - 1 = #(g j) - 1 ↔ g i = g j
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
⊢ Nonempty α

Tactic:
infer_instance

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

Goal state before:
pp: case pos.refl
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
⊢ ∀ (H₂ : i.succAbove j = i.succAbove j), H₂ ▸ p j = p j

Tactic:
intro

Goal state after:
case pos.refl
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
H₂✝ : i.succAbove j = i.succAbove j
⊢ H₂✝ ▸ p j = p j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg.refl
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
⊢ ∀ (H₂ : i.succAbove j = i.succAbove j), H₂ ▸ p j = p j

Tactic:
intro

Goal state after:
case neg.refl
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
H₂✝ : i.succAbove j = i.succAbove j
⊢ H₂✝ ▸ p j = p j
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case pos
α : 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
⊢ ↑(f ⟨i, hi⟩) < ↑(f ⟨j, hj⟩)

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
⊢ ↑(f ⟨i, hi⟩) < j + l'.length

pp: case pos
α : 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 < ↑(f ⟨j, hj⟩)

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:
· rwa [Fin.val_fin_lt, f.lt_iff_lt]

Goal state after:
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
⊢ ↑(f ⟨i, hi⟩) < j + l'.length

case pos
α : 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 < ↑(f ⟨j, hj⟩)

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
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
val✝¹ : Fintype ↑s
val✝ : Fintype ↑t
⊢ Finite ↑(s ∪ t)

Tactic:
infer_instance

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

Goal state before:
pp: case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ Finite ↑{a | a ∈ s ∧ p a}

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑{x | x ∈ s ∧ x ∈ t}

Tactic:
infer_instance

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

Goal state before:
pp: case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ Finite ↑(f '' s)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : Std.Trichotomous r
a : α
l₁ l₂ : List α
hab : ¬Lex r (a :: l₁) (a :: l₂)
hba : ¬Lex r (a :: l₂) (a :: l₁)
⊢ a :: l₁ = a :: l₂

Tactic:
aux l₁ l₂ (mt cons hab) (mt cons hba)

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : Std.Trichotomous r
a : α
l₁ l₂ : List α
hab : ¬Lex r (a :: l₁) (a :: l₂)
hba : ¬Lex r (a :: l₂) (a :: l₁)
⊢ a :: l₂ = a :: l₂
Module: Mathlib.Data.List.Range

Goal state before:
pp: case cons
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (a :: l).ranges

Tactic:
simp only [ranges, pairwise_cons]
    constructor
    · intro s hs
      obtain ⟨s', _, rfl⟩ := mem_map.mp hs
      intro u hu
      rw [mem_map]
      rw [mem_range] at hu
      lia
    · rw [pairwise_map]
      apply Pairwise.imp _ hl
      intro u v
      apply disjoint_map
      exact fun u v => Nat.add_left_cancel

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I).PairwiseDisjoint f
⊢ ⋃₀ ↑(I.disjiUnion f hf) = ⋃ a ∈ I, ⋃₀ ↑(f a)

Tactic:
by
  ext
  simp only [coe_disjiUnion, Set.mem_sUnion, Set.mem_iUnion, mem_coe, exists_prop]
  tauto

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

Goal state before:
pp: case cons
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
m : Multiset α
ih : filter p m = m.bind fun a ↦ if p a then {a} else 0
⊢ filter p (a ::ₘ m) = (a ::ₘ m).bind fun a ↦ if p a then {a} else 0

Tactic:
| cons a m ih =>

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

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
s : Multiset M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
l : List M
⊢ (map ⇑f ⟦l⟧).prod = f (prod ⟦l⟧)

Tactic:
simp only [l.prod_hom f, quot_mk_to_coe, map_coe, prod_coe]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → Option β
a : α
m : Multiset α
ih : filterMap f m = m.bind fun a ↦ (Option.map singleton (f a)).getD 0
⊢ filterMap f (a ::ₘ m) = (a ::ₘ m).bind fun a ↦ (Option.map singleton (f a)).getD 0

Tactic:
| cons a m ih =>

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
⊢ l.offDiag.Nodup

Tactic:
rw [nodup_iff_count_le_one]

Goal state after:
α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
⊢ ∀ (a : α × α), List.count a l.offDiag ≤ 1
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ 1 + List.count a l < List.count a l * List.count a l

Tactic:
calc
    1 + l.count a < l.count a + l.count a := by simpa
    _ ≤ l.count a * l.count a := by
      rw [← Nat.two_mul]
      exact Nat.mul_le_mul_right _ h

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

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
H : (Nonempty β → Finite α) ∧ (Nonempty α → Finite β)
this✝ : Finite α
this : Finite β
⊢ Finite (α × β)

Tactic:
infer_instance

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

Goal state before:
pp: ι : Sort u_4
π : ι → Sort u_5
i : ι
inst✝¹ : Infinite (π i)
inst✝ : ∀ (i : ι), Nonempty (π i)
⊢ Infinite ((i : ι) → π i)

Tactic:
by
  classical
  let ⟨m⟩ := @Pi.instNonempty ι π _
  exact Infinite.of_injective _ (update_injective m i)

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

Goal state before:
pp: m : ℕ
⊢ 2 * m + 1 = m + 1 + m

Tactic:
Nat.add_comm m 1,

Goal state after:
m : ℕ
⊢ 2 * m + 1 = 1 + m + m
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
γ : α → Type u_3
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
f : (a : α) → γ a → δ a
s : (a : α) → Finset (γ a)
⊢ (piFinset fun a ↦ image (f a) (s a)) = image (fun b a ↦ f a (b a)) (piFinset s)

Tactic:
ext; simp only [mem_piFinset, mem_image, Classical.skolem, forall_and, funext_iff]

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

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

Tactic:
by
  ext
  simp [Fin.exists_iff_castSucc, or_comm]

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

Goal state before:
pp: case cons
α : 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
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ f ∈ (a ::ₘ m).pi t ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1

Tactic:
| cons a m ih =>

Goal state after:
case cons
α : 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
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ f ∈ (a ::ₘ m).pi t ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Finite (α × β)

Tactic:
infer_instance

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

Goal state before:
pp: case inl
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h✝ : IsEmpty (α ↪ β)
⊢ Finite (α ↪ β)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑((fun x ↦ f x.1 x.2) '' s ×ˢ t)

Tactic:
infer_instance

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

Goal state before:
pp: case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ DecidablePred fun x ↦ x = 1

Tactic:
infer_instance

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

Goal state before:
pp: case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : DecidablePred fun x ↦ x ∈ s ^ n
⊢ DecidablePred fun x ↦ x ∈ s ^ n * s

Tactic:
infer_instance

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s : Set M
p q : Subsemigroup M
h : p.carrier = q.carrier
⊢ p = q

Tactic:
cases p; cases q; congr

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : Nonempty ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

Tactic:
· exact hf.injective.injOn.image_iInter_eq

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

Goal state before:
pp: M' : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Monoid M'
S : Submonoid M'
⊢ IsScalarTower (↥S) M' M'

Tactic:
infer_instance

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : ∃ g, ↑H = {g}
g : G
hg : ↑H = {g}
⊢ Subsingleton ↑{g}

Tactic:
infer_instance

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

Goal state before:
pp: case mem.inv
G : Type u_1
inst✝ : Group G
k : Set G
p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : x ∈ closure k), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : x ∈ closure k), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : x ∈ closure k) (hy : y ∈ closure k) (hz : z ∈ closure k),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : y ∈ closure k) (hz : z ∈ closure k) (hx : x ∈ closure k),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x y⁻¹ hx ⋯
x y z : G
hz : z ∈ k
x✝ : G
hx✝ : x✝ ∈ closure k
h : p x✝ z hx✝ ⋯
⊢ p x✝⁻¹ z ⋯ ⋯

Tactic:
| inv _ _ h =>

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

Goal state before:
pp: case inv
G : Type u_1
inst✝ : Group G
k : Set G
p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : x ∈ closure k), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : x ∈ closure k), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : x ∈ closure k) (hy : y ∈ closure k) (hz : z ∈ closure k),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : y ∈ closure k) (hz : z ∈ closure k) (hx : x ∈ closure k),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : x ∈ closure k
x✝ : G
hx✝ : x✝ ∈ closure k
h : p x x✝ hx hx✝
⊢ p x x✝⁻¹ hx ⋯

Tactic:
| inv _ _ h =>

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x : ↥(IsUnit.submonoid M)
⊢ ⟨↑(IsUnit.unit ⋯), ⋯⟩ = x

Tactic:
IsUnit.unit_spec

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x y : Mˣ
⊢ ⟨↑(x * y), ⋯⟩ = ⟨↑x, ⋯⟩ * ⟨↑y, ⋯⟩

Tactic:
by simp_rw [Units.val_mul]; rfl

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

Goal state before:
pp: ⊢ Countable { n // 0 < n }

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
⊢ Encodable ↑(Set.range Encodable.encode)

Tactic:
infer_instance

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ map (↑(MulAut.conj h)) (closure s) = closure s

Tactic:
MonoidHom.map_closure

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ closure (⇑↑(MulAut.conj h) '' s) = closure s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ (normalClosure s).Normal

Tactic:
infer_instance

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
ha : a ∈ t
hb : b ∈ s
⊢ ((a * b⁻¹) • s ∩ t).Nonempty

Tactic:
exact ⟨a, mem_inter (mem_smul_set.mpr ⟨b, hb, by simp⟩) ha⟩

Goal state after: