5. Projects🔗

Summary: In the second phase of this course, students can assign themselves projects. For this, they were asked to look for simple exercises, e.g. from their first year courses. Here comes a list of exercises they used.

5.1. Induction (Luis Jaschke und Felicitas Kissel)

Compute the following sums and products, and show your result by induction.

open Finset example (n : ) : k range (n + 1), (k:) ^ 2 = n * (n + 1) * (2*n + 1) / 6 := n:krange (n + 1), ↑k ^ 2 = n * (n + 1) * (2 * n + 1) / 6 induction n with | zero => All goals completed! 🐙 | succ n ih => n:ih:krange (n + 1), ↑k ^ 2 = n * (n + 1) * (2 * n + 1) / 6xrange (n + 1), ↑x ^ 2 + (n + 1) ^ 2 = (n + 1) * ((n + 1) + 1) * (2 * (n + 1) + 1) / 6 n:ih:krange (n + 1), ↑k ^ 2 = n * (n + 1) * (2 * n + 1) / 6n * (n + 1) * (2 * n + 1) / 6 + (n + 1) ^ 2 = (n + 1) * ((n + 1) + 1) * (2 * (n + 1) + 1) / 6 n:ih:krange (n + 1), ↑k ^ 2 = n * (n + 1) * (2 * n + 1) / 6n * (1 / 6) + n ^ 2 * (1 / 2) + n ^ 3 * (1 / 3) + (1 + n) ^ 2 = (1 + n) * (1 / 6) + (1 + n) ^ 2 * (1 / 2) + (1 + n) ^ 3 * (1 / 3) n:ih:krange (n + 1), ↑k ^ 2 = n * (n + 1) * (2 * n + 1) / 6(n * 2 + n ^ 2 * 6) * 3 + n ^ 3 * (6 * 2) + (1 + n) ^ 2 * (6 * 2 * 3) = ((1 + n) * 2 + (1 + n) ^ 2 * 6) * 3 + (1 + n) ^ 3 * (6 * 2) All goals completed! 🐙 example (n : ) : k Finset.range (n + 1), (k : ) ^ 3 = n * n * (n + 1) * (n + 1) / 4 := n:krange (n + 1), ↑k ^ 3 = n * n * (n + 1) * (n + 1) / 4 induction n with | zero => All goals completed! 🐙 | succ n ih => n:ih:krange (n + 1), ↑k ^ 3 = n * n * (n + 1) * (n + 1) / 4n * n * (n + 1) * (n + 1) / 4 + (n + 1) ^ 3 = (n + 1) * (n + 1) * ((n + 1) + 1) * ((n + 1) + 1) / 4 n:ih:krange (n + 1), ↑k ^ 3 = n * n * (n + 1) * (n + 1) / 4n ^ 2 * (1 / 4) + n ^ 3 * (1 / 2) + n ^ 4 * (1 / 4) + (1 + n) ^ 3 = (1 + n) ^ 2 * (1 / 4) + (1 + n) ^ 3 * (1 / 2) + (1 + n) ^ 4 * (1 / 4) n:ih:krange (n + 1), ↑k ^ 3 = n * n * (n + 1) * (n + 1) / 4(n ^ 2 * 2 + n ^ 3 * 4) * 4 + n ^ 4 * (4 * 2) + (1 + n) ^ 3 * (4 * 2 * 4) = ((1 + n) ^ 2 * 2 + (1 + n) ^ 3 * 4) * 4 + (1 + n) ^ 4 * (4 * 2) All goals completed! 🐙 example (n : ) : k Finset.range n, (2 * (k : ) + 1) = (n : )^2 := n:krange n, (2 * k + 1) = n ^ 2 induction n with | zero => All goals completed! 🐙 | succ n ih => n:ih:krange n, (2 * k + 1) = n ^ 2n ^ 2 + (2 * n + 1) = (n + 1) ^ 2 n:ih:krange n, (2 * k + 1) = n ^ 2n ^ 2 + (2 * n + 1) = (n + 1) ^ 2 All goals completed! 🐙 open Finset example (n : ) : k Finset.range n, (1 + 1 / (k + 1 : )) = n + 1 := n:krange n, (1 + 1 / (k + 1)) = n + 1 -- gleicher Nenner: 1 + (1/(k+1)) = (1+2)/(k+1) have h_gleicher_Nenner : k Finset.range n, (1 + 1 / (k + 1 : )) = k Finset.range n, ((k + 2) : ) / (k + 1) := n:krange n, (1 + 1 / (k + 1)) = n + 1 n:xrange n, 1 + 1 / (x + 1) = (x + 2) / (x + 1) n:k:hk:krange n1 + 1 / (k + 1) = (k + 2) / (k + 1) n:k:hk:krange nk + 1 + 1 = k + 2 All goals completed! 🐙 n:h_gleicher_Nenner:krange n, (1 + 1 / (k + 1)) = krange n, (k + 2) / (k + 1)krange n, (k + 2) / (k + 1) = n + 1 -- Nun zur Induktion induction n with | zero => All goals completed! 🐙 | succ n kh => n:kh:krange n, (1 + 1 / (k + 1)) = krange n, (k + 2) / (k + 1) → ∏ krange n, (k + 2) / (k + 1) = n + 1h_gleicher_Nenner:krange (n + 1), (1 + 1 / (k + 1)) = krange (n + 1), (k + 2) / (k + 1)(n + 2) / (n + 1) * xrange n, (x + 2) / (x + 1) = (n + 1) + 1 have h' := kh (n:kh:krange n, (1 + 1 / (k + 1)) = krange n, (k + 2) / (k + 1) → ∏ krange n, (k + 2) / (k + 1) = n + 1h_gleicher_Nenner:krange (n + 1), (1 + 1 / (k + 1)) = krange (n + 1), (k + 2) / (k + 1)krange n, (1 + 1 / (k + 1)) = krange n, (k + 2) / (k + 1) n:kh:krange n, (1 + 1 / (k + 1)) = krange n, (k + 2) / (k + 1) → ∏ krange n, (k + 2) / (k + 1) = n + 1h_gleicher_Nenner:krange (n + 1), (1 + 1 / (k + 1)) = krange (n + 1), (k + 2) / (k + 1)xrange n, 1 + 1 / (x + 1) = (x + 2) / (x + 1) n:kh:krange n, (1 + 1 / (k + 1)) = krange n, (k + 2) / (k + 1) → ∏ krange n, (k + 2) / (k + 1) = n + 1h_gleicher_Nenner:krange (n + 1), (1 + 1 / (k + 1)) = krange (n + 1), (k + 2) / (k + 1)k:hk:krange n1 + 1 / (k + 1) = (k + 2) / (k + 1) n:kh:krange n, (1 + 1 / (k + 1)) = krange n, (k + 2) / (k + 1) → ∏ krange n, (k + 2) / (k + 1) = n + 1h_gleicher_Nenner:krange (n + 1), (1 + 1 / (k + 1)) = krange (n + 1), (k + 2) / (k + 1)k:hk:krange nk + 1 + 1 = k + 2 All goals completed! 🐙) n:kh:krange n, (1 + 1 / (k + 1)) = krange n, (k + 2) / (k + 1) → ∏ krange n, (k + 2) / (k + 1) = n + 1h_gleicher_Nenner:krange (n + 1), (1 + 1 / (k + 1)) = krange (n + 1), (k + 2) / (k + 1)h':krange n, (k + 2) / (k + 1) = n + 1(n + 2) / (n + 1) * (n + 1) = (n + 1) + 1 n:kh:krange n, (1 + 1 / (k + 1)) = krange n, (k + 2) / (k + 1) → ∏ krange n, (k + 2) / (k + 1) = n + 1h_gleicher_Nenner:krange (n + 1), (1 + 1 / (k + 1)) = krange (n + 1), (k + 2) / (k + 1)h':krange n, (k + 2) / (k + 1) = n + 1n + 2 = n + 1 + 1 All goals completed! 🐙 declaration uses 'sorry'example (q : ) (hq : abs q < 1) : Filter.Tendsto (fun n q^n) atTop (nhds 0) := atTop:Filter q:hq:|q| < 1Filter.Tendsto (fun n => q ^ n) atTop (nhds 0) All goals completed! 🐙

