mathlib-initiative/mathlib-tactics huggingface dataset:
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:
constructor

Goal state after:
case 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
⊢ (fun x ↦ (f x, g x)) a ∈ {x | ∀ ⦃a : β × γ⦄, a ∈ (fun x ↦ (f x, g x)) '' d → a ≤ x}

case right
α : 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 ∈ lowerBounds {x | ∀ ⦃a : β × γ⦄, a ∈ (fun x ↦ (f x, g x)) '' d → a ≤ x}
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case right
α : 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₂
⊢ (fun x ↦ (f x, g x)) a ≤ (p₁, p₂)

Tactic:
constructor

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₂
⊢ ((fun x ↦ (f x, g x)) a).1 ≤ (p₁, p₂).1

case right.right
α : 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₂
⊢ ((fun x ↦ (f x, g x)) a).2 ≤ (p₁, p₂).2
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Part α
⊢ o ≠ none ↔ ∃ x, o = some x

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
o : Part α
⊢ o ≠ none → ∃ x, o = some x

case mpr
α : Type u_1
o : Part α
⊢ (∃ x, o = some x) → o ≠ none
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
p : Prop
f : p → Part α
h : p
⊢ assert p f = f h

Tactic:
ext

Goal state after:
α : Type u_1
p : Prop
f : p → Part α
h : p
a✝ : α
⊢ a✝ ∈ assert p f ↔ a✝ ∈ f h
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ assert p f = none

Tactic:
ext

Goal state after:
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
a✝ : α
⊢ a✝ ∈ assert p f ↔ a✝ ∈ none
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsLeast (bot x f) x

Tactic:
constructor

Goal state after:
case left
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ bot x f

case right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ lowerBounds (bot x f)
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ IsLeast {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} x

Tactic:
constructor

Goal state after:
case base_isLeast.left
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ x ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}

case base_isLeast.right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ x ∈ lowerBounds {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast.left
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ x ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}

Tactic:
constructor

Goal state after:
case base_isLeast.left.left
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ x ∈ bot x f

case base_isLeast.left.right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ x ≤ y ∨ f y ≤ x
Module: Mathlib.Data.Part

Goal state before:
pp: β α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ x >>= f ≤ y ↔ ∀ (a : α), a ∈ x → f a ≤ y

Tactic:
constructor

Goal state after:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ x >>= f ≤ y → ∀ (a : α), a ∈ x → f a ≤ y

case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ (∀ (a : α), a ∈ x → f a ≤ y) → x >>= f ≤ y
Module: Mathlib.Order.OmegaCompletePartialOrder

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

Tactic:
ext

Goal state after:
α : Type u_2
inst✝ : Preorder α
c : Chain α
x✝ : ℕ
⊢ (c.map OrderHom.id) x✝ = c x✝
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a b : α
hab : a ≤ b
⊢ Set.range ⇑(pair a b hab) = {a, b}

Tactic:
ext

Goal state after:
α : Type u_2
inst✝ : Preorder α
a b : α
hab : a ≤ b
x✝ : α
⊢ x✝ ∈ Set.range ⇑(pair a b hab) ↔ x✝ ∈ {a, b}
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ h_1, o.get ⋯ = a) ↔ p ∧ ∃ h, o.get h = a

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ h_1, o.get ⋯ = a) → p ∧ ∃ h, o.get h = a

case mpr
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (p ∧ ∃ h, o.get h = a) → ∃ h_1, o.get ⋯ = a
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ ωSup c ≤ x ↔ ∀ (i : ℕ), c i ≤ x

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ ωSup c ≤ x → ∀ (i : ℕ), c i ≤ x

case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ (∀ (i : ℕ), c i ≤ x) → ωSup c ≤ x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ IsLUB (Set.range ⇑c) (ωSup c)

Tactic:
constructor

Goal state after:
case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ upperBounds (Set.range ⇑c)

case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ lowerBounds (upperBounds (Set.range ⇑c))
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ a ≤ ωSup c ∧ ωSup c ≤ a

Tactic:
constructor

Goal state after:
case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ a ≤ ωSup c

case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ωSup c ≤ a
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsLeast {y | IsExtremePt x f y} x

Tactic:
constructor

Goal state after:
case base_isLeast.left
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ {y | IsExtremePt x f y}

case base_isLeast.right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ lowerBounds {y | IsExtremePt x f y}
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
x : α
c : Chain (Part α)
⊢ (x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none) ↔ some x ∈ c

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
x : α
c : Chain (Part α)
⊢ (x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none) → some x ∈ c

case mpr
α : Type u_2
x : α
c : Chain (Part α)
⊢ some x ∈ c → x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : ChainCompletePartialOrder α
f : α → α
inst✝ : Nonempty α
le_map : ∀ (x : α), x ≤ f x
x : α := ⋯
y : α := ⋯
⊢ y ∈ fixedPoints f

Tactic:
apply le_antisymm (le_cSup _ _ (_ : f y ∈ bot x f)) (le_map y)

Goal state after:
α : Type u_1
inst✝¹ : ChainCompletePartialOrder α
f : α → α
inst✝ : Nonempty α
le_map : ∀ (x : α), x ≤ f x
x : α := ⋯
y : α := ⋯
⊢ f y ∈ bot x f
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ (∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x) ↔ ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ (∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x) → ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x

case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ (∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x) → ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (i j : ℕ), (c₀ i) (c₁ j) ≤ z) ↔ ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (i j : ℕ), (c₀ i) (c₁ j) ≤ z) → ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z

case mpr
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z) → ∀ (i j : ℕ), (c₀ i) (c₁ j) ≤ z
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α✝ β✝ : Type u
a b : Cardinal.{u}
α β : Type u
x✝ : #α ≤ #β
f : α → β
hf : Injective f
⊢ α ⊕ ↑(Set.range f)ᶜ ≃ β

Tactic:
classical
        exact (Equiv.sumCongr (Equiv.ofInjective f hf) (Equiv.refl _)).trans <|
          Equiv.Set.sumCompl (range f)

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β✝
inst✝¹ : OmegaCompletePartialOrder γ✝
inst✝ : OmegaCompletePartialOrder δ
β γ : Type v
f : α →𝒄 Part (β → γ)
g : α →𝒄 Part β
⊢ (fun x ↦ f x <*> g x) = ⇑(f.bind (flip (_root_.flip map g)))

Tactic:
ext

Goal state after:
ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β✝
inst✝¹ : OmegaCompletePartialOrder γ✝
inst✝ : OmegaCompletePartialOrder δ
β γ : Type v
f : α →𝒄 Part (β → γ)
g : α →𝒄 Part β
x✝ : α
a✝ : γ
⊢ a✝ ∈ f x✝ <*> g x✝ ↔ a✝ ∈ (f.bind (flip (_root_.flip map g))) x✝
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: m : ℕ∞
n : ℕ
⊢ ↑m < ↑n ↔ m < ↑n

Tactic:
by norm_cast

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

Goal state before:
pp: m : ℕ
n : ℕ∞
⊢ ↑m < ↑n ↔ ↑m < n

Tactic:
by norm_cast

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

Goal state before:
pp: m : ℕ∞
⊢ 0 < ↑m ↔ 0 < m

Tactic:
by norm_cast

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

Goal state before:
pp: m : ℕ∞
⊢ 1 < ↑m ↔ 1 < m

Tactic:
by norm_cast

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

Goal state before:
pp: m : ℕ∞
n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
by norm_cast

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

Goal state before:
pp: m : ℕ∞
⊢ ↑m ≤ 1 ↔ m ≤ 1

Tactic:
by norm_cast

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

Goal state before:
pp: m : ℕ
n : ℕ∞
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
by norm_cast

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

Goal state before:
pp: n : ℕ∞
⊢ 1 ≤ ↑n ↔ 1 ≤ n

Tactic:
by norm_cast

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

Goal state before:
pp: m : ℕ∞
n : ℕ
⊢ ↑m = ↑n ↔ m = ↑n

Tactic:
by norm_cast

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

Goal state before:
pp: m : ℕ
n : ℕ∞
⊢ ↑m = ↑n ↔ ↑m = n

Tactic:
by norm_cast

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

Goal state before:
pp: m : ℕ∞
⊢ ↑m = 0 ↔ m = 0

Tactic:
by norm_cast

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

Goal state before:
pp: m : ℕ∞
⊢ ↑m = 1 ↔ m = 1

Tactic:
by norm_cast

Goal state after:
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
σ : M →* M
h : _root_.CompTriple.IsId ⇑σ
⊢ σ = id M

Tactic:
ext

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
σ : M →* M
h : _root_.CompTriple.IsId ⇑σ
x✝ : M
⊢ σ x✝ = (id M) x✝
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃ ↔ φ₁₂.CompTriple φ₃ φ₁₂₃

Tactic:
constructor

Goal state after:
case mp
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃ → φ₁₂.CompTriple φ₃ φ₁₂₃

case mpr
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁₂.CompTriple φ₃ φ₁₂₃ → φ₁.CompTriple φ₂₃ φ₁₂₃
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ Nonempty (↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s)

Tactic:
constructor

