mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a : ℕ
⊢ (↑a)⁻¹.den = if a = 0 then 1 else a

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' = Int.ofNat (a.pow b' * a.pow b')

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : FunLike F α β
R : Type u_5
inst✝ : Semiring R
f g : ℚ≥0 →+* R
⊢ ∀ (n : ℕ), f ↑n = g ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n✝¹ n✝ : ℕ
⊢ ↑n✝¹ ^ ↑n✝ = ↑(n✝¹.pow n✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n✝¹ : ℤ
n✝ : ℕ
⊢ ↑n✝¹ ^ ↑n✝ = ↑(n✝¹.pow n✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNat (a ^ nb)⁻¹ ne
⊢ IsNat (a ^ b) ne

Tactic:
by
  rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)
⊢ IsInt (a ^ b) (Int.negOfNat ne)

Tactic:
by
  rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNNRat (a ^ nb)⁻¹ num den
⊢ IsNNRat (a ^ b) num den

Tactic:
by
  rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsRat (a ^ nb)⁻¹ num den
⊢ IsRat (a ^ b) num den

Tactic:
by
  rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ ↑n.rawCast = n.rawCast

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₁ a₃ a₂ : ℕ
⊢ ↑(a₁ ^ a₂ * a₃) = ↑a₁ ^ a₂ * ↑a₃

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ : ℕ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
n : ℕ
⊢ ↑n.rawCast = n.rawCast

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
n : ℕ
⊢ ↑(Int.negOfNat n).rawCast = (Int.negOfNat n).rawCast

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a₁ a₃ : ℤ
a₂ : ℕ
⊢ ↑(a₁ ^ a₂ * a₃) = ↑a₁ ^ a₂ * ↑a₃

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a₁ a₂ : ℤ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b : R
⊢ 0 + b = b

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a + 0 = a

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : Nontrivial R
k : R
⊢ 0 < 2 * k + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a * 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b : R
⊢ 0 * b = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a : R
⊢ -a = -1 * a

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * -a₃

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
⊢ -0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a ^ 1 = a

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝⁶ : NonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * (b - 1) = a * b - a

Tactic:
by rw [mul_tsub, mul_one]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a ^ Nat.rawCast 1 = a

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : Semifield R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ (a₁ ^ a₂ * a₃)⁻¹ = a₃⁻¹ * (a₁⁻¹ ^ a₂ * Nat.rawCast 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ : ℕ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ULift

Goal state before:
pp: α : Sort u
x y : α
⊢ { down := x } = { down := y } ↔ x = y

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ULift

Goal state before:
pp: α : Type u
x y : α
⊢ { down := x } = { down := y } ↔ x = y

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ 0 ∈ {0} ∪ range succ ↔ 0 ∈ univ

Tactic:
simp

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ n✝ + 1 ∈ {0} ∪ range succ ↔ n✝ + 1 ∈ univ

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ 0 ∈ range succ ↔ 0 ∈ {i | 0 < i}

Tactic:
simp

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

Goal state before:
pp: case succ
i : ℕ
⊢ i + 1 ∈ range succ ↔ i + 1 ∈ {i | 0 < i}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : InfSet α
isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)
a : α
⊢ a ∈ lowerBounds ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : SupSet α
isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)
x : α
⊢ x ∈ upperBounds ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
⊢ ⨅ i, ⨅ (_ : i > 0), f i = ⨅ b ∈ {i | 0 < i}, f b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.BooleanAlgebra

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : Set α), a ⊆ univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift ι → α
x : α
⊢ (x ∈ range fun i ↦ f i) ↔ x ∈ range fun i ↦ f { down := i }

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j = ⊥ ↔ ∀ (i : ι) (j : κ i), f i j = ⊥

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : False → α
⊢ iSup s = ⊥

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ x ∈ ∅, f x = ⊥

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ x ∈ univ, f x = ⨆ x, f x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
i₀ : β
⊢ f i₀ = ⨆ i, ⨆ (_ : i = i₀), f i

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
b : β
⊢ ⨆ x ∈ {b}, f x = f b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
a b : β
⊢ ⨆ x ∈ {a, b}, f x = f a ⊔ f b

Tactic:
rw [iSup_insert, iSup_singleton]

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set α
s : α → Set β
⊢ (⋃ i ∈ t, s i).Nonempty ↔ ∃ i ∈ t, (s i).Nonempty

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
s : Set α
t : α → Set β
⊢ ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ∀ (x : α), x ∈ ⋃ x ∈ s, {x} ↔ x ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
s : Set α
t : α → Set β
⊢ ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
a b : α
s : α → Set β
⊢ ⋃ x ∈ {a, b}, s x = s a ∪ s b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
a : α
⊢ a ⊓ ⨆ i, ⨆ j, f i j = ⨆ i, ⨆ j, a ⊓ f i j

Tactic:
by
  simp only [minAx.inf_iSup_eq]

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋂ i, ⋂ j, s i j).Nonempty ↔ ∃ a, ∀ (i : ι) (j : κ i), a ∈ s i j

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
x : α
⊢ x ∈ (⋃₀ S)ᶜ ↔ x ∈ ⋂₀ (compl '' S)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : α → Type u_12
f : Sigma γ → β
⊢ ∀ (x : β), x ∈ range f ↔ x ∈ ⋃ a, range fun b ↦ f ⟨a, b⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
⊢ ⋃ i, Sigma.mk i '' Sigma.mk i ⁻¹' s = s

Tactic:
by
  ext x
  simp only [mem_iUnion, mem_image, mem_preimage]
  grind

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ⋃ i, {↑i} = s

Tactic:
simp

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

Goal state before:
pp: α : Type u_8
s : Set (α → Prop)
a : α
⊢ sSup s a ↔ ∃ r ∈ s, r a

Tactic:
simp

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

Goal state before:
pp: α : Type u_8
s : Set (α → Prop)
a : α
⊢ sInf s a ↔ ∀ r ∈ s, r a

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_12
σ : Type u_13
s : ι → Set α
t : σ → Set α
x✝ : α
⊢ x✝ ∈ ⋃ x, Sum.elim s t x ↔ x✝ ∈ (⋃ x, s x) ∪ ⋃ x, t x

Tactic:
simp

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

Goal state before:
pp: α : Type u_8
β : Type u_9
s : Set (α → β → Prop)
a : α
b : β
⊢ sSup s a b ↔ ∃ r ∈ s, r a b

Tactic:
simp

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

Goal state before:
pp: α : Type u_8
β : Type u_9
s : Set (α → β → Prop)
a : α
b : β
⊢ sInf s a b ↔ ∀ r ∈ s, r a b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
π : α → Type u_12
i : Set α
s : (a : α) → Set (π a)
x✝ : (i : α) → π i
⊢ x✝ ∈ i.pi s ↔ x✝ ∈ ⋂ a ∈ i, eval a ⁻¹' s a

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
π : α → Type u_12
α' : Type u_13
s : α' → Set α
t : (a : α) → Set (π a)
f : (i : α) → π i
⊢ f ∈ (⋃ i, s i).pi t ↔ f ∈ ⋂ i, (s i).pi t

Tactic:
simp

Goal state after:
α : Type u_1
π : α → Type u_12
α' : Type u_13
s : α' → Set α
t : (a : α) → Set (π a)
f : (i : α) → π i
⊢ (∀ (i : α) (x : α'), i ∈ s x → f i ∈ t i) ↔ ∀ (i : α'), ∀ i_1 ∈ s i, f i_1 ∈ t i_1
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : InfSet α
⊢ ∅ ⊆ {⊤} ∨ ¬BddBelow ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
⊢ sSup {⊤} = ⊤

Tactic:
simp

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

Goal state before:
pp: case hnc
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ⊤ ∉ (fun a ↦ ↑a) '' s

Tactic:
· rintro ⟨x, _, ⟨⟩⟩

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

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
⊢ ⊤ ∉ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : Frame α
a : α
f : ι → α
b : α
⊢ b ≤ a ⇨ ⨅ x, f x ↔ b ≤ ⨅ x, a ⇨ f x

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : Frame α
a : α
f : ι → α
b : α
⊢ b ≤ (⨆ x, f x) ⇨ a ↔ b ≤ ⨅ x, f x ⇨ a

Tactic:
by simp [inf_iSup_eq]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
⊢ sSup (∅ ∪ t) ≤ max (sSup ∅) (sSup t)

Tactic:
simp

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.Nonempty
⊢ sSup (s ∪ ∅) ≤ max (sSup s) (sSup ∅)

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
ht : BddAbove t
hs : BddAbove ∅
⊢ sSup (∅ ∪ t) = max (sSup ∅) (sSup t)

Tactic:
simp

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

Goal state before:
pp: case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ BddBelow ((fun a ↦ ↑a) ⁻¹' s)

Tactic:
exfalso
        apply h
        intro c hc
        rw [mem_singleton_iff, ← top_le_iff]
        exact hb hc

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Icc (e x) (e y) ↔ x✝ ∈ Icc x y

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ico (e x) (e y) ↔ x✝ ∈ Ico x y

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ioc (e x) (e y) ↔ x✝ ∈ Ioc x y

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ioo (e x) (e y) ↔ x✝ ∈ Ioo x y

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Lattice α
inst✝ : Lattice β
a b : α × β
⊢ [[a, b]] = [[a.1, b.1]] ×ˢ [[a.2, b.2]]

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
⊢ ∅.Pairwise (r on f) ↔ ∃ z, ∀ (x : α), x ∈ ∅ → r (f x) z

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → α
⊢ (Pairwise fun i j ↦ f i ≠ f j) ↔ Injective f

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
r : α → α → Prop
c c₁ c₂ s✝ t : Set α
a b x y : α
inst✝¹ : PartialOrder α
inst✝ : DecidableLE α
s : Set α
hs : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
⊢ ∀ (a b : ↑s), a ≤ b ∨ b ≤ a

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_3
r : α → α → Prop
c c₁ c₂ s✝ t : Set α
a✝ b✝ x y : α
inst✝¹ : PartialOrder α
inst✝ : DecidableLE α
s : Set α
hs : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ ⟨a, ha⟩ ≤ ⟨b, hb⟩ ∨ ⟨b, hb⟩ ≤ ⟨a, ha⟩
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝ : LE α
s✝ t✝ : Flag α
a : α
s t : Flag α
h : s.carrier = t.carrier
⊢ s = t

Tactic:
by
    cases s
    cases t
    congr

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
hs : IsChain r s
ht : IsAntichain r t
⊢ s ∩ t ⊆ s

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
hs : IsChain r s
ht : IsAntichain r t
⊢ s ∩ t ⊆ t

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : NoZeroDivisors α
⊢ ∀ {a b : { x // 0 ≤ x }}, a * b = 0 → a = 0 ∨ b = 0

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Goal state after:
α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : NoZeroDivisors α
a : α
ha : 0 ≤ a
b : α
hb : 0 ≤ b
⊢ ⟨a, ha⟩ * ⟨b, hb⟩ = 0 → ⟨a, ha⟩ = 0 ∨ ⟨b, hb⟩ = 0
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case neg
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬S = ∅
⊢ IsGLB S ⟨sInf (Subtype.val '' S), ⋯⟩

Tactic:
· exact .of_image Subtype.coe_le_coe <| isGLB_csInf ((Set.nonempty_iff_ne_empty.mpr hS).image _)
        ((Subtype.mono_coe _).map_bddBelow (OrderBot.bddBelow S))

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝ : CompleteLattice α
a : α
S : Set ↑(Iic a)
⊢ a ⊓ sInf (Subtype.val '' S) ∈ Iic a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝ : CompleteLattice α
a : α
⊢ ∀ (a_1 : ↑(Iic a)), a_1 ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝ : CompleteLattice α
a : α
⊢ ∀ (a_1 : ↑(Iic a)), ⊥ ≤ a_1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
x✝ : α
⊢ (x✝ ∈ Subtype.val '' range fun i ↦ f i) ↔ x✝ ∈ range fun i ↦ ↑(f i)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
⊢ ↑(⨆ i, ⨆ (_ : p i), f i) = ⨆ i, ⨆ (_ : p i), ↑(f i)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case e_a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
x✝ : α
⊢ (x✝ ∈ Subtype.val '' range fun i ↦ f i) ↔ x✝ ∈ range fun i ↦ ↑(f i)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case inl
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
h✝ : IsEmpty ι
⊢ ↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsInt a (Int.negOfNat na)
⊢ |↑(Int.negOfNat na)| = ↑na

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: case H1
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ 0 ≤ ↑r

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: case H1
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ 0 ≤ ↑r

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: case hb
K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ 0 < ↑p.den

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: case hd
K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ 0 < ↑q.den

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ (∀ (x : ι), ¬x ∈ ∅ → f x = 1) ↔ ∀ (x : ι), f x = 1 x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
⊢ mulSupport (mulSingle i 1) = ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : a = 1
⊢ ∅.Subsingleton

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : ¬a = 1
⊢ {i}.Subsingleton

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.Cast.Field

Goal state before:
pp: R : Type u_2
inst✝ : DivisionRing R
n : ℕ
⊢ ↑(-↑n) = -↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.Cast.Field

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
⊢ ↑(n * k / n) = ↑(n * k) / ↑n

Tactic:
have : n ≠ 0 := by rintro rfl; simp at hn

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
this : n ≠ 0
⊢ ↑(n * k / n) = ↑(n * k) / ↑n
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m : ℕ
⊢ m ! * (m + 1) ^ 0 ≤ (m + 0)!

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!

Tactic:
have := (i + n).self_le_factorial

Goal state after:
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
h✝ : 0 < 2
⊢ 0 + (n + 1)! ≤ (0 + (n + 1))!

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : 0 < n
⊢ n.pred ! * (n.pred + succ 0).ascFactorial k = (n.pred + k)!

Tactic:
factorial_mul_ascFactorial

Goal state after:
n k : ℕ
h : 0 < n
⊢ (n.pred + k)! = (n.pred + k)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n.ascFactorial 0 ≤ 0! * n ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n.descFactorial 1 = n

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n - k = 0 ∨ n < k ↔ n ≤ k

Tactic:
Nat.sub_eq_zero_iff_le,

Goal state after:
n k : ℕ
⊢ n ≤ k ∨ n < k ↔ n ≤ k