awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
⊢ Eq (α := Pic R) (Pic.mk R (M.AsModule ⊗[R] M⁻¹.AsModule)) 1
have simp_rw : HMul.hMul (α := Pic R) (Pic.mk R M.AsModule) (Pic.mk R M⁻¹.AsModule) = 1
Tactic: simp_rw [mk_tensor, mk_eq_self, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
simp_rw : HMul.hMul (α := Pic R) (Pic.mk R M.AsModule) (Pic.mk R M⁻¹.AsModule) = 1
⊢ Eq (α := Pic R) (Pic.mk R (M.AsModule ⊗[R] M⁻¹.AsModule)) 1
have simp_rw₁ : M * M⁻¹ = 1
Tactic: simp_rw [mk_tensor, mk_eq_self, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (hypothesis)
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
⊢ IsUnit (submoduleAlgebra e * submoduleAlgebra f)
have this : submoduleAlgebra e * submoduleAlgebra f =
  R ∙
    (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ sorry.some) ≪≫ₗ
                  tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
              R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
            (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
          1) :
      A)
Tactic: have := eq_span_singleton_of_surjective <| LinearEquiv.surjective <|
    (congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ
    (mk_eq_one_iff.mp <| by simp_rw [mk_tensor, mk_eq_self, mul_inv_cancel]).some).symm ≪≫ₗ
    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  submoduleAlgebra e * submoduleAlgebra f =
    R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A)
⊢ IsUnit (submoduleAlgebra e * submoduleAlgebra f)
have h₁ : IsUnit (M := Submodule R A)
  (R ∙
    (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ sorry.some) ≪≫ₗ
                  tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
              R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
            (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
          1) :
      A))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (hypothesis)
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  submoduleAlgebra e * submoduleAlgebra f =
    R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A)
⊢ IsUnit (M := Submodule R A)
    (R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A))
have this₁ : ⊤ * (submoduleAlgebra e * submoduleAlgebra f) =
  HMul.hMul (α := Submodule R A) ⊤
    (R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ sorry.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A))
Tactic: apply_fun (⊤ * ·) at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (hypothesis)
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  ⊤ * (submoduleAlgebra e * submoduleAlgebra f) =
    HMul.hMul (α := Submodule R A) ⊤
      (R ∙
        (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                      tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                  R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
                (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
              1) :
          A))
⊢ IsUnit (M := Submodule R A)
    (R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A))
have this₁ : ⊤ =
  HMul.hMul (α := Submodule R A) ⊤
    (R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ sorry.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A))
Tactic: simp_rw [← mul_assoc, top_mul_submoduleAlgebra] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
M : Pic R
h : Membership.mem (γ := Subgroup (Pic R)) (relPic R A) M
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  ⊤ =
    HMul.hMul (α := Submodule R A) ⊤
      (R ∙
        (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                      tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                  R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
                (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
              1) :
          A))
⊢ IsUnit (M := Submodule R A)
    (R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A))
have h₁ : ∀ (a : A)
  (eq :
    a *
        (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ sorry.some) ≪≫ₗ
                      tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                  R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
                (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
              1) :
          A) =
      1),
  IsUnit (M := Submodule R A)
    (R ∙
      (↑(((↑(LinearEquiv.symm (TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ sorry.some) ≪≫ₗ
                    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)) :
                R →ₗ[R] ↥(submoduleAlgebra e * submoduleAlgebra f)) :
              (a : R) → ↥(submoduleAlgebra e * submoduleAlgebra f))
            1) :
        A))
