harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWithAll_map {μ} (f : Option γ → Option δ → μ) (g : α → γ) (h : β → δ) (l₁ : Array α) (l₂ : Array β) :
    zipWithAll f (l₁.map g) (l₂.map h) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂

Proof state:
γ : Type u_1
δ : Type u_2
α : Type u_1
β : Type u_2
μ : Type u_3
f : Option γ → Option δ → μ
g : α → γ
h : β → δ
l₁ : Array α
l₂ : Array β
⊢ zipWithAll f (map g l₁) (map h l₂) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂

Tactic:
cases l₁

Result:
case mk
γ : Type u_1
δ : Type u_2
α : Type u_1
β : Type u_2
μ : Type u_3
f : Option γ → Option δ → μ
g : α → γ
h : β → δ
l₂ : Array β
toList✝ : List α
⊢ zipWithAll f (map g { toList := toList✝ }) (map h l₂) =
    zipWithAll (fun a b => f (g <$> a) (h <$> b)) { toList := toList✝ } l₂

Proof state:
case mk
γ : Type u_1
δ : Type u_2
α : Type u_1
β : Type u_2
μ : Type u_3
f : Option γ → Option δ → μ
g : α → γ
h : β → δ
l₂ : Array β
toList✝ : List α
⊢ zipWithAll f (map g { toList := toList✝ }) (map h l₂) =
    zipWithAll (fun a b => f (g <$> a) (h <$> b)) { toList := toList✝ } l₂

Tactic:
cases l₂

Result:
case mk.mk
γ : Type u_1
δ : Type u_2
α : Type u_1
β : Type u_2
μ : Type u_3
f : Option γ → Option δ → μ
g : α → γ
h : β → δ
toList✝¹ : List α
toList✝ : List β
⊢ zipWithAll f (map g { toList := toList✝¹ }) (map h { toList := toList✝ }) =
    zipWithAll (fun a b => f (g <$> a) (h <$> b)) { toList := toList✝¹ } { toList := toList✝ }

Proof state:
case mk.mk
γ : Type u_1
δ : Type u_2
α : Type u_1
β : Type u_2
μ : Type u_3
f : Option γ → Option δ → μ
g : α → γ
h : β → δ
toList✝¹ : List α
toList✝ : List β
⊢ zipWithAll f (map g { toList := toList✝¹ }) (map h { toList := toList✝ }) =
    zipWithAll (fun a b => f (g <$> a) (h <$> b)) { toList := toList✝¹ } { toList := toList✝ }

Tactic:
simp [List.zipWithAll_map]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
@[simp]
lemma densityProcess_empty (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ) (a : α) (x : γ) :
    densityProcess κ ν n a x ∅ = 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
a : α
x : γ
⊢ κ.densityProcess ν n a x ∅ = 0

Tactic:
simp [densityProcess]

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
lemma strongConcaveOn_iff_convex :
    StrongConcaveOn s m f ↔ ConcaveOn ℝ s fun x ↦ f x + m / (2 : ℝ) * ‖x‖ ^ 2

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
⊢ StrongConcaveOn s m f ↔ ConcaveOn ℝ s fun x => f x + m / 2 * ‖x‖ ^ 2

Tactic:
refine and_congr_right fun _ ↦ forall₄_congr fun x _ y _ ↦ forall₅_congr fun a b ha hb hab ↦ ?_

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
x✝² : Convex ℝ s
x : E
x✝¹ : x ∈ s
y : E
x✝ : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y + a * b * (fun r => m / 2 * r ^ 2) ‖x - y‖ ≤ f (a • x + b • y) ↔
    a • (fun x => f x + m / 2 * ‖x‖ ^ 2) x + b • (fun x => f x + m / 2 * ‖x‖ ^ 2) y ≤
      (fun x => f x + m / 2 * ‖x‖ ^ 2) (a • x + b • y)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
