-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem ext {c1 c2 : NumDenSameDeg 𝒜 x} (hdeg : c1.deg = c2.deg) (hnum : (c1.num : A) = c2.num)
    (hden : (c1.den : A) = c2.den) : c1 = c2

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
hdeg : c1.deg = c2.deg
hnum : ↑c1.num = ↑c2.num
hden : ↑c1.den = ↑c2.den
⊢ c1 = c2

Tactic:
rcases c1 with ⟨i1, ⟨n1, hn1⟩, ⟨d1, hd1⟩, h1⟩

Result:
case mk.mk.mk
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
c2 : NumDenSameDeg 𝒜 x
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : ↑⟨d1, hd1⟩ ∈ x
hdeg : { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.deg = c2.deg
hnum : ↑{ deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.num = ↑c2.num
hden : ↑{ deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.den = ↑c2.den
⊢ { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 } = c2

Proof state:
case mk.mk.mk.mk.mk.mk
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : ↑⟨d1, hd1⟩ ∈ x
hn2 : n1 ∈ 𝒜 i1
hd2 : d1 ∈ 𝒜 i1
h2 : ↑⟨d1, hd2⟩ ∈ x
⊢ { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 } =
    { deg := i1, num := ⟨n1, hn2⟩, den := ⟨d1, hd2⟩, den_mem := h2 }

Tactic:
congr

Result:
no goals

Proof state:
case mk.mk.mk.mk.mk.mk
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : ↑⟨d1, hd1⟩ ∈ x
i2 : ι
n2 : A
hn2 : n2 ∈ 𝒜 i2
d2 : A
hd2 : d2 ∈ 𝒜 i2
h2 : ↑⟨d2, hd2⟩ ∈ x
hdeg : i1 = i2
hnum : n1 = n2
hden : d1 = d2
⊢ { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 } =
    { deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }

Tactic:
subst hdeg hnum hden

Result:
case mk.mk.mk.mk.mk.mk
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : ↑⟨d1, hd1⟩ ∈ x
hn2 : n1 ∈ 𝒜 i1
hd2 : d1 ∈ 𝒜 i1
h2 : ↑⟨d1, hd2⟩ ∈ x
⊢ { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 } =
    { deg := i1, num := ⟨n1, hn2⟩, den := ⟨d1, hd2⟩, den_mem := h2 }

Proof state:
case mk.mk.mk.mk.mk.mk
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : ↑⟨d1, hd1⟩ ∈ x
i2 : ι
n2 : A
hn2 : n2 ∈ 𝒜 i2
d2 : A
hd2 : d2 ∈ 𝒜 i2
h2 : ↑⟨d2, hd2⟩ ∈ x
hdeg :
  { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.deg =
    { deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }.deg
hnum :
  ↑{ deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.num =
    ↑{ deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }.num
hden :
  ↑{ deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.den =
    ↑{ deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }.den
⊢ { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 } =
    { deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }

Tactic:
dsimp only [Subtype.coe_mk] at *

Result:
case mk.mk.mk.mk.mk.mk
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : ↑⟨d1, hd1⟩ ∈ x
i2 : ι
n2 : A
hn2 : n2 ∈ 𝒜 i2
d2 : A
hd2 : d2 ∈ 𝒜 i2
h2 : ↑⟨d2, hd2⟩ ∈ x
hdeg : i1 = i2
hnum : n1 = n2
hden : d1 = d2
⊢ { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 } =
    { deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }

Proof state:
case mk.mk.mk
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
c2 : NumDenSameDeg 𝒜 x
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : ↑⟨d1, hd1⟩ ∈ x
hdeg : { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.deg = c2.deg
hnum : ↑{ deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.num = ↑c2.num
hden : ↑{ deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.den = ↑c2.den
⊢ { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 } = c2

Tactic:
rcases c2 with ⟨i2, ⟨n2, hn2⟩, ⟨d2, hd2⟩, h2⟩

Result:
case mk.mk.mk.mk.mk.mk
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : ↑⟨d1, hd1⟩ ∈ x
i2 : ι
n2 : A
hn2 : n2 ∈ 𝒜 i2
d2 : A
hd2 : d2 ∈ 𝒜 i2
h2 : ↑⟨d2, hd2⟩ ∈ x
hdeg :
  { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.deg =
    { deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }.deg
hnum :
  ↑{ deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.num =
    ↑{ deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }.num
hden :
  ↑{ deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.den =
    ↑{ deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }.den
⊢ { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 } =
    { deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }