harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Union.lean
@[simp, norm_cast]
lemma coe_biUnion : (s.biUnion t : Set β) = ⋃ x ∈ (s : Set α), t x

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ ↑(s.biUnion t) = ⋃ x ∈ ↑s, ↑(t x)

Tactic:
simp [Set.ext_iff, mem_biUnion, Set.mem_iUnion, mem_coe, imp_true_iff]

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
lemma UniformConcaveOn.strictConcaveOn (hf : UniformConcaveOn s φ f) (hφ : ∀ r, r ≠ 0 → 0 < φ r) :
    StrictConcaveOn ℝ s f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * b * φ ‖x - y‖

Tactic:
rw [← sub_ne_zero, ← norm_pos_iff] at hxy

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : 0 < ‖x - y‖
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * b * φ ‖x - y‖

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : 0 < ‖x - y‖
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * b * φ ‖x - y‖

Tactic:
have := hφ _ hxy.ne'

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : 0 < ‖x - y‖
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
this : 0 < φ ‖x - y‖
⊢ 0 < a * b * φ ‖x - y‖

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : 0 < ‖x - y‖
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
this : 0 < φ ‖x - y‖
⊢ 0 < a * b * φ ‖x - y‖

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
⊢ StrictConcaveOn ℝ s f

Tactic:
refine ⟨hf.1, fun x hx y hy hxy a b ha hb hab ↦ (hf.2 hx hy ha.le hb.le hab).trans_lt' <|
  lt_add_of_pos_right _ ?_⟩

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * b * φ ‖x - y‖
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem disjoint_sSup_iff {s : Set α} : Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b

Proof state:
α : Type u
inst✝ : Frame α
a : α
s : Set α
⊢ Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b

Tactic:
simpa only [disjoint_comm] using @sSup_disjoint_iff

Result:
no goals
-- Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean
theorem dist_birkhoffAverage_birkhoffAverage (f : α → α) (g : α → E) (n : ℕ) (x y : α) :
    dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) =
      dist (birkhoffSum f g n x) (birkhoffSum f g n y) / n

Proof state:
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : α → α
g : α → E
n : ℕ
x y : α
⊢ dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) = dist (birkhoffSum f g n x) (birkhoffSum f g n y) / ↑n

