harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffOn.comp_contDiff {s : Set F} {g : F → G} {f : E → F} (hg : ContDiffOn 𝕜 n g s)
    (hf : ContDiff 𝕜 n f) (hs : ∀ x, f x ∈ s) : ContDiff 𝕜 n (g ∘ f)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set F
g : F → G
f : E → F
hg : ContDiffOn 𝕜 n g s
hf : ContDiffOn 𝕜 n f univ
hs : ∀ (x : E), f x ∈ s
⊢ ContDiffOn 𝕜 n (g ∘ f) univ

Tactic:
exact hg.comp hf fun x _ => hs x

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
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set F
g : F → G
f : E → F
hg : ContDiffOn 𝕜 n g s
hf : ContDiff 𝕜 n f
hs : ∀ (x : E), f x ∈ s
⊢ ContDiff 𝕜 n (g ∘ f)

Tactic:
rw [← contDiffOn_univ] 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
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set F
g : F → G
f : E → F
hg : ContDiffOn 𝕜 n g s
hf : ContDiffOn 𝕜 n f univ
hs : ∀ (x : E), f x ∈ s
⊢ ContDiffOn 𝕜 n (g ∘ f) univ
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem sizeUpTo_succ {i : ℕ} (h : i < c.length) :
    c.sizeUpTo (i + 1) = c.sizeUpTo i + c.blocks[i]

Proof state:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ c.sizeUpTo (i + 1) = c.sizeUpTo i + c.blocks[i]

Tactic:
simp only [sizeUpTo]

Result:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ (take (i + 1) c.blocks).sum = (take i c.blocks).sum + c.blocks[i]

Proof state:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ (take (i + 1) c.blocks).sum = (take i c.blocks).sum + c.blocks[i]

Tactic:
rw [sum_take_succ _ _ h]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ioo_sub_one_left_eq_Ioc_of_not_isMin (ha : ¬ IsMin a) (b : α) : Ioo (a - 1) b = Ico a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioo (a - 1) b = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioo_pred_left_eq_Ioc_of_not_isMin ha b

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem IsBigO.eq_zero_of_norm_pow {f : E'' → F''} {x₀ : E''} {n : ℕ}
    (h : f =O[𝓝 x₀] fun x => ‖x - x₀‖ ^ n) (hn : n ≠ 0) : f x₀ = 0

Proof state:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : E'' → F''
x₀ : E''
n : ℕ
h : f =O[𝓝 x₀] fun x => ‖x - x₀‖ ^ n
hn : n ≠ 0
⊢ f x₀ = 0

Tactic:
rw [← nhdsWithin_univ] at h

Result:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : E'' → F''
x₀ : E''
n : ℕ
h : f =O[𝓝[univ] x₀] fun x => ‖x - x₀‖ ^ n
hn : n ≠ 0
⊢ f x₀ = 0

Proof state:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : E'' → F''
x₀ : E''
n : ℕ
h : f =O[𝓝[univ] x₀] fun x => ‖x - x₀‖ ^ n
hn : n ≠ 0
⊢ f x₀ = 0

Tactic:
exact h.eq_zero_of_norm_pow_within (mem_univ _) hn

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem div_to_nat : ∀ n d, ((n / d : Num) : ℕ) = n / d
  | 0, 0 => by simp
  | 0, pos _ => (Nat.zero_div _).symm
  | pos _, 0 => (Nat.div_zero _).symm
  | pos _, pos _ => PosNum.div'_to_nat _ _

Proof state:
⊢ ↑(0 / 0) = ↑0 / ↑0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem isUnit_mk {a : M} : IsUnit (Associates.mk a) ↔ IsUnit a :=
  calc
    IsUnit (Associates.mk a) ↔ a ~ᵤ 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ IsUnit (Associates.mk a) ↔ a ~ᵤ 1

Tactic:
rw [isUnit_iff_eq_one, one_eq_mk_one, mk_eq_mk_iff_associated]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean
theorem toTensorAlgebra_galgebra_toFun (r : R) :
    TensorPower.toTensorAlgebra (DirectSum.GAlgebra.toFun (R := R) (A := fun n => ⨂[R]^n M) r) =
      algebraMap _ _ r

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ toTensorAlgebra (DirectSum.GAlgebra.toFun r) = (algebraMap R (TensorAlgebra R M)) r

