mathlib-initiative/mathlib-tactics huggingface dataset:
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
j : N →* P
x✝ : N
⊢ (f.lift ⋯) x✝ = j x✝

Tactic:
lift_spec,

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
j : N →* P
x✝ : N
⊢ (j.comp f.toMonoidHom) (f.sec x✝).1 = (j.comp f.toMonoidHom) ↑(f.sec x✝).2 * j 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
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
j : N →* P
hj : ∀ (x : M), j (f x) = g x
x✝ : N
⊢ (f.lift hg) x✝ = j x✝

Tactic:
lift_spec,

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
hg : ∀ (y : ↥S), IsUnit (g ↑y)
j : N →* P
hj : ∀ (x : M), j (f x) = g x
x✝ : N
⊢ g (f.sec x✝).1 = g ↑(f.sec x✝).2 * j x✝
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mp.mpr
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 : Injective ⇑(f.lift hg)
x y : M
h : (f.lift hg) (f x) = g y
⊢ f x = f y

Tactic:
← f.lift_eq hg

Goal state after:
case mp.mpr
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 : Injective ⇑(f.lift hg)
x y : M
h : (f.lift hg) (f x) = (f.lift hg) (f y)
⊢ f x = f y
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
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
⊢ ↑s₄' * r₃' * ↑s₁' * ↑s ∈ S

Tactic:
mul_assoc _ r₃',

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

Goal state before:
pp: case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ ↑s₄' * r₃' * ↑s₁' * ↑s = ↑s₄' * ↑s₃' * ↑s₂' * r₂ * ↑s

Tactic:
mul_assoc _ r₃',

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

Goal state before:
pp: case inl
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
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' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
this : k (g z') = k (g w')
surj : Set.SurjOn ⇑g ↑S ↑T
c : M
hc : c ∈ ↑S
hc' : g c ∈ T
eq : g (c * z') = g (c * w')
⊢ z = w

Tactic:
hg.eq_iff

Goal state after:
case inl
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
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' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
this : k (g z') = k (g w')
surj : Set.SurjOn ⇑g ↑S ↑T
c : M
hc : c ∈ ↑S
hc' : g c ∈ T
eq : c * z' = c * w'
⊢ 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₁ x₂ : M
y : ↥S
⊢ f.mk' (x₁ * x₂) (1 * y) = f.mk' (x₁ * x₂) y

Tactic:
one_mul

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 : ↥S
⊢ f.mk' (x₁ * x₂) y = f.mk' (x₁ * 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
P : Type u_3
inst✝ : CommMonoid P
z : Localization S
x : M × ↥S
⊢ 1 * mk x.1 1 = mk x.1 1

Tactic:
one_mul

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
z : Localization S
x : M × ↥S
⊢ mk x.1 1 = mk x.1 1
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
a : α
⊢ ↑(1 * a) = ↑a

Tactic:
one_mul

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
a : α
⊢ ↑a = ↑a
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
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)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
⊢ f ra * f r₂ = f ra * (1 * f r₂)

Tactic:
one_mul

Goal state after:
case c.c
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)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
⊢ f ra * f r₂ = f ra * f r₂
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
h : IsSuccPrelimit x
⊢ IsSuccPrelimit ↑x

Tactic:
by
  simpa [IsSuccPrelimit, WithTop.forall]

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

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

Tactic:
simpa [ha.succ_eq] using le_of_eq

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b : α
⊢ b ≤ b ∧ b ≤ succ b

pp: case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
⊢ a ≤ succ a ∧ succ a ≤ succ a

Tactic:
· exact ⟨le_rfl, le_succ b⟩

Goal state after:
case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
⊢ a ≤ succ a ∧ succ a ≤ succ a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : IsMax b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b

Tactic:
hb.succ_eq,

Goal state after:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : IsMax b
⊢ a ≤ b ↔ a = b ∨ a ≤ b
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:
rw [← pred_eq_sub_one]
  exact le_pred_of_lt h

Goal state after:
Module: Mathlib.Logic.Small.Defs

Goal state before:
pp: S : Type u
e✝ : Type (max u v) ≃ S
a b : Set ((α : S) × e✝.symm α)
e : ⟨e✝ (Set ((α : S) × e✝.symm α)), cast ⋯ a⟩ = ⟨e✝ (Set ((α : S) × e✝.symm α)), cast ⋯ b⟩
⊢ a = b

