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

Goal state before:
pp: α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑s + 1

Tactic:
simp [Fintype.card_ofFinset]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → ∀ (d : List α), d ~ c → d <+ tail✝ → c <+ insertionSort r tail✝
c : List α
hs : Pairwise r c
d : List α
hc : d ~ c
hd : d <+ a :: tail✝
⊢ c <+ insertionSort r (a :: tail✝)

Tactic:
cases hd with

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this : Finite ↑(f '' s)
⊢ ¬InjOn f s

Tactic:
have : Infinite s := infinite_coe_iff.mpr h_inf

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
⊢ ¬InjOn f s
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : a = b
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)

pp: case neg
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : ¬a = b
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
· subst b
        exact .cons <| IH (le_of_succ_le_succ H) (mt (congr_arg _) h)

Goal state after:
case neg
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : ¬a = b
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun a b ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun a b ↦ R b a) (y :: l)
⊢ IsChain R (a :: b :: l).reverse ↔ IsChain (fun a b ↦ R b a) (a :: b :: l)

Tactic:
| cons_cons a b l IH IH2 =>

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

Goal state before:
pp: case cons
α : 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 x ↦ count x (a :: as)) (filter p (a :: as).dedup)).sum = countP p as + if p a = true then 1 else 0

Tactic:
List.count_cons,

Goal state after:
case cons
α : 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 x ↦ count x as + if (a == x) = true then 1 else 0) (filter p (a :: as).dedup)).sum =
    countP p as + if p a = true then 1 else 0
Module: Mathlib.Data.List.Rotate

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

Tactic:
length_rotate'

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.length = l.length
Module: Mathlib.Data.List.Chain

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

Tactic:
| cons_cons a b l IH IH2 =>

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

Goal state before:
pp: case empty
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b 0)) 0 = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) 0)

Tactic:
map_zero,

Goal state after:
case empty
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ 0) 0 = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) 0)
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case empty
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ 0) 0 = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) 0)

Tactic:
map_zero,

Goal state after:
case empty
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ 0) 0 = fold op b₀ 0
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u_1
L✝ : List α
a b : α
L : List α
hL : a :: b :: L ≠ []
hL' : a = (b :: L).getLast ⋯
⊢ (a :: b :: L).dropLast ~r (a :: b :: L).tail

