/-
Copyright (c) 2022 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies

! This file was ported from Lean 3 source module group_theory.group_action.support
! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Set.Pointwise.SMul

/-!
# Support of an element under an action action

Given an action of a group `G` on a type `α`, we say that a set `s : Set α` supports an element
`a : α` if, for all `g` that fix `s` pointwise, `g` fixes `a`.

This is crucial in Fourier-Motzkin constructions.
-/

open Pointwise

variable {G: Type ?u.292
G H: Type ?u.5
H α: Type ?u.298
α β: Type ?u.301
β : Type _: Type (?u.11+1)
Type _}

namespace MulAction

section SMul

variable (G: ?m.26
G) [SMul: Type ?u.30 → Type ?u.29 → Type (max?u.30?u.29)
SMul G: ?m.26
G α: Type ?u.298
α] [SMul: Type ?u.34 → Type ?u.33 → Type (max?u.34?u.33)
SMul G: ?m.26
G β: Type ?u.23
β]

/-- A set `s` supports `b` if `g • b = b` whenever `g • a = a` for all `a ∈ s`. -/
@[to_additive: (G : Type u_1) → {α : Type u_2} → {β : Type u_3} → [inst : VAdd G α] → [inst : VAdd G β] → Set α → β → Prop
to_additive "A set `s` supports `b` if `g +ᵥ b = b` whenever `g +ᵥ a = a` for all `a ∈ s`."]
def Supports: (G : Type u_1) → {α : Type u_2} → {β : Type u_3} → [inst : SMul G α] → [inst : SMul G β] → Set α → β → Prop
Supports (s: Set α
s : Set: Type ?u.57 → Type ?u.57
Set α: Type ?u.43
α) (b: β
b : β: Type ?u.46
β) :=
  ∀ g: G
g : G: Type ?u.37
G, (∀ ⦃a: ?m.72
a⦄, a: ?m.72
a ∈ s: Set α
s → g: G
g • a: ?m.72
a = a: ?m.72
a) → g: G
g • b: β
b = b: β
b
#align mul_action.supports MulAction.Supports: (G : Type u_1) → {α : Type u_2} → {β : Type u_3} → [inst : SMul G α] → [inst : SMul G β] → Set α → β → Prop
MulAction.Supports
#align add_action.supports AddAction.Supports: (G : Type u_1) → {α : Type u_2} → {β : Type u_3} → [inst : VAdd G α] → [inst : VAdd G β] → Set α → β → Prop
AddAction.Supports

variable {s: Set α
s t: Set α
t : Set: Type ?u.312 → Type ?u.312
Set α: Type ?u.444
α} {a: α
a : α: Type ?u.268
α} {b: β
b : β: Type ?u.271
β}

@[to_additive: ∀ (G : Type u_2) {α : Type u_1} [inst : VAdd G α] {s : Set α} {a : α}, a ∈ s → AddAction.Supports G s a
to_additive]
theorem supports_of_mem: a ∈ s → Supports G s a
supports_of_mem (ha: a ∈ s
ha : a: α
a ∈ s: Set α
s) : Supports: (G : Type ?u.352) → {α : Type ?u.351} → {β : Type ?u.350} → [inst : SMul G α] → [inst : SMul G β] → Set α → β → Prop
Supports G: Type ?u.292
G s: Set α
s a: α
a := fun _: ?m.373
_ h: ?m.376
h => h: ?m.376
h ha: a ∈ s
ha
#align mul_action.supports_of_mem MulAction.supports_of_mem: ∀ (G : Type u_2) {α : Type u_1} [inst : SMul G α] {s : Set α} {a : α}, a ∈ s → Supports G s a
MulAction.supports_of_mem
#align add_action.supports_of_mem AddAction.supports_of_mem: ∀ (G : Type u_2) {α : Type u_1} [inst : VAdd G α] {s : Set α} {a : α}, a ∈ s → AddAction.Supports G s a
AddAction.supports_of_mem

variable {G: ?m.468
G}

@[to_additive: ∀ {G : Type u_2} {α : Type u_1} {β : Type u_3} [inst : VAdd G α] [inst_1 : VAdd G β] {s t : Set α} {b : β},
  s ⊆ t → AddAction.Supports G s b → AddAction.Supports G t b
to_additive]
theorem Supports.mono: ∀ {G : Type u_2} {α : Type u_1} {β : Type u_3} [inst : SMul G α] [inst_1 : SMul G β] {s t : Set α} {b : β},
  s ⊆ t → Supports G s b → Supports G t b
Supports.mono (h: s ⊆ t
h : s: Set α
s ⊆ t: Set α
t) (hs: Supports G s b
hs : Supports: (G : Type ?u.522) → {α : Type ?u.521} → {β : Type ?u.520} → [inst : SMul G α] → [inst : SMul G β] → Set α → β → Prop
Supports G: Type ?u.471
G s: Set α
s b: β
b) : Supports: (G : Type ?u.553) → {α : Type ?u.552} → {β : Type ?u.551} → [inst : SMul G α] → [inst : SMul G β] → Set α → β → Prop
Supports G: Type ?u.471
G t: Set α
t b: β
b := fun _: ?m.566
_ hg: ?m.569
hg =>
  (hs: Supports G s b
hs _: G
_) fun _: ?m.585
_ ha: ?m.588
ha => hg: ?m.569
hg <| h: s ⊆ t
h ha: ?m.588
ha
#align mul_action.supports.mono MulAction.Supports.mono: ∀ {G : Type u_2} {α : Type u_1} {β : Type u_3} [inst : SMul G α] [inst_1 : SMul G β] {s t : Set α} {b : β},
  s ⊆ t → Supports G s b → Supports G t b
MulAction.Supports.mono
#align add_action.supports.mono AddAction.Supports.mono: ∀ {G : Type u_2} {α : Type u_1} {β : Type u_3} [inst : VAdd G α] [inst_1 : VAdd G β] {s t : Set α} {b : β},
  s ⊆ t → AddAction.Supports G s b → AddAction.Supports G t b
AddAction.Supports.mono

end SMul

variable [Group: Type ?u.1985 → Type ?u.1985
Group H: Type ?u.690
H] [SMul: Type ?u.703 → Type ?u.702 → Type (max?u.703?u.702)
SMul G: Type ?u.687
G α: Type ?u.693
α] [SMul: Type ?u.707 → Type ?u.706 → Type (max?u.707?u.706)
SMul G: Type ?u.687
G β: Type ?u.696
β] [MulAction: (α : Type ?u.711) → Type ?u.710 → [inst : Monoid α] → Type (max?u.711?u.710)
MulAction H: Type ?u.690
H α: Type ?u.693
α] [SMul: Type ?u.1001 → Type ?u.1000 → Type (max?u.1001?u.1000)
SMul H: Type ?u.690
H β: Type ?u.696
β] [SMulCommClass: (M : Type ?u.1006) → (N : Type ?u.1005) → (α : Type ?u.1004) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass G: Type ?u.687
G H: Type ?u.690
H β: Type ?u.696
β]
  [SMulCommClass: (M : Type ?u.1033) → (N : Type ?u.1032) → (α : Type ?u.1031) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass G: Type ?u.687
G H: Type ?u.690
H α: Type ?u.1979
α] {s: Set α
s t: Set α
t : Set: Type ?u.1968 → Type ?u.1968
Set α: Type ?u.693
α} {b: β
b : β: Type ?u.696
β}

-- TODO: This should work without `SMulCommClass`
@[to_additive: ∀ {G : Type u_1} {H : Type u_4} {α : Type u_2} {β : Type u_3} [inst : AddGroup H] [inst_1 : VAdd G α]
  [inst_2 : VAdd G β] [inst_3 : AddAction H α] [inst_4 : VAdd H β] [inst_5 : VAddCommClass G H β]
  [inst_6 : VAddCommClass G H α] {s : Set α} {b : β} (g : H),
  AddAction.Supports G s b → AddAction.Supports G (g +ᵥ s) (g +ᵥ b)
to_additive]
theorem Supports.smul: ∀ (g : H), Supports G s b → Supports G (g • s) (g • b)
Supports.smul (g: H
g : H: Type ?u.1976
H) (h: Supports G s b
h : Supports: (G : Type ?u.3263) → {α : Type ?u.3262} → {β : Type ?u.3261} → [inst : SMul G α] → [inst : SMul G β] → Set α → β → Prop
Supports G: Type ?u.1973
G s: Set α
s b: β
b) : Supports: (G : Type ?u.3295) → {α : Type ?u.3294} → {β : Type ?u.3293} → [inst : SMul G α] → [inst : SMul G β] → Set α → β → Prop
Supports G: Type ?u.1973
G (g: H
g • s: Set α
s) (g: H
g • b: β
b) := by
Goals accomplished! 🐙
  G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

