mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
hx : x ∈ closure (Set.range f)
⊢ ∃ a, x = ∏ i, f i ^ a i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ x ∈ closure (Set.range f) ↔ ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ x ∈ closure (Set.range f) ↔ ∃ a, x = ∏ i, f i ^ a i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommGroup M
x : M
s : Set M
inst✝ : Fintype ↑s
⊢ x ∈ closure s ↔ ∃ a, x = ∏ i, ↑i ^ a i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: S : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : LinearOrder G
x✝ : SetLike S G
inst✝ : InvMemClass S G
H : S
x : G
⊢ |x|ₘ ∈ H ↔ x ∈ H

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
a : C
ha : a ∈ (x ⊔ y) ⊓ z
⊢ a ∈ x ⊔ y ⊓ z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : M ≠ ⊤
⊢ comap φ M ≠ ⊤

Tactic:
← (comap_injective hφ).ne_iff,

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : comap φ M ≠ comap φ ⊤
⊢ comap φ M ≠ ⊤
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM : IsCoatom M
⊢ IsCoatom (comap φ M)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝³ : CommMonoid G
inst✝² : LinearOrder G
inst✝¹ : CommMonoid G'
inst✝ : Preorder G'
e : G ≃* G'
he : StrictMono ⇑e
⊢ StrictMono ⇑e.symm

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ f i = (Finsupp.single i 1).prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
hx : x ∈ closure (Set.range f)
⊢ ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: R : Type u_4
inst✝ : Ring R
r : R
k : ℤ
⊢ ↑k * r ∈ zmultiples r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: R : Type u_4
inst✝ : Ring R
k : ℤ
⊢ (fun x ↦ x • 1) k = ↑k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
inst✝ : Fintype ι
a : ι →₀ ℕ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ (a.prod fun x1 x2 ↦ f x1 ^ x2) = ∏ i, f i ^ a i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
hx : x ∈ closure (Set.range f)
⊢ ∃ a, x = ∏ i, f i ^ a i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: A : Type u_4
inst✝ : AddGroupWithOne A
⊢ (castAddHom A).range = zmultiples 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: n : ℕ
⊢ (nsmulAddMonoidHom n).range = zmultiples ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ x ∈ closure (Set.range f) ↔ ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: a b : ℤ
⊢ closure {a, b} = zmultiples ↑(a.gcd b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ x ∈ closure (Set.range f) ↔ ∃ a, x = ∏ i, f i ^ a i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: a b : ℤ
⊢ zmultiples a ⊔ zmultiples b = zmultiples ↑(a.gcd b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
x : M
s : Set M
inst✝ : Fintype ↑s
⊢ x ∈ closure s ↔ ∃ a, x = ∏ i, ↑i ^ a i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: a b : ℤ
⊢ zmultiples a ⊓ zmultiples b = zmultiples ↑(a.lcm b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
f : G → α
⊢ τ 0 f = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
⊢ τ a (τ b f) = τ (a + b) f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
⊢ τ (a + b) f = τ a (τ b f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
⊢ τ (a + b) f = τ b (τ a f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
⊢ τ a (τ b f) = τ b (τ a f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a : G
f : G → α
⊢ τ a f = DomAddAct.mk (-a) +ᵥ f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
⊢ ∀ {x : G}, x ∈ (M ⊓ M⁻¹).carrier → x⁻¹ ∈ (M ⊓ M⁻¹).carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : AddCommMonoid M
a : G
f : ι → G → M
s : Finset ι
⊢ τ a (∑ i ∈ s, f i) = ∑ i ∈ s, τ a (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x✝³ : Subgroup G
x✝² : Submonoid G
x✝¹ : x✝³.toSubmonoid ≤ x✝²
x✝ : G
⊢ x✝ ∈ x✝³ → x✝ ∈ x✝².mulSupport

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
⊢ M.IsMulPointed → M.mulSupport = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: G : Type u_5
H : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
f : G → H
⊢ support (τ a f) = a +ᵥ support f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
h : M.mulSupport = ⊥
x : G
⊢ x ∈ M → x⁻¹ ∈ M → x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
hM : M.IsMulSpanning
a : G
⊢ a ∈ M ∨ a⁻¹ ∈ M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M N : Submonoid G
hM : M.IsMulSpanning
h : M ≤ N
⊢ N.IsMulSpanning

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : CommMonoid M
a : G
f : ι → G → M
s : Finset ι
⊢ τ a (∏ i ∈ s, f i) = ∏ i ∈ s, τ a (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
hMp : M.IsMulPointed
hMs : M.IsMulSpanning
N : Submonoid G
hN : N.IsMulPointed
h : M ≤ N
⊢ N ≤ M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (Submonoid M)
hf : ∀ s ∈ f, s.MulSaturated
x✝¹ x✝ : M
hxy : x✝¹ * x✝ ∈ InfSet.sInf f
⊢ x✝¹ ∈ InfSet.sInf f ∧ x✝ ∈ InfSet.sInf f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝¹ x✝ : SaturatedSubmonoid M
s₁ : Submonoid M
h₁ : s₁.MulSaturated
s₂ : Submonoid M
h₂ : s₂.MulSaturated
eq : { toSubmonoid := s₁, mulSaturated := h₁ }.toSubmonoid = { toSubmonoid := s₂, mulSaturated := h₂ }.toSubmonoid
⊢ { toSubmonoid := s₁, mulSaturated := h₁ } = { toSubmonoid := s₂, mulSaturated := h₂ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ s ∈ f, ↑s
hy : b✝ ∈ ⋂ s ∈ f, ↑s
⊢ a✝ * b✝ ∈ ⋂ s ∈ f, ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
⊢ ∀ s ∈ toSubmonoid '' f, s.MulSaturated

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
⊢ { carrier := ⋂ s ∈ f, ↑s, mul_mem' := ⋯, one_mem' := ⋯ }.MulSaturated

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Submonoid M
hs : s.saturation.toSubmonoid ≤ s
⊢ s.saturation.MulSaturated

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Submonoid M
p : (x : M) → x ∈ s.saturation → Prop
mem : ∀ (x : M) (hx : x ∈ s), p x ⋯
mul : ∀ (x y : M) (hx : x ∈ s.saturation) (hy : y ∈ s.saturation), p x hx → p y hy → p (x * y) ⋯
of_mul : ∀ (x y : M) (hxy : x * y ∈ s.saturation), p (x * y) hxy → p x ⋯ ∧ p y ⋯
x : M
hx : x ∈ s.saturation
⊢ p x hx

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x✝ : M
hx : x✝ ∈ s
⊢ x✝ * 1 ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x✝ y✝ : M
hx✝ : x✝ ∈ s.saturation
hy✝ : y✝ ∈ s.saturation
ih₁ : ∃ y, x✝ * y ∈ s
ih₂ : ∃ y, y✝ * y ∈ s
y₁ : M
h₁ : x✝ * y₁ ∈ s
y₂ : M
h₂ : y✝ * y₂ ∈ s
⊢ x✝ * y✝ * (y₁ * y₂) ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy✝ : x₁ * x₂ ∈ s.saturation
ih : ∃ y, x₁ * x₂ * y ∈ s
y : M
h : x₁ * x₂ * y ∈ s
⊢ x₁ * (x₂ * y) ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy✝ : x₁ * x₂ ∈ s.saturation
ih : ∃ y, x₁ * x₂ * y ∈ s
y : M
h : x₁ * x₂ * y ∈ s
⊢ x₂ * (x₁ * y) ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x : M
h : x ∈ s.saturation
⊢ ∃ y, x * y ∈ s

Tactic:
induction h using saturation_induction with

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x : M
⊢ x ∈ s.saturation ↔ ∃ y, x * y ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x : M
⊢ x ∈ s.saturation ↔ ∃ y, y * x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x : M
⊢ x ∈ s.saturation ↔ ∃ m ∈ s, x ∣ m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
⊢ x ∈ ⊥ ↔ IsUnit x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Center

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
u : ↥(center G₀ˣ)
⊢ ↥(Submonoid.center G₀)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : Monoid M
v : ι → M
s : Set ι
⊢ {i | IsMulIndecomposable v s i} ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: M : Type u_2
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x : M
hx : x ≠ 1
h : IsMulIndecomposable id univ x
⊢ ¬IsUnit x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: M : Type u_2
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x : M
hx : x ≠ 1
h : IsMulIndecomposable id univ x
⊢ ∀ ⦃a b : M⦄, x = a * b → IsUnit a ∨ IsUnit b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: M : Type u_2
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x : M
hx : x ≠ 1
h : Irreducible x
⊢ IsMulIndecomposable id univ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
this : ∀ (f : G →* S), v '' baseOf v (invMonoidHom.comp f) ⊆ ⇑invMonoidHom ∘ v '' baseOf v f
⊢ v '' baseOf v (invMonoidHom.comp f) = ⇑invMonoidHom ∘ v '' baseOf v f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi : i ∈ {i | 1 < (invMonoidHom.comp f) (v i)}
hi' :
  ∀ j ∈ {i | 1 < (invMonoidHom.comp f) (v i)},
    ∀ k ∈ {i | 1 < (invMonoidHom.comp f) (v i)}, v i = v j * v k → v j = 1 ∨ v k = 1
⊢ i⁻¹ ∈ {i | 1 < f (v i)}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi : i ∈ {i | 1 < (invMonoidHom.comp f) (v i)}
hi' :
  ∀ j ∈ {i | 1 < (invMonoidHom.comp f) (v i)},
    ∀ k ∈ {i | 1 < (invMonoidHom.comp f) (v i)}, v i = v j * v k → v j = 1 ∨ v k = 1
⊢ (⇑invMonoidHom ∘ v) i⁻¹ = v i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Conj

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
⊢ IsConj a b ↔ ∃ c, c ≠ 0 ∧ c * a * c⁻¹ = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi✝ : i ∈ {i | 1 < (invMonoidHom.comp f) (v i)}
hi' :
  ∀ j ∈ {i | 1 < (invMonoidHom.comp f) (v i)},
    ∀ k ∈ {i | 1 < (invMonoidHom.comp f) (v i)}, v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : j ∈ {i | 1 < f (v i)}
k : ι
hk : k ∈ {i | 1 < f (v i)}
hi : v i⁻¹ = v j * v k
⊢ v i = v j⁻¹ * v k⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi✝ : i ∈ {i | 1 < (invMonoidHom.comp f) (v i)}
hi' :
  ∀ j ∈ {i | 1 < (invMonoidHom.comp f) (v i)},
    ∀ k ∈ {i | 1 < (invMonoidHom.comp f) (v i)}, v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : j ∈ {i | 1 < f (v i)}
k : ι
hk : k ∈ {i | 1 < f (v i)}
hi : v i = v j⁻¹ * v k⁻¹
⊢ j⁻¹ ∈ {i | 1 < (invMonoidHom.comp f) (v i)}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi✝ : i ∈ {i | 1 < (invMonoidHom.comp f) (v i)}
hi' :
  ∀ j ∈ {i | 1 < (invMonoidHom.comp f) (v i)},
    ∀ k ∈ {i | 1 < (invMonoidHom.comp f) (v i)}, v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : j ∈ {i | 1 < f (v i)}
k : ι
hk : k ∈ {i | 1 < f (v i)}
hi : v i = v j⁻¹ * v k⁻¹
⊢ k⁻¹ ∈ {i | 1 < (invMonoidHom.comp f) (v i)}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
⊢ v '' baseOf v (invMonoidHom.comp f) = ⇑invMonoidHom ∘ v '' baseOf v f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : IsLeftCancelMulZero α
⊢ #s ≤ #(s * s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
s : Finset α
⊢ s * 0 ⊆ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
s : Finset α
⊢ 0 * s ⊆ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ s * 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ 0 * s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
⊢ s / 0 ⊆ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
⊢ 0 / s ⊆ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
k : ι
hk₀ : 1 < f (v k)
hk₁ : f (v k) < f (v i)
⊢ v k ∈ closure (v '' t)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ s / 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ 0 / s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
⊢ 0⁻¹ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
⊢ i ∉ t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
hi₃ : i ∉ t
⊢ ∃ j k, ∃ (_ : 1 < f (v j)) (_ : 1 < f (v k)), v i = v j * v k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
hi₃ : i ∉ t
j k : ι
hj : 1 < f (v j)
hk : 1 < f (v k)
hjk : v i = v j * v k
⊢ f (v j) < f (v i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
hi₃ : i ∉ t
j k : ι
hj : 1 < f (v j)
hk : 1 < f (v k)
hjk : v i = v j * v k
hj' : v j ∈ closure (v '' t)
⊢ f (v k) < f (v i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
⊢ closure (v '' IsMulIndecomposable.baseOf v f) = closure (v '' {i | 1 < f (v i)})

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
⊢ IsMulIndecomposable.baseOf v f ⊆ univ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
⊢ univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}

Tactic:
by

Goal state after: