harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Insert.lean
theorem ssubset_singleton_iff {s : Finset α} {a : α} : s ⊂ {a} ↔ s = ∅

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ s ⊂ {a} ↔ s = ∅

Tactic:
rw [← coe_ssubset, coe_singleton, Set.ssubset_singleton_iff, coe_eq_empty]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem cos_arccos {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) : cos (arccos x) = x

Proof state:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arccos x) = x

Tactic:
rw [arccos, cos_pi_div_two_sub, sin_arcsin hx₁ hx₂]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `div_lt_iff₀` for a version with multiplication on the other side. -/
lemma div_lt_iff₀' (hc : 0 < c) : b / c < a ↔ b < c * a

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
hc : 0 < c
⊢ b / c < a ↔ b < c * a

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›

Result:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
hc : 0 < c
this : MulPosStrictMono G₀
⊢ b / c < a ↔ b < c * a

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
hc : 0 < c
this : MulPosStrictMono G₀
⊢ b / c < a ↔ b < c * a

Tactic:
rw [div_lt_iff₀ hc, mul_comm]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
lemma denest_nest : p.nest.denest .nest = p

Proof state:
p : DyckWord
⊢ ([U] ++ ↑p).tail = ↑p

Tactic:
rfl

Result:
no goals

Proof state:
p : DyckWord
⊢ p.nest.denest ⋯ = p

Tactic:
simp_rw [nest, denest, DyckWord.ext_iff, dropLast_concat]

Result:
p : DyckWord
⊢ ([U] ++ ↑p).tail = ↑p
-- Mathlib/RingTheory/Ideal/Span.lean
theorem span_one : span (1 : Set α) = ⊤

Proof state:
α : Type u
inst✝ : Semiring α
⊢ span 1 = ⊤

