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

Goal state before:
pp: α : Type u_1
β : Type u_2
l✝ : List α
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
⊢ l ∈ {l | ∀ (x : α), x ∈ l → x ∈ Set.range c}

Tactic:
exact fun a ha => CanLift.prf a (H a ha)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s - (t + u) = s - t - u

Tactic:
ext; simp [Nat.sub_add_eq]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ (∃ a, s = {a} ∧ f a = b) → map f s = {b}

Tactic:
· rintro ⟨a, rfl, rfl⟩
    simp

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} ↔ ∃ a, s = {a} ∧ f a = b

Tactic:
constructor
  · intro h
    obtain ⟨a, ha⟩ : ∃ a, s = {a} := by rw [← card_eq_one, ← card_map, h, card_singleton]
    refine ⟨a, ha, ?_⟩
    rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]
  · rintro ⟨a, rfl, rfl⟩
    simp

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ take (n + 1) (b :: l) = List.filter (fun a ↦ elem a (take (n + 1) (b :: l))) (b :: l)

Tactic:
rw [take_succ_cons, Nodup.take_eq_filter_mem (Nodup.of_cons hl), filter_cons_of_pos (by simp)]
    congr 1
    refine List.filter_congr ?_
    intro x hx
    have : x ≠ b := fun h => (nodup_cons.1 hl).1 (h ▸ hx)
    simp +contextual [List.mem_filter, this, hx]

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ t + s ≤ s ∪ t + s ∩ t

Tactic:
add_inter_distrib

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ t + s ≤ (s ∪ t + s) ∩ (s ∪ t + t)
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s : Finset α
a : α
⊢ Disjoint {a} s ↔ a ∉ s

Tactic:
by
  simp only [disjoint_left, mem_singleton, forall_eq]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ filter p s = s ↔ ∀ (x : α), x ∈ s → p x

Tactic:
simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ filter p s = ∅ ↔ ∀ ⦃x : α⦄, x ∈ s → ¬p x

Tactic:
simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
j : β
u : Finset α
hj : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
h : f x ≠ j
hi : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) (f x)
⊢ x ∈ t ∧ f x = j

Tactic:
simpa using hj hx

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s t : Finset α
⊢ filter p s = filter p t ↔ ∀ ⦃a : α⦄, p a → (a ∈ s ↔ a ∈ t)

Tactic:
simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ filter p s = filter q s ↔ ∀ ⦃a : α⦄, a ∈ s → (p a ↔ q a)

Tactic:
simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ s = univ ↔ ∀ (x : α), x ∈ s

Tactic:
simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Finset.subtype p s = univ ↔ ∀ ⦃a : α⦄, p a → a ∈ s

Tactic:
simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c✝ : β
c : α → β
p : β → Prop
inst✝ : CanLift β α c p
⊢ ∀ (x : Finset β), (∀ x_1 ∈ x, p x_1) → ∃ y, image c y = x

Tactic:
rintro ⟨⟨l⟩, hd : l.Nodup⟩ hl
    lift l to List α using hl
    exact ⟨⟨l, hd.of_map _⟩, ext fun a => by simp⟩

Goal state after:
Module: Mathlib.Data.Int.DivMod

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

Tactic:
exact Int.mul_le_mul_of_nonneg_left (Int.ediv_mul_le b (Int.ne_of_gt hlt)) ha

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i.rev < j ↔ j.rev < i

Tactic:
rw [← rev_lt_rev, rev_rev]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i < j.rev ↔ j < i.rev

Tactic:
rw [← rev_lt_rev, rev_rev]

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

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

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

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

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

Tactic:
by rw [pred_castSucc_lt_iff, le_def]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
h : i ≠ last n
⊢ i.castPred h = castPred 0 ⋯ ↔ i = 0

Tactic:
castPred_inj

Goal state after:
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
h : i ≠ last n
⊢ i = 0 ↔ i = 0
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ i.predAbove (last (n + 1)) = last n

Tactic:
rw [predAbove_of_castSucc_lt _ _ (castSucc_lt_last _), pred_last]

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
hi : i = last (n + 1)
⊢ (last n).predAbove (last (n + 1)) = last n

Tactic:
predAbove_right_last

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
hi : i = last (n + 1)
⊢ last n = last n
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 1 < #s ↔ s.Nontrivial

Tactic:
by
  rw [← not_iff_not, not_lt, Finset.Nontrivial, ← Set.nontrivial_coe_sort,
    not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton_coe, coe_sort_coe]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ univ = ∅ ↔ IsEmpty α

Tactic:
univ_eq_empty_iff

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ IsEmpty α ↔ IsEmpty α
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: α : Type u_1
l : List α
x : α
h : x ∈+ l
y : α
⊢ l ≠ [y]

Tactic:
induction h with
  | cons_mem h => simp [ne_nil_of_mem h]
  | cons_duplicate h => simp [ne_nil_of_mem h.mem]

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

Goal state before:
pp: case h.inr
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
⊢ ∀ (β : Type u_4) [inst : Fintype β], card β < card α → P β

Tactic:
intro β

