awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
n : ℕ
zero : HPow.hPow (α := Ideal R) (β := ℕ) (comap f K) 0 ≤ comap f (HPow.hPow (β := ℕ) K 0)
⊢ HPow.hPow (α := Ideal R) (comap f K) n ≤ comap f (K ^ n)
have succ : ∀ (n : ℕ) (n_ih : HPow.hPow (α := Ideal R) (comap f K) n ≤ comap f (K ^ n)),
  HPow.hPow (α := Ideal R) (comap f K) (n + 1) ≤ comap f (K ^ (n + 1))
Tactic: induction n with
  | zero =>
    rw [pow_zero, pow_zero, Ideal.one_eq_top, Ideal.one_eq_top]
    exact rfl.le
  | succ n n_ih =>
    rw [pow_succ, pow_succ]
    exact (Ideal.mul_mono_left n_ih).trans (Ideal.le_comap_mul f)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
p : Ideal R
inst_2 : p.IsPrime
⊢ comap f (map f p) = p ↔ ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p
have refine_1 : ∀ (hp : comap f (map f p) = p), ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p
Tactic: refine ⟨fun hp ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
p : Ideal R
inst_2 : p.IsPrime
refine_1 : ∀ (hp : comap f (map f p) = p), ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p
⊢ comap f (map f p) = p ↔ ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p
have refine_2 : (∃ (q : Ideal S), q.IsPrime ∧ comap f q = p) → comap f (map f p) = p
Tactic: refine ⟨fun hp ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
p : Ideal R
inst_2 : p.IsPrime
hp : comap f (map f p) = p
⊢ ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p
have refine_1 : ∀ (q : Ideal S) (hq₁ : q.IsPrime) (hq₂ : map f p ≤ q)
  (hq₃ : Disjoint (↑q : Set S) (↑(Submonoid.map f p.primeCompl) : Set S)), ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p
Tactic: obtain ⟨q, hq₁, hq₂, hq₃⟩ := Ideal.exists_le_prime_disjoint _ _
      (disjoint_map_primeCompl_iff_comap_le.mpr hp.le)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rcf : RingHomClass F R S
