awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑s₁ : R) = r₃ * (↑s₂ : R)
c :
  HMul.hMul (β := T) (HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T))
      ((f : (a : R) → T) r₃ : T) =
    (↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T)
⊢ HMul.hMul (β := T)
      (HMul.hMul (β := T) (HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T))
        ((f : (a : R) → T) r₃ : T))
      ((f : (a : R) → T) r₂ : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)

Tactic:
congr 1
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑(s₃ * s₁) : R) = r₃ * (↑s₂ : R)
⊢ s₃ * s₁ = Subtype.mk (p := fun (a : R) ↦ a ∈ S) (r₃ * (↑s₂ : R)) ⋯

Tactic:
have h₃' := Subtype.coe_eq_of_eq_mk h₃
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑(s₃ * s₁) : R) = r₃ * (↑s₂ : R)
h₃' : s₃ * s₁ = Subtype.mk (p := fun (a : R) ↦ a ∈ S) (r₃ * (↑s₂ : R)) ⋯
c :
  HMul.hMul (α := T) (β := T)
      ((↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (a : R) ↦ a ∈ S) (r₃ * (↑s₂ : R)) ⋯))⁻¹ : T) : T)
      ((f : (a : R) → T) r₃ : T) =
    (↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T)
⊢ HMul.hMul (β := T) (HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T))
      ((f : (a : R) → T) r₃ : T) =
    (↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T)

Tactic:
rw [← Units.val_mul, ← mul_inv_rev, ← fS.map_mul, h₃']

Premises used: mul_inv_rev, MonoidHom.map_mul, Units.val_mul
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑(s₃ * s₁) : R) = r₃ * (↑s₂ : R)
h₃' : s₃ * s₁ = Subtype.mk (p := fun (a : R) ↦ a ∈ S) (r₃ * (↑s₂ : R)) ⋯
c :
  HMul.hMul (α := T) (β := T) ((f : (a : R) → T) r₃ : T) ((f : (a : R) → T) (↑s₂ : R) : T) =
    (f : (a : R) → T) (↑(Subtype.mk (p := fun (a : R) ↦ a ∈ S) (r₃ * (↑s₂ : R)) ⋯) : R)
⊢ HMul.hMul (α := T) (β := T)
      ((↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (a : R) ↦ a ∈ S) (r₃ * (↑s₂ : R)) ⋯))⁻¹ : T) : T)
      ((f : (a : R) → T) r₃ : T) =
    (↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T)

Tactic:
rw [Units.inv_mul_eq_iff_eq_mul, Units.eq_mul_inv_iff_mul_eq, ← hf, ← hf]

Premises used: Units.eq_mul_inv_iff_mul_eq, Units.inv_mul_eq_iff_eq_mul
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑(s₃ * s₁) : R) = r₃ * (↑s₂ : R)
h₃' : s₃ * s₁ = Subtype.mk (p := fun (a : R) ↦ a ∈ S) (r₃ * (↑s₂ : R)) ⋯
⊢ HMul.hMul (α := T) (β := T) ((f : (a : R) → T) r₃ : T) ((f : (a : R) → T) (↑s₂ : R) : T) =
    (f : (a : R) → T) (↑(Subtype.mk (p := fun (a : R) ↦ a ∈ S) (r₃ * (↑s₂ : R)) ⋯) : R)

Tactic:
simp only [map_mul]

Premises used: map_mul
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
T : Type u_3
inst_2 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r : R
s : ↥S
⊢ (universalHom f fS hf : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)

Tactic:
rfl

Premises used: OreLocalization.liftExpand, rfl
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
T : Type u_3
inst_2 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r : R
⊢ Eq.{u_3 + 1} (α := T)
    ((universalHom f fS hf : (a : OreLocalization S R) → T)
        ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) :
      T)
    ((f : (a : R) → T) r : T)

Tactic:
simp [numeratorHom_apply, universalHom_apply]

Premises used: OreLocalization.universalHom_apply, OreLocalization.numeratorHom_apply
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
T : Type u_3
inst_2 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
φ : RingHom.{u_1, u_3} (OreLocalization S R) T
huniv :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
      ((f : (a : R) → T) r : T)
⊢ φ = universalHom f fS hf

