awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : i ∈ t
⊢ v i = v k * v j

Tactic:
simp [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
⊢ i ∈ t → ∃ (x : ι) (_ : x ∈ t) (x_1 : ι) (_ : x_1 ∈ t), v i = v x * v x_1

Tactic:
exact fun _ ↦ ⟨k, hk', j, h_sub hj, by simp [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
inr : ¬IsMulIndecomposable v t j
⊢ False

Tactic:
suffices ¬ IsMulIndecomposable v t j from this (hst hj)
-- 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
inr : j ∈ t → ∃ (x : ι) (_ : x ∈ t) (x_1 : ι) (_ : x_1 ∈ t), v j = v x * v x_1
⊢ ¬IsMulIndecomposable v t j

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
-- 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
h : j ∈ t
⊢ v j = v k⁻¹ * v i

Tactic:
simp [hv_inv, 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
⊢ j ∈ t → ∃ (x : ι) (_ : x ∈ t) (x_1 : ι) (_ : x_1 ∈ t), v j = v x * v x_1

Tactic:
exact fun _ ↦ ⟨k⁻¹, hk', i, h_sub hi, by simp [hv_inv, hk]⟩
-- 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 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : 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)
s : Set ι
hst : s ⊆ {j : ι | IsMulIndecomposable v {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j}
i : ι
contrapose! : ∀ (hf : v i = 1), ∃ (i : ι), Eq.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
⊢ v i ≠ 1

Tactic:
contrapose! hf
-- 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 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
s : Set ι
hst : s ⊆ {j : ι | IsMulIndecomposable v {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j}
i : ι
hf : v i = 1
⊢ Eq.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)

Tactic:
simp [hf]
-- 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 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
s : Set ι
hst : s ⊆ {j : ι | IsMulIndecomposable v {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j}
i : ι
hf : v i = 1
⊢ ∃ (i : ι), Eq.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)

Tactic:
exact ⟨i, by simp [hf]⟩
-- 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 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : 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)
s : Set ι
hst : s ⊆ {j : ι | IsMulIndecomposable v {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j}
⊢ ∀ (i : ι), v i ≠ 1

Tactic:
have hv_one : ∀ i, v i ≠ 1 := fun i ↦ by contrapose! hf; exact ⟨i, by simp [hf]⟩
-- 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 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : 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)
s : Set ι
hst : s ⊆ {j : ι | IsMulIndecomposable v {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j}
hv_one : ∀ (i : ι), v i ≠ 1
apply :
  ∀ (i : ι),
    Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} i ∨
      Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} i⁻¹
⊢ s.Pairwise fun (i j : ι) ↦ v i / v j ∉ range v

Tactic:
apply pairwise_div_notMem_range v hv_one hv_inv s {i | 1 < f (v i)} hst fun i ↦ ?_

Premises used: IsMulIndecomposable.pairwise_div_notMem_range, setOf, LT.lt, OfNat.ofNat, DFunLike.coe
-- 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 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : 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)
s : Set ι
hst : s ⊆ {j : ι | IsMulIndecomposable v {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j}
hv_one : ∀ (i : ι), v i ≠ 1
i : ι
⊢ Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} i ∨
    Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} i⁻¹

Tactic:
simpa [hv_inv] using (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 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : 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)
⊢ (baseOf v f).Pairwise fun (i j : ι) ↦ v i / v j ∉ range v

Tactic:
pairwise_div_notMem_range' v hv_inv f hf (baseOf v f) (.refl _)

Premises used: Set.Subset.refl, IsMulIndecomposable.baseOf, IsMulIndecomposable.pairwise_div_notMem_range'
-- 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
f : G →* S
i : ι
hi : Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi' : v i⁻¹ = (v i)⁻¹
rw :
  Membership.mem (γ := Submonoid G)
      (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i) ∨
    Membership.mem (γ := Submonoid G)
      (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i)⁻¹
⊢ Membership.mem (γ := Submonoid G) (Submonoid.closure (v '' baseOf v f)) (v i) ∨
    Membership.mem (γ := Submonoid G) (Submonoid.closure (v '' baseOf v f)) (v i)⁻¹

Tactic:
rw [Submonoid.closure_image_isMulIndecomposable_baseOf v f]

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
f : G →* S
i : ι
hi : Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi' : v i⁻¹ = (v i)⁻¹
inl :
  ∀ (hj : LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)),
    Membership.mem (γ := Submonoid G)
        (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i) ∨
      Membership.mem (γ := Submonoid G)
        (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i)⁻¹
inr :
  ∀ (hj : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)),
    Membership.mem (γ := Submonoid G)
        (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i) ∨
      Membership.mem (γ := Submonoid G)
        (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i)⁻¹
⊢ Membership.mem (γ := Submonoid G)
      (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i) ∨
    Membership.mem (γ := Submonoid G)
      (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i)⁻¹

Tactic:
rcases lt_or_gt_of_ne hi with hj | hj

Premises used: lt_or_gt_of_ne
-- 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
f : G →* S
i : ι
hi : Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi' : v i⁻¹ = (v i)⁻¹
hj : LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
inl :
  Membership.mem (γ := Submonoid G)
    (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i)⁻¹
⊢ Membership.mem (γ := Submonoid G)
      (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i) ∨
    Membership.mem (γ := Submonoid G)
      (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i)⁻¹

Tactic:
right
-- 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
f : G →* S
i : ι
hi : Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi' : v i⁻¹ = (v i)⁻¹
hj : LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
⊢ Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} i⁻¹ ∧ v i⁻¹ = (v i)⁻¹

Tactic:
simpa [hi']
-- 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
f : G →* S
i : ι
hi : Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi' : v i⁻¹ = (v i)⁻¹
hj : LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
⊢ Membership.mem (γ := Submonoid G)
    (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i)⁻¹

Tactic:
exact Submonoid.subset_closure ⟨i⁻¹, by simpa [hi']⟩
-- 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
f : G →* S
i : ι
hi : Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi' : v i⁻¹ = (v i)⁻¹
hj : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
inr :
  Membership.mem (γ := Submonoid G)
    (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i)
⊢ Membership.mem (γ := Submonoid G)
      (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i) ∨
    Membership.mem (γ := Submonoid G)
      (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i)⁻¹

Tactic:
left
-- 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
f : G →* S
i : ι
hi : Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi' : v i⁻¹ = (v i)⁻¹
hj : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
⊢ Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} i ∧ v i = v i

Tactic:
simpa
-- 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
f : G →* S
i : ι
hi : Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi' : v i⁻¹ = (v i)⁻¹
hj : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
⊢ Membership.mem (γ := Submonoid G)
    (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i)

Tactic:
exact Submonoid.subset_closure ⟨i, by simpa⟩
-- 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 : CommMonoid S
inst_3 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
⊢ Membership.mem (γ := Submonoid M)
      (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) (v i) ↔
    LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)

Tactic:
⟨fun hi ↦ ?_, fun hi ↦ subset_closure <| mem_image_of_mem v hi⟩

Premises used: Set.mem_image_of_mem, Iff.intro, Submonoid.subset_closure
-- 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 : CommMonoid S
inst_3 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
refine :
  ∀
    (hi :
      Membership.mem (γ := Submonoid M)
        (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) (v i)),
    LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
⊢ Membership.mem (γ := Submonoid M)
      (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) (v i) ↔
    LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)

Tactic:
refine ⟨fun hi ↦ ?_, fun hi ↦ subset_closure <| mem_image_of_mem v hi⟩
-- 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 : CommMonoid S
inst_3 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) (v i)
suffices : v i = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
⊢ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)

Tactic:
suffices v i = 1 ∨ 1 < f (v i) from this.resolve_left hv_one
-- 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 : CommMonoid S
inst_3 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) (v i)
⊢ ∀ (x : M) (h : x ∈ v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)}),
    x = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) x : S)

Tactic:
grind
-- 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 : CommMonoid S
inst_3 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) (v i)
⊢ Eq.{u_2 + 1} (α := M) 1 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) 1 : S)

Tactic:
simp
-- 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 : CommMonoid S
inst_3 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) (v i)
refine :
  ∀ (x y : M),
    Membership.mem (γ := Submonoid M)
        (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) x →
      Membership.mem (γ := Submonoid M)
          (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) y →
        ∀ (hx : x = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) x : S))
          (hy : y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) y : S)),
          x * y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * y) : S)
⊢ v i = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)

Tactic:
refine closure_induction (by grind) (by simp) (fun x y _ _ hx hy ↦ ?_) hi
-- 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 : CommMonoid S
inst_3 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) (v i)
x y : M
h :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) x
h_1 :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) y
hx : x = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) x : S)
hy : y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) y : S)
inl :
  Membership.mem (γ := Submonoid M)
      (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) 1 →
    1 * y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (1 * y) : S)
inr :
  ∀ (hx : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) x : S)),
    x * y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * y) : S)
⊢ x * y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * y) : S)

Tactic:
rcases hx with rfl | hx

Premises used: rfl
-- 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 : CommMonoid S
inst_3 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) (v i)
y : M
h :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) y
hy : y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) y : S)
h_1 :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) 1
⊢ 1 * y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (1 * y) : S)

Tactic:
simpa
-- 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 : CommMonoid S
inst_3 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) (v i)
x y : M
h :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) x
h_1 :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) y
hy : y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) y : S)
hx : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) x : S)
inr :
  Membership.mem (γ := Submonoid M)
      (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) 1 →
    x * 1 = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * 1) : S)
inr₁ :
  ∀ (hy : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) y : S)),
    x * y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * y) : S)
⊢ x * y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * y) : S)

Tactic:
rcases hy with rfl | hy

Premises used: rfl
-- 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 : CommMonoid S
inst_3 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) (v i)
x : M
h :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) x
hx : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) x : S)
h_1 :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) 1
inr : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * 1) : S)
⊢ x * 1 = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * 1) : S)

Tactic:
right
-- 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 : CommMonoid S
inst_3 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) (v i)
x : M
h :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) x
hx : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) x : S)
h_1 :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) 1
⊢ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * 1) : S)

Tactic:
simpa
-- 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 : CommMonoid S
inst_3 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) (v i)
x y : M
h :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) x
h_1 :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) y
hx : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) x : S)
hy : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) y : S)
inr : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * y) : S)
⊢ x * y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * y) : S)

Tactic:
right