harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_replicate_replicate : (replicate n (replicate m a)).flatten = replicate (n * m) a

Proof state:
n m : Nat
α✝ : Type u_1
a : α✝
⊢ (replicate n (replicate m a)).flatten = replicate (n * m) a

Tactic:
induction n with
| zero => simp
| succ n ih =>
  simp only [replicate_succ, flatten_cons, ih, replicate_append_replicate, replicate_inj, or_true,
    and_true, add_one_mul, Nat.add_comm]

Result:
no goals

Proof state:
case zero
m : Nat
α✝ : Type u_1
a : α✝
⊢ (replicate 0 (replicate m a)).flatten = replicate (0 * m) a

Tactic:
simp

Result:
no goals

Proof state:
case succ
m : Nat
α✝ : Type u_1
a : α✝
n : Nat
ih : (replicate n (replicate m a)).flatten = replicate (n * m) a
⊢ (replicate (n + 1) (replicate m a)).flatten = replicate ((n + 1) * m) a

Tactic:
simp only [replicate_succ, flatten_cons, ih, replicate_append_replicate, replicate_inj, or_true,
  and_true, add_one_mul, Nat.add_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma tendsto_rightDeriv_mul_log_atTop :
    Tendsto (fun x ↦ derivWithin (fun x ↦ x * log x) (Set.Ioi x) x) atTop atTop

Proof state:
⊢ Tendsto (fun x => derivWithin (fun x => x * log x) (Set.Ioi x) x) atTop atTop

Tactic:
refine (tendsto_congr' ?_).mpr (tendsto_log_atTop.atTop_add (tendsto_const_nhds (x := 1)))

Result:
⊢ (fun x => derivWithin (fun x => x * log x) (Set.Ioi x) x) =ᶠ[atTop] fun x => log x + 1

Proof state:
⊢ ∃ a, ∀ b ≥ a, derivWithin (fun x => x * log x) (Set.Ioi b) b = log b + 1

Tactic:
exact ⟨1, fun _ hx ↦ rightDeriv_mul_log (zero_lt_one.trans_le hx).ne'⟩

Result:
no goals

Proof state:
⊢ (fun x => derivWithin (fun x => x * log x) (Set.Ioi x) x) =ᶠ[atTop] fun x => log x + 1

Tactic:
rw [EventuallyEq, eventually_atTop]

Result:
⊢ ∃ a, ∀ b ≥ a, derivWithin (fun x => x * log x) (Set.Ioi b) b = log b + 1
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem coeff_sub' {x y : HahnSeries Γ R} : (x - y).coeff = x.coeff - y.coeff

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : HahnSeries Γ R
⊢ (x - y).coeff = x.coeff - y.coeff

Tactic:
ext

Result:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : HahnSeries Γ R
x✝ : Γ
⊢ (x - y).coeff x✝ = (x.coeff - y.coeff) x✝

Proof state:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : HahnSeries Γ R
x✝ : Γ
⊢ (x - y).coeff x✝ = (x.coeff - y.coeff) x✝

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_congr_Prop {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q)
    (f : ∀ x, f₁ (pq.mpr x) = f₂ x) : iSup f₁ = iSup f₂

Proof state:
case e_s.h
α : Type u_1
inst✝ : SupSet α
p : Prop
f₁ f₂ : p → α
pq : p ↔ p
f : ∀ (x : p), f₁ ⋯ = f₂ x
x : p
⊢ f₁ x = f₂ x

Tactic:
apply f

Result:
no goals

Proof state:
α : Type u_1
inst✝ : SupSet α
p : Prop
f₁ f₂ : p → α
pq : p ↔ p
f : ∀ (x : p), f₁ ⋯ = f₂ x
⊢ iSup f₁ = iSup f₂

Tactic:
congr with x

Result:
case e_s.h
α : Type u_1
inst✝ : SupSet α
p : Prop
f₁ f₂ : p → α
pq : p ↔ p
f : ∀ (x : p), f₁ ⋯ = f₂ x
x : p
⊢ f₁ x = f₂ x

Proof state:
α : Type u_1
inst✝ : SupSet α
p q : Prop
f₁ : p → α
f₂ : q → α
pq : p ↔ q
f : ∀ (x : q), f₁ ⋯ = f₂ x
⊢ iSup f₁ = iSup f₂

Tactic:
obtain rfl := propext pq

Result:
α : Type u_1
inst✝ : SupSet α
p : Prop
f₁ f₂ : p → α
pq : p ↔ p
f : ∀ (x : p), f₁ ⋯ = f₂ x
⊢ iSup f₁ = iSup f₂
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
lemma _root_.MvPolynomial.isHomogeneous_X_pow (i : σ) (n : ℕ) :
    (X (R := R) i ^ n).IsHomogeneous n

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
n : ℕ
⊢ (X i ^ n).IsHomogeneous n

Tactic:
simpa only [one_mul] using (isHomogeneous_X _ _).pow n

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem constantCoeff_X (i : σ) : constantCoeff (X i : MvPolynomial σ R) = 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
⊢ constantCoeff (X i) = 0

Tactic:
simp [constantCoeff_eq]

Result:
no goals
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem mem_nhdsLT_iff_exists_Ico_subset [NoMinOrder α] [DenselyOrdered α] {a : α} {s : Set α} :
    s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
this : ⇑ofDual ⁻¹' s ∈ 𝓝[>] toDual a ↔ ∃ u ∈ Ioi (toDual a), Ioc (toDual a) u ⊆ ⇑ofDual ⁻¹' s
⊢ s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s

Tactic:
simpa only [OrderDual.exists, exists_prop, dual_Ioc] using this

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s

Tactic:
have : ofDual ⁻¹' s ∈ 𝓝[>] toDual a ↔ _ := mem_nhdsGT_iff_exists_Ioc_subset

Result:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
this : ⇑ofDual ⁻¹' s ∈ 𝓝[>] toDual a ↔ ∃ u ∈ Ioi (toDual a), Ioc (toDual a) u ⊆ ⇑ofDual ⁻¹' s
⊢ s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s
-- Mathlib/Order/Cover.lean
theorem covBy_iff_lt_iff_le_right {x y : α} : x ⋖ y ↔ ∀ {z}, x < z ↔ y ≤ z

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ (∀ {z : α}, ¬z ≤ x ↔ ¬z < y) ↔ ∀ {z : α}, x < z ↔ y ≤ z

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ x ⋖ y ↔ ∀ {z : α}, x < z ↔ y ≤ z

Tactic:
trans ∀ {z}, ¬ z ≤ x ↔ ¬ z < y

Result:
α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ x ⋖ y ↔ ∀ {z : α}, ¬z ≤ x ↔ ¬z < y

α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ (∀ {z : α}, ¬z ≤ x ↔ ¬z < y) ↔ ∀ {z : α}, x < z ↔ y ≤ z

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ x ⋖ y ↔ ∀ {z : α}, ¬z ≤ x ↔ ¬z < y

Tactic:
simp_rw [covBy_iff_le_iff_lt_left, not_iff_not]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem add_sub_cancel_of_le {a b : Ordinal} (h : b ≤ a) : b + (a - b) = a :=
  (le_add_sub a b).antisymm'
    (by
      rcases zero_or_succ_or_limit (a - b) with (e | ⟨c, e⟩ | l)
      · simp only [e, add_zero, h]
      · rw [e, add_succ, succ_le_iff, ← lt_sub, e]
        exact lt_succ c
      · exact (add_le_of_limit l).2 fun c l => (lt_sub.1 l).le)

Proof state:
case inr.inl.intro
a b : Ordinal.{u_4}
h : b ≤ a
c : Ordinal.{u_4}
e : a - b = succ c
⊢ b + (a - b) ≤ a

Tactic:
rw [e, add_succ, succ_le_iff, ← lt_sub, e]

Result:
case inr.inl.intro
a b : Ordinal.{u_4}
h : b ≤ a
c : Ordinal.{u_4}
e : a - b = succ c
⊢ c < succ c

Proof state:
case inr.inr
a b : Ordinal.{u_4}
h : b ≤ a
l : (a - b).IsLimit
⊢ b + (a - b) ≤ a

Tactic:
exact (add_le_of_limit l).2 fun c l => (lt_sub.1 l).le

Result:
no goals

Proof state:
case inr.inl.intro
a b : Ordinal.{u_4}
h : b ≤ a
c : Ordinal.{u_4}
e : a - b = succ c
⊢ c < succ c

Tactic:
exact lt_succ c

Result:
no goals

Proof state:
a b : Ordinal.{u_4}
h : b ≤ a
⊢ b + (a - b) ≤ a

Tactic:
rcases zero_or_succ_or_limit (a - b) with (e | ⟨c, e⟩ | l)

Result:
case inl
a b : Ordinal.{u_4}
h : b ≤ a
e : a - b = 0
⊢ b + (a - b) ≤ a

case inr.inl.intro
a b : Ordinal.{u_4}
h : b ≤ a
c : Ordinal.{u_4}
e : a - b = succ c
⊢ b + (a - b) ≤ a

case inr.inr
a b : Ordinal.{u_4}
h : b ≤ a
l : (a - b).IsLimit
⊢ b + (a - b) ≤ a

Proof state:
case inl
a b : Ordinal.{u_4}
h : b ≤ a
e : a - b = 0
⊢ b + (a - b) ≤ a

Tactic:
simp only [e, add_zero, h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
theorem isLimit_iff (c : Cone F) :
    Nonempty (IsLimit c) ↔ ∀ s ∈ F.sections, ∃! x : c.pt, ∀ j, c.π.app j x = s j

Proof state:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
x✝ : Nonempty (IsLimit c)
s : (j : J) → F.obj j
hs : s ∈ F.sections
t : IsLimit c
⊢ ∃! x, ∀ (j : J), c.π.app j x = s j

Tactic:
let cs := coneOfSection hs

Result:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
x✝ : Nonempty (IsLimit c)
s : (j : J) → F.obj j
hs : s ∈ F.sections
t : IsLimit c
cs : Cone F := coneOfSection ⋯
⊢ ∃! x, ∀ (j : J), c.π.app j x = s j

Proof state:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), c.π.app j x = s j
x : (c_1 : Cone F) → c_1.pt → c.pt
hx :
  ∀ (c_1 : Cone F) (y : c_1.pt),
    (fun x => ∀ (j : J), c.π.app j x = ↑(sectionOfCone c_1 y) j) (x c_1 y) ∧
      ∀ (y_1 : c.pt), (fun x => ∀ (j : J), c.π.app j x = ↑(sectionOfCone c_1 y) j) y_1 → y_1 = x c_1 y
⊢ IsLimit c

Tactic:
exact ⟨x, fun c j ↦ funext fun y ↦ (hx c y).1 j,
  fun c f hf ↦ funext fun y ↦ (hx c y).2 (f y) (fun j ↦ congr_fun (hf j) y)⟩

Result:
no goals

Proof state:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
x✝ : Nonempty (IsLimit c)
s : (j : J) → F.obj j
hs : s ∈ F.sections
t : IsLimit c
cs : Cone F := coneOfSection ⋯
⊢ ∃! x, ∀ (j : J), c.π.app j x = s j

Tactic:
exact ⟨t.lift cs ⟨⟩, fun j ↦ congr_fun (t.fac cs j) ⟨⟩,
  fun x hx ↦ congr_fun (t.uniq cs (fun _ ↦ x) fun j ↦ funext fun _ ↦ hx j) ⟨⟩⟩

Result:
no goals

Proof state:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), c.π.app j x = s j
⊢ IsLimit c

Tactic:
choose x hx using fun c y ↦ h _ (sectionOfCone c y).2

Result:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), c.π.app j x = s j
x : (c_1 : Cone F) → c_1.pt → c.pt
hx :
  ∀ (c_1 : Cone F) (y : c_1.pt),
    (fun x => ∀ (j : J), c.π.app j x = ↑(sectionOfCone c_1 y) j) (x c_1 y) ∧
      ∀ (y_1 : c.pt), (fun x => ∀ (j : J), c.π.app j x = ↑(sectionOfCone c_1 y) j) y_1 → y_1 = x c_1 y
⊢ IsLimit c

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
⊢ Nonempty (IsLimit c) ↔ ∀ s ∈ F.sections, ∃! x, ∀ (j : J), c.π.app j x = s j

Tactic:
refine ⟨fun ⟨t⟩ s hs ↦ ?_, fun h ↦ ⟨?_⟩⟩

Result:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
x✝ : Nonempty (IsLimit c)
s : (j : J) → F.obj j
hs : s ∈ F.sections
t : IsLimit c
⊢ ∃! x, ∀ (j : J), c.π.app j x = s j

case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), c.π.app j x = s j
⊢ IsLimit c
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem rescale_X (a : A) : rescale a X = C A a * X

Proof state:
case h
A : Type u_2
inst✝ : CommRing A
a : A
n✝ : ℕ
⊢ (coeff A n✝) ((rescale a) X) = (coeff A n✝) ((C A) a * X)

Tactic:
simp only [coeff_rescale, coeff_C_mul, coeff_X]

Result:
case h
A : Type u_2
inst✝ : CommRing A
a : A
n✝ : ℕ
⊢ (a ^ n✝ * if n✝ = 1 then 1 else 0) = a * if n✝ = 1 then 1 else 0

Proof state:
A : Type u_2
inst✝ : CommRing A
a : A
⊢ (rescale a) X = (C A) a * X

Tactic:
ext

Result:
case h
A : Type u_2
inst✝ : CommRing A
a : A
n✝ : ℕ
⊢ (coeff A n✝) ((rescale a) X) = (coeff A n✝) ((C A) a * X)

Proof state:
case h
A : Type u_2
inst✝ : CommRing A
a : A
n✝ : ℕ
⊢ (a ^ n✝ * if n✝ = 1 then 1 else 0) = a * if n✝ = 1 then 1 else 0

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem empty : μ ⊥ = 0

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ μ ⊥ = 0

Tactic:
simpa [toNNReal_eq_zero_iff] using μ.sup_disjoint' ⊥ ⊥

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem iInf {κ : Sort*} {f : κ → Ideal A} (h : ∀ i, (f i).IsHomogeneous 𝒜) :
    (⨅ i, f i).IsHomogeneous 𝒜

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_4
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
i : ι
x : A
hx : x ∈ ⨅ i, f i
⊢ ↑(((decompose 𝒜) x) i) ∈ ⨅ i, f i

Tactic:
simp only [Ideal.mem_iInf] at hx ⊢

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_4
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
i : ι
x : A
hx : ∀ (i : κ), x ∈ f i
⊢ ∀ (i_1 : κ), ↑(((decompose 𝒜) x) i) ∈ f i_1

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_4
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
⊢ IsHomogeneous 𝒜 (⨅ i, f i)

