awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
I J : Ideal R
m : (z : (↑s : Type u_1)) → ℕ
a b : (z : (↑s : Type u_1)) → R
ha : ∀ (z : (↑s : Type u_1)), a z ∈ I
hb : ∀ (z : (↑s : Type u_1)), b z ∈ J
heq : ∀ (z : (↑s : Type u_1)), a z + b z = (↑z : R) ^ m z
refine :
  ∀ (z : R) (hz : z ∈ s),
    a (Subtype.mk (p := fun (x : R) ↦ x ∈ s) z hz) + b (Subtype.mk (p := fun (x : R) ↦ x ∈ s) z hz) ∈
      span (Set.range a) ⊔ J
⊢ ∃ (t : (↑s : Type u_1) → R), Set.range t ⊆ (↑I : Set R) ∧ s ⊆ (↑(span (Set.range t) ⊔ J).radical : Set R)

Tactic:
refine ⟨a, by rwa [Set.range_subset_iff], fun z hz ↦ ⟨m ⟨z, hz⟩, heq ⟨z, hz⟩ ▸ ?_⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
I J : Ideal R
m : (z : (↑s : Type u_1)) → ℕ
a b : (z : (↑s : Type u_1)) → R
ha : ∀ (z : (↑s : Type u_1)), a z ∈ I
hb : ∀ (z : (↑s : Type u_1)), b z ∈ J
heq : ∀ (z : (↑s : Type u_1)), a z + b z = (↑z : R) ^ m z
z : R
hz : z ∈ s
⊢ a (Subtype.mk (p := fun (x : R) ↦ x ∈ s) z hz) + b (Subtype.mk (p := fun (x : R) ↦ x ∈ s) z hz) ∈
    span (Set.range a) ⊔ J

Tactic:
Ideal.add_mem _ (mem_sup_left (subset_span ⟨⟨z, hz⟩, rfl⟩)) (mem_sup_right <| hb _)

Premises used: Ideal.subset_span, Ideal.mem_sup_left, Ideal.add_mem, Subtype.mk, Exists.intro, Ideal.mem_sup_right, rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
I J : Ideal R
m : (z : (↑s : Type u_1)) → ℕ
a b : (z : (↑s : Type u_1)) → R
ha : ∀ (z : (↑s : Type u_1)), a z ∈ I
hb : ∀ (z : (↑s : Type u_1)), b z ∈ J
heq : ∀ (z : (↑s : Type u_1)), a z + b z = (↑z : R) ^ m z
z : R
hz : z ∈ s
⊢ a (Subtype.mk (p := fun (x : R) ↦ x ∈ s) z hz) + b (Subtype.mk (p := fun (x : R) ↦ x ∈ s) z hz) ∈
    span (Set.range a) ⊔ J

Tactic:
exact Ideal.add_mem _ (mem_sup_left (subset_span ⟨⟨z, hz⟩, rfl⟩)) (mem_sup_right <| hb _)
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
p : Ideal R
P : Ideal S
inst_2 : Algebra R S
inst_3 : Algebra.{u_1, u_2} (R ⧸ p) (S ⧸ P)
inst_4 : IsScalarTower.{u_1, u_1, u_2} R (R ⧸ p) (S ⧸ P)
h :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ p) (β := S ⧸ P) (⇑(algebraMap (R ⧸ p) (S ⧸ P)) : (a : R ⧸ p) → S ⧸ P)
h₁ : ∀ (x : R), Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) x ↔ x ∈ p
⊢ comap (F := R →+* S) (algebraMap R S) P = p

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
p : Ideal R
P : Ideal S
inst_2 : Algebra R S
inst_3 : Algebra.{u_1, u_2} (R ⧸ p) (S ⧸ P)
inst_4 : IsScalarTower.{u_1, u_1, u_2} R (R ⧸ p) (S ⧸ P)
h :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ p) (β := S ⧸ P) (⇑(algebraMap (R ⧸ p) (S ⧸ P)) : (a : R ⧸ p) → S ⧸ P)
x : R
h₁ :
  Eq.{u_2 + 1} (α := S ⧸ P)
      ((algebraMap (R ⧸ p) (S ⧸ P) : (a : R ⧸ p) → S ⧸ P) ((Quotient.mk p : (a : R) → R ⧸ p) x) : S ⧸ P) (0 : S ⧸ P) ↔
    Eq (α := R ⧸ p) ((Quotient.mk p : (a : R) → R ⧸ p) x : R ⧸ p) (0 : R ⧸ p)
