awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i : ι
hi_1 :
  Membership.mem (γ := Set ι)
    {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} i
hi' :
  ∀ (j : ι),
    Membership.mem (γ := Set ι)
        {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} j →
      ∀ (k : ι),
        Membership.mem (γ := Set ι)
            {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} k →
          v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j
k : ι
hk : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} k
hi : v i⁻¹ = v j * v k
rwa : ∀ (hi : (v i)⁻¹ = v j * v k), v i = v j⁻¹ * v k⁻¹
⊢ v i = v j⁻¹ * v k⁻¹
have rwa₁ : ∀ (hi : v i = (v j * v k)⁻¹), v i = v j⁻¹ * v k⁻¹
Tactic: rwa [hv_inv, inv_eq_iff_eq_inv, mul_inv, ← hv_inv, ← hv_inv] at hi
Cleared hypotheses: hi
-- 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
i : ι
hi_1 :
  Membership.mem (γ := Set ι)
    {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} i
hi' :
  ∀ (j : ι),
    Membership.mem (γ := Set ι)
        {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} j →
      ∀ (k : ι),
        Membership.mem (γ := Set ι)
            {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} k →
          v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j
k : ι
hk : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} k
hi : v i⁻¹ = v j * v k
rwa : ∀ (hi : (v i)⁻¹ = v j * v k), v i = v j⁻¹ * v k⁻¹
rwa₁ : ∀ (hi : v i = (v j * v k)⁻¹), v i = v j⁻¹ * v k⁻¹
⊢ v i = v j⁻¹ * v k⁻¹
have rwa₂ : ∀ (hi : v i = (v j)⁻¹ * (v k)⁻¹), v i = v j⁻¹ * v k⁻¹
Tactic: rwa [hv_inv, inv_eq_iff_eq_inv, mul_inv, ← hv_inv, ← hv_inv] at hi
Cleared hypotheses: hi
-- 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
i : ι
hi_1 :
  Membership.mem (γ := Set ι)
    {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} i
hi' :
  ∀ (j : ι),
    Membership.mem (γ := Set ι)
        {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} j →
      ∀ (k : ι),
        Membership.mem (γ := Set ι)
            {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} k →
          v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j
k : ι
hk : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} k
hi : v i⁻¹ = v j * v k
rwa : ∀ (hi : (v i)⁻¹ = v j * v k), v i = v j⁻¹ * v k⁻¹
rwa₁ : ∀ (hi : v i = (v j * v k)⁻¹), v i = v j⁻¹ * v k⁻¹
rwa₂ : ∀ (hi : v i = (v j)⁻¹ * (v k)⁻¹), v i = v j⁻¹ * v k⁻¹
⊢ v i = v j⁻¹ * v k⁻¹
have rwa₃ : ∀ (hi : v i = v j⁻¹ * (v k)⁻¹), v i = v j⁻¹ * v k⁻¹
Tactic: rwa [hv_inv, inv_eq_iff_eq_inv, mul_inv, ← hv_inv, ← hv_inv] at hi
Cleared hypotheses: hi
-- 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
i : ι
hi_1 :
  Membership.mem (γ := Set ι)
    {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} i
hi' :
  ∀ (j : ι),
    Membership.mem (γ := Set ι)
        {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} j →
      ∀ (k : ι),
        Membership.mem (γ := Set ι)
            {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} k →
          v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j
k : ι
hk : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} k
hi : v i⁻¹ = v j * v k
rwa : ∀ (hi : (v i)⁻¹ = v j * v k), v i = v j⁻¹ * v k⁻¹
rwa₁ : ∀ (hi : v i = (v j * v k)⁻¹), v i = v j⁻¹ * v k⁻¹
rwa₂ : ∀ (hi : v i = (v j)⁻¹ * (v k)⁻¹), v i = v j⁻¹ * v k⁻¹
rwa₃ : ∀ (hi : v i = v j⁻¹ * (v k)⁻¹), v i = v j⁻¹ * v k⁻¹
⊢ v i = v j⁻¹ * v k⁻¹
have rwa₄ : ∀ (hi : v i = v j⁻¹ * v k⁻¹), v i = v j⁻¹ * v k⁻¹
Tactic: rwa [hv_inv, inv_eq_iff_eq_inv, mul_inv, ← hv_inv, ← hv_inv] at hi
Cleared hypotheses: hi
-- 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
i : ι
hi_1 :
  Membership.mem (γ := Set ι)
    {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} i
hi' :
  ∀ (j : ι),
    Membership.mem (γ := Set ι)
        {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} j →
      ∀ (k : ι),
        Membership.mem (γ := Set ι)
            {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} k →
          v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j
k : ι
hk : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} k
hi : v i⁻¹ = v j * v k
⊢ v j = 1 ∨ v k = 1
have hi₁ : v i = v j⁻¹ * v k⁻¹
Tactic: replace hi : v i = v j⁻¹ * v k⁻¹ := by
    rwa [hv_inv, inv_eq_iff_eq_inv, mul_inv, ← hv_inv, ← hv_inv] at hi
Cleared hypotheses: hi
-- 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
i : ι
hi_1 :
  Membership.mem (γ := Set ι)
    {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} i
hi' :
  ∀ (j : ι),
    Membership.mem (γ := Set ι)
        {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} j →
      ∀ (k : ι),
        Membership.mem (γ := Set ι)
            {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} k →
          v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j
k : ι
hk : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} k
hi : v i = v j⁻¹ * v k⁻¹
⊢ v j = 1 ∨ v k = 1
have hi'₁ : v j⁻¹ = 1 ∨ v k⁻¹ = 1
Tactic: specialize hi' j⁻¹ (by simpa [hv_inv]) k⁻¹ (by simpa [hv_inv]) hi
Cleared hypotheses: 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
⊢ Eq (α := Submonoid M) (closure (v '' IsMulIndecomposable.baseOf v f))
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)}))
have refine : v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)} ⊆
  (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set M)
Tactic: refine le_antisymm (closure_mono (image_mono <| IsMulIndecomposable.baseOf_subset_one_lt v f))
    (closure_le.mpr ?_)
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hi : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
⊢ v i ∈ (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set M)
have by_contra : ∀ (hi' : v i ∉ (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set M)), False
Tactic: by_contra hi'
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (hypothesis)
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
i : ι
hi : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi' : v i ∉ (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set M)
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)}
⊢ False
have hne : s.Nonempty
Tactic: have hne : s.Nonempty := ⟨i, hi, 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 : 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
⊢ False
have obtain : ∀ (i : ι) (hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i), False
Tactic: obtain ⟨i, hi⟩ := s.toFinite.exists_minimalFor (f ∘ v) s hne
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (hypothesis)
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
⊢ False
have hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
Tactic: have ⟨(hi₀ : 1 < f (v i)), (hi₁ : v i ∉ _)⟩ : i ∈ s := hi.prop
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (hypothesis)
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)
⊢ False
have hi₁ : v i ∉ closure (v '' t)
Tactic: have ⟨(hi₀ : 1 < f (v i)), (hi₁ : v i ∉ _)⟩ : i ∈ s := hi.prop
-- 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 : 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)
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)
have by_contra : ∀ (hk₂ : v k ∉ closure (v '' t)), False
Tactic: by_contra hk₂
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (hypothesis)
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)
⊢ False
have 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)
Tactic: have hi₂ (k : ι) (hk₀ : 1 < f (v k)) (hk₁ : f (v k) < f (v i)) : v k ∈ closure (v '' t) := by
    by_contra hk₂; exact not_le.mpr hk₁ <| hi.le_of_le ⟨hk₀, hk₂⟩ hk₁.le
-- 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 : 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)
⊢ i ∉ t
have contrapose : ∀ (hi₁ : i ∈ t), Membership.mem (γ := Submonoid M) (closure (v '' t)) (v i)
Tactic: contrapose hi₁
Cleared hypotheses: hi₁
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (hypothesis)
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)
⊢ False
have hi₃ : i ∉ t
Tactic: have hi₃ : i ∉ t := by contrapose hi₁; exact 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 : 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
⊢ False
have obtain : ∀ (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), False
Tactic: obtain ⟨j, k, hj, hk, hjk⟩ : ∃ (j k : ι) (hj : 1 < f (v j)) (hk : 1 < f (v k)),
      v i = v j * v k := by
    grind [IsMulIndecomposable]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (hypothesis)
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
⊢ False
have hj' : Membership.mem (γ := Submonoid M) (closure (v '' t)) (v j)
Tactic: have hj' : v j ∈ closure (v '' t) := hi₂ j hj <| by aesop
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (hypothesis)
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)
⊢ False
have hk' : Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
Tactic: have hk' : v k ∈ closure (v '' t) := hi₂ k hk <| by aesop
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (hypothesis)
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)
⊢ False
have hjk₁ : Membership.mem (γ := Submonoid M) (closure (v '' t)) (v i)
Tactic: replace hjk : v i ∈ closure (v '' t) := hjk ▸ mul_mem hj' hk'
Cleared hypotheses: hjk
-- 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)
⊢ Eq (α := Subgroup G) (closure (v '' IsMulIndecomposable.baseOf v f)) (closure (range v))
have rw : Eq (α := Subgroup G) (closure (v '' IsMulIndecomposable.baseOf v f)) (closure (v '' univ))
Tactic: rw [← image_univ]
-- 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)
⊢ Eq (α := Subgroup G) (closure (v '' IsMulIndecomposable.baseOf v f)) (closure (v '' univ))
have refine : v '' univ ⊆ (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set G)
Tactic: refine le_antisymm (closure_mono (image_mono <| by simp)) ((closure_le _).mpr ?_)
-- 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)
⊢ 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)})
have 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
Tactic: ext i