awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α → α' → β
a : α
a' : α'
b : β
⊢ uncurry (update (β := fun (a : α) ↦ α' → β) f a (update (β := fun (a : α') ↦ β) (f a) a' b)) =
    update (β := fun (a : α × α') ↦ β) (uncurry f) (a, a') b
have a₁ : curry (uncurry (update (β := fun (a : α) ↦ α' → β) f a (update (β := fun (a : α') ↦ β) (f a) a' b))) =
  curry (update (β := fun (a : α × α') ↦ β) (uncurry f) (a, a') b)
Tactic: apply curry_injective
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
f : α → α
h : Involutive f
g : α → α
hg : LeftInverse g f
x : α
⊢ g x = f x
have rw : g (f (f x)) = f (f (f x))
Tactic: rw [← h x, hg, h]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
f : α → α
h : Involutive f
g : α → α
hg : LeftInverse g f
x : α
rw : g (f (f x)) = f (f (f x))
⊢ g x = f x
have rw₁ : f x = f (f (f x))
Tactic: rw [← h x, hg, h]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
f : α → α
h : Involutive f
g : α → α
hg : LeftInverse g f
x : α
rw : g (f (f x)) = f (f (f x))
rw₁ : f x = f (f (f x))
⊢ g x = f x
have rw₂ : f x = f x
Tactic: rw [← h x, hg, h]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
f : α → α
h : Involutive f
P : Prop
inst : Decidable P
x : α
⊢ f (if P then x else f x) = if ¬P then x else f x
have rw : (if P then f x else f (f x)) = if ¬P then x else f x
Tactic: rw [apply_ite f, h, ite_not]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
f : α → α
h : Involutive f
P : Prop
inst : Decidable P
x : α
rw : (if P then f x else f (f x)) = if ¬P then x else f x
⊢ f (if P then x else f x) = if ¬P then x else f x
have rw₁ : (if P then f x else x) = if ¬P then x else f x
Tactic: rw [apply_ite f, h, ite_not]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u
f : α → α
h : Involutive f
P : Prop
inst : Decidable P
x : α
rw : (if P then f x else f (f x)) = if ¬P then x else f x
rw₁ : (if P then f x else x) = if ¬P then x else f x
⊢ f (if P then x else f x) = if ¬P then x else f x
have rw₂ : (if P then f x else x) = if P then f x else x
Tactic: rw [apply_ite f, h, ite_not]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∀ (a : α), ∃! b : β, r a b) ↔ ∃ (f : α → β), ∀ {a : α} {b : β}, r a b ↔ f a = b
have refine_1 : ∀ (h : ∀ (a : α), ∃! b : β, r a b), ∃ (f : α → β), ∀ {a : α} {b : β}, r a b ↔ f a = b
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
refine_1 : ∀ (h : ∀ (a : α), ∃! b : β, r a b), ∃ (f : α → β), ∀ {a : α} {b : β}, r a b ↔ f a = b
⊢ (∀ (a : α), ∃! b : β, r a b) ↔ ∃ (f : α → β), ∀ {a : α} {b : β}, r a b ↔ f a = b
have refine_2 : (∃ (f : α → β), ∀ {a : α} {b : β}, r a b ↔ f a = b) → ∀ (a : α), ∃! b : β, r a b
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b : β, r a b
⊢ ∃ (f : α → β), ∀ {a : α} {b : β}, r a b ↔ f a = b
have refine_1 : ∀ {a : α} {b : β} (hr : r a b),
  (fun (a : α) ↦
        Exists.choose (p := fun (x : β) ↦ (fun (b : β) ↦ r a b) x ∧ ∀ (y : β), (fun (b : β) ↦ r a b) y → y = x) sorry)
      a =
    b
Tactic: refine ⟨fun a ↦ (h a).choose, fun hr ↦ ?_, fun h' ↦ h' ▸ ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b : β, r a b
refine_1 :
  ∀ {a : α} {b : β} (hr : r a b),
    (fun (a : α) ↦
          Exists.choose (p := fun (x : β) ↦ (fun (b : β) ↦ r a b) x ∧ ∀ (y : β), (fun (b : β) ↦ r a b) y → y = x) ⋯)
        a =
      b
⊢ ∃ (f : α → β), ∀ {a : α} {b : β}, r a b ↔ f a = b
have refine_1₁ : ∀ {a : α} {b : β}
  (h' :
    (fun (a : α) ↦
          Exists.choose (p := fun (x : β) ↦ (fun (b : β) ↦ r a b) x ∧ ∀ (y : β), (fun (b : β) ↦ r a b) y → y = x) sorry)
        a =
      b),
  r a
    ((fun (a : α) ↦
        Exists.choose (p := fun (x : β) ↦ (fun (b : β) ↦ r a b) x ∧ ∀ (y : β), (fun (b : β) ↦ r a b) y → y = x) sorry)
      a)
Tactic: refine ⟨fun a ↦ (h a).choose, fun hr ↦ ?_, fun h' ↦ h' ▸ ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
⊢ (∀ (a : α), ∃! b : α, r a b) ↔ ∃ (f : α → α), Involutive f ∧ Eq.{max 1 u_1} r fun (x1 x2 : α) ↦ f x1 = x2
have refine : ∀ (h : ∀ (a : α), ∃! b : α, r a b), ∃ (f : α → α), Involutive f ∧ Eq.{max 1 u_1} r fun (x1 x2 : α) ↦ f x1 = x2
Tactic: refine ⟨fun h ↦ ?_, fun ⟨f, _, hf⟩ ↦ forall_existsUnique_iff'.2 ⟨f, hf⟩⟩
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
h : ∀ (a : α), ∃! b : α, r a b
⊢ ∃ (f : α → α), Involutive f ∧ Eq.{max 1 u_1} r fun (x1 x2 : α) ↦ f x1 = x2
have rcases : ∀ (f : α → α) (hr : Symmetric fun (x1 x2 : α) ↦ f x1 = x2) (h : ∀ (a : α), ∃! b : α, (fun (x1 x2 : α) ↦ f x1 = x2) a b),
  ∃ (f_1 : α → α),
    Involutive f_1 ∧ Eq.{max 1 u_1} (α := α → α → Prop) (fun (x1 x2 : α) ↦ f x1 = x2) fun (x1 x2 : α) ↦ f_1 x1 = x2
Tactic: rcases forall_existsUnique_iff'.1 h with ⟨f, rfl : r = _⟩
Cleared hypotheses: r, hr, h
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α β : Sort u_3
h : α = β
⊢ Bijective h.mp
have refl : Bijective sorry.mp
Tactic: cases h
Cleared hypotheses: β, h
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α β : Sort u_3
h : α = β
⊢ Bijective h.mpr
have refl : Bijective sorry.mpr
Tactic: cases h
Cleared hypotheses: β, h
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α β : Sort u_3
h : α = β
⊢ Bijective (cast h)
have refl : Bijective (cast sorry)
Tactic: cases h
Cleared hypotheses: β, h
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ HEq (α := γ (f (g (f a)))) (C (g (f a))) (C a)
have rw : C a ≍ C a
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Logic.Function.CompTypeclasses (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
φ : M → N
ψ : N → P
χ : M → P
h : CompTriple φ ψ χ
x : M
⊢ ψ (φ x) = χ x
have rw : ψ (φ x) = (ψ ∘ φ) x
Tactic: rw [← h.comp_eq, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Logic.Function.CompTypeclasses (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
φ : M → N
ψ : N → P
χ : M → P
h : CompTriple φ ψ χ
x : M
rw : ψ (φ x) = (ψ ∘ φ) x
⊢ ψ (φ x) = χ x
have rw₁ : ψ (φ x) = ψ (φ x)
Tactic: rw [← h.comp_eq, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Logic.Function.Conjugate (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
⊢ f (ga' x) = gb' (f x)
have rw : gb' (gb (f (ga' x))) = gb' (f x)
Tactic: rw [← hb (f (ga' x)), ← h.eq, ha x]
-- Lean 4 proof step from Mathlib.Logic.Function.Conjugate (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
rw : gb' (gb (f (ga' x))) = gb' (f x)
⊢ f (ga' x) = gb' (f x)
have rw₁ : gb' (f (ga (ga' x))) = gb' (f x)
Tactic: rw [← hb (f (ga' x)), ← h.eq, ha x]
-- Lean 4 proof step from Mathlib.Logic.Function.Conjugate (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
rw : gb' (gb (f (ga' x))) = gb' (f x)
rw₁ : gb' (f (ga (ga' x))) = gb' (f x)
⊢ f (ga' x) = gb' (f x)
have rw₂ : gb' (f x) = gb' (f x)
Tactic: rw [← hb (f (ga' x)), ← h.eq, ha x]
-- Lean 4 proof step from Mathlib.Logic.Function.Conjugate (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
f' : β → α
h : Semiconj f ga gb
hf₁ : LeftInverse f' f
hf₂ : RightInverse f' f
x : β
⊢ f' (gb x) = ga (f' x)
have rw : f (f' (gb x)) = f (ga (f' x))
Tactic: rw [← hf₁.injective.eq_iff, h, hf₂, hf₂]
-- Lean 4 proof step from Mathlib.Logic.Function.Conjugate (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
f' : β → α
h : Semiconj f ga gb
hf₁ : LeftInverse f' f
hf₂ : RightInverse f' f
x : β
rw : f (f' (gb x)) = f (ga (f' x))
⊢ f' (gb x) = ga (f' x)
have rw₁ : f (f' (gb x)) = gb (f (f' x))
Tactic: rw [← hf₁.injective.eq_iff, h, hf₂, hf₂]
-- Lean 4 proof step from Mathlib.Logic.Function.Conjugate (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
f' : β → α
h : Semiconj f ga gb
hf₁ : LeftInverse f' f
hf₂ : RightInverse f' f
x : β
rw : f (f' (gb x)) = f (ga (f' x))
rw₁ : f (f' (gb x)) = gb (f (f' x))
⊢ f' (gb x) = ga (f' x)
have rw₂ : gb x = gb (f (f' x))
Tactic: rw [← hf₁.injective.eq_iff, h, hf₂, hf₂]
-- Lean 4 proof step from Mathlib.Logic.Function.Conjugate (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
f' : β → α
h : Semiconj f ga gb
hf₁ : LeftInverse f' f
hf₂ : RightInverse f' f
x : β
rw : f (f' (gb x)) = f (ga (f' x))
rw₁ : f (f' (gb x)) = gb (f (f' x))
rw₂ : gb x = gb (f (f' x))
⊢ f' (gb x) = ga (f' x)
have rw₃ : gb x = gb x
Tactic: rw [← hf₁.injective.eq_iff, h, hf₂, hf₂]
-- Lean 4 proof step from Mathlib.Logic.Function.Conjugate (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst : Std.IdempotentOp gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x : α
⊢ f (ga x x) = f x
have rw : gb (f x) (f x) = f x
Tactic: rw [h.eq, Std.IdempotentOp.idempotent (op := gb)]
-- Lean 4 proof step from Mathlib.Logic.Function.Conjugate (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst : Std.IdempotentOp gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x : α
rw : gb (f x) (f x) = f x
⊢ f (ga x x) = f x
have rw₁ : f x = f x
Tactic: rw [h.eq, Std.IdempotentOp.idempotent (op := gb)]
-- Lean 4 proof step from Mathlib.Logic.Function.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
I : Injective f
a b : α
⊢ (f a == f b) = (a == b)
have pos : ∀ (h : (a == b) = true), (f a == f b) = (a == b)
Tactic: by_cases h : a == b
-- Lean 4 proof step from Mathlib.Logic.Function.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
I : Injective f
a b : α
pos : ∀ (h : (a == b) = true), (f a == f b) = (a == b)
⊢ (f a == f b) = (a == b)
have neg : ∀ (h : ¬(a == b) = true), (f a == f b) = (a == b)
Tactic: by_cases h : a == b
-- Lean 4 proof step from Mathlib.Logic.Function.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : (a == b) = true
⊢ (f a == f b) = (a == b)
have pos : f a = f b
Tactic: simp [h]
-- Lean 4 proof step from Mathlib.Logic.Function.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : ¬(a == b) = true
⊢ (f a == f b) = (a == b)
have neg : ¬f a = f b
Tactic: simp [h]
-- Lean 4 proof step from Mathlib.Logic.Function.DependsOn (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst : Nonempty β
f : ((i : ι) → α i) → β
s : Set ι
⊢ DependsOn (α := α) f s ↔ ∃ (g : ((i : (↑s : Type u_1)) → α (↑i : ι)) → β), f = g ∘ s.restrict (π := α)
have rw : FactorsThrough f (s.restrict (π := α)) ↔ ∃ (g : ((i : (↑s : Type u_1)) → α (↑i : ι)) → β), f = g ∘ s.restrict (π := α)
Tactic: rw [dependsOn_iff_factorsThrough, factorsThrough_iff]
-- Lean 4 proof step from Mathlib.Logic.Function.DependsOn (goal)
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 (π := α)
⊢ DependsOn (α := α) f s ↔ ∃ (g : ((i : (↑s : Type u_1)) → α (↑i : ι)) → β), f = g ∘ s.restrict (π := α)
have rw₁ : (∃ (e : ((a : (↑s : Type u_1)) → α (↑a : ι)) → β), f = e ∘ s.restrict (π := α)) ↔
  ∃ (g : ((i : (↑s : Type u_1)) → α (↑i : ι)) → β), f = g ∘ s.restrict (π := α)
Tactic: rw [dependsOn_iff_factorsThrough, factorsThrough_iff]
-- Lean 4 proof step from Mathlib.Logic.Function.FiberPartition (hypothesis)
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
x : (↑(↑a : Set Y) : Type u_2)
⊢ f (↑x : Y) = image f a
have 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)) sorry) =
  (↑a : Set Y)
Tactic: have := a.2.choose_spec
-- Lean 4 proof step from Mathlib.Logic.Function.FiberPartition (goal)
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
y : Y
a : Fiber f
h : f y = image f a
⊢ y ∈ (↑a : Set Y)
have rw : y ∈ f ⁻¹' {image f a}
Tactic: rw [a.eq_fiber_image]
-- Lean 4 proof step from Mathlib.Logic.Function.FiberPartition (goal)
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
⊢ (↑a : Set Y).Nonempty
have refine : preimage f a ∈ (↑a : Set Y)
Tactic: refine ⟨preimage f a, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Function.FiberPartition (goal)
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
⊢ preimage f a ∈ (↑a : Set Y)
have rw : f (preimage f a) = image f a
Tactic: rw [mem_iff_eq_image, ← map_preimage_eq_image]
-- Lean 4 proof step from Mathlib.Logic.Function.FiberPartition (goal)
Goal:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
rw : f (preimage f a) = image f a
⊢ preimage f a ∈ (↑a : Set Y)
have rw₁ : f (preimage f a) = f (preimage f a)
Tactic: rw [mem_iff_eq_image, ← map_preimage_eq_image]
-- Lean 4 proof step from Mathlib.Logic.Function.FiberPartition (goal)
Goal:
Y : Type u_2
Z : Type u_3
W : Type u_4
f : Y → Z
g : Z → W
a : Fiber (g ∘ f)
⊢ g (f (preimage (g ∘ f) a)) = image (g ∘ f) a
have rw : g (f (preimage (g ∘ f) a)) = (g ∘ f) (preimage (g ∘ f) a)
Tactic: rw [← map_preimage_eq_image, comp_apply]
-- Lean 4 proof step from Mathlib.Logic.Function.FiberPartition (goal)
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)
⊢ g (f (preimage (g ∘ f) a)) = image (g ∘ f) a
have rw₁ : g (f (preimage (g ∘ f) a)) = g (f (preimage (g ∘ f) a))
Tactic: rw [← map_preimage_eq_image, comp_apply]
-- Lean 4 proof step from Mathlib.Logic.Function.FiberPartition (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : Y → Z
g : X → Y
a : Fiber (f ∘ g)
⊢ image (f ∘ g) a = image f (mk f (g (preimage (f ∘ g) a)))
have rw : f (g (preimage (f ∘ g) a)) = image f (mk f (g (preimage (f ∘ g) a)))
Tactic: rw [← map_preimage_eq_image_map _ _ a, mk_image]
-- Lean 4 proof step from Mathlib.Logic.Function.FiberPartition (goal)
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)))
⊢ image (f ∘ g) a = image f (mk f (g (preimage (f ∘ g) a)))
have rw₁ : f (g (preimage (f ∘ g) a)) = f (g (preimage (f ∘ g) a))
Tactic: rw [← map_preimage_eq_image_map _ _ a, mk_image]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
n_1 n : ℕ
ihn : Eq.{u + 1} (α := α → α) id^[n] id
⊢ Eq.{u + 1} (α := α → α) id^[n.succ] id
have rw : Eq.{u + 1} (α := α → α) (id^[n] ∘ id) id
Tactic: rw [iterate_succ, ihn, id_comp]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
n_1 n : ℕ
ihn : Eq.{u + 1} (α := α → α) id^[n] id
rw : Eq.{u + 1} (α := α → α) (id^[n] ∘ id) id
⊢ Eq.{u + 1} (α := α → α) id^[n.succ] id
have rw₁ : Eq.{u + 1} (α := α → α) (id ∘ id) id
Tactic: rw [iterate_succ, ihn, id_comp]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
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
⊢ Eq.{u + 1} (α := α → α) id^[n.succ] id
have rw₂ : Eq.{u + 1} (α := α → α) id id
Tactic: rw [iterate_succ, ihn, id_comp]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
m n : ℕ
⊢ f^[m + n.succ] = f^[m] ∘ f^[n.succ]
have rw : (f^[m] ∘ f^[n]) ∘ f = f^[m] ∘ f^[n] ∘ f
Tactic: rw [Nat.add_succ, iterate_succ, iterate_succ, iterate_add m n]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
m n : ℕ
x : α
⊢ f^[m + n] x = f^[m] (f^[n] x)
have rw : (f^[m] ∘ f^[n]) x = f^[m] (f^[n] x)
Tactic: rw [iterate_add f m n]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
x : α
h : f x = x
n_1 n : ℕ
ihn : f^[n] x = x
⊢ f^[n.succ] x = x
have rw : f^[n] (f x) = x
Tactic: rw [iterate_succ_apply, h, ihn]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
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
⊢ f^[n.succ] x = x
have rw₂ : x = x
Tactic: rw [iterate_succ_apply, h, ihn]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n : ℕ
⊢ g ∘ f^[0] = g
have rw : g ∘ id = g
Tactic: rw [iterate_zero, comp_id]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n : ℕ
rw : g ∘ id = g
⊢ g ∘ f^[0] = g
have rw₁ : g = g
Tactic: rw [iterate_zero, comp_id]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n m : ℕ
⊢ g ∘ f^[m + 1] = g
have rwa : g ∘ f^[m] ∘ f = g
Tactic: rwa [iterate_succ, ← comp_assoc, iterate_invariant h m]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n m : ℕ
rwa : g ∘ f^[m] ∘ f = g
⊢ g ∘ f^[m + 1] = g
have rwa₁ : (g ∘ f^[m]) ∘ f = g
Tactic: rwa [iterate_succ, ← comp_assoc, iterate_invariant h m]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k : ℕ
⊢ Semiconj f^[0] (g k) (g (0 + k))
have zero : Semiconj f^[0] (g k) (g k)
Tactic: rw [Nat.zero_add]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
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 + 1 + k))
have succ : Semiconj f^[n + 1] (g k) (g (n + (k + 1)))
Tactic: rw [Nat.add_right_comm, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n k : ℕ
⊢ Semiconj f^[n] (g k) (g (n + k))
have zero : ∀ (k : ℕ), Semiconj f^[0] (g k) (g (0 + 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))
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
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))
⊢ Semiconj f^[n] (g k) (g (n + k))
have succ : ∀ (n : ℕ) (ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))) (k : ℕ), Semiconj f^[n + 1] (g k) (g (n + 1 + 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))
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f g : α → α
h : Commute f g
n : ℕ
ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]
⊢ (f ∘ g)^[n + 1] = f^[n + 1] ∘ g^[n + 1]
have succ : ∀ (x : α), (f ∘ g)^[n + 1] x = (f^[n + 1] ∘ g^[n + 1]) x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f g : α → α
h : Commute f g
n : ℕ
⊢ (f ∘ g)^[n] = f^[n] ∘ g^[n]
have zero : (f ∘ g)^[0] = f^[0] ∘ g^[0]
Tactic: induction n with
  | zero => rfl
  | succ n ihn =>
    funext x
    simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f g : α → α
