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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g
a : ↥s
x✝¹ : a ∈ ↑s.attach
b : ↥s
x✝ : b ∈ ↑s.attach
hab : a ≠ b
x : γ
hxa : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) a
hxb : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) b
xa : β
hfa : xa ∈ f ↑a
hga : x ∈ g xa
⊢ False

Tactic:
obtain ⟨xb, hfb, hgb⟩ := mem_disjiUnion.mp hxb

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g
a : ↥s
x✝¹ : a ∈ ↑s.attach
b : ↥s
x✝ : b ∈ ↑s.attach
hab : a ≠ b
x : γ
hxa : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) a
hxb : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) b
xa : β
hfa : xa ∈ f ↑a
hga : x ∈ g xa
xb : β
hfb : xb ∈ f ↑b
hgb : x ∈ g xb
⊢ False
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case nil
α : Type u
n : ℕ
⊢ [].rotate n ~r []

pp: case cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ (hd :: tl).rotate n ~r hd :: tl

Tactic:
· exists 0

Goal state after:
case cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ (hd :: tl).rotate n ~r hd :: tl
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
hf : Function.Injective f
⊢ s.disjiUnion (fun a ↦ {f a}) ⋯ = map { toFun := f, inj' := hf } s

Tactic:
by
  ext; simp [eq_comm]

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

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

Tactic:
by
  apply Nat.mul_left_cancel k.factorial_pos
  rw [← ascFactorial_eq_factorial_mul_choose]
  exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : DecidablePred fun x ↦ x ∈ s ^ n
⊢ DecidablePred fun x ↦ x ∈ s ^ (n + 1)

Tactic:
rw [pow_succ]
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Monoid N
g : N →* M
x✝ : α
⊢ 1 • x✝ = x✝

Tactic:
simpa [(· • ·)] using one_smul ..

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

Goal state before:
pp: case negSucc
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.negSucc a✝ = a * b ^ Int.negSucc a✝ * a⁻¹

Tactic:
simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]

Goal state after:
case negSucc
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ a * ((b ^ (a✝ + 1))⁻¹ * a⁻¹) = a * (b ^ (a✝ + 1))⁻¹ * a⁻¹
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ kernImage f ∅ = (range f)ᶜ

Tactic:
by
  rw [kernImage_eq_compl, compl_empty, image_univ]

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
m : M
⊢ (∀ (b : Subsemigroup M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔
    ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
simp only [closure_singleton_le_iff_mem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ i, s i)
⊢ SurjOn f (⋂ i, s i) t

Tactic:
by
  intro y hy
  rw [Hinj.image_iInter_eq, mem_iInter]
  exact fun i => H i hy

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k

Tactic:
by_cases i = k

Goal state after:
case pos
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h✝ : i = k
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k

case neg
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h✝ : ¬i = k
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = ⋃ i ∈ s, ⋃ j ∈ t, {f i j}

Tactic:
by
  ext; simp [eq_comm]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ (∀ (b : Submonoid M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
simp only [closure_singleton_le_iff_mem]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
⊢ H ≤ comap f (map f K) ↔ H ≤ K ⊔ f.ker

Tactic:
comap_map_eq

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
⊢ H ≤ K ⊔ f.ker ↔ H ≤ K ⊔ f.ker
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ (match n.bodd, n / 2 with
    | false, m => Option.map Sum.inl (decode m)
    | x, m => Option.map Sum.inr (decode m)) =
    none

Tactic:
cases bodd n <;> simp [e]

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) (none.bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    none.bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)

Tactic:
cases (decode n.unpair.2 : Option β)

Goal state after:
case none.none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) (none.bind fun a ↦ Option.map (Sigma.mk a) none) =
    none.bind fun a ↦ Option.map (Prod.mk a) none

case none.some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝ : β
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) (none.bind fun a ↦ Option.map (Sigma.mk a) (some val✝)) =
    none.bind fun a ↦ Option.map (Prod.mk a) (some val✝)
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝ : α
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) ((some val✝).bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    (some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)

Tactic:
cases (decode n.unpair.2 : Option β)

Goal state after:
case some.none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝ : α
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) ((some val✝).bind fun a ↦ Option.map (Sigma.mk a) none) =
    (some val✝).bind fun a ↦ Option.map (Prod.mk a) none

case some.some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) ((some val✝¹).bind fun a ↦ Option.map (Sigma.mk a) (some val✝)) =
    (some val✝¹).bind fun a ↦ Option.map (Prod.mk a) (some val✝)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_4
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ g * x⁻¹ * g⁻¹ ∈ normalClosure s

Tactic:
· rw [← conj_inv]
      exact inv_mem ihx

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ (Subgroup.map f H).Normal

Tactic:
rw [← normalizer_eq_top_iff, ← top_le_iff, ← f.range_eq_top_of_surjective hf, f.range_eq_map,
    ← H.normalizer_eq_top]
  exact le_normalizer_map _

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
⊢ normalClosure s ≤ comap f (normalClosure (⇑f '' s))

Tactic:
simp [normalClosure_le_normal, ← Set.image_subset_iff, subset_normalClosure]

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h) ⟨c⁻¹ * x * c, ⋯⟩ = ⟨x, hx⟩

Tactic:
simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply,
      MonoidHom.domRestrict_apply, Subtype.mk_eq_mk, ← mul_assoc, mul_inv_cancel, one_mul]

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ x * c * c⁻¹ = x
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LE β
t c : Lex (α × β)
h : t ≤ c
⊢ (ofLex t).1 ≤ (ofLex c).1

Tactic:
by
  cases toLex_le_toLex.mp h with
  | inl h' => exact h'.le
  | inr h' => exact h'.1.le

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

Goal state before:
pp: case mp
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ Lex r s a b → r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

Tactic:
rintro (⟨a, b, hij⟩ | ⟨i, hab⟩)
    · exact Or.inl hij
    · exact Or.inr ⟨rfl, hab⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
s : Submonoid M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
by
  rw [← SetLike.le_def]
  exact le_sSup hs

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

Goal state before:
pp: case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ foldl (argAux r) (foldl (argAux r) o tl) [a]
⊢ ¬r b m

Tactic:
foldl_cons,

Goal state after:
case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ foldl (argAux r) (argAux r (foldl (argAux r) o tl) a) []
⊢ ¬r b m
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ inr b ∈ s.disjSum t ↔ b ∈ t

Tactic:
by
  rw [mem_disjSum, or_iff_right]
  · simp only [inr.injEq, exists_eq_right]
  rintro ⟨a, _, ha⟩
  exact inl_ne_inr ha

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.min' ⋯ = a

Tactic:
simp [min']

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

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

Tactic:
simp [revzip]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ (powersetAux l₁).revzip ~ (powersetAux l₂).revzip

Tactic:
by
  have := Classical.decEq α
  simp only [fun l : List α => revzip_powersetAux_lemma l revzip_powersetAux, coe_eq_coe.2 p]
  exact (powersetAux_perm p).map _

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

Goal state before:
pp: case succ
α✝ : 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 : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
this : card (Option (ULift.{?u.79, 0} (Fin n))) = card (ULift.{?u.82, 0} (Fin n.succ))
e : Option (ULift.{?u.79, 0} (Fin n)) ≃ ULift.{?u.82, 0} (Fin n.succ)
⊢ Trunc (P (ULift.{u, 0} (Fin (n + 1))))

Tactic:
apply Trunc.map _ ih

Goal state after:
α✝ : 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 : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
this : card (Option (ULift.{?u.79, 0} (Fin n))) = card (ULift.{?u.82, 0} (Fin n.succ))
e : Option (ULift.{?u.79, 0} (Fin n)) ≃ ULift.{?u.82, 0} (Fin n.succ)
⊢ P (ULift.{u, 0} (Fin n)) → P (ULift.{u, 0} (Fin (n + 1)))
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:
← biUnion_range

Goal state after:
α : Type u
β : Type v
f : α → Finset β
h : (range f).Finite
⊢ (⋃ x ∈ range f, ↑x).Finite
Module: Mathlib.Order.Cover

Goal state before:
pp: ⊢ ∀ {a b : Bool}, a ⩿ b ↔ a ≤ b

Tactic:
unfold WCovBy

Goal state after:
⊢ ∀ {a b : Bool}, (a ≤ b ∧ ∀ ⦃c : Bool⦄, a < c → ¬c < b) ↔ a ≤ b
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
⊢ a ⩿ b → ∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
intro h
    obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h
    exact ⟨i, h.eval _, hi⟩

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 γ
h : b.fst ≠ x.fst
⊢ x ∉ sigmaLift f a b

Tactic:
by
  rw [mem_sigmaLift]
  exact fun H => h H.snd.fst

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case inr
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
a : α
ha : Maximal (fun x ↦ x ∈ s) a
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t

Tactic:
(Mathlib.Tactic.useSyntax
 "use"
 []
 (group)
 [(choice
   («term{_}» "{" [`a] "}")
   (Term.structInst
    "{"
    []
    (Term.structInstFields [(Term.structInstField (Term.structInstLVal `a []) [])])
    (Term.optEllipsis [])
    []
    "}"))])

Goal state after:
case h
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
a : α
ha : Maximal (fun x ↦ x ∈ s) a
⊢ {a}.Subsingleton ∧ IsCofinal {a}
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DenselyOrdered α
⊢ Ioo a b = 0 ↔ ¬a < b

Tactic:
rw [Ioo, Finset.val_eq_zero, Finset.Ioo_eq_empty_iff]

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

Goal state before:
pp: b : ℕ
⊢ b + 1 - ⊥ = b + 1

Tactic:
Nat.bot_eq_zero,

Goal state after:
b : ℕ
⊢ b + 1 - 0 = b + 1
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: b : ℕ
⊢ b - ⊥ = b

Tactic:
Nat.bot_eq_zero,

Goal state after:
b : ℕ
⊢ b - 0 = b
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
h₁ : n ≤ sInf {m | p (m - n)}
⊢ sInf {m | p m} + n = sInf {m | p (m - n)}

Tactic:
convert! sInf_add h₁
    simp_rw [Nat.add_sub_cancel_right]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : DecidableLT α
inst✝ : LocallyFiniteOrder α
a b : { x // x < y }
⊢ b ∈ Finset.subtype (fun x ↦ x < y) (Ioo (↑a) y) ↔ a < b

Tactic:
by
    simp only [Finset.mem_subtype, Finset.mem_Ioo, Subtype.coe_lt_coe, and_iff_left_iff_imp]
    exact fun _ => b.property

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

Goal state before:
pp: case mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := ⋯
f : α → Quotient (orbitRel G α) := ⋯
a : α
⊢ a ∈ f ⁻¹' f '' U → a ∈ ⋃ g, (fun x ↦ g • x) '' U

pp: case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := ⋯
f : α → Quotient (orbitRel G α) := ⋯
a : α
⊢ a ∈ ⋃ g, (fun x ↦ g • x) '' U → a ∈ f ⁻¹' f '' U

Tactic:
· rintro ⟨b, hb, hab⟩
    obtain ⟨g, rfl⟩ := Quotient.exact hab
    rw [Set.mem_iUnion]
    exact ⟨g⁻¹, g • a, hb, inv_smul_smul g a⟩

Goal state after:
case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := ⋯
f : α → Quotient (orbitRel G α) := ⋯
a : α
⊢ a ∈ ⋃ g, (fun x ↦ g • x) '' U → a ∈ f ⁻¹' f '' U
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
g✝ : Mˣ
⊢ ↑g✝ * ↑x✝ = ↑x✝ * ↑g✝

Tactic:
ha.comm

Goal state after:
M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
g✝ : Mˣ
⊢ ↑g✝ * ↑x✝ = ↑g✝ * ↑x✝
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
⊢ ↑(ConjAct.ofConjAct ↑u) ∈ Submonoid.centralizer {↑x}

Tactic:
rintro x ⟨rfl⟩

Goal state after:
α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
⊢ ↑x * ↑(ConjAct.ofConjAct ↑u) = ↑(ConjAct.ofConjAct ↑u) * ↑x
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
n : G
hmem : n ∈ ↑(H ⊔ K)
g : G
⊢ g * n * g⁻¹ ∈ ↑(H ⊔ K)

Tactic:
normal_mul

Goal state after:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
n : G
hmem : n ∈ ↑H * ↑K
g : G
⊢ g * n * g⁻¹ ∈ ↑H * ↑K
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

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

Tactic:
by
  simp [ofMul]; rfl

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

Goal state before:
pp: case trans.inl.inr
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
i✝¹ i✝ x✝ y✝ : β
a✝¹ : Relation.EqvGen (Relation.Map (⇑r) f f) x✝ y✝
ih1 : Relation.Map (⇑r) f f x✝ y✝
a✝ : Relation.EqvGen (Relation.Map (⇑r) f f) y✝ y✝
⊢ (Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2) x✝ y✝

Tactic:
exact .inl ih1

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
r : Setoid α
hf : ker f ≤ r
x y : α
h : f x = f y
⊢ r x y

Tactic:
· exact hf h

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝ : CommMonoid M
f : ι → M
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁.disjUnion s₂ h, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x

Tactic:
by
  refine Eq.trans ?_ (fold_disjUnion h)
  rw [one_mul]
  rfl

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

Goal state before:
pp: 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}

Tactic:
#adaptation_note /-- 2025-09-12 (kmill) copied from private lemma pairwiseDisjoint_fibers -/

Goal state after:
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: 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}

Tactic:
#adaptation_note /-- 2025-09-12 (kmill) copied from private lemma pairwiseDisjoint_fibers -/

Goal state after:
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: ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
| ∏ a ∈ s₁ \ s₂ ∪ s₁ ∩ s₂, f a

Tactic:
prod_union_eq_right (by simp_all)

Goal state after:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
| ∏ a ∈ s₁ ∩ s₂, f 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
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
⊢ ∏ x ∈ s, f x = 1

Tactic:
by
    rw [← prod_sdiff this, h, one_mul]
    cases eq_or_ne (g x hx) x with
    | inl hx' => simpa [hx'] using hg₃ x hx
    | inr hx' => grind

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
inst✝ : AddCommGroup G
f g : α → G
a : FreeAbelianGroup α
⊢ (lift (f + g)) a = (lift f) a + (lift g) a

Tactic:
induction a using FreeAbelianGroup.induction_on with
  | zero => simp only [(lift _).map_zero, zero_add]
  | of x => simp only [lift_apply_of, Pi.add_apply]
  | neg x => simp only [map_neg, lift_apply_of, Pi.add_apply, neg_add]
  | add x y hx hy => simp only [(lift _).map_add, hx, hy, add_add_add_comm]

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

Goal state before:
pp: case h
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)
H : Surjective ⇑(f.lift hg)
v : P
z : N
hz : (f.lift hg) z = v
x : M × ↥S
hx : z * f ↑x.2 = f x.1
⊢ g x.1 * (↑((IsUnit.liftRight (g.domRestrict S) hg) x.2)⁻¹ * g ↑x.2) = g x.1

Tactic:
mul_comm _ (g ↑x.2),

Goal state after:
case h
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)
H : Surjective ⇑(f.lift hg)
v : P
z : N
hz : (f.lift hg) z = v
x : M × ↥S
hx : z * f ↑x.2 = f x.1
⊢ g x.1 * (g ↑x.2 * ↑((IsUnit.liftRight (g.domRestrict S) hg) x.2)⁻¹) = g x.1
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : WithZero G ≃*o WithZero H
⊢ (fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ }) x✝) =
    x✝

Tactic:
by ext x; cases x <;> simp

Goal state after: