harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
@[simp] lemma uIoo_of_ge (h : b ≤ a) : uIoo a b = Ioo b a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ uIoo a b = Ioo b a

Tactic:
rw [uIoo, inf_eq_right.2 h, sup_eq_left.2 h]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
lemma injective_iff_map_algebraMap_eq {T} [CommRing T] (f : S →+* T) :
    Function.Injective f ↔ ∀ x y,
      algebraMap R S x = algebraMap R S y ↔ f (algebraMap R S x) = f (algebraMap R S y)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_4
inst✝ : CommRing T
f : S →+* T
⊢ (∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ (f.comp (algebraMap R S)) x = (f.comp (algebraMap R S)) y) ↔
    ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ (lift ⋯) ((algebraMap R S) x) = (lift ⋯) ((algebraMap R S) y)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_4
inst✝ : CommRing T
f : S →+* T
⊢ Injective ⇑f ↔ ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ f ((algebraMap R S) x) = f ((algebraMap R S) y)

Tactic:
rw [← IsLocalization.lift_of_comp (M := M) f, IsLocalization.lift_injective_iff]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_4
inst✝ : CommRing T
f : S →+* T
⊢ (∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ (f.comp (algebraMap R S)) x = (f.comp (algebraMap R S)) y) ↔
    ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ (lift ⋯) ((algebraMap R S) x) = (lift ⋯) ((algebraMap R S) y)
-- Mathlib/Analysis/Complex/Circle.lean
theorem exp_zero : exp 0 = 1 :=
  Subtype.ext <| by rw [coe_exp, ofReal_zero, zero_mul, Complex.exp_zero, coe_one]

Proof state:
⊢ ↑(exp 0) = ↑1

Tactic:
rw [coe_exp, ofReal_zero, zero_mul, Complex.exp_zero, coe_one]

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem map_inr (f : M →ₗ[R'] N) (x : M) : map f (inr x) = inr (f x)

Proof state:
R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
x : M
⊢ (map f) (inr x) = inr (f x)

Tactic:
rw [map, liftEquivOfComm_apply, lift_apply_inr, LinearMap.comp_apply, inrHom_apply]

Result:
no goals
-- Mathlib/Combinatorics/Additive/ETransform.lean
theorem MulETransform.card :
    (mulETransformLeft e x).1.card + (mulETransformLeft e x).2.card +
        ((mulETransformRight e x).1.card + (mulETransformRight e x).2.card) =
      x.1.card + x.2.card + (x.1.card + x.2.card)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ #(mulETransformLeft e x).1 + #(mulETransformLeft e x).2 +
      (#(mulETransformRight e x).1 + #(mulETransformRight e x).2) =
    #x.1 + #x.2 + (#x.1 + #x.2)

Tactic:
rw [add_add_add_comm, mulETransformLeft.card, mulETransformRight.card, ← mul_add, two_mul]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
theorem pi_eq_zero (f : ∀ i, M →L[R] φ i) : pi f = 0 ↔ ∀ i, f i = 0

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M →L[R] φ i
⊢ pi f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
simp only [ContinuousLinearMap.ext_iff, pi_apply, funext_iff]

Result:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M →L[R] φ i
⊢ (∀ (x : M) (x_1 : ι), (f x_1) x = 0 x x_1) ↔ ∀ (i : ι) (x : M), (f i) x = 0 x

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M →L[R] φ i
⊢ (∀ (x : M) (x_1 : ι), (f x_1) x = 0 x x_1) ↔ ∀ (i : ι) (x : M), (f i) x = 0 x

Tactic:
exact forall_swap

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x

Proof state:
w : Nat
x : BitVec w
⊢ x.abs = if x.msb = true then -x else x

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivAtFilter.const_smul (c : R) (hf : HasDerivAtFilter f f' x L) :
    HasDerivAtFilter (fun y => c • f y) (c • f') x L

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
R : Type u_2
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : HasDerivAtFilter f f' x L
⊢ HasDerivAtFilter (fun y => c • f y) (c • f') x L

Tactic:
simpa using (hf.const_smul c).hasDerivAtFilter

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
lemma specializingMap_iff_closure_singleton (hf : Continuous f) :
    SpecializingMap f ↔ ∀ x, f '' closure {x} = closure {f x}

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
⊢ SpecializingMap f ↔ ∀ (x : X), f '' closure {x} = closure {f x}

Tactic:
simpa only [closure_singleton_eq_Iic] using
  Relation.fibration_iff_image_Iic hf.specialization_monotone

Result:
no goals
-- Mathlib/Data/FinEnum.lean
theorem Pi.mem_enum (f : ∀ a, β a) :
    f ∈ Pi.enum β

Proof state:
α : Type u_1
inst✝¹ : FinEnum α
β : α → Type u_2
inst✝ : (a : α) → FinEnum (β a)
f : (a : α) → β a
⊢ f ∈ enum β

Tactic:
simpa [Pi.enum] using ⟨fun a _ => f a, mem_pi_toList _ _, rfl⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem comap_exp_nhds_zero : comap exp (𝓝 0) = atBot :=
  (comap_nhdsWithin_range exp 0).symm.trans <| by simp

Proof state:
⊢ comap rexp (𝓝[Set.range rexp] 0) = atBot

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ToNat.lean
theorem cast_toNat_of_aleph0_le {c : Cardinal} (h : ℵ₀ ≤ c) : ↑(toNat c) = (0 : Cardinal)

Proof state:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ↑(toNat c) = 0

Tactic:
rw [toNat_apply_of_aleph0_le h, Nat.cast_zero]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem subtypePerm_apply_pow_of_mem {g : Perm α} {s : Finset α}
    (hs : ∀ x : α, x ∈ s ↔ g x ∈ s) {n : ℕ} {x : α} (hx : x ∈ s) :
    ((g.subtypePerm hs ^ n) (⟨x, hx⟩ : s) : α) = (g ^ n) x

Proof state:
α : Type u_2
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
x : α
hx : x ∈ s
⊢ ↑((g.subtypePerm hs ^ n) ⟨x, hx⟩) = (g ^ n) x

Tactic:
simp only [subtypePerm_pow, subtypePerm_apply]

Result:
no goals
-- Mathlib/Data/Int/Lemmas.lean
theorem natAbs_inj_of_nonpos_of_nonpos {a b : ℤ} (ha : a ≤ 0) (hb : b ≤ 0) :
    natAbs a = natAbs b ↔ a = b

Proof state:
a b : ℤ
ha : a ≤ 0
hb : b ≤ 0
⊢ a.natAbs = b.natAbs ↔ a = b

Tactic:
simpa only [Int.natAbs_neg, neg_inj] using
  natAbs_inj_of_nonneg_of_nonneg (neg_nonneg_of_nonpos ha) (neg_nonneg_of_nonpos hb)

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Dual.lean
theorem continuousLinearMapOfBilin_apply (v w : E) : ⟪B♯ v, w⟫ = B v w

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v w : E
⊢ ⟪B♯ v, w⟫_𝕜 = (B v) w

Tactic:
rw [continuousLinearMapOfBilin, coe_comp', ContinuousLinearEquiv.coe_coe,
  LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, toDual_symm_apply]

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
theorem imp_iff_not_sup : (φ.imp ψ) ⇔[T] (φ.not ⊔ ψ) :=
  fun M v xs => by simp [imp_iff_not_or]

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⟹ ψ ⇔ ∼φ ⊔ ψ).Realize v xs

Tactic:
simp [imp_iff_not_or]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
@[to_additive] lemma map_comp_one [OneHomClass F M N] (f : F) : f ∘ (1 : ι → M) = 1

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : One M
inst✝² : One N
inst✝¹ : FunLike F M N
inst✝ : OneHomClass F M N
f : F
⊢ ⇑f ∘ 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem mul_lt_iff_lt_one_left' [MulLeftStrictMono α]
    [MulLeftReflectLT α] {a b : α} :
    a * b < a ↔ b < 1 :=
  Iff.trans (by rw [mul_one]) (mul_lt_mul_iff_left a)

Proof state:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulLeftReflectLT α
a b : α
⊢ a * b < a ↔ a * b < a * 1

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasFDerivWithinAt_inter (h : t ∈ 𝓝 x) :
    HasFDerivWithinAt f f' (s ∩ t) x ↔ HasFDerivWithinAt f f' s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
h : t ∈ 𝓝 x
⊢ HasFDerivWithinAt f f' (s ∩ t) x ↔ HasFDerivWithinAt f f' s x

Tactic:
simp [HasFDerivWithinAt, nhdsWithin_restrict' s h]

Result:
no goals
-- Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
lemma functorHomEquiv_id [HasFunctorEnrichedHom V F₁ F₁] [HasEnrichedHom V F₁ F₁] :
    (functorHomEquiv V) (𝟙 F₁) = functorEnrichedId V F₁

Proof state:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₁
⊢ (functorHomEquiv V) (𝟙 F₁) = functorEnrichedId V F₁

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem unattach_attach (o : Option α) : o.attach.unattach = o

Proof state:
α : Type u_1
o : Option α
⊢ o.attach.unattach = o

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem ones_sizeUpTo (n : ℕ) (i : ℕ) : (ones n).sizeUpTo i = min i n

Proof state:
n i : ℕ
⊢ (ones n).sizeUpTo i = i ⊓ n

Tactic:
simp [sizeUpTo, ones_blocks, take_replicate]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
theorem log_pos_real' {x : ℝ≥0∞} (h : 0 < x.toReal) :
    log x = Real.log (ENNReal.toReal x)

Proof state:
x : ℝ≥0∞
h : 0 < x.toReal
⊢ x.log = ↑(Real.log x.toReal)

Tactic:
simp [log, (ENNReal.toReal_pos_iff.1 h).1.ne', (ENNReal.toReal_pos_iff.1 h).2.ne]

Result:
no goals
-- Mathlib/Data/Finsupp/Interval.lean
theorem card_Icc : #(Icc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i))

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(Icc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i))

Tactic:
simp_rw [Icc_eq, card_finsupp, coe_rangeIcc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem natAdd_zero {n : Nat} : natAdd 0 = Fin.cast (Nat.zero_add n).symm

Proof state:
n : Nat
⊢ natAdd 0 = Fin.cast ⋯

Tactic:
ext

Result:
case h.h
n : Nat
x✝ : Fin n
⊢ ↑(natAdd 0 x✝) = ↑(Fin.cast ⋯ x✝)

Proof state:
case h.h
n : Nat
x✝ : Fin n
⊢ ↑(natAdd 0 x✝) = ↑(Fin.cast ⋯ x✝)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Integral.lean
theorem ConvexOn.average_mem_epigraph [IsFiniteMeasure μ] [NeZero μ] (hg : ConvexOn ℝ s g)
    (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ x ∂μ, f x ∈ s)
    (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ) :
    (⨍ x, f x ∂μ, ⨍ x, g (f x) ∂μ) ∈ {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2}

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ g p.1 ≤ p.2}

Tactic:
have ht_mem : ∀ᵐ x ∂μ, (f x, g (f x)) ∈ {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} :=
  hfs.mono fun x hx => ⟨hx, le_rfl⟩

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
ht_mem : ∀ᵐ (x : α) ∂μ, (f x, g (f x)) ∈ {p | p.1 ∈ s ∧ g p.1 ≤ p.2}
⊢ (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ g p.1 ≤ p.2}

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
ht_mem : ∀ᵐ (x : α) ∂μ, (f x, g (f x)) ∈ {p | p.1 ∈ s ∧ g p.1 ≤ p.2}
⊢ (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ g p.1 ≤ p.2}

Tactic:
exact average_pair hfi hgi ▸
  hg.convex_epigraph.average_mem (hsc.epigraph hgc) ht_mem (hfi.prod_mk hgi)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_singleton (R) (a : α) : Pairwise R [a]

Proof state:
α : Type u_1
R : α → α → Prop
a : α
⊢ Pairwise R [a]

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/InitTail.lean
theorem init_sub (x y : 𝕎 R) (n : ℕ) : init n (x - y) = init n (init n x - init n y)

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
n : ℕ
⊢ init n (x - y) = init n (init n x - init n y)

Tactic:
init_ring using wittSub_vars

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
@[to_additive]
protected lemma div_self (h : IsUnit a) : a / a = 1

Proof state:
α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ a / a = 1

Tactic:
rw [div_eq_mul_inv, h.mul_inv_cancel]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/VectorSpace.lean
theorem range_extend (hs : LinearIndepOn K id s) :
    range (Basis.extend hs) = hs.extend (subset_univ _)

Proof state:
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
hs : LinearIndepOn K id s
⊢ range ⇑(extend hs) = hs.extend ⋯

Tactic:
rw [coe_extend, Subtype.range_coe_subtype, setOf_mem_eq]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tanh_zero : tanh 0 = 0

Proof state:
⊢ tanh 0 = 0

Tactic:
simp [tanh]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem support_map : (p.map f).support = p.support.map f

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
⊢ (Walk.map f p).support = List.map (⇑f) p.support

Tactic:
induction p <;> simp [*]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem prod_eq_top : s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : UpperSet α
t : UpperSet β
⊢ ↑(s ×ˢ t) = ↑⊤ ↔ ↑s = ↑⊤ ∨ ↑t = ↑⊤

Tactic:
exact prod_eq_empty_iff

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : UpperSet α
t : UpperSet β
⊢ s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤

Tactic:
simp_rw [SetLike.ext'_iff]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : UpperSet α
t : UpperSet β
⊢ ↑(s ×ˢ t) = ↑⊤ ↔ ↑s = ↑⊤ ∨ ↑t = ↑⊤
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueFinset_eq_empty_iff : G.cliqueFinset n = ∅ ↔ G.CliqueFree n

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
⊢ G.cliqueFinset n = ∅ ↔ G.CliqueFree n

Tactic:
simp_rw [CliqueFree, eq_empty_iff_forall_not_mem, mem_cliqueFinset_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem take_toArray (l : List α) (n : Nat) : l.toArray.take n = (l.take n).toArray

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ l.toArray.take n = (take n l).toArray

Tactic:
apply Array.ext <;> simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Comp.lean
lemma comp_add_right (μ κ : Kernel α β) (η : Kernel β γ) :
    η ∘ₖ (μ + κ) = η ∘ₖ μ + η ∘ₖ κ

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((η ∘ₖ (μ + κ)) a✝) s✝ = ((η ∘ₖ μ + η ∘ₖ κ) a✝) s✝

Tactic:
simp [comp_apply' _ _ _ hs]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel β γ
⊢ η ∘ₖ (μ + κ) = η ∘ₖ μ + η ∘ₖ κ

Tactic:
ext _ _ hs

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((η ∘ₖ (μ + κ)) a✝) s✝ = ((η ∘ₖ μ + η ∘ₖ κ) a✝) s✝
-- Mathlib/Algebra/Module/Torsion.lean
lemma torsionBy.neg : A[-n] = A[n]

Proof state:
A : Type u_3
inst✝ : AddCommGroup A
n : ℤ
⊢ A[-n] = A[n]

Tactic:
ext a

Result:
case h
A : Type u_3
inst✝ : AddCommGroup A
n : ℤ
a : A
⊢ a ∈ A[-n] ↔ a ∈ A[n]

Proof state:
case h
A : Type u_3
inst✝ : AddCommGroup A
n : ℤ
a : A
⊢ a ∈ A[-n] ↔ a ∈ A[n]

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem zeroLocus_bUnion (s : Set (Set R)) :
    zeroLocus (⋃ s' ∈ s, s' : Set R) = ⋂ s' ∈ s, zeroLocus s'

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set (Set R)
⊢ zeroLocus (⋃ s' ∈ s, s') = ⋂ s' ∈ s, zeroLocus s'

Tactic:
simp only [zeroLocus_iUnion]

Result:
no goals
-- Mathlib/Data/PFunctor/Multivariate/W.lean
theorem wDest'_wMk {α : TypeVec n} (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α) :
    P.wDest' (P.wMk a f' f) = ⟨a, splitFun f' f⟩

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ P.wDest' (P.wMk a f' f) = ⟨a, splitFun f' f⟩

Tactic:
rw [wDest', wRec_eq]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
@[simp] lemma oddKernel_zero (x : ℝ) : oddKernel 0 x = 0

Proof state:
x : ℝ
⊢ oddKernel 0 x = 0

Tactic:
simpa using oddKernel_neg 0 x

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
lemma IsUpperSet.isLowerSet_preimage_coe (hs : IsUpperSet s) :
    IsLowerSet ((↑) ⁻¹' t : Set s) ↔ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t

Proof state:
α : Type u_1
inst✝ : LE α
s t : Set α
hs : IsUpperSet s
⊢ IsLowerSet (Subtype.val ⁻¹' t) ↔ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t

Tactic:
aesop

Result:
no goals
-- Mathlib/RingTheory/Ideal/Cotangent.lean
theorem map_toCotangent_ker : I.toCotangent.ker.map I.subtype = I ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Submodule.map (Submodule.subtype I) (LinearMap.ker I.toCotangent) = I ^ 2

Tactic:
rw [Ideal.toCotangent, Submodule.ker_mkQ, pow_two, Submodule.map_smul'' I ⊤ (Submodule.subtype I),
  Algebra.id.smul_eq_mul, Submodule.map_subtype_top]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem lintegral_enorm_neg {f : α → β} : ∫⁻ a, ‖(-f) a‖ₑ ∂μ = ∫⁻ a, ‖f a‖ₑ ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
⊢ ∫⁻ (a : α), ‖(-f) a‖ₑ ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast!_of_perm [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α}
    [Inhabited (β a)] (hl : DistinctKeys l) (h : Perm l l') :
    getValueCast! a l = getValueCast! a l'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l l' : List ((a : α) × β a)
a : α
inst✝ : Inhabited (β a)
hl : DistinctKeys l
h : l.Perm l'
⊢ getValueCast! a l = getValueCast! a l'

Tactic:
simp only [getValueCast!_eq_getValueCast?, getValueCast?_of_perm hl h]

Result:
no goals
-- Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
@[simp]
private lemma card_triangleIndices : #(triangleIndices s) = card α * #s

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
⊢ #(triangleIndices s) = Fintype.card α * #s

Tactic:
simp [triangleIndices, card_univ]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem isThreeCycle_cycleRange_two {n : ℕ} : IsThreeCycle (cycleRange 2 : Perm (Fin (n + 3)))

Proof state:
n : ℕ
⊢ (cycleRange 2).IsThreeCycle

Tactic:
rw [IsThreeCycle, cycleType_cycleRange] <;> simp [Fin.ext_iff]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem uniformity_dist_of_mem_uniformity [LinearOrder β] {U : Filter (α × α)} (z : β)
    (D : α → α → β) (H : ∀ s, s ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s) :
    U = ⨅ ε > z, 𝓟 { p : α × α | D p.1 p.2 < ε } :=
  HasBasis.eq_biInf ⟨fun s => by simp only [H, subset_def, Prod.forall, mem_setOf]⟩

Proof state:
α : Type u
β : Type v
inst✝ : LinearOrder β
U : Filter (α × α)
z : β
D : α → α → β
H : ∀ (s : Set (α × α)), s ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s
s : Set (α × α)
⊢ s ∈ U ↔ ∃ i > z, {p | D p.1 p.2 < i} ⊆ s

Tactic:
simp only [H, subset_def, Prod.forall, mem_setOf]

Result:
no goals