awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Function.Defs
Goal:
α : Type u₁
f : α → α
⊢ (∀ (x : α), IsFixedPt f x) ↔ f = id

Tactic:
⟨funext, fun h ↦ h ▸ isFixedPt_id⟩

Premises used: Eq.rec, Function.isFixedPt_id, funext, Iff.intro, Eq.symm
-- Module: Mathlib.Logic.Function.Defs
Goal:
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
a : (i : ι) → α i
i : ι
⊢ Pi.map (α := α) (β := β) f a i = f i (a i)

Tactic:
rfl

Premises used: Pi.map, rfl
-- Module: Mathlib.Logic.Function.DependsOn
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s : Set ι
⊢ (∀ ⦃x y : (i : ι) → α i⦄, (∀ i ∈ s, x i = y i) → f x = f y) ↔
    ∀ ⦃a b : (i : ι) → α i⦄, s.restrict (π := α) a = s.restrict (π := α) b → f a = f b

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Logic.Function.DependsOn
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst : Nonempty β
f : ((i : ι) → α i) → β
s : Set ι
rw :
  FactorsThrough f (s.restrict (π := α)) ↔ ∃ (g : ((i : (↑s : Type u_1)) → α (↑i : ι)) → β), f = g ∘ s.restrict (π := α)
rw₁ rw₂ :
  (∃ (e : ((a : (↑s : Type u_1)) → α (↑a : ι)) → β), f = e ∘ s.restrict (π := α)) ↔
    ∃ (g : ((i : (↑s : Type u_1)) → α (↑i : ι)) → β), f = g ∘ s.restrict (π := α)
⊢ DependsOn (α := α) f s ↔ ∃ (g : ((i : (↑s : Type u_1)) → α (↑i : ι)) → β), f = g ∘ s.restrict (π := α)

Tactic:
rw [dependsOn_iff_factorsThrough, factorsThrough_iff]

Premises used: Function.factorsThrough_iff, dependsOn_iff_factorsThrough
-- Module: Mathlib.Logic.Function.DependsOn
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
⊢ DependsOn (α := α) f univ

Tactic:
fun _ _ h ↦ congrArg _ <| funext fun i ↦ h i trivial

Premises used: trivial, congrArg, DependsOn, funext
-- Module: Mathlib.Logic.Function.DependsOn
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
b : β
⊢ DependsOn.{u_1, u_2, u_3} (α := α) (β := β) (fun (x : (i : ι) → α i) ↦ b) ∅

Tactic:
simp [DependsOn]

Premises used: DependsOn
-- Module: Mathlib.Logic.Function.DependsOn
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s t : Set ι
hst : s ⊆ t
hf : DependsOn (α := α) f s
⊢ DependsOn (α := α) f t

Tactic:
fun _ _ h ↦ hf fun i hi ↦ h i (hst hi)

Premises used: DependsOn
-- Module: Mathlib.Logic.Function.DependsOn
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
hf : DependsOn (α := α) f ∅
x y : (i : ι) → α i
⊢ ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → x i = y i

Tactic:
simp
-- Module: Mathlib.Logic.Function.DependsOn
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
⊢ DependsOn (α := α) (s.restrict (π := α)) s

Tactic:
fun _ _ h ↦ funext fun i ↦ h i.1 i.2

Premises used: DependsOn, funext, Subtype.val, Subtype.property
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
⊢ (↑a : Set Y) = f ⁻¹' {image f a}

Tactic:
a.2.choose_spec.symm

Premises used: Exists.choose_spec, Function.Fiber.image, Eq.symm, Subtype.property
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : Y → Z
y : Y
⊢ Membership.mem (γ := Set (Set Y)) (Set.range fun (x : (↑(Set.range f) : Type u_3)) ↦ f ⁻¹' {(↑x : Z)}) (f ⁻¹' {f y})