Tactic:
injection e with h₁ h₂

Goal state after:
S : Type u
e : Type (max u v) ≃ S
a b : Set ((α : S) × e.symm α)
h₁ : e (Set ((α : S) × e.symm α)) = e (Set ((α : S) × e.symm α))
h₂ : cast ⋯ a = cast ⋯ b
⊢ a = b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∈ s
⊢ ↑(succ a) = succ ↑a

Tactic:
change Subtype.val (dite ..) = _
  split_ifs <;> trivial

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
⊢ (map f v).tail = map f v.tail

Tactic:
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
  rw [h, map_cons, tail_cons, tail_cons]

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ s = replicate n a ↔ ∀ b ∈ s, b = a

Tactic:
by
  rw [Subtype.ext_iff, val_replicate, Multiset.eq_replicate]
  exact and_iff_right s.2

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
x : α
⊢ scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v

Tactic:
apply Vector.eq; simp [scanl]

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

Goal state before:
pp: m : Type u_6 → Type u_7
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ (mOfFn fun i ↦ pure (f i)) = pure (ofFn f)

Tactic:
by
    rw [mOfFn, @mOfFn_pure m _ _ _ n _, ofFn]
    simp

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

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : i < j
⊢ ((↑v).insertIdx j a).eraseIdx ↑⟨i, ⋯⟩ =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j, hj⟩.pred ⋯)) a

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero
        (Nat.pos_iff_ne_zero.1 (lt_of_le_of_lt (Nat.zero_le _) hij)) with ⟨j, rfl⟩

Goal state after:
case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ((↑v).insertIdx j.succ a).eraseIdx ↑⟨i, ⋯⟩ =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j.succ, hj⟩.pred ⋯)) a
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 : ℕ
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
f : α → F β
v : List α
Hv : v.length = n
⊢ F (Vector β v.length) = F (Vector β n)

Tactic:
rw [Hv]

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
⊢ ⨆ a, ↑a = x ↔ IsSuccPrelimit x

Tactic:
rw [← sSup_eq_iSup', sSup_Iio_eq_self_iff_isSuccPrelimit]

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s

Tactic:
by
  obtain ⟨y, hy⟩ := not_forall_not.mp hlim
  obtain ⟨i, his, hi⟩ := lt_sSup_iff.mp hy.lt
  exact eq_of_le_of_not_lt (le_sSup his) (hy.2 hi) ▸ his

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: ι : Type u
a : Cardinal.{max u v}
f : ι → Cardinal.{max u v}
⊢ a ^ sum f = prod fun i ↦ a ^ f i

Tactic:
by
  simpa [← lift_umax] using lift_power_sum a f

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case mp
α : Type u_1
o : Part α
⊢ o ≠ none → ∃ x, o = some x

pp: case mpr
α : Type u_1
o : Part α
⊢ (∃ x, o = some x) → o ≠ none

Tactic:
· rw [Ne, eq_none_iff', not_not]
    exact fun h => ⟨o.get h, eq_some_iff.2 (get_mem h)⟩

Goal state after:
case mpr
α : Type u_1
o : Part α
⊢ (∃ x, o = some x) → o ≠ none
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
H : ∃ m, c ⊆ m ∧ Maximal (fun x ↦ x ∈ {s | c ⊆ s ∧ IsChain r s}) m
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M

Tactic:
obtain ⟨M, hcM, hM⟩ := H
    exact ⟨M, ⟨hM.prop.2, fun d hd hMd ↦ hM.eq_of_subset ⟨hcM.trans hMd, hd⟩ hMd⟩, hcM⟩

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ {y | IsExtremePt x f y} ⊆ bot x f

pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsAdmissible x f {y | IsExtremePt x f y}

Tactic:
· exact fun _ h ↦ h.mem_bot

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsAdmissible x f {y | IsExtremePt x f y}
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case refine_2
α✝ β✝ : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h : #β < (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding #α
e : β ↪ α
⊢ β ≃ ↑(Set.range ⇑e)

Tactic:
apply (e.codRestrict _ mem_range_self).equivOfSurjective

Goal state after:
case refine_2
α✝ β✝ : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h : #β < (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding #α
e : β ↪ α
⊢ Surjective ⇑(Embedding.codRestrict (Set.range ⇑e) e ⋯)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ (f (ωSup c)) (g (ωSup c)) = ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })

Tactic:
rw [hf.map_ωSup, hg.map_ωSup]
    simp only [ωSup_def, ωSup_apply]
    apply le_antisymm
    · apply ωSup_le
      intro i
      dsimp
      rw [(f (c i)).continuous]
      apply ωSup_le
      intro j
      apply le_ωSup_of_le (i ⊔ j)
      apply apply_mono
      · apply hf.monotone (c.monotone le_sup_left)
      · apply hg.monotone (c.monotone le_sup_right)
    · simp only [ωSup_le_iff]
      intro i
      apply le_ωSup_of_le i
      apply (f (c i)).monotone
      apply le_ωSup_of_le i
      rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
⊢ toNat a = n ↔ a = ↑n

Tactic:
by
  nth_rw 2 [← Cardinal.cast_toNat_of_lt_aleph0 lt]
  exact Nat.cast_inj.symm

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹ : AddGroup M
inst✝ : DistribSMul R M
r : R
h : ∀ (m : M), r • m = 0 → m = 0
m₁ m₂ : M
eq : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ r • (m₁ - m₂) = 0

Tactic:
smul_sub,

Goal state after:
R : Type u_1
M : Type u_3
inst✝¹ : AddGroup M
inst✝ : DistribSMul R M
r : R
h : ∀ (m : M), r • m = 0 → m = 0
m₁ m₂ : M
eq : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ r • m₁ - r • m₂ = 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: S : Set ℕ
h' : #↑S < #ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
this : S.Finite
⊢ ∃ n, lift.{u_1, 0} #↑S = ↑n

Tactic:
lift S to Finset ℕ using this

Goal state after:
S : Finset ℕ
h' : #↑↑S < #ℕ
h : lift.{u_1, 0} #↑↑S < ℵ₀
⊢ ∃ n, lift.{u_1, 0} #↑↑S = ↑n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
S T : Set α
H : Disjoint S T
⊢ #↑(S ∪ T) = #↑S + #↑T

Tactic:
classical
  exact Quot.sound ⟨Equiv.Set.union H⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
A B : Set α
hfin : B.Finite
hlt : A ⊂ B
⊢ #↑A < #↑B

Tactic:
have : Fintype A := (hfin.subset hlt.subset).fintype
  have : Fintype B := hfin.fintype
  simpa using Finset.card_lt_card <| Set.toFinset_ssubset_toFinset.mpr hlt

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u_1
h : 3 ≤ #α
x y : α
this✝¹ : ↑3 ≤ #α
this✝ : ↑2 < #α
this : ∃ z, z ∉ [x, y]
⊢ ∃ z, z ≠ x ∧ z ≠ y

Tactic:
simpa [not_or] using this

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b c : Cardinal.{u}
⊢ a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c

Tactic:
powerlt,

Goal state after:
a b c : Cardinal.{u}
⊢ ⨆ c, a ^ ↑c ≤ c ↔ ∀ x < b, a ^ x ≤ c
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ r • (1 * x) = r • x

Tactic:
one_mul

Goal state after:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ r • x = r • x
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
x✝ : MulAction (M × N) α
instM : MulAction M α := compHom α (MonoidHom.inl M N)
instN : MulAction N α := compHom α (MonoidHom.inr M N)
m : M
n : N
a : α
⊢ (m, 1 * n) • a = (1 * m, n) • a

Tactic:
one_mul

Goal state after:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
m : M
n : N
a : α
⊢ (m, 1 * n) • a = SMul.smul (m, n) a

Tactic:
one_mul

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
m : M
n : N
a : α
⊢ (m, n) • a = SMul.smul (m, n) a
Module: Mathlib.Algebra.GroupWithZero.Action.Basic

Goal state before:
pp: G : Type u_1
R : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Monoid R
inst✝³ : AddGroup R
inst✝² : DistribMulAction G R
inst✝¹ : IsScalarTower G R R
inst✝ : SMulCommClass G R R
r : G
a : R
⊢ IsUnit (r • 1 - a) ↔ IsUnit (r • (1 - r⁻¹ • a))

Tactic:
smul_sub,

