harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma log_coverMincard_iterate_le {T : X → X} {F : Set X} (F_inv : MapsTo T F F) {U : Set (X × X)}
    (U_symm : SymmetricRel U) (m : ℕ) {n : ℕ} (n_pos : 0 < n) :
    log (coverMincard T F (U ○ U) (m * n)) / n ≤ log (coverMincard T F U m)

Proof state:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
n_pos : 0 < n
⊢ (↑(coverMincard T F (U ○ U) (m * n))).log / ↑n ≤ (↑(coverMincard T F U m)).log

Tactic:
apply (EReal.div_le_iff_le_mul (b := n) (Nat.cast_pos'.2 n_pos) (natCast_ne_top n)).2

Result:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
n_pos : 0 < n
⊢ (↑(coverMincard T F (U ○ U) (m * n))).log ≤ ↑n * (↑(coverMincard T F U m)).log

Proof state:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
n_pos : 0 < n
⊢ (↑(coverMincard T F (U ○ U) (m * n))).log ≤ ↑n * (↑(coverMincard T F U m)).log

Tactic:
rw [← log_pow, StrictMono.le_iff_le log_strictMono]

Result:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
n_pos : 0 < n
⊢ ↑(coverMincard T F (U ○ U) (m * n)) ≤ ↑(coverMincard T F U m) ^ n

Proof state:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
n_pos : 0 < n
⊢ ↑(coverMincard T F (U ○ U) (m * n)) ≤ ENat.toENNRealRingHom (coverMincard T F U m) ^ n

Tactic:
rw [← RingHom.map_pow ENat.toENNRealRingHom _ n, ENat.toENNRealRingHom_apply, ENat.toENNReal_le]

Result:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
n_pos : 0 < n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Proof state:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
n_pos : 0 < n
⊢ ↑(coverMincard T F (U ○ U) (m * n)) ≤ ↑(coverMincard T F U m) ^ n

Tactic:
nth_rw 2 [← ENat.toENNRealRingHom_apply]

Result:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
n_pos : 0 < n
⊢ ↑(coverMincard T F (U ○ U) (m * n)) ≤ ENat.toENNRealRingHom (coverMincard T F U m) ^ n

Proof state:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
n_pos : 0 < n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
exact coverMincard_mul_le_pow F_inv U_symm m n

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem IsOpen.inter_closure (h : IsOpen s) : s ∩ closure t ⊆ closure (s ∩ t) :=
  compl_subset_compl.mp <| by
    simpa only [← interior_compl, compl_inter] using IsClosed.interior_union_left h.isClosed_compl

Proof state:
X : Type u
s t : Set X
inst✝ : TopologicalSpace X
h : IsOpen s
⊢ (closure (s ∩ t))ᶜ ⊆ (s ∩ closure t)ᶜ

Tactic:
simpa only [← interior_compl, compl_inter] using IsClosed.interior_union_left h.isClosed_compl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
lemma Rel'.symm {x y : X₁ ⊕ X₂} (h : Rel' f g x y) :
    Rel' f g y x

Proof state:
case refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x : X₁ ⊕ X₂
⊢ Rel' f g x x

Tactic:
apply Rel'.refl

Result:
no goals

Proof state:
case inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Rel' f g (Sum.inr (g s✝)) (Sum.inl (f s✝))

Tactic:
exact Rel'.inr_inl _

Result:
no goals

Proof state:
case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀✝ y₀✝ : S
h : g x₀✝ = g y₀✝
⊢ Rel' f g (Sum.inl (f y₀✝)) (Sum.inl (f x₀✝))

Tactic:
exact Rel'.inl_inl _ _ h.symm

Result:
no goals

Proof state:
case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Rel' f g (Sum.inl (f s✝)) (Sum.inr (g s✝))

Tactic:
exact Rel'.inl_inr _

Result:
no goals

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x y : X₁ ⊕ X₂
h : Rel' f g x y
⊢ Rel' f g y x

Tactic:
obtain _|⟨_, _, h⟩|_|_ := h

Result:
case refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x : X₁ ⊕ X₂
⊢ Rel' f g x x

case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀✝ y₀✝ : S
h : g x₀✝ = g y₀✝
⊢ Rel' f g (Sum.inl (f y₀✝)) (Sum.inl (f x₀✝))

case inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Rel' f g (Sum.inr (g s✝)) (Sum.inl (f s✝))

case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Rel' f g (Sum.inl (f s✝)) (Sum.inr (g s✝))
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
/-- **Cauchy-Schwarz inequality** in terms of `Finset.expect`. -/
lemma expect_mul_sq_le_sq_mul_sq (s : Finset ι) (f g : ι → R) :
    (𝔼 i ∈ s, f i * g i) ^ 2 ≤ (𝔼 i ∈ s, f i ^ 2) * 𝔼 i ∈ s, g i ^ 2

Proof state:
ι : Type u_1
R : Type u_3
inst✝³ : LinearOrderedCommSemiring R
inst✝² : ExistsAddOfLE R
inst✝¹ : Module ℚ≥0 R
inst✝ : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
⊢ (↑(#s) ^ 2)⁻¹ • (∑ x ∈ s, f x * g x) ^ 2 ≤ (↑(#s) ^ 2)⁻¹ • ((∑ x ∈ s, f x ^ 2) * ∑ x ∈ s, g x ^ 2)

Tactic:
gcongr

Result:
case hb
ι : Type u_1
R : Type u_3
inst✝³ : LinearOrderedCommSemiring R
inst✝² : ExistsAddOfLE R
inst✝¹ : Module ℚ≥0 R
inst✝ : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
⊢ (∑ x ∈ s, f x * g x) ^ 2 ≤ (∑ x ∈ s, f x ^ 2) * ∑ x ∈ s, g x ^ 2

Proof state:
ι : Type u_1
R : Type u_3
inst✝³ : LinearOrderedCommSemiring R
inst✝² : ExistsAddOfLE R
inst✝¹ : Module ℚ≥0 R
inst✝ : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
⊢ (𝔼 i ∈ s, f i * g i) ^ 2 ≤ (𝔼 i ∈ s, f i ^ 2) * 𝔼 i ∈ s, g i ^ 2

Tactic:
simp only [expect, smul_pow, inv_pow, smul_mul_smul_comm, ← sq]

Result:
ι : Type u_1
R : Type u_3
inst✝³ : LinearOrderedCommSemiring R
inst✝² : ExistsAddOfLE R
inst✝¹ : Module ℚ≥0 R
inst✝ : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
⊢ (↑(#s) ^ 2)⁻¹ • (∑ x ∈ s, f x * g x) ^ 2 ≤ (↑(#s) ^ 2)⁻¹ • ((∑ x ∈ s, f x ^ 2) * ∑ x ∈ s, g x ^ 2)

Proof state:
case hb
ι : Type u_1
R : Type u_3
inst✝³ : LinearOrderedCommSemiring R
inst✝² : ExistsAddOfLE R
inst✝¹ : Module ℚ≥0 R
inst✝ : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
⊢ (∑ x ∈ s, f x * g x) ^ 2 ≤ (∑ x ∈ s, f x ^ 2) * ∑ x ∈ s, g x ^ 2

Tactic:
exact sum_mul_sq_le_sq_mul_sq ..

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
@[simp]
lemma two_mul_semilength_eq_length : 2 * p.semilength = p.toList.length

Proof state:
case h.e'_2.h.e'_6.h.e
p : DyckWord
⊢ (countP fun x => x == U) = countP fun a => decide ¬(a == D) = true

Tactic:
congr!

Result:
case h.e'_2.h.e'_6.h.e.h.e'_2.h
p : DyckWord
x✝ : DyckStep
⊢ (x✝ == U) = decide ¬(x✝ == D) = true

Proof state:
case h.e'_2.h.e'_6.h.e.h.e'_2.h
p : DyckWord
x✝ : DyckStep
⊢ (x✝ == U) = decide ¬(x✝ == D) = true

Tactic:
rename_i s

Result:
case h.e'_2.h.e'_6.h.e.h.e'_2.h
p : DyckWord
s : DyckStep
⊢ (s == U) = decide ¬(s == D) = true

Proof state:
case h.e'_2.h.e'_6.h.e
p : DyckWord
⊢ count U = countP fun a => decide ¬(a == D) = true

Tactic:
rw [count]

Result:
case h.e'_2.h.e'_6.h.e
p : DyckWord
⊢ (countP fun x => x == U) = countP fun a => decide ¬(a == D) = true

Proof state:
case h.e'_2.h.e'_6.h.e.h.e'_2.h
p : DyckWord
s : DyckStep
⊢ (s == U) = decide ¬(s == D) = true

Tactic:
cases s <;> tauto

Result:
no goals

Proof state:
p : DyckWord
⊢ 2 * p.semilength = (↑p).length

Tactic:
nth_rw 1 [two_mul, semilength, p.count_U_eq_count_D, semilength]

Result:
p : DyckWord
⊢ count D ↑p + count U ↑p = (↑p).length
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem nndist_equiv_symm_snd (y₁ y₂ : β) :
    nndist ((WithLp.equiv p (α × β)).symm (0, y₁)) ((WithLp.equiv p (α × β)).symm (0, y₂)) =
      nndist y₁ y₂

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
y₁ y₂ : β
⊢ nndist ((WithLp.equiv p (α × β)).symm (0, y₁)) ((WithLp.equiv p (α × β)).symm (0, y₂)) = nndist y₁ y₂

Tactic:
rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← WithLp.equiv_symm_sub, Prod.mk_sub_mk, sub_zero,
  nnnorm_equiv_symm_snd]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Basic.lean
theorem equivCongrLeft_apply (h : ι ≃ κ) (f : ⨁ i, β i) (k : κ) :
    equivCongrLeft h f k = f (h.symm k)

Proof state:
ι : Type v
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
κ : Type u_1
h : ι ≃ κ
f : ⨁ (i : ι), β i
k : κ
⊢ ((equivCongrLeft h) f) k = f (h.symm k)

Tactic:
exact DFinsupp.comapDomain'_apply _ h.right_inv _ _

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mfderivWithin_inter (ht : t ∈ 𝓝 x) :
    mfderivWithin I I' f (s ∩ t) x = mfderivWithin I I' f s x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
ht : t ∈ 𝓝 x
⊢ mfderivWithin I I' f (s ∩ t) x = mfderivWithin I I' f s x

Tactic:
rw [mfderivWithin, mfderivWithin, extChartAt_preimage_inter_eq, mdifferentiableWithinAt_inter ht,
  fderivWithin_inter (extChartAt_preimage_mem_nhds ht)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_insertMany_list_le [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)} :
    (insertMany m l).size ≤ m.size + l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
⊢ (insertMany m l).size ≤ m.size + l.length

Tactic:
simp_to_raw using Raw₀.Const.size_insertMany_list_le

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
@[to_additive] lemma antivaryOn_inv : AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedCommGroup α
inst✝ : OrderedCommGroup β
s : Set ι
f : ι → α
g : ι → β
⊢ AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem countP_pmap {p : α → Prop} (g : ∀ a, p a → β) (f : β → Bool) (l : List α) (H₁) :
    (l.pmap g H₁).countP f =
      l.attach.countP (fun ⟨a, m⟩ => f (g a (H₁ a m)))

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
g : (a : α) → p a → β
f : β → Bool
l : List α
H₁ : ∀ (a : α), a ∈ l → p a
⊢ countP f (pmap g l H₁) =
    countP
      (fun x =>
        match x with
        | ⟨a, m⟩ => f (g a ⋯))
      l.attach

Tactic:
simp [pmap_eq_map_attach, countP_map, Function.comp_def]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Nilpotent.lean
@[simp] lemma isNilpotent_mul_X_iff :
    IsNilpotent (P * X) ↔ IsNilpotent P

Proof state:
R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (P * X) ↔ IsNilpotent P

Tactic:
rw [← commute_X P]

Result:
R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P

Proof state:
R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P

Tactic:
exact isNilpotent_X_mul_iff

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
lemma ball_prod_same (x : α) (y : β) (r : ℝ) : ball x r ×ˢ ball y r = ball (x, y) r :=
  ext fun z => by simp [Prod.dist_eq]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α
y : β
r : ℝ
z : α × β
⊢ z ∈ ball x r ×ˢ ball y r ↔ z ∈ ball (x, y) r

Tactic:
simp [Prod.dist_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Function/UnifTight.lean
theorem unifTight_of_tendsto_Lp_zero (hp' : p ≠ ∞) (hf : ∀ n, MemLp (f n) p μ)
    (hf_tendsto : Tendsto (fun n ↦ eLpNorm (f n) p μ) atTop (𝓝 0)) : UnifTight f p μ := fun ε hε ↦by
  rw [ENNReal.tendsto_atTop_zero] at hf_tendsto
  obtain ⟨N, hNε⟩ := hf_tendsto ε (by simpa only [gt_iff_lt, ENNReal.coe_pos])
  let F : Fin N → α → β := fun n => f n
  have hF : ∀ n, MemLp (F n) p μ := fun n => hf n
  obtain ⟨s, hμs, hFε⟩ := unifTight_fin hp' hF hε
  refine ⟨s, hμs, fun n => ?_⟩
  by_cases hn : n < N
  · exact hFε ⟨n, hn⟩
  · exact (eLpNorm_indicator_le _).trans (hNε n (not_lt.mp hn))

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : Tendsto (fun n => eLpNorm (f n) p μ) atTop (𝓝 0)
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
rw [ENNReal.tendsto_atTop_zero] at hf_tendsto

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
⊢ ↑ε > 0

Tactic:
simpa only [gt_iff_lt, ENNReal.coe_pos]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ext_of_generateFrom_of_cover {S T : Set (Set α)} (h_gen : ‹_› = generateFrom S)
    (hc : T.Countable) (h_inter : IsPiSystem S) (hU : ⋃₀ T = univ) (htop : ∀ t ∈ T, μ t ≠ ∞)
    (ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)) (T_eq : ∀ t ∈ T, μ t = ν t) : μ = ν

Proof state:
case h.empty
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ⊤
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
u : Set α
⊢ μ (∅ ∩ t) = ν (∅ ∩ t)

Tactic:
simp only [Set.empty_inter, measure_empty]

Result:
no goals

Proof state:
case h.iUnion
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ⊤
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
u : Set α
f : ℕ → Set α
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), (μ.restrict t) (f i) = (ν.restrict t) (f i)
⊢ (μ.restrict t) (⋃ i, f i) = (ν.restrict t) (⋃ i, f i)

Tactic:
simp only [measure_iUnion hfd hfm, ihf]

Result:
no goals
-- Mathlib/Topology/LocallyFinite.lean
theorem isClosed_iUnion (hf : LocallyFinite f) (hc : ∀ i, IsClosed (f i)) :
    IsClosed (⋃ i, f i)

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
⊢ IsClosed (⋃ i, f i)

Tactic:
simp only [← closure_eq_iff_isClosed, hf.closure_iUnion, (hc _).closure_eq]

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem bodd_neg (n : ℤ) : bodd (-n) = bodd n

Proof state:
case negSucc
n : ℕ
⊢ (!n.bodd) = -[n+1].bodd

Tactic:
change (!Nat.bodd n) = !(bodd n)

Result:
case negSucc
n : ℕ
⊢ (!n.bodd) = !(↑n).bodd

Proof state:
n : ℤ
⊢ (-n).bodd = n.bodd

Tactic:
cases n with
| ofNat =>
  rw [← negOfNat_eq, bodd_negOfNat]
  simp
| negSucc n =>
  rw [neg_negSucc, bodd_coe, Nat.bodd_succ]
  change (!Nat.bodd n) = !(bodd n)
  rw [bodd_coe]

Result:
no goals

Proof state:
case negSucc
n : ℕ
⊢ (!n.bodd) = !(↑n).bodd

Tactic:
rw [bodd_coe]

Result:
no goals

Proof state:
case negSucc
n : ℕ
⊢ (- -[n+1]).bodd = -[n+1].bodd

Tactic:
rw [neg_negSucc, bodd_coe, Nat.bodd_succ]

Result:
case negSucc
n : ℕ
⊢ (!n.bodd) = -[n+1].bodd

Proof state:
case ofNat
a✝ : ℕ
⊢ (-ofNat a✝).bodd = (ofNat a✝).bodd

Tactic:
rw [← negOfNat_eq, bodd_negOfNat]

Result:
case ofNat
a✝ : ℕ
⊢ a✝.bodd = (ofNat a✝).bodd

Proof state:
case ofNat
a✝ : ℕ
⊢ a✝.bodd = (ofNat a✝).bodd

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem toAffineIsometryEquiv_linearIsometryEquiv :
    e.toAffineIsometryEquiv.linearIsometryEquiv = e

Proof state:
case h
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : NormedSpace 𝕜 V₂
e : V ≃ₗᵢ[𝕜] V₂
x✝ : V
⊢ e.toAffineIsometryEquiv.linearIsometryEquiv x✝ = e x✝

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : NormedSpace 𝕜 V₂
e : V ≃ₗᵢ[𝕜] V₂
⊢ e.toAffineIsometryEquiv.linearIsometryEquiv = e

Tactic:
ext

Result:
case h
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : NormedSpace 𝕜 V₂
e : V ≃ₗᵢ[𝕜] V₂
x✝ : V
⊢ e.toAffineIsometryEquiv.linearIsometryEquiv x✝ = e x✝
-- Mathlib/Topology/Sheaves/Stalks.lean
@[reassoc (attr := simp)]
lemma germ_stalkPullbackInv (f : X ⟶ Y) (F : Y.Presheaf C) (x : X) (V : Opens X) (hV : x ∈ V) :
    ((pullback C f).obj F).germ _ x hV ≫ stalkPullbackInv C f F x =
    F.germToPullbackStalk _ f V x hV

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
x : ↑X
V : Opens ↑X
hV : x ∈ V
⊢ ((pullback C f).obj F).germ V x hV ≫ stalkPullbackInv C f F x = germToPullbackStalk C f F V x hV

Tactic:
apply colimit.ι_desc

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem connectedComponentEquiv_trans (φ : G ≃g G') (φ' : G' ≃g G'') :
    connectedComponentEquiv (φ.trans φ') =
    φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv

Proof state:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
φ : G ≃g G'
φ' : G' ≃g G''
⊢ connectedComponentEquiv (RelIso.trans φ φ') = φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv

Tactic:
ext ⟨_⟩

Result:
case H.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
φ : G ≃g G'
φ' : G' ≃g G''
x✝ : G.ConnectedComponent
a✝ : V
⊢ (connectedComponentEquiv (RelIso.trans φ φ')) (Quot.mk G.Reachable a✝) =
    (φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv) (Quot.mk G.Reachable a✝)

Proof state:
case H.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
φ : G ≃g G'
φ' : G' ≃g G''
x✝ : G.ConnectedComponent
a✝ : V
⊢ (connectedComponentEquiv (RelIso.trans φ φ')) (Quot.mk G.Reachable a✝) =
    (φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv) (Quot.mk G.Reachable a✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem ofNat_mul_nonneg {a b : Nat} : 0 ≤ (a : Int) * b

Proof state:
a b : Nat
⊢ 0 ≤ ↑(a * b)

Tactic:
exact Int.ofNat_zero_le (a * b)

Result:
no goals

Proof state:
a b : Nat
⊢ 0 ≤ ↑a * ↑b

Tactic:
rw [← Int.ofNat_mul]

Result:
a b : Nat
⊢ 0 ≤ ↑(a * b)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem and_xor_distrib_left {a b c : Nat} : a &&& (b ^^^ c) = (a &&& b) ^^^ (a &&& c)

Proof state:
case pred
a b c : Nat
⊢ ∀ (i : Nat), (a &&& (b ^^^ c)).testBit i = (a &&& b ^^^ a &&& c).testBit i

Tactic:
simp [Bool.and_xor_distrib_left]

Result:
no goals

Proof state:
a b c : Nat
⊢ a &&& (b ^^^ c) = a &&& b ^^^ a &&& c

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
a b c : Nat
⊢ ∀ (i : Nat), (a &&& (b ^^^ c)).testBit i = (a &&& b ^^^ a &&& c).testBit i
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem tendsto_pow_atTop_nhds_zero_of_norm_lt_one {R : Type*} [NormedRing R] {x : R}
    (h : ‖x‖ < 1) :
    Tendsto (fun n : ℕ ↦ x ^ n) atTop (𝓝 0)

Proof state:
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
⊢ Tendsto (fun n => x ^ n) atTop (𝓝 0)

Tactic:
apply squeeze_zero_norm' (eventually_norm_pow_le x)

Result:
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
⊢ Tendsto (HPow.hPow ‖x‖) atTop (𝓝 0)

Proof state:
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
⊢ Tendsto (HPow.hPow ‖x‖) atTop (𝓝 0)

Tactic:
exact tendsto_pow_atTop_nhds_zero_of_lt_one (norm_nonneg _) h

Result:
no goals
-- Mathlib/LinearAlgebra/FreeModule/PID.lean
@[simp] lemma repr_comp_embedding_eq_smul :
    snf.bM.repr m ∘ snf.f = snf.a • (snf.bN.repr m : Fin n → R)

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
⊢ ⇑(snf.bM.repr ↑m) ∘ ⇑snf.f = snf.a • ⇑(snf.bN.repr m)

Tactic:
ext i

Result:
case h
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
i : Fin n
⊢ (⇑(snf.bM.repr ↑m) ∘ ⇑snf.f) i = (snf.a • ⇑(snf.bN.repr m)) i

Proof state:
case h
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
i : Fin n
⊢ (⇑(snf.bM.repr ↑m) ∘ ⇑snf.f) i = (snf.a • ⇑(snf.bN.repr m)) i

Tactic:
simp [Pi.smul_apply (snf.a i)]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem map₂_mk_top_top_eq_top : Submodule.map₂ (mk R M N) ⊤ ⊤ = ⊤

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} ≤ Submodule.span R (Set.image2 (fun m n => ((mk R M N) m) n) ↑⊤ ↑⊤)

Tactic:
exact Submodule.span_mono fun _ ⟨m, n, h⟩ => ⟨m, trivial, n, trivial, h⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ Submodule.map₂ (mk R M N) ⊤ ⊤ = ⊤

Tactic:
rw [← top_le_iff, ← span_tmul_eq_top, Submodule.map₂_eq_span_image2]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} ≤ Submodule.span R (Set.image2 (fun m n => ((mk R M N) m) n) ↑⊤ ↑⊤)
-- Mathlib/Data/List/Sublists.lean
theorem nodup_sublistsLen (n : ℕ) {l : List α} (h : Nodup l) : (sublistsLen n l).Nodup

Proof state:
α : Type u
n : ℕ
l : List α
h : l.Nodup
this : Pairwise (fun x1 x2 => x1 ≠ x2) l.sublists'
⊢ (sublistsLen n l).Nodup

Tactic:
exact this.sublist (sublistsLen_sublist_sublists' _ _)

Result:
no goals

Proof state:
case h.e'_2.h.e'_4.h.h
α : Type u
n : ℕ
l : List α
h✝ : l.Nodup
a✝ b✝ : List α
h : Lex (swap fun x1 x2 => x1 ≠ x2) a✝ b✝
x✝ : α
⊢ (fun x1 => ¬x1 = x✝) = fun x2 => x✝ ≠ x2

Tactic:
simp [swap, eq_comm]

Result:
no goals

Proof state:
α : Type u
n : ℕ
l : List α
h✝ : l.Nodup
a✝ b✝ : List α
h : Lex (swap fun x1 x2 => x1 ≠ x2) a✝ b✝
⊢ Lex (fun x1 x2 => x1 ≠ x2) a✝ b✝

Tactic:
convert h using 3

Result:
case h.e'_2.h.e'_4.h.h
α : Type u
n : ℕ
l : List α
h✝ : l.Nodup
a✝ b✝ : List α
h : Lex (swap fun x1 x2 => x1 ≠ x2) a✝ b✝
x✝ : α
⊢ (fun x1 => ¬x1 = x✝) = fun x2 => x✝ ≠ x2
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_zero (x : ℝ) : x ^ (0 : ℝ) = 1

Proof state:
x : ℝ
⊢ x ^ 0 = 1

Tactic:
simp [rpow_def]

Result:
no goals