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

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
h : IsExtent r s
hs' : s' ⊆ s
⊢ lowerPolar r (upperPolar r s') ⊆ lowerPolar r (upperPolar r s)

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
h : IsExtent r s
hs' : s' ⊆ s
⊢ lowerPolar r (upperPolar r s') ⊆ lowerPolar r (upperPolar r s)
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
t t' : Set β
h : IsIntent r t
ht' : t' ⊆ t
⊢ upperPolar r (lowerPolar r t') ⊆ upperPolar r (lowerPolar r t)

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
t t' : Set β
h : IsIntent r t
ht' : t' ⊆ t
⊢ upperPolar r (lowerPolar r t') ⊆ upperPolar r (lowerPolar r t)
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
x : α
y : β
hx : x ∈ c.extent
hy : y ∈ upperPolar r c.extent
⊢ r x y

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
x : α
y : β
hx : x ∈ c.extent
hy : y ∈ upperPolar r c.extent
⊢ r x y
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : Std.Irrefl r'
⊢ ∀ ⦃a : α⦄, a ∈ c'.extent → ∀ ⦃b : α⦄, b ∈ c'.intent → a ≠ b

Tactic:
]

Goal state after:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : Std.Irrefl r'
⊢ ∀ ⦃a : α⦄, a ∈ c'.extent → ∀ ⦃b : α⦄, b ∈ c'.intent → a ≠ b
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : Std.Irrefl r'
⊢ Disjoint c'.extent c'.intent

Tactic:
rw [disjoint_iff_forall_ne]
  rintro x hx _ hx' rfl
  exact irrefl x (rel_extent_intent hx hx')

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : IsTrans α r'
x y : α
hy : r' y x
hx : x ∈ c'.extent
⊢ y ∈ lowerPolar r' c'.intent

Tactic:
]

Goal state after:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : IsTrans α r'
x y : α
hy : r' y x
hx : x ∈ c'.extent
⊢ y ∈ lowerPolar r' c'.intent
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : IsTrans α r'
x y : α
hy : r' x y
hx : x ∈ c'.intent
⊢ y ∈ upperPolar r' c'.extent

Tactic:
]

Goal state after:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : IsTrans α r'
x y : α
hy : r' x y
hx : x ∈ c'.intent
⊢ y ∈ upperPolar r' c'.extent
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝¹ : Std.Trichotomous r'
inst✝ : IsTrans α r'
⊢ ⊤ ⊆ c'.extent ⊔ c'.intent

Tactic:
]

Goal state after:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝¹ : Std.Trichotomous r'
inst✝ : IsTrans α r'
⊢ ⊤ ⊆ c'.extent ⊔ c'.intent
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝¹ : Std.Trichotomous r'
inst✝ : IsTrans α r'
x : α
x✝ : x ∈ ⊤
hx : x ∉ c'.extent
⊢ x ∈ upperPolar r' c'.extent

Tactic:
]

Goal state after:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝¹ : Std.Trichotomous r'
inst✝ : IsTrans α r'
x : α
x✝ : x ∈ ⊤
hx : x ∉ c'.extent
⊢ x ∈ upperPolar r' c'.extent
Module: Mathlib.Order.Concept

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.intent ⊆ d.intent
⊢ lowerPolar r d.intent ⊆ lowerPolar r c.intent

Tactic:
]

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.intent ⊆ d.intent
⊢ lowerPolar r d.intent ⊆ lowerPolar r c.intent
Module: Mathlib.Order.Concept

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : d ≤ c
⊢ upperPolar r c.extent ⊆ upperPolar r d.extent

Tactic:
]

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : d ≤ c
⊢ upperPolar r c.extent ⊆ upperPolar r d.extent
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ (∀ b ∈ A.left, b ≤ x✝) ↔ ∀ x ∈ A.left, x ≤ x✝

Tactic:
]

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ d ≤ c ∧ ¬c ≤ d ↔ d ≤ c ∧ ¬c ≤ d

Tactic:
]

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ (∀ b ∈ A.right, x✝ ≤ b) ↔ ∀ x ∈ A.right, x✝ ≤ x

