ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>M : Type u_4<VAR>N : Type u_5<VAR>FunLike F M N<VAR>FunLike G N M<VAR>Monoid M<VAR>Monoid N<VAR>MonoidHomClass G N M<VAR>f : F<VAR>x : M<VAR>g : G<VAR>hfg : Function.LeftInverse ⇑g ⇑f<VAR>h : IsUnit (f x)<GOAL>IsUnit x
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>M : Type u_4<VAR>N : Type u_5<VAR>FunLike F M N<VAR>FunLike G N M<VAR>Monoid M<VAR>Monoid N<VAR>MonoidHomClass F M N<VAR>MonoidHomClass G N M<VAR>f : F<VAR>x : M<VAR>g : G<VAR>hfg : Function.LeftInverse ⇑g ⇑f<GOAL>IsUnit (f x) ↔ IsUnit x
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>M : Type u_4<VAR>N : Type u_5<VAR>FunLike F M N<VAR>FunLike G N M<VAR>AddMonoid M<VAR>AddMonoid N<VAR>AddMonoidHomClass F M N<VAR>AddMonoidHomClass G N M<VAR>f : F<VAR>x : M<VAR>g : G<VAR>hfg : Function.LeftInverse ⇑g ⇑f<GOAL>IsAddUnit (f x) ↔ IsAddUnit x
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddMonoid M<VAR>AddMonoid N<VAR>f : M →+ N<VAR>hf : ∀ (x : M), IsAddUnit (f x)<VAR>x : M<GOAL>↑((IsAddUnit.liftRight f hf) x) = f x
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>hf : ∀ (x : M), IsUnit (f x)<VAR>x : M<GOAL>↑((IsUnit.liftRight f hf) x) = f x
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>h : ∀ (x : M), IsUnit (f x)<VAR>x : M<GOAL>f x * ↑((IsUnit.liftRight f h) x)⁻¹ = 1
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddMonoid M<VAR>AddMonoid N<VAR>f : M →+ N<VAR>h : ∀ (x : M), IsAddUnit (f x)<VAR>x : M<GOAL>f x + ↑(-(IsAddUnit.liftRight f h) x) = 0
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>h : ∀ (x : M), IsUnit (f x)<VAR>x : M<GOAL>↑((IsUnit.liftRight f h) x)⁻¹ * f x = 1
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddMonoid M<VAR>AddMonoid N<VAR>f : M →+ N<VAR>h : ∀ (x : M), IsAddUnit (f x)<VAR>x : M<GOAL>↑(-(IsAddUnit.liftRight f h) x) + f x = 0
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Type u_1<VAR>SetLike S K<VAR>h : SubfieldClass S K<VAR>s : S<VAR>q : ℚ≥0<GOAL>↑q ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Type u_1<VAR>SetLike S K<VAR>h : SubfieldClass S K<VAR>s : S<VAR>q : ℚ<GOAL>↑q ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Type u_1<VAR>SetLike S K<VAR>h : SubfieldClass S K<VAR>s : S<VAR>q : ℚ≥0<GOAL>↑↑q = ↑q
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Type u_1<VAR>SetLike S K<VAR>h : SubfieldClass S K<VAR>s : S<VAR>x : ℚ<GOAL>↑↑x = ↑x
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Type u_1<VAR>SetLike S K<VAR>h : SubfieldClass S K<VAR>x : K<VAR>s : S<VAR>q : ℚ≥0<VAR>hx : x ∈ s<GOAL>q • x ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Type u_1<VAR>SetLike S K<VAR>h : SubfieldClass S K<VAR>x : K<VAR>s : S<VAR>q : ℚ<VAR>hx : x ∈ s<GOAL>q • x ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Type u_1<VAR>SetLike S K<VAR>h : SubfieldClass S K<VAR>s : S<VAR>b : Bool<VAR>n m : ℕ<GOAL>OfScientific.ofScientific n b m ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Type u_1<VAR>SetLike S K<VAR>h : SubfieldClass S K<VAR>s : S<VAR>q : ℚ≥0<VAR>x : ↥s<GOAL>↑(q • x) = q • ↑x
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Type u_1<VAR>SetLike S K<VAR>h : SubfieldClass S K<VAR>s : S<VAR>q : ℚ<VAR>x : ↥s<GOAL>↑(q • x) = q • ↑x
<VAR>K : Type u<VAR>DivisionRing K<VAR>self : Subfield K<VAR>x : K<GOAL>x ∈ self.carrier → x⁻¹ ∈ self.carrier
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x : K<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Subring K<VAR>x : K<VAR>h : ∀ x ∈ S.carrier, x⁻¹ ∈ S.carrier<GOAL>x ∈ { toSubring := S, inv_mem' := h } ↔ x ∈ S
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Subring K<VAR>h : ∀ x ∈ S.carrier, x⁻¹ ∈ S.carrier<GOAL>↑{ toSubring := S, inv_mem' := h } = ↑S
<VAR>K : Type u<VAR>DivisionRing K<VAR>S S' : Subring K<VAR>h : ∀ x ∈ S.carrier, x⁻¹ ∈ S.carrier<VAR>h' : ∀ x ∈ S'.carrier, x⁻¹ ∈ S'.carrier<GOAL>{ toSubring := S, inv_mem' := h } ≤ { toSubring := S', inv_mem' := h' } ↔ S ≤ S'
<VAR>K : Type u<VAR>DivisionRing K<VAR>S T : Subfield K<VAR>h : ∀ (x : K), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Subfield K<VAR>s : Set K<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Subfield K<VAR>s : Set K<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<GOAL>↑s.toSubring = ↑s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x : K<GOAL>x ∈ s.toSubring ↔ x ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<GOAL>1 ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<GOAL>0 ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x y : K<GOAL>x ∈ s → y ∈ s → x * y ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x y : K<GOAL>x ∈ s → y ∈ s → x + y ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x : K<GOAL>x ∈ s → -x ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x y : K<GOAL>x ∈ s → y ∈ s → x - y ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x : K<GOAL>x ∈ s → x⁻¹ ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x y : K<GOAL>x ∈ s → y ∈ s → x / y ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>l : List K<GOAL>(∀ x ∈ l, x ∈ s) → l.prod ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>l : List K<GOAL>(∀ x ∈ l, x ∈ s) → l.sum ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>m : Multiset K<GOAL>(∀ a ∈ m, a ∈ s) → m.sum ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>f : ι → K<VAR>h : ∀ c ∈ t, f c ∈ s<GOAL>∑ i ∈ t, f i ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x : K<VAR>hx : x ∈ s<VAR>n : ℕ<GOAL>x ^ n ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x : K<VAR>hx : x ∈ s<VAR>n : ℤ<GOAL>n • x ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>n : ℤ<GOAL>↑n ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x : K<VAR>hx : x ∈ s<VAR>n : ℤ<GOAL>x ^ n ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x y : ↥s<GOAL>↑(x + y) = ↑x + ↑y
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x y : ↥s<GOAL>↑(x - y) = ↑x - ↑y
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x : ↥s<GOAL>↑(-x) = -↑x
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x y : ↥s<GOAL>↑(x * y) = ↑x * ↑y
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x y : ↥s<GOAL>↑(x / y) = ↑x / ↑y
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x : ↥s<GOAL>↑x⁻¹ = (↑x)⁻¹
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<GOAL>↑0 = 0
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<GOAL>↑1 = 1
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<GOAL>⇑s.subtype = Subtype.val
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Subfield K<GOAL>S.subtype = S.subtype
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x : K<GOAL>x ∈ s.toSubmonoid ↔ x ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<GOAL>↑s.toSubmonoid = ↑s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<VAR>x : K<GOAL>x ∈ s.toAddSubgroup ↔ x ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<GOAL>↑s.toAddSubgroup = ↑s
<VAR>K : Type u<VAR>DivisionRing K<VAR>x : K<GOAL>x ∈ ⊤
<VAR>K : Type u<VAR>DivisionRing K<GOAL>↑⊤ = Set.univ
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<VAR>s : Subfield L<GOAL>↑(Subfield.comap f s) = ⇑f ⁻¹' ↑s
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>s : Subfield L<VAR>f : K →+* L<VAR>x : K<GOAL>x ∈ Subfield.comap f s ↔ f x ∈ s
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>DivisionRing K<VAR>DivisionRing L<VAR>DivisionRing M<VAR>s : Subfield M<VAR>g : L →+* M<VAR>f : K →+* L<GOAL>Subfield.comap f (Subfield.comap g s) = Subfield.comap (g.comp f) s
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>s : Subfield K<VAR>f : K →+* L<GOAL>↑(Subfield.map f s) = ⇑f '' ↑s
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<VAR>s : Subfield K<VAR>y : L<GOAL>y ∈ Subfield.map f s ↔ ∃ x ∈ s, f x = y
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>DivisionRing K<VAR>DivisionRing L<VAR>DivisionRing M<VAR>s : Subfield K<VAR>g : L →+* M<VAR>f : K →+* L<GOAL>Subfield.map g (Subfield.map f s) = Subfield.map (g.comp f) s
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<VAR>s : Subfield K<VAR>t : Subfield L<GOAL>Subfield.map f s ≤ t ↔ s ≤ Subfield.comap f t
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<GOAL>GaloisConnection (Subfield.map f) (Subfield.comap f)
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<GOAL>↑f.fieldRange = Set.range ⇑f
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<VAR>y : L<GOAL>y ∈ f.fieldRange ↔ ∃ x, f x = y
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<GOAL>f.fieldRange = Subfield.map f ⊤
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>DivisionRing K<VAR>DivisionRing L<VAR>DivisionRing M<VAR>g : L →+* M<VAR>f : K →+* L<GOAL>Subfield.map g f.fieldRange = (g.comp f).fieldRange
<VAR>K : Type u<VAR>DivisionRing K<VAR>p p' : Subfield K<GOAL>↑(p ⊓ p') = p.carrier ∩ p'.carrier
<VAR>K : Type u<VAR>DivisionRing K<VAR>p p' : Subfield K<VAR>x : K<GOAL>x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Set (Subfield K)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Set (Subfield K)<VAR>x : K<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Set (Subfield K)<GOAL>(sInf s).toSubring = ⨅ t ∈ s, t.toSubring
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Set (Subfield K)<GOAL>IsGLB S (sInf S)
<VAR>K : Type u<VAR>DivisionRing K<VAR>x : K<VAR>s : Set K<GOAL>x ∈ Subfield.closure s ↔ ∀ (S : Subfield K), s ⊆ ↑S → x ∈ S
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Set K<GOAL>s ⊆ ↑(Subfield.closure s)
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Set K<GOAL>Subring.closure s ≤ (Subfield.closure s).toSubring
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Set K<VAR>P : K<VAR>hP : P ∉ Subfield.closure s<GOAL>P ∉ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Set K<VAR>t : Subfield K<GOAL>Subfield.closure s ≤ t ↔ s ⊆ ↑t
<VAR>K : Type u<VAR>DivisionRing K<VAR>s t : Set K<VAR>h : s ⊆ t<GOAL>Subfield.closure s ≤ Subfield.closure t
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Set K<VAR>t : Subfield K<VAR>h₁ : s ⊆ ↑t<VAR>h₂ : t ≤ Subfield.closure s<GOAL>Subfield.closure s = t
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Set K<VAR>p : K → Prop<VAR>x : K<VAR>h : x ∈ Subfield.closure s<VAR>mem : ∀ x ∈ s, p x<VAR>one : p 1<VAR>add : ∀ (x y : K), p x → p y → p (x + y)<VAR>neg : ∀ (x : K), p x → p (-x)<VAR>inv : ∀ (x : K), p x → p x⁻¹<VAR>mul : ∀ (x y : K), p x → p y → p (x * y)<GOAL>p x
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<GOAL>Subfield.closure ↑s = s
<VAR>K : Type u<VAR>DivisionRing K<GOAL>Subfield.closure ∅ = ⊥
<VAR>K : Type u<VAR>DivisionRing K<GOAL>Subfield.closure Set.univ = ⊤
<VAR>K : Type u<VAR>DivisionRing K<VAR>s t : Set K<GOAL>Subfield.closure (s ∪ t) = Subfield.closure s ⊔ Subfield.closure t
<VAR>K : Type u<VAR>DivisionRing K<VAR>ι : Sort u_1<VAR>s : ι → Set K<GOAL>Subfield.closure (⋃ i, s i) = ⨆ i, Subfield.closure (s i)
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Set (Set K)<GOAL>Subfield.closure (⋃₀ s) = ⨆ t ∈ s, Subfield.closure t
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>s t : Subfield K<VAR>f : K →+* L<GOAL>Subfield.map f (s ⊔ t) = Subfield.map f s ⊔ Subfield.map f t
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>ι : Sort u_1<VAR>f : K →+* L<VAR>s : ι → Subfield K<GOAL>Subfield.map f (iSup s) = ⨆ i, Subfield.map f (s i)
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>s t : Subfield L<VAR>f : K →+* L<GOAL>Subfield.comap f (s ⊓ t) = Subfield.comap f s ⊓ Subfield.comap f t
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>ι : Sort u_1<VAR>f : K →+* L<VAR>s : ι → Subfield L<GOAL>Subfield.comap f (iInf s) = ⨅ i, Subfield.comap f (s i)
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<GOAL>Subfield.map f ⊥ = ⊥
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<GOAL>Subfield.comap f ⊤ = ⊤
<VAR>K : Type u<VAR>DivisionRing K<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subfield K<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : K<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>K : Type u<VAR>DivisionRing K<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subfield K<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<GOAL>↑(⨆ i, S i) = ⋃ i, ↑(S i)
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Set (Subfield K)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : K<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>K : Type u<VAR>DivisionRing K<VAR>S : Set (Subfield K)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<GOAL>↑(sSup S) = ⋃ s ∈ S, ↑s
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<VAR>x : K<GOAL>↑(f.rangeRestrictField x) = f x
<VAR>K : Type u<VAR>DivisionRing K<VAR>L : Type v<VAR>Semiring L<VAR>f g : K →+* L<VAR>s : Set K<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn ⇑f ⇑g ↑(Subfield.closure s)
<VAR>K : Type u<VAR>DivisionRing K<VAR>L : Type v<VAR>Semiring L<VAR>f g : K →+* L<VAR>h : Set.EqOn ⇑f ⇑g ↑⊤<GOAL>f = g
<VAR>K : Type u<VAR>DivisionRing K<VAR>L : Type v<VAR>Semiring L<VAR>s : Set K<VAR>hs : Subfield.closure s = ⊤<VAR>f g : K →+* L<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<VAR>s : Set L<GOAL>Subfield.closure (⇑f ⁻¹' s) ≤ Subfield.comap f (Subfield.closure s)
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<VAR>s : Set K<GOAL>Subfield.map f (Subfield.closure s) = Subfield.closure (⇑f '' s)
<VAR>K : Type u<VAR>DivisionRing K<VAR>s : Subfield K<GOAL>s.subtype.fieldRange = s
<VAR>K : Type u<VAR>Field K<VAR>s : Subfield K<VAR>m : Multiset K<GOAL>(∀ a ∈ m, a ∈ s) → m.prod ∈ s
<VAR>K : Type u<VAR>Field K<VAR>s : Subfield K<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>f : ι → K<VAR>h : ∀ c ∈ t, f c ∈ s<GOAL>∏ i ∈ t, f i ∈ s
<VAR>K : Type u<VAR>Field K<VAR>s : Set K<GOAL>Subfield.commClosure s = Subfield.closure s
<VAR>K : Type u<VAR>Field K<VAR>s : Set K<VAR>x : K<GOAL>x ∈ Subfield.closure s ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<VAR>s : Subfield L<GOAL>Subfield.map f (Subfield.comap f s) = s ⊓ f.fieldRange
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<VAR>s : Subfield L<VAR>h : s ≤ f.fieldRange<GOAL>Subfield.map f (Subfield.comap f s) = s
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<VAR>hf : Function.Surjective ⇑f<VAR>s : Subfield L<GOAL>Subfield.map f (Subfield.comap f s) = s
<VAR>K : Type u<VAR>L : Type v<VAR>DivisionRing K<VAR>DivisionRing L<VAR>f : K →+* L<VAR>s : Subfield K<GOAL>Subfield.comap f (Subfield.map f s) = s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<GOAL>(CochainComplex.mappingCone.triangle φ).obj₃ = CochainComplex.mappingCone φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<GOAL>(CochainComplex.mappingCone.triangle φ).mor₁ = φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<GOAL>(CochainComplex.mappingCone.triangle φ).mor₂ = CochainComplex.mappingCone.inr φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<GOAL>(CochainComplex.mappingCone.triangle φ).obj₁ = K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<GOAL>(CochainComplex.mappingCone.triangle φ).obj₂ = L
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>p q : ℤ<VAR>hpq : p + -1 = q<GOAL>(CochainComplex.mappingCone.inl φ).v p q hpq ≫ (CochainComplex.mappingCone.triangle φ).mor₃.f q = -(K.shiftFunctorObjXIso 1 q p ⋯).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>p : ℤ<GOAL>(CochainComplex.mappingCone.inr φ).f p ≫ (CochainComplex.mappingCone.triangle φ).mor₃.f p = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<GOAL>CochainComplex.mappingCone.inr φ ≫ (CochainComplex.mappingCone.triangle φ).mor₃ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K₁ L₁ K₂ L₂ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)<GOAL>CochainComplex.mappingCone.inr φ₁ ≫ CochainComplex.mappingCone.mapOfHomotopy H = b ≫ CochainComplex.mappingCone.inr φ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K₁ L₁ K₂ L₂ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)<GOAL>CochainComplex.mappingCone.mapOfHomotopy H ≫ (CochainComplex.mappingCone.triangle φ₂).mor₃ = (CochainComplex.mappingCone.triangle φ₁).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K₁ L₁ K₂ L₂ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)<GOAL>(CochainComplex.mappingCone.trianglehMapOfHomotopy H).hom₁ = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K₁ L₁ K₂ L₂ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)<GOAL>(CochainComplex.mappingCone.trianglehMapOfHomotopy H).hom₂ = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map b
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K₁ L₁ K₂ L₂ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)<GOAL>(CochainComplex.mappingCone.trianglehMapOfHomotopy H).hom₃ = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.mapOfHomotopy H)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K₁ L₁ K₂ L₂ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>comm : φ₁ ≫ b = a ≫ φ₂<GOAL>CochainComplex.mappingCone.map φ₁ φ₂ a b comm = CochainComplex.mappingCone.mapOfHomotopy (Homotopy.ofEq comm)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<GOAL>CochainComplex.mappingCone.map φ φ (𝟙 K) (𝟙 L) ⋯ = 𝟙 (CochainComplex.mappingCone φ)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>φ₃ : K₃ ⟶ L₃<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>comm : φ₁ ≫ b = a ≫ φ₂<VAR>a' : K₂ ⟶ K₃<VAR>b' : L₂ ⟶ L₃<VAR>comm' : φ₂ ≫ b' = a' ≫ φ₃<GOAL>CochainComplex.mappingCone.map φ₁ φ₃ (a ≫ a') (b ≫ b') ⋯ = CochainComplex.mappingCone.map φ₁ φ₂ a b comm ≫ CochainComplex.mappingCone.map φ₂ φ₃ a' b' comm'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K₁ L₁ K₂ L₂ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>comm : φ₁ ≫ b = a ≫ φ₂<GOAL>(CochainComplex.mappingCone.triangleMap φ₁ φ₂ a b comm).hom₃ = CochainComplex.mappingCone.map φ₁ φ₂ a b comm
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K₁ L₁ K₂ L₂ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>comm : φ₁ ≫ b = a ≫ φ₂<GOAL>(CochainComplex.mappingCone.triangleMap φ₁ φ₂ a b comm).hom₂ = b
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K₁ L₁ K₂ L₂ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>comm : φ₁ ≫ b = a ≫ φ₂<GOAL>(CochainComplex.mappingCone.triangleMap φ₁ φ₂ a b comm).hom₁ = a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<GOAL>(HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle φ).mor₃ ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.inr (CochainComplex.mappingCone.inr φ))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<GOAL>(CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom ≫ (CochainComplex.mappingCone.triangle (CochainComplex.mappingCone.inr φ)).mor₃ = -(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Limits.HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>G : C ⥤ D<VAR>G.Additive<GOAL>(G.mapHomologicalComplex (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle φ).mor₃ ≫ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso 1).hom.app K = (CochainComplex.mappingCone.mapHomologicalComplexIso φ G).hom ≫ (CochainComplex.mappingCone.triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>T₁ : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))<VAR>hT₁ : T₁ ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C<VAR>T₂ : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))<VAR>e : T₂ ≅ T₁<GOAL>T₂ ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X : HomotopyCategory C (ComplexShape.up ℤ)<GOAL>CategoryTheory.Pretriangulated.contractibleTriangle X ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X Y : HomotopyCategory C (ComplexShape.up ℤ)<VAR>f : X ⟶ Y<GOAL>∃ Z g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C