harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Homotopy/HomotopyGroup.lean
theorem inv_spec [Nonempty N] {i} {p : Ω^ N X x} :
    ((⟦p⟧)⁻¹ : HomotopyGroup N X x) = ⟦symmAt i p⟧

Proof state:
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p : ↑(Ω^ N X x)
⊢ (⟦p⟧)⁻¹ = ⟦fromLoop (Classical.arbitrary N) (Path.symm (toLoop (Classical.arbitrary N) p))⟧

Tactic:
apply Quotient.sound

Result:
case a
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p : ↑(Ω^ N X x)
⊢ (loopHomeo (Classical.arbitrary N)).symm (Path.symm ((loopHomeo (Classical.arbitrary N)).toEquiv p)) ≈
    fromLoop (Classical.arbitrary N) (Path.symm (toLoop (Classical.arbitrary N) p))

Proof state:
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p : ↑(Ω^ N X x)
⊢ (⟦p⟧)⁻¹ = ⟦symmAt i p⟧

Tactic:
rw [symmAt_indep (Classical.arbitrary N) p, ← fromLoop_symm_toLoop]

Result:
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p : ↑(Ω^ N X x)
⊢ (⟦p⟧)⁻¹ = ⟦fromLoop (Classical.arbitrary N) (Path.symm (toLoop (Classical.arbitrary N) p))⟧

Proof state:
case a
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p : ↑(Ω^ N X x)
⊢ (loopHomeo (Classical.arbitrary N)).symm (Path.symm ((loopHomeo (Classical.arbitrary N)).toEquiv p)) ≈
    fromLoop (Classical.arbitrary N) (Path.symm (toLoop (Classical.arbitrary N) p))

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem coe_iInf₂ (f : ∀ i, κ i → LowerSet α) :
    (↑(⨅ (i) (j), f i j) : Set α) = ⋂ (i) (j), f i j

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
f : (i : ι) → κ i → LowerSet α
⊢ ↑(⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)

Tactic:
simp_rw [coe_iInf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/List.lean
theorem mem_toList {a : α} {o : Option α} : a ∈ o.toList ↔ a ∈ o

Proof state:
α : Type u_1
a : α
o : Option α
⊢ a ∈ o.toList ↔ a ∈ o

Tactic:
cases o <;> simp [eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Depth.lean
theorem Balanced.le_size : @Balanced α t c n → 2 ^ depthLB c n ≤ t.size + 1
  | .nil => Nat.le_refl _
  | .red hl hr => by
    rw [size, Nat.add_right_comm (size _), Nat.add_assoc, depthLB, Nat.pow_succ, Nat.mul_two]
    exact Nat.add_le_add hl.le_size hr.le_size
  | .black hl hr => by
    rw [size, Nat.add_right_comm (size _), Nat.add_assoc, depthLB, Nat.pow_succ, Nat.mul_two]
    refine Nat.add_le_add (Nat.le_trans ?_ hl.le_size) (Nat.le_trans ?_ hr.le_size) <;>
      exact Nat.pow_le_pow_of_le_right (by decide) (depthLB_le ..)

Proof state:
α : Type u_1
t : RBNode α
c : RBColor
n✝ n : Nat
x✝ y✝ : RBNode α
v✝ : α
hl : x✝.Balanced black n
hr : y✝.Balanced black n
⊢ 2 ^ n + 2 ^ n ≤ x✝.size + 1 + (y✝.size + 1)

Tactic:
exact Nat.add_le_add hl.le_size hr.le_size

Result:
no goals

Proof state:
α : Type u_1
t : RBNode α
c : RBColor
n : Nat
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α
c₂✝ : RBColor
v✝ : α
hl : x✝.Balanced c₁✝ n✝
hr : y✝.Balanced c₂✝ n✝
⊢ 2 > 0

Tactic:
decide

Result:
no goals

Proof state:
α : Type u_1
t : RBNode α
c : RBColor
n : Nat
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α
c₂✝ : RBColor
v✝ : α
hl : x✝.Balanced c₁✝ n✝
hr : y✝.Balanced c₂✝ n✝
⊢ 2 ^ n✝ + 2 ^ n✝ ≤ x✝.size + 1 + (y✝.size + 1)

Tactic:
refine Nat.add_le_add (Nat.le_trans ?_ hl.le_size) (Nat.le_trans ?_ hr.le_size) <;>
  exact Nat.pow_le_pow_of_le_right (by decide) (depthLB_le ..)

Result:
no goals

Proof state:
α : Type u_1
t : RBNode α
c : RBColor
n✝ n : Nat
x✝ y✝ : RBNode α
v✝ : α
hl : x✝.Balanced black n
hr : y✝.Balanced black n
⊢ 2 ^ depthLB red n ≤ (node red x✝ v✝ y✝).size + 1

Tactic:
rw [size, Nat.add_right_comm (size _), Nat.add_assoc, depthLB, Nat.pow_succ, Nat.mul_two]

Result:
α : Type u_1
t : RBNode α
c : RBColor
n✝ n : Nat
x✝ y✝ : RBNode α
v✝ : α
hl : x✝.Balanced black n
hr : y✝.Balanced black n
⊢ 2 ^ n + 2 ^ n ≤ x✝.size + 1 + (y✝.size + 1)

Proof state:
α : Type u_1
t : RBNode α
c : RBColor
n : Nat
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α
c₂✝ : RBColor
v✝ : α
hl : x✝.Balanced c₁✝ n✝
hr : y✝.Balanced c₂✝ n✝
⊢ 2 ^ depthLB black (n✝ + 1) ≤ (node black x✝ v✝ y✝).size + 1

Tactic:
rw [size, Nat.add_right_comm (size _), Nat.add_assoc, depthLB, Nat.pow_succ, Nat.mul_two]

Result:
α : Type u_1
t : RBNode α
c : RBColor
n : Nat
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α
c₂✝ : RBColor
v✝ : α
hl : x✝.Balanced c₁✝ n✝
hr : y✝.Balanced c₂✝ n✝
⊢ 2 ^ n✝ + 2 ^ n✝ ≤ x✝.size + 1 + (y✝.size + 1)
-- Mathlib/Algebra/Group/Nat/Even.lean
@[simp] lemma not_even_one : ¬Even 1

Proof state:
⊢ ¬Even 1

Tactic:
simp [even_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem findSome?_toList (p : α → Option β) (as : Array α) :
    as.toList.findSome? p = as.findSome? p

Proof state:
α : Type u_1
β : Type u_2
p : α → Option β
as : Array α
⊢ List.findSome? p as.toList = findSome? p as

Tactic:
cases as

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Option β
toList✝ : List α
⊢ List.findSome? p { toList := toList✝ }.toList = findSome? p { toList := toList✝ }

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Option β
toList✝ : List α
⊢ List.findSome? p { toList := toList✝ }.toList = findSome? p { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
lemma term_delta (s : ℂ) (n : ℕ) : term δ s n = if n = 1 then 1 else 0

Proof state:
case inr
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term δ s n = if n = 1 then 1 else 0

Tactic:
rcases eq_or_ne n 1 with hn' | hn' <;>
simp [hn, hn', delta]

Result:
no goals

Proof state:
case inl
s : ℂ
⊢ term δ s 0 = if 0 = 1 then 1 else 0

Tactic:
simp

Result:
no goals

Proof state:
s : ℂ
n : ℕ
⊢ term δ s n = if n = 1 then 1 else 0

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case inl
s : ℂ
⊢ term δ s 0 = if 0 = 1 then 1 else 0

case inr
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term δ s n = if n = 1 then 1 else 0
-- Mathlib/Order/Heyting/Basic.lean
theorem himp_inf_distrib (a b c : α) : a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c) :=
  eq_of_forall_le_iff fun d => by simp_rw [le_himp_iff, le_inf_iff, le_himp_iff]

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⇨ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)

Tactic:
simp_rw [le_himp_iff, le_inf_iff, le_himp_iff]

Result:
no goals
-- Mathlib/Tactic/NormNum/Prime.lean
theorem isNat_minFac_2 : {a a' : ℕ} → IsNat a a' → a' % 2 = 0 → IsNat a.minFac 2
  | a, _, ⟨rfl⟩, h => ⟨by rw [cast_ofNat, minFac_eq_two_iff, Nat.dvd_iff_mod_eq_zero, h]⟩

Proof state:
a : ℕ
h : a % 2 = 0
⊢ a.minFac = ↑2

Tactic:
rw [cast_ofNat, minFac_eq_two_iff, Nat.dvd_iff_mod_eq_zero, h]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_diff_right : Icc a b \ {b} = Ico a b :=
  ext fun x => by simp [lt_iff_le_and_ne, and_assoc]

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b x : α
⊢ x ∈ Icc a b \ {b} ↔ x ∈ Ico a b

Tactic:
simp [lt_iff_le_and_ne, and_assoc]

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
theorem ContMDiffInv₀.of_le {m n : WithTop ℕ∞} (hmn : m ≤ n)
    [h : ContMDiffInv₀ I n G] : ContMDiffInv₀ I m G

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Inv G
inst✝ : Zero G
m n : WithTop ℕ∞
hmn : m ≤ n
h : ContMDiffInv₀ I n G
⊢ ContMDiffInv₀ I m G

Tactic:
exact ⟨fun x hx ↦ (h.contMDiffAt_inv₀ hx).of_le hmn⟩

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.mem_nhds_iff (hp : WithSeminorms p) (x : E) (U : Set E) :
    U ∈ 𝓝 x ↔ ∃ s : Finset ι, ∃ r > 0, (s.sup p).ball x r ⊆ U

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
U : Set E
⊢ U ∈ 𝓝 x ↔ ∃ s, ∃ r > 0, (s.sup p).ball x r ⊆ U

Tactic:
rw [hp.hasBasis_ball.mem_iff, Prod.exists]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem nat_add_iff : LiouvilleWith p (n + x) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
n : ℕ
⊢ LiouvilleWith p (↑n + x) ↔ LiouvilleWith p x

Tactic:
rw [add_comm, add_nat_iff]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
theorem tendsto_iff_coeff_tendsto [Semiring R] {ι : Type*}
    (f : ι → MvPowerSeries σ R) (u : Filter ι) (g : MvPowerSeries σ R) :
    Tendsto f u (nhds g) ↔
    ∀ d : σ →₀ ℕ, Tendsto (fun i => coeff R d (f i)) u (nhds (coeff R d g))

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
u : Filter ι
g : MvPowerSeries σ R
⊢ (∀ (i : σ →₀ ℕ), Tendsto (fun x => f x i) u (nhds (g i))) ↔
    ∀ (d : σ →₀ ℕ), Tendsto (fun i => (coeff R d) (f i)) u (nhds ((coeff R d) g))

Tactic:
exact forall_congr' (fun d => Iff.rfl)

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
u : Filter ι
g : MvPowerSeries σ R
⊢ Tendsto f u (nhds g) ↔ ∀ (d : σ →₀ ℕ), Tendsto (fun i => (coeff R d) (f i)) u (nhds ((coeff R d) g))

Tactic:
rw [nhds_pi, tendsto_pi]

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
u : Filter ι
g : MvPowerSeries σ R
⊢ (∀ (i : σ →₀ ℕ), Tendsto (fun x => f x i) u (nhds (g i))) ↔
    ∀ (d : σ →₀ ℕ), Tendsto (fun i => (coeff R d) (f i)) u (nhds ((coeff R d) g))
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_lt_one_eq_interior (hc : Convex ℝ s) (hs₀ : s ∈ 𝓝 0) :
    { x | gauge s x < 1 } = interior s

Proof state:
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
x : E
hx : x ∈ {x | gauge s x < 1}
⊢ x ∈ interior s

Tactic:
rcases mem_openSegment_of_gauge_lt_one (absorbent_nhds_zero hs₀) hx with ⟨y, hys, hxy⟩

Result:
case intro.intro
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
x : E
hx : x ∈ {x | gauge s x < 1}
y : E
hys : y ∈ s
hxy : x ∈ openSegment ℝ 0 y
⊢ x ∈ interior s

Proof state:
case intro.intro
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
x : E
hx : x ∈ {x | gauge s x < 1}
y : E
hys : y ∈ s
hxy : x ∈ openSegment ℝ 0 y
⊢ x ∈ interior s

Tactic:
exact hc.openSegment_interior_self_subset_interior (mem_interior_iff_mem_nhds.2 hs₀) hys hxy

Result:
no goals

Proof state:
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
⊢ {x | gauge s x < 1} = interior s

Tactic:
refine Subset.antisymm (fun x hx ↦ ?_) (interior_subset_gauge_lt_one s)

Result:
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
x : E
hx : x ∈ {x | gauge s x < 1}
⊢ x ∈ interior s
-- Mathlib/CategoryTheory/Sites/IsSheafOneHypercover.lean
lemma isSheaf_iff_of_isGeneratedByOneHypercovers
    [GrothendieckTopology.IsGeneratedByOneHypercovers.{w} J] (P : Cᵒᵖ ⥤ A) :
    IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : GrothendieckTopology.OneHypercover.{w} J X),
        Nonempty (IsLimit (E.multifork P))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : J.IsGeneratedByOneHypercovers
P : Cᵒᵖ ⥤ A
⊢ IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : J.OneHypercover X), Nonempty (IsLimit (E.multifork P))

Tactic:
simpa using GrothendieckTopology.OneHypercoverFamily.isSheaf_iff.{w} ⊤ P

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/Classification.lean
theorem isAlgClosure_of_transcendence_basis [IsAlgClosed K] (hv : IsTranscendenceBasis R v) :
    IsAlgClosure (Algebra.adjoin R (Set.range v)) K :=
  letI := RingHom.domain_nontrivial (algebraMap R K)
  { isAlgClosed

Proof state:
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
ι : Type u_4
v : ι → K
inst✝ : IsAlgClosed K
hv : IsTranscendenceBasis R v
this : Nontrivial R := RingHom.domain_nontrivial (algebraMap R K)
⊢ IsAlgClosed K

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem nnnorm_equiv_symm_const {β} [SeminormedAddCommGroup β] (hp : p ≠ ∞) (b : β) :
    ‖(WithLp.equiv p (ι → β)).symm (Function.const _ b)‖₊ =
      (Fintype.card ι : ℝ≥0) ^ (1 / p).toReal * ‖b‖₊

Proof state:
case inl
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
β : Type u_5
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : p = ⊤
⊢ ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

Tactic:
exact False.elim (hp h)

Result:
no goals

Proof state:
case inr
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
β : Type u_5
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : 1 ≤ p.toReal
⊢ ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

Tactic:
have ne_zero : p.toReal ≠ 0 := (zero_lt_one.trans_le h).ne'

Result:
case inr
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
β : Type u_5
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : 1 ≤ p.toReal
ne_zero : p.toReal ≠ 0
⊢ ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

Proof state:
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
β : Type u_5
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
⊢ ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

Tactic:
rcases p.dichotomy with (h | h)

Result:
case inl
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
β : Type u_5
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : p = ⊤
⊢ ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

case inr
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
β : Type u_5
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : 1 ≤ p.toReal
⊢ ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

Proof state:
case inr
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
β : Type u_5
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : 1 ≤ p.toReal
ne_zero : p.toReal ≠ 0
⊢ ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

Tactic:
simp_rw [nnnorm_eq_sum hp, WithLp.equiv_symm_pi_apply, Function.const_apply, Finset.sum_const,
  Finset.card_univ, nsmul_eq_mul, NNReal.mul_rpow, ← NNReal.rpow_mul,
  mul_one_div_cancel ne_zero, NNReal.rpow_one, ENNReal.toReal_div, ENNReal.one_toReal]

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp) existing card_mul_cast_subConst]
lemma card_mul_cast_divConst (A B : Finset G) : (#A * δₘ[A, B] : 𝕜) = #(A / B)

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑(#A) * ↑δₘ[A, B] = ↑(#(A / B))

Tactic:
norm_cast

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑(#A) * δₘ[A, B] = ↑(#(A / B))

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑(#A) * δₘ[A, B] = ↑(#(A / B))

Tactic:
exact card_mul_divConst _ _

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
@[reassoc (attr := simp)]
lemma glueDataT_snd (U V : X.affineOpens) :
    I.glueDataT U V ≫ pullback.snd _ _ = pullback.snd _ _ ≫ X.homOfLE (by simp) :=
  pullback.lift_snd _ _ _

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ ↑U ⊓ ↑V ≤ ↑V ⊓ ↑U

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_X : X.eval₂ f x = x

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x X = x

Tactic:
simp [eval₂_eq_sum]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem zero_le_padicValRat_of_nat (n : ℕ) : 0 ≤ padicValRat p n

Proof state:
p n : ℕ
⊢ 0 ≤ padicValRat p ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Ergodic.lean
theorem preErgodic_conjugate_iff {e : α ≃ᵐ β} (h : MeasurePreserving e μ μ') :
    PreErgodic (e ∘ f ∘ e.symm) μ' ↔ PreErgodic f μ

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
hf : PreErgodic f μ
⊢ Semiconj (⇑e) f (⇑e ∘ f ∘ ⇑e.symm)

Tactic:
simp [Semiconj]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
⊢ PreErgodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ PreErgodic f μ

Tactic:
refine ⟨fun hf => preErgodic_of_preErgodic_conjugate (h.symm e) hf ?_,
    fun hf => preErgodic_of_preErgodic_conjugate h hf ?_⟩

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
hf : PreErgodic (⇑e ∘ f ∘ ⇑e.symm) μ'
⊢ Semiconj (⇑e.symm) (⇑e ∘ f ∘ ⇑e.symm) f

case refine_2
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
hf : PreErgodic f μ
⊢ Semiconj (⇑e) f (⇑e ∘ f ∘ ⇑e.symm)

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
hf : PreErgodic (⇑e ∘ f ∘ ⇑e.symm) μ'
⊢ Semiconj (⇑e.symm) (⇑e ∘ f ∘ ⇑e.symm) f

Tactic:
simp [Semiconj]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsCondKernelCDF.lintegral [IsFiniteKernel κ]
    {f : α × β → StieltjesFunction} (hf : IsCondKernelCDF f κ ν) (a : α) (x : ℝ) :
    ∫⁻ b, ENNReal.ofReal (f (a, b) x) ∂(ν a) = κ a (univ ×ˢ Iic x)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
inst✝ : IsFiniteKernel κ
f : α × β → StieltjesFunction
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
⊢ ∫⁻ (b : β), ENNReal.ofReal (↑(f (a, b)) x) ∂ν a = (κ a) (univ ×ˢ Iic x)

Tactic:
rw [← hf.setLIntegral _ MeasurableSet.univ, Measure.restrict_univ]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Real.lean
lemma dist_le_of_mem_Icc {x y x' y' : ℝ} (hx : x ∈ Icc x' y') (hy : y ∈ Icc x' y') :
    dist x y ≤ y' - x'

Proof state:
x y x' y' : ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
⊢ dist x y ≤ y' - x'

Tactic:
simpa only [Real.dist_eq, abs_of_nonpos (sub_nonpos.2 <| hx.1.trans hx.2), neg_sub] using
  Real.dist_le_of_mem_uIcc (Icc_subset_uIcc hx) (Icc_subset_uIcc hy)

Result:
no goals
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem pNilradical_eq_bot_of_frobenius_inj (R : Type*) [CommRing R] (p : ℕ) [ExpChar R p]
    (h : Function.Injective (frobenius R p)) : pNilradical R p = ⊥ := bot_unique fun x ↦ by
  rw [mem_pNilradical, Ideal.mem_bot]
  exact fun ⟨n, _⟩ ↦ h.iterate n (by rwa [← coe_iterateFrobenius, map_zero])

Proof state:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : ExpChar R p
h : Function.Injective ⇑(frobenius R p)
x : R
⊢ (∃ n, x ^ p ^ n = 0) → x = 0

Tactic:
exact fun ⟨n, _⟩ ↦ h.iterate n (by rwa [← coe_iterateFrobenius, map_zero])

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : ExpChar R p
h : Function.Injective ⇑(frobenius R p)
x : R
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h✝ : x ^ p ^ n = 0
⊢ (⇑(frobenius R p))^[n] x = (⇑(frobenius R p))^[n] 0

Tactic:
rwa [← coe_iterateFrobenius, map_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : ExpChar R p
h : Function.Injective ⇑(frobenius R p)
x : R
⊢ x ∈ pNilradical R p → x ∈ ⊥

Tactic:
rw [mem_pNilradical, Ideal.mem_bot]

Result:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : ExpChar R p
h : Function.Injective ⇑(frobenius R p)
x : R
⊢ (∃ n, x ^ p ^ n = 0) → x = 0
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem tangentCone_mono (h : s ⊆ t) : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x : E
s t : Set E
h : s ⊆ t
⊢ tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

Tactic:
rintro y ⟨c, d, ds, ctop, clim⟩

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x : E
s t : Set E
h : s ⊆ t
y : E
c : ℕ → 𝕜
d : ℕ → E
ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
ctop : Tendsto (fun n => ‖c n‖) atTop atTop
clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ y ∈ tangentConeAt 𝕜 t x

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x : E
s t : Set E
h : s ⊆ t
y : E
c : ℕ → 𝕜
d : ℕ → E
ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
ctop : Tendsto (fun n => ‖c n‖) atTop atTop
clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ y ∈ tangentConeAt 𝕜 t x

Tactic:
exact ⟨c, d, mem_of_superset ds fun n hn => h hn, ctop, clim⟩

Result:
no goals
-- Mathlib/Probability/Independence/Conditional.lean
lemma condIndepFun_iff_condIndep {β γ : Type*} [mβ : MeasurableSpace β]
    [mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ) (μ : Measure Ω) [IsFiniteMeasure μ] :
    CondIndepFun m' hm' f g μ
      ↔ CondIndep m' (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) hm' μ

Proof state:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndepFun m' hm' f g μ ↔ CondIndep m' (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) hm' μ

Tactic:
simp only [CondIndepFun, CondIndep, Kernel.IndepFun]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma truncatedSup_union_left (hs : a ∈ lowerClosure s) (ht : a ∉ lowerClosure t) :
    truncatedSup (s ∪ t) a = truncatedSup s a

Proof state:
α : Type u_1
inst✝³ : SemilatticeSup α
s t : Finset α
a : α
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
hs : a ∈ lowerClosure ↑s
ht : a ∉ lowerClosure ↑t
⊢ (s ∪ t).truncatedSup a = s.truncatedSup a

Tactic:
simp only [mem_lowerClosure, mem_coe, exists_prop, not_exists, not_and] at ht

Result:
α : Type u_1
inst✝³ : SemilatticeSup α
s t : Finset α
a : α
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
hs : a ∈ lowerClosure ↑s
ht : ∀ x ∈ t, ¬a ≤ x
⊢ (s ∪ t).truncatedSup a = s.truncatedSup a

Proof state:
α : Type u_1
inst✝³ : SemilatticeSup α
s t : Finset α
a : α
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
hs : a ∈ lowerClosure ↑s
ht : ∀ x ∈ t, ¬a ≤ x
⊢ (s ∪ t).truncatedSup a = s.truncatedSup a

Tactic:
simp only [truncatedSup_of_mem, hs, filter_union, filter_false_of_mem ht, union_empty,
  lower_aux.2 (Or.inl hs), ht]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem isClosedMap_iff_clusterPt :
    IsClosedMap f ↔ ∀ s y, MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosedMap f ↔ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)

Tactic:
simp [MapClusterPt, isClosedMap_iff_closure_image, subset_def, mem_closure_iff_clusterPt,
  and_comm]

Result:
no goals