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

Goal state before:
pp: r : ℕ → ℕ → Prop
n a : ℕ
⊢ IsChain r (a :: range n.succ) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
rw [range_succ_eq_map, isChain_cons_cons, and_congr_right_iff,
    ← isChain_range_succ, range_succ_eq_map]

Goal state after:
r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (IsChain r (0 :: map succ (range n)) ↔ IsChain r (0 :: map succ (range n)))
Module: Mathlib.Data.List.Range

Goal state before:
pp: r : ℕ → ℕ → Prop
n a : ℕ
⊢ IsChain r (a :: range n.succ) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
by
  rw [range_succ_eq_map, isChain_cons_cons, and_congr_right_iff,
    ← isChain_range_succ, range_succ_eq_map]
  exact fun _ => Iff.rfl

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
x : α
l : List α
h : IsChain R (x :: l)
y : α
hy : y ∈ l.head?
⊢ R x y

Tactic:
rw [← cons_head?_tail hy] at h

Goal state after:
α : Type u_1
R : α → α → Prop
x : α
l : List α
y : α
h : IsChain R (x :: y :: l.tail)
hy : y ∈ l.head?
⊢ R x y
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons.e_a
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).sum

Tactic:
by_cases ha : a ∈ as

Goal state after:
case pos
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : a ∈ as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).sum

case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : ¬a ∈ as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).sum
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons.cons.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun x1 x2 ↦ x1 > x2) (a' :: as)
hmas : b :: bs = a' :: as
⊢ b ≤ a'

Tactic:
· simp_all only [List.cons.injEq, le_refl]

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

Goal state before:
pp: α : Type u_3
f : α → α
l : List α
hl : IsChain (fun x y ↦ f x = y) l
i : ℕ
hi : i < l.length
⊢ f^[i] l[0] = l[i]

Tactic:
by
  induction i with
  | zero => rfl
  | succ i h =>
    rw [Function.iterate_succ', Function.comp_apply, h (by lia)]
    rw [List.isChain_iff_getElem] at hl
    apply hl

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ l.prod = (map id l).prod

Tactic:
map_id

Goal state after:
M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ l.prod = l.prod
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
b : β
⊢ DependsOn (fun x ↦ b) ∅

Tactic:
simp [DependsOn]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ ∀ (x : (a : α) → a ∈ univ → δ a),
    (∀ (a : α), x a ⋯ ∈ t a) → { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } x = f → ∀ (a : α), f a ∈ t a

Tactic:
rintro g hg hgf a

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf : { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } g = f
a : α
⊢ f a ∈ t a
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: a c : ℕ
⊢ a.choose c ≤ a.succ.choose c

Tactic:
cases c <;> grind

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (uncurry f '' s ×ˢ t).Infinite
⊢ (s ×ˢ t).Infinite

Tactic:
exact h.of_image _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
i : ι
hi : f x ∈ U i
⊢ x = y

Tactic:
injection @H i ⟨x, hi⟩ ⟨y, show f y ∈ U i from e ▸ hi⟩ (Subtype.ext e)

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
x : M
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
by
  simp only [iInf, mem_sInf, Set.forall_mem_range]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_9
κ : Sort u_10
f : ι → Set α
g : κ → Set α
⊢ (⋂ i, f i) ∪ ⋂ j, g j = ⋂ i, ⋂ j, f i ∪ g j

Tactic:
iInter_union,

Goal state after:
α : Type u_1
ι : Sort u_9
κ : Sort u_10
f : ι → Set α
g : κ → Set α
⊢ ⋂ i, f i ∪ ⋂ j, g j = ⋂ i, ⋂ j, f i ∪ g j
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
ι₁ : Sort u_9
κ₁ : Sort u_10
ι₂ : ι₁ → Sort u_11
k₂ : κ₁ → Sort u_12
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
⊢ (⋂ i₁, ⋂ i₂, f i₁ i₂) ∪ ⋂ j₁, ⋂ j₂, g j₁ j₂ = ⋂ i₁, ⋂ i₂, ⋂ j₁, ⋂ j₂, f i₁ i₂ ∪ g j₁ j₂

Tactic:
iInter_union,

Goal state after:
α : Type u_1
ι₁ : Sort u_9
κ₁ : Sort u_10
ι₂ : ι₁ → Sort u_11
k₂ : κ₁ → Sort u_12
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
⊢ ⋂ i, ⋂ i_1, f i i_1 ∪ ⋂ j₁, ⋂ j₂, g j₁ j₂ = ⋂ i₁, ⋂ i₂, ⋂ j₁, ⋂ j₂, f i₁ i₂ ∪ g j₁ j₂
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
x : M
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
by
  simp only [iInf, mem_sInf, Set.forall_mem_range]

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Tactic:
by cases n <;> aesop

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
p₁ p₂ : Submonoid M
⊢ (∀ ⦃x : M⦄, x ∈ p₁ ∧ x ∈ p₂ → x ∈ ⊥) ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1

Tactic:
and_imp,

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
p₁ p₂ : Submonoid M
⊢ (∀ ⦃x : M⦄, x ∈ p₁ → x ∈ p₂ → x ∈ ⊥) ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → Inv (α i)
s : Set ι
t : (i : ι) → Set (α i)
⊢ (s.pi t)⁻¹ = s.pi fun i ↦ (t i)⁻¹

Tactic:
ext x; simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
S : ι → Subgroup G
x : G
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
by
  simp only [iInf, mem_sInf, Set.forall_mem_range]

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

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (MonoidHom.id N) H = H

Tactic:
map_id

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ H = H
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (MonoidHom.id G) K = K

Tactic:
map_id

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ K = K
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:
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_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_5
inst✝² : Group N
P : Type u_6
inst✝¹ : Group P
inst✝ : IsMulTorsionFree G
n : ℕ
hn : n ≠ 0
a b : ↥H
⊢ (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b → a = b

Tactic:
have := pow_left_injective hn (M := G) (a₁ := a) (a₂ := b)
    dsimp at *
    norm_cast at this

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : ⇑(MulAut.conj g) '' s = s
⊢ map (↑(MulAut.conj g)) (closure s) = closure s

Tactic:
MonoidHom.map_closure,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : ⇑(MulAut.conj g) '' s = s
⊢ closure (⇑↑(MulAut.conj g) '' s) = closure s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_4
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
⊢ x⁻¹ ∈ N

Tactic:
· exact inv_mem ihx

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mpr.of_mul
α : Type u_1
β : Type u_2
f : α → β
head : β
fs : ∃ a, f a = head
tail : FreeMonoid β
ih : ∃ a, (map f) a = tail
⊢ ∃ a, (map f) a = of head * tail

Tactic:
rcases fs with ⟨a, rfl⟩

Goal state after:
case mpr.of_mul
α : Type u_1
β : Type u_2
f : α → β
tail : FreeMonoid β
ih : ∃ a, (map f) a = tail
a : α
⊢ ∃ a_1, (map f) a_1 = of (f a) * tail
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : CommGroup β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
x : α × β
s : Set α
f : F
⊢ x • graphOn (⇑f) s = graphOn (fun a ↦ x.2 / f x.1 * f a) (x.1 • s)

Tactic:
ext ⟨a, b⟩
  simp [mem_smul_set_iff_inv_smul_mem, inv_mul_eq_iff_eq_mul, mul_left_comm _ _⁻¹,
    eq_inv_mul_iff_mul_eq, ← mul_div_right_comm, div_eq_iff_eq_mul, mul_comm b]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : Std.Symm r
inst✝ : ∀ (i : ι), Std.Symm (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b → Lex r s b a

Tactic:
rintro _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩)

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

case right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Symm r
inst✝ : ∀ (i : ι), Std.Symm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
⊢ Lex r s ⟨i✝, b⟩ ⟨i✝, a⟩
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ c ∈ closure {a, b} ↔ ∃ m n, a ^ m * b ^ n = c

Tactic:
by
  rw [← Set.singleton_union, Submonoid.closure_union, mem_sup]
  simp_rw [mem_closure_singleton, exists_exists_eq_and]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s.disjSum t).toLeft = s

Tactic:
ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s.disjSum t).toRight = t

Tactic:
ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ (map (Equiv.sumComm α β).toEmbedding u).toLeft = u.toRight

Tactic:
ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ (map (Equiv.sumComm α β).toEmbedding u).toRight = u.toLeft

Tactic:
ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (image Sum.swap u).toLeft = u.toRight

Tactic:
ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (image Sum.swap u).toRight = u.toLeft

Tactic:
ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∩ v).toLeft = u.toLeft ∩ v.toLeft

