awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ Function.Bijective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
          Ideal.Quotient.mk (Ideal.span {1 - e i})) :
      (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})

Tactic:
⟨?_, he.1.surjective_pi⟩

Premises used: CompleteOrthogonalIdempotents.toOrthogonalIdempotents, OrthogonalIdempotents.surjective_pi, And.intro, Function.Bijective
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
refine :
  Function.Injective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
          Ideal.Quotient.mk (Ideal.span {1 - e i})) :
      (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
⊢ Function.Bijective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
          Ideal.Quotient.mk (Ideal.span {1 - e i})) :
      (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})

Tactic:
refine ⟨?_, he.1.surjective_pi⟩
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
rw :
  ∀ (a : R),
    Eq (α := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
        ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
                Ideal.Quotient.mk (Ideal.span {1 - e i}) :
              (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
            a :
          (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
        (0 : (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) →
      a = 0
⊢ Function.Injective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
          Ideal.Quotient.mk (Ideal.span {1 - e i})) :
      (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx :
  Eq (α := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
            Ideal.Quotient.mk (Ideal.span {1 - e i}) :
          (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
        x :
      (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    (0 : (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
⊢ ∀ (x_1 : I), 1 - e x_1 ∣ x

Tactic:
simp only [funext_iff, Pi.ringHom_apply, Pi.zero_apply, Ideal.Quotient.eq_zero_iff_mem,
    Ideal.mem_span_singleton] at hx

Premises used: funext_iff, Pi.zero_apply, Ideal.Quotient.eq_zero_iff_mem, Pi.ringHom_apply, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
this : ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
rw : (∏ i : I, (1 - e i)) * x = 0
rw₁ : 0 * x = 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ x = 0

Tactic:
rw [← this Finset.univ, he.prod_one_sub, zero_mul]

Premises used: Finset.univ, MulZeroClass.zero_mul, CompleteOrthogonalIdempotents.prod_one_sub
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
suffices : ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
⊢ x = 0

Tactic:
suffices ∀ s : Finset I, (∏ i ∈ s, (1 - e i)) * x = x by
    rw [← this Finset.univ, he.prod_one_sub, zero_mul]
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s : Finset I
⊢ (∏ i ∈ ∅, (1 - e i)) * x = x

Tactic:
simp
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
refine :
  ∀ (s : Finset I) (a : I) (s : Finset I), a ∉ s → (∏ i ∈ s, (1 - e i)) * x = x → (∏ i ∈ insert a s, (1 - e i)) * x = x
⊢ ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x

Tactic:
refine fun s ↦ Finset.induction_on s (by simp) ?_
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s_1 : Finset I
a : I
s : Finset I
has : a ∉ s
e' : (∏ i ∈ s, (1 - e i)) * x = x
this : (1 - e a) * x = x
⊢ (∏ i ∈ insert a s, (1 - e i)) * x = x

Tactic:
simp [has, mul_assoc, e', this]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s_1 : Finset I
a : I
s : Finset I
has : a ∉ s
e' : (∏ i ∈ s, (1 - e i)) * x = x
suffices : (1 - e a) * x = x
⊢ (∏ i ∈ insert a s, (1 - e i)) * x = x

Tactic:
suffices (1 - e a) * x = x by simp [has, mul_assoc, e', this]
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s_1 : Finset I
a : I
s : Finset I
has : a ∉ s
e' : (∏ i ∈ s, (1 - e i)) * x = x
obtain :
  ∀ (c : R) (hx : ∀ (x : I), 1 - e x ∣ (1 - e a) * c) (e' : (∏ i ∈ s, (1 - e i)) * ((1 - e a) * c) = (1 - e a) * c),
    (1 - e a) * ((1 - e a) * c) = (1 - e a) * c
⊢ (1 - e a) * x = x

Tactic:
obtain ⟨c, rfl⟩ := hx a

Premises used: rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
s_1 : Finset I
a : I
s : Finset I
has : a ∉ s
c : R
hx : ∀ (x : I), 1 - e x ∣ (1 - e a) * c
e' : (∏ i ∈ s, (1 - e i)) * ((1 - e a) * c) = (1 - e a) * c
rw : (1 - e a) * (1 - e a) * c = (1 - e a) * c
rw₁ rw₂ : (1 - e a) * c = (1 - e a) * c
⊢ (1 - e a) * ((1 - e a) * c) = (1 - e a) * c

Tactic:
rw [← mul_assoc, (he.idem a).one_sub.eq]

Premises used: IsIdempotentElem.one_sub, CompleteOrthogonalIdempotents.toOrthogonalIdempotents, mul_assoc, OrthogonalIdempotents.idem, IsIdempotentElem.eq
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
refine :
  Function.Injective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
          Ideal.Quotient.mk (Ideal.span {1 - e i})) :
      (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
refine₁ refine₂ :
  ∀ (x : R)
    (hx :
      Eq (α := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
        ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
                Ideal.Quotient.mk (Ideal.span {1 - e i}) :
              (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
            x :
          (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
        (0 : (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))),
    x = 0
refine₃ : ∀ (x : R) (hx : ∀ (x_1 : I), 1 - e x_1 ∣ x), x = 0
refine₄ : ∀ (x : R) (hx : ∀ (x_1 : I), 1 - e x_1 ∣ x) (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
refine₅ refine₆ :
  ∀ (x : R) (hx : ∀ (x_1 : I), 1 - e x_1 ∣ x) (s : Finset I) (a : I) (s : Finset I) (has : a ∉ s)
    (e' : (∏ i ∈ s, (1 - e i)) * x = x), (∏ i ∈ insert a s, (1 - e i)) * x = x
refine₇ :
  ∀ (x : R) (hx : ∀ (x_1 : I), 1 - e x_1 ∣ x) (s : Finset I) (a : I) (s : Finset I) (has : a ∉ s)
    (e' : (∏ i ∈ s, (1 - e i)) * x = x), (1 - e a) * x = x
refine₈ :
  ∀ (s : Finset I) (a : I) (s : Finset I) (has : a ∉ s) (c : R) (hx : ∀ (x : I), 1 - e x ∣ (1 - e a) * c)
    (e' : (∏ i ∈ s, (1 - e i)) * ((1 - e a) * c) = (1 - e a) * c), (1 - e a) * ((1 - e a) * c) = (1 - e a) * c
⊢ Function.Bijective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
          Ideal.Quotient.mk (Ideal.span {1 - e i})) :
      (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})

Tactic:
classical
  refine ⟨?_, he.1.surjective_pi⟩
  rw [injective_iff_map_eq_zero]
  intro x hx
  simp only [funext_iff, Pi.ringHom_apply, Pi.zero_apply, Ideal.Quotient.eq_zero_iff_mem,
    Ideal.mem_span_singleton] at hx
  suffices ∀ s : Finset I, (∏ i ∈ s, (1 - e i)) * x = x by
    rw [← this Finset.univ, he.prod_one_sub, zero_mul]
  refine fun s ↦ Finset.induction_on s (by simp) ?_
  intro a s has e'
  suffices (1 - e a) * x = x by simp [has, mul_assoc, e', this]
  obtain ⟨c, rfl⟩ := hx a
  rw [← mul_assoc, (he.idem a).one_sub.eq]

Premises used: mul_assoc, funext_iff, Pi.zero_apply, Ideal.Quotient.eq_zero_iff_mem, injective_iff_map_eq_zero, Pi.ringHom_apply, Ideal.mem_span_singleton, rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents.{u_1, u_3} (R := R) fun (x : I) ↦ 1 - e x
⊢ ∀ (x : I), 1 - (1 - e x) = e x

Tactic:
simp
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents.{u_1, u_3} (R := R) fun (x : I) ↦ 1 - e x
obtain :
  ∀ (e' : I → R)
    (h :
      Function.Bijective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i}))
        (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i})) fun (i : I) ↦
              Ideal.Quotient.mk (Ideal.span {e' i})) :
          (a : R) → (i : I) → R ⧸ Ideal.span {e' i}))
    (he : CompleteOrthogonalIdempotents.{u_1, u_3} (R := R) fun (x : I) ↦ 1 - e' x),
    Function.Bijective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i}))
      (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i})) fun (i : I) ↦
            Ideal.Quotient.mk (Ideal.span {e' i})) :
        (a : R) → (i : I) → R ⧸ Ideal.span {e' i})
⊢ Function.Bijective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e i}))
    (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e i})) fun (i : I) ↦
          Ideal.Quotient.mk (Ideal.span {e i})) :
      (a : R) → (i : I) → R ⧸ Ideal.span {e i})

Tactic:
obtain ⟨e', rfl, h⟩ : ∃ e' : I → R, (e' = e) ∧ Function.Bijective (Pi.ringHom fun i ↦
      Ideal.Quotient.mk (Ideal.span {e' i})) := ⟨_, funext (by simp), he.bijective_pi⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e' : I → R
h :
  Function.Bijective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i}))
    (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i})) fun (i : I) ↦
          Ideal.Quotient.mk (Ideal.span {e' i})) :
      (a : R) → (i : I) → R ⧸ Ideal.span {e' i})
he : CompleteOrthogonalIdempotents.{u_1, u_3} (R := R) fun (x : I) ↦ 1 - e' x
⊢ Function.Bijective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i}))
    (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i})) fun (i : I) ↦
          Ideal.Quotient.mk (Ideal.span {e' i})) :
      (a : R) → (i : I) → R ⧸ Ideal.span {e' i})

Tactic:
h
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e' : I → R
h :
  Function.Bijective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i}))
    (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i})) fun (i : I) ↦
          Ideal.Quotient.mk (Ideal.span {e' i})) :
      (a : R) → (i : I) → R ⧸ Ideal.span {e' i})
he : CompleteOrthogonalIdempotents.{u_1, u_3} (R := R) fun (x : I) ↦ 1 - e' x
⊢ Function.Bijective (α := R) (β := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i}))
    (⇑(Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e' i})) fun (i : I) ↦
          Ideal.Quotient.mk (Ideal.span {e' i})) :
      (a : R) → (i : I) → R ⧸ Ideal.span {e' i})

Tactic:
exact h
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Fintype I
e : I → R
he : ∀ (i : I), IsIdempotentElem (e i)
he₁ : ∀ (i j : I), i ≠ j → (1 - e i) * (1 - e j) = 0
he₂ : Eq.{u_1 + 1} (α := R) (∏ i : I, e i) 0
⊢ Eq.{u_1 + 1} (α := R) (∏ i : I, (1 - (1 - e i))) 0

Tactic:
simpa using he₂
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
change :
  Function.Bijective.{u_1 + 1, u_1 + 1} (α := R) (β :=
    HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o 0}) × HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o 1}))
    (Function.comp (β := (i : Fin 2) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i}))
      (⇑(piFinTwoEquiv fun (i : Fin 2) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i})) :
        (a : (i : Fin 2) → R ⧸ Ideal.span {o i}) → (R ⧸ Ideal.span {o 0}) × R ⧸ Ideal.span {o 1})
      (⇑(Pi.ringHom (f := fun (i : Fin 2) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i})) fun (i : Fin 2) ↦
            Ideal.Quotient.mk (Ideal.span {o i})) :
        (a : R) → (i : Fin 2) → R ⧸ Ideal.span {o i}))
⊢ Function.Bijective (α := R) (β :=
    HasQuotient.Quotient R (B := Ideal R) (Ideal.span {e}) × HasQuotient.Quotient R (B := Ideal R) (Ideal.span {f}))
    (⇑(RingHom.prod (Ideal.Quotient.mk (Ideal.span {e})) (Ideal.Quotient.mk (Ideal.span {f}))) :
      (a : R) → (R ⧸ Ideal.span {e}) × R ⧸ Ideal.span {f})

Tactic:
change Function.Bijective
    (piFinTwoEquiv _ ∘ Pi.ringHom (fun i : Fin 2 ↦ Ideal.Quotient.mk (Ideal.span {o i})))

Premises used: Ideal.Quotient.mk, Function.comp, Pi.ringHom, Function.Bijective, Ideal.span, Singleton.singleton, DFunLike.coe, piFinTwoEquiv
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
rw :
  Function.Bijective.{u_1 + 1, u_1 + 1} (α := R) (β :=
    (i : Fin 2) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i}))
    (⇑(Pi.ringHom (f := fun (i : Fin 2) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i})) fun (i : Fin 2) ↦
          Ideal.Quotient.mk (Ideal.span {o i})) :
      (a : R) → (i : Fin 2) → R ⧸ Ideal.span {o i})
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := R) (β :=
    HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o 0}) × HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o 1}))
    (Function.comp (β := (i : Fin 2) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i}))
      (⇑(piFinTwoEquiv fun (i : Fin 2) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i})) :
        (a : (i : Fin 2) → R ⧸ Ideal.span {o i}) → (R ⧸ Ideal.span {o 0}) × R ⧸ Ideal.span {o 1})
      (⇑(Pi.ringHom (f := fun (i : Fin 2) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i})) fun (i : Fin 2) ↦
            Ideal.Quotient.mk (Ideal.span {o i})) :
        (a : R) → (i : Fin 2) → R ⧸ Ideal.span {o i}))

