awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst_3 : CommSemiring R₀
inst_4 : Algebra R₀ R
inst_5 : AddCommMonoid M
inst_6 : Module R₀ M
inst_7 : Module R M
inst_8 : IsScalarTower R₀ R M
inst_9 : AddCommMonoid N
inst_10 : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM :
  Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑sM : (a : M) → M →₀ R)
sN : N →ₗ[R₀] N →₀ R₀
hsN :
  Function.LeftInverse (α := N) (β := N →₀ R₀) (⇑(linearCombination R₀ id) : (a : N →₀ R₀) → N)
    (⇑sN : (a : N) → N →₀ R₀)
this : Projective R (M ⊗[R₀] (N →₀ R₀))
H :
  ∀ (x : M) (x_1 : N),
    Eq (α := M ⊗[R₀] N)
      (((((AlgebraTensorModule.curry
                      ((AlgebraTensorModule.map LinearMap.id (linearCombination R₀ id) :
                          M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] N) ∘ₗ
                        (AlgebraTensorModule.map LinearMap.id sN : M ⊗[R₀] N →ₗ[R] M ⊗[R₀] (N →₀ R₀))) :
                    M →ₗ[R] N →ₗ[R₀] M ⊗[R₀] N) :
                  (a : M) → N →ₗ[R₀] M ⊗[R₀] N)
                x :
              N →ₗ[R₀] M ⊗[R₀] N) :
            (a : N) → M ⊗[R₀] N)
          x_1 :
        M ⊗[R₀] N)
      (((((AlgebraTensorModule.curry LinearMap.id : M →ₗ[R] N →ₗ[R₀] M ⊗[R₀] N) : (a : M) → N →ₗ[R₀] M ⊗[R₀] N) x :
              N →ₗ[R₀] M ⊗[R₀] N) :
            (a : N) → M ⊗[R₀] N)
          x_1 :
        M ⊗[R₀] N)
⊢ Eq (α := M ⊗[R₀] N →ₗ[R] M ⊗[R₀] N)
    ((AlgebraTensorModule.map LinearMap.id (linearCombination R₀ id) : M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] N) ∘ₗ
        (AlgebraTensorModule.map LinearMap.id sN : M ⊗[R₀] N →ₗ[R] M ⊗[R₀] (N →₀ R₀)) :
      M ⊗[R₀] N →ₗ[R] M ⊗[R₀] N)
    (LinearMap.id : M ⊗[R₀] N →ₗ[R] M ⊗[R₀] N)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst_3 : CommSemiring R₀
inst_4 : Algebra R₀ R
inst_5 : AddCommMonoid M
inst_6 : Module R₀ M
inst_7 : Module R M
inst_8 : IsScalarTower R₀ R M
inst_9 : AddCommMonoid N
inst_10 : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM :
  Function.LeftInverse (α := M) (β := M →₀ R) (⇑(linearCombination R id) : (a : M →₀ R) → M) (⇑sM : (a : M) → M →₀ R)
sN : N →ₗ[R₀] N →₀ R₀
hsN :
  Function.LeftInverse (α := N) (β := N →₀ R₀) (⇑(linearCombination R₀ id) : (a : N →₀ R₀) → N)
    (⇑sN : (a : N) → N →₀ R₀)
this : Projective R (M ⊗[R₀] (N →₀ R₀))
x : M
x_1 : N
⊢ Eq (α := M ⊗[R₀] N)
    (((((AlgebraTensorModule.curry
                    ((AlgebraTensorModule.map LinearMap.id (linearCombination R₀ id) :
                        M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] N) ∘ₗ
                      (AlgebraTensorModule.map LinearMap.id sN : M ⊗[R₀] N →ₗ[R] M ⊗[R₀] (N →₀ R₀))) :
                  M →ₗ[R] N →ₗ[R₀] M ⊗[R₀] N) :
                (a : M) → N →ₗ[R₀] M ⊗[R₀] N)
              x :
            N →ₗ[R₀] M ⊗[R₀] N) :
          (a : N) → M ⊗[R₀] N)
        x_1 :
      M ⊗[R₀] N)
    (((((AlgebraTensorModule.curry LinearMap.id : M →ₗ[R] N →ₗ[R₀] M ⊗[R₀] N) : (a : M) → N →ₗ[R₀] M ⊗[R₀] N) x :
            N →ₗ[R₀] M ⊗[R₀] N) :
          (a : N) → M ⊗[R₀] N)
        x_1 :
      M ⊗[R₀] N)

Tactic:
simp [hsN _]
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : Module R M] [inst_7 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
⊢ Projective R P

Tactic:
of_lifting_property'' (fun p hp ↦ ?_)

Premises used: Module.Projective.of_lifting_property''
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : Module R M] [inst_7 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
refine :
  ∀ (p : (P →₀ R) →ₗ[R] P) (hp : Function.Surjective (α := P →₀ R) (β := P) (⇑p : (a : P →₀ R) → P)),
    ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id
⊢ Projective R P

Tactic:
refine of_lifting_property'' (fun p hp ↦ ?_)

Premises used: Module.Projective.of_lifting_property''
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : Module R M] [inst_7 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective (α := P →₀ R) (β := P) (⇑p : (a : P →₀ R) → P)
e : (P →₀ Shrink.{v, u} R) ≃ₗ[R] P →₀ R := mapRange.linearEquiv (Shrink.linearEquiv R R)
rcases :
  ∀ (g : P →ₗ[R] P →₀ Shrink.{v, u} R) (hg : (p ∘ₗ (↑e : (P →₀ Shrink.{v, u} R) →ₗ[R] P →₀ R)) ∘ₗ g = LinearMap.id),
    ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id
⊢ ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id

Tactic:
rcases h (p ∘ₗ e.toLinearMap) LinearMap.id (hp.comp e.surjective) with ⟨g, hg⟩

Premises used: LinearMap.id, LinearEquiv.surjective, LinearMap.comp, LinearEquiv.toLinearMap, Function.Surjective.comp
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : Module R M] [inst_7 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective (α := P →₀ R) (β := P) (⇑p : (a : P →₀ R) → P)
e : (P →₀ Shrink.{v, u} R) ≃ₗ[R] P →₀ R := mapRange.linearEquiv (Shrink.linearEquiv R R)
g : P →ₗ[R] P →₀ Shrink.{v, u} R
hg : (p ∘ₗ (↑e : (P →₀ Shrink.{v, u} R) →ₗ[R] P →₀ R)) ∘ₗ g = LinearMap.id
⊢ ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id

Tactic:
⟨e.toLinearMap ∘ₗ g, hg⟩

Premises used: LinearMap.comp, LinearEquiv.toLinearMap, Exists.intro
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : Module R M] [inst_7 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective (α := P →₀ R) (β := P) (⇑p : (a : P →₀ R) → P)
e : (P →₀ Shrink.{v, u} R) ≃ₗ[R] P →₀ R := mapRange.linearEquiv (Shrink.linearEquiv R R)
g : P →ₗ[R] P →₀ Shrink.{v, u} R
hg : (p ∘ₗ (↑e : (P →₀ Shrink.{v, u} R) →ₗ[R] P →₀ R)) ∘ₗ g = LinearMap.id
⊢ ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id

Tactic:
exact ⟨e.toLinearMap ∘ₗ g, hg⟩
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Ring R
P : Type v
inst_1 : AddCommGroup P
inst_2 : Module R P
inst_3 : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst_4 : AddCommGroup M] [inst_5 : AddCommGroup N] [inst_6 : Module R M] [inst_7 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
⊢ Projective R P

Tactic:
of_lifting_property'' (fun p hp ↦ ?_)

Premises used: Module.Projective.of_lifting_property''
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Ring R
P : Type v
inst_1 : AddCommGroup P
inst_2 : Module R P
inst_3 : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst_4 : AddCommGroup M] [inst_5 : AddCommGroup N] [inst_6 : Module R M] [inst_7 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
refine :
  ∀ (p : (P →₀ R) →ₗ[R] P) (hp : Function.Surjective (α := P →₀ R) (β := P) (⇑p : (a : P →₀ R) → P)),
    ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id
⊢ Projective R P

Tactic:
refine of_lifting_property'' (fun p hp ↦ ?_)

Premises used: Module.Projective.of_lifting_property''
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Ring R
P : Type v
inst_1 : AddCommGroup P
inst_2 : Module R P
inst_3 : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst_4 : AddCommGroup M] [inst_5 : AddCommGroup N] [inst_6 : Module R M] [inst_7 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective (α := P →₀ R) (β := P) (⇑p : (a : P →₀ R) → P)
e : (P →₀ Shrink.{v, u} R) ≃ₗ[R] P →₀ R := mapRange.linearEquiv (Shrink.linearEquiv R R)
rcases :
  ∀ (g : P →ₗ[R] P →₀ Shrink.{v, u} R) (hg : (p ∘ₗ (↑e : (P →₀ Shrink.{v, u} R) →ₗ[R] P →₀ R)) ∘ₗ g = LinearMap.id),
    ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id
⊢ ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id

Tactic:
rcases h (p ∘ₗ e.toLinearMap) LinearMap.id (hp.comp e.surjective) with ⟨g, hg⟩

Premises used: LinearMap.id, LinearEquiv.surjective, LinearMap.comp, LinearEquiv.toLinearMap, Function.Surjective.comp
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Ring R
P : Type v
inst_1 : AddCommGroup P
inst_2 : Module R P
inst_3 : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst_4 : AddCommGroup M] [inst_5 : AddCommGroup N] [inst_6 : Module R M] [inst_7 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective (α := P →₀ R) (β := P) (⇑p : (a : P →₀ R) → P)
e : (P →₀ Shrink.{v, u} R) ≃ₗ[R] P →₀ R := mapRange.linearEquiv (Shrink.linearEquiv R R)
g : P →ₗ[R] P →₀ Shrink.{v, u} R
hg : (p ∘ₗ (↑e : (P →₀ Shrink.{v, u} R) →ₗ[R] P →₀ R)) ∘ₗ g = LinearMap.id
⊢ ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id

Tactic:
⟨e.toLinearMap ∘ₗ g, hg⟩

Premises used: LinearMap.comp, LinearEquiv.toLinearMap, Exists.intro
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Ring R
P : Type v
inst_1 : AddCommGroup P
inst_2 : Module R P
inst_3 : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst_4 : AddCommGroup M] [inst_5 : AddCommGroup N] [inst_6 : Module R M] [inst_7 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective (α := P →₀ R) (β := P) (⇑p : (a : P →₀ R) → P)
e : (P →₀ Shrink.{v, u} R) ≃ₗ[R] P →₀ R := mapRange.linearEquiv (Shrink.linearEquiv R R)
g : P →ₗ[R] P →₀ Shrink.{v, u} R
hg : (p ∘ₗ (↑e : (P →₀ Shrink.{v, u} R) →ₗ[R] P →₀ R)) ∘ₗ g = LinearMap.id
⊢ ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id

Tactic:
exact ⟨e.toLinearMap ∘ₗ g, hg⟩
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
⊢ Projective R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Projective.{u, w} R (M i)

Tactic:
⟨fun H i ↦ ?_, fun H ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
refine_1 : ∀ (H : Projective R (⨁ (i : ι), M i)) (i : ι), Projective.{u, w} R (M i)
refine_2 : ∀ (H : ∀ (i : ι), Projective.{u, w} R (M i)), Projective R (⨁ (i : ι), M i)
⊢ Projective R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Projective.{u, w} R (M i)

Tactic:
refine ⟨fun H i ↦ ?_, fun H ↦ ?_⟩
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
H : Projective R (⨁ (i : ι), M i)
i : ι
⊢ Eq (α := M i →ₗ[R] M i) (component R ι M i ∘ₗ lof R ι M i) LinearMap.id

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
H : Projective R (⨁ (i : ι), M i)
i : ι
⊢ Projective.{u, w} R (M i)

Tactic:
exact .of_split (DirectSum.lof ..) (DirectSum.component ..) (by simp)
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
H : ∀ (i : ι), Projective.{u, w} R (M i)
e : (⨁ (i : ι), M i) ≃ₗ[R] Π₀ (i : ι), M i := LinearEquiv.refl R (⨁ (i : ι), M i)
⊢ Projective R (⨁ (i : ι), M i)

Tactic:
Projective.of_equiv' e.symm

Premises used: LinearEquiv.symm, Module.Projective.of_equiv'
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
H : ∀ (i : ι), Projective.{u, w} R (M i)
e : (⨁ (i : ι), M i) ≃ₗ[R] Π₀ (i : ι), M i := LinearEquiv.refl R (⨁ (i : ι), M i)
⊢ Projective R (⨁ (i : ι), M i)

Tactic:
exact Projective.of_equiv' e.symm

Premises used: LinearEquiv.symm, Module.Projective.of_equiv'
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
refine_1 : ∀ (H : Projective R (⨁ (i : ι), M i)) (i : ι), Projective.{u, w} R (M i)
refine_2 refine_2₁ : ∀ (H : ∀ (i : ι), Projective.{u, w} R (M i)), Projective R (⨁ (i : ι), M i)
⊢ Projective R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Projective.{u, w} R (M i)

Tactic:
classical
  refine ⟨fun H i ↦ ?_, fun H ↦ ?_⟩
  · exact .of_split (DirectSum.lof ..) (DirectSum.component ..) (by simp)
  · let e : (⨁ i, M i) ≃ₗ[R] Π₀ i, M i := .refl ..
    exact Projective.of_equiv' e.symm
-- Module: Mathlib.Algebra.Module.Projective
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : ∀ (i : ι), Projective.{u, w} R (M i)
⊢ Projective R (⨁ (i : ι), M i)

Tactic:
directSum_iff.mpr ‹_›

Premises used: Iff.mpr, Module.Projective.directSum_iff
-- Module: Mathlib.Algebra.Module.Rat
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ≥0
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
rw₁ :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₂ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₃ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
rw₄ :
  (f : (a : M) → M₂)
      (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
rw₅ :
  (f : (a : M) → M₂)
      (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
      (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
rw₆ :
  HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.num : S)
      ((f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x) : M₂) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
      (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
rw₇ rw₈ :
  HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
      (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂)) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
      (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)

Tactic:
rw [NNRat.cast_def, NNRat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_natCast_smul f R S, map_inv_natCast_smul f R S]

Premises used: NNRat.cast_def, map_inv_natCast_smul, div_eq_mul_inv, map_natCast_smul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.Rat
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
rw₁ :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₂ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₃ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
rw₄ :
  (f : (a : M) → M₂)
      (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
rw₅ :
  (f : (a : M) → M₂)
      (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
      (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
rw₆ :
  HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.num : S)
      ((f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x) : M₂) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
      (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
rw₇ rw₈ :
  HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
      (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂)) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
      (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)

Tactic:
rw [Rat.cast_def, Rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_intCast_smul f R S, map_inv_natCast_smul f R S]

Premises used: map_inv_natCast_smul, div_eq_mul_inv, Rat.cast_def, map_intCast_smul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.Rat
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
_instM : Module ℚ≥0 M
_instM₂ : Module ℚ≥0 M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
c : ℚ≥0
x : M
⊢ (f : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂)

Tactic:
map_nnratCast_smul f ℚ≥0 ℚ≥0 c x

Premises used: NNRat, map_nnratCast_smul
-- Module: Mathlib.Algebra.Module.Rat
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
_instM : Module ℚ M
_instM₂ : Module ℚ M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
c : ℚ
x : M
⊢ (f : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x : M₂)

Tactic:
map_ratCast_smul f ℚ ℚ c x

Premises used: map_ratCast_smul, Rat
-- Module: Mathlib.Algebra.Module.Rat
Goal:
M : Type u_1
M₂ : Type u_2
E : Type u_3
inst : AddCommMonoid E
⊢ Subsingleton.{max (u_3 + 1) 1} (Module ℚ≥0 E)

Tactic:
⟨fun P Q => (Module.ext' P Q) fun r x =>
    map_nnrat_smul (_instM := P) (_instM₂ := Q) (AddMonoidHom.id E) r x⟩

Premises used: Module.ext', map_nnrat_smul, AddMonoidHom.id, Subsingleton.intro
-- Module: Mathlib.Algebra.Module.Rat
Goal:
M : Type u_1
M₂ : Type u_2
E : Type u_3
inst : AddCommGroup E
⊢ Subsingleton.{max (u_3 + 1) 1} (Module ℚ E)

Tactic:
⟨fun P Q => (Module.ext' P Q) fun r x =>
    map_rat_smul (_instM := P) (_instM₂ := Q) (AddMonoidHom.id E) r x⟩

Premises used: Module.ext', AddMonoidHom.id, Subsingleton.intro, map_rat_smul
-- Module: Mathlib.Algebra.Module.Rat
Goal:
E : Type u_3
R : Type u_4
S : Type u_5
inst : AddCommMonoid E
inst_1 : DivisionSemiring R
inst_2 : DivisionSemiring S
inst_3 : Module R E
inst_4 : Module S E
r : ℚ≥0
x : E
⊢ HSMul.hSMul.{u_4, u_3, u_3} (α := R) (↑r : R) x = HSMul.hSMul.{u_5, u_3, u_3} (α := S) (↑r : S) x

Tactic:
map_nnratCast_smul (AddMonoidHom.id E) R S r x

Premises used: AddMonoidHom.id, map_nnratCast_smul
-- Module: Mathlib.Algebra.Module.Rat
Goal:
E : Type u_3
R : Type u_4
S : Type u_5
inst : AddCommGroup E
inst_1 : DivisionRing R
inst_2 : DivisionRing S
inst_3 : Module R E
inst_4 : Module S E
r : ℚ
x : E
⊢ HSMul.hSMul.{u_4, u_3, u_3} (α := R) (↑r : R) x = HSMul.hSMul.{u_5, u_3, u_3} (α := S) (↑r : S) x

Tactic:
map_ratCast_smul (AddMonoidHom.id E) R S r x

Premises used: map_ratCast_smul, AddMonoidHom.id
-- Module: Mathlib.Algebra.Module.Rat
Goal:
M : Type u_1
R : Type u_3
inst : DivisionSemiring R
inst_1 : MulAction R M
inst_2 : MulAction ℚ≥0 M
inst_3 : IsScalarTower ℚ≥0 R M
q : ℚ≥0
x : M
rw : HSMul.hSMul (α := R) (β := R) (↑q : R) 1 • x = HSMul.hSMul (β := R) q 1 • x
⊢ HSMul.hSMul.{u_3, u_1, u_1} (α := R) (↑q : R) x = q • x

Tactic:
rw [← one_smul R x, ← smul_assoc, ← smul_assoc]

Premises used: smul_assoc, one_smul
-- Module: Mathlib.Algebra.Module.Rat
Goal:
M : Type u_1
R : Type u_3
inst : DivisionSemiring R
inst_1 : MulAction R M
inst_2 : MulAction ℚ≥0 M
inst_3 : IsScalarTower ℚ≥0 R M
q : ℚ≥0
x : M
⊢ HSMul.hSMul (α := R) (β := R) (↑q : R) 1 • x = HSMul.hSMul (β := R) q 1 • x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Rat
Goal:
M : Type u_1
R : Type u_3
inst : DivisionRing R
inst_1 : MulAction R M
inst_2 : MulAction ℚ M
inst_3 : IsScalarTower ℚ R M
q : ℚ
x : M
rw : HSMul.hSMul (α := R) (β := R) (↑q : R) 1 • x = HSMul.hSMul (β := R) q 1 • x
⊢ HSMul.hSMul.{u_3, u_1, u_1} (α := R) (↑q : R) x = q • x

Tactic:
rw [← one_smul R x, ← smul_assoc, ← smul_assoc]

Premises used: smul_assoc, one_smul
-- Module: Mathlib.Algebra.Module.Rat
Goal:
M : Type u_1
R : Type u_3
inst : DivisionRing R
inst_1 : MulAction R M
inst_2 : MulAction ℚ M
inst_3 : IsScalarTower ℚ R M
q : ℚ
x : M
⊢ HSMul.hSMul (α := R) (β := R) (↑q : R) 1 • x = HSMul.hSMul (β := R) q 1 • x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Rat
Goal:
M_1 : Type u_1
M₂ : Type u_2
α : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : DistribSMul α M
inst_2 : Module ℚ≥0 M
⊢ SMulCommClass α ℚ≥0 M

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.Algebra.Module.Rat
Goal:
M_1 : Type u_1
M₂ : Type u_2
α : Type u
M : Type v
inst : AddCommGroup M
inst_1 : DistribSMul α M
inst_2 : Module ℚ M
⊢ SMulCommClass α ℚ M

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.Algebra.Module.Rat
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
n : ℕ
hn : n ≠ 0
x y : M
hxy : Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ n • a) x) ((fun (a : M) ↦ n • a) y)
⊢ x = y

Tactic:
simpa [← Nat.cast_smul_eq_nsmul ℚ≥0 n, *] using congr((n⁻¹ : ℚ≥0) • $hxy)

Premises used: NNRat, Nat.cast, Inv.inv, Nat.cast_smul_eq_nsmul