harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
/-- The norm, relative to `ℤ`, of `ζ - 1` in a `p ^ (k + 1)`-th cyclotomic extension of `ℚ` is
a prime if `p ^ (k  + 1) ≠ 2`. -/
lemma prime_norm_toInteger_sub_one_of_prime_pow_ne_two [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (htwo : p ^ (k + 1) ≠ 2) :
    Prime (Algebra.norm ℤ (hζ.toInteger - 1))

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p
⊢ Prime ↑↑p

Tactic:
exact Nat.prime_iff_prime_int.1 hp.out

Result:
no goals

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
rw [this]

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p
⊢ Prime ↑↑p

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger ^ ↑p ^ 0 - 1) = ↑↑p ^ ↑p ^ 0
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
simp only [pow_zero, pow_one] at this

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
have := hζ.norm_toInteger_pow_sub_one_of_prime_pow_ne_two (zero_le _) htwo

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger ^ ↑p ^ 0 - 1) = ↑↑p ^ ↑p ^ 0
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem EqOnSource.trans' {e e' : PartialEquiv α β} {f f' : PartialEquiv β γ} (he : e ≈ e')
    (hf : f ≈ f') : e.trans f ≈ e'.trans f'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ e.trans f ≈ e'.trans f'

Tactic:
constructor

Result:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ (e.trans f).source = (e'.trans f').source

case right
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ EqOn (↑(e.trans f)) (↑(e'.trans f')) (e.trans f).source

Proof state:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ ↑e.symm '' (e.target ∩ f.source) = ↑e'.symm '' (e.target ∩ f.source)

Tactic:
exact (he.symm'.eqOn.mono inter_subset_left).image_eq

Result:
no goals

Proof state:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ (e.trans f).source = (e'.trans f').source

Tactic:
rw [trans_source'', trans_source'', ← target_eq he, ← hf.1]

Result:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ ↑e.symm '' (e.target ∩ f.source) = ↑e'.symm '' (e.target ∩ f.source)

Proof state:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ (e.trans f).source
⊢ ↑(e.trans f) x = ↑(e'.trans f') x

Tactic:
rw [trans_source] at hx

Result:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ e.source ∩ ↑e ⁻¹' f.source
⊢ ↑(e.trans f) x = ↑(e'.trans f') x

Proof state:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ EqOn (↑(e.trans f)) (↑(e'.trans f')) (e.trans f).source

Tactic:
intro x hx

Result:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ (e.trans f).source
⊢ ↑(e.trans f) x = ↑(e'.trans f') x

Proof state:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ e.source ∩ ↑e ⁻¹' f.source
⊢ ↑(e.trans f) x = ↑(e'.trans f') x

Tactic:
simp [Function.comp_apply, PartialEquiv.coe_trans, (he.2 hx.1).symm, hf.2 hx.2]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem eventually_pow_one_div_le {x : ℝ≥0∞} (hx : x ≠ ∞) {y : ℝ≥0∞} (hy : 1 < y) :
    ∀ᶠ n : ℕ in atTop, x ^ (1 / n : ℝ) ≤ y

Proof state:
case neg.intro
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ ↑y

Tactic:
refine this.congr (Eventually.of_forall fun n => ?_)

Result:
case neg.intro
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
n : ℕ
⊢ x ^ (1 / ↑n) ≤ y ↔ ↑x ^ (1 / ↑n) ≤ ↑y

Proof state:
case neg
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : ¬y = ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y

Tactic:
lift y to ℝ≥0 using h

Result:
case neg.intro
x y : ℝ≥0
hy : 1 < ↑y
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ ↑y

Proof state:
case pos
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : y = ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y

Tactic:
exact Eventually.of_forall fun n => h.symm ▸ le_top

Result:
no goals

Proof state:
case neg.intro
x y : ℝ≥0
hy : 1 < ↑y
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ ↑y

Tactic:
have := NNReal.eventually_pow_one_div_le x (mod_cast hy : 1 < y)

Result:
case neg.intro
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ ↑y

Proof state:
x : ℝ≥0∞
hx : x ≠ ⊤
y : ℝ≥0∞
hy : 1 < y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y

Tactic:
lift x to ℝ≥0 using hx

Result:
case intro
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y

Proof state:
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
n : ℕ
⊢ 0 ≤ 1 / ↑n

Tactic:
positivity

Result:
no goals

Proof state:
case neg.intro
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
n : ℕ
⊢ x ^ (1 / ↑n) ≤ y ↔ ↑x ^ (1 / ↑n) ≤ ↑y

Tactic:
rw [← coe_rpow_of_nonneg x (by positivity : 0 ≤ (1 / n : ℝ)), coe_le_coe]

Result:
no goals

Proof state:
case intro
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y

Tactic:
by_cases h : y = ∞

Result:
case pos
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : y = ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y

case neg
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : ¬y = ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y
-- Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
lemma NNReal.closedBall_zero_eq_Icc {c : ℝ} (c_nn : 0 ≤ c) :
    Metric.closedBall (0 : ℝ≥0) c = Set.Icc 0 c.toNNReal

Proof state:
case h.e'_3.h.e'_4
c : ℝ
c_nn : 0 ≤ c
⊢ c.toNNReal = ⟨c, c_nn⟩

Tactic:
simp [Real.toNNReal, c_nn]

Result:
no goals

Proof state:
c : ℝ
c_nn : 0 ≤ c
⊢ closedBall 0 c = Icc 0 c.toNNReal

Tactic:
convert NNReal.closedBall_zero_eq_Icc' ⟨c, c_nn⟩

Result:
case h.e'_3.h.e'_4
c : ℝ
c_nn : 0 ≤ c
⊢ c.toNNReal = ⟨c, c_nn⟩
-- Mathlib/Order/CompleteLattice.lean
lemma biSup_lt_eq_iSup {ι : Type*} [LT ι] [NoMaxOrder ι] {f : ι → α} :
    ⨆ (i) (j < i), f j = ⨆ i, f i

Proof state:
case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
⊢ ⨆ i, f i ≤ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j

Tactic:
refine iSup_le fun j ↦ ?_

Result:
case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
j : ι
⊢ f j ≤ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j

Proof state:
case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
j : ι
⊢ f j ≤ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j

Tactic:
obtain ⟨i, jlt⟩ := exists_gt j

Result:
case a.intro
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
j i : ι
jlt : j < i
⊢ f j ≤ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j

Proof state:
case a.intro
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
j i : ι
jlt : j < i
⊢ f j ≤ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j

Tactic:
exact le_iSup_of_le i (le_iSup₂_of_le j jlt le_rfl)

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j ≤ ⨆ i, f i

Tactic:
exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j = ⨆ i, f i

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j ≤ ⨆ i, f i

case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
⊢ ⨆ i, f i ≤ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem lineDerivWithin_of_mem_nhds (h : s ∈ 𝓝 x) :
    lineDerivWithin 𝕜 f s x v = lineDeriv 𝕜 f x v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
s : Set E
x v : E
h : s ∈ 𝓝 x
⊢ lineDerivWithin 𝕜 f s x v = lineDeriv 𝕜 f x v

Tactic:
apply derivWithin_of_mem_nhds

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
s : Set E
x v : E
h : s ∈ 𝓝 x
⊢ (fun t => x + t • v) ⁻¹' s ∈ 𝓝 0

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
s : Set E
x v : E
h : s ∈ 𝓝 x
⊢ (fun t => x + t • v) ⁻¹' s ∈ 𝓝 0

Tactic:
apply (Continuous.continuousAt _).preimage_mem_nhds (by simpa using h)

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
s : Set E
x v : E
h : s ∈ 𝓝 x
⊢ Continuous fun t => x + t • v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
s : Set E
x v : E
h : s ∈ 𝓝 x
⊢ s ∈ 𝓝 (x + 0 • v)

Tactic:
simpa using h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
s : Set E
x v : E
h : s ∈ 𝓝 x
⊢ Continuous fun t => x + t • v

Tactic:
fun_prop

Result:
no goals
-- Mathlib/MeasureTheory/Measure/DiracProba.lean
/-- In a completely regular T0 topological space, the inverse of `diracProbaEquiv` is continuous. -/
lemma continuous_diracProbaEquivSymm [T0Space X] [CompletelyRegularSpace X] :
    Continuous (diracProbaEquiv (X := X)).symm

Proof state:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
⊢ ContinuousAt (⇑diracProbaEquiv.symm) μ

Tactic:
apply continuousAt_of_tendsto_nhds (y := diracProbaInverse μ)

Result:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
⊢ Tendsto (⇑diracProbaEquiv.symm) (𝓝 μ) (𝓝 (diracProbaInverse μ))

Proof state:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
⊢ Continuous ⇑diracProbaEquiv.symm

Tactic:
apply continuous_iff_continuousAt.mpr

Result:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
⊢ ∀ (x : ↑(range diracProba)), ContinuousAt (⇑diracProbaEquiv.symm) x

Proof state:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
⊢ ∀ (x : ↑(range diracProba)), ContinuousAt (⇑diracProbaEquiv.symm) x

Tactic:
intro μ

Result:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
⊢ ContinuousAt (⇑diracProbaEquiv.symm) μ

Proof state:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
⊢ Tendsto (⇑diracProbaEquiv.symm) (𝓝 μ) (𝓝 (diracProbaInverse μ))

Tactic:
exact (tendsto_diracProbaEquivSymm_iff_tendsto _).mpr fun _ mem_nhd ↦ mem_nhd

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_eq (x : BitVec n) : setWidth n x = x

Proof state:
case a
n : Nat
x : BitVec n
⊢ (setWidth n x).toNat = x.toNat

Tactic:
let ⟨x, lt_n⟩ := x

Result:
case a
n : Nat
x✝ : BitVec n
x : Nat
lt_n : x < 2 ^ n
⊢ (setWidth n { toFin := ⟨x, lt_n⟩ }).toNat = { toFin := ⟨x, lt_n⟩ }.toNat

Proof state:
n : Nat
x : BitVec n
⊢ setWidth n x = x

Tactic:
apply eq_of_toNat_eq

Result:
case a
n : Nat
x : BitVec n
⊢ (setWidth n x).toNat = x.toNat

Proof state:
case a
n : Nat
x✝ : BitVec n
x : Nat
lt_n : x < 2 ^ n
⊢ (setWidth n { toFin := ⟨x, lt_n⟩ }).toNat = { toFin := ⟨x, lt_n⟩ }.toNat

Tactic:
simp [setWidth]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem compact_open_separated_mul_right {K U : Set G} (hK : IsCompact K) (hU : IsOpen U)
    (hKU : K ⊆ U) : ∃ V ∈ 𝓝 (1 : G), K * V ⊆ U

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ V ∈ 𝓝 1, K * V ⊆ U

Tactic:
refine hK.induction_on ?_ ?_ ?_ ?_

Result:
case refine_1
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ V ∈ 𝓝 1, ∅ * V ⊆ U

case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, s ⊆ t → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, s * V ⊆ U

case refine_3
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, (∃ V ∈ 𝓝 1, s * V ⊆ U) → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, (s ∪ t) * V ⊆ U

case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U
-- Mathlib/RepresentationTheory/Basic.lean
theorem smul_ofModule_asModule (r : MonoidAlgebra k G) (m : (ofModule M).asModule) :
    (RestrictScalars.addEquiv k _ _) ((ofModule M).asModuleEquiv (r • m)) =
      r • (RestrictScalars.addEquiv k _ _) ((ofModule M).asModuleEquiv (G := G) m)

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : (ofModule M).asModule
⊢ (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) ((ofModule M).asModuleEquiv (r • m)) =
    r • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) ((ofModule M).asModuleEquiv m)

Tactic:
dsimp

Result:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : (ofModule M).asModule
⊢ (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) (((ofModule M).asAlgebraHom r) ((ofModule M).asModuleEquiv m)) =
    r • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) ((ofModule M).asModuleEquiv m)

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : (ofModule M).asModule
⊢ (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) (((ofModule M).asAlgebraHom r) ((ofModule M).asModuleEquiv m)) =
    r • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) ((ofModule M).asModuleEquiv m)