Tactic: obtain ⟨a, -, eq⟩ := mem_mul_span_singleton.mp (this ▸ mem_top (x := 1))
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
⊢ I = ⊤ ∧ J = ⊤
have have : ∀ (e : ↥I ⊗[R] ↥J ≃ₗ[R] R), I = ⊤ ∧ J = ⊤
Tactic: have ⟨e⟩ := mk_eq_one_iff.mp h
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e : ↥I ⊗[R] ↥J ≃ₗ[R] R
⊢ I = ⊤ ∧ J = ⊤
have have : ∀ (e : R ≃ₗ[R] ↥(I * J)), I = ⊤ ∧ J = ⊤
Tactic: have e := e.symm ≪≫ₗ Submodule.LinearDisjoint.mulMap
    (.of_left_le_one_of_flat I J <| le_top.trans one_eq_top.ge)
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
⊢ Function.Injective (β := R) fun (x : R) ↦ x * (↑((e : (a : R) → ↥(I * J)) 1) : R)
have h₁ : ∀ (x : R),
  x * (↑((e : (a : R) → ↥(I * J)) 1) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
Tactic: convert! Subtype.val_injective.comp e.injective using 2
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
x : R
⊢ x * (↑((e : (a : R) → ↥(I * J)) 1) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
have h₁ : HSMul.hSMul (β := R) x (↑((e : (a : R) → ↥(I * J)) 1) : R) =
  Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
Tactic: rw [← smul_eq_mul, ← Submodule.coe_smul, ← map_smul, smul_eq_mul, mul_one, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
x : R
h₁ :
  HSMul.hSMul (β := R) x (↑((e : (a : R) → ↥(I * J)) 1) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
⊢ x * (↑((e : (a : R) → ↥(I * J)) 1) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
have h₂ : (↑(HSMul.hSMul (β := ↥(I * J)) x ((e : (a : R) → ↥(I * J)) 1)) : R) =
  Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
Tactic: rw [← smul_eq_mul, ← Submodule.coe_smul, ← map_smul, smul_eq_mul, mul_one, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
x : R
h₁ :
  HSMul.hSMul (β := R) x (↑((e : (a : R) → ↥(I * J)) 1) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
h₂ :
  (↑(HSMul.hSMul (β := ↥(I * J)) x ((e : (a : R) → ↥(I * J)) 1)) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
⊢ x * (↑((e : (a : R) → ↥(I * J)) 1) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
have h₃ : Eq (α := R) (↑((e : (a : R) → ↥(I * J)) (HSMul.hSMul (β := R) x 1)) : R)
  (Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x)
Tactic: rw [← smul_eq_mul, ← Submodule.coe_smul, ← map_smul, smul_eq_mul, mul_one, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
x : R
h₁ :
  HSMul.hSMul (β := R) x (↑((e : (a : R) → ↥(I * J)) 1) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
h₂ :
  (↑(HSMul.hSMul (β := ↥(I * J)) x ((e : (a : R) → ↥(I * J)) 1)) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
h₃ :
  Eq (α := R) (↑((e : (a : R) → ↥(I * J)) (HSMul.hSMul (β := R) x 1)) : R)
    (Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x)
⊢ x * (↑((e : (a : R) → ↥(I * J)) 1) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
have h₄ : Eq (α := R) (↑((e : (a : R) → ↥(I * J)) (x * 1)) : R)
  (Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x)
Tactic: rw [← smul_eq_mul, ← Submodule.coe_smul, ← map_smul, smul_eq_mul, mul_one, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
x : R
h₁ :
  HSMul.hSMul (β := R) x (↑((e : (a : R) → ↥(I * J)) 1) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
h₂ :
  (↑(HSMul.hSMul (β := ↥(I * J)) x ((e : (a : R) → ↥(I * J)) 1)) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
h₃ :
  Eq (α := R) (↑((e : (a : R) → ↥(I * J)) (HSMul.hSMul (β := R) x 1)) : R)
    (Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x)
h₄ :
  Eq (α := R) (↑((e : (a : R) → ↥(I * J)) (x * 1)) : R)
    (Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x)
⊢ x * (↑((e : (a : R) → ↥(I * J)) 1) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
have h₅ : Eq (α := R) (↑((e : (a : R) → ↥(I * J)) x) : R)
  (Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x)
Tactic: rw [← smul_eq_mul, ← Submodule.coe_smul, ← map_smul, smul_eq_mul, mul_one, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
x : R
h₁ :
  HSMul.hSMul (β := R) x (↑((e : (a : R) → ↥(I * J)) 1) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
h₂ :
  (↑(HSMul.hSMul (β := ↥(I * J)) x ((e : (a : R) → ↥(I * J)) 1)) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
h₃ :
  Eq (α := R) (↑((e : (a : R) → ↥(I * J)) (HSMul.hSMul (β := R) x 1)) : R)
    (Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x)
h₄ :
  Eq (α := R) (↑((e : (a : R) → ↥(I * J)) (x * 1)) : R)
    (Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x)
h₅ :
  Eq (α := R) (↑((e : (a : R) → ↥(I * J)) x) : R)
    (Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x)
⊢ x * (↑((e : (a : R) → ↥(I * J)) 1) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
have h₆ : Eq.{u_5 + 1} (α := R) (↑((e : (a : R) → ↥(I * J)) x) : R) (↑((e : (a : R) → ↥(I * J)) x) : R)
Tactic: rw [← smul_eq_mul, ← Submodule.coe_smul, ← map_smul, smul_eq_mul, mul_one, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (hypothesis)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
⊢ I = ⊤ ∧ J = ⊤
have this : IsUnit (M := R) (↑((e : (a : R) → ↥(I * J)) 1) : R)
Tactic: have : IsUnit (e 1 : R) := IsFractionRing.self_iff_nonZeroDivisors_le_isUnit.mp ‹_› <|
      IsRegular.mem_nonZeroDivisors <| isRightRegular_iff_isRegular.mp <| by
    rw [IsRightRegular]
    convert! Subtype.val_injective.comp e.injective using 2
    rw [← smul_eq_mul, ← Submodule.coe_smul, ← map_smul, smul_eq_mul, mul_one, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit (M := R) (↑((e : (a : R) → ↥(I * J)) 1) : R)
⊢ I = ⊤ ∧ J = ⊤
have left : I = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit (M := R) (↑((e : (a : R) → ↥(I * J)) 1) : R)
left : I = ⊤
⊢ I = ⊤ ∧ J = ⊤
have right : J = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit (M := R) (↑((e : (a : R) → ↥(I * J)) 1) : R)
⊢ I = ⊤
have left : (↑((e : (a : R) → ↥(I * J)) 1) : R) ∈ I
Tactic: refine eq_top_of_isUnit_mem _ ?_ this
-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit (M := R) (↑((e : (a : R) → ↥(I * J)) 1) : R)
⊢ J = ⊤
have right : (↑((e : (a : R) → ↥(I * J)) 1) : R) ∈ J
Tactic: refine eq_top_of_isUnit_mem _ ?_ this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
p : ℕ
h_1 : CharP R p
h : ∀ (x : ℕ), Eq.{u + 1} (α := R) (↑x : R) 0 ↔ p ∣ x
n : ℕ
⊢ Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ p ∣ n
have rw : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) 0 ↔ p ∣ n
Tactic: rw [← map_natCast C, ← C_0, C_inj, h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
p : ℕ
h_1 : CharP R p
h : ∀ (x : ℕ), Eq.{u + 1} (α := R) (↑x : R) 0 ↔ p ∣ x
n : ℕ
rw : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) 0 ↔ p ∣ n
⊢ Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ p ∣ n
have rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) ((C : (a : R) → R[X]) 0) ↔ p ∣ n
Tactic: rw [← map_natCast C, ← C_0, C_inj, h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
p : ℕ
h_1 : CharP R p
h : ∀ (x : ℕ), Eq.{u + 1} (α := R) (↑x : R) 0 ↔ p ∣ x
n : ℕ
rw : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) 0 ↔ p ∣ n
rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) ((C : (a : R) → R[X]) 0) ↔ p ∣ n
⊢ Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ p ∣ n
have rw₂ : Eq.{u + 1} (α := R) (↑n : R) 0 ↔ p ∣ n
Tactic: rw [← map_natCast C, ← C_0, C_inj, h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
p : ℕ
h_1 : CharP R p
h : ∀ (x : ℕ), Eq.{u + 1} (α := R) (↑x : R) 0 ↔ p ∣ x
n : ℕ
rw : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) 0 ↔ p ∣ n
rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) ((C : (a : R) → R[X]) 0) ↔ p ∣ n
rw₂ : Eq.{u + 1} (α := R) (↑n : R) 0 ↔ p ∣ n
⊢ Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ p ∣ n
have rw₃ : p ∣ n ↔ p ∣ n
Tactic: rw [← map_natCast C, ← C_0, C_inj, h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
p : ℕ
h : ExpChar R p
⊢ ExpChar.{u} R[X] p
have zero : ∀ [CharZero R], ExpChar.{u} R[X] 1
Tactic: cases h
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
p : ℕ
h : ExpChar R p
zero : ∀ [CharZero R], ExpChar.{u} R[X] 1
⊢ ExpChar.{u} R[X] p
have prime : Nat.Prime p → ∀ [CharP R p], ExpChar.{u} R[X] p
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : WithBot ℕ
f : R[X]
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLE R n) f ↔ f.degree ≤ n
have simp : (∀ (i : ℕ) (i_1 : (↑i : WithBot ℕ) > n), Eq (α := R) ((lcoeff R i : (a : R[X]) → R) f : R) (0 : R)) ↔
  ∀ (m : ℕ), n < (↑m : WithBot ℕ) → f.coeff m = 0
Tactic: simp only [degreeLE, Submodule.mem_iInf, degree_le_iff_coeff_zero, LinearMap.mem_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
⊢ degreeLE R (↑n : WithBot ℕ) =
    Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X])
have a : degreeLE R (↑n : WithBot ℕ) ≤
  Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X])
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
a :
  degreeLE R (↑n : WithBot ℕ) ≤
    Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X])
⊢ degreeLE R (↑n : WithBot ℕ) =
    Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X])
have a₁ : Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]) ≤
  degreeLE R (↑n : WithBot ℕ)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) p
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X])) p
have hp₁ : p.degree ≤ (↑n : WithBot ℕ)
Tactic: replace hp := mem_degreeLE.1 hp
Cleared hypotheses: hp