mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ a • A ⊆ B ↔ A ⊆ a⁻¹ • B

Tactic:
by
  refine image_subset_iff.trans ?_
  congr! 1
  exact ((MulAction.toPerm _).image_symm_eq_preimage _).symm

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ (fun x ↦ a⁻¹ • x) ⁻¹' B = a • B

Tactic:
exact ((MulAction.toPerm _).image_eq_preimage_symm _).symm

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
y : Lex (α × β)
x : α × β
h : toLex x < y
⊢ ∃ a, toLex x < a ∧ a < y

Tactic:
cases y with | h y
     =>  _ 

Goal state after:
case h.h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : toLex x < toLex y
⊢ ∃ a, toLex x < a ∧ a < toLex y
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
y : Lex (α × β)
x : α × β
h : toLex x < y
⊢ ∃ a, toLex x < a ∧ a < y

Tactic:
cases y with | h y
     =>  _ 

Goal state after:
case h.h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : toLex x < toLex y
⊢ ∃ a, toLex x < a ∧ a < toLex y
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
b : β
left✝ : b ∈ t
hb : inr b = inl a
⊢ False

Tactic:
exact inr_ne_inl hb

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
⊢ #s ≤ #t + 1

Tactic:
by
  replace h : ∀ᵉ (x ∈ s) (y ∈ s), x < y → ∃ z ∈ t, x < z ∧ z < y := by
    intro x hx y hy hxy
    rcases exists_next_right ⟨y, hy, hxy⟩ with ⟨a, has, hxa, ha⟩
    rcases h x hx a has hxa fun z hzs hz => hz.2.not_ge <| ha _ hzs hz.1 with ⟨b, hbt, hxb, hba⟩
    exact ⟨b, hbt, hxb, hba.trans_le <| ha _ hy hxy⟩
  set f : α → WithTop α := fun x => (t.filter fun y => x < y).min
  have f_mono : StrictMonoOn f s := by
    intro x hx y hy hxy
    rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩
    calc
      f x ≤ a := min_le (mem_filter.2 ⟨hat, by simpa⟩)
      _ < f y :=
        (Finset.lt_inf_iff <| WithTop.coe_lt_top a).2 fun b hb =>
          WithTop.coe_lt_coe.2 <| hay.trans (by simpa using (mem_filter.1 hb).2)
  calc
    s.card = (s.image f).card := (card_image_of_injOn f_mono.injOn).symm
    _ ≤ (insert ⊤ (t.image (↑)) : Finset (WithTop α)).card :=
      card_mono <| image_subset_iff.2 fun x _ =>
          insert_subset_insert _ (image_subset_image <| filter_subset _ _)
            (min_mem_insert_top_image_coe _)
    _ ≤ t.card + 1 := (card_insert_le _ _).trans (Nat.add_le_add_right card_image_le _)

Goal state after:
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:
exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Set ι
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ i ∈ s, f i ∈ f '' s

Tactic:
by
  lift s to Finset ι using hs
  simp only [Finset.mem_coe] at h
  simpa using Finset.ciInf_mem_image f h

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

Goal state before:
pp: α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : ↑hs.toFinset ⊆ ⋃₀ c
⊢ ∃ t ∈ c, s ⊆ t

Tactic:
sUnion_eq_biUnion

Goal state after:
α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : ↑hs.toFinset ⊆ ⋃ i ∈ c, i
⊢ ∃ t ∈ c, s ⊆ t
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
bdd : ¬BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f

Tactic:
ciSup_of_not_bddAbove bdd,

Goal state after:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
bdd : ¬BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = sSup ∅
Module: Mathlib.Data.Set.Sigma

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
⊢ Sigma.map f g ⁻¹' Sigma.mk (f i) '' s ⊆ Sigma.mk i '' g i ⁻¹' s

Tactic:
rintro ⟨j, x⟩ ⟨y, hys, hxy⟩

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
j : ι
x : α j
y : β (f i)
hys : y ∈ s
hxy : ⟨f i, y⟩ = Sigma.map f g ⟨j, x⟩
⊢ ⟨j, x⟩ ∈ Sigma.mk i '' g i ⁻¹' s
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ s \ {a} ⩿ s

