harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem dist_indicatorConstLp_eq_norm {t : Set α} {ht : MeasurableSet t} {hμt : μ t ≠ ∞} :
    dist (indicatorConstLp p hs hμs c) (indicatorConstLp p ht hμt c) =
      ‖indicatorConstLp p (hs.symmDiff ht) (measure_symmDiff_ne_top hμs hμt) c‖

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ dist (indicatorConstLp p hs hμs c) (indicatorConstLp p ht hμt c) = ‖indicatorConstLp p ⋯ ⋯ c‖

Tactic:
simp only [Lp.dist_edist, edist_indicatorConstLp_eq_enorm, enorm, ENNReal.coe_toReal,
  Lp.coe_nnnorm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_takeWhile (p : α → Bool) (as : Array α) :
    (as.takeWhile p).toList = as.toList.takeWhile p

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ (takeWhile p as).toList = List.takeWhile p as.toList

Tactic:
induction as

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ (takeWhile p { toList := toList✝ }).toList = List.takeWhile p { toList := toList✝ }.toList

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ (takeWhile p { toList := toList✝ }).toList = List.takeWhile p { toList := toList✝ }.toList

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem changeForm_ι_mul_ι (m₁ m₂ : M) :
    changeForm h (ι Q m₁ * ι Q m₂) = ι Q' m₁ * ι Q' m₂ - algebraMap _ _ (B m₁ m₂)

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m₁ m₂ : M
⊢ (changeForm h) ((ι Q) m₁ * (ι Q) m₂) = (ι Q') m₁ * (ι Q') m₂ - (algebraMap R (CliffordAlgebra Q')) ((B m₁) m₂)

Tactic:
rw [changeForm_ι_mul, changeForm_ι, contractLeft_ι]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_const_mul_atTop_iff_neg [NeBot l] (h : Tendsto f l atBot) :
    Tendsto (fun x => r * f x) l atTop ↔ r < 0

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

Tactic:
simp [tendsto_const_mul_atTop_iff, h, h.not_tendsto disjoint_atBot_atTop]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma SMulPosReflectLE.lift [SMulPosReflectLE α γ]
    (hf : ∀ {b₁ b₂}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂)
    (smul : ∀ (a : α) b, f (a • b) = a • f b)
    (zero : f 0 = 0) : SMulPosReflectLE α β where
  elim b hb a₁ a₂ h

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 < b
a₁ a₂ : α
h : a₁ • b ≤ a₂ • b
⊢ a₁ ≤ a₂

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosReflectLE α γ
b : β
a₁ a₂ : α
hf : ∀ {b₁ b₂ : β}, True
smul : α → β → True
zero : True
hb : 0 < f b
h : a₁ • f b ≤ a₂ • f b
⊢ a₁ ≤ a₂

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosReflectLE α γ
b : β
a₁ a₂ : α
hf : ∀ {b₁ b₂ : β}, True
smul : α → β → True
zero : True
hb : 0 < f b
h : a₁ • f b ≤ a₂ • f b
⊢ a₁ ≤ a₂

Tactic:
exact le_of_smul_le_smul_right h hb

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem nil_eq {α} {xs : List α} : [] = xs ↔ xs = []

Proof state:
α : Type u_1
xs : List α
⊢ [] = xs ↔ xs = []

Tactic:
cases xs <;> simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_preimage (e : X ≃ᵢ Y) (s : Set Y) : dimH (e ⁻¹' s) = dimH s

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
e : X ≃ᵢ Y
s : Set Y
⊢ dimH (⇑e ⁻¹' s) = dimH s

Tactic:
rw [← e.image_symm, e.symm.dimH_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_filterMap (f : α → Option β) (g : β → γ) (l : Array α) :
    map g (filterMap f l) = filterMap (fun x => (f x).map g) l

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ
toList✝ : List α
⊢ map g (filterMap f { toList := toList✝ }) = filterMap (fun x => Option.map g (f x)) { toList := toList✝ }

Tactic:
simp [List.map_filterMap]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ
l : Array α
⊢ map g (filterMap f l) = filterMap (fun x => Option.map g (f x)) l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ
toList✝ : List α
⊢ map g (filterMap f { toList := toList✝ }) = filterMap (fun x => Option.map g (f x)) { toList := toList✝ }
-- Mathlib/Topology/Basic.lean
theorem frontier_subset_iff_isClosed : frontier s ⊆ s ↔ IsClosed s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ frontier s ⊆ s ↔ IsClosed s

Tactic:
rw [frontier, diff_subset_iff, union_eq_right.mpr interior_subset, closure_subset_iff_isClosed]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean
theorem cancel_right_of_mono {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z} [Mono f₂]
    (big_k : IsKernelPair (f₁ ≫ f₂) a b) : IsKernelPair f₁ a b :=
  cancel_right (by rw [← cancel_mono f₂, assoc, assoc, big_k.w]) big_k

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
big_k : IsKernelPair (f₁ ≫ f₂) a b
⊢ a ≫ f₁ = b ≫ f₁

Tactic:
rw [← cancel_mono f₂, assoc, assoc, big_k.w]

Result:
no goals
-- Mathlib/Data/PEquiv.lean
theorem mem_single_iff (a₁ a₂ : α) (b₁ b₂ : β) : b₁ ∈ single a₂ b₂ a₁ ↔ a₁ = a₂ ∧ b₁ = b₂

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ b₁ ∈ (single a₂ b₂) a₁ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
dsimp [single]

Result:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ (b₁ ∈ if a₁ = a₂ then some b₂ else none) ↔ a₁ = a₂ ∧ b₁ = b₂

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ (b₁ ∈ if a₁ = a₂ then some b₂ else none) ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
split_ifs <;> simp [*, eq_comm]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive mul_nsmul] lemma pow_mul (a : M) (m : ℕ) : ∀ n, a ^ (m * n) = (a ^ m) ^ n
  | 0 => by rw [Nat.mul_zero, pow_zero, pow_zero]
  | n + 1 => by rw [Nat.mul_succ, pow_add, pow_succ, pow_mul]

Proof state:
M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m * (n + 1)) = (a ^ m) ^ (n + 1)

Tactic:
rw [Nat.mul_succ, pow_add, pow_succ, pow_mul]

Result:
no goals

Proof state:
M : Type u_2
inst✝ : Monoid M
a : M
m : ℕ
⊢ a ^ (m * 0) = (a ^ m) ^ 0

Tactic:
rw [Nat.mul_zero, pow_zero, pow_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean
theorem additive_of_preservesBinaryBiproducts [HasBinaryBiproducts C] [PreservesZeroMorphisms F]
    [PreservesBinaryBiproducts F] : Additive F where
  map_add {X Y f g}

Proof state:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : HasBinaryBiproducts C
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
⊢ F.map (f + g) = F.map f + F.map g

Tactic:
rw [biprod.add_eq_lift_id_desc, F.map_comp, ← biprod.lift_mapBiprod,
  ← biprod.mapBiprod_hom_desc, Category.assoc, Iso.inv_hom_id_assoc, F.map_id,
  biprod.add_eq_lift_id_desc]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem coe_iInf (f : ι → LowerSet α) : (↑(⨅ i, f i) : Set α) = ⋂ i, f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
f : ι → LowerSet α
⊢ ↑(⨅ i, f i) = ⋂ i, ↑(f i)

Tactic:
simp_rw [iInf, coe_sInf, mem_range, iInter_exists, iInter_iInter_eq']

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Bisect.lean
theorem avg_comm (a b : Nat) : avg a b = avg b a

Proof state:
a b : Nat
⊢ a.avg b = b.avg a

Tactic:
rw [avg, Nat.add_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Preadditive.lean
theorem Preadditive.isCoseparator_iff (G : C) :
    IsCoseparator G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : Y ⟶ G, f ≫ h = 0) → f = 0 :=
  ⟨fun hG X Y f hf => hG.def _ _ (by simpa only [Limits.zero_comp] using hf), fun hG =>
    (isCoseparator_def _).2 fun X Y f g hfg =>
      sub_eq_zero.1 <| hG _ (by simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg)⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ ∀ (h : Y ⟶ G), (f - g) ≫ h = 0

Tactic:
simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : IsCoseparator G
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ G), f ≫ h = 0
⊢ ∀ (h : Y ⟶ G), f ≫ h = 0 ≫ h

Tactic:
simpa only [Limits.zero_comp] using hf

Result:
no goals
-- Mathlib/Topology/Separation/Regular.lean
theorem TopologicalSpace.IsTopologicalBasis.exists_closure_subset {B : Set (Set X)}
    (hB : IsTopologicalBasis B) {x : X} {s : Set X} (h : s ∈ 𝓝 x) :
    ∃ t ∈ B, x ∈ t ∧ closure t ⊆ s

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
B : Set (Set X)
hB : IsTopologicalBasis B
x : X
s : Set X
h : s ∈ 𝓝 x
⊢ ∃ t ∈ B, x ∈ t ∧ closure t ⊆ s

Tactic:
simpa only [exists_prop, and_assoc] using hB.nhds_hasBasis.nhds_closure.mem_iff.mp h

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem coe_zsmulRec : ∀ z, ⇑(zsmulRec (· • ·) z f) = z • ⇑f
  | Int.ofNat n => by rw [zsmulRec, Int.ofNat_eq_coe, coe_nsmul, natCast_zsmul]
  | Int.negSucc n => by rw [zsmulRec, negSucc_zsmul, coe_neg, coe_nsmul]

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ ⇑(zsmulRec (fun x1 x2 => x1 • x2) (Int.negSucc n) f) = Int.negSucc n • ⇑f

Tactic:
rw [zsmulRec, negSucc_zsmul, coe_neg, coe_nsmul]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ ⇑(zsmulRec (fun x1 x2 => x1 • x2) (Int.ofNat n) f) = Int.ofNat n • ⇑f

Tactic:
rw [zsmulRec, Int.ofNat_eq_coe, coe_nsmul, natCast_zsmul]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma exists_isCircuit_of_mem_closure (he : e ∈ M.closure X) (heX : e ∉ X) :
    ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C :=
  let ⟨I, hI⟩ := M.exists_isBasis' X
  ⟨_, (fundCircuit_subset_insert ..).trans (insert_subset_insert hI.subset),
    hI.indep.fundCircuit_isCircuit (by rwa [hI.closure_eq_closure]) (not_mem_subset
    hI.subset heX), M.mem_fundCircuit e I⟩

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
heX : e ∉ X
I : Set α
hI : M.IsBasis' I X
⊢ e ∈ M.closure I

Tactic:
rwa [hI.closure_eq_closure]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_subset_Ici_self : Ico a b ⊆ Ici a

Proof state:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b ⊆ Ici a

Tactic:
simpa [← coe_subset] using Set.Ico_subset_Ici_self

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem star_add_self : star a + a = 2 * a.re

Proof state:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ star a + a = 2 * ↑a.re

Tactic:
simp [a.star_add_self, Quaternion.coe]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem mulRight_bound (x : α) : ∀ y : α, ‖AddMonoidHom.mulRight x y‖ ≤ ‖x‖ * ‖y‖ := fun y => by
  rw [mul_comm]
  exact norm_mul_le y x

Proof state:
α : Type u_2
inst✝ : NonUnitalSeminormedRing α
x y : α
⊢ ‖(AddMonoidHom.mulRight x) y‖ ≤ ‖x‖ * ‖y‖

Tactic:
rw [mul_comm]

Result:
α : Type u_2
inst✝ : NonUnitalSeminormedRing α
x y : α
⊢ ‖(AddMonoidHom.mulRight x) y‖ ≤ ‖y‖ * ‖x‖

Proof state:
α : Type u_2
inst✝ : NonUnitalSeminormedRing α
x y : α
⊢ ‖(AddMonoidHom.mulRight x) y‖ ≤ ‖y‖ * ‖x‖

Tactic:
exact norm_mul_le y x

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.merge_lemma {a b c : ℕ} (h₁ : 3 * a < b + c + 1) (h₂ : b ≤ 3 * c) :
    2 * (a + b) ≤ 9 * c + 5

Proof state:
a b c : ℕ
h₁ : 3 * a < b + c + 1
h₂ : b ≤ 3 * c
⊢ 2 * (a + b) ≤ 9 * c + 5

Tactic:
omega

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem induction_on {C : M ∗ N → Prop} (m : M ∗ N)
    (inl : ∀ m, C (inl m)) (inr : ∀ n, C (inr n)) (mul : ∀ x y, C x → C y → C (x * y)) : C m :=
  induction_on' m (by simpa using inl 1) (fun _ _ ↦ mul _ _ (inl _)) fun _ _ ↦ mul _ _ (inr _)

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
C : M ∗ N → Prop
m : M ∗ N
inl : ∀ (m : M), C (Monoid.Coprod.inl m)
inr : ∀ (n : N), C (Monoid.Coprod.inr n)
mul : ∀ (x y : M ∗ N), C x → C y → C (x * y)
⊢ C 1

Tactic:
simpa using inl 1

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_comap_comap_eq_relfinrank_of_surjective
    (f : L →ₐ[F] E) (h : Function.Surjective f) :
    relfinrank (A.comap f) (B.comap f) = relfinrank A B

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : Type w
inst✝¹ : Field L
inst✝ : Algebra F L
A B : IntermediateField F E
f : L →ₐ[F] E
h : Function.Surjective ⇑f
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank B

Tactic:
simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_of_surjective A B f h))

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bsup_eq_sup' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal.{max u v}) :
    bsup.{_, v} _ (bfamilyOfFamily' r f) = sup.{_, v} f

Proof state:
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → Ordinal.{max u v}
⊢ (type r).bsup (bfamilyOfFamily' r f) = sup f

Tactic:
simp (config := { unfoldPartialApp := true }) only [← sup_eq_bsup' r, enum_typein,
  familyOfBFamily', bfamilyOfFamily']

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem coe_sort_true : (true : Prop) = True

Proof state:
⊢ (true = true) = True

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem not_isRoot_C (r a : R) (hr : r ≠ 0) : ¬IsRoot (C r) a

Proof state:
R : Type u
inst✝ : Semiring R
r a : R
hr : r ≠ 0
⊢ ¬(C r).IsRoot a

Tactic:
simpa using hr

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Opposite.lean
theorem cokernel.π_op :
    (cokernel.π f.op).unop =
      (cokernelOpUnop f).hom ≫ kernel.ι f ≫ eqToHom (Opposite.unop_op _).symm

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (cokernel.π f.op).unop = (cokernelOpUnop f).hom ≫ kernel.ι f ≫ eqToHom ⋯

Tactic:
simp [cokernelOpUnop]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_of_hasDerivAt_of_tendsto [CompleteSpace E]
    (hderiv : ∀ x, HasDerivAt f (f' x) x) (hf' : Integrable f')
    (hbot : Tendsto f atBot (𝓝 m)) (htop : Tendsto f atTop (𝓝 n)) : ∫ x, f' x = n - m

Proof state:
E : Type u_1
f f' : ℝ → E
m n : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hbot : Tendsto f atBot (𝓝 m)
htop : Tendsto f atTop (𝓝 n)
⊢ ∫ (x : ℝ), f' x = n - m

Tactic:
rw [← setIntegral_univ, ← Set.Iic_union_Ioi (a := 0),
  setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi hf'.integrableOn hf'.integrableOn,
  integral_Iic_of_hasDerivAt_of_tendsto' (fun x _ ↦ hderiv x) hf'.integrableOn hbot,
  integral_Ioi_of_hasDerivAt_of_tendsto' (fun x _ ↦ hderiv x) hf'.integrableOn htop]

Result:
E : Type u_1
f f' : ℝ → E
m n : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hbot : Tendsto f atBot (𝓝 m)
htop : Tendsto f atTop (𝓝 n)
⊢ f 0 - m + (n - f 0) = n - m

Proof state:
E : Type u_1
f f' : ℝ → E
m n : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hbot : Tendsto f atBot (𝓝 m)
htop : Tendsto f atTop (𝓝 n)
⊢ f 0 - m + (n - f 0) = n - m

Tactic:
abel

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Integral.lean
lemma extendScalars_of_isIntegral [NoZeroDivisors S] [Algebra.IsIntegral R S] :
    Transcendental S a

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
a : A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsIntegral R S
ha : IsAlgebraic S a
⊢ IsAlgebraic R a

Tactic:
exact ha.restrictScalars_of_isIntegral _

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
a : A
ha : Transcendental R a
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsIntegral R S
⊢ Transcendental S a

Tactic:
contrapose ha

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
a : A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsIntegral R S
ha : ¬Transcendental S a
⊢ ¬Transcendental R a

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
a : A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsIntegral R S
ha : ¬Transcendental S a
⊢ ¬Transcendental R a

Tactic:
rw [Transcendental, not_not] at ha ⊢

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
a : A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsIntegral R S
ha : IsAlgebraic S a
⊢ IsAlgebraic R a
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem indepSetFree_compl : Gᶜ.IndepSetFree n ↔ G.CliqueFree n

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ Gᶜ.IndepSetFree n ↔ G.CliqueFree n

Tactic:
simp [IndepSetFree, CliqueFree]

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem R1Space.t2Space_iff_t0Space [R1Space X] : T2Space X ↔ T0Space X

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ T2Space X ↔ T0Space X

Tactic:
constructor <;> intro <;> infer_instance

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
lemma wInner_const_right (f : ι → 𝕜) (a : 𝕜) :
    ⟪f, const _ a⟫_[𝕜, w] = (∑ i, w i • conj (f i)) * a

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
w : ι → ℝ
f : ι → 𝕜
a : 𝕜
⊢ wInner w f (const ι a) = (∑ i : ι, w i • (starRingEnd 𝕜) (f i)) * a

Tactic:
simp [wInner, const_apply, sum_mul]

Result:
no goals
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem nullHomotopicMap_f_eq_zero {k₀ : ι} (hk₀ : ∀ l : ι, ¬c.Rel k₀ l)
    (hk₀' : ∀ l : ι, ¬c.Rel l k₀) (hom : ∀ i j, C.X i ⟶ D.X j) :
    (nullHomotopicMap hom).f k₀ = 0

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ C.d k₀ (c.next k₀) ≫ hom (c.next k₀) k₀ + hom k₀ (c.prev k₀) ≫ D.d (c.prev k₀) k₀ = 0

Tactic:
rw [C.shape, D.shape, zero_comp, comp_zero, add_zero] <;> apply_assumption

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (nullHomotopicMap hom).f k₀ = 0

Tactic:
dsimp [nullHomotopicMap, dNext, prevD]

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ C.d k₀ (c.next k₀) ≫ hom (c.next k₀) k₀ + hom k₀ (c.prev k₀) ≫ D.d (c.prev k₀) k₀ = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem lt_of_le_of_ne : ∀ {x y : Bool}, x ≤ y → x ≠ y → x < y

Proof state:
⊢ ∀ {x y : Bool}, x ≤ y → x ≠ y → x < y

Tactic:
decide

Result:
no goals
-- Mathlib/Data/ENNReal/Action.lean
lemma nnreal_smul_ne_top {x : ℝ≥0} {y : ℝ≥0∞} (hy : y ≠ ⊤) : x • y ≠ ⊤ := mul_ne_top (by simp) hy

Proof state:
x : ℝ≥0
y : ℝ≥0∞
hy : y ≠ ⊤
⊢ ↑ofNNRealHom.toMonoidWithZeroHom x ≠ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobjectIso_comp_image_map {W X Y Z : C} {f : W ⟶ X} [HasImage f] {g : Y ⟶ Z}
    [HasImage g] (sq : Arrow.mk f ⟶ Arrow.mk g) [HasImageMap sq] :
    (imageSubobjectIso _).hom ≫ image.map sq =
      imageSubobjectMap sq ≫ (imageSubobjectIso _).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (imageSubobjectIso (Arrow.mk f).hom).hom ≫ image.map sq = imageSubobjectMap sq ≫ (imageSubobjectIso g).hom

Tactic:
erw [← Iso.comp_inv_eq, Category.assoc, ← (imageSubobjectIso f).eq_inv_comp,
  image_map_comp_imageSubobjectIso_inv sq]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
lemma δ_comp_zero_cochain {n₁ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K 0)
    (m₁ : ℤ) (h₁ : n₁ + 1 = m₁) :
    δ n₁ m₁ (z₁.comp z₂ (add_zero n₁)) =
      z₁.comp (δ 0 1 z₂) h₁ + (δ n₁ m₁ z₁).comp z₂ (add_zero m₁)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K 0
m₁ : ℤ
h₁ : n₁ + 1 = m₁
⊢ δ n₁ m₁ (z₁.comp z₂ ⋯) = z₁.comp (δ 0 1 z₂) h₁ + (δ n₁ m₁ z₁).comp z₂ ⋯

Tactic:
simp only [δ_comp z₁ z₂ (add_zero n₁) m₁ 1 m₁ h₁ h₁ (zero_add 1), one_smul,
  Int.negOnePow_zero]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem blsub_congr {o₁ o₂ : Ordinal.{u}} (f : ∀ a < o₁, Ordinal.{max u v}) (ho : o₁ = o₂) :
    blsub.{_, v} o₁ f = blsub.{_, v} o₂ fun a h => f a (h.trans_eq ho.symm)

Proof state:
o₁ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
⊢ o₁.blsub f = o₁.blsub fun a h => f a ⋯

Tactic:
rfl

Result:
no goals

Proof state:
o₁ o₂ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
ho : o₁ = o₂
⊢ o₁.blsub f = o₂.blsub fun a h => f a ⋯

Tactic:
subst ho

Result:
o₁ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
⊢ o₁.blsub f = o₁.blsub fun a h => f a ⋯
-- Mathlib/Data/Set/Image.lean
theorem Nonempty.subset_preimage_const {s : Set α} (hs : Set.Nonempty s) (t : Set β) (a : β) :
    s ⊆ (fun _ => a) ⁻¹' t ↔ a ∈ t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
t : Set β
a : β
⊢ s ⊆ (fun x => a) ⁻¹' t ↔ a ∈ t

Tactic:
rw [← image_subset_iff, hs.image_const, singleton_subset_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/WF.lean
theorem fixF_eq_fixFC : @fixF = @fixFC

Proof state:
⊢ @fixF = @WellFounded.fixFC

Tactic:
funext α r C F x a

Result:
case h.h.h.h.h.h
α : Sort u_1
r : α → α → Prop
C : α → Sort u_2
F : (x : α) → ((y : α) → r y x → C y) → C x
x : α
a : Acc r x
⊢ fixF F x a = WellFounded.fixFC F x a

Proof state:
case h.h.h.h.h.h
α : Sort u_1
r : α → α → Prop
C : α → Sort u_2
F : (x : α) → ((y : α) → r y x → C y) → C x
x : α
a : Acc r x
⊢ fixF F x a = WellFounded.fixFC F x a

Tactic:
rw [fixF, Acc.rec_eq_recC, fixFC]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_X_mul_zero (p : R[X]) : coeff (X * p) 0 = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (X * p).coeff 0 = 0

Tactic:
simp

Result:
no goals