harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem eq_iff_prime_padicValNat_eq (a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) :
    a = b ↔ ∀ p : ℕ, p.Prime → padicValNat p a = padicValNat p b

Proof state:
case mp
a : ℕ
ha hb : a ≠ 0
⊢ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p a

Tactic:
simp

Result:
no goals

Proof state:
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b) → a = b

Tactic:
intro h

Result:
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
⊢ a = b

Proof state:
case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : ¬Prime p
⊢ a.factorization p = b.factorization p

Tactic:
simp [factorization_eq_zero_of_non_prime, pp]

Result:
no goals

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b ↔ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b

Tactic:
constructor

Result:
case mp
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b → ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b

case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b) → a = b

Proof state:
case mp
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b → ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b

Tactic:
rintro rfl

Result:
case mp
a : ℕ
ha hb : a ≠ 0
⊢ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p a

Proof state:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : Prime p
⊢ a.factorization p = b.factorization p

Tactic:
simp [factorization_def, pp, h p pp]

Result:
no goals

Proof state:
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
⊢ a.factorization p = b.factorization p

Tactic:
by_cases pp : p.Prime

Result:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : Prime p
⊢ a.factorization p = b.factorization p

case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : ¬Prime p
⊢ a.factorization p = b.factorization p

Proof state:
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
⊢ a = b

Tactic:
refine eq_of_factorization_eq ha hb fun p => ?_

Result:
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
⊢ a.factorization p = b.factorization p
-- Mathlib/Combinatorics/Additive/RuzsaCovering.lean
theorem ruzsa_covering_mul (hB : B.Nonempty) (hK : #(A * B) ≤ K * #B) :
    ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * (B / B)

Proof state:
case pos
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ insert a F ∈ C

Tactic:
rw [mem_filter, mem_powerset, insert_subset_iff, coe_insert]

Result:
case pos
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ (a ∈ A ∧ F ⊆ A) ∧ (insert a ↑F).PairwiseDisjoint fun x => x • B

Proof state:
case neg.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
a : G
ha : a ∈ A
hau : a ∉ F
b : G
hb : b ∈ F
c : G
hc₁ : a⁻¹ • c ∈ B
hc₂ : b⁻¹ • c ∈ B
⊢ a ∈ F * (B / B)

Tactic:
exact mem_mul.2 ⟨b, hb, b⁻¹ * a, mem_div.2 ⟨_, hc₂, _, hc₁, by simp⟩, by simp⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x => x • B)
C : Finset (Finset G) := filter (fun F => (↑F).PairwiseDisjoint fun x => x • B) A.powerset
F : Finset G
hFmax : ∀ x ∈ C, ¬F < x
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x => x • B
⊢ 0 < ↑(#B)

Tactic:
positivity

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem IsSwap.of_subtype_isSwap {p : α → Prop} [DecidablePred p] {f : Perm (Subtype p)}
    (h : f.IsSwap) : (ofSubtype f).IsSwap :=
  let ⟨⟨x, hx⟩, ⟨y, hy⟩, hxy⟩ := h
  ⟨x, y, by
    simp only [Ne, Subtype.ext_iff] at hxy
    exact hxy.1, by
    rw [hxy.2, ofSubtype_swap_eq]⟩

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩ ∧ f = swap ⟨x, hx⟩ ⟨y, hy⟩
⊢ ofSubtype f = swap x y

Tactic:
rw [hxy.2, ofSubtype_swap_eq]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩ ∧ f = swap ⟨x, hx⟩ ⟨y, hy⟩
⊢ x ≠ y

Tactic:
simp only [Ne, Subtype.ext_iff] at hxy

Result:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy : ¬x = y ∧ f = swap ⟨x, hx⟩ ⟨y, hy⟩
⊢ x ≠ y

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy : ¬x = y ∧ f = swap ⟨x, hx⟩ ⟨y, hy⟩
⊢ x ≠ y

Tactic:
exact hxy.1

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
theorem preCDF_le_one (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] :
    ∀ᵐ a ∂ρ.fst, ∀ r, preCDF ρ r a ≤ 1

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ ∀ (i : ℚ), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ 1

Tactic:
refine fun r ↦ ae_le_of_forall_setLIntegral_le_of_sigmaFinite measurable_preCDF fun s hs _ ↦ ?_

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
s : Set α
hs : MeasurableSet s
x✝ : ρ.fst s < ⊤
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, 1 ∂ρ.fst

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
s : Set α
hs : MeasurableSet s
x✝ : ρ.fst s < ⊤
⊢ (ρ.IicSnd ↑r) s ≤ ρ.fst s

Tactic:
exact Measure.IicSnd_le_fst ρ r s

Result:
no goals

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

Tactic:
simp only [Pi.one_apply, lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
s : Set α
hs : MeasurableSet s
x✝ : ρ.fst s < ⊤
⊢ (ρ.IicSnd ↑r) s ≤ ρ.fst s

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
s : Set α
hs : MeasurableSet s
x✝ : ρ.fst s < ⊤
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, 1 ∂ρ.fst

Tactic:
rw [setLIntegral_preCDF_fst ρ r hs]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
s : Set α
hs : MeasurableSet s
x✝ : ρ.fst s < ⊤
⊢ (ρ.IicSnd ↑r) s ≤ ∫⁻ (x : α) in s, 1 ∂ρ.fst

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, ∀ (r : ℚ), preCDF ρ r a ≤ 1

Tactic:
rw [ae_all_iff]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ ∀ (i : ℚ), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ 1
-- Mathlib/Topology/ContinuousOn.lean
theorem continuous_of_cover_nhds {ι : Sort*} {s : ι → Set α}
    (hs : ∀ x : α, ∃ i, s i ∈ 𝓝 x) (hf : ∀ i, ContinuousOn f (s i)) :
    Continuous f :=
  continuous_iff_continuousAt.mpr fun x ↦ let ⟨i, hi⟩ := hs x; by
    rw [ContinuousAt, ← nhdsWithin_eq_nhds.2 hi]
    exact hf _ _ (mem_of_mem_nhds hi)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Sort u_5
s : ι → Set α
hs : ∀ (x : α), ∃ i, s i ∈ 𝓝 x
hf : ∀ (i : ι), ContinuousOn f (s i)
x : α
i : ι
hi : s i ∈ 𝓝 x
⊢ Tendsto f (𝓝[s i] x) (𝓝 (f x))

Tactic:
exact hf _ _ (mem_of_mem_nhds hi)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Sort u_5
s : ι → Set α
hs : ∀ (x : α), ∃ i, s i ∈ 𝓝 x
hf : ∀ (i : ι), ContinuousOn f (s i)
x : α
i : ι
hi : s i ∈ 𝓝 x
⊢ ContinuousAt f x

Tactic:
rw [ContinuousAt, ← nhdsWithin_eq_nhds.2 hi]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Sort u_5
s : ι → Set α
hs : ∀ (x : α), ∃ i, s i ∈ 𝓝 x
hf : ∀ (i : ι), ContinuousOn f (s i)
x : α
i : ι
hi : s i ∈ 𝓝 x
⊢ Tendsto f (𝓝[s i] x) (𝓝 (f x))
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem braiding_tensor_left (X Y Z : C) :
    (β_ (X ⊗ Y) Z).hom  =
      (α_ X Y Z).hom ≫ X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫
        (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((α_ X Y Z).inv ≫ (β_ (X ⊗ Y) Z).hom) ≫ (α_ Z X Y).inv =
    ((α_ X Y Z).inv ≫ (α_ X Y Z).hom ≫ X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom) ≫
      (α_ Z X Y).inv

Tactic:
simp [hexagon_reverse]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ (X ⊗ Y) Z).hom = (α_ X Y Z).hom ≫ X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom

Tactic:
apply (cancel_epi (α_ X Y Z).inv).1

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ (β_ (X ⊗ Y) Z).hom =
    (α_ X Y Z).inv ≫ (α_ X Y Z).hom ≫ X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ (β_ (X ⊗ Y) Z).hom =
    (α_ X Y Z).inv ≫ (α_ X Y Z).hom ≫ X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom

Tactic:
apply (cancel_mono (α_ Z X Y).inv).1

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((α_ X Y Z).inv ≫ (β_ (X ⊗ Y) Z).hom) ≫ (α_ Z X Y).inv =
    ((α_ X Y Z).inv ≫ (α_ X Y Z).hom ≫ X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom) ≫
      (α_ Z X Y).inv
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_C_mul_X_le (a : R) : degree (C a * X) ≤ 1

Proof state:
R : Type u
inst✝ : Semiring R
a : R
⊢ (C a * X).degree ≤ 1

Tactic:
simpa only [pow_one] using degree_C_mul_X_pow_le 1 a

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma isStableUnderColimitsOfShape_iff_colimitsOfShape_le :
    W.IsStableUnderColimitsOfShape J ↔ W.colimitsOfShape J ≤ W

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
⊢ W.colimitsOfShape J ≤ W → W.IsStableUnderColimitsOfShape J

Tactic:
intro h _ _ _ _ h₁ h₂ f hf

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
h : W.colimitsOfShape J ≤ W
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cocone X₁✝
c₂✝ : Cocone X₂✝
h₁ : IsColimit c₁✝
h₂ : IsColimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W.functorCategory J f
⊢ W (h₁.desc { pt := c₂✝.pt, ι := f ≫ c₂✝.ι })

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
⊢ W.IsStableUnderColimitsOfShape J ↔ W.colimitsOfShape J ≤ W

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
⊢ W.IsStableUnderColimitsOfShape J → W.colimitsOfShape J ≤ W

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
⊢ W.colimitsOfShape J ≤ W → W.IsStableUnderColimitsOfShape J

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
⊢ W.IsStableUnderColimitsOfShape J → W.colimitsOfShape J ≤ W

Tactic:
rintro h _ _ _ ⟨_, _, _, _, h₁, h₂, f, hf⟩

Result:
case mp.mk
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
h : W.IsStableUnderColimitsOfShape J
X Y : C
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cocone X₁✝
c₂✝ : Cocone X₂✝
h₁ : IsColimit c₁✝
h₂ : IsColimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W.functorCategory J f
⊢ W (h₁.desc { pt := c₂✝.pt, ι := f ≫ c₂✝.ι })

Proof state:
case mp.mk
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
h : W.IsStableUnderColimitsOfShape J
X Y : C
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cocone X₁✝
c₂✝ : Cocone X₂✝
h₁ : IsColimit c₁✝
h₂ : IsColimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W.functorCategory J f
⊢ W (h₁.desc { pt := c₂✝.pt, ι := f ≫ c₂✝.ι })

Tactic:
exact h _ _ _ _ h₁ h₂ f hf

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
h : W.colimitsOfShape J ≤ W
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cocone X₁✝
c₂✝ : Cocone X₂✝
h₁ : IsColimit c₁✝
h₂ : IsColimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W.functorCategory J f
⊢ W (h₁.desc { pt := c₂✝.pt, ι := f ≫ c₂✝.ι })

Tactic:
exact h _ ⟨_, _, _, _, _, h₂, _, hf⟩

Result:
no goals
-- Mathlib/Topology/MetricSpace/Antilipschitz.lean
theorem antilipschitzWith_iff_le_mul_dist :
    AntilipschitzWith K f ↔ ∀ x y, dist x y ≤ K * dist (f x) (f y)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ AntilipschitzWith K f ↔ ∀ (x y : α), dist x y ≤ ↑K * dist (f x) (f y)

Tactic:
simp only [antilipschitzWith_iff_le_mul_nndist, dist_nndist]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) ↔ ∀ (x y : α), ↑(nndist x y) ≤ ↑K * ↑(nndist (f x) (f y))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) ↔ ∀ (x y : α), ↑(nndist x y) ≤ ↑K * ↑(nndist (f x) (f y))

Tactic:
norm_cast

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
lemma enorm_toLp {f : α → E} (hf : MemLp f p μ) : ‖hf.toLp f‖ₑ = eLpNorm f p μ

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
⊢ ‖MemLp.toLp f hf‖ₑ = eLpNorm f p μ

Tactic:
simp [enorm, nnnorm_toLp f hf, ENNReal.coe_toNNReal hf.2.ne]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_inv_natCast_pow (x : ℝ≥0) {n : ℕ} (hn : n ≠ 0) : (x ^ (n⁻¹ : ℝ)) ^ n = x

Proof state:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x

Tactic:
rw [← NNReal.coe_inj, NNReal.coe_pow, coe_rpow]

Result:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ (↑x ^ (↑n)⁻¹) ^ n = ↑x

Proof state:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ (↑x ^ (↑n)⁻¹) ^ n = ↑x

Tactic:
exact Real.rpow_inv_natCast_pow x.2 hn

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_pos_of_eval₂_root {p : R[X]} (hp : p ≠ 0) (f : R →+* S) {z : S}
    (hz : eval₂ f z p = 0) (inj : ∀ x : R, f x = 0 → x = 0) : 0 < natDegree p :=
  lt_of_not_ge fun hlt => by
    have A : p = C (p.coeff 0) := eq_C_of_natDegree_le_zero hlt
    rw [A, eval₂_C] at hz
    simp only [inj (p.coeff 0) hz, RingHom.map_zero] at A
    exact hp A

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : 0 ≥ p.natDegree
⊢ False

Tactic:
have A : p = C (p.coeff 0) := eq_C_of_natDegree_le_zero hlt

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : 0 ≥ p.natDegree
A : p = C (p.coeff 0)
⊢ False

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : f (p.coeff 0) = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : 0 ≥ p.natDegree
A : p = C (p.coeff 0)
⊢ False

Tactic:
simp only [inj (p.coeff 0) hz, RingHom.map_zero] at A

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : f (p.coeff 0) = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : 0 ≥ p.natDegree
A : p = 0
⊢ False

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : 0 ≥ p.natDegree
A : p = C (p.coeff 0)
⊢ False

Tactic:
rw [A, eval₂_C] at hz

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : f (p.coeff 0) = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : 0 ≥ p.natDegree
A : p = C (p.coeff 0)
⊢ False

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : f (p.coeff 0) = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : 0 ≥ p.natDegree
A : p = 0
⊢ False

Tactic:
exact hp A

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem circulantGraph_eq_symm : circulantGraph s = circulantGraph (s ∪ (-s))

Proof state:
G : Type u_1
inst✝ : AddGroup G
s : Set G
⊢ circulantGraph s = circulantGraph (s ∪ -s)

Tactic:
ext (u v : G)

Result:
case Adj.h.h.a
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
⊢ (circulantGraph s).Adj u v ↔ (circulantGraph (s ∪ -s)).Adj u v

Proof state:
case Adj.h.h.a
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
a✝ : u ≠ v
h : v - u ∈ s ∨ u - v ∈ s
⊢ u - v ∈ s ∨ v - u ∈ s

Tactic:
exact Or.symm h

Result:
no goals

Proof state:
case Adj.h.h.a
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
⊢ u ≠ v → v - u ∈ s ∨ u - v ∈ s → u - v ∈ s ∨ v - u ∈ s

Tactic:
intro _ h

Result:
case Adj.h.h.a
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
a✝ : u ≠ v
h : v - u ∈ s ∨ u - v ∈ s
⊢ u - v ∈ s ∨ v - u ∈ s

Proof state:
case Adj.h.h.a
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
⊢ (circulantGraph s).Adj u v ↔ (circulantGraph (s ∪ -s)).Adj u v

Tactic:
simp only [circulantGraph, fromRel_adj, Set.mem_union, Set.mem_neg, neg_sub, and_congr_right_iff,
  iff_self_or]

Result:
case Adj.h.h.a
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
⊢ u ≠ v → v - u ∈ s ∨ u - v ∈ s → u - v ∈ s ∨ v - u ∈ s
-- Mathlib/Data/List/Rotate.lean
theorem cyclicPermutations_rotate (l : List α) (k : ℕ) :
    (l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k

Proof state:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
⊢ (l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k

Tactic:
refine ext_get this fun n hn hn' => ?_

Result:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ (l.rotate k).cyclicPermutations.get ⟨n, hn⟩ = (l.cyclicPermutations.rotate k).get ⟨n, hn'⟩

Proof state:
case nil
α : Type u
k : ℕ
⊢ ([].rotate k).cyclicPermutations.length = ([].cyclicPermutations.rotate k).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ (l.rotate k).cyclicPermutations.get ⟨n, hn⟩ = (l.cyclicPermutations.rotate k).get ⟨n, hn'⟩

Tactic:
rw [get_rotate, get_cyclicPermutations, rotate_rotate, ← rotate_mod, Nat.add_comm]

Result:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ l.rotate ((↑⟨n, hn⟩ + k) % l.length) = l.cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % l.cyclicPermutations.length, ⋯⟩

Proof state:
case cons
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ ((head✝ :: tail✝).rotate k).cyclicPermutations.length = ((head✝ :: tail✝).cyclicPermutations.rotate k).length

Tactic:
rw [length_cyclicPermutations_of_ne_nil] <;> simp

Result:
no goals

Proof state:
α : Type u
l : List α
k : ℕ
⊢ (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length

Tactic:
cases l

Result:
case nil
α : Type u
k : ℕ
⊢ ([].rotate k).cyclicPermutations.length = ([].cyclicPermutations.rotate k).length

case cons
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ ((head✝ :: tail✝).rotate k).cyclicPermutations.length = ((head✝ :: tail✝).cyclicPermutations.rotate k).length

Proof state:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ l.rotate ((↑⟨n, hn⟩ + k) % l.length) = l.cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % l.cyclicPermutations.length, ⋯⟩

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Topology/Separation/Profinite.lean
theorem loc_compact_t2_tot_disc_iff_tot_sep :
    TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H

Proof state:
case mpr
H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallySeparatedSpace H → TotallyDisconnectedSpace H

Tactic:
apply TotallySeparatedSpace.totallyDisconnectedSpace

Result:
no goals

Proof state:
H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H

Tactic:
constructor

Result:
case mp
H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallyDisconnectedSpace H → TotallySeparatedSpace H

case mpr
H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallySeparatedSpace H → TotallyDisconnectedSpace H

Proof state:
case mp
H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallyDisconnectedSpace H → TotallySeparatedSpace H

Tactic:
intro h

Result:
case mp
H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
h : TotallyDisconnectedSpace H
⊢ TotallySeparatedSpace H

Proof state:
case mp
H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
h : TotallyDisconnectedSpace H
⊢ TotallySeparatedSpace H

Tactic:
exact totallySeparatedSpace_of_t1_of_basis_clopen loc_compact_Haus_tot_disc_of_zero_dim

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_inf_mul_relfinrank :
    A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
⊢ A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C

Tactic:
simpa using congr(toNat $(relrank_inf_mul_relrank A B C))

Result:
no goals