harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Girth.lean
lemma exists_egirth_eq_length :
    (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.egirth = w.length) ↔ ¬ G.IsAcyclic

Proof state:
case refine_1.intro.intro.intro
α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
hw : w.IsCycle
right✝ : G.egirth = ↑w.length
hG : G.IsAcyclic
⊢ False

Tactic:
exact hG _ hw

Result:
no goals

Proof state:
case refine_2
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
⊢ ∃ a w, w.IsCycle ∧ G.egirth = ↑w.length

Tactic:
simp_rw [← egirth_eq_top, ← Ne.eq_def, egirth, iInf_subtype', iInf_sigma', ENat.iInf_coe_ne_top,
  ← exists_prop, Subtype.exists', Sigma.exists', eq_comm] at h ⊢

Result:
case refine_2
α : Type u_1
G : SimpleGraph α
h : Nonempty ((i : α) × Subtype Walk.IsCycle)
⊢ ∃ x, ↑(↑x.snd).length = ⨅ x, ↑(↑x.snd).length

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ (∃ a w, w.IsCycle ∧ G.egirth = ↑w.length) ↔ ¬G.IsAcyclic

Tactic:
refine ⟨?_, fun h ↦ ?_⟩

Result:
case refine_1
α : Type u_1
G : SimpleGraph α
⊢ (∃ a w, w.IsCycle ∧ G.egirth = ↑w.length) → ¬G.IsAcyclic

case refine_2
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
⊢ ∃ a w, w.IsCycle ∧ G.egirth = ↑w.length

Proof state:
case refine_1
α : Type u_1
G : SimpleGraph α
⊢ (∃ a w, w.IsCycle ∧ G.egirth = ↑w.length) → ¬G.IsAcyclic

Tactic:
rintro ⟨a, w, hw, _⟩ hG

Result:
case refine_1.intro.intro.intro
α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
hw : w.IsCycle
right✝ : G.egirth = ↑w.length
hG : G.IsAcyclic
⊢ False

Proof state:
case refine_2
α : Type u_1
G : SimpleGraph α
h : Nonempty ((i : α) × Subtype Walk.IsCycle)
⊢ ∃ x, ↑(↑x.snd).length = ⨅ x, ↑(↑x.snd).length

Tactic:
exact ciInf_mem _

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem fin_val_iff {n} {f : α → Fin n} : (Primrec fun a => (f a).1) ↔ Primrec f

Proof state:
α : Type u_1
inst✝ : Primcodable α
n : ℕ
f : α → Fin n
this : Primcodable { a // id a < n } := Primcodable.subtype ⋯
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec fun a => ↑(Fin.equivSubtype (f a))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Primcodable α
n : ℕ
f : α → Fin n
this : Primcodable { a // id a < n } := Primcodable.subtype ⋯
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec f

Tactic:
exact (Iff.trans (by rfl) subtype_val_iff).trans (of_equiv_iff _)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Primcodable α
n : ℕ
f : α → Fin n
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec f

Tactic:
letI : Primcodable { a // id a < n } := Primcodable.subtype (nat_lt.comp .id (const _))

Result:
α : Type u_1
inst✝ : Primcodable α
n : ℕ
f : α → Fin n
this : Primcodable { a // id a < n } := Primcodable.subtype ⋯
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec f
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_zero : s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C

Tactic:
simp_rw [einfsep, ← _root_.bot_eq_zero, iInf_eq_bot, iInf_lt_iff, exists_prop]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_sub_mul_self (x y : E) :
    ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖

Tactic:
repeat' rw [← sq (M := ℝ)]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2

Tactic:
exact norm_sub_sq _ _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖

Tactic:
rw [← sq (M := ℝ)]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2
-- Mathlib/Data/ZMod/Basic.lean
theorem inv_zero : ∀ n : ℕ, (0 : ZMod n)⁻¹ = 0
  | 0 => Int.sign_zero
  | n + 1 =>
    show (Nat.gcdA _ (n + 1) : ZMod (n + 1)) = 0 by
      rw [val_zero]
      unfold Nat.gcdA Nat.xgcd Nat.xgcdAux
      rfl

Proof state:
n : ℕ
⊢ ↑(Nat.gcdA 0 (n + 1)) = 0

Tactic:
unfold Nat.gcdA Nat.xgcd Nat.xgcdAux

Result:
n : ℕ
⊢ ↑(n + 1, 0, 1).2.1 = 0

Proof state:
n : ℕ
⊢ ↑((val 0).gcdA (n + 1)) = 0

Tactic:
rw [val_zero]

Result:
n : ℕ
⊢ ↑(Nat.gcdA 0 (n + 1)) = 0

Proof state:
n : ℕ
⊢ ↑(n + 1, 0, 1).2.1 = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/LeftDerived.lean
@[reassoc]
lemma ProjectiveResolution.isoLeftDerivedObj_inv_naturality
    {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y)
    (φ : P.complex ⟶ Q.complex) (comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f)
    (F : C ⥤ D) [F.Additive] (n : ℕ) :
    (P.isoLeftDerivedObj F n).inv ≫ (F.leftDerived n).map f =
        (F.mapHomologicalComplex _ ⋙ HomologicalComplex.homologyFunctor _ _ n).map φ ≫
          (Q.isoLeftDerivedObj F n).inv

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (P.isoLeftDerivedObj F n).inv ≫ (F.leftDerived n).map f =
    (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
        φ ≫
      (Q.isoLeftDerivedObj F n).inv

Tactic:
rw [← cancel_mono (Q.isoLeftDerivedObj F n).hom, assoc, assoc,
  ProjectiveResolution.isoLeftDerivedObj_hom_naturality f P Q φ comm F n,
  Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem inl_mul_eq_smul [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M]
    (r : R) (x : tsze R M) :
    inl r * x = r •> x :=
  ext rfl (by dsimp; rw [smul_zero, add_zero])

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
r : R
x : tsze R M
⊢ r •> x.snd + 0 <• x.fst = r •> x.snd

Tactic:
rw [smul_zero, add_zero]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
r : R
x : tsze R M
⊢ (inl r * x).snd = (r •> x).snd

Tactic:
dsimp

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
r : R
x : tsze R M
⊢ r •> x.snd + 0 <• x.fst = r •> x.snd
-- Mathlib/.lake/packages/lean4/src/lean/lake/Lake/Util/Name.lean
theorem eq_of_quickCmp {n n' : Name} : n.quickCmp n' = .eq → n = n'

Proof state:
n n' : Name
h_cmp :
  (match compare n.hash n'.hash with
    | Ordering.eq => n.quickCmpAux n'
    | ord => ord) =
    Ordering.eq
⊢ n = n'

Tactic:
split at h_cmp

Result:
case h_1
n n' : Name
x✝ : Ordering
heq✝ : compare n.hash n'.hash = Ordering.eq
h_cmp : n.quickCmpAux n' = Ordering.eq
⊢ n = n'

case h_2
n n' : Name
x✝¹ : Ordering
x✝ : compare n.hash n'.hash = Ordering.eq → False
h_cmp : compare n.hash n'.hash = Ordering.eq
⊢ n = n'

Proof state:
n n' : Name
⊢ n.quickCmp n' = Ordering.eq → n = n'

Tactic:
unfold Name.quickCmp

Result:
n n' : Name
⊢ (match compare n.hash n'.hash with
      | Ordering.eq => n.quickCmpAux n'
      | ord => ord) =
      Ordering.eq →
    n = n'

Proof state:
n n' : Name
x✝¹ : Ordering
x✝ : compare n.hash n'.hash = Ordering.eq → False
h_cmp : compare n.hash n'.hash = Ordering.eq
⊢ n = n'

Tactic:
contradiction

Result:
no goals

Proof state:
n n' : Name
⊢ (match compare n.hash n'.hash with
      | Ordering.eq => n.quickCmpAux n'
      | ord => ord) =
      Ordering.eq →
    n = n'

Tactic:
intro h_cmp

Result:
n n' : Name
h_cmp :
  (match compare n.hash n'.hash with
    | Ordering.eq => n.quickCmpAux n'
    | ord => ord) =
    Ordering.eq
⊢ n = n'

Proof state:
case h_2
n n' : Name
x✝¹ : Ordering
x✝ : compare n.hash n'.hash = Ordering.eq → False
h_cmp : compare n.hash n'.hash = Ordering.eq
⊢ n = n'

Tactic:
next => contradiction

Result:
no goals

Proof state:
case h_1
n n' : Name
x✝ : Ordering
heq✝ : compare n.hash n'.hash = Ordering.eq
h_cmp : n.quickCmpAux n' = Ordering.eq
⊢ n = n'

case h_2
n n' : Name
x✝¹ : Ordering
x✝ : compare n.hash n'.hash = Ordering.eq → False
h_cmp : compare n.hash n'.hash = Ordering.eq
⊢ n = n'

Tactic:
next => exact eq_of_cmp h_cmp

Result:
case h_2
n n' : Name
x✝¹ : Ordering
x✝ : compare n.hash n'.hash = Ordering.eq → False
h_cmp : compare n.hash n'.hash = Ordering.eq
⊢ n = n'

Proof state:
n n' : Name
x✝ : Ordering
heq✝ : compare n.hash n'.hash = Ordering.eq
h_cmp : n.quickCmpAux n' = Ordering.eq
⊢ n = n'

Tactic:
exact eq_of_cmp h_cmp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_X_pow_eq_natCast_mul (n k : ℕ) :
    derivative^[k] (X ^ n : R[X]) = ↑(Nat.descFactorial n k : R[X]) * X ^ (n - k)

Proof state:
case succ
R : Type u
inst✝ : CommSemiring R
n k : ℕ
ih : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)
⊢ (⇑derivative)^[k + 1] (X ^ n) = ↑(n.descFactorial (k + 1)) * X ^ (n - (k + 1))

Tactic:
rw [Function.iterate_succ_apply', ih, derivative_natCast_mul, derivative_X_pow, C_eq_natCast,
  Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul]

Result:
case succ
R : Type u
inst✝ : CommSemiring R
n k : ℕ
ih : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)
⊢ ↑(n.descFactorial k) * (↑(n - k) * X ^ (n - (k + 1))) = ↑(n - k) * ↑(n.descFactorial k) * X ^ (n - (k + 1))

Proof state:
R : Type u
inst✝ : CommSemiring R
n k : ℕ
⊢ (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)

Tactic:
induction k with
| zero =>
  rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
| succ k ih =>
  rw [Function.iterate_succ_apply', ih, derivative_natCast_mul, derivative_X_pow, C_eq_natCast,
    Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul]
  simp [mul_comm, mul_assoc, mul_left_comm]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ (⇑derivative)^[0] (X ^ n) = ↑(n.descFactorial 0) * X ^ (n - 0)

Tactic:
rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : CommSemiring R
n k : ℕ
ih : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)
⊢ ↑(n.descFactorial k) * (↑(n - k) * X ^ (n - (k + 1))) = ↑(n - k) * ↑(n.descFactorial k) * X ^ (n - (k + 1))

Tactic:
simp [mul_comm, mul_assoc, mul_left_comm]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
lemma isZero_extend_X (i' : ι') (hi' : ∀ i, e.f i ≠ i') :
    IsZero ((K.extend e).X i') :=
  K.isZero_extend_X' e i' (by
    obtain hi'|⟨i, hi⟩ := (e.r i').eq_none_or_eq_some
    · exact hi'
    · exfalso
      exact hi' _ (e.f_eq_of_r_eq_some hi))

Proof state:
case inr.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
hi : e.r i' = some i
⊢ e.r i' = none

Tactic:
exfalso

Result:
case inr.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
hi : e.r i' = some i
⊢ False

Proof state:
case inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi'✝ : ∀ (i : ι), e.f i ≠ i'
hi' : e.r i' = none
⊢ e.r i' = none

Tactic:
exact hi'

Result:
no goals

Proof state:
case inr.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
hi : e.r i' = some i
⊢ False

Tactic:
exact hi' _ (e.f_eq_of_r_eq_some hi)

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ e.r i' = none

Tactic:
obtain hi'|⟨i, hi⟩ := (e.r i').eq_none_or_eq_some

Result:
case inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi'✝ : ∀ (i : ι), e.f i ≠ i'
hi' : e.r i' = none
⊢ e.r i' = none

case inr.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
hi : e.r i' = some i
⊢ e.r i' = none
-- Mathlib/Algebra/Ring/Divisibility/Basic.lean
theorem dvd_neg : a ∣ -b ↔ a ∣ b :=
  (Equiv.neg _).exists_congr_left.trans <| by
    simp only [Equiv.neg_symm, Equiv.neg_apply, mul_neg, neg_inj, Dvd.dvd]

Proof state:
α : Type u_1
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b : α
⊢ (∃ b_1, -b = a * (Equiv.symm (Equiv.neg α)) b_1) ↔ a ∣ b

Tactic:
simp only [Equiv.neg_symm, Equiv.neg_apply, mul_neg, neg_inj, Dvd.dvd]

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem upperSemicontinuousAt_sum {f : ι → α → γ} {a : Finset ι}
    (ha : ∀ i ∈ a, UpperSemicontinuousAt (f i) x) :
    UpperSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
x : α
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, UpperSemicontinuousAt (f i) x
⊢ UpperSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x

Tactic:
simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *

Result:
α : Type u_1
inst✝⁴ : TopologicalSpace α
x : α
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) univ x
⊢ UpperSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) univ x

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
x : α
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) univ x
⊢ UpperSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) univ x

Tactic:
exact upperSemicontinuousWithinAt_sum ha

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem smul (μ : Measure α) [OuterRegular μ] {x : ℝ≥0∞} (hx : x ≠ ∞) :
    (x • μ).OuterRegular

Proof state:
case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ⊤
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > (x • μ) A
⊢ ∃ U ⊇ A, IsOpen U ∧ (x • μ) U < r

Tactic:
rw [smul_apply, A.measure_eq_iInf_isOpen, smul_eq_mul] at hr

Result:
case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ⊤
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > x * ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen U), μ U
⊢ ∃ U ⊇ A, IsOpen U ∧ (x • μ) U < r

Proof state:
case inl
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
hx : 0 ≠ ⊤
⊢ OuterRegular 0

Tactic:
exact OuterRegular.zero

Result:
no goals

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ⊤
⊢ (x • μ).OuterRegular

Tactic:
rcases eq_or_ne x 0 with (rfl | h0)

Result:
case inl
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
hx : 0 ≠ ⊤
⊢ (0 • μ).OuterRegular

case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ⊤
h0 : x ≠ 0
⊢ (x • μ).OuterRegular

Proof state:
case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ⊤
h0 : x ≠ 0
⊢ (x • μ).OuterRegular

Tactic:
refine ⟨fun A _ r hr => ?_⟩

Result:
case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ⊤
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > (x • μ) A
⊢ ∃ U ⊇ A, IsOpen U ∧ (x • μ) U < r

Proof state:
case inl
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
hx : 0 ≠ ⊤
⊢ (0 • μ).OuterRegular

Tactic:
rw [zero_smul]

Result:
case inl
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
hx : 0 ≠ ⊤
⊢ OuterRegular 0

Proof state:
case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ⊤
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > x * ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen U), μ U
⊢ ∃ U ⊇ A, IsOpen U ∧ (x • μ) U < r

Tactic:
simpa only [ENNReal.mul_iInf_of_ne h0 hx, gt_iff_lt, iInf_lt_iff, exists_prop] using hr

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem disjoint_union_right (x y z : Finmap β) :
    Disjoint x (y ∪ z) ↔ Disjoint x y ∧ Disjoint x z

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y z : Finmap β
⊢ x.Disjoint (y ∪ z) ↔ x.Disjoint y ∧ x.Disjoint z

Tactic:
rw [Disjoint.symm_iff, disjoint_union_left, Disjoint.symm_iff _ x, Disjoint.symm_iff _ x]

Result:
no goals
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem tendsto_indicator_ge (f : α → β) (x : α) :
    Tendsto (fun M : ℕ => { x | (M : ℝ) ≤ ‖f x‖₊ }.indicator f x) atTop (𝓝 0)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ ↑⌈↑‖f x‖₊⌉₊ < ↑n

Tactic:
refine lt_of_lt_of_le (lt_add_one _) ?_

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ ↑⌈↑‖f x‖₊⌉₊ + 1 ≤ ↑n

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
⊢ Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)

Tactic:
refine tendsto_atTop_of_eventually_const (i₀ := Nat.ceil (‖f x‖₊ : ℝ) + 1) fun n hn => ?_

Result:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ {x | ↑n ≤ ↑‖f x‖₊}.indicator f x = 0

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ x ∉ {x | ↑n ≤ ↑‖f x‖₊}

Tactic:
simp only [not_le, Set.mem_setOf_eq]

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ ↑‖f x‖₊ < ↑n

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ {x | ↑n ≤ ↑‖f x‖₊}.indicator f x = 0

Tactic:
rw [Set.indicator_of_not_mem]

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ x ∉ {x | ↑n ≤ ↑‖f x‖₊}

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ ↑‖f x‖₊ < ↑n

Tactic:
refine lt_of_le_of_lt (Nat.le_ceil _) ?_

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ ↑⌈↑‖f x‖₊⌉₊ < ↑n

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ ↑⌈↑‖f x‖₊⌉₊ + 1 ≤ ↑n

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Expand.lean
theorem rename_comp_expand (f : σ → τ) (p : ℕ) :
    (rename f).comp (expand p) =
      (expand p).comp (rename f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R)

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : σ → τ
p : ℕ
⊢ (rename f).comp (expand p) = (expand p).comp (rename f)

Tactic:
ext1 φ

Result:
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : σ → τ
p : ℕ
φ : σ
⊢ ((rename f).comp (expand p)) (X φ) = ((expand p).comp (rename f)) (X φ)

Proof state:
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : σ → τ
p : ℕ
φ : σ
⊢ ((rename f).comp (expand p)) (X φ) = ((expand p).comp (rename f)) (X φ)

Tactic:
simp only [rename_expand, AlgHom.comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem or_zero (x : Nat) : x ||| 0 = x

Proof state:
x : Nat
⊢ (if x = 0 then if (false || true) = true then 0 else 0
    else
      if 0 = 0 then if (true || false) = true then x else 0
      else
        let n' := x / 2;
        let m' := 0 / 2;
        let b₁ := x % 2 = 1;
        let b₂ := 0 % 2 = 1;
        let r := bitwise or n' m';
        if (decide b₁ || decide b₂) = true then r + r + 1 else r + r) =
    x

Tactic:
simp [@eq_comm _ 0]

Result:
no goals

Proof state:
x : Nat
⊢ bitwise or x 0 = x

Tactic:
unfold bitwise

Result:
x : Nat
⊢ (if x = 0 then if (false || true) = true then 0 else 0
    else
      if 0 = 0 then if (true || false) = true then x else 0
      else
        let n' := x / 2;
        let m' := 0 / 2;
        let b₁ := x % 2 = 1;
        let b₂ := 0 % 2 = 1;
        let r := bitwise or n' m';
        if (decide b₁ || decide b₂) = true then r + r + 1 else r + r) =
    x

Proof state:
x : Nat
⊢ x ||| 0 = x

Tactic:
simp only [HOr.hOr, OrOp.or, lor]

Result:
x : Nat
⊢ bitwise or x 0 = x
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem ceil_lt_mul {x : ℝ} (hx : 50 / 19 ≤ x) : (⌈x⌉₊ : ℝ) < 1.38 * x

Proof state:
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 0 < 50 / 19

Tactic:
norm_num1

Result:
no goals

Proof state:
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 69 / 50 - 1 = (50 / 19)⁻¹

Tactic:
norm_num1

Result:
no goals

Proof state:
x : ℝ
hx : 50 / 19 ≤ x
⊢ 1 ≤ (1.38 - 1) * x

Tactic:
have : (1.38 : ℝ) = 69 / 50 := by norm_num

Result:
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 1 ≤ (1.38 - 1) * x

Proof state:
x : ℝ
hx : 50 / 19 ≤ x
⊢ 1.38 = 69 / 50

Tactic:
norm_num

Result:
no goals

Proof state:
x : ℝ
hx : 50 / 19 ≤ x
⊢ 0 ≤ 50 / 19

Tactic:
norm_num

Result:
no goals

Proof state:
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 1 ≤ (1.38 - 1) * x

Tactic:
rwa [this, show (69 / 50 - 1 : ℝ) = (50 / 19)⁻¹ by norm_num1, ←
  div_eq_inv_mul, one_le_div]

Result:
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 0 < 50 / 19

Proof state:
x : ℝ
hx : 50 / 19 ≤ x
⊢ x + 1 ≤ 1.38 * x

Tactic:
rw [← le_sub_iff_add_le', ← sub_one_mul]

Result:
x : ℝ
hx : 50 / 19 ≤ x
⊢ 1 ≤ (1.38 - 1) * x

Proof state:
x : ℝ
hx : 50 / 19 ≤ x
⊢ ↑⌈x⌉₊ < 1.38 * x

Tactic:
refine (ceil_lt_add_one <| hx.trans' <| by norm_num).trans_le ?_

Result:
x : ℝ
hx : 50 / 19 ≤ x
⊢ x + 1 ≤ 1.38 * x