harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
theorem addRupCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
    (f_readyForRupAdd : ReadyForRupAdd f)
    (f_readyForRatAdd : ReadyForRatAdd f) (c : β) (f' : σ) (rupHints : Array Nat)
    (heq : performRupAdd f c rupHints = (f', true))
    (restPrf : List (Action β α)) (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a)
    (ih : ∀ (f : σ),
      ReadyForRupAdd f → ReadyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) →
      lratChecker f restPrf = success → Unsatisfiable α f)
    (f'_success : lratChecker f' restPrf = success) :
    Unsatisfiable α f

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
c : β
f' : σ
rupHints : Array Nat
heq : performRupAdd f c rupHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f'_success : lratChecker f' restPrf = success
⊢ Unsatisfiable α f

Tactic:
have f'_def := rupAdd_result f c rupHints f' f_readyForRupAdd heq

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
c : β
f' : σ
rupHints : Array Nat
heq : performRupAdd f c rupHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
⊢ Unsatisfiable α f
-- Mathlib/Algebra/Order/Group/Multiset.lean
lemma Nodup.le_nsmul_iff_le {s t : Multiset α} {n : ℕ} (h : s.Nodup) (hn : n ≠ 0) :
    s ≤ n • t ↔ s ≤ t

Proof state:
α : Type u_1
s t : Multiset α
n : ℕ
h : s.Nodup
hn : n ≠ 0
⊢ s ≤ n • t ↔ s ≤ t

Tactic:
simp [← h.le_dedup_iff_le, Iff.comm, ← h.le_dedup_iff_le, hn]

Result:
no goals

Proof state:
α : Type u_1
s t : Multiset α
n : ℕ
h : s.Nodup
hn : n ≠ 0
⊢ s ≤ n • t ↔ s ≤ t

Tactic:
classical simp [← h.le_dedup_iff_le, Iff.comm, ← h.le_dedup_iff_le, hn]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/FloorPow.lean
theorem tendsto_div_of_monotone_of_exists_subseq_tendsto_div (u : ℕ → ℝ) (l : ℝ)
    (hmono : Monotone u)
    (hlim : ∀ a : ℝ, 1 < a → ∃ c : ℕ → ℕ, (∀ᶠ n in atTop, (c (n + 1) : ℝ) ≤ a * c n) ∧
      Tendsto c atTop atTop ∧ Tendsto (fun n => u (c n) / c n) atTop (𝓝 l)) :
    Tendsto (fun n => u n / n) atTop (𝓝 l)

Proof state:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n => u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n => u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := (image (fun i => c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
⊢ (1 + ε) * ↑(c (N - 1)) * l - u (c (N - 1)) = ↑(c (N - 1)) * l - u (c (N - 1)) + ε * ↑(c (N - 1)) * l

Tactic:
ring

Result:
no goals

Proof state:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n => u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n => u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := (image (fun i => c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
⊢ ε * ↑(c N) + ε * ↑(c (N - 1)) * l ≤ ε * ((1 + ε) * ↑(c (N - 1))) + ε * ↑(c (N - 1)) * l

Tactic:
gcongr

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem Transcendental.of_aeval {r : A} {f : R[X]}
    (H : Transcendental R (Polynomial.aeval r f)) : Transcendental R f

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
H : ∀ (p : R[X]), (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0
⊢ ∀ (p : R[X]), (Polynomial.aeval f) p = 0 → p = 0

Tactic:
intro p hp

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
H : ∀ (p : R[X]), (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval f) p = 0
⊢ p = 0

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
H : Transcendental R ((Polynomial.aeval r) f)
⊢ Transcendental R f

Tactic:
rw [transcendental_iff] at H ⊢

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
H : ∀ (p : R[X]), (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0
⊢ ∀ (p : R[X]), (Polynomial.aeval f) p = 0 → p = 0

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
H : ∀ (p : R[X]), (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval f) p = 0
⊢ p = 0

Tactic:
exact H p (by rw [← aeval_comp, comp_eq_aeval, hp, map_zero])

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
H : ∀ (p : R[X]), (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval f) p = 0
⊢ (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0

Tactic:
rw [← aeval_comp, comp_eq_aeval, hp, map_zero]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
lemma mk_image2_le {α β γ : Type u} {f : α → β → γ} {s : Set α} {t : Set β} :
    #(image2 f s t) ≤ #s * #t

Proof state:
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ #↑(image2 f s t) ≤ #↑s * #↑t

Tactic:
rw [← image_uncurry_prod, ← mk_setProd]

Result:
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ #↑(uncurry f '' s ×ˢ t) ≤ #↑(s ×ˢ t)

Proof state:
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ #↑(uncurry f '' s ×ˢ t) ≤ #↑(s ×ˢ t)

Tactic:
exact mk_image_le

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem wittOne_zero_eq_one : wittOne p 0 = 1

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittOne p 0) = (map (Int.castRingHom ℚ)) 1

Tactic:
simp only [wittOne, wittStructureRat, xInTermsOfW_zero, map_one, bind₁_X_right,
  map_wittStructureInt]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittOne p 0 = 1

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittOne p 0) = (map (Int.castRingHom ℚ)) 1
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem ichildren_mk [DecidableEq F.A] [Inhabited (M F)] (x : F (M F)) (i : F.Idx) :
    ichildren i (M.mk x) = x.iget i

Proof state:
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
x : ↑F F.M
i : F.Idx
⊢ (if H' : i.fst = (M.mk x).head then (M.mk x).children (cast ⋯ i.snd) else default) =
    if h : i.fst = x.fst then x.snd (cast ⋯ i.snd) else default

Tactic:
congr with h

Result:
no goals

Proof state:
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
x : ↑F F.M
i : F.Idx
⊢ ichildren i (M.mk x) = x.iget i

Tactic:
dsimp only [ichildren, PFunctor.Obj.iget]

Result:
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
x : ↑F F.M
i : F.Idx
⊢ (if H' : i.fst = (M.mk x).head then (M.mk x).children (cast ⋯ i.snd) else default) =
    if h : i.fst = x.fst then x.snd (cast ⋯ i.snd) else default
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
/-- A characterization of the a.e.-measurability of the indicator function which takes a constant
value `b` on a set `A` and `0` elsewhere. -/
lemma aemeasurable_indicator_const_iff {s} [MeasurableSingletonClass β] (b : β) [NeZero b] :
    AEMeasurable (s.indicator (fun _ ↦ b)) μ ↔ NullMeasurableSet s μ

Proof state:
case h.e'_3
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : AEMeasurable (s.indicator fun x => b) μ
⊢ s = (if b ∈ {0}ᶜ then s else ∅) ∪ if 0 ∈ {0}ᶜ then sᶜ else ∅

Tactic:
simp [NeZero.ne b]

Result:
no goals

Proof state:
case mp
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : AEMeasurable (s.indicator fun x => b) μ
⊢ NullMeasurableSet s μ

Tactic:
convert h.nullMeasurable (MeasurableSet.singleton (0 : β)).compl

Result:
case h.e'_3
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : AEMeasurable (s.indicator fun x => b) μ
⊢ s = (s.indicator fun x => b) ⁻¹' {0}ᶜ

Proof state:
case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : NullMeasurableSet s μ
⊢ AEMeasurable (s.indicator fun x => b) μ

Tactic:
exact (aemeasurable_indicator_iff₀ h).mpr aemeasurable_const

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ AEMeasurable (s.indicator fun x => b) μ ↔ NullMeasurableSet s μ

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : AEMeasurable (s.indicator fun x => b) μ
⊢ NullMeasurableSet s μ

case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : NullMeasurableSet s μ
⊢ AEMeasurable (s.indicator fun x => b) μ

Proof state:
case h.e'_3
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : AEMeasurable (s.indicator fun x => b) μ
⊢ s = (s.indicator fun x => b) ⁻¹' {0}ᶜ

Tactic:
rw [indicator_const_preimage_eq_union s {0}ᶜ b]

Result:
case h.e'_3
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : AEMeasurable (s.indicator fun x => b) μ
⊢ s = (if b ∈ {0}ᶜ then s else ∅) ∪ if 0 ∈ {0}ᶜ then sᶜ else ∅
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem sInf_toSubring (s : Set (Subfield K)) :
    (sInf s).toSubring = ⨅ t ∈ s, Subfield.toSubring t

Proof state:
case h
K : Type u
inst✝ : DivisionRing K
s : Set (Subfield K)
x : K
⊢ x ∈ (sInf s).toSubring ↔ x ∈ ⨅ t ∈ s, t.toSubring

Tactic:
simp [mem_sInf, ← sInf_image, Subring.mem_sInf]

Result:
no goals

Proof state:
K : Type u
inst✝ : DivisionRing K
s : Set (Subfield K)
⊢ (sInf s).toSubring = ⨅ t ∈ s, t.toSubring

Tactic:
ext x

Result:
case h
K : Type u
inst✝ : DivisionRing K
s : Set (Subfield K)
x : K
⊢ x ∈ (sInf s).toSubring ↔ x ∈ ⨅ t ∈ s, t.toSubring
-- Mathlib/Probability/Distributions/Pareto.lean
/-- The pdf of the Pareto distribution integrates to `1`. -/
@[simp]
lemma lintegral_paretoPDF_eq_one (ht : 0 < t) (hr : 0 < r) :
    ∫⁻ x, paretoPDF t r x = 1

Proof state:
case hf
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ 0 ≤ᶠ[ae (ℙ.restrict (Ici t))] fun x => r * t ^ r * x ^ (-(r + 1))

Tactic:
rw [EventuallyLE, ae_restrict_iff' measurableSet_Ici]

Result:
case hf
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ ∀ᵐ (x : ℝ), x ∈ Ici t → 0 x ≤ r * t ^ r * x ^ (-(r + 1))
-- Mathlib/Topology/Algebra/Module/FiniteDimension.lean
theorem isClosedMap_smul_left [T2Space E] (c : E) : IsClosedMap fun x : 𝕜 => x • c

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space E
c : E
⊢ IsClosedMap fun x => x • c

Tactic:
by_cases hc : c = 0

Result:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space E
c : E
hc : c = 0
⊢ IsClosedMap fun x => x • c

case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space E
c : E
hc : ¬c = 0
⊢ IsClosedMap fun x => x • c

Proof state:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space E
c : E
hc : ¬c = 0
⊢ IsClosedMap fun x => x • c

Tactic:
exact (isClosedEmbedding_smul_left hc).isClosedMap

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space E
c : E
hc : c = 0
⊢ IsClosedMap fun x => x • c

Tactic:
simp_rw [hc, smul_zero]

Result:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space E
c : E
hc : c = 0
⊢ IsClosedMap fun x => 0

Proof state:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space E
c : E
hc : c = 0
⊢ IsClosedMap fun x => 0

Tactic:
exact isClosedMap_const

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem digits_two_eq_bits (n : ℕ) : digits 2 n = n.bits.map fun b => cond b 1 0

Proof state:
case f
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits
⊢ digits 2 (bit b n) = List.map (fun b => bif b then 1 else 0) (b :: n.bits)

Tactic:
cases b

Result:
case f.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits
⊢ digits 2 (bit false n) = List.map (fun b => bif b then 1 else 0) (false :: n.bits)

case f.true
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits
⊢ digits 2 (bit true n) = List.map (fun b => bif b then 1 else 0) (true :: n.bits)

Proof state:
case f
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits
⊢ digits 2 (bit b n) = List.map (fun b => bif b then 1 else 0) (bit b n).bits

Tactic:
rw [bits_append_bit _ _ fun hn => absurd hn h]

Result:
case f
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits
⊢ digits 2 (bit b n) = List.map (fun b => bif b then 1 else 0) (b :: n.bits)

Proof state:
case f.true
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits
⊢ digits 2 (bit true n) = List.map (fun b => bif b then 1 else 0) (true :: n.bits)

Tactic:
simpa [Nat.bit, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]

Result:
no goals

Proof state:
case f.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits
⊢ bit false n % 2 :: digits 2 (bit false n / 2) = List.map (fun b => bif b then 1 else 0) (false :: n.bits)

Tactic:
simpa [Nat.bit]

Result:
no goals

Proof state:
n : ℕ
⊢ digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits

Tactic:
induction' n using Nat.binaryRecFromOne with b n h ih

Result:
case z₀

⊢ digits 2 0 = List.map (fun b => bif b then 1 else 0) (bits 0)

case z₁

⊢ digits 2 1 = List.map (fun b => bif b then 1 else 0) (bits 1)

case f
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits
⊢ digits 2 (bit b n) = List.map (fun b => bif b then 1 else 0) (bit b n).bits

Proof state:
case f.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits
⊢ digits 2 (bit false n) = List.map (fun b => bif b then 1 else 0) (false :: n.bits)

Tactic:
rw [digits_def' one_lt_two]

Result:
case f.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits
⊢ bit false n % 2 :: digits 2 (bit false n / 2) = List.map (fun b => bif b then 1 else 0) (false :: n.bits)

case f.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits
⊢ 0 < bit false n

Proof state:
case z₁

⊢ digits 2 1 = List.map (fun b => bif b then 1 else 0) (bits 1)

Tactic:
simp

Result:
no goals

Proof state:
case z₀

⊢ digits 2 0 = List.map (fun b => bif b then 1 else 0) (bits 0)

Tactic:
simp

Result:
no goals

Proof state:
case f.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits
⊢ 0 < bit false n

Tactic:
simpa [Nat.bit, pos_iff_ne_zero]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem mul_pow_charP_coeff_succ [CharP R p] (x : 𝕎 R) {m n : ℕ} :
    (x * p ^ n).coeff (m + n) = x.coeff m ^ (p ^ n)

Proof state:
case succ.e_a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
⊢ (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n

Tactic:
exact ih

Result:
no goals

Proof state:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
m : ℕ
⊢ (x * ↑p ^ 0).coeff (m + 0) = x.coeff m ^ p ^ 0

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
m n : ℕ
⊢ (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n

Tactic:
induction' n with n ih generalizing m

Result:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
m : ℕ
⊢ (x * ↑p ^ 0).coeff (m + 0) = x.coeff m ^ p ^ 0

case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
⊢ (x * ↑p ^ (n + 1)).coeff (m + (n + 1)) = x.coeff m ^ p ^ (n + 1)

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
⊢ (x * ↑p ^ (n + 1)).coeff (m + (n + 1)) = x.coeff m ^ p ^ (n + 1)

Tactic:
rw [pow_succ, ← mul_assoc, ← add_assoc,mul_charP_coeff_succ, pow_succ, pow_mul]

Result:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
⊢ (x * ↑p ^ n).coeff (m + n) ^ p = (x.coeff m ^ p ^ n) ^ p

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
⊢ (x * ↑p ^ n).coeff (m + n) ^ p = (x.coeff m ^ p ^ n) ^ p

Tactic:
congr

Result:
case succ.e_a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
⊢ (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n
-- Mathlib/GroupTheory/Perm/Cycle/PossibleTypes.lean
theorem Equiv.Perm.exists_with_cycleType_iff {m : Multiset ℕ} :
    (∃ g : Equiv.Perm α, g.cycleType = m) ↔
      (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ (List.map (fun l => l.formPerm) p).prod.cycleType = m

Tactic:
rw [Equiv.Perm.cycleType_eq _ rfl]

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ ↑(List.map (Finset.card ∘ support) (List.map (fun l => l.formPerm) p)) = m

case h.h1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ ∀ σ ∈ List.map (fun l => l.formPerm) p, σ.IsCycle

case h.h2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.Pairwise Disjoint (List.map (fun l => l.formPerm) p)

Proof state:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.map ((Finset.card ∘ support) ∘ fun l => l.formPerm) p = m.toList

Tactic:
rw [← hp_length]

Result:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.map ((Finset.card ∘ support) ∘ fun l => l.formPerm) p = List.map List.length p

Proof state:
case h.h1.intro.intro.hn
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
hx_nodup : x.Nodup
⊢ 2 ≤ x.length

Tactic:
exact hp2 x hx

Result:
no goals