errors_filtered.txt

1. FIXED

/mathlib/src/algebra/opposites.lean:117:4: error: invalid 'or.cases_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but term
  eq_zero_or_eq_zero_of_mul_eq_zero (op_inj H)
must not contain metavariables because it is used to compute the motive

2.

/mathlib/src/category_theory/opposites.lean:192:29: error: rewrite tactic failed, did not find instance of the pattern in the target expression
  (functor.op F).map ?m_3 ≫ α.app ?m_2
state:
C : Type u₁,
_inst_1 : category C,
D : Type u₂,
_inst_2 : category D,
F G : C ⥤ D,
α : functor.op F ⟶ functor.op G,
X Y : C,
f : X ⟶ Y
⊢ G.map f ≫ has_hom.hom.unop (α.app (opposite.op Y)) = has_hom.hom.unop (α.app (opposite.op X)) ≫ F.map f

3.

/mathlib/src/category_theory/opposites.lean:211:29: error: rewrite tactic failed, did not find instance of the pattern in the target expression
  (functor.left_op F).map ?m_3 ≫ α.app ?m_2
state:
C : Type u₁,
_inst_1 : category C,
D : Type u₂,
_inst_2 : category D,
F G : C ⥤ Dᵒᵖ,
α : functor.left_op F ⟶ functor.left_op G,
X Y : C,
f : X ⟶ Y
⊢ G.map f ≫ has_hom.hom.op (α.app (opposite.op Y)) = has_hom.hom.op (α.app (opposite.op X)) ≫ F.map f

4.

/mathlib/src/category_theory/yoneda.lean:50:6: error: rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_5.app ?m_6 (?m_3.map ?m_8 ?m_9)
state:
C : Type u₁,
_inst_1 : category C,
X Y : C,
α : yoneda.obj X ⟶ yoneda.obj Y,
Z Z' : C,
f : Z ⟶ Z',
h : Z' ⟶ X
⊢ f ≫ α.app (op Z') h = α.app (op Z) (f ≫ h)

5.

/mathlib/src/category_theory/yoneda.lean:147:6: error: rewrite tactic failed, did not find instance of the pattern in the target expression
  (yoneda.obj ?m_3).map ?m_5 (𝟙 ?m_3)
state:
C : Type u₁,
_inst_1 : category C,
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁),
f : X ⟶ Y,
x : (yoneda_pairing C).obj X
⊢ f.snd.app Y.fst (x.app Y.fst (has_hom.hom.unop f.fst)) =
    f.snd.app Y.fst (x.app Y.fst ((yoneda.obj (unop X.fst)).map f.fst (𝟙 (unop X.fst))))
/mathlib/src/data/pfun.lean:206:20: error: don't know how to synthesize placeholder
context:
α : Type u_1,
p : Prop,
f : p → roption α,
mem_assert : ∀ {a : α} (h : p), a ∈ f h → a ∈ assert p f,
_x : p,
h : (f _x).dom
⊢ p

6. FIXED

/mathlib/src/data/pfun.lean:215:30: error: don't know how to synthesize placeholder
context:
α : Type u_1,
β : Type u_2,
f : roption α,
g : α → roption β,
mem_bind : ∀ {a : α} {b : β}, a ∈ f → b ∈ g a → b ∈ roption.bind f g,
h : f.dom,
h₂ : (g (f.get h)).dom
⊢ f.dom

7. FIXED

/mathlib/src/data/array/lemmas.lean:194:61: error: don't know how to synthesize placeholder
context:
α : Type u,
l : list α,
n : ℕ,
h1 : n < list.length (to_list (list.to_array l)),
h2 : n < list.length l
⊢ n < list.length l

8. FIXED

/mathlib/src/data/padics/padic_norm.lean:279:22: error: tactic failed, there are unsolved goals
state:
p : ℕ,
q : ℚ,
hq : q = 0
⊢ 0 ≤ padic_norm p 0

9. FIXED

/mathlib/src/data/padics/padic_norm.lean:359:22: error: tactic failed, there are unsolved goals
state:
p : ℕ,
hp : fact (prime p),
z : ℤ,
hz : z = 0
⊢ 0 ≤ 1

10.

/mathlib/src/category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean:81:26: error: invalid type ascription, term has type
  (functor.const limits.walking_parallel_pair).obj (limits.fork.of_ι ?m_8 ?m_9).X ⟶
    limits.parallel_pair ?m_5 ?m_6 : Type ?
