harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_insertEntry_le [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
    (insertEntry k v l).length ≤ l.length + 1

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ (if containsKey k l = true then l.length else l.length + 1) ≤ l.length + 1

Tactic:
split <;> omega

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ (insertEntry k v l).length ≤ l.length + 1

Tactic:
rw [length_insertEntry]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ (if containsKey k l = true then l.length else l.length + 1) ≤ l.length + 1
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
private lemma aux (h : ∀ t ∈ 𝒜, a ∉ t) (ht : 𝒜.Shatters t) : a ∉ t

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a : α
h : ∀ t ∈ 𝒜, a ∉ t
ht : 𝒜.Shatters t
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
⊢ a ∉ t

Tactic:
exact not_mem_mono htu <| h u hu

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a : α
h : ∀ t ∈ 𝒜, a ∉ t
ht : 𝒜.Shatters t
⊢ a ∉ t

Tactic:
obtain ⟨u, hu, htu⟩ := ht.exists_superset

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a : α
h : ∀ t ∈ 𝒜, a ∉ t
ht : 𝒜.Shatters t
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
⊢ a ∉ t
-- Mathlib/CategoryTheory/HomCongr.lean
theorem homCongr_comp {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X ⟶ Y)
    (g : Y ⟶ Z) : α.homCongr γ (f ≫ g) = α.homCongr β f ≫ β.homCongr γ g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (α.homCongr γ) (f ≫ g) = (α.homCongr β) f ≫ (β.homCongr γ) g

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem mul_sub_left_distrib (n m k : Nat) : n * (m - k) = n * m - n * k

Proof state:
n m k : Nat
⊢ n * (m - k) = n * m - n * k

Tactic:
rw [Nat.mul_comm, Nat.mul_sub_right_distrib, Nat.mul_comm m n, Nat.mul_comm n k]

Result:
no goals
-- Mathlib/Data/ENat/Lattice.lean
lemma exists_eq_iSup₂_of_lt_top {ι₁ ι₂ : Type*} {f : ι₁ → ι₂ → ℕ∞} [Nonempty ι₁] [Nonempty ι₂]
    (h : ⨆ i, ⨆ j, f i j < ⊤) : ∃ i j, f i j = ⨆ i, ⨆ j, f i j

Proof state:
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ι₂ → ℕ∞
inst✝¹ : Nonempty ι₁
inst✝ : Nonempty ι₂
h : ⨆ i, ⨆ j, f i j < ⊤
⊢ ∃ i j, f i j = ⨆ i, ⨆ j, f i j

Tactic:
rw [iSup_prod'] at h ⊢

Result:
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ι₂ → ℕ∞
inst✝¹ : Nonempty ι₁
inst✝ : Nonempty ι₂
h : ⨆ x, f x.1 x.2 < ⊤
⊢ ∃ i j, f i j = ⨆ x, f x.1 x.2

Proof state:
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ι₂ → ℕ∞
inst✝¹ : Nonempty ι₁
inst✝ : Nonempty ι₂
h : ⨆ x, f x.1 x.2 < ⊤
⊢ ∃ i j, f i j = ⨆ x, f x.1 x.2

Tactic:
exact Prod.exists'.mp (exists_eq_iSup_of_lt_top h)

Result:
no goals
-- Mathlib/Data/Matroid/Dual.lean
theorem coindep_iff_subset_compl_isBase : M.Coindep X ↔ ∃ B, M.IsBase B ∧ X ⊆ M.E \ B

Proof state:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.Coindep X ↔ ∃ B, M.IsBase B ∧ X ⊆ M.E \ B

Tactic:
simp_rw [coindep_iff_exists', subset_diff]

Result:
α : Type u_1
M : Matroid α
X : Set α
⊢ (∃ B, M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X) ∧ X ⊆ M.E ↔ ∃ B, M.IsBase B ∧ X ⊆ M.E ∧ Disjoint X B

Proof state:
α : Type u_1
M : Matroid α
X : Set α
⊢ (∃ B, M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X) ∧ X ⊆ M.E ↔ ∃ B, M.IsBase B ∧ X ⊆ M.E ∧ Disjoint X B

Tactic:
exact ⟨fun ⟨⟨B, hB, _, hBX⟩, hX⟩ ↦ ⟨B, hB, hX, hBX.symm⟩,
  fun ⟨B, hB, hXE, hXB⟩ ↦ ⟨⟨B, hB, hB.subset_ground,  hXB.symm⟩, hXE⟩⟩

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem sZMod_eq_sMod (p : ℕ) (i : ℕ) : sZMod p i = (sMod p i : ZMod (2 ^ p - 1))

Proof state:
p i : ℕ
⊢ sZMod p i = ↑(sMod p i)

Tactic:
induction i <;> push_cast [← Int.coe_nat_two_pow_pred p, sMod, sZMod, *] <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_erase_self [LawfulBEq α] (h : m.WF) {k : α} [Inhabited (β k)] :
    (m.erase k).get! k = default

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
k : α
inst✝ : Inhabited (β k)
⊢ (m.erase k).get! k = default

Tactic:
simp_to_raw using Raw₀.get!_erase_self

Result:
no goals
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
lemma completedRiemannZeta_eq (s : ℂ) :
    completedRiemannZeta s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)

Proof state:
s : ℂ
⊢ completedRiemannZeta s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)

Tactic:
simp_rw [completedRiemannZeta, completedRiemannZeta₀, completedHurwitzZetaEven_eq, if_true]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem le_tsub_iff_le_tsub (ha : AddLECancellable a) (hc : AddLECancellable c)
    (h₁ : a ≤ b) (h₂ : c ≤ b) : a ≤ b - c ↔ c ≤ b - a

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h₁ : a ≤ b
h₂ : c ≤ b
⊢ a ≤ b - c ↔ c ≤ b - a

Tactic:
rw [ha.le_tsub_iff_left h₁, hc.le_tsub_iff_right h₂]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
@[simp]
lemma star_le_one_iff {x : R} : star x ≤ 1 ↔ x ≤ 1

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
⊢ star x ≤ 1 ↔ x ≤ 1

Tactic:
simpa using star_le_star_iff (x := x) (y := 1)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_eq_some_get! [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
    a ∈ m → m.get? a = some (m.get! a)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
a : α
inst✝ : Inhabited (β a)
⊢ a ∈ m → m.get? a = some (m.get! a)

Tactic:
simpa [mem_iff_contains] using get?_eq_some_get!_of_contains h

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem finrank_eq_nat_card_basis (h : Basis ι R M) :
    finrank R M = Nat.card ι

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
h : Basis ι R M
⊢ finrank R M = Nat.card ι

Tactic:
rw [Nat.card, ← toNat_lift.{v}, h.mk_eq_rank, toNat_lift, finrank]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_zero_sub_comm (a b : α) : toIocMod hp 0 (a - b) = p - toIcoMod hp 0 (b - a)

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

Tactic:
rw [← neg_sub, toIocMod_neg, neg_zero]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBase.ncard_eq_ncard_of_isBase (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) :
    B₁.ncard = B₂.ncard

Proof state:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ B₁.ncard = B₂.ncard

Tactic:
rw [ncard_def B₁, hB₁.encard_eq_encard_of_isBase hB₂, ← ncard_def]

Result:
no goals
-- Mathlib/Topology/Sets/OpenCover.lean
lemma exists_mem (hu : IsOpenCover u) (a : X) : ∃ i, a ∈ u i

Proof state:
ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
a : X
⊢ ∃ i, a ∈ u i

Tactic:
simpa [← hu.iSup_set_eq_univ] using mem_univ a

Result:
no goals
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem t0Space_iff_uniformity :
    T0Space α ↔ ∀ x y, (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y

Proof state:
α : Type u
inst✝ : UniformSpace α
⊢ T0Space α ↔ ∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y

Tactic:
simp only [t0Space_iff_inseparable, inseparable_iff_ker_uniformity, mem_ker, id]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/DotProduct.lean
theorem dotProduct_star_self_eq_zero {v : n → R} : dotProduct (star v) v = 0 ↔ v = 0 :=
  (Fintype.sum_eq_zero_iff_of_nonneg fun _ => star_mul_self_nonneg _).trans <|
    by simp [funext_iff, mul_eq_zero]

Proof state:
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
⊢ (fun i => star v i * v i) = 0 ↔ v = 0

Tactic:
simp [funext_iff, mul_eq_zero]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma IsCircuit.ssubset_indep (hC : M.IsCircuit C) (hXC : X ⊂ C) : M.Indep X

Proof state:
α : Type u_1
M : Matroid α
C X : Set α
hC : M.IsCircuit C
hXC : X ⊂ C
⊢ ¬M.Dep X

Tactic:
exact fun h ↦ hXC.ne ((isCircuit_iff.1 hC).2 h hXC.subset)

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
C X : Set α
hC : M.IsCircuit C
hXC : X ⊂ C
⊢ M.Indep X

Tactic:
rw [← not_dep_iff (hXC.subset.trans hC.subset_ground)]

Result:
α : Type u_1
M : Matroid α
C X : Set α
hC : M.IsCircuit C
hXC : X ⊂ C
⊢ ¬M.Dep X
-- Mathlib/Data/Finmap.lean
theorem induction_on {C : Finmap β → Prop} (s : Finmap β) (H : ∀ a : AList β, C ⟦a⟧) : C s

Proof state:
α : Type u
β : α → Type v
C : Finmap β → Prop
s : Finmap β
H : ∀ (a : AList β), C ⟦a⟧
⊢ C s

Tactic:
rcases s with ⟨⟨a⟩, h⟩

Result:
case mk.mk
α : Type u
β : α → Type v
C : Finmap β → Prop
H : ∀ (a : AList β), C ⟦a⟧
entries✝ : Multiset (Sigma β)
a : List (Sigma β)
h : Multiset.NodupKeys (Quot.mk (⇑(isSetoid (Sigma β))) a)
⊢ C { entries := Quot.mk (⇑(isSetoid (Sigma β))) a, nodupKeys := h }

Proof state:
case mk.mk
α : Type u
β : α → Type v
C : Finmap β → Prop
H : ∀ (a : AList β), C ⟦a⟧
entries✝ : Multiset (Sigma β)
a : List (Sigma β)
h : Multiset.NodupKeys (Quot.mk (⇑(isSetoid (Sigma β))) a)
⊢ C { entries := Quot.mk (⇑(isSetoid (Sigma β))) a, nodupKeys := h }

Tactic:
exact H ⟨a, h⟩

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem map_equiv_eq_comap_symm (e : M ≃ₛₗ[τ₁₂] M₂) (K : Submodule R M) :
    K.map (e : M →ₛₗ[τ₁₂] M₂) = K.comap (e.symm : M₂ →ₛₗ[τ₂₁] M) :=
  Submodule.ext fun _ => by rw [mem_map_equiv, mem_comap, LinearEquiv.coe_coe]

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R M
x✝ : M₂
⊢ x✝ ∈ map (↑e) K ↔ x✝ ∈ comap (↑e.symm) K

Tactic:
rw [mem_map_equiv, mem_comap, LinearEquiv.coe_coe]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_monomial : (monomial s a).eval₂ f g = f a * s.prod fun n e => g n ^ e :=
  Finsupp.sum_single_index (by simp [f.map_zero])

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
a : R
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
⊢ (f 0 * s.prod fun n e => g n ^ e) = 0

Tactic:
simp [f.map_zero]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem nil_diff (l : List α) : [].diff l = []

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
⊢ [].diff l = []

Tactic:
induction l <;> simp [*, erase_of_not_mem]

Result:
no goals
-- Mathlib/Analysis/Convex/Integral.lean
theorem ConcaveOn.average_mem_hypograph [IsFiniteMeasure μ] [NeZero μ] (hg : ConcaveOn ℝ s g)
    (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ x ∂μ, f x ∈ s)
    (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ) :
    (⨍ x, f x ∂μ, ⨍ x, g (f x) ∂μ) ∈ {p : E × ℝ | p.1 ∈ s ∧ p.2 ≤ g p.1}

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ p.2 ≤ g p.1}

Tactic:
simpa only [mem_setOf_eq, Pi.neg_apply, average_neg, neg_le_neg_iff] using
  hg.neg.average_mem_epigraph hgc.neg hsc hfs hfi hgi.neg

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma isIdempotentElemEquivClopens_symm_compl (s : Clopens (PrimeSpectrum R)) :
    isIdempotentElemEquivClopens.symm sᶜ = ⟨_, (isIdempotentElemEquivClopens.symm s).2.one_sub⟩ :=
  isIdempotentElemEquivClopens.symm_apply_eq.mpr <| by
    rw [isIdempotentElemEquivClopens_one_sub, Equiv.apply_symm_apply]

Proof state:
R : Type u
inst✝ : CommRing R
s : Clopens (PrimeSpectrum R)
⊢ sᶜ = isIdempotentElemEquivClopens ⟨1 - ↑(isIdempotentElemEquivClopens.symm s), ⋯⟩

Tactic:
rw [isIdempotentElemEquivClopens_one_sub, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem inner_smul_rotation_pi_div_two_right (x : V) (r : ℝ) :
    ⟪x, r • 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
r : ℝ
⊢ inner x (r • (o.rotation ↑(π / 2)) x) = 0

Tactic:
rw [real_inner_comm, inner_smul_rotation_pi_div_two_left]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem mul_pos_iff_of_pos_left [PosMulStrictMono α] [PosMulReflectLT α] (h : 0 < a) :
    0 < a * b ↔ 0 < b

Proof state:
α : Type u_3
a b : α
inst✝³ : MulZeroClass α
inst✝² : Preorder α
inst✝¹ : PosMulStrictMono α
inst✝ : PosMulReflectLT α
h : 0 < a
⊢ 0 < a * b ↔ 0 < b

Tactic:
simpa using mul_lt_mul_left (b := 0) h

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem sInf_toSubmodule (S : Set (NonUnitalSubalgebra R A)) :
    (sInf S).toSubmodule = sInf (NonUnitalSubalgebra.toSubmodule '' S) :=
  SetLike.coe_injective <| by simp

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : Set (NonUnitalSubalgebra R A)
⊢ ↑(sInf S).toSubmodule = ↑(sInf (NonUnitalSubalgebra.toSubmodule '' S))

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
theorem pre_map {A₁ A₂ A₃ : C} [Closed A₁] [Closed A₂] [Closed A₃] (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) :
    pre (f ≫ g) = pre g ≫ pre f

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
A₁ A₂ A₃ : C
inst✝² : Closed A₁
inst✝¹ : Closed A₂
inst✝ : Closed A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ pre (f ≫ g) = pre g ≫ pre f

Tactic:
rw [pre, pre, pre, conjugateEquiv_comp, (tensoringLeft C).map_comp]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem equiv_symm_eq_apply {X : C} {P : Cᵒᵖ ⥤ D} {S : J.Cover X} [HasMultiequalizer (S.index P)]
    (x : Meq P S) (I : S.Arrow) :
    -- We can hint `ConcreteCategory.hom (Y := P.obj (op I.Y))` below to put it into `simp`-normal
    -- form, but that doesn't seem to fix the `erw`s below...
    (Multiequalizer.ι (S.index P) I) ((Meq.equiv P S).symm x) = x I

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : PreservesLimits (forget D)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
inst✝ : HasMultiequalizer (S.index P)
x : Meq P S
I : S.Arrow
⊢ (ConcreteCategory.hom (Multiequalizer.ι (S.index P) I)) ((equiv P S).symm x) = ↑x I

Tactic:
simp [← GrothendieckTopology.Cover.index_left, ← equiv_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β} {h₁} :
    get (m.insertIfNew k v) a h₁ =
      if h₂ : k == a ∧ m.contains k = false then v
      else get m a (contains_of_contains_insertIfNew' _ h h₁ h₂)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
v : β
h₁ : (m.insertIfNew k v).contains a = true
⊢ get (m.insertIfNew k v) a h₁ = if h₂ : (k == a) = true ∧ m.contains k = false then v else get m a ⋯

Tactic:
simp_to_model [insertIfNew] using List.getValue_insertEntryIfNew

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem bind_none (x : Option α) : x.bind (fun _ => none (α := β)) = none

Proof state:
α : Type u_1
β : Type u_2
x : Option α
⊢ (x.bind fun x => none) = none

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma inter_pow_subset : (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

Proof state:
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

Tactic:
apply subset_inter <;> gcongr <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
lemma map_update [DecidableEq ι] (x : (i : ι) → M₁ i) (i : ι) (v : M₁ i)  :
    f (update x i v) = f x - f (update x i (x i - v))

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
x : (i : ι) → M₁ i
i : ι
v : M₁ i
⊢ f (update x i v) = f x - f (update x i (x i - v))

Tactic:
rw [map_update_sub, update_eq_self, sub_sub_cancel]

Result:
no goals
-- Mathlib/Logic/Encodable/Basic.lean
theorem mem_decode₂' [Encodable α] {n : ℕ} {a : α} :
    a ∈ decode₂ α n ↔ a ∈ decode n ∧ encode a = n

Proof state:
α : Type u_1
inst✝ : Encodable α
n : ℕ
a : α
⊢ a ∈ decode₂ α n ↔ a ∈ decode n ∧ encode a = n

Tactic:
simp [decode₂, bind_eq_some]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
@[to_additive] lemma IsUnit.pow (n : ℕ) : IsUnit a → IsUnit (a ^ n)

Proof state:
case intro
M : Type u_1
inst✝ : Monoid M
n : ℕ
u : Mˣ
⊢ IsUnit (↑u ^ n)

Tactic:
exact ⟨u ^ n, rfl⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
n : ℕ
⊢ IsUnit a → IsUnit (a ^ n)

Tactic:
rintro ⟨u, rfl⟩

Result:
case intro
M : Type u_1
inst✝ : Monoid M
n : ℕ
u : Mˣ
⊢ IsUnit (↑u ^ n)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma map_mk (x : R[X][Y]) : map W f (mk W x) = mk (W.map f) (x.map <| mapRingHom f)

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
x : R[X][Y]
⊢ eval₂ (AdjoinRoot.of (WeierstrassCurve.map W f).toAffine.polynomial)
      (AdjoinRoot.root (WeierstrassCurve.map W f).toAffine.polynomial) (Polynomial.map (mapRingHom f) x) =
    (mk (WeierstrassCurve.map W f)) (Polynomial.map (mapRingHom f) x)

Tactic:
exact AdjoinRoot.aeval_eq <| x.map <| mapRingHom f

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
x : R[X][Y]
⊢ (map W f) ((mk W) x) = (mk (WeierstrassCurve.map W f)) (Polynomial.map (mapRingHom f) x)

Tactic:
rw [map, AdjoinRoot.lift_mk, ← eval₂_map]

Result:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
x : R[X][Y]
⊢ eval₂ (AdjoinRoot.of (WeierstrassCurve.map W f).toAffine.polynomial)
      (AdjoinRoot.root (WeierstrassCurve.map W f).toAffine.polynomial) (Polynomial.map (mapRingHom f) x) =
    (mk (WeierstrassCurve.map W f)) (Polynomial.map (mapRingHom f) x)
-- Mathlib/Order/Interval/Finset/Basic.lean
lemma Icc_map_sectL : (Icc a b).map (.sectL _ c) = Icc (a, c) (b, c)

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : Preorder α
inst✝³ : PartialOrder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
c : β
⊢ map (Embedding.sectL α c) (Icc a b) = Icc (a, c) (b, c)

Tactic:
aesop (add safe forward [le_antisymm])

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem sign_zero : sign (0 : α) = 0

Proof state:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
⊢ sign 0 = 0

Tactic:
simp [sign_apply]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
@[simp] lemma inner_neg_right {x y : E} : ⟪x, -y⟫ = -⟪x, y⟫

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
x y : E
⊢ inner x (-y) = -inner x y

Tactic:
simp [← innerₛₗ_apply]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioi_union_left : Ioi a ∪ {a} = Ici a :=
  ext fun x => by simp [eq_comm, le_iff_eq_or_lt]

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a x : α
⊢ x ∈ Ioi a ∪ {a} ↔ x ∈ Ici a

Tactic:
simp [eq_comm, le_iff_eq_or_lt]

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

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' uIcc a (f i) = uIcc (update f i a) f

Tactic:
simpa using image_update_uIcc f i a (f i)

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem isAlgebraic_adjoin {S : Set L} (hS : ∀ x ∈ S, IsIntegral K x) :
    Algebra.IsAlgebraic K (adjoin K S)

Proof state:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
S : Set L
hS : ∀ x ∈ S, IsIntegral K x
⊢ Algebra.IsAlgebraic K ↥(⨆ i, K⟮↑i⟯)

Tactic:
exact isAlgebraic_iSup fun x ↦ isAlgebraic_adjoin_simple (hS x x.2)

Result:
no goals

Proof state:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
S : Set L
hS : ∀ x ∈ S, IsIntegral K x
⊢ Algebra.IsAlgebraic K ↥(adjoin K S)

Tactic:
rw [← biSup_adjoin_simple, ← iSup_subtype'']

Result:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
S : Set L
hS : ∀ x ∈ S, IsIntegral K x
⊢ Algebra.IsAlgebraic K ↥(⨆ i, K⟮↑i⟯)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α } : ¬a ∈ m → get? m a = none

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
a : α
⊢ ¬a ∈ m → get? m a = none

Tactic:
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem insertMany_list_singleton {k : α} {v : β k} [EquivBEq α] [LawfulHashable α] (h : m.WF) :
    m.insertMany [⟨k, v⟩] = m.insert k v

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
k : α
v : β k
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ (Raw₀.insertMany ⟨m, ⋯⟩ [⟨k, v⟩]).val.val = (Raw₀.insert ⟨m, ⋯⟩ k v).val

Tactic:
rw [Raw₀.insertMany_list_singleton]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
k : α
v : β k
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ m.insertMany [⟨k, v⟩] = m.insert k v

Tactic:
simp_to_raw

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
k : α
v : β k
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ (Raw₀.insertMany ⟨m, ⋯⟩ [⟨k, v⟩]).val.val = (Raw₀.insert ⟨m, ⋯⟩ k v).val
-- Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
theorem card [NeZero n] : Fintype.card (QuaternionGroup n) = 4 * n

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ n + n + (n + n) = 4 * n

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (QuaternionGroup n) = 4 * n

Tactic:
rw [← Fintype.card_eq.mpr ⟨fintypeHelper⟩, Fintype.card_sum, ZMod.card, two_mul]

Result:
n : ℕ
inst✝ : NeZero n
⊢ n + n + (n + n) = 4 * n
-- Mathlib/Analysis/Convex/StrictConvexSpace.lean
theorem norm_midpoint_lt_iff (h : ‖x‖ = ‖y‖) : ‖(1 / 2 : ℝ) • (x + y)‖ < ‖x‖ ↔ x ≠ y

Proof state:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
h : ‖x‖ = ‖y‖
⊢ ‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y

Tactic:
rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ←
  div_eq_inv_mul, div_lt_iff₀ (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h,
  not_sameRay_iff_norm_add_lt, h]

Result:
no goals