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

Goal state before:
pp: α β : FinBddDistLat
e : ↑α.toDistLat ≃o ↑β.toDistLat
⊢ ofHom
        (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
      ofHom
        (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) =
    𝟙 α

Tactic:
ext

Goal state after:
α β : FinBddDistLat
e : ↑α.toDistLat ≃o ↑β.toDistLat
a✝ : ↑α.toDistLat
⊢ (Hom.hom
        (ofHom
            (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
          ofHom
            (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })))
      a✝ =
    (Hom.hom (𝟙 α)) a✝
Module: Mathlib.Order.Category.FinBddDistLat

Goal state before:
pp: α β : FinBddDistLat
e : ↑α.toDistLat ≃o ↑β.toDistLat
⊢ ofHom
        (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
      ofHom
        (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) =
    𝟙 β

Tactic:
ext

Goal state after:
α β : FinBddDistLat
e : ↑α.toDistLat ≃o ↑β.toDistLat
a✝ : ↑β.toDistLat
⊢ (Hom.hom
        (ofHom
            (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
          ofHom
            (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })))
      a✝ =
    (Hom.hom (𝟙 β)) a✝
Module: Mathlib.Order.Category.FinBoolAlg

Goal state before:
pp: α β : FinBoolAlg
e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg
⊢ InducedCategory.homMk
        (BoolAlg.ofHom
          (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
          { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })) ≫
      InducedCategory.homMk
        (BoolAlg.ofHom
          (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
          { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })) =
    𝟙 α

Tactic:
ext

Goal state after:
α β : FinBoolAlg
e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg
a✝ : ↑α.toBoolAlg
⊢ (ConcreteCategory.hom
        (InducedCategory.homMk
            (BoolAlg.ofHom
              (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
              { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })) ≫
          InducedCategory.homMk
            (BoolAlg.ofHom
              (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
              { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }))))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝
Module: Mathlib.Order.Category.FinBoolAlg

Goal state before:
pp: α β : FinBoolAlg
e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg
⊢ InducedCategory.homMk
        (BoolAlg.ofHom
          (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
          { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })) ≫
      InducedCategory.homMk
        (BoolAlg.ofHom
          (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
          { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })) =
    𝟙 β

Tactic:
ext

Goal state after:
α β : FinBoolAlg
e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg
a✝ : ↑β.toBoolAlg
⊢ (ConcreteCategory.hom
        (InducedCategory.homMk
            (BoolAlg.ofHom
              (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
              { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })) ≫
          InducedCategory.homMk
            (BoolAlg.ofHom
              (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
              { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }))))
      a✝ =
    (ConcreteCategory.hom (𝟙 β)) a✝
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
e : Lex ((i : ι) → (fun i ↦ α i) i)
he : e ∈ s
⊢ sInf s ≤ e

Tactic:
by_contra! hs
    obtain ⟨a, ha⟩ := hs
    exact ha.2.not_ge (sInf_apply_le he ha.1)

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
x✝ : ↥L
a : α
ha : a ∈ L
⊢ ∃ b, IsCompl ⟨a, ha⟩ b

Tactic:
· obtain ⟨b, hb, hb'⟩ := h a ha
    exact ⟨⟨b, hb⟩, CompleteSublattice.isCompl_iff.mpr hb'⟩

Goal state after:
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
⊢ c.copy e i he hi = c

Tactic:
ext

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.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
⊢ f '' B p ⊆ blimsup (fun n ↦ approxAddOrderOf 𝕊 n (↑p * δ n)) atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n

Tactic:
refine (sSupHom.setImage f).apply_blimsup_le.trans (mono_blimsup ?_)

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
⊢ ∀ (x : ℕ), 0 < x ∧ p ∣ x ∧ ¬p * p ∣ x → (⇑(sSupHom.setImage f) ∘ X) x ⊆ approxAddOrderOf 𝕊 x (↑p * δ x)
Module: Mathlib.Order.Completion

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

Tactic:
ext

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 : α
⊢ Ici a = (ofObject (fun x1 x2 ↦ x1 ≤ x2) a).intent

Tactic:
ext

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 : α
⊢ ofAttribute (fun x1 x2 ↦ x1 ≤ x2) a = principal a

Tactic:
ext

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
inst✝ : CompleteLattice α
A : DedekindCut α
⊢ (principal (sSup A.left)).right = A.right

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ x✝ ∈ (principal (sSup A.left)).right ↔ x✝ ∈ A.right
Module: Mathlib.Order.Completion

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

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ x✝ ∈ (principal (sInf A.right)).left ↔ x✝ ∈ A.left
Module: Mathlib.Order.Completion

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

Tactic:
ext

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
⊢ f = (fun y ↦ x + y) ∘ fun y ↦ p • y

Tactic:
ext

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
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s : Set α
⊢ CountableSupClosed {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a}

Tactic:
constructor

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s : Set α
⊢ ∀ t ⊆ {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a},
    t.Nonempty →
      t.Countable → ∀ (x : α), IsLUB t x → x ∈ {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a}
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
⊢ CountableSupClosed (⋂₀ {t | s ⊆ t ∧ CountableSupClosed t})

Tactic:
constructor

Goal state after:
α : Type u_2
inst✝ : Preorder α
s : Set α
⊢ ∀ t ⊆ ⋂₀ {t | s ⊆ t ∧ CountableSupClosed t},
    t.Nonempty → t.Countable → ∀ (x : α), IsLUB t x → x ∈ ⋂₀ {t | s ⊆ t ∧ CountableSupClosed t}
Module: Mathlib.Order.Filter.ListTraverse

Goal state before:
pp: α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
⊢ t ∈ traverse f fs ↔ ∃ us, Forall₂ (fun b s ↦ s ∈ f b) fs us ∧ sequence us ⊆ t

Tactic:
constructor

Goal state after:
case mp
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
⊢ t ∈ traverse f fs → ∃ us, Forall₂ (fun b s ↦ s ∈ f b) fs us ∧ sequence us ⊆ t

case mpr
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
⊢ (∃ us, Forall₂ (fun b s ↦ s ∈ f b) fs us ∧ sequence us ⊆ t) → t ∈ traverse f fs
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
⊢ s ∈ cardinalGenerate g ⋯ ↔ ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s

Tactic:
constructor

Goal state after:
case mp
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
⊢ s ∈ cardinalGenerate g ⋯ → ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s

case mpr
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
⊢ (∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s) → s ∈ cardinalGenerate g ⋯
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ (∃ a, (∃ a_1 ∈ l, s.core a_1 ⊆ a) ∧ r.core a ⊆ t) ↔ ∃ a ∈ l, r.core (s.core a) ⊆ t

Tactic:
constructor

Goal state after:
case mp
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ (∃ a, (∃ a_1 ∈ l, s.core a_1 ⊆ a) ∧ r.core a ⊆ t) → ∃ a ∈ l, r.core (s.core a) ⊆ t

case mpr
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ (∃ a ∈ l, r.core (s.core a) ⊆ t) → ∃ a, (∃ a_1 ∈ l, s.core a_1 ⊆ a) ∧ r.core a ⊆ t
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂.sets, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂

Tactic:
constructor

Goal state after:
case mp
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂.sets, r.core s ∈ l₁) → l₁ ≤ rcomap r l₂

case mpr
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤ rcomap r l₂ → ∀ s ∈ l₂.sets, r.core s ∈ l₁
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t) ↔ ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t

Tactic:
constructor

Goal state after:
case mp
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t) → ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t

case mpr
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t) → ∃ t_1, (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t
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:
constructor

Goal state after:
case mp
α : 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₁

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
⊢ f ≤ cardinalGenerate g hc ↔ g ⊆ f.sets

Tactic:
constructor

Goal state after:
case mp
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
⊢ f ≤ cardinalGenerate g hc → g ⊆ f.sets

case mpr
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
⊢ g ⊆ f.sets → f ≤ cardinalGenerate g hc
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ 1 ≤ s.chainHeight r ↔ s.Nonempty

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s : Set α
r : α → α → Prop
⊢ 1 ≤ s.chainHeight r → s.Nonempty

case mpr
α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.Nonempty → 1 ≤ s.chainHeight r
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a b : α
n : ℕ
ha : 0 ≤ a
⊢ ↑n ∈ Set.Ioo a b ↔ n ∈ Finset.Ioo ⌊a⌋₊ ⌈b⌉₊

Tactic:
simp [floor_lt ha, lt_ceil]

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
⊢ ∃ f, f 0 = ⊥ ∧ (∀ (i : ℕ), f i ⋖ f (i + 1)) ∧ ∀ (i : ℕ), grade ℕ (f i) = i

Tactic:
by
  obtain ⟨f, h0, hf⟩ := exists_orderEmbedding_covby_of_forall_covby_finite_of_bot hfin
  refine ⟨f, h0, hf, fun i ↦ ?_⟩
  induction i with
  | zero => simp [h0]
  | succ i ih => simpa [Order.covBy_iff_add_one_eq, ih, eq_comm] using CovBy.grade ℕ <| hf i

Goal state after:
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
⊢ n = 0

Tactic:
have h'' : ∀ j, (B j).Nonempty := by intro j; rwa [nonempty_closedBall]

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
h'' : ∀ (j : ↑(Icc 0 n)), (B j).Nonempty
⊢ n = 0
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x✝ y : X
n : Nucleus X
x : X
hx : ↑(rangeFactorization (⇑n) x) ≤ x
⊢ ⟨x, ⋯⟩ = rangeFactorization (⇑n) x

Tactic:
ext

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x✝ y : X
n : Nucleus X
x : X
hx : ↑(rangeFactorization (⇑n) x) ≤ x
⊢ ↑⟨x, ⋯⟩ = ↑(rangeFactorization (⇑n) x)
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
n : Nucleus X
a b : X
⊢ rangeFactorization (⇑n) (a ⊓ b) = rangeFactorization (⇑n) a ⊓ rangeFactorization (⇑n) b

Tactic:
ext

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
n : Nucleus X
a b : X
⊢ ↑(rangeFactorization (⇑n) (a ⊓ b)) = ↑(rangeFactorization (⇑n) a ⊓ rangeFactorization (⇑n) b)
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
n : Nucleus X
⊢ rangeFactorization ⇑n ⊤ = ⊤

Tactic:
ext

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
n : Nucleus X
⊢ ↑(rangeFactorization ⇑n ⊤) = ↑⊤
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
⊢ a₁ ∉ J ∧ a₂ ∉ J → a₁ ⊓ a₂ ∉ J

Tactic:
intro ⟨ha₁, ha₂⟩

Goal state after:
case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
⊢ a₁ ⊓ a₂ ∉ J
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
s t x y z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q : Partition s
P : Partition ⊥
⊢ P = removeBot ∅ ⋯ ⋯

Tactic:
ext

Goal state after:
α : Type u_1
s t x y z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q : Partition s
P : Partition ⊥
x✝ : α
⊢ x✝ ∈ P ↔ x✝ ∈ removeBot ∅ ⋯ ⋯
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b

Tactic:
constructor

Goal state after:
case left
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b

case right
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x y : α
u : Set α
P : Partition u
hx : x ∈ u
hy : y ∈ u
x✝ : P.Rel x y
t : Set α
htP : t ∈ P
hxt : x ∈ t
hyt : y ∈ t
⊢ y ∈ P.partOf x

Tactic:
rwa [← eq_partOf_of_mem htP hxt]

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

Goal state before:
pp: case refine_2
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
a : α
ha : a ∉ u
b : α
⊢ a = f b ↔ a = b

Tactic:
constructor

Goal state after:
case refine_2.mp
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
a : α
ha : a ∉ u
b : α
⊢ a = f b → a = b

case refine_2.mpr
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
a : α
ha : a ∉ u
b : α
⊢ a = b → a = f b
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f g : α → α
hf : P.IsRepFun f
hg : P.IsRepFun g
x : α
⊢ f (g x) = f x

Tactic:
obtain (hx | hx) := em (x ∈ u)

Goal state after:
case inl
α : Type u_1
u : Set α
P : Partition u
f g : α → α
hf : P.IsRepFun f
hg : P.IsRepFun g
x : α
hx : x ∈ u
⊢ f (g x) = f x

case inr
α : Type u_1
u : Set α
P : Partition u
f g : α → α
hf : P.IsRepFun f
hg : P.IsRepFun g
x : α
hx : x ∉ u
⊢ f (g x) = f x