but is expected to have type
  (functor.cones (diagram F)).obj X : Type v
state:
C : Type u,
_inst_1 : category C,
J : Type v,
_inst_2 : small_category J,
F : J ⥤ C,
H₁ : limits.has_limit (functor.of_function F.obj),
H₂ : limits.has_limit (functor.of_function (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd)),
X : Cᵒᵖ,
c : (functor.cones F).obj X
⊢ (functor.cones (diagram F)).obj X

11.

/mathlib/src/category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean:102:16: error: solve1 tactic failed, focused goal has not been solved
state:
C : Type u,
_inst_1 : category C,
J : Type v,
_inst_2 : small_category J,
F : J ⥤ C,
H₁ : limits.has_limit (functor.of_function F.obj),
H₂ : limits.has_limit (functor.of_function (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd)),
X : Cᵒᵖ,
c : (functor.cones (diagram F)).obj X,
j : discrete J
⊢ ⁇.app limits.walking_parallel_pair.zero ≫ limits.limit.π (functor.of_function F.obj) j =
    c.app limits.walking_parallel_pair.zero ≫ limits.limit.π (functor.of_function F.obj) j

12. FIXED    

/mathlib/src/data/complex/basic.lean:136:18: error: "eliminator" elaborator type mismatch, term
  rfl
has type
  ?m_2 = ?m_2
but is expected to have type
  conj ↑h = ↑h
Additional information:
/mathlib/src/data/complex/basic.lean:136:18: context: the inferred motive for the eliminator-like application is
  λ (_x : ℂ), conj _x = _x

13. FIXED

/mathlib/src/topology/metric_space/emetric_space.lean:79:66: error: "eliminator" elaborator type mismatch, term
  ennreal.nat_ne_top 2
has type
  ↑2 ≠ ⊤
but is expected to have type
  2 ≠ ⊤
Additional information:
/mathlib/src/topology/metric_space/emetric_space.lean:79:66: context: the inferred motive for the eliminator-like application is
  λ (_x : ennreal), 2 ≠ ⊤

14.

/mathlib/src/set_theory/cofinality.lean:72:8: error: invalid constructor ⟨...⟩, expected type is not an inductive type
  ∀ (a : α), ¬r a a
state:
3 goals
o : ordinal,
_x : Well_order,
_fun_match :
  ∀ (_a b : Well_order),
    setoid.r _a b → (λ (_x : Well_order), cof._match_1 _x) _a = (λ (_x : Well_order), cof._match_1 _x) b,
α : Type u,
r : α → α → Prop,
_x : is_well_order α r,
_x : Well_order,
_fun_match :
  ∀ (_a : Well_order),
    setoid.r {α := α, r := r, wo := _x} _a →
    (λ (_x : Well_order), cof._match_1 _x) {α := α, r := r, wo := _x} = (λ (_x : Well_order), cof._match_1 _x) _a,
β : Type u,
s : β → β → Prop,
_x : is_well_order β s,
_x : setoid.r {α := α, r := r, wo := _x} {α := β, r := s, wo := _x},
_fun_match :
  setoid.r {α := α, r := r, wo := _x} {α := β, r := s, wo := _x} →
  (λ (_x : Well_order), cof._match_1 _x) {α := α, r := r, wo := _x} =
    (λ (_x : Well_order), cof._match_1 _x) {α := β, r := s, wo := _x},
f : α ≃ β,
hf : ∀ {a b : α}, r a b ↔ s (⇑f a) (⇑f b)
⊢ ∀ (a : α), ¬r a a

o : ordinal,
_x : Well_order,
_fun_match :
  ∀ (_a b : Well_order),
    setoid.r _a b → (λ (_x : Well_order), cof._match_1 _x) _a = (λ (_x : Well_order), cof._match_1 _x) b,
α : Type u,
r : α → α → Prop,
_x : is_well_order α r,
_x : Well_order,
_fun_match :
  ∀ (_a : Well_order),
    setoid.r {α := α, r := r, wo := _x} _a →
    (λ (_x : Well_order), cof._match_1 _x) {α := α, r := r, wo := _x} = (λ (_x : Well_order), cof._match_1 _x) _a,
