awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst_2 : Algebra R S
x : R
rw :
  Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
          (a : R) → S ⧸ map (algebraMap R S) p)
        x :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    ((algebraMap (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
          (a : R ⧸ p) → S ⧸ map (algebraMap R S) p)
        ((mk p : (a : R) → R ⧸ p) x) :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
rw₁ :
  Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
          (a : R) → S ⧸ map (algebraMap R S) p)
        x :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    ((mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p)
        ((algebraMap R S : (a : R) → S) x) :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
⊢ Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
          (a : R) → S ⧸ map (algebraMap R S) p)
        x :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    ((algebraMap (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
          (a : R ⧸ p) → S ⧸ map (algebraMap R S) p)
        ((algebraMap R (R ⧸ p) : (a : R) → R ⧸ p) x) :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
have rw₂ : Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
  ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
        (a : R) → S ⧸ map (algebraMap R S) p)
      x :
    HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
  ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :
        (a : R) → S ⧸ map (algebraMap R S) p)
      x :
    HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
Tactic: rw [Quotient.algebraMap_eq, Quotient.algebraMap_quotient_map_quotient,
      Quotient.mk_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : Semiring B
inst_2 : Algebra A B
P : Ideal B
G : Type u_5
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
g : G
⊢ Eq (α := Ideal A) (under A (g • P)) (under A P)
have h : ∀ (a : A), Membership.mem (γ := Ideal A) (under A (g • P)) a ↔ Membership.mem (γ := Ideal A) (under A P) a
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : Semiring B
inst_2 : Algebra A B
P : Ideal B
G : Type u_5
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
g : G
a : A
⊢ Membership.mem (γ := Ideal A) (under A (g • P)) a ↔ Membership.mem (γ := Ideal A) (under A P) a
have h : Membership.mem (α := B) (g • P) ((algebraMap A B : (a : A) → B) a : B) ↔ Membership.mem (γ := Ideal A) (under A P) a
Tactic: rw [mem_comap, mem_comap, mem_pointwise_smul_iff_inv_smul_mem, smul_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : Semiring B
inst_2 : Algebra A B
P : Ideal B
G : Type u_5
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
g : G
a : A
h : Membership.mem (α := B) (g • P) ((algebraMap A B : (a : A) → B) a : B) ↔ Membership.mem (γ := Ideal A) (under A P) a
⊢ Membership.mem (γ := Ideal A) (under A (g • P)) a ↔ Membership.mem (γ := Ideal A) (under A P) a
have h₁ : Membership.mem (α := B) (g • P) ((algebraMap A B : (a : A) → B) a : B) ↔
  Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) a : B)
Tactic: rw [mem_comap, mem_comap, mem_pointwise_smul_iff_inv_smul_mem, smul_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : Semiring B
inst_2 : Algebra A B
P : Ideal B
G : Type u_5
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
g : G
a : A
h : Membership.mem (α := B) (g • P) ((algebraMap A B : (a : A) → B) a : B) ↔ Membership.mem (γ := Ideal A) (under A P) a
h₁ :
  Membership.mem (α := B) (g • P) ((algebraMap A B : (a : A) → B) a : B) ↔
    Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) a : B)
⊢ Membership.mem (γ := Ideal A) (under A (g • P)) a ↔ Membership.mem (γ := Ideal A) (under A P) a
have h₂ : HSMul.hSMul (β := B) g⁻¹ ((algebraMap A B : (a : A) → B) a : B) ∈ P ↔
  Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) a : B)
Tactic: rw [mem_comap, mem_comap, mem_pointwise_smul_iff_inv_smul_mem, smul_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : Semiring B
inst_2 : Algebra A B
P : Ideal B
G : Type u_5
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
g : G
a : A
h : Membership.mem (α := B) (g • P) ((algebraMap A B : (a : A) → B) a : B) ↔ Membership.mem (γ := Ideal A) (under A P) a
h₁ :
  Membership.mem (α := B) (g • P) ((algebraMap A B : (a : A) → B) a : B) ↔
    Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) a : B)
h₂ :
  HSMul.hSMul (β := B) g⁻¹ ((algebraMap A B : (a : A) → B) a : B) ∈ P ↔
    Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) a : B)
⊢ Membership.mem (γ := Ideal A) (under A (g • P)) a ↔ Membership.mem (γ := Ideal A) (under A P) a
have h₃ : Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) a : B) ↔
  Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) a : B)
Tactic: rw [mem_comap, mem_comap, mem_pointwise_smul_iff_inv_smul_mem, smul_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : Semiring B
inst_2 : Algebra A B
P : Ideal B
p : Ideal A
inst_3 : P.LiesOver p
x : A
⊢ x ∈ p ↔ Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) x : B)
have rw : Membership.mem (γ := Ideal A) (under A P) x ↔ Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) x : B)
Tactic: rw [P.over_def p]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : Semiring B
inst_2 : Algebra A B
P : Ideal B
p : Ideal A
inst_3 : P.LiesOver p
⊢ P = ⊤ ↔ p = ⊤
have rw : P = ⊤ ↔ Eq (α := Ideal A) (under A P) ⊤
Tactic: rw [P.over_def p]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : Semiring B
inst_2 : Algebra A B
P : Ideal B
p : Ideal A
inst_3 : P.LiesOver p
inst_4 : P.IsPrime
⊢ p.IsPrime
have rw : IsPrime (under A P)
Tactic: rw [over_def P p]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
C : Type u_4
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
inst_5 : Q.LiesOver p
F : Type u_6
inst_6 : FunLike F B C
inst_7 : AlgHomClass F A B C
f : F
h : P = comap f Q
⊢ p = under A P
have rw : p = under A (comap f Q)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (hypothesis)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
C : Type u_4
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
inst_5 : P.LiesOver p
E : Type u_6
inst_6 : EquivLike E B C
inst_7 : AlgEquivClass E A B C
σ : E
h : Q = map σ P
⊢ Q.LiesOver p
have h₁ : Q = comap (F := C ≃+* B) (RingEquiv.symm (↑σ : B ≃+* C)) P
Tactic: rw [← show _ = P.map σ from comap_symm (RingEquivClass.toRingEquiv σ)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : CommSemiring B
C : Type u_4
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
𝔓 : Ideal C
⊢ Eq (α := Ideal A) (under A (under B 𝔓)) (under A 𝔓)
have simp_rw : Eq (α := Ideal A)
  (comap (F := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap A B)) 𝔓)
  (under A 𝔓)
