awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Over
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
h₁ : IsMaximal.{u_5} (α := C) (map (F := A →+* C) (algebraMap A C) (under A P))
h₂ : Ne.{u_6 + 1} (α := Ideal D) (map (F := B →+* D) (algebraMap B D) P) ⊤
⊢ Eq (α := Ideal C) (under.{u_5, u_6} C (B := D) (map (F := B →+* D) (algebraMap B D) P))
    (map (F := A →+* C) (algebraMap A C) (under A P))

Tactic:
(IsCoatom.le_iff_eq (isMaximal_def.mp h₁) (comap_ne_top (algebraMap C D) h₂)).mp <|
    map_under_le_under_map P

Premises used: Ideal.map_under_le_under_map, Algebra.algebraMap, Ideal.comap_ne_top, Iff.mp, IsCoatom.le_iff_eq, Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.Ideal.Over
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
⊢ (↑p : Set A) = (⇑(algebraMap A C) : (a : A) → C) ⁻¹' (↑𝔓 : Set C)

Tactic:
rw [liesOver_iff, under_def, SetLike.ext'_iff, coe_comap] at hPp

Premises used: Ideal.liesOver_iff, Ideal.under_def, Ideal.coe_comap, SetLike.ext'_iff
-- Module: Mathlib.RingTheory.Ideal.Over
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 : (↑p : Set A) = (⇑(algebraMap A C) : (a : A) → C) ⁻¹' (↑𝔓 : Set C)
⊢ (↑(Submonoid.map (F := A →+* C) (algebraMap A C)
          { carrier := ((⇑(algebraMap A C) : (a : A) → C) ⁻¹' (↑𝔓 : Set C))ᶜ, mul_mem' := ⋯, one_mem' := ⋯ :
            Submonoid A }) :
      Set C) ⊆
    (↑𝔓 : Set C)ᶜ

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Over
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 : (↑p : Set A) = (⇑(algebraMap A C) : (a : A) → C) ⁻¹' (↑𝔓 : Set C)
⊢ Disjoint (↑(Algebra.algebraMapSubmonoid C p.primeCompl) : Set C) (↑𝔓 : Set C)

Tactic:
simpa only [Algebra.algebraMapSubmonoid, primeCompl, hPp, ← le_compl_iff_disjoint_left]
    using Set.subset_compl_comm.mp (by simp)

Premises used: Set.subset_compl_comm, le_compl_iff_disjoint_left, Iff.mp, Ideal.primeCompl, Algebra.algebraMapSubmonoid
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : CommSemiring B
inst_2 : Algebra A B
P : Ideal B
p : Ideal A
inst_3 : p.IsPrime
inst_4 : P.IsPrime
inst_5 : P.LiesOver p
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Algebra.algebraMapSubmonoid B p.primeCompl = P.primeCompl

Tactic:
simpa [over_def P p] using P.map_primeCompl_comap_of_surjective (algebraMap A B) hf

Premises used: Ideal.map_primeCompl_comap_of_surjective, Algebra.algebraMap, Ideal.over_def
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommSemiring A
B : Type u_3
inst_2 : CommSemiring B
C : Type u_4
inst_3 : Semiring C
inst_4 : Algebra A B
inst_5 : Algebra B C
inst_6 : Algebra A C
inst_7 : IsScalarTower A B C
𝔓 : Ideal C
P : Ideal B
p : Ideal A
inst_8 : 𝔓.LiesOver p
⊢ LiesOver (under B 𝔓) p

Tactic:
LiesOver.tower_bot 𝔓 (𝔓.under B) p

Premises used: Ideal.LiesOver.tower_bot, Ideal.under
-- Module: Mathlib.RingTheory.Ideal.Over
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
⊢ Eq (α := Ideal A) (under.{u_2, u_3} A (B := B) ⊥) ⊥

Tactic:
comap_bot_of_injective (algebraMap A B) (FaithfulSMul.algebraMap_injective A B)

Premises used: Algebra.algebraMap, Ideal.comap_bot_of_injective, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Ideal.Over
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
contrapose : ∀ (hp : P = ⊥), p = ⊥
⊢ P ≠ ⊥

Tactic:
contrapose hp
-- Module: Mathlib.RingTheory.Ideal.Over
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) ⊥) ⊥
rw₂ rw₃ : Eq.{u_2 + 1} (α := Ideal A) ⊥ ⊥
⊢ p = ⊥

Tactic:
rw [over_def P p, hp, under_bot]

Premises used: Ideal.under_bot, Ideal.over_def
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
A : Type u_3
inst_1 : Field K
inst_2 : Semiring A
inst_3 : Algebra K A
P : Ideal A
inst_4 : P.IsPrime
⊢ LiesOver.{u_2, u_3} (A := K) P ⊥

