harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Cycle.lean
theorem prev_mem (s : Cycle α) (hs : Nodup s) (x : α) (hx : x ∈ s) : s.prev hs x hx ∈ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.reverse.next ⋯ x ⋯ ∈ s.reverse

Tactic:
apply next_mem

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.prev hs x hx ∈ s

Tactic:
rw [← next_reverse_eq_prev, ← mem_reverse_iff]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.reverse.next ⋯ x ⋯ ∈ s.reverse
-- Mathlib/Tactic/Linarith/Lemmas.lean
theorem mul_neg {α} [StrictOrderedRing α] {a b : α} (ha : a < 0) (hb : 0 < b) : b * a < 0 :=
  have : (-b)*a > 0 := mul_pos_of_neg_of_neg (neg_neg_of_pos hb) ha
  neg_of_neg_pos (by simpa)

Proof state:
α : Type u_1
inst✝ : StrictOrderedRing α
a b : α
ha : a < 0
hb : 0 < b
this : -b * a > 0
⊢ 0 < -(b * a)

Tactic:
simpa

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma toUnitHom_inj (ψ : DirichletCharacter R n) : toUnitHom χ = toUnitHom ψ ↔ χ = ψ

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
⊢ toUnitHom χ = toUnitHom ψ ↔ χ = ψ

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/IsNonarchimedean.lean
theorem add_le {α : Type*} [Add α] {f : α → ℝ} (hf : ∀ x : α, 0 ≤ f x)
    (hna : IsNonarchimedean f) {a b : α} : f (a + b) ≤ f a + f b

Proof state:
α : Type u_1
inst✝ : Add α
f : α → ℝ
hf : ∀ (x : α), 0 ≤ f x
hna : IsNonarchimedean f
a b : α
⊢ f a ⊔ f b ≤ f a + f b

Tactic:
rw [max_le_iff, le_add_iff_nonneg_right, le_add_iff_nonneg_left]

Result:
α : Type u_1
inst✝ : Add α
f : α → ℝ
hf : ∀ (x : α), 0 ≤ f x
hna : IsNonarchimedean f
a b : α
⊢ 0 ≤ f b ∧ 0 ≤ f a

Proof state:
α : Type u_1
inst✝ : Add α
f : α → ℝ
hf : ∀ (x : α), 0 ≤ f x
hna : IsNonarchimedean f
a b : α
⊢ 0 ≤ f b ∧ 0 ≤ f a

Tactic:
exact ⟨hf _, hf _⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Add α
f : α → ℝ
hf : ∀ (x : α), 0 ≤ f x
hna : IsNonarchimedean f
a b : α
⊢ f (a + b) ≤ f a + f b

Tactic:
apply le_trans (hna _ _)

Result:
α : Type u_1
inst✝ : Add α
f : α → ℝ
hf : ∀ (x : α), 0 ≤ f x
hna : IsNonarchimedean f
a b : α
⊢ f a ⊔ f b ≤ f a + f b
-- Mathlib/Probability/UniformOn.lean
theorem finite_of_uniformOn_ne_zero {s t : Set Ω} (h : uniformOn s t ≠ 0) : s.Finite

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
s t : Set Ω
h : (uniformOn s) t ≠ 0
hs' : ¬s.Finite
⊢ False

