awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
S : Type u_3
inst_2 : CommSemiring S
inst_3 : Algebra S R
inst_4 : Algebra.IsCentral S R
u v : ↥(unitary R)
simp_rw :
  (∀ (a : R),
      Eq (α := R) ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)
        ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₁ : (∀ (a : R), (↑v : R) * a * star (↑v : R) = (↑u : R) * a * star (↑u : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₂ :
  (∀ (a : R), (↑v : R) * a * (↑(star v) : R) = (↑u : R) * a * (↑(star u) : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₃ : (∀ (a : R), (↑v : R) * a * (↑v⁻¹ : R) = (↑u : R) * a * (↑u⁻¹ : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₄ :
  (∀ (a : R),
      (↑v : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) =
        (↑u : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u)⁻¹ : R)) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)
⊢ Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R)
      ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)
have simp_rw₅ : (∀ (a : R),
    (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) =
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u)⁻¹ : R)) ↔
  ∃ (α : S),
    (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
      HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
Tactic: simp_rw [StarAlgEquiv.ext_iff, conjStarAlgAut_apply, ← coe_star, star_eq_inv,
    ← val_inv_toUnits_apply, ← val_toUnits_apply, mul_assoc, ← Units.eq_inv_mul_iff_mul_eq,
    ← mul_assoc, Units.eq_mul_inv_iff_mul_eq, mul_assoc, ← mul_assoc (((toUnits v)⁻¹ : Rˣ) : R),
    ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot, Algebra.mem_bot,
    Set.mem_range, Algebra.algebraMap_eq_smul_one, Units.eq_inv_mul_iff_mul_eq, mul_smul_comm,
    mul_one, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
S : Type u_3
inst_2 : CommSemiring S
inst_3 : Algebra S R
inst_4 : Algebra.IsCentral S R
u v : ↥(unitary R)
simp_rw :
  (∀ (a : R),
      Eq (α := R) ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)
        ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₁ : (∀ (a : R), (↑v : R) * a * star (↑v : R) = (↑u : R) * a * star (↑u : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₂ :
  (∀ (a : R), (↑v : R) * a * (↑(star v) : R) = (↑u : R) * a * (↑(star u) : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₃ : (∀ (a : R), (↑v : R) * a * (↑v⁻¹ : R) = (↑u : R) * a * (↑u⁻¹ : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₄ :
  (∀ (a : R),
      (↑v : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) =
        (↑u : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u)⁻¹ : R)) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₅ :
  (∀ (a : R),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) =
        (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u)⁻¹ : R)) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
⊢ Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R)
      ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)
have simp_rw₆ : (∀ (a : R),
    (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R) * (a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R)) =
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) * (a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u)⁻¹ : R))) ↔
  ∃ (α : S),
    (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
      HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
Tactic: simp_rw [StarAlgEquiv.ext_iff, conjStarAlgAut_apply, ← coe_star, star_eq_inv,
    ← val_inv_toUnits_apply, ← val_toUnits_apply, mul_assoc, ← Units.eq_inv_mul_iff_mul_eq,
    ← mul_assoc, Units.eq_mul_inv_iff_mul_eq, mul_assoc, ← mul_assoc (((toUnits v)⁻¹ : Rˣ) : R),
    ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot, Algebra.mem_bot,
    Set.mem_range, Algebra.algebraMap_eq_smul_one, Units.eq_inv_mul_iff_mul_eq, mul_smul_comm,
    mul_one, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
S : Type u_3
inst_2 : CommSemiring S
inst_3 : Algebra S R
inst_4 : Algebra.IsCentral S R
u v : ↥(unitary R)
simp_rw :
  (∀ (a : R),
      Eq (α := R) ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)
        ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₁ : (∀ (a : R), (↑v : R) * a * star (↑v : R) = (↑u : R) * a * star (↑u : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₂ :
  (∀ (a : R), (↑v : R) * a * (↑(star v) : R) = (↑u : R) * a * (↑(star u) : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₃ : (∀ (a : R), (↑v : R) * a * (↑v⁻¹ : R) = (↑u : R) * a * (↑u⁻¹ : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₄ :
  (∀ (a : R),
      (↑v : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) =
        (↑u : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u)⁻¹ : R)) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₅ :
  (∀ (a : R),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) =
        (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u)⁻¹ : R)) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₆ :
  (∀ (a : R),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R) * (a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R)) =
        (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) * (a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u)⁻¹ : R))) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
⊢ Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R)
      ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)
have simp_rw₇ : (∀ (a : R),
    a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) =
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) *
        ((↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) * (a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u)⁻¹ : R)))) ↔
  ∃ (α : S),
    (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
      HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
Tactic: simp_rw [StarAlgEquiv.ext_iff, conjStarAlgAut_apply, ← coe_star, star_eq_inv,
    ← val_inv_toUnits_apply, ← val_toUnits_apply, mul_assoc, ← Units.eq_inv_mul_iff_mul_eq,
    ← mul_assoc, Units.eq_mul_inv_iff_mul_eq, mul_assoc, ← mul_assoc (((toUnits v)⁻¹ : Rˣ) : R),
    ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot, Algebra.mem_bot,
    Set.mem_range, Algebra.algebraMap_eq_smul_one, Units.eq_inv_mul_iff_mul_eq, mul_smul_comm,
    mul_one, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
| Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R)
    ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R)
have rw : Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R)
  ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R)
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R)
      ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R) ↔
    ∃ (α : ↥(unitary S)), u = α • v
have conv_lhs : Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R)
    ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) ↔
  ∃ (α : ↥(unitary S)), u = α • v
Tactic: conv_lhs => rw [eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R)
      ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) ↔
    ∃ (α : ↥(unitary S)), u = α • v
have simp_rw : (∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)) ↔ ∃ (α : ↥(unitary S)), u = α • v
Tactic: simp_rw [StarAlgEquiv.ext_iff, conjStarAlgAut_apply, ← coe_star, star_eq_inv,
    ← val_inv_toUnits_apply, ← val_toUnits_apply, mul_assoc, ← Units.eq_inv_mul_iff_mul_eq,
    ← mul_assoc, Units.eq_mul_inv_iff_mul_eq, mul_assoc, ← mul_assoc (((toUnits v)⁻¹ : Rˣ) : R),
    ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot, Algebra.mem_bot,
    Set.mem_range, Algebra.algebraMap_eq_smul_one, val_inv_toUnits_apply, val_toUnits_apply,
    ← star_eq_inv, coe_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (α : ↥(unitary S)), u = α • v
y : ↥(unitary S)
h : u = y • v
⊢ HSMul.hSMul (β := R) (↑y : S) 1 = star (↑v : R) * (↑u : R)
have simp : HSMul.hSMul (β := R) (↑y : S) 1 = HSMul.hSMul (β := R) y 1
Tactic: simp only [h, coe_smul, mul_smul_comm, SetLike.coe_mem, star_mul_self_of_mem]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)) ↔ ∃ (α : ↥(unitary S)), u = α • v
have refine : (∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)) →
  ∀ (y : S) (h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)), ∃ (α : ↥(unitary S)), u = α • v
Tactic: refine ⟨fun ⟨y, h⟩ ↦ ?_, fun ⟨y, h⟩ ↦ ⟨(y : S), by
    simp only [h, coe_smul, mul_smul_comm, SetLike.coe_mem, star_mul_self_of_mem]; rfl⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (hypothesis)
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
⊢ ∃ (α : ↥(unitary S)), u = α • v
have huv : (↑u : R) = y • (↑v : R)
Tactic: have huv : (u : R) = y • (v : R) := by simpa [← mul_assoc] using congr(v * $h).symm
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (hypothesis)
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
⊢ ∃ (α : ↥(unitary S)), u = α • v
have hvu : (↑v : R) = star y • (↑u : R)
Tactic: have hvu : (v : R) = star y • (u : R) := by simpa [← mul_assoc] using congr(u * (star $h)).symm
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (hypothesis)
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
⊢ ∃ (α : ↥(unitary S)), u = α • v
have hvy : (↑v : R) = (star y * y) • (↑v : R)
Tactic: have hvy : (v : R) = (star y * y) • (v : R) := by simp [← smul_smul, ← huv, ← hvu]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (hypothesis)
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
hvy : (↑v : R) = (star y * y) • (↑v : R)
⊢ ∃ (α : ↥(unitary S)), u = α • v
have hvy₁ : HSMul.hSMul.{u_4, u_3, u_3} (α := S) 1 (↑v : R) = (star y * y) • (↑v : R)
Tactic: nth_rw 1 [← one_smul S (v : R)] at hvy
Cleared hypotheses: hvy
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (hypothesis)
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
hvy : HSMul.hSMul.{u_4, u_3, u_3} (α := S) 1 (↑v : R) = (star y * y) • (↑v : R)
⊢ ∃ (α : ↥(unitary S)), u = α • v
have hvy₁ : star y * y = 1 ∨ (↑v : R) = 0
Tactic: rw [← sub_eq_zero, ← sub_smul, smul_eq_zero, sub_eq_zero, eq_comm] at hvy
Cleared hypotheses: hvy
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
hvy : star y * y = 1 ∨ (↑v : R) = 0
⊢ ∃ (α : ↥(unitary S)), u = α • v
have inl : ∀ (this : star y * y = 1), ∃ (α : ↥(unitary S)), u = α • v
Tactic: obtain (this | this) := hvy
Cleared hypotheses: hvy
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
hvy : star y * y = 1 ∨ (↑v : R) = 0
inl : ∀ (this : star y * y = 1), ∃ (α : ↥(unitary S)), u = α • v
⊢ ∃ (α : ↥(unitary S)), u = α • v
have inr : ∀ (this : (↑v : R) = 0), ∃ (α : ↥(unitary S)), u = α • v
Tactic: obtain (this | this) := hvy
Cleared hypotheses: hvy
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
this : star y * y = 1
⊢ u = Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (unitary S) x) y ⋯ • v
have a : (↑u : R) = (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (unitary S) x) y sorry • v) : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
this : (↑v : R) = 0
⊢ u = HSMul.hSMul.{u_4, u_3, u_3} (α := ↥(unitary S)) 1 v
have a : (↑u : R) = (↑(HSMul.hSMul.{u_4, u_3, u_3} (α := ↥(unitary S)) 1 v) : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) =
    1
have rw : Eq (α := αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a +
          a * @Invertible.invOf _ inst AddMonoidWithOne.toOne a _)) :
    αˢʸᵐ)
  (1 : αˢʸᵐ)
Tactic: rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a +
            a * @Invertible.invOf _ inst AddMonoidWithOne.toOne a _)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) =
    1
have rw₁ : Eq (α := αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a + 1)) :
    αˢʸᵐ)
  (1 : αˢʸᵐ)
Tactic: rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a +
            a * @Invertible.invOf _ inst AddMonoidWithOne.toOne a _)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₁ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a + 1)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) =
    1
have rw₂ : Eq (α := αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ * HAdd.hAdd (α := α) 1 1) : αˢʸᵐ)
  (1 : αˢʸᵐ)
Tactic: rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a +
            a * @Invertible.invOf _ inst AddMonoidWithOne.toOne a _)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₁ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a + 1)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₂ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ * HAdd.hAdd (α := α) 1 1) : αˢʸᵐ)
    (1 : αˢʸᵐ)
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) =
    1
have rw₃ : Eq (α := αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ) (HMul.hMul (α := α) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _) 2) : αˢʸᵐ)
  (1 : αˢʸᵐ)
Tactic: rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a +
            a * @Invertible.invOf _ inst AddMonoidWithOne.toOne a _)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₁ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a + 1)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₂ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ * HAdd.hAdd (α := α) 1 1) : αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₃ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (HMul.hMul (α := α) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _) 2) : αˢʸᵐ)
    (1 : αˢʸᵐ)
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) =
    1
have rw₄ : Eq.{u_1 + 1} (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) 1 : αˢʸᵐ) (1 : αˢʸᵐ)
Tactic: rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]