Tactic:
ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∩ v).toRight = u.toRight ∩ v.toRight

Tactic:
ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∪ v).toLeft = u.toLeft ∪ v.toLeft

Tactic:
ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∪ v).toRight = u.toRight ∪ v.toRight

Tactic:
ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u \ v).toLeft = u.toLeft \ v.toLeft

Tactic:
ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u \ v).toRight = u.toRight \ v.toRight

Tactic:
ext x; simp

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.revzip.reverse = l.reverse.revzip

Tactic:
rw [← zip_unzip (revzip l).reverse]

Goal state after:
α : Type u
l : List α
⊢ l.revzip.reverse.unzip.fst.zip l.revzip.reverse.unzip.snd = l.reverse.revzip
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
s : Finset α
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
⊢ motive s

Tactic:
induction s using Finset.eraseInduction with | _ s ih
   =>  _ 

Goal state after:
case H
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
⊢ motive s
Module: Mathlib.Data.Multiset.Powerset

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

Tactic:
| cons _ _ IH =>

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
⊢ IsLeast (↑s) i

Tactic:
suffices i = min' s hs by
    rw [this]
    exact isLeast_min' s hs

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
⊢ i = s.min' hs
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
⊢ l₁ ∈ sublistsLen l₁.length (a :: l₂)

Tactic:
rcases l₁ with - | ⟨b, l₁⟩
    · simp
    · rw [length, sublistsLen_succ_cons]
      exact mem_append_left _ IH

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

Goal state before:
pp: case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h : (l₁, l₂) ∈ (l' ++ [a]).sublists.zip (l' ++ [a]).sublists.reverse
⊢ l₁ ++ l₂ ~ l' ++ [a]

Tactic:
rw [sublists_concat, reverse_append, zip_append (by simp), ← map_reverse, zip_map_right,
      zip_map_left] at *

Goal state after:
case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id fun x ↦ x ++ [a]) (l'.sublists.zip l'.sublists.reverse) ++
      map (Prod.map (fun x ↦ x ++ [a]) id) (l'.sublists.zip l'.sublists.reverse)
⊢ l₁ ++ l₂ ~ l' ++ [a]
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset (Option α)
h : none ∉ s
⊢ #(eraseNone s) = #s

Tactic:
by
  classical rw [card_eraseNone_eq_card_erase, erase_eq_of_notMem h]

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

Goal state before:
pp: P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
⊢ P α

