harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_sInf_eq_sInf_restrict {m0 : MeasurableSpace α} {m : Set (Measure α)}
    (hm : m.Nonempty) (ht : MeasurableSet t) :
    (sInf m).restrict t = sInf ((fun μ : Measure α => μ.restrict t) '' m)

Proof state:
α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
⊢ (sInf m).restrict t = sInf ((fun μ => μ.restrict t) '' m)

Tactic:
ext1 s hs

Result:
case h
α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
⊢ ((sInf m).restrict t) s = (sInf ((fun μ => μ.restrict t) '' m)) s

Proof state:
case h
α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
⊢ ((sInf m).restrict t) s = (sInf ((fun μ => μ.restrict t) '' m)) s

Tactic:
simp_rw [sInf_apply hs, restrict_apply hs, sInf_apply (MeasurableSet.inter hs ht),
  Set.image_image, restrict_toOuterMeasure_eq_toOuterMeasure_restrict ht, ←
  Set.image_image _ toOuterMeasure, ← OuterMeasure.restrict_sInf_eq_sInf_restrict _ (hm.image _),
  OuterMeasure.restrict_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean
lemma projectiveFamilyContent_congr (hP : IsProjectiveMeasureFamily P) (s : Set (Π i, α i))
    (hs_eq : s = cylinder I S) (hS : MeasurableSet S) :
    projectiveFamilyContent hP s = P I S

Proof state:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
hP : IsProjectiveMeasureFamily P
s : Set ((i : ι) → α i)
hs_eq : s = cylinder I S
hS : MeasurableSet S
⊢ (projectiveFamilyContent hP) s = (P I) S

Tactic:
rw [projectiveFamilyContent_eq,
  projectiveFamilyFun_congr hP ((mem_measurableCylinders s).mpr ⟨I, S, hS, hs_eq⟩) hs_eq hS]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
lemma sup'_univ_eq_ciSup (f : ι → α) : univ.sup' univ_nonempty f = ⨆ i, f i

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
f : ι → α
⊢ univ.sup' ⋯ f = ⨆ i, f i

Tactic:
simp [sup'_eq_csSup_image, iSup]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem tendsto_ae_unique {ι : Type*} [T2Space β]
    {g h : α → β} {f : ι → α → β} {l : Filter ι} [l.NeBot]
    (hg : ∀ᵐ ω ∂μ, Tendsto (fun i => f i ω) l (𝓝 (g ω)))
    (hh : ∀ᵐ ω ∂μ, Tendsto (fun i => f i ω) l (𝓝 (h ω))) : g =ᵐ[μ] h

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
ι : Type u_5
inst✝¹ : T2Space β
g h : α → β
f : ι → α → β
l : Filter ι
inst✝ : l.NeBot
hg : ∀ᵐ (ω : α) ∂μ, Tendsto (fun i => f i ω) l (𝓝 (g ω))
hh : ∀ᵐ (ω : α) ∂μ, Tendsto (fun i => f i ω) l (𝓝 (h ω))
⊢ g =ᶠ[ae μ] h

Tactic:
filter_upwards [hg, hh] with ω hg1 hh1 using tendsto_nhds_unique hg1 hh1

Result:
no goals
-- Mathlib/Tactic/Positivity/Basic.lean
private lemma ite_ne_zero (ha : a ≠ 0) (hb : b ≠ 0) : ite p a b ≠ 0

Proof state:
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ (if p then a else b) ≠ 0

Tactic:
by_cases p <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem add_sub_div_two_lt (h : a < b) : a + (b - a) / 2 < b

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
h : a < b
⊢ a + (b - a) / 2 < b

Tactic:
rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ←
  lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two,
  div_lt_div_iff_of_pos_right (zero_lt_two' α)]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma lt_div_comm₀ (ha : 0 < a) (hc : 0 < c) : a < b / c ↔ c < b / a

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
this : MulPosStrictMono G₀
⊢ a < b / c ↔ c < b / a

Tactic:
rw [lt_div_iff₀ ha, lt_div_iff₀' hc]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
⊢ a < b / c ↔ c < b / a

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›

Result:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
this : MulPosStrictMono G₀
⊢ a < b / c ↔ c < b / a
-- Mathlib/Algebra/Group/Subsemigroup/Operations.lean
theorem map_srange (g : N →ₙ* P) (f : M →ₙ* N) : f.srange.map g = (g.comp f).srange

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
g : N →ₙ* P
f : M →ₙ* N
⊢ map g f.srange = (g.comp f).srange

Tactic:
simpa only [srange_eq_map] using (⊤ : Subsemigroup M).map_map g f

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Decomposition.lean
/-- To check equality of natural transformations `F ⟶ G`, it suffices to check it on
Galois objects. -/
lemma natTrans_ext_of_isGalois {G : C ⥤ FintypeCat.{w}} {t s : F ⟶ G}
    (h : ∀ (X : C) [IsGalois X], t.app X = s.app X) :
    t = s

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [inst : IsGalois X], t.app X = s.app X
⊢ t = s

Tactic:
ext X x

Result:
case w.h.h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [inst : IsGalois X], t.app X = s.app X
X : C
x : (F.obj X).carrier
⊢ t.app X x = s.app X x

Proof state:
case w.h.h.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [inst : IsGalois X], t.app X = s.app X
X A : C
f : A ⟶ X
a : (F.obj A).carrier
left✝ : IsGalois A
⊢ t.app X (F.map f a) = s.app X (F.map f a)

Tactic:
rw [FunctorToFintypeCat.naturality, FunctorToFintypeCat.naturality, h A]

Result:
no goals

Proof state:
case w.h.h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [inst : IsGalois X], t.app X = s.app X
X : C
x : (F.obj X).carrier
⊢ t.app X x = s.app X x

Tactic:
obtain ⟨A, f, a, _, rfl⟩ := exists_hom_from_galois_of_fiber F X x

Result:
case w.h.h.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [inst : IsGalois X], t.app X = s.app X
X A : C
f : A ⟶ X
a : (F.obj A).carrier
left✝ : IsGalois A
⊢ t.app X (F.map f a) = s.app X (F.map f a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_add_one (x y : Nat) : gcd (x + 1) y = gcd (y % (x + 1)) (x + 1)

Proof state:
x y : Nat
⊢ (x + 1).gcd y = (y % (x + 1)).gcd (x + 1)

Tactic:
rw [gcd]

Result:
x y : Nat
⊢ (if x + 1 = 0 then y else (y % (x + 1)).gcd (x + 1)) = (y % (x + 1)).gcd (x + 1)

Proof state:
x y : Nat
⊢ (if x + 1 = 0 then y else (y % (x + 1)).gcd (x + 1)) = (y % (x + 1)).gcd (x + 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/WellPowered.lean
theorem wellPowered_of_equiv (e : C ≌ D) [LocallySmall.{w} C] [LocallySmall.{w} D]
    [WellPowered.{w} C] : WellPowered.{w} D :=
  wellPowered_of_essentiallySmall_monoOver fun X =>
    (essentiallySmall_congr (MonoOver.congr X e.symm)).2 <| by infer_instance

Proof state:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
e : C ≌ D
inst✝² : LocallySmall.{w, v, u₁} C
inst✝¹ : LocallySmall.{w, v₂, u₂} D
inst✝ : WellPowered.{w, v, u₁} C
X : D
⊢ EssentiallySmall.{w, v, max u₁ v} (MonoOver (e.symm.functor.obj X))

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem foldl_attach (l : Vector α n) (f : β → α → β) (b : β) :
    l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b

Proof state:
case mk
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l : Array α
⊢ foldl (fun acc t => f acc t.val) b { toArray := l, size_toArray := ⋯ }.attach =
    foldl f b { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.foldl_attach]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : β → α → β
b : β
⊢ foldl (fun acc t => f acc t.val) b l.attach = foldl f b l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l : Array α
⊢ foldl (fun acc t => f acc t.val) b { toArray := l, size_toArray := ⋯ }.attach =
    foldl f b { toArray := l, size_toArray := ⋯ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/UInt/Bitwise.lean
theorem Bool.toBitVec_toUInt8 {b : Bool} :
    b.toUInt8.toBitVec = (BitVec.ofBool b).setWidth 8

Proof state:
b : Bool
⊢ b.toUInt8.toBitVec = BitVec.setWidth 8 (BitVec.ofBool b)

Tactic:
cases b <;> simp [toUInt8]

Result:
no goals
-- Mathlib/GroupTheory/Torsion.lean
theorem IsTorsionFree.subgroup (tG : IsTorsionFree G) (H : Subgroup G) : IsTorsionFree H :=
  fun h hne ↦ Submonoid.isOfFinOrder_coe.not.1 <| tG h <| by norm_cast

Proof state:
G : Type u_1
inst✝ : Group G
tG : IsTorsionFree G
H : Subgroup G
h : ↥H
hne : h ≠ 1
⊢ ↑h ≠ 1

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem preimage_coe_Ico_top : (some : α → WithTop α) ⁻¹' Ico a ⊤ = Ici a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some ⁻¹' Ico ↑a ⊤ = Ici a

Tactic:
simp [← Ici_inter_Iio]

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp) card_mul_subConst]
lemma card_mul_divConst (A B : Finset G) : #A * δₘ[A, B] = #(A / B)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ ↑(#A) * δₘ[A, B] = ↑(#(A / B))

Tactic:
rw [mul_comm, divConst_mul_card]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.coeff_zero (hf : HasFPowerSeriesOnBall f pf x r)
    (v : Fin 0 → E) : pf 0 v = f x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf univ x r
v : Fin 0 → E
⊢ (pf 0) v = f x

Tactic:
exact hf.coeff_zero v

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
v : Fin 0 → E
⊢ (pf 0) v = f x

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf univ x r
v : Fin 0 → E
⊢ (pf 0) v = f x
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma add_of_X_ne {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ≠ Q x * P z) : W.add P Q = W.addZ P Q •
      ![W.toAffine.addX (P x / P z) (Q x / Q z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)), 1]

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ W.add P Q =
    W.addZ P Q •
      ![(toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
          ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]

Tactic:
rw [add, if_neg <| not_equiv_of_X_ne hx, addXYZ_of_Z_ne_zero hP hQ hPz hQz hx]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsRestriction.of_subset {R' : Set α} (M : Matroid α) (h : R ⊆ R') :
    (M ↾ R) ≤r (M ↾ R')

Proof state:
α : Type u_1
R R' : Set α
M : Matroid α
h : R ⊆ R'
⊢ M ↾ R' ↾ R ≤r M ↾ R'

Tactic:
exact restrict_isRestriction _ _ h

Result:
no goals

Proof state:
α : Type u_1
R R' : Set α
M : Matroid α
h : R ⊆ R'
⊢ M ↾ R ≤r M ↾ R'

Tactic:
rw [← restrict_restrict_eq M h]

Result:
α : Type u_1
R R' : Set α
M : Matroid α
h : R ⊆ R'
⊢ M ↾ R' ↾ R ≤r M ↾ R'
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
theorem natDegree_scaleRoots (p : R[X]) (s : R) : natDegree (scaleRoots p s) = natDegree p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).natDegree = p.natDegree

Tactic:
simp only [natDegree, degree_scaleRoots]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem insertNth_apply_below {i j : Fin (n + 1)} (h : j < i) (x : α i)
    (p : ∀ k, α (i.succAbove k)) :
    i.insertNth x p j = @Eq.recOn _ _ (fun x _ ↦ α x) _
    (succAbove_castPred_of_lt _ _ h) (p <| j.castPred _)

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : j < i
x : α i
p : (k : Fin n) → α (i.succAbove k)
⊢ i.insertNth x p j = Eq.recOn ⋯ (p (j.castPred ⋯))

Tactic:
rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_lt h), dif_pos h]

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem toList_ne_nil {i j} (w : NeWord M i j) : w.toList ≠ List.nil

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
⊢ w.toList ≠ []

Tactic:
induction w

Result:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).toList ≠ []

case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : _w₁✝.toList ≠ []
_w₂_ih✝ : _w₂✝.toList ≠ []
⊢ (_w₁✝.append _hne✝ _w₂✝).toList ≠ []

Proof state:
case append.h
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : _w₁✝.toList ≠ []
_w₂_ih✝ : _w₂✝.toList ≠ []
⊢ _w₁✝.toList ≠ []

Tactic:
assumption

Result:
no goals

Proof state:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : _w₁✝.toList ≠ []
_w₂_ih✝ : _w₂✝.toList ≠ []
⊢ (_w₁✝.append _hne✝ _w₂✝).toList ≠ []

Tactic:
apply List.append_ne_nil_of_left_ne_nil

Result:
case append.h
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : _w₁✝.toList ≠ []
_w₂_ih✝ : _w₂✝.toList ≠ []
⊢ _w₁✝.toList ≠ []

Proof state:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).toList ≠ []

Tactic:
rintro ⟨rfl⟩

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem lintegral_swapLeft (κ : Kernel (α × β) γ) (a : β × α) (g : γ → ℝ≥0∞) :
    ∫⁻ c, g c ∂swapLeft κ a = ∫⁻ c, g c ∂κ a.swap

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
a : β × α
g : γ → ℝ≥0∞
⊢ ∫⁻ (c : γ), g c ∂κ.swapLeft a = ∫⁻ (c : γ), g c ∂κ a.swap

Tactic:
rw [swapLeft_apply]

Result:
no goals
-- Mathlib/GroupTheory/GroupExtension/Basic.lean
theorem mul_inv_mem_range_inl : σ g * (σ' g)⁻¹ ∈ S.inl.range

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
⊢ σ g * (σ' g)⁻¹ ∈ S.inl.range

Tactic:
simp only [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, rightHom_section,
  mul_inv_cancel]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_eq_iff {l : BitVec w} {n : Nat} {h : n < w} : l[n] = x ↔ l[n]? = some x

Proof state:
w : Nat
x : Bool
l : BitVec w
n : Nat
h : n < w
⊢ l[n] = x ↔ l[n]? = some x

Tactic:
simp only [getElem?_eq_some]

Result:
w : Nat
x : Bool
l : BitVec w
n : Nat
h : n < w
⊢ l[n] = x ↔ ∃ h, l[n] = x

Proof state:
w : Nat
x : Bool
l : BitVec w
n : Nat
h : n < w
⊢ l[n] = x ↔ ∃ h, l[n] = x

Tactic:
exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩

Result:
no goals
-- Mathlib/Algebra/Ring/Invertible.lean
theorem invOf_two_add_invOf_two [NonAssocSemiring α] [Invertible (2 : α)] :
    (⅟ 2 : α) + (⅟ 2 : α) = 1

Proof state:
α : Type u
inst✝¹ : NonAssocSemiring α
inst✝ : Invertible 2
⊢ ⅟2 + ⅟2 = 1

Tactic:
rw [← two_mul, mul_invOf_self]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/ZMod.lean
@[simp] lemma completedLFunction_zero (s : ℂ) : completedLFunction (0 : ZMod N → ℂ) s = 0

Proof state:
N : ℕ
inst✝ : NeZero N
s : ℂ
⊢ completedLFunction 0 s = 0

Tactic:
simp only [completedLFunction, Pi.zero_apply, zero_mul, sum_const_zero, mul_zero, zero_add]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem isLUB_hasProd (h : ∀ i, 1 ≤ f i) (hf : HasProd f a) :
    IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
h : ∀ (i : ι), 1 ≤ f i
hf : HasProd f a
⊢ IsLUB (Set.range fun s => ∏ i ∈ s, f i) a

Tactic:
classical
exact isLUB_of_tendsto_atTop (Finset.prod_mono_set_of_one_le' h) hf

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
h : ∀ (i : ι), 1 ≤ f i
hf : HasProd f a
⊢ IsLUB (Set.range fun s => ∏ i ∈ s, f i) a

Tactic:
exact isLUB_of_tendsto_atTop (Finset.prod_mono_set_of_one_le' h) hf

Result:
no goals
-- Mathlib/Data/Nat/Count.lean
theorem count_succ_eq_succ_count_iff {n : ℕ} : count p (n + 1) = count p n + 1 ↔ p n

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n + 1 ↔ p n

Tactic:
by_cases h : p n <;> simp [h, count_succ]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_norm_sq_eq_of_L2 (x : WithLp 2 (α × β)) : ‖x‖ ^ 2 = ‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
this : ‖x‖₊ ^ 2 = ‖x.1‖₊ ^ 2 + ‖x.2‖₊ ^ 2
⊢ ‖x‖ ^ 2 = ‖x.1‖ ^ 2 + ‖x.2‖ ^ 2

Tactic:
simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ ‖x‖₊ ^ 2 = ‖x.1‖₊ ^ 2 + ‖x.2‖₊ ^ 2

Tactic:
rw [prod_nnnorm_eq_of_L2, NNReal.sq_sqrt]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ ‖x‖ ^ 2 = ‖x.1‖ ^ 2 + ‖x.2‖ ^ 2

Tactic:
suffices ‖x‖₊ ^ 2 = ‖x.fst‖₊ ^ 2 + ‖x.snd‖₊ ^ 2 by
  simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ ‖x‖₊ ^ 2 = ‖x.1‖₊ ^ 2 + ‖x.2‖₊ ^ 2
-- Mathlib/Order/Monotone/Odd.lean
theorem strictMono_of_odd_strictMonoOn_nonneg {f : G → H} (h₁ : ∀ x, f (-x) = -f x)
    (h₂ : StrictMonoOn f (Ici 0)) : StrictMono f

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
⊢ StrictMono f

Tactic:
refine StrictMonoOn.Iic_union_Ici (fun x hx y hy hxy => neg_lt_neg_iff.1 ?_) h₂

Result:
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x < y
⊢ -f y < -f x

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x < y
⊢ -f y < -f x

Tactic:
rw [← h₁, ← h₁]

Result:
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x < y
⊢ f (-y) < f (-x)

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x < y
⊢ f (-y) < f (-x)

Tactic:
exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_lt_neg hxy)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_zero {w : Nat} : (0#w).toInt = 0

Proof state:
w : Nat
⊢ (0#w).toInt = 0

Tactic:
simp [BitVec.toInt, show 0 < 2^w by exact Nat.two_pow_pos w]

Result:
no goals

Proof state:
w : Nat
⊢ 0 < 2 ^ w

Tactic:
exact Nat.two_pow_pos w

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
@[simp] lemma map_id (H : G.Subgraph) : H.map Hom.id = H

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ Subgraph.map Hom.id H = H

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem extractLsb'_xor {x y : BitVec w} {start len : Nat} :
   (x ^^^ y).extractLsb' start len = (x.extractLsb' start len) ^^^ (y.extractLsb' start len)

Proof state:
case pred
w : Nat
x y : BitVec w
start len i : Nat
hi : i < len
⊢ (extractLsb' start len (x ^^^ y)).getLsbD i = (extractLsb' start len x ^^^ extractLsb' start len y).getLsbD i

Tactic:
simp [hi]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
start len : Nat
⊢ extractLsb' start len (x ^^^ y) = extractLsb' start len x ^^^ extractLsb' start len y

Tactic:
ext i hi

Result:
case pred
w : Nat
x y : BitVec w
start len i : Nat
hi : i < len
⊢ (extractLsb' start len (x ^^^ y)).getLsbD i = (extractLsb' start len x ^^^ extractLsb' start len y).getLsbD i