harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/W/Cardinal.lean
theorem cardinalMk_eq_sum_lift : #(WType β) = sum fun a ↦ #(WType β) ^ lift.{u} #(β a) :=
  (mk_congr <| equivSigma β).trans <| by
    simp_rw [mk_sigma, mk_arrow]; rw [lift_id'.{v, u}, lift_umax.{v, u}]

Proof state:
α : Type u
β : α → Type v
⊢ #((a : α) × (β a → WType β)) = sum fun a => #(WType β) ^ lift.{u, v} #(β a)

Tactic:
simp_rw [mk_sigma, mk_arrow]

Result:
α : Type u
β : α → Type v
⊢ (sum fun i => lift.{v, max u v} #(WType β) ^ lift.{max u v, v} #(β i)) = sum fun a => #(WType β) ^ lift.{u, v} #(β a)

Proof state:
α : Type u
β : α → Type v
⊢ (sum fun i => lift.{v, max u v} #(WType β) ^ lift.{max u v, v} #(β i)) = sum fun a => #(WType β) ^ lift.{u, v} #(β a)

Tactic:
rw [lift_id'.{v, u}, lift_umax.{v, u}]

Result:
no goals
-- Mathlib/ModelTheory/Order.lean
theorem realize_noTopOrder_iff : M ⊨ L.noTopOrderSentence ↔ NoTopOrder M

Proof state:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
⊢ NoTopOrder M →
    ∀ (a : M),
      ∃ a_1,
        ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) ≤
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0)

Tactic:
intro h a

Result:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
h : NoTopOrder M
a : M
⊢ ∃ a_1,
    ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) ≤
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0)

Proof state:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
⊢ (∀ (a : M),
      ∃ a_1,
        ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) ≤
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0)) ↔
    NoTopOrder M

Tactic:
refine ⟨fun h => ⟨fun a => h a⟩, ?_⟩

Result:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
⊢ NoTopOrder M →
    ∀ (a : M),
      ∃ a_1,
        ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) ≤
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0)

Proof state:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
⊢ M ⊨ L.noTopOrderSentence ↔ NoTopOrder M

Tactic:
simp only [noTopOrderSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_all,
  BoundedFormula.realize_ex, BoundedFormula.realize_not, Term.realize, Term.realize_le,
  Sum.elim_inr]

Result:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
⊢ (∀ (a : M),
      ∃ a_1,
        ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) ≤
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0)) ↔
    NoTopOrder M

Proof state:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
h : NoTopOrder M
a : M
⊢ ∃ a_1,
    ¬Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) ≤
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0)

Tactic:
exact exists_not_le a

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem card_filter_mem_Icc_le [Fintype ι] (x : ι → ℝ) :
    #{J ∈ π.boxes | x ∈ Box.Icc J} ≤ 2 ^ Fintype.card ι

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
inst✝ : Fintype ι
x : ι → ℝ
⊢ #(filter (fun J => x ∈ Box.Icc J) π.boxes) ≤ 2 ^ Fintype.card ι

Tactic:
rw [← Fintype.card_set]

Result:
ι : Type u_1
I : Box ι
π : Prepartition I
inst✝ : Fintype ι
x : ι → ℝ
⊢ #(filter (fun J => x ∈ Box.Icc J) π.boxes) ≤ Fintype.card (Set ι)

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
inst✝ : Fintype ι
x : ι → ℝ
⊢ #(filter (fun J => x ∈ Box.Icc J) π.boxes) ≤ Fintype.card (Set ι)

Tactic:
refine Finset.card_le_card_of_injOn (fun J : Box ι => { i | J.lower i = x i })
  (fun _ _ => Finset.mem_univ _) ?_

Result:
ι : Type u_1
I : Box ι
π : Prepartition I
inst✝ : Fintype ι
x : ι → ℝ
⊢ InjOn (fun J => {i | J.lower i = x i}) ↑(filter (fun J => x ∈ Box.Icc J) π.boxes)

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
inst✝ : Fintype ι
x : ι → ℝ
⊢ InjOn (fun J => {i | J.lower i = x i}) ↑(filter (fun J => x ∈ Box.Icc J) π.boxes)

Tactic:
simpa using π.injOn_setOf_mem_Icc_setOf_lower_eq x

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_ge_eq_iSup_nat_add (u : ℕ → α) (n : ℕ) : ⨆ i ≥ n, u i = ⨆ i, u (i + n)

Proof state:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), u (i + n) ≤ ⨆ i, ⨆ (_ : i ≥ n), u i

Tactic:
exact fun i => le_sSup ⟨i + n, iSup_pos (Nat.le_add_left _ _)⟩

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ (fun i => u (i + n)) (i - n) = u i

Tactic:
dsimp only

Result:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ u (i - n + n) = u i

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ i, ⨆ (_ : i ≥ n), u i = ⨆ i, u (i + n)

Tactic:
apply le_antisymm <;> simp only [iSup_le_iff]

Result:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ i ≥ n, u i ≤ ⨆ i, u (i + n)

case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), u (i + n) ≤ ⨆ i, ⨆ (_ : i ≥ n), u i

Proof state:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ u (i - n + n) = u i

Tactic:
rw [Nat.sub_add_cancel hi]

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ i ≥ n, u i ≤ ⨆ i, u (i + n)

Tactic:
refine fun i hi => le_sSup ⟨i - n, ?_⟩

Result:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ (fun i => u (i + n)) (i - n) = u i
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem _root_.MeasurableSet.exists_isCompact_isClosed_diff_lt [BorelSpace α] [R1Space α]
    [InnerRegularCompactLTTop μ] ⦃A : Set α⦄ (hA : MeasurableSet A) (h'A : μ A ≠ ∞)
    {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ K, K ⊆ A ∧ IsCompact K ∧ IsClosed K ∧ μ (A \ K) < ε

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : R1Space α
inst✝ : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
K : Set α
hKA : K ⊆ A
hKco : IsCompact K
hKcl : IsClosed K
hK : μ A < μ K + ε
⊢ ∃ K ⊆ A, IsCompact K ∧ IsClosed K ∧ μ (A \ K) < ε

Tactic:
exact ⟨K, hKA, hKco, hKcl, measure_diff_lt_of_lt_add hKcl.nullMeasurableSet hKA
  (ne_top_of_le_ne_top h'A <| measure_mono hKA) hK⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : R1Space α
inst✝ : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ K ⊆ A, IsCompact K ∧ IsClosed K ∧ μ (A \ K) < ε

Tactic:
rcases hA.exists_isCompact_isClosed_lt_add h'A hε with ⟨K, hKA, hKco, hKcl, hK⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : R1Space α
inst✝ : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
K : Set α
hKA : K ⊆ A
hKco : IsCompact K
hKcl : IsClosed K
hK : μ A < μ K + ε
⊢ ∃ K ⊆ A, IsCompact K ∧ IsClosed K ∧ μ (A \ K) < ε
-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_mem_iff {l : List (Option α)} {x : α} : x ∈ l.reduceOption ↔ some x ∈ l

Proof state:
α : Type u_1
l : List (Option α)
x : α
⊢ x ∈ l.reduceOption ↔ some x ∈ l

Tactic:
simp only [reduceOption, id, mem_filterMap, exists_eq_right]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem lipschitzOnWith_iff_dist_le_mul [PseudoMetricSpace α] [PseudoMetricSpace β] {K : ℝ≥0}
    {s : Set α} {f : α → β} :
    LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)) ↔
    ∀ x ∈ s, ∀ y ∈ s, ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)

Tactic:
norm_cast

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y

Tactic:
simp only [LipschitzOnWith, edist_nndist, dist_nndist]

Result:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)) ↔
    ∀ x ∈ s, ∀ y ∈ s, ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)
-- Mathlib/Data/Set/Image.lean
theorem mem_compl_image [BooleanAlgebra α] (t : α) (S : Set α) :
    t ∈ HasCompl.compl '' S ↔ tᶜ ∈ S

Proof state:
α : Type u_1
inst✝ : BooleanAlgebra α
t : α
S : Set α
⊢ t ∈ compl '' S ↔ tᶜ ∈ S

Tactic:
simp [← preimage_compl_eq_image_compl]

