-- Mathlib/RingTheory/Unramified/Pi.lean
theorem pi_iff :
    FormallyUnramified R (∀ i, f i) ↔ ∀ i, FormallyUnramified R (f i)

Proof state:
case intro.mpr.H
R : Type (max u v)
I : Type v
inst✝⁵ : Finite I
f : I → Type (max u v)
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 v)
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 := Pi.single x 1
he : IsIdempotentElem e
⊢ f₁ (Pi.single x (g x)) = f₂ (Pi.single x (g x))

Tactic:
have h₁ : (f₁ e) * (1 - f₂ e) = 0 := by
  rw [← Ideal.mem_bot, ← hJ, ← ((he.map f₁).mul (he.map f₂).one_sub).eq, ← pow_two]
  apply Ideal.pow_mem_pow
  convert Ideal.mul_mem_left _ (f₁ e) (hf e) using 1
  rw [mul_sub, mul_sub, mul_one, (he.map f₁).eq]

Result:
case intro.mpr.H
R : Type (max u v)
I : Type v
inst✝⁵ : Finite I
f : I → Type (max u v)
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 v)
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 := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
⊢ f₁ (Pi.single x (g x)) = f₂ (Pi.single x (g x))

Proof state:
case intro.mp
R : Type (max u v)
I : Type v
inst✝³ : Finite I
f : I → Type (max u v)
inst✝² : CommRing R
inst✝¹ : (i : I) → CommRing (f i)
inst✝ : (i : I) → Algebra R (f i)
val✝ : Fintype I
a✝ : FormallyUnramified R ((i : I) → f i)
i : I
⊢ FormallyUnramified R (f i)

Tactic:
exact FormallyUnramified.of_surjective (Pi.evalAlgHom R f i) (Function.surjective_eval i)

Result:
no goals

Proof state:
case intro.mpr.H.a.H
R : Type (max u v)
I : Type v
inst✝⁵ : Finite I
f : I → Type (max u v)
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 v)
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 := Pi.single x 1
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.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
f₂' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
r : f x
⊢ (Ideal.Quotient.mk J') (f₁ (Pi.single x r) - f₂ (Pi.single x r)) ∈ Ideal.map (Ideal.Quotient.mk J') J

Tactic:
exact Ideal.mem_map_of_mem (Ideal.Quotient.mk J') (hf (Pi.single x r))

Result:
no goals

Proof state:
case hx
R : Type (max u v)
I : Type v
inst✝⁵ : Finite I
f : I → Type (max u v)
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 v)
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 := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
⊢ f₂ e * (1 - f₁ e) ∈ J

Tactic:
convert Ideal.mul_mem_left _ (-f₂ e) (hf e) using 1

Result:
case h.e'_5
R : Type (max u v)
I : Type v
inst✝⁵ : Finite I
f : I → Type (max u v)
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 v)
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 := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
⊢ f₂ e * (1 - f₁ e) = -f₂ e * (f₁ e - f₂ e)

Proof state:
case intro
R : Type (max u v)
I : Type v
inst✝³ : Finite I
f : I → Type (max u v)
inst✝² : CommRing R
inst✝¹ : (i : I) → CommRing (f i)
inst✝ : (i : I) → Algebra R (f i)
val✝ : Fintype I
⊢ FormallyUnramified R ((i : I) → f i) ↔ ∀ (i : I), FormallyUnramified R (f i)

Tactic:
constructor

Result:
case intro.mp
R : Type (max u v)
I : Type v
inst✝³ : Finite I
f : I → Type (max u v)
inst✝² : CommRing R
inst✝¹ : (i : I) → CommRing (f i)
inst✝ : (i : I) → Algebra R (f i)
val✝ : Fintype I
⊢ FormallyUnramified R ((i : I) → f i) → ∀ (i : I), FormallyUnramified R (f i)

case intro.mpr
R : Type (max u v)
I : Type v
inst✝³ : Finite I
f : I → Type (max u v)
inst✝² : CommRing R
inst✝¹ : (i : I) → CommRing (f i)
inst✝ : (i : I) → Algebra R (f i)
val✝ : Fintype I
⊢ (∀ (i : I), FormallyUnramified R (f i)) → FormallyUnramified R ((i : I) → f i)

Proof state:
R : Type (max u v)
I : Type v
inst✝⁵ : Finite I
f : I → Type (max u v)
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 v)
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 := Pi.single x 1
he : IsIdempotentElem e
⊢ f₁ e * (1 - f₂ e) = 0

Tactic:
rw [← Ideal.mem_bot, ← hJ, ← ((he.map f₁).mul (he.map f₂).one_sub).eq, ← pow_two]

Result:
R : Type (max u v)
I : Type v
inst✝⁵ : Finite I
f : I → Type (max u v)
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 v)
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 := Pi.single x 1
he : IsIdempotentElem e
⊢ (f₁ e * (1 - f₂ e)) ^ 2 ∈ J ^ 2

Proof state:
case h.e'_5
R : Type (max u v)
I : Type v
inst✝⁵ : Finite I
f : I → Type (max u v)
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 v)
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 := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
⊢ f₂ e * (1 - f₁ e) = -f₂ e * (f₁ e - f₂ e)

Tactic:
rw [neg_mul, mul_sub, mul_sub, mul_one, neg_sub, (he.map f₂).eq]

Result:
no goals