awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
⊢ Ne (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s ∩ s) : ENNReal) (⊤ : ENNReal)

Tactic:
finiteness
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
⊢ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)

Tactic:
have hμ_diff : μ (f ⁻¹' s \ s) = μ (s \ f ⁻¹' s) :=
    measure_diff_symm (hfμ.measurable hsm).nullMeasurableSet hsm.nullMeasurableSet
      (hfμ.measure_preimage hsm.nullMeasurableSet) (by finiteness)
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hμ_diff :
  Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
⊢ Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s ∩ s) : ENNReal) (⊤ : ENNReal)

Tactic:
finiteness
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hμ_diff :
  Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
⊢ Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)

Tactic:
have hν_diff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s) :=
    measure_diff_symm (hfν.measurable hsm).nullMeasurableSet hsm.nullMeasurableSet
      (hfν.measure_preimage hsm.nullMeasurableSet) (by finiteness)
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hμ_diff :
  Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
suffices : f ⁻¹' s =ᶠ[ae ν] s
⊢ ∀ᵐ (a : X) ∂ν, (μ.rnDeriv ν ∘ f) a < c ↔ μ.rnDeriv ν a < c

Tactic:
suffices f ⁻¹' s =ᵐ[ν] s from this.mem_iff
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hμ_diff :
  Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
suffices : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
⊢ f ⁻¹' s =ᶠ[ae ν] s

Tactic:
suffices ν (f ⁻¹' s \ s) = 0 from (ae_le_set.mpr this).antisymm (ae_le_set.mpr <| hν_diff ▸ this)
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hμ_diff :
  Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
contrapose! :
  ∀ (h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)),
    Ne (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
      ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
⊢ Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)

