mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s t : Set α
⊢ (s ∪ t).Countable ↔ s.Countable ∧ t.Countable

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
a : α
⊢ (insert a s).Countable ↔ s.Countable

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
h : i ≠ j
a : α
⊢ (v.set i a).get j = v.get j

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Countable
⊢ {t | t.Finite ∧ t ⊆ s}.Countable

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Countable α
⊢ {s | s.Finite}.Countable

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
⊢ (v.set i a).get j = if i = j then a else v.get j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).toList.prod = (take (↑i) v).toList.prod * a * (drop (↑i + 1) v).toList.prod

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
inst✝ : Countable β
h : ∀ (b : β), (f ⁻¹' {b}).Countable
⊢ Countable α

Tactic:
by

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

Goal state before:
pp: α : Type u
π : α → Type u_1
inst✝ : Finite α
s : (a : α) → Set (π a)
hs : ∀ (a : α), (s a).Countable
⊢ {f | ∀ (a : α), f a ∈ s a}.Countable

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a

Tactic:
by

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 : ℕ
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
f : α → F β
v : List α
Hv : v.length = n
⊢ F (Vector β v.length) = F (Vector β n)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Set α
t : Set β
hs : s.Countable
ht : t.Countable
f : α → β → γ
⊢ (Set.image2 f s t).Countable

Tactic:
by

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

Goal state before:
pp: n : ℕ
F : Type u → Type u
inst✝ : Applicative F
α β : Type u
f : α → F β
x : α
⊢ ∀ (xs : Vector α n), Vector.traverse f (x ::ᵥ xs) = cons <$> f x <*> Vector.traverse f xs

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u
⊢ ∀ (x : Vector α n), Vector.traverse pure x = pure x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
⊢ ∀ (t : { t // (f t).Nonempty }), ∃ x, ↑x ∈ f ↑t

Tactic:
by

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

Goal state before:
pp: n : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : Vector α n
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) x = Comp.mk (Vector.traverse f <$> Vector.traverse g x)

Tactic:
by

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

Goal state before:
pp: n : ℕ
α β : Type u_6
f : α → β
⊢ ∀ (x : Vector α n), Vector.traverse (pure ∘ f) x = pure (map f x)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
⊢ (f t ∩ f t').Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
⊢ Injective F

Tactic:
by

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

Goal state before:
pp: n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
x : Vector α n
⊢ (fun {α} ↦ η.app α) (Vector.traverse f x) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) x

Tactic:
by

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} (x : flip Vector n α), id <$> x = x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : s.Countable
⊢ {t | (f t).Nonempty}.Countable

Tactic:
by

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} (g : α → β) (h : β → γ) (x : flip Vector n α), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
xs : Vector α n
⊢ xs ++ nil = xs

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
v₁ : Vector α n
v₂ : Vector β n
f : α → β → γ
i : Fin n
⊢ (map₂ f v₁ v₂).get i = f (v₁.get i) (v₂.get i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
⊢ ∀ (a : α ⊕ β), ¬LiftRel r s a a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
⊢ ∀ (a b : α ⊕ β), LiftRel r s a b → LiftRel r s b a → a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Refl r
inst✝ : Std.Refl s
⊢ ∀ (a : α ⊕ β), Lex r s a a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
⊢ ∀ (a : α ⊕ β), ¬Lex r s a a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
⊢ ∀ {a b : { x_1 // r x_1 x } ⊕ { x_1 // ¬r x_1 x }},
    r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) a) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) b) ↔
      Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
⊢ ∀ (a b c : α ⊕ β), Lex r s a b → Lex r s b c → Lex r s a c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
⊢ ∀ (a b : α ⊕ β), Lex r s a b → Lex r s b a → a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
⊢ Std.Trichotomous (Lex r s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ β
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : y < x
⊢ (sumLexIioIci x).symm y = toLex (Sum.inl ⟨y, h⟩)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x ≤ y
⊢ (sumLexIioIci x).symm y = toLex (Sum.inr ⟨y, h⟩)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : α
⊢ ∃ b, b < a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : y ≤ x
⊢ (sumLexIicIoi x).symm y = toLex (Sum.inl ⟨y, h⟩)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : β
⊢ ∃ b, b < a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x < y
⊢ (sumLexIicIoi x).symm y = toLex (Sum.inr ⟨y, h⟩)

Tactic:
by

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 : Lex (α × β)
x✝ : α × β
a : α
b : β
⊢ (fun x ↦ toLex (x, default)) ((fun x ↦ (ofLex x).1) (toLex (a, b))) = toLex (a, b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : α
⊢ ∃ b, a < b

Tactic:
by

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

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 β
a✝ b✝ : Lex (α × β)
a b : α × β
⊢ { toFun := fun x ↦ (ofLex x).1, invFun := fun x ↦ toLex (x, default), left_inv := ⋯, right_inv := ⋯ } (toLex a) ≤
      { toFun := fun x ↦ (ofLex x).1, invFun := fun x ↦ toLex (x, default), left_inv := ⋯, right_inv := ⋯ } (toLex b) ↔
    toLex a ≤ toLex b

Tactic:
simpa [Prod.Lex.toLex_le_toLex] using le_iff_lt_or_eq

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 β
a✝ b✝ : Lex (α × β)
a b : α × β
⊢ { toFun := fun x ↦ (ofLex x).1, invFun := fun x ↦ toLex (x, default), left_inv := ⋯, right_inv := ⋯ } (toLex a) ≤
      { toFun := fun x ↦ (ofLex x).1, invFun := fun x ↦ toLex (x, default), left_inv := ⋯, right_inv := ⋯ } (toLex b) ↔
    toLex a ≤ toLex b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : β
⊢ ∃ b, a < b

Tactic:
by

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 : Lex (α × β)
x✝ : α × β
a : α
b : β
⊢ (fun x ↦ toLex (default, x)) ((fun x ↦ (ofLex x).2) (toLex (a, b))) = toLex (a, b)

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
by

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 β
a✝ b✝ : Lex (α × β)
a b : α × β
⊢ { toFun := fun x ↦ (ofLex x).2, invFun := fun x ↦ toLex (default, x), left_inv := ⋯, right_inv := ⋯ } (toLex a) ≤
      { toFun := fun x ↦ (ofLex x).2, invFun := fun x ↦ toLex (default, x), left_inv := ⋯, right_inv := ⋯ } (toLex b) ↔
    toLex a ≤ toLex b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
by

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

Goal state before:
pp: α✝¹ : Type u_1
α✝ : Type u_2
β✝ : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
⊢ ∀ {a b : Lex (Lex (α × β) × γ)},
    (ofLex.trans
            ((ofLex.prodCongr (Equiv.refl γ)).trans
              ((Equiv.prodAssoc α β γ).trans (((Equiv.refl α).prodCongr toLex).trans toLex))))
          a ≤
        (ofLex.trans
            ((ofLex.prodCongr (Equiv.refl γ)).trans
              ((Equiv.prodAssoc α β γ).trans (((Equiv.refl α).prodCongr toLex).trans toLex))))
          b ↔
      a ≤ b

Tactic:
by

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

Goal state before:
pp: α✝¹ : Type u_1
α✝ : Type u_2
β✝ : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
⊢ ∀ {a b : Lex ((α ⊕ₗ β) × γ)},
    (ofLex.trans
            ((ofLex.prodCongr (Equiv.refl γ)).trans
              ((Equiv.sumProdDistrib α β γ).trans ((toLex.sumCongr toLex).trans toLex))))
          a ≤
        (ofLex.trans
            ((ofLex.prodCongr (Equiv.refl γ)).trans
              ((Equiv.sumProdDistrib α β γ).trans ((toLex.sumCongr toLex).trans toLex))))
          b ↔
      a ≤ b

Tactic:
by

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

Goal state before:
pp: α✝¹ : Type u_1
α✝ : Type u_2
β✝ : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
δ : Type u_7
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
ea : α ≃o β
eb : γ ≃o δ
⊢ ∀ {a b : Lex (α × γ)},
    (ofLex.trans (((↑ea).prodCongr ↑eb).trans toLex)) a ≤ (ofLex.trans (((↑ea).prodCongr ↑eb).trans toLex)) b ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ₗ β
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
⊢ ∀ (a : α ⊕ₗ β), inl ⊥ ≤ a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccLimit (sSup s)
⊢ sSup s ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
⊢ ∀ (a : α ⊕ₗ β), a ≤ inr ⊤

Tactic:
by

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

Goal state before:
pp: α : 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 : α₁ ⊕ β₁}, ((↑ea).sumCongr ↑eb) a ≤ ((↑ea).sumCongr ↑eb) b ↔ a ≤ b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
⊢ ⨆ a, ↑a = x

Tactic:
by

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 γ₂
⊢ (e₁.sumCongr e₂).trans (f₁.sumCongr f₂) = (e₁.trans f₁).sumCongr (e₂.trans f₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
⊢ sSup (Iio x) = x ↔ IsSuccPrelimit x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
⊢ ⨆ a, ↑a = x ↔ IsSuccPrelimit x

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
⊢ succ x ∈ upperBounds (range fun a ↦ succ ↑a)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
⊢ ⨆ a, succ ↑a = x

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
⊢ sInf s ∈ s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
⊢ Nonempty (Quotient.out (lift.{v, u} a) ≃ Quotient.out a)

Tactic:
by

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

Goal state before:
pp: x : Cardinal.{u_1}
h : x ≠ 0
⊢ Nonempty (Quotient.out x)

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ #(Option α) = #α + 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
a : ι
⊢ Nonempty (Quotient.out (f a) ≃ Quotient.out ((fun i ↦ lift.{w, v} (f i)) a))

Tactic:
by

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

Goal state before:
pp: f : ℕ → Cardinal.{u}
⊢ sum f = f 0 + sum fun i ↦ f (i + 1)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
f : ι → Cardinal.{u}
⊢ prod f = 0 ↔ ∃ i, f i = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
f : ι → Cardinal.{u_2}
⊢ prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0

Tactic:
by

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

Goal state before:
pp: ι : Type u
a : Cardinal.{v}
f : ι → Cardinal.{v}
⊢ lift.{u, v} a ^ sum f = prod fun i ↦ a ^ f i

Tactic:
by

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

Goal state before:
pp: ι : Type u
a : Cardinal.{max u v}
f : ι → Cardinal.{max u v}
⊢ a ^ sum f = prod fun i ↦ a ^ f i

Tactic:
by

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

Goal state before:
pp: ι : Type u
c : ι → Cardinal.{v}
⊢ lift.{w, max v u} (prod c) = prod fun i ↦ lift.{w, v} (c i)

Tactic:
by

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

Goal state before:
pp: α✝ : 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 : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
a b : (α ⊕ β) ⊕ γ
⊢ (Equiv.sumAssoc α β γ) a ≤ (Equiv.sumAssoc α β γ) b ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x✝ : α
⊢ x✝ ∈ fixedPoints id ↔ x✝ ∈ Set.univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f g : α → α
⊢ fixedPoints f ∩ fixedPoints g ⊆ fixedPoints (f ∘ g)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
hx : IsFixedPt f x
⊢ IsFixedPt f (f x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f^[n]) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
e : Perm α
⊢ fixedPoints ⇑(Equiv.symm e) = fixedPoints ⇑e

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.InvOn f g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.BijOn f (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.BijOn g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
by

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

Goal state before:
pp: α✝ : 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
⊢ ∀ {a b : (α ⊕ β)ᵒᵈ}, (Equiv.refl (α ⊕ β)ᵒᵈ) a ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ Injective fun f ↦ f.toFun

Tactic:
by

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a : α
b : β
h : s b (f a)
⊢ ∃ a', f a' = b ∧ r a' a

Tactic:
by

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

Goal state after:
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 ≼i s
g : s ≼i t
a : α
c : γ
h : t c ((f.trans g.toRelEmbedding) a)
⊢ c ∈ Set.range ⇑(f.trans g.toRelEmbedding)

Tactic:
by

Goal state after: