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

Goal state before:
pp: α : Type u
s : Set (Set α)
hs : s.Finite
H : ∀ t ∈ s, t.Finite
⊢ (⋃₀ s).Finite

Tactic:
simpa only [sUnion_eq_biUnion] using hs.biUnion H

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : Preorder α
inst✝ : SupSet α
f : ι → α
h : BddAbove (range f)
⊢ ↑(⨆ i, f i) = ⨆ i, ↑(f i)

Tactic:
rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp, Function.comp_def]

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

Goal state before:
pp: case pos
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
i : ι
h : i ∈ s
⊢ ⨅ i ∈ s, ↑(f i) ≤ ↑(⨅ (_ : i ∈ s), f i)

pp: case neg
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
i : ι
h : i ∉ s
⊢ ⨅ i ∈ s, ↑(f i) ≤ ↑(⨅ (_ : i ∈ s), f i)

Tactic:
· simpa only [iInf_pos h] using by apply biInf_le _ h

Goal state after:
case neg
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
i : ι
h : i ∉ s
⊢ ⨅ i ∈ s, ↑(f i) ≤ ↑(⨅ (_ : i ∈ s), f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h✝ : IsEmpty ι
⊢ ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x

pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h✝ : Nonempty ι
⊢ ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x

Tactic:
· simp [iSup_of_empty']

Goal state after:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h✝ : Nonempty ι
⊢ ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝ : IsEmpty β
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝ : Nonempty β
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

Tactic:
· simp [iSup_of_empty']

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝ : Nonempty β
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : IsEmpty γ
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

Tactic:
· simp [iSup_of_empty']

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun x ↦ x ∈ s) f j
hji : f j ≤ f i
⊢ ∀ ⦃j : ι⦄, (fun x ↦ x ∈ cons i s hi) j → f i ≤ f j → f j ≤ f i

Tactic:
simp only [mem_cons, forall_eq_or_imp, imp_self, true_and]

Goal state after:
case pos
ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun x ↦ x ∈ s) f j
hji : f j ≤ f i
⊢ ∀ a ∈ s, f i ≤ f a → f a ≤ f i
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
t : Set β
f : α → β
inst✝ : Infinite α
hf : ∀ (a : α), f a ∈ t
ht : t.Finite
⊢ ∃ a b, a < b ∧ f a = f b

Tactic:
rw [← mapsTo_univ_iff] at hf

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
t : Set β
f : α → β
inst✝ : Infinite α
hf : MapsTo f univ t
ht : t.Finite
⊢ ∃ a b, a < b ∧ f a = f b
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
hcb : c ≤ b
⊢ {x ∈ Finset.Ico a b | x < c}.val = Ico a c

Tactic:
Finset.Ico_filter_lt_of_le_right hcb

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

Goal state before:
pp: case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
have hp : ∃ n, n ∈ { m | p m } := ⟨_, hm⟩
    rw [Nat.sInf_def ⟨m, hm⟩, Nat.sInf_def hp]
    rw [Nat.sInf_def hp] at hn
    exact find_add hn

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

Goal state before:
pp: case zero
a : ℕ
⊢ Set.InjOn (fun x ↦ x % a) ↑(Ico 0 (0 + a))

Tactic:
simp only [zero_add, Ico_zero_eq_range]
    rintro k hk l hl (hkl : k % a = l % a)
    simp only [Finset.mem_range, Finset.mem_coe] at hk hl
    rwa [mod_eq_of_lt hk, mod_eq_of_lt hl] at hkl

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

Goal state before:
pp: a : ℕ
⊢ (range a).toFinset = Finset.range a

Tactic:
ext x
  rw [List.mem_toFinset, List.mem_range, Finset.mem_range]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a b x : WithTop α
⊢ (x ∈
      match a, b with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    a < x ∧ x ≤ b

Tactic:
cases a <;> cases b <;> cases x

Goal state after:
case top.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
⊢ (⊤ ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < ⊤ ∧ ⊤ ≤ ⊤

case top.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < ↑a✝ ∧ ↑a✝ ≤ ⊤

case top.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < ⊤ ∧ ⊤ ≤ ↑a✝

case top.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ↑a✝¹ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < ↑a✝ ∧ ↑a✝ ≤ ↑a✝¹

case coe.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝ < ⊤ ∧ ⊤ ≤ ⊤

case coe.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝¹, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝¹ < ↑a✝ ∧ ↑a✝ ≤ ⊤

case coe.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (⊤ ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝¹ < ⊤ ∧ ⊤ ≤ ↑a✝

case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝² a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝², ↑a✝¹ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝² < ↑a✝ ∧ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ m = n

pp: case refine_1.inr.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m = n
⊢ m = n

pp: case refine_1.inr.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ m = n

Tactic:
· refine (H _ _ h ?_).elim
      rw [hmn]
      exact refl _

Goal state after:
case refine_1.inr.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m = n
⊢ m = n

case refine_1.inr.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ m = n
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ ≤ (closure s)⁻¹

Tactic:
rw [closure_le, coe_inv, ← Set.inv_subset, inv_inv]
    exact subset_closure

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1.inr.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ m = n

Tactic:
· refine (H _ _ h ?_).elim
      rw [hmn]
      exact refl _

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
simp_rw [disjoint_iff_inter_eq_empty, Ioc_inter_Ioc, Ioc_eq_empty_iff, not_lt]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
⊢ ∀ (b : M), 1 • b = b

Tactic:
simp [units_smul_def]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
⊢ ∀ (r : ConjAct Mˣ), r • 1 = 1

Tactic:
simp [units_smul_def]

Goal state after:
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
⊢ ↑(H ⊔ N) = ↑H * ↑N

Tactic:
sup_eq_closure_mul

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).prod % n = (∏ i ∈ s, f i % n) % n

Tactic:
rw [Finset.prod, Multiset.map_map]; rfl

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).prod % n = (∏ i ∈ s, f i % n) % n

Tactic:
rw [Finset.prod, Multiset.map_map]; rfl

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f : M →* P
H : c ≤ ker f
⊢ Con.liftOn 1 ⇑f ⋯ = 1

Tactic:
by rw [← f.map_one]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, ↑a * y = x) ↔ ∃ a, y * x⁻¹ = ↑a⁻¹

Tactic:
simp only [mul_inv_eq_iff_eq_mul, Subgroup.coe_inv, eq_inv_mul_iff_mul_eq]

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

Goal state before:
pp: α : Type u_1
⊢ Subgroup.closure (Set.range of) = ⊤

Tactic:
rw [← range_lift_eq_closure, lift_of_eq_id]

Goal state after:
α : Type u_1
⊢ (MonoidHom.id (FreeGroup α)).range = ⊤
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
F : Fintype ↥s
h : ∀ (x : ι), x ∈ s ↔ (fun x ↦ x ∈ s) x
⊢ ∏ a ∈ s, f a = ∏ a, f ↑a

Tactic:
rw [← prod_coe_sort]

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
F : Fintype ↥s
h : ∀ (x : ι), x ∈ s ↔ (fun x ↦ x ∈ s) x
⊢ ∏ i, f ↑i = ∏ a, f ↑a
Module: Mathlib.GroupTheory.Finiteness

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

Tactic:
refine ⟨S, le_antisymm ?_ ?_⟩

Goal state after:
case mpr.refine_1
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ closure ↑S ≤ P

case mpr.refine_2
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ P ≤ closure ↑S
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ : R
s : ↥⊥
h : x✝¹ * ↑s = x✝ * ↑s
⊢ ↑s * x✝¹ = ↑s * x✝

Tactic:
by
      rcases s with ⟨s, hs⟩
      rw [Submonoid.mem_bot] at hs
      subst hs
      rw [mul_one, mul_one] at h
      subst h
      rfl

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
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
j : κ
hj : j ∈ {i ∈ I | f i = f n}.erase n
⊢ g (f j) = 1

Tactic:
simp only [mem_erase, mem_filter] at hj

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
j : κ
hj : j ≠ n ∧ j ∈ I ∧ f j = f n
⊢ g (f j) = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
G : Type u_3
s : Finset ι
inst✝¹ : CommGroup G
inst✝ : DecidableEq ι
f : ι → G
a : ι
h : a ∈ s
⊢ ∏ x ∈ s.erase a, f x = (∏ x ∈ s, f x) / f a

Tactic:
eq_div_iff_mul_eq',

Goal state after:
ι : Type u_1
G : Type u_3
s : Finset ι
inst✝¹ : CommGroup G
inst✝ : DecidableEq ι
f : ι → G
a : ι
h : a ∈ s
⊢ (∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ f 0 * ∏ i ∈ range n, f (i + 1) / f i = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1)

Tactic:
simp [Finset.prod_range_succ', mul_comm]

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
s₁ s₂ : Finset ι
inst✝¹ : CommGroup G
inst✝ : DecidableEq ι
f : ι → G
h : s₁ ⊆ s₂
⊢ ∏ x ∈ s₂ \ s₁, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x

Tactic:
eq_div_iff_mul_eq',

Goal state after:
ι : Type u_1
G : Type u_3
s₁ s₂ : Finset ι
inst✝¹ : CommGroup G
inst✝ : DecidableEq ι
f : ι → G
h : s₁ ⊆ s₂
⊢ (∏ x ∈ s₂ \ s₁, f x) * ∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
s : Finset ι
m : ℕ
f : ι → ℕ
h₁ : ∀ x ∈ s, f x = m
⊢ ∑ x ∈ s, f x = ∑ _x ∈ s, m

Tactic:
apply sum_congr rfl h₁

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆ ≤ center G

Tactic:
← Subgroup.centralizer_univ,

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ ⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆ ≤ centralizer Set.univ
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 L1 : α
⊢ f (L1 * L2) = f L1 * f L2

Tactic:
exact f.map_mul _ _

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : 0 ≤ a
⊢ 0 ≤ f a

Tactic:
by
  rw [← map_zero f]
  exact OrderHomClass.mono _ ha

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ f a ≤ 0

Tactic:
by
  rw [← map_zero f]
  exact OrderHomClass.mono _ ha

Goal state after:
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₁ s₂ : ↥S
⊢ (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Tactic:
with_unfolding_all rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = oreNum r₁ s₂ * r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Tactic:
with_unfolding_all rfl

Goal state after:
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
inst✝ : One X
⊢ 1 = 1 /ₒ 1

Tactic:
with_unfolding_all rfl

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

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑sc * ↑sa * r₁ = rc * ↑sb * ↑s₂

Tactic:
← hc,

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑sc * ↑sa * r₁ = ↑sc * ra * ↑s₂
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.10
inst✝ : MulAction R X
⊢ 1 /ₒ 1 = 1

Tactic:
with_unfolding_all rfl

Goal state after:
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.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
x y : OreLocalization S R
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (x * y) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ x * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ y

Tactic:
by
    cases x with | _ r₁ s₁
    cases y with | _ r₂ s₂
    rcases oreDivMulChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩; rw [ha']; clear ha'
    rw [liftExpand_of, liftExpand_of, liftExpand_of, Units.inv_mul_eq_iff_eq_mul, map_mul, map_mul,
      Units.val_mul, mul_assoc, ← mul_assoc (fS s₁ : T), ← mul_assoc (fS s₁ : T), Units.mul_inv,
      one_mul, ← hf, ← mul_assoc, ← map_mul _ _ r₁, ha, map_mul, hf s₂, mul_assoc,
      ← mul_assoc (fS s₂ : T), (fS s₂).mul_inv, one_mul]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
x : X
s : ↥S
⊢ r • (x /ₒ s) = oreNum (r • 1) s • x /ₒ oreDenom (r • 1) s

Tactic:
with_unfolding_all rfl

Goal state after:
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✝¹ : Zero X
inst✝ : MulAction R X
⊢ 0 = 0 /ₒ 1

Tactic:
with_unfolding_all rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a : α
⊢ ¬IsSuccPrelimit a ↔ ∃ b, b ⋖ a

Tactic:
simp [IsSuccPrelimit]

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
⊢ IsSuccLimit (toDual a) ↔ IsPredLimit a

Tactic:
by
  simp [isSuccLimit_iff, isPredLimit_iff]

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

Goal state before:
pp: case top
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
⊢ IsSuccPrelimit ⊤ ↔ ⊤ = ⊤ ∨ ∃ y, ⊤ = ↑y ∧ IsSuccPrelimit y

Tactic:
simp [IsSuccPrelimit]

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

Goal state before:
pp: case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
⊢ ∃ x, IsGreatest S x

Tactic:
by_cases hmS : m ∈ S

Goal state after:
case pos
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
hmS : m ∈ S
⊢ ∃ x, IsGreatest S x

case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
hmS : m ∉ S
⊢ ∃ x, IsGreatest S x
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred c ∈ s
⊢ b ≤ pred c

Tactic:
← hn

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred c ∈ s
⊢ pred^[n] (pred c) ≤ pred c
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg.inl
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∉ s
h✝¹ : ⟨x, hx⟩ ≤ ⟨x, hx⟩
y : α
hy : y ∈ s
h✝ : ⟨y, hy⟩ ≤ ⟨x, hx⟩
h : y < x
this : y ≤ pred x
⊢ pred x ∈ s

Tactic:
apply out' hy hx

Goal state after:
case neg.inl
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∉ s
h✝¹ : ⟨x, hx⟩ ≤ ⟨x, hx⟩
y : α
hy : y ∈ s
h✝ : ⟨y, hy⟩ ≤ ⟨x, hx⟩
h : y < x
this : y ≤ pred x
⊢ pred x ∈ Icc y x