mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑qi * ↑denom✝ = 1

Tactic:
by norm_cast

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑denom✝ * ↑qi = 1

Tactic:
by norm_cast

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 ↔ n ∣ m

Tactic:
constructor

Goal state after:
case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 → n ∣ m

case mpr
m n : ℤ
hn : ↑n ≠ 0
⊢ n ∣ m → (↑m / ↑n).den = 1
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a ≤ b) = (1 / gcd * (bd * a') ≤ 1 / gcd * (ad * b'))

Tactic:
rw [mul_le_mul_iff_right₀, ← ha, ← hb, ← mul_assoc, ← mul_assoc, mul_comm bd,
    mul_le_mul_iff_right₀]
  · exact mul_pos had hbd
  · exact one_div_pos.2 hgcd

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝⁷ : NonAssocSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : CanonicallyOrderedAdd R
inst✝⁴ : Sub R
inst✝³ : OrderedSub R
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : MulRightMono R
inst✝ : AddLeftReflectLE R
a b : R
⊢ (a - 1) * b = a * b - b

Tactic:
rw [tsub_mul, one_mul]

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

Goal state before:
pp: α : Type u_1
f : ℕ → α
⊢ f '' {0} ∪ f '' range succ = range f

Tactic:
← image_union,

Goal state after:
α : Type u_1
f : ℕ → α
⊢ f '' ({0} ∪ range succ) = range f
Module: Mathlib.Data.Set.BooleanAlgebra

Goal state before:
pp: α ι✝ : Type u_1
κ✝ : ι✝ → Type u_1
f✝ : (a : ι✝) → κ✝ a → Set α
⊢ ⨅ a, ⨆ b, f✝ a b = ⨆ g, ⨅ a, f✝ a (g a)

Tactic:
ext

Goal state after:
α ι✝ : Type u_1
κ✝ : ι✝ → Type u_1
f✝ : (a : ι✝) → κ✝ a → Set α
x✝ : α
⊢ x✝ ∈ ⨅ a, ⨆ b, f✝ a b ↔ x✝ ∈ ⨆ g, ⨅ a, f✝ a (g a)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
P : ι → α → Prop
⊢ ⋃ i, {x | P i x} = {x | ∃ i, P i x}

Tactic:
ext

Goal state after:
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
x✝ : α
⊢ x✝ ∈ ⋃ i, {x | P i x} ↔ x✝ ∈ {x | ∃ i, P i x}
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
P : ι → α → Prop
⊢ ⋂ i, {x | P i x} = {x | ∀ (i : ι), P i x}

Tactic:
ext

Goal state after:
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
x✝ : α
⊢ x✝ ∈ ⋂ i, {x | P i x} ↔ x✝ ∈ {x | ∀ (i : ι), P i x}
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ (⨆ (_ : i ≥ i), f i) ⊔ ⨆ i_1, ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≥ i), f i_1 = f i ⊔ ⨆ j, ⨆ (_ : j > i), f j

Tactic:
simp only [ge_iff_le, le_refl, iSup_pos, ne_comm, iSup_and', gt_iff_lt, lt_iff_le_and_ne,
    and_comm]

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

Goal state before:
pp: α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ y, range fun s ↦ ↑(f s y)) ↔ x ∈ ⋃₀ C

Tactic:
constructor

Goal state after:
case mp
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ y, range fun s ↦ ↑(f s y)) → x ∈ ⋃₀ C

case mpr
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ x ∈ ⋃₀ C → x ∈ ⋃ y, range fun s ↦ ↑(f s y)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ range fun x ↦ ↑(f x i)) ↔ ∃ i, x ∈ C i

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ range fun x ↦ ↑(f x i)) → ∃ i, x ∈ C i

case mpr
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ C i) → ∃ i, x ∈ range fun x ↦ ↑(f x i)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_12
σ : Type u_13
s : ι → Set α
t : σ → Set α
⊢ ⋃ x, Sum.elim s t x = (⋃ x, s x) ∪ ⋃ x, t x

Tactic:
ext

Goal state after:
α : Type u_1
ι : Type u_12
σ : Type u_13
s : ι → Set α
t : σ → Set α
x✝ : α
⊢ x✝ ∈ ⋃ x, Sum.elim s t x ↔ x✝ ∈ (⋃ x, s x) ∪ ⋃ x, t x
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
π : α → Type u_12
i : Set α
s : (a : α) → Set (π a)
⊢ i.pi s = ⋂ a ∈ i, eval a ⁻¹' s a

