harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma IsUnramified.comap_algHom {w : InfinitePlace F} (h : IsUnramified k w) (f : K →ₐ[k] F) :
    IsUnramified k (w.comap (f : K →+* F))

Proof state:
k : Type u_1
inst✝⁴ : Field k
K : Type u_2
inst✝³ : Field K
F : Type u_3
inst✝² : Field F
inst✝¹ : Algebra k K
inst✝ : Algebra k F
w : InfinitePlace F
h : IsUnramified k w
f : K →ₐ[k] F
⊢ (w.comap ↑f).mult ≤ w.mult

Tactic:
exact InfinitePlace.mult_comap_le _ _

Result:
no goals

Proof state:
k : Type u_1
inst✝⁴ : Field k
K : Type u_2
inst✝³ : Field K
F : Type u_3
inst✝² : Field F
inst✝¹ : Algebra k K
inst✝ : Algebra k F
w : InfinitePlace F
h : IsUnramified k w
f : K →ₐ[k] F
⊢ IsUnramified k (w.comap ↑f)

Tactic:
rw [InfinitePlace.isUnramified_iff_mult_le, ← InfinitePlace.comap_comp, f.comp_algebraMap, h.eq]

Result:
k : Type u_1
inst✝⁴ : Field k
K : Type u_2
inst✝³ : Field K
F : Type u_3
inst✝² : Field F
inst✝¹ : Algebra k K
inst✝ : Algebra k F
w : InfinitePlace F
h : IsUnramified k w
f : K →ₐ[k] F
⊢ (w.comap ↑f).mult ≤ w.mult
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem Filter.HasBasis.equicontinuousAt_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set X}
    {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → X → α} {x₀ : X} (hX : (𝓝 x₀).HasBasis p₁ s₁)
    (hα : (𝓤 α).HasBasis p₂ s₂) :
    EquicontinuousAt F x₀ ↔
      ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ i, (F i x₀, F i x) ∈ s₂ k₂

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ EquicontinuousAt F x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
  hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]

Result:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s₂ ib)}) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s₂ ib)}) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem zpow_apply_eq_of_apply_apply_eq_self {x : α} (hffx : f (f x) = x) :
    ∀ i : ℤ, (f ^ i) x = x ∨ (f ^ i) x = f x
  | (n : ℕ) => pow_apply_eq_of_apply_apply_eq_self hffx n
  | Int.negSucc n => by
    rw [zpow_negSucc, inv_eq_iff_eq, ← f.injective.eq_iff, ← mul_apply, ← pow_succ', eq_comm,
      inv_eq_iff_eq, ← mul_apply, ← pow_succ, @eq_comm _ x, or_comm]
    exact pow_apply_eq_of_apply_apply_eq_self hffx _

Proof state:
α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ (f ^ Int.negSucc n) x = x ∨ (f ^ Int.negSucc n) x = f x

Tactic:
rw [zpow_negSucc, inv_eq_iff_eq, ← f.injective.eq_iff, ← mul_apply, ← pow_succ', eq_comm,
  inv_eq_iff_eq, ← mul_apply, ← pow_succ, @eq_comm _ x, or_comm]

Result:
α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ (f ^ (n + 1 + 1)) x = x ∨ (f ^ (n + 1 + 1)) x = f x

Proof state:
α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ (f ^ (n + 1 + 1)) x = x ∨ (f ^ (n + 1 + 1)) x = f x

Tactic:
exact pow_apply_eq_of_apply_apply_eq_self hffx _

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem ofRestrict_invApp {C : Type*} [Category C] (X : PresheafedSpace C) {Y : TopCat}
    {f : Y ⟶ TopCat.of X.carrier} (h : IsOpenEmbedding f) (U : Opens (X.restrict h).carrier) :
    (PresheafedSpace.IsOpenImmersion.ofRestrict X h).invApp _ U = 𝟙 _

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ invApp (X.ofRestrict h) U = 𝟙 ((X.restrict h).presheaf.obj (op U))

Tactic:
delta invApp

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ (X.restrict h).presheaf.map (eqToHom ⋯) ≫ inv ((X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))) =
    𝟙 ((X.restrict h).presheaf.obj (op U))

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ (X.restrict h).presheaf.map (eqToHom ⋯) ≫ inv ((X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))) =
    𝟙 ((X.restrict h).presheaf.obj (op U))

Tactic:
rw [IsIso.comp_inv_eq, Category.id_comp]

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ (X.restrict h).presheaf.map (eqToHom ⋯) = (X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ (X.restrict h).presheaf.map (eqToHom ⋯) = (X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))

