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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
i : Fin n✝.succ
⊢ (map₂ f (a✝ ::ᵥ x✝) (b✝ ::ᵥ y✝)).get i = f ((a✝ ::ᵥ x✝).get i) ((b✝ ::ᵥ y✝).get i)

Tactic:
map₂_cons

Goal state after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
i : Fin n✝.succ
⊢ (f a✝ b✝ ::ᵥ map₂ f x✝ y✝).get i = f ((a✝ ::ᵥ x✝).get i) ((b✝ ::ᵥ y✝).get i)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
i : Fin n✝.succ
⊢ (f a✝ b✝ ::ᵥ map₂ f x✝ y✝).get i = f ((a✝ ::ᵥ x✝).get i) ((b✝ ::ᵥ y✝).get i)

Tactic:
]

Goal state after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
i : Fin n✝.succ
⊢ (f a✝ b✝ ::ᵥ map₂ f x✝ y✝).get i = f ((a✝ ::ᵥ x✝).get i) ((b✝ ::ᵥ y✝).get i)
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
a✝ c✝ : α
hab : r a✝ c✝
hba : r c✝ a✝
⊢ inl c✝ = inl c✝

Tactic:
]

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
b✝ d✝ : β
hab : s b✝ d✝
hba : s d✝ b✝
⊢ inr d✝ = inr d✝

Tactic:
]

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

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
a₁✝ a₂✝ : α
hab : r a₁✝ a₂✝
hba : r a₂✝ a₁✝
⊢ inl a₂✝ = inl a₂✝

Tactic:
]

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
b₁✝ b₂✝ : β
hab : s b₁✝ b₂✝
hba : s b₂✝ b₁✝
⊢ inr b₂✝ = inr b₂✝

Tactic:
]

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

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

Tactic:
rintro ⟨⟨hab⟩ | ⟨hab⟩, hba⟩
        · exact LiftRel.inl (hab.lt_of_not_ge fun h => hba <| LiftRel.inl h)
        · exact LiftRel.inr (hab.lt_of_not_ge fun h => hba <| LiftRel.inr h)

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : y < x
⊢ y = ↑⟨y, h⟩

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x ≤ y
⊢ y = ↑⟨y, h⟩

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : y ≤ x
⊢ y = ↑⟨y, h⟩

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x < y
⊢ y = ↑⟨y, h⟩

Tactic:
]

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 : IsMin (sSup s) ∨ ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : IsMin (sSup s) ∨ ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hmin : IsMin (sSup s)
a : α
has : a ∈ s
⊢ a ∈ s

Tactic:
]

Goal state after:
case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hmin : IsMin (sSup s)
a : α
has : a ∈ s
⊢ a ∈ s
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
hlim : ¬BddAbove s
⊢ IsSuccPrelimit ⊥

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
hlim : ¬BddAbove s
⊢ IsSuccPrelimit ⊥
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
hx : ¬IsSuccPrelimit (sSup (Iio x))
⊢ False
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
⊢ IsSuccPrelimit x ↔ IsSuccPrelimit x

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
⊢ ∀ (i : ↑(Iio x)), succ ↑i ≤ x

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
⊢ ∀ (i : ↑(Iio x)), succ ↑i ≤ x
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
y : α
hy : y < x
⊢ ∃ i, y < succ ↑i

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
y : α
hy : y < x
⊢ ∃ i, y < succ ↑i
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: a : Cardinal.{u}
⊢ Nonempty (Quotient.out #(ULift (Quotient.out a)) ≃ Quotient.out a)

Tactic:
]

Goal state after:
a : Cardinal.{u}
⊢ Nonempty (Quotient.out #(ULift (Quotient.out a)) ≃ Quotient.out a)
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: x : Cardinal.{u_1}
h : x ≠ 0
⊢ x ≠ 0

Tactic:
]

