harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem orthonormal_sUnion_of_directed {s : Set (Set E)} (hs : DirectedOn (· ⊆ ·) s)
    (h : ∀ a ∈ s, Orthonormal 𝕜 (fun x => ((x : a) : E))) :
    Orthonormal 𝕜 (fun x => x : ⋃₀ s → E)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set (Set E)
hs : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, Orthonormal 𝕜 fun x => ↑x
⊢ Orthonormal 𝕜 fun x => ↑x

Tactic:
exact orthonormal_iUnion_of_directed hs.directed_val (by simpa using h)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set (Set E)
hs : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, Orthonormal 𝕜 fun x => ↑x
⊢ ∀ (i : ↑s), Orthonormal 𝕜 fun x => ↑x

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
@[simp]
lemma DifferentiableOn.add_iff_right (hg : DifferentiableOn 𝕜 f s) :
    DifferentiableOn 𝕜 (fun y => f y + g y) s ↔ DifferentiableOn 𝕜 g s

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 g : E → F
s : Set E
hg : DifferentiableOn 𝕜 f s
⊢ DifferentiableOn 𝕜 (fun y => f y + g y) s ↔ DifferentiableOn 𝕜 g s

Tactic:
simp only [add_comm (f _), hg.add_iff_left]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Ordered.insert (h : t.Ordered cmp) : (insert cmp t v).Ordered cmp

Proof state:
α✝ : Type u_1
cmp : α✝ → α✝ → Ordering
t : RBNode α✝
v : α✝
h : Ordered cmp t
⊢ Ordered cmp
    (match t.isRed with
    | red => (ins cmp v t).setBlack
    | black => ins cmp v t)

Tactic:
split <;> simp [Ordered.setBlack, h.ins (x := v)]

Result:
no goals

Proof state:
α✝ : Type u_1
cmp : α✝ → α✝ → Ordering
t : RBNode α✝
v : α✝
h : Ordered cmp t
⊢ Ordered cmp (insert cmp t v)

Tactic:
unfold RBNode.insert

Result:
α✝ : Type u_1
cmp : α✝ → α✝ → Ordering
t : RBNode α✝
v : α✝
h : Ordered cmp t
⊢ Ordered cmp
    (match t.isRed with
    | red => (ins cmp v t).setBlack
    | black => ins cmp v t)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
    a.get! i = (a.get? i).getD default

Proof state:
α : Type u_1
inst✝ : Inhabited α
a : Array α
i : Nat
⊢ a.get! i = (a.get? i).getD default

Tactic:
by_cases p : i < a.size <;>
simp only [get!_eq_getD, getD_eq_get?, getD_getElem?, p, get?_eq_getElem?]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq {g : β → γ} {t : Set β} {y : β}
    (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (h : f ⁻¹' t ∈ 𝓝[s] x)
    (hy : f x = y) :
    ContinuousWithinAt (g ∘ f) s x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
h : f ⁻¹' t ∈ 𝓝[s] x
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
subst hy

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
h : f ⁻¹' t ∈ 𝓝[s] x
hg : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) s x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
h : f ⁻¹' t ∈ 𝓝[s] x
hg : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
exact hg.comp_of_preimage_mem_nhdsWithin hf h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem setIfInBounds_mk (a : Array α) (h : a.size = n) (i x) :
    (Vector.mk a h).setIfInBounds i x = Vector.mk (a.setIfInBounds i x) (by simp [h]) := rfl

Proof state:
α : Type ?u.14462
n : Nat
a : Array α
h : a.size = n
i : Nat
x : α
⊢ (a.setIfInBounds i x).size = n

Tactic:
simp [h]

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem prop_y (a : Solution₁ d) : d * a.y ^ 2 = a.x ^ 2 - 1

Proof state:
d : ℤ
a : Solution₁ d
⊢ d * a.y ^ 2 = a.x ^ 2 - 1

Tactic:
rw [← a.prop]

Result:
d : ℤ
a : Solution₁ d
⊢ d * a.y ^ 2 = a.x ^ 2 - (a.x ^ 2 - d * a.y ^ 2)

Proof state:
d : ℤ
a : Solution₁ d
⊢ d * a.y ^ 2 = a.x ^ 2 - (a.x ^ 2 - d * a.y ^ 2)

Tactic:
ring

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
@[reassoc (attr := simp)]
lemma μ_inv_natural_left {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
    (μ L W ε X₁ Y).inv ≫ (L').map f ▷ (L').obj Y =
      (L').map (f ▷ Y) ≫ (μ L W ε X₂ Y).inv

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₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ (μ L W ε X₁ Y).inv ≫ L'.map f ▷ L'.obj Y = L'.map (f ▷ Y) ≫ (μ L W ε X₂ Y).inv

Tactic:
simp [Iso.eq_comp_inv]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_nonneg_iff_of_base_lt_one (hx : 0 < x) : 0 ≤ logb b x ↔ x ≤ 1

Proof state:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ 0 ≤ logb b x ↔ x ≤ 1

Tactic:
rw [← not_lt, logb_neg_iff_of_base_lt_one b_pos b_lt_one hx, not_lt]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Spectrum.lean
/-- rank of a hermitian matrix is the rank of after diagonalization by the eigenvector unitary -/
lemma rank_eq_rank_diagonal : A.rank = (Matrix.diagonal hA.eigenvalues).rank

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ (↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * ↑(star hA.eigenvectorUnitary)).rank =
    (diagonal hA.eigenvalues).rank

Tactic:
simp [-isUnit_iff_ne_zero, -unitary.coe_star, rank_diagonal]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ A.rank = (diagonal hA.eigenvalues).rank

Tactic:
conv_lhs => rw [hA.spectral_theorem, ← unitary.coe_star]

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ (↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * ↑(star hA.eigenvectorUnitary)).rank =
    (diagonal hA.eigenvalues).rank
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem tsub_eq_of_eq_add_rev (hb : AddLECancellable b) (h : a = b + c) : a - b = c :=
  hb.tsub_eq_of_eq_add <| by rw [add_comm, h]

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a = b + c
⊢ a = c + b

Tactic:
rw [add_comm, h]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Spectrum.lean
theorem det_eq_prod_eigenvalues : det A = ∏ i, (hA.eigenvalues i : 𝕜)

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ A.det = ∏ i : n, ↑(hA.eigenvalues i)

Tactic:
convert congr_arg det hA.spectral_theorem

Result:
case h.e'_3
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ ∏ i : n, ↑(hA.eigenvalues i) =
    (↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary).det

Proof state:
case h.e'_3
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ ∏ i : n, ↑(hA.eigenvalues i) =
    (↑hA.eigenvectorUnitary * star ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues)).det

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ ∏ i : n, ↑(hA.eigenvalues i) =
    (↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary).det

Tactic:
rw [det_mul_right_comm]

Result:
case h.e'_3
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ ∏ i : n, ↑(hA.eigenvalues i) =
    (↑hA.eigenvectorUnitary * star ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues)).det
-- Mathlib/Computability/PostTuringMachine.lean
theorem supportsStmt_write {S : Finset (Λ' Γ Λ σ)} {l : List Bool} {q : Stmt Bool (Λ' Γ Λ σ) σ} :
    SupportsStmt S (write l q) = SupportsStmt S q

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset (Λ' Γ Λ σ)
l : List Bool
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S (write l q) = SupportsStmt S q

Tactic:
induction' l with _ l IH <;> simp only [write, SupportsStmt, *]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallyInjective.lean
@[simp]
lemma equalizerSieve_self_eq_top {F : Cᵒᵖ ⥤ D} {X : Cᵒᵖ} (x : ToType (F.obj X)) :
    equalizerSieve x x = ⊤

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
F : Cᵒᵖ ⥤ D
X : Cᵒᵖ
x : ToType (F.obj X)
⊢ equalizerSieve x x = ⊤

Tactic:
aesop

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem ae_eq_set_compl_compl {s t : Set α} : sᶜ =ᵐ[μ] tᶜ ↔ s =ᵐ[μ] t

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ sᶜ =ᶠ[ae μ] tᶜ ↔ s =ᶠ[ae μ] t

Tactic:
simp only [← measure_symmDiff_eq_zero_iff, compl_symmDiff_compl]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
@[simp]
lemma dist_prod_same_left {x : α} {y₁ y₂ : β} : dist (x, y₁) (x, y₂) = dist y₁ y₂

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α
y₁ y₂ : β
⊢ dist (x, y₁) (x, y₂) = dist y₁ y₂

Tactic:
simp [Prod.dist_eq, dist_nonneg]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem mem_Lp_iff_memLp {f : α →ₘ[μ] E} : f ∈ Lp E p μ ↔ MemLp f p μ

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α →ₘ[μ] E
⊢ f ∈ Lp E p μ ↔ MemLp (↑f) p μ

Tactic:
simp [mem_Lp_iff_eLpNorm_lt_top, MemLp, f.stronglyMeasurable.aestronglyMeasurable]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
lemma append_take : x ++ (a.take n) = (x ++ₛ a).take (x.length + n)

Proof state:
α : Type u
n : ℕ
x : List α
a : Stream' α
⊢ x ++ take n a = take (x.length + n) (x ++ₛ a)

Tactic:
induction' x <;> simp [take, Nat.add_comm, cons_append_stream, *]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_lt_iff_of_neg' (hc : c < 0) : b / c < a ↔ c * a < b

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : c < 0
⊢ b / c < a ↔ c * a < b

Tactic:
rw [mul_comm, div_lt_iff_of_neg hc]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem T_pow (m : ℤ) (n : ℕ) : (T m ^ n : R[T;T⁻¹]) = T (n * m)

Proof state:
R : Type u_1
inst✝ : Semiring R
m : ℤ
n : ℕ
⊢ T m ^ n = T (↑n * m)

Tactic:
rw [T, T, single_pow n, one_pow, nsmul_eq_mul]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_sdiff_eq_div (h : s₁ ⊆ s₂) :
    ∏ x ∈ s₂ \ s₁, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f : α → β
inst✝¹ : CommGroup β
inst✝ : DecidableEq α
h : s₁ ⊆ s₂
⊢ ∏ x ∈ s₂ \ s₁, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x

Tactic:
rw [eq_div_iff_mul_eq', prod_sdiff h]

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem equivPair_smul_same {i} (m : M i) (w : Word M) :
    equivPair i (of m • w) = ⟨m * (equivPair i w).head, (equivPair i w).tail,
      (equivPair i w).fstIdx_ne⟩

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
⊢ (equivPair i)
      ((equivPair i).symm
        (let __src := (equivPair i) w;
        { head := m * ((equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯ })) =
    { head := m * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
⊢ (equivPair i) (of m • w) = { head := m * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯ }

Tactic:
rw [of_smul_def, ← equivPair_symm]

Result:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
⊢ (equivPair i)
      ((equivPair i).symm
        (let __src := (equivPair i) w;
        { head := m * ((equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯ })) =
    { head := m * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯ }
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem ne_one [Nontrivial B] : minpoly A x ≠ 1

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ False

Tactic:
refine (one_ne_zero : (1 : B) ≠ 0) ?_

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ 1 = 0

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ 1 = 0

Tactic:
simpa using congr_arg (Polynomial.aeval x) h

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
⊢ minpoly A x ≠ 1

Tactic:
intro h

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ False
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
theorem map_comap_le (f : V ↪ W) (G : SimpleGraph W) : (G.comap f).map f ≤ G

Proof state:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph W
⊢ SimpleGraph.map f (SimpleGraph.comap (⇑f) G) ≤ G

Tactic:
rw [map_le_iff_le_comap]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image_image2_antidistrib_right {g : γ → δ} {f' : β → α' → δ} {g' : α → α'}
    (h_antidistrib : ∀ a b, g (f a b) = f' b (g' a)) :
    (image2 f s t).image g = image2 f' t (s.image g') :=
  (image_image2_antidistrib h_antidistrib).trans <| by rw [image_id']

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ image2 f' ((fun b => b) '' t) (g' '' s) = image2 f' t (g' '' s)

Tactic:
rw [image_id']

Result:
no goals
-- Mathlib/CategoryTheory/Opposites.lean
@[reassoc (attr := simp)]
lemma unop_inv_hom_id_app : (e.inv.app X).unop ≫ (e.hom.app X).unop = 𝟙 _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F G : C ⥤ Dᵒᵖ
e : F ≅ G
X : C
⊢ (e.inv.app X).unop ≫ (e.hom.app X).unop = 𝟙 (Opposite.unop (F.obj X))

Tactic:
rw [← unop_comp, hom_inv_id_app, unop_id]

Result:
no goals
-- Mathlib/Data/Finsupp/Multiset.lean
theorem toMultiset_strictMono : StrictMono (@toMultiset ι)

Proof state:
ι : Type u_3
⊢ StrictMono ⇑toMultiset

Tactic:
exact (@orderIsoMultiset ι _).strictMono

Result:
no goals

Proof state:
ι : Type u_3
⊢ StrictMono ⇑toMultiset

Tactic:
classical exact (@orderIsoMultiset ι _).strictMono

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_div_two (x i : Nat) : testBit (x / 2) i = testBit x (i + 1)

Proof state:
x i : Nat
⊢ (x / 2).testBit i = x.testBit (i + 1)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
theorem zeroProdIso_inv_snd (X : C) : (zeroProdIso X).inv ≫ prod.snd = 𝟙 X

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (zeroProdIso X).inv ≫ prod.snd = 𝟙 X

Tactic:
dsimp [zeroProdIso, binaryFanZeroLeft]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (limit.isoLimitCone { cone := BinaryFan.mk 0 (𝟙 X), isLimit := binaryFanZeroLeftIsLimit X }).inv ≫ prod.snd = 𝟙 X

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (limit.isoLimitCone { cone := BinaryFan.mk 0 (𝟙 X), isLimit := binaryFanZeroLeftIsLimit X }).inv ≫ prod.snd = 𝟙 X

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem hasProd_prod_disjoint {ι} (s : Finset ι) {t : ι → Set β} {a : ι → α}
    (hs : (s : Set ι).Pairwise (Disjoint on t)) (hf : ∀ i ∈ s, HasProd (f ∘ (↑) : t i → α) (a i)) :
    HasProd (f ∘ (↑) : (⋃ i ∈ s, t i) → α) (∏ i ∈ s, a i)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd ((t i).mulIndicator f) (a i)
⊢ HasProd (fun a => ∏ i ∈ s, (t i).mulIndicator f a) (∏ i ∈ s, a i)

Tactic:
exact hasProd_prod hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd (f ∘ Subtype.val) (a i)
⊢ HasProd (f ∘ Subtype.val) (∏ i ∈ s, a i)

Tactic:
simp_rw [hasProd_subtype_iff_mulIndicator] at *

Result:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd ((t i).mulIndicator f) (a i)
⊢ HasProd ((⋃ i ∈ s, t i).mulIndicator f) (∏ i ∈ s, a i)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd ((t i).mulIndicator f) (a i)
⊢ HasProd ((⋃ i ∈ s, t i).mulIndicator f) (∏ i ∈ s, a i)

Tactic:
rw [Finset.mulIndicator_biUnion _ _ hs]

Result:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd ((t i).mulIndicator f) (a i)
⊢ HasProd (fun a => ∏ i ∈ s, (t i).mulIndicator f a) (∏ i ∈ s, a i)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_insertEntryIfNew_le [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
    (insertEntryIfNew k v l).length ≤ l.length + 1

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ (if containsKey k l = true then l.length else l.length + 1) ≤ l.length + 1

Tactic:
split <;> omega

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ (insertEntryIfNew k v l).length ≤ l.length + 1

Tactic:
rw [length_insertEntryIfNew]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ (if containsKey k l = true then l.length else l.length + 1) ≤ l.length + 1
-- Mathlib/Algebra/Algebra/Bilinear.lean
theorem mulRight_mul [IsScalarTower R A A] (a b : A) :
    mulRight R (a * b) = (mulRight R b).comp (mulRight R a)

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a b x✝ : A
⊢ (mulRight R (a * b)) x✝ = (mulRight R b ∘ₗ mulRight R a) x✝

Tactic:
simp only [mulRight_apply, comp_apply, mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a b : A
⊢ mulRight R (a * b) = mulRight R b ∘ₗ mulRight R a

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a b x✝ : A
⊢ (mulRight R (a * b)) x✝ = (mulRight R b ∘ₗ mulRight R a) x✝
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma map_zero_one : map F f 0 1 (by simp) = f := rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.85656, u_1} C
n m : ℕ
F G : ComposableArrows C n
X : C
f : X ⟶ F.left
⊢ 0 ≤ 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem getElem_zip {l : Array α} {l' : Array β} {i : Nat} {h : i < (zip l l').size} :
    (zip l l')[i] =
      (l[i]'(lt_size_left_of_zip h), l'[i]'(lt_size_right_of_zip h)) :=
  getElem_zipWith (hi

Proof state:
α : Type u_1
β : Type u_2
l : Array α
l' : Array β
i : Nat
h : i < (l.zip l').size
⊢ i < (zipWith Prod.mk l l').size

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem head?_cyclicPermutations (l : List α) : (cyclicPermutations l).head? = l

Proof state:
α : Type u
l : List α
⊢ l.cyclicPermutations.head? = some l

Tactic:
rw [head?_eq_head, head_cyclicPermutations]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem _root_.Summable.countable_support_ennreal {f : α → ℝ≥0∞} (h : ∑' (i : α), f i ≠ ∞) :
    f.support.Countable

Proof state:
α : Type u_1
f : α → ℝ≥0∞
h : ∑' (i : α), f i ≠ ⊤
⊢ (support f).Countable

Tactic:
lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top h

Result:
case intro
α : Type u_1
f : α → ℝ≥0
h : ∑' (i : α), (fun i => ↑(f i)) i ≠ ⊤
⊢ (support fun i => ↑(f i)).Countable

Proof state:
case intro
α : Type u_1
f : α → ℝ≥0
h : ∑' (i : α), (fun i => ↑(f i)) i ≠ ⊤
⊢ (support fun i => ↑(f i)).Countable

Tactic:
simpa [support] using (ENNReal.tsum_coe_ne_top_iff_summable.1 h).countable_support_nnreal

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Cartan.lean
theorem coe_rootSpaceWeightSpaceProduct_tmul (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃)
    (x : rootSpace H χ₁) (m : genWeightSpace M χ₂) :
    (rootSpaceWeightSpaceProduct R L H M χ₁ χ₂ χ₃ hχ (x ⊗ₜ m) : M) = ⁅(x : L), (m : M)⁆

Proof state:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x : ↥(rootSpace H χ₁)
m : ↥(genWeightSpace M χ₂)
⊢ ↑((rootSpaceWeightSpaceProduct R L H M χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] m)) = ⁅↑x, ↑m⁆

Tactic:
simp only [rootSpaceWeightSpaceProduct, rootSpaceWeightSpaceProductAux, coe_liftLie_eq_lift_coe,
  AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, lift_apply, LinearMap.coe_mk, AddHom.coe_mk,
  Submodule.coe_mk]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Basic.lean
theorem mono_inl_of_factor_thru_epi_mono_factorization (f : X ⟶ Y) (g : X ⟶ Z) (g₁ : X ⟶ W) [Epi g₁]
    (g₂ : W ⟶ Z) [Mono g₂] (hg : g₁ ≫ g₂ = g) (f' : W ⟶ Y) (hf : g₁ ≫ f' = f)
    (t : PushoutCocone f g) (ht : IsColimit t) : Mono t.inl

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g₁ : X ⟶ W
inst✝¹ : Epi g₁
g₂ : W ⟶ Z
inst✝ : Mono g₂
hg : g₁ ≫ g₂ = g
f' : W ⟶ Y
hf : g₁ ≫ f' = f
t : PushoutCocone f g
ht : IsColimit t
⊢ Mono t.inl

Tactic:
apply mono_inl_of_isColimit _ _ (PushoutCocone.isColimitOfFactors _ _ _ _ _ hf hg t ht)

Result:
no goals