Tactic:
change X.presheaf.map _ = X.presheaf.map _

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ X.presheaf.map (⋯.functor.op.map (eqToHom ⋯)) =
    X.presheaf.map (⋯.adjunction.counit.app (unop (op ((opensFunctor (X.ofRestrict h)).obj U)))).op

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ X.presheaf.map (⋯.functor.op.map (eqToHom ⋯)) =
    X.presheaf.map (⋯.adjunction.counit.app (unop (op ((opensFunctor (X.ofRestrict h)).obj U)))).op

Tactic:
congr 1

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
theorem ediv_eq_zero_of_lt_abs {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < |b|) : a / b = 0 :=
  match b, |b|, abs_eq_natAbs b, H2 with
  | (n : ℕ), _, rfl, H2 => ediv_eq_zero_of_lt H1 H2
  | -[n+1], _, rfl, H2 => neg_injective <| by rw [← Int.ediv_neg]; exact ediv_eq_zero_of_lt H1 H2

Proof state:
a b : ℤ
H1 : 0 ≤ a
H2✝ : a < |b|
n : ℕ
H2 : a < ↑-[n+1].natAbs
⊢ a / - -[n+1] = -0

Tactic:
exact ediv_eq_zero_of_lt H1 H2

Result:
no goals

Proof state:
a b : ℤ
H1 : 0 ≤ a
H2✝ : a < |b|
n : ℕ
H2 : a < ↑-[n+1].natAbs
⊢ -(a / -[n+1]) = -0

Tactic:
rw [← Int.ediv_neg]

Result:
a b : ℤ
H1 : 0 ≤ a
H2✝ : a < |b|
n : ℕ
H2 : a < ↑-[n+1].natAbs
⊢ a / - -[n+1] = -0
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem degree_mul_C (a0 : a ≠ 0) : (p * C a).degree = p.degree

Proof state:
R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
a0 : a ≠ 0
⊢ (p * C a).degree = p.degree

Tactic:
rw [degree_mul, degree_C a0, add_zero]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_eq_finset_prod_of_mulSupport_subset (f : α → M) {s : Finset α}
    (h : mulSupport f ⊆ (s : Set α)) : ∏ᶠ i, f i = ∏ i ∈ s, f i :=
  haveI h' : (s.finite_toSet.subset h).toFinset ⊆ s

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
⊢ ⋯.toFinset ⊆ s

Tactic:
simpa [← Finset.coe_subset, Set.coe_toFinset]

Result:
no goals
-- Mathlib/Algebra/Group/Int/Units.lean
lemma isUnit_ne_iff_eq_neg (hu : IsUnit u) (hv : IsUnit v) : u ≠ v ↔ u = -v

Proof state:
u v : ℤ
hu : IsUnit u
hv : IsUnit v
⊢ u ≠ v ↔ u = -v

Tactic:
obtain rfl | rfl := isUnit_eq_one_or hu <;> obtain rfl | rfl := isUnit_eq_one_or hv <;> decide

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
theorem hasBasis_toFilteriUnion (l : IntegrationParams) (I : Box ι) (π₀ : Prepartition I) :
    (l.toFilteriUnion I π₀).HasBasis (fun r : ℝ≥0 → (ι → ℝ) → Ioi (0 : ℝ) => ∀ c, l.RCond (r c))
      fun r => { π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.iUnion = π₀.iUnion }

Proof state:
ι : Type u_1
inst✝ : Fintype ι
l : IntegrationParams
I : Box ι
π₀ : Prepartition I
this :
  ∀ (c : ℝ≥0),
    (l.toFilterDistortioniUnion I c π₀).HasBasis l.RCond fun r => {π | l.MemBaseSet I c r π ∧ π.iUnion = π₀.iUnion}
⊢ (toFilteriUnion I π₀).HasBasis (fun r => ∀ (c : ℝ≥0), l.RCond (r c)) fun r =>
    {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.iUnion = π₀.iUnion}

Tactic:
simpa only [setOf_and, setOf_exists] using hasBasis_iSup this

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
l : IntegrationParams
I : Box ι
π₀ : Prepartition I
⊢ (toFilteriUnion I π₀).HasBasis (fun r => ∀ (c : ℝ≥0), l.RCond (r c)) fun r =>
    {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.iUnion = π₀.iUnion}

Tactic:
have := fun c => l.hasBasis_toFilterDistortioniUnion I c π₀

Result:
ι : Type u_1
inst✝ : Fintype ι
l : IntegrationParams
I : Box ι
π₀ : Prepartition I
this :
  ∀ (c : ℝ≥0),
    (l.toFilterDistortioniUnion I c π₀).HasBasis l.RCond fun r => {π | l.MemBaseSet I c r π ∧ π.iUnion = π₀.iUnion}
⊢ (toFilteriUnion I π₀).HasBasis (fun r => ∀ (c : ℝ≥0), l.RCond (r c)) fun r =>
    {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.iUnion = π₀.iUnion}
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem liftRel_iff_coeFn {r : β → γ → Prop} {f : α →ₘ[μ] β} {g : α →ₘ[μ] γ} :
    LiftRel r f g ↔ ∀ᵐ a ∂μ, r (f a) (g a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
r : β → γ → Prop
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
⊢ LiftRel r f g ↔ ∀ᵐ (a : α) ∂μ, r (↑f a) (↑g a)

Tactic:
rw [← liftRel_mk_mk, mk_coeFn, mk_coeFn]

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
theorem ex {φ ψ : L.BoundedFormula α (n + 1)} (h : φ ⇔[T] ψ) :
    φ.ex ⇔[T] ψ.ex

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M),
    (∃ a, φ.Realize v (Fin.snoc xs a)) ↔ ∃ a, ψ.Realize v (Fin.snoc xs a)

Tactic:
exact fun M v xs => exists_congr fun a => h.realize_bd_iff

Result:
no goals

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∃'φ ⇔[T] ∃'ψ

Tactic:
simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
  BoundedFormula.realize_ex]

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M),
    (∃ a, φ.Realize v (Fin.snoc xs a)) ↔ ∃ a, ψ.Realize v (Fin.snoc xs a)
-- Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
theorem Ico_mul_Icc_subset' [LocallyFiniteOrder α] (a b c d : α) :
    Ico a b * Icc c d ⊆ Ico (a * c) (b * d) :=
  Finset.coe_subset.mp <| by simpa using Set.Ico_mul_Icc_subset' _ _ _ _

Proof state:
α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : PartialOrder α
inst✝³ : DecidableEq α
inst✝² : MulLeftStrictMono α
inst✝¹ : MulRightStrictMono α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ ↑(Ico a b * Icc c d) ⊆ ↑(Ico (a * c) (b * d))

Tactic:
simpa using Set.Ico_mul_Icc_subset' _ _ _ _

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_sum {ι : Type*} {m : MeasurableSpace α} (μ : ι → Measure α) (f : α → ℝ≥0∞) :
    (sum μ).withDensity f = sum fun n => (μ n).withDensity f

Proof state:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : ι → Measure α
f : α → ℝ≥0∞
⊢ (sum μ).withDensity f = sum fun n => (μ n).withDensity f

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : ι → Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ((sum μ).withDensity f) s = (sum fun n => (μ n).withDensity f) s

Proof state:
case h
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : ι → Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ((sum μ).withDensity f) s = (sum fun n => (μ n).withDensity f) s

Tactic:
simp_rw [sum_apply _ hs, withDensity_apply f hs, restrict_sum μ hs, lintegral_sum_measure]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem hasMFDerivAt_neg : HasMFDerivAt I 𝓘(𝕜, E') (-f) z (-f') ↔ HasMFDerivAt I 𝓘(𝕜, E') f z f' :=
  ⟨fun hf => by convert hf.neg <;> rw [neg_neg], fun hf => hf.neg⟩

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
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
z : M
f : M → E'
f' : TangentSpace I z →L[𝕜] E'
hf : HasMFDerivAt I 𝓘(𝕜, E') (-f) z (-f')
⊢ HasMFDerivAt I 𝓘(𝕜, E') f z f'

Tactic:
convert hf.neg <;> rw [neg_neg]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_digits_append_digits {b m n : ℕ} :
    ofDigits b (digits b n ++ digits b m) = n + b ^ (digits b n).length * m

Proof state:
b m n : ℕ
⊢ ofDigits b (b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m

Tactic:
rw [ofDigits_append, ofDigits_digits, ofDigits_digits]

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem coe_fract_self (k : K) : (fract (Basis.singleton ι K) k : K) = Int.fract k :=
  Basis.ext_elem (Basis.singleton ι K) fun _ => by
    rw [repr_fract_apply, Basis.singleton_repr, Basis.singleton_repr]

Proof state:
ι : Type u_2
K : Type u_3
inst✝³ : NormedLinearOrderedField K
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : Unique ι
k : K
x✝ : ι
⊢ ((Basis.singleton ι K).repr (fract (Basis.singleton ι K) k)) x✝ = ((Basis.singleton ι K).repr (Int.fract k)) x✝

Tactic:
rw [repr_fract_apply, Basis.singleton_repr, Basis.singleton_repr]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ioo_add_one_right_eq_Ioc (a b : α) : Ioo a (b + 1) = Ioc a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ioo_succ_right_eq_Ioc a b

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem some_eq_dite_none_left {p : Prop} [Decidable p] {b : ¬p → Option β} :
    some a = (if h : p then none else b h) ↔ ∃ h, some a = b h

Proof state:
β : Type u_1
a : β
p : Prop
inst✝ : Decidable p
b : ¬p → Option β
⊢ (some a = if h : p then none else b h) ↔ ∃ h, some a = b h

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
@[simp] lemma wInner_of_isEmpty [IsEmpty ι] (w : ι → ℝ) (f g : ∀ i, E i) : ⟪f, g⟫_[𝕜, w] = 0

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝⁴ : Fintype ι
inst✝³ : RCLike 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (E i)
inst✝ : IsEmpty ι
w : ι → ℝ
f g : (i : ι) → E i
⊢ wInner w f g = 0

Tactic:
simp [Subsingleton.elim f 0]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem mul_logb {a b c : ℝ} (h₁ : b ≠ 0) (h₂ : b ≠ 1) (h₃ : b ≠ -1) :
    logb a b * logb b c = logb a c

Proof state:
a b c : ℝ
h₁ : b ≠ 0
h₂ : b ≠ 1
h₃ : b ≠ -1
⊢ log b / log a * (log c / log b) = log c / log a

Tactic:
rw [mul_comm, div_mul_div_cancel₀ (log_ne_zero.mpr ⟨h₁, h₂, h₃⟩)]

Result:
no goals

Proof state:
a b c : ℝ
h₁ : b ≠ 0
h₂ : b ≠ 1
h₃ : b ≠ -1
⊢ logb a b * logb b c = logb a c

Tactic:
unfold logb

Result:
a b c : ℝ
h₁ : b ≠ 0
h₂ : b ≠ 1
h₃ : b ≠ -1
⊢ log b / log a * (log c / log b) = log c / log a
-- Mathlib/Data/TypeVec.lean
theorem dropFun_prod {α α' β β' : TypeVec (n + 1)} (f : α ⟹ β) (f' : α' ⟹ β') :
    dropFun (f ⊗' f') = (dropFun f ⊗' dropFun f')

Proof state:
case a.h
n : ℕ
α α' β β' : TypeVec.{u_1} (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
i : Fin2 n
x✝ : (α ⊗ α').drop i
⊢ dropFun (f ⊗' f') i x✝ = (dropFun f ⊗' dropFun f') i x✝

Tactic:
induction i <;> simp [dropFun, *] <;> rfl

Result:
no goals

Proof state:
n : ℕ
α α' β β' : TypeVec.{u_1} (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
⊢ dropFun (f ⊗' f') = (dropFun f ⊗' dropFun f')

Tactic:
ext i : 2

Result:
case a.h
n : ℕ
α α' β β' : TypeVec.{u_1} (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
i : Fin2 n
x✝ : (α ⊗ α').drop i
⊢ dropFun (f ⊗' f') i x✝ = (dropFun f ⊗' dropFun f') i x✝
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem finInsepDegree_self : finInsepDegree F F = 1

Proof state:
F : Type u
inst✝ : Field F
⊢ finInsepDegree F F = 1

Tactic:
rw [finInsepDegree_def', insepDegree_self, Cardinal.one_toNat]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma sub_neg {x y : EReal} (h_top : x ≠ ⊤ ∨ y ≠ ⊤) (h_bot : x ≠ ⊥ ∨ y ≠ ⊥) :
    x - y < 0 ↔ x < y

Proof state:
x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
⊢ x - y < 0 ↔ x < y

Tactic:
cases x <;> cases y <;> simp_all [← EReal.coe_sub]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem setIntegral_eq_tsum' (h : IsFundamentalDomain G s μ) {f : α → E} {t : Set α}
    (hf : IntegrableOn f t μ) : ∫ x in t, f x ∂μ = ∑' g : G, ∫ x in g • t ∩ s, f (g⁻¹ • x) ∂μ :=
  calc
    ∫ x in t, f x ∂μ = ∑' g : G, ∫ x in t ∩ g • s, f x ∂μ := h.setIntegral_eq_tsum hf
    _ = ∑' g : G, ∫ x in t ∩ g⁻¹ • s, f x ∂μ := ((Equiv.inv G).tsum_eq _).symm
    _ = ∑' g : G, ∫ x in g⁻¹ • (g • t ∩ s), f x ∂μ

Proof state:
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
f : α → E
t : Set α
hf : IntegrableOn f t μ
⊢ ∑' (g : G), ∫ (x : α) in t ∩ g⁻¹ • s, f x ∂μ = ∑' (g : G), ∫ (x : α) in g⁻¹ • (g • t ∩ s), f x ∂μ

Tactic:
simp only [smul_set_inter, inv_smul_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
theorem one_gradedMul (x : (⨁ i, 𝒜 i) ⊗[R] (⨁ i, ℬ i)) :
    gradedMul R 𝒜 ℬ 1 x = x

Proof state:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
⊢ ((gradedMul R 𝒜 ℬ) 1) x = x

Tactic:
simpa only [RingHom.map_one, one_smul] using algebraMap_gradedMul 𝒜 ℬ 1 x

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
theorem LinearMap.exists_monic_and_aeval_eq_zero [Module.Finite R M] (f : Module.End R M) :
    ∃ p : R[X], p.Monic ∧ Polynomial.aeval f p = 0 :=
  (LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul R f ⊤ (by simp)).imp
    fun _ h => h.imp_right And.right

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
⊢ range f ≤ ⊤ • ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem id_tensor_comp_tensor_id (f : W ⟶ X) (g : Y ⟶ Z) : (𝟙 Y ⊗ f) ≫ (g ⊗ 𝟙 X) = g ⊗ f

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ (𝟙 Y ⊗ f) ≫ (g ⊗ 𝟙 X) = g ⊗ f

Tactic:
rw [← tensor_comp]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ 𝟙 Y ≫ g ⊗ f ≫ 𝟙 X = g ⊗ f

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ 𝟙 Y ≫ g ⊗ f ≫ 𝟙 X = g ⊗ f

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If 0 belongs to the interior of the interval `integrableExpSet X μ`,
then `X ^ n` is integrable for all `n : ℕ`. -/
lemma integrable_pow_of_mem_interior_integrableExpSet
    (h : 0 ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    Integrable (fun ω ↦ X ω ^ n) μ

Proof state:
case h.e'_6.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
x✝ : Ω
⊢ X x✝ ^ n = X x✝ ^ n * rexp (0 * X x✝)

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (fun ω => X ω ^ n) μ

Tactic:
convert integrable_pow_mul_exp_of_mem_interior_integrableExpSet h n

Result:
case h.e'_6.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
x✝ : Ω
⊢ X x✝ ^ n = X x✝ ^ n * rexp (0 * X x✝)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem getRight?_eq_some_iff : x.getRight? = some b ↔ x = inr b

Proof state:
β✝ : Type u_1
b : β✝
α✝ : Type u_2
x : α✝ ⊕ β✝
⊢ x.getRight? = some b ↔ x = inr b

Tactic:
cases x <;> simp only [getRight?, Option.some.injEq, inr.injEq, reduceCtorEq]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem liftRel_pure_right (R : α → β → Prop) (ca : Computation α) (b : β) :
    LiftRel R ca (pure b) ↔ ∃ a, a ∈ ca ∧ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
b : β
⊢ LiftRel R ca (pure b) ↔ ∃ a, a ∈ ca ∧ R a b

Tactic:
rw [LiftRel.swap, liftRel_pure_left]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_eq_zero_of_ae {f : α → G} (hf : f =ᵐ[μ] 0) : ∫ a, f a ∂μ = 0

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : f =ᶠ[ae μ] 0
⊢ ∫ (a : α), f a ∂μ = 0

Tactic:
simp [integral_congr_ae hf, integral_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem neg_mul_eq_neg_mul (a b : Int) : -(a * b) = -a * b :=
  Int.neg_eq_of_add_eq_zero <| by rw [← Int.add_mul, Int.add_right_neg, Int.zero_mul]

Proof state:
a b : Int
⊢ a * b + -a * b = 0

Tactic:
rw [← Int.add_mul, Int.add_right_neg, Int.zero_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem zero_sub (a : Int) : 0 - a = -a

Proof state:
a : Int
⊢ 0 - a = -a

Tactic:
simp [Int.sub_eq_add_neg]

Result:
no goals