awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p q : Submodule R M
⊢ map f (p ⊓ q) ≤ map f p ⊓ map f q

Tactic:
image_inter_subset f p q

Premises used: Set.Mem, setOf, Set.image_inter_subset, Set.inter, Set.Subset, SetLike.coe, Set.image, DFunLike.coe
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p q : Submodule R M
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ map f (p ⊓ q) = map f p ⊓ map f q

Tactic:
SetLike.coe_injective <| Set.image_inter hf

Premises used: Set.image_inter, SetLike.coe_injective
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
ι : Sort u_9
inst_7 : Nonempty ι
p : ι → Submodule R M
f : M →ₛₗ[σ₁₂] M₂
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ (↑(map f (⨅ (i : ι), p i)) : Set M₂) = (↑(⨅ (i : ι), map f (p i)) : Set M₂)

Tactic:
simpa only [map_coe, coe_iInf] using hf.injOn.image_iInter_eq

Premises used: Function.Injective.injOn, Set.InjOn.image_iInter_eq, Submodule.coe_iInf, Submodule.map_coe
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
N : Submodule R M
⊢ Set.Nonempty.{u_7} (α := Submodule R₂ M₂) (range fun (ϕ : M →ₛₗ[σ₁₂] M₂) ↦ map ϕ N)

Tactic:
⟨_, Set.mem_range.mpr ⟨0, rfl⟩⟩