Tactic:
simp only [AddEquiv.apply_symm_apply, ofModule_asAlgebraHom_apply_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_univ_three [CommMonoid β] (f : Fin 3 → β) : ∏ i, f i = f 0 * f 1 * f 2

Proof state:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 3 → β
⊢ ∏ i : Fin 3, f i = f 0 * f 1 * f 2

Tactic:
rw [prod_univ_castSucc, prod_univ_two]

Result:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 3 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (last 2) = f 0 * f 1 * f 2

Proof state:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 3 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (last 2) = f 0 * f 1 * f 2

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
theorem mapPiLocalization_id : mapPiLocalization (.id R) = .id _

Proof state:
case a.h
R : Type u_1
inst✝ : CommSemiring R
x✝¹ : PiLocalization R
x✝ : PrimeSpectrum R
⊢ (mapPiLocalization (RingHom.id R)) x✝¹ x✝ = (RingHom.id (PiLocalization R)) x✝¹ x✝

Tactic:
exact congr($(Localization.localRingHom_id _) _)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ mapPiLocalization (RingHom.id R) = RingHom.id (PiLocalization R)

Tactic:
ext

Result:
case a.h
R : Type u_1
inst✝ : CommSemiring R
x✝¹ : PiLocalization R
x✝ : PrimeSpectrum R
⊢ (mapPiLocalization (RingHom.id R)) x✝¹ x✝ = (RingHom.id (PiLocalization R)) x✝¹ x✝
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem measurableSet_insert {a : α} {s : Set α} :
    MeasurableSet (insert a s) ↔ MeasurableSet s

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : MeasurableSet (insert a s)
ha : a ∈ s
⊢ MeasurableSet s

Tactic:
rwa [← insert_eq_of_mem ha]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ MeasurableSet (insert a s) ↔ MeasurableSet s

Tactic:
classical
exact ⟨fun h =>
  if ha : a ∈ s then by rwa [← insert_eq_of_mem ha]
  else insert_diff_self_of_not_mem ha ▸ h.diff (.singleton _),
  fun h => h.insert a⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ MeasurableSet (insert a s) ↔ MeasurableSet s

Tactic:
exact ⟨fun h =>
  if ha : a ∈ s then by rwa [← insert_eq_of_mem ha]
  else insert_diff_self_of_not_mem ha ▸ h.diff (.singleton _),
  fun h => h.insert a⟩

Result:
no goals
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem isVanKampenColimit_of_evaluation [HasPullbacks D] [HasColimitsOfShape J D] (F : J ⥤ C ⥤ D)
    (c : Cocone F) (hc : ∀ x : C, IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)) :
    IsVanKampenColimit c

