awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ x * y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * y) : S)
have 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)
Tactic: rcases hx with rfl | hx
Cleared hypotheses: x, h, hx
-- 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)
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)
⊢ x * y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * y) : S)
have 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)
Tactic: rcases hx with rfl | hx
Cleared hypotheses: hx
-- 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)
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)
⊢ x * y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * y) : S)
have 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)
Tactic: rcases hy with rfl | hy
Cleared hypotheses: y, h_1, hy
-- 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)
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)
⊢ x * y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * y) : S)
have 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)
Tactic: rcases hy with rfl | hy
Cleared hypotheses: hy
-- 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)
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
⊢ x * 1 = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * 1) : S)
have inr : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * 1) : S)
Tactic: right
-- 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)
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)
⊢ x * y = 1 ∨ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * y) : S)
have inr : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * y) : S)
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 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
⊢ Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
have inr : ∀
  (this :
    ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S]
      [inst_6 : InvolutiveInv ι] [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
      (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
      (hv_inv : v i⁻¹ = (v i)⁻¹)
      (hsp :
        Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
          Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
      (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
      Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S))
  (hi : v i ∉ closure (v '' s)), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
Tactic: wlog hi : v i ∈ closure (v '' s)
-- 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
inr :
  ∀
    (this :
      ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S]
        [inst_6 : InvolutiveInv ι] [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
        (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
        (hv_inv : v i⁻¹ = (v i)⁻¹)
        (hsp :
          Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
            Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
        (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
        Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S))
    (hi : v i ∉ closure (v '' s)), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
⊢ Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
have wlog : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S] [inst_6 : InvolutiveInv ι]
  [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
  (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
  (hv_inv : v i⁻¹ = (v i)⁻¹)
  (hsp :
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
      Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
  (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
  Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
Tactic: wlog hi : v i ∈ closure (v '' s)
Cleared hypotheses: inst_2, inst_3, inst_4, v, f, s, hf, i, hv_one, hv_inv, hsp
-- 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S]
    [inst_6 : InvolutiveInv ι] [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
    (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
    (hv_inv : v i⁻¹ = (v i)⁻¹)
    (hsp :
      Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
        Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
    (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
    Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi : v i ∉ closure (v '' s)
⊢ Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
have inr : ∀ (hi' : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
  Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
Tactic: rcases hsp with hi' | hi'
Cleared hypotheses: hsp
-- 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S]
    [inst_6 : InvolutiveInv ι] [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
    (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
    (hv_inv : v i⁻¹ = (v i)⁻¹)
    (hsp :
      Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
        Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
    (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
    Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi : v i ∉ closure (v '' s)
inr :
  ∀ (hi' : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
    Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
⊢ Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
have inr₁ : ∀ (hi' : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹),
  Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
Tactic: rcases hsp with hi' | hi'
Cleared hypotheses: hsp
-- 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S]
    [inst_6 : InvolutiveInv ι] [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
    (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
    (hv_inv : v i⁻¹ = (v i)⁻¹)
    (hsp :
      Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
        Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
    (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
    Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi : v i ∉ closure (v '' s)
hi' : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
⊢ Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i⁻¹) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i⁻¹)⁻¹
have h : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i⁻¹)
Tactic: left
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
⊢ Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
have suffices : v i ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
Tactic: suffices v i ≠ 1 → 1 < f (v i) from (this hv_one).ne'
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
⊢ v i ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
have refine : ∀ (x y : G),
  Membership.mem (γ := Submonoid G) (closure (v '' s)) x →
    Membership.mem (γ := Submonoid G) (closure (v '' s)) y →
      ∀ (hx : x ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) x : S))
        (hy : y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) y : S)),
        x * y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * y) : S)
Tactic: refine closure_induction (by simp_all) (by simp) (fun x y _ _ hx hy _ ↦ ?_) hi
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
x y : G
h : Membership.mem (γ := Submonoid G) (closure (v '' s)) x
h_1 : Membership.mem (γ := Submonoid G) (closure (v '' s)) y
hx : x ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) x : S)
hy : y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) y : S)
h_2 : x * y ≠ 1
⊢ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * y) : S)
have inl : Membership.mem (γ := Submonoid G) (closure (v '' s)) 1 →
  ∀ (hx : Ne.{u_3 + 1} (α := G) 1 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) 1 : S)),
    1 * y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (1 * y) : S)
Tactic: rcases eq_or_ne x 1 with rfl | hx'
Cleared hypotheses: x, h, hx, h_2
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
x y : G
h : Membership.mem (γ := Submonoid G) (closure (v '' s)) x
h_1 : Membership.mem (γ := Submonoid G) (closure (v '' s)) y
hx : x ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) x : S)
hy : y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) y : S)
h_2 : x * y ≠ 1
inl :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) 1 →
    ∀ (hx : Ne.{u_3 + 1} (α := G) 1 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) 1 : S)),
      1 * y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (1 * y) : S)
⊢ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * y) : S)
have inr : ∀ (hx' : x ≠ 1), LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * y) : S)
Tactic: rcases eq_or_ne x 1 with rfl | hx'
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
x y : G
h : Membership.mem (γ := Submonoid G) (closure (v '' s)) x
h_1 : Membership.mem (γ := Submonoid G) (closure (v '' s)) y
hx : x ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) x : S)
hy : y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) y : S)
h_2 : x * y ≠ 1
hx' : x ≠ 1
⊢ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * y) : S)
have inr : Membership.mem (γ := Submonoid G) (closure (v '' s)) 1 →
  ∀ (hy : Ne.{u_3 + 1} (α := G) 1 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) 1 : S)),
    x * 1 ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * 1) : S)
Tactic: rcases eq_or_ne y 1 with rfl | hy'
Cleared hypotheses: y, h_1, hy, h_2
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Indecomposable (goal)
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
x y : G
h : Membership.mem (γ := Submonoid G) (closure (v '' s)) x
h_1 : Membership.mem (γ := Submonoid G) (closure (v '' s)) y
hx : x ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) x : S)
hy : y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) y : S)
h_2 : x * y ≠ 1
hx' : x ≠ 1
inr :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) 1 →
    ∀ (hy : Ne.{u_3 + 1} (α := G) 1 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) 1 : S)),
      x * 1 ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * 1) : S)
⊢ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * y) : S)
have inr₁ : ∀ (hy' : y ≠ 1), LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * y) : S)
Tactic: rcases eq_or_ne y 1 with rfl | hy'
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (hypothesis)
Goal:
M : Type u_2
inst : Monoid M
x : M
n : ℕ
h : n + 2 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 2))
h₂ : ∀ ⦃a b : M⦄, x ^ (n + 2) = a * b → IsUnit a ∨ IsUnit b
⊢ False
have this : IsUnit (x ^ (n + 1)) ∨ IsUnit x
Tactic: have := h₂ (pow_succ _ _)
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (hypothesis)
Goal:
M : Type u_2
inst : Monoid M
x : M
n : ℕ
h : n + 2 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 2))
h₂ : ∀ ⦃a b : M⦄, x ^ (n + 2) = a * b → IsUnit a ∨ IsUnit b
this : IsUnit (x ^ (n + 1)) ∨ IsUnit x
⊢ False
have this₁ : IsUnit x
Tactic: rw [isUnit_pow_iff n.succ_ne_zero, or_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
⊢ Irreducible ((↑u : M) * y) ↔ Irreducible y
have simp : ¬IsUnit y → ((∀ ⦃a b : M⦄, (↑u : M) * y = a * b → IsUnit a ∨ IsUnit b) ↔ ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b)
Tactic: simp only [irreducible_iff, Units.isUnit_units_mul, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
⊢ ¬IsUnit y → ((∀ ⦃a b : M⦄, (↑u : M) * y = a * b → IsUnit a ∨ IsUnit b) ↔ ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b)
have refine_1 : ¬IsUnit y →
  ∀ (h : ∀ ⦃a b : M⦄, (↑u : M) * y = a * b → IsUnit a ∨ IsUnit b) (A B : M) (HAB : y = A * B), IsUnit A ∨ IsUnit B
Tactic: refine fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Irreducible.Lemmas (goal)
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
refine_1 :
  ¬IsUnit y →
    ∀ (h : ∀ ⦃a b : M⦄, (↑u : M) * y = a * b → IsUnit a ∨ IsUnit b) (A B : M) (HAB : y = A * B), IsUnit A ∨ IsUnit B
⊢ ¬IsUnit y → ((∀ ⦃a b : M⦄, (↑u : M) * y = a * b → IsUnit a ∨ IsUnit b) ↔ ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b)
have refine_2 : ¬IsUnit y →
  ∀ (h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b) (A B : M) (HAB : (↑u : M) * y = A * B), IsUnit A ∨ IsUnit B
Tactic: refine fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