x✝² : Convex ℝ s
x : E
x✝¹ : x ∈ s
y : E
x✝ : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y + a * b * (fun r => m / 2 * r ^ 2) ‖x - y‖ ≤ f (a • x + b • y) ↔
    a • (fun x => f x + m / 2 * ‖x‖ ^ 2) x + b • (fun x => f x + m / 2 * ‖x‖ ^ 2) y ≤
      (fun x => f x + m / 2 * ‖x‖ ^ 2) (a • x + b • y)

Tactic:
simp_rw [← sub_le_iff_le_add, smul_eq_mul, aux_add ha hb hab, mul_assoc, mul_left_comm]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
theorem mk_num_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = n /. d) : n ≠ 0 :=
  fun this => hq <| by simpa [this] using hqnd

Proof state:
q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : n = 0
⊢ q = 0

Tactic:
simpa [this] using hqnd

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem sup_left_comm (a b c : α) : a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)

Tactic:
rw [← sup_assoc, ← sup_assoc, @sup_comm α _ a]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ico_add_one_add_one_eq_Ioc_of_not_isMax (hb : ¬ IsMax b) (a : α) :
    Ico (a + 1) (b + 1) = Ioc a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico (a + 1) (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_succ_eq_Ioc_of_not_isMax hb a

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem isLittleO_rpow_exp_atTop (s : ℝ) : (fun x : ℝ => x ^ s) =o[atTop] exp

Proof state:
s : ℝ
⊢ (fun x => x ^ s) =o[atTop] rexp

Tactic:
simpa only [one_mul] using isLittleO_rpow_exp_pos_mul_atTop s one_pos

Result:
no goals
-- Mathlib/Data/Fin/VecNotation.lean
theorem range_cons_cons_empty (x y : α) (u : Fin 0 → α) :
    Set.range (vecCons x <| vecCons y u) = {x, y}

Proof state:
α : Type u
x y : α
u : Fin 0 → α
⊢ Set.range (vecCons x (vecCons y u)) = {x, y}

Tactic:
rw [range_cons, range_cons_empty, Set.singleton_union]

Result:
no goals
-- Mathlib/CategoryTheory/DifferentialObject.lean
theorem eqToHom_f {X Y : DifferentialObject S C} (h : X = Y) :
    Hom.f (eqToHom h) = eqToHom (congr_arg _ h)

Proof state:
S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ (eqToHom ⋯).f = eqToHom ⋯

Tactic:
rw [eqToHom_refl, eqToHom_refl]

Result:
S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ (𝟙 X).f = 𝟙 X.obj

Proof state:
S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ (𝟙 X).f = 𝟙 X.obj

Tactic:
rfl

Result:
no goals

Proof state:
S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X Y : DifferentialObject S C
h : X = Y
⊢ (eqToHom h).f = eqToHom ⋯

Tactic:
subst h

Result:
S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ (eqToHom ⋯).f = eqToHom ⋯
-- Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean
theorem transcendental_adjoin {s : Set ι} {i : ι} (hi : i ∉ s) :
    Transcendental (adjoin R (x '' s)) (x i)

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
s : Set ι
i : ι
hi : i ∉ s
⊢ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
convert ← hx.adjoin_of_disjoint (Set.disjoint_singleton_right.mpr hi)

Result:
case a
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
s : Set ι
i : ι
hi : i ∉ s
⊢ (AlgebraicIndependent ↥(adjoin R (x '' s)) fun i_1 => x ↑i_1) ↔ Transcendental (↥(adjoin R (x '' s))) (x i)

Proof state:
case a
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
s : Set ι
i : ι
hi : i ∉ s
⊢ (AlgebraicIndependent ↥(adjoin R (x '' s)) fun i_1 => x ↑i_1) ↔ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
rw [algebraicIndependent_singleton_iff ⟨i, rfl⟩]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_restrict_union_iff (s t : Set α) (p : α → Prop) :
    (∀ᵐ x ∂μ.restrict (s ∪ t), p x) ↔ (∀ᵐ x ∂μ.restrict s, p x) ∧ ∀ᵐ x ∂μ.restrict t, p x

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict (s ∪ t), p x) ↔ (∀ᵐ (x : α) ∂μ.restrict s, p x) ∧ ∀ᵐ (x : α) ∂μ.restrict t, p x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List ((a : α) × β a)} {k : α}
    (contains_eq_false : (l.map Sigma.fst).contains k = false)
    {h'} :
    (m.insertMany l).getKey k h' =
      m.getKey k (mem_of_mem_insertMany_list h h' contains_eq_false)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List ((a : α) × β a)
k : α
contains_eq_false : (List.map Sigma.fst l).contains k = false
h' : k ∈ m.insertMany l
⊢ (m.insertMany l).getKey k h' = m.getKey k ⋯

Tactic:
simp_to_raw using Raw₀.getKey_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma toENNReal_eq_zero_iff {x : EReal} : x.toENNReal = 0 ↔ x ≤ 0

Proof state:
x : EReal
⊢ x.toENNReal = 0 ↔ x ≤ 0

Tactic:
induction x <;> simp [toENNReal]

Result:
no goals
-- Mathlib/RingTheory/Perfection.lean
theorem pthRoot_frobenius : (pthRoot R p).comp (frobenius _ p) = RingHom.id _ :=
  RingHom.ext fun x =>
    ext fun n => by rw [RingHom.comp_apply, RingHom.id_apply, coeff_pthRoot, coeff_frobenius]

Proof state:
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x : Ring.Perfection R p
n : ℕ
⊢ (coeff R p n) (((pthRoot R p).comp (frobenius (Ring.Perfection R p) p)) x) =
    (coeff R p n) ((RingHom.id (Ring.Perfection R p)) x)

Tactic:
rw [RingHom.comp_apply, RingHom.id_apply, coeff_pthRoot, coeff_frobenius]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean
theorem nhds_basis_ball {x : E} : (𝓝 x).HasBasis (fun r : ℝ => 0 < r) (ball x)

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (𝓝 x).HasBasis (fun r => 0 < r) (ball x)

Tactic:
rw [toEuclidean.toHomeomorph.nhds_eq_comap x]

Result:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (Filter.comap (⇑toEuclidean.toHomeomorph) (𝓝 (toEuclidean.toHomeomorph x))).HasBasis (fun r => 0 < r) (ball x)

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (Filter.comap (⇑toEuclidean.toHomeomorph) (𝓝 (toEuclidean.toHomeomorph x))).HasBasis (fun r => 0 < r) (ball x)

Tactic:
exact Metric.nhds_basis_ball.comap _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem sat_relabel {f : CNF α} (h : Sat (r1 ∘ r2) f) : Sat r1 (relabel r2 f)

Proof state:
α : Type u_1
β✝ : Type u_2
r1 : β✝ → Bool
r2 : α → β✝
f : CNF α
h : Sat (r1 ∘ r2) f
⊢ Sat r1 (relabel r2 f)

Tactic:
simp_all [sat_def]

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
@[simp]
lemma factoredNumbers_empty : factoredNumbers ∅ = {1}

Proof state:
⊢ factoredNumbers ∅ = {1}

Tactic:
ext m

Result:
case h
m : ℕ
⊢ m ∈ factoredNumbers ∅ ↔ m ∈ {1}

Proof state:
case h
m : ℕ
⊢ m ∈ factoredNumbers ∅ ↔ m ∈ {1}

Tactic:
simp only [mem_factoredNumbers, Finset.not_mem_empty, ← List.eq_nil_iff_forall_not_mem,
  primeFactorsList_eq_nil, and_or_left, not_and_self_iff, ne_and_eq_iff_right zero_ne_one,
  false_or, Set.mem_singleton_iff]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem countP_filter (q) [DecidablePred q] (s : Multiset α) :
    countP p (filter q s) = countP (fun a => p a ∧ q a) s

Proof state:
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
⊢ countP p (filter q s) = countP (fun a => p a ∧ q a) s

Tactic:
simp [countP_eq_card_filter]

Result:
no goals
-- Mathlib/Data/Int/Sqrt.lean
theorem sqrt_eq (n : ℤ) : sqrt (n * n) = n.natAbs

Proof state:
n : ℤ
⊢ sqrt (n * n) = ↑n.natAbs

Tactic:
rw [sqrt, ← natAbs_mul_self, toNat_natCast, Nat.sqrt_eq]

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem dropFun_of_subtype {α} (p : α ⟹ «repeat» (n + 1) Prop) :
    dropFun (ofSubtype p) = ofSubtype _

Proof state:
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
⊢ dropFun (ofSubtype p) = ofSubtype (dropFun p)

Tactic:
ext i : 2

Result:
case a.h
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
i : Fin2 n
x✝ : (Subtype_ p).drop i
⊢ dropFun (ofSubtype p) i x✝ = ofSubtype (dropFun p) i x✝

Proof state:
case a.h
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
i : Fin2 n
x✝ : (Subtype_ p).drop i
⊢ dropFun (ofSubtype p) i x✝ = ofSubtype (dropFun p) i x✝

Tactic:
induction i <;> simp [dropFun, *] <;> rfl

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsRestriction.eq_restrict (h : N ≤r M) : M ↾ N.E = N

Proof state:
α : Type u_1
M N : Matroid α
h : N ≤r M
⊢ M ↾ N.E = N

Tactic:
obtain ⟨R, -, rfl⟩ := h

Result:
case intro.intro
α : Type u_1
M : Matroid α
R : Set α
⊢ M ↾ (M ↾ R).E = M ↾ R

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
R : Set α
⊢ M ↾ (M ↾ R).E = M ↾ R

Tactic:
rw [restrict_ground_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
@[simp]
lemma shiftMap_zero (X Y : C) (n a a' : M) (ha' : n + a = a') :
    F.shiftMap (0 : X ⟶ Y⟦n⟧) a a' ha' = 0

Proof state:
C : Type u_1
A : Type u_2
inst✝⁸ : Category.{u_6, u_1} C
inst✝⁷ : Category.{u_5, u_2} A
F : C ⥤ A
M : Type u_3
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : F.ShiftSequence M
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms A
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (n : M), (shiftFunctor C n).PreservesZeroMorphisms
X Y : C
n a a' : M
ha' : n + a = a'
⊢ F.shiftMap 0 a a' ha' = 0

Tactic:
simp [shiftMap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_one_zero : testBit 1 0 = true

Proof state:
⊢ testBit 1 0 = true

Tactic:
trivial

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/HermitianFunctionalCalculus.lean
lemma cfcAux_id : hA.cfcAux (.restrict (spectrum ℝ A) (.id ℝ)) = A

Proof state:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ hA.cfcAux (ContinuousMap.restrict (spectrum ℝ A) (ContinuousMap.id ℝ)) = A

Tactic:
conv_rhs => rw [hA.spectral_theorem]

Result:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ hA.cfcAux (ContinuousMap.restrict (spectrum ℝ A) (ContinuousMap.id ℝ)) =
    ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary

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

Tactic:
congr!

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ioo_pred_right_eq_insert (h : a < b) : Ioo (pred a) b = insert a (Ioo a b)

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
h : a < b
⊢ Ioo (pred a) b = insert a (Ioo a b)

Tactic:
simp_rw [← Ioi_inter_Iio, Ioi_pred_eq_insert, insert_inter_of_mem (mem_Iio.2 h)]

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem inl_pow [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r : R)
    (n : ℕ) : (inl r ^ n : tsze R M) = inl (r ^ n) :=
  ext rfl <| by simp [snd_pow_eq_sum, List.map_const']

Proof state:
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r : R
n : ℕ
⊢ (inl r ^ n).snd = (inl (r ^ n)).snd

Tactic:
simp [snd_pow_eq_sum, List.map_const']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem take_size (a : Array α) : a.take a.size = a

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.take { toList := toList✝ }.size = { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : Array α
⊢ a.take a.size = a

Tactic:
cases a

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.take { toList := toList✝ }.size = { toList := toList✝ }
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem toLp_sub (f g : α →ₛ E) (hf : MemLp f p μ) (hg : MemLp g p μ) :
    toLp (f - g) (hf.sub hg) = toLp f hf - toLp g hg

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α →ₛ E
hf : MemLp (⇑f) p μ
hg : MemLp (⇑g) p μ
⊢ toLp (f - g) ⋯ = toLp f hf - toLp g hg

Tactic:
simp only [sub_eq_add_neg, ← toLp_neg, ← toLp_add]

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem IsIntegral.pow {x : B} (h : IsIntegral R x) (n : ℕ) : IsIntegral R (x ^ n) :=
  .of_mem_of_fg _ h.fg_adjoin_singleton _ <|
    Subalgebra.pow_mem _ (by exact Algebra.subset_adjoin rfl) _

Proof state:
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
h : IsIntegral R x
n : ℕ
⊢ x ∈ Algebra.adjoin R {x}

Tactic:
exact Algebra.subset_adjoin rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem tendsto_rpow_div : Tendsto (fun x => x ^ ((1 : ℝ) / x)) atTop (𝓝 1)

Proof state:
case h.e'_3.h.h.e'_6.h.e'_6
x✝ : ℝ
⊢ x✝ = 1 * x✝ + 0

Tactic:
ring

Result:
no goals

Proof state:
⊢ Tendsto (fun x => x ^ (1 / x)) atTop (𝓝 1)

Tactic:
convert tendsto_rpow_div_mul_add (1 : ℝ) _ (0 : ℝ) zero_ne_one

Result:
case h.e'_3.h.h.e'_6.h.e'_6
x✝ : ℝ
⊢ x✝ = 1 * x✝ + 0
-- Mathlib/Dynamics/OmegaLimit.lean
theorem omegaLimit_image_eq {α' : Type*} (ϕ : τ → α' → β) (f : Filter τ) (g : α → α') :
    ω f ϕ (g '' s) = ω f (fun t x ↦ ϕ t (g x)) s

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
s : Set α
α' : Type u_5
ϕ : τ → α' → β
f : Filter τ
g : α → α'
⊢ ω f ϕ (g '' s) = ω f (fun t x => ϕ t (g x)) s

Tactic:
simp only [omegaLimit, image2_image_right]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem star_im : star a.im = -a.im + c₂ * a.imI

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a.im = -a.im + ↑c₂ * ↑a.imI

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
theorem ι_leftInverse : Function.LeftInverse ιInv (ι R : M → TensorAlgebra R M) := fun x ↦ by
  simp [ιInv]

Proof state:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ ιInv ((ι R) x) = x

Tactic:
simp [ιInv]

Result:
no goals
-- Mathlib/RingTheory/Bialgebra/Hom.lean
theorem coe_coalgHom_mk {f : A →ₗc[R] B} (h h₁) :
    ((⟨f, h, h₁⟩ : A →ₐc[R] B) : A →ₗc[R] B) = f

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : CoalgebraStruct R A
inst✝ : CoalgebraStruct R B
f : A →ₗc[R] B
h : f.toFun 1 = 1
h₁ : ∀ (x y : A), f.toFun (x * y) = f.toFun x * f.toFun y
⊢ ↑{ toCoalgHom := f, map_one' := h, map_mul' := h₁ } = f

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive (attr := simp) one_nsmul]
lemma pow_one (a : M) : a ^ 1 = a

Proof state:
M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 1 = a

Tactic:
rw [pow_succ, pow_zero, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m] {t : RBNode α} :
    forIn (m := m) t init f = forIn t.toList init f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
α✝ : Type u_1
init : α✝
f : α → α✝ → m (ForInStep α✝)
inst✝¹ : Monad m
inst✝ : LawfulMonad m
t : RBNode α
⊢ forIn t init f = forIn t.toList init f

Tactic:
conv => lhs; simp only [forIn, RBNode.forIn]

Result:
m : Type u_1 → Type u_2
α : Type u_3
α✝ : Type u_1
init : α✝
f : α → α✝ → m (ForInStep α✝)
inst✝¹ : Monad m
inst✝ : LawfulMonad m
t : RBNode α
⊢ ForInStep.run <$> forIn.visit f t init = forIn t.toList init f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
α✝ : Type u_1
init : α✝
f : α → α✝ → m (ForInStep α✝)
inst✝¹ : Monad m
inst✝ : LawfulMonad m
t : RBNode α
⊢ ForInStep.run <$> forIn.visit f t init = forIn t.toList init f

Tactic:
rw [List.forIn_eq_bindList, forIn_visit_eq_bindList]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem not_unsat_nil : ¬Unsat ([] : CNF α) :=
  fun h => by simp [unsat_def] at h

Proof state:
α : Type u_1
h : Unsat []
⊢ False

Tactic:
simp [unsat_def] at h

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
@[simp]
lemma coverEntropyInf_empty {T : X → X} : coverEntropyInf T ∅ = ⊥

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
⊢ coverEntropyInf T ∅ = ⊥

Tactic:
simp only [coverEntropyInf, coverEntropyInfEntourage_empty, iSup_bot]

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem sup_def {c d : Con M} : c ⊔ d = conGen (⇑c ⊔ ⇑d)

Proof state:
M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ (conGen fun x y => c x y ∨ d x y) = conGen (⇑c ⊔ ⇑d)

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ c ⊔ d = conGen (⇑c ⊔ ⇑d)

Tactic:
rw [sup_eq_conGen]

Result:
M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ (conGen fun x y => c x y ∨ d x y) = conGen (⇑c ⊔ ⇑d)
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem coconePointsIsoOfNatIso_inv_desc {F G : J ⥤ C} {s : Cocone G} {r t : Cocone F}
    (P : IsColimit t) (Q : IsColimit s) (w : F ≅ G) :
    (coconePointsIsoOfNatIso P Q w).inv ≫ P.desc r = Q.map _ w.inv :=
  Q.hom_ext (by simp)

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F G : J ⥤ C
s : Cocone G
r t : Cocone F
P : IsColimit t
Q : IsColimit s
w : F ≅ G
⊢ ∀ (j : J), s.ι.app j ≫ (P.coconePointsIsoOfNatIso Q w).inv ≫ P.desc r = s.ι.app j ≫ Q.map r w.inv

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem nonpos_of_ge {a b : α} (h : b ≤ a) : variationOnFromTo f s a b ≤ 0

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
h : b ≤ a
⊢ variationOnFromTo f s a b ≤ 0

Tactic:
rw [variationOnFromTo.eq_neg_swap]

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
h : b ≤ a
⊢ -variationOnFromTo f s b a ≤ 0

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
h : b ≤ a
⊢ -variationOnFromTo f s b a ≤ 0

Tactic:
exact neg_nonpos_of_nonneg (variationOnFromTo.nonneg_of_le f s h)

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma div_le_one₀ (hb : 0 < b) : a / b ≤ 1 ↔ a ≤ b

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : MulPosMono G₀
hb : 0 < b
⊢ a / b ≤ 1 ↔ a ≤ b

Tactic:
rw [div_le_iff₀ hb, one_mul]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
theorem surjective_of_comp_eq_id : Surjective g :=
  .of_comp (g := f) <| by simp_rw [← coe_comp, h, id_coe, bijective_id.2]

Proof state:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g.comp f = id
⊢ Surjective (⇑g ∘ ⇑f)

Tactic:
simp_rw [← coe_comp, h, id_coe, bijective_id.2]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem derivative_apply (f : LaurentSeries V) : derivative R f = hasseDeriv R 1 f

Proof state:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : V⸨X⸩
⊢ (derivative R) f = (hasseDeriv R 1) f

Tactic:
exact rfl

Result:
no goals