text:
/-
Copyright (c) 2022 Riccardo Brasca. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Riccardo Brasca

! This file was ported from Lean 3 source module algebra.gcd_monoid.div
! leanprover-community/mathlib commit b537794f8409bc9598febb79cd510b1df5f4539d
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.GCDMonoid.Finset
import Mathlib.Algebra.GCDMonoid.Basic
import Mathlib.RingTheory.Int.Basic
import Mathlib.RingTheory.Polynomial.Content

/-!
# Basic results about setwise gcds on normalized gcd monoid with a division.

## Main results

* `Finset.Nat.gcd_div_eq_one`: given a nonempty Finset `s` and a function `f` from `s` to
  `ℕ`, if `d = s.gcd`, then the `gcd` of `(f i) / d` equals `1`.
* `Finset.Int.gcd_div_eq_one`: given a nonempty Finset `s` and a function `f` from `s` to
  `ℤ`, if `d = s.gcd`, then the `gcd` of `(f i) / d` equals `1`.
* `Finset.Polynomial.gcd_div_eq_one`: given a nonempty Finset `s` and a function `f` from
  `s` to `K[X]`, if `d = s.gcd`, then the `gcd` of `(f i) / d` equals `1`.

## TODO
Add a typeclass to state these results uniformly.

-/

namespace Finset

namespace Nat

/-- Given a nonempty Finset `s` and a function `f` from `s` to `ℕ`, if `d = s.gcd`,
then the `gcd` of `(f i) / d` is equal to `1`. -/
theorem gcd_div_eq_one {β : Type _} {f : β → ℕ} (s : Finset β) {x : β} (hx : x ∈ s)
    (hfz : f x ≠ 0) : (s.gcd fun b => f b / s.gcd f) = 1 := by
  obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨x, hx⟩
  refine' (Finset.gcd_congr rfl fun a ha => _).trans hg
  rw [he a ha, Nat.mul_div_cancel_left]
  exact Nat.pos_of_ne_zero (mt Finset.gcd_eq_zero_iff.1 fun h => hfz <| h x hx)
#align finset.nat.gcd_div_eq_one Finset.Nat.gcd_div_eq_one

theorem gcd_div_id_eq_one {s : Finset ℕ} {x : ℕ} (hx : x ∈ s) (hnz : x ≠ 0) :
    (s.gcd fun b => b / s.gcd id) = 1 :=
  gcd_div_eq_one s hx hnz
#align finset.nat.gcd_div_id_eq_one Finset.Nat.gcd_div_id_eq_one

end Nat

namespace Int

/-- Given a nonempty Finset `s` and a function `f` from `s` to `ℤ`, if `d = s.gcd`,
then the `gcd` of `(f i) / d` is equal to `1`. -/
theorem gcd_div_eq_one {β : Type _} {f : β → ℤ} (s : Finset β) {x : β} (hx : x ∈ s)
    (hfz : f x ≠ 0) : (s.gcd fun b => f b / s.gcd f) = 1 := by
  obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨x, hx⟩
  refine' (Finset.gcd_congr rfl fun a ha => _).trans hg
  rw [he a ha, Int.mul_ediv_cancel_left]
  exact mt Finset.gcd_eq_zero_iff.1 fun h => hfz <| h x hx
#align finset.int.gcd_div_eq_one Finset.Int.gcd_div_eq_one

theorem gcd_div_id_eq_one {s : Finset ℤ} {x : ℤ} (hx : x ∈ s) (hnz : x ≠ 0) :
    (s.gcd fun b => b / s.gcd id) = 1 :=
  gcd_div_eq_one s hx hnz
#align finset.int.gcd_div_id_eq_one Finset.Int.gcd_div_id_eq_one

end Int

namespace Polynomial

open Polynomial Classical

noncomputable section

variable {K : Type _} [Field K]

/-- Given a nonempty Finset `s` and a function `f` from `s` to `K[X]`, if `d = s.gcd f`,
then the `gcd` of `(f i) / d` is equal to `1`. -/
theorem gcd_div_eq_one {β : Type _} {f : β → Polynomial K} (s : Finset β) {x : β} (hx : x ∈ s)
    (hfz : f x ≠ 0) : (s.gcd fun b => f b / s.gcd f) = 1 := by
  obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨x, hx⟩
  refine' (Finset.gcd_congr rfl fun a ha => _).trans hg
  rw [he a ha, EuclideanDomain.mul_div_cancel_left]
  exact mt Finset.gcd_eq_zero_iff.1 fun h => hfz <| h x hx
