mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
x✝ : R
⊢ (e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom) x✝ = (NonUnitalRingHom.id R) x✝

Tactic:
simp

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
x : G × ↥S
eq : m * f ↑x.2 = f x.1
⊢ ∃ a, f a = m

Tactic:
use x.1 / x.2

Goal state after:
case h
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
x : G × ↥S
eq : m * f ↑x.2 = f x.1
⊢ f (x.1 / ↑x.2) = m
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
e : R ≃+* S
⊢ e.toRingHom.comp e.symm.toRingHom = RingHom.id S

Tactic:
simp

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
e : R ≃+* S
⊢ e.symm.toRingHom.comp e.toRingHom = RingHom.id R

Tactic:
simp

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

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x : WithTop α
⊢ x - ⊤ ≤ ⊤ ↔ x ≤ ⊤ + ⊤

Tactic:
simp

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

Goal state before:
pp: case top.coe
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x : WithTop α
a✝ : α
⊢ x - ⊤ ≤ ↑a✝ ↔ x ≤ ↑a✝ + ⊤

Tactic:
simp

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

Goal state before:
pp: case coe.top
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
z : WithTop α
a✝ : α
⊢ ⊤ - ↑a✝ ≤ z ↔ ⊤ ≤ z + ↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.coe.top
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝¹ a✝ : α
⊢ ↑a✝ - ↑a✝¹ ≤ ⊤ ↔ ↑a✝ ≤ ⊤ + ↑a✝¹

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
⊢ map (⇑f) (0 * y) = map (⇑f) 0 * map (⇑f) y

Tactic:
simp

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
x : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * 0) = map (⇑f) x * map (⇑f) 0

Tactic:
simp

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

