ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DecidableEq ι<VAR>G' : ι → Type v'<VAR>(i : ι) → AddCommGroup (G' i)<VAR>(i : ι) → Module R (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>e : (i : ι) → G i ≃ₗ[R] G' i<VAR>he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)<VAR>i : ι<VAR>g : G' i<GOAL>(Module.DirectLimit.congr e he).symm ((Module.DirectLimit.of R ι G' f' i) g) = (Module.DirectLimit.of R ι G f i) ((e i).symm g)
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>i j : ι<VAR>h : i ≤ j<GOAL>Module.DirectLimit.totalize G f i j = f i j h
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>i j : ι<VAR>h : ¬i ≤ j<GOAL>Module.DirectLimit.totalize G f i j = 0
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DecidableEq ι<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>(i : ι) → (k : G i) → Decidable (k ≠ 0)<VAR>x : DirectSum ι G<VAR>i j : ι<VAR>hij : i ≤ j<VAR>hx : ∀ k ∈ DFinsupp.support x, k ≤ i<GOAL>(DirectSum.toModule R ι (G j) fun k => Module.DirectLimit.totalize G f k j) x = (f i j hij) ((DirectSum.toModule R ι (G i) fun k => Module.DirectLimit.totalize G f k i) x)
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DecidableEq ι<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>(i : ι) → (k : G i) → Decidable (k ≠ 0)<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>x : DirectSum ι G<VAR>H : Submodule.Quotient.mk x = 0<GOAL>∃ j, (∀ k ∈ DFinsupp.support x, k ≤ j) ∧ (DirectSum.toModule R ι (G j) fun i => Module.DirectLimit.totalize G f i j) x = 0
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DecidableEq ι<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>x : G i<VAR>H : (Module.DirectLimit.of R ι G f i) x = 0<GOAL>∃ j, ∃ (hij : i ≤ j), (f i j hij) x = 0
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>h : DirectedSystem G fun i j h => ⇑(f i j h)<GOAL>DirectedSystem G fun i j hij => ⇑(f i j hij).toIntLinearMap
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>DecidableEq ι<VAR>(i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>i j : ι<VAR>hij : i ≤ j<VAR>x : G i<GOAL>(AddCommGroup.DirectLimit.of G f j) ((f i j hij) x) = (AddCommGroup.DirectLimit.of G f i) x
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>DecidableEq ι<VAR>(i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>C : AddCommGroup.DirectLimit G f → Prop<VAR>z : AddCommGroup.DirectLimit G f<VAR>ih : ∀ (i : ι) (x : G i), C ((AddCommGroup.DirectLimit.of G f i) x)<GOAL>C z
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>DecidableEq ι<VAR>(i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>i : ι<VAR>x : G i<VAR>h : (AddCommGroup.DirectLimit.of G f i) x = 0<GOAL>∃ j, ∃ (hij : i ≤ j), (f i j hij) x = 0
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>DecidableEq ι<VAR>(i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>AddCommGroup P<VAR>g : (i : ι) → G i →+ P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>i : ι<VAR>x : G i<GOAL>(AddCommGroup.DirectLimit.lift G f P g Hg) ((AddCommGroup.DirectLimit.of G f i) x) = (g i) x
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>DecidableEq ι<VAR>(i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>AddCommGroup P<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : AddCommGroup.DirectLimit G f →+ P<VAR>x : AddCommGroup.DirectLimit G f<GOAL>F x = (AddCommGroup.DirectLimit.lift G f P (fun i => F.comp (AddCommGroup.DirectLimit.of G f i)) ⋯) x
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>DecidableEq ι<VAR>(i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>AddCommGroup P<VAR>g : (i : ι) → G i →+ P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>injective : ∀ (i : ι), Function.Injective ⇑(g i)<GOAL>Function.Injective ⇑(AddCommGroup.DirectLimit.lift G f P g Hg)
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>DecidableEq ι<VAR>(i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>G' : ι → Type v'<VAR>(i : ι) → AddCommGroup (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →+ G' j<VAR>g : (i : ι) → G i →+ G' i<VAR>hg : ∀ (i j : ι) (h : i ≤ j), (g j).comp (f i j h) = (f' i j h).comp (g i)<VAR>i : ι<VAR>x : G i<GOAL>(AddCommGroup.DirectLimit.map g hg) ((AddCommGroup.DirectLimit.of G f i) x) = (AddCommGroup.DirectLimit.of G' f' i) ((g i) x)
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>DecidableEq ι<VAR>(i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<GOAL>AddCommGroup.DirectLimit.map (fun i => AddMonoidHom.id (G i)) ⋯ = AddMonoidHom.id (AddCommGroup.DirectLimit G f)
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>DecidableEq ι<VAR>(i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>G' : ι → Type v'<VAR>(i : ι) → AddCommGroup (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →+ G' j<VAR>G'' : ι → Type v''<VAR>(i : ι) → AddCommGroup (G'' i)<VAR>f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>g₁ : (i : ι) → G i →+ G' i<VAR>g₂ : (i : ι) → G' i →+ G'' i<VAR>hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)<VAR>hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)<GOAL>(AddCommGroup.DirectLimit.map g₂ hg₂).comp (AddCommGroup.DirectLimit.map g₁ hg₁) = AddCommGroup.DirectLimit.map (fun i => (g₂ i).comp (g₁ i)) ⋯
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>DecidableEq ι<VAR>(i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>G' : ι → Type v'<VAR>(i : ι) → AddCommGroup (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →+ G' j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>e : (i : ι) → G i ≃+ G' i<VAR>he : ∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i)<VAR>i : ι<VAR>g : G i<GOAL>(AddCommGroup.DirectLimit.congr e he) ((AddCommGroup.DirectLimit.of G f i) g) = (AddCommGroup.DirectLimit.of G' f' i) ((e i) g)
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>DecidableEq ι<VAR>(i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>G' : ι → Type v'<VAR>(i : ι) → AddCommGroup (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →+ G' j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>e : (i : ι) → G i ≃+ G' i<VAR>he : ∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i)<VAR>i : ι<VAR>g : G' i<GOAL>(AddCommGroup.DirectLimit.congr e he).symm ((AddCommGroup.DirectLimit.of G' f' i) g) = (AddCommGroup.DirectLimit.of G f i) ((e i).symm g)
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>i j : ι<VAR>hij : i ≤ j<VAR>x : G i<GOAL>(Ring.DirectLimit.of G f j) (f i j hij x) = (Ring.DirectLimit.of G f i) x
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>z : Ring.DirectLimit G f<GOAL>∃ i x, (Ring.DirectLimit.of G f i) x = z
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>q : Polynomial (Ring.DirectLimit G fun i j h => ⇑(f' i j h))<GOAL>∃ i p, Polynomial.map (Ring.DirectLimit.of G (fun i j h => ⇑(f' i j h)) i) p = q
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>C : Ring.DirectLimit G f → Prop<VAR>z : Ring.DirectLimit G f<VAR>ih : ∀ (i : ι) (x : G i), C ((Ring.DirectLimit.of G f i) x)<GOAL>C z
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>x : FreeCommRing ((i : ι) × G i)<VAR>s t : Set ((i : ι) × G i)<VAR>DecidablePred fun x => x ∈ s<VAR>DecidablePred fun x => x ∈ t<VAR>hxs : x.IsSupported s<VAR>j k : ι<VAR>hj : ∀ z ∈ s, z.fst ≤ j<VAR>hk : ∀ z ∈ t, z.fst ≤ k<VAR>hjk : j ≤ k<VAR>hst : s ⊆ t<GOAL>(f' j k hjk) ((FreeCommRing.lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((FreeCommRing.restriction s) x)) = (FreeCommRing.lift fun ix => (f' (↑ix).fst k ⋯) (↑ix).snd) ((FreeCommRing.restriction t) x)
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>x : FreeCommRing ((i : ι) × G i)<VAR>H : (Ideal.Quotient.mk (Ideal.span {a | (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, (fun i j h => ⇑(f' i j h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨ (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨ (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨ ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a})) x = 0<GOAL>∃ j s, ∃ (H : ∀ k ∈ s, k.fst ≤ j), x.IsSupported s ∧ ∀ [inst : DecidablePred fun x => x ∈ s], (FreeCommRing.lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((FreeCommRing.restriction s) x) = 0
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>x : G i<VAR>hix : (Ring.DirectLimit.of G (fun i j h => ⇑(f' i j h)) i) x = 0<GOAL>∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ⇑(f' i j hij)<VAR>i : ι<GOAL>Function.Injective ⇑(Ring.DirectLimit.of G (fun i j h => ⇑(f' i j h)) i)
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>P : Type u₁<VAR>CommRing P<VAR>g : (i : ι) → G i →+* P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x<VAR>i : ι<VAR>x : G i<GOAL>(Ring.DirectLimit.lift G f P g Hg) ((Ring.DirectLimit.of G f i) x) = (g i) x
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>P : Type u₁<VAR>CommRing P<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : Ring.DirectLimit G f →+* P<VAR>x : Ring.DirectLimit G f<GOAL>F x = (Ring.DirectLimit.lift G f P (fun i => F.comp (Ring.DirectLimit.of G f i)) ⋯) x
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>P : Type u₁<VAR>CommRing P<VAR>g : (i : ι) → G i →+* P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>injective : ∀ (i : ι), Function.Injective ⇑(g i)<GOAL>Function.Injective ⇑(Ring.DirectLimit.lift G f P g Hg)
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+* G j<VAR>G' : ι → Type v'<VAR>(i : ι) → CommRing (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →+* G' j<VAR>g : (i : ι) → G i →+* G' i<VAR>hg : ∀ (i j : ι) (h : i ≤ j), (g j).comp (f i j h) = (f' i j h).comp (g i)<VAR>i : ι<VAR>x : G i<GOAL>(Ring.DirectLimit.map g hg) ((Ring.DirectLimit.of G (fun x x_1 h => ⇑(f x x_1 h)) i) x) = (Ring.DirectLimit.of G' (fun x x_1 h => ⇑(f' x x_1 h)) i) ((g i) x)
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+* G j<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<GOAL>Ring.DirectLimit.map (fun i => RingHom.id (G i)) ⋯ = RingHom.id (Ring.DirectLimit G fun x x_1 h => ⇑(f x x_1 h))
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+* G j<VAR>G' : ι → Type v'<VAR>(i : ι) → CommRing (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →+* G' j<VAR>G'' : ι → Type v''<VAR>(i : ι) → CommRing (G'' i)<VAR>f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>g₁ : (i : ι) → G i →+* G' i<VAR>g₂ : (i : ι) → G' i →+* G'' i<VAR>hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)<VAR>hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)<GOAL>(Ring.DirectLimit.map g₂ hg₂).comp (Ring.DirectLimit.map g₁ hg₁) = Ring.DirectLimit.map (fun i => (g₂ i).comp (g₁ i)) ⋯
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+* G j<VAR>G' : ι → Type v'<VAR>(i : ι) → CommRing (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →+* G' j<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>e : (i : ι) → G i ≃+* G' i<VAR>he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)<VAR>i : ι<VAR>g : G i<GOAL>(Ring.DirectLimit.congr e he) ((Ring.DirectLimit.of G (fun x x_1 h => ⇑(f x x_1 h)) i) g) = (Ring.DirectLimit.of G' (fun x x_1 h => ⇑(f' x x_1 h)) i) ((e i) g)
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+* G j<VAR>G' : ι → Type v'<VAR>(i : ι) → CommRing (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →+* G' j<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>e : (i : ι) → G i ≃+* G' i<VAR>he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)<VAR>i : ι<VAR>g : G' i<GOAL>(Ring.DirectLimit.congr e he).symm ((Ring.DirectLimit.of G' (fun x x_1 h => ⇑(f' x x_1 h)) i) g) = (Ring.DirectLimit.of G (fun x x_1 h => ⇑(f x x_1 h)) i) ((e i).symm g)
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>(i : ι) → Field (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>p : Ring.DirectLimit G f<GOAL>p ≠ 0 → ∃ y, p * y = 1
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>(i : ι) → Field (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>p : Ring.DirectLimit G f<VAR>hp : p ≠ 0<GOAL>p * Field.DirectLimit.inv G f p = 1
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>(i : ι) → Field (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>p : Ring.DirectLimit G f<VAR>hp : p ≠ 0<GOAL>Field.DirectLimit.inv G f p * p = 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>StarAddMonoid M<VAR>n : ℕ<VAR>x : M<GOAL>star (↑n • x) = ↑n • star x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StarAddMonoid M<VAR>n : ℤ<VAR>x : M<GOAL>star (↑n • x) = ↑n • star x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>DivisionSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>StarAddMonoid M<VAR>n : ℕ<VAR>x : M<GOAL>star ((↑n)⁻¹ • x) = (↑n)⁻¹ • star x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>DivisionRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>StarAddMonoid M<VAR>n : ℤ<VAR>x : M<GOAL>star ((↑n)⁻¹ • x) = (↑n)⁻¹ • star x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>DivisionRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>StarAddMonoid M<VAR>n : ℚ<VAR>x : M<GOAL>star (↑n • x) = ↑n • star x
<VAR>R : Type u_3<VAR>AddCommGroup R<VAR>StarAddMonoid R<VAR>Module ℚ R<VAR>x : R<VAR>n : ℚ<GOAL>star (n • x) = n • star x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>AddCommMonoid A<VAR>StarAddMonoid A<VAR>Module R A<VAR>StarModule R A<GOAL>∀ (a : A), (starLinearEquiv R).symm a = starAddEquiv.invFun a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>AddCommMonoid A<VAR>StarAddMonoid A<VAR>Module R A<VAR>StarModule R A<GOAL>∀ (a : A), (starLinearEquiv R) a = star a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>x : A<GOAL>↑((selfAdjointPart R) x) = ⅟2 • (x + star x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>x : A<GOAL>↑((skewAdjointPart R) x) = ⅟2 • (x - star x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>x : A<GOAL>↑((selfAdjointPart R) x) + ↑((skewAdjointPart R) x) = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>x : A<VAR>hx : IsSelfAdjoint x<GOAL>↑((selfAdjointPart R) x) = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>x : A<VAR>hx : IsSelfAdjoint x<GOAL>(selfAdjointPart R) x = ⟨x, hx⟩
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<GOAL>selfAdjointPart R ∘ₗ (selfAdjoint.submodule R A).subtype = LinearMap.id
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>x : A<VAR>hx : IsSelfAdjoint x<GOAL>(skewAdjointPart R) x = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<GOAL>skewAdjointPart R ∘ₗ (selfAdjoint.submodule R A).subtype = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<GOAL>selfAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<GOAL>skewAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype = LinearMap.id
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>i : A<GOAL>(StarModule.decomposeProdAdjoint R A) i = ((selfAdjointPart R) i, (skewAdjointPart R) i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarMul R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>Invertible 2<VAR>a : ↥(selfAdjoint A) × ↥(skewAdjoint A)<GOAL>(StarModule.decomposeProdAdjoint R A).symm a = (selfAdjoint.submodule R A).subtype a.1 + (skewAdjoint.submodule R A).subtype a.2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarMul A<VAR>Algebra R A<VAR>StarModule R A<VAR>r : R<GOAL>(algebraMap R A) (star r) = star ((algebraMap R A) r)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarMul A<VAR>Algebra R A<VAR>StarModule R A<VAR>r : R<VAR>hr : IsSelfAdjoint r<GOAL>IsSelfAdjoint ((algebraMap R A) r)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarMul A<VAR>Algebra R A<VAR>StarModule R A<VAR>r : R<VAR>h : Function.Injective ⇑(algebraMap R A)<GOAL>IsSelfAdjoint ((algebraMap R A) r) ↔ IsSelfAdjoint r
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ MonCat<GOAL>Quot.mk Setoid.r MonCat.Colimits.Prequotient.one = 1
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ MonCat<VAR>x y : MonCat.Colimits.Prequotient F<GOAL>Quot.mk Setoid.r (x.mul y) = Quot.mk Setoid.r x * Quot.mk Setoid.r y
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ MonCat<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>F.map f ≫ MonCat.Colimits.coconeMorphism F j' = MonCat.Colimits.coconeMorphism F j
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ MonCat<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>x : ↑(F.obj j)<GOAL>(MonCat.Colimits.coconeMorphism F j') ((F.map f) x) = (MonCat.Colimits.coconeMorphism F j) x
<VAR>R : Type u_1<VAR>Mul R<VAR>Star R<VAR>x : R<VAR>self : IsStarNormal x<GOAL>Commute (star x) x
<VAR>R : Type u_1<VAR>Mul R<VAR>Star R<VAR>x : R<GOAL>IsStarNormal x ↔ Commute (star x) x
<VAR>R : Type u_1<VAR>Mul R<VAR>Star R<VAR>x : R<VAR>IsStarNormal x<GOAL>star x * x = x * star x
<VAR>R : Type u_1<VAR>Star R<VAR>TrivialStar R<VAR>r : R<GOAL>IsSelfAdjoint r
<VAR>R : Type u_1<VAR>Star R<VAR>x : R<VAR>hx : IsSelfAdjoint x<GOAL>star x = x
<VAR>R : Type u_1<VAR>Star R<VAR>x : R<GOAL>IsSelfAdjoint x ↔ star x = x
<VAR>R : Type u_1<VAR>InvolutiveStar R<VAR>x : R<GOAL>IsSelfAdjoint (star x) ↔ IsSelfAdjoint x
<VAR>R : Type u_1<VAR>Mul R<VAR>StarMul R<VAR>x : R<GOAL>IsSelfAdjoint (star x * x)
<VAR>R : Type u_1<VAR>Mul R<VAR>StarMul R<VAR>x : R<GOAL>IsSelfAdjoint (x * star x)
<VAR>R : Type u_3<VAR>Mul R<VAR>StarMul R<VAR>x y : R<VAR>hx : IsSelfAdjoint x<VAR>hy : IsSelfAdjoint y<GOAL>Commute x y ↔ IsSelfAdjoint (x * y)
<VAR>F : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Star R<VAR>Star S<VAR>FunLike F R S<VAR>StarHomClass F R S<VAR>x : R<VAR>hx : IsSelfAdjoint x<VAR>f : F<GOAL>IsSelfAdjoint (f x)
<VAR>F : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Star R<VAR>Star S<VAR>FunLike F R S<VAR>StarHomClass F R S<VAR>TrivialStar R<VAR>f : F<VAR>x : R<GOAL>IsSelfAdjoint (f x)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>StarAddMonoid R<GOAL>IsSelfAdjoint 0
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>StarAddMonoid R<VAR>x y : R<VAR>hx : IsSelfAdjoint x<VAR>hy : IsSelfAdjoint y<GOAL>IsSelfAdjoint (x + y)
<VAR>R : Type u_1<VAR>AddGroup R<VAR>StarAddMonoid R<VAR>x : R<VAR>hx : IsSelfAdjoint x<GOAL>IsSelfAdjoint (-x)
<VAR>R : Type u_1<VAR>AddGroup R<VAR>StarAddMonoid R<VAR>x y : R<VAR>hx : IsSelfAdjoint x<VAR>hy : IsSelfAdjoint y<GOAL>IsSelfAdjoint (x - y)
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>StarAddMonoid R<VAR>x : R<GOAL>IsSelfAdjoint (x + star x)
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>StarAddMonoid R<VAR>x : R<GOAL>IsSelfAdjoint (star x + x)
<VAR>R : Type u_1<VAR>Semigroup R<VAR>StarMul R<VAR>x : R<VAR>hx : IsSelfAdjoint x<VAR>z : R<GOAL>IsSelfAdjoint (z * x * star z)
<VAR>R : Type u_1<VAR>Semigroup R<VAR>StarMul R<VAR>x : R<VAR>hx : IsSelfAdjoint x<VAR>z : R<GOAL>IsSelfAdjoint (star z * x * z)
<VAR>R : Type u_1<VAR>Semigroup R<VAR>StarMul R<VAR>x : R<VAR>hx : IsSelfAdjoint x<GOAL>IsStarNormal x
<VAR>R : Type u_1<VAR>MulOneClass R<VAR>StarMul R<GOAL>IsSelfAdjoint 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>x : R<VAR>hx : IsSelfAdjoint x<VAR>n : ℕ<GOAL>IsSelfAdjoint (x ^ n)
<VAR>R : Type u_1<VAR>Semiring R<VAR>StarRing R<VAR>n : ℕ<GOAL>IsSelfAdjoint ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>StarRing R<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>IsSelfAdjoint (OfNat.ofNat n)
<VAR>R : Type u_1<VAR>CommSemigroup R<VAR>StarMul R<VAR>x y : R<VAR>hx : IsSelfAdjoint x<VAR>hy : IsSelfAdjoint y<GOAL>IsSelfAdjoint (x * y)
<VAR>α : Type u_3<VAR>CommSemiring α<VAR>StarRing α<VAR>a : α<VAR>ha : IsSelfAdjoint a<GOAL>(starRingEnd α) a = a
<VAR>R : Type u_1<VAR>Ring R<VAR>StarRing R<VAR>z : ℤ<GOAL>IsSelfAdjoint ↑z
<VAR>R : Type u_1<VAR>DivisionSemiring R<VAR>StarRing R<VAR>x : R<VAR>hx : IsSelfAdjoint x<GOAL>IsSelfAdjoint x⁻¹