mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ i, ⨆ (_ : i ≥ n), u i ≤ ⨆ i, u (i + n)

pp: case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ i, u (i + n) ≤ ⨆ i, ⨆ (_ : i ≥ n), u i

Tactic:
<;>

Goal state after:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ i, ⨆ (_ : i ≥ n), u i ≤ ⨆ i, u (i + n)

case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ i, u (i + n) ≤ ⨆ i, ⨆ (_ : i ≥ n), u i
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝ : CompleteLattice α
s : Set (ULift α)
⊢ (sInf s).down = ⨅ a ∈ s, a.down

Tactic:
sInf_eq_iInf',

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝ : CompleteLattice α
s : Set (ULift α)
⊢ (⨅ a, ↑a).down = ⨅ a ∈ s, a.down
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), l (u a ⊓ u b) ≤ b

Tactic:
exact fun a b => gi.gc.l_le inf_le_right

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CompleteLattice α
p : Prop
inst✝ : Decidable p
a : p → α
h : p
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥

pp: case neg
α : Type u_1
inst✝¹ : CompleteLattice α
p : Prop
inst✝ : Decidable p
a : p → α
h : ¬p
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝¹ : CompleteLattice α
p : Prop
inst✝ : Decidable p
a : p → α
h : p
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥

case neg
α : Type u_1
inst✝¹ : CompleteLattice α
p : Prop
inst✝ : Decidable p
a : p → α
h : ¬p
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
h : p i
⊢ f i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h

pp: case neg
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
h : ¬p i
⊢ g i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
h : p i
⊢ f i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h

case neg
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
h : ¬p i
⊢ g i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Iic (⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, Iic (f i j)

Tactic:
simp_rw [Iic_iInf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
b₂ : β
h₂ : b₂ ∈ t a₂
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₂, ⟨b₂, h₂⟩⟩
b_eq : b₁ = b₂
a_eq : a₁ = a₂
⊢ ↑(Eq.recOn a_eq ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₂, ⟨b₂, h₂⟩⟩.snd

Tactic:
subst b_eq; subst a_eq; rfl

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
a b c : α
⊢ a ⇨ b ≤ c ↔ ∀ (d : α), d ⊓ a ≤ b → d ≤ c

Tactic:
by simp [himp_eq_sSup]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case fst
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝¹ : CompletelyDistribLattice α
inst✝ : CompletelyDistribLattice β
ι✝ : Type (max u v)
κ✝ : ι✝ → Type (max u v)
f : (a : ι✝) → κ✝ a → α × β
⊢ (⨅ a, ⨆ b, f a b).1 = (⨆ g, ⨅ a, f a (g a)).1

pp: case snd
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝¹ : CompletelyDistribLattice α
inst✝ : CompletelyDistribLattice β
ι✝ : Type (max u v)
κ✝ : ι✝ → Type (max u v)
f : (a : ι✝) → κ✝ a → α × β
⊢ (⨅ a, ⨆ b, f a b).2 = (⨆ g, ⨅ a, f a (g a)).2

Tactic:
<;>

Goal state after:
case fst
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝¹ : CompletelyDistribLattice α
inst✝ : CompletelyDistribLattice β
ι✝ : Type (max u v)
κ✝ : ι✝ → Type (max u v)
f : (a : ι✝) → κ✝ a → α × β
⊢ (⨅ a, ⨆ b, f a b).1 = (⨆ g, ⨅ a, f a (g a)).1

case snd
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝¹ : CompletelyDistribLattice α
inst✝ : CompletelyDistribLattice β
ι✝ : Type (max u v)
κ✝ : ι✝ → Type (max u v)
f : (a : ι✝) → κ✝ a → α × β
⊢ (⨅ a, ⨆ b, f a b).2 = (⨆ g, ⨅ a, f a (g a)).2
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
h✝ : BddAbove (s ∪ t)
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
h✝ : ¬BddAbove (s ∪ t)
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
h✝ : BddAbove (s ∪ t)
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
h✝ : ¬BddAbove (s ∪ t)
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: case e'_1.e'_3
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
e_1✝ : Set α = Set αᵒᵈ
⊢ Ioc a₁ b₁ = Ico b₁ a₁

pp: case e'_1.e'_4
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
e_1✝ : Set α = Set αᵒᵈ
⊢ Ioc a₂ b₂ = Ico b₂ a₂

Tactic:
<;>

Goal state after:
case e'_1.e'_3
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
e_1✝ : Set α = Set αᵒᵈ
⊢ Ioc a₁ b₁ = Ico b₁ a₁

case e'_1.e'_4
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
e_1✝ : Set α = Set αᵒᵈ
⊢ Ioc a₂ b₂ = Ico b₂ a₂
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: case left
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ a₂ ≤ a₁

pp: case right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ b₁ ≤ b₂

Tactic:
<;>

Goal state after:
case left
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ a₂ ≤ a₁

case right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ b₁ ≤ b₂
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
a : α
ha : a ∈ t
x : α
hxs : x ∈ s
hxa : x ≤ a
⊢ sInf (f '' s) ≤ f a

Tactic:
exact csInf_le_of_le (ht.mono (image_mono hst)) ⟨x, hxs, rfl⟩ (hf (hst hxs) ha hxa)

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderEmbedding

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
e : α ↪o β
x y : α
h✝ : x ≤ y
⊢ ⇑e ⁻¹' uIcc (e x) (e y) = uIcc x y

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
e : α ↪o β
x y : α
h✝ : y ≤ x
⊢ ⇑e ⁻¹' uIcc (e x) (e y) = uIcc x y

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
e : α ↪o β
x y : α
h✝ : x ≤ y
⊢ ⇑e ⁻¹' uIcc (e x) (e y) = uIcc x y

case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
e : α ↪o β
x y : α
h✝ : y ≤ x
⊢ ⇑e ⁻¹' uIcc (e x) (e y) = uIcc x y
Module: Mathlib.Order.Interval.Set.OrderEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' uIcc (e x) (e y) = uIcc x y

Tactic:
cases le_total x y <;> simp [*]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderEmbedding

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
e : α ↪o β
x y : α
h✝ : x ≤ y
⊢ ⇑e ⁻¹' uIoc (e x) (e y) = uIoc x y

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
e : α ↪o β
x y : α
h✝ : y ≤ x
⊢ ⇑e ⁻¹' uIoc (e x) (e y) = uIoc x y

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
e : α ↪o β
x y : α
h✝ : x ≤ y
⊢ ⇑e ⁻¹' uIoc (e x) (e y) = uIoc x y

case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
e : α ↪o β
x y : α
h✝ : y ≤ x
⊢ ⇑e ⁻¹' uIoc (e x) (e y) = uIoc x y
Module: Mathlib.Order.Interval.Set.OrderEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' uIoc (e x) (e y) = uIoc x y

Tactic:
cases le_total x y <;> simp [*]

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (min a b)) (f (max a b)))

pp: case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

pp: case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

pp: case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

pp: case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

Tactic:
<;>

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (min a b)) (f (max a b)))

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (max a b)) (f (min a b)))

pp: case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

pp: case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

pp: case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

pp: case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

Tactic:
<;>

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (max a b)) (f (min a b)))

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ [[a, b]] = Icc (min a b) (max a b)

pp: case h₁
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b ≤ b

pp: case h₂
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a ≤ a

Tactic:
<;>

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ [[a, b]] = Icc (min a b) (max a b)

case h₁
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b ≤ b

case h₂
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a ≤ a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b c x : α
h2 : x ≤ b
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b

pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c x : α
h2 : b ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c x : α
h2 : x ≤ b
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b

case inr
α : Type u_1
inst✝ : LinearOrder α
a b c x : α
h2 : b ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case mp.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]

pp: case mp.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Antitone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
<;>

Goal state after:
case mp.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]

case mp.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Antitone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝ : a ≤ b
⊢ Ι a b = Ioc a b ∪ Ioc b a

pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝ : b ≤ a
⊢ Ι a b = Ioc a b ∪ Ioc b a

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝ : a ≤ b
⊢ Ι a b = Ioc a b ∪ Ioc b a

case inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝ : b ≤ a
⊢ Ι a b = Ioc a b ∪ Ioc b a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a = b

pp: case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a = b

pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ a = b

pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ a = b

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a = b

case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a = b

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ a = b

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ a = b
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inl.inl.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b

pp: case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a

pp: case inl.inr.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b

pp: case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a

pp: case inr.inl.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b

pp: case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a

pp: case inr.inr.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b

pp: case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a

