harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma toCycles_comp_homologyπ :
    S.toCycles ≫ S.homologyπ = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.toCycles ≫ S.homologyπ = 0

Tactic:
dsimp only [homologyπ]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.toCycles ≫ S.leftHomologyπ ≫ S.leftHomologyIso.hom = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.toCycles ≫ S.leftHomologyπ ≫ S.leftHomologyIso.hom = 0

Tactic:
simp only [toCycles_comp_leftHomologyπ_assoc, zero_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem min?_eq_none_iff {xs : List α} [Min α] : xs.min? = none ↔ xs = []

Proof state:
α : Type u_1
xs : List α
inst✝ : Min α
⊢ xs.min? = none ↔ xs = []

Tactic:
cases xs <;> simp [min?]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem sbtw_comm {x y z : P} : Sbtw R x y z ↔ Sbtw R z y x

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
x y z : P
⊢ Sbtw R x y z ↔ Sbtw R z y x

Tactic:
rw [Sbtw, Sbtw, wbtw_comm, ← and_assoc, ← and_assoc, and_right_comm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem toList_mapFinIdxM [Monad m] [LawfulMonad m] (l : Array α)
    (f : (i : Nat) → α → (h : i < l.size) → m β) :
    toList <$> l.mapFinIdxM f = l.toList.mapFinIdxM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
f : (i : Nat) → α → i < l.size → m β
⊢ toList <$> l.mapFinIdxM f = l.toList.mapFinIdxM f

Tactic:
rw [List.mapFinIdxM_toArray]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
f : (i : Nat) → α → i < l.size → m β
⊢ toList <$> List.toArray <$> l.toList.mapFinIdxM f = l.toList.mapFinIdxM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
f : (i : Nat) → α → i < l.size → m β
⊢ toList <$> List.toArray <$> l.toList.mapFinIdxM f = l.toList.mapFinIdxM f

Tactic:
simp only [Functor.map_map, id_map']

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem moveLeft_neg_toLeftMovesNeg {x : PGame} (i) :
    (-x).moveLeft (toLeftMovesNeg i) = -x.moveRight i

Proof state:
x : PGame
i : x.RightMoves
⊢ (-x).moveLeft (toLeftMovesNeg i) = -x.moveRight i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem restrict_idem (M : Matroid α) (R : Set α) : M ↾ R ↾ R = M ↾ R

Proof state:
α : Type u_1
M : Matroid α
R : Set α
⊢ M ↾ R ↾ R = M ↾ R

Tactic:
rw [M.restrict_restrict_eq Subset.rfl]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.image_sub_sub_deriv_le
    (hf : HasFPowerSeriesOnBall f p x r) (hr : r' < r) :
    ∃ C, ∀ᵉ (y ∈ EMetric.ball x r') (z ∈ EMetric.ball x r'),
      ‖f y - f z - p 1 fun _ => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hr : r' < r
⊢ ∃ C,
    ∀ y ∈ EMetric.ball x r',
      ∀ z ∈ EMetric.ball x r', ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * (‖y - x‖ ⊔ ‖z - x‖) * ‖y - z‖

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
hr : r' < r
⊢ ∃ C,
    ∀ y ∈ EMetric.ball x r',
      ∀ z ∈ EMetric.ball x r', ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * (‖y - x‖ ⊔ ‖z - x‖) * ‖y - z‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
hr : r' < r
⊢ ∃ C,
    ∀ y ∈ EMetric.ball x r',
      ∀ z ∈ EMetric.ball x r', ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * (‖y - x‖ ⊔ ‖z - x‖) * ‖y - z‖

Tactic:
simpa only [mem_univ, insert_eq_of_mem, univ_inter] using hf.image_sub_sub_deriv_le hr

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

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

Tactic:
simp only [mem_dite, mem_empty_iff_false, imp_false, not_not]

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

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

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

Result:
no goals
-- Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
lemma norm_irreducible_pos {ϖ : 𝒪[K]} (h : Irreducible ϖ) : 0 < ‖ϖ‖ :=
  lt_of_le_of_ne (_root_.norm_nonneg ϖ) (by simp [eq_comm, h.ne_zero])

Proof state:
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
ϖ : ↥𝒪[K]
h : Irreducible ϖ
⊢ 0 ≠ ‖ϖ‖

Tactic:
simp [eq_comm, h.ne_zero]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem image2_sUnion_right (s : Set α) (T : Set (Set β)) :
    image2 f s (⋃₀ T) = ⋃ t ∈ T, image2 f s t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
⊢ image2 f s (⋃₀ T) = ⋃ t ∈ T, image2 f s t

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem mapRange.addEquiv_trans (f : M ≃+ N) (f₂ : N ≃+ P) :
    (mapRange.addEquiv (f.trans f₂) : (α →₀ M) ≃+ (α →₀ P)) =
      (mapRange.addEquiv f).trans (mapRange.addEquiv f₂) :=
  AddEquiv.ext (mapRange_comp _ f₂.map_zero _ f.map_zero (by simp))

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : M ≃+ N
f₂ : N ≃+ P
⊢ (⇑f₂ ∘ ⇑f) 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem suffix_of_suffix_length_le
    (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) (ll : length l₁ ≤ length l₂) : l₁ <:+ l₂ :=
  reverse_prefix.1 <|
    prefix_of_prefix_length_le (reverse_prefix.2 h₁) (reverse_prefix.2 h₂) (by simp [ll])

Proof state:
α✝ : Type u_1
l₁ l₃ l₂ : List α✝
h₁ : l₁ <:+ l₃
h₂ : l₂ <:+ l₃
ll : l₁.length ≤ l₂.length
⊢ l₁.reverse.length ≤ l₂.reverse.length

Tactic:
simp [ll]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem C_neg_one : C R (-1) = X := show X * 2 - X = X by ring

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ X * 2 - X = X

Tactic:
ring

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
protected lemma IsLittleO.sqrt (hfg : f =o[l] g) (hg : 0 ≤ᶠ[l] g) :
    (Real.sqrt <| f ·) =o[l] (Real.sqrt <| g ·)

Proof state:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f =o[l] g
hg : 0 ≤ᶠ[l] g
⊢ (fun x => √(f x)) =o[l] fun x => √(g x)

Tactic:
simpa [Real.sqrt_eq_rpow] using hfg.rpow one_half_pos hg

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
theorem toSubgraph_rotate [DecidableEq V] (c : G.Walk v v) (h : u ∈ c.support) :
    (c.rotate h).toSubgraph = c.toSubgraph

Proof state:
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.rotate h).toSubgraph = c.toSubgraph

Tactic:
rw [rotate, toSubgraph_append, sup_comm, ← toSubgraph_append, take_spec]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_insert_self [LawfulBEq α] (h : m.WF) {k : α} [Inhabited (β k)] {v : β k} :
    (m.insert k v).get! k = v

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
k : α
inst✝ : Inhabited (β k)
v : β k
⊢ (m.insert k v).get! k = v

Tactic:
simp_to_raw using Raw₀.get!_insert_self

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem trans_left (hab : TransGen r a b) (hbc : ReflTransGen r b c) : TransGen r a c

Proof state:
case tail
α : Type u_1
r : α → α → Prop
a b c : α
hab : TransGen r a b
b✝ c✝ : α
a✝ : ReflTransGen r b b✝
hcd : r b✝ c✝
hac : TransGen r a b✝
⊢ TransGen r a c✝

Tactic:
exact hac.tail hcd

Result:
no goals

Proof state:
case refl
α : Type u_1
r : α → α → Prop
a b c : α
hab : TransGen r a b
⊢ TransGen r a b

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a b c : α
hab : TransGen r a b
hbc : ReflTransGen r b c
⊢ TransGen r a c

Tactic:
induction hbc with
| refl => assumption
| tail _ hcd hac => exact hac.tail hcd

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem moebius_ne_zero_iff_squarefree {n : ℕ} : μ n ≠ 0 ↔ Squarefree n

Proof state:
case mp
n : ℕ
h : ¬Squarefree n
⊢ μ n = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
case mpr
n : ℕ
h : Squarefree n
⊢ μ n ≠ 0

Tactic:
simp [h, pow_ne_zero]

Result:
no goals

Proof state:
n : ℕ
⊢ μ n ≠ 0 ↔ Squarefree n

Tactic:
constructor <;> intro h

Result:
case mp
n : ℕ
h : μ n ≠ 0
⊢ Squarefree n

case mpr
n : ℕ
h : Squarefree n
⊢ μ n ≠ 0

Proof state:
case mp
n : ℕ
h : μ n ≠ 0
⊢ Squarefree n

Tactic:
contrapose! h

Result:
case mp
n : ℕ
h : ¬Squarefree n
⊢ μ n = 0
-- Mathlib/RingTheory/LaurentSeries.lean
theorem valuation_X_pow (s : ℕ) :
    Valued.v (((X : K⟦X⟧) : K⸨X⸩) ^ s) = Multiplicative.ofAdd (-(s : ℤ))

Proof state:
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ Valued.v ((ofPowerSeries ℤ K) PowerSeries.X ^ s) = ↑(Multiplicative.ofAdd (-↑s))

Tactic:
erw [map_pow, ← one_mul (s : ℤ), ← neg_mul (1 : ℤ) s, Int.ofAdd_mul,
  WithZero.coe_zpow, ofAdd_neg, WithZero.coe_inv, zpow_natCast, valuation_of_algebraMap,
  intValuation_toFun, intValuation_X, ofAdd_neg, WithZero.coe_inv, inv_pow]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
theorem colimitObjIsoColimitCompEvaluation_ι_inv [HasColimitsOfShape J C] (F : J ⥤ K ⥤ C) (j : J)
    (k : K) :
    colimit.ι (F ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation F k).inv =
      (colimit.ι F j).app k

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ colimit.ι (F ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation F k).inv = (colimit.ι F j).app k

Tactic:
dsimp [colimitObjIsoColimitCompEvaluation]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ colimit.ι (F ⋙ (evaluation K C).obj k) j ≫ (preservesColimitIso ((evaluation K C).obj k) F).inv =
    (colimit.ι F j).app k

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ colimit.ι (F ⋙ (evaluation K C).obj k) j ≫ (preservesColimitIso ((evaluation K C).obj k) F).inv =
    (colimit.ι F j).app k

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_umod_of_msb {x y : BitVec w} (h : x.msb = false) :
    (x % y).toInt = x.toInt % y.toNat

Proof state:
w : Nat
x y : BitVec w
h : x.msb = false
⊢ (x % y).toInt = x.toInt % ↑y.toNat

Tactic:
simp [toInt_eq_msb_cond, h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
/-- The following diagram is a pullback
```
X --id--> X
|         |
f         f
v         v
Z --id--> Z
```
-/
lemma id_horiz (f : X ⟶ Z) : IsPushout (𝟙 X) f f (𝟙 Z) :=
  of_horiz_isIso ⟨by simp only [Category.id_comp, Category.comp_id]⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X : C
f : X ⟶ Z
⊢ 𝟙 X ≫ f = f ≫ 𝟙 Z

Tactic:
simp only [Category.id_comp, Category.comp_id]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
lemma coeffs_one : coeffs (1 : MvPolynomial σ R) ⊆ {1}

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ coeffs 1 ⊆ {1}

Tactic:
rw [coeffs, Finset.image_subset_iff]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ ∀ x ∈ support 1, coeff x 1 ∈ {1}

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ coeffs 1 ⊆ {1}

Tactic:
classical
  rw [coeffs, Finset.image_subset_iff]
  simp_all [coeff_one]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ ∀ x ∈ support 1, coeff x 1 ∈ {1}

Tactic:
simp_all [coeff_one]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem toList_singleton (v : Vector α 1) : v.toList = [v.head]

Proof state:
α : Type u_1
v : Vector α 1
⊢ (v.head ::ᵥ v.tail).toList = [(v.head ::ᵥ v.tail).head]

Tactic:
simp only [toList_cons, toList_nil, head_cons, eq_self_iff_true, and_self_iff, singleton_tail]

Result:
no goals

Proof state:
α : Type u_1
v : Vector α 1
⊢ v.toList = [v.head]

Tactic:
rw [← v.cons_head_tail]

Result:
α : Type u_1
v : Vector α 1
⊢ (v.head ::ᵥ v.tail).toList = [(v.head ::ᵥ v.tail).head]
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem support_reverse {u v : V} (p : G.Walk u v) : p.reverse.support = p.support.reverse

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.support = p.support.reverse

Tactic:
induction p <;> simp [support_append, *]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem eq_neg_self_iff {θ : Angle} : θ = -θ ↔ θ = 0 ∨ θ = π

Proof state:
θ : Angle
⊢ θ = -θ ↔ θ = 0 ∨ θ = ↑π

Tactic:
rw [← add_eq_zero_iff_eq_neg, ← two_nsmul, two_nsmul_eq_zero_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Bimon_.lean
theorem hom_comul_hom {M N : Bimon_ C} (f : M ⟶ N) :
    f.hom.hom ≫ N.comul.hom = M.comul.hom ≫ (f.hom.hom ⊗ f.hom.hom)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Bimon_ C
f : M ⟶ N
⊢ f.hom.hom ≫ N.comul.hom = M.comul.hom ≫ (f.hom.hom ⊗ f.hom.hom)

Tactic:
simpa [- Comon_.Hom.hom_comul] using congr_arg Mon_.Hom.hom f.hom_comul

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
theorem ι_mul_ι (r₁ r₂) : ι (0 : QuadraticForm R R) r₁ * ι (0 : QuadraticForm R R) r₂ = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
r₁ r₂ : R
⊢ (ι 0) r₁ * (ι 0) r₂ = 0

Tactic:
rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, LinearMap.map_smul,
  LinearMap.map_smul, smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, RingHom.map_zero,
  smul_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
@[simp]
lemma basis_zero : CoordinateRing.basis W 0 = 1

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
⊢ (CoordinateRing.basis W) 0 = 1

Tactic:
simpa only [basis_apply] using pow_zero _

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_insert (f : (∀ i, π i) → ℝ≥0∞) (hf : Measurable f) {i : δ}
    (hi : i ∉ s) (x : ∀ i, π i) :
    (∫⋯∫⁻_insert i s, f ∂μ) x = ∫⁻ xᵢ, (∫⋯∫⁻_s, f ∂μ) (Function.update x i xᵢ) ∂μ i

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∉ s
x : (i : δ) → π i
⊢ (∫⋯∫⁻_insert i s, f ∂μ) x = ∫⁻ (xᵢ : π i), (∫⋯∫⁻_s, f ∂μ) (update x i xᵢ) ∂μ i

Tactic:
rw [Finset.insert_eq, lmarginal_union μ f hf (Finset.disjoint_singleton_left.mpr hi),
  lmarginal_singleton]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
@[simp, norm_cast]
lemma ofReal_qsmul (q : ℚ) (r : ℝ) : ofReal (q • r) = q • r

Proof state:
q : ℚ
r : ℝ
⊢ ↑(q • r) = q • ↑r

Tactic:
simp [Rat.smul_def]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem one_pow (b : ℕ) : ((nat_lit 1).rawCast : R) ^ b = (nat_lit 1).rawCast

Proof state:
R : Type u_1
inst✝ : CommSemiring R
b : ℕ
⊢ Nat.rawCast 1 ^ b = Nat.rawCast 1

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Basic.lean
theorem salient_iff_not_flat (S : ConvexCone 𝕜 E) : S.Salient ↔ ¬S.Flat

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
⊢ S.Salient ↔ ¬S.Flat

Tactic:
simp [Salient, Flat]

Result:
no goals
-- Mathlib/RingTheory/Derivation/MapCoeffs.lean
@[simp]
lemma mapCoeffs_monomial (n : ℕ) (x : A) :
    d.mapCoeffs (monomial n x) = .single A n (d x) := Finsupp.ext fun _ ↦ by
  simp [coeff_monomial, apply_ite d, PolynomialModule.single_apply]

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
n : ℕ
x : A
x✝ : ℕ
⊢ (d.mapCoeffs ((monomial n) x)) x✝ = ((PolynomialModule.single A n) (d x)) x✝

Tactic:
simp [coeff_monomial, apply_ite d, PolynomialModule.single_apply]

Result:
no goals
-- Mathlib/Data/Finset/Interval.lean
theorem card_Iic_finset : (Iic s).card = 2 ^ s.card

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #(Iic s) = 2 ^ #s

Tactic:
rw [Iic_eq_powerset, card_powerset]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_insertListConst_of_mem [BEq α] [EquivBEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)}
    {k k' : α} (k_beq : k == k') {v : β}
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ toInsert)
    {h} :
    getValue k' (insertListConst l toInsert) h = v

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
h : containsKey k' (insertListConst l toInsert) = true
⊢ getValue k' (insertListConst l toInsert) h = v

Tactic:
rw [← Option.some_inj, ← getValue?_eq_some_getValue,
  getValue?_insertListConst_of_mem k_beq distinct_l distinct_toInsert mem]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Lemmas.lean
theorem cast_pow {K} [DivisionSemiring K] (q : ℚ≥0) (n : ℕ) :
    NNRat.cast (q ^ n) = (NNRat.cast q : K) ^ n

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ ↑(q ^ n) = ↑q ^ n

Tactic:
rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Nat.cast_pow, div_eq_mul_inv, ← inv_pow,
  ← (Nat.cast_commute _ _).mul_pow, ← div_eq_mul_inv]

Result:
no goals
-- Mathlib/Computability/EpsilonNFA.lean
theorem stepSet_empty (a : α) : M.stepSet ∅ a = ∅

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
a : α
⊢ M.stepSet ∅ a = ∅

Tactic:
simp_rw [stepSet, mem_empty_iff_false, iUnion_false, iUnion_empty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
    (h : m.1.WF) {l : List α} {k k' fallback : α} (k_beq : k == k') :
    m.contains k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
      getKeyD (insertManyIfNewUnit m l).1 k' fallback = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
k k' fallback : α
k_beq : (k == k') = true
⊢ m.contains k = false →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).val.getKeyD k' fallback = k

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.getKeyD_insertListIfNewUnit_of_contains_eq_false_of_mem

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
lemma desc_f' (j : ι) (hj : ¬ c.Rel j (c.next j)) :
    (desc φ α hα).f j = sndX φ j ≫ α.f j

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hj : ¬c.Rel j (c.next j)
⊢ (desc φ α hα).f j = sndX φ j ≫ α.f j

Tactic:
apply dif_neg hj

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
    m.contains a = (get? m a).isSome

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
⊢ m.contains a = (get? m a).isSome

Tactic:
simp_to_model using List.containsKey_eq_isSome_getValue?

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_ne_zero : a⁻¹ ≠ 0 ↔ a ≠ ∞

Proof state:
a : ℝ≥0∞
⊢ a⁻¹ ≠ 0 ↔ a ≠ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mul_inv {f : M →* N} (h : ∀ y : S, IsUnit (f y)) {x₁ x₂} {y₁ y₂ : S} :
    f x₁ * (IsUnit.liftRight (f.restrict S) h y₁)⁻¹ =
        f x₂ * (IsUnit.liftRight (f.restrict S) h y₂)⁻¹ ↔
      f (x₁ * y₂) = f (x₂ * y₁)

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f x₁ * ↑((IsUnit.liftRight (f.restrict S) h) y₁)⁻¹ = f x₂ * ↑((IsUnit.liftRight (f.restrict S) h) y₂)⁻¹ ↔
    f (x₁ * ↑y₂) = f (x₂ * ↑y₁)

Tactic:
rw [mul_inv_right h, mul_assoc, mul_comm _ (f y₂), ← mul_assoc, mul_inv_left h, mul_comm x₂,
  f.map_mul, f.map_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
@[simp]
lemma map_zero_hom_app (X : C) :
    F.map ((zero hF s i).hom.app X) =
      (i 0).hom.app X ≫ (shiftFunctorZero D A).hom.app (F.obj X)

Proof state:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
X : C
⊢ F.map ((zero hF s i).hom.app X) = (i 0).hom.app X ≫ (shiftFunctorZero D A).hom.app (F.obj X)

Tactic:
simp [zero]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean
lemma transfiniteCompositionsOfShape_monotone :
    Monotone (transfiniteCompositionsOfShape (C := C) (J := J))

Proof state:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
t : a✝.TransfiniteCompositionOfShape J f✝
⊢ b✝.transfiniteCompositionsOfShape J f✝

Tactic:
exact ⟨t.ofLE h⟩

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ Monotone fun W => W.transfiniteCompositionsOfShape J

Tactic:
rintro _ _ h _ _ _ ⟨t⟩

Result:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
t : a✝.TransfiniteCompositionOfShape J f✝
⊢ b✝.transfiniteCompositionsOfShape J f✝
-- Mathlib/CategoryTheory/Preadditive/Basic.lean
theorem kernelForkOfFork_ofι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) :
    kernelForkOfFork (Fork.ofι ι w) = KernelFork.ofι ι (by simp [w]) :=
  rfl

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ι ≫ (f - g) = 0

Tactic:
simp [w]

Result:
no goals