Cannot start Primzahlen 8 because of Lean error (ambiguity due to name clash)

[sozysozbot]

Accessing https://adam.math.hhu.de/#/g/hhu-adam/robo/world/Prime/level/8 results in the following message:

ambiguous, possible interpretations 
  _root_.Prime p : Prop

  Nat.Prime p : Prop

[joneugster]

Thanks! Indeed "Primzahlen" isn't really playable right now and requires a few final modifications which should be ready shortly.

Sorry for that

[sozysozbot]

For reference, here is how I solved the Primzahlen level with my very limited understanding of Lean, with Rules "none". Hope this horrible proofs serves as the data to help you make decisions on what theorems and tactics to introduce, so that the proofs do not become too painful.

Level 1 / 8 : Teilbarkeit

obtain ⟨c, hc⟩ := h
obtain ⟨d, gd⟩ := g
rw [hc, gd]
use (c+d)
ring

Level 2 / 8 : Primzahlen

rw [Nat.prime_def_lt''] at h
obtain ⟨_, h2 ⟩ := h
assumption

Level 3 / 8 : Primzahlen

symm
constructor
intro prime_element
rw [Nat.prime_def_lt'']
constructor
assumption
intro m
intro h
obtain ⟨s, hs⟩ :=  (λ a => a) h
have q := prime_element m s
rw [← hs] at q
have k: p ∣ p
use 1
ring
apply q at k
obtain k|k := k
have j := Nat.dvd_antisymm h k
right
assumption
have j : s ∣ p
use m
rw [hs]
ring
have u := Nat.dvd_antisymm k j
rw [← u] at hs
suffices h₃ : p ≠ 0
have hh : 1 * p = m * p → 1 = m := (Nat.mul_left_inj h₃).mp
rw [one_mul] at hh
apply hh at hs
left
symm
assumption
linarith
intro h a b
exact (Nat.Prime.dvd_mul h).mp

Level 4 / 8 : Existiert eindeutig

use 2
simp
have not_zero_or_one_then_ge_two : ∀(y : ℕ ), y ≠ 0 ∧ y ≠ 1 →  y ≥ 2
intro y h
induction y
contradiction
obtain ⟨l, r⟩ := h
simp at r
have neq : n ≠ 0
assumption
rw [← Nat.pos_iff_ne_zero] at neq
induction n
contradiction
linarith
constructor
rw [Nat.prime_def_lt'']
constructor
simp
intro
intro
induction m
obtain ⟨q, aq⟩ := a
simp at aq
obtain ⟨q, aq⟩ := a
revert aq
contrapose
push_neg
intro
obtain ⟨l,r⟩ := a
simp at l
simp at r
have nn : n ≠ 0 ∧ n ≠ 1
constructor
assumption
assumption
apply not_zero_or_one_then_ge_two n at nn
induction q
ring
intro
contradiction
intro
have f : ∀ (n m : ℕ), 2 ≤ n →  3 ≤  (n + 1) * (m + 1)
repeat intro
have g : 3 ≤ n_2 +1
linarith
rw [mul_add, mul_one]
have hh :=  Nat.le_add_left (n_2 + 1) ((n_2 + 1) * m)
exact le_trans g hh
simp at nn
apply f n n_1 at nn
linarith
repeat intro
rw [Nat.prime_def_lt''] at a
unfold Even at a_1
obtain ⟨r, ar⟩ := a_1
have q : r + r = 2 * r
ring
rw [q] at ar
have p : 2 ∣ y
use r
have o := a.right 2 p
symm
obtain o|o:= o
contradiction
assumption

Level 5 / 8 : Unendlich viele Primzahlen

apply minFac_prime
have k := factorial_ne_zero n
revert k
simp

Level 6 / 8 : Unendlich viele Primzahlen

have u := Nat.minFac_dvd (n ! + 1)
have k := Nat.minFac_pos (n ! + 1)
by_contra h
simp at h
apply le_of_lt at h
have j := Nat.dvd_factorial k h
have p := Nat.dvd_sub' u j
simp at p
have q := Nat.factorial_pos n
rw [Nat.pos_iff_ne_zero] at q
contradiction

Level 7 / 8 : Unendlich viele Primzahlen

use (Nat.minFac (Nat.factorial n + 1))
constructor
have u := le_minFac_factorial_succ n
assumption
have u := minFac_factorial_succ_prime n
assumption