harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem opNNNorm_prod (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') :
    ‖f.prod g‖₊ = max ‖f‖₊ ‖g‖₊ :=
  eq_of_forall_ge_iff fun _ ↦ by
    simp only [opNNNorm_le_iff, prod_apply, Prod.nnnorm_def, max_le_iff, forall_and]

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
G' : Type wG'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
g : ContinuousMultilinearMap 𝕜 E G'
x✝ : ℝ≥0
⊢ ‖f.prod g‖₊ ≤ x✝ ↔ ‖f‖₊ ⊔ ‖g‖₊ ≤ x✝

Tactic:
simp only [opNNNorm_le_iff, prod_apply, Prod.nnnorm_def, max_le_iff, forall_and]

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ici_succ_eq_Ioi (a : α) : Ici (succ a) = Ioi a := coe_injective <| by simp

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
⊢ ↑(Ici (succ a)) = ↑(Ioi a)

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem adjMatrix_dotProduct [NonAssocSemiring α] (v : V) (vec : V → α) :
    dotProduct (G.adjMatrix α v) vec = ∑ u ∈ G.neighborFinset v, vec u

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ adjMatrix α G v ⬝ᵥ vec = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
simp [neighborFinset_eq_filter, dotProduct, sum_filter]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem interedges_mono (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) : interedges r s₂ t₂ ⊆ interedges r s₁ t₁ :=
  fun x ↦ by
    simp_rw [mem_interedges_iff]
    exact fun h ↦ ⟨hs h.1, ht h.2.1, h.2.2⟩

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
x : α × β
⊢ x ∈ interedges r s₂ t₂ → x ∈ interedges r s₁ t₁

Tactic:
simp_rw [mem_interedges_iff]

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
x : α × β
⊢ x.1 ∈ s₂ ∧ x.2 ∈ t₂ ∧ r x.1 x.2 → x.1 ∈ s₁ ∧ x.2 ∈ t₁ ∧ r x.1 x.2

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
x : α × β
⊢ x.1 ∈ s₂ ∧ x.2 ∈ t₂ ∧ r x.1 x.2 → x.1 ∈ s₁ ∧ x.2 ∈ t₁ ∧ r x.1 x.2

Tactic:
exact fun h ↦ ⟨hs h.1, ht h.2.1, h.2.2⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem ite_eq_left_iff {p : Prop} [Decidable p] {x y : α} : (if p then x else y) = x ↔ ¬ p → y = x

Proof state:
α : Sort u_1
p : Prop
inst✝ : Decidable p
x y : α
⊢ (if p then x else y) = x ↔ ¬p → y = x

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.translate_right (hf : ConvexOn 𝕜 s f) (c : E) :
    ConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z) :=
  ⟨hf.1.translate_preimage_right _, fun x hx y hy a b ha hb hab =>
    calc
      f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
c x : E
hx : x ∈ (fun z => c + z) ⁻¹' s
y : E
hy : y ∈ (fun z => c + z) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))

Tactic:
rw [smul_add, smul_add, add_add_add_comm, Convex.combo_self hab]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_filterMap (f : α → Option β) (g : γ → β → γ) (l : Array α) (init : γ) :
    (l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
l : Array α
init : γ
⊢ foldl g init (filterMap f l) =
    foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init l

Tactic:
simp [foldl_filterMap']

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean
theorem Sphere.secondInter_zero (s : Sphere P) (p : P) : s.secondInter p (0 : V) = p

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
⊢ s.secondInter p 0 = p

Tactic:
simp [Sphere.secondInter]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
@[simp]
lemma fst_add {μ ν : Measure (α × β)} : (μ + ν).fst = μ.fst + ν.fst

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ ν : Measure (α × β)
s : Set α
hs : MeasurableSet s
⊢ (μ + ν).fst s = (μ.fst + ν.fst) s

Tactic:
simp_rw [coe_add, Pi.add_apply, fst_apply hs, coe_add, Pi.add_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ ν : Measure (α × β)
⊢ (μ + ν).fst = μ.fst + ν.fst

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ ν : Measure (α × β)
s : Set α
hs : MeasurableSet s
⊢ (μ + ν).fst s = (μ.fst + ν.fst) s
-- Mathlib/Algebra/Homology/SingleHomology.lean
@[reassoc (attr := simp)]
lemma singleObjHomologySelfIso_hom_naturality :
    homologyMap ((single C c j).map f) j ≫ (singleObjHomologySelfIso c j B).hom =
      (singleObjHomologySelfIso c j A).hom ≫ f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ homologyMap ((single C c j).map f) j ≫ (singleObjHomologySelfIso c j B).hom = (singleObjHomologySelfIso c j A).hom ≫ f

Tactic:
rw [← cancel_epi (((single C c j).obj A).homologyπ j),
  homologyπ_naturality_assoc, homologyπ_singleObjHomologySelfIso_hom,
  singleObjCyclesSelfIso_hom_naturality, homologyπ_singleObjHomologySelfIso_hom_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem Const.get!ₘ_eq_getValue! [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α]
    [Inhabited β] {m : Raw₀ α (fun _ => β)} (hm : Raw.WFImp m.1) {a : α} :
    Const.get!ₘ m a = getValue! a (toListModel m.1.buckets)

Proof state:
α : Type u
β : Type v
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : PartialEquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
m : Raw₀ α fun x => β
hm : Raw.WFImp m.val
a : α
⊢ get!ₘ m a = getValue! a (toListModel m.val.buckets)

Tactic:
rw [get!ₘ, get?ₘ_eq_getValue? hm, List.getValue!_eq_getValue?]

Result:
no goals
-- Mathlib/Computability/TMConfig.lean
theorem tail_eval : tail.eval = fun v => pure v.tail

Proof state:
⊢ tail.eval = fun v => pure v.tail

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/Order/Filter/CardinalInter.lean
theorem _root_.Filter.cardinalInterFilter_aleph0 (l : Filter α) : CardinalInterFilter l ℵ₀ where
  cardinal_sInter_mem

Proof state:
α : Type u
l : Filter α
⊢ ∀ (S : Set (Set α)), #↑S < ℵ₀ → (∀ s ∈ S, s ∈ l) → ⋂₀ S ∈ l

Tactic:
simp_all only [aleph_zero, lt_aleph0_iff_subtype_finite, setOf_mem_eq, sInter_mem,
  implies_true, forall_const]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleOf_apply_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
    cycleOf f x (f x) = f (f x)

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
⊢ (f.cycleOf x) (f x) = f (f x)

Tactic:
convert cycleOf_apply_apply_pow_self f x 1 using 1

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_of_isEmpty [IsEmpty α] : Nat.card α = 0

Proof state:
α : Type u_1
inst✝ : IsEmpty α
⊢ Nat.card α = 0

Tactic:
simp [Nat.card]

Result:
no goals
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem inl_aut_inv (g : G) (n : N) : (inl ((φ g)⁻¹ n) : N ⋊[φ] G) = inr g⁻¹ * inl n * inr g

Proof state:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ inl ((φ g)⁻¹ n) = inr g⁻¹ * inl n * inr g

Tactic:
rw [← MonoidHom.map_inv, inl_aut, inv_inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_reverse (f : α → Option β) (l : Array α) : (l.reverse.filterMap f) = (l.filterMap f).reverse

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ filterMap f { toList := toList✝ }.reverse = (filterMap f { toList := toList✝ }).reverse

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ filterMap f l.reverse = (filterMap f l).reverse

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ filterMap f { toList := toList✝ }.reverse = (filterMap f { toList := toList✝ }).reverse
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem prehaar_empty (K₀ : PositiveCompacts G) {U : Set G} : prehaar (K₀ : Set G) U ⊥ = 0

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
⊢ prehaar (↑K₀) U ⊥ = 0

Tactic:
rw [prehaar, Compacts.coe_bot, index_empty, Nat.cast_zero, zero_div]

Result:
no goals
-- Mathlib/Data/Finset/Filter.lean
theorem filter_eq_empty_iff : s.filter p = ∅ ↔ ∀ ⦃x⦄, x ∈ s → ¬p x

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ filter p s = ∅ ↔ ∀ ⦃x : α⦄, x ∈ s → ¬p x

Tactic:
simp [Finset.ext_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Currying.lean
lemma uncurry_obj_injective {F₁ F₂ : B ⥤ C ⥤ D} (h : uncurry.obj F₁ = uncurry.obj F₂) :
    F₁ = F₂

Proof state:
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ C ⥤ D
h : uncurry.obj F₁ = uncurry.obj F₂
⊢ F₁ = F₂

Tactic:
rw [← curry_obj_uncurry_obj F₁, ← curry_obj_uncurry_obj F₂, h]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem uniqueBaseOn_self (I : Set α) : uniqueBaseOn I I = freeOn I

Proof state:
α : Type u_1
I : Set α
⊢ uniqueBaseOn I I = freeOn I

Tactic:
rw [uniqueBaseOn, freeOn_restrict rfl.subset]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Algebra.lean
@[mono] lemma algebraMap_strictMono : StrictMono (algebraMap α β) :=
  fun a₁ a₂ ha ↦ by
    simpa only [Algebra.algebraMap_eq_smul_one] using smul_lt_smul_of_pos_right ha zero_lt_one

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : OrderedCommSemiring α
inst✝² : StrictOrderedSemiring β
inst✝¹ : Algebra α β
inst✝ : SMulPosStrictMono α β
a₁ a₂ : α
ha : a₁ < a₂
⊢ (algebraMap α β) a₁ < (algebraMap α β) a₂

Tactic:
simpa only [Algebra.algebraMap_eq_smul_one] using smul_lt_smul_of_pos_right ha zero_lt_one

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem card_incidenceFinset_eq_degree [DecidableEq V] : #(G.incidenceFinset v) = G.degree v

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableEq V
⊢ #(G.incidenceFinset v) = Fintype.card ↑(G.incidenceSet v)

Tactic:
apply Set.toFinset_card

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableEq V
⊢ #(G.incidenceFinset v) = G.degree v

Tactic:
rw [← G.card_incidenceSet_eq_degree]

Result:
V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableEq V
⊢ #(G.incidenceFinset v) = Fintype.card ↑(G.incidenceSet v)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem map_val [BEq α] [Hashable α] {m : Raw₀ α β} {f : (a : α) → β a → δ a} :
    m.val.map f = m.map f

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
f : (a : α) → β a → δ a
⊢ Raw.map f m.val = (Raw₀.map f m).val

Tactic:
simp [Raw.map, m.2]

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Defs.lean
lemma IsNilpotent.map_iff [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type*}
    [FunLike F R S] [MonoidWithZeroHomClass F R S] {f : F} (hf : Function.Injective f) :
    IsNilpotent (f r) ↔ IsNilpotent r :=
  ⟨fun ⟨k, hk⟩ ↦ ⟨k, (map_eq_zero_iff f hf).mp <| by rwa [map_pow]⟩, fun h ↦ h.map f⟩

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
r : R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
f : F
hf : Injective ⇑f
x✝ : IsNilpotent (f r)
k : ℕ
hk : f r ^ k = 0
⊢ f (r ^ k) = 0

Tactic:
rwa [map_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range'_succ_left : range' (s + 1) n step = (range' s n step).map (· + 1)

Proof state:
s n step : Nat
⊢ range' (s + 1) n step = map (fun x => x + 1) (range' s n step)

Tactic:
ext <;> simp <;> omega

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
@[to_additive (attr := simp)]
lemma pow_mul_subgroupClosure (hs : s.Nonempty) : ∀ n, s ^ n * closure s = closure s
  | 0 => by simp
  | n + 1 => by rw [pow_succ, mul_assoc, mul_subgroupClosure hs, pow_mul_subgroupClosure hs]

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ s ^ 0 * ↑(closure s) = ↑(closure s)

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ s ^ (n + 1) * ↑(closure s) = ↑(closure s)

Tactic:
rw [pow_succ, mul_assoc, mul_subgroupClosure hs, pow_mul_subgroupClosure hs]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_mul_const_atTop_iff [NeBot l] :
    Tendsto (fun x => f x * r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
⊢ Tendsto (fun x => f x * r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atTop_iff]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem lcm_eq_right_iff [NormalizedGCDMonoid α] (a b : α) (h : normalize b = b) :
    lcm a b = b ↔ a ∣ b

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
h : normalize b = b
⊢ lcm a b = b ↔ a ∣ b

Tactic:
simpa only [lcm_comm b a] using lcm_eq_left_iff b a h

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem map_map_symm (g : P ≃ₐ[R] P') : (I.map (g : P →ₐ[R] P')).map (g.symm : P' →ₐ[R] P) = I

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
I : FractionalIdeal S P
g : P ≃ₐ[R] P'
⊢ map (↑g.symm) (map (↑g) I) = I

Tactic:
rw [← map_comp, g.symm_comp, map_id]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
theorem orderOf_a [NeZero n] (i : ZMod (2 * n)) :
    orderOf (a i) = 2 * n / Nat.gcd (2 * n) i.val

Proof state:
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a i) = 2 * n / (2 * n).gcd i.val

Tactic:
conv_lhs => rw [← ZMod.natCast_zmod_val i]

Result:
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a ↑i.val) = 2 * n / (2 * n).gcd i.val

Proof state:
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a ↑i.val) = 2 * n / (2 * n).gcd i.val

Tactic:
rw [← a_one_pow, orderOf_pow, orderOf_a_one]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Inductions.lean
theorem divX_mul_X_add (p : R[X]) : divX p * X + C (p.coeff 0) = p :=
  ext <| by rintro ⟨_ | _⟩ <;> simp [coeff_C, Nat.succ_ne_zero, coeff_mul_X]

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ), (p.divX * X + C (p.coeff 0)).coeff n = p.coeff n

Tactic:
rintro ⟨_ | _⟩ <;> simp [coeff_C, Nat.succ_ne_zero, coeff_mul_X]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p → Vector α 0} :
    (x ∈ if h : p then #v[] else l h) ↔ ∃ h : ¬ p, x ∈ l h

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : ¬p → Vector α 0
⊢ (x ∈ if h : p then { toArray := #[], size_toArray := ⋯ } else l h) ↔ ∃ h, x ∈ l h

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem flip' (n ν : ℕ) (h : ν ≤ n) :
    bernsteinPolynomial R n ν = (bernsteinPolynomial R n (n - ν)).comp (1 - X)

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ bernsteinPolynomial R n ν = (bernsteinPolynomial R n (n - ν)).comp (1 - X)

Tactic:
simp [← flip _ _ _ h, Polynomial.comp_assoc]

Result:
no goals
-- Mathlib/Data/Holor.lean
theorem slice_unitVec_mul [Ring α] {i : ℕ} {j : ℕ} (hid : i < d) (x : Holor α ds) :
    slice (unitVec d j ⊗ x) i hid = if i = j then x else 0 :=
  funext fun t : HolorIndex ds =>
    if h : i = j then by simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]
    else by simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]; rfl

Proof state:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : i = j
⊢ (unitVec d j ⊗ x).slice i hid t = (if i = j then x else 0) t

Tactic:
simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]

Result:
no goals

Proof state:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ (unitVec d j ⊗ x).slice i hid t = (if i = j then x else 0) t

Tactic:
simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]

Result:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ 0 = 0 t

Proof state:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ 0 = 0 t

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_sub_sin_I : cos x - sin x * I = exp (-x * I)

Proof state:
x : ℂ
⊢ cos x - sin x * I = cexp (-x * I)

Tactic:
rw [neg_mul, ← cosh_sub_sinh, sinh_mul_I, cosh_mul_I]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem getLsbD_congr (i : Nat) (w : Nat) (e e' : BitVec w) (h : e' = e) :
    (e'.getLsbD i) = (e.getLsbD i)

Proof state:
i w : Nat
e e' : BitVec w
h : e' = e
⊢ e'.getLsbD i = e.getLsbD i

Tactic:
simp[*]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblU_of_Z_eq_zero {P : Fin 3 → F} (hPz : P z = 0) : W.dblU P = 0

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z = 0
⊢ W.dblU P = 0

Tactic:
rw [dblU_eq, hPz, zero_pow two_ne_zero, div_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem pi_pi (s : ∀ i, Set (α i)) : Measure.pi μ (pi univ s) = ∏ i, μ i (s i)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
this : Encodable ι
⊢ (Measure.pi μ) (univ.pi s) = ∏ i : ι, (μ i) (s i)

Tactic:
rw [← pi'_eq_pi, pi'_pi]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (Measure.pi μ) (univ.pi s) = ∏ i : ι, (μ i) (s i)

Tactic:
haveI : Encodable ι := Fintype.toEncodable ι

Result:
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
this : Encodable ι
⊢ (Measure.pi μ) (univ.pi s) = ∏ i : ι, (μ i) (s i)
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeriesHasSum.sum {a : ι → ℂ} (hf : ∀ i ∈ S, LSeriesHasSum (f i) s (a i)) :
    LSeriesHasSum (∑ i ∈ S, f i) s (∑ i ∈ S, a i)

Proof state:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
a : ι → ℂ
hf : ∀ i ∈ S, LSeriesHasSum (f i) s (a i)
⊢ LSeriesHasSum (∑ i ∈ S, f i) s (∑ i ∈ S, a i)

Tactic:
simpa [LSeriesHasSum, term_sum, Finset.sum_fn S fun i ↦ term (f i) s] using hasSum_sum hf

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem ascFactorial_of_sub {n k : ℕ} :
    (n - k) * (n - k + 1).ascFactorial k = (n - k).ascFactorial (k + 1)

Proof state:
n k : ℕ
⊢ (n - k) * (n - k + 1).ascFactorial k = (n - k).ascFactorial (k + 1)

Tactic:
rw [succ_ascFactorial, ascFactorial_succ]

Result:
no goals
-- Mathlib/Computability/NFA.lean
theorem pumping_lemma [Fintype σ] {x : List α} (hx : x ∈ M.accepts)
    (hlen : Fintype.card (Set σ) ≤ List.length x) :
    ∃ a b c,
      x = a ++ b ++ c ∧
        a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts

Proof state:
α : Type u
σ : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ M.toDFA.accepts
hlen : Fintype.card (Set σ) ≤ x.length
⊢ ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.toDFA.accepts

Tactic:
exact M.toDFA.pumping_lemma hx hlen

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ M.accepts
hlen : Fintype.card (Set σ) ≤ x.length
⊢ ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts

Tactic:
rw [← toDFA_correct] at hx ⊢

Result:
α : Type u
σ : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ M.toDFA.accepts
hlen : Fintype.card (Set σ) ≤ x.length
⊢ ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.toDFA.accepts
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_comm {x y z : P} : Wbtw R x y z ↔ Wbtw R z y x

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
⊢ Wbtw R x y z ↔ Wbtw R z y x

Tactic:
rw [Wbtw, Wbtw, affineSegment_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem fold_eq {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
    l.fold f init = l.buckets.foldl (fun acc l => l.foldl f acc) init

Proof state:
α : Type u
β : α → Type v
γ : Type w
l : Raw α β
f : γ → (a : α) → β a → γ
init : γ
⊢ Raw.fold f init l = Array.foldl (fun acc l => AssocList.foldl f acc l) init l.buckets

Tactic:
simp only [Raw.fold, Raw.foldM, ← Array.foldlM_toList, Array.foldl_toList,
  ← List.foldl_eq_foldlM, Id.run, AssocList.foldl]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_omega0 : cof ω = ℵ₀ :=
  (aleph0_le_cof.2 isLimit_omega0).antisymm' <| by
    rw [← card_omega0]
    apply cof_le_card

Proof state:
⊢ ω.cof ≤ ω.card

Tactic:
apply cof_le_card

Result:
no goals

Proof state:
⊢ ω.cof ≤ ℵ₀

Tactic:
rw [← card_omega0]

Result:
⊢ ω.cof ≤ ω.card
-- Mathlib/Data/ENat/Lattice.lean
lemma iInf_coe_ne_top : ⨅ i, (f i : ℕ∞) ≠ ⊤ ↔ Nonempty ι

Proof state:
ι : Sort u_1
f : ι → ℕ
⊢ ⨅ i, ↑(f i) ≠ ⊤ ↔ Nonempty ι

Tactic:
rw [Ne, iInf_coe_eq_top, not_isEmpty_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem toNat_lt {n : Nat} {z : Int} (h : 0 ≤ z) : z.toNat < n ↔ z < (n : Int)

Proof state:
n : Nat
z : Int
h : 0 ≤ z
⊢ z.toNat < n ↔ z < ↑n

Tactic:
rw [← Int.not_le, ← Nat.not_le, Int.le_toNat h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem natDegree_C_add {a : R} : (C a + p).natDegree = p.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
⊢ (C a + p).natDegree = p.natDegree

Tactic:
simp [add_comm _ p]

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_preimage_of_not_mem (s : Set α) (f : α → M) {t : Set M} (ht : (1 : M) ∉ t) :
    mulIndicator s f ⁻¹' t = f ⁻¹' t ∩ s

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
t : Set M
ht : 1 ∉ t
⊢ s.mulIndicator f ⁻¹' t = f ⁻¹' t ∩ s

Tactic:
simp [mulIndicator_preimage, Pi.one_def, Set.preimage_const_of_not_mem ht]

Result:
no goals