Tactic:
ext

Goal state after:
α : Type u_1
π : α → Type u_12
i : Set α
s : (a : α) → Set (π a)
x✝ : (i : α) → π i
⊢ x✝ ∈ i.pi s ↔ x✝ ∈ ⋂ a ∈ i, eval a ⁻¹' s a
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
π : α → Type u_12
ι : α → Type u_13
t : (a : α) → ι a → Set (π a)
⊢ (⋃ x, univ.pi fun a ↦ t a (x a)) = univ.pi fun a ↦ ⋃ j, t a j

Tactic:
ext

Goal state after:
α : Type u_1
π : α → Type u_12
ι : α → Type u_13
t : (a : α) → ι a → Set (π a)
x✝ : (i : α) → π i
⊢ (x✝ ∈ ⋃ x, univ.pi fun a ↦ t a (x a)) ↔ x✝ ∈ univ.pi fun a ↦ ⋃ j, t a j
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
π : α → Type u_12
ι : α → Type u_13
s : (a : α) → Set (ι a)
t : (a : α) → ι a → Set (π a)
⊢ (⋃ x ∈ univ.pi s, univ.pi fun a ↦ t a (x a)) = univ.pi fun a ↦ ⋃ j ∈ s a, t a j

Tactic:
ext

Goal state after:
α : Type u_1
π : α → Type u_12
ι : α → Type u_13
s : (a : α) → Set (ι a)
t : (a : α) → ι a → Set (π a)
x✝ : (i : α) → π i
⊢ (x✝ ∈ ⋃ x ∈ univ.pi s, univ.pi fun a ↦ t a (x a)) ↔ x✝ ∈ univ.pi fun a ↦ ⋃ j ∈ s a, t a j
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h1 : (fun a ↦ ↑a) '' s ⊆ {⊤}
⊢ ↑(sInf s) = ⊤

pp: case pos.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h2 : ¬BddBelow ((fun a ↦ ↑a) '' s)
⊢ ↑(sInf s) = ⊤

Tactic:
· cases h1 (mem_image_of_mem _ hx)

Goal state after:
case pos.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h2 : ¬BddBelow ((fun a ↦ ↑a) '' s)
⊢ ↑(sInf s) = ⊤
Module: Mathlib.Order.Interval.Set.Image

Goal state before:
pp: α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r (↑c) x → p a x
⊢ {x | p a x ∧ q x b} ∩ {y | r (↑c) y} = {y | r (↑c) y ∧ q y b}

Tactic:
ext

Goal state after:
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r (↑c) x → p a x
x✝ : α
⊢ x✝ ∈ {x | p a x ∧ q x b} ∩ {y | r (↑c) y} ↔ x✝ ∈ {y | r (↑c) y ∧ q y b}
Module: Mathlib.Order.Interval.Set.Image

Goal state before:
pp: α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r x ↑c → q x b
⊢ {x | p a x ∧ q x b} ∩ {y | r y ↑c} = {y | p a y ∧ r y ↑c}

Tactic:
ext

Goal state after:
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r x ↑c → q x b
x✝ : α
⊢ x✝ ∈ {x | p a x ∧ q x b} ∩ {y | r y ↑c} ↔ x✝ ∈ {y | p a y ∧ r y ↑c}
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : 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 = ⨆ g, ⨅ a, f a (g a)

Tactic:
ext

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.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
ext

Goal state after:
α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
x✝ : ι
⊢ (⨅ a, ⨆ b, f a b) x✝ = (⨆ g, ⨅ a, f a (g a)) x✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : Frame.MinimalAxioms β
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
a : α
s : Set α
⊢ ⨆ i ∈ s, f (a ⊓ i) ≤ f (sSup (min a '' s))

Tactic:
exact ((map_sSup _).trans iSup_image).ge

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

Goal state before:
pp: α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ sInf s = n ↔ n ∈ s ∧ ∀ a ∈ s, n ≤ a

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ sInf s = n → n ∈ s ∧ ∀ a ∈ s, n ≤ a

case mpr
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ (n ∈ s ∧ ∀ a ∈ s, n ≤ a) → sInf s = n
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
constructor

