ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>α β : TypeVec.{u_1} n<GOAL>TypeVec.prod.map TypeVec.id TypeVec.id = TypeVec.id
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<GOAL>TypeVec.comp (TypeVec.subtypeVal α.repeatEq) TypeVec.diagSub = TypeVec.prod.diag
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>p : α.Arrow (TypeVec.repeat n Prop)<GOAL>TypeVec.comp (TypeVec.toSubtype p) (TypeVec.ofSubtype p) = TypeVec.id
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>p : α.Arrow (TypeVec.repeat n Prop)<GOAL>TypeVec.comp (TypeVec.subtypeVal p) (TypeVec.toSubtype p) = fun x => Subtype.val
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>β : TypeVec.{u_2} n<VAR>p : α.Arrow (TypeVec.repeat n Prop)<VAR>f : β.Arrow (TypeVec.Subtype_ p)<GOAL>TypeVec.comp (TypeVec.toSubtype p) (TypeVec.comp (TypeVec.ofSubtype p) f) = f
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>r : (α.prod α).Arrow (TypeVec.repeat n Prop)<GOAL>TypeVec.comp (TypeVec.toSubtype' r) (TypeVec.ofSubtype' r) = TypeVec.id
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>r : (α.prod α).Arrow (TypeVec.repeat n Prop)<GOAL>TypeVec.comp (TypeVec.subtypeVal r) (TypeVec.toSubtype' r) = fun i x => TypeVec.prod.mk i (↑x).1 (↑x).2
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<VAR>a : (i : ι) × α i<GOAL>a ∈ s.sigma t ↔ a.fst ∈ s ∧ a.snd ∈ t a.fst
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<GOAL>↑(s.sigma t) = (↑s).sigma fun i => ↑(t i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<GOAL>(s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<GOAL>s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s₁ s₂ : Finset ι<VAR>t₁ t₂ : (i : ι) → Finset (α i)<VAR>hs : s₁ ⊆ s₂<VAR>ht : ∀ (i : ι), t₁ i ⊆ t₂ i<GOAL>s₁.sigma t₁ ⊆ s₂.sigma t₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<GOAL>(↑s).PairwiseDisjoint fun i => Finset.map (Function.Embedding.sigmaMk i) (t i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<GOAL>s.disjiUnion (fun i => Finset.map (Function.Embedding.sigmaMk i) (t i)) ⋯ = s.sigma t
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ((i : ι) × α i)<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<GOAL>s.sigma t = s.biUnion fun i => Finset.map (Function.Embedding.sigmaMk i) (t i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<VAR>f : (i : ι) × α i → β<VAR>SemilatticeSup β<VAR>OrderBot β<GOAL>(s.sigma t).sup f = s.sup fun i => (t i).sup fun b => f ⟨i, b⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<VAR>f : (i : ι) × α i → β<VAR>SemilatticeInf β<VAR>OrderTop β<GOAL>(s.sigma t).inf f = s.inf fun i => (t i).inf fun b => f ⟨i, b⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<VAR>f : Sigma α → β<GOAL>⨆ ij ∈ s.sigma t, f ij = ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<VAR>f : (i : ι) → α i → β<GOAL>⨆ i ∈ s, ⨆ j ∈ t i, f i j = ⨆ ij ∈ s.sigma t, f ij.fst ij.snd
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<VAR>f : Sigma α → β<GOAL>⨅ ij ∈ s.sigma t, f ij = ⨅ i ∈ s, ⨅ j ∈ t i, f ⟨i, j⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>CompleteLattice β<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<VAR>f : (i : ι) → α i → β<GOAL>⨅ i ∈ s, ⨅ j ∈ t i, f i j = ⨅ ij ∈ s.sigma t, f ij.fst ij.snd
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<VAR>f : Sigma α → Set β<GOAL>⋃ ij ∈ s.sigma t, f ij = ⋃ i ∈ s, ⋃ j ∈ t i, f ⟨i, j⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<VAR>f : (i : ι) → α i → Set β<GOAL>⋃ i ∈ s, ⋃ j ∈ t i, f i j = ⋃ ij ∈ s.sigma t, f ij.fst ij.snd
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<VAR>f : Sigma α → Set β<GOAL>⋂ ij ∈ s.sigma t, f ij = ⋂ i ∈ s, ⋂ j ∈ t i, f ⟨i, j⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<VAR>f : (i : ι) → α i → Set β<GOAL>⋂ i ∈ s, ⋂ j ∈ t i, f i j = ⋂ ij ∈ s.sigma t, f ij.fst ij.snd
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>a : Sigma α<VAR>b : Sigma β<VAR>x : Sigma γ<GOAL>x ∈ Finset.sigmaLift f a b ↔ ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>i : ι<VAR>a : α i<VAR>b : β i<VAR>x : γ i<GOAL>⟨i, x⟩ ∈ Finset.sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔ x ∈ f a b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>a : Sigma α<VAR>b : Sigma β<VAR>x : Sigma γ<VAR>h : a.fst ≠ x.fst<GOAL>x ∉ Finset.sigmaLift f a b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>a : Sigma α<VAR>b : Sigma β<VAR>x : Sigma γ<VAR>h : b.fst ≠ x.fst<GOAL>x ∉ Finset.sigmaLift f a b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>a : (i : ι) × α i<VAR>b : (i : ι) × β i<GOAL>(Finset.sigmaLift f a b).Nonempty ↔ ∃ (h : a.fst = b.fst), (f (h ▸ a.snd) b.snd).Nonempty
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>a : (i : ι) × α i<VAR>b : (i : ι) × β i<GOAL>Finset.sigmaLift f a b = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>DecidableEq ι<VAR>f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b<VAR>a : (i : ι) × α i<VAR>b : (i : ι) × β i<GOAL>Finset.sigmaLift f a b ⊆ Finset.sigmaLift g a b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>a : (i : ι) × α i<VAR>b : (i : ι) × β i<GOAL>(Finset.sigmaLift f a b).card = if h : a.fst = b.fst then (f (h ▸ a.snd) b.snd).card else 0
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>x : Subtype p<GOAL>p ↑x
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>q : { a // p a } → Prop<GOAL>(∀ (x : { a // p a }), q x) ↔ ∀ (a : α) (b : p a), q ⟨a, b⟩
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>q : (x : α) → p x → Prop<GOAL>(∀ (x : α) (h : p x), q x h) ↔ ∀ (x : { a // p a }), q ↑x ⋯
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>q : { a // p a } → Prop<GOAL>(∃ x, q x) ↔ ∃ a b, q ⟨a, b⟩
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>q : (x : α) → p x → Prop<GOAL>(∃ x h, q x h) ↔ ∃ x, q ↑x ⋯
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a1 a2 : { x // p x }<GOAL>↑a1 = ↑a2 → a1 = a2
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a1 a2 : { x // p x }<GOAL>a1 = a2 ↔ ↑a1 = ↑a2
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>h : ∀ (x : α), p x ↔ q x<VAR>a1 : { x // p x }<VAR>a2 : { x // q x }<GOAL>HEq a1 a2 ↔ ↑a1 = ↑a2
<VAR>α β : Sort u_4<VAR>p : α → Prop<VAR>q : β → Prop<VAR>a : { x // p x }<VAR>b : { y // q y }<VAR>h : α = β<VAR>h' : HEq p q<GOAL>HEq a b ↔ HEq ↑a ↑b
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a : { a // p a }<VAR>h : p ↑a<GOAL>⟨↑a, h⟩ = a
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a : α<VAR>h : p a<GOAL>↑⟨a, h⟩ = a
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a : α<VAR>h : p a<VAR>a' : α<VAR>h' : p a'<GOAL>⟨a, h⟩ = ⟨a', h'⟩ ↔ a = a'
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a : { a // p a }<VAR>b : α<VAR>h : ↑a = b<GOAL>a = ⟨b, ⋯⟩
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a : { a // p a }<VAR>b : α<GOAL>↑a = b ↔ ∃ h, a = ⟨b, h⟩
<VAR>α : Sort u_1<VAR>p : α → Prop<GOAL>Function.Injective fun a => ↑a
<VAR>α : Sort u_1<VAR>p : α → Prop<GOAL>Function.Injective Subtype.val
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a b : Subtype p<GOAL>↑a = ↑b ↔ a = b
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a b : Subtype p<GOAL>↑a ≠ ↑b ↔ a ≠ b
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a : Subtype p<VAR>b : α<GOAL>(∃ h, a = ⟨b, h⟩) ↔ ↑a = b
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a : Subtype p<VAR>b : α<GOAL>(∃ h, ⟨b, h⟩ = a) ↔ b = ↑a
<VAR>α : Sort u_5<VAR>β : α → Type u_4<VAR>f : (x : α) → β x<VAR>p : α → Prop<VAR>x : Subtype p<GOAL>Subtype.restrict p f x = f ↑x
<VAR>α : Sort u_4<VAR>β : Type u_5<VAR>f : α → β<VAR>p : α → Prop<GOAL>Subtype.restrict p f = f ∘ fun a => ↑a
<VAR>α : Sort u_4<VAR>β : Type u_5<VAR>f : α → β<VAR>p : α → Prop<VAR>h : Function.Injective f<GOAL>Function.Injective (Subtype.restrict p f)
<VAR>α : Sort u_5<VAR>β : α → Type u_4<VAR>ne : ∀ (a : α), Nonempty (β a)<VAR>p : α → Prop<GOAL>Function.Surjective fun f => Subtype.restrict p f
<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>f : α → β<VAR>p : β → Prop<VAR>h : ∀ (a : α), p (f a)<GOAL>∀ (a : α), ↑(Subtype.coind f h a) = f a
<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>f : α → β<VAR>p : β → Prop<VAR>h : ∀ (a : α), p (f a)<VAR>hf : Function.Injective f<GOAL>Function.Injective (Subtype.coind f h)
<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>f : α → β<VAR>p : β → Prop<VAR>h : ∀ (a : α), p (f a)<VAR>hf : Function.Surjective f<GOAL>Function.Surjective (Subtype.coind f h)
<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>f : α → β<VAR>p : β → Prop<VAR>h : ∀ (a : α), p (f a)<VAR>hf : Function.Bijective f<GOAL>Function.Bijective (Subtype.coind f h)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : α → Prop<VAR>q : β → Prop<VAR>f : α → β<VAR>h : ∀ (a : α), p a → q (f a)<GOAL>∀ (a : Subtype p), ↑(Subtype.map f h a) = f ↑a
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : α → Prop<VAR>q : β → Prop<VAR>f : α → β<VAR>h : ∀ (a : α), p a → q (f a)<GOAL>Subtype.map f h = fun x => ⟨f ↑x, ⋯⟩
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<VAR>x : Subtype p<VAR>f : α → β<VAR>h : ∀ (a : α), p a → q (f a)<VAR>g : β → γ<VAR>l : ∀ (a : β), q a → r (g a)<GOAL>Subtype.map g l (Subtype.map f h x) = Subtype.map (g ∘ f) ⋯ x
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>h : ∀ (a : α), p a → p (id a)<GOAL>Subtype.map id h = id
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : α → Prop<VAR>q : β → Prop<VAR>f : α → β<VAR>h : ∀ (a : α), p a → q (f a)<VAR>hf : Function.Injective f<GOAL>Function.Injective (Subtype.map f h)
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>f : α → α<VAR>h : ∀ (a : α), p a → p (f a)<VAR>hf : Function.Involutive f<GOAL>Function.Involutive (Subtype.map f h)
<VAR>α : Sort u_1<VAR>HasEquiv α<VAR>p : α → Prop<VAR>s t : Subtype p<GOAL>s ≈ t ↔ ↑s ≈ ↑t
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>Setoid α<VAR>s : Subtype p<GOAL>s ≈ s
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>Setoid α<VAR>s t : Subtype p<VAR>h : s ≈ t<GOAL>t ≈ s
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>Setoid α<VAR>s t u : Subtype p<VAR>h₁ : s ≈ t<VAR>h₂ : t ≈ u<GOAL>s ≈ u
<VAR>α : Sort u_1<VAR>Setoid α<VAR>p : α → Prop<GOAL>Equivalence HasEquiv.Equiv
<VAR>α : Type u_1<VAR>S : Set α<VAR>a : { a // a ∈ S }<GOAL>↑a ∈ S
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>a₁ a₂ : α<VAR>b₁ : β a₁<VAR>b₂ : β a₂<GOAL>⟨a₁, b₁⟩ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ HEq b₁ b₂
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>x : (a : α) × β a<GOAL>⟨x.fst, x.snd⟩ = x
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>x₀ x₁ : Sigma β<GOAL>x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ HEq x₀.snd x₁.snd
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>γ : Type u_7<VAR>Nonempty γ<VAR>a b : α<VAR>f : γ → β a<VAR>g : γ → β b<VAR>h : Sigma.mk a ∘ f = Sigma.mk b ∘ g<GOAL>a = b ∧ HEq f g
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>p : α → β → Prop<VAR>x₀ x₁ : (a : α) × Subtype (p a)<GOAL>x₀.fst = x₁.fst → x₀.snd.val = x₁.snd.val → x₀ = x₁
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>p : α → β → Prop<VAR>x₀ x₁ : (a : α) × Subtype (p a)<GOAL>x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ x₀.snd.val = x₁.snd.val
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>p : (a : α) × β a → Prop<GOAL>(∀ (x : (a : α) × β a), p x) ↔ ∀ (a : α) (b : β a), p ⟨a, b⟩
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>p : (a : α) × β a → Prop<GOAL>(∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>p : (a : α) → β a → Prop<GOAL>(∃ a b, p a b) ↔ ∃ x, p x.fst x.snd
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>p : (a : α) → β a → Prop<GOAL>(∀ (a : α) (b : β a), p a b) ↔ ∀ (x : (a : α) × β a), p x.fst x.snd
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>i : α<GOAL>Function.Injective (Sigma.mk i)
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>h : ∀ (a : α), Nonempty (β a)<GOAL>Function.Surjective Sigma.fst
<VAR>α : Type u_1<VAR>β : α → Type u_4<GOAL>Function.Surjective Sigma.fst ↔ ∀ (a : α), Nonempty (β a)
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>h : ∀ (a : α), Subsingleton (β a)<GOAL>Function.Injective Sigma.fst
<VAR>α : Type u_1<VAR>β : α → Type u_4<GOAL>Function.Injective Sigma.fst ↔ ∀ (a : α), Subsingleton (β a)
<VAR>α₁ : Type u_2<VAR>α₂ : Type u_3<VAR>β₁ : α₁ → Type u_5<VAR>β₂ : α₂ → Type u_6<VAR>f₁ : α₁ → α₂<VAR>f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)<VAR>x : α₁<VAR>y : β₁ x<GOAL>Sigma.map f₁ f₂ ⟨x, y⟩ = ⟨f₁ x, f₂ x y⟩
<VAR>α₁ : Type u_2<VAR>α₂ : Type u_3<VAR>β₁ : α₁ → Type u_5<VAR>β₂ : α₂ → Type u_6<VAR>f₁ : α₁ → α₂<VAR>f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)<VAR>h₁ : Function.Injective f₁<VAR>h₂ : ∀ (a : α₁), Function.Injective (f₂ a)<GOAL>Function.Injective (Sigma.map f₁ f₂)
<VAR>α₁ : Type u_2<VAR>α₂ : Type u_3<VAR>β₁ : α₁ → Type u_5<VAR>β₂ : α₂ → Type u_6<VAR>f₁ : α₁ → α₂<VAR>f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)<VAR>h : Function.Injective (Sigma.map f₁ f₂)<VAR>a : α₁<GOAL>Function.Injective (f₂ a)
<VAR>α₁ : Type u_2<VAR>α₂ : Type u_3<VAR>β₁ : α₁ → Type u_5<VAR>β₂ : α₂ → Type u_6<VAR>f₁ : α₁ → α₂<VAR>f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)<VAR>h₁ : Function.Injective f₁<GOAL>Function.Injective (Sigma.map f₁ f₂) ↔ ∀ (a : α₁), Function.Injective (f₂ a)
<VAR>α₁ : Type u_2<VAR>α₂ : Type u_3<VAR>β₁ : α₁ → Type u_5<VAR>β₂ : α₂ → Type u_6<VAR>f₁ : α₁ → α₂<VAR>f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)<VAR>h₁ : Function.Surjective f₁<VAR>h₂ : ∀ (a : α₁), Function.Surjective (f₂ a)<GOAL>Function.Surjective (Sigma.map f₁ f₂)
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_7<VAR>f : (x : Sigma β) → γ x.fst x.snd<GOAL>Sigma.uncurry (Sigma.curry f) = f
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_7<VAR>f : (x : α) → (y : β x) → γ x y<GOAL>Sigma.curry (Sigma.uncurry f) = f
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_7<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (β a)<VAR>i : (a : α) × β a<VAR>f : (i : (a : α) × β a) → γ i.fst i.snd<VAR>x : γ i.fst i.snd<GOAL>Sigma.curry (Function.update f i x) = Function.update (Sigma.curry f) i.fst (Function.update (Sigma.curry f i.fst) i.snd x)
<VAR>α : Type u_7<VAR>β : Type u_8<GOAL>Sigma.fst ∘ Prod.toSigma = Prod.fst
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>x : α × β<GOAL>x.toSigma.fst = x.fst
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>x : α × β<GOAL>x.toSigma.snd = x.snd
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>x : α<VAR>y : β<GOAL>(x, y).toSigma = ⟨x, y⟩
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>γ : Sort u_3<VAR>f : (a : α) → β a → γ<VAR>a : α<VAR>b : β a<GOAL>PSigma.elim f ⟨a, b⟩ = f a b
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>a₁ a₂ : α<VAR>b₁ : β a₁<VAR>b₂ : β a₂<GOAL>⟨a₁, b₁⟩ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ HEq b₁ b₂
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>x₀ x₁ : PSigma β<GOAL>x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ HEq x₀.snd x₁.snd
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>p : (a : α) ×' β a → Prop<GOAL>(∀ (x : (a : α) ×' β a), p x) ↔ ∀ (a : α) (b : β a), p ⟨a, b⟩
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>p : (a : α) ×' β a → Prop<GOAL>(∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩
<VAR>α : Sort u_1<VAR>β : Sort u_3<VAR>p : α → β → Prop<VAR>x₀ x₁ : (a : α) ×' Subtype (p a)<GOAL>x₀.fst = x₁.fst → x₀.snd.val = x₁.snd.val → x₀ = x₁
<VAR>α : Sort u_1<VAR>β : Sort u_3<VAR>p : α → β → Prop<VAR>x₀ x₁ : (a : α) ×' Subtype (p a)<GOAL>x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ x₀.snd.val = x₁.snd.val
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → LE (α i)<VAR>i : ι<VAR>a b : α i<GOAL>⟨i, a⟩ ≤ ⟨i, b⟩ ↔ a ≤ b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → LT (α i)<VAR>i : ι<VAR>a b : α i<GOAL>⟨i, a⟩ < ⟨i, b⟩ ↔ a < b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → LE (α i)<VAR>a b : (i : ι) × α i<GOAL>a ≤ b ↔ ∃ h, h ▸ a.snd ≤ b.snd
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → LT (α i)<VAR>a b : (i : ι) × α i<GOAL>a < b ↔ ∃ h, h ▸ a.snd < b.snd
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>LT ι<VAR>(i : ι) → LE (α i)<VAR>a b : Σₗ (i : ι), α i<GOAL>a ≤ b ↔ a.fst < b.fst ∨ ∃ h, h ▸ a.snd ≤ b.snd
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>LT ι<VAR>(i : ι) → LT (α i)<VAR>a b : Σₗ (i : ι), α i<GOAL>a < b ↔ a.fst < b.fst ∨ ∃ h, h ▸ a.snd < b.snd
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : PProd α β<GOAL>⟨p.fst, p.snd⟩ = p
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : PProd α β → Prop<GOAL>(∀ (x : PProd α β), p x) ↔ ∀ (a : α) (b : β), p ⟨a, b⟩
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : PProd α β → Prop<GOAL>(∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : α → β → Prop<GOAL>(∀ (x : PProd α β), p x.fst x.snd) ↔ ∀ (a : α) (b : β), p a b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : α → β → Prop<GOAL>(∃ x, p x.fst x.snd) ↔ ∃ a b, p a b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>δ : Sort u_4<VAR>f : α → β<VAR>g : γ → δ<VAR>hf : Function.Injective f<VAR>hg : Function.Injective g<GOAL>Function.Injective fun x => ⟨f x.fst, g x.snd⟩
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>PartialOrder G<VAR>PartialOrder P<VAR>SMul G P<VAR>IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>(s • t).IsPWO
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>PartialOrder G<VAR>PartialOrder P<VAR>VAdd G P<VAR>IsOrderedCancelVAdd G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>(s +ᵥ t).IsPWO
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>LinearOrder G<VAR>LinearOrder P<VAR>VAdd G P<VAR>IsOrderedCancelVAdd G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsWF<VAR>ht : t.IsWF<GOAL>(s +ᵥ t).IsWF
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>LinearOrder G<VAR>LinearOrder P<VAR>SMul G P<VAR>IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsWF<VAR>ht : t.IsWF<GOAL>(s • t).IsWF
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>LinearOrder G<VAR>LinearOrder P<VAR>VAdd G P<VAR>IsOrderedCancelVAdd G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hsn : s.Nonempty<VAR>htn : t.Nonempty<GOAL>⋯.min ⋯ = hs.min hsn +ᵥ ht.min htn
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>LinearOrder G<VAR>LinearOrder P<VAR>SMul G P<VAR>IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hsn : s.Nonempty<VAR>htn : t.Nonempty<GOAL>⋯.min ⋯ = hs.min hsn • ht.min htn
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>PartialOrder G<VAR>PartialOrder P<VAR>SMul G P<VAR>IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>x : G × P<GOAL>x ∈ Finset.SMulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>PartialOrder G<VAR>PartialOrder P<VAR>VAdd G P<VAR>IsOrderedCancelVAdd G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>x : G × P<GOAL>x ∈ Finset.VAddAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 +ᵥ x.2 = a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>PartialOrder G<VAR>PartialOrder P<VAR>SMul G P<VAR>IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>u : Set G<VAR>hu : u.IsPWO<VAR>a : P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>h : u ⊆ s<GOAL>Finset.SMulAntidiagonal hu ht a ⊆ Finset.SMulAntidiagonal hs ht a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>PartialOrder G<VAR>PartialOrder P<VAR>VAdd G P<VAR>IsOrderedCancelVAdd G P<VAR>s : Set G<VAR>t : Set P<VAR>u : Set G<VAR>hu : u.IsPWO<VAR>a : P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>h : u ⊆ s<GOAL>Finset.VAddAntidiagonal hu ht a ⊆ Finset.VAddAntidiagonal hs ht a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>PartialOrder G<VAR>PartialOrder P<VAR>SMul G P<VAR>IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t v : Set P<VAR>hv : v.IsPWO<VAR>a : P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>h : v ⊆ t<GOAL>Finset.SMulAntidiagonal hs hv a ⊆ Finset.SMulAntidiagonal hs ht a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>PartialOrder G<VAR>PartialOrder P<VAR>VAdd G P<VAR>IsOrderedCancelVAdd G P<VAR>s : Set G<VAR>t v : Set P<VAR>hv : v.IsPWO<VAR>a : P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>h : v ⊆ t<GOAL>Finset.VAddAntidiagonal hs hv a ⊆ Finset.VAddAntidiagonal hs ht a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>PartialOrder G<VAR>PartialOrder P<VAR>SMul G P<VAR>IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>{a | (Finset.SMulAntidiagonal hs ht a).Nonempty} ⊆ s • t
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>PartialOrder G<VAR>PartialOrder P<VAR>VAdd G P<VAR>IsOrderedCancelVAdd G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>{a | (Finset.VAddAntidiagonal hs ht a).Nonempty} ⊆ s +ᵥ t
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>PartialOrder G<VAR>PartialOrder P<VAR>SMul G P<VAR>IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>{a | (Finset.SMulAntidiagonal hs ht a).Nonempty}.IsPWO
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>PartialOrder G<VAR>PartialOrder P<VAR>VAdd G P<VAR>IsOrderedCancelVAdd G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>{a | (Finset.VAddAntidiagonal hs ht a).Nonempty}.IsPWO
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>LinearOrder G<VAR>LinearOrder P<VAR>SMul G P<VAR>IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hns : s.Nonempty<VAR>hnt : t.Nonempty<GOAL>Finset.SMulAntidiagonal ⋯ ⋯ (hs.min hns • ht.min hnt) = {(hs.min hns, ht.min hnt)}
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>LinearOrder G<VAR>LinearOrder P<VAR>VAdd G P<VAR>IsOrderedCancelVAdd G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hns : s.Nonempty<VAR>hnt : t.Nonempty<GOAL>Finset.VAddAntidiagonal ⋯ ⋯ (hs.min hns +ᵥ ht.min hnt) = {(hs.min hns, ht.min hnt)}
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>a b : (i : ι) × α i<GOAL>(Finset.Icc a b).card = if h : a.fst = b.fst then (Finset.Icc (h ▸ a.snd) b.snd).card else 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>a b : (i : ι) × α i<GOAL>(Finset.Ico a b).card = if h : a.fst = b.fst then (Finset.Ico (h ▸ a.snd) b.snd).card else 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>a b : (i : ι) × α i<GOAL>(Finset.Ioc a b).card = if h : a.fst = b.fst then (Finset.Ioc (h ▸ a.snd) b.snd).card else 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>a b : (i : ι) × α i<GOAL>(Finset.Ioo a b).card = if h : a.fst = b.fst then (Finset.Ioo (h ▸ a.snd) b.snd).card else 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>i : ι<VAR>a b : α i<GOAL>Finset.Icc ⟨i, a⟩ ⟨i, b⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Icc a b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>i : ι<VAR>a b : α i<GOAL>Finset.Ico ⟨i, a⟩ ⟨i, b⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Ico a b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>i : ι<VAR>a b : α i<GOAL>Finset.Ioc ⟨i, a⟩ ⟨i, b⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Ioc a b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>i : ι<VAR>a b : α i<GOAL>Finset.Ioo ⟨i, a⟩ ⟨i, b⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Ioo a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LE β<VAR>a b : α × β<GOAL>toLex a ≤ toLex b ↔ a.1 < b.1 ∨ a.1 = b.1 ∧ a.2 ≤ b.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>a b : α × β<GOAL>toLex a < toLex b ↔ a.1 < b.1 ∨ a.1 = b.1 ∧ a.2 < b.2