Tactic:
simp
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
x : (↑(↑a : Set Y) : Type u_2)
⊢ (fun (x : (↑(Set.range f) : Type u_3)) ↦ f ⁻¹' {(↑x : Z)})
      (Exists.choose (p := fun (y : (↑(Set.range f) : Type u_3)) ↦
        (fun (x : (↑(Set.range f) : Type u_3)) ↦ f ⁻¹' {(↑x : Z)}) y = (↑a : Set Y)) ⋯) =
    (↑a : Set Y)

Tactic:
have := a.2.choose_spec
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
x : (↑(↑a : Set Y) : Type u_2)
this :
  (fun (x : (↑(Set.range f) : Type u_3)) ↦ f ⁻¹' {(↑x : Z)})
      (Exists.choose (p := fun (y : (↑(Set.range f) : Type u_3)) ↦
        (fun (x : (↑(Set.range f) : Type u_3)) ↦ f ⁻¹' {(↑x : Z)}) y = (↑a : Set Y)) ⋯) =
    (↑a : Set Y)
⊢ (↑x : Y) ∈ (↑a : Set Y)

Tactic:
x.prop

Premises used: Subtype.prop
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
x : (↑(↑a : Set Y) : Type u_2)
this :
  (fun (x : (↑(Set.range f) : Type u_3)) ↦ f ⁻¹' {(↑x : Z)})
      (Exists.choose (p := fun (y : (↑(Set.range f) : Type u_3)) ↦
        (fun (x : (↑(Set.range f) : Type u_3)) ↦ f ⁻¹' {(↑x : Z)}) y = (↑a : Set Y)) ⋯) =
    (↑a : Set Y)
⊢ (↑x : Y) ∈ f ⁻¹' {image f a}

Tactic:
convert! x.prop

Premises used: Subtype.prop
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
y : Y
⊢ image f (mk f y) = f y

Tactic:
(map_eq_image (x := mkSelf f y)).symm

Premises used: Function.Fiber.map_eq_image, Function.Fiber.mkSelf, Eq.symm
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
y : Y
a : Fiber f
h : f y = image f a
rw : y ∈ f ⁻¹' {image f a}
⊢ y ∈ (↑a : Set Y)

Tactic:
rw [a.eq_fiber_image]

Premises used: Function.Fiber.eq_fiber_image
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
y : Y
a : Fiber f
h : f y = image f a
⊢ y ∈ f ⁻¹' {image f a}

Tactic:
h

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
y : Y
a : Fiber f
h : f y = image f a
⊢ y ∈ f ⁻¹' {image f a}

Tactic:
exact h
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
⊢ f (preimage f a) = image f a

Tactic:
a.2.choose.2.choose_spec

Premises used: Exists.choose_spec, Function.Fiber.preimage, Function.Fiber.image, Exists.choose, Subtype.property
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
⊢ (↑a : Set Y).Nonempty

Tactic:
⟨preimage f a, ?_⟩

Premises used: Function.Fiber.preimage, Set.Nonempty, Exists.intro
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
refine : preimage f a ∈ (↑a : Set Y)
⊢ (↑a : Set Y).Nonempty

Tactic:
refine ⟨preimage f a, ?_⟩
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
rw : f (preimage f a) = image f a
rw₁ rw₂ : f (preimage f a) = f (preimage f a)
⊢ preimage f a ∈ (↑a : Set Y)

Tactic:
rw [mem_iff_eq_image, ← map_preimage_eq_image]

Premises used: Function.Fiber.mem_iff_eq_image, Function.Fiber.map_preimage_eq_image
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
Y : Type u_2
Z : Type u_3
W : Type u_4
f : Y → Z
g : Z → W
a : Fiber (g ∘ f)
rw : g (f (preimage (g ∘ f) a)) = (g ∘ f) (preimage (g ∘ f) a)
rw₁ rw₂ : g (f (preimage (g ∘ f) a)) = g (f (preimage (g ∘ f) a))
⊢ g (f (preimage (g ∘ f) a)) = image (g ∘ f) a

Tactic:
rw [← map_preimage_eq_image, comp_apply]

Premises used: Function.comp_apply, Function.Fiber.map_preimage_eq_image
-- Module: Mathlib.Logic.Function.FiberPartition
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : Y → Z
g : X → Y
a : Fiber (f ∘ g)
rw : f (g (preimage (f ∘ g) a)) = image f (mk f (g (preimage (f ∘ g) a)))
rw₁ rw₂ : f (g (preimage (f ∘ g) a)) = f (g (preimage (f ∘ g) a))
⊢ image (f ∘ g) a = image f (mk f (g (preimage (f ∘ g) a)))

Tactic:
rw [← map_preimage_eq_image_map _ _ a, mk_image]

Premises used: Function.Fiber.map_preimage_eq_image_map, Function.Fiber.mk_image
-- Module: Mathlib.Logic.Function.FromTypes
Goal:
p : Fin 0 → Type u
τ : Type u
⊢ FromTypes p τ = τ

Tactic:
rfl

Premises used: Function.FromTypes, rfl
-- Module: Mathlib.Logic.Function.FromTypes
Goal:
τ : Type u
⊢ FromTypes ![] τ = τ

Tactic:
fromTypes_zero ![] τ

Premises used: Function.fromTypes_zero, Matrix.vecEmpty
-- Module: Mathlib.Logic.Function.FromTypes
Goal:
n : ℕ
p : Fin (n + 1) → Type u
τ : Type u
⊢ FromTypes p τ = (vecHead p → FromTypes (vecTail p) τ)

Tactic:
rfl

Premises used: Function.FromTypes, rfl
-- Module: Mathlib.Logic.Function.FromTypes
Goal:
n : ℕ
α : Type u
p : Fin n → Type u
τ : Type u
⊢ FromTypes (vecCons α p) τ = (α → FromTypes p τ)

Tactic:
fromTypes_succ _ τ

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Matrix.vecHead, Fin.cases, Matrix.vecTail, Matrix.vecCons, Function.fromTypes_succ
-- Module: Mathlib.Logic.Function.FromTypes
Goal:
p : Fin 0 → Type u
τ : Type u
t : τ
⊢ const p t = t

Tactic:
rfl

Premises used: Function.FromTypes.const, rfl
-- Module: Mathlib.Logic.Function.FromTypes
Goal:
n : ℕ
p : Fin (n + 1) → Type u
τ : Type u
t : τ
⊢ const p t = fun (x : vecHead p) ↦ const (vecTail p) t

Tactic:
rfl

Premises used: Function.FromTypes.const, rfl
-- Module: Mathlib.Logic.Function.FromTypes
Goal:
n : ℕ
p : Fin (n + 1) → Type u
τ : Type u
t : τ
x : p 0
⊢ const p t x = const (vecTail p) t

Tactic:
rfl

Premises used: Function.FromTypes.const, rfl
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
⊢ f^[0] = id

Tactic:
rfl

Premises used: Nat.iterate, rfl
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
x : α
⊢ f^[0] x = x

Tactic:
rfl

Premises used: Nat.iterate, rfl
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
n : ℕ
⊢ f^[n.succ] = f^[n] ∘ f

Tactic:
rfl

Premises used: Nat.iterate, rfl
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
n : ℕ
x : α
⊢ f^[n.succ] x = f^[n] (f x)

Tactic:
rfl

Premises used: Nat.iterate, rfl
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
n_1 n : ℕ
ihn : Eq.{u + 1} (α := α → α) id^[n] id
rw : Eq.{u + 1} (α := α → α) (id^[n] ∘ id) id
rw₁ : Eq.{u + 1} (α := α → α) (id ∘ id) id
rw₂ rw₃ : Eq.{u + 1} (α := α → α) id id
⊢ Eq.{u + 1} (α := α → α) id^[n.succ] id

Tactic:
rw [iterate_succ, ihn, id_comp]

Premises used: Function.iterate_succ, Function.id_comp
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m n : ℕ
rw : (f^[m] ∘ f^[n]) ∘ f = f^[m] ∘ f^[n] ∘ f
⊢ f^[m + n.succ] = f^[m] ∘ f^[n.succ]

Tactic:
rw [Nat.add_succ, iterate_succ, iterate_succ, iterate_add m n]

Premises used: Function.iterate_succ, Nat.add_succ
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m n : ℕ
⊢ (f^[m] ∘ f^[n]) ∘ f = f^[m] ∘ f^[n] ∘ f

Tactic:
rfl
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m n : ℕ
x : α
rw : (f^[m] ∘ f^[n]) x = f^[m] (f^[n] x)
⊢ f^[m + n] x = f^[m] (f^[n] x)

Tactic:
rw [iterate_add f m n]

Premises used: Function.iterate_add
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m n : ℕ
x : α
⊢ (f^[m] ∘ f^[n]) x = f^[m] (f^[n] x)

Tactic:
rfl
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
⊢ f^[1] = f

Tactic:
funext fun _ ↦ rfl

Premises used: funext, rfl
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m : ℕ
⊢ f^[m * 0] = f^[m]^[0]

Tactic:
simp only [Nat.mul_zero, iterate_zero]

Premises used: Function.iterate_zero, Nat.mul_zero
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m n : ℕ
⊢ f^[m * (n + 1)] = f^[m]^[n + 1]

Tactic:
simp only [Nat.mul_succ, iterate_one, iterate_add, iterate_mul m n]

Premises used: Nat.mul_succ, Function.iterate_add, Function.iterate_one
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
x : α
h : f x = x
n_1 n : ℕ
ihn : f^[n] x = x
rw : f^[n] (f x) = x
rw₁ : f^[n] x = x
rw₂ rw₃ : x = x
⊢ f^[n.succ] x = x

Tactic:
rw [iterate_succ_apply, h, ihn]

Premises used: Function.iterate_succ_apply
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n : ℕ
rw : g ∘ id = g
rw₁ rw₂ : g = g
⊢ g ∘ f^[0] = g

Tactic:
rw [iterate_zero, comp_id]

Premises used: Function.comp_id, Function.iterate_zero
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n m : ℕ
rwa : g ∘ f^[m] ∘ f = g
rwa₁ : (g ∘ f^[m]) ∘ f = g
rwa₂ rwa₃ rwa₄ rwa₅ : g ∘ f = g
⊢ g ∘ f^[m + 1] = g

Tactic:
rwa [iterate_succ, ← comp_assoc, iterate_invariant h m]

Premises used: Function.iterate_succ, Function.comp_assoc
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
Hinj : Injective f
n : ℕ
⊢ Injective f^[n]

Tactic:
Nat.recOn n injective_id fun _ ihn ↦ ihn.comp Hinj

Premises used: Nat.recOn
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
Hsurj : Surjective f
n : ℕ
⊢ Surjective f^[n]

Tactic:
Nat.recOn n surjective_id fun _ ihn ↦ ihn.comp Hsurj

Premises used: Nat.recOn
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
Hbij : Bijective f
n : ℕ
⊢ Bijective f^[n]

Tactic:
⟨Hbij.1.iterate n, Hbij.2.iterate n⟩

Premises used: Function.Injective.iterate, And.right, And.left, And.intro, Function.Bijective, Function.Surjective.iterate
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
β : Type v
f : α → β
ga : α → α
gb : β → β
h : Semiconj f ga gb
n : ℕ
⊢ Semiconj f ga^[n] gb^[n]

Tactic:
Nat.recOn n id_right fun _ ihn ↦ ihn.comp_right h

Premises used: Nat.recOn
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k : ℕ
zero : Semiconj f^[0] (g k) (g k)
⊢ Semiconj f^[0] (g k) (g (0 + k))

Tactic:
rw [Nat.zero_add]

Premises used: Nat.zero_add
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k : ℕ
⊢ Semiconj f^[0] (g k) (g k)

Tactic:
id_left

Premises used: Nat.iterate, Function.Semiconj.id_left
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k : ℕ
⊢ Semiconj f^[0] (g k) (g k)

Tactic:
exact id_left

Premises used: Function.Semiconj.id_left
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
succ : Semiconj f^[n + 1] (g k) (g (n + (k + 1)))
⊢ Semiconj f^[n + 1] (g k) (g (n + 1 + k))

Tactic:
rw [Nat.add_right_comm, Nat.add_assoc]

Premises used: Nat.add_assoc, Nat.add_right_comm
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + (k + 1)))

Tactic:
(H k).trans (ihn (k + 1))

Premises used: Function.Semiconj.trans, Nat.iterate, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + (k + 1)))

Tactic:
exact (H k).trans (ihn (k + 1))

Premises used: Function.Semiconj.trans, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n k : ℕ
zero : ∀ (k : ℕ), Semiconj f^[0] (g k) (g (0 + k))
succ : ∀ (n : ℕ) (ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))) (k : ℕ), Semiconj f^[n + 1] (g k) (g (n + 1 + k))
⊢ Semiconj f^[n] (g k) (g (n + k))

Tactic:
induction n generalizing k with
  | zero =>
    rw [Nat.zero_add]
    exact id_left
  | succ n ihn =>
    rw [Nat.add_right_comm, Nat.add_assoc]
    exact (H k).trans (ihn (k + 1))

Premises used: Function.Semiconj.id_left, Nat.add_assoc, Nat.zero_add, Nat.add_right_comm
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f g : α → α
h : Commute f g
n : ℕ
⊢ Commute f g^[n]

Tactic:
Semiconj.iterate_right h n

Premises used: Function.Commute, Function.Semiconj.iterate_right
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f g : α → α
h : Commute f g
n : ℕ
⊢ Commute f^[n] g

Tactic:
(h.symm.iterate_right n).symm

Premises used: Function.Commute.iterate_right, Function.Commute.symm
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f g : α → α
h : Commute f g
m n : ℕ
⊢ Commute f^[m] g^[n]

Tactic:
(h.iterate_left m).iterate_right n

Premises used: Function.Commute.iterate_right, Function.Commute.iterate_left
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f g : α → α
h : Commute f g
n_1 : ℕ
x : α
hx : f x = g x
n : ℕ
ihn : f^[n] x = g^[n] x
⊢ f^[n.succ] x = g^[n.succ] x

Tactic:
simp only [iterate_succ_apply, hx, (h.iterate_left n).eq, ihn, ((refl g).iterate_right n).eq]

Premises used: Function.Semiconj.eq, Function.Commute.refl, Function.Commute.iterate_right, Function.iterate_succ_apply, Function.Commute.iterate_left
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f g : α → α
h : Commute f g
⊢ (f ∘ g)^[0] = f^[0] ∘ g^[0]

Tactic:
rfl
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f g : α → α
h : Commute f g
n : ℕ
ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]
succ : ∀ (x : α), (f ∘ g)^[n + 1] x = (f^[n + 1] ∘ g^[n + 1]) x
⊢ (f ∘ g)^[n + 1] = f^[n + 1] ∘ g^[n + 1]

Tactic:
funext x
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f g : α → α
h : Commute f g
n : ℕ
ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]
x : α
⊢ (f ∘ g)^[n + 1] x = (f^[n + 1] ∘ g^[n + 1]) x

Tactic:
simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]

Premises used: Function.iterate_succ, Function.Semiconj.eq, Function.Commute.iterate_right, Function.comp_apply
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f g : α → α
h : Commute f g
n : ℕ
zero : (f ∘ g)^[0] = f^[0] ∘ g^[0]
succ : ∀ (n : ℕ) (ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]), (f ∘ g)^[n + 1] = f^[n + 1] ∘ g^[n + 1]
⊢ (f ∘ g)^[n] = f^[n] ∘ g^[n]

Tactic:
induction n with
  | zero => rfl
  | succ n ihn =>
    funext x
    simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]

Premises used: Function.iterate_succ, Function.Semiconj.eq, Function.Commute.iterate_right, Function.comp_apply
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
n : ℕ
⊢ Commute f^[n] f

Tactic:
(refl f).iterate_left n

Premises used: Function.Commute.refl, Function.Commute.iterate_left
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
n : ℕ
⊢ Commute f f^[n]

Tactic:
(refl f).iterate_right n

Premises used: Function.Commute.refl, Function.Commute.iterate_right
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m n : ℕ
⊢ Commute f^[m] f^[n]

Tactic:
(refl f).iterate_iterate m n

Premises used: Function.Commute.iterate_iterate, Function.Commute.refl
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
op : α → α → α
hf : Semiconj₂ f op op
n : ℕ
⊢ Semiconj₂ f^[n] op op

Tactic:
Nat.recOn n (Semiconj₂.id_left op) fun _ ihn ↦ ihn.comp hf

Premises used: Nat.recOn
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
n : ℕ
rw : f^[n] ∘ f = f ∘ f^[n]
rw₁ rw₂ : f^[n] ∘ f = f^[n] ∘ f
⊢ f^[n.succ] = f ∘ f^[n]

Tactic:
rw [iterate_succ, (Commute.self_iterate f n).comp_eq]

Premises used: Function.Semiconj.comp_eq, Function.iterate_succ, Function.Commute.self_iterate
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
n : ℕ
x : α
rw : (f ∘ f^[n]) x = f (f^[n] x)
⊢ f^[n.succ] x = f (f^[n] x)

Tactic:
rw [iterate_succ']

Premises used: Function.iterate_succ'
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
n : ℕ
x : α
⊢ (f ∘ f^[n]) x = f (f^[n] x)

Tactic:
rfl
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
n : ℕ
hn : 0 < n
rw : f^[n.pred.succ] = f^[n]
rw₁ rw₂ : f^[n] = f^[n]
⊢ f^[n.pred] ∘ f = f^[n]

Tactic:
rw [← iterate_succ, Nat.succ_pred_eq_of_pos hn]

Premises used: Nat.succ_pred_eq_of_pos, Function.iterate_succ
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
n : ℕ
hn : 0 < n
rw : f^[n.pred.succ] = f^[n]
rw₁ rw₂ : f^[n] = f^[n]
⊢ f ∘ f^[n.pred] = f^[n]

Tactic:
rw [← iterate_succ', Nat.succ_pred_eq_of_pos hn]

Premises used: Nat.succ_pred_eq_of_pos, Function.iterate_succ'
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
motive : α → Sort u_1
f : α → α
app : (a : α) → motive a → motive (f a)
a : α
arg : motive a
⊢ rec motive arg app 0 = arg

Tactic:
rfl

Premises used: Function.Iterate.rec, rfl
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f g : α → α
hg : LeftInverse g f
n_1 n : ℕ
ihn : LeftInverse g^[n] f^[n]
rw : LeftInverse (g ∘ g^[n]) (f^[n] ∘ f)
⊢ LeftInverse g^[n.succ] f^[n.succ]

Tactic:
rw [iterate_succ', iterate_succ]

Premises used: Function.iterate_succ, Function.iterate_succ'
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f g : α → α
hg : LeftInverse g f
n_1 n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse (g ∘ g^[n]) (f^[n] ∘ f)

Tactic:
ihn.comp hg

Premises used: Function.LeftInverse.comp
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f g : α → α
hg : LeftInverse g f
n_1 n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse (g ∘ g^[n]) (f^[n] ∘ f)

Tactic:
exact ihn.comp hg

Premises used: Function.LeftInverse.comp
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f g : α → α
hg : RightInverse g f
n : ℕ
⊢ RightInverse g^[n] f^[n]

Tactic:
LeftInverse.iterate hg n

Premises used: Function.LeftInverse.iterate, Function.RightInverse
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m n : ℕ
rw rw₁ : f^[m * n] = f^[m * n]
⊢ f^[n * m] = f^[m * n]

Tactic:
rw [Nat.mul_comm]

Premises used: Nat.mul_comm
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
m n : ℕ
⊢ Commute (fun (f : α → α) ↦ f^[m]) fun (f : α → α) ↦ f^[n]

Tactic:
fun f ↦ iterate_comm f m n

Premises used: Function.Commute, Function.Semiconj, Function.iterate_comm
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
rw : f^[m + n] a = f^[n] a ↔ f^[n + m] a = f^[n] a
rw₁ rw₂ : f^[n + m] a = f^[n] a ↔ f^[n + m] a = f^[n] a
⊢ f^[m + n] a = f^[n] a ↔ f^[n] (f^[m] a) = f^[n] a

Tactic:
rw [← iterate_add_apply, Nat.add_comm]

Premises used: Function.iterate_add_apply, Nat.add_comm
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
inl : ∀ (h : m ≤ n), f^[m - n] a = a
inr : ∀ (h : n ≤ m), f^[m - n] a = a
⊢ f^[m - n] a = a

Tactic:
obtain h | h := Nat.le_total m n

Premises used: Nat.le_total
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : m ≤ n
⊢ f^[m - n] a = a

Tactic:
simp [Nat.sub_eq_zero_of_le h]

Premises used: Nat.sub_eq_zero_of_le
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : m ≤ n
⊢ f^[m - n] a = a

Tactic:
{ simp [Nat.sub_eq_zero_of_le h] }

Premises used: Nat.sub_eq_zero_of_le
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
rwa rwa₁ rwa₂ rwa₃ : f^[m] a = f^[n] a
⊢ f^[m - n + n] a = f^[n] a

Tactic:
rwa [Nat.sub_add_cancel h]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a

Tactic:
exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h])

Premises used: Function.iterate_cancel_of_add
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a

Tactic:
{ exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h]) }

Premises used: Function.iterate_cancel_of_add
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Sort u_1
f : α → α
⊢ Involutive f ↔ f^[2] = id

Tactic:
funext_iff.symm

Premises used: funext_iff, Nat.iterate, Function.Involutive, Iff.symm
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
β : Type v
f : α → α
a : α
⊢ foldl (fun (b : α) (x : β) ↦ f b) a [] = f^[length.{v} (α := β) []] a

Tactic:
rfl
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
β : Type v
f : α → α
b : β
l : List β
H : ∀ (a : α), foldl (fun (b : α) (x : β) ↦ f b) a l = f^[l.length] a
a : α
cons : foldl (fun (b : α) (x : β) ↦ f b) a (b :: l) = f^[l.length + 1] a
cons₁ : foldl (fun (b : α) (x : β) ↦ f b) (f a) l = f^[l.length + 1] a
cons₂ : foldl (fun (b : α) (x : β) ↦ f b) (f a) l = f^[l.length] (f a)
cons₃ cons₄ : f^[l.length] (f a) = f^[l.length] (f a)
⊢ foldl (fun (b : α) (x : β) ↦ f b) a (b :: l) = f^[(b :: l).length] a

Tactic:
rw [length_cons, foldl, iterate_succ_apply, H]

Premises used: List.length_cons, List.foldl, Function.iterate_succ_apply