harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Denumerable.lean
theorem encode_ofNat (n) : encode (ofNat α n) = n

Proof state:
case intro.intro
α : Type u_1
inst✝ : Denumerable α
n : ℕ
a : α
h : a ∈ decode n
e : encode a = n
⊢ encode (ofNat α n) = n

Tactic:
rwa [ofNat_of_decode h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Denumerable α
n : ℕ
⊢ encode (ofNat α n) = n

Tactic:
obtain ⟨a, h, e⟩ := decode_inv (α := α) n

Result:
case intro.intro
α : Type u_1
inst✝ : Denumerable α
n : ℕ
a : α
h : a ∈ decode n
e : encode a = n
⊢ encode (ofNat α n) = n
-- Mathlib/Data/ENat/Basic.lean
@[simp]
lemma not_lt_zero (n : ℕ∞) : ¬ n < 0

Proof state:
n : ℕ∞
⊢ ¬n < 0

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Char/Basic.lean
theorem isValidChar_zero : isValidChar 0 :=
  Or.inl (by decide)

Proof state:
⊢ 0 < 55296

Tactic:
decide

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualCoannihilator_top (W : Subspace K V) :
    (⊤ : Subspace K (Module.Dual K W)).dualCoannihilator = ⊥

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ dualCoannihilator ⊤ = ⊥

Tactic:
rw [dualCoannihilator, dualAnnihilator_top, comap_bot, Module.eval_ker]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_sub' (a b : α) : toIocDiv hp (a - p) b = toIocDiv hp a b + 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp (a - p) b = toIocDiv hp a b + 1

Tactic:
simpa only [one_zsmul] using toIocDiv_sub_zsmul' hp a b 1

Result:
no goals
-- Mathlib/Algebra/Order/Module/Rat.lean
@[simp] lemma abs_nnqsmul [DistribMulAction ℚ≥0 α] [PosSMulMono ℚ≥0 α] (q : ℚ≥0) (a : α) :
    |q • a| = q • |a|

Proof state:
α : Type u_1
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : DistribMulAction ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
q : ℚ≥0
a : α
⊢ |q • a| = q • |a|

Tactic:
obtain ha | ha := le_total a 0 <;>
  simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem dist_pointReflection_self_real (x y : P) :
    dist (pointReflection ℝ x y) y = 2 * dist x y

Proof state:
V : Type u_2
P : Type u_10
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedSpace ℝ V
x y : P
⊢ dist ((pointReflection ℝ x) y) y = 2 * dist x y

Tactic:
rw [dist_pointReflection_self, Real.norm_two]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem coeff_single_mul_add [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ}
    {b : Γ} : (single b r * x).coeff (a + b) = r * x.coeff a

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
⊢ ((single b) r * x).coeff (a + b) = r * x.coeff a

Tactic:
rw [← of_symm_smul_of_eq_mul, add_comm, ← vadd_eq_add]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
⊢ ((HahnModule.of R).symm ((single b) r • (HahnModule.of R) x)).coeff (b +ᵥ a) = r * x.coeff a

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
⊢ ((HahnModule.of R).symm ((single b) r • (HahnModule.of R) x)).coeff (b +ᵥ a) = r * x.coeff a

Tactic:
exact HahnModule.coeff_single_smul_vadd

Result:
no goals
-- Mathlib/Data/Set/Image.lean
/-- Alias of `Set.image_compl_eq_range_sdiff_image`. -/
lemma range_diff_image {f : α → β} (hf : Injective f) (s : Set α) : range f \ f '' s = f '' sᶜ

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ range f \ f '' s = f '' sᶜ

Tactic:
rw [image_compl_eq_range_diff_image hf]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem left_mem_Ioc : a ∈ Ioc a b ↔ False

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ a ∈ Ioc a b ↔ False

Tactic:
simp [lt_irrefl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
    (∀ b, b ∈ replicate n a → p b) ↔ n = 0 ∨ p a

Proof state:
α : Type u_1
p : α → Prop
a : α
n : Nat
⊢ (∀ (b : α), b ∈ replicate n a → p b) ↔ n = 0 ∨ p a

Tactic:
cases n <;> simp [mem_replicate]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofNat_le_ofNat {n} {x y : Nat} : (BitVec.ofNat n x) ≤ (BitVec.ofNat n y) ↔ x % 2^n ≤ y % 2^n

Proof state:
n x y : Nat
⊢ BitVec.ofNat n x ≤ BitVec.ofNat n y ↔ x % 2 ^ n ≤ y % 2 ^ n

Tactic:
simp [le_def]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem mgf_zero_fun : mgf 0 μ t = (μ Set.univ).toReal

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
⊢ mgf 0 μ t = (μ Set.univ).toReal

Tactic:
simp only [mgf, Pi.zero_apply, mul_zero, exp_zero, integral_const, smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/GroupTheory/Sylow.lean
theorem smul_eq_of_normal {g : G} {P : Sylow p G} [h : P.Normal] :
    g • P = P

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
h : (↑P).Normal
⊢ g • P = P

Tactic:
simp only [smul_eq_iff_mem_normalizer, P.normalizer_eq_top, mem_top]

Result:
no goals
-- Mathlib/Dynamics/FixedPoints/Basic.lean
theorem Commute.left_bijOn_fixedPoints_comp (h : Commute f g) :
    Set.BijOn f (fixedPoints <| f ∘ g) (fixedPoints <| f ∘ g)

Proof state:
α : Type u
f g : α → α
h : Function.Commute f g
⊢ Set.BijOn f (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
simpa only [h.comp_eq] using bijOn_fixedPoints_comp g f

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma map_neg : (-z).map Φ = -z.map Φ

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
⊢ (-z).map Φ = -z.map Φ

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
lemma isIntegralCurveAt_iff :
    IsIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
⊢ IsIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s

Tactic:
simp_rw [IsIntegralCurveOn, ← Filter.eventually_iff_exists_mem, IsIntegralCurveAt]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_add_orthogonalProjection_orthogonal [HasOrthogonalProjection K]
    (w : E) : (orthogonalProjection K w : E) + (orthogonalProjection Kᗮ w : E) = w

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
w : E
⊢ ↑((orthogonalProjection K) w) + ↑((orthogonalProjection Kᗮ) w) = w

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get?_set_ne (a : α) {m n} (l : List α) (h : m ≠ n) : (set l m a).get? n = l.get? n

Proof state:
α : Type u_1
a : α
m n : Nat
l : List α
h : m ≠ n
⊢ (l.set m a).get? n = l.get? n

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem real_inner_self_eq_norm_sq (x : F) : ⟪x, x⟫_ℝ = ‖x‖ ^ 2

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
⊢ ⟪x, x⟫_ℝ = ‖x‖ ^ 2

Tactic:
rw [pow_two, real_inner_self_eq_norm_mul_norm]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/CommShift.lean
lemma commShiftIso_comp_inv_app [F.CommShift A] [G.CommShift A] (a : A) (X : C) :
    (commShiftIso (F ⋙ G) a).inv.app X =
      (commShiftIso G a).inv.app (F.obj X) ≫ G.map ((commShiftIso F a).inv.app X)

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_7, u_2} D
inst✝⁶ : Category.{u_8, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
a : A
X : C
⊢ ((F ⋙ G).commShiftIso a).inv.app X = (G.commShiftIso a).inv.app (F.obj X) ≫ G.map ((F.commShiftIso a).inv.app X)

Tactic:
simp [commShiftIso, CommShift.iso]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem intCast_comp (i : ℤ) : comp (i : R[X]) p = i

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
i : ℤ
⊢ (↑i).comp p = ↑i

Tactic:
cases i <;> simp

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem liftOn_div {P : Sort v} (p q : K[X]) (f : K[X] → K[X] → P) (f0 : ∀ p, f p 0 = f 0 1)
    (H' : ∀ {p q p' q'} (_hq : q ≠ 0) (_hq' : q' ≠ 0), q' * p = q * p' → f p q = f p' q')
    (H : ∀ {p q p' q'} (_hq : q ∈ K[X]⁰) (_hq' : q' ∈ K[X]⁰), q' * p = q * p' → f p q = f p' q' :=
      fun {_ _ _ _} hq hq' h => H' (nonZeroDivisors.ne_zero hq) (nonZeroDivisors.ne_zero hq') h) :
    (RatFunc.liftOn (algebraMap _ (RatFunc K) p / algebraMap _ _ q)) f @H = f p q

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H' : ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'
H : optParam (∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q') ⋯
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).liftOn f H = f p q

Tactic:
rw [← mk_eq_div, liftOn_mk _ _ f f0 @H']

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
@[simp]
private lemma mem_pairs (k : ℕ) (t : Finset σ × σ) :
    t ∈ pairs σ k ↔ #t.1 ≤ k ∧ (#t.1 = k → t.snd ∈ t.fst)

Proof state:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
⊢ t ∈ MvPolynomial.NewtonIdentities.pairs σ k ↔ #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)

Tactic:
simp [pairs]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem im_ofReal_mul (r : ℝ) (z : ℂ) : (r * z).im = r * z.im

Proof state:
r : ℝ
z : ℂ
⊢ (↑r * z).im = r * z.im

Tactic:
simp [ofReal]

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem _root_.HasCompactSupport.convolution_integrand_bound_right_of_subset
    (hcg : HasCompactSupport g) (hg : Continuous g)
    {x t : G} {s u : Set G} (hx : x ∈ s) (hu : -tsupport g + s ⊆ u) :
    ‖L (f t) (g (x - t))‖ ≤ u.indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖) t

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 E'
inst✝² : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹ : AddGroup G
inst✝ : TopologicalSpace G
hcg : HasCompactSupport g
hg : Continuous g
x t : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
i : G
⊢ ‖g i‖ ≤ ⨆ i, ‖g i‖

Tactic:
exact le_ciSup (hg.norm.bddAbove_range_of_hasCompactSupport hcg.norm) _

Result:
no goals

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 E'
inst✝² : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹ : AddGroup G
inst✝ : TopologicalSpace G
hcg : HasCompactSupport g
hg : Continuous g
x t : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
⊢ ‖(L (f t)) (g (x - t))‖ ≤ u.indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖) t

Tactic:
refine convolution_integrand_bound_right_of_le_of_subset _ (fun i => ?_) hx hu

Result:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 E'
inst✝² : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹ : AddGroup G
inst✝ : TopologicalSpace G
hcg : HasCompactSupport g
hg : Continuous g
x t : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
i : G
⊢ ‖g i‖ ≤ ⨆ i, ‖g i‖
-- Mathlib/Order/Filter/AtTopBot/Field.lean
/-- If `r` is a negative constant, `fun x ↦ f x / r` tends to infinity along a filter `l`
if and only if `f` tends to negative infinity along `l`. -/
lemma tendsto_div_const_atTop_of_neg (hr : r < 0) :
    Tendsto (fun x ↦ f x / r) l atTop ↔ Tendsto f l atBot

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x => f x / r) l atTop ↔ Tendsto f l atBot

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atTop_of_neg, hr]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem abs_moebius_le_one {n : ℕ} : |μ n| ≤ 1

Proof state:
n : ℕ
⊢ if Squarefree n then 1 ≤ 1 else 0 ≤ 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem toDual_min' {s : Finset α} (hs : s.Nonempty) :
    toDual (min' s hs) = max' (s.image toDual) (hs.image _)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ s.sup (WithBot.some ∘ fun x => toDual x) = s.sup ((WithBot.some ∘ fun x => x) ∘ ⇑toDual)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ ↑(toDual (s.min' hs)) = ↑((image (⇑toDual) s).max' ⋯)

Tactic:
simp only [min'_eq_inf', id_eq, toDual_inf', Function.comp_apply, coe_sup', max'_eq_sup',
  sup_image]

Result:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ s.sup (WithBot.some ∘ fun x => toDual x) = s.sup ((WithBot.some ∘ fun x => x) ∘ ⇑toDual)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ toDual (s.min' hs) = (image (⇑toDual) s).max' ⋯

Tactic:
rw [← WithBot.coe_eq_coe]

Result:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ ↑(toDual (s.min' hs)) = ↑((image (⇑toDual) s).max' ⋯)
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem norm_eq (f : α →ᵇ β) : ‖f‖ = sInf { C : ℝ | 0 ≤ C ∧ ∀ x : α, ‖f x‖ ≤ C }

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f‖ = sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C}

Tactic:
simp [norm_def, BoundedContinuousFunction.dist_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem lift_comp_conePointsIsoOfNatIso_inv {F G : J ⥤ C} {r s : Cone G} {t : Cone F}
    (P : IsLimit t) (Q : IsLimit s) (w : F ≅ G) :
    Q.lift r ≫ (conePointsIsoOfNatIso P Q w).inv = P.map r w.inv :=
  P.hom_ext (by simp)

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F G : J ⥤ C
r s : Cone G
t : Cone F
P : IsLimit t
Q : IsLimit s
w : F ≅ G
⊢ ∀ (j : J), (Q.lift r ≫ (P.conePointsIsoOfNatIso Q w).inv) ≫ t.π.app j = map r P w.inv ≫ t.π.app j

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_eq_zero_iff {f : α → E} (hf : AEStronglyMeasurable f μ) (h0 : p ≠ 0) :
    eLpNorm f p μ = 0 ↔ f =ᵐ[μ] 0

Proof state:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : p = ⊤
⊢ eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
rw [h_top, eLpNorm_exponent_top, eLpNormEssSup_eq_zero_iff]

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : ¬p = ⊤
⊢ eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
rw [eLpNorm_eq_eLpNorm' h0 h_top]

Result:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : ¬p = ⊤
⊢ eLpNorm' f p.toReal μ = 0 ↔ f =ᶠ[ae μ] 0

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
⊢ eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
by_cases h_top : p = ∞

Result:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : p = ⊤
⊢ eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0

case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : ¬p = ⊤
⊢ eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : ¬p = ⊤
⊢ eLpNorm' f p.toReal μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
exact eLpNorm'_eq_zero_iff (ENNReal.toReal_pos h0 h_top) hf

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
lemma of_id_fst : IsPushout (𝟙 _) f f (𝟙 _) := IsPushout.of_horiz_isIso ⟨by simp⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X : C
f : Z ⟶ X
⊢ 𝟙 Z ≫ f = f ≫ 𝟙 X

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem colLen_anti (μ : YoungDiagram) (j1 j2 : ℕ) (hj : j1 ≤ j2) : μ.colLen j2 ≤ μ.colLen j1

Proof state:
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ μ.colLen j2 ≤ μ.colLen j1

Tactic:
convert μ.transpose.rowLen_anti j1 j2 hj using 1 <;> simp

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem valuedAdicCompletion_eq_valuation' (k : K) :
    Valued.v (k : v.adicCompletion K) = v.valuation K k

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
k : K
⊢ Valued.v ↑k = (valuation K v) k

Tactic:
convert Valued.valuedCompletion_apply k

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findSome?_mkArray : findSome? f (mkArray n a) = if n = 0 then none else f a

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
⊢ findSome? f (mkArray n a) = if n = 0 then none else f a

Tactic:
simp [← List.toArray_replicate, List.findSome?_replicate]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem xor_self : ∀ (x : Bool), (x ^^ x) = false

Proof state:
⊢ ∀ (x : Bool), (x ^^ x) = false

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Proper.lean
theorem comap_comap (g : F →L[ℝ] G) (f : E →L[ℝ] F) (S : ProperCone ℝ G) :
    (S.comap g).comap f = S.comap (g.comp f) :=
  SetLike.coe_injective <| by congr

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
g : F →L[ℝ] G
f : E →L[ℝ] F
S : ProperCone ℝ G
⊢ ↑(comap f (comap g S)) = ↑(comap (g.comp f) S)

Tactic:
congr

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem prod_map {δ} [PseudoEMetricSpace δ] {f : α → β} {g : γ → δ} (hf : Isometry f)
    (hg : Isometry g) : Isometry (Prod.map f g) := fun x y => by
  simp only [Prod.edist_eq, Prod.map_fst, hf.edist_eq, Prod.map_snd, hg.edist_eq]

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
δ : Type u_2
inst✝ : PseudoEMetricSpace δ
f : α → β
g : γ → δ
hf : Isometry f
hg : Isometry g
x y : α × γ
⊢ edist (Prod.map f g x) (Prod.map f g y) = edist x y

Tactic:
simp only [Prod.edist_eq, Prod.map_fst, hf.edist_eq, Prod.map_snd, hg.edist_eq]

Result:
no goals
-- Mathlib/Data/Matrix/Basic.lean
lemma entryAddMonoidHom_eq_comp {i : m} {j : n} :
    entryAddMonoidHom α i j =
      ((Pi.evalAddMonoidHom (fun _ => α) j).comp (Pi.evalAddMonoidHom _ i)).comp
        (AddMonoidHomClass.toAddMonoidHom ofAddEquiv.symm)

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝ : AddZeroClass α
i : m
j : n
⊢ entryAddMonoidHom α i j =
    ((Pi.evalAddMonoidHom (fun x => α) j).comp (Pi.evalAddMonoidHom (fun i => n → α) i)).comp ↑ofAddEquiv.symm

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem boundedLimitRec_zero {l} (lLim : l.IsLimit) {C} (H₁ H₂ H₃) :
    @boundedLimitRecOn l lLim C ⟨0, lLim.pos⟩ H₁ H₂ H₃ = H₁

Proof state:
l : Ordinal.{u_4}
lLim : l.IsLimit
C : ↑(Iio l) → Sort u_5
H₁ : C ⟨0, ⋯⟩
H₂ : (o : ↑(Iio l)) → C o → C ⟨succ ↑o, ⋯⟩
H₃ : (o : ↑(Iio l)) → (↑o).IsLimit → ((o' : ↑(Iio l)) → o' < o → C o') → C o
⊢ boundedLimitRecOn lLim ⟨0, ⋯⟩ H₁ H₂ H₃ = H₁

Tactic:
rw [boundedLimitRecOn, limitRecOn_zero]

Result:
no goals
-- Mathlib/Data/Fintype/Sigma.lean
lemma Set.biInter_finsetSigma_univ' (s : Finset ι) (f : Π i, κ i → Set α) :
    ⋂ i ∈ s, ⋂ j, f i j = ⋂ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij.1 ij.2

Proof state:
ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : (i : ι) → κ i → Set α
⊢ ⋂ i ∈ s, ⋂ j, f i j = ⋂ ij ∈ s.sigma fun x => Finset.univ, f ij.fst ij.snd

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem Nat.zero_eq_one_mod_iff {n : Nat} : 0 = 1 % n ↔ n = 1

Proof state:
n : Nat
⊢ 0 = 1 % n ↔ n = 1

Tactic:
rw [eq_comm]

Result:
n : Nat
⊢ 1 % n = 0 ↔ n = 1

Proof state:
n : Nat
⊢ 1 % n = 0 ↔ n = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem LinearMap.convexOn (f : E →ₗ[𝕜] β) {s : Set E} (hs : Convex 𝕜 s) : ConvexOn 𝕜 s f :=
  ⟨hs, fun _ _ _ _ _ _ _ _ _ => by rw [f.map_add, f.map_smul, f.map_smul]⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
f : E →ₗ[𝕜] β
s : Set E
hs : Convex 𝕜 s
x✝⁸ : E
x✝⁷ : x✝⁸ ∈ s
x✝⁶ : E
x✝⁵ : x✝⁶ ∈ s
x✝⁴ x✝³ : 𝕜
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
⊢ f (x✝⁴ • x✝⁸ + x✝³ • x✝⁶) ≤ x✝⁴ • f x✝⁸ + x✝³ • f x✝⁶

Tactic:
rw [f.map_add, f.map_smul, f.map_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α}
    (h : DistinctKeys l) : getValue? k (eraseKey k l) = none

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k : α
h : DistinctKeys l
⊢ getValue? k (eraseKey k l) = none

Tactic:
simp [getValue?_eq_getEntry?, getEntry?_eraseKey_self h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forIn'_map [Monad m] [LawfulMonad m]
    (l : List α) (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :
    forIn' (l.map g) init f = forIn' l init fun a h y => f (g a) (mem_map_of_mem g h) y

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
g : α → β
f : (b : β) → b ∈ map g l → γ → m (ForInStep γ)
⊢ forIn' (map g l) init f = forIn' l init fun a h y => f (g a) ⋯ y

Tactic:
induction l generalizing init <;> simp_all

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem derivFamily_lt_ord {ι} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c) (hι : #ι < c)
    (hc' : c ≠ ℵ₀) (hf : ∀ (i), ∀ b < c.ord, f i b < c.ord) {a} :
    a < c.ord → derivFamily.{u, u} f a < c.ord :=
  derivFamily_lt_ord_lift hc (by rwa [lift_id]) hc' hf

Proof state:
ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{u}
⊢ lift.{?u.138353, u} #ι < c

Tactic:
rwa [lift_id]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem det_conj' {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :
    det (M⁻¹ * N * M) = det N

Proof state:
m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (M⁻¹ * N * M).det = N.det

Tactic:
rw [← h.unit_spec, ← coe_units_inv, det_units_conj']

Result:
no goals