Goal state after:
case h.inr
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_4
⊢ ∀ [inst : Fintype β], card β < card α → P β
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
⊢ ∃ f, map f univ = s

Tactic:
by
  obtain ⟨f : α ↪ β, hf⟩ := exists_of_card_le_finset (Nat.le_of_eq hsn)
  use f
  apply Finset.eq_of_subset_of_card_le
  · simp [← coe_subset, hf]
  · simp [← hsn]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

Tactic:
rcases hn.eq_or_lt with hn' | hn'

Goal state after:
case succ.inl
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s = n + 1
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

case succ.inr
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
⊢ ∃ t, s ⊆ t ∧ #t = n + 1
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
⊢ ¬Finite α ↔ Infinite α

Tactic:
not_finite_iff_infinite

Goal state after:
α : Type u
⊢ Infinite α ↔ Infinite α
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:
by
  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.List.Sort

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
f : Fin n → α
⊢ (ofFn f).SortedGE ↔ Antitone f

Tactic:
simp only [sortedGE_iff_antitone_get, Antitone, Fin.forall_iff,
    length_ofFn, get_ofFn, Fin.cast_mk, Fin.mk_le_mk]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
this : Std.Symm fun x y ↦ x ≠ y → R x y
a b : α
h : R a b
x✝ : a ≠ b
⊢ R a b

Tactic:
by exact h

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ a ∈ l.reverse.tail

Tactic:
tail_reverse,

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ a ∈ l.dropLast.reverse
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
m : Multiset ι
⊢ (replicate m.card 1).prod = 1

Tactic:
prod_replicate,

Goal state after:
ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
m : Multiset ι
⊢ 1 ^ m.card = 1
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case succ
α : Type u_1
a : α
s : Multiset α
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ n • s + s
⊢ a ∈ s

Tactic:
mem_add

Goal state after:
case succ
α : Type u_1
a : α
s : Multiset α
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ n • s ∨ a ∈ s
⊢ a ∈ s
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s + s

Tactic:
mem_add

Goal state after:
case refine_2
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s ∨ a ∈ s
Module: Mathlib.Data.List.Chain

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

Tactic:
let l' : List.chains r := ⟨l, hl'⟩

Goal state after:
case cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl : List.IsChain (flip r) (a :: l)
hl' : List.IsChain (flip r) l
l' : List.chains r := ⟨l, hl'⟩
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ∃ n_1, n_1 ≤ (hd :: tl).length ∧ (hd :: tl).rotate n_1 = (hd :: tl).rotate n

Tactic:
refine ⟨n % (hd :: tl).length, ?_, rotate_mod _ _⟩

Goal state after:
case cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n % (hd :: tl).length ≤ (hd :: tl).length
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ (↑l₁).product ↑l₂ = ↑(l₁.product l₂)

Tactic:
rw [product, List.product, ← coe_bind]

Goal state after:
α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ ((↑l₁).bind fun a ↦ map (Prod.mk a) ↑l₂) = (↑l₁).bind fun a ↦ ↑(List.map (Prod.mk a) l₂)
Module: Mathlib.Data.List.OffDiag

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

Tactic:
← zipIdx_map_fst 0 l,

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

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

Tactic:
rw [h, Nat.add_sub_cancel_right] at this; rwa [h]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Monoid N
g : N →* M
x✝² x✝¹ : N
x✝ : α
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
simpa [(· • ·)] using mul_smul ..

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
b : β
⊢ ∃ a, map f a = ConjClasses.mk b

Tactic:
obtain ⟨a, rfl⟩ := hf b

Goal state after:
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
a : α
⊢ ∃ a_1, map f a_1 = ConjClasses.mk (f a)
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
motive : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
⊢ motive x

Tactic:
induction closure.symm ▸ mem_top x using closure_induction with
  | mem _ h => exact mem _ h
  | one => exact one
  | mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s / t) = ⇑m '' (⇑m ⁻¹' s / ⇑m ⁻¹' t)

Tactic:
rw [image_div, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (div_subset_range m hs ht)]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H : Subgroup G
f : G' →* G
hf : Injective ⇑f
inst✝ : IsMulCommutative ↥H
a : G'
ha : f a ∈ H
b : G'
hb : f b ∈ H
⊢ f (a * b) = f (b * a)

Tactic:
by
    simpa using setLike_mul_comm ha hb

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

Goal state before:
pp: case succ
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
⊢ (n + 1).boddDiv2 = ((n + 1).bodd, (n + 1).div2)

Tactic:
boddDiv2,