5.2. Own addition on ℚ (Adrian Eckstein und Debora Ortlieb)

open Rat open BigOperators -- Zu bearbeiten war das `Blatt 1` der Vorlesung `Lineare Algebra I` im _WiSe 2021/22_ -- an der _Universität Freiburg_ bei _Prof. Dr. Heike Mildenberger_. -- `Aufgabe 1`: Betrachten Sie auf der Menge der rationalen Zahlen ℚ die folgende Verknüpfung. -- Definiere die Operation _star_: a ∗ b := ab + 2a + 2b + 2 def star (a b : ) : := a * b + 2 * a + 2 * b + 2 theorem LA1_Sheet1_Task1a (a b : ) : star a b = star b a := a:b:_root_.star a b = _root_.star b a a:b:a * b + 2 * a + 2 * b + 2 = b * a + 2 * b + 2 * a + 2 All goals completed! 🐙 -- `Aufgabe 1b`: Ist _(ℚ, star)_ assoziativ? -- Beweis der Assoziativität: (a ∗ b) ∗ c = a ∗ (b ∗ c) theorem LA1_Sheet1_Task1b (a b c : ) : star (star a b) c = star a (star b c) := a:b:c:_root_.star (_root_.star a b) c = _root_.star a (_root_.star b c) a:b:c:(a * b + 2 * a + 2 * b + 2) * c + 2 * (a * b + 2 * a + 2 * b + 2) + 2 * c + 2 = a * (b * c + 2 * b + 2 * c + 2) + 2 * a + 2 * (b * c + 2 * b + 2 * c + 2) + 2 All goals completed! 🐙 -- `Aufgabe 1c`: Besitzt _(ℚ, star)_ ein neutrales Element? -- Beweis: -1 ist das neutrale Element, d.h. -1 ∗ a = a und a ∗ (-1) = a theorem LA1_Sheet1_Task1c (a : ) : star (-1) a = a star a (-1) = a := a:_root_.star (-1) a = a_root_.star a (-1) = a a:-1 * a + 2 * -1 + 2 * a + 2 = aa * -1 + 2 * a + 2 * -1 + 2 = a a:-1 * a + 2 * -1 + 2 * a + 2 = aa:a * -1 + 2 * a + 2 * -1 + 2 = a a:-1 * a + 2 * -1 + 2 * a + 2 = a All goals completed! 🐙 a:a * -1 + 2 * a + 2 * -1 + 2 = a All goals completed! 🐙 -- `Aufgabe 1d`: Ist _(ℚ, star)_ eine Gruppe? -- Zeige: Nein, da -2 kein Inverses bezüglich _star_ hat. theorem LA1_Sheet1_Task1d : ¬ b : , star (-2) b = -1 := ¬b, _root_.star (-2) b = -1 h:b, _root_.star (-2) b = -1False b:hb:_root_.star (-2) b = -1False b:hb:-2 * b + 2 * -2 + 2 * b + 2 = -1False b:hb:-2 = -1False All goals completed! 🐙 theorem Ana1_Sheet1_Task3d (n : ) (hn : 1 < n) : i Finset.range n, (1 - 1 / (i + 1 : )) = 0 := n:hn:1 < nirange n, (1 - 1 / (i + 1)) = 0 have h_mem : 0 Finset.range n := n:hn:1 < nirange n, (1 - 1 / (i + 1)) = 0 n:hn:1 < nh_pos:0 < n0range n All goals completed! 🐙 n:hn:1 < nh_mem:0range n1 - 1 / (↑0 + 1) = 0 All goals completed! 🐙

