harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/LaurentSeries.lean
theorem derivative_iterate (k : ℕ) (f : LaurentSeries V) :
    (derivative R)^[k] f = k.factorial • (hasseDeriv R k f)

Proof state:
case coeff.h
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((⇑(derivative R))^[k] f).coeff n = (k.factorial • (hasseDeriv R k) f).coeff n

Tactic:
induction k generalizing f with
| zero => simp
| succ k ih =>
  rw [Function.iterate_succ, Function.comp_apply, ih, derivative_apply, hasseDeriv_comp,
    Nat.choose_symm_add, Nat.choose_one_right, Nat.factorial, mul_nsmul]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
⊢ (⇑(derivative R))^[k] f = k.factorial • (hasseDeriv R k) f

Tactic:
ext n

Result:
case coeff.h
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((⇑(derivative R))^[k] f).coeff n = (k.factorial • (hasseDeriv R k) f).coeff n

Proof state:
case coeff.h.succ
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
n : ℤ
k : ℕ
ih : ∀ (f : V⸨X⸩), ((⇑(derivative R))^[k] f).coeff n = (k.factorial • (hasseDeriv R k) f).coeff n
f : V⸨X⸩
⊢ ((⇑(derivative R))^[k + 1] f).coeff n = ((k + 1).factorial • (hasseDeriv R (k + 1)) f).coeff n

Tactic:
rw [Function.iterate_succ, Function.comp_apply, ih, derivative_apply, hasseDeriv_comp,
  Nat.choose_symm_add, Nat.choose_one_right, Nat.factorial, mul_nsmul]

Result:
no goals

Proof state:
case coeff.h.zero
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
n : ℤ
f : V⸨X⸩
⊢ ((⇑(derivative R))^[0] f).coeff n = (Nat.factorial 0 • (hasseDeriv R 0) f).coeff n

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@[simp]
lemma arrowMap_refl {j : J} (F : Set.Iic j ⥤ C) (i : J) (hi : i ≤ j) :
    arrowMap F i i (by simp) hi = Arrow.mk (𝟙 (F.obj ⟨i, hi⟩))

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iic j) ⥤ C
i : J
hi : i ≤ j
⊢ i ≤ i

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iic j) ⥤ C
i : J
hi : i ≤ j
⊢ arrowMap F i i ⋯ hi = Arrow.mk (𝟙 (F.obj ⟨i, hi⟩))