Tactic:
simp [birkhoffAverage, dist_smul₀, div_eq_inv_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem isUnit_map [Field k] (f : R →+* k) : IsUnit (p.map f) ↔ IsUnit p

Proof state:
R : Type u
k : Type y
inst✝¹ : Field R
p : R[X]
inst✝ : Field k
f : R →+* k
⊢ IsUnit (map f p) ↔ IsUnit p

Tactic:
simp_rw [isUnit_iff_degree_eq_zero, degree_map]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_norm_rpow (f : α → F) (p q : ℝ) (hq_pos : 0 < q) :
    eLpNorm' (fun x => ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ eLpNorm' (fun x => ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q

Tactic:
simp_rw [eLpNorm', ← ENNReal.rpow_mul, ← one_div_mul_one_div, one_div,
  mul_assoc, inv_mul_cancel₀ hq_pos.ne.symm, mul_one, ← ofReal_norm_eq_enorm,
  Real.norm_eq_abs, abs_eq_self.mpr (Real.rpow_nonneg (norm_nonneg _) _), mul_comm p,
  ← ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hq_pos.le, ENNReal.rpow_mul]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem ext₁ [TopologicalSpace R₁] {f g : R₁ ≃L[R₁] M₁} (h : f 1 = g 1) : f = g :=
  ext <| funext fun x => mul_one x ▸ by rw [← smul_eq_mul, map_smul, h, map_smul]

Proof state:
R₁ : Type u_3
inst✝⁴ : Semiring R₁
M₁ : Type u_6
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
inst✝ : TopologicalSpace R₁
f g : R₁ ≃L[R₁] M₁
h : f 1 = g 1
x : R₁
⊢ f (x * 1) = g (x * 1)

Tactic:
rw [← smul_eq_mul, map_smul, h, map_smul]

Result:
no goals
-- Mathlib/Data/Int/Sqrt.lean
theorem sqrt_natCast (n : ℕ) : Int.sqrt (n : ℤ) = Nat.sqrt n

Proof state:
n : ℕ
⊢ sqrt ↑n = ↑n.sqrt

Tactic:
rw [sqrt, toNat_ofNat]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive (attr := simp) enorm_eq_zero]
lemma enorm_eq_zero' : ‖a‖ₑ = 0 ↔ a = 1

Proof state:
E : Type u_5
inst✝ : NormedGroup E
a : E
⊢ ‖a‖ₑ = 0 ↔ a = 1

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem infinite_pigeonhole_card_lt {β α : Type u} (f : β → α) (w : #α < #β) (w' : ℵ₀ ≤ #α) :
    ∃ a : α, #α < #(f ⁻¹' {a})

Proof state:
β α : Type u
f : β → α
w : #α < #β
w' : ℵ₀ ≤ #α
⊢ ∃ a, succ #α ≤ #↑(f ⁻¹' {a})

Tactic:
exact
  Ordinal.infinite_pigeonhole_card f (succ #α) (succ_le_of_lt w) (w'.trans (lt_succ _).le)
    ((lt_succ _).trans_le (isRegular_succ w').2.ge)

Result:
no goals

Proof state:
β α : Type u
f : β → α
w : #α < #β
w' : ℵ₀ ≤ #α
⊢ ∃ a, #α < #↑(f ⁻¹' {a})

Tactic:
simp_rw [← succ_le_iff]

Result:
β α : Type u
f : β → α
w : #α < #β
w' : ℵ₀ ≤ #α
⊢ ∃ a, succ #α ≤ #↑(f ⁻¹' {a})
-- Mathlib/Data/Int/Bitwise.lean
theorem bodd_negOfNat (n : ℕ) : bodd (negOfNat n) = n.bodd

Proof state:
case succ
n✝ : ℕ
⊢ (negOfNat (n✝ + 1)).bodd = !n✝.bodd

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ (negOfNat n).bodd = n.bodd

Tactic:
cases n <;> simp +decide

Result:
case succ
n✝ : ℕ
⊢ (negOfNat (n✝ + 1)).bodd = !n✝.bodd
-- Mathlib/Algebra/AddTorsor/Basic.lean
theorem singleton_vsub_self (p : P) : ({p} : Set P) -ᵥ {p} = {(0 : G)}

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p : P
⊢ {p} -ᵥ {p} = {0}

Tactic:
rw [Set.singleton_vsub_singleton, vsub_self]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem associated_eq_self_apply (x : M) : associatedHom S Q x x = Q x

Proof state:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x : M
⊢ (((associatedHom S) Q) x) x = Q x

Tactic:
rw [associated_apply, map_add_self, ← three_add_one_eq_four, ← two_add_one_eq_three, add_smul,
  add_smul, one_smul, add_sub_cancel_right, add_sub_cancel_right, two_smul, ← two_smul R,
  invOf_smul_eq_iff, two_smul, two_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem mem_range {m n : Nat} : m ∈ range n ↔ m < n

Proof state:
m n : Nat
⊢ m ∈ range n ↔ m < n

Tactic:
simp only [range_eq_range', mem_range'_1, Nat.zero_le, true_and, Nat.zero_add]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_C {a : R} : derivative (C a) = 0

Proof state:
R : Type u
inst✝ : Semiring R
a : R
⊢ derivative (C a) = 0

Tactic:
simp [derivative_apply]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem nndist_equiv_symm_single_same (i : ι) (b₁ b₂ : β i) :
    nndist
        ((WithLp.equiv p (∀ i, β i)).symm (Pi.single i b₁))
        ((WithLp.equiv p (∀ i, β i)).symm (Pi.single i b₂)) =
      nndist b₁ b₂

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b₁ b₂ : β i
⊢ nndist ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₁))
      ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₂)) =
    nndist b₁ b₂

Tactic:
rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← WithLp.equiv_symm_sub, ← Pi.single_sub,
  nnnorm_equiv_symm_single]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
theorem contMDiffAt_prod_module_iff (f : M → F₁ × F₂) :
    ContMDiffAt I 𝓘(𝕜, F₁ × F₂) n f x ↔
      ContMDiffAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) x

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffAt I 𝓘(𝕜, F₁ × F₂) n f x ↔
    ContMDiffAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) x

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