Goal state after:
case succ
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
⊢ (match n.boddDiv2 with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ decode₂ α n ≠ none ↔ n ∈ Set.range encode

Tactic:
Set.range,

Goal state after:
α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ decode₂ α n ≠ none ↔ n ∈ {x | ∃ y, encode y = x}
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ Pairwise (Disjoint on fun a ↦ a • s) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1

Tactic:
simp_rw [Pairwise, disjoint_smul_set_right, ← mul_smul,
    ← not_imp_not (b := _ ≠ _), not_ne_iff, not_disjoint_iff_nonempty_inter]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ (∀ ⦃i j : α⦄, ((j⁻¹ * i) • s ∩ s).Nonempty → i = j) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
hAB : a • s ∩ b • t = ∅
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

pp: case inr
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
· exact ⟨1, by simp [hAB]⟩

Goal state after:
case inr
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ (replicate ?m.37 1).prod = 1

pp: M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ ℕ

pp: M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ l.length = ?m.37

Tactic:
prod_replicate,

Goal state after:
M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ 1 ^ ?n = 1

case n
M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ ℕ

M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ l.length = ?n
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
α : Type u_4
f : α → M
⊢ closure (⇑(FreeMonoid.lift f) '' Set.range FreeMonoid.of) = closure (Set.range f)

Tactic:
← Set.range_comp,

Goal state after:
M : Type u_1
inst✝ : Monoid M
α : Type u_4
f : α → M
⊢ closure (Set.range (⇑(FreeMonoid.lift f) ∘ FreeMonoid.of)) = closure (Set.range f)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ Option.rec (some tl) (fun val ↦ if f val < f tl then some tl else some val) (some (if f a < f m then m else a)) =
    Option.rec (some a) (fun val ↦ if f a < f val then some val else some a) (some (if f m < f tl then tl else m))

Tactic:
grind -abstractProof

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ (if hd = val✝ then 0 else idxOf val✝ tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
if_neg,

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ idxOf val✝ tl + 1 ≤ if hd = a then 0 else idxOf a tl + 1

case pos.hnc
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ ¬hd = val✝
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ s.disjSum t = ∅ ↔ s = ∅ ∧ t = ∅

Tactic:
simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
s₁ s₂ : Finset α
t₁ t₂ : Finset β
⊢ s₁.disjSum t₁ = s₂.disjSum t₂ ↔ s₁ = s₂ ∧ t₁ = t₂

Tactic:
simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
x✝³ x✝² : Finset α
x✝¹ x✝ : Finset β
⊢ x✝³.disjSum x✝¹ = x✝².disjSum x✝ → x✝³ = x✝² ∧ x✝¹ = x✝

Tactic:
simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])

Tactic:
rw [map_append, map_singleton, ← append_assoc, ← ih, sublists'Aux, foldl_append, foldl]
    simp [sublists'Aux]

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

Goal state before:
pp: case H.inr
α : 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)
hne : s.Nonempty
⊢ motive s

Tactic:
have H : s.max' hne ∈ s := max'_mem s hne
    rw [← insert_erase H]
    exact insert _ _ (fun x ↦ s.lt_max'_of_mem_erase_max' hne) (ih _ H)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ {x ∈ (insert x s).powerset | #x = n.succ} = powersetCard n.succ s ∪ image (insert x) (powersetCard n s)

Tactic:
powerset_insert,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ {x ∈ s.powerset ∪ image (insert x) s.powerset | #x = n.succ} =
    powersetCard n.succ s ∪ image (insert x) (powersetCard n s)
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.powerset = (range (#s + 1)).disjiUnion (fun i ↦ powersetCard i s) ⋯

Tactic:
refine ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩
  · rw [mem_disjiUnion]
    exact
      ⟨a.card, mem_range.mpr (Nat.lt_succ_of_le (card_le_card (mem_powerset.mp ha))),
        mem_powersetCard.mpr ⟨mem_powerset.mp ha, rfl⟩⟩
  · rcases mem_disjiUnion.mp ha with ⟨i, _hi, ha⟩
    exact mem_powerset.mpr (mem_powersetCard.mp ha).1

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

Goal state before:
pp: α : Type u
ι : Sort u_1
inst✝ : Subsingleton ι
s : ι → Set α
⊢ (⋃ i, s i.down).Finite ↔ ∀ (i : ι), (s i).Finite

Tactic:
finite_iUnion_iff _root_.Subsingleton.pairwise

Goal state after:
α : Type u
ι : Sort u_1
inst✝ : Subsingleton ι
s : ι → Set α
⊢ (∀ (i : PLift ι), (s i.down).Finite) ∧ {i | (s i.down).Nonempty}.Finite ↔ ∀ (i : ι), (s i).Finite
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∉ s
⊢ ↑(⨆ (_ : i ∈ s), f i) ≤ ⨆ i ∈ s, ↑(f i)

Tactic:
simpa only [iSup_neg h] using le_trans (by simp) (le_biSup _ hj)

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

Goal state before:
pp: α : Type u
s : Set (Set α)
hs : s.Infinite
⊢ (⋃₀ s).Infinite

Tactic:
by
  rw [sUnion_eq_iUnion]
  have _ := hs.to_subtype
  exact infinite_iUnion Subtype.coe_injective

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ x ∈ s, f x ∈ map f s

Tactic:
by
  classical
  simpa using s.toFinset.ciInf_mem_image f (by simpa using h)

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
j : ι
hj : a j < b j
this : Nonempty ι
⊢ ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h.wcovBy

Goal state after:
case mp
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
j : ι
hj : a j < b j
this : Nonempty ι
i : ι
hi : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
⊢ ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)