harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma lift_μ {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) :
    lift (F.map f) (F.map g) ≫ LaxMonoidal.μ F _ _ = F.map (lift f g) :=
  (cancel_mono (μIso _ _ _).inv).1 (by simp)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (lift (F.map f) (F.map g) ≫ LaxMonoidal.μ F Y Z) ≫ (μIso F Y Z).inv = F.map (lift f g) ≫ (μIso F Y Z).inv

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem refl : IntervalIntegrable f μ a a

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a : ℝ
μ : Measure ℝ
⊢ IntervalIntegrable f μ a a

Tactic:
constructor <;> simp

Result:
no goals
-- Mathlib/Probability/Kernel/Invariance.lean
theorem comp_const_apply_eq_bind (κ : Kernel α β) (μ : Measure α) (a : α) :
    (κ ∘ₖ const α μ) a = μ.bind κ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
a : α
⊢ (κ ∘ₖ const α μ) a = μ.bind ⇑κ

Tactic:
rw [← const_apply (μ.bind κ) a, const_bind_eq_comp_const κ μ]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive]
protected lemma eq_div_iff (h : IsUnit c) : a = b / c ↔ a * c = b

Proof state:
α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a = b / c ↔ a * c = b

Tactic:
rw [div_eq_mul_inv, h.eq_mul_inv_iff_mul_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerLeft_iff {X Y : C} (f g : X ⟶ Y) : 𝟙_ C ◁ f = 𝟙_ C ◁ g ↔ f = g

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
⊢ 𝟙_ C ◁ f = 𝟙_ C ◁ g ↔ f = g

Tactic:
simp

Result:
no goals
-- Mathlib/Order/BooleanSubalgebra.lean
@[simp] lemma compl_mem_iff : aᶜ ∈ L ↔ a ∈ L := ⟨fun ha ↦ by simpa using compl_mem ha, compl_mem⟩

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
a : α
ha : aᶜ ∈ L
⊢ a ∈ L

Tactic:
simpa using compl_mem ha

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Constructions.lean
lemma cross_mk_of_ne {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) (h : mk F v hv ≠ mk F w hw) :
    cross (mk F v hv) (mk F w hw) = mk F (crossProduct v w)
      (mt (mk_eq_mk_iff_crossProduct_eq_zero hv hw).mpr h)

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ (mk F v hv).cross (mk F w hw) = mk F ((crossProduct v) w) ⋯

Tactic:
rw [cross_mk_of_cross_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
    (as.modify i f)[j]? = if i = j then as[j]?.map f else as[j]?

Proof state:
α : Type u_1
as : Array α
i : Nat
f : α → α
j : Nat
⊢ (if h : j < as.size then some (if i = j then f as[j] else as[j]) else none) =
    if i = j then if h : j < as.size then some (f as[j]) else none else if h : j < as.size then some as[j] else none

Tactic:
split <;> split <;> rfl

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
f : α → α
j : Nat
⊢ (as.modify i f)[j]? = if i = j then Option.map f as[j]? else as[j]?

Tactic:
simp only [getElem?_def, size_modify, getElem_modify, Option.map_dif]

Result:
α : Type u_1
as : Array α
i : Nat
f : α → α
j : Nat
⊢ (if h : j < as.size then some (if i = j then f as[j] else as[j]) else none) =
    if i = j then if h : j < as.size then some (f as[j]) else none else if h : j < as.size then some as[j] else none
-- Mathlib/Data/Set/Prod.lean
theorem univ_pi_nonempty_iff : (pi univ t).Nonempty ↔ ∀ i, (t i).Nonempty

Proof state:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
⊢ (univ.pi t).Nonempty ↔ ∀ (i : ι), (t i).Nonempty

Tactic:
simp [Classical.skolem, Set.Nonempty]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem hasFPowerSeriesOn_cauchy_integral {f : ℂ → E} {c : ℂ} {R : ℝ≥0}
    (hf : CircleIntegrable f c R) (hR : 0 < R) :
    HasFPowerSeriesOnBall (fun w => (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z)
      (cauchyPowerSeries f c R) c R :=
  { r_le := le_radius_cauchyPowerSeries _ _ _
    r_pos := ENNReal.coe_pos.2 hR
    hasSum := fun hy ↦ hasSum_cauchyPowerSeries_integral hf <| by simpa using hy }

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
hf : CircleIntegrable f c ↑R
hR : 0 < R
y✝ : ℂ
hy : y✝ ∈ EMetric.ball 0 ↑R
⊢ ‖y✝‖ < ↑R

Tactic:
simpa using hy

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma completedHurwitzZetaOdd_neg (a : UnitAddCircle) (s : ℂ) :
    completedHurwitzZetaOdd (-a) s = -completedHurwitzZetaOdd a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaOdd (-a) s = -completedHurwitzZetaOdd a s

Tactic:
simp [completedHurwitzZetaOdd, StrongFEPair.Λ, hurwitzOddFEPair, mellin, oddKernel_neg,
  integral_neg, neg_div]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem repr_range : LinearMap.range (b.repr : M →ₗ[R] ι →₀ R) = Finsupp.supported R R univ

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
⊢ LinearMap.range ↑b.repr = supported R R univ

Tactic:
rw [LinearEquiv.range, Finsupp.supported_univ]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_one (s) : ∫⁻ _ in s, 1 ∂μ = μ s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ∫⁻ (x : α) in s, 1 ∂μ = μ s

Tactic:
rw [setLIntegral_const, one_mul]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean
lemma unitization_norm_inr (x : A) : ‖(WithLp.equiv 1 (Unitization 𝕜 A)).symm x‖ = ‖x‖

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NonUnitalNormedRing A
inst✝ : NormedSpace 𝕜 A
x : A
⊢ ‖(WithLp.equiv 1 (Unitization 𝕜 A)).symm ↑x‖ = ‖x‖

Tactic:
simp [unitization_norm_def]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem self_add_star : a + star a = 2 * a.re

Proof state:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a + star a = 2 * ↑a.re

Tactic:
simp [a.self_add_star, Quaternion.coe]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.infinite_compl [Infinite α] {s : Set α} (hs : s.Finite) : sᶜ.Infinite := fun h =>
  Set.infinite_univ (α := α) (by simpa using hs.union h)

Proof state:
α : Type u
inst✝ : Infinite α
s : Set α
hs : s.Finite
h : sᶜ.Finite
⊢ univ.Finite

Tactic:
simpa using hs.union h

Result:
no goals
-- Mathlib/Order/Closure.lean
theorem closure_sup_closure (x y : α) : c (c x ⊔ c y) = c (x ⊔ y)

Proof state:
α : Type u_1
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ c (c x ⊔ c y) = c (x ⊔ y)

Tactic:
rw [closure_sup_closure_left, closure_sup_closure_right]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem preimage_coe_nonempty {s t : Set α} :
    (((↑) : s → α) ⁻¹' t).Nonempty ↔ (s ∩ t).Nonempty

Proof state:
α : Type u_1
s t : Set α
⊢ (val ⁻¹' t).Nonempty ↔ (s ∩ t).Nonempty

Tactic:
rw [← image_preimage_coe, image_nonempty]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma inr_snd :
    (Cochain.ofHom (inr φ)).comp (snd φ) (zero_add 0) = Cochain.ofHom (𝟙 G)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
⊢ (Cochain.ofHom (inr φ)).comp (snd φ) ⋯ = Cochain.ofHom (𝟙 G)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Prod.lean
theorem map_prodComm_antidiagonal [AddCommMonoid A] [HasAntidiagonal A] {n : A} :
    (antidiagonal n).map (Equiv.prodComm A A) = antidiagonal n :=
  Finset.ext fun ⟨a, b⟩ => by simp [add_comm]

Proof state:
A : Type u_1
inst✝¹ : AddCommMonoid A
inst✝ : HasAntidiagonal A
n : A
x✝ : A × A
a b : A
⊢ (a, b) ∈ map (Equiv.prodComm A A).toEmbedding (antidiagonal n) ↔ (a, b) ∈ antidiagonal n

Tactic:
simp [add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Power2.lean
theorem pos_of_isPowerOfTwo (h : isPowerOfTwo n) : n > 0

Proof state:
n : Nat
h✝ : n.isPowerOfTwo
k : Nat
h : n = 2 ^ k
⊢ n > 0

Tactic:
rw [h]

Result:
n : Nat
h✝ : n.isPowerOfTwo
k : Nat
h : n = 2 ^ k
⊢ 2 ^ k > 0

Proof state:
case h
n : Nat
h✝ : n.isPowerOfTwo
k : Nat
h : n = 2 ^ k
⊢ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
n : Nat
h✝ : n.isPowerOfTwo
k : Nat
h : n = 2 ^ k
⊢ 2 ^ k > 0

Tactic:
apply Nat.pos_pow_of_pos

Result:
case h
n : Nat
h✝ : n.isPowerOfTwo
k : Nat
h : n = 2 ^ k
⊢ 0 < 2

Proof state:
n : Nat
h : n.isPowerOfTwo
⊢ n > 0

Tactic:
have ⟨k, h⟩ := h

Result:
n : Nat
h✝ : n.isPowerOfTwo
k : Nat
h : n = 2 ^ k
⊢ n > 0
-- Mathlib/Analysis/Normed/Module/Basic.lean
theorem norm_zsmul (n : ℤ) (x : E) : ‖n • x‖ = ‖(n : 𝕜)‖ * ‖x‖

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℤ
x : E
⊢ ‖n • x‖ = ‖↑n‖ * ‖x‖

Tactic:
rw [← norm_smul, ← Int.smul_one_eq_cast, smul_assoc, one_smul]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem Filter.Tendsto.finCons
    {f : Y → π 0} {g : Y → ∀ j : Fin n, π j.succ} {l : Filter Y} {x : π 0} {y : ∀ j, π (Fin.succ j)}
    (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
    Tendsto (fun a => Fin.cons (f a) (g a)) l (𝓝 <| Fin.cons x y) :=
  tendsto_pi_nhds.2 fun j => Fin.cases (by simpa) (by simpa using tendsto_pi_nhds.1 hg) j

Proof state:
Y : Type v
n : ℕ
π : Fin (n + 1) → Type u_8
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (π i)
f : Y → π 0
g : Y → (j : Fin n) → π j.succ
l : Filter Y
x : π 0
y : (j : Fin n) → π j.succ
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ Tendsto (fun i => Fin.cons (f i) (g i) 0) l (𝓝 (Fin.cons x y 0))

Tactic:
simpa

Result:
no goals

Proof state:
Y : Type v
n : ℕ
π : Fin (n + 1) → Type u_8
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (π i)
f : Y → π 0
g : Y → (j : Fin n) → π j.succ
l : Filter Y
x : π 0
y : (j : Fin n) → π j.succ
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (i : Fin n), Tendsto (fun i_1 => Fin.cons (f i_1) (g i_1) i.succ) l (𝓝 (Fin.cons x y i.succ))

Tactic:
simpa using tendsto_pi_nhds.1 hg

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem linfty_opNNNorm_row (v : n → α) : ‖row ι v‖₊ = ∑ i, ‖v i‖₊

Proof state:
n : Type u_4
α : Type u_5
ι : Type u_7
inst✝² : Fintype n
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : n → α
⊢ ‖row ι v‖₊ = ∑ i : n, ‖v i‖₊

Tactic:
simp [linfty_opNNNorm_def]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negAddY_of_X_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) : W.negAddY P Q = -addU P Q

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W.negAddY P Q = -addU P Q

Tactic:
rw [addU, neg_div, neg_neg, ← mul_div_mul_right _ _ <| mul_ne_zero hPz hQz,
  ← negAddY_of_X_eq' hP hQ hx, ← sq,
  mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem extend_zero : γ.extend 0 = x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.extend 0 = x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/RestrictScalars.lean
theorem restrictScalars_eq_bot_iff {p : Submodule R M} : restrictScalars S p = ⊥ ↔ p = ⊥

Proof state:
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p : Submodule R M
⊢ restrictScalars S p = ⊥ ↔ p = ⊥

Tactic:
simp [SetLike.ext_iff]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem map_subtype_top : map p.subtype (⊤ : Submodule R p) = p

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ map p.subtype ⊤ = p

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem dist_map (x y : P) : dist (f x) (f y) = dist x y

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
x y : P
⊢ dist (f x) (f y) = dist x y

Tactic:
rw [dist_eq_norm_vsub V₂, dist_eq_norm_vsub V, ← map_vsub, f.linearIsometry.norm_map]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_diff_Iic : Ioc a b \ Iic c = Ioc (max a c) b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioc a b \ Iic c = Ioc (a ⊔ c) b

Tactic:
rw [diff_eq, compl_Iic, Ioc_inter_Ioi]

Result:
no goals
-- Mathlib/Order/UpperLower/LocallyFinite.lean
theorem Finite.upperClosure [LocallyFiniteOrderTop α] (hs : s.Finite) :
    (upperClosure s : Set α).Finite

Proof state:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderTop α
hs : s.Finite
⊢ (⋃ a ∈ s, Ici a).Finite

Tactic:
exact hs.biUnion fun _ _ => finite_Ici _

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderTop α
hs : s.Finite
⊢ (↑(upperClosure s)).Finite

Tactic:
rw [coe_upperClosure]

Result:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderTop α
hs : s.Finite
⊢ (⋃ a ∈ s, Ici a).Finite
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem isPell_star : ∀ {b : ℤ√d}, IsPell b ↔ IsPell (star b)
  | ⟨x, y⟩ => by simp [IsPell, Zsqrtd.star_mk]

Proof state:
d x y : ℤ
⊢ IsPell { re := x, im := y } ↔ IsPell (star { re := x, im := y })

Tactic:
simp [IsPell, Zsqrtd.star_mk]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem hasFDerivAt_comp_sub (a : E) :
    HasFDerivAt (fun x ↦ f (x - a)) f' x ↔ HasFDerivAt f f' (x - a)

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
f' : E →L[𝕜] F
x a : E
⊢ HasFDerivAt (fun x => f (x - a)) f' x ↔ HasFDerivAt f f' (x - a)

Tactic:
simp [← hasFDerivWithinAt_univ, hasFDerivWithinAt_comp_sub]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
/-- The root number of the unique Dirichlet character modulo 1 is 1. -/
lemma rootNumber_modOne (χ : DirichletCharacter ℂ 1) : rootNumber χ = 1

Proof state:
χ : DirichletCharacter ℂ 1
⊢ χ.rootNumber = 1

Tactic:
simp [rootNumber, gaussSum, -univ_unique, ← singleton_eq_univ (1 : ZMod 1),
  (show stdAddChar (1 : ZMod 1) = 1 from AddChar.map_zero_eq_one _),
  (show χ.Even from map_one _)]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Basic.lean
@[reassoc (attr := simp)]
lemma _root_.CategoryTheory.Iso.hom_inv_id_triangle_hom₃ {A B : Triangle C} (e : A ≅ B) :
    e.hom.hom₃ ≫ e.inv.hom₃ = 𝟙 _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ e.hom.hom₃ ≫ e.inv.hom₃ = 𝟙 A.obj₃

Tactic:
rw [← comp_hom₃, e.hom_inv_id, id_hom₃]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem star_mul_eq_coe : star a * a = (star a * a).re

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a * a = ↑(star a * a).re

Tactic:
ext <;> simp <;> ring

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup₂_eq_bot {f : ∀ i, κ i → α} : ⨆ (i) (j), f i j = ⊥ ↔ ∀ i j, f i j = ⊥

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j = ⊥ ↔ ∀ (i : ι) (j : κ i), f i j = ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem sigma_eq_of_eq_comp_cast {α : Type*} :
    ∀ {a b : Σii, Fin ii → α} (h : a.fst = b.fst), a.snd = b.snd ∘ Fin.cast h → a = b
  | ⟨ai, a⟩, ⟨bi, b⟩, hi, h => by
    dsimp only at hi
    subst hi
    simpa using h

Proof state:
α : Type u_1
ai : ℕ
a : Fin ai → α
bi : ℕ
b : Fin bi → α
hi : ai = bi
h : ⟨ai, a⟩.snd = ⟨bi, b⟩.snd ∘ Fin.cast hi
⊢ ⟨ai, a⟩ = ⟨bi, b⟩

Tactic:
subst hi

Result:
α : Type u_1
ai : ℕ
a b : Fin ai → α
h : ⟨ai, a⟩.snd = ⟨ai, b⟩.snd ∘ Fin.cast ⋯
⊢ ⟨ai, a⟩ = ⟨ai, b⟩

Proof state:
α : Type u_1
ai : ℕ
a : Fin ai → α
bi : ℕ
b : Fin bi → α
hi : ⟨ai, a⟩.fst = ⟨bi, b⟩.fst
h : ⟨ai, a⟩.snd = ⟨bi, b⟩.snd ∘ Fin.cast hi
⊢ ⟨ai, a⟩ = ⟨bi, b⟩

Tactic:
dsimp only at hi

Result:
α : Type u_1
ai : ℕ
a : Fin ai → α
bi : ℕ
b : Fin bi → α
hi : ai = bi
h : ⟨ai, a⟩.snd = ⟨bi, b⟩.snd ∘ Fin.cast hi
⊢ ⟨ai, a⟩ = ⟨bi, b⟩

Proof state:
α : Type u_1
ai : ℕ
a b : Fin ai → α
h : ⟨ai, a⟩.snd = ⟨ai, b⟩.snd ∘ Fin.cast ⋯
⊢ ⟨ai, a⟩ = ⟨ai, b⟩

Tactic:
simpa using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_flatten (p : α → Bool) (L : List (List α)) :
    filter p (flatten L) = flatten (map (filter p) L)

Proof state:
α : Type u_1
p : α → Bool
L : List (List α)
⊢ filter p L.flatten = (map (filter p) L).flatten

Tactic:
induction L <;> simp [*, filter_append]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem length_take_of_le (h : n ≤ length l) : length (take n l) = n

Proof state:
n : Nat
α✝ : Type u_1
l : List α✝
h : n ≤ l.length
⊢ (take n l).length = n

Tactic:
simp [Nat.min_eq_left h]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem mem_C'_eq_false : ∀ x, x ∈ C' C ho → x (term I ho) = false

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ ∀ x ∈ C' C ho, x (term I ho) = false

Tactic:
rintro x ⟨_, y, _, rfl⟩

Result:
case intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
y : I → Bool
left✝¹ : y ∈ C1 C ho
left✝ : Proj (fun x => ord I x < o) y ∈ C0 C ho
⊢ Proj (fun x => ord I x < o) y (term I ho) = false

Proof state:
case intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
y : I → Bool
left✝¹ : y ∈ C1 C ho
left✝ : Proj (fun x => ord I x < o) y ∈ C0 C ho
⊢ Proj (fun x => ord I x < o) y (term I ho) = false

Tactic:
simp only [Proj, ord_term_aux, lt_self_iff_false, ite_false]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem nsmul_toReal_eq_mul {n : ℕ} (h : n ≠ 0) {θ : Angle} :
    (n • θ).toReal = n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / n) (π / n)

Proof state:
n : ℕ
h : n ≠ 0
θ : Angle
⊢ (n • ↑θ.toReal).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)

Tactic:
have h' : 0 < (n : ℝ) := mod_cast Nat.pos_of_ne_zero h

Result:
n : ℕ
h : n ≠ 0
θ : Angle
h' : 0 < ↑n
⊢ (n • ↑θ.toReal).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)

Proof state:
n : ℕ
h : n ≠ 0
θ : Angle
⊢ (n • θ).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)

Tactic:
nth_rw 1 [← coe_toReal θ]

Result:
n : ℕ
h : n ≠ 0
θ : Angle
⊢ (n • ↑θ.toReal).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)

Proof state:
n : ℕ
h : n ≠ 0
θ : Angle
h' : 0 < ↑n
⊢ (n • ↑θ.toReal).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)

Tactic:
rw [← coe_nsmul, nsmul_eq_mul, toReal_coe_eq_self_iff, Set.mem_Ioc, div_lt_iff₀' h',
  le_div_iff₀' h']

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem piCongrLeft_symm_preimage_pi (f : ι' ≃ ι) (s : Set ι') (t : ∀ i, Set (α i)) :
    (f.piCongrLeft α).symm ⁻¹' s.pi (fun i' => t <| f i') = (f '' s).pi t

Proof state:
case h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
x✝ : (b : ι) → α b
⊢ (x✝ ∈ ⇑(piCongrLeft α f).symm ⁻¹' s.pi fun i' => t (f i')) ↔ x✝ ∈ (⇑f '' s).pi t

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ (⇑(piCongrLeft α f).symm ⁻¹' s.pi fun i' => t (f i')) = (⇑f '' s).pi t

Tactic:
ext

Result:
case h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
x✝ : (b : ι) → α b
⊢ (x✝ ∈ ⇑(piCongrLeft α f).symm ⁻¹' s.pi fun i' => t (f i')) ↔ x✝ ∈ (⇑f '' s).pi t
-- Mathlib/Order/CompleteLattice/SetLike.lean
@[simp] lemma mem_inf : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Proof state:
X : Type u_1
L : CompleteSublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Tactic:
simp [← mem_subtype]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AEDisjoint.lean
theorem _root_.Disjoint.aedisjoint (h : Disjoint s t) : AEDisjoint μ s t

Proof state:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : Disjoint s t
⊢ AEDisjoint μ s t

Tactic:
rw [AEDisjoint, disjoint_iff_inter_eq_empty.1 h, measure_empty]

Result:
no goals
-- Mathlib/Algebra/Star/Pointwise.lean
theorem star_subset [InvolutiveStar α] {s t : Set α} : s⋆ ⊆ t ↔ s ⊆ t⋆

Proof state:
α : Type u_1
inst✝ : InvolutiveStar α
s t : Set α
⊢ s⋆ ⊆ t ↔ s ⊆ t⋆

Tactic:
rw [← star_subset_star, star_star]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Rat.lean
@[simp] lemma abs_qsmul [Module ℚ α] [PosSMulMono ℚ α] (q : ℚ) (a : α) :
    |q • a| = |q| • |a|

Proof state:
α : Type u_1
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : Module ℚ α
inst✝ : PosSMulMono ℚ α
q : ℚ
a : α
⊢ |q • a| = |q| • |a|

Tactic:
obtain ha | ha := le_total a 0 <;> obtain hq | hq := le_total q 0 <;>
  simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos,
    smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
@[simp] lemma sqrt_zero : sqrt 0 = 0

Proof state:
⊢ sqrt 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem empty_def : (∅ : PSet) = ⟨_, PEmpty.elim⟩

Proof state:
⊢ ∅ = mk PEmpty.{u_1 + 1} PEmpty.elim

Tactic:
simp [EmptyCollection.emptyCollection, PSet.empty]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem _root_.Matrix.Nondegenerate.toLinearMap₂' {M : Matrix ι ι R₁} (h : M.Nondegenerate) :
    (Matrix.toLinearMap₂' R₁ M).SeparatingLeft (R := R₁) := fun x hx =>
  h.eq_zero_of_ortho fun y => by simpa only [toLinearMap₂'_apply'] using hx y

Proof state:
R₁ : Type u_2
ι : Type u_15
inst✝² : CommRing R₁
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
M : Matrix ι ι R₁
h : M.Nondegenerate
x : ι → R₁
hx : ∀ (y : ι → R₁), (((Matrix.toLinearMap₂' R₁) M) x) y = 0
y : ι → R₁
⊢ x ⬝ᵥ M *ᵥ y = 0

Tactic:
simpa only [toLinearMap₂'_apply'] using hx y

Result:
no goals
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem measure_union₀_aux (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ)
    (hd : AEDisjoint μ s t) : μ (s ∪ t) = μ s + μ t

Proof state:
case hd
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ Pairwise (AEDisjoint μ on fun b => bif b then s else t)

case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ ∀ (i : Bool), NullMeasurableSet (bif i then s else t) μ

Tactic:
exacts [(pairwise_on_bool AEDisjoint.symmetric).2 hd, fun b => Bool.casesOn b ht hs]

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ μ (s ∪ t) = μ s + μ t

Tactic:
rw [union_eq_iUnion, measure_iUnion₀, tsum_fintype, Fintype.sum_bool, cond, cond]

Result:
case hd
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ Pairwise (AEDisjoint μ on fun b => bif b then s else t)

case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ ∀ (i : Bool), NullMeasurableSet (bif i then s else t) μ