⊢ Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) x ↔ x ∈ p

Tactic:
rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← Quotient.eq_zero_iff_mem, Quotient.mk_algebraMap,
    IsScalarTower.algebraMap_apply R (R ⧸ p) (S ⧸ P), Quotient.algebraMap_eq]

Premises used: Ideal.Quotient.algebraMap_eq, Ideal.Quotient.eq_zero_iff_mem, HasQuotient.Quotient, Ideal.mem_comap, IsScalarTower.algebraMap_apply, Ideal.Quotient.mk_algebraMap
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
p : Ideal R
P : Ideal S
inst_2 : Algebra R S
inst_3 : Algebra.{u_1, u_2} (R ⧸ p) (S ⧸ P)
inst_4 : IsScalarTower.{u_1, u_1, u_2} R (R ⧸ p) (S ⧸ P)
h :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ p) (β := S ⧸ P) (⇑(algebraMap (R ⧸ p) (S ⧸ P)) : (a : R ⧸ p) → S ⧸ P)
x : R
⊢ Eq.{u_2 + 1} (α := S ⧸ P)
      ((algebraMap (R ⧸ p) (S ⧸ P) : (a : R ⧸ p) → S ⧸ P) ((Quotient.mk p : (a : R) → R ⧸ p) x) : S ⧸ P) (0 : S ⧸ P) ↔
    Eq (α := R ⧸ p) ((Quotient.mk p : (a : R) → R ⧸ p) x : R ⧸ p) (0 : R ⧸ p)

Tactic:
map_eq_zero_iff _ h

Premises used: map_eq_zero_iff
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
p : Ideal R
P : Ideal S
inst_2 : Algebra R S
inst_3 : Algebra.{u_1, u_2} (R ⧸ p) (S ⧸ P)
inst_4 : IsScalarTower.{u_1, u_1, u_2} R (R ⧸ p) (S ⧸ P)
h :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ p) (β := S ⧸ P) (⇑(algebraMap (R ⧸ p) (S ⧸ P)) : (a : R ⧸ p) → S ⧸ P)
x : R
⊢ Eq.{u_2 + 1} (α := S ⧸ P)
      ((algebraMap (R ⧸ p) (S ⧸ P) : (a : R ⧸ p) → S ⧸ P) ((Quotient.mk p : (a : R) → R ⧸ p) x) : S ⧸ P) (0 : S ⧸ P) ↔
    Eq (α := R ⧸ p) ((Quotient.mk p : (a : R) → R ⧸ p) x : R ⧸ p) (0 : R ⧸ p)

Tactic:
exact map_eq_zero_iff _ h

Premises used: map_eq_zero_iff
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
p : Ideal R
inst_2 : Algebra R S
x : R
⊢ Eq (α := 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))
    ((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))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
p : Ideal R
inst_2 : Algebra R S
x : R
y : S
⊢ HSMul.hSMul (α := R ⧸ p) (β := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      ((mk p : (a : R) → R ⧸ p) x : R ⧸ p)
      ((mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
        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)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) y)

Tactic:
Algebra.smul_def _ _

Premises used: Submodule.Quotient.mk, Quotient.map₂, Algebra.smul_def
-- Module: Mathlib.RingTheory.Ideal.Over
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))
rw₂ 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))
⊢ 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))

Tactic:
rw [Quotient.algebraMap_eq, Quotient.algebraMap_quotient_map_quotient,
      Quotient.mk_algebraMap]

Premises used: Ideal.Quotient.algebraMap_eq, Ideal.Quotient.algebraMap_quotient_map_quotient, Ideal.Quotient.mk_algebraMap
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : Semiring B
inst_2 : Algebra A B
P : Ideal B
⊢ Eq (α := Ideal A) (under A P) (comap (F := A →+* B) (algebraMap A B) P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : Semiring B
inst_2 : Algebra A B
P : Ideal B
x : A
⊢ Membership.mem (γ := Ideal A) (under A P) x ↔ Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) x : B)

Tactic:
mem_comap

Premises used: Set.Mem, Ideal.mem_comap
-- 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
C : Type u_4
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra A B
inst_5 : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
G : Type u_5
inst_6 : Group G
inst_7 : MulSemiringAction G B
inst_8 : SMulCommClass G A B
g : G
hP : P.IsPrime
⊢ IsPrime (Ideal.under A P)

Tactic:
hP.comap (algebraMap A B)

