harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem tendsto_atTop : Tendsto f atTop atTop :=
  tendsto_atTop_mono f.le_map_of_map_zero <| tendsto_atTop_add_const_left _ _ <|
    (tendsto_atTop_mono fun x => (sub_one_lt_floor x).le) <| by
      simpa [sub_eq_add_neg] using tendsto_atTop_add_const_right _ _ tendsto_id

Proof state:
f : CircleDeg1Lift
⊢ Tendsto (fun x => x - 1) atTop atTop

Tactic:
simpa [sub_eq_add_neg] using tendsto_atTop_add_const_right _ _ tendsto_id

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.neg [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) :
    Antiperiodic f (-c)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
⊢ Antiperiodic f (-c)

Tactic:
simpa only [sub_eq_add_neg, Antiperiodic] using h.sub_eq

Result:
no goals
-- Mathlib/Data/Holor.lean
theorem mul_scalar_mul [Monoid α] (x : Holor α []) (y : Holor α ds) :
    x ⊗ y = x ⟨[], Forall₂.nil⟩ • y

Proof state:
α : Type
ds : List ℕ
inst✝ : Monoid α
x : Holor α []
y : Holor α ds
⊢ x ⊗ y = x ⟨[], ⋯⟩ • y

Tactic:
simp (config := { unfoldPartialApp := true }) [mul, SMul.smul, HolorIndex.take, HolorIndex.drop,
  HSMul.hSMul]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
@[reassoc (attr := simp)]
lemma rotateHomotopyEquiv_comm₂ :
    (HomotopyCategory.quotient _ _ ).map (triangle φ).mor₃ ≫
      (HomotopyCategory.quotient _ _ ).map (rotateHomotopyEquiv φ).hom =
      (HomotopyCategory.quotient _ _ ).map (inr (inr φ))

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ).mor₃ ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (rotateHomotopyEquiv φ).hom =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (inr φ))

Tactic:
simpa only [Functor.map_comp]
  using HomotopyCategory.eq_of_homotopy _ _  (rotateHomotopyEquivComm₂Homotopy φ)

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem insert_mem_nhdsWithin_insert {a : α} {s t : Set α} (h : t ∈ 𝓝[s] a) :
    insert a t ∈ 𝓝[insert a s] a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝[s] a
⊢ insert a t ∈ 𝓝[insert a s] a

Tactic:
simp [mem_of_superset h]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean
lemma opEquiv'_zero_add_symm (a : ℤ) (f : Opposite.op (Y⟦a⟧) ⟶ (Opposite.op X)⟦(0 : ℤ)⟧) :
    (opEquiv' 0 a a (zero_add a)).symm f =
      ((shiftFunctorZero Cᵒᵖ ℤ).hom.app _).unop ≫ f.unop

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ 0).obj (Opposite.op X)
⊢ (opEquiv' 0 a a ⋯).symm f = ((shiftFunctorZero Cᵒᵖ ℤ).hom.app (Opposite.op X)).unop ≫ f.unop

Tactic:
simp [opEquiv'_symm_apply, opEquiv_symm_apply, shiftFunctorAdd'_add_zero,
  opShiftFunctorEquivalence_zero_unitIso_inv_app]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_ofList_of_mem [LawfulBEq α]
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    get? (ofList l) k' = some v

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : LawfulBEq α
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
⊢ get? (ofList l) k' = some v

Tactic:
simp_to_raw using Raw₀.Const.get?_insertMany_empty_list_of_mem

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
lemma disjoint_singleton : Disjoint ({a} : Set α) {b} ↔ a ≠ b

Proof state:
α : Type u
a b : α
⊢ Disjoint {a} {b} ↔ a ≠ b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finite/Prod.lean
theorem Finite.toFinset_offDiag {s : Set α} [DecidableEq α] (hs : s.Finite) :
    hs.offDiag.toFinset = hs.toFinset.offDiag :=
  Finset.ext <| by simp

Proof state:
α : Type u_1
s : Set α
inst✝ : DecidableEq α
hs : s.Finite
⊢ ∀ (a : α × α), a ∈ ⋯.toFinset ↔ a ∈ hs.toFinset.offDiag

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
    (m.insertIfNew k v).1.size = if m.contains k then m.1.size else m.1.size + 1

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
v : β k
⊢ (m.insertIfNew k v).val.size = if m.contains k = true then m.val.size else m.val.size + 1

Tactic:
simp_to_model [insertIfNew] using List.length_insertEntryIfNew

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem filterMap_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF)
    {f : (a : α) → β a → Option (δ a)} : m.filterMap f =
      Raw₀.filterMap f ⟨m, h.size_buckets_pos⟩

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
f : (a : α) → β a → Option (δ a)
⊢ Raw.filterMap f m = (Raw₀.filterMap f ⟨m, ⋯⟩).val

Tactic:
simp [Raw.filterMap, h.size_buckets_pos]

Result:
no goals
-- Mathlib/CategoryTheory/Types.lean
theorem homOfElement_eq_iff {X : Type u} (x y : X) : homOfElement x = homOfElement y ↔ x = y :=
  ⟨fun H => congr_fun H PUnit.unit, by aesop⟩

Proof state:
X : Type u
x y : X
⊢ x = y → homOfElement x = homOfElement y

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mkArray_succ : mkArray (n + 1) a = (mkArray n a).push a

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ mkArray (n + 1) a = (mkArray n a).push a

Tactic:
apply toList_inj.1

Result:
n : Nat
α✝ : Type u_1
a : α✝
⊢ (mkArray (n + 1) a).toList = ((mkArray n a).push a).toList

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ (mkArray (n + 1) a).toList = ((mkArray n a).push a).toList

Tactic:
simp [List.replicate_succ']

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem truncateFun_out (x : TruncatedWittVector p n R) : x.out.truncateFun n = x

Proof state:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : TruncatedWittVector p n R
⊢ WittVector.truncateFun n x.out = x

Tactic:
simp only [WittVector.truncateFun, coeff_out, mk_coeff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.false_or (b : Bool) : (false || b) = b

Proof state:
b : Bool
⊢ (false || b) = b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem not_indep_iff (hX : X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ¬M.Indep X ↔ M.Dep X

Tactic:
rw [Dep, and_iff_left hX]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_eq_top [RingHomSurjective τ₁₂] {f : F} :
    range f = ⊤ ↔ Surjective f

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : F
⊢ range f = ⊤ ↔ Surjective ⇑f

Tactic:
rw [SetLike.ext'_iff, range_coe, top_coe, Set.range_eq_univ]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem lt_omega_iff_card_lt {x o : Ordinal} : x < ω_ o ↔ x.card < ℵ_ o

Proof state:
x o : Ordinal.{u_1}
⊢ x < ω_ o ↔ x.card < ℵ_ o

Tactic:
rw [← (isInitial_omega o).card_lt_card, card_omega]

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

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

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem leadingCoeff_mul [IsDomain R] {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : g ≠ 0) :
    m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
rw [leadingCoeff, degree_mul hf hg, ← coeff_mul_of_degree_add]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_fintype [MeasurableSingletonClass α] [Fintype α] (f : α → E)
    (hf : Integrable f μ) :
    ∫ x, f x ∂μ = ∑ x, (μ {x}).toReal • f x

Proof state:
case hf
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝² : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Fintype α
f : α → E
hf : Integrable f μ
⊢ IntegrableOn f (↑Finset.univ) μ

Tactic:
simp [Finset.coe_univ, Measure.restrict_univ, hf]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝² : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Fintype α
f : α → E
hf : Integrable f μ
⊢ ∫ (x : α), f x ∂μ = ∑ x : α, (μ {x}).toReal • f x

Tactic:
rw [← integral_finset .univ, Finset.coe_univ, Measure.restrict_univ]

Result:
case hf
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝² : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Fintype α
f : α → E
hf : Integrable f μ
⊢ IntegrableOn f (↑Finset.univ) μ
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sub_self (a : Ordinal) : a - a = 0

Proof state:
a : Ordinal.{u_4}
⊢ a - a = 0

Tactic:
simpa only [add_zero] using add_sub_cancel a 0

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
lemma isIso_p (hf : S.f = 0) : IsIso h.p :=
  ⟨h.descQ (𝟙 S.X₂) (by rw [hf, comp_id]), p_descQ _ _ _, by
    simp only [← cancel_epi h.p, p_descQ_assoc, id_comp, comp_id]⟩

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hf : S.f = 0
⊢ h.descQ (𝟙 S.X₂) ⋯ ≫ h.p = 𝟙 h.Q

Tactic:
simp only [← cancel_epi h.p, p_descQ_assoc, id_comp, comp_id]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hf : S.f = 0
⊢ S.f ≫ 𝟙 S.X₂ = 0

Tactic:
rw [hf, comp_id]

Result:
no goals
-- Mathlib/Algebra/Ring/Equiv.lean
theorem coe_nonUnitalRingHom_inj_iff {R S : Type*} [NonUnitalNonAssocSemiring R]
    [NonUnitalNonAssocSemiring S] (f g : R ≃+* S) : f = g ↔ (f : R →ₙ+* S) = g :=
  ⟨fun h => by rw [h], fun h => ext <| NonUnitalRingHom.ext_iff.mp h⟩

Proof state:
R : Type u_7
S : Type u_8
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R ≃+* S
h : f = g
⊢ ↑f = ↑g

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Data/Vector/Mem.lean
theorem mem_succ_iff (v : Vector α (n + 1)) : a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList

Tactic:
obtain ⟨a', v', h⟩ := exists_eq_cons v

Result:
case intro.intro
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
a' : α
v' : Vector α n
h : v = a' ::ᵥ v'
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList

Proof state:
case intro.intro
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
a' : α
v' : Vector α n
h : v = a' ::ᵥ v'
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList

Tactic:
simp_rw [h, Vector.mem_cons_iff, Vector.head_cons, Vector.tail_cons]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma preimage_coe_Ioc_bot (y : ℝ) : Real.toEReal ⁻¹' Ioc ⊥ y = Iic y

Proof state:
y : ℝ
⊢ Real.toEReal ⁻¹' Ioc ⊥ ↑y = Iic y

Tactic:
rw [← Ioi_inter_Iic]

Result:
y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iic ↑y) = Iic y

Proof state:
y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iic ↑y) = Iic y

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem natDegree_toSubring : (toSubring p T hp).natDegree = p.natDegree

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).natDegree = p.natDegree

Tactic:
simp [natDegree]

Result:
no goals
-- Mathlib/Order/Hom/CompleteLattice.lean
theorem cancel_left {g : CompleteLatticeHom β γ} {f₁ f₂ : CompleteLatticeHom α β}
    (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
g : CompleteLatticeHom β γ
f₁ f₂ : CompleteLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem Cofork.ofCocone_ι {F : WalkingParallelPair ⥤ C} (t : Cocone F) (j) :
    (Cofork.ofCocone t).ι.app j = eqToHom (by simp) ≫ t.ι.app j := rfl

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
j : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj j = F.obj j

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
/-- A small set of pre-games is bounded below. -/
lemma bddBelow_of_small (s : Set PGame.{u}) [Small.{u} s] : BddBelow s

Proof state:
s : Set PGame
inst✝ : Small.{u, u + 1} ↑s
⊢ BddBelow s

Tactic:
simpa using bddBelow_range_of_small (Subtype.val : s → PGame.{u})

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_eq_getMsbD_zero (x : BitVec w) : x.msb = x.getMsbD 0

Proof state:
w : Nat
x : BitVec w
⊢ x.msb = x.getMsbD 0

Tactic:
cases w <;> simp [getMsbD_eq_getLsbD, msb_eq_getLsbD_last]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
lemma condition : f ≫ inl f g = g ≫ inr f g

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
⊢ f ≫ inl f g = g ≫ inr f g

Tactic:
ext x

Result:
case h
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x : S
⊢ (f ≫ inl f g) x = (g ≫ inr f g) x

Proof state:
case h
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x : S
⊢ (f ≫ inl f g) x = (g ≫ inr f g) x

Tactic:
exact Quot.sound (Rel.inl_inr x)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_intCast_mul (x : ℝ≥0∞) (n : ℤ) (z : ℝ) : x ^ (n * z) = (x ^ n) ^ z

Proof state:
x : ℝ≥0∞
n : ℤ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
rw [rpow_mul, rpow_intCast]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_iSup_le {ι} {f : ι → Ordinal} (H : ∀ i, f i < iSup f) :
    cof (iSup f) ≤ #ι

Proof state:
ι : Type u_1
f : ι → Ordinal.{u_1}
H : ∀ (i : ι), f i < iSup f
⊢ (iSup f).cof ≤ Cardinal.lift.{u_1, u_1} #ι

Tactic:
exact cof_iSup_le_lift H

Result:
no goals

Proof state:
ι : Type u_1
f : ι → Ordinal.{u_1}
H : ∀ (i : ι), f i < iSup f
⊢ (iSup f).cof ≤ #ι

Tactic:
rw [← (#ι).lift_id]

Result:
ι : Type u_1
f : ι → Ordinal.{u_1}
H : ∀ (i : ι), f i < iSup f
⊢ (iSup f).cof ≤ Cardinal.lift.{u_1, u_1} #ι
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem mem_ker_map (h : IsAdjoinRoot S f) {p} : p ∈ RingHom.ker h.map ↔ f ∣ p

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRoot S f
p : R[X]
⊢ p ∈ RingHom.ker h.map ↔ f ∣ p

Tactic:
rw [h.ker_map, Ideal.mem_span_singleton]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/InclusionExclusion.lean
theorem inclusion_exclusion_card_inf_compl (s : Finset ι) (S : ι → Finset α) :
    #(s.inf fun i ↦ (S i)ᶜ) = ∑ t ∈ s.powerset, (-1 : ℤ) ^ #t * #(t.inf S)

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
⊢ ↑(#(s.inf fun i => (S i)ᶜ)) = ∑ t ∈ s.powerset, (-1) ^ #t * ↑(#(t.inf S))

Tactic:
simpa using inclusion_exclusion_sum_inf_compl (G := ℤ) s S (f := 1)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem measure_union₀' (hs : NullMeasurableSet s μ) (hd : AEDisjoint μ s t) :
    μ (s ∪ t) = μ s + μ t

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hd : AEDisjoint μ s t
⊢ μ (s ∪ t) = μ s + μ t

Tactic:
rw [union_comm, measure_union₀ hs (AEDisjoint.symm hd), add_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblXYZ_smul (P : Fin 3 → R) (u : R) : W'.dblXYZ (u • P) = u ^ 4 • W'.dblXYZ P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ W'.dblXYZ (u • P) = u ^ 4 • W'.dblXYZ P

Tactic:
rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]

Result:
no goals
-- Mathlib/Analysis/Complex/Periodic.lean
theorem im_invQParam (q : ℂ) : im (invQParam h q) = -h / (2 * π) * Real.log ‖q‖

Proof state:
h : ℝ
q : ℂ
⊢ (invQParam h q).im = -h / (2 * π) * Real.log ‖q‖

Tactic:
simp only [invQParam, ← div_div, div_I, neg_mul, neg_im, mul_im, mul_re, div_ofReal_re,
  div_ofNat_re, ofReal_re, I_re, mul_zero, div_ofReal_im, div_ofNat_im, ofReal_im, zero_div, I_im,
  mul_one, sub_self, zero_mul, add_zero, log_re, zero_add, neg_div]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem coe_deleteEdges_eq (s : Set (Sym2 V)) :
    (G'.deleteEdges s).coe = G'.coe.deleteEdges (Sym2.map (↑) ⁻¹' s)

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ (G'.deleteEdges s).coe = G'.coe.deleteEdges (Sym2.map Subtype.val ⁻¹' s)

Tactic:
ext ⟨v, hv⟩ ⟨w, hw⟩

Result:
case Adj.h.mk.h.mk.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
v : V
hv : v ∈ (G'.deleteEdges s).verts
w : V
hw : w ∈ (G'.deleteEdges s).verts
⊢ (G'.deleteEdges s).coe.Adj ⟨v, hv⟩ ⟨w, hw⟩ ↔ (G'.coe.deleteEdges (Sym2.map Subtype.val ⁻¹' s)).Adj ⟨v, hv⟩ ⟨w, hw⟩

Proof state:
case Adj.h.mk.h.mk.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
v : V
hv : v ∈ (G'.deleteEdges s).verts
w : V
hw : w ∈ (G'.deleteEdges s).verts
⊢ (G'.deleteEdges s).coe.Adj ⟨v, hv⟩ ⟨w, hw⟩ ↔ (G'.coe.deleteEdges (Sym2.map Subtype.val ⁻¹' s)).Adj ⟨v, hv⟩ ⟨w, hw⟩

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem diff_ae_eq_self : (s \ t : Set α) =ᵐ[μ] s ↔ μ (s ∩ t) = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ s \ t =ᶠ[ae μ] s ↔ μ (s ∩ t) = 0

Tactic:
simp [eventuallyLE_antisymm_iff, ae_le_set, diff_diff_right, diff_diff,
  diff_eq_empty.2 Set.subset_union_right]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem inf_union [DecidableEq β] : (s₁ ∪ s₂).inf f = s₁.inf f ⊓ s₂.inf f :=
  eq_of_forall_le_iff fun c ↦ by simp [or_imp, forall_and]

Proof state:
α : Type u_2
β : Type u_3
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
c : α
⊢ c ≤ (s₁ ∪ s₂).inf f ↔ c ≤ s₁.inf f ⊓ s₂.inf f

Tactic:
simp [or_imp, forall_and]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem X_pow_mul_assoc {n : ℕ} : p * X ^ n * q = p * q * X ^ n

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p * X ^ n * q = p * q * X ^ n

Tactic:
rw [mul_assoc, X_pow_mul, ← mul_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_pi_ball (a : ι → ℝ) {r : ℝ} (hr : 0 < r) :
    volume (Metric.ball a r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 < r
⊢ volume (Metric.ball a r) = ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
simp only [MeasureTheory.volume_pi_ball a hr, volume_ball, Finset.prod_const]

Result:
ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 < r
⊢ ofReal (2 * r) ^ Finset.univ.card = ofReal ((2 * r) ^ Fintype.card ι)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 < r
⊢ ofReal (2 * r) ^ Finset.univ.card = ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
exact (ENNReal.ofReal_pow (mul_nonneg zero_le_two hr.le) _).symm

Result:
no goals
-- Mathlib/RingTheory/Trace/Defs.lean
theorem traceForm_toMatrix [DecidableEq ι] (b : Basis ι R S) (i j) :
    BilinForm.toMatrix b (traceForm R S) i j = trace R S (b i * b j)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
i j : ι
⊢ (BilinForm.toMatrix b) (traceForm R S) i j = (trace R S) (b i * b j)

Tactic:
rw [BilinForm.toMatrix_apply, traceForm_apply]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma lt_of_pow_dvd_right (hb : b ≠ 0) (ha : 2 ≤ a) (h : a ^ n ∣ b) : n < b

Proof state:
a b n : ℕ
hb : b ≠ 0
ha : 2 ≤ a
h : a ^ n ∣ b
⊢ n < b

Tactic:
rw [← Nat.pow_lt_pow_iff_right (succ_le_iff.1 ha)]

Result:
a b n : ℕ
hb : b ≠ 0
ha : 2 ≤ a
h : a ^ n ∣ b
⊢ a ^ n < a ^ b

Proof state:
a b n : ℕ
hb : b ≠ 0
ha : 2 ≤ a
h : a ^ n ∣ b
⊢ a ^ n < a ^ b

Tactic:
exact Nat.lt_of_le_of_lt (le_of_dvd (Nat.pos_iff_ne_zero.2 hb) h) (Nat.lt_pow_self ha)

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem associated_isSymm (Q : QuadraticMap R M N) (x y : M) :
    associatedHom S Q x y = associatedHom S Q y x

Proof state:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x y : M
⊢ (((associatedHom S) Q) x) y = (((associatedHom S) Q) y) x

Tactic:
simp only [associated_apply, sub_eq_add_neg, add_assoc, add_comm, add_left_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_eq_left_iff_dvd : m ∣ n ↔ gcd m n = m :=
  ⟨fun h => by rw [gcd_rec, mod_eq_zero_of_dvd h, gcd_zero_left],
   fun h => h ▸ gcd_dvd_right m n⟩

Proof state:
m n : Nat
h : m ∣ n
⊢ m.gcd n = m

Tactic:
rw [gcd_rec, mod_eq_zero_of_dvd h, gcd_zero_left]

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommFoldr_eq_foldr (s : Multiset α) [h : LeftCommutative f] (b : β) :
    noncommFoldr f s (fun x _ y _ _ => h.left_comm x y) b = foldr f b s

Proof state:
α : Type u_3
β : Type u_4
f : α → β → β
s : Multiset α
h : LeftCommutative f
b : β
⊢ noncommFoldr f s ⋯ b = foldr f b s

Tactic:
induction s using Quotient.inductionOn

Result:
case h
α : Type u_3
β : Type u_4
f : α → β → β
h : LeftCommutative f
b : β
a✝ : List α
⊢ noncommFoldr f ⟦a✝⟧ ⋯ b = foldr f b ⟦a✝⟧

Proof state:
case h
α : Type u_3
β : Type u_4
f : α → β → β
h : LeftCommutative f
b : β
a✝ : List α
⊢ noncommFoldr f ⟦a✝⟧ ⋯ b = foldr f b ⟦a✝⟧

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
@[simp] lemma add_bot (x : WithBot α) : x + ⊥ = ⊥

Proof state:
α : Type u
inst✝ : Add α
x : WithBot α
⊢ x + ⊥ = ⊥

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem ΓSpecIso_hom_fromSpec_app :
    (Scheme.ΓSpecIso Γ(X, U)).hom ≫ hU.fromSpec.app U =
      (Spec Γ(X, U)).presheaf.map (eqToHom hU.fromSpec_preimage_self).op

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ (Scheme.ΓSpecIso Γ(X, U)).hom ≫ Scheme.Hom.app hU.fromSpec U = (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op

Tactic:
simp only [fromSpec, Scheme.comp_coeBase, Opens.map_comp_obj, Scheme.comp_app,
  Scheme.Opens.ι_app_self, eqToHom_op, Scheme.app_eq _ U.ι_preimage_self,
  Scheme.Opens.toScheme_presheaf_map, eqToHom_unop, eqToHom_map U.ι.opensFunctor, Opens.map_top,
  isoSpec_inv_appTop, Scheme.Opens.topIso_hom, Category.assoc, ← Functor.map_comp_assoc,
  eqToHom_trans, eqToHom_refl, X.presheaf.map_id, Category.id_comp, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/Algebra/Star/Basic.lean
theorem star_star_mul (x y : R) : star (star x * y) = star y * x

Proof state:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ star (star x * y) = star y * x

Tactic:
rw [star_mul, star_star]

Result:
no goals