Goal state after:
case left
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ sSup s ∈ upperBounds s

case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ sSup s ∈ lowerBounds (upperBounds s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
constructor

Goal state after:
case left
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ lowerBounds s

case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ upperBounds (lowerBounds s)
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : 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₁ ∧ b₁ ≤ b₂

Tactic:
constructor

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.Interval.Set.OrderEmbedding

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

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Icc (e x) (e y) ↔ x✝ ∈ Icc x y
Module: Mathlib.Order.Interval.Set.OrderEmbedding

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

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ico (e x) (e y) ↔ x✝ ∈ Ico x y
Module: Mathlib.Order.Interval.Set.OrderEmbedding

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

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ioc (e x) (e y) ↔ x✝ ∈ Ioc x y
Module: Mathlib.Order.Interval.Set.OrderEmbedding

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

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ioo (e x) (e y) ↔ x✝ ∈ Ioo x y
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ s.Pairwise (r on f) ↔ ∃ z, ∀ (x : ι), x ∈ s → r (f x) z

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ s.Pairwise (r on f) → ∃ z, ∀ (x : ι), x ∈ s → r (f x) z

case mpr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ (∃ z, ∀ (x : ι), x ∈ s → r (f x) z) → s.Pairwise (r on f)
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ Monotone f ∨ Antitone f ↔ ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ Monotone f ∨ Antitone f → ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ (∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]) → Monotone f ∨ Antitone f
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
h' : s = ∅
⊢ IsEmpty α

Tactic:
constructor

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
h' : s = ∅
⊢ ∀ (a : α), False
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
ht : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun x ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun x ↦ x ∈ s) b
x : α
hx : x ∈ t
y : α
hyx : y ≤ x
hy : Maximal (fun x ↦ x ∈ s) y
⊢ x ∈ {x | Maximal (fun x ↦ x ∈ s) x}

Tactic:
rwa [← ht.eq (h y hy) hx hyx]

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
h' : s = ∅
⊢ IsEmpty α

Tactic:
constructor

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
h' : s = ∅
⊢ ∀ (a : α), False
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ (Subtype.val '' range fun i ↦ f i) = range fun i ↦ ↑(f i)

Tactic:
ext

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
x✝ : α
⊢ (x✝ ∈ Subtype.val '' range fun i ↦ f i) ↔ x✝ ∈ range fun i ↦ ↑(f i)
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case e_a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ (Subtype.val '' range fun i ↦ f i) = range fun i ↦ ↑(f i)

Tactic:
ext

Goal state after:
case e_a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
x✝ : α
⊢ (x✝ ∈ Subtype.val '' range fun i ↦ f i) ↔ x✝ ∈ range fun i ↦ ↑(f i)
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ⟨↑r, ⋯⟩ * ⟨(↑r)⁻¹, ⋯⟩ = 1

Tactic:
ext

Goal state after:
α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ↑(⟨↑r, ⋯⟩ * ⟨(↑r)⁻¹, ⋯⟩) = ↑1
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ⟨(↑r)⁻¹, ⋯⟩ * ⟨↑r, ⋯⟩ = 1

Tactic:
ext

Goal state after:
α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ↑(⟨(↑r)⁻¹, ⋯⟩ * ⟨↑r, ⋯⟩) = ↑1
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 ≤ r }ˣ
⊢ (fun r ↦ { val := ⟨↑r, ⋯⟩, inv := ⟨(↑r)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }) ((fun r ↦ ⟨↑↑r, ⋯⟩) r) = r

Tactic:
ext

Goal state after:
α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 ≤ r }ˣ
⊢ ↑↑((fun r ↦ { val := ⟨↑r, ⋯⟩, inv := ⟨(↑r)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }) ((fun r ↦ ⟨↑↑r, ⋯⟩) r)) = ↑↑r
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ (fun r ↦ ⟨↑↑r, ⋯⟩) ((fun r ↦ { val := ⟨↑r, ⋯⟩, inv := ⟨(↑r)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }) r) = r

Tactic:
ext

Goal state after:
α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ↑((fun r ↦ ⟨↑↑r, ⋯⟩) ((fun r ↦ { val := ⟨↑r, ⋯⟩, inv := ⟨(↑r)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }) r)) = ↑r
Module: Mathlib.Tactic.NormNum.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
⊢ IsNat (↑na) na

