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

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i ↦ ⟨Exists.choose ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ↑(u ⟨i, hi⟩) ∈ s ↑⟨j, hj⟩

Tactic:
rw [hij]

Goal state after:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i ↦ ⟨Exists.choose ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ↑(u ⟨j, hj⟩) ∈ s ↑⟨j, hj⟩
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t st : Finset ι
a : α
x✝ : a ∈ Set.range fun x ↦ ⨆ (_ : x ∈ st), f x
i : ι
ha : (fun x ↦ ⨆ (_ : x ∈ st), f x) i = a
⊢ (fun x ↦ ⨆ (_ : x ∈ st), f x) i ≤ st.sup f

Tactic:
by_cases h : i ∈ st

Goal state after:
case pos
ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t st : Finset ι
a : α
x✝ : a ∈ Set.range fun x ↦ ⨆ (_ : x ∈ st), f x
i : ι
ha : (fun x ↦ ⨆ (_ : x ∈ st), f x) i = a
h : i ∈ st
⊢ (fun x ↦ ⨆ (_ : x ∈ st), f x) i ≤ st.sup f

case neg
ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t st : Finset ι
a : α
x✝ : a ∈ Set.range fun x ↦ ⨆ (_ : x ∈ st), f x
i : ι
ha : (fun x ↦ ⨆ (_ : x ∈ st), f x) i = a
h : i ∉ st
⊢ (fun x ↦ ⨆ (_ : x ∈ st), f x) i ≤ st.sup f
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
cases isEmpty_or_nonempty ι <;>
      simp [h, iSup_of_empty', ciSup_const]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
h : Minimal (fun x ↦ P x ∨ Q x) x
⊢ Minimal P x ∨ Minimal Q x

Tactic:
obtain ⟨h | h, hmin⟩ := h

Goal state after:
case inl
α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hmin : ∀ ⦃y : α⦄, (fun x ↦ P x ∨ Q x) y → y ≤ x → x ≤ y
h : P x
⊢ Minimal P x ∨ Minimal Q x

case inr
α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hmin : ∀ ⦃y : α⦄, (fun x ↦ P x ∨ Q x) y → y ≤ x → x ≤ y
h : Q x
⊢ Minimal P x ∨ Minimal Q x
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ b ::ₘ Ico a b = Icc a b

Tactic:
classical
    rw [Ico, ← Finset.insert_val_of_notMem right_notMem_Ico, Finset.Ico_insert_right h]
    rfl

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

Goal state before:
pp: ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℕ
⊢ iInf f = 0

Tactic:
iInf_of_isEmpty,

Goal state after:
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℕ
⊢ sInf ∅ = 0
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Set.Ioc a b ∪ Set.Ioc b c = Set.Ioc a c

Tactic:
Set.Ioc_union_Ioc_eq_Ioc h₁ h₂

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Set.Ioc a c = Set.Ioc a c
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a c ⊆ Ico a b ∪ Ico b c

Tactic:
by
  rw [← coe_subset, coe_union, coe_Ico, coe_Ico, coe_Ico]
  exact Set.Ico_subset_Ico_union_Ico

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_2
inst✝ : CommGroup G
x y : G
⊢ y * x = x * y

Tactic:
exact mul_comm y x

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
x : M
⊢ op x ∈ Set.center Mᵐᵒᵖ ↔ x ∈ Set.center M

Tactic:
by
  simp_rw [Set.mem_center_iff, isMulCentral_iff, MulOpposite.forall, ← op_mul, op_inj]; aesop

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

Goal state before:
pp: α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
⊢ (s.erase a).noncommProd comm' * a = s.noncommProd comm

Tactic:
suffices ∀ b ∈ erase s a, Commute a b by
    rw [← (noncommProd_commute (s.erase a) comm' a this).eq, mul_noncommProd_erase s h comm comm']
  intro b hb
  rcases eq_or_ne a b with rfl | hab
  · rfl
  exact comm h (mem_of_mem_erase hb) hab

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
⊢ s₁.noncommProd f comm = s₂.noncommProd g ⋯

Tactic:
noncommProd,

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
⊢ (Multiset.map f s₁.val).noncommProd ⋯ = (Multiset.map g s₂.val).noncommProd ⋯
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (cons a s ha).noncommProd f comm = f a * s.noncommProd f ⋯

Tactic:
noncommProd,

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (Multiset.map f (cons a s ha).val).noncommProd ⋯ = f a * (Multiset.map f s.val).noncommProd ⋯
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (cons a s ha).noncommProd f comm = s.noncommProd f ⋯ * f a

Tactic:
noncommProd,

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (Multiset.map f (cons a s ha).val).noncommProd ⋯ = (Multiset.map f s.val).noncommProd ⋯ * f a
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ s.noncommProd f comm = m ^ #s

Tactic:
noncommProd,

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ (Multiset.map f s.val).noncommProd ⋯ = m ^ #s
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective ⇑f
y✝ z✝ : N
h₂ : (c.mapOfSurjective (⇑f) h hf) y✝ z✝
a b : M
h1 : c.toSetoid a b
⊢ (c.mapOfSurjective (⇑f) h hf) (f a * y✝) (f b * z✝)

Tactic:
rcases h₂ with ⟨p, q, h2, rfl, rfl⟩

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective ⇑f
a b : M
h1 : c.toSetoid a b
p q : M
h2 : c.toSetoid p q
⊢ (c.mapOfSurjective (⇑f) h hf) (f a * f p) (f b * f q)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case tail
α : Type u
L₁ L₂ b✝ c✝ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ b✝
h₂₃ : Step b✝ c✝
ih : ∃ n, L₁.length = b✝.length + 2 * n
⊢ ∃ n, L₁.length = c✝.length + 2 * n

Tactic:
rcases ih with ⟨n, eq⟩

Goal state after:
case tail
α : Type u
L₁ L₂ b✝ c✝ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ b✝
h₂₃ : Step b✝ c✝
n : ℕ
eq : L₁.length = b✝.length + 2 * n
⊢ ∃ n, L₁.length = c✝.length + 2 * n
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_neg, zpow_natCast, map_inv, map_pow, map.of, sum.map_inv, neg_inj] at ih
        simp [zpow_add, ih, sub_eq_add_neg]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ FG M ↔ ∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ

Tactic:
refine ⟨fun ⟨S, hS⟩ ↦ ⟨S, S.finite_toSet, FreeMonoid.lift Subtype.val, ?_⟩, ?_⟩

Goal state after:
case refine_1
M : Type u_1
inst✝ : Monoid M
x✝ : FG M
S : Finset M
hS : Submonoid.closure ↑S = ⊤
⊢ Function.Surjective ⇑(FreeMonoid.lift Subtype.val)

case refine_2
M : Type u_1
inst✝ : Monoid M
⊢ (∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ) → FG M
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
φ : G →* H
hφ : Surjective ⇑φ
HN : N = φ.ker
⊢ Subgroup.map (mk' N) φ.ker = ⊥

Tactic:
← HN,

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
φ : G →* H
hφ : Surjective ⇑φ
HN : N = φ.ker
⊢ Subgroup.map (mk' N) N = ⊥
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
G' : Subgroup G
inst✝ : G'.Normal
he : Subgroup.map (↑(MulEquiv.refl G)) G' = G'
⊢ congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G')

Tactic:
ext ⟨x⟩
  rfl

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
⊢ Function.Injective of

Tactic:
classical
  exact fun x y hoxy ↦ Classical.by_contradiction fun hxy : x ≠ y ↦
    let f : FreeAbelianGroup α →+ ℤ := lift fun z ↦ if x = z then (1 : ℤ) else 0
    have hfx1 : f (of x) = 1 := (lift_apply_of _ _).trans <| if_pos rfl
    have hfy1 : f (of y) = 1 := hoxy ▸ hfx1
    have hfy0 : f (of y) = 0 := (lift_apply_of _ _).trans <| if_neg hxy
    one_ne_zero <| hfy1.symm.trans hfy0

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x✝ y✝ : FreeAbelianGroup α
h₁ : (lift (g ∘ f)) x✝ = (lift g) ((map f) x✝)
h₂ : (lift (g ∘ f)) y✝ = (lift g) ((map f) y✝)
⊢ (lift (g ∘ f)) (x✝ + y✝) = (lift g) ((map f) (x✝ + y✝))

Tactic:
| add _ _ h₁ h₂ =>

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
L : α
⊢ (lift fun x₂ ↦ of (1 * x₂)) (of L) = of L

Tactic:
rw [lift_apply_of, one_mul]

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
f : M →* G
x : GrothendieckGroup M
⊢ (lift f) x = f ((monoidOf ⊤).sec x).1 / f ↑((monoidOf ⊤).sec x).2

Tactic:
simp [lift, (monoidOf ⊤).lift_apply, div_eq_mul_inv]; congr

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

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ r' * (↑u * ↑s₂) = r' * (v * ↑s₁)

Tactic:
hs₁u

Goal state after:
case refine_2.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ r' * (v * ↑s₁) = r' * (v * ↑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_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := ⋯
u₀ : ↥S := ⋯
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ v • r₂ /ₒ (u * s₁) = v₀ • r₂ /ₒ (u₀ * s₁)

Tactic:
oreDiv_eq_iff

Goal state after:
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₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ ∃ u_1 v_1, u_1 • v₀ • r₂ = v_1 • v • r₂ ∧ ↑u_1 * ↑(u₀ * s₁) = v_1 * ↑(u * 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
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
⊢ ↑s₄' * (r₃' * ↑s₂' * ↑s) ∈ S

Tactic:
← h₃

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
⊢ ↑s₄' * (↑s₃' * ↑s₁' * ↑s) ∈ S
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
hr : r ∈ S
⊢ r /ₒ ⟨r, hr⟩ = 1 /ₒ 1

Tactic:
oreDiv_eq_iff

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
hr : r ∈ S
⊢ ∃ u v, u • 1 = v • r ∧ ↑u * ↑1 = v * ↑⟨r, hr⟩
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
⊢ f.ofMulEquivOfLocalizations (MulEquiv.refl N) = f

Tactic:
by
  ext; rfl

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
Q : Type u_4
inst✝ : CommMonoid Q
k : N ≃* P
j : P ≃* Q
⊢ (f.ofMulEquivOfLocalizations (k.trans j)).toMonoidHom = j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMonoidHom

Tactic:
by
  ext; rfl

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
hg : ∀ (y : ↥S), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
d : P
hc : k (d * x) = k (d * y)
hd : k d = ↑c
⊢ ↑⟨d, ⋯⟩ * x = ↑⟨d, ⋯⟩ * y

Tactic:
exact k.injective hc

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₁ x₂ : M
y₁ y₂ : ↥S
H : f (↑y₂ * x₁) = f (↑y₁ * x₂)
⊢ f x₁ = f x₁ * f ↑y₂ * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y₂)⁻¹

Tactic:
mul_inv_right f.map_units,

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₁ x₂ : M
y₁ y₂ : ↥S
H : f (↑y₂ * x₁) = f (↑y₁ * x₂)
⊢ f x₁ * f.toMonoidHom ↑y₂ = f x₁ * f ↑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
⊢ f.ofMulEquivOfDom ⋯ = f

Tactic:
by
  ext; rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a * b ≠ ⊤

Tactic:
by
  simp [mul_eq_top_iff, *]

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
a b : WithTop α
inst✝ : NoZeroDivisors α
⊢ NoZeroDivisors (WithTop α)

Tactic:
refine ⟨fun h₁ => Decidable.byContradiction fun h₂ => ?_⟩

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
a b : WithTop α
inst✝ : NoZeroDivisors α
a✝ b✝ : WithTop α
h₁ : a✝ * b✝ = 0
h₂ : ¬(a✝ = 0 ∨ b✝ = 0)
⊢ False
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
⊢ ¬IsSuccLimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a

Tactic:
isSuccLimit_iff,

Goal state after:
α : Type u_1
a : α
inst✝ : Preorder α
⊢ ¬(¬IsMin a ∧ IsSuccPrelimit a) ↔ IsMin a ∨ ¬IsSuccPrelimit a
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
x : α
⊢ IsPredPrelimit ↑x ↔ ↑x = ⊤ ∨ ∃ y, ↑x = ↑y ∧ IsPredLimit y

Tactic:
simp [IsPredPrelimit, Order.isPredLimit_iff, WithTop.forall]

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

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a

Tactic:
isSuccLimit_iff,

Goal state after:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ ¬IsMin a ∧ IsSuccPrelimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ico a (succ b) = Icc a b

Tactic:
by
  rw [← Ici_inter_Iio, Iio_succ_of_not_isMax hb, Ici_inter_Iic]

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 α
f : α → β
⊢ (∀ (a : α), ¬IsMin a → f a < f (a - 1)) → StrictAnti f

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

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℕ
⊢ (↑a✝¹ * ↑a✝).toNat = (↑a✝¹).toNat * (↑a✝).toNat

Tactic:
simp only [toNat_natCast]

Goal state after:
case coe.coe
a✝¹ a✝ : ℕ
⊢ (↑a✝¹ * ↑a✝).toNat = a✝¹ * a✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case e_5
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun i ↦ f i) ≍ fun x ↦ f ⟨↑x, ⋯⟩

Tactic:
apply Function.hfunext

Goal state after:
case e_5.hα
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ↥s = ↥{x | x ∈ s}

case e_5.h
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∀ (a : ↥s) (a' : ↥{x | x ∈ s}), a ≍ a' → f a ≍ f ⟨↑a', ⋯⟩
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f (a ::ᵥ v') ⋯).head = f (a ::ᵥ v').head ⋯

Tactic:
pmap_cons,

Goal state after:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (f a ⋯ ::ᵥ pmap f v' ⋯).head = f (a ::ᵥ v').head ⋯
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f (a ::ᵥ v') ⋯).tail = pmap f (a ::ᵥ v').tail ⋯

Tactic:
pmap_cons,

Goal state after:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (f a ⋯ ::ᵥ pmap f v' ⋯).tail = pmap f (a ::ᵥ v').tail ⋯
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n✝ n' m : ℕ
s✝ : Sym α n✝
a b : α
n : ℕ
inst✝ : IsEmpty α
s : Sym α n.succ
⊢ False

Tactic:
obtain ⟨a, -⟩ := exists_mem s

Goal state after:
α : Type u_1
β : Type u_2
n✝ n' m : ℕ
s✝ : Sym α n✝
a✝ b : α
n : ℕ
inst✝ : IsEmpty α
s : Sym α n.succ
a : α
⊢ False
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map some (map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach) = map some s

Tactic:
refine Eq.trans ?_ (.trans (SymOptionSuccEquiv.decode (Sum.inr s)).attach_map_coe ?_) <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : y ≤ x
⊢ y = (sumLexIicIoi x) (toLex (Sum.inl ⟨y, h⟩))

Tactic:
sumLexIicIoi_apply_inl

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x y : α
h : y ≤ x
⊢ y = ↑⟨y, h⟩
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccLimit (sSup s)
⊢ sSup s ∈ s

Tactic:
isSuccLimit_iff,

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬(¬IsMin (sSup s) ∧ IsSuccPrelimit (sSup s))
⊢ sSup s ∈ s
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: a : Cardinal.{u}
⊢ Nonempty (Quotient.out (lift.{v, u} #(Quotient.out a)) ≃ Quotient.out #(Quotient.out a))

Tactic:
← mk_uLift,

Goal state after:
a : Cardinal.{u}
⊢ Nonempty (Quotient.out #(ULift (Quotient.out a)) ≃ Quotient.out #(Quotient.out a))
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: case mk.mk
ι : Type u
α : Type v
f : ι → Type v
⊢ (lift.{u, v} #α ^ sum fun i ↦ #(f i)) = prod fun i ↦ #α ^ #(f i)

Tactic:
← mk_uLift,

Goal state after:
case mk.mk
ι : Type u
α : Type v
f : ι → Type v
⊢ (#(ULift α) ^ sum fun i ↦ #(f i)) = prod fun i ↦ #α ^ #(f i)
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a✝ : α
h : Acc r a✝
a : α
x✝ : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s (f y)
a' : α
hb : s (f a') (f a)
⊢ Acc s (f a')

Tactic:
exact ha _ (f.map_rel_iff.mp hb)

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ ScottContinuous Prod.fst

Tactic:
simp_rw [← scottContinuousOn_univ, ScottContinuousOn.fst]

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ cSup c ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}

Tactic:
refine ⟨(bot_isAdmissible le_map).cSup_mem _ (subset_trans hc (sep_subset _ _)), ?_⟩

Goal state after:
case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ cSup c ≤ y ∨ f y ≤ cSup c