mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α × β
⊢ Icc a b = Icc a.1 b.1 ×ˢ Icc a.2 b.2

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) = ↑a✝

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ ↑n✝ = ↑(Int.ofNat n✝)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
num : ℕ
inv : Invertible ↑1
this : Invertible 1
⊢ ↑num * ⅟↑1 = ↑num

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
a✝ denom✝ : ℕ
inv : Invertible ↑denom✝
⊢ ↑(Int.ofNat a✝) * ⅟↑denom✝ = ↑a✝ * ⅟↑denom✝

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n✝ : ℕ
⊢ 1 * ↑1 = 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n✝ : ℕ
⊢ ↑1 * 1 = 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n✝ : ℕ
⊢ ↑n✝ = ↑n✝ * ⅟↑1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
num✝ denom✝ : ℕ
inv : Invertible ↑denom✝
⊢ ↑num✝ * ⅟↑denom✝ = ↑(Int.ofNat num✝) * ⅟↑denom✝

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
num✝ : ℤ
inv : Invertible ↑1
this : Invertible 1
⊢ ↑num✝ * ⅟↑1 = ↑num✝

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ 1 * ↑1 = 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ ↑1 * 1 = 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ ↑n✝ = ↑n✝ * ⅟↑1

Tactic:
by simp

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
c : ℤ
⊢ smulg c 0 = 0

Tactic:
simp [smulg, zsmul_zero]

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

Goal state before:
pp: a✝ : ℕ
⊢ (↑(Int.negOfNat a✝)).natAbs = ↑a✝

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ ↑↑m = ↑m

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
⊢ IsLUB ((fun b ↦ 0 * b) '' s) (0 * b)

Tactic:
· simp_rw [zero_mul]
    obtain rfl | ne := s.eq_empty_or_nonempty
    · simp only [Set.image_empty, isLUB_empty_iff] at hs ⊢
      have hb := hs (b + b)
      rw [le_add_iff_nonneg_right] at hb
      exact hs.mono hb
    rw [ne.image_const]
    exact isLUB_singleton

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

Goal state before:
pp: n✝ : ℕ
⊢ (↑n✝).succ = ↑n✝.succ

Tactic:
by simp

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

Goal state before:
pp: n✝¹ n✝ : ℕ
⊢ ↑n✝¹ - ↑n✝ = ↑(n✝¹.sub n✝)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
l : List α
i : ℕ
h : i < l.length
⊢ take i l ++ [l[i]] = take (i + 1) l

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
Rₐ : α → α → Prop
⊢ Forall₂ Rₐ [] [] ↔ ∀ (x : α), x ∈ [] → Rₐ x x

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (take l₁.length l) l₁

Tactic:
have h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂)) :=
    forall₂_take (length l₁) h

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (take l₁.length l) (take l₁.length (l₁ ++ l₂))
⊢ Forall₂ R (take l₁.length l) l₁
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
f : α → α
hf : Involutive f
l : List α
y : α
h : y ∈ l
⊢ f (f y) ∈ l

Tactic:
hf y

Goal state after:
α : Type u
f : α → α
hf : Involutive f
l : List α
y : α
h : y ∈ l
⊢ y ∈ l
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
a b : α
p : (some a).toList ~ (some b).toList
⊢ b ∈ (some b).toList

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
L : List M
i : ℕ
p : i < L.length
⊢ (take i L ++ [L[i]]).prod = (take i L).prod * L[i]

Tactic:
prod_append

Goal state after:
M : Type u_4
inst✝ : Monoid M
L : List M
i : ℕ
p : i < L.length
⊢ (take i L).prod * [L[i]].prod = (take i L).prod * L[i]
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
a : α
⊢ [] = replicate [].length a ↔ ∀ (b : α), b ∈ [] → b = a

Tactic:
by simp

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

Goal state before:
pp: α : Type u
a b : α
⊢ replicate 0 a = replicate 0 b ↔ 0 = 0 ∨ a = b

Tactic:
by simp

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

Goal state before:
pp: α : Type u
x y : α
⊢ x ∈ pure y ↔ x = y

Tactic:
by simp

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

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ (l ++ [a]).reverse = a :: l.reverse

Tactic:
rw [reverse_append]

Goal state after:
α : Type u
l : List α
a : α
⊢ [a].reverse ++ l.reverse = a :: l.reverse
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₂ ≠ []
⊢ (l₁ ++ l₂).getLast ⋯ = l₂.getLast h

Tactic:
induction l₁ with

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

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ : List α
a : α
l : List α
⊢ l.concat a ≠ []

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
i : Fin l.length
⊢ l[i]?.isSome = true

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
ys : List M
⊢ [].prod * ys.prod = (zipWith (fun x1 x2 ↦ x1 * x2) [] ys).prod * (drop ys.length []).prod * (drop [].length ys).prod

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
xs : List M
⊢ xs.prod * [].prod = (zipWith (fun x1 x2 ↦ x1 * x2) xs []).prod * (drop [].length xs).prod * (drop xs.length []).prod

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
x y : α
hx : x ∈ l
⊢ idxOf x l = idxOf y l ↔ x = y

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ rfl⟩

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
x y : α
hx : x ∈ l
h : idxOf x l = idxOf y l
⊢ x = y
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : Group G
⊢ [].prod⁻¹ = (map (fun x ↦ x⁻¹) []).reverse.prod

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : Group G
head✝ : G
tail✝ : List G
x✝ : 0 < (head✝ :: tail✝).length
⊢ (drop (0 + 1) (head✝ :: tail✝)).prod = (head✝ :: tail✝)[0]⁻¹ * (drop 0 (head✝ :: tail✝)).prod

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: K : Type u_8
inst✝ : DivisionCommMonoid K
⊢ [].prod⁻¹ = (map (fun x ↦ x⁻¹) []).prod

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
p : α → Bool
f : α → β
hf : Injective f
l : List α
inst✝ : DecidablePred fun b ↦ ∃ a, p a = true ∧ f a = b
⊢ map f (filter p l) = filter (fun b ↦ decide (∃ a, p a = true ∧ f a = b)) (map f l)

Tactic:
simp [comp_def, filter_map, hf.eq_iff]

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

Goal state before:
pp: x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x * (x /. d) = n /. d

Tactic:
by_cases hd : d = 0

Goal state after:
case pos
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. d) = n /. d

case neg
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n /. x * (x /. d) = n /. d
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
p : α → Prop
ys✝ : List α
⊢ Forall p ([] ++ ys✝) ↔ Forall p [] ∧ Forall p ys✝

Tactic:
by simp

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

Goal state before:
pp: α : Type u
l : List α
i : Fin l.attach.length
⊢ ↑(l.attach.get i) = l.get ⟨↑i, ⋯⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a : α
u : αˣ
⊢ a = ↑u * (↑u⁻¹ * a)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 = 0 * 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : SemigroupWithZero α
a : α
⊢ a * 0 = 0

Tactic:
by simp

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

Goal state before:
pp: n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ ⟨n, hn⟩ ≤ ⟨k, hk⟩ ↔ n ≤ k

Tactic:
by simp

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

Goal state before:
pp: n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ ⟨n, hn⟩ < ⟨k, hk⟩ ↔ n < k

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ q₁.den ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ q₂.den ≠ 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : DivisionRing R
n✝ : ℕ
⊢ ↑↑n✝ = ↑n✝

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
n✝ : ℕ
⊢ ↑↑n✝ = ↑n✝

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : DivisionRing R
n✝ : ℤ
⊢ ↑↑n✝ = ↑n✝

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑n.succ
⊢ (↑n.succ * ⅟↑d)⁻¹ = ↑d * ⅟↑n.succ

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑n.succ
⊢ (↑(Int.ofNat n.succ) * ⅟↑d)⁻¹ = ↑(Int.ofNat d) * ⅟↑n.succ

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
⊢ (↑1)⁻¹ = ↑1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
⊢ (↑0)⁻¹ = ↑0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
⊢ (↑(Int.negOfNat 1))⁻¹ = ↑(Int.negOfNat 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a : ℤ
⊢ (↑a)⁻¹.num = a.sign

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a : ℕ
⊢ (↑a)⁻¹.num = (↑a).sign

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

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

Tactic:
by 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:
by 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:
by 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:
by simp

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:
by 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:
by 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:
by 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:
by 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:
by simp

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

Goal state before:
pp: R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ b * a ≤ (b + c) * a

Tactic:
add_mul

Goal state after:
R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ b * a ≤ b * a + c * a
Module: Mathlib.Tactic.Ring.Common

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

Tactic:
by 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:
by simp

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

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

Tactic:
by 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:
by simp

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:
by simp

Goal state after:
Module: Mathlib.Data.ULift

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.ULift

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

Tactic:
by 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:
by 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:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by 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:
by 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:
by 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:
by simp

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:
by 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:
by 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:
by 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:
by 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:
by 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:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by 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:
by simp

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

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

Tactic:
contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim

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:
by simp

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
F : Type u_3
inst✝ : LE α
s t✝ : Flag α
a : α
t : Flag α
carrier✝ : Set α
Chain'✝ : IsChain (fun x1 x2 ↦ x1 ≤ x2) carrier✝
max_chain'✝ : ∀ ⦃s : Set α⦄, IsChain (fun x1 x2 ↦ x1 ≤ x2) s → carrier✝ ⊆ s → carrier✝ = s
h : { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ } = t

Tactic:
cases t

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
F : Type u_3
inst✝ : LE α
s t : Flag α
a : α
carrier✝¹ : Set α
Chain'✝¹ : IsChain (fun x1 x2 ↦ x1 ≤ x2) carrier✝¹
max_chain'✝¹ : ∀ ⦃s : Set α⦄, IsChain (fun x1 x2 ↦ x1 ≤ x2) s → carrier✝¹ ⊆ s → carrier✝¹ = s
carrier✝ : Set α
Chain'✝ : IsChain (fun x1 x2 ↦ x1 ≤ x2) carrier✝
max_chain'✝ : ∀ ⦃s : Set α⦄, IsChain (fun x1 x2 ↦ x1 ≤ x2) s → carrier✝ ⊆ s → carrier✝ = s
h :
  { carrier := carrier✝¹, Chain' := Chain'✝¹, max_chain' := max_chain'✝¹ }.carrier =
    { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ }.carrier
⊢ { carrier := carrier✝¹, Chain' := Chain'✝¹, max_chain' := max_chain'✝¹ } =
    { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ }
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:
by 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:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ b * a ≤ c * a

Tactic:
by
    rw [← le, mul, mul]; refine mul_le_mul_of_nonneg_right (le.2 hbc) ?_; rwa [← zero, le]

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:
by 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:
by 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:
by 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:
by simp

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

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_3
inst✝² : One M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
f : ι → M
x : ι
⊢ mulSupport (update f x 1) = if 1 = 1 then mulSupport f \ {x} else insert x (mulSupport f)

Tactic:
simp [mulSupport_update_one, mulSupport_update_of_ne_one, *]

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

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_3
inst✝² : One M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
f : ι → M
x : ι
y : M
hy : y ≠ 1
⊢ mulSupport (update f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)

Tactic:
simp [mulSupport_update_one, mulSupport_update_of_ne_one, *]

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:
by 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:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
hi : 3 ≤ n
⊢ n < n !

Tactic:
have : 0 < n := by lia
  have hn : 1 < pred n := le_pred_of_lt (succ_le_iff.mp hi)
  rw [← succ_pred_eq_of_pos ‹0 < n›, factorial_succ]
  exact (Nat.lt_mul_iff_one_lt_right (pred n).succ_pos).2
    ((Nat.lt_of_lt_of_le hn (self_le_factorial _)))

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

Goal state before:
pp: case succ
n m : ℕ
h : n ≤ m
k : ℕ
ih : n.ascFactorial k ≤ m.ascFactorial k
⊢ n.ascFactorial (k + 1) ≤ m.ascFactorial (k + 1)

Tactic:
| succ k ih =>

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2)

Tactic:
by
  rw [Nat.pow_succ, ascFactorial, Nat.mul_comm]
  exact Nat.mul_lt_mul_of_lt_of_le' (Nat.lt_add_of_pos_right k.succ_pos)
    (pow_succ_le_ascFactorial n.succ _) (Nat.pow_pos n.succ_pos)

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

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

Tactic:
by simp

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

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

Tactic:
by simp

Goal state after: