harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/Mul.lean
theorem mul_diagonal [Fintype n] [DecidableEq n] (d : n → α) (M : Matrix m n α) (i j) :
    (M * diagonal d) i j = M i j * d j

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d : n → α
M : Matrix m n α
i : m
j : n
⊢ (M * (diagonal d)ᵀ) i j = M i j * d j

Tactic:
apply dotProduct_diagonal

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d : n → α
M : Matrix m n α
i : m
j : n
⊢ (M * diagonal d) i j = M i j * d j

Tactic:
rw [← diagonal_transpose]

Result:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d : n → α
M : Matrix m n α
i : m
j : n
⊢ (M * (diagonal d)ᵀ) i j = M i j * d j
-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem pullbackRestrictIsoRestrict_inv_fst {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) :
    (pullbackRestrictIsoRestrict f U).inv ≫ pullback.fst f _ = (f ⁻¹ᵁ U).ι

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (IsOpenImmersion.isoOfRangeEq (pullback.fst f U.ι) (f ⁻¹ᵁ U).ι ⋯).inv ≫ pullback.fst f U.ι = (f ⁻¹ᵁ U).ι

Tactic:
simp

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (pullbackRestrictIsoRestrict f U).inv ≫ pullback.fst f U.ι = (f ⁻¹ᵁ U).ι

Tactic:
delta pullbackRestrictIsoRestrict

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (IsOpenImmersion.isoOfRangeEq (pullback.fst f U.ι) (f ⁻¹ᵁ U).ι ⋯).inv ≫ pullback.fst f U.ι = (f ⁻¹ᵁ U).ι
-- Mathlib/Probability/ConditionalProbability.lean
lemma cond_eq_zero_of_meas_eq_zero (hμs : μ s = 0) : μ[|s] = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hμs : μ s = 0
⊢ μ[|s] = 0

Tactic:
simp [hμs]

Result:
no goals
-- Mathlib/Analysis/Complex/Circle.lean
lemma coe_inv_eq_conj (z : Circle) : ↑z⁻¹ = conj (z : ℂ)

Proof state:
z : Circle
⊢ ↑z⁻¹ = (starRingEnd ℂ) ↑z

Tactic:
rw [coe_inv, inv_def, normSq_coe, inv_one, ofReal_one, mul_one]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_image (f : ZFSet → ZFSet) [Definable₁ f] (x : ZFSet) :
    (image f x).toSet = f '' x.toSet

Proof state:
case h
f : ZFSet.{u_1} → ZFSet.{u_1}
inst✝ : Definable₁ f
x x✝ : ZFSet.{u_1}
⊢ x✝ ∈ (image f x).toSet ↔ x✝ ∈ f '' x.toSet

Tactic:
simp

Result:
no goals

Proof state:
f : ZFSet.{u_1} → ZFSet.{u_1}
inst✝ : Definable₁ f
x : ZFSet.{u_1}
⊢ (image f x).toSet = f '' x.toSet

Tactic:
ext

Result:
case h
f : ZFSet.{u_1} → ZFSet.{u_1}
inst✝ : Definable₁ f
x x✝ : ZFSet.{u_1}
⊢ x✝ ∈ (image f x).toSet ↔ x✝ ∈ f '' x.toSet
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem nonnegg_pos_neg {c d} {a b : ℕ} : Nonnegg c d a (-b) ↔ SqLe b c a d

Proof state:
c d a b : ℕ
⊢ Nonnegg c d (↑a) (-↑b) ↔ SqLe b c a d

Tactic:
rw [nonnegg_comm]

Result:
c d a b : ℕ
⊢ Nonnegg d c (-↑b) ↑a ↔ SqLe b c a d

Proof state:
c d a b : ℕ
⊢ Nonnegg d c (-↑b) ↑a ↔ SqLe b c a d

Tactic:
exact nonnegg_neg_pos

Result:
no goals
-- Mathlib/Topology/Sheaves/LocalPredicate.lean
theorem stalkToFiber_germ (P : LocalPredicate T) (U : Opens X) (x : X) (hx : x ∈ U) (f) :
    stalkToFiber P x ((subsheafToTypes P).presheaf.germ U x hx f) = f.1 ⟨x, hx⟩

Proof state:
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
U : Opens ↑X
x : ↑X
hx : x ∈ U
f : (subsheafToTypes P).presheaf.obj (op U)
⊢ stalkToFiber P x ((subsheafToTypes P).presheaf.germ U x hx f) = ↑f ⟨x, hx⟩

Tactic:
simp [Presheaf.germ, stalkToFiber]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem coe_xor_iff (a b : Bool) : xor a b ↔ Xor' (a = true) (b = true)

Proof state:
a b : Bool
⊢ (a ^^ b) = true ↔ Xor' (a = true) (b = true)

Tactic:
cases a <;> cases b <;> decide

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem AnalyticAt.comp_of_eq' {g : F → G} {f : E → F} {y : F} {x : E} (hg : AnalyticAt 𝕜 g y)
    (hf : AnalyticAt 𝕜 f x) (hy : f x = y) : AnalyticAt 𝕜 (fun z ↦ g (f z)) x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
y : F
x : E
hg : AnalyticAt 𝕜 g y
hf : AnalyticAt 𝕜 f x
hy : f x = y
⊢ AnalyticAt 𝕜 (fun z => g (f z)) x

Tactic:
apply hg.comp_of_eq hf hy

Result:
no goals
-- Mathlib/Algebra/Ring/CharZero.lean
lemma charZero (ϕ : R →+* S) [CharZero S] : CharZero R where
  cast_injective a b h := CharZero.cast_injective (R := S) <| by
    rw [← map_natCast ϕ, ← map_natCast ϕ, h]

Proof state:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
ϕ : R →+* S
inst✝ : CharZero S
a b : ℕ
h : ↑a = ↑b
⊢ ↑a = ↑b

Tactic:
rw [← map_natCast ϕ, ← map_natCast ϕ, h]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma supClosed_univ : SupClosed (univ : Set α)

Proof state:
α : Type u_3
inst✝ : SemilatticeSup α
⊢ SupClosed univ

Tactic:
simp [SupClosed]

Result:
no goals
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.qr₁ (a b : ℕ) (r : ℤ) (ha : a % 4 = 1) (hb : b % 2 = 1)
    (hr : jacobiSymNat b a = r) : jacobiSymNat a b = r

Proof state:
a b : ℕ
r : ℤ
ha : a % 4 = 1
hb : b % 2 = 1
hr : jacobiSymNat b a = r
⊢ jacobiSymNat a b = r

Tactic:
rwa [jacobiSymNat, jacobiSym.quadratic_reciprocity_one_mod_four ha (Nat.odd_iff.mpr hb)]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem prod_nhds_le_of_disjoint_cocompact {f : Filter X} (y : Y)
    (hf : Disjoint f (Filter.cocompact X)) :
    f ×ˢ 𝓝 y ≤ 𝓝ˢ (Set.univ ×ˢ {y})

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Filter X
y : Y
hf : Disjoint f (cocompact X)
⊢ f ×ˢ 𝓝 y ≤ 𝓝ˢ (univ ×ˢ {y})

Tactic:
simpa using prod_nhdsSet_le_of_disjoint_cocompact isCompact_singleton hf

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/BinaryProducts.lean
theorem PreservesLimitPair.iso_inv_snd :
    (PreservesLimitPair.iso G X Y).inv ≫ G.map prod.snd = prod.snd

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ (iso G X Y).inv ≫ G.map prod.snd = prod.snd

Tactic:
rw [← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y), ← Category.assoc, Iso.hom_inv_id]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.snd = (iso G X Y).hom ≫ prod.snd

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.snd = (iso G X Y).hom ≫ prod.snd

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
theorem coe_basisOneI : ⇑basisOneI = ![1, I] :=
  funext fun i =>
    Basis.apply_eq_iff.mpr <|
      Finsupp.ext fun j => by
        fin_cases i <;> fin_cases j <;>
          -- Porting note: removed `only`, consider squeezing again
          simp [coe_basisOneI_repr, Finsupp.single_eq_of_ne, Matrix.cons_val_zero,
            Matrix.cons_val_one, Matrix.head_cons, Fin.one_eq_zero_iff, Ne, not_false_iff, I_re,
            Nat.succ_succ_ne_one, one_im, I_im, one_re, Finsupp.single_eq_same, Fin.zero_eq_one_iff]

Proof state:
i j : Fin 2
⊢ (basisOneI.repr (![1, I] i)) j = (Finsupp.single i 1) j

Tactic:
fin_cases i <;> fin_cases j <;>
  simp [coe_basisOneI_repr, Finsupp.single_eq_of_ne, Matrix.cons_val_zero,
    Matrix.cons_val_one, Matrix.head_cons, Fin.one_eq_zero_iff, Ne, not_false_iff, I_re,
    Nat.succ_succ_ne_one, one_im, I_im, one_re, Finsupp.single_eq_same, Fin.zero_eq_one_iff]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem measurableSet_preimage (hf : MeasurableEmbedding f) {s : Set β} :
    MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set β
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)

Tactic:
rw [← image_preimage_eq_inter_range, hf.measurableSet_image]

Result:
no goals
-- Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean
theorem Module.rank_linearMap_self :
    Module.rank S (M →ₗ[R] S) = lift.{u'} (Module.rank R M)

Proof state:
R : Type u
S : Type u'
M : Type v
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : StrongRankCondition R
inst✝² : StrongRankCondition S
inst✝¹ : Module R S
inst✝ : SMulCommClass R S S
⊢ Module.rank S (M →ₗ[R] S) = lift.{u', v} (Module.rank R M)

Tactic:
rw [rank_linearMap, rank_self, lift_one, mul_one]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem edist_eq_of_L2 (x y : PiLp 2 β) :
    edist x y = (∑ i, edist (x i) (y i) ^ 2) ^ (1 / 2 : ℝ)

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ edist x y = (∑ i : ι, edist (x i) (y i) ^ 2) ^ (1 / 2)

Tactic:
simp [PiLp.edist_eq_sum]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_range {g : β → α} {f : ι → β} : ⨆ b ∈ range f, g b = ⨆ i, g (f i)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
g : β → α
f : ι → β
⊢ ⨆ b ∈ range f, g b = ⨆ i, g (f i)

Tactic:
rw [← iSup_subtype'', iSup_range']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_range' {start size step} :
     (range' start size step).toList = List.range' start size step

Proof state:
start size step : Nat
⊢ (range' start size step).toList = List.range' start size step

Tactic:
apply List.ext_getElem <;> simp [range']

Result:
no goals
-- Mathlib/GroupTheory/Subsemigroup/Center.lean
theorem mem_center_iff {z : M} : z ∈ center M ↔ ∀ g, g * z = z * g

Proof state:
M : Type u_1
inst✝ : Semigroup M
z : M
⊢ z ∈ center M ↔ ∀ (g : M), g * z = z * g

Tactic:
rw [← Semigroup.mem_center_iff]

Result:
M : Type u_1
inst✝ : Semigroup M
z : M
⊢ z ∈ center M ↔ z ∈ Set.center M

Proof state:
M : Type u_1
inst✝ : Semigroup M
z : M
⊢ z ∈ center M ↔ z ∈ Set.center M

Tactic:
exact Iff.rfl

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem map_neg (f : M →SL[σ₁₂] M₂) (x : M) : f (-x) = -f x

Proof state:
R : Type u_1
inst✝⁷ : Ring R
R₂ : Type u_2
inst✝⁶ : Ring R₂
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup M
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →SL[σ₁₂] M₂
x : M
⊢ f (-x) = -f x

Tactic:
exact map_neg f x

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
theorem isMatching_iff_forall_degree [∀ v, Fintype (M.neighborSet v)] :
    M.IsMatching ↔ ∀ v : V, v ∈ M.verts → M.degree v = 1

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : (v : V) → Fintype ↑(M.neighborSet v)
⊢ M.IsMatching ↔ ∀ v ∈ M.verts, M.degree v = 1

Tactic:
simp only [degree_eq_one_iff_unique_adj, IsMatching]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insertManyIfNewUnit_empty_list
    {l : List α} {k : α} :
    get! (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l) k = ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
l : List α
k : α
⊢ get! (insertManyIfNewUnit empty l).val k = ()

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem ae_eq_set {s t : Set α} : s =ᵐ[μ] t ↔ μ (s \ t) = 0 ∧ μ (t \ s) = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ s =ᶠ[ae μ] t ↔ μ (s \ t) = 0 ∧ μ (t \ s) = 0

Tactic:
simp [eventuallyLE_antisymm_iff, ae_le_set]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_insert_le (s : Set α) (x : α) : (insert x s).encard ≤ s.encard + 1

Proof state:
α : Type u_1
s : Set α
x : α
⊢ (s ∪ {x}).encard ≤ s.encard + {x}.encard

Tactic:
apply encard_union_le

Result:
no goals

Proof state:
α : Type u_1
s : Set α
x : α
⊢ (insert x s).encard ≤ s.encard + 1

Tactic:
rw [← union_singleton, ← encard_singleton x]

Result:
α : Type u_1
s : Set α
x : α
⊢ (s ∪ {x}).encard ≤ s.encard + {x}.encard
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.trans_sbtw_left [NoZeroSMulDivisors R V] {w x y z : P} (h₁ : Wbtw R w y z)
    (h₂ : Sbtw R w x y) : Sbtw R w x z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x y z : P
h₁ : Wbtw R w y z
h₂ : Sbtw R w x y
⊢ Sbtw R w x z

Tactic:
refine ⟨h₁.trans_left h₂.wbtw, h₂.ne_left, ?_⟩

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x y z : P
h₁ : Wbtw R w y z
h₂ : Sbtw R w x y
⊢ x ≠ z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x y : P
h₂ : Sbtw R w x y
h₁ : Wbtw R w y x
⊢ False

Tactic:
exact h₂.right_ne ((wbtw_swap_right_iff R w).1 ⟨h₁, h₂.wbtw⟩)

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x y z : P
h₁ : Wbtw R w y z
h₂ : Sbtw R w x y
⊢ x ≠ z

Tactic:
rintro rfl

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x y : P
h₂ : Sbtw R w x y
h₁ : Wbtw R w y x
⊢ False
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem associator_inv_naturality {X Y Z X' Y' Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') :
    (f ⊗ g ⊗ h) ≫ (α_ X' Y' Z').inv = (α_ X Y Z).inv ≫ ((f ⊗ g) ⊗ h)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z X' Y' Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ (f ⊗ g ⊗ h) ≫ (α_ X' Y' Z').inv = (α_ X Y Z).inv ≫ ((f ⊗ g) ⊗ h)

Tactic:
simp [tensorHom_def]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem Gamma_ne_zero_of_re_pos {s : ℂ} (hs : 0 < re s) : Gamma s ≠ 0

Proof state:
s : ℂ
hs : 0 < s.re
⊢ Gamma s ≠ 0

Tactic:
refine Gamma_ne_zero fun m => ?_

Result:
s : ℂ
hs : 0 < s.re
m : ℕ
⊢ s ≠ -↑m

Proof state:
s : ℂ
m : ℕ
hs : s = -↑m
⊢ s.re ≤ 0

Tactic:
simpa only [hs, neg_re, ← ofReal_natCast, ofReal_re, neg_nonpos] using Nat.cast_nonneg _

Result:
no goals

Proof state:
s : ℂ
hs : 0 < s.re
m : ℕ
⊢ s ≠ -↑m

Tactic:
contrapose! hs

Result:
s : ℂ
m : ℕ
hs : s = -↑m
⊢ s.re ≤ 0
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem induct (motive : ℤ → Prop)
    (zero : motive 0)
    (one : motive 1)
    (add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2))
    (neg_add_one : ∀ (n : ℕ), motive (-↑n) → motive (-↑n + 1) → motive (-↑n - 1)) :
    ∀ (a : ℤ), motive a :=
  T.induct motive zero one add_two fun n hn hnm => by
    simpa only [Int.negSucc_eq, neg_add] using neg_add_one n hn hnm

Proof state:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)
neg_add_one : ∀ (n : ℕ), motive (-↑n) → motive (-↑n + 1) → motive (-↑n - 1)
n : ℕ
hn : motive (-↑n)
hnm : motive (-↑n + 1)
⊢ motive (Int.negSucc n)

Tactic:
simpa only [Int.negSucc_eq, neg_add] using neg_add_one n hn hnm

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem first_num_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
    g.nums 1 = gp.b * g.h + gp.a

Proof state:
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.nums 1 = gp.b * g.h + gp.a

Tactic:
simp [num_eq_conts_a, first_cont_eq zeroth_s_eq]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
theorem exists_isIdempotentElem_eq_of_ker_isNilpotent (h : ∀ x ∈ RingHom.ker f, IsNilpotent x)
    (e : S) (he : e ∈ f.range) (he' : IsIdempotentElem e) :
    ∃ e' : R, IsIdempotentElem e' ∧ f e' = e

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : S
he : e ∈ f.range
he' : IsIdempotentElem e
⊢ e * f 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : S
he : e ∈ f.range
he' : IsIdempotentElem e
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = e

Tactic:
simpa using exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent f h e he he' 0 .zero (by simp)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) :
    get? (insertMany m l).1 k' = v

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
⊢ get? (insertMany m l).val k' = some v

Tactic:
simp_to_model [Const.insertMany] using List.getValue?_insertListConst_of_mem

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem inv_sub_inv {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = (b - a) / (a * b)

Proof state:
K : Type u_1
inst✝ : Field K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)

Tactic:
rw [inv_eq_one_div, inv_eq_one_div, div_sub_div _ _ ha hb, one_mul, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n

Proof state:
x : Int
n : Nat
y : Int
this : (x.bmod n + y).bmod n = (x.bmod n + y + ↑n * x.bdiv n).bmod n
⊢ (x.bmod n + y).bmod n = (x + y).bmod n

Tactic:
rwa [Int.add_right_comm, bmod_add_bdiv] at this

Result:
no goals

Proof state:
x : Int
n : Nat
y : Int
⊢ (x.bmod n + y).bmod n = (x + y).bmod n

Tactic:
have := (@bmod_add_mul_cancel (Int.bmod x n + y) n (bdiv x n)).symm

Result:
x : Int
n : Nat
y : Int
this : (x.bmod n + y).bmod n = (x.bmod n + y + ↑n * x.bdiv n).bmod n
⊢ (x.bmod n + y).bmod n = (x + y).bmod n
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α}
    (hl : DistinctKeys l) (h : Perm l l') : getKey? a l = getKey? a l'

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
hl : DistinctKeys l
h : l.Perm l'
⊢ getKey? a l = getKey? a l'

Tactic:
rw [getKey?_eq_getEntry?, getKey?_eq_getEntry?, getEntry?_of_perm hl h]

Result:
no goals
-- Mathlib/Probability/Independence/Conditional.lean
lemma iCondIndep_iff_iCondIndepSets (m : ι → MeasurableSpace Ω)
    (μ : @Measure Ω mΩ) [IsFiniteMeasure μ] :
    iCondIndep m' hm' m μ ↔ iCondIndepSets m' hm' (fun x ↦ {s | MeasurableSet[m x] s}) μ

Proof state:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndep m' hm' m μ ↔ iCondIndepSets m' hm' (fun x => {s | MeasurableSet s}) μ

Tactic:
simp only [iCondIndep, iCondIndepSets, Kernel.iIndep]

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
theorem hasSum_ofReal {f : α → ℝ} {x : ℝ} : HasSum (fun x => (f x : 𝕜)) x ↔ HasSum f x :=
  ⟨fun h => by simpa only [RCLike.reCLM_apply, RCLike.ofReal_re] using reCLM.hasSum h,
    ofRealCLM.hasSum⟩

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
f : α → ℝ
x : ℝ
h : HasSum (fun x => ↑(f x)) ↑x
⊢ HasSum f x

Tactic:
simpa only [RCLike.reCLM_apply, RCLike.ofReal_re] using reCLM.hasSum h

Result:
no goals
-- Mathlib/NumberTheory/SumPrimeReciprocals.lean
theorem Nat.Primes.not_summable_one_div : ¬ Summable (fun p : Nat.Primes ↦ (1 / p : ℝ))

Proof state:
⊢ ¬Summable fun p => 1 / ↑↑p

Tactic:
convert summable_subtype_iff_indicator.mp.mt not_summable_one_div_on_primes

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma lift_fst :
    (Cochain.ofHom (lift φ α β eq)).comp (fst φ).1 (zero_add 1) = α.1

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
⊢ (Cochain.ofHom (lift φ α β eq)).comp ↑(fst φ) ⋯ = ↑α

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Goursat.lean
@[to_additive (attr := simp)]
lemma mem_goursatFst {g : G} : g ∈ I.goursatFst ↔ (g, 1) ∈ I

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
g : G
⊢ g ∈ I.goursatFst ↔ (g, 1) ∈ I

Tactic:
simp [goursatFst]

Result:
no goals
-- Mathlib/Algebra/Lie/Free.lean
theorem Rel.subLeft (a : lib R X) {b c : lib R X} (h : Rel R X b c) : Rel R X (a - b) (a - c)

Proof state:
R : Type u
X : Type v
inst✝ : CommRing R
a b c : lib R X
h : Rel R X b c
⊢ Rel R X (a - b) (a - c)

Tactic:
simpa only [sub_eq_add_neg] using h.neg.addLeft a

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
theorem Complex.volume_ball (a : ℂ) (r : ℝ) :
    volume (Metric.ball a r) = .ofReal r ^ 2 * NNReal.pi

Proof state:
a : ℂ
r : ℝ
⊢ volume (Metric.ball a r) = ENNReal.ofReal r ^ 2 * ↑NNReal.pi

Tactic:
simp [InnerProductSpace.volume_ball_of_dim_even (k := 1) (by simp) a,
  ← NNReal.coe_real_pi, ofReal_coe_nnreal]

Result:
no goals

Proof state:
a : ℂ
r : ℝ
⊢ Module.finrank ℝ ℂ = 2 * 1

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_le_card [Finite G] : orderOf x ≤ Nat.card G

Proof state:
G : Type u_1
inst✝¹ : Monoid G
x : G
inst✝ : Finite G
⊢ orderOf x ≤ Nat.card G

Tactic:
obtain ⟨⟩ := nonempty_fintype G

Result:
case intro
G : Type u_1
inst✝¹ : Monoid G
x : G
inst✝ : Finite G
val✝ : Fintype G
⊢ orderOf x ≤ Nat.card G

Proof state:
case intro
G : Type u_1
inst✝¹ : Monoid G
x : G
inst✝ : Finite G
val✝ : Fintype G
⊢ orderOf x ≤ Nat.card G

Tactic:
simpa using orderOf_le_card_univ

Result:
no goals
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem liftAux_self_apply [ExpChar L p] [PerfectRing L p] (x : L) : liftAux i i p x = x

Proof state:
K : Type u_1
L : Type u_2
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
i : K →+* L
p : ℕ
inst✝² : IsPRadical i p
inst✝¹ : ExpChar L p
inst✝ : PerfectRing L p
x : L
⊢ liftAux i i p x = x

Tactic:
rw [liftAux, Classical.choose_spec (lift_aux i p x), ← iterateFrobenius_def,
  ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
theorem npowRec_succ : npowRec (n + 1) a = a * npowRec n a

Proof state:
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
⊢ npowRec (n + 1) a = a * npowRec n a

Tactic:
rw [Nat.add_comm, npowRec_add 1 n hn a ha, npowRec, npowRec, ha]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem coe_units_iff {ζ : Mˣ} : IsPrimitiveRoot (ζ : M) k ↔ IsPrimitiveRoot ζ k

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k

Tactic:
simp only [iff_def, Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
@[simp]
lemma map_j : (W.map φ).j = φ W.j

Proof state:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ (W.map φ).j = φ W.j

Tactic:
rw [j, coe_inv_map_Δ', map_c₄, j, map_mul, map_pow]

Result:
no goals