harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Lean/Data/HashSet.lean
theorem HashSetBucket.size_update {α : Type u} (data : HashSetBucket α) (i : USize) (d : List α) (h : i.toNat < data.val.size) :
    (data.update i d h).val.size = data.val.size

Proof state:
α : Type u
data : HashSetBucket α
i : USize
d : List α
h : i.toNat < data.val.size
⊢ (data.update i d h).val.size = data.val.size

Tactic:
simp [update, Array.uset]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem norm_cpow_eq_rpow_re_of_nonneg {x : ℝ} (hx : 0 ≤ x) {y : ℂ} (hy : re y ≠ 0) :
    ‖(x : ℂ) ^ y‖ = x ^ re y

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ‖↑x ^ y‖ = x ^ y.re

Tactic:
rw [norm_cpow_of_imp] <;> simp [*, arg_ofReal_of_nonneg, abs_of_nonneg]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem of_mono_zero (X Y : C) [Mono (0 : X ⟶ Y)] : IsZero X :=
  (iff_id_eq_zero X).mpr ((cancel_mono (0 : X ⟶ Y)).1 (by simp))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Mono 0
⊢ 𝟙 X ≫ 0 = 0 ≫ 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem rank_eq_of_equiv_equiv (i : R → R') (j : M ≃+ M₁)
    (hi : Bijective i) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) :
    Module.rank R M = Module.rank R' M₁

Proof state:
R : Type u
R' : Type u'
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R' M₁
i : R → R'
j : M ≃+ M₁
hi : Bijective i
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
⊢ Module.rank R M = Module.rank R' M₁

Tactic:
simpa only [lift_id] using lift_rank_eq_of_equiv_equiv i j hi hc

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem le_rootMultiplicity_map {p : A[X]} {f : A →+* B} (hmap : map f p ≠ 0) (a : A) :
    rootMultiplicity a p ≤ rootMultiplicity (f a) (p.map f)

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - C (f a)) ^ rootMultiplicity a p ∣ map f p

Tactic:
refine _root_.trans ?_ ((mapRingHom f).map_dvd (pow_rootMultiplicity_dvd p a))

Result:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - C (f a)) ^ rootMultiplicity a p ∣ (mapRingHom f) ((X - C a) ^ rootMultiplicity a p)

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ rootMultiplicity a p ≤ rootMultiplicity (f a) (map f p)

Tactic:
rw [le_rootMultiplicity_iff hmap]

Result:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - C (f a)) ^ rootMultiplicity a p ∣ map f p

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - C (f a)) ^ rootMultiplicity a p ∣ (mapRingHom f) ((X - C a) ^ rootMultiplicity a p)

Tactic:
rw [map_pow, map_sub, coe_mapRingHom, map_X, map_C]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem SimpleFunc.integral_L1_eq_integral (f : α →₁ₛ[μ] E) :
    L1.integral (f : α →₁[μ] E) = SimpleFunc.integral f

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(simpleFunc E 1 μ)
⊢ L1.integralCLM ↑f = MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)

Tactic:
exact setToL1_eq_setToL1SCLM (dominatedFinMeasAdditive_weightedSMul μ) f

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(simpleFunc E 1 μ)
⊢ L1.integral ↑f = integral f

Tactic:
simp only [integral, L1.integral]

Result:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(simpleFunc E 1 μ)
⊢ L1.integralCLM ↑f = MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)
-- Mathlib/Data/Nat/Squarefree.lean
lemma prod_primeFactors_of_squarefree (hn : Squarefree n) : ∏ p ∈ n.primeFactors, p = n

Proof state:
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, p = n

Tactic:
rw [← toFinset_factors, List.prod_toFinset _ hn.nodup_primeFactorsList,
  List.map_id', Nat.prod_primeFactorsList hn.ne_zero]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_Icc_succ_top {a b : ℕ} (hab : a ≤ b + 1) (f : ℕ → M) :
    (∏ k ∈ Icc a (b + 1), f k) = (∏ k ∈ Icc a b, f k) * f (b + 1)

Proof state:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b + 1
f : ℕ → M
⊢ ∏ k ∈ Icc a (b + 1), f k = (∏ k ∈ Icc a b, f k) * f (b + 1)

Tactic:
rw [← Nat.Ico_succ_right, prod_Ico_succ_top hab, Nat.Ico_succ_right]

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem iSup_eq_closure {ι : Sort*} (S : ι → L.Substructure M) :
    ⨆ i, S i = closure L (⋃ i, (S i : Set M))

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Sort u_3
S : ι → L.Substructure M
⊢ ⨆ i, S i = (closure L).toFun (⋃ i, ↑(S i))

Tactic:
simp_rw [closure_iUnion, closure_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tan_pi_div_two_sub (x : ℂ) : tan (π / 2 - x) = (tan x)⁻¹

Proof state:
x : ℂ
⊢ tan (↑π / 2 - x) = (tan x)⁻¹

Tactic:
rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_eq_self {p : α → Bool} {l : Array α} :
    filter p l = l ↔ ∀ a ∈ l, p a

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ filter p l = l ↔ ∀ (a : α), a ∈ l → p a = true

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
l : List α
⊢ filter p { toList := l } = { toList := l } ↔ ∀ (a : α), a ∈ { toList := l } → p a = true

Proof state:
case mk
α : Type u_1
p : α → Bool
l : List α
⊢ filter p { toList := l } = { toList := l } ↔ ∀ (a : α), a ∈ { toList := l } → p a = true

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem cokernel.map_desc {X Y Z X' Y' Z' : C} (f : X ⟶ Y) [HasCokernel f] (g : Y ⟶ Z)
    (w : f ≫ g = 0) (f' : X' ⟶ Y') [HasCokernel f'] (g' : Y' ⟶ Z') (w' : f' ≫ g' = 0) (p : X ⟶ X')
    (q : Y ⟶ Y') (r : Z ⟶ Z') (h₁ : f ≫ q = p ≫ f') (h₂ : g ≫ r = q ≫ g') :
    cokernel.map f f' p q h₁ ≫ cokernel.desc f' g' w' = cokernel.desc f g w ≫ r

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z X' Y' Z' : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
g : Y ⟶ Z
w : f ≫ g = 0
f' : X' ⟶ Y'
inst✝ : HasCokernel f'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ coequalizer.π f 0 ≫ map f f' p q h₁ ≫ desc f' g' w' = coequalizer.π f 0 ≫ desc f g w ≫ r

Tactic:
simp [h₂]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z X' Y' Z' : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
g : Y ⟶ Z
w : f ≫ g = 0
f' : X' ⟶ Y'
inst✝ : HasCokernel f'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ map f f' p q h₁ ≫ desc f' g' w' = desc f g w ≫ r

Tactic:
ext

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z X' Y' Z' : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
g : Y ⟶ Z
w : f ≫ g = 0
f' : X' ⟶ Y'
inst✝ : HasCokernel f'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ coequalizer.π f 0 ≫ map f f' p q h₁ ≫ desc f' g' w' = coequalizer.π f 0 ≫ desc f g w ≫ r
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
lemma functor_additive :
    letI := preadditive L W
    L.Additive :=
  letI := preadditive L W
  ⟨by apply Preadditive.map_add⟩

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
this : Preadditive D := preadditive L W
⊢ ∀ {X Y : C} {f g : X ⟶ Y}, L.map (f + g) = L.map f + L.map g

Tactic:
apply Preadditive.map_add

Result:
no goals
-- Mathlib/Data/Matroid/Loop.lean
@[simp]
lemma singleton_not_indep (he : e ∈ M.E

Proof state:
α : Type u_1
M : Matroid α
e : α
he : autoParam (e ∈ M.E) _auto✝
⊢ ¬M.Indep {e} ↔ M.IsLoop e

Tactic:
rw [← singleton_dep, ← not_indep_iff]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Norm.lean
theorem absNorm_one : absNorm (1 : FractionalIdeal R⁰ K) = 1

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ absNorm 1 = 1

Tactic:
convert absNorm.map_one'

Result:
no goals
-- Mathlib/RingTheory/Valuation/RankOne.lean
theorem hom_eq_zero_iff {x : Γ₀} : RankOne.hom v x = 0 ↔ x = 0 :=
  ⟨fun h ↦ zero_of_hom_zero v h, fun h ↦ by rw [h, _root_.map_zero]⟩

Proof state:
R : Type u_1
inst✝² : Ring R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.RankOne
x : Γ₀
h : x = 0
⊢ (hom v) x = 0

Tactic:
rw [h, _root_.map_zero]

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma compls_compls (s : Finset α) : sᶜˢᶜˢ = s

Proof state:
case h
α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
a✝ : α
⊢ a✝ ∈ sᶜˢᶜˢ ↔ a✝ ∈ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
⊢ sᶜˢᶜˢ = s

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
a✝ : α
⊢ a✝ ∈ sᶜˢᶜˢ ↔ a✝ ∈ s
-- Mathlib/Algebra/Order/Group/DenselyOrdered.lean
@[to_additive]
private lemma exists_mul_left_lt [Group α] [LT α] [DenselyOrdered α]
    [CovariantClass α α (Function.swap (· * ·)) (· < ·)] {a b c : α} (hc : a * b < c) :
    ∃ a' > a, a' * b < c

Proof state:
case intro.intro
α : Type u_1
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : CovariantClass α α (Function.swap fun x1 x2 => x1 * x2) fun x1 x2 => x1 < x2
a b c : α
hc : a * b < c
a' : α
ha' : a < a'
hc' : a' < c / b
⊢ ∃ a', a' > a ∧ a' * b < c

Tactic:
exact ⟨a', ha', lt_div_iff_mul_lt.1 hc'⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : CovariantClass α α (Function.swap fun x1 x2 => x1 * x2) fun x1 x2 => x1 < x2
a b c : α
hc : a * b < c
⊢ ∃ a', a' > a ∧ a' * b < c

Tactic:
obtain ⟨a', ha', hc'⟩ := exists_between (lt_div_iff_mul_lt.2 hc)

Result:
case intro.intro
α : Type u_1
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : CovariantClass α α (Function.swap fun x1 x2 => x1 * x2) fun x1 x2 => x1 < x2
a b c : α
hc : a * b < c
a' : α
ha' : a < a'
hc' : a' < c / b
⊢ ∃ a', a' > a ∧ a' * b < c
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem aemeasurable_uIoc_iff [LinearOrder α] {f : α → β} {a b : α} :
    (AEMeasurable f <| μ.restrict <| Ι a b) ↔
      (AEMeasurable f <| μ.restrict <| Ioc a b) ∧ (AEMeasurable f <| μ.restrict <| Ioc b a)

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : LinearOrder α
f : α → β
a b : α
⊢ AEMeasurable f (μ.restrict (Ι a b)) ↔ AEMeasurable f (μ.restrict (Ioc a b)) ∧ AEMeasurable f (μ.restrict (Ioc b a))

Tactic:
rw [uIoc_eq_union, aemeasurable_union_iff]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem restrict_dep_iff : (M ↾ R).Dep X ↔ ¬ M.Indep X ∧ X ⊆ R

Proof state:
α : Type u_1
M : Matroid α
R X : Set α
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
R X : Set α
⊢ (M ↾ R).Dep X ↔ ¬M.Indep X ∧ X ⊆ R

Tactic:
rw [Dep, restrict_indep_iff, restrict_ground_eq]

Result:
α : Type u_1
M : Matroid α
R X : Set α
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
/-- An element `p` of `FreeAddMonoid (R × Π i, s i)` lifts an element `x` of `⨂[R] i, s i`
if and only if `x` is equal to the sum of `a • ⨂ₜ[R] i, m i` over all the entries
`(a, m)` of `p`.
-/
lemma mem_lifts_iff (x : ⨂[R] i, s i) (p : FreeAddMonoid (R × Π i, s i)) :
    p ∈ lifts x ↔ List.sum (List.map (fun x ↦ x.1 • ⨂ₜ[R] i, x.2 i) p) = x

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
⊢ p ∈ x.lifts ↔ (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum = x

Tactic:
simp only [lifts, Set.mem_setOf_eq, FreeAddMonoid.toPiTensorProduct]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem map_comap_eq_self {f : L →ₐ[K] L'} {S : IntermediateField K L'} (h : S ≤ f.fieldRange) :
    (S.comap f).map f = S

Proof state:
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
f : L →ₐ[K] L'
S : IntermediateField K L'
h : S ≤ f.fieldRange
⊢ map f (comap f S) = S

Tactic:
simpa only [inf_of_le_left h] using map_comap_eq f S

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
protected lemma inv_inv (hab : a + b = 1) : a⁻¹.IsConjExponent b⁻¹ where
  inv_add_inv_conj

Proof state:
a b : ℝ≥0∞
hab : a + b = 1
⊢ a⁻¹⁻¹ + b⁻¹⁻¹ = 1

Tactic:
simpa only [inv_inv] using hab

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_bmod {x : Int} {m : Nat} : bmod (x % m) m = bmod x m

Proof state:
x : Int
m : Nat
⊢ (x % ↑m).bmod m = x.bmod m

Tactic:
simp [bmod]

Result:
no goals
-- Mathlib/Dynamics/OmegaLimit.lean
theorem isInvariant_omegaLimit (hf : ∀ t, Tendsto (t + ·) f f) : IsInvariant ϕ (ω f ϕ s)

Proof state:
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => t + x) f f
⊢ IsInvariant ϕ.toFun (ω f ϕ.toFun s)

Tactic:
refine fun t ↦ MapsTo.mono_right ?_ (omegaLimit_subset_of_tendsto ϕ s (hf t))

Result:
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => t + x) f f
t : τ
⊢ MapsTo (ϕ.toFun t) (ω f ϕ.toFun s) (ω f (fun t_1 x => ϕ.toFun (t + t_1) x) s)

Proof state:
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => t + x) f f
t : τ
⊢ MapsTo (ϕ.toFun t) (ω f ϕ.toFun s) (ω f (fun t_1 x => ϕ.toFun (t + t_1) x) s)

Tactic:
exact
  mapsTo_omegaLimit _ (mapsTo_id _) (fun t' x ↦ (ϕ.map_add _ _ _).symm)
    (continuous_const.flow ϕ continuous_id)

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem prod_eq_bot_iff {p₁ : Submodule R M} {p₂ : Submodule R M₂} :
    p₁.prod p₂ = ⊥ ↔ p₁ = ⊥ ∧ p₂ = ⊥

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
⊢ p₁.prod p₂ = ⊥ ↔ p₁ = ⊥ ∧ p₂ = ⊥

Tactic:
simp only [eq_bot_iff, prod_le_iff, (gc_map_comap _).le_iff_le, comap_bot, ker_inl, ker_inr]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
theorem head_desc : head arrows ≫ desc f fs w = f

Proof state:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
⊢ head arrows ≫ desc f fs w = f

Tactic:
simp only [colimit.ι_desc, WidePushoutShape.mkCocone_pt, WidePushoutShape.mkCocone_ι_app]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_replicate_self [LawfulBEq α] {a : α} :
    (replicate n a).erase a = replicate (n - 1) a

Proof state:
α : Type u_1
inst✝¹ : BEq α
n : Nat
inst✝ : LawfulBEq α
a : α
⊢ (replicate n a).erase a = replicate (n - 1) a

Tactic:
cases n <;> simp [replicate_succ]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
lemma Multiset.iSup_mem_map_of_ne_zero {s : Multiset ι} (f : ι → α) (h : s ≠ 0) :
    ⨆ x ∈ s, f x ∈ s.map f :=
  s.iSup_mem_map_of_exists_sSup_empty_le _ (by simpa using exists_mem_of_ne_zero h)

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Multiset ι
f : ι → α
h : s ≠ 0
⊢ ∃ x ∈ s, sSup ∅ ≤ f x

Tactic:
simpa using exists_mem_of_ne_zero h

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem mem_finPairsLT {n : ℕ} {a : Σ_ : Fin n, Fin n} : a ∈ finPairsLT n ↔ a.2 < a.1

Proof state:
n : ℕ
a : (_ : Fin n) × Fin n
⊢ a ∈ finPairsLT n ↔ a.snd < a.fst

Tactic:
simp only [finPairsLT, Fin.lt_iff_val_lt_val, true_and, mem_attachFin, mem_range, mem_univ,
  mem_sigma]

Result:
no goals
-- Mathlib/NumberTheory/ZetaValues.lean
theorem bernoulliFun_endpoints_eq_of_ne_one {k : ℕ} (hk : k ≠ 1) :
    bernoulliFun k 1 = bernoulliFun k 0

Proof state:
k : ℕ
hk : k ≠ 1
⊢ bernoulliFun k 1 = bernoulliFun k 0

Tactic:
rw [bernoulliFun_eval_zero, bernoulliFun, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one,
  bernoulli_eq_bernoulli'_of_ne_one hk, eq_ratCast]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem mem_support {x : α} : x ∈ f.support ↔ f x ≠ x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ x ∈ f.support ↔ f x ≠ x

Tactic:
rw [support, mem_filter, and_iff_right (mem_univ x)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_cons : (cons a x).msb = a

Proof state:
a : Bool
w✝ : Nat
x : BitVec w✝
⊢ (cons a x).msb = a

Tactic:
simp [cons, msb_cast, msb_append]

Result:
no goals
-- Mathlib/Order/Bounds/Lattice.lean
theorem gc_upperBounds_lowerBounds : GaloisConnection
    (OrderDual.toDual ∘ upperBounds : Set α → (Set α)ᵒᵈ)
    (lowerBounds ∘ OrderDual.ofDual : (Set α)ᵒᵈ → Set α)

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ GaloisConnection (⇑OrderDual.toDual ∘ upperBounds) (lowerBounds ∘ ⇑OrderDual.ofDual)

Tactic:
simpa [GaloisConnection, subset_def, mem_upperBounds, mem_lowerBounds]
  using fun S T ↦ forall₂_swap

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc (attr := simp)]
lemma inr_desc :
    inr φ ≫ desc φ α hα = α

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

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast_of_perm [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} {h'}
    (hl : DistinctKeys l) (h : Perm l l') :
    getValueCast a l h' = getValueCast a l' ((containsKey_of_perm h).symm.trans h')

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l l' : List ((a : α) × β a)
a : α
h' : containsKey a l = true
hl : DistinctKeys l
h : l.Perm l'
⊢ getValueCast a l h' = getValueCast a l' ⋯

Tactic:
rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, ← getValueCast?_eq_some_getValueCast,
  getValueCast?_of_perm hl h]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma infClosure_univ : infClosure (Set.univ : Set α) = Set.univ

Proof state:
α : Type u_3
inst✝ : SemilatticeInf α
⊢ infClosure Set.univ = Set.univ

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem compl_sup_distrib (a b : α) : (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

Tactic:
simp_rw [← himp_bot, sup_himp_distrib]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem biproduct.matrix_desc [Fintype K] {f : J → C} {g : K → C}
    (m : ∀ j k, f j ⟶ g k) {P} (x : ∀ k, g k ⟶ P) :
    biproduct.matrix m ≫ biproduct.desc x = biproduct.desc fun j => ∑ k, m j k ≫ x k

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J K : Type
inst✝² : Finite J
inst✝¹ : HasFiniteBiproducts C
inst✝ : Fintype K
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
P : C
x : (k : K) → g k ⟶ P
⊢ matrix m ≫ desc x = desc fun j => ∑ k : K, m j k ≫ x k

Tactic:
ext

Result:
case w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J K : Type
inst✝² : Finite J
inst✝¹ : HasFiniteBiproducts C
inst✝ : Fintype K
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
P : C
x : (k : K) → g k ⟶ P
j✝ : J
⊢ ι f j✝ ≫ matrix m ≫ desc x = ι f j✝ ≫ desc fun j => ∑ k : K, m j k ≫ x k

Proof state:
case w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J K : Type
inst✝² : Finite J
inst✝¹ : HasFiniteBiproducts C
inst✝ : Fintype K
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
P : C
x : (k : K) → g k ⟶ P
j✝ : J
⊢ ι f j✝ ≫ matrix m ≫ desc x = ι f j✝ ≫ desc fun j => ∑ k : K, m j k ≫ x k

Tactic:
simp [lift_desc]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Real.lean
theorem inv_norm_smul_mem_unitClosedBall (x : E) :
    ‖x‖⁻¹ • x ∈ closedBall (0 : E) 1

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ ‖x‖⁻¹ • x ∈ closedBall 0 1

Tactic:
simp only [mem_closedBall_zero_iff, norm_smul, norm_inv, norm_norm, ← div_eq_inv_mul,
  div_self_le_one]

Result:
no goals
-- Mathlib/Topology/Category/CompHausLike/Limits.lean
@[reassoc]
lemma pullback.condition : pullback.fst f g ≫ f = pullback.snd f g ≫ g

Proof state:
case h.h.mk
P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
val✝ : ↑X.toTop × ↑Y.toTop
h : val✝ ∈ {xy | (ConcreteCategory.hom f) xy.1 = (ConcreteCategory.hom g) xy.2}
⊢ (ConcreteCategory.hom (fst f g ≫ f)) ⟨val✝, h⟩ = (ConcreteCategory.hom (snd f g ≫ g)) ⟨val✝, h⟩

Tactic:
exact h

Result:
no goals

Proof state:
P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
⊢ fst f g ≫ f = snd f g ≫ g

Tactic:
ext ⟨_,h⟩

Result:
case h.h.mk
P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
val✝ : ↑X.toTop × ↑Y.toTop
h : val✝ ∈ {xy | (ConcreteCategory.hom f) xy.1 = (ConcreteCategory.hom g) xy.2}
⊢ (ConcreteCategory.hom (fst f g ≫ f)) ⟨val✝, h⟩ = (ConcreteCategory.hom (snd f g ≫ g)) ⟨val✝, h⟩
-- Mathlib/Algebra/Group/Pi/Basic.lean
theorem elim_mulSingle_one [DecidableEq α] [DecidableEq β] [One γ] (i : α) (c : γ) :
    Sum.elim (Pi.mulSingle i c) (1 : β → γ) = Pi.mulSingle (Sum.inl i) c

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : One γ
i : α
c : γ
⊢ Sum.elim (Pi.mulSingle i c) 1 = Pi.mulSingle (inl i) c

Tactic:
simp only [Pi.mulSingle, Sum.elim_update_left, elim_one_one]

Result:
no goals