#align finset.polynomial.gcd_div_eq_one Finset.Polynomial.gcd_div_eq_one

theorem gcd_div_id_eq_one {s : Finset (Polynomial K)} {x : Polynomial K}
    (hx : x ∈ s) (hnz : x ≠ 0) : (s.gcd fun b => b / s.gcd id) = 1 :=
  gcd_div_eq_one s hx hnz
#align finset.polynomial.gcd_div_id_eq_one Finset.Polynomial.gcd_div_id_eq_one

end

end Polynomial

end Finset

author: leanprover-community


text:
open classical

variables (α : Type*) (p q : α → Prop)
variable a : α
variable r : Prop

example : (∃ x : α, r) → r :=
assume h : ∃ x : α, r,
show r, from
exists.elim h
  (assume w : α,
    assume hw : r, hw)

-- a shorter proof using an implicit match in assume
example : (∃ x : α, r) → r :=
assume ⟨w, hw⟩, hw

example : r → (∃ x : α, r) :=
assume hr : r,
exists.intro a hr

-- a shorter proof using the constructor for exists.intro
example : r → (∃ x : α, r) := λ hr : r, ⟨a, hr⟩

example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
iff.intro
(assume h : ∃ x, p x ∧ r,
  exists.elim h
    (assume w : α,
      assume hw : p w ∧ r,
      show (∃ x, p x) ∧ r,
      from ⟨⟨w, hw.left⟩, hw.right⟩
    )
)
(assume h : (∃ x, p x) ∧ r,
  have hp : ∃ x, p x := h.left,
  have hr : r := h.right,
  exists.elim hp
    (assume w : α,
      assume hw : p w,
      show ∃ x, p x ∧ r,
      from ⟨w, ⟨hw, hr⟩⟩)
)

example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
iff.intro
(assume h : ∃ x, p x ∨ q x,
  exists.elim h
    (assume w : α, assume hw : p w ∨ q w,
      show (∃ x, p x) ∨ (∃ x, q x),
      from or.elim hw
      (assume hp : p w, or.inl ⟨w, hp⟩)
      (assume hq : q w, or.inr ⟨w, hq⟩)
    )
)
(assume h : (∃ x, p x) ∨ (∃ x, q x),
  show ∃ x, p x ∨ q x,
  from or.elim h
  (assume hp : ∃ x, p x,
    exists.elim hp
    (assume w : α, assume hw : p w, ⟨w, or.inl hw⟩)
  )
  (assume hq : ∃ x, q x,
    exists.elim hq
    (assume w : α, assume hw : q w, ⟨w, or.inr hw⟩)
  )
)

theorem dne {p : Prop} (h : ¬¬p) : p :=
or.elim (em p)
  (assume hp : p, hp)
  (assume hnp : ¬p, absurd hnp h)

example : (∀ x, p x) ↔ ¬ (∃ x, ¬ p x) :=
iff.intro
(assume h : ∀ x, p x, show ¬ (∃ x, ¬ p x), from
  assume henp : ∃ x, ¬ p x,
  match henp with ⟨w, hw⟩ :=
    hw (h w)
  end
)
(assume h : ¬ (∃ x, ¬ p x), show ∀ x, p x, from
  assume w : α, show p w, from
    or.elim (em ¬ p w)
      (assume hnpw : ¬ p w, absurd (exists.intro w hnpw) h)
      (assume hnnpw : ¬ ¬ p w, dne hnnpw)
)

example : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
iff.intro
(assume h: (∃ x, p x), show ¬ (∀ x, ¬ p x), from
  assume hnp: (∀ x, ¬ p x), show false, from
  exists.elim h (
    assume w: α , assume hw: p w, absurd hw (hnp w)
  )
)
(assume h: ¬ (∀ x, ¬ p x), show ∃ x, p x, from
  by_contradiction
    (assume h1: ¬ ∃ x, p x, show false, from
      have h2: ∀ x, ¬ p x :=
        (assume w: α, show ¬ p w, from
          (assume h3: p w, show false, from
            h1 ⟨w, h3⟩
          )
        ),
      h h2
    )
)

example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) :=
iff.intro
(assume h: ¬ ∃ x, p x, show ∀ x, ¬ p x, from
  assume w: α, show ¬ p w, from
  assume h1: p w, show false, from
  h ⟨w, h1⟩
)
(assume h: ∀ x, ¬ p x, show ¬ ∃ x, p x, from
  assume h1: ∃ x, p x, show false, from
  exists.elim h1
  (assume w: α, assume hw: p w, h w hw)
)