Tactic:
]

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
⊢ principal (sInf A.right) = A

Tactic:
by
  ext
  rw [left_principal, mem_Iic, le_sInf_iff, ← lowerBounds_right, mem_lowerBounds]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u ⟨p, hp⟩
f : 𝕊 → 𝕊 := fun y ↦ p • y + x
q : ℕ
hn : 0 < p * q
h_ndiv : ¬p * p ∣ p * q
⊢ ¬p ∣ q

Tactic:
]

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u ⟨p, hp⟩
f : 𝕊 → 𝕊 := fun y ↦ p • y + x
q : ℕ
hn : 0 < p * q
h_ndiv : ¬p * p ∣ p * q
⊢ ¬p ∣ q
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
A B : DedekindCut β
x : β
hx : x ∈ A.extent
h : ∀ b ∈ upperBounds (⇑f '' B.left), ∀ ⦃x : β⦄, x ∈ A.left → f x ≤ b
y : β
hy : y ∈ B.right
⊢ f x ≤ f y

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
A B : DedekindCut β
x : β
hx : x ∈ A.extent
h : ∀ b ∈ upperBounds (⇑f '' B.left), ∀ ⦃x : β⦄, x ∈ A.left → f x ≤ b
y : β
hy : y ∈ B.right
⊢ f x ≤ f y
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
x : β
⊢ sSup (⇑f '' (principal x).left) = f x

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
x : β
⊢ sSup (⇑f '' (principal x).left) = f x
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
x : β
⊢ ∀ b ∈ upperBounds (⇑f '' (principal x).left), f x ≤ b

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
x : β
⊢ ∀ b ∈ upperBounds (⇑f '' (principal x).left), f x ≤ b
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
c : Concept α β r
⊢ (ofObjects r s).extent ⊆ c.extent ↔ s ⊆ c.extent

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
c : Concept α β r
⊢ (ofObjects r s).extent ⊆ c.extent ↔ s ⊆ c.extent
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
⊢ (ofAttributes r t).intent ⊆ c.intent ↔ t ⊆ c.intent

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
⊢ (ofAttributes r t).intent ⊆ c.intent ↔ t ⊆ c.intent
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
h : c.intent ⊆ t
⊢ c.intent ⊆ (ofAttributes r t).intent

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
h : c.intent ⊆ t
⊢ c.intent ⊆ (ofAttributes r t).intent
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : a.extent ⊆ b.extent ∧ ∃ x ∈ b.extent, x ∉ a.extent
⊢ ∃ c, a < principal c ∧ principal c ≤ b

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : a.extent ⊆ b.extent ∧ ∃ x ∈ b.extent, x ∉ a.extent
⊢ ∃ c, a < principal c ∧ principal c ≤ b
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : b.intent ⊆ a.intent ∧ ∃ x ∈ a.intent, x ∉ b.intent
⊢ ∃ c, a ≤ principal c ∧ principal c < b

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : b.intent ⊆ a.intent ∧ ∃ x ∈ a.intent, x ∉ b.intent
⊢ ∃ c, a ≤ principal c ∧ principal c < b
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : CompleteLattice α
hs : ∀ (A : ℕ → α), (∀ (n : ℕ), A n ∈ s) → ⨆ n, A n ∈ s
x : α
f : ℕ → α
hAs : range f ⊆ s
hA_ne : (range f).Nonempty
hAc : (range f).Countable
hx : IsLUB (range f) x
⊢ ⨆ n, f n ∈ s

Tactic:
]

Goal state after:
α : Type u_2
s : Set α
inst✝ : CompleteLattice α
hs : ∀ (A : ℕ → α), (∀ (n : ℕ), A n ∈ s) → ⨆ n, A n ∈ s
x : α
f : ℕ → α
hAs : range f ⊆ s
hA_ne : (range f).Nonempty
hAc : (range f).Countable
hx : IsLUB (range f) x
⊢ ⨆ n, f n ∈ s
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ a ∉ c.right ↔ ∃ b ∈ c.left, a < b

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ a ∉ c.right ↔ ∃ b ∈ c.left, a < b
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ (∀ (x : α), ¬(x ∈ c.left ∧ a < x)) ↔ c ≤ principal a

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ (∀ (x : α), ¬(x ∈ c.left ∧ a < x)) ↔ c ≤ principal a
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : CompleteLattice α
hs : CountableSupClosed s
A : Set α
hA_c : A.Countable
hA_ne : A.Nonempty
hA : ∀ a ∈ A, a ∈ s
⊢ ⨆ a, ↑a ∈ s

Tactic:
]

Goal state after:
α : Type u_2
s : Set α
inst✝ : CompleteLattice α
hs : CountableSupClosed s
A : Set α
hA_c : A.Countable
hA_ne : A.Nonempty
hA : ∀ a ∈ A, a ∈ s
⊢ ⨆ a, ↑a ∈ s
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ a ∉ c.left ↔ ∃ b ∈ c.right, b < a

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ a ∉ c.left ↔ ∃ b ∈ c.right, b < a
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ (∀ (x : α), ¬(x ∈ c.right ∧ x < a)) ↔ principal a ≤ c

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ (∀ (x : α), ¬(x ∈ c.right ∧ x < a)) ↔ principal a ≤ c
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
s : Set α
y✝ y : α
x✝ : s.Countable
hy : IsLUB s y✝
hs_subset : ∀ y_1 ∈ s, y_1 = y
z : α
hzs : y ∈ s
⊢ y ∈ s

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : PartialOrder α
s : Set α
y✝ y : α
x✝ : s.Countable
hy : IsLUB s y✝
hs_subset : ∀ y_1 ∈ s, y_1 = y
z : α
hzs : y ∈ s
⊢ y ∈ s
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ (∀ (x : α), ¬(x ∈ c.right ∧ x < a)) ↔ c.intent ⊆ (principal a).intent

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ (∀ (x : α), ¬(x ∈ c.right ∧ x < a)) ↔ c.intent ⊆ (principal a).intent
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
β : Type u_3
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
t : Set β
hs : CountableSupClosed s
ht : CountableSupClosed t
A : Set (α × β)
hAst : A ⊆ s ×ˢ t
hA_ne : A.Nonempty
hAc : A.Countable
x : α
y : β
hxy : IsLUB (Prod.fst '' A) (x, y).1 ∧ IsLUB (Prod.snd '' A) (x, y).2
⊢ (x, y) ∈ s ×ˢ t

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
t : Set β
hs : CountableSupClosed s
ht : CountableSupClosed t
A : Set (α × β)
hAst : A ⊆ s ×ˢ t
hA_ne : A.Nonempty
hAc : A.Countable
x : α
y : β
hxy : IsLUB (Prod.fst '' A) (x, y).1 ∧ IsLUB (Prod.snd '' A) (x, y).2
⊢ (x, y) ∈ s ×ˢ t
Module: Mathlib.SetTheory.Ordinal.Rank

Goal state before:
pp: α : Type u
a b : α
r : α → α → Prop
hb : Acc r b
h : r a b
⊢ Order.succ ⋯.rank ≤ ⨆ b_1, Order.succ ⋯.rank

Tactic:
]

Goal state after:
α : Type u
a b : α
r : α → α → Prop
hb : Acc r b
h : r a b
⊢ Order.succ ⋯.rank ≤ ⨆ b_1, Order.succ ⋯.rank
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
h : ¬s' x y ∧ ¬s' y x
⊢ False

pp: α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
⊢ s' ∈ S

Tactic:
]

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
h : ¬s' x y ∧ ¬s' y x
⊢ False

α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
⊢ s' ∈ S
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u ⟨p, hp⟩
f : 𝕊 → 𝕊 := fun y ↦ p • y + x
n : ℕ
hn : 0 < n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
h_div : n / p * p = n
hf : f = (fun y ↦ x + y) ∘ fun y ↦ p • y
⊢ (fun y ↦ x + y) '' (fun y ↦ p • y) '' X n ⊆ approxAddOrderOf 𝕊 n (↑p * δ n)

Tactic:
]

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u ⟨p, hp⟩
f : 𝕊 → 𝕊 := fun y ↦ p • y + x
n : ℕ
hn : 0 < n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
h_div : n / p * p = n
hf : f = (fun y ↦ x + y) ∘ fun y ↦ p • y
⊢ (fun y ↦ x + y) '' (fun y ↦ p • y) '' X n ⊆ approxAddOrderOf 𝕊 n (↑p * δ n)
Module: Mathlib.SetTheory.Ordinal.Rank

Goal state before:
pp: case inr
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
ho : ∃ i, o < Order.succ ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Tactic:
]

Goal state after:
case inr
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
ho : ∃ i, o < Order.succ ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o
Module: Mathlib.SetTheory.Ordinal.Rank

Goal state before:
pp: case inr
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
b : α
hb : r b a
ho : o ≤ ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Tactic:
]

Goal state after:
case inr
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
b : α
hb : r b a
ho : o ≤ ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: case refine_3
ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s A : Set α
hA_ne : A.Nonempty
hAc : A.Countable
x : α
hx : IsLUB A x
B : ⦃a : α⦄ → a ∈ A → Set α
hB : ∀ ⦃a : α⦄ (a_1 : a ∈ A), B a_1 ⊆ s
hB_ne : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Nonempty
hBc : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Countable
hB_lub : ∀ ⦃a : α⦄ (a_1 : a ∈ A), IsLUB (B a_1) a
this : Nonempty ↑A
⊢ IsLUB (Set.range fun a ↦ ↑a) x

Tactic:
]

Goal state after:
case refine_3
ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s A : Set α
hA_ne : A.Nonempty
hAc : A.Countable
x : α
hx : IsLUB A x
B : ⦃a : α⦄ → a ∈ A → Set α
hB : ∀ ⦃a : α⦄ (a_1 : a ∈ A), B a_1 ⊆ s
hB_ne : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Nonempty
hBc : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Countable
hB_lub : ∀ ⦃a : α⦄ (a_1 : a ∈ A), IsLUB (B a_1) a
this : Nonempty ↑A
⊢ IsLUB (Set.range fun a ↦ ↑a) x
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A b
⊢ b ≤ a

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A b
⊢ b ≤ a
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : Order.Coframe α
hs : SupClosed s
a : α
ha : ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨅ n, t n = a
b : α
hb : ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨅ n, t n = b
⊢ ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨅ n, t n = a ⊔ b

Tactic:
]

Goal state after:
α : Type u_2
s : Set α
inst✝ : Order.Coframe α
hs : SupClosed s
a : α
ha : ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨅ n, t n = a
b : α
hb : ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨅ n, t n = b
⊢ ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨅ n, t n = a ⊔ b
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : Order.Coframe α
hs : SupClosed s
t : ℕ → α
ht : ∀ (n : ℕ), t n ∈ s
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ s
⊢ ∃ t_1, (∀ (n : ℕ), t_1 n ∈ s) ∧ ⨅ n, t_1 n = ⨅ i, t i.1 ⊔ u i.2

Tactic:
]

Goal state after:
α : Type u_2
s : Set α
inst✝ : Order.Coframe α
hs : SupClosed s
t : ℕ → α
ht : ∀ (n : ℕ), t n ∈ s
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ s
⊢ ∃ t_1, (∀ (n : ℕ), t_1 n ∈ s) ∧ ⨅ n, t_1 n = ⨅ i, t i.1 ⊔ u i.2
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: case refine_2
α : Type u_2
s : Set α
inst✝ : Order.Coframe α
hs : SupClosed s
t : ℕ → α
ht : ∀ (n : ℕ), t n ∈ s
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ s
⊢ ⨅ x, t x.1 ⊔ u x.2 = ⨅ i, t i.1 ⊔ u i.2

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case e'_4
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this✝ : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u ⟨p, hp⟩
f : 𝕊 → 𝕊 := fun y ↦ p • y + x
n : ℕ
hn : 0 < n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
h_div : n / p * p = n
hf : f = (fun y ↦ x + y) ∘ fun y ↦ p • y
this :
  (fun y ↦ x + y) '' (fun y ↦ p • y) '' approxAddOrderOf 𝕊 n (δ n) ⊆
    (fun y ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) (↑p * δ n)
⊢ n = n

Tactic:
]

Goal state after: