mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
⊢ f₁ e = f₁ e * f₂ e

pp: R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
⊢ f₁ e * f₂ e = f₂ e

Tactic:
·

Goal state after:
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
⊢ f₁ e = f₁ e * f₂ e
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
⊢ f₁ e * f₂ e = f₂ e

Tactic:
·

Goal state after:
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
⊢ f₁ e * f₂ e = f₂ e
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: case map_one
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} := ⋯
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := ⋯
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i := ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
⊢ (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) 1 = 1

pp: case map_mul
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} := ⋯
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := ⋯
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i := ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
⊢ ∀ (x y : A i),
    (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) (x * y) =
      (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) x *
        (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) y

Tactic:
·

Goal state after:
case map_one
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} := ⋯
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := ⋯
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i := ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
⊢ (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) 1 = 1
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case map_one
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
⊢ (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) 1 = 1

pp: case map_mul
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
⊢ ∀ (x_1 y : f x),
    (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) (x_1 * y) =
      (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) x_1 *
        (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) y

Tactic:
·

Goal state after:
case map_one
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
⊢ (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) 1 = 1
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case map_mul
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
⊢ ∀ (x_1 y : f x),
    (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) (x_1 * y) =
      (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) x_1 *
        (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) y

Tactic:
·

Goal state after:
case map_mul
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
⊢ ∀ (x_1 y : f x),
    (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) (x_1 * y) =
      (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) x_1 *
        (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) y
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: case map_mul
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} := ⋯
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := ⋯
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i := ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
⊢ ∀ (x y : A i),
    (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) (x * y) =
      (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) x *
        (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) y

Tactic:
·

Goal state after:
case map_mul
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} := ⋯
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := ⋯
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i := ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
⊢ ∀ (x y : A i),
    (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) (x * y) =
      (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) x *
        (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) y
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case map_one
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
f₁' : f x →ₐ[R] B ⧸ J' := ⋯
⊢ (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) 1 = 1

pp: case map_mul
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
f₁' : f x →ₐ[R] B ⧸ J' := ⋯
⊢ ∀ (x_1 y : f x),
    (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) (x_1 * y) =
      (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) x_1 *
        (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) y

Tactic:
·

Goal state after:
case map_one
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
f₁' : f x →ₐ[R] B ⧸ J' := ⋯
⊢ (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) 1 = 1
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case map_mul
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
f₁' : f x →ₐ[R] B ⧸ J' := ⋯
⊢ ∀ (x_1 y : f x),
    (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) (x_1 * y) =
      (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) x_1 *
        (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) y

Tactic:
·

Goal state after:
case map_mul
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
f₁' : f x →ₐ[R] B ⧸ J' := ⋯
⊢ ∀ (x_1 y : f x),
    (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) (x_1 * y) =
      (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) x_1 *
        (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) y
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case intro.mpr.hI
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
f₁' : f x →ₐ[R] B ⧸ J' := ⋯
f₂' : f x →ₐ[R] B ⧸ J' := ⋯
⊢ Ideal.map (algebraMap B (B ⧸ J')) J ^ 2 = ⊥

pp: case intro.mpr.a
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
f₁' : f x →ₐ[R] B ⧸ J' := ⋯
f₂' : f x →ₐ[R] B ⧸ J' := ⋯
⊢ (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap B (B ⧸ J')) J)).comp f₁' =
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap B (B ⧸ J')) J)).comp f₂'

Tactic:
·

Goal state after:
case intro.mpr.hI
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
f₁' : f x →ₐ[R] B ⧸ J' := ⋯
f₂' : f x →ₐ[R] B ⧸ J' := ⋯
⊢ Ideal.map (algebraMap B (B ⧸ J')) J ^ 2 = ⊥
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case intro.mpr.a
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
f₁' : f x →ₐ[R] B ⧸ J' := ⋯
f₂' : f x →ₐ[R] B ⧸ J' := ⋯
⊢ (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap B (B ⧸ J')) J)).comp f₁' =
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap B (B ⧸ J')) J)).comp f₂'

Tactic:
·

Goal state after:
case intro.mpr.a
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
f₁' : f x →ₐ[R] B ⧸ J' := ⋯
f₂' : f x →ₐ[R] B ⧸ J' := ⋯
⊢ (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap B (B ⧸ J')) J)).comp f₁' =
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap B (B ⧸ J')) J)).comp f₂'
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := ⋯
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (Ideal.Quotient.mkₐ K I).comp (pb.liftEquiv.symm ⟨x + u * (aeval x) (minpoly K pb.gen), ?w⟩) = f

pp: case w
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (aeval (x + u * (aeval x) (minpoly K pb.gen))) (minpoly K pb.gen) = 0

Tactic:
·

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := ⋯
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (Ideal.Quotient.mkₐ K I).comp (pb.liftEquiv.symm ⟨x + u * (aeval x) (minpoly K pb.gen), ?w⟩) = f