harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem curr : ∀ {it}, ValidFor l r it → it.curr = r.headD default
  | it, h => by cases h.out'; apply get_of_valid

Proof state:
case refl
l r : List Char
h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }
⊢ { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }.curr = r.headD default

Tactic:
apply get_of_valid

Result:
no goals

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ it.curr = r.headD default

Tactic:
cases h.out'

Result:
case refl
l r : List Char
h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }
⊢ { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }.curr = r.headD default
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma rightUnshift_units_smul {n' a : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ)
    (hn : n' + a = n) (x : Rˣ) :
    (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
x : Rˣ
⊢ (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn

Tactic:
apply rightUnshift_smul

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp]
lemma notNilRec_cons {motive : {u w : V} → (p : G.Walk u w) → ¬ p.Nil → Sort*}
    (cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) →
    motive (q.cons h) Walk.not_nil_cons) (h' : G.Adj u v) (q' : G.Walk v w) :
    @Walk.notNilRec _ _ _ _ _ cons _ _ = cons h' q'

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
motive : {u w : V} → (p : G.Walk u w) → ¬p.Nil → Sort u_1
cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (SimpleGraph.Walk.cons h q) ⋯
h' : G.Adj u v
q' : G.Walk v w
⊢ notNilRec (fun {u v w} => cons) (SimpleGraph.Walk.cons h' q') ⋯ = cons h' q'

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Oscillation.lean
theorem uniform_oscillation {K : Set E} (comp : IsCompact K)
    {f : E → F} {ε : ENNReal} (hK : ∀ x ∈ K, oscillation f x < ε) :
    ∃ δ > 0, ∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ))) ≤ ε

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
comp : IsCompact K
f : E → F
ε : ℝ≥0∞
hK : ∀ x ∈ K, oscillationWithin f univ x < ε
⊢ ∃ δ > 0, ∀ x ∈ K, diam (f '' ball x (ENNReal.ofReal δ)) ≤ ε

Tactic:
convert ← comp.uniform_oscillationWithin hK

Result:
case h.e'_2.h.h.e'_2.h.h'.h.e'_3.h.e'_3.h.e'_4
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
comp : IsCompact K
f : E → F
ε : ℝ≥0∞
hK : ∀ x ∈ K, oscillationWithin f univ x < ε
x✝ : ℝ
a✝¹ : E
a✝ : a✝¹ ∈ K
⊢ ball a✝¹ (ENNReal.ofReal x✝) ∩ univ = ball a✝¹ (ENNReal.ofReal x✝)

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
comp : IsCompact K
f : E → F
ε : ℝ≥0∞
hK : ∀ x ∈ K, oscillation f x < ε
⊢ ∃ δ > 0, ∀ x ∈ K, diam (f '' ball x (ENNReal.ofReal δ)) ≤ ε

Tactic:
simp only [← oscillationWithin_univ_eq_oscillation] at hK

Result:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
comp : IsCompact K
f : E → F
ε : ℝ≥0∞
hK : ∀ x ∈ K, oscillationWithin f univ x < ε
⊢ ∃ δ > 0, ∀ x ∈ K, diam (f '' ball x (ENNReal.ofReal δ)) ≤ ε

Proof state:
case h.e'_2.h.h.e'_2.h.h'.h.e'_3.h.e'_3.h.e'_4
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
comp : IsCompact K
f : E → F
ε : ℝ≥0∞
hK : ∀ x ∈ K, oscillationWithin f univ x < ε
x✝ : ℝ
a✝¹ : E
a✝ : a✝¹ ∈ K
⊢ ball a✝¹ (ENNReal.ofReal x✝) ∩ univ = ball a✝¹ (ENNReal.ofReal x✝)

Tactic:
exact inter_univ _

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem Asymptotics.IsBigO.hasFDerivWithinAt {s : Set E} {x₀ : E} {n : ℕ}
    (h : f =O[𝓝[s] x₀] fun x => ‖x - x₀‖ ^ n) (hx₀ : x₀ ∈ s) (hn : 1 < n) :
    HasFDerivWithinAt f (0 : E →L[𝕜] F) s x₀

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x₀ : E
n : ℕ
h : f =O[𝓝[s] x₀] fun x => ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : 1 < n
⊢ HasFDerivWithinAt f 0 s x₀

Tactic:
simp_rw [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleO,
  h.eq_zero_of_norm_pow_within hx₀ hn.ne_bot, zero_apply, sub_zero,
  h.trans_isLittleO ((isLittleO_pow_sub_sub x₀ hn).mono nhdsWithin_le_nhds)]

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem supIndep_univ_bool (f : Bool → α) :
    (Finset.univ : Finset Bool).SupIndep f ↔ Disjoint (f false) (f true) :=
  haveI : true ≠ false

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : Bool → α
⊢ true ≠ false

