harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Analytic/OfScalars.lean
@[simp]
lemma coeff_ofScalars {𝕜 : Type*} [NontriviallyNormedField 𝕜] {p : ℕ → 𝕜} {n : ℕ} :
    (FormalMultilinearSeries.ofScalars 𝕜 p).coeff n = p n

Proof state:
𝕜 : Type u_3
inst✝ : NontriviallyNormedField 𝕜
p : ℕ → 𝕜
n : ℕ
⊢ (ofScalars 𝕜 p).coeff n = p n

Tactic:
simp [FormalMultilinearSeries.coeff, FormalMultilinearSeries.ofScalars, List.prod_ofFn]

Result:
no goals
-- Mathlib/Data/List/TFAE.lean
theorem tfae_singleton (p) : TFAE [p]

Proof state:
p : Prop
⊢ [p].TFAE

Tactic:
simp [TFAE, -eq_iff_iff]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem erase_union_distrib (s t : Finset α) (a : α) : (s ∪ t).erase a = s.erase a ∪ t.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ (s ∪ t).erase a = s.erase a ∪ t.erase a

Tactic:
simp_rw [erase_eq, union_sdiff_distrib]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma ofπ'_π : (ofπ' π hπ).π = π

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : π ∘ₗ relations.map = 0
⊢ (ofπ' π hπ).π = π

Tactic:
simp [ofπ']

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_const_smul_le : eLpNorm (c • f) p μ ≤ ‖c‖ₑ * eLpNorm f p μ :=
  eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
    (Eventually.of_forall fun _ => by simp [nnnorm_smul_le]) _

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 F
inst✝ : BoundedSMul 𝕜 F
c : 𝕜
f : α → F
x✝ : α
⊢ ‖(c • f) x✝‖₊ ≤ ‖c‖₊ * ‖f x✝‖₊

Tactic:
simp [nnnorm_smul_le]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
lemma span_range_update_sub_smul (hij : i ≠ j) (v : ι → M) (r : R) :
    span R (Set.range (Function.update v j (v j - r • v i))) = span R (Set.range v)

Proof state:
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ span R (range (update v j (v j - r • v i))) = span R (range v)

Tactic:
rw [sub_eq_add_neg, ← neg_smul, span_range_update_add_smul hij]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_div_le (a b : Ordinal) : b * (a / b) ≤ a :=
  if b0 : b = 0 then by simp only [b0, zero_mul, Ordinal.zero_le] else (le_div b0).1 le_rfl

Proof state:
a b : Ordinal.{u_4}
b0 : b = 0
⊢ b * (a / b) ≤ a

Tactic:
simp only [b0, zero_mul, Ordinal.zero_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem none_eq_getElem?_iff {l : List α} {i : Nat} : none = l[i]? ↔ length l ≤ i

Proof state:
α : Type u_1
l : List α
i : Nat
⊢ none = l[i]? ↔ l.length ≤ i

Tactic:
simp [eq_comm (a := none)]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrixAlgEquiv_reindexRange [DecidableEq M₁] (f : M₁ →ₗ[R] M₁) (k i : n) :
    LinearMap.toMatrixAlgEquiv v₁.reindexRange f
        ⟨v₁ k, Set.mem_range_self k⟩ ⟨v₁ i, Set.mem_range_self i⟩ =
      LinearMap.toMatrixAlgEquiv v₁ f k i

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
M₁ : Type u_5
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R M₁
v₁ : Basis n R M₁
inst✝ : DecidableEq M₁
f : M₁ →ₗ[R] M₁
k i : n
⊢ (toMatrixAlgEquiv v₁.reindexRange) f ⟨v₁ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (toMatrixAlgEquiv v₁) f k i

Tactic:
simp_rw [LinearMap.toMatrixAlgEquiv_apply, Basis.reindexRange_self, Basis.reindexRange_repr]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
@[simp] lemma zero_pow : ∀ {n : ℕ}, n ≠ 0 → (0 : M₀) ^ n = 0
  | n + 1, _ => by rw [pow_succ, mul_zero]

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 0 ^ (n + 1) = 0

Tactic:
rw [pow_succ, mul_zero]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
@[reassoc (attr := simp)]
lemma ιObj_πObj : ιObj I κ f ≫ πObj I κ f = f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
⊢ ιObj I κ f ≫ πObj I κ f = f

Tactic:
simp [ιObj, πObj]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_le_of_le_mul_right₀ [MulPosReflectLE α] (hb : 0 < b) (h : b ≤ a * b) : 1 ≤ a :=
  le_of_mul_le_mul_right (by simpa) hb

Proof state:
α : Type u_3
a b : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
hb : 0 < b
h : b ≤ a * b
⊢ 1 * b ≤ a * b

Tactic:
simpa

Result:
no goals
-- Mathlib/Topology/Algebra/Valued/NormedValued.lean
theorem norm_lt_one_iff : ‖x‖ < 1 ↔ val.v x < 1

Proof state:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
⊢ ‖x‖ < 1 ↔ v x < 1

Tactic:
simpa only [_root_.map_one] using (Valuation.RankOne.strictMono val.v).lt_iff_lt (b := 1)

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Operations.lean
theorem map_comap_eq_self {f : M →ₙ* N} {S : Subsemigroup N} (h : S ≤ f.srange) :
    (S.comap f).map f = S

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
S : Subsemigroup N
h : S ≤ f.srange
⊢ map f (comap f S) = S

Tactic:
simpa only [inf_of_le_left h] using map_comap_eq f S

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem not_isReal_iff_isComplex {w : InfinitePlace K} : ¬IsReal w ↔ IsComplex w

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ ¬w.IsReal ↔ w.IsComplex

Tactic:
rw [isComplex_iff, isReal_iff]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem filter_product (p : α → Prop) (q : β → Prop) [DecidablePred p] [DecidablePred q] :
    ((s ×ˢ t).filter fun x : α × β => p x.1 ∧ q x.2) = s.filter p ×ˢ t.filter q

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ filter (fun x => p x.1 ∧ q x.2) (s ×ˢ t) = filter p s ×ˢ filter q t

Tactic:
ext ⟨a, b⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a, b) ∈ filter (fun x => p x.1 ∧ q x.2) (s ×ˢ t) ↔ (a, b) ∈ filter p s ×ˢ filter q t

Proof state:
case h.mk
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
b : β
⊢ (a, b) ∈ filter (fun x => p x.1 ∧ q x.2) (s ×ˢ t) ↔ (a, b) ∈ filter p s ×ˢ filter q t

Tactic:
simp [mem_filter, mem_product, decide_eq_true_eq, and_comm, and_left_comm, and_assoc]

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Submodule.eq_top_of_isLocalized₀_span {N : Submodule R M}
    (h : ∀ r : s, N.localized₀ (.powers r.1) (f r) = ⊤) : N = ⊤ :=
  eq_of_isLocalized₀_span s span_eq Mₚ f fun _ ↦ by simp only [h, Submodule.localized₀_top]

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
N : Submodule R M
h : ∀ (r : ↑s), localized₀ (Submonoid.powers ↑r) (f r) N = ⊤
x✝ : ↑s
⊢ localized₀ (Submonoid.powers ↑x✝) (f x✝) N = localized₀ (Submonoid.powers ↑x✝) (f x✝) ⊤

Tactic:
simp only [h, Submodule.localized₀_top]

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem refl_prod_refl :
    (PartialEquiv.refl α).prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β)

Proof state:
α : Type u_1
β : Type u_2
⊢ (PartialEquiv.refl α).prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β)

Tactic:
ext ⟨x, y⟩ <;> simp

Result:
no goals
-- Mathlib/Algebra/Order/Field/Power.lean
theorem Even.zpow_abs {p : ℤ} (hp : Even p) (a : α) : |a| ^ p = a ^ p

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
p : ℤ
hp : Even p
a : α
⊢ |a| ^ p = a ^ p

Tactic:
rcases abs_choice a with h | h <;> simp only [h, hp.neg_zpow _]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma negMap_of_Z_eq_zero {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P z = 0) :
    W.negMap ⟦P⟧ = ⟦![1, 1, 0]⟧

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.negMap ⟦P⟧ = ⟦![1, 1, 0]⟧

Tactic:
rw [negMap_eq, neg_of_Z_eq_zero hP hPz,
  smul_eq _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg]

Result:
no goals
-- Mathlib/Data/Setoid/Basic.lean
theorem lift_unique {r : Setoid α} {f : α → β} (H : r ≤ ker f) (g : Quotient r → β)
    (Hg : f = g ∘ Quotient.mk'') : Quotient.lift f H = g

Proof state:
case h.mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x✝ : Quotient r
x : α
⊢ Quotient.lift f H (Quot.mk (⇑r) x) = g (Quot.mk (⇑r) x)

Tactic:
rw [← Quotient.mk, Quotient.lift_mk f H, Hg, Function.comp_apply, Quotient.mk''_eq_mk]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
⊢ Quotient.lift f H = g

Tactic:
ext ⟨x⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x✝ : Quotient r
x : α
⊢ Quotient.lift f H (Quot.mk (⇑r) x) = g (Quot.mk (⇑r) x)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem bind_map_comm {α β} {x : Option (Option α)} {f : α → β} :
    x.bind (Option.map f) = (x.map (Option.map f)).bind id

Proof state:
α : Type u_1
β : Type u_2
x : Option (Option α)
f : α → β
⊢ x.bind (Option.map f) = (Option.map (Option.map f) x).bind id

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Inductions.lean
theorem divX_C (a : R) : divX (C a) = 0 :=
  ext fun n => by simp [coeff_divX, coeff_C, Finsupp.single_eq_of_ne _]

Proof state:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (C a).divX.coeff n = coeff 0 n

Tactic:
simp [coeff_divX, coeff_C, Finsupp.single_eq_of_ne _]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_image [DecidableEq β] (f : α → β) (hs : s.Finite) (h : (f '' s).Finite) :
    h.toFinset = hs.toFinset.image f

Proof state:
case h
α : Type u
β : Type v
s : Set α
inst✝ : DecidableEq β
f : α → β
hs : s.Finite
h : (f '' s).Finite
a✝ : β
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ Finset.image f hs.toFinset

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
s : Set α
inst✝ : DecidableEq β
f : α → β
hs : s.Finite
h : (f '' s).Finite
⊢ h.toFinset = Finset.image f hs.toFinset

Tactic:
ext

Result:
case h
α : Type u
β : Type v
s : Set α
inst✝ : DecidableEq β
f : α → β
hs : s.Finite
h : (f '' s).Finite
a✝ : β
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ Finset.image f hs.toFinset
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem comap_lt_comap_of_surjective {f : G →* N} {K L : Subgroup N} (hf : Function.Surjective f) :
    K.comap f < L.comap f ↔ K < L

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
K L : Subgroup N
hf : Surjective ⇑f
⊢ comap f K < comap f L ↔ K < L

Tactic:
simp_rw [lt_iff_le_not_le, comap_le_comap_of_surjective hf]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem restrict_eq_self {i : Set α} (hi : MeasurableSet i) {j : Set α} (hj : MeasurableSet j)
    (hij : j ⊆ i) : v.restrict i j = v j

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
hij : j ⊆ i
⊢ ↑(v.restrict i) j = ↑v j

Tactic:
rw [restrict_apply v hi hj, Set.inter_eq_left.2 hij]

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem unbotD_eq_unbotD_iff {d : α} {x y : WithBot α} :
    unbotD d x = unbotD d y ↔ x = y ∨ x = d ∧ y = ⊥ ∨ x = ⊥ ∧ y = d

Proof state:
α : Type u_1
d : α
x y : WithBot α
⊢ unbotD d x = unbotD d y ↔ x = y ∨ x = ↑d ∧ y = ⊥ ∨ x = ⊥ ∧ y = ↑d

Tactic:
induction y <;> simp [unbotD_eq_iff, or_comm]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem attach_nonempty_iff {s : Finset α} : s.attach.Nonempty ↔ s.Nonempty

Proof state:
α : Type u_1
s : Finset α
⊢ s.attach.Nonempty ↔ s.Nonempty

Tactic:
simp [Finset.Nonempty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatMap_id (l : List (List α)) : l.flatMap id = l.flatten

Proof state:
α : Type u_1
l : List (List α)
⊢ flatMap id l = l.flatten

Tactic:
simp [flatMap_def]

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma not_odd_iff : ¬Odd n ↔ n % 2 = 0

Proof state:
n : ℤ
⊢ ¬Odd n ↔ n % 2 = 0

Tactic:
rw [odd_iff, emod_two_ne_one]

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

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ as.any p = true ↔ ∃ i x, p as[i] = true

Tactic:
simp [any_iff_exists]

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem eq_class_eq_leftCoset (s : Subgroup α) (g : α) :
    { x : α | (x : α ⧸ s) = g } = g • s :=
  Set.ext fun z => by
    rw [mem_leftCoset_iff, Set.mem_setOf_eq, eq_comm, QuotientGroup.eq, SetLike.mem_coe]

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
g z : α
⊢ z ∈ {x | ↑x = ↑g} ↔ z ∈ g • ↑s

Tactic:
rw [mem_leftCoset_iff, Set.mem_setOf_eq, eq_comm, QuotientGroup.eq, SetLike.mem_coe]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
theorem shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app (n : A) (X : C) :
    ((shiftFunctorCompIsoId C (-n) n (neg_add_cancel n)).hom.app X)⟦-n⟧' =
    (shiftFunctorCompIsoId C n (-n) (add_neg_cancel n)).hom.app (X⟦-n⟧)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n : A
X : C
⊢ (shiftFunctor C (-n)).map ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app X) =
    (shiftFunctorCompIsoId C n (-n) ⋯).hom.app ((shiftFunctor C (-n)).obj X)

Tactic:
apply shift_shiftFunctorCompIsoId_hom_app

Result:
no goals
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem map_update_self [DecidableEq ι] {i j : ι} (hij : i ≠ j) :
    f (Function.update v i (v j)) = 0 :=
  f.map_eq_zero_of_eq _ (by rw [Function.update_self, Function.update_of_ne hij.symm]) hij

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ update v i (v j) i = update v i (v j) j

Tactic:
rw [Function.update_self, Function.update_of_ne hij.symm]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
theorem IsSymmSndFDerivAt.isSymmSndFDerivWithinAt (h : IsSymmSndFDerivAt 𝕜 f x)
    (hf : ContDiffAt 𝕜 2 f x) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    IsSymmSndFDerivWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : IsSymmSndFDerivAt 𝕜 f x
hf : ContDiffAt 𝕜 2 f x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x

Tactic:
simp only [← isSymmSndFDerivWithinAt_univ, ← contDiffWithinAt_univ] at h hf

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : IsSymmSndFDerivWithinAt 𝕜 f univ x
hf : ContDiffWithinAt 𝕜 2 f univ x
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : IsSymmSndFDerivWithinAt 𝕜 f univ x
hf : ContDiffWithinAt 𝕜 2 f univ x
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x

Tactic:
exact h.mono_of_mem_nhdsWithin univ_mem hf hs uniqueDiffOn_univ hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mk_isEqv_mk (r : α → α → Bool) (a b : Array α) (ha : a.size = n) (hb : b.size = n) :
    Vector.isEqv (Vector.mk a ha) (Vector.mk b hb) r = Array.isEqv a b r

Proof state:
α : Type u_1
n : Nat
r : α → α → Bool
a b : Array α
ha : a.size = n
hb : b.size = n
⊢ { toArray := a, size_toArray := ha }.isEqv { toArray := b, size_toArray := hb } r = a.isEqv b r

Tactic:
simp [Vector.isEqv, Array.isEqv, ha, hb]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
theorem leftUnitor_inv_tensor_id (X Y : C) : (λ_ X).inv ⊗ 𝟙 Y = (λ_ _).inv ≫ (α_ _ _ _).inv

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ X).inv ⊗ 𝟙 Y = (λ_ (X ⊗ Y)).inv ≫ (α_ (𝟙_ C) X Y).inv

Tactic:
monoidal_coherence

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_add_zsmul (a b : α) (m : ℤ) : toIocMod hp a (b + m • p) = toIocMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b + m • p - (toIocDiv hp a b • p + m • p) = b - toIocDiv hp a b • p

Tactic:
abel

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp a (b + m • p) = toIocMod hp a b

Tactic:
rw [toIocMod, toIocDiv_add_zsmul, toIocMod, add_smul]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b + m • p - (toIocDiv hp a b • p + m • p) = b - toIocDiv hp a b • p
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem monic_of_d_eq_one (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d = 1) :
    P.toPoly.Monic

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d = 1
⊢ P.toPoly.Monic

Tactic:
rw [Monic, leadingCoeff_of_c_eq_zero ha hb hc, hd]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem kahler_rotation_left' (x y : V) (θ : Real.Angle) :
    o.kahler (o.rotation θ x) y = (-θ).toCircle * o.kahler x y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ (o.kahler ((o.rotation θ) x)) y = ↑(-θ).toCircle * (o.kahler x) y

Tactic:
simp only [Real.Angle.toCircle_neg, Circle.coe_inv_eq_conj, kahler_rotation_left]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem IsVonNBounded.vadd (hs : IsVonNBounded 𝕜 s) (x : E) :
    IsVonNBounded 𝕜 (x +ᵥ s)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : IsVonNBounded 𝕜 s
x : E
⊢ IsVonNBounded 𝕜 ({x} +ᵥ s)

Tactic:
exact IsVonNBounded.add (isVonNBounded_singleton x) hs

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : IsVonNBounded 𝕜 s
x : E
⊢ IsVonNBounded 𝕜 (x +ᵥ s)

Tactic:
rw [← singleton_vadd]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : IsVonNBounded 𝕜 s
x : E
⊢ IsVonNBounded 𝕜 ({x} +ᵥ s)
-- Mathlib/Data/Finset/NatAntidiagonal.lean
lemma antidiagonal_eq_map' (n : ℕ) :
    antidiagonal n =
      (range (n + 1)).map ⟨fun i ↦ (n - i, i), fun _ _ h ↦ (Prod.ext_iff.1 h).2⟩

Proof state:
n : ℕ
⊢ map ({ toFun := fun i => (i, n - i), inj' := ⋯ }.trans { toFun := Prod.swap, inj' := ⋯ }) (range (n + 1)) =
    map { toFun := fun i => (n - i, i), inj' := ⋯ } (range (n + 1))

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ antidiagonal n = map { toFun := fun i => (n - i, i), inj' := ⋯ } (range (n + 1))

Tactic:
rw [← map_swap_antidiagonal, antidiagonal_eq_map, map_map]

Result:
n : ℕ
⊢ map ({ toFun := fun i => (i, n - i), inj' := ⋯ }.trans { toFun := Prod.swap, inj' := ⋯ }) (range (n + 1)) =
    map { toFun := fun i => (n - i, i), inj' := ⋯ } (range (n + 1))
-- Mathlib/Order/WithBot.lean
theorem le_coe_iff : x ≤ b ↔ ∀ a : α, x = ↑a → a ≤ b

Proof state:
α : Type u_1
b : α
inst✝ : LE α
x : WithBot α
⊢ x ≤ ↑b ↔ ∀ (a : α), x = ↑a → a ≤ b

Tactic:
simp [le_def]

Result:
no goals
-- Mathlib/Data/Fintype/Pi.lean
theorem Finset.univ_pi_univ {α : Type*} {β : α → Type*} [DecidableEq α] [Fintype α]
    [∀ a, Fintype (β a)] :
    (Finset.univ.pi fun a : α => (Finset.univ : Finset (β a))) = Finset.univ

Proof state:
α : Type u_3
β : α → Type u_4
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
⊢ (univ.pi fun a => univ) = univ

Tactic:
ext

Result:
case h
α : Type u_3
β : α → Type u_4
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
a✝ : (a : α) → a ∈ univ → β a
⊢ (a✝ ∈ univ.pi fun a => univ) ↔ a✝ ∈ univ

Proof state:
case h
α : Type u_3
β : α → Type u_4
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
a✝ : (a : α) → a ∈ univ → β a
⊢ (a✝ ∈ univ.pi fun a => univ) ↔ a✝ ∈ univ

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
@[reassoc]
lemma associator_naturality₃ {X₁ X₂ X₃ Y₃ : LocalizedMonoidal L W ε} (f₃ : X₃ ⟶ Y₃) :
    ((X₁ ⊗ X₂) ◁ f₃) ≫ (α_ X₁ X₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (X₁ ◁ (X₂ ◁ f₃))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₃ : LocalizedMonoidal L W ε
f₃ : X₃ ⟶ Y₃
⊢ (X₁ ⊗ X₂) ◁ f₃ ≫ (α_ X₁ X₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ X₁ ◁ X₂ ◁ f₃

Tactic:
simp only [← id_tensorHom, ← tensor_id, associator_naturality]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_self_add_right {m n : ℕ} : Coprime m (m + n) ↔ Coprime m n

Proof state:
m n : ℕ
⊢ m.Coprime (m + n) ↔ m.Coprime n

Tactic:
rw [add_comm, coprime_add_self_right]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
@[simp]
lemma coeff_C_succ {r : R} {n : ℕ} : coeff (C r) (n + 1) = 0

Proof state:
R : Type u
inst✝ : Semiring R
r : R
n : ℕ
⊢ (C r).coeff (n + 1) = 0

Tactic:
simp [coeff_C]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[reassoc]
lemma mapLeftHomologyIso_inv_naturality [S₁.HasLeftHomology] [S₂.HasLeftHomology]
    [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
    F.map (leftHomologyMap φ) ≫ (S₂.mapLeftHomologyIso F).inv =
      (S₁.mapLeftHomologyIso F).inv ≫ leftHomologyMap (F.mapShortComplex.map φ)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Category.{u_4, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ F.map (leftHomologyMap φ) ≫ (S₂.mapLeftHomologyIso F).inv =
    (S₁.mapLeftHomologyIso F).inv ≫ leftHomologyMap (F.mapShortComplex.map φ)

Tactic:
rw [← cancel_epi (S₁.mapLeftHomologyIso F).hom, ← mapLeftHomologyIso_hom_naturality_assoc,
  Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem preimage_coe_Ioo : (some : α → WithTop α) ⁻¹' Ioo a b = Ioo a b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Ioo ↑a ↑b = Ioo a b

Tactic:
simp [← Ioi_inter_Iio]

Result:
no goals