harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/MyhillNerode.lean
theorem IsRegular.finite_range_leftQuotient (h : L.IsRegular) :
    (Set.range L.leftQuotient).Finite

Proof state:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
x : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ (Set.range (M.acceptsFrom ∘ M.eval)).Finite

Tactic:
exact Set.finite_of_finite_preimage (Set.toFinite _)
  (Set.range_comp_subset_range M.eval M.acceptsFrom)

Result:
no goals

Proof state:
α : Type u
L : Language α
h : L.IsRegular
⊢ (Set.range L.leftQuotient).Finite

Tactic:
have ⟨σ, x, M, hM⟩ := h

Result:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
x : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ (Set.range L.leftQuotient).Finite

Proof state:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
x : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ (Set.range L.leftQuotient).Finite

Tactic:
rw [← hM, leftQuotient_accepts]

Result:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
x : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ (Set.range (M.acceptsFrom ∘ M.eval)).Finite
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem map_zero : Q 0 = 0

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
⊢ Q 0 = 0

Tactic:
rw [← @zero_smul R _ _ _ _ (0 : M), map_smul, zero_mul, zero_smul]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem leadingCoeff_neg {f : MvPolynomial σ R} :
    m.leadingCoeff (-f) = - m.leadingCoeff f

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.leadingCoeff (-f) = -m.leadingCoeff f

Tactic:
simp only [leadingCoeff, degree_neg, coeff_neg]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem arcsin_eq_arctan {x : ℝ} (h : x ∈ Ioo (-(1 : ℝ)) 1) :
    arcsin x = arctan (x / √(1 - x ^ 2))

Proof state:
x : ℝ
h : x ∈ Ioo (-1) 1
⊢ arcsin x = arctan (x / √(1 - x ^ 2))

Tactic:
rw_mod_cast [arctan_eq_arcsin, div_pow, sq_sqrt, one_add_div, div_div, ← sqrt_mul,
  mul_div_cancel₀, sub_add_cancel, sqrt_one, div_one] <;> simp at h <;> nlinarith [h.1, h.2]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Path.lean
lemma hom_heq_of_cons_eq_cons {p : Path a b} {p' : Path a c}
    {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : HEq e e'

Proof state:
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
p' : Path a c
e : b ⟶ d
e' : c ⟶ d
h : p.cons e = p'.cons e'
⊢ HEq e e'

Tactic:
injection h

Result:
no goals
-- Mathlib/LinearAlgebra/Orientation.lean
theorem orientation_comp_linearEquiv_eq_neg_iff_det_neg (e : Basis ι R M) (f : M ≃ₗ[R] M) :
    (e.map f).orientation = -e.orientation ↔ LinearMap.det (f : M →ₗ[R] M) < 0

Proof state:
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
f : M ≃ₗ[R] M
⊢ (e.map f).orientation = -e.orientation ↔ LinearMap.det ↑f < 0

Tactic:
rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_neg_iff,
  LinearEquiv.coe_det]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_and : eval .and = ((· &&& ·) : BitVec w → BitVec w → BitVec w)

Proof state:
w : Nat
⊢ and.eval = fun x1 x2 => x1 &&& x2

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Setoid/Partition.lean
theorem proj_fiber (x : hs.Quotient) : hs.proj ⁻¹' {x} = s (hs.equivQuotient.symm x) :=
  Quotient.inductionOn' x fun x => by
    ext y
    simp only [Set.mem_preimage, Set.mem_singleton_iff, hs.mem_iff_index_eq]
    exact Quotient.eq''

Proof state:
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : hs.Quotient
x y : α
⊢ y ∈ hs.proj ⁻¹' {Quotient.mk'' x} ↔ y ∈ s (hs.equivQuotient.symm (Quotient.mk'' x))

Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff, hs.mem_iff_index_eq]

Result:
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : hs.Quotient
x y : α
⊢ hs.proj y = Quotient.mk'' x ↔ hs.index y = hs.equivQuotient.symm (Quotient.mk'' x)

Proof state:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : hs.Quotient
x : α
⊢ hs.proj ⁻¹' {Quotient.mk'' x} = s (hs.equivQuotient.symm (Quotient.mk'' x))

Tactic:
ext y

