harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem _root_.IsCompact.exists_isCompact_cthickening [LocallyCompactSpace α] (hs : IsCompact s) :
    ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s)

Proof state:
case intro.intro
α : Type u
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
⊢ ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s)

Tactic:
rcases hs.exists_cthickening_subset_open isOpen_interior hK with ⟨δ, δpos, hδ⟩

Result:
case intro.intro.intro.intro
α : Type u
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
δ : ℝ
δpos : 0 < δ
hδ : cthickening δ s ⊆ interior K
⊢ ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s)

Proof state:
α : Type u
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : LocallyCompactSpace α
hs : IsCompact s
⊢ ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s)

Tactic:
rcases exists_compact_superset hs with ⟨K, K_compact, hK⟩

Result:
case intro.intro
α : Type u
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
⊢ ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s)

Proof state:
case intro.intro.intro.intro
α : Type u
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
δ : ℝ
δpos : 0 < δ
hδ : cthickening δ s ⊆ interior K
⊢ IsCompact (cthickening δ s)

Tactic:
exact K_compact.of_isClosed_subset isClosed_cthickening (hδ.trans interior_subset)

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
δ : ℝ
δpos : 0 < δ
hδ : cthickening δ s ⊆ interior K
⊢ ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s)

Tactic:
refine ⟨δ, δpos, ?_⟩

Result:
case intro.intro.intro.intro
α : Type u
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
δ : ℝ
δpos : 0 < δ
hδ : cthickening δ s ⊆ interior K
⊢ IsCompact (cthickening δ s)
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem nhdsWithin_extChartAt_target_eq' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    𝓝[(extChartAt I x).target] extChartAt I x y = 𝓝[range I] extChartAt I x y :=
  nhdsWithin_extend_target_eq _ <| by rwa [← extChartAt_source I]

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ y ∈ (chartAt H x).source

Tactic:
rwa [← extChartAt_source I]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
lemma setIntegral_preCDF_fst (ρ : Measure (α × ℝ)) (r : ℚ) {s : Set α} (hs : MeasurableSet s)
    [IsFiniteMeasure ρ] :
    ∫ x in s, (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd r s).toReal

Proof state:
case hf
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ ∀ᵐ (x : α) ∂ρ.fst, preCDF ρ r x < ⊤

Tactic:
filter_upwards [preCDF_le_one ρ] with a ha

Result:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
a : α
ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ preCDF ρ r a < ⊤

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ ∫ (x : α) in s, (preCDF ρ r x).toReal ∂ρ.fst = ((ρ.IicSnd ↑r) s).toReal

Tactic:
rw [integral_toReal]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ (∫⁻ (a : α) in s, preCDF ρ r a ∂ρ.fst).toReal = ((ρ.IicSnd ↑r) s).toReal

case hfm
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ AEMeasurable (preCDF ρ r) (ρ.fst.restrict s)

case hf
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ ∀ᵐ (x : α) ∂ρ.fst.restrict s, preCDF ρ r x < ⊤

Proof state:
case hf
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ ∀ᵐ (x : α) ∂ρ.fst.restrict s, preCDF ρ r x < ⊤

Tactic:
refine ae_restrict_of_ae ?_

Result:
case hf
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ ∀ᵐ (x : α) ∂ρ.fst, preCDF ρ r x < ⊤

Proof state:
case hfm
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ AEMeasurable (preCDF ρ r) (ρ.fst.restrict s)

Tactic:
exact measurable_preCDF.aemeasurable

Result:
no goals

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
a : α
ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ preCDF ρ r a < ⊤

Tactic:
exact (ha r).trans_lt ENNReal.one_lt_top

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ (∫⁻ (a : α) in s, preCDF ρ r a ∂ρ.fst).toReal = ((ρ.IicSnd ↑r) s).toReal

Tactic:
rw [setLIntegral_preCDF_fst _ _ hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Pairwise.lean
theorem sublist_eq_map_getElem {l l' : List α} (h : l' <+ l) : ∃ is : List (Fin l.length),
    l' = is.map (l[·]) ∧ is.Pairwise (· < ·)

Proof state:
case slnil
α : Type u_1
l l' : List α
⊢ ∃ is, [] = map (fun x => [][x]) is ∧ Pairwise (fun x1 x2 => x1 < x2) is

Tactic:
exact ⟨[], by simp⟩

Result:
no goals

Proof state:
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
is : List (Fin l₂✝.length)
IH : l₁✝ = map (fun x => l₂✝[x]) is ∧ Pairwise (fun x1 x2 => x1 < x2) is
⊢ 0 < (a✝¹ :: l₂✝).length

Tactic:
simp [Nat.zero_lt_succ]

Result:
no goals

Proof state:
case cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
IH : ∃ is, l₁✝ = map (fun x => l₂✝[x]) is ∧ Pairwise (fun x1 x2 => x1 < x2) is
⊢ ∃ is, l₁✝ = map (fun x => (a✝¹ :: l₂✝)[x]) is ∧ Pairwise (fun x1 x2 => x1 < x2) is

Tactic:
let ⟨is, IH⟩ := IH

Result:
case cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
IH✝ : ∃ is, l₁✝ = map (fun x => l₂✝[x]) is ∧ Pairwise (fun x1 x2 => x1 < x2) is
is : List (Fin l₂✝.length)
IH : l₁✝ = map (fun x => l₂✝[x]) is ∧ Pairwise (fun x1 x2 => x1 < x2) is
⊢ ∃ is, l₁✝ = map (fun x => (a✝¹ :: l₂✝)[x]) is ∧ Pairwise (fun x1 x2 => x1 < x2) is

Proof state:
case cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
IH✝ : ∃ is, l₁✝ = map (fun x => l₂✝[x]) is ∧ Pairwise (fun x1 x2 => x1 < x2) is
is : List (Fin l₂✝.length)
IH : l₁✝ = map (fun x => l₂✝[x]) is ∧ Pairwise (fun x1 x2 => x1 < x2) is
⊢ l₁✝ = map (fun x => (a✝¹ :: l₂✝)[x]) (map (fun x => x.succ) is) ∧
    Pairwise (fun x1 x2 => x1 < x2) (map (fun x => x.succ) is)

Tactic:
simpa [Function.comp_def, pairwise_map]

Result:
no goals

Proof state:
case cons₂
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
IH : ∃ is, l₁✝ = map (fun x => l₂✝[x]) is ∧ Pairwise (fun x1 x2 => x1 < x2) is
⊢ ∃ is, a✝¹ :: l₁✝ = map (fun x => (a✝¹ :: l₂✝)[x]) is ∧ Pairwise (fun x1 x2 => x1 < x2) is

Tactic:
rcases IH with ⟨is,IH⟩

Result:
case cons₂.intro
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
is : List (Fin l₂✝.length)
IH : l₁✝ = map (fun x => l₂✝[x]) is ∧ Pairwise (fun x1 x2 => x1 < x2) is
⊢ ∃ is, a✝¹ :: l₁✝ = map (fun x => (a✝¹ :: l₂✝)[x]) is ∧ Pairwise (fun x1 x2 => x1 < x2) is

Proof state:
case cons₂.intro
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
is : List (Fin l₂✝.length)
IH : l₁✝ = map (fun x => l₂✝[x]) is ∧ Pairwise (fun x1 x2 => x1 < x2) is
⊢ a✝¹ :: l₁✝ = map (fun x => (a✝¹ :: l₂✝)[x]) (⟨0, ⋯⟩ :: map (fun x => x.succ) is) ∧
    Pairwise (fun x1 x2 => x1 < x2) (⟨0, ⋯⟩ :: map (fun x => x.succ) is)

Tactic:
simp [Function.comp_def, pairwise_map, IH, ← get_eq_getElem, get_cons_zero, get_cons_succ']

Result:
no goals

Proof state:
α : Type u_1
l l' : List α
⊢ [] = map (fun x => [][x]) [] ∧ Pairwise (fun x1 x2 => x1 < x2) []

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
theorem curryFinFinset_apply_const (hk : #s = k) (hl : #sᶜ = l) (f : G[×n]→L[𝕜] G')
    (x y : G) : (curryFinFinset 𝕜 G G' hk hl f (fun _ => x) fun _ => y) =
      f (s.piecewise (fun _ => x) fun _ => y)

Proof state:
𝕜 : Type u
n : ℕ
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
k l : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
x y : G
⊢ ((curryFinFinset 𝕜 G G' hk hl).symm ((curryFinFinset 𝕜 G G' hk hl) f)) (s.piecewise (fun x_1 => x) fun x => y) =
    f (s.piecewise (fun x_1 => x) fun x => y)

Tactic:
rw [LinearIsometryEquiv.symm_apply_apply]

Result:
no goals

Proof state:
𝕜 : Type u
n : ℕ
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
k l : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
x y : G
⊢ ((((curryFinFinset 𝕜 G G' hk hl) f) fun x_1 => x) fun x => y) = f (s.piecewise (fun x_1 => x) fun x => y)

Tactic:
refine (curryFinFinset_symm_apply_piecewise_const hk hl _ _ _).symm.trans ?_

Result:
𝕜 : Type u
n : ℕ
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
k l : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
x y : G
⊢ ((curryFinFinset 𝕜 G G' hk hl).symm ((curryFinFinset 𝕜 G G' hk hl) f)) (s.piecewise (fun x_1 => x) fun x => y) =
    f (s.piecewise (fun x_1 => x) fun x => y)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
@[simp]
lemma natDegree_polynomial [Nontrivial R] : W'.polynomial.natDegree = 2

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ { a := 0, b := 1, c := { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly,
          d := { a := -1, b := -W'.a₂, c := -W'.a₄, d := -W'.a₆ }.toPoly }.toPoly.natDegree =
    2

Tactic:
exact Cubic.natDegree_of_b_ne_zero' one_ne_zero

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ W'.polynomial.natDegree = 2

Tactic:
rw [polynomial_eq]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ { a := 0, b := 1, c := { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly,
          d := { a := -1, b := -W'.a₂, c := -W'.a₄, d := -W'.a₆ }.toPoly }.toPoly.natDegree =
    2
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_δ'' {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ Fin.castSucc j) :
    X.δ j.succ ≫ X.δ (i.castLT (Nat.lt_of_le_of_lt (Fin.le_iff_val_le_val.mp H) j.is_lt)) =
      X.δ i ≫ X.δ j

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ X.map (SimplexCategory.δ j.succ).op ≫ X.map (SimplexCategory.δ (i.castLT ⋯)).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.δ j).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ'' H]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ X.δ j.succ ≫ X.δ (i.castLT ⋯) = X.δ i ≫ X.δ j

Tactic:
dsimp [δ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ X.map (SimplexCategory.δ j.succ).op ≫ X.map (SimplexCategory.δ (i.castLT ⋯)).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.δ j).op
-- Mathlib/Data/Holor.lean
theorem mul_assoc0 [Semigroup α] (x : Holor α ds₁) (y : Holor α ds₂) (z : Holor α ds₃) :
    x ⊗ y ⊗ z = (x ⊗ (y ⊗ z)).assocLeft :=
  funext fun t : HolorIndex (ds₁ ++ ds₂ ++ ds₃) => by
    rw [assocLeft]
    unfold mul
    rw [mul_assoc, ← HolorIndex.take_take, ← HolorIndex.drop_take, ← HolorIndex.drop_drop,
      cast_type]
    · rfl
    rw [append_assoc]

Proof state:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ (x ⊗ y ⊗ z) t = cast ⋯ (x ⊗ (y ⊗ z)) t

Tactic:
unfold mul

Result:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.take.take * y t.take.drop * z t.drop = cast ⋯ (fun t => x t.take * (y t.drop.take * z t.drop.drop)) t

Proof state:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ (x ⊗ y ⊗ z) t = (x ⊗ (y ⊗ z)).assocLeft t

Tactic:
rw [assocLeft]

Result:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ (x ⊗ y ⊗ z) t = cast ⋯ (x ⊗ (y ⊗ z)) t

Proof state:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.assocRight.take * (y t.assocRight.drop.take * z t.assocRight.drop.drop) =
    (fun t => x (cast ⋯ t).take * (y (cast ⋯ t).drop.take * z (cast ⋯ t).drop.drop)) t

Tactic:
rfl

Result:
no goals

Proof state:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.take.take * y t.take.drop * z t.drop = cast ⋯ (fun t => x t.take * (y t.drop.take * z t.drop.drop)) t

Tactic:
rw [mul_assoc, ← HolorIndex.take_take, ← HolorIndex.drop_take, ← HolorIndex.drop_drop,
  cast_type]

Result:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.assocRight.take * (y t.assocRight.drop.take * z t.assocRight.drop.drop) =
    (fun t => x (cast ⋯ t).take * (y (cast ⋯ t).drop.take * z (cast ⋯ t).drop.drop)) t

case eq
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃

Proof state:
case eq
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃

Tactic:
rw [append_assoc]

Result:
no goals
-- Mathlib/Data/Matrix/Kronecker.lean
theorem kronecker_natCast [NonAssocSemiring α] [DecidableEq n] (A : Matrix l m α) (b : ℕ) :
    A ⊗ₖ (b : Matrix n n α) = blockDiagonal fun _ => b • A :=
  kronecker_diagonal _ _ |>.trans <| by
    congr! 2
    ext
    simp [(Nat.cast_commute b _).eq]

Proof state:
case h.e'_7.h
α : Type u_2
l : Type u_8
m : Type u_9
n : Type u_10
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
A : Matrix l m α
b : ℕ
x✝ : n
⊢ A <• ↑b = b •> A

Tactic:
ext

Result:
case h.e'_7.h.a
α : Type u_2
l : Type u_8
m : Type u_9
n : Type u_10
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
A : Matrix l m α
b : ℕ
x✝ : n
i✝ : l
j✝ : m
⊢ (A <• ↑b) i✝ j✝ = (b •> A) i✝ j✝

Proof state:
case h.e'_7.h.a
α : Type u_2
l : Type u_8
m : Type u_9
n : Type u_10
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
A : Matrix l m α
b : ℕ
x✝ : n
i✝ : l
j✝ : m
⊢ (A <• ↑b) i✝ j✝ = (b •> A) i✝ j✝

Tactic:
simp [(Nat.cast_commute b _).eq]

Result:
no goals

Proof state:
α : Type u_2
l : Type u_8
m : Type u_9
n : Type u_10
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
A : Matrix l m α
b : ℕ
⊢ (blockDiagonal fun i => A <• ↑b) = blockDiagonal fun x => b •> A

Tactic:
congr! 2

Result:
case h.e'_7.h
α : Type u_2
l : Type u_8
m : Type u_9
n : Type u_10
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
A : Matrix l m α
b : ℕ
x✝ : n
⊢ A <• ↑b = b •> A
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem EReal.tendsto_const_div_atTop_nhds_zero_nat {C : EReal} (h : C ≠ ⊥) (h' : C ≠ ⊤) :
    Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0)

Proof state:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
this : (fun n => C / ↑n) = fun n => ↑(C.toReal / ↑n)
⊢ Tendsto (fun n => C / ↑n) atTop (𝓝 0)

Tactic:
rw [this, ← coe_zero, tendsto_coe]

Result:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
this : (fun n => C / ↑n) = fun n => ↑(C.toReal / ↑n)
⊢ Tendsto (fun n => C.toReal / ↑n) atTop (𝓝 0)

Proof state:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
⊢ Tendsto (fun n => C / ↑n) atTop (𝓝 0)

Tactic:
have : (fun n : ℕ ↦ C / n) = fun n : ℕ ↦ ((C.toReal / n : ℝ) : EReal) := by
  ext n
  nth_rw 1 [← coe_toReal h' h, ← coe_coe_eq_natCast n, ← coe_div C.toReal n]

Result:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
this : (fun n => C / ↑n) = fun n => ↑(C.toReal / ↑n)
⊢ Tendsto (fun n => C / ↑n) atTop (𝓝 0)

Proof state:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
⊢ (fun n => C / ↑n) = fun n => ↑(C.toReal / ↑n)

Tactic:
ext n

Result:
case h
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
n : ℕ
⊢ C / ↑n = ↑(C.toReal / ↑n)

Proof state:
case h
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
n : ℕ
⊢ C / ↑n = ↑(C.toReal / ↑n)

Tactic:
nth_rw 1 [← coe_toReal h' h, ← coe_coe_eq_natCast n, ← coe_div C.toReal n]

Result:
no goals

Proof state:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
this : (fun n => C / ↑n) = fun n => ↑(C.toReal / ↑n)
⊢ Tendsto (fun n => C.toReal / ↑n) atTop (𝓝 0)

Tactic:
exact _root_.tendsto_const_div_atTop_nhds_zero_nat C.toReal

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem image_sub_const_Ico (h : c ≤ a) :
    ((Ico a b).image fun x => x - c) = Ico (a - c) (b - c)

Proof state:
case h
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ a_1 - c = x) ↔ a - c ≤ x ∧ x < b - c

Tactic:
refine ⟨?_, fun h ↦ ⟨x + c, by omega⟩⟩

Result:
case h
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ a_1 - c = x) → a - c ≤ x ∧ x < b - c

Proof state:
a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : a - c ≤ x ∧ x < b - c
⊢ (a ≤ x + c ∧ x + c < b) ∧ x + c - c = x

Tactic:
omega

Result:
no goals

Proof state:
a b c : ℕ
h : c ≤ a
⊢ image (fun x => x - c) (Ico a b) = Ico (a - c) (b - c)

Tactic:
ext x

Result:
case h
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ x ∈ image (fun x => x - c) (Ico a b) ↔ x ∈ Ico (a - c) (b - c)

Proof state:
case h.intro.intro
a b c : ℕ
h : c ≤ a
x : ℕ
hx : a ≤ x ∧ x < b
⊢ a - c ≤ x - c ∧ x - c < b - c

Tactic:
omega

Result:
no goals

Proof state:
case h
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ a_1 - c = x) → a - c ≤ x ∧ x < b - c

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case h.intro.intro
a b c : ℕ
h : c ≤ a
x : ℕ
hx : a ≤ x ∧ x < b
⊢ a - c ≤ x - c ∧ x - c < b - c

Proof state:
case h
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ x ∈ image (fun x => x - c) (Ico a b) ↔ x ∈ Ico (a - c) (b - c)

Tactic:
simp_rw [mem_image, mem_Ico]

Result:
case h
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ a_1 - c = x) ↔ a - c ≤ x ∧ x < b - c
-- Mathlib/Algebra/Module/Injective.lean
theorem ExtensionOfMaxAdjoin.extendIdealTo_wd (h : Module.Baer R Q) {y : N} (r r' : R)
    (eq1 : r • y = r' • y) : ExtensionOfMaxAdjoin.extendIdealTo i f h y r =
    ExtensionOfMaxAdjoin.extendIdealTo i f h y r'

Proof state:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r r' : R
eq1 : r • y = r' • y
⊢ (extendIdealTo i f h y) (r - r') = 0

Tactic:
convert ExtensionOfMaxAdjoin.extendIdealTo_wd' i f h (r - r') _

Result:
case convert_2
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r r' : R
eq1 : r • y = r' • y
⊢ (r - r') • y = 0

Proof state:
case convert_2
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r r' : R
eq1 : r • y = r' • y
⊢ (r - r') • y = 0

Tactic:
rw [sub_smul, sub_eq_zero, eq1]

Result:
no goals

Proof state:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r r' : R
eq1 : r • y = r' • y
⊢ (extendIdealTo i f h y) r = (extendIdealTo i f h y) r'

Tactic:
rw [← sub_eq_zero, ← map_sub]

Result:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r r' : R
eq1 : r • y = r' • y
⊢ (extendIdealTo i f h y) (r - r') = 0
-- Mathlib/NumberTheory/Ostrowski.lean
theorem equiv_real_or_padic (f : AbsoluteValue ℚ ℝ) (hf_nontriv : f.IsNontrivial) :
    f ≈ real ∨ ∃! p, ∃ (_ : Fact p.Prime), f ≈ (padic p)

Proof state:
case neg
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ¬∀ (n : ℕ), f ↑n ≤ 1
⊢ f ≈ real ∨ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Tactic:
exact .inl <| equiv_real_of_unbounded bdd

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
⊢ f ≈ real ∨ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Tactic:
by_cases bdd : ∀ n : ℕ, f n ≤ 1

Result:
case pos
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
⊢ f ≈ real ∨ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

case neg
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ¬∀ (n : ℕ), f ↑n ≤ 1
⊢ f ≈ real ∨ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Proof state:
case pos
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
⊢ f ≈ real ∨ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Tactic:
exact .inr <| equiv_padic_of_bounded hf_nontriv bdd

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem disjoint_assoc : Disjoint (a ⊓ b) c ↔ Disjoint a (b ⊓ c)

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint (a ⊓ b) c ↔ Disjoint a (b ⊓ c)

Tactic:
rw [disjoint_iff_inf_le, disjoint_iff_inf_le, inf_assoc]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean
theorem Complex.hasSum_sin (z : ℂ) :
    HasSum (fun n : ℕ => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) (Complex.sin z)

Proof state:
case h.e'_5
z : ℂ
⊢ (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) = fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I

Tactic:
simp_rw [mul_pow, pow_succ, pow_mul, Complex.I_sq, ← mul_assoc, mul_div_assoc, div_right_comm,
  div_self Complex.I_ne_zero, mul_comm _ ((-1 : ℂ) ^ _), mul_one_div, mul_div_assoc, mul_assoc]

Result:
no goals

Proof state:
z : ℂ
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) (sin z)

Tactic:
convert Complex.hasSum_sin' z using 1

Result:
case h.e'_5
z : ℂ
⊢ (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) = fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I