Tactic:
RingHom.coe_monoidHom_injective <| universalMulHom_unique (RingHom.toMonoidHom f) fS hf (↑φ) huniv

Premises used: MonoidHomClass.toMonoidHom, OreLocalization.universalMulHom_unique, RingHom.coe_monoidHom_injective, RingHom.toMonoidHom
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst_1 : Ring R
S : Submonoid R
inst_2 : OreSet S
X : Type u_2
inst_3 : AddCommGroup X
inst_4 : Module R X
n : ℤ
x : OreLocalization S X
inst : Module ℤ (OreLocalization S X) := instModuleOfIsScalarTower
⊢ n • x = n • x

Tactic:
congr($(AddCommGroup.uniqueIntModule.2 inst).smul n x)

Premises used: AddCommGroup.uniqueIntModule, congrArg, id, Unique.uniq, SMul.smul
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst_1 : Ring R
S : Submonoid R
inst_2 : OreSet S
X : Type u_2
inst_3 : AddCommGroup X
inst_4 : Module R X
n : ℤ
x : OreLocalization S X
inst : Module ℤ (OreLocalization S X) := instModuleOfIsScalarTower
⊢ n • x = n • x

Tactic:
exact congr($(AddCommGroup.uniqueIntModule.2 inst).smul n x)
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
inst_1 : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
h :
  Eq (α := OreLocalization S R) ((numeratorHom : (a : R) → OreLocalization S R) r₁ : OreLocalization S R)
    ((numeratorHom : (a : R) → OreLocalization S R) r₂ : OreLocalization S R)
⊢ ∃ (u : ↥S) (v : R), u • r₂ = v • r₁ ∧ (↑u : R) * (↑1 : R) = v * (↑1 : R)

Tactic:
rw [numeratorHom_apply, numeratorHom_apply, oreDiv_eq_iff] at h

Premises used: OreLocalization.oreDiv_eq_iff, OreLocalization.numeratorHom_apply
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
inst_1 : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
h : ∃ (u : ↥S) (v : R), u • r₂ = v • r₁ ∧ (↑u : R) * (↑1 : R) = v * (↑1 : R)
rcases : ∀ (u : ↥S) (v : R) (h₁ : u • r₂ = v • r₁) (h₂ : (↑u : R) * (↑1 : R) = v * (↑1 : R)), r₁ = r₂
⊢ r₁ = r₂

Tactic:
rcases h with ⟨u, v, h₁, h₂⟩
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
inst_1 : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
u : ↥S
v : R
h₁ : u • r₂ = v • r₁
h₂ : (↑u : R) * (↑1 : R) = v * (↑1 : R)
⊢ (↑u : R) = v

Tactic:
simp only [S.coe_one, mul_one, Submonoid.smul_def, smul_eq_mul] at h₁ h₂

Premises used: Submonoid.smul_def, Submonoid.coe_one, smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
inst_1 : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
u : ↥S
v : R
h₁ : (↑u : R) * r₂ = v * r₁
h₂ : (↑u : R) = v
⊢ (↑u : R) * (r₂ - r₁) = 0

Tactic:
rw [← h₂, ← sub_eq_zero, ← mul_sub] at h₁

Premises used: mul_sub, sub_eq_zero
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
inst_1 : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
u : ↥S
v : R
h₁ : (↑u : R) * r₂ = v * r₁
h₂ : (↑u : R) = v
h₃ : (↑u : R) * (r₂ - r₁) = 0
⊢ (↑u : R) = v

Tactic:
rw [← h₂, ← sub_eq_zero, ← mul_sub] at h₁

Premises used: mul_sub, sub_eq_zero
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
inst_1 : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
u : ↥S
v : R
h₁ : (↑u : R) * (r₂ - r₁) = 0
h₂ : (↑u : R) = v
⊢ r₁ = r₂

Tactic:
(sub_eq_zero.mp (hS u.2 _ h₁)).symm

Premises used: sub_eq_zero, Iff.mp, Eq.symm, Subtype.property
-- Module: Mathlib.RingTheory.OreLocalization.Ring
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
inst_1 : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
u : ↥S
v : R
h₁ : (↑u : R) * (r₂ - r₁) = 0
h₂ : (↑u : R) = v
⊢ r₁ = r₂

