-- Mathlib/Analysis/Analytic/Composition.lean
theorem sigma_composition_eq_iff (i j : Σ a : Composition n, Composition a.length) :
    i = j ↔ i.1.blocks = j.1.blocks ∧ i.2.blocks = j.2.blocks

Proof state:
case blocks
n : ℕ
a : Composition n
b : Composition a.length
a' : Composition n
b' : Composition a'.length
h : ⟨a, b⟩.fst.blocks = ⟨a', b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a', b'⟩.snd.blocks
⊢ a.blocks = a'.blocks

Tactic:
exact h

Result:
no goals

Proof state:
n : ℕ
a : Composition n
b b' : Composition a.length
h : ⟨a, b⟩.fst.blocks = ⟨a, b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a, b'⟩.snd.blocks
⊢ b = b'

Tactic:
ext1

Result:
case blocks
n : ℕ
a : Composition n
b b' : Composition a.length
h : ⟨a, b⟩.fst.blocks = ⟨a, b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a, b'⟩.snd.blocks
⊢ b.blocks = b'.blocks

Proof state:
n : ℕ
i : (a : Composition n) × Composition a.length
⊢ i.fst.blocks = i.fst.blocks ∧ i.snd.blocks = i.snd.blocks

Tactic:
exact ⟨rfl, rfl⟩

Result:
no goals

Proof state:
case mk.mk
n : ℕ
a : Composition n
b : Composition a.length
a' : Composition n
b' : Composition a'.length
⊢ ⟨a, b⟩.fst.blocks = ⟨a', b'⟩.fst.blocks ∧ ⟨a, b⟩.snd.blocks = ⟨a', b'⟩.snd.blocks → ⟨a, b⟩ = ⟨a', b'⟩

Tactic:
rintro ⟨h, h'⟩

Result:
case mk.mk.intro
n : ℕ
a : Composition n
b : Composition a.length
a' : Composition n
b' : Composition a'.length
h : ⟨a, b⟩.fst.blocks = ⟨a', b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a', b'⟩.snd.blocks
⊢ ⟨a, b⟩ = ⟨a', b'⟩

Proof state:
n : ℕ
i j : (a : Composition n) × Composition a.length
⊢ i = j ↔ i.fst.blocks = j.fst.blocks ∧ i.snd.blocks = j.snd.blocks

Tactic:
refine ⟨by rintro rfl; exact ⟨rfl, rfl⟩, ?_⟩

Result:
n : ℕ
i j : (a : Composition n) × Composition a.length
⊢ i.fst.blocks = j.fst.blocks ∧ i.snd.blocks = j.snd.blocks → i = j

Proof state:
case mk.mk.intro
n : ℕ
a : Composition n
b b' : Composition a.length
h : ⟨a, b⟩.fst.blocks = ⟨a, b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a, b'⟩.snd.blocks
⊢ ⟨a, b⟩ = ⟨a, b'⟩

Tactic:
obtain rfl : b = b' := by ext1; exact h'

Result:
case mk.mk.intro
n : ℕ
a : Composition n
b : Composition a.length
h : ⟨a, b⟩.fst.blocks = ⟨a, b⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a, b⟩.snd.blocks
⊢ ⟨a, b⟩ = ⟨a, b⟩

Proof state:
n : ℕ
i j : (a : Composition n) × Composition a.length
⊢ i = j → i.fst.blocks = j.fst.blocks ∧ i.snd.blocks = j.snd.blocks

Tactic:
rintro rfl

Result:
n : ℕ
i : (a : Composition n) × Composition a.length
⊢ i.fst.blocks = i.fst.blocks ∧ i.snd.blocks = i.snd.blocks

Proof state:
case mk.mk.intro
n : ℕ
a : Composition n
b : Composition a.length
a' : Composition n
b' : Composition a'.length
h : ⟨a, b⟩.fst.blocks = ⟨a', b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a', b'⟩.snd.blocks
⊢ ⟨a, b⟩ = ⟨a', b'⟩

Tactic:
obtain rfl : a = a' := by ext1; exact h

Result:
case mk.mk.intro
n : ℕ
a : Composition n
b b' : Composition a.length
h : ⟨a, b⟩.fst.blocks = ⟨a, b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a, b'⟩.snd.blocks
⊢ ⟨a, b⟩ = ⟨a, b'⟩

Proof state:
case mk.mk.intro
n : ℕ
a : Composition n
b : Composition a.length
h : ⟨a, b⟩.fst.blocks = ⟨a, b⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a, b⟩.snd.blocks
⊢ ⟨a, b⟩ = ⟨a, b⟩

Tactic:
rfl

Result:
no goals

Proof state:
case mk
n : ℕ
j : (a : Composition n) × Composition a.length
a : Composition n
b : Composition a.length
⊢ ⟨a, b⟩.fst.blocks = j.fst.blocks ∧ ⟨a, b⟩.snd.blocks = j.snd.blocks → ⟨a, b⟩ = j

Tactic:
rcases j with ⟨a', b'⟩

Result:
case mk.mk
n : ℕ
a : Composition n
b : Composition a.length
a' : Composition n
b' : Composition a'.length
⊢ ⟨a, b⟩.fst.blocks = ⟨a', b'⟩.fst.blocks ∧ ⟨a, b⟩.snd.blocks = ⟨a', b'⟩.snd.blocks → ⟨a, b⟩ = ⟨a', b'⟩

Proof state:
n : ℕ
a : Composition n
b : Composition a.length
a' : Composition n
b' : Composition a'.length
h : ⟨a, b⟩.fst.blocks = ⟨a', b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a', b'⟩.snd.blocks
⊢ a = a'

Tactic:
ext1

Result:
case blocks
n : ℕ
a : Composition n
b : Composition a.length
a' : Composition n
b' : Composition a'.length
h : ⟨a, b⟩.fst.blocks = ⟨a', b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a', b'⟩.snd.blocks
⊢ a.blocks = a'.blocks

Proof state:
n : ℕ
i j : (a : Composition n) × Composition a.length
⊢ i.fst.blocks = j.fst.blocks ∧ i.snd.blocks = j.snd.blocks → i = j

Tactic:
rcases i with ⟨a, b⟩

Result:
case mk
n : ℕ
j : (a : Composition n) × Composition a.length
a : Composition n
b : Composition a.length
⊢ ⟨a, b⟩.fst.blocks = j.fst.blocks ∧ ⟨a, b⟩.snd.blocks = j.snd.blocks → ⟨a, b⟩ = j

Proof state:
case blocks
n : ℕ
a : Composition n
b b' : Composition a.length
h : ⟨a, b⟩.fst.blocks = ⟨a, b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a, b'⟩.snd.blocks
⊢ b.blocks = b'.blocks

Tactic:
exact h'

Result:
no goals