ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>Add M<VAR>S : ι → AddSubsemigroup M<VAR>C : (x : M) → x ∈ ⨆ i, S i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯<VAR>mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x + y) ⋯<VAR>x₁ : M<VAR>hx₁ : x₁ ∈ ⨆ i, S i<GOAL>C x₁ hx₁
<VAR>S : Type u_4<VAR>M : Type u_5<VAR>Mul M<VAR>SetLike S M<VAR>self : MulMemClass S M<VAR>s : S<VAR>a b : M<GOAL>a ∈ s → b ∈ s → a * b ∈ s
<VAR>S : Type u_4<VAR>M : Type u_5<VAR>Add M<VAR>SetLike S M<VAR>self : AddMemClass S M<VAR>s : S<VAR>a b : M<GOAL>a ∈ s → b ∈ s → a + b ∈ s
<VAR>M : Type u_4<VAR>Mul M<VAR>self : Subsemigroup M<VAR>a b : M<GOAL>a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
<VAR>M : Type u_4<VAR>Add M<VAR>self : AddSubsemigroup M<VAR>a b : M<GOAL>a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
<VAR>M : Type u_1<VAR>Mul M<VAR>s : Subsemigroup M<VAR>x : M<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>M : Type u_1<VAR>Add M<VAR>s : AddSubsemigroup M<VAR>x : M<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>M : Type u_1<VAR>Mul M<VAR>s : Set M<VAR>x : M<VAR>h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s<GOAL>x ∈ { carrier := s, mul_mem' := h_mul } ↔ x ∈ s
<VAR>M : Type u_1<VAR>Add M<VAR>s : Set M<VAR>x : M<VAR>h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s<GOAL>x ∈ { carrier := s, add_mem' := h_mul } ↔ x ∈ s
<VAR>M : Type u_1<VAR>Mul M<VAR>s : Set M<VAR>h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s<GOAL>↑{ carrier := s, mul_mem' := h_mul } = s
<VAR>M : Type u_1<VAR>Add M<VAR>s : Set M<VAR>h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s<GOAL>↑{ carrier := s, add_mem' := h_mul } = s
<VAR>M : Type u_1<VAR>Add M<VAR>s t : Set M<VAR>h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s<VAR>h_mul' : ∀ {a b : M}, a ∈ t → b ∈ t → a + b ∈ t<GOAL>{ carrier := s, add_mem' := h_mul } ≤ { carrier := t, add_mem' := h_mul' } ↔ s ⊆ t
<VAR>M : Type u_1<VAR>Mul M<VAR>s t : Set M<VAR>h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s<VAR>h_mul' : ∀ {a b : M}, a ∈ t → b ∈ t → a * b ∈ t<GOAL>{ carrier := s, mul_mem' := h_mul } ≤ { carrier := t, mul_mem' := h_mul' } ↔ s ⊆ t
<VAR>M : Type u_1<VAR>Add M<VAR>S T : AddSubsemigroup M<VAR>h : ∀ (x : M), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>M : Type u_1<VAR>Mul M<VAR>S T : Subsemigroup M<VAR>h : ∀ (x : M), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>M : Type u_1<VAR>Add M<VAR>S : AddSubsemigroup M<VAR>s : Set M<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Subsemigroup M<VAR>s : Set M<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>M : Type u_1<VAR>Add M<VAR>S : AddSubsemigroup M<VAR>s : Set M<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Subsemigroup M<VAR>s : Set M<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>M : Type u_1<VAR>Add M<VAR>S : AddSubsemigroup M<VAR>x y : M<GOAL>x ∈ S → y ∈ S → x + y ∈ S
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Subsemigroup M<VAR>x y : M<GOAL>x ∈ S → y ∈ S → x * y ∈ S
<VAR>M : Type u_1<VAR>Add M<VAR>x : M<GOAL>x ∉ ⊥
<VAR>M : Type u_1<VAR>Mul M<VAR>x : M<GOAL>x ∉ ⊥
<VAR>M : Type u_1<VAR>Mul M<VAR>x : M<GOAL>x ∈ ⊤
<VAR>M : Type u_1<VAR>Add M<VAR>x : M<GOAL>x ∈ ⊤
<VAR>M : Type u_1<VAR>Add M<GOAL>↑⊤ = Set.univ
<VAR>M : Type u_1<VAR>Mul M<GOAL>↑⊤ = Set.univ
<VAR>M : Type u_1<VAR>Add M<GOAL>↑⊥ = ∅
<VAR>M : Type u_1<VAR>Mul M<GOAL>↑⊥ = ∅
<VAR>M : Type u_1<VAR>Mul M<VAR>p p' : Subsemigroup M<GOAL>↑(p ⊓ p') = ↑p ∩ ↑p'
<VAR>M : Type u_1<VAR>Add M<VAR>p p' : AddSubsemigroup M<GOAL>↑(p ⊓ p') = ↑p ∩ ↑p'
<VAR>M : Type u_1<VAR>Mul M<VAR>p p' : Subsemigroup M<VAR>x : M<GOAL>x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
<VAR>M : Type u_1<VAR>Add M<VAR>p p' : AddSubsemigroup M<VAR>x : M<GOAL>x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
<VAR>M : Type u_1<VAR>Add M<VAR>S : Set (AddSubsemigroup M)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Set (Subsemigroup M)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>M : Type u_1<VAR>Add M<VAR>S : Set (AddSubsemigroup M)<VAR>x : M<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Set (Subsemigroup M)<VAR>x : M<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>M : Type u_1<VAR>Mul M<VAR>ι : Sort u_4<VAR>S : ι → Subsemigroup M<VAR>x : M<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>M : Type u_1<VAR>Add M<VAR>ι : Sort u_4<VAR>S : ι → AddSubsemigroup M<VAR>x : M<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>M : Type u_1<VAR>Mul M<VAR>ι : Sort u_4<VAR>S : ι → Subsemigroup M<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>M : Type u_1<VAR>Add M<VAR>ι : Sort u_4<VAR>S : ι → AddSubsemigroup M<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>M : Type u_1<VAR>Mul M<VAR>Subsingleton (Subsemigroup M)<GOAL>Subsingleton M
<VAR>M : Type u_1<VAR>Add M<VAR>Subsingleton (AddSubsemigroup M)<GOAL>Subsingleton M
<VAR>M : Type u_1<VAR>Mul M<VAR>s : Set M<VAR>x : M<GOAL>x ∈ Subsemigroup.closure s ↔ ∀ (S : Subsemigroup M), s ⊆ ↑S → x ∈ S
<VAR>M : Type u_1<VAR>Add M<VAR>s : Set M<VAR>x : M<GOAL>x ∈ AddSubsemigroup.closure s ↔ ∀ (S : AddSubsemigroup M), s ⊆ ↑S → x ∈ S
<VAR>M : Type u_1<VAR>Add M<VAR>s : Set M<GOAL>s ⊆ ↑(AddSubsemigroup.closure s)
<VAR>M : Type u_1<VAR>Mul M<VAR>s : Set M<GOAL>s ⊆ ↑(Subsemigroup.closure s)
<VAR>M : Type u_1<VAR>Mul M<VAR>s : Set M<VAR>P : M<VAR>hP : P ∉ Subsemigroup.closure s<GOAL>P ∉ s
<VAR>M : Type u_1<VAR>Add M<VAR>s : Set M<VAR>P : M<VAR>hP : P ∉ AddSubsemigroup.closure s<GOAL>P ∉ s
<VAR>M : Type u_1<VAR>Add M<VAR>s : Set M<VAR>S : AddSubsemigroup M<GOAL>AddSubsemigroup.closure s ≤ S ↔ s ⊆ ↑S
<VAR>M : Type u_1<VAR>Mul M<VAR>s : Set M<VAR>S : Subsemigroup M<GOAL>Subsemigroup.closure s ≤ S ↔ s ⊆ ↑S
<VAR>M : Type u_1<VAR>Mul M<VAR>s t : Set M<VAR>h : s ⊆ t<GOAL>Subsemigroup.closure s ≤ Subsemigroup.closure t
<VAR>M : Type u_1<VAR>Add M<VAR>s t : Set M<VAR>h : s ⊆ t<GOAL>AddSubsemigroup.closure s ≤ AddSubsemigroup.closure t
<VAR>M : Type u_1<VAR>Add M<VAR>s : Set M<VAR>S : AddSubsemigroup M<VAR>h₁ : s ⊆ ↑S<VAR>h₂ : S ≤ AddSubsemigroup.closure s<GOAL>AddSubsemigroup.closure s = S
<VAR>M : Type u_1<VAR>Mul M<VAR>s : Set M<VAR>S : Subsemigroup M<VAR>h₁ : s ⊆ ↑S<VAR>h₂ : S ≤ Subsemigroup.closure s<GOAL>Subsemigroup.closure s = S
<VAR>M : Type u_1<VAR>Add M<VAR>s : Set M<VAR>p : M → Prop<VAR>x : M<VAR>h : x ∈ AddSubsemigroup.closure s<VAR>mem : ∀ x ∈ s, p x<VAR>mul : ∀ (x y : M), p x → p y → p (x + y)<GOAL>p x
<VAR>M : Type u_1<VAR>Mul M<VAR>s : Set M<VAR>p : M → Prop<VAR>x : M<VAR>h : x ∈ Subsemigroup.closure s<VAR>mem : ∀ x ∈ s, p x<VAR>mul : ∀ (x y : M), p x → p y → p (x * y)<GOAL>p x
<VAR>M : Type u_1<VAR>Mul M<VAR>s : Set M<VAR>p : (x : M) → x ∈ Subsemigroup.closure s → Prop<VAR>mem : ∀ (x : M) (h : x ∈ s), p x ⋯<VAR>mul : ∀ (x : M) (hx : x ∈ Subsemigroup.closure s) (y : M) (hy : y ∈ Subsemigroup.closure s), p x hx → p y hy → p (x * y) ⋯<VAR>x : M<VAR>hx : x ∈ Subsemigroup.closure s<GOAL>p x hx
<VAR>M : Type u_1<VAR>Add M<VAR>s : Set M<VAR>p : (x : M) → x ∈ AddSubsemigroup.closure s → Prop<VAR>mem : ∀ (x : M) (h : x ∈ s), p x ⋯<VAR>mul : ∀ (x : M) (hx : x ∈ AddSubsemigroup.closure s) (y : M) (hy : y ∈ AddSubsemigroup.closure s), p x hx → p y hy → p (x + y) ⋯<VAR>x : M<VAR>hx : x ∈ AddSubsemigroup.closure s<GOAL>p x hx
<VAR>M : Type u_1<VAR>Add M<VAR>s : Set M<VAR>p : M → M → Prop<VAR>x y : M<VAR>hx : x ∈ AddSubsemigroup.closure s<VAR>hy : y ∈ AddSubsemigroup.closure s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>Hmul_left : ∀ (x y z : M), p x z → p y z → p (x + y) z<VAR>Hmul_right : ∀ (x y z : M), p z x → p z y → p z (x + y)<GOAL>p x y
<VAR>M : Type u_1<VAR>Mul M<VAR>s : Set M<VAR>p : M → M → Prop<VAR>x y : M<VAR>hx : x ∈ Subsemigroup.closure s<VAR>hy : y ∈ Subsemigroup.closure s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>Hmul_left : ∀ (x y z : M), p x z → p y z → p (x * y) z<VAR>Hmul_right : ∀ (x y z : M), p z x → p z y → p z (x * y)<GOAL>p x y
<VAR>M : Type u_1<VAR>Mul M<VAR>p : M → Prop<VAR>x : M<VAR>s : Set M<VAR>hs : Subsemigroup.closure s = ⊤<VAR>mem : ∀ x ∈ s, p x<VAR>mul : ∀ (x y : M), p x → p y → p (x * y)<GOAL>p x
<VAR>M : Type u_1<VAR>Add M<VAR>p : M → Prop<VAR>x : M<VAR>s : Set M<VAR>hs : AddSubsemigroup.closure s = ⊤<VAR>mem : ∀ x ∈ s, p x<VAR>mul : ∀ (x y : M), p x → p y → p (x + y)<GOAL>p x
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Subsemigroup M<GOAL>Subsemigroup.closure ↑S = S
<VAR>M : Type u_1<VAR>Add M<VAR>S : AddSubsemigroup M<GOAL>AddSubsemigroup.closure ↑S = S
<VAR>M : Type u_1<VAR>Add M<GOAL>AddSubsemigroup.closure ∅ = ⊥
<VAR>M : Type u_1<VAR>Mul M<GOAL>Subsemigroup.closure ∅ = ⊥
<VAR>M : Type u_1<VAR>Add M<GOAL>AddSubsemigroup.closure Set.univ = ⊤
<VAR>M : Type u_1<VAR>Mul M<GOAL>Subsemigroup.closure Set.univ = ⊤
<VAR>M : Type u_1<VAR>Add M<VAR>s t : Set M<GOAL>AddSubsemigroup.closure (s ∪ t) = AddSubsemigroup.closure s ⊔ AddSubsemigroup.closure t
<VAR>M : Type u_1<VAR>Mul M<VAR>s t : Set M<GOAL>Subsemigroup.closure (s ∪ t) = Subsemigroup.closure s ⊔ Subsemigroup.closure t
<VAR>M : Type u_1<VAR>Mul M<VAR>ι : Sort u_4<VAR>s : ι → Set M<GOAL>Subsemigroup.closure (⋃ i, s i) = ⨆ i, Subsemigroup.closure (s i)
<VAR>M : Type u_1<VAR>Add M<VAR>ι : Sort u_4<VAR>s : ι → Set M<GOAL>AddSubsemigroup.closure (⋃ i, s i) = ⨆ i, AddSubsemigroup.closure (s i)
<VAR>M : Type u_1<VAR>Mul M<VAR>m : M<VAR>p : Subsemigroup M<GOAL>Subsemigroup.closure {m} ≤ p ↔ m ∈ p
<VAR>M : Type u_1<VAR>Add M<VAR>m : M<VAR>p : AddSubsemigroup M<GOAL>AddSubsemigroup.closure {m} ≤ p ↔ m ∈ p
<VAR>M : Type u_1<VAR>Add M<VAR>ι : Sort u_4<VAR>p : ι → AddSubsemigroup M<VAR>m : M<GOAL>m ∈ ⨆ i, p i ↔ ∀ (N : AddSubsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
<VAR>M : Type u_1<VAR>Mul M<VAR>ι : Sort u_4<VAR>p : ι → Subsemigroup M<VAR>m : M<GOAL>m ∈ ⨆ i, p i ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
<VAR>M : Type u_1<VAR>Add M<VAR>ι : Sort u_4<VAR>p : ι → AddSubsemigroup M<GOAL>⨆ i, p i = AddSubsemigroup.closure (⋃ i, ↑(p i))
<VAR>M : Type u_1<VAR>Mul M<VAR>ι : Sort u_4<VAR>p : ι → Subsemigroup M<GOAL>⨆ i, p i = Subsemigroup.closure (⋃ i, ↑(p i))
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f g : AddHom M N<VAR>s : Set M<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn ⇑f ⇑g ↑(AddSubsemigroup.closure s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f g : M →ₙ* N<VAR>s : Set M<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn ⇑f ⇑g ↑(Subsemigroup.closure s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f g : AddHom M N<VAR>h : Set.EqOn ⇑f ⇑g ↑⊤<GOAL>f = g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f g : M →ₙ* N<VAR>h : Set.EqOn ⇑f ⇑g ↑⊤<GOAL>f = g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>s : Set M<VAR>hs : Subsemigroup.closure s = ⊤<VAR>f g : M →ₙ* N<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>s : Set M<VAR>hs : AddSubsemigroup.closure s = ⊤<VAR>f g : AddHom M N<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Semigroup M<VAR>Semigroup N<VAR>s : Set M<VAR>f : M → N<VAR>hs : Subsemigroup.closure s = ⊤<VAR>hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y<GOAL>⇑(MulHom.ofDense f hs hmul) = f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddSemigroup M<VAR>AddSemigroup N<VAR>s : Set M<VAR>f : M → N<VAR>hs : AddSubsemigroup.closure s = ⊤<VAR>hmul : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y<GOAL>⇑(AddHom.ofDense f hs hmul) = f
<VAR>K : Type u_1<VAR>Field K<VAR>s : SimpContFract K<VAR>n : ℕ<VAR>hyp : n = 0 ∨ ¬(↑s).TerminatedAt (n - 1)<GOAL>((↑s).contsAux n).a * ((↑s).contsAux (n + 1)).b - ((↑s).contsAux n).b * ((↑s).contsAux (n + 1)).a = (-1) ^ n
<VAR>K : Type u_1<VAR>Field K<VAR>s : SimpContFract K<VAR>n : ℕ<VAR>not_terminatedAt_n : ¬(↑s).TerminatedAt n<GOAL>(↑s).nums n * (↑s).dens (n + 1) - (↑s).dens n * (↑s).nums (n + 1) = (-1) ^ (n + 1)
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>n : ℕ<GOAL>∀ (x : α), (nsmulAddMonoidHom n) x = n • x
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>n : ℕ<GOAL>∀ (x : α), (powMonoidHom n) x = x ^ n
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>n : ℤ<GOAL>∀ (x : α), (zpowGroupHom n) x = x ^ n
<VAR>α : Type u_1<VAR>SubtractionCommMonoid α<VAR>n : ℤ<GOAL>∀ (x : α), (zsmulAddGroupHom n) x = n • x
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<GOAL>⇑invMonoidHom = Inv.inv
<VAR>α : Type u_1<VAR>DivisionCommMonoid α<VAR>a : α<GOAL>invMonoidHom a = a⁻¹
<VAR>M : Type u_9<VAR>N : Type u_10<VAR>Add M<VAR>AddCommSemigroup N<VAR>f g : AddHom M N<VAR>x : M<GOAL>(f + g) x = f x + g x
<VAR>M : Type u_9<VAR>N : Type u_10<VAR>Mul M<VAR>CommSemigroup N<VAR>f g : M →ₙ* N<VAR>x : M<GOAL>(f * g) x = f x * g x
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>Mul M<VAR>Mul N<VAR>CommSemigroup P<VAR>g₁ g₂ : N →ₙ* P<VAR>f : M →ₙ* N<GOAL>(g₁ * g₂).comp f = g₁.comp f * g₂.comp f
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>Add M<VAR>Add N<VAR>AddCommSemigroup P<VAR>g₁ g₂ : AddHom N P<VAR>f : AddHom M N<GOAL>(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>Mul M<VAR>CommSemigroup N<VAR>CommSemigroup P<VAR>g : N →ₙ* P<VAR>f₁ f₂ : M →ₙ* N<GOAL>g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>Add M<VAR>AddCommSemigroup N<VAR>AddCommSemigroup P<VAR>g : AddHom N P<VAR>f₁ f₂ : AddHom M N<GOAL>g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
<VAR>F : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>AddGroup G<VAR>AddZeroClass H<VAR>FunLike F G H<VAR>AddMonoidHomClass F G H<VAR>f : F<GOAL>Function.Injective ⇑f ↔ ∀ (a : G), f a = 0 → a = 0
<VAR>F : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>Group G<VAR>MulOneClass H<VAR>FunLike F G H<VAR>MonoidHomClass F G H<VAR>f : F<GOAL>Function.Injective ⇑f ↔ ∀ (a : G), f a = 1 → a = 1
<VAR>F : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>AddGroup G<VAR>AddZeroClass H<VAR>FunLike F G H<VAR>AddMonoidHomClass F G H<VAR>f : F<GOAL>Function.Injective ⇑f ↔ ∀ (a : G), f a = 0 ↔ a = 0
<VAR>F : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>Group G<VAR>MulOneClass H<VAR>FunLike F G H<VAR>MonoidHomClass F G H<VAR>f : F<GOAL>Function.Injective ⇑f ↔ ∀ (a : G), f a = 1 ↔ a = 1
<VAR>G : Type u_6<VAR>Group G<VAR>H : Type u_9<VAR>Group H<VAR>f : G → H<VAR>map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹<GOAL>⇑(MonoidHom.ofMapMulInv f map_div) = f
<VAR>G : Type u_6<VAR>AddGroup G<VAR>H : Type u_9<VAR>AddGroup H<VAR>f : G → H<VAR>map_div : ∀ (a b : G), f (a + -b) = f a + -f b<GOAL>⇑(AddMonoidHom.ofMapAddNeg f map_div) = f
<VAR>G : Type u_6<VAR>Group G<VAR>H : Type u_9<VAR>Group H<VAR>f : G → H<VAR>hf : ∀ (x y : G), f (x / y) = f x / f y<GOAL>⇑(MonoidHom.ofMapDiv f hf) = f
<VAR>G : Type u_6<VAR>AddGroup G<VAR>H : Type u_9<VAR>AddGroup H<VAR>f : G → H<VAR>hf : ∀ (x y : G), f (x - y) = f x - f y<GOAL>⇑(AddMonoidHom.ofMapSub f hf) = f
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>MulOneClass M<VAR>CommMonoid N<VAR>f g : M →* N<VAR>x : M<GOAL>(f * g) x = f x * g x
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>AddZeroClass M<VAR>AddCommMonoid N<VAR>f g : M →+ N<VAR>x : M<GOAL>(f + g) x = f x + g x
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>MulOneClass M<VAR>CommMonoid N<VAR>MulOneClass P<VAR>g₁ g₂ : M →* N<VAR>f : P →* M<GOAL>(g₁ * g₂).comp f = g₁.comp f * g₂.comp f
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>AddZeroClass M<VAR>AddCommMonoid N<VAR>AddZeroClass P<VAR>g₁ g₂ : M →+ N<VAR>f : P →+ M<GOAL>(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>AddZeroClass M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>g : N →+ P<VAR>f₁ f₂ : M →+ N<GOAL>g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>MulOneClass M<VAR>CommMonoid N<VAR>CommMonoid P<VAR>g : N →* P<VAR>f₁ f₂ : M →* N<GOAL>g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
<VAR>M : Type u_3<VAR>G : Type u_6<VAR>AddZeroClass M<VAR>AddCommGroup G<VAR>f : M →+ G<VAR>x : M<GOAL>(-f) x = -f x
<VAR>M : Type u_3<VAR>G : Type u_6<VAR>MulOneClass M<VAR>CommGroup G<VAR>f : M →* G<VAR>x : M<GOAL>f⁻¹ x = (f x)⁻¹
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>G : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>CommGroup G<VAR>φ : N →* G<VAR>ψ : M →* N<GOAL>φ⁻¹.comp ψ = (φ.comp ψ)⁻¹
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>G : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddCommGroup G<VAR>φ : N →+ G<VAR>ψ : M →+ N<GOAL>(-φ).comp ψ = -φ.comp ψ
<VAR>M : Type u_3<VAR>G : Type u_6<VAR>H : Type u_7<VAR>MulOneClass M<VAR>CommGroup G<VAR>CommGroup H<VAR>φ : G →* H<VAR>ψ : M →* G<GOAL>φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹
<VAR>M : Type u_3<VAR>G : Type u_6<VAR>H : Type u_7<VAR>AddZeroClass M<VAR>AddCommGroup G<VAR>AddCommGroup H<VAR>φ : G →+ H<VAR>ψ : M →+ G<GOAL>φ.comp (-ψ) = -φ.comp ψ
<VAR>M : Type u_3<VAR>G : Type u_6<VAR>MulOneClass M<VAR>CommGroup G<VAR>f g : M →* G<VAR>x : M<GOAL>(f / g) x = f x / g x
<VAR>M : Type u_3<VAR>G : Type u_6<VAR>AddZeroClass M<VAR>AddCommGroup G<VAR>f g : M →+ G<VAR>x : M<GOAL>(f - g) x = f x - g x
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>G : Type u_6<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddCommGroup G<VAR>f g : N →+ G<VAR>h : M →+ N<GOAL>(f - g).comp h = f.comp h - g.comp h
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>G : Type u_6<VAR>MulOneClass M<VAR>MulOneClass N<VAR>CommGroup G<VAR>f g : N →* G<VAR>h : M →* N<GOAL>(f / g).comp h = f.comp h / g.comp h
<VAR>M : Type u_3<VAR>G : Type u_6<VAR>H : Type u_7<VAR>AddZeroClass M<VAR>AddCommGroup G<VAR>AddCommGroup H<VAR>f : G →+ H<VAR>g h : M →+ G<GOAL>f.comp (g - h) = f.comp g - f.comp h
<VAR>M : Type u_3<VAR>G : Type u_6<VAR>H : Type u_7<VAR>MulOneClass M<VAR>CommGroup G<VAR>CommGroup H<VAR>f : G →* H<VAR>g h : M →* G<GOAL>f.comp (g / h) = f.comp g / f.comp h
<VAR>R : Type u_1<VAR>Zero R<VAR>One R<GOAL>TrivSqZeroExt.fst ε = 0
<VAR>R : Type u_1<VAR>Zero R<VAR>One R<GOAL>TrivSqZeroExt.snd ε = 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>x y : R[ε]<GOAL>TrivSqZeroExt.snd (x * y) = TrivSqZeroExt.fst x * TrivSqZeroExt.snd y + TrivSqZeroExt.snd x * TrivSqZeroExt.fst y
<VAR>R : Type u_1<VAR>Semiring R<GOAL>ε * ε = 0
<VAR>R : Type u_1<VAR>DivisionRing R<GOAL>ε⁻¹ = 0
<VAR>R : Type u_1<VAR>MulZeroOneClass R<VAR>r : R<GOAL>TrivSqZeroExt.inr r = r • ε
<VAR>R : Type u_1<VAR>Semiring R<VAR>x : R[ε]<GOAL>Commute ε x
<VAR>R : Type u_1<VAR>Semiring R<VAR>x : R[ε]<GOAL>Commute x ε
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f g : A[ε] →ₐ[R] B<VAR>hinl : f.comp (TrivSqZeroExt.inlAlgHom R A A) = g.comp (TrivSqZeroExt.inlAlgHom R A A)<VAR>hinr : f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε) = g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε)<GOAL>f = g
<VAR>R : Type u_1<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>f g : R[ε] →ₐ[R] A<VAR>hε : f ε = g ε<GOAL>f = g
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) }<VAR>a : A[ε]<GOAL>(DualNumber.lift fe) a = (↑fe).1 (TrivSqZeroExt.fst a) + (↑fe).1 (TrivSqZeroExt.snd a) * (↑fe).2
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>F : A[ε] →ₐ[R] B<GOAL>↑(DualNumber.lift.symm F) = (F.comp (TrivSqZeroExt.inlAlgHom R A A), F ε)
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }<VAR>a : A<GOAL>(DualNumber.lift fe) (TrivSqZeroExt.inl a) = (↑fe).1 a
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }<VAR>a : A<VAR>ad : A[ε]<GOAL>(DualNumber.lift fe) (a • ad) = (↑fe).1 a * (DualNumber.lift fe) ad
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }<VAR>a : A<VAR>ad : A[ε]<GOAL>(DualNumber.lift fe) (MulOpposite.op a • ad) = (DualNumber.lift fe) ad * (↑fe).1 a
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }<GOAL>(DualNumber.lift fe) ε = (↑fe).2
<VAR>R : Type u_1<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>DualNumber.lift ⟨(TrivSqZeroExt.inlAlgHom R A A, ε), ⋯⟩ = AlgHom.id R A[ε]
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Monoid M<VAR>Monoid N<VAR>Monoid P<VAR>φ : M →* N<VAR>ψ : N →* P<VAR>χ : outParam (M →* P)<VAR>self : φ.CompTriple ψ χ<GOAL>ψ.comp φ = χ
<VAR>M : Type u_2<VAR>Monoid M<VAR>σ : M →* M<VAR>self : MonoidHom.CompTriple.IsId σ<GOAL>σ = MonoidHom.id M
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Monoid M<VAR>Monoid N<VAR>φ : M →* N<VAR>ψ : N →* M<VAR>h : Function.RightInverse ⇑φ ⇑ψ<VAR>χ : M →* M<VAR>MonoidHom.CompTriple.IsId χ<GOAL>φ.CompTriple ψ χ
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Monoid M<VAR>Monoid N<VAR>Monoid P<VAR>φ : M →* N<VAR>ψ : N →* P<GOAL>φ.CompTriple ψ (ψ.comp φ)
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Monoid M<VAR>Monoid N<VAR>Monoid P<VAR>φ : M →* N<VAR>ψ : N →* P<VAR>χ : M →* P<VAR>h : φ.CompTriple ψ χ<VAR>x : M<GOAL>ψ (φ x) = χ x
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Monoid M<VAR>Monoid N<VAR>Monoid P<VAR>Q : Type u_5<VAR>Monoid Q<VAR>φ₁ : M →* N<VAR>φ₂ : N →* P<VAR>φ₁₂ : M →* P<VAR>κ : φ₁.CompTriple φ₂ φ₁₂<VAR>φ₃ : P →* Q<VAR>φ₂₃ : N →* Q<VAR>κ' : φ₂.CompTriple φ₃ φ₂₃<VAR>φ₁₂₃ : M →* Q<GOAL>φ₁.CompTriple φ₂₃ φ₁₂₃ ↔ φ₁₂.CompTriple φ₃ φ₁₂₃
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<GOAL>(((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).X i₁).d i₂ i₂' = (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>i₁ i₁' : I₁<VAR>i₂ : I₂<GOAL>(((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).d i₁ i₁').f i₂ = (F.map (K₁.d i₁ i₁')).app (K₂.X i₂)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ K₂' : HomologicalComplex C₂ c₂<VAR>φ : K₂ ⟶ K₂'<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>(((F.mapBifunctorHomologicalComplexObj c₂ K₁).map φ).f i₁).f i₂ = (F.obj (K₁.X i₁)).map (φ.f i₂)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>(((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).X i₁).X i₂ = (F.obj (K₁.X i₁)).obj (K₂.X i₂)