mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ.succ.refine_1
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ (scanl f (f b v.head) v.tail).get 0 =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get (Fin.castSucc 0)) ((v.head ::ᵥ v.tail).get 0)

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 : α
s : Sym α 1
l : { x // x.length = 1 }
⊢ 0 < (↑l).length

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : Bool → α
⊢ ∏ b, f b = f true * f false

Tactic:
simp

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

Goal state before:
pp: m : Type u_6 → Type u_7
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ (do
      let a ← pure (f 0)
      let v ← pure (ofFn fun i ↦ f i.succ)
      pure (a ::ᵥ v)) =
    pure (ofFn f)

Tactic:
ofFn

Goal state after:
m : Type u_6 → Type u_7
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ (do
      let a ← pure (f 0)
      let v ← pure (ofFn fun i ↦ f i.succ)
      pure (a ::ᵥ v)) =
    pure (f 0 ::ᵥ ofFn fun i ↦ f i.succ)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: m : Type u_6 → Type u_7
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ (do
      let a ← pure (f 0)
      let v ← pure (ofFn fun i ↦ f i.succ)
      pure (a ::ᵥ v)) =
    pure (f 0 ::ᵥ ofFn fun i ↦ f i.succ)

Tactic:
simp

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

Goal state before:
pp: α : Type u_7
s : Finset α
n : ℕ
⊢ #(piFinset fun x ↦ s) = #s ^ n

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ filter (fun x ↦ a ≠ x) ↑m + ↑(replicate (count a ↑m) a) = ↑m

Tactic:
ext b

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x ↦ a ≠ x) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card (α → β) = card β ^ card α

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n : ℕ
⊢ Fintype.card (Fin n → α) = Fintype.card α ^ n

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := mem_filter.mp ha
⊢ (fun j ↦ a.get ⟨↑j, ⋯⟩) ∈ univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := mem_filter.mp ha
⊢ ∀ (n : ℕ) (h₁ : n < (List.ofFn fun j ↦ a.get ⟨↑j, ⋯⟩).length) (h₂ : n < a.length),
    (List.ofFn fun j ↦ a.get ⟨↑j, ⋯⟩).get ⟨n, h₁⟩ = a.get ⟨n, h₂⟩

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n
⊢ encode (decode (Sum.inl s)) = Sum.inl s

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Unique α
u : List α
⊢ ((fun n ↦ replicate n default) u.length).length = u.length

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (x : ℕ), x < n ↔ x ∈ range n

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (x : Fin n), f ↑x = f ↑((equivSubtype.trans (Equiv.subtypeEquivRight ⋯)) x)

Tactic:
simp

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

Goal state before:
pp: case neg.refine_1
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map some (map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach) = map Subtype.val (decode (Sum.inr s)).attach

Tactic:
simp

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

Goal state before:
pp: case neg.refine_2
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ decode (Sum.inr s) = map some s

Tactic:
simp

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

Goal state before:
pp: α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
val : ↑s
⊢ (match some val with
    | some y => ↑y
    | none => default) ∈
    insert default s

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), x ∈ {x | p x} ↔ p x

Tactic:
simp

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

Goal state before:
pp: case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x, f ↑x ⋯ = ∏ a, f ↑a ⋯

pp: case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x, g ↑x ⋯ = ∏ a, g ↑a ⋯

Tactic:
· exact (Equiv.subtypeEquivRight <| by simp).prod_comp fun x : { x // p x } => f x x.2

Goal state after:
case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x, g ↑x ⋯ = ∏ a, g ↑a ⋯
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), x ∈ {x | ¬p x} ↔ ¬p x

Tactic:
simp

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

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

Tactic:
· dsimp
      rw [← List.insertIdx_eraseIdx_of_le]
      · rfl
      · simpa
      · simpa [not_lt] using hij

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 : ℕ
β : Type u_6
γ : Type u_7
v : Vector α n
i : Fin n
a : α
⊢ ((↑v).set (↑i) a).length = n

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inl.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r a x
b : α
hb : r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inl ⟨a, ha⟩) (Sum.inl ⟨b, hb⟩)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inr.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : ¬r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inr ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inl.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r x a
b : α
hb : ¬r x b
⊢ r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inl ⟨a, ha⟩))
      (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inl ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) (Sum.inl ⟨a, ha⟩) (Sum.inl ⟨b, hb⟩)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inr.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r x a
b : α
hb : r x b
⊢ r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨a, ha⟩))
      (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) (Sum.inr ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y x✝ : α
⊢ x✝ ∈ Ici x ↔ x✝ ∈ {y | ¬y < x}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y x✝ : α
⊢ x✝ ∈ Iic x ↔ x✝ ∈ {y | ¬x < y}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : Preorder β
inst✝ : Unique β
x : α
⊢ (fun x ↦ (ofLex x).1) ((fun x ↦ toLex (x, default)) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : Unique α
inst✝ : LE β
x : β
⊢ (fun x ↦ (ofLex x).2) ((fun x ↦ toLex (default, x)) x) = x

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
h : IsSuccPrelimit ⊥
⊢ sSup (Iio ⊥) = ⊥

Tactic:
simp

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

Goal state before:
pp: α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
e₁ : α₁ ≃o β₁
e₂ : α₂ ≃o β₂
f₁ : β₁ ≃o γ₁
f₂ : β₂ ≃o γ₂
x✝ : α₁ ⊕ α₂
⊢ ((e₁.sumCongr e₂).trans (f₁.sumCongr f₂)) x✝ = ((e₁.trans f₁).sumCongr (e₂.trans f₂)) x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : LE β
x✝ : α ⊕ β
⊢ ((refl α).sumCongr (refl β)) x✝ = (refl (α ⊕ β)) x✝

Tactic:
simp

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

Goal state before:
pp: α✝ β : Type u
α : Type v
⊢ #(Quotient.out #α) = #α

Tactic:
simp

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

Goal state before:
pp: ι : Type u
a : Cardinal.{u}
⊢ (sum fun x ↦ a) = #ι * a

Tactic:
simp

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Defs

Goal state before:
pp: α : Type u_1
f g : α → α
x : α
hf : f x = x
hg : g x = x
⊢ f x = x

Tactic:
hf

Goal state after:
α : Type u_1
f g : α → α
x : α
hf : f x = x
hg : g x = x
⊢ x = x
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≃r s
⊢ ∀ (a : α) (b : β), s b (f.toRelEmbedding a) → b ∈ Set.range ⇑f.toRelEmbedding

Tactic:
simp

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

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁸ : LE α
inst✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a✝ : α
b✝ : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a b : α₁
⊢ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inl a)) ≤
      (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inl b)) ↔
    toLex (inl a) ≤ toLex (inl b)

Tactic:
simp

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

Goal state before:
pp: case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁸ : LE α
inst✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a✝ : α
b✝ : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a : α₁
b : β₁
⊢ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inl a)) ≤
      (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inr b)) ↔
    toLex (inl a) ≤ toLex (inr b)

Tactic:
simp

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁸ : LE α
inst✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a✝ : α
b✝ : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a : β₁
b : α₁
⊢ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inr a)) ≤
      (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inl b)) ↔
    toLex (inr a) ≤ toLex (inl b)

Tactic:
simp

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁸ : LE α
inst✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a✝ : α
b✝ : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a b : β₁
⊢ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inr a)) ≤
      (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inr b)) ↔
    toLex (inr a) ≤ toLex (inr b)

Tactic:
simp

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

Goal state before:
pp: α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
e₁ : α₁ ≃o β₁
e₂ : α₂ ≃o β₂
f₁ : β₁ ≃o γ₁
f₂ : β₂ ≃o γ₂
x✝ : α₁ ⊕ₗ α₂
⊢ ((e₁.sumLexCongr e₂).trans (f₁.sumLexCongr f₂)) x✝ = ((e₁.trans f₁).sumLexCongr (e₂.trans f₂)) x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : LE β
x✝ : α ⊕ₗ β
⊢ ((refl α).sumLexCongr (refl β)) x✝ = (refl (α ⊕ₗ β)) x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
⊢ s.Nonempty → ¬BddAbove s

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

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
⊢ False
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
h : b ≤ f a
c : α
hc : f c = b
⊢ ∃ c ≤ a, f c = b

Tactic:
refine ⟨c, ?_, hc⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
h : b ≤ f a
c : α
hc : f c = b
⊢ c ≤ a
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
h : b < f a
c : α
hc : f c = b
⊢ ∃ a' < a, f a' = b

Tactic:
refine ⟨c, ?_, hc⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
h : b < f a
c : α
hc : f c = b
⊢ c < a
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ ∀ (a b : α), a ≤ b → {a, b} ∈ univ

