harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem smul_eq_self_of_mem_zpowers {α : Type*} [MulAction G α] (hx : x ∈ Subgroup.zpowers y)
    {a : α} (hs : y • a = a) : x • a = a

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
y : G
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ zpowers y
⊢ (MulAction.toPerm y ^ k) a = a

Tactic:
exact Function.IsFixedPt.perm_zpow (by exact hs) k

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
y : G
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ zpowers y
⊢ IsFixedPt (⇑(MulAction.toPerm y)) a

Tactic:
exact hs

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
y : G
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ zpowers y
⊢ y ^ k • a = a

Tactic:
rw [← MulAction.toPerm_apply, ← MulAction.toPermHom_apply, MonoidHom.map_zpow _ y k,
  MulAction.toPermHom_apply]

Result:
case intro
G : Type u_1
inst✝¹ : Group G
y : G
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ zpowers y
⊢ (MulAction.toPerm y ^ k) a = a

Proof state:
G : Type u_1
inst✝¹ : Group G
x y : G
α : Type u_6
inst✝ : MulAction G α
hx : x ∈ zpowers y
a : α
hs : y • a = a
⊢ x • a = a

Tactic:
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp hx

Result:
case intro
G : Type u_1
inst✝¹ : Group G
y : G
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ zpowers y
⊢ y ^ k • a = a
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderiv_zero_of_not_differentiableAt (h : ¬DifferentiableAt 𝕜 f x) : fderiv 𝕜 f x = 0

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
x : E
h : ¬DifferentiableAt 𝕜 f x
⊢ ¬DifferentiableWithinAt 𝕜 f univ x

Tactic:
rwa [differentiableWithinAt_univ]

Result:
no goals

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
x : E
h : ¬DifferentiableAt 𝕜 f x
⊢ fderiv 𝕜 f x = 0

Tactic:
rw [fderiv, fderivWithin_zero_of_not_differentiableWithinAt]

Result:
𝕜 : 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
x : E
h : ¬DifferentiableAt 𝕜 f x
⊢ ¬DifferentiableWithinAt 𝕜 f univ x
-- Mathlib/Data/Int/Init.lean
lemma pred_self_lt (a : ℤ) : pred a < a

Proof state:
a : ℤ
⊢ a - 1 < a

Tactic:
omega

Result:
no goals

Proof state:
a : ℤ
⊢ a.pred < a

Tactic:
unfold pred

Result:
a : ℤ
⊢ a - 1 < a
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
/-- The character of level `d` through which `χ` factors is uniquely determined. -/
lemma existsUnique {d : ℕ} [NeZero n] (h : FactorsThrough χ d) :
    ∃! χ' : DirichletCharacter R d, χ = changeLevel h.dvd χ'

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
h : χ.FactorsThrough d
⊢ ∃! χ', χ = (changeLevel ⋯) χ'

Tactic:
rcases h with ⟨hd, χ₂, rfl⟩

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n d : ℕ
inst✝ : NeZero n
hd : d ∣ n
χ₂ : DirichletCharacter R d
⊢ ∃! χ', (changeLevel hd) χ₂ = (changeLevel ⋯) χ'

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n d : ℕ
inst✝ : NeZero n
hd : d ∣ n
χ₂ : DirichletCharacter R d
⊢ ∃! χ', (changeLevel hd) χ₂ = (changeLevel ⋯) χ'

Tactic:
exact ⟨χ₂, rfl, fun χ₃ hχ₃ ↦ (changeLevel_injective hd hχ₃).symm⟩

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem val_smul (n : α) : ∀ y : HomogeneousLocalization 𝒜 x, (n • y).val = n • y.val :=
  Quotient.ind' fun _ ↦ by rw [← mk_smul, val_mk, val_mk, Localization.smul_mk]; rfl

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
α : Type u_4
inst✝³ : SMul α R
inst✝² : SMul α A
inst✝¹ : IsScalarTower α R A
inst✝ : IsScalarTower α A A
n : α
x✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(n • x✝).num ⟨↑(n • x✝).den, ⋯⟩ = Localization.mk (n • ↑x✝.num) ⟨↑x✝.den, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
α : Type u_4
inst✝³ : SMul α R
inst✝² : SMul α A
inst✝¹ : IsScalarTower α R A
inst✝ : IsScalarTower α A A
n : α
x✝ : NumDenSameDeg 𝒜 x
⊢ (n • Quotient.mk'' x✝).val = n • val (Quotient.mk'' x✝)

