awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x : M
⊢ x ∈ p.toAddSubgroup ↔ x ∈ p

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p p' : Submodule R M
⊢ p.toAddSubgroup = p'.toAddSubgroup ↔ p = p'

Tactic:
toAddSubgroup_injective.eq_iff

Premises used: Function.Injective.eq_iff, Submodule.toAddSubgroup_injective
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
⊢ x ∈ p → y ∈ p → x - y ∈ p

Tactic:
sub_mem

Premises used: sub_mem
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x : M
⊢ -x ∈ p ↔ x ∈ p

Tactic:
neg_mem_iff

Premises used: neg_mem_iff, Set.Mem
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
⊢ y ∈ p → (x + y ∈ p ↔ x ∈ p)

Tactic:
add_mem_cancel_right

Premises used: Set.Mem, add_mem_cancel_right
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
⊢ x ∈ p → (x + y ∈ p ↔ y ∈ p)

Tactic:
add_mem_cancel_left

Premises used: Set.Mem, add_mem_cancel_left
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x : ↥p
⊢ (↑(-x) : M) = -(↑x : M)

Tactic:
NegMemClass.coe_neg _

Premises used: NegMemClass.coe_neg
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : ↥p
⊢ (↑(x - y) : M) = (↑x : M) - (↑y : M)

Tactic:
AddSubgroupClass.coe_sub _ _

Premises used: AddSubgroupClass.coe_sub
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hy : y ∈ p
rw : x + -y ∈ p ↔ x ∈ p
rw₁ rw₂ : x ∈ p ↔ x ∈ p
⊢ x - y ∈ p ↔ x ∈ p

Tactic:
rw [sub_eq_add_neg, p.add_mem_iff_left (p.neg_mem hy)]

Premises used: sub_eq_add_neg, Submodule.neg_mem, Submodule.add_mem_iff_left
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hx : x ∈ p
rw : x + -y ∈ p ↔ y ∈ p
rw₁ : -y ∈ p ↔ y ∈ p
rw₂ rw₃ : y ∈ p ↔ y ∈ p
⊢ x - y ∈ p ↔ y ∈ p

Tactic:
rw [sub_eq_add_neg, p.add_mem_iff_right hx, p.neg_mem_iff]

Premises used: sub_eq_add_neg, Submodule.neg_mem_iff, Submodule.add_mem_iff_right
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x x_1 : S
x_2 : ↥t
a : (↑((x * x_1) • x_2) : M) = (↑(x • x_1 • x_2) : M)
⊢ (x * x_1) • x_2 = x • x_1 • x_2

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x x_1 : S
x_2 : ↥t
⊢ (↑((x * x_1) • x_2) : M) = (↑(x • x_1 • x_2) : M)

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x : ↥t
a : (↑(HSMul.hSMul.{u', v, v} (α := S) 1 x) : M) = (↑x : M)
⊢ HSMul.hSMul.{u', v, v} (α := S) 1 x = x

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x : ↥t
⊢ (↑(HSMul.hSMul.{u', v, v} (α := S) 1 x) : M) = (↑x : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x : S
a : (↑(HSMul.hSMul (β := ↥t) x 0) : M) = (↑0 : M)
⊢ HSMul.hSMul (β := ↥t) x 0 = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x : S
⊢ (↑(HSMul.hSMul (β := ↥t) x 0) : M) = (↑0 : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x : S
x_1 x_2 : ↥t
a : (↑(x • (x_1 + x_2)) : M) = (↑(x • x_1 + x • x_2) : M)
⊢ x • (x_1 + x_2) = x • x_1 + x • x_2

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x : S
x_1 x_2 : ↥t
⊢ (↑(x • (x_1 + x_2)) : M) = (↑(x • x_1 + x • x_2) : M)

Tactic:
simp [smul_add]

Premises used: smul_add
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x x_1 : S
x_2 : ↥t
a : (↑((x + x_1) • x_2) : M) = (↑(x • x_2 + x_1 • x_2) : M)
⊢ (x + x_1) • x_2 = x • x_2 + x_1 • x_2

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x x_1 : S
x_2 : ↥t
⊢ (↑((x + x_1) • x_2) : M) = (↑(x • x_2 + x_1 • x_2) : M)

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x : ↥t
a : (↑(HSMul.hSMul.{u', v, v} (α := S) 0 x) : M) = (↑0 : M)
⊢ HSMul.hSMul.{u', v, v} (α := S) 0 x = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
inst_7 : SetLike T M
inst_8 : AddSubmonoidClass T M
inst_9 : SMulMemClass T R M
t : T
x : ↥t
⊢ (↑(HSMul.hSMul.{u', v, v} (α := S) 0 x) : M) = (↑0 : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.EqLocus
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst_6 : FunLike F M M₂
inst_7 : SemilinearMapClass F τ₁₂ M M₂
f g : F
r : R
x : M
hx : Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)
⊢ Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) (r • x) : M₂) ((g : (a : M) → M₂) (r • x) : M₂)

Tactic:
simpa only [map_smulₛₗ _] using congr_arg (τ₁₂ r • ·) hx

Premises used: MulActionSemiHomClass.map_smulₛₗ, congr_arg, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.Algebra.Module.Submodule.EqLocus
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst_6 : FunLike F M M₂
inst_7 : SemilinearMapClass F τ₁₂ M M₂
x : M
f g : F
⊢ Membership.mem (γ := Submodule R M) (eqLocus f g) x ↔
    Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Module.Submodule.EqLocus
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst_6 : FunLike F M M₂
inst_7 : SemilinearMapClass F τ₁₂ M M₂
f g : F
⊢ Eq (α := AddSubmonoid M) (toAddSubmonoid (eqLocus f g)) (AddMonoidHom.eqLocusM (↑f : M →+ M₂) (↑g : M →+ M₂))

Tactic:
rfl

Premises used: AddMonoidHom.eqLocusM, setOf, rfl
-- Module: Mathlib.Algebra.Module.Submodule.EqLocus
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst_6 : FunLike F M M₂
inst_7 : SemilinearMapClass F τ₁₂ M M₂
f g : F
⊢ Eq (α := Submodule R M) (eqLocus f g) ⊤ ↔ f = g

Tactic:
simp [SetLike.ext_iff, DFunLike.ext_iff]

Premises used: SetLike.ext_iff, DFunLike.ext_iff
-- Module: Mathlib.Algebra.Module.Submodule.EqLocus
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst_6 : FunLike F M M₂
inst_7 : SemilinearMapClass F τ₁₂ M M₂
f : F
⊢ Eq (α := Submodule R M) (eqLocus f f) ⊤

Tactic:
eqLocus_eq_top.2 rfl

Premises used: Iff.mpr, LinearMap.eqLocus_eq_top, rfl
-- Module: Mathlib.Algebra.Module.Submodule.EqLocus
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst_6 : FunLike F M M₂
inst_7 : SemilinearMapClass F τ₁₂ M M₂
f g : F
S : Submodule R M
⊢ S ≤ eqLocus f g ↔ Set.EqOn.{u_3, u_4} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑S : Set M)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.EqOn
-- Module: Mathlib.Algebra.Module.Submodule.EqLocus
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst_6 : FunLike F M M₂
inst_7 : SemilinearMapClass F τ₁₂ M M₂
f g : F
S T : Submodule R M
hS : Set.EqOn.{u_3, u_4} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑S : Set M)
hT : Set.EqOn.{u_3, u_4} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑T : Set M)
⊢ S ≤ eqLocus f g

Tactic:
rw [← le_eqLocus] at hS hT ⊢

Premises used: LinearMap.le_eqLocus
-- Module: Mathlib.Algebra.Module.Submodule.EqLocus
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst_6 : FunLike F M M₂
inst_7 : SemilinearMapClass F τ₁₂ M M₂
f g : F
S T : Submodule R M
hS : Set.EqOn.{u_3, u_4} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑S : Set M)
hT : Set.EqOn.{u_3, u_4} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑T : Set M)
hS₁ : S ≤ eqLocus f g
⊢ T ≤ eqLocus f g

Tactic:
rw [← le_eqLocus] at hS hT ⊢

Premises used: LinearMap.le_eqLocus
-- Module: Mathlib.Algebra.Module.Submodule.EqLocus
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst_6 : FunLike F M M₂
inst_7 : SemilinearMapClass F τ₁₂ M M₂
f g : F
S T : Submodule R M
hS : S ≤ eqLocus f g
hT : T ≤ eqLocus f g
⊢ S ⊔ T ≤ eqLocus f g

Tactic:
sup_le hS hT

Premises used: sup_le
-- Module: Mathlib.Algebra.Module.Submodule.EqLocus
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst_6 : FunLike F M M₂
inst_7 : SemilinearMapClass F τ₁₂ M M₂
f g : F
S T : Submodule R M
hS : S ≤ eqLocus f g
hT : T ≤ eqLocus f g
⊢ S ⊔ T ≤ eqLocus f g

Tactic:
exact sup_le hS hT

Premises used: sup_le
-- Module: Mathlib.Algebra.Module.Submodule.EqLocus
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst_6 : FunLike F M M₂
inst_7 : SemilinearMapClass F τ₁₂ M M₂
f g : F
S T : Submodule R M
hST : Codisjoint S T
hS : Set.EqOn.{u_3, u_4} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑S : Set M)
hT : Set.EqOn.{u_3, u_4} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑T : Set M)
⊢ f = g

Tactic:
DFunLike.ext _ _ fun _ ↦ eqOn_sup hS hT <| hST.eq_top.symm ▸ trivial

Premises used: trivial, DFunLike.ext, Eq.rec, LinearMap.eqOn_sup, Eq.symm, Codisjoint.eq_top
-- Module: Mathlib.Algebra.Module.Submodule.EqLocus
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f g : M →ₛₗ[τ₁₂] M₂
⊢ eqLocus f g = (f - g).ker

Tactic:
SetLike.ext fun _ => sub_eq_zero.symm

Premises used: sub_eq_zero, SetLike.ext, Iff.symm
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
h : p = q
x : ↥p
⊢ (↑((ofEq p q h : (a : ↥p) → ↥q) x) : M) = (↑x : M)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
h : p = q
⊢ (ofEq p q h).symm = ofEq q p ⋯

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.ofEq, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
h : ∀ (x : ↥p), Eq.{u_5 + 1} (α := M) (↑((ofEq p p ⋯ : (a : ↥p) → ↥p) x) : M) (↑((refl R ↥p : (a : ↥p) → ↥p) x) : M)
⊢ ofEq p p ⋯ = refl R ↥p

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Equiv
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x : ↥p
⊢ Eq.{u_5 + 1} (α := M) (↑((ofEq p p ⋯ : (a : ↥p) → ↥p) x) : M) (↑((refl R ↥p : (a : ↥p) → ↥p) x) : M)

Tactic:
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
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
h : Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p = q
x : ↥p
⊢ Eq.{u_7 + 1} (α := M₂) ((↑((e.ofSubmodules p q h : (a : ↥p) → ↥q) x) : M₂) : M₂) ((e : (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
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
h : Submodule.map (↑e : M →ₛₗ[σ₁₂] M₂) p = q
x : ↥q
⊢ Eq.{u_5 + 1} (α := M) ((↑(((e.ofSubmodules p q h).symm : (a : ↥q) → ↥p) x) : M) : M)
    ((e.symm : (a : M₂) → M) (↑x : M₂) : 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_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
f : M ≃ₛₗ[σ₁₂] M₂
U : Submodule R₂ M₂
h :
  ∀ (x : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)),
    Eq.{u_7 + 1} (α := M₂)
      (↑(((↑(f.ofSubmodule' U) : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U) →ₛₗ[σ₁₂] ↥U) :
              (a : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)) → ↥U)
            x) :
        M₂)
      (↑(((LinearMap.codRestrict U ((↑f : M →ₛₗ[σ₁₂] M₂).domRestrict (Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)) ⋯ :
                LinearMap.{u_1, u_3, u_5, u_7} σ₁₂ ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U) ↥U) :
              (a : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)) → ↥U)
            x) :
        M₂)
⊢ (↑(f.ofSubmodule' U) : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U) →ₛₗ[σ₁₂] ↥U) =
    LinearMap.codRestrict U ((↑f : M →ₛₗ[σ₁₂] M₂).domRestrict (Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)) ⋯

Tactic:
ext
-- 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₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
f : M ≃ₛₗ[σ₁₂] M₂
U : Submodule R₂ M₂
x : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)
⊢ Eq.{u_7 + 1} (α := M₂)
    (↑(((↑(f.ofSubmodule' U) : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U) →ₛₗ[σ₁₂] ↥U) :
            (a : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)) → ↥U)
          x) :
      M₂)
    (↑(((LinearMap.codRestrict U ((↑f : M →ₛₗ[σ₁₂] M₂).domRestrict (Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)) ⋯ :
              LinearMap.{u_1, u_3, u_5, u_7} σ₁₂ ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U) ↥U) :
            (a : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)) → ↥U)
          x) :
      M₂)

Tactic:
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₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
f : M ≃ₛₗ[σ₁₂] M₂
U : Submodule R₂ M₂
x : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)
⊢ Eq.{u_7 + 1} (α := M₂) ((↑((f.ofSubmodule' U : (a : ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)) → ↥U) x) : M₂) : M₂)
    ((f : (a : M) → M₂) (↑x : M) : M₂)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, 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₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
f : M ≃ₛₗ[σ₁₂] M₂
U : Submodule R₂ M₂
x : ↥U
⊢ Eq.{u_5 + 1} (α := M)
    ((↑(((f.ofSubmodule' U).symm : (a : ↥U) → ↥(Submodule.comap (↑f : M →ₛₗ[σ₁₂] M₂) U)) x) : M) : M)
    ((f.symm : (a : M₂) → M) (↑x : M₂) : 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
module_M : Module R M
p : Submodule R M
h : p = ⊤
x : ↥p
⊢ (ofTop p h : (a : ↥p) → M) x = (↑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
module_M : Module R M
p : Submodule R M
h : p = ⊤
x : M
⊢ (↑(((ofTop p h).symm : (a : M) → ↥p) x) : M) = x

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
module_M : Module R M
p : Submodule R M
h : p = ⊤
x : M
⊢ Eq (α := ↥p) (((ofTop p h).symm : (a : M) → ↥p) x : ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x ⋯ : ↥p)

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
module_M : Module R M
p : Submodule R M
h : p = ⊤
⊢ (↑(ofTop p h) : ↥p →ₗ[R] M) = p.subtype

Tactic:
rfl

Premises used: Submodule.subtype, 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
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
⊢ (↑e : M →ₛₗ[σ₁₂] M₂).range = ⊤

Tactic:
LinearMap.range_eq_top.2 e.toEquiv.surjective

Premises used: Iff.mpr, LinearMap.range_eq_top, LinearEquiv.toEquiv, Equiv.surjective
-- 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 ↥⊥
⊢ p = ⊥

Tactic:
bot_unique (SetLike.le_def.2 fun b hb => (Submodule.mem_bot R).2 ?_)

Premises used: Iff.mpr, Submodule.mem_bot, SetLike.le_def, bot_unique
-- 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 ↥⊥
refine : ∀ (b : M) (hb : b ∈ p), b = 0
⊢ p = ⊥

Tactic:
refine bot_unique (SetLike.le_def.2 fun b hb => (Submodule.mem_bot R).2 ?_)

Premises used: Iff.mpr, Submodule.mem_bot, SetLike.le_def, bot_unique
-- 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
rw : Eq.{u_7 + 1} (α := ↥⊥) ((e : (a : ↥p) → ↥⊥) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) b hb) : ↥⊥) (0 : ↥⊥)
⊢ b = 0

Tactic:
rw [← p.mk_eq_zero hb, ← e.map_eq_zero_iff]

Premises used: LinearEquiv.map_eq_zero_iff, Submodule.mk_eq_zero