-- Mathlib/Algebra/FreeMonoid/Basic.lean
theorem map_surjective {f : α → β} : Function.Surjective (map f) ↔ Function.Surjective f

Proof state:
case mpr.mul_of
α : Type u_1
β : Type u_2
f : α → β
head : β
tail : FreeMonoid β
ih : ∃ a, (map f) a = tail
fs : ∃ a, f a = head
⊢ ∃ a, (map f) a = of head * tail

Tactic:
rcases fs with ⟨a, rfl⟩

Result:
case mpr.mul_of.intro
α : Type u_1
β : Type u_2
f : α → β
tail : FreeMonoid β
ih : ∃ a, (map f) a = tail
a : α
⊢ ∃ a_1, (map f) a_1 = of (f a) * tail

Proof state:
case mpr.mul_of
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
head : β
tail : FreeMonoid β
ih : ∃ a, (map f) a = tail
⊢ ∃ a, (map f) a = of head * tail

Tactic:
specialize fs head

Result:
case mpr.mul_of
α : Type u_1
β : Type u_2
f : α → β
head : β
tail : FreeMonoid β
ih : ∃ a, (map f) a = tail
fs : ∃ a, f a = head
⊢ ∃ a, (map f) a = of head * tail

Proof state:
case mp.intro.mul_of
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : (map f) (of head * a✝¹) = of d
⊢ ∃ a, f a = d

Tactic:
simp only [map_mul, map_of] at hb

Result:
case mp.intro.mul_of
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
⊢ ∃ a, f a = d

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
⊢ (map f) 1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
⊢ ∃ a, f a = d

Tactic:
rcases fs (FreeMonoid.of d) with ⟨b, hb⟩

Result:
case mp.intro
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
b : FreeMonoid α
hb : (map f) b = of d
⊢ ∃ a, f a = d

Proof state:
case mpr.one
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
⊢ ∃ a, (map f) a = 1

Tactic:
use 1

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
⊢ (map f) 1 = 1

Proof state:
case mpr.mul_of.intro
α : Type u_1
β : Type u_2
f : α → β
tail : FreeMonoid β
ih : ∃ a, (map f) a = tail
a : α
⊢ ∃ a_1, (map f) a_1 = of (f a) * tail

Tactic:
rcases ih with ⟨b, rfl⟩

Result:
case mpr.mul_of.intro.intro
α : Type u_1
β : Type u_2
f : α → β
a : α
b : FreeMonoid α
⊢ ∃ a_1, (map f) a_1 = of (f a) * (map f) b

Proof state:
case mp.intro.mul_of
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
⊢ ∃ a, f a = d

Tactic:
use head

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
⊢ f head = d

Proof state:
case mp
α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective ⇑(map f) → Function.Surjective f

Tactic:
intro fs d

Result:
case mp
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
⊢ ∃ a, f a = d

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) = of d
H : (map f) a✝¹ = 1
⊢ f head = d

Tactic:
exact FreeMonoid.of_injective hb

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
d : FreeMonoid β
⊢ ∃ a, (map f) a = d

Tactic:
induction' d using FreeMonoid.inductionOn' with head tail ih

Result:
case mpr.one
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
⊢ ∃ a, (map f) a = 1

case mpr.mul_of
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
head : β
tail : FreeMonoid β
ih : ∃ a, (map f) a = tail
⊢ ∃ a, (map f) a = of head * tail

Proof state:
case mp.intro.one
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
hb : (map f) 1 = of d
⊢ ∃ a, f a = d

Tactic:
have H := congr_arg length hb

Result:
case mp.intro.one
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
hb : (map f) 1 = of d
H : ((map f) 1).length = (of d).length
⊢ ∃ a, f a = d

Proof state:
case mp.intro.one
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
hb : (map f) 1 = of d
H : ((map f) 1).length = (of d).length
⊢ ∃ a, f a = d

Tactic:
simp only [length_one, length_of, Nat.zero_ne_one, map_one] at H

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
H : (map f) a✝¹ = 1
⊢ f head = d

Tactic:
rw [H, mul_one] at hb

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) = of d
H : (map f) a✝¹ = 1
⊢ f head = d

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
⊢ f head = d

Tactic:
have H := congr_arg length hb

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
H : (of (f head) * (map f) a✝¹).length = (of d).length
⊢ f head = d

Proof state:
case mpr.mul_of.intro.intro
α : Type u_1
β : Type u_2
f : α → β
a : α
b : FreeMonoid α
⊢ ∃ a_1, (map f) a_1 = of (f a) * (map f) b

Tactic:
use FreeMonoid.of a * b

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
a : α
b : FreeMonoid α
⊢ (map f) (of a * b) = of (f a) * (map f) b

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective ⇑(map f) ↔ Function.Surjective f

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective ⇑(map f) → Function.Surjective f

case mpr
α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective f → Function.Surjective ⇑(map f)

Proof state:
case mpr
α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective f → Function.Surjective ⇑(map f)

Tactic:
intro fs d

Result:
case mpr
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
d : FreeMonoid β
⊢ ∃ a, (map f) a = d

Proof state:
case mp.intro
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
b : FreeMonoid α
hb : (map f) b = of d
⊢ ∃ a, f a = d

Tactic:
induction' b using FreeMonoid.inductionOn' with head _ _

Result:
case mp.intro.one
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
hb : (map f) 1 = of d
⊢ ∃ a, f a = d

case mp.intro.mul_of
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : (map f) (of head * a✝¹) = of d
⊢ ∃ a, f a = d

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
a : α
b : FreeMonoid α
⊢ (map f) (of a * b) = of (f a) * (map f) b

Tactic:
rfl

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
H : (of (f head) * (map f) a✝¹).length = (of d).length
⊢ f head = d

Tactic:
simp only [length_mul, length_of, add_right_eq_self, length_eq_zero] at H

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
H : (map f) a✝¹ = 1
⊢ f head = d