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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
⊢ (l ++ [a]).maximum = max l.maximum ↑a

Tactic:
simp only [maximum, argmax_concat, id]
  cases argmax id l
  · exact (max_eq_right bot_le).symm
  · simp [WithBot.some_eq_coe, max_def_lt, WithBot.coe_lt_coe]

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

Goal state before:
pp: case cons.inl
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ x :: l
⊢ a ≤ max x (foldr max b l)

pp: case cons.inr
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ y :: l
hl : x ∈ l
⊢ a ≤ max y (foldr max b l)

Tactic:
· exact le_max_of_le_left h

Goal state after:
case cons.inr
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ y :: l
hl : x ∈ l
⊢ a ≤ max y (foldr max b l)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ flatMap (fun x ↦ map (fun x_1 ↦ x_1 ++ x) l.sublists) [[], [a]] = l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists

Tactic:
flatMap_cons,

Goal state after:
α : Type u
l : List α
a : α
⊢ map (fun x ↦ x ++ []) l.sublists ++ flatMap (fun x ↦ map (fun x_1 ↦ x_1 ++ x) l.sublists) [[a]] =
    l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ map (fun x ↦ x ++ []) l.sublists ++ flatMap (fun x ↦ map (fun x_1 ↦ x_1 ++ x) l.sublists) [[a]] =
    l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists

Tactic:
flatMap_cons,

Goal state after:
α : Type u
l : List α
a : α
⊢ map (fun x ↦ x ++ []) l.sublists ++
      (map (fun x ↦ x ++ [a]) l.sublists ++ flatMap (fun x ↦ map (fun x_1 ↦ x_1 ++ x) l.sublists) []) =
    l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case h
α : Type u_2
a✝ : List α
⊢ ((range (card ⟦a✝⟧ + 1)).bind fun k ↦ powersetCard k ⟦a✝⟧) = powerset ⟦a✝⟧

Tactic:
quot_mk_to_coe,

Goal state after:
case h
α : Type u_2
a✝ : List α
⊢ ((range ((↑a✝).card + 1)).bind fun k ↦ powersetCard k ↑a✝) = (↑a✝).powerset
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 ++ map (fun x ↦ x ++ [a]) l'.sublists).zip (l'.sublists ++ map (fun x ↦ x ++ [a]) l'.sublists).reverse
⊢ l₁ ++ l₂ ~ l' ++ [a]

Tactic:
reverse_append,

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

Tactic:
reverse_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' ++ map (cons a) l.sublists').zip ((map (cons a) l.sublists').reverse ++ l.sublists'.reverse)
⊢ l₁ ++ l₂ ~ a :: l
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n ↦ sublistsLen n (h :: tl)) (0 :: map succ (range (tl.length + 1))) ~ (h :: tl).sublists'

Tactic:
flatMap_cons,

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 (h :: tl) ++ flatMap (fun n ↦ sublistsLen n (h :: tl)) (map succ (range (tl.length + 1))) ~
    (h :: tl).sublists'
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case mk
α : Type u_1
n : ℕ
t : Finset α
val✝ : Multiset α
nodup✝ : val✝.Nodup
⊢ { val := val✝, nodup := nodup✝ } ∈ powersetCard n t ↔
    { val := val✝, nodup := nodup✝ } ⊆ t ∧ #{ val := val✝, nodup := nodup✝ } = n

Tactic:
simp [powersetCard, val_le_iff.symm]

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

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

Tactic:
rw [map_eq_image, Embedding.some_apply, image_some_eraseNone]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
t : Finset β
f g : β → α
h₁ : s = t
h₂ : ∀ x ∈ s, f x = g x
⊢ s.sup' H f = t.sup' ⋯ g

Tactic:
subst s

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
t : Finset β
f g : β → α
H : t.Nonempty
h₂ : ∀ x ∈ t, f x = g x
⊢ t.sup' H f = t.sup' ⋯ g
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons.inr
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s✝ : Finset ι
H : s✝.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
b : ι
hb : b ∈ s
h' : s.sup' hs f = f b
h : f c ≤ f b
⊢ ∃ i ∈ cons c s hcs, max (f c) (f b) = f i

Tactic:
| inr h =>

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

Goal state before:
pp: case pos
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∈ t
⊢ x ∈ ⋃ i ∈ t, s i

Tactic:
exact mem_biUnion hi hx

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

Goal state before:
pp: case mp
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
x_in : x ∈ t
i : ι
hi : i ∈ I
H : x ∈ (fun h ↦ s i) hi
⊢ ∃ i, x ∈ s ↑i ∩ t

Tactic:
exact ⟨⟨i, hi⟩, ⟨H, x_in⟩⟩

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Ioc ↑a ↑b = Ioc a b

Tactic:
simp [← Ioi_inter_Iic]

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

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

Tactic:
by
  refine le_antisymm ciSup_exists_le <| ciSup_le' fun i ↦ ciSup_le' fun hi ↦ ?_
  simp [show Exists p from ⟨i, hi⟩]

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

Goal state before:
pp: case inl.mp
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ →
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨i, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨i, b⟩.snd)

Tactic:
simp_rw [sigmaLift]
      simp only [dite_eq_ite, ite_true, mem_map, Embedding.sigmaMk_apply, forall_exists_index,
        and_imp]
      rintro x hx rfl
      exact ⟨rfl, rfl, hx⟩

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

Goal state before:
pp: case inr
s : Set ℕ
h : s.Nonempty
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

Tactic:
| inr h =>

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

Goal state before:
pp: case inr
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s.Nonempty
⊢ m ∉ s

Tactic:
| inr h =>

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

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀ h₁ : LocallyFiniteOrder α
⊢ h₀ = h₁

Tactic:
obtain ⟨h₀_finset_Icc, h₀_finset_Ico, h₀_finset_Ioc, h₀_finset_Ioo,
      h₀_finset_mem_Icc, h₀_finset_mem_Ico, h₀_finset_mem_Ioc, h₀_finset_mem_Ioo⟩ := h₀
    obtain ⟨h₁_finset_Icc, h₁_finset_Ico, h₁_finset_Ioc, h₁_finset_Ioo,
      h₁_finset_mem_Icc, h₁_finset_mem_Ico, h₁_finset_mem_Ioc, h₁_finset_mem_Ioo⟩ := h₁
    have hIcc : h₀_finset_Icc = h₁_finset_Icc := by
      ext a b x
      rw [h₀_finset_mem_Icc, h₁_finset_mem_Icc]
    have hIco : h₀_finset_Ico = h₁_finset_Ico := by
      ext a b x
      rw [h₀_finset_mem_Ico, h₁_finset_mem_Ico]
    have hIoc : h₀_finset_Ioc = h₁_finset_Ioc := by
      ext a b x
      rw [h₀_finset_mem_Ioc, h₁_finset_mem_Ioc]
    have hIoo : h₀_finset_Ioo = h₁_finset_Ioo := by
      ext a b x
      rw [h₀_finset_mem_Ioo, h₁_finset_mem_Ioo]
    simp_rw [hIcc, hIco, hIoc, hIoo]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
⊢ (∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m

Tactic:
by
  congrm ∀ a, ∃ n, ∀ m h, ?_
  rw [lt_iff_le_and_ne]
  simp [a.mono h]

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

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

Tactic:
rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, Nat.zero_sub]

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

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
g : M
x : ↥(FixedPoints.submonoid M α)
y : α
⊢ g • x • y = x • g • y