Tactic:
exact (sub_eq_zero.mp (hS u.2 _ h₁)).symm

Premises used: sub_eq_zero, Iff.mp, Eq.symm, Subtype.property
-- Module: Mathlib.RingTheory.OrzechProperty
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Type w
inst_5 : AddCommMonoid N
inst_6 : Module R N
i f : N →ₗ[R] M
hi : Injective.{w + 1, v + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
obtain :
  ∀ (n : ℕ) (g : (Fin n → R) →ₗ[R] M)
    (hg : Surjective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑g : (a : Fin n → R) → M)),
    Injective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
⊢ Injective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)

Tactic:
obtain ⟨n, g, hg⟩ := Module.Finite.exists_fin' R M

Premises used: Module.Finite.exists_fin'
-- Module: Mathlib.RingTheory.OrzechProperty
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Type w
inst_5 : AddCommMonoid N
inst_6 : Module R N
i f : N →ₗ[R] M
hi : Injective.{w + 1, v + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑g : (a : Fin n → R) → M)
⊢ Small.{u, v} M

Tactic:
haveI := small_of_surjective hg
-- Module: Mathlib.RingTheory.OrzechProperty
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Type w
inst_5 : AddCommMonoid N
inst_6 : Module R N
i f : N →ₗ[R] M
hi : Injective.{w + 1, v + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑g : (a : Fin n → R) → M)
this_1 : Small.{u, v} M
this_2 : AddCommMonoid (Shrink.{u, v} M) := Equiv.addCommMonoid (Equiv.symm (equivShrink M))
this : Module R (Shrink.{u, v} M) := Equiv.module R (Equiv.symm (equivShrink M))
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (Equiv.symm (equivShrink M))
⊢ Module.Finite R (Shrink.{u, v} M)

Tactic:
haveI := Module.Finite.equiv j.symm
-- Module: Mathlib.RingTheory.OrzechProperty
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Type w
inst_5 : AddCommMonoid N
inst_6 : Module R N
i f : N →ₗ[R] M
hi : Injective.{w + 1, v + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑g : (a : Fin n → R) → M)
this_1 : Small.{u, v} M
this_2 : AddCommMonoid (Shrink.{u, v} M) := Equiv.addCommMonoid (Equiv.symm (equivShrink M))
this_3 : Module R (Shrink.{u, v} M) := Equiv.module R (Equiv.symm (equivShrink M))
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (Equiv.symm (equivShrink M))
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := (↑j.symm : M →ₗ[R] Shrink.{u, v} M) ∘ₗ i
⊢ Injective.{w + 1, u + 1} (α := N) (β := Shrink.{u, v} M) (⇑i' : (a : N) → Shrink.{u, v} M)

Tactic:
simpa [i'] using hi
-- Module: Mathlib.RingTheory.OrzechProperty
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Type w
inst_5 : AddCommMonoid N
inst_6 : Module R N
i f : N →ₗ[R] M
hi : Injective.{w + 1, v + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑g : (a : Fin n → R) → M)
this_1 : Small.{u, v} M
this_2 : AddCommMonoid (Shrink.{u, v} M) := Equiv.addCommMonoid (Equiv.symm (equivShrink M))
this_3 : Module R (Shrink.{u, v} M) := Equiv.module R (Equiv.symm (equivShrink M))
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (Equiv.symm (equivShrink M))
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := (↑j.symm : M →ₗ[R] Shrink.{u, v} M) ∘ₗ i
⊢ Injective.{w + 1, u + 1} (α := N) (β := Shrink.{u, v} M) (⇑i' : (a : N) → Shrink.{u, v} M)

Tactic:
replace hi : Injective i' := by simpa [i'] using hi
-- Module: Mathlib.RingTheory.OrzechProperty
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Type w
inst_5 : AddCommMonoid N
inst_6 : Module R N
i f : N →ₗ[R] M
hf : Surjective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑g : (a : Fin n → R) → M)
this_1 : Small.{u, v} M
this_2 : AddCommMonoid (Shrink.{u, v} M) := Equiv.addCommMonoid (Equiv.symm (equivShrink M))
this_3 : Module R (Shrink.{u, v} M) := Equiv.module R (Equiv.symm (equivShrink M))
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (Equiv.symm (equivShrink M))
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := (↑j.symm : M →ₗ[R] Shrink.{u, v} M) ∘ₗ i
hi : Injective.{w + 1, u + 1} (α := N) (β := Shrink.{u, v} M) (⇑i' : (a : N) → Shrink.{u, v} M)
f' : ↥i'.range →ₗ[R] Shrink.{u, v} M :=
  (↑j.symm : M →ₗ[R] Shrink.{u, v} M) ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (LinearEquiv.ofInjective i' hi)) : ↥i'.range →ₗ[R] N)
⊢ Surjective (α := ↥i'.range) (β := Shrink.{u, v} M) (⇑f' : (a : ↥i'.range) → Shrink.{u, v} M)

Tactic:
simpa [f'] using hf
-- Module: Mathlib.RingTheory.OrzechProperty
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Type w
inst_5 : AddCommMonoid N
inst_6 : Module R N
i f : N →ₗ[R] M
hf : Surjective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑g : (a : Fin n → R) → M)
this_1 : Small.{u, v} M
this_2 : AddCommMonoid (Shrink.{u, v} M) := Equiv.addCommMonoid (Equiv.symm (equivShrink M))
this_3 : Module R (Shrink.{u, v} M) := Equiv.module R (Equiv.symm (equivShrink M))
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (Equiv.symm (equivShrink M))
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := (↑j.symm : M →ₗ[R] Shrink.{u, v} M) ∘ₗ i
hi : Injective.{w + 1, u + 1} (α := N) (β := Shrink.{u, v} M) (⇑i' : (a : N) → Shrink.{u, v} M)
f' : ↥i'.range →ₗ[R] Shrink.{u, v} M :=
  (↑j.symm : M →ₗ[R] Shrink.{u, v} M) ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (LinearEquiv.ofInjective i' hi)) : ↥i'.range →ₗ[R] N)
⊢ Surjective (α := ↥i'.range) (β := Shrink.{u, v} M) (⇑f' : (a : ↥i'.range) → Shrink.{u, v} M)

Tactic:
replace hf : Surjective f' := by simpa [f'] using hf
-- Module: Mathlib.RingTheory.OrzechProperty
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Type w
inst_5 : AddCommMonoid N
inst_6 : Module R N
i f : N →ₗ[R] M
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑g : (a : Fin n → R) → M)
this_1 : Small.{u, v} M
this_2 : AddCommMonoid (Shrink.{u, v} M) := Equiv.addCommMonoid (Equiv.symm (equivShrink M))
this_3 : Module R (Shrink.{u, v} M) := Equiv.module R (Equiv.symm (equivShrink M))
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (Equiv.symm (equivShrink M))
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := (↑j.symm : M →ₗ[R] Shrink.{u, v} M) ∘ₗ i
hi : Injective.{w + 1, u + 1} (α := N) (β := Shrink.{u, v} M) (⇑i' : (a : N) → Shrink.{u, v} M)
f' : ↥i'.range →ₗ[R] Shrink.{u, v} M :=
  (↑j.symm : M →ₗ[R] Shrink.{u, v} M) ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (LinearEquiv.ofInjective i' hi)) : ↥i'.range →ₗ[R] N)
hf : Surjective (α := ↥i'.range) (β := Shrink.{u, v} M) (⇑f' : (a : ↥i'.range) → Shrink.{u, v} M)
⊢ Injective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)

Tactic:
simpa [f'] using injective_of_surjective_of_submodule' f' hf

Premises used: OrzechProperty.injective_of_surjective_of_submodule'
-- Module: Mathlib.RingTheory.OrzechProperty
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Type w
inst_5 : AddCommMonoid N
inst_6 : Module R N
i f : N →ₗ[R] M
hi : Injective.{w + 1, v + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
⊢ Bijective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)

Tactic:
⟨OrzechProperty.injective_of_surjective_of_injective _ _ hi hf, hf⟩

Premises used: OrzechProperty.injective_of_surjective_of_injective, And.intro, Function.Bijective
-- Module: Mathlib.RingTheory.OrzechProperty
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)
⊢ Injective (α := ↥N) (β := M) (⇑f : (a : ↥N) → M)

Tactic:
injective_of_surjective_of_injective N.subtype f N.injective_subtype hf

Premises used: OrzechProperty.injective_of_surjective_of_injective, Submodule.injective_subtype, Submodule.subtype
-- Module: Mathlib.RingTheory.OrzechProperty
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
hf : Surjective (α := M) (β := M) (⇑f : (a : M) → M)
⊢ Injective (α := M) (β := M) (⇑f : (a : M) → M)

Tactic:
injective_of_surjective_of_injective _ f (LinearEquiv.refl _ _).injective hf

Premises used: OrzechProperty.injective_of_surjective_of_injective, LinearEquiv.refl, LinearEquiv.injective
-- Module: Mathlib.RingTheory.OrzechProperty
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
hf : Surjective (α := M) (β := M) (⇑f : (a : M) → M)
⊢ Bijective (α := M) (β := M) (⇑f : (a : M) → M)

Tactic:
⟨injective_of_surjective_endomorphism f hf, hf⟩

Premises used: And.intro, Function.Bijective, OrzechProperty.injective_of_surjective_endomorphism
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f g : Perfection M p
h :
  ∀ (n : ℕ),
    Eq (α := M) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
      ((coeffMonoidHom M p n : (a : Perfection M p) → M) g : M)
⊢ f = g

Tactic:
Subtype.ext <| funext h

Premises used: Perfection, funext, Subtype.ext
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : ℕ → M
hf : ∀ (n : ℕ), f (n + 1) ^ p = f n
n : ℕ
⊢ (coeffMonoidHom M p n : (a : Perfection M p) → M)
      (Subtype.mk (p := fun (f : ℕ → M) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n) f hf) =
    f n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n : ℕ
⊢ Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) f : Perfection M p) :
      M)
    ((coeffMonoidHom M p (n + 1) : (a : Perfection M p) → M) f : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n : ℕ
rw :
  HPow.hPow (α := M) ((coeffMonoidHom M p (n + 1) : (a : Perfection M p) → M) f : M) p =
    (coeffMonoidHom M p n : (a : Perfection M p) → M) f
⊢ Eq (α := M) ((coeffMonoidHom M p (n + 1) : (a : Perfection M p) → M) (f ^ p) : M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)

Tactic:
rw [map_pow]

Premises used: map_pow
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n : ℕ
⊢ HPow.hPow (α := M) ((coeffMonoidHom M p (n + 1) : (a : Perfection M p) → M) f : M) p =
    (coeffMonoidHom M p n : (a : Perfection M p) → M) f

Tactic:
f.2 n

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n : ℕ
⊢ HPow.hPow (α := M) ((coeffMonoidHom M p (n + 1) : (a : Perfection M p) → M) f : M) p =
    (coeffMonoidHom M p n : (a : Perfection M p) → M) f

Tactic:
exact f.2 n

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
x : Perfection M p
h :
  ∀ (n : ℕ),
    Eq (α := M)
      ((coeffMonoidHom M p n : (a : Perfection M p) → M)
          ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) ((fun (x : Perfection M p) ↦ x ^ p) x)) :
        M)
      ((coeffMonoidHom M p n : (a : Perfection M p) → M) x : M)
⊢ (pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) ((fun (x : Perfection M p) ↦ x ^ p) x) = x

Tactic:
ext
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
x : Perfection M p
n : ℕ
⊢ Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) ((fun (x : Perfection M p) ↦ x ^ p) x)) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) x : M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
x : Perfection M p
h :
  ∀ (n : ℕ),
    Eq (α := M)
      ((coeffMonoidHom M p n : (a : Perfection M p) → M)
          ((fun (x : Perfection M p) ↦ x ^ p) ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) x)) :
        M)
      ((coeffMonoidHom M p n : (a : Perfection M p) → M) x : M)
⊢ (fun (x : Perfection M p) ↦ x ^ p) ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) x) = x

Tactic:
ext
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
x : Perfection M p
n : ℕ
⊢ Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((fun (x : Perfection M p) ↦ x ^ p) ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) x)) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) x : M)

Tactic:
simp