mathlib-initiative/mathlib-tactics huggingface dataset:
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
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : ↑u * ↑s₂ = v * ↑s₁
⊢ v * ↑s₁ ∈ S

Tactic:
rw [← hs₂, ← S.coe_mul]

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : ↑u * ↑s₂ = v * ↑s₁
⊢ ↑(u * s₂) ∈ S
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * ↑y.2 = v * ↑x.2
⊢ v * x.1 * ↑x.2 = u * (↑x.2 * y.1)

Tactic:
← e₁,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * ↑y.2 = v * ↑x.2
⊢ u * y.1 * ↑x.2 = u * (↑x.2 * y.1)
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
P : Type u_4
inst✝ : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : n * f ↑s = f m
h : ∀ (a : M), j (f a) = k (f a)
⊢ j (f m) = k (f m)

Tactic:
h m

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
P : Type u_4
inst✝ : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : n * f ↑s = f m
h : ∀ (a : M), j (f a) = k (f a)
⊢ k (f m) = k (f m)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : α
h₀ : 0 < ↑a
c✝ : WithTop α
b c : α
hbc : ↑b < ↑c
⊢ (fun x ↦ ↑a * x) ↑b < (fun x ↦ ↑a * x) ↑c

Tactic:
simp only [coe_pos, coe_lt_coe, ← coe_mul, gt_iff_lt] at *

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : α
c✝ : WithTop α
b c : α
h₀ : 0 < a
hbc : b < c
⊢ a * b < a * c
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : α
h₀ : 0 < ↑a
c✝ : WithTop α
b c : α
hbc : ↑b < ↑c
⊢ (fun x ↦ x * ↑a) ↑b < (fun x ↦ x * ↑a) ↑c

Tactic:
simp only [coe_pos, coe_lt_coe, ← coe_mul, gt_iff_lt] at *

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : α
c✝ : WithTop α
b c : α
h₀ : 0 < a
hbc : b < c
⊢ b * a < c * a
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r : R
⊢ (universalMulHom f fS hf) (numeratorHom r) = f r

Tactic:
by
  simp [numeratorHom_apply, universalMulHom_apply]

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

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ φ (r /ₒ s) = (universalMulHom f fS hf) (r /ₒ s)

Tactic:
universalMulHom_apply,

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ φ (r /ₒ s) = ↑(fS s)⁻¹ * f r
Module: Mathlib.Algebra.Order.Ring.WithTop

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

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Goal state after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
b c : WithTop α
⊢ 0 * b * c = 0 * (b * c)

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
⊢ a * b * c = a * (b * c)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
⊢ Contravariant { x // 0 ≤ x } (WithBot α) (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 < x2

Tactic:
intro ⟨x, x0⟩ a b h
    simp only at h
    rcases eq_or_ne x 0 with rfl | x0'
    · simp at h
    lift x to α
    · rintro rfl
      exact (WithBot.bot_lt_coe (0 : α)).not_ge x0
    cases b
    · rw [mul_bot x0'] at h
      exact absurd h bot_le.not_gt
    cases a
    · exact WithBot.bot_lt_coe _
    simp only [← coe_mul, coe_lt_coe] at *
    norm_cast at x0
    exact lt_of_mul_lt_mul_left h x0

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
⊢ IsMin a ∨ a ∈ range succ ∨ IsSuccLimit a

Tactic:
rw [isSuccLimit_iff]

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
⊢ IsMin a ∨ a ∈ range succ ∨ ¬IsMin a ∧ IsSuccPrelimit a
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccPrelimit b
⊢ prelimitRecOn b succ isSuccPrelimit = isSuccPrelimit b hb fun x x_1 ↦ prelimitRecOn x succ isSuccPrelimit

Tactic:
by
  rw [prelimitRecOn, WellFounded.fix_eq, dif_pos hb]; rfl

Goal state after:
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: m n a b : ℕ
h : a ≤ b
⊢ a + (b - a) = b

Tactic:
add_tsub_cancel_of_le h

Goal state after:
m n a b : ℕ
h : a ≤ b
⊢ b = b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
n : ℕ
IH : ∀ {a : Y}, succ^[n] a = f (succ^[n] (EquivLike.inv f a))
a : Y
⊢ succ^[n + 1] a = f (succ^[n + 1] (EquivLike.inv f a))

Tactic:
| succ n IH =>

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

Goal state before:
pp: case succ
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
n : ℕ
IH : ∀ {b : Y}, pred^[n] b = f (pred^[n] (EquivLike.inv f b))
b : Y
⊢ pred^[n + 1] b = f (pred^[n + 1] (EquivLike.inv f b))

Tactic:
| succ n IH =>

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
IH : succ^[n] x = x + ↑n
⊢ succ^[n + 1] x = x + ↑(n + 1)

Tactic:
| succ n IH =>

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - ↑n
⊢ pred^[n + 1] x = x - ↑(n + 1)

Tactic:
| succ n IH =>

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha' : ¬succ a✝ = a✝
ha : ↑(succ a✝) ≤ ↑a✝
⊢ IsMax ↑a✝

Tactic:
coe_le_coe,

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha' : ¬succ a✝ = a✝
ha : succ a✝ ≤ a✝
⊢ IsMax ↑a✝
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: m n : ℕ∞
hm : m ≠ ⊤
hn : n ≠ ⊤
⊢ (m + n).toNat = m.toNat + n.toNat

Tactic:
by
  lift m to ℕ using hm
  lift n to ℕ using hn
  rfl

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

Goal state before:
pp: n : WithBot ℕ∞
m : ℕ
⊢ n < ↑m + 1 ↔ n ≤ ↑m

Tactic:
← WithBot.coe_one,

Goal state after:
n : WithBot ℕ∞
m : ℕ
⊢ n < ↑m + ↑1 ↔ n ≤ ↑m
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ
m : WithBot ℕ∞
⊢ ↑n + 1 ≤ m ↔ ↑n < m

Tactic:
← WithBot.coe_one,

Goal state after:
n : ℕ
m : WithBot ℕ∞
⊢ ↑n + ↑1 ≤ m ↔ ↑n < m
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑n < a✝ ↔ ↑n < ↑a✝

Tactic:
← WithBot.coe_lt_coe,

Goal state after:
case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑↑n < ↑a✝ ↔ ↑n < ↑a✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : ι → M
h : a ∈ s
⊢ (∏ x ∈ s, if x = a then b x else 1) = b a

Tactic:
simp only [prod_ite_eq', if_pos h]

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝³ : Applicative F
G : Type u → Type w
inst✝² : Applicative G
η : ApplicativeTransformation F G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
x : α → β
⊢ (fun {α} ↦ η.app α) ∘ Functor.map x = Functor.map x ∘ fun {α} ↦ η.app α

Tactic:
by
  ext y
  exact preserves_map η x y

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
h : v.head = a ∧ v.tail = v'
⊢ v.head ::ᵥ v.tail = a ::ᵥ v'

Tactic:
h.1,

Goal state after:
α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
h : v.head = a ∧ v.tail = v'
⊢ a ::ᵥ v.tail = a ::ᵥ v'
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ insertIdx b j.succ (insertIdx a i ⟨l, hl⟩) = insertIdx a i.castSucc (insertIdx b j ⟨l, hl⟩)

Tactic:
refine Subtype.ext ?_

Goal state after:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑(insertIdx b j.succ (insertIdx a i ⟨l, hl⟩)) = ↑(insertIdx a i.castSucc (insertIdx b j ⟨l, hl⟩))
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
⊢ (⇑f)^[n₁] ((⇑f)^[n₂] (a₁ ⊔ a₂)) = (⇑f)^[n₁] ((⇑f)^[n₂] (a₂ ⊔ a₁))

Tactic:
sup_comm

Goal state after:
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
⊢ (⇑f)^[n₁] ((⇑f)^[n₂] (a₂ ⊔ a₁)) = (⇑f)^[n₁] ((⇑f)^[n₂] (a₂ ⊔ a₁))
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
⊢ (⇑f)^[n₁] ((⇑f)^[n₂] a₂ ⊔ a₁) = (⇑f)^[n₁] (a₁ ⊔ (⇑f)^[n₂] a₂)

Tactic:
sup_comm

Goal state after:
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
⊢ (⇑f)^[n₁] (a₁ ⊔ (⇑f)^[n₂] a₂) = (⇑f)^[n₁] (a₁ ⊔ (⇑f)^[n₂] a₂)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none

Tactic:
rw [dif_pos h']

Goal state after:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ some (Classical.choose h')
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
i j : ℕ
⊢ (c₀ i) (c₁ j) ≤ (c₀ i) (c₁ (max i j))

Tactic:
apply (c₀ i).monotone
      apply c₁.monotone
      apply le_max_right

Goal state after:
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]

Goal state after:
α : 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 α
⊢ (ωSup (c.map { toFun := f, monotone' := ⋯ })) (ωSup (c.map { toFun := g, monotone' := ⋯ })) =
    ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
b : Cardinal.{v}
⊢ lift.{max v w, u} a = lift.{max u w, v} b ↔ lift.{v, u} a = lift.{u, v} b

Tactic:
rw [← lift_lift.{v, w, u}, ← lift_lift.{u, w, v}, lift_inj]

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

Goal state before:
pp: a b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ a ≤ a ^ b

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Goal state after:
case inl
b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ 0 ≤ 0 ^ b

case inr
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a ≤ a ^ b
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case neg
a b c : Cardinal.{u_1}
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ max (a ^ c) 1

Tactic:
exact (power_le_power_left ha h).trans (le_max_left _ _)

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
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β✝
inst✝¹ : OmegaCompletePartialOrder γ✝
inst✝ : OmegaCompletePartialOrder δ
β γ : Type v
f : β → γ
g : α →𝒄 Part β
x✝ : α
⊢ f <$> g x✝ = (g.bind (const (pure ∘ f))) x✝

Tactic:
simp only [map_eq_bind_pure_comp, bind, coe_mk, OrderHom.partBind_coe, coe_apply,
      coe_toOrderHom, const_apply, Part.bind_eq_bind]

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

Goal state before:
pp: a : Cardinal.{u}
⊢ lift.{v, u} (succ a) = succ (lift.{v, u} a)

Tactic:
by
  apply (succ_le_of_lt <| lift_lt.2 <| lt_succ a).antisymm'
  by_contra! h
  rcases lt_lift_iff.1 h with ⟨b, h, hb⟩
  rw [lt_succ_iff, ← lift_le, hb] at h
  exact h.not_gt (lt_succ _)

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

Goal state before:
pp: case inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux

Tactic:
| inr hy =>

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

Goal state before:
pp: case inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux

Tactic:
| inr hy =>

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

Goal state before:
pp: α : Type u
s : Set α
f : ↑(ULift.down ⁻¹' s) → ULift.{?u.29, u} ↑s := fun x ↦ { down := s.restrictPreimage ULift.down x }
⊢ ↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s

Tactic:
have : Function.Bijective f :=
    ULift.up_bijective.comp (restrictPreimage_bijective _ (ULift.down_bijective))

Goal state after:
α : Type u
s : Set α
f : ↑(ULift.down ⁻¹' s) → ULift.{?u.37, u} ↑s := fun x ↦ { down := s.restrictPreimage ULift.down x }
this : Bijective f
⊢ ↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M b

Tactic:
rw [← smul_eq_mul] at ab
  exact ab.of_smul _

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

Goal state before:
pp: α : Type u
⊢ ¬#α ≤ ℵ₀ ↔ ¬Countable α

Tactic:
not_iff_not,

Goal state after:
α : Type u
⊢ #α ≤ ℵ₀ ↔ Countable α
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι α : Type u
A : ι → Set α
s : Set ι
⊢ #↑(⋃ x ∈ s, A x) ≤ #↑s * ⨆ x, #↑(A ↑x)

Tactic:
rw [biUnion_eq_iUnion]
  apply mk_iUnion_le

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

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

Tactic:
have := exists_notMem_of_length_lt [x, y] this

Goal state after:
α : Type u_1
h : 3 ≤ #α
x y : α
this✝¹ : ↑3 ≤ #α
this✝ : ↑2 < #α
this : ∃ z, z ∉ [x, y]
⊢ ∃ z, z ≠ x ∧ z ≠ y
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
h : a ≠ 0
⊢ 0 ^< a = 1

Tactic:
apply (powerlt_le.2 fun c _ => zero_power_le _).antisymm
  rw [← power_zero]
  exact le_powerlt 0 (pos_iff_ne_zero.2 h)

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r : R
m : M
inst✝ : IsTorsionFree R M
hr : IsRegular r
⊢ r • m = 0 ↔ m = 0

Tactic:
← hr.smul_right_inj (m₁ := m),

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r : R
m : M
inst✝ : IsTorsionFree R M
hr : IsRegular r
⊢ r • m = 0 ↔ r • m = r • 0
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : ∀ (r : R) (m : M), r • m = 0 → r = 0 ∨ m = 0
r : R
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ m₁ = m₂

Tactic:
simpa [sub_eq_zero, hr.ne_zero] using h r (m₁ - m₂) (by simpa [smul_sub, sub_eq_zero] using hm)

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

Goal state before:
pp: M : Type u_1
S : Set M
a : M
inst✝¹ : Mul M
inst✝ : HasDistribNeg M
ha : a ∈ S.centralizer
c : M
hc : c ∈ S
⊢ c * -a = -a * c

Tactic:
by rw [mul_neg, ha c hc, neg_mul]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
s : NonUnitalSubsemiring R
x : R × S
⊢ x ∈ s.prod ⊤ ↔ x ∈ comap (NonUnitalRingHom.fst R S) s

Tactic:
by simp [mem_prod]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
s : NonUnitalSubsemiring S
x : R × S
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (NonUnitalRingHom.snd R S) s

Tactic:
by simp [mem_prod]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
s : NonUnitalSubring R
x : R × S
⊢ x ∈ s.prod ⊤ ↔ x ∈ comap (NonUnitalRingHom.fst R S) s

Tactic:
by simp [mem_prod]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
s : NonUnitalSubring S
x : R × S
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (NonUnitalRingHom.snd R S) s

Tactic:
by simp [mem_prod]

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : A →ₐ[R] A
⊢ x✝ • 1 = 1

Tactic:
ext; exact map_one _

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

Goal state before:
pp: case mp
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ f ((algebraMap R A) r) ∈ algebraMapSubmonoid B M

Tactic:
simp only [AlgHom.commutes]

Goal state after:
case mp
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ (algebraMap R B) r ∈ algebraMapSubmonoid B M
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
s : Subsemiring R
x : R × S
⊢ x ∈ s.prod ⊤ ↔ x ∈ comap (RingHom.fst R S) s

Tactic:
by simp [mem_prod]

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
s : Subsemiring S
x : R × S
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (RingHom.snd R S) s

Tactic:
by simp [mem_prod]

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s t : Subsemiring R
g : S → R
f : R →+* S
h : Function.LeftInverse g ⇑f
x : ↥f.rangeS
⊢ ↑((fun x ↦ f.rangeSRestrict x) ((fun x ↦ (g ∘ ⇑f.rangeS.subtype) x) x)) = ↑x

Tactic:
by
        let ⟨x', hx'⟩ := RingHom.mem_rangeS.mp x.prop
        simp [← hx', h x']

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
s : Subring R
x : R × S
⊢ x ∈ s.prod ⊤ ↔ x ∈ comap (RingHom.fst R S) s

Tactic:
by simp [mem_prod]

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
s : Subring S
x : R × S
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (RingHom.snd R S) s

Tactic:
by simp [mem_prod]

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd = -1
⊢ (hd :: tl).prod = L.prod

Tactic:
by rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : Associates M
⊢ IsUnit a ↔ a = ⊥

Tactic:
by
  rw [Associates.isUnit_iff_eq_one, bot_eq_one]

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
⊢ s • N ≤ p ↔ ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p

Tactic:
fconstructor

Goal state after:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
⊢ s • N ≤ p → ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p

case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
⊢ (∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) → s • N ≤ p
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
⊢ s • N ≤ p ↔ ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p

Tactic:
by
  fconstructor
  · intro h r n hr hn
    exact h <| mem_set_smul_of_mem_mem hr hn
  · apply set_smul_le

Goal state after: