text:
import Preloaded

-- Task: prove that n + m = n + m
theorem immediate : ∀ n m : ℕ, n + m = n + m :=
  by intros; refl

author: DonaldKellett


text:
/-
Copyright (c) 2018 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
-/
import Mathlib.PrePort
import Mathlib.Lean3Lib.init.default
import Mathlib.algebra.group.hom
import Mathlib.algebra.group.type_tags
import Mathlib.algebra.group.units_hom
import Mathlib.PostPort

universes u_8 u_9 l u_3 u_4 u_1 u_5 u_2 u_6 u_7

namespace Mathlib

/-!
# Multiplicative and additive equivs

In this file we define two extensions of `equiv` called `add_equiv` and `mul_equiv`, which are
datatypes representing isomorphisms of `add_monoid`s/`add_group`s and `monoid`s/`group`s.

## Notations

The extended equivs all have coercions to functions, and the coercions are the canonical
notation when treating the isomorphisms as maps.

## Implementation notes

The fields for `mul_equiv`, `add_equiv` now avoid the unbundled `is_mul_hom` and `is_add_hom`, as
these are deprecated.

## Tags

equiv, mul_equiv, add_equiv
-/

/-- add_equiv α β is the type of an equiv α ≃ β which preserves addition. -/
structure add_equiv (A : Type u_8) (B : Type u_9) [Add A] [Add B] extends add_hom A B, A ≃ B where

/-- The `equiv` underlying an `add_equiv`. -/
/-- The `add_hom` underlying a `add_equiv`. -/
/-- `mul_equiv α β` is the type of an equiv `α ≃ β` which preserves multiplication. -/
structure mul_equiv (M : Type u_8) (N : Type u_9) [Mul M] [Mul N] extends mul_hom M N, M ≃ N where

infixl:25 " ≃* " => Mathlib.mul_equiv

infixl:25 " ≃+ " => Mathlib.add_equiv

/-- The `equiv` underlying a `mul_equiv`. -/
/-- The `mul_hom` underlying a `mul_equiv`. -/
namespace mul_equiv

protected instance has_coe_to_fun {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] :
    has_coe_to_fun (M ≃* N) :=
  has_coe_to_fun.mk (fun (x : M ≃* N) => M → N) to_fun

@[simp] theorem Mathlib.add_equiv.to_fun_apply {M : Type u_3} {N : Type u_4} [Add M] [Add N]
    {f : M ≃+ N} {m : M} : add_equiv.to_fun f m = coe_fn f m :=
  rfl

@[simp] theorem Mathlib.add_equiv.to_equiv_apply {M : Type u_3} {N : Type u_4} [Add M] [Add N]
    {f : M ≃+ N} {m : M} : coe_fn (add_equiv.to_equiv f) m = coe_fn f m :=
  rfl

/-- A multiplicative isomorphism preserves multiplication (canonical form). -/
@[simp] theorem map_mul {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : M ≃* N) (x : M) (y : M) :
    coe_fn f (x * y) = coe_fn f x * coe_fn f y :=
  map_mul' f

/-- Makes a multiplicative isomorphism from a bijection which preserves multiplication. -/
def mk' {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : M ≃ N)
    (h : ∀ (x y : M), coe_fn f (x * y) = coe_fn f x * coe_fn f y) : M ≃* N :=
  mk (equiv.to_fun f) (equiv.inv_fun f) (equiv.left_inv f) (equiv.right_inv f) h

protected theorem Mathlib.add_equiv.bijective {M : Type u_3} {N : Type u_4} [Add M] [Add N]
    (e : M ≃+ N) : function.bijective ⇑e :=
  equiv.bijective (add_equiv.to_equiv e)

protected theorem Mathlib.add_equiv.injective {M : Type u_3} {N : Type u_4} [Add M] [Add N]
    (e : M ≃+ N) : function.injective ⇑e :=
  equiv.injective (add_equiv.to_equiv e)

protected theorem Mathlib.add_equiv.surjective {M : Type u_3} {N : Type u_4} [Add M] [Add N]
    (e : M ≃+ N) : function.surjective ⇑e :=
  equiv.surjective (add_equiv.to_equiv e)

/-- The identity map is a multiplicative isomorphism. -/
def refl (M : Type u_1) [Mul M] : M ≃* M :=
  mk (equiv.to_fun (equiv.refl M)) (equiv.inv_fun (equiv.refl M)) sorry sorry sorry

protected instance inhabited {M : Type u_3} [Mul M] : Inhabited (M ≃* M) := { default := refl M }

/-- The inverse of an isomorphism is an isomorphism. -/
def Mathlib.add_equiv.symm {M : Type u_3} {N : Type u_4} [Add M] [Add N] (h : M ≃+ N) : N ≃+ M :=
  add_equiv.mk (equiv.to_fun (equiv.symm (add_equiv.to_equiv h)))
    (equiv.inv_fun (equiv.symm (add_equiv.to_equiv h))) sorry sorry sorry

/-- See Note [custom simps projection] -/
-- we don't hyperlink the note in the additive version, since that breaks syntax highlighting

-- in the whole file.

def simps.inv_fun {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (e : M ≃* N) : N → M := ⇑(symm e)

@[simp] theorem Mathlib.add_equiv.to_equiv_symm {M : Type u_3} {N : Type u_4} [Add M] [Add N]
    (f : M ≃+ N) : add_equiv.to_equiv (add_equiv.symm f) = equiv.symm (add_equiv.to_equiv f) :=
  rfl

@[simp] theorem Mathlib.add_equiv.coe_mk {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : M → N)
    (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f)
    (h₃ : ∀ (x y : M), f (x + y) = f x + f y) : ⇑(add_equiv.mk f g h₁ h₂ h₃) = f :=
  rfl

@[simp] theorem Mathlib.add_equiv.coe_symm_mk {M : Type u_3} {N : Type u_4} [Add M] [Add N]
    (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f)
    (h₃ : ∀ (x y : M), f (x + y) = f x + f y) : ⇑(add_equiv.symm (add_equiv.mk f g h₁ h₂ h₃)) = g :=
  rfl

/-- Transitivity of multiplication-preserving isomorphisms -/
def Mathlib.add_equiv.trans {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P]
    (h1 : M ≃+ N) (h2 : N ≃+ P) : M ≃+ P :=
  add_equiv.mk (equiv.to_fun (equiv.trans (add_equiv.to_equiv h1) (add_equiv.to_equiv h2)))
    (equiv.inv_fun (equiv.trans (add_equiv.to_equiv h1) (add_equiv.to_equiv h2))) sorry sorry sorry

/-- e.right_inv in canonical form -/
@[simp] theorem apply_symm_apply {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (e : M ≃* N)
    (y : N) : coe_fn e (coe_fn (symm e) y) = y :=
  equiv.apply_symm_apply (to_equiv e)

/-- e.left_inv in canonical form -/
@[simp] theorem Mathlib.add_equiv.symm_apply_apply {M : Type u_3} {N : Type u_4} [Add M] [Add N]
    (e : M ≃+ N) (x : M) : coe_fn (add_equiv.symm e) (coe_fn e x) = x :=
  equiv.symm_apply_apply (add_equiv.to_equiv e)

@[simp] theorem Mathlib.add_equiv.refl_apply {M : Type u_3} [Add M] (m : M) :
    coe_fn (add_equiv.refl M) m = m :=
  rfl

@[simp] theorem Mathlib.add_equiv.trans_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M]
    [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (m : M) :
    coe_fn (add_equiv.trans e₁ e₂) m = coe_fn e₂ (coe_fn e₁ m) :=
  rfl

@[simp] theorem Mathlib.add_equiv.apply_eq_iff_eq {M : Type u_3} {N : Type u_4} [Add M] [Add N]
    (e : M ≃+ N) {x : M} {y : M} : coe_fn e x = coe_fn e y ↔ x = y :=
  function.injective.eq_iff (add_equiv.injective e)

theorem Mathlib.add_equiv.apply_eq_iff_symm_apply {M : Type u_3} {N : Type u_4} [Add M] [Add N]
    (e : M ≃+ N) {x : M} {y : N} : coe_fn e x = y ↔ x = coe_fn (add_equiv.symm e) y :=
  equiv.apply_eq_iff_eq_symm_apply (add_equiv.to_equiv e)

theorem symm_apply_eq {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} :
    coe_fn (symm e) x = y ↔ x = coe_fn e y :=
  equiv.symm_apply_eq (to_equiv e)

theorem eq_symm_apply {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} :
    y = coe_fn (symm e) x ↔ coe_fn e y = x :=
  equiv.eq_symm_apply (to_equiv e)

/-- a multiplicative equiv of monoids sends 1 to 1 (and is hence a monoid isomorphism) -/
@[simp] theorem Mathlib.add_equiv.map_zero {M : Type u_1} {N : Type u_2} [add_monoid M]
    [add_monoid N] (h : M ≃+ N) : coe_fn h 0 = 0 :=
  sorry

@[simp] theorem Mathlib.add_equiv.map_eq_zero_iff {M : Type u_1} {N : Type u_2} [add_monoid M]
    [add_monoid N] (h : M ≃+ N) {x : M} : coe_fn h x = 0 ↔ x = 0 :=
  add_equiv.map_zero h ▸ equiv.apply_eq_iff_eq (add_equiv.to_equiv h)

theorem map_ne_one_iff {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (h : M ≃* N) {x : M} :
    coe_fn h x ≠ 1 ↔ x ≠ 1 :=
  { mp := mt (iff.mpr (map_eq_one_iff h)), mpr := mt (iff.mp (map_eq_one_iff h)) }

/-- A bijective `monoid` homomorphism is an isomorphism -/
def Mathlib.add_equiv.of_bijective {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N]
    (f : M →+ N) (hf : function.bijective ⇑f) : M ≃+ N :=
  add_equiv.mk (equiv.to_fun (equiv.of_bijective (⇑f) hf))
    (equiv.inv_fun (equiv.of_bijective (⇑f) hf)) sorry sorry (add_monoid_hom.map_add' f)

/--
Extract the forward direction of a multiplicative equivalence
as a multiplication-preserving function.
-/
def Mathlib.add_equiv.to_add_monoid_hom {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N]
    (h : M ≃+ N) : M →+ N :=
  add_monoid_hom.mk (add_equiv.to_fun h) (add_equiv.map_zero h) sorry

@[simp] theorem coe_to_monoid_hom {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (e : M ≃* N) :
    ⇑(to_monoid_hom e) = ⇑e :=
  rfl

theorem Mathlib.add_equiv.to_add_monoid_hom_apply {M : Type u_1} {N : Type u_2} [add_monoid M]
    [add_monoid N] (e : M ≃+ N) (x : M) : coe_fn (add_equiv.to_add_monoid_hom e) x = coe_fn e x :=
  rfl

/-- A multiplicative equivalence of groups preserves inversion. -/
@[simp] theorem map_inv {G : Type u_6} {H : Type u_7} [group G] [group H] (h : G ≃* H) (x : G) :
    coe_fn h (x⁻¹) = (coe_fn h x⁻¹) :=
  monoid_hom.map_inv (to_monoid_hom h) x

/-- Two multiplicative isomorphisms agree if they are defined by the
    same underlying function. -/
theorem ext {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] {f : M ≃* N} {g : M ≃* N}
    (h : ∀ (x : M), coe_fn f x = coe_fn g x) : f = g :=
  sorry

protected theorem congr_arg {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] {f : M ≃* N} {x : M}
    {x' : M} : x = x' → coe_fn f x = coe_fn f x' :=
  sorry

protected theorem congr_fun {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] {f : M ≃* N} {g : M ≃* N}
    (h : f = g) (x : M) : coe_fn f x = coe_fn g x :=
  h ▸ rfl

theorem ext_iff {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] {f : M ≃* N} {g : M ≃* N} :
    f = g ↔ ∀ (x : M), coe_fn f x = coe_fn g x :=
  { mp := fun (h : f = g) (x : M) => h ▸ rfl, mpr := ext }

theorem Mathlib.add_equiv.to_add_monoid_hom_injective {M : Type u_1} {N : Type u_2} [add_monoid M]
    [add_monoid N] : function.injective add_equiv.to_add_monoid_hom :=
  fun (f g : M ≃+ N) (h : add_equiv.to_add_monoid_hom f = add_equiv.to_add_monoid_hom g) =>
    add_equiv.ext (iff.mp add_monoid_hom.ext_iff h)

end mul_equiv

-- We don't use `to_additive` to generate definition because it fails to tell Lean about

-- equational lemmas

/-- Given a pair of additive monoid homomorphisms `f`, `g` such that `g.comp f = id` and
`f.comp g = id`, returns an additive equivalence with `to_fun = f` and `inv_fun = g`.  This
constructor is useful if the underlying type(s) have specialized `ext` lemmas for additive
monoid homomorphisms. -/
def add_monoid_hom.to_add_equiv {M : Type u_3} {N : Type u_4} [add_monoid M] [add_monoid N]
    (f : M →+ N) (g : N →+ M) (h₁ : add_monoid_hom.comp g f = add_monoid_hom.id M)
    (h₂ : add_monoid_hom.comp f g = add_monoid_hom.id N) : M ≃+ N :=
  add_equiv.mk ⇑f ⇑g sorry sorry (add_monoid_hom.map_add f)

/-- Given a pair of monoid homomorphisms `f`, `g` such that `g.comp f = id` and `f.comp g = id`,
returns an multiplicative equivalence with `to_fun = f` and `inv_fun = g`.  This constructor is
useful if the underlying type(s) have specialized `ext` lemmas for monoid homomorphisms. -/
def monoid_hom.to_mul_equiv {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] (f : M →* N)
    (g : N →* M) (h₁ : monoid_hom.comp g f = monoid_hom.id M)
    (h₂ : monoid_hom.comp f g = monoid_hom.id N) : M ≃* N :=
  mul_equiv.mk ⇑f ⇑g sorry sorry (monoid_hom.map_mul f)

@[simp] theorem monoid_hom.coe_to_mul_equiv {M : Type u_3} {N : Type u_4} [monoid M] [monoid N]
    (f : M →* N) (g : N →* M) (h₁ : monoid_hom.comp g f = monoid_hom.id M)
    (h₂ : monoid_hom.comp f g = monoid_hom.id N) : ⇑(monoid_hom.to_mul_equiv f g h₁ h₂) = ⇑f :=
  rfl

/-- An additive equivalence of additive groups preserves subtraction. -/
theorem add_equiv.map_sub {A : Type u_1} {B : Type u_2} [add_group A] [add_group B] (h : A ≃+ B)
    (x : A) (y : A) : coe_fn h (x - y) = coe_fn h x - coe_fn h y :=
  add_monoid_hom.map_sub (add_equiv.to_add_monoid_hom h) x y

protected instance add_equiv.inhabited {M : Type u_1} [Add M] : Inhabited (M ≃+ M) :=
  { default := add_equiv.refl M }

/-- A group is isomorphic to its group of units. -/
def to_add_units {G : Type u_1} [add_group G] : G ≃+ add_units G :=
  add_equiv.mk (fun (x : G) => add_units.mk x (-x) (add_neg_self x) (neg_add_self x)) coe sorry
    sorry sorry

namespace units

/-- A multiplicative equivalence of monoids defines a multiplicative equivalence
of their groups of units. -/
def map_equiv {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] (h : M ≃* N) :
    units M ≃* units N :=
  mul_equiv.mk (monoid_hom.to_fun (map (mul_equiv.to_monoid_hom h)))
    ⇑(map (mul_equiv.to_monoid_hom (mul_equiv.symm h))) sorry sorry sorry

/-- Left multiplication by a unit of a monoid is a permutation of the underlying type. -/
def mul_left {M : Type u_3} [monoid M] (u : units M) : equiv.perm M :=
  equiv.mk (fun (x : M) => ↑u * x) (fun (x : M) => ↑(u⁻¹) * x) (inv_mul_cancel_left u)
    (mul_inv_cancel_left u)

@[simp] theorem coe_mul_left {M : Type u_3} [monoid M] (u : units M) : ⇑(mul_left u) = Mul.mul ↑u :=
  rfl

@[simp] theorem Mathlib.add_units.add_left_symm {M : Type u_3} [add_monoid M] (u : add_units M) :
    equiv.symm (add_units.add_left u) = add_units.add_left (-u) :=
  equiv.ext fun (x : M) => rfl

/-- Right multiplication by a unit of a monoid is a permutation of the underlying type. -/
def mul_right {M : Type u_3} [monoid M] (u : units M) : equiv.perm M :=
  equiv.mk (fun (x : M) => x * ↑u) (fun (x : M) => x * ↑(u⁻¹)) sorry sorry

@[simp] theorem Mathlib.add_units.coe_add_right {M : Type u_3} [add_monoid M] (u : add_units M) :
    ⇑(add_units.add_right u) = fun (x : M) => x + ↑u :=
  rfl

@[simp] theorem Mathlib.add_units.add_right_symm {M : Type u_3} [add_monoid M] (u : add_units M) :
    equiv.symm (add_units.add_right u) = add_units.add_right (-u) :=
  equiv.ext fun (x : M) => rfl

end units

namespace equiv

/-- Left multiplication in a `group` is a permutation of the underlying type. -/
protected def add_left {G : Type u_6} [add_group G] (a : G) : perm G :=
  add_units.add_left (coe_fn to_add_units a)

@[simp] theorem coe_add_left {G : Type u_6} [add_group G] (a : G) :
    ⇑(equiv.add_left a) = Add.add a :=
  rfl

/-- extra simp lemma that `dsimp` can use. `simp` will never use this. -/
@[simp] theorem add_left_symm_apply {G : Type u_6} [add_group G] (a : G) :
    ⇑(equiv.symm (equiv.add_left a)) = Add.add (-a) :=
  rfl

@[simp] theorem mul_left_symm {G : Type u_6} [group G] (a : G) :
    equiv.symm (equiv.mul_left a) = equiv.mul_left (a⁻¹) :=
  ext fun (x : G) => rfl

/-- Right multiplication in a `group` is a permutation of the underlying type. -/
protected def add_right {G : Type u_6} [add_group G] (a : G) : perm G :=
  add_units.add_right (coe_fn to_add_units a)

@[simp] theorem coe_mul_right {G : Type u_6} [group G] (a : G) :
    ⇑(equiv.mul_right a) = fun (x : G) => x * a :=
  rfl

@[simp] theorem mul_right_symm {G : Type u_6} [group G] (a : G) :
    equiv.symm (equiv.mul_right a) = equiv.mul_right (a⁻¹) :=
  ext fun (x : G) => rfl

/-- extra simp lemma that `dsimp` can use. `simp` will never use this.  -/
@[simp] theorem add_right_symm_apply {G : Type u_6} [add_group G] (a : G) :
    ⇑(equiv.symm (equiv.add_right a)) = fun (x : G) => x + -a :=
  rfl

/-- Inversion on a `group` is a permutation of the underlying type. -/
protected def neg (G : Type u_6) [add_group G] : perm G :=
  mk (fun (a : G) => -a) (fun (a : G) => -a) sorry sorry

@[simp] theorem coe_inv {G : Type u_6} [group G] : ⇑(equiv.inv G) = has_inv.inv := rfl

@[simp] theorem neg_symm {G : Type u_6} [add_group G] : equiv.symm (equiv.neg G) = equiv.neg G :=
  rfl

end equiv

/-- Reinterpret `G ≃+ H` as `multiplicative G ≃* multiplicative H`. -/
def add_equiv.to_multiplicative {G : Type u_6} {H : Type u_7} [add_monoid G] [add_monoid H] :
    G ≃+ H ≃ (multiplicative G ≃* multiplicative H) :=
  equiv.mk
    (fun (f : G ≃+ H) =>
      mul_equiv.mk ⇑(coe_fn add_monoid_hom.to_multiplicative (add_equiv.to_add_monoid_hom f))
        ⇑(coe_fn add_monoid_hom.to_multiplicative (add_equiv.to_add_monoid_hom (add_equiv.symm f)))
        sorry sorry sorry)
    (fun (f : multiplicative G ≃* multiplicative H) =>
      add_equiv.mk ⇑(mul_equiv.to_monoid_hom f) ⇑(mul_equiv.to_monoid_hom (mul_equiv.symm f)) sorry
        sorry sorry)
    sorry sorry

/-- Reinterpret `G ≃* H` as `additive G ≃+ additive H`. -/
def mul_equiv.to_additive {G : Type u_6} {H : Type u_7} [monoid G] [monoid H] :
    G ≃* H ≃ (additive G ≃+ additive H) :=
  equiv.mk
    (fun (f : G ≃* H) =>
      add_equiv.mk ⇑(coe_fn monoid_hom.to_additive (mul_equiv.to_monoid_hom f))
        ⇑(coe_fn monoid_hom.to_additive (mul_equiv.to_monoid_hom (mul_equiv.symm f))) sorry sorry
        sorry)
    (fun (f : additive G ≃+ additive H) =>
      mul_equiv.mk ⇑(add_equiv.to_add_monoid_hom f)
        ⇑(add_equiv.to_add_monoid_hom (add_equiv.symm f)) sorry sorry sorry)
    sorry sorry

/-- Reinterpret `additive G ≃+ H` as `G ≃* multiplicative H`. -/
def add_equiv.to_multiplicative' {G : Type u_6} {H : Type u_7} [monoid G] [add_monoid H] :
    additive G ≃+ H ≃ (G ≃* multiplicative H) :=
  equiv.mk
    (fun (f : additive G ≃+ H) =>
      mul_equiv.mk ⇑(coe_fn add_monoid_hom.to_multiplicative' (add_equiv.to_add_monoid_hom f))
        ⇑(coe_fn add_monoid_hom.to_multiplicative''
            (add_equiv.to_add_monoid_hom (add_equiv.symm f)))
        sorry sorry sorry)
    (fun (f : G ≃* multiplicative H) =>
      add_equiv.mk ⇑(mul_equiv.to_monoid_hom f) ⇑(mul_equiv.to_monoid_hom (mul_equiv.symm f)) sorry
        sorry sorry)
    sorry sorry

/-- Reinterpret `G ≃* multiplicative H` as `additive G ≃+ H` as. -/
def mul_equiv.to_additive' {G : Type u_6} {H : Type u_7} [monoid G] [add_monoid H] :
    G ≃* multiplicative H ≃ (additive G ≃+ H) :=
  equiv.symm add_equiv.to_multiplicative'

/-- Reinterpret `G ≃+ additive H` as `multiplicative G ≃* H`. -/
def add_equiv.to_multiplicative'' {G : Type u_6} {H : Type u_7} [add_monoid G] [monoid H] :
    G ≃+ additive H ≃ (multiplicative G ≃* H) :=
  equiv.mk
    (fun (f : G ≃+ additive H) =>
      mul_equiv.mk ⇑(coe_fn add_monoid_hom.to_multiplicative'' (add_equiv.to_add_monoid_hom f))
        ⇑(coe_fn add_monoid_hom.to_multiplicative' (add_equiv.to_add_monoid_hom (add_equiv.symm f)))
        sorry sorry sorry)
    (fun (f : multiplicative G ≃* H) =>
      add_equiv.mk ⇑(mul_equiv.to_monoid_hom f) ⇑(mul_equiv.to_monoid_hom (mul_equiv.symm f)) sorry
        sorry sorry)
    sorry sorry

/-- Reinterpret `multiplicative G ≃* H` as `G ≃+ additive H` as. -/
def mul_equiv.to_additive'' {G : Type u_6} {H : Type u_7} [add_monoid G] [monoid H] :
    multiplicative G ≃* H ≃ (G ≃+ additive H) :=
  equiv.symm add_equiv.to_multiplicative''

end Mathlib

author: AurelienSaue


text:
/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes, Patrick Stevens
-/
import data.nat.choose.basic
import tactic.linarith
import algebra.big_operators.ring
import algebra.big_operators.intervals
import algebra.big_operators.order
import algebra.big_operators.nat_antidiagonal

/-!
# Sums of binomial coefficients

This file includes variants of the binomial theorem and other results on sums of binomial
coefficients. Theorems whose proofs depend on such sums may also go in this file for import
reasons.

-/
open nat
open finset

open_locale big_operators

variables {R : Type*}

namespace commute

variables [semiring R] {x y : R} (h : commute x y) (n : ℕ)

include h

/-- A version of the **binomial theorem** for noncommutative semirings. -/
theorem add_pow :
  (x + y) ^ n = ∑ m in range (n + 1), x ^ m * y ^ (n - m) * choose n m :=
begin
  let t : ℕ → ℕ → R := λ n m, x ^ m * (y ^ (n - m)) * (choose n m),
  change (x + y) ^ n = ∑ m in range (n + 1), t n m,
  have h_first : ∀ n, t n 0 = y ^ n :=
    λ n, by { dsimp [t], rw [choose_zero_right, pow_zero, nat.cast_one, mul_one, one_mul] },
  have h_last : ∀ n, t n n.succ = 0 :=
    λ n, by { dsimp [t], rw [choose_succ_self, nat.cast_zero, mul_zero] },
  have h_middle : ∀ (n i : ℕ), (i ∈ range n.succ) →
   ((t n.succ) ∘ nat.succ) i = x * (t n i) + y * (t n i.succ) :=
  begin
    intros n i h_mem,
    have h_le : i ≤ n := nat.le_of_lt_succ (mem_range.mp h_mem),
    dsimp [t],
    rw [choose_succ_succ, nat.cast_add, mul_add],
    congr' 1,
    { rw [pow_succ x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc] },
    { rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq],
      by_cases h_eq : i = n,
      { rw [h_eq, choose_succ_self, nat.cast_zero, mul_zero, mul_zero] },
      { rw [succ_sub (lt_of_le_of_ne h_le h_eq)],
        rw [pow_succ y, mul_assoc, mul_assoc, mul_assoc, mul_assoc] } }
  end,
  induction n with n ih,
  { rw [pow_zero, sum_range_succ, range_zero, sum_empty, zero_add],
    dsimp [t], rw [pow_zero, pow_zero, choose_self, nat.cast_one, mul_one, mul_one] },
  { rw [sum_range_succ', h_first],
    rw [sum_congr rfl (h_middle n), sum_add_distrib, add_assoc],
    rw [pow_succ (x + y), ih, add_mul, mul_sum, mul_sum],
    congr' 1,
    rw [sum_range_succ', sum_range_succ, h_first, h_last,
       mul_zero, add_zero, pow_succ] }
end

/-- A version of `commute.add_pow` that avoids ℕ-subtraction by summing over the antidiagonal and
also with the binomial coefficient applied via scalar action of ℕ. -/
lemma add_pow' :
  (x + y) ^ n = ∑ m in nat.antidiagonal n, choose n m.fst • (x ^ m.fst * y ^ m.snd) :=
by simp_rw [finset.nat.sum_antidiagonal_eq_sum_range_succ (λ m p, choose n m • (x^m * y^p)),
  _root_.nsmul_eq_mul, cast_comm, h.add_pow]

end commute

/-- The **binomial theorem** -/
theorem add_pow [comm_semiring R] (x y : R) (n : ℕ) :
  (x + y) ^ n = ∑ m in range (n + 1), x ^ m * y ^ (n - m) * choose n m :=
(commute.all x y).add_pow n

namespace nat

/-- The sum of entries in a row of Pascal's triangle -/
theorem sum_range_choose (n : ℕ) :
  ∑ m in range (n + 1), choose n m = 2 ^ n :=
by simpa using (add_pow 1 1 n).symm

lemma sum_range_choose_halfway (m : nat) :
  ∑ i in range (m + 1), choose (2 * m + 1) i = 4 ^ m :=
have ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) =
  ∑ i in range (m + 1), choose (2 * m + 1) i,
from sum_congr rfl $ λ i hi, choose_symm $ by linarith [mem_range.1 hi],
(nat.mul_right_inj zero_lt_two).1 $
calc 2 * (∑ i in range (m + 1), choose (2 * m + 1) i) =
  (∑ i in range (m + 1), choose (2 * m + 1) i) +
    ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) :
  by rw [two_mul, this]
... = (∑ i in range (m + 1), choose (2 * m + 1) i) +
  ∑ i in Ico (m + 1) (2 * m + 2), choose (2 * m + 1) i : begin
    rw [range_eq_Ico, sum_Ico_reflect],
    { congr,
      have A : m + 1 ≤ 2 * m + 1, by linarith,
      rw [add_comm, add_tsub_assoc_of_le A, ← add_comm],
      congr,
      rw tsub_eq_iff_eq_add_of_le A,
      ring, },
   { linarith }
  end
... = ∑ i in range (2 * m + 2), choose (2 * m + 1) i : sum_range_add_sum_Ico _ (by linarith)
... = 2^(2 * m + 1) : sum_range_choose (2 * m + 1)
... = 2 * 4^m : by { rw [pow_succ, pow_mul], refl }

lemma choose_middle_le_pow (n : ℕ) : choose (2 * n + 1) n ≤ 4 ^ n :=
begin
  have t : choose (2 * n + 1) n ≤ ∑ i in range (n + 1), choose (2 * n + 1) i :=
    single_le_sum (λ x _, by linarith) (self_mem_range_succ n),
  simpa [sum_range_choose_halfway n] using t
end

lemma four_pow_le_two_mul_add_one_mul_central_binom (n : ℕ) :
  4 ^ n ≤ (2 * n + 1) * choose (2 * n) n :=
calc 4 ^ n = (1 + 1) ^ (2 * n) : by norm_num [pow_mul]
...        = ∑ m in range (2 * n + 1), choose (2 * n) m : by simp [add_pow]
...        ≤ ∑ m in range (2 * n + 1), choose (2 * n) (2 * n / 2) :
  sum_le_sum (λ i hi, choose_le_middle i (2 * n))
...        = (2 * n + 1) * choose (2 * n) n : by simp

end nat

theorem int.alternating_sum_range_choose {n : ℕ} :
  ∑ m in range (n + 1), ((-1) ^ m * ↑(choose n m) : ℤ) = if n = 0 then 1 else 0 :=
begin
  cases n, { simp },
  have h := add_pow (-1 : ℤ) 1 n.succ,
  simp only [one_pow, mul_one, add_left_neg, int.nat_cast_eq_coe_nat] at h,
  rw [← h, zero_pow (nat.succ_pos n), if_neg (nat.succ_ne_zero n)],
end

theorem int.alternating_sum_range_choose_of_ne {n : ℕ} (h0 : n ≠ 0) :
  ∑ m in range (n + 1), ((-1) ^ m * ↑(choose n m) : ℤ) = 0 :=
by rw [int.alternating_sum_range_choose, if_neg h0]

namespace finset

theorem sum_powerset_apply_card {α β : Type*} [add_comm_monoid α] (f : ℕ → α) {x : finset β} :
  ∑ m in x.powerset, f m.card = ∑ m in range (x.card + 1), (x.card.choose m) • f m :=
begin
  transitivity ∑ m in range (x.card + 1), ∑ j in x.powerset.filter (λ z, z.card = m), f j.card,
  { refine (sum_fiberwise_of_maps_to _ _).symm,
    intros y hy,
    rw [mem_range, nat.lt_succ_iff],
    rw mem_powerset at hy,
    exact card_le_of_subset hy },
  { refine sum_congr rfl (λ y hy, _),
    rw [← card_powerset_len, ← sum_const],
    refine sum_congr powerset_len_eq_filter.symm (λ z hz, _),
    rw (mem_powerset_len.1 hz).2 }
end

theorem sum_powerset_neg_one_pow_card {α : Type*} [decidable_eq α] {x : finset α} :
  ∑ m in x.powerset, (-1 : ℤ) ^ m.card = if x = ∅ then 1 else 0 :=
begin
  rw sum_powerset_apply_card,
  simp only [nsmul_eq_mul', ← card_eq_zero],
  convert int.alternating_sum_range_choose,
  ext,
  simp,
end

theorem sum_powerset_neg_one_pow_card_of_nonempty {α : Type*} {x : finset α}
  (h0 : x.nonempty) :
  ∑ m in x.powerset, (-1 : ℤ) ^ m.card = 0 :=
begin
  classical,
  rw [sum_powerset_neg_one_pow_card, if_neg],
  rw [← ne.def, ← nonempty_iff_ne_empty],
  apply h0,
end

end finset

author: jjaassoonn


text:
/-
Copyright (c) 2021 Patrick Massot. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Patrick Massot, Scott Morrison

! This file was ported from Lean 3 source module topology.algebra.field
! leanprover-community/mathlib commit f47581155c818e6361af4e4fda60d27d020c226b
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Topology.Algebra.Ring.Basic
import Mathbin.Topology.Algebra.GroupWithZero
import Mathbin.Topology.LocalExtr
import Mathbin.FieldTheory.Subfield

/-!
# Topological fields

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

A topological division ring is a topological ring whose inversion function is continuous at every
non-zero element.

-/

variable {K : Type _} [DivisionRing K] [TopologicalSpace K]

/- warning: filter.tendsto_cocompact_mul_left₀ -> Filter.tendsto_cocompact_mul_left₀ is a dubious translation:
lean 3 declaration is
  forall {K : Type.{u1}} [_inst_1 : DivisionRing.{u1} K] [_inst_2 : TopologicalSpace.{u1} K] [_inst_3 : ContinuousMul.{u1} K _inst_2 (Distrib.toHasMul.{u1} K (Ring.toDistrib.{u1} K (DivisionRing.toRing.{u1} K _inst_1)))] {a : K}, (Ne.{succ u1} K a (OfNat.ofNat.{u1} K 0 (OfNat.mk.{u1} K 0 (Zero.zero.{u1} K (MulZeroClass.toHasZero.{u1} K (NonUnitalNonAssocSemiring.toMulZeroClass.{u1} K (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} K (NonAssocRing.toNonUnitalNonAssocRing.{u1} K (Ring.toNonAssocRing.{u1} K (DivisionRing.toRing.{u1} K _inst_1)))))))))) -> (Filter.Tendsto.{u1, u1} K K (fun (x : K) => HMul.hMul.{u1, u1, u1} K K K (instHMul.{u1} K (Distrib.toHasMul.{u1} K (Ring.toDistrib.{u1} K (DivisionRing.toRing.{u1} K _inst_1)))) a x) (Filter.cocompact.{u1} K _inst_2) (Filter.cocompact.{u1} K _inst_2))
but is expected to have type
  forall {K : Type.{u1}} [_inst_1 : DivisionRing.{u1} K] [_inst_2 : TopologicalSpace.{u1} K] [_inst_3 : ContinuousMul.{u1} K _inst_2 (NonUnitalNonAssocRing.toMul.{u1} K (NonAssocRing.toNonUnitalNonAssocRing.{u1} K (Ring.toNonAssocRing.{u1} K (DivisionRing.toRing.{u1} K _inst_1))))] {a : K}, (Ne.{succ u1} K a (OfNat.ofNat.{u1} K 0 (Zero.toOfNat0.{u1} K (MonoidWithZero.toZero.{u1} K (Semiring.toMonoidWithZero.{u1} K (DivisionSemiring.toSemiring.{u1} K (DivisionRing.toDivisionSemiring.{u1} K _inst_1))))))) -> (Filter.Tendsto.{u1, u1} K K (fun (x : K) => HMul.hMul.{u1, u1, u1} K K K (instHMul.{u1} K (NonUnitalNonAssocRing.toMul.{u1} K (NonAssocRing.toNonUnitalNonAssocRing.{u1} K (Ring.toNonAssocRing.{u1} K (DivisionRing.toRing.{u1} K _inst_1))))) a x) (Filter.cocompact.{u1} K _inst_2) (Filter.cocompact.{u1} K _inst_2))
Case conversion may be inaccurate. Consider using '#align filter.tendsto_cocompact_mul_left₀ Filter.tendsto_cocompact_mul_left₀ₓ'. -/
/-- Left-multiplication by a nonzero element of a topological division ring is proper, i.e.,
inverse images of compact sets are compact. -/
theorem Filter.tendsto_cocompact_mul_left₀ [ContinuousMul K] {a : K} (ha : a ≠ 0) :
    Filter.Tendsto (fun x : K => a * x) (Filter.cocompact K) (Filter.cocompact K) :=
  Filter.tendsto_cocompact_mul_left (inv_mul_cancel ha)
#align filter.tendsto_cocompact_mul_left₀ Filter.tendsto_cocompact_mul_left₀

/- warning: filter.tendsto_cocompact_mul_right₀ -> Filter.tendsto_cocompact_mul_right₀ is a dubious translation:
lean 3 declaration is
  forall {K : Type.{u1}} [_inst_1 : DivisionRing.{u1} K] [_inst_2 : TopologicalSpace.{u1} K] [_inst_3 : ContinuousMul.{u1} K _inst_2 (Distrib.toHasMul.{u1} K (Ring.toDistrib.{u1} K (DivisionRing.toRing.{u1} K _inst_1)))] {a : K}, (Ne.{succ u1} K a (OfNat.ofNat.{u1} K 0 (OfNat.mk.{u1} K 0 (Zero.zero.{u1} K (MulZeroClass.toHasZero.{u1} K (NonUnitalNonAssocSemiring.toMulZeroClass.{u1} K (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} K (NonAssocRing.toNonUnitalNonAssocRing.{u1} K (Ring.toNonAssocRing.{u1} K (DivisionRing.toRing.{u1} K _inst_1)))))))))) -> (Filter.Tendsto.{u1, u1} K K (fun (x : K) => HMul.hMul.{u1, u1, u1} K K K (instHMul.{u1} K (Distrib.toHasMul.{u1} K (Ring.toDistrib.{u1} K (DivisionRing.toRing.{u1} K _inst_1)))) x a) (Filter.cocompact.{u1} K _inst_2) (Filter.cocompact.{u1} K _inst_2))
but is expected to have type
  forall {K : Type.{u1}} [_inst_1 : DivisionRing.{u1} K] [_inst_2 : TopologicalSpace.{u1} K] [_inst_3 : ContinuousMul.{u1} K _inst_2 (NonUnitalNonAssocRing.toMul.{u1} K (NonAssocRing.toNonUnitalNonAssocRing.{u1} K (Ring.toNonAssocRing.{u1} K (DivisionRing.toRing.{u1} K _inst_1))))] {a : K}, (Ne.{succ u1} K a (OfNat.ofNat.{u1} K 0 (Zero.toOfNat0.{u1} K (MonoidWithZero.toZero.{u1} K (Semiring.toMonoidWithZero.{u1} K (DivisionSemiring.toSemiring.{u1} K (DivisionRing.toDivisionSemiring.{u1} K _inst_1))))))) -> (Filter.Tendsto.{u1, u1} K K (fun (x : K) => HMul.hMul.{u1, u1, u1} K K K (instHMul.{u1} K (NonUnitalNonAssocRing.toMul.{u1} K (NonAssocRing.toNonUnitalNonAssocRing.{u1} K (Ring.toNonAssocRing.{u1} K (DivisionRing.toRing.{u1} K _inst_1))))) x a) (Filter.cocompact.{u1} K _inst_2) (Filter.cocompact.{u1} K _inst_2))
Case conversion may be inaccurate. Consider using '#align filter.tendsto_cocompact_mul_right₀ Filter.tendsto_cocompact_mul_right₀ₓ'. -/
/-- Right-multiplication by a nonzero element of a topological division ring is proper, i.e.,
inverse images of compact sets are compact. -/
theorem Filter.tendsto_cocompact_mul_right₀ [ContinuousMul K] {a : K} (ha : a ≠ 0) :
    Filter.Tendsto (fun x : K => x * a) (Filter.cocompact K) (Filter.cocompact K) :=
  Filter.tendsto_cocompact_mul_right (mul_inv_cancel ha)
#align filter.tendsto_cocompact_mul_right₀ Filter.tendsto_cocompact_mul_right₀

variable (K)

#print TopologicalDivisionRing /-
/-- A topological division ring is a division ring with a topology where all operations are
    continuous, including inversion. -/
class TopologicalDivisionRing extends TopologicalRing K, HasContinuousInv₀ K : Prop
#align topological_division_ring TopologicalDivisionRing
-/

section Subfield

variable {α : Type _} [Field α] [TopologicalSpace α] [TopologicalDivisionRing α]

#print Subfield.topologicalClosure /-
/-- The (topological-space) closure of a subfield of a topological field is
itself a subfield. -/
def Subfield.topologicalClosure (K : Subfield α) : Subfield α :=
  {
    K.toSubring.topologicalClosure with
    carrier := closure (K : Set α)
    inv_mem' := fun x hx => by
      rcases eq_or_ne x 0 with (rfl | h)
      · rwa [inv_zero]
      · rw [← inv_coe_set, ← Set.image_inv]
        exact mem_closure_image (continuous_at_inv₀ h) hx }
#align subfield.topological_closure Subfield.topologicalClosure
-/

/- warning: subfield.le_topological_closure -> Subfield.le_topologicalClosure is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} [_inst_3 : Field.{u1} α] [_inst_4 : TopologicalSpace.{u1} α] [_inst_5 : TopologicalDivisionRing.{u1} α (Field.toDivisionRing.{u1} α _inst_3) _inst_4] (s : Subfield.{u1} α _inst_3), LE.le.{u1} (Subfield.{u1} α _inst_3) (Preorder.toLE.{u1} (Subfield.{u1} α _inst_3) (PartialOrder.toPreorder.{u1} (Subfield.{u1} α _inst_3) (SetLike.partialOrder.{u1, u1} (Subfield.{u1} α _inst_3) α (Subfield.setLike.{u1} α _inst_3)))) s (Subfield.topologicalClosure.{u1} α _inst_3 _inst_4 _inst_5 s)
but is expected to have type
  forall {α : Type.{u1}} [_inst_3 : Field.{u1} α] [_inst_4 : TopologicalSpace.{u1} α] [_inst_5 : TopologicalDivisionRing.{u1} α (Field.toDivisionRing.{u1} α _inst_3) _inst_4] (s : Subfield.{u1} α _inst_3), LE.le.{u1} (Subfield.{u1} α _inst_3) (Preorder.toLE.{u1} (Subfield.{u1} α _inst_3) (PartialOrder.toPreorder.{u1} (Subfield.{u1} α _inst_3) (CompleteSemilatticeInf.toPartialOrder.{u1} (Subfield.{u1} α _inst_3) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Subfield.{u1} α _inst_3) (Subfield.instCompleteLatticeSubfield.{u1} α _inst_3))))) s (Subfield.topologicalClosure.{u1} α _inst_3 _inst_4 _inst_5 s)
Case conversion may be inaccurate. Consider using '#align subfield.le_topological_closure Subfield.le_topologicalClosureₓ'. -/
theorem Subfield.le_topologicalClosure (s : Subfield α) : s ≤ s.topologicalClosure :=
  subset_closure
#align subfield.le_topological_closure Subfield.le_topologicalClosure

/- warning: subfield.is_closed_topological_closure -> Subfield.isClosed_topologicalClosure is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} [_inst_3 : Field.{u1} α] [_inst_4 : TopologicalSpace.{u1} α] [_inst_5 : TopologicalDivisionRing.{u1} α (Field.toDivisionRing.{u1} α _inst_3) _inst_4] (s : Subfield.{u1} α _inst_3), IsClosed.{u1} α _inst_4 ((fun (a : Type.{u1}) (b : Type.{u1}) [self : HasLiftT.{succ u1, succ u1} a b] => self.0) (Subfield.{u1} α _inst_3) (Set.{u1} α) (HasLiftT.mk.{succ u1, succ u1} (Subfield.{u1} α _inst_3) (Set.{u1} α) (CoeTCₓ.coe.{succ u1, succ u1} (Subfield.{u1} α _inst_3) (Set.{u1} α) (SetLike.Set.hasCoeT.{u1, u1} (Subfield.{u1} α _inst_3) α (Subfield.setLike.{u1} α _inst_3)))) (Subfield.topologicalClosure.{u1} α _inst_3 _inst_4 _inst_5 s))
but is expected to have type
  forall {α : Type.{u1}} [_inst_3 : Field.{u1} α] [_inst_4 : TopologicalSpace.{u1} α] [_inst_5 : TopologicalDivisionRing.{u1} α (Field.toDivisionRing.{u1} α _inst_3) _inst_4] (s : Subfield.{u1} α _inst_3), IsClosed.{u1} α _inst_4 (SetLike.coe.{u1, u1} (Subfield.{u1} α _inst_3) α (Subfield.instSetLikeSubfield.{u1} α _inst_3) (Subfield.topologicalClosure.{u1} α _inst_3 _inst_4 _inst_5 s))
Case conversion may be inaccurate. Consider using '#align subfield.is_closed_topological_closure Subfield.isClosed_topologicalClosureₓ'. -/
theorem Subfield.isClosed_topologicalClosure (s : Subfield α) :
    IsClosed (s.topologicalClosure : Set α) :=
  isClosed_closure
#align subfield.is_closed_topological_closure Subfield.isClosed_topologicalClosure

/- warning: subfield.topological_closure_minimal -> Subfield.topologicalClosure_minimal is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} [_inst_3 : Field.{u1} α] [_inst_4 : TopologicalSpace.{u1} α] [_inst_5 : TopologicalDivisionRing.{u1} α (Field.toDivisionRing.{u1} α _inst_3) _inst_4] (s : Subfield.{u1} α _inst_3) {t : Subfield.{u1} α _inst_3}, (LE.le.{u1} (Subfield.{u1} α _inst_3) (Preorder.toLE.{u1} (Subfield.{u1} α _inst_3) (PartialOrder.toPreorder.{u1} (Subfield.{u1} α _inst_3) (SetLike.partialOrder.{u1, u1} (Subfield.{u1} α _inst_3) α (Subfield.setLike.{u1} α _inst_3)))) s t) -> (IsClosed.{u1} α _inst_4 ((fun (a : Type.{u1}) (b : Type.{u1}) [self : HasLiftT.{succ u1, succ u1} a b] => self.0) (Subfield.{u1} α _inst_3) (Set.{u1} α) (HasLiftT.mk.{succ u1, succ u1} (Subfield.{u1} α _inst_3) (Set.{u1} α) (CoeTCₓ.coe.{succ u1, succ u1} (Subfield.{u1} α _inst_3) (Set.{u1} α) (SetLike.Set.hasCoeT.{u1, u1} (Subfield.{u1} α _inst_3) α (Subfield.setLike.{u1} α _inst_3)))) t)) -> (LE.le.{u1} (Subfield.{u1} α _inst_3) (Preorder.toLE.{u1} (Subfield.{u1} α _inst_3) (PartialOrder.toPreorder.{u1} (Subfield.{u1} α _inst_3) (SetLike.partialOrder.{u1, u1} (Subfield.{u1} α _inst_3) α (Subfield.setLike.{u1} α _inst_3)))) (Subfield.topologicalClosure.{u1} α _inst_3 _inst_4 _inst_5 s) t)
but is expected to have type
  forall {α : Type.{u1}} [_inst_3 : Field.{u1} α] [_inst_4 : TopologicalSpace.{u1} α] [_inst_5 : TopologicalDivisionRing.{u1} α (Field.toDivisionRing.{u1} α _inst_3) _inst_4] (s : Subfield.{u1} α _inst_3) {t : Subfield.{u1} α _inst_3}, (LE.le.{u1} (Subfield.{u1} α _inst_3) (Preorder.toLE.{u1} (Subfield.{u1} α _inst_3) (PartialOrder.toPreorder.{u1} (Subfield.{u1} α _inst_3) (CompleteSemilatticeInf.toPartialOrder.{u1} (Subfield.{u1} α _inst_3) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Subfield.{u1} α _inst_3) (Subfield.instCompleteLatticeSubfield.{u1} α _inst_3))))) s t) -> (IsClosed.{u1} α _inst_4 (SetLike.coe.{u1, u1} (Subfield.{u1} α _inst_3) α (Subfield.instSetLikeSubfield.{u1} α _inst_3) t)) -> (LE.le.{u1} (Subfield.{u1} α _inst_3) (Preorder.toLE.{u1} (Subfield.{u1} α _inst_3) (PartialOrder.toPreorder.{u1} (Subfield.{u1} α _inst_3) (CompleteSemilatticeInf.toPartialOrder.{u1} (Subfield.{u1} α _inst_3) (CompleteLattice.toCompleteSemilatticeInf.{u1} (Subfield.{u1} α _inst_3) (Subfield.instCompleteLatticeSubfield.{u1} α _inst_3))))) (Subfield.topologicalClosure.{u1} α _inst_3 _inst_4 _inst_5 s) t)
Case conversion may be inaccurate. Consider using '#align subfield.topological_closure_minimal Subfield.topologicalClosure_minimalₓ'. -/
theorem Subfield.topologicalClosure_minimal (s : Subfield α) {t : Subfield α} (h : s ≤ t)
    (ht : IsClosed (t : Set α)) : s.topologicalClosure ≤ t :=
  closure_minimal h ht
#align subfield.topological_closure_minimal Subfield.topologicalClosure_minimal

end Subfield

section affineHomeomorph

/-!
This section is about affine homeomorphisms from a topological field `𝕜` to itself.
Technically it does not require `𝕜` to be a topological field, a topological ring that
happens to be a field is enough.
-/

variable {𝕜 : Type _} [Field 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜]

/- warning: affine_homeomorph -> affineHomeomorph is a dubious translation:
lean 3 declaration is
  forall {𝕜 : Type.{u1}} [_inst_3 : Field.{u1} 𝕜] [_inst_4 : TopologicalSpace.{u1} 𝕜] [_inst_5 : TopologicalRing.{u1} 𝕜 _inst_4 (NonAssocRing.toNonUnitalNonAssocRing.{u1} 𝕜 (Ring.toNonAssocRing.{u1} 𝕜 (DivisionRing.toRing.{u1} 𝕜 (Field.toDivisionRing.{u1} 𝕜 _inst_3))))] (a : 𝕜), 𝕜 -> (Ne.{succ u1} 𝕜 a (OfNat.ofNat.{u1} 𝕜 0 (OfNat.mk.{u1} 𝕜 0 (Zero.zero.{u1} 𝕜 (MulZeroClass.toHasZero.{u1} 𝕜 (NonUnitalNonAssocSemiring.toMulZeroClass.{u1} 𝕜 (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} 𝕜 (NonAssocRing.toNonUnitalNonAssocRing.{u1} 𝕜 (Ring.toNonAssocRing.{u1} 𝕜 (DivisionRing.toRing.{u1} 𝕜 (Field.toDivisionRing.{u1} 𝕜 _inst_3))))))))))) -> (Homeomorph.{u1, u1} 𝕜 𝕜 _inst_4 _inst_4)
but is expected to have type
  forall {𝕜 : Type.{u1}} [_inst_3 : Field.{u1} 𝕜] [_inst_4 : TopologicalSpace.{u1} 𝕜] [_inst_5 : TopologicalRing.{u1} 𝕜 _inst_4 (NonAssocRing.toNonUnitalNonAssocRing.{u1} 𝕜 (Ring.toNonAssocRing.{u1} 𝕜 (DivisionRing.toRing.{u1} 𝕜 (Field.toDivisionRing.{u1} 𝕜 _inst_3))))] (a : 𝕜), 𝕜 -> (Ne.{succ u1} 𝕜 a (OfNat.ofNat.{u1} 𝕜 0 (Zero.toOfNat0.{u1} 𝕜 (CommMonoidWithZero.toZero.{u1} 𝕜 (CommGroupWithZero.toCommMonoidWithZero.{u1} 𝕜 (Semifield.toCommGroupWithZero.{u1} 𝕜 (Field.toSemifield.{u1} 𝕜 _inst_3))))))) -> (Homeomorph.{u1, u1} 𝕜 𝕜 _inst_4 _inst_4)
Case conversion may be inaccurate. Consider using '#align affine_homeomorph affineHomeomorphₓ'. -/
/--
The map `λ x, a * x + b`, as a homeomorphism from `𝕜` (a topological field) to itself, when `a ≠ 0`.
-/
@[simps]
def affineHomeomorph (a b : 𝕜) (h : a ≠ 0) : 𝕜 ≃ₜ 𝕜
    where
  toFun x := a * x + b
  invFun y := (y - b) / a
  left_inv x := by
    simp only [add_sub_cancel]
    exact mul_div_cancel_left x h
  right_inv y := by simp [mul_div_cancel' _ h]
#align affine_homeomorph affineHomeomorph

end affineHomeomorph

section LocalExtr

variable {α β : Type _} [TopologicalSpace α] [LinearOrderedSemifield β] {a : α}

open Topology

/- warning: is_local_min.inv -> IsLocalMin.inv is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {β : Type.{u2}} [_inst_3 : TopologicalSpace.{u1} α] [_inst_4 : LinearOrderedSemifield.{u2} β] {f : α -> β} {a : α}, (IsLocalMin.{u1, u2} α β _inst_3 (PartialOrder.toPreorder.{u2} β (OrderedCancelAddCommMonoid.toPartialOrder.{u2} β (StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{u2} β (LinearOrderedSemiring.toStrictOrderedSemiring.{u2} β (LinearOrderedCommSemiring.toLinearOrderedSemiring.{u2} β (LinearOrderedSemifield.toLinearOrderedCommSemiring.{u2} β _inst_4)))))) f a) -> (Filter.Eventually.{u1} α (fun (z : α) => LT.lt.{u2} β (Preorder.toLT.{u2} β (PartialOrder.toPreorder.{u2} β (OrderedCancelAddCommMonoid.toPartialOrder.{u2} β (StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{u2} β (LinearOrderedSemiring.toStrictOrderedSemiring.{u2} β (LinearOrderedCommSemiring.toLinearOrderedSemiring.{u2} β (LinearOrderedSemifield.toLinearOrderedCommSemiring.{u2} β _inst_4))))))) (OfNat.ofNat.{u2} β 0 (OfNat.mk.{u2} β 0 (Zero.zero.{u2} β (MulZeroClass.toHasZero.{u2} β (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} β (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} β (Semiring.toNonAssocSemiring.{u2} β (DivisionSemiring.toSemiring.{u2} β (Semifield.toDivisionSemiring.{u2} β (LinearOrderedSemifield.toSemifield.{u2} β _inst_4)))))))))) (f z)) (nhds.{u1} α _inst_3 a)) -> (IsLocalMax.{u1, u2} α β _inst_3 (PartialOrder.toPreorder.{u2} β (OrderedCancelAddCommMonoid.toPartialOrder.{u2} β (StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{u2} β (LinearOrderedSemiring.toStrictOrderedSemiring.{u2} β (LinearOrderedCommSemiring.toLinearOrderedSemiring.{u2} β (LinearOrderedSemifield.toLinearOrderedCommSemiring.{u2} β _inst_4)))))) (Inv.inv.{max u1 u2} (α -> β) (Pi.instInv.{u1, u2} α (fun (ᾰ : α) => β) (fun (i : α) => DivInvMonoid.toHasInv.{u2} β (GroupWithZero.toDivInvMonoid.{u2} β (DivisionSemiring.toGroupWithZero.{u2} β (Semifield.toDivisionSemiring.{u2} β (LinearOrderedSemifield.toSemifield.{u2} β _inst_4)))))) f) a)
but is expected to have type
  forall {α : Type.{u2}} {β : Type.{u1}} [_inst_3 : TopologicalSpace.{u2} α] [_inst_4 : LinearOrderedSemifield.{u1} β] {f : α -> β} {a : α}, (IsLocalMin.{u2, u1} α β _inst_3 (PartialOrder.toPreorder.{u1} β (StrictOrderedSemiring.toPartialOrder.{u1} β (LinearOrderedSemiring.toStrictOrderedSemiring.{u1} β (LinearOrderedCommSemiring.toLinearOrderedSemiring.{u1} β (LinearOrderedSemifield.toLinearOrderedCommSemiring.{u1} β _inst_4))))) f a) -> (Filter.Eventually.{u2} α (fun (z : α) => LT.lt.{u1} β (Preorder.toLT.{u1} β (PartialOrder.toPreorder.{u1} β (StrictOrderedSemiring.toPartialOrder.{u1} β (LinearOrderedSemiring.toStrictOrderedSemiring.{u1} β (LinearOrderedCommSemiring.toLinearOrderedSemiring.{u1} β (LinearOrderedSemifield.toLinearOrderedCommSemiring.{u1} β _inst_4)))))) (OfNat.ofNat.{u1} β 0 (Zero.toOfNat0.{u1} β (CommMonoidWithZero.toZero.{u1} β (CommGroupWithZero.toCommMonoidWithZero.{u1} β (Semifield.toCommGroupWithZero.{u1} β (LinearOrderedSemifield.toSemifield.{u1} β _inst_4)))))) (f z)) (nhds.{u2} α _inst_3 a)) -> (IsLocalMax.{u2, u1} α β _inst_3 (PartialOrder.toPreorder.{u1} β (StrictOrderedSemiring.toPartialOrder.{u1} β (LinearOrderedSemiring.toStrictOrderedSemiring.{u1} β (LinearOrderedCommSemiring.toLinearOrderedSemiring.{u1} β (LinearOrderedSemifield.toLinearOrderedCommSemiring.{u1} β _inst_4))))) (Inv.inv.{max u1 u2} (α -> β) (Pi.instInv.{u2, u1} α (fun (ᾰ : α) => β) (fun (i : α) => LinearOrderedSemifield.toInv.{u1} β _inst_4)) f) a)