Premises used: Iff.mpr, Set.mem_range, Set.Nonempty, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p_1 p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
x_1 y : ↥p
simp :
  Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
      (HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) (↑x_1 : M) : M₂) ((f : (a : M) → M₂) (↑y : M) : M₂)) ⋯ =
    HAdd.hAdd (α := ↥(map f p)) (β := ↥(map f p))
      (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
          ((f : (a : M) → M₂) (↑x_1 : M)) ⋯ :
        { x : M₂ // Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x })
      (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
          ((f : (a : M) → M₂) (↑y : M)) ⋯ :
        { x : M₂ // Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x })
⊢ (Equiv.Set.image (⇑f : (a : M) → M₂) (↑p : Set M) i).toFun (x_1 + y) =
    (Equiv.Set.image (⇑f : (a : M) → M₂) (↑p : Set M) i).toFun x_1 +
      (Equiv.Set.image (⇑f : (a : M) → M₂) (↑p : Set M) i).toFun y

Tactic:
simp only [coe_add, map_add, Equiv.toFun_as_coe, Equiv.Set.image_apply]

Premises used: Submodule.coe_add, Equiv.Set.image_apply, Equiv.toFun_as_coe, map_add
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p_1 p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
x_1 y : ↥p
⊢ Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
      (HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) (↑x_1 : M) : M₂) ((f : (a : M) → M₂) (↑y : M) : M₂)) ⋯ =
    HAdd.hAdd (α := ↥(map f p)) (β := ↥(map f p))
      (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
          ((f : (a : M) → M₂) (↑x_1 : M)) ⋯ :
        { x : M₂ // Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x })
      (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
          ((f : (a : M) → M₂) (↑y : M)) ⋯ :
        { x : M₂ // Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x })

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p_1 p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
m : R
x_1 : ↥p
simp :
  Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
      (HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := M₂) ((σ₁₂ : (a : R) → R₂) m : R₂)
        ((f : (a : M) → M₂) (↑x_1 : M) : M₂))
      ⋯ =
    HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := ↥(map f p)) ((σ₁₂ : (a : R) → R₂) m : R₂)
      (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
          ((f : (a : M) → M₂) (↑x_1 : M)) ⋯ :
        { x : M₂ // Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x })
⊢ (Equiv.Set.image (⇑f : (a : M) → M₂) (↑p : Set M) i).toFun (m • x_1) =
    HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) ((σ₁₂ : (a : R) → R₂) m : R₂)
      ((Equiv.Set.image (⇑f : (a : M) → M₂) (↑p : Set M) i).toFun x_1)

Tactic:
simp only [coe_smul_of_tower, map_smulₛₗ _, Equiv.toFun_as_coe, Equiv.Set.image_apply]

Premises used: Equiv.Set.image_apply, Equiv.toFun_as_coe, MulActionSemiHomClass.map_smulₛₗ, Submodule.coe_smul_of_tower
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p_1 p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
m : R
x_1 : ↥p
⊢ Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
      (HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := M₂) ((σ₁₂ : (a : R) → R₂) m : R₂)
        ((f : (a : M) → M₂) (↑x_1 : M) : M₂))
      ⋯ =
    HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := ↥(map f p)) ((σ₁₂ : (a : R) → R₂) m : R₂)
      (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
          ((f : (a : M) → M₂) (↑x_1 : M)) ⋯ :
        { x : M₂ // Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x })

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
x : ↥p
⊢ Eq.{u_7 + 1} (α := M₂)
    ((↑(((equivMapOfInjective f i p : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(map f p)) : (a : ↥p) → ↥(map f p)) x) :
        M₂) :
      M₂)
    ((f : (a : M) → M₂) (↑x : M) : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p_1 p' : Submodule R M
q q' : Submodule R₂ M₂
x_1 : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R₂ M₂
a : R
x : M
h : Membership.mem (γ := Set M) ((⇑f : (a : M) → M₂) ⁻¹' (↑p : Set M₂)) x
⊢ Membership.mem (γ := Set M) ((⇑f : (a : M) → M₂) ⁻¹' (↑p : Set M₂)) (a • x)

Tactic:
simp [p.smul_mem (σ₁₂ a) h, map_smulₛₗ _]

Premises used: MulActionSemiHomClass.map_smulₛₗ, DFunLike.coe, Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R₂ M₂
⊢ (↑(comap f p) : Set M) = (⇑f : (a : M) → M₂) ⁻¹' (↑p : Set M₂)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
Goal:
A : Type u_9
A₂ : Type u_10
inst : AddCommGroup A
inst_1 : AddCommGroup A₂
f : A →+ A₂
s : AddSubgroup A₂
⊢ comap f.toIntLinearMap ((AddSubgroup.toIntSubmodule : (a : AddSubgroup A₂) → Submodule ℤ A₂) s) =
    (AddSubgroup.toIntSubmodule : (a : AddSubgroup A) → Submodule ℤ A) (AddSubgroup.comap f s)

Tactic:
rfl

Premises used: Submodule.comap, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
x : M
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R₂ M₂
⊢ x ∈ comap f p ↔ Membership.mem (α := M₂) p ((f : (a : M) → M₂) x : M₂)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
⊢ comap LinearMap.id p = p

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
p : Submodule R₃ M₃
⊢ comap (g ∘ₛₗ f) p = comap f (comap g p)

Tactic:
rfl

Premises used: Set.Mem, setOf, Submodule.comap, Set.preimage, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
q q' : Submodule R₂ M₂
⊢ q ≤ q' → comap f q ≤ comap f q'

Tactic:
preimage_mono

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage_mono, Set.preimage
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
f : M →ₗ[R] M
h : p ≤ comap f p
⊢ p ≤ comap (HPow.hPow (β := ℕ) f 0) p

Tactic:
simp [Module.End.one_eq_id]

Premises used: Module.End.one_eq_id
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : p ≤ comap (f ^ k) p
⊢ p ≤ comap (f ^ (k + 1)) p

Tactic:
simp [Module.End.iterate_succ, comap_comp, h.trans (comap_mono ih)]

Premises used: Submodule.comap_mono, Submodule.comap_comp, LE.le.trans, Module.End.iterate_succ
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
zero : p ≤ comap (HPow.hPow (β := ℕ) f 0) p
succ : ∀ (k : ℕ) (ih : p ≤ comap (f ^ k) p), p ≤ comap (f ^ (k + 1)) p
⊢ p ≤ comap (f ^ k) p

Tactic:
induction k with
  | zero => simp [Module.End.one_eq_id]
  | succ k ih => simp [Module.End.iterate_succ, comap_comp, h.trans (comap_mono ih)]

Premises used: Module.End.one_eq_id, Submodule.comap_comp, Submodule.zero, Module.End.iterate_succ
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
⊢ map f p ≤ q ↔ p ≤ comap f q

Tactic:
image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
⊢ map f ⊥ = ⊥

Tactic:
(gc_map_comap f).l_bot

Premises used: Submodule.gc_map_comap, GaloisConnection.l_bot
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
p p' : Submodule R M
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
⊢ map f (p ⊔ p') = map f p ⊔ map f p'

Tactic:
(gc_map_comap f : GaloisConnection (map f) (comap f)).l_sup

Premises used: Submodule.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
ι : Sort u_9
f : M →ₛₗ[σ₁₂] M₂
p : ι → Submodule R M
⊢ map f (⨆ (i : ι), p i) = ⨆ (i : ι), map f (p i)

Tactic:
(gc_map_comap f : GaloisConnection (map f) (comap f)).l_iSup

Premises used: GaloisConnection.l_iSup, Submodule.gc_map_comap
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
hpq : Disjoint p q
rw : map f p ⊓ map f q = ⊥
rw₁ : map f (p ⊓ q) = ⊥
rw₂ : map f ⊥ = ⊥
rw₃ rw₄ : Eq.{u_7 + 1} (α := Submodule R₂ M₂) ⊥ ⊥
⊢ Disjoint (map f p) (map f q)

Tactic:
rw [disjoint_iff, ← map_inf f hf, disjoint_iff.mp hpq, map_bot]

Premises used: Submodule.map_bot, disjoint_iff, Submodule.map_inf, Iff.mp
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
⊢ comap f ⊤ = ⊤

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Submodule.comap, Set.preimage, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
q q' : Submodule R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
⊢ comap f (q ⊓ q') = comap f q ⊓ comap f q'

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, Submodule.comap, Set.preimage, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
ι : Sort u_9
f : M →ₛₗ[σ₁₂] M₂
p : ι → Submodule R₂ M₂
⊢ comap f (⨅ (i : ι), p i) = ⨅ (i : ι), comap f (p i)

Tactic:
(gc_map_comap f).u_iInf

Premises used: GaloisConnection.u_iInf, Submodule.gc_map_comap
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
ι : Type u_9
f : M →ₛₗ[σ₁₂] M₂
s : Finset ι
p : ι → Submodule R₂ M₂
⊢ comap f (s.inf p) = s.inf fun (i : ι) ↦ comap f (p i)

Tactic:
simp [Finset.inf_eq_iInf]

Premises used: Finset.inf_eq_iInf
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
q : Submodule R₂ M₂
⊢ ∀ (x : M), Membership.mem (γ := Submodule R M) (comap (σ₁₂ := σ₁₂) 0 q) x ↔ Membership.mem (γ := Submodule R M) ⊤ x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
q : Submodule R₂ M₂
⊢ map f (comap f q) ≤ q

Tactic:
(gc_map_comap f).l_u_le _

Premises used: Submodule.gc_map_comap, GaloisConnection.l_u_le
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
⊢ p ≤ comap f (map f p)

Tactic:
(gc_map_comap f).le_u_l _

Premises used: GaloisConnection.le_u_l, Submodule.gc_map_comap
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
x_1 : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
inst_12 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
S : Submodule R₂ M₂
x : M₂
hx : x ∈ S
rcases :
  ∀ (y : M) (hx : Membership.mem (α := M₂) S ((f : (a : M) → M₂) y : M₂)),
    Membership.mem (α := M₂) (map f (comap f S)) ((f : (a : M) → M₂) y : M₂)
⊢ x ∈ map f (comap f S)

Tactic:
rcases hf x with ⟨y, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
inst_12 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
S : Submodule R₂ M₂
y : M
hx : Membership.mem (α := M₂) S ((f : (a : M) → M₂) y : M₂)
simp :
  ∃ (y_1 : M),
    Membership.mem (α := M₂) S ((f : (a : M) → M₂) y_1 : M₂) ∧
      Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) y_1 : M₂) ((f : (a : M) → M₂) y : M₂)
⊢ Membership.mem (α := M₂) (map f (comap f S)) ((f : (a : M) → M₂) y : M₂)

Tactic:
simp only [mem_map, mem_comap]

Premises used: Submodule.mem_map, Submodule.mem_comap
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
inst_12 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
S : Submodule R₂ M₂
y : M
hx : Membership.mem (α := M₂) S ((f : (a : M) → M₂) y : M₂)
⊢ ∃ (y_1 : M),
    Membership.mem (α := M₂) S ((f : (a : M) → M₂) y_1 : M₂) ∧
      Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) y_1 : M₂) ((f : (a : M) → M₂) y : M₂)

Tactic:
⟨y, hx, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Map
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
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
inst_12 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
S : Submodule R₂ M₂
y : M
hx : Membership.mem (α := M₂) S ((f : (a : M) → M₂) y : M₂)
⊢ ∃ (y_1 : M),
    Membership.mem (α := M₂) S ((f : (a : M) → M₂) y_1 : M₂) ∧
      Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) y_1 : M₂) ((f : (a : M) → M₂) y : M₂)

Tactic:
exact ⟨y, hx, rfl⟩
-- Module: Mathlib.Algebra.Module.Submodule.Map
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₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R₂ M₂
⊢ map f (comap f p) = p

Tactic:
(giMapComap hf).l_u_eq _

Premises used: GaloisInsertion.l_u_eq, Submodule.giMapComap