Goal state after:
x : Cardinal.{u_1}
h : x ≠ 0
⊢ x ≠ 0
Module: Mathlib.SetTheory.Cardinal.Defs

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

Tactic:
]

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
a : ι
⊢ lift.{max v w, v} (f a) = lift.{max w v, v} (f a)

Tactic:
]

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 ∘ g) x = x

Tactic:
]

Goal state after:
α : Type u_1
f g : α → α
x : α
hf : f x = x
hg : g x = x
⊢ (f ∘ g) x = x
Module: Mathlib.Dynamics.FixedPoints.Defs

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

Tactic:
]

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

Goal state after:
α : Type u_1
f : α → α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f)^[n] s
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : Set α
h : IsUpperSet sᶜ
⊢ s = s

Tactic:
]

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
inst✝² : Std.Trichotomous s
inst✝¹ : Std.Irrefl s
inst✝ : IsWellFounded α r
f g : r ≼i s
a b : α
IH : ∀ (y : α), r y b → f y = g y
x : β
⊢ (∃ a', f a' = x ∧ r a' b) ↔ ∃ a', g a' = x ∧ r a' b

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝² : Std.Trichotomous s
inst✝¹ : Std.Irrefl s
inst✝ : IsWellFounded α r
f g : r ≼i s
a b : α
IH : ∀ (y : α), r y b → f y = g y
x : β
⊢ (∃ a', f a' = x ∧ r a' b) ↔ ∃ a', g a' = x ∧ r a' b
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (⇑(↑f).symm ⁻¹' s)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (⇑(↑f).symm ⁻¹' s)
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f g : r ≼i s
a : α
⊢ g a = g a

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : IsUpperSet (range ⇑e)
a : α
⊢ Ici (e a) = Ici (e a)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : IsUpperSet (range ⇑e)
a : α
⊢ Ioi (e a) = Ioi (e a)

Tactic:
]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case e_top
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f : r ↪r s
a : β
hf : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b a
b : β
hg : ∀ (b_1 : β), b_1 ∈ Set.range ⇑{ toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding ↔ s b_1 b
x : β
⊢ s x b ↔ s x b

Tactic:
]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f g : r ≺i s
h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
⊢ f.toRelEmbedding = g.toRelEmbedding

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f g : r ≺i s
h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
⊢ f.toRelEmbedding = g.toRelEmbedding
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r f.top f.top
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r f.top f.top
⊢ False
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f g : r ≺i s
a : α
⊢ g.toRelEmbedding a = g.toRelEmbedding a

Tactic:
]

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
inst✝ : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ (relIsoTrans e g).top = g.top

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ (relIsoTrans e g).top = g.top
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
f : r ≺i s
g : s ≺i t
h : r ≺i t
⊢ t (f.trans g).top g.top

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
f : r ≺i s
g : s ≺i t
h : r ≺i t
⊢ t (f.trans g).top g.top
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ (match f.principalSumRelIso with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ (match f.principalSumRelIso with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≺i s
⊢ g.toRelEmbedding (f a) = g.toRelEmbedding (f a)

Tactic:
]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≃r s
⊢ g.toRelEmbedding (f a) = g.toRelEmbedding (f a)

Tactic:
]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(have H := ⋯;
      ⟨⋯.min
          {b |
            ∀ (a_1 : α) (h : r a_1 a),
              s
                (↑((fun y x ↦
                      IsWellFounded.fix r
                        (fun a IH ↦
                          have H := ⋯;
                          ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                        y)
                    a_1 h))
                b}
          ⋯,
        ⋯⟩) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(IsWellFounded.fix r
                (fun a IH ↦
                  have H := ⋯;
                  ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩)
                a'))
            b}

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(have H := ⋯;
      ⟨⋯.min
          {b |
            ∀ (a_1 : α) (h : r a_1 a),
              s
                (↑((fun y x ↦
                      IsWellFounded.fix r
                        (fun a IH ↦
                          have H := ⋯;
                          ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                        y)
                    a_1 h))
                b}
          ⋯,
        ⋯⟩) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(IsWellFounded.fix r
                (fun a IH ↦
                  have H := ⋯;
                  ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩)
                a'))
            b}
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      ↑(have H := ⋯;
        ⟨⋯.min
            {b |
              ∀ (a_1 : α) (h : r a_1 a),
                s
                  (↑((fun y x ↦
                        IsWellFounded.fix r
                          (fun a IH ↦
                            have H := ⋯;
                            ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                          y)
                      a_1 h))
                  b}
            ⋯,
          ⋯⟩)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      ↑(have H := ⋯;
        ⟨⋯.min
            {b |
              ∀ (a_1 : α) (h : r a_1 a),
                s
                  (↑((fun y x ↦
                        IsWellFounded.fix r
                          (fun a IH ↦
                            have H := ⋯;
                            ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                          y)
                      a_1 h))
                  b}
            ⋯,
          ⋯⟩)
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f✝ : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : f✝.top = g.top
f : (Subrel (Sum.Lex r s) fun x ↦ Sum.Lex r s x g.top) ≃r r
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
]

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f✝ : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : f✝.top = g.top
f : (Subrel (Sum.Lex r s) fun x ↦ Sum.Lex r s x g.top) ≃r r
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : α ≤i β
h : IsMin a
x : α
hb : x ≤ a
⊢ a ≤ x

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : α ≤i β
h : IsMin a
x : α
hb : x ≤ a
⊢ a ≤ x
Module: Mathlib.Order.InitialSeg

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

Tactic:
]

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
c : α
h : c ≤ a
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 β
c : α
h : c < a
hc : f c = b
⊢ c < a

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLeast (Ici b) b

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLeast (Ici b) b
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
⊢ d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (g ∘ f '' d) ((g ∘ f) a)

Tactic:
hd₁

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
⊢ d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (g ∘ f '' d) ((g ∘ f) a)
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' d)
⊢ IsLUB (g '' f '' d) ((g ∘ f) a)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' d)
⊢ IsLUB (g '' f '' d) ((g ∘ f) a)
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ (fun x ↦ (f x, g x)) a ∈ {x | ∀ ⦃a : β × γ⦄, a ∈ (fun x ↦ (f x, g x)) '' d → a ≤ x} ∧
    (fun x ↦ (f x, g x)) a ∈ lowerBounds {x | ∀ ⦃a : β × γ⦄, a ∈ (fun x ↦ (f x, g x)) '' d → a ≤ x}

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ (fun x ↦ (f x, g x)) a ∈ {x | ∀ ⦃a : β × γ⦄, a ∈ (fun x ↦ (f x, g x)) '' d → a ≤ x} ∧
    (fun x ↦ (f x, g x)) a ∈ lowerBounds {x | ∀ ⦃a : β × γ⦄, a ∈ (fun x ↦ (f x, g x)) '' d → a ≤ x}
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
a₁ a₂ : α
⊢ (⇑f)^[n.succ] a₁ ⊔ a₂ = (⇑f)^[n + 1] a₁ ⊔ a₂

Tactic:
]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case right.left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ (p₁, p₂).1 ∈ {x | ∀ ⦃a : β⦄, a ∈ f '' d → a ≤ x}

Tactic:
]

Goal state after:
case right.left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ (p₁, p₂).1 ∈ {x | ∀ ⦃a : β⦄, a ∈ f '' d → a ≤ x}
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
⊢ (⇑f)^[n₁] ((⇑f)^[n₂] (a₂ ⊔ a₁)) = (⇑f)^[n₁] ((⇑f)^[n₂] (a₂ ⊔ a₁))

Tactic:
]

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

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
⊢ (⇑f)^[n₁] (a₁ ⊔ (⇑f)^[n₂] a₂) = (⇑f)^[n₁] (a₁ ⊔ (⇑f)^[n₂] a₂)

Tactic:
]

Goal state after: