mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → Finset β
hf : (↑s).PairwiseDisjoint f
t : Finset β
⊢ Disjoint (s.disjiUnion f hf) t ↔ ∀ i ∈ s, Disjoint (f i) t

Tactic:
induction s using Finset.cons_induction

Goal state after:
case empty
α : Type u_1
β : Type u_2
f : α → Finset β
t : Finset β
hf : (↑∅).PairwiseDisjoint f
⊢ Disjoint (∅.disjiUnion f hf) t ↔ ∀ i ∈ ∅, Disjoint (f i) t

case cons
α : Type u_1
β : Type u_2
f : α → Finset β
t : Finset β
a✝¹ : α
s✝ : Finset α
h✝ : a✝¹ ∉ s✝
a✝ : ∀ (hf : (↑s✝).PairwiseDisjoint f), Disjoint (s✝.disjiUnion f hf) t ↔ ∀ i ∈ s✝, Disjoint (f i) t
hf : (↑(cons a✝¹ s✝ h✝)).PairwiseDisjoint f
⊢ Disjoint ((cons a✝¹ s✝ h✝).disjiUnion f hf) t ↔ ∀ i ∈ cons a✝¹ s✝ h✝, Disjoint (f i) t
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case mp
α : Type u
l l' : List α
⊢ l ∈ l'.cyclicPermutations → l ~r l'

Tactic:
simp_rw [mem_iff_get, get_cyclicPermutations]

