mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
| Nat.card { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }

Tactic:
1,

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
| { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
| { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }

Tactic:
1,

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
| fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
⊢ ∀ [inst : CommRing B] [Small.{w, u} B] [inst_2 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type v
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
inst✝ : CommRing B
⊢ ∀ [Small.{w, u} B] [inst : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
inst✝ : CommRing B
⊢ ∀ [Small.{w, u} B] [inst : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
inst✝¹ : CommRing B
inst✝ : Small.{w, u} B
⊢ ∀ [inst : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
inst✝¹ : CommRing B
inst✝ : Small.{w, u} B
⊢ ∀ [inst : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
inst✝² : CommRing B
inst✝¹ : Small.{w, u} B
inst✝ : Algebra R B
⊢ ∀ (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case h₁
R : Type v
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : Algebra R A
B✝ : Type w
inst✝¹ : CommRing B✝
inst✝ : FormallyUnramified R A
I : Ideal B✝
hI : IsNilpotent I
B : Type w
⊢ ∀ [inst : CommRing B] (I : Ideal B),
    I ^ 2 = ⊥ → ∀ [inst_1 : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
case h₁
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type w
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I : Ideal B✝
hI : IsNilpotent I
B : Type w
inst✝ : CommRing B
⊢ ∀ (I : Ideal B), I ^ 2 = ⊥ → ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case h₁
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type w
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I✝ : Ideal B✝
hI✝ : IsNilpotent I✝
B : Type w
inst✝ : CommRing B
I : Ideal B
hI : I ^ 2 = ⊥
⊢ ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
case h₁
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type w
inst✝³ : CommRing B✝
inst✝² : FormallyUnramified R A
I✝ : Ideal B✝
hI✝ : IsNilpotent I✝
B : Type w
inst✝¹ : CommRing B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝ : Algebra R B
⊢ Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case h₂
R : Type v
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : Algebra R A
B✝ : Type w
inst✝¹ : CommRing B✝
inst✝ : FormallyUnramified R A
I : Ideal B✝
hI : IsNilpotent I
B : Type w
⊢ ∀ [inst : CommRing B] (I J : Ideal B),
    I ≤ J →
      (∀ [inst_1 : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst_1 : Algebra R (B ⧸ I)],
            Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst_1 : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R J).comp

Tactic:
_

Goal state after:
case h₂
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type w
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I : Ideal B✝
hI : IsNilpotent I
B : Type w
inst✝ : CommRing B
⊢ ∀ (I J : Ideal B),
    I ≤ J →
      (∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst : Algebra R (B ⧸ I)],
            Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R J).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case h₂
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type w
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type w
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
⊢ ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R J).comp

Tactic:
_

Goal state after:
case h₂
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type w
inst✝³ : CommRing B✝
inst✝² : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type w
inst✝¹ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
inst✝ : Algebra R B
⊢ Function.Injective (Ideal.Quotient.mkₐ R J).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
B : Type u
⊢ ∀ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type u
inst✝¹ : CommRing R
B : Type u
inst✝ : CommRing B
⊢ ∀ [inst : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
B : Type u
inst✝ : CommRing B
⊢ ∀ [inst : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type u
inst✝² : CommRing R
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
⊢ ∀ (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
⊢ ∀ (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type u
inst✝² : CommRing R
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I✝ : Ideal B
⊢ I✝ ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I✝).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I✝ : Ideal B
⊢ I✝ ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I✝).comp

Tactic:
_

Goal state after:
R : Type u
inst✝² : CommRing R
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I✝ : Ideal B
x✝ : I✝ ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ R I✝).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I✝ : Ideal B
x✝ : I✝ ^ 2 = ⊥
f₁ f₂ : R →ₐ[R] B
⊢ (Ideal.Quotient.mkₐ R I✝).comp f₁ = (Ideal.Quotient.mkₐ R I✝).comp f₂ → f₁ = f₂

Tactic:
_

Goal state after:
R : Type u
inst✝² : CommRing R
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I✝ : Ideal B
x✝ : I✝ ^ 2 = ⊥
f₁ f₂ : R →ₐ[R] B
a✝ : (Ideal.Quotient.mkₐ R I✝).comp f₁ = (Ideal.Quotient.mkₐ R I✝).comp f₂
⊢ f₁ = f₂
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
⊢ ∀ [inst : CommRing C] [inst_1 : Algebra R C] (I : Ideal C),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst✝ : CommRing C
⊢ ∀ [inst : Algebra R C] (I : Ideal C), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst✝ : CommRing C
⊢ ∀ [inst : Algebra R C] (I : Ideal C), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
⊢ ∀ (I : Ideal C), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
A : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallyUnramified R A
inst✝ : FormallyUnramified A B
C : Type u_3
⊢ ∀ [inst : CommRing C] [inst_1 : Algebra R C] (I : Ideal C),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R A
inst✝¹ : FormallyUnramified A B
C : Type u_3
inst✝ : CommRing C
⊢ ∀ [inst : Algebra R C] (I : Ideal C), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R A
inst✝¹ : FormallyUnramified A B
C : Type u_3
inst✝ : CommRing C
⊢ ∀ [inst : Algebra R C] (I : Ideal C), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
A : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
B : Type u_3
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
⊢ ∀ (I : Ideal C), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_3
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : FormallyUnramified R B
Q : Type u_3
⊢ ∀ [inst : CommRing Q] [inst_1 : Algebra A Q] (I : Ideal Q),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ A I).comp

Tactic:
_

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
A : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallyUnramified R B
Q : Type u_3
inst✝ : CommRing Q
⊢ ∀ [inst : Algebra A Q] (I : Ideal Q), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ A I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
A : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallyUnramified R B
Q : Type u_3
inst✝ : CommRing Q
⊢ ∀ [inst : Algebra A Q] (I : Ideal Q), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ A I).comp

Tactic:
_

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
⊢ ∀ (I : Ideal Q), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ A I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
⊢ ∀ [inst : CommRing Q] [inst_1 : Algebra R Q] (I : Ideal Q),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝ : CommRing Q
⊢ ∀ [inst : Algebra R Q] (I : Ideal Q), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝ : CommRing Q
⊢ ∀ [inst : Algebra R Q] (I : Ideal Q), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
⊢ ∀ (I : Ideal Q), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
C : Type (max u_2 u_3)
⊢ ∀ [inst : CommRing C] [inst_1 : Algebra B C] (I : Ideal C),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ B I).comp

Tactic:
_

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : FormallyUnramified R A
C : Type (max u_2 u_3)
inst✝ : CommRing C
⊢ ∀ [inst : Algebra B C] (I : Ideal C), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ B I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : FormallyUnramified R A
C : Type (max u_2 u_3)
inst✝ : CommRing C
⊢ ∀ [inst : Algebra B C] (I : Ideal C), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ B I).comp

Tactic:
_

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_3
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
C : Type (max u_2 u_3)
inst✝¹ : CommRing C
inst✝ : Algebra B C
⊢ ∀ (I : Ideal C), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ B I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
Rₘ : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
Q : Type u_3
⊢ ∀ [inst : CommRing Q] [inst_1 : Algebra R Q] (I : Ideal Q),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type u_1
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing Rₘ
M : Submonoid R
inst✝² : Algebra R Rₘ
inst✝¹ : IsLocalization M Rₘ
Q : Type u_3
inst✝ : CommRing Q
⊢ ∀ [inst : Algebra R Q] (I : Ideal Q), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing Rₘ
M : Submonoid R
inst✝² : Algebra R Rₘ
inst✝¹ : IsLocalization M Rₘ
Q : Type u_3
inst✝ : CommRing Q
⊢ ∀ [inst : Algebra R Q] (I : Ideal Q), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
⊢ ∀ (I : Ideal Q), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
⊢ I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
_

Goal state after:
R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
⊢ (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂ → f₁ = f₂

Tactic:
_

Goal state after:
R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
a✝ : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ f₁ = f₂
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
b' : Basis I S (S ⊗[R] S) := ((Basis.singleton PUnit.{1} S).tensorProduct b).reindex (Equiv.punitProd I)
⊢ ((b'.repr (elem R S)).sum fun i a ↦ a • b' i) = (b'.repr (elem R S)).sum fun i x ↦ x ⊗ₜ[R] b i

Tactic:
congr! with _ i x

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
b' : Basis I S (S ⊗[R] S) := ((Basis.singleton PUnit.{1} S).tensorProduct b).reindex (Equiv.punitProd I)
x✝ : I
i : S
⊢ i • b' x✝ = i ⊗ₜ[R] b x✝
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i ↦ (a i).support) (fun j ↦ b.repr (f.sum fun i y ↦ (a i) j • y)) ⋯
this : ∀ (i : I), ((b.repr (x * f i)).sum fun j k ↦ k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i
⊢ ∑ x_1 ∈ f.support, (x * f x_1) ⊗ₜ[R] b x_1 = ∑ i ∈ f.support, x ⊗ₜ[R] 1 * f i ⊗ₜ[R] b i

Tactic:
TensorProduct.tmul_mul_tmul,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i ↦ (a i).support) (fun j ↦ b.repr (f.sum fun i y ↦ (a i) j • y)) ⋯
this : ∀ (i : I), ((b.repr (x * f i)).sum fun j k ↦ k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i
⊢ ∑ x_1 ∈ f.support, (x * f x_1) ⊗ₜ[R] b x_1 = ∑ i ∈ f.support, (x * f i) ⊗ₜ[R] (1 * b i)