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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ (a ::ₘ 0).toFinset = {a}

Tactic:
toFinset_cons,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ insert a (toFinset 0) = {a}
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.toFinset = ∅ ↔ l = []

Tactic:
cases l

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].toFinset = ∅ ↔ [] = []

case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).toFinset = ∅ ↔ head✝ :: tail✝ = []
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : a ∈ s
ht : a ∉ t
⊢ s.erase a = t ↔ s = insert a t

Tactic:
by
  aesop

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∉ t₁) s) ⊆ t₂ \ t₁

Tactic:
intro x

Goal state after:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ ↑(filter (fun x ↦ x ∉ t₁) s) → x ∈ t₂ \ t₁
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ (piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = g ⟨i, hi⟩

Tactic:
simp_rw [piFinsetUnion, sumPiEquivProdPi, piCongrLeft, piCongrLeft', trans_apply, coe_fn_symm_mk]
  rw! [Finset.union_symm_right h hi hi']
  rfl

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ range ⇑i.succAboveOrderEmb = {i}ᶜ

Tactic:
by
  aesop

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

Goal state before:
pp: case zero
p i : Fin 0
h : p < i
⊢ i.castSucc ≠ 0

pp: case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : p < i
⊢ i.castSucc ≠ 0

Tactic:
· exact i.elim0

Goal state after:
case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : p < i
⊢ i.castSucc ≠ 0
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ #s = #t

Tactic:
by
  refine card_nbij' e e.symm ?_ ?_ ?_ ?_ <;> simp [hst, Set.MapsTo, Set.LeftInvOn, Set.RightInvOn]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f ↑s ↑t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
⊢ Set.InjOn f ↑s

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f ↑s ↑t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
x : α
⊢ x ∈ ↑s → ∀ ⦃x₂ : α⦄, x₂ ∈ ↑s → f x = f x₂ → x = x₂
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case cast
n : ℕ
i✝ : Fin n
ha : i✝.castSucc ≠ last n
⊢ (i✝.castSucc.castPred ha).succ = i✝.castSucc + 1

Tactic:
castPred_castSucc,

Goal state after:
case cast
n : ℕ
i✝ : Fin n
ha : i✝.castSucc ≠ last n
⊢ i✝.succ = i✝.castSucc + 1
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ f 0 :: (ofFn fun i ↦ f i.castSucc.succ).concat (f (Fin.last n.succ)) =
    f 0 :: (ofFn fun i ↦ f i.succ.castSucc).concat (f (Fin.last (n + 1)))

Tactic:
simp only [succ_eq_add_one, Fin.castSucc_succ]

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

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = m - ↑b + ↑a + n - m

Tactic:
have h' : a.val < b.val := h

Goal state after:
n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
h' : ↑a < ↑b
⊢ n - ↑b + ↑a = m - ↑b + ↑a + n - m
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i h, (ofFn f)[i] = b ∧ ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true
hpb : p b = true
i : ℕ
hi : i < (ofFn f).length
hfb : (ofFn f)[i] = b
h : ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true
j : Fin n
hj : j < ⟨i, ⋯⟩
⊢ ¬p (f j) = true

Tactic:
simpa using! h j hj

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

Goal state before:
pp: case zero
inst✝ : NeZero 0
i : Fin 0
⊢ i.predAbove 0 = 0

pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i : Fin (n✝ + 1)
⊢ i.predAbove 0 = 0

Tactic:
· exact i.elim0

Goal state after:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i : Fin (n✝ + 1)
⊢ i.predAbove 0 = 0
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case neg
n : ℕ
p i : Fin n
hi : ¬i ≤ p
⊢ ∃ a, p.predAbove a = i

Tactic:
Fin.not_le

Goal state after:
case neg
n : ℕ
p i : Fin n
hi : p < i
⊢ ∃ a, p.predAbove a = i
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
S₁ S₂ : Finset ι
h : Disjoint S₁ S₂
h' : #S₁ + #S₂ = #univ
⊢ #S₁ᶜ ≤ #S₂

Tactic:
simp [← Nat.add_le_add_iff_left (n := S₁.card), h']

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
⊢ Surjective f

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
⊢ ∃ a, f a = x
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
⊢ ∃ n ≤ #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s

Tactic:
obtain ⟨n, hn', hn⟩ := image_iterate_stabilises_lt_card hs hs₀

Goal state after:
case inr
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
n : ℕ
hn' : n < #s
hn : ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s
⊢ ∃ n ≤ #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s
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
a b : ℕ
⊢ a + 1 ≤ b + 1 ↔ a ≤ b

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
a b : ℕ
⊢ f 0 + 1 ≤ f (b + 1)

Tactic:
Nat.succ_le_succ_iff

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
a b : ℕ
⊢ a ≤ b ↔ a ≤ b

α : 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
a b : ℕ
⊢ f 0 + 1 ≤ f (b + 1)
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.8
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Trunc (α ≃ Fin (card α))

Tactic:
by
  unfold card Finset.card
  exact
    Quot.recOnSubsingleton
      (motive := fun s : Multiset α =>
        (∀ x : α, x ∈ s) → s.Nodup → Trunc (α ≃ Fin (Multiset.card s)))
      univ.val
      (fun l (h : ∀ x : α, x ∈ l) (nd : l.Nodup) => Trunc.mk (nd.getEquivOfForallMemList _ h).symm)
      mem_univ_val univ.2

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

Goal state before:
pp: case pos
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 ((i.succAbove j).castPred H₁) = i.succAbove j), H₂ ▸ p ((i.succAbove j).castPred H₁) = p j

Tactic:
generalize hk : castPred ((succAbove i) j) H₁ = k

Goal state after:
case pos
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
k : Fin n
hk : (i.succAbove j).castPred H₁ = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
⊢ p.removeNth (p.insertNth a f) = f

Tactic:
by ext; unfold removeNth; simp

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

Goal state before:
pp: α : Type u
s : Set α
h : s.Finite
⊢ ∃ s', ↑s' = s

Tactic:
by
  cases h.nonempty_fintype
  exact ⟨s.toFinset, s.coe_toFinset⟩

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

Goal state before:
pp: n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Tactic:
rcases lt_trichotomy (x : ℕ) j with (h | h | h)

Goal state after:
case inl
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑x < ↑j
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

case inr.inl
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑x = ↑j
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

case inr.inr
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑j < ↑x
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x
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 : β}, x ≥ min y z ↔ x ≥ y ∨ x ≥ z

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x : β
⊢ ∀ {y z : β}, x ≥ min y z ↔ x ≥ y ∨ x ≥ z
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 : β}, x > min y z ↔ x > y ∨ x > z

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x : β
⊢ ∀ {y z : β}, x > min y z ↔ x > y ∨ x > z
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 : β}, x ≥ max y z ↔ x ≥ y ∧ x ≥ z

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x : β
⊢ ∀ {y z : β}, x ≥ max y z ↔ x ≥ y ∧ x ≥ z
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 : β}, x > max y z ↔ x > y ∧ x > z

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x : β
⊢ ∀ {y z : β}, x > max y z ↔ x > y ∧ x > z
Module: Mathlib.Data.List.Pairwise

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