Tactic: simp_rw [comap_comap, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : CommSemiring B
C : Type u_4
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
𝔓 : Ideal C
P : Ideal B
p : Ideal A
inst_7 : 𝔓.LiesOver P
inst_8 : P.LiesOver p
⊢ p = under A 𝔓
have rw : Eq (α := Ideal A) (under A P) (under A 𝔓)
Tactic: rw [P.over_def p, 𝔓.over_def P, under_under]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : CommSemiring B
C : Type u_4
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
𝔓 : Ideal C
P : Ideal B
p : Ideal A
inst_7 : 𝔓.LiesOver P
inst_8 : P.LiesOver p
rw : Eq (α := Ideal A) (under A P) (under A 𝔓)
⊢ p = under A 𝔓
have rw₁ : Eq (α := Ideal A) (under A (under B 𝔓)) (under A 𝔓)
Tactic: rw [P.over_def p, 𝔓.over_def P, under_under]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : CommSemiring B
C : Type u_4
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
𝔓 : Ideal C
P : Ideal B
p : Ideal A
inst_7 : 𝔓.LiesOver P
inst_8 : P.LiesOver p
rw : Eq (α := Ideal A) (under A P) (under A 𝔓)
rw₁ : Eq (α := Ideal A) (under A (under B 𝔓)) (under A 𝔓)
⊢ p = under A 𝔓
have rw₂ : Eq (α := Ideal A) (under A 𝔓) (under A 𝔓)
Tactic: rw [P.over_def p, 𝔓.over_def P, under_under]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : CommSemiring B
inst_2 : Algebra A B
P : Ideal B
C : Type u_5
D : Type u_6
inst_3 : CommSemiring C
inst_4 : Semiring D
inst_5 : Algebra A C
inst_6 : Algebra C D
inst_7 : Algebra A D
inst_8 : Algebra B D
inst_9 : IsScalarTower A C D
inst_10 : IsScalarTower A B D
⊢ LE.le (α := Ideal C) (map (F := A →+* C) (algebraMap A C) (under A P))
    (under.{u_5, u_6} C (B := D) (map (F := B →+* D) (algebraMap B D) P))
have a : LE.le.{u_6} (α := Ideal D)
  (map (R := C) (F := C →+* D) (algebraMap C D) (map (F := A →+* C) (algebraMap A C) (under A P)))
  (map (F := B →+* D) (algebraMap B D) P)
Tactic: apply le_comap_of_map_le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : CommSemiring B
inst_2 : Algebra A B
P : Ideal B
C : Type u_5
D : Type u_6
inst_3 : CommSemiring C
inst_4 : Semiring D
inst_5 : Algebra A C
inst_6 : Algebra C D
inst_7 : Algebra A D
inst_8 : Algebra B D
inst_9 : IsScalarTower A C D
inst_10 : IsScalarTower A B D
⊢ LE.le.{u_6} (α := Ideal D)
    (map (R := C) (F := C →+* D) (algebraMap C D) (map (F := A →+* C) (algebraMap A C) (under A P)))
    (map (F := B →+* D) (algebraMap B D) P)
have a : LE.le (α := Ideal A) (under A P)
  (comap (F := A →+* B) (algebraMap A B)
    (comap (F := B →+* D) (algebraMap B D) (map (F := B →+* D) (algebraMap B D) P)))
Tactic: rw [map_map, ← IsScalarTower.algebraMap_eq, map_le_iff_le_comap,
    IsScalarTower.algebraMap_eq A B D, ← comap_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (hypothesis)
Goal:
A : Type u_2
inst : CommSemiring A
C : Type u_4
inst_1 : Semiring C
inst_2 : Algebra A C
𝔓 : Ideal C
p : Ideal A
inst_3 : p.IsPrime
hPp : 𝔓.LiesOver p
⊢ Disjoint (↑(Algebra.algebraMapSubmonoid C p.primeCompl) : Set C) (↑𝔓 : Set C)
have hPp₁ : (↑p : Set A) = (⇑(algebraMap A C) : (a : A) → C) ⁻¹' (↑𝔓 : Set C)
Tactic: rw [liesOver_iff, under_def, SetLike.ext'_iff, coe_comap] at hPp
Cleared hypotheses: hPp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
B : Type u_3
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Ring B
inst_3 : Nontrivial B
inst_4 : Algebra A B
inst_5 : Module.IsTorsionFree A B
p : Ideal A
hp : p ≠ ⊥
P : Ideal B
inst_6 : P.LiesOver p
⊢ P ≠ ⊥
have contrapose : ∀ (hp : P = ⊥), p = ⊥
Tactic: contrapose hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
B : Type u_3
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Ring B
inst_3 : Nontrivial B
inst_4 : Algebra A B
inst_5 : Module.IsTorsionFree A B
p : Ideal A
P : Ideal B
inst_6 : P.LiesOver p
hp : P = ⊥
⊢ p = ⊥
have rw : Eq (α := Ideal A) (under A P) ⊥
Tactic: rw [over_def P p, hp, under_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
B : Type u_3
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Ring B
inst_3 : Nontrivial B
inst_4 : Algebra A B
inst_5 : Module.IsTorsionFree A B
p : Ideal A
P : Ideal B
inst_6 : P.LiesOver p
hp : P = ⊥
rw : Eq (α := Ideal A) (under A P) ⊥
⊢ p = ⊥
have rw₁ : Eq (α := Ideal A) (under.{u_2, u_3} A (B := B) ⊥) ⊥
Tactic: rw [over_def P p, hp, under_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_2
B : Type u_3
inst : CommRing A
inst_1 : IsDomain A
inst_2 : Ring B
inst_3 : Nontrivial B
inst_4 : Algebra A B
inst_5 : Module.IsTorsionFree A B
p : Ideal A
P : Ideal B
inst_6 : P.LiesOver p
hp : P = ⊥
rw : Eq (α := Ideal A) (under A P) ⊥
rw₁ : Eq (α := Ideal A) (under.{u_2, u_3} A (B := B) ⊥) ⊥
⊢ p = ⊥
have rw₂ : Eq.{u_2 + 1} (α := Ideal A) ⊥ ⊥
Tactic: rw [over_def P p, hp, under_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : CommRing C
inst_5 : Algebra A B
inst_6 : Algebra A C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst_10 : Q.LiesOver p
inst_11 : P.LiesOver p
G : Type u_6
inst_12 : Group G
inst_13 : MulSemiringAction G B
inst_14 : SMulCommClass G A B
⊢ FaithfulSMul.{u_3, u_4} (A ⧸ p) (B ⧸ P)
have rw : Function.Injective.{u_3 + 1, u_4 + 1} (α := A ⧸ p) (β := B ⧸ P) (⇑(algebraMap (A ⧸ p) (B ⧸ P)) : (a : A ⧸ p) → B ⧸ P)
Tactic: rw [faithfulSMul_iff_algebraMap_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : CommRing C
inst_5 : Algebra A B
inst_6 : Algebra A C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst_10 : Q.LiesOver p
inst_11 : P.LiesOver p
G : Type u_6
inst_12 : Group G
inst_13 : MulSemiringAction G B
inst_14 : SMulCommClass G A B
a₁ : A ⧸ p
a : A
a₂ : A ⧸ p
b : A
hab :
  Eq.{u_4 + 1} (α := B ⧸ P)
    ((algebraMap (A ⧸ p) (B ⧸ P) : (a : A ⧸ p) → B ⧸ P) (Quot.mk (⇑(quotientRel p) : A → A → Prop) a) : B ⧸ P)
    ((algebraMap (A ⧸ p) (B ⧸ P) : (a : A ⧸ p) → B ⧸ P) (Quot.mk (⇑(quotientRel p) : A → A → Prop) b) : B ⧸ P)
⊢ Eq (α := A ⧸ p) (Quot.mk (⇑(quotientRel p) : A → A → Prop) a) (Quot.mk (⇑(quotientRel p) : A → A → Prop) b)
have apply : Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) (a - b) : B)
Tactic: apply Quotient.eq.mpr ((mem_of_liesOver P p (a - b)).mpr _)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : CommRing C
inst_5 : Algebra A B
inst_6 : Algebra A C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst_10 : Q.LiesOver p
inst_11 : P.LiesOver p
G : Type u_6
inst_12 : Group G
inst_13 : MulSemiringAction G B
inst_14 : SMulCommClass G A B
a₁ : A ⧸ p
a : A
a₂ : A ⧸ p
b : A
hab :
  Eq.{u_4 + 1} (α := B ⧸ P)
    ((algebraMap (A ⧸ p) (B ⧸ P) : (a : A ⧸ p) → B ⧸ P) (Quot.mk (⇑(quotientRel p) : A → A → Prop) a) : B ⧸ P)
    ((algebraMap (A ⧸ p) (B ⧸ P) : (a : A ⧸ p) → B ⧸ P) (Quot.mk (⇑(quotientRel p) : A → A → Prop) b) : B ⧸ P)
⊢ Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) (a - b) : B)
have rw : HSub.hSub (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B) ∈ P
Tactic: rw [map_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
P : Ideal B
p : Ideal A
inst_3 : P.LiesOver p
hp : p ≠ ⊤
⊢ Nontrivial.{u_4} (B ⧸ P)
have rwa : P ≠ ⊤
Tactic: rwa [Quotient.nontrivial_iff, ne_top_iff_of_liesOver _ p]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : CommRing C
inst_5 : Algebra A B
inst_6 : Algebra A C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst_10 : Q.LiesOver p
inst_11 : P.LiesOver p
G : Type u_6
inst_12 : Group G
inst_13 : MulSemiringAction G B
inst_14 : SMulCommClass G A B
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext ⟨x⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : CommRing C
inst_5 : Algebra A B
inst_6 : Algebra A C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst_10 : Q.LiesOver p
inst_11 : P.LiesOver p
G : Type u_6
inst_12 : Group G
inst_13 : MulSemiringAction G B
inst_14 : SMulCommClass G A B
g h : ↥(MulAction.stabilizer G P)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext ⟨x⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
A : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
P : Ideal B
p : Ideal A
inst_3 : P.LiesOver p
G : Type u_6
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
⊢ Eq (α := Subgroup ↥(MulAction.stabilizer G P))
    (MonoidHom.ker (M := AlgEquiv.{u_3, u_4, u_4} (A ⧸ p) (B ⧸ P) (B ⧸ P)) (stabilizerHom P p G))
    (Subgroup.subgroupOf (inertia G P) (MulAction.stabilizer G P))
have h : ∀ (σ : ↥(MulAction.stabilizer G P)),
  Membership.mem (γ := Subgroup ↥(MulAction.stabilizer G P))
      (MonoidHom.ker (M := AlgEquiv.{u_3, u_4, u_4} (A ⧸ p) (B ⧸ P) (B ⧸ P)) (stabilizerHom P p G)) σ ↔
    Membership.mem (γ := Subgroup ↥(MulAction.stabilizer G P))
      (Subgroup.subgroupOf (inertia G P) (MulAction.stabilizer G P)) σ
Tactic: ext σ
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : CommRing C
inst_5 : Algebra A B
inst_6 : Algebra A C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
P_1 : Ideal B
Q : Ideal C
p_1 : Ideal A
inst_10 : Q.LiesOver p_1
inst_11 : P_1.LiesOver p_1
G : Type u_6
inst_12 : Group G
inst_13 : MulSemiringAction G B
inst_14 : SMulCommClass G A B
p : Ideal R
P : Ideal A
inst_15 : P.IsPrime
inst_16 : P.LiesOver p
⊢ IsPrime (α := HasQuotient.Quotient A (B := Ideal A) (map (F := R →+* A) (algebraMap R A) p))
    (map (F := A →+* HasQuotient.Quotient A (B := Ideal A) (map (F := R →+* A) (algebraMap R A) p))
      (mk (map (F := R →+* A) (algebraMap R A) p)) P)
have hIP : map (F := R →+* A) (algebraMap R A) p ≤ P
Tactic: apply Ideal.isPrime_map_quotientMk_of_isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : CommRing C
inst_5 : Algebra A B
inst_6 : Algebra A C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
P_1 : Ideal B
Q : Ideal C
p_1 : Ideal A
inst_10 : Q.LiesOver p_1
inst_11 : P_1.LiesOver p_1
G : Type u_6
inst_12 : Group G
inst_13 : MulSemiringAction G B
inst_14 : SMulCommClass G A B
p : Ideal R
P : Ideal A
inst_15 : P.IsPrime
inst_16 : P.LiesOver p
⊢ map (F := R →+* A) (algebraMap R A) p ≤ P
have hIP : p ≤ comap (F := R →+* A) (algebraMap R A) P
Tactic: rw [Ideal.map_le_iff_le_comap, Ideal.LiesOver.over (p := p) (P := P)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : CommRing C
inst_5 : Algebra A B
inst_6 : Algebra A C
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
P_1 : Ideal B
Q : Ideal C
p_1 : Ideal A
inst_10 : Q.LiesOver p_1
inst_11 : P_1.LiesOver p_1
G : Type u_6
inst_12 : Group G
inst_13 : MulSemiringAction G B
inst_14 : SMulCommClass G A B
p : Ideal R
P : Ideal A
inst_15 : P.IsPrime
inst_16 : P.LiesOver p
hIP : p ≤ comap (F := R →+* A) (algebraMap R A) P
⊢ map (F := R →+* A) (algebraMap R A) p ≤ P
have hIP₁ : LE.le (α := Ideal R) (under R P) (under R P)
Tactic: rw [Ideal.map_le_iff_le_comap, Ideal.LiesOver.over (p := p) (P := P)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Over (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : Ring S
inst_3 : Algebra R S
inst_4 : Nontrivial S
inst_5 : Module.IsTorsionFree R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
hP : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P
⊢ P ≠ ⊥
have this : P.LiesOver p
Tactic: have : P.LiesOver p := hP.2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
Goal:
M : Type u_1
R_1 : Type u_2
inst : Monoid M
inst_1 : Semiring R_1
inst_2 : MulSemiringAction M R_1
R : Type u_3
inst_3 : CommRing R
inst_4 : MulSemiringAction M R
a : M
⊢ HSMul.hSMul (β := Ideal R) a 1 = 1
have simp : HSMul.hSMul (β := Ideal R) a ⊤ = ⊤
Tactic: simp only [Ideal.one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective (β := R) fun (r : R) ↦ a • r
⊢ (a • S).toAddSubmonoid = a • S.toAddSubmonoid
have h : ∀ (x : R), x ∈ (a • S).toAddSubmonoid ↔ x ∈ a • S.toAddSubmonoid
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pointwise (goal)
Goal:
M : Type u_1
inst : Monoid M
R : Type u_3
inst_1 : Ring R
inst_2 : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective (β := R) fun (r : R) ↦ a • r
⊢ Submodule.toAddSubgroup (a • S) = HSMul.hSMul (β := AddSubgroup R) a (Submodule.toAddSubgroup S)
have h : ∀ (x : R),
  Membership.mem (γ := AddSubgroup R) (Submodule.toAddSubgroup (a • S)) x ↔
    x ∈ HSMul.hSMul (β := AddSubgroup R) a (Submodule.toAddSubgroup S)
Tactic: ext