Result:
no goals
-- Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
theorem maxVar_bound [CompactSpace X] [Nonempty X] [CompactSpace Y] [Nonempty Y] :
    dist x y ≤ maxVar X Y :=
  calc
    dist x y ≤ diam (univ : Set (X ⊕ Y)) :=
      dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)
    _ = diam (range inl ∪ range inr : Set (X ⊕ Y))

Proof state:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
x y : X ⊕ Y
inst✝³ : CompactSpace X
inst✝² : Nonempty X
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ 1 * diam univ + 1 + 1 * diam univ ≤ 2 * diam univ + 1 + 2 * diam univ

Tactic:
gcongr <;> norm_num

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
x y : X ⊕ Y
inst✝³ : CompactSpace X
inst✝² : Nonempty X
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ diam univ + dist (inl default) (inr default) + diam univ =
    diam univ + (dist default default + 1 + dist default default) + diam univ

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
x y : X ⊕ Y
inst✝³ : CompactSpace X
inst✝² : Nonempty X
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ diam univ + (dist default default + 1 + dist default default) + diam univ = 1 * diam univ + 1 + 1 * diam univ

Tactic:
simp

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
x y : X ⊕ Y
inst✝³ : CompactSpace X
inst✝² : Nonempty X
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ diam univ = diam (range inl ∪ range inr)

Tactic:
rw [range_inl_union_range_inr]

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
x y : X ⊕ Y
inst✝³ : CompactSpace X
inst✝² : Nonempty X
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ diam (range inl) + dist (inl default) (inr default) + diam (range inr) =
    diam univ + (dist default default + 1 + dist default default) + diam univ

Tactic:
rw [isometry_inl.diam_range, isometry_inr.diam_range]

Result:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
x y : X ⊕ Y
inst✝³ : CompactSpace X
inst✝² : Nonempty X
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ diam univ + dist (inl default) (inr default) + diam univ =
    diam univ + (dist default default + 1 + dist default default) + diam univ
-- Mathlib/Algebra/Ring/Parity.lean
@[simp] lemma odd_add_self_one' : Odd (a + (a + 1))

Proof state:
α : Type u_2
inst✝ : Semiring α
a : α
⊢ Odd (a + (a + 1))

Tactic:
simp [← add_assoc]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
theorem tprod_pi_single [DecidableEq β] (b : β) (a : α) : ∏' b', Pi.mulSingle b a b' = a

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
⊢ Pi.mulSingle b a b = a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
b' : β
hb' : b' ≠ b
⊢ Pi.mulSingle b a b' = 1

Tactic:
simp [hb']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
⊢ ∏' (b' : β), Pi.mulSingle b a b' = a

Tactic:
rw [tprod_eq_mulSingle b]

Result:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
⊢ Pi.mulSingle b a b = a

α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
⊢ ∀ (b' : β), b' ≠ b → Pi.mulSingle b a b' = 1

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
⊢ ∀ (b' : β), b' ≠ b → Pi.mulSingle b a b' = 1

Tactic:
intro b' hb'

Result:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
b' : β
hb' : b' ≠ b
⊢ Pi.mulSingle b a b' = 1
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
lemma map_ι₀_eq_map_ι₁ {D : Type*} [Category D] (H : HomologicalComplex C c ⥤ D)
    (hH : (homotopyEquivalences C c).IsInvertedBy H) :
    H.map (ι₀ K) = H.map (ι₁ K)

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝³ : DecidableRel c.Rel
inst✝² : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝¹ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
D : Type u_3
inst✝ : Category.{u_4, u_3} D
H : HomologicalComplex C c ⥤ D
hH : (homotopyEquivalences C c).IsInvertedBy H
this : IsIso (H.map (π K))
⊢ H.map (ι₀ K) = H.map (ι₁ K)

Tactic:
simp only [← cancel_mono (H.map (cylinder.π K)), ← H.map_comp, ι₀_π, H.map_id, ι₁_π]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝³ : DecidableRel c.Rel
inst✝² : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝¹ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
D : Type u_3
inst✝ : Category.{u_4, u_3} D
H : HomologicalComplex C c ⥤ D
hH : (homotopyEquivalences C c).IsInvertedBy H
⊢ H.map (ι₀ K) = H.map (ι₁ K)

Tactic:
have : IsIso (H.map (cylinder.π K)) := hH _ ⟨homotopyEquiv K hc, rfl⟩

Result:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝³ : DecidableRel c.Rel
inst✝² : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝¹ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
D : Type u_3
inst✝ : Category.{u_4, u_3} D
H : HomologicalComplex C c ⥤ D
hH : (homotopyEquivalences C c).IsInvertedBy H
this : IsIso (H.map (π K))
⊢ H.map (ι₀ K) = H.map (ι₁ K)
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem C_eq (n : ℤ) : C R n = X * C R (n - 1) - C R (n - 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ C R n = X * C R (n - 1) - C R (n - 2)

Tactic:
linear_combination (norm := ring_nf) C_add_two R (n - 2)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem diam_eq_zero_of_unbounded (h : ¬IsBounded s) : diam s = 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
h : ¬Bornology.IsBounded s
⊢ diam s = 0

Tactic:
rw [diam, ediam_of_unbounded h, ENNReal.top_toReal]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
theorem comm_trans_rTensorOne :
    (TensorProduct.comm R _ _).trans M.rTensorOne = M.lTensorOne

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
x : R
h : (algebraMap R ↥⊥) x = r
⊢ ↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) (r ⊗ₜ[R] m) = ↑M.lTensorOne (r ⊗ₜ[R] m)

Tactic:
rw [← h]

Result:
case intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
x : R
h : (algebraMap R ↥⊥) x = r
⊢ ↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) ((algebraMap R ↥⊥) x ⊗ₜ[R] m) =
    ↑M.lTensorOne ((algebraMap R ↥⊥) x ⊗ₜ[R] m)

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
⊢ TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne = M.lTensorOne

Tactic:
refine LinearEquiv.toLinearMap_injective <| TensorProduct.ext' fun r m ↦ ?_

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
⊢ ↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) (r ⊗ₜ[R] m) = ↑M.lTensorOne (r ⊗ₜ[R] m)

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
x : R
h : (algebraMap R S) x = ↑r
⊢ ↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) (r ⊗ₜ[R] m) = ↑M.lTensorOne (r ⊗ₜ[R] m)

Tactic:
replace h : algebraMap R _ x = r := Subtype.val_injective h

Result:
case intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
x : R
h : (algebraMap R ↥⊥) x = r
⊢ ↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) (r ⊗ₜ[R] m) = ↑M.lTensorOne (r ⊗ₜ[R] m)

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
x : R
h : (algebraMap R ↥⊥) x = r
⊢ ↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) ((algebraMap R ↥⊥) x ⊗ₜ[R] m) =
    ↑M.lTensorOne ((algebraMap R ↥⊥) x ⊗ₜ[R] m)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
⊢ ↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) (r ⊗ₜ[R] m) = ↑M.lTensorOne (r ⊗ₜ[R] m)

Tactic:
obtain ⟨x, h⟩ := Algebra.mem_bot.1 r.2