Result:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffAt I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) n f x ↔
    ContMDiffAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) x

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffAt I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) n f x ↔
    ContMDiffAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) x

Tactic:
exact contMDiffAt_prod_iff f

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attach_ne_empty_iff {l : Array α} : l.attach ≠ #[] ↔ l ≠ #[]

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.attach ≠ #[] ↔ { toList := toList✝ } ≠ #[]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : Array α
⊢ l.attach ≠ #[] ↔ l ≠ #[]

Tactic:
cases l

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.attach ≠ #[] ↔ { toList := toList✝ } ≠ #[]
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem update_zero_eq_erase (p : R[X]) (n : ℕ) : p.update n 0 = p.erase n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.update n 0 = erase n p

Tactic:
ext

Result:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ (p.update n 0).coeff n✝ = (erase n p).coeff n✝

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ (p.update n 0).coeff n✝ = (erase n p).coeff n✝

Tactic:
rw [coeff_update_apply, coeff_erase]

Result:
no goals
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem equiv_comp_equiv_apply_eq_self (x : L) :
    equiv j i p (equiv i j p x) = x

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing K
inst✝⁸ : CommRing L
inst✝⁷ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝⁶ : ExpChar M p
inst✝⁵ : ExpChar K p
inst✝⁴ : ExpChar L p
inst✝³ : PerfectRing L p
inst✝² : IsPerfectClosure i p
inst✝¹ : PerfectRing M p
inst✝ : IsPerfectClosure j p
x : L
⊢ (equiv j i p) ((equiv i j p) x) = x

Tactic:
rw [equiv_comp_equiv_apply, equiv_self_apply]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/PowerSeries.lean
theorem ofPowerSeries_apply_coeff (x : PowerSeries R) (n : ℕ) :
    (ofPowerSeries Γ R x).coeff n = PowerSeries.coeff R n x

Proof state:
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
x : PowerSeries R
n : ℕ
⊢ ((ofPowerSeries Γ R) x).coeff ↑n = (PowerSeries.coeff R n) x

Tactic:
simp [ofPowerSeries_apply]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem continuousAt_zero_of_forall' [TopologicalSpace E] {p : Seminorm 𝕝 E}
    (hp : ∀ r > 0, p.closedBall 0 r ∈ (𝓝 0 : Filter E)) :
    ContinuousAt p 0

Proof state:
𝕝 : Type u_6
E : Type u_7
inst✝³ : SeminormedRing 𝕝
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕝 E
inst✝ : TopologicalSpace E
p : Seminorm 𝕝 E
hp : ∀ r > 0, ⇑p ⁻¹' Metric.closedBall 0 r ∈ 𝓝 0
⊢ ContinuousAt (⇑p) 0

Tactic:
rwa [ContinuousAt, Metric.nhds_basis_closedBall.tendsto_right_iff, map_zero]

Result:
no goals

Proof state:
𝕝 : Type u_6
E : Type u_7
inst✝³ : SeminormedRing 𝕝
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕝 E
inst✝ : TopologicalSpace E
p : Seminorm 𝕝 E
hp : ∀ r > 0, p.closedBall 0 r ∈ 𝓝 0
⊢ ContinuousAt (⇑p) 0

Tactic:
simp_rw [Seminorm.closedBall_zero_eq_preimage_closedBall] at hp

Result:
𝕝 : Type u_6
E : Type u_7
inst✝³ : SeminormedRing 𝕝
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕝 E
inst✝ : TopologicalSpace E
p : Seminorm 𝕝 E
hp : ∀ r > 0, ⇑p ⁻¹' Metric.closedBall 0 r ∈ 𝓝 0
⊢ ContinuousAt (⇑p) 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem sum_replicate_nat (n : Nat) (a : Nat) : (replicate n a).sum = n * a

Proof state:
n a : Nat
⊢ (replicate n a).sum = n * a

Tactic:
induction n <;> simp_all [replicate_succ, Nat.add_mul, Nat.add_comm]

Result:
no goals
-- Mathlib/Combinatorics/Additive/CovBySMul.lean
@[to_additive]
lemma CovBySMul.subset_left (hA : A₁ ⊆ A₂) (hAB : CovBySMul M K A₂ B) :
    CovBySMul M K A₁ B

Proof state:
M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
K : ℝ
A₁ A₂ B : Set X
hA : A₁ ⊆ A₂
hAB : CovBySMul M K A₂ B
⊢ CovBySMul M K A₁ B

Tactic:
simpa using (CovBySMul.of_subset (M := M) hA).trans hAB

Result:
no goals
-- Mathlib/Data/Set/List.lean
theorem range_list_map_coe (s : Set α) : range (map ((↑) : s → α)) = { l | ∀ x ∈ l, x ∈ s }

Proof state:
α : Type u_1
s : Set α
⊢ range (map Subtype.val) = {l | ∀ x ∈ l, x ∈ s}

Tactic:
rw [range_list_map, Subtype.range_coe]

Result:
no goals
-- Mathlib/Algebra/Prime/Defs.lean
theorem Irreducible.dvd_symm [Monoid M] {p q : M} (hp : Irreducible p) (hq : Irreducible q) :
    p ∣ q → q ∣ p

Proof state:
M : Type u_1
inst✝ : Monoid M
p q : M
hp : Irreducible p
hq : Irreducible q
⊢ p ∣ q → q ∣ p

Tactic:
rintro ⟨q', rfl⟩

Result:
case intro
M : Type u_1
inst✝ : Monoid M
p : M
hp : Irreducible p
q' : M
hq : Irreducible (p * q')
⊢ p * q' ∣ p

Proof state:
case intro
M : Type u_1
inst✝ : Monoid M
p : M
hp : Irreducible p
q' : M
hq : Irreducible (p * q')
⊢ p * q' ∣ p

Tactic:
rw [IsUnit.mul_right_dvd (Or.resolve_left (of_irreducible_mul hq) hp.not_unit)]

Result:
no goals
-- Mathlib/Logic/Hydra.lean
theorem cutExpand_singleton_singleton {x' x} (h : r x' x) : CutExpand r {x'} {x} :=
  cutExpand_singleton fun a h ↦ by rwa [mem_singleton.1 h]

Proof state:
α : Type u_1
r : α → α → Prop
x' x : α
h✝ : r x' x
a : α
h : a ∈ {x'}
⊢ r a x

Tactic:
rwa [mem_singleton.1 h]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
lemma Set.Finite.latticeClosure (hs : s.Finite) : (latticeClosure s).Finite

Proof state:
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : s.Finite
⊢ (_root_.latticeClosure s).Finite

Tactic:
rw [← supClosure_infClosure]

Result:
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : s.Finite
⊢ (supClosure (infClosure s)).Finite

Proof state:
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : s.Finite
⊢ (supClosure (infClosure s)).Finite

Tactic:
exact hs.infClosure.supClosure

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
theorem FiberBundle.chartedSpace_chartAt_symm_fst (x : TotalSpace F E) (y : ModelProd HB F)
    (hy : y ∈ (chartAt (ModelProd HB F) x).target) :
    ((chartAt (ModelProd HB F) x).symm y).proj = (chartAt HB x.proj).symm y.1

Proof state:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
y : ModelProd HB F
hy :
  y ∈ (chartAt HB x.proj).target ×ˢ univ ∧
    ↑((chartAt HB x.proj).prod (PartialEquiv.refl F)).symm y ∈ (trivializationAt F E x.proj).target
⊢ (↑(trivializationAt F E x.proj).symm (↑((chartAt HB x.proj).prod (PartialHomeomorph.refl F)).symm y)).proj =
    ↑(chartAt HB x.proj).symm y.1

Tactic:
exact (trivializationAt F E x.proj).proj_symm_apply hy.2

Result:
no goals

Proof state:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
y : ModelProd HB F
hy : y ∈ (chartAt (ModelProd HB F) x).target
⊢ (↑(chartAt (ModelProd HB F) x).symm y).proj = ↑(chartAt HB x.proj).symm y.1

Tactic:
simp only [FiberBundle.chartedSpace_chartAt, mfld_simps] at hy ⊢

Result:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
y : ModelProd HB F
hy :
  y ∈ (chartAt HB x.proj).target ×ˢ univ ∧
    ↑((chartAt HB x.proj).prod (PartialEquiv.refl F)).symm y ∈ (trivializationAt F E x.proj).target
⊢ (↑(trivializationAt F E x.proj).symm (↑((chartAt HB x.proj).prod (PartialHomeomorph.refl F)).symm y)).proj =
    ↑(chartAt HB x.proj).symm y.1
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp, norm_cast] lemma cast_abs (q : ℚ) : ((|q| : ℚ) : K) = |(q : K)|

Proof state:
K : Type u_5
inst✝ : LinearOrderedField K
q : ℚ
⊢ ↑|q| = |↑q|

Tactic:
simp [abs_eq_max_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n

Proof state:
a b n : Int
⊢ a * b % n = a % n * (b % n) % n

Tactic:
conv => lhs; rw [
  ← emod_add_ediv a n, ← emod_add_ediv' b n, Int.add_mul, Int.mul_add, Int.mul_add,
  Int.mul_assoc, Int.mul_assoc, ← Int.mul_add n _ _, add_mul_emod_self_left,
  ← Int.mul_assoc, add_mul_emod_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulOperator.lean
theorem denote_cast_entry (entry : Entrypoint α) {input} {h} :
    ⟦(f entry.aig input).aig, entry.ref.cast h, assign⟧
      =
    ⟦entry, assign⟧

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
assign : α → Bool
entry : Entrypoint α
input : β entry.aig
h : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ ⟦assign, { aig := (f entry.aig input).aig, ref := entry.ref.cast h }⟧ = ⟦assign, entry⟧

Tactic:
simp [Ref.cast]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@[simp]
lemma stalkMap_inv_hom_apply (e : X ≅ Y) (x : X) (y) :
    e.hom.stalkMap x (e.inv.stalkMap (e.hom.base x) y) =
      X.presheaf.stalkSpecializes (specializes_of_eq <| by simp) y :=
  DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkMap_inv_hom e x)) y

Proof state:
X✝ X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
x : ↑X.toTopCat
y : ↑(X.presheaf.stalk ((ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x)))
⊢ x = (ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Divisibility/Basic.lean
theorem dvd_iff_exists_eq_mul_left : a ∣ b ↔ ∃ c, b = c * a :=
  ⟨exists_eq_mul_left_of_dvd, by
    rintro ⟨c, rfl⟩
    exact ⟨c, mul_comm _ _⟩⟩

Proof state:
α : Type u_1
inst✝ : CommSemigroup α
a b : α
⊢ (∃ c, b = c * a) → a ∣ b

Tactic:
rintro ⟨c, rfl⟩

Result:
case intro
α : Type u_1
inst✝ : CommSemigroup α
a c : α
⊢ a ∣ c * a

Proof state:
case intro
α : Type u_1
inst✝ : CommSemigroup α
a c : α
⊢ a ∣ c * a

Tactic:
exact ⟨c, mul_comm _ _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem Option.isSome_dmap {o : Option α} {f : (a : α) → (o = some a) → β} :
    (Option.dmap o f).isSome = o.isSome

Proof state:
α : Type u
β : Type v
o : Option α
f : (a : α) → o = some a → β
⊢ (Std.DHashMap.Internal.List.Option.dmap o f).isSome = o.isSome

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/Computability/TMConfig.lean
theorem id_eval (v) : id.eval v = pure v

Proof state:
v : List ℕ
⊢ id.eval v = pure v

Tactic:
simp [id]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
lemma logTaylor_succ (n : ℕ) :
    logTaylor (n + 1) = logTaylor n + (fun z : ℂ ↦ (-1) ^ (n + 1) * z ^ n / n)

Proof state:
n : ℕ
⊢ logTaylor (n + 1) = logTaylor n + fun z => (-1) ^ (n + 1) * z ^ n / ↑n

Tactic:
funext

Result:
case h
n : ℕ
x✝ : ℂ
⊢ logTaylor (n + 1) x✝ = (logTaylor n + fun z => (-1) ^ (n + 1) * z ^ n / ↑n) x✝

Proof state:
case h
n : ℕ
x✝ : ℂ
⊢ logTaylor (n + 1) x✝ = (logTaylor n + fun z => (-1) ^ (n + 1) * z ^ n / ↑n) x✝

Tactic:
simpa only [logTaylor] using Finset.sum_range_succ ..

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem le_sub_of_add_le {a b c : Ordinal} (h : b + c ≤ a) : c ≤ a - b

Proof state:
a b c : Ordinal.{u_4}
h : b + c ≤ a
⊢ b + c ≤ b + (a - b)

Tactic:
exact h.trans (le_add_sub a b)

Result:
no goals

Proof state:
a b c : Ordinal.{u_4}
h : b + c ≤ a
⊢ c ≤ a - b

Tactic:
rw [← add_le_add_iff_left b]

Result:
a b c : Ordinal.{u_4}
h : b + c ≤ a
⊢ b + c ≤ b + (a - b)
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem piecewise_ae_eq_restrict_compl [DecidablePred (· ∈ s)] (hs : MeasurableSet s) :
    piecewise s f g =ᵐ[μ.restrict sᶜ] g

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
⊢ s.piecewise f g =ᶠ[ae (μ.restrict sᶜ)] g

Tactic:
rw [ae_restrict_eq hs.compl]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
⊢ s.piecewise f g =ᶠ[ae μ ⊓ 𝓟 sᶜ] g

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
⊢ s.piecewise f g =ᶠ[ae μ ⊓ 𝓟 sᶜ] g

Tactic:
exact (piecewise_eqOn_compl s f g).eventuallyEq.filter_mono inf_le_right

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_X_sub_C_pow (c : R) (m : ℕ) :
    derivative ((X - C c) ^ m) = C (m : R) * (X - C c) ^ (m - 1)

Proof state:
R : Type u
inst✝ : CommRing R
c : R
m : ℕ
⊢ derivative ((X - C c) ^ m) = C ↑m * (X - C c) ^ (m - 1)

Tactic:
rw [derivative_pow, derivative_X_sub_C, mul_one]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem mem_span_mul_finite_of_mem_mul {I J : FractionalIdeal S P} {x : P} (hx : x ∈ I * J) :
    ∃ T T' : Finset P, (T : Set P) ⊆ I ∧ (T' : Set P) ⊆ J ∧ x ∈ span R (T * T' : Set P) :=
  Submodule.mem_span_mul_finite_of_mem_mul (by simpa using mem_coe.mpr hx)

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
x : P
hx : x ∈ I * J
⊢ x ∈ ↑I * ↑J

Tactic:
simpa using mem_coe.mpr hx

Result:
no goals