Tactic:
cases l

Goal state after:
case nil
α : Type u_1
R : α → α → Prop
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
h : Pairwise R []
ha : a ∈ []
⊢ R [].head! a

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

Goal state before:
pp: case refine_1.inr
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ Lex r (a :: l₁) (a :: l₂)

Tactic:
exact Lex.cons h

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
c : α
l₁ l₂ : List α
⊢ IsChain R (l₁ ++ c :: l₂) ↔ IsChain R (l₁ ++ [c]) ∧ IsChain R (c :: l₂)

Tactic:
by
  induction l₁ using twoStepInduction generalizing l₂ with grind

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
⊢ IsChain R (a :: l) ↔ l = [] ∨ Forall₂ R (a :: l.dropLast) l

Tactic:
cases l

Goal state after:
case nil
α : Type u_1
R : α → α → Prop
a : α
⊢ IsChain R [a] ↔ [] = [] ∨ Forall₂ R (a :: [].dropLast) []

case cons
α : Type u_1
R : α → α → Prop
a head✝ : α
tail✝ : List α
⊢ IsChain R (a :: head✝ :: tail✝) ↔ head✝ :: tail✝ = [] ∨ Forall₂ R (a :: (head✝ :: tail✝).dropLast) (head✝ :: tail✝)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
⊢ l.rotate' 0 = l