Tactic:
intro i x hx

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_4
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
i : ι
x : A
hx : x ∈ ⨅ i, f i
⊢ ↑(((decompose 𝒜) x) i) ∈ ⨅ i, f i

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_4
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
i : ι
x : A
hx : ∀ (i : κ), x ∈ f i
⊢ ∀ (i_1 : κ), ↑(((decompose 𝒜) x) i) ∈ f i_1

Tactic:
exact fun j => h _ _ (hx j)

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem adjoin_union_coe_submodule :
    Subalgebra.toSubmodule (adjoin R (s ∪ t)) =
      Subalgebra.toSubmodule (adjoin R s) * Subalgebra.toSubmodule (adjoin R t)

Proof state:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ span R ↑(Submonoid.closure (s ∪ t)) = span R (↑(Submonoid.closure s) * ↑(Submonoid.closure t))

Tactic:
congr 1 with z

Result:
case e_s.h
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
z : A
⊢ z ∈ ↑(Submonoid.closure (s ∪ t)) ↔ z ∈ ↑(Submonoid.closure s) * ↑(Submonoid.closure t)

Proof state:
case e_s.h
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
z : A
⊢ z ∈ ↑(Submonoid.closure (s ∪ t)) ↔ z ∈ ↑(Submonoid.closure s) * ↑(Submonoid.closure t)

Tactic:
simp [Submonoid.closure_union, Submonoid.mem_sup, Set.mem_mul]

Result:
no goals

Proof state:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ Subalgebra.toSubmodule (adjoin R (s ∪ t)) = Subalgebra.toSubmodule (adjoin R s) * Subalgebra.toSubmodule (adjoin R t)

Tactic:
rw [adjoin_eq_span, adjoin_eq_span, adjoin_eq_span, span_mul_span]

Result:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ span R ↑(Submonoid.closure (s ∪ t)) = span R (↑(Submonoid.closure s) * ↑(Submonoid.closure t))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) (a : {x // p x}) :
    (l.attachWith p H).count a = l.count ↑a :=
  Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attachWith _ _ _

Proof state:
α : Type u_1
inst✝ : DecidableEq α
p : α → Prop
l : List α
H : ∀ (a : α), a ∈ l → p a
a x✝¹ : { x // p x }
x✝ : x✝¹ ∈ l.attachWith p H
⊢ (x✝¹ == a) = true ↔ (x✝¹.val == a.val) = true

Tactic:
simp [Subtype.ext_iff]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem abs_re_div_norm_le_one (z : ℂ) : |z.re / ‖z‖| ≤ 1 :=
 if hz : z = 0 then by simp [hz, zero_le_one]
 else by simp_rw [abs_div, abs_norm,
   div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_re_le_norm]

Proof state:
z : ℂ
hz : ¬z = 0
⊢ |z.re / ‖z‖| ≤ 1

Tactic:
simp_rw [abs_div, abs_norm,
div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_re_le_norm]

Result:
no goals

Proof state:
z : ℂ
hz : z = 0
⊢ |z.re / ‖z‖| ≤ 1

Tactic:
simp [hz, zero_le_one]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem smul_boundedBy {c : ℝ≥0∞} (hc : c ≠ ∞) : c • boundedBy m = boundedBy (c • m)

Proof state:
case e_m.h
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
⊢ (c • fun s => ⨆ (_ : s.Nonempty), m s) s = ⨆ (_ : s.Nonempty), (c • m) s

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs) <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ OuterMeasure.ofFunction (c • fun s => ⨆ (_ : s.Nonempty), m s) ⋯ =
    OuterMeasure.ofFunction (fun s => ⨆ (_ : s.Nonempty), (c • m) s) ⋯

Tactic:
congr 1 with s : 1

Result:
case e_m.h
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
⊢ (c • fun s => ⨆ (_ : s.Nonempty), m s) s = ⨆ (_ : s.Nonempty), (c • m) s

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ c • boundedBy m = boundedBy (c • m)

Tactic:
simp only [boundedBy , smul_ofFunction hc]

Result:
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ OuterMeasure.ofFunction (c • fun s => ⨆ (_ : s.Nonempty), m s) ⋯ =
    OuterMeasure.ofFunction (fun s => ⨆ (_ : s.Nonempty), (c • m) s) ⋯
-- Mathlib/MeasureTheory/Measure/DiracProba.lean
/-- The assignment `x ↦ diracProba x` is injective if all singletons are measurable. -/
lemma injective_diracProba {X : Type*} [MeasurableSpace X] [MeasurableSpace.SeparatesPoints X] :
    Function.Injective (fun (x : X) ↦ diracProba x)

Proof state:
X : Type u_2
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace.SeparatesPoints X
x y : X
x_eq_y : (fun x => diracProba x) x = (fun x => diracProba x) y
⊢ x = y

Tactic:
rw [← dirac_eq_dirac_iff]

Result:
X : Type u_2
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace.SeparatesPoints X
x y : X
x_eq_y : (fun x => diracProba x) x = (fun x => diracProba x) y
⊢ Measure.dirac x = Measure.dirac y

Proof state:
X : Type u_2
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace.SeparatesPoints X
⊢ Function.Injective fun x => diracProba x

Tactic:
intro x y x_eq_y

Result:
X : Type u_2
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace.SeparatesPoints X
x y : X
x_eq_y : (fun x => diracProba x) x = (fun x => diracProba x) y
⊢ x = y

Proof state:
X : Type u_2
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace.SeparatesPoints X
x y : X
x_eq_y : (fun x => diracProba x) x = (fun x => diracProba x) y
⊢ Measure.dirac x = Measure.dirac y

Tactic:
rwa [Subtype.ext_iff] at x_eq_y

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
@[simp high] lemma natCast_self (n : ℕ) [NeZero n] : (n : Fin n) = 0

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ ↑n = 0

Tactic:
ext

Result:
case h
n : ℕ
inst✝ : NeZero n
⊢ ↑↑n = ↑0

Proof state:
case h
n : ℕ
inst✝ : NeZero n
⊢ ↑↑n = ↑0

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem lf_or_equiv_or_gf (x y : PGame) : x ⧏ y ∨ (x ≈ y) ∨ y ⧏ x

Proof state:
case neg.h.inl
x y : PGame
h : ¬x ⧏ y
h' : y < x
⊢ x ≈ y ∨ y ⧏ x

Tactic:
exact Or.inr h'.lf

Result:
no goals

Proof state:
case pos
x y : PGame
h : x ⧏ y
⊢ x ⧏ y ∨ x ≈ y ∨ y ⧏ x

Tactic:
exact Or.inl h

Result:
no goals

Proof state:
case neg
x y : PGame
h : ¬x ⧏ y
⊢ x ⧏ y ∨ x ≈ y ∨ y ⧏ x

Tactic:
right

Result:
case neg.h
x y : PGame
h : ¬x ⧏ y
⊢ x ≈ y ∨ y ⧏ x

Proof state:
case neg.h.inr
x y : PGame
h : ¬x ⧏ y
h' : y ≈ x
⊢ x ≈ y ∨ y ⧏ x

Tactic:
exact Or.inl (Equiv.symm h')

Result:
no goals

Proof state:
x y : PGame
⊢ x ⧏ y ∨ x ≈ y ∨ y ⧏ x

Tactic:
by_cases h : x ⧏ y

Result:
case pos
x y : PGame
h : x ⧏ y
⊢ x ⧏ y ∨ x ≈ y ∨ y ⧏ x

case neg
x y : PGame
h : ¬x ⧏ y
⊢ x ⧏ y ∨ x ≈ y ∨ y ⧏ x

Proof state:
case neg.h
x y : PGame
h : ¬x ⧏ y
⊢ x ≈ y ∨ y ⧏ x

Tactic:
rcases lt_or_equiv_of_le (PGame.not_lf.1 h) with h' | h'

Result:
case neg.h.inl
x y : PGame
h : ¬x ⧏ y
h' : y < x
⊢ x ≈ y ∨ y ⧏ x

case neg.h.inr
x y : PGame
h : ¬x ⧏ y
h' : y ≈ x
⊢ x ≈ y ∨ y ⧏ x
-- Mathlib/Order/SupClosed.lean
lemma SupClosed.preimage [FunLike F β α] [SupHomClass F β α] (hs : SupClosed s) (f : F) :
    SupClosed (f ⁻¹' s) :=
  fun a ha b hb ↦ by simpa [map_sup] using hs ha hb

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F β α
inst✝ : SupHomClass F β α
hs : SupClosed s
f : F
a : β
ha : a ∈ ⇑f ⁻¹' s
b : β
hb : b ∈ ⇑f ⁻¹' s
⊢ a ⊔ b ∈ ⇑f ⁻¹' s

Tactic:
simpa [map_sup] using hs ha hb

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem prod_comap_comap_eq.{u, v, w, x} {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x}
    {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : β₁ → α₁} {m₂ : β₂ → α₂} :
    comap m₁ f₁ ×ˢ comap m₂ f₂ = comap (fun p : β₁ × β₂ => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)

Proof state:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : β₁ → α₁
m₂ : β₂ → α₂
⊢ comap m₁ f₁ ×ˢ comap m₂ f₂ = comap (fun p => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)

Tactic:
simp only [prod_eq_inf, comap_comap, comap_inf, Function.comp_def]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Convex.lean
theorem Wbtw.dist_add_dist {x y z : P} (h : Wbtw ℝ x y z) :
    dist x y + dist y z = dist x z

Proof state:
case intro.intro.intro
E : Type u_1
P : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
x z : P
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ dist x ((AffineMap.lineMap x z) a) + dist ((AffineMap.lineMap x z) a) z = dist x z

Tactic:
simp [abs_of_nonneg, ha₀, ha₁, sub_mul]

Result:
no goals

Proof state:
E : Type u_1
P : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
x y z : P
h : Wbtw ℝ x y z
⊢ dist x y + dist y z = dist x z

Tactic:
obtain ⟨a, ⟨ha₀, ha₁⟩, rfl⟩ := h

Result:
case intro.intro.intro
E : Type u_1
P : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
x z : P
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ dist x ((AffineMap.lineMap x z) a) + dist ((AffineMap.lineMap x z) a) z = dist x z
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem eval_at_1 (n ν : ℕ) : (bernsteinPolynomial R n ν).eval 1 = if ν = n then 1 else 0

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
ν : ℕ
⊢ Polynomial.eval 1 (↑(ν.choose ν) * X ^ ν * (1 - X) ^ (ν - ν)) = 1

Tactic:
simp

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν = n
⊢ Polynomial.eval 1 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 1

Tactic:
subst h

Result:
case pos
R : Type u_1
inst✝ : CommRing R
ν : ℕ
⊢ Polynomial.eval 1 (↑(ν.choose ν) * X ^ ν * (1 - X) ^ (ν - ν)) = 1

Proof state:
case neg.inl
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
hνn : ν < n
⊢ Polynomial.eval 1 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0

Tactic:
simp [zero_pow <| Nat.sub_ne_zero_of_lt hνn]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
⊢ Polynomial.eval 1 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0

Tactic:
obtain hνn | hnν := Ne.lt_or_lt h

Result:
case neg.inl
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
hνn : ν < n
⊢ Polynomial.eval 1 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0

case neg.inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
hnν : n < ν
⊢ Polynomial.eval 1 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 1 (bernsteinPolynomial R n ν) = if ν = n then 1 else 0

Tactic:
rw [bernsteinPolynomial]

Result:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 1 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = if ν = n then 1 else 0

Proof state:
case neg.inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
hnν : n < ν
⊢ Polynomial.eval 1 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0

Tactic:
simp [Nat.choose_eq_zero_of_lt hnν]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 1 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = if ν = n then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν = n
⊢ Polynomial.eval 1 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 1

case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
⊢ Polynomial.eval 1 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0