harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/EulerProduct/ExpLog.lean
theorem exp_tsum_primes_log_eq_tsum {f : ℕ →*₀ ℂ} (hsum : Summable (‖f ·‖)) :
    exp (∑' p : Nat.Primes, -log (1 - f p)) = ∑' n : ℕ, f n

Proof state:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
hp : ∀ (p : Nat.Primes), 1 - f ↑p ≠ 0
H :
  ∏' (b : ↑{p | Nat.Prime p}), (cexp ∘ (fun b => -log (1 - f b)) ∘ Subtype.val) b =
    cexp (∑' (b : ↑{p | Nat.Prime p}), ((fun b => -log (1 - f b)) ∘ Subtype.val) b)
⊢ cexp (∑' (p : Nat.Primes), -log (1 - f ↑p)) = ∑' (n : ℕ), f n

Tactic:
simp only [Set.coe_setOf, Set.mem_setOf_eq, Function.comp_apply, exp_neg, exp_log (hp _)] at H

Result:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
hp : ∀ (p : Nat.Primes), 1 - f ↑p ≠ 0
H : ∏' (b : { x // Nat.Prime x }), (1 - f ↑b)⁻¹ = cexp (∑' (b : { x // Nat.Prime x }), -log (1 - f ↑b))
⊢ cexp (∑' (p : Nat.Primes), -log (1 - f ↑p)) = ∑' (n : ℕ), f n

Proof state:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
⊢ cexp (∑' (p : Nat.Primes), -log (1 - f ↑p)) = ∑' (n : ℕ), f n

Tactic:
have hp (p : Nat.Primes) : 1 - f p ≠ 0 :=
  fun h ↦ (norm_one (α := ℂ) ▸ (sub_eq_zero.mp h) ▸ hs p.prop.one_lt).false

Result:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
hp : ∀ (p : Nat.Primes), 1 - f ↑p ≠ 0
⊢ cexp (∑' (p : Nat.Primes), -log (1 - f ↑p)) = ∑' (n : ℕ), f n

Proof state:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
⊢ cexp (∑' (p : Nat.Primes), -log (1 - f ↑p)) = ∑' (n : ℕ), f n

Tactic:
have hs {p : ℕ} (hp : 1 < p) : ‖f p‖ < 1 := hsum.of_norm.norm_lt_one (f := f.toMonoidHom) hp

Result:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
⊢ cexp (∑' (p : Nat.Primes), -log (1 - f ↑p)) = ∑' (n : ℕ), f n

Proof state:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
hp : ∀ (p : Nat.Primes), 1 - f ↑p ≠ 0
⊢ cexp (∑' (p : Nat.Primes), -log (1 - f ↑p)) = ∑' (n : ℕ), f n

Tactic:
have H := hsum.of_norm.clog_one_sub.neg.subtype {p | p.Prime} |>.hasSum.cexp.tprod_eq

Result:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
hp : ∀ (p : Nat.Primes), 1 - f ↑p ≠ 0
H :
  ∏' (b : ↑{p | Nat.Prime p}), (cexp ∘ (fun b => -log (1 - f b)) ∘ Subtype.val) b =
    cexp (∑' (b : ↑{p | Nat.Prime p}), ((fun b => -log (1 - f b)) ∘ Subtype.val) b)
⊢ cexp (∑' (p : Nat.Primes), -log (1 - f ↑p)) = ∑' (n : ℕ), f n

Proof state:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
hp : ∀ (p : Nat.Primes), 1 - f ↑p ≠ 0
H : ∏' (b : { x // Nat.Prime x }), (1 - f ↑b)⁻¹ = cexp (∑' (b : { x // Nat.Prime x }), -log (1 - f ↑b))
⊢ cexp (∑' (p : Nat.Primes), -log (1 - f ↑p)) = ∑' (n : ℕ), f n

Tactic:
exact H.symm.trans <| eulerProduct_completely_multiplicative_tprod hsum

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Convex.lean
theorem convexHull_exists_dist_ge2 {s t : Set E} {x y : E} (hx : x ∈ convexHull ℝ s)
    (hy : y ∈ convexHull ℝ t) : ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'

Proof state:
case right
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y : E
hx : x ∈ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ dist x y ≤ dist x' y'

Tactic:
exact le_trans Hx' (dist_comm y x' ▸ dist_comm y' x' ▸ Hy')

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y : E
hx : x ∈ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) t
⊢ ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'

Tactic:
rcases convexHull_exists_dist_ge hx y with ⟨x', hx', Hx'⟩

Result:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y : E
hx : x ∈ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
⊢ ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'

Proof state:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y : E
hx : x ∈ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
⊢ ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'

Tactic:
rcases convexHull_exists_dist_ge hy x' with ⟨y', hy', Hy'⟩

Result:
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y : E
hx : x ∈ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'

Proof state:
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y : E
hx : x ∈ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'

Tactic:
use x', hx', y', hy'

Result:
case right
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y : E
hx : x ∈ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ dist x y ≤ dist x' y'
-- Mathlib/Data/Finsupp/Basic.lean
theorem mapDomain.addMonoidHom_comp_mapRange [AddCommMonoid N] (f : α → β) (g : M →+ N) :
    (mapDomain.addMonoidHom f).comp (mapRange.addMonoidHom g) =
      (mapRange.addMonoidHom g).comp (mapDomain.addMonoidHom f)

Proof state:
case H.h.h
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
x✝¹ : α
x✝ : M
a✝ : β
⊢ ((((addMonoidHom f).comp (mapRange.addMonoidHom g)).comp (singleAddHom x✝¹)) x✝) a✝ =
    ((((mapRange.addMonoidHom g).comp (addMonoidHom f)).comp (singleAddHom x✝¹)) x✝) a✝

Tactic:
simp only [AddMonoidHom.coe_comp, Finsupp.mapRange_single, Finsupp.mapDomain.addMonoidHom_apply,
  Finsupp.singleAddHom_apply, eq_self_iff_true, Function.comp_apply, Finsupp.mapDomain_single,
  Finsupp.mapRange.addMonoidHom_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
⊢ (addMonoidHom f).comp (mapRange.addMonoidHom g) = (mapRange.addMonoidHom g).comp (addMonoidHom f)

Tactic:
ext

Result:
case H.h.h
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
x✝¹ : α
x✝ : M
a✝ : β
⊢ ((((addMonoidHom f).comp (mapRange.addMonoidHom g)).comp (singleAddHom x✝¹)) x✝) a✝ =
    ((((mapRange.addMonoidHom g).comp (addMonoidHom f)).comp (singleAddHom x✝¹)) x✝) a✝
-- Mathlib/Topology/Instances/Matrix.lean
theorem Matrix.blockDiagonal_tsum [DecidableEq p] [T2Space R] {f : X → p → Matrix m n R} :
    blockDiagonal (∑' x, f x) = ∑' x, blockDiagonal (f x)

Proof state:
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)

Tactic:
by_cases hf : Summable f

Result:
case pos
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : Summable f
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)

case neg
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)

Proof state:
case neg
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal (f x)
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)

Tactic:
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft]

Result:
case neg
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal (f x)
⊢ blockDiagonal 0 = 0

Proof state:
case neg
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal (f x)
⊢ blockDiagonal 0 = 0

Tactic:
exact blockDiagonal_zero

Result:
no goals

Proof state:
case neg
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)

Tactic:
have hft := summable_matrix_blockDiagonal.not.mpr hf

Result:
case neg
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal (f x)
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)

Proof state:
case pos
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : Summable f
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)

Tactic:
exact hf.hasSum.matrix_blockDiagonal.tsum_eq.symm

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma mk₀_comp_mk₀_assoc (f : X ⟶ Y) (g : Y ⟶ Z) {n : ℕ} (α : Ext Z T n) :
    (mk₀ f).comp ((mk₀ g).comp α (zero_add n)) (zero_add n) =
      (mk₀ (f ≫ g)).comp α (zero_add n)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
n : ℕ
α : Ext Z T n
⊢ (mk₀ f).comp ((mk₀ g).comp α ⋯) ⋯ = (mk₀ (f ≫ g)).comp α ⋯

Tactic:
rw [← mk₀_comp_mk₀, comp_assoc]

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
n : ℕ
α : Ext Z T n
⊢ 0 + 0 + n = n

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
n : ℕ
α : Ext Z T n
⊢ 0 + 0 + n = n

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem Nontrivial.preimage {s : Set β} (hs : s.Nontrivial)
    (hf : Function.Surjective f) : (f ⁻¹' s).Nontrivial

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : Surjective f
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
hxy : f x ≠ f y
⊢ (f ⁻¹' s).Nontrivial

Tactic:
exact ⟨x, hx, y, hy, mt (congr_arg f) hxy⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hs : s.Nontrivial
hf : Surjective f
⊢ (f ⁻¹' s).Nontrivial

Tactic:
rcases hs with ⟨fx, hx, fy, hy, hxy⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : Surjective f
fx : β
hx : fx ∈ s
fy : β
hy : fy ∈ s
hxy : fx ≠ fy
⊢ (f ⁻¹' s).Nontrivial

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : Surjective f
fx : β
hx : fx ∈ s
fy : β
hy : fy ∈ s
hxy : fx ≠ fy
⊢ (f ⁻¹' s).Nontrivial

Tactic:
rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : Surjective f
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
hxy : f x ≠ f y
⊢ (f ⁻¹' s).Nontrivial
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
lemma memberSubfamily_image_insert (h𝒜 : ∀ s ∈ 𝒜, a ∉ s) :
    (𝒜.image <| insert a).memberSubfamily a = 𝒜

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
⊢ memberSubfamily a (image (insert a) 𝒜) = 𝒜

Tactic:
ext s

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
⊢ s ∈ memberSubfamily a (image (insert a) 𝒜) ↔ s ∈ 𝒜

Proof state:
case h.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
hs : a ∉ s
t : Finset α
ht : t ∈ 𝒜
hts : insert a t = insert a s
⊢ s ∈ 𝒜

Tactic:
rwa [← insert_erase_invOn.2.injOn (h𝒜 _ ht) hs hts]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
⊢ s ∈ memberSubfamily a (image (insert a) 𝒜) ↔ s ∈ 𝒜

Tactic:
simp only [mem_memberSubfamily, mem_image]

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
⊢ (∃ a_1 ∈ 𝒜, insert a a_1 = insert a s) ∧ a ∉ s ↔ s ∈ 𝒜

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
⊢ (∃ a_1 ∈ 𝒜, insert a a_1 = insert a s) ∧ a ∉ s ↔ s ∈ 𝒜

Tactic:
refine ⟨?_, fun hs ↦ ⟨⟨s, hs, rfl⟩, h𝒜 _ hs⟩⟩

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
⊢ (∃ a_1 ∈ 𝒜, insert a a_1 = insert a s) ∧ a ∉ s → s ∈ 𝒜

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
⊢ (∃ a_1 ∈ 𝒜, insert a a_1 = insert a s) ∧ a ∉ s → s ∈ 𝒜

Tactic:
rintro ⟨⟨t, ht, hts⟩, hs⟩

Result:
case h.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
hs : a ∉ s
t : Finset α
ht : t ∈ 𝒜
hts : insert a t = insert a s
⊢ s ∈ 𝒜
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsPath.transfer (hp) (pp : p.IsPath) :
    (p.transfer H hp).IsPath

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), p✝.IsPath → (p✝.transfer H hp).IsPath
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
pp : (cons h✝ p✝).IsPath
⊢ ((cons h✝ p✝).transfer H hp).IsPath

Tactic:
simp only [Walk.transfer, cons_isPath_iff, support_transfer _ ] at pp ⊢

Result:
case cons
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), p✝.IsPath → (p✝.transfer H hp).IsPath
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
pp : p✝.IsPath ∧ u✝ ∉ p✝.support
⊢ (p✝.transfer H ⋯).IsPath ∧ u✝ ∉ p✝.support

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
u✝ : V
hp : ∀ e ∈ Walk.nil.edges, e ∈ H.edgeSet
pp : Walk.nil.IsPath
⊢ (Walk.nil.transfer H hp).IsPath

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
pp : p.IsPath
⊢ (p.transfer H hp).IsPath

Tactic:
induction p with
| nil => simp
| cons _ _ ih =>
  simp only [Walk.transfer, cons_isPath_iff, support_transfer _ ] at pp ⊢
  exact ⟨ih _ pp.1, pp.2⟩

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), p✝.IsPath → (p✝.transfer H hp).IsPath
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
pp : p✝.IsPath ∧ u✝ ∉ p✝.support
⊢ (p✝.transfer H ⋯).IsPath ∧ u✝ ∉ p✝.support

Tactic:
exact ⟨ih _ pp.1, pp.2⟩

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthInf_le_iff {u : ℕ → ℝ≥0∞} {a : EReal} :
    expGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ n : ℕ in atTop, u n < exp (b * n)

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : n ≥ 1
⊢ (u n).log / ↑n < b ↔ u n < (b * ↑n).exp

Tactic:
rw [EReal.div_lt_iff (by norm_cast) (natCast_ne_top n)]

Result:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : n ≥ 1
⊢ (u n).log < b * ↑n ↔ u n < (b * ↑n).exp

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : n ≥ 1
⊢ 0 < ↑n

Tactic:
norm_cast

Result:
no goals

Proof state:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, (u a).log / ↑a < y) ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n < (b * ↑n).exp

Tactic:
refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Result:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : n ≥ 1
⊢ (u n).log / ↑n < b ↔ u n < (b * ↑n).exp

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : n ≥ 1
⊢ (u n).log < b * ↑n ↔ u n < (b * ↑n).exp

Tactic:
nth_rw 1 [← EReal.log_exp (b * n)]

Result:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : n ≥ 1
⊢ (u n).log < (b * ↑n).exp.log ↔ u n < (b * ↑n).exp

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : n ≥ 1
⊢ (u n).log < (b * ↑n).exp.log ↔ u n < (b * ↑n).exp

Tactic:
exact logOrderIso.lt_iff_lt

Result:
no goals

Proof state:
u : ℕ → ℝ≥0∞
a : EReal
⊢ expGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n < (b * ↑n).exp

Tactic:
rw [expGrowthInf, Filter.liminf_le_iff]

Result:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, (u a).log / ↑a < y) ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n < (b * ↑n).exp
-- Mathlib/GroupTheory/CoprodI.lean
theorem cons_eq_smul {i} {m : M i} {ls h1 h2} :
    cons m ls h1 h2 = of m • ls

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ ls.fstIdx ≠ some i

Tactic:
exact h1

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ cons m ls h1 h2 = of m • ls

Tactic:
rw [of_smul_def, equivPair_eq_of_fstIdx_ne _]

Result:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ cons m ls h1 h2 =
    rcons
      (let __src := { head := 1, tail := ls, fstIdx_ne := ?m.188502 };
      { head := m * { head := 1, tail := ls, fstIdx_ne := ?m.188502 }.head, tail := __src.tail, fstIdx_ne := ⋯ })

ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ ls.fstIdx ≠ some i

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ cons m ls h1 h2 =
    rcons
      (let __src := { head := 1, tail := ls, fstIdx_ne := ?m.188502 };
      { head := m * { head := 1, tail := ls, fstIdx_ne := ?m.188502 }.head, tail := __src.tail, fstIdx_ne := ⋯ })

Tactic:
simp [cons, rcons, h2]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem Monotone.pow_const {f : β → M} (hf : Monotone f) : ∀ n : ℕ, Monotone fun a => f a ^ n
  | 0 => by simpa using monotone_const
  | n + 1 => by
    simp_rw [pow_succ]
    exact (Monotone.pow_const hf _).mul' hf

Proof state:
β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
f : β → M
hf : Monotone f
⊢ Monotone fun a => f a ^ 0

Tactic:
simpa using monotone_const

Result:
no goals

Proof state:
β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone fun a => f a ^ (n + 1)

Tactic:
simp_rw [pow_succ]

Result:
β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone fun a => f a ^ n * f a

Proof state:
β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone fun a => f a ^ n * f a

Tactic:
exact (Monotone.pow_const hf _).mul' hf

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
@[simp]
lemma valuation_natCast (n : ℕ) : valuation (n : ℚ_[p]) = padicValNat p n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (↑n).valuation = ↑(padicValNat p n)

Tactic:
rw [← Rat.cast_natCast, valuation_ratCast, padicValRat.of_nat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findFinIdx?_subtype {p : α → Prop} {l : Vector { x // p x } n}
    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.findFinIdx? f = l.unattach.findFinIdx? g

Proof state:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
l : Array { x // p x }
⊢ findFinIdx? f { toArray := l, size_toArray := ⋯ } = findFinIdx? g { toArray := l, size_toArray := ⋯ }.unattach

Tactic:
simp [hf, Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
p : α → Prop
l : Vector { x // p x } n
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findFinIdx? f l = findFinIdx? g l.unattach

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
l : Array { x // p x }
⊢ findFinIdx? f { toArray := l, size_toArray := ⋯ } = findFinIdx? g { toArray := l, size_toArray := ⋯ }.unattach
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem strictMonoOn_of_deriv_pos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
    (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, 0 < deriv f x) : StrictMonoOn f D

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
⊢ StrictMonoOn f D

Tactic:
intro x hx y hy

Result:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
⊢ x < y → f x < f y

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
this : DifferentiableOn ℝ f (interior D)
⊢ x < y → f x < f y

Tactic:
simpa only [zero_mul, sub_pos] using
  hD.mul_sub_lt_image_sub_of_lt_deriv hf this hf' x hx y hy

Result:
no goals

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
⊢ x < y → f x < f y

Tactic:
have : DifferentiableOn ℝ f (interior D) := fun z hz =>
  (differentiableAt_of_deriv_ne_zero (hf' z hz).ne').differentiableWithinAt

Result:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
this : DifferentiableOn ℝ f (interior D)
⊢ x < y → f x < f y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modifyHead_dropLast {l : List α} {f : α → α} :
    l.dropLast.modifyHead f = (l.modifyHead f).dropLast

Proof state:
case cons
α : Type u_1
f : α → α
a : α
l : List α
⊢ modifyHead f (a :: l).dropLast = (modifyHead f (a :: l)).dropLast

Tactic:
rcases l with _|⟨b, l⟩ <;> simp

Result:
no goals

Proof state:
case nil
α : Type u_1
f : α → α
⊢ modifyHead f [].dropLast = (modifyHead f []).dropLast

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
f : α → α
⊢ modifyHead f l.dropLast = (modifyHead f l).dropLast

Tactic:
rcases l with _|⟨a, l⟩

Result:
case nil
α : Type u_1
f : α → α
⊢ modifyHead f [].dropLast = (modifyHead f []).dropLast

case cons
α : Type u_1
f : α → α
a : α
l : List α
⊢ modifyHead f (a :: l).dropLast = (modifyHead f (a :: l)).dropLast
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem iSup_lt_ord_of_isRegular {ι} {f : ι → Ordinal} {c} (hc : IsRegular c) (hι : #ι < c) :
    (∀ i, f i < c.ord) → iSup f < c.ord :=
  iSup_lt_ord (by rwa [hc.cof_eq])

Proof state:
ι : Type u_1
f : ι → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c.ord.cof

Tactic:
rwa [hc.cof_eq]

Result:
no goals