ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y = ↑π ↔ InnerProductGeometry.angle x y = π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>x = 0 ∨ y = 0 ∨ o.oangle x y = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2) ↔ ⟪x, y⟫_ℝ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>⟪x, y⟫_ℝ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>⟪y, x⟫_ℝ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(-π / 2)<GOAL>⟪x, y⟫_ℝ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(-π / 2)<GOAL>⟪y, x⟫_ℝ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle (-x) y).sign = -(o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle x (-y)).sign = -(o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<GOAL>(o.oangle (r • x) y).sign = SignType.sign r * (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<GOAL>(o.oangle x (r • y)).sign = SignType.sign r * (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<GOAL>o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = ↑π ↔ o.oangle x y = 0 ∨ o.oangle x y = ↑π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<GOAL>(o.oangle x (r • x + y)).sign = (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<GOAL>(o.oangle (x + r • y) y).sign = (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<GOAL>(o.oangle x (y - r • x)).sign = (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<GOAL>(o.oangle (x - r • y) y).sign = (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle x (x + y)).sign = (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle (x + y) y).sign = (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle x (y - x)).sign = (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle (x - y) y).sign = (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<GOAL>(o.oangle x (r • x - y)).sign = -(o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<GOAL>(o.oangle (r • y - x) y).sign = -(o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle x (x - y)).sign = -(o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle (y - x) y).sign = -(o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle y (y - x)).sign = (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle (x - y) x).sign = (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r₁ r₂ : ℝ<GOAL>(o.oangle x (r₁ • x + r₂ • y)).sign = SignType.sign r₂ * (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r₁ r₂ : ℝ<GOAL>(o.oangle (r₁ • x + r₂ • y) y).sign = SignType.sign r₁ * (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r₁ r₂ r₃ r₄ : ℝ<GOAL>(o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : ‖x‖ = ‖y‖<GOAL>|(o.oangle (y - x) y).toReal| < π / 2
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : ‖x‖ = ‖y‖<GOAL>|(o.oangle x (x - y)).toReal| < π / 2
<VAR>α : Sort u<VAR>self : Unique α<VAR>a : α<GOAL>a = default
<VAR>α : Sort u<GOAL>Nonempty (Unique α) ↔ ∃! x, True
<VAR>α : Sort u_1<VAR>p : α → Prop<GOAL>Nonempty (Unique (Subtype p)) ↔ ∃! a, p a
<VAR>α : Sort u_1<VAR>Unique α<VAR>a : α<GOAL>a = default
<VAR>α : Sort u_1<VAR>Unique α<VAR>a : α<GOAL>default = a
<VAR>α : Sort u_1<VAR>Unique α<VAR>p : α → Prop<GOAL>(∀ (a : α), p a) ↔ p default
<VAR>α : Sort u_1<VAR>Unique α<VAR>p : α → Prop<GOAL>Exists p ↔ p default
<VAR>α : Sort u_1<VAR>h₁ h₂ : Unique α<GOAL>h₁ = h₂
<VAR>α : Sort u<GOAL>Nonempty (Unique α) ↔ Subsingleton α ∧ Nonempty α
<VAR>α : Sort u_1<VAR>β : α → Sort v<VAR>(a : α) → Inhabited (β a)<GOAL>default = fun a => default
<VAR>α : Sort u_1<VAR>β : α → Sort v<VAR>(a : α) → Inhabited (β a)<VAR>a : α<GOAL>default a = default
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Subsingleton α<VAR>f : α → β<VAR>a : α<GOAL>f = Function.const α (f a)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Unique α<VAR>f : α → β<GOAL>f = Function.const α (f default)
<VAR>α : Sort u_1<VAR>Unique α<VAR>β : α → Sort v<VAR>f : (a : α) → β a<GOAL>HEq f (Function.const α (f default))
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>Subsingleton β<GOAL>Subsingleton α
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>Subsingleton α<VAR>hf : Function.Surjective f<GOAL>Subsingleton β
<VAR>ι : Sort u_2<VAR>α : ι → Sort u_3<GOAL>∀ {x : Unique ι} (x_1 : α default), uniqueElim x_1 default = x_1
<VAR>ι : Sort u_2<VAR>β : Sort u_4<GOAL>∀ {x : Unique ι} (x_1 : β) (i : ι), uniqueElim x_1 i = x_1
<VAR>A : Sort u_2<VAR>B : Sort u_3<VAR>Unique A<VAR>Unique B<VAR>f : A → B<GOAL>Function.Bijective f
<VAR>α : Type u<GOAL>Subsingleton (Option α) ↔ IsEmpty α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α × β<GOAL>Equiv.pprodEquivProd.symm x = ⟨x.1, x.2⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : PProd α β<GOAL>Equiv.pprodEquivProd x = (x.fst, x.snd)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>δ : Sort u_4<VAR>e₁ : α ≃ β<VAR>e₂ : γ ≃ δ<VAR>x : PProd α γ<GOAL>(e₁.pprodCongr e₂) x = ⟨e₁ x.fst, e₂ x.snd⟩
<VAR>α₁ : Sort u_1<VAR>α₂ : Type u_2<VAR>β₁ : Sort u_3<VAR>β₂ : Type u_4<VAR>ea : α₁ ≃ α₂<VAR>eb : β₁ ≃ β₂<GOAL>∀ (a : PProd α₁ β₁), (ea.pprodProd eb) a = (ea a.fst, eb a.snd)
<VAR>α₁ : Sort u_1<VAR>α₂ : Type u_2<VAR>β₁ : Sort u_3<VAR>β₂ : Type u_4<VAR>ea : α₁ ≃ α₂<VAR>eb : β₁ ≃ β₂<GOAL>∀ (a : α₂ × β₂), (ea.pprodProd eb).symm a = (ea.pprodCongr eb).symm ⟨a.1, a.2⟩
<VAR>α₁ : Type u_1<VAR>α₂ : Sort u_2<VAR>β₁ : Type u_3<VAR>β₂ : Sort u_4<VAR>ea : α₁ ≃ α₂<VAR>eb : β₁ ≃ β₂<GOAL>∀ (a : PProd α₂ β₂), (ea.prodPProd eb).symm a = (ea.symm a.fst, eb.symm a.snd)
<VAR>α₁ : Type u_1<VAR>α₂ : Sort u_2<VAR>β₁ : Type u_3<VAR>β₂ : Sort u_4<VAR>ea : α₁ ≃ α₂<VAR>eb : β₁ ≃ β₂<GOAL>∀ (a : α₁ × β₁), (ea.prodPProd eb) a = (ea.symm.pprodCongr eb.symm).symm ⟨a.1, a.2⟩
<VAR>α : Sort u_1<VAR>β : Sort u_2<GOAL>∀ (a : PLift α × PLift β), Equiv.pprodEquivProdPLift.symm a = (Equiv.plift.symm.pprodCongr Equiv.plift.symm).symm ⟨a.1, a.2⟩
<VAR>α : Sort u_1<VAR>β : Sort u_2<GOAL>∀ (a : PProd α β), Equiv.pprodEquivProdPLift a = (Equiv.plift.symm a.fst, Equiv.plift.symm a.snd)
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>e₁ : α₁ ≃ α₂<VAR>e₂ : β₁ ≃ β₂<GOAL>⇑(e₁.prodCongr 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₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>⇑(Equiv.prodComm α β) = Prod.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α × β<GOAL>(Equiv.prodComm α β) x = x.swap
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>(Equiv.prodComm α β).symm = Equiv.prodComm β α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : (α × β) × γ<GOAL>(Equiv.prodAssoc α β γ) p = (p.1.1, p.1.2, p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : α × β × γ<GOAL>(Equiv.prodAssoc α β γ).symm p = ((p.1, p.2.1), p.2.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>abcd : (α × β) × γ × δ<GOAL>(Equiv.prodProdProdComm α β γ δ) abcd = ((abcd.1.1, abcd.2.1), abcd.1.2, abcd.2.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<GOAL>(Equiv.prodProdProdComm α β γ δ).symm = Equiv.prodProdProdComm α γ β δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<GOAL>⇑(Equiv.curry α β γ).symm = Function.uncurry
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<GOAL>⇑(Equiv.curry α β γ) = Function.curry
<VAR>α : Type u_1<VAR>a : α<GOAL>(Equiv.prodPUnit α).symm a = (a, PUnit.unit)
<VAR>α : Type u_1<VAR>p : α × PUnit.{u_2 + 1}<GOAL>(Equiv.prodPUnit α) p = p.1
<VAR>α : Type u_1<GOAL>∀ (a : α), (Equiv.punitProd α).symm a = (PUnit.unit, a)
<VAR>α : Type u_1<GOAL>∀ (a : PUnit.{u_2 + 1} × α), (Equiv.punitProd α) a = a.2
<VAR>α : Type u_1<VAR>p : (_ : α) × PUnit.{u_2 + 1}<GOAL>(Equiv.sigmaPUnit α) p = p.fst
<VAR>α : Type u_1<VAR>a : α<GOAL>((Equiv.sigmaPUnit α).symm a).fst = a
<VAR>α : Type u_1<VAR>a : α<GOAL>((Equiv.sigmaPUnit α).symm a).snd = PUnit.unit
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>Unique β<GOAL>⇑(Equiv.prodUnique α β) = Prod.fst
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>Unique β<VAR>x : α × β<GOAL>(Equiv.prodUnique α β) x = x.1
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>Unique β<VAR>x : α<GOAL>(Equiv.prodUnique α β).symm x = (x, default)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>Unique β<GOAL>⇑(Equiv.uniqueProd α β) = Prod.snd
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>Unique β<VAR>x : β × α<GOAL>(Equiv.uniqueProd α β) x = x.2
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>Unique β<VAR>x : α<GOAL>(Equiv.uniqueProd α β).symm x = (default, x)
<VAR>α : Type u_2<VAR>β : α → Type u_1<VAR>(a : α) → Unique (β a)<GOAL>⇑(Equiv.sigmaUnique α β) = Sigma.fst
<VAR>α : Type u_2<VAR>β : α → Type u_1<VAR>(a : α) → Unique (β a)<VAR>x : (a : α) × β a<GOAL>(Equiv.sigmaUnique α β) x = x.fst
<VAR>α : Type u_2<VAR>β : α → Type u_1<VAR>(a : α) → Unique (β a)<VAR>x : α<GOAL>(Equiv.sigmaUnique α β).symm x = ⟨x, default⟩
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>ea : α₁ ≃ α₂<VAR>eb : β₁ ≃ β₂<GOAL>∀ (a : α₁ ⊕ β₁), (ea.sumCongr eb) a = Sum.map (⇑ea) (⇑eb) a
<VAR>α₁ : Type u_1<VAR>β₁ : Type u_2<VAR>α₂ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>e : α₁ ≃ β₁<VAR>f : α₂ ≃ β₂<VAR>g : β₁ ≃ γ₁<VAR>h : β₂ ≃ γ₂<GOAL>(e.sumCongr f).trans (g.sumCongr h) = (e.trans g).sumCongr (f.trans h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : α ≃ β<VAR>f : γ ≃ δ<GOAL>(e.sumCongr f).symm = e.symm.sumCongr f.symm
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>(Equiv.refl α).sumCongr (Equiv.refl β) = Equiv.refl (α ⊕ β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ea : Equiv.Perm α<VAR>eb : Equiv.Perm β<VAR>x : α ⊕ β<GOAL>(ea.sumCongr eb) x = Sum.map (⇑ea) (⇑eb) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Equiv.Perm α<VAR>f : Equiv.Perm β<VAR>g : Equiv.Perm α<VAR>h : Equiv.Perm β<GOAL>Equiv.trans (e.sumCongr f) (g.sumCongr h) = Equiv.Perm.sumCongr (Equiv.trans e g) (Equiv.trans f h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Equiv.Perm α<VAR>f : Equiv.Perm β<GOAL>Equiv.symm (e.sumCongr f) = Equiv.Perm.sumCongr (Equiv.symm e) (Equiv.symm f)
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Equiv.Perm.sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>⇑(Equiv.sumComm α β) = Sum.swap
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>(Equiv.sumComm α β).symm = Equiv.sumComm β α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<GOAL>(Equiv.sumAssoc α β γ) (Sum.inl (Sum.inl a)) = Sum.inl a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>b : β<GOAL>(Equiv.sumAssoc α β γ) (Sum.inl (Sum.inr b)) = Sum.inr (Sum.inl b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>c : γ<GOAL>(Equiv.sumAssoc α β γ) (Sum.inr c) = Sum.inr (Sum.inr c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<GOAL>(Equiv.sumAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>b : β<GOAL>(Equiv.sumAssoc α β γ).symm (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>c : γ<GOAL>(Equiv.sumAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>IsEmpty β<VAR>val : α<GOAL>(Equiv.sumEmpty α β).symm val = Sum.inl val
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>IsEmpty β<VAR>a : α<GOAL>(Equiv.sumEmpty α β) (Sum.inl a) = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>IsEmpty α<GOAL>∀ (a : β), (Equiv.emptySum α β).symm a = Sum.inr a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>IsEmpty α<VAR>b : β<GOAL>(Equiv.emptySum α β) (Sum.inr b) = b
<VAR>α : Type u_1<GOAL>(Equiv.optionEquivSumPUnit α) none = Sum.inr PUnit.unit
<VAR>α : Type u_1<VAR>a : α<GOAL>(Equiv.optionEquivSumPUnit α) (some a) = Sum.inl a
<VAR>α : Type u_1<VAR>a : α<GOAL>(Equiv.optionEquivSumPUnit α).symm (Sum.inl a) = some a
<VAR>α : Type u_1<VAR>a : PUnit.{u_2 + 1}<GOAL>(Equiv.optionEquivSumPUnit α).symm (Sum.inr a) = none
<VAR>α : Type u_1<VAR>o : { x // x.isSome = true }<GOAL>(Equiv.optionIsSomeEquiv α) o = (↑o).get ⋯
<VAR>α : Type u_1<VAR>x : α<GOAL>↑((Equiv.optionIsSomeEquiv α).symm x) = some x
<VAR>α : Type u_2<VAR>β : Option α → Type u_1<VAR>f : (a : Option α) → β a<GOAL>Equiv.piOptionEquivProd f = (f none, fun a => f (some a))
<VAR>α : Type u_2<VAR>β : Option α → Type u_1<VAR>x : β none × ((a : α) → β (some a))<VAR>a : Option α<GOAL>Equiv.piOptionEquivProd.symm x a = Option.casesOn a x.1 x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : α<GOAL>↑((Equiv.sigmaFiberEquiv f).symm x).snd = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : (y : β) × { x // f x = y }<GOAL>(Equiv.sigmaFiberEquiv f) x = ↑x.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : α<GOAL>((Equiv.sigmaFiberEquiv f).symm x).fst = f x
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>x : { a // p a }<GOAL>(Equiv.sumCompl p) (Sum.inl x) = ↑x
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>x : { a // ¬p a }<GOAL>(Equiv.sumCompl p) (Sum.inr x) = ↑x
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>h : p a<GOAL>(Equiv.sumCompl p).symm a = Sum.inl ⟨a, h⟩
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>h : ¬p a<GOAL>(Equiv.sumCompl p).symm a = Sum.inr ⟨a, h⟩
<VAR>ε : Type u_1<VAR>p : ε → Prop<VAR>DecidablePred p<VAR>ep : Equiv.Perm { a // p a }<VAR>en : Equiv.Perm { a // ¬p a }<VAR>a : ε<GOAL>(ep.subtypeCongr en) a = if h : p a then ↑(ep ⟨a, h⟩) else ↑(en ⟨a, h⟩)
<VAR>ε : Type u_1<VAR>p : ε → Prop<VAR>DecidablePred p<VAR>ep : Equiv.Perm { a // p a }<VAR>en : Equiv.Perm { a // ¬p a }<VAR>a : ε<VAR>h : p a<GOAL>(ep.subtypeCongr en) a = ↑(ep ⟨a, h⟩)
<VAR>ε : Type u_1<VAR>p : ε → Prop<VAR>DecidablePred p<VAR>ep : Equiv.Perm { a // p a }<VAR>en : Equiv.Perm { a // ¬p a }<VAR>a : { a // p a }<GOAL>(ep.subtypeCongr en) ↑a = ↑(ep a)
<VAR>ε : Type u_1<VAR>p : ε → Prop<VAR>DecidablePred p<VAR>ep : Equiv.Perm { a // p a }<VAR>en : Equiv.Perm { a // ¬p a }<VAR>a : ε<VAR>h : ¬p a<GOAL>(ep.subtypeCongr en) a = ↑(en ⟨a, h⟩)
<VAR>ε : Type u_1<VAR>p : ε → Prop<VAR>DecidablePred p<VAR>ep : Equiv.Perm { a // p a }<VAR>en : Equiv.Perm { a // ¬p a }<VAR>a : { a // ¬p a }<GOAL>(ep.subtypeCongr en) ↑a = ↑(en a)
<VAR>ε : Type u_1<VAR>p : ε → Prop<VAR>DecidablePred p<GOAL>Equiv.Perm.subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a }) = Equiv.refl ε
<VAR>ε : Type u_1<VAR>p : ε → Prop<VAR>DecidablePred p<VAR>ep : Equiv.Perm { a // p a }<VAR>en : Equiv.Perm { a // ¬p a }<GOAL>Equiv.symm (ep.subtypeCongr en) = Equiv.Perm.subtypeCongr (Equiv.symm ep) (Equiv.symm en)
<VAR>ε : Type u_1<VAR>p : ε → Prop<VAR>DecidablePred p<VAR>ep ep' : Equiv.Perm { a // p a }<VAR>en en' : Equiv.Perm { a // ¬p a }<GOAL>Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en') = Equiv.Perm.subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : α → Prop<VAR>DecidablePred p<VAR>x₀ : { a // p a } → β<VAR>x : { x // x ∘ Subtype.val = x₀ }<VAR>a : { a // ¬p a }<GOAL>(Equiv.subtypePreimage p x₀) x a = ↑x ↑a
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : α → Prop<VAR>DecidablePred p<VAR>x₀ : { a // p a } → β<VAR>x : { a // ¬p a } → β<VAR>a : α<GOAL>↑((Equiv.subtypePreimage p x₀).symm x) a = if h : p a then x₀ ⟨a, h⟩ else x ⟨a, h⟩
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : α → Prop<VAR>DecidablePred p<VAR>x₀ : { a // p a } → β<VAR>x : { a // ¬p a } → β<VAR>a : α<VAR>h : p a<GOAL>↑((Equiv.subtypePreimage p x₀).symm x) a = x₀ ⟨a, h⟩
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : α → Prop<VAR>DecidablePred p<VAR>x₀ : { a // p a } → β<VAR>x : { a // ¬p a } → β<VAR>a : α<VAR>h : ¬p a<GOAL>↑((Equiv.subtypePreimage p x₀).symm x) a = x ⟨a, h⟩
<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>φ : α → β → Sort u_1<VAR>f : (x : α) → (y : β) → φ x y<VAR>y : β<VAR>x : α<GOAL>(Equiv.piComm φ) f y x = Function.swap f y x
<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>φ : α → β → Sort u_1<GOAL>(Equiv.piComm φ).symm = Equiv.piComm (Function.swap φ)
<VAR>α : Type u_3<VAR>β : α → Type u_1<VAR>γ : (a : α) → β a → Type u_2<VAR>f : (x : (i : α) × β i) → γ x.fst x.snd<GOAL>(Equiv.piCurry γ) f = Sigma.curry f
<VAR>α : Type u_3<VAR>β : α → Type u_1<VAR>γ : (a : α) → β a → Type u_2<VAR>f : (a : α) → (b : β a) → γ a b<GOAL>(Equiv.piCurry γ).symm f = Sigma.uncurry f
<VAR>α₁ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_1<VAR>e : α₁ → β₁ ≃ β₂<VAR>b : β₁<VAR>a : α₁<GOAL>(Equiv.prodCongrLeft e) (b, a) = ((e a) b, a)
<VAR>α₁ : Type u_3<VAR>β₁ : Type u_1<VAR>β₂ : Type u_2<VAR>e : β₁ ≃ β₂<GOAL>e.prodCongr (Equiv.refl α₁) = Equiv.prodCongrLeft fun x => e
<VAR>α₁ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_1<VAR>e : α₁ → β₁ ≃ β₂<VAR>a : α₁<VAR>b : β₁<GOAL>(Equiv.prodCongrRight e) (a, b) = (a, (e a) b)
<VAR>α₁ : Type u_3<VAR>β₁ : Type u_1<VAR>β₂ : Type u_2<VAR>e : β₁ ≃ β₂<GOAL>(Equiv.refl α₁).prodCongr e = Equiv.prodCongrRight fun x => e
<VAR>α₁ : Type u_3<VAR>β₁ : Type u_2<VAR>β₂ : Type u_1<VAR>e : α₁ → β₁ ≃ β₂<GOAL>(Equiv.prodCongrLeft e).trans (Equiv.prodComm β₂ α₁) = (Equiv.prodComm β₁ α₁).trans (Equiv.prodCongrRight e)
<VAR>α₁ : Type u_3<VAR>β₁ : Type u_2<VAR>β₂ : Type u_1<VAR>e : α₁ → β₁ ≃ β₂<GOAL>(Equiv.prodCongrRight e).trans (Equiv.prodComm α₁ β₂) = (Equiv.prodComm α₁ β₁).trans (Equiv.prodCongrLeft e)
<VAR>α₁ : Type u_1<VAR>β₁ : Type u_3<VAR>β₂ : Type u_2<VAR>e : α₁ → β₁ ≃ β₂<GOAL>(Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂) = (Equiv.sigmaEquivProd α₁ β₁).trans (Equiv.prodCongrRight e)
<VAR>α₁ : Type u_2<VAR>β₁ : Type u_1<VAR>β₂ : Type u_3<VAR>e : α₁ → β₁ ≃ β₂<GOAL>(Equiv.sigmaEquivProd α₁ β₁).symm.trans (Equiv.sigmaCongrRight e) = (Equiv.prodCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂).symm
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>β : Type u_3<VAR>f : α → γ<VAR>g : β → γ<VAR>e : (c : γ) → { a // f a = c } ≃ { b // g b = c }<GOAL>∀ (a : β), (Equiv.ofFiberEquiv e).symm a = ↑((Equiv.sigmaCongrRight e).symm ((Equiv.sigmaFiberEquiv g).symm a)).snd
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>β : Type u_3<VAR>f : α → γ<VAR>g : β → γ<VAR>e : (c : γ) → { a // f a = c } ≃ { b // g b = c }<GOAL>∀ (a : α), (Equiv.ofFiberEquiv e) a = ↑((e (f a)) ((Equiv.sigmaFiberEquiv f).symm a).snd)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → γ<VAR>g : β → γ<VAR>e : (c : γ) → { a // f a = c } ≃ { b // g b = c }<VAR>a : α<GOAL>g ((Equiv.ofFiberEquiv e) a) = f a
<VAR>α₁ : Type u_1<VAR>β₁ : Type u_2<VAR>β₂ : Type u_3<VAR>α₂ : Type u_4<VAR>e₁ : α₁ ≃ α₂<VAR>e₂ : α₁ → β₁ ≃ β₂<GOAL>⇑(e₁.prodShear e₂).symm = fun y => (e₁.symm y.1, (e₂ (e₁.symm y.1)).symm y.2)
<VAR>α₁ : Type u_1<VAR>β₁ : Type u_2<VAR>β₂ : Type u_3<VAR>α₂ : Type u_4<VAR>e₁ : α₁ ≃ α₂<VAR>e₂ : α₁ → β₁ ≃ β₂<GOAL>⇑(e₁.prodShear e₂) = fun x => (e₁ x.1, (e₂ x.1) x.2)
<VAR>α₁ : Type u_2<VAR>β₁ : Type u_1<VAR>DecidableEq α₁<VAR>a : α₁<VAR>e : Equiv.Perm β₁<VAR>b : β₁<GOAL>(Equiv.Perm.prodExtendRight a e) (a, b) = (a, e b)
<VAR>α₁ : Type u_1<VAR>β₁ : Type u_2<VAR>DecidableEq α₁<VAR>e : Equiv.Perm β₁<VAR>a a' : α₁<VAR>h : a' ≠ a<VAR>b : β₁<GOAL>(Equiv.Perm.prodExtendRight a e) (a', b) = (a', b)
<VAR>α₁ : Type u_2<VAR>β₁ : Type u_1<VAR>DecidableEq α₁<VAR>e : Equiv.Perm β₁<VAR>a a' : α₁<VAR>b : β₁<VAR>h : (Equiv.Perm.prodExtendRight a e) (a', b) ≠ (a', b)<GOAL>a' = a
<VAR>α₁ : Type u_1<VAR>β₁ : Type u_2<VAR>DecidableEq α₁<VAR>a : α₁<VAR>e : Equiv.Perm β₁<VAR>ab : α₁ × β₁<GOAL>((Equiv.Perm.prodExtendRight a e) ab).1 = ab.1
<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>π : ι ⊕ ι' → Type u_1<VAR>g : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))<VAR>t : ι ⊕ ι'<GOAL>(Equiv.sumPiEquivProdPi π).symm g t = Sum.rec g.1 g.2 t
<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>π : ι ⊕ ι' → Type u_1<VAR>f : (i : ι ⊕ ι') → π i<GOAL>(Equiv.sumPiEquivProdPi π) f = (fun i => f (Sum.inl i), fun i' => f (Sum.inr i'))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>π : ι → Type u<VAR>π' : ι' → Type u<GOAL>∀ (a : ((i : ι) → Sum.elim π π' (Sum.inl i)) × ((i' : ι') → Sum.elim π π' (Sum.inr i'))) (i : ι ⊕ ι'), (Equiv.prodPiEquivSumPi π π') a i = (Equiv.sumPiEquivProdPi (Sum.elim π π')).symm a i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>π : ι → Type u<VAR>π' : ι' → Type u<GOAL>∀ (a : (i : ι ⊕ ι') → Sum.elim π π' i), (Equiv.prodPiEquivSumPi π π').symm a = (Equiv.sumPiEquivProdPi (Sum.elim π π')) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ⊕ β → γ<VAR>a : α<GOAL>((Equiv.sumArrowEquivProdArrow α β γ) f).1 a = f (Sum.inl a)