Tactic:
simp only [Ne, not_false_iff, reduceCtorEq]

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem not_mem_erase_self {a : α} {s : Finmap β} : ¬a ∈ erase a s

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a ∉ erase a s

Tactic:
rw [mem_erase, not_and_or, not_not]

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a = a ∨ a ∉ s

Proof state:
case h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a = a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a = a ∨ a ∉ s

Tactic:
left

Result:
case h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a = a
-- Mathlib/RingTheory/Ideal/Defs.lean
theorem pow_mem_of_pow_mem {m n : ℕ} (ha : a ^ m ∈ I) (h : m ≤ n) : a ^ n ∈ I

Proof state:
α : Type u
inst✝ : Semiring α
I : Ideal α
a : α
m n : ℕ
ha : a ^ m ∈ I
h : m ≤ n
⊢ a ^ n ∈ I

Tactic:
rw [← Nat.add_sub_of_le h, add_comm, pow_add]

Result:
α : Type u
inst✝ : Semiring α
I : Ideal α
a : α
m n : ℕ
ha : a ^ m ∈ I
h : m ≤ n
⊢ a ^ (n - m) * a ^ m ∈ I

Proof state:
α : Type u
inst✝ : Semiring α
I : Ideal α
a : α
m n : ℕ
ha : a ^ m ∈ I
h : m ≤ n
⊢ a ^ (n - m) * a ^ m ∈ I

Tactic:
exact I.mul_mem_left _ ha

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZeta.lean
lemma differentiableAt_hurwitzZeta_sub_one_div (a : UnitAddCircle) :
    DifferentiableAt ℂ (fun s ↦ hurwitzZeta a s - 1 / (s - 1) / Gammaℝ s) 1

Proof state:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s => hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) 1

Tactic:
simp only [hurwitzZeta, add_sub_right_comm]

Result:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s => hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ + hurwitzZetaOdd a s) 1

Proof state:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s => hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ + hurwitzZetaOdd a s) 1

Tactic:
exact (differentiableAt_hurwitzZetaEven_sub_one_div a).add (differentiable_hurwitzZetaOdd a 1)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_left_eq_self {x y : Array α} : x ++ y = y ↔ x = #[]

Proof state:
α : Type u_1
x y : Array α
⊢ x ++ y = y ↔ x = #[]

Tactic:
rw [← append_left_inj (s₁ := x), empty_append]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
lemma nnnorm_commutator_sub_one_le (ha : a ≠ 0) (hb : b ≠ 0) :
    ‖a * b * a⁻¹ * b⁻¹ - 1‖₊ ≤ 2 * ‖a‖₊⁻¹ * ‖b‖₊⁻¹ * ‖a - 1‖₊ * ‖b - 1‖₊

Proof state:
α : Type u_2
inst✝ : NormedDivisionRing α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ ‖a * b * a⁻¹ * b⁻¹ - 1‖₊ ≤ 2 * ‖a‖₊⁻¹ * ‖b‖₊⁻¹ * ‖a - 1‖₊ * ‖b - 1‖₊

Tactic:
simpa using nnnorm_commutator_units_sub_one_le (.mk0 a ha) (.mk0 b hb)

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem singularPart_smul_nnreal (s : SignedMeasure α) (μ : Measure α) (r : ℝ≥0) :
    (r • s).singularPart μ = r • s.singularPart μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ (r • s).singularPart μ = r • s.singularPart μ

Tactic:
rw [singularPart, singularPart, smul_sub, ← toSignedMeasure_smul, ← toSignedMeasure_smul]

Result:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
-- Mathlib/Computability/Primrec.lean
theorem list_append : Primrec₂ ((· ++ ·) : List α → List α → List α) :=
  (list_foldr fst snd <| to₂ <| comp (@list_cons α _) snd).to₂.of_eq fun l₁ l₂ => by
    induction l₁ <;> simp [*]

Proof state:
α : Type u_1
inst✝ : Primcodable α
l₁ l₂ : List α
⊢ List.foldr (fun b s => ((l₁, l₂), b, s).2.1 :: ((l₁, l₂), b, s).2.2) (l₁, l₂).2 (l₁, l₂).1 = l₁ ++ l₂

Tactic:
induction l₁ <;> simp [*]

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
theorem directSumLeft_tmul_lof (i : ι₁) (x : M₁ i) (y : M₂') :
    directSumLeft R M₁ M₂' (DirectSum.lof R _ _ i x ⊗ₜ[R] y) =
    DirectSum.lof R _ _ i (x ⊗ₜ[R] y)

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
ι₁ : Type v₁
inst✝⁴ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝³ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝² : AddCommMonoid M₂'
inst✝¹ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝ : Module R M₂'
i : ι₁
x : M₁ i
y : M₂'
⊢ ((toModule R ι₁ (M₂' →ₗ[R] ⨁ (i : ι₁), M₁ i ⊗[R] M₂') fun x =>
          (mk R (M₁ x) M₂').compr₂ (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') x))
        ((lof R ι₁ M₁ i) x))
      y =
    (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)

Tactic:
rw [DirectSum.toModule_lof R i]

Result:
R : Type u
inst✝⁵ : CommSemiring R
ι₁ : Type v₁
inst✝⁴ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝³ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝² : AddCommMonoid M₂'
inst✝¹ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝ : Module R M₂'
i : ι₁
x : M₁ i
y : M₂'
⊢ (((mk R (M₁ i) M₂').compr₂ (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i)) x) y =
    (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
ι₁ : Type v₁
inst✝⁴ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝³ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝² : AddCommMonoid M₂'
inst✝¹ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝ : Module R M₂'
i : ι₁
x : M₁ i
y : M₂'
⊢ (directSumLeft R M₁ M₂') ((lof R ι₁ M₁ i) x ⊗ₜ[R] y) = (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)

Tactic:
dsimp only [directSumLeft, LinearEquiv.ofLinear_apply, lift.tmul]

Result:
R : Type u
inst✝⁵ : CommSemiring R
ι₁ : Type v₁
inst✝⁴ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝³ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝² : AddCommMonoid M₂'
inst✝¹ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝ : Module R M₂'
i : ι₁
x : M₁ i
y : M₂'
⊢ ((toModule R ι₁ (M₂' →ₗ[R] ⨁ (i : ι₁), M₁ i ⊗[R] M₂') fun x =>
          (mk R (M₁ x) M₂').compr₂ (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') x))
        ((lof R ι₁ M₁ i) x))
      y =
    (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
ι₁ : Type v₁
inst✝⁴ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝³ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝² : AddCommMonoid M₂'
inst✝¹ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝ : Module R M₂'
i : ι₁
x : M₁ i
y : M₂'
⊢ (((mk R (M₁ i) M₂').compr₂ (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i)) x) y =
    (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
    {l : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Sigma.fst) :
    (insertMany empty l).1.getKey! k' = k

Proof state:
α : Type u
β : α → Type v
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Sigma.fst l
⊢ (empty.insertMany l).val.getKey! k' = k

Tactic:
rw [getKey!_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_zero_right (x : F) : ⟪x, 0⟫ = 0

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ ⟪x, 0⟫_𝕜 = 0

Tactic:
rw [← inner_conj_symm, inner_zero_left]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ (starRingEnd 𝕜) 0 = 0

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ (starRingEnd 𝕜) 0 = 0

Tactic:
simp only [RingHom.map_zero]

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem map_trans (γ : Path x y) (γ' : Path y z) {f : X → Y}
    (h : Continuous f) : (γ.trans γ').map h = (γ.map h).trans (γ'.map h)

Proof state:
case a.h
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous f
t : ↑I
⊢ ((γ.trans γ').map h) t = ((γ.map h).trans (γ'.map h)) t

Tactic:
rw [trans_apply, map_coe, Function.comp_apply, trans_apply]

Result:
case a.h
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous f
t : ↑I
⊢ f (if h : ↑t ≤ 1 / 2 then γ ⟨2 * ↑t, ⋯⟩ else γ' ⟨2 * ↑t - 1, ⋯⟩) =
    if h_1 : ↑t ≤ 1 / 2 then (γ.map h) ⟨2 * ↑t, ⋯⟩ else (γ'.map h) ⟨2 * ↑t - 1, ⋯⟩

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous f
⊢ (γ.trans γ').map h = (γ.map h).trans (γ'.map h)

Tactic:
ext t

Result:
case a.h
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous f
t : ↑I
⊢ ((γ.trans γ').map h) t = ((γ.map h).trans (γ'.map h)) t

Proof state:
case a.h
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous f
t : ↑I
⊢ f (if h : ↑t ≤ 1 / 2 then γ ⟨2 * ↑t, ⋯⟩ else γ' ⟨2 * ↑t - 1, ⋯⟩) =
    if h_1 : ↑t ≤ 1 / 2 then (γ.map h) ⟨2 * ↑t, ⋯⟩ else (γ'.map h) ⟨2 * ↑t - 1, ⋯⟩

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_zero_right (n : ℕ) : choose n 0 = 1

Proof state:
n : ℕ
⊢ n.choose 0 = 1

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Basic.lean
@[simp]
lemma neg_div_neg_eq (a b : R) : -a / -b = a / b

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -a / -b = a / b

Tactic:
rw [div_neg_eq_neg_div, neg_div, neg_neg]

Result:
no goals
-- Mathlib/Algebra/Group/Int/Even.lean
@[parity_simps] lemma even_sub_one : Even (n - 1) ↔ ¬Even n

Proof state:
n : ℤ
⊢ Even (n - 1) ↔ ¬Even n

Tactic:
simp [even_sub]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean
theorem one_of_one_le (h : 1 ≤ x) : smoothTransition x = 1 :=
  (div_eq_one_iff_eq <| (pos_denom x).ne').2 <| by rw [zero_of_nonpos (sub_nonpos.2 h), add_zero]

Proof state:
x : ℝ
h : 1 ≤ x
⊢ expNegInvGlue x = expNegInvGlue x + expNegInvGlue (1 - x)

Tactic:
rw [zero_of_nonpos (sub_nonpos.2 h), add_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem _root_.ContinuousLinearMap.intervalIntegral_apply {a b : ℝ} {φ : ℝ → F →L[𝕜] E}
    (hφ : IntervalIntegrable φ μ a b) (v : F) :
    (∫ x in a..b, φ x ∂μ) v = ∫ x in a..b, φ x v ∂μ

Proof state:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
μ : Measure ℝ
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b : ℝ
φ : ℝ → F →L[𝕜] E
hφ : IntervalIntegrable φ μ a b
v : F
⊢ (∫ (x : ℝ) in a..b, φ x ∂μ) v = ∫ (x : ℝ) in a..b, (φ x) v ∂μ

Tactic:
simp_rw [intervalIntegral_eq_integral_uIoc, ← integral_apply hφ.def' v, coe_smul', Pi.smul_apply]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem eventuallyEq_empty {s : Set α} {l : Filter α} : s =ᶠ[l] (∅ : Set α) ↔ ∀ᶠ x in l, x ∉ s :=
  eventuallyEq_set.trans <| by simp

Proof state:
α : Type u
s : Set α
l : Filter α
⊢ (∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ ∅) ↔ ∀ᶠ (x : α) in l, x ∉ s

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma lambda_not_dvd_Y : ¬ λ ∣ S.Y :=
  fun h ↦ lambda_not_dvd_y S <| Y_u₂_spec S ▸ dvd_mul_of_dvd_left (dvd_pow h (by decide)) _

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ FermatLastTheoremForThreeGen.Solution.Y S
⊢ 3 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_range_div' {M : Type*} [CommGroup M] (f : ℕ → M) (n : ℕ) :
    (∏ i ∈ range n, f i / f (i + 1)) = f 0 / f n

Proof state:
M : Type u_6
inst✝ : CommGroup M
f : ℕ → M
n : ℕ
⊢ ∏ i ∈ range n, f i / f (i + 1) = f 0 / f n

Tactic:
apply prod_range_induction <;> simp

Result:
no goals
-- Mathlib/Topology/OmegaCompletePartialOrder.lean
theorem isOpen_sUnion (s : Set (Set α)) (hs : ∀ t ∈ s, IsOpen α t) : IsOpen α (⋃₀ s)

Proof state:
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ t ∈ s, IsOpen α t
⊢ IsOpen α (⋃₀ s)

Tactic:
simp only [IsOpen] at hs ⊢

Result:
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ t ∈ s, ωScottContinuous fun x => x ∈ t
⊢ ωScottContinuous fun x => x ∈ ⋃₀ s

Proof state:
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ t ∈ s, ωScottContinuous fun x => x ∈ t
⊢ ωScottContinuous fun x => x ∈ ⋃₀ s

Tactic:
convert CompleteLattice.ωScottContinuous.sSup hs

Result:
case h.e'_5.h.h.e
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ t ∈ s, ωScottContinuous fun x => x ∈ t
x✝ : α
⊢ Membership.mem (⋃₀ s) = sSup s

Proof state:
case h.e'_5.h.h.e
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ t ∈ s, ωScottContinuous fun x => x ∈ t
x✝ : α
⊢ Membership.mem (⋃₀ s) = sSup s

Tactic:
aesop

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
lemma levyProkhorovEDist_comm (μ ν : Measure Ω) :
    levyProkhorovEDist μ ν = levyProkhorovEDist ν μ

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
⊢ levyProkhorovEDist μ ν = levyProkhorovEDist ν μ

Tactic:
simp only [levyProkhorovEDist, and_comm]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem map_smul (x : S) (z : R) : map Q g hy (z • x : S) = g z • map Q g hy x

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
⊢ (map Q g hy) (z • x) = g z • (map Q g hy) x

Tactic:
rw [Algebra.smul_def, Algebra.smul_def, RingHom.map_mul, map_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean
theorem VanishesTrivially.of_fintype {κ} [Fintype κ] (a : ι → κ → R) (y : κ → N)
    (hay : ∀ i, n i = ∑ j, a i j • y j) (ham : ∀ j, ∑ i, a i j • m i = 0) :
    VanishesTrivially R m n :=
  have e := (Fintype.equivFin κ).symm
  ⟨Fintype.card κ, (a · ∘ e), y ∘ e, by simpa only [← e.sum_comp] using hay, by
    rwa [← e.forall_congr_right] at ham⟩

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type u_4
inst✝¹ : Fintype ι
m : ι → M
n : ι → N
κ : Type u_5
inst✝ : Fintype κ
a : ι → κ → R
y : κ → N
hay : ∀ (i : ι), n i = ∑ j : κ, a i j • y j
ham : ∀ (j : κ), ∑ i : ι, a i j • m i = 0
e : Fin (Fintype.card κ) ≃ κ
⊢ ∀ (i : ι), n i = ∑ j : Fin (Fintype.card κ), (fun x => a x ∘ ⇑e) i j • (y ∘ ⇑e) j

Tactic:
simpa only [← e.sum_comp] using hay

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type u_4
inst✝¹ : Fintype ι
m : ι → M
n : ι → N
κ : Type u_5
inst✝ : Fintype κ
a : ι → κ → R
y : κ → N
hay : ∀ (i : ι), n i = ∑ j : κ, a i j • y j
ham : ∀ (j : κ), ∑ i : ι, a i j • m i = 0
e : Fin (Fintype.card κ) ≃ κ
⊢ ∀ (j : Fin (Fintype.card κ)), ∑ i : ι, (fun x => a x ∘ ⇑e) i j • m i = 0

Tactic:
rwa [← e.forall_congr_right] at ham

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
lemma map (hφ : φ.IsHomogeneous n) (f : R →+* S) : (map f φ).IsHomogeneous n

Proof state:
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
f : R →+* S
⊢ ((MvPolynomial.map f) φ).IsHomogeneous n

Tactic:
simpa only [one_mul] using hφ.eval₂ _ _ (fun r ↦ isHomogeneous_C _ (f r)) (isHomogeneous_X _)

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem count_finsupp_prod (exps : HeightOneSpectrum R →₀ ℤ) :
    count K v (exps.prod (HeightOneSpectrum.asIdeal · ^ ·)) = exps v

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
⊢ count K v (exps.prod fun x1 x2 => ↑x1.asIdeal ^ x2) = exps v

Tactic:
rw [Finsupp.prod, count_prod]

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
⊢ ∑ i ∈ exps.support, count K v (↑i.asIdeal ^ exps i) = exps v

case hS
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
⊢ ∀ i ∈ exps.support, ↑i.asIdeal ^ exps i ≠ 0

Proof state:
case hS
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
⊢ ∀ i ∈ exps.support, ↑i.asIdeal ^ exps i ≠ 0

Tactic:
exact fun v hv ↦ zpow_ne_zero _ (coeIdeal_ne_zero.mpr v.ne_bot)

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
⊢ ∑ i ∈ exps.support, count K v (↑i.asIdeal ^ exps i) = exps v

Tactic:
classical simp only [count_zpow, count_maximal, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq',
  exps.mem_support_iff, ne_eq, ite_not, ite_eq_right_iff, @eq_comm ℤ 0, imp_self]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
⊢ ∑ i ∈ exps.support, count K v (↑i.asIdeal ^ exps i) = exps v

Tactic:
simp only [count_zpow, count_maximal, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq',
exps.mem_support_iff, ne_eq, ite_not, ite_eq_right_iff, @eq_comm ℤ 0, imp_self]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem coe_iInf {ι : Sort*} {S : ι → Subgroup G} : (↑(⨅ i, S i) : Set G) = ⋂ i, S i

Proof state:
G : Type u_1
inst✝ : Group G
ι : Sort u_2
S : ι → Subgroup G
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Result:
no goals