mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ sup ?m.35 = s₁.sup ⊔ s₂.sup

pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ ?m.35

Tactic:
sup_add

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ sup ?s₁ ⊔ sup ?s₂ = s₁.sup ⊔ s₂.sup

case s₁
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

case s₂
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ ?s₁ + ?s₂
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ sup ?m.35 = s₁.sup ⊔ s₂.sup

pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ ?m.35

Tactic:
sup_add

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ sup ?s₁ ⊔ sup ?s₂ = s₁.sup ⊔ s₂.sup

case s₁
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

case s₂
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ ?s₁ + ?s₂
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ decode n = some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩

Tactic:
decode_sigma_val

Goal state after:
α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ ((decode (unpair n).1).bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ (⇑f ∘ ⇑g) (a ⊔ b) = (⇑f ∘ ⇑g) a ⊔ (⇑f ∘ ⇑g) b

Tactic:
rw [comp_apply, map_sup, map_sup]; rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : s.Nonempty
⊢ i ∈ ↑s

Tactic:
exact ((isGLB_iff_isLeast i s hs).mp his).1

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

Goal state before:
pp: α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
⊢ Pairwise (Lex (Function.swap R)) (a :: l).sublists'

Tactic:
simp only [sublists'_cons, pairwise_append, pairwise_map, mem_sublists', mem_map, exists_imp,
      and_imp]

Goal state after:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
⊢ Pairwise (Lex (Function.swap R)) l.sublists' ∧
    Pairwise (fun a_1 b ↦ Lex (Function.swap R) (a :: a_1) (a :: b)) l.sublists' ∧
      ∀ (a_1 : List α), a_1 <+ l → ∀ (b x : List α), x <+ l → a :: x = b → Lex (Function.swap R) a_1 b
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
l : List α
h : l.Nodup
⊢ (sublistsLen n l).Nodup

Tactic:
have : Pairwise (· ≠ ·) l.sublists' := Pairwise.imp
    (fun h => Lex.to_ne (by convert! h using 3; simp [eq_comm])) h.sublists'

Goal state after:
α : Type u
n : ℕ
l : List α
h : l.Nodup
this : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l.sublists'
⊢ (sublistsLen n l).Nodup
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case insert.inr.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : s.sup f ≤ f a
⊢ max (f a) (s.sup f) ∈ f '' insert a ↑s

Tactic:
sup_eq_left.mpr ha

Goal state after:
case insert.inr.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : s.sup f ≤ f a
⊢ f a ∈ f '' insert a ↑s
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Nonempty ι
f : ι → α
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hf : BddAbove (range f)
⊢ Ici (⨆ i, f i) = ⋂ i, Ici (f i)

Tactic:
by
  ext
  simpa using hd.ciSup_le_iff hf

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
⊢ ⋃ j, ⋂ x, eval ↑x ⁻¹' s (↑x) j = ⋂ x, ⋃ i, eval ↑x ⁻¹' s (↑x) i

Tactic:
have := hI.fintype.finite

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
this : Finite ↑I
⊢ ⋃ j, ⋂ x, eval ↑x ⁻¹' s (↑x) j = ⋂ x, ⋃ i, eval ↑x ⁻¹' s (↑x) i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

Tactic:
rw [Set.image_empty, cbiSup_empty, cbiSup_empty]

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
⊢ Disjoint (map (Embedding.sigmaMk i) (t i)) (map (Embedding.sigmaMk j) (t j))

Tactic:
disjoint_left

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk i) (t i) → a ∉ map (Embedding.sigmaMk j) (t j)
Module: Mathlib.Data.Finset.Sigma

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

Tactic:
rintro ⟨⟨⟩, ⟨⟩, hx⟩
      rw [sigmaLift, dif_pos rfl, mem_map]
      exact ⟨_, hx, by simp⟩

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

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

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_left hca]

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hca : c ≤ a
⊢ ∅.val = ∅
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: ⊢ sInf ∅ = 0