Tactic:
rw [TensorPower.galgebra_toFun_def, TensorPower.algebraMap₀_eq_smul_one, LinearMap.map_smul,
  TensorPower.toTensorAlgebra_gOne, Algebra.algebraMap_eq_smul_one]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_sq (p : R[X]) : derivative (p ^ 2) = C 2 * p * derivative p

Proof state:
R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ derivative (p ^ 2) = C 2 * p * derivative p

Tactic:
rw [derivative_pow_succ, Nat.cast_one, one_add_one_eq_two, pow_one]

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem roots_expand : (expand R p f).roots = p • f.roots.map (frobeniusEquiv R p).symm

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
⊢ ((expand R p) f).roots = p • Multiset.map (⇑(frobeniusEquiv R p).symm) f.roots

Tactic:
conv_lhs => rw [← pow_one p, roots_expand_pow, iterateFrobeniusEquiv_eq_pow, pow_one]

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
⊢ p • Multiset.map (⇑(frobeniusEquiv R p ^ 1).symm) f.roots = p • Multiset.map (⇑(frobeniusEquiv R p).symm) f.roots

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
⊢ p • Multiset.map (⇑(frobeniusEquiv R p ^ 1).symm) f.roots = p • Multiset.map (⇑(frobeniusEquiv R p).symm) f.roots

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem lineDifferentiableWithinAt_smul_iff {c : 𝕜} (hc : c ≠ 0) :
    LineDifferentiableWithinAt 𝕜 f s x (c • v) ↔ LineDifferentiableWithinAt 𝕜 f s x v :=
  ⟨fun h ↦ by simpa [smul_smul, inv_mul_cancel₀ hc] using h.smul (c ⁻¹), fun h ↦ h.smul c⟩

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
s : Set E
x v : E
c : 𝕜
hc : c ≠ 0
h : LineDifferentiableWithinAt 𝕜 f s x (c • v)
⊢ LineDifferentiableWithinAt 𝕜 f s x v

Tactic:
simpa [smul_smul, inv_mul_cancel₀ hc] using h.smul (c ⁻¹)

Result:
no goals
-- Mathlib/RepresentationTheory/Basic.lean
theorem asAlgebraHom_single_one (g : G) : asAlgebraHom ρ (Finsupp.single g 1) = ρ g

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
⊢ ρ.asAlgebraHom (Finsupp.single g 1) = ρ g

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem forall_eq_of_chain [IsTrans α r] [IsAntisymm α r] (hs : Chain r s) {a b : α} (ha : a ∈ s)
    (hb : b ∈ s) : a = b

Proof state:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsAntisymm α r
hs : ∀ a ∈ s, ∀ b ∈ s, r a b
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b

Tactic:
exact antisymm (hs a ha b hb) (hs b hb a ha)

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsAntisymm α r
hs : Chain r s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b

Tactic:
rw [chain_iff_pairwise] at hs

Result:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsAntisymm α r
hs : ∀ a ∈ s, ∀ b ∈ s, r a b
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b
-- Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean
theorem UniqueMDiffOn.uniqueMDiffOn_target_inter (hs : UniqueMDiffOn I s) (x : M) :
    UniqueMDiffOn 𝓘(𝕜, E) ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
s : Set M
inst✝ : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
⊢ UniqueMDiffOn 𝓘(𝕜, E) (↑(extChartAt I x) '' (s ∩ (chartAt H x).source))

Tactic:
exact (hs.inter (chartAt H x).open_source).image_denseRange'
  (fun y hy ↦ hasMFDerivWithinAt_extChartAt hy.2)
  fun y hy ↦ ((mdifferentiable_chart _).mfderiv_surjective hy.2).denseRange

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
s : Set M
inst✝ : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
⊢ UniqueMDiffOn 𝓘(𝕜, E) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)

Tactic:
rw [← PartialEquiv.image_source_inter_eq', inter_comm, extChartAt_source]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
s : Set M
inst✝ : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
⊢ UniqueMDiffOn 𝓘(𝕜, E) (↑(extChartAt I x) '' (s ∩ (chartAt H x).source))
-- Mathlib/Order/Antisymmetrization.lean
theorem antisymmetrization_fibration :
    Relation.Fibration (· < ·) (· < ·) (@toAntisymmetrization α (· ≤ ·) _)

Proof state:
case mk
α : Type u_1
inst✝ : Preorder α
a : α
b✝ : Antisymmetrization α fun x1 x2 => x1 ≤ x2
b : α
h : Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 => x1 ≤ x2)) b < toAntisymmetrization (fun x1 x2 => x1 ≤ x2) a
⊢ ∃ a',
    (fun x1 x2 => x1 < x2) a' a ∧
      toAntisymmetrization (fun x1 x2 => x1 ≤ x2) a' = Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 => x1 ≤ x2)) b

Tactic:
exact ⟨b, h, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ Relation.Fibration (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) (toAntisymmetrization fun x1 x2 => x1 ≤ x2)

Tactic:
rintro a ⟨b⟩ h

Result:
case mk
α : Type u_1
inst✝ : Preorder α
a : α
b✝ : Antisymmetrization α fun x1 x2 => x1 ≤ x2
b : α
h : Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 => x1 ≤ x2)) b < toAntisymmetrization (fun x1 x2 => x1 ≤ x2) a
⊢ ∃ a',
    (fun x1 x2 => x1 < x2) a' a ∧
      toAntisymmetrization (fun x1 x2 => x1 ≤ x2) a' = Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 => x1 ≤ x2)) b
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem psum_one : psum σ R 1 = ∑ i, X i

Proof state:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ psum σ R 1 = ∑ i : σ, X i

Tactic:
simp [psum]

Result:
no goals
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
theorem ne_zero_of_order_ne_zero (hp : p.order ≠ 0) : p ≠ 0 := fun h => by simp [h] at hp

Proof state:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
hp : p.order ≠ 0
h : p = 0
⊢ False

Tactic:
simp [h] at hp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem cauchyPowerSeries_apply (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℕ) (w : ℂ) :
    (cauchyPowerSeries f c R n fun _ => w) =
      (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
w : ℂ
⊢ ((cauchyPowerSeries f c R n) fun x => w) = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z

Tactic:
simp only [cauchyPowerSeries, ContinuousMultilinearMap.mkPiRing_apply, Fin.prod_const,
  div_eq_mul_inv, mul_pow, mul_smul, circleIntegral.integral_smul]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
w : ℂ
⊢ (w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) =
    (2 * ↑π * I)⁻¹ • w ^ n • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
w : ℂ
⊢ (w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) =
    (2 * ↑π * I)⁻¹ • w ^ n • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z

Tactic:
rw [← smul_comm (w ^ n)]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem isUniformEmbedding_set_inclusion {s t : Set α} (hst : s ⊆ t) :
    IsUniformEmbedding (inclusion hst) where
  comap_uniformity

Proof state:
α : Type u
inst✝ : UniformSpace α
s t : Set α
hst : s ⊆ t
⊢ comap (fun x => (inclusion hst x.1, inclusion hst x.2)) (𝓤 ↑t) = 𝓤 ↑s

Tactic:
rw [uniformity_subtype, uniformity_subtype, comap_comap]

Result:
α : Type u
inst✝ : UniformSpace α
s t : Set α
hst : s ⊆ t
⊢ comap ((fun q => (↑q.1, ↑q.2)) ∘ fun x => (inclusion hst x.1, inclusion hst x.2)) (𝓤 α) =
    comap (fun q => (↑q.1, ↑q.2)) (𝓤 α)

Proof state:
α : Type u
inst✝ : UniformSpace α
s t : Set α
hst : s ⊆ t
⊢ comap ((fun q => (↑q.1, ↑q.2)) ∘ fun x => (inclusion hst x.1, inclusion hst x.2)) (𝓤 α) =
    comap (fun q => (↑q.1, ↑q.2)) (𝓤 α)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/UInt/Bitwise.lean
theorem Bool.toBitVec_toUInt32 {b : Bool} :
    b.toUInt32.toBitVec = (BitVec.ofBool b).setWidth 32

Proof state:
b : Bool
⊢ b.toUInt32.toBitVec = BitVec.setWidth 32 (BitVec.ofBool b)

Tactic:
cases b <;> simp [toUInt32]

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem Minpoly.toAdjoin_apply' (a : AdjoinRoot (minpoly R x)) :
    Minpoly.toAdjoin R x a =
      liftHom (minpoly R x) (⟨x, self_mem_adjoin_singleton R x⟩ : adjoin R ({x} : Set S))
        (by simp [← Subalgebra.coe_eq_zero, aeval_subalgebra_coe]) a :=
  rfl

Proof state:
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a : AdjoinRoot (minpoly R x)
⊢ (aeval ⟨x, ⋯⟩) (minpoly R x) = 0

Tactic:
simp [← Subalgebra.coe_eq_zero, aeval_subalgebra_coe]

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Iic : (some : α → WithTop α) '' Iic a = Iic (a : WithTop α)

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Iic a = Iic ↑a

Tactic:
rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Iic_subset_Iio.2 <| coe_lt_top a)]

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Finite.lean
@[simp]
lemma isRkFinite_ground_iff_rankFinite : M.IsRkFinite M.E ↔ M.RankFinite

Proof state:
α : Type u_1
M : Matroid α
⊢ M.IsRkFinite M.E ↔ M.RankFinite

Tactic:
rw [IsRkFinite, restrict_ground_eq_self]

Result:
no goals
-- Mathlib/GroupTheory/HNNExtension.lean
theorem of_mul_t (b : B) :
    (of (b : G) : HNNExtension G A B φ) * t = t * of (φ.symm b : G)

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ of ↑b * t = of ↑(φ (φ.symm b)) * t

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ of ↑b * t = t * of ↑(φ.symm b)

Tactic:
rw [t_mul_of]

Result:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ of ↑b * t = of ↑(φ (φ.symm b)) * t
-- Mathlib/Data/Matrix/Notation.lean
theorem vecMul_cons (v : Fin n.succ → α) (w : o' → α) (B : Fin n → o' → α) :
    v ᵥ* of (vecCons w B) = vecHead v • w + vecTail v ᵥ* of B

Proof state:
case h
α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
v : Fin n.succ → α
w : o' → α
B : Fin n → o' → α
i : o'
⊢ (v ᵥ* of (vecCons w B)) i = (vecHead v • w + vecTail v ᵥ* of B) i

Tactic:
simp [vecMul]

Result:
no goals

Proof state:
α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
v : Fin n.succ → α
w : o' → α
B : Fin n → o' → α
⊢ v ᵥ* of (vecCons w B) = vecHead v • w + vecTail v ᵥ* of B

Tactic:
ext i

Result:
case h
α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
v : Fin n.succ → α
w : o' → α
B : Fin n → o' → α
i : o'
⊢ (v ᵥ* of (vecCons w B)) i = (vecHead v • w + vecTail v ᵥ* of B) i
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
theorem eval₂_eq_sum_range :
    p.eval₂ f x = ∑ i ∈ Finset.range (p.natDegree + 1), f (p.coeff i) * x ^ i :=
  _root_.trans (congr_arg _ p.as_sum_range)
    (_root_.trans (eval₂_finset_sum f _ _ x) (congr_arg _ (by simp)))

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ (fun i => eval₂ f x ((monomial i) (p.coeff i))) = fun i => f (p.coeff i) * x ^ i

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousWithinAt_singleton : ContinuousWithinAt f {x} x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
⊢ ContinuousWithinAt f {x} x

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_singleton, tendsto_pure_nhds]

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra.lean
theorem lift_comp_ι (g : FreeAlgebra R X →ₐ[R] A) :
    lift R ((g : FreeAlgebra R X → A) ∘ ι R) = g

Proof state:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : FreeAlgebra R X →ₐ[R] A
⊢ (lift R) ((lift R).symm g) = g

Tactic:
exact (lift R).apply_symm_apply g

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : FreeAlgebra R X →ₐ[R] A
⊢ (lift R) (⇑g ∘ ι R) = g

Tactic:
rw [← lift_symm_apply]

Result:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : FreeAlgebra R X →ₐ[R] A
⊢ (lift R) ((lift R).symm g) = g
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_lt_one (hb : 0 < b) : a / b < 1 ↔ a < b

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
hb : 0 < b
⊢ a / b < 1 ↔ a < b

Tactic:
rw [div_lt_iff₀ hb, one_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallySurjective.lean
lemma isLocallySurjective_sheafToPresheaf_map_iff :
    Presheaf.IsLocallySurjective J ((sheafToPresheaf J A).map φ) ↔ IsLocallySurjective φ

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F₁ F₂ : Sheaf J A
φ : F₁ ⟶ F₂
⊢ Presheaf.IsLocallySurjective J ((sheafToPresheaf J A).map φ) ↔ IsLocallySurjective φ

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem zipWith_replicate {a : α} {b : β} {m n : Nat} :
    zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b)

Proof state:
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
a : α
b : β
m n : Nat
⊢ zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b)

Tactic:
rw [zipWith_eq_zipWith_take_min]

Result:
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
a : α
b : β
m n : Nat
⊢ zipWith f (take (min (replicate m a).length (replicate n b).length) (replicate m a))
      (take (min (replicate m a).length (replicate n b).length) (replicate n b)) =
    replicate (min m n) (f a b)

Proof state:
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
a : α
b : β
m n : Nat
⊢ zipWith f (take (min (replicate m a).length (replicate n b).length) (replicate m a))
      (take (min (replicate m a).length (replicate n b).length) (replicate n b)) =
    replicate (min m n) (f a b)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem HasDerivAt.le_of_lipschitzOn {f : 𝕜 → F} {f' : F} {x₀ : 𝕜} (hf : HasDerivAt f f' x₀)
    {s : Set 𝕜} (hs : s ∈ 𝓝 x₀) {C : ℝ≥0} (hlip : LipschitzOnWith C f s) : ‖f'‖ ≤ C

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x₀ : 𝕜
hf : HasDerivAt f f' x₀
s : Set 𝕜
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖f'‖ ≤ ↑C

Tactic:
simpa using HasFDerivAt.le_of_lipschitzOn hf.hasFDerivAt hs hlip

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Trunc.lean
theorem trunc'_map [CommSemiring S] (n : σ →₀ ℕ) (f : R →+* S) (p : MvPowerSeries σ R) :
    trunc' S n (map σ f p) = MvPolynomial.map f (trunc' R n p)

Proof state:
case a
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
n : σ →₀ ℕ
f : R →+* S
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc' S n) ((map σ f) p)) = MvPolynomial.coeff m ((MvPolynomial.map f) ((trunc' R n) p))

Tactic:
simp [coeff_trunc', MvPolynomial.coeff_map, apply_ite f]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
n : σ →₀ ℕ
f : R →+* S
p : MvPowerSeries σ R
⊢ (trunc' S n) ((map σ f) p) = (MvPolynomial.map f) ((trunc' R n) p)

Tactic:
ext m

Result:
case a
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
n : σ →₀ ℕ
f : R →+* S
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc' S n) ((map σ f) p)) = MvPolynomial.coeff m ((MvPolynomial.map f) ((trunc' R n) p))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get_ofList_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l)
    {h} :
    (ofList l).get k' h = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v :=
  Raw₀.get_insertMany_empty_list_of_mem k_beq distinct mem

Proof state:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h : k' ∈ ofList l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h : k' ∈ ofList l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h : k' ∈ ofList l
⊢ k = k'
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.one_right (ha : FiniteMultiplicity a 1) : multiplicity a 1 = 0

Proof state:
α : Type u_1
inst✝ : Monoid α
a : α
ha : FiniteMultiplicity a 1
⊢ multiplicity a 1 = 0

Tactic:
simp [ha.multiplicity_eq_iff, ha.not_dvd_of_one_right]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Pi.lean
lemma prod_indicator_const (s : Finset ι) (f : ι → Set κ) (g : κ → α) :
    ∏ i ∈ s, (f i).indicator g = (⋂ x ∈ s, f x).indicator (g ^ #s)

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : κ → α
⊢ ∏ i ∈ s, (f i).indicator g = (⋂ x ∈ s, f x).indicator (g ^ #s)

Tactic:
simp [prod_indicator]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem denom_div (p : K[X]) {q : K[X]} (hq : q ≠ 0) :
    denom (algebraMap _ _ p / algebraMap _ _ q) =
      Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)

Proof state:
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom =
    C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)

Tactic:
rw [denom, numDenom_div _ hq]

Result:
no goals