harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/StdBasis.lean
theorem matrix_apply (b : Basis ι R M) (i : m) (j : n) (k : ι) [DecidableEq m] [DecidableEq n] :
    b.matrix m n (i, j, k) = Matrix.stdBasisMatrix i j (b k)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
m : Type u_4
n : Type u_5
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
i : m
j : n
k : ι
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
⊢ (Basis.matrix m n b) (i, j, k) = Matrix.stdBasisMatrix i j (b k)

Tactic:
simp [Basis.matrix, Matrix.stdBasisMatrix_eq_of_single_single]

Result:
no goals
-- Mathlib/Dynamics/FixedPoints/Basic.lean
theorem Commute.invOn_fixedPoints_comp (h : Commute f g) :
    Set.InvOn f g (fixedPoints <| f ∘ g) (fixedPoints <| f ∘ g)

Proof state:
α : Type u
f g : α → α
h : Function.Commute f g
⊢ Set.InvOn f g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
simpa only [h.comp_eq] using Function.invOn_fixedPoints_comp f g

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
theorem cospherical_iff_exists_sphere {ps : Set P} :
    Cospherical ps ↔ ∃ s : Sphere P, ps ⊆ (s : Set P)

Proof state:
case refine_2
P : Type u_2
inst✝ : MetricSpace P
ps : Set P
h : ∃ s, ps ⊆ Metric.sphere s.center s.radius
⊢ Cospherical ps

Tactic:
rcases h with ⟨s, h⟩

Result:
case refine_2.intro
P : Type u_2
inst✝ : MetricSpace P
ps : Set P
s : Sphere P
h : ps ⊆ Metric.sphere s.center s.radius
⊢ Cospherical ps

Proof state:
case refine_1.intro.intro
P : Type u_2
inst✝ : MetricSpace P
ps : Set P
c : P
r : ℝ
h : ∀ p ∈ ps, dist p c = r
⊢ ∃ s, ps ⊆ Metric.sphere s.center s.radius

Tactic:
exact ⟨⟨c, r⟩, h⟩

Result:
no goals

Proof state:
case refine_1
P : Type u_2
inst✝ : MetricSpace P
ps : Set P
h : Cospherical ps
⊢ ∃ s, ps ⊆ Metric.sphere s.center s.radius

Tactic:
rcases h with ⟨c, r, h⟩

Result:
case refine_1.intro.intro
P : Type u_2
inst✝ : MetricSpace P
ps : Set P
c : P
r : ℝ
h : ∀ p ∈ ps, dist p c = r
⊢ ∃ s, ps ⊆ Metric.sphere s.center s.radius

Proof state:
case refine_2.intro
P : Type u_2
inst✝ : MetricSpace P
ps : Set P
s : Sphere P
h : ps ⊆ Metric.sphere s.center s.radius
⊢ Cospherical ps

Tactic:
exact ⟨s.center, s.radius, h⟩

Result:
no goals

Proof state:
P : Type u_2
inst✝ : MetricSpace P
ps : Set P
⊢ Cospherical ps ↔ ∃ s, ps ⊆ Metric.sphere s.center s.radius

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
P : Type u_2
inst✝ : MetricSpace P
ps : Set P
h : Cospherical ps
⊢ ∃ s, ps ⊆ Metric.sphere s.center s.radius

case refine_2
P : Type u_2
inst✝ : MetricSpace P
ps : Set P
h : ∃ s, ps ⊆ Metric.sphere s.center s.radius
⊢ Cospherical ps
-- Mathlib/Order/CompleteLattice.lean
lemma iInf_psigma {ι : Sort*} {κ : ι → Sort*} (f : (Σ' i, κ i) → α) :
    ⨅ ij, f ij = ⨅ i, ⨅ j, f ⟨i, j⟩ :=
  eq_of_forall_le_iff fun c ↦ by simp only [le_iInf_iff, PSigma.forall]

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_8
κ : ι → Sort u_9
f : (i : ι) ×' κ i → α
c : α
⊢ c ≤ ⨅ ij, f ij ↔ c ≤ ⨅ i, ⨅ j, f ⟨i, j⟩

Tactic:
simp only [le_iInf_iff, PSigma.forall]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma tilted_const (μ : Measure α) [IsProbabilityMeasure μ] (c : ℝ) :
    μ.tilted (fun _ ↦ c) = μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
c : ℝ
⊢ (μ.tilted fun x => c) = μ

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_cons (s : Multiset α) (a : α) (comm) :
    noncommProd (a ::ₘ s) comm = a * noncommProd s (comm.mono fun _ => mem_cons_of_mem)

Proof state:
case h
α : Type u_3
inst✝ : Monoid α
a : α
a✝ : List α
comm : {x | x ∈ a ::ₘ ⟦a✝⟧}.Pairwise Commute
⊢ (a ::ₘ ⟦a✝⟧).noncommProd comm = a * noncommProd ⟦a✝⟧ ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
inst✝ : Monoid α
s : Multiset α
a : α
comm : {x | x ∈ a ::ₘ s}.Pairwise Commute
⊢ (a ::ₘ s).noncommProd comm = a * s.noncommProd ⋯

Tactic:
induction s using Quotient.inductionOn

Result:
case h
α : Type u_3
inst✝ : Monoid α
a : α
a✝ : List α
comm : {x | x ∈ a ::ₘ ⟦a✝⟧}.Pairwise Commute
⊢ (a ::ₘ ⟦a✝⟧).noncommProd comm = a * noncommProd ⟦a✝⟧ ⋯
-- Mathlib/Analysis/CStarAlgebra/Multiplier.lean
theorem norm_snd (a : 𝓜(𝕜, A)) : ‖a.snd‖ = ‖a‖

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.toProd.2‖ = ‖a‖

Tactic:
rw [← norm_fst, norm_fst_eq_snd]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem coeff_order_ne_zero {x : HahnSeries Γ R} (hx : x ≠ 0) : x.coeff x.order ≠ 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
hx : x ≠ 0
⊢ x.coeff x.order ≠ 0

Tactic:
rw [order_of_ne hx]

Result:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
hx : x ≠ 0
⊢ x.coeff (⋯.min ⋯) ≠ 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
hx : x ≠ 0
⊢ x.coeff (⋯.min ⋯) ≠ 0

Tactic:
exact x.isWF_support.min_mem (support_nonempty_iff.2 hx)

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_singleton (x : ZFSet) : ({x} : ZFSet).toSet = {x}

Proof state:
case h
x x✝ : ZFSet.{u_1}
⊢ x✝ ∈ {x}.toSet ↔ x✝ ∈ {x}

Tactic:
simp

Result:
no goals

Proof state:
x : ZFSet.{u_1}
⊢ {x}.toSet = {x}

Tactic:
ext

Result:
case h
x x✝ : ZFSet.{u_1}
⊢ x✝ ∈ {x}.toSet ↔ x✝ ∈ {x}
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.map_pre' [HasLimitsOfShape K C] (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
    limit.pre F E₂ = limit.pre F E₁ ≫ lim.map (whiskerRight α F)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
⊢ pre F E₂ = pre F E₁ ≫ lim.map (whiskerRight α F)

Tactic:
ext1

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
j✝ : K
⊢ pre F E₂ ≫ π (E₂ ⋙ F) j✝ = (pre F E₁ ≫ lim.map (whiskerRight α F)) ≫ π (E₂ ⋙ F) j✝

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
j✝ : K
⊢ pre F E₂ ≫ π (E₂ ⋙ F) j✝ = (pre F E₁ ≫ lim.map (whiskerRight α F)) ≫ π (E₂ ⋙ F) j✝

Tactic:
simp [← category.assoc]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
theorem LinearMap.lift_rank_range_add_rank_ker (f : M →ₗ[R] M') :
    lift.{u} (Module.rank R (LinearMap.range f)) + lift.{v} (Module.rank R (LinearMap.ker f)) =
      lift.{v} (Module.rank R M)

Proof state:
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
this : (p : Submodule R M) → DecidableEq (M ⧸ p)
⊢ lift.{u, v} (Module.rank R ↥(range f)) + lift.{v, u} (Module.rank R ↥(ker f)) = lift.{v, u} (Module.rank R M)

Tactic:
rw [← f.quotKerEquivRange.lift_rank_eq, ← lift_add, rank_quotient_add_rank]

Result:
no goals

Proof state:
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
⊢ lift.{u, v} (Module.rank R ↥(range f)) + lift.{v, u} (Module.rank R ↥(ker f)) = lift.{v, u} (Module.rank R M)

Tactic:
haveI := fun p : Submodule R M => Classical.decEq (M ⧸ p)

Result:
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
this : (p : Submodule R M) → DecidableEq (M ⧸ p)
⊢ lift.{u, v} (Module.rank R ↥(range f)) + lift.{v, u} (Module.rank R ↥(ker f)) = lift.{v, u} (Module.rank R M)
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem coe_inv_coe' {c d : S.objs} (p : c ⟶ d) :
    (CategoryTheory.inv p).val = CategoryTheory.inv p.val

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : ↑S.objs
p : c ⟶ d
⊢ ↑(inv p) = inv ↑p

Tactic:
simp only [← inv_eq_inv, coe_inv_coe]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem coe_support_eq_set_support (f : Perm α) : (f.support : Set α) = { x | f x ≠ x }

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x✝ : α
⊢ x✝ ∈ ↑f.support ↔ x✝ ∈ {x | f x ≠ x}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ ↑f.support = {x | f x ≠ x}

Tactic:
ext

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x✝ : α
⊢ x✝ ∈ ↑f.support ↔ x✝ ∈ {x | f x ≠ x}
-- Mathlib/Data/Finmap.lean
theorem lookup_insert_of_ne {a a'} {b : β a} (s : Finmap β) (h : a' ≠ a) :
    lookup a' (insert a b s) = lookup a' s :=
  induction_on s fun s => by simp only [insert_toFinmap, lookup_toFinmap, lookup_insert_ne h]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s✝ : Finmap β
h : a' ≠ a
s : AList β
⊢ lookup a' (insert a b ⟦s⟧) = lookup a' ⟦s⟧

Tactic:
simp only [insert_toFinmap, lookup_toFinmap, lookup_insert_ne h]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_rotate_sign (p₁ p₂ p₃ : P) : (∡ p₂ p₃ p₁).sign = (∡ p₁ p₂ p₃).sign

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ (∡ p₂ p₃ p₁).sign = (∡ p₁ p₂ p₃).sign

Tactic:
rw [← oangle_swap₁₂_sign, oangle_swap₁₃_sign]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem mk_eq_mk' (f : Polynomial K) {g : Polynomial K} (hg : g ≠ 0) :
    RatFunc.mk f g = IsLocalization.mk' (RatFunc K) f ⟨g, mem_nonZeroDivisors_iff_ne_zero.2 hg⟩ :=
  by simp only [mk_eq_div, IsFractionRing.mk'_eq_div]

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
f g : K[X]
hg : g ≠ 0
⊢ RatFunc.mk f g = IsLocalization.mk' (RatFunc K) f ⟨g, ⋯⟩

Tactic:
simp only [mk_eq_div, IsFractionRing.mk'_eq_div]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean
@[reassoc, to_app]
lemma mapComp_id_right_inv (f : a ⟶ b) : (F.mapComp f (𝟙 b)).inv =
    F.map f ◁ (F.mapId b).hom ≫ (ρ_ (F.map f)).hom ≫ F.map₂ (ρ_ f).inv

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : Pseudofunctor B C
a b : B
f : a ⟶ b
⊢ (F.mapComp f (𝟙 b)).inv = F.map f ◁ (F.mapId b).hom ≫ (ρ_ (F.map f)).hom ≫ F.map₂ (ρ_ f).inv

Tactic:
simp [mapComp_id_right]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
@[fun_prop]
lemma continuous_realContinuousMapZeroOfNNReal (φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A)
    (hφ : Continuous φ) : Continuous φ.realContinuousMapZeroOfNNReal

Proof state:
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous ⇑φ
⊢ Continuous ⇑φ.realContinuousMapZeroOfNNReal

Tactic:
simp [realContinuousMapZeroOfNNReal]

Result:
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous ⇑φ
⊢ Continuous fun f => φ f.toNNReal - φ (-f).toNNReal

Proof state:
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous ⇑φ
⊢ Continuous fun f => φ f.toNNReal - φ (-f).toNNReal

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem proj_symm_apply {x : B × F} (hx : x ∈ e.target) : proj (e.toPartialEquiv.symm x) = x.1

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
this : proj (↑e.symm x) = (↑e (↑e.symm x)).1
⊢ proj (↑e.symm x) = x.1

Tactic:
rwa [← e.coe_coe, e.right_inv hx] at this

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
⊢ proj (↑e.symm x) = x.1

Tactic:
have := (e.coe_fst (e.map_target hx)).symm

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
this : proj (↑e.symm x) = (↑e (↑e.symm x)).1
⊢ proj (↑e.symm x) = x.1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem any_iff_exists {p : α → Bool} {xs : Vector α n} :
    xs.any p ↔ ∃ (i : Nat) (_ : i < n), p xs[i]

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.any p = true ↔ ∃ i x, p { toArray := xs, size_toArray := ⋯ }[i] = true

Tactic:
simp [Array.any_iff_exists]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ xs.any p = true ↔ ∃ i x, p xs[i] = true

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.any p = true ↔ ∃ i x, p { toArray := xs, size_toArray := ⋯ }[i] = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem natAbs_div_le_natAbs (a b : Int) : natAbs (a / b) ≤ natAbs a :=
  match b, eq_nat_or_neg b with
  | _, ⟨n, .inl rfl⟩ => aux _ _
  | _, ⟨n, .inr rfl⟩ => by rw [Int.ediv_neg, natAbs_neg]; apply aux
where
  aux : ∀ (a : Int) (n : Nat), natAbs (a / n) ≤ natAbs a
  | ofNat _, _ => Nat.div_le_self ..
  | -[_+1], 0 => Nat.zero_le _
  | -[_+1], succ _ => Nat.succ_le_succ (Nat.div_le_self _ _)

Proof state:
a b : Int
n : Nat
⊢ (a / ↑n).natAbs ≤ a.natAbs

Tactic:
apply aux

Result:
no goals

Proof state:
a b : Int
n : Nat
⊢ (a / -↑n).natAbs ≤ a.natAbs

Tactic:
rw [Int.ediv_neg, natAbs_neg]

Result:
a b : Int
n : Nat
⊢ (a / ↑n).natAbs ≤ a.natAbs
-- Mathlib/Data/Set/Lattice.lean
theorem sUnion_eq_iUnion {s : Set (Set α)} : ⋃₀ s = ⋃ i : s, i

Proof state:
α : Type u_1
s : Set (Set α)
⊢ ⋃₀ s = ⋃ i, ↑i

Tactic:
simp only [← sUnion_range, Subtype.range_coe]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_split (f : β → α) (p : β → Prop) :
    ⨆ i, f i = (⨆ (i) (_ : p i), f i) ⊔ ⨆ (i) (_ : ¬p i), f i

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
p : β → Prop
⊢ ⨆ i, f i = (⨆ i, ⨆ (_ : p i), f i) ⊔ ⨆ i, ⨆ (_ : ¬p i), f i

Tactic:
simpa [Classical.em] using @iSup_union _ _ _ f { i | p i } { i | ¬p i }

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma mul_div_left_comm (a b c : EReal) : a * (b / c) = b * (a / c)

Proof state:
a b c : EReal
⊢ a * (b / c) = b * (a / c)

Tactic:
rw [mul_div a b c, mul_comm a b, ← mul_div b a c]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem HasIntegral.neg (hf : HasIntegral I l f vol y) : HasIntegral I l (-f) vol (-y)

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y : F
hf : HasIntegral I l f vol y
⊢ HasIntegral I l (-f) vol (-y)

Tactic:
simpa only [HasIntegral, ← integralSum_neg] using hf.neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem insert_eq {l : List α} {a : α} : l.insert a = if a ∈ l then l else a :: l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ List.insert a l = if a ∈ l then l else a :: l

Tactic:
simp [List.insert]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
lemma edge_adj (v w : V) : (edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w

Proof state:
V : Type u_1
s t v w : V
⊢ (edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w

Tactic:
rw [edge, fromEdgeSet_adj, Set.mem_singleton_iff, Sym2.eq_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a fallback : α}
    (hl : DistinctKeys l) :
    getKeyD a (eraseKey k l) fallback = if k == a then fallback else getKeyD a l fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a fallback : α
hl : DistinctKeys l
⊢ getKeyD a (eraseKey k l) fallback = if (k == a) = true then fallback else getKeyD a l fallback

Tactic:
simp [getKeyD_eq_getKey?, getKey?_eraseKey hl, apply_ite (fun x => Option.getD x fallback)]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem C_sub_two (n : ℤ) : C R (n - 2) = X * C R (n - 1) - C R n

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ C R (n - 2) = X * C R (n - 1) - C R n

Tactic:
linear_combination (norm := ring_nf) C_add_two R (n - 2)

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
theorem hasSum_sq_mFourierCoeff (f : L²(UnitAddTorus d)) :
    HasSum (fun i ↦ ‖mFourierCoeff f i‖ ^ 2) (∫ t, ‖f t‖ ^ 2)

Proof state:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
⊢ HasSum (fun i => ‖mFourierCoeff (↑↑f) i‖ ^ 2) (∫ (t : UnitAddTorus d), ‖↑↑f t‖ ^ 2)

Tactic:
simpa only [← RCLike.inner_apply, inner_self_eq_norm_sq, ← integral_re
  (L2.integrable_inner f f)] using RCLike.hasSum_re ℂ (hasSum_prod_mFourierCoeff f f)

Result:
no goals
-- Mathlib/Data/Finsupp/Interval.lean
theorem card_Iic : #(Iic f) = ∏ i ∈ f.support, #(Iic (f i))

Proof state:
ι : Type u_1
α : Type u_2
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : LocallyFiniteOrder α
f : ι →₀ α
⊢ #(Iic f) = ∏ i ∈ f.support, #(Iic (f i))

Tactic:
simp_rw [Iic_eq_Icc, card_Icc, Finsupp.bot_eq_zero, support_zero, empty_union,
zero_apply, bot_eq_zero]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : LocallyFiniteOrder α
f : ι →₀ α
⊢ #(Iic f) = ∏ i ∈ f.support, #(Iic (f i))

Tactic:
classical simp_rw [Iic_eq_Icc, card_Icc, Finsupp.bot_eq_zero, support_zero, empty_union,
    zero_apply, bot_eq_zero]

Result:
no goals
-- Mathlib/Data/Int/Basic.lean
lemma natCast_dvd {m : ℕ} : (m : ℤ) ∣ n ↔ m ∣ n.natAbs

Proof state:
n : ℤ
m : ℕ
⊢ ↑m ∣ n ↔ m ∣ n.natAbs

Tactic:
obtain hn | hn := natAbs_eq n <;> rw [hn] <;> simp [← natCast_dvd_natCast, Int.dvd_neg]

Result:
no goals
-- Mathlib/Data/List/Range.lean
theorem getElem_range'_1 {n m} (i) (H : i < (range' n m).length) :
    (range' n m)[i] = n + i

Proof state:
n m i : ℕ
H : i < (range' n m).length
⊢ (range' n m)[i] = n + i

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerRight_tensor {X X' : C} (f : X ⟶ X') (Y Z : C) :
    f ▷ (Y ⊗ Z) = (α_ X Y Z).inv ≫ f ▷ Y ▷ Z ≫ (α_ X' Y Z).hom

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

Tactic:
simp only [← id_tensorHom, ← tensorHom_id]

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

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

Tactic:
simp [tensor_id]

Result:
no goals

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

Tactic:
rw [associator_naturality]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ f ⊗ 𝟙 (Y ⊗ Z) = (α_ X Y Z).inv ≫ (α_ X Y Z).hom ≫ (f ⊗ 𝟙 Y ⊗ 𝟙 Z)
-- Mathlib/Data/Multiset/Bind.lean
theorem mem_bind {b s} {f : α → Multiset β} : b ∈ bind s f ↔ ∃ a ∈ s, b ∈ f a

Proof state:
α : Type u_1
β : Type v
b : β
s : Multiset α
f : α → Multiset β
⊢ b ∈ s.bind f ↔ ∃ a ∈ s, b ∈ f a

Tactic:
simp [bind]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
lemma of_iso (h : IsPushout f g inl inr)
    {Z' X' Y' P' : C} {f' : Z' ⟶ X'} {g' : Z' ⟶ Y'} {inl' : X' ⟶ P'} {inr' : Y' ⟶ P'}
    (e₁ : Z ≅ Z') (e₂ : X ≅ X') (e₃ : Y ≅ Y') (e₄ : P ≅ P')
    (commf : f ≫ e₂.hom = e₁.hom ≫ f')
    (commg : g ≫ e₃.hom = e₁.hom ≫ g')
    (comminl : inl ≫ e₄.hom = e₂.hom ≫ inl')
    (comminr : inr ≫ e₄.hom = e₃.hom ≫ inr') :
    IsPushout f' g' inl' inr' where
  w

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z ≅ Z'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : P ≅ P'
commf : f ≫ e₂.hom = e₁.hom ≫ f'
commg : g ≫ e₃.hom = e₁.hom ≫ g'
comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'
comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'
⊢ f' ≫ inl' = g' ≫ inr'

Tactic:
rw [← cancel_epi e₁.hom, ← reassoc_of% commf, ← comminl,
  ← reassoc_of% commg, ← comminr, h.w_assoc]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffOn.continuousOn_deriv_of_isOpen (h : ContDiffOn 𝕜 n f₂ s₂) (hs : IsOpen s₂)
    (hn : 1 ≤ n) : ContinuousOn (deriv f₂) s₂

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
h : ContDiffOn 𝕜 n f₂ s₂
hs : IsOpen s₂
hn : 1 ≤ n
⊢ ContinuousOn (deriv f₂) s₂

Tactic:
rw [show (1 : WithTop ℕ∞) = 0 + 1 from rfl] at hn

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
h : ContDiffOn 𝕜 n f₂ s₂
hs : IsOpen s₂
hn : 0 + 1 ≤ n
⊢ ContinuousOn (deriv f₂) s₂

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
h : ContDiffOn 𝕜 n f₂ s₂
hs : IsOpen s₂
hn : 0 + 1 ≤ n
⊢ ContinuousOn (deriv f₂) s₂

Tactic:
exact ((contDiffOn_succ_iff_deriv_of_isOpen hs).1 (h.of_le hn)).2.2.continuousOn

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem dvd_mod_iff {a b c : R} (h : c ∣ b) : c ∣ a % b ↔ c ∣ a

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : c ∣ b
⊢ c ∣ a % b ↔ c ∣ a

Tactic:
rw [← dvd_add_right (h.mul_right _), div_add_mod]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_imp_of_ae_restrict {s : Set α} {p : α → Prop} (h : ∀ᵐ x ∂μ.restrict s, p x) :
    ∀ᵐ x ∂μ, x ∈ s → p x

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
h : ∀ᵐ (x : α) ∂μ.restrict s, p x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

Tactic:
simp only [ae_iff] at h ⊢

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
h : (μ.restrict s) {a | ¬p a} = 0
⊢ μ {a | ¬(a ∈ s → p a)} = 0

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
h : (μ.restrict s) {a | ¬p a} = 0
⊢ μ {a | ¬(a ∈ s → p a)} = 0

Tactic:
simpa [setOf_and, inter_comm] using measure_inter_eq_zero_of_restrict h

Result:
no goals