harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
theorem identity_N₂ :
    (𝟙 (N₂ : Karoubi (SimplicialObject C) ⥤ _) ◫ N₂Γ₂.inv) ≫
    (Functor.associator _ _ _).inv ≫ Γ₂N₂.natTrans ◫ 𝟙 (@N₂ C _ _) = 𝟙 N₂

Proof state:
case w.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ (N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂.map (𝟙 (N₂.obj P)))) ≫
      𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ 𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ N₂.map (Γ₂N₂.natTrans.app P) =
    𝟙 (N₂.obj P)

Tactic:
rw [Γ₂.map_id, N₂.map_id, comp_id, id_comp, id_comp, identity_N₂_objectwise P]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ (𝟙 N₂ ◫ N₂Γ₂.inv) ≫ (N₂.associator Γ₂ N₂).inv ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂ = 𝟙 N₂

Tactic:
ext P : 2

Result:
case w.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ ((𝟙 N₂ ◫ N₂Γ₂.inv) ≫ (N₂.associator Γ₂ N₂).inv ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂).app P = (𝟙 N₂).app P

Proof state:
case w.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ ((𝟙 N₂ ◫ N₂Γ₂.inv) ≫ (N₂.associator Γ₂ N₂).inv ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂).app P = (𝟙 N₂).app P

Tactic:
dsimp only [NatTrans.comp_app, NatTrans.hcomp_app, Functor.comp_map, Functor.associator,
  NatTrans.id_app, Functor.comp_obj]

Result:
case w.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ (N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂.map (𝟙 (N₂.obj P)))) ≫
      𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ 𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ N₂.map (Γ₂N₂.natTrans.app P) =
    𝟙 (N₂.obj P)
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_univ_def [CommMonoid β] {n : ℕ} (f : Fin n → β) :
    ∏ i, f i = ((List.finRange n).map f).prod

Proof state:
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
f : Fin n → β
⊢ ∏ i : Fin n, f i = (List.map f (List.finRange n)).prod

Tactic:
rw [← List.ofFn_eq_map, prod_ofFn]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
@[to_additive]
lemma isComplement_subgroup_right_iff_existsUnique_quotientGroupMk :
    IsComplement S H ↔ ∀ q : G ⧸ H, ∃! s : S, QuotientGroup.mk s.1 = q

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
⊢ IsComplement S ↑H ↔ ∀ (q : G ⧸ H), ∃! s, ↑↑s = q

Tactic:
simp_rw [isComplement_iff_existsUnique_inv_mul_mem, SetLike.mem_coe, ← QuotientGroup.eq,
  QuotientGroup.forall_mk]

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem colLen_transpose (μ : YoungDiagram) (j : ℕ) : μ.transpose.colLen j = μ.rowLen j

Proof state:
μ : YoungDiagram
j : ℕ
⊢ μ.transpose.colLen j = μ.rowLen j

Tactic:
simp [rowLen, colLen]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem smul_mul [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] (a : R)
    (M : Matrix m n α) (N : Matrix n l α) : (a • M) * N = a • (M * N)

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
M : Matrix m n α
N : Matrix n l α
⊢ a • M * N = a • (M * N)

Tactic:
ext

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
M : Matrix m n α
N : Matrix n l α
i✝ : m
j✝ : l
⊢ (a • M * N) i✝ j✝ = (a • (M * N)) i✝ j✝

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
M : Matrix m n α
N : Matrix n l α
i✝ : m
j✝ : l
⊢ (a • M * N) i✝ j✝ = (a • (M * N)) i✝ j✝

Tactic:
apply smul_dotProduct a

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_filter_le_left {a b : α} [DecidablePred (· ≤ a)] (hab : a < b) :
    ((Ico a b).filter fun x => x ≤ a) = {a}

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
⊢ {a}.val = {a}

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
⊢ filter (fun x => x ≤ a) (Ico a b) = {a}

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_left hab]

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
⊢ {a}.val = {a}
-- Mathlib/Order/Filter/Basic.lean
theorem inter_eventuallyEq_right {s t : Set α} {l : Filter α} :
    (s ∩ t : Set α) =ᶠ[l] t ↔ ∀ᶠ x in l, x ∈ t → x ∈ s

Proof state:
α : Type u
s t : Set α
l : Filter α
⊢ s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s

Tactic:
rw [inter_comm, inter_eventuallyEq_left]

Result:
no goals
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.skeletonLT_zero_eq_base [RelCWComplex C D] : skeletonLT C 0 = D

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
⊢ skeletonLT C 0 = D

Tactic:
simp only [skeletonLT, ENat.not_lt_zero, iUnion_of_empty, iUnion_empty, union_empty]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem lcm_eq_zero_iff [Nontrivial α] : s.lcm f = 0 ↔ 0 ∈ f '' s

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : Nontrivial α
⊢ s.lcm f = 0 ↔ 0 ∈ f '' ↑s

Tactic:
simp only [Multiset.mem_map, lcm_def, Multiset.lcm_eq_zero_iff, Set.mem_image, mem_coe, ←
  Finset.mem_def]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem mem_darts_reverse {u v : V} {d : G.Dart} {p : G.Walk u v} :
    d ∈ p.reverse.darts ↔ d.symm ∈ p.darts

Proof state:
V : Type u
G : SimpleGraph V
u v : V
d : G.Dart
p : G.Walk u v
⊢ d ∈ p.reverse.darts ↔ d.symm ∈ p.darts

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma lt_mul_right [PosMulStrictMono M₀] (ha : 0 < a) (hb : 1 < b) : a < a * b

Proof state:
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a b : M₀
inst✝ : PosMulStrictMono M₀
ha : 0 < a
hb : 1 < b
⊢ a < a * b

Tactic:
simpa using mul_lt_mul_of_pos_left hb ha

Result:
no goals
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem IsMaximal.of_liesOver_isMaximal [hpm : p.IsMaximal] [P.IsPrime] : P.IsMaximal

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
B : Type u_2
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
hpm : (Ideal.under A P).IsMaximal
inst✝ : P.IsPrime
⊢ P.IsMaximal

Tactic:
exact isMaximal_of_isIntegral_of_isMaximal_comap P hpm

Result:
no goals

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
B : Type u_2
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
hpm : p.IsMaximal
inst✝ : P.IsPrime
⊢ P.IsMaximal

Tactic:
rw [P.over_def p] at hpm

Result:
A : Type u_1
inst✝⁵ : CommRing A
B : Type u_2
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
hpm : (Ideal.under A P).IsMaximal
inst✝ : P.IsPrime
⊢ P.IsMaximal
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insertManyIfNewUnit_empty_list [EquivBEq α] [LawfulHashable α]
    {l : List α}
    (distinct : l.Pairwise (fun a b => (a == b) = false)) :
    (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1.1.size = l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
distinct : List.Pairwise (fun a b => (a == b) = false) l
⊢ (insertManyIfNewUnit empty l).val.val.size = l.length

Tactic:
simp [size_insertManyIfNewUnit_list _ Raw.WF.empty₀ distinct]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
/-- A definition of krullDim for nonempty `α` that avoids `WithBot` -/
lemma krullDim_eq_iSup_length [Nonempty α] :
    krullDim α = ⨆ (p : LTSeries α), (p.length : ℕ∞)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α = ↑(⨆ p, ↑p.length)

Tactic:
unfold krullDim

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ p, ↑p.length = ↑(⨆ p, ↑p.length)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ p, ↑p.length = ⨆ i, ↑↑i.length

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ p, ↑p.length = ↑(⨆ p, ↑p.length)

Tactic:
rw [WithBot.coe_iSup (OrderTop.bddAbove _)]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ p, ↑p.length = ⨆ i, ↑↑i.length
-- Mathlib/GroupTheory/GroupAction/Basic.lean
@[to_additive]
lemma snd_mem_orbit_of_mem_orbit {x y : α × β} (h : x ∈ MulAction.orbit M y) :
    x.2 ∈ MulAction.orbit M y.2

Proof state:
M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
β : Type u_1
inst✝ : MulAction M β
x y : α × β
h : x ∈ orbit M y
⊢ x.2 ∈ orbit M y.2

Tactic:
rcases h with ⟨g, rfl⟩

Result:
case intro
M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
β : Type u_1
inst✝ : MulAction M β
y : α × β
g : M
⊢ ((fun m => m • y) g).2 ∈ orbit M y.2

Proof state:
case intro
M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
β : Type u_1
inst✝ : MulAction M β
y : α × β
g : M
⊢ ((fun m => m • y) g).2 ∈ orbit M y.2

Tactic:
exact mem_orbit _ _

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma equiv_of_X_eq_of_Y_eq {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 = Q y * P z ^ 3) : P ≈ Q

Proof state:
case h
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
⊢ (fun m => m • Q) (Units.mk0 (P z) hPz / Units.mk0 (Q z) hQz) = P

Tactic:
simp only [Units.smul_def, smul_fin3, Units.val_div_eq_div_val, Units.val_mk0, div_pow, mul_comm,
  mul_div, ← hx, ← hy, mul_div_cancel_right₀ _ <| pow_ne_zero _ hQz, mul_div_cancel_right₀ _ hQz,
  fin3_def]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
⊢ P ≈ Q

Tactic:
use Units.mk0 _ hPz / Units.mk0 _ hQz

Result:
case h
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
⊢ (fun m => m • Q) (Units.mk0 (P z) hPz / Units.mk0 (Q z) hQz) = P
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem IsLindelof.compl_mem_sets (hs : IsLindelof s) {f : Filter X} [CountableInterFilter f]
    (hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f) : sᶜ ∈ f

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f
⊢ sᶜ ∈ f

Tactic:
contrapose! hf

Result:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : sᶜ ∉ f
⊢ ∃ x ∈ s, sᶜ ∉ 𝓝 x ⊓ f

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : sᶜ ∉ f
⊢ ∃ x ∈ s, sᶜ ∉ 𝓝 x ⊓ f

Tactic:
simp only [not_mem_iff_inf_principal_compl, compl_compl, inf_assoc] at hf ⊢

Result:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : (f ⊓ 𝓟 s).NeBot
⊢ ∃ x ∈ s, (𝓝 x ⊓ (f ⊓ 𝓟 s)).NeBot

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : (f ⊓ 𝓟 s).NeBot
⊢ ∃ x ∈ s, (𝓝 x ⊓ (f ⊓ 𝓟 s)).NeBot

Tactic:
exact hs inf_le_right

Result:
no goals
-- Mathlib/Control/Bifunctor.lean
theorem comp_snd {α β₀ β₁ β₂} (g : β₀ → β₁) (g' : β₁ → β₂) (x : F α β₀) :
    snd g' (snd g x) = snd (g' ∘ g) x

Proof state:
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
β₀ β₁ β₂ : Type u₁
g : β₀ → β₁
g' : β₁ → β₂
x : F α β₀
⊢ snd g' (snd g x) = snd (g' ∘ g) x

Tactic:
simp [snd, bimap_bimap]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem _root_.Associated.normalizedFactors_eq {a b : α} (h : Associated a b) :
    normalizedFactors a = normalizedFactors b

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ Multiset.map (⇑normalize) (factors a) = Multiset.map (⇑normalize) (factors b)

Tactic:
have h' : ⇑(normalize (α := α)) = Associates.out ∘ Associates.mk := funext Associates.out_mk

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
h' : ⇑normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map (⇑normalize) (factors a) = Multiset.map (⇑normalize) (factors b)

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
h' : ⇑normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map (⇑normalize) (factors a) = Multiset.map (⇑normalize) (factors b)

Tactic:
rw [h', ← Multiset.map_map, ← Multiset.map_map,
  Associates.rel_associated_iff_map_eq_map.mp (factors_rel_of_associated h)]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ normalizedFactors a = normalizedFactors b

Tactic:
unfold normalizedFactors

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ Multiset.map (⇑normalize) (factors a) = Multiset.map (⇑normalize) (factors b)
-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem hasFDerivAt_polarCoord_symm (p : ℝ × ℝ) :
    HasFDerivAt polarCoord.symm (fderivPolarCoordSymm p) p

Proof state:
p : ℝ × ℝ
⊢ HasFDerivAt (↑polarCoord.symm)
    ((cos p.2 • ContinuousLinearMap.fst ℝ ℝ ℝ + (-p.1 * sin p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ).prod
      (sin p.2 • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 * cos p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ))
    p

Tactic:
convert HasFDerivAt.prod (𝕜 := ℝ)
  (hasFDerivAt_fst.mul ((hasDerivAt_cos p.2).comp_hasFDerivAt p hasFDerivAt_snd))
  (hasFDerivAt_fst.mul ((hasDerivAt_sin p.2).comp_hasFDerivAt p hasFDerivAt_snd)) using 2 <;>
simp [smul_smul, add_comm, neg_mul, smul_neg, neg_smul _ (ContinuousLinearMap.snd ℝ ℝ ℝ)]

Result:
no goals

Proof state:
p : ℝ × ℝ
⊢ HasFDerivAt (↑polarCoord.symm)
    (LinearMap.toContinuousLinearMap
      ((Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)) !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2]))
    p

Tactic:
rw [Matrix.toLin_finTwoProd_toContinuousLinearMap]

Result:
p : ℝ × ℝ
⊢ HasFDerivAt (↑polarCoord.symm)
    ((cos p.2 • ContinuousLinearMap.fst ℝ ℝ ℝ + (-p.1 * sin p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ).prod
      (sin p.2 • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 * cos p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ))
    p

Proof state:
p : ℝ × ℝ
⊢ HasFDerivAt (↑polarCoord.symm) (fderivPolarCoordSymm p) p

Tactic:
unfold fderivPolarCoordSymm

Result:
p : ℝ × ℝ
⊢ HasFDerivAt (↑polarCoord.symm)
    (LinearMap.toContinuousLinearMap
      ((Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)) !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2]))
    p
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem expSeries_hasSum_exp_of_mem_ball' (x : 𝔸)
    (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    HasSum (fun n => (n !⁻¹ : 𝕂) • x ^ n) (exp 𝕂 x)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ HasSum (fun n => (expSeries 𝕂 𝔸 n) fun x_1 => x) (exp 𝕂 x)

Tactic:
exact expSeries_hasSum_exp_of_mem_ball x hx

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ HasSum (fun n => (↑n !)⁻¹ • x ^ n) (exp 𝕂 x)

Tactic:
rw [← expSeries_apply_eq']

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ HasSum (fun n => (expSeries 𝕂 𝔸 n) fun x_1 => x) (exp 𝕂 x)
-- Mathlib/Order/Fin/Basic.lean
theorem zero_eq_top {n : ℕ} [NeZero n] : (0 : Fin n) = ⊤ ↔ n = 1

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ 0 = ⊤ ↔ n = 1

Tactic:
rw [← bot_eq_zero, subsingleton_iff_bot_eq_top, subsingleton_iff_le_one, LE.le.le_iff_eq]

Result:
n : ℕ
inst✝ : NeZero n
⊢ 1 ≤ n

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ 1 ≤ n

Tactic:
exact pos_of_neZero n

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem SymmetricRel.inter {U V : Set (α × α)} (hU : SymmetricRel U) (hV : SymmetricRel V) :
    SymmetricRel (U ∩ V)

Proof state:
α : Type ua
U V : Set (α × α)
hU : SymmetricRel U
hV : SymmetricRel V
⊢ SymmetricRel (U ∩ V)

Tactic:
rw [SymmetricRel, preimage_inter, hU.eq, hV.eq]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/SlashActions.lean
theorem is_invariant_one' (A : SL(2, ℤ)) : (1 : ℍ → ℂ) ∣[(0 : ℤ)] (A : GL(2, ℝ)⁺) = 1

Proof state:
A : SL(2, ℤ)
⊢ 1 ∣[0] ↑A = 1

Tactic:
simpa using is_invariant_one A

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/KleinFour.lean
@[to_additive]
lemma inv_eq_self (x : G) : x⁻¹ = x := inv_eq_self_of_exponent_two (by simp) x

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
x : G
⊢ Monoid.exponent G = 2

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zip_map' (f : α → β) (g : α → γ) (l : Array α) :
    zip (l.map f) (l.map g) = l.map fun a => (f a, g a)

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
toList✝ : List α
⊢ (map f { toList := toList✝ }).zip (map g { toList := toList✝ }) = map (fun a => (f a, g a)) { toList := toList✝ }

Tactic:
simp [List.zip_map']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
l : Array α
⊢ (map f l).zip (map g l) = map (fun a => (f a, g a)) l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
toList✝ : List α
⊢ (map f { toList := toList✝ }).zip (map g { toList := toList✝ }) = map (fun a => (f a, g a)) { toList := toList✝ }
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem squarefree_iff_no_irreducibles {x : R} (hx₀ : x ≠ 0) :
    Squarefree x ↔ ∀ p, Irreducible p → ¬ (p * p ∣ x)

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
hd₀ : d ≠ 0
p : R
irr : Irreducible p
dvd : p ∣ d
⊢ False

Tactic:
exact h p irr ((mul_dvd_mul dvd dvd).trans hd)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
hd₀ : d ≠ 0
⊢ False

Tactic:
obtain ⟨p, irr, dvd⟩ := WfDvdMonoid.exists_irreducible_factor hdu hd₀

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
hd₀ : d ≠ 0
p : R
irr : Irreducible p
dvd : p ∣ d
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
⊢ Squarefree x ↔ ∀ (p : R), Irreducible p → ¬p * p ∣ x

Tactic:
refine ⟨fun h p hp hp' ↦ hp.not_unit (h p hp'), fun h d hd ↦ by_contra fun hdu ↦ ?_⟩

Result:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
⊢ False

Tactic:
have hd₀ : d ≠ 0 := ne_zero_of_dvd_ne_zero (ne_zero_of_dvd_ne_zero hx₀ hd) (dvd_mul_left d d)

Result:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
hd₀ : d ≠ 0
⊢ False
-- Mathlib/Computability/Reduce.lean
theorem manyOneReducible_refl {α} [Primcodable α] (p : α → Prop) : p ≤₀ p :=
  ⟨id, Computable.id, by simp⟩

Proof state:
α : Type u_1
inst✝ : Primcodable α
p : α → Prop
⊢ ∀ (a : α), p a ↔ p (id a)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem range_algebraMap {R A : Type*} [CommRing R] [CommRing A] [Algebra R A]
    (S : Subalgebra R A) : (algebraMap S A).range = S.toSubring

Proof state:
R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (algebraMap (↥S) A).range = S.toSubring

Tactic:
rw [algebraMap_eq, Algebra.id.map_eq_id, RingHom.id_comp, ← toSubring_subtype,
  Subring.range_subtype]

Result:
no goals
-- Mathlib/Order/GameAdd.lean
theorem GameAdd.fix_eq {C : α → α → Sort*} (hr : WellFounded rα)
    (IH : ∀ a₁ b₁, (∀ a₂ b₂, Sym2.GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁) (a b : α) :
    GameAdd.fix hr IH a b = IH a b fun a' b' _ => GameAdd.fix hr IH a' b'

Proof state:
α : Type u_1
rα : α → α → Prop
C : α → α → Sort u_3
hr : WellFounded rα
IH : (a₁ b₁ : α) → ((a₂ b₂ : α) → GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁
a b : α
⊢ fix hr IH a b = IH a b fun a' b' x => fix hr IH a' b'

Tactic:
dsimp [GameAdd.fix]

Result:
α : Type u_1
rα : α → α → Prop
C : α → α → Sort u_3
hr : WellFounded rα
IH : (a₁ b₁ : α) → ((a₂ b₂ : α) → GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁
a b : α
⊢ ⋯.fix (fun x IH' => IH x.1 x.2 fun a' b' => IH' (a', b')) (a, b) =
    IH a b fun a' b' x => ⋯.fix (fun x IH' => IH x.1 x.2 fun a' b' => IH' (a', b')) (a', b')

Proof state:
α : Type u_1
rα : α → α → Prop
C : α → α → Sort u_3
hr : WellFounded rα
IH : (a₁ b₁ : α) → ((a₂ b₂ : α) → GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁
a b : α
⊢ ⋯.fix (fun x IH' => IH x.1 x.2 fun a' b' => IH' (a', b')) (a, b) =
    IH a b fun a' b' x => ⋯.fix (fun x IH' => IH x.1 x.2 fun a' b' => IH' (a', b')) (a', b')

Tactic:
exact WellFounded.fix_eq _ _ _

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem convolutionExistsAt_flip :
    ConvolutionExistsAt g f x L.flip μ ↔ ConvolutionExistsAt f g x L μ

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 E'
inst✝⁶ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁵ : MeasurableSpace G
μ : Measure G
inst✝⁴ : AddCommGroup G
inst✝³ : MeasurableNeg G
inst✝² : μ.IsAddLeftInvariant
inst✝¹ : MeasurableAdd G
inst✝ : μ.IsNegInvariant
⊢ ConvolutionExistsAt g f x L.flip μ ↔ ConvolutionExistsAt f g x L μ

Tactic:
simp_rw [ConvolutionExistsAt, ← integrable_comp_sub_left (fun t => L (f t) (g (x - t))) x,
  sub_sub_cancel, flip_apply]

Result:
no goals