ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Semiring A₃<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>Algebra R A₃<VAR>e₁ : A₁ ≃ₐ[R] A₂<VAR>e₂ : A₂ ≃ₐ[R] A₃<GOAL>(e₁.trans e₂).toLinearEquiv = e₁.toLinearEquiv ≪≫ₗ e₂.toLinearEquiv
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<GOAL>Function.Injective AlgEquiv.toLinearEquiv
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>(↑e).toLinearMap = e.toLinearMap
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f : A₁ →ₐ[R] A₂<VAR>g : A₂ →ₐ[R] A₁<VAR>h₁ : f.comp g = AlgHom.id R A₂<VAR>h₂ : g.comp f = AlgHom.id R A₁<GOAL>(AlgEquiv.ofAlgHom f g h₁ h₂).toLinearMap = f.toLinearMap
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>↑e.toLinearEquiv = e.toLinearMap
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>x : A₁<GOAL>e.toLinearMap x = e x
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<GOAL>Function.Injective AlgEquiv.toLinearMap
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Semiring A₃<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>Algebra R A₃<VAR>f : A₁ ≃ₐ[R] A₂<VAR>g : A₂ ≃ₐ[R] A₃<GOAL>(f.trans g).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>l : A₁ ≃ₗ[R] A₂<VAR>map_one : l 1 = 1<VAR>map_mul : ∀ (x y : A₁), l (x * y) = l x * l y<VAR>a : A₁<GOAL>(AlgEquiv.ofLinearEquiv l map_one map_mul) a = l a
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>l : A₁ ≃ₗ[R] A₂<VAR>map_one : l 1 = 1<VAR>map_mul : ∀ (x y : A₁), l (x * y) = l x * l y<GOAL>(AlgEquiv.ofLinearEquiv l map_one map_mul).symm = AlgEquiv.ofLinearEquiv l.symm ⋯ ⋯
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>map_mul : e.toLinearEquiv 1 = 1<VAR>map_one : ∀ (x y : A₁), e.toLinearEquiv (x * y) = e.toLinearEquiv x * e.toLinearEquiv y<GOAL>AlgEquiv.ofLinearEquiv e.toLinearEquiv map_mul map_one = e
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>l : A₁ ≃ₗ[R] A₂<VAR>map_one : l 1 = 1<VAR>map_mul : ∀ (x y : A₁), l (x * y) = l x * l y<GOAL>(AlgEquiv.ofLinearEquiv l map_one map_mul).toLinearEquiv = l
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f : A₁ ≃+* A₂<VAR>hf : ∀ (x : R), f ((algebraMap R A₁) x) = (algebraMap R A₂) x<VAR>a : A₁<GOAL>(AlgEquiv.ofRingEquiv hf) a = f a
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f : A₁ ≃+* A₂<VAR>hf : ∀ (x : R), f ((algebraMap R A₁) x) = (algebraMap R A₂) x<VAR>a : A₂<GOAL>(AlgEquiv.ofRingEquiv hf).symm a = f.symm a
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>f : A₁ ≃+* A₂<VAR>hf : ∀ (x : R), f ((algebraMap R A₁) x) = (algebraMap R A₂) x<GOAL>↑(AlgEquiv.ofRingEquiv hf) = { toFun := ⇑f, invFun := ⇑f.symm, left_inv := ⋯, right_inv := ⋯ }
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Algebra R A₁<VAR>ϕ ψ : A₁ ≃ₐ[R] A₁<GOAL>ϕ * ψ = ψ.trans ϕ
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Algebra R A₁<GOAL>1 = AlgEquiv.refl
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Algebra R A₁<VAR>x : A₁<GOAL>1 x = x
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Algebra R A₁<VAR>e₁ e₂ : A₁ ≃ₐ[R] A₁<VAR>x : A₁<GOAL>(e₁ * e₂) x = e₁ (e₂ x)
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>ϕ : A₁ ≃ₐ[R] A₂<VAR>ψ : A₁ ≃ₐ[R] A₁<GOAL>ϕ.autCongr ψ = ϕ.symm.trans (ψ.trans ϕ)
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Algebra R A₁<GOAL>AlgEquiv.refl.autCongr = MulEquiv.refl (A₁ ≃ₐ[R] A₁)
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>ϕ : A₁ ≃ₐ[R] A₂<GOAL>ϕ.autCongr.symm = ϕ.symm.autCongr
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Semiring A₃<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>Algebra R A₃<VAR>ϕ : A₁ ≃ₐ[R] A₂<VAR>ψ : A₂ ≃ₐ[R] A₃<GOAL>ϕ.autCongr.trans ψ.autCongr = (ϕ.trans ψ).autCongr
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Algebra R A₁<VAR>f : A₁ ≃ₐ[R] A₁<VAR>a : A₁<GOAL>f • a = f a
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Algebra R A₁<VAR>f : A₁ ≃ₐ[R] A₁<VAR>x : A₁ˣ<GOAL>f • x = (Units.map ↑f) x
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Semiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>y : R<VAR>x : A₁<GOAL>(algebraMap R A₂) y = e x ↔ (algebraMap R A₁) y = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>e : A ≃ₐ[R] A<GOAL>(AlgEquiv.toLinearMapHom R A) e = e.toLinearMap
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Algebra R A₁<VAR>σ : A₁ ≃ₐ[R] A₁<VAR>n : ℕ<GOAL>(σ ^ n).toLinearMap = σ.toLinearMap ^ n
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>CommSemiring R<VAR>Semiring A₁<VAR>Algebra R A₁<GOAL>AlgEquiv.toLinearMap 1 = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>f : S ≃ₐ[R] S<GOAL>↑((AlgEquiv.algHomUnitsEquiv R S).symm f) = ↑f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>f : (S →ₐ[R] S)ˣ<GOAL>∀ (a : S), ((AlgEquiv.algHomUnitsEquiv R S) f) a = (↑↑(↑f).toRingHom).toFun a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>f : (S →ₐ[R] S)ˣ<VAR>a : S<GOAL>((AlgEquiv.algHomUnitsEquiv R S) f).symm a = ↑↑f⁻¹ a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>f : S ≃ₐ[R] S<GOAL>↑((AlgEquiv.algHomUnitsEquiv R S).symm f)⁻¹ = ↑f.symm
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>CommSemiring A₁<VAR>CommSemiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>ι : Type u_1<VAR>f : ι → A₁<VAR>s : Finset ι<GOAL>e (∏ x ∈ s, f x) = ∏ x ∈ s, e (f x)
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>CommSemiring A₁<VAR>CommSemiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>α : Type u_1<VAR>Zero α<VAR>ι : Type u_2<VAR>f : ι →₀ α<VAR>g : ι → α → A₁<GOAL>e (f.prod g) = f.prod fun i a => e (g i a)
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Ring A₁<VAR>Ring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>x : A₁<GOAL>e (-x) = -e x
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>CommSemiring R<VAR>Ring A₁<VAR>Ring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>x y : A₁<GOAL>e (x - y) = e x - e y
<VAR>G : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Group G<VAR>MulSemiringAction G A<VAR>SMulCommClass G R A<VAR>g : G<GOAL>↑(MulSemiringAction.toAlgEquiv R A g) = ↑(MulSemiringAction.toRingEquiv G A g)
<VAR>G : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Group G<VAR>MulSemiringAction G A<VAR>SMulCommClass G R A<VAR>g : G<GOAL>∀ (a : A), (MulSemiringAction.toAlgEquiv R A g).symm a = g⁻¹ • a
<VAR>G : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Group G<VAR>MulSemiringAction G A<VAR>SMulCommClass G R A<VAR>g : G<GOAL>∀ (a : A), (MulSemiringAction.toAlgEquiv R A g) a = g • a
<VAR>G : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Group G<VAR>MulSemiringAction G A<VAR>SMulCommClass G R A<VAR>FaithfulSMul G A<GOAL>Function.Injective (MulSemiringAction.toAlgEquiv R A)
<VAR>α : Type u_2<VAR>Monoid α<VAR>HasDistribNeg α<VAR>n : ℕ<GOAL>Even n → ∀ (a : α), (-a) ^ n = a ^ n
<VAR>α : Type u_2<VAR>Monoid α<VAR>HasDistribNeg α<VAR>n : ℕ<VAR>h : Even n<GOAL>(-1) ^ n = 1
<VAR>α : Type u_2<VAR>DivisionMonoid α<VAR>HasDistribNeg α<VAR>n : ℤ<GOAL>Even n → ∀ (a : α), (-a) ^ n = a ^ n
<VAR>α : Type u_2<VAR>DivisionMonoid α<VAR>HasDistribNeg α<VAR>n : ℤ<VAR>h : Even n<GOAL>(-1) ^ n = 1
<VAR>α : Type u_2<VAR>MulZeroClass α<GOAL>IsSquare 0
<VAR>α : Type u_2<VAR>Semiring α<VAR>a : α<GOAL>Even a ↔ ∃ b, a = 2 * b
<VAR>α : Type u_2<VAR>Semiring α<VAR>a : α<GOAL>Even a ↔ 2 ∣ a
<VAR>α : Type u_2<VAR>Semiring α<VAR>a b : α<VAR>ha : Even a<VAR>hab : a ∣ b<GOAL>Even b
<VAR>α : Type u_2<VAR>Semiring α<VAR>a b : α<VAR>hab : a ∣ b<VAR>ha : Even a<GOAL>Even b
<VAR>α : Type u_5<VAR>Semiring α<GOAL>(Set.range fun x => 2 * x) = {a | Even a}
<VAR>α : Type u_2<VAR>Semiring α<GOAL>Even 2
<VAR>α : Type u_2<VAR>Semiring α<VAR>a : α<VAR>ha : Even a<VAR>b : α<GOAL>Even (b * a)
<VAR>α : Type u_2<VAR>Semiring α<VAR>a : α<VAR>ha : Even a<VAR>b : α<GOAL>Even (a * b)
<VAR>α : Type u_2<VAR>Semiring α<VAR>a : α<GOAL>Even (2 * a)
<VAR>α : Type u_2<VAR>Semiring α<VAR>a : α<VAR>ha : Even a<VAR>n : ℕ<GOAL>n ≠ 0 → Even (a ^ n)
<VAR>α : Type u_2<VAR>Semiring α<VAR>a : α<GOAL>Odd a ↔ ∃ b, a = 2 * b + 1
<VAR>α : Type u_5<VAR>Semiring α<GOAL>(Set.range fun x => 2 * x + 1) = {a | Odd a}
<VAR>α : Type u_2<VAR>Semiring α<VAR>a b : α<GOAL>Even a → Odd b → Odd (a + b)
<VAR>α : Type u_2<VAR>Semiring α<VAR>a b : α<VAR>ha : Even a<VAR>hb : Odd b<GOAL>Odd (b + a)
<VAR>α : Type u_2<VAR>Semiring α<VAR>a b : α<VAR>ha : Odd a<VAR>hb : Even b<GOAL>Odd (a + b)
<VAR>α : Type u_2<VAR>Semiring α<VAR>a b : α<GOAL>Odd a → Odd b → Even (a + b)
<VAR>α : Type u_2<VAR>Semiring α<GOAL>Odd 1
<VAR>α : Type u_2<VAR>Semiring α<VAR>a : α<VAR>h : Even a<GOAL>Odd (a + 1)
<VAR>α : Type u_2<VAR>Semiring α<VAR>a : α<VAR>h : Even a<GOAL>Odd (1 + a)
<VAR>α : Type u_2<VAR>Semiring α<VAR>a : α<GOAL>Odd (2 * a + 1)
<VAR>α : Type u_2<VAR>Semiring α<VAR>a : α<GOAL>Odd (a + (a + 1))
<VAR>α : Type u_2<VAR>Semiring α<VAR>a : α<GOAL>Odd (a + 1 + a)
<VAR>α : Type u_2<VAR>Semiring α<VAR>a : α<GOAL>Odd (a + (1 + a))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Semiring α<VAR>Semiring β<VAR>a : α<VAR>FunLike F α β<VAR>RingHomClass F α β<VAR>f : F<GOAL>Odd a → Odd (f a)
<VAR>R : Type u_5<VAR>Semiring R<VAR>n : ℕ<VAR>hn : Odd n<GOAL>Odd ↑n
<VAR>α : Type u_2<VAR>Semiring α<VAR>a b : α<GOAL>Odd a → Odd b → Odd (a * b)
<VAR>α : Type u_2<VAR>Semiring α<VAR>a : α<VAR>ha : Odd a<VAR>n : ℕ<GOAL>Odd (a ^ n)
<VAR>α : Type u_2<VAR>Semiring α<VAR>a b : α<VAR>n : ℕ<VAR>IsCancelAdd α<VAR>hn : Odd n<VAR>hab : a + b = 0<GOAL>a ^ n + b ^ n = 0
<VAR>α : Type u_2<VAR>Monoid α<VAR>HasDistribNeg α<VAR>n : ℕ<GOAL>Odd n → ∀ (a : α), (-a) ^ n = -a ^ n
<VAR>α : Type u_2<VAR>Monoid α<VAR>HasDistribNeg α<VAR>n : ℕ<VAR>h : Odd n<GOAL>(-1) ^ n = -1
<VAR>α : Type u_2<VAR>Ring α<GOAL>Even (-2)
<VAR>α : Type u_2<VAR>Ring α<VAR>a : α<VAR>hp : Odd a<GOAL>Odd (-a)
<VAR>α : Type u_2<VAR>Ring α<VAR>a : α<GOAL>Odd (-a) ↔ Odd a
<VAR>α : Type u_2<VAR>Ring α<GOAL>Odd (-1)
<VAR>α : Type u_2<VAR>Ring α<VAR>a b : α<VAR>ha : Odd a<VAR>hb : Even b<GOAL>Odd (a - b)
<VAR>α : Type u_2<VAR>Ring α<VAR>a b : α<VAR>ha : Even a<VAR>hb : Odd b<GOAL>Odd (a - b)
<VAR>α : Type u_2<VAR>Ring α<VAR>a b : α<VAR>ha : Odd a<VAR>hb : Odd b<GOAL>Even (a - b)
<VAR>n : ℕ<GOAL>Odd n ↔ n % 2 = 1
<VAR>n : ℕ<GOAL>¬Odd n ↔ n % 2 = 0
<VAR>n : ℕ<GOAL>Even n ↔ ¬Odd n
<VAR>n : ℕ<GOAL>Odd n ↔ ¬Even n
<VAR>n : ℕ<VAR>h : Odd n<GOAL>¬2 ∣ n
<VAR>n : ℕ<GOAL>Xor' (Even n) (Odd n)
<VAR>n : ℕ<GOAL>Even n ∨ Odd n
<VAR>n : ℕ<GOAL>∃ k, n = 2 * k ∨ n = 2 * k + 1
<VAR>n : ℕ<GOAL>∃ k, Xor' (n = 2 * k) (n = 2 * k + 1)
<VAR>m : ℕ<VAR>n : ℕ<VAR>hn : Odd n<GOAL>m % 2 + (m + n) % 2 = 1
<VAR>m : ℕ<GOAL>m % 2 + (m + 1) % 2 = 1
<VAR>m : ℕ<GOAL>(m + 1) % 2 + m % 2 = 1
<VAR>m n : ℕ<GOAL>Even (m + n) ↔ (Odd m ↔ Odd n)
<VAR>n : ℕ<GOAL>¬Even (2 * n + 1)
<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>Even (m - n) ↔ (Odd m ↔ Odd n)
<VAR>m n : ℕ<VAR>hm : Odd m<VAR>hn : Odd n<GOAL>Even (m - n)
<VAR>m n : ℕ<GOAL>Odd (m * n) ↔ Odd m ∧ Odd n
<VAR>m n : ℕ<VAR>h : Odd (m * n)<GOAL>Odd m
<VAR>m n : ℕ<VAR>h : Odd (m * n)<GOAL>Odd n
<VAR>m n : ℕ<GOAL>Even (m / n) ↔ m % (2 * n) / n = 0
<VAR>m n : ℕ<GOAL>Odd (m + n) ↔ (Odd m ↔ Even n)
<VAR>m n : ℕ<GOAL>Odd (m + n) ↔ (Odd n ↔ Even m)
<VAR>m n : ℕ<VAR>h : Odd (m + n)<GOAL>m ≠ n
<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>Odd (m - n) ↔ (Odd m ↔ Even n)
<VAR>m n : ℕ<VAR>h : n ≤ m<VAR>hm : Odd m<VAR>hn : Even n<GOAL>Odd (m - n)
<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>Odd (m - n) ↔ (Odd n ↔ Even m)
<VAR>m n : ℕ<VAR>h : n ≤ m<VAR>hm : Even m<VAR>hn : Odd n<GOAL>Odd (m - n)
<VAR>n : ℕ<VAR>h : Odd n<GOAL>2 * (n / 2) + 1 = n
<VAR>n : ℕ<VAR>h : Odd n<GOAL>n / 2 * 2 + 1 = n
<VAR>n : ℕ<VAR>h : Odd n<GOAL>1 + n / 2 * 2 = n
<VAR>α : Type u_5<VAR>f : α → α<VAR>hf : Function.Involutive f<VAR>n : ℕ<GOAL>f^[2 * n] = id
<VAR>α : Type u_5<VAR>f : α → α<VAR>hf : Function.Involutive f<VAR>n : ℕ<GOAL>f^[2 * n + 1] = f
<VAR>α : Type u_5<VAR>f : α → α<VAR>n : ℕ<VAR>hf : Function.Involutive f<VAR>hn : Even n<GOAL>f^[n] = id
<VAR>α : Type u_5<VAR>f : α → α<VAR>n : ℕ<VAR>hf : Function.Involutive f<VAR>hn : Odd n<GOAL>f^[n] = f
<VAR>α : Type u_5<VAR>f : α → α<VAR>n : ℕ<VAR>hf : Function.Involutive f<VAR>hne : f ≠ id<GOAL>f^[n] = f ↔ Odd n
<VAR>α : Type u_5<VAR>f : α → α<VAR>n : ℕ<VAR>hf : Function.Involutive f<VAR>hne : f ≠ id<GOAL>f^[n] = id ↔ Even n
<VAR>R : Type u_5<VAR>Monoid R<VAR>HasDistribNeg R<VAR>n : ℕ<VAR>h : -1 ≠ 1<GOAL>(-1) ^ n = 1 ↔ Even n
<VAR>α : Type u_4<VAR>self : BooleanRing α<VAR>a : α<GOAL>a * a = a
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a : α<GOAL>a * a = a
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a : α<GOAL>a + a = 0
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a : α<GOAL>-a = a
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : α<GOAL>a + b = 0 ↔ a = b
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : α<GOAL>a * b + b * a = 0
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : α<GOAL>a - b = a + b
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a : α<GOAL>a * (1 + a) = 0
<VAR>α : Type u_1<GOAL>toBoolAlg.symm = ofBoolAlg
<VAR>α : Type u_1<GOAL>ofBoolAlg.symm = toBoolAlg
<VAR>α : Type u_1<VAR>a : AsBoolAlg α<GOAL>toBoolAlg (ofBoolAlg a) = a
<VAR>α : Type u_1<VAR>a : α<GOAL>ofBoolAlg (toBoolAlg a) = a
<VAR>α : Type u_1<VAR>a b : α<GOAL>toBoolAlg a = toBoolAlg b ↔ a = b
<VAR>α : Type u_1<VAR>a b : AsBoolAlg α<GOAL>ofBoolAlg a = ofBoolAlg b ↔ a = b
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : α<GOAL>a ⊔ b = b ⊔ a
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : α<GOAL>a ⊓ b = b ⊓ a
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b c : α<GOAL>a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b c : α<GOAL>a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : α<GOAL>a ⊔ a ⊓ b = a
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : α<GOAL>a ⊓ (a ⊔ b) = a
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b c : α<GOAL>(a + b + a * b) * (a + c + a * c) = a + b * c + a * (b * c)
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b c : α<GOAL>(a ⊔ b) ⊓ (a ⊔ c) ⊔ (a ⊔ b ⊓ c) = a ⊔ b ⊓ c
<VAR>α : Type u_1<VAR>BooleanRing α<GOAL>ofBoolAlg ⊤ = 1
<VAR>α : Type u_1<VAR>BooleanRing α<GOAL>ofBoolAlg ⊥ = 0
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : AsBoolAlg α<GOAL>ofBoolAlg (a ⊔ b) = ofBoolAlg a + ofBoolAlg b + ofBoolAlg a * ofBoolAlg b
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : AsBoolAlg α<GOAL>ofBoolAlg (a ⊓ b) = ofBoolAlg a * ofBoolAlg b
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a : AsBoolAlg α<GOAL>ofBoolAlg aᶜ = 1 + ofBoolAlg a
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : AsBoolAlg α<GOAL>ofBoolAlg (a \ b) = ofBoolAlg a * (1 + ofBoolAlg b)
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : α<GOAL>(a + b + a * b) * (1 + a * b) = a + b
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : AsBoolAlg α<GOAL>ofBoolAlg (a ∆ b) = ofBoolAlg a + ofBoolAlg b
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : AsBoolAlg α<GOAL>ofBoolAlg a * ofBoolAlg b = ofBoolAlg a ↔ a ≤ b
<VAR>α : Type u_1<VAR>BooleanRing α<GOAL>toBoolAlg 0 = ⊥
<VAR>α : Type u_1<VAR>BooleanRing α<GOAL>toBoolAlg 1 = ⊤
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : α<GOAL>toBoolAlg (a * b) = toBoolAlg a ⊓ toBoolAlg b
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : α<GOAL>toBoolAlg (a + b + a * b) = toBoolAlg a ⊔ toBoolAlg b
<VAR>α : Type u_1<VAR>BooleanRing α<VAR>a b : α<GOAL>toBoolAlg (a + b) = toBoolAlg a ∆ toBoolAlg b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BooleanRing α<VAR>BooleanRing β<VAR>f : α →+* β<GOAL>∀ (a : AsBoolAlg α), f.asBoolAlg.toSupHom a = (⇑toBoolAlg ∘ ⇑f ∘ ⇑ofBoolAlg) a
<VAR>α : Type u_1<VAR>BooleanRing α<GOAL>(RingHom.id α).asBoolAlg = BoundedLatticeHom.id (AsBoolAlg α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>BooleanRing α<VAR>BooleanRing β<VAR>BooleanRing γ<VAR>g : β →+* γ<VAR>f : α →+* β<GOAL>(g.comp f).asBoolAlg = g.asBoolAlg.comp f.asBoolAlg
<VAR>α : Type u_1<GOAL>toBoolRing.symm = ofBoolRing
<VAR>α : Type u_1<GOAL>ofBoolRing.symm = toBoolRing
<VAR>α : Type u_1<VAR>a : AsBoolRing α<GOAL>toBoolRing (ofBoolRing a) = a
<VAR>α : Type u_1<VAR>a : α<GOAL>ofBoolRing (toBoolRing a) = a
<VAR>α : Type u_1<VAR>a b : α<GOAL>toBoolRing a = toBoolRing b ↔ a = b
<VAR>α : Type u_1<VAR>a b : AsBoolRing α<GOAL>ofBoolRing a = ofBoolRing b ↔ a = b
<VAR>α : Type u_1<VAR>BooleanAlgebra α<GOAL>ofBoolRing 0 = ⊥
<VAR>α : Type u_1<VAR>BooleanAlgebra α<GOAL>ofBoolRing 1 = ⊤
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>a : AsBoolRing α<GOAL>ofBoolRing (-a) = ofBoolRing a
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>a b : AsBoolRing α<GOAL>ofBoolRing (a + b) = ofBoolRing a ∆ ofBoolRing b
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>a b : AsBoolRing α<GOAL>ofBoolRing (a - b) = ofBoolRing a ∆ ofBoolRing b
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>a b : AsBoolRing α<GOAL>ofBoolRing (a * b) = ofBoolRing a ⊓ ofBoolRing b
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>a b : AsBoolRing α<GOAL>ofBoolRing a ≤ ofBoolRing b ↔ a * b = a
<VAR>α : Type u_1<VAR>BooleanAlgebra α<GOAL>toBoolRing ⊥ = 0
<VAR>α : Type u_1<VAR>BooleanAlgebra α<GOAL>toBoolRing ⊤ = 1
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>toBoolRing (a ⊓ b) = toBoolRing a * toBoolRing b
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>toBoolRing (a ∆ b) = toBoolRing a + toBoolRing b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BooleanAlgebra α<VAR>BooleanAlgebra β<VAR>f : BoundedLatticeHom α β<GOAL>∀ (a : AsBoolRing α), f.asBoolRing a = (⇑toBoolRing ∘ ⇑f ∘ ⇑ofBoolRing) a
<VAR>α : Type u_1<VAR>BooleanAlgebra α<GOAL>(BoundedLatticeHom.id α).asBoolRing = RingHom.id (AsBoolRing α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>BooleanAlgebra α<VAR>BooleanAlgebra β<VAR>BooleanAlgebra γ<VAR>g : BoundedLatticeHom β γ<VAR>f : BoundedLatticeHom α β<GOAL>(g.comp f).asBoolRing = g.asBoolRing.comp f.asBoolRing
<VAR>α : Type u_4<VAR>BooleanAlgebra α<GOAL>∀ (a : AsBoolAlg (AsBoolRing α)), (OrderIso.asBoolAlgAsBoolRing α) a = ofBoolRing (ofBoolAlg a)
<VAR>α : Type u_4<VAR>BooleanAlgebra α<GOAL>∀ (a : α), (RelIso.symm (OrderIso.asBoolAlgAsBoolRing α)) a = toBoolAlg (toBoolRing a)
<VAR>α : Type u_4<VAR>BooleanRing α<GOAL>∀ (a : AsBoolRing (AsBoolAlg α)), (RingEquiv.asBoolRingAsBoolAlg α) a = ofBoolAlg (ofBoolRing a)
<VAR>α : Type u_4<VAR>BooleanRing α<GOAL>∀ (a : α), (RingEquiv.asBoolRingAsBoolAlg α).symm a = toBoolRing (toBoolAlg a)
<VAR>R : Type u<VAR>inst₁ inst₂ : Distrib R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : Distrib R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalNonAssocSemiring R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<GOAL>Function.Injective (@NonUnitalNonAssocSemiring.toDistrib R)
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalNonAssocSemiring R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>R : Type u<GOAL>Function.Injective (@NonUnitalSemiring.toNonUnitalNonAssocSemiring R)
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalSemiring R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalSemiring R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>R : Type u<VAR>inst₁ inst₂ : AddMonoidWithOne R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_one : One.one = One.one<GOAL>inst₁ = inst₂
<VAR>R : Type u<GOAL>Function.Injective (@AddCommMonoidWithOne.toAddMonoidWithOne R)
<VAR>R : Type u<VAR>inst₁ inst₂ : AddCommMonoidWithOne R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_one : One.one = One.one<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : NonAssocSemiring R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<GOAL>Function.Injective (@NonAssocSemiring.toNonUnitalNonAssocSemiring R)
<VAR>R : Type u<VAR>inst₁ inst₂ : NonAssocSemiring R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalNonAssocRing R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<GOAL>Function.Injective (@NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring R)
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalNonAssocRing R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalRing R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<GOAL>Function.Injective (@NonUnitalRing.toNonUnitalSemiring R)
<VAR>R : Type u<GOAL>Function.Injective (@NonUnitalRing.toNonUnitalNonAssocRing R)
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalRing R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>R : Type u<VAR>inst₁ inst₂ : NonAssocRing R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<GOAL>Function.Injective (@NonAssocRing.toNonAssocSemiring R)
<VAR>R : Type u<GOAL>Function.Injective (@NonAssocRing.toNonUnitalNonAssocRing R)
<VAR>R : Type u<VAR>inst₁ inst₂ : NonAssocRing R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>R : Type u<VAR>inst₁ inst₂ : Semiring R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<GOAL>Function.Injective (@Semiring.toNonUnitalSemiring R)
<VAR>R : Type u<GOAL>Function.Injective (@Semiring.toNonAssocSemiring R)
<VAR>R : Type u<VAR>inst₁ inst₂ : Semiring R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>R : Type u<VAR>inst₁ inst₂ : Ring R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<GOAL>Function.Injective (@Ring.toNonUnitalRing R)
<VAR>R : Type u<GOAL>Function.Injective (@Ring.toNonAssocRing R)
<VAR>R : Type u<GOAL>Function.Injective (@Ring.toSemiring R)
<VAR>R : Type u<VAR>inst₁ inst₂ : Ring R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>R : Type u<GOAL>Function.Injective (@NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring R)
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalNonAssocCommSemiring R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : NonUnitalNonAssocCommSemiring R<GOAL>inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
<VAR>R : Type u<GOAL>Function.Injective (@NonUnitalCommSemiring.toNonUnitalSemiring R)