-- Mathlib/GroupTheory/PushoutI.lean
theorem rcons_injective {i : ι} : Function.Injective (rcons (d := d) i)

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
⊢ Injective (rcons i)

Tactic:
rintro ⟨⟨head₁, tail₁⟩, _⟩ ⟨⟨head₂, tail₂⟩, _⟩

Result:
case mk.mk.mk.mk
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
tail₂ : Word G
fstIdx_ne✝ : tail₂.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
⊢ rcons i { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹, normalized := normalized✝¹ } =
      rcons i { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝, normalized := normalized✝ } →
    { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹, normalized := normalized✝¹ } =
      { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝, normalized := normalized✝ }

Proof state:
case mk.mk.mk.mk
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
tail₂ : Word G
fstIdx_ne✝ : tail₂.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
⊢ ↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2 →
    tail₁ = tail₂ → (⋯.equiv head₁).1 = (⋯.equiv head₂).1 → head₁ = head₂ ∧ tail₁ = tail₂

Tactic:
intro h₁ h₂ h₃

Result:
case mk.mk.mk.mk
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
tail₂ : Word G
fstIdx_ne✝ : tail₂.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
h₁ : ↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2
h₂ : tail₁ = tail₂
h₃ : (⋯.equiv head₁).1 = (⋯.equiv head₂).1
⊢ head₁ = head₂ ∧ tail₁ = tail₂

Proof state:
case mk.mk.mk.mk
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
h₁ : ↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2
h₃ : (⋯.equiv head₁).1 = (⋯.equiv head₂).1
fstIdx_ne✝ : tail₁.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₁, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
⊢ head₁ = head₂ ∧ tail₁ = tail₁

Tactic:
rw [← equiv_fst_mul_equiv_snd (d.compl i) head₁,
    ← equiv_fst_mul_equiv_snd (d.compl i) head₂,
  h₁, h₃]

Result:
case mk.mk.mk.mk
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
h₁ : ↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2
h₃ : (⋯.equiv head₁).1 = (⋯.equiv head₂).1
fstIdx_ne✝ : tail₁.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₁, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
⊢ ↑(⋯.equiv head₂).1 * ↑(⋯.equiv head₂).2 = ↑(⋯.equiv head₂).1 * ↑(⋯.equiv head₂).2 ∧ tail₁ = tail₁

Proof state:
case mk.mk.mk.mk
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
tail₂ : Word G
fstIdx_ne✝ : tail₂.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
h₁ : ↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2
h₂ : tail₁ = tail₂
h₃ : (⋯.equiv head₁).1 = (⋯.equiv head₂).1
⊢ head₁ = head₂ ∧ tail₁ = tail₂

Tactic:
subst h₂

Result:
case mk.mk.mk.mk
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
h₁ : ↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2
h₃ : (⋯.equiv head₁).1 = (⋯.equiv head₂).1
fstIdx_ne✝ : tail₁.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₁, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
⊢ head₁ = head₂ ∧ tail₁ = tail₁

Proof state:
case mk.mk.mk.mk
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
h₁ : ↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2
h₃ : (⋯.equiv head₁).1 = (⋯.equiv head₂).1
fstIdx_ne✝ : tail₁.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₁, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
⊢ ↑(⋯.equiv head₂).1 * ↑(⋯.equiv head₂).2 = ↑(⋯.equiv head₂).1 * ↑(⋯.equiv head₂).2 ∧ tail₁ = tail₁

Tactic:
simp

Result:
no goals