Tactic:
<;>

Goal state after:
case inl.inl.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b

case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a

case inl.inr.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b

case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a

case inr.inl.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b

case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a

case inr.inr.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b

case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
p : ℚ≥0
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑p < OfNat.ofNat n ↔ p < OfNat.ofNat n

Tactic:
simp [← cast_lt (K := K)]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
p : ℚ≥0
n : ℕ
inst✝ : n.AtLeastTwo
⊢ OfNat.ofNat n < ↑p ↔ OfNat.ofNat n < p

Tactic:
simp [← cast_lt (K := K)]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ mulSupport f = s ↔ (∀ (x : ι), x ∈ s → f x ≠ 1) ∧ ∀ (x : ι), ¬x ∈ s → f x = 1

Tactic:
simp +contextual only [Set.ext_iff, mem_mulSupport, ne_eq, iff_def,
    not_imp_comm, and_comm, forall_and]

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

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
y : M
hy : y ≠ 1
a : ι
⊢ a ∈ mulSupport (update f a y) ↔ a ∈ insert a (mulSupport f)

pp: case inr
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
a : ι
hne : a ≠ x
⊢ a ∈ mulSupport (update f x y) ↔ a ∈ insert x (mulSupport f)

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
y : M
hy : y ≠ 1
a : ι
⊢ a ∈ mulSupport (update f a y) ↔ a ∈ insert a (mulSupport f)

case inr
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
a : ι
hne : a ≠ x
⊢ a ∈ mulSupport (update f x y) ↔ a ∈ insert x (mulSupport f)
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
a : ι
⊢ a ∈ mulSupport (update f a 1) ↔ a ∈ mulSupport f \ {a}

pp: case inr
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x a : ι
hne : a ≠ x
⊢ a ∈ mulSupport (update f x 1) ↔ a ∈ mulSupport f \ {x}

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
a : ι
⊢ a ∈ mulSupport (update f a 1) ↔ a ∈ mulSupport f \ {a}

case inr
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x a : ι
hne : a ≠ x
⊢ a ∈ mulSupport (update f x 1) ↔ a ∈ mulSupport f \ {x}
Module: Mathlib.Algebra.Notation.Support

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

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

Tactic:
<;>

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

case inr
ι : Type u_1
M : Type u_3
inst✝² : One M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
f : ι → M
x : ι
y : M
hy : y ≠ 1
⊢ mulSupport (update f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : One M
i : ι
a : M
inst✝ : DecidableEq M
h : a = 1
⊢ mulSupport (mulSingle i a) = ∅

pp: case neg
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : One M
i : ι
a : M
inst✝ : DecidableEq M
h : ¬a = 1
⊢ mulSupport (mulSingle i a) = {i}

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : One M
i : ι
a : M
inst✝ : DecidableEq M
h : a = 1
⊢ mulSupport (mulSingle i a) = ∅

case neg
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : One M
i : ι
a : M
inst✝ : DecidableEq M
h : ¬a = 1
⊢ mulSupport (mulSingle i a) = {i}
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : a = 1
⊢ ∅.Subsingleton

pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : ¬a = 1
⊢ {i}.Subsingleton

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : a = 1
⊢ ∅.Subsingleton

case neg
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : ¬a = 1
⊢ {i}.Subsingleton
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case mpr.refl
⊢ 1! = 1

pp: case mpr.step.refl
⊢ 0! = 1

Tactic:
<;>

Goal state after:
case mpr.refl
⊢ 1! = 1

case mpr.step.refl
⊢ 0! = 1
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case refine_1
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ i ≤ i + n

pp: case refine_2
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ 0 < i + n

pp: case refine_3
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ 1 < (i + n)!

pp: case refine_4
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ n + 1 ≤ i + n

Tactic:
<;>

Goal state after:
case refine_1
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ i ≤ i + n

case refine_2
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ 0 < i + n

case refine_3
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ 1 < (i + n)!

case refine_4
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ n + 1 ≤ i + n
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1 - (k + 1)) ^ (k + 1) ≤ n.descFactorial (k + 1)

Tactic:
rw [descFactorial_succ, Nat.pow_succ, succ_sub_succ, Nat.mul_comm]
    apply Nat.mul_le_mul_left
    exact (le_trans (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) k)
      (pow_sub_le_descFactorial n k))

Goal state after: