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₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ Surjective (map f)

Tactic:
(giMapComap hf).l_surjective

Premises used: GaloisInsertion.l_surjective, Submodule.giMapComap
-- 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₂)
⊢ Injective (comap f)

Tactic:
(giMapComap hf).u_injective

Premises used: GaloisInsertion.u_injective, Submodule.giMapComap
-- 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 q : Submodule R₂ M₂
⊢ map f (comap f p ⊔ comap f q) = p ⊔ q

Tactic:
(giMapComap hf).l_sup_u _ _

Premises used: GaloisInsertion.l_sup_u, Submodule.giMapComap
-- 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₂)
ι : Sort u_9
S : ι → Submodule R₂ M₂
⊢ map f (⨆ (i : ι), comap f (S i)) = iSup S

Tactic:
(giMapComap hf).l_iSup_u _

Premises used: GaloisInsertion.l_iSup_u, Submodule.giMapComap
-- 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 q : Submodule R₂ M₂
⊢ map f (comap f p ⊓ comap f q) = p ⊓ q

Tactic:
(giMapComap hf).l_inf_u _ _

Premises used: GaloisInsertion.l_inf_u, Submodule.giMapComap
-- 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₂)
ι : Sort u_9
S : ι → Submodule R₂ M₂
⊢ map f (⨅ (i : ι), comap f (S i)) = iInf S

Tactic:
(giMapComap hf).l_iInf_u _

Premises used: GaloisInsertion.l_iInf_u, Submodule.giMapComap
-- 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 q : Submodule R₂ M₂
⊢ comap f p ≤ comap f q ↔ p ≤ q

Tactic:
(giMapComap hf).u_le_u_iff

Premises used: GaloisInsertion.u_le_u_iff, Submodule.giMapComap
-- 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 q : Submodule R₂ M₂
H : comap f q ≤ comap f p ↔ q ≤ p
H' : comap f p ≤ comap f q ↔ p ≤ q
⊢ comap f p < comap f q ↔ p < q

Tactic:
apply lt_iff_lt_of_le_iff_le'

Premises used: lt_iff_lt_of_le_iff_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₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R₂ M₂
⊢ comap f q ≤ comap f p ↔ q ≤ p

Tactic:
comap_le_comap_iff_of_surjective hf

Premises used: Submodule.comap_le_comap_iff_of_surjective
-- 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 q : Submodule R₂ M₂
⊢ comap f q ≤ comap f p ↔ q ≤ p

Tactic:
exact comap_le_comap_iff_of_surjective hf

Premises used: Submodule.comap_le_comap_iff_of_surjective
-- 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 q : Submodule R₂ M₂
⊢ comap f p ≤ comap f q ↔ p ≤ q

Tactic:
comap_le_comap_iff_of_surjective hf

Premises used: Submodule.comap_le_comap_iff_of_surjective
-- 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 q : Submodule R₂ M₂
⊢ comap f p ≤ comap f q ↔ p ≤ q

Tactic:
exact comap_le_comap_iff_of_surjective hf

Premises used: Submodule.comap_le_comap_iff_of_surjective
-- 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₂)
⊢ StrictMono (comap f)

Tactic:
(giMapComap hf).strictMono_u

Premises used: GaloisInsertion.strictMono_u, Submodule.giMapComap
-- 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 : Submodule R M
q : Submodule R₂ M₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h : comap f q ≤ p
⊢ q ≤ map f p

Tactic:
map_comap_eq_of_surjective hf q ▸ map_mono h

Premises used: Eq.rec, Submodule.map_mono, Submodule.map_comap_eq_of_surjective
-- 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 : Submodule R M
q : Submodule R₂ M₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h : comap f q < p
⊢ comap f q ≤ p ∧ ¬p ≤ comap f q

Tactic:
rw [lt_iff_le_not_ge] at h ⊢

Premises used: lt_iff_le_not_ge
-- 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 : Submodule R M
q : Submodule R₂ M₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h : comap f q ≤ p ∧ ¬p ≤ comap f q
rw : q ≤ map f p ∧ ¬p ≤ comap f q
⊢ q ≤ map f p ∧ ¬map f p ≤ q

Tactic:
rw [map_le_iff_le_comap]

Premises used: Submodule.map_le_iff_le_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₂
p : Submodule R M
q : Submodule R₂ M₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h : comap f q ≤ p ∧ ¬p ≤ comap f q
⊢ q ≤ map f p ∧ ¬p ≤ comap f q

Tactic:
h.imp_left (le_map_of_comap_le_of_surjective hf)

Premises used: And.imp_left, Submodule.le_map_of_comap_le_of_surjective
-- 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 : Submodule R M
q : Submodule R₂ M₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h : comap f q ≤ p ∧ ¬p ≤ comap f q
⊢ q ≤ map f p ∧ ¬p ≤ comap f q

Tactic:
exact h.imp_left (le_map_of_comap_le_of_surjective hf)

Premises used: And.imp_left, Submodule.le_map_of_comap_le_of_surjective
-- 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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
S : Submodule R M
x : M
simp : ∀ x_2 ∈ S, Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x_2 : M₂) ((f : (a : M) → M₂) x : M₂) → x ∈ S
⊢ x ∈ comap f (map f S) → x ∈ S

Tactic:
simp only [mem_comap, mem_map, forall_exists_index, and_imp]

Premises used: Submodule.mem_map, and_imp, Submodule.mem_comap, forall_exists_index
-- 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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
S : Submodule R M
x y : M
hy : y ∈ S
hxy : Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) ((f : (a : M) → M₂) x : M₂)
⊢ y = x

Tactic:
rw [hf.eq_iff] at hxy

Premises used: Function.Injective.eq_iff
-- 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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
S : Submodule R M
x y : M
hy : y ∈ S
hxy : y = x
rwa rwa₁ rwa₂ rwa₃ : y ∈ S
⊢ x ∈ S

Tactic:
rwa [← hxy]
-- 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 : Submodule R M
⊢ comap f (map f p) = p

Tactic:
(gciMapComap hf).u_l_eq _

Premises used: Submodule.gciMapComap, GaloisCoinsertion.u_l_eq
-- 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₂)
⊢ Surjective (comap f)

Tactic:
(gciMapComap hf).u_surjective

Premises used: Submodule.gciMapComap, GaloisCoinsertion.u_surjective
-- 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₂)
⊢ Injective (map f)

Tactic:
(gciMapComap hf).l_injective

Premises used: GaloisCoinsertion.l_injective, Submodule.gciMapComap
-- 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
⊢ comap f (map f p ⊓ map f q) = p ⊓ q

Tactic:
(gciMapComap hf).u_inf_l _ _

Premises used: Submodule.gciMapComap, GaloisCoinsertion.u_inf_l
-- 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₂)
ι : Sort u_9
S : ι → Submodule R M
⊢ comap f (⨅ (i : ι), map f (S i)) = iInf S

Tactic:
(gciMapComap hf).u_iInf_l _

Premises used: GaloisCoinsertion.u_iInf_l, Submodule.gciMapComap
-- 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
⊢ comap f (map f p ⊔ map f q) = p ⊔ q

Tactic:
(gciMapComap hf).u_sup_l _ _

Premises used: Submodule.gciMapComap, GaloisCoinsertion.u_sup_l
-- 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₂)
ι : Sort u_9
S : ι → Submodule R M
⊢ comap f (⨆ (i : ι), map f (S i)) = iSup S

Tactic:
(gciMapComap hf).u_iSup_l _

Premises used: Submodule.gciMapComap, GaloisCoinsertion.u_iSup_l
-- 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
⊢ map f p ≤ map f q ↔ p ≤ q

Tactic:
(gciMapComap hf).l_le_l_iff

Premises used: GaloisCoinsertion.l_le_l_iff, Submodule.gciMapComap
-- 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₂)
⊢ StrictMono (map f)

Tactic:
(gciMapComap hf).strictMono_l

Premises used: Submodule.gciMapComap, GaloisCoinsertion.strictMono_l
-- 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
rw : map f p ≤ map f q ∧ map f p ≠ map f q ↔ p < q
rw₁ : map f p ≤ map f q ∧ map f p ≠ map f q ↔ p ≤ q ∧ p ≠ q
rw₂ : p ≤ q ∧ map f p ≠ map f q ↔ p ≤ q ∧ p ≠ q
rw₃ rw₄ : p ≤ q ∧ p ≠ q ↔ p ≤ q ∧ p ≠ q
⊢ map f p < map f q ↔ p < q

Tactic:
rw [lt_iff_le_and_ne, lt_iff_le_and_ne, map_le_map_iff_of_injective hf,
    (map_injective_of_injective hf).ne_iff]

Premises used: lt_iff_le_and_ne, Submodule.map_le_map_iff_of_injective, Function.Injective.ne_iff, Submodule.map_injective_of_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 σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
q : Submodule R₂ M₂
h : q < map f p
rw : map f (comap f q) < map f p
⊢ comap f q < p

Tactic:
rw [← map_lt_map_iff_of_injective hf]

Premises used: Submodule.map_lt_map_iff_of_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 σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
q : Submodule R₂ M₂
h : q < map f p
⊢ map f (comap f q) < map f p

Tactic:
(map_comap_le _ _).trans_lt h

Premises used: Submodule.map_comap_le, LE.le.trans_lt
-- 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 : Submodule R M
q : Submodule R₂ M₂
h : q < map f p
⊢ map f (comap f q) < map f p

Tactic:
exact (map_comap_le _ _).trans_lt h

Premises used: Submodule.map_comap_le, LE.le.trans_lt
-- 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
h : p ⋖ q
⊢ map f p ⋖ map f q

Tactic:
⟨lt_of_le_of_ne (map_mono h.1.le) ((map_injective_of_injective hf).ne h.1.ne), ?_⟩

Premises used: CovBy, Function.Injective.ne, LT.lt.le, And.left, And.intro, Submodule.map_mono, Submodule.map_injective_of_injective, lt_of_le_of_ne, LT.lt.ne
-- 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
h : p ⋖ q
refine : ∀ ⦃c : Submodule R₂ M₂⦄, map f p < c → ¬c < map f q
⊢ map f p ⋖ map f q

Tactic:
refine ⟨lt_of_le_of_ne (map_mono h.1.le) ((map_injective_of_injective hf).ne h.1.ne), ?_⟩
-- 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
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
⊢ False

Tactic:
h.2 ?_ (Submodule.comap_lt_of_lt_map_of_injective hf h₂)

Premises used: And.right, Submodule.comap_lt_of_lt_map_of_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 σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
refine : p < comap f P
⊢ False

Tactic:
refine h.2 ?_ (Submodule.comap_lt_of_lt_map_of_injective hf h₂)

Premises used: And.right, Submodule.comap_lt_of_lt_map_of_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 σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
rw : map f p < map f (comap f P)
⊢ p < comap f P

Tactic:
rw [← Submodule.map_lt_map_iff_of_injective hf]

Premises used: Submodule.map_lt_map_iff_of_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 σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
⊢ map f p < map f (comap f P)

Tactic:
h₁.trans_le ?_

Premises used: LT.lt.trans_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₂
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
refine : P ≤ map f (comap f P)
⊢ map f p < map f (comap f P)

Tactic:
refine h₁.trans_le ?_

Premises used: LT.lt.trans_le