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

Proof state:
case map_one
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) ⋯ ⋯
⊢ (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) 1 = 1

Tactic:
simp only [AlgHom.comp_toLinearMap, LinearMap.coe_comp, LinearMap.coe_single,
  Function.comp_apply, AlgHom.toLinearMap_apply, Ideal.Quotient.mkₐ_eq_mk]

Result:
case map_one
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) ⋯ ⋯
⊢ (Ideal.Quotient.mk J') (f₂ (Pi.single x 1)) = 1

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
⊢ ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J

Tactic:
intro g

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
g : (i : I) → f i
⊢ f₁ g - f₂ g ∈ J

Proof state:
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
H : ∀ (i : I), FormallyUnramified R (f i)
⊢ ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I_1 : Ideal B),
    I_1 ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I_1).comp

Tactic:
intros B _ _ J hJ f₁ f₂ e

Result:
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
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₂
⊢ f₁ = f₂

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
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
⊢ f₁ e = f₁ e * f₂ e

Tactic:
rw [← sub_eq_zero, ← h₁, mul_sub, mul_one]

Result:
no goals

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)) ^ 2 ∈ J ^ 2

Tactic:
apply Ideal.pow_mem_pow

Result:
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
⊢ f₁ e * (1 - f₂ e) ∈ J

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
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) ⋯ ⋯
this : f₁' = f₂'
c : B
hc : f₁ e * (f₁ (Pi.single x (g x)) - f₂ (Pi.single x (g x))) = f₁ e * ((1 - f₁ e) * c)
⊢ f₁ (Pi.single x (g x)) = f₂ (Pi.single x (g x))

Tactic:
rwa [← mul_assoc, mul_sub, mul_sub, mul_one, (he.map f₁).eq, sub_self, zero_mul,
  ← map_mul, H, ← map_mul, ← Pi.single_mul, one_mul, sub_eq_zero] at hc

Result:
no goals