Goal state after:
G : Type u_1
R : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Monoid R
inst✝³ : AddGroup R
inst✝² : DistribMulAction G R
inst✝¹ : IsScalarTower G R R
inst✝ : SMulCommClass G R R
r : G
a : R
⊢ IsUnit (r • 1 - a) ↔ IsUnit (r • 1 - r • r⁻¹ • a)
Module: Mathlib.Algebra.GroupWithZero.Action.Basic

Goal state before:
pp: G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), x • 0 = 0
hb : ¬b = 0
⊢ h⁻¹ • h • b ≠ h⁻¹ • 0

Tactic:
simpa [this]

Goal state after:
Module: Mathlib.Algebra.Ring.Opposite

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ op 0 = 0

Tactic:
op_zero

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 0 = 0
Module: Mathlib.Algebra.Ring.Opposite

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoidWithOne R
⊢ op 0 = 0

Tactic:
op_zero

Goal state after:
R : Type u_1
inst✝ : AddCommMonoidWithOne R
⊢ 0 = 0
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: case mk.mk
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ : R →+* S
toAddHom✝¹ : M →ₙ+ M₃
map_smul'✝¹ : ∀ (m : R) (x : M), toAddHom✝¹.toFun (m • x) = σ m • toAddHom✝¹.toFun x
toAddHom✝ : M →ₙ+ M₃
map_smul'✝ : ∀ (m : R) (x : M), toAddHom✝.toFun (m • x) = σ m • toAddHom✝.toFun x
h :
  (fun f ↦ f.toFun) { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } =
    (fun f ↦ f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }
⊢ toAddHom✝¹ = toAddHom✝

Tactic:
apply DFunLike.coe_injective

Goal state after:
case mk.mk
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ : R →+* S
toAddHom✝¹ : M →ₙ+ M₃
map_smul'✝¹ : ∀ (m : R) (x : M), toAddHom✝¹.toFun (m • x) = σ m • toAddHom✝¹.toFun x
toAddHom✝ : M →ₙ+ M₃
map_smul'✝ : ∀ (m : R) (x : M), toAddHom✝.toFun (m • x) = σ m • toAddHom✝.toFun x
h :
  (fun f ↦ f.toFun) { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } =
    (fun f ↦ f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }
⊢ ⇑toAddHom✝¹ = ⇑toAddHom✝
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
x✝ : DistribMulAction (M × N) α
m : M
n : N
a : α
⊢ (m, 1 * n) • a = SMul.smul (m, n) a

Tactic:
one_mul

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
x✝ : DistribMulAction (M × N) α
m : M
n : N
a : α
⊢ (m, n) • a = SMul.smul (m, n) a
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
x m : ↥p
⊢ x ∈ Subtype.val ⁻¹' MulAction.orbit R ↑m ↔ ↑x ∈ MulAction.orbit R ↑m

Tactic:
Set.mem_preimage

Goal state after:
R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
x m : ↥p
⊢ ↑x ∈ MulAction.orbit R ↑m ↔ ↑x ∈ MulAction.orbit R ↑m
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ MulAction.stabilizerSubmonoid R m = MulAction.stabilizerSubmonoid R ↑m

Tactic:
ext
  simp only [MulAction.mem_stabilizerSubmonoid_iff, ← SubMulAction.val_smul, SetLike.coe_eq_coe]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
⊢ map f p < map f q ↔ p < q

Tactic:
rw [lt_iff_le_and_ne, lt_iff_le_and_ne, map_le_map_iff_of_injective hf,
    (map_injective_of_injective hf).ne_iff]

Goal state after:
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : ↑n * (x✝¹ * x✝) = ↑n * x✝¹ * x✝
⊢ ↑n * x✝¹ * x✝ + x✝¹ * x✝ = ↑n * x✝¹ * x✝ + 1 * x✝¹ * x✝

Tactic:
one_mul

Goal state after:
case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : ↑n * (x✝¹ * x✝) = ↑n * x✝¹ * x✝
⊢ ↑n * x✝¹ * x✝ + x✝¹ * x✝ = ↑n * x✝¹ * x✝ + x✝¹ * x✝
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: case refine_1
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
i : ι
x₂ : M
hx₂ : x₂ ∈ S i
⊢ ∃ (hx'' : x₂ ∈ ⨆ i, S i), C x₂ hx''

Tactic:
exact ⟨_, mem _ _ hx₂⟩

Goal state after: