harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Prod.lean
theorem prod_eq_bot : f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥

Tactic:
simp_rw [← empty_mem_iff_bot, mem_prod_iff, subset_empty_iff, prod_eq_empty_iff, ← exists_prop,
  Subtype.exists', exists_or, exists_const, Subtype.exists, exists_prop, exists_eq_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem bind_attach {o : Option α} {f : {x // x ∈ o} → Option β} :
    o.attach.bind f = o.pbind fun a h => f ⟨a, h⟩

Proof state:
α : Type u_1
β : Type u_2
o : Option α
f : { x // x ∈ o } → Option β
⊢ o.attach.bind f = o.pbind fun a h => f ⟨a, h⟩

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalWhiskerLeft_of_cons {f g h i j : C}
    (α : g ≅ h) (η : h ⟶ i) {ηs : i ⟶ j} {θ : f ⊗ i ⟶ f ⊗ j} (e_θ : f ◁ ηs = θ) :
    f ◁ (α.hom ≫ η ≫ ηs) = (whiskerLeftIso f α).hom ≫ f ◁ η ≫ θ

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j : C
α : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
θ : f ⊗ i ⟶ f ⊗ j
e_θ : f ◁ ηs = θ
⊢ f ◁ (α.hom ≫ η ≫ ηs) = (whiskerLeftIso f α).hom ≫ f ◁ η ≫ θ

Tactic:
simp [e_θ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem root_X_sub_C : IsRoot (X - C a) b ↔ a = b

Proof state:
R : Type u
a b : R
inst✝ : Ring R
⊢ (X - C a).IsRoot b ↔ a = b

Tactic:
rw [IsRoot.def, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem limitRecOn_isMin (hb : IsMin b) : limitRecOn b hm hs hl = hm b hb

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hm : (a : α) → IsMin a → C a
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccLimit a → ((b : α) → b < a → C b) → C a
hb : IsMin b
⊢ limitRecOn b hm hs hl = hm b hb

Tactic:
rw [limitRecOn, prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_ne {x y : BitVec n} : x ≠ y ↔ x.toNat ≠ y.toNat

Proof state:
n : Nat
x y : BitVec n
⊢ x ≠ y ↔ x.toNat ≠ y.toNat

Tactic:
rw [Ne, toNat_eq]

Result:
no goals
-- Mathlib/RingTheory/Localization/Cardinality.lean
theorem cardinalMk_le {L : Type u} [CommSemiring L] [Algebra R L]
    (S : Submonoid R) [IsLocalization S L] : #L ≤ #R

Proof state:
R : Type u
inst✝³ : CommSemiring R
L : Type u
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
⊢ #L ≤ #R

Tactic:
simpa using lift_cardinalMk_le (L := L) S

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Completion.lean
theorem nnnorm_coe {E} [SeminormedAddCommGroup E] (x : E) : ‖(x : Completion E)‖₊ = ‖x‖₊

Proof state:
E : Type u_2
inst✝ : SeminormedAddCommGroup E
x : E
⊢ ‖↑x‖₊ = ‖x‖₊

Tactic:
simp [nnnorm]

Result:
no goals
-- Mathlib/Algebra/Ring/CharZero.lean
theorem units_ne_neg_self (u : Rˣ) : u ≠ -u

Proof state:
R : Type u_2
inst✝¹ : Ring R
inst✝ : CharZero R
u : Rˣ
⊢ u ≠ -u

Tactic:
simp_rw [ne_eq, Units.ext_iff, Units.val_neg, eq_neg_iff_add_eq_zero, ← two_mul,
  Units.mul_left_eq_zero, two_ne_zero, not_false_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem rightUnitor_inv_naturality {f g : a ⟶ b} (η : f ⟶ g) :
    η ≫ (ρ_ g).inv = (ρ_ f).inv ≫ η ▷ 𝟙 b

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ≫ (ρ_ g).inv = (ρ_ f).inv ≫ η ▷ 𝟙 b

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Conj.lean
theorem trans_conjAut {Z : C} (β : Y ≅ Z) (f : Aut X) :
    (α ≪≫ β).conjAut f = β.conjAut (α.conjAut f)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
Z : C
β : Y ≅ Z
f : Aut X
⊢ (α ≪≫ β).conjAut f = β.conjAut (α.conjAut f)

Tactic:
simp only [conjAut_apply, Iso.trans_symm, Iso.trans_assoc]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma CompleteOrthogonalIdempotents.map_injective_iff (hf : Function.Injective f) :
    CompleteOrthogonalIdempotents (f ∘ e) ↔ CompleteOrthogonalIdempotents e

Proof state:
R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
I : Type u_3
e : I → R
inst✝ : Fintype I
hf : Function.Injective ⇑f
⊢ CompleteOrthogonalIdempotents (⇑f ∘ e) ↔ CompleteOrthogonalIdempotents e

Tactic:
simp [completeOrthogonalIdempotents_iff, ← hf.eq_iff, apply_ite,
  OrthogonalIdempotents.map_injective_iff f hf]

Result:
no goals
-- Mathlib/LinearAlgebra/Semisimple.lean
lemma IsSemisimple_smul_iff {t : K} (ht : t ≠ 0) :
    (t • f).IsSemisimple ↔ f.IsSemisimple

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
t : K
ht : t ≠ 0
⊢ (t • f).IsSemisimple ↔ f.IsSemisimple

Tactic:
simp [isSemisimple_iff, mem_invtSubmodule, Submodule.comap_smul f (h := ht)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
    m.1.isEmpty = false ↔ ∃ a, m.contains a = true

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
⊢ m.val.isEmpty = false ↔ ∃ a, m.contains a = true

Tactic:
simp_to_model using List.isEmpty_eq_false_iff_exists_containsKey

Result:
no goals
-- Mathlib/Data/Fintype/Inv.lean
theorem invOfMemRange_surjective : Function.Surjective f.invOfMemRange := fun a =>
  ⟨⟨f a, Set.mem_range_self a⟩, by simp⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α ↪ β
a : α
⊢ f.invOfMemRange ⟨f a, ⋯⟩ = a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_one_sub' (h : 1 - y ≠ 0) (x : ℝ≥0) : x ^ (1 - y) = x / x ^ y

Proof state:
y : ℝ
h : 1 - y ≠ 0
x : ℝ≥0
⊢ x ^ (1 - y) = x / x ^ y

Tactic:
rw [rpow_sub' h, rpow_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem drop_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) :
    (l₁ ++ l₂).drop n = l₁.drop n ++ l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
n : Nat
h : n ≤ l₁.length
⊢ drop n (l₁ ++ l₂) = drop n l₁ ++ l₂

Tactic:
simp [drop_append_eq_append_drop, Nat.sub_eq_zero_of_le h]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernelSubobject_comp_le (f : X ⟶ Y) [HasKernel f] {Z : C} (h : Y ⟶ Z) [HasKernel (f ≫ h)] :
    kernelSubobject f ≤ kernelSubobject (f ≫ h) :=
  le_kernelSubobject _ _ (by simp)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : HasKernel (f ≫ h)
⊢ (kernelSubobject f).arrow ≫ f ≫ h = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_eq_empty : p.support = ∅ ↔ p = 0

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ { toFinsupp := toFinsupp✝ }.support = ∅ ↔ { toFinsupp := toFinsupp✝ } = 0

Tactic:
simp [support]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.support = ∅ ↔ p = 0

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ { toFinsupp := toFinsupp✝ }.support = ∅ ↔ { toFinsupp := toFinsupp✝ } = 0
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
theorem cancel_right_of_respectsIso (P : MorphismProperty C) [hP : RespectsIso P] {X Y Z : C}
    (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] : P (f ≫ g) ↔ P f :=
  ⟨fun h => by simpa using RespectsIso.postcomp P (inv g) (f ≫ g) h, RespectsIso.postcomp P g f⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
h : P (f ≫ g)
⊢ P f

Tactic:
simpa using RespectsIso.postcomp P (inv g) (f ≫ g) h

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
lemma insertNth_self_removeNth (p : Fin (n + 1)) (f : ∀ j, α j) :
    insertNth p (f p) (removeNth p f) = f

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
f : (j : Fin (n + 1)) → α j
⊢ p.insertNth (f p) (p.removeNth f) = f

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem exists_eq_right_right' : (∃ (a : α), p a ∧ q a ∧ a' = a) ↔ p a' ∧ q a'

Proof state:
α : Sort u_1
p q : α → Prop
a' : α
⊢ (∃ a, p a ∧ q a ∧ a' = a) ↔ p a' ∧ q a'

Tactic:
simp [@eq_comm _ a']

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iUnion_Ico_right [NoMaxOrder α] (a : α) : ⋃ b, Ico a b = Ici a

Proof state:
α : Type v
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
⊢ ⋃ b, Ico a b = Ici a

Tactic:
simp only [← Ici_inter_Iio, ← inter_iUnion, iUnion_Iio, inter_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/GetElem.lean
theorem isSome_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
    (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isSome = dom c i

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
c : cont
i : idx
inst✝ : Decidable (dom c i)
⊢ ((getElem? c i).isSome = true) = dom c i

Tactic:
simp only [getElem?_def]

Result:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
c : cont
i : idx
inst✝ : Decidable (dom c i)
⊢ ((if h : dom c i then some (getElem c i h) else none).isSome = true) = dom c i

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
c : cont
i : idx
inst✝ : Decidable (dom c i)
⊢ ((if h : dom c i then some (getElem c i h) else none).isSome = true) = dom c i

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
@[simp] lemma set_smul_bot : s • (⊥ : Submodule R M) = ⊥ :=
  eq_bot_iff.mpr fun x hx ↦ by induction x, hx using set_smul_inductionOn <;> aesop

Proof state:
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
x : M
hx : x ∈ s • ⊥
⊢ x ∈ ⊥

Tactic:
induction x, hx using set_smul_inductionOn <;> aesop

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem compl_le [LinearOrder α] : (· ≤ · : α → α → _)ᶜ = (· > ·)

Proof state:
case h.h.a
α : Type u_2
inst✝ : LinearOrder α
x✝¹ x✝ : α
⊢ (fun x1 x2 => x1 ≤ x2)ᶜ x✝¹ x✝ ↔ x✝¹ > x✝

Tactic:
simp [compl]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 => x1 ≤ x2)ᶜ = fun x1 x2 => x1 > x2

Tactic:
ext

Result:
case h.h.a
α : Type u_2
inst✝ : LinearOrder α
x✝¹ x✝ : α
⊢ (fun x1 x2 => x1 ≤ x2)ᶜ x✝¹ x✝ ↔ x✝¹ > x✝
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem derivWithin_const_mul (c : 𝔸) (hd : DifferentiableWithinAt 𝕜 d s x) :
    derivWithin (fun y => c * d y) s x = c * derivWithin d s x

Proof state:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
c : 𝔸
hd : DifferentiableWithinAt 𝕜 d s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => c * d y) s x = c * derivWithin d s x

Tactic:
exact (hd.hasDerivWithinAt.const_mul c).derivWithin hxs

Result:
no goals

Proof state:
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
c : 𝔸
hd : DifferentiableWithinAt 𝕜 d s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => c * d y) s x = c * derivWithin d s x

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
c : 𝔸
hd : DifferentiableWithinAt 𝕜 d s x
⊢ derivWithin (fun y => c * d y) s x = c * derivWithin d s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
c : 𝔸
hd : DifferentiableWithinAt 𝕜 d s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => c * d y) s x = c * derivWithin d s x

case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
c : 𝔸
hd : DifferentiableWithinAt 𝕜 d s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => c * d y) s x = c * derivWithin d s x
-- Mathlib/Data/Finset/Functor.lean
theorem image₂_def {α β γ : Type u} (f : α → β → γ) (s : Finset α) (t : Finset β) :
    image₂ f s t = f <$> s <*> t

Proof state:
inst✝ : (P : Prop) → Decidable P
α β γ : Type u
f : α → β → γ
s : Finset α
t : Finset β
⊢ image₂ f s t = f <$> s <*> t

Tactic:
ext

Result:
case h
inst✝ : (P : Prop) → Decidable P
α β γ : Type u
f : α → β → γ
s : Finset α
t : Finset β
a✝ : γ
⊢ a✝ ∈ image₂ f s t ↔ a✝ ∈ f <$> s <*> t

Proof state:
case h
inst✝ : (P : Prop) → Decidable P
α β γ : Type u
f : α → β → γ
s : Finset α
t : Finset β
a✝ : γ
⊢ a✝ ∈ image₂ f s t ↔ a✝ ∈ f <$> s <*> t

Tactic:
simp [mem_sup]

Result:
no goals
-- Mathlib/Algebra/Category/Semigrp/Basic.lean
@[to_additive]
lemma comp_apply {M N T : MagmaCat} (f : M ⟶ N) (g : N ⟶ T) (x : M) :
    (f ≫ g) x = g (f x)

Proof state:
M N T : MagmaCat
f : M ⟶ N
g : N ⟶ T
x : ↑M
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem nat_card_centralizer :
    Nat.card (centralizer {g}) =
      (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        (∏ n ∈ g.cycleType.toFinset, (g.cycleType.count n)!)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↥(centralizer {g}) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
rw [← (toPermHom g).ker.card_mul_index, index_ker, nat_card_range_toPermHom,
  ← kerParam_range_card, ← Nat.card_eq_fintype_card, kerParam_range_eq, card_subtype]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem nhds_prod_eq {x : X} {y : Y} : 𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ 𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y

Tactic:
rw [prod_eq_inf, instTopologicalSpaceProd, nhds_inf (t₁ := TopologicalSpace.induced Prod.fst _)
  (t₂ := TopologicalSpace.induced Prod.snd _), nhds_induced, nhds_induced]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma inv_rnDeriv' [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
    (ν.rnDeriv μ)⁻¹ =ᵐ[μ] μ.rnDeriv ν

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ (ν.rnDeriv μ)⁻¹ x = μ.rnDeriv ν x

Tactic:
simp only [Pi.inv_apply, ← hx, inv_inv]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ (ν.rnDeriv μ)⁻¹ =ᶠ[ae μ] μ.rnDeriv ν

Tactic:
filter_upwards [inv_rnDeriv hμν] with x hx

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ (ν.rnDeriv μ)⁻¹ x = μ.rnDeriv ν x
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
@[simp]
lemma pairingIn_reflection_perm_self_left [FaithfulSMul S R] [P.IsValuedIn S] (i j : ι) :
    P.pairingIn S (P.reflection_perm i i) j = - P.pairingIn S i j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : FaithfulSMul S R
inst✝ : P.IsValuedIn S
i j : ι
⊢ P.pairingIn S ((P.reflection_perm i) i) j = -P.pairingIn S i j

Tactic:
simp [← (FaithfulSMul.algebraMap_injective S R).eq_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem sum_toArray [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum

Proof state:
α : Type u_1
inst✝¹ : Add α
inst✝ : Zero α
l : List α
⊢ l.toArray.sum = l.sum

Tactic:
simp [Array.sum, List.sum]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean
@[reassoc (attr := simp, elementwise)]
lemma toCycles_moduleCatCyclesIso_hom :
    S.toCycles ≫ S.moduleCatCyclesIso.hom = ModuleCat.ofHom S.moduleCatToCycles

Proof state:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.toCycles ≫ S.moduleCatCyclesIso.hom = ModuleCat.ofHom S.moduleCatToCycles

Tactic:
rw [← cancel_mono S.moduleCatLeftHomologyData.i, moduleCatLeftHomologyData_i,
  Category.assoc, S.moduleCatCyclesIso_hom_subtype, toCycles_i]

Result:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.f = ModuleCat.ofHom S.moduleCatToCycles ≫ ModuleCat.ofHom (LinearMap.ker (ModuleCat.Hom.hom S.g)).subtype

Proof state:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.f = ModuleCat.ofHom S.moduleCatToCycles ≫ ModuleCat.ofHom (LinearMap.ker (ModuleCat.Hom.hom S.g)).subtype

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Char/Lemmas.lean
theorem le_refl (a : Char) : a ≤ a

Proof state:
a : Char
⊢ a ≤ a

Tactic:
simp [le_def]

Result:
no goals
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_moveLeft_hEq {o : Ordinal} :
    HEq o.toPGame.moveLeft fun x : o.toType => ((enumIsoToType o).symm x).val.toPGame

Proof state:
o : Ordinal.{u_1}
⊢ HEq o.toPGame.moveLeft fun x => (↑(o.enumIsoToType.symm x)).toPGame

Tactic:
rw [toPGame]

Result:
o : Ordinal.{u_1}
⊢ HEq (mk o.toType PEmpty.{u_1 + 1} (fun x => (↑(o.enumIsoToType.symm x)).toPGame) PEmpty.elim).moveLeft fun x =>
    (↑(o.enumIsoToType.symm x)).toPGame

Proof state:
o : Ordinal.{u_1}
⊢ HEq (mk o.toType PEmpty.{u_1 + 1} (fun x => (↑(o.enumIsoToType.symm x)).toPGame) PEmpty.elim).moveLeft fun x =>
    (↑(o.enumIsoToType.symm x)).toPGame

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toList_perm_toListModel {m : Raw α β} : Perm m.toList (toListModel m.buckets)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
⊢ m.toList ~ toListModel m.buckets

Tactic:
simp [Raw.toList, foldRev_cons]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem HasDerivAt.norm_sq {f : ℝ → F} {f' : F} {x : ℝ} (hf : HasDerivAt f f' x) :
    HasDerivAt (‖f ·‖ ^ 2) (2 * Inner.inner (f x) f') x

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
f : ℝ → F
f' : F
x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun x => ‖f x‖ ^ 2) (2 * Inner.inner (f x) f') x

Tactic:
simpa using hf.hasFDerivAt.norm_sq.hasDerivAt

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_union_left (s₁ s₂ t : Set E) :
    convexJoin 𝕜 (s₁ ∪ s₂) t = convexJoin 𝕜 s₁ t ∪ convexJoin 𝕜 s₂ t

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s₁ s₂ t : Set E
⊢ convexJoin 𝕜 (s₁ ∪ s₂) t = convexJoin 𝕜 s₁ t ∪ convexJoin 𝕜 s₂ t

Tactic:
simp_rw [convexJoin, mem_union, iUnion_or, iUnion_union_distrib]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Tendsto.atBot_zsmul_neg_const {f : α → ℤ} (hr : r < 0) (hf : Tendsto f l atBot) :
    Tendsto (fun x => f x • r) l atTop

Proof state:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto (fun x => f x • r) l atTop

Tactic:
simpa using hf.atBot_zsmul_const (neg_pos.2 hr)

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasFDerivWithinAt_univ : HasFDerivWithinAt f f' univ x ↔ HasFDerivAt f f' x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
⊢ HasFDerivWithinAt f f' univ x ↔ HasFDerivAt f f' x

Tactic:
simp only [HasFDerivWithinAt, nhdsWithin_univ, HasFDerivAt]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem taylor_coeff_one : (taylor r f).coeff 1 = f.derivative.eval r

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ((taylor r) f).coeff 1 = eval r (derivative f)

Tactic:
rw [taylor_coeff, hasseDeriv_one]

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplexSymmetry.lean
@[reassoc]
lemma totalFlipIso_hom_f_D₂ (j j' : J) :
    (K.totalFlipIso c).hom.f j ≫ K.D₂ c j j' =
      K.flip.D₁ c j j' ≫ (K.totalFlipIso c).hom.f j'

Proof state:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{u_5, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
⊢ (K.totalFlipIso c).hom.f j ≫ K.D₂ c j j' = K.flip.D₁ c j j' ≫ (K.totalFlipIso c).hom.f j'

Tactic:
apply totalFlipIsoX_hom_D₂

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma π_comp_colimitUnopIsoOpLimit_inv (F : Jᵒᵖ ⥤ Cᵒᵖ) [HasLimit F] (j : Jᵒᵖ) :
    (limit.π F j).unop ≫ (colimitUnopIsoOpLimit F).inv = colimit.ι F.unop j.unop

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
inst✝ : HasLimit F
j : Jᵒᵖ
⊢ (limit.π F j).unop ≫ (colimitUnopIsoOpLimit F).inv = colimit.ι F.unop (unop j)

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range'_1_concat (s n : Nat) : range' s (n + 1) = range' s n ++ [s + n]

Proof state:
s n : Nat
⊢ range' s (n + 1) = range' s n ++ [s + n]

Tactic:
simp [range'_concat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem any_eq_true {p : α → Bool} {xs : Vector α n} :
    xs.any p = true ↔ ∃ (i : Nat) (_ : i < n), p xs[i]

Proof state:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ xs.any p = true ↔ ∃ i x, p xs[i] = true

Tactic:
simp [any_iff_exists]

Result:
no goals
-- Mathlib/Topology/Algebra/WithZeroTopology.lean
theorem singleton_mem_nhds_of_units (γ : Γ₀ˣ) : ({↑γ} : Set Γ₀) ∈ 𝓝 (γ : Γ₀)

Proof state:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ : Γ₀ˣ
⊢ {↑γ} ∈ 𝓝 ↑γ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_cons {a : α} : (a::l).getLast? = l.getLast?.getD a

Proof state:
α : Type u_1
l : List α
a : α
⊢ (a :: l).getLast? = some (l.getLast?.getD a)

Tactic:
cases l <;> simp [getLast?, getLast]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_neg (n : ℤ) : S R (-n) = -S R (n - 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ S R (-n) = -S R (n - 2)

Tactic:
simpa [sub_sub] using S_neg_sub_one R (n - 1)

Result:
no goals
-- Mathlib/Algebra/Ring/Divisibility/Basic.lean
theorem dvd_add_left (h : a ∣ c) : a ∣ b + c ↔ a ∣ b :=
  ⟨fun H => by simpa only [add_sub_cancel_right] using dvd_sub H h, fun h₂ => dvd_add h₂ h⟩

Proof state:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ c
H : a ∣ b + c
⊢ a ∣ b

Tactic:
simpa only [add_sub_cancel_right] using dvd_sub H h

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem card_fintypeIoi : Fintype.card (Set.Ioi a) = n - 1 - a

Proof state:
n : ℕ
a : Fin n
⊢ Fintype.card ↑(Set.Ioi a) = n - 1 - ↑a

Tactic:
rw [Fintype.card_ofFinset, card_Ioi]

Result:
no goals