harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Martingale/Convergence.lean
theorem Submartingale.exists_ae_tendsto_of_bdd [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)
    (hbdd : ∀ n, eLpNorm (f n) 1 μ ≤ R) : ∀ᵐ ω ∂μ, ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)

Tactic:
filter_upwards [hf.upcrossings_ae_lt_top hbdd, ae_bdd_liminf_atTop_of_eLpNorm_bdd one_ne_zero
  (fun n => (hf.stronglyMeasurable n).measurable.mono (ℱ.le n) le_rfl) hbdd] with ω h₁ h₂

Result:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
ω : Ω
h₁ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
h₂ : liminf (fun n => ‖f n ω‖ₑ) atTop < ⊤
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)

Proof state:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
ω : Ω
h₁ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
h₂ : liminf (fun n => ‖f n ω‖ₑ) atTop < ⊤
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)

Tactic:
exact tendsto_of_uncrossing_lt_top h₂ h₁

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_one (a : Int) : a % 1 = 0

Proof state:
a : Int
⊢ a % 1 = 0

Tactic:
simp [emod_def, Int.one_mul, Int.sub_self]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem Topology.IsClosedEmbedding.subtypeVal (h : IsClosed {a | p a}) :
    IsClosedEmbedding ((↑) : Subtype p → X) :=
  ⟨.subtypeVal, by rwa [Subtype.range_coe_subtype]⟩

Proof state:
X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
h : IsClosed {a | p a}
⊢ IsClosed (range Subtype.val)

Tactic:
rwa [Subtype.range_coe_subtype]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem comap_dist_left_atTop_eq_cocompact [ProperSpace α] (x : α) :
    comap (dist x) atTop = cocompact α

Proof state:
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
⊢ comap (dist x) atTop = cocompact α

Tactic:
simp [cobounded_eq_cocompact]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma even_xor_odd (n : ℕ) : Xor' (Even n) (Odd n)

Proof state:
n : ℕ
⊢ Xor' (Even n) (Odd n)

Tactic:
simp [Xor', ← not_even_iff_odd, Decidable.em (Even n)]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem rel_iff' {p q : α × α} : Rel α p q ↔ p = q ∨ p = q.swap

Proof state:
α : Type u_1
p q : α × α
⊢ Rel α p q ↔ p = q ∨ p = q.swap

Tactic:
aesop (rule_sets := [Sym2])

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
theorem mul_inv_cancel : a ≠ 0 → a * a⁻¹ = 1 :=
  numDenCasesOn' a fun n d hd hn ↦ by
    simp only [divInt_ofNat, ne_eq, hd, not_false_eq_true, mkRat_eq_zero] at hn
    simp [-divInt_ofNat, mkRat_eq_divInt, Int.mul_comm, Int.mul_ne_zero hn (Int.ofNat_ne_zero.2 hd)]

Proof state:
a : ℚ
n : ℤ
d : ℕ
hd : d ≠ 0
hn : n /. ↑d ≠ 0
⊢ n /. ↑d * (n /. ↑d)⁻¹ = 1

Tactic:
simp only [divInt_ofNat, ne_eq, hd, not_false_eq_true, mkRat_eq_zero] at hn

Result:
a : ℚ
n : ℤ
d : ℕ
hd : d ≠ 0
hn : ¬n = 0
⊢ n /. ↑d * (n /. ↑d)⁻¹ = 1

Proof state:
a : ℚ
n : ℤ
d : ℕ
hd : d ≠ 0
hn : ¬n = 0
⊢ n /. ↑d * (n /. ↑d)⁻¹ = 1

Tactic:
simp [-divInt_ofNat, mkRat_eq_divInt, Int.mul_comm, Int.mul_ne_zero hn (Int.ofNat_ne_zero.2 hd)]

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma id_apply (R : CommSemiRingCat) (r : R) :
    (𝟙 R : R ⟶ R) r = r

Proof state:
R : CommSemiRingCat
r : ↑R
⊢ (ConcreteCategory.hom (𝟙 R)) r = r

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem preimage_mul_right_singleton : (· * a) ⁻¹' {b} = {b * a⁻¹}

Proof state:
α : Type u_2
inst✝ : Group α
a b : α
⊢ (fun x => x * a) ⁻¹' {b} = {b * a⁻¹}

Tactic:
rw [← image_mul_right', image_singleton]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem preimage_sUnion {f : α → β} {s : Set (Set β)} : f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
⊢ f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t

Tactic:
rw [sUnion_eq_biUnion, preimage_iUnion₂]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem sign_inv (f : Perm α) : sign f⁻¹ = sign f

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ sign f⁻¹ = sign f

Tactic:
rw [MonoidHom.map_inv sign f, Int.units_inv_eq_self]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem one_not_equiv_zero : ¬const abv 1 ≈ const abv 0 := fun h =>
  have : ∀ ε > 0, ∃ i, ∀ k, i ≤ k → abv (1 - 0) < ε := h
  have h1 : abv 1 ≤ 0 :=
    le_of_not_gt fun h2 : 0 < abv 1 =>
      (Exists.elim (this _ h2)) fun i hi => lt_irrefl (abv 1) <| by simpa using hi _ le_rfl
  have h2 : 0 ≤ abv 1 := abv_nonneg abv _
  have : abv 1 = 0 := le_antisymm h1 h2
  have : (1 : β) = 0 := (abv_eq_zero abv).mp this
  absurd this one_ne_zero

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedField α
inst✝² : Ring β
inst✝¹ : IsDomain β
abv : β → α
inst✝ : IsAbsoluteValue abv
h : const abv 1 ≈ const abv 0
this : ∀ ε > 0, ∃ i, ∀ (k : ℕ), i ≤ k → abv (1 - 0) < ε
h2 : 0 < abv 1
i : ℕ
hi : ∀ (k : ℕ), i ≤ k → abv (1 - 0) < abv 1
⊢ abv 1 < abv 1

Tactic:
simpa using hi _ le_rfl

Result:
no goals
-- Mathlib/Algebra/DirectSum/Idempotents.lean
lemma decompose_eq_mul_idempotent (x : R) (i : I) : decompose V x i = x * idempotent V i

Proof state:
R : Type u_1
I : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq I
V : I → Ideal R
inst✝ : Decomposition V
x : R
i : I
⊢ ↑(((decompose V) x) i) = x * idempotent V i

Tactic:
rw [← smul_eq_mul (a := x), idempotent, ← Submodule.coe_smul, ← smul_apply, ← decompose_smul,
  smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/Data/List/Nodup.lean
theorem nodup_append_comm {l₁ l₂ : List α} : Nodup (l₁ ++ l₂) ↔ Nodup (l₂ ++ l₁)

Proof state:
α : Type u
l₁ l₂ : List α
⊢ (l₁ ++ l₂).Nodup ↔ (l₂ ++ l₁).Nodup

Tactic:
simp only [nodup_append, and_left_comm, disjoint_comm]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem coe_algEquivOfAssociated {p q : K[X]} (hp : p ≠ 0) (hpq : Associated p q) :
    (algEquivOfAssociated hp hpq).toFun =
      liftHom p (root q) (by simp only [aeval_eq, mk_eq_zero, hpq.symm.dvd]) :=
  rfl

Proof state:
K : Type ?u.377291
L : Type ?u.377294
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p q : K[X]
hp : p ≠ 0
hpq : Associated p q
⊢ (aeval (root q)) p = 0

Tactic:
simp only [aeval_eq, mk_eq_zero, hpq.symm.dvd]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma truncatedInf_union_left (hs : a ∈ upperClosure s) (ht : a ∉ upperClosure t) :
    truncatedInf (s ∪ t) a = truncatedInf s a

Proof state:
α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∈ upperClosure ↑s
ht : ∀ x ∈ t, ¬x ≤ a
⊢ (s ∪ t).truncatedInf a = s.truncatedInf a

Tactic:
simp only [truncatedInf_of_mem, hs, filter_union, filter_false_of_mem ht, union_empty,
  upper_aux.2 (Or.inl hs), ht]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∈ upperClosure ↑s
ht : a ∉ upperClosure ↑t
⊢ (s ∪ t).truncatedInf a = s.truncatedInf a

Tactic:
simp only [mem_upperClosure, mem_coe, exists_prop, not_exists, not_and] at ht

Result:
α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∈ upperClosure ↑s
ht : ∀ x ∈ t, ¬x ≤ a
⊢ (s ∪ t).truncatedInf a = s.truncatedInf a
-- Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Strong.lean
theorem whiskerRight_naturality_naturality {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a') :
    F.map₂ β ▷ η.app b ▷ h ≫ (η.naturality g).hom ▷ h =
      (η.naturality f).hom ▷ h ≫ (α_ _ _ _).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ _ _ _).inv

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η : StrongOplaxNatTrans F G
a b : B
a' : C
f g : a ⟶ b
β : f ⟶ g
h : G.obj b ⟶ a'
⊢ F.map₂ β ▷ η.app b ▷ h ≫ (η.naturality g).hom ▷ h =
    (η.naturality f).hom ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv

Tactic:
apply η.toOplax.whiskerRight_naturality_naturality

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem iSup_inf_iSup {ι ι' : Type*} {f : ι → α} {g : ι' → α} :
    ((⨆ i, f i) ⊓ ⨆ j, g j) = ⨆ i : ι × ι', f i.1 ⊓ g i.2

Proof state:
α : Type u
inst✝ : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
⊢ (⨆ i, f i) ⊓ ⨆ j, g j = ⨆ i, f i.1 ⊓ g i.2

Tactic:
simp_rw [iSup_inf_eq, inf_iSup_eq, iSup_prod]

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem isGLB_congr (h : lowerBounds s = lowerBounds t) : IsGLB s a ↔ IsGLB t a

Proof state:
α : Type u
inst✝ : Preorder α
s t : Set α
a : α
h : lowerBounds s = lowerBounds t
⊢ IsGLB s a ↔ IsGLB t a

Tactic:
rw [IsGLB, IsGLB, h]

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
lemma isSemisimpleModule_of_isSemisimpleModule_submodule' {p : ι → Submodule R M}
    (hp : ∀ i, IsSemisimpleModule R (p i)) (hp' : ⨆ i, p i = ⊤) :
    IsSemisimpleModule R M :=
  isSemisimpleModule_of_isSemisimpleModule_submodule (s := Set.univ) (fun i _ ↦ hp i) (by simpa)

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : ι → Submodule R M
hp : ∀ (i : ι), IsSemisimpleModule R ↥(p i)
hp' : ⨆ i, p i = ⊤
⊢ ⨆ i ∈ Set.univ, p i = ⊤

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem hasNeg_addPos (assignment : Assignment) :
    hasNegAssignment (addPosAssignment assignment) = hasNegAssignment assignment

Proof state:
assignment : Assignment
⊢ assignment.addPosAssignment.hasNegAssignment = assignment.hasNegAssignment

Tactic:
cases assignment <;> simp [hasNegAssignment, addPosAssignment]

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
@[simp] lemma wInner_cWeight_const_left (a : 𝕜) (f : ι → 𝕜) :
    ⟪const _ a, f⟫ₙ_[𝕜] = conj a * 𝔼 i, f i

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
a : 𝕜
f : ι → 𝕜
⊢ wInner cWeight (const ι a) f = (starRingEnd 𝕜) a * 𝔼 i : ι, f i

Tactic:
simp [wInner_cWeight_eq_expect, mul_expect]

Result:
no goals
-- Mathlib/GroupTheory/GroupExtension/Basic.lean
theorem right_splitting (g : G) : (s g).right = g

Proof state:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
s : (toGroupExtension φ).Splitting
g : G
⊢ (s g).right = g

Tactic:
rw [← rightHom_eq_right, ← toGroupExtension_rightHom, s.rightHom_splitting]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem rank_comap {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) :
    Module.rank (A.comap f) L = relrank A f.fieldRange

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A : IntermediateField F E
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : L →ₐ[F] E
⊢ Module.rank (↥(comap f A)) L = A.relrank f.fieldRange

Tactic:
simpa only [lift_id] using A.lift_rank_comap f

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem apply_norm_eq_sqrt_inner_adjoint_right (A : E →L[𝕜] F) (x : E) :
    ‖A x‖ = √(re ⟪x, (A† ∘L A) x⟫)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ‖A x‖ = √(re ⟪x, ((adjoint A).comp A) x⟫_𝕜)

Tactic:
rw [← apply_norm_sq_eq_inner_adjoint_right, Real.sqrt_sq (norm_nonneg _)]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem prodIsoProd_inv_fst (X Y : TopCat.{u}) :
    (prodIsoProd X Y).inv ≫ Limits.prod.fst = prodFst

Proof state:
X Y : TopCat
⊢ (X.prodIsoProd Y).inv ≫ prod.fst = prodFst

Tactic:
simp [Iso.inv_comp_eq]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem map_comap_eq_self_of_surjective
    {f : A →ₐ[R] B} (hf : Function.Surjective f) (S : Subalgebra R B) : (S.comap f).map f = S :=
  map_comap_eq_self <| by simp [(AlgHom.range_eq_top f).2 hf]

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Surjective ⇑f
S : Subalgebra R B
⊢ S ≤ f.range

Tactic:
simp [(AlgHom.range_eq_top f).2 hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_eq_none_iff : l[i]? = none ↔ length l ≤ i

Proof state:
α✝ : Type u_1
l : List α✝
i : Nat
⊢ l[i]? = none ↔ l.length ≤ i

Tactic:
simp only [← get?_eq_getElem?, get?_eq_none_iff]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma δ_comp_equiv
    (Q : Generators.{u₁} S T) (P : Generators.{u₂} R S)
    (Q' : Generators.{u₃} S T) (P' : Generators.{u₄} R S) :
    δ Q P ∘ₗ (H1Cotangent.equiv _ _).toLinearMap = δ Q' P'

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
Q' : Generators S T
P' : Generators R S
⊢ δ Q P ∘ₗ ↑(equiv Q' Q) = δ Q' P'

Tactic:
ext x

Result:
case h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
Q' : Generators S T
P' : Generators R S
x : Q'.toExtension.H1Cotangent
⊢ (δ Q P ∘ₗ ↑(equiv Q' Q)) x = (δ Q' P') x

Proof state:
case h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
Q' : Generators S T
P' : Generators R S
x : Q'.toExtension.H1Cotangent
⊢ (δ Q P ∘ₗ ↑(equiv Q' Q)) x = (δ Q' P') x

Tactic:
exact δ_map Q P Q' P' _ _

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
lemma edist_top [DecidableEq V] : (⊤ : SimpleGraph V).edist u v = (if u = v then 0 else 1)

Proof state:
V : Type u_1
u v : V
inst✝ : DecidableEq V
⊢ ⊤.edist u v = if u = v then 0 else 1

Tactic:
by_cases h : u = v <;> simp [h]

Result:
no goals
-- Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean
@[to_additive]
lemma card_mul_self_le [DecidableEq G] {A : Finset G} (hA : IsApproximateSubgroup K (A : Set G)) :
    #(A * A) ≤ K * #A

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
⊢ ↑(#(A * A)) ≤ K * ↑(#A)

Tactic:
simpa [sq] using hA.card_pow_le (n := 2)

Result:
no goals
-- Mathlib/Data/Ordering/Lemmas.lean
@[simp]
lemma dthen_eq_then (o₁ o₂ : Ordering) : o₁.dthen (fun _ => o₂) = o₁.then o₂

Proof state:
o₁ o₂ : Ordering
⊢ (o₁.dthen fun x => o₂) = o₁.then o₂

Tactic:
cases o₁ <;> rfl

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem toFinsupp_eq_zero {a : SkewMonoidAlgebra k G} : a.toFinsupp = 0 ↔ a = 0

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a : SkewMonoidAlgebra k G
⊢ a.toFinsupp = 0 ↔ a = 0

Tactic:
rw [← toFinsupp_zero, toFinsupp_inj]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem mem_nhdsSet_iff_forall : s ∈ 𝓝ˢ t ↔ ∀ x : X, x ∈ t → s ∈ 𝓝 x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∈ 𝓝ˢ t ↔ ∀ x ∈ t, s ∈ 𝓝 x

Tactic:
simp_rw [nhdsSet, Filter.mem_sSup, forall_mem_image]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_biUnion_closure_eq_closure_biUnion (M : Matroid α) (Xs : ι → Set α) (A : Set ι) :
    M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Xs i)

Proof state:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
A : Set ι
⊢ M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Xs i)

Tactic:
rw [biUnion_eq_iUnion, M.closure_iUnion_closure_eq_closure_iUnion, biUnion_eq_iUnion]

Result:
no goals
-- Mathlib/Order/RelSeries.lean
@[simp] lemma last_cons (p : RelSeries r) (newHead : α) (rel : r newHead p.head) :
    (p.cons newHead rel).last = p.last

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
newHead : α
rel : r newHead p.head
⊢ ((singleton r newHead).append p rel).last = p.last

Tactic:
rw [last_append]

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
newHead : α
rel : r newHead p.head
⊢ (p.cons newHead rel).last = p.last

Tactic:
delta cons

Result:
α : Type u_1
r : Rel α α
p : RelSeries r
newHead : α
rel : r newHead p.head
⊢ ((singleton r newHead).append p rel).last = p.last
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem coeff_mul_order_add_order  (x y : HahnSeries Γ R) :
    (x * y).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff

Proof state:
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ (x * y).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff

Tactic:
simp only [← of_symm_smul_of_eq_mul]

Result:
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ ((HahnModule.of R).symm (x • (HahnModule.of R) y)).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff

Proof state:
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ ((HahnModule.of R).symm (x • (HahnModule.of R) y)).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff

Tactic:
exact HahnModule.coeff_smul_order_add_order x y

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_natCast (n : ℕ) : ⌊(n : α)⌋ = n :=
  eq_of_forall_le_iff fun a => by rw [le_floor, ← cast_natCast, cast_le]

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
n : ℕ
a : ℤ
⊢ a ≤ ⌊↑n⌋ ↔ a ≤ ↑n

Tactic:
rw [le_floor, ← cast_natCast, cast_le]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma ofHom_sub (φ₁ φ₂ : F ⟶ G) :
    Cochain.ofHom (φ₁ - φ₂) = Cochain.ofHom φ₁ - Cochain.ofHom φ₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ₁ φ₂ : F ⟶ G
⊢ ofHom (φ₁ - φ₂) = ofHom φ₁ - ofHom φ₂

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem disjoint_divisors_filter_isPrimePow {a b : ℕ} (hab : a.Coprime b) :
    Disjoint (a.divisors.filter IsPrimePow) (b.divisors.filter IsPrimePow)

Proof state:
a b : ℕ
hab : a.Coprime b
⊢ Disjoint (filter IsPrimePow a.divisors) (filter IsPrimePow b.divisors)

Tactic:
simp only [Finset.disjoint_left, Finset.mem_filter, and_imp, Nat.mem_divisors, not_and]

Result:
a b : ℕ
hab : a.Coprime b
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 ∣ a → a ≠ 0 → IsPrimePow a_1 → a_1 ∣ b → b ≠ 0 → ¬IsPrimePow a_1

Proof state:
a b : ℕ
hab : a.Coprime b
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 ∣ a → a ≠ 0 → IsPrimePow a_1 → a_1 ∣ b → b ≠ 0 → ¬IsPrimePow a_1

Tactic:
rintro n han _ha hn hbn _hb -

Result:
a b : ℕ
hab : a.Coprime b
n : ℕ
han : n ∣ a
_ha : a ≠ 0
hn : IsPrimePow n
hbn : n ∣ b
_hb : b ≠ 0
⊢ False

Proof state:
a b : ℕ
hab : a.Coprime b
n : ℕ
han : n ∣ a
_ha : a ≠ 0
hn : IsPrimePow n
hbn : n ∣ b
_hb : b ≠ 0
⊢ False

Tactic:
exact hn.ne_one (Nat.eq_one_of_dvd_coprimes hab han hbn)

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem midpoint_self_neg (x : V) : midpoint R x (-x) = 0

Proof state:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x : V
⊢ midpoint R x (-x) = 0

Tactic:
rw [midpoint_eq_smul_add, add_neg_cancel, smul_zero]

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem UniformGroup.ext {G : Type*} [Group G] {u v : UniformSpace G} (hu : @UniformGroup G u _)
    (hv : @UniformGroup G v _)
    (h : @nhds _ u.toTopologicalSpace 1 = @nhds _ v.toTopologicalSpace 1) : u = v :=
  UniformSpace.ext <| by
    rw [@uniformity_eq_comap_nhds_one _ u _ hu, @uniformity_eq_comap_nhds_one _ v _ hv, h]

Proof state:
G : Type u_3
inst✝ : Group G
u v : UniformSpace G
hu : UniformGroup G
hv : UniformGroup G
h : 𝓝 1 = 𝓝 1
⊢ 𝓤 G = 𝓤 G

Tactic:
rw [@uniformity_eq_comap_nhds_one _ u _ hu, @uniformity_eq_comap_nhds_one _ v _ hv, h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem lintegral_restrict {m : MeasurableSpace α} (f : α →ₛ ℝ≥0∞) (s : Set α) (μ : Measure α) :
    f.lintegral (μ.restrict s) = ∑ y ∈ f.range, y * μ (f ⁻¹' {y} ∩ s)

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
s : Set α
μ : Measure α
⊢ f.lintegral (μ.restrict s) = ∑ y ∈ f.range, y * μ (⇑f ⁻¹' {y} ∩ s)

Tactic:
simp only [lintegral, Measure.restrict_apply, f.measurableSet_preimage]

Result:
no goals
-- Mathlib/GroupTheory/PushoutI.lean
theorem base_smul_eq_smul (h : H) (w : NormalWord d) :
    base φ h • w = h • w

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
h : H
w : NormalWord d
⊢ (base φ) h • w = h • w

Tactic:
rw [base_smul_def, base_smul_def']

Result:
no goals
-- Mathlib/Topology/Algebra/Algebra.lean
theorem isClosedEmbedding_coe (x : A) : IsClosedEmbedding ((↑) : elemental R x → A) where
  eq_induced := rfl
  injective := Subtype.coe_injective
  isClosed_range

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
x : A
⊢ IsClosed (range Subtype.val)

Tactic:
simpa using isClosed R x

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem invFun_eq (h : ∃ a, f a = b) : f (invFun f b) = b

Proof state:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
b : β
h : ∃ a, f a = b
⊢ f (invFun f b) = b

Tactic:
simp only [invFun, dif_pos h, h.choose_spec]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem cancel_iso_inv_left {X Y Z : C} (f : Y ≅ X) (g g' : Y ⟶ Z) :
    f.inv ≫ g = f.inv ≫ g' ↔ g = g'

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ≅ X
g g' : Y ⟶ Z
⊢ f.inv ≫ g = f.inv ≫ g' ↔ g = g'

Tactic:
simp only [cancel_epi]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma even_div : Even (m / n) ↔ m % (2 * n) / n = 0

Proof state:
m n : ℕ
⊢ Even (m / n) ↔ m % (2 * n) / n = 0

Tactic:
rw [even_iff_two_dvd, dvd_iff_mod_eq_zero, ← Nat.mod_mul_right_div_self, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem or_of_isSome {o o' : Option α} (h : o.isSome) : o.or o' = o

Proof state:
α : Type u_1
o o' : Option α
h : o.isSome = true
val✝ : α
x✝ : (some val✝).isSome = true
⊢ (some val✝).or o' = some val✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
o o' : Option α
h : o.isSome = true
⊢ o.or o' = o

Tactic:
match o, h with
| some _, _ => simp

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
lemma Ici_inf_erase (ha : a ∈ s) (has : ∀ b ∈ s, b ≤ a → b = a) : Ici a ⊓ s.erase a = s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ Ici a ⊓ s.erase a = s

Tactic:
rw [inf_comm, erase_inf_Ici ha has]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
theorem completedRiemannZeta_one_sub (s : ℂ) :
    completedRiemannZeta (1 - s) = completedRiemannZeta s

Proof state:
s : ℂ
⊢ completedRiemannZeta (1 - s) = completedRiemannZeta s

Tactic:
rw [← completedHurwitzZetaEven_zero, ← completedCosZeta_zero, completedHurwitzZetaEven_one_sub]

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
@[parity_simps] lemma odd_add : Odd (m + n) ↔ (Odd m ↔ Even n)

Proof state:
m n : ℤ
⊢ Odd (m + n) ↔ (Odd m ↔ Even n)

Tactic:
rw [← not_even_iff_odd, even_add, not_iff, ← not_even_iff_odd]

Result:
no goals