Tactic:
rw [← mk_smul, val_mk, val_mk, Localization.smul_mk]

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
α : Type u_4
inst✝³ : SMul α R
inst✝² : SMul α A
inst✝¹ : IsScalarTower α R A
inst✝ : IsScalarTower α A A
n : α
x✝ : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(n • x✝).num ⟨↑(n • x✝).den, ⋯⟩ = Localization.mk (n • ↑x✝.num) ⟨↑x✝.den, ⋯⟩
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_finset_sum (hT : DominatedFinMeasAdditive μ T C) {ι} (s : Finset ι) {f : ι → α → E}
    (hf : ∀ i ∈ s, Integrable (f i) μ) :
    (setToFun μ T hT fun a => ∑ i ∈ s, f i a) = ∑ i ∈ s, setToFun μ T hT (f i)

Proof state:
case h.e'_2.h.e'_14.h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, Integrable (f i) μ
a : α
⊢ ∑ i ∈ s, f i a = (∑ i ∈ s, f i) a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, Integrable (f i) μ
⊢ (setToFun μ T hT fun a => ∑ i ∈ s, f i a) = ∑ i ∈ s, setToFun μ T hT (f i)

Tactic:
convert setToFun_finset_sum' hT s hf with a

Result:
case h.e'_2.h.e'_14.h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, Integrable (f i) μ
a : α
⊢ ∑ i ∈ s, f i a = (∑ i ∈ s, f i) a
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
@[simp]
lemma inner_smul_left_real {z : ℝ} {x y : E} : ⟪z • x, y⟫ = z • ⟪x, y⟫

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> x = ↑z •> x
⊢ star (↑z •> inner y x) = z •> inner x y

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
⊢ inner (z •> x) y = z •> inner x y

Tactic:
have h₁ : z • x = (z : ℂ) • x := by simp

Result:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> x = ↑z •> x
⊢ inner (z •> x) y = z •> inner x y

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> x = ↑z •> x
⊢ inner (z •> x) y = z •> inner x y

Tactic:
rw [h₁, ← star_inner, inner_smul_right_complex]

Result:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> x = ↑z •> x
⊢ star (↑z •> inner y x) = z •> inner x y

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
⊢ z •> x = ↑z •> x

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
theorem coeff_hermite_of_odd_add {n k : ℕ} (hnk : Odd (n + k)) : coeff (hermite n) k = 0

Proof state:
case zero
k : ℕ
hnk : Odd (0 + k)
⊢ (hermite 0).coeff k = 0

Tactic:
rw [zero_add k] at hnk

Result:
case zero
k : ℕ
hnk : Odd k
⊢ (hermite 0).coeff k = 0

Proof state:
case succ.succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + k + 2)
⊢ Odd (n + k)

Tactic:
exact (Nat.odd_add.mp hnk).mpr even_two

Result:
no goals

Proof state:
case succ.succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ Odd (n + (k + 2))

Tactic:
rwa [Nat.succ_add_eq_add_succ] at hnk

Result:
no goals

Proof state:
case succ.succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ (hermite (n + 1)).coeff (k + 1) = 0

Tactic:
rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]

Result:
case succ.succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ Odd (n + (k + 2))

case succ.succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ Odd (n + k)

Proof state:
case succ.zero
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
hnk : Odd (n + Nat.succ 0)
⊢ (hermite (n + 1)).coeff 0 = 0

Tactic:
rw [coeff_hermite_succ_zero, ih hnk, neg_zero]

Result:
no goals

Proof state:
case zero
k : ℕ
hnk : Odd k
⊢ (hermite 0).coeff k = 0

Tactic:
exact coeff_hermite_of_lt hnk.pos

Result:
no goals

Proof state:
case succ.zero
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
hnk : Odd (n + 1 + 0)
⊢ (hermite (n + 1)).coeff 0 = 0

Tactic:
rw [Nat.succ_add_eq_add_succ] at hnk

Result:
case succ.zero
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
hnk : Odd (n + Nat.succ 0)
⊢ (hermite (n + 1)).coeff 0 = 0

Proof state:
case succ.succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ Odd (n + k)

Tactic:
rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk

Result:
case succ.succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + k + 2)
⊢ Odd (n + k)

Proof state:
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ n.succ + k.succ = n + k + 2

Tactic:
rw [Nat.succ_add, Nat.add_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_dropLast (xs : List α) (i : Nat) :
    xs.dropLast[i]? = if i < xs.length - 1 then xs[i]? else none

Proof state:
case isTrue
α : Type u_1
xs : List α
i : Nat
h✝ : i < xs.length - 1
⊢ xs.dropLast[i]? = xs[i]?

Tactic:
rw [getElem?_eq_getElem, getElem?_eq_getElem, getElem_dropLast]

Result:
case isTrue.h
α : Type u_1
xs : List α
i : Nat
h✝ : i < xs.length - 1
⊢ i < xs.dropLast.length

Proof state:
case isTrue.h
α : Type u_1
xs : List α
i : Nat
h✝ : i < xs.length - 1
⊢ i < xs.dropLast.length

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
xs : List α
i : Nat
⊢ xs.dropLast[i]? = if i < xs.length - 1 then xs[i]? else none

Tactic:
split

Result:
case isTrue
α : Type u_1
xs : List α
i : Nat
h✝ : i < xs.length - 1
⊢ xs.dropLast[i]? = xs[i]?

case isFalse
α : Type u_1
xs : List α
i : Nat
h✝ : ¬i < xs.length - 1
⊢ xs.dropLast[i]? = none

Proof state:
case isFalse
α : Type u_1
xs : List α
i : Nat
h✝ : ¬i < xs.length - 1
⊢ xs.dropLast[i]? = none

Tactic:
simp_all

Result:
no goals
-- Mathlib/Data/Nat/Sqrt.lean
lemma sqrt_add_eq' (n : ℕ) (h : a ≤ n + n) : sqrt (n ^ 2 + a) = n

Proof state:
a n : ℕ
h : a ≤ n + n
⊢ (n ^ 2 + a).sqrt = n

Tactic:
simpa [Nat.pow_two] using sqrt_add_eq n h

Result:
no goals
-- Mathlib/Data/Set/Functor.lean
theorem coe_eq_image_val (t : Set s) :
    @Lean.Internal.coeM Set s α _ Set.monad t = (t : Set α)

Proof state:
α : Type u
s : Set α
t : Set ↑s
⊢ ⋃ x ∈ t, {↑x} = Subtype.val '' t

Tactic:
ext

Result:
case h
α : Type u
s : Set α
t : Set ↑s
x✝ : α
⊢ x✝ ∈ ⋃ x ∈ t, {↑x} ↔ x✝ ∈ Subtype.val '' t

Proof state:
α : Type u
s : Set α
t : Set ↑s
⊢ Lean.Internal.coeM t = Subtype.val '' t

Tactic:
change ⋃ (x ∈ t), {x.1} = _

Result:
α : Type u
s : Set α
t : Set ↑s
⊢ ⋃ x ∈ t, {↑x} = Subtype.val '' t

Proof state:
case h
α : Type u
s : Set α
t : Set ↑s
x✝ : α
⊢ x✝ ∈ ⋃ x ∈ t, {↑x} ↔ x✝ ∈ Subtype.val '' t

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
@[simp]
lemma fromCols_mulVec_sumElim [Fintype n₁] [Fintype n₂]
    (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v₁ : n₁ → R) (v₂ : n₂ → R) :
    fromCols A₁ A₂ *ᵥ Sum.elim v₁ v₂ = A₁ *ᵥ v₁ + A₂ *ᵥ v₂

Proof state:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
v₁ : n₁ → R
v₂ : n₂ → R
⊢ A₁.fromCols A₂ *ᵥ Sum.elim v₁ v₂ = A₁ *ᵥ v₁ + A₂ *ᵥ v₂

Tactic:
ext

Result:
case h
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
v₁ : n₁ → R
v₂ : n₂ → R
x✝ : m
⊢ (A₁.fromCols A₂ *ᵥ Sum.elim v₁ v₂) x✝ = (A₁ *ᵥ v₁ + A₂ *ᵥ v₂) x✝

Proof state:
case h
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
v₁ : n₁ → R
v₂ : n₂ → R
x✝ : m
⊢ (A₁.fromCols A₂ *ᵥ Sum.elim v₁ v₂) x✝ = (A₁ *ᵥ v₁ + A₂ *ᵥ v₂) x✝

Tactic:
simp [Matrix.mulVec, fromCols]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem integral_eq_tsum_of_ac (h : IsFundamentalDomain G s μ) (hν : ν ≪ μ) (f : α → E)
    (hf : Integrable f ν) : ∫ x, f x ∂ν = ∑' g : G, ∫ x in g • s, f x ∂ν

Proof state:
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
ν : Measure α
inst✝ : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → E
hf : Integrable f ν
⊢ Integrable f ν

Tactic:
exact hf

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
ν : Measure α
inst✝ : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → E
hf : Integrable f ν
⊢ ∫ (x : α), f x ∂ν = ∑' (g : G), ∫ (x : α) in g • s, f x ∂ν

Tactic:
rw [← MeasureTheory.integral_sum_measure, h.sum_restrict_of_ac hν]

Result:
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
ν : Measure α
inst✝ : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → E
hf : Integrable f ν
⊢ Integrable f (sum fun g => ν.restrict (g • s))

Proof state:
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
ν : Measure α
inst✝ : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → E
hf : Integrable f ν
⊢ Integrable f (sum fun g => ν.restrict (g • s))

Tactic:
rw [h.sum_restrict_of_ac hν]

Result:
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
ν : Measure α
inst✝ : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → E
hf : Integrable f ν
⊢ Integrable f ν
-- Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean
theorem withDensity_eq_iff_of_sigmaFinite [SigmaFinite μ] {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
    (hg : AEMeasurable g μ) : μ.withDensity f = μ.withDensity g ↔ f =ᵐ[μ] g :=
  ⟨fun hfg ↦ by
    refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hf hg fun s hs _ ↦ ?_
    rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg], withDensity_congr_ae⟩

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
x✝ : μ s < ⊤
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

Tactic:
rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : μ.withDensity f = μ.withDensity g
⊢ f =ᶠ[ae μ] g

Tactic:
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hf hg fun s hs _ ↦ ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
x✝ : μ s < ⊤
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
-- Mathlib/CategoryTheory/Iso.lean
theorem hom_comp_eq_id (α : X ≅ Y) {f : Y ⟶ X} : α.hom ≫ f = 𝟙 X ↔ f = α.inv

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Y ⟶ X
⊢ α.hom ≫ f = 𝟙 X ↔ f = α.inv

Tactic:
rw [← eq_inv_comp, comp_id]

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem comap_comap (f : Ultrafilter γ) {m : α → β} {n : β → γ} (inj₀ : Injective n)
    (large₀ : range n ∈ f) (inj₁ : Injective m) (large₁ : range m ∈ f.comap inj₀ large₀)
    (inj₂ : Injective (n ∘ m) := inj₀.comp inj₁)
    (large₂ : range (n ∘ m) ∈ f :=
      (by rw [range_comp]; exact image_mem_of_mem_comap large₀ large₁)) :
    (f.comap inj₀ large₀).comap inj₁ large₁ = f.comap inj₂ large₂ :=
  coe_injective comap_comap

Proof state:
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ n '' range m ∈ f

Tactic:
exact image_mem_of_mem_comap large₀ large₁

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ range (n ∘ m) ∈ f

Tactic:
rw [range_comp]

Result:
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ n '' range m ∈ f
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_zero_apply (x : α →₀ R) : (linearCombination R (0 : α → M)) x = 0

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : α →₀ R
⊢ (linearCombination R 0) x = 0

Tactic:
simp [linearCombination_apply]

Result:
no goals
-- Mathlib/RingTheory/LocalRing/Module.lean
theorem span_eq_top_of_tmul_eq_basis [Module.Finite R M] {ι}
    (f : ι → M) (b : Basis ι k (k ⊗[R] M))
    (hb : ∀ i, 1 ⊗ₜ f i = b i) : Submodule.span R (Set.range f) = ⊤

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R M
ι : Type u_3
f : ι → M
b : Basis ι k (k ⊗[R] M)
hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i
⊢ Submodule.span k (Set.range (⇑((mk R k M) 1) ∘ f)) = Submodule.span k (Set.range ⇑b)

Tactic:
simp only [Function.comp_def, mk_apply, hb, Basis.span_eq]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R M
ι : Type u_3
f : ι → M
b : Basis ι k (k ⊗[R] M)
hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i
⊢ Submodule.span R (Set.range f) = ⊤

Tactic:
rw [← map_tensorProduct_mk_eq_top, Submodule.map_span, ← Submodule.restrictScalars_span R k
  Ideal.Quotient.mk_surjective, Submodule.restrictScalars_eq_top_iff,
  ← b.span_eq, ← Set.range_comp]

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R M
ι : Type u_3
f : ι → M
b : Basis ι k (k ⊗[R] M)
hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i
⊢ Submodule.span k (Set.range (⇑((mk R k M) 1) ∘ f)) = Submodule.span k (Set.range ⇑b)
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_eq_zero_of_scalar_zero {n : ℕ} (hc : c n = 0) : ofScalars E c n = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
hc : c n = 0
⊢ ofScalars E c n = 0

Tactic:
rw [ofScalars, hc, zero_smul 𝕜 (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem mem_dite_empty_left (p : Prop) [Decidable p] (t : ¬p → Set α) (x : α) :
    (x ∈ if h : p then ∅ else t h) ↔ ∃ h : ¬p, x ∈ t h

Proof state:
α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
⊢ (¬p ∧ ∀ (h : ¬p), x ∈ t h) ↔ ∃ (h : ¬p), x ∈ t h

Tactic:
exact ⟨fun h => ⟨h.1, h.2 h.1⟩, fun ⟨h₁, h₂⟩ => ⟨fun h => h₁ h, fun _ => h₂⟩⟩

Result:
no goals

Proof state:
α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
⊢ (x ∈ if h : p then ∅ else t h) ↔ ∃ (h : ¬p), x ∈ t h

Tactic:
simp only [mem_dite, mem_empty_iff_false, imp_false]

Result:
α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
⊢ (¬p ∧ ∀ (h : ¬p), x ∈ t h) ↔ ∃ (h : ¬p), x ∈ t h