Tactic:
rw [(Equiv.bijective _).of_comp_iff']

Premises used: Equiv.bijective, Function.Bijective.of_comp_iff'
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
he₁ : ∀ (i : Fin 2), IsIdempotentElem (o i)
he₂ : ∀ (i j : Fin 2), i ≠ j → (1 - o i) * (1 - o j) = 0
he₃ : Eq.{u_1 + 1} (α := R) (∏ i : Fin 2, o i) 0
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := R) (β :=
    (i : Fin 2) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i}))
    (⇑(Pi.ringHom (f := fun (i : Fin 2) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {o i})) fun (i : Fin 2) ↦
          Ideal.Quotient.mk (Ideal.span {o i})) :
      (a : R) → (i : Fin 2) → R ⧸ Ideal.span {o i})

Tactic:
apply pi_bijective_of_isIdempotentElem

Premises used: RingHom.pi_bijective_of_isIdempotentElem
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
i : Fin 2
he₁ : IsIdempotentElem (o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))
he₂ : IsIdempotentElem (o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))
⊢ IsIdempotentElem (o i)

Tactic:
fin_cases i
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
⊢ IsIdempotentElem (o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))

Tactic:
simpa [o]
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
⊢ IsIdempotentElem (o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))

Tactic:
simpa [o]
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
i j : Fin 2
hij : i ≠ j
he₁ : ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j), (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) * (1 - o j) = 0
he₂ : ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j), (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) * (1 - o j) = 0
⊢ (1 - o i) * (1 - o j) = 0