Tactic:
constructor

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
⊢ ↑na = ↑na
Module: Mathlib.Tactic.NormNum.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsInt a (Int.negOfNat na)
⊢ IsNat |↑(Int.negOfNat na)| na

Tactic:
constructor

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsInt a (Int.negOfNat na)
⊢ |↑(Int.negOfNat na)| = ↑na
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: n✝¹ n✝ : ℤ
e : (n✝.emod n✝¹ != 0) = true
⊢ ¬↑n✝ % ↑n✝¹ = 0

Tactic:
simpa using! e

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

Goal state before:
pp: q : ℚ
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
⊢ 0 ≤ ↑q ↔ 0 ≤ q

Tactic:
by norm_cast

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

Goal state before:
pp: q : ℚ
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
⊢ ↑q ≤ 0 ↔ q ≤ 0

Tactic:
by norm_cast

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

Goal state before:
pp: q : ℚ
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
⊢ 0 < ↑q ↔ 0 < q

Tactic:
by norm_cast

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

Goal state before:
pp: q : ℚ
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
⊢ ↑q < 0 ↔ q < 0

Tactic:
by norm_cast

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
q : ℚ≥0
⊢ ↑q ≤ 0 ↔ q ≤ 0

Tactic:
by norm_cast

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
q : ℚ≥0
⊢ 0 < ↑q ↔ 0 < q

Tactic:
by norm_cast

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
q : ℚ≥0
⊢ ↑q < 0 ↔ q < 0

Tactic:
by norm_cast

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
⊢ ↑p ≤ 1 ↔ p ≤ 1

Tactic:
by norm_cast

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
⊢ 1 ≤ ↑p ↔ 1 ≤ p

Tactic:
by norm_cast

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
⊢ ↑p < 1 ↔ p < 1

Tactic:
by norm_cast

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
⊢ 1 < ↑p ↔ 1 < p

Tactic:
by norm_cast

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

Goal state before:
pp: case pos
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ∃ a, f a = x
⊢ ¬Classical.choose hf ∈ mulSupport g

Tactic:
← Classical.choose_spec hf

Goal state after:
case pos
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hf : ∃ a, f a = x
hfg : ¬f (Classical.choose hf) ∈ f '' mulSupport g
⊢ ¬Classical.choose hf ∈ mulSupport g
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n ! = 1 ↔ n ≤ 1

Tactic:
constructor

Goal state after:
case mp
n : ℕ
⊢ n ! = 1 → n ≤ 1

case mpr
n : ℕ
⊢ n ≤ 1 → n ! = 1
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: k m : ℕ+
⊢ k ∣ m ↔ ↑k ∣ ↑m

Tactic:
constructor

Goal state after:
case mp
k m : ℕ+
⊢ k ∣ m → ↑k ∣ ↑m

case mpr
k m : ℕ+
⊢ ↑k ∣ ↑m → k ∣ m
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: k m : ℕ+
⊢ ↑m % ↑k = 0 ↔ m.mod k = k

Tactic:
constructor

Goal state after:
case mp
k m : ℕ+
⊢ ↑m % ↑k = 0 → m.mod k = k

case mpr
k m : ℕ+
⊢ m.mod k = k → ↑m % ↑k = 0
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: n : ℕ+
a : ℕ
h : a ∣ ↑n
⊢ 0 < a

Tactic:
apply pos_iff_ne_zero.2

Goal state after:
n : ℕ+
a : ℕ
h : a ∣ ↑n
⊢ a ≠ 0
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
this✝ : ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
this : x + 1 / 2 < ↑⌊x + 1 / 2⌋ + 1
⊢ x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2 ∧ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2

Tactic:
constructor

Goal state after:
case left
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
this✝ : ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
this : x + 1 / 2 < ↑⌊x + 1 / 2⌋ + 1
⊢ x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2

case right
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
this✝ : ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
this : x + 1 / 2 < ↑⌊x + 1 / 2⌋ + 1
⊢ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ ⌊a + 1⌋ = ⌊a⌋ + 1

Tactic:
by
  rw [← cast_one, floor_add_intCast]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ a - b ≤ a ∧ a < a - b + 1

Tactic:
constructor

Goal state after:
case left
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ a - b ≤ a

case right
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ a < a - b + 1