Tactic:
simp [uniformOn, cond, Measure.count_apply_infinite hs'] at h

Result:
no goals

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
s t : Set Ω
h : (uniformOn s) t ≠ 0
⊢ s.Finite

Tactic:
by_contra hs'

Result:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
s t : Set Ω
h : (uniformOn s) t ≠ 0
hs' : ¬s.Finite
⊢ False
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem lowerCrossingTime_le : lowerCrossingTime a b f N n ω ≤ N

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤ N

Tactic:
simp only [lowerCrossingTime, hitting_le ω]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
theorem BitVec.ne_to_beq (a b : BitVec w) : (a ≠ b) = ((!(a == b)) = true)

Proof state:
w : Nat
a b : BitVec w
⊢ (a ≠ b) = ((!a == b) = true)

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/DeriveCountable.lean
theorem cons_eq_imp_init {p : Prop} {a b b' : ℕ}
    (h : b = b' → p) : Nat.pair a b = Nat.pair a b' → p

Proof state:
p : Prop
a b b' : ℕ
h : b = b' → p
⊢ Nat.pair a b = Nat.pair a b' → p

Tactic:
simpa [Nat.pair_eq_pair, and_imp] using h

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem choose_eq_nat_choose [NatPowAssoc R] (n k : ℕ) : choose (n : R) k = Nat.choose n k

Proof state:
case zero
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
k : ℕ
⊢ choose (↑0) k = ↑(Nat.choose 0 k)

Tactic:
cases k with
| zero => rw [choose_zero_right, Nat.choose_zero_right, Nat.cast_one]
| succ k => rw [Nat.cast_zero, choose_zero_succ, Nat.choose_zero_succ, Nat.cast_zero]

Result:
no goals

Proof state:
case zero.succ
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
k : ℕ
⊢ choose (↑0) (k + 1) = ↑(Nat.choose 0 (k + 1))

Tactic:
rw [Nat.cast_zero, choose_zero_succ, Nat.choose_zero_succ, Nat.cast_zero]

Result:
no goals

Proof state:
case zero.zero
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
⊢ choose (↑0) 0 = ↑(Nat.choose 0 0)

Tactic:
rw [choose_zero_right, Nat.choose_zero_right, Nat.cast_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
n k : ℕ
⊢ choose (↑n) k = ↑(n.choose k)

Tactic:
induction n generalizing k with
| zero => cases k with
  | zero => rw [choose_zero_right, Nat.choose_zero_right, Nat.cast_one]
  | succ k => rw [Nat.cast_zero, choose_zero_succ, Nat.choose_zero_succ, Nat.cast_zero]
| succ n ih => cases k with
  | zero => rw [choose_zero_right, Nat.choose_zero_right, Nat.cast_one]
  | succ k => rw [Nat.cast_succ, choose_succ_succ, ih, ih, Nat.choose_succ_succ, Nat.cast_add]

Result:
no goals

Proof state:
case succ.zero
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
n : ℕ
ih : ∀ (k : ℕ), choose (↑n) k = ↑(n.choose k)
⊢ choose (↑(n + 1)) 0 = ↑((n + 1).choose 0)

Tactic:
rw [choose_zero_right, Nat.choose_zero_right, Nat.cast_one]

Result:
no goals

Proof state:
case succ.succ
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
n : ℕ
ih : ∀ (k : ℕ), choose (↑n) k = ↑(n.choose k)
k : ℕ
⊢ choose (↑(n + 1)) (k + 1) = ↑((n + 1).choose (k + 1))

Tactic:
rw [Nat.cast_succ, choose_succ_succ, ih, ih, Nat.choose_succ_succ, Nat.cast_add]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
n : ℕ
ih : ∀ (k : ℕ), choose (↑n) k = ↑(n.choose k)
k : ℕ
⊢ choose (↑(n + 1)) k = ↑((n + 1).choose k)

Tactic:
cases k with
| zero => rw [choose_zero_right, Nat.choose_zero_right, Nat.cast_one]
| succ k => rw [Nat.cast_succ, choose_succ_succ, ih, ih, Nat.choose_succ_succ, Nat.cast_add]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive nsmul_prod]
lemma prod_pow [Monoid β] (s : Set α) (t : Set β) : ∀ n, (s ×ˢ t) ^ n = (s ^ n) ×ˢ (t ^ n)
  | 0 => by simp
  | n + 1 => by simp [pow_succ, prod_pow _ _ n]

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Set α
t : Set β
⊢ s ×ˢ t ^ 0 = (s ^ 0) ×ˢ (t ^ 0)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Set α
t : Set β
n : ℕ
⊢ s ×ˢ t ^ (n + 1) = (s ^ (n + 1)) ×ˢ (t ^ (n + 1))

Tactic:
simp [pow_succ, prod_pow _ _ n]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem ker_le_comap {p : Submodule R₂ M₂} (f : M →ₛₗ[τ₁₂] M₂) :
    ker f ≤ p.comap f :=
  fun x hx ↦ by simp [mem_ker.mp hx]

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
x : M
hx : x ∈ ker f
⊢ x ∈ comap f p

Tactic:
simp [mem_ker.mp hx]

Result:
no goals
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem aeval_modByMonic_eq_self_of_root [Algebra R S] {p q : R[X]} (hq : q.Monic) {x : S}
    (hx : aeval x q = 0) : aeval x (p %ₘ q) = aeval x p

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : R[X]
hq : q.Monic
x : S
hx : (aeval x) q = 0
⊢ (aeval x) (p %ₘ q) = (aeval x) p

Tactic:
rw [modByMonic_eq_sub_mul_div p hq, _root_.map_sub, _root_.map_mul, hx, zero_mul,
  sub_zero]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_two_add_inv_two : (2 : ℝ≥0∞)⁻¹ + 2⁻¹ = 1

Proof state:
⊢ 2⁻¹ + 2⁻¹ = 1

Tactic:
rw [← two_mul, ← div_eq_mul_inv, ENNReal.div_self two_ne_zero ofNat_ne_top]

Result:
no goals
-- Mathlib/Topology/Basic.lean
lemma isClosed_iff_forall_filter :
    IsClosed s ↔ ∀ x, ∀ F : Filter X, F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ IsClosed s ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Tactic:
simp_rw [isClosed_iff_clusterPt]

Result:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ (∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s) ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ (∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s) ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Tactic:
exact ⟨fun hs x F F_ne FS Fx ↦ hs _ <| NeBot.mono F_ne (le_inf Fx FS),
       fun hs x hx ↦ hs x (𝓝 x ⊓ 𝓟 s) hx inf_le_right inf_le_left⟩

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem δ_comp_σ_self' {n} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.castSucc) :
    δ j ≫ σ i = 𝟙 ⦋n⦌

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ δ i.castSucc ≫ σ i = 𝟙 ⦋n⦌

Tactic:
rw [δ_comp_σ_self]

Result:
no goals

Proof state:
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.castSucc
⊢ δ j ≫ σ i = 𝟙 ⦋n⦌

Tactic:
subst H

Result:
n : ℕ
i : Fin (n + 1)
⊢ δ i.castSucc ≫ σ i = 𝟙 ⦋n⦌
-- Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean
lemma toCircle_intCast (j : ℤ) :
    toCircle (j : ZMod N) = exp (2 * π * I * j / N)

Proof state:
N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ ↑(toCircle ↑j) = cexp (2 * ↑π * I * ↑j / ↑N)

Tactic:
rw [toCircle, AddChar.compAddMonoidHom_apply, toCircle_addChar, AddChar.coe_mk,
  AddCircle.toCircle, toAddCircle_intCast, Function.Periodic.lift_coe, Circle.coe_exp]

Result:
N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ cexp (↑(2 * π / 1 * (↑j / ↑N)) * I) = cexp (2 * ↑π * I * ↑j / ↑N)

Proof state:
N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ cexp (↑(2 * π / 1 * (↑j / ↑N)) * I) = cexp (2 * ↑π * I * ↑j / ↑N)

Tactic:
push_cast

Result:
N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ cexp (2 * ↑π / 1 * (↑j / ↑N) * I) = cexp (2 * ↑π * I * ↑j / ↑N)

Proof state:
N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ cexp (2 * ↑π / 1 * (↑j / ↑N) * I) = cexp (2 * ↑π * I * ↑j / ↑N)

Tactic:
ring_nf

Result:
no goals
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem measurable_lintegral {f : α → ℝ≥0∞} (hf : Measurable f) :
    Measurable fun μ : Measure α => ∫⁻ x, f x ∂μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun μ => ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x})

Tactic:
refine .iSup fun n => Finset.measurable_sum _ fun i _ => ?_

Result:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ (SimpleFunc.eapprox f n).range
⊢ Measurable fun μ => i * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {i})

Proof state:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun μ => ∫⁻ (x : α), f x ∂μ

Tactic:
simp only [lintegral_eq_iSup_eapprox_lintegral, hf, SimpleFunc.lintegral]

Result:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun μ => ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x})

Proof state:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ (SimpleFunc.eapprox f n).range
⊢ Measurable fun μ => i * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {i})

Tactic:
refine Measurable.const_mul ?_ _

Result:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ (SimpleFunc.eapprox f n).range
⊢ Measurable fun μ => μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {i})

Proof state:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ (SimpleFunc.eapprox f n).range
⊢ Measurable fun μ => μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {i})

Tactic:
exact measurable_coe ((SimpleFunc.eapprox f n).measurableSet_preimage _)

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem map_sup {β} (f : α → β) (m m' : OuterMeasure α) : map f (m ⊔ m') = map f m ⊔ map f m' :=
  ext fun s => by simp only [map_apply, sup_apply]

Proof state:
α : Type u_1
β : Type u_3
f : α → β
m m' : OuterMeasure α
s : Set β
⊢ ((map f) (m ⊔ m')) s = ((map f) m ⊔ (map f) m') s

Tactic:
simp only [map_apply, sup_apply]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_eq_max_of_aleph0_le_right {a b : Cardinal} (h' : a ≠ 0) (h : ℵ₀ ≤ b) :
    a * b = max a b

Proof state:
a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ b * a = b ⊔ a

Tactic:
exact mul_eq_max_of_aleph0_le_left h h'

Result:
no goals

Proof state:
a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ a * b = a ⊔ b

Tactic:
rw [mul_comm, max_comm]

Result:
a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ b * a = b ⊔ a
-- Mathlib/Topology/Separation/Basic.lean
lemma eventuallyEq_insert [T1Space X] {s t : Set X} {x y : X} (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
    (insert x s : Set X) =ᶠ[𝓝 x] (insert x t : Set X)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ insert x s =ᶠ[𝓝 x] insert x t

Tactic:
simp_rw [eventuallyEq_set] at h ⊢

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, x_1 ∈ insert x s ↔ x_1 ∈ insert x t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ ∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 = x ∨ x_1 ∈ s ↔ x_1 = x ∨ x_1 ∈ t

Tactic:
filter_upwards [nhdsWithin_compl_singleton_le x y h] with y using or_congr (Iff.rfl)

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, x_1 ∈ insert x s ↔ x_1 ∈ insert x t

Tactic:
simp_rw [← union_singleton, ← nhdsWithin_univ, ← compl_union_self {x},
  nhdsWithin_union, eventually_sup, nhdsWithin_singleton,
  eventually_pure, union_singleton, mem_insert_iff, true_or, and_true]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ ∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 = x ∨ x_1 ∈ s ↔ x_1 = x ∨ x_1 ∈ t
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_lt_inv_iff : a⁻¹ < b⁻¹ ↔ b < a

Proof state:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b : α
inst✝ : MulRightStrictMono α
⊢ a * a⁻¹ * b < a * b⁻¹ * b ↔ b < a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b : α
inst✝ : MulRightStrictMono α
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
rw [← mul_lt_mul_iff_left a, ← mul_lt_mul_iff_right b]

Result:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b : α
inst✝ : MulRightStrictMono α
⊢ a * a⁻¹ * b < a * b⁻¹ * b ↔ b < a
-- Mathlib/Order/Category/BddOrd.lean
lemma comp_apply {X Y Z : BddOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y Z : BddOrd
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X.toPartOrd
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean
theorem σ_comp_PInfty (X : SimplicialObject C) {n : ℕ} (i : Fin (n + 1)) :
    X.σ i ≫ PInfty.f (n + 1) = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ PInfty.f (n + 1) = 0

Tactic:
rw [PInfty_f, σ_comp_P_eq_zero X i]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ n + 1 ≤ ↑i + (n + 1)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ n + 1 ≤ ↑i + (n + 1)

Tactic:
simp only [le_add_iff_nonneg_left, zero_le]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem edgeFinset_top [DecidableEq V] :
    (⊤ : SimpleGraph V).edgeFinset = ({e | ¬e.IsDiag} : Finset _)

Proof state:
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
⊢ ⊤.edgeFinset = filter (fun e => ¬e.IsDiag) univ

Tactic:
simp [← coe_inj]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem bind_dirac {m : Measure α} : bind m dirac = m

Proof state:
α : Type u_1
mα : MeasurableSpace α
m : Measure α
⊢ m.bind dirac = m

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
mα : MeasurableSpace α
m : Measure α
s : Set α
hs : MeasurableSet s
⊢ (m.bind dirac) s = m s

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
m : Measure α
s : Set α
hs : MeasurableSet s
⊢ (m.bind dirac) s = m s

Tactic:
simp only [bind_apply hs measurable_dirac, dirac_apply' _ hs, lintegral_indicator hs,
  Pi.one_apply, lintegral_one, restrict_apply, MeasurableSet.univ, univ_inter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_eq_singleton_iff :
    a ++ b = [x] ↔ (a = [] ∧ b = [x]) ∨ (a = [x] ∧ b = [])

Proof state:
α✝ : Type u_1
a b : List α✝
x : α✝
⊢ a ++ b = [x] ↔ a = [] ∧ b = [x] ∨ a = [x] ∧ b = []

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

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma integral_density (hκν : fst κ ≤ ν) [IsFiniteKernel ν]
    (a : α) {s : Set β} (hs : MeasurableSet s) :
    ∫ x, density κ ν a x s ∂(ν a) = (κ a (univ ×ˢ s)).toReal

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫ (x : γ), κ.density ν a x s ∂ν a = ((κ a) (univ ×ˢ s)).toReal

Tactic:
rw [← setIntegral_univ, setIntegral_density_of_measurableSet hκν 0 a hs MeasurableSet.univ]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top {f : α → ε} (hq0_lt : 0 < q)
    (hfq : eLpNorm' f q μ < ∞) : ∫⁻ a, ‖f a‖ₑ ^ q ∂μ < ∞

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq0_lt : 0 < q
hfq : eLpNorm' f q μ < ⊤
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ < ⊤

Tactic:
rw [lintegral_rpow_enorm_eq_rpow_eLpNorm' hq0_lt]

Result:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq0_lt : 0 < q
hfq : eLpNorm' f q μ < ⊤
⊢ eLpNorm' f q μ ^ q < ⊤

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq0_lt : 0 < q
hfq : eLpNorm' f q μ < ⊤
⊢ eLpNorm' f q μ ^ q < ⊤

Tactic:
exact ENNReal.rpow_lt_top_of_nonneg (le_of_lt hq0_lt) (ne_of_lt hfq)

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem map_adjoin_singleton (e : A →ₐ[R] B) (x : A) :
    (adjoin R {x}).map e = adjoin R {e x}

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A →ₐ[R] B
x : A
⊢ Subalgebra.map e (adjoin R {x}) = adjoin R {e x}

Tactic:
rw [map_adjoin, Set.image_singleton]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem IsVonNBounded.add (hs : IsVonNBounded 𝕜 s) (ht : IsVonNBounded 𝕜 t) :
    IsVonNBounded 𝕜 (s + t) := fun U hU ↦ by
  rcases exists_open_nhds_zero_add_subset hU with ⟨V, hVo, hV, hVU⟩
  exact ((hs <| hVo.mem_nhds hV).add (ht <| hVo.mem_nhds hV)).mono_left hVU

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddZeroClass E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : DistribSMul 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
U : Set E
hU : U ∈ 𝓝 0
V : Set E
hVo : IsOpen V
hV : 0 ∈ V
hVU : V + V ⊆ U
⊢ Absorbs 𝕜 U (s + t)

Tactic:
exact ((hs <| hVo.mem_nhds hV).add (ht <| hVo.mem_nhds hV)).mono_left hVU

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddZeroClass E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : DistribSMul 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
U : Set E
hU : U ∈ 𝓝 0
⊢ Absorbs 𝕜 U (s + t)

Tactic:
rcases exists_open_nhds_zero_add_subset hU with ⟨V, hVo, hV, hVU⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddZeroClass E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : DistribSMul 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
U : Set E
hU : U ∈ 𝓝 0
V : Set E
hVo : IsOpen V
hV : 0 ∈ V
hVU : V + V ⊆ U
⊢ Absorbs 𝕜 U (s + t)
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_re_zero_right (x : E) : re ⟪x, 0⟫ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ re ⟪x, 0⟫_𝕜 = 0

Tactic:
simp only [inner_zero_right, AddMonoidHom.map_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc]
lemma descOpcycles_comp {A' : C} (α : A ⟶ A') :
    S.descOpcycles k hk ≫ α = S.descOpcycles (k ≫ α) (by rw [reassoc_of% hk, zero_comp])

Proof state:
C : Type u_1
inst✝² : Category.{?u.250960, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
A' : C
α : A ⟶ A'
⊢ S.f ≫ k ≫ α = 0

Tactic:
rw [reassoc_of% hk, zero_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
A' : C
α : A ⟶ A'
⊢ S.descOpcycles k hk ≫ α = S.descOpcycles (k ≫ α) ⋯

Tactic:
simp only [← cancel_epi S.pOpcycles, p_descOpcycles_assoc, p_descOpcycles]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Classes/Order.lean
theorem BEqCmp.cmp_iff_eq [BEq α] [LawfulBEq α] [BEqCmp (α := α) cmp] : cmp x y = .eq ↔ x = y

Proof state:
α : Type u_1
cmp : α → α → Ordering
x y : α
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : BEqCmp cmp
⊢ cmp x y = Ordering.eq ↔ x = y

Tactic:
simp [BEqCmp.cmp_iff_beq]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem mkPiAlgebraFin_apply_const (a : A) :
    (MultilinearMap.mkPiAlgebraFin R n A fun _ => a) = a ^ n

Proof state:
R : Type uR
n : ℕ
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ ((MultilinearMap.mkPiAlgebraFin R n A) fun x => a) = a ^ n

Tactic:
simp

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

Proof state:
R : Type u_1
A : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : NonUnitalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : TopologicalSpace A
inst✝² : IsTopologicalSemiring A
inst✝¹ : ContinuousConstSMul R A
inst✝ : ContinuousStar A
x : A
⊢ IsClosed (Set.range Subtype.val)

Tactic:
simpa using isClosed R x

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
@[simp] lemma update_eq_self_iff : update f a b = f ↔ b = f a

Proof state:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
⊢ update f a b = f ↔ b = f a

Tactic:
simp [update_eq_iff]

Result:
no goals