ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₃ p₁ p₂).tan * dist p₁ p₂ = dist p₃ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>dist p₃ p₂ / (∡ p₂ p₃ p₁).cos = dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>dist p₁ p₂ / (∡ p₃ p₁ p₂).cos = dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>dist p₁ p₂ / (∡ p₂ p₃ p₁).sin = dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>dist p₃ p₂ / (∡ p₃ p₁ p₂).sin = dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>dist p₁ p₂ / (∡ p₂ p₃ p₁).tan = dist p₃ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>dist p₃ p₂ / (∡ p₃ p₁ p₂).tan = dist p₁ p₂
<VAR>α : Type u_3<VAR>self : Denumerable α<VAR>n : ℕ<GOAL>∃ a ∈ Encodable.decode n, Encodable.encode a = n
<VAR>α : Type u_3<VAR>Denumerable α<VAR>n : ℕ<GOAL>(Encodable.decode n).isSome = true
<VAR>α : Type u_3<VAR>Denumerable α<VAR>n : ℕ<GOAL>Encodable.decode n = some (Denumerable.ofNat α n)
<VAR>α : Type u_1<VAR>Denumerable α<VAR>n : ℕ<VAR>b : α<VAR>h : Encodable.decode n = some b<GOAL>Denumerable.ofNat α n = b
<VAR>α : Type u_1<VAR>Denumerable α<VAR>n : ℕ<GOAL>Encodable.encode (Denumerable.ofNat α n) = n
<VAR>α : Type u_1<VAR>Denumerable α<VAR>a : α<GOAL>Denumerable.ofNat α (Encodable.encode a) = a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Denumerable α<VAR>e : β ≃ α<VAR>n : ℕ<GOAL>Denumerable.ofNat β n = e.symm (Denumerable.ofNat α n)
<VAR>n : ℕ<GOAL>Denumerable.ofNat ℕ n = n
<VAR>α : Type u_1<VAR>Denumerable α<VAR>γ : α → Type u_3<VAR>(a : α) → Denumerable (γ a)<VAR>n : ℕ<GOAL>Denumerable.ofNat (Sigma γ) n = ⟨Denumerable.ofNat α (Nat.unpair n).1, Denumerable.ofNat (γ (Denumerable.ofNat α (Nat.unpair n).1)) (Nat.unpair n).2⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Denumerable α<VAR>Denumerable β<VAR>n : ℕ<GOAL>Denumerable.ofNat (α × β) n = (Denumerable.ofNat α (Nat.unpair n).1, Denumerable.ofNat β (Nat.unpair n).2)
<GOAL>Denumerable.ofNat (ℕ × ℕ) = Nat.unpair
<VAR>s : Set ℕ<VAR>Infinite ↑s<VAR>x : ↑s<GOAL>∃ n, ↑x + n + 1 ∈ s
<VAR>s : Set ℕ<VAR>Infinite ↑s<VAR>DecidablePred fun x => x ∈ s<VAR>x y : ↑s<VAR>h : y < x<GOAL>Nat.Subtype.succ y ≤ x
<VAR>s : Set ℕ<VAR>Infinite ↑s<VAR>DecidablePred fun x => x ∈ s<VAR>x y : ↑s<VAR>h : ∀ z < x, z ≤ y<GOAL>x ≤ Nat.Subtype.succ y
<VAR>s : Set ℕ<VAR>Infinite ↑s<VAR>DecidablePred fun x => x ∈ s<VAR>x : ↑s<GOAL>x < Nat.Subtype.succ x
<VAR>s : Set ℕ<VAR>Infinite ↑s<VAR>DecidablePred fun x => x ∈ s<VAR>x y : ↑s<GOAL>x < Nat.Subtype.succ y ↔ x ≤ y
<VAR>s : Set ℕ<VAR>Infinite ↑s<VAR>DecidablePred fun x => x ∈ s<VAR>x : ℕ<VAR>hx : x ∈ s<GOAL>∃ n, Nat.Subtype.ofNat s n = ⟨x, hx⟩
<VAR>s : Set ℕ<VAR>Infinite ↑s<VAR>DecidablePred fun x => x ∈ s<GOAL>Function.Surjective (Nat.Subtype.ofNat s)
<VAR>s : Set ℕ<VAR>Infinite ↑s<VAR>DecidablePred fun x => x ∈ s<GOAL>Set.range (Nat.Subtype.ofNat s) = Set.univ
<VAR>s : Set ℕ<VAR>Infinite ↑s<VAR>DecidablePred fun x => x ∈ s<GOAL>Set.range (Subtype.val ∘ Nat.Subtype.ofNat s) = s
<VAR>s : Set ℕ<VAR>DecidablePred fun x => x ∈ s<VAR>x : ↑s<GOAL>Nat.Subtype.toFunAux x = (Finset.filter (fun x => x ∈ s) (Finset.range ↑x)).card
<VAR>s : Set ℕ<VAR>Infinite ↑s<VAR>DecidablePred fun x => x ∈ s<VAR>n : ℕ<GOAL>Nat.Subtype.toFunAux (Nat.Subtype.ofNat s n) = n
<VAR>α : Type u_3<VAR>Countable α<VAR>Infinite α<GOAL>Nonempty (Denumerable α)
<VAR>α : Type u_3<GOAL>Nonempty (Denumerable α) ↔ Countable α ∧ Infinite α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α ↪ β<VAR>a : α<GOAL>f.toEquivRange a = ⟨f a, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α ↪ β<VAR>a : α<GOAL>f.toEquivRange.symm ⟨f a, ⋯⟩ = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α ↪ β<GOAL>f.toEquivRange = Equiv.ofInjective ⇑f ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>e : Equiv.Perm α<VAR>f : α ↪ β<VAR>a : α<GOAL>(e.viaFintypeEmbedding f) (f a) = f (e a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>e : Equiv.Perm α<VAR>f : α ↪ β<VAR>b : β<VAR>h : b ∈ Set.range ⇑f<GOAL>(e.viaFintypeEmbedding f) b = f (e (f.invOfMemRange ⟨b, h⟩))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>e : Equiv.Perm α<VAR>f : α ↪ β<VAR>b : β<VAR>h : b ∉ Set.range ⇑f<GOAL>(e.viaFintypeEmbedding f) b = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>e : Equiv.Perm α<VAR>f : α ↪ β<VAR>DecidableEq α<VAR>Fintype β<GOAL>Equiv.Perm.sign (e.viaFintypeEmbedding f) = Equiv.Perm.sign e
<VAR>α : Type u_1<VAR>Finite α<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>e : { x // p x } ≃ { x // q x }<VAR>x : α<VAR>hx : p x<GOAL>e.extendSubtype x = ↑(e ⟨x, hx⟩)
<VAR>α : Type u_1<VAR>Finite α<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>e : { x // p x } ≃ { x // q x }<VAR>x : α<VAR>hx : p x<GOAL>q (e.extendSubtype x)
<VAR>α : Type u_1<VAR>Finite α<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>e : { x // p x } ≃ { x // q x }<VAR>x : α<VAR>hx : ¬p x<GOAL>e.extendSubtype x = ↑(e.toCompl ⟨x, hx⟩)
<VAR>α : Type u_1<VAR>Finite α<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>e : { x // p x } ≃ { x // q x }<VAR>x : α<VAR>hx : ¬p x<GOAL>¬q (e.extendSubtype x)
<GOAL>∀ (a : Bool × ℕ), Equiv.boolProdNatEquivNat a = Function.uncurry Nat.bit a
<GOAL>∀ (a : ℕ), Equiv.boolProdNatEquivNat.symm a = a.boddDiv2
<GOAL>∀ (a : ℕ), Equiv.natSumNatEquivNat.symm a = Bool.rec (Sum.inl a.div2) (Sum.inr a.div2) a.bodd
<GOAL>⇑Equiv.natSumNatEquivNat = Sum.elim (fun x => 2 * x) fun x => 2 * x + 1
<VAR>α : Sort u_1<VAR>β : Type u_2<VAR>p : β → Prop<VAR>e : α ≃ Subtype p<GOAL>Set.range ⇑e.asEmbedding = setOf p
<VAR>α : Type u_1<GOAL>∀ (a : α), Function.Embedding.coeWithTop a = ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>x : β<VAR>h : x ∉ Set.range ⇑f<GOAL>∀ (a : Option α), (f.optionElim x h) a = Option.elim' x (⇑f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : (f : α ↪ β) × ↑(Set.range ⇑f)ᶜ<GOAL>(Function.Embedding.optionEmbeddingEquiv α β).symm f = f.fst.optionElim ↑f.snd ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Option α ↪ β<GOAL>↑((Function.Embedding.optionEmbeddingEquiv α β) f).snd = f none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Option α ↪ β<GOAL>((Function.Embedding.optionEmbeddingEquiv α β) f).fst = Function.Embedding.coeWithTop.trans f
<VAR>α : Sort u_1<VAR>β : Type u_2<VAR>p : Set β<VAR>f : α ↪ β<VAR>H : ∀ (a : α), f a ∈ p<VAR>a : α<GOAL>(Function.Embedding.codRestrict p f H) a = ⟨f a, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s : Set α<GOAL>f.image s = ⇑f '' s
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>x : ↑s<GOAL>↑((s.embeddingOfSubset t h) x) = ↑x
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>h : Disjoint p q<VAR>a : { x // p x ∨ q x }<GOAL>(subtypeOrEquiv p q h) a = (subtypeOrLeftEmbedding p q) a
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>h : Disjoint p q<VAR>x : { x // p x }<GOAL>(subtypeOrEquiv p q h).symm (Sum.inl x) = ⟨↑x, ⋯⟩
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>h : Disjoint p q<VAR>x : { x // q x }<GOAL>(subtypeOrEquiv p q h).symm (Sum.inr x) = ⟨↑x, ⋯⟩
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : Disjoint s t<GOAL>∀ (a : ↑s ⊕ ↑t), (Function.Embedding.sumSet h) a = Sum.elim Subtype.val Subtype.val a
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : Disjoint s t<GOAL>⇑(Function.Embedding.sumSet h) = Sum.elim Subtype.val Subtype.val
<VAR>α : Type u_1<VAR>s t r : Set α<VAR>h : Disjoint s t<GOAL>↑(Sum.inl ⁻¹' (⇑(Function.Embedding.sumSet h) ⁻¹' r)) = r ∩ s
<VAR>α : Type u_1<VAR>s t r : Set α<VAR>h : Disjoint s t<GOAL>↑(Sum.inr ⁻¹' (⇑(Function.Embedding.sumSet h) ⁻¹' r)) = r ∩ t
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : Disjoint s t<GOAL>Set.range ⇑(Function.Embedding.sumSet h) = s ∪ t
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>h : Pairwise (Disjoint on s)<VAR>x : (i : ι) × ↑(s i)<GOAL>(Function.Embedding.sigmaSet h) x = ↑x.snd
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>h : Pairwise (Disjoint on s)<GOAL>⇑(Function.Embedding.sigmaSet h) = fun x => ↑x.snd
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>h : Pairwise (Disjoint on s)<VAR>i : ι<VAR>r : Set α<GOAL>↑(Sigma.mk i ⁻¹' (⇑(Function.Embedding.sigmaSet h) ⁻¹' r)) = r ∩ s i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>h : Pairwise (Disjoint on s)<GOAL>Set.range ⇑(Function.Embedding.sigmaSet h) = ⋃ i, s i
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>self : α ↪ β<GOAL>Function.Injective self.toFun
<VAR>α : Sort u_1<VAR>β : Sort u_2<GOAL>(∃ f, Function.Surjective f) ↔ Nonempty (α → β) ∧ Nonempty (β ↪ α)
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α ≃ β<GOAL>⇑f.toEmbedding = ⇑f
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α ≃ β<VAR>a : α<GOAL>f.toEmbedding a = f a
<VAR>α : Sort u<VAR>β : Sort v<GOAL>Function.Injective Equiv.toEmbedding
<VAR>α : Sort u_1<VAR>β : Sort u_2<GOAL>Function.Injective fun f => ⇑f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f g : α ↪ β<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f g : α ↪ β<GOAL>(∀ (x : α), f x = g x) ↔ f = g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α ↪ β<GOAL>f.toFun = ⇑f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>i : Function.Injective f<GOAL>⇑{ toFun := f, inj' := i } = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>inj : Function.Injective ⇑f<GOAL>{ toFun := ⇑f, inj' := inj } = f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α ↪ β<GOAL>Function.Injective ⇑f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α ↪ β<VAR>x y : α<GOAL>f x = f y ↔ x = y
<VAR>α : Sort u_1<VAR>a : α<GOAL>(Function.Embedding.refl α) a = a
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α ↪ β<VAR>g : β ↪ γ<GOAL>∀ (a : α), (f.trans g) a = g (f a)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>e : α ≃ β<GOAL>e.toEmbedding.trans e.symm.toEmbedding = Function.Embedding.refl α
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>e : α ≃ β<GOAL>e.symm.toEmbedding.trans e.toEmbedding = Function.Embedding.refl β
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>δ : Sort x<VAR>e₁ : α ≃ β<VAR>e₂ : γ ≃ δ<VAR>f : α ↪ γ<GOAL>⇑(Function.Embedding.congr e₁ e₂ f) = ⇑(f.trans e₂.toEmbedding) ∘ ⇑e₁.symm
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α ↪ β<VAR>a : α<VAR>b : β<VAR>(a' : α) → Decidable (a' = a)<VAR>(a' : α) → Decidable (f a' = b)<GOAL>(f.setValue a b) a = b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α ↪ β<VAR>a a' : α<VAR>b : β<VAR>(a' : α) → Decidable (a' = a)<VAR>(a' : α) → Decidable (f a' = b)<GOAL>(f.setValue a b) a' = b ↔ a' = a
<VAR>α : Type u_1<GOAL>⇑Function.Embedding.some = some
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<GOAL>⇑f.optionMap = Option.map ⇑f
<VAR>α : Sort u_1<VAR>p : α → Prop<GOAL>⇑(Function.Embedding.subtype p) = Subtype.val
<VAR>α : Sort u_1<VAR>Setoid α<GOAL>⇑(Function.Embedding.quotientOut α) = Quotient.out
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>a : α<GOAL>(Function.Embedding.sectl α b) a = (a, b)
<VAR>α : Type u_1<VAR>a : α<VAR>β : Type u_2<VAR>b : β<GOAL>(Function.Embedding.sectr a β) b = (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e₁ : α ↪ β<VAR>e₂ : γ ↪ δ<GOAL>⇑(e₁.prodMap e₂) = Prod.map ⇑e₁ ⇑e₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e₁ : α ↪ β<VAR>e₂ : γ ↪ δ<GOAL>⇑(e₁.sumMap e₂) = Sum.map ⇑e₁ ⇑e₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>val : α<GOAL>Function.Embedding.inl val = Sum.inl val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>val : β<GOAL>Function.Embedding.inr val = Sum.inr val
<VAR>α : Type u_1<VAR>β : α → Type u_3<VAR>a : α<VAR>snd : β a<GOAL>(Function.Embedding.sigmaMk a) snd = ⟨a, snd⟩
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : α → Type u_3<VAR>β' : α' → Type u_4<VAR>f : α ↪ α'<VAR>g : (a : α) → β a ↪ β' (f a)<VAR>x : (a : α) × β a<GOAL>(f.sigmaMap g) x = Sigma.map (⇑f) (fun a => ⇑(g a)) x
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>γ : α → Sort u_3<VAR>e : (a : α) → β a ↪ γ a<VAR>f : (a : α) → β a<VAR>a : α<GOAL>(Function.Embedding.piCongrRight e) f a = (e a) (f a)
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>e : α ↪ β<VAR>f : γ → α<GOAL>e.arrowCongrRight f = ⇑e ∘ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α ↪ β<VAR>x y z : α<GOAL>(Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α ↪ β<VAR>x y : α<GOAL>⇑(Equiv.swap (f x) (f y)) ∘ ⇑f = ⇑f ∘ ⇑(Equiv.swap x y)
<VAR>β : Sort u_1<VAR>α : Sort u_2<VAR>p : β → Prop<VAR>e : α ≃ Subtype p<GOAL>∀ (a : α), e.asEmbedding a = ↑(e a)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>δ : Sort u_4<VAR>h : α ≃ β<VAR>h' : γ ≃ δ<VAR>f : α ↪ γ<GOAL>(h.embeddingCongr h') f = Function.Embedding.congr h h' f
<VAR>α : Sort u_1<VAR>β : Sort u_2<GOAL>(Equiv.refl α).embeddingCongr (Equiv.refl β) = Equiv.refl (α ↪ β)
<VAR>α₁ : Sort u_1<VAR>β₁ : Sort u_2<VAR>α₂ : Sort u_3<VAR>β₂ : Sort u_4<VAR>α₃ : Sort u_5<VAR>β₃ : Sort u_6<VAR>e₁ : α₁ ≃ α₂<VAR>e₁' : β₁ ≃ β₂<VAR>e₂ : α₂ ≃ α₃<VAR>e₂' : β₂ ≃ β₃<GOAL>(e₁.trans e₂).embeddingCongr (e₁'.trans e₂') = (e₁.embeddingCongr e₁').trans (e₂.embeddingCongr e₂')
<VAR>α₁ : Sort u_1<VAR>β₁ : Sort u_2<VAR>α₂ : Sort u_3<VAR>β₂ : Sort u_4<VAR>e₁ : α₁ ≃ α₂<VAR>e₂ : β₁ ≃ β₂<GOAL>(e₁.embeddingCongr e₂).symm = e₁.symm.embeddingCongr e₂.symm
<VAR>α₁ : Sort u_1<VAR>β₁ : Sort u_2<VAR>γ₁ : Sort u_3<VAR>α₂ : Sort u_4<VAR>β₂ : Sort u_5<VAR>γ₂ : Sort u_6<VAR>ea : α₁ ≃ α₂<VAR>eb : β₁ ≃ β₂<VAR>ec : γ₁ ≃ γ₂<VAR>f : α₁ ↪ β₁<VAR>g : β₁ ↪ γ₁<GOAL>(ea.embeddingCongr ec) (f.trans g) = ((ea.embeddingCongr eb) f).trans ((eb.embeddingCongr ec) g)
<VAR>α : Type u_1<GOAL>(Equiv.refl α).toEmbedding = Function.Embedding.refl α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : α ≃ β<VAR>f : β ≃ γ<GOAL>(e.trans f).toEmbedding = e.toEmbedding.trans f.toEmbedding
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>x : { x // p x ∨ q x }<VAR>hx : p ↑x<GOAL>(subtypeOrLeftEmbedding p q) x = Sum.inl ⟨↑x, hx⟩
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>x : { x // p x ∨ q x }<VAR>hx : ¬p ↑x<GOAL>(subtypeOrLeftEmbedding p q) x = Sum.inr ⟨↑x, ⋯⟩
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>h : ∀ (x : α), p x → q x<VAR>x : { x // p x }<GOAL>↑((Subtype.impEmbedding p q h) x) = ↑x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (InnerProductGeometry.angle x y)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ‖x‖ = ‖y‖<GOAL>InnerProductGeometry.angle x (x - y) = InnerProductGeometry.angle y (y - x)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : InnerProductGeometry.angle x (x - y) = InnerProductGeometry.angle y (y - x)<VAR>hpi : InnerProductGeometry.angle x y ≠ π<GOAL>‖x‖ = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>Real.cos (InnerProductGeometry.angle x (x - y) + InnerProductGeometry.angle y (y - x)) = -Real.cos (InnerProductGeometry.angle x y)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>Real.sin (InnerProductGeometry.angle x (x - y) + InnerProductGeometry.angle y (y - x)) = Real.sin (InnerProductGeometry.angle x y)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>Real.cos (InnerProductGeometry.angle x y + InnerProductGeometry.angle x (x - y) + InnerProductGeometry.angle y (y - x)) = -1
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>Real.sin (InnerProductGeometry.angle x y + InnerProductGeometry.angle x (x - y) + InnerProductGeometry.angle y (y - x)) = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>InnerProductGeometry.angle x y + InnerProductGeometry.angle x (x - y) + InnerProductGeometry.angle y (y - x) = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<GOAL>dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 - 2 * dist p1 p2 * dist p3 p2 * Real.cos (EuclideanGeometry.angle p1 p2 p3)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : dist p1 p2 = dist p1 p3<GOAL>EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p1 p3 p2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p1 p3 p2<VAR>hpi : EuclideanGeometry.angle p2 p1 p3 ≠ π<GOAL>dist p1 p2 = dist p1 p3
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h2 : p2 ≠ p1<VAR>h3 : p3 ≠ p1<GOAL>EuclideanGeometry.angle p1 p2 p3 + EuclideanGeometry.angle p2 p3 p1 + EuclideanGeometry.angle p3 p1 p2 = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>Module.Oriented ℝ V (Fin 2)<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>p1 p2 p3 : P<VAR>h21 : p2 ≠ p1<VAR>h32 : p3 ≠ p2<VAR>h13 : p1 ≠ p3<GOAL>EuclideanGeometry.oangle p1 p2 p3 + EuclideanGeometry.oangle p2 p3 p1 + EuclideanGeometry.oangle p3 p1 p2 = ↑π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>a b c p : P<VAR>h : EuclideanGeometry.angle b p c = π<GOAL>dist a b ^ 2 * dist c p + dist a c ^ 2 * dist b p = dist b c * (dist a p ^ 2 + dist b p * dist c p)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>a b c : P<GOAL>dist a b ^ 2 + dist a c ^ 2 = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>a b c a' b' c' : P<VAR>r : ℝ<VAR>h : EuclideanGeometry.angle a' b' c' = EuclideanGeometry.angle a b c<VAR>hab : dist a' b' = r * dist a b<VAR>hcb : dist c' b' = r * dist c b<GOAL>dist a' c' = r * dist a c
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>self : α ≃ β<GOAL>Function.RightInverse self.invFun self.toFun
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>self : α ≃ β<GOAL>Function.LeftInverse self.invFun self.toFun
<VAR>α : Sort u<VAR>β : Sort v<VAR>F : Sort u_1<VAR>EquivLike F α β<VAR>e : F<GOAL>⇑↑e = ⇑e
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<VAR>g : β → α<VAR>l : Function.LeftInverse g f<VAR>r : Function.RightInverse g f<GOAL>⇑{ toFun := f, invFun := g, left_inv := l, right_inv := r } = f
<VAR>α : Sort u<VAR>β : Sort v<GOAL>Function.Injective fun e => ⇑e
<VAR>α : Sort u<VAR>β : Sort v<VAR>e₁ e₂ : α ≃ β<GOAL>⇑e₁ = ⇑e₂ ↔ e₁ = e₂
<VAR>α : Sort u<VAR>β : Sort v<VAR>f g : α ≃ β<VAR>H : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α ≃ β<VAR>x x' : α<GOAL>x = x' → f x = f x'
<VAR>α : Sort u<VAR>β : Sort v<VAR>f g : α ≃ β<VAR>h : f = g<VAR>x : α<GOAL>f x = g x
<VAR>α : Sort u<VAR>β : Sort v<VAR>f g : α ≃ β<GOAL>f = g ↔ ∀ (x : α), f x = g x
<VAR>α : Sort u<VAR>σ τ : Equiv.Perm α<VAR>H : ∀ (x : α), σ x = τ x<GOAL>σ = τ
<VAR>α : Sort u<VAR>f : Equiv.Perm α<VAR>x x' : α<GOAL>x = x' → f x = f x'
<VAR>α : Sort u<VAR>f g : Equiv.Perm α<VAR>h : f = g<VAR>x : α<GOAL>f x = g x
<VAR>α : Sort u<VAR>σ τ : Equiv.Perm α<GOAL>σ = τ ↔ ∀ (x : α), σ x = τ x
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>Function.LeftInverse ⇑e.symm ⇑e
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>Function.RightInverse ⇑e.symm ⇑e
<GOAL>∀ {a : Sort u_2} {b : Sort u_1} {c : Sort u_3} (e₁ : a ≃ b) (e₂ : b ≃ c), Trans.trans e₁ e₂ = e₁.trans e₂
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>e.toFun = ⇑e
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>e.invFun = ⇑e.symm
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>Function.Injective ⇑e
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>Function.Surjective ⇑e
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>Function.Bijective ⇑e
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<VAR>Subsingleton β<GOAL>Subsingleton α
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<VAR>Subsingleton α<GOAL>Subsingleton β
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>Subsingleton α ↔ Subsingleton β
<VAR>α : Sort u<VAR>Subsingleton α<VAR>e : Equiv.Perm α<GOAL>e = Equiv.refl α
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>Nonempty α ↔ Nonempty β
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<VAR>Nonempty β<GOAL>Nonempty α
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<VAR>g : β → α<VAR>l : Function.LeftInverse g f<VAR>r : Function.RightInverse g f<GOAL>⇑{ toFun := f, invFun := g, left_inv := l, right_inv := r }.symm = g
<VAR>α : Sort u<GOAL>⇑(Equiv.refl α) = id
<VAR>α : Type u_1<VAR>Subsingleton α<VAR>e : Equiv.Perm α<GOAL>⇑e = id
<VAR>α : Sort u<VAR>x : α<GOAL>(Equiv.refl α) x = x
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>f : α ≃ β<VAR>g : β ≃ γ<GOAL>⇑(f.trans g) = ⇑g ∘ ⇑f
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>f : α ≃ β<VAR>g : β ≃ γ<VAR>a : α<GOAL>(f.trans g) a = g (f a)
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<VAR>x : β<GOAL>e (e.symm x) = x
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<VAR>x : α<GOAL>e.symm (e x) = x
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>⇑e.symm ∘ ⇑e = id
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>⇑e ∘ ⇑e.symm = id
<VAR>α : Sort u<VAR>β : Sort v<VAR>F : Sort u_1<VAR>EquivLike F α β<VAR>e : F<VAR>x : β<GOAL>e ((↑e).symm x) = x
<VAR>α : Sort u<VAR>β : Sort v<VAR>F : Sort u_1<VAR>EquivLike F α β<VAR>e : F<VAR>x : α<GOAL>(↑e).symm (e x) = x
<VAR>α : Sort u<VAR>β : Sort v<VAR>F : Sort u_1<VAR>EquivLike F α β<VAR>e : F<GOAL>⇑(↑e).symm ∘ ⇑e = id
<VAR>α : Sort u<VAR>β : Sort v<VAR>F : Sort u_1<VAR>EquivLike F α β<VAR>e : F<GOAL>⇑e ∘ ⇑(↑e).symm = id
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>f : α ≃ β<VAR>g : β ≃ γ<VAR>a : γ<GOAL>(f.trans g).symm a = f.symm (g.symm a)
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α ≃ β<VAR>b : α<GOAL>f.symm.symm b = f b
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α ≃ β<VAR>x y : α<GOAL>f x = f y ↔ x = y
<VAR>α : Sort u<VAR>β : Sort v<VAR>x : α<VAR>y : β<VAR>f : α ≃ β<GOAL>f x = y ↔ x = f.symm y
<VAR>α β : Sort u_1<VAR>h : α = β<VAR>x : α<GOAL>(Equiv.cast h) x = cast h x
<VAR>α β : Sort u_1<VAR>h : α = β<GOAL>(Equiv.cast h).symm = Equiv.cast ⋯
<VAR>α : Sort u_1<VAR>h : α = α := ⋯<GOAL>Equiv.cast h = Equiv.refl α
<VAR>α β γ : Sort u_1<VAR>h : α = β<VAR>h2 : β = γ<GOAL>(Equiv.cast h).trans (Equiv.cast h2) = Equiv.cast ⋯
<VAR>α β : Sort u_1<VAR>h : α = β<VAR>a : α<VAR>b : β<GOAL>(Equiv.cast h) a = b ↔ HEq a b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>e : α ≃ β<VAR>x : β<VAR>y : α<GOAL>e.symm x = y ↔ x = e y