/home/runner/work/lftcm2020/lftcm2020/src/solutions/friday/manifolds.lean:598:18: type mismatch, term rfl has type ?m_2 = ?m_2 but is expected to have type tangent_bundle 𝓡1 myℝ = Σ (x : myℝ), ℝ

Process completed with exit code 1.

/home/runner/work/lftcm2020/lftcm2020/src/hints/category_theory/exercise1/hint1.lean:9:0: declaration 'iso_of_hom_iso_attempt_1' uses sorry

/home/runner/work/lftcm2020/lftcm2020/src/hints/category_theory/exercise2/hint1.lean:13:0: declaration 'CommRing.polynomial' uses sorry

/home/runner/work/lftcm2020/lftcm2020/src/hints/category_theory/exercise2/hint3.lean:35:0: declaration 'CommRing.polynomial' uses sorry

/home/runner/work/lftcm2020/lftcm2020/src/hints/category_theory/exercise2/hint2.lean:21:0: declaration 'CommRing.polynomial' uses sorry

/home/runner/work/lftcm2020/lftcm2020/src/exercises_sources/thursday/category_theory/exercise2.lean:15:0: declaration 'Ring.polynomial' uses sorry

/home/runner/work/lftcm2020/lftcm2020/src/hints/category_theory/exercise2/hint5.lean:12:0: declaration 'CommRing.polynomial' uses sorry

/home/runner/work/lftcm2020/lftcm2020/src/exercises_sources/thursday/category_theory/exercise2.lean:18:0: declaration 'CommRing.polynomial' uses sorry

/home/runner/work/lftcm2020/lftcm2020/src/exercises_sources/monday/metaprogramming.lean:41:0: declaration '[anonymous]' uses sorry

/home/runner/work/lftcm2020/lftcm2020/src/exercises_sources/tuesday/numbers.lean:23:0: declaration '[anonymous]' uses sorry

/home/runner/work/lftcm2020/lftcm2020/src/hints/category_theory/exercise2/hint1.lean:18:0: declaration 'commutes' uses sorry

/home/runner/work/lftcm2020/lftcm2020/src/demos/linalg.lean:23:0: @[_ext_core id.{1} name module.ext, class, ext option.none.{0} name, protect_proj list.nil.{0} name] structure module : Π (R : Type u) (M : Type v) [_inst_1 : semiring R] [_inst_2 : add_comm_monoid M], Type (max u v) fields: module.to_distrib_mul_action : Π {R : Type u} {M : Type v} [_inst_1 : semiring R] [_inst_2 : add_comm_monoid M] [self : module R M], distrib_mul_action R M module.add_smul : ∀ {R : Type u} {M : Type v} [_inst_1 : semiring R] [_inst_2 : add_comm_monoid M] [self : module R M] (r s : R) (x : M), (r + s) • x = r • x + s • x module.zero_smul : ∀ {R : Type u} {M : Type v} [_inst_1 : semiring R] [_inst_2 : add_comm_monoid M] [self : module R M] (x : M), 0 • x = 0

/home/runner/work/lftcm2020/lftcm2020/src/demos/linalg.lean:32:0: add_smul : ∀ (r s : ?M_1) (x : ?M_2), (r + s) • x = r • x + s • x

/home/runner/work/lftcm2020/lftcm2020/src/demos/linalg.lean:33:0: smul_add : ∀ (a : ?M_1) (b₁ b₂ : ?M_2), a • (b₁ + b₂) = a • b₁ + a • b₂

/home/runner/work/lftcm2020/lftcm2020/src/demos/linalg.lean:34:0: mul_smul : ∀ (x y : ?M_1) (b : ?M_2), (x * y) • b = x • y • b

/home/runner/work/lftcm2020/lftcm2020/src/demos/linalg.lean:35:0: one_smul : ∀ (M : Type u_1) {α : Type u_2} [_inst_1 : monoid M] [_inst_2 : mul_action M α] (b : α), 1 • b = b

/home/runner/work/lftcm2020/lftcm2020/src/solutions/friday/topology.lean:97:0: sets_of_superset : ∀ {α : Type u_1} (self : filter α) {x y : set α}, x ∈ self.sets → x ⊆ y → y ∈ self.sets

/home/runner/work/lftcm2020/lftcm2020/src/demos/linalg.lean:36:0: zero_smul : ∀ (R : Type u_1) {M : Type u_2} [_inst_1 : has_zero R] [_inst_2 : has_zero M] [_inst_3 : smul_with_zero R M] (m : M), 0 • m = 0

/home/runner/work/lftcm2020/lftcm2020/src/solutions/friday/topology.lean:98:0: mem_of_superset : ∀ {α : Type u_1} {f : filter α} {x y : set α}, x ∈ f → x ⊆ y → y ∈ f

/home/runner/work/lftcm2020/lftcm2020/src/solutions/thursday/category_theory/exercise4.lean:27:3: Try this: exact algebra_map ℤ ↥R