Tactic:
obtain ⟨p⟩ :=
    let f_empty := fun i => by convert! h_empty
    let h_option : ∀ {α : Type u} [Fintype α] [DecidableEq α],
          (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α) := by
      rintro α hα - Pα hα'
      convert! h_option α (Pα _)
    @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _))
      f_empty h_option α _ (Classical.decEq α)
  exact p _

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ g (s.sup' H f) = s.sup' H (g ∘ f)

Tactic:
refine H.cons_induction ?_ ?_ <;> intros <;> simp [*]

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

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : i ∉ s
ih : count b (s.sup f) = s.sup fun a ↦ count b (f a)
⊢ count b (f i ⊔ s.sup f) = (insert i s).sup fun a ↦ count b (f a)

Tactic:
sup_eq_union,

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : i ∉ s
ih : count b (s.sup f) = s.sup fun a ↦ count b (f a)
⊢ count b (f i ∪ s.sup f) = (insert i s).sup fun a ↦ count b (f a)
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hdg : Directed (fun x1 x2 ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : Nonempty ι
⊢ iSup f ≤ iSup g

Tactic:
· exact hdf.ciSup_le fun x ↦ hdg.le_ciSup_of_le B x (H x)

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ∀ y ∈ f '' ↑s, ∃ x ∈ Set.range fun i ↦ ⨆ (_ : i ∈ s), f i, y ≤ x

Tactic:
· simp only [Set.mem_image, mem_coe, ciSup_eq_ite, dite_eq_ite, Set.mem_range,
      exists_exists_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    intro i hi
    refine ⟨i, ?_⟩
    simp [hi]

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

Goal state before:
pp: case mpr
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
i : ↑{i | i ∈ I}
H : x ∈ t
⊢ x ∈ t

Tactic:
exact H

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

Goal state before:
pp: case h_option
α : Type u
ι✝ : Sort v
κ✝ : ι✝ → Sort w
inst✝³ : Order.Frame α
inst✝² : Finite ι✝
f✝ : (a : ι✝) → κ✝ a → α
ι : Type v
inst✝¹ : Finite ι
α✝ : Type v
inst✝ : Fintype α✝
h : ∀ {κ : α✝ → Type w} (f : (a : α✝) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
κ : Option α✝ → Type w
f : (a : Option α✝) → κ a → α
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
| h_option h =>

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t ⊆ s

Tactic:
rwa [← sdiff_singleton_eq_self h, sdiff_singleton_subset_iff]

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h✝ : IsEmpty ι
⊢ e (⨆ i, f i) = ⨆ i, e (f i)

pp: case inr
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h✝ : Nonempty ι
⊢ e (⨆ i, f i) = ⨆ i, e (f i)

Tactic:
· simp [map_bot]

Goal state after:
case inr
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h✝ : Nonempty ι
⊢ e (⨆ i, f i) = ⨆ i, e (f i)
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
s : Finset (α ⊕ β)
⊢ s.preimage Sum.inl ⋯ = s.toLeft

Tactic:
ext x; simp

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

Goal state before:
pp: α : Type u
β : Type v
s : Finset (α ⊕ β)
⊢ s.preimage Sum.inr ⋯ = s.toRight

Tactic:
ext x; simp

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a : α
s : Finset α
ha : a ∈ ↑s
⊢ ∃ b, a ≤ b ∧ Maximal (fun x ↦ x ∈ ↑s) b

Tactic:
exact s.exists_le_maximal ha

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
⊢ s.Infinite

Tactic:
inhabit α

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
⊢ s.Infinite
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
hs : ¬BddAbove s
⊢ 0 = Nat.find ⋯

pp: case hnc
s : Set ℕ
hs : ¬BddAbove s
⊢ ¬∃ n, ∀ a ∈ s, a ≤ n

Tactic:
· exact le_antisymm (zero_le _) (find_le trivial)

Goal state after:
case hnc
s : Set ℕ
hs : ¬BddAbove s
⊢ ¬∃ n, ∀ a ∈ s, a ≤ n
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
rw [Nat.sInf_def ⟨m, hm⟩, Nat.sInf_def hp]

Goal state after:
case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ Nat.find ⋯ + n = Nat.find hp
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b c : ℕ
hac : a ≤ c
⊢ image (fun x ↦ c - x) (Ico a b) = Ico (c + 1 - b) (c + 1 - a)

Tactic:
ext x
  simp_rw [mem_image, mem_Ico]
  refine ⟨?_, fun h ↦ ⟨c - x, by lia⟩⟩
  rintro ⟨x, hx, rfl⟩
  lia

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂

Tactic:
simpa [← coe_subset] using Set.Icc_subset_Icc ha hb

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

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
⊢ 1⁻¹ ∈ ↑S

Tactic:
inv_one

Goal state after:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
⊢ 1 ∈ ↑S