Supports G (g • s) (g • b)rintro g': G
g' hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
hg'G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

g': G

hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a

g' • g • b = g • b
  G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

Supports G (g • s) (g • b)rw [G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

g': G

hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a

g' • g • b = g • bsmul_comm: ∀ {M : Type ?u.4365} {N : Type ?u.4364} {α : Type ?u.4363} [inst : SMul M α] [inst_1 : SMul N α]
  [self : SMulCommClass M N α] (m : M) (n : N) (a : α), m • n • a = n • m • a
smul_comm,G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

g': G

hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a

g • g' • b = g • b G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

g': G

hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a

g' • g • b = g • bh: Supports G s b
hG: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

g': G

hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a

g • b = g • b
G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

g': G

hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a

a∀ ⦃a : α⦄, a ∈ s → g' • a = a]G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

g': G

hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a

a∀ ⦃a : α⦄, a ∈ s → g' • a = a
  G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

Supports G (g • s) (g • b)rintro a: α
a ha: a ∈ s
haG: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

g': G

hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a

a: α

ha: a ∈ s

ag' • a = a
  G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

Supports G (g • s) (g • b)have := Set.ball_image_iff: ∀ {α : Type ?u.4730} {β : Type ?u.4731} {f : α → β} {s : Set α} {p : β → Prop},
  (∀ (y : β), y ∈ f '' s → p y) ↔ ∀ (x : α), x ∈ s → p (f x)
Set.ball_image_iff.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
hg' a: α
a ha: a ∈ s
haG: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

g': G

hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a

a: α

ha: a ∈ s

this: g' • g • a = g • a

ag' • a = a
  G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

Supports G (g • s) (g • b)rwa [G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

g': G

hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a

a: α

ha: a ∈ s

this: g' • g • a = g • a

ag' • a = asmul_comm: ∀ {M : Type ?u.4775} {N : Type ?u.4774} {α : Type ?u.4773} [inst : SMul M α] [inst_1 : SMul N α]
  [self : SMulCommClass M N α] (m : M) (n : N) (a : α), m • n • a = n • m • a
smul_comm,G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

g': G

hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a

a: α

ha: a ∈ s

this: g • g' • a = g • a

ag' • a = a G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

g': G

hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a

a: α

ha: a ∈ s

this: g' • g • a = g • a

ag' • a = asmul_left_cancel_iff: ∀ {α : Type ?u.6089} {β : Type ?u.6088} [inst : Group α] [inst_1 : MulAction α β] (g : α) {x y : β},
  g • x = g • y ↔ x = y
smul_left_cancel_iffG: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

g': G

hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a

a: α

ha: a ∈ s

this: g' • a = a

ag' • a = a]G: Type u_1

H: Type u_4

α: Type u_2

β: Type u_3

inst✝⁶: Group H

inst✝⁵: SMul G α

inst✝⁴: SMul G β

inst✝³: MulAction H α

inst✝²: SMul H β

inst✝¹: SMulCommClass G H β

inst✝: SMulCommClass G H α

s, t: Set α

b: β

g: H

h: Supports G s b

g': G

hg': ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a

a: α

ha: a ∈ s

this: g' • a = a

ag' • a = a at this: ?m.4729
this
Goals accomplished! 🐙
#align mul_action.supports.smul MulAction.Supports.smul: ∀ {G : Type u_1} {H : Type u_4} {α : Type u_2} {β : Type u_3} [inst : Group H] [inst_1 : SMul G α] [inst_2 : SMul G β]
  [inst_3 : MulAction H α] [inst_4 : SMul H β] [inst_5 : SMulCommClass G H β] [inst_6 : SMulCommClass G H α] {s : Set α}
  {b : β} (g : H), Supports G s b → Supports G (g • s) (g • b)
MulAction.Supports.smul
#align add_action.supports.vadd AddAction.Supports.vadd: ∀ {G : Type u_1} {H : Type u_4} {α : Type u_2} {β : Type u_3} [inst : AddGroup H] [inst_1 : VAdd G α]
  [inst_2 : VAdd G β] [inst_3 : AddAction H α] [inst_4 : VAdd H β] [inst_5 : VAddCommClass G H β]
  [inst_6 : VAddCommClass G H α] {s : Set α} {b : β} (g : H),
  AddAction.Supports G s b → AddAction.Supports G (g +ᵥ s) (g +ᵥ b)
AddAction.Supports.vadd

end MulAction