Theorem: obvious_iff (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
⊢ (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y ↔ RingConGen.Rel rel x y
Tactic:
constructor
State after:
case mp
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
⊢ (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y → RingConGen.Rel rel x y

case mpr
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
⊢ RingConGen.Rel rel x y → (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y

State before:
case mp
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
⊢ (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y → RingConGen.Rel rel x y

case mpr
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
⊢ RingConGen.Rel rel x y → (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
Tactic:
. intro h
  suffices ∀ x, Quot.mk (RingQuot.Rel rel) x = ((RingQuot.mkRingHom rel) x).toQuot by
    rw [← RingQuot.eqvGen_rel_eq, ← Quot.eq, this x, this y, h]
  intro x
  simp only [RingQuot.mkRingHom]
  rfl
State after:
case mpr
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
⊢ RingConGen.Rel rel x y → (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y

State before:
case mpr
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
⊢ RingConGen.Rel rel x y → (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
Tactic:
. intro h
  induction h with
  | of x y h => exact RingQuot.mkRingHom_rel h
  | refl x => exact rfl
  | symm _ k => exact k.symm
  | trans h h' k k' => rw [k, k']
  | add _ _ k k' => simp only [map_add, k, k']
  | mul _ _ k k' => simp only [map_mul, k, k']
State after:
no goals

State before:
case mp
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
⊢ (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y → RingConGen.Rel rel x y
Tactic:
intro h
State after:
case mp
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
h : (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
⊢ RingConGen.Rel rel x y

State before:
case mp
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
h : (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
⊢ RingConGen.Rel rel x y
Tactic:
suffices ∀ x, Quot.mk (RingQuot.Rel rel) x = ((RingQuot.mkRingHom rel) x).toQuot by
  rw [← RingQuot.eqvGen_rel_eq, ← Quot.eq, this x, this y, h]
State after:
case mp
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
h : (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
⊢ ∀ (x : A), Quot.mk (RingQuot.Rel rel) x = ((RingQuot.mkRingHom rel) x).toQuot

State before:
case mp
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
h : (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
⊢ ∀ (x : A), Quot.mk (RingQuot.Rel rel) x = ((RingQuot.mkRingHom rel) x).toQuot
Tactic:
intro x
State after:
case mp
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x✝ y : A
h : (RingQuot.mkRingHom rel) x✝ = (RingQuot.mkRingHom rel) y
x : A
⊢ Quot.mk (RingQuot.Rel rel) x = ((RingQuot.mkRingHom rel) x).toQuot

State before:
case mp
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x✝ y : A
h : (RingQuot.mkRingHom rel) x✝ = (RingQuot.mkRingHom rel) y
x : A
⊢ Quot.mk (RingQuot.Rel rel) x = ((RingQuot.mkRingHom rel) x).toQuot
Tactic:
simp only [RingQuot.mkRingHom]
State after:
case mp
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x✝ y : A
h : (RingQuot.mkRingHom rel) x✝ = (RingQuot.mkRingHom rel) y
x : A
⊢ Quot.mk (RingQuot.Rel rel) x =
    ({ toFun := fun x => { toQuot := Quot.mk (RingQuot.Rel rel) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        x).toQuot

State before:
case mp
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x✝ y : A
h : (RingQuot.mkRingHom rel) x✝ = (RingQuot.mkRingHom rel) y
x : A
⊢ Quot.mk (RingQuot.Rel rel) x =
    ({ toFun := fun x => { toQuot := Quot.mk (RingQuot.Rel rel) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        x).toQuot
Tactic:
rfl
State after:
no goals

State before:
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
h : (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
this : ∀ (x : A), Quot.mk (RingQuot.Rel rel) x = ((RingQuot.mkRingHom rel) x).toQuot
⊢ RingConGen.Rel rel x y
Tactic:
rw [← RingQuot.eqvGen_rel_eq, ← Quot.eq, this x, this y, h]
State after:
no goals

State before:
case mpr
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
⊢ RingConGen.Rel rel x y → (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
Tactic:
intro h
State after:
case mpr
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
h : RingConGen.Rel rel x y
⊢ (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y

State before:
case mpr
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y : A
h : RingConGen.Rel rel x y
⊢ (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
Tactic:
induction h with
| of x y h => exact RingQuot.mkRingHom_rel h
| refl x => exact rfl
| symm _ k => exact k.symm
| trans h h' k k' => rw [k, k']
| add _ _ k k' => simp only [map_add, k, k']
| mul _ _ k k' => simp only [map_mul, k, k']
State after:
no goals

State before:
case mpr.of
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x✝ y✝ x y : A
h : rel x y
⊢ (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
Tactic:
exact RingQuot.mkRingHom_rel h
State after:
no goals

State before:
case mpr.refl
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x✝ y x : A
⊢ (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) x
Tactic:
exact rfl
State after:
no goals

State before:
case mpr.symm
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y x✝ y✝ : A
a✝ : RingConGen.Rel rel x✝ y✝
k : (RingQuot.mkRingHom rel) x✝ = (RingQuot.mkRingHom rel) y✝
⊢ (RingQuot.mkRingHom rel) y✝ = (RingQuot.mkRingHom rel) x✝
Tactic:
exact k.symm
State after:
no goals

State before:
case mpr.trans
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y x✝ y✝ z✝ : A
h : RingConGen.Rel rel x✝ y✝
h' : RingConGen.Rel rel y✝ z✝
k : (RingQuot.mkRingHom rel) x✝ = (RingQuot.mkRingHom rel) y✝
k' : (RingQuot.mkRingHom rel) y✝ = (RingQuot.mkRingHom rel) z✝
⊢ (RingQuot.mkRingHom rel) x✝ = (RingQuot.mkRingHom rel) z✝
Tactic:
rw [k, k']
State after:
no goals

State before:
case mpr.add
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y w✝ x✝ y✝ z✝ : A
a✝¹ : RingConGen.Rel rel w✝ x✝
a✝ : RingConGen.Rel rel y✝ z✝
k : (RingQuot.mkRingHom rel) w✝ = (RingQuot.mkRingHom rel) x✝
k' : (RingQuot.mkRingHom rel) y✝ = (RingQuot.mkRingHom rel) z✝
⊢ (RingQuot.mkRingHom rel) (w✝ + y✝) = (RingQuot.mkRingHom rel) (x✝ + z✝)
Tactic:
simp only [map_add, k, k']
State after:
no goals

State before:
case mpr.mul
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
x y w✝ x✝ y✝ z✝ : A
a✝¹ : RingConGen.Rel rel w✝ x✝
a✝ : RingConGen.Rel rel y✝ z✝
k : (RingQuot.mkRingHom rel) w✝ = (RingQuot.mkRingHom rel) x✝
k' : (RingQuot.mkRingHom rel) y✝ = (RingQuot.mkRingHom rel) z✝
⊢ (RingQuot.mkRingHom rel) (w✝ * y✝) = (RingQuot.mkRingHom rel) (x✝ * z✝)
Tactic:
simp only [map_mul, k, k']
State after:
no goals