awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (hypothesis)
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)
⊢ v '' univ ⊆ (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)
have 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)})
Tactic: have : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1} := by ext i; simp [(hf i).symm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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 '' univ ⊆ (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)
have 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)
Tactic: rw [this, image_union, union_subset_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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)
have 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)
Tactic: refine ⟨le_trans ?_ (le_closure_toSubmonoid (v '' IsMulIndecomposable.baseOf v f)), ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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)
⊢ 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)
have 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)
Tactic: refine ⟨le_trans ?_ (le_closure_toSubmonoid (v '' IsMulIndecomposable.baseOf v f)), ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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
have rw : Function.comp (β := G) (⇑invMonoidHom : (a : G) → G) (⇑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]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (hypothesis)
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
⊢ v '' {i : ι | LT.lt.{u_4} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)} ⊆
    (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)
have h₁ : (⇑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
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (hypothesis)
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)} ⊆
    (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)
have 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)}
Tactic: have h₂ : v '' {i | f (v i) < 1} = v '' {i | 1 < f' (v i)} := by simp [f']
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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) ((f : (a : G) → S) (v i) : S) (1 : S)} ⊆
    (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)
have 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)
Tactic: rw [h₂, ← h₁, image_comp, coe_invMonoidHom, image_inv_eq_inv, closure_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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)
have 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)
Tactic: refine le_trans ?_ (le_closure_toSubmonoid (v '' IsMulIndecomposable.baseOf v f'))
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (hypothesis)
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.Pairwise fun (i j : ι) ↦ v i / v j ∉ range v
have h_sub : s ⊆ t
Tactic: have h_sub : s ⊆ t := hst.trans (IsMulIndecomposable.subset _ _)
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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
⊢ v i / v j ∉ range v
have by_contra! : ∀ (k : ι) (hk : v k = v i / v j), False
Tactic: by_contra! ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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
⊢ False
have inl : ∀ (hk' : k ∈ t), False
Tactic: rcases hv_t k with hk' | hk'
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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
⊢ False
have inr : ∀ (hk' : k⁻¹ ∈ t), False
Tactic: rcases hv_t k with hk' | hk'
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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
⊢ False
have inl : ¬IsMulIndecomposable v t i
Tactic: suffices ¬ IsMulIndecomposable v t i from this (hst hi)
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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
⊢ ¬IsMulIndecomposable v t i
have inl : i ∈ t → ∃ (x : ι) (_ : x ∈ t) (x_1 : ι) (_ : x_1 ∈ t), v i = v x * v x_1
Tactic: simp only [IsMulIndecomposable, hv_one, or_self, imp_false, not_and, not_forall, not_not]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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
⊢ False
have inr : ¬IsMulIndecomposable v t j
Tactic: suffices ¬ IsMulIndecomposable v t j from this (hst hj)
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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
⊢ ¬IsMulIndecomposable v t j
have inr : j ∈ t → ∃ (x : ι) (_ : x ∈ t) (x_1 : ι) (_ : x_1 ∈ t), v j = v x * v x_1
Tactic: simp only [IsMulIndecomposable, hv_one, or_self, imp_false, not_and, not_forall, not_not]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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
have contrapose! : ∀ (hf : v i = 1), ∃ (i : ι), Eq.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
Tactic: contrapose! hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (hypothesis)
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}
⊢ s.Pairwise fun (i j : ι) ↦ v i / v j ∉ range v
have hv_one : ∀ (i : ι), v i ≠ 1
Tactic: have hv_one : ∀ i, v i ≠ 1 := fun i ↦ by contrapose! hf; exact ⟨i, by simp [hf]⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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
⊢ s.Pairwise fun (i j : ι) ↦ v i / v j ∉ range v
have 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⁻¹
Tactic: apply pairwise_div_notMem_range v hv_one hv_inv s {i | 1 < f (v i)} hst fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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)⁻¹
⊢ Membership.mem (γ := Submonoid G) (Submonoid.closure (v '' baseOf v f)) (v i) ∨
    Membership.mem (γ := Submonoid G) (Submonoid.closure (v '' baseOf v f)) (v i)⁻¹
have 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)⁻¹
Tactic: rw [Submonoid.closure_image_isMulIndecomposable_baseOf v f]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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)⁻¹
⊢ 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)⁻¹
have 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)⁻¹
Tactic: rcases lt_or_gt_of_ne hi with hj | hj
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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)⁻¹
⊢ 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)⁻¹
have 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)⁻¹
Tactic: rcases lt_or_gt_of_ne hi with hj | hj
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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) ∨
    Membership.mem (γ := Submonoid G)
      (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i)⁻¹
have 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)⁻¹
Tactic: right
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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) ∨
    Membership.mem (γ := Submonoid G)
      (Submonoid.closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)})) (v i)⁻¹
have 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)
Tactic: left
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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)
have 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)
Tactic: refine ⟨fun hi ↦ ?_, fun hi ↦ subset_closure <| mem_image_of_mem v hi⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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)
⊢ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
have suffices : v i = 1 ∨ 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
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
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)
⊢ v i = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
have 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)
Tactic: refine closure_induction (by grind) (by simp) (fun x y _ _ hx hy ↦ ?_) hi