Tactic:
simp [arrowMap]

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
theorem exists_lt_card_nth_eq {x} (h : p x) :
    ∃ n, (∀ hf : (setOf p).Finite, n < #hf.toFinset) ∧ nth p n = x

Proof state:
case refine_2
p : ℕ → Prop
x : ℕ
h : p x
hf : (setOf p).Infinite
⊢ ∃ n, (∀ (hf : (setOf p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
rw [← @Set.mem_setOf_eq _ _ p, ← range_nth_of_infinite hf] at h

Result:
case refine_2
p : ℕ → Prop
x : ℕ
h : x ∈ Set.range (nth p)
hf : (setOf p).Infinite
⊢ ∃ n, (∀ (hf : (setOf p).Finite), n < #hf.toFinset) ∧ nth p n = x

Proof state:
case refine_1.intro.intro
p : ℕ → Prop
x : ℕ
h : p x
hf : (setOf p).Finite
n : ℕ
hn : n < #hf.toFinset
hx : nth p n = x
⊢ ∃ n, (∀ (hf : (setOf p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
exact ⟨n, fun _ => hn, hx⟩

Result:
no goals

Proof state:
p : ℕ → Prop
x : ℕ
h : p x
⊢ ∃ n, (∀ (hf : (setOf p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
refine (setOf p).finite_or_infinite.elim (fun hf => ?_) fun hf => ?_

Result:
case refine_1
p : ℕ → Prop
x : ℕ
h : p x
hf : (setOf p).Finite
⊢ ∃ n, (∀ (hf : (setOf p).Finite), n < #hf.toFinset) ∧ nth p n = x

case refine_2
p : ℕ → Prop
x : ℕ
h : p x
hf : (setOf p).Infinite
⊢ ∃ n, (∀ (hf : (setOf p).Finite), n < #hf.toFinset) ∧ nth p n = x

Proof state:
case refine_2
p : ℕ → Prop
x : ℕ
h : x ∈ Set.range (nth p)
hf : (setOf p).Infinite
⊢ ∃ n, (∀ (hf : (setOf p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
rcases h with ⟨n, hx⟩

Result:
case refine_2.intro
p : ℕ → Prop
x : ℕ
hf : (setOf p).Infinite
n : ℕ
hx : nth p n = x
⊢ ∃ n, (∀ (hf : (setOf p).Finite), n < #hf.toFinset) ∧ nth p n = x

Proof state:
case refine_1
p : ℕ → Prop
x : ℕ
h : p x
hf : (setOf p).Finite
⊢ ∃ n, (∀ (hf : (setOf p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
rcases exists_lt_card_finite_nth_eq hf h with ⟨n, hn, hx⟩

Result:
case refine_1.intro.intro
p : ℕ → Prop
x : ℕ
h : p x
hf : (setOf p).Finite
n : ℕ
hn : n < #hf.toFinset
hx : nth p n = x
⊢ ∃ n, (∀ (hf : (setOf p).Finite), n < #hf.toFinset) ∧ nth p n = x

Proof state:
case refine_2.intro
p : ℕ → Prop
x : ℕ
hf : (setOf p).Infinite
n : ℕ
hx : nth p n = x
⊢ ∃ n, (∀ (hf : (setOf p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
exact ⟨n, fun hf' => absurd hf' hf, hx⟩

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_union_right : image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t'

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
⊢ image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t'

Tactic:
rw [← image2_swap, image2_union_left, image2_swap f, image2_swap f]

Result:
no goals
-- Mathlib/Tactic/Peel.lean
theorem frequently_congr {α : Type*} {p q : α → Prop} {f : Filter α}
    (hq : ∀ (x : α), p x ↔ q x) : (∃ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, q x

Proof state:
α : Type u_1
p q : α → Prop
f : Filter α
hq : ∀ (x : α), p x ↔ q x
⊢ (∃ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, q x

Tactic:
congr! 2

Result:
case a.h.e'_2.h.a
α : Type u_1
p q : α → Prop
f : Filter α
hq : ∀ (x : α), p x ↔ q x
x✝ : α
⊢ p x✝ ↔ q x✝

Proof state:
case a.h.e'_2.h.a
α : Type u_1
p q : α → Prop
f : Filter α
hq : ∀ (x : α), p x ↔ q x
x✝ : α
⊢ p x✝ ↔ q x✝

Tactic:
exact hq _

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem normSq_neg (z : ℂ) : normSq (-z) = normSq z

Proof state:
z : ℂ
⊢ normSq (-z) = normSq z

Tactic:
simp [normSq]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem dist_le_distortion_mul (I : Box ι) (i : ι) :
    dist I.lower I.upper ≤ I.distortion * (I.upper i - I.lower i)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
⊢ dist I.lower I.upper ≤ ↑I.distortion * (I.upper i - I.lower i)

Tactic:
have A : I.lower i - I.upper i < 0 := sub_neg.2 (I.lower_lt_upper i)

Result:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
A : I.lower i - I.upper i < 0
⊢ dist I.lower I.upper ≤ ↑I.distortion * (I.upper i - I.lower i)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
A : I.lower i - I.upper i < 0
⊢ dist I.lower I.upper ≤ ↑I.distortion * (I.upper i - I.lower i)

Tactic:
simpa only [← NNReal.coe_le_coe, ← dist_nndist, NNReal.coe_mul, Real.dist_eq, abs_of_neg A,
  neg_sub] using I.nndist_le_distortion_mul i

Result:
no goals
-- Mathlib/Algebra/Order/Round.lean
theorem round_le_add_half (x : α) : round x ≤ x + 1 / 2

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ ↑(round x) ≤ x + 1 / 2

Tactic:
rw [round_eq x]

Result:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2

Tactic:
exact Int.floor_le (x + 1 / 2)

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_eq_add_tsum_ite {f : α → ℝ≥0} (hf : Summable f) (i : α) :
    ∑' x, f x = f i + ∑' x, ite (x = i) 0 (f x)

Proof state:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ (if i' = i then 0 else f i') ≤ f i'

Tactic:
split_ifs <;> simp only [zero_le', le_rfl]

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ update f i 0 i' ≤ f i'

Tactic:
rw [Function.update_apply]

Result:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ (if i' = i then 0 else f i') ≤ f i'

Proof state:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i : α
⊢ ∑' (x : α), f x = f i + ∑' (x : α), if x = i then 0 else f x

Tactic:
refine tsum_eq_add_tsum_ite' i (NNReal.summable_of_le (fun i' => ?_) hf)

Result:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ update f i 0 i' ≤ f i'
-- Mathlib/Data/Int/CardIntervalMod.lean
lemma Ioc_filter_modEq_eq (v : ℤ) :
    {x ∈ Ioc a b | x ≡ v [ZMOD r]} =
    {x ∈ Ioc (a - v) (b - v) | r ∣ x}.map ⟨(· + v), add_left_injective v⟩

Proof state:
case h
a b r v x : ℤ
⊢ x ∈ filter (fun x => x ≡ v [ZMOD r]) (Ioc a b) ↔
    x ∈ map { toFun := fun x => x + v, inj' := ⋯ } (filter (fun x => r ∣ x) (Ioc (a - v) (b - v)))

Tactic:
simp_rw [mem_map, mem_filter, mem_Ioc, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
  exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]

Result:
no goals

Proof state:
a b r v : ℤ
⊢ filter (fun x => x ≡ v [ZMOD r]) (Ioc a b) =
    map { toFun := fun x => x + v, inj' := ⋯ } (filter (fun x => r ∣ x) (Ioc (a - v) (b - v)))

Tactic:
ext x

Result:
case h
a b r v x : ℤ
⊢ x ∈ filter (fun x => x ≡ v [ZMOD r]) (Ioc a b) ↔
    x ∈ map { toFun := fun x => x + v, inj' := ⋯ } (filter (fun x => r ∣ x) (Ioc (a - v) (b - v)))
-- Mathlib/Data/Int/Bitwise.lean
theorem testBit_lnot : ∀ n k, testBit (lnot n) k = not (testBit n k)
  | (n : ℕ), k => by simp [lnot, testBit]
  | -[n+1], k => by simp [lnot, testBit]

Proof state:
n k : ℕ
⊢ -[n+1].lnot.testBit k = !-[n+1].testBit k

Tactic:
simp [lnot, testBit]

Result:
no goals

Proof state:
n k : ℕ
⊢ (↑n).lnot.testBit k = !(↑n).testBit k

Tactic:
simp [lnot, testBit]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_prod_le (s : Finset ι) (f : ι → E) : ‖∏ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖

Proof state:
case refine_1
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ (⇑Multiplicative.ofAdd ∘ norm) 1 = 1

Tactic:
simp only [comp_apply, norm_one', ofAdd_zero]

Result:
no goals

Proof state:
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ Multiplicative.ofAdd ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, Multiplicative.ofAdd ‖f i‖

Tactic:
refine Finset.le_prod_of_submultiplicative (Multiplicative.ofAdd ∘ norm) ?_ (fun x y => ?_) _ _

Result:
case refine_1
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ (⇑Multiplicative.ofAdd ∘ norm) 1 = 1

case refine_2
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f : ι → E
x y : E
⊢ (⇑Multiplicative.ofAdd ∘ norm) (x * y) ≤ (⇑Multiplicative.ofAdd ∘ norm) x * (⇑Multiplicative.ofAdd ∘ norm) y

Proof state:
case refine_2
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f : ι → E
x y : E
⊢ (⇑Multiplicative.ofAdd ∘ norm) (x * y) ≤ (⇑Multiplicative.ofAdd ∘ norm) x * (⇑Multiplicative.ofAdd ∘ norm) y

Tactic:
exact norm_mul_le' x y

Result:
no goals

Proof state:
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ ‖∏ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖

Tactic:
rw [← Multiplicative.ofAdd_le, ofAdd_sum]

Result:
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ Multiplicative.ofAdd ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, Multiplicative.ofAdd ‖f i‖
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_map (f : α → β) (a : Vector α n) (i : Nat) :
    (a.map f)[i]? = a[i]?.map f

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β
a : Vector α n
i : Nat
⊢ (map f a)[i]? = Option.map f a[i]?

Tactic:
cases a

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (map f { toArray := toArray✝, size_toArray := size_toArray✝ })[i]? =
    Option.map f { toArray := toArray✝, size_toArray := size_toArray✝ }[i]?

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (map f { toArray := toArray✝, size_toArray := size_toArray✝ })[i]? =
    Option.map f { toArray := toArray✝, size_toArray := size_toArray✝ }[i]?

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem rec_heq_of_heq {α β : Sort _} {a b : α} {C : α → Sort*} {x : C a} {y : β}
    (e : a = b) (h : HEq x y) : HEq (e ▸ x) y

Proof state:
α : Sort u_2
β : Sort u_1
a b : α
C : α → Sort u_1
x : C a
y : β
e : a = b
h : HEq x y
⊢ HEq (e ▸ x) y

Tactic:
subst e

Result:
α : Sort u_2
β : Sort u_1
a : α
C : α → Sort u_1
x : C a
y : β
h : HEq x y
⊢ HEq (⋯ ▸ x) y

Proof state:
α : Sort u_2
β : Sort u_1
a : α
C : α → Sort u_1
x : C a
y : β
h : HEq x y
⊢ HEq (⋯ ▸ x) y

Tactic:
exact h

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
lemma MeasurableSet.of_union₃_range_cover (hi₁ : MeasurableEmbedding i₁)
    (hi₂ : MeasurableEmbedding i₂) (hi₃ : MeasurableEmbedding i₃)
    (h : univ ⊆ range i₁ ∪ range i₂ ∪ range i₃) (hs₁ : MeasurableSet (i₁ ⁻¹' s))
    (hs₂ : MeasurableSet (i₂ ⁻¹' s)) (hs₃ : MeasurableSet (i₃ ⁻¹' s)) : MeasurableSet s

Proof state:
α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
α₃ : Type u_8
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
mα₃ : MeasurableSpace α₃
i₁ : α₁ → α
i₂ : α₂ → α
i₃ : α₃ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
hi₃ : MeasurableEmbedding i₃
h : univ ⊆ range i₁ ∪ range i₂ ∪ range i₃
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
hs₃ : MeasurableSet (i₃ ⁻¹' s)
⊢ MeasurableSet s

Tactic:
convert (hi₁.measurableSet_image' hs₁).union (hi₂.measurableSet_image' hs₂) |>.union
  (hi₃.measurableSet_image' hs₃)

Result:
case h.e'_3
α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
α₃ : Type u_8
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
mα₃ : MeasurableSpace α₃
i₁ : α₁ → α
i₂ : α₂ → α
i₃ : α₃ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
hi₃ : MeasurableEmbedding i₃
h : univ ⊆ range i₁ ∪ range i₂ ∪ range i₃
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
hs₃ : MeasurableSet (i₃ ⁻¹' s)
⊢ s = i₁ '' (i₁ ⁻¹' s) ∪ i₂ '' (i₂ ⁻¹' s) ∪ i₃ '' (i₃ ⁻¹' s)

Proof state:
case h.e'_3
α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
α₃ : Type u_8
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
mα₃ : MeasurableSpace α₃
i₁ : α₁ → α
i₂ : α₂ → α
i₃ : α₃ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
hi₃ : MeasurableEmbedding i₃
h : univ ⊆ range i₁ ∪ range i₂ ∪ range i₃
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
hs₃ : MeasurableSet (i₃ ⁻¹' s)
⊢ s = i₁ '' (i₁ ⁻¹' s) ∪ i₂ '' (i₂ ⁻¹' s) ∪ i₃ '' (i₃ ⁻¹' s)

Tactic:
simp [image_preimage_eq_range_inter, ← union_inter_distrib_right, univ_subset_iff.1 h]

Result:
no goals
-- Mathlib/Algebra/Star/Pointwise.lean
theorem star_inv [Group α] [StarMul α] (s : Set α) : s⁻¹⋆ = s⋆⁻¹

Proof state:
case h
α : Type u_1
inst✝¹ : Group α
inst✝ : StarMul α
s : Set α
x✝ : α
⊢ x✝ ∈ s⁻¹⋆ ↔ x✝ ∈ s⋆⁻¹

Tactic:
simp only [mem_star, mem_inv, star_inv]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : StarMul α
s : Set α
⊢ s⁻¹⋆ = s⋆⁻¹

Tactic:
ext

Result:
case h
α : Type u_1
inst✝¹ : Group α
inst✝ : StarMul α
s : Set α
x✝ : α
⊢ x✝ ∈ s⁻¹⋆ ↔ x✝ ∈ s⋆⁻¹
-- Mathlib/Logic/Function/ULift.lean
theorem PLift.down_injective : Function.Injective (@PLift.down α)
  | ⟨a⟩, ⟨b⟩, _ => by congr

Proof state:
α : Sort u_1
a b : α
x✝ : { down := a }.down = { down := b }.down
⊢ { down := a } = { down := b }

Tactic:
congr

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
lemma map_evalRingHom_eval (x y : R) (p : R[X][Y]) :
    (p.map <| evalRingHom x).eval y = p.evalEval x y

Proof state:
R : Type u_1
inst✝ : CommSemiring R
x y : R
p : R[X][Y]
⊢ eval y (map (evalRingHom x) p) = evalEval x y p

Tactic:
rw [eval_map, eval₂_evalRingHom]

Result:
no goals
-- Mathlib/Data/Nat/MaxPowDiv.lean
theorem base_pow_mul {p n exp : ℕ} (hp : 1 < p) (hn : 0 < n) :
    p.maxPowDiv (p ^ exp * n) = p.maxPowDiv n + exp

Proof state:
p n exp : ℕ
hp : 1 < p
hn : 0 < n
e : ℕ
⊢ p.maxPowDiv n + e + 1 = p.maxPowDiv n + (e + 1)

Tactic:
ac_rfl

Result:
no goals

Proof state:
p n exp : ℕ
hp : 1 < p
hn : 0 < n
e : ℕ
⊢ 0 < n * p ^ e

Tactic:
apply Nat.mul_pos hn <| pow_pos (pos_of_gt hp) e

Result:
no goals

Proof state:
p n exp : ℕ
hp : 1 < p
hn : 0 < n
⊢ p.maxPowDiv (p ^ 0 * n) = p.maxPowDiv n + 0

Tactic:
simp

Result:
no goals

Proof state:
p n exp : ℕ
hp : 1 < p
hn : 0 < n
e : ℕ
⊢ p.maxPowDiv (p ^ (e + 1) * n) = p.maxPowDiv n + (e + 1)

Tactic:
rw [Nat.pow_succ, mul_assoc, mul_comm, mul_assoc, base_mul_eq_succ hp, mul_comm,
  base_pow_mul hp hn]

Result:
p n exp : ℕ
hp : 1 < p
hn : 0 < n
e : ℕ
⊢ p.maxPowDiv n + e + 1 = p.maxPowDiv n + (e + 1)

p n exp : ℕ
hp : 1 < p
hn : 0 < n
e : ℕ
⊢ 0 < n * p ^ e
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem minimalPeriod_pos_of_mem_periodicPts (hx : x ∈ periodicPts f) : 0 < minimalPeriod f x

Proof state:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ 0 < minimalPeriod f x

Tactic:
classical
simp only [minimalPeriod, dif_pos hx, (Nat.find_spec hx).1.lt]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ 0 < minimalPeriod f x

Tactic:
simp only [minimalPeriod, dif_pos hx, (Nat.find_spec hx).1.lt]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem sUnion_eq_biUnion {s : Set (Set α)} : ⋃₀ s = ⋃ (i : Set α) (_ : i ∈ s), i

Proof state:
α : Type u_1
s : Set (Set α)
⊢ ⋃₀ s = ⋃ i ∈ s, i

Tactic:
rw [← sUnion_image, image_id']

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem convolution_eq_swap : (f ⋆[L, μ] g) x = ∫ t, L (f (x - t)) (g t) ∂μ

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddCommGroup G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : μ.IsNegInvariant
inst✝¹ : MeasurableNeg G
inst✝ : MeasurableAdd G
⊢ (f ⋆[L, μ] g) x = ∫ (t : G), (L (f (x - t))) (g t) ∂μ

Tactic:
rw [← convolution_flip]

Result:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddCommGroup G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : μ.IsNegInvariant
inst✝¹ : MeasurableNeg G
inst✝ : MeasurableAdd G
⊢ (g ⋆[L.flip, μ] f) x = ∫ (t : G), (L (f (x - t))) (g t) ∂μ

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddCommGroup G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : μ.IsNegInvariant
inst✝¹ : MeasurableNeg G
inst✝ : MeasurableAdd G
⊢ (g ⋆[L.flip, μ] f) x = ∫ (t : G), (L (f (x - t))) (g t) ∂μ

Tactic:
rfl

Result:
no goals
-- Mathlib/ModelTheory/Order.lean
theorem aleph0_categorical_dlo : (ℵ₀).Categorical Language.order.dlo := fun M₁ M₂ h₁ h₂ => by
  obtain ⟨_⟩ := denumerable_iff.2 h₁
  obtain ⟨_⟩ := denumerable_iff.2 h₂
  exact (isFraisseLimit_of_countable_nonempty_dlo M₁).nonempty_equiv
    (isFraisseLimit_of_countable_nonempty_dlo M₂)

Proof state:
case intro.intro
M₁ M₂ : Language.order.dlo.ModelType
h₁ : #↑M₁ = ℵ₀
h₂ : #↑M₂ = ℵ₀
val✝¹ : Denumerable ↑M₁
val✝ : Denumerable ↑M₂
⊢ Nonempty (↑M₁ ≃[Language.order] ↑M₂)

Tactic:
exact (isFraisseLimit_of_countable_nonempty_dlo M₁).nonempty_equiv
  (isFraisseLimit_of_countable_nonempty_dlo M₂)

Result:
no goals

Proof state:
case intro
M₁ M₂ : Language.order.dlo.ModelType
h₁ : #↑M₁ = ℵ₀
h₂ : #↑M₂ = ℵ₀
val✝ : Denumerable ↑M₁
⊢ Nonempty (↑M₁ ≃[Language.order] ↑M₂)

Tactic:
obtain ⟨_⟩ := denumerable_iff.2 h₂

Result:
case intro.intro
M₁ M₂ : Language.order.dlo.ModelType
h₁ : #↑M₁ = ℵ₀
h₂ : #↑M₂ = ℵ₀
val✝¹ : Denumerable ↑M₁
val✝ : Denumerable ↑M₂
⊢ Nonempty (↑M₁ ≃[Language.order] ↑M₂)

Proof state:
M₁ M₂ : Language.order.dlo.ModelType
h₁ : #↑M₁ = ℵ₀
h₂ : #↑M₂ = ℵ₀
⊢ Nonempty (↑M₁ ≃[Language.order] ↑M₂)

Tactic:
obtain ⟨_⟩ := denumerable_iff.2 h₁

Result:
case intro
M₁ M₂ : Language.order.dlo.ModelType
h₁ : #↑M₁ = ℵ₀
h₂ : #↑M₂ = ℵ₀
val✝ : Denumerable ↑M₁
⊢ Nonempty (↑M₁ ≃[Language.order] ↑M₂)
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem norm_eq_of_L2 (x : PiLp 2 β) :
    ‖x‖ = √(∑ i : ι, ‖x i‖ ^ 2)

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ = √(∑ i : ι, ‖x i‖ ^ 2)

Tactic:
rw [norm_eq_of_nat 2 (by norm_cast) _]

Result:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / ↑2) = √(∑ i : ι, ‖x i‖ ^ 2)

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ 2 = ↑2

Tactic:
norm_cast

Result:
no goals

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / ↑2) = √(∑ i : ι, ‖x i‖ ^ 2)

Tactic:
rw [Real.sqrt_eq_rpow]

Result:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / ↑2) = (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / 2)

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / ↑2) = (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / 2)

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem cont_normedSpace_to_withSeminorms (E) [SeminormedAddCommGroup E] [NormedSpace 𝕝 E]
    [TopologicalSpace F] {q : ι → Seminorm 𝕝₂ F} (hq : WithSeminorms q)
    (f : E →ₛₗ[τ₁₂] F) (hf : ∀ i : ι, ∃ C : ℝ≥0, (q i).comp f ≤ C • normSeminorm 𝕝 E) :
    Continuous f

Proof state:
𝕝 : Type u_3
𝕝₂ : Type u_4
F : Type u_6
ι : Type u_8
inst✝⁸ : NormedField 𝕝
inst✝⁷ : AddCommGroup F
inst✝⁶ : NormedField 𝕝₂
inst✝⁵ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁴ : RingHomIsometric τ₁₂
inst✝³ : Nonempty ι
E : Type u_10
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕝 E
inst✝ : TopologicalSpace F
q : ι → Seminorm 𝕝₂ F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded (fun x => normSeminorm 𝕝 E) q f
⊢ Continuous ⇑f

Tactic:
exact continuous_from_bounded (norm_withSeminorms 𝕝 E) hq f hf

Result:
no goals

Proof state:
𝕝 : Type u_3
𝕝₂ : Type u_4
F : Type u_6
ι : Type u_8
inst✝⁸ : NormedField 𝕝
inst✝⁷ : AddCommGroup F
inst✝⁶ : NormedField 𝕝₂
inst✝⁵ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁴ : RingHomIsometric τ₁₂
inst✝³ : Nonempty ι
E : Type u_10
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕝 E
inst✝ : TopologicalSpace F
q : ι → Seminorm 𝕝₂ F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι), ∃ C, (q i).comp f ≤ C • normSeminorm 𝕝 E
⊢ Continuous ⇑f

Tactic:
rw [← Seminorm.const_isBounded (Fin 1)] at hf

Result:
𝕝 : Type u_3
𝕝₂ : Type u_4
F : Type u_6
ι : Type u_8
inst✝⁸ : NormedField 𝕝
inst✝⁷ : AddCommGroup F
inst✝⁶ : NormedField 𝕝₂
inst✝⁵ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁴ : RingHomIsometric τ₁₂
inst✝³ : Nonempty ι
E : Type u_10
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕝 E
inst✝ : TopologicalSpace F
q : ι → Seminorm 𝕝₂ F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded (fun x => normSeminorm 𝕝 E) q f
⊢ Continuous ⇑f