Tactic:
by
  by_cases ha : a ∈ s
  · convert! wcovBy_insert a _
    ext
    simp [ha]
  · simp [ha]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
y : α i
left✝¹ : y ∈ t i
z : α j
left✝ : z ∈ t j
hz' : ⟨j, z⟩ = ⟨i, y⟩
⊢ False

Tactic:
exact hij (congr_arg Sigma.fst hz'.symm)

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

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

Tactic:
obtain ⟨⟨i, a⟩, j, b⟩ := a, b

Goal state after:
ι : 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
j : ι
b : β j
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨j, b⟩ ↔
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
h : Minimal (fun x ↦ P x ∨ Q x) x
⊢ Minimal P x ∨ Minimal Q x

Tactic:
obtain ⟨h | h, hmin⟩ := h
  · exact .inl ⟨h, fun y hy hyx ↦ hmin (Or.inl hy) hyx⟩
  exact .inr ⟨h, fun y hy hyx ↦ hmin (Or.inr hy) hyx⟩

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

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

Tactic:
by
  rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_right_le]
  rfl

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

Goal state before:
pp: α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a b : α
h : a < b
⊢ False

Tactic:
induction hs : Finset.Icc a b using Finset.strongInduction generalizing b with | H i ih
   =>  _ 

Goal state after:
case H
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a : α
i : Finset α
ih : ∀ t ⊂ i, ∀ (b : α), a < b → Icc a b = t → False
b : α
h : a < b
hs : Icc a b = i
⊢ False
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a < x ∧ x < ↑b
⊢ p x

Tactic:
exact hp hx.1.le hx.2.le a.prop b.prop

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
⊢ (∀ t ⊆ s, IsAntichain r t → t.Finite) → s.PartiallyWellOrderedOn r

Tactic:
rw [partiallyWellOrderedOn_iff_exists_lt]

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
⊢ (∀ t ⊆ s, IsAntichain r t → t.Finite) → ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst✝ : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
⊢ (s ×ˢ t).PartiallyWellOrderedOn fun x y ↦ r x.1 y.1 ∧ r' x.2 y.2

Tactic:
rw [partiallyWellOrderedOn_iff_exists_lt]

Goal state after:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst✝ : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
⊢ ∀ (f : ℕ → α × β), (∀ (n : ℕ), f n ∈ s ×ˢ t) → ∃ m n, m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ ↑(Ico a b ∪ Ico b c) = ↑(Ico a c)

Tactic:
coe_union,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ ↑(Ico a b) ∪ ↑(Ico b c) = ↑(Ico a c)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ ↑(Ioc a b ∪ Ioc b c) = ↑(Ioc a c)

Tactic:
coe_union,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ ↑(Ioc a b) ∪ ↑(Ioc b c) = ↑(Ioc a c)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(Ico a c) ⊆ ↑(Ico a b ∪ Ico b c)

Tactic:
coe_union,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(Ico a c) ⊆ ↑(Ico a b) ∪ ↑(Ico b c)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ ↑(Ico a b ∪ Ico c d) = ↑(Ico (min a c) (max b d))

Tactic:
coe_union,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ ↑(Ico a b) ∪ ↑(Ico c d) = ↑(Ico (min a c) (max b d))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ ↑(Ico a b ∪ Ico c d) = ↑(Ico (min a c) (max b d))

Tactic:
coe_union,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ ↑(Ico a b) ∪ ↑(Ico c d) = ↑(Ico (min a c) (max b d))
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
⊢ s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), ¬IsBadSeq r s f

Tactic:
rw [partiallyWellOrderedOn_iff_exists_lt]

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
⊢ (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)) ↔ ∀ (f : ℕ → α), ¬IsBadSeq r s f
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
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
m n : ℕ
mn : m < n
⊢ ¬r ((fun n ↦ ↑(fs n) n) m) ((fun n ↦ ↑(fs n) n) n)

pp: case refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
n : ℕ
g : ℕ → α
hg1 : ∀ m < n, (fun n ↦ ↑(fs n) n) m = g m
hg2 : rk (g n) < rk ((fun n ↦ ↑(fs n) n) n)
⊢ ¬IsBadSeq r s g