Tactic:
simp [hL', IsRotated.cons_getLast_dropLast]

Goal state after:
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 <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
exact nonempty_product

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

Goal state before:
pp: r n : ℕ
h : r < n / 2
⊢ r + 1 ≤ n - r

Tactic:
rw [← Nat.lt_iff_add_one_le, Nat.lt_sub_iff_add_lt, ← Nat.mul_two]

Goal state after:
r n : ℕ
h : r < n / 2
⊢ r * 2 < n
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:
inter_iUnion

Goal state after:
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_1, f i i_1 ∩ ⋃ j₁, ⋃ j₂, g j₁ j₂ = ⋃ i₁, ⋃ i₂, ⋃ j₁, ⋃ j₂, f i₁ i₂ ∩ g j₁ j₂

Tactic:
inter_iUnion

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

Goal state before:
pp: case mp.inl
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

pp: case mp.inr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (s ^ 0).Nonempty

Tactic:
· exact hs.zpow

Goal state after:
case mp.inr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (s ^ 0).Nonempty
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ {1} ⊆ ↑(closure (s \ {1}))

Tactic:
by simp [one_mem]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K : Subgroup G
s : Set G
hsn : s.Nonempty
hs : ∀ (x : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s
one_mem : 1 ∈ s
inv_mem : ∀ (x : G), x ∈ s → x⁻¹ ∈ s
a✝ b✝ : G
hx : a✝ ∈ s
hy : b✝ ∈ s
⊢ a✝ * b✝ ∈ s

Tactic:
by simpa using hs _ hx _ (inv_mem _ hy)

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:
exact inv_left _ _ _ _ h

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

Goal state before:
pp: case mp.refine_1.inl
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x✝ : G
hx✝ : x✝ ∈ closure (↑s ∪ ↑t)
x : G
hx : x ∈ ↑s
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

pp: case mp.refine_1.inr
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x✝ : G
hx✝ : x✝ ∈ closure (↑s ∪ ↑t)
x : G
hx : x ∈ ↑t
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
· exact ⟨x, hx, 1, t.one_mem, by simp⟩

Goal state after:
case mp.refine_1.inr
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x✝ : G
hx✝ : x✝ ∈ closure (↑s ∪ ↑t)
x : G
hx : x ∈ ↑t
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x
Module: Mathlib.Algebra.Group.Subgroup.MulOpposite

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ (normalizer ↑H).op = normalizer ↑H.op

Tactic:
by
  ext x
  rw [mem_op, mem_normalizer_iff', mem_normalizer_iff']
  simp [iff_comm]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
M' : Type u_5
N' : Type u_6
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
f : M →* N
g : M' →* N'
⊢ mker (f.prodMap g) = (mker f).prod (mker g)

Tactic:
by
  rw [← comap_bot', ← comap_bot', ← comap_bot', ← prod_map_comap_prod', bot_prod_bot]

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

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
x y : α
e : encode x = encode y
⊢ decode (encode y) = some y

Tactic:
encodek

Goal state after:
α : Type u_1
inst✝ : Encodable α
x y : α
e : encode x = encode y
⊢ some y = some y
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + b₁ < b₂ * b₂

Tactic:
← sqrt_lt,

Goal state after:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ (a * a + b₁).sqrt < b₂
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
n : ↑(Set.range encode)
x : α
hx : encode x = ↑n
⊢ (decode₂ α ↑n).isSome = true

Tactic:
rw [← hx, encodek₂]

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
n : ↑(Set.range encode)
x : α
hx : encode x = ↑n
⊢ (some x).isSome = true
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case mk
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
inst✝ : Encodable α
a✝ : Quotient s
l : α
⊢ Option.map Quotient.mk'' (decode (encode (rep (Quot.mk (⇑s) l)))) = some (Quot.mk (⇑s) l)

Tactic:
encodek

Goal state after:
case mk
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
inst✝ : Encodable α
a✝ : Quotient s
l : α
⊢ Option.map Quotient.mk'' (some (rep (Quot.mk (⇑s) l))) = some (Quot.mk (⇑s) l)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
this : x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
by
    simpa only [closure_iUnion, closure_eq (S _)] using this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
⊢ toLex (a₁, b₁) ⋖ toLex (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ ⋖ b₂ ∨ a₁ ⋖ a₂ ∧ IsMax b₁ ∧ IsMin b₂

Tactic:
by
  simp only [CovBy, toLex_lt_toLex, toLex.surjective.forall, Prod.forall, isMax_iff_forall_not_lt,
    isMin_iff_forall_not_lt]
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ toLex x < toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)

Tactic:
by
  rw [toLex_lt_toLex]
  simp only [lt_iff_le_not_ge, le_antisymm_iff]
  tauto

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
⊢ Injective (Sum.elim Subtype.val Subtype.val)

Tactic:
rintro (⟨a, ha⟩ | ⟨a, ha⟩) (⟨b, hb⟩ | ⟨b, hb⟩)
    · simp
    · simpa using h.ne_of_mem ha hb
    · simpa using h.symm.ne_of_mem ha hb
    simp

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ Set.range ⇑(FreeMonoid.lift Subtype.val) = List.prod '' {l | ∀ x ∈ l, x ∈ s}

Tactic:
← Set.range_list_map_coe,

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ Set.range ⇑(FreeMonoid.lift Subtype.val) = List.prod '' Set.range (List.map Subtype.val)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case append_singleton.some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c ↦ if r a c then some a else some c
c : α
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m

Tactic:
hf,

Goal state after:
case append_singleton.some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
ho : m ∈ Option.casesOn (some c) (some a) fun c ↦ if r a c then some a else some c
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ Disjoint (map Embedding.inl s) (map Embedding.inr t)

Tactic:
simp_rw [disjoint_left, mem_map]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ∀ ⦃a : α ⊕ β⦄, (∃ a_1 ∈ s, Embedding.inl a_1 = a) → ¬∃ a_2 ∈ t, Embedding.inr a_2 = a
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithBot.map (⇑ofDual) s.max = (image (⇑ofDual) s).min

Tactic:
by
  rw [min_eq_inf_withTop, inf_image]
  exact congr_fun WithTop.map_id _

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithBot.map (⇑toDual) s.max = (image (⇑toDual) s).min

Tactic:
by
  rw [min_eq_inf_withTop, inf_image]
  exact congr_fun WithTop.map_id _

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
H : s.max' hne ∈ s
⊢ motive s

Tactic:
← insert_erase H

Goal state after:
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
H : s.max' hne ∈ s
⊢ motive (Insert.insert (s.max' hne) (s.erase (s.max' hne)))
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case nil
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₂ : List α
a✝ : l₂ <+ l
sl₁ : [] <+ l
⊢ Lex (Function.swap R) [] (a :: l₂)

pp: case cons
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₂ : List α
a✝ : l₂ <+ l
b : α
l₁ : List α
sl₁ : b :: l₁ <+ l
⊢ Lex (Function.swap R) (b :: l₁) (a :: l₂)

Tactic:
· constructor

Goal state after:
case cons
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₂ : List α
a✝ : l₂ <+ l
b : α
l₁ : List α
sl₁ : b :: l₁ <+ l
⊢ Lex (Function.swap R) (b :: l₁) (a :: l₂)
Module: Mathlib.Data.Set.Finite.Range

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
f : ι → α
inst✝ : Finite ι
⊢ Finite ↑(range f)

Tactic:
have := Fintype.ofFinite (PLift ι)
  infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ #(eraseNone s) = #(s.erase none)

Tactic:
by
  rw [← card_map Function.Embedding.some, map_some_eraseNone]

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

Goal state before:
pp: case mp.cons
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : c ∉ t
ih : a < t.sup f → ∃ b ∈ t, a < f b
⊢ a < f c ∨ a < t.sup f → ∃ b ∈ cons c t hc, a < f b

Tactic:
exact fun
      | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
      | Or.inr h => let ⟨b, hb, hlt⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hlt⟩

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
⊢ iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Tactic:
cases isEmpty_or_nonempty (Subtype p)

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : IsEmpty (Subtype p)
⊢ iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
⊢ iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j ↦ f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ i ∈ c, f i
⊢ ∃ i ∈ c, ↑s ⊆ f i

Tactic:
rw [Set.biUnion_eq_iUnion] at hs

Goal state after:
α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j ↦ f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ x, f ↑x
⊢ ∃ i ∈ c, ↑s ⊆ f i
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
f : γ → α
g : α → β
s : Finset γ
⊢ ⨆ x ∈ image f s, g x = ⨆ y ∈ s, g (f y)

Tactic:
by
  simpa using! iSup_image

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
β : ι → Type u_6
f : (i : ι) → α i → β i
⊢ ∀ (x : (i : ι) × β i), (x ∈ univ.sigma fun i ↦ range (f i)) ↔ x ∈ range fun x ↦ ⟨x.fst, f x.fst x.snd⟩

Tactic:
by simp [range, Sigma.forall]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk i) (t i) → a ∉ map (Embedding.sigmaMk j) (t j)