Proof state:
case mp
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
⊢ Nonempty (IsColimit c') → ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

Tactic:
rintro ⟨hc'⟩ j

Result:
case mp.intro
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
hc' : IsColimit c'
j : J
⊢ IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
-- Mathlib/Topology/Algebra/Module/WeakDual.lean
theorem toWeakSpaceCLM_eq_toWeakSpace (x : E) :
    toWeakSpaceCLM 𝕜 E x = toWeakSpace 𝕜 E x

Proof state:
𝕜 : Type u_2
E : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x : E
⊢ (toWeakSpaceCLM 𝕜 E) x = (toWeakSpace 𝕜 E) x

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem le_sup_left (f g : α →ₘ[μ] β) : f ≤ f ⊔ g

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g : α →ₘ[μ] β
a✝ : α
ha : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑f a✝ ≤ ↑(f ⊔ g) a✝

Tactic:
rw [ha]

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g : α →ₘ[μ] β
a✝ : α
ha : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑f a✝ ≤ ↑f a✝ ⊔ ↑g a✝

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g : α →ₘ[μ] β
⊢ f ≤ f ⊔ g

Tactic:
rw [← coeFn_le]

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g : α →ₘ[μ] β
⊢ ↑f ≤ᶠ[ae μ] ↑(f ⊔ g)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g : α →ₘ[μ] β
a✝ : α
ha : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑f a✝ ≤ ↑f a✝ ⊔ ↑g a✝

Tactic:
exact le_sup_left

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g : α →ₘ[μ] β
⊢ ↑f ≤ᶠ[ae μ] ↑(f ⊔ g)

Tactic:
filter_upwards [coeFn_sup f g] with _ ha

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g : α →ₘ[μ] β
a✝ : α
ha : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑f a✝ ≤ ↑(f ⊔ g) a✝