f : F
r : R
⊢ Membership.mem (γ := Ideal R) (ker f) r ↔ Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
have rw : Membership.mem (γ := Ideal R) (Ideal.comap f ⊥) r ↔ Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
Tactic: rw [ker, Ideal.mem_comap, Submodule.mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rcf : RingHomClass F R S
f : F
r : R
rw : Membership.mem (γ := Ideal R) (Ideal.comap f ⊥) r ↔ Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
⊢ Membership.mem (γ := Ideal R) (ker f) r ↔ Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
have rw₁ : Membership.mem.{v, v} (α := S) (γ := Ideal S) ⊥ ((f : (a : R) → S) r : S) ↔
  Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
Tactic: rw [ker, Ideal.mem_comap, Submodule.mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rcf : RingHomClass F R S
f : F
r : R
rw : Membership.mem (γ := Ideal R) (Ideal.comap f ⊥) r ↔ Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
rw₁ :
  Membership.mem.{v, v} (α := S) (γ := Ideal S) ⊥ ((f : (a : R) → S) r : S) ↔
    Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
⊢ Membership.mem (γ := Ideal R) (ker f) r ↔ Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
have rw₂ : Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S) ↔ Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
Tactic: rw [ker, Ideal.mem_comap, Submodule.mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : S →+* R
g : T →+* S
⊢ Eq (α := Ideal T) (Ideal.comap g (ker f)) (ker (f.comp g))
have rw : Eq (α := Ideal T) (Ideal.comap g (Ideal.comap f ⊥)) (ker (f.comp g))
Tactic: rw [RingHom.ker_eq_comap_bot, Ideal.comap_comap, RingHom.ker_eq_comap_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : S →+* R
g : T →+* S
rw : Eq (α := Ideal T) (Ideal.comap g (Ideal.comap f ⊥)) (ker (f.comp g))
⊢ Eq (α := Ideal T) (Ideal.comap g (ker f)) (ker (f.comp g))
have rw₁ : Eq (α := Ideal T) (Ideal.comap (f.comp g) ⊥) (ker (f.comp g))
Tactic: rw [RingHom.ker_eq_comap_bot, Ideal.comap_comap, RingHom.ker_eq_comap_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : S →+* R
g : T →+* S
rw : Eq (α := Ideal T) (Ideal.comap g (Ideal.comap f ⊥)) (ker (f.comp g))
rw₁ : Eq (α := Ideal T) (Ideal.comap (f.comp g) ⊥) (ker (f.comp g))
⊢ Eq (α := Ideal T) (Ideal.comap g (ker f)) (ker (f.comp g))
have rw₂ : Eq (α := Ideal T) (Ideal.comap (f.comp g) ⊥) (Ideal.comap (f.comp g) ⊥)
Tactic: rw [RingHom.ker_eq_comap_bot, Ideal.comap_comap, RingHom.ker_eq_comap_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rcf : RingHomClass F R S
inst_3 : Nontrivial S
f : F
⊢ 1 ∉ ker f
have rw : ¬Eq.{v + 1} (α := S) 1 0
Tactic: rw [mem_ker, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
S : Type v
inst : Semiring S
ι : Type u_3
R : ι → Type u_4
inst_1 : (i : ι) → Semiring (R i)
φ : (i : ι) → RingHom.{v, u_4} S (R i)
⊢ Eq (α := Ideal S) (ker (Pi.ringHom (f := R) φ)) (⨅ (i : ι), ker (φ i))
have h : ∀ (x : S),
  Membership.mem (γ := Ideal S) (ker (Pi.ringHom (f := R) φ)) x ↔ Membership.mem (γ := Ideal S) (⨅ (i : ι), ker (φ i)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R ≃+* S
⊢ Eq (α := Ideal R) (ker (F := R →+* S) (↑f : R →+* S)) ⊥
have h : ∀ (x : R), Membership.mem (γ := Ideal R) (ker (F := R →+* S) (↑f : R →+* S)) x ↔ Membership.mem (γ := Ideal R) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
F' : Type u_3
inst_2 : EquivLike F' R S
inst_3 : RingEquivClass F' R S
f : F'
⊢ Eq (α := Ideal R) (ker f) ⊥
have h : ∀ (x : R), Membership.mem (γ := Ideal R) (ker f) x ↔ Membership.mem (γ := Ideal R) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
e : S ≃+* T
⊢ Eq (α := Ideal R) (ker (e.toRingHom.comp f)) (ker f)
have rw : Eq (α := Ideal R) (Ideal.comap f (ker e.toRingHom)) (ker f)
Tactic: rw [← RingHom.comap_ker, RingEquiv.toRingHom_eq_coe, RingHom.ker_coe_equiv, RingHom.ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
e : S ≃+* T
rw : Eq (α := Ideal R) (Ideal.comap f (ker e.toRingHom)) (ker f)
⊢ Eq (α := Ideal R) (ker (e.toRingHom.comp f)) (ker f)
have rw₁ : Eq (α := Ideal R) (Ideal.comap f (ker (F := S →+* T) (↑e : S →+* T))) (ker f)
Tactic: rw [← RingHom.comap_ker, RingEquiv.toRingHom_eq_coe, RingHom.ker_coe_equiv, RingHom.ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
e : S ≃+* T
rw : Eq (α := Ideal R) (Ideal.comap f (ker e.toRingHom)) (ker f)
rw₁ : Eq (α := Ideal R) (Ideal.comap f (ker (F := S →+* T) (↑e : S →+* T))) (ker f)
⊢ Eq (α := Ideal R) (ker (e.toRingHom.comp f)) (ker f)
have rw₂ : Eq (α := Ideal R) (Ideal.comap f ⊥) (ker f)
Tactic: rw [← RingHom.comap_ker, RingEquiv.toRingHom_eq_coe, RingHom.ker_coe_equiv, RingHom.ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
e : S ≃+* T
rw : Eq (α := Ideal R) (Ideal.comap f (ker e.toRingHom)) (ker f)
rw₁ : Eq (α := Ideal R) (Ideal.comap f (ker (F := S →+* T) (↑e : S →+* T))) (ker f)
rw₂ : Eq (α := Ideal R) (Ideal.comap f ⊥) (ker f)
⊢ Eq (α := Ideal R) (ker (e.toRingHom.comp f)) (ker f)
have rw₃ : Eq (α := Ideal R) (Ideal.comap f ⊥) (Ideal.comap f ⊥)
Tactic: rw [← RingHom.comap_ker, RingEquiv.toRingHom_eq_coe, RingHom.ker_coe_equiv, RingHom.ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S) ↔ Eq (α := Ideal R) (ker f) ⊥
have rw : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S) ↔
  ∀ (x : R), Membership.mem (γ := Set R) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) x ↔ x ∈ (↑⊥ : Set R)
Tactic: rw [SetLike.ext'_iff, ker_eq, Set.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ Eq (α := Ideal R) (ker f) ⊥ ↔ ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
have rw : Eq (α := Ideal R) (ker f) ⊥ ↔ Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
Tactic: rw [← injective_iff_map_eq_zero f, injective_iff_ker_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
rw : Eq (α := Ideal R) (ker f) ⊥ ↔ Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq (α := Ideal R) (ker f) ⊥ ↔ ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
have rw₁ : Eq (α := Ideal R) (ker f) ⊥ ↔ Eq (α := Ideal R) (ker f) ⊥
Tactic: rw [← injective_iff_map_eq_zero f, injective_iff_ker_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Ring R
inst_1 : Semiring S
inst_2 : Semiring T
g : T →+* R
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq (α := Ideal T) (ker (f.comp g)) (ker g)
have rw : Eq (α := Ideal T) (Ideal.comap g (ker f)) (ker g)
Tactic: rw [← RingHom.comap_ker, (injective_iff_ker_eq_bot f).mp hf, RingHom.ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Ring R
inst_1 : Semiring S
inst_2 : Semiring T
g : T →+* R
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
rw : Eq (α := Ideal T) (Ideal.comap g (ker f)) (ker g)
⊢ Eq (α := Ideal T) (ker (f.comp g)) (ker g)
have rw₁ : Eq (α := Ideal T) (Ideal.comap g ⊥) (ker g)
Tactic: rw [← RingHom.comap_ker, (injective_iff_ker_eq_bot f).mp hf, RingHom.ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Ring R
inst_1 : Semiring S
inst_2 : Semiring T
g : T →+* R
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
rw : Eq (α := Ideal T) (Ideal.comap g (ker f)) (ker g)
rw₁ : Eq (α := Ideal T) (Ideal.comap g ⊥) (ker g)
⊢ Eq (α := Ideal T) (ker (f.comp g)) (ker g)
have rw₂ : Eq (α := Ideal T) (Ideal.comap g ⊥) (Ideal.comap g ⊥)
Tactic: rw [← RingHom.comap_ker, (injective_iff_ker_eq_bot f).mp hf, RingHom.ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
x y : R
⊢ Membership.mem (γ := Ideal R) (ker f) (x - y) ↔
    Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
have rw : Eq.{v + 1} (α := S) ((f : (a : R) → S) (x - y) : S) (0 : S) ↔
  Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
Tactic: rw [mem_ker, map_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
x y : R
rw :
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (x - y) : S) (0 : S) ↔
    Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
⊢ Membership.mem (γ := Ideal R) (ker f) (x - y) ↔
    Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
have rw₁ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) = 0 ↔
  Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
Tactic: rw [mem_ker, map_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
x y : R
rw :
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (x - y) : S) (0 : S) ↔
    Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
rw₁ :
  HSub.hSub (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) = 0 ↔
    Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
⊢ Membership.mem (γ := Ideal R) (ker f) (x - y) ↔
    Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
have rw₂ : Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) ↔
  Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
Tactic: rw [mem_ker, map_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : Membership.mem (γ := Submodule R R) (Module.annihilator R M') x
⊢ Membership.mem (γ := Submodule R R) (Module.annihilator R M) x
have rw : ∀ (h : ∀ (m : M'), x • m = 0) (m : M), x • m = 0
Tactic: rw [Module.mem_annihilator] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : ∀ (m : M'), x • m = 0
m : M
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (x • m) : M') ((f : (a : M) → M') 0 : M')
have rw : HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M') = (f : (a : M) → M') 0
Tactic: rw [map_smul, h, f.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : ∀ (m : M'), x • m = 0
m : M
rw : HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M') = (f : (a : M) → M') 0
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (x • m) : M') ((f : (a : M) → M') 0 : M')
have rw₁ : Eq.{u_3 + 1} (α := M') (0 : M') ((f : (a : M) → M') 0 : M')
Tactic: rw [map_smul, h, f.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : ∀ (m : M'), x • m = 0
m : M
rw : HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M') = (f : (a : M) → M') 0
rw₁ : Eq.{u_3 + 1} (α := M') (0 : M') ((f : (a : M) → M') 0 : M')
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (x • m) : M') ((f : (a : M) → M') 0 : M')
have rw₂ : Eq.{u_3 + 1} (α := M') 0 0
Tactic: rw [map_smul, h, f.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : Membership.mem (γ := Submodule R R) (Module.annihilator R M) x
⊢ Membership.mem (γ := Submodule R R) (Module.annihilator R M') x
have rw : ∀ (h : ∀ (m : M), x • m = 0) (m : M'), x • m = 0
Tactic: rw [Module.mem_annihilator] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : ∀ (m : M), x • m = 0
m : M'
⊢ x • m = 0
have obtain : ∀ (m : M), HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M') = 0
Tactic: obtain ⟨m, rfl⟩ := hf m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : ∀ (m : M), x • m = 0
m : M
⊢ HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M') = 0
have rw : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (x • m) : M') (0 : M')
Tactic: rw [← map_smul, h, f.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : ∀ (m : M), x • m = 0
m : M
rw : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (x • m) : M') (0 : M')
⊢ HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M') = 0
have rw₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') 0 : M') (0 : M')
Tactic: rw [← map_smul, h, f.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : ∀ (m : M), x • m = 0
m : M
rw : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (x • m) : M') (0 : M')
rw₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') 0 : M') (0 : M')
⊢ HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M') = 0
have rw₂ : Eq.{u_3 + 1} (α := M') 0 0
Tactic: rw [← map_smul, h, f.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₀ : Type u_4
inst_3 : CommSemiring R₀
inst_4 : Module R₀ M
inst_5 : Algebra R₀ R
inst_6 : IsScalarTower R₀ R M
⊢ Eq (α := Ideal R₀) (Ideal.comap (F := R₀ →+* R) (algebraMap R₀ R) (annihilator R M)) (annihilator R₀ M)
have h : ∀ (x : R₀),
  Membership.mem (γ := Ideal R₀) (Ideal.comap (F := R₀ →+* R) (algebraMap R₀ R) (annihilator R M)) x ↔
    Membership.mem (γ := Ideal R₀) (annihilator R₀ M) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq (α := Ideal R) (annihilator R M) ⊥ ↔ FaithfulSMul R M
have rw : LE.le (α := Ideal R) (annihilator R M) ⊥ ↔ FaithfulSMul R M
Tactic: rw [← le_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ LE.le (α := Ideal R) (annihilator R M) ⊥ ↔ FaithfulSMul R M
have refine_1 : ∀ (H : LE.le (α := Ideal R) (annihilator R M) ⊥) {r s : R} (H' : ∀ (a : M), r • a = s • a), r = s
Tactic: refine ⟨fun H ↦ ⟨fun {r s} H' ↦ ?_⟩, fun ⟨H⟩ {a} ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
refine_1 : ∀ (H : LE.le (α := Ideal R) (annihilator R M) ⊥) {r s : R} (H' : ∀ (a : M), r • a = s • a), r = s
⊢ LE.le (α := Ideal R) (annihilator R M) ⊥ ↔ FaithfulSMul R M
have refine_2 : FaithfulSMul R M →
  ∀ {a : R} (ha : Membership.mem (γ := Submodule R R) (annihilator R M) a)
    (H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂), Membership.mem (γ := Submodule R R) ⊥ a
Tactic: refine ⟨fun H ↦ ⟨fun {r s} H' ↦ ?_⟩, fun ⟨H⟩ {a} ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_4
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : LE.le (α := Ideal R) (annihilator R M) ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ r = s
have refine_1 : r - s = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Eq (α := Ideal R) (annihilator R M) ⊤
m m' : M
⊢ m = m'
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m'
Tactic: rw [← one_smul R m, ← one_smul R m']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
⊢ Eq (α := Ideal R) (annihilator R (M × M')) (annihilator R M ⊓ annihilator R M')
have h : ∀ (x : R),
  Membership.mem (γ := Ideal R) (annihilator R (M × M')) x ↔
    Membership.mem (γ := Ideal R) (annihilator R M ⊓ annihilator R M') x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
x : R
⊢ Membership.mem (γ := Ideal R) (annihilator R (M × M')) x ↔
    Membership.mem (γ := Ideal R) (annihilator R M ⊓ annihilator R M') x
have h : Membership.mem (γ := Ideal R) (annihilator R (M × M')) x ↔
  Membership.mem (γ := Ideal R) (annihilator R M) x ∧ Membership.mem (γ := Ideal R) (annihilator R M') x
Tactic: simp_rw [Ideal.mem_inf, mem_annihilator,
    Prod.forall, Prod.smul_mk, Prod.mk_eq_zero, forall_and_left, ← forall_and_right]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
x : R
h :
  Membership.mem (γ := Ideal R) (annihilator R (M × M')) x ↔
    Membership.mem (γ := Ideal R) (annihilator R M) x ∧ Membership.mem (γ := Ideal R) (annihilator R M') x
⊢ Membership.mem (γ := Ideal R) (annihilator R (M × M')) x ↔
    Membership.mem (γ := Ideal R) (annihilator R M ⊓ annihilator R M') x
have h₁ : (∀ (m : M × M'), x • m = 0) ↔ (∀ (m : M), x • m = 0) ∧ ∀ (m : M'), x • m = 0
Tactic: simp_rw [Ideal.mem_inf, mem_annihilator,
    Prod.forall, Prod.smul_mk, Prod.mk_eq_zero, forall_and_left, ← forall_and_right]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
x : R
h :
  Membership.mem (γ := Ideal R) (annihilator R (M × M')) x ↔
    Membership.mem (γ := Ideal R) (annihilator R M) x ∧ Membership.mem (γ := Ideal R) (annihilator R M') x
h₁ : (∀ (m : M × M'), x • m = 0) ↔ (∀ (m : M), x • m = 0) ∧ ∀ (m : M'), x • m = 0
⊢ Membership.mem (γ := Ideal R) (annihilator R (M × M')) x ↔
    Membership.mem (γ := Ideal R) (annihilator R M ⊓ annihilator R M') x
have h₂ : (∀ (a : M) (b : M'), x • (a, b) = 0) ↔ (∀ (m : M), x • m = 0) ∧ ∀ (m : M'), x • m = 0
Tactic: simp_rw [Ideal.mem_inf, mem_annihilator,
    Prod.forall, Prod.smul_mk, Prod.mk_eq_zero, forall_and_left, ← forall_and_right]