harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem coeff_p [CharP R p] (i : ℕ) : (p : 𝕎 R).coeff i = if i = 1 then 1 else 0

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
⊢ (↑p).coeff i = if i = 1 then 1 else 0

Tactic:
split_ifs with hi

Result:
case pos
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : i = 1
⊢ (↑p).coeff i = 1

case neg
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ¬i = 1
⊢ (↑p).coeff i = 0

Proof state:
case neg
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ¬i = 1
⊢ (↑p).coeff i = 0

Tactic:
simpa only [pow_one] using coeff_p_pow_eq_zero p R hi

Result:
no goals

Proof state:
case pos
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : i = 1
⊢ (↑p).coeff i = 1

Tactic:
simpa only [hi, pow_one] using coeff_p_pow p R 1

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem divInt_neg' (num den) : num /. -den = -num /. den

Proof state:
num den : Int
⊢ num /. -den = -num /. den

Tactic:
rw [← neg_divInt_neg, Int.neg_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
theorem Cocone.ofCotrident_ι {F : WalkingParallelFamily J ⥤ C}
    (t : Cotrident fun j => F.map (line j)) (j) :
    (Cocone.ofCotrident t).ι.app j = eqToHom (by cases j <;> aesop_cat) ≫ t.ι.app j :=
  rfl

Proof state:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j => F.map (line j)
j : WalkingParallelFamily J
⊢ F.obj j = (parallelFamily fun j => F.map (line j)).obj j

Tactic:
cases j <;> aesop_cat

Result:
no goals
-- Mathlib/Topology/Algebra/GroupWithZero.lean
theorem Filter.Tendsto.div {l : Filter α} {a b : G₀} (hf : Tendsto f l (𝓝 a))
    (hg : Tendsto g l (𝓝 b)) (hy : b ≠ 0) : Tendsto (f / g) l (𝓝 (a / b))

Proof state:
α : Type u_1
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
f g : α → G₀
l : Filter α
a b : G₀
hf : Tendsto f l (𝓝 a)
hg : Tendsto g l (𝓝 b)
hy : b ≠ 0
⊢ Tendsto (f / g) l (𝓝 (a / b))

Tactic:
simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ hy)

Result:
no goals
-- Mathlib/Topology/ContinuousMap/CompactlySupported.lean
lemma toRealLinearMap_apply_apply (f : C_c(α, ℝ≥0)) (x : α) :
    toRealLinearMap f x = (f x).toReal

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ≥0
x : α
⊢ (toRealLinearMap f) x = ↑(f x)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
theorem rank_kaehlerDifferential [Nontrivial S]
    (P : SubmersivePresentation R S) : Module.rank S (Ω[S⁄R]) = P.dimension

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
P : SubmersivePresentation R S
⊢ Module.rank S (Ω[S⁄R]) = ↑P.dimension

Tactic:
simp only [rank_eq_card_basis P.basisKaehler, Nat.cast_inj, Fintype.card_compl_set,
  Presentation.dimension, Nat.card_eq_fintype_card, Set.card_range_of_injective P.map_inj]

Result:
no goals
-- Mathlib/Data/Nat/Bits.lean
lemma shiftLeft'_sub (b m) : ∀ {n k}, k ≤ n → shiftLeft' b m (n - k) = (shiftLeft' b m n) >>> k
  | _, 0, _ => rfl
  | n + 1, k + 1, h => by
    rw [succ_sub_succ_eq_sub, shiftLeft', Nat.add_comm, shiftRight_add]
    simp only [shiftLeft'_sub, Nat.le_of_succ_le_succ h, shiftRight_succ, shiftRight_zero]
    simp [← div2_val, div2_bit]

Proof state:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m n >>> k = (bit b (shiftLeft' b m n) / 2) >>> k

Tactic:
simp [← div2_val, div2_bit]

Result:
no goals

Proof state:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n - k) = bit b (shiftLeft' b m n) >>> 1 >>> k

Tactic:
simp only [shiftLeft'_sub, Nat.le_of_succ_le_succ h, shiftRight_succ, shiftRight_zero]

Result:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m n >>> k = (bit b (shiftLeft' b m n) / 2) >>> k

Proof state:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n + 1 - (k + 1)) = shiftLeft' b m (n + 1) >>> (k + 1)

Tactic:
rw [succ_sub_succ_eq_sub, shiftLeft', Nat.add_comm, shiftRight_add]

Result:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n - k) = bit b (shiftLeft' b m n) >>> 1 >>> k
-- Mathlib/RingTheory/Coalgebra/Basic.lean
@[simp]
lemma sum_tmul_counit_eq {a : A} (repr : Coalgebra.Repr R a) :
    ∑ i ∈ repr.index, (repr.left i) ⊗ₜ counit (R := R) (repr.right i) = a ⊗ₜ[R] 1

Proof state:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
repr : Repr R a
⊢ ∑ i ∈ repr.index, repr.left i ⊗ₜ[R] counit (repr.right i) = a ⊗ₜ[R] 1

Tactic:
simpa [← repr.eq, map_sum] using congr($(lTensor_counit_comp_comul (R := R) (A := A)) a)

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
lemma iIndep.meas_iInter [Fintype ι] (h : iIndep m κ μ) (hs : ∀ i, MeasurableSet[m i] (s i)) :
    ∀ᵐ a ∂μ, κ a (⋂ i, s i) = ∏ i, κ a (s i)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndep m κ μ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i, s i) = ∏ i : ι, (κ a) (s i)

Tactic:
filter_upwards [h.meas_biInter (fun i (_ : i ∈ Finset.univ) ↦ hs _)] with a ha

Result:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndep m κ μ
hs : ∀ (i : ι), MeasurableSet (s i)
a : α
ha : (κ a) (⋂ i ∈ Finset.univ, s i) = ∏ i : ι, (κ a) (s i)
⊢ (κ a) (⋂ i, s i) = ∏ i : ι, (κ a) (s i)

Proof state:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndep m κ μ
hs : ∀ (i : ι), MeasurableSet (s i)
a : α
ha : (κ a) (⋂ i ∈ Finset.univ, s i) = ∏ i : ι, (κ a) (s i)
⊢ (κ a) (⋂ i, s i) = ∏ i : ι, (κ a) (s i)

Tactic:
simp [← ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem mul_assoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k)
  | _, _, 0      => rfl
  | n, m, succ k => by simp [mul_succ, Nat.mul_assoc n m k, Nat.left_distrib]

Proof state:
n m k : Nat
⊢ n * m * k.succ = n * (m * k.succ)

Tactic:
simp [mul_succ, Nat.mul_assoc n m k, Nat.left_distrib]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_hasFDerivAt_iff {f : G → E} {x : G} {f' : G →L[𝕜] E} :
    HasFDerivAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') x ↔ HasFDerivAt f f' x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
f' : G →L[𝕜] E
⊢ HasFDerivAt (⇑iso ∘ f) ((↑iso).comp f') x ↔ HasFDerivAt f f' x

Tactic:
simp_rw [← hasFDerivWithinAt_univ, iso.comp_hasFDerivWithinAt_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem midpoint_neg_self (x : V) : midpoint R (-x) x = 0

Proof state:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x : V
⊢ midpoint R (-x) x = 0

Tactic:
simpa using midpoint_self_neg R (-x)

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma zero_div_subset (s : Finset α) : 0 / s ⊆ 0

Proof state:
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
⊢ 0 / s ⊆ 0

Tactic:
simp [subset_iff, mem_div]

Result:
no goals
-- Mathlib/Order/Bounded.lean
theorem unbounded_lt_inter_lt [LinearOrder α] [NoMaxOrder α] (a : α) :
    Unbounded (· < ·) (s ∩ { b | a < b }) ↔ Unbounded (· < ·) s

Proof state:
α : Type u_1
s : Set α
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 < x2) (s ∩ {b | a < b}) ↔ Bounded (fun x1 x2 => x1 < x2) s

Tactic:
exact bounded_lt_inter_lt a

Result:
no goals

Proof state:
α : Type u_1
s : Set α
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Unbounded (fun x1 x2 => x1 < x2) (s ∩ {b | a < b}) ↔ Unbounded (fun x1 x2 => x1 < x2) s

Tactic:
rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]

Result:
α : Type u_1
s : Set α
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 < x2) (s ∩ {b | a < b}) ↔ Bounded (fun x1 x2 => x1 < x2) s
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem equiv_push : Equiv self.push a b ↔ Equiv self a b

Proof state:
a b : Nat
self : UnionFind
⊢ self.push.Equiv a b ↔ self.Equiv a b

Tactic:
simp [Equiv]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem one_sub_X_sq_mul_U_eq_pol_in_T (n : ℤ) :
    (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)

Tactic:
linear_combination T_eq_X_mul_T_sub_pol_U R n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eq_false_of_or_eq_false_left {a b : Prop} (h : (a ∨ b) = False) : a = False

Proof state:
a b : Prop
h : (a ∨ b) = False
⊢ a = False

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
@[to_additive]
protected lemma div_mul_cancel_left (h : IsUnit a) (b : α) : a / (a * b) = b⁻¹

Proof state:
α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a / (a * b) = b⁻¹

Tactic:
rw [mul_comm, h.div_mul_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Completion.lean
theorem inv_mk {f} (hf) : (mk (abv := abv) f)⁻¹ = mk (inv f hf) :=
  congr_arg mk <| by rw [dif_neg]

Proof state:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ (if h : f.LimZero then 0 else f.inv h) = f.inv hf

Tactic:
rw [dif_neg]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem norm_div (z w : ℂ) : ‖z / w‖ = ‖z‖ / ‖w‖

Proof state:
z w : ℂ
⊢ ‖z / w‖ = ‖z‖ / ‖w‖

Tactic:
rw [norm_def, norm_def, norm_def, normSq_div, Real.sqrt_div (normSq_nonneg _)]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem disjoint_comap_iff_map' {f : α → β} {F : Filter α} {G : Filter β} :
    Disjoint (comap f G) F ↔ Disjoint G (map f F)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ Disjoint (comap f G) F ↔ Disjoint G (map f F)

Tactic:
simp only [disjoint_iff, ← Filter.push_pull', map_eq_bot_iff]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Period.lean
theorem period_dvd_orderOf (m : M) (a : α) : period m a ∣ orderOf m

Proof state:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
⊢ period m a ∣ orderOf m

Tactic:
rw [← pow_smul_eq_iff_period_dvd, pow_orderOf_eq_one, one_smul]

Result:
no goals
-- Mathlib/Control/Traversable/Instances.lean
theorem naturality {α β} (f : α → F β) (x : σ ⊕ α) :
    η (Sum.traverse f x) = Sum.traverse (@η _ ∘ f) x

Proof state:
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : σ ⊕ α
⊢ (fun {α} => η.app α) (Sum.traverse f x) = Sum.traverse ((fun {α} => η.app α) ∘ f) x

Tactic:
cases x <;> simp! [Sum.traverse, functor_norm, ApplicativeTransformation.preserves_map,
  ApplicativeTransformation.preserves_seq, ApplicativeTransformation.preserves_pure]

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
/-- Conjugation by a unit preserves the spectrum, inverse on left. -/
@[simp]
lemma spectrum.units_conjugate' {a : A} {u : Aˣ} :
    spectrum R (u⁻¹ * a * u) = spectrum R a

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
⊢ spectrum R (↑u⁻¹ * a * ↑u) = spectrum R a

Tactic:
simpa using spectrum.units_conjugate (u := u⁻¹)

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem add_le_of_lt (h1 : a ≡ b [MOD m]) (h2 : a < b) : a + m ≤ b :=
  le_of_lt_add (add_modEq_right.trans h1) (by omega)

Proof state:
m a b : ℕ
h1 : a ≡ b [MOD m]
h2 : a < b
⊢ a + m < b + m

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem mul_le_iff_le_one_right' [MulLeftMono α]
    [MulLeftReflectLE α] (a : α) {b : α} :
    a * b ≤ a ↔ b ≤ 1 :=
  Iff.trans (by rw [mul_one]) (mul_le_mul_iff_left a)

Proof state:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulLeftMono α
inst✝ : MulLeftReflectLE α
a b : α
⊢ a * b ≤ a ↔ a * b ≤ a * 1

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma ne_of_odd_add (h : Odd (m + n)) : m ≠ n

Proof state:
m n : ℕ
h : Odd (m + n)
⊢ m ≠ n

Tactic:
rintro rfl

Result:
m : ℕ
h : Odd (m + m)
⊢ False

Proof state:
m : ℕ
h : Odd (m + m)
⊢ False

Tactic:
simp [← not_even_iff_odd] at h

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
theorem FarFromTriangleFree.mono (hε : G.FarFromTriangleFree ε) (h : δ ≤ ε) :
    G.FarFromTriangleFree δ := hε.mono <| by gcongr

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝² : LinearOrderedField 𝕜
G : SimpleGraph α
ε δ : 𝕜
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hε : G.FarFromTriangleFree ε
h : δ ≤ ε
⊢ δ * ↑(Fintype.card α ^ 2) ≤ ε * ↑(Fintype.card α ^ 2)

Tactic:
gcongr

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
lemma exp_int_mul_two_pi (n : ℤ) : exp (n * (2 * π)) = 1 :=
  ext <| by simpa [mul_assoc] using Complex.exp_int_mul_two_pi_mul_I n

Proof state:
n : ℤ
⊢ ↑(exp (↑n * (2 * π))) = ↑1

Tactic:
simpa [mul_assoc] using Complex.exp_int_mul_two_pi_mul_I n

Result:
no goals
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem Antivary.sum_comp_perm_smul_eq_sum_smul_iff (hfg : Antivary f g) :
    ∑ i, f (σ i) • g i = ∑ i, f i • g i ↔ Antivary (f ∘ σ) g

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedSemiring α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i : ι, f (σ i) • g i = ∑ i : ι, f i • g i ↔ Antivary (f ∘ ⇑σ) g

Tactic:
simp [(hfg.antivaryOn _).sum_comp_perm_smul_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem tendsto_symm {x} (hx : x ∈ e.source) : Tendsto e.symm (𝓝 (e x)) (𝓝 x)

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
hx : x ∈ e.source
⊢ Tendsto (↑e.symm) (𝓝 (↑e x)) (𝓝 x)

Tactic:
simpa only [ContinuousAt, e.left_inv hx] using e.continuousAt_symm (e.map_source hx)

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_iUnion_eq_or_left {b : β} {p : β → Prop} {s : ∀ x : β, x = b ∨ p x → Set α} :
    ⋃ (x) (h), s x h = s b (Or.inl rfl) ∪ ⋃ (x) (h : p x), s x (Or.inr h)

Proof state:
α : Type u_1
β : Type u_2
b : β
p : β → Prop
s : (x : β) → x = b ∨ p x → Set α
⊢ ⋃ x, ⋃ (h : x = b ∨ p x), s x h = s b ⋯ ∪ ⋃ x, ⋃ (h : p x), s x ⋯

Tactic:
simp only [iUnion_or, iUnion_union_distrib, iUnion_iUnion_eq_left]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem exists_not_mem_null_le_lintegral (hf : AEMeasurable f μ) (hN : μ N = 0) :
    ∃ x, x ∉ N ∧ f x ≤ ∫⁻ a, f a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst✝ : IsProbabilityMeasure μ
hf : AEMeasurable f μ
hN : μ N = 0
⊢ ∃ x ∉ N, f x ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
simpa only [laverage_eq_lintegral] using
  exists_not_mem_null_le_laverage (IsProbabilityMeasure.ne_zero μ) hf hN

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem Fin.cast_eq_cast' {n m : ℕ} (h : Fin n = Fin m) :
    _root_.cast h = Fin.cast (fin_injective h)

Proof state:
case refl
n : ℕ
h : Fin n = Fin n
⊢ cast h = Fin.cast ⋯

Tactic:
rfl

Result:
no goals

Proof state:
n m : ℕ
h : Fin n = Fin m
⊢ cast h = Fin.cast ⋯

Tactic:
cases fin_injective h

Result:
case refl
n : ℕ
h : Fin n = Fin n
⊢ cast h = Fin.cast ⋯
-- Mathlib/Analysis/Analytic/Basic.lean
@[simp] lemma analyticOn_univ {f : E → F} :
    AnalyticOn 𝕜 f univ ↔ AnalyticOnNhd 𝕜 f univ

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ AnalyticOn 𝕜 f univ ↔ AnalyticOnNhd 𝕜 f univ

Tactic:
simp only [AnalyticOn, analyticWithinAt_univ, AnalyticOnNhd]

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.const {x : β} : ωScottContinuous (Function.const α x)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
x : β
⊢ ωScottContinuous (Function.const α x)

Tactic:
simp [ωScottContinuous, ScottContinuousOn, Set.range_nonempty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_filter {xs : Vector α n} (p q : α → Bool) :
    (xs.filter p).find? q = xs.find? (fun a => p a ∧ q a)

Proof state:
α : Type
n : Nat
xs : Vector α n
p q : α → Bool
⊢ Array.find? q (Array.filter p xs.toArray) = find? (fun a => decide (p a = true ∧ q a = true)) xs

Tactic:
cases xs

Result:
case mk
α : Type
n : Nat
p q : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.find? q (Array.filter p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray) =
    find? (fun a => decide (p a = true ∧ q a = true)) { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type
n : Nat
p q : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.find? q (Array.filter p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray) =
    find? (fun a => decide (p a = true ∧ q a = true)) { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubOfPoint_subtype_eq_filter (w : ι → k) (p : ι → P) (b : P) (pred : ι → Prop)
    [DecidablePred pred] :
    ((s.subtype pred).weightedVSubOfPoint (fun i => p i) b fun i => w i) =
      {x ∈ s | pred x}.weightedVSubOfPoint p b w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
⊢ (((Finset.subtype pred s).weightedVSubOfPoint (fun i => p ↑i) b) fun i => w ↑i) =
    ((filter (fun x => pred x) s).weightedVSubOfPoint p b) w

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_subtype_eq_sum_filter]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
/-- `castPred` commutes with `succAbove`. -/
lemma castPred_succAbove_castPred {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ last (n + 1))
    (hb : b ≠ last n) (hk := succAbove_ne_last ha hb) :
    (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk

Proof state:
n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
hb : b ≠ last n
hk : optParam (a.succAbove b ≠ last (n + 1)) ⋯
⊢ (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk

Tactic:
simp_rw [← castSucc_inj (b := (a.succAbove b).castPred hk), ← castSucc_succAbove_castSucc,
  castSucc_castPred]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblU_eq (P : Fin 3 → F) : W.dblU P =
    (W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2)) ^ 3 / P z ^ 2

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
⊢ W.dblU P = (W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2)) ^ 3 / P z ^ 2

Tactic:
rw [dblU, eval_polynomialX]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/Basic.lean
theorem mem_rootsOfUnity_iff_mem_nthRoots {ζ : Rˣ} :
    ζ ∈ rootsOfUnity k R ↔ (ζ : R) ∈ nthRoots k (1 : R)

Proof state:
R : Type u_4
k : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : Rˣ
⊢ ζ ∈ rootsOfUnity k R ↔ ↑ζ ∈ nthRoots k 1

Tactic:
simp only [mem_rootsOfUnity, mem_nthRoots (NeZero.pos k), Units.ext_iff, Units.val_one,
  Units.val_pow_eq_pow_val]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_diff_both (a b : α) : Icc a b \ {a, b} = Ioo a b

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ Icc a b \ {a, b} = Ioo a b

Tactic:
simp [← coe_inj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
    {l : List ((a : α) × β a)} {k : α}
    (contains_eq_false : (l.map Sigma.fst).contains k = false) :
    (ofList l).getKey! k = default

Proof state:
α : Type u
β : α → Type v
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List ((a : α) × β a)
k : α
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ (ofList l).getKey! k = default

Tactic:
simp_to_raw using Raw₀.getKey!_insertMany_empty_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem nhdsWithin_eq_comap_uniformity_of_mem {x : α} {T : Set α} (hx : x ∈ T) (S : Set α) :
    𝓝[S] x = (𝓤 α ⊓ 𝓟 (T ×ˢ S)).comap (Prod.mk x)

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
T : Set α
hx : x ∈ T
S : Set α
⊢ 𝓝[S] x = comap (Prod.mk x) (𝓤 α ⊓ 𝓟 (T ×ˢ S))

Tactic:
simp [nhdsWithin, nhds_eq_comap_uniformity, hx]

Result:
no goals
-- Mathlib/Data/Matrix/Invertible.lean
theorem invOf_mul_cancel_left (A : Matrix n n α) (B : Matrix n m α) [Invertible A] :
    ⅟ A * (A * B) = B

Proof state:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ ⅟A * (A * B) = B

Tactic:
rw [← Matrix.mul_assoc, invOf_mul_self, Matrix.one_mul]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[simp] lemma ofIsLimitKernelFork_g' (hf : S.f = 0) (c : KernelFork S.g)
    (hc : IsLimit c) : (ofIsLimitKernelFork S hf c hc).g' = S.g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ (ofIsLimitKernelFork S hf c hc).g' = S.g

Tactic:
rw [← cancel_epi (ofIsLimitKernelFork S hf c hc).p, p_g',
  ofIsLimitKernelFork_p, id_comp]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem natDegree_add_le (p q : R[X]) : natDegree (p + q) ≤ max (natDegree p) (natDegree q)

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p + q).natDegree ≤ p.natDegree ⊔ q.natDegree

Tactic:
rcases le_max_iff.1 (degree_add_le p q) with h | h <;> simp [natDegree_le_natDegree h]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem closedBall_div_singleton : closedBall x δ / {y} = closedBall (x / y) δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ closedBall x δ / {y} = closedBall (x / y) δ

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Algebra/Order/UpperLower.lean
theorem IsUpperSet.mul_left (ht : IsUpperSet t) : IsUpperSet (s * t)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
ht : IsUpperSet t
⊢ IsUpperSet (s * t)

Tactic:
rw [← smul_eq_mul, ← Set.iUnion_smul_set]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
ht : IsUpperSet t
⊢ IsUpperSet (⋃ a ∈ s, a • t)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
ht : IsUpperSet t
⊢ IsUpperSet (⋃ a ∈ s, a • t)

Tactic:
exact isUpperSet_iUnion₂ fun x _ ↦ ht.smul

Result:
no goals