Tactic:
· dsimp
    rw [h m n mn.le]
    exact (fs n).2.1.2 m n mn

Goal state after:
case refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
n : ℕ
g : ℕ → α
hg1 : ∀ m < n, (fun n ↦ ↑(fs n) n) m = g m
hg2 : rk (g n) < rk ((fun n ↦ ↑(fs n) n) n)
⊢ ¬IsBadSeq r s g
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ h * g = g * h

Tactic:
rw [← mul_inv_eq_iff_eq_mul]

Goal state after:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ h * g * h⁻¹ = g
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ ↑(closure (↑H * ↑N)) = ↑H * ↑N

Tactic:
refine Set.Subset.antisymm (fun x hx => ?_) subset_closure

Goal state after:
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ x ∈ ↑H * ↑N
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
a1 : ι
h1 : a1 ∈ s
a2 : ι
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ a1 = a2

Tactic:
← left_inv a1 h1,

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
a1 : ι
h1 : a1 ∈ s
a2 : ι
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ j (i a1 h1) ⋯ = a2
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y✝ : β
h : ∀ x ∈ s, Commute y✝ (f x)
y : β
⊢ (∃ a ∈ s.val, f a = y) → Commute y✝ y

Tactic:
rintro ⟨x, ⟨hx, rfl⟩⟩

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y : β
h : ∀ x ∈ s, Commute y (f x)
x : α
hx : x ∈ s.val
⊢ Commute y (f x)
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
y : M
⊢ (∃ a ∈ t.val, f a = y) → y ∈ S

Tactic:
rintro ⟨x, ⟨hx, rfl⟩⟩

Goal state after:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
x : ι
hx : x ∈ t.val
⊢ f x ∈ S
Module: Mathlib.Data.Finset.NoncommProd

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

Tactic:
cases nonempty_fintype ι

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

Goal state before:
pp: α : Type u_1
s : Setoid α
a b : α
⊢ Quotient.mk' a = Quotient.mk' b ↔ s a b

Tactic:
Quotient.eq'

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
l : List (α × Bool)
⊢ Step (p :: l ++ L₁) (p :: l ++ L₂) ↔ Step L₁ L₂

Tactic:
by simp [Step.append_left_iff l, Step.cons_cons_iff]

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
⊢ Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)]

Tactic:
apply reflTransGen_iff_eq

Goal state after:
α : Type u
L : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
⊢ ∀ (b : List (α × Bool)), ¬Step [(x1, !b1), (x2, b2)] b
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 κ
f : ι → M
g : κ → M
e : ι → κ
he : Set.InjOn e ↑s
hest : Set.MapsTo e ↑s ↑t
h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ ∀ x ∈ t, x ∉ image e s → g x = 1

Tactic:
simpa using h'

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
i : ℕ
ih : (fun x ↦ ((map fun x ↦ 1) x).sum) ((fun x ↦ of () ^ x) (-↑i)) = -↑i
⊢ (fun x ↦ ((map fun x ↦ 1) x).sum) ((fun x ↦ of () ^ x) (-↑i - 1)) = -↑i - 1

Tactic:
by
        simp only [zpow_neg, zpow_natCast, map_inv, map_pow, map.of, sum.map_inv, neg_inj] at ih
        simp [zpow_add, ih, sub_eq_add_neg]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : Monoid M
N : Subgroup G
nN : N.Normal
G' : Subgroup G
H' : Subgroup H
inst✝¹ : G'.Normal
inst✝ : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e) G' = H'
x : G ⧸ G'
⊢ (map H' G' ↑e.symm ⋯) ((map G' H' ↑e ⋯) x) = x