5.3. Path-connected spaces (Jasper Ganten)

open Set section PathConnected variable {X : Type*} [TopologicalSpace X] /-- An intuitive definition of path connectedness: A set `S` is path connected if it is nonempty and any two points in `S` can be joined by a continuous path in `S`. -/ def IsPathConnected' (S : Set X) : Prop := S.Nonempty x y : X, x S y S γ : Set.Icc (0 : ) 1 X, Continuous γ γ 0 = x γ 1 = y t, γ t S /-- `IsPathConnected'` is equivalent to Mathlib's `IsPathConnected`. -/ theorem pathConnected_iff (A : Set X) : IsPathConnected A IsPathConnected' A := X:Type u_1inst✝:TopologicalSpace XA:Set XIsPathConnected AIsPathConnected' A X:Type u_1inst✝:TopologicalSpace XA:Set XIsPathConnected AIsPathConnected' AX:Type u_1inst✝:TopologicalSpace XA:Set XIsPathConnected' AIsPathConnected A X:Type u_1inst✝:TopologicalSpace XA:Set XIsPathConnected AIsPathConnected' A -- Mathlib ⇒ Intuitive X:Type u_1inst✝:TopologicalSpace XA:Set Xp1:Xhp1:p1Ah1:∀ {y : X}, yAJoinedIn A p1 yIsPathConnected' A -- show that the set is nonempty X:Type u_1inst✝:TopologicalSpace XA:Set Xp1:Xhp1:p1Ah1:∀ {y : X}, yAJoinedIn A p1 y∀ (x y : X), xAyA → ∃ γ, Continuous γγ 0 = xγ 1 = y∀ (t : ↑(Set.Icc 0 1)), γ tA X:Type u_1inst✝:TopologicalSpace XA:Set Xp1:Xhp1:p1Ah1:∀ {y : X}, yAJoinedIn A p1 yp2:Xp3:Xhp2:p2Ahp3:p3Aγ, Continuous γγ 0 = p2γ 1 = p3∀ (t : ↑(Set.Icc 0 1)), γ tA -- construct a path from p2 to p3 by using the -- transitivity of the JoinedIn relation X:Type u_1inst✝:TopologicalSpace XA:Set Xp1:Xhp1:p1Ah1:∀ {y : X}, yAJoinedIn A p1 yp2:Xp3:Xhp2:p2Ahp3:p3Aγ:_root_.Path p2 p3:∀ (t : ↑unitInterval), γ tAγ, Continuous γγ 0 = p2γ 1 = p3∀ (t : ↑(Set.Icc 0 1)), γ tA All goals completed! 🐙 X:Type u_1inst✝:TopologicalSpace XA:Set XIsPathConnected' AIsPathConnected A -- Intuitive ⇒ Mathlib X:Type u_1inst✝:TopologicalSpace XA:Set Xhne:A.NonemptyhC:∀ (x y : X), xAyA → ∃ γ, Continuous γγ 0 = xγ 1 = y∀ (t : ↑(Set.Icc 0 1)), γ tAIsPathConnected A X:Type u_1inst✝:TopologicalSpace XA:Set XhC:∀ (x y : X), xAyA → ∃ γ, Continuous γγ 0 = xγ 1 = y∀ (t : ↑(Set.Icc 0 1)), γ tAx:Xhx:xAIsPathConnected A X:Type u_1inst✝:TopologicalSpace XA:Set XhC:∀ (x y : X), xAyA → ∃ γ, Continuous γγ 0 = xγ 1 = y∀ (t : ↑(Set.Icc 0 1)), γ tAx:Xhx:xAy:Xhy:yAJoinedIn A x y X:Type u_1inst✝:TopologicalSpace XA:Set XhC:∀ (x y : X), xAyA → ∃ γ, Continuous γγ 0 = xγ 1 = y∀ (t : ↑(Set.Icc 0 1)), γ tAx:Xhx:xAy:Xhy:yAγ:↑(Set.Icc 0 1) → Xγ_cont:Continuous γγ0:γ 0 = xγ1:γ 1 = y:∀ (t : ↑(Set.Icc 0 1)), γ tAJoinedIn A x y -- construct a Path type from my intuitive definition X:Type u_1inst✝:TopologicalSpace XA:Set XhC:∀ (x y : X), xAyA → ∃ γ, Continuous γγ 0 = xγ 1 = y∀ (t : ↑(Set.Icc 0 1)), γ tAx:Xhx:xAy:Xhy:yAγ:↑(Set.Icc 0 1) → Xγ_cont:Continuous γγ0:γ 0 = xγ1:γ 1 = y:∀ (t : ↑(Set.Icc 0 1)), γ tAp:_root_.Path x y := { toFun := γ, continuous_toFun := γ_cont, source' := γ0, target' := γ1 }JoinedIn A x y All goals completed! 🐙 /-- If `A` and `B` are path connected, and their intersetion is nonempty, `A ∪ B` is pathconnected. -/ theorem my_task {A B : Set X} (hA : IsPathConnected A) (hB : IsPathConnected B) (hAB : (A B).Nonempty) : IsPathConnected (A B) := X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected BhAB:(AB).NonemptyIsPathConnected (AB) -- select a point z in the intersection X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:xAhxB:xBIsPathConnected (AB) X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:xAhxB:xBxAB∀ {y : X}, yABJoinedIn (AB) x y X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:xAhxB:xBy:Xhy:yABJoinedIn (AB) x y -- split in cases depending on where y is X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:xAhxB:xBy:XhyA:yAJoinedIn (AB) x yX:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:xAhxB:xBy:XhyB:yBJoinedIn (AB) x y X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:xAhxB:xBy:XhyA:yAJoinedIn (AB) x y -- y ∈ A then x and y are joined in A X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:xAhxB:xBy:XhyA:yAjoinedInA:JoinedIn A x yJoinedIn (AB) x y -- but then also in the superset A ∪ B All goals completed! 🐙 X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:xAhxB:xBy:XhyB:yBJoinedIn (AB) x y -- y ∈ A then x and y are joined in B X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:xAhxB:xBy:XhyB:yBjoinedInB:JoinedIn B x yJoinedIn (AB) x y -- but then also in the superset A ∪ B All goals completed! 🐙 end PathConnected

5.4. A homomorphism is injective iff its kernel is trivial (Moritz Graßnitzer, Natalie Jahnes)

structure our_Group where uni : Type mul : uni uni uni one : uni inv : uni uni mul_assoc : a b c : uni, mul (mul a b) c = mul a (mul b c) one_mul : a : uni, mul one a = a mul_one : a : uni, mul a one = a mul_inv : a : uni, mul a (inv a) = one inv_mul : a : uni, mul (inv a) a = one lemma our_unique_inv {G : our_Group} (a b : G.uni) : G.mul a b = G.one b = G.inv a := G:our_Groupa:G.unib:G.uniG.mul a b = G.oneb = G.inv a G:our_Groupa:G.unib:G.unih:G.mul a b = G.oneb = G.inv a G:our_Groupa:G.unib:G.unih:G.mul a b = G.oneh1:G.mul a (G.inv a) = G.oneb = G.inv a G:our_Groupa:G.unib:G.unih:G.mul a b = G.oneh1:G.mul a (G.inv a) = G.mul a bb = G.inv a have h2 : G.mul (G.inv a) (G.mul a b) = G.mul (G.inv a) G.one := G:our_Groupa:G.unib:G.uniG.mul a b = G.oneb = G.inv a All goals completed! 🐙 have h3 : G.mul (G.mul (G.inv a) a) b = G.mul (G.inv a) G.one := G:our_Groupa:G.unib:G.uniG.mul a b = G.oneb = G.inv a All goals completed! 🐙 have h4 : G.mul (G.one) b = G.mul (G.inv a) G.one := G:our_Groupa:G.unib:G.uniG.mul a b = G.oneb = G.inv a G:our_Groupa:G.unib:G.unih:G.mul a b = G.oneh1:G.mul a (G.inv a) = G.mul a bh2:G.mul (G.inv a) (G.mul a b) = G.mul (G.inv a) G.oneh3:G.mul G.one b = G.mul (G.inv a) G.oneG.mul G.one b = G.mul (G.inv a) G.one All goals completed! 🐙 have h5 : b = G.mul (G.inv a) G.one := G:our_Groupa:G.unib:G.uniG.mul a b = G.oneb = G.inv a G:our_Groupa:G.unib:G.unih:G.mul a b = G.oneh1:G.mul a (G.inv a) = G.mul a bh2:G.mul (G.inv a) (G.mul a b) = G.mul (G.inv a) G.oneh3:G.mul (G.mul (G.inv a) a) b = G.mul (G.inv a) G.oneh4:b = G.mul (G.inv a) G.oneb = G.mul (G.inv a) G.one All goals completed! 🐙 have h6 : b = G.inv a := G:our_Groupa:G.unib:G.uniG.mul a b = G.oneb = G.inv a G:our_Groupa:G.unib:G.unih:G.mul a b = G.oneh1:G.mul a (G.inv a) = G.mul a bh2:G.mul (G.inv a) (G.mul a b) = G.mul (G.inv a) G.oneh3:G.mul (G.mul (G.inv a) a) b = G.mul (G.inv a) G.oneh4:G.mul G.one b = G.mul (G.inv a) G.oneh5:b = G.inv ab = G.inv a All goals completed! 🐙 All goals completed! 🐙 lemma our_unique_inv_inv {G : our_Group} (a : G.uni) : a = G.inv (G.inv a) := G:our_Groupa:G.unia = G.inv (G.inv a) G:our_Groupa:G.unih1:G.mul (G.inv a) a = G.onea = G.inv (G.inv a) G:our_Groupa:G.unih1:a = G.inv (G.inv a)a = G.inv (G.inv a) All goals completed! 🐙

5.5. There is only one prime triplet (Patrick Nasdala, Max Lehr)

There is only one prime triplet, i.e. only one n : ℕ prime, such that n + 2 and n + 4 are prime as well.

lemma div3 (n : ) : (3 n) (3 (n+1)) (3 (n+2)) := n:3n3n + 13n + 2 induction n with | zero => 30 All goals completed! 🐙 | succ n hn => n:hn:3n3n + 13n + 231 + n32 + n33 + n n:hn:3n3n + 13n + 2h0:3n31 + n32 + n33 + nn:hn:3n3n + 13n + 2h0:¬3n31 + n32 + n33 + n n:hn:3n3n + 13n + 2h0:3n31 + n32 + n33 + n n:hn:3n3n + 13n + 2h0:3n32 + n33 + n n:hn:3n3n + 13n + 2h0:3n33 + n All goals completed! 🐙 n:hn:3n3n + 13n + 2h0:¬3n31 + n32 + n33 + n n:hn:3n3n + 13n + 2h0:¬3nh1:3n + 131 + n32 + n33 + nn:hn:3n3n + 13n + 2h0:¬3nh1:¬3n + 131 + n32 + n33 + n n:hn:3n3n + 13n + 2h0:¬3nh1:3n + 131 + n32 + n33 + n n:hn:3n3n + 13n + 2h0:¬3nh1:3n + 131 + n n:hn:3n3n + 13n + 2h0:¬3nh1:31 + n31 + n All goals completed! 🐙 n:hn:3n3n + 13n + 2h0:¬3nh1:¬3n + 131 + n32 + n33 + n n:hn:3n3n + 13n + 2h0:¬3nh1:¬3n + 1h2:3n + 231 + n32 + n33 + nn:hn:3n3n + 13n + 2h0:¬3nh1:¬3n + 1h2:¬3n + 231 + n32 + n33 + n n:hn:3n3n + 13n + 2h0:¬3nh1:¬3n + 1h2:3n + 231 + n32 + n33 + n n:hn:3n3n + 13n + 2h0:¬3nh1:¬3n + 1h2:3n + 232 + n33 + n n:hn:3n3n + 13n + 2h0:¬3nh1:¬3n + 1h2:3n + 232 + n n:hn:3n3n + 13n + 2h0:¬3nh1:¬3n + 1h2:32 + n32 + n All goals completed! 🐙 n:hn:3n3n + 13n + 2h0:¬3nh1:¬3n + 1h2:¬3n + 231 + n32 + n33 + n n:hn:3n3n + 13n + 2h0:¬3nh1:¬3n + 1h2:¬3n + 2False n:h0:¬3nh1:¬3n + 1h2:¬3n + 2l0:3nFalsen:h0:¬3nh1:¬3n + 1h2:¬3n + 2lr:3n + 13n + 2False n:h0:¬3nh1:¬3n + 1h2:¬3n + 2l0:3nFalse All goals completed! 🐙 n:h0:¬3nh1:¬3n + 1h2:¬3n + 2lr:3n + 13n + 2False n:h0:¬3nh1:¬3n + 1h2:¬3n + 2l1:3n + 1Falsen:h0:¬3nh1:¬3n + 1h2:¬3n + 2l2:3n + 2False n:h0:¬3nh1:¬3n + 1h2:¬3n + 2l1:3n + 1False All goals completed! 🐙 n:h0:¬3nh1:¬3n + 1h2:¬3n + 2l2:3n + 2False All goals completed! 🐙 lemma lem1 (n : ) : (n < 3) ¬ (Nat.Prime n Nat.Prime (n + 2) Nat.Prime (n + 4)) := n:n < 3 → ¬(Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)) n:hns3:n < 3¬(Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)) n:hns3:n < 3h:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)False n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)False n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:2nFalsen:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2nFalse n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:2nFalse have hne2 : n = 2 := n:n < 3 → ¬(Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)) All goals completed! 🐙 n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:2nhne2:n = 2hnp4:¬Nat.Prime 4False n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (2 + 2)pn4:Nat.Prime (n + 4)hnge2:2nhne2:n = 2hnp4:¬Nat.Prime 4False n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime 4pn4:Nat.Prime (n + 4)hnge2:2nhne2:n = 2hnp4:¬Nat.Prime 4False All goals completed! 🐙 n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2nFalse n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2nhnge1:1nFalsen:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2nhnge1:¬1nFalse n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2nhnge1:1nFalse have hne1 : n = 1 := n:n < 3 → ¬(Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)) All goals completed! 🐙 n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2nhnge1:1nhne1:n = 1hnp1:¬Nat.Prime 1False n:hns3:n < 3pn:Nat.Prime 1pn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2nhnge1:1nhne1:n = 1hnp1:¬Nat.Prime 1False All goals completed! 🐙 n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2nhnge1:¬1nFalse n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2nhnge1:¬1nhnge0:0nFalsen:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2nhnge1:¬1nhnge0:¬0nFalse n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2nhnge1:¬1nhnge0:0nFalse have hne0 : n = 0 := n:n < 3 → ¬(Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)) All goals completed! 🐙 n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2nhnge1:¬1nhnge0:0nhne0:n = 0hnp0:¬Nat.Prime 0False n:hns3:n < 3pn:Nat.Prime 0pn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2nhnge1:¬1nhnge0:0nhne0:n = 0hnp0:¬Nat.Prime 0False All goals completed! 🐙 n:hns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2nhnge1:¬1nhnge0:¬0nFalse All goals completed! 🐙 lemma lem2 (n : ) : (3 < n) ¬ (Nat.Prime n Nat.Prime (n + 2) Nat.Prime (n + 4)) := n:3 < n¬(Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)) n:hng3:3 < n¬(Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)) n:hng3:3 < nh:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)False n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)False n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)super:3n3n + 13n + 2False n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)k0:3nFalsen:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)kr:3n + 13n + 2False n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)k0:3nFalse n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:g:n = 3 * xFalse n:hng3:3 < npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:g:n = 3 * xu1:¬IsUnit nu2:∀ (a b : ), n = a * bIsUnit aIsUnit bFalse n:hng3:3 < npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:g:n = 3 * xu1:¬n = 1u2:∀ (a b : ), n = a * ba = 1b = 1False n:hng3:3 < npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:g:n = 3 * xu1:¬n = 1u2:∀ (a b : ), 3 * x = a * ba = 1b = 1False n:hng3:3 < npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:g:n = 3 * xu1:¬n = 1u2:∀ (a b : ), 3 * x = a * ba = 1b = 1u3:3 * x = 3 * x → 3 = 1x = 1False n:hng3:3 < npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:g:n = 3 * xu1:¬n = 1u2:∀ (a b : ), 3 * x = a * ba = 1b = 1u3:x = 1False n:hng3:3 < npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:g:n = 3 * xu1:¬n = 1u2:∀ (a b : ), 3 * x = a * ba = 1b = 1u3:x = 1False All goals completed! 🐙 n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)kr:3n + 13n + 2False n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)k1:3n + 1Falsen:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)k2:3n + 2False n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)k1:3n + 1False n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:g:n + 1 = 3 * xFalse n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)x:g:n + 1 = 3 * xu1:¬IsUnit (n + 4)u2:∀ (a b : ), n + 4 = a * bIsUnit aIsUnit bFalse n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)x:g:n + 1 = 3 * xu1:Trueu2:∀ (a b : ), n + 4 = a * ba = 1b = 1False n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)x:g:n + 1 = 3 * xu1:Trueu2:∀ (a b : ), n + 4 = a * ba = 1b = 1gp3:n + 4 = 3 * (x + 1)False n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)x:g:n + 1 = 3 * xu1:Trueu2:∀ (a b : ), 3 * (x + 1) = a * ba = 1b = 1gp3:n + 4 = 3 * (x + 1)False n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)x:g:n + 1 = 3 * xu1:Trueu2:∀ (a b : ), 3 * (x + 1) = a * ba = 1b = 1gp3:n + 4 = 3 * (x + 1)u3:3 * (x + 1) = 3 * (x + 1) → 3 = 1x + 1 = 1False n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)x:g:n + 1 = 3 * xu1:Trueu2:∀ (a b : ), 3 * (x + 1) = a * ba = 1b = 1gp3:n + 4 = 3 * (x + 1)u3:x = 0False n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)x:g:n + 1 = 3 * xu1:Trueu2:∀ (a b : ), 3 * (x + 1) = a * ba = 1b = 1gp3:n + 4 = 3 * (x + 1)u3:x = 0False All goals completed! 🐙 n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)k2:3n + 2False n:hng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:g:n + 2 = 3 * xFalse n:hng3:3 < npn:Nat.Prime npn4:Nat.Prime (n + 4)x:g:n + 2 = 3 * xu1:¬IsUnit (n + 2)u2:∀ (a b : ), n + 2 = a * bIsUnit aIsUnit bFalse n:hng3:3 < npn:Nat.Prime npn4:Nat.Prime (n + 4)x:g:n + 2 = 3 * xu1:Trueu2:∀ (a b : ), n + 2 = a * ba = 1b = 1False n:hng3:3 < npn:Nat.Prime npn4:Nat.Prime (n + 4)x:g:n + 2 = 3 * xu1:Trueu2:∀ (a b : ), 3 * x = a * ba = 1b = 1False n:hng3:3 < npn:Nat.Prime npn4:Nat.Prime (n + 4)x:g:n + 2 = 3 * xu1:Trueu2:∀ (a b : ), 3 * x = a * ba = 1b = 1u3:3 * x = 3 * x → 3 = 1x = 1False n:hng3:3 < npn:Nat.Prime npn4:Nat.Prime (n + 4)x:g:n + 2 = 3 * xu1:Trueu2:∀ (a b : ), 3 * x = a * ba = 1b = 1u3:x = 1False n:hng3:3 < npn:Nat.Prime npn4:Nat.Prime (n + 4)x:g:n + 2 = 3 * xu1:Trueu2:∀ (a b : ), 3 * x = a * ba = 1b = 1u3:x = 1False All goals completed! 🐙 theorem pt_forward (n : ) : Nat.Prime n Nat.Prime (n + 2) Nat.Prime (n + 4) n = 3 := n:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)n = 3 n:h:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)n = 3 n:h:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)hns3:n < 3n = 3n:h:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)hns3:¬n < 3n = 3 n:h:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)hns3:n < 3n = 3 n:h:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)hns3:n < 3False n:h:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)hns3:n < 3hn:¬(Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4))False All goals completed! 🐙 n:h:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)hns3:¬n < 3n = 3 n:h:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)hns3:¬n < 3hng3:3 < nn = 3n:h:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)hns3:¬n < 3hng3:¬3 < nn = 3 n:h:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)hns3:¬n < 3hng3:3 < nn = 3 n:h:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)hns3:¬n < 3hng3:3 < nFalse n:h:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)hns3:¬n < 3hng3:3 < nhn:¬(Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4))False All goals completed! 🐙 n:h:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)hns3:¬n < 3hng3:¬3 < nn = 3 All goals completed! 🐙 theorem pt_backward (n : ) : n = 3 Nat.Prime n Nat.Prime (n + 2) Nat.Prime (n + 4) := n:n = 3 → Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4) n:hne3:n = 3Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4) n:hne3:n = 3Nat.Prime 3Nat.Prime (3 + 2)Nat.Prime (3 + 4) n:hne3:n = 3Nat.Prime 3Nat.Prime 5Nat.Prime 7 n:hne3:n = 3Nat.Prime 3n:hne3:n = 3Nat.Prime 5Nat.Prime 7 n:hne3:n = 3Nat.Prime 3 All goals completed! 🐙 n:hne3:n = 3Nat.Prime 5Nat.Prime 7 n:hne3:n = 3Nat.Prime 5n:hne3:n = 3Nat.Prime 7 n:hne3:n = 3Nat.Prime 5 All goals completed! 🐙 n:hne3:n = 3Nat.Prime 7 All goals completed! 🐙 theorem prime_tripple (n : ) : Nat.Prime n Nat.Prime (n + 2) Nat.Prime (n + 4) n = 3 := n:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)n = 3 n:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)n = 3n:n = 3 → Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4) n:Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4)n = 3 All goals completed! 🐙 n:n = 3 → Nat.Prime nNat.Prime (n + 2)Nat.Prime (n + 4) All goals completed! 🐙

5.6. An equivalence on sets (Emma Reichel, Luisa Caspary)

We have U ⊆ V ↔ U = U ∩ V ↔ V = U ∪ V. So, the following needs to be proved:

variable (U V : Set α) example : (U V) U = U V := α:Type u_1U:Set αV:Set αUVU = UV α:Type u_1U:Set αV:Set αh:UVU = UV α:Type u_1U:Set αV:Set αh:UVx:αxUxUV α:Type u_1U:Set αV:Set αh:UVx:αxUxUVα:Type u_1U:Set αV:Set αh:UVx:αxUVxU α:Type u_1U:Set αV:Set αh:UVx:αxUxUV α:Type u_1U:Set αV:Set αh:UVx:αhxU:xUxUV All goals completed! 🐙 α:Type u_1U:Set αV:Set αh:UVx:αxUVxU α:Type u_1U:Set αV:Set αh:UVx:αhxU:xUhxV:xVxU All goals completed! 🐙 example : U = U V V = U V:= α:Type u_1U:Set αV:Set αU = UVV = UV α:Type u_1U:Set αV:Set αh:U = UVV = UV α:Type u_1U:Set αV:Set αh:U = UVx:αxVxUV α:Type u_1U:Set αV:Set αh:U = UVx:αxVxUVα:Type u_1U:Set αV:Set αh:U = UVx:αxUVxV α:Type u_1U:Set αV:Set αh:U = UVx:αxVxUV α:Type u_1U:Set αV:Set αh:U = UVx:αhxV:xVxUV All goals completed! 🐙 α:Type u_1U:Set αV:Set αh:U = UVx:αxUVxV α:Type u_1U:Set αV:Set αh:U = UVx:αh':xUVxV cases h' with | inl hxU => α:Type u_1U:Set αV:Set αh:U = UVx:αhxU:xUVxV All goals completed! 🐙 | inr hxV => All goals completed! 🐙 example : V = U V U V := α:Type u_1U:Set αV:Set αV = UVUV α:Type u_1U:Set αV:Set αh:V = UVUV α:Type u_1U:Set αV:Set αh:V = UVx:αhxU:xUxV α:Type u_1U:Set αV:Set αh:V = UVx:αhxU:xUxUV All goals completed! 🐙