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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
⊢ ∀ {a b : α}, [a, b] <+ l → R a b

Tactic:
intro a b hab

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
⊢ R a b
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
a : M
⊢ {a}.prod = a

Tactic:
simp only [mul_one, prod_cons, ← cons_zero, prod_zero]

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : ¬l.length = 0
⊢ l.rotate n = l.rotate' n

Tactic:
rw [← rotate'_mod,
        rotate'_eq_drop_append_take (le_of_lt (Nat.mod_lt _ (Nat.pos_of_ne_zero h)))]
    simp [rotate]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ S.bind f

Tactic:
refine le_iff_count.2 fun a ↦ ?_
  obtain ⟨m', hm'⟩ := exists_cons_of_mem <| mem_map_of_mem (fun b ↦ count a (f b)) hx
  rw [count_bind, hm', sum_cons]
  exact Nat.le_add_right _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f✝ : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
i : α
hi : i ∈ s
j : α
hj : j ∈ s
⊢ Disjoint (f i) (g j)

Tactic:
specialize hfg' hi hj

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f✝ : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
i : α
hi : i ∈ s
j : α
hfg' : i ≠ j → (fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)) i j
hj : j ∈ s
⊢ Disjoint (f i) (g j)
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
s : Multiset α
t : α → Multiset β
x : β
⊢ x ∈ (s.bind t).toFinset ↔ x ∈ s.toFinset.biUnion fun a ↦ (t a).toFinset

Tactic:
simp only [Multiset.mem_toFinset, mem_biUnion, Multiset.mem_bind]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype ↑s
ht : Fintype ↑t
⊢ Fintype ↑(image2 f s t)

Tactic:
by
  rw [← image_prod]
  apply Set.fintypeImage

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

Goal state before:
pp: α : Type u_1
ι : Sort u_9
f : ι → α
a : α
⊢ a ∈ range f ↔ a ∈ ⋃ i, {f i}

Tactic:
simp [@eq_comm α a]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set β
⊢ (⋃ i, ⋃ j, s i j) ×ˢ t = ⋃ i, ⋃ j, s i j ×ˢ t

Tactic:
iUnion_prod_const

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Div α
inst✝ : Div β
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ s₁ ×ˢ t₁ / s₂ ×ˢ t₂ = (s₁ / s₂) ×ˢ (t₁ / t₂)

Tactic:
by aesop (add simp mem_div)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Mul α
inst✝ : IsLeftCancelMul α
s t : Set α
⊢ t.Nontrivial → s.Nonempty → (s * t).Nontrivial

Tactic:
rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩
  exact ⟨c * a, mul_mem_mul hc ha, c * b, mul_mem_mul hc hb, by simpa⟩

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✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ s * t ⊆ range ⇑m

Tactic:
rintro _ ⟨a, ha, b, hb, rfl⟩

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
a : β
ha : a ∈ s
b : β
hb : b ∈ t
⊢ (fun x1 x2 ↦ x1 * x2) a b ∈ range ⇑m
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
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ s / t ⊆ range ⇑m

Tactic:
rintro _ ⟨a, ha, b, hb, rfl⟩

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
a : β
ha : a ∈ s
b : β
hb : b ∈ t
⊢ (fun x1 x2 ↦ x1 / x2) a b ∈ range ⇑m
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H = ⊥ ∨ ∃ x ∈ H, x ≠ 1

Tactic:
convert! H.bot_or_nontrivial
  rw [nontrivial_iff_exists_ne_one]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H K : Subgroup G
h : Codisjoint H K
⊢ map f H ⊔ map f K = ⊤

Tactic:
← map_sup,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H K : Subgroup G
h : Codisjoint H K
⊢ map f (H ⊔ K) = ⊤
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : G
⊢ ∀ (x : ι), a ∈ S x → ∀ (b : G) (x : ι), b ∈ S x → a * b = b * a

Tactic:
i

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : G
i : ι
⊢ a ∈ S i → ∀ (b : G) (x : ι), b ∈ S x → a * b = b * a
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
M : Type u_7
inst✝ : MulOneClass M
f : G →* G'
g : G' →* M
h : g.comp f = 1
y : G
⊢ f y ∈ g.ker

Tactic:
exact DFunLike.congr_fun h y

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

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
N : Type u_5
P : Type u_6
inst✝² : Group N
inst✝¹ : Group P
K : Subgroup G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x : G
hx : x ∈ f.ker
y : G
⊢ f y * f x * f y⁻¹ = 1

Tactic:
mem_ker.1 hx,

Goal state after:
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
N : Type u_5
P : Type u_6
inst✝² : Group N
inst✝¹ : Group P
K : Subgroup G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x : G
hx : x ∈ f.ker
y : G
⊢ f y * 1 * f y⁻¹ = 1
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ closure (Set.range ⇑f) = mrange f

Tactic:
rw [← Set.image_univ, ← map_mclosure, mrange_eq_map, closure_univ]

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
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
hf : Surjective ⇑f
H K : Submonoid M
h : Codisjoint H K
⊢ map f H ⊔ map f K = ⊤

Tactic:
← map_sup,

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
hf : Surjective ⇑f
H K : Submonoid M
h : Codisjoint H K
⊢ map f (H ⊔ K) = ⊤
Module: Mathlib.Logic.Equiv.Nat

Goal state before:
pp: ⊢ ⇑natSumNatEquivNat = Sum.elim (fun x ↦ 2 * x) fun x ↦ 2 * x + 1

Tactic:
by
  ext (x | x) <;> rfl

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

Goal state before:
pp: case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < a₂ * a₂ + (a₂ + b)

Tactic:
apply add_lt_add

Goal state after:
case neg.h₁
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ < a₂ * a₂

case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ + b < a₂ + b
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 : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : M
⊢ ∀ (x : ι), a ∈ S x → ∀ (b : M) (x : ι), b ∈ S x → a * b = b * a

Tactic:
i

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : M
i : ι
⊢ a ∈ S i → ∀ (b : M) (x : ι), b ∈ S x → a * b = b * a
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
j : ι
b : α j
hji : r j i
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩ ∨ ⟨i, a⟩ = ⟨j, b⟩ ∨ Lex r s ⟨j, b⟩ ⟨i, a⟩

Tactic:
exact Or.inr (Or.inr <| Lex.left _ _ hji)

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeSup α
inst✝¹ : SemilatticeSup β
inst✝ : SupHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f a ⊔ f b = f b

Tactic:
← map_sup,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeSup α
inst✝¹ : SemilatticeSup β
inst✝ : SupHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f (a ⊔ b) = f b
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
s t : Multiset α
h : (s, t) ∈ l'.revzip
⊢ (s, t) = (s, ↑l - s)

Tactic:
← H h,

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
s t : Multiset α
h : (s, t) ∈ l'.revzip
⊢ (s, t) = (s, (s, t).1 + (s, t).2 - s)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
l : List α
h : l.Nodup
⊢ (sublistsLen n l).Nodup

Tactic:
by
  have : Pairwise (· ≠ ·) l.sublists' := Pairwise.imp
    (fun h => Lex.to_ne (by convert! h using 3; simp [eq_comm])) h.sublists'
  exact this.sublist (sublistsLen_sublist_sublists' _ _)

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ (map f (a :: l)).sublists = map (map f) (a :: l).sublists

Tactic:
rw [map_cons, sublists_cons, bind_eq_flatMap, sublists_map f l, sublists_cons,
      bind_eq_flatMap, map_eq_flatMap, map_eq_flatMap]
    induction sublists l <;> simp [*]

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'.sublists.zip (map (fun x ↦ x ++ [a]) l'.sublists.reverse) ++
      (map (fun x ↦ x ++ [a]) l'.sublists).zip l'.sublists.reverse
⊢ l₁ ++ l₂ ~ l' ++ [a]

Tactic:
zip_map_right,

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 (fun x ↦ x ++ [a]) l'.sublists).zip l'.sublists.reverse
⊢ l₁ ++ l₂ ~ l' ++ [a]
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
⊢ (⋃ n, f n).Pairwise r

Tactic:
i

Goal state after:
case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
⊢ i ∈ ⋃ n, f n → ∀ ⦃y : α⦄, y ∈ ⋃ n, f n → i ≠ y → r i y
Module: Mathlib.Data.List.Sublists

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

pp: case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (l.sublists' ++ map (cons a) l.sublists').zip ((map (cons a) l.sublists').reverse ++ l.sublists'.reverse)
⊢ l.sublists'.length = (map (cons a) l.sublists').reverse.length

Tactic:
zip_map_right,

Goal state after:
case cons
α : Type u
a : α
l : List α
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 (cons a)) (l.sublists'.zip l.sublists'.reverse) ++
      (map (cons a) l.sublists').zip l.sublists'.reverse
⊢ l₁ ++ l₂ ~ a :: l

case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (l.sublists' ++ map (cons a) l.sublists').zip ((map (cons a) l.sublists').reverse ++ l.sublists'.reverse)
⊢ l.sublists'.length = (map (cons a) l.sublists').reverse.length
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ico ↑a ↑b ∩ Iio ⊤ = Ico ↑a ↑b

Tactic:
inter_eq_self_of_subset_left (Subset.trans Ico_subset_Iio_self <| Iio_subset_Iio le_top)

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ico ↑a ↑b = Ico ↑a ↑b
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
by_cases! h : Exists p
  · have : Nonempty <| Exists p := ⟨h⟩
    refine ciSup_le fun ⟨i, hi⟩ ↦ le_ciSup₂ (f := fun _ _ ↦ _) ⟨f ⟨i, hi⟩, ?_⟩ i hi
    rintro _ ⟨_, ⟨j, rfl⟩, ⟨hj, rfl⟩⟩
    rfl
  · cases isEmpty_or_nonempty ι <;>
      simp [h, iSup_of_empty', ciSup_const]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a = c
⊢ c = a ∨ c = b

pp: case inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a < c
⊢ c = a ∨ c = b

Tactic:
· exact Or.inl h2.symm

Goal state after:
case inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a < c
⊢ c = a ∨ c = b
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
⊢ (fun x1 x2 ↦ x1 ⩿ x2) = ReflGen fun x1 x2 ↦ x1 ⋖ x2

Tactic:
ext x y; simp_rw [wcovBy_iff_eq_or_covBy, @eq_comm _ x, reflGen_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | ¬b ≤ x} ↔ a ≤ x ∧ x < b

Tactic:
by rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_not_ge]

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

Goal state before:
pp: a b : ℕ
h : a ≤ b
x : ℕ
⊢ x ∈ Ico a b.succ ↔ x ∈ insert b (Ico a b)

Tactic:
simp_rw [mem_insert, mem_Ico]

Goal state after:
a b : ℕ
h : a ≤ b
x : ℕ
⊢ a ≤ x ∧ x < b.succ ↔ x = b ∨ a ≤ x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
hIoi : h₀_finset_Ioi = h₁_finset_Ioi
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := ⋯, finset_mem_Ioi := h₀_finset_mem_Ioi } =
    { finsetIoi := h₁_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := h₁_finset_mem_Ici,
      finset_mem_Ioi := h₁_finset_mem_Ioi }

Tactic:
hIoi

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b = ∅ ↔ ¬a < b

Tactic:
by
  rw [← coe_eq_empty, coe_Ioc, Set.Ioc_eq_empty_iff]

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → f (g m) > f (g n)
⊢ False

Tactic:
apply RelEmbedding.not_wellFounded _ hwf.wf

Goal state after:
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → f (g m) > f (g n)
⊢ (fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x1 < x2
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ #(Ioi a) = #(Ici a) - 1

Tactic:
rw [Ici_eq_cons_Ioi, card_cons, Nat.add_sub_cancel_right]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

Tactic:
have : #(Ico x y) < #(Icc x y) := card_lt_card <|
    ⟨Ico_subset_Icc_self, not_subset.mpr ⟨y, ⟨right_mem_Icc.mpr hxy, right_notMem_Ico⟩⟩⟩

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
z : α
hxz : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

Tactic:
have z_card := calc
      #(Icc x z) ≤ #(Ico x y) := card_le_card <| Icc_subset_Ico_right hz.1.2
      _          < #(Icc x y) := this

Goal state after:
case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
z : α
hxz : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Icc x z) < #(Icc x y)
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
⊢ { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f }

pp: case refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
n : ℕ
fn : { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }
⊢ { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f }

Tactic:
· exact ⟨(minBadSeqOfBadSeq r rk s 0 f0 hf0).1, (minBadSeqOfBadSeq r rk s 0 f0 hf0).2.2⟩

Goal state after:
case refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
n : ℕ
fn : { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }
⊢ { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f }
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
y : α
h : ∀ x ∈ s, Commute y x
⊢ Commute y (s.noncommProd comm)

Tactic:
induction s using Quotient.inductionOn
  simp only [quot_mk_to_coe, noncommProd_coe]
  exact Commute.list_prod_right _ _ h

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ ↑H * {h} = ↑H

Tactic:
by
  simp [preimage, mul_mem_cancel_right (inv_mem hh)]

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

Goal state before:
pp: ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ univ.noncommProd (fun i_1 ↦ (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M i_1) (x i_1))) ⋯ = x i

Tactic:
convert! (noncommProd_congr (insert_erase (mem_univ i)).symm _ _).trans _

Goal state after:
case convert_3
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ι → M i

case convert_4
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ insert i (univ.erase i), (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M x_1) (x x_1)) = ?convert_3 x_1

case convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (insert i (univ.erase i)).noncommProd ?convert_3 ⋯ = x i
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
a✝ : (i : ι) → α i
i : ι
⊢ (fun i ↦ (Quotient.mk'' (a✝ i)).out) i ≈ a✝ i

Tactic:
change Setoid.r _ _

Goal state after:
case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
a✝ : (i : ι) → α i
i : ι
⊢ (r i) ((fun i ↦ (Quotient.mk'' (a✝ i)).out) i) (a✝ i)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
⊢ ∏ x ∈ image (fun a ↦ ↑a) s.attach, f x = ∏ x ∈ s, f x

Tactic:
attach_image_val

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
⊢ ∏ x ∈ s, f x = ∏ x ∈ s, f x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
| ∏ a ∈ s₁, f a

Tactic:
← sdiff_union_inter s₁ s₂,

Goal state after:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
| ∏ a ∈ s₁ \ s₂ ∪ s₁ ∩ s₂, f a
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b : Bool
⊢ Lift.aux f (L₁✝ ++ (x✝, b) :: (x✝, !b) :: L₂✝) = Lift.aux f (L₁✝ ++ L₂✝)

Tactic:
cases b <;> simp [Lift.aux, List.prod_append]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : FreeGroup Unit
⊢ FreeGroup ℤ

Tactic:
by
    revert x
    exact ↑(map fun _ => (1 : ℤ))

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
F : Fintype ↥s
h : ∀ (x : ι), x ∈ s ↔ (fun x ↦ x ∈ s) x
⊢ ∏ a ∈ s, f a = ∏ a, f ↑a

Tactic:
← prod_coe_sort

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
F : Fintype ↥s
h : ∀ (x : ι), x ∈ s ↔ (fun x ↦ x ∈ s) x
⊢ ∏ i, f ↑i = ∏ a, f ↑a