Premises used: Algebra.algebraMap, Ideal.IsPrime.comap
-- Module: Mathlib.RingTheory.Ideal.Over
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
h : ∀ (a : A), Membership.mem (γ := Ideal A) (under A (g • P)) a ↔ Membership.mem (γ := Ideal A) (under A P) a
⊢ Eq (α := Ideal A) (under A (g • P)) (under A P)

Tactic:
ext a
-- Module: Mathlib.RingTheory.Ideal.Over
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)
h₃ 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)
⊢ Membership.mem (γ := Ideal A) (under A (g • P)) a ↔ Membership.mem (γ := Ideal A) (under A P) a

Tactic:
rw [mem_comap, mem_comap, mem_pointwise_smul_iff_inv_smul_mem, smul_algebraMap]

Premises used: Ideal.mem_pointwise_smul_iff_inv_smul_mem, smul_algebraMap, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Over
Goal:
A : Type u_2
inst : CommSemiring A
B : Type u_3
inst_1 : Semiring B
inst_2 : Algebra A B
⊢ Eq (α := Ideal A) (under.{u_2, u_3} A (B := B) ⊤) ⊤

Tactic:
comap_top

Premises used: Ideal.comap_top
-- Module: Mathlib.RingTheory.Ideal.Over
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 = under A P

Tactic:
LiesOver.over

Premises used: Ideal.LiesOver.over
-- Module: Mathlib.RingTheory.Ideal.Over
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
rw : Membership.mem (γ := Ideal A) (under A P) x ↔ Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) x : B)
⊢ x ∈ p ↔ Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) x : B)

Tactic:
rw [P.over_def p]

Premises used: Ideal.over_def
-- Module: Mathlib.RingTheory.Ideal.Over
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
⊢ Membership.mem (γ := Ideal A) (under A P) x ↔ Membership.mem (α := B) P ((algebraMap A B : (a : A) → B) x : B)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Over
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
rw : P = ⊤ ↔ Eq (α := Ideal A) (under A P) ⊤
⊢ P = ⊤ ↔ p = ⊤

Tactic:
rw [P.over_def p]

Premises used: Ideal.over_def
-- Module: Mathlib.RingTheory.Ideal.Over
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 = ⊤ ↔ Eq (α := Ideal A) (under A P) ⊤

Tactic:
comap_eq_top_iff.symm

Premises used: Ideal.comap_eq_top_iff, Iff.symm
-- Module: Mathlib.RingTheory.Ideal.Over
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 = ⊤ ↔ Eq (α := Ideal A) (under A P) ⊤

Tactic:
exact comap_eq_top_iff.symm

Premises used: Ideal.comap_eq_top_iff, Iff.symm
-- Module: Mathlib.RingTheory.Ideal.Over
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 ≠ ⊤

Tactic:
(eq_top_iff_of_liesOver ..).ne

Premises used: Iff.ne, Ideal.eq_top_iff_of_liesOver
-- Module: Mathlib.RingTheory.Ideal.Over
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
rw : IsPrime (under A P)
⊢ p.IsPrime

Tactic:
rw [over_def P p]

Premises used: Ideal.over_def
-- Module: Mathlib.RingTheory.Ideal.Over
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
⊢ IsPrime (under A P)

Tactic:
IsPrime.under A P

Premises used: Ideal.IsPrime.under
-- Module: Mathlib.RingTheory.Ideal.Over
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
⊢ IsPrime (under A P)

Tactic:
exact IsPrime.under A P

Premises used: Ideal.IsPrime.under
-- Module: Mathlib.RingTheory.Ideal.Over
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
rw : p = under A (comap f Q)
⊢ p = under A P

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Ideal.Over
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 (comap f Q)

Tactic:
(over_def Q p).trans <|
      congrFun (congrFun (congrArg
        comap ((AlgHomClass.toAlgHom f : B →ₐ[A] C).comp_algebraMap.symm)) _) Q

Premises used: AlgHom.comp_algebraMap, congrArg, congrFun, Ideal.comap, Ideal.over_def, Eq.symm, AlgHomClass.toAlgHom, Eq.trans
-- Module: Mathlib.RingTheory.Ideal.Over
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 (comap f Q)

Tactic:
exact (over_def Q p).trans <|
      congrFun (congrFun (congrArg
        comap ((AlgHomClass.toAlgHom f : B →ₐ[A] C).comp_algebraMap.symm)) _) Q

Premises used: AlgHom.comp_algebraMap, congrArg, congrFun, Ideal.comap, Ideal.over_def, Eq.symm, AlgHomClass.toAlgHom, Eq.trans
-- Module: Mathlib.RingTheory.Ideal.Over
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 = comap (F := C ≃+* B) (RingEquiv.symm (↑σ : B ≃+* C)) P