Tactic:
cases l

Goal state after:
case nil
α : Type u
⊢ [].rotate' 0 = []

case cons
α : Type u
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).rotate' 0 = head✝ :: tail✝
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ l₃ : List α
h₁ : IsChain R (l₁ ++ l₂)
h₂ : IsChain R (l₂ ++ l₃)
hn : l₂ ≠ []
⊢ ∀ (x : α), x ∈ (l₁ ++ l₂).getLast? → ∀ (y : α), y ∈ l₃.head? → R x y

Tactic:
simpa only [getLast?_append_of_ne_nil _ hn] using (isChain_append.1 h₂).2.2

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (l.rotate n).length = l.length

Tactic:
by
  rw [rotate_eq_rotate', length_rotate']

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

Goal state before:
pp: α : Type u_3
R : α → α → Prop
l : List α
v : α
hl : IsChain R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
⊢ IsChain R (v :: l)

Tactic:
cases l

Goal state after:
case nil
α : Type u_3
R : α → α → Prop
v : α
hl : IsChain R []
hv : ∀ (lne : [] ≠ []), R v ([].head lne)
⊢ IsChain R [v]

case cons
α : Type u_3
R : α → α → Prop
v head✝ : α
tail✝ : List α
hl : IsChain R (head✝ :: tail✝)
hv : ∀ (lne : head✝ :: tail✝ ≠ []), R v ((head✝ :: tail✝).head lne)
⊢ IsChain R (v :: head✝ :: tail✝)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse =
    (x :: l).reverse.rotate
      ((x :: l).reverse.length - ((x :: l).reverse.length - n % (x :: l).reverse.length) % (x :: l).reverse.length +
        ((x :: l).reverse.length - n % (x :: l).reverse.length))

Tactic:
rw [Nat.mod_eq_of_lt, Nat.sub_add_cancel, rotate_length]
      · exact Nat.sub_le _ _
      · exact Nat.sub_lt (by simp) (by simp_all! [k])

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

Goal state before:
pp: case cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ (hd :: tl).rotate n ~r hd :: tl