Case conversion may be inaccurate. Consider using '#align is_local_min.inv IsLocalMin.invₓ'. -/
theorem IsLocalMin.inv {f : α → β} {a : α} (h1 : IsLocalMin f a) (h2 : ∀ᶠ z in 𝓝 a, 0 < f z) :
    IsLocalMax f⁻¹ a := by
  filter_upwards [h1, h2]with z h3 h4 using(inv_le_inv h4 h2.self_of_nhds).mpr h3
#align is_local_min.inv IsLocalMin.inv

end LocalExtr

section Preconnected

/-! Some results about functions on preconnected sets valued in a ring or field with a topology. -/

open Set

variable {α 𝕜 : Type _} {f g : α → 𝕜} {S : Set α} [TopologicalSpace α] [TopologicalSpace 𝕜]
  [T1Space 𝕜]

/- warning: is_preconnected.eq_one_or_eq_neg_one_of_sq_eq -> IsPreconnected.eq_one_or_eq_neg_one_of_sq_eq is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {𝕜 : Type.{u2}} {f : α -> 𝕜} {S : Set.{u1} α} [_inst_3 : TopologicalSpace.{u1} α] [_inst_4 : TopologicalSpace.{u2} 𝕜] [_inst_5 : T1Space.{u2} 𝕜 _inst_4] [_inst_6 : Ring.{u2} 𝕜] [_inst_7 : NoZeroDivisors.{u2} 𝕜 (Distrib.toHasMul.{u2} 𝕜 (Ring.toDistrib.{u2} 𝕜 _inst_6)) (MulZeroClass.toHasZero.{u2} 𝕜 (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} 𝕜 (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} 𝕜 (NonAssocRing.toNonUnitalNonAssocRing.{u2} 𝕜 (Ring.toNonAssocRing.{u2} 𝕜 _inst_6)))))], (IsPreconnected.{u1} α _inst_3 S) -> (ContinuousOn.{u1, u2} α 𝕜 _inst_3 _inst_4 f S) -> (Set.EqOn.{u1, u2} α 𝕜 (HPow.hPow.{max u1 u2, 0, max u1 u2} (α -> 𝕜) Nat (α -> 𝕜) (instHPow.{max u1 u2, 0} (α -> 𝕜) Nat (Pi.hasPow.{u1, u2, 0} α Nat (fun (ᾰ : α) => 𝕜) (fun (i : α) => Monoid.Pow.{u2} 𝕜 (Ring.toMonoid.{u2} 𝕜 _inst_6)))) f (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (OfNat.ofNat.{max u1 u2} (α -> 𝕜) 1 (OfNat.mk.{max u1 u2} (α -> 𝕜) 1 (One.one.{max u1 u2} (α -> 𝕜) (Pi.instOne.{u1, u2} α (fun (ᾰ : α) => 𝕜) (fun (i : α) => AddMonoidWithOne.toOne.{u2} 𝕜 (AddGroupWithOne.toAddMonoidWithOne.{u2} 𝕜 (AddCommGroupWithOne.toAddGroupWithOne.{u2} 𝕜 (Ring.toAddCommGroupWithOne.{u2} 𝕜 _inst_6)))))))) S) -> (Or (Set.EqOn.{u1, u2} α 𝕜 f (OfNat.ofNat.{max u1 u2} (α -> 𝕜) 1 (OfNat.mk.{max u1 u2} (α -> 𝕜) 1 (One.one.{max u1 u2} (α -> 𝕜) (Pi.instOne.{u1, u2} α (fun (ᾰ : α) => 𝕜) (fun (i : α) => AddMonoidWithOne.toOne.{u2} 𝕜 (AddGroupWithOne.toAddMonoidWithOne.{u2} 𝕜 (AddCommGroupWithOne.toAddGroupWithOne.{u2} 𝕜 (Ring.toAddCommGroupWithOne.{u2} 𝕜 _inst_6)))))))) S) (Set.EqOn.{u1, u2} α 𝕜 f (Neg.neg.{max u1 u2} (α -> 𝕜) (Pi.instNeg.{u1, u2} α (fun (ᾰ : α) => 𝕜) (fun (i : α) => SubNegMonoid.toHasNeg.{u2} 𝕜 (AddGroup.toSubNegMonoid.{u2} 𝕜 (AddGroupWithOne.toAddGroup.{u2} 𝕜 (AddCommGroupWithOne.toAddGroupWithOne.{u2} 𝕜 (Ring.toAddCommGroupWithOne.{u2} 𝕜 _inst_6)))))) (OfNat.ofNat.{max u1 u2} (α -> 𝕜) 1 (OfNat.mk.{max u1 u2} (α -> 𝕜) 1 (One.one.{max u1 u2} (α -> 𝕜) (Pi.instOne.{u1, u2} α (fun (ᾰ : α) => 𝕜) (fun (i : α) => AddMonoidWithOne.toOne.{u2} 𝕜 (AddGroupWithOne.toAddMonoidWithOne.{u2} 𝕜 (AddCommGroupWithOne.toAddGroupWithOne.{u2} 𝕜 (Ring.toAddCommGroupWithOne.{u2} 𝕜 _inst_6))))))))) S))
but is expected to have type
  forall {α : Type.{u1}} {𝕜 : Type.{u2}} {f : α -> 𝕜} {S : Set.{u1} α} [_inst_3 : TopologicalSpace.{u1} α] [_inst_4 : TopologicalSpace.{u2} 𝕜] [_inst_5 : T1Space.{u2} 𝕜 _inst_4] [_inst_6 : Ring.{u2} 𝕜] [_inst_7 : NoZeroDivisors.{u2} 𝕜 (NonUnitalNonAssocRing.toMul.{u2} 𝕜 (NonAssocRing.toNonUnitalNonAssocRing.{u2} 𝕜 (Ring.toNonAssocRing.{u2} 𝕜 _inst_6))) (MonoidWithZero.toZero.{u2} 𝕜 (Semiring.toMonoidWithZero.{u2} 𝕜 (Ring.toSemiring.{u2} 𝕜 _inst_6)))], (IsPreconnected.{u1} α _inst_3 S) -> (ContinuousOn.{u1, u2} α 𝕜 _inst_3 _inst_4 f S) -> (Set.EqOn.{u1, u2} α 𝕜 (HPow.hPow.{max u1 u2, 0, max u2 u1} (α -> 𝕜) Nat (α -> 𝕜) (instHPow.{max u1 u2, 0} (α -> 𝕜) Nat (Monoid.Pow.{max u1 u2} (α -> 𝕜) (Pi.monoid.{u1, u2} α (fun (a._@.Mathlib.Topology.Algebra.Field._hyg.738 : α) => 𝕜) (fun (i : α) => MonoidWithZero.toMonoid.{u2} 𝕜 (Semiring.toMonoidWithZero.{u2} 𝕜 (Ring.toSemiring.{u2} 𝕜 _inst_6)))))) f (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (OfNat.ofNat.{max u2 u1} (α -> 𝕜) 1 (One.toOfNat1.{max u1 u2} (α -> 𝕜) (Pi.instOne.{u1, u2} α (fun (a._@.Mathlib.Data.Set.Function._hyg.1349 : α) => 𝕜) (fun (i : α) => NonAssocRing.toOne.{u2} 𝕜 (Ring.toNonAssocRing.{u2} 𝕜 _inst_6))))) S) -> (Or (Set.EqOn.{u1, u2} α 𝕜 f (OfNat.ofNat.{max u1 u2} (α -> 𝕜) 1 (One.toOfNat1.{max u1 u2} (α -> 𝕜) (Pi.instOne.{u1, u2} α (fun (a._@.Mathlib.Data.Set.Function._hyg.1349 : α) => 𝕜) (fun (i : α) => NonAssocRing.toOne.{u2} 𝕜 (Ring.toNonAssocRing.{u2} 𝕜 _inst_6))))) S) (Set.EqOn.{u1, u2} α 𝕜 f (Neg.neg.{max u1 u2} (α -> 𝕜) (Pi.instNeg.{u1, u2} α (fun (ᾰ : α) => 𝕜) (fun (i : α) => Ring.toNeg.{u2} 𝕜 _inst_6)) (OfNat.ofNat.{max u1 u2} (α -> 𝕜) 1 (One.toOfNat1.{max u1 u2} (α -> 𝕜) (Pi.instOne.{u1, u2} α (fun (a._@.Mathlib.Data.Set.Function._hyg.1349 : α) => 𝕜) (fun (i : α) => NonAssocRing.toOne.{u2} 𝕜 (Ring.toNonAssocRing.{u2} 𝕜 _inst_6)))))) S))
Case conversion may be inaccurate. Consider using '#align is_preconnected.eq_one_or_eq_neg_one_of_sq_eq IsPreconnected.eq_one_or_eq_neg_one_of_sq_eqₓ'. -/
/-- If `f` is a function `α → 𝕜` which is continuous on a preconnected set `S`, and
`f ^ 2 = 1` on `S`, then either `f = 1` on `S`, or `f = -1` on `S`. -/
theorem IsPreconnected.eq_one_or_eq_neg_one_of_sq_eq [Ring 𝕜] [NoZeroDivisors 𝕜]
    (hS : IsPreconnected S) (hf : ContinuousOn f S) (hsq : EqOn (f ^ 2) 1 S) :
    EqOn f 1 S ∨ EqOn f (-1) S :=
  by
  simp_rw [eq_on, Pi.one_apply, Pi.pow_apply, sq_eq_one_iff] at hsq
  -- First deal with crazy case where `S` is empty.
  by_cases hSe : ∀ x : α, x ∉ S
  · left
    intro x hx
    exfalso
    exact hSe x hx
  push_neg  at hSe
  choose y hy using hSe
  suffices ∀ x : α, x ∈ S → f x = f y by
    rcases hsq hy with ⟨⟩
    · left
      intro z hz
      rw [Pi.one_apply z, ← h]
      exact this z hz
    · right
      intro z hz
      rw [Pi.neg_apply, Pi.one_apply, ← h]
      exact this z hz
  refine' fun x hx => hS.constant_of_maps_to hf (fun z hz => _) hx hy
  show f z ∈ ({-1, 1} : Set 𝕜)
  · exact mem_insert_iff.mpr (hsq hz).symm
  exact discrete_of_t1_of_finite
#align is_preconnected.eq_one_or_eq_neg_one_of_sq_eq IsPreconnected.eq_one_or_eq_neg_one_of_sq_eq

/- warning: is_preconnected.eq_or_eq_neg_of_sq_eq -> IsPreconnected.eq_or_eq_neg_of_sq_eq is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {𝕜 : Type.{u2}} {f : α -> 𝕜} {g : α -> 𝕜} {S : Set.{u1} α} [_inst_3 : TopologicalSpace.{u1} α] [_inst_4 : TopologicalSpace.{u2} 𝕜] [_inst_5 : T1Space.{u2} 𝕜 _inst_4] [_inst_6 : Field.{u2} 𝕜] [_inst_7 : HasContinuousInv₀.{u2} 𝕜 (MulZeroClass.toHasZero.{u2} 𝕜 (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} 𝕜 (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} 𝕜 (NonAssocRing.toNonUnitalNonAssocRing.{u2} 𝕜 (Ring.toNonAssocRing.{u2} 𝕜 (DivisionRing.toRing.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6))))))) (DivInvMonoid.toHasInv.{u2} 𝕜 (DivisionRing.toDivInvMonoid.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6))) _inst_4] [_inst_8 : ContinuousMul.{u2} 𝕜 _inst_4 (Distrib.toHasMul.{u2} 𝕜 (Ring.toDistrib.{u2} 𝕜 (DivisionRing.toRing.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6))))], (IsPreconnected.{u1} α _inst_3 S) -> (ContinuousOn.{u1, u2} α 𝕜 _inst_3 _inst_4 f S) -> (ContinuousOn.{u1, u2} α 𝕜 _inst_3 _inst_4 g S) -> (Set.EqOn.{u1, u2} α 𝕜 (HPow.hPow.{max u1 u2, 0, max u1 u2} (α -> 𝕜) Nat (α -> 𝕜) (instHPow.{max u1 u2, 0} (α -> 𝕜) Nat (Pi.hasPow.{u1, u2, 0} α Nat (fun (ᾰ : α) => 𝕜) (fun (i : α) => Monoid.Pow.{u2} 𝕜 (Ring.toMonoid.{u2} 𝕜 (DivisionRing.toRing.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6)))))) f (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (HPow.hPow.{max u1 u2, 0, max u1 u2} (α -> 𝕜) Nat (α -> 𝕜) (instHPow.{max u1 u2, 0} (α -> 𝕜) Nat (Pi.hasPow.{u1, u2, 0} α Nat (fun (ᾰ : α) => 𝕜) (fun (i : α) => Monoid.Pow.{u2} 𝕜 (Ring.toMonoid.{u2} 𝕜 (DivisionRing.toRing.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6)))))) g (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) S) -> (forall {x : α}, (Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) x S) -> (Ne.{succ u2} 𝕜 (g x) (OfNat.ofNat.{u2} 𝕜 0 (OfNat.mk.{u2} 𝕜 0 (Zero.zero.{u2} 𝕜 (MulZeroClass.toHasZero.{u2} 𝕜 (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} 𝕜 (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} 𝕜 (NonAssocRing.toNonUnitalNonAssocRing.{u2} 𝕜 (Ring.toNonAssocRing.{u2} 𝕜 (DivisionRing.toRing.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6)))))))))))) -> (Or (Set.EqOn.{u1, u2} α 𝕜 f g S) (Set.EqOn.{u1, u2} α 𝕜 f (Neg.neg.{max u1 u2} (α -> 𝕜) (Pi.instNeg.{u1, u2} α (fun (ᾰ : α) => 𝕜) (fun (i : α) => SubNegMonoid.toHasNeg.{u2} 𝕜 (AddGroup.toSubNegMonoid.{u2} 𝕜 (AddGroupWithOne.toAddGroup.{u2} 𝕜 (AddCommGroupWithOne.toAddGroupWithOne.{u2} 𝕜 (Ring.toAddCommGroupWithOne.{u2} 𝕜 (DivisionRing.toRing.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6)))))))) g) S))
but is expected to have type
  forall {α : Type.{u1}} {𝕜 : Type.{u2}} {f : α -> 𝕜} {g : α -> 𝕜} {S : Set.{u1} α} [_inst_3 : TopologicalSpace.{u1} α] [_inst_4 : TopologicalSpace.{u2} 𝕜] [_inst_5 : T1Space.{u2} 𝕜 _inst_4] [_inst_6 : Field.{u2} 𝕜] [_inst_7 : HasContinuousInv₀.{u2} 𝕜 (CommMonoidWithZero.toZero.{u2} 𝕜 (CommGroupWithZero.toCommMonoidWithZero.{u2} 𝕜 (Semifield.toCommGroupWithZero.{u2} 𝕜 (Field.toSemifield.{u2} 𝕜 _inst_6)))) (Field.toInv.{u2} 𝕜 _inst_6) _inst_4] [_inst_8 : ContinuousMul.{u2} 𝕜 _inst_4 (NonUnitalNonAssocRing.toMul.{u2} 𝕜 (NonAssocRing.toNonUnitalNonAssocRing.{u2} 𝕜 (Ring.toNonAssocRing.{u2} 𝕜 (DivisionRing.toRing.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6)))))], (IsPreconnected.{u1} α _inst_3 S) -> (ContinuousOn.{u1, u2} α 𝕜 _inst_3 _inst_4 f S) -> (ContinuousOn.{u1, u2} α 𝕜 _inst_3 _inst_4 g S) -> (Set.EqOn.{u1, u2} α 𝕜 (HPow.hPow.{max u1 u2, 0, max u2 u1} (α -> 𝕜) Nat (α -> 𝕜) (instHPow.{max u1 u2, 0} (α -> 𝕜) Nat (Monoid.Pow.{max u1 u2} (α -> 𝕜) (Pi.monoid.{u1, u2} α (fun (a._@.Mathlib.Topology.Algebra.Field._hyg.872 : α) => 𝕜) (fun (i : α) => MonoidWithZero.toMonoid.{u2} 𝕜 (Semiring.toMonoidWithZero.{u2} 𝕜 (DivisionSemiring.toSemiring.{u2} 𝕜 (Semifield.toDivisionSemiring.{u2} 𝕜 (Field.toSemifield.{u2} 𝕜 _inst_6)))))))) f (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (HPow.hPow.{max u1 u2, 0, max u2 u1} (α -> 𝕜) Nat (α -> 𝕜) (instHPow.{max u1 u2, 0} (α -> 𝕜) Nat (Monoid.Pow.{max u1 u2} (α -> 𝕜) (Pi.monoid.{u1, u2} α (fun (a._@.Mathlib.Topology.Algebra.Field._hyg.872 : α) => 𝕜) (fun (i : α) => MonoidWithZero.toMonoid.{u2} 𝕜 (Semiring.toMonoidWithZero.{u2} 𝕜 (DivisionSemiring.toSemiring.{u2} 𝕜 (Semifield.toDivisionSemiring.{u2} 𝕜 (Field.toSemifield.{u2} 𝕜 _inst_6)))))))) g (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) S) -> (forall {x : α}, (Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x S) -> (Ne.{succ u2} 𝕜 (g x) (OfNat.ofNat.{u2} 𝕜 0 (Zero.toOfNat0.{u2} 𝕜 (CommMonoidWithZero.toZero.{u2} 𝕜 (CommGroupWithZero.toCommMonoidWithZero.{u2} 𝕜 (Semifield.toCommGroupWithZero.{u2} 𝕜 (Field.toSemifield.{u2} 𝕜 _inst_6)))))))) -> (Or (Set.EqOn.{u1, u2} α 𝕜 f g S) (Set.EqOn.{u1, u2} α 𝕜 f (Neg.neg.{max u1 u2} (α -> 𝕜) (Pi.instNeg.{u1, u2} α (fun (ᾰ : α) => 𝕜) (fun (i : α) => Ring.toNeg.{u2} 𝕜 (DivisionRing.toRing.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6)))) g) S))
Case conversion may be inaccurate. Consider using '#align is_preconnected.eq_or_eq_neg_of_sq_eq IsPreconnected.eq_or_eq_neg_of_sq_eqₓ'. -/
/-- If `f, g` are functions `α → 𝕜`, both continuous on a preconnected set `S`, with
`f ^ 2 = g ^ 2` on `S`, and `g z ≠ 0` all `z ∈ S`, then either `f = g` or `f = -g` on
`S`. -/
theorem IsPreconnected.eq_or_eq_neg_of_sq_eq [Field 𝕜] [HasContinuousInv₀ 𝕜] [ContinuousMul 𝕜]
    (hS : IsPreconnected S) (hf : ContinuousOn f S) (hg : ContinuousOn g S)
    (hsq : EqOn (f ^ 2) (g ^ 2) S) (hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0) :
    EqOn f g S ∨ EqOn f (-g) S :=
  by
  rcases hS.eq_one_or_eq_neg_one_of_sq_eq (hf.div hg fun z hz => hg_ne hz) fun x hx => _ with
    (h | h)
  · refine' Or.inl fun x hx => _
    rw [← div_eq_one_iff_eq (hg_ne hx)]
    exact h hx
  · refine' Or.inr fun x hx => _
    specialize h hx
    rwa [Pi.div_apply, Pi.neg_apply, Pi.one_apply, div_eq_iff (hg_ne hx), neg_one_mul] at h
  · rw [Pi.one_apply, div_pow, Pi.div_apply, hsq hx, div_self]
    exact pow_ne_zero _ (hg_ne hx)
#align is_preconnected.eq_or_eq_neg_of_sq_eq IsPreconnected.eq_or_eq_neg_of_sq_eq

/- warning: is_preconnected.eq_of_sq_eq -> IsPreconnected.eq_of_sq_eq is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {𝕜 : Type.{u2}} {f : α -> 𝕜} {g : α -> 𝕜} {S : Set.{u1} α} [_inst_3 : TopologicalSpace.{u1} α] [_inst_4 : TopologicalSpace.{u2} 𝕜] [_inst_5 : T1Space.{u2} 𝕜 _inst_4] [_inst_6 : Field.{u2} 𝕜] [_inst_7 : HasContinuousInv₀.{u2} 𝕜 (MulZeroClass.toHasZero.{u2} 𝕜 (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} 𝕜 (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} 𝕜 (NonAssocRing.toNonUnitalNonAssocRing.{u2} 𝕜 (Ring.toNonAssocRing.{u2} 𝕜 (DivisionRing.toRing.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6))))))) (DivInvMonoid.toHasInv.{u2} 𝕜 (DivisionRing.toDivInvMonoid.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6))) _inst_4] [_inst_8 : ContinuousMul.{u2} 𝕜 _inst_4 (Distrib.toHasMul.{u2} 𝕜 (Ring.toDistrib.{u2} 𝕜 (DivisionRing.toRing.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6))))], (IsPreconnected.{u1} α _inst_3 S) -> (ContinuousOn.{u1, u2} α 𝕜 _inst_3 _inst_4 f S) -> (ContinuousOn.{u1, u2} α 𝕜 _inst_3 _inst_4 g S) -> (Set.EqOn.{u1, u2} α 𝕜 (HPow.hPow.{max u1 u2, 0, max u1 u2} (α -> 𝕜) Nat (α -> 𝕜) (instHPow.{max u1 u2, 0} (α -> 𝕜) Nat (Pi.hasPow.{u1, u2, 0} α Nat (fun (ᾰ : α) => 𝕜) (fun (i : α) => Monoid.Pow.{u2} 𝕜 (Ring.toMonoid.{u2} 𝕜 (DivisionRing.toRing.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6)))))) f (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (HPow.hPow.{max u1 u2, 0, max u1 u2} (α -> 𝕜) Nat (α -> 𝕜) (instHPow.{max u1 u2, 0} (α -> 𝕜) Nat (Pi.hasPow.{u1, u2, 0} α Nat (fun (ᾰ : α) => 𝕜) (fun (i : α) => Monoid.Pow.{u2} 𝕜 (Ring.toMonoid.{u2} 𝕜 (DivisionRing.toRing.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6)))))) g (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) S) -> (forall {x : α}, (Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) x S) -> (Ne.{succ u2} 𝕜 (g x) (OfNat.ofNat.{u2} 𝕜 0 (OfNat.mk.{u2} 𝕜 0 (Zero.zero.{u2} 𝕜 (MulZeroClass.toHasZero.{u2} 𝕜 (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} 𝕜 (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} 𝕜 (NonAssocRing.toNonUnitalNonAssocRing.{u2} 𝕜 (Ring.toNonAssocRing.{u2} 𝕜 (DivisionRing.toRing.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6)))))))))))) -> (forall {y : α}, (Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) y S) -> (Eq.{succ u2} 𝕜 (f y) (g y)) -> (Set.EqOn.{u1, u2} α 𝕜 f g S))
but is expected to have type
  forall {α : Type.{u1}} {𝕜 : Type.{u2}} {f : α -> 𝕜} {g : α -> 𝕜} {S : Set.{u1} α} [_inst_3 : TopologicalSpace.{u1} α] [_inst_4 : TopologicalSpace.{u2} 𝕜] [_inst_5 : T1Space.{u2} 𝕜 _inst_4] [_inst_6 : Field.{u2} 𝕜] [_inst_7 : HasContinuousInv₀.{u2} 𝕜 (CommMonoidWithZero.toZero.{u2} 𝕜 (CommGroupWithZero.toCommMonoidWithZero.{u2} 𝕜 (Semifield.toCommGroupWithZero.{u2} 𝕜 (Field.toSemifield.{u2} 𝕜 _inst_6)))) (Field.toInv.{u2} 𝕜 _inst_6) _inst_4] [_inst_8 : ContinuousMul.{u2} 𝕜 _inst_4 (NonUnitalNonAssocRing.toMul.{u2} 𝕜 (NonAssocRing.toNonUnitalNonAssocRing.{u2} 𝕜 (Ring.toNonAssocRing.{u2} 𝕜 (DivisionRing.toRing.{u2} 𝕜 (Field.toDivisionRing.{u2} 𝕜 _inst_6)))))], (IsPreconnected.{u1} α _inst_3 S) -> (ContinuousOn.{u1, u2} α 𝕜 _inst_3 _inst_4 f S) -> (ContinuousOn.{u1, u2} α 𝕜 _inst_3 _inst_4 g S) -> (Set.EqOn.{u1, u2} α 𝕜 (HPow.hPow.{max u1 u2, 0, max u2 u1} (α -> 𝕜) Nat (α -> 𝕜) (instHPow.{max u1 u2, 0} (α -> 𝕜) Nat (Monoid.Pow.{max u1 u2} (α -> 𝕜) (Pi.monoid.{u1, u2} α (fun (a._@.Mathlib.Topology.Algebra.Field._hyg.1060 : α) => 𝕜) (fun (i : α) => MonoidWithZero.toMonoid.{u2} 𝕜 (Semiring.toMonoidWithZero.{u2} 𝕜 (DivisionSemiring.toSemiring.{u2} 𝕜 (Semifield.toDivisionSemiring.{u2} 𝕜 (Field.toSemifield.{u2} 𝕜 _inst_6)))))))) f (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (HPow.hPow.{max u1 u2, 0, max u2 u1} (α -> 𝕜) Nat (α -> 𝕜) (instHPow.{max u1 u2, 0} (α -> 𝕜) Nat (Monoid.Pow.{max u1 u2} (α -> 𝕜) (Pi.monoid.{u1, u2} α (fun (a._@.Mathlib.Topology.Algebra.Field._hyg.1060 : α) => 𝕜) (fun (i : α) => MonoidWithZero.toMonoid.{u2} 𝕜 (Semiring.toMonoidWithZero.{u2} 𝕜 (DivisionSemiring.toSemiring.{u2} 𝕜 (Semifield.toDivisionSemiring.{u2} 𝕜 (Field.toSemifield.{u2} 𝕜 _inst_6)))))))) g (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) S) -> (forall {x : α}, (Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x S) -> (Ne.{succ u2} 𝕜 (g x) (OfNat.ofNat.{u2} 𝕜 0 (Zero.toOfNat0.{u2} 𝕜 (CommMonoidWithZero.toZero.{u2} 𝕜 (CommGroupWithZero.toCommMonoidWithZero.{u2} 𝕜 (Semifield.toCommGroupWithZero.{u2} 𝕜 (Field.toSemifield.{u2} 𝕜 _inst_6)))))))) -> (forall {y : α}, (Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) y S) -> (Eq.{succ u2} 𝕜 (f y) (g y)) -> (Set.EqOn.{u1, u2} α 𝕜 f g S))
Case conversion may be inaccurate. Consider using '#align is_preconnected.eq_of_sq_eq IsPreconnected.eq_of_sq_eqₓ'. -/
/-- If `f, g` are functions `α → 𝕜`, both continuous on a preconnected set `S`, with
`f ^ 2 = g ^ 2` on `S`, and `g z ≠ 0` all `z ∈ S`, then as soon as `f = g` holds at
one point of `S` it holds for all points. -/
theorem IsPreconnected.eq_of_sq_eq [Field 𝕜] [HasContinuousInv₀ 𝕜] [ContinuousMul 𝕜]
    (hS : IsPreconnected S) (hf : ContinuousOn f S) (hg : ContinuousOn g S)
    (hsq : EqOn (f ^ 2) (g ^ 2) S) (hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0) {y : α} (hy : y ∈ S)
    (hy' : f y = g y) : EqOn f g S := fun x hx =>
  by
  rcases hS.eq_or_eq_neg_of_sq_eq hf hg @hsq @hg_ne with (h | h)
  · exact h hx
  · rw [h hy, eq_comm, ← sub_eq_zero, sub_eq_add_neg, Pi.neg_apply, neg_neg, ← mul_two,
      mul_eq_zero] at hy'
    cases hy'
    -- need to handle case of `char 𝕜 = 2` separately
    · exfalso
      exact hg_ne hy hy'
    ·
      rw [h hx, Pi.neg_apply, eq_comm, ← sub_eq_zero, sub_eq_add_neg, neg_neg, ← mul_two, hy',
        MulZeroClass.mul_zero]
#align is_preconnected.eq_of_sq_eq IsPreconnected.eq_of_sq_eq

end Preconnected

author: leanprover-community


text:
import weighted_homogeneous
import algebra.direct_sum.basic
import algebra.direct_sum.ring
import algebra.direct_sum.internal

noncomputable theory

open_locale big_operators

namespace mv_polynomial
variables {σ : Type*} {τ : Type*} {R : Type*} [comm_semiring R] {S : Type*}

-- TODO : delete or replace below
/-- The degree of a monoomial -/
def degree' := weighted_degree' (1 : σ → ℕ)

lemma degree'_eq_weighted_degree' (d : σ →₀ ℕ) :
  ∑ i in d.support, d i = weighted_degree' (1 : σ → ℕ) d :=
by simp [weighted_degree', finsupp.total, finsupp.sum]

lemma unit_weight_is_non_trivial_weight : non_trivial_weight (1 : σ → ℕ) :=
  non_trivial_weight_of (λ x : σ, one_ne_zero)

/-- A multivariate polynomial `φ` is homogeneous of degree `n`
if all monomials occuring in `φ` have degree `n`. -/
def is_homogeneous (φ : mv_polynomial σ R) (n : ℕ) :=
is_weighted_homogeneous (1 : σ → ℕ) φ n

variables (σ R)

lemma total_degree_eq_weighted_total_degree (φ : mv_polynomial σ R) :
  φ.total_degree = weighted_total_degree (1 : σ → ℕ) φ :=
by simp only [total_degree, weighted_total_degree, weighted_degree',
  finsupp.total, pi.one_apply, finsupp.coe_lsum, linear_map.coe_smul_right,
  linear_map.id_coe, id.def, algebra.id.smul_eq_mul, mul_one]

/-- The submodule of homogeneous `mv_polynomial`s of degree `n`. -/
def homogeneous_submodule (n : ℕ) : submodule R (mv_polynomial σ R) :=
weighted_homogeneous_submodule R (1 : σ → ℕ) n

variables {σ R}

@[simp] lemma mem_homogeneous_submodule (n : ℕ) (p : mv_polynomial σ R) :
  p ∈ homogeneous_submodule σ R n ↔ p.is_homogeneous n := iff.rfl

variables (σ R)

/-- While equal, the former has a convenient definitional reduction. -/
lemma homogeneous_submodule_eq_finsupp_supported (n : ℕ) :
  homogeneous_submodule σ R n = finsupp.supported _ R {d | ∑ i in d.support, d i = n} :=
begin
  simp_rw degree'_eq_weighted_degree',
  exact weighted_homogeneous_submodule_eq_finsupp_supported R 1 n,
end

variables {σ R}

lemma homogeneous_submodule_mul (m n : ℕ) :
  homogeneous_submodule σ R m * homogeneous_submodule σ R n ≤ homogeneous_submodule σ R (m + n) :=
weighted_homogeneous_submodule_mul (1 : σ → ℕ) m n

section

variables {σ R}

lemma is_homogeneous_monomial [decidable_eq σ] (d : σ →₀ ℕ) (r : R) (n : ℕ) (hn : ∑ i in d.support, d i = n) :
  is_homogeneous (monomial d r) n :=
begin
  simp_rw degree'_eq_weighted_degree' at hn,
  exact is_weighted_homogeneous_monomial 1 d r hn
end

variables (σ) {R}

lemma total_degree_eq_zero_iff
  (p : mv_polynomial σ R) :
  p.total_degree = 0
  ↔ ∀ (m : σ →₀ ℕ) (hm : m ∈ p.support) (x : σ), m x = 0 :=
begin
  rw [total_degree_eq_weighted_total_degree,
    weighted_total_degree_eq_zero_iff _ p, bot_eq_zero],
  intros n x,
  simp only [pi.one_apply, algebra.id.smul_eq_mul, mul_one, imp_self],
end

  /-
begin
  rw [total_degree, ← bot_eq_zero, finset.sup_eq_bot_iff, bot_eq_zero],
  apply forall_congr, intro a,
  apply forall_congr, intro hap,
  simp only [finsupp.sum, finset.sum_eq_zero_iff, finsupp.mem_support_iff],
  apply forall_congr,
  intro x,
  simp only [not_imp_self],
end
 -/

lemma is_homogeneous_of_total_degree_zero_iff {p : mv_polynomial σ R} :
  p.total_degree = 0 ↔ is_homogeneous p 0 :=
by rw [total_degree_eq_weighted_total_degree,
  is_weighted_homogeneous_of_total_weighted_degree_zero_iff, is_homogeneous]

lemma is_homogeneous_of_total_degree_zero {p : mv_polynomial σ R}
  (hp : p.total_degree = 0) : is_homogeneous p 0  := (is_homogeneous_of_total_degree_zero_iff σ).mp hp

lemma is_homogeneous_C [decidable_eq σ] (r : R) :
  is_homogeneous (C r : mv_polynomial σ R) 0 :=
is_weighted_homogeneous_C (1 : σ → ℕ) r

variables (σ R)

lemma is_homogeneous_zero [decidable_eq σ] (n : ℕ) : is_homogeneous (0 : mv_polynomial σ R) n :=
is_weighted_homogeneous_zero R (1 : σ → ℕ) n

lemma is_homogeneous_one [decidable_eq σ] : is_homogeneous (1 : mv_polynomial σ R) 0 :=
is_weighted_homogeneous_one R (1 : σ → ℕ)

variables {σ} (R)

lemma is_homogeneous_X [decidable_eq σ] (i : σ) :
  is_homogeneous (X i : mv_polynomial σ R) 1 :=
is_weighted_homogeneous_X R (1 : σ → ℕ) i

end

namespace is_homogeneous
variables {φ ψ : mv_polynomial σ R} {m n : ℕ}

lemma coeff_eq_zero (hφ : is_homogeneous φ n) (d : σ →₀ ℕ) (hd : ∑ i in d.support, d i ≠ n) :
  coeff d φ = 0 :=
by simp_rw degree'_eq_weighted_degree' at hd; exact is_weighted_homogeneous.coeff_eq_zero hφ d hd

lemma inj_right (hm : is_homogeneous φ m) (hn : is_homogeneous φ n) (hφ : φ ≠ 0) :
  m = n :=
is_weighted_homogeneous.inj_right hφ hm hn

lemma add (hφ : is_homogeneous φ n) (hψ : is_homogeneous ψ n) :
  is_homogeneous (φ + ψ) n :=
is_weighted_homogeneous.add hφ hψ

lemma sum {ι : Type*} (s : finset ι) (φ : ι → mv_polynomial σ R) (n : ℕ)
  (h : ∀ i ∈ s, is_homogeneous (φ i) n) :
  is_homogeneous (∑ i in s, φ i) n :=
is_weighted_homogeneous.sum s φ n h

lemma mul (hφ : is_homogeneous φ m) (hψ : is_homogeneous ψ n) :
  is_homogeneous (φ * ψ) (m + n) :=
is_weighted_homogeneous.mul hφ hψ

lemma prod [decidable_eq σ] {ι : Type*} [decidable_eq ι] (s : finset ι) (φ : ι → mv_polynomial σ R) (n : ι → ℕ)
  (h : ∀ i ∈ s, is_homogeneous (φ i) (n i)) :
  is_homogeneous (∏ i in s, φ i) (∑ i in s, n i) :=
is_weighted_homogeneous.prod s φ n h

lemma total_degree_eq_weighted_total_degree :
  total_degree φ = weighted_total_degree (1 : σ → ℕ) φ :=
begin
  rw [total_degree, weighted_total_degree, weighted_degree'],
  apply finset.sup_congr rfl,
  intros a ha,
  simp only [finsupp.total, pi.one_apply, linear_map.to_add_monoid_hom_coe, finsupp.coe_lsum, linear_map.coe_smul_right,
  linear_map.id_coe, id.def, algebra.id.smul_eq_mul, mul_one],
end

lemma total_degree (hφ : is_homogeneous φ n) (h : φ ≠ 0) :
  total_degree φ = n :=
by rw [total_degree_eq_weighted_total_degree, ← with_bot.coe_eq_coe,
    ← weighted_total_degree_coe _ φ h,
    is_weighted_homogeneous.weighted_total_degree hφ h]

/-- The homogeneous submodules form a graded ring.
This instance is used by `direct_sum.comm_semiring` and `direct_sum.algebra`. -/
instance homogeneous_submodule.gcomm_monoid [decidable_eq σ] :
  set_like.graded_monoid (homogeneous_submodule σ R) :=
is_weighted_homogeneous.weighted_homogeneous_submodule.gcomm_monoid

open_locale direct_sum

/-
noncomputable example :
  direct_sum.gcomm_semiring [decidable_eq σ] (λ i, homogeneous_submodule σ R i) :=
begin
-- apply direct_sum.comm_semiring ,
  haveI : set_like.graded_monoid (λ (i : ℕ), homogeneous_submodule σ R i),
  apply is_weighted_homogeneous.weighted_homogeneous_submodule.gcomm_monoid,
apply set_like.gcomm_semiring,
sorry,
end
-/

--noncomputable example : algebra R (⨁ i, homogeneous_submodule σ R i) := sorry --infer_instance

end is_homogeneous

section
noncomputable theory
-- open_locale classical
open finset

variable (R)
/-- `homogeneous_component n φ` is the part of `φ` that is homogeneous of degree `n`.
See `sum_homogeneous_component` for the statement that `φ` is equal to the sum
of all its homogeneous components. -/
def homogeneous_component (n : ℕ) :
  mv_polynomial σ R →ₗ[R] mv_polynomial σ R :=
weighted_homogeneous_component R (1 : σ → ℕ) n

variable {R}

lemma homogeneous_component_mem
  (φ : mv_polynomial σ R) (i : ℕ) :
  homogeneous_component R i φ ∈ homogeneous_submodule σ R i :=
weighted_homogeneous_component_mem _ φ i

section homogeneous_component

open finset
variables (n : ℕ) (φ ψ : mv_polynomial σ R)

lemma coeff_homogeneous_component (d : σ →₀ ℕ) :
  coeff d (homogeneous_component R n φ) = if ∑ i in d.support, d i = n then coeff d φ else 0 :=
begin
  simp_rw degree'_eq_weighted_degree',
  convert coeff_weighted_homogeneous_component n φ d,
end

lemma homogeneous_component_apply :
  homogeneous_component R n φ =
  ∑ d in φ.support.filter (λ d, ∑ i in d.support, d i = n), monomial d (coeff d φ) :=
begin
  simp_rw degree'_eq_weighted_degree',
  convert weighted_homogeneous_component_apply n φ,
end

lemma homogeneous_component_is_homogeneous :
  (homogeneous_component R n φ).is_homogeneous n :=
weighted_homogeneous_component_is_weighted_homogeneous n φ

@[simp]
lemma homogeneous_component_zero [decidable_eq σ] :
  homogeneous_component R 0 φ = C (coeff 0 φ) :=
weighted_homogeneous_component_zero φ unit_weight_is_non_trivial_weight

@[simp]
lemma homogeneous_component_C_mul (n : ℕ) (r : R) :
  homogeneous_component R n (C r * φ) = C r * homogeneous_component R n φ :=
weighted_homogeneous_component_C_mul φ n r

lemma homogeneous_component_eq_zero' (h : ∀ d : σ →₀ ℕ, d ∈ φ.support → ∑ i in d.support, d i ≠ n) :
  homogeneous_component R n φ = 0 :=
begin
  simp_rw degree'_eq_weighted_degree' at h,
  exact weighted_homogeneous_component_eq_zero' n φ h,
end

--TODO: change proof when `weighted_total_degree` exists.
lemma homogeneous_component_eq_zero (h : φ.total_degree < n) :
  homogeneous_component R n φ = 0 :=
begin
  apply homogeneous_component_eq_zero',
  rw [total_degree, finset.sup_lt_iff] at h,
  { intros d hd, exact ne_of_lt (h d hd), },
  { exact lt_of_le_of_lt (nat.zero_le _) h, }
end

--TODO: change proof when `weighted_total_degree` exists.
lemma sum_homogeneous_component :
  ∑ i in range (φ.total_degree + 1), homogeneous_component R i φ = φ :=
begin
  ext1 d,
  suffices : φ.total_degree < d.support.sum d → 0 = coeff d φ,
    by simpa [coeff_sum, coeff_homogeneous_component],
  exact λ h, (coeff_eq_zero_of_total_degree_lt h).symm
end

lemma homogeneous_component_homogeneous_polynomial (m n : ℕ)
  (p : mv_polynomial σ R) (h : p ∈ homogeneous_submodule σ R n) :
  homogeneous_component R m p = if m = n then p else 0 :=
by convert weighted_homogeneous_component_weighted_homogeneous_polynomial m n p h

end homogeneous_component

end

section graded_algebra

variable (σ)
/-- The decomposition of mv_polynomial σ R into  homogeneous submodules -/
def decomposition [decidable_eq σ] [decidable_eq R] :
  direct_sum.decomposition (homogeneous_submodule σ R) :=  weighted_decomposition R (1 : σ → ℕ)

/-- Given a weight, mv_polynomial as a graded algebra -/
def graded_algebra
  [decidable_eq σ] [decidable_eq R] :
  graded_algebra (homogeneous_submodule σ R) :=
  weighted_graded_algebra R (1 : σ → ℕ)

lemma decomposition.decompose'_eq [decidable_eq σ] [decidable_eq R] : (decomposition σ).decompose' =
λ (φ : mv_polynomial σ R), direct_sum.mk
  (λ (i : ℕ), ↥(homogeneous_submodule σ R i))
  (finset.image degree' φ.support)
  (λ m, ⟨homogeneous_component R m φ, homogeneous_component_mem φ m⟩) := rfl

lemma decomposition.decompose'_apply [decidable_eq σ] [decidable_eq R] (φ : mv_polynomial σ R) (i : ℕ) : ((decomposition σ).decompose' φ i : mv_polynomial σ R) = homogeneous_component R i φ :=
weighted_decomposition.decompose'_apply R _ φ i

end graded_algebra

end mv_polynomial

author: AntoineChambert-Loir