harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma add_of_Y_ne' {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) (hy : P y * Q z ≠ W.negY Q * P z) :
    W.add P Q = W.dblZ P •
      ![W.toAffine.addX (P x / P z) (Q x / Q z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)), 1]

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
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.add P Q =
    W.dblZ P •
      ![(toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
          ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]

Tactic:
rw [add, if_pos <| equiv_of_X_eq_of_Y_eq hPz hQz hx <| Y_eq_of_Y_ne' hP hQ hPz hQz hx hy,
  dblXYZ_of_Z_ne_zero hP hQ hPz hQz hx hy]

Result:
no goals
-- Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
@[simp]
lemma residue_eq_zero_iff (x : R) : residue R x = 0 ↔ x ∈ maximalIdeal R

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
x : R
⊢ (residue R) x = 0 ↔ x ∈ maximalIdeal R

Tactic:
rw [← RingHom.mem_ker, ker_residue]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem enorm_indicatorConstLp_le :
    ‖indicatorConstLp p hs hμs c‖ₑ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ ‖indicatorConstLp p hs hμs c‖ₑ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
simpa [ENNReal.coe_rpow_of_nonneg, ENNReal.coe_toNNReal hμs, Lp.enorm_def, ← enorm_eq_nnnorm]
  using ENNReal.coe_le_coe.2 <| nnnorm_indicatorConstLp_le (c := c) (hμs := hμs)

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem image_update_Ioc_right (f : ∀ i, α i) (i : ι) (b : α i) :
    update f i '' Ioc (f i) b = Ioc f (update f i b)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' Ioc (f i) b = Ioc f (update f i b)

Tactic:
simpa using image_update_Ioc f i (f i) b

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_inter_singleton [DecidableEq α] (s₁ s₂ : Finset α) (hf : Injective fun a => f a b) :
    image₂ f (s₁ ∩ s₂) {b} = image₂ f s₁ {b} ∩ image₂ f s₂ {b}

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
b : β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
hf : Injective fun a => f a b
⊢ image₂ f (s₁ ∩ s₂) {b} = image₂ f s₁ {b} ∩ image₂ f s₂ {b}

Tactic:
simp_rw [image₂_singleton_right, image_inter _ _ hf]

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_disjoint_iff {f : α → M} {s : Set α} :
    Disjoint (mulSupport f) s ↔ EqOn f 1 s

Proof state:
α : Type u_1
M : Type u_5
inst✝ : One M
f : α → M
s : Set α
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s

Tactic:
simp_rw [← subset_compl_iff_disjoint_right, mulSupport_subset_iff', not_mem_compl_iff, EqOn,
  Pi.one_apply]

Result:
no goals
-- Mathlib/Analysis/Complex/Asymptotics.lean
lemma isBigO_comp_ofReal_nhds_ne {f g : ℂ → ℂ} {x : ℝ} (h : f =O[𝓝[≠] (x : ℂ)] g) :
    (fun y : ℝ ↦ f y) =O[𝓝[≠] x] (fun y : ℝ ↦ g y) :=
  h.comp_tendsto <| continuous_ofReal.continuousWithinAt.tendsto_nhdsWithin fun _ _ ↦ by simp_all

Proof state:
f g : ℂ → ℂ
x : ℝ
h : f =O[𝓝[≠] ↑x] g
x✝¹ : ℝ
x✝ : x✝¹ ∈ {x}ᶜ
⊢ ↑x✝¹ ∈ {↑x}ᶜ

Tactic:
simp_all

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem restrict_le_zero_of_not_measurable (hi : ¬MeasurableSet i) : v ≤[i] 0

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ v ≤[i] 0

Tactic:
rw [restrict_zero, restrict_not_measurable _ hi]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem neg_equiv_neg {f g : CauSeq β abv} (hf : f ≈ g) : -f ≈ -g

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : f ≈ g
⊢ -f ≈ -g

Tactic:
simpa only [neg_sub'] using neg_limZero hf

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem principal_eq_map_coe_top (s : Set α) : 𝓟 s = map ((↑) : s → α) ⊤

Proof state:
α : Type u_1
s : Set α
⊢ 𝓟 s = map Subtype.val ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial.lean
theorem rank_eq_lift : Module.rank K (MvPolynomial σ K) = lift.{v} #(σ →₀ ℕ)

Proof state:
σ : Type u
K : Type v
inst✝¹ : CommRing K
inst✝ : Nontrivial K
⊢ Module.rank K (MvPolynomial σ K) = lift.{v, u} #(σ →₀ ℕ)

Tactic:
rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank, lift_lift, lift_umax.{u,v}]

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem mk_self : mk f f = 0 :=
  Quotient.sound' <| QuotientAddGroup.leftRel_apply.mpr (mem_span_singleton.2 <| by simp)

Proof state:
R : Type u
inst✝ : CommRing R
f : R[X]
⊢ f ∣ -f + 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_add_le (p q : R[X]) : degree (p + q) ≤ max (degree p) (degree q)

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p + q).degree ≤ p.degree ⊔ q.degree

Tactic:
simpa only [degree, ← support_toFinsupp, toFinsupp_add]
  using AddMonoidAlgebra.sup_support_add_le _ _ _

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
@[simp] lemma Even.neg_pow : Even n → ∀ a : α, (-a) ^ n = a ^ n

Proof state:
case intro
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)

Tactic:
simp_rw [← two_mul, pow_mul, neg_sq]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n

Tactic:
rintro ⟨c, rfl⟩ a

Result:
case intro
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma ΨSq_two : W.ΨSq 2 = W.Ψ₂Sq

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.ΨSq 2 = W.Ψ₂Sq

Tactic:
rw [← Nat.cast_two, ΨSq_ofNat, preΨ'_two, one_pow, one_mul, if_pos even_two]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
theorem IsSRGWith.card_neighborFinset_union_of_adj {v w : V} (h : G.IsSRGWith n k ℓ μ)
    (ha : G.Adj v w) : #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - ℓ

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
ha : G.Adj v w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card ↑(G.commonNeighbors v w)

Tactic:
apply h.card_neighborFinset_union_eq

Result:
no goals

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
ha : G.Adj v w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - ℓ

Tactic:
rw [← h.of_adj v w ha]

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
ha : G.Adj v w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card ↑(G.commonNeighbors v w)
-- Mathlib/Order/Interval/Set/Basic.lean
@[simp] lemma Ioi_False : Ioi False = {True}

Proof state:
⊢ Ioi False = {True}

Tactic:
aesop (add simp [Ioi, lt_iff_le_not_le])

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma le_inv_smul_iff_of_pos [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
    b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁵ : GroupWithZero α
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : MulAction α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : 0 < a
⊢ b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂

Tactic:
rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem spanExt_inv_app_right : (spanExt iX iY iZ wf wg).inv.app WalkingSpan.right = iZ.inv

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).inv.app WalkingSpan.right = iZ.inv

Tactic:
dsimp [spanExt]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem withTopEquiv_symm_lt {x y : ℕ∞} : withTopEquiv.symm x < withTopEquiv.symm y ↔ x < y

Proof state:
x y : ℕ∞
⊢ withTopEquiv.symm x < withTopEquiv.symm y ↔ x < y

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_mul_const_Ico (a b : α) {c : α} (h : 0 < c) :
    (fun x => x * c) ⁻¹' Ico a b = Ico (a / c) (b / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : 0 < c
⊢ (fun x => x * c) ⁻¹' Ico a b = Ico (a / c) (b / c)

Tactic:
simp [← Ici_inter_Iio, h]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem Filter.Tendsto.div_atBot {a : 𝕜} (h : Tendsto f l (𝓝 a)) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x / g x) l (𝓝 0)

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atBot
⊢ Tendsto (fun x => f x * (g x)⁻¹) l (𝓝 0)

Tactic:
exact mul_zero a ▸ h.mul (tendsto_inv_atBot_zero.comp hg)

Result:
no goals

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atBot
⊢ Tendsto (fun x => f x / g x) l (𝓝 0)

Tactic:
simp only [div_eq_mul_inv]

Result:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atBot
⊢ Tendsto (fun x => f x * (g x)⁻¹) l (𝓝 0)
-- Mathlib/Algebra/Group/Prod.lean
theorem one_mk_mul_one_mk [Monoid M] [Mul N] (b₁ b₂ : N) :
    ((1 : M), b₁) * (1, b₂) = (1, b₁ * b₂)

Proof state:
M : Type u_3
N : Type u_4
inst✝¹ : Monoid M
inst✝ : Mul N
b₁ b₂ : N
⊢ (1, b₁) * (1, b₂) = (1, b₁ * b₂)

Tactic:
rw [mk_mul_mk, mul_one]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Basic.lean
theorem closure_singleton_le_iff_mem (m : M) (p : Submonoid M) : closure {m} ≤ p ↔ m ∈ p

Proof state:
M : Type u_1
inst✝ : MulOneClass M
m : M
p : Submonoid M
⊢ closure {m} ≤ p ↔ m ∈ p

Tactic:
rw [closure_le, singleton_subset_iff, SetLike.mem_coe]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul {f : α → F} {g : α → G} {c : ℝ≥0}
    (h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) : eLpNormEssSup f μ ≤ c • eLpNormEssSup g μ :=
  calc
    essSup (‖f ·‖ₑ) μ ≤ essSup (fun x => (↑(c * ‖g x‖₊) : ℝ≥0∞)) μ :=
      essSup_mono_ae <| h.mono fun _ hx => ENNReal.coe_le_coe.mpr hx
    _ = essSup (c * ‖g ·‖ₑ) μ

Proof state:
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
⊢ essSup (fun x => ↑(c * ‖g x‖₊)) μ = essSup (fun x => ↑c * ‖g x‖ₑ) μ

Tactic:
simp_rw [ENNReal.coe_mul, enorm]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem UniformContinuousOn.tendstoUniformly [UniformSpace α] [UniformSpace γ] {x : α} {U : Set α}
    (hU : U ∈ 𝓝 x) {F : α → β → γ} (hF : UniformContinuousOn (↿F) (U ×ˢ (univ : Set β))) :
    TendstoUniformly F (F x) (𝓝 x)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
hU : U ∈ 𝓝 x
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ univ)
⊢ TendstoUniformly F (F x) (𝓝 x)

Tactic:
simpa only [tendstoUniformlyOn_univ, nhdsWithin_eq_nhds.2 hU]
  using hF.tendstoUniformlyOn (mem_of_mem_nhds hU)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Associated.lean
theorem exists_mem_multiset_map_dvd (hp : Prime p) {s : Multiset β} {f : β → α} :
    p ∣ (s.map f).prod → ∃ a ∈ s, p ∣ f a := fun h => by
  simpa only [exists_prop, Multiset.mem_map, exists_exists_and_eq_and] using
    hp.exists_mem_multiset_dvd h

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CommMonoidWithZero α
p : α
hp : Prime p
s : Multiset β
f : β → α
h : p ∣ (Multiset.map f s).prod
⊢ ∃ a ∈ s, p ∣ f a

Tactic:
simpa only [exists_prop, Multiset.mem_map, exists_exists_and_eq_and] using
  hp.exists_mem_multiset_dvd h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem singleton_inj {α : Type _} {a b : α} : [a] = [b] ↔ a = b

Proof state:
α : Type u_1
a b : α
⊢ [a] = [b] ↔ a = b

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
theorem IsSRGWith.compl_is_regular (h : G.IsSRGWith n k ℓ μ) :
    Gᶜ.IsRegularOfDegree (n - k - 1)

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
⊢ Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k)

Tactic:
exact h.regular.compl

Result:
no goals

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
⊢ Gᶜ.IsRegularOfDegree (n - k - 1)

Tactic:
rw [← h.card, Nat.sub_sub, add_comm, ← Nat.sub_sub]

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
⊢ Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k)
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullbackDiagonalMapIso.inv_snd_fst :
    (pullbackDiagonalMapIso f i i₁ i₂).inv ≫ pullback.snd _ _ ≫ pullback.fst _ _ =
      pullback.fst _ _

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.inv ≫
      snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) =
    fst i₁ i₂

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).inv ≫
      snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) =
    fst i₁ i₂

Tactic:
delta pullbackDiagonalMapIso

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.inv ≫
      snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) =
    fst i₁ i₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_zero : ∀ a : Int, tdiv a 0 = 0
  | ofNat _ => show ofNat _ = _ by simp
  | -[_+1] => rfl

Proof state:
a✝ : Nat
⊢ ofNat (a✝ / 0) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_unique [Unique α] (l : α →₀ R) (v : α → M) :
    linearCombination R v l = l default • v default

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Unique α
l : α →₀ R
v : α → M
⊢ (linearCombination R v) l = l default • v default

Tactic:
rw [← linearCombination_single, ← unique_single l]

Result:
no goals
-- Mathlib/Algebra/Group/Equiv/Defs.lean
@[to_additive]
lemma comp_left_injective (e : M ≃* N) : Injective fun f : N →* P ↦ f.comp (e : M →* N) :=
  LeftInverse.injective (g := fun f ↦ f.comp e.symm) fun f ↦ by simp [MonoidHom.comp_assoc]

Proof state:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
e : M ≃* N
f : N →* P
⊢ (fun f => f.comp ↑e.symm) (f.comp ↑e) = f

Tactic:
simp [MonoidHom.comp_assoc]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
protected lemma Antitone.iSup (hf : ∀ i, Antitone (f i)) : Antitone (⨆ i, f i) :=
  Antitone.sSup (by simpa)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : Preorder α
inst✝ : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), Antitone (f i)
⊢ ∀ f_1 ∈ range fun i => f i, Antitone f_1

Tactic:
simpa

Result:
no goals
-- Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean
lemma refl (γ : OneCochain G U) : OneCohomologyRelation γ γ 1 := fun _ _ _ _ _ ↦ by simp

Proof state:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ Grp
I : Type w'
U : I → C
γ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (ConcreteCategory.hom (G.map x✝¹.op)) (1 x✝⁴) * γ.ev x✝⁴ x✝³ x✝¹ x✝ =
    γ.ev x✝⁴ x✝³ x✝¹ x✝ * (ConcreteCategory.hom (G.map x✝.op)) (1 x✝³)

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
lemma mem_primesBelow {k n : ℕ} :
    n ∈ primesBelow k ↔ n < k ∧ n.Prime

Proof state:
k n : ℕ
⊢ n ∈ k.primesBelow ↔ n < k ∧ Prime n

Tactic:
simp [primesBelow]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/WithZero.lean
theorem coe_unitsWithZeroEquiv_eq_units_val (γ : (WithZero α)ˣ) :
    ↑(unitsWithZeroEquiv γ) = γ.val

Proof state:
α : Type u_1
inst✝ : Group α
γ : (WithZero α)ˣ
⊢ ↑(unitsWithZeroEquiv γ) = ↑γ

Tactic:
simp only [WithZero.unitsWithZeroEquiv, MulEquiv.coe_mk, Equiv.coe_fn_mk, WithZero.coe_unzero]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
/-- **Cauchy-Schwarz inequality** for finsets using square roots in `ℝ`. -/
lemma sum_sqrt_mul_sqrt_le (s : Finset ι) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) :
    ∑ i ∈ s, √(f i) * √(g i) ≤ √(∑ i ∈ s, f i) * √(∑ i ∈ s, g i)

Proof state:
ι : Type u_2
f g : ι → ℝ
s : Finset ι
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
⊢ ∑ i ∈ s, √(f i) * √(g i) ≤ √(∑ i ∈ s, f i) * √(∑ i ∈ s, g i)

Tactic:
simpa [*] using sum_mul_le_sqrt_mul_sqrt _ (fun x ↦ √(f x)) (fun x ↦ √(g x))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
theorem lhs_cast {aig1 aig2 : AIG α} (s : FullAdderInput aig1)
    (hcast : aig1.decls.size ≤ aig2.decls.size) :
    (s.cast hcast).lhs = s.lhs.cast hcast

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
s : FullAdderInput aig1
hcast : aig1.decls.size ≤ aig2.decls.size
⊢ (s.cast hcast).lhs = s.lhs.cast hcast

Tactic:
simp [cast]

Result:
no goals
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem soln_dist_to_a_lt_deriv : ‖soln - a‖ < ‖F.derivative.eval a‖

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖soln - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖

Tactic:
rw [soln_dist_to_a, div_lt_iff₀ (deriv_norm_pos _), ← sq] <;> assumption

Result:
no goals
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem finInsepDegree_eq_of_equiv (i : E ≃ₐ[F] K) :
    finInsepDegree F E = finInsepDegree F K

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E ≃ₐ[F] K
⊢ finInsepDegree F E = finInsepDegree F K

Tactic:
simpa only [Cardinal.toNat_lift] using congr_arg Cardinal.toNat
  (lift_insepDegree_eq_of_equiv F E K i)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_zsmul_ne_zero_iff {θ : Angle} : (2 : ℤ) • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ π

Proof state:
θ : Angle
⊢ 2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
rw [← not_or, ← two_zsmul_eq_zero_iff]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem measure_union_null_iff : μ (s ∪ t) = 0 ↔ μ s = 0 ∧ μ t = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ μ (s ∪ t) = 0 ↔ μ s = 0 ∧ μ t = 0

Tactic:
simp [union_eq_iUnion, and_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α}
    {f : Option β → Option β} (h : (k == k') = false) : k' ∈ Const.alter m k f ↔ k' ∈ m

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
h : (k == k') = false
⊢ k' ∈ alter m k f ↔ k' ∈ m

Tactic:
simp only [mem_iff_contains, contains_alter_of_beq_eq_false, h]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem leadingCoeff_eq_zero_iff {f : MvPolynomial σ R} :
    leadingCoeff m f = 0 ↔ f = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.leadingCoeff f = 0 ↔ f = 0

Tactic:
simp only [← not_iff_not, leadingCoeff_ne_zero_iff]

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem lieSpan_mono {t : Set L} (h : s ⊆ t) : lieSpan R L s ≤ lieSpan R L t

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s t : Set L
h : s ⊆ t
⊢ lieSpan R L s ≤ lieSpan R L t

Tactic:
rw [lieSpan_le]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s t : Set L
h : s ⊆ t
⊢ s ⊆ ↑(lieSpan R L t)

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s t : Set L
h : s ⊆ t
⊢ s ⊆ ↑(lieSpan R L t)

Tactic:
exact Set.Subset.trans h subset_lieSpan

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem inner_rotation_pi_div_two_right (x : V) : ⟪x, o.rotation (π / 2 : ℝ) x⟫ = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ inner x ((o.rotation ↑(π / 2)) x) = 0

Tactic:
rw [real_inner_comm, inner_rotation_pi_div_two_left]

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem neg_eq (a : A) : -σ a = σ (-a) :=
  Set.ext fun x => by
    simp only [mem_neg, mem_iff, map_neg, ← neg_add', IsUnit.neg_iff, sub_neg_eq_add]

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
x : R
⊢ x ∈ -σ a ↔ x ∈ σ (-a)

Tactic:
simp only [mem_neg, mem_iff, map_neg, ← neg_add', IsUnit.neg_iff, sub_neg_eq_add]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem card_product : card (s ×ˢ t) = card s * card t

Proof state:
α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
⊢ (s ×ˢ t).card = s.card * t.card

Tactic:
simp [SProd.sprod, product]

Result:
no goals