Tactic:
⟨((IsSimpleOrder.eq_bot_or_eq_top _).resolve_right Ideal.IsPrime.ne_top').symm⟩

Premises used: Ideal.LiesOver.mk, Or.resolve_right, Ideal.IsPrime.ne_top', Eq.symm, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.RingTheory.Ideal.Over
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
x : A
⊢ Eq.{u_4 + 1} (α := B ⧸ P) ((algebraMap (A ⧸ p) (B ⧸ P) : (a : A ⧸ p) → B ⧸ P) ((mk p : (a : A) → A ⧸ p) x) : B ⧸ P)
    ((mk P : (a : B) → B ⧸ P) ((algebraMap A B : (a : A) → B) x) : B ⧸ P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Over
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
⊢ IsScalarTower.{u_2, u_3, u_4} R (A ⧸ p) (B ⧸ P)

Tactic:
IsScalarTower.of_algebraMap_eq' <|
    congrArg (algebraMap B (B ⧸ P)).comp (IsScalarTower.algebraMap_eq R A B)

Premises used: Algebra.algebraMap, congrArg, IsScalarTower.of_algebraMap_eq', HasQuotient.Quotient, RingHom.comp, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Ideal.Over
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
rw :
  Function.Injective.{u_3 + 1, u_4 + 1} (α := A ⧸ p) (β := B ⧸ P) (⇑(algebraMap (A ⧸ p) (B ⧸ P)) : (a : A ⧸ p) → B ⧸ P)
⊢ FaithfulSMul.{u_3, u_4} (A ⧸ p) (B ⧸ P)

Tactic:
rw [faithfulSMul_iff_algebraMap_injective]

Premises used: faithfulSMul_iff_algebraMap_injective
-- Module: Mathlib.RingTheory.Ideal.Over
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)
apply : Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) (a - b) : B)
⊢ Eq (α := A ⧸ p) (Quot.mk (⇑(quotientRel p) : A → A → Prop) a) (Quot.mk (⇑(quotientRel p) : A → A → Prop) b)

Tactic:
apply Quotient.eq.mpr ((mem_of_liesOver P p (a - b)).mpr _)

Premises used: Iff.mpr, HSub.hSub, Ideal.mem_of_liesOver, Ideal.Quotient.eq
-- Module: Mathlib.RingTheory.Ideal.Over
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)
rw : HSub.hSub (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B) ∈ P
⊢ Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) (a - b) : B)

Tactic:
rw [map_sub]

Premises used: map_sub
-- Module: Mathlib.RingTheory.Ideal.Over
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)
⊢ HSub.hSub (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B) ∈ P

Tactic:
Quotient.eq.mp hab

Premises used: Set.Mem, Ideal.Quotient.eq, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Over
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)
⊢ HSub.hSub (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B) ∈ P

Tactic:
exact Quotient.eq.mp hab

Premises used: Ideal.Quotient.eq, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Over
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 ≠ ⊤
rwa : P ≠ ⊤
rwa₁ rwa₂ rwa₃ rwa₄ : p ≠ ⊤
⊢ Nontrivial.{u_4} (B ⧸ P)

Tactic:
rwa [Quotient.nontrivial_iff, ne_top_iff_of_liesOver _ p]

Premises used: Ideal.Quotient.nontrivial_iff, Ideal.ne_top_iff_of_liesOver
-- Module: Mathlib.RingTheory.Ideal.Over
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.IsPrime
⊢ Nontrivial.{u_4} (B ⧸ P)

Tactic:
nontrivial_of_liesOver_of_ne_top P hp.ne_top

Premises used: Ideal.Quotient.nontrivial_of_liesOver_of_ne_top, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.Over
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
E : Type u_7
inst_15 : EquivLike E B C
inst_16 : AlgEquivClass E A B C
σ : E
h : Q = map σ P
r : A ⧸ p
x : A
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
congrArg (Ideal.Quotient.mk Q) (AlgHomClass.commutes σ x)

Premises used: Quotient.liftOn', congrArg, Ideal.Quotient.mk, AddCon.liftOn, Submodule.Quotient.mk, AlgHomClass.commutes, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Over
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
E : Type u_7
inst_15 : EquivLike E B C
inst_16 : AlgEquivClass E A B C
σ : E
h : Q = map σ P
r : A ⧸ p
x : A
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact congrArg (Ideal.Quotient.mk Q) (AlgHomClass.commutes σ x)

Premises used: congrArg, Ideal.Quotient.mk, AlgHomClass.commutes, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing 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
inst_6 : P.LiesOver p
E : Type u_7
inst_7 : EquivLike E B C
inst_8 : AlgEquivClass E A B C
σ : E
h : Q = map σ P
x : B
⊢ Eq.{u_5 + 1} (α := C ⧸ Q)
    (((algEquivOfEqMap p σ h : AlgEquiv.{u_3, u_4, u_5} (A ⧸ p) (B ⧸ P) (C ⧸ Q)) : (a : B ⧸ P) → C ⧸ Q)
        ((mk P : (a : B) → B ⧸ P) x) :
      C ⧸ Q)
    ((mk Q : (a : C) → C ⧸ Q) ((σ : (a : B) → C) x) : C ⧸ Q)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing 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
inst_6 : P.LiesOver p
E : Type u_7
inst_7 : EquivLike E B C
inst_8 : AlgEquivClass E A B C
σ : E
h : P = comap σ Q
x : B
⊢ Eq.{u_5 + 1} (α := C ⧸ Q)
    (((algEquivOfEqComap p σ h : AlgEquiv.{u_3, u_4, u_5} (A ⧸ p) (B ⧸ P) (C ⧸ Q)) : (a : B ⧸ P) → C ⧸ Q)
        ((mk P : (a : B) → B ⧸ P) x) :
      C ⧸ Q)
    ((mk Q : (a : C) → C ⧸ Q) ((σ : (a : B) → C) x) : C ⧸ Q)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Over
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
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext ⟨x⟩
-- Module: Mathlib.RingTheory.Ideal.Over
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 : B ⧸ P
x : B
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
congrArg (Ideal.Quotient.mk P) (one_smul G x)

Premises used: Quotient.liftOn', congrArg, Ideal.Quotient.mk, AddCon.liftOn, Submodule.Quotient.mk, one_smul, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Over
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 : B ⧸ P
x : B
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact congrArg (Ideal.Quotient.mk P) (one_smul G x)

Premises used: congrArg, Ideal.Quotient.mk, one_smul, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Over
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)
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext ⟨x⟩
-- Module: Mathlib.RingTheory.Ideal.Over
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)
a : B ⧸ P
x : B
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
congrArg (Ideal.Quotient.mk P) (mul_smul g h x)

Premises used: Quotient.liftOn', congrArg, Ideal.Quotient.mk, AddCon.liftOn, Submodule.Quotient.mk, DFunLike.coe, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Ideal.Over
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)
a : B ⧸ P
x : B
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact congrArg (Ideal.Quotient.mk P) (mul_smul g h x)

Premises used: congrArg, Ideal.Quotient.mk, DFunLike.coe, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Ideal.Over
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
g : ↥(MulAction.stabilizer G P)
b : B
⊢ Eq (α := B ⧸ P)
    (((((stabilizerHom P p G :
                  MonoidHom.{u_6, u_4} (↥(MulAction.stabilizer G P))
                    (AlgEquiv.{u_3, u_4, u_4} (A ⧸ p) (B ⧸ P) (B ⧸ P))) :
                (a : ↥(MulAction.stabilizer G P)) → (B ⧸ P) ≃ₐ[A ⧸ p] B ⧸ P)
              g :
            AlgEquiv.{u_3, u_4, u_4} (A ⧸ p) (B ⧸ P) (B ⧸ P)) :
          (a : B ⧸ P) → B ⧸ P)
        ((mk P : (a : B) → B ⧸ P) b) :
      B ⧸ P)
    ((mk P : (a : B) → B ⧸ P) (g • b) : B ⧸ P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Over
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
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)) σ
⊢ 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))

Tactic:
ext σ
-- Module: Mathlib.RingTheory.Ideal.Over
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
σ : ↥(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:
simp [DFunLike.ext_iff, mk_surjective.forall, Quotient.eq]

Premises used: Function.Surjective.forall, DFunLike.ext_iff, Ideal.Quotient.mk_surjective, Ideal.Quotient.eq
-- Module: Mathlib.RingTheory.Ideal.Over
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 G)
    (Subgroup.map (G := ↥(MulAction.stabilizer G P)) (Subgroup.subtype (MulAction.stabilizer G P))
      (MonoidHom.ker (M := AlgEquiv.{u_3, u_4, u_4} (A ⧸ p) (B ⧸ P) (B ⧸ P)) (stabilizerHom P p G)))
    (inertia G P)

Tactic:
simp [ker_stabilizerHom, Ideal.inertia_le_stabilizer]

Premises used: Ideal.inertia_le_stabilizer, Ideal.Quotient.ker_stabilizerHom
-- Module: Mathlib.RingTheory.Ideal.Over
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 : map (F := R →+* A) (algebraMap R A) p ≤ 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)

Tactic:
apply Ideal.isPrime_map_quotientMk_of_isPrime

Premises used: Ideal.isPrime_map_quotientMk_of_isPrime