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

Goal state before:
pp: case cons.tail
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)

Tactic:
exact le_max_of_le_right (IH (by assumption))

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

Goal state before:
pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (min a b) = f a ⊓ f b

Tactic:
· rw [inf_eq_right.2 h, inf_eq_right.2 (OrderHomClass.mono f h : f b ≤ f a)]

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

Goal state before:
pp: α : Type u
⊢ sublistsAux = fun a r ↦ (Array.foldl (fun r l ↦ (r.push l).push (a :: l)) #[] r.toArray).toList

Tactic:
funext a r
  simp only [sublistsAux]
  have := foldl_hom Array.toList (g₁ := fun r l => (r.push l).push (a :: l))
    (g₂ := fun r l => r ++ [l, a :: l]) (l := r) (init := #[]) (by simp)
  simpa using this

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.sublists'.Nodup ↔ l.Nodup

Tactic:
by
  rw [sublists'_eq_sublists, nodup_map_iff reverse_injective, nodup_sublists, nodup_reverse]

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

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

Tactic:
rw [_root_.inf_comm, s.sup_inf_distrib_left]
  simp_rw [_root_.inf_comm]

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
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁ a₂ x✝ : WithBot α
h₁ : WithBot.recBotCoe True p ⊥
h₂ : WithBot.recBotCoe True p x✝
⊢ WithBot.recBotCoe True p (⊥ ⊔ x✝)

Tactic:
rwa [bot_sup_eq]

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

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

Tactic:
rcases ih with ⟨b, hb, h'⟩

Goal state after:
case cons
α : 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
⊢ ∃ i ∈ cons c s hcs, (cons c s hcs).sup' ⋯ f = f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
h✝¹ : Nonempty β
h✝ : Nonempty γ
B : α
hB : ∀ y ∈ range f, y ≤ B
y : α
hy : y ∈ range fun b ↦ ⨆ c, f (b, c)
⊢ y ≤ B

Tactic:
obtain ⟨z, rfl⟩ := Set.mem_range.mp hy

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
h✝¹ : Nonempty β
h✝ : Nonempty γ
B : α
hB : ∀ y ∈ range f, y ≤ B
z : β
hy : ⨆ c, f (z, c) ∈ range fun b ↦ ⨆ c, f (b, c)
⊢ ⨆ c, f (z, c) ≤ B
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), a < x ∧ x < b ↔ x = c
hac : a < c
hcb : c < b
⊢ a ⋖ c ∧ c ⋖ b

Tactic:
exact ⟨⟨hac, fun d had hdc ↦ hdc.ne ((h d).mp ⟨had, hdc.trans hcb⟩)⟩,
      ⟨hcb, fun d hcd hdb ↦ hcd.ne ((h d).mp ⟨hac.trans hcd, hdb⟩).symm⟩⟩

Goal state after:
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
⊢ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
let c : (i : ι) → α i := Function.update a i (b i)

Goal state after:
ι : 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)
⊢ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a : α
s : Finset α
ha : a ∈ s
⊢ ∃ b, a ≤ b ∧ Maximal (fun x ↦ x ∈ s) b

Tactic:
classical
  obtain ⟨b, hb, hab, hbmin⟩ : ∃ b ∈ s, a ≤ b ∧ _ := by
    simpa [Maximal, and_assoc] using {x ∈ s | a ≤ x}.exists_maximal ⟨a, mem_filter.2 ⟨ha, le_rfl⟩⟩
  exact ⟨b, hab, hb, fun c hc hbc ↦ hbmin hc (hab.trans hbc) hbc⟩

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

Goal state before:
pp: case refine_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ p (m + n - n)

Tactic:
rwa [Nat.add_sub_cancel_right]

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

Goal state before:
pp: case refine_2
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
b : ℕ
hb : b ∈ {m | p (m - n)}
hbn : b < n
⊢ b - n ∈ {m | p m}

Tactic:
· exact hb

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

Goal state before:
pp: case inr.mpr.inl
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
    · rw [add_comm (n / a), Nat.mul_add, mul_one, ← add_assoc]
      refine hn.symm.le.trans (Nat.add_le_add_right ?_ _)
      simpa only [zero_add] using add_le_add (zero_le i) (Nat.mod_lt n ha.bot_lt).le
    · refine lt_of_lt_of_le (Nat.add_lt_add_right hi (a * (n / a + 1))) ?_
      rw [Nat.mul_add, mul_one, ← add_assoc, hn]
    · rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
⊢ t.Nonempty → ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
ht

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
by
  simpa [← coe_subset] using Set.Ioi_subset_Ici_self

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a : α
⊢ insert a (Ioi a) = Ici a

Tactic:
by
  ext
  simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]

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

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