Tactic:
simp

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: β : Type u_2
inst✝ : SemilatticeSup β
d : Set (β × β)
x✝² : d.Nonempty
x✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : β × β
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
⊢ p₁ ⊔ p₂ ∈ {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} ∧
    p₁ ⊔ p₂ ∈ lowerBounds {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x}

Tactic:
have e1 : (p₁, p₂) ∈ lowerBounds {x | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x} := hdp.2

Goal state after:
β : Type u_2
inst✝ : SemilatticeSup β
d : Set (β × β)
x✝² : d.Nonempty
x✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : β × β
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
e1 : (p₁, p₂) ∈ lowerBounds {x | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x}
⊢ p₁ ⊔ p₂ ∈ {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} ∧
    p₁ ⊔ p₂ ∈ lowerBounds {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x}
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : β
⊢ ¬a ∈ map f none

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
⊢ o.bind f = f (o.get h)

Tactic:
ext b

Goal state after:
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ b ∈ o.bind f ↔ b ∈ f (o.get h)
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Part β
a : β
⊢ ¬a ∈ none.bind f

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → Part β
⊢ ∀ (a_1 : β), a_1 ∈ (some a).bind f ↔ a_1 ∈ f a

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : o.Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a ↦ (f a).toOption

pp: case neg
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : ¬o.Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a ↦ (f a).toOption

Tactic:
· simp_rw [h.toOption, h.bind]
    rfl

Goal state after:
case neg
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : ¬o.Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a ↦ (f a).toOption
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ (x.bind fun x ↦ (some (f x)).bind g) = x.bind fun y ↦ g (f y)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
c : Chain α
x✝ : ℕ
⊢ (c.map OrderHom.id) x✝ = c x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
c : Chain α
hf : ωScottContinuous f
⊢ Set.range ⇑c ∈ Set.range fun c ↦ Set.range ⇑c

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma \ mb ∈ a \ b

Tactic:
simp [sdiff_def]

Goal state after:
α : Type u_1
inst✝ : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 \ a = ma \ mb
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ (a \ b).get hab = a.get ⋯ \ b.get ⋯

Tactic:
simp [sdiff_def]

Goal state after:
α : Type u_1
inst✝ : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ (a.bind fun y ↦ map (fun x ↦ y \ x) b).get ⋯ = a.get ⋯ \ b.get ⋯
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : SDiff α
a b : α
⊢ some a \ some b = some (a \ b)

Tactic:
simp [sdiff_def]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case inl
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hij : i ≤ j
⊢ a = b

Tactic:
have := c.monotone hij _ ha

Goal state after:
case inl
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hij : i ≤ j
this : a ∈ c.toOrderHom j
⊢ a = b
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), c i ≤ x
a : α
i : ℕ
ha : some a = c i
⊢ a ∈ c i

Tactic:
rw [← ha]

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), c i ≤ x
a : α
i : ℕ
ha : some a = c i
⊢ a ∈ some 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
hh : some (Classical.choose h') ∈ c
⊢ x ∈ some x

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : IsEmpty β
this : IsEmpty α
⊢ ∀ (a : α), R a (((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm) a)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
c : Chain α
a : β
⊢ ⊤ (ωSup c) ≤ a ↔ ωSup (c.map { toFun := ⊤, monotone' := ⋯ }) ≤ a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
⊢ ∀ f ∈ ∅, ωScottContinuous f

Tactic:
simp

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : 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 α
i : ℕ
⊢ ∀ (i_1 : ℕ),
    ((c.map { toFun := g, monotone' := ⋯ }).map ↑(f (c i))) i_1 ≤
      ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })

Tactic:
intro j

Goal state after:
case a
α : 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 α
i j : ℕ
⊢ ((c.map { toFun := g, monotone' := ⋯ }).map ↑(f (c i))) j ≤
    ω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:
← lift_lift.{v, w, u},

Goal state after:
a : Cardinal.{u}
b : Cardinal.{v}
⊢ lift.{w, max v u} (lift.{v, u} a) = lift.{max u w, v} b ↔ lift.{v, u} a = lift.{u, v} b
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α : Type u
h : Fintype α
⊢ Fintype.card α = Fintype.card (ULift.{u, 0} (Fin (Fintype.card α)))

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ #(ULift.{u, 0} (Fin (n + 1))) = #(Option (ULift.{u, 0} (Fin n)))

Tactic:
simp

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

Goal state before:
pp: ⊢ #Bool = 2

Tactic:
simp

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

Goal state before:
pp: ⊢ #Prop = 2

Tactic:
simp

Goal state after: