ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>Ring R<VAR>S : Type v<VAR>Semiring S<VAR>s : Set R<VAR>hs : Subring.closure s = ⊤<VAR>f g : R →+* S<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>s : Set S<GOAL>Subring.closure (⇑f ⁻¹' s) ≤ Subring.comap f (Subring.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>s : Set R<GOAL>Subring.map f (Subring.closure s) = Subring.closure (⇑f '' s)
<VAR>R : Type u<VAR>Ring R<VAR>s : Subring R<GOAL>s.subtype.range = s
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<GOAL>(RingHom.fst R S).rangeS = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<GOAL>(RingHom.snd R S).rangeS = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>s : Subring R<VAR>t : Subring S<GOAL>s.prod ⊥ ⊔ ⊥.prod t = s.prod t
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>g : S → R<VAR>f : R →+* S<VAR>h : Function.LeftInverse g ⇑f<VAR>x : R<GOAL>↑((RingEquiv.ofLeftInverse h) x) = f x
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>g : S → R<VAR>f : R →+* S<VAR>h : Function.LeftInverse g ⇑f<VAR>x : ↥f.range<GOAL>(RingEquiv.ofLeftInverse h).symm x = g ↑x
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>s : Subring R<VAR>e : R ≃+* S<VAR>y : ↑(⇑↑e.toAddEquiv '' ↑s.toAddSubmonoid)<GOAL>↑(e.subringMap.symm y) = (↑e).symm ↑y
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>s : Subring R<VAR>e : R ≃+* S<VAR>x : ↑↑s.toAddSubmonoid<GOAL>↑(e.subringMap x) = e ↑x
<VAR>R : Type u<VAR>Ring R<VAR>s : Set R<VAR>C : R → Prop<VAR>x : R<VAR>hx : x ∈ Subring.closure s<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<GOAL>C x
<VAR>R : Type u<VAR>Ring R<VAR>G : AddSubgroup R<VAR>k : ℤ<VAR>g : R<VAR>h : g ∈ G<GOAL>↑k * g ∈ G
<VAR>R : Type u<VAR>Ring R<VAR>α : Type u_1<VAR>SMul R α<VAR>S : Subring R<VAR>g : ↥S<VAR>m : α<GOAL>g • m = ↑g • m
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>t : Subring S<GOAL>Subring.map f (Subring.comap f t) = t ⊓ f.range
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>t : Subring S<VAR>h : t ≤ f.range<GOAL>Subring.map f (Subring.comap f t) = t
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>t : Subring S<GOAL>Subring.map f (Subring.comap f t) = t
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>s : Subring R<GOAL>Subring.comap f (Subring.map f s) = s ⊔ Subring.closure (⇑f ⁻¹' {0})
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>s : Subring R<VAR>h : ⇑f ⁻¹' {0} ⊆ ↑s<GOAL>Subring.comap f (Subring.map f s) = s
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>s : Subring R<GOAL>Subring.comap f (Subring.map f s) = s
<VAR>G : Type u_1<VAR>Group G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<GOAL>BddAbove s⁻¹ ↔ BddBelow s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<GOAL>BddAbove (-s) ↔ BddBelow s
<VAR>G : Type u_1<VAR>Group G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<GOAL>BddBelow s⁻¹ ↔ BddAbove s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<GOAL>BddBelow (-s) ↔ BddAbove s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>h : BddAbove s<GOAL>BddBelow (-s)
<VAR>G : Type u_1<VAR>Group G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>h : BddAbove s<GOAL>BddBelow s⁻¹
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>h : BddBelow s<GOAL>BddAbove (-s)
<VAR>G : Type u_1<VAR>Group G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>h : BddBelow s<GOAL>BddAbove s⁻¹
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>a : G<GOAL>IsLUB (-s) a ↔ IsGLB s (-a)
<VAR>G : Type u_1<VAR>Group G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>a : G<GOAL>IsLUB s⁻¹ a ↔ IsGLB s a⁻¹
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>a : G<GOAL>IsLUB (-s) (-a) ↔ IsGLB s a
<VAR>G : Type u_1<VAR>Group G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>a : G<GOAL>IsLUB s⁻¹ a⁻¹ ↔ IsGLB s a
<VAR>G : Type u_1<VAR>Group G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>a : G<VAR>h : IsGLB s a<GOAL>IsLUB s⁻¹ a⁻¹
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>a : G<VAR>h : IsGLB s a<GOAL>IsLUB (-s) (-a)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>a : G<GOAL>IsGLB (-s) a ↔ IsLUB s (-a)
<VAR>G : Type u_1<VAR>Group G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>a : G<GOAL>IsGLB s⁻¹ a ↔ IsLUB s a⁻¹
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>a : G<GOAL>IsGLB (-s) (-a) ↔ IsLUB s a
<VAR>G : Type u_1<VAR>Group G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>a : G<GOAL>IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a
<VAR>G : Type u_1<VAR>Group G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>a : G<VAR>h : IsLUB s a<GOAL>IsGLB s⁻¹ a⁻¹
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Set G<VAR>a : G<VAR>h : IsLUB s a<GOAL>IsGLB (-s) (-a)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>α : Type u_2<VAR>f : α → G<VAR>hf : BddBelow (Set.range f)<GOAL>BddAbove (Set.range fun x => -f x)
<VAR>G : Type u_1<VAR>Group G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>α : Type u_2<VAR>f : α → G<VAR>hf : BddBelow (Set.range f)<GOAL>BddAbove (Set.range fun x => (f x)⁻¹)
<VAR>G : Type u_1<VAR>Group G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>α : Type u_2<VAR>f : α → G<VAR>hf : BddAbove (Set.range f)<GOAL>BddBelow (Set.range fun x => (f x)⁻¹)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Preorder G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>α : Type u_2<VAR>f : α → G<VAR>hf : BddAbove (Set.range f)<GOAL>BddBelow (Set.range fun x => -f x)
<VAR>M : Type u_1<VAR>Mul M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set M<VAR>a b : M<VAR>ha : a ∈ upperBounds s<VAR>hb : b ∈ upperBounds t<GOAL>a * b ∈ upperBounds (s * t)
<VAR>M : Type u_1<VAR>Add M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set M<VAR>a b : M<VAR>ha : a ∈ upperBounds s<VAR>hb : b ∈ upperBounds t<GOAL>a + b ∈ upperBounds (s + t)
<VAR>M : Type u_1<VAR>Mul M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set M<GOAL>upperBounds s * upperBounds t ⊆ upperBounds (s * t)
<VAR>M : Type u_1<VAR>Add M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set M<GOAL>upperBounds s + upperBounds t ⊆ upperBounds (s + t)
<VAR>M : Type u_1<VAR>Mul M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set M<VAR>a b : M<VAR>ha : a ∈ lowerBounds s<VAR>hb : b ∈ lowerBounds t<GOAL>a * b ∈ lowerBounds (s * t)
<VAR>M : Type u_1<VAR>Add M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set M<VAR>a b : M<VAR>ha : a ∈ lowerBounds s<VAR>hb : b ∈ lowerBounds t<GOAL>a + b ∈ lowerBounds (s + t)
<VAR>M : Type u_1<VAR>Mul M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set M<GOAL>lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t)
<VAR>M : Type u_1<VAR>Add M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set M<GOAL>lowerBounds s + lowerBounds t ⊆ lowerBounds (s + t)
<VAR>M : Type u_1<VAR>Add M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set M<VAR>hs : BddAbove s<VAR>ht : BddAbove t<GOAL>BddAbove (s + t)
<VAR>M : Type u_1<VAR>Mul M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set M<VAR>hs : BddAbove s<VAR>ht : BddAbove t<GOAL>BddAbove (s * t)
<VAR>M : Type u_1<VAR>Add M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set M<VAR>hs : BddBelow s<VAR>ht : BddBelow t<GOAL>BddBelow (s + t)
<VAR>M : Type u_1<VAR>Mul M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set M<VAR>hs : BddBelow s<VAR>ht : BddBelow t<GOAL>BddBelow (s * t)
<VAR>M : Type u_1<VAR>Mul M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>α : Type u_2<VAR>f g : α → M<VAR>hf : BddAbove (Set.range f)<VAR>hg : BddAbove (Set.range g)<GOAL>BddAbove (Set.range fun x => f x * g x)
<VAR>M : Type u_1<VAR>Add M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>α : Type u_2<VAR>f g : α → M<VAR>hf : BddAbove (Set.range f)<VAR>hg : BddAbove (Set.range g)<GOAL>BddAbove (Set.range fun x => f x + g x)
<VAR>M : Type u_1<VAR>Mul M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>α : Type u_2<VAR>f g : α → M<VAR>hf : BddBelow (Set.range f)<VAR>hg : BddBelow (Set.range g)<GOAL>BddBelow (Set.range fun x => f x * g x)
<VAR>M : Type u_1<VAR>Add M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>α : Type u_2<VAR>f g : α → M<VAR>hf : BddBelow (Set.range f)<VAR>hg : BddBelow (Set.range g)<GOAL>BddBelow (Set.range fun x => f x + g x)
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>ConditionallyCompleteLattice G<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>Nonempty ι<VAR>f : ι → G<VAR>hf : BddAbove (Set.range f)<VAR>a : G<GOAL>(⨆ i, f i) * a = ⨆ i, f i * a
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>ConditionallyCompleteLattice G<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Nonempty ι<VAR>f : ι → G<VAR>hf : BddAbove (Set.range f)<VAR>a : G<GOAL>(⨆ i, f i) + a = ⨆ i, f i + a
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>ConditionallyCompleteLattice G<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>Nonempty ι<VAR>f : ι → G<VAR>hf : BddAbove (Set.range f)<VAR>a : G<GOAL>(⨆ i, f i) / a = ⨆ i, f i / a
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>ConditionallyCompleteLattice G<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Nonempty ι<VAR>f : ι → G<VAR>hf : BddAbove (Set.range f)<VAR>a : G<GOAL>(⨆ i, f i) - a = ⨆ i, f i - a
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>ConditionallyCompleteLattice G<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Nonempty ι<VAR>f : ι → G<VAR>hf : BddBelow (Set.range f)<VAR>a : G<GOAL>(⨅ i, f i) + a = ⨅ i, f i + a
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>ConditionallyCompleteLattice G<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>Nonempty ι<VAR>f : ι → G<VAR>hf : BddBelow (Set.range f)<VAR>a : G<GOAL>(⨅ i, f i) * a = ⨅ i, f i * a
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>ConditionallyCompleteLattice G<VAR>CovariantClass G G (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>Nonempty ι<VAR>f : ι → G<VAR>hf : BddBelow (Set.range f)<VAR>a : G<GOAL>(⨅ i, f i) / a = ⨅ i, f i / a
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>ConditionallyCompleteLattice G<VAR>CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Nonempty ι<VAR>f : ι → G<VAR>hf : BddBelow (Set.range f)<VAR>a : G<GOAL>(⨅ i, f i) - a = ⨅ i, f i - a
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>Group G<VAR>ConditionallyCompleteLattice G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>Nonempty ι<VAR>f : ι → G<VAR>hf : BddAbove (Set.range f)<VAR>a : G<GOAL>a * ⨆ i, f i = ⨆ i, a * f i
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>ConditionallyCompleteLattice G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Nonempty ι<VAR>f : ι → G<VAR>hf : BddAbove (Set.range f)<VAR>a : G<GOAL>a + ⨆ i, f i = ⨆ i, a + f i
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>Group G<VAR>ConditionallyCompleteLattice G<VAR>CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>Nonempty ι<VAR>f : ι → G<VAR>hf : BddBelow (Set.range f)<VAR>a : G<GOAL>a * ⨅ i, f i = ⨅ i, a * f i
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>ConditionallyCompleteLattice G<VAR>CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Nonempty ι<VAR>f : ι → G<VAR>hf : BddBelow (Set.range f)<VAR>a : G<GOAL>a + ⨅ i, f i = ⨅ i, a + f i
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>f : R →ₙ+* S<VAR>g : S → R<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>∀ (a : S), (f.inverse g h₁ h₂) a = g a
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>g : S → R<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>∀ (a : S), (f.inverse g h₁ h₂) a = g a
<VAR>F : Type u_7<VAR>R : Type u_8<VAR>S : Type u_9<VAR>Mul R<VAR>Add R<VAR>Mul S<VAR>Add S<VAR>EquivLike F R S<VAR>self : RingEquivClass F R S<VAR>f : F<VAR>a b : R<GOAL>f (a + b) = f a + f b
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>f : R ≃+* S<GOAL>f.toEquiv = ↑f
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>f : R ≃+* S<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>e : R ≃+* S<VAR>x y : R<GOAL>e (x * y) = e x * e y
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>e : R ≃+* S<VAR>x y : R<GOAL>e (x + y) = e x + e y
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>f g : R ≃+* S<VAR>h : ∀ (x : R), f x = g x<GOAL>f = g
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>e : R ≃ S<VAR>h₃ : ∀ (x y : R), e.toFun (x * y) = e.toFun x * e.toFun y<VAR>h₄ : ∀ (x y : R), e.toFun (x + y) = e.toFun x + e.toFun y<GOAL>⇑{ toEquiv := e, map_mul' := h₃, map_add' := h₄ } = ⇑e
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>e : R ≃+* S<VAR>e' : S → R<VAR>h₁ : Function.LeftInverse e' ⇑e<VAR>h₂ : Function.RightInverse e' ⇑e<VAR>h₃ : ∀ (x y : R), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₄ : ∀ (x y : R), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y<GOAL>{ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ } = e
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>f : R ≃+* S<VAR>x x' : R<GOAL>x = x' → f x = f x'
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>f g : R ≃+* S<VAR>h : f = g<VAR>x : R<GOAL>f x = g x
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>f g : R ≃+* S<GOAL>f = g ↔ ∀ (x : R), f x = g x
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>f : R ≃+* S<GOAL>f.toAddEquiv = ↑f
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>f : R ≃+* S<GOAL>f.toMulEquiv = ↑f
<VAR>R : Type u_4<VAR>Mul R<VAR>Add R<VAR>x : R<GOAL>(RingEquiv.refl R) x = x
<VAR>R : Type u_4<VAR>Mul R<VAR>Add R<GOAL>↑(RingEquiv.refl R) = AddEquiv.refl R
<VAR>R : Type u_4<VAR>Mul R<VAR>Add R<GOAL>↑(RingEquiv.refl R) = MulEquiv.refl R
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>f : R ≃+* S<GOAL>EquivLike.inv f = ⇑f.symm
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>e : R ≃+* S<GOAL>e.symm.symm = e
<VAR>R : Type u_4<VAR>Mul R<VAR>Add R<GOAL>(RingEquiv.refl R).symm = RingEquiv.refl R
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>e : R ≃+* S<GOAL>↑e.symm = (↑e).symm
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<GOAL>Function.Bijective RingEquiv.symm
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>e : R ≃+* S<VAR>f : S → R<VAR>h₁ : Function.LeftInverse (⇑e) f<VAR>h₂ : Function.RightInverse (⇑e) f<VAR>h₃ : ∀ (x y : S), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₄ : ∀ (x y : S), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y<GOAL>{ toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ } = e.symm
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>f : R → S<VAR>g : S → R<VAR>h₁ : Function.LeftInverse g f<VAR>h₂ : Function.RightInverse g f<VAR>h₃ : ∀ (x y : R), { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₄ : ∀ (x y : R), { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toFun y<GOAL>{ toFun := f, invFun := g, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.symm = let __src := RingEquiv.symm_mk.aux f g h₁ h₂ h₃ h₄; { toFun := g, invFun := f, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>Mul S'<VAR>Add S'<VAR>e₁ : R ≃+* S<VAR>e₂ : S ≃+* S'<VAR>a : R<GOAL>(e₁.trans e₂) a = e₂ (e₁ a)
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>Mul S'<VAR>Add S'<VAR>e₁ : R ≃+* S<VAR>e₂ : S ≃+* S'<GOAL>⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>Mul S'<VAR>Add S'<VAR>e₁ : R ≃+* S<VAR>e₂ : S ≃+* S'<VAR>a : S'<GOAL>(e₁.trans e₂).symm a = e₁.symm (e₂.symm a)
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>Mul S'<VAR>Add S'<VAR>e₁ : R ≃+* S<VAR>e₂ : S ≃+* S'<GOAL>(e₁.trans e₂).symm = e₂.symm.trans e₁.symm
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>e : R ≃+* S<GOAL>Function.Bijective ⇑e
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>e : R ≃+* S<GOAL>Function.Injective ⇑e
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>e : R ≃+* S<GOAL>Function.Surjective ⇑e
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>e : R ≃+* S<VAR>x : S<GOAL>e (e.symm x) = x
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>e : R ≃+* S<VAR>x : R<GOAL>e.symm (e x) = x
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>e : R ≃+* S<VAR>s : Set R<GOAL>⇑e '' s = ⇑e.symm ⁻¹' s
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>Mul R<VAR>Mul S<VAR>Add R<VAR>Add S<VAR>Mul S'<VAR>Add S'<VAR>e₁ : R ≃+* S<VAR>e₂ : S ≃+* S'<GOAL>↑(e₁.trans e₂) = (↑e₁).trans ↑e₂
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Add α<VAR>Mul α<VAR>Add β<VAR>Mul β<VAR>f : α ≃+* β<GOAL>∀ (a : βᵐᵒᵖ), (RingEquiv.op f).symm a = MulOpposite.op ((↑f).symm (MulOpposite.unop a))
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Add α<VAR>Mul α<VAR>Add β<VAR>Mul β<VAR>f : αᵐᵒᵖ ≃+* βᵐᵒᵖ<GOAL>∀ (a : β), (RingEquiv.op.symm f).symm a = MulOpposite.unop ((↑f).symm (MulOpposite.op a))