mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A' A B : Subgroup G
hN : A ≤ normalizer ↑(A' ⊓ A)
⊢ A ⊓ B ≤ normalizer ↑(A' ⊓ B ⊓ (A ⊓ B))

Tactic:
inf_inf_inf_comm,

Goal state after:
G : Type u_1
inst✝ : Group G
A' A B : Subgroup G
hN : A ≤ normalizer ↑(A' ⊓ A)
⊢ A ⊓ B ≤ normalizer ↑(A' ⊓ A ⊓ (B ⊓ B))
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : ∀ (i_1 : ι), i_1 ∈ i :: l → f i_1 ≤ g i_1
h₂ : ∃ i_1, i_1 ∈ i :: l ∧ f i_1 < g i_1
⊢ (map f (i :: l)).prod < (map g (i :: l)).prod

Tactic:
simp only [forall_mem_cons, map_cons, prod_cons] at h₁ ⊢

Goal state after:
case cons
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₂ : ∃ i_1, i_1 ∈ i :: l ∧ f i_1 < g i_1
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
⊢ f i * (map f l).prod < g i * (map g l).prod
Module: Mathlib.Data.List.Sublists

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

Tactic:
Array.foldl_toList

Goal state after:
α : Type u
a : α
r₁ r₂ : List (List α)
⊢ Array.foldl (fun r l ↦ r ++ [a :: l]) r₂ { toList := r₁ } =
    (Array.foldl (fun r l ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) (a :: l)
⊢ l'.length = n + 1

Tactic:
rw [sublistsLen_succ_cons, mem_append, mem_map] at h
    rcases h with (h | ⟨l', h, rfl⟩)
    · exact length_of_sublistsLen h
    · exact congr_arg (· + 1) (length_of_sublistsLen h)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
⊢ #({x ∈ powersetCard n t | s ⊆ x}) = (#t - #s).choose (n - #s)

Tactic:
by
  have hinj : Set.InjOn (· ∪ s) ↑((t \ s).powersetCard (n - #s)) := fun a ha b hb hab =>
    (union_sdiff_cancel_right
      (disjoint_of_subset_left (mem_powersetCard.mp ha).1 disjoint_sdiff_self_left)).symm.trans
    ((congrArg (· \ s) hab).trans
      (union_sdiff_cancel_right
        (disjoint_of_subset_left (mem_powersetCard.mp hb).1 disjoint_sdiff_self_left)))
  simp only [filter_powersetCard_subset s t n hst hsn, card_image_of_injOn hinj,
             card_powersetCard, card_sdiff_of_subset hst]

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : Finset α
h : x ⊆ u
⊢ id x ⊆ u

Tactic:
exact h

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

Goal state before:
pp: α : Type u
ι✝ : Sort v
κ✝ : ι✝ → Sort w
inst✝² : Order.Frame α
inst✝¹ : Finite ι✝
f✝ : (a : ι✝) → κ✝ a → α
ι : Type v
κ : ι → Type w
inst✝ : Finite ι
f : (a : ι) → κ a → α
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
induction ι using Finite.induction_empty_option with
  | of_equiv e h => simp [← e.iInf_comp, ← e.piCongrLeft κ |>.iSup_comp, h]
  | h_empty => simp [iInf_of_empty, iSup_const]
  | h_option h =>
    simp only [iInf_option, h, ← (Equiv.piOptionEquivProd (β := κ)).symm.iSup_comp,
      Equiv.piOptionEquivProd_symm_apply, iSup_prod, ← inf_iSup_eq, ← iSup_inf_eq]

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

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

Tactic:
by_cases bdd : BddAbove (range f)

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

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

Goal state before:
pp: α : Type u_2
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i.down

Tactic:
by
  rw [← iSup_eq_iSup_finset, ← Equiv.plift.surjective.iSup_comp]; rfl

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
this : Nonempty ι
⊢ a < b

Tactic:
exact Pi.lt_def.2 ⟨fun j ↦ (eq_or_ne j i).elim (· ▸ hi.1.le) (h j · |>.1), i, hi.1⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ a ⋖ b ↔ ∃ i x, a i ⋖ x ∧ b = Function.update a i x

Tactic:
covBy_iff

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔ ∃ i x, a i ⋖ x ∧ b = Function.update a i x
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
⊢ ∀ ⦃a : (x : ι) × α x⦄, (∃ a_1 ∈ t i, (Embedding.sigmaMk i) a_1 = a) → ¬∃ a_2 ∈ t j, (Embedding.sigmaMk j) a_2 = a

Tactic:
Function.Embedding.sigmaMk_apply

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_1 ∈ t i, ⟨i, a_1⟩ = a) → ¬∃ a_2 ∈ t j, ⟨j, a_2⟩ = a
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ a ⋖ b ↔ ∃ i x, x ⋖ b i ∧ a = Function.update b i x

Tactic:
covBy_iff

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔ ∃ i x, x ⋖ b i ∧ a = Function.update b i x
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
⊢ x ∈ f '' {x | Minimal P x} → x ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}

Tactic:
rintro ⟨x, (hx : Minimal _ x), rfl⟩
    exact (minimal_mem_image_monotone_iff hx.prop hf).2 hx

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

Goal state before:
pp: s : Set ℕ
h : s.Nonempty
⊢ Nat.find h ∈ s

Tactic:
exact Nat.find_spec h

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

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ ∃ n, r ^ n • x ∈ closure (r • s)

Tactic:
induction hx using closure_induction with

Goal state after:
Module: Mathlib.Order.WellFoundedSet

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

Tactic:
exact h

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ [[a, b]] = Icc a b

Tactic:
uIcc,

Goal state after:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc (a ⊓ b) (a ⊔ b) = Icc a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : b ≤ a
⊢ [[a, b]] = Icc b a

Tactic:
uIcc,

Goal state after:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : b ≤ a
⊢ Icc (a ⊓ b) (a ⊔ b) = Icc b a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ [[a, b]] = [[b, a]]

Tactic:
uIcc,

Goal state after:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc (a ⊓ b) (a ⊔ b) = [[b, a]]
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc (a ⊓ b) (a ⊔ b) = [[b, a]]

Tactic:
uIcc,

Goal state after:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc (a ⊓ b) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
⊢ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
have hzy : z ⋖ y :=
    ⟨hz.1.2, fun c hc hcy ↦ hc.not_ge <| hz.2 (⟨(hz.1.1.trans_lt hc).le, hcy⟩) hc.le⟩

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
⊢ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ s • ↑(closure s) = ↑(closure s)

Tactic:
← Set.iUnion_smul_set

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ⋃ a ∈ s, a • ↑(closure s) = ↑(closure s)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
⊢ (Multiset.map f ↑s.toList).prod = (Multiset.map f s.val).prod

Tactic:
Finset.coe_toList

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
⊢ (Multiset.map f s.val).prod = (Multiset.map f s.val).prod
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
ι : Sort u_5
H : ι → Subgroup G
inst✝ : ∀ (i : ι), (H i).Normal
⊢ (⨆ i, H i).Normal

Tactic:
grw [← normalizer_eq_top_iff, eq_top_iff, ← iInf_normalizer_le_normalizer_iSup]

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
ι : Sort u_5
H : ι → Subgroup G
inst✝ : ∀ (i : ι), (H i).Normal
⊢ ⊤ ≤ ⨅ i, normalizer ↑(H i)
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

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

Tactic:
induction hx using closure_induction with

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

Goal state before:
pp: case trans
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → s x y → s y z → s x z

Tactic:
exact fun _ _ => s.trans'

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

Goal state before:
pp: case mul
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → s w x → s y z → s (w * y) (x * z)

Tactic:
exact fun _ _ => s.mul

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

Goal state before:
pp: M : Type u_1
inst✝ : Group M
c : Con M
n : ℕ
w x : M
h : c w x
⊢ c (w ^ Int.negSucc n) (x ^ Int.negSucc n)

Tactic:
simpa only [zpow_negSucc] using c.inv (c.pow _ h)

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

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

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

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 κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : κ → M
⊢ ∏ j ∈ t, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s, f (g i)

Tactic:
calc
    _ = ∏ j ∈ t, ∏ i ∈ s with g i = j, f (g i) :=
        prod_congr rfl fun y _ ↦ prod_congr rfl fun x hx ↦ by rw [(mem_filter.1 hx).2]
    _ = _ := prod_fiberwise_of_maps_to h _

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

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ φ.ker ≤ (mk' N).ker ↔ N = φ.ker

Tactic:
grind [QuotientGroup.ker_mk']

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁴ : Group G
inst✝³ : Group H
N : Subgroup G
nN : N.Normal
I : Type u_5
inst✝² : Group I
M : Subgroup H
O : Subgroup I
inst✝¹ : M.Normal
inst✝ : O.Normal
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : N ≤ Subgroup.comap (g.comp f) O
x : G ⧸ N
⊢ (map M O g hg) ((map N M f hf) x) = (map N O (g.comp f) hgf) x

Tactic:
refine induction_on x fun x => ?_

Goal state after:
G : Type u_1
H : Type u_2
inst✝⁴ : Group G
inst✝³ : Group H
N : Subgroup G
nN : N.Normal
I : Type u_5
inst✝² : Group I
M : Subgroup H
O : Subgroup I
inst✝¹ : M.Normal
inst✝ : O.Normal
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : N ≤ Subgroup.comap (g.comp f) O
x✝ : G ⧸ N
x : G
⊢ (map M O g hg) ((map N M f hf) ↑x) = (map N O (g.comp f) hgf) ↑x
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ ¬z * y ≤ y

Tactic:
· rw [mul_le_iff_le_one_left']
      exact (one_lt_of_ne_one hz₃).not_ge

Goal state after:
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) * f a = ∏ x ∈ s, f x

Tactic:
prod_erase_mul _ _ h

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, f x = ∏ x ∈ s, f x
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ map H.subtype ⁅⊤, ⊤⁆ = ⁅H, H⁆

Tactic:
map_commutator,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅map H.subtype ⊤, map H.subtype ⊤⁆ = ⁅H, H⁆
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : Monotone ⇑f
a : α
⊢ 0 ≤ a → f 0 ≤ f a

Tactic:
apply h

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

Goal state before:
pp: case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : StrictMono ⇑f
a : α
⊢ 0 < a → f 0 < f a

Tactic:
apply h

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
⊢ v * g ↑x.2 = g x.1

Tactic:
rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
      ← MonoidHom.domRestrict_apply, IsUnit.mul_liftRight_inv (g.domRestrict S) hg, mul_one]

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

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ j (l (k.sec ((f.map hy k) z)).1) =
    (j.toMonoidHom.comp l) ↑(k.sec ((f.map hy k) z)).2 * j (l (g (f.sec z).1)) *
      ↑((IsUnit.liftRight ((j.toMonoidHom.comp (l.comp g)).domRestrict S) ⋯) (f.sec z).2)⁻¹

Tactic:
mul_inv_right

Goal state after:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ j (l (k.sec ((f.map hy k) z)).1) * (j.toMonoidHom.comp (l.comp g)) ↑(f.sec z).2 =
    (j.toMonoidHom.comp l) ↑(k.sec ((f.map hy k) z)).2 * j (l (g (f.sec z).1))
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
or : Set.SurjOn ⇑g ↑S ↑T ∨ Injective ⇑k
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
⊢ z = w

Tactic:
have ifkg (a : M) : i (f a) = k (g a) := f.map_eq hy a

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
or : Set.SurjOn ⇑g ↑S ↑T ∨ Injective ⇑k
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
⊢ z = w
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 : M
y : ↥S
z : N
H : z * f ↑y = f x
⊢ z = f x * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y)⁻¹

Tactic:
mul_inv_right

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 : M
y : ↥S
z : N
H : z * f ↑y = f x
⊢ z * f.toMonoidHom ↑y = f x
Module: Mathlib.GroupTheory.OreLocalization.Basic

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

Tactic:
simp [oreDiv_mul_char s.1 r t s 1 1 (by simp)]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
p : Sort u_4
f : M → ↥S → M → ↥S → p
H :
  ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
    (r S) (a, b) (a', b') → (r S) (c, d) (c', d') → f a b c d = f a' b' c' d'
a c : M
b d : ↥S
⊢ (mk a b).liftOn₂ (mk c d) f H = f a b c d

Tactic:
liftOn₂_mk

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
p : Sort u_4
f : M → ↥S → M → ↥S → p
H :
  ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
    (r S) (a, b) (a', b') → (r S) (c, d) (c', d') → f a b c d = f a' b' c' d'
a c : M
b d : ↥S
⊢ f a b c d = f a b c d
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
n : ℕ
hn : n ≠ 0
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
hab : mk a.1 a.2 ^ n = mk b.1 b.2 ^ n
⊢ mk a.1 a.2 = mk b.1 b.2

Tactic:
simp only [mk_pow, mk_eq_mk_iff, r_iff_exists, SubmonoidClass.coe_pow, Subtype.exists,
      exists_prop] at hab ⊢

Goal state after:
case mk.mk
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
n : ℕ
hn : n ≠ 0
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
hab : ∃ a_1 ∈ S, a_1 * (↑b.2 ^ n * a.1 ^ n) = a_1 * (↑a.2 ^ n * b.1 ^ n)
⊢ ∃ a_1 ∈ S, a_1 * (↑b.2 * a.1) = a_1 * (↑a.2 * b.1)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
M : Type u_3
X : Type u_4
inst✝² : Monoid M
S : Submonoid M
inst✝¹ : OreSet S
inst✝ : MulAction M X
r : M
r✝ : X
s✝ : ↥S
⊢ (r /ₒ 1) • (r✝ /ₒ s✝) = oreNum (r • 1) s✝ • r✝ /ₒ oreDenom (r • 1) s✝

Tactic:
oreDiv_smul_oreDiv,

Goal state after:
case c
M : Type u_3
X : Type u_4
inst✝² : Monoid M
S : Submonoid M
inst✝¹ : OreSet S
inst✝ : MulAction M X
r : M
r✝ : X
s✝ : ↥S
⊢ oreNum r s✝ • r✝ /ₒ (oreDenom r s✝ * 1) = oreNum (r • 1) s✝ • r✝ /ₒ oreDenom (r • 1) s✝
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
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
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
r : R
m : OreLocalization S M
x : OreLocalization S X
⊢ (r • m) • x = r • m • x

Tactic:
by
    rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← mul_smul, smul_eq_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a = b ∨ a < b
⊢ ∃ n, pred^[n] b = a

Tactic:
rcases hab with (rfl | hab)

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b : α
ih : ∀ y < a, a ≤ y → ∃ n, pred^[n] y = a
⊢ ∃ n, pred^[n] a = a

case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
⊢ ∃ n, pred^[n] b = a
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
c : α
hc : c ∈ s
hbc : b < c
hca : c ≤ a
⊢ False

Tactic:
obtain rfl := (hb.ge_of_gt hbc).antisymm hca

Goal state after:
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
hc : a ∈ s
hbc : b < a
hca : a ≤ a
⊢ False
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ b ≤ succ a ∧ a ≤ b ↔ b = a ∨ b = succ a

Tactic:
rw [and_comm]
  exact le_and_le_succ_iff

Goal state after: