ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<GOAL>1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>H : ι → AddSubgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ<GOAL>1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>H : ι → AddSubgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ<VAR>DecidablePred AddSubgroup.FiniteIndex<GOAL>∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑(Finset.filter (fun i => (H i).FiniteIndex) s)).PairwiseDisjoint fun i => g i +ᵥ ↑(H i)
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<VAR>DecidablePred Subgroup.FiniteIndex<GOAL>∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑(Finset.filter (fun i => (H i).FiniteIndex) s)).PairwiseDisjoint fun i => g i • ↑(H i)
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<GOAL>∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>H : ι → AddSubgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ<GOAL>∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : ι → Submodule R M<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, ↑(p i) = Set.univ<GOAL>∃ k ∈ s, (p k).toAddSubgroup.FiniteIndex
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>DivisionRing k<VAR>Infinite k<VAR>AddCommGroup E<VAR>Module k E<VAR>s : Finset (Subspace k E)<VAR>hs : ∀ p ∈ s, p ≠ ⊤<GOAL>⋃ p ∈ s, ↑p ≠ Set.univ
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>DivisionRing k<VAR>Infinite k<VAR>AddCommGroup E<VAR>Module k E<VAR>s : Finset (Subspace k E)<VAR>hcovers : ⋃ p ∈ s, ↑p = Set.univ<GOAL>∃ p ∈ s, p = ⊤
<VAR>P : Type u_1<VAR>Preorder P<VAR>F : Set P<VAR>nonempty : F.Nonempty<VAR>directed : DirectedOn (fun x x_1 => x ≥ x_1) F<VAR>mem_of_le : ∀ {x y : P}, x ≤ y → x ∈ F → y ∈ F<GOAL>Order.IsPFilter F
<VAR>P : Type u_1<VAR>Preorder P<VAR>F : Order.PFilter P<GOAL>Order.IsPFilter ↑F
<VAR>P : Type u_1<VAR>Preorder P<VAR>F : Order.PFilter P<GOAL>(↑F).Nonempty
<VAR>P : Type u_1<VAR>Preorder P<VAR>F : Order.PFilter P<GOAL>DirectedOn (fun x x_1 => x ≥ x_1) ↑F
<VAR>P : Type u_1<VAR>Preorder P<VAR>x y : P<VAR>F : Order.PFilter P<GOAL>x ≤ y → x ∈ F → y ∈ F
<VAR>P : Type u_1<VAR>Preorder P<VAR>s t : Order.PFilter P<VAR>h : ↑s = ↑t<GOAL>s = t
<VAR>P : Type u_1<VAR>Preorder P<VAR>x : P<VAR>F G : Order.PFilter P<VAR>hx : x ∈ F<VAR>hle : F ≤ G<GOAL>x ∈ G
<VAR>P : Type u_1<VAR>Preorder P<VAR>x : P<VAR>I : Order.Ideal Pᵒᵈ<GOAL>x ∈ { dual := I } ↔ OrderDual.toDual x ∈ I
<VAR>P : Type u_1<VAR>Preorder P<VAR>x : P<VAR>F : Order.PFilter P<GOAL>Order.PFilter.principal x ≤ F ↔ x ∈ F
<VAR>P : Type u_1<VAR>Preorder P<VAR>x y : P<GOAL>x ∈ Order.PFilter.principal y ↔ y ≤ x
<VAR>P : Type u_1<VAR>Preorder P<VAR>p q : P<GOAL>Order.PFilter.principal q ≤ Order.PFilter.principal p ↔ p ≤ q
<VAR>P : Type u_1<VAR>Preorder P<GOAL>Antitone Order.PFilter.principal
<VAR>P : Type u_1<VAR>Preorder P<VAR>OrderTop P<VAR>F : Order.PFilter P<GOAL>⊤ ∈ F
<VAR>P : Type u_1<VAR>SemilatticeInf P<VAR>x y : P<VAR>F : Order.PFilter P<VAR>hx : x ∈ F<VAR>hy : y ∈ F<GOAL>x ⊓ y ∈ F
<VAR>P : Type u_1<VAR>SemilatticeInf P<VAR>x y : P<VAR>F : Order.PFilter P<GOAL>x ⊓ y ∈ F ↔ x ∈ F ∧ y ∈ F
<VAR>P : Type u_1<VAR>CompleteSemilatticeInf P<GOAL>GaloisConnection (fun x => OrderDual.toDual (Order.PFilter.principal x)) fun F => sInf ↑(OrderDual.ofDual F)
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>x y : ℕ → α<VAR>hf : Monotone f<VAR>n : ℕ<VAR>h₀ : x 0 ≤ y 0<VAR>hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)<VAR>hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)<GOAL>x n ≤ y n
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>x y : ℕ → α<VAR>hf : Monotone f<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h₀ : x 0 ≤ y 0<VAR>hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)<VAR>hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)<GOAL>x n < y n
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>x y : ℕ → α<VAR>hf : Monotone f<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h₀ : x 0 ≤ y 0<VAR>hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)<VAR>hy : ∀ (k : ℕ), k < n → f (y k) < y (k + 1)<GOAL>x n < y n
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>x y : ℕ → α<VAR>hf : Monotone f<VAR>n : ℕ<VAR>h₀ : x 0 < y 0<VAR>hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)<VAR>hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)<GOAL>x n < y n
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>x y : ℕ → α<VAR>hf : Monotone f<VAR>n : ℕ<VAR>h₀ : x 0 < y 0<VAR>hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)<VAR>hy : ∀ (k : ℕ), k < n → f (y k) < y (k + 1)<GOAL>x n < y n
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>β : Type u_2<VAR>g : β → β<VAR>h : β → α<VAR>hf : Monotone f<VAR>H : h ∘ g ≤ f ∘ h<VAR>n : ℕ<GOAL>h ∘ g^[n] ≤ f^[n] ∘ h
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>β : Type u_2<VAR>g : β → β<VAR>h : β → α<VAR>hf : Monotone f<VAR>H : f ∘ h ≤ h ∘ g<VAR>n : ℕ<GOAL>f^[n] ∘ h ≤ h ∘ g^[n]
<VAR>α : Type u_1<VAR>Preorder α<VAR>f g : α → α<VAR>hf : Monotone f<VAR>h : f ≤ g<VAR>n : ℕ<GOAL>f^[n] ≤ g^[n]
<VAR>α : Type u_1<VAR>Preorder α<VAR>f g : α → α<VAR>hg : Monotone g<VAR>h : f ≤ g<VAR>n : ℕ<GOAL>f^[n] ≤ g^[n]
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>h : id ≤ f<VAR>n : ℕ<GOAL>id ≤ f^[n]
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>h : f ≤ id<VAR>n : ℕ<GOAL>f^[n] ≤ id
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>h : id ≤ f<GOAL>Monotone fun m => f^[m]
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>h : f ≤ id<GOAL>Antitone fun m => f^[m]
<VAR>α : Type u_1<VAR>Preorder α<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>hf : Monotone f<VAR>hg : Monotone g<VAR>x : α<VAR>hx : f x ≤ g x<VAR>n : ℕ<GOAL>f^[n] x ≤ g^[n] x
<VAR>α : Type u_1<VAR>Preorder α<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>x : α<VAR>hx : f x < g x<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[n] x < g^[n] x
<VAR>α : Type u_1<VAR>Preorder α<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>hf : StrictMono f<VAR>hg : Monotone g<VAR>x : α<VAR>hx : f x < g x<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[n] x < g^[n] x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[n] x < g^[n] x ↔ f x < g x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>hf : StrictMono f<VAR>hg : Monotone g<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[n] x < g^[n] x ↔ f x < g x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[n] x ≤ g^[n] x ↔ f x ≤ g x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>hf : StrictMono f<VAR>hg : Monotone g<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[n] x ≤ g^[n] x ↔ f x ≤ g x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[n] x = g^[n] x ↔ f x = g x
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>x : α<VAR>hf : Monotone f<VAR>hx : x ≤ f x<GOAL>Monotone fun n => f^[n] x
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>x : α<VAR>hf : Monotone f<VAR>hx : f x ≤ x<GOAL>Antitone fun n => f^[n] x
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>x : α<VAR>hf : StrictMono f<VAR>hx : x < f x<GOAL>StrictMono fun n => f^[n] x
<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → α<VAR>x : α<VAR>hf : StrictMono f<VAR>hx : f x < x<GOAL>StrictAnti fun n => f^[n] x
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>f : ℕ → α<GOAL>(partialSups f) 0 = f 0
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>f : ℕ → α<VAR>n : ℕ<GOAL>(partialSups f) (n + 1) = (partialSups f) n ⊔ f (n + 1)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>f : ℕ → α<VAR>p : α → Prop<VAR>hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b<VAR>n : ℕ<GOAL>p ((partialSups f) n) ↔ ∀ k ≤ n, p (f k)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>f : ℕ → α<VAR>n : ℕ<VAR>a : α<GOAL>(partialSups f) n ≤ a ↔ ∀ k ≤ n, f k ≤ a
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>f : ℕ → α<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>f m ≤ (partialSups f) n
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>f : ℕ → α<GOAL>f ≤ ⇑(partialSups f)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>f : ℕ → α<VAR>n : ℕ<VAR>a : α<VAR>w : ∀ m ≤ n, f m ≤ a<GOAL>(partialSups f) n ≤ a
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>f : ℕ → α<GOAL>upperBounds (Set.range ⇑(partialSups f)) = upperBounds (Set.range f)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>f : ℕ → α<GOAL>BddAbove (Set.range ⇑(partialSups f)) ↔ BddAbove (Set.range f)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>f : ℕ → α<VAR>hf : Monotone f<GOAL>⇑(partialSups f) = f
<VAR>α : Type u_1<VAR>SemilatticeSup α<GOAL>Monotone partialSups
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>f : ℕ → α<VAR>n : ℕ<GOAL>(partialSups f) n = (Finset.range (n + 1)).sup' ⋯ f
<VAR>ι : Type u_2<VAR>π : ι → Type u_3<VAR>(i : ι) → SemilatticeSup (π i)<VAR>f : ℕ → (i : ι) → π i<VAR>n : ℕ<VAR>i : ι<GOAL>(partialSups f) n i = (partialSups fun x => f x i) n
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>f : ℕ → α<VAR>n : ℕ<GOAL>(partialSups f) n = (Finset.range (n + 1)).sup f
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>f : ℕ → α<VAR>n : ℕ<VAR>x : α<GOAL>Disjoint ((partialSups f) n) x ↔ ∀ k ≤ n, Disjoint (f k) x
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>f : ℕ → α<VAR>n : ℕ<VAR>x : α<GOAL>Disjoint x ((partialSups f) n) ↔ ∀ k ≤ n, Disjoint x (f k)
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>f : ℕ → α<VAR>h : Pairwise (Disjoint on f)<VAR>m n : ℕ<VAR>hmn : m < n<GOAL>Disjoint ((partialSups f) m) (f n)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>f : ℕ → α<VAR>n : ℕ<GOAL>(partialSups f) n = ⨆ i, f ↑i
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>f : ℕ → α<VAR>h : BddAbove (Set.range f)<GOAL>⨆ n, (partialSups f) n = ⨆ n, f n
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : ℕ → α<VAR>n : ℕ<GOAL>(partialSups f) n = ⨆ i, ⨆ (_ : i ≤ n), f i
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : ℕ → α<GOAL>⨆ n, (partialSups f) n = ⨆ n, f n
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f g : ℕ → α<VAR>h : partialSups f ≤ partialSups g<GOAL>⨆ n, f n ≤ ⨆ n, g n
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f g : ℕ → α<VAR>h : partialSups f = partialSups g<GOAL>⨆ n, f n = ⨆ n, g n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>Preorder β<VAR>f : α → β<GOAL>IsOrderRightAdjoint f fun y => sSup {x | f x ≤ y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>Preorder β<VAR>f : α → β<VAR>hne : ∀ (y : β), ∃ x, f x ≤ y<VAR>hbdd : ∀ (y : β), BddAbove {x | f x ≤ y}<GOAL>IsOrderRightAdjoint f fun y => sSup {x | f x ≤ y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>Preorder β<VAR>f : α → β<VAR>g₁ g₂ : β → α<VAR>h₁ : IsOrderRightAdjoint f g₁<VAR>h₂ : IsOrderRightAdjoint f g₂<GOAL>g₁ = g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>g : β → α<VAR>h : IsOrderRightAdjoint f g<GOAL>Monotone g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>g : β → α<VAR>h : IsOrderRightAdjoint f g<VAR>e : β ≃o γ<GOAL>IsOrderRightAdjoint (⇑e ∘ f) (g ∘ ⇑e.symm)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>g : β → α<VAR>h : IsOrderRightAdjoint f g<VAR>e : γ ≃o α<GOAL>IsOrderRightAdjoint (f ∘ ⇑e) (⇑e.symm ∘ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>Preorder β<VAR>fa : α ≃o α<VAR>fb : β ↪o β<VAR>g : α → β<VAR>h : Function.Semiconj g ⇑fa ⇑fb<VAR>g' : β → α<VAR>hg' : IsOrderRightAdjoint g g'<GOAL>Function.Semiconj g' ⇑fb ⇑fa
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>PartialOrder α<VAR>Group G<VAR>f₁ f₂ : G →* α ≃o α<VAR>h : α → α<VAR>H : ∀ (x : α), IsLUB (Set.range fun g' => (f₁ g')⁻¹ ((f₂ g') x)) (h x)<VAR>g : G<GOAL>Function.Semiconj h ⇑(f₂ g) ⇑(f₁ g)
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>CompleteLattice α<VAR>Group G<VAR>f₁ f₂ : G →* α ≃o α<VAR>g : G<GOAL>Function.Semiconj (fun x => ⨆ g', (f₁ g')⁻¹ ((f₂ g') x)) ⇑(f₂ g) ⇑(f₁ g)
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>ConditionallyCompleteLattice α<VAR>Group G<VAR>f₁ f₂ : G →* α ≃o α<VAR>hbdd : ∀ (x : α), BddAbove (Set.range fun g => (f₁ g)⁻¹ ((f₂ g) x))<VAR>g : G<GOAL>Function.Semiconj (fun x => ⨆ g', (f₁ g')⁻¹ ((f₂ g') x)) ⇑(f₂ g) ⇑(f₁ g)
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>self : r →r s<VAR>a b : α<GOAL>r a b → s (self.toFun a) (self.toFun b)
<VAR>F : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>r : outParam (α → α → Prop)<VAR>s : outParam (β → β → Prop)<VAR>FunLike F α β<VAR>self : RelHomClass F r s<VAR>f : F<VAR>a b : α<GOAL>r a b → s (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>F : Type u_5<VAR>FunLike F α β<VAR>RelHomClass F r s<VAR>f : F<VAR>IsIrrefl β s<GOAL>IsIrrefl α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>F : Type u_5<VAR>FunLike F α β<VAR>RelHomClass F r s<VAR>f : F<VAR>IsAsymm β s<GOAL>IsAsymm α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>F : Type u_5<VAR>FunLike F α β<VAR>RelHomClass F r s<VAR>f : F<VAR>a : α<GOAL>Acc s (f a) → Acc r a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>F : Type u_5<VAR>FunLike F α β<VAR>RelHomClass F r s<VAR>f : F<GOAL>WellFounded s → WellFounded r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r →r s<VAR>a b : α<GOAL>r a b → s (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r →r s<GOAL>f.toFun = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<GOAL>Function.Injective fun f => ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f g : r →r s<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f g : r →r s<GOAL>f = g ↔ ∀ (x : α), f x = g x
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>x : α<GOAL>(RelHom.id r) x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>g : s →r t<VAR>f : r →r s<VAR>x : α<GOAL>(g.comp f) x = g (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsTrichotomous α r<VAR>IsIrrefl β s<VAR>f : α → β<VAR>hf : ∀ {x y : α}, r x y → s (f x) (f y)<GOAL>Function.Injective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsTrichotomous α r<VAR>IsIrrefl β s<VAR>f : r →r s<GOAL>Function.Injective ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>o : ∀ {a b : α}, r a b ↔ s (f a) (f b)<GOAL>WellFounded r ↔ WellFounded s
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>self : r ↪r s<VAR>a b : α<GOAL>s (self.toEmbedding a) (self.toEmbedding b) ↔ r a b
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>f : α → β<VAR>s : β → β → Prop<VAR>hs : Equivalence s<GOAL>Equivalence (f ⁻¹'o s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<GOAL>⇑f.toEmbedding = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<GOAL>⇑f.toRelHom = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<GOAL>Function.Injective ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>a b : α<GOAL>f a = f b ↔ a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>a b : α<GOAL>s (f a) (f b) ↔ r a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : α ↪ β<VAR>h : ∀ {a b : α}, s (f a) (f b) ↔ r a b<GOAL>⇑{ toEmbedding := f, map_rel_iff' := h } = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f g : r ↪r s<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f g : r ↪r s<GOAL>f = g ↔ ∀ (x : α), f x = g x
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : α<GOAL>(RelEmbedding.refl r) a = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : r ↪r s<VAR>g : s ↪r t<VAR>a : α<GOAL>(f.trans g) a = g (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : r ↪r s<VAR>g : s ↪r t<GOAL>⇑(f.trans g) = ⇑g ∘ ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<GOAL>r = ⇑f ⁻¹'o s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>IsIrrefl β s<GOAL>IsIrrefl α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>IsRefl β s<GOAL>IsRefl α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>IsSymm β s<GOAL>IsSymm α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>IsAsymm β s<GOAL>IsAsymm α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<GOAL>r ↪r s → ∀ [inst : IsAntisymm β s], IsAntisymm α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<GOAL>r ↪r s → ∀ [inst : IsTrans β s], IsTrans α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<GOAL>r ↪r s → ∀ [inst : IsTotal β s], IsTotal α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<GOAL>r ↪r s → ∀ [inst : IsPreorder β s], IsPreorder α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<GOAL>r ↪r s → ∀ [inst : IsPartialOrder β s], IsPartialOrder α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<GOAL>r ↪r s → ∀ [inst : IsLinearOrder β s], IsLinearOrder α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<GOAL>r ↪r s → ∀ [inst : IsStrictOrder β s], IsStrictOrder α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<GOAL>r ↪r s → ∀ [inst : IsTrichotomous β s], IsTrichotomous α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<GOAL>r ↪r s → ∀ [inst : IsStrictTotalOrder β s], IsStrictTotalOrder α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>a : α<GOAL>Acc s (f a) → Acc r a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<GOAL>r ↪r s → WellFounded s → WellFounded r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>IsWellFounded β s<GOAL>IsWellFounded α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<GOAL>r ↪r s → ∀ [inst : IsWellOrder β s], IsWellOrder α r
<VAR>α : Type u_1<VAR>Setoid α<VAR>r : α → α → Prop<VAR>H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂<VAR>a : α<GOAL>(Quotient.mkRelHom H) a = Quotient.mk' a
<VAR>α : Type u_1<VAR>Setoid α<VAR>r : α → α → Prop<VAR>H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂<GOAL>∀ (a : Quotient inst✝), (Quotient.outRelEmbedding H) a = a.out
<VAR>α : Type u_1<GOAL>∀ {x : Setoid α} {r : α → α → Prop} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) (a : Quotient x), (Quotient.out'RelEmbedding H) a = a.out'
<VAR>α : Type u_1<VAR>Setoid α<VAR>r : α → α → Prop<VAR>H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂<VAR>a : α<GOAL>Acc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a
<VAR>α : Type u_1<VAR>s : Setoid α<VAR>r : α → α → Prop<VAR>H : ∀ (a₁ a₂ b₁ b₂ : α), Setoid.r a₁ b₁ → Setoid.r a₂ b₂ → r a₁ a₂ = r b₁ b₂<VAR>a : α<GOAL>Acc (fun x y => x.liftOn₂' y r H) (Quotient.mk'' a) ↔ Acc r a
<VAR>α : Type u_1<VAR>Setoid α<VAR>r : α → α → Prop<VAR>H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂<GOAL>WellFounded (Quotient.lift₂ r H) ↔ WellFounded r
<VAR>α : Type u_1<VAR>s : Setoid α<VAR>r : α → α → Prop<VAR>H : ∀ (a₁ a₂ b₁ b₂ : α), Setoid.r a₁ b₁ → Setoid.r a₂ b₂ → r a₁ a₂ = r b₁ b₂<GOAL>(WellFounded fun x y => x.liftOn₂' y r H) ↔ WellFounded r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : α → β<VAR>IsAntisymm α r<VAR>IsRefl β s<VAR>hf : ∀ (a b : α), s (f a) (f b) ↔ r a b<GOAL>⇑(RelEmbedding.ofMapRelIff f hf) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsTrichotomous α r<VAR>IsAsymm β s<VAR>f : α → β<VAR>H : ∀ (a b : α), r a b → s (f a) (f b)<GOAL>⇑(RelEmbedding.ofMonotone f H) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>val : α<GOAL>(RelEmbedding.sumLiftRelInl r s) val = Sum.inl val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>val : β<GOAL>(RelEmbedding.sumLiftRelInr r s) val = Sum.inr val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>f : r ↪r s<VAR>g : t ↪r u<GOAL>∀ (a : α ⊕ γ), (f.sumLiftRelMap g) a = Sum.map (⇑f) (⇑g) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>val : α<GOAL>(RelEmbedding.sumLexInl r s) val = Sum.inl val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>val : β<GOAL>(RelEmbedding.sumLexInr r s) val = Sum.inr val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>f : r ↪r s<VAR>g : t ↪r u<GOAL>∀ (a : α ⊕ γ), (f.sumLexMap g) a = Sum.map (⇑f) (⇑g) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>a : α<VAR>h : ¬r a a<VAR>snd : β<GOAL>(RelEmbedding.prodLexMkLeft s h) snd = (a, snd)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : β → β → Prop<VAR>r : α → α → Prop<VAR>b : β<VAR>h : ¬s b b<VAR>a : α<GOAL>(RelEmbedding.prodLexMkRight r h) a = (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>f : r ↪r s<VAR>g : t ↪r u<GOAL>∀ (a : α × γ), (f.prodLexMap g) a = Prod.map (⇑f) (⇑g) a
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>self : r ≃r s<VAR>a b : α<GOAL>s (self.toEquiv a) (self.toEquiv b) ↔ r a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<GOAL>Function.Injective RelIso.toEquiv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≃r s<GOAL>⇑f.toRelEmbedding = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≃r s<GOAL>⇑f.toEmbedding = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≃r s<VAR>a b : α<GOAL>s (f a) (f b) ↔ r a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : α ≃ β<VAR>o : ∀ ⦃a b : α⦄, s (f a) (f b) ↔ r a b<GOAL>⇑{ toEquiv := f, map_rel_iff' := o } = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≃r s<GOAL>⇑f.toEquiv = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f g : r ≃r s<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f g : r ≃r s<GOAL>f = g ↔ ∀ (x : α), f x = g x
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : α<GOAL>(RelIso.refl r) a = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f₁ : r ≃r s<VAR>f₂ : s ≃r t<GOAL>∀ (a : α), (f₁.trans f₂) a = f₂ (f₁ a)
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>default = RelIso.refl r
<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>h₁ : α = β<VAR>h₂ : HEq r s<GOAL>(RelIso.cast h₁ h₂).toEquiv = Equiv.cast h₁