harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Shift/Localization.lean
lemma commShiftOfLocalization_iso_hom_app (a : A) (X : C) :
    letI := Functor.commShiftOfLocalization L W A F F'
    (F'.commShiftIso a).hom.app (L.obj X) =
      F'.map ((L.commShiftIso a).inv.app X) ≫ (Lifting.iso L W F F').hom.app (X⟦a⟧) ≫
        (F.commShiftIso a).hom.app X ≫
          (shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)

Proof state:
C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a : A
X : C
⊢ (F'.commShiftIso a).hom.app (L.obj X) =
    F'.map ((L.commShiftIso a).inv.app X) ≫
      (Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X) ≫
        (F.commShiftIso a).hom.app X ≫ (shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)

Tactic:
apply commShiftOfLocalization.iso_hom_app

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem piCongrLeft_preimage_univ_pi (f : ι' ≃ ι) (t : ∀ i, Set (α i)) :
    f.piCongrLeft α ⁻¹' univ.pi t = univ.pi fun i => t (f i)

Proof state:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
t : (i : ι) → Set (α i)
⊢ ⇑(piCongrLeft α f) ⁻¹' univ.pi t = univ.pi fun i => t (f i)

Tactic:
simpa [f.surjective.range_eq] using piCongrLeft_preimage_pi f univ t

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem Fork.condition (t : Fork f g) : t.ι ≫ f = t.ι ≫ g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
t : Fork f g
⊢ t.ι ≫ f = t.ι ≫ g

Tactic:
rw [← t.app_one_eq_ι_comp_left, ← t.app_one_eq_ι_comp_right]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iInter_setOf (P : ι → α → Prop) : ⋂ i, { x : α | P i x } = { x : α | ∀ i, P i x }

Proof state:
case h
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
x✝ : α
⊢ x✝ ∈ ⋂ i, {x | P i x} ↔ x✝ ∈ {x | ∀ (i : ι), P i x}

Tactic:
exact mem_iInter

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
⊢ ⋂ i, {x | P i x} = {x | ∀ (i : ι), P i x}

Tactic:
ext

Result:
case h
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
x✝ : α
⊢ x✝ ∈ ⋂ i, {x | P i x} ↔ x✝ ∈ {x | ∀ (i : ι), P i x}
-- Mathlib/Data/Set/Image.lean
theorem image_diff_preimage {f : α → β} {s : Set α} {t : Set β} :
    f '' (s \ f ⁻¹' t) = f '' s \ t

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (s \ f ⁻¹' t) = f '' s \ t

Tactic:
simp_rw [diff_eq, ← preimage_compl, image_inter_preimage]

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem finiteType_iff_group_fg {G : Type*} [AddCommGroup G] [CommRing R] [Nontrivial R] :
    FiniteType R R[G] ↔ AddGroup.FG G

Proof state:
R : Type u_1
G : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ FiniteType R R[G] ↔ AddGroup.FG G

Tactic:
simpa [AddGroup.fg_iff_addMonoid_fg] using finiteType_iff_fg

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem join_cons_nil (a : α) (S) : join (cons (a, nil) S) = cons a (join S) :=
  destruct_eq_cons <| by simp [join]

Proof state:
α : Type u
a : α
S : Seq (Seq1 α)
⊢ (cons (a, nil) S).join.destruct = some (a, S.join)

Tactic:
simp [join]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_neg : cosh (-x) = cosh x :=
  ofReal_inj.1 <| by simp

Proof state:
x : ℝ
⊢ ↑(cosh (-x)) = ↑(cosh x)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_replicate_of_none {f : α → Option β} (h : f a = none) :
    (replicate n a).filterMap f = []

Proof state:
α : Type u_1
β : Type u_2
a : α
n : Nat
f : α → Option β
h : f a = none
⊢ filterMap f (replicate n a) = []

Tactic:
simp [filterMap_replicate, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_alter_eq_self_of_not_mem [LawfulBEq α] (h : m.1.WF) {k : α}
    {f : Option (β k) → Option (β k)} (h₁ : m.contains k = false) (h₂ : (f (m.get? k)).isNone) :
    (m.alter k f).1.size = m.1.size

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
h₁ : m.contains k = false
h₂ : (f (m.get? k)).isNone = true
⊢ (m.alter k f).val.size = m.val.size

Tactic:
simp [size_alter, h, h₁, h₂]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma smul_iSup {R} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (f : ι → ℝ≥0∞) (c : R) :
    c • ⨆ i, f i = ⨆ i, c • f i

Proof state:
ι : Sort u_1
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
f : ι → ℝ≥0∞
c : R
⊢ c • ⨆ i, f i = ⨆ i, c • f i

Tactic:
simp only [← smul_one_mul c (f _), ← smul_one_mul c (iSup _), ENNReal.mul_iSup]

Result:
no goals
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem HasDerivAtFilter.hasGradientAtFilter (h : HasDerivAtFilter g g' u L') :
    HasGradientAtFilter g (starRingEnd 𝕜 g') u L'

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasDerivAtFilter g g' u L'
⊢ ContinuousLinearMap.smulRight 1 g' = (toDual 𝕜 𝕜) ((starRingEnd 𝕜) g')

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasDerivAtFilter g g' u L'
⊢ (ContinuousLinearMap.smulRight 1 g') 1 = ((toDual 𝕜 𝕜) ((starRingEnd 𝕜) g')) 1

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasDerivAtFilter g g' u L'
this : ContinuousLinearMap.smulRight 1 g' = (toDual 𝕜 𝕜) ((starRingEnd 𝕜) g')
⊢ HasGradientAtFilter g ((starRingEnd 𝕜) g') u L'

Tactic:
rwa [HasGradientAtFilter, ← this]

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasDerivAtFilter g g' u L'
⊢ (ContinuousLinearMap.smulRight 1 g') 1 = ((toDual 𝕜 𝕜) ((starRingEnd 𝕜) g')) 1

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasDerivAtFilter g g' u L'
⊢ HasGradientAtFilter g ((starRingEnd 𝕜) g') u L'

Tactic:
have : ContinuousLinearMap.smulRight (1 : 𝕜 →L[𝕜] 𝕜) g' = (toDual 𝕜 𝕜) (starRingEnd 𝕜 g') := by
  ext; simp

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasDerivAtFilter g g' u L'
this : ContinuousLinearMap.smulRight 1 g' = (toDual 𝕜 𝕜) ((starRingEnd 𝕜) g')
⊢ HasGradientAtFilter g ((starRingEnd 𝕜) g') u L'
-- Mathlib/Topology/PartialHomeomorph.lean
theorem eventually_nhds {x : X} (p : Y → Prop) (hx : x ∈ e.source) :
    (∀ᶠ y in 𝓝 (e x), p y) ↔ ∀ᶠ x in 𝓝 x, p (e x) :=
  Iff.trans (by rw [e.map_nhds_eq hx]) eventually_map

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
p : Y → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝 (↑e x), p y) ↔ ∀ᶠ (b : Y) in map (↑e) (𝓝 x), p b

Tactic:
rw [e.map_nhds_eq hx]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C
    (hx : AlgebraicIndependent R x) (r) :
    hx.mvPolynomialOptionEquivPolynomialAdjoin (C r) = Polynomial.C (algebraMap _ _ r)

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
r : R
⊢ hx.mvPolynomialOptionEquivPolynomialAdjoin (C r) = Polynomial.C ((algebraMap R ↥(adjoin R (range x))) r)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive abs_sub_eq_two_nsmul_negPart]
lemma mabs_div_eq_leOnePart_sq (a : α) : |a|ₘ / a = a⁻ᵐ ^ 2

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ mabs a / a = a⁻ᵐ ^ 2

Tactic:
rw [sq, ← mul_div_div_cancel, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem nilradical_eq_iInf : nilradical R = iInf asIdeal

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ nilradical R = iInf asIdeal

Tactic:
apply range_asIdeal R ▸ nilradical_eq_sInf R

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
theorem map_comp (f : M →ₗ[R] N) (g : N →ₗ[R] N') :
    map n (g ∘ₗ f) = map n g ∘ₗ map n f

Proof state:
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : M →ₗ[R] N
g : N →ₗ[R] N'
⊢ map n (g ∘ₗ f) = map n g ∘ₗ map n f

Tactic:
aesop

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
@[to_additive]
lemma IsCyclic.card_orderOf_eq_totient [IsCyclic α] [Fintype α] {d : ℕ} (hd : d ∣ Fintype.card α) :
    #{a : α | orderOf a = d} = totient d

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
d : ℕ
hd : d ∣ Fintype.card α
⊢ #(filter (fun a => orderOf a = d) univ) = φ d

Tactic:
classical apply card_orderOf_eq_totient_aux₂ (fun n => IsCyclic.card_pow_eq_one_le) hd

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
d : ℕ
hd : d ∣ Fintype.card α
⊢ #(filter (fun a => orderOf a = d) univ) = φ d

Tactic:
apply card_orderOf_eq_totient_aux₂ (fun n => IsCyclic.card_pow_eq_one_le) hd

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mem_range {m n : Nat} : m ∈ range n ↔ m < n

Proof state:
m n : Nat
⊢ m ∈ range n ↔ m < n

Tactic:
simp only [range_eq_range', mem_range'_1, Nat.zero_le, true_and, Nat.zero_add]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem sameCycle_apply_left : SameCycle f (f x) y ↔ SameCycle f x y :=
  (Equiv.addRight 1).exists_congr_left.trans <| by
    simp [zpow_sub, SameCycle, Int.add_neg_one, Function.comp]

Proof state:
α : Type u_2
f : Perm α
x y : α
⊢ (∃ b, (f ^ (Equiv.symm (Equiv.addRight 1)) b) (f x) = y) ↔ f.SameCycle x y

Tactic:
simp [zpow_sub, SameCycle, Int.add_neg_one, Function.comp]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem dvd_C_mul (ha : a ≠ 0) : p ∣ Polynomial.C a * q ↔ p ∣ q :=
  ⟨fun ⟨r, hr⟩ =>
    ⟨C a⁻¹ * r, by
      rw [mul_left_comm p, ← hr, ← mul_assoc, ← C.map_mul, inv_mul_cancel₀ ha, C.map_one,
        one_mul]⟩,
    fun h => dvd_trans h (dvd_mul_left _ _)⟩

Proof state:
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a ≠ 0
x✝ : p ∣ C a * q
r : R[X]
hr : C a * q = p * r
⊢ q = p * (C a⁻¹ * r)

Tactic:
rw [mul_left_comm p, ← hr, ← mul_assoc, ← C.map_mul, inv_mul_cancel₀ ha, C.map_one,
  one_mul]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Rat.comap_cast_atTop [LinearOrderedField R] [Archimedean R] :
    comap ((↑) : ℚ → R) atTop = atTop :=
  comap_embedding_atTop (fun _ _ => Rat.cast_le) fun r =>
    let ⟨n, hn⟩ := exists_nat_ge r; ⟨n, by simpa⟩

Proof state:
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
r : R
n : ℕ
hn : r ≤ ↑n
⊢ r ≤ ↑↑n

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldrM_append [Monad m] [LawfulMonad m] (f : α → β → m β) (b) (l l' : Array α) :
    (l ++ l').foldrM f b = l'.foldrM f b >>= l.foldrM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l l' : Array α
⊢ foldrM f b (l ++ l') = do
    let init ← foldrM f b l'
    foldrM f init l

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem measure_sUnion_null_iff {S : Set (Set α)} (hS : S.Countable) :
    μ (⋃₀ S) = 0 ↔ ∀ s ∈ S, μ s = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
S : Set (Set α)
hS : S.Countable
⊢ μ (⋃₀ S) = 0 ↔ ∀ s ∈ S, μ s = 0

Tactic:
rw [sUnion_eq_biUnion, measure_biUnion_null_iff hS]

Result:
no goals
-- Mathlib/Algebra/Module/Equiv/Defs.lean
theorem toFun_eq_coe : e.toFun = e

Proof state:
R : Type u_1
S : Type u_5
M : Type u_6
M₂ : Type u_8
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
⊢ (↑e).toFun = ⇑e

Tactic:
dsimp

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iInf_le_iff {s : ι → α} : iInf s ≤ a ↔ ∀ b, (∀ i, b ≤ s i) → b ≤ a

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteSemilatticeInf α
a : α
s : ι → α
⊢ iInf s ≤ a ↔ ∀ (b : α), (∀ (i : ι), b ≤ s i) → b ≤ a

Tactic:
simp [iInf, sInf_le_iff, lowerBounds]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem extendScalars_top : extendScalars (le_top : F ≤ ⊤) = ⊤ :=
  IntermediateField.toSubfield_injective (by simp)

Proof state:
L : Type u_2
inst✝ : Field L
F : Subfield L
⊢ (extendScalars ⋯).toSubfield = ⊤.toSubfield

Tactic:
simp

Result:
no goals
-- Mathlib/Order/MinMax.lean
theorem min_lt_min_left_iff : min a c < min b c ↔ a < b ∧ a < c

Proof state:
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ a ⊓ c < b ⊓ c ↔ a < b ∧ a < c

Tactic:
simp_rw [lt_min_iff, min_lt_iff, or_iff_left (lt_irrefl _)]

Result:
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ (a < b ∨ c < b) ∧ a < c ↔ a < b ∧ a < c

Proof state:
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ (a < b ∨ c < b) ∧ a < c ↔ a < b ∧ a < c

Tactic:
exact and_congr_left fun h => or_iff_left_of_imp h.trans

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem onFinset_prod {s : Finset α} {f : α → M} {g : α → M → N} (hf : ∀ a, f a ≠ 0 → a ∈ s)
    (hg : ∀ a, g a 0 = 1) : (onFinset s f hf).prod g = ∏ a ∈ s, g a (f a) :=
  Finset.prod_subset support_onFinset_subset <| by simp +contextual [*]

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : α → M
g : α → M → N
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
hg : ∀ (a : α), g a 0 = 1
⊢ ∀ x ∈ s, x ∉ (onFinset s f hf).support → g x ((onFinset s f hf) x) = 1

Tactic:
simp +contextual [*]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem inner_indicatorConstLp_eq_inner_setIntegral [CompleteSpace E] [NormedSpace ℝ E]
    (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (c : E) (f : Lp E 2 μ) :
    (⟪indicatorConstLp 2 hs hμs c, f⟫ : 𝕜) = ⟪c, ∫ x in s, f x ∂μ⟫

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁵ : RCLike 𝕜
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
s : Set α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
f : ↥(Lp E 2 μ)
⊢ inner (indicatorConstLp 2 hs hμs c) f = inner c (∫ (x : α) in s, ↑↑f x ∂μ)

Tactic:
rw [← integral_inner (integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs),
  L2.inner_indicatorConstLp_eq_setIntegral_inner]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderiv_mem_iff {f : E → F} {s : Set (E →L[𝕜] F)} {x : E} : fderiv 𝕜 f x ∈ s ↔
    DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ (0 : E →L[𝕜] F) ∈ s

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
s : Set (E →L[𝕜] F)
x : E
⊢ fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s

Tactic:
by_cases hx : DifferentiableAt 𝕜 f x <;> simp [fderiv_zero_of_not_differentiableAt, *]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[simp] lemma enorm_ne_top : ‖x‖ₑ ≠ ∞

Proof state:
E : Type u_8
inst✝ : NNNorm E
x : E
⊢ ‖x‖ₑ ≠ ⊤

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
lemma binEntropy_eq_log_two : binEntropy p = log 2 ↔ p = 2⁻¹

Proof state:
p : ℝ
⊢ binEntropy p = log 2 ↔ p = 2⁻¹

Tactic:
rw [binEntropy_le_log_two.eq_iff_not_lt, binEntropy_lt_log_two, not_ne_iff]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem vector_get {n} : Primrec₂ (@List.Vector.get α n) :=
  option_some_iff.1 <|
    (list_get?.comp (vector_toList.comp fst) (fin_val.comp snd)).of_eq fun a => by
      rw [Vector.get_eq_get_toList, ← List.get?_eq_get]
      rfl

Proof state:
α : Type u_1
inst✝ : Primcodable α
n : ℕ
a : List.Vector α n × Fin n
⊢ a.1.toList.get? ↑a.2 = some (a.1.get a.2)

Tactic:
rw [Vector.get_eq_get_toList, ← List.get?_eq_get]

Result:
α : Type u_1
inst✝ : Primcodable α
n : ℕ
a : List.Vector α n × Fin n
⊢ a.1.toList.get? ↑a.2 = a.1.toList.get? ↑(Fin.cast ⋯ a.2)

Proof state:
α : Type u_1
inst✝ : Primcodable α
n : ℕ
a : List.Vector α n × Fin n
⊢ a.1.toList.get? ↑a.2 = a.1.toList.get? ↑(Fin.cast ⋯ a.2)

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem vectorSpan_pair_rev (p₁ p₂ : P) : vectorSpan k ({p₁, p₂} : Set P) = k ∙ p₂ -ᵥ p₁

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
⊢ vectorSpan k {p₁, p₂} = Submodule.span k {p₂ -ᵥ p₁}

Tactic:
rw [pair_comm, vectorSpan_pair]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem image_openSegment (f : E →ᵃ[𝕜] F) (a b : E) :
    f '' openSegment 𝕜 a b = openSegment 𝕜 (f a) (f b) :=
  Set.ext fun x => by
    simp_rw [openSegment_eq_image_lineMap, mem_image, exists_exists_and_eq_and,
      AffineMap.apply_lineMap]

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
⊢ x ∈ ⇑f '' openSegment 𝕜 a b ↔ x ∈ openSegment 𝕜 (f a) (f b)

Tactic:
simp_rw [openSegment_eq_image_lineMap, mem_image, exists_exists_and_eq_and,
  AffineMap.apply_lineMap]

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
lemma Algebra.intNorm_ne_zero {x : B} : Algebra.intNorm A B x ≠ 0 ↔ x ≠ 0

Proof state:
A : Type u_1
B : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
x : B
⊢ (intNorm A B) x ≠ 0 ↔ x ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_pos_iff :
    0 < emultiplicity a b ↔ 0 < multiplicity a b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
⊢ 0 < emultiplicity a b ↔ 0 < multiplicity a b

Tactic:
simp [pos_iff_ne_zero, pos_iff_ne_zero, emultiplicity_eq_zero_iff_multiplicity_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem Monovary.sum_smul_comp_perm_lt_sum_smul_iff (hfg : Monovary f g) :
    ∑ i, f i • g (σ i) < ∑ i, f i • g i ↔ ¬Monovary f (g ∘ σ)

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedSemiring α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i : ι, f i • g (σ i) < ∑ i : ι, f i • g i ↔ ¬Monovary f (g ∘ ⇑σ)

Tactic:
simp [(hfg.monovaryOn _).sum_smul_comp_perm_lt_sum_smul_iff fun _ _ ↦ mem_univ _]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem toList'_think (l : List α) (s : WSeq α) :
    Computation.corec (fun ⟨l, s⟩ =>
      match Seq.destruct s with
      | none => Sum.inl l.reverse
      | some (none, s') => Sum.inr (l, s')
      | some (some a, s') => Sum.inr (a::l, s')) (l, think s) =
      (Computation.corec (fun ⟨l, s⟩ =>
        match Seq.destruct s with
        | none => Sum.inl l.reverse
        | some (none, s') => Sum.inr (l, s')
        | some (some a, s') => Sum.inr (a::l, s')) (l, s)).think :=
  destruct_eq_think <| by simp [toList, think]

Proof state:
α : Type u
l : List α
s : WSeq α
⊢ (Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l, s.think)).destruct =
    Sum.inr
      (Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l, s))

Tactic:
simp [toList, think]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem insertNth_eq_iff {p : Fin (n + 1)} {a : α p} {f : ∀ i, α (p.succAbove i)} {g : ∀ j, α j} :
    insertNth p a f = g ↔ a = g p ∧ f = removeNth p g

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
g : (j : Fin (n + 1)) → α j
⊢ p.insertNth a f = g ↔ a = g p ∧ f = p.removeNth g

Tactic:
simp [funext_iff, forall_iff_succAbove p, removeNth]

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.comp (hg : ωScottContinuous g) (hf : ωScottContinuous f) :
    ωScottContinuous (g.comp f) :=
  ωScottContinuous.of_monotone_map_ωSup
    ⟨hg.monotone.comp hf.monotone, by simp [hf.map_ωSup, hg.map_ωSup, map_comp]⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β
g : β → γ
hg : ωScottContinuous g
hf : ωScottContinuous f
⊢ ∀ (c : Chain α), (g ∘ f) (ωSup c) = ωSup (c.map { toFun := g ∘ f, monotone' := ⋯ })

Tactic:
simp [hf.map_ωSup, hg.map_ωSup, map_comp]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
lemma kernImage_union_preimage {s : Set α} {t : Set β} :
    kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t

Tactic:
rw [kernImage_eq_compl, kernImage_eq_compl, compl_union, ← preimage_compl, image_inter_preimage,
    compl_inter, compl_compl]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
lemma pairingIn_neg_one_neg_four_iff [NoZeroDivisors R] :
    P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔ P.root j = (-2 : R) • P.root i

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
i j : ι
inst✝⁸ : Finite ι
inst✝⁷ : CharZero R
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : LinearOrderedCommRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : P.IsValuedIn S
inst✝¹ : NoZeroSMulDivisors R N
inst✝ : NoZeroDivisors R
⊢ P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔ P.root j = -2 • P.root i

Tactic:
rw [← P.pairing_neg_one_neg_four_iff, ← P.algebraMap_pairingIn S, ← P.algebraMap_pairingIn S,
  ← map_one (algebraMap S R), ← map_ofNat (algebraMap S R), ← map_neg, ← map_neg,
  (algebraMap_injective S R).eq_iff, (algebraMap_injective S R).eq_iff]

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Hom.lean
theorem comap_eq {f : N →* M} : comap f f.map_mul c = ker (c.mk'.comp f) :=
  ext fun x y => show c _ _ ↔ c.mk' _ = c.mk' _ by rw [← c.eq]; rfl

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
c : Con M
f : N →* M
x y : N
⊢ c (f x) (f y) ↔ c.mk' (f x) = c.mk' (f y)

Tactic:
rw [← c.eq]

Result:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
c : Con M
f : N →* M
x y : N
⊢ ↑(f x) = ↑(f y) ↔ c.mk' (f x) = c.mk' (f y)

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
c : Con M
f : N →* M
x y : N
⊢ ↑(f x) = ↑(f y) ↔ c.mk' (f x) = c.mk' (f y)

Tactic:
rfl

Result:
no goals