alreadydone

import data.nat.prime

example (m : ℕ) : m ^ 2 ≠ 2 :=
λ he, by cases (nat.dvd_prime nat.prime_two).1 ⟨m * 1, he.symm⟩; subst h; cases he

example (m : ℕ) : m ^ 2 ≠ 2 :=
λ he, by { cases (nat.dvd_prime nat.prime_two).1
  (⟨m, by rw [← he, pow_two]⟩: m ∣ 2) with h; subst h; cases he }
  
import tactic

alreadydone

import ring_theory.unique_factorization_domain
import ring_theory.polynomial.basic
/- based on mathlib at commit 45061f3692 -/

lemma mul_equiv.is_unit_iff {R S : Type*} [monoid R] [monoid S]
  (e : R ≃* S) (r : R) : is_unit r ↔ is_unit (e r) :=
⟨is_unit.map e, λ h, by { convert h.map e.symm, simp }⟩

lemma mul_equiv.prime {R S : Type*} [comm_monoid_with_zero R] [comm_monoid_with_zero S]
  (e : R ≃* S) {r : R} (hr : prime r) : prime (e r) :=

alreadydone

import ring_theory.unique_factorization_domain

variables {α : Type*} [cancel_comm_monoid_with_zero α] (s : submonoid α) [hmem : fact ((0 : α) ∈ s)]

abbreviation semi_saturated := ∀ ⦃a b : α⦄, a ∈ s → a ≠ 0 → a * b ∈ s → b ∈ s
abbreviation saturated := ∀ ⦃a b : α⦄, a ∈ s → a ≠ 0 → b ∣ a → b ∈ s
-- a ≠ 0 → a * b ∈ s → b ∈ s

instance [hs : fact (saturated s)] : fact (semi_saturated s) :=
let hs := hs.out in ⟨λ a b ha hn hab, begin

alreadydone

import ring_theory.graded_algebra.basic

abbreviation saturated {α : Type*} [monoid_with_zero α] (s : submonoid α) : Prop :=
∀ ⦃a b : α⦄, a ∈ s → a ≠ 0 → b ∣ a → b ∈ s

variables {ι R A : Type*} [comm_semiring R] [semiring A] [algebra R A] 

namespace graded_algebra

variables [decidable_eq ι] [add_monoid ι] (𝒜 : ι → submodule R A) [graded_algebra 𝒜]

alreadydone

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : nontrivial (witt_vector p R) := @ulift.nontrivial ?x_1 ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : nontrivial (witt_vector p R) := @witt_vector.nontrivial ?x_3 ?x_4 ?x_5 ?x_6 ?x_7
[class_instances] (1) ?x_7 : nontrivial R := @ulift.nontrivial ?x_8 ?x_9
failed is_def_eq
[class_instances] (1) ?x_7 : nontrivial R := @witt_vector.nontrivial ?x_10 ?x_11 ?x_12 ?x_13 ?x_14
failed is_def_eq
[class_instances] (1) ?x_7 : nontrivial R := @zmod.nontrivial ?x_15 ?x_16
failed is_def_eq

alreadydone

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : nontrivial.{?u_0} (witt_vector.{?l__fresh.516.4} p R) := @ulift.nontrivial.{?u_1 ?u_2} ?x_1 ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : nontrivial.{?u_0} (witt_vector.{?l__fresh.516.4} p R) := @witt_vector.nontrivial.{?u_3} ?x_3 ?x_4 ?x_5 ?x_6 ?x_7
[class_instances] (1) ?x_7 : nontrivial.{?l__fresh.516.4} R := @ulift.nontrivial.{?u_4 ?u_5} ?x_8 ?x_9
failed is_def_eq
[class_instances] (1) ?x_7 : nontrivial.{?l__fresh.516.4} R := @witt_vector.nontrivial.{?u_6} ?x_10 ?x_11 ?x_12 ?x_13 ?x_14
failed is_def_eq
[class_instances] (1) ?x_7 : nontrivial.{?l__fresh.516.4} R := @zmod.nontrivial ?x_15 ?x_16
failed is_def_eq

alreadydone

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : @discrete_valuation_ring (witt_vector p R) (@witt_vector.comm_ring p R hp _inst_1) _inst_2 := @witt_vector.discrete_valuation_ring ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6
[type_context.is_def_eq_detail] [1]: @discrete_valuation_ring (witt_vector p R) (@witt_vector.comm_ring p R hp _inst_1) _inst_2 =?= @discrete_valuation_ring (witt_vector ?x_1 ?x_3)
  (@witt_vector.comm_ring ?x_1 ?x_3 ?x_2 (@euclidean_domain.to_comm_ring ?x_3 (@field.to_euclidean_domain ?x_3 ?x_4)))
  _
[type_context.is_def_eq_detail] [2]: discrete_valuation_ring =?= discrete_valuation_ring
[type_context.is_def_eq_detail] [2]: witt_vector p R =?= witt_vector ?x_1 ?x_3
[type_context.is_def_eq_detail] [3]: witt_vector =?= witt_vector
[type_context.is_def_eq_detail] process_assignment ?x_1 := p
[type_context.is_def_eq_detail] assign: ?x_1 := p

alreadydone

[type_context.is_def_eq_detail] [1]: ?m_2 = ?m_2 =?= witt_vector.comm_ring p R = witt_vector.comm_ring p R
[type_context.is_def_eq_detail] [2]: eq =?= eq
[type_context.is_def_eq_detail] process_assignment ?m_1 := comm_ring (witt_vector p R)
[type_context.is_def_eq_detail] assign: ?m_1 := comm_ring (witt_vector p R)
[type_context.is_def_eq_detail] process_assignment ?m_1 := witt_vector.comm_ring p R
[type_context.is_def_eq_detail] assign: ?m_1 := witt_vector.comm_ring p R
[type_context.is_def_eq_detail] [2]: witt_vector.comm_ring p R =?= witt_vector.comm_ring p R
[type_context.is_def_eq_detail] [3]: _inst_1 =?= euclidean_domain.to_comm_ring
[type_context.is_def_eq_detail] [4]: _inst_1 =?= {add := has_add.add (distrib.to_has_add R),
 add_assoc := _,

alreadydone

--set_option trace.class_instances true
--set_option trace.type_context.is_def_eq_detail true

class comm_ring (n : ℕ) := (ucr : unit)
variable (n : ℕ)
class field extends comm_ring n := (e : empty)
class dvr [comm_ring n] := (u : unit)

instance [c : comm_ring n] : comm_ring n.succ := ⟨id^[19] c.ucr⟩
instance [field n] : dvr n.succ := ⟨()⟩

alreadydone

/- Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Generalization.20of.20map_diff/near/280148939 -/

import data.multiset.basic

/- The stronger version `list.map_diff_sublist` doesn't hold; here is a counterexample. -/
def l₁ := [0,1,2]
def l₂ := [2]
def f : ℕ → ℕ | 1 := 1 | _ := 0

#eval (l₁.map f).diff (l₂.map f) /- [1, 0] -/