Result:
case intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
r : ↥⊥
m : ↥M
x : R
h : (algebraMap R S) x = ↑r
⊢ ↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) (r ⊗ₜ[R] m) = ↑M.lTensorOne (r ⊗ₜ[R] m)
-- Mathlib/Algebra/Homology/ComplexShape.lean
lemma next_eq_self (c : ComplexShape ι) (j : ι) (hj : ¬ c.Rel j (c.next j)) :
    c.next j = j :=
  c.next_eq_self' j (fun k hk' => hj (by simpa only [c.next_eq' hk'] using hk'))

Proof state:
ι : Type u_1
c : ComplexShape ι
j : ι
hj : ¬c.Rel j (c.next j)
k : ι
hk' : c.Rel j k
⊢ c.Rel j (c.next j)

Tactic:
simpa only [c.next_eq' hk'] using hk'

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
lemma append_left_injective (h : x ++ₛ a = y ++ₛ b) (hl : x.length = y.length) : x = y

Proof state:
α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
i✝ : ℕ
h₁✝ : i✝ < x.length
h₂✝ : i✝ < y.length
⊢ x[i✝] = y[i✝]

Tactic:
rw [← get_append_left, ← get_append_left, h]

Result:
no goals

Proof state:
α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
⊢ ∀ (i : ℕ) (h₁ : i < x.length) (h₂ : i < y.length), x[i] = y[i]

Tactic:
intros

Result:
α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
i✝ : ℕ
h₁✝ : i✝ < x.length
h₂✝ : i✝ < y.length
⊢ x[i✝] = y[i✝]

Proof state:
α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
⊢ x = y

Tactic:
apply List.ext_getElem hl

Result:
α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
⊢ ∀ (i : ℕ) (h₁ : i < x.length) (h₂ : i < y.length), x[i] = y[i]
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem rootMultiplicity_expand_pow :
    (expand R (p ^ n) f).rootMultiplicity r = p ^ n * f.rootMultiplicity (r ^ p ^ n)

Proof state:
case inl
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
r : R
⊢ rootMultiplicity r ((expand R (p ^ n)) 0) = p ^ n * rootMultiplicity (r ^ p ^ n) 0

Tactic:
simp

Result:
no goals

Proof state:
case inr.intro.intro
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
conv_lhs => rw [hg, map_mul, map_pow, map_sub, expand_X, expand_C, map_pow, ← sub_pow_expChar_pow,
  ← pow_mul, mul_comm, rootMultiplicity_mul_X_sub_C_pow (expand_ne_zero (expChar_pow_pos R p n)
    |>.mpr <| right_ne_zero_of_mul <| hg ▸ h0), rootMultiplicity_eq_zero ndvd, zero_add]

Result:
no goals

Proof state:
case inr.intro.intro
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬X - C (r ^ p ^ n) ∣ g
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
rw [dvd_iff_isRoot, ← eval_X (x := r), ← eval_pow, ← isRoot_comp, ← expand_eq_comp_X_pow] at ndvd

Result:
case inr.intro.intro
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Proof state:
case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
obtain ⟨g, hg, ndvd⟩ := f.exists_eq_pow_rootMultiplicity_mul_and_not_dvd h0 (r ^ p ^ n)

Result:
case inr.intro.intro
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬X - C (r ^ p ^ n) ∣ g
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Proof state:
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
obtain rfl | h0 := eq_or_ne f 0

Result:
case inl
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
r : R
⊢ rootMultiplicity r ((expand R (p ^ n)) 0) = p ^ n * rootMultiplicity (r ^ p ^ n) 0

case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
@[simp]
lemma measure_add (f g : StieltjesFunction) : (f + g).measure = f.measure + g.measure

Proof state:
f g : StieltjesFunction
a b : ℝ
h : a < b
⊢ ofReal (↑f b + ↑g b - (↑f a + ↑g a)) = ofReal (↑f b - ↑f a) + ofReal (↑g b - ↑g a)

Tactic:
rw [← ENNReal.ofReal_add (sub_nonneg_of_le (f.mono h.le)) (sub_nonneg_of_le (g.mono h.le))]

Result:
f g : StieltjesFunction
a b : ℝ
h : a < b
⊢ ofReal (↑f b + ↑g b - (↑f a + ↑g a)) = ofReal (↑f b - ↑f a + (↑g b - ↑g a))

Proof state:
f g : StieltjesFunction
a b : ℝ
h : a < b
⊢ ofReal (↑f b + ↑g b - (↑f a + ↑g a)) = ofReal (↑f b - ↑f a + (↑g b - ↑g a))

Tactic:
ring_nf

Result:
no goals

Proof state:
f g : StieltjesFunction
⊢ (f + g).measure = f.measure + g.measure

Tactic:
refine Measure.ext_of_Ioc _ _ (fun a b h ↦ ?_)

Result:
f g : StieltjesFunction
a b : ℝ
h : a < b
⊢ (f + g).measure (Ioc a b) = (f.measure + g.measure) (Ioc a b)

Proof state:
f g : StieltjesFunction
a b : ℝ
h : a < b
⊢ (f + g).measure (Ioc a b) = (f.measure + g.measure) (Ioc a b)

Tactic:
simp only [measure_Ioc, add_apply, Measure.coe_add, Pi.add_apply]

Result:
f g : StieltjesFunction
a b : ℝ
h : a < b
⊢ ofReal (↑f b + ↑g b - (↑f a + ↑g a)) = ofReal (↑f b - ↑f a) + ofReal (↑g b - ↑g a)
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_symmDiff_symmDiff_comm : a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)

Tactic:
simp_rw [symmDiff_assoc, symmDiff_left_comm]

Result:
no goals