Result:
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : hs.Quotient
x y : α
⊢ y ∈ hs.proj ⁻¹' {Quotient.mk'' x} ↔ y ∈ s (hs.equivQuotient.symm (Quotient.mk'' x))

Proof state:
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : hs.Quotient
x y : α
⊢ hs.proj y = Quotient.mk'' x ↔ hs.index y = hs.equivQuotient.symm (Quotient.mk'' x)

Tactic:
exact Quotient.eq''

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem sizeUpTo_le (i : ℕ) : c.sizeUpTo i ≤ n

Proof state:
n : ℕ
c : Composition n
i : ℕ
⊢ c.sizeUpTo i ≤ n

Tactic:
conv_rhs => rw [← c.blocks_sum, ← sum_take_add_sum_drop _ i]

Result:
n : ℕ
c : Composition n
i : ℕ
⊢ c.sizeUpTo i ≤ (take i c.blocks).sum + (drop i c.blocks).sum

Proof state:
n : ℕ
c : Composition n
i : ℕ
⊢ c.sizeUpTo i ≤ (take i c.blocks).sum + (drop i c.blocks).sum

Tactic:
exact Nat.le_add_right _ _

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem exists_bilinForm_self_ne_zero [htwo : Invertible (2 : R)] {B : BilinForm R M}
    (hB₁ : B ≠ 0) (hB₂ : B.IsSymm) : ∃ x, ¬B.IsOrtho x x

Proof state:
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
hB₁ : B ≠ 0
hB₂ : IsSymm B
⊢ ∃ x, ¬IsOrtho B x x

Tactic:
lift B to QuadraticForm R M using hB₂ with Q

Result:
case intro
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
Q : QuadraticMap R M R
hB₁✝ hB₁ : (QuadraticMap.associatedHom ℕ) Q ≠ 0
⊢ ∃ x, ¬IsOrtho ((QuadraticMap.associatedHom ℕ) Q) x x

Proof state:
case intro.intro
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
Q : QuadraticMap R M R
hB₁✝ hB₁ : (QuadraticMap.associatedHom ℕ) Q ≠ 0
x : M
hx : Q x ≠ 0
⊢ ∃ x, ¬IsOrtho ((QuadraticMap.associatedHom ℕ) Q) x x

Tactic:
exact ⟨x, fun h => hx (Q.associated_eq_self_apply ℕ x ▸ h)⟩

Result:
no goals

Proof state:
case intro
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
Q : QuadraticMap R M R
hB₁✝ hB₁ : (QuadraticMap.associatedHom ℕ) Q ≠ 0
⊢ ∃ x, ¬IsOrtho ((QuadraticMap.associatedHom ℕ) Q) x x

Tactic:
obtain ⟨x, hx⟩ := QuadraticMap.exists_quadraticMap_ne_zero hB₁

Result:
case intro.intro
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
Q : QuadraticMap R M R
hB₁✝ hB₁ : (QuadraticMap.associatedHom ℕ) Q ≠ 0
x : M
hx : Q x ≠ 0
⊢ ∃ x, ¬IsOrtho ((QuadraticMap.associatedHom ℕ) Q) x x
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousOn_rpow_const {r : ℝ} {s : Set ℝ≥0}
    (h : 0 ∉ s ∨ 0 ≤ r) : ContinuousOn (fun z : ℝ≥0 => z ^ r) s :=
  h.elim (fun _ ↦ ContinuousOn.mono (s := {0}ᶜ) (by fun_prop) (by aesop))
    (NNReal.continuous_rpow_const · |>.continuousOn)

Proof state:
r : ℝ
s : Set ℝ≥0
h : 0 ∉ s ∨ 0 ≤ r
x✝ : 0 ∉ s
⊢ ContinuousOn (fun z => z ^ r) {0}ᶜ

Tactic:
fun_prop

Result:
no goals

Proof state:
r : ℝ
s : Set ℝ≥0
h : 0 ∉ s ∨ 0 ≤ r
x✝ : 0 ∉ s
⊢ s ⊆ {0}ᶜ

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_keys_eq_isEmpty (l : List ((a : α) × β a)) : (keys l).isEmpty = l.isEmpty

Proof state:
α : Type u
β : α → Type v
l : List ((a : α) × β a)
⊢ (keys l).isEmpty = l.isEmpty

Tactic:
induction l using assoc_induction <;> simp_all

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Arsinh.lean
theorem hasStrictDerivAt_arsinh (x : ℝ) : HasStrictDerivAt arsinh (√(1 + x ^ 2))⁻¹ x

Proof state:
case h.e'_9.h.e'_3
x : ℝ
⊢ √(1 + x ^ 2) = cosh (↑sinhHomeomorph.toPartialHomeomorph.symm x)

Tactic:
exact (cosh_arsinh _).symm

Result:
no goals

Proof state:
x : ℝ
⊢ HasStrictDerivAt arsinh (√(1 + x ^ 2))⁻¹ x

Tactic:
convert sinhHomeomorph.toPartialHomeomorph.hasStrictDerivAt_symm (mem_univ x) (cosh_pos _).ne'
  (hasStrictDerivAt_sinh _) using 2

Result:
case h.e'_9.h.e'_3
x : ℝ
⊢ √(1 + x ^ 2) = cosh (↑sinhHomeomorph.toPartialHomeomorph.symm x)
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem lt_antisymm {s₁ s₂ : String} (h₁ : ¬s₁ < s₂) (h₂ : ¬s₂ < s₁) : s₁ = s₂

Proof state:
s₁ s₂ : String
h₁ : s₂ ≤ s₁
h₂ : s₁ ≤ s₂
⊢ s₁ = s₂

Tactic:
exact String.le_antisymm h₂ h₁

Result:
no goals

Proof state:
s₁ s₂ : String
h₁ : ¬s₁ < s₂
h₂ : ¬s₂ < s₁
⊢ s₁ = s₂

Tactic:
simp at h₁ h₂

Result:
s₁ s₂ : String
h₁ : s₂ ≤ s₁
h₂ : s₁ ≤ s₂
⊢ s₁ = s₂
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem rootMultiplicity_X_sub_C_pow [Nontrivial R] (a : R) (n : ℕ) :
    rootMultiplicity a ((X - C a) ^ n) = n

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
n : ℕ
⊢ rootMultiplicity a ((X - C a) ^ n) = n

Tactic:
have := rootMultiplicity_mul_X_sub_C_pow (a := a) (n := n) C.map_one_ne_zero

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
n : ℕ
this : rootMultiplicity a (C 1 * (X - C a) ^ n) = rootMultiplicity a (C 1) + n
⊢ rootMultiplicity a ((X - C a) ^ n) = n

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
n : ℕ
this : rootMultiplicity a (C 1 * (X - C a) ^ n) = rootMultiplicity a (C 1) + n
⊢ rootMultiplicity a ((X - C a) ^ n) = n

Tactic:
rwa [rootMultiplicity_C, map_one, one_mul, zero_add] at this

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_equiv_iff {x y : PGame} : (-x ≈ y) ↔ (x ≈ -y)

Proof state:
x y : PGame
⊢ -x ≈ y ↔ x ≈ -y

Tactic:
rw [← neg_neg y, neg_equiv_neg_iff, neg_neg]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem sub_one_wcovBy (x : α) : x - 1 ⩿ x

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
x : α
⊢ x - 1 ⩿ x

Tactic:
rw [← pred_eq_sub_one]

Result:
α : Type u_1
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
x : α
⊢ pred x ⩿ x

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
x : α
⊢ pred x ⩿ x

Tactic:
exact pred_wcovBy x

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem div_ae_eq_one {β} [Group β] (f g : α → β) : f / g =ᵐ[μ] 1 ↔ f =ᵐ[μ] g

Proof state:
case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f =ᶠ[ae μ] g
x : α
hx : f x = g x
⊢ (f / g) x = 1 x

Tactic:
rwa [Pi.div_apply, Pi.one_apply, div_eq_one]

Result:
no goals

Proof state:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f / g =ᶠ[ae μ] 1
x : α
hx : (f / g) x = 1 x
⊢ f x = g x

Tactic:
rwa [Pi.div_apply, Pi.one_apply, div_eq_one] at hx

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
⊢ f / g =ᶠ[ae μ] 1 ↔ f =ᶠ[ae μ] g

Tactic:
refine ⟨fun h ↦ h.mono fun x hx ↦ ?_, fun h ↦ h.mono fun x hx ↦ ?_⟩

Result:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f / g =ᶠ[ae μ] 1
x : α
hx : (f / g) x = 1 x
⊢ f x = g x

case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f =ᶠ[ae μ] g
x : α
hx : f x = g x
⊢ (f / g) x = 1 x
-- Mathlib/Data/Seq/Seq.lean
theorem map_join (f : α → β) : ∀ S, map f (join S) = join (map (map f) S)
  | ((a, s), S) => by cases s <;> simp [map]

Proof state:
α : Type u
β : Type v
f : α → β
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ map f (join ((a, s), S)) = (map (map f) ((a, s), S)).join

Tactic:
cases s <;> simp [map]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma associator_hom_snd_snd (X Y Z : C) :
    (α_ X Y Z).hom ≫ snd _ _ ≫ snd _ _ = snd _ _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z : C
⊢ Limits.BinaryFan.snd (product (product X Y).cone.pt Z).cone = snd (X ⊗ Y) Z

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z : C
⊢ (α_ X Y Z).hom ≫ snd X (Y ⊗ Z) ≫ snd Y Z = snd (X ⊗ Y) Z

Tactic:
erw [lift_snd_assoc, lift_snd]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z : C
⊢ Limits.BinaryFan.snd (product (product X Y).cone.pt Z).cone = snd (X ⊗ Y) Z
-- Mathlib/Data/Set/Basic.lean
theorem Eq.subset {α} {s t : Set α} : s = t → s ⊆ t :=
  fun h₁ _ h₂ => by rw [← h₁]; exact h₂

Proof state:
α : Type u_1
s t : Set α
h₁ : s = t
x✝ : α
h₂ : x✝ ∈ s
⊢ x✝ ∈ t

Tactic:
rw [← h₁]

Result:
α : Type u_1
s t : Set α
h₁ : s = t
x✝ : α
h₂ : x✝ ∈ s
⊢ x✝ ∈ s

Proof state:
α : Type u_1
s t : Set α
h₁ : s = t
x✝ : α
h₂ : x✝ ∈ s
⊢ x✝ ∈ s

Tactic:
exact h₂

Result:
no goals
-- Mathlib/CategoryTheory/Category/Cat/Limit.lean
theorem limit_π_homDiagram_eqToHom {F : J ⥤ Cat.{v, v}} (X Y : limit (F ⋙ Cat.objects.{v, v}))
    (j : J) (h : X = Y) :
    limit.π (homDiagram X Y) j (eqToHom h) =
      eqToHom (congr_arg (limit.π (F ⋙ Cat.objects.{v, v}) j) h)

Proof state:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X : limit (F ⋙ objects)
j : J
⊢ limit.π (homDiagram X X) j (eqToHom ⋯) = eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
j : J
h : X = Y
⊢ limit.π (homDiagram X Y) j (eqToHom h) = eqToHom ⋯

Tactic:
subst h

Result:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X : limit (F ⋙ objects)
j : J
⊢ limit.π (homDiagram X X) j (eqToHom ⋯) = eqToHom ⋯
-- Mathlib/ModelTheory/Substructures.lean
theorem comap_id (S : L.Substructure P) : S.comap (Hom.id _ _) = S :=
  ext (by simp)

Proof state:
L : Language
P : Type u_2
inst✝ : L.Structure P
S : L.Substructure P
⊢ ∀ (x : P), x ∈ comap (Hom.id L P) S ↔ x ∈ S

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_mul_nat_iff : Irrational (x * n) ↔ n ≠ 0 ∧ Irrational x

Proof state:
n : ℕ
x : ℝ
⊢ Irrational (x * ↑n) ↔ n ≠ 0 ∧ Irrational x

Tactic:
rw [← cast_natCast, irrational_mul_rat_iff, Nat.cast_ne_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem map_rightUnitor_inv (X : C) :
    F.map (ρ_ X).inv = (ρ_ (F.obj X)).inv ≫ F.obj X ◁ ε F  ≫ μ F X (𝟙_ C)

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.Monoidal
X : C
⊢ F.map (ρ_ X).inv = (ρ_ (F.obj X)).inv ≫ F.obj X ◁ ε F ≫ μ F X (𝟙_ C)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean
@[reassoc]
lemma homologyFunctor_shiftMap
    {K L : CochainComplex C ℤ} {n : ℤ} (f : K ⟶ L⟦n⟧) (a a' : ℤ) (h : n + a = a') :
    (homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap
      ((quotient _ _).map f ≫ ((quotient _ _).commShiftIso n).hom.app _) a a' h =
        (homologyFunctorFactors _ _ a).hom.app K ≫
          (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫
            (homologyFunctorFactors _ _ a').inv.app L

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : CochainComplex C ℤ
n : ℤ
f : K ⟶ (shiftFunctor (CochainComplex C ℤ) n).obj L
a a' : ℤ
h : n + a = a'
⊢ (homologyFunctor C (up ℤ) 0).shiftMap ((quotient C (up ℤ)).map f ≫ ((quotient C (up ℤ)).commShiftIso n).hom.app L) a
      a' h =
    (homologyFunctorFactors C (up ℤ) a).hom.app K ≫
      (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap f a a' h ≫ (homologyFunctorFactors C (up ℤ) a').inv.app L

Tactic:
apply Functor.ShiftSequence.induced_shiftMap

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
/-- Any two measures satisfying `QuotientMeasureEqMeasurePreimage` are equal. -/
@[to_additive]
lemma QuotientMeasureEqMeasurePreimage.unique
    [hasFun : HasFundamentalDomain G α ν] (μ μ' : Measure (Quotient α_mod_G))
    [QuotientMeasureEqMeasurePreimage ν μ] [QuotientMeasureEqMeasurePreimage ν μ'] :
    μ = μ'

Proof state:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
ν : Measure α
hasFun : HasFundamentalDomain G α ν
μ μ' : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : QuotientMeasureEqMeasurePreimage ν μ'
⊢ μ = μ'

Tactic:
obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain

Result:
case intro
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
ν : Measure α
hasFun : HasFundamentalDomain G α ν
μ μ' : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : QuotientMeasureEqMeasurePreimage ν μ'
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ μ = μ'

Proof state:
case intro
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
ν : Measure α
hasFun : HasFundamentalDomain G α ν
μ μ' : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : QuotientMeasureEqMeasurePreimage ν μ'
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ μ = μ'

Tactic:
rw [h𝓕.projection_respects_measure (μ := μ), h𝓕.projection_respects_measure (μ := μ')]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem disjoint_cons_right : Disjoint l₁ (a :: l₂) ↔ (a ∉ l₁) ∧ Disjoint l₁ l₂ :=
  disjoint_comm.trans <| by rw [disjoint_cons_left]; simp [disjoint_comm]

Proof state:
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ (a :: l₂).Disjoint l₁ ↔ ¬a ∈ l₁ ∧ l₁.Disjoint l₂

Tactic:
rw [disjoint_cons_left]

Result:
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ ¬a ∈ l₁ ∧ l₂.Disjoint l₁ ↔ ¬a ∈ l₁ ∧ l₁.Disjoint l₂

Proof state:
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ ¬a ∈ l₁ ∧ l₂.Disjoint l₁ ↔ ¬a ∈ l₁ ∧ l₁.Disjoint l₂

Tactic:
simp [disjoint_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_insertManyIfNewUnit_empty_list [EquivBEq α] [LawfulHashable α]
    {l : List α} {k : α} :
    (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1.contains k = l.contains k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k : α
⊢ (insertManyIfNewUnit empty l).val.contains k = l.contains k

Tactic:
simp [contains_insertManyIfNewUnit_list _ Raw.WF.empty₀]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem compl_apply [Zero α] [One α] (i j : V) : A.compl i j = 0 ∨ A.compl i j = 1

Proof state:
V : Type u_1
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ (if i = j then 0 else if A i j = 0 then 1 else 0) = 0 ∨ (if i = j then 0 else if A i j = 0 then 1 else 0) = 1

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
V : Type u_1
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ A.compl i j = 0 ∨ A.compl i j = 1

Tactic:
unfold compl

Result:
V : Type u_1
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ (if i = j then 0 else if A i j = 0 then 1 else 0) = 0 ∨ (if i = j then 0 else if A i j = 0 then 1 else 0) = 1
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_eq_sub (a b : α) : toIcoMod hp a b = toIcoMod hp 0 (b - a) + a

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b = toIcoMod hp 0 (b - a) + a

Tactic:
rw [toIcoMod_sub_eq_sub, zero_add, sub_add_cancel]

Result:
no goals
-- Mathlib/Data/Matroid/Loop.lean
lemma comap_loops {M : Matroid β} {f : α → β} : (M.comap f).loops = f ⁻¹' M.loops

Proof state:
α : Type u_1
β : Type u_2
M : Matroid β
f : α → β
⊢ (M.comap f).loops = f ⁻¹' M.loops

Tactic:
rw [loops, comap_closure_eq, image_empty]

Result:
no goals
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.openCell_zero_eq_singleton [RelCWComplex C D] {j : cell C 0} :
    openCell 0 j = {map 0 j ![]}

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
j : cell C 0
⊢ openCell 0 j = {↑(map 0 j) ![]}

Tactic:
simp [openCell, Matrix.empty_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean
lemma leftAdjointObjIsDefined_iff (X : C) :
    F.LeftAdjointObjIsDefined X ↔ IsCorepresentable (F ⋙ coyoneda.obj (op X))

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X : C
⊢ F.LeftAdjointObjIsDefined X ↔ (F ⋙ coyoneda.obj (op X)).IsCorepresentable

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_min_mul_right (a b c : Nat) : min (a * c) (b * c) = min a b * c

Proof state:
case zero
c b : Nat
⊢ min (0 * c) (b * c) = min 0 b * c

Tactic:
simp

Result:
no goals

Proof state:
a b c : Nat
⊢ min (a * c) (b * c) = min a b * c

Tactic:
induction a generalizing b with
| zero => simp
| succ i ind =>
  cases b <;> simp [succ_eq_add_one, Nat.succ_mul, Nat.add_min_add_right, ind]

Result:
no goals

Proof state:
case succ
c i : Nat
ind : ∀ (b : Nat), min (i * c) (b * c) = min i b * c
b : Nat
⊢ min ((i + 1) * c) (b * c) = min (i + 1) b * c

Tactic:
cases b <;> simp [succ_eq_add_one, Nat.succ_mul, Nat.add_min_add_right, ind]

Result:
no goals
-- Mathlib/Algebra/Group/ForwardDiff.lean
lemma shiftₗ_apply (f : M → G) (y : M) : shiftₗ M G h f y = f (y + h)

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
y : M
⊢ (shiftₗ M G h) f y = f (y + h)

Tactic:
rw [shiftₗ, LinearMap.add_apply, Pi.add_apply, LinearMap.one_apply, fwdDiffₗ_apply, fwdDiff,
  sub_add_cancel]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem cauchy_series_of_le_geometric {C : ℝ} {u : ℕ → α} {r : ℝ} (hr : r < 1)
    (h : ∀ n, ‖u n‖ ≤ C * r ^ n) : CauchySeq fun n ↦ ∑ k ∈ range n, u k :=
  cauchySeq_of_le_geometric r C hr (by simp [h])

Proof state:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
r : ℝ
hr : r < 1
h : ∀ (n : ℕ), ‖u n‖ ≤ C * r ^ n
⊢ ∀ (n : ℕ), dist (∑ k ∈ Finset.range n, u k) (∑ k ∈ Finset.range (n + 1), u k) ≤ C * r ^ n

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_pi_closedBall (a : ι → ℝ) {r : ℝ} (hr : 0 ≤ r) :
    volume (Metric.closedBall a r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 ≤ r
⊢ volume (Metric.closedBall a r) = ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
simp only [MeasureTheory.volume_pi_closedBall a hr, volume_closedBall, Finset.prod_const]

Result:
ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 ≤ r
⊢ ofReal (2 * r) ^ Finset.univ.card = ofReal ((2 * r) ^ Fintype.card ι)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 ≤ r
⊢ ofReal (2 * r) ^ Finset.univ.card = ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
exact (ENNReal.ofReal_pow (mul_nonneg zero_le_two hr) _).symm

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem rowLen_transpose (μ : YoungDiagram) (i : ℕ) : μ.transpose.rowLen i = μ.colLen i

Proof state:
μ : YoungDiagram
i : ℕ
⊢ μ.transpose.rowLen i = μ.colLen i

Tactic:
simp [rowLen, colLen]

Result:
no goals