Tactic:
fin_cases i
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
j : Fin 2
hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j
he₁ :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) = 0
he₂ :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)),
    (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) = 0
⊢ (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) * (1 - o j) = 0

Tactic:
fin_cases j
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
j : Fin 2
hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j
he₁ :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) = 0
he₂ :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)),
    (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) = 0
⊢ (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) * (1 - o j) = 0

Tactic:
fin_cases j
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) = 0

Tactic:
simp at hij ⊢
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
he₁ : ∀ (hij : True), (1 - o 0) * (1 - o 1) = 0
⊢ (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) = 0

Tactic:
simp at hij ⊢
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
he₁ : ∀ (hij : True), (1 - o 1) * (1 - o 0) = 0
⊢ (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) = 0

Tactic:
simp at hij ⊢
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) * (1 - o ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) = 0

Tactic:
simp at hij ⊢
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
hij : True
⊢ (1 - o 0) * (1 - o 1) = 0

Tactic:
simp [o, mul_comm, hef₂, ← hef₁]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
hij : True
⊢ (1 - o 1) * (1 - o 0) = 0

Tactic:
simp [o, mul_comm, hef₂, ← hef₁]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
inst : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : (i : Fin 2) → R :=
  fun (i : Fin 2) ↦
    match (motive := Fin 2 → R) i with
    | 0 => e
    | 1 => f
⊢ Eq.{u_1 + 1} (α := R) (∏ i : Fin 2, o i) 0

Tactic:
simpa