harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convolution.lean
theorem _root_.HasCompactSupport.contDiff_convolution_left [μ.IsAddLeftInvariant] [μ.IsNegInvariant]
    {n : ℕ∞} (hcf : HasCompactSupport f) (hf : ContDiff 𝕜 n f) (hg : LocallyIntegrable g μ) :
    ContDiff 𝕜 n (f ⋆[L, μ] g)

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'
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : μ.IsNegInvariant
n : ℕ∞
hcf : HasCompactSupport f
hf : ContDiff 𝕜 (↑n) f
hg : LocallyIntegrable g μ
⊢ ContDiff 𝕜 (↑n) (g ⋆[L.flip, μ] f)

Tactic:
exact hcf.contDiff_convolution_right L.flip hg hf

Result:
no goals

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'
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : μ.IsNegInvariant
n : ℕ∞
hcf : HasCompactSupport f
hf : ContDiff 𝕜 (↑n) f
hg : LocallyIntegrable g μ
⊢ ContDiff 𝕜 (↑n) (f ⋆[L, μ] g)

Tactic:
rw [← convolution_flip]

Result:
𝕜 : 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'
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : μ.IsNegInvariant
n : ℕ∞
hcf : HasCompactSupport f
hf : ContDiff 𝕜 (↑n) f
hg : LocallyIntegrable g μ
⊢ ContDiff 𝕜 (↑n) (g ⋆[L.flip, μ] f)
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem leftUnitor_inv_naturality {f g : a ⟶ b} (η : f ⟶ g) :
    η ≫ (λ_ g).inv = (λ_ f).inv ≫ 𝟙 a ◁ η

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

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem inv_zpow' {A : M} (h : IsUnit A.det) (n : ℤ) : A⁻¹ ^ n = A ^ (-n)

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℤ
⊢ A⁻¹ ^ n = A ^ (-n)

Tactic:
rw [zpow_neg h, inv_zpow]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma one_le_cfc_iff (f : R → R) (a : A)
    (hf : ContinuousOn f (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.837198) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ 1 ≤ cfc f a ↔ ∀ x ∈ spectrum R a, 1 ≤ f x

Tactic:
simpa using algebraMap_le_cfc_iff f 1 a

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma mul_eq_right (hb : b ≠ 0) : a * b = b ↔ a = 1

Proof state:
a b : ℕ
hb : b ≠ 0
⊢ a * b = b ↔ a = 1

Tactic:
simpa using Nat.mul_left_inj hb (c := 1)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_filter_not_mul_prod_filter (s : Finset α) (p : α → Prop) [DecidablePred p]
    [∀ x, Decidable (¬p x)] (f : α → β) :
    (∏ x ∈ s.filter fun x ↦ ¬p x, f x) * ∏ x ∈ s.filter p, f x = ∏ x ∈ s, f x

Proof state:
α : Type u_3
β : Type u_4
inst✝² : CommMonoid β
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
f : α → β
⊢ (∏ x ∈ filter (fun x => ¬p x) s, f x) * ∏ x ∈ filter p s, f x = ∏ x ∈ s, f x

Tactic:
rw [mul_comm, prod_filter_mul_prod_filter_not]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsPath.reverse {u v : V} {p : G.Walk u v} (h : p.IsPath) : p.reverse.IsPath

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsPath
⊢ p.reverse.IsPath

Tactic:
simpa [isPath_def] using h

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean
theorem homotopyEquiv_inv_π {X : C} (P Q : ProjectiveResolution X) :
    (homotopyEquiv P Q).inv ≫ P.π = Q.π

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P Q : ProjectiveResolution X
⊢ (P.homotopyEquiv Q).inv ≫ P.π = Q.π

Tactic:
simp [homotopyEquiv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_eq : ∀ {a b : Bool}, ((!a) = b) ↔ (a ≠ b)

Proof state:
⊢ ∀ {a b : Bool}, (!a) = b ↔ a ≠ b

Tactic:
decide

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem not_isPredPrelimit_iff' : ¬ IsPredPrelimit a ↔ a ∈ range (pred : α → α)

Proof state:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
⊢ ¬IsPredPrelimit a ↔ a ∈ range pred

Tactic:
simp_rw [isPredPrelimit_iff_pred_ne, not_forall, not_ne_iff, mem_range]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem memLp_map_measure_iff (hg : AEStronglyMeasurable g (Measure.map f μ))
    (hf : AEMeasurable f μ) : MemLp g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ MemLp g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ

Tactic:
simp [MemLp, eLpNorm_map_measure hg hf, hg.comp_aemeasurable hf, hg]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma CompleteOrthogonalIdempotents.pair_iff'ₛ {x y : R} :
    CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ y * x = 0 ∧ x + y = 1

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
⊢ CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ y * x = 0 ∧ x + y = 1

Tactic:
simp [iff_ortho_complete, Pairwise, Fin.forall_fin_two, and_assoc]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem generate_eq_generate_inter (s : Set (Set α)) :
    generate s = generate (sInter '' { t | Set.Finite t ∧ t ⊆ s })

Proof state:
α : Type u_1
s : Set (Set α)
⊢ ⋯.filter = (FilterBasis.ofSets s).filter

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
s : Set (Set α)
⊢ generate s = generate (sInter '' {t | t.Finite ∧ t ⊆ s})

Tactic:
rw [← FilterBasis.ofSets_sets, FilterBasis.generate, ← (hasBasis_generate s).filter_eq]

Result:
α : Type u_1
s : Set (Set α)
⊢ ⋯.filter = (FilterBasis.ofSets s).filter
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_sub : exp (x - y) = exp x / exp y

Proof state:
x y : ℝ
⊢ rexp (x - y) = rexp x / rexp y

Tactic:
simp [sub_eq_add_neg, exp_add, exp_neg, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Order/Fin/Tuple.lean
lemma finSuccAboveOrderIso_symm_apply_ne_last {p : Fin (n + 1)} (h : p ≠ Fin.last n)
    (x : { x : Fin (n + 1) // x ≠ p }) :
    (finSuccAboveEquiv p).symm x = (p.castLT (Fin.val_lt_last h)).predAbove x

Proof state:
n : ℕ
p : Fin (n + 1)
h : p ≠ last n
x : { x // x ≠ p }
⊢ some ((finSuccAboveEquiv p).symm x) = some ((p.castLT ⋯).predAbove ↑x)

Tactic:
simpa [finSuccAboveEquiv, OrderIso.symm] using finSuccEquiv'_ne_last_apply h x.property

Result:
no goals

Proof state:
n : ℕ
p : Fin (n + 1)
h : p ≠ last n
x : { x // x ≠ p }
⊢ (finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x

Tactic:
rw [← Option.some_inj]

Result:
n : ℕ
p : Fin (n + 1)
h : p ≠ last n
x : { x // x ≠ p }
⊢ some ((finSuccAboveEquiv p).symm x) = some ((p.castLT ⋯).predAbove ↑x)
-- Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean
theorem foldl_ι (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) (m : M) : foldl Q f hf n (ι Q m) = f m n

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
m : M
⊢ ((foldl Q f hf) n) ((ι Q) m) = (f m) n

Tactic:
rw [← foldr_reverse, reverse_ι, foldr_ι]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_eq_range_psigma (s : ι → Set β) : ⋃ i, s i = range fun a : Σ'i, s i => a.2

Proof state:
β : Type u_2
ι : Sort u_5
s : ι → Set β
⊢ ⋃ i, s i = range fun a => ↑a.snd

Tactic:
simp [Set.ext_iff]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem sub_algebraMap {B : Type*} [CommRing B] [Algebra A B] (x : B)
    (a : A) : minpoly A (x - algebraMap A B a) = (minpoly A x).comp (X + C a)

Proof state:
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
⊢ minpoly A (x - (algebraMap A B) a) = (minpoly A x).comp (X + C a)

Tactic:
simpa [sub_eq_add_neg] using add_algebraMap x (-a)

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_preimage_mem_nhds {x : M} (h : x ∈ f.source) (ht : t ∈ 𝓝 x) :
    (f.extend I).symm ⁻¹' t ∈ 𝓝 (f.extend I x)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝 x
⊢ ↑(f.extend I).symm ⁻¹' t ∈ 𝓝 (↑(f.extend I) x)

Tactic:
apply (continuousAt_extend_symm f h).preimage_mem_nhds

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝 x
⊢ t ∈ 𝓝 (↑(f.extend I).symm (↑(f.extend I) x))

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝 x
⊢ x ∈ (f.extend I).source

Tactic:
rwa [f.extend_source]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝 x
⊢ t ∈ 𝓝 (↑(f.extend I).symm (↑(f.extend I) x))

Tactic:
rwa [(f.extend I).left_inv]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝 x
⊢ x ∈ (f.extend I).source
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_div_iff_mul_eq'' : a = b / c ↔ c * a = b

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a = b / c ↔ c * a = b

Tactic:
rw [eq_div_iff_mul_eq', mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem drop_tail (l : List α) (n : Nat) : l.tail.drop n = l.drop (n + 1)

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ drop n l.tail = drop (n + 1) l

Tactic:
rw [Nat.add_comm, ← drop_drop, drop_one]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
lemma prod_nat_mod (l : List ℕ) (n : ℕ) : l.prod % n = (l.map (· % n)).prod % n

Proof state:
case cons
n a : ℕ
l : List ℕ
ih : l.prod % n = (map (fun x => x % n) l).prod % n
⊢ (a :: l).prod % n = (map (fun x => x % n) (a :: l)).prod % n

Tactic:
simpa only [prod_cons, map_cons, Nat.mod_mul_mod, Nat.mul_mod_mod] using congr((a * $ih) % n)

Result:
no goals

Proof state:
case nil
n : ℕ
⊢ [].prod % n = (map (fun x => x % n) []).prod % n

Tactic:
simp only [Nat.zero_mod, map_nil]

Result:
no goals

Proof state:
l : List ℕ
n : ℕ
⊢ l.prod % n = (map (fun x => x % n) l).prod % n

Tactic:
induction l with
| nil => simp only [Nat.zero_mod, map_nil]
| cons a l ih =>
  simpa only [prod_cons, map_cons, Nat.mod_mul_mod, Nat.mul_mod_mod] using congr((a * $ih) % n)

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem spanSingleton_inv_mul {x : K} (hx : x ≠ 0) :
    (spanSingleton R₁⁰ x)⁻¹ * spanSingleton R₁⁰ x = 1

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : K
hx : x ≠ 0
⊢ (spanSingleton R₁⁰ x)⁻¹ * spanSingleton R₁⁰ x = 1

Tactic:
rw [mul_comm, spanSingleton_mul_inv K hx]

Result:
no goals
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem perpBisector_self (p : P) : perpBisector p p = ⊤ :=
  top_unique fun _ ↦ by simp [mem_perpBisector_iff_inner_eq_inner]

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p x✝ : P
⊢ x✝ ∈ ↑⊤ → x✝ ∈ ↑(perpBisector p p)

Tactic:
simp [mem_perpBisector_iff_inner_eq_inner]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Inductions.lean
theorem divX_C_mul_X_pow : divX (C a * X ^ n) = if n = 0 then 0 else C a * X ^ (n - 1)

Proof state:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
⊢ (C a * X ^ n).divX = if n = 0 then 0 else C a * X ^ (n - 1)

Tactic:
simp only [divX_C_mul, divX_X_pow, mul_ite, mul_zero]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem canonicalEquiv_coeIdeal (I : Ideal R) : canonicalEquiv S P P' I = I

Proof state:
case a
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : Ideal R
x✝ : P'
⊢ x✝ ∈ (canonicalEquiv S P P') ↑I ↔ x✝ ∈ ↑I

Tactic:
simp [IsLocalization.map_eq]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : Ideal R
⊢ (canonicalEquiv S P P') ↑I = ↑I

Tactic:
ext

Result:
case a
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : Ideal R
x✝ : P'
⊢ x✝ ∈ (canonicalEquiv S P P') ↑I ↔ x✝ ∈ ↑I
-- Mathlib/Data/Sign.lean
@[simp, norm_cast]
lemma coe_neg {α : Type*} [One α] [SubtractionMonoid α] (s : SignType) :
    (↑(-s) : α) = -↑s

Proof state:
α : Type u_2
inst✝¹ : One α
inst✝ : SubtractionMonoid α
s : SignType
⊢ ↑(-s) = -↑s

Tactic:
cases s <;> simp

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem dvd_gcd_mul_iff_dvd_mul : x ∣ gcd x n * m ↔ x ∣ n * m

Proof state:
x n m : ℕ
x✝ : x ∣ n * m
y : ℕ
hy : n * m = x * y
⊢ x ∣ x * m.gcd y

Tactic:
exact dvd_mul_right x (gcd m y)

Result:
no goals

Proof state:
x n m : ℕ
x✝ : x ∣ n * m
y : ℕ
hy : n * m = x * y
⊢ x ∣ x.gcd n * m

Tactic:
rw [← gcd_mul_right, hy, gcd_mul_left]

Result:
x n m : ℕ
x✝ : x ∣ n * m
y : ℕ
hy : n * m = x * y
⊢ x ∣ x * m.gcd y
-- Mathlib/Analysis/Complex/RealDeriv.lean
theorem HasDerivAt.complexToReal_fderiv' {f : ℂ → E} {x : ℂ} {f' : E} (h : HasDerivAt f f' x) :
    HasFDerivAt f (reCLM.smulRight f' + I • imCLM.smulRight f') x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
x : ℂ
f' : E
h : HasDerivAt f f' x
⊢ HasFDerivAt f (reCLM.smulRight f' + I • imCLM.smulRight f') x

Tactic:
simpa only [Complex.restrictScalars_one_smulRight'] using h.hasFDerivAt.restrictScalars ℝ

Result:
no goals
-- Mathlib/Algebra/Homology/Opposite.lean
@[simp]
lemma quasiIso_opFunctor_map_iff
    {K L : HomologicalComplex V c} (φ : K ⟶ L)
    [∀ i, K.HasHomology i] [∀ i, L.HasHomology i] :
    QuasiIso ((opFunctor _ _).map φ.op) ↔ QuasiIso φ

Proof state:
ι : Type u_1
V : Type u_2
inst✝³ : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝² : HasZeroMorphisms V
K L : HomologicalComplex V c
φ : K ⟶ L
inst✝¹ : ∀ (i : ι), K.HasHomology i
inst✝ : ∀ (i : ι), L.HasHomology i
⊢ QuasiIso ((opFunctor V c).map φ.op) ↔ QuasiIso φ

Tactic:
simp only [quasiIso_iff, quasiIsoAt_opFunctor_map_iff]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
@[simp] lemma expect_empty (f : ι → M) : 𝔼 i ∈ ∅, f i = 0

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
f : ι → M
⊢ 𝔼 i ∈ ∅, f i = 0

Tactic:
simp [expect]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem isSome_eq_isSome : (isSome x = isSome y) ↔ (x = none ↔ y = none)

Proof state:
α✝¹ : Type u_1
x : Option α✝¹
α✝ : Type u_2
y : Option α✝
⊢ x.isSome = y.isSome ↔ (x = none ↔ y = none)

Tactic:
cases x <;> cases y <;> simp

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem prod_top (s : NonUnitalSubring R) :
    s.prod (⊤ : NonUnitalSubring S) = s.comap (NonUnitalRingHom.fst R S) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_fst]

Proof state:
R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
s : NonUnitalSubring R
x : R × S
⊢ x ∈ s.prod ⊤ ↔ x ∈ comap (NonUnitalRingHom.fst R S) s

Tactic:
simp [mem_prod, MonoidHom.coe_fst]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean
@[simp]
lemma partialLeftAdjointHomEquiv_map {X Y : F.PartialLeftAdjointSource}
    (f : X ⟶ Y) :
    F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f) =
      by exact f ≫ F.partialLeftAdjointHomEquiv (𝟙 _)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X Y : F.PartialLeftAdjointSource
f : X ⟶ Y
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f) =
    f ≫ F.partialLeftAdjointHomEquiv (𝟙 (F.partialLeftAdjointObj Y))

Tactic:
simp [partialLeftAdjointMap]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X Y : F.PartialLeftAdjointSource
f : X ⟶ Y
⊢ X.obj ⟶ F.obj (F.partialLeftAdjointObj Y)

Tactic:
exact f ≫ F.partialLeftAdjointHomEquiv (𝟙 _)

Result:
no goals
-- Mathlib/Topology/JacobsonSpace.lean
lemma closure_closedPoints [JacobsonSpace X] : closure (closedPoints X) = Set.univ

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
⊢ closure (closedPoints X) = Set.univ

Tactic:
simpa using closure_inter_closedPoints isClosed_univ

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem getElem_attachWith {xs : Array α} {P : α → Prop} {H : ∀ a ∈ xs, P a}
    {i : Nat} (h : i < (xs.attachWith P H).size) :
    (xs.attachWith P H)[i] = ⟨xs[i]'(by simpa using h), H _ (getElem_mem (by simpa using h))⟩ :=
  getElem_pmap _ _ h

Proof state:
α : Type ?u.38564
xs : Array α
P : α → Prop
H : ∀ (a : α), a ∈ xs → P a
i : Nat
h : i < (xs.attachWith P H).size
⊢ i < xs.size

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem preimage_id (s : Set α) : preimage (@Eq α) s = s

Proof state:
α : Type u_1
s : Set α
⊢ preimage Eq s = s

Tactic:
simp only [preimage, inv_id, image_id]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem zero_eq_lift_iff {a : Cardinal.{u}} :
    (0 : Cardinal) = lift.{v} a ↔ 0 = a

Proof state:
a : Cardinal.{u}
⊢ 0 = lift.{v, u} a ↔ 0 = a

Tactic:
simpa using nat_eq_lift_iff (n := 0)

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem pullbackP1Iso_inv_fst (i : 𝒰.J) :
    (pullbackP1Iso 𝒰 f g i).inv ≫ pullback.fst _ _ = (gluing 𝒰 f g).ι i

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
⊢ (pullbackP1Iso 𝒰 f g i).inv ≫ pullback.fst (p1 𝒰 f g) (𝒰.map i) = (gluing 𝒰 f g).ι i

Tactic:
simp_rw [pullbackP1Iso, pullback.lift_fst]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Control/ForInStep/Lemmas.lean
theorem ForInStep.done_bindList [Monad m]
    (f : α → β → m (ForInStep β)) (a l) :
    (ForInStep.done a).bindList f l = pure (.done a)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m (ForInStep β)
a : β
l : List α
⊢ bindList f l (done a) = pure (done a)

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem findSome?_toArray (f : α → Option β) (l : List α) :
    l.toArray.findSome? f = l.findSome? f

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ Array.findSome? f l.toArray = findSome? f l

Tactic:
rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run]

Result:
no goals
-- Mathlib/NumberTheory/SumFourSquares.lean
theorem euler_four_squares {R : Type*} [CommRing R] (a b c d x y z w : R) :
    (a * x - b * y - c * z - d * w) ^ 2 + (a * y + b * x + c * w - d * z) ^ 2 +
      (a * z - b * w + c * x + d * y) ^ 2 + (a * w + b * z - c * y + d * x) ^ 2 =
      (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
a b c d x y z w : R
⊢ (a * x - b * y - c * z - d * w) ^ 2 + (a * y + b * x + c * w - d * z) ^ 2 + (a * z - b * w + c * x + d * y) ^ 2 +
      (a * w + b * z - c * y + d * x) ^ 2 =
    (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2)

Tactic:
ring

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem dist_def (f g : α →₁[μ] β) : dist f g = (∫⁻ a, edist (f a) (g a) ∂μ).toReal

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ dist f g = (∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ).toReal

Tactic:
simp_rw [dist_edist, edist_def]

Result:
no goals
-- Mathlib/Tactic/NormNum/Pow.lean
theorem isNat_pow {α} [Semiring α] : ∀ {f : α → ℕ → α} {a : α} {b a' b' c : ℕ},
    f = HPow.hPow → IsNat a a' → IsNat b b' → Nat.pow a' b' = c → IsNat (f a b) c
  | _, _, _, _, _, _, rfl, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨by simp⟩

Proof state:
α : Type u_1
inst✝ : Semiring α
n✝¹ n✝ : ℕ
⊢ ↑n✝¹ ^ ↑n✝ = ↑(n✝¹.pow n✝)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem not_bddAbove_iff' : ¬BddAbove s ↔ ∀ x, ∃ y ∈ s, ¬y ≤ x

Proof state:
α : Type u
inst✝ : Preorder α
s : Set α
⊢ ¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, ¬y ≤ x

Tactic:
simp [BddAbove, upperBounds, Set.Nonempty]

Result:
no goals
-- Mathlib/Data/List/EditDistance/Defs.lean
theorem suffixLevenshtein_eq (xs : List α) (y ys) :
    impl C xs y (suffixLevenshtein C xs ys) = suffixLevenshtein C xs (y :: ys)

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
y : β
ys : List β
⊢ impl C xs y (suffixLevenshtein C xs ys) = suffixLevenshtein C xs (y :: ys)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem closedBall_one_mul_singleton : closedBall 1 δ * {x} = closedBall x δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ closedBall 1 δ * {x} = closedBall x δ

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Basic.lean
theorem isClosed_of_pairwise_le_dist {s : Set γ} {ε : ℝ} (hε : 0 < ε)
    (hs : s.Pairwise fun x y => ε ≤ dist x y) : IsClosed s :=
  isClosed_of_spaced_out (dist_mem_uniformity hε) <| by simpa using hs

Proof state:
γ : Type w
inst✝ : MetricSpace γ
s : Set γ
ε : ℝ
hε : 0 < ε
hs : s.Pairwise fun x y => ε ≤ dist x y
⊢ s.Pairwise fun x y => (x, y) ∉ {p | dist p.1 p.2 < ε}

Tactic:
simpa using hs

Result:
no goals