h : Commute f g
n : ℕ
zero : (f ∘ g)^[0] = f^[0] ∘ g^[0]
⊢ (f ∘ g)^[n] = f^[n] ∘ g^[n]
have succ : ∀ (n : ℕ) (ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]), (f ∘ g)^[n + 1] = f^[n + 1] ∘ g^[n + 1]
Tactic: induction n with
  | zero => rfl
  | succ n ihn =>
    funext x
    simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
n : ℕ
⊢ f^[n.succ] = f ∘ f^[n]
have rw : f^[n] ∘ f = f ∘ f^[n]
Tactic: rw [iterate_succ, (Commute.self_iterate f n).comp_eq]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
n : ℕ
rw : f^[n] ∘ f = f ∘ f^[n]
⊢ f^[n.succ] = f ∘ f^[n]
have rw₁ : f^[n] ∘ f = f^[n] ∘ f
Tactic: rw [iterate_succ, (Commute.self_iterate f n).comp_eq]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
n : ℕ
x : α
⊢ f^[n.succ] x = f (f^[n] x)
have rw : (f ∘ f^[n]) x = f (f^[n] x)
Tactic: rw [iterate_succ']
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f^[n.pred] ∘ f = f^[n]
have rw : f^[n.pred.succ] = f^[n]
Tactic: rw [← iterate_succ, Nat.succ_pred_eq_of_pos hn]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
n : ℕ
hn : 0 < n
rw : f^[n.pred.succ] = f^[n]
⊢ f^[n.pred] ∘ f = f^[n]
have rw₁ : f^[n] = f^[n]
Tactic: rw [← iterate_succ, Nat.succ_pred_eq_of_pos hn]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f ∘ f^[n.pred] = f^[n]
have rw : f^[n.pred.succ] = f^[n]
Tactic: rw [← iterate_succ', Nat.succ_pred_eq_of_pos hn]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
n : ℕ
hn : 0 < n
rw : f^[n.pred.succ] = f^[n]
⊢ f ∘ f^[n.pred] = f^[n]
have rw₁ : f^[n] = f^[n]
Tactic: rw [← iterate_succ', Nat.succ_pred_eq_of_pos hn]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f g : α → α
hg : LeftInverse g f
n_1 n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse g^[n.succ] f^[n.succ]
have rw : LeftInverse (g ∘ g^[n]) (f^[n] ∘ f)
Tactic: rw [iterate_succ', iterate_succ]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
m n : ℕ
⊢ f^[n * m] = f^[m * n]
have rw : f^[m * n] = f^[m * n]
Tactic: rw [Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
⊢ f^[m + n] a = f^[n] a ↔ f^[n] (f^[m] a) = f^[n] a
have rw : f^[m + n] a = f^[n] a ↔ f^[n + m] a = f^[n] a
Tactic: rw [← iterate_add_apply, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
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
⊢ f^[m + n] a = f^[n] a ↔ f^[n] (f^[m] a) = f^[n] a
have rw₁ : f^[n + m] a = f^[n] a ↔ f^[n + m] a = f^[n] a
Tactic: rw [← iterate_add_apply, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
⊢ f^[m - n] a = a
have inl : ∀ (h : m ≤ n), f^[m - n] a = a
Tactic: obtain h | h := Nat.le_total m n
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
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
⊢ f^[m - n] a = a
have inr : ∀ (h : n ≤ m), f^[m - n] a = a
Tactic: obtain h | h := Nat.le_total m n
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
β : Type v
f : α → α
b : β
l : List β
H : ∀ (a : α), foldl (fun (b : α) (x : β) ↦ f b) a l = f^[l.length] a
a : α
⊢ foldl (fun (b : α) (x : β) ↦ f b) a (b :: l) = f^[(b :: l).length] a
have cons : foldl (fun (b : α) (x : β) ↦ f b) a (b :: l) = f^[l.length + 1] a
Tactic: rw [length_cons, foldl, iterate_succ_apply, H]