harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
lemma twoCocycles_ρ_map_inv_sub_map_inv (f : twoCocycles A) (g : G) :
    A.ρ g (f (g⁻¹, g)) - f (g, g⁻¹)
      = f (1, 1) - f (g, 1)

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(twoCocycles A)
g : G
this : f (g * g⁻¹, g) + f (g, g⁻¹) = (A.ρ g) (f (g⁻¹, g)) + f (g, g⁻¹ * g)
⊢ (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
simp only [mul_inv_cancel, inv_mul_cancel, twoCocycles_map_one_fst _ g]
  at this

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(twoCocycles A)
g : G
this : f (1, 1) + f (g, g⁻¹) = (A.ρ g) (f (g⁻¹, g)) + f (g, 1)
⊢ (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(twoCocycles A)
g : G
this : f (1, 1) + f (g, g⁻¹) = (A.ρ g) (f (g⁻¹, g)) + f (g, 1)
⊢ (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
exact sub_eq_sub_iff_add_eq_add.2 this.symm

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(twoCocycles A)
g : G
⊢ (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
have := (mem_twoCocycles_iff f).1 f.2 g g⁻¹ g

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(twoCocycles A)
g : G
this : f (g * g⁻¹, g) + f (g, g⁻¹) = (A.ρ g) (f (g⁻¹, g)) + f (g, g⁻¹ * g)
⊢ (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
-- Mathlib/Algebra/GroupWithZero/Divisibility.lean
theorem dvd_antisymm : a ∣ b → b ∣ a → a = b

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
a : α
inst✝ : Subsingleton αˣ
c d : α
hcd : a = a * c * d
⊢ a = a * c

Tactic:
rw [mul_assoc, eq_comm, mul_right_eq_self₀, mul_eq_one] at hcd

Result:
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
a : α
inst✝ : Subsingleton αˣ
c d : α
hcd : c = 1 ∧ d = 1 ∨ a = 0
⊢ a = a * c

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
a : α
inst✝ : Subsingleton αˣ
c d : α
hcd : c = 1 ∧ d = 1 ∨ a = 0
⊢ a = a * c

Tactic:
obtain ⟨rfl, -⟩ | rfl := hcd <;> simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
a b : α
inst✝ : Subsingleton αˣ
⊢ a ∣ b → b ∣ a → a = b

Tactic:
rintro ⟨c, rfl⟩ ⟨d, hcd⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
a : α
inst✝ : Subsingleton αˣ
c d : α
hcd : a = a * c * d
⊢ a = a * c
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedDerivWithin_zero : iteratedDerivWithin 0 f s = f

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin 0 f s x = f x

Tactic:
simp [iteratedDerivWithin]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
⊢ iteratedDerivWithin 0 f s = f

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin 0 f s x = f x
-- Mathlib/Algebra/Category/AlgebraCat/Basic.lean
lemma id_apply (A : AlgebraCat.{v} R) (a : A) :
    (𝟙 A : A ⟶ A) a = a

Proof state:
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
a : ↑A
⊢ (ConcreteCategory.hom (𝟙 A)) a = a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_rel {l : Array α} {f g : β → α → β} {a b : β} (r : β → β → Prop)
    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
    r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b)

Proof state:
α : Type u_1
β : Type u_2
f g : β → α → β
a b : β
r : β → β → Prop
h : r a b
l : List α
h' : ∀ (a : α), a ∈ { toList := l } → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)

Tactic:
simpa using h'

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f g : β → α → β
a b : β
r : β → β → Prop
h : r a b
h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ r (foldl (fun acc a => f acc a) a l) (foldl (fun acc a => g acc a) b l)

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f g : β → α → β
a b : β
r : β → β → Prop
h : r a b
l : List α
h' : ∀ (a : α), a ∈ { toList := l } → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ r (foldl (fun acc a => f acc a) a { toList := l }) (foldl (fun acc a => g acc a) b { toList := l })

Proof state:
case mk
α : Type u_1
β : Type u_2
f g : β → α → β
a b : β
r : β → β → Prop
h : r a b
l : List α
h' : ∀ (a : α), a ∈ { toList := l } → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ r (foldl (fun acc a => f acc a) a { toList := l }) (foldl (fun acc a => g acc a) b { toList := l })

Tactic:
simpa using List.foldl_rel r h (by simpa using h')

Result:
no goals
-- Mathlib/MeasureTheory/Group/Action.lean
theorem isLocallyFiniteMeasure_of_smulInvariant (hU : IsOpen U) (hne : U.Nonempty) (hμU : μ U ≠ ∞) :
    IsLocallyFiniteMeasure μ :=
  ⟨fun x =>
    let ⟨g, hg⟩ := hU.exists_smul_mem G x hne
    ⟨(g • ·) ⁻¹' U, (hU.preimage (continuous_id.const_smul _)).mem_nhds hg,
      Ne.lt_top <| by rwa [measure_preimage_smul]⟩⟩

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
μ : Measure α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousConstSMul G α
inst✝ : MulAction.IsMinimal G α
U : Set α
hU : IsOpen U
hne : U.Nonempty
hμU : μ U ≠ ⊤
x : α
g : G
hg : g • x ∈ U
⊢ μ ((fun x => g • x) ⁻¹' U) ≠ ⊤

Tactic:
rwa [measure_preimage_smul]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_eq_Ico_same_iff : Ioo a b = Ico a b ↔ ¬a < b where
  mp h

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h : Ioo a b = Ico a b
⊢ ¬a < b

Tactic:
simpa using Set.ext_iff.mp h a

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a < b
⊢ Ioo a b = Ico a b

Tactic:
rw [Ioo_eq_empty h, Ico_eq_empty h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_eq_iff_eq_or_eq_neg {θ ψ : Angle} : cos θ = cos ψ ↔ θ = ψ ∨ θ = -ψ

Proof state:
θ ψ : Angle
⊢ θ.cos = ψ.cos ↔ θ = ψ ∨ θ = -ψ

Tactic:
induction ψ using Real.Angle.induction_on

Result:
case h
θ : Angle
x✝ : ℝ
⊢ θ.cos = (↑x✝).cos ↔ θ = ↑x✝ ∨ θ = -↑x✝

Proof state:
case h
θ : Angle
x✝ : ℝ
⊢ θ.cos = (↑x✝).cos ↔ θ = ↑x✝ ∨ θ = -↑x✝

Tactic:
exact cos_eq_real_cos_iff_eq_or_eq_neg

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem MeasurableSet.biInter {f : β → Set α} {s : Set β} (hs : s.Countable)
    (h : ∀ b ∈ s, MeasurableSet (f b)) : MeasurableSet (⋂ b ∈ s, f b) :=
  .of_compl <| by rw [compl_iInter₂]; exact .biUnion hs fun b hb => (h b hb).compl

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ i ∈ s, (f i)ᶜ)

Tactic:
exact .biUnion hs fun b hb => (h b hb).compl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋂ b ∈ s, f b)ᶜ

Tactic:
rw [compl_iInter₂]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ i ∈ s, (f i)ᶜ)
-- Mathlib/RingTheory/Int/Basic.lean
theorem span_natAbs (a : ℤ) : Ideal.span ({(a.natAbs : ℤ)} : Set ℤ) = Ideal.span {a}

Proof state:
a : ℤ
⊢ Associated (↑a.natAbs) a

Tactic:
exact (associated_natAbs _).symm

Result:
no goals

Proof state:
a : ℤ
⊢ Ideal.span {↑a.natAbs} = Ideal.span {a}

Tactic:
rw [Ideal.span_singleton_eq_span_singleton]

Result:
a : ℤ
⊢ Associated (↑a.natAbs) a
-- Mathlib/Analysis/Complex/Basic.lean
lemma le_of_eq_sum_of_eq_sum_norm {ι : Type*} {a b : ℝ} (f : ι → ℂ) (s : Finset ι) (ha₀ : 0 ≤ a)
    (ha : a = ∑ i ∈ s, f i) (hb : b = ∑ i ∈ s, (‖f i‖ : ℂ)) : a ≤ b

Proof state:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : ↑b = ∑ i ∈ s, ↑‖f i‖
⊢ a ≤ b

Tactic:
norm_cast at hb

Result:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ a ≤ b

Proof state:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ a ≤ b

Tactic:
rw [← Complex.norm_of_nonneg ha₀, ha, hb]

Result:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖

Proof state:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖

Tactic:
exact norm_sum_le s f

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Reflective.lean
theorem unitCompPartialBijectiveAux_symm_apply [Reflective i] {A : C} {B : D}
    (f : i.obj ((reflector i).obj A) ⟶ i.obj B) :
    (unitCompPartialBijectiveAux _ _).symm f = (reflectorAdjunction i).unit.app A ≫ f

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
A : C
B : D
f : i.obj ((reflector i).obj A) ⟶ i.obj B
⊢ (unitCompPartialBijectiveAux A B).symm f = (reflectorAdjunction i).unit.app A ≫ f

Tactic:
simp [unitCompPartialBijectiveAux, Adjunction.homEquiv_unit]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem eq_replicate_length {a : α} : ∀ {l : List α}, l = replicate l.length a ↔ ∀ b ∈ l, b = a
  | [] => by simp
  | (b :: l) => by simp [eq_replicate_length, replicate_succ]

Proof state:
α : Type u
a : α
⊢ [] = replicate [].length a ↔ ∀ (b : α), b ∈ [] → b = a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
a b : α
l : List α
⊢ b :: l = replicate (b :: l).length a ↔ ∀ (b_1 : α), b_1 ∈ b :: l → b_1 = a

Tactic:
simp [eq_replicate_length, replicate_succ]

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
/-- Dense sets have small difference constant. -/
@[to_additive subConst_le_inv_dens "Dense sets have small difference constant."]
lemma divConst_le_inv_dens : δₘ[A, B] ≤ A.dens⁻¹

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ δₘ[A, B] ≤ A.dens⁻¹

Tactic:
rw [dens, inv_div, divConst]

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ ↑(#(A / B)) / ↑(#A) ≤ ↑(Fintype.card G) / ↑(#A)

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ ↑(#(A / B)) / ↑(#A) ≤ ↑(Fintype.card G) / ↑(#A)

Tactic:
gcongr

Result:
case hab.h
G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ #(A / B) ≤ Fintype.card G

Proof state:
case hab.h
G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ #(A / B) ≤ Fintype.card G

Tactic:
exact card_le_univ _

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Pi.lean
@[simp]
lemma piScalarRight_apply (x : N ⊗[R] (ι → R)) :
    piScalarRight R S N ι x = piScalarRightHom R S N ι x

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N ⊗[R] (ι → R)
⊢ (piScalarRight R S N ι) x = (piScalarRightHom R S N ι) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem cRk_mono (M : Matroid α) : Monotone M.cRk

Proof state:
α : Type u
M : Matroid α
⊢ ∀ ⦃a b : Set α⦄, a ⊆ b → ∀ ⦃I : Set α⦄, M.IsBasis' I a → #↑I ≤ M.cRk b

Tactic:
intro X Y hXY I hIX

Result:
α : Type u
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hIX : M.IsBasis' I X
⊢ #↑I ≤ M.cRk Y

Proof state:
α : Type u
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hIX : M.IsBasis' I X
⊢ #↑I ≤ M.cRk Y

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hIX.indep.subset_isBasis'_of_subset (hIX.subset.trans hXY)

Result:
case intro.intro
α : Type u
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hIX : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ #↑I ≤ M.cRk Y

Proof state:
case intro.intro
α : Type u
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hIX : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ #↑I ≤ M.cRk Y

Tactic:
exact (mk_le_mk_of_subset hIJ).trans hJ.cardinalMk_le_cRk

Result:
no goals

Proof state:
α : Type u
M : Matroid α
⊢ Monotone M.cRk

Tactic:
simp only [Monotone, le_eq_subset, cRk_le_iff]

Result:
α : Type u
M : Matroid α
⊢ ∀ ⦃a b : Set α⦄, a ⊆ b → ∀ ⦃I : Set α⦄, M.IsBasis' I a → #↑I ≤ M.cRk b
-- Mathlib/RingTheory/Ideal/Quotient/Basic.lean
theorem map_pi [I.IsTwoSided] {ι : Type*} [Finite ι] {ι' : Type w} (x : ι → R) (hi : ∀ i, x i ∈ I)
    (f : (ι → R) →ₗ[R] ι' → R) (i : ι') : f x i ∈ I

Proof state:
R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
⊢ f x i ∈ I

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ f x i ∈ I

Proof state:
case intro
R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ f (∑ i : ι, x i • fun j => if i = j then 1 else 0) i ∈ I

Tactic:
simp only [Finset.sum_apply, smul_eq_mul, map_sum, Pi.smul_apply, map_smul]

Result:
case intro
R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ ∑ x_1 : ι, x x_1 * f (fun j => if x_1 = j then 1 else 0) i ∈ I

Proof state:
R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
⊢ f x i ∈ I

Tactic:
classical
  cases nonempty_fintype ι
  rw [pi_eq_sum_univ x]
  simp only [Finset.sum_apply, smul_eq_mul, map_sum, Pi.smul_apply, map_smul]
  exact I.sum_mem fun j _ => I.mul_mem_right _ (hi j)

Result:
no goals

Proof state:
case intro
R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ f x i ∈ I

Tactic:
rw [pi_eq_sum_univ x]

Result:
case intro
R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ f (∑ i : ι, x i • fun j => if i = j then 1 else 0) i ∈ I

Proof state:
case intro
R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ ∑ x_1 : ι, x x_1 * f (fun j => if x_1 = j then 1 else 0) i ∈ I

Tactic:
exact I.sum_mem fun j _ => I.mul_mem_right _ (hi j)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bmex_not_mem_brange {o : Ordinal} (f : ∀ a < o, Ordinal) : bmex o f ∉ brange o f

Proof state:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}
⊢ o.bmex f ∉ o.brange f

Tactic:
rw [← range_familyOfBFamily]

Result:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}
⊢ o.bmex f ∉ range (o.familyOfBFamily f)

Proof state:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}
⊢ o.bmex f ∉ range (o.familyOfBFamily f)

Tactic:
apply mex_not_mem_range

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma Sigma.map'_id_id {f : α → C} [HasCoproduct f] :
    Sigma.map' id (fun a => 𝟙 (f a)) = 𝟙 (∐ f)

Proof state:
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
⊢ (map' id fun a => 𝟙 (f a)) = 𝟙 (∐ f)

Tactic:
ext

Result:
case h
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
b✝ : α
⊢ (ι f b✝ ≫ map' id fun a => 𝟙 (f a)) = ι f b✝ ≫ 𝟙 (∐ f)

Proof state:
case h
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
b✝ : α
⊢ (ι f b✝ ≫ map' id fun a => 𝟙 (f a)) = ι f b✝ ≫ 𝟙 (∐ f)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem singularPart_totalVariation (s : SignedMeasure α) (μ : Measure α) :
    (s.singularPart μ).totalVariation =
      s.toJordanDecomposition.posPart.singularPart μ +
        s.toJordanDecomposition.negPart.singularPart μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (s.singularPart μ).totalVariation =
    s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ

Tactic:
have :
  (s.singularPart μ).toJordanDecomposition =
    ⟨s.toJordanDecomposition.posPart.singularPart μ,
      s.toJordanDecomposition.negPart.singularPart μ, singularPart_mutuallySingular s μ⟩ := by
  refine JordanDecomposition.toSignedMeasure_injective ?_
  rw [toSignedMeasure_toJordanDecomposition, singularPart, JordanDecomposition.toSignedMeasure]

Result:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
this :
  (s.singularPart μ).toJordanDecomposition =
    JordanDecomposition.mk (s.toJordanDecomposition.posPart.singularPart μ)
      (s.toJordanDecomposition.negPart.singularPart μ) ⋯
⊢ (s.singularPart μ).totalVariation =
    s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (s.singularPart μ).toJordanDecomposition.toSignedMeasure =
    (JordanDecomposition.mk (s.toJordanDecomposition.posPart.singularPart μ)
        (s.toJordanDecomposition.negPart.singularPart μ) ⋯).toSignedMeasure

Tactic:
rw [toSignedMeasure_toJordanDecomposition, singularPart, JordanDecomposition.toSignedMeasure]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
this :
  (s.singularPart μ).toJordanDecomposition =
    JordanDecomposition.mk (s.toJordanDecomposition.posPart.singularPart μ)
      (s.toJordanDecomposition.negPart.singularPart μ) ⋯
⊢ (s.singularPart μ).totalVariation =
    s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ

Tactic:
rw [totalVariation, this]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (s.singularPart μ).toJordanDecomposition =
    JordanDecomposition.mk (s.toJordanDecomposition.posPart.singularPart μ)
      (s.toJordanDecomposition.negPart.singularPart μ) ⋯

Tactic:
refine JordanDecomposition.toSignedMeasure_injective ?_

Result:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (s.singularPart μ).toJordanDecomposition.toSignedMeasure =
    (JordanDecomposition.mk (s.toJordanDecomposition.posPart.singularPart μ)
        (s.toJordanDecomposition.negPart.singularPart μ) ⋯).toSignedMeasure
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma nilRank_le_finrank : nilRank φ ≤ finrank R M

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : Nontrivial R
⊢ φ.nilRank ≤ finrank R M

Tactic:
simpa only [finrank_eq_card_chooseBasisIndex R M] using nilRank_le_card φ (chooseBasis R M)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem nat_abs_sum_le {ι : Type*} (s : Finset ι) (f : ι → ℤ) :
    (∑ i ∈ s, f i).natAbs ≤ ∑ i ∈ s, (f i).natAbs

Proof state:
ι : Type u_6
s : Finset ι
f : ι → ℤ
⊢ (∑ i ∈ s, f i).natAbs ≤ ∑ i ∈ s, (f i).natAbs

Tactic:
induction s using Finset.cons_induction with
| empty => simp only [Finset.sum_empty, Int.natAbs_zero, le_refl]
| cons i s his IH =>
  simp only [Finset.sum_cons, not_false_iff]
  exact (Int.natAbs_add_le _ _).trans (Nat.add_le_add_left IH _)

Result:
no goals

Proof state:
case cons
ι : Type u_6
f : ι → ℤ
i : ι
s : Finset ι
his : i ∉ s
IH : (∑ i ∈ s, f i).natAbs ≤ ∑ i ∈ s, (f i).natAbs
⊢ (∑ i ∈ Finset.cons i s his, f i).natAbs ≤ ∑ i ∈ Finset.cons i s his, (f i).natAbs

Tactic:
simp only [Finset.sum_cons, not_false_iff]

Result:
case cons
ι : Type u_6
f : ι → ℤ
i : ι
s : Finset ι
his : i ∉ s
IH : (∑ i ∈ s, f i).natAbs ≤ ∑ i ∈ s, (f i).natAbs
⊢ (f i + ∑ i ∈ s, f i).natAbs ≤ (f i).natAbs + ∑ i ∈ s, (f i).natAbs

Proof state:
case empty
ι : Type u_6
f : ι → ℤ
⊢ (∑ i ∈ ∅, f i).natAbs ≤ ∑ i ∈ ∅, (f i).natAbs

Tactic:
simp only [Finset.sum_empty, Int.natAbs_zero, le_refl]

Result:
no goals

Proof state:
case cons
ι : Type u_6
f : ι → ℤ
i : ι
s : Finset ι
his : i ∉ s
IH : (∑ i ∈ s, f i).natAbs ≤ ∑ i ∈ s, (f i).natAbs
⊢ (f i + ∑ i ∈ s, f i).natAbs ≤ (f i).natAbs + ∑ i ∈ s, (f i).natAbs

Tactic:
exact (Int.natAbs_add_le _ _).trans (Nat.add_le_add_left IH _)

Result:
no goals
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_lf_iff {a b : Ordinal} : a.toPGame ⧏ b.toPGame ↔ a < b :=
  ⟨by contrapose; rw [not_lt, not_lf]; exact toPGame_le, toPGame_lf⟩

Proof state:
a b : Ordinal.{u_1}
⊢ ¬a < b → ¬a.toPGame ⧏ b.toPGame

Tactic:
rw [not_lt, not_lf]

Result:
a b : Ordinal.{u_1}
⊢ b ≤ a → b.toPGame ≤ a.toPGame

Proof state:
a b : Ordinal.{u_1}
⊢ a.toPGame ⧏ b.toPGame → a < b

Tactic:
contrapose

Result:
a b : Ordinal.{u_1}
⊢ ¬a < b → ¬a.toPGame ⧏ b.toPGame

Proof state:
a b : Ordinal.{u_1}
⊢ b ≤ a → b.toPGame ≤ a.toPGame

Tactic:
exact toPGame_le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsb?_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsb? x i = none

Proof state:
w : Nat
x : BitVec w
i : Nat
ge : w ≤ i
⊢ x.getMsb? i = none

Tactic:
simp [getMsb?_eq_getLsb?]

Result:
w : Nat
x : BitVec w
i : Nat
ge : w ≤ i
⊢ i < w → w ≤ w - 1 - i

Proof state:
w : Nat
x : BitVec w
i : Nat
ge : w ≤ i
⊢ i < w → w ≤ w - 1 - i

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem init_update_castSucc : init (update q i.castSucc y) = update (init q) i y

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
⊢ init (update q i.castSucc y) j = update (init q) i y j

Tactic:
by_cases h : j = i

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : j = i
⊢ init (update q i.castSucc y) j = update (init q) i y j

case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : ¬j = i
⊢ init (update q i.castSucc y) j = update (init q) i y j

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : j = i
⊢ init (update q i.castSucc y) i = update (init q) i y i

Tactic:
simp [init]

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
⊢ init (update q i.castSucc y) = update (init q) i y

Tactic:
ext j

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
⊢ init (update q i.castSucc y) j = update (init q) i y j

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : j = i
⊢ init (update q i.castSucc y) j = update (init q) i y j

Tactic:
rw [h]

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : j = i
⊢ init (update q i.castSucc y) i = update (init q) i y i

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : ¬j = i
⊢ init (update q i.castSucc y) j = update (init q) i y j

Tactic:
simp [init, h, castSucc_inj]

Result:
no goals