harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_eq_ofFn {as : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
    as.mapFinIdx f = Vector.ofFn fun i : Fin n => f i as[i] i.2

Proof state:
α : Type u_1
n : Nat
β : Type u_2
as : Vector α n
f : (i : Nat) → α → i < n → β
⊢ as.mapFinIdx f = ofFn fun i => f (↑i) as[i] ⋯

Tactic:
rcases as with ⟨as, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
as : Array α
f : (i : Nat) → α → i < as.size → β
⊢ { toArray := as, size_toArray := ⋯ }.mapFinIdx f = ofFn fun i => f ↑i { toArray := as, size_toArray := ⋯ }[i] ⋯

Proof state:
case mk
α : Type u_1
β : Type u_2
as : Array α
f : (i : Nat) → α → i < as.size → β
⊢ { toArray := as, size_toArray := ⋯ }.mapFinIdx f = ofFn fun i => f ↑i { toArray := as, size_toArray := ⋯ }[i] ⋯

Tactic:
simp [Array.mapFinIdx_eq_ofFn]

Result:
no goals
-- Mathlib/Probability/Kernel/Integral.lean
theorem setIntegral_deterministic [MeasurableSingletonClass β] (hg : Measurable g)
    (s : Set β) [Decidable (g a ∈ s)] :
    ∫ x in s, f x ∂deterministic g hg a = if g a ∈ s then f (g a) else 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : β → E
a : α
inst✝² : CompleteSpace E
g : α → β
inst✝¹ : MeasurableSingletonClass β
hg : Measurable g
s : Set β
inst✝ : Decidable (g a ∈ s)
⊢ ∫ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0

Tactic:
rw [deterministic_apply, setIntegral_dirac f _ s]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem continuous_induced_rng {g : γ → α} {t₂ : TopologicalSpace β} {t₁ : TopologicalSpace γ} :
    Continuous[t₁, induced f t₂] g ↔ Continuous[t₁, t₂] (f ∘ g)

Proof state:
α : Type u
β : Type v
γ : Type u_1
f : α → β
g : γ → α
t₂ : TopologicalSpace β
t₁ : TopologicalSpace γ
⊢ Continuous g ↔ Continuous (f ∘ g)

Tactic:
simp only [continuous_iff_le_induced, induced_compose]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem comap_exp_nhds_zero : comap exp (𝓝 0) = comap re atBot :=
  calc
    comap exp (𝓝 0) = comap re (comap Real.exp (𝓝 0))

Proof state:
⊢ comap cexp (𝓝 0) = comap re (comap Real.exp (𝓝 0))

Tactic:
rw [← comap_norm_nhds_zero, comap_comap, Function.comp_def]

Result:
⊢ comap (fun x => ‖cexp x‖) (𝓝 0) = comap re (comap Real.exp (𝓝 0))

Proof state:
⊢ comap (fun x => ‖cexp x‖) (𝓝 0) = comap re (comap Real.exp (𝓝 0))

Tactic:
simp_rw [norm_exp, comap_comap, Function.comp_def]

Result:
no goals

Proof state:
⊢ comap re (comap Real.exp (𝓝 0)) = comap re atBot

Tactic:
rw [Real.comap_exp_nhds_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem smul_integral_comp_mul_right (c) :
    (c • ∫ x in a..b, f (x * c)) = ∫ x in a * c..b * c, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c : ℝ
⊢ c • ∫ (x : ℝ) in a..b, f (x * c) = ∫ (x : ℝ) in a * c..b * c, f x

Tactic:
by_cases hc : c = 0 <;> simp [hc, integral_comp_mul_right]

Result:
no goals
-- Mathlib/Algebra/Homology/HasNoLoop.lean
lemma not_rel_of_eq {j' : ι } (h : j = j') : ¬ c.Rel j j'

Proof state:
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
⊢ ¬c.Rel j j

Tactic:
exact c.not_rel_self j

Result:
no goals

Proof state:
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j j' : ι
h : j = j'
⊢ ¬c.Rel j j'

Tactic:
subst h

Result:
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
⊢ ¬c.Rel j j
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
/-- `curry'` and `uncurry`' are inverse bijections. -/
@[simp]
lemma uncurry'_curry' {X Y : C} [Closed X] (f : X ⟶ Y) :
    uncurry' (curry' f) = f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : Closed X
f : X ⟶ Y
⊢ uncurry' (curry' f) = f

Tactic:
simp [curry', uncurry']

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma top_induce_pair_connected_of_adj {u v : V} (huv : G.Adj u v) :
    ((⊤ : G.Subgraph).induce {u, v}).Connected

Proof state:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (⊤.induce {u, v}).Connected

Tactic:
rw [← subgraphOfAdj_eq_induce huv]

Result:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (G.subgraphOfAdj huv).Connected

Proof state:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (G.subgraphOfAdj huv).Connected

Tactic:
exact subgraphOfAdj_connected huv

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
@[simp] lemma expect_const_zero (s : Finset ι) : 𝔼 _i ∈ s, (0 : M) = 0

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
⊢ 𝔼 _i ∈ s, 0 = 0

Tactic:
simp [expect]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
theorem sum_eq_card_of_eq_one {ψ : AddChar R R'} (hψ : ψ = 1) :
    ∑ a, ψ a = Fintype.card R

Proof state:
R : Type u_1
inst✝² : AddGroup R
inst✝¹ : Fintype R
R' : Type u_2
inst✝ : CommRing R'
ψ : AddChar R R'
hψ : ψ = 1
⊢ ∑ a : R, ψ a = ↑(Fintype.card R)

Tactic:
simp [hψ]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma snd_dirac_unit_compProd_const (μ : Measure β) [IsFiniteMeasure μ] :
    snd (Measure.dirac () ⊗ₘ Kernel.const Unit μ) = μ

Proof state:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
inst✝ : IsFiniteMeasure μ
⊢ (dirac () ⊗ₘ Kernel.const Unit μ).snd = μ

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft {X Y : C} [HasLeftDual X]
    [HasLeftDual Y] (f : X ⟶ Y) :
    (tensorRightHomEquiv _ (ᘁY) _ _).symm (η_ (ᘁX : C) X ≫ (ᘁX : C) ◁ f) = (λ_ _).hom ≫ ᘁf

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (tensorRightHomEquiv (𝟙_ C) (ᘁY) Y ᘁX).symm (η_ (ᘁX) X ≫ ᘁX ◁ f) = (λ_ ᘁY).hom ≫ ᘁf

Tactic:
dsimp [tensorRightHomEquiv, leftAdjointMate]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (η_ (ᘁX) X ≫ ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom =
    (λ_ ᘁY).hom ≫ (λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (η_ (ᘁX) X ≫ ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom =
    (λ_ ᘁY).hom ≫ (λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem pairwise_disjoint_Ioo_zpow :
    Pairwise (Disjoint on fun n : ℤ => Ioo (b ^ n) (b ^ (n + 1)))

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
b : α
⊢ Pairwise (Disjoint on fun n => Ioo (b ^ n) (b ^ (n + 1)))

Tactic:
simpa only [one_mul] using pairwise_disjoint_Ioo_mul_zpow 1 b

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem cancel_unit_right {X Y : C} (f f' : X ⟶ Y) :
    f ≫ e.unit.app Y = f' ≫ e.unit.app Y ↔ f = f'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X Y : C
f f' : X ⟶ Y
⊢ f ≫ e.unit.app Y = f' ≫ e.unit.app Y ↔ f = f'

Tactic:
simp only [cancel_mono]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Infinite.nonempty {s : Set α} (h : s.Infinite) : s.Nonempty :=
  nonempty_iff_ne_empty.2 <| by
    rintro rfl
    exact h finite_empty

Proof state:
α : Type u
s : Set α
h : s.Infinite
⊢ s ≠ ∅

Tactic:
rintro rfl

Result:
α : Type u
h : ∅.Infinite
⊢ False

Proof state:
α : Type u
h : ∅.Infinite
⊢ False

Tactic:
exact h finite_empty

Result:
no goals
-- Mathlib/Order/Monotone/MonovaryOrder.lean
lemma antivary_iff_exists_antitone_monotone :
    Antivary f g ↔ ∃ (_ : LinearOrder ι), Antitone f ∧ Monotone g

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
⊢ Antivary f g ↔ ∃ x, Antitone f ∧ Monotone g

Tactic:
simp [← antivaryOn_univ, antivaryOn_iff_exists_antitoneOn_monotoneOn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_modifyKey_self [BEq α] [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k (modifyKey k f l)) :
    getKey k (modifyKey k f l) h = k

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
h : containsKey k (modifyKey k f l) = true
⊢ getKey k (modifyKey k f l) h = k

Tactic:
simp [getKey_modifyKey, hl]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem orderTop_single_le : a ≤ (single a r).orderTop

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ ↑a ≤ ((single a) r).orderTop

Tactic:
by_cases hr : r = 0

Result:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
hr : r = 0
⊢ ↑a ≤ ((single a) r).orderTop

case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
hr : ¬r = 0
⊢ ↑a ≤ ((single a) r).orderTop

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
hr : ¬r = 0
⊢ ↑a ≤ ((single a) r).orderTop

Tactic:
rw [orderTop_single hr]

Result:
no goals

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
hr : r = 0
⊢ ↑a ≤ ((single a) r).orderTop

Tactic:
simp only [hr, map_zero, orderTop_zero, le_top]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc (attr := simp)]
lemma p_comp_opcyclesIso_inv : h.p ≫ h.opcyclesIso.inv = S.pOpcycles

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
inst✝ : S.HasRightHomology
⊢ h.p ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData = S.rightHomologyData.p

Tactic:
simp only [p_opcyclesMap', id_τ₂, id_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
inst✝ : S.HasRightHomology
⊢ h.p ≫ h.opcyclesIso.inv = S.pOpcycles

Tactic:
dsimp [pOpcycles, RightHomologyData.opcyclesIso]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
inst✝ : S.HasRightHomology
⊢ h.p ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData = S.rightHomologyData.p
-- Mathlib/Algebra/Category/Ring/Constructions.lean
theorem subsingleton_of_isTerminal {X : CommRingCat} (hX : IsTerminal X) : Subsingleton X :=
  (hX.uniqueUpToIso punitIsTerminal).commRingCatIsoToRingEquiv.toEquiv.subsingleton_congr.mpr
    (show Subsingleton PUnit by infer_instance)

Proof state:
X : CommRingCat
hX : IsTerminal X
⊢ Subsingleton PUnit.{u_1 + 1}

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_image_right : ⋃ b ∈ t, (f · b) '' s = image2 f s t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ ⋃ b ∈ t, (fun x => f x b) '' s = image2 f s t

Tactic:
rw [image2_swap, iUnion_image_left]

Result:
no goals
-- Mathlib/ModelTheory/Algebra/Ring/Basic.lean
theorem realize_mul (x y : ring.Term α) (v : α → R) :
    Term.realize v (x * y) = Term.realize v x * Term.realize v y

Proof state:
α : Type u_1
R : Type u_2
inst✝⁵ : Add R
inst✝⁴ : Mul R
inst✝³ : Neg R
inst✝² : One R
inst✝¹ : Zero R
inst✝ : CompatibleRing R
x y : ring.Term α
v : α → R
⊢ Term.realize v (x * y) = Term.realize v x * Term.realize v y

Tactic:
simp [mul_def, funMap_mul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem edgeSet_sup : (G₁ ⊔ G₂).edgeSet = G₁.edgeSet ∪ G₂.edgeSet

Proof state:
V : Type u
G₁ G₂ : SimpleGraph V
⊢ (G₁ ⊔ G₂).edgeSet = G₁.edgeSet ∪ G₂.edgeSet

Tactic:
ext ⟨x, y⟩

Result:
case h.mk.mk
V : Type u
G₁ G₂ : SimpleGraph V
x✝ : Sym2 V
x y : V
⊢ Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ ⊔ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet ∪ G₂.edgeSet

Proof state:
case h.mk.mk
V : Type u
G₁ G₂ : SimpleGraph V
x✝ : Sym2 V
x y : V
⊢ Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ ⊔ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet ∪ G₂.edgeSet

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_comp_map (f : α → β) (g : β → γ) :
    Option.map g ∘ Option.map f = Option.map (g ∘ f)

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
x : Option α
⊢ (Option.map g ∘ Option.map f) x = Option.map (g ∘ f) x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ Option.map g ∘ Option.map f = Option.map (g ∘ f)

Tactic:
funext x

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
x : Option α
⊢ (Option.map g ∘ Option.map f) x = Option.map (g ∘ f) x
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_pointReflection_right (p q : P) :
    dist (Equiv.pointReflection p q) q = ‖(2 : 𝕜)‖ * dist p q

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p q : P
⊢ dist ((Equiv.pointReflection p) q) q = ‖2‖ * dist p q

Tactic:
simp [dist_eq_norm_vsub V, Equiv.pointReflection_vsub_right (G := V), ← Nat.cast_smul_eq_nsmul 𝕜,
  norm_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem Basis.toMatrix_mul_toMatrix_flip [DecidableEq ι] [Fintype ι'] :
    b.toMatrix b' * b'.toMatrix b = 1

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
⊢ b.toMatrix ⇑b' * b'.toMatrix ⇑b = 1

Tactic:
rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]

Result:
no goals
-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem trinomial_mirror (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) (hw : w ≠ 0) :
    (trinomial k m n u v w).mirror = trinomial k (n - m + k) n w v u

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ (trinomial k m n u v w).mirror = trinomial k (n - m + k) n w v u

Tactic:
rw [mirror, trinomial_natTrailingDegree hkm hmn hu, reverse, trinomial_natDegree hkm hmn hw,
  trinomial_def, reflect_add, reflect_add, reflect_C_mul_X_pow, reflect_C_mul_X_pow,
  reflect_C_mul_X_pow, revAt_le (hkm.trans hmn).le, revAt_le hmn.le, revAt_le le_rfl, add_mul,
  add_mul, mul_assoc, mul_assoc, mul_assoc, ← pow_add, ← pow_add, ← pow_add,
  Nat.sub_add_cancel (hkm.trans hmn).le, Nat.sub_self, zero_add, add_comm, add_comm (C u * X ^ n),
  ← add_assoc, ← trinomial_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem isSome_attachWith {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
    (o.attachWith p H).isSome = o.isSome

Proof state:
α : Type u_1
p : α → Prop
o : Option α
H : ∀ (a : α), a ∈ o → p a
⊢ (o.attachWith p H).isSome = o.isSome

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem Asymptotics.IsBigO.hasFDerivAt {x₀ : E} {n : ℕ} (h : f =O[𝓝 x₀] fun x => ‖x - x₀‖ ^ n)
    (hn : 1 < n) : HasFDerivAt f (0 : E →L[𝕜] 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
x₀ : E
n : ℕ
h : f =O[𝓝 x₀] fun x => ‖x - x₀‖ ^ n
hn : 1 < n
⊢ HasFDerivAt f 0 x₀

Tactic:
rw [← nhdsWithin_univ] at h

Result:
𝕜 : 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
x₀ : E
n : ℕ
h : f =O[𝓝[univ] x₀] fun x => ‖x - x₀‖ ^ n
hn : 1 < n
⊢ HasFDerivAt f 0 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
x₀ : E
n : ℕ
h : f =O[𝓝[univ] x₀] fun x => ‖x - x₀‖ ^ n
hn : 1 < n
⊢ HasFDerivAt f 0 x₀

Tactic:
exact (h.hasFDerivWithinAt (mem_univ _) hn).hasFDerivAt_of_univ

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
theorem norm_inr (m : M) : ‖(inr m : tsze R M)‖ = ‖m‖

Proof state:
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
m : M
⊢ ‖inr m‖ = ‖m‖

Tactic:
simp [norm_def]

Result:
no goals
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem open_target (he : e ∈ c.atlas) : IsOpen e.target

Proof state:
H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ IsOpen e.target

Tactic:
have E : e.target ∩ e.symm ⁻¹' e.source = e.target :=
  Subset.antisymm inter_subset_left fun x hx ↦
    ⟨hx, PartialEquiv.target_subset_preimage_source _ hx⟩

Result:
H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
E : e.target ∩ ↑e.symm ⁻¹' e.source = e.target
⊢ IsOpen e.target

Proof state:
H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
E : e.target ∩ ↑e.symm ⁻¹' e.source = e.target
⊢ IsOpen e.target

Tactic:
simpa [PartialEquiv.trans_source, E] using c.open_source e e he he

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_succ (x i : Nat) : testBit x (succ i) = testBit (x/2) i

Proof state:
x i : Nat
⊢ x.testBit i.succ = (x / 2).testBit i

Tactic:
unfold testBit

Result:
x i : Nat
⊢ (1 &&& x >>> i.succ != 0) = (1 &&& (x / 2) >>> i != 0)

Proof state:
x i : Nat
⊢ (1 &&& x >>> i.succ != 0) = (1 &&& (x / 2) >>> i != 0)

Tactic:
simp [shiftRight_succ_inside]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_add [Semiring α] (m n) : ((m + n : Num) : α) = m + n

Proof state:
α : Type u_1
inst✝ : Semiring α
m n : Num
⊢ ↑(m + n) = ↑m + ↑n

Tactic:
rw [← cast_to_nat, add_to_nat, Nat.cast_add, cast_to_nat, cast_to_nat]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma equation_iff (P : Fin 3 → R) : W'.Equation P ↔
    P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3
      - (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ W'.Equation P ↔
    P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
        (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) =
      0

Tactic:
rw [Equation, eval_polynomial]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma preimage_mul (hm : Injective m) {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) :
    m ⁻¹' (s * t) = m ⁻¹' s * m ⁻¹' t :=
  hm.image_injective <| by
    rw [image_mul, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (mul_subset_range m hs ht)]

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' (⇑m ⁻¹' (s * t)) = ⇑m '' (⇑m ⁻¹' s * ⇑m ⁻¹' t)

Tactic:
rw [image_mul, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
  image_preimage_eq_iff.2 (mul_subset_range m hs ht)]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem rank_push {m : UnionFind} : m.push.rank a = m.rank a

Proof state:
a : Nat
m : UnionFind
⊢ m.push.rank a = m.rank a

Tactic:
simp [rank]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem hnot_hnot_sup_distrib (a b : α) : ￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b

Tactic:
refine ((hnot_inf_distrib _ _).ge.trans <| hnot_anti le_hnot_inf_hnot).antisymm' ?_

Result:
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢￢(a ⊔ b) ≤ ￢￢a ⊔ ￢￢b

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint (a ⊔ b) (￢(a ⊔ b))

Tactic:
exact codisjoint_hnot_right

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢￢(a ⊔ b) ≤ ￢￢a ⊔ ￢￢b

Tactic:
rw [hnot_le_iff_codisjoint_left, codisjoint_assoc, codisjoint_hnot_hnot_left_iff,
  codisjoint_left_comm, codisjoint_hnot_hnot_left_iff, ← codisjoint_assoc, sup_comm]

Result:
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint (a ⊔ b) (￢(a ⊔ b))
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma ι_comp_colimitUnopIsoOpLimit_hom (F : Jᵒᵖ ⥤ Cᵒᵖ) [HasLimit F] (j : J) :
    colimit.ι F.unop j ≫ (colimitUnopIsoOpLimit F).hom = (limit.π F (op 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
⊢ colimit.ι F.unop j ≫ (colimitUnopIsoOpLimit F).hom = (limit.π F (op j)).unop

Tactic:
simp [colimitUnopIsoOpLimit]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k
  | 0 => rfl
  | k + 1 => by simp [← Nat.add_assoc, shiftLeft_add _ _ k, shiftLeft_succ]

Proof state:
m n k : Nat
⊢ m <<< (n + (k + 1)) = m <<< n <<< (k + 1)

Tactic:
simp [← Nat.add_assoc, shiftLeft_add _ _ k, shiftLeft_succ]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem aleph0_le_aleph (o : Ordinal) : ℵ₀ ≤ ℵ_ o

Proof state:
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ ℵ_ o

Tactic:
rw [aleph_eq_preAleph, aleph0_le_preAleph]

Result:
o : Ordinal.{u_1}
⊢ ω ≤ ω + o

Proof state:
o : Ordinal.{u_1}
⊢ ω ≤ ω + o

Tactic:
apply Ordinal.le_add_right

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_neg_two : S R (-2) = -1

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

Tactic:
simpa [zero_sub, Int.reduceNeg, S_neg_one, mul_zero, S_zero] using S_sub_two R 0

Result:
no goals
-- Mathlib/GroupTheory/CosetCover.lean
theorem Submodule.exists_finiteIndex_of_cover (hcovers : ⋃ i ∈ s, (p i : Set M) = Set.univ) :
    ∃ k ∈ s, (p k).toAddSubgroup.FiniteIndex :=
  have hcovers' : ⋃ i ∈ s, (0 : M) +ᵥ ((p i).toAddSubgroup : Set M) = Set.univ

Proof state:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : ι → Submodule R M
s : Finset ι
hcovers : ⋃ i ∈ s, ↑(p i) = Set.univ
⊢ ⋃ i ∈ s, 0 +ᵥ ↑(p i).toAddSubgroup = Set.univ

Tactic:
simpa only [zero_vadd] using hcovers

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Root.lean
lemma floorRoot_ne_zero : floorRoot n a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0

Proof state:
a n : ℕ
⊢ n.floorRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0

Tactic:
simp +contextual [floorRoot, not_imp_not, not_or]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue!_insertListConst_of_mem [BEq α] [EquivBEq α] [Inhabited β]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v: β} (k_beq : k == k')
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ toInsert):
    getValue! k' (insertListConst l toInsert) = v

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
v : β
k_beq : (k == k') = true
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
⊢ getValue! k' (insertListConst l toInsert) = v

Tactic:
rw [getValue!_eq_getValue?,
  getValue?_insertListConst_of_mem k_beq distinct_l distinct_toInsert mem, Option.get!_some]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem re_ofReal_mul (r : ℝ) (z : K) : re (↑r * z) = r * re z

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

Tactic:
simp only [mul_re, ofReal_im, zero_mul, ofReal_re, sub_zero]

Result:
no goals