awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
I : Ideal S
⊢ (↑(comap f I) : Set R) = (⇑f : (a : R) → S) ⁻¹' (↑I : Set S)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
I : Ideal S
⊢ Eq (α := Ideal R) (comap (F := R →+* S) (↑f : R →+* S) I) (comap f I)

Tactic:
rfl

Premises used: RingHomClass.toRingHom, Ideal.comap, rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
I : Ideal R
⊢ Eq.{v + 1} (α := Ideal S) (map (F := R →+* S) (↑f : R →+* S) I) (map f I)

Tactic:
rfl

Premises used: Ideal.map, RingHomClass.toRingHom, rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I J : Ideal R
h : I ≤ J
⊢ LE.le.{v} (α := Ideal S) (map f I) (map f J)

Tactic:
span_mono <| Set.image_mono h

Premises used: Set.Mem, Set.image_mono, Ideal.span_mono
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I : Ideal R
x : R
h : x ∈ I
⊢ Membership.mem.{v, v} (α := S) (γ := Ideal S) (map f I) ((f : (a : R) → S) x : S)

Tactic:
subset_span ⟨x, h, rfl⟩

Premises used: Ideal.subset_span, Set.Mem, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I : Ideal R
x : ↥I
⊢ Membership.mem.{v, v} (α := S) (γ := Ideal S) (map f I) ((f : (a : R) → S) (↑x : R) : S)

Tactic:
mem_map_of_mem f x.2

Premises used: Ideal.mem_map_of_mem, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I : Ideal R
K : Ideal S
inst_3 : RingHomClass F R S
⊢ map f I ≤ K ↔ I ≤ comap f K

Tactic:
span_le.trans Set.image_subset_iff

Premises used: Ideal.span_le, Set.Mem, Iff.trans, Set.image_subset_iff
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
K : Ideal S
inst_3 : RingHomClass F R S
x : R
⊢ Membership.mem (γ := Ideal R) (comap f K) x ↔ Membership.mem (α := S) K ((f : (a : R) → S) x : S)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
K L : Ideal S
inst_3 : RingHomClass F R S
h : K ≤ L
⊢ LE.le (α := Ideal R) (comap f K) (comap f L)

Tactic:
Set.preimage_mono fun _ hx => h hx

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage_mono, Set.preimage
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
K : Ideal S
inst_3 : RingHomClass F R S
hK : K ≠ ⊤
rw : 1 ∉ K
⊢ 1 ∉ comap f K

Tactic:
rw [mem_comap, map_one]

Premises used: map_one, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
K : Ideal S
inst_3 : RingHomClass F R S
hK : K ≠ ⊤
⊢ 1 ∉ K

Tactic:
(ne_top_iff_one _).1 hK

Premises used: Ideal.ne_top_iff_one, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
K : Ideal S
inst_3 : RingHomClass F R S
hK : K ≠ ⊤
⊢ 1 ∉ K

Tactic:
exact (ne_top_iff_one _).1 hK

Premises used: Ideal.ne_top_iff_one, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
F : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
P : Ideal R
inst_4 : P.IsPrime
I : Ideal S
le : comap f I ≤ P
r : R
hp : r ∈ (↑P.primeCompl : Set R)
hI : Membership.mem (α := S) (↑I : Set S) ((f : (a : R) → S) r : S)
⊢ False

Tactic:
hp (le hI)
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
F : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
P : Ideal R
inst_4 : P.IsPrime
I : Ideal S
le : comap f I ≤ P
r : R
hp : r ∈ (↑P.primeCompl : Set R)
hI : Membership.mem (α := S) (↑I : Set S) ((f : (a : R) → S) r : S)
⊢ False

Tactic:
exact hp (le hI)
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn.{u, v} (β := S) (⇑g : (a : S) → R) (⇑f : (a : R) → S) (↑I : Set R)
⊢ LE.le (α := Ideal S) (map f I) (comap g I)

Tactic:
Ideal.span_le.2 ?_

Premises used: Ideal.span_le, Iff.mpr, Set.Mem
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn.{u, v} (β := S) (⇑g : (a : S) → R) (⇑f : (a : R) → S) (↑I : Set R)
refine : (⇑f : (a : R) → S) '' (↑I : Set R) ⊆ (↑(comap g I) : Set S)
⊢ LE.le (α := Ideal S) (map f I) (comap g I)

Tactic:
refine Ideal.span_le.2 ?_

Premises used: Ideal.span_le, Iff.mpr
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn.{u, v} (β := S) (⇑g : (a : S) → R) (⇑f : (a : R) → S) (↑I : Set R)
x : R
hx : x ∈ (↑I : Set R)
rw : x ∈ I
⊢ Membership.mem (α := S) (↑(comap g I) : Set S) ((f : (a : R) → S) x : S)

Tactic:
rw [SetLike.mem_coe, mem_comap, hf hx]

Premises used: SetLike.mem_coe, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn.{u, v} (β := S) (⇑g : (a : S) → R) (⇑f : (a : R) → S) (↑I : Set R)
x : R
hx : x ∈ (↑I : Set R)
⊢ x ∈ I

Tactic:
hx
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn.{u, v} (β := S) (⇑g : (a : S) → R) (⇑f : (a : R) → S) (↑I : Set R)
x : R
hx : x ∈ (↑I : Set R)
⊢ x ∈ I

Tactic:
exact hx
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
g : G
I : Ideal S
hf : Set.LeftInvOn.{u, v} (α := R) (β := S) (⇑g : (a : S) → R) (⇑f : (a : R) → S) ((⇑f : (a : R) → S) ⁻¹' (↑I : Set S))
⊢ LE.le (α := Ideal R) (comap f I) (map g I)

Tactic:
fun x (hx : f x ∈ I) => hf hx ▸ Ideal.mem_map_of_mem g hx

Premises used: Ideal.mem_map_of_mem, Set.Mem, setOf, Eq.rec, Set.preimage
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass G S R
g : G
I : Ideal R
h : Function.LeftInverse.{u + 1, v + 1} (α := R) (β := S) (⇑g : (a : S) → R) (⇑f : (a : R) → S)
⊢ LE.le (α := Ideal S) (map f I) (comap g I)

Tactic:
map_le_comap_of_inv_on _ _ _ <| h.leftInvOn _

Premises used: Ideal.map_le_comap_of_inv_on, Function.LeftInverse.leftInvOn
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
h : Eq (α := Ideal R) (comap f I) ⊥
h₁ : ∀ (x : S), x ∈ I ↔ Membership.mem (γ := Ideal S) ⊥ x
⊢ I = ⊥

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
h : Eq (α := Ideal R) (comap f I) ⊥
x : S
h₁ : ∀ (y : R) (hy : (f : (a : R) → S) y = x), x ∈ I ↔ Membership.mem (γ := Ideal S) ⊥ x
⊢ x ∈ I ↔ Membership.mem (γ := Ideal S) ⊥ x

Tactic:
obtain ⟨y, hy⟩ := hf x
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
h : Eq (α := Ideal R) (comap f I) ⊥
x : S
y : R
hy : (f : (a : R) → S) y = x
⊢ x ∈ I ↔ Membership.mem (γ := Ideal S) ⊥ x

Tactic:
aesop (add norm [Submodule.eq_bot_iff])

Premises used: Submodule.eq_bot_iff
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
inst_5 : K.IsTwoSided
a b : R
ha : Membership.mem (γ := Ideal R) (comap f K) a
rw : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ∈ K
⊢ Membership.mem (γ := Ideal R) (comap f K) (a * b)

Tactic:
rw [mem_comap, map_mul]

Premises used: map_mul, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
inst_5 : K.IsTwoSided
a b : R
ha : Membership.mem (γ := Ideal R) (comap f K) a
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ∈ K

Tactic:
mul_mem_right _ _ ha

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
inst_5 : K.IsTwoSided
a b : R
ha : Membership.mem (γ := Ideal R) (comap f K) a
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ∈ K

Tactic:
exact mul_mem_right _ _ ha

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
g : G
I : Ideal S
h : Function.LeftInverse.{u + 1, v + 1} (α := R) (β := S) (⇑g : (a : S) → R) (⇑f : (a : R) → S)
⊢ LE.le (α := Ideal R) (comap f I) (map g I)

Tactic:
comap_le_map_of_inv_on _ _ _ <| h.leftInvOn _

Premises used: Function.LeftInverse.leftInvOn, Ideal.comap_le_map_of_inv_on
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
hK : K.IsPrime
x y : R
simp :
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) ∈ K →
    Membership.mem (α := S) K ((f : (a : R) → S) x : S) ∨ Membership.mem (α := S) K ((f : (a : R) → S) y : S)
⊢ Membership.mem (γ := Ideal R) (Ideal.comap f K) (x * y) →
    Membership.mem (γ := Ideal R) (Ideal.comap f K) x ∨ Membership.mem (γ := Ideal R) (Ideal.comap f K) y

Tactic:
simp only [mem_comap, map_mul]

Premises used: map_mul, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
hK : K.IsPrime
x y : R
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) ∈ K →
    Membership.mem (α := S) K ((f : (a : R) → S) x : S) ∨ Membership.mem (α := S) K ((f : (a : R) → S) y : S)

Tactic:
apply hK.2

Premises used: Ideal.IsPrime.mem_or_mem'
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
⊢ Eq.{v + 1} (α := Ideal S) (map.{u, v, u_1} (R := R) f ⊤) ⊤

Tactic:
(eq_top_iff_one _).2 <| subset_span ⟨1, trivial, map_one f⟩