Tactic:
simp_rw [mem_map, Function.Embedding.sigmaMk_apply]

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, (∃ a_1 ∈ t i, ⟨i, a_1⟩ = a) → ¬∃ a_2 ∈ t j, ⟨j, a_2⟩ = a
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hcb : c ≤ b
⊢ filter (fun x ↦ x < c) (Ico a b) = Ico a c

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_right hcb]

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hcb : c ≤ b
⊢ (Finset.Ico a c).val = Ico a c
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
⊢ k + 1 ∈ s ∧ ∀ n < k + 1, n ∉ s

Tactic:
exact ⟨H, fun n hnk hns ↦ H' <| hs n k (Nat.lt_succ_iff.mp hnk) hns⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ x ∈ (Ico (f a) (f b)).preimage ⇑f ⋯ ↔ a ≤ x ∧ x < b

Tactic:
by rw [mem_preimage, mem_Ico, f.le_iff_le, f.lt_iff_lt]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
he : hbad.toFinset.Nonempty
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → n ∉ bad

Tactic:
refine
            ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
              Nat.not_succ_le_self _
                (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
obtain ⟨m, n, hlt, hle⟩ := h (f ∘ g)

Goal state after:
case inr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
m n : ℕ
hlt : m < n
hle : r ((f ∘ ⇑g) m) ((f ∘ ⇑g) n)
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ #(Ico a b) = #(Ico a b) + 1 - 1

Tactic:
exact (Nat.add_sub_cancel _ _).symm

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ #(Ioo a b) = #(Ioo a b) + 1 - 1

Tactic:
exact (Nat.add_sub_cancel _ _).symm

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
g : ↥H
⊢ 1 • g = g

Tactic:
simp [HSMul.hSMul]

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
⊢ ∀ (r : ↥(normalizer ↑H)), r • 1 = 1

Tactic:
simp [HSMul.hSMul]

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
⊢ ∀ (r : ↥(normalizer ↑H)) (x y : ↥H), r • (x * y) = r • x * r • y

Tactic:
simp [HSMul.hSMul]

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hf : Function.Injective ⇑f
h : Commute (f x) (f y)
⊢ f (x * y) = f (y * x)

Tactic:
simpa only [map_mul] using h.eq

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
a : α
f : α → β
⊢ {a}.Pairwise (Commute on f)

Tactic:
exact Set.pairwise_singleton _ _

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

Goal state before:
pp: case intro
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
⊢ f x = g x

Tactic:
rw [← noncommProd_mulSingle x, univ.map_noncommProd, univ.map_noncommProd]

Goal state after:
case intro
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
⊢ univ.noncommProd (fun i ↦ f (Pi.mulSingle i (x i))) ⋯ = univ.noncommProd (fun i ↦ g (Pi.mulSingle i (x i))) ⋯