harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem Multipliable.map_iff_of_leftInverse [CommMonoid γ] [TopologicalSpace γ] {G G'}
    [FunLike G α γ] [MonoidHomClass G α γ] [FunLike G' γ α] [MonoidHomClass G' γ α]
    (g : G) (g' : G') (hg : Continuous g) (hg' : Continuous g') (hinv : Function.LeftInverse g' g) :
    Multipliable (g ∘ f) ↔ Multipliable f :=
  ⟨fun h ↦ by
    have := h.map _ hg'
    rwa [← Function.comp_assoc, hinv.id] at this, fun h ↦ h.map _ hg⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : CommMonoid α
inst✝⁶ : TopologicalSpace α
f : β → α
inst✝⁵ : CommMonoid γ
inst✝⁴ : TopologicalSpace γ
G : Type u_4
G' : Type u_5
inst✝³ : FunLike G α γ
inst✝² : MonoidHomClass G α γ
inst✝¹ : FunLike G' γ α
inst✝ : MonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous ⇑g
hg' : Continuous ⇑g'
hinv : LeftInverse ⇑g' ⇑g
h : Multipliable (⇑g ∘ f)
this : Multipliable (⇑g' ∘ ⇑g ∘ f)
⊢ Multipliable f

Tactic:
rwa [← Function.comp_assoc, hinv.id] at this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : CommMonoid α
inst✝⁶ : TopologicalSpace α
f : β → α
inst✝⁵ : CommMonoid γ
inst✝⁴ : TopologicalSpace γ
G : Type u_4
G' : Type u_5
inst✝³ : FunLike G α γ
inst✝² : MonoidHomClass G α γ
inst✝¹ : FunLike G' γ α
inst✝ : MonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous ⇑g
hg' : Continuous ⇑g'
hinv : LeftInverse ⇑g' ⇑g
h : Multipliable (⇑g ∘ f)
⊢ Multipliable f

Tactic:
have := h.map _ hg'

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : CommMonoid α
inst✝⁶ : TopologicalSpace α
f : β → α
inst✝⁵ : CommMonoid γ
inst✝⁴ : TopologicalSpace γ
G : Type u_4
G' : Type u_5
inst✝³ : FunLike G α γ
inst✝² : MonoidHomClass G α γ
inst✝¹ : FunLike G' γ α
inst✝ : MonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous ⇑g
hg' : Continuous ⇑g'
hinv : LeftInverse ⇑g' ⇑g
h : Multipliable (⇑g ∘ f)
this : Multipliable (⇑g' ∘ ⇑g ∘ f)
⊢ Multipliable f
-- Mathlib/LinearAlgebra/Dimension/DivisionRing.lean
theorem linearIndependent_iff_card_le_finrank_span {ι : Type*} [Fintype ι] {b : ι → V} :
    LinearIndependent K b ↔ Fintype.card ι ≤ (Set.range b).finrank K

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_2
inst✝ : Fintype ι
b : ι → V
⊢ LinearIndependent K b ↔ Fintype.card ι ≤ Set.finrank K (range b)

Tactic:
rw [linearIndependent_iff_card_eq_finrank_span, (finrank_range_le_card _).le_iff_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getD_insertIfNew [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
    (m.insertIfNew k v).getD a fallback =
      if h : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h.1)) v
      else m.getD a fallback

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k a : α
fallback : β a
v : β k
⊢ (m.insertIfNew k v).getD a fallback =
    if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.getD a fallback

Tactic:
exact Raw₀.getD_insertIfNew ⟨m.1, _⟩ m.2

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k a : α
fallback : β a
v : β k
⊢ (m.insertIfNew k v).getD a fallback = if h : (k == a) = true ∧ ¬k ∈ m then cast ⋯ v else m.getD a fallback

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k a : α
fallback : β a
v : β k
⊢ (m.insertIfNew k v).getD a fallback =
    if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.getD a fallback
-- Mathlib/LinearAlgebra/Determinant.lean
theorem bot_lt_ker_of_det_eq_zero {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] {f : M →ₗ[𝕜] M}
    (hf : LinearMap.det f = 0) : ⊥ < LinearMap.ker f

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f = 0
this : FiniteDimensional 𝕜 M
⊢ ⊥ < ker f

Tactic:
contrapose hf

Result:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
this : FiniteDimensional 𝕜 M
hf : ¬⊥ < ker f
⊢ ¬LinearMap.det f = 0

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
this : FiniteDimensional 𝕜 M
hf : IsUnit f
⊢ ¬LinearMap.det f = 0

Tactic:
exact isUnit_iff_ne_zero.1 (f.isUnit_det hf)

Result:
no goals

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f = 0
⊢ FiniteDimensional 𝕜 M

Tactic:
simp [f.finiteDimensional_of_det_ne_one, hf]

Result:
no goals

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
this : FiniteDimensional 𝕜 M
hf : ¬⊥ < ker f
⊢ ¬LinearMap.det f = 0

Tactic:
simp only [bot_lt_iff_ne_bot, Classical.not_not, ← isUnit_iff_ker_eq_bot] at hf

Result:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
this : FiniteDimensional 𝕜 M
hf : IsUnit f
⊢ ¬LinearMap.det f = 0

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f = 0
⊢ ⊥ < ker f

Tactic:
have : FiniteDimensional 𝕜 M := by simp [f.finiteDimensional_of_det_ne_one, hf]

Result:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f = 0
this : FiniteDimensional 𝕜 M
⊢ ⊥ < ker f
-- Mathlib/RingTheory/Bialgebra/Hom.lean
theorem toAlgHom_toLinearMap (f : A →ₐc[R] B) :
    ((f : A →ₐ[R] B) : A →ₗ[R] B) = f

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : CoalgebraStruct R A
inst✝ : CoalgebraStruct R B
f : A →ₐc[R] B
⊢ ↑↑f = ↑f

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem gcd_map [Field k] [DecidableEq R] [DecidableEq k] (f : R →+* k) :
    gcd (p.map f) (q.map f) = (gcd p q).map f :=
  GCD.induction p q (fun x => by simp_rw [Polynomial.map_zero, EuclideanDomain.gcd_zero_left])
    fun x y _ ih => by rw [gcd_val, ← map_mod, ih, ← gcd_val]

Proof state:
R : Type u
k : Type y
inst✝³ : Field R
p q : R[X]
inst✝² : Field k
inst✝¹ : DecidableEq R
inst✝ : DecidableEq k
f : R →+* k
x : R[X]
⊢ EuclideanDomain.gcd (map f 0) (map f x) = map f (EuclideanDomain.gcd 0 x)

Tactic:
simp_rw [Polynomial.map_zero, EuclideanDomain.gcd_zero_left]

Result:
no goals

Proof state:
R : Type u
k : Type y
inst✝³ : Field R
p q : R[X]
inst✝² : Field k
inst✝¹ : DecidableEq R
inst✝ : DecidableEq k
f : R →+* k
x y : R[X]
x✝ : x ≠ 0
ih : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd (y % x) x)
⊢ EuclideanDomain.gcd (map f x) (map f y) = map f (EuclideanDomain.gcd x y)

Tactic:
rw [gcd_val, ← map_mod, ih, ← gcd_val]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Measure.lean
theorem volume_apply (I : Box ι) :
    (volume : Measure (ι → ℝ)).toBoxAdditive I = ∏ i, (I.upper i - I.lower i)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
⊢ volume.toBoxAdditive I = ∏ i : ι, (I.upper i - I.lower i)

Tactic:
rw [Measure.toBoxAdditive_apply, coe_eq_pi, Real.volume_pi_Ioc_toReal I.lower_le_upper]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Products.lean
theorem piObjIso_hom_comp_π (f : α → D ⥤ C) (d : D) (s : α) :
    (piObjIso f d).hom ≫ Pi.π (fun s => (f s).obj d) s = (Pi.π f s).app d

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
α : Type w
inst✝ : HasLimitsOfShape (Discrete α) C
f : α → D ⥤ C
d : D
s : α
⊢ (piObjIso f d).hom ≫ Pi.π (fun s => (f s).obj d) s = (Pi.π f s).app d

Tactic:
simp [piObjIso]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
/-- Half of **Jordan's inequality** for negative values. -/
lemma sin_le_mul (hx : -(π / 2) ≤ x) (hx₀ : x ≤ 0) : sin x ≤ 2 / π * x

Proof state:
x : ℝ
hx : -(π / 2) ≤ x
hx₀ : x ≤ 0
⊢ sin x ≤ 2 / π * x

Tactic:
simpa using mul_le_sin (neg_nonneg.2 hx₀) (neg_le.2 hx)

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
theorem shiftComm_hom_comp (i j : A) :
    (shiftComm X i j).hom ≫ f⟦j⟧'⟦i⟧' = f⟦i⟧'⟦j⟧' ≫ (shiftComm Y i j).hom

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftComm X i j).hom ≫ (shiftFunctor C i).map ((shiftFunctor C j).map f) =
    (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫ (shiftComm Y i j).hom

Tactic:
rw [shiftComm', ← shiftComm_symm, Iso.symm_hom, Iso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Basic.lean
theorem coe_iInf {ι : Sort*} (f : ι → ConvexCone 𝕜 E) : ↑(iInf f) = ⋂ i, (f i : Set E)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_5
f : ι → ConvexCone 𝕜 E
⊢ ↑(iInf f) = ⋂ i, ↑(f i)

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem hasFDerivAt_iff_hasGradientAt {frechet : F →L[𝕜] 𝕜} :
    HasFDerivAt f frechet x ↔ HasGradientAt f ((toDual 𝕜 F).symm frechet) x

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
frechet : F →L[𝕜] 𝕜
⊢ HasFDerivAt f frechet x ↔ HasGradientAt f ((toDual 𝕜 F).symm frechet) x

Tactic:
rw [hasGradientAt_iff_hasFDerivAt, (toDual 𝕜 F).apply_symm_apply frechet]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_add_const_Ico : (fun x => x + a) ⁻¹' Ico b c = Ico (b - a) (c - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) ⁻¹' Ico b c = Ico (b - a) (c - a)

Tactic:
simp [← Ici_inter_Iio]

Result:
no goals
-- Mathlib/Tactic/NormNum/Basic.lean
theorem isNat_natSub : {a b : ℕ} → {a' b' c : ℕ} →
    IsNat a a' → IsNat b b' → Nat.sub a' b' = c → IsNat (a - b) c
  | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨by simp⟩

Proof state:
n✝¹ n✝ : ℕ
⊢ ↑n✝¹ - ↑n✝ = ↑(n✝¹.sub n✝)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Instances/Rat.lean
theorem Nat.isUniformEmbedding_coe_rat : IsUniformEmbedding ((↑) : ℕ → ℚ) :=
  isUniformEmbedding_bot_of_pairwise_le_dist zero_lt_one <| by simpa using Nat.pairwise_one_le_dist

Proof state:
⊢ Pairwise fun x y => 1 ≤ dist ↑x ↑y

Tactic:
simpa using Nat.pairwise_one_le_dist

Result:
no goals
-- Mathlib/Data/Fin/VecNotation.lean
theorem vecHead_vecAlt1 (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α) :
    vecHead (vecAlt1 hm v) = v 1

Proof state:
α : Type u
m n : ℕ
hm : m + 2 = n + 1 + (n + 1)
v : Fin (m + 2) → α
⊢ vecHead (vecAlt1 hm v) = v 1

Tactic:
simp [vecHead, vecAlt1]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem eval_relabel (r : α → β) (a : β → Bool) (f : CNF α) :
    (relabel r f).eval a = f.eval (a ∘ r)

Proof state:
α : Type u_1
β : Type u_2
r : α → β
a : β → Bool
f : CNF α
⊢ eval a (relabel r f) = eval (a ∘ r) f

Tactic:
induction f <;> simp_all

Result:
no goals
-- Mathlib/Data/Matrix/Basic.lean
theorem scalar_commute_iff {r : α} {M : Matrix n n α} :
    Commute (scalar n r) M ↔ r • M = MulOpposite.op r • M

Proof state:
n : Type u_3
α : Type v
inst✝² : Semiring α
inst✝¹ : DecidableEq n
inst✝ : Fintype n
r : α
M : Matrix n n α
⊢ Commute ((scalar n) r) M ↔ r • M = MulOpposite.op r • M

Tactic:
simp_rw [Commute, SemiconjBy, scalar_apply, ← smul_eq_diagonal_mul, ← op_smul_eq_mul_diagonal]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean
theorem forall_mem_single (p : (ι → ℝ) → Box ι → Prop) (hJ : J ≤ I) (h : x ∈ Box.Icc I) :
    (∀ J' ∈ single I J hJ x h, p ((single I J hJ x h).tag J') J') ↔ p x J

Proof state:
ι : Type u_1
I J : Box ι
x : ι → ℝ
p : (ι → ℝ) → Box ι → Prop
hJ : J ≤ I
h : x ∈ Box.Icc I
⊢ (∀ J' ∈ single I J hJ x h, p ((single I J hJ x h).tag J') J') ↔ p x J

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_flatten (L : Array (Array α)) : L.flatten.size = (L.map size).sum

Proof state:
α : Type u_1
L : Array (Array α)
⊢ L.flatten.size = (map size L).sum

Tactic:
cases L using array₂_induction

Result:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.map List.toArray xss✝).toArray.flatten.size = (map size (List.map List.toArray xss✝).toArray).sum

Proof state:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.map List.toArray xss✝).toArray.flatten.size = (map size (List.map List.toArray xss✝).toArray).sum

Tactic:
simp [Function.comp_def]

Result:
no goals
-- Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean
theorem exists_partition_polynomial (n : ℕ) {ε : ℝ} (hε : 0 < ε) {b : Fq[X]} (hb : b ≠ 0)
    (A : Fin n → Fq[X]) : ∃ t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (Fintype.card Fq)⌉₊),
      ∀ i₀ i₁ : Fin n, t i₀ = t i₁ →
        (cardPowDegree (A i₁ % b - A i₀ % b) : ℝ) < cardPowDegree b • ε

Proof state:
case intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
exact ⟨t, fun i₀ i₁ hi => (ht i₀ i₁).mp hi⟩

Result:
no goals

Proof state:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
obtain ⟨t, ht⟩ := exists_partition_polynomial_aux n hε hb A

Result:
case intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
theorem le_add (a b : R) : abv a - abv b ≤ abv (a + b)

Proof state:
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a b : R
⊢ abv a - abv b ≤ abv (a + b)

Tactic:
simpa only [tsub_le_iff_right, add_neg_cancel_right, abv.map_neg] using abv.add_le (a + b) (-b)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem hasSum_integral_iUnion_ae {ι : Type*} [Countable ι] {s : ι → Set X}
    (hm : ∀ i, NullMeasurableSet (s i) μ) (hd : Pairwise (AEDisjoint μ on s))
    (hfi : IntegrableOn f (⋃ i, s i) μ) :
    HasSum (fun n => ∫ x in s n, f x ∂μ) (∫ x in ⋃ n, s n, f x ∂μ)

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝ : Countable ι
s : ι → Set X
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
hfi : IntegrableOn f (⋃ i, s i) μ
⊢ HasSum (fun n => ∫ (x : X) in s n, f x ∂μ) (∫ (x : X) in ⋃ n, s n, f x ∂μ)

Tactic:
simp only [IntegrableOn, Measure.restrict_iUnion_ae hd hm] at hfi ⊢

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝ : Countable ι
s : ι → Set X
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
hfi : Integrable f (Measure.sum fun i => μ.restrict (s i))
⊢ HasSum (fun n => ∫ (x : X) in s n, f x ∂μ) (∫ (x : X), f x ∂Measure.sum fun i => μ.restrict (s i))

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝ : Countable ι
s : ι → Set X
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
hfi : Integrable f (Measure.sum fun i => μ.restrict (s i))
⊢ HasSum (fun n => ∫ (x : X) in s n, f x ∂μ) (∫ (x : X), f x ∂Measure.sum fun i => μ.restrict (s i))

Tactic:
exact hasSum_integral_measure hfi

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem mem_iSup {ι : Sort*} (p : ι → Submodule R M) {m : M} :
    (m ∈ ⨆ i, p i) ↔ ∀ N, (∀ i, p i ≤ N) → m ∈ N

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
m : M
⊢ (∀ (b : Submodule R M), (∀ (i : ι), p i ≤ b) → span R {m} ≤ b) ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
simp only [span_singleton_le_iff_mem]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
rw [← span_singleton_le_iff_mem, le_iSup_iff]

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
m : M
⊢ (∀ (b : Submodule R M), (∀ (i : ι), p i ≤ b) → span R {m} ≤ b) ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N
-- Mathlib/RingTheory/Flat/Equalizer.lean
@[simp]
private lemma LinearMap.lTensor_ker_subtype_tensorKerInv [Module.Flat R M]
    (x : ker (AlgebraTensorModule.lTensor S M f)) :
    (lTensor M (ker f).subtype) ((tensorKerInv S M f) x) = x

Proof state:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f : N →ₗ[R] P
inst✝ : Module.Flat R M
x : ↥(ker ((AlgebraTensorModule.lTensor S M) f))
⊢ ((AlgebraTensorModule.lTensor S M) (ker f).subtype) ((LinearMap.tensorKerInv S M f) x) = ↑x

Tactic:
simp [LinearMap.tensorKerInv]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f : N →ₗ[R] P
inst✝ : Module.Flat R M
x : ↥(ker ((AlgebraTensorModule.lTensor S M) f))
⊢ (lTensor M (ker f).subtype) ((LinearMap.tensorKerInv S M f) x) = ↑x

Tactic:
rw [← AlgebraTensorModule.coe_lTensor (A := S)]

Result:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f : N →ₗ[R] P
inst✝ : Module.Flat R M
x : ↥(ker ((AlgebraTensorModule.lTensor S M) f))
⊢ ((AlgebraTensorModule.lTensor S M) (ker f).subtype) ((LinearMap.tensorKerInv S M f) x) = ↑x
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem cthickening_ball (hε : 0 ≤ ε) (hδ : 0 < δ) (x : E) :
    cthickening ε (ball x δ) = closedBall x (ε + δ)

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
x : E
⊢ cthickening ε (Metric.ball x δ) = Metric.closedBall x (ε + δ)

Tactic:
rw [← thickening_singleton, cthickening_thickening hε hδ,
    cthickening_singleton _ (add_nonneg hε hδ.le)]

Result:
no goals
-- Mathlib/Data/Sign.lean
/-- Casting out of `SignType` respects composition with functions preserving `0, 1, -1`. -/
lemma map_cast' {β : Type*} [One β] [Neg β] [Zero β]
    (f : α → β) (h₁ : f 1 = 1) (h₂ : f 0 = 0) (h₃ : f (-1) = -1) (s : SignType) :
    f s = s

Proof state:
α : Type u_1
inst✝⁵ : Zero α
inst✝⁴ : One α
inst✝³ : Neg α
β : Type u_2
inst✝² : One β
inst✝¹ : Neg β
inst✝ : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
s : SignType
⊢ f ↑s = ↑s

Tactic:
cases s <;> simp only [SignType.cast, h₁, h₂, h₃]

Result:
no goals
-- Mathlib/Data/Fintype/Quotient.lean
lemma eval_finChoice (f : ∀ i, Quotient (S i)) :
    eval (finChoice f) = f :=
  induction_on_fintype_pi f (fun a ↦ by rw [finChoice_eq]; rfl)

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ ⟦a⟧.eval = fun x => ⟦a x⟧

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ (finChoice fun x => ⟦a x⟧).eval = fun x => ⟦a x⟧

Tactic:
rw [finChoice_eq]

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ ⟦a⟧.eval = fun x => ⟦a x⟧
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem image_eq_image [HasImages V] [HasEqualizers V] {i i' j : ι} (r : c.Rel i j)
    (r' : c.Rel i' j) : imageSubobject (C.d i j) = imageSubobject (C.d i' j)

Proof state:
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i i' j : ι
r : c.Rel i j
r' : c.Rel i' j
⊢ imageSubobject (eqToHom ⋯ ≫ C.d i' j) = imageSubobject (C.d i' j)

Tactic:
apply imageSubobject_iso_comp

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i i' j : ι
r : c.Rel i j
r' : c.Rel i' j
⊢ imageSubobject (C.d i j) = imageSubobject (C.d i' j)

Tactic:
rw [← eqToHom_comp_d C r r']

Result:
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i i' j : ι
r : c.Rel i j
r' : c.Rel i' j
⊢ imageSubobject (eqToHom ⋯ ≫ C.d i' j) = imageSubobject (C.d i' j)