awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a_1 b_1 : α
G : Type u_1
inst_1 : Group G
a b : G
⊢ a * b⁻¹ * b = a

Tactic:
inv_mul_cancel_right a b

Premises used: inv_mul_cancel_right
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible b
⊢ a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * b = a

Tactic:
invOf_mul_cancel_right' _ _

Premises used: invOf_mul_cancel_right'
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
x : Invertible b
⊢ a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ = a

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a_1 b_1 : α
G : Type u_1
inst_1 : Group G
a b : G
⊢ a * b * b⁻¹ = a

Tactic:
mul_inv_cancel_right a b

Premises used: mul_inv_cancel_right
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible b
⊢ a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ = a

Tactic:
mul_invOf_cancel_right' _ _

Premises used: mul_invOf_cancel_right'
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
hac : a * b = 1
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = b

Tactic:
left_inv_eq_right_inv (invOf_mul_self _) hac

Premises used: invOf_mul_self, left_inv_eq_right_inv
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
hac : b * a = 1
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = b

Tactic:
(left_inv_eq_right_inv hac (mul_invOf_self _)).symm

Premises used: mul_invOf_self, left_inv_eq_right_inv, Eq.symm
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
h : @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = b
rw : a * @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = 1
rw₁ rw₂ : Eq.{u + 1} (α := α) 1 1
⊢ a * b = 1

Tactic:
rw [← h, mul_invOf_self]

Premises used: mul_invOf_self
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
h : @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = b
rw : @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * a = 1
rw₁ rw₂ : Eq.{u + 1} (α := α) 1 1
⊢ b * a = 1

Tactic:
rw [← h, invOf_mul_self]

Premises used: invOf_mul_self
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible b
h : a = b
hac : a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ = 1
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = @Invertible.invOf _ MulOne.toMul MulOne.toOne b _

Tactic:
apply invOf_eq_right_inv

Premises used: invOf_eq_right_inv
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible b
h : a = b
hac : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ = 1
hac₁ hac₂ : Eq.{u + 1} (α := α) 1 1
⊢ a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ = 1

Tactic:
rw [h, mul_invOf_self]

Premises used: mul_invOf_self
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b_1 : α
x x_1 : Invertible a
b : α
hba : b * a = 1
hab : a * b = 1
c : α
invOf_mul_self : c * a = 1
hac : a * c = 1
e_invOf : b = c
⊢ { invOf := b, invOf_mul_self := hba, mul_invOf_self := hab : Invertible a } =
    { invOf := c, invOf_mul_self := invOf_mul_self, mul_invOf_self := hac }

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b_1 : α
x x_1 : Invertible a
b : α
hba : b * a = 1
hab : a * b = 1
c : α
invOf_mul_self : c * a = 1
hac : a * c = 1
⊢ b = c

Tactic:
left_inv_eq_right_inv hba hac

Premises used: left_inv_eq_right_inv
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b_1 : α
x x_1 : Invertible a
b : α
hba : b * a = 1
hab : a * b = 1
c : α
invOf_mul_self : c * a = 1
hac : a * c = 1
⊢ b = c

Tactic:
exact left_inv_eq_right_inv hba hac

Premises used: left_inv_eq_right_inv
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible b
h : a = b
⊢ @invOf _ MulOne.toMul MulOne.toOne a _ = @invOf _ MulOne.toMul MulOne.toOne b _

Tactic:
invertible_unique a b h

Premises used: invertible_unique
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = @invOf _ MulOne.toMul MulOne.toOne r _
rw : si * r = 1
rw₁ : @invOf _ MulOne.toMul MulOne.toOne r _ * r = 1
rw₂ rw₃ : Eq.{u + 1} (α := α) 1 1
⊢ si * s = 1

Tactic:
rw [hs, hsi, invOf_mul_self]

Premises used: Invertible.invOf_mul_self
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = @invOf _ MulOne.toMul MulOne.toOne r _
rw : r * si = 1
rw₁ : r * @invOf _ MulOne.toMul MulOne.toOne r _ = 1
rw₂ rw₃ : Eq.{u + 1} (α := α) 1 1
⊢ s * si = 1

Tactic:
rw [hs, hsi, mul_invOf_self]

Premises used: Invertible.mul_invOf_self
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Group α
a : α
inst_1 : Invertible a
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = a⁻¹

Tactic:
invOf_eq_right_inv (mul_inv_cancel a)

Premises used: invOf_eq_right_inv, mul_inv_cancel
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
x : Invertible (α := α) 1
⊢ Eq.{u + 1} (α := α) (@Invertible.invOf _ MulOne.toMul MulOne.toOne 1 _) 1

Tactic:
invOf_eq_right_inv (mul_one _)

Premises used: invOf_eq_right_inv, mul_one
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
inst_1 : Invertible (α := α) 1
⊢ Eq.{u + 1} (α := α) (@Invertible.invOf _ MulOne.toMul MulOne.toOne 1 _) 1

Tactic:
invOf_one'

Premises used: invOf_one'
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a : α
inst_1 : Invertible a
inst_2 : Invertible (@Invertible.invOf _ MulOne.toMul MulOne.toOne a _)
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne (@Invertible.invOf _ MulOne.toMul MulOne.toOne a _) _ = a

Tactic:
invOf_eq_right_inv (invOf_mul_self _)

Premises used: invOf_eq_right_inv, invOf_mul_self
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible b
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ ↔ a = b

Tactic:
⟨invertible_unique _ _, invertible_unique _ _⟩

Premises used: invertible_unique, Iff.intro
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible b
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * (a * b) = 1

Tactic:
simp [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible b
⊢ a * b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * @Invertible.invOf _ MulOne.toMul MulOne.toOne a _) = 1

Tactic:
simp [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible b
inst_3 : Invertible (a * b)
⊢ a * b * (@Invertible.invOf _ MulOne.toMul MulOne.toOne b _ * @Invertible.invOf _ MulOne.toMul MulOne.toOne a _) = 1

Tactic:
simp [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b c : α
inst_1 : Invertible c
h : a * c = b * c
⊢ a = b

Tactic:
simpa using congr_arg (· * ⅟c) h

Premises used: HMul.hMul, Invertible.invOf, congr_arg
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b c : α
inst_1 : Invertible c
h : c * a = c * b
⊢ a = b

Tactic:
simpa using congr_arg (⅟c * ·) h

Premises used: HMul.hMul, Invertible.invOf, congr_arg
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b c : α
inst_1 : Invertible c
rw : c * (@Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * a) = c * b ↔ a = c * b
rw₁ rw₂ : a = c * b ↔ a = c * b
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * a = b ↔ a = c * b

Tactic:
rw [← mul_right_inj_of_invertible (c := c), mul_invOf_cancel_left]

Premises used: mul_right_inj_of_invertible, mul_invOf_cancel_left
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b c : α
inst_1 : Invertible c
rw :
  @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * (c * a) = @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * b ↔
    a = @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * b
rw₁ rw₂ :
  a = @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * b ↔ a = @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * b
⊢ c * a = b ↔ a = @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * b

Tactic:
rw [← mul_right_inj_of_invertible (c := ⅟c), invOf_mul_cancel_left]

Premises used: invOf_mul_cancel_left, Invertible.invOf, mul_right_inj_of_invertible
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b c : α
inst_1 : Invertible c
rw : a * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * c = b * c ↔ a = b * c
rw₁ rw₂ : a = b * c ↔ a = b * c
⊢ a * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ = b ↔ a = b * c

Tactic:
rw [← mul_left_inj_of_invertible (c := c), invOf_mul_cancel_right]

Premises used: mul_left_inj_of_invertible, invOf_mul_cancel_right
-- Module: Mathlib.Algebra.Group.Invertible.Defs
Goal:
α : Type u
inst : Monoid α
a b c : α
inst_1 : Invertible c
rw :
  a * c * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ = b * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ ↔
    a = b * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _
rw₁ rw₂ :
  a = b * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ ↔ a = b * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _
⊢ a * c = b ↔ a = b * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _

Tactic:
rw [← mul_left_inj_of_invertible (c := ⅟c), mul_invOf_cancel_right]

Premises used: mul_left_inj_of_invertible, mul_invOf_cancel_right, Invertible.invOf
-- Module: Mathlib.Algebra.Group.Irreducible.Defs
Goal:
M : Type u_1
inst : Monoid M
⊢ ¬Irreducible.{u_1} (M := M) 1

Tactic:
simp [irreducible_iff]

Premises used: irreducible_iff
-- Module: Mathlib.Algebra.Group.Irreducible.Defs
Goal:
M : Type u_1
inst : Monoid M
hp : Irreducible.{u_1} (M := M) 1
⊢ False

Tactic:
not_irreducible_one hp

Premises used: not_irreducible_one
-- Module: Mathlib.Algebra.Group.Irreducible.Defs
Goal:
M : Type u_1
inst : Monoid M
hp : Irreducible.{u_1} (M := M) 1
⊢ False

Tactic:
exact not_irreducible_one hp

Premises used: not_irreducible_one
-- Module: Mathlib.Algebra.Group.Irreducible.Defs
Goal:
M : Type u_1
inst : Monoid M
p : M
hp : ¬IsUnit p
⊢ Irreducible p ∨ ∃ (a : M), ∃ (b : M), ¬IsUnit a ∧ ¬IsUnit b ∧ p = a * b

Tactic:
simpa [irreducible_iff, hp, and_rotate] using em (∀ a b, p = a * b → IsUnit a ∨ IsUnit b)

Premises used: em, irreducible_iff, and_rotate
-- Module: Mathlib.Algebra.Group.Irreducible.Defs
Goal:
M : Type u_1
inst : Monoid M
a b : M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
hab : Irreducible (a * b)
⊢ a = 1 ∨ b = 1

Tactic:
simpa using hab.isUnit_or_isUnit rfl

Premises used: Irreducible.isUnit_or_isUnit, rfl
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
M : Type u_2
inst : Monoid M
v : ι → M
s : Set ι
⊢ {i : ι | IsMulIndecomposable v s i} ⊆ s

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
M : Type u_2
inst : Monoid M
inst_1 : Subsingleton.{u_2 + 1} Mˣ
x : M
hx : x ≠ 1
h : IsMulIndecomposable id univ x
⊢ ¬IsUnit x

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
M : Type u_2
inst : Monoid M
inst_1 : Subsingleton.{u_2 + 1} Mˣ
x : M
hx : x ≠ 1
h : IsMulIndecomposable id univ x
⊢ ∀ ⦃a b : M⦄, x = a * b → IsUnit a ∨ IsUnit b

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
M : Type u_2
inst : Monoid M
inst_1 : Subsingleton.{u_2 + 1} Mˣ
x : M
hx : x ≠ 1
h : Irreducible x
⊢ IsMulIndecomposable id univ x

Tactic:
simpa using h.isUnit_or_isUnit

Premises used: Irreducible.isUnit_or_isUnit
-- 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 : Monoid S
v : ι → M
f : M →* S
⊢ baseOf v f ⊆ {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)}

Tactic:
IsMulIndecomposable.subset _ _

Premises used: IsMulIndecomposable.subset, 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 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
this :
  ∀ (f : G →* S),
    v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f) ⊆
      (⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f
apply :
  (⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f ⊆
    v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f)
⊢ v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f) =
    (⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f

Tactic:
apply subset_antisymm (this f)

Premises used: subset_antisymm
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
this :
  ∀ (f : G →* S),
    v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f) ⊆
      (⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f
⊢ Subset (α := Set G)
    ((⇑invMonoidHom : (a : G) → G) ''
      v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom (MonoidHom.comp invMonoidHom f)))
    (image (α := G) (⇑invMonoidHom : (a : G) → G)
      ((⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f : G →* S)))

Tactic:
replace this := image_mono (f := invMonoidHom) <| this (invMonoidHom.comp f)
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
this :
  Subset (α := Set G)
    ((⇑invMonoidHom : (a : G) → G) ''
      v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom (MonoidHom.comp invMonoidHom f)))
    (image (α := G) (⇑invMonoidHom : (a : G) → G)
      ((⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f : G →* S)))
⊢ Subset (α := Set G) ((⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f)
    ((⇑(MonoidHom.id G) : (a : G) → G) ''
      v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f : G →* S))

Tactic:
rw [← MonoidHom.comp_assoc, invMonoidHom_comp_invMonoidHom, MonoidHom.id_comp, image_comp,
      ← image_comp invMonoidHom invMonoidHom, ← MonoidHom.coe_comp, invMonoidHom_comp_invMonoidHom,
      ← image_comp] at this

Premises used: MonoidHom.coe_comp, invMonoidHom, MonoidHom.comp_assoc, invMonoidHom_comp_invMonoidHom, MonoidHom.id_comp, Set.image_comp, 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
this :
  Subset (α := Set G) ((⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f)
    ((⇑(MonoidHom.id G) : (a : G) → G) ''
      v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f : G →* S))
⊢ (⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f ⊆
    v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f)

Tactic:
simpa using this
-- 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
suffices :
  ∀ (f : G →* S),
    v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f) ⊆
      (⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f
⊢ v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f) =
    (⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f

Tactic:
suffices ∀ (f : G →* S),
      v '' baseOf v (invMonoidHom.comp f) ⊆ (invMonoidHom ∘ v) '' baseOf v f by
    apply subset_antisymm (this f)
    replace this := image_mono (f := invMonoidHom) <| this (invMonoidHom.comp f)
    rw [← MonoidHom.comp_assoc, invMonoidHom_comp_invMonoidHom, MonoidHom.id_comp, image_comp,
      ← image_comp invMonoidHom invMonoidHom, ← MonoidHom.coe_comp, invMonoidHom_comp_invMonoidHom,
      ← image_comp] at this
    simpa using this
-- 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
i : ι
hi :
  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
⊢ Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} i⁻¹

Tactic:
simpa [hv_inv] using 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 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi :
  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
⊢ ((⇑invMonoidHom : (a : G) → G) ∘ v) i⁻¹ = v i

Tactic:
simp [hv_inv]
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi :
  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
refine :
  ∀ (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
⊢ Membership.mem (γ := Set G) ((⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f) (v i)

Tactic:
refine ⟨i⁻¹, ⟨by simpa [hv_inv] using hi, fun j hj k hk hi ↦ ?_⟩, by simp [hv_inv]⟩
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : 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⁻¹
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (hi : v i = v j⁻¹ * v k⁻¹), 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

Premises used: mul_inv, inv_eq_iff_eq_inv
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : 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 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
-- 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
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⁻¹
⊢ Membership.mem (γ := Set ι)
    {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} j⁻¹

Tactic:
simpa [hv_inv]