Tactic:
rw [map_map G' H' G' e e.symm (he ▸ G'.le_comap_map (e : G →* H))
        (he ▸ (G'.map_equiv_eq_comap_symm e).le)]

Goal state after:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : Monoid M
N : Subgroup G
nN : N.Normal
G' : Subgroup G
H' : Subgroup H
inst✝¹ : G'.Normal
inst✝ : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e) G' = H'
x : G ⧸ G'
⊢ (map G' G' ((↑e.symm).comp ↑e) ⋯) x = x
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ (lift (⇑g ∘ f)) a = g ((lift f) a)

Tactic:
← AddMonoidHom.comp_apply g (lift f)

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ (lift (⇑g ∘ f)) a = (g.comp (lift f)) a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : Fintype κ
inst✝ : CommMonoid M
e : ι → κ
he : Injective e
f : ι → M
g : κ → M
h' : ∀ i ∉ Set.range e, g i = 1
h : ∀ (i : ι), f i = g (e i)
⊢ ∀ i ∈ univ, i ∉ e '' ↑univ → g i = 1

Tactic:
simpa using h'

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

Goal state before:
pp: case h
ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
h₂ : ∑ x ∈ s.toFinset, k • (count x s / k) • {x} = ∑ x ∈ s.toFinset, count x s • {x}
⊢ s = ∑ x ∈ s.toFinset, count x s • {x}

Tactic:
toFinset_sum_count_nsmul_eq

Goal state after:
case h
ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
h₂ : ∑ x ∈ s.toFinset, k • (count x s / k) • {x} = ∑ x ∈ s.toFinset, count x s • {x}
⊢ s = s
Module: Mathlib.GroupTheory.OreLocalization.Basic

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

Tactic:
rintro ⟨r, s⟩ ⟨r', s'⟩ ⟨u, v, hru, hsu⟩; dsimp only at *
      rcases oreCondition (s : R) s' with ⟨r₂, s₂, h₁⟩
      rcases oreCondition r₂ u with ⟨r₃, s₃, h₂⟩
      have : r₃ * v * s = s₃ * s₂ * s := by
        -- Porting note: the proof used `assoc_rw`
        rw [mul_assoc _ (s₂ : R), h₁, ← mul_assoc, h₂, mul_assoc, ← hsu, ← mul_assoc]
      rcases ore_right_cancel (r₃ * v) (s₃ * s₂) s this with ⟨w, hw⟩
      refine ⟨w * (s₃ * s₂), w * (r₃ * u), ?_, ?_⟩ <;>
        simp only [Submonoid.coe_mul, Submonoid.smul_def, ← hw]
      · simp only [mul_smul, hru, ← Submonoid.smul_def]
      · simp only [mul_assoc, hsu]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
m₁ m₂ : M
s₁ s₂ : ↥⊤
⊢ mk m₁ s₁ / mk m₂ s₂ = mk (m₁ * ↑s₂) ⟨↑s₁ * m₂, ⋯⟩

Tactic:
by
  simp [div_eq_mul_inv, mk_mul]; rfl

Goal state after:
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 y : M
h : f x = f y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ ↑((IsUnit.liftRight (g.domRestrict S) hg) c)⁻¹ * g (↑c * x) = g y

Tactic:
hc,

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 y : M
h : f x = f y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ ↑((IsUnit.liftRight (g.domRestrict S) hg) c)⁻¹ * g (↑c * y) = g y
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case refine_2
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
⊢ ∀ {w x y z : M × ↥S},
    (∃ c, ↑c * (↑x.2 * w.1) = ↑c * (↑w.2 * x.1)) →
      (∃ c, ↑c * (↑z.2 * y.1) = ↑c * (↑y.2 * z.1)) → ∃ c, ↑c * (↑(x * z).2 * (w * y).1) = ↑c * (↑(w * y).2 * (x * z).1)

Tactic:
rintro a b c d ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩

Goal state after:
case refine_2
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c d : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑d.2 * c.1) = ↑t₂ * (↑c.2 * d.1)
⊢ ∃ c_1, ↑c_1 * (↑(b * d).2 * (a * c).1) = ↑c_1 * (↑(a * c).2 * (b * d).1)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S
⊢ mk (↑a) a = 1

Tactic:
symm
  rw [← mk_one, mk_eq_mk_iff]
  exact one_rel a

Goal state after:
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
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f) (mk x y) = f.mk' x y

Tactic:
rw [mk_eq_monoidOf_mk'_apply]; exact mulEquivOfQuotient_mk' _ _

Goal state after: