harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem self_sub_toIocMod (a b : α) : b - toIocMod hp a b = toIocDiv hp a b • p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIocMod hp a b = toIocDiv hp a b • p

Tactic:
rw [toIocMod, sub_sub_cancel]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem IsSelfAdjoint.conjugate_le_conjugate {a b : R} (hab : a ≤ b) {c : R}
    (hc : IsSelfAdjoint c) : c * a * c ≤ c * b * c

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
hc : IsSelfAdjoint c
⊢ c * a * c ≤ c * b * c

Tactic:
simpa only [hc.star_eq] using conjugate_le_conjugate hab c

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem isOpenMap_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} :
    IsOpenMap f ↔ ∀ b, IsOpenMap (f ⟨·, b⟩)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ (∀ (y : β) (x : α), 𝓝 (f (x, y)) ≤ map (f ∘ fun a => (a, y)) (𝓝 x)) ↔
    ∀ (b : β) (x : α), 𝓝 (f (x, b)) ≤ map (fun x => f (x, b)) (𝓝 x)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ IsOpenMap f ↔ ∀ (b : β), IsOpenMap fun x => f (x, b)

Tactic:
simp_rw [isOpenMap_iff_nhds_le, Prod.forall, forall_swap (α := α) (β := β), nhds_prod_eq,
  nhds_discrete, prod_pure, map_map]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ (∀ (y : β) (x : α), 𝓝 (f (x, y)) ≤ map (f ∘ fun a => (a, y)) (𝓝 x)) ↔
    ∀ (b : β) (x : α), 𝓝 (f (x, b)) ≤ map (fun x => f (x, b)) (𝓝 x)
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive (attr := simp) zsmul_empty]
lemma empty_zpow (hn : n ≠ 0) : (∅ : Set α) ^ n = ∅

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Tactic:
cases n <;> aesop

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem zsmul_modEq_zsmul [NoZeroSMulDivisors ℤ α] (hn : z ≠ 0) :
    z • a ≡ z • b [PMOD z • p] ↔ a ≡ b [PMOD p] :=
  exists_congr fun m => by rw [← smul_sub, smul_comm, smul_right_inj hn]

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
p a b : α
z : ℤ
inst✝ : NoZeroSMulDivisors ℤ α
hn : z ≠ 0
m : ℤ
⊢ z • b - z • a = m • z • p ↔ b - a = m • p

Tactic:
rw [← smul_sub, smul_comm, smul_right_inj hn]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Finite.lean
lemma eq_inf :
    @IsFinite = (@IsIntegralHom ⊓ @LocallyOfFiniteType : MorphismProperty Scheme)

Proof state:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsFinite x✝ ↔ (@IsIntegralHom ⊓ @LocallyOfFiniteType) x✝

Tactic:
exact IsFinite.iff_isIntegralHom_and_locallyOfFiniteType _

Result:
no goals

Proof state:
⊢ @IsFinite = @IsIntegralHom ⊓ @LocallyOfFiniteType

Tactic:
ext

Result:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsFinite x✝ ↔ (@IsIntegralHom ⊓ @LocallyOfFiniteType) x✝
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.map_swap {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y)
    [HasLimitsOfShape (Discrete WalkingPair) C] :
    prod.map (𝟙 X) f ≫ prod.map g (𝟙 B) = prod.map g (𝟙 A) ≫ prod.map (𝟙 Y) f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
A B X Y : C
f : A ⟶ B
g : X ⟶ Y
inst✝ : HasLimitsOfShape (Discrete WalkingPair) C
⊢ map (𝟙 X) f ≫ map g (𝟙 B) = map g (𝟙 A) ≫ map (𝟙 Y) f

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
    allM p as = (! ·) <$> anyM ((! ·) <$> p ·) as

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
⊢ (do
      let __do_lift ←
        if h : as.size ≤ as.size then
            anyM.loop
              (fun v => do
                let __do_lift ← p v
                pure !__do_lift)
              as as.size h 0
          else
            anyM.loop
              (fun v => do
                let __do_lift ← p v
                pure !__do_lift)
              as as.size ⋯ 0
      pure !__do_lift) =
    (fun x => !x) <$>
      if h : as.size ≤ as.size then anyM.loop (fun x => (fun x => !x) <$> p x) as as.size h 0
      else anyM.loop (fun x => (fun x => !x) <$> p x) as as.size ⋯ 0

Tactic:
simp

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
⊢ allM p as = (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) as

Tactic:
dsimp [allM, anyM]

Result:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
⊢ (do
      let __do_lift ←
        if h : as.size ≤ as.size then
            anyM.loop
              (fun v => do
                let __do_lift ← p v
                pure !__do_lift)
              as as.size h 0
          else
            anyM.loop
              (fun v => do
                let __do_lift ← p v
                pure !__do_lift)
              as as.size ⋯ 0
      pure !__do_lift) =
    (fun x => !x) <$>
      if h : as.size ≤ as.size then anyM.loop (fun x => (fun x => !x) <$> p x) as as.size h 0
      else anyM.loop (fun x => (fun x => !x) <$> p x) as as.size ⋯ 0
-- Mathlib/Data/Sum/Basic.lean
theorem update_elim_inl [DecidableEq α] [DecidableEq (α ⊕ β)] {f : α → γ} {g : β → γ} {i : α}
    {x : γ} : update (Sum.elim f g) (inl i) x = Sum.elim (update f i x) g :=
  update_eq_iff.2 ⟨by simp, by simp +contextual⟩

Proof state:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : α
x : γ
⊢ x = Sum.elim (update f i x) g (inl i)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : α
x : γ
⊢ ∀ (x_1 : α ⊕ β), x_1 ≠ inl i → Sum.elim f g x_1 = Sum.elim (update f i x) g x_1

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
lemma obj_succ_eq : obj F X ⟨Order.succ j, by simp⟩ = X :=
  dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj)

Proof state:
C : Type u_1
inst✝² : Category.{?u.11558, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
⊢ Order.succ j ∈ Set.Iic (Order.succ j)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
⊢ ¬↑⟨Order.succ j, ⋯⟩ ≤ j

Tactic:
simpa only [Order.succ_le_iff_isMax] using hj

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourier_eval_zero (n : ℤ) : fourier n (0 : AddCircle T) = 1

Proof state:
T : ℝ
n : ℤ
⊢ (fourier n) 0 = 1

Tactic:
rw [← QuotientAddGroup.mk_zero, fourier_coe_apply, Complex.ofReal_zero, mul_zero,
  zero_div, Complex.exp_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem eval_add_of_sq_eq_zero {A} [CommSemiring A] (p : Polynomial A) (x y : A) (hy : y ^ 2 = 0) :
    p.eval (x + y) = p.eval x + p.derivative.eval x * y

Proof state:
A : Type u_2
inst✝ : CommSemiring A
p : A[X]
x y : A
hy : y ^ 2 = 0
⊢ ∑ k ∈ Finset.range ((taylor x) p).natDegree, ((taylor x) p).coeff (k + 1 + 1) * y ^ (k + 1 + 1) +
        ((taylor x) p).coeff (0 + 1) * y ^ (0 + 1) +
      ((taylor x) p).coeff 0 * y ^ 0 =
    eval x p + eval x (derivative p) * y

Tactic:
simp [pow_succ, mul_assoc, ← pow_two, hy, add_comm (eval x p)]

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CommSemiring A
p : A[X]
x y : A
hy : y ^ 2 = 0
⊢ eval (x + y) p = eval x p + eval x (derivative p) * y

Tactic:
rw [add_comm, ← Polynomial.taylor_eval,
  Polynomial.eval_eq_sum_range' ((Nat.lt_succ_self _).trans (Nat.lt_succ_self _)),
  Finset.sum_range_succ', Finset.sum_range_succ']

Result:
A : Type u_2
inst✝ : CommSemiring A
p : A[X]
x y : A
hy : y ^ 2 = 0
⊢ ∑ k ∈ Finset.range ((taylor x) p).natDegree, ((taylor x) p).coeff (k + 1 + 1) * y ^ (k + 1 + 1) +
        ((taylor x) p).coeff (0 + 1) * y ^ (0 + 1) +
      ((taylor x) p).coeff 0 * y ^ 0 =
    eval x p + eval x (derivative p) * y
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem inl_left_mul_inr_right (x : N ⋊[φ] G) : inl x.left * inr x.right = x

Proof state:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x : N ⋊[φ] G
⊢ inl x.left * inr x.right = x

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
@[simp] lemma nonMemberSubfamily_image_insert : (𝒜.image <| insert a).nonMemberSubfamily a = ∅

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ nonMemberSubfamily a (image (insert a) 𝒜) = ∅

Tactic:
simp [eq_empty_iff_forall_not_mem]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem measurable_coe_nnreal_real_iff {f : α → ℝ≥0} :
    Measurable (fun x => f x : α → ℝ) ↔ Measurable f :=
  ⟨fun h => by simpa only [Real.toNNReal_coe] using h.real_toNNReal, Measurable.coe_nnreal_real⟩

Proof state:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
h : Measurable fun x => ↑(f x)
⊢ Measurable f

Tactic:
simpa only [Real.toNNReal_coe] using h.real_toNNReal

Result:
no goals
-- Mathlib/Analysis/Convex/Topology.lean
theorem Convex.combo_closure_interior_subset_interior {s : Set E} (hs : Convex 𝕜 s) {a b : 𝕜}
    (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) : a • closure s + b • interior s ⊆ interior s

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a • closure s + b • interior s ⊆ interior s

Tactic:
rw [add_comm]

Result:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ b • interior s + a • closure s ⊆ interior s

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ b • interior s + a • closure s ⊆ interior s

Tactic:
exact hs.combo_interior_closure_subset_interior hb ha (add_comm a b ▸ hab)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_eq_size_filter (l) : countP p l = (filter p l).size

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ countP p l = (filter p l).size

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ countP p { toList := toList✝ } = (filter p { toList := toList✝ }).size

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ countP p { toList := toList✝ } = (filter p { toList := toList✝ }).size

Tactic:
simp [List.countP_eq_length_filter]

Result:
no goals
-- Mathlib/Probability/Kernel/Defs.lean
theorem finset_sum_apply (I : Finset ι) (κ : ι → Kernel α β) (a : α) :
    (∑ i ∈ I, κ i) a = ∑ i ∈ I, κ i a

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → Kernel α β
a : α
⊢ (∑ i ∈ I, κ i) a = ∑ i ∈ I, (κ i) a

Tactic:
rw [coe_finset_sum, Finset.sum_apply]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma postcomp_desc (s : relations.Solution N) :
    solution.postcomp (h.desc s) = s

Proof state:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : relations.Solution N
⊢ solution.postcomp (h.desc s) = s

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContinuousLinearEquiv.comp_contDiffOn_iff (e : F ≃L[𝕜] G) :
    ContDiffOn 𝕜 n (e ∘ f) s ↔ ContDiffOn 𝕜 n f s

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
n : WithTop ℕ∞
e : F ≃L[𝕜] G
⊢ ContDiffOn 𝕜 n (⇑e ∘ f) s ↔ ContDiffOn 𝕜 n f s

Tactic:
simp [ContDiffOn, e.comp_contDiffWithinAt_iff]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem card_dvd_of_surjective (f : G →* G') (hf : Function.Surjective f) :
    Nat.card G' ∣ Nat.card G

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
⊢ Nat.card (G ⧸ f.ker) ∣ Nat.card G

Tactic:
exact Dvd.intro_left (Nat.card f.ker) f.ker.card_mul_index

Result:
no goals

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
⊢ Nat.card G' ∣ Nat.card G

Tactic:
rw [← Nat.card_congr (QuotientGroup.quotientKerEquivOfSurjective f hf).toEquiv]

Result:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
⊢ Nat.card (G ⧸ f.ker) ∣ Nat.card G
-- Mathlib/Algebra/Category/ModuleCat/Images.lean
theorem imageIsoRange_hom_subtype {G H : ModuleCat.{v} R} (f : G ⟶ H) :
    (imageIsoRange f).hom ≫ ModuleCat.ofHom f.hom.range.subtype = Limits.image.ι f

Proof state:
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
⊢ (imageIsoRange f).hom ≫ ↟(LinearMap.range (Hom.hom f)).subtype = Limits.image.ι f

Tactic:
rw [← imageIsoRange_inv_image_ι f, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem Results.len_unique {s : Computation α} {a b m n} (h1 : Results s a m) (h2 : Results s b n) :
    m = n

Proof state:
α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
⊢ m = n

Tactic:
haveI := h1.terminates

Result:
α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this : s.Terminates
⊢ m = n

Proof state:
α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this✝ this : s.Terminates
⊢ m = n

Tactic:
rw [← h1.length, h2.length]

Result:
no goals

Proof state:
α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this : s.Terminates
⊢ m = n

Tactic:
haveI := h2.terminates

Result:
α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this✝ this : s.Terminates
⊢ m = n
-- Mathlib/Data/Set/Finite/Range.lean
theorem Finite.dependent_image {s : Set α} (hs : s.Finite) (F : ∀ i ∈ s, β) :
    {y : β | ∃ x hx, F x hx = y}.Finite

Proof state:
α : Type u
β : Type v
s : Set α
hs : s.Finite
F : (i : α) → i ∈ s → β
⊢ {y | ∃ x, ∃ (hx : x ∈ s), F x hx = y}.Finite

Tactic:
have := hs.to_subtype

Result:
α : Type u
β : Type v
s : Set α
hs : s.Finite
F : (i : α) → i ∈ s → β
this : Finite ↑s
⊢ {y | ∃ x, ∃ (hx : x ∈ s), F x hx = y}.Finite

Proof state:
α : Type u
β : Type v
s : Set α
hs : s.Finite
F : (i : α) → i ∈ s → β
this : Finite ↑s
⊢ {y | ∃ x, ∃ (hx : x ∈ s), F x hx = y}.Finite

Tactic:
simpa [range] using finite_range fun x : s => F x x.2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem isEmpty_toList {l : Array α} : l.toList.isEmpty = l.isEmpty

Proof state:
α : Type u_1
l : Array α
⊢ l.toList.isEmpty = l.isEmpty

Tactic:
rcases l with ⟨_ | _⟩ <;> simp

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Nat.lean
theorem finMulAntidiag_three {n : ℕ} (a) (ha : a ∈ finMulAntidiag 3 n) : a 0 * a 1 * a 2 = n

Proof state:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * a 1 * a 2 = n

Tactic:
rw [← (mem_finMulAntidiag.mp ha).1, Fin.prod_univ_three a]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem ite_empty_left (t s : Set α) : t.ite ∅ s = s \ t

Proof state:
α : Type u
t s : Set α
⊢ t.ite ∅ s = s \ t

Tactic:
simp [Set.ite]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem abs_sum_of_nonneg' {G : Type*} [LinearOrderedAddCommGroup G] {f : ι → G} {s : Finset ι}
    (hf : ∀ i, 0 ≤ f i) : |∑ i ∈ s, f i| = ∑ i ∈ s, f i

Proof state:
ι : Type u_1
G : Type u_9
inst✝ : LinearOrderedAddCommGroup G
f : ι → G
s : Finset ι
hf : ∀ (i : ι), 0 ≤ f i
⊢ |∑ i ∈ s, f i| = ∑ i ∈ s, f i

Tactic:
rw [abs_of_nonneg (Finset.sum_nonneg' hf)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_alter_eq_self_of_mem [LawfulBEq α] (h : m.1.WF) {k : α}
    {f : Option (β k) → Option (β k)} (h₁ : m.contains k) (h₂ : (f (m.get? k)).isSome) :
    (m.alter k f).1.size = m.1.size

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
h₁ : m.contains k = true
h₂ : (f (m.get? k)).isSome = true
⊢ (m.alter k f).val.size = m.val.size

Tactic:
simp [size_alter, h, h₁, Option.isSome_iff_ne_none.mp h₂]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem mem_map {f : α ≃o β} {b : β} : b ∈ map f s ↔ f.symm b ∈ s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
f : α ≃o β
b : β
⊢ b ∈ (map f) s ↔ f.symm b ∈ s

Tactic:
rw [← f.symm_symm, ← symm_map, f.symm_symm]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
f : α ≃o β
b : β
⊢ b ∈ (map f.symm).symm s ↔ f.symm b ∈ s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
f : α ≃o β
b : β
⊢ b ∈ (map f.symm).symm s ↔ f.symm b ∈ s

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem hasSum_lt {f g : α → ℝ≥0} {sf sg : ℝ≥0} {i : α} (h : ∀ a : α, f a ≤ g a)
    (hi : f i < g i) (hf : HasSum f sf) (hg : HasSum g sg) : sf < sg

Proof state:
α : Type u_1
f g : α → ℝ≥0
sf sg : ℝ≥0
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hf : HasSum f sf
hg : HasSum g sg
⊢ sf < sg

Tactic:
have A : ∀ a : α, (f a : ℝ) ≤ g a := fun a => NNReal.coe_le_coe.2 (h a)

Result:
α : Type u_1
f g : α → ℝ≥0
sf sg : ℝ≥0
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hf : HasSum f sf
hg : HasSum g sg
A : ∀ (a : α), ↑(f a) ≤ ↑(g a)
⊢ sf < sg

Proof state:
α : Type u_1
f g : α → ℝ≥0
sf sg : ℝ≥0
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hf : HasSum f sf
hg : HasSum g sg
A : ∀ (a : α), ↑(f a) ≤ ↑(g a)
⊢ sf < sg

Tactic:
have : (sf : ℝ) < sg := hasSum_lt A (NNReal.coe_lt_coe.2 hi) (hasSum_coe.2 hf) (hasSum_coe.2 hg)

Result:
α : Type u_1
f g : α → ℝ≥0
sf sg : ℝ≥0
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hf : HasSum f sf
hg : HasSum g sg
A : ∀ (a : α), ↑(f a) ≤ ↑(g a)
this : ↑sf < ↑sg
⊢ sf < sg

Proof state:
α : Type u_1
f g : α → ℝ≥0
sf sg : ℝ≥0
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hf : HasSum f sf
hg : HasSum g sg
A : ∀ (a : α), ↑(f a) ≤ ↑(g a)
this : ↑sf < ↑sg
⊢ sf < sg

Tactic:
exact NNReal.coe_lt_coe.1 this

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBase.ncard_diff_comm (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) :
    (B₁ \ B₂).ncard = (B₂ \ B₁).ncard

Proof state:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ (B₁ \ B₂).ncard = (B₂ \ B₁).ncard

Tactic:
rw [ncard_def, hB₁.encard_diff_comm hB₂, ← ncard_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem getElem_attachWith {xs : Vector α n} {P : α → Prop} {H : ∀ a ∈ xs, P a}
    {i : Nat} (h : i < n) :
    (xs.attachWith P H)[i] = ⟨xs[i]'(by simpa using h), H _ (getElem_mem (by simpa using h))⟩ :=
  getElem_pmap _ _ h

Proof state:
α : Type ?u.31428
n : Nat
xs : Vector α n
P : α → Prop
H : ∀ (a : α), a ∈ xs → P a
i : Nat
h : i < n
⊢ i < n

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma le_unbot_iff (hy : y ≠ ⊥) : a ≤ unbot y hy ↔ a ≤ y

Proof state:
α : Type u_1
a : α
inst✝ : LE α
y : WithBot α
hy : y ≠ ⊥
⊢ a ≤ y.unbot hy ↔ ↑a ≤ y

Tactic:
lift y to α using id hy

Result:
case intro
α : Type u_1
a : α
inst✝ : LE α
y : α
hy : ↑y ≠ ⊥
⊢ a ≤ (↑y).unbot hy ↔ ↑a ≤ ↑y

Proof state:
case intro
α : Type u_1
a : α
inst✝ : LE α
y : α
hy : ↑y ≠ ⊥
⊢ a ≤ (↑y).unbot hy ↔ ↑a ≤ ↑y

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem norm_real (c : ℝ) :
    mixedEmbedding.norm ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = |c| ^ finrank ℚ K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
⊢ mixedEmbedding.norm (fun x => c, fun x => ↑c) = |c| ^ finrank ℚ K

Tactic:
rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, norm_smul, map_one,
  mul_one]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
⊢ (fun x => c, fun x => ↑c) = c • 1

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem isRightInversion_simple_iff_isRightDescent (w : W) (i : B) :
    cs.IsRightInversion w (s i) ↔ cs.IsRightDescent w i

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsRightInversion w (cs.simple i) ↔ cs.IsRightDescent w i

Tactic:
simp [IsRightInversion, IsRightDescent, cs.isReflection_simple i]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
@[reassoc]
lemma associator_naturality₂ {X₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε} (f₂ : X₂ ⟶ Y₂) :
    ((X₁ ◁ f₂) ▷ X₃) ≫ (α_ X₁ Y₂ X₃).hom = (α_ X₁ X₂ X₃).hom ≫ (X₁ ◁ (f₂ ▷ X₃))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε
f₂ : X₂ ⟶ Y₂
⊢ (X₁ ◁ f₂) ▷ X₃ ≫ (α_ X₁ Y₂ X₃).hom = (α_ X₁ X₂ X₃).hom ≫ X₁ ◁ f₂ ▷ X₃

Tactic:
simp only [← tensorHom_id, ← id_tensorHom, associator_naturality]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean
theorem GradedAlgebra.ι_sq_zero (m : M) : GradedAlgebra.ι R M m * GradedAlgebra.ι R M m = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ (DirectSum.of (fun i => ↥(⋀[R]^i M)) (1 + 1)) (GradedMonoid.GMul.mul ⟨(ι R) m, ⋯⟩ ⟨(ι R) m, ⋯⟩) = 0

Tactic:
exact DFinsupp.single_eq_zero.mpr (Subtype.ext <| ExteriorAlgebra.ι_sq_zero _)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ (GradedAlgebra.ι R M) m * (GradedAlgebra.ι R M) m = 0

Tactic:
rw [GradedAlgebra.ι_apply, DirectSum.of_mul_of]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ (DirectSum.of (fun i => ↥(⋀[R]^i M)) (1 + 1)) (GradedMonoid.GMul.mul ⟨(ι R) m, ⋯⟩ ⟨(ι R) m, ⋯⟩) = 0
-- Mathlib/Data/Multiset/UnionInter.lean
lemma add_inter_distrib (s t u : Multiset α) : s + t ∩ u = (s + t) ∩ (s + u)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s + t ∩ u = (s + t) ∩ (s + u)

Tactic:
rw [Multiset.add_comm, inter_add_distrib, s.add_comm, s.add_comm]

Result:
no goals
-- Mathlib/Order/Antichain.lean
theorem isAntichain_and_greatest_iff : IsAntichain (· ≤ ·) s ∧ IsGreatest s a ↔ s = {a} :=
  ⟨fun h => eq_singleton_iff_unique_mem.2 ⟨h.2.1, fun _ hb => h.1.eq hb h.2.1 (h.2.2 hb)⟩, by
    rintro rfl
    exact ⟨isAntichain_singleton _ _, isGreatest_singleton⟩⟩

Proof state:
α : Type u_1
s : Set α
a : α
inst✝ : Preorder α
⊢ s = {a} → IsAntichain (fun x1 x2 => x1 ≤ x2) s ∧ IsGreatest s a

Tactic:
rintro rfl

Result:
α : Type u_1
a : α
inst✝ : Preorder α
⊢ IsAntichain (fun x1 x2 => x1 ≤ x2) {a} ∧ IsGreatest {a} a

Proof state:
α : Type u_1
a : α
inst✝ : Preorder α
⊢ IsAntichain (fun x1 x2 => x1 ≤ x2) {a} ∧ IsGreatest {a} a

Tactic:
exact ⟨isAntichain_singleton _ _, isGreatest_singleton⟩

Result:
no goals