Goal state before:
pp: case top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
⊢ (match ⊤, 0 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    1

Tactic:
simp

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

Goal state before:
pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a✝ : α
⊢ (match ↑a✝, 0 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    1

Tactic:
simp

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

Goal state before:
pp: case top.zero
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
⊢ ⊤ ^ 0 = ⊤ ↔ ⊤ = ⊤ ∧ 0 ≠ 0

Tactic:
simp [← coe_pow]

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

Goal state before:
pp: case top.succ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n✝ : ℕ
⊢ ⊤ ^ (n✝ + 1) = ⊤ ↔ ⊤ = ⊤ ∧ n✝ + 1 ≠ 0

Tactic:
simp [← coe_pow]

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

Goal state before:
pp: case coe.zero
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a✝ : α
⊢ ↑a✝ ^ 0 = ⊤ ↔ ↑a✝ = ⊤ ∧ 0 ≠ 0

Tactic:
simp [← coe_pow]

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

Goal state before:
pp: case coe.succ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a✝ : α
n✝ : ℕ
⊢ ↑a✝ ^ (n✝ + 1) = ⊤ ↔ ↑a✝ = ⊤ ∧ n✝ + 1 ≠ 0

Tactic:
simp [← coe_pow]

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ ↑s₁ * r • 1 = r • 1 * ↑s₁

Tactic:
simp

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

Goal state before:
pp: case c.c
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ (r • 1 * r₁ /ₒ s₁) • (r₂ /ₒ s₂) = (r₁ * r • 1 /ₒ s₁) • (r₂ /ₒ s₂)

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
a b : WithBot α
h : a ≤ b
x0 : 0 ≤ 0
⊢ 0 * a ≤ 0 * b

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
a b : WithBot α
h : a ≤ b
x0 : 0 ≤ 0
⊢ a * 0 ≤ b * 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
x✝¹ : WithBot α
x✝ : ⊥ ≤ x✝¹
⊢ ⊥.succ ≤ x✝¹.succ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
b : α
hab : ⊥ < ↑b
⊢ ⊥.succ < (↑b).succ

Tactic:
simp

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

Goal state before:
pp: case bot
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
⊢ ⊥.succ = ⊥ ↔ ⊥ = ⊥

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
x✝¹ : WithTop α
x✝ : x✝¹ ≤ ⊤
⊢ x✝¹.pred ≤ ⊤.pred

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderTop α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
b : α
hab : ↑b < ⊤
⊢ (↑b).pred < ⊤.pred

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
⊢ v₁ < v₂ ∨ v₂ ≤ v₁

Tactic:
rw [Classical.or_iff_not_imp_right]
  intro nh
  rcases le_total_of_codirected h₁ h₂ with h | h
  · apply lt_of_le_of_ne h (ne_of_not_le nh).symm
  · contradiction

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

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

Tactic:
simp

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

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

Tactic:
by
  simpa [WithTop.isPredPrelimit_iff, isPredLimit_iff, WithTop.exists] using h

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

Goal state before:
pp: α : Type u_1
a : α
inst✝⁴ : Preorder α
inst✝³ : SuccOrder α
inst✝² : IsSuccArchimedean α
inst✝¹ : NoMaxOrder α
inst✝ : NoMinOrder α
⊢ ¬IsSuccPrelimit a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Iic a ⊆ Iio (succ a)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
a : α
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMinOrder α
⊢ ¬IsSuccPrelimit a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b : α
ha : IsLUB (Iic b) b
hb : b ⋖ b
⊢ False

Tactic:
cases hb.lt.false

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ succ a ≤ succ b ↔ a ≤ b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ succ a < succ b ↔ a < b

Tactic:
simp

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

Goal state before:
pp: case zero
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
a : Y
⊢ succ^[0] a = f (succ^[0] (EquivLike.inv f a))

Tactic:
simp

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

Goal state before:
pp: case zero
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
b : Y
⊢ pred^[0] b = f (pred^[0] (EquivLike.inv f b))

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
h₀ h₁ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ SuccOrder.succ a = SuccOrder.succ a

Tactic:
exact @CovBy.succ_eq _ _ h₀ _ _ (covBy_succ_of_not_isMax ha)

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

Goal state before:
pp: case zero
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
hb : succ^[0] a ∈ s
⊢ f a ≤ f (succ^[0] a)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : SuccAddOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : NeZero 1
x✝ : α
⊢ x✝ ∈ Set.Iio 1 ↔ x✝ ∈ {0}

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
ha : pred^[0] b ∈ s
⊢ f (pred^[0] b) ≤ f b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a b : WithTop α
h : a < b
⊢ a ≤
    match b with
    | none => ↑⊤
    | Option.some a => ↑(pred a)

Tactic:
by
    cases a
    · exact (le_top.not_gt h).elim
    cases b
    · exact coe_le_coe.2 le_top
    exact coe_le_coe.2 (le_pred_of_lt <| coe_lt_coe.1 h)

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

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
ha : ⊤ ≠ ⊤
⊢ pred ⊤ ≠ ⊤

Tactic:
simp

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

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a✝ : α
ha : ↑a✝ ≠ ⊤
⊢ pred ↑a✝ ≠ ⊤

Tactic:
simp

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

Goal state before:
pp: case top
a b c d m n : ℕ∞
⊢ SuccOrder.succ ⊤ = ⊤ + 1

Tactic:
simp

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

Goal state before:
pp: case coe
a b c d m n : ℕ∞
a✝ : ℕ
⊢ SuccOrder.succ ↑a✝ = ↑a✝ + 1

Tactic:
simp

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

Goal state before:
pp: a b : ℕ∞
h : a + b < ⊤
⊢ ↑((a + b).lift h) = ↑(a.lift ⋯ + b.lift ⋯)

Tactic:
simp

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

Goal state before:
pp: case coe
m : ℕ
inst✝ : NeZero m
a✝ : ℕ
⊢ (↑a✝).toNat = m ↔ ↑a✝ = ↑m

Tactic:
simp

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

Goal state before:
pp: case top.top
⊢ (⊤ * ⊤).toNat = ⊤.toNat * ⊤.toNat

Tactic:
simp

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

Goal state before:
pp: case top.coe.zero
⊢ (⊤ * ↑0).toNat = ⊤.toNat * (↑0).toNat

Tactic:
simp

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

Goal state before:
pp: case top.coe.succ
n✝ : ℕ
⊢ (⊤ * ↑(n✝ + 1)).toNat = ⊤.toNat * (↑(n✝ + 1)).toNat

Tactic:
simp

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

Goal state before:
pp: case coe.top.zero
⊢ (↑0 * ⊤).toNat = (↑0).toNat * ⊤.toNat

Tactic:
simp

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

Goal state before:
pp: case coe.top.succ
n✝ : ℕ
⊢ (↑(n✝ + 1) * ⊤).toNat = (↑(n✝ + 1)).toNat * ⊤.toNat

Tactic:
simp

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

Goal state before:
pp: n m : ℕ
⊢ ↑n < ↑m ↔ n < m

Tactic:
simp

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

Goal state before:
pp: n m : ℕ
⊢ ↑n ≤ ↑m ↔ n ≤ m

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ ↑n < ↑n + 1

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, natCast_lt_natCast]

Goal state after:
n : ℕ
⊢ n < n + 1
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case top
a : ℕ∞
h : a < ⊤
⊢ a ≤ ⊤ - 1

Tactic:
simp

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

Goal state before:
pp: case inr.inl
c : ℕ∞
hc : c ≠ 0
hne : 0 ≠ ⊤
⊢ 0 ≤ 0 * c

Tactic:
simp

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

Goal state before:
pp: n : WithTop ℕ∞
⊢ ↑⊤ + 1 = ↑⊤ ↔ ↑⊤ = ↑⊤

Tactic:
simp

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

Goal state before:
pp: case top
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
⊢ 0 ≤ map Nat.cast ⊤

Tactic:
simp

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

Goal state before:
pp: case coe
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
a✝ : ℕ
⊢ 0 ≤ map Nat.cast ↑a✝

Tactic:
simp

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

Goal state before:
pp: a b c d m n : ℕ∞
α : Type u_1
N : Type u_2
inst✝ : One N
f : OneHom ℕ N
⊢ map (⇑f) 1 = 1

Tactic:
simp

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

Goal state before:
pp: a b c d m n : ℕ∞
α : Type u_1
N : Type u_2
inst✝ : Zero N
f : ZeroHom ℕ N
⊢ map (⇑f) 0 = 0

Tactic:
simp

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

Goal state before:
pp: case inl
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
⊢ map (⇑f) (0 * y) = map (⇑f) 0 * map (⇑f) y

Tactic:
simp

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

Goal state before:
pp: case inr.inl
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
x : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * 0) = map (⇑f) x * map (⇑f) 0