Tactic:
by simp_rw [Submonoid.smul_def, smul_eq_mul, smul_mul', x.2 g]

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

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
b c : A i
⊢ x i * (b * c) = x i * b * c

Tactic:
by simpa using h2 (update x i b) (update x i c) i

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
h : ↥H
⊢ ↑((MulEquiv.symm (MulAut.conjNormal g)) h) = g⁻¹ * ↑h * g

Tactic:
change _ * g⁻¹⁻¹ = _

Goal state after:
G : Type u_3
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
h : ↥H
⊢ ofConjAct (toConjAct.toMonoidHom g)⁻¹ * ↑h * g⁻¹⁻¹ = g⁻¹ * ↑h * g
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
hH : H.Characteristic
⊢ (centralizer ↑H).Characteristic

Tactic:
refine Subgroup.characteristic_iff_comap_le.mpr fun ϕ g hg h hh => ϕ.injective ?_
  rw [map_mul, map_mul]
  exact hg (ϕ h) (Subgroup.characteristic_iff_le_comap.mp hH ϕ hh)

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

Goal state before:
pp: case mul
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x' : G
hy✝ : x' ∈ closure (↑H * ↑N)
hx' : x' ∈ ↑H * ↑N
x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 ↦ x1 * x2) x y ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 ↦ x1 * x2) x y * x' ∈ ↑H * ↑N

Tactic:
obtain ⟨x', hx', y', hy', rfl⟩ := hx'

Goal state after:
case mul
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 ↦ x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 ↦ x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 ↦ x1 * x2) x y * (fun x1 x2 ↦ x1 * x2) x' y' ∈ ↑H * ↑N
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∏ x, f x = ∏ x ∈ m.toFinset, g x

Tactic:
by
  refine prod_bij' (fun x _ ↦ x) (fun x hx ↦ ⟨x, Multiset.mem_toFinset.1 hx⟩) ?_ ?_ ?_ ?_ ?_ <;>
    simp [hfg]

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

Goal state before:
pp: α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
l : List (Multiset α)
⊢ Disjoint (sum ⟦l⟧) a ↔ ∀ b ∈ ⟦l⟧, Disjoint b a

Tactic:
quot_mk_to_coe,

