-- Mathlib/GroupTheory/PushoutI.lean
theorem base_injective (hφ : ∀ i, Function.Injective (φ i)) :
    Function.Injective (base φ)

Proof state:
case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
d : Transversal φ
⊢ Injective ⇑(base φ)

Tactic:
let _ := Classical.decEq ι

Result:
case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
d : Transversal φ
x✝ : DecidableEq ι := Classical.decEq ι
⊢ Injective ⇑(base φ)

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
hφ : ∀ (i : ι), Injective ⇑(φ i)
⊢ Injective ⇑(base φ)

Tactic:
rcases transversal_nonempty φ hφ with ⟨d⟩

Result:
case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
d : Transversal φ
⊢ Injective ⇑(base φ)

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
hφ : ∀ (i : ι), Injective ⇑(φ i)
d : Transversal φ
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : (i : ι) → DecidableEq (G i) := fun i => Classical.decEq (G i)
a₁✝ a₂✝ : H
h : ((fun x1 x2 => x1 • x2) ∘ ⇑(base φ)) a₁✝ = ((fun x1 x2 => x1 • x2) ∘ ⇑(base φ)) a₂✝
w : NormalWord d
⊢ a₁✝ • w = a₂✝ • w

Tactic:
simp_all [funext_iff, base_smul_eq_smul]

Result:
no goals

Proof state:
case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
d : Transversal φ
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : (i : ι) → DecidableEq (G i) := fun i => Classical.decEq (G i)
⊢ Injective ((fun x1 x2 => x1 • x2) ∘ ⇑(base φ))

Tactic:
intros _ _ h

Result:
case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
d : Transversal φ
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : (i : ι) → DecidableEq (G i) := fun i => Classical.decEq (G i)
a₁✝ a₂✝ : H
h : ((fun x1 x2 => x1 • x2) ∘ ⇑(base φ)) a₁✝ = ((fun x1 x2 => x1 • x2) ∘ ⇑(base φ)) a₂✝
⊢ a₁✝ = a₂✝

Proof state:
case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
d : Transversal φ
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : (i : ι) → DecidableEq (G i) := fun i => Classical.decEq (G i)
a₁✝ a₂✝ : H
h : ((fun x1 x2 => x1 • x2) ∘ ⇑(base φ)) a₁✝ = ((fun x1 x2 => x1 • x2) ∘ ⇑(base φ)) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
exact eq_of_smul_eq_smul (fun w : NormalWord d =>
  by simp_all [funext_iff, base_smul_eq_smul])

Result:
no goals

Proof state:
case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
d : Transversal φ
x✝ : DecidableEq ι := Classical.decEq ι
⊢ Injective ⇑(base φ)

Tactic:
let _ := fun i => Classical.decEq (G i)

Result:
case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
d : Transversal φ
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : (i : ι) → DecidableEq (G i) := fun i => Classical.decEq (G i)
⊢ Injective ⇑(base φ)