awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
M : Type u_2
S : Type u_4
inst : Monoid M
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
hi₂ :
  ∀ (k : ι) (hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S))
    (hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)),
    Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
hi₃ : i ∉ t
j k : ι
hj : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)
hk : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S)
hjk : v i = v j * v k
hj' : Membership.mem (γ := Submonoid M) (closure (v '' t)) (v j)
hk' : Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
⊢ Membership.mem (γ := Submonoid M) (closure (v '' t)) (v i)

Tactic:
replace hjk : v i ∈ closure (v '' t) := hjk ▸ mul_mem hj' hk'
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
M : Type u_2
S : Type u_4
inst : Monoid M
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
hi₂ :
  ∀ (k : ι) (hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S))
    (hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)),
    Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
hi₃ : i ∉ t
j k : ι
hj : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)
hk : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S)
hj' : Membership.mem (γ := Submonoid M) (closure (v '' t)) (v j)
hk' : Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
hjk : Membership.mem (γ := Submonoid M) (closure (v '' t)) (v i)
⊢ False

Tactic:
hi₁ hjk
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
M : Type u_2
S : Type u_4
inst : Monoid M
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
hi₂ :
  ∀ (k : ι) (hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S))
    (hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)),
    Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
hi₃ : i ∉ t
j k : ι
hj : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)
hk : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S)
hj' : Membership.mem (γ := Submonoid M) (closure (v '' t)) (v j)
hk' : Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
hjk : Membership.mem (γ := Submonoid M) (closure (v '' t)) (v i)
⊢ False

Tactic:
exact hi₁ hjk
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
rw : Eq (α := Subgroup G) (closure (v '' IsMulIndecomposable.baseOf v f)) (closure (v '' univ))
⊢ Eq (α := Subgroup G) (closure (v '' IsMulIndecomposable.baseOf v f)) (closure (range v))

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
⊢ IsMulIndecomposable.baseOf v f ⊆ univ

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
refine : v '' univ ⊆ (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)
⊢ Eq (α := Subgroup G) (closure (v '' IsMulIndecomposable.baseOf v f)) (closure (v '' univ))

Tactic:
refine le_antisymm (closure_mono (image_mono <| by simp)) ((closure_le _).mpr ?_)

Premises used: Iff.mpr, Set.image_mono, Subgroup.closure_le, Subgroup.closure_mono, le_antisymm
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
h :
  ∀ (i : ι),
    Membership.mem (γ := Set ι) univ i ↔
      Membership.mem (γ := Set ι)
        ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
          {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
        i
⊢ Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})

Tactic:
ext i
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
i : ι
⊢ Membership.mem (γ := Set ι) univ i ↔
    Membership.mem (γ := Set ι)
      ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
        {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
      i

Tactic:
simp [(hf i).symm]

Premises used: Ne.symm
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
⊢ Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})

Tactic:
have : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1} := by ext i; simp [(hf i).symm]
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
this :
  Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
rw :
  v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ⊆
      (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G) ∧
    v '' {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)} ⊆
      (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)
⊢ v '' univ ⊆ (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)

Tactic:
rw [this, image_union, union_subset_iff]

Premises used: Set.union_subset_iff, Set.image_union
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
this :
  Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
⊢ v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ⊆
      (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G) ∧
    v '' {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)} ⊆
      (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)

Tactic:
⟨le_trans ?_ (le_closure_toSubmonoid (v '' IsMulIndecomposable.baseOf v f)), ?_⟩

Premises used: Subgroup.le_closure_toSubmonoid, IsMulIndecomposable.baseOf, And.intro, Set.image, le_trans
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
this :
  Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
refine_1 :
  v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ≤
    (↑(Submonoid.closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)
refine_2 :
  v '' {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)} ⊆
    (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)
⊢ v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ⊆
      (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G) ∧
    v '' {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)} ⊆
      (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)

Tactic:
refine ⟨le_trans ?_ (le_closure_toSubmonoid (v '' IsMulIndecomposable.baseOf v f)), ?_⟩
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
this :
  Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
⊢ v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ≤
    (↑(Submonoid.closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)

Tactic:
simp [Submonoid.closure_image_isMulIndecomposable_baseOf]

Premises used: Submonoid.closure_image_isMulIndecomposable_baseOf
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
this :
  Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
f' : G →* S := MonoidHom.comp invMonoidHom f
rw :
  Function.comp (β := G) (⇑invMonoidHom : (a : G) → G) (⇑invMonoidHom : (a : G) → G) ''
      v '' IsMulIndecomposable.baseOf v f =
    v '' IsMulIndecomposable.baseOf v f
⊢ (⇑invMonoidHom : (a : G) → G) ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f

Tactic:
rw [image_comp, IsMulIndecomposable.image_baseOf_inv_comp_eq v hv_inv f, image_comp,
        ← image_comp]

Premises used: IsMulIndecomposable.image_baseOf_inv_comp_eq, Set.image_comp
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
this :
  Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
f' : G →* S := MonoidHom.comp invMonoidHom f
⊢ Function.comp (β := G) (⇑invMonoidHom : (a : G) → G) (⇑invMonoidHom : (a : G) → G) ''
      v '' IsMulIndecomposable.baseOf v f =
    v '' IsMulIndecomposable.baseOf v f

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
this :
  Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
f' : G →* S := MonoidHom.comp invMonoidHom f
⊢ (⇑invMonoidHom : (a : G) → G) ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f

Tactic:
have h₁ : (invMonoidHom ∘ v) '' IsMulIndecomposable.baseOf v f' =
        v '' IsMulIndecomposable.baseOf v f := by
      rw [image_comp, IsMulIndecomposable.image_baseOf_inv_comp_eq v hv_inv f, image_comp,
        ← image_comp]
      simp
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
this :
  Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
f' : G →* S := MonoidHom.comp invMonoidHom f
h₁ : (⇑invMonoidHom : (a : G) → G) ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
⊢ v '' {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)} =
    v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f' : (a : G) → S) (v i) : S)}

Tactic:
simp [f']
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
this :
  Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
f' : G →* S := MonoidHom.comp invMonoidHom f
h₁ : (⇑invMonoidHom : (a : G) → G) ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
⊢ v '' {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)} =
    v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f' : (a : G) → S) (v i) : S)}

Tactic:
have h₂ : v '' {i | f (v i) < 1} = v '' {i | 1 < f' (v i)} := by simp [f']
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
this :
  Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
f' : G →* S := MonoidHom.comp invMonoidHom f
h₁ : (⇑invMonoidHom : (a : G) → G) ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
h₂ :
  v '' {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)} =
    v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f' : (a : G) → S) (v i) : S)}
refine_2 :
  v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f' : (a : G) → S) (v i) : S)} ⊆
    (↑(closure (v '' IsMulIndecomposable.baseOf v f')) : Set G)
⊢ v '' {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)} ⊆
    (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)

Tactic:
rw [h₂, ← h₁, image_comp, coe_invMonoidHom, image_inv_eq_inv, closure_inv]

Premises used: coe_invMonoidHom, Subgroup.closure_inv, Set.image_comp, Set.image_inv_eq_inv
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
this :
  Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
f' : G →* S := MonoidHom.comp invMonoidHom f
h₁ : (⇑invMonoidHom : (a : G) → G) ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
h₂ :
  v '' {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)} =
    v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f' : (a : G) → S) (v i) : S)}
⊢ v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f' : (a : G) → S) (v i) : S)} ⊆
    (↑(closure (v '' IsMulIndecomposable.baseOf v f')) : Set G)

Tactic:
le_trans ?_ (le_closure_toSubmonoid (v '' IsMulIndecomposable.baseOf v f'))

Premises used: Subgroup.le_closure_toSubmonoid, IsMulIndecomposable.baseOf, Set.image, le_trans
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
this :
  Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
f' : G →* S := MonoidHom.comp invMonoidHom f
h₁ : (⇑invMonoidHom : (a : G) → G) ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
h₂ :
  v '' {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)} =
    v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f' : (a : G) → S) (v i) : S)}
refine_2 :
  v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f' : (a : G) → S) (v i) : S)} ≤
    (↑(Submonoid.closure (v '' IsMulIndecomposable.baseOf v f')) : Set G)
⊢ v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f' : (a : G) → S) (v i) : S)} ⊆
    (↑(closure (v '' IsMulIndecomposable.baseOf v f')) : Set G)

Tactic:
refine le_trans ?_ (le_closure_toSubmonoid (v '' IsMulIndecomposable.baseOf v f'))

Premises used: Subgroup.le_closure_toSubmonoid, IsMulIndecomposable.baseOf, Set.image, le_trans
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
this :
  Eq.{u_1 + 1} (α := Set ι) univ
    ({i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} ∪
      {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)})
f' : G →* S := MonoidHom.comp invMonoidHom f
h₁ : (⇑invMonoidHom : (a : G) → G) ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
h₂ :
  v '' {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)} =
    v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f' : (a : G) → S) (v i) : S)}
⊢ v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f' : (a : G) → S) (v i) : S)} ≤
    (↑(Submonoid.closure (v '' IsMulIndecomposable.baseOf v f')) : Set G)

Tactic:
simp [Submonoid.closure_image_isMulIndecomposable_baseOf]

Premises used: Submonoid.closure_image_isMulIndecomposable_baseOf
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
inst : CommGroup G
inst_1 : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i : ι | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
⊢ s ⊆ t

Tactic:
have h_sub : s ⊆ t := hst.trans (IsMulIndecomposable.subset _ _)
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
inst : CommGroup G
inst_1 : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i : ι | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
by_contra! : ∀ (k : ι) (hk : v k = v i / v j), False
⊢ v i / v j ∉ range v

Tactic:
by_contra! ⟨k, hk⟩
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
inst : CommGroup G
inst_1 : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i : ι | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
inl : ∀ (hk' : k ∈ t), False
inr : ∀ (hk' : k⁻¹ ∈ t), False
⊢ False

Tactic:
rcases hv_t k with hk' | hk'
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
inst : CommGroup G
inst_1 : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i : ι | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
hk' : k ∈ t
inl : ¬IsMulIndecomposable v t i
⊢ False

Tactic:
suffices ¬ IsMulIndecomposable v t i from this (hst hi)
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
inst : CommGroup G
inst_1 : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i : ι | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
hk' : k ∈ t
inl : i ∈ t → ∃ (x : ι) (_ : x ∈ t) (x_1 : ι) (_ : x_1 ∈ t), v i = v x * v x_1
⊢ ¬IsMulIndecomposable v t i

Tactic:
simp only [IsMulIndecomposable, hv_one, or_self, imp_false, not_and, not_forall, not_not]

Premises used: Classical.not_not, IsMulIndecomposable, imp_false, or_self, not_and, Classical.not_forall