Premises used: Iff.mpr, Ideal.subset_span, trivial, Ideal.eq_top_iff_one, map_one, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
⊢ GaloisConnection (α := Ideal R) (β := Ideal S) (map f) (comap f)

Tactic:
fun _ _ =>
  Ideal.map_le_iff_le_comap

Premises used: Ideal.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
inst : Semiring R
I : Ideal R
⊢ comap (F := R →+* R) (RingHom.id R) I = I

Tactic:
Ideal.ext fun _ => Iff.rfl

Premises used: Iff.rfl, Ideal.ext
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
I : Ideal S
⊢ comap (F := S →ₐ[R] S) (AlgHom.id R S) I = I

Tactic:
I.comap_id

Premises used: AlgHom.id, Ideal.comap, Ideal.comap_id
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
inst : Semiring R
I : Ideal R
⊢ map (F := R →+* R) (RingHom.id R) I = I

Tactic:
(gc_map_comap (RingHom.id R)).l_unique GaloisConnection.id comap_id

Premises used: GaloisConnection.l_unique, GaloisConnection.id, RingHom.id, Ideal.comap_id, Ideal.gc_map_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
I : Ideal S
⊢ map (F := S →ₐ[R] S) (AlgHom.id R S) I = I

Tactic:
I.map_id

Premises used: Ideal.map_id, AlgHom.id, Ideal.map
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
T : Type u_3
inst_2 : Semiring T
I : Ideal T
f : R →+* S
g : S →+* T
⊢ Eq (α := Ideal R) (comap f (comap g I)) (comap (g.comp f) I)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Ideal.comap, rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
I : Ideal C
f : A →ₐ[R] B
g : B →ₐ[R] C
⊢ Eq (α := Ideal A) (comap f (comap g I)) (comap (g.comp f) I)

Tactic:
I.comap_comap f.toRingHom g.toRingHom

Premises used: AlgHom.toRingHom, Ideal.comap, AlgHom.comp, Ideal.comap_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
T : Type u_3
inst_2 : Semiring T
I : Ideal R
f : R →+* S
g : S →+* T
⊢ Eq.{u_3 + 1} (α := Ideal T) (map (R := S) g (map f I)) (map (g.comp f) I)

Tactic:
((gc_map_comap f).compose (gc_map_comap g)).l_unique (gc_map_comap (g.comp f)) fun _ =>
    comap_comap _ _

Premises used: GaloisConnection.l_unique, Ideal.map, RingHom.comp, Submodule.span, GaloisConnection.compose, Ideal.gc_map_comap, Ideal.comap_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
I : Ideal A
f : A →ₐ[R] B
g : B →ₐ[R] C
⊢ Eq.{u_6 + 1} (α := Ideal C) (map (R := B) g (map f I)) (map (g.comp f) I)

Tactic:
I.map_map f.toRingHom g.toRingHom

Premises used: Set.Mem, setOf, Ideal.map, AlgHom.toRingHom, Ideal.map_map, AlgHom.comp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
s : Set R
⊢ Eq.{v + 1} (α := Ideal S) (map f (span s)) (span ((⇑f : (a : R) → S) '' s))

Tactic:
(Submodule.span_eq_of_le _ ?_ ?_).symm

Premises used: Submodule.span_eq_of_le, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
s : Set R
refine_1 : (⇑f : (a : R) → S) '' s ⊆ (↑(map f (span s)) : Set S)
refine_2 : LE.le (α := Submodule S S) (map f (span s)) (Submodule.span S ((⇑f : (a : R) → S) '' s))
⊢ Eq.{v + 1} (α := Ideal S) (map f (span s)) (span ((⇑f : (a : R) → S) '' s))

Tactic:
refine (Submodule.span_eq_of_le _ ?_ ?_).symm

Premises used: Submodule.span_eq_of_le, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
s : Set R
x : R
hx : x ∈ s
⊢ Membership.mem (α := S) (↑(map f (span s)) : Set S) ((f : (a : R) → S) x : S)

Tactic:
mem_map_of_mem f (subset_span hx)

Premises used: Ideal.subset_span, Ideal.mem_map_of_mem, Set.Mem
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
s : Set R
x : R
hx : x ∈ s
⊢ Membership.mem (α := S) (↑(map f (span s)) : Set S) ((f : (a : R) → S) x : S)

Tactic:
exact mem_map_of_mem f (subset_span hx)

Premises used: Ideal.subset_span, Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
s : Set R
refine_2 : (⇑f : (a : R) → S) '' s ⊆ (↑(Submodule.span S ((⇑f : (a : R) → S) '' s)) : Set S)
⊢ LE.le (α := Submodule S S) (map f (span s)) (Submodule.span S ((⇑f : (a : R) → S) '' s))

Tactic:
rw [map_le_iff_le_comap, span_le, coe_comap, ← Set.image_subset_iff]

Premises used: Ideal.span_le, Ideal.map_le_iff_le_comap, Ideal.coe_comap, Set.image_subset_iff
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
s : Set R
⊢ (⇑f : (a : R) → S) '' s ⊆ (↑(Submodule.span S ((⇑f : (a : R) → S) '' s)) : Set S)

Tactic:
subset_span

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
s : Set R
⊢ (⇑f : (a : R) → S) '' s ⊆ (↑(Submodule.span S ((⇑f : (a : R) → S) '' s)) : Set S)

Tactic:
exact subset_span

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I : Ideal R
K : Ideal S
inst_3 : RingHomClass F R S
⊢ I ≤ comap f K → map f I ≤ K

Tactic:
(gc_map_comap f).l_le

Premises used: GaloisConnection.l_le, Ideal.gc_map_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I : Ideal R
K : Ideal S
inst_3 : RingHomClass F R S
⊢ map f I ≤ K → I ≤ comap f K

Tactic:
(gc_map_comap f).le_u

Premises used: GaloisConnection.le_u, Ideal.gc_map_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I : Ideal R
inst_3 : RingHomClass F R S
⊢ I ≤ comap f (map f I)

Tactic:
(gc_map_comap f).le_u_l _

Premises used: GaloisConnection.le_u_l, Ideal.gc_map_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
K : Ideal S
inst_3 : RingHomClass F R S
⊢ map f (comap f K) ≤ K

Tactic:
(gc_map_comap f).l_u_le _

Premises used: GaloisConnection.l_u_le, Ideal.gc_map_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
⊢ Eq (α := Ideal R) (comap f ⊤) ⊤

Tactic:
(gc_map_comap f).u_top

Premises used: GaloisConnection.u_top, Ideal.gc_map_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
I : Ideal S
h : I = ⊤
rw : Eq (α := Ideal R) (comap f ⊤) ⊤
rw₁ rw₂ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
⊢ Eq (α := Ideal R) (comap f I) ⊤

Tactic:
rw [h, comap_top]

Premises used: Ideal.comap_top
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
⊢ Eq.{v + 1} (α := Ideal S) (map.{u, v, u_1} (R := R) f ⊥) ⊥

Tactic:
(gc_map_comap f).l_bot

Premises used: GaloisConnection.l_bot, Ideal.gc_map_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I : Ideal R
inst_3 : RingHomClass F R S
hI : Ne.{v + 1} (α := Ideal S) (map f I) ⊥
⊢ I ≠ ⊥

Tactic:
fun h => hI (Eq.mpr (congrArg (fun I ↦ map f I = ⊥) h) map_bot)

Premises used: Eq.mpr, congrArg, Ideal.map, Bot.bot, Ideal.map_bot, Eq, Not
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I : Ideal R
inst_3 : RingHomClass F R S
⊢ Eq.{v + 1} (α := Ideal S) (map f (comap f (map f I))) (map f I)

Tactic:
(gc_map_comap f).l_u_l_eq_l I

Premises used: GaloisConnection.l_u_l_eq_l, Ideal.gc_map_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
K : Ideal S
inst_3 : RingHomClass F R S
⊢ Eq (α := Ideal R) (comap f (map f (comap f K))) (comap f K)

Tactic:
(gc_map_comap f).u_l_u_eq_u K

Premises used: GaloisConnection.u_l_u_eq_u, Ideal.gc_map_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I J : Ideal R
inst_3 : RingHomClass F R S
⊢ Eq.{v + 1} (α := Ideal S) (map f (I ⊔ J)) (map f I ⊔ map f J)

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

Premises used: GaloisConnection.l_sup, Ideal.gc_map_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
K L : Ideal S
inst_3 : RingHomClass F R S
⊢ Eq (α := Ideal R) (comap f (K ⊓ L)) (comap f K ⊓ comap f L)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, Set.preimage, Ideal.comap, rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
ι : Sort u_3
K : ι → Ideal R
⊢ Eq.{v + 1} (α := Ideal S) (map f (iSup K)) (⨆ (i : ι), map f (K i))

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

Premises used: GaloisConnection.l_iSup, Ideal.gc_map_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
ι : Sort u_3
K : ι → Ideal S
⊢ Eq (α := Ideal R) (comap f (iInf K)) (⨅ (i : ι), comap f (K i))

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

Premises used: GaloisConnection.u_iInf, Ideal.gc_map_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
ι : Type u_4
s : Finset ι
K : ι → Ideal S
⊢ Eq (α := Ideal R) (comap f (s.inf K)) (s.inf fun (i : ι) ↦ comap f (K i))

Tactic:
simp [Finset.inf_eq_iInf, comap_iInf]

Premises used: Ideal.comap_iInf, Finset.inf_eq_iInf