Goal state after:
case mp
α : Type u
l l' : List α
⊢ (∃ n, l'.rotate ↑n = l) → l ~r l'
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg.hf.hf.hf
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ ∀ (a_1 : (a : α) → a ∈ m → β a),
    a_1 ∈ n → Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' a_1) ≍ Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b a_1)

Tactic:
intro f _

Goal state after:
case neg.hf.hf.hf
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝² : b ∈ t a
b' : β a'
a✝¹ : b' ∈ t a'
f : (a : α) → a ∈ m → β a
a✝ : f ∈ n
⊢ Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' f) ≍ Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b f)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + k).choose k = (n + 1).ascFactorial k / k !

Tactic:
apply Nat.mul_left_cancel k.factorial_pos

Goal state after:
n k : ℕ
⊢ k ! * (n + k).choose k = k ! * ((n + 1).ascFactorial k / k !)
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : ↑p.toSubmonoid = ↑q.toSubmonoid
⊢ p = q

Tactic:
coe_toSubmonoid,

Goal state after:
G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : ↑p = ↑q.toSubmonoid
⊢ p = q
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ s ⊔ t
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
rw [sup_eq_closure] at h
    refine Subgroup.closure_induction ?_ ?_ ?_ ?_ h
    · rintro y (h | h)
      · exact ⟨y, h, 1, t.one_mem, by simp⟩
      · exact ⟨1, s.one_mem, y, h, by simp⟩
    · exact ⟨1, s.one_mem, 1, ⟨t.one_mem, mul_one 1⟩⟩
    · rintro _ _ _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
      exact ⟨_, mul_mem hy₁ hy₂, _, mul_mem hz₁ hz₂, by simp [mul_assoc, mul_left_comm]⟩
    · rintro _ _ ⟨y, hy, z, hz, rfl⟩
      exact ⟨_, inv_mem hy, _, inv_mem hz, mul_comm z y ▸ (mul_inv_rev z y).symm⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
⊢ mrange (id M) = ⊤

Tactic:
simp [mrange_eq_map]

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

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

Tactic:
exact Nat.mul_self_lt_mul_self h

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a ∈ decode n, encode a = n

Tactic:
by
    cases n with
    | zero =>
      refine ⟨none, ?_, encode_none⟩
      rw [decode_option_zero, Option.mem_def]
    | succ n =>
      refine ⟨some (ofNat α n), ?_, ?_⟩
      · rw [decode_option_succ, decode_eq_ofNat, Option.map_some, Option.mem_def]
      rw [encode_some, encode_ofNat]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s₁ s₂ : Multiset α
⊢ (s₁ + s₂).sup = fold (fun x1 x2 ↦ x1 ⊔ x2) (⊥ ⊔ ⊥) (s₁ + s₂)

Tactic:
by simp [sup]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case bot
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
hmax : t.maximum = ⊥
h : ofNat s 0 < ⟨x, hx⟩
⊢ ⊥ ∈ []

Tactic:
rwa [← List.maximum_eq_bot.1 hmax, hmt]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ ∀ {a : α}, s.max = ↑a → a ∈ s

Tactic:
by
  induction s using Finset.induction_on with
  | empty => intro _ H; cases H
  | _ => grind [WithBot.coe_eq_coe]

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

Goal state before:
pp: α : Type u
l : List α
⊢ map Prod.snd l.revzip = l.reverse

Tactic:
by
  rw [← unzip_snd, unzip_revzip]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
⊢ List.map ofList (List.map pure l) <+~ List.map ofList l.sublists

Tactic:
exact ((map_pure_sublist_sublists _).map _).subperm

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
⊢ ↑(t.sup f) = t.sup fun x ↦ ↑(f x)

Tactic:
apply apply_sup_eq_sup_comp Subtype.val

Goal state after:
case g_sup
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := ⋯
this : OrderBot { x // P x } := ⋯
⊢ ∀ (x y : { x // P x }), ↑(x ⊔ y) = ↑x ⊔ ↑y

case bot
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := ⋯
this : OrderBot { x // P x } := ⋯
⊢ ↑⊥ = ⊥
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'
⊢ sublistsLen 0 tl ++ flatMap (fun a ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ~ tl.sublists'

Tactic:
rw [List.range_succ, flatMap_append, flatMap_singleton,
      sublistsLen_of_length_lt (Nat.lt_succ_self _), append_nil,
      ← List.flatMap_map Nat.succ fun n => sublistsLen n tl,
      ← flatMap_cons (f := fun n => sublistsLen n tl), ← range_succ_eq_map]

Goal state after:
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 tl) (range (tl.length + 1)) ~ tl.sublists'
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case inr.refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (j, j') ≤ (fun i ↦ ⨆ i' ∈ t, f (i, i')) (j, j').1

Tactic:
convert! le_iSup₂ (α := α) j' hj.2

Goal state after:
case e'_3
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (j, j') = f ((j, j').1, j')
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ ∀ i_1 ∈ t, Disjoint (f (i, i_1)) (⨆ i' ∈ t, f (j, i'))

Tactic:
disjoint_iSup_iff

Goal state after:
case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ ∀ i_1 ∈ t, ∀ i_3 ∈ t, Disjoint (f (i, i_1)) (f (j, i_3))
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ ∀ i_1 ∈ s, Disjoint (f (i_1, i)) (⨆ i ∈ s, f (i, j))

Tactic:
disjoint_iSup_iff

Goal state after:
case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ ∀ i_1 ∈ s, ∀ i_3 ∈ s, Disjoint (f (i_1, i)) (f (i_3, j))
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case empty
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ι → α
a : α
⊢ a ⊓ ∅.sup f = ∅.sup fun i ↦ a ⊓ f i

Tactic:
simp_rw [Finset.sup_empty, inf_bot_eq]

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

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

Tactic:
by
  rw [powersetCard_eq_filter, powerset_insert, filter_union, ← powersetCard_eq_filter]
  grind

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
⊢ Trunc (P (ULift.{u, 0} (Fin n)))

Tactic:
induction n with
  | zero =>
    have : card PEmpty = card (ULift (Fin 0)) := by
      simp only [card_fin, card_pempty, card_ulift]
    apply Trunc.bind (truncEquivOfCardEq this)
    intro e
    apply Trunc.mk
    exact of_equiv e h_empty
  | succ n ih =>
    have : card (Option (ULift (Fin n))) = card (ULift (Fin n.succ)) := by
      simp only [card_fin, card_option, card_ulift]
    apply Trunc.bind (truncEquivOfCardEq this)
    intro e
    apply Trunc.map _ ih
    intro ih
    exact of_equiv e (h_option ih)

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

Goal state before:
pp: α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
x : β
⊢ x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v

Tactic:
induction s using Finset.cons_induction

Goal state after:
case empty
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
⊢ x ∈ ∅.sup f ↔ ∃ v ∈ ∅, x ∈ f v

case cons
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a✝¹ : α
s✝ : Finset α
h✝ : a✝¹ ∉ s✝
a✝ : x ∈ s✝.sup f ↔ ∃ v ∈ s✝, x ∈ f v
⊢ x ∈ (Finset.cons a✝¹ s✝ h✝).sup f ↔ ∃ v ∈ Finset.cons a✝¹ s✝ h✝, x ∈ f v
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → Finset β
h : (range f).Finite
⊢ (⋃ a, ↑(f a)).Finite

Tactic:
rw [← biUnion_range]
  exact h.biUnion fun y _ => y.finite_toSet

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

Goal state before:
pp: case neg
α : 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)
this : Nonempty ι
i : ι
h✝ : ¬p i
⊢ sSup ∅ ≤ iSup f

Tactic:
exact hf'

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
hf' : sSup ∅ ≤ ⨆ i, g ↑i
⊢ ⨆ i ∈ f '' s, g i = ⨆ x ∈ s, g (f x)

Tactic:
rw [← csSup_image hg hf', ← csSup_image hf hg', ← Set.image_comp, comp_def]

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

Goal state before:
pp: α : Type u
β : Type v
s : Finset β
f : α → β
hf : InjOn f (f ⁻¹' ↑s)
inst✝ : DecidablePred fun x ↦ x ∈ Set.range f
⊢ MapsTo f ↑(s.preimage f hf) ↑({x ∈ s | x ∈ Set.range f})

Tactic:
simp [Set.MapsTo]

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Iio b ↔ x < b

Tactic:
rw [Iio, ← Finset.mem_def, Finset.mem_Iio]

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b - Ico c b = Ico a (min b c)

Tactic:
by
  rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_sdiff_Ico_right]

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

Goal state before:
pp: s : Set ℕ
h : 0 < sInf s
contra : ¬s.Nonempty
⊢ False

Tactic:
Set.not_nonempty_iff_eq_empty

Goal state after:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
⊢ False
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: n : ℕ
⊢ image (fun j ↦ n - 1 - j) (range n) = range n

Tactic:
by
  cases n
  · rw [range_zero, image_empty]
  · rw [Finset.range_eq_Ico, Nat.Ico_image_const_sub_eq_Ico (Nat.zero_le _)]
    simp_rw [succ_sub_succ, Nat.sub_zero, Nat.sub_self]

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
⊢ WellQuasiOrdered fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
have := Fintype.ofFinite ι

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this : Fintype ι
⊢ WellQuasiOrdered fun a b ↦ ∀ (i : ι), r i (a i) (b i)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b ⊆ Icc a b

Tactic:
rw [← coe_subset, coe_Ico, coe_Icc]

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ico a b ⊆ Set.Icc a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ioi a ⊆ Ici a

Tactic:
simpa [← coe_subset] using Set.Ioi_subset_Ici_self

Goal state after:
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)
⊢ (univ.pi s).PartiallyWellOrderedOn fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
have := Fintype.ofFinite ι

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 ι
⊢ (univ.pi s).PartiallyWellOrderedOn fun a b ↦ ∀ (i : ι), r i (a i) (b i)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
f : ι → α
s : Finset ι
⊢ image f s ⊆ Iic (s.sup f)

Tactic:
refine fun i hi ↦ mem_Iic.2 ?_
  obtain ⟨j, hj, rfl⟩ := mem_image.1 hi
  exact le_sup hj

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
a b : α
h : ⟦a⟧ = ⟦b⟧
⊢ ⟦a⟧ = ⟦b⟧

Tactic:
@Quotient.eq

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
a b : α
h : (orbitRel (↥H) α) a b
⊢ (orbitRel G α) a b
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
N : Type u_2
inst✝ : Mul N
⊢ center (M × N) = center M ×ˢ center N

Tactic:
by
  aesop (add simp [forall_and, commute_iff_eq, isMulCentral_iff, mem_center_iff])

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ ↑(normalizer ↑N)
⊢ S * ↑N = ↑N * S

Tactic:
rw [← iUnion_mul_left_image, ← iUnion_mul_right_image]

Goal state after:
G : Type u_2
inst✝ : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ ↑(normalizer ↑N)
⊢ ⋃ a ∈ S, (fun x ↦ a * x) '' ↑N = ⋃ a ∈ S, (fun x ↦ x * a) '' ↑N
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_6
inst✝ : DecidableEq α
s : Finset ι
a : α
f : ι → Multiset α
⊢ count a (∑ x ∈ s, f x) = ∑ x ∈ s, count a (f x)

Tactic:
dsimp only [Finset.sum]

Goal state after:
ι : Type u_1
α : Type u_6
inst✝ : DecidableEq α
s : Finset ι
a : α
f : ι → Multiset α
⊢ count a (map (fun x ↦ f x) s.val).sum = (map (fun x ↦ count a (f x)) s.val).sum
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : List (Additive M)
⊢ toMul s.sum = (List.map (⇑toMul) s).prod

Tactic:
simp [toMul, ofMul]

Goal state after:
M : Type u_3
inst✝ : Monoid M
s : List (Additive M)
⊢ s.sum = s.prod
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset (Additive M)
⊢ toMul s.sum = (Multiset.map (⇑toMul) s).prod

Tactic:
simp [toMul, ofMul]

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
s : Multiset (Additive M)
⊢ s.sum = s.prod
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
inst✝ : Subsingleton Mˣ
⊢ ∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1

Tactic:
induction s using Finset.cons_induction

Goal state after:
case empty
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : Subsingleton Mˣ
⊢ ∏ i ∈ ∅, f i = 1 ↔ ∀ i ∈ ∅, f i = 1

case cons
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : Subsingleton Mˣ
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∏ i ∈ s✝, f i = 1 ↔ ∀ i ∈ s✝, f i = 1
⊢ ∏ i ∈ cons a✝¹ s✝ h✝, f i = 1 ↔ ∀ i ∈ cons a✝¹ s✝ h✝, f i = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ ∏ x ∈ s.toFinset, f x = ∏ i, g i

Tactic:
prod_subtype (p := (· ∈ s)) _ (by simp)

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ ∏ a, f ↑a = ∏ i, g i

ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ Fintype { x // x ∈ s }
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_3
inst✝² : Finite ι
M : ι → Type u_4
inst✝¹ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst✝ : DecidableEq ι
⊢ ⨆ i, map (MonoidHom.mulSingle M i) (P i) = pi Set.univ P

Tactic:
have := Fintype.ofFinite ι

Goal state after:
ι : Type u_3
inst✝² : Finite ι
M : ι → Type u_4
inst✝¹ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst✝ : DecidableEq ι
this : Fintype ι
⊢ ⨆ i, map (MonoidHom.mulSingle M i) (P i) = pi Set.univ P
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
hP : ∀ (i : ι), (P i).FG
⊢ (Submonoid.pi Set.univ P).FG

Tactic:
have := Fintype.ofFinite ι

Goal state after:
ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
hP : ∀ (i : ι), (P i).FG
this : Fintype ι
⊢ (Submonoid.pi Set.univ P).FG
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case refine_2
M : Type u_1
inst✝ : Monoid M
S : Set M
hfin : Finite ↑S
φ : FreeMonoid ↑S →* M
hφ : Function.Surjective ⇑φ
⊢ Submonoid.closure (⇑φ '' Set.range FreeMonoid.of) = ⊤

Tactic:
simp [← MonoidHom.map_mclosure, hφ, FreeMonoid.closure_range_of, ← MonoidHom.mrange_eq_map]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr.refine_1
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(Submonoid.closure ↑S)

Tactic:
exact Submonoid.subset_closure

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case refine_2
G : Type u_3
inst✝ : Group G
⊢ (∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ) → FG G

Tactic:
· rintro ⟨S, hfin : Finite S, φ, hφ⟩
    exact Group.fg_of_surjective hφ

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
⊢ FG G ↔ ∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ

Tactic:
by
  refine ⟨fun ⟨S, hS⟩ ↦ ⟨S, S.finite_toSet, FreeGroup.lift Subtype.val, ?_⟩, ?_⟩
  · rwa [← MonoidHom.range_eq_top, ← FreeGroup.closure_eq_range]
  · rintro ⟨S, hfin : Finite S, φ, hφ⟩
    exact Group.fg_of_surjective hφ

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case pos
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
y : M
x✝ : y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : y ∈ P
hy₂ : y ≠ 1
ih : ∀ z ∈ P, z ≠ 1 → z ≤ y → ¬y ≤ z → z ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) y
⊢ y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}

pp: case neg
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
y : M
x✝ : y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : y ∈ P
hy₂ : y ≠ 1
ih : ∀ z ∈ P, z ≠ 1 → z ≤ y → ¬y ≤ z → z ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) y
⊢ y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}

Tactic:
· exact mem_closure_of_mem hy₃

Goal state after:
case neg
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
y : M
x✝ : y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : y ∈ P
hy₂ : y ≠ 1
ih : ∀ z ∈ P, z ≠ 1 → z ≤ y → ¬y ≤ z → z ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) y
⊢ y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}
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 ι
inst✝¹ : PartialOrder ι
inst✝ : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I).PairwiseDisjoint f
i j : κ
hdisj : f i = ⊥
hfij : f i = f j
⊢ g (f i) = 1

Tactic:
rw [hdisj, hg_bot]

Goal state after: