awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Azumaya.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
e : A ≃ₐ[R] B
⊢ AlgHom.comp (AlgHom.mulLeftRight R B)
      (↑(Algebra.TensorProduct.congr e ((AlgEquiv.op : (a : A ≃ₐ[R] B) → Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) e)) :
        A ⊗[R] Aᵐᵒᵖ →ₐ[R] B ⊗[R] Bᵐᵒᵖ) =
    AlgHom.comp (↑(LinearEquiv.conjAlgEquiv R (↑e : A ≃ₗ[R] B)) : Module.End R A →ₐ[R] Module.End R B)
      (AlgHom.mulLeftRight R A)
have ha : ∀ (x : A) (x_1 : B),
  Eq (α := B)
    ((((AlgHom.comp (B := A ⊗[R] Aᵐᵒᵖ)
                  (AlgHom.comp (AlgHom.mulLeftRight R B)
                    (↑(Algebra.TensorProduct.congr e ((AlgEquiv.op : (a : A ≃ₐ[R] B) → Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) e)) :
                      A ⊗[R] Aᵐᵒᵖ →ₐ[R] B ⊗[R] Bᵐᵒᵖ))
                  Algebra.TensorProduct.includeLeft :
                (a : A) → Module.End R B)
              x :
            Module.End R B) :
          (a : B) → B)
        x_1 :
      B)
    (((((AlgHom.comp
                    (AlgHom.comp (↑(LinearEquiv.conjAlgEquiv R (↑e : A ≃ₗ[R] B)) : Module.End R A →ₐ[R] Module.End R B)
                      (AlgHom.mulLeftRight R A))
                    Algebra.TensorProduct.includeLeft :
                  AlgHom.{u_1, u_2, u_3} R A (Module.End R B)) :
                (a : A) → Module.End R B)
              x :
            Module.End R B) :
          (a : B) → B)
        x_1 :
      B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Azumaya.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
e : A ≃ₐ[R] B
ha :
  ∀ (x : A) (x_1 : B),
    Eq (α := B)
      ((((AlgHom.comp (B := A ⊗[R] Aᵐᵒᵖ)
                    (AlgHom.comp (AlgHom.mulLeftRight R B)
                      (↑(Algebra.TensorProduct.congr e ((AlgEquiv.op : (a : A ≃ₐ[R] B) → Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) e)) :
                        A ⊗[R] Aᵐᵒᵖ →ₐ[R] B ⊗[R] Bᵐᵒᵖ))
                    Algebra.TensorProduct.includeLeft :
                  (a : A) → Module.End R B)
                x :
              Module.End R B) :
            (a : B) → B)
          x_1 :
        B)
      (((((AlgHom.comp
                      (AlgHom.comp
                        (↑(LinearEquiv.conjAlgEquiv R (↑e : A ≃ₗ[R] B)) : Module.End R A →ₐ[R] Module.End R B)
                        (AlgHom.mulLeftRight R A))
                      Algebra.TensorProduct.includeLeft :
                    AlgHom.{u_1, u_2, u_3} R A (Module.End R B)) :
                  (a : A) → Module.End R B)
                x :
              Module.End R B) :
            (a : B) → B)
          x_1 :
        B)
⊢ AlgHom.comp (AlgHom.mulLeftRight R B)
      (↑(Algebra.TensorProduct.congr e ((AlgEquiv.op : (a : A ≃ₐ[R] B) → Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) e)) :
        A ⊗[R] Aᵐᵒᵖ →ₐ[R] B ⊗[R] Bᵐᵒᵖ) =
    AlgHom.comp (↑(LinearEquiv.conjAlgEquiv R (↑e : A ≃ₗ[R] B)) : Module.End R A →ₐ[R] Module.End R B)
      (AlgHom.mulLeftRight R A)
have hb : ∀ (x : Aᵐᵒᵖ) (x_1 : B),
  Eq (α := B)
    ((((AlgHom.comp (B := A ⊗[R] Aᵐᵒᵖ)
                  (AlgHom.restrictScalars R
                    (AlgHom.comp (AlgHom.mulLeftRight R B)
                      (↑(Algebra.TensorProduct.congr e ((AlgEquiv.op : (a : A ≃ₐ[R] B) → Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) e)) :
                        A ⊗[R] Aᵐᵒᵖ →ₐ[R] B ⊗[R] Bᵐᵒᵖ)))
                  Algebra.TensorProduct.includeRight :
                (a : Aᵐᵒᵖ) → Module.End R B)
              x :
            Module.End R B) :
          (a : B) → B)
        x_1 :
      B)
    (((((AlgHom.comp
                    (AlgHom.restrictScalars R
                      (AlgHom.comp
                        (↑(LinearEquiv.conjAlgEquiv R (↑e : A ≃ₗ[R] B)) : Module.End R A →ₐ[R] Module.End R B)
                        (AlgHom.mulLeftRight R A)))
                    Algebra.TensorProduct.includeRight :
                  AlgHom.{u_1, u_2, u_3} R Aᵐᵒᵖ (Module.End R B)) :
                (a : Aᵐᵒᵖ) → Module.End R B)
              x :
            Module.End R B) :
          (a : B) → B)
        x_1 :
      B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Azumaya.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
e : A ≃ₐ[R] B
inst_5 : IsAzumaya R A
h : Module.Projective R B := ⋯
h_1 : FaithfulSMul R B := ⋯
h_2 : Module.Finite R B := ⋯
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := A ⊗[R] Aᵐᵒᵖ) (β := Module.End R B)
    (Function.comp (β := B ⊗[R] Bᵐᵒᵖ) (⇑(AlgHom.mulLeftRight R B) : (a : B ⊗[R] Bᵐᵒᵖ) → Module.End R B)
      (⇑(Algebra.TensorProduct.congr e ((AlgEquiv.op : (a : A ≃ₐ[R] B) → Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) e) :
            AlgEquiv.{u_1, u_2, u_3} R (A ⊗[R] Aᵐᵒᵖ) (B ⊗[R] Bᵐᵒᵖ)) :
        (a : A ⊗[R] Aᵐᵒᵖ) → B ⊗[R] Bᵐᵒᵖ))
have rw : Function.Bijective.{u_2 + 1, u_3 + 1} (α := A ⊗[R] Aᵐᵒᵖ) (β := Module.End R B)
  (⇑(AlgHom.comp (↑(LinearEquiv.conjAlgEquiv R (↑e : A ≃ₗ[R] B)) : Module.End R A →ₐ[R] Module.End R B)
        (AlgHom.mulLeftRight R A)) :
    (a : A ⊗[R] Aᵐᵒᵖ) → Module.End R B)
Tactic: rw [← AlgEquiv.coe_algHom, ← AlgHom.coe_comp, mulLeftRight_comp_congr]
-- Lean 4 proof step from Mathlib.Algebra.Azumaya.Defs (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
this : Module (A ⊗[R] Aᵐᵒᵖ) A := Algebra.module
r : R
ab : A ⊗[R] Aᵐᵒᵖ
a : A
⊢ (r • ab) • a = r • ab • a
have change : (((Algebra.moduleAux : (a : A ⊗[R] Aᵐᵒᵖ) → A →ₗ[R] A) (r • ab) : A →ₗ[R] A) : (a : A) → A) a =
  HSMul.hSMul (β := A) r ((((Algebra.moduleAux : (a : A ⊗[R] Aᵐᵒᵖ) → A →ₗ[R] A) ab : A →ₗ[R] A) : (a : A) → A) a : A)
Tactic: change TensorProduct.Algebra.moduleAux _ _ = _ • TensorProduct.Algebra.moduleAux _ _
-- Lean 4 proof step from Mathlib.Algebra.Azumaya.Defs (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
b : Aᵐᵒᵖ
x : A
⊢ (((mulLeftRight R A : (a : A ⊗[R] Aᵐᵒᵖ) → Module.End R A) (a ⊗ₜ[R] b) : Module.End R A) : (a : A) → A) x =
    a * x * MulOpposite.unop b
have simp : HSMul.hSMul (α := A ⊗[R] Aᵐᵒᵖ) (a ⊗ₜ[R] b) x = a * x * MulOpposite.unop b
Tactic: simp only [AlgHom.mulLeftRight, Algebra.lsmul_coe]
-- Lean 4 proof step from Mathlib.Algebra.Azumaya.Defs (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
b : Aᵐᵒᵖ
x : A
⊢ HSMul.hSMul (α := A ⊗[R] Aᵐᵒᵖ) (a ⊗ₜ[R] b) x = a * x * MulOpposite.unop b
have change : (((Algebra.moduleAux : (a : A ⊗[R] Aᵐᵒᵖ) → A →ₗ[R] A) (a ⊗ₜ[R] b) : A →ₗ[R] A) : (a : A) → A) x =
  a * x * MulOpposite.unop b
Tactic: change TensorProduct.Algebra.moduleAux _ _ = _
-- Lean 4 proof step from Mathlib.Algebra.Azumaya.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Eq (α := Module.End R (Matrix n n R) →ₗ[R] Module.End R (Matrix n n R))
    (toLinearMap (mulLeftRight R (Matrix n n R)) ∘ₗ mulLeftRightMatrix_inv R n :
      Module.End R (Matrix n n R) →ₗ[R] Module.End R (Matrix n n R))
    (LinearMap.id : Module.End R (Matrix n n R) →ₗ[R] Module.End R (Matrix n n R))
have h : ∀ (f : Module.End R (Matrix n n R)),
  Eq (α := Module.End R (Matrix n n R))
    ((toLinearMap (mulLeftRight R (Matrix n n R)) ∘ₗ mulLeftRightMatrix_inv R n :
          (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R))
        f :
      Module.End R (Matrix n n R))
    ((LinearMap.id : (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R)) f : Module.End R (Matrix n n R))
Tactic: ext f : 1
-- Lean 4 proof step from Mathlib.Algebra.Azumaya.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
f : Module.End R (Matrix n n R)
⊢ Eq (α := Module.End R (Matrix n n R))
    ((toLinearMap (mulLeftRight R (Matrix n n R)) ∘ₗ mulLeftRightMatrix_inv R n :
          (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R))
        f :
      Module.End R (Matrix n n R))
    ((LinearMap.id : (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R)) f : Module.End R (Matrix n n R))
have h : ∀ (i : n × n),
  Eq (α := Matrix n n R)
    ((((toLinearMap (mulLeftRight R (Matrix n n R)) ∘ₗ mulLeftRightMatrix_inv R n :
                (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R))
              f :
            Module.End R (Matrix n n R)) :
          (a : Matrix n n R) → Matrix n n R)
        ((stdBasis R n n : (a : n × n) → Matrix n n R) i) :
      Matrix n n R)
    ((((LinearMap.id : (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R)) f :
            Module.End R (Matrix n n R)) :
          (a : Matrix n n R) → Matrix n n R)
        ((stdBasis R n n : (a : n × n) → Matrix n n R) i) :
      Matrix n n R)
Tactic: apply (Matrix.stdBasis _ _ _).ext
-- Lean 4 proof step from Mathlib.Algebra.Azumaya.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
f : Module.End R (Matrix n n R)
i j : n
⊢ Eq (α := Matrix n n R)
    ((((toLinearMap (mulLeftRight R (Matrix n n R)) ∘ₗ mulLeftRightMatrix_inv R n :
                (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R))
              f :
            Module.End R (Matrix n n R)) :
          (a : Matrix n n R) → Matrix n n R)
        ((stdBasis R n n : (a : n × n) → Matrix n n R) (i, j)) :
      Matrix n n R)
    ((((LinearMap.id : (a : Module.End R (Matrix n n R)) → Module.End R (Matrix n n R)) f :
            Module.End R (Matrix n n R)) :
          (a : Matrix n n R) → Matrix n n R)
        ((stdBasis R n n : (a : n × n) → Matrix n n R) (i, j)) :
      Matrix n n R)
have h : Eq (α := Matrix n n R)
  (∑ x : (n × n) × n × n,
      HSMul.hSMul (α := R) (β := Matrix n n R)
        ((f : (a : Matrix n n R) → Matrix n n R) (single x.1.2 x.2.1 1) x.1.1 x.2.2 : R)
        ((((toLinearMap (mulLeftRight R (Matrix n n R)) :
                    (a : Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) → Module.End R (Matrix n n R))
                  (single x.1.1 x.1.2 1 ⊗ₜ[R] op (single x.2.1 x.2.2 1)) :
                Module.End R (Matrix n n R)) :
              (a : Matrix n n R) → Matrix n n R)
            (single i j 1) :
          Matrix n n R) :
    Matrix n n R)
  ((f : (a : Matrix n n R) → Matrix n n R) (single i j 1) : Matrix n n R)
Tactic: simp only [LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, map_sum,
    map_smul, stdBasis_eq_single, LinearMap.coe_sum, Finset.sum_apply,
    LinearMap.smul_apply, LinearMap.id_coe, id_eq]
-- Lean 4 proof step from Mathlib.Algebra.Azumaya.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
f : Module.End R (Matrix n n R)
i j : n
⊢ Eq (α := Matrix n n R)
    (∑ x : (n × n) × n × n,
        HSMul.hSMul (α := R) (β := Matrix n n R)
          ((f : (a : Matrix n n R) → Matrix n n R) (single x.1.2 x.2.1 1) x.1.1 x.2.2 : R)
          ((((toLinearMap (mulLeftRight R (Matrix n n R)) :
                      (a : Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) → Module.End R (Matrix n n R))
                    (single x.1.1 x.1.2 1 ⊗ₜ[R] op (single x.2.1 x.2.2 1)) :
                  Module.End R (Matrix n n R)) :
                (a : Matrix n n R) → Matrix n n R)
              (single i j 1) :
            Matrix n n R) :
      Matrix n n R)
    ((f : (a : Matrix n n R) → Matrix n n R) (single i j 1) : Matrix n n R)
have h : ∀ (k l : n),
  Eq.{u_1 + 1} (α := R)
    ((∑ x : (n × n) × n × n,
          HSMul.hSMul (α := R) (β := Matrix n n R)
            ((f : (a : Matrix n n R) → Matrix n n R) (single x.1.2 x.2.1 1) x.1.1 x.2.2 : R)
            ((((toLinearMap (mulLeftRight R (Matrix n n R)) :
                        (a : Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ) → Module.End R (Matrix n n R))
                      (single x.1.1 x.1.2 1 ⊗ₜ[R] op (single x.2.1 x.2.2 1)) :
                    Module.End R (Matrix n n R)) :
                  (a : Matrix n n R) → Matrix n n R)
                (single i j 1) :
              Matrix n n R))
        k l :
      R)
    ((f : (a : Matrix n n R) → Matrix n n R) (single i j 1) k l : R)
Tactic: ext k l
-- Lean 4 proof step from Mathlib.Algebra.Azumaya.Matrix (hypothesis)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
⊢ ∀ {m₁ m₂ : R}, (∀ (a : Matrix n n R), m₁ • a = m₂ • a) → m₁ = m₂
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M : Type u_4
inst : CommMonoid M
ι : Type u_5
f g : ι → M
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ~ᵤ g i
⊢ Associated.{u_4} (M := M) (∏ i ∈ ∅, f i) (∏ i ∈ ∅, g i)
have empty : Associated.{u_4} (M := M) 1 1
Tactic: simp only [Finset.prod_empty]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M : Type u_4
inst : CommMonoid M
ι : Type u_5
s : Finset ι
f g : ι → M
h : ∀ i ∈ s, f i ~ᵤ g i
⊢ Associated.{u_4} (M := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have empty : ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ~ᵤ g i),
  Associated.{u_4} (M := M) (∏ i ∈ ∅, f i) (∏ i ∈ ∅, g i)
Tactic: induction s using Finset.induction with
  | empty =>
    simp only [Finset.prod_empty]
    rfl
  | insert j s hjs IH =>
    classical
    convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i)
    grind [Associated.mul_mul]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M : Type u_4
inst : CommMonoid M
ι : Type u_5
s : Finset ι
f g : ι → M
h : ∀ i ∈ s, f i ~ᵤ g i
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ~ᵤ g i),
    Associated.{u_4} (M := M) (∏ i ∈ ∅, f i) (∏ i ∈ ∅, g i)
⊢ Associated.{u_4} (M := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have insert : ∀ (j : ι) (s : Finset ι) (hjs : j ∉ s)
  (IH : ∀ (h : ∀ i ∈ s, f i ~ᵤ g i), Associated.{u_4} (M := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i))
  (h : ∀ i ∈ insert j s, f i ~ᵤ g i), Associated.{u_4} (M := M) (∏ i ∈ insert j s, f i) (∏ i ∈ insert j s, g i)
Tactic: induction s using Finset.induction with
  | empty =>
    simp only [Finset.prod_empty]
    rfl
  | insert j s hjs IH =>
    classical
    convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i)
    grind [Associated.mul_mul]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (hypothesis)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
p : M₀
hp : Prime p
s_1 : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ (a ::ₘ s).prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q
have hps₁ : p ∣ a * s.prod
Tactic: rw [Multiset.prod_cons] at hps
Cleared hypotheses: hps
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
p : M₀
hp : Prime p
s_1 : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q
have inl : ∀ (h : p ∣ a), ∃ q ∈ a ::ₘ s, p ~ᵤ q
Tactic: rcases hp.dvd_or_dvd hps with h | h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
p : M₀
hp : Prime p
s_1 : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
inl : ∀ (h : p ∣ a), ∃ q ∈ a ::ₘ s, p ~ᵤ q
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q
have inr : ∀ (h : p ∣ s.prod), ∃ q ∈ a ::ₘ s, p ~ᵤ q
Tactic: rcases hp.dvd_or_dvd hps with h | h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (hypothesis)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
p : M₀
hp : Prime p
s_1 : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ a
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q
have hap : Prime a
Tactic: have hap := hs a (Multiset.mem_cons.2 (Or.inl rfl))
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
p : M₀
hp : Prime p
s_1 : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q
have inr : ∀ (q : M₀) (hq₁ : q ∈ s) (hq₂ : p ~ᵤ q), ∃ q ∈ a ::ₘ s, p ~ᵤ q
Tactic: rcases ih (fun r hr => hs _ (Multiset.mem_cons.2 (Or.inr hr))) h with ⟨q, hq₁, hq₂⟩
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
have obtain : ∀ (m : Multiset M₀) (hm : ∀ y ∈ m, Membership.mem (γ := Set M₀) {r : M₀ | IsUnit r ∨ Prime r} y)
  (hprod : m.prod = x * y), Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
Tactic: obtain ⟨m, hm, hprod⟩ := exists_multiset_of_mem_closure hxy
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hm : ∀ (y : M₀), Membership.mem (γ := Multiset M₀) 0 y → Membership.mem (γ := Set M₀) {r : M₀ | IsUnit r ∨ Prime r} y
hprod : Multiset.prod 0 = x * y
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
have empty : Membership.mem (γ := Set M₀) {r : M₀ | IsUnit r ∨ Prime r} x
Tactic: apply subset_closure
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hm : ∀ (y : M₀), Membership.mem (γ := Multiset M₀) 0 y → Membership.mem (γ := Set M₀) {r : M₀ | IsUnit r ∨ Prime r} y
hprod : 1 = x * y
⊢ IsUnit x ∨ Prime x
have empty : IsUnit x
Tactic: left
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (hypothesis)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, Membership.mem (γ := Set M₀) {r : M₀ | IsUnit r ∨ Prime r} y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hm : ∀ y ∈ c ::ₘ s, Membership.mem (γ := Set M₀) {r : M₀ | IsUnit r ∨ Prime r} y
hprod : (c ::ₘ s).prod = x * y
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
have hm₁ : (IsUnit c ∨ Prime c) ∧ ∀ a ∈ s, IsUnit a ∨ Prime a
Tactic: simp only [Multiset.mem_cons, forall_eq_or_imp, Set.mem_setOf] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (hypothesis)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, Membership.mem (γ := Set M₀) {r : M₀ | IsUnit r ∨ Prime r} y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hprod : (c ::ₘ s).prod = x * y
hm : (IsUnit c ∨ Prime c) ∧ ∀ a ∈ s, IsUnit a ∨ Prime a
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
have hprod₁ : c * s.prod = x * y
Tactic: simp only [Multiset.prod_cons] at hprod
Cleared hypotheses: hprod
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hm : (IsUnit c ∨ Prime c) ∧ ∀ a ∈ s, IsUnit a ∨ Prime a
hprod : c * s.prod = x * y
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
have cons : ∀ (hs : ∀ a ∈ s, IsUnit a ∨ Prime a) (ha₁ : IsUnit c),
  Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
Tactic: obtain ⟨ha₁ | ha₂, hs⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hm : (IsUnit c ∨ Prime c) ∧ ∀ a ∈ s, IsUnit a ∨ Prime a
hprod : c * s.prod = x * y
cons :
  ∀ (hs : ∀ a ∈ s, IsUnit a ∨ Prime a) (ha₁ : IsUnit c),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
have cons₁ : ∀ (hs : ∀ a ∈ s, IsUnit a ∨ Prime a) (ha₂ : Prime c),
  Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
Tactic: obtain ⟨ha₁ | ha₂, hs⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
have cons : ∀ (k : M₀) (hk : c * k = 1), Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
Tactic: rcases ha₁.exists_right_inv with ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
have cons : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * (y * k))
Tactic: refine hind x (y * k) ?_ hs ?_