harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Composition/Lemmas.lean
lemma parallelComp_id_left_comp_parallelComp
    {η : Kernel α' γ} [IsSFiniteKernel η] {ξ : Kernel γ δ} [IsSFiniteKernel ξ] :
    (Kernel.id ∥ₖ ξ) ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
α' : Type u_5
mα' : MeasurableSpace α'
inst✝² : IsSFiniteKernel κ
η : Kernel α' γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel γ δ
inst✝ : IsSFiniteKernel ξ
⊢ Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η)

Tactic:
ext a

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
α' : Type u_5
mα' : MeasurableSpace α'
inst✝² : IsSFiniteKernel κ
η : Kernel α' γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel γ δ
inst✝ : IsSFiniteKernel ξ
a : α × α'
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η)) a) s✝ = ((κ ∥ₖ (ξ ∘ₖ η)) a) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
α' : Type u_5
mα' : MeasurableSpace α'
inst✝² : IsSFiniteKernel κ
η : Kernel α' γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel γ δ
inst✝ : IsSFiniteKernel ξ
a : α × α'
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((Kernel.id ∥ₖ ξ ∘ₖ (κ ∥ₖ η)) a) s✝ = ((κ ∥ₖ (ξ ∘ₖ η)) a) s✝

Tactic:
rw [parallelComp_apply, comp_apply, comp_apply, parallelComp_apply, Measure.prod_comp_right]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
@[reassoc (attr := simp), elementwise (attr := simp)]
lemma isoZeroCocycles_inv_comp_iCocycles :
    (isoZeroCocycles A).inv ≫ iCocycles A 0 =
        ModuleCat.ofHom A.ρ.invariants.subtype ≫ (zeroCochainsLequiv A).toModuleIso.inv

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (isoZeroCocycles A).inv ≫ iCocycles A 0 =
    ModuleCat.ofHom A.ρ.invariants.subtype ≫ (zeroCochainsLequiv A).toModuleIso.inv

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, isoZeroCocycles_hom_comp_subtype]

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Proper.lean
theorem mem_dual {K : ProperCone ℝ E} {y : E} : y ∈ dual K ↔ ∀ ⦃x⦄, x ∈ K → 0 ≤ ⟪x, y⟫_ℝ

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
K : ProperCone ℝ E
y : E
⊢ y ∈ K.dual ↔ ∀ ⦃x : E⦄, x ∈ K → 0 ≤ ⟪x, y⟫_ℝ

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem sub'_one (a : PosNum) : sub' a 1 = (pred' a).toZNum

Proof state:
a : PosNum
⊢ a.sub' 1 = a.pred'.toZNum

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem apply_pow_apply_eq_iff (f : Perm α) (n : ℕ) {x : α} :
    f ((f ^ n) x) = (f ^ n) x ↔ f x = x

Proof state:
α : Type u_1
f : Perm α
n : ℕ
x : α
⊢ f ((f ^ n) x) = (f ^ n) x ↔ f x = x

Tactic:
rw [← mul_apply, Commute.self_pow f, mul_apply, apply_eq_iff_eq]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
@[simp] lemma insertNth_removeNth (p : Fin (n + 1)) (x) (f : ∀ j, α j) :
    insertNth p x (removeNth p f) = update f p x

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
f : (j : Fin (n + 1)) → α j
⊢ p.insertNth x (p.removeNth f) = update f p x

Tactic:
simp [Fin.insertNth_eq_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
lemma unitForward_unitBackward {F : Cᵒᵖ ⥤ Type v} (η : F ⟶ A) (X : C) :
    unitForward η X ∘ unitBackward η X = id :=
  funext fun x => by simp [unitForward, unitBackward]

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
x : F.obj (op X)
⊢ (unitForward η X ∘ unitBackward η X) x = id x

Tactic:
simp [unitForward, unitBackward]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem dotProduct_comm [AddCommMonoid α] [CommSemigroup α] (v w : m → α) : v ⬝ᵥ w = w ⬝ᵥ v

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : AddCommMonoid α
inst✝ : CommSemigroup α
v w : m → α
⊢ v ⬝ᵥ w = w ⬝ᵥ v

Tactic:
simp_rw [dotProduct, mul_comm]

Result:
no goals
-- Mathlib/Data/Fin/Rev.lean
/-- `rev` commutes with `succAbove`. -/
lemma rev_succAbove (p : Fin (n + 1)) (i : Fin n) :
    rev (succAbove p i) = succAbove (rev p) (rev i)

Proof state:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ (p.succAbove i).rev = p.rev.succAbove i.rev

Tactic:
rw [succAbove_rev_left, rev_rev]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
@[simp]
lemma isCycle_reverse {p : G.Walk u u} : p.reverse.IsCycle ↔ p.IsCycle where
  mp h

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

Tactic:
simpa using h.reverse

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem powerset_cons (a : α) (s) : powerset (a ::ₘ s) = powerset s + map (cons a) (powerset s) :=
  Quotient.inductionOn s fun l => by simp [Function.comp_def]

Proof state:
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (a ::ₘ ⟦l⟧).powerset = powerset ⟦l⟧ + map (cons a) (powerset ⟦l⟧)

Tactic:
simp [Function.comp_def]

Result:
no goals
-- Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean
@[reassoc (attr := simp)]
lemma idem_f (P : Karoubi (Karoubi C)) : P.p.f ≫ P.p.f = P.p.f

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi (Karoubi C)
⊢ P.p.f ≫ P.p.f = P.p.f

Tactic:
simpa only [hom_ext_iff, comp_f] using P.idem

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma desc_f (p q : ℤ) (hpq : p + 1 = q) :
    (desc φ α β eq).f p = (fst φ).1.v p q hpq ≫ α.v q p (by omega) +
      (snd φ).v p p (add_zero p) ≫ β.f p

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
p q : ℤ
hpq : p + 1 = q
⊢ (desc φ α β eq).f p = (↑(fst φ)).v p q hpq ≫ α.v q p ⋯ + (snd φ).v p p ⋯ ≫ β.f p

Tactic:
simp [ext_from_iff _ _ _ hpq]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.161614, u_1} C
inst✝³ : Category.{?u.161618, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
p q : ℤ
hpq : p + 1 = q
⊢ q + -1 = p

Tactic:
omega

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem image_update_Ico_left (f : ∀ i, α i) (i : ι) (a : α i) :
    update f i '' Ico a (f i) = Ico (update f i a) f

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Ico a (f i) = Ico (update f i a) f

Tactic:
simpa using image_update_Ico f i a (f i)

Result:
no goals
-- Mathlib/Logic/Function/Conjugate.lean
theorem isIdempotent_right [Std.IdempotentOp ga] (h : Semiconj₂ f ga gb) (h_surj : Surjective f) :
    Std.IdempotentOp gb :=
  ⟨h_surj.forall.2 fun x ↦ by simp only [← h.eq, Std.IdempotentOp.idempotent (op := ga)]⟩

Proof state:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.IdempotentOp ga
h : Semiconj₂ f ga gb
h_surj : Surjective f
x : α
⊢ gb (f x) (f x) = f x

Tactic:
simp only [← h.eq, Std.IdempotentOp.idempotent (op := ga)]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_eq_bot {a b : α} : a ∆ b = ⊥ ↔ a = b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b = ⊥ ↔ a = b

Tactic:
simp_rw [symmDiff, sup_eq_bot_iff, sdiff_eq_bot_iff, le_antisymm_iff]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma ringEquivCongr_intCast {a b : ℕ} (h : a = b) (z : ℤ) :
    ZMod.ringEquivCongr h z = z

Proof state:
a : ℕ
z : ℤ
⊢ (ringEquivCongr ⋯) ↑z = ↑z

Tactic:
cases a <;> rfl

Result:
no goals

Proof state:
a b : ℕ
h : a = b
z : ℤ
⊢ (ringEquivCongr h) ↑z = ↑z

Tactic:
subst h

Result:
a : ℕ
z : ℤ
⊢ (ringEquivCongr ⋯) ↑z = ↑z
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem map_snd_add_zipIdx_eq_zipIdx (l : Array α) (n k : Nat) :
    map (Prod.map id (· + n)) (zipIdx l k) = zipIdx l (n + k) :=
  ext_getElem? fun i ↦ by simp [(· ∘ ·), Nat.add_comm, Nat.add_left_comm]; rfl

Proof state:
α : Type u_1
l : Array α
n k i : Nat
⊢ Option.map ((Prod.map id fun x => n + x) ∘ fun a => (a, k + i)) l[i]? = Option.map (fun a => (a, n + (k + i))) l[i]?

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem pairwise_disjoint_Ioo_intCast : Pairwise (Disjoint on fun n : ℤ => Ioo (n : α) (n + 1)) :=
  by simpa only [zero_add] using pairwise_disjoint_Ioo_add_intCast (0 : α)

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

Tactic:
simpa only [zero_add] using pairwise_disjoint_Ioo_add_intCast (0 : α)

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem opNorm_le_of_lipschitz {f : E →SL[σ₁₂] F} {K : ℝ≥0} (hf : LipschitzWith K f) : ‖f‖ ≤ K :=
  f.opNorm_le_bound K.2 fun x => by
    simpa only [dist_zero_right, f.map_zero] using hf.dist_le_mul x 0

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
K : ℝ≥0
hf : LipschitzWith K ⇑f
x : E
⊢ ‖f x‖ ≤ ↑K * ‖x‖

Tactic:
simpa only [dist_zero_right, f.map_zero] using hf.dist_le_mul x 0

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem Left.one_lt_inv_iff : 1 < a⁻¹ ↔ a < 1

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a : α
⊢ 1 < a⁻¹ ↔ a < 1

Tactic:
rw [← mul_lt_mul_iff_left a, mul_inv_cancel, mul_one]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem cons_eq_insert (a s h) : @cons α a s h = insert a s :=
  ext fun a => by simp

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
s : Finset α
h : a✝ ∉ s
a : α
⊢ a ∈ cons a✝ s h ↔ a ∈ insert a✝ s

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem SpectralRadius.of_subsingleton [Subsingleton A] (a : A) : spectralRadius 𝕜 a = 0

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : Subsingleton A
a : A
⊢ spectralRadius 𝕜 a = 0

Tactic:
simp [spectralRadius]

Result:
no goals
-- Mathlib/Topology/Sets/Closeds.lean
theorem mem_iInf {ι} {x : α} {s : ι → Closeds α} : x ∈ iInf s ↔ ∀ i, x ∈ s i

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
x : α
s : ι → Closeds α
⊢ x ∈ iInf s ↔ ∀ (i : ι), x ∈ s i

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean
theorem convolution_eq_right {x₀ : G} (hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀) :
    (φ ⋆[lsmul ℝ ℝ, μ] g : G → E') x₀ = integral μ φ • g x₀

Proof state:
G : Type uG
E' : Type uE'
inst✝⁶ : NormedAddCommGroup E'
g : G → E'
inst✝⁵ : MeasurableSpace G
μ : Measure G
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : HasContDiffBump G
inst✝ : CompleteSpace E'
φ : ContDiffBump 0
x₀ : G
hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀
⊢ (↑φ ⋆[lsmul ℝ ℝ, μ] g) x₀ = integral μ ↑φ • g x₀

Tactic:
simp_rw [convolution_eq_right' _ φ.support_eq.subset hg, lsmul_apply, integral_smul_const]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem right_mem_Iic : a ∈ Iic a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ a ∈ Iic a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_two_pi : cos (2 * π) = 1

Proof state:
⊢ cos (2 * π) = 1

Tactic:
simp [two_mul, cos_add]

Result:
no goals
-- Mathlib/Data/String/Basic.lean
theorem asString_inj {l l' : List Char} : l.asString = l'.asString ↔ l = l' :=
  ⟨fun h ↦ by rw [← toList_asString l, ← toList_asString l', toList_inj, h],
   fun h ↦ h ▸ rfl⟩

Proof state:
l l' : List Char
h : l.asString = l'.asString
⊢ l = l'

Tactic:
rw [← toList_asString l, ← toList_asString l', toList_inj, h]

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem lcm_zero_right (x : R) : lcm x 0 = 0

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x : R
⊢ lcm x 0 = 0

Tactic:
rw [lcm, mul_zero, zero_div]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
lemma cylinderEvents_le_pi : cylinderEvents (π := π) Δ ≤ MeasurableSpace.pi

Proof state:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
⊢ cylinderEvents Δ ≤ MeasurableSpace.pi

Tactic:
simpa using cylinderEvents_mono (subset_univ _)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_closedBall' (x : E) {r : ℝ} (hr : 0 ≤ r) :
    μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 ≤ r
⊢ μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1)

Tactic:
rw [← addHaar_closedBall_mul μ x hr zero_le_one, mul_one]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem HasStrictFDerivAt.sub (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) :
    HasStrictFDerivAt (fun x => f x - g x) (f' - g') 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 g : E → F
f' g' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
hg : HasStrictFDerivAt g g' x
⊢ HasStrictFDerivAt (fun x => f x - g x) (f' - g') x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
theorem e0_mul_v_mul_e0 (m : M) : e0 Q * v Q m * e0 Q = v Q m

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ e0 Q * (v Q) m * e0 Q = (v Q) m

Tactic:
rw [← neg_v_mul_e0, ← neg_mul, mul_assoc, e0_mul_e0, mul_neg_one, neg_neg]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem map_eq_comap_of_inverse {f : G →* N} {g : N →* G} (hl : Function.LeftInverse g f)
    (hr : Function.RightInverse g f) (H : Subgroup G) : map f H = comap g H :=
  SetLike.ext' <| by rw [coe_map, coe_comap, Set.image_eq_preimage_of_inverse hl hr]

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
g : N →* G
hl : LeftInverse ⇑g ⇑f
hr : RightInverse ⇑g ⇑f
H : Subgroup G
⊢ ↑(map f H) = ↑(comap g H)

Tactic:
rw [coe_map, coe_comap, Set.image_eq_preimage_of_inverse hl hr]

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransform.lean
lemma fourierIntegral_comp_linearIsometry (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) :
    𝓕 (f ∘ A) w = (𝓕 f) (A w)

Proof state:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
V : Type u_2
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
W : Type u_3
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
A : W ≃ₗᵢ[ℝ] V
f : V → E
w : W
⊢ 𝓕 (f ∘ ⇑A) w = 𝓕 f (A w)

Tactic:
simp only [fourierIntegral_eq, ← A.inner_map_map, Function.comp_apply,
  ← MeasurePreserving.integral_comp A.measurePreserving A.toHomeomorph.measurableEmbedding]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Span.lean
theorem span_pair_add_mul_right {R : Type u} [CommRing R] {x y : R} (z : R) :
    (span {x, y + x * z} : Ideal R) = span {x, y}

Proof state:
R : Type u
inst✝ : CommRing R
x y z : R
⊢ span {x, y + x * z} = span {x, y}

Tactic:
rw [span_pair_comm, span_pair_add_mul_left, span_pair_comm]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean
@[reassoc (attr := simp)]
lemma biprod_inl_snd_f (i : ι) :
    (biprod.inl : K ⟶ K ⊞ L).f i ≫ (biprod.snd : K ⊞ L ⟶ L).f i = 0

Proof state:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ biprod.inl.f i ≫ biprod.snd.f i = 0

Tactic:
rw [← comp_f, biprod.inl_snd, zero_f]

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem singleton_inter_nonempty : ({a} ∩ s).Nonempty ↔ a ∈ s

Proof state:
α : Type u
s : Set α
a : α
⊢ ({a} ∩ s).Nonempty ↔ a ∈ s

Tactic:
simp only [Set.Nonempty, mem_inter_iff, mem_singleton_iff, exists_eq_left]

Result:
no goals
-- Mathlib/Order/BooleanSubalgebra.lean
@[simp, norm_cast] lemma coe_eq_univ : L = (univ : Set α) ↔ L = ⊤

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ ↑L = univ ↔ L = ⊤

Tactic:
rw [← coe_top, coe_inj]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reflect_eq_zero_iff {N : ℕ} {f : R[X]} : reflect N (f : R[X]) = 0 ↔ f = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
N : ℕ
f : R[X]
⊢ reflect N f = 0 ↔ f = 0

Tactic:
rw [ofFinsupp_eq_zero, reflect, embDomain_eq_zero, ofFinsupp_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem distinctKeys_of_sublist [BEq α] {l l' : List ((a : α) × β a)} (h : Sublist l' l) :
    DistinctKeys l → DistinctKeys l' :=
  distinctKeys_of_sublist_keys (by simpa only [keys_eq_map] using h.map _)

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
h : l'.Sublist l
⊢ (keys l').Sublist (keys l)

Tactic:
simpa only [keys_eq_map] using h.map _

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma ZModModule.add_add_add_cancel (x y z : G) : (x + y) + (y + z) = x + z

Proof state:
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x y z : G
⊢ x + y + (y + z) = x + z

Tactic:
simpa [sub_eq_add] using sub_add_sub_cancel x y z

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_flatMap {l : List α} {f : α → List β} :
    (l.flatMap f).any p = l.any fun a => (f a).any p

Proof state:
α : Type u_1
β : Type u_2
p : β → Bool
l : List α
f : α → List β
⊢ (flatMap f l).any p = l.any fun a => (f a).any p

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublists_concat (l : List α) (a : α) :
    sublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)

Proof state:
α : Type u
l : List α
a : α
⊢ (l ++ [a]).sublists = l.sublists ++ map (fun x => x ++ [a]) l.sublists

Tactic:
rw [sublists_append, sublists_singleton, bind_eq_flatMap, flatMap_cons, flatMap_cons, flatMap_nil,
   map_id'' append_nil, append_nil]

Result:
no goals
-- Mathlib/RepresentationTheory/Basic.lean
theorem asGroupHom_apply (g : G) : ↑(asGroupHom ρ g) = ρ g

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
⊢ ↑(ρ.asGroupHom g) = ρ g

Tactic:
simp only [asGroupHom, MonoidHom.coe_toHomUnits]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem dense_closure : Dense (closure s) ↔ Dense s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ Dense (closure s) ↔ Dense s

Tactic:
rw [Dense, Dense, closure_closure]

Result:
no goals
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma disjointSum_isBasis_iff {h I X} :
    (M.disjointSum N h).IsBasis I X ↔ M.IsBasis (I ∩ M.E) (X ∩ M.E) ∧
      N.IsBasis (I ∩ N.E) (X ∩ N.E) ∧ I ⊆ X ∧ X ⊆ M.E ∪ N.E

Proof state:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I X : Set α
⊢ (M.disjointSum N h).IsBasis I X ↔
    M.IsBasis (I ∩ M.E) (X ∩ M.E) ∧ N.IsBasis (I ∩ N.E) (X ∩ N.E) ∧ I ⊆ X ∧ X ⊆ M.E ∪ N.E

Tactic:
simp [disjointSum, and_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem umod_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    (lhs' % rhs') = (lhs % rhs)

Proof state:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs' % rhs' = lhs % rhs

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Algebra/Polynomial/GroupRingAction.lean
theorem prodXSubSMul.smul (x : R) (g : G) : g • prodXSubSMul G R x = prodXSubSMul G R x :=
  letI := Classical.decEq R
  Finset.smul_prod'.trans <|
    Fintype.prod_bijective _ (MulAction.bijective g) _ _ fun g' ↦ by
      rw [ofQuotientStabilizer_smul, smul_sub, Polynomial.smul_X, Polynomial.smul_C]

Proof state:
G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
g : G
this : DecidableEq R := Classical.decEq R
g' : G ⧸ stabilizer G x
⊢ g • (X - C (ofQuotientStabilizer G x g')) = X - C (ofQuotientStabilizer G x (g • g'))

Tactic:
rw [ofQuotientStabilizer_smul, smul_sub, Polynomial.smul_X, Polynomial.smul_C]

Result:
no goals
-- Mathlib/GroupTheory/Archimedean.lean
theorem Int.subgroup_cyclic (H : AddSubgroup ℤ) : ∃ a, H = AddSubgroup.closure {a} :=
  have : Ioo (0 : ℤ) 1 = ∅ := eq_empty_of_forall_not_mem fun _ hm =>
    hm.1.not_le (lt_add_one_iff.1 hm.2)
  AddSubgroup.cyclic_of_isolated_zero one_pos <| by simp [this]

Proof state:
H : AddSubgroup ℤ
this : Ioo 0 1 = ∅
⊢ Disjoint (↑H) (Ioo 0 1)

Tactic:
simp [this]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem nat_mul_iff (hn : n ≠ 0) : LiouvilleWith p (n * x) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
n : ℕ
hn : n ≠ 0
⊢ LiouvilleWith p (↑n * x) ↔ LiouvilleWith p x

Tactic:
rw [mul_comm, mul_nat_iff hn]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem add_zsmul_modEq (z : ℤ) : a + z • p ≡ a [PMOD p] :=
  ⟨-z, by simp⟩

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a : α
z : ℤ
⊢ a - (a + z • p) = -z • p

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
lemma uIcc_map_sectL [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β]
    [DecidableRel (α := α × β) (· ≤ ·)] (a b : α) (c : β) :
    (uIcc a b).map (.sectL _ c) = uIcc (a, c) (b, c)

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
c : β
⊢ map (Embedding.sectL α c) [[a, b]] = [[(a, c), (b, c)]]

Tactic:
aesop (add safe forward [le_antisymm])

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
@[gcongr]
lemma toRight_subset_toRight : u ⊆ v → u.toRight ⊆ v.toRight :=
  fun h _ => by simpa only [mem_toRight] using @h _

Proof state:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
h : u ⊆ v
x✝ : β
⊢ x✝ ∈ u.toRight → x✝ ∈ v.toRight

Tactic:
simpa only [mem_toRight] using @h _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_lt_mul_of_neg_left {a b c : Int} (h : b < a) (hc : c < 0) : c * a < c * b :=
  have : -c > 0 := Int.neg_pos_of_neg hc
  have : -c * b < -c * a := Int.mul_lt_mul_of_pos_left h this
  have : -(c * b) < -(c * a)

Proof state:
a b c : Int
h : b < a
hc : c < 0
this✝ : -c > 0
this : -c * b < -c * a
⊢ -(c * b) < -(c * a)

Tactic:
rwa [← Int.neg_mul_eq_neg_mul, ← Int.neg_mul_eq_neg_mul] at this

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem leadingCoeff_neg (p : R[X]) : (-p).leadingCoeff = -p.leadingCoeff

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).leadingCoeff = -p.leadingCoeff

Tactic:
rw [leadingCoeff, leadingCoeff, natDegree_neg, coeff_neg]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_sub [Ring α] (m n) : ((m - n : ZNum) : α) = m - n

Proof state:
α : Type u_1
inst✝ : Ring α
m n : ZNum
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
simp [sub_eq_neg_add]

Result:
no goals