awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.CotangentBaseChange (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
I : Ideal S
inst_5 : Module.Flat R T
a : S →+* T ⊗[R] S := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : Cotangent (R := T ⊗[R] S) (map a I) →ₗ[T] T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2 := sorry
g : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent →ₗ[T]
  TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) :=
  ((AlgebraTensorModule.lTensor T T :
        (I.Cotangent →ₗ[R] S ⧸ HPow.hPow (β := ℕ) I 2) →ₗ[R]
          TensorProduct.{u_1, u_3, u_2} R T I.Cotangent →ₗ[T]
            TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2)) :
      (a : I.Cotangent →ₗ[R] S ⧸ I ^ 2) → T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2))
    ((↑R :
        {S M M₂ : Type u_2} →
          [inst : Semiring R] →
            [inst_6 : Semiring S] →
              [inst_7 : AddCommMonoid M] →
                [inst_8 : AddCommMonoid M₂] →
                  [inst_9 : Module R M] →
                    [inst_10 : Module R M₂] →
                      [inst_11 : Module S M] →
                        [inst_12 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      I.cotangentToQuotientSquare)
hₐ : TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) ≃ₐ[T]
  T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2 :=
  AlgEquiv.trans
    (Algebra.TensorProduct.tensorQuotientEquiv T S T (HPow.hPow (β := ℕ) I 2) :
      TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) ≃ₐ[T]
        HasQuotient.Quotient (T ⊗[R] S) (B := Ideal (T ⊗[R] S))
          (map (F := S →ₐ[R] T ⊗[R] S) Algebra.TensorProduct.includeRight (HPow.hPow (β := ℕ) I 2)))
    (quotientEquivAlgOfEq T ⋯ :
      HasQuotient.Quotient (T ⊗[R] S) (B := Ideal (T ⊗[R] S))
          (map (F := S →ₐ[R] T ⊗[R] S) Algebra.TensorProduct.includeRight (HPow.hPow (β := ℕ) I 2)) ≃ₐ[T]
        T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
⊢ Function.Injective (α := TensorProduct.{u_1, u_3, u_2} R T I.Cotangent) (β :=
    T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
    (⇑(f ∘ₗ tensorCotangentHom R T I) : (a_1 : T ⊗[R] I.Cotangent) → T ⊗[R] S ⧸ map a I ^ 2)
have this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
Tactic: have : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g := by
    ext x
    obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
    dsimp [f, g, hₐ]
    rw [tensorCotangentHom_tmul, one_smul, Ideal.toCotangent_to_quotient_square]
    simp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.CotangentBaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
I : Ideal S
inst_5 : Module.Flat R T
a : S →+* T ⊗[R] S := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : Cotangent (R := T ⊗[R] S) (map a I) →ₗ[T] T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2 := sorry
g : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent →ₗ[T]
  TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) :=
  ((AlgebraTensorModule.lTensor T T :
        (I.Cotangent →ₗ[R] S ⧸ HPow.hPow (β := ℕ) I 2) →ₗ[R]
          TensorProduct.{u_1, u_3, u_2} R T I.Cotangent →ₗ[T]
            TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2)) :
      (a : I.Cotangent →ₗ[R] S ⧸ I ^ 2) → T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2))
    ((↑R :
        {S M M₂ : Type u_2} →
          [inst : Semiring R] →
            [inst_6 : Semiring S] →
              [inst_7 : AddCommMonoid M] →
                [inst_8 : AddCommMonoid M₂] →
                  [inst_9 : Module R M] →
                    [inst_10 : Module R M₂] →
                      [inst_11 : Module S M] →
                        [inst_12 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      I.cotangentToQuotientSquare)
hₐ : TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) ≃ₐ[T]
  T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2 :=
  AlgEquiv.trans
    (Algebra.TensorProduct.tensorQuotientEquiv T S T (HPow.hPow (β := ℕ) I 2) :
      TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) ≃ₐ[T]
        HasQuotient.Quotient (T ⊗[R] S) (B := Ideal (T ⊗[R] S))
          (map (F := S →ₐ[R] T ⊗[R] S) Algebra.TensorProduct.includeRight (HPow.hPow (β := ℕ) I 2)))
    (quotientEquivAlgOfEq T ⋯ :
      HasQuotient.Quotient (T ⊗[R] S) (B := Ideal (T ⊗[R] S))
          (map (F := S →ₐ[R] T ⊗[R] S) Algebra.TensorProduct.includeRight (HPow.hPow (β := ℕ) I 2)) ≃ₐ[T]
        T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
⊢ Function.Injective (α := TensorProduct.{u_1, u_3, u_2} R T I.Cotangent) (β :=
    T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
    (⇑(f ∘ₗ tensorCotangentHom R T I) : (a_1 : T ⊗[R] I.Cotangent) → T ⊗[R] S ⧸ map a I ^ 2)
have rw : Function.Injective (α := TensorProduct.{u_1, u_3, u_2} R T I.Cotangent) (β :=
  T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
  (Function.comp (β := TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2))
    (⇑hₐ.toLinearMap : (a_1 : T ⊗[R] (S ⧸ I ^ 2)) → T ⊗[R] S ⧸ map a I ^ 2)
    (⇑g : (a : T ⊗[R] I.Cotangent) → T ⊗[R] (S ⧸ I ^ 2)))
Tactic: rw [this, LinearMap.coe_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.CotangentBaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
I : Ideal S
inst_5 : Module.Flat R T
a : S →+* T ⊗[R] S := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : Cotangent (R := T ⊗[R] S) (map a I) →ₗ[T] T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2 := sorry
g : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent →ₗ[T]
  TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) :=
  ((AlgebraTensorModule.lTensor T T :
        (I.Cotangent →ₗ[R] S ⧸ HPow.hPow (β := ℕ) I 2) →ₗ[R]
          TensorProduct.{u_1, u_3, u_2} R T I.Cotangent →ₗ[T]
            TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2)) :
      (a : I.Cotangent →ₗ[R] S ⧸ I ^ 2) → T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2))
    ((↑R :
        {S M M₂ : Type u_2} →
          [inst : Semiring R] →
            [inst_6 : Semiring S] →
              [inst_7 : AddCommMonoid M] →
                [inst_8 : AddCommMonoid M₂] →
                  [inst_9 : Module R M] →
                    [inst_10 : Module R M₂] →
                      [inst_11 : Module S M] →
                        [inst_12 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      I.cotangentToQuotientSquare)
hₐ : TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) ≃ₐ[T]
  T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2 :=
  AlgEquiv.trans
    (Algebra.TensorProduct.tensorQuotientEquiv T S T (HPow.hPow (β := ℕ) I 2) :
      TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) ≃ₐ[T]
        HasQuotient.Quotient (T ⊗[R] S) (B := Ideal (T ⊗[R] S))
          (map (F := S →ₐ[R] T ⊗[R] S) Algebra.TensorProduct.includeRight (HPow.hPow (β := ℕ) I 2)))
    (quotientEquivAlgOfEq T ⋯ :
      HasQuotient.Quotient (T ⊗[R] S) (B := Ideal (T ⊗[R] S))
          (map (F := S →ₐ[R] T ⊗[R] S) Algebra.TensorProduct.includeRight (HPow.hPow (β := ℕ) I 2)) ≃ₐ[T]
        T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
⊢ Function.Injective (α := TensorProduct.{u_1, u_3, u_2} R T I.Cotangent) (β :=
    T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
    (Function.comp (β := TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2))
      (⇑hₐ.toLinearMap : (a_1 : T ⊗[R] (S ⧸ I ^ 2)) → T ⊗[R] S ⧸ map a I ^ 2)
      (⇑g : (a : T ⊗[R] I.Cotangent) → T ⊗[R] (S ⧸ I ^ 2)))
have apply : Function.Injective (α := TensorProduct.{u_1, u_3, u_2} R T I.Cotangent) (β :=
  TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2)) (⇑g : (a : T ⊗[R] I.Cotangent) → T ⊗[R] (S ⧸ I ^ 2))
Tactic: apply hₐ.injective.comp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.CotangentBaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
I : Ideal S
inst_5 : Module.Flat R T
a : S →+* T ⊗[R] S := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : Cotangent (R := T ⊗[R] S) (map a I) →ₗ[T] T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2 := sorry
g : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent →ₗ[T]
  TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) :=
  ((AlgebraTensorModule.lTensor T T :
        (I.Cotangent →ₗ[R] S ⧸ HPow.hPow (β := ℕ) I 2) →ₗ[R]
          TensorProduct.{u_1, u_3, u_2} R T I.Cotangent →ₗ[T]
            TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2)) :
      (a : I.Cotangent →ₗ[R] S ⧸ I ^ 2) → T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2))
    ((↑R :
        {S M M₂ : Type u_2} →
          [inst : Semiring R] →
            [inst_6 : Semiring S] →
              [inst_7 : AddCommMonoid M] →
                [inst_8 : AddCommMonoid M₂] →
                  [inst_9 : Module R M] →
                    [inst_10 : Module R M₂] →
                      [inst_11 : Module S M] →
                        [inst_12 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      I.cotangentToQuotientSquare)
hₐ : TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) ≃ₐ[T]
  T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2 :=
  AlgEquiv.trans
    (Algebra.TensorProduct.tensorQuotientEquiv T S T (HPow.hPow (β := ℕ) I 2) :
      TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) ≃ₐ[T]
        HasQuotient.Quotient (T ⊗[R] S) (B := Ideal (T ⊗[R] S))
          (map (F := S →ₐ[R] T ⊗[R] S) Algebra.TensorProduct.includeRight (HPow.hPow (β := ℕ) I 2)))
    (quotientEquivAlgOfEq T ⋯ :
      HasQuotient.Quotient (T ⊗[R] S) (B := Ideal (T ⊗[R] S))
          (map (F := S →ₐ[R] T ⊗[R] S) Algebra.TensorProduct.includeRight (HPow.hPow (β := ℕ) I 2)) ≃ₐ[T]
        T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
⊢ Function.Injective (α := TensorProduct.{u_1, u_3, u_2} R T I.Cotangent) (β :=
    TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2)) (⇑g : (a : T ⊗[R] I.Cotangent) → T ⊗[R] (S ⧸ I ^ 2))
have apply : Function.Injective (α := I.Cotangent) (β := S ⧸ HPow.hPow (β := ℕ) I 2)
  (⇑((↑R :
          {S M M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_6 : Semiring S] →
                [inst_7 : AddCommMonoid M] →
                  [inst_8 : AddCommMonoid M₂] →
                    [inst_9 : Module R M] →
                      [inst_10 : Module R M₂] →
                        [inst_11 : Module S M] →
                          [inst_12 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        I.cotangentToQuotientSquare) :
    (a : I.Cotangent) → S ⧸ I ^ 2)
Tactic: apply Module.Flat.lTensor_preserves_injective_linearMap (M := T)
      (I.cotangentToQuotientSquare.restrictScalars R)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Defs (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
⊢ y * x ∈ I ↔ x ∈ I
have refine : ∀ (h : y * x ∈ I), x ∈ I
Tactic: refine ⟨fun h => ?_, fun h => I.mul_mem_left y h⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Defs (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
⊢ x ∈ I
have obtain : ∀ (y' : α) (hy' : y' * y = 1), x ∈ I
Tactic: obtain ⟨y', hy'⟩ := hy.exists_left_inv
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Defs (hypothesis)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
⊢ x ∈ I
have this : y' * (y * x) ∈ I
Tactic: have := I.mul_mem_left y' h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Defs (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
this : y' * (y * x) ∈ I
⊢ x ∈ I
have rwa : ∀ (this : y' * y * x ∈ I), x ∈ I
Tactic: rwa [← mul_assoc, hy', one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Defs (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
this : y' * (y * x) ∈ I
rwa : ∀ (this : y' * y * x ∈ I), x ∈ I
⊢ x ∈ I
have rwa₁ : ∀ (this : 1 * x ∈ I), x ∈ I
Tactic: rwa [← mul_assoc, hy', one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Defs (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
this : y' * (y * x) ∈ I
rwa : ∀ (this : y' * y * x ∈ I), x ∈ I
rwa₁ : ∀ (this : 1 * x ∈ I), x ∈ I
⊢ x ∈ I
have rwa₂ : ∀ (this : x ∈ I), x ∈ I
Tactic: rwa [← mul_assoc, hy', one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Defs (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
a : α
m n : ℕ
ha : a ^ m ∈ I
h : m ≤ n
⊢ a ^ n ∈ I
have rw : a ^ (n - m) * a ^ m ∈ I
Tactic: rw [← Nat.add_sub_of_le h, add_comm, pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Defs (goal)
Goal:
α : Type u
a b : α
inst : CommSemiring α
I : Ideal α
hab : a ∣ b
ha : a ∈ I
⊢ b ∈ I
have obtain : ∀ (c : α), a * c ∈ I
Tactic: obtain ⟨c, rfl⟩ := hab
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Defs (goal)
Goal:
α : Type u
inst : Ring α
I : Ideal α
a b c d : α
inst_1 : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = (a - b) * c + b * (c - d)
have rw : a * c - b * d = a * c - b * c + (b * c - b * d)
Tactic: rw [sub_mul, mul_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Defs (goal)
Goal:
α : Type u
inst : Ring α
I : Ideal α
a b c d : α
inst_1 : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d ∈ I
have rw : (a - b) * c + b * (c - d) ∈ I
Tactic: rw [show a * c - b * d = (a - b) * c + b * (c - d) by rw [sub_mul, mul_sub]; abel]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hle : p ≤ q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have pos : ∀ (h : p = q), ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
Tactic: by_cases h : p = q
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hle : p ≤ q
pos : ∀ (h : p = q), ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have neg : ∀ (h : ¬p = q), ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
Tactic: by_cases h : p = q
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hle : p ≤ q
h : p = q
inst : p.IsPrime
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have inst₁ : Q.LiesOver p
Tactic: subst h
Cleared hypotheses: q, inst_6, inst_8, hle, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hle : p ≤ q
h : p = q
inst : p.IsPrime
inst₁ : Q.LiesOver p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have hle₁ : p ≤ p
Tactic: subst h
Cleared hypotheses: q, inst_6, inst_8, hle, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p : Ideal R
inst_4 : p.IsPrime
Q : Ideal S
inst_5 : Q.IsPrime
inst_6 : p.IsPrime
inst_7 : Q.LiesOver p
hle : p ≤ p
w : Ideal S
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have h : Q ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver p
Tactic: use Q
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hle : p ≤ q
h : ¬p = q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have this : q = under R Q
Tactic: have := Q.over_def q
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hle : p ≤ q
h : ¬p = q
this : q = under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have inst : IsPrime (under R Q)
Tactic: subst this
Cleared hypotheses: q, inst_5, inst_7, hle, h, this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hle : p ≤ q
h : ¬p = q
this : q = under R Q
inst : IsPrime (under R Q)
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have inst₁ : Q.LiesOver (under R Q)
Tactic: subst this
Cleared hypotheses: q, inst_6, inst_8, hle, h, this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hle : p ≤ q
h : ¬p = q
this : q = under R Q
inst : IsPrime (under R Q)
inst₁ : Q.LiesOver (under R Q)
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have hle₁ : p ≤ under R Q
Tactic: subst this
Cleared hypotheses: q, inst_6, inst_8, hle, h, this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hle : p ≤ q
h : ¬p = q
this : q = under R Q
inst : IsPrime (under R Q)
inst₁ : Q.LiesOver (under R Q)
hle₁ : p ≤ under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have h₁ : ¬p = under R Q
Tactic: subst this
Cleared hypotheses: q, inst_6, inst_8, hle, h, this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hpq : p < q
⊢ ∃ P < Q, P.IsPrime ∧ P.LiesOver p
have obtain : ∀ (P : Ideal S) (hPQ : P ≤ Q), P.IsPrime → P.LiesOver p → ∃ P < Q, P.IsPrime ∧ P.LiesOver p
Tactic: obtain ⟨P, hPQ, _, _⟩ := Q.exists_ideal_le_liesOver_of_le (p := p) (q := q) hpq.le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left : P.IsPrime
right : P.LiesOver p
⊢ ∃ P < Q, P.IsPrime ∧ P.LiesOver p
have refine : P < Q
Tactic: refine ⟨P, ?_, inferInstance, inferInstance⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left : P.IsPrime
right : P.LiesOver p
⊢ P < Q
have by_contra : ∀ (hc : ¬P < Q), False
Tactic: by_contra hc
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
p q : Ideal R
inst_4 : p.IsPrime
inst_5 : q.IsPrime
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : Q.LiesOver q
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left : P.IsPrime
right : P.LiesOver p
hc : ¬P < Q
⊢ False
have this : P = Q
Tactic: have : P = Q := eq_of_le_of_not_lt hPQ hc
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left : P.IsPrime
right : P.LiesOver p
hc : ¬P < Q
this : P = Q
inst : P.IsPrime
⊢ False
have inst₁ : P.LiesOver q
Tactic: subst this
Cleared hypotheses: Q, inst_7, inst_8, hPQ, hc, this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left : P.IsPrime
right : P.LiesOver p
hc : ¬P < Q
this : P = Q
inst : P.IsPrime
inst₁ : P.LiesOver q
⊢ False
have hPQ₁ : P ≤ P
Tactic: subst this
Cleared hypotheses: Q, inst_7, inst_8, hPQ, hc, this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra.HasGoingDown R S
p q : Ideal R
inst_5 : p.IsPrime
inst_6 : q.IsPrime
Q : Ideal S
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver q
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left : P.IsPrime
right : P.LiesOver p
hc : ¬P < Q
this : P = Q
inst : P.IsPrime
inst₁ : P.LiesOver q
hPQ₁ : P ≤ P
⊢ False
have hc₁ : ¬P < P
Tactic: subst this
Cleared hypotheses: Q, inst_7, inst_8, hPQ, hc, this