Tactic:
simp

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

Goal state before:
pp: case e_s
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
x✝ : ι
⊢ ↑(insert j s) = insert j ↑s

Tactic:
simp

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

Goal state before:
pp: case bot
n : ℕ
⊢ ↑↑(n + 1) ≤ ⊥ ↔ ↑n < ⊥

Tactic:
simp

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

Goal state before:
pp: case bot
m : ℕ
⊢ ⊥ + 1 ≤ ↑m ↔ ⊥ < ↑m

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Sigma

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : Fintype ι
⊢ ∀ (x : (i : ι) × κ i), x ∈ univ.sigma fun x ↦ univ

Tactic:
simp

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

Goal state before:
pp: case e_1
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun x ↦ x ∈ s) = fun x ↦ x ∈ {x | x ∈ s}

Tactic:
simp

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

Goal state before:
pp: case e_4.e_2
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
a✝ : ι
⊢ a✝ ∈ s ↔ a✝ ∈ {x | x ∈ s}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
fill : α
⊢ n - i + min n i = n

Tactic:
simp

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
⊢ ∀ {α : Type u} (x : α), id (pure x) = pure x

Tactic:
simp

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
α✝ β✝ : Type u
x : F (α✝ → β✝)
y : F α✝
⊢ id (x <*> y) = id x <*> id y

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case inl
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
val✝ : α
⊢ Sum.inl val✝ ∈ univ.disjSum univ

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case inr
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
val✝ : β
⊢ Sum.inr val✝ ∈ univ.disjSum univ

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
a✝ : α
⊢ a✝ ∈ univ.toLeft ↔ a✝ ∈ univ

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
a✝ : β
⊢ a✝ ∈ univ.toRight ↔ a✝ ∈ univ

Tactic:
simp

Goal state after:
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 ι
i : ι
h : i ∉ s
f : ι → M
b : M
⊢ ∀ x ∈ s, Function.update f i b x = f x

Tactic:
intro j

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∉ s
f : ι → M
b : M
j : ι
⊢ j ∈ s → Function.update f i b j = f j
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
e : α ≃ ↥t
⊢ ∀ i ∈ ∅, ↑(e i) = f i

Tactic:
simp

Goal state after:
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 ι
f : ι → M
a : ι
⊢ (∏ x ∈ s, f x ^ if a = x then 1 else 0) = if a ∈ s then f a else 1

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
⊢ (∏ i, if i ∈ s then f i else 1) = ∏ i ∈ s, f i

Tactic:
simp

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type v
f : α → β
x : α
⊢ (f <$> pure x).run = (pure (f x)).run

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case h.inl
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
s : Finset α
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
i : α
has : i ∉ s
hfst : image f (insert i s) ⊆ t
hfs : Set.InjOn f ↑(insert i s)
hfat : f i ∈ t
⊢ ↑((g'.trans (Equiv.swap ⟨f i, hfat⟩ (g' i))) i) = f i

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
p q : α → Prop
h : Disjoint p q
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x } + card { x // q x } = card ({ x // p x } ⊕ { x // q x })

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s a✝ : Finset α
⊢ a✝ ∈ {t | t ⊆ s} ↔ a✝ ∈ s.powerset

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
k : ℕ
a✝ : Finset α
⊢ a✝ ∈ {s | #s = k} ↔ a✝ ∈ powersetCard k univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Set α
⊢ {x | x ∈ Finset.univ ∧ x ∈ s} = s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : List α
hv : v.length = n
w : List α
hw : w.length = n
h : ∀ (m : Fin n), get ⟨v, hv⟩ m = get ⟨w, hw⟩ m
⊢ n = (↑⟨w, hw⟩).length

Tactic:
hw

Goal state after:
α : Type u_1
n : ℕ
v : List α
hv : v.length = n
w : List α
hw : w.length = n
h : ∀ (m : Fin n), get ⟨v, hv⟩ m = get ⟨w, hw⟩ m
⊢ n = n
Module: Mathlib.Data.Countable.Basic

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Uncountable α
inst✝ : Nonempty β
⊢ Uncountable (α × β)

Tactic:
inhabit β

Goal state after:
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Uncountable α
inst✝ : Nonempty β
inhabited_h : Inhabited β
⊢ Uncountable (α × β)
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n✝ n' m : ℕ
s : Sym α n✝
a b : α
n : ℕ
f : α → β
x : Sym α n
⊢ (Multiset.map f ↑x).card = n

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ Multiset.map g (Multiset.map f ↑s) = Multiset.map (g ∘ f) ↑s

Tactic:
simp

Goal state after:
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 : ℕ
v : Vector α n
⊢ v.toList.reverse.length = n

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a✝ b a : α
⊢ {a}.card = 1

Tactic:
simp

Goal state after: