ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⇑↑(MulOpposite.opLinearEquiv R) = MulOpposite.op
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⇑↑(MulOpposite.opLinearEquiv R).symm = MulOpposite.unop
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>(MulOpposite.opLinearEquiv R).toAddEquiv = MulOpposite.opAddEquiv
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>↑(MulOpposite.opLinearEquiv R) = MulOpposite.opAddEquiv
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>(MulOpposite.opLinearEquiv R).symm.toAddEquiv = MulOpposite.opAddEquiv.symm
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>↑(MulOpposite.opLinearEquiv R).symm = MulOpposite.opAddEquiv.symm
<VAR>R : Type u_5<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>l : List R<VAR>x : M<GOAL>l.sum • x = (List.map (fun r => r • x) l).sum
<VAR>R : Type u_5<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>l : Multiset R<VAR>x : M<GOAL>l.sum • x = (Multiset.map (fun r => r • x) l).sum
<VAR>R : Type u_5<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Multiset R<VAR>t : Multiset M<GOAL>s.sum • t.sum = (Multiset.map (fun p => p.1 • p.2) (s ×ˢ t)).sum
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : ι → R<VAR>s : Finset ι<VAR>x : M<GOAL>(∑ i ∈ s, f i) • x = ∑ i ∈ s, f i • x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → R<VAR>g : β → M<GOAL>(∑ i ∈ s, f i) • ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i • g j
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype α<VAR>Fintype β<VAR>f : α → R<VAR>g : β → M<GOAL>(∑ i : α, f i) • ∑ j : β, g j = ∑ i : α, ∑ j : β, f i • g j
<VAR>α : Type u_3<VAR>R : Type u_5<VAR>CommSemiring R<VAR>s : Finset α<GOAL>↑s.card = ∑ a ∈ s, 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>DecidableEq ι<VAR>Fintype ι<VAR>AddCommMonoid α<VAR>f : κ → α<VAR>s : Finset κ<VAR>i : ι<GOAL>∑ g ∈ Fintype.piFinset fun x => s, f (g i) = s.card ^ (Fintype.card ι - 1) • ∑ b ∈ s, f b
<VAR>α : Type u_1<VAR>a : α<GOAL>SymAlg.unsym (SymAlg.sym a) = a
<VAR>α : Type u_1<VAR>a : α<GOAL>SymAlg.sym (SymAlg.unsym a) = a
<VAR>α : Type u_1<GOAL>⇑SymAlg.sym ∘ ⇑SymAlg.unsym = id
<VAR>α : Type u_1<GOAL>⇑SymAlg.unsym ∘ ⇑SymAlg.sym = id
<VAR>α : Type u_1<GOAL>SymAlg.sym.symm = SymAlg.unsym
<VAR>α : Type u_1<GOAL>SymAlg.unsym.symm = SymAlg.sym
<VAR>α : Type u_1<GOAL>Function.Bijective ⇑SymAlg.sym
<VAR>α : Type u_1<GOAL>Function.Bijective ⇑SymAlg.unsym
<VAR>α : Type u_1<GOAL>Function.Injective ⇑SymAlg.sym
<VAR>α : Type u_1<GOAL>Function.Surjective ⇑SymAlg.sym
<VAR>α : Type u_1<GOAL>Function.Injective ⇑SymAlg.unsym
<VAR>α : Type u_1<GOAL>Function.Surjective ⇑SymAlg.unsym
<VAR>α : Type u_1<VAR>a b : α<GOAL>SymAlg.sym a = SymAlg.sym b ↔ a = b
<VAR>α : Type u_1<VAR>a b : αˢʸᵐ<GOAL>SymAlg.unsym a = SymAlg.unsym b ↔ a = b
<VAR>α : Type u_1<VAR>One α<GOAL>SymAlg.sym 1 = 1
<VAR>α : Type u_1<VAR>Zero α<GOAL>SymAlg.sym 0 = 0
<VAR>α : Type u_1<VAR>Zero α<GOAL>SymAlg.unsym 0 = 0
<VAR>α : Type u_1<VAR>One α<GOAL>SymAlg.unsym 1 = 1
<VAR>α : Type u_1<VAR>Add α<VAR>a b : α<GOAL>SymAlg.sym (a + b) = SymAlg.sym a + SymAlg.sym b
<VAR>α : Type u_1<VAR>Add α<VAR>a b : αˢʸᵐ<GOAL>SymAlg.unsym (a + b) = SymAlg.unsym a + SymAlg.unsym b
<VAR>α : Type u_1<VAR>Sub α<VAR>a b : α<GOAL>SymAlg.sym (a - b) = SymAlg.sym a - SymAlg.sym b
<VAR>α : Type u_1<VAR>Sub α<VAR>a b : αˢʸᵐ<GOAL>SymAlg.unsym (a - b) = SymAlg.unsym a - SymAlg.unsym b
<VAR>α : Type u_1<VAR>Neg α<VAR>a : α<GOAL>SymAlg.sym (-a) = -SymAlg.sym a
<VAR>α : Type u_1<VAR>Neg α<VAR>a : αˢʸᵐ<GOAL>SymAlg.unsym (-a) = -SymAlg.unsym a
<VAR>α : Type u_1<VAR>Add α<VAR>Mul α<VAR>One α<VAR>OfNat α 2<VAR>Invertible 2<VAR>a b : αˢʸᵐ<GOAL>a * b = SymAlg.sym (⅟2 * (SymAlg.unsym a * SymAlg.unsym b + SymAlg.unsym b * SymAlg.unsym a))
<VAR>α : Type u_1<VAR>Mul α<VAR>Add α<VAR>One α<VAR>OfNat α 2<VAR>Invertible 2<VAR>a b : αˢʸᵐ<GOAL>SymAlg.unsym (a * b) = ⅟2 * (SymAlg.unsym a * SymAlg.unsym b + SymAlg.unsym b * SymAlg.unsym a)
<VAR>α : Type u_1<VAR>Mul α<VAR>Add α<VAR>One α<VAR>OfNat α 2<VAR>Invertible 2<VAR>a b : α<GOAL>SymAlg.sym a * SymAlg.sym b = SymAlg.sym (⅟2 * (a * b + b * a))
<VAR>α : Type u_1<VAR>Inv α<VAR>a : α<GOAL>SymAlg.sym a⁻¹ = (SymAlg.sym a)⁻¹
<VAR>α : Type u_1<VAR>Inv α<VAR>a : αˢʸᵐ<GOAL>SymAlg.unsym a⁻¹ = (SymAlg.unsym a)⁻¹
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>SMul R α<VAR>c : R<VAR>a : α<GOAL>SymAlg.sym (c • a) = c • SymAlg.sym a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>SMul R α<VAR>c : R<VAR>a : αˢʸᵐ<GOAL>SymAlg.unsym (c • a) = c • SymAlg.unsym a
<VAR>α : Type u_1<VAR>One α<VAR>a : αˢʸᵐ<GOAL>SymAlg.unsym a = 1 ↔ a = 1
<VAR>α : Type u_1<VAR>Zero α<VAR>a : αˢʸᵐ<GOAL>SymAlg.unsym a = 0 ↔ a = 0
<VAR>α : Type u_1<VAR>Zero α<VAR>a : α<GOAL>SymAlg.sym a = 0 ↔ a = 0
<VAR>α : Type u_1<VAR>One α<VAR>a : α<GOAL>SymAlg.sym a = 1 ↔ a = 1
<VAR>α : Type u_1<VAR>One α<VAR>a : αˢʸᵐ<GOAL>SymAlg.unsym a ≠ 1 ↔ a ≠ 1
<VAR>α : Type u_1<VAR>Zero α<VAR>a : αˢʸᵐ<GOAL>SymAlg.unsym a ≠ 0 ↔ a ≠ 0
<VAR>α : Type u_1<VAR>One α<VAR>a : α<GOAL>SymAlg.sym a ≠ 1 ↔ a ≠ 1
<VAR>α : Type u_1<VAR>Zero α<VAR>a : α<GOAL>SymAlg.sym a ≠ 0 ↔ a ≠ 0
<VAR>α : Type u_1<VAR>Mul α<VAR>AddMonoidWithOne α<VAR>Invertible 2<VAR>a : α<VAR>Invertible a<GOAL>⅟(SymAlg.sym a) = SymAlg.sym ⅟a
<VAR>α : Type u_1<VAR>Semiring α<VAR>Invertible 2<VAR>a : αˢʸᵐ<GOAL>SymAlg.unsym (a * a) = SymAlg.unsym a * SymAlg.unsym a
<VAR>α : Type u_1<VAR>Semiring α<VAR>Invertible 2<VAR>a : α<GOAL>SymAlg.sym (a * a) = SymAlg.sym a * SymAlg.sym a
<VAR>α : Type u_1<VAR>Mul α<VAR>AddCommSemigroup α<VAR>One α<VAR>OfNat α 2<VAR>Invertible 2<VAR>a b : αˢʸᵐ<GOAL>a * b = b * a
<VAR>M₀ : Type u_1<VAR>MonoidWithZero M₀<VAR>x : M₀<GOAL>x ∈ nonZeroDivisorsLeft M₀ ↔ ∀ (y : M₀), y * x = 0 → y = 0
<VAR>M₀ : Type u_1<VAR>MonoidWithZero M₀<VAR>r : M₀<GOAL>r ∉ nonZeroDivisorsLeft M₀ ↔ {s | s * r = 0 ∧ s ≠ 0}.Nonempty
<VAR>M₀ : Type u_1<VAR>MonoidWithZero M₀<VAR>x : M₀<GOAL>x ∈ nonZeroDivisorsRight M₀ ↔ ∀ (y : M₀), x * y = 0 → y = 0
<VAR>M₀ : Type u_1<VAR>MonoidWithZero M₀<VAR>r : M₀<GOAL>r ∉ nonZeroDivisorsRight M₀ ↔ {s | r * s = 0 ∧ s ≠ 0}.Nonempty
<VAR>M₀ : Type u_2<VAR>CommMonoidWithZero M₀<GOAL>nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀
<VAR>M₀ : Type u_1<VAR>MonoidWithZero M₀<VAR>NoZeroDivisors M₀<VAR>Nontrivial M₀<GOAL>↑(nonZeroDivisorsLeft M₀) = {x | x ≠ 0}
<VAR>M₀ : Type u_1<VAR>MonoidWithZero M₀<VAR>NoZeroDivisors M₀<VAR>Nontrivial M₀<GOAL>↑(nonZeroDivisorsRight M₀) = {x | x ≠ 0}
<VAR>M : Type u_2<VAR>MonoidWithZero M<VAR>r : M<GOAL>r ∈ M⁰ ↔ ∀ (x : M), x * r = 0 → x = 0
<VAR>M : Type u_2<VAR>MonoidWithZero M<VAR>r : M<GOAL>r ∉ M⁰ ↔ {s | s * r = 0 ∧ s ≠ 0}.Nonempty
<VAR>M : Type u_2<VAR>MonoidWithZero M<VAR>x r : M<VAR>hr : r ∈ M⁰<GOAL>x * r = 0 ↔ x = 0
<VAR>M : Type u_2<VAR>MonoidWithZero M<VAR>x : M<VAR>c : ↥M⁰<GOAL>x * ↑c = 0 ↔ x = 0
<VAR>M₁ : Type u_4<VAR>CommMonoidWithZero M₁<VAR>r x : M₁<VAR>hr : r ∈ M₁⁰<GOAL>r * x = 0 ↔ x = 0
<VAR>M₁ : Type u_4<VAR>CommMonoidWithZero M₁<VAR>c : ↥M₁⁰<VAR>x : M₁<GOAL>↑c * x = 0 ↔ x = 0
<VAR>R : Type u_5<VAR>Ring R<VAR>x y r : R<VAR>hr : r ∈ R⁰<GOAL>x * r = y * r ↔ x = y
<VAR>R : Type u_5<VAR>Ring R<VAR>x y : R<VAR>c : ↥R⁰<GOAL>x * ↑c = y * ↑c ↔ x = y
<VAR>R' : Type u_6<VAR>CommRing R'<VAR>x y r : R'<VAR>hr : r ∈ R'⁰<GOAL>r * x = r * y ↔ x = y
<VAR>R' : Type u_6<VAR>CommRing R'<VAR>x y : R'<VAR>c : ↥R'⁰<GOAL>↑c * x = ↑c * y ↔ x = y
<VAR>R' : Type u_6<VAR>CommRing R'<VAR>x y r : R'<VAR>hr : r ∈ R'⁰<GOAL>x * r ∣ y * r ↔ x ∣ y
<VAR>R' : Type u_6<VAR>CommRing R'<VAR>x y : R'<VAR>c : ↥R'⁰<GOAL>x * ↑c ∣ y * ↑c ↔ x ∣ y
<VAR>R' : Type u_6<VAR>CommRing R'<VAR>x y r : R'<VAR>hr : r ∈ R'⁰<GOAL>r * x ∣ r * y ↔ x ∣ y
<VAR>R' : Type u_6<VAR>CommRing R'<VAR>x y : R'<VAR>c : ↥R'⁰<GOAL>↑c * x ∣ ↑c * y ↔ x ∣ y
<VAR>M : Type u_2<VAR>MonoidWithZero M<VAR>Nontrivial M<GOAL>0 ∉ M⁰
<VAR>M : Type u_2<VAR>MonoidWithZero M<VAR>Nontrivial M<VAR>x : M<VAR>hx : x ∈ M⁰<GOAL>x ≠ 0
<VAR>M : Type u_2<VAR>MonoidWithZero M<VAR>Nontrivial M<VAR>x : ↥M⁰<GOAL>↑x ≠ 0
<VAR>M₁ : Type u_4<VAR>CommMonoidWithZero M₁<VAR>a b : M₁<GOAL>a * b ∈ M₁⁰ ↔ a ∈ M₁⁰ ∧ b ∈ M₁⁰
<VAR>G₀ : Type u_8<VAR>GroupWithZero G₀<VAR>x : G₀<VAR>hx : x ∈ G₀⁰<GOAL>IsUnit x
<VAR>M : Type u_2<VAR>MonoidWithZero M<VAR>a : M<VAR>ha : IsUnit a<GOAL>a ∈ M⁰
<VAR>M : Type u_2<VAR>MonoidWithZero M<VAR>NoZeroDivisors M<VAR>x y : M<VAR>hnx : x ≠ 0<VAR>hxy : y * x = 0<GOAL>y = 0
<VAR>M : Type u_2<VAR>MonoidWithZero M<VAR>NoZeroDivisors M<VAR>x y : M<VAR>hnx : x ≠ 0<VAR>hxy : x * y = 0<GOAL>y = 0
<VAR>M : Type u_2<VAR>MonoidWithZero M<VAR>NoZeroDivisors M<VAR>x : M<VAR>hx : x ≠ 0<GOAL>x ∈ M⁰
<VAR>M : Type u_2<VAR>MonoidWithZero M<VAR>NoZeroDivisors M<VAR>Nontrivial M<VAR>x : M<GOAL>x ∈ M⁰ ↔ x ≠ 0
<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>F : Type u_7<VAR>MonoidWithZero M<VAR>MonoidWithZero M'<VAR>FunLike F M M'<VAR>Nontrivial M<VAR>ZeroHomClass F M M'<VAR>g : F<VAR>hg : Function.Injective ⇑g<VAR>x : M<VAR>h : x ∈ M⁰<GOAL>g x ≠ 0
<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>F : Type u_7<VAR>MonoidWithZero M<VAR>MonoidWithZero M'<VAR>FunLike F M M'<VAR>Nontrivial M<VAR>NoZeroDivisors M'<VAR>ZeroHomClass F M M'<VAR>g : F<VAR>hg : Function.Injective ⇑g<VAR>x : M<VAR>h : x ∈ M⁰<GOAL>g x ∈ M'⁰
<VAR>M : Type u_2<VAR>MonoidWithZero M<VAR>NoZeroDivisors M<VAR>S : Submonoid M<VAR>hS : 0 ∉ S<GOAL>S ≤ M⁰
<VAR>M : Type u_2<VAR>MonoidWithZero M<VAR>NoZeroDivisors M<VAR>a : M<VAR>ha : a ≠ 0<GOAL>Submonoid.powers a ≤ M⁰
<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>F : Type u_7<VAR>MonoidWithZero M<VAR>MonoidWithZero M'<VAR>FunLike F M M'<VAR>NoZeroDivisors M'<VAR>MonoidWithZeroHomClass F M M'<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>S : Submonoid M<VAR>hS : S ≤ M⁰<GOAL>Submonoid.map f S ≤ M'⁰
<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>F : Type u_7<VAR>MonoidWithZero M<VAR>MonoidWithZero M'<VAR>FunLike F M M'<VAR>NoZeroDivisors M'<VAR>MonoidWithZeroHomClass F M M'<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>M⁰ ≤ Submonoid.comap f M'⁰
<VAR>R : Type u_5<VAR>Ring R<VAR>Finite R<VAR>a : R<GOAL>IsUnit a ↔ a ∈ R⁰
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>MonoidWithZero R<VAR>Zero M<VAR>MulAction R M<VAR>x : R<GOAL>x ∈ nonZeroSMulDivisors R M ↔ ∀ (m : M), x • m = 0 → m = 0
<VAR>R : Type u_2<VAR>MonoidWithZero R<GOAL>(nonZeroSMulDivisors Rᵐᵒᵖ R).unop = R⁰
<VAR>R : Type u_2<VAR>MonoidWithZero R<GOAL>nonZeroSMulDivisors Rᵐᵒᵖ R = R⁰.op
<VAR>M₀ : Type u_1<VAR>MonoidWithZero M₀<GOAL>∀ (a : (↥M₀⁰)ˣ), unitsNonZeroDivisorsEquiv a = (↑(Units.map M₀⁰.subtype)).toFun a
<VAR>M₀ : Type u_1<VAR>MonoidWithZero M₀<VAR>u : M₀ˣ<GOAL>↑↑(unitsNonZeroDivisorsEquiv.symm u)⁻¹ = ↑u⁻¹
<VAR>M₀ : Type u_1<VAR>MonoidWithZero M₀<VAR>u : M₀ˣ<GOAL>↑↑(unitsNonZeroDivisorsEquiv.symm u) = ↑u
<VAR>M₀ : Type u_1<VAR>MonoidWithZero M₀<VAR>a b : ↥M₀⁰<GOAL>Associated ↑a ↑b ↔ Associated a b
<VAR>M₀ : Type u_2<VAR>CommMonoidWithZero M₀<VAR>a : M₀<GOAL>Associates.mk a ∈ (Associates M₀)⁰ ↔ a ∈ M₀⁰
<VAR>M₀ : Type u_2<VAR>CommMonoidWithZero M₀<VAR>a : M₀<VAR>ha : ⟦a⟧ ∈ (Associates M₀)⁰<GOAL>associatesNonZeroDivisorsEquiv ⟨⟦a⟧, ha⟩ = ⟦⟨a, ⋯⟩⟧
<VAR>M₀ : Type u_2<VAR>CommMonoidWithZero M₀<VAR>a : M₀<VAR>ha : a ∈ M₀⁰<GOAL>associatesNonZeroDivisorsEquiv.symm ⟦⟨a, ha⟩⟧ = ⟨⟦a⟧, ⋯⟩
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>L : AddSubgroup E<VAR>DiscreteTopology ↥L<VAR>IsZlattice ℝ L<VAR>μ : MeasureTheory.Measure E := by volume_tac<VAR>MeasureTheory.Measure.IsAddHaarMeasure μ<VAR>F : Set E<VAR>h : MeasureTheory.IsAddFundamentalDomain (↥L) F μ<GOAL>Zlattice.covolume L μ = (μ F).toReal
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>L : AddSubgroup E<VAR>DiscreteTopology ↥L<VAR>IsZlattice ℝ L<VAR>μ : MeasureTheory.Measure E := by volume_tac<VAR>MeasureTheory.Measure.IsAddHaarMeasure μ<GOAL>Zlattice.covolume L μ ≠ 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>L : AddSubgroup E<VAR>DiscreteTopology ↥L<VAR>IsZlattice ℝ L<VAR>μ : MeasureTheory.Measure E := by volume_tac<VAR>MeasureTheory.Measure.IsAddHaarMeasure μ<GOAL>0 < Zlattice.covolume L μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>L : AddSubgroup E<VAR>DiscreteTopology ↥L<VAR>IsZlattice ℝ L<VAR>μ : MeasureTheory.Measure E := by volume_tac<VAR>MeasureTheory.Measure.IsAddHaarMeasure μ<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι ℤ ↥L<VAR>b₀ : Basis ι ℝ E<GOAL>Zlattice.covolume L μ = |b₀.det (Subtype.val ∘ ⇑b)| * (μ (Zspan.fundamentalDomain b₀)).toReal
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>L : AddSubgroup (ι → ℝ)<VAR>DiscreteTopology ↥L<VAR>IsZlattice ℝ L<VAR>b : Basis ι ℤ ↥L<GOAL>Zlattice.covolume L MeasureTheory.volume = |(Matrix.of (Subtype.val ∘ ⇑b)).det|
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>self : AddConstMap G H a b<VAR>x : G<GOAL>self.toFun (x + a) = self.toFun x + b
<VAR>F : Type u_1<VAR>G : outParam (Type u_2)<VAR>H : outParam (Type u_3)<VAR>Add G<VAR>Add H<VAR>a : outParam G<VAR>b : outParam H<VAR>FunLike F G H<VAR>self : AddConstMapClass F G H a b<VAR>f : F<VAR>x : G<GOAL>f (x + a) = f x + b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>Add G<VAR>Add H<VAR>AddConstMapClass F G H a b<VAR>f : F<GOAL>Function.Semiconj (⇑f) (fun x => x + a) fun x => x + b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>AddMonoid G<VAR>AddMonoid H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>x : G<VAR>n : ℕ<GOAL>f (x + n • a) = f x + n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddMonoidWithOne G<VAR>AddMonoid H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<VAR>x : G<VAR>n : ℕ<GOAL>f (x + ↑n) = f x + n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddMonoidWithOne G<VAR>Add H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<VAR>x : G<GOAL>f (x + 1) = f x + b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddMonoidWithOne G<VAR>AddMonoid H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<VAR>x : G<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>f (x + OfNat.ofNat n) = f x + OfNat.ofNat n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>AddMonoidWithOne G<VAR>AddMonoidWithOne H<VAR>AddConstMapClass F G H 1 1<VAR>f : F<VAR>x : G<VAR>n : ℕ<GOAL>f (x + ↑n) = f x + ↑n
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>AddMonoidWithOne G<VAR>AddMonoidWithOne H<VAR>AddConstMapClass F G H 1 1<VAR>f : F<VAR>x : G<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>f (x + OfNat.ofNat n) = f x + OfNat.ofNat n
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>AddZeroClass G<VAR>Add H<VAR>AddConstMapClass F G H a b<VAR>f : F<GOAL>f a = f 0 + b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddZeroClass G<VAR>One G<VAR>Add H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<GOAL>f 1 = f 0 + b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>AddMonoid G<VAR>AddMonoid H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>n : ℕ<GOAL>f (n • a) = f 0 + n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddMonoidWithOne G<VAR>AddMonoid H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<VAR>n : ℕ<GOAL>f ↑n = f 0 + n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddMonoidWithOne G<VAR>AddMonoid H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>f (OfNat.ofNat n) = f 0 + OfNat.ofNat n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>AddMonoidWithOne G<VAR>AddMonoidWithOne H<VAR>AddConstMapClass F G H 1 1<VAR>f : F<VAR>n : ℕ<GOAL>f ↑n = f 0 + ↑n
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>AddMonoidWithOne G<VAR>AddMonoidWithOne H<VAR>AddConstMapClass F G H 1 1<VAR>f : F<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>f (OfNat.ofNat n) = f 0 + OfNat.ofNat n
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>AddCommSemigroup G<VAR>Add H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>x : G<GOAL>f (a + x) = f x + b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddCommMonoidWithOne G<VAR>Add H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<VAR>x : G<GOAL>f (1 + x) = f x + b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>AddCommMonoid G<VAR>AddMonoid H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>n : ℕ<VAR>x : G<GOAL>f (n • a + x) = f x + n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddCommMonoidWithOne G<VAR>AddMonoid H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<VAR>n : ℕ<VAR>x : G<GOAL>f (↑n + x) = f x + n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddCommMonoidWithOne G<VAR>AddMonoid H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>x : G<GOAL>f (OfNat.ofNat n + x) = f x + OfNat.ofNat n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>AddCommMonoidWithOne G<VAR>AddMonoidWithOne H<VAR>AddConstMapClass F G H 1 1<VAR>f : F<VAR>n : ℕ<VAR>x : G<GOAL>f (↑n + x) = f x + ↑n
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>AddCommMonoidWithOne G<VAR>AddMonoidWithOne H<VAR>AddConstMapClass F G H 1 1<VAR>f : F<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>x : G<GOAL>f (OfNat.ofNat n + x) = f x + OfNat.ofNat n
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>AddGroup G<VAR>AddGroup H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>x : G<VAR>n : ℕ<GOAL>f (x - n • a) = f x - n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>AddGroup G<VAR>AddGroup H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>x : G<GOAL>f (x - a) = f x - b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddGroup G<VAR>One G<VAR>AddGroup H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<VAR>x : G<GOAL>f (x - 1) = f x - b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddGroupWithOne G<VAR>AddGroup H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<VAR>x : G<VAR>n : ℕ<GOAL>f (x - ↑n) = f x - n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddGroupWithOne G<VAR>AddGroup H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<VAR>x : G<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>f (x - OfNat.ofNat n) = f x - OfNat.ofNat n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>AddGroup G<VAR>AddGroup H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>x : G<VAR>n : ℤ<GOAL>f (x + n • a) = f x + n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>AddGroup G<VAR>AddGroup H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>n : ℤ<GOAL>f (n • a) = f 0 + n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddGroupWithOne G<VAR>AddGroup H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<VAR>x : G<VAR>n : ℤ<GOAL>f (x + ↑n) = f x + n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>AddGroupWithOne G<VAR>AddGroupWithOne H<VAR>AddConstMapClass F G H 1 1<VAR>f : F<VAR>x : G<VAR>n : ℤ<GOAL>f (x + ↑n) = f x + ↑n
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>AddGroup G<VAR>AddGroup H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>x : G<VAR>n : ℤ<GOAL>f (x - n • a) = f x - n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddGroupWithOne G<VAR>AddGroup H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<VAR>x : G<VAR>n : ℤ<GOAL>f (x - ↑n) = f x - n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>AddGroupWithOne G<VAR>AddGroupWithOne H<VAR>AddConstMapClass F G H 1 1<VAR>f : F<VAR>x : G<VAR>n : ℤ<GOAL>f (x - ↑n) = f x - ↑n
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>AddCommGroup G<VAR>AddGroup H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>n : ℤ<VAR>x : G<GOAL>f (n • a + x) = f x + n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>b : H<VAR>AddCommGroupWithOne G<VAR>AddGroup H<VAR>AddConstMapClass F G H 1 b<VAR>f : F<VAR>n : ℤ<VAR>x : G<GOAL>f (↑n + x) = f x + n • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>AddCommGroupWithOne G<VAR>AddGroupWithOne H<VAR>AddConstMapClass F G H 1 1<VAR>f : F<VAR>n : ℤ<VAR>x : G<GOAL>f (↑n + x) = f x + ↑n
<VAR>F : Type u_1<VAR>H : Type u_3<VAR>b : H<VAR>R : Type u_4<VAR>LinearOrderedRing R<VAR>FloorRing R<VAR>AddGroup H<VAR>FunLike F R H<VAR>AddConstMapClass F R H 1 b<VAR>f : F<VAR>x : R<GOAL>f (Int.fract x) = f x - ⌊x⌋ • b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>LinearOrderedAddCommGroup G<VAR>Archimedean G<VAR>AddGroup H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>R : H → H → Prop<VAR>IsTrans H R<VAR>hR : CovariantClass H H (fun x y => y + x) R<VAR>ha : 0 < a<VAR>l : G<VAR>hf : ∀ x ∈ Set.Icc l (l + a), ∀ y ∈ Set.Icc l (l + a), x < y → R (f x) (f y)<GOAL>((fun x x_1 => x < x_1) ⇒ R) ⇑f ⇑f
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>LinearOrderedAddCommGroup G<VAR>Archimedean G<VAR>OrderedAddCommGroup H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>ha : 0 < a<VAR>l : G<GOAL>Monotone ⇑f ↔ MonotoneOn (⇑f) (Set.Icc l (l + a))
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>LinearOrderedAddCommGroup G<VAR>Archimedean G<VAR>OrderedAddCommGroup H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>ha : 0 < a<VAR>l : G<GOAL>Antitone ⇑f ↔ AntitoneOn (⇑f) (Set.Icc l (l + a))
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>LinearOrderedAddCommGroup G<VAR>Archimedean G<VAR>OrderedAddCommGroup H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>ha : 0 < a<VAR>l : G<GOAL>StrictMono ⇑f ↔ StrictMonoOn (⇑f) (Set.Icc l (l + a))
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>FunLike F G H<VAR>a : G<VAR>b : H<VAR>LinearOrderedAddCommGroup G<VAR>Archimedean G<VAR>OrderedAddCommGroup H<VAR>AddConstMapClass F G H a b<VAR>f : F<VAR>ha : 0 < a<VAR>l : G<GOAL>StrictAnti ⇑f ↔ StrictAntiOn (⇑f) (Set.Icc l (l + a))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>f : G → H<VAR>hf : ∀ (x : G), f (x + a) = f x + b<GOAL>⇑{ toFun := f, map_add_const' := hf } = f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>f : AddConstMap G H a b<GOAL>{ toFun := ⇑f, map_add_const' := ⋯ } = f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>f : AddConstMap G H a b<GOAL>f.toFun = ⇑f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>f g : AddConstMap G H a b<VAR>h : ∀ (x : G), f x = g x<GOAL>f = g
<VAR>G : Type u_1<VAR>Add G<VAR>a : G<GOAL>⇑AddConstMap.id = id
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>K : Type u_3<VAR>Add K<VAR>c : K<VAR>g : AddConstMap H K b c<VAR>f : AddConstMap G H a b<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>f : AddConstMap G H a b<GOAL>f.comp AddConstMap.id = f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>f : AddConstMap G H a b<GOAL>AddConstMap.id.comp f = f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Add G<VAR>Add H<VAR>a : G<VAR>b : H<VAR>f : AddConstMap G H a b<VAR>a' : G<VAR>b' : H<VAR>ha : a = a'<VAR>hb : b = b'<GOAL>⇑(f.replaceConsts a' b' ha hb) = ⇑f