mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
by
  ext x
  rcases lt_trichotomy (x : ℕ) j with (h | h | h)
  · simp only [Function.comp_apply, contractNth_apply_of_lt, h]
  · simp only [Function.comp_apply, contractNth_apply_of_eq, h, hf]
  · simp only [Function.comp_apply, contractNth_apply_of_gt, h]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ l₁.prod = l₂.prod

Tactic:
by
  have : Std.Symm fun x y ↦ ∀ z : M, y * (x * z) = x * (y * z) := { symm x y h z := h z |>.symm }
  refine h.foldr_eq' (Pairwise.forall_of_forall (fun _ _ _ ↦ rfl) <| hc.imp fun {a b} h z ↦ ?_) 1
  rw [← mul_assoc, ← mul_assoc, h]

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

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ drop n (l ++ [a]) ++ take n (l ++ [a]) = drop n l ++ take (n + 1) (a :: l)

Tactic:
take,

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ drop n (l ++ [a]) ++ take n (l ++ [a]) = drop n l ++ a :: take n l
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
n m : ℕ
⊢ ((a :: l).rotate' (n + 1)).rotate' m = (a :: l).rotate' (n + 1 + m)

Tactic:
by
    rw [rotate'_cons_succ, rotate'_rotate' _ n, Nat.add_right_comm, ← rotate'_cons_succ,
      Nat.succ_eq_add_one]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
⊢ (map (fun x ↦ count x l) l.dedup).sum = l.length

Tactic:
simpa using sum_map_count_dedup_filter_eq_countP (fun _ => True) l

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

Goal state before:
pp: l s : List ℕ
hs : s ∈ l.ranges
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (range l.sum)

Tactic:
exact nodup_range

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

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

Tactic:
let k := n % l.reverse.length

Goal state after:
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a ↦ t a + u a) = s.sigma t + s.sigma u
t u : (a : α) → Multiset (σ a)
⊢ ((a ::ₘ s).sigma fun a ↦ t a + u a) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u

Tactic:
cons_sigma,

Goal state after:
α : Type u_1
σ : α → Type u_4
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a ↦ t a + u a) = s.sigma t + s.sigma u
t u : (a : α) → Multiset (σ a)
⊢ (map (Sigma.mk a) (t a + u a) + s.sigma fun a ↦ t a + u a) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 x✝

Tactic:
Nat.eq_zero_of_le_zero hk

Goal state after:
x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 0
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.diag = {a ∈ s ×ˢ s | a.1 = a.2}

Tactic:
by
  ext; simp +contextual

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

Goal state before:
pp: r n : ℕ
h : r < n / 2
⊢ n.choose r ≤ n.choose (r + 1)

Tactic:
refine Nat.le_of_mul_le_mul_right ?_ (Nat.sub_pos_of_lt (h.trans_le (n.div_le_self 2)))

Goal state after:
r n : ℕ
h : r < n / 2
⊢ n.choose r * (n - r) ≤ n.choose (r + 1) * (n - r)
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:
by simp_rw [iUnion_inter, inter_iUnion]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ map K.subtype (H.subgroupOf K) = H

Tactic:
by
  rwa [subgroupOf_map_subtype, inf_eq_left]

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

Goal state before:
pp: a b : ℕ
⊢ a ≤ pair a b

Tactic:
by simpa using unpair_left_le (pair a b)

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : α
⊢ (fun n ↦ (decode₂ α ↑n).get ⋯) ((fun a ↦ ⟨encode a, ⋯⟩) x✝) = x✝

Tactic:
dsimp; rw [← Option.some_inj, Option.some_get, encodek₂]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ comap f (normalizer ↑H) = normalizer ↑(comap f H)

Tactic:
by
  apply le_antisymm (le_normalizer_comap f)
  rw [← map_le_iff_le_comap]
  apply (le_normalizer_map f).trans
  rw [map_comap_eq_self h]

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

Goal state before:
pp: case hS
M : Type u_1
inst✝ : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ S ↑x

Tactic:
rw [← Function.comp_def, directed_comp]

