harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal'_conjTranspose {α} [AddMonoid α] [StarAddMonoid α]
    (M : ∀ i, Matrix (m' i) (n' i) α) : (blockDiagonal' M)ᴴ = blockDiagonal' fun k => (M k)ᴴ

Proof state:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
inst✝² : DecidableEq o
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : (i : o) → Matrix (m' i) (n' i) α
⊢ (blockDiagonal' M)ᴴ = blockDiagonal' fun k => (M k)ᴴ

Tactic:
simp only [conjTranspose, blockDiagonal'_transpose]

Result:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
inst✝² : DecidableEq o
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : (i : o) → Matrix (m' i) (n' i) α
⊢ (blockDiagonal' fun k => (M k)ᵀ).map star = blockDiagonal' fun k => (M k)ᵀ.map star

Proof state:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
inst✝² : DecidableEq o
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : (i : o) → Matrix (m' i) (n' i) α
⊢ (blockDiagonal' fun k => (M k)ᵀ).map star = blockDiagonal' fun k => (M k)ᵀ.map star

Tactic:
exact blockDiagonal'_map _ star (star_zero α)

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiffAt.prod_map {f : E → F} {g : E' → F'} {x : E} {y : E'} (hf : ContDiffAt 𝕜 n f x)
    (hg : ContDiffAt 𝕜 n g y) : ContDiffAt 𝕜 n (Prod.map f g) (x, y)

Proof state:
case h.e'_11
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : WithTop ℕ∞
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_4
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
x : E
y : E'
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ y
⊢ univ = univ ×ˢ univ

Tactic:
simp only [univ_prod_univ]

Result:
no goals

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
n : WithTop ℕ∞
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_4
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
x : E
y : E'
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g y
⊢ ContDiffAt 𝕜 n (Prod.map f g) (x, y)

Tactic:
rw [ContDiffAt] at *

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : WithTop ℕ∞
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_4
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
x : E
y : E'
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ y
⊢ ContDiffWithinAt 𝕜 n (Prod.map f g) univ (x, y)

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
n : WithTop ℕ∞
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_4
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
x : E
y : E'
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ y
⊢ ContDiffWithinAt 𝕜 n (Prod.map f g) univ (x, y)

Tactic:
convert hf.prod_map hg

Result:
case h.e'_11
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : WithTop ℕ∞
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_4
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
x : E
y : E'
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ y
⊢ univ = univ ×ˢ univ
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem indicator_ae_eq_of_ae_eq_set (hst : s =ᵐ[μ] t) : s.indicator f =ᵐ[μ] t.indicator f

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → β
inst✝ : Zero β
hst : s =ᶠ[ae μ] t
⊢ s.indicator f =ᶠ[ae μ] t.indicator f

Tactic:
classical exact piecewise_ae_eq_of_ae_eq_set hst

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → β
inst✝ : Zero β
hst : s =ᶠ[ae μ] t
⊢ s.indicator f =ᶠ[ae μ] t.indicator f

Tactic:
exact piecewise_ae_eq_of_ae_eq_set hst

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
lemma le_valuation_add (hxy : x + y ≠ 0) : min x.valuation y.valuation ≤ (x + y).valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hxy : x + y ≠ 0
⊢ ↑x.valuation ⊓ ↑y.valuation ≤ ↑(x + y).valuation

Tactic:
simpa [← valuation_coe] using Padic.le_valuation_add <| coe_ne_zero.2 hxy

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hxy : x + y ≠ 0
⊢ x.valuation ⊓ y.valuation ≤ (x + y).valuation

Tactic:
zify

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hxy : x + y ≠ 0
⊢ ↑x.valuation ⊓ ↑y.valuation ≤ ↑(x + y).valuation
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem limZero_congr {f g : CauSeq β abv} (h : f ≈ g) : LimZero f ↔ LimZero g :=
  ⟨fun l => by simpa using add_limZero (Setoid.symm h) l, fun l => by simpa using add_limZero h l⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
l : f.LimZero
⊢ g.LimZero

Tactic:
simpa using add_limZero (Setoid.symm h) l

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
l : g.LimZero
⊢ f.LimZero

Tactic:
simpa using add_limZero h l

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Lemmas.lean
theorem sum_append {l₁ l₂ : List Nat}: (l₁ ++ l₂).sum = l₁.sum + l₂.sum

Proof state:
l₁ l₂ : List Nat
⊢ (l₁ ++ l₂).sum = l₁.sum + l₂.sum

Tactic:
induction l₁ <;> simp [*, Nat.add_assoc]

Result:
no goals
-- Mathlib/Order/Hom/CompleteLattice.lean
theorem cancel_left {g : sSupHom β γ} {f₁ f₂ : sSupHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : SupSet γ
g : sSupHom β γ
f₁ f₂ : sSupHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem PointedMap.headI_map {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ')
    (l : List Γ) : (l.map f).headI = f l.headI

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : List Γ
⊢ (List.map f.f l).headI = f.f l.headI

Tactic:
cases l <;> [exact (PointedMap.map_pt f).symm; rfl]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
theorem ContinuousMultilinearMap.norm_map_init_le
    (f : ContinuousMultilinearMap 𝕜 (fun i : Fin n => Ei <| castSucc i) (Ei (last n) →L[𝕜] G))
    (m : ∀ i, Ei i) : ‖f (init m) (m (last n))‖ ≤ ‖f‖ * ∏ i, ‖m i‖ :=
  calc
    ‖f (init m) (m (last n))‖ ≤ ‖f (init m)‖ * ‖m (last n)‖ := (f (init m)).le_opNorm _
    _ ≤ (‖f‖ * ∏ i, ‖(init m) i‖) * ‖m (last n)‖ :=
      (mul_le_mul_of_nonneg_right (f.le_opNorm _) (norm_nonneg _))
    _ = ‖f‖ * ((∏ i, ‖(init m) i‖) * ‖m (last n)‖) := mul_assoc _ _ _
    _ = ‖f‖ * ∏ i, ‖m i‖

Proof state:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 (fun i => Ei i.castSucc) (Ei (last n) →L[𝕜] G)
m : (i : Fin n.succ) → Ei i
⊢ ‖f‖ * ((∏ i : Fin n, ‖init m i‖) * ‖m (last n)‖) = ‖f‖ * ∏ i : Fin n.succ, ‖m i‖

Tactic:
rw [prod_univ_castSucc]

Result:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 (fun i => Ei i.castSucc) (Ei (last n) →L[𝕜] G)
m : (i : Fin n.succ) → Ei i
⊢ ‖f‖ * ((∏ i : Fin n, ‖init m i‖) * ‖m (last n)‖) = ‖f‖ * ((∏ i : Fin n, ‖m i.castSucc‖) * ‖m (last n)‖)

Proof state:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 (fun i => Ei i.castSucc) (Ei (last n) →L[𝕜] G)
m : (i : Fin n.succ) → Ei i
⊢ ‖f‖ * ((∏ i : Fin n, ‖init m i‖) * ‖m (last n)‖) = ‖f‖ * ((∏ i : Fin n, ‖m i.castSucc‖) * ‖m (last n)‖)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
theorem cons_add (a : α) (s t : Multiset α) : a ::ₘ s + t = a ::ₘ (s + t)

Proof state:
α : Type u_1
a : α
s t : Multiset α
⊢ a ::ₘ s + t = a ::ₘ (s + t)

Tactic:
rw [← singleton_add, ← singleton_add, Multiset.add_assoc]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem not_bddAbove_isInitial : ¬ BddAbove {x | IsInitial x}

Proof state:
case intro
a : Ordinal.{u_1}
ha : a ∈ upperBounds {x | x.IsInitial}
this : (succ a.card).ord ≤ a
⊢ False

Tactic:
rw [ord_le] at this

Result:
case intro
a : Ordinal.{u_1}
ha : a ∈ upperBounds {x | x.IsInitial}
this : succ a.card ≤ a.card
⊢ False

Proof state:
case intro
a : Ordinal.{u_1}
ha : a ∈ upperBounds {x | x.IsInitial}
this : succ a.card ≤ a.card
⊢ False

Tactic:
exact (lt_succ _).not_le this

Result:
no goals

Proof state:
⊢ ¬BddAbove {x | x.IsInitial}

Tactic:
rintro ⟨a, ha⟩

Result:
case intro
a : Ordinal.{u_1}
ha : a ∈ upperBounds {x | x.IsInitial}
⊢ False

Proof state:
case intro
a : Ordinal.{u_1}
ha : a ∈ upperBounds {x | x.IsInitial}
⊢ False

Tactic:
have := ha (isInitial_ord (succ a.card))

Result:
case intro
a : Ordinal.{u_1}
ha : a ∈ upperBounds {x | x.IsInitial}
this : (succ a.card).ord ≤ a
⊢ False
-- Mathlib/Tactic/ENatToNat.lean
@[enat_to_nat_top] lemma not_lt_top (x : ENat) :
    ¬(⊤ < x)

Proof state:
x : ℕ∞
⊢ ¬⊤ < x

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem comp₂_eq_mk (g : β → γ → δ) (hg : Continuous (uncurry g)) (f₁ : α →ₘ[μ] β)
    (f₂ : α →ₘ[μ] γ) : comp₂ g hg f₁ f₂ = mk (fun a => g (f₁ a) (f₂ a))
      (hg.comp_aestronglyMeasurable (f₁.aestronglyMeasurable.prod_mk f₂.aestronglyMeasurable))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ → δ
hg : Continuous (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ comp₂ g hg f₁ f₂ = mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯

Tactic:
rw [comp₂_eq_pair, pair_eq_mk, comp_mk]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ → δ
hg : Continuous (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ mk (uncurry g ∘ fun x => (↑f₁ x, ↑f₂ x)) ⋯ = mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ → δ
hg : Continuous (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ mk (uncurry g ∘ fun x => (↑f₁ x, ↑f₂ x)) ⋯ = mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem guard_comp {p : α → Prop} [DecidablePred p] {f : β → α} :
    guard p ∘ f = Option.map f ∘ guard (p ∘ f)

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : β → α
⊢ guard p ∘ f = Option.map f ∘ guard (p ∘ f)

Tactic:
ext1 b

Result:
case h
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : β → α
b : β
⊢ (guard p ∘ f) b = (Option.map f ∘ guard (p ∘ f)) b

Proof state:
case h
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : β → α
b : β
⊢ (guard p ∘ f) b = (Option.map f ∘ guard (p ∘ f)) b

Tactic:
simp [guard]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem augment_hom_zero (X : CosimplicialObject C) (X₀ : C) (f : X₀ ⟶ X.obj ⦋0⦌) (w) :
    (X.augment X₀ f w).hom.app ⦋0⦌ = f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X ^⦋0⦌
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
⊢ (X.augment X₀ f w).hom.app ⦋0⦌ = f

Tactic:
simp

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma infClosure_singleton : infClosure {a} = {a}

Proof state:
α : Type u_3
inst✝ : SemilatticeInf α
a : α
⊢ infClosure {a} = {a}

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) {h'} :
    get (insertMany m l).1 k' h' = v

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
h' : (insertMany m l).val.contains k' = true
⊢ get (insertMany m l).val k' h' = v

Tactic:
simp_to_model [Const.insertMany] using List.getValue_insertListConst_of_mem

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem take_zipWith : (zipWith f l l').take n = zipWith f (l.take n) (l'.take n)

Proof state:
case mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l' : Array α✝¹
n : Nat
toList✝ : List α✝²
⊢ (zipWith f { toList := toList✝ } l').take n = zipWith f ({ toList := toList✝ }.take n) (l'.take n)

Tactic:
cases l'

Result:
case mk.mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
n : Nat
toList✝¹ : List α✝²
toList✝ : List α✝¹
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ }).take n =
    zipWith f ({ toList := toList✝¹ }.take n) ({ toList := toList✝ }.take n)

Proof state:
case mk.mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
n : Nat
toList✝¹ : List α✝²
toList✝ : List α✝¹
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ }).take n =
    zipWith f ({ toList := toList✝¹ }.take n) ({ toList := toList✝ }.take n)

Tactic:
simp [List.take_zipWith]

Result:
no goals

Proof state:
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l : Array α✝²
l' : Array α✝¹
n : Nat
⊢ (zipWith f l l').take n = zipWith f (l.take n) (l'.take n)

Tactic:
cases l

Result:
case mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l' : Array α✝¹
n : Nat
toList✝ : List α✝²
⊢ (zipWith f { toList := toList✝ } l').take n = zipWith f ({ toList := toList✝ }.take n) (l'.take n)
-- Mathlib/RingTheory/Flat/Basic.lean
/-- `M` is flat if and only if `𝟙 M ⊗ f` is injective whenever `f` is an injective linear map.
  See `Module.Flat.iff_lTensor_preserves_injective_linearMap` to specialize the universe of
  `N, N', N''` to `Type (max u v)`. -/
lemma iff_lTensor_preserves_injective_linearMap' [Small.{v'} R] : Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N']
      (f : N →ₗ[R] N'), Function.Injective f → Function.Injective (f.lTensor M)

Proof state:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
⊢ Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(lTensor M f)

Tactic:
simp_rw [iff_rTensor_preserves_injective_linearMap', LinearMap.lTensor_inj_iff_rTensor_inj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
    (m.insert k v).getKey k (mem_insert_self h) = k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ (m.insert k v).getKey k ⋯ = k

Tactic:
simp_to_raw using Raw₀.getKey_insert_self ⟨m, _⟩

Result:
no goals
-- Mathlib/Algebra/Divisibility/Units.lean
theorem dvd_mul_left (hu : IsUnit u) : a ∣ u * b ↔ a ∣ b

Proof state:
case intro
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ ↑u * b ↔ a ∣ b

Tactic:
apply Units.dvd_mul_left

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
a b u : α
hu : IsUnit u
⊢ a ∣ u * b ↔ a ∣ b

Tactic:
rcases hu with ⟨u, rfl⟩

Result:
case intro
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ ↑u * b ↔ a ∣ b
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_eq_pGameBirthday (x : Game) :
    ∃ y : PGame.{u}, ⟦y⟧ = x ∧ y.birthday = birthday x

Proof state:
x : Game
⊢ ∃ y, ⟦y⟧ = x ∧ y.birthday = x.birthday

Tactic:
refine csInf_mem (Set.image_nonempty.2 ?_)

Result:
x : Game
⊢ Set.Nonempty fun y => ⟦y⟧ = x

Proof state:
x : Game
⊢ Set.Nonempty fun y => ⟦y⟧ = x

Tactic:
exact ⟨_, x.out_eq⟩

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Polar.lean
theorem polar_nonempty (s : Set E) : Set.Nonempty (B.polar s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ (B.polar s).Nonempty

Tactic:
use 0

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ 0 ∈ B.polar s

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ 0 ∈ B.polar s

Tactic:
exact zero_mem_polar B s

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem unbounded_of_unbounded_iUnion {α β : Type u} (r : α → α → Prop) [wo : IsWellOrder α r]
    (s : β → Set α) (h₁ : Unbounded r <| ⋃ x, s x) (h₂ : #β < Order.cof (swap rᶜ)) :
    ∃ x : β, Unbounded r (s x)

Proof state:
case intro.intro.intro
α β : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : β → Set α
h₁ : Unbounded r (⋃₀ range s)
h₂ : #β < Order.cof (swap rᶜ)
x : β
u : Unbounded r (s x)
⊢ ∃ x, Unbounded r (s x)

Tactic:
exact ⟨x, u⟩

Result:
no goals

Proof state:
α β : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : β → Set α
h₁ : Unbounded r (⋃ x, s x)
h₂ : #β < Order.cof (swap rᶜ)
⊢ ∃ x, Unbounded r (s x)

Tactic:
rw [← sUnion_range] at h₁

Result:
α β : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : β → Set α
h₁ : Unbounded r (⋃₀ range s)
h₂ : #β < Order.cof (swap rᶜ)
⊢ ∃ x, Unbounded r (s x)

Proof state:
α β : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : β → Set α
h₁ : Unbounded r (⋃₀ range s)
h₂ : #β < Order.cof (swap rᶜ)
⊢ ∃ x, Unbounded r (s x)

Tactic:
rcases unbounded_of_unbounded_sUnion r h₁ (mk_range_le.trans_lt h₂) with ⟨_, ⟨x, rfl⟩, u⟩

Result:
case intro.intro.intro
α β : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : β → Set α
h₁ : Unbounded r (⋃₀ range s)
h₂ : #β < Order.cof (swap rᶜ)
x : β
u : Unbounded r (s x)
⊢ ∃ x, Unbounded r (s x)
-- Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
@[reassoc]
lemma ofCoconeObjIso_hom_naturality (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) :
    (ofCocone c).map (homOfLE hi : ⟨i₁, hi.trans hi₂.le⟩ ⟶ ⟨i₂, hi₂.le⟩) ≫
      (ofCoconeObjIso c i₂ hi₂).hom =
      (ofCoconeObjIso c i₁ (lt_of_le_of_lt hi hi₂)).hom ≫ F.map (homOfLE hi)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ < j
⊢ (ofCocone c).map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).hom = (ofCoconeObjIso c i₁ ⋯).hom ≫ F.map (homOfLE hi)

Tactic:
rw [ofCocone_map c i₁ i₂ hi hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/CurryingThree.lean
@[simp]
lemma currying₃_unitIso_inv_app_app_app_app (F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E)
    (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
    (((currying₃.unitIso.inv.app F).app X₁).app X₂).app X₃ = 𝟙 _

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_4
E : Type u_9
inst✝³ : Category.{u_10, u_1} C₁
inst✝² : Category.{u_13, u_2} C₂
inst✝¹ : Category.{u_12, u_4} C₃
inst✝ : Category.{u_11, u_9} E
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (((currying₃.unitIso.inv.app F).app X₁).app X₂).app X₃ =
    𝟙 (((((currying₃.functor ⋙ currying₃.inverse).obj F).obj X₁).obj X₂).obj X₃)

Tactic:
simp [currying₃, Equivalence.unitInv]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/ExteriorPower.lean
@[simp]
lemma map_mk {M N : ModuleCat.{v} R} (f : M ⟶ N) {n : ℕ} (x : Fin n → M) :
    map f n (mk x) = mk (f ∘ x)

Proof state:
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
n : ℕ
x : Fin n → ↑M
⊢ (ConcreteCategory.hom (map f n)) (mk x) = mk (⇑(ConcreteCategory.hom f) ∘ x)

Tactic:
apply exteriorPower.map_apply_ιMulti

Result:
no goals
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem sub_mem_posTangentConeAt_of_segment_subset (h : segment ℝ x y ⊆ s) :
    y - x ∈ posTangentConeAt s x :=
  mem_posTangentConeAt_of_segment_subset <| by rwa [add_sub_cancel]

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : [x-[ℝ]y] ⊆ s
⊢ [x-[ℝ]x + (y - x)] ⊆ s

Tactic:
rwa [add_sub_cancel]

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem constant_of_has_deriv_right_zero (hcont : ContinuousOn f (Icc a b))
    (hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt f 0 (Ici x) x) : ∀ x ∈ Icc a b, f x = f a

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt f 0 (Ici x) x
⊢ ∀ x ∈ Icc a b, f x = f a

Tactic:
have : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ 0 * (x - a) := fun x hx =>
  norm_image_sub_le_of_norm_deriv_right_le_segment hcont hderiv (fun _ _ => norm_zero.le) x hx

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt f 0 (Ici x) x
this : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ 0 * (x - a)
⊢ ∀ x ∈ Icc a b, f x = f a

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt f 0 (Ici x) x
this : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ 0 * (x - a)
⊢ ∀ x ∈ Icc a b, f x = f a

Tactic:
simpa only [zero_mul, norm_le_zero_iff, sub_eq_zero] using this

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.node4L_lemma₂ {b c d : ℕ} (mr₂ : b + c + 1 ≤ 3 * d) : c ≤ 3 * d

Proof state:
b c d : ℕ
mr₂ : b + c + 1 ≤ 3 * d
⊢ c ≤ 3 * d

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
@[simp]
lemma imaginaryPart_ofReal (r : ℝ) : ℑ (r : ℂ) = 0

Proof state:
case a
r : ℝ
⊢ ↑(ℑ ↑r) = ↑0

Tactic:
simp [imaginaryPart_apply_coe, conj_ofReal]

Result:
no goals

Proof state:
r : ℝ
⊢ ℑ ↑r = 0

Tactic:
ext1

Result:
case a
r : ℝ
⊢ ↑(ℑ ↑r) = ↑0
-- Mathlib/.lake/packages/lean4/src/lean/lake/Lake/Util/Name.lean
theorem isPrefixOf_self {n : Name} : n.isPrefixOf n

Proof state:
n : Name
⊢ n.isPrefixOf n = true

Tactic:
cases n <;> simp [isPrefixOf]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem coe_eq_univ : (s : Set α) = univ ↔ s = ⊤

Proof state:
α : Type u_1
inst✝ : LE α
s : LowerSet α
⊢ ↑s = univ ↔ s = ⊤

Tactic:
simp [SetLike.ext'_iff]

Result:
no goals