Tactic:
rw [← show _ = P.map σ from comap_symm (RingEquivClass.toRingEquiv σ)] at h

Premises used: Ideal.comap_symm, RingEquivClass.toRingEquiv
-- Module: Mathlib.RingTheory.Ideal.Over
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 = comap (F := C ≃+* B) (RingEquiv.symm (↑σ : B ≃+* C)) P
⊢ Q.LiesOver p

Tactic:
of_eq_comap p (AlgEquivClass.toAlgEquiv σ : B ≃ₐ[A] C).symm h

Premises used: Ideal.LiesOver.of_eq_comap, AlgEquiv.symm, AlgEquivClass.toAlgEquiv
-- Module: Mathlib.RingTheory.Ideal.Over
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 = comap (F := C ≃+* B) (RingEquiv.symm (↑σ : B ≃+* C)) P
⊢ Q.LiesOver p

Tactic:
exact of_eq_comap p (AlgEquivClass.toAlgEquiv σ : B ≃ₐ[A] C).symm h

Premises used: Ideal.LiesOver.of_eq_comap, AlgEquiv.symm, AlgEquivClass.toAlgEquiv
-- 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
C : Type u_4
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra A B
inst_5 : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
G : Type u_5
inst_6 : Group G
inst_7 : MulSemiringAction G B
inst_8 : SMulCommClass G A B
g : G
h : P.LiesOver p
⊢ (g • P).LiesOver p

Tactic:
⟨h.over.trans (under_smul A P g).symm⟩

Premises used: Ideal.under_smul, Ideal.LiesOver.mk, Ideal.LiesOver.over, Eq.symm, Eq.trans
-- 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
C : Type u_4
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra A B
inst_5 : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
G : Type u_5
inst_6 : Group G
inst_7 : MulSemiringAction G B
inst_8 : SMulCommClass G A B
g : G
inst_9 : Q.LiesOver p
F : Type u_6
inst_10 : FunLike F B C
inst_11 : AlgHomClass F A B C
f : F
⊢ LiesOver (comap f Q) p

Tactic:
LiesOver.of_eq_comap p f rfl

Premises used: Ideal.LiesOver.of_eq_comap, rfl
-- 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
C : Type u_4
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra A B
inst_5 : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
G : Type u_5
inst_6 : Group G
inst_7 : MulSemiringAction G B
inst_8 : SMulCommClass G A B
g : G
inst_9 : P.LiesOver p
E : Type u_6
inst_10 : EquivLike E B C
inst_11 : AlgEquivClass E A B C
σ : E
⊢ LiesOver.{u_2, u_4} (B := C) (map σ P) p

Tactic:
LiesOver.of_eq_map_equiv p σ rfl

Premises used: Ideal.LiesOver.of_eq_map_equiv, rfl
-- Module: Mathlib.RingTheory.Ideal.Over
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
simp_rw :
  Eq (α := Ideal A)
    (comap (F := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap A B)) 𝔓)
    (under A 𝔓)
⊢ Eq (α := Ideal A) (under A (under B 𝔓)) (under A 𝔓)

Tactic:
simp_rw [comap_comap, ← IsScalarTower.algebraMap_eq]

Premises used: IsScalarTower.algebraMap_eq, Ideal.comap_comap
-- Module: Mathlib.RingTheory.Ideal.Over
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 𝔓)
rw₂ rw₃ : Eq (α := Ideal A) (under A 𝔓) (under A 𝔓)
⊢ p = under A 𝔓

Tactic:
rw [P.over_def p, 𝔓.over_def P, under_under]

Premises used: Ideal.under_under, Ideal.over_def
-- 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
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)
⊢ 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))

Tactic:
apply le_comap_of_map_le

Premises used: Ideal.le_comap_of_map_le
-- 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
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)))
⊢ 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:
rw [map_map, ← IsScalarTower.algebraMap_eq, map_le_iff_le_comap,
    IsScalarTower.algebraMap_eq A B D, ← comap_comap]

Premises used: Ideal.map_le_iff_le_comap, Ideal.map_map, IsScalarTower.algebraMap_eq, Ideal.comap_comap
-- 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
⊢ 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:
comap_mono <| le_comap_map

Premises used: Set.Mem, Ideal.comap_mono, Ideal.le_comap_map
-- 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
⊢ 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:
exact comap_mono <| le_comap_map

Premises used: Ideal.comap_mono, Ideal.le_comap_map