Goal state after:
case hS
M : Type u_1
inst✝ : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ Directed (S ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) Subtype.val
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
a : α
l : List α
⊢ foldl (argAux fun b c ↦ f c < f b) none (l ++ [a]) =
    Option.casesOn (argmax f l) (some a) fun c ↦ if f c < f a then some a else some c

Tactic:
argmax

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
a : α
l : List α
⊢ foldl (argAux fun b c ↦ f c < f b) none (l ++ [a]) =
    Option.casesOn (foldl (argAux fun b c ↦ f c < f b) none l) (some a) fun c ↦ if f c < f a then some a else some c
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val ↦ if f hd < f val then some val else some hd) (argmax f tl) = some m
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1

Tactic:
cases h : argmax f tl

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val ↦ if f hd < f val then some val else some hd) (argmax f tl) = some m
h : argmax f tl = none
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1

case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val ↦ if f hd < f val then some val else some hd) (argmax f tl) = some m
val✝ : α
h : argmax f tl = some val✝
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ (a :: l).sublists' = l.sublists' ++ map (cons a) l.sublists'

Tactic:
simp [sublists'_eq_sublists'Aux, foldr_cons, sublists'Aux_eq_map]

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ ([a] ++ l).sublists = do
    let x ← l.sublists
    [x, a :: x]

Tactic:
rw [sublists_append]
  simp only [sublists_singleton, map_cons, bind_eq_flatMap, nil_append, cons_append, map_nil]

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

Goal state before:
pp: α : Type u_1
n : ℕ
l : List α
s : Multiset α
⊢ ∀ (a : List α), (∃ a_1, (a_1 <+ l ∧ a_1.length = n) ∧ a_1 ~ a) ↔ (∃ l_1, l_1 ~ a ∧ l_1 <+ l) ∧ a.length = n

Tactic:
exact fun l₁ =>
      ⟨fun ⟨l₂, ⟨s, e⟩, p⟩ => ⟨⟨_, p, s⟩, p.symm.length_eq.trans e⟩,
       fun ⟨⟨l₂, p, s⟩, e⟩ => ⟨_, ⟨s, p.length_eq.trans e⟩, p⟩⟩

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

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ powersetCard s.card s = {s}

Tactic:
induction s using Multiset.induction with

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 :
  (∃ a_1 b, (a_1, b) ∈ l'.sublists.zip l'.sublists.reverse ∧ id a_1 = l₁ ∧ b ++ [a] = l₂) ∨
    ∃ a_1 b, (a_1, b) ∈ l'.sublists.zip l'.sublists.reverse ∧ a_1 ++ [a] = l₁ ∧ id b = l₂
⊢ l₁ ++ l₂ ~ l' ++ [a]

Tactic:
rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', l₂, h, rfl, rfl⟩)

Goal state after:
case append_singleton.inl
α : 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 l'.sublists.reverse
⊢ id l₁ ++ (l₂' ++ [a]) ~ l' ++ [a]

case append_singleton.inr
α : 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 l'.sublists.reverse
⊢ l₁' ++ [a] ++ id l₂ ~ l' ++ [a]
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case append_singleton.inl
α : 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 l'.sublists.reverse
⊢ id l₁ ++ (l₂' ++ [a]) ~ l' ++ [a]

Tactic:
← append_assoc

Goal state after:
case append_singleton.inl
α : 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 l'.sublists.reverse
⊢ id l₁ ++ l₂' ++ [a] ~ l' ++ [a]
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case append_singleton.inr
α : 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 l'.sublists.reverse
⊢ l₁' ++ (id l₂ ++ [a]) ~ l' ++ [a]

Tactic:
← append_assoc

Goal state after:
case append_singleton.inr
α : 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 l'.sublists.reverse
⊢ l₁' ++ id l₂ ++ [a] ~ l' ++ [a]
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' ++ map (cons a) l.sublists').zip ((map (cons a) l.sublists').reverse ++ l.sublists'.reverse)
⊢ l₁ ++ l₂ ~ a :: l

Tactic:
zip_append,

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₂) ∈ l.sublists'.zip (map (cons a) 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.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
β : Type u_2
inst✝ : DecidableEq β
f : α → β
H : Set.InjOn f ↑s
this : ∀ {z : Finset α} {a : α}, z ⊆ s → a ∈ s → (a ∈ z ↔ f a ∈ image f z)
⊢ Set.InjOn (fun x ↦ image f x) ↑s.powerset

Tactic:
exact fun _ _ _ _ _ => by grind

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

Goal state before:
pp: case singleton
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
⊢ ({a✝}.inf fun b ↦ a \ f b) = a \ {a✝}.sup f

Tactic:
rw [sup_singleton, inf_singleton]

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

Goal state before:
pp: case insert.inr.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : s.sup f ≤ f a
⊢ f a ∈ f '' insert a ↑s

Tactic:
apply Set.mem_image_of_mem _ (Set.mem_insert a ↑s)

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 α
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (count b (s.sup f) = s.sup fun a ↦ count b (f a)) →
        count b ((insert a s).sup f) = (insert a s).sup fun a ↦ count b (f a)

Tactic:
intro i s _ ih

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 ((insert i s).sup f) = (insert i s).sup fun a ↦ count b (f a)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow (⋃ i, range (f i))
⊢ BddBelow (range fun i ↦ ⨅ j, f i j)

Tactic:
by
  have ⟨a, h⟩ := H
  refine ⟨a ⊓ (sInf ∅), fun x ⟨i, hx⟩ ↦ hx ▸ ?_⟩
  cases isEmpty_or_nonempty <| κ i
  · exact iInf_of_isEmpty (f i) ▸ inf_le_right
  exact le_ciInf fun j ↦ inf_le_of_left_le <| h ⟨_, ⟨i, rfl⟩, ⟨j, rfl⟩⟩

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

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLinearOrder α
s : Set α
hfin : s.Finite
a : α
hne : a ≠ ⊥
hmem : a ∉ s
⊢ sSup s ≠ a

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hnonempty

Goal state after:
case inl
α : Type u_5
inst✝ : CompleteLinearOrder α
a : α
hne : a ≠ ⊥
hfin : ∅.Finite
hmem : a ∉ ∅
⊢ sSup ∅ ≠ a

case inr
α : Type u_5
inst✝ : CompleteLinearOrder α
s : Set α
hfin : s.Finite
a : α
hne : a ≠ ⊥
hmem : a ∉ s
hnonempty : s.Nonempty
⊢ sSup s ≠ a
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
h : a < b
⊢ ¬a ⋖ b ↔ ∃ c, a < c ∧ c < b

Tactic:
simp_rw [CovBy, h, true_and, not_forall, exists_prop, not_not]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case pos
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∈ t
⊢ t = s ∨ t = insert x s

pp: case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t = s ∨ t = insert x s

Tactic:
· exact Or.inr (subset_antisymm h2t <| insert_subset_iff.mpr ⟨h, hst⟩)

Goal state after:
case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t = s ∨ t = insert x s
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update a i (b i)
h₁ : c ≤ b
h₂ : ¬c j < b j
⊢ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
exact ⟨hab j, by simpa [lt_iff_le_not_ge, hab j, c, hj] using h₂⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
⊢ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯ ⊆ cons ⊤ (Finset.map Embedding.coeWithTop t) ⋯ ↔ s ⊆ t

Tactic:
by rw [cons_subset_cons, map_subset_map]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
h : WellFoundedGT α
a : ℕ →o α
n : ℕ
H : ∀ x ∈ Set.range ⇑a, ¬a n < x
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

Tactic:
exact ⟨n, fun m _ => H _ (Set.mem_range_self _)⟩

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : a₁ < a₂
⊢ Ico a₂ b ⊆ Ioo a₁ b

Tactic:
rw [← coe_subset, coe_Ico, coe_Ioo]

Goal state after:
α : Type u_2
a₁ a₂ b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : a₁ < a₂
⊢ Set.Ico a₂ b ⊆ Set.Ioo a₁ b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝¹ : Fintype ι
this✝ : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
this :
  ∀ (t : Finset ι) (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ (univ.pi s).PartiallyWellOrderedOn fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
partiallyWellOrderedOn_iff_exists_monotone_subseq

Goal state after:
ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝¹ : Fintype ι
this✝ : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
this :
  ∀ (t : Finset ι) (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ ∀ (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ), f n ∈ univ.pi s) → ∃ g, ∀ (m n : ℕ), m ≤ n → ∀ (i : ι), r i (f (g m) i) (f (g n) i)
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h
α : Type u_3
inst✝ : Monoid α
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
l : List α
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
base : ∀ x ∈ ⟦l⟧, p x
⊢ p (noncommProd ⟦l⟧ comm)

Tactic:
| _ l
   => 

Goal state after:
case h
α : Type u_3
inst✝ : Monoid α
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
l : List α
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
base : ∀ x ∈ ⟦l⟧, p x
⊢ p (noncommProd ⟦l⟧ comm)
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ ⟦l⟧
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
⊢ a * (erase ⟦l⟧ a).noncommProd comm' = noncommProd ⟦l⟧ comm

Tactic:
| _ l
   => 

Goal state after:
case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ ⟦l⟧
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
⊢ a * (erase ⟦l⟧ a).noncommProd comm' = noncommProd ⟦l⟧ comm
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (cons a s ha).noncommProd f comm = s.noncommProd f ⋯ * f a

Tactic:
simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons']

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s).Pairwise (Commute on f)
comm' : ∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → (Commute on f) x x_1
⊢ (s.erase a).noncommProd f comm' * f a = s.noncommProd f comm

Tactic:
simpa only [← Multiset.map_erase_of_mem _ _ h] using!
    Multiset.noncommProd_erase_mul (s.1.map f) (Multiset.mem_map_of_mem f h) _

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case of
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ (x y : M), r x y → s x y

Tactic:
exact fun x y h => hs x y h

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ : Type u
x✝ : FreeAbelianGroup α✝
x : α✝
ih : id <$> pure x = pure x
⊢ id <$> (-pure x) = -pure x

Tactic:
rw [FreeAbelianGroup.map_neg, ih]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
p : α✝
ih : Prod.mk <$> pure p <*> y = (fun b a ↦ (a, b)) <$> y <*> pure p
⊢ Prod.mk <$> (-pure p) <*> y = (fun b a ↦ (a, b)) <$> y <*> -pure p

Tactic:
rw [FreeAbelianGroup.map_neg, neg_seq, seq_neg, ih]

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
s : Multiset M
⊢ IsUnit s.prod ↔ ∀ a ∈ s, IsUnit a

Tactic:
induction s using Multiset.induction with

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
⊢ ∀ {x y z : X × ↥S},
    (∃ u v, u • y.fst = v • x.fst ∧ ↑u * ↑y.snd = v * ↑x.snd) →
      (∃ u v, u • z.fst = v • y.fst ∧ ↑u * ↑z.snd = v * ↑y.snd) →
        ∃ u v, u • z.fst = v • x.fst ∧ ↑u * ↑z.snd = v * ↑x.snd

Tactic:
rintro ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨r₃, s₃⟩ ⟨u, v, hur₁, hs₁u⟩ ⟨u', v', hur₂, hs₂u⟩

Goal state after:
case refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • (r₂, s₂).fst = v • (r₁, s₁).fst
hs₁u : ↑u * ↑(r₂, s₂).snd = v * ↑(r₁, s₁).snd
u' : ↥S
v' : R
hur₂ : u' • (r₃, s₃).fst = v' • (r₂, s₂).fst
hs₂u : ↑u' * ↑(r₃, s₃).snd = v' * ↑(r₂, s₂).snd
⊢ ∃ u v, u • (r₃, s₃).fst = v • (r₁, s₁).fst ∧ ↑u * ↑(r₃, s₃).snd = v * ↑(r₁, s₁).snd
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ r' • ↑u • r₂ = r' • v • r₁

Tactic:
hur₁

Goal state after:
case refine_2.refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ r' • v • r₁ = r' • v • r₁
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
or : Set.SurjOn ⇑g ↑S ↑T ∨ Injective ⇑k
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
⊢ z = w

Tactic:
have : k (g z') = k (g w') := by rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
or : Set.SurjOn ⇑g ↑S ↑T ∨ Injective ⇑k
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
this : k (g z') = k (g w')
⊢ z = w