harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Complex/Liouville.lean
theorem norm_deriv_le_aux [CompleteSpace F] {c : ℂ} {R C : ℝ} {f : ℂ → F} (hR : 0 < R)
    (hf : DiffContOnCl ℂ f (ball c R)) (hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C) :
    ‖deriv f c‖ ≤ C / R

Proof state:
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ∀ z ∈ sphere c R, ‖(z - c) ^ (-2) • f z‖ ≤ C / (R * R)
⊢ R * (C / (R * R)) = C / R

Tactic:
rw [mul_div_left_comm, div_self_mul_self', div_eq_mul_inv]

Result:
no goals

Proof state:
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ∀ z ∈ sphere c R, ‖(z - c) ^ (-2) • f z‖ ≤ C / (R * R)
⊢ ‖deriv f c‖ ≤ C / R

Tactic:
calc
  ‖deriv f c‖ = ‖(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (-2 : ℤ) • f z‖ :=
    congr_arg norm (deriv_eq_smul_circleIntegral hR hf)
  _ ≤ R * (C / (R * R)) :=
    (circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const hR.le this)
  _ = C / R := by rw [mul_div_left_comm, div_self_mul_self', div_eq_mul_inv]

Result:
no goals

Proof state:
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ‖deriv f c‖ ≤ C / R

Tactic:
have : ∀ z ∈ sphere c R, ‖(z - c) ^ (-2 : ℤ) • f z‖ ≤ C / (R * R) :=
  fun z (hz : ‖z - c‖ = R) => by
  simpa [-mul_inv_rev, norm_smul, hz, zpow_two, ← div_eq_inv_mul] using
    (div_le_div_iff_of_pos_right (mul_pos hR hR)).2 (hC z hz)

Result:
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ∀ z ∈ sphere c R, ‖(z - c) ^ (-2) • f z‖ ≤ C / (R * R)
⊢ ‖deriv f c‖ ≤ C / R

Proof state:
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
z : ℂ
hz : ‖z - c‖ = R
⊢ ‖(z - c) ^ (-2) • f z‖ ≤ C / (R * R)

Tactic:
simpa [-mul_inv_rev, norm_smul, hz, zpow_two, ← div_eq_inv_mul] using
  (div_le_div_iff_of_pos_right (mul_pos hR hR)).2 (hC z hz)

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem preimage_inl_image_inr (s : Set β) : Sum.inl ⁻¹' (@Sum.inr α β '' s) = ∅

Proof state:
α : Type u_1
β : Type u_2
s : Set β
⊢ Sum.inl ⁻¹' (Sum.inr '' s) = ∅

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
s : Set β
x✝ : α
⊢ x✝ ∈ Sum.inl ⁻¹' (Sum.inr '' s) ↔ x✝ ∈ ∅

Proof state:
case h
α : Type u_1
β : Type u_2
s : Set β
x✝ : α
⊢ x✝ ∈ Sum.inl ⁻¹' (Sum.inr '' s) ↔ x✝ ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
@[reassoc (attr := simp)]
lemma tensorδ_tensorμ (X₁ X₂ Y₁ Y₂ : C) :
    tensorδ X₁ X₂ Y₁ Y₂ ≫ tensorμ X₁ X₂ Y₁ Y₂ = 𝟙 _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ : C
⊢ tensorδ X₁ X₂ Y₁ Y₂ ≫ tensorμ X₁ X₂ Y₁ Y₂ = 𝟙 ((X₁ ⊗ Y₁) ⊗ X₂ ⊗ Y₂)

Tactic:
simp only [tensorμ, tensorδ, assoc, Iso.inv_hom_id_assoc,
  ← MonoidalCategory.whiskerLeft_comp_assoc, Iso.hom_inv_id_assoc,
  inv_hom_whiskerRight_assoc, Iso.inv_hom_id, Iso.hom_inv_id,
  MonoidalCategory.whiskerLeft_id, id_comp]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma hasDerivAt_mul_log {x : ℝ} (hx : x ≠ 0) : HasDerivAt (fun x ↦ x * log x) (log x + 1) x

Proof state:
x : ℝ
hx : x ≠ 0
⊢ {0}ᶜ ∈ 𝓝 x

Tactic:
simp [hx]

Result:
no goals

Proof state:
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ (fun x => x * log x) x

Tactic:
refine DifferentiableOn.differentiableAt differentiableOn_mul_log ?_

Result:
x : ℝ
hx : x ≠ 0
⊢ {0}ᶜ ∈ 𝓝 x

Proof state:
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt (fun x => x * log x) (log x + 1) x

Tactic:
rw [← deriv_mul_log hx, hasDerivAt_deriv_iff]

Result:
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ (fun x => x * log x) x
-- Mathlib/Data/Set/Basic.lean
theorem ite_inter_self (t s s' : Set α) : t.ite s s' ∩ t = s ∩ t

Proof state:
α : Type u
t s s' : Set α
⊢ t.ite s s' ∩ t = s ∩ t

Tactic:
rw [Set.ite, union_inter_distrib_right, diff_inter_self, inter_assoc, inter_self, union_empty]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem IsInitial.card_le_card {a b : Ordinal} (ha : IsInitial a) : a.card ≤ b.card ↔ a ≤ b

Proof state:
a b : Ordinal.{u_1}
ha : a.IsInitial
h : a ≤ b.card.ord
⊢ a ≤ b

Tactic:
exact h.trans (ord_card_le b)

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
ha : a.IsInitial
h : a.card ≤ b.card
⊢ a ≤ b

Tactic:
rw [← ord_le_ord, ha.ord_card] at h

Result:
a b : Ordinal.{u_1}
ha : a.IsInitial
h : a ≤ b.card.ord
⊢ a ≤ b

Proof state:
a b : Ordinal.{u_1}
ha : a.IsInitial
⊢ a.card ≤ b.card ↔ a ≤ b

Tactic:
refine ⟨fun h ↦ ?_, Ordinal.card_le_card⟩

Result:
a b : Ordinal.{u_1}
ha : a.IsInitial
h : a.card ≤ b.card
⊢ a ≤ b
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isLittleO_iff : f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
⊢ f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
simp only [IsLittleO_def, IsBigOWith_def]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem image_mem_of_mem_comap {f : Filter α} {c : β → α} (h : range c ∈ f) {W : Set β}
    (W_in : W ∈ comap c f) : c '' W ∈ f

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
c : β → α
h : range c ∈ f
W : Set β
W_in : W ∈ comap c f
⊢ c '' W ∈ f

Tactic:
rw [← map_comap_of_mem h]

Result:
α : Type u_1
β : Type u_2
f : Filter α
c : β → α
h : range c ∈ f
W : Set β
W_in : W ∈ comap c f
⊢ c '' W ∈ map c (comap c f)

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
c : β → α
h : range c ∈ f
W : Set β
W_in : W ∈ comap c f
⊢ c '' W ∈ map c (comap c f)

Tactic:
exact image_mem_map W_in

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem intMin_sle (x : BitVec w) : (intMin w).sle x

Proof state:
w : Nat
x : BitVec w
⊢ (intMin w).sle x = true

Tactic:
simp only [BitVec.sle, toInt_intMin_le x, decide_true]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Basic.lean
theorem le_map_mul_map_div [Group α] [CommSemigroup β] [LE β] [SubmultiplicativeHomClass F α β]
    (f : F) (a b : α) : f a ≤ f b * f (a / b)

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : CommSemigroup β
inst✝¹ : LE β
inst✝ : SubmultiplicativeHomClass F α β
f : F
a b : α
⊢ f a ≤ f b * f (a / b)

Tactic:
simpa only [mul_comm, div_mul_cancel] using map_mul_le_mul f (a / b) b

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem prod_apply {s : Set (α × β)} (hs : MeasurableSet s) :
    μ.prod ν s = ∫⁻ x, ν (Prod.mk x ⁻¹' s) ∂μ

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.prod ν) s = ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ

Tactic:
simp_rw [Measure.prod, bind_apply hs (Measurable.map_prod_mk_left (ν := ν)),
  map_apply measurable_prod_mk_left hs]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem minimalPeriod_eq_zero_of_nmem_periodicPts (hx : x ∉ periodicPts f) :
    minimalPeriod f x = 0

Proof state:
α : Type u_1
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ minimalPeriod f x = 0

Tactic:
simp only [minimalPeriod, dif_neg hx]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem map_eq_range_iff {f : G →* N} {H : Subgroup G} :
    H.map f = f.range ↔ Codisjoint H f.ker

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ map f H = f.range ↔ Codisjoint H f.ker

Tactic:
rw [f.range_eq_map, map_eq_map_iff, codisjoint_iff, top_sup_eq]

Result:
no goals
-- Mathlib/Tactic/Abel.lean
theorem zero_smulg {α} [AddCommGroup α] (c) : smulg c (0 : α) = 0

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
c : ℤ
⊢ smulg c 0 = 0

Tactic:
simp [smulg, zsmul_zero]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma mem_Icc_algebraMap_iff_norm_le {x : A} {r : ℝ} (hr : 0 ≤ r) :
    x ∈ Icc 0 (algebraMap ℝ A r) ↔ 0 ≤ x ∧ ‖x‖ ≤ r

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
r : ℝ
hr : 0 ≤ r
⊢ x ∈ Icc 0 ((algebraMap ℝ A) r) ↔ 0 ≤ x ∧ ‖x‖ ≤ r

Tactic:
rw [mem_Icc, and_congr_right_iff, iff_comm]

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ x → (‖x‖ ≤ r ↔ x ≤ (algebraMap ℝ A) r)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem one_le_cosh (x : ℝ) : 1 ≤ cosh x :=
  cosh_zero ▸ cosh_le_cosh.2 (by simp only [_root_.abs_zero, _root_.abs_nonneg])

Proof state:
x : ℝ
⊢ |0| ≤ |x|

Tactic:
simp only [_root_.abs_zero, _root_.abs_nonneg]

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem map_updateCol [DecidableEq n] (f : α → β) :
    map (updateCol M j c) f = updateCol (M.map f) j (f ∘ c)

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
j✝ : n
⊢ (M.updateCol j c).map f i✝ j✝ = (M.map f).updateCol j (f ∘ c) i✝ j✝

Tactic:
rw [updateCol_apply, map_apply, map_apply, updateCol_apply]

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
j✝ : n
⊢ f (if j✝ = j then c i✝ else M i✝ j✝) = if j✝ = j then (f ∘ c) i✝ else f (M i✝ j✝)

Proof state:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
⊢ (M.updateCol j c).map f = (M.map f).updateCol j (f ∘ c)

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
j✝ : n
⊢ (M.updateCol j c).map f i✝ j✝ = (M.map f).updateCol j (f ∘ c) i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
j✝ : n
⊢ f (if j✝ = j then c i✝ else M i✝ j✝) = if j✝ = j then (f ∘ c) i✝ else f (M i✝ j✝)

Tactic:
exact apply_ite f _ _ _

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean
@[reassoc (attr := simp)]
lemma biprodXIso_hom_fst (i : ι) :
    (biprodXIso K L i).hom ≫ biprod.fst = (biprod.fst : K ⊞ L ⟶ K).f i

Proof state:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ (K.biprodXIso L i).hom ≫ biprod.fst = biprod.fst.f i

Tactic:
simp [biprodXIso]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_congr (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f g : α → β
inst✝ : CommMonoid β
h : s₁ = s₂
⊢ (∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g

Tactic:
rw [h]

Result:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f g : α → β
inst✝ : CommMonoid β
h : s₁ = s₂
⊢ (∀ x ∈ s₂, f x = g x) → s₂.prod f = s₂.prod g

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f g : α → β
inst✝ : CommMonoid β
h : s₁ = s₂
⊢ (∀ x ∈ s₂, f x = g x) → s₂.prod f = s₂.prod g

Tactic:
exact fold_congr

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem map_valEmbedding_Ioc : (Ioc a b).map Fin.valEmbedding = Ioc ↑a ↑b

Proof state:
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ioc a b) = Ioc ↑a ↑b

Tactic:
simp [Ioc_eq_finset_subtype, Finset.fin, Finset.map_map, Ioc_filter_lt_of_lt_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_mkArray_singleton : (mkArray n #[a]).flatten = mkArray n a

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ (mkArray n #[a]).flatten.toList = (mkArray n a).toList

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ (mkArray n #[a]).flatten = mkArray n a

Tactic:
rw [← toList_inj]

Result:
n : Nat
α✝ : Type u_1
a : α✝
⊢ (mkArray n #[a]).flatten.toList = (mkArray n a).toList
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem one_le_padicValNat_of_dvd {n : ℕ} [hp : Fact p.Prime] (hn : 0 < n) (div : p ∣ n) :
    1 ≤ padicValNat p n

Proof state:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
div : p ∣ n
⊢ 1 ≤ padicValNat p n

Tactic:
rwa [← WithTop.coe_le_coe, ENat.some_eq_coe, padicValNat_eq_emultiplicity hn,
  ← pow_dvd_iff_le_emultiplicity, pow_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} {h₁} :
    (m.insert k v).getKey a h₁ =
      if h₂ : k == a then
        k
      else
        m.getKey a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂))

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
h₁ : a ∈ m.insert k v
⊢ (m.insert k v).getKey a h₁ = if h₂ : (k == a) = true then k else m.getKey a ⋯

Tactic:
simp_to_raw using Raw₀.getKey_insert ⟨m, _⟩

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem lift_spec_mul_add {g : R →+* P} (hg : ∀ y : M, IsUnit (g y)) (z w w' v) :
    ((toLocalizationWithZeroMap M S).lift g.toMonoidWithZeroHom hg) z * w + w' = v ↔
      g ((toLocalizationMap M S).sec z).1 * w + g ((toLocalizationMap M S).sec z).2 * w' =
        g ((toLocalizationMap M S).sec z).2 * v

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
z : S
w w' v : P
⊢ ↑g.toMonoidWithZeroHom ((toLocalizationWithZeroMap M S).sec z).1 * w +
        g ↑((toLocalizationWithZeroMap M S).sec z).2 * w' =
      g ↑((toLocalizationWithZeroMap M S).sec z).2 * v ↔
    g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
z : S
w w' v : P
⊢ ((toLocalizationWithZeroMap M S).lift g.toMonoidWithZeroHom hg) z * w + w' = v ↔
    g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v

Tactic:
erw [mul_comm, ← mul_assoc, mul_add_inv_left hg, mul_comm]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
z : S
w w' v : P
⊢ ↑g.toMonoidWithZeroHom ((toLocalizationWithZeroMap M S).sec z).1 * w +
        g ↑((toLocalizationWithZeroMap M S).sec z).2 * w' =
      g ↑((toLocalizationWithZeroMap M S).sec z).2 * v ↔
    g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem leadingCoeff_X_pow (n : ℕ) : leadingCoeff ((X : R[X]) ^ n) = 1

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).leadingCoeff = 1

Tactic:
simpa only [C_1, one_mul] using leadingCoeff_C_mul_X_pow (1 : R) n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_tdiv_cancel_of_tmod_eq_zero {a b : Int} (H : a.tmod b = 0) : b * (a.tdiv b) = a

Proof state:
a b : Int
H : a.tmod b = 0
this : a.tmod b + b * a.tdiv b = a
⊢ b * a.tdiv b = a

Tactic:
rwa [H, Int.zero_add] at this

Result:
no goals

Proof state:
a b : Int
H : a.tmod b = 0
⊢ b * a.tdiv b = a

Tactic:
have := tmod_add_tdiv a b

Result:
a b : Int
H : a.tmod b = 0
this : a.tmod b + b * a.tdiv b = a
⊢ b * a.tdiv b = a
-- Mathlib/Analysis/RCLike/Basic.lean
theorem div_re_ofReal {z : K} {r : ℝ} : re (z / r) = re z / r

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ re (z / ↑r) = re z / r

Tactic:
rw [div_eq_inv_mul, div_eq_inv_mul, ← ofReal_inv, re_ofReal_mul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem cpow_natCast (x : ℂ) (n : ℕ) : x ^ (n : ℂ) = x ^ n

Proof state:
x : ℂ
n : ℕ
⊢ x ^ ↑n = x ^ n

Tactic:
simpa using cpow_nat_mul x n 1

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Units.lean
theorem inverse_add_norm_diff_second_order (x : Rˣ) :
    (fun t : R => inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ ^ 2

Proof state:
case h.e'_7.h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
x✝ : R
⊢ inverse (↑x + x✝) - ↑x⁻¹ + ↑x⁻¹ * x✝ * ↑x⁻¹ = inverse (↑x + x✝) - (∑ i ∈ range 2, (-↑x⁻¹ * x✝) ^ i) * ↑x⁻¹

Tactic:
simp only [sum_range_succ, sum_range_zero, zero_add, pow_zero, pow_one, add_mul, one_mul,
  ← sub_sub, neg_mul, sub_neg_eq_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
⊢ (fun t => inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ ^ 2

Tactic:
convert inverse_add_norm_diff_nth_order x 2 using 2

Result:
case h.e'_7.h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
x✝ : R
⊢ inverse (↑x + x✝) - ↑x⁻¹ + ↑x⁻¹ * x✝ * ↑x⁻¹ = inverse (↑x + x✝) - (∑ i ∈ range 2, (-↑x⁻¹ * x✝) ^ i) * ↑x⁻¹
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_reverse {l : List α} :
    l.reverse.Pairwise R ↔ l.Pairwise (fun a b => R b a)

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
⊢ Pairwise R l.reverse ↔ Pairwise (fun a b => R b a) l

Tactic:
induction l <;> simp [*, pairwise_append, and_comm]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp)]
lemma dens_inv [Fintype α] (s : Finset α) : s⁻¹.dens = s.dens

Proof state:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
inst✝ : Fintype α
s : Finset α
⊢ s⁻¹.dens = s.dens

Tactic:
simp [dens]

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

Proof state:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Zero β
inst✝ : SMulZeroClass α β
s : Finset α
⊢ s • 0 ⊆ 0

Tactic:
simp [subset_iff, mem_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_mkArray_self (a : α) (n : Nat) : count a (mkArray n a) = n

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
n : Nat
⊢ count a (mkArray n a) = n

Tactic:
simp [← List.toArray_replicate]

Result:
no goals
-- Mathlib/GroupTheory/Finiteness.lean
theorem Subgroup.fg_iff (P : Subgroup G) :
    Subgroup.FG P ↔ ∃ S : Set G, Subgroup.closure S = P ∧ S.Finite :=
  ⟨fun ⟨S, hS⟩ => ⟨S, hS, Finset.finite_toSet S⟩, fun ⟨S, hS, hf⟩ =>
    ⟨Set.Finite.toFinset hf, by simp [hS]⟩⟩

Proof state:
G : Type u_3
inst✝ : Group G
P : Subgroup G
x✝ : ∃ S, closure S = P ∧ S.Finite
S : Set G
hS : closure S = P
hf : S.Finite
⊢ closure ↑hf.toFinset = P

Tactic:
simp [hS]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem braiding_rightUnitor_aux₁ (X : C) :
    (α_ X (𝟙_ C) (𝟙_ C)).inv ≫
        ((β_ (𝟙_ C) X).inv ▷ 𝟙_ C) ≫ (α_ _ X _).hom ≫ (_ ◁ (ρ_ X).hom) =
      (X ◁ (ρ_ _).hom) ≫ (β_ (𝟙_ C) X).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom =
    X ◁ (ρ_ (𝟙_ C)).hom ≫ (β_ (𝟙_ C) X).inv

Tactic:
monoidal

Result:
no goals
-- Mathlib/CategoryTheory/Category/Cat.lean
lemma associator_hom_app {B C D E : Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : B) :
    (α_ F G H).hom.app X = eqToHom (by simp) :=
  rfl

Proof state:
B C D E : Cat
F : B ⟶ C
G : C ⟶ D
H : D ⟶ E
X : ↑B
⊢ ((F ≫ G) ≫ H).obj X = (F ≫ G ≫ H).obj X

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem smuld_val (n x y : ℤ) : sqrtd * (n : ℤ√d) * ⟨x, y⟩ = ⟨d * n * y, n * x⟩

Proof state:
d n x y : ℤ
⊢ sqrtd * ↑n * { re := x, im := y } = { re := d * n * y, im := n * x }

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
lemma monotone_to_upperTopology_continuous [TopologicalSpace α] [TopologicalSpace β]
    [Topology.IsUpperSet α] [IsUpper β] {f : α → β} (hf : Monotone f) : Continuous f

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper β
f : α → β
hf : Monotone f
s : Set β
hs : IsOpen s
⊢ IsUpperSet (f ⁻¹' s)

Tactic:
exact (IsUpper.isUpperSet_of_isOpen hs).preimage hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper β
f : α → β
hf : Monotone f
⊢ Continuous f

Tactic:
simp_rw [continuous_def, isOpen_iff_isUpperSet]

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper β
f : α → β
hf : Monotone f
⊢ ∀ (s : Set β), IsOpen s → IsUpperSet (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper β
f : α → β
hf : Monotone f
⊢ ∀ (s : Set β), IsOpen s → IsUpperSet (f ⁻¹' s)

Tactic:
intro s hs

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper β
f : α → β
hf : Monotone f
s : Set β
hs : IsOpen s
⊢ IsUpperSet (f ⁻¹' s)
-- Mathlib/Algebra/Homology/ImageToKernel.lean
theorem image_le_kernel (w : f ≫ g = 0) : imageSubobject f ≤ kernelSubobject g :=
  imageSubobject_le_mk _ _ (kernel.lift _ _ w) (by simp)

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ kernel.lift g f w ≫ kernel.ι g = f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Exact.lean
lemma injective_range_liftQ_of_exact (h : Function.Exact f g) :
    Function.Injective ((range f).liftQ g (h · |>.mpr))

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
⊢ Function.Injective ⇑((range f).liftQ g ⋯)

Tactic:
simpa only [← LinearMap.ker_eq_bot, ker_eq_bot_range_liftQ_iff, exact_iff] using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem rev_rev (i : Fin n) : rev (rev i) = i := Fin.ext <| by
  rw [val_rev, val_rev, ← Nat.sub_sub, Nat.sub_sub_self (by exact i.2), Nat.add_sub_cancel]

Proof state:
n : Nat
i : Fin n
⊢ ↑i + 1 ≤ n

Tactic:
exact i.2

Result:
no goals

Proof state:
n : Nat
i : Fin n
⊢ ↑i.rev.rev = ↑i

Tactic:
rw [val_rev, val_rev, ← Nat.sub_sub, Nat.sub_sub_self (by exact i.2), Nat.add_sub_cancel]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma subset_closure_iff_forall_subset_isFlat (X : Set α) (hX : X ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
Y X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ Y ⊆ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F

Tactic:
simp_rw [M.closure_def' X, subset_sInter_iff, mem_setOf, and_imp]

Result:
no goals