harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MonoidAlgebra/Support.lean
theorem support_mul_single [Mul G] [IsRightCancelMul G] (f : MonoidAlgebra k G) (r : k)
    (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
    (f * single x r).support = f.support.map (mulRightEmbedding x)

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsRightCancelMul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support

Tactic:
classical
  ext
  simp only [support_mul_single_eq_image f hr (IsRightRegular.all x),
    mem_image, mem_map, mulRightEmbedding_apply]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsRightCancelMul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support

Tactic:
ext

Result:
case h
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsRightCancelMul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x a✝ : G
⊢ a✝ ∈ (f * single x r).support ↔ a✝ ∈ map (mulRightEmbedding x) f.support

Proof state:
case h
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsRightCancelMul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x a✝ : G
⊢ a✝ ∈ (f * single x r).support ↔ a✝ ∈ map (mulRightEmbedding x) f.support

Tactic:
simp only [support_mul_single_eq_image f hr (IsRightRegular.all x),
  mem_image, mem_map, mulRightEmbedding_apply]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem terminatedAt_iff_s_terminatedAt : g.TerminatedAt n ↔ g.s.TerminatedAt n

Proof state:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.TerminatedAt n ↔ g.s.TerminatedAt n

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma ext_of_isAffine {X Y : Scheme} [IsAffine Y] {f g : X ⟶ Y} (e : f.appTop = g.appTop) :
    f = g

Proof state:
X Y : Scheme
inst✝ : IsAffine Y
f g : X ⟶ Y
e : Scheme.Hom.appTop f = Scheme.Hom.appTop g
⊢ f = g

Tactic:
rw [← cancel_mono Y.toSpecΓ, Scheme.toSpecΓ_naturality, Scheme.toSpecΓ_naturality, e]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findSome?_eq_none_iff : findSome? p l = none ↔ ∀ x ∈ l, p x = none

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
p : α✝¹ → Option α✝
l : Array α✝¹
⊢ findSome? p l = none ↔ ∀ (x : α✝¹), x ∈ l → p x = none

Tactic:
cases l

Result:
case mk
α✝¹ : Type u_1
α✝ : Type u_2
p : α✝¹ → Option α✝
toList✝ : List α✝¹
⊢ findSome? p { toList := toList✝ } = none ↔ ∀ (x : α✝¹), x ∈ { toList := toList✝ } → p x = none

Proof state:
case mk
α✝¹ : Type u_1
α✝ : Type u_2
p : α✝¹ → Option α✝
toList✝ : List α✝¹
⊢ findSome? p { toList := toList✝ } = none ↔ ∀ (x : α✝¹), x ∈ { toList := toList✝ } → p x = none

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
@[simp, norm_cast] lemma cast_neg (q : ℚ) : ↑(-q) = (-q : α)

Proof state:
α : Type u_3
inst✝ : DivisionRing α
q : ℚ
⊢ ↑(-q) = -↑q

Tactic:
simp [cast_def, neg_div]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem monomial_mul_X (n : ℕ) (r : R) : monomial n r * X = monomial (n + 1) r

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial n) r * X = (monomial (n + 1)) r

Tactic:
rw [X, monomial_mul_monomial, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Relabel.lean
theorem relabel_gate {decls : Array (Decl α)} {r : α → β} {hidx : idx < decls.size}
    (h : relabel r decls[idx] = .gate lhs rhs linv rinv) :
    decls[idx] = (.gate lhs rhs linv rinv : Decl α)

Proof state:
α β : Type
idx lhs rhs : Nat
linv rinv : Bool
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
h : relabel r decls[idx] = gate lhs rhs linv rinv
⊢ decls[idx] = gate lhs rhs linv rinv

Tactic:
unfold relabel at h

Result:
α β : Type
idx lhs rhs : Nat
linv rinv : Bool
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
h :
  (match decls[idx] with
    | const b => const b
    | atom a => atom (r a)
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    gate lhs rhs linv rinv
⊢ decls[idx] = gate lhs rhs linv rinv

Proof state:
α β : Type
idx lhs rhs : Nat
linv rinv : Bool
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
h :
  (match decls[idx] with
    | const b => const b
    | atom a => atom (r a)
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    gate lhs rhs linv rinv
⊢ decls[idx] = gate lhs rhs linv rinv

Tactic:
split at h <;> simp_all

Result:
no goals
-- Mathlib/AlgebraicGeometry/Fiber.lean
lemma Scheme.Hom.finite_preimage (f : X.Hom Y) [IsFinite f] {s : Set Y} (hs : s.Finite) :
    (f.base ⁻¹' s).Finite

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : IsFinite f
s : Set ↑↑Y.toPresheafedSpace
hs : s.Finite
⊢ (⋃ i ∈ s, ⇑(ConcreteCategory.hom f.base) ⁻¹' {i}).Finite

Tactic:
exact hs.biUnion fun _ _ ↦ IsFinite.finite_preimage_singleton f _

Result:
no goals

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : IsFinite f
s : Set ↑↑Y.toPresheafedSpace
hs : s.Finite
⊢ (⇑(ConcreteCategory.hom f.base) ⁻¹' s).Finite

Tactic:
rw [← Set.biUnion_of_singleton s, Set.preimage_iUnion₂]

Result:
X Y : Scheme
f : X.Hom Y
inst✝ : IsFinite f
s : Set ↑↑Y.toPresheafedSpace
hs : s.Finite
⊢ (⋃ i ∈ s, ⇑(ConcreteCategory.hom f.base) ⁻¹' {i}).Finite
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem eraseP_toArray {as : List α} {p : α → Bool} :
    as.toArray.eraseP p = (as.eraseP p).toArray

Proof state:
α : Type u_1
as : List α
p : α → Bool
⊢ as.toArray.eraseP p = (eraseP p as).toArray

Tactic:
rw [Array.eraseP, List.eraseP_eq_eraseIdx, findFinIdx?_toArray]

Result:
α : Type u_1
as : List α
p : α → Bool
⊢ (match findFinIdx? p as with
    | none => as.toArray
    | some i => as.toArray.eraseIdx ↑i ⋯) =
    (match findIdx? p as with
      | none => as
      | some i => as.eraseIdx i).toArray

Proof state:
α : Type u_1
as : List α
p : α → Bool
⊢ (match findFinIdx? p as with
    | none => as.toArray
    | some i => as.toArray.eraseIdx ↑i ⋯) =
    (match findIdx? p as with
      | none => as
      | some i => as.eraseIdx i).toArray

Tactic:
split <;> simp [*, findIdx?_eq_map_findFinIdx?_val]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry_cons_of_beq [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : k == a) :
    getEntry a (⟨k, v⟩ :: l) (containsKey_cons_of_beq (v := v) h) = ⟨k, v⟩

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : (k == a) = true
⊢ getEntry a (⟨k, v⟩ :: l) ⋯ = ⟨k, v⟩

Tactic:
simp [getEntry, getEntry?_cons_of_true h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem pullbackP1Iso_hom_ι (i : 𝒰.J) :
    (pullbackP1Iso 𝒰 f g i).hom ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i =
    pullback.fst _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
⊢ (pullbackP1Iso 𝒰 f g i).hom ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i = pullback.fst (p1 𝒰 f g) (𝒰.map i)

Tactic:
rw [← gluing_ι, ← pullbackP1Iso_inv_fst, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/Logic/IsEmpty.lean
theorem isEmpty_pprod : IsEmpty (PProd α β) ↔ IsEmpty α ∨ IsEmpty β

Proof state:
α : Sort u_1
β : Sort u_2
⊢ IsEmpty (α ×' β) ↔ IsEmpty α ∨ IsEmpty β

Tactic:
simp only [← not_nonempty_iff, nonempty_pprod, not_and_or]

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

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

Tactic:
simp only [nodup_append, not_or, and_left_comm, and_assoc, nodup_cons, mem_append,
  disjoint_cons_right]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean
lemma one_mem_iff {R : Type*} [NonAssocRing R] (I : TwoSidedIdeal R) :
    (1 : R) ∈ I ↔ I = ⊤ :=
  ⟨fun h => eq_top_iff.2 fun x _ => by simpa using I.mul_mem_left x _ h, fun h ↦ h.symm ▸ trivial⟩

Proof state:
R : Type u_2
inst✝ : NonAssocRing R
I : TwoSidedIdeal R
h : 1 ∈ I
x : R
x✝ : x ∈ ⊤
⊢ x ∈ I

Tactic:
simpa using I.mul_mem_left x _ h

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonUnitalRing_injective :
    Function.Injective (@toNonUnitalRing R)

Proof state:
R : Type u
⊢ Function.Injective (@toNonUnitalRing R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Result:
case mk.mk
R : Type u
toNonUnitalRing✝¹ : NonUnitalRing R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalRing✝ : NonUnitalRing R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : toNonUnitalRing = toNonUnitalRing
⊢ mk mul_comm✝¹ = mk mul_comm✝

Proof state:
case mk.mk
R : Type u
toNonUnitalRing✝¹ : NonUnitalRing R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalRing✝ : NonUnitalRing R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : toNonUnitalRing = toNonUnitalRing
⊢ mk mul_comm✝¹ = mk mul_comm✝

Tactic:
congr

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem lt_rpow_inv_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
    x < y ^ z⁻¹ ↔ y < x ^ z

Proof state:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x < y ^ z⁻¹ ↔ y < x ^ z

Tactic:
rw [← rpow_lt_rpow_iff_of_neg _ hx hz, rpow_inv_rpow _ hz.ne] <;> positivity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_map (f : β → α) (l : Array β) : findIdx? p (l.map f) = l.findIdx? (p ∘ f)

Proof state:
case mk
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : List β
⊢ findIdx? p (map f { toList := l }) = findIdx? (p ∘ f) { toList := l }

Tactic:
simp [List.findIdx?_map]

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : Array β
⊢ findIdx? p (map f l) = findIdx? (p ∘ f) l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : List β
⊢ findIdx? p (map f { toList := l }) = findIdx? (p ∘ f) { toList := l }
-- Mathlib/Geometry/Manifold/VectorField.lean
@[simp] lemma mlieBracket_self : mlieBracket I V V = 0

Proof state:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
V : (x : M) → TangentSpace I x
x : M
⊢ mlieBracket I V V x = 0 x

Tactic:
simp_rw [mlieBracket, mlieBracketWithin_self, Pi.zero_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
V : (x : M) → TangentSpace I x
⊢ mlieBracket I V V = 0

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
V : (x : M) → TangentSpace I x
x : M
⊢ mlieBracket I V V x = 0 x
-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem mulHom_map_iff (f : G ↪ H) (mul : ∀ x y, f (x * y) = f x * f y) :
    UniqueMul (A.map f) (B.map f) (f a0) (f b0) ↔ UniqueMul A B a0 b0

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), f (x * y) = f x * f y
⊢ UniqueMul (map f A) (map f B) (f a0) (f b0) ↔ UniqueMul A B a0 b0

Tactic:
classical simp_rw [← mulHom_image_iff ⟨f, mul⟩ f.2, Finset.map_eq_image]; rfl

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), f (x * y) = f x * f y
⊢ UniqueMul (map f A) (map f B) (f a0) (f b0) ↔ UniqueMul A B a0 b0

Tactic:
simp_rw [← mulHom_image_iff ⟨f, mul⟩ f.2, Finset.map_eq_image]

Result:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), f (x * y) = f x * f y
⊢ UniqueMul (image (⇑f) A) (image (⇑f) B) (f a0) (f b0) ↔
    UniqueMul (image (⇑{ toFun := ⇑f, map_mul' := mul }) A) (image (⇑{ toFun := ⇑f, map_mul' := mul }) B)
      ({ toFun := ⇑f, map_mul' := mul } a0) ({ toFun := ⇑f, map_mul' := mul } b0)

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), f (x * y) = f x * f y
⊢ UniqueMul (image (⇑f) A) (image (⇑f) B) (f a0) (f b0) ↔
    UniqueMul (image (⇑{ toFun := ⇑f, map_mul' := mul }) A) (image (⇑{ toFun := ⇑f, map_mul' := mul }) B)
      ({ toFun := ⇑f, map_mul' := mul } a0) ({ toFun := ⇑f, map_mul' := mul } b0)

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ioo_eq_zero_iff [DenselyOrdered α] : Ioo a b = 0 ↔ ¬a < b

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DenselyOrdered α
⊢ Ioo a b = 0 ↔ ¬a < b

Tactic:
rw [Ioo, Finset.val_eq_zero, Finset.Ioo_eq_empty_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem finStronglyMeasurable [TopologicalSpace β] [Zero β] {m0 : MeasurableSpace α}
    (hf : StronglyMeasurable f) (μ : Measure α) [SigmaFinite μ] : FinStronglyMeasurable f μ :=
  hf.finStronglyMeasurable_of_set_sigmaFinite MeasurableSet.univ (by simp)
    (by rwa [Measure.restrict_univ])

Proof state:
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
m0 : MeasurableSpace α
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite μ
⊢ ∀ x ∈ univᶜ, f x = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Zero β
m0 : MeasurableSpace α
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite μ
⊢ SigmaFinite (μ.restrict univ)

Tactic:
rwa [Measure.restrict_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_reverseAux {x : α} : ∀ {as bs}, x ∈ reverseAux as bs ↔ x ∈ as ∨ x ∈ bs
  | [], _ => ⟨.inr, fun | .inr h => h⟩
  | a :: _, _ => by rw [reverseAux, mem_cons, or_assoc, or_left_comm, mem_reverseAux, mem_cons]

Proof state:
α : Type u_1
x a : α
tail✝ x✝ : List α
⊢ x ∈ (a :: tail✝).reverseAux x✝ ↔ x ∈ a :: tail✝ ∨ x ∈ x✝

Tactic:
rw [reverseAux, mem_cons, or_assoc, or_left_comm, mem_reverseAux, mem_cons]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma eq_of_mem_uIoc_of_mem_uIoc' : b ∈ Ι a c → c ∈ Ι a b → b = c

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b ∈ Ι a c → c ∈ Ι a b → b = c

Tactic:
simpa only [uIoc_comm a] using eq_of_mem_uIoc_of_mem_uIoc

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem edgeSet_iInf (f : ι → G.Subgraph) :
    (⨅ i, f i).edgeSet = (⋂ i, (f i).edgeSet) ∩ G.edgeSet

Proof state:
ι : Sort u_1
V : Type u
G : SimpleGraph V
f : ι → G.Subgraph
⊢ (⨅ i, f i).edgeSet = (⋂ i, (f i).edgeSet) ∩ G.edgeSet

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem mem_sphere_comm : x ∈ sphere y ε ↔ y ∈ sphere x ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ x ∈ sphere y ε ↔ y ∈ sphere x ε

Tactic:
rw [mem_sphere', mem_sphere]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_insert_left : image2 f (insert a s) t = (fun b => f a b) '' t ∪ image2 f s t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
⊢ image2 f (insert a s) t = (fun b => f a b) '' t ∪ image2 f s t

Tactic:
rw [insert_eq, image2_union_left, image2_singleton_left]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem exists_range_iff {p : α → Prop} : (∃ a ∈ range f, p a) ↔ ∃ i, p (f i)

Proof state:
α : Type u_1
ι : Sort u_4
f : ι → α
p : α → Prop
⊢ (∃ a ∈ range f, p a) ↔ ∃ i, p (f i)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_average_le_pos (hμ : μ ≠ 0) (hf : Integrable f μ) :
    0 < μ {x | ⨍ a, f a ∂μ ≤ f x}

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
⊢ 0 < μ {x | ⨍ (a : α), f a ∂μ ≤ f x}

Tactic:
simpa using measure_setAverage_le_pos (Measure.measure_univ_ne_zero.2 hμ) (measure_ne_top _ _)
  hf.integrableOn

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem toFinset_cons : toFinset (a :: l) = insert a (toFinset l) :=
  Finset.eq_of_veq <| by by_cases h : a ∈ l <;> simp [Finset.insert_val', Multiset.dedup_cons, h]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val

Tactic:
by_cases h : a ∈ l <;> simp [Finset.insert_val', Multiset.dedup_cons, h]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem supDegree_sum_le {ι} {s : Finset ι} {f : ι → R[A]} :
    (∑ i ∈ s, f i).supDegree D ≤ s.sup (fun i => (f i).supDegree D)

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
⊢ supDegree D (∑ i ∈ s, f i) ≤ s.sup fun i => supDegree D (f i)

Tactic:
classical
exact (Finset.sup_mono Finsupp.support_finset_sum).trans_eq (Finset.sup_biUnion _ _)

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
⊢ supDegree D (∑ i ∈ s, f i) ≤ s.sup fun i => supDegree D (f i)

Tactic:
exact (Finset.sup_mono Finsupp.support_finset_sum).trans_eq (Finset.sup_biUnion _ _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulVecOperator.lean
theorem denote_mem_prefix {aig : AIG α} {input : β aig len} (h) :
    ⟦(f aig input).aig, ⟨start, by apply lt_size_of_lt_aig_size; omega⟩, assign⟧
      =
    ⟦aig, ⟨start, h⟩, assign⟧ :=  by
  rw [denote_input_entry ⟨aig, start, h⟩]

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
assign : α → Bool
start : Nat
aig : AIG α
input : β aig len
h : start < aig.decls.size
⊢ start < (f aig input).aig.decls.size

Tactic:
apply lt_size_of_lt_aig_size

Result:
case h
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
assign : α → Bool
start : Nat
aig : AIG α
input : β aig len
h : start < aig.decls.size
⊢ start < aig.decls.size

Proof state:
case h
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
assign : α → Bool
start : Nat
aig : AIG α
input : β aig len
h : start < aig.decls.size
⊢ start < aig.decls.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
assign : α → Bool
start : Nat
aig : AIG α
input : β aig len
h : start < aig.decls.size
⊢ ⟦assign, { aig := (f aig input).aig, ref := { gate := start, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, hgate := h } }⟧

Tactic:
rw [denote_input_entry ⟨aig, start, h⟩]

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem smul_oreDiv_one (r : R) (x : X) : r • (x /ₒ (1 : S)) = (r • x) /ₒ (1 : S)

Proof state:
R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
x : X
⊢ r • (x /ₒ 1) = r • x /ₒ 1

Tactic:
rw [← smul_one_oreDiv_one_smul, smul_div_one, smul_assoc, one_smul]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem divp_eq_divp_iff {x y : α} {ux uy : αˣ} : x /ₚ ux = y /ₚ uy ↔ x * uy = y * ux

Proof state:
α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ x /ₚ ux = y /ₚ uy ↔ x * ↑uy = y * ↑ux

Tactic:
rw [divp_eq_iff_mul_eq, divp_mul_eq_mul_divp, divp_eq_iff_mul_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem cos_arctan (x : ℝ) : cos (arctan x) = 1 / √(1 + x ^ 2)

Proof state:
x : ℝ
⊢ cos (arctan x) = 1 / √(1 + x ^ 2)

Tactic:
rw_mod_cast [one_div, ← inv_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]

Result:
no goals
-- Mathlib/Algebra/Divisibility/Units.lean
theorem IsRelPrime.mul_right (H1 : IsRelPrime x y) (H2 : IsRelPrime x z) :
    IsRelPrime x (y * z)

Proof state:
α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime y x
H2 : IsRelPrime z x
⊢ IsRelPrime (y * z) x

Tactic:
exact H1.mul_left H2

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime x y
H2 : IsRelPrime x z
⊢ IsRelPrime x (y * z)

Tactic:
rw [isRelPrime_comm] at H1 H2 ⊢

Result:
α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime y x
H2 : IsRelPrime z x
⊢ IsRelPrime (y * z) x
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem sin_oangle_add_right_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.sin (o.oangle x (x + y)) = ‖y‖ / ‖x + y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).sin = ‖y‖ / ‖x + y‖

Tactic:
have hs : (o.oangle x (x + y)).sign = 1 := by
  rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).sin = ‖y‖ / ‖x + y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).sin = ‖y‖ / ‖x + y‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  InnerProductGeometry.sin_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.left_ne_zero_of_oangle_eq_pi_div_two h))]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).sign = 1

Tactic:
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem braiding_inv_fst {X Y : C} : (β_ X Y).inv ≫ fst _ _ = snd _ _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y : C
⊢ (β_ X Y).inv ≫ fst X Y = snd Y X

Tactic:
simp [braiding_eq_braiding, fst, snd]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem coe_submonoidClass_iff {M B : Type*} [CommMonoid M] [SetLike B M] [SubmonoidClass B M]
    {N : B} {ζ : N} : IsPrimitiveRoot (ζ : M) k ↔ IsPrimitiveRoot ζ k

Proof state:
k : ℕ
M : Type u_7
B : Type u_8
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
N : B
ζ : ↥N
⊢ IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k

Tactic:
simp_rw [iff_def]

Result:
k : ℕ
M : Type u_7
B : Type u_8
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
N : B
ζ : ↥N
⊢ (↑ζ ^ k = 1 ∧ ∀ (l : ℕ), ↑ζ ^ l = 1 → k ∣ l) ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l

Proof state:
k : ℕ
M : Type u_7
B : Type u_8
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
N : B
ζ : ↥N
⊢ (↑ζ ^ k = 1 ∧ ∀ (l : ℕ), ↑ζ ^ l = 1 → k ∣ l) ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l

Tactic:
norm_cast

Result:
no goals