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

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L : CompleteSublattice α
toSublattice✝¹ : Sublattice α
sSupClosed'✝¹ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝¹.carrier → sSup s ∈ toSublattice✝¹.carrier
sInfClosed'✝¹ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝¹.carrier → sInf s ∈ toSublattice✝¹.carrier
toSublattice✝ : Sublattice α
sSupClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sSup s ∈ toSublattice✝.carrier
sInfClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sInf s ∈ toSublattice✝.carrier
h :
  (fun L ↦ L.carrier) { toSublattice := toSublattice✝¹, sSupClosed' := sSupClosed'✝¹, sInfClosed' := sInfClosed'✝¹ } =
    (fun L ↦ L.carrier) { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ }
⊢ toSublattice✝¹ = toSublattice✝

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L : CompleteSublattice α
toSublattice✝¹ : Sublattice α
sSupClosed'✝¹ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝¹.carrier → sSup s ∈ toSublattice✝¹.carrier
sInfClosed'✝¹ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝¹.carrier → sInf s ∈ toSublattice✝¹.carrier
toSublattice✝ : Sublattice α
sSupClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sSup s ∈ toSublattice✝.carrier
sInfClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sInf s ∈ toSublattice✝.carrier
h :
  (fun L ↦ L.carrier) { toSublattice := toSublattice✝¹, sSupClosed' := sSupClosed'✝¹, sInfClosed' := sInfClosed'✝¹ } =
    (fun L ↦ L.carrier) { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ }
⊢ toSublattice✝¹ = toSublattice✝
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
e : Set α
i : Set β
he : e = c.extent
hi : i = c.intent
x✝ : α
⊢ x✝ ∈ (c.copy e i he hi).extent ↔ x✝ ∈ c.extent

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
e : Set α
i : Set β
he : e = c.extent
hi : i = c.intent
x✝ : α
⊢ x✝ ∈ (c.copy e i he hi).extent ↔ x✝ ∈ c.extent
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a x✝ : α
⊢ x✝ ∈ Iic a ↔ x✝ ∈ (ofObject (fun x1 x2 ↦ x1 ≤ x2) a).extent

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a x✝ : α
⊢ x✝ ∈ Iic a ↔ x✝ ∈ (ofObject (fun x1 x2 ↦ x1 ≤ x2) a).extent
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a x✝ : α
⊢ x✝ ∈ Ici a ↔ x✝ ∈ (ofObject (fun x1 x2 ↦ x1 ≤ x2) a).intent

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a x✝ : α
⊢ x✝ ∈ Ici a ↔ x✝ ∈ (ofObject (fun x1 x2 ↦ x1 ≤ x2) a).intent
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a x✝ : α
⊢ x✝ ∈ left (ofAttribute (fun x1 x2 ↦ x1 ≤ x2) a) ↔ x✝ ∈ (principal a).left

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
a x✝ : α
⊢ x✝ ∈ left (ofAttribute (fun x1 x2 ↦ x1 ≤ x2) a) ↔ x✝ ∈ (principal a).left
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
x✝ : β
⊢ (RelEmbedding.trans principalEmbedding (factorEmbedding f)) x✝ = f x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
x✝ : β
⊢ (RelEmbedding.trans principalEmbedding (factorEmbedding f)) x✝ = f x✝
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
x✝ : 𝕊
⊢ f x✝ = ((fun y ↦ x + y) ∘ fun y ↦ p • y) x✝

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
x✝ : 𝕊
⊢ f x✝ = ((fun y ↦ x + y) ∘ fun y ↦ p • y) x✝
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝² : CompleteLattice α
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hs : CountableSupClosed s
A : ι → α
hA : ∀ (n : ι), A n ∈ s
i₀ : ι := ⋯.some
⊢ {x | ∃ y, A y = x} ⊆ s

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
s : Set α
inst✝² : CompleteLattice α
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hs : CountableSupClosed s
A : ι → α
hA : ∀ (n : ι), A n ∈ s
i₀ : ι := ⋯.some
⊢ {x | ∃ y, A y = x} ⊆ s
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s : Set α
x : α
hxs : x ∈ s
⊢ x ∈ s

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s : Set α
x : α
hxs : x ∈ s
⊢ x ∈ s
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : 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
⊢ ∀ (i : α) (i_1 : i ∈ A), B ⋯ ⊆ s

Tactic:
;

Goal state after:
ι : 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
⊢ ∀ (i : α) (i_1 : i ∈ A), B ⋯ ⊆ s
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: case refine_1.inl.inr
α : 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'
a b c : α
ab : s a b
bx : s b x
yc : s y c
⊢ s' a c

pp: case refine_1.inr.inl
α : 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'
a b c : α
ax : s a x
yb : s y b
bc : s b c
⊢ s' a c

pp: case refine_1.inr.inr
α : 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'
a b c : α
ax : s a x
yb : s y b
bx : s b x
yc : s y c
⊢ s' a c

Tactic:
· exact Or.inr ⟨_root_.trans ab bx, yc⟩