Goal state after:
α : Type u
s : Set α
⊢ ↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_1
α : Type u
h : Fintype α
⊢ ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β),
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

Tactic:
intro α β hβ e h f

Goal state after:
case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : β → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i, f i)
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ n)

Tactic:
by
  induction n with
  | zero => rw [pow_zero]; simp only [one]
  | succ n hn =>
    rw [pow_succ']
    exact (ra.smul_iff (a ^ n)).mpr hn

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

Goal state before:
pp: s : Set Cardinal.{u}
⊢ Small.{u, u + 1} ↑s → BddAbove s

Tactic:
rintro ⟨ι, ⟨e⟩⟩
    use sum.{u, u} fun x ↦ e.symm x
    intro a ha
    simpa using le_sum (fun x ↦ e.symm x) (e ⟨a, ha⟩)

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

Goal state before:
pp: ⊢ succ 0 = 1

Tactic:
by norm_cast

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

Goal state before:
pp: ⊢ 1 < 2

Tactic:
by norm_cast

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

Goal state before:
pp: a b : Cardinal.{u_1}
hb : succ 1 ≤ b
⊢ succ 1 = 2

Tactic:
by norm_cast

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

Goal state before:
pp: case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀ ∧ b < ℵ₀

Tactic:
constructor

Goal state after:
case neg.left
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀

case neg.right
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
⊢ #↑s = ↑n ↔ ∃ t, ↑t = s ∧ t.card = n

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s : Set α
n : ℕ
⊢ #↑s = ↑n → ∃ t, ↑t = s ∧ t.card = n

case mpr
α : Type u_1
s : Set α
n : ℕ
⊢ (∃ t, ↑t = s ∧ t.card = n) → #↑s = ↑n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) ↔ ∃ h, Fintype.card α = n

Tactic:
constructor

Goal state after:
case mp
α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) → ∃ h, Fintype.card α = n

case mpr
α : Type u
n : ℕ
⊢ (∃ h, Fintype.card α = n) → ∃ t, ↑t = univ ∧ t.card = n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) ↔ ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
constructor

Goal state after:
case mp
α : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) → ∃ x y, x ≠ y ∧ {x, y} = univ

case mpr
α : Type u
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) ↔ ∃! y, y ≠ x

Tactic:
constructor

Goal state after:
case mp
α : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃! y, y ≠ x

case mpr
α : Type u
x : α
⊢ (∃! y, y ≠ x) → ∃ x y, x ≠ y ∧ {x, y} = univ
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mpr
α : Type u
x y : α
hne : y ≠ x
hy : ∀ (y_1 : α), (fun y ↦ y ≠ x) y_1 → y_1 = y
⊢ ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
exact ⟨x, y, hne.symm, eq_univ_of_forall fun z => or_iff_not_imp_left.2 (hy z)⟩

Goal state after:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a : M
x : α × β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ (x✝² • x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
ext

Goal state after:
case fst
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a : M
x : α × β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ ((x✝² • x✝¹) • x✝).1 = (x✝² • x✝¹ • x✝).1

case snd
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a : M
x : α × β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ ((x✝² • x✝¹) • x✝).2 = (x✝² • x✝¹ • x✝).2
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a : M
x : α × β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ x✝² • x✝¹ • x✝ = x✝¹ • x✝² • x✝

Tactic:
ext

Goal state after:
case fst
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a : M
x : α × β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ (x✝² • x✝¹ • x✝).1 = (x✝¹ • x✝² • x✝).1

case snd
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a : M
x : α × β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ (x✝² • x✝¹ • x✝).2 = (x✝¹ • x✝² • x✝).2
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
x✝² x✝¹ : M
x✝ : α × β
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
ext

Goal state after:
case fst
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
x✝² x✝¹ : M
x✝ : α × β
⊢ ((x✝² * x✝¹) • x✝).1 = (x✝² • x✝¹ • x✝).1

case snd
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
x✝² x✝¹ : M
x✝ : α × β
⊢ ((x✝² * x✝¹) • x✝).2 = (x✝² • x✝¹ • x✝).2
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
x✝ : α × β
⊢ 1 • x✝ = x✝

Tactic:
ext

Goal state after:
case fst
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
x✝ : α × β
⊢ (1 • x✝).1 = x✝.1

case snd
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
x✝ : α × β
⊢ (1 • x✝).2 = x✝.2
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
⊢ ↑e₁₂ ∘ₛₗ ↑e₁₂.symm ∘ₛₗ f = f

Tactic:
ext

Goal state after:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
x✝ : M₃
⊢ (↑e₁₂ ∘ₛₗ ↑e₁₂.symm ∘ₛₗ f) x✝ = f x✝