harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/LeftRight.lean
lemma nhdsWithin_right_sup_nhds_singleton (a : α) :
    𝓝[>] a ⊔ 𝓝[{a}] a = 𝓝[≥] a

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[>] a ⊔ 𝓝[{a}] a = 𝓝[≥] a

Tactic:
simp only [union_singleton, Ioi_insert, ← nhdsWithin_union]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem haarMeasure_eq_iff (K₀ : PositiveCompacts G) (μ : Measure G) [SigmaFinite μ]
    [IsMulLeftInvariant μ] :
    haarMeasure K₀ = μ ↔ μ K₀ = 1 :=
  ⟨fun h => h.symm ▸ haarMeasure_self, fun h => by rw [haarMeasure_unique μ K₀, h, one_smul]⟩

Proof state:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
K₀ : PositiveCompacts G
μ : Measure G
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsMulLeftInvariant
h : μ ↑K₀ = 1
⊢ haarMeasure K₀ = μ

Tactic:
rw [haarMeasure_unique μ K₀, h, one_smul]

Result:
no goals
-- Mathlib/Algebra/Star/Free.lean
theorem star_algebraMap (r : R) : star (algebraMap R (FreeAlgebra R X) r) = algebraMap R _ r

Proof state:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
r : R
⊢ star ((algebraMap R (FreeAlgebra R X)) r) = (algebraMap R (FreeAlgebra R X)) r

Tactic:
simp [star, Star.star]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_nsmul (a : ℝ≥0∞) (n : ℕ) : (n • a).toReal = n • a.toReal

Proof state:
a : ℝ≥0∞
n : ℕ
⊢ (n • a).toReal = n • a.toReal

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem congr_tprod (f : Π i, s i ≃ₗ[R] t i) (m : Π i, s i) :
    congr f (tprod R m) = tprod R (fun (i : ι) ↦ (f i) (m i))

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i ≃ₗ[R] t i
m : (i : ι) → s i
⊢ (congr f) ((tprod R) m) = ⨂ₜ[R] (i : ι), (f i) (m i)

Tactic:
simp only [congr, LinearEquiv.ofLinear_apply, map_tprod, LinearEquiv.coe_coe]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem prod_ne_zero {ι} (f : ι → Cardinal) : prod f ≠ 0 ↔ ∀ i, f i ≠ 0

Proof state:
ι : Type u_1
f : ι → Cardinal.{u_2}
⊢ prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0

Tactic:
simp [prod_eq_zero]

Result:
no goals
-- Mathlib/Topology/UniformSpace/CompactConvergence.lean
theorem tendsto_iff_tendstoUniformly :
    Tendsto F p (𝓝 f) ↔ TendstoUniformly (fun i a => F i a) f p

Proof state:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : CompactSpace α
⊢ Tendsto F p (𝓝 f) ↔ TendstoUniformly (fun i a => (F i) a) (⇑f) p

Tactic:
rw [tendsto_iff_forall_isCompact_tendstoUniformlyOn, ← tendstoUniformlyOn_univ]

Result:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : CompactSpace α
⊢ (∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K) ↔
    TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p univ

Proof state:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : CompactSpace α
⊢ (∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K) ↔
    TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p univ

Tactic:
exact ⟨fun h => h univ isCompact_univ, fun h K _hK => h.mono (subset_univ K)⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_sub_natCast' (hx : 0 ≤ x) (h : y - n ≠ 0) : x ^ (y - n) = x ^ y / x ^ n

Proof state:
x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y - ↑n ≠ 0
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
rw [rpow_sub' hx h, rpow_natCast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eq_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a = b) = b

Proof state:
a b : Prop
h : a = True
⊢ (a = b) = b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem pos_of_neg_neg {a : Int} (h : -a < 0) : 0 < a :=
  Int.lt_of_neg_lt_neg <| by rwa [Int.neg_zero]

Proof state:
a : Int
h : -a < 0
⊢ -a < -0

Tactic:
rwa [Int.neg_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_neg_iff_of_pos_left [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
    a • b < 0 ↔ b < 0

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulZeroClass α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : 0 < a
⊢ a • b < 0 ↔ b < 0

Tactic:
simpa only [smul_zero]  using smul_lt_smul_iff_of_pos_left ha (b₂ := (0 : β))

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem coeff_mul_right_one_sub_of_lt_order (d : σ →₀ ℕ) (h : degree d < g.order) :
    coeff R d ((1 - g) * f) = coeff R d f

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight fun x => 1) d) < g.order
⊢ (coeff R d) ((1 - g) * f) = (coeff R d) f

Tactic:
exact coeff_mul_right_one_sub_of_lt_weightedOrder _ h

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑d.degree < g.order
⊢ (coeff R d) ((1 - g) * f) = (coeff R d) f

Tactic:
rw [degree_eq_weight_one] at h

Result:
σ : Type u_1
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight fun x => 1) d) < g.order
⊢ (coeff R d) ((1 - g) * f) = (coeff R d) f
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_eq_finite_toFinset_prod (f : α → M) {s : Set α} (hs : s.Finite) :
    ∏ᶠ i ∈ s, f i = ∏ i ∈ hs.toFinset, f i :=
  finprod_mem_eq_prod_of_inter_mulSupport_eq _ <| by rw [hs.coe_toFinset]

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : s.Finite
⊢ s ∩ mulSupport f = ↑hs.toFinset ∩ mulSupport f

Tactic:
rw [hs.coe_toFinset]

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem pi_pure [Finite ι] (f : (i : ι) → α i) : pi (pure <| f ·) = pure f

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
f : (i : ι) → α i
⊢ (pi fun x => pure (f x)) = pure f

Tactic:
simp only [← principal_singleton, pi_principal, univ_pi_singleton]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean
theorem unitization_range :
    (unitization s).range = subalgebraOfSubsemiring (.closure s)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
⊢ (unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure ↑s)

Tactic:
have := AddSubmonoidClass.nsmulMemClass (S := S)

Result:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
this : SMulMemClass S ℕ R
⊢ (unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure ↑s)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
this : SMulMemClass S ℕ R
⊢ (unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure ↑s)

Tactic:
rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_nat]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean
lemma shiftFunctorZero_op_inv_app (X : Cᵒᵖ) :
    (shiftFunctorZero Cᵒᵖ ℤ).inv.app X =
      ((shiftFunctorZero C ℤ).hom.app X.unop).op ≫
      (shiftFunctorOpIso C 0 0 (zero_add 0)).inv.app X

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctorZero Cᵒᵖ ℤ).inv.app X =
    ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C 0 0 ⋯).inv.app X

Tactic:
rw [← cancel_epi ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X), Iso.hom_inv_id_app,
  shiftFunctorZero_op_hom_app, assoc, ← op_comp_assoc, Iso.hom_inv_id_app, op_id,
  id_comp, Iso.hom_inv_id_app]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc]
lemma cyclesOpIso_hom_naturality (φ : S₁ ⟶ S₂)
    [S₁.HasRightHomology] [S₂.HasRightHomology] :
    cyclesMap (opMap φ) ≫ (S₁.cyclesOpIso).hom =
      S₂.cyclesOpIso.hom ≫ (opcyclesMap φ).op

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ cyclesMap (opMap φ) ≫ S₁.cyclesOpIso.hom = S₂.cyclesOpIso.hom ≫ (opcyclesMap φ).op

Tactic:
rw [← cancel_mono (S₁.cyclesOpIso).inv, assoc, assoc, Iso.hom_inv_id, comp_id,
  cyclesOpIso_inv_naturality, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem sInter_eq_compl_sUnion_compl (S : Set (Set α)) : ⋂₀ S = (⋃₀ (compl '' S))ᶜ

Proof state:
α : Type u_1
S : Set (Set α)
⊢ ⋂₀ S = (⋃₀ (compl '' S))ᶜ

Tactic:
rw [← compl_compl (⋂₀ S), compl_sInter]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.ι_π_self (f : J → C) [HasBiproduct f] (j : J) :
    biproduct.ι f j ≫ biproduct.π f j = 𝟙 _

Proof state:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : J
⊢ ι f j ≫ π f j = 𝟙 (f j)

Tactic:
simp [biproduct.ι_π]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.smul [Add α] [Monoid γ] [AddGroup β] [DistribMulAction γ β]
    (h : Antiperiodic f c) (a : γ) : Antiperiodic (a • f) c

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝³ : Add α
inst✝² : Monoid γ
inst✝¹ : AddGroup β
inst✝ : DistribMulAction γ β
h : Antiperiodic f c
a : γ
⊢ Antiperiodic (a • f) c

Tactic:
simp_all

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBasis'.inter_eq_of_subset_indep (hI : M.IsBasis' I X) (hIJ : I ⊆ J) (hJ : M.Indep J) :
    J ∩ X = I

Proof state:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
hIJ : I ⊆ J
hJ : M.Indep J
⊢ J ∩ X = I

Tactic:
rw [← hI.isBasis_inter_ground.inter_eq_of_subset_indep hIJ hJ, inter_comm X, ← inter_assoc,
  inter_eq_self_of_subset_left hJ.subset_ground]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem lintegral_eq_tsum_of_ac (h : IsFundamentalDomain G s μ) (hν : ν ≪ μ) (f : α → ℝ≥0∞) :
    ∫⁻ x, f x ∂ν = ∑' g : G, ∫⁻ x in g • s, f x ∂ν

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂ν

Tactic:
rw [← lintegral_sum_measure, h.sum_restrict_of_ac hν]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.not_eq_eq_eq_not {a b : Bool} : ((!a) = b) ↔ (a = !b)

Proof state:
a b : Bool
⊢ (!a) = b ↔ a = !b

Tactic:
cases a <;> cases b <;> simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem darts_reverse {u v : V} (p : G.Walk u v) :
    p.reverse.darts = (p.darts.map Dart.symm).reverse

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.darts = (List.map Dart.symm p.darts).reverse

Tactic:
induction p <;> simp [*, Sym2.eq_swap]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem of_edist_le (h : ∀ x y, edist (f x) (f y) ≤ edist x y) : LipschitzWith 1 f :=
  fun x y => by simp only [ENNReal.coe_one, one_mul, h]

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : ∀ (x y : α), edist (f x) (f y) ≤ edist x y
x y : α
⊢ edist (f x) (f y) ≤ ↑1 * edist x y

Tactic:
simp only [ENNReal.coe_one, one_mul, h]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
@[to_additive] lemma monovary_inv : Monovary f⁻¹ g⁻¹ ↔ Monovary f g

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedCommGroup α
inst✝ : OrderedCommGroup β
f : ι → α
g : ι → β
⊢ Monovary f⁻¹ g⁻¹ ↔ Monovary f g

Tactic:
simp

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
@[simp] lemma num_pow (q : ℚ≥0) (n : ℕ) : (q ^ n).num = q.num ^ n

Proof state:
q : ℚ≥0
n : ℕ
⊢ (q ^ n).num = q.num ^ n

Tactic:
simp [num, Int.natAbs_pow]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem norm_indicatorConstLp_top (hμs_ne_zero : μ s ≠ 0) :
    ‖indicatorConstLp ∞ hs hμs c‖ = ‖c‖

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
hμs_ne_zero : μ s ≠ 0
⊢ ‖indicatorConstLp ⊤ hs hμs c‖ = ‖c‖

Tactic:
rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
  eLpNorm_indicator_const' hs hμs_ne_zero ENNReal.top_ne_zero, ENNReal.top_toReal,
  _root_.div_zero, ENNReal.rpow_zero, mul_one, toReal_enorm]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
@[simp] lemma lineMap_lineMap_right (p₀ p₁ : P1) (c d : k) :
    lineMap p₀ (lineMap p₀ p₁ c) d = lineMap p₀ p₁ (d * c)

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c d : k
⊢ (lineMap p₀ ((lineMap p₀ p₁) c)) d = (lineMap p₀ p₁) (d * c)

Tactic:
simp [lineMap_apply, mul_smul]

Result:
no goals
-- Mathlib/Data/Finset/Preimage.lean
theorem preimage_univ {f : α → β} [Fintype α] [Fintype β] (hf) : preimage univ f hf = univ :=
  Finset.coe_injective (by simp)

Proof state:
α : Type u
β : Type v
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype β
hf : InjOn f (f ⁻¹' ↑univ)
⊢ ↑(univ.preimage f hf) = ↑univ

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem projIci_of_mem (hx : x ∈ Ici a) : projIci a x = ⟨x, hx⟩

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a x : α
hx : x ∈ Ici a
⊢ projIci a x = ⟨x, hx⟩

Tactic:
simpa [projIci]

Result:
no goals
-- Mathlib/NumberTheory/PrimeCounting.lean
theorem primesBelow_card_eq_primeCounting' (n : ℕ) : #n.primesBelow = primeCounting' n

Proof state:
n : ℕ
⊢ #n.primesBelow = π' n

Tactic:
simp only [primesBelow, primeCounting']

Result:
n : ℕ
⊢ #(filter (fun p => Prime p) (range n)) = count Prime n

Proof state:
n : ℕ
⊢ #(filter (fun p => Prime p) (range n)) = count Prime n

Tactic:
exact (count_eq_card_filter_range Prime n).symm

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Shift.lean
lemma deriv_comp_sub_const : deriv (fun x ↦ f (x - a)) x = deriv f (x - a)

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
⊢ deriv (fun x => f (x - a)) x = deriv f (x - a)

Tactic:
simp_rw [sub_eq_add_neg, deriv_comp_add_const]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left
    (hab : IntervalIntegrable f volume a b) (hmeas : StronglyMeasurableAtFilter f la')
    (hf : Tendsto f (la' ⊓ ae volume) (𝓝 c)) (hu : Tendsto u lt la) (hv : Tendsto v lt la) :
    (fun t => ((∫ x in v t..b, f x) - ∫ x in u t..b, f x) + (v t - u t) • c) =o[lt] (v - u)

Proof state:
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℝ → E
c : E
la la' : Filter ℝ
lt : Filter ι
a b : ℝ
u v : ι → ℝ
inst✝ : FTCFilter a la la'
hab : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter f la' volume
hf : Tendsto f (la' ⊓ ae volume) (𝓝 c)
hu : Tendsto u lt la
hv : Tendsto v lt la
⊢ (fun t => ((∫ (x : ℝ) in v t..b, f x) - ∫ (x : ℝ) in u t..b, f x) + (v t - u t) • c) =o[lt] (v - u)

Tactic:
simpa only [integral_const, smul_eq_mul, mul_one] using
  measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left hab hmeas hf hu hv

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem xor_true : Xor' True = Not

Proof state:
⊢ Xor' True = Not

Tactic:
simp (config := { unfoldPartialApp := true }) [Xor']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem toList_pmap {l : Array α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l, P a} :
    (l.pmap f H).toList = l.toList.pmap f (fun a m => H a (mem_def.mpr m))

Proof state:
α : Type u_1
β : Type u_2
l : Array α
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ l → P a
⊢ (pmap f l H).toList = List.pmap f l.toList ⋯

Tactic:
simp [pmap]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem filter_or (s : Finset α) : (s.filter fun a => p a ∨ q a) = s.filter p ∪ s.filter q :=
  ext fun _ => by simp [mem_filter, mem_union, and_or_left]

Proof state:
α : Type u_1
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
x✝ : α
⊢ x✝ ∈ filter (fun a => p a ∨ q a) s ↔ x✝ ∈ filter p s ∪ filter q s

Tactic:
simp [mem_filter, mem_union, and_or_left]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_zsmul_toReal_eq_two_mul {θ : Angle} :
    ((2 : ℤ) • θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)

Proof state:
θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)

Tactic:
rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ToNat.lean
theorem toNat_apply_of_aleph0_le {c : Cardinal} (h : ℵ₀ ≤ c) : toNat c = 0

Proof state:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ toNat c = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_nonsingular (hf : Function.Injective f) (P : Fin 3 → A) :
    (W'.baseChange B).toProjective.Nonsingular (f ∘ P) ↔
      (W'.baseChange A).toProjective.Nonsingular P

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (baseChange W' B).toProjective.Nonsingular (⇑f ∘ P) ↔ (baseChange W' A).toProjective.Nonsingular P

Tactic:
rw [← RingHom.coe_coe, ← map_nonsingular hf, AlgHom.toRingHom_eq_coe, map_baseChange]

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem eq_top_of_isCompl_bot (h : IsCompl x ⊥) : x = ⊤

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
x : α
h : IsCompl x ⊥
⊢ x = ⊤

Tactic:
rw [← sup_bot_eq x, h.sup_eq_top]

Result:
no goals
-- Mathlib/Logic/Embedding/Set.lean
theorem Function.Embedding.sumSet_preimage_inl (h : Disjoint s t) :
    .inl ⁻¹' (Function.Embedding.sumSet h ⁻¹' r) = r ∩ s

Proof state:
α : Type u_1
s t r : Set α
h : Disjoint s t
⊢ Subtype.val '' (Sum.inl ⁻¹' (⇑(sumSet h) ⁻¹' r)) = r ∩ s

Tactic:
simp [Set.ext_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_apply_eq_zero (ht : MeasurableSet t) : μ.restrict s t = 0 ↔ μ (t ∩ s) = 0

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
⊢ (μ.restrict s) t = 0 ↔ μ (t ∩ s) = 0

Tactic:
rw [restrict_apply ht]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_eq_fallback_of_contains_eq_false [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
    m.contains a = false → m.getD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
a : α
fallback : β a
⊢ m.contains a = false → m.getD a fallback = fallback

Tactic:
simp_to_raw using Raw₀.getD_eq_fallback

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toOuterMeasure_apply_inter_support :
    p.toOuterMeasure (s ∩ p.support) = p.toOuterMeasure s

Proof state:
α : Type u_1
p : PMF α
s : Set α
⊢ p.toOuterMeasure (s ∩ p.support) = p.toOuterMeasure s

Tactic:
simp only [toOuterMeasure_apply, PMF.support, Set.indicator_inter_support]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_sub {f : ℕ → ℝ≥0∞} {g : ℕ → ℝ≥0∞} (h₁ : ∑' i, g i ≠ ∞) (h₂ : g ≤ f) :
    ∑' i, (f i - g i) = ∑' i, f i - ∑' i, g i :=
  have : ∀ i, f i - g i + g i = f i := fun i => tsub_add_cancel_of_le (h₂ i)
  ENNReal.eq_sub_of_add_eq h₁ <| by simp only [← ENNReal.tsum_add, this]

Proof state:
f g : ℕ → ℝ≥0∞
h₁ : ∑' (i : ℕ), g i ≠ ⊤
h₂ : g ≤ f
this : ∀ (i : ℕ), f i - g i + g i = f i
⊢ ∑' (i : ℕ), (f i - g i) + ∑' (i : ℕ), g i = ∑' (i : ℕ), f i

Tactic:
simp only [← ENNReal.tsum_add, this]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem one_lt_val_iff (v : Valuation K Γ₀) {x : K} (h : x ≠ 0) : 1 < v x ↔ v x⁻¹ < 1

Proof state:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x ≠ 0
⊢ 1 < v x ↔ v x⁻¹ < 1

Tactic:
simp [inv_lt_one₀ (v.pos_iff.2 h)]

Result:
no goals
-- Mathlib/Order/SuccPred/Archimedean.lean
lemma strictMono_of_lt_succ (hf : ∀ a, ¬ IsMax a → f a < f (succ a)) : StrictMono f

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a < f (succ a)
⊢ StrictMono f

Tactic:
simpa using strictMonoOn_of_lt_succ Set.ordConnected_univ (by simpa using hf)

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a < f (succ a)
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f a < f (succ a)

Tactic:
simpa using hf

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem renameEquiv_refl : renameEquiv R (Equiv.refl σ) = AlgEquiv.refl :=
  AlgEquiv.ext (by simp)

Proof state:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
⊢ ∀ (a : MvPolynomial σ R), (renameEquiv R (Equiv.refl σ)) a = AlgEquiv.refl a

Tactic:
simp

Result:
no goals
-- Mathlib/Control/Applicative.lean
theorem seq_assoc (x : Comp F G α) (f : Comp F G (α → β)) (g : Comp F G (β → γ)) :
    g <*> (f <*> x) = @Function.comp α β γ <$> g <*> f <*> x :=
  Comp.ext <| by simp [comp_def, functor_norm]

Proof state:
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
x : Comp F G α
f : Comp F G (α → β)
g : Comp F G (β → γ)
⊢ (g <*> (f <*> x)).run = (Function.comp <$> g <*> f <*> x).run

Tactic:
simp [comp_def, functor_norm]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
lemma map_tails {β : Type*} (g : α → β) : (l.map g).tails = l.tails.map (map g)

Proof state:
α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g l).tails = map (map g) l.tails

Tactic:
induction' l using reverseRecOn <;> simp [*]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
lemma disjoint_iff_forall_ne : Disjoint s t ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ t → a ≠ b

Proof state:
α : Type u
s t : Set α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b

Tactic:
simp only [Ne, disjoint_left, @imp_not_comm _ (_ = _), forall_eq']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem and_and_and_comm : (a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d

Proof state:
a b c d : Prop
⊢ (a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d

Tactic:
rw [← and_assoc, @and_right_comm a, and_assoc]

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

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a \ b = ￢b \ a

Tactic:
simp_rw [← top_sdiff', sdiff_right_comm]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem continuousAt_iff'_right [TopologicalSpace β] {f : β → α} {b : β} :
    ContinuousAt f b ↔ Tendsto (fun x => (f b, f x)) (𝓝 b) (𝓤 α)

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ Tendsto (fun x => (f b, f x)) (𝓝 b) (𝓤 α)

Tactic:
rw [ContinuousAt, tendsto_nhds_right]

Result:
no goals