harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem maybeNormalize_eq_normalize {num : Int} {den g : Nat} (den_nz reduced)
    (hn : ↑g ∣ num) (hd : g ∣ den) :
    maybeNormalize num den g den_nz reduced = normalize num den (mt (by simp [·]) den_nz)

Proof state:
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)
hn : ↑g ∣ num
hd : g ∣ den
⊢ maybeNormalize num den g den_nz reduced = normalize num den ⋯

Tactic:
simp only [maybeNormalize_eq, mk_eq_normalize, Int.tdiv_eq_ediv_of_dvd hn]

Result:
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)
hn : ↑g ∣ num
hd : g ∣ den
⊢ normalize (num / ↑g) (den / g) den_nz = normalize num den ⋯

Proof state:
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)
hn : ↑g ∣ num
hd : g ∣ den
this : g ≠ 0
⊢ normalize num (den / g * g) ⋯ = normalize num den ⋯

Tactic:
congr 1

Result:
case e_den
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)
hn : ↑g ∣ num
hd : g ∣ den
this : g ≠ 0
⊢ den / g * g = den

Proof state:
case e_den
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)
hn : ↑g ∣ num
hd : g ∣ den
this : g ≠ 0
⊢ den / g * g = den

Tactic:
exact Nat.div_mul_cancel hd

Result:
no goals

Proof state:
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)
hn : ↑g ∣ num
hd : g ∣ den
this : g ≠ 0
⊢ normalize (num / ↑g) (den / g) den_nz = normalize num den ⋯

Tactic:
rw [← normalize_mul_right _ this, Int.ediv_mul_cancel hn]

Result:
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)
hn : ↑g ∣ num
hd : g ∣ den
this : g ≠ 0
⊢ normalize num (den / g * g) ⋯ = normalize num den ⋯
-- Mathlib/Analysis/SpecialFunctions/CompareExp.lean
theorem abs_im_pow_eventuallyLE_exp_re (hl : IsExpCmpFilter l) (n : ℕ) :
    (fun z : ℂ => |z.im| ^ n) ≤ᶠ[l] fun z => Real.exp z.re

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z => |z.im| ^ n) ≤ᶠ[l] fun z => Real.exp z.re

Tactic:
simpa using (hl.isLittleO_im_pow_exp_re n).bound zero_lt_one

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
theorem isCompactOpen_iff_eq_finset_affine_union {X : Scheme} (U : Set X) :
    IsCompact U ∧ IsOpen U ↔ ∃ s : Set X.affineOpens, s.Finite ∧ U = ⋃ i ∈ s, i

Proof state:
case hb'
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ ∀ (i : ↑X.affineOpens), IsCompact ↑↑i

Tactic:
exact fun i => i.2.isCompact

Result:
no goals

Proof state:
case hb
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ Opens.IsBasis X.affineOpens

Tactic:
exact isBasis_affine_open X

Result:
no goals

Proof state:
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, ↑↑i

Tactic:
apply Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion
  (fun (U : X.affineOpens) => (U : X.Opens))

Result:
case hb
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ Opens.IsBasis (Set.range fun U => ↑U)

case hb'
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ ∀ (i : ↑X.affineOpens), IsCompact ↑↑i

Proof state:
case hb
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ Opens.IsBasis (Set.range fun U => ↑U)

Tactic:
rw [Subtype.range_coe]

Result:
case hb
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ Opens.IsBasis X.affineOpens
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem map_ne_zero [Nontrivial R] (hI : I ≠ 0) : I.map h ≠ 0

Proof state:
case intro.intro
R : Type u_1
inst✝⁷ : CommRing R
K : Type u_3
K' : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Field K'
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra R K'
inst✝¹ : IsFractionRing R K'
I : FractionalIdeal R⁰ K
h : K →ₐ[R] K'
inst✝ : Nontrivial R
hI : I ≠ 0
x : R
hx : (algebraMap R K) x ∈ I
map_eq_zero : map h I = 0
⊢ ∃ x_1 ∈ I, h x_1 = (algebraMap R K') x

Tactic:
exact ⟨algebraMap R K x, hx, h.commutes x⟩

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝⁷ : CommRing R
K : Type u_3
K' : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Field K'
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra R K'
inst✝¹ : IsFractionRing R K'
I : FractionalIdeal R⁰ K
h : K →ₐ[R] K'
inst✝ : Nontrivial R
hI : I ≠ 0
x : R
x_ne_zero : x ≠ 0
hx : (algebraMap R K) x ∈ I
⊢ map h I ≠ 0

Tactic:
contrapose! x_ne_zero with map_eq_zero

Result:
case intro.intro
R : Type u_1
inst✝⁷ : CommRing R
K : Type u_3
K' : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Field K'
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra R K'
inst✝¹ : IsFractionRing R K'
I : FractionalIdeal R⁰ K
h : K →ₐ[R] K'
inst✝ : Nontrivial R
hI : I ≠ 0
x : R
hx : (algebraMap R K) x ∈ I
map_eq_zero : map h I = 0
⊢ x = 0

Proof state:
case intro.intro
R : Type u_1
inst✝⁷ : CommRing R
K : Type u_3
K' : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Field K'
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra R K'
inst✝¹ : IsFractionRing R K'
I : FractionalIdeal R⁰ K
h : K →ₐ[R] K'
inst✝ : Nontrivial R
hI : I ≠ 0
x : R
hx : (algebraMap R K) x ∈ I
map_eq_zero : map h I = 0
⊢ x = 0

Tactic:
refine IsFractionRing.to_map_eq_zero_iff.mp (eq_zero_iff.mp map_eq_zero _ (mem_map.mpr ?_))

Result:
case intro.intro
R : Type u_1
inst✝⁷ : CommRing R
K : Type u_3
K' : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Field K'
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra R K'
inst✝¹ : IsFractionRing R K'
I : FractionalIdeal R⁰ K
h : K →ₐ[R] K'
inst✝ : Nontrivial R
hI : I ≠ 0
x : R
hx : (algebraMap R K) x ∈ I
map_eq_zero : map h I = 0
⊢ ∃ x_1 ∈ I, h x_1 = (algebraMap R K') x

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
K : Type u_3
K' : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Field K'
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra R K'
inst✝¹ : IsFractionRing R K'
I : FractionalIdeal R⁰ K
h : K →ₐ[R] K'
inst✝ : Nontrivial R
hI : I ≠ 0
⊢ map h I ≠ 0

Tactic:
obtain ⟨x, x_ne_zero, hx⟩ := exists_ne_zero_mem_isInteger hI

Result:
case intro.intro
R : Type u_1
inst✝⁷ : CommRing R
K : Type u_3
K' : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Field K'
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra R K'
inst✝¹ : IsFractionRing R K'
I : FractionalIdeal R⁰ K
h : K →ₐ[R] K'
inst✝ : Nontrivial R
hI : I ≠ 0
x : R
x_ne_zero : x ≠ 0
hx : (algebraMap R K) x ∈ I
⊢ map h I ≠ 0
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem ext {c d : Con M} (H : ∀ x y, c x y ↔ d x y) : c = d :=
  ext' <| by ext; apply H

Proof state:
case h.h.a
M : Type u_1
inst✝ : Mul M
c d : Con M
H : ∀ (x y : M), c x y ↔ d x y
x✝¹ x✝ : M
⊢ c x✝¹ x✝ ↔ d x✝¹ x✝

Tactic:
apply H

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
c d : Con M
H : ∀ (x y : M), c x y ↔ d x y
⊢ ⇑c = ⇑d

Tactic:
ext

Result:
case h.h.a
M : Type u_1
inst✝ : Mul M
c d : Con M
H : ∀ (x y : M), c x y ↔ d x y
x✝¹ x✝ : M
⊢ c x✝¹ x✝ ↔ d x✝¹ x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem if_false_left [h : Decidable p] :
    ite p False q ↔ ¬p ∧ q

Proof state:
p q : Prop
h : Decidable p
⊢ (if p then False else q) ↔ ¬p ∧ q

Tactic:
cases h <;> (rename_i g; simp [g])

Result:
no goals

Proof state:
case isTrue
p q : Prop
g : p
⊢ (if p then False else q) ↔ ¬p ∧ q

Tactic:
simp [g]

Result:
no goals

Proof state:
case isTrue
p q : Prop
h✝ : p
⊢ (if p then False else q) ↔ ¬p ∧ q

Tactic:
rename_i g

Result:
case isTrue
p q : Prop
g : p
⊢ (if p then False else q) ↔ ¬p ∧ q
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_append : (l₁ ++ l₂).prod = l₁.prod * l₂.prod :=
  calc
    (l₁ ++ l₂).prod = foldr (· * ·) (1 * foldr (· * ·) 1 l₂) l₁

Proof state:
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
⊢ (l₁ ++ l₂).prod = foldr (fun x1 x2 => x1 * x2) (1 * foldr (fun x1 x2 => x1 * x2) 1 l₂) l₁

Tactic:
simp [List.prod]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
@[simp]
lemma zero_comp (a : M) {b c : M} (β : ShiftedHom Y Z b) (h : b + a = c) :
    (0 : ShiftedHom X Y a).comp β h = 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_5, u_1} C
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
X Y Z : C
inst✝ : Preadditive C
a b c : M
β : ShiftedHom Y Z b
h : b + a = c
⊢ comp 0 β h = 0

Tactic:
rw [comp, Limits.zero_comp]

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma homMk₅_app_five :
    (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨5, by valid⟩ = app₅ := rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.374178, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯
app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯
app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯
app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯
app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯
app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯
w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯
w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯
w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯
w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄ = app₃ ≫ g.map' 3 4 ⋯ ⋯
w₄ : f.map' 4 5 ⋯ ⋯ ≫ app₅ = app₄ ≫ g.map' 4 5 ⋯ ⋯
⊢ 5 < 5 + 1

Tactic:
valid

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem smul_set_neg : a • -t = -(a • t)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
a : α
t : Set β
⊢ a • -t = -(a • t)

Tactic:
simp_rw [← image_smul, ← image_neg_eq_neg, image_image, smul_neg]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem diam_univ_of_noncompact [ProperSpace α] [NoncompactSpace α] : diam (univ : Set α) = 0

Proof state:
α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : ProperSpace α
inst✝ : NoncompactSpace α
⊢ diam univ = 0

Tactic:
simp [diam]

Result:
no goals
-- Mathlib/Computability/Language.lean
theorem kstar_def_nonempty (l : Language α) :
    l∗ = { x | ∃ S : List (List α), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ [] }

Proof state:
case h
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ ↔ x ∈ {x | ∃ S, x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []}

Tactic:
apply mem_kstar_iff_exists_nonempty

Result:
no goals

Proof state:
α : Type u_1
l : Language α
⊢ l∗ = {x | ∃ S, x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []}

Tactic:
ext x

Result:
case h
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ ↔ x ∈ {x | ∃ S, x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []}
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem contMDiff_tangentBundleModelSpaceHomeomorph_symm {n : ℕ∞} :
    ContMDiff (I.prod 𝓘(𝕜, E)) I.tangent n
    ((tangentBundleModelSpaceHomeomorph I).symm : ModelProd H E → TangentBundle I H)

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
⊢ ContMDiff (I.prod 𝓘(𝕜, E)) I.tangent ↑n ⇑(tangentBundleModelSpaceHomeomorph I).symm

Tactic:
apply contMDiff_iff.2 ⟨Homeomorph.continuous _, fun x y ↦ ?_⟩

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞
x : ModelProd H E
y : TangentBundle I H
⊢ ContDiffOn 𝕜 (↑n)
    (↑(extChartAt I.tangent y) ∘ ⇑(tangentBundleModelSpaceHomeomorph I).symm ∘ ↑(extChartAt (I.prod 𝓘(𝕜, E)) x).symm)
    ((extChartAt (I.prod 𝓘(𝕜, E)) x).target ∩
      ↑(extChartAt (I.prod 𝓘(𝕜, E)) x).symm ⁻¹'
        (⇑(tangentBundleModelSpaceHomeomorph I).symm ⁻¹' (extChartAt I.tangent y).source))
-- Mathlib/Probability/Martingale/Centering.lean
theorem martingalePart_eq_sum : martingalePart f ℱ μ = fun n =>
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i|ℱ i])

Proof state:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
⊢ (fun n => f n - ∑ i ∈ Finset.range n, μ[f (i + 1) - f i|↑ℱ i]) = fun n =>
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i])

Tactic:
ext1 n

Result:
case h
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
n : ℕ
⊢ f n - ∑ i ∈ Finset.range n, μ[f (i + 1) - f i|↑ℱ i] =
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i])

Proof state:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
⊢ martingalePart f ℱ μ = fun n => f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i])

Tactic:
unfold martingalePart predictablePart

Result:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
⊢ (fun n => f n - ∑ i ∈ Finset.range n, μ[f (i + 1) - f i|↑ℱ i]) = fun n =>
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i])

Proof state:
case h
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
n : ℕ
⊢ f n - ∑ i ∈ Finset.range n, μ[f (i + 1) - f i|↑ℱ i] =
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i])

Tactic:
rw [Finset.eq_sum_range_sub f n, ← add_sub, ← Finset.sum_sub_distrib]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem add_div_of_dvd_right {a b c : ℕ} (hca : c ∣ a) : (a + b) / c = a / c + b / c :=
  if h : c = 0 then by simp [h]
  else
    add_div_eq_of_add_mod_lt
      (by
        rw [Nat.mod_eq_zero_of_dvd hca, zero_add]
        exact Nat.mod_lt _ (zero_lt_of_ne_zero h))

Proof state:
a b c : ℕ
hca : c ∣ a
h : ¬c = 0
⊢ b % c < c

Tactic:
exact Nat.mod_lt _ (zero_lt_of_ne_zero h)

Result:
no goals

Proof state:
a b c : ℕ
hca : c ∣ a
h : c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
simp [h]

Result:
no goals

Proof state:
a b c : ℕ
hca : c ∣ a
h : ¬c = 0
⊢ a % c + b % c < c

Tactic:
rw [Nat.mod_eq_zero_of_dvd hca, zero_add]

Result:
a b c : ℕ
hca : c ∣ a
h : ¬c = 0
⊢ b % c < c
-- Mathlib/Data/Finset/Erase.lean
theorem mem_erase_of_ne_of_mem : a ≠ b → a ∈ s → a ∈ erase s b

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ∈ s.erase b

Tactic:
simp only [mem_erase]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ≠ b ∧ a ∈ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ≠ b ∧ a ∈ s

Tactic:
exact And.intro

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem smeval_single (n : ℤ) (r : R) : smeval (Finsupp.single n r) x = r • (x ^ n).val

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
n : ℤ
r : R
⊢ smeval (Finsupp.single n r) x = r • ↑(x ^ n)

Tactic:
simp only [smeval_eq_sum]

Result:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
n : ℤ
r : R
⊢ ((Finsupp.single n r).sum fun n r => r • ↑(x ^ n)) = r • ↑(x ^ n)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
n : ℤ
r : R
⊢ ((Finsupp.single n r).sum fun n r => r • ↑(x ^ n)) = r • ↑(x ^ n)

Tactic:
rw [Finsupp.sum_single_index (zero_smul R (x ^ n).val)]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallyBijective.lean
lemma WEqualsLocallyBijective.mk' [HasWeakSheafify J A] [(forget A).ReflectsIsomorphisms]
    [J.HasSheafCompose (forget A)]
    [∀ (P : Cᵒᵖ ⥤ A), Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)]
    [∀ (P : Cᵒᵖ ⥤ A), Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)] :
    J.WEqualsLocallyBijective A where
  iff {P Q} f

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasWeakSheafify J A
inst✝³ : (forget A).ReflectsIsomorphisms
inst✝² : J.HasSheafCompose (forget A)
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ A), Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)
inst✝ : ∀ (P : Cᵒᵖ ⥤ A), Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ J.W f ↔ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f

Tactic:
rw [W_iff, ← Sheaf.isLocallyBijective_iff_isIso (A := A),
  ← Presheaf.isLocallyInjective_comp_iff J f (CategoryTheory.toSheafify J Q),
  ← Presheaf.isLocallySurjective_comp_iff J f (CategoryTheory.toSheafify J Q),
  CategoryTheory.toSheafify_naturality, Presheaf.comp_isLocallyInjective_iff,
  Presheaf.comp_isLocallySurjective_iff]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem one_sub_inv_two : (1 : ℝ≥0∞) - 2⁻¹ = 2⁻¹

Proof state:
⊢ 1 - 2⁻¹ = 2⁻¹

Tactic:
rw [← one_div, sub_half one_ne_top]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem truncate_liftFun (s : S) : WittVector.truncate n (liftFun f s) = f n s

Proof state:
case h
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff i ((truncate n) (liftFun f s)) = TruncatedWittVector.coeff i ((f n) s)

Tactic:
simp only [liftFun, TruncatedWittVector.coeff_mk, WittVector.truncate_mk']

Result:
case h
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff (Fin.last ↑i) ((f (↑i + 1)) s) = TruncatedWittVector.coeff i ((f n) s)

Proof state:
case h
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff (Fin.castLE ⋯ (Fin.last ↑i)) ((f n) s) = TruncatedWittVector.coeff i ((f n) s)

Tactic:
congr 1 with _

Result:
no goals

Proof state:
case h
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff (Fin.last ↑i) ((f (↑i + 1)) s) = TruncatedWittVector.coeff i ((f n) s)

Tactic:
rw [← f_compat (i + 1) n i.is_lt, RingHom.comp_apply, TruncatedWittVector.coeff_truncate]

Result:
case h
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff (Fin.castLE ⋯ (Fin.last ↑i)) ((f n) s) = TruncatedWittVector.coeff i ((f n) s)

Proof state:
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
s : S
⊢ (truncate n) (liftFun f s) = (f n) s

Tactic:
ext i

Result:
case h
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff i ((truncate n) (liftFun f s)) = TruncatedWittVector.coeff i ((f n) s)
-- Mathlib/Logic/Embedding/Basic.lean
@[simp]
lemma setValue_right_apply_eq {α β} (f : α ↪ β) (a c : α) [∀ a', Decidable (a' = a)]
    [∀ a', Decidable (f a' = f c)] : setValue f a (f c) c = f a

Proof state:
α : Sort u_1
β : Sort u_2
f : α ↪ β
a c : α
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (f a' = f c)
⊢ (f.setValue a (f c)) c = f a

Tactic:
simp [setValue]

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem not_summable_natCast_inv : ¬Summable (fun n => n⁻¹ : ℕ → ℝ)

Proof state:
⊢ ¬Summable fun n => (↑n)⁻¹

Tactic:
have : ¬Summable (fun n => ((n : ℝ) ^ 1)⁻¹ : ℕ → ℝ) :=
  mt (summable_nat_pow_inv (p := 1)).1 (lt_irrefl 1)

Result:
this : ¬Summable fun n => (↑n ^ 1)⁻¹
⊢ ¬Summable fun n => (↑n)⁻¹

Proof state:
this : ¬Summable fun n => (↑n ^ 1)⁻¹
⊢ ¬Summable fun n => (↑n)⁻¹

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default

Proof state:
α : Type u_1
n : Nat
inst✝ : Inhabited α
a : Array α
⊢ a.get! n = (a.get? n).getD default

Tactic:
simp only [get!_eq_getElem?, get?_eq_getElem?]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Expand.lean
theorem expand_one_apply (f : MvPolynomial σ R) : expand 1 f = f

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ (expand 1) f = f

Tactic:
simp only [expand, pow_one, eval₂Hom_eq_bind₂, bind₂_C_left, RingHom.toMonoidHom_eq_coe,
  RingHom.coe_monoidHom_id, AlgHom.coe_mk, RingHom.coe_mk, MonoidHom.id_apply, RingHom.id_apply]

Result:
no goals
-- Mathlib/Algebra/Category/MonCat/Basic.lean
theorem MonoidHom.comp_id_monCat {G : MonCat.{u}} {H : Type u} [Monoid H] (f : G →* H) :
    f.comp (MonCat.Hom.hom (𝟙 G)) = f

Proof state:
G : MonCat
H : Type u
inst✝ : Monoid H
f : ↑G →* H
⊢ f.comp (MonCat.Hom.hom (𝟙 G)) = f

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioi_disjUnion_Iio (a : α) :
    (Ioi a).disjUnion (Iio a) (disjoint_Ioi_Iio a) = ({a} : Finset α)ᶜ

Proof state:
case h
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
a a✝ : α
⊢ a✝ ∈ (Ioi a).disjUnion (Iio a) ⋯ ↔ a✝ ∈ {a}ᶜ

Tactic:
simp [eq_comm]

Result:
no goals

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ (Ioi a).disjUnion (Iio a) ⋯ = {a}ᶜ

Tactic:
ext

Result:
case h
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
a a✝ : α
⊢ a✝ ∈ (Ioi a).disjUnion (Iio a) ⋯ ↔ a✝ ∈ {a}ᶜ
-- Mathlib/LinearAlgebra/BilinearForm/Properties.lean
theorem nondegenerate_congr_iff {B : BilinForm R M} (e : M ≃ₗ[R] M') :
    (congr e B).Nondegenerate ↔ B.Nondegenerate :=
  ⟨fun h => by
    convert h.congr e.symm
    rw [congr_congr, e.self_trans_symm, congr_refl, LinearEquiv.refl_apply], Nondegenerate.congr e⟩

Proof state:
case h.e'_6
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B : BilinForm R M
e : M ≃ₗ[R] M'
h : ((congr e) B).Nondegenerate
⊢ B = (congr e.symm) ((congr e) B)

Tactic:
rw [congr_congr, e.self_trans_symm, congr_refl, LinearEquiv.refl_apply]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B : BilinForm R M
e : M ≃ₗ[R] M'
h : ((congr e) B).Nondegenerate
⊢ B.Nondegenerate

Tactic:
convert h.congr e.symm

Result:
case h.e'_6
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B : BilinForm R M
e : M ≃ₗ[R] M'
h : ((congr e) B).Nondegenerate
⊢ B = (congr e.symm) ((congr e) B)
-- Mathlib/Algebra/GroupWithZero/Conj.lean
@[simp] lemma isConj_iff₀ : IsConj a b ↔ ∃ c : α, c ≠ 0 ∧ c * a * c⁻¹ = b

Proof state:
α : Type u_1
inst✝ : GroupWithZero α
a b : α
⊢ (∃ x, x ≠ 0 ∧ SemiconjBy x a b) ↔ ∃ c, c ≠ 0 ∧ c * a * c⁻¹ = b

Tactic:
congr! 2 with c

Result:
case a.h.e'_2.h.a
α : Type u_1
inst✝ : GroupWithZero α
a b c : α
⊢ c ≠ 0 ∧ SemiconjBy c a b ↔ c ≠ 0 ∧ c * a * c⁻¹ = b