Tactic:
exact Set.Ico_subset_Ico_union_Ico

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 α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
| x.orbit

Tactic:
← hφ x

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
| orbit (Quotient.mk' (φ x))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case tail
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y b✝ c✝ : α
a✝ : TransGen (fun x1 x2 ↦ x1 ⩿ x2) x b✝
h₁ : b✝ ⩿ c✝
h₂ : x ≤ b✝
⊢ x ≤ c✝

Tactic:
| tail _ h₁ h₂ =>

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
⊢ { g // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }

Tactic:
have h : ∃ (k : ℕ) (g : ℕ → α), (∀ m, m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k :=
      ⟨_, f, fun _ _ => rfl, hf, rfl⟩
    obtain ⟨h1, h2, h3⟩ := Classical.choose_spec (Nat.find_spec h)
    refine ⟨Classical.choose (Nat.find_spec h), h1, by convert! h2, fun g hg1 hg2 con => ?_⟩
    refine Nat.find_min h ?_ ⟨g, fun m mn => (h1 m mn).trans (hg1 m mn), con, rfl⟩
    rwa [← h3]

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_3
G : Type u_2
inst✝ : Group G
⊢ Set.SurjOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ

Tactic:
rintro ⟨g⟩ hg
    refine ⟨g, ?_, rfl⟩
    simp only [mem_noncenter, Set.compl_def, Set.mem_ofPred, Set.not_nontrivial_iff] at hg
    rw [SetLike.mem_coe, Subgroup.mem_center_iff]
    intro h
    rw [← mul_inv_eq_iff_eq_mul]
    refine hg ?_ mem_carrier_mk
    rw [mem_carrier_iff_mk_eq]
    apply mk_eq_mk_iff_isConj.mpr
    rw [isConj_comm, isConj_iff]
    exact ⟨h, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_3
G : Type u_2
inst✝ : Group G
⊢ Set.SurjOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ

Tactic:
· rintro ⟨g⟩ hg
    refine ⟨g, ?_, rfl⟩
    simp only [mem_noncenter, Set.compl_def, Set.mem_ofPred, Set.not_nontrivial_iff] at hg
    rw [SetLike.mem_coe, Subgroup.mem_center_iff]
    intro h
    rw [← mul_inv_eq_iff_eq_mul]
    refine hg ?_ mem_carrier_mk
    rw [mem_carrier_iff_mk_eq]
    apply mk_eq_mk_iff_isConj.mpr
    rw [isConj_comm, isConj_iff]
    exact ⟨h, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
g h : G
⊢ h ∈ centralizer {g} → h ∈ normalizer {g}

Tactic:
refine fun hh g ↦ ⟨?_, ?_⟩ <;> rintro rfl
    · exact (eq_mul_inv_of_mul_eq <| hh g rfl).symm
    · simpa using hh _ rfl

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

Goal state before:
pp: G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
⊢ a • ↑s = ↑s

Tactic:
ext; simp [Set.mem_smul_set_iff_inv_smul_mem, mul_mem_cancel_left, ha]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
⊢ Submonoid.powers g ≤ (zpowers g).toSubmonoid

Tactic:
rw [toSubmonoid_zpowers]
  exact le_sup_left

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ ConjAct.toConjAct g • H = H ↔ g ∈ normalizer ↑H

Tactic:
by
  rw [← (normalizer H : Subgroup G).inv_mem_iff]
  simp only [Subgroup.ext_iff, mem_pointwise_smul_iff_inv_smul_mem,
    ← ConjAct.toConjAct_inv, ConjAct.toConjAct_smul, mem_normalizer_iff, inv_inv, Iff.comm]

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

Goal state before:
pp: case mul
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∃ f_1 t_1, ↑t_1 ⊆ s ∧ Function.support f_1 ⊆ ↑t_1 ∧ ∏ a ∈ t_1, a ^ f_1 a = (∏ a ∈ t, a ^ f a) * ∏ a ∈ u, a ^ g a

Tactic:
refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩

Goal state after:
case mul
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ a ∈ t ∪ u, a ^ (f + g) a = (∏ a ∈ t, a ^ f a) * ∏ a ∈ u, a ^ g a
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
⊢ ⇑(r.map f) = Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2

Tactic:
refine le_antisymm ?_ (sup_le Relation.EqvGen.rel (by rintro _ _ rfl; exact .refl _))
  rintro _ _ hxy
  induction hxy with
  | rel _ _ hab => exact .inl hab
  | refl _ => exact .inr rfl
  | symm _ _ _ ih => exact ih.imp (Std.Symm.symm _ _) (Std.Symm.symm _ _)
  | trans _ _ _ _ _ ih1 ih2 =>
    rcases ih1 with ih1 | rfl
    · rcases ih2 with ih2 | rfl
      · exact .inl <| r.iseqv.isTrans.map hf |>.trans _ _ _ ih1 ih2
      · exact .inl ih1
    · exact ih2

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : ι) → Decidable ¬p x
f : ι → M
⊢ (∏ x ∈ s with ¬p x, f x) * ∏ x ∈ s with p x, f x = ∏ x ∈ s, f x

Tactic:
by
  rw [mul_comm, prod_filter_mul_prod_filter_not]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι × ι → M
⊢ ∏ i ∈ s.diag, f i = ∏ i ∈ s, f (i, i)

Tactic:
by
  simp [diag]

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

Goal state before:
pp: case neg
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : Nonempty α
⊢ Function.Injective ⇑(map f)

Tactic:
· rw [Function.injective_iff_hasLeftInverse]
    use map (Function.invFun f)
    simp [Function.LeftInverse, map.comp, Function.invFun_comp hf]

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
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 ≠ 1

Tactic:
by simpa using (mem_filter.mp ha).2

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ x⁻¹ * y ∈ N ↔ ∃ z ∈ N, x * z = y

Tactic:
by
    simp only [← _root_.eq_inv_mul_iff_mul_eq, exists_eq_right]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
l : List ι
f : ι → M
⊢ (List.map f l).prod = ∏ m ∈ l.toFinset, f m ^ count m l

Tactic:
by
  induction l with
  | nil => simp only [map_nil, prod_nil, count_nil, pow_zero, prod_const_one]
  | cons a s IH =>
  simp only [List.map, List.prod_cons, toFinset_cons, IH]
  by_cases has : a ∈ s.toFinset
  · rw [insert_eq_of_mem has, ← insert_erase has, prod_insert (notMem_erase _ _),
      prod_insert (notMem_erase _ _), ← mul_assoc, count_cons_self, pow_succ']
    congr 1
    refine prod_congr rfl fun x hx => ?_
    rw [count_cons_of_ne (ne_of_mem_erase hx).symm]
  rw [prod_insert has, count_cons_self, count_eq_zero_of_not_mem (mt mem_toFinset.2 has), pow_one]
  grind [Finset.prod_congr]

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

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ mk ⁻¹' mk '' s → a ∈ ↑N * s

Tactic:
rintro ⟨b, hb, h⟩
    refine ⟨a / b, (QuotientGroup.eq_one_iff _).1 ?_, b, hb, div_mul_cancel _ _⟩
    simp only [h, QuotientGroup.mk_div, div_self']

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

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h : ∏ x ∈ s \ {x, g x hx}, f x = 1
hx' : g x hx ≠ x
⊢ ∏ x ∈ {x, g x hx}, f x = 1

Tactic:
| inr hx' =>

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g₁ g₂ g₃ : G
⊢ g₃ * ⁅g₁, g₂⁆ * g₃⁻¹ = ⁅g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹⁆

Tactic:
simp [mul_assoc, commutatorElement_def]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ ⁅a * b, c⁆ = a * ⁅b, c⁆ * a⁻¹ * ⁅a, c⁆

Tactic:
simp [mul_assoc, commutatorElement_def]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ ⁅a, b * c⁆ = ⁅a, b⁆ * b * ⁅a, c⁆ * b⁻¹

Tactic:
simp [mul_assoc, commutatorElement_def]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ ⁅a⁻¹, b⁆ = a⁻¹ * ⁅b, a⁆ * a

Tactic:
simp [mul_assoc, commutatorElement_def]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ ⁅a, b⁻¹⁆ = b⁻¹ * ⁅b, a⁆ * b

Tactic:
simp [mul_assoc, commutatorElement_def]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ a * ⁅⁅a⁻¹, b⁆, c⁆ * a⁻¹ * c * ⁅⁅c⁻¹, a⁆, b⁆ * c⁻¹ * b * ⁅⁅b⁻¹, c⁆, a⁆ * b⁻¹ = 1

Tactic:
simp [mul_assoc, commutatorElement_def]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ b * ⁅a, ⁅b⁻¹, c⁆⁆ * b⁻¹ * c * ⁅b, ⁅c⁻¹, a⁆⁆ * c⁻¹ * a * ⁅c, ⁅a⁻¹, b⁆⁆ * a⁻¹ = 1

Tactic:
simp [mul_assoc, commutatorElement_def]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ ⁅⁅a, b⁆, b * c * b⁻¹⁆ * ⁅⁅b, c⁆, c * a * c⁻¹⁆ * ⁅⁅c, a⁆, a * b * a⁻¹⁆ = 1

Tactic:
simp [mul_assoc, commutatorElement_def]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ ⁅a * b * a⁻¹, ⁅c, a⁆⁆ * ⁅c * a * c⁻¹, ⁅b, c⁆⁆ * ⁅b * c * b⁻¹, ⁅a, b⁆⁆ = 1

Tactic:
simp [mul_assoc, commutatorElement_def]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ ⁅a * b, c⁆ * ⁅c * a, b⁆ * ⁅b * c, a⁆ = 1

Tactic:
simp [mul_assoc, commutatorElement_def]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ ⁅a, b * c⁆ * ⁅b, c * a⁆ * ⁅c, a * b⁆ = 1

Tactic:
simp [mul_assoc, commutatorElement_def]

Goal state after:
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 : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
z : N
H : f ↑y * z = 1
⊢ ↑((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹ = z

Tactic:
← one_mul _⁻¹,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
z : N
H : f ↑y * z = 1
⊢ ↑(1 * ((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹) = z
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
x₁ x₂ : M
y₁ y₂ : ↥S
H : f (↑y₂ * x₁) = f (↑y₁ * x₂)
⊢ f x₁ = f (↑y₁ * x₂) * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y₂)⁻¹

Tactic:
← H,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f (↑y₂ * x₁) = f (↑y₁ * x₂)
⊢ f x₁ = f (↑y₂ * x₁) * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y₂)⁻¹
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
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f (x₁ * ↑y₂) = f (x₂ * ↑y₁)

Tactic:
by
  simp only [f.mk'_eq_iff_eq, mul_comm]

Goal state after:
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
P : Type u_3
inst✝ : CommMonoid P
y : ↥S
⊢ mk (↑y) 1 * mk 1 y = 1

Tactic:
by rw [mk_mul, mul_one, one_mul, mk_self]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
a : α
⊢ 1 * ↑a = ↑a

Tactic:
by rw [← coe_one, ← coe_mul, one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccLimit a
this : ¬IsMin a
⊢ ¬IsMin ↑a

Tactic:
not_isMin_iff

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccLimit a
this : ∃ b, b < a
⊢ ∃ b, b < ↑a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
⊢ a ≤ succ a ∧ succ a ≤ succ a

Tactic:
exact ⟨le_succ a, le_rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
⊢ pred^[n] x = x - ↑n

Tactic:
by
  induction n with
  | zero =>
    rw [Function.iterate_zero_apply, Nat.cast_zero, sub_zero]
  | succ n IH =>
    rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
σ : α → Type u_6
s : Finset α
t : (a : α) → Finset (σ a)
f : Sigma σ → β
⊢ ∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩

Tactic:
← disjiUnion_map_sigma_mk,

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
σ : α → Type u_6
s : Finset α
t : (a : α) → Finset (σ a)
f : Sigma σ → β
⊢ ∏ x ∈ s.disjiUnion (fun i ↦ map (Embedding.sigmaMk i) (t i)) ⋯, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
⊢ { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 } =
    { toFunctor := F2, pure := p1, seq := s2, seqLeft := sl2, seqRight := sr2 }

Tactic:
obtain rfl : @s1 = @s2 := by
      funext α β f x
      exact H2 f (x Unit.unit)

Goal state after:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
⊢ { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 } =
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
i : Fin 0
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
exact i.elim0

Goal state after: