harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ofLEMk_comp {B A : C} {X : Subobject B} {f : A ⟶ B} [Mono f] (h : X ≤ mk f) :
    ofLEMk X f h ≫ f = X.arrow

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
h : X ≤ mk f
⊢ X.ofLEMk f h ≫ f = X.arrow

Tactic:
simp [ofLEMk]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem inf_eq_right : a ⊓ b = b ↔ b ≤ a :=
  le_antisymm_iff.trans <| by simp [le_rfl]

Proof state:
α : Type u
inst✝ : SemilatticeInf α
a b : α
⊢ a ⊓ b ≤ b ∧ b ≤ a ⊓ b ↔ b ≤ a

Tactic:
simp [le_rfl]

Result:
no goals
-- Mathlib/RepresentationTheory/Rep.lean
theorem ρ_inv_self_apply {G : Type u} [Group G] (A : Rep k G) (g : G) (x : A) :
    A.ρ g⁻¹ (A.ρ g x) = x :=
  show (A.ρ g⁻¹ * A.ρ g) x = x by rw [← map_mul, inv_mul_cancel, map_one, LinearMap.one_apply]

Proof state:
k : Type u
inst✝¹ : CommRing k
G : Type u
inst✝ : Group G
A : Rep k G
g : G
x : ↑A.V
⊢ (A.ρ g⁻¹ * A.ρ g) x = x

Tactic:
rw [← map_mul, inv_mul_cancel, map_one, LinearMap.one_apply]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem sigma_zero_apply_prime_pow {p i : ℕ} (hp : p.Prime) : σ 0 (p ^ i) = i + 1

Proof state:
p i : ℕ
hp : Nat.Prime p
⊢ (σ 0) (p ^ i) = i + 1

Tactic:
simp [sigma_apply_prime_pow hp]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem esymm_eq_multiset_esymm : esymm σ R = (univ.val.map X).esymm

Proof state:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ esymm σ R = (Multiset.map X univ.val).esymm

Tactic:
exact funext fun n => (esymm_map_val X _ n).symm

Result:
no goals
-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem matPolyEquiv_symm_C (M : Matrix n n R) : matPolyEquiv.symm (C M) = M.map C

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ matPolyEquiv.symm (C M) = M.map ⇑C

Tactic:
simp [matPolyEquiv, ← C_eq_algebraMap]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma closure_spanning_iff (hS : S ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
S : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ M.Spanning (M.closure S) ↔ M.Spanning S

Tactic:
rw [spanning_iff_closure_eq, closure_closure, ← spanning_iff_closure_eq]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
theorem PInftyToNormalizedMooreComplex_naturality {X Y : SimplicialObject A} (f : X ⟶ Y) :
    AlternatingFaceMapComplex.map f ≫ PInftyToNormalizedMooreComplex Y =
      PInftyToNormalizedMooreComplex X ≫ NormalizedMooreComplex.map f

Proof state:
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X Y : SimplicialObject A
f : X ⟶ Y
⊢ AlternatingFaceMapComplex.map f ≫ PInftyToNormalizedMooreComplex Y =
    PInftyToNormalizedMooreComplex X ≫ NormalizedMooreComplex.map f

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.map_inl_inr_codiag {X Y : C} [HasBinaryCoproduct X Y]
    [HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)] :
    coprod.map coprod.inl coprod.inr ≫ codiag (X ⨿ Y) = 𝟙 (X ⨿ Y)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)
⊢ map inl inr ≫ codiag (X ⨿ Y) = 𝟙 (X ⨿ Y)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertMany_empty_list_cons {k : α} {v : β}
    {tl : List (α × β)} :
    (insertMany empty (⟨k, v⟩ :: tl)) = (insertMany (empty.insert k v) tl).1

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
k : α
v : β
tl : List (α × β)
⊢ (insertMany empty ((k, v) :: tl)).val = (insertMany (empty.insert k v) tl).val

Tactic:
rw [insertMany_cons]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem eq_false_of_not_eq_true' {a : Bool} : !a = true → a = false

Proof state:
a : Bool
⊢ (!decide (a = true)) = true → a = false

Tactic:
cases a <;> decide

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma dirac_unit_compProd_const (μ : Measure β) [IsFiniteMeasure μ] :
    Measure.dirac () ⊗ₘ Kernel.const Unit μ = μ.map (Prod.mk ())

Proof state:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
inst✝ : IsFiniteMeasure μ
⊢ dirac () ⊗ₘ Kernel.const Unit μ = map (Prod.mk ()) μ

Tactic:
rw [dirac_unit_compProd, Kernel.const_apply]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem dist_self_div_left (a b : E) : dist (a / b) a = ‖b‖

Proof state:
E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist (a / b) a = ‖b‖

Tactic:
rw [dist_comm, dist_self_div_right]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem inf_sdiff_self_left : y \ x ⊓ x = ⊥

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y \ x ⊓ x = ⊥

Tactic:
rw [inf_comm, inf_sdiff_self_right]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Algebra.lean
@[simp] lemma algebraMap_le_algebraMap : algebraMap α β a₁ ≤ algebraMap α β a₂ ↔ a₁ ≤ a₂

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : OrderedCommSemiring α
inst✝³ : StrictOrderedSemiring β
inst✝² : Algebra α β
inst✝¹ : SMulPosMono α β
inst✝ : SMulPosReflectLE α β
a₁ a₂ : α
⊢ (algebraMap α β) a₁ ≤ (algebraMap α β) a₂ ↔ a₁ ≤ a₂

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem mem_tail_support_append_iff {t u v w : V} (p : G.Walk u v) (p' : G.Walk v w) :
    t ∈ (p.append p').support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail

Proof state:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ t ∈ (p.append p').support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail

Tactic:
rw [tail_support_append, List.mem_append]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
@[simp] lemma div_ofReal_im (z : ℂ) (x : ℝ) : (z / x).im = z.im / x

Proof state:
z : ℂ
x : ℝ
⊢ (z / ↑x).im = z.im / x

Tactic:
rw [div_ofReal]

Result:
no goals
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem midpoint_mem_perpBisector (p₁ p₂ : P) :
    midpoint ℝ p₁ p₂ ∈ perpBisector p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ midpoint ℝ p₁ p₂ ∈ perpBisector p₁ p₂

Tactic:
simp [mem_perpBisector_iff_inner_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertManyIfNewUnit_empty_list_singleton {k : α} :
    (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) [k]).1 = empty.insertIfNew k ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
⊢ (insertManyIfNewUnit empty [k]).val = empty.insertIfNew k ()

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem map_floor (f : F) (hf : StrictMono f) (a : α) : ⌊f a⌋ = ⌊a⌋ :=
  floor_congr fun n => by rw [← map_intCast f, hf.le_iff_le]

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : LinearOrderedRing β
inst✝³ : FloorRing α
inst✝² : FloorRing β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
n : ℤ
⊢ ↑n ≤ f a ↔ ↑n ≤ a

Tactic:
rw [← map_intCast f, hf.le_iff_le]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Constructions.lean
@[to_additive (attr := simp) pi_norm_const]
lemma pi_norm_const' [Nonempty ι] (a : E) : ‖fun _i : ι => a‖ = ‖a‖

Proof state:
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Nonempty ι
a : E
⊢ ‖fun _i => a‖ = ‖a‖

Tactic:
simpa only [← dist_one_right] using dist_pi_const a 1

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoUniformlyOn_empty : TendstoUniformlyOn F f p ∅ := fun u _ => by simp

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
u : Set (β × β)
x✝ : u ∈ 𝓤 β
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ ∅, (f x, F n x) ∈ u

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem geom_mean_le_arith_mean4_weighted {w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ} (hw₁ : 0 ≤ w₁)
    (hw₂ : 0 ≤ w₂) (hw₃ : 0 ≤ w₃) (hw₄ : 0 ≤ w₄) (hp₁ : 0 ≤ p₁) (hp₂ : 0 ≤ p₂) (hp₃ : 0 ≤ p₃)
    (hp₄ : 0 ≤ p₄) (hw : w₁ + w₂ + w₃ + w₄ = 1) :
    p₁ ^ w₁ * p₂ ^ w₂ * p₃ ^ w₃ * p₄ ^ w₄ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄ :=
  NNReal.geom_mean_le_arith_mean4_weighted ⟨w₁, hw₁⟩ ⟨w₂, hw₂⟩ ⟨w₃, hw₃⟩ ⟨w₄, hw₄⟩ ⟨p₁, hp₁⟩
      ⟨p₂, hp₂⟩ ⟨p₃, hp₃⟩ ⟨p₄, hp₄⟩ <|
    NNReal.coe_inj.1 <| by assumption

Proof state:
w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ
hw₁ : 0 ≤ w₁
hw₂ : 0 ≤ w₂
hw₃ : 0 ≤ w₃
hw₄ : 0 ≤ w₄
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hp₃ : 0 ≤ p₃
hp₄ : 0 ≤ p₄
hw : w₁ + w₂ + w₃ + w₄ = 1
⊢ ↑(⟨w₁, hw₁⟩ + ⟨w₂, hw₂⟩ + ⟨w₃, hw₃⟩ + ⟨w₄, hw₄⟩) = ↑1

Tactic:
assumption

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem lintegral_fst (κ : Kernel α (β × γ)) (a : α) {g : β → ℝ≥0∞} (hg : Measurable g) :
    ∫⁻ c, g c ∂fst κ a = ∫⁻ bc : β × γ, g bc.fst ∂κ a

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

Tactic:
rw [fst_eq, lintegral_map _ measurable_fst a hg]

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
lemma natDegree_sum_le_of_forall_le {n : ℕ} (f : ι → S[X]) (h : ∀ i ∈ s, natDegree (f i) ≤ n) :
    natDegree (∑ i ∈ s, f i) ≤ n :=
  le_trans (natDegree_sum_le s f) <| (Finset.fold_max_le n).mpr <| by simpa

Proof state:
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
n : ℕ
f : ι → S[X]
h : ∀ i ∈ s, (f i).natDegree ≤ n
⊢ 0 ≤ n ∧ ∀ x ∈ s, (natDegree ∘ f) x ≤ n

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem univ_nonempty_iff : (univ : Finset α).Nonempty ↔ Nonempty α

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ univ.Nonempty ↔ Nonempty α

Tactic:
rw [← coe_nonempty, coe_univ, Set.nonempty_iff_univ_nonempty]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Basic.lean
theorem mapDomain_algebraMap (A : Type*) {H F : Type*} [CommSemiring k] [Semiring A] [Algebra k A]
    [AddMonoid G] [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H]
    (f : F) (r : k) :
    mapDomain f (algebraMap k A[G] r) = algebraMap k A[H] r

Proof state:
k : Type u₁
G : Type u₂
A : Type u_3
H : Type u_4
F : Type u_5
inst✝⁶ : CommSemiring k
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : AddMonoid G
inst✝² : AddMonoid H
inst✝¹ : FunLike F G H
inst✝ : AddMonoidHomClass F G H
f : F
r : k
⊢ mapDomain (⇑f) ((algebraMap k A[G]) r) = (algebraMap k A[H]) r

Tactic:
simp only [Function.comp_apply, mapDomain_single, AddMonoidAlgebra.coe_algebraMap, map_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_le_one_iff_of_pos (hx : 0 < x) : x ^ y ≤ 1 ↔ 1 ≤ x ∧ y ≤ 0 ∨ x ≤ 1 ∧ 0 ≤ y

Proof state:
x y : ℝ
hx : 0 < x
⊢ x ^ y ≤ 1 ↔ 1 ≤ x ∧ y ≤ 0 ∨ x ≤ 1 ∧ 0 ≤ y

Tactic:
rw [rpow_def_of_pos hx, exp_le_one_iff, mul_nonpos_iff, log_nonneg_iff hx, log_nonpos_iff hx.le]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iInter_eq_empty_iff {f : ι → Set α} : ⋂ i, f i = ∅ ↔ ∀ x, ∃ i, x ∉ f i

Proof state:
α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ ⋂ i, f i = ∅ ↔ ∀ (x : α), ∃ i, x ∉ f i

Tactic:
simp [Set.eq_empty_iff_forall_not_mem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none

Proof state:
α✝ : Type u_1
p : α✝ → Bool
n : Nat
a : α✝
h : ¬p a = true
⊢ find? p (replicate n a) = none

Tactic:
simp [find?_replicate, h]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
theorem PInfty_f_idem (n : ℕ) : (PInfty.f n : X _⦋n⦌ ⟶ _) ≫ PInfty.f n = PInfty.f n

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f n ≫ PInfty.f n = PInfty.f n

Tactic:
simp only [PInfty_f, P_f_idem]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_of_forall_fin_meas_le [SigmaFinite μ] (C : ℝ≥0∞) (hC : C < ∞) {f : α → E}
    (hf_meas : AEStronglyMeasurable[m] f μ)
    (hf : ∀ s : Set α, MeasurableSet[m] s → μ s ≠ ∞ → ∫⁻ x in s, ‖f x‖ₑ ∂μ ≤ C) :
    Integrable f μ :=
  have : SigmaFinite (μ.trim le_rfl)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite μ
C : ℝ≥0∞
hC : C < ⊤
f : α → E
hf_meas : AEStronglyMeasurable f μ
hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ ≤ C
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
rwa [@trim_eq_self _ m]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_add_Icc : (fun x => a + x) ⁻¹' Icc b c = Icc (b - a) (c - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) ⁻¹' Icc b c = Icc (b - a) (c - a)

Tactic:
simp [← Ici_inter_Iic]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Semiconj.lean
theorem zero_right [MulZeroClass G₀] (a : G₀) : SemiconjBy a 0 0

Proof state:
G₀ : Type u_1
inst✝ : MulZeroClass G₀
a : G₀
⊢ SemiconjBy a 0 0

Tactic:
simp only [SemiconjBy, mul_zero, zero_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem bneTrueOfEqFalse {a b : Nat} (p : (a = b) = False) : (a != b) = true

Proof state:
a b : Nat
p : (a = b) = False
⊢ (a != b) = true

Tactic:
simp [bne, beqFalseOfEqFalse p]

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem map_mkQ_eq_top : map p.mkQ p' = ⊤ ↔ p ⊔ p' = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ map p.mkQ p' = ⊤ ↔ p ⊔ p' = ⊤

Tactic:
simp only [LinearMap.map_eq_top_iff p.range_mkQ, sup_comm, ker_mkQ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem empty_eq_flatten_iff {L : Array (Array α)} : #[] = L.flatten ↔ ∀ l ∈ L, l = #[]

Proof state:
α : Type u_1
L : Array (Array α)
⊢ #[] = L.flatten ↔ ∀ (l : Array α), l ∈ L → l = #[]

Tactic:
rw [eq_comm, flatten_eq_empty_iff]

Result:
no goals
-- Mathlib/Control/Functor/Multivariate.lean
theorem LiftP_def (x : F α) : LiftP' P x ↔ ∃ u : F (Subtype_ P), subtypeVal P <$$> u = x :=
  exists_iff_exists_of_mono F _ _ (toSubtype_of_subtype P) (by simp [MvFunctor.map_map])

Proof state:
n : ℕ
α : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
P : α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
x : F α
⊢ ∀ (u : F fun i => Subtype ((fun i x => ofRepeat (P i x)) i)),
    (fun i => Subtype.val) <$$> u = x ↔ subtypeVal P <$$> toSubtype P <$$> u = x

Tactic:
simp [MvFunctor.map_map]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ioc_pred_left_of_not_isMin (ha : ¬IsMin a) : Ioc (pred a) b = Icc a b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ioc (pred a) b = Icc a b

Tactic:
rw [← Ioi_inter_Iic, Ioi_pred_of_not_isMin ha, Ici_inter_Iic]

Result:
no goals
-- Mathlib/Dynamics/OmegaLimit.lean
theorem mem_omegaLimit_iff_frequently₂ (y : β) :
    y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ t in f, (ϕ t '' s ∩ n).Nonempty

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (ϕ t '' s ∩ n).Nonempty

Tactic:
simp_rw [mem_omegaLimit_iff_frequently, image_inter_nonempty_iff]

Result:
no goals
-- Mathlib/Algebra/Ring/Semiconj.lean
theorem neg_one_left (x : R) : SemiconjBy (-1) x x

Proof state:
R : Type u
inst✝¹ : MulOneClass R
inst✝ : HasDistribNeg R
x : R
⊢ SemiconjBy (-1) x x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)} {k : α}
    (contains_eq_false : (l.map Prod.fst).contains k = false)
    {h'} :
    get (insertMany m l) k h' =
      get m k (mem_of_mem_insertMany_list h h' contains_eq_false)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k : α
contains_eq_false : (List.map Prod.fst l).contains k = false
h' : k ∈ insertMany m l
⊢ get (insertMany m l) k h' = get m k ⋯

Tactic:
simp_to_raw using Raw₀.Const.get_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_modify_self (h : m.1.WF) {k : α} [Inhabited (β)] {f : β → β} :
    Const.get! (Const.modify m k f) k = ((Const.get? m k).map f).get!

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k : α
inst✝ : Inhabited β
f : β → β
⊢ get! (modify m k f) k = (Option.map f (get? m k)).get!

Tactic:
simp_to_model [Const.modify] using List.Const.getValue!_modifyKey_self

Result:
no goals
-- Mathlib/LinearAlgebra/StdBasis.lean
@[simp] lemma surjective_piEquiv_apply_iff (v : ι → M) :
    Surjective (piEquiv ι R M v) ↔ span R (range v) = ⊤

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝³ : Finite ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
⊢ Surjective ⇑((piEquiv ι R M) v) ↔ span R (range v) = ⊤

Tactic:
rw [← LinearMap.range_eq_top, range_piEquiv]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem comap_unop_one :
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (1 : Submodule R A) = 1

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ comap (↑(opLinearEquiv R).symm) 1 = 1

Tactic:
rw [← map_equiv_eq_comap_symm, map_op_one]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem IsOfFinOrder.mono [Monoid β] {y : β} (hx : IsOfFinOrder x) (h : orderOf y ∣ orderOf x) :
    IsOfFinOrder y

Proof state:
G : Type u_1
β : Type u_5
inst✝¹ : Monoid G
x : G
inst✝ : Monoid β
y : β
hx : IsOfFinOrder x
h : orderOf y ∣ orderOf x
⊢ IsOfFinOrder y

Tactic:
rw [← orderOf_pos_iff] at hx ⊢

Result:
G : Type u_1
β : Type u_5
inst✝¹ : Monoid G
x : G
inst✝ : Monoid β
y : β
hx : 0 < orderOf x
h : orderOf y ∣ orderOf x
⊢ 0 < orderOf y

Proof state:
G : Type u_1
β : Type u_5
inst✝¹ : Monoid G
x : G
inst✝ : Monoid β
y : β
hx : 0 < orderOf x
h : orderOf y ∣ orderOf x
⊢ 0 < orderOf y

Tactic:
exact Nat.pos_of_dvd_of_pos h hx

Result:
no goals
-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem binomial_one [DecidableEq α] (h : a ≠ b) (h₁ : f a = 1) :
    multinomial {a, b} f = (f b).succ

Proof state:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
h₁ : f a = 1
⊢ multinomial {a, b} f = (f b).succ

Tactic:
simp [multinomial_insert_one (Finset.not_mem_singleton.mpr h) h₁]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean
theorem ι_f_succ (n : ℕ) : I.ι.f (n + 1) = 0 :=
  (isZero_single_obj_X _ _ _ _ (by simp)).eq_of_src _ _

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
@[gcongr]
lemma verticalStrip_mono {A B A' B' : ℝ} (hA : A ≤ A') (hB : B' ≤ B) :
    verticalStrip A B ⊆ verticalStrip A' B'

Proof state:
A B A' B' : ℝ
hA : A ≤ A'
hB : B' ≤ B
⊢ verticalStrip A B ⊆ verticalStrip A' B'

Tactic:
rintro z ⟨hzre, hzim⟩

Result:
case intro
A B A' B' : ℝ
hA : A ≤ A'
hB : B' ≤ B
z : ℍ
hzre : |z.re| ≤ A
hzim : B ≤ z.im
⊢ z ∈ verticalStrip A' B'

Proof state:
case intro
A B A' B' : ℝ
hA : A ≤ A'
hB : B' ≤ B
z : ℍ
hzre : |z.re| ≤ A
hzim : B ≤ z.im
⊢ z ∈ verticalStrip A' B'

Tactic:
exact ⟨hzre.trans hA, hB.trans hzim⟩

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma isReal_comap_iff (f : k ≃+* K) {w : InfinitePlace K} :
    IsReal (w.comap (f : k →+* K)) ↔ IsReal w

Proof state:
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k ≃+* K
w : InfinitePlace K
⊢ (w.comap ↑f).IsReal ↔ w.IsReal

Tactic:
rw [← mk_embedding w, comap_mk, isReal_mk_iff, isReal_mk_iff, ComplexEmbedding.isReal_comp_iff]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Prod.lean
lemma map_prod_map {ε} {mε : MeasurableSpace ε} (κ : Kernel α β) [IsSFiniteKernel κ]
    (η : Kernel α δ) [IsSFiniteKernel η] {f : β → γ} (hf : Measurable f) {g : δ → ε}
    (hg : Measurable g) : (κ.map f) ×ₖ (η.map g) = (κ ×ₖ η).map (Prod.map f g)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α δ
inst✝ : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
x : α
⊢ (κ.map f ×ₖ η.map g) x = ((κ ×ₖ η).map (Prod.map f g)) x

Tactic:
rw [map_apply _ (hf.prod_map hg), prod_apply κ, ← Measure.map_prod_map _ _ hf hg, prod_apply,
  map_apply _ hf, map_apply _ hg]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α δ
inst✝ : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
⊢ κ.map f ×ₖ η.map g = (κ ×ₖ η).map (Prod.map f g)

Tactic:
ext1 x

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α δ
inst✝ : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
x : α
⊢ (κ.map f ×ₖ η.map g) x = ((κ ×ₖ η).map (Prod.map f g)) x
-- Mathlib/Computability/ContextFreeGrammar.lean
lemma derives_reverse : g.reverse.Derives u.reverse v.reverse ↔ g.Derives u v :=
  ⟨fun h ↦ by convert h.reverse <;> simp, .reverse⟩

Proof state:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
⊢ g.Derives u v

Tactic:
convert h.reverse <;> simp

Result:
no goals
-- Mathlib/Data/Setoid/Partition.lean
theorem classes_inj {r₁ r₂ : Setoid α} : r₁ = r₂ ↔ r₁.classes = r₂.classes :=
  ⟨fun h => h ▸ rfl, fun h => ext fun a b => by simp only [rel_iff_exists_classes, exists_prop, h]⟩

Proof state:
α : Type u_1
r₁ r₂ : Setoid α
h : r₁.classes = r₂.classes
a b : α
⊢ r₁ a b ↔ r₂ a b

Tactic:
simp only [rel_iff_exists_classes, exists_prop, h]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma lift_whiskerLeft {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Z ⟶ W) :
    lift f g ≫ (Y ◁ h) = lift f (g ≫ h)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Z ⟶ W
⊢ lift f g ≫ Y ◁ h = lift f (g ≫ h)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = (x / z) + 1

Proof state:
x z : Nat
H : 0 < z
⊢ (x + z) / z = x / z + 1

Tactic:
rw [div_eq_sub_div H (Nat.le_add_left _ _), Nat.add_sub_cancel]

Result:
no goals
-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem ruzsa_triangle_inequality_mulInv_mul_mul (A B C : Finset G) :
    #(A * C⁻¹) * #B ≤ #(A * B) * #(C * B)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A * B) * #(C * B)

Tactic:
simpa using ruzsa_triangle_inequality_mulInv_mulInv_mulInv A B⁻¹ C

Result:
no goals
-- Mathlib/Data/Holor.lean
theorem mul_assoc [Semigroup α] (x : Holor α ds₁) (y : Holor α ds₂) (z : Holor α ds₃) :
    HEq (mul (mul x y) z) (mul x (mul y z))

Proof state:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
⊢ HEq (x ⊗ y ⊗ z) (x ⊗ (y ⊗ z))

Tactic:
simp [cast_heq, mul_assoc0, assocLeft]

Result:
no goals