Goal state after:
α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
l : List (Multiset α)
⊢ Disjoint (↑l).sum a ↔ ∀ b ∈ ↑l, Disjoint b a
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
⊢ (fun x ↦ Quotient.mk'' fun i ↦ (x i).out) ((fun q ↦ q.liftOn' (fun x i ↦ Quotient.mk'' (x i)) ⋯) (Quotient.mk'' a✝)) =
    Quotient.mk'' a✝

Tactic:
simp only [Quotient.liftOn'_mk'', Quotient.eq'']

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
⊢ piSetoid (fun i ↦ (Quotient.mk'' (a✝ i)).out) a✝
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case tail.inr
α : Type u
L L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂

Tactic:
have : s ++ (a, b) :: (a, not b) :: e' ++ L₂ =
            s ++ (a, b) :: (a, not b) :: (e' ++ L₂) := by simp
          rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩
          exact ⟨w₁, w₂, rfl, h₁.tail Step.not, h₂⟩

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
⊢ ∏ j ∈ t, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s with g i ∈ t, f i

Tactic:
← prod_disjiUnion,

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
⊢ ∏ x ∈ t.disjiUnion (fun j ↦ {i ∈ s | g i = j}) ?h, f x = ∏ i ∈ s with g i ∈ t, f i

case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
⊢ (↑t).PairwiseDisjoint fun j ↦ {i ∈ s | g i = j}
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
⊢ ∏ j ∈ t, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s, f i

Tactic:
← prod_disjiUnion,

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
⊢ ∏ x ∈ t.disjiUnion (fun j ↦ {i ∈ s | g i = j}) ?h, f x = ∏ i ∈ s, f i

case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
⊢ (↑t).PairwiseDisjoint fun j ↦ {i ∈ s | g i = j}
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case calc_3
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ b ∈ {x ∈ t | g x ≠ 1}, ∃ a, ∃ (ha : a ∈ {x ∈ s | f x ≠ 1}), i a ⋯ ⋯ = b

pp: case calc_4
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), f a = g (i a ⋯ ⋯)

Tactic:
· intro b hb
    refine (mem_filter.mp hb).elim fun h₁ h₂ ↦ ?_
    obtain ⟨a, ha₁, ha₂, eq⟩ := i_surj b h₁ fun H ↦ by rw [H] at h₂; simp at h₂
    exact ⟨a, mem_filter.mpr ⟨ha₁, ha₂⟩, eq⟩

Goal state after:
case calc_4
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), f a = g (i a ⋯ ⋯)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ι → M
h : ∏ x ∈ s, f x ≠ 1
⊢ ∃ a ∈ s, f a ≠ 1

Tactic:
by
  contrapose! h
  exact prod_eq_one h

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
⊢ Function.LeftInverse ⇑(Abelianization.map e.symm.toMonoidHom) ⇑(Abelianization.map e.toMonoidHom)

Tactic:
by
    rintro ⟨a⟩
    simp

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
⊢ Function.RightInverse ⇑(Abelianization.map e.symm.toMonoidHom) ⇑(Abelianization.map e.toMonoidHom)

Tactic:
by
    rintro ⟨a⟩
    simp

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ≠ 1

Tactic:
exact (one_lt_of_lt_mul_right hz₁).ne.symm

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ (QuotientGroup.mk' N) x * (QuotientGroup.mk' N) y = (QuotientGroup.mk' N) y * (QuotientGroup.mk' N) x

Tactic:
rw [← commutatorElement_eq_one_iff_mul_comm, ← map_commutatorElement, QuotientGroup.mk'_apply,
      QuotientGroup.eq_one_iff]

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ N
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
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
⊢ (f.lift hg) (f x) = g x

Tactic:
rw [lift_spec, ← g.map_mul]

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
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
⊢ g (f.sec (f x)).1 = g (↑(f.sec (f x)).2 * x)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
P : Type u_4
inst✝ : Monoid P
j k : N →* P
h : j.comp f.toMonoidHom = k.comp f.toMonoidHom
⊢ j = k

Tactic:
by
  ext n
  obtain ⟨⟨m, s⟩, hn : n * f s = f m⟩ := f.surj n
  replace h (a) : j (f a) = k (f a) := congr($h a)
  exact ((f.map_units s).map j).mul_left_inj.mp <| by rw [← j.map_mul, h, ← k.map_mul, hn, h m]

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

Goal state before:
pp: case c.c
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ r • (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = (r₁ /ₒ s₁) • r • (r₂ /ₒ s₂)

Tactic:
rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, smul_smul, smul_smul,
      mul_div_one, oreDiv_mul_char _ _ _ _ (r • 1) s₁ (by simp), mul_one]

Goal state after:
case c.c
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ (r • 1 * r₁ /ₒ s₁) • (r₂ /ₒ s₂) = (r₁ * r • 1 /ₒ s₁) • (r₂ /ₒ s₂)
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[n] x ≤ g^[n] x

Tactic:
by
  apply hf.seq_le_seq n
  · rfl
  · intros; rw [iterate_succ_apply']
  · simp [h.iterate_right _ _, hg.iterate _ hx]

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : IsSuccLimit b
⊢ isSuccLimitRecOn b isMin succ isSuccLimit = isSuccLimit b hb

Tactic:
rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit,
    dif_neg hb.not_isMin]

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case pos
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
hmS : m ∈ S
⊢ ∃ x, IsGreatest S x

Tactic:
exact ⟨m, hmS, hm⟩

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

Goal state before:
pp: m n a b : ℕ
h : a ≤ b
⊢ Order.succ^[b - a] a = b

Tactic:
by rw [succ_eq_succ, Nat.succ_iterate, add_tsub_cancel_of_le h]

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_3
n : ℕ
a : α
s : Sym α n
⊢ (a :: symEquivSym' s) = symEquivSym' (a ::ₛ s)

Tactic:
rcases s with ⟨⟨l⟩, _⟩

Goal state after:
case mk
α : Type u_3
n : ℕ
a : α
val✝ : Multiset α
l : List α
property✝ : Multiset.card (Quot.mk (⇑(List.isSetoid α)) l) = n
⊢ (a :: symEquivSym' ⟨Quot.mk (⇑(List.isSetoid α)) l, property✝⟩) =
    symEquivSym' (a ::ₛ ⟨Quot.mk (⇑(List.isSetoid α)) l, property✝⟩)
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_3
n : ℕ
s : Sym α n
⊢ map (fun x ↦ x) s = s

Tactic:
ext; simp only [map, Multiset.map_id', ← val_eq_coe]

Goal state after: