awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p : Submodule R M
inst_4 : Module R₂ M₂
e : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥⊥
b : M
hb : b ∈ p
⊢ Eq.{u_7 + 1} (α := ↥⊥) ((e : (a : ↥p) → ↥⊥) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) b hb) : ↥⊥) (0 : ↥⊥)

Tactic:
apply Submodule.eq_zero_of_bot_submodule

Premises used: Submodule.eq_zero_of_bot_submodule
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M : Module R M
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
h : M₂ →ₛₗ[σ₂₃] M₃
inst_7 : RingHomSurjective σ₂₃
inst_8 : RingHomSurjective σ₁₃
⊢ (h ∘ₛₗ (↑e : M →ₛₗ[σ₁₂] M₂)).range = h.range

Tactic:
LinearMap.range_comp_of_range_eq_top _ e.range

Premises used: LinearMap.range_comp_of_range_eq_top, LinearEquiv.range
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M : Module R M
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
f : M →ₛₗ[σ₁₂] M₂
g_1 : M₂ →ₛₗ[σ₂₁] M
e : M ≃ₛₗ[σ₁₂] M₂
h_1 : M₂ →ₛₗ[σ₂₃] M₃
p q : Submodule R M
inst_7 : RingHomInvPair σ₁₂ σ₂₁
inst_8 : RingHomInvPair σ₂₁ σ₁₂
g : M₂ → M
h : LeftInverse g (⇑f : (a : M) → M₂)
x : ↥f.range
x' : M
hx' : (f : (a : M) → M₂) x' = (↑x : M₂)
rw : Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) (g ((f : (a : M) → M₂) x')) : M₂) ((f : (a : M) → M₂) x' : M₂)
rw₁ rw₂ : Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x' : M₂) ((f : (a : M) → M₂) x' : M₂)
⊢ (f : (a : M) → M₂) (g (↑x : M₂)) = (↑x : M₂)

Tactic:
rw [← hx', h x']
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₁] M
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
h : LeftInverse.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑g : (a : M₂) → M) (⇑f : (a : M) → M₂)
x : M
⊢ Eq.{u_7 + 1} (α := M₂)
    ((↑(((ofLeftInverse h : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ M ↥f.range) : (a : M) → ↥f.range) x) : M₂) : M₂)
    ((f : (a : M) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₁] M
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
h : LeftInverse.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑g : (a : M₂) → M) (⇑f : (a : M) → M₂)
x : ↥f.range
⊢ Eq.{u_5 + 1} (α := M) ((symm (ofLeftInverse h) : (a : ↥f.range) → M) x : M) ((g : (a : M₂) → M) (↑x : M₂) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
h : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
x : M
⊢ Eq.{u_7 + 1} (α := M₂)
    ((↑(((ofInjective f h : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ M ↥f.range) : (a : M) → ↥f.range) x) : M₂) : M₂)
    ((f : (a : M) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
h : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
x : ↥f.range
obtain :
  ∀ (y : M),
    Eq.{u_7 + 1} (α := M₂)
      ((f : (a : M) → M₂)
          ((symm (ofInjective f h) : (a : ↥f.range) → M)
              (Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) y) ⋯ : ↥f.range) :
            M) :
        M₂)
      ((↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) y) ⋯) : M₂) : M₂)
⊢ (f : (a : M) → M₂) ((symm (ofInjective f h) : (a : ↥f.range) → M) x : M) = (↑x : M₂)

Tactic:
obtain ⟨-, ⟨y, rfl⟩⟩ := x

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
h : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
y : M
⊢ Eq.{u_7 + 1} (α := ↥f.range) (Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) y) ⋯ : ↥f.range)
    (((ofInjective f h : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ M ↥f.range) : (a : M) → ↥f.range) y : ↥f.range)

Tactic:
have : ⟨f y, LinearMap.mem_range_self f y⟩ = LinearEquiv.ofInjective f h y := rfl
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
h : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
y : M
this :
  Eq.{u_7 + 1} (α := ↥f.range) (Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) y) ⋯ : ↥f.range)
    (((ofInjective f h : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ M ↥f.range) : (a : M) → ↥f.range) y : ↥f.range)
⊢ Eq.{u_7 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        ((symm (ofInjective f h) : (a : ↥f.range) → M)
            (Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) y) ⋯ : ↥f.range) :
          M) :
      M₂)
    ((↑(Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) y) ⋯) : M₂) : M₂)

Tactic:
simp [this]
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
hf : Bijective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
x : M
⊢ Eq.{u_7 + 1} (α := M₂) ((ofBijective f hf : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
h : Bijective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
x : M
⊢ (symm (ofBijective f h) : (a : M₂) → M) ((f : (a : M) → M₂) x : M₂) = x

Tactic:
simp [LinearEquiv.symm_apply_eq]

Premises used: LinearEquiv.symm_apply_eq
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
h : Bijective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
x : M₂
rw : (ofBijective f h : (a : M) → M₂) ((symm (ofBijective f h) : (a : M₂) → M) x : M) = x
rw₁ rw₂ : x = x
⊢ (f : (a : M) → M₂) ((symm (ofBijective f h) : (a : M₂) → M) x : M) = x

Tactic:
rw [← ofBijective_apply f (hf := h) ((ofBijective f h).symm x), apply_symm_apply]

Premises used: LinearEquiv.symm, LinearEquiv.ofBijective_apply, LinearEquiv.apply_symm_apply, DFunLike.coe, LinearEquiv.ofBijective
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
p : Submodule R M
q : Submodule R ↥p
x : ↥p
hx : x ∈ q
⊢ Membership.mem (α := M) (map p.subtype q)
    ((p.subtype.domRestrict q : (a : ↥q) → M) (Subtype.mk (p := fun (x : ↥p) ↦ x ∈ q) x hx) : M)

Tactic:
⟨x, hx, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
p : Submodule R M
q : Submodule R ↥p
x : ↥p
hx : x ∈ q
⊢ Membership.mem (α := M) (map p.subtype q)
    ((p.subtype.domRestrict q : (a : ↥q) → M) (Subtype.mk (p := fun (x : ↥p) ↦ x ∈ q) x hx) : M)

Tactic:
exact ⟨x, hx, rfl⟩
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
refine_1 : x ∈ p
refine_2 : Subtype.mk (p := fun (x : M) ↦ x ∈ p) x ⋯ ∈ q
⊢ ↥q

Tactic:
refine ⟨⟨x, ?_⟩, ?_⟩
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
refine_1 :
  ∀ (val : M) (h : val ∈ p),
    Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h ∈ (↑q : Set ↥p) →
      Membership.mem (α := M) p ((p.subtype : (a : ↥p) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h) : M)
⊢ x ∈ p

Tactic:
rcases hx with ⟨⟨_, h⟩, _, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
refine_2 :
  ∀ (val : M) (h : val ∈ p) (left : Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h ∈ (↑q : Set ↥p)),
    Membership.mem (α := ↥p) q
      (Subtype.mk (p := fun (x : M) ↦ x ∈ p) ((p.subtype : (a : ↥p) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h))
          ⋯ :
        ↥p)
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ p) x ⋯ ∈ q

Tactic:
rcases hx with ⟨⟨_, h⟩, _, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
p : Submodule R M
q : Submodule R ↥p
val : M
h : val ∈ p
left : Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h ∈ (↑q : Set ↥p)
⊢ Membership.mem (α := M) p ((p.subtype : (a : ↥p) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h) : M)

Tactic:
assumption
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
p : Submodule R M
q : Submodule R ↥p
val : M
h : val ∈ p
left : Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h ∈ (↑q : Set ↥p)
⊢ Membership.mem (α := ↥p) q
    (Subtype.mk (p := fun (x : M) ↦ x ∈ p) ((p.subtype : (a : ↥p) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) val h))
        ⋯ :
      ↥p)

Tactic:
assumption
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
q : Submodule R ↥p
x : ↥q
⊢ Eq (α := M) ((↑((p.equivSubtypeMap q : (a : ↥q) → ↥(map p.subtype q)) x) : M) : M)
    ((p.subtype.domRestrict q : (a : ↥q) → M) x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
q : Submodule R ↥p
x : ↥(map p.subtype q)
⊢ (↑(↑(((p.equivSubtypeMap q).symm : (a : ↥(map p.subtype q)) → ↥q) x) : ↥p) : M) = (↑x : M)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
p : Submodule R N
hf : Injective.{u_5 + 1, u_9 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
h : p ≤ f.range
x y : ↥(comap f p)
hxy :
  Eq.{u_9 + 1} (α := ↥p) ((LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯ : (a : ↥(comap f p)) → ↥p) x : ↥p)
    ((LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯ : (a : ↥(comap f p)) → ↥p) y : ↥p)
⊢ x = y

Tactic:
simpa using hf (Subtype.ext_iff.mp hxy)

Premises used: Subtype.ext_iff, Iff.mp
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
p : Submodule R N
hf : Injective.{u_5 + 1, u_9 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
h : p ≤ f.range
x_1 : ↥p
x : N
hx : x ∈ p
obtain :
  ∀ (y : M) (hx : Membership.mem (α := N) p ((f : (a : M) → N) y : N)),
    ∃ (a : ↥(comap f p)),
      Eq.{u_9 + 1} (α := ↥p) ((LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯ : (a : ↥(comap f p)) → ↥p) a : ↥p)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ p) ((f : (a : M) → N) y) hx : ↥p)
⊢ ∃ (a : ↥(comap f p)),
    (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯ : (a : ↥(comap f p)) → ↥p) a =
      Subtype.mk (p := fun (x : N) ↦ x ∈ p) x hx

Tactic:
obtain ⟨y, rfl⟩ := h hx

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
p : Submodule R N
hf : Injective.{u_5 + 1, u_9 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
h : p ≤ f.range
x : ↥p
y : M
hx : Membership.mem (α := N) p ((f : (a : M) → N) y : N)
⊢ Eq.{u_9 + 1} (α := ↥p)
    ((LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯ : (a : ↥(comap f p)) → ↥p)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ comap f p) y hx) :
      ↥p)
    (Subtype.mk (p := fun (x : N) ↦ x ∈ p) ((f : (a : M) → N) y) hx : ↥p)

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
p : Submodule R N
hf : Injective.{u_5 + 1, u_9 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
h : p ≤ f.range
x : ↥p
y : M
hx : Membership.mem (α := N) p ((f : (a : M) → N) y : N)
⊢ ∃ (a : ↥(comap f p)),
    Eq.{u_9 + 1} (α := ↥p) ((LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯ : (a : ↥(comap f p)) → ↥p) a : ↥p)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ p) ((f : (a : M) → N) y) hx : ↥p)

Tactic:
exact ⟨⟨y, hx⟩, by simp [Subtype.ext_iff]⟩
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M₁ →ₗ[R] M₂
i : M₃ →ₗ[R] M₂
hi : Injective.{u_8 + 1, u_7 + 1} (α := M₃) (β := M₂) (⇑i : (a : M₃) → M₂)
hf : ∀ (x : M₁), Membership.mem (α := M₂) i.range ((f : (a : M₁) → M₂) x : M₂)
x : M₁
⊢ Eq.{u_7 + 1} (α := M₂) ((i : (a : M₃) → M₂) ((f.codRestrictOfInjective i hi hf : (a : M₁) → M₃) x : M₃) : M₂)
    ((f : (a : M₁) → M₂) x : M₂)

Tactic:
simp [LinearMap.codRestrictOfInjective]

Premises used: LinearMap.codRestrictOfInjective
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M₁ →ₗ[R] M₂
i : M₃ →ₗ[R] M₂
hi : Injective.{u_8 + 1, u_7 + 1} (α := M₃) (β := M₂) (⇑i : (a : M₃) → M₂)
hf : ∀ (x : M₁), Membership.mem (α := M₂) i.range ((f : (a : M₁) → M₂) x : M₂)
h :
  ∀ (x : M₁),
    Eq.{u_7 + 1} (α := M₂) ((i ∘ₗ f.codRestrictOfInjective i hi hf : (a : M₁) → M₂) x : M₂) ((f : (a : M₁) → M₂) x : M₂)
⊢ i ∘ₗ f.codRestrictOfInjective i hi hf = f

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M₁ →ₗ[R] M₂
i : M₃ →ₗ[R] M₂
hi : Injective.{u_8 + 1, u_7 + 1} (α := M₃) (β := M₂) (⇑i : (a : M₃) → M₂)
hf : ∀ (x : M₁), Membership.mem (α := M₂) i.range ((f : (a : M₁) → M₂) x : M₂)
x : M₁
⊢ Eq.{u_7 + 1} (α := M₂) ((i ∘ₗ f.codRestrictOfInjective i hi hf : (a : M₁) → M₂) x : M₂) ((f : (a : M₁) → M₂) x : M₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Module R M
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective.{u_8 + 1, u_5 + 1} (α := M₃) (β := M) (⇑i : (a : M₃) → M)
hf :
  ∀ (x : M₁) (y : M₂),
    Membership.mem (α := M) i.range ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M)
e : LinearEquiv.{u_1, u_1, u_5, u_8} (RingHom.id R) (↥i.range) M₃ := LinearEquiv.symm (LinearEquiv.ofInjective i hi)
x₁ x₂ : M₁
h :
  ∀ (y : M₂),
    Eq.{u_8 + 1} (α := M₃)
      (((↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) (x₁ + x₂)) ⋯ : (a : M₂) → M₃) y :
        M₃)
      (((↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) x₁) ⋯ +
              (↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) x₂) ⋯ :
            (a : M₂) → M₃)
          y :
        M₃)
⊢ (↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) (x₁ + x₂)) ⋯ =
    (↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) x₁) ⋯ +
      (↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) x₂) ⋯

Tactic:
ext y
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Module R M
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective.{u_8 + 1, u_5 + 1} (α := M₃) (β := M) (⇑i : (a : M₃) → M)
hf :
  ∀ (x : M₁) (y : M₂),
    Membership.mem (α := M) i.range ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M)
e : LinearEquiv.{u_1, u_1, u_5, u_8} (RingHom.id R) (↥i.range) M₃ := LinearEquiv.symm (LinearEquiv.ofInjective i hi)
x₁ x₂ : M₁
y : M₂
⊢ Eq.{u_8 + 1} (α := M₃)
    (((↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) (x₁ + x₂)) ⋯ : (a : M₂) → M₃) y : M₃)
    (((↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) x₁) ⋯ +
            (↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) x₂) ⋯ :
          (a : M₂) → M₃)
        y :
      M₃)

Tactic:
simp [f.map_add, ← e.map_add, codRestrict]

Premises used: LinearMap.map_add, LinearEquiv.map_add, LinearMap.codRestrict
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Module R M
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective.{u_8 + 1, u_5 + 1} (α := M₃) (β := M) (⇑i : (a : M₃) → M)
hf :
  ∀ (x : M₁) (y : M₂),
    Membership.mem (α := M) i.range ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M)
e : LinearEquiv.{u_1, u_1, u_5, u_8} (RingHom.id R) (↥i.range) M₃ := LinearEquiv.symm (LinearEquiv.ofInjective i hi)
t : R
x : M₁
h :
  ∀ (y : M₂),
    Eq.{u_8 + 1} (α := M₃)
      (((↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) (t • x)) ⋯ : (a : M₂) → M₃) y : M₃)
      ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) t : R)
              ((↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) x) ⋯) :
            (a : M₂) → M₃)
          y :
        M₃)
⊢ (↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) (t • x)) ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) t : R)
      ((↑e : ↥i.range →ₗ[R] M₃) ∘ₗ codRestrict i.range ((f : (a : M₁) → M₂ →ₗ[R] M) x) ⋯)

Tactic:
ext y
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Module R M
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective.{u_8 + 1, u_5 + 1} (α := M₃) (β := M) (⇑i : (a : M₃) → M)
hf :
  ∀ (x : M₁) (y : M₂),
    Membership.mem (α := M) i.range ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M)
x : M₁
y : M₂
⊢ Eq.{u_5 + 1} (α := M)
    ((i : (a : M₃) → M) ((((f.codRestrict₂ i hi hf : (a : M₁) → M₂ →ₗ[R] M₃) x : M₂ →ₗ[R] M₃) : (a : M₂) → M₃) y : M₃) :
      M)
    ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M)

Tactic:
simp [codRestrict₂]

Premises used: LinearMap.codRestrict₂