mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
⊢ (ConjClasses.mk g).carrier.Subsingleton

Tactic:
intro x

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
x : G
⊢ x ∈ (ConjClasses.mk g).carrier → ∀ ⦃y : G⦄, y ∈ (ConjClasses.mk g).carrier → x = y
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
⊢ z₁ * z₂ ∈ center M

Tactic:
simp only [commute_iff_eq, mem_center_iff, isMulCentral_iff] at *

Goal state after:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : (∀ (a : M), z₁ * a = a * z₁) ∧ (∀ (b c : M), z₁ * (b * c) = z₁ * b * c) ∧ ∀ (a b : M), a * b * z₁ = a * (b * z₁)
hz₂ : (∀ (a : M), z₂ * a = a * z₂) ∧ (∀ (b c : M), z₂ * (b * c) = z₂ * b * c) ∧ ∀ (a b : M), a * b * z₂ = a * (b * z₂)
⊢ (∀ (a : M), z₁ * z₂ * a = a * (z₁ * z₂)) ∧
    (∀ (b c : M), z₁ * z₂ * (b * c) = z₁ * z₂ * b * c) ∧ ∀ (a b : M), a * b * (z₁ * z₂) = a * (b * (z₁ * z₂))
Module: Mathlib.Algebra.Group.Support

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Monoid M
f : α → M
n : ℕ
⊢ (mulSupport fun x ↦ f x ^ n) ⊆ mulSupport f

Tactic:
by
  induction n with
  | zero => simp [pow_zero]
  | succ n hfn =>
    simpa only [pow_succ'] using (mulSupport_mul f _).trans (union_subset Subset.rfl hfn)

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

Goal state before:
pp: case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
⊢ {x | x ∈ ↑tl}.Pairwise Commute

Tactic:
intro x

Goal state after:
case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
x : α
⊢ x ∈ {x | x ∈ ↑tl} → ∀ ⦃y : α⦄, y ∈ {x | x ∈ ↑tl} → x ≠ y → Commute x y
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute

Tactic:
intro x

Goal state after:
case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x : α
⊢ x ∈ {x | x ∈ a ::ₘ ⟦tl⟧} → ∀ ⦃y : α⦄, y ∈ {x | x ∈ a ::ₘ ⟦tl⟧} → x ≠ y → Commute x y
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
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

Tactic:
refine ⟨A.mul_mem hyA (h hz), ?_⟩

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
⊢ ∃ x ∈ ↑B, ∃ y_1 ∈ ↑C, x * y_1 = y * z
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
⊢ ∀ x ∈ l, ∀ y ∈ l, x * y = y * x

Tactic:
intro x

Goal state after:
case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
x : α
⊢ x ∈ l → ∀ y ∈ l, x * y = y * x
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (f x) (g y)

Tactic:
← h₂ _ hy

Goal state after:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (f x) (f y)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_6
inst✝ : DecidableEq α
s : Finset ι
a : α
f : ι → Multiset α
⊢ count a (∑ x ∈ s, f x) = ∑ x ∈ s, count a (f x)

Tactic:
dsimp only [Finset.sum]
  rw [count_sum]

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

Goal state before:
pp: M : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
S : Multiset M
⊢ map id S.toFinset.val ≤ S

Tactic:
simp [Multiset.dedup_le S]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
⊢ (↑s).Pairwise fun x y ↦ Commute ((f * g) x) ((f * g) y)

Tactic:
intro x

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
⊢ x ∈ ↑s → ∀ ⦃y : α⦄, y ∈ ↑s → x ≠ y → (fun x y ↦ Commute ((f * g) x) ((f * g) y)) x y
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
⊢ (↑s).Pairwise fun x y ↦ Commute ((f * g) x) ((f * g) y)

Tactic:
intro x hx y hy h

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute ((f * g) x) ((f * g) y)
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c d x y : Con M
h : (fun c ↦ ⇑c.toSetoid) x = (fun c ↦ ⇑c.toSetoid) y
⊢ x = y

Tactic:
rcases x with ⟨⟨x, _⟩, _⟩

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c d y : Con M
x : M → M → Prop
iseqv✝ : Equivalence x
mul'✝ :
  ∀ {w x_1 y z : M},
    { r := x, iseqv := iseqv✝ } w x_1 → { r := x, iseqv := iseqv✝ } y z → { r := x, iseqv := iseqv✝ } (w * y) (x_1 * z)
h : (fun c ↦ ⇑c.toSetoid) { r := x, iseqv := iseqv✝, mul' := mul'✝ } = (fun c ↦ ⇑c.toSetoid) y
⊢ { r := x, iseqv := iseqv✝, mul' := mul'✝ } = y
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
c : Con M
p : c.Quotientˣ → Prop
u : c.Quotientˣ
H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p { val := ↑x, inv := ↑y, val_inv := ⋯, inv_val := ⋯ }
⊢ p u

Tactic:
by
  rcases u with ⟨⟨x⟩, ⟨y⟩, h₁, h₂⟩
  exact H x y (c.eq.1 h₁) (c.eq.1 h₂)

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
⊢ ∏ x ∈ s.attach, f ↑x = ∏ x ∈ s, f x

Tactic:
← prod_image Subtype.coe_injective.injOn,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
⊢ ∏ x ∈ image (fun a ↦ ↑a) s.attach, f x = ∏ x ∈ s, f x
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
i : ℕ
ih : (fun x ↦ ((map fun x ↦ 1) x).sum) ((fun x ↦ of () ^ x) ↑i) = ↑i
⊢ (fun x ↦ ((map fun x ↦ 1) x).sum) ((fun x ↦ of () ^ x) (↑i + 1)) = ↑i + 1

Tactic:
simp only [zpow_natCast, map_pow, map.of] at ih

Goal state after:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
i : ℕ
ih : (of 1 ^ i).sum = ↑i
⊢ (fun x ↦ ((map fun x ↦ 1) x).sum) ((fun x ↦ of () ^ x) (↑i + 1)) = ↑i + 1
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
⊢ leftRel N = ⊤ ↔ N = ⊤

Tactic:
simpa [leftRel, MulAction.orbitRel, funext_iff, MulAction.mem_orbit_iff,
    MulAction.subgroup_smul_def, ← eq_inv_mul_iff_mul_eq]
    using ⟨fun h ↦ by ext; simpa using h _ 1, fun h ↦ by simp [h]⟩

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M✝ : Type u_4
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : Monoid M✝
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst✝ : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ N ≤ ((mk' M).comp f).ker

Tactic:
intro x

Goal state after:
G : Type u_1
H : Type u_2
I : Type u_3
M✝ : Type u_4
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : Monoid M✝
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst✝ : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
⊢ x ∈ N → x ∈ ((mk' M).comp f).ker
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
⊢ ∀ x ∈ s, f x = b

Tactic:
intro x

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
⊢ x ∈ s → f x = b
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
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
⊢ ∀ x ∈ s, f x = 1

Tactic:
intro x

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
⊢ x ∈ s → f x = 1
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 ι
inst✝¹ : PartialOrder ι
inst✝ : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I).PairwiseDisjoint f
i j : κ
hdisj : _root_.Disjoint (f i) (f i)
hfij : f i = f j
⊢ g (f i) = 1

Tactic:
disjoint_self

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : DecidableEq ι
inst✝¹ : PartialOrder ι
inst✝ : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I).PairwiseDisjoint f
i j : κ
hdisj : f i = ⊥
hfij : f i = f j
⊢ g (f i) = 1
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
⊢ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ∀ h ∈ ↑H₃, ⁅h, ⁅g₁, g₂⁆⁆ = 1

Tactic:
intro x

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
⊢ x ∈ H₁ → ∀ g₂ ∈ H₂, ∀ h ∈ ↑H₃, ⁅h, ⁅x, g₂⁆⁆ = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ ∀ x ∈ s.toFinset, k • (count x s / k) • {x} = count x s • {x}

Tactic:
intro x

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
x : ι
⊢ x ∈ s.toFinset → k • (count x s / k) • {x} = count x s • {x}
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
f : S.LocalizationMap N
T : Submonoid M
hST : S ≤ T
Q : Type u_4
inst✝¹ : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝ : CommMonoid A
l : M →* A
hl : ∀ (w : ↥T), IsUnit (l ↑w)
x : M
⊢ (((k.lift hl).comp (f.lift ⋯)).comp f.toMonoidHom) x = l x

Tactic:
MonoidHom.comp_assoc,

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
f : S.LocalizationMap N
T : Submonoid M
hST : S ≤ T
Q : Type u_4
inst✝¹ : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝ : CommMonoid A
l : M →* A
hl : ∀ (w : ↥T), IsUnit (l ↑w)
x : M
⊢ ((k.lift hl).comp ((f.lift ⋯).comp f.toMonoidHom)) x = l x
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
w z : N
⊢ z = w * ↑((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹ ↔ z * f ↑y = w

Tactic:
rw [eq_comm, mul_inv_left h, mul_comm, eq_comm]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ f.mk' x y * f ↑y = f x

Tactic:
mk'_spec

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
⊢ f x = f x
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.mk' x y
⊢ f.mk' x y * f ↑y = f x

Tactic:
mk'_spec

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.mk' x y
⊢ f x = f x
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
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f) (mk x y) = f.mk' x y

Tactic:
rw [mk_eq_monoidOf_mk'_apply]

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
⊢ (mulEquivOfQuotient f) ((monoidOf S).mk' x y) = f.mk' x y
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
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f).symm (f.mk' x y) = mk x y

Tactic:
rw [mk_eq_monoidOf_mk'_apply]

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
⊢ (mulEquivOfQuotient f).symm (f.mk' x y) = (monoidOf S).mk' x y
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ f x * f.mk' 1 y = f.mk' x y

Tactic:
by
  rw [mul_mk'_eq_mk'_of_mul, mul_one]

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

Goal state before:
pp: case refine_2
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
m : M
⊢ ∃ a, f a = m

Tactic:
· have ⟨x, eq⟩ := h.surj m
      use x.1 / x.2
      rw [div_eq_mul_inv, map_mul, ← eq, mul_assoc, ← map_mul, mul_inv_cancel, h.map_one, mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
⊢ b ≤ succ a

Tactic:
obtain hab | ⟨-, hba⟩ := h.covBy_or_le_and_le
  · by_contra hba
    exact h.2 (lt_succ_of_not_isMax hab.lt.not_isMax) <| hab.lt.succ_le.lt_of_not_ge hba
  · exact hba.trans (le_succ _)

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

Goal state before:
pp: 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 = succ m ∨ x ≤ m
⊢ ∀ x ∈ S, x ≤ m

Tactic:
intro x

Goal state after:
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 = succ m ∨ x ≤ m
x : X
⊢ x ∈ S → x ≤ m
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
h : x < y
⊢ x ≤ y - 1

Tactic:
by
  rw [← pred_eq_sub_one]
  exact le_pred_of_lt h

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) ≤ f a) → MonotoneOn f s

Tactic:
by
  simpa [Order.pred_eq_sub_one] using monotoneOn_of_pred_le hs (f := f)

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.toList.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))

Tactic:
simp_rw [toList_reverse]

Goal state after:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.toList.reverse.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))
Module: Mathlib.Data.Vector.Basic

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

pp: case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n : ℕ
v : Vector α (n + 1)
i : Fin (n + 1)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
· exact i.elim0

Goal state after:
case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n : ℕ
v : Vector α (n + 1)
i : Fin (n + 1)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
n : ℕ
v : Vector α n
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
⊢ C v

Tactic:
by
  induction n with
  | zero =>
    rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
    exact nil
  | succ n ih =>
    rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
    cases v_property
    exact cons (ih ⟨v, (add_left_inj 1).mp v_property⟩)

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

Goal state before:
pp: α : Type u_1
n : ℕ
m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ↑m₁.snd = ↑m₂.snd
⊢ n - (n - ↑m₁.fst) = ↑m₂.fst

Tactic:
← m₁.2.2,

Goal state after:
α : Type u_1
n : ℕ
m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ↑m₁.snd = ↑m₂.snd
⊢ n - (↑m₁.snd).card = ↑m₂.fst
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s t : Set α
⊢ (s ∪ t).Countable ↔ s.Countable ∧ t.Countable

Tactic:
by
  simp [union_eq_iUnion, and_comm]

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

Goal state before:
pp: n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
x : Vector α n
⊢ (fun {α} ↦ η.app α) (Vector.traverse f x) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) x

Tactic:
by
  induction x with
  | nil => simp! [functor_norm, cast, η.preserves_pure]
  | cons ih =>
    rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]
    rfl

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

Goal state before:
pp: α✝¹ : Type u_1
α✝ : Type u_2
β✝ : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
⊢ ∀ {a b : Lex (Lex (α × β) × γ)},
    (ofLex.trans
            ((ofLex.prodCongr (Equiv.refl γ)).trans
              ((Equiv.prodAssoc α β γ).trans (((Equiv.refl α).prodCongr toLex).trans toLex))))
          a ≤
        (ofLex.trans
            ((ofLex.prodCongr (Equiv.refl γ)).trans
              ((Equiv.prodAssoc α β γ).trans (((Equiv.refl α).prodCongr toLex).trans toLex))))
          b ↔
      a ≤ b

Tactic:
by
    simp only [Prod.Lex.le_iff, Prod.Lex.lt_iff, Equiv.trans_apply, Equiv.prodCongr_apply,
      Equiv.prodAssoc_apply]
    grind [EmbeddingLike.apply_eq_iff_eq, ofLex_toLex]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
⊢ ∀ (x : β), (∀ (y : β), s y x → ∃ a, f a = y) → ∃ a, f a = x

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
⊢ (∀ (y : β), s y x → ∃ a, f a = y) → ∃ a, f a = x
Module: Mathlib.Order.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hg : Monotone g
x y : α
h : x ≤ y
a : γ
⊢ ∀ (x_1 : β), x_1 ∈ f x → a ∈ g x x_1 → ∃ a_3, a_3 ∈ f y ∧ a ∈ g y a_3

Tactic:
exact fun b hb ha ↦ ⟨b, hf h _ hb, hg h _ _ ha⟩

Goal state after:
Module: Mathlib.Order.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Antitone f
hg : Antitone g
x y : α
h : x ≤ y
a : γ
⊢ ∀ (x_1 : β), x_1 ∈ f y → a ∈ g y x_1 → ∃ a_3, a_3 ∈ f x ∧ a ∈ g x a_3

Tactic:
exact fun b hb ha ↦ ⟨b, hf h _ hb, hg h _ _ ha⟩

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case right.left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ((fun x ↦ (f x, g x)) a).1 ≤ (p₁, p₂).1

Tactic:
rw [isLUB_le_iff (hf hd₁ hd₂ hd₃ hda), upperBounds]
      simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_ofPred_eq]
      intro _ hb
      exact (hp _ hb).1

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1.inr
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Tactic:
rcases ih c (fun z hz => (hcs hz).1) hc y hy with ⟨z, hzs, hz⟩
      exact ⟨z, ⟨hzs, (hcs hy).2.trans <| hz _ hy⟩, hz⟩

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
⊢ c i ≤ Part.ωSup c

Tactic:
intro x

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
⊢ x ∈ c i → x ∈ Part.ωSup c
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
⊢ f y ≤ cSup c

Tactic:
have hc' := (bot_isAdmissible le_map).cSup_mem _ (subset_trans hc fun _ h ↦ h.mem_bot)

Goal state after:
case cSup_mem.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
hc' : cSup c ∈ bot x f
⊢ f y ≤ cSup c
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
⊢ ∀ (c_1 : Part γ), ωSup (c.map (f.partBind g)) ≤ c_1 ↔ ωSup (c.map f) >>= ωSup (c.map g) ≤ c_1

Tactic:
intro x

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ ωSup (c.map (f.partBind g)) ≤ x ↔ ωSup (c.map f) >>= ωSup (c.map g) ≤ x