Tactic:
rw [← Set.singleton_one, span_singleton_one]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Icc_sub_one_right_eq_Ico (a b : α) : Icc a (b - 1) = Ico a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Icc a (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Icc_pred_right_eq_Ico a b

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_0 : (0 : MvPolynomial σ R).vars = ∅

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ vars 0 = ∅

Tactic:
classical rw [vars_def, degrees_zero, Multiset.toFinset_zero]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ vars 0 = ∅

Tactic:
rw [vars_def, degrees_zero, Multiset.toFinset_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_zero_measure {m : MeasurableSpace α} (f : α → ℝ≥0∞) :
    ∫⁻ a, f a ∂(0 : Measure α) = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂0 = 0

Tactic:
simp [lintegral]

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
lemma StrictMono.map_isGreatest (hf : StrictMono f) :
    IsGreatest (f '' s) (f a) ↔ IsGreatest s a

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictMono f
⊢ IsGreatest (f '' s) (f a) ↔ IsGreatest s a

Tactic:
simp [IsGreatest, hf.injective.eq_iff, hf.mem_upperBounds_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem extract_loop_eq (as bs : Array α) (size start : Nat) (h : start + size ≤ as.size) :
  extract.loop as size start bs = bs ++ as.extract start (start + size)

Proof state:
α : Type u_1
as bs : Array α
size start : Nat
h : start + size ≤ as.size
⊢ extract.loop as size start bs = bs ++ extract.loop as (min (start + size) as.size - start) start #[]

Tactic:
rw [extract_loop_eq_aux, Nat.min_eq_left h, Nat.add_sub_cancel_left]

Result:
no goals

Proof state:
α : Type u_1
as bs : Array α
size start : Nat
h : start + size ≤ as.size
⊢ extract.loop as size start bs = bs ++ as.extract start (start + size)

Tactic:
simp only [extract, Nat.sub_eq, mkEmpty_eq]

Result:
α : Type u_1
as bs : Array α
size start : Nat
h : start + size ≤ as.size
⊢ extract.loop as size start bs = bs ++ extract.loop as (min (start + size) as.size - start) start #[]
-- Mathlib/Data/Num/Lemmas.lean
theorem of_to_nat' : ∀ n : PosNum, Num.ofNat' (n : ℕ) = Num.pos n
  | 1 => by erw [@Num.ofNat'_bit true 0, Num.ofNat'_zero]; rfl
  | bit0 p => by
      simpa only [Nat.bit_false, cond_false, two_mul, of_to_nat' p] using Num.ofNat'_bit false p
  | bit1 p => by
      simpa only [Nat.bit_true, cond_true, two_mul, of_to_nat' p] using Num.ofNat'_bit true p

Proof state:
⊢ (bif true then Num.bit1 else Num.bit0) 0 = Num.pos 1

Tactic:
rfl

Result:
no goals

Proof state:
p : PosNum
⊢ Num.ofNat' ↑p.bit0 = Num.pos p.bit0

Tactic:
simpa only [Nat.bit_false, cond_false, two_mul, of_to_nat' p] using Num.ofNat'_bit false p

Result:
no goals

Proof state:
⊢ Num.ofNat' ↑1 = Num.pos 1

Tactic:
erw [@Num.ofNat'_bit true 0, Num.ofNat'_zero]

Result:
⊢ (bif true then Num.bit1 else Num.bit0) 0 = Num.pos 1

Proof state:
p : PosNum
⊢ Num.ofNat' ↑p.bit1 = Num.pos p.bit1

Tactic:
simpa only [Nat.bit_true, cond_true, two_mul, of_to_nat' p] using Num.ofNat'_bit true p

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem support_smul_subset_vadd_support [MulZeroClass R] [SMulWithZero R V] {x : HahnSeries Γ R}
    {y : HahnModule Γ' R V} :
    ((of R).symm (x • y)).support ⊆ x.support +ᵥ ((of R).symm y).support

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
⊢ ((of R).symm (x • y)).support ⊆ x.support +ᵥ ((of R).symm y).support

Tactic:
have h : x.support +ᵥ ((of R).symm y).support =
    x.support +ᵥ ((of R).symm y).support := by
  exact rfl

Result:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
h : x.support +ᵥ ((of R).symm y).support = x.support +ᵥ ((of R).symm y).support
⊢ ((of R).symm (x • y)).support ⊆ x.support +ᵥ ((of R).symm y).support

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
⊢ x.support +ᵥ ((of R).symm y).support = x.support +ᵥ ((of R).symm y).support

Tactic:
exact rfl

Result:
no goals

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
h : x.support +ᵥ ((of R).symm y).support = x.support +ᵥ ((of R).symm y).support
⊢ ((of R).symm (x • y)).support ⊆ x.support +ᵥ ((of R).symm y).support

Tactic:
exact support_smul_subset_vadd_support'

Result:
no goals
-- Mathlib/Algebra/Order/Group/Finset.lean
/-- Also see `Finset.add_sup'` that works for ordered groups. -/
lemma add_sup'' (hs : s.Nonempty) (f : ι → M) (a : M) :
    a + s.sup' hs f = s.sup' hs fun i ↦ a + f i

Proof state:
ι : Type u_1
M : Type u_3
inst✝⁴ : LinearOrderedAddCommMonoid M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
hs : s.Nonempty
f : ι → M
a : M
⊢ a + s.sup' hs f = s.sup' hs fun i => a + f i

Tactic:
simp_rw [add_comm a, Finset.sup'_add']

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
/-- Post-composing an additive character to `ℂ` with complex conjugation gives the inverse
character. -/
lemma starComp_eq_inv (hR : 0 < ringChar R) {φ : AddChar R ℂ} :
    (starRingEnd ℂ).compAddChar φ = φ⁻¹

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
H : ‖↑⋯.unit‖ = 1
⊢ (starRingEnd ℂ) (φ a) = (φ a)⁻¹

Tactic:
exact (Complex.inv_eq_conj H).symm

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
⊢ (↑(starRingEnd ℂ)).compAddChar φ = φ⁻¹

Tactic:
ext1 a

Result:
case h
R : Type u_1
inst✝ : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
⊢ ((↑(starRingEnd ℂ)).compAddChar φ) a = φ⁻¹ a

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
⊢ (starRingEnd ℂ) (φ a) = (φ a)⁻¹

Tactic:
have H := Complex.norm_eq_one_of_mem_rootsOfUnity <| φ.val_mem_rootsOfUnity a hR

Result:
case h
R : Type u_1
inst✝ : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
H : ‖↑⋯.unit‖ = 1
⊢ (starRingEnd ℂ) (φ a) = (φ a)⁻¹

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
⊢ ((↑(starRingEnd ℂ)).compAddChar φ) a = φ⁻¹ a

Tactic:
simp only [RingHom.toMonoidHom_eq_coe, MonoidHom.coe_compAddChar, MonoidHom.coe_coe,
  Function.comp_apply, inv_apply']

Result:
case h
R : Type u_1
inst✝ : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
⊢ (starRingEnd ℂ) (φ a) = (φ a)⁻¹
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem mk_eq_of_comm {B A : C} {X : Subobject B} (f : A ⟶ B) [Mono f] (i : A ≅ (X : C))
    (w : i.hom ≫ X.arrow = f) : mk f = X :=
  Eq.symm <| eq_mk_of_comm _ i.symm <| by rw [Iso.symm_hom, Iso.inv_comp_eq, w]

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
i : A ≅ underlying.obj X
w : i.hom ≫ X.arrow = f
⊢ i.symm.hom ≫ f = X.arrow

Tactic:
rw [Iso.symm_hom, Iso.inv_comp_eq, w]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc (attr := simp)]
lemma associativity (X Y Z : C) :
    δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
    F.map (α_ X Y Z).hom ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z

Tactic:
apply oplax_associativity'

Result:
no goals
-- Mathlib/CategoryTheory/LiftingProperties/Adjunction.lean
theorem left_adjoint_hasLift_iff : HasLift (sq.left_adjoint adj) ↔ HasLift sq

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ ⋯.HasLift ↔ sq.HasLift

Tactic:
simp only [HasLift.iff]

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ Nonempty ⋯.LiftStruct ↔ Nonempty sq.LiftStruct

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ Nonempty ⋯.LiftStruct ↔ Nonempty sq.LiftStruct

Tactic:
exact Equiv.nonempty_congr (sq.leftAdjointLiftStructEquiv adj).symm

Result:
no goals
-- Mathlib/RingTheory/Derivation/Basic.lean
theorem leibniz_inv (a : K) : D a⁻¹ = -a⁻¹ ^ 2 • D a

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
⊢ D a⁻¹ = -a⁻¹ ^ 2 • D a

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Result:
case inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
⊢ D 0⁻¹ = -0⁻¹ ^ 2 • D 0

case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
ha : a ≠ 0
⊢ D a⁻¹ = -a⁻¹ ^ 2 • D a

Proof state:
case inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
⊢ D 0⁻¹ = -0⁻¹ ^ 2 • D 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
ha : a ≠ 0
⊢ D a⁻¹ = -a⁻¹ ^ 2 • D a

Tactic:
exact D.leibniz_of_mul_eq_one (inv_mul_cancel₀ ha)

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extChartAt_preimage_mem_nhds {x : M} (ht : t ∈ 𝓝 x) :
    (extChartAt I x).symm ⁻¹' t ∈ 𝓝 ((extChartAt I x) x)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
t : Set M
inst✝ : ChartedSpace H M
x : M
ht : t ∈ 𝓝 x
⊢ ↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝 (↑(extChartAt I x) x)

Tactic:
apply (continuousAt_extChartAt_symm x).preimage_mem_nhds

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
t : Set M
inst✝ : ChartedSpace H M
x : M
ht : t ∈ 𝓝 x
⊢ t ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
t : Set M
inst✝ : ChartedSpace H M
x : M
ht : t ∈ 𝓝 x
⊢ t ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))

Tactic:
rwa [(extChartAt I x).left_inv (mem_extChartAt_source _)]

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIsoAt_iff' (f : K ⟶ L) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
    [K.HasHomology j] [L.HasHomology j] [(K.sc' i j k).HasHomology] [(L.sc' i j k).HasHomology] :
    QuasiIsoAt f j ↔
      ShortComplex.QuasiIso ((shortComplexFunctor' C c i j k).map f)

Proof state:
ι : Type u_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.sc' i j k).HasHomology
inst✝ : (L.sc' i j k).HasHomology
⊢ QuasiIsoAt f j ↔ ShortComplex.QuasiIso ((shortComplexFunctor' C c i j k).map f)

Tactic:
rw [quasiIsoAt_iff]

Result:
ι : Type u_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.sc' i j k).HasHomology
inst✝ : (L.sc' i j k).HasHomology
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map f) ↔
    ShortComplex.QuasiIso ((shortComplexFunctor' C c i j k).map f)

Proof state:
ι : Type u_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.sc' i j k).HasHomology
inst✝ : (L.sc' i j k).HasHomology
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map f) ↔
    ShortComplex.QuasiIso ((shortComplexFunctor' C c i j k).map f)

Tactic:
exact ShortComplex.quasiIso_iff_of_arrow_mk_iso _ _
  (Arrow.isoOfNatIso (natIsoSc' C c i j k hi hk) (Arrow.mk f))

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem monomial_mul_C : monomial n a * C b = monomial n (a * b)

Proof state:
R : Type u
a b : R
n : ℕ
inst✝ : Semiring R
⊢ (monomial n) a * C b = (monomial n) (a * b)

Tactic:
simp only [← monomial_zero_left, monomial_mul_monomial, add_zero]

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_filter_le_of_le_left [DecidablePred (c ≤ ·)] (hca : c ≤ a) :
    ((Ico a b).filter fun x => c ≤ x) = Ico a b

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => c ≤ x
hca : c ≤ a
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico a b

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_le_left hca]

Result:
no goals
-- Mathlib/Order/KonigLemma.lean
theorem exists_seq_covby_of_forall_covby_finite (hfin : ∀ (a : α), {x | a ⋖ x}.Finite)
    (hb : (Ici b).Infinite) : ∃ f : ℕ → α, f 0 = b ∧ ∀ i, f i ⋖ f (i+1) :=
  let h := fun a : {a : α // (Ici a).Infinite} ↦
    exists_covby_infinite_Ici_of_infinite_Ici a.2 (hfin a)
  let ks : ℕ → {a : α // (Ici a).Infinite} := Nat.rec ⟨b, hb⟩ fun _ a ↦ ⟨_, (h a).choose_spec.2⟩
  ⟨fun i ↦ (ks i).1, by simp [ks], fun i ↦ by simpa using (h (ks i)).choose_spec.1⟩

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
hb : (Ici b).Infinite
h : ∀ (a : { a // (Ici a).Infinite }), ∃ b, ↑a ⋖ b ∧ (Ici b).Infinite :=
  fun a => exists_covby_infinite_Ici_of_infinite_Ici a.property (hfin ↑a)
ks : ℕ → { a // (Ici a).Infinite } := fun t => Nat.rec ⟨b, hb⟩ (fun x a => ⟨⋯.choose, ⋯⟩) t
i : ℕ
⊢ (fun i => ↑(ks i)) i ⋖ (fun i => ↑(ks i)) (i + 1)

Tactic:
simpa using (h (ks i)).choose_spec.1

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
hb : (Ici b).Infinite
h : ∀ (a : { a // (Ici a).Infinite }), ∃ b, ↑a ⋖ b ∧ (Ici b).Infinite :=
  fun a => exists_covby_infinite_Ici_of_infinite_Ici a.property (hfin ↑a)
ks : ℕ → { a // (Ici a).Infinite } := fun t => Nat.rec ⟨b, hb⟩ (fun x a => ⟨⋯.choose, ⋯⟩) t
⊢ (fun i => ↑(ks i)) 0 = b

Tactic:
simp [ks]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_ite_eq_of_mem' [DecidableEq α] (s : Finset α) (a : α) (b : α → β) (h : a ∈ s) :
    (∏ x ∈ s, if x = a then b x else 1) = b a

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : α → β
h : a ∈ s
⊢ (∏ x ∈ s, if x = a then b x else 1) = b a

Tactic:
simp only [prod_ite_eq', if_pos h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem cokernel.desc_zero {W : C} {h} : cokernel.desc f (0 : Y ⟶ W) h = 0

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
W : C
h : f ≫ 0 = 0
⊢ coequalizer.π f 0 ≫ desc f 0 h = coequalizer.π f 0 ≫ 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
W : C
h : f ≫ 0 = 0
⊢ desc f 0 h = 0

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
W : C
h : f ≫ 0 = 0
⊢ coequalizer.π f 0 ≫ desc f 0 h = coequalizer.π f 0 ≫ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attach_eq_empty_iff {l : Array α} : l.attach = #[] ↔ l = #[]

Proof state:
α : Type u_1
l : Array α
⊢ l.attach = #[] ↔ l = #[]

Tactic:
cases l

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.attach = #[] ↔ { toList := toList✝ } = #[]

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.attach = #[] ↔ { toList := toList✝ } = #[]

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
lemma log_smul {r : ℝ} (a : A) (ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x) (hr : 0 < r)
    (ha₁ : IsSelfAdjoint a

Proof state:
case h.h
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
r : ℝ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
hr : 0 < r
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
x : ℝ
hx : x ∈ spectrum ℝ a
h : 0 < x
⊢ x ≠ 0

Tactic:
exact h.ne'

Result:
no goals

Proof state:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
r : ℝ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
hr : 0 < r
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
⊢ ∀ x ∈ spectrum ℝ a, x ≠ 0

Tactic:
peel ha₂ with x hx h

Result:
case h.h
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
r : ℝ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
hr : 0 < r
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
x : ℝ
hx : x ∈ spectrum ℝ a
h : 0 < x
⊢ x ≠ 0

Proof state:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
r : ℝ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
hr : 0 < r
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
⊢ log (r • a) = (algebraMap ℝ A) (Real.log r) + log a

Tactic:
have : ∀ x ∈ spectrum ℝ a, x ≠ 0 := by peel ha₂ with x hx h; exact h.ne'

Result:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
r : ℝ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
hr : 0 < r
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
this : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ log (r • a) = (algebraMap ℝ A) (Real.log r) + log a

Proof state:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
r : ℝ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x
hr : 0 < r
ha₁ : autoParam (IsSelfAdjoint a) _auto✝
this : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ cfc (fun z => Real.log r + Real.log z) a = (algebraMap ℝ A) (Real.log r) + cfc Real.log a

Tactic:
rw [cfc_const_add _ _ _]

Result:
no goals
-- Mathlib/Data/Nat/BitIndices.lean
theorem bitIndices_zero : bitIndices 0 = []

Proof state:
⊢ bitIndices 0 = []

Tactic:
simp [bitIndices]

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem sSupIndep_singleton (a : α) : sSupIndep ({a} : Set α) := fun i hi ↦ by
  simp_all

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
a i : α
hi : i ∈ {a}
⊢ Disjoint i (sSup ({a} \ {i}))

Tactic:
simp_all

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem map_coe (γ : Path x y) {f : X → Y} (h : Continuous f) :
    (γ.map h : I → Y) = f ∘ γ

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
γ : Path x y
f : X → Y
h : Continuous f
⊢ ⇑(γ.map h) = f ∘ ⇑γ

Tactic:
ext t

Result:
case h
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
γ : Path x y
f : X → Y
h : Continuous f
t : ↑I
⊢ (γ.map h) t = (f ∘ ⇑γ) t

Proof state:
case h
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
γ : Path x y
f : X → Y
h : Continuous f
t : ↑I
⊢ (γ.map h) t = (f ∘ ⇑γ) t

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_mul_prod_comm (f g h i : α → β) :
    (∏ a ∈ s, f a * g a) * ∏ a ∈ s, h a * i a = (∏ a ∈ s, f a * h a) * ∏ a ∈ s, g a * i a

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
inst✝ : CommMonoid β
f g h i : α → β
⊢ (∏ a ∈ s, f a * g a) * ∏ a ∈ s, h a * i a = (∏ a ∈ s, f a * h a) * ∏ a ∈ s, g a * i a

Tactic:
simp_rw [prod_mul_distrib, mul_mul_mul_comm]

Result:
no goals