Tactic:
· use (hd :: tl).length * n - n
    rw [rotate_rotate, Nat.add_sub_cancel', rotate_length_mul]
    exact Nat.le_mul_of_pos_left _ (by simp)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
a : α
⊢ (insert a s).biUnion t = t a ∪ s.biUnion t

Tactic:
by
  aesop

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

Goal state before:
pp: α : Type u
l : List α
k : ℕ
⊢ (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length

Tactic:
cases l

Goal state after:
case nil
α : Type u
k : ℕ
⊢ ([].rotate k).cyclicPermutations.length = ([].cyclicPermutations.rotate k).length

case cons
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ ((head✝ :: tail✝).rotate k).cyclicPermutations.length = ((head✝ :: tail✝).cyclicPermutations.rotate k).length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ l.rotate ((↑⟨n, hn⟩ + k) % l.length) = l.cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % l.cyclicPermutations.length, ⋯⟩

Tactic:
cases l

Goal state after:
case nil
α : Type u
k n : ℕ
this : ([].rotate k).cyclicPermutations.length = ([].cyclicPermutations.rotate k).length
hn : n < ([].rotate k).cyclicPermutations.length
hn' : n < ([].cyclicPermutations.rotate k).length
⊢ [].rotate ((↑⟨n, hn⟩ + k) % [].length) = [].cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % [].cyclicPermutations.length, ⋯⟩

case cons
α : Type u
k n : ℕ
head✝ : α
tail✝ : List α
this : ((head✝ :: tail✝).rotate k).cyclicPermutations.length = ((head✝ :: tail✝).cyclicPermutations.rotate k).length
hn : n < ((head✝ :: tail✝).rotate k).cyclicPermutations.length
hn' : n < ((head✝ :: tail✝).cyclicPermutations.rotate k).length
⊢ (head✝ :: tail✝).rotate ((↑⟨n, hn⟩ + k) % (head✝ :: tail✝).length) =
    (head✝ :: tail✝).cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % (head✝ :: tail✝).cyclicPermutations.length, ⋯⟩
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
⊢ Injective l.cyclicPermutations.get

Tactic:
rintro ⟨i, hi⟩ ⟨j, hj⟩ h

Goal state after:
case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi : i < l.cyclicPermutations.length
j : ℕ
hj : j < l.cyclicPermutations.length
h : l.cyclicPermutations.get ⟨i, hi⟩ = l.cyclicPermutations.get ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
⊢ (n + 1).choose (k + 1) = 0

Tactic:
have hnk1 : n < k + 1 := lt_of_succ_lt hk

Goal state after:
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ (n + 1).choose (k + 1) = 0
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
by
  have e : (n + 1) * choose n k = choose n (k + 1) * (k + 1) + choose n k * (k + 1) := by
    rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, add_one_mul_choose_eq]
  rw [← Nat.sub_eq_of_eq_add e, Nat.mul_comm, ← Nat.mul_sub_left_distrib, Nat.add_sub_add_right]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pretransitive

Goal state before:
pp: G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
⊢ ∀ (x y : X), ∃ g, g • x = y

Tactic:
intro x

Goal state after:
G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
x : X
⊢ ∀ (y : X), ∃ g, g • x = y
Module: Mathlib.Data.Finite.Prod

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

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Finite (α × β)
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case refine_2
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ Fintype.card ↑(S ^ n) ≤ Fintype.card ↑(S ^ n * {a})

Tactic:
· convert! key a (S ^ n) (S ^ n * { a }) fun b hb ↦ Set.mul_mem_mul hb (Set.mem_singleton a)

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

Goal state before:
pp: case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
h₂ : S ^ n * {a} = S ^ (n + 1)
⊢ ∀ ⦃x : G⦄, x ∈ S ^ (n + 1) → x * a * a⁻¹ ∈ S ^ (n + 1)

Tactic:
intro x

Goal state after:
case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
h₂ : S ^ n * {a} = S ^ (n + 1)
x : G
⊢ x ∈ S ^ (n + 1) → x * a * a⁻¹ ∈ S ^ (n + 1)
Module: Mathlib.Algebra.Group.Action.End

Goal state before:
pp: G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
⊢ ∀ (x y : α), ∃ g, g • x = y

Tactic:
intro x

Goal state after:
G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
x : α
⊢ ∀ (y : α), ∃ g, g • x = y
Module: Mathlib.Algebra.Group.Action.End

Goal state before:
pp: G : Type u_1
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ toPerm 1 = 1

Tactic:
by
  aesop

Goal state after:
Module: Mathlib.Algebra.Group.Action.End

Goal state before:
pp: G : Type u_1
α : Type u_5
inst✝¹ : AddGroup G
inst✝ : AddAction G α
⊢ toPerm 0 = 1

Tactic:
by
  aesop

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
⊢ ∀ (a b : M), a = b

Tactic:
intro x

Goal state after:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
x : M
⊢ ∀ (b : M), x = b
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Set α
S : Set (Set β)
f : α → β → γ
⊢ image2 f t (⋂₀ S) ⊆ ⋂ s ∈ S, image2 f t s

Tactic:
by
  aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
S : Set (Set α)
t : Set β
f : α → β → γ
⊢ image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

Tactic:
by
  aesop

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)
⊢ InjOn f (⋃ i, s i)

Tactic:
intro x

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 : α
⊢ x ∈ ⋃ i, s i → ∀ ⦃x₂ : α⦄, x₂ ∈ ⋃ i, s i → f x = f x₂ → x = x₂
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case left
α : 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 → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i

Tactic:
intro x

Goal state after:
case left
α : 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 → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i
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

Goal state after:
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
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
S : Set (Set α)
t : Set β
⊢ image2 f (⋃₀ S) t = ⋃ s ∈ S, image2 f s t

Tactic:
by
  aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
⊢ image2 f s (⋃₀ T) = ⋃ t ∈ T, image2 f s t

Tactic:
by
  aesop

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

Goal state before:
pp: case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ ↑(closure s) ⊆ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
intro x

Goal state after:
case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
⊢ x ∈ ↑(closure s) → x ∈ {1} ∪ ↑(Subsemigroup.closure s)