awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible (a * b)
inst_2 : Invertible b
rw : a * b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _ = 1
⊢ a * (b * @Invertible.invOf _ MulOne.toMul MulOne.toOne (a * b) _) = 1
have rw₁ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [← mul_assoc, mul_invOf_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
m : α
inst_1 : Invertible m
n : ℕ
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne m _ ^ n * m ^ n = 1
have rw : (@Invertible.invOf _ MulOne.toMul MulOne.toOne m _ * m) ^ n = 1
Tactic: rw [← (commute_invOf m).symm.mul_pow, invOf_mul_self, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
m : α
inst_1 : Invertible m
n : ℕ
rw : (@Invertible.invOf _ MulOne.toMul MulOne.toOne m _ * m) ^ n = 1
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne m _ ^ n * m ^ n = 1
have rw₁ : HPow.hPow (α := α) 1 n = 1
Tactic: rw [← (commute_invOf m).symm.mul_pow, invOf_mul_self, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
m : α
inst_1 : Invertible m
n : ℕ
rw : (@Invertible.invOf _ MulOne.toMul MulOne.toOne m _ * m) ^ n = 1
rw₁ : HPow.hPow (α := α) 1 n = 1
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne m _ ^ n * m ^ n = 1
have rw₂ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [← (commute_invOf m).symm.mul_pow, invOf_mul_self, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
m : α
inst_1 : Invertible m
n : ℕ
⊢ m ^ n * @Invertible.invOf _ MulOne.toMul MulOne.toOne m _ ^ n = 1
have rw : (m * @Invertible.invOf _ MulOne.toMul MulOne.toOne m _) ^ n = 1
Tactic: rw [← (commute_invOf m).mul_pow, mul_invOf_self, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
m : α
inst_1 : Invertible m
n : ℕ
rw : (m * @Invertible.invOf _ MulOne.toMul MulOne.toOne m _) ^ n = 1
⊢ m ^ n * @Invertible.invOf _ MulOne.toMul MulOne.toOne m _ ^ n = 1
have rw₁ : HPow.hPow (α := α) 1 n = 1
Tactic: rw [← (commute_invOf m).mul_pow, mul_invOf_self, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
inst : Monoid α
m : α
inst_1 : Invertible m
n : ℕ
rw : (m * @Invertible.invOf _ MulOne.toMul MulOne.toOne m _) ^ n = 1
rw₁ : HPow.hPow (α := α) 1 n = 1
⊢ m ^ n * @Invertible.invOf _ MulOne.toMul MulOne.toOne m _ ^ n = 1
have rw₂ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [← (commute_invOf m).mul_pow, mul_invOf_self, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst : MulOneClass R
inst_1 : MulOneClass S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
f : F
r : R
inst_4 : Invertible r
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (@invOf _ MulOne.toMul MulOne.toOne r _) : S)
      ((f : (a : R) → S) r : S) =
    1
have rw : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (@invOf _ MulOne.toMul MulOne.toOne r _ * r) : S) (1 : S)
Tactic: rw [← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst : MulOneClass R
inst_1 : MulOneClass S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
f : F
r : R
inst_4 : Invertible r
rw : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (@invOf _ MulOne.toMul MulOne.toOne r _ * r) : S) (1 : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (@invOf _ MulOne.toMul MulOne.toOne r _) : S)
      ((f : (a : R) → S) r : S) =
    1
have rw₁ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
Tactic: rw [← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst : MulOneClass R
inst_1 : MulOneClass S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
f : F
r : R
inst_4 : Invertible r
rw : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (@invOf _ MulOne.toMul MulOne.toOne r _ * r) : S) (1 : S)
rw₁ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (@invOf _ MulOne.toMul MulOne.toOne r _) : S)
      ((f : (a : R) → S) r : S) =
    1
have rw₂ : Eq.{u_2 + 1} (α := S) 1 1
Tactic: rw [← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst : MulOneClass R
inst_1 : MulOneClass S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
f : F
r : R
inst_4 : Invertible r
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) r : S)
      ((f : (a : R) → S) (@invOf _ MulOne.toMul MulOne.toOne r _) : S) =
    1
have rw : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (r * @invOf _ MulOne.toMul MulOne.toOne r _) : S) (1 : S)
Tactic: rw [← map_mul, mul_invOf_self, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst : MulOneClass R
inst_1 : MulOneClass S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
f : F
r : R
inst_4 : Invertible r
rw : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (r * @invOf _ MulOne.toMul MulOne.toOne r _) : S) (1 : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) r : S)
      ((f : (a : R) → S) (@invOf _ MulOne.toMul MulOne.toOne r _) : S) =
    1
have rw₁ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
Tactic: rw [← map_mul, mul_invOf_self, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst : MulOneClass R
inst_1 : MulOneClass S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
f : F
r : R
inst_4 : Invertible r
rw : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (r * @invOf _ MulOne.toMul MulOne.toOne r _) : S) (1 : S)
rw₁ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) r : S)
      ((f : (a : R) → S) (@invOf _ MulOne.toMul MulOne.toOne r _) : S) =
    1
have rw₂ : Eq.{u_2 + 1} (α := S) 1 1
Tactic: rw [← map_mul, mul_invOf_self, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : MulOneClass R
inst_1 : Monoid S
inst_2 : FunLike F R S
inst_3 : MonoidHomClass F R S
f : F
r : R
inst_4 : Invertible r
ifr : Invertible (α := S) ((f : (a : R) → S) r : S)
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (@Invertible.invOf _ MulOne.toMul MulOne.toOne r _) : S)
    (@Invertible.invOf _ MulOne.toMul MulOne.toOne ((f : (a : R) → S) r) _ : S)
have obtain : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (@Invertible.invOf _ MulOne.toMul MulOne.toOne r _) : S)
  (@Invertible.invOf _ MulOne.toMul MulOne.toOne ((f : (a : R) → S) r) _ : S)
Tactic: obtain rfl : ifr = Invertible.map f r := Subsingleton.elim _ _
Cleared hypotheses: ifr
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
x : Invertible a
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * (a * b) = b
have rw : @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * a * b = b
Tactic: rw [← mul_assoc, invOf_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
x : Invertible a
rw : @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * a * b = b
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * (a * b) = b
have rw₁ : 1 * b = b
Tactic: rw [← mul_assoc, invOf_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
x : Invertible a
rw : @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * a * b = b
rw₁ : 1 * b = b
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * (a * b) = b
have rw₂ : b = b
Tactic: rw [← mul_assoc, invOf_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
x : Invertible a
⊢ a * (@Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * b) = b
have rw : a * @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * b = b
Tactic: rw [← mul_assoc, mul_invOf_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
x : Invertible a
rw : a * @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * b = b
⊢ a * (@Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * b) = b
have rw₁ : 1 * b = b
Tactic: rw [← mul_assoc, mul_invOf_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
x : Invertible a
rw : a * @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * b = b
rw₁ : 1 * b = b
⊢ a * (@Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * b) = b
have rw₂ : b = b
Tactic: rw [← mul_assoc, mul_invOf_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
h : @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = b
⊢ a * b = 1
have rw : a * @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = 1
Tactic: rw [← h, mul_invOf_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
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
⊢ a * b = 1
have rw₁ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [← h, mul_invOf_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
h : @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = b
⊢ b * a = 1
have rw : @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * a = 1
Tactic: rw [← h, invOf_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
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
⊢ b * a = 1
have rw₁ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [← h, invOf_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible b
h : a = b
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = @Invertible.invOf _ MulOne.toMul MulOne.toOne b _
have hac : a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ = 1
Tactic: apply invOf_eq_right_inv
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
inst_1 : Invertible a
inst_2 : Invertible b
h : a = b
⊢ a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ = 1
have hac : b * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ = 1
Tactic: rw [h, mul_invOf_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
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
⊢ a * @Invertible.invOf _ MulOne.toMul MulOne.toOne b _ = 1
have hac₁ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [h, mul_invOf_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
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
⊢ { invOf := b, invOf_mul_self := hba, mul_invOf_self := hab : Invertible a } =
    { invOf := c, invOf_mul_self := invOf_mul_self, mul_invOf_self := hac }
have e_invOf : b = c
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = @invOf _ MulOne.toMul MulOne.toOne r _
⊢ si * s = 1
have rw : si * r = 1
Tactic: rw [hs, hsi, invOf_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
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
⊢ si * s = 1
have rw₁ : @invOf _ MulOne.toMul MulOne.toOne r _ * r = 1
Tactic: rw [hs, hsi, invOf_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
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
⊢ si * s = 1
have rw₂ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [hs, hsi, invOf_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = @invOf _ MulOne.toMul MulOne.toOne r _
⊢ s * si = 1
have rw : r * si = 1
Tactic: rw [hs, hsi, mul_invOf_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
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
⊢ s * si = 1
have rw₁ : r * @invOf _ MulOne.toMul MulOne.toOne r _ = 1
Tactic: rw [hs, hsi, mul_invOf_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
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
⊢ s * si = 1
have rw₂ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [hs, hsi, mul_invOf_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a b c : α
inst_1 : Invertible c
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * a = b ↔ a = c * b
have rw : c * (@Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * a) = c * b ↔ a = c * b
Tactic: rw [← mul_right_inj_of_invertible (c := c), mul_invOf_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
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
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * a = b ↔ a = c * b
have rw₁ : a = c * b ↔ a = c * b
Tactic: rw [← mul_right_inj_of_invertible (c := c), mul_invOf_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a b c : α
inst_1 : Invertible c
⊢ c * a = b ↔ a = @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * b
have 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
Tactic: rw [← mul_right_inj_of_invertible (c := ⅟c), invOf_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
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
⊢ c * a = b ↔ a = @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * b
have rw₁ : a = @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * b ↔ a = @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * b
Tactic: rw [← mul_right_inj_of_invertible (c := ⅟c), invOf_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a b c : α
inst_1 : Invertible c
⊢ a * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ = b ↔ a = b * c
have rw : a * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ * c = b * c ↔ a = b * c
Tactic: rw [← mul_left_inj_of_invertible (c := c), invOf_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
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
⊢ a * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ = b ↔ a = b * c
have rw₁ : a = b * c ↔ a = b * c
Tactic: rw [← mul_left_inj_of_invertible (c := c), invOf_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
Goal:
α : Type u
inst : Monoid α
a b c : α
inst_1 : Invertible c
⊢ a * c = b ↔ a = b * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _
have 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 _
Tactic: rw [← mul_left_inj_of_invertible (c := ⅟c), mul_invOf_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Invertible.Defs (goal)
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 _
⊢ a * c = b ↔ a = b * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _
have rw₁ : a = b * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ ↔ a = b * @Invertible.invOf _ MulOne.toMul MulOne.toOne c _
Tactic: rw [← mul_left_inj_of_invertible (c := ⅟c), mul_invOf_cancel_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
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
⊢ v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f) =
    (⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f
have apply : (⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f ⊆ v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f)
Tactic: apply subset_antisymm (this f)
-- 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
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
⊢ (⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f ⊆
    v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f)
have 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)))
Tactic: replace this := image_mono (f := invMonoidHom) <| this (invMonoidHom.comp f)
Cleared hypotheses: this
-- 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
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)))
⊢ (⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f ⊆
    v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f)
have 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))
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
Cleared hypotheses: this
-- 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
⊢ v '' baseOf.{u_1, u_3, u_4} (S := S) v (MonoidHom.comp invMonoidHom f) =
    (⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f
have 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
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
-- 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 :
  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 G) ((⇑invMonoidHom : (a : G) → G) ∘ v '' baseOf v f) (v i)
have 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
Tactic: refine ⟨i⁻¹, ⟨by simpa [hv_inv] using hi, fun j hj k hk hi ↦ ?_⟩, by simp [hv_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 : 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⁻¹
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