harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finsupp/Weight.lean
theorem le_weight (w : σ → ℕ) {s : σ} (hs : w s ≠ 0) (f : σ →₀ ℕ) :
    f s ≤ weight w f

Proof state:
case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : f s = 0
⊢ 0 ≤ ∑ x ∈ f.support, f x • w x

Tactic:
apply zero_le

Result:
no goals

Proof state:
case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∉ f.support
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
simp only [not_mem_support_iff] at h

Result:
case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : f s = 0
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Proof state:
case pos
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
rw [Finset.sum_eq_add_sum_diff_singleton h]

Result:
case pos
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ f s ≤ f s • w s + ∑ x ∈ f.support \ {s}, f x • w x

Proof state:
case pos
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ f s ≤ f s • w s + ∑ x ∈ f.support \ {s}, f x • w x

Tactic:
refine le_trans ?_ (Nat.le_add_right _ _)

Result:
case pos
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ f s ≤ f s • w s

Proof state:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
by_cases h : s ∈ f.support

Result:
case pos
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∉ f.support
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Proof state:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
⊢ f s ≤ (weight w) f

Tactic:
simp only [weight_apply, Finsupp.sum]

Result:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Proof state:
case pos
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ f s ≤ f s • w s

Tactic:
apply Nat.le_mul_of_pos_right

Result:
case pos.h
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ 0 < w s

Proof state:
case pos.h
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ 0 < w s

Tactic:
exact Nat.zero_lt_of_ne_zero hs

Result:
no goals

Proof state:
case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : f s = 0
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
rw [h]

Result:
case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : f s = 0
⊢ 0 ≤ ∑ x ∈ f.support, f x • w x
-- Mathlib/Logic/Equiv/Basic.lean
theorem sumCongr_swap_refl {α β : Sort _} [DecidableEq α] [DecidableEq β] (i j : α) :
    Equiv.Perm.sumCongr (Equiv.swap i j) (Equiv.refl β) = Equiv.swap (Sum.inl i) (Sum.inl j)

Proof state:
case H.inr
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
val✝ : β
⊢ ((swap i j).sumCongr (Equiv.refl β)) (Sum.inr val✝) = (swap (Sum.inl i) (Sum.inl j)) (Sum.inr val✝)

Tactic:
simp [Sum.map, swap_apply_of_ne_of_ne]

Result:
no goals

Proof state:
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
⊢ (swap i j).sumCongr (Equiv.refl β) = swap (Sum.inl i) (Sum.inl j)

Tactic:
ext x

Result:
case H
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
x : α ⊕ β
⊢ ((swap i j).sumCongr (Equiv.refl β)) x = (swap (Sum.inl i) (Sum.inl j)) x

Proof state:
case H.inl
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : α
⊢ Sum.inl (if val✝ = i then j else if val✝ = j then i else val✝) =
    if val✝ = i then Sum.inl j else if val✝ = j then Sum.inl i else Sum.inl val✝

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
case H
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
x : α ⊕ β
⊢ ((swap i j).sumCongr (Equiv.refl β)) x = (swap (Sum.inl i) (Sum.inl j)) x

Tactic:
cases x

Result:
case H.inl
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : α
⊢ ((swap i j).sumCongr (Equiv.refl β)) (Sum.inl val✝) = (swap (Sum.inl i) (Sum.inl j)) (Sum.inl val✝)

case H.inr
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
val✝ : β
⊢ ((swap i j).sumCongr (Equiv.refl β)) (Sum.inr val✝) = (swap (Sum.inl i) (Sum.inl j)) (Sum.inr val✝)

Proof state:
case H.inl
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : α
⊢ ((swap i j).sumCongr (Equiv.refl β)) (Sum.inl val✝) = (swap (Sum.inl i) (Sum.inl j)) (Sum.inl val✝)

Tactic:
simp only [Equiv.sumCongr_apply, Sum.map, coe_refl, comp_id, Sum.elim_inl, comp_apply,
  swap_apply_def, Sum.inl.injEq]

Result:
case H.inl
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : α
⊢ Sum.inl (if val✝ = i then j else if val✝ = j then i else val✝) =
    if val✝ = i then Sum.inl j else if val✝ = j then Sum.inl i else Sum.inl val✝
-- Mathlib/Data/Matroid/Closure.lean
lemma subset_closure (M : Matroid α) (X : Set α) (hX : X ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ X ⊆ M.closure X

Tactic:
simp [M.closure_def' X, subset_sInter_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_mapM (f : γ → α → m β) (xs : List α) (hmono : monotone f) :
    monotone (fun x => xs.mapM (f x))

Proof state:
case cons.hmono₂.h.cons.hmono₂
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m β
hmono : monotone f
head✝¹ : α
y : β
head✝ : α
tail✝ : List α
ih : ∀ (ys : List β), monotone fun x => List.mapM.loop (f x) tail✝ ys
ys : List β
⊢ monotone fun x __do_lift => List.mapM.loop (f x) tail✝ (__do_lift :: ys)

Tactic:
apply monotone_of_monotone_apply

Result:
case cons.hmono₂.h.cons.hmono₂.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m β
hmono : monotone f
head✝¹ : α
y : β
head✝ : α
tail✝ : List α
ih : ∀ (ys : List β), monotone fun x => List.mapM.loop (f x) tail✝ ys
ys : List β
⊢ ∀ (y : β), monotone fun x => List.mapM.loop (f x) tail✝ (y :: ys)

Proof state:
case cons.hmono₂.h.nil
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m β
hmono : monotone f
head✝ : α
y : β
ys : List β
⊢ monotone fun x => List.mapM.loop (f x) [] ys

Tactic:
apply monotone_const

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem Collinear.coplanar_insert {s : Set P} (h : Collinear k s) (p : P) :
    Coplanar k (insert p s)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional k ↥(vectorSpan k s)
⊢ finrank k ↥(vectorSpan k (insert p s)) ≤ 2

Tactic:
exact (finrank_vectorSpan_insert_le_set k s p).trans (add_le_add_right h.finrank_le_one _)

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional k ↥(vectorSpan k s)
⊢ Coplanar k (insert p s)

Tactic:
rw [coplanar_iff_finrank_le_two]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional k ↥(vectorSpan k s)
⊢ finrank k ↥(vectorSpan k (insert p s)) ≤ 2

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p : P
⊢ Coplanar k (insert p s)

Tactic:
have : FiniteDimensional k { x // x ∈ vectorSpan k s } := h.finiteDimensional_vectorSpan

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional k ↥(vectorSpan k s)
⊢ Coplanar k (insert p s)
-- Mathlib/Algebra/Group/Embedding.lean
theorem mulLeftEmbedding_eq_mulRightEmbedding [CommSemigroup G] [IsCancelMul G] (g : G) :
    mulLeftEmbedding g = mulRightEmbedding g

Proof state:
case h
G : Type u_1
inst✝¹ : CommSemigroup G
inst✝ : IsCancelMul G
g x✝ : G
⊢ (mulLeftEmbedding g) x✝ = (mulRightEmbedding g) x✝

Tactic:
exact mul_comm _ _

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : CommSemigroup G
inst✝ : IsCancelMul G
g : G
⊢ mulLeftEmbedding g = mulRightEmbedding g

Tactic:
ext

Result:
case h
G : Type u_1
inst✝¹ : CommSemigroup G
inst✝ : IsCancelMul G
g x✝ : G
⊢ (mulLeftEmbedding g) x✝ = (mulRightEmbedding g) x✝
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsMatching.subgraphOfAdj (h : G.Adj v w) : (G.subgraphOfAdj h).IsMatching

Proof state:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
⊢ (G.subgraphOfAdj h).IsMatching

Tactic:
intro _ hv

Result:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
hv : v✝ ∈ (G.subgraphOfAdj h).verts
⊢ ∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1

Proof state:
case inl
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
h✝ : v✝ = v
⊢ ∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1

Tactic:
use w

Result:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
h✝ : v✝ = v
⊢ (fun w_1 => (G.subgraphOfAdj h).Adj v✝ w_1) w ∧ ∀ (y : V), (fun w_1 => (G.subgraphOfAdj h).Adj v✝ w_1) y → y = w

Proof state:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
hv : v✝ = v ∨ v✝ = w
⊢ ∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1

Tactic:
cases hv with
| inl => use w; aesop
| inr => use v; aesop

Result:
no goals

Proof state:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
h✝ : v✝ = v
⊢ (fun w_1 => (G.subgraphOfAdj h).Adj v✝ w_1) w ∧ ∀ (y : V), (fun w_1 => (G.subgraphOfAdj h).Adj v✝ w_1) y → y = w

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
hv : v✝ ∈ (G.subgraphOfAdj h).verts
⊢ ∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1

Tactic:
rw [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at hv

Result:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
hv : v✝ = v ∨ v✝ = w
⊢ ∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1

Proof state:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
h✝ : v✝ = w
⊢ (fun w_1 => (G.subgraphOfAdj h).Adj v✝ w_1) v ∧ ∀ (y : V), (fun w_1 => (G.subgraphOfAdj h).Adj v✝ w_1) y → y = v

Tactic:
aesop

Result:
no goals

Proof state:
case inr
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
h✝ : v✝ = w
⊢ ∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1

Tactic:
use v

Result:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
h✝ : v✝ = w
⊢ (fun w_1 => (G.subgraphOfAdj h).Adj v✝ w_1) v ∧ ∀ (y : V), (fun w_1 => (G.subgraphOfAdj h).Adj v✝ w_1) y → y = v
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_X_pow_eq_smul (n : ℕ) (k : ℕ) :
    derivative^[k] (X ^ n : R[X]) = (Nat.descFactorial n k : R) • X ^ (n - k)

Proof state:
R : Type u
inst✝ : CommSemiring R
n k : ℕ
⊢ (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) • X ^ (n - k)

Tactic:
rw [iterate_derivative_X_pow_eq_C_mul n k, smul_eq_C_mul]

Result:
no goals
-- Mathlib/RingTheory/Norm/Transitivity.lean
lemma polyToMatrix_cornerAddX :
    f.polyToMatrix (cornerAddX M k k k) = (-f (M k k)).charmatrix

Proof state:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁴ : CommRing R
inst✝³ : CommRing S
M : Matrix m m S
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
k : m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ f.polyToMatrix (cornerAddX M k k k) = (-f (M k k)).charmatrix

Tactic:
simp [cornerAddX, Matrix.add_apply, charmatrix,
  RingHom.polyToMatrix, ← AlgEquiv.symm_toRingEquiv, map_neg]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_erase_eq_div {a : α} (h : a ∈ s) :
    ∏ x ∈ s.erase a, f x = (∏ x ∈ s, f x) / f a

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommGroup β
inst✝ : DecidableEq α
a : α
h : a ∈ s
⊢ ∏ x ∈ s.erase a, f x = (∏ x ∈ s, f x) / f a

Tactic:
rw [eq_div_iff_mul_eq', prod_erase_mul _ _ h]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProd_restrict {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) :
    Kernel.restrict κ hs ⊗ₖ Kernel.restrict η ht = Kernel.restrict (κ ⊗ₖ η) (hs.prod ht)

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
⊢ ∫⁻ (b : β), ((η.restrict ht) (a, b)) {c | (b, c) ∈ u} ∂(κ.restrict hs) a =
    ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ u ∩ s ×ˢ t} ∂κ a

Tactic:
simp only [Kernel.restrict_apply, Measure.restrict_apply' ht, Set.mem_inter_iff,
  Set.prod_mk_mem_set_prod_eq]

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
⊢ ∫⁻ (b : β) in s, (η (a, b)) ({c | (b, c) ∈ u} ∩ t) ∂κ a = ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ κ.restrict hs ⊗ₖ η.restrict ht = (κ ⊗ₖ η).restrict ⋯

Tactic:
ext a u hu

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
⊢ ((κ.restrict hs ⊗ₖ η.restrict ht) a) u = (((κ ⊗ₖ η).restrict ⋯) a) u
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_mkArray {a b : α} {n} : b ∈ mkArray n a ↔ n ≠ 0 ∧ b = a

Proof state:
α : Type u_1
a b : α
n : Nat
⊢ b ∈ { toList := List.replicate n a } ↔ n ≠ 0 ∧ b = a

Tactic:
simp only [mem_toArray, List.mem_replicate]

Result:
no goals

Proof state:
α : Type u_1
a b : α
n : Nat
⊢ b ∈ mkArray n a ↔ n ≠ 0 ∧ b = a

Tactic:
unfold mkArray

Result:
α : Type u_1
a b : α
n : Nat
⊢ b ∈ { toList := List.replicate n a } ↔ n ≠ 0 ∧ b = a
-- Mathlib/Control/Fold.lean
theorem foldlm.ofFreeMonoid_comp_of {m} [Monad m] [LawfulMonad m] (f : α → β → m α) :
    foldlM.ofFreeMonoid f ∘ FreeMonoid.of = foldlM.mk ∘ flip f

Proof state:
α β : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
⊢ ⇑(foldlM.ofFreeMonoid f) ∘ FreeMonoid.of = foldlM.mk ∘ flip f

Tactic:
ext1 x

Result:
case h
α β : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : β
⊢ (⇑(foldlM.ofFreeMonoid f) ∘ FreeMonoid.of) x = (foldlM.mk ∘ flip f) x

Proof state:
case h
α β : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : β
⊢ (fun a => f a x) = fun a => f a x

Tactic:
rfl

Result:
no goals

Proof state:
case h
α β : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : β
⊢ (⇑(foldlM.ofFreeMonoid f) ∘ FreeMonoid.of) x = (foldlM.mk ∘ flip f) x

Tactic:
simp only [foldlM.ofFreeMonoid, Function.flip_def, MonoidHom.coe_mk, OneHom.coe_mk,
  Function.comp_apply, FreeMonoid.toList_of, List.foldlM_cons, List.foldlM_nil, bind_pure,
  foldlM.mk, op_inj]

Result:
case h
α β : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : β
⊢ (fun a => f a x) = fun a => f a x
-- Mathlib/GroupTheory/Order/Min.lean
@[simp]
protected lemma minOrder {n : ℕ} (hn : n ≠ 0) (hn₁ : n ≠ 1) : minOrder (ZMod n) = n.minFac

Proof state:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
⊢ minOrder (ZMod n) = ↑n.minFac

Tactic:
have : Fact (1 < n) := ⟨one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn, hn₁⟩⟩

Result:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
⊢ minOrder (ZMod n) = ↑n.minFac

Proof state:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
⊢ ↑(n / n.minFac) ≠ 0

Tactic:
rw [Ne, ringChar.spec, ringChar.eq (ZMod n) n]

Result:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
⊢ ¬n ∣ n / n.minFac

Proof state:
case refine_1
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
⊢ ↑(Nat.card ↥(zmultiples ↑(n / n.minFac))) ≤ ↑n.minFac

Tactic:
rw [Nat.card_zmultiples, ZMod.addOrderOf_coe _ hn,
  gcd_eq_right (div_dvd_of_dvd n.minFac_dvd), Nat.div_div_self n.minFac_dvd hn]

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
⊢ minOrder (ZMod n) = ↑n.minFac

Tactic:
refine ((minOrder_le_natCard (zmultiples_eq_bot.not.2 this) <| toFinite _).trans ?_).antisymm <|
  le_minOrder_iff_forall_addSubgroup.2 fun s hs _ ↦ ?_

Result:
case refine_1
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
⊢ ↑(Nat.card ↥(zmultiples ↑(n / n.minFac))) ≤ ↑n.minFac

case refine_2
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
s : AddSubgroup (ZMod n)
hs : s ≠ ⊥
x✝ : (↑s).Finite
⊢ ↑n.minFac ≤ ↑(Nat.card ↥s)

Proof state:
case refine_2
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
s : AddSubgroup (ZMod n)
hs : s ≠ ⊥
x✝ : (↑s).Finite
⊢ ↑n.minFac ≤ ↑(Nat.card ↥s)

Tactic:
haveI : Nontrivial s := s.bot_or_nontrivial.resolve_left hs

Result:
case refine_2
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝¹ : Fact (1 < n)
this✝ : ↑(n / n.minFac) ≠ 0
s : AddSubgroup (ZMod n)
hs : s ≠ ⊥
x✝ : (↑s).Finite
this : Nontrivial ↥s
⊢ ↑n.minFac ≤ ↑(Nat.card ↥s)

Proof state:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
⊢ ¬n ∣ n / n.minFac

Tactic:
exact
  not_dvd_of_pos_of_lt (Nat.div_pos (minFac_le hn.bot_lt) n.minFac_pos)
    (div_lt_self hn.bot_lt (minFac_prime hn₁).one_lt)

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
⊢ minOrder (ZMod n) = ↑n.minFac

Tactic:
have : (↑(n / n.minFac) : ZMod n) ≠ 0 := by
  rw [Ne, ringChar.spec, ringChar.eq (ZMod n) n]
  exact
    not_dvd_of_pos_of_lt (Nat.div_pos (minFac_le hn.bot_lt) n.minFac_pos)
      (div_lt_self hn.bot_lt (minFac_prime hn₁).one_lt)

Result:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
⊢ minOrder (ZMod n) = ↑n.minFac

Proof state:
case refine_2
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝¹ : Fact (1 < n)
this✝ : ↑(n / n.minFac) ≠ 0
s : AddSubgroup (ZMod n)
hs : s ≠ ⊥
x✝ : (↑s).Finite
this : Nontrivial ↥s
⊢ ↑n.minFac ≤ ↑(Nat.card ↥s)

Tactic:
exact WithTop.coe_le_coe.2 <| minFac_le_of_dvd Finite.one_lt_card <|
  (card_addSubgroup_dvd_card _).trans n.card_zmod.dvd

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem countable_preimage_exp {s : Set ℂ} : (exp ⁻¹' s).Countable ↔ s.Countable

Proof state:
s : Set ℂ
⊢ (cexp ⁻¹' s).Countable ↔ s.Countable

Tactic:
refine ⟨fun hs => ?_, fun hs => ?_⟩

Result:
case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s.Countable

case refine_2
s : Set ℂ
hs : s.Countable
⊢ (cexp ⁻¹' s).Countable

Proof state:
case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ s ∪ {0}

Tactic:
exact Set.subset_union_left

Result:
no goals

Proof state:
case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s.Countable

Tactic:
refine ((hs.image exp).insert 0).mono ?_

Result:
case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ insert 0 (cexp '' (cexp ⁻¹' s))

Proof state:
case refine_2
s : Set ℂ
hs : s.Countable
⊢ (cexp ⁻¹' s).Countable

Tactic:
rw [← Set.biUnion_preimage_singleton]

Result:
case refine_2
s : Set ℂ
hs : s.Countable
⊢ (⋃ y ∈ s, cexp ⁻¹' {y}).Countable

Proof state:
case refine_2.inl.intro
s : Set ℂ
hs : s.Countable
w : ℂ
hz : cexp w ∈ s
⊢ (cexp ⁻¹' {cexp w}).Countable

Tactic:
simp only [Set.preimage, Set.mem_singleton_iff, exp_eq_exp_iff_exists_int, Set.setOf_exists]

Result:
case refine_2.inl.intro
s : Set ℂ
hs : s.Countable
w : ℂ
hz : cexp w ∈ s
⊢ (⋃ i, {x | x = w + ↑i * (2 * ↑π * I)}).Countable

Proof state:
case refine_2.inl.intro
s : Set ℂ
hs : s.Countable
w : ℂ
hz : cexp w ∈ s
⊢ (⋃ i, {x | x = w + ↑i * (2 * ↑π * I)}).Countable

Tactic:
exact Set.countable_iUnion fun m => Set.countable_singleton _

Result:
no goals

Proof state:
case refine_2
s : Set ℂ
hs : s.Countable
⊢ (⋃ y ∈ s, cexp ⁻¹' {y}).Countable

Tactic:
refine hs.biUnion fun z hz => ?_

Result:
case refine_2
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
⊢ (cexp ⁻¹' {z}).Countable

Proof state:
case refine_2
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
⊢ (cexp ⁻¹' {z}).Countable

Tactic:
rcases em (∃ w, exp w = z) with (⟨w, rfl⟩ | hne)

Result:
case refine_2.inl.intro
s : Set ℂ
hs : s.Countable
w : ℂ
hz : cexp w ∈ s
⊢ (cexp ⁻¹' {cexp w}).Countable

case refine_2.inr
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
hne : ¬∃ w, cexp w = z
⊢ (cexp ⁻¹' {z}).Countable

Proof state:
case refine_2.inr
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
hne : ∀ (w : ℂ), cexp w ≠ z
⊢ (cexp ⁻¹' {z}).Countable

Tactic:
simp [Set.preimage, hne]

Result:
no goals

Proof state:
case refine_2.inr
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
hne : ¬∃ w, cexp w = z
⊢ (cexp ⁻¹' {z}).Countable

Tactic:
push_neg at hne

Result:
case refine_2.inr
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
hne : ∀ (w : ℂ), cexp w ≠ z
⊢ (cexp ⁻¹' {z}).Countable

Proof state:
case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ insert 0 (cexp '' (cexp ⁻¹' s))

Tactic:
rw [Set.image_preimage_eq_inter_range, range_exp, ← Set.diff_eq, ← Set.union_singleton,
    Set.diff_union_self]

Result:
case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ s ∪ {0}
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem recF_eq {α : Type _} (g : F α → α) (x : q.P.W) :
    recF g x = g (abs (q.P.map (recF g) x.dest))

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : (P F).W
⊢ recF g x = g (abs ((P F).map (recF g) x.dest))

Tactic:
cases x

Result:
case mk
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
a✝ : (P F).A
f✝ : (P F).B a✝ → WType (P F).B
⊢ recF g (WType.mk a✝ f✝) = g (abs ((P F).map (recF g) (PFunctor.W.dest (WType.mk a✝ f✝))))

Proof state:
case mk
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
a✝ : (P F).A
f✝ : (P F).B a✝ → WType (P F).B
⊢ recF g (WType.mk a✝ f✝) = g (abs ((P F).map (recF g) (PFunctor.W.dest (WType.mk a✝ f✝))))

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi
    (hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x)
    (f'int : IntegrableOn f' (Ioi a)) (fint : IntegrableOn f (Ioi a)) :
    Tendsto f atTop (𝓝 0)

Proof state:
case intro
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
fint : IntegrableOn f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (limUnder atTop (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atTop volume
s : Set ℝ
hs : s ∈ atTop
b : ℝ
hb : ∀ b_1 ≥ b, b_1 ∈ s
⊢ volume s = ⊤

Tactic:
rw [← top_le_iff, ← volume_Ici (a := b)]

Result:
case intro
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
fint : IntegrableOn f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (limUnder atTop (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atTop volume
s : Set ℝ
hs : s ∈ atTop
b : ℝ
hb : ∀ b_1 ≥ b, b_1 ∈ s
⊢ volume (Ici b) ≤ volume s