Goal state after:
case refine_1.inr.inl
α : 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'
a b c : α
ax : s a x
yb : s y b
bc : s b c
⊢ s' a c

case refine_1.inr.inr
α : 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'
a b c : α
ax : s a x
yb : s y b
bx : s b x
yc : s y c
⊢ s' a c
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
p : α → (i : ι) → i ∈ S → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi

Tactic:
by
  simp only [Filter.Eventually, ofPred_forall]
  exact cardinal_bInter_mem hS

Goal state after:
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case refine_1
ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝ : CardinalInterFilter l✝ c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : #↑S < c
hSp : S ⊆ {s | sᶜ ∈ l}
⊢ ⋂₀ S ∈ {s | sᶜ ∈ l}

pp: case refine_2
ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝ : CardinalInterFilter l✝ c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : s ⊆ t
⊢ t ∈ {s | sᶜ ∈ l}

Tactic:
· rw [mem_ofPred_eq, compl_sInter]
    apply hUnion (compl '' S) (lt_of_le_of_lt mk_image_le hSc)
    intro s hs
    rw [mem_image] at hs
    rcases hs with ⟨t, ht, rfl⟩
    apply hSp ht

Goal state after:
case refine_2
ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝ : CardinalInterFilter l✝ c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : s ⊆ t
⊢ t ∈ {s | sᶜ ∈ l}
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case refine_1
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst✝² : CardinalInterFilter l c
l₁ l₂ : Filter α
inst✝¹ : CardinalInterFilter l₁ c
inst✝ : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #↑S < c
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₁

pp: case refine_2
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst✝² : CardinalInterFilter l c
l₁ l₂ : Filter α
inst✝¹ : CardinalInterFilter l₁ c
inst✝ : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #↑S < c
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₂

Tactic:
exacts [(hS s hs).1, (hS s hs).2]

Goal state after:
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst✝² : CardinalInterFilter l c
l₁ l₂ : Filter α
inst✝¹ : CardinalInterFilter l₁ c
inst✝ : CardinalInterFilter l₂ c
⊢ CardinalInterFilter (l₁ ⊔ l₂) c

Tactic:
by
  refine ⟨fun S hSc hS => ⟨?_, ?_⟩⟩ <;> refine (cardinal_sInter_mem hSc).2 fun s hs => ?_
  exacts [(hS s hs).1, (hS s hs).2]

Goal state after:
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤
      { sets := SetRel.image {(s, t) | r.preimage s ⊆ t} l₂.sets, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ } ↔
    ∀ s ∈ l₂, r.preimage s ∈ l₁

Tactic:
;

Goal state after:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤
      { sets := SetRel.image {(s, t) | r.preimage s ⊆ t} l₂.sets, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ } ↔
    ∀ s ∈ l₂, r.preimage s ∈ l₁
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
hc :
  ((⇑(Subtype.relEmbedding (fun x1 x2 ↦ r x1 x2) fun x ↦ x ∈ s) '' univ).chainHeight fun x1 x2 ↦ r x1 x2) =
    univ.chainHeight (Subtype.val ⁻¹'o fun x1 x2 ↦ r x1 x2)
x✝¹ x✝ : { x // x ∈ s }
⊢ (Subtype.val ⁻¹'o fun x1 x2 ↦ r x1 x2) x✝¹ x✝ = r ↑x✝¹ ↑x✝

Tactic:
;

Goal state after:
α : Type u_1
s : Set α
r : α → α → Prop
hc :
  ((⇑(Subtype.relEmbedding (fun x1 x2 ↦ r x1 x2) fun x ↦ x ∈ s) '' univ).chainHeight fun x1 x2 ↦ r x1 x2) =
    univ.chainHeight (Subtype.val ⁻¹'o fun x1 x2 ↦ r x1 x2)
x✝¹ x✝ : { x // x ∈ s }
⊢ (Subtype.val ⁻¹'o fun x1 x2 ↦ r x1 x2) x✝¹ x✝ = r ↑x✝¹ ↑x✝
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
i j : ↑(Icc 0 n)
hij : i < j
x : A
hx : x ∈ B i ∩ B j
⊢ ‖(↑j - ↑i) • ξ‖ ≤ δ

Tactic:
sub_nsmul _ (Subtype.coe_le_coe.mpr hij.le),

Goal state after:
case refine_2
A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
i j : ↑(Icc 0 n)
hij : i < j
x : A
hx : x ∈ B i ∩ B j
⊢ ‖↑j • ξ + -(↑i • ξ)‖ ≤ δ
Module: Mathlib.Order.Interval.Set.SurjOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : f x ∈ Ioo (f a) (f b)
⊢ a < x ∧ x < b

Tactic:
contrapose! hp

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : a < x → b ≤ x
⊢ ¬f x ∈ Ioo (f a) (f b)
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : ⋃ j, B j = univ
hδ : 0 ≤ δ / 2
j : ↑(Icc 0 n)
⊢ (B j).Nonempty

Tactic:
;

Goal state after:
A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : ⋃ j, B j = univ
hδ : 0 ≤ δ / 2
j : ↑(Icc 0 n)
⊢ (B j).Nonempty
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : ⋃ j, B j = univ
hδ : 0 ≤ δ / 2
j : ↑(Icc 0 n)
⊢ (B j).Nonempty

Tactic:
rwa [nonempty_closedBall]

Goal state after:
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
i : ι
⊢ ¬Prod.Lex (fun x1 x2 ↦ x1 < x2) (Prod.Lex (fun x1 x2 ↦ x1 < x2) WellOrderingRel) (f i, g i, i) (f i, g i, i)

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
i : ι
⊢ ¬Prod.Lex (fun x1 x2 ↦ x1 < x2) (Prod.Lex (fun x1 x2 ↦ x1 < x2) WellOrderingRel) (f i, g i, i) (f i, g i, i)
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
i j k : ι
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) (Prod.Lex (fun x1 x2 ↦ x1 < x2) WellOrderingRel) (f i, g i, i) (f j, g j, j) →
    MonovaryOrder f g j k → MonovaryOrder f g i k

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
i j k : ι
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) (Prod.Lex (fun x1 x2 ↦ x1 < x2) WellOrderingRel) (f i, g i, i) (f j, g j, j) →
    MonovaryOrder f g j k → MonovaryOrder f g i k
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝¹ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
i : ℕ
b : α i
h : i ≤ i
x✝ :
  ¬⟨i, π h b⟩ = ⟨i, b⟩ ∧
    ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨i, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨i, b⟩
hne : ¬⟨i, π h b⟩ = ⟨i, b⟩
h' : ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨i, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨i, b⟩
⊢ False

Tactic:
;

Goal state after:
α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝¹ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
i : ℕ
b : α i
h : i ≤ i
x✝ :
  ¬⟨i, π h b⟩ = ⟨i, b⟩ ∧
    ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨i, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨i, b⟩
hne : ¬⟨i, π h b⟩ = ⟨i, b⟩
h' : ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨i, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨i, b⟩
⊢ False
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
i : ℕ
b : α (i + 1)
h : i ≤ i + 1
hij : i ≤ i
hji : i ≤ i + 1
hcb : π hij (π hji b) = π h b
hne : ¬⟨i, π hji b⟩ = ⟨i, π h b⟩
⊢ False

Tactic:
;

Goal state after:
α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
i : ℕ
b : α (i + 1)
h : i ≤ i + 1
hij : i ≤ i
hji : i ≤ i + 1
hcb : π hij (π hji b) = π h b
hne : ¬⟨i, π hji b⟩ = ⟨i, π h b⟩
⊢ False
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : SemilatticeInf X
n m : Nucleus X
x y : X
g : Nucleus X
toFun✝ : X → X
map_inf'✝ : ∀ (a b : X), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
idempotent'✝ :
  ∀ (x : X),
    { toFun := toFun✝, map_inf' := map_inf'✝ }.toFun ({ toFun := toFun✝, map_inf' := map_inf'✝ }.toFun x) ≤
      { toFun := toFun✝, map_inf' := map_inf'✝ }.toFun x
le_apply'✝ : ∀ (x : X), x ≤ { toFun := toFun✝, map_inf' := map_inf'✝ }.toFun x
h :
  (fun x ↦ x.toFun) { toFun := toFun✝, map_inf' := map_inf'✝, idempotent' := idempotent'✝, le_apply' := le_apply'✝ } =
    (fun x ↦ x.toFun) g
⊢ { toFun := toFun✝, map_inf' := map_inf'✝, idempotent' := idempotent'✝, le_apply' := le_apply'✝ } = g

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : SemilatticeInf X
n m : Nucleus X
x y : X
g : Nucleus X
toFun✝ : X → X
map_inf'✝ : ∀ (a b : X), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
idempotent'✝ :
  ∀ (x : X),
    { toFun := toFun✝, map_inf' := map_inf'✝ }.toFun ({ toFun := toFun✝, map_inf' := map_inf'✝ }.toFun x) ≤
      { toFun := toFun✝, map_inf' := map_inf'✝ }.toFun x
le_apply'✝ : ∀ (x : X), x ≤ { toFun := toFun✝, map_inf' := map_inf'✝ }.toFun x
h :
  (fun x ↦ x.toFun) { toFun := toFun✝, map_inf' := map_inf'✝, idempotent' := idempotent'✝, le_apply' := le_apply'✝ } =
    (fun x ↦ x.toFun) g
⊢ { toFun := toFun✝, map_inf' := map_inf'✝, idempotent' := idempotent'✝, le_apply' := le_apply'✝ } = g
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
i : ℕ
a b : α i
hne : ⟨i, a⟩ ≠ ⟨i, b⟩
hij : i ≤ i
h2 : π hij b = a
⊢ False

Tactic:
;

Goal state after:
α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
i : ℕ
a b : α i
hne : ⟨i, a⟩ ≠ ⟨i, b⟩
hij : i ≤ i
h2 : π hij b = a
⊢ False