example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
iff.intro
(assume h: ¬ ∀ x, p x, show ∃ x, ¬ p x, from
  by_contradiction
    (assume h1: ¬ ∃ x, ¬ p x, show false, from
      have h2: ∀ x, p x :=
        (assume w: α, show p w, from
          or.elim (em (p w))
          (assume hpw: p w, hpw)
          (assume hnpw: ¬ p w, absurd (exists.intro w hnpw)  h1)
        ),
      h h2
    )
)
(assume h: ∃ x, ¬ p x, show ¬ ∀ x, p x, from
  match h with ⟨w, hw⟩ :=
    assume h1: ∀ x, p x, show false, from
    hw (h1 w)
  end
)

example : (∀ x, p x → r) ↔ (∃ x, p x) → r :=
iff.intro
(assume h: ∀ x, p x → r, show (∃ x, p x) → r, from
  assume h1: ∃ x, p x, show r, from
    match h1 with ⟨w, hw⟩ :=
      have h2: p w → r := h w,
      h2 hw
    end
)
(assume h: (∃ x, p x) → r, show ∀ x, p x → r, from
  assume w: α, show p w → r, from
    assume hpw: p w, show r, from
      h ⟨w, hpw⟩
)

-- The predicate calculus example: (∃ x, p x → r) ↔ (∀ x, p x) → r
-- is analogous to
-- the propositional calculus example: (P → r) ∨ (Q → r) ↔ P ∧ Q → r
-- First prove: (P ∧ Q → r) → (P → r) ∨ (Q → r)
-- and then modify it to be a proof of the predicate calculus example.

variables P Q : Prop

example : (P ∧ Q → r) → (P → r) ∨ (Q → r) :=
assume h: P ∧ Q → r, show (P → r) ∨ (Q → r), from
or.elim (em r)
(assume hr: r, show (P → r) ∨ (Q → r), from
  or.inl (assume hP: P, hr)
)
(assume hnr: ¬r, show (P → r) ∨ (Q → r), from
  or.elim (em P)
  (assume hP: P,show (P → r) ∨ (Q → r), from
    or.elim (em Q)
    (assume hQ: Q,
      have hPQ: P ∧ Q := and.intro hP hQ,
      have hr: r := h hPQ,
      show (P → r) ∨ (Q → r), from
      absurd hr hnr
    )
    (assume hnQ: ¬Q,
    have hQr : Q → r := (assume hQ: Q, show r, from absurd hQ hnQ),
    show (P → r) ∨ (Q → r), from or.inr hQr)
  )
  (assume hnP: ¬P,
    have hPr : P → r := (assume hP: P, show r, from absurd hP hnP),
    show (P → r) ∨ (Q → r), from or.inl hPr
  )
)

-- In the above proof we first use em on r.
-- The proof when r holds is trivial since anything implies r.
-- We then deal with the case when ¬ r holds.
-- Then we examine each conjunct and apply em to it.
-- I need the following lemma, which I proved in an example above.

lemma not_forall_exists_not : ¬ (∀ x: α, p x) → ∃ x, ¬(p x) :=
assume h: ¬ ∀ x: α, p x, show ∃ x, ¬(p x), from
by_contradiction
  (assume h1: ¬(∃ x, ¬(p x)), show false, from
    have h2: ∀ x, p x :=
      (assume w: α, show p w, from
        or.elim (em (p w))
        (assume hpw: p w, hpw)
        (assume hnpw: ¬ p w, absurd (exists.intro w hnpw)  h1)
      ),
    h h2
  )

example : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
iff.intro
(assume h: ∃ x, p x → r, show (∀ x, p x) → r, from
  match h with ⟨w, hw⟩ :=
    assume h1: ∀ x, p x, show r, from
    have h2: p w := h1 w,
    hw h2
  end
)
(assume h: (∀ x, p x) → r, show ∃ x, p x → r, from
  by_cases
  (assume hr: r,
    have h1: ∀ x: α, p x → r := assume w: α, assume hw: p w, hr,
    show ∃ x, p x → r, from
    ⟨a, h1 a⟩
  )
  (assume hnr: ¬r, show ∃ x, p x → r, from
    by_cases
    (assume h1: ∀ x, p x, show ∃ x, p x → r, from
      absurd (h h1) hnr
    )
    (assume h1: ¬ ∀ x, p x,
      have h2: ∃ x, ¬ (p x) := not_forall_exists_not α p h1,
      show ∃ x, p x → r, from
        match h2 with ⟨w, hw⟩ :=
          have hpwr : p w → r := (assume hpw, absurd hpw hw),
          ⟨w, hpwr⟩
        end
    )
  )
)

example : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
iff.intro
(assume h: ∃ x, r → p x, show r → ∃ x, p x, from
  assume hr: r, show ∃ x, p x, from
  match h with ⟨w, hw⟩ :=
    have hpw: p w := hw hr,
    ⟨w, hpw⟩
  end
)
(assume h: r → ∃ x, p x, show ∃ x, r → p x, from
  by_cases
    (assume hr: r,
      have hepx : ∃ x, p x := h hr,
      show ∃ x, r → p x, from
      match hepx with ⟨w, hpw⟩ :=
        have hrpw : r → p w := (assume hr1: r, hpw),
        ⟨w, hrpw⟩
      end
    )
    (assume hnr: ¬r,
      have hrpa: r → p a := (assume hr: r, absurd hr hnr),
      ⟨a, hrpa⟩
    )
)

#check @by_cases

#check @by_contradiction

author: agryman

repo: theorem-proving-in-lean


text:
/-
Copyright (c) 2018 Patrick Massot. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Patrick Massot, Johannes Hölzl

Theory of topological rings.
-/
import topology.algebra.group
import ring_theory.ideal.basic
import ring_theory.subring
import algebra.ring.prod

open classical set filter topological_space
open_locale classical

section topological_ring
variables (α : Type*)

/-- A topological semiring is a semiring where addition and multiplication are continuous. -/
class topological_semiring [topological_space α] [semiring α]
  extends has_continuous_add α, has_continuous_mul α : Prop

section
variables {α} [topological_space α] [semiring α] [topological_semiring α]

/-- The (topological-space) closure of a subsemiring of a topological semiring is
itself a subsemiring. -/
def subsemiring.topological_closure (s : subsemiring α) : subsemiring α :=
{ carrier := closure (s : set α),
  ..(s.to_submonoid.topological_closure),
  ..(s.to_add_submonoid.topological_closure ) }

@[simp] lemma subsemiring.topological_closure_coe (s : subsemiring α) :
  (s.topological_closure : set α) = closure (s : set α) :=
rfl

instance subsemiring.topological_closure_topological_semiring (s : subsemiring α) :
  topological_semiring (s.topological_closure) :=
{ ..s.to_add_submonoid.topological_closure_has_continuous_add,
  ..s.to_submonoid.topological_closure_has_continuous_mul }

lemma subsemiring.subring_topological_closure (s : subsemiring α) :
  s ≤ s.topological_closure :=
subset_closure

lemma subsemiring.is_closed_topological_closure (s : subsemiring α) :
  is_closed (s.topological_closure : set α) :=
by convert is_closed_closure

lemma subsemiring.topological_closure_minimal
  (s : subsemiring α) {t : subsemiring α} (h : s ≤ t) (ht : is_closed (t : set α)) :
  s.topological_closure ≤ t :=
closure_minimal h ht

instance (S : submonoid α) : has_continuous_mul (S.topological_closure) :=
{ continuous_mul :=
  begin
    apply continuous_induced_rng,
    change continuous (λ p : S.topological_closure × S.topological_closure, (p.1 : α) * (p.2 : α)),
    continuity,
  end }

/-- The product topology on the cartesian product of two topological semirings
  makes the product into a topological semiring. -/
instance prod_semiring {β : Type*}
  [semiring β] [topological_space β] [topological_semiring β] : topological_semiring (α × β) :=
{}

end

/-- A topological ring is a ring where the ring operations are continuous. -/
class topological_ring [topological_space α] [ring α]
  extends has_continuous_add α, has_continuous_mul α : Prop :=
(continuous_neg : continuous (λa:α, -a))

variables {α} [ring α] [topological_space α]

section
variables [t : topological_ring α]
@[priority 100] -- see Note [lower instance priority]
instance topological_ring.to_topological_semiring : topological_semiring α := {..t}

@[priority 100] -- see Note [lower instance priority]
instance topological_ring.to_topological_add_group : topological_add_group α := {..t}
end

variables [topological_ring α]

/-- The product topology on the cartesian product of two topological rings
  makes the product into a topological ring. -/
instance prod_ring {β : Type*}
  [ring β] [topological_space β] [topological_ring β] : topological_ring (α × β) :=
{ continuous_neg := continuous_neg }

/-- In a topological ring, the left-multiplication `add_monoid_hom` is continuous. -/
lemma mul_left_continuous (x : α) : continuous (add_monoid_hom.mul_left x) :=
continuous_const.mul continuous_id