β : Type u,
s : β → β → Prop,
_x : is_well_order β s,
_x : setoid.r {α := α, r := r, wo := _x} {α := β, r := s, wo := _x},
_fun_match :
  setoid.r {α := α, r := r, wo := _x} {α := β, r := s, wo := _x} →
  (λ (_x : Well_order), cof._match_1 _x) {α := α, r := r, wo := _x} =
    (λ (_x : Well_order), cof._match_1 _x) {α := β, r := s, wo := _x},
f : α ≃ β,
hf : ∀ {a b : α}, r a b ↔ s (⇑f a) (⇑f b)
⊢ ∀ (a : β), ¬s a a

o : ordinal,
_x : Well_order,
_fun_match :
  ∀ (_a b : Well_order),
    setoid.r _a b → (λ (_x : Well_order), cof._match_1 _x) _a = (λ (_x : Well_order), cof._match_1 _x) b,
α : Type u,
r : α → α → Prop,
_x : is_well_order α r,
_x : Well_order,
_fun_match :
  ∀ (_a : Well_order),
    setoid.r {α := α, r := r, wo := _x} _a →
    (λ (_x : Well_order), cof._match_1 _x) {α := α, r := r, wo := _x} = (λ (_x : Well_order), cof._match_1 _x) _a,
β : Type u,
s : β → β → Prop,
_x : is_well_order β s,
_x : setoid.r {α := α, r := r, wo := _x} {α := β, r := s, wo := _x},
_fun_match :
  setoid.r {α := α, r := r, wo := _x} {α := β, r := s, wo := _x} →
  (λ (_x : Well_order), cof._match_1 _x) {α := α, r := r, wo := _x} =
    (λ (_x : Well_order), cof._match_1 _x) {α := β, r := s, wo := _x},
f : α ≃ β,
hf : ∀ {a b : α}, r a b ↔ s (⇑f a) (⇑f b)
⊢ (λ (x y : α), ¬r y x) ≃o λ (x y : β), ¬s y x

15.

/mathlib/src/data/polynomial.lean:1838:47: error: don't know how to synthesize placeholder
context:
R : Type u,
_inst_1 : comm_ring R,
p : polynomial R,
a : R,
hp : p ≠ 0,
_inst : nonzero_comm_ring R := nonzero_comm_ring.of_polynomial_ne hp,
q : polynomial R,
hq : p /ₘ (X - C a) ^ root_multiplicity a p = (X - C a) * q,
this : (X - C a) ^ ((multiplicity (X - C a) p).get _ + 1) * q = p
⊢ monic (X - C a)
state:
R : Type u,
_inst_1 : comm_ring R,
p : polynomial R,
a : R,
hp : p ≠ 0,
_inst : nonzero_comm_ring R := nonzero_comm_ring.of_polynomial_ne hp,
q : polynomial R,
hq : p /ₘ (X - C a) ^ root_multiplicity a p = (X - C a) * q,
this : (X - C a) ^ ((multiplicity (X - C a) p).get _ + 1) * q = p
⊢ false

16.

/mathlib/src/data/real/hyperreal.lean:591:11: error: "eliminator" elaborator type mismatch, term
  is_st_add
has type
  is_st ?m_1 ?m_2 → is_st ?m_3 ?m_4 → is_st (?m_1 + ?m_3) (?m_2 + ?m_4)
but is expected to have type
  infinitesimal x → infinitesimal y → infinitesimal (x + y)
Additional information:
/mathlib/src/data/real/hyperreal.lean:591:11: context: the inferred motive for the eliminator-like application is
  λ (_x : ℕ), infinitesimal x → infinitesimal y → infinitesimal (x + y)

17.

/mathlib/src/data/real/hyperreal.lean:594:26: error: "eliminator" elaborator type mismatch, term
  is_st_neg
has type
  is_st ?m_1 ?m_2 → is_st (-?m_1) (-?m_2)
but is expected to have type
  infinitesimal x → infinitesimal (-x)
Additional information:
/mathlib/src/data/real/hyperreal.lean:594:26: context: the inferred motive for the eliminator-like application is
  λ (_x : ℝ), infinitesimal x → infinitesimal (-x)

18.

/mathlib/src/data/real/hyperreal.lean:601:11: error: "eliminator" elaborator type mismatch, term
  is_st_mul
has type
  is_st ?m_1 ?m_2 → is_st ?m_3 ?m_4 → is_st (?m_1 * ?m_3) (?m_2 * ?m_4)
but is expected to have type
  infinitesimal x → infinitesimal y → infinitesimal (x * y)
Additional information:
/mathlib/src/data/real/hyperreal.lean:601:11: context: the inferred motive for the eliminator-like application is
  λ (_x : ℕ), infinitesimal x → infinitesimal y → infinitesimal (x * y)

19.

/mathlib/src/measure_theory/bochner_integration.lean:967:51: error: invalid type ascription, term has type
  uniform_continuous ⇑simple_func.integral_clm
but is expected to have type
  uniform_inducing ⇑(coe_to_l1 α β ℝ)
state:
3 goals
α : Type u,
_inst_1 : measure_space α,
β : Type v,
_inst_2 : normed_group β,
_inst_3 : second_countable_topology β,
_inst_4 : measurable_space β,
_inst_5 : borel_space β,
_inst_10 : normed_space ℝ β,
_inst_12 : complete_space β,
f : α →₁ₛ β
⊢ uniform_inducing ⇑(coe_to_l1 α β ℝ)

α : Type u,
_inst_1 : measure_space α,
β : Type v,
_inst_2 : normed_group β,
_inst_3 : second_countable_topology β,
_inst_4 : measurable_space β,
_inst_5 : borel_space β,
_inst_10 : normed_space ℝ β,
_inst_12 : complete_space β,
f : α →₁ₛ β
⊢ dense_range ⇑(coe_to_l1 α β ℝ)

α : Type u,
_inst_1 : measure_space α,
β : Type v,
_inst_2 : normed_group β,
_inst_3 : second_countable_topology β,
_inst_4 : measurable_space β,
_inst_5 : borel_space β,
_inst_10 : normed_space ℝ β,
_inst_12 : complete_space β,
f : α →₁ₛ β
⊢ uniform_continuous ⇑simple_func.integral_clm

20.

/mathlib/src/geometry/manifold/real_instances.lean:217:7: error: type mismatch at application
  continuous_apply 0 ?m_5 this
term
  this
has type
  is_open {z : ℝ | z < y - x}
but is expected to have type
  is_open ?m_5
Additional information:
/mathlib/src/geometry/manifold/real_instances.lean:217:7: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch, term
    continuous_apply ?m_4 ?m_5 ?m_6
  has type
    is_open ((λ (p : Π (i : ?m_1), ?m_2 i), p ?m_4) ⁻¹' ?m_5)
  but is expected to have type
    is_open {z : fin 1 → ℝ | z 0 < y - x}
state:
x y : ℝ,
_inst_1 : fact (x < y),
this : is_open {z : ℝ | z < y - x}
⊢ is_open
    {to_fun := λ (z : ↥(Icc x y)), ⟨λ (i : fin 1), z.val - x, _⟩,
     inv_fun := λ (z : euclidean_half_space 1), ⟨min (z.val 0 + x) y, _⟩,
     source := {z : ↥(Icc x y) | z.val < y},
     target := {z : euclidean_half_space 1 | z.val 0 < y - x},
     map_source := _,
     map_target := _,
     left_inv := _,
     right_inv := _}.target

21.

/mathlib/src/geometry/manifold/real_instances.lean:266:7: error: type mismatch at application
  continuous_apply 0 ?m_5 this
term
  this
has type
  is_open {z : ℝ | z < y - x}
but is expected to have type
  is_open ?m_5
Additional information:
/mathlib/src/geometry/manifold/real_instances.lean:266:7: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch, term
    continuous_apply ?m_4 ?m_5 ?m_6
  has type
    is_open ((λ (p : Π (i : ?m_1), ?m_2 i), p ?m_4) ⁻¹' ?m_5)
  but is expected to have type
    is_open {z : fin 1 → ℝ | z 0 < y - x}
state:
x y : ℝ,
_inst_1 : fact (x < y),
this : is_open {z : ℝ | z < y - x}
⊢ is_open
    {to_fun := λ (z : ↥(Icc x y)), ⟨λ (i : fin 1), y - z.val, _⟩,
     inv_fun := λ (z : euclidean_half_space 1), ⟨max (y - z.val 0) x, _⟩,
     source := {z : ↥(Icc x y) | x < z.val},
     target := {z : euclidean_half_space 1 | z.val 0 < y - x},
     map_source := _,
     map_target := _,
     left_inv := _,
     right_inv := _}.target