harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Hom/Basic.lean
theorem Disjoint.map_orderIso [SemilatticeInf α] [OrderBot α] [SemilatticeInf β] [OrderBot β]
    {a b : α} (f : α ≃o β) (ha : Disjoint a b) : Disjoint (f a) (f b)

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ Disjoint (f a) (f b)

Tactic:
rw [disjoint_iff_inf_le, ← f.map_inf, ← f.map_bot]

Result:
α : Type u_2
β : Type u_3
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ f (a ⊓ b) ≤ f ⊥

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ f (a ⊓ b) ≤ f ⊥

Tactic:
exact f.monotone ha.le_bot

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_eq (x : ℝ) : cosh x = (exp x + exp (-x)) / 2 :=
  eq_div_of_mul_eq two_ne_zero <| by
    rw [cosh, exp, exp, Complex.ofReal_neg, Complex.cosh, mul_two, ← Complex.add_re, ← mul_two,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), Complex.add_re]

Proof state:
x : ℝ
⊢ cosh x * 2 = rexp x + rexp (-x)

Tactic:
rw [cosh, exp, exp, Complex.ofReal_neg, Complex.cosh, mul_two, ← Complex.add_re, ← mul_two,
  div_mul_cancel₀ _ (two_ne_zero' ℂ), Complex.add_re]

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem chain'_pair {x y} : Chain' R [x, y] ↔ R x y

Proof state:
α : Type u
R : α → α → Prop
x y : α
⊢ Chain' R [x, y] ↔ R x y

Tactic:
simp only [chain'_singleton, chain'_cons, and_true]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem map_id {n : ℕ} (v : Vector α n) : Vector.map id v = v :=
  Vector.eq _ _ (by simp only [List.map_id, Vector.toList_map])

Proof state:
α : Type u_1
n : ℕ
v : Vector α n
⊢ (map id v).toList = v.toList

Tactic:
simp only [List.map_id, Vector.toList_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modifyHead_eq_nil_iff {f : α → α} {l : List α} :
    l.modifyHead f = [] ↔ l = []

Proof state:
α : Type u_1
f : α → α
l : List α
⊢ modifyHead f l = [] ↔ l = []

Tactic:
cases l <;> simp [modifyHead]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma lintegral_condKernel_mem (a : α) {s : Set (β × Ω)} (hs : MeasurableSet s) :
    ∫⁻ x, Kernel.condKernel κ (a, x) {y | (x, y) ∈ s} ∂(Kernel.fst κ a) = κ a s

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), (κ.condKernel (a, x)) {y | (x, y) ∈ s} ∂κ.fst a = ((κ.fst ⊗ₖ κ.condKernel) a) s

Tactic:
simp_rw [Kernel.compProd_apply hs]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), (κ.condKernel (a, x)) {y | (x, y) ∈ s} ∂κ.fst a = (κ a) s

Tactic:
conv_rhs => rw [← κ.disintegrate κ.condKernel]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), (κ.condKernel (a, x)) {y | (x, y) ∈ s} ∂κ.fst a = ((κ.fst ⊗ₖ κ.condKernel) a) s
-- Mathlib/RingTheory/Ideal/IsPrimary.lean
/-- A proper ideal `I` is primary iff `xy ∈ I` implies `x ∈ I` or `y ∈ radical I`. -/
lemma isPrimary_iff {I : Ideal R} :
    I.IsPrimary ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ radical I

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ (I ≠ ⊤ ∧ ∀ (b a : R), a • b ∈ I → b ∈ I ∨ ∃ n, a ^ n • ⊤ ≤ I) ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical

Tactic:
simp only [mul_comm, mem_radical_iff, and_congr_right_iff,
  ← Submodule.ideal_span_singleton_smul, smul_eq_mul, mul_top, span_singleton_le_iff_mem]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.IsPrimary ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical

Tactic:
rw [IsPrimary, Submodule.IsPrimary, forall_comm]

Result:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ (I ≠ ⊤ ∧ ∀ (b a : R), a • b ∈ I → b ∈ I ∨ ∃ n, a ^ n • ⊤ ≤ I) ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
-- Mathlib/Algebra/Order/Field/Defs.lean
/-- Equality holds when `a ≠ 0`. See `mul_inv_cancel_left`. -/
lemma le_mul_inv_left (hb : b ≤ 0) : b ≤ a * (a⁻¹ * b)

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
hb : b ≤ 0
⊢ b ≤ a * (a⁻¹ * b)

Tactic:
obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

Result:
no goals
-- Mathlib/Data/Nat/ChineseRemainder.lean
theorem chineseRemainderOfMultiset_lt_prod {m : Multiset ι}
    (nod : m.Nodup) (hs : ∀ i ∈ m, s i ≠ 0) (pp : Set.Pairwise {x | x ∈ m} (Coprime on s)) :
    chineseRemainderOfMultiset a s nod hs pp < (m.map s).prod

Proof state:
ι : Type u_1
a s : ι → ℕ
m : Multiset ι
nod : m.Nodup
hs : ∀ i ∈ m, s i ≠ 0
pp : {x | x ∈ m}.Pairwise (Coprime on s)
⊢ ↑(chineseRemainderOfMultiset a s nod hs pp) < (Multiset.map s m).prod

Tactic:
induction' m using Quot.ind with l

Result:
case mk
ι : Type u_1
a s : ι → ℕ
l : List ι
nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, s i ≠ 0
pp : {x | x ∈ Quot.mk (⇑(List.isSetoid ι)) l}.Pairwise (Coprime on s)
⊢ ↑(chineseRemainderOfMultiset a s nod hs pp) < (Multiset.map s (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Proof state:
case mk
ι : Type u_1
a s : ι → ℕ
l : List ι
nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, s i ≠ 0
pp : {x | x ∈ Quot.mk (⇑(List.isSetoid ι)) l}.Pairwise (Coprime on s)
⊢ ↑(chineseRemainderOfMultiset a s nod hs pp) < (Multiset.map s (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Tactic:
unfold chineseRemainderOfMultiset

Result:
case mk
ι : Type u_1
a s : ι → ℕ
l : List ι
nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, s i ≠ 0
pp : {x | x ∈ Quot.mk (⇑(List.isSetoid ι)) l}.Pairwise (Coprime on s)
⊢ ↑(Quotient.recOn (motive := fun x =>
        x.Nodup → (∀ i ∈ x, s i ≠ 0) → {x_1 | x_1 ∈ x}.Pairwise (Coprime on s) → { k // ∀ i ∈ x, k ≡ a i [MOD s i] })
        (Quot.mk (⇑(List.isSetoid ι)) l) (fun l nod x co => chineseRemainderOfList a s l ⋯) ⋯ nod hs pp) <
    (Multiset.map s (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Proof state:
case mk
ι : Type u_1
a s : ι → ℕ
l : List ι
nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, s i ≠ 0
pp : {x | x ∈ Quot.mk (⇑(List.isSetoid ι)) l}.Pairwise (Coprime on s)
⊢ ↑(Quotient.recOn (motive := fun x =>
        x.Nodup → (∀ i ∈ x, s i ≠ 0) → {x_1 | x_1 ∈ x}.Pairwise (Coprime on s) → { k // ∀ i ∈ x, k ≡ a i [MOD s i] })
        (Quot.mk (⇑(List.isSetoid ι)) l) (fun l nod x co => chineseRemainderOfList a s l ⋯) ⋯ nod hs pp) <
    (Multiset.map s (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Tactic:
simpa using chineseRemainderOfList_lt_prod a s l
  (List.Nodup.pairwise_of_forall_ne nod pp) (by simpa using hs)

Result:
no goals

Proof state:
ι : Type u_1
a s : ι → ℕ
l : List ι
nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, s i ≠ 0
pp : {x | x ∈ Quot.mk (⇑(List.isSetoid ι)) l}.Pairwise (Coprime on s)
⊢ ∀ i ∈ l, s i ≠ 0

Tactic:
simpa using hs

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
theorem sat_iff_forall [Clause α β] [Entails α σ] [Formula α β σ] (p : α → Bool) (f : σ) :
    p ⊨ f ↔ ∀ c : β, c ∈ toList f → p ⊨ c

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
p : α → Bool
f : σ
⊢ ((toList f).all fun c => decide (eval p c = true)) = true ↔ ∀ (c : β), c ∈ toList f → eval p c = true

Tactic:
simp only [List.all_eq_true, decide_eq_true_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorAdd_zero_add_inv_app (a : A) (X : C) : (shiftFunctorAdd C 0 a).inv.app X =
    ((shiftFunctorZero C A).hom.app X)⟦a⟧' ≫ eqToHom (by dsimp; rw [zero_add])

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C a).obj ((𝟭 C).obj X) = (shiftFunctor C (0 + a)).obj X

Tactic:
dsimp

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C a).obj X = (shiftFunctor C (0 + a)).obj X

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C a).obj X = (shiftFunctor C (0 + a)).obj X

Tactic:
rw [zero_add]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd C 0 a).inv.app X = (shiftFunctor C a).map ((shiftFunctorZero C A).hom.app X) ≫ eqToHom ⋯

Tactic:
simp [← shiftFunctorAdd'_zero_add_inv_app, shiftFunctorAdd']

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_neg_left (x y : V) : (o.oangle (-x) y).sign = -(o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

Tactic:
by_cases hx : x = 0

Result:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x = 0
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

Tactic:
rw [o.oangle_neg_left hx hy, Real.Angle.sign_add_pi]

Result:
no goals

Proof state:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : y = 0
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

Tactic:
simp [hy]

Result:
no goals

Proof state:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x = 0
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

Tactic:
simp [hx]

Result:
no goals

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

Tactic:
by_cases hy : y = 0

Result:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : y = 0
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign
-- Mathlib/Data/Set/NAry.lean
theorem image2_eq_empty_iff : image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ ¬s.Nonempty ∨ ¬t.Nonempty ↔ s = ∅ ∨ t = ∅

Tactic:
simp [not_nonempty_iff_eq_empty]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
rw [← not_nonempty_iff_eq_empty, image2_nonempty_iff, not_and_or]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ ¬s.Nonempty ∨ ¬t.Nonempty ↔ s = ∅ ∨ t = ∅
-- Mathlib/Data/ENNReal/Action.lean
lemma nnreal_smul_ne_top_iff {x : ℝ≥0} {y : ℝ≥0∞} (hx : x ≠ 0) : x • y ≠ ⊤ ↔ y ≠ ⊤ :=
  ⟨by rintro h rfl; simp [smul_top, hx] at h, nnreal_smul_ne_top⟩

Proof state:
x : ℝ≥0
hx : x ≠ 0
h : x • ⊤ ≠ ⊤
⊢ False

Tactic:
simp [smul_top, hx] at h

Result:
no goals

Proof state:
x : ℝ≥0
y : ℝ≥0∞
hx : x ≠ 0
⊢ x • y ≠ ⊤ → y ≠ ⊤

Tactic:
rintro h rfl

Result:
x : ℝ≥0
hx : x ≠ 0
h : x • ⊤ ≠ ⊤
⊢ False
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
lemma natDegree_eq_zero {p : R[X]} : p.natDegree = 0 ↔ ∃ x, C x = p :=
  ⟨fun h ↦ ⟨_, (eq_C_of_natDegree_eq_zero h).symm⟩, by aesop⟩

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (∃ x, C x = p) → p.natDegree = 0

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem IsVonNBounded.sub (hs : IsVonNBounded 𝕜 s) (ht : IsVonNBounded 𝕜 t) :
    IsVonNBounded 𝕜 (s - t)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddGroup E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : DistribMulAction 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
⊢ IsVonNBounded 𝕜 (s - t)

Tactic:
rw [sub_eq_add_neg]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddGroup E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : DistribMulAction 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
⊢ IsVonNBounded 𝕜 (s + -t)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddGroup E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : DistribMulAction 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
⊢ IsVonNBounded 𝕜 (s + -t)

Tactic:
exact hs.add ht.neg

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem norm_integral_le_of_norm_le_const' {f : ℂ → E} {c : ℂ} {R C : ℝ}
    (hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C) : ‖∮ z in C(c, R), f z‖ ≤ 2 * π * |R| * C :=
  calc
    ‖∮ z in C(c, R), f z‖ ≤ |R| * C * |2 * π - 0| :=
      intervalIntegral.norm_integral_le_of_norm_le_const fun θ _ =>
        calc
          ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ = |R| * ‖f (circleMap c R θ)‖

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
⊢ ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ = |R| * ‖f (circleMap c R θ)‖

Tactic:
simp [norm_smul]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
⊢ |R| * C * |2 * π - 0| = 2 * π * |R| * C

Tactic:
rw [sub_zero, _root_.abs_of_pos Real.two_pi_pos]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
⊢ |R| * C * (2 * π) = 2 * π * |R| * C

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
⊢ |R| * C * (2 * π) = 2 * π * |R| * C

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_of_ne_of_mem {a y : α} {l : Array α} (h₁ : a ≠ y) (h₂ : a ∈ l.push y) : a ∈ l

Proof state:
α : Type u_1
a y : α
l : Array α
h₁ : a ≠ y
h₂ : a ∈ l.push y
⊢ a ∈ l

Tactic:
simpa [h₁] using h₂

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem contained_eq_proj (o : Ordinal) (h : contained C o) :
    C = π C (ord I · < o)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
h : contained C o
this : (∀ (i : I), ∀ x ∈ C, x i ≠ false → ord I i < o) → (π C fun x => ord I x < o) = C
⊢ C = π C fun x => ord I x < o

Tactic:
simp only [ne_eq, Bool.not_eq_false, π] at this

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
h : contained C o
this : (∀ (i : I), ∀ x ∈ C, x i = true → ord I i < o) → (Proj fun x => ord I x < o) '' C = C
⊢ C = π C fun x => ord I x < o

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
h : contained C o
this : (∀ (i : I), ∀ x ∈ C, x i = true → ord I i < o) → (Proj fun x => ord I x < o) '' C = C
⊢ C = π C fun x => ord I x < o

Tactic:
exact (this (fun i x hx ↦ h x hx i)).symm

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem prev_cons_cons_eq' (y z : α) (h : x ∈ y :: z :: l) (hx : x = y) :
    prev (y :: z :: l) x h = getLast (z :: l) (cons_ne_nil _ _)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ (y :: z :: l).prev x h = (z :: l).getLast ⋯

Tactic:
rw [prev, dif_pos hx]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/OpenPos.lean
theorem _root_.Continuous.isOpenPosMeasure_map [OpensMeasurableSpace X]
    {Z : Type*} [TopologicalSpace Z] [MeasurableSpace Z] [BorelSpace Z]
    {f : X → Z} (hf : Continuous f) (hf_surj : Function.Surjective f) :
    (Measure.map f μ).IsOpenPosMeasure

Proof state:
X : Type u_1
inst✝⁵ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝⁴ : μ.IsOpenPosMeasure
inst✝³ : OpensMeasurableSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
inst✝¹ : MeasurableSpace Z
inst✝ : BorelSpace Z
f : X → Z
hf : Continuous f
hf_surj : Surjective f
⊢ (map f μ).IsOpenPosMeasure

Tactic:
refine ⟨fun U hUo hUne => ?_⟩

Result:
X : Type u_1
inst✝⁵ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝⁴ : μ.IsOpenPosMeasure
inst✝³ : OpensMeasurableSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
inst✝¹ : MeasurableSpace Z
inst✝ : BorelSpace Z
f : X → Z
hf : Continuous f
hf_surj : Surjective f
U : Set Z
hUo : IsOpen U
hUne : U.Nonempty
⊢ (map f μ) U ≠ 0

Proof state:
X : Type u_1
inst✝⁵ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝⁴ : μ.IsOpenPosMeasure
inst✝³ : OpensMeasurableSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
inst✝¹ : MeasurableSpace Z
inst✝ : BorelSpace Z
f : X → Z
hf : Continuous f
hf_surj : Surjective f
U : Set Z
hUo : IsOpen U
hUne : U.Nonempty
⊢ (map f μ) U ≠ 0

Tactic:
rw [Measure.map_apply hf.measurable hUo.measurableSet]

Result:
X : Type u_1
inst✝⁵ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝⁴ : μ.IsOpenPosMeasure
inst✝³ : OpensMeasurableSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
inst✝¹ : MeasurableSpace Z
inst✝ : BorelSpace Z
f : X → Z
hf : Continuous f
hf_surj : Surjective f
U : Set Z
hUo : IsOpen U
hUne : U.Nonempty
⊢ μ (f ⁻¹' U) ≠ 0

Proof state:
X : Type u_1
inst✝⁵ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝⁴ : μ.IsOpenPosMeasure
inst✝³ : OpensMeasurableSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
inst✝¹ : MeasurableSpace Z
inst✝ : BorelSpace Z
f : X → Z
hf : Continuous f
hf_surj : Surjective f
U : Set Z
hUo : IsOpen U
hUne : U.Nonempty
⊢ μ (f ⁻¹' U) ≠ 0

Tactic:
exact (hUo.preimage hf).measure_ne_zero μ (hf_surj.nonempty_preimage.mpr hUne)

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
lemma UniformEquicontinuousOn.mono {F : ι → β → α} {S T : Set β}
    (H : UniformEquicontinuousOn F T) (hST : S ⊆ T) : UniformEquicontinuousOn F S :=
  fun U hU ↦ (H U hU).filter_mono <| by gcongr

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S T : Set β
H : UniformEquicontinuousOn F T
hST : S ⊆ T
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ 𝓤 β ⊓ 𝓟 (S ×ˢ S) ≤ 𝓤 β ⊓ 𝓟 (T ×ˢ T)

Tactic:
gcongr

Result:
no goals
-- Mathlib/RingTheory/AlgebraTower.lean
theorem Basis.smulTower'_repr (x ij) :
    (b.smulTower' c).repr x ij = b.repr (c.repr x ij.1) ij.2

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
x : A
ij : ι' × ι
⊢ (b.repr ((c.repr x) ((Equiv.prodComm ι ι').symm ij).2)) ((Equiv.prodComm ι ι').symm ij).1 =
    (b.repr ((c.repr x) ij.1)) ij.2

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
x : A
ij : ι' × ι
⊢ ((b.smulTower' c).repr x) ij = (b.repr ((c.repr x) ij.1)) ij.2

Tactic:
rw [smulTower', repr_reindex_apply, smulTower_repr]

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
x : A
ij : ι' × ι
⊢ (b.repr ((c.repr x) ((Equiv.prodComm ι ι').symm ij).2)) ((Equiv.prodComm ι ι').symm ij).1 =
    (b.repr ((c.repr x) ij.1)) ij.2
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSub_weightedVSubVSubWeights [DecidableEq ι] (p : ι → P) {i j : ι} (hi : i ∈ s)
    (hj : j ∈ s) : s.weightedVSub p (weightedVSubVSubWeights k i j) = p i -ᵥ p j

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
p : ι → P
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ (s.weightedVSub p) (weightedVSubVSubWeights k i j) = p i -ᵥ p j

Tactic:
rw [weightedVSubVSubWeights, ← affineCombination_vsub,
  s.affineCombination_affineCombinationSingleWeights k p hi,
  s.affineCombination_affineCombinationSingleWeights k p hj]

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Basic.lean
theorem neg_def (r : X) (s : S) : -(r /ₒ s) = -r /ₒ s

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
r : X
s : ↥S
⊢ -(r /ₒ s) = -r /ₒ s

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
r : X
s : ↥S
⊢ -(r /ₒ s) = -r /ₒ s

Tactic:
with_unfolding_all rfl

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
lemma map_sups (f : F) (hf) (s t : Finset α) :
    map ⟨f, hf⟩ (s ⊻ t) = map ⟨f, hf⟩ s ⊻ map ⟨f, hf⟩ t

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq β
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
hf : Injective ⇑f
s t : Finset α
⊢ map { toFun := ⇑f, inj' := hf } (s ⊻ t) = map { toFun := ⇑f, inj' := hf } s ⊻ map { toFun := ⇑f, inj' := hf } t

Tactic:
simpa [map_eq_image] using image_sups f s t

Result:
no goals