/-- In a topological ring, the right-multiplication `add_monoid_hom` is continuous. -/
lemma mul_right_continuous (x : α) : continuous (add_monoid_hom.mul_right x) :=
continuous_id.mul continuous_const

/-- The (topological-space) closure of a subring of a topological semiring is
itself a subring. -/
def subring.topological_closure (S : subring α) : subring α :=
{ carrier := closure (S : set α),
  ..(S.to_submonoid.topological_closure),
  ..(S.to_add_subgroup.topological_closure) }

instance subring.topological_closure_topological_ring (s : subring α) :
  topological_ring (s.topological_closure) :=
{ ..s.to_add_subgroup.topological_closure_topological_add_group,
  ..s.to_submonoid.topological_closure_has_continuous_mul }

lemma subring.subring_topological_closure (s : subring α) :
  s ≤ s.topological_closure :=
subset_closure

lemma subring.is_closed_topological_closure (s : subring α) :
  is_closed (s.topological_closure : set α) :=
by convert is_closed_closure

lemma subring.topological_closure_minimal
  (s : subring α) {t : subring α} (h : s ≤ t) (ht : is_closed (t : set α)) :
  s.topological_closure ≤ t :=
closure_minimal h ht

end topological_ring

section topological_comm_ring
variables {α : Type*} [topological_space α] [comm_ring α] [topological_ring α]

/-- The closure of an ideal in a topological ring as an ideal. -/
def ideal.closure (S : ideal α) : ideal α :=
{ carrier := closure S,
  smul_mem' := assume c x hx,
    have continuous (λx:α, c * x) := continuous_const.mul continuous_id,
    map_mem_closure this hx $ assume a, S.mul_mem_left _,
  ..(add_submonoid.topological_closure S.to_add_submonoid) }

@[simp] lemma ideal.coe_closure (S : ideal α) :
  (S.closure : set α) = closure S := rfl

end topological_comm_ring

section topological_ring
variables {α : Type*} [topological_space α] [comm_ring α] (N : ideal α)
open ideal.quotient

instance topological_ring_quotient_topology : topological_space N.quotient :=
by dunfold ideal.quotient submodule.quotient; apply_instance

lemma quotient_ring_saturate {α : Type*} [comm_ring α] (N : ideal α) (s : set α) :
  mk N ⁻¹' (mk N '' s) = (⋃ x : N, (λ y, x.1 + y) '' s) :=
begin
  ext x,
  simp only [mem_preimage, mem_image, mem_Union, ideal.quotient.eq],
  split,
  { exact assume ⟨a, a_in, h⟩, ⟨⟨_, N.neg_mem h⟩, a, a_in, by simp⟩ },
  { exact assume ⟨⟨i, hi⟩, a, ha, eq⟩, ⟨a, ha,
      by rw [← eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub];
      exact N.neg_mem hi⟩ }
end

variable [topological_ring α]

lemma quotient_ring.is_open_map_coe : is_open_map (mk N) :=
begin
  assume s s_op,
  show is_open (mk N ⁻¹' (mk N '' s)),
  rw quotient_ring_saturate N s,
  exact is_open_Union (assume ⟨n, _⟩, is_open_map_add_left n s s_op)
end

lemma quotient_ring.quotient_map_coe_coe : quotient_map (λ p : α × α, (mk N p.1, mk N p.2)) :=
begin
  apply is_open_map.to_quotient_map,
  { exact (quotient_ring.is_open_map_coe N).prod (quotient_ring.is_open_map_coe N) },
  { exact (continuous_quot_mk.comp continuous_fst).prod_mk
          (continuous_quot_mk.comp continuous_snd) },
  { rintro ⟨⟨x⟩, ⟨y⟩⟩,
    exact ⟨(x, y), rfl⟩ }
end

instance topological_ring_quotient : topological_ring N.quotient :=
{ continuous_add :=
    have cont : continuous (mk N ∘ (λ (p : α × α), p.fst + p.snd)) :=
      continuous_quot_mk.comp continuous_add,
    (quotient_map.continuous_iff (quotient_ring.quotient_map_coe_coe N)).2 cont,
  continuous_neg :=
  begin
    convert continuous_quotient_lift _ (continuous_quot_mk.comp continuous_neg),
    apply_instance,
  end,
  continuous_mul :=
    have cont : continuous (mk N ∘ (λ (p : α × α), p.fst * p.snd)) :=
      continuous_quot_mk.comp continuous_mul,
    (quotient_map.continuous_iff (quotient_ring.quotient_map_coe_coe N)).2 cont }

end topological_ring

author: JLimperg