Tactic:
rw [sInf_eq_zero]

Goal state after:
⊢ 0 ∈ ∅ ∨ ∅ = ∅
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | a ≠ x ∧ x ≠ b} ↔ a < x ∧ x < b

Tactic:
rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_and_ne, lt_iff_le_and_ne]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ ∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t

Tactic:
by
  classical
    have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
      simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
        Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
    cases this
    exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
      ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
h : WellFoundedGT α
a : ℕ →o α
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

Tactic:
obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.wf.has_min _ (Set.range_nonempty a)

Goal state after:
case refine_1
α : Type u_1
inst✝ : Preorder α
h : WellFoundedGT α
a : ℕ →o α
n : ℕ
H : ∀ x ∈ Set.range ⇑a, ¬a n < x
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
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
⊢ map (Embedding.subtype p) (Ioo a b) = Ioo ↑a ↑b

Tactic:
subtype_Ioo_eq

Goal state after:
α : 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
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioo ↑a ↑b)) = Ioo ↑a ↑b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), ↑(f (g n)) ∈ t
⊢ ∃ m n, m < n ∧ Subrel r (fun x ↦ x ∈ s ∪ t) (f m) (f n)

Tactic:
rcases ht.exists_lt hgt with ⟨m, n, hlt, hr⟩
    exact ⟨g m, g n, g.strictMono hlt, hr⟩

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

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : Set M
S : Submonoid M
n : ℕ
hs : s ⊆ ↑S
⊢ s ^ n ⊆ ↑S

Tactic:
induction n <;> simp [pow_succ, *]

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 α
⊢ Injective orbit

Tactic:
by
  intro x y h
  simp_rw [orbitRel.Quotient.orbit_eq_orbit_out _ Quotient.out_eq', orbit_eq_iff,
    ← orbitRel_apply] at h
  simpa [← Quotient.eq''] using h

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
⊢ x ≤ y ↔ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

Tactic:
by
  refine ⟨transGen_wcovBy_of_le, fun h ↦ ?_⟩
  induction h with
  | single h => exact h.le
  | tail _ h₁ h₂ => exact h₂.trans h₁.le

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case neg
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m - g 0 < n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ List.SublistForall₂ r (f (g (m - g 0))) (f (g n'))

Tactic:
← List.cons_head!_tail (hnil (g (m - g 0))),

Goal state after:
case neg
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m - g 0 < n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ List.SublistForall₂ r ((f (g (m - g 0))).head! :: (f (g (m - g 0))).tail) (f (g n'))
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
H : Subgroup G
n : ℕ
hs : s ⊆ ↑H
⊢ s ^ n ⊆ ↑H

Tactic:
induction n <;> simp [pow_succ, *]

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

Goal state before:
pp: case mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y ∈ ↑C, x * y = x✝) → x✝ ∈ ↑A ∧ ∃ x ∈ ↑B, ∃ y ∈ ↑C, x * y = x✝

Tactic:
rintro ⟨y, ⟨hyA, hyB⟩, z, hz, rfl⟩

Goal state after:
case mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hyA : y ∈ ↑A
hyB : y ∈ ↑B
z : G
hz : z ∈ ↑C
⊢ y * z ∈ ↑A ∧ ∃ x ∈ ↑B, ∃ y_1 ∈ ↑C, x * y_1 = y * z
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
f : ι → M
inst✝¹ : CommMonoid M
inst✝ : IsEmpty ι
s : Finset ι
⊢ ∏ i ∈ ∅, f i = 1

Tactic:
prod_empty

Goal state after:
ι : Type u_1
M : Type u_3
f : ι → M
inst✝¹ : CommMonoid M
inst✝ : IsEmpty ι
s : Finset ι
⊢ 1 = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
⊢ ∏ k ∈ ∅, f k = 1

Tactic:
prod_empty

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
⊢ 1 = 1
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
⊢ ∏ a ∈ t ∪ u, a ^ (f + g) a = (∏ a ∈ t, a ^ f a) * ∏ a ∈ u, a ^ g a

Tactic:
simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]

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
⊢ (∏ x ∈ t ∪ u, x ^ f x) * ∏ x ∈ t ∪ u, x ^ g x = (∏ x ∈ t, x ^ f x) * ∏ x ∈ u, x ^ g x
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
s : Finset M
⊢ x ∈ closure ↑s → ∃ f, Function.support f ⊆ ↑s ∧ ∏ a ∈ s, a ^ f a = x

Tactic:
by
    rw [mem_closure_iff_exists_finset_subset]
    rintro ⟨f, t, hts, hf, rfl⟩
    refine ⟨f, hf.trans hts, .symm <| Finset.prod_subset hts ?_⟩
    simp +contextual [Function.support_subset_iff'.1 hf]

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

Goal state before:
pp: α : Type u_1
s : Set (Setoid α)
⊢ sSup s = EqvGen.setoid (sSup (@r α '' s))

Tactic:
sSup_eq_eqvGen,

Goal state after:
α : Type u_1
s : Set (Setoid α)
⊢ (EqvGen.setoid fun x y ↦ ∃ r ∈ s, r x y) = EqvGen.setoid (sSup (@r α '' s))
Module: Mathlib.Data.Setoid.Basic

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

Tactic:
exact .inr rfl

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 g : ι → M
inst✝ : DecidableEq ι
h : s₁ ⊆ s₂
hg : ∀ x ∈ s₂ \ s₁, g x = 1
hfg : ∀ x ∈ s₁, f x = g x
⊢ ∏ i ∈ s₁, f i = ∏ i ∈ s₂, g i

Tactic:
rw [← prod_sdiff h, prod_eq_one hg, one_mul]

Goal state after:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f g : ι → M
inst✝ : DecidableEq ι
h : s₁ ⊆ s₂
hg : ∀ x ∈ s₂ \ s₁, g x = 1
hfg : ∀ x ∈ s₁, f x = g x
⊢ ∏ i ∈ s₁, f i = ∏ x ∈ s₁, g x
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ Function.LeftInverse (fun x ↦ of () ^ x) fun x ↦ ((map fun x ↦ 1) x).sum

Tactic:
by
    rintro ⟨L⟩
    simp only [quot_mk_eq_mk, map.mk, sum_mk, List.map_map]
    exact List.recOn L
     rfl
     (fun ⟨⟨⟩, b⟩ tl ih => by
        cases b <;> simp [zpow_add, ih] <;> rfl)

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

Goal state before:
pp: case of
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : α
⊢ (fun x ↦ of default ^ x) ((fun x ↦ ((map 1) x).sum) (of x)) = of x

Tactic:
| of x =>

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

Goal state before:
pp: case of
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : α
⊢ (fun x ↦ x • FreeAddGroup.of default) ((fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) (FreeAddGroup.of x)) =
    FreeAddGroup.of x

Tactic:
| of x =>

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ x ∈ range (n + 1), f x = (∏ x ∈ range n, f x) * f n

Tactic:
by
  simp only [mul_comm, prod_range_succ_comm]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ closure ↑(Finset.image (⇑e) s) = Submonoid.map e (closure ↑s)

Tactic:
rw [Finset.coe_image, MonoidHom.map_mclosure]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddCommGroup β
f : α → β
x : α
⊢ (lift f) (of x) = f x

Tactic:
convert! Abelianization.lift_apply_of (FreeGroup.lift f (β := Multiplicative β)) (FreeGroup.of x)
  exact (FreeGroup.lift_apply_of (β := Multiplicative β)).symm

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
| of x =>

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

Goal state before:
pp: ι : Type u_1
κ : Type u_5
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
⊢ ∑ j ∈ t, #({i ∈ s | g i = j}) = #({i ∈ s | g i ∈ t})

Tactic:
by
  simpa only [card_eq_sum_ones] using sum_fiberwise_eq_sum_filter _ _ _ _

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₁

Tactic:
mul_inv_eq_iff_eq_mul

Goal state after:
G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ g₁ * g₂ = g₂ * g₁ ↔ g₁ * g₂ = g₂ * g₁
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * 1⁻¹ * y⁻¹ * x⁻¹ = 1

Tactic:
h2 _ (H₃.inv_mem hz) _ (H₁.inv_mem hx) _ hy

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * 1⁻¹ * z⁻¹ * y * 1⁻¹ * y⁻¹ * x⁻¹ = 1
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H ≤ centralizer ↑⊤ ↔ H ≤ center G

Tactic:
coe_top,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H ≤ centralizer Set.univ ↔ H ≤ center G
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.zero
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 : α
⊢ x * 0 * of L3 = x * (0 * of L3)

Tactic:
simp only [mul_zero, zero_mul]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅⊤, H⁆ ≤ H ↔ H.Normal

Tactic:
refine ⟨fun hle ↦ ⟨fun h hh g ↦ ?_⟩, fun h ↦ commutator_le_right ⊤ H⟩
  exact (H.mul_mem_cancel_right <| H.inv_mem hh).mp <| commutator_le.mp hle g trivial h hh

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ H₁ ≤ normalizer ↑⁅H₁, H₂⁆

Tactic:
apply le_normalizer_closure_iff.mpr

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ ∀ h ∈ H₁,
    ∀ g ∈ {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}, h * g * h⁻¹ ∈ closure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

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
a b c : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑c.2 * b.1) = ↑t₂ * (↑b.2 * c.1)
⊢ ↑t₂ * ↑t₁ * ↑b.2 * (↑c.2 * a.1) = ↑t₂ * ↑t₁ * ↑b.2 * (↑a.2 * c.1)

Tactic:
calc
      (t₂ * t₁ * b.2 : M) * (c.2 * a.1) = t₂ * c.2 * (t₁ * (b.2 * a.1)) := by ac_rfl
      _ = t₁ * a.2 * (t₂ * (c.2 * b.1)) := by rw [ht₁]; ac_rfl
      _ = t₂ * t₁ * b.2 * (a.2 * c.1) := by rw [ht₂]; ac_rfl

Goal state after:
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
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ w * (f ↑a.2 * f ↑b.2) = f ↑a.2 * f b.1

Tactic:
← hb

Goal state after:
case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ w * (f ↑a.2 * f ↑b.2) = f ↑a.2 * (w * f ↑b.2)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s t : ↥S
⊢ (r₁ * ↑s /ₒ t) • (r₂ /ₒ s) = r₁ • r₂ /ₒ t

Tactic:
by
  simp [oreDiv_smul_char (r₁ * s) r₂ t s r₁ 1 (by simp)]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
⊢ a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0

Tactic:
by rw [mul_def]; aesop

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
⊢ a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0

Tactic:
by rw [mul_def]; aesop

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
ha : a ≠ ⊤
⊢ sInf (Ioi a) ≤ succ a

Tactic:
exact sInf_le (lt_succ_iff_ne_top.2 ha)

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

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
⊢ IsMax a

Tactic:
by
  classical
  rw [← succ_eq_iff_isMax]
  change dite .. = _
  split_ifs <;> trivial

Goal state after:
Module: Mathlib.Data.Countable.Small

Goal state before:
pp: α : Type v
h : ¬Small.{w, v} α
⊢ Uncountable α

Tactic:
rw [uncountable_iff_not_countable]

Goal state after:
α : Type v
h : ¬Small.{w, v} α
⊢ ¬Countable α
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : WithBot ℕ∞
m : ℕ
⊢ n < ↑m + ↑↑1 ↔ n ≤ ↑m

Tactic:
WithBot.coe_natCast,

Goal state after:
n : WithBot ℕ∞
m : ℕ
⊢ n < ↑m + ↑1 ↔ n ≤ ↑m