Tactic:
contrapose! hμ_diff with h₀
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
h :
  LT.lt (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
⊢ Ne (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)

Tactic:
apply ne_of_gt

Premises used: ne_of_gt
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
⊢ (μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) = ∫⁻ (a : X) in s \ f ⁻¹' s, μ.rnDeriv ν a ∂ν

Tactic:
(setLIntegral_rnDeriv hμν _).symm

Premises used: MeasureTheory.Measure.setLIntegral_rnDeriv, Eq.symm
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
hfi : ∫⁻ (x : X) in s \ f ⁻¹' s, μ.rnDeriv ν x ∂ν ≠ ⊤
h : ∀ᵐ (x : X) ∂ν, x ∈ s \ f ⁻¹' s → μ.rnDeriv ν x < c
⊢ ∫⁻ (a : X) in s \ f ⁻¹' s, μ.rnDeriv ν a ∂ν < ∫⁻ (x : X) in s \ f ⁻¹' s, c ∂ν

Tactic:
apply setLIntegral_strict_mono (hsm.diff (hfμ.measurable hsm)) (hν_diff ▸ h₀) measurable_const

Premises used: MeasurableSet.diff, MeasureTheory.setLIntegral_strict_mono, MeasureTheory.MeasurePreserving.measurable, measurable_const
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
hfi : Ne (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal) (⊤ : ENNReal)
⊢ ∫⁻ (x : X) in s \ f ⁻¹' s, μ.rnDeriv ν x ∂ν ≠ ⊤

Tactic:
rw [setLIntegral_rnDeriv hμν]

Premises used: MeasureTheory.Measure.setLIntegral_rnDeriv
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
⊢ Ne (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal) (⊤ : ENNReal)

Tactic:
finiteness
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
⊢ ∀ᵐ (x : X) ∂ν, x ∈ s \ f ⁻¹' s → μ.rnDeriv ν x < c

Tactic:
.of_forall fun x hx ↦ hx.1

Premises used: Filter.Eventually.of_forall, And.left
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
⊢ ∀ᵐ (x : X) ∂ν, x ∈ s \ f ⁻¹' s → μ.rnDeriv ν x < c

Tactic:
exact .of_forall fun x hx ↦ hx.1
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
⊢ ∫⁻ (x : X) in s \ f ⁻¹' s, c ∂ν = ∫⁻ (x : X) in f ⁻¹' s \ s, c ∂ν

Tactic:
simp [hν_diff]
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
⊢ Measurable (μ.rnDeriv ν)

Tactic:
fun_prop
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
⊢ ∫⁻ (a : X) in f ⁻¹' s \ s, μ.rnDeriv ν a ∂ν = (μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s)

Tactic:
setLIntegral_rnDeriv hμν _

Premises used: MeasureTheory.Measure.setLIntegral_rnDeriv
-- Module: Mathlib.Dynamics.Ergodic.RadonNikodym
Goal:
X : Type u_1
m : MeasurableSpace X
μ_1 ν : Measure X
inst : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst_1 : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a : X | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_diff :
  Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)
    ((ν : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
h₀ : Ne (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal) (0 : ENNReal)
μ₁ : ∫⁻ (a : X) in s \ f ⁻¹' s, μ.rnDeriv ν a ∂ν < ∫⁻ (x : X) in s \ f ⁻¹' s, c ∂ν
μ₂ : ∫⁻ (x : X) in s \ f ⁻¹' s, c ∂ν = ∫⁻ (x : X) in f ⁻¹' s \ s, c ∂ν
⊢ LT.lt (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ f ⁻¹' s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (f ⁻¹' s \ s) : ENNReal)

Tactic:
calc
    μ (s \ f ⁻¹' s) = ∫⁻ a in s \ f ⁻¹' s, μ.rnDeriv ν a ∂ν := (setLIntegral_rnDeriv hμν _).symm
    _ < ∫⁻ _ in s \ f ⁻¹' s, c ∂ν := by
      apply setLIntegral_strict_mono (hsm.diff (hfμ.measurable hsm)) (hν_diff ▸ h₀) measurable_const
      · rw [setLIntegral_rnDeriv hμν]
        finiteness
      · exact .of_forall fun x hx ↦ hx.1
    _ = ∫⁻ _ in f ⁻¹' s \ s, c ∂ν := by simp [hν_diff]
    _ ≤ ∫⁻ a in f ⁻¹' s \ s, μ.rnDeriv ν a ∂ν :=
      setLIntegral_mono (by fun_prop) (fun x hx ↦ not_lt.mp hx.2)
    _ = μ (f ⁻¹' s \ s) := setLIntegral_rnDeriv hμν _

Premises used: MeasureTheory.Measure.setLIntegral_rnDeriv, MeasureTheory.setLIntegral_mono, SDiff.sdiff, not_lt, Set.preimage, Iff.mp, Eq.symm, DFunLike.coe
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
f g : α → α
x : α
hf : IsFixedPt f x
hg : IsFixedPt g x
⊢ IsFixedPt (f ∘ g) x

Tactic:
calc
    f (g x) = f x := congr_arg f hg
    _ = x := hf

Premises used: Trans.trans, congr_arg, Function.IsFixedPt
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
f : α → α
x : α
hf : IsFixedPt f x
n : ℕ
⊢ IsFixedPt f^[n] x

Tactic:
iterate_fixed hf n

Premises used: Function.IsFixedPt, Function.iterate_fixed
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
f g : α → α
x : α
hfg : IsFixedPt (f ∘ g) x
hg : IsFixedPt g x
⊢ IsFixedPt f x

Tactic:
calc
    f x = f (g x) := congr_arg f hg.symm
    _ = x := hfg

Premises used: Trans.trans, congr_arg, Function.IsFixedPt, Eq.symm
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
f g : α → α
x : α
hf : IsFixedPt f x
h : LeftInverse g f
⊢ IsFixedPt g x

Tactic:
calc
    g x = g (f x) := congr_arg g hf.symm
    _ = x := h x

Premises used: Trans.trans, congr_arg, Function.IsFixedPt, Eq.symm
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
x : α
hx : IsFixedPt fa x
g : α → β
h : Semiconj g fa fb
⊢ IsFixedPt fb (g x)

Tactic:
calc
    fb (g x) = g (fa x) := (h.eq x).symm
    _ = g x := congr_arg g hx

Premises used: Trans.trans, Function.Semiconj.eq, congr_arg, Function.IsFixedPt, Eq.symm
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
f : α → α
x : α
hx : IsFixedPt f x
⊢ IsFixedPt f x

Tactic:
hx
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
f : α → α
x : α
hx : IsFixedPt f x
⊢ IsFixedPt f (f x)

Tactic:
convert! hx
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
f : α → α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
rw : IsFixedPt (Set.preimage f)^[n] s
⊢ IsFixedPt (Set.preimage f^[n]) s

Tactic:
rw [Set.preimage_iterate_eq]

Premises used: Set.preimage_iterate_eq
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
f : α → α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f)^[n] s

Tactic:
h.iterate n

Premises used: Function.IsFixedPt.iterate
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
f : α → α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f)^[n] s

Tactic:
exact h.iterate n

Premises used: Function.IsFixedPt.iterate
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
f : α → α
s : Set α
h : IsFixedPt (Set.image f) s
n : ℕ
⊢ IsFixedPt (Set.image f^[n]) s

Tactic:
Set.image_iterate_eq ▸ h.iterate n

Premises used: Set.image_iterate_eq, Eq.rec, Function.IsFixedPt.iterate, Eq.symm
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
x : α
e : Perm α
h : IsFixedPt (⇑e : (a : α) → α) x
⊢ IsFixedPt (⇑(Equiv.symm e) : (a : α) → α) x

Tactic:
h.to_leftInverse e.leftInverse_symm

Premises used: Equiv.leftInverse_symm, Function.IsFixedPt.to_leftInverse
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
x : α
e : Perm α
h : IsFixedPt (⇑e : (a : α) → α) x
⊢ IsFixedPt (⇑e⁻¹ : (a : α) → α) x

Tactic:
h.equiv_symm

Premises used: Function.IsFixedPt.equiv_symm
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
x : α
e : Perm α
h : IsFixedPt (⇑e : (a : α) → α) x
n : ℕ
⊢ IsFixedPt (⇑(e ^ n) : (a : α) → α) x

Tactic:
h.iterate _

Premises used: Function.IsFixedPt.iterate
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
f : α → α
hf : Injective f
x : α
⊢ IsFixedPt f (f x) ↔ IsFixedPt f x

Tactic:
⟨fun h => hf h.eq, IsFixedPt.apply⟩

Premises used: Function.IsFixedPt.apply, Function.IsFixedPt.eq, Iff.intro
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
g : α → β
h : Semiconj g fa fb
⊢ Set.MapsTo g (fixedPoints fa) (fixedPoints fb)

Tactic:
fun _ hx => hx.map h

Premises used: Set.Mem, setOf, Function.fixedPoints, Set.MapsTo, Function.IsFixedPt, Function.IsFixedPt.map
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
⊢ Set.InvOn f g (fixedPoints (f ∘ g)) (fixedPoints (g ∘ f))

Tactic:
⟨fun _ => id, fun _ => id⟩

Premises used: Set.InvOn, id, And.intro
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
⊢ Set.MapsTo f (fixedPoints (g ∘ f)) (fixedPoints (f ∘ g))

Tactic:
fun _ hx => hx.map fun _ => rfl

Premises used: Set.Mem, setOf, Function.fixedPoints, Set.MapsTo, Function.IsFixedPt, Function.IsFixedPt.map, rfl
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
⊢ Set.BijOn g (fixedPoints (f ∘ g)) (fixedPoints (g ∘ f))

Tactic:
(invOn_fixedPoints_comp f g).bijOn (mapsTo_fixedPoints_comp g f) (mapsTo_fixedPoints_comp f g)

Premises used: Function.mapsTo_fixedPoints_comp, Function.invOn_fixedPoints_comp, Set.InvOn.bijOn
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.InvOn f g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
simpa only [h.comp_eq] using Function.invOn_fixedPoints_comp f g

Premises used: Function.Semiconj.comp_eq, Function.invOn_fixedPoints_comp
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.BijOn f (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
simpa only [h.comp_eq] using bijOn_fixedPoints_comp g f

Premises used: Function.Semiconj.comp_eq, Function.bijOn_fixedPoints_comp
-- Module: Mathlib.Dynamics.FixedPoints.Basic
Goal:
α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.BijOn g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
simpa only [h.comp_eq] using bijOn_fixedPoints_comp f g

Premises used: Function.Semiconj.comp_eq, Function.bijOn_fixedPoints_comp
-- Module: Mathlib.Dynamics.FixedPoints.Defs
Goal:
α : Type u_1
x : α
f : α → α
⊢ x ∈ fixedPoints f ↔ IsFixedPt f x

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Function.fixedPoints, Function.IsFixedPt
-- Module: Mathlib.Dynamics.FixedPoints.Defs
Goal:
α : Type u_2
f : α → α
x : α
⊢ x ∈ fixedPoints f ↔ f x = x

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Function.fixedPoints, Function.IsFixedPt
-- Module: Mathlib.Dynamics.FixedPoints.Defs
Goal:
α : Type u_1
x : α
⊢ Membership.mem (γ := Set α) (fixedPoints id) x ↔ Membership.mem (γ := Set α) Set.univ x

Tactic:
simpa using isFixedPt_id _

Premises used: Function.isFixedPt_id
-- Module: Mathlib.Dynamics.FixedPoints.Defs
Goal:
α : Type u_1
f : α → α
⊢ fixedPoints f ⊆ Set.range f

Tactic:
fun x hx => ⟨x, hx⟩

Premises used: Set.Mem, setOf, Set.Subset, Exists.intro, Set.range
-- Module: Mathlib.Dynamics.FixedPoints.Prufer
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ g • s = s

Tactic:
le_antisymm (this hg) ?_

Premises used: le_antisymm
-- Module: Mathlib.Dynamics.FixedPoints.Prufer
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
refine : s ≤ g • s
⊢ g • s = s

Tactic:
refine le_antisymm (this hg) ?_

Premises used: le_antisymm
-- Module: Mathlib.Dynamics.FixedPoints.Prufer
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
rw : g • g⁻¹ • s
| s

Tactic:
rw [← smul_inv_smul g s]

Premises used: smul_inv_smul
-- Module: Mathlib.Dynamics.FixedPoints.Prufer
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
conv_lhs : g • g⁻¹ • s ≤ g • s
⊢ s ≤ g • s

Tactic:
conv_lhs => rw [← smul_inv_smul g s]

Premises used: smul_inv_smul
-- Module: Mathlib.Dynamics.FixedPoints.Prufer
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
rw : (g ^ n ^ j)⁻¹ = 1
rw₁ : Eq.{u_1 + 1} (α := G) 1⁻¹ 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := G) 1 1
⊢ g⁻¹ ^ n ^ j = 1

Tactic:
rw [inv_zpow, hg, inv_one]

Premises used: inv_one, inv_zpow
-- Module: Mathlib.Dynamics.FixedPoints.Prufer
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ g⁻¹ ^ n ^ j = 1

Tactic:
replace hg : g⁻¹ ^ n ^ j = 1 := by rw [inv_zpow, hg, inv_one]
-- Module: Mathlib.Dynamics.FixedPoints.Prufer
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
hg : g⁻¹ ^ n ^ j = 1
⊢ g • g⁻¹ • s ≤ g • s

Tactic:
simpa only [le_eq_subset, smul_set_subset_smul_set_iff] using this hg

Premises used: Set.le_eq_subset, Set.smul_set_subset_smul_set_iff
-- Module: Mathlib.Dynamics.FixedPoints.Prufer
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
suffices : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ g • s = s

Tactic:
suffices ∀ {g' : G} (_ : g' ^ n ^ j = 1), g' • s ⊆ s by
    refine le_antisymm (this hg) ?_
    conv_lhs => rw [← smul_inv_smul g s]
    replace hg : g⁻¹ ^ n ^ j = 1 := by rw [inv_zpow, hg, inv_one]
    simpa only [le_eq_subset, smul_set_subset_smul_set_iff] using this hg
-- Module: Mathlib.Dynamics.FixedPoints.Prufer
Goal:
G : Type u_1
inst : CommGroup G
n : ℤ
s : Set G
hs : (fun (x : G) ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
rw : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s ⊆ (fun (x : G) ↦ x ^ n)^[j] ⁻¹' s
⊢ ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s

Tactic:
rw [(IsFixedPt.preimage_iterate hs j : (zpowGroupHom n)^[j] ⁻¹' s = s).symm]

Premises used: Function.IsFixedPt.preimage_iterate, Eq.symm