harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem Algebra.IsIntegral.finite [Algebra.IsIntegral R A] [h' : Algebra.FiniteType R A] :
    Module.Finite R A :=
  have ⟨s, hs⟩ := h'
  ⟨by apply hs ▸ fg_adjoin_of_finite s.finite_toSet fun x _ ↦ Algebra.IsIntegral.isIntegral x⟩

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsIntegral R A
h' : FiniteType R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ ⊤.FG

Tactic:
apply hs ▸ fg_adjoin_of_finite s.finite_toSet fun x _ ↦ Algebra.IsIntegral.isIntegral x

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
@[to_additive sum_le_sum]
lemma prod_le_prod' [Preorder M] [MulRightMono M]
    [MulLeftMono M] {l : List ι} {f g : ι → M} (h : ∀ i ∈ l, f i ≤ g i) :
    (l.map f).prod ≤ (l.map g).prod :=
  Forall₂.prod_le_prod' <| by simpa

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l : List ι
f g : ι → M
h : ∀ (i : ι), i ∈ l → f i ≤ g i
⊢ Forall₂ (fun x1 x2 => x1 ≤ x2) (map f l) (map g l)

Tactic:
simpa

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
lemma not_nil_iff {p : G.Walk v w} :
    ¬ p.Nil ↔ ∃ (u : V) (h : G.Adj v u) (q : G.Walk u w), p = cons h q

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ ¬p.Nil ↔ ∃ u, ∃ (h : G.Adj v u), ∃ q, p = cons h q

Tactic:
cases p <;> simp [*]

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndep_comap_mem_iff {f : ι → Set Ω} {_mΩ : MeasurableSpace Ω}
    {κ : Kernel α Ω} {μ : Measure α} :
    iIndep (fun i => MeasurableSpace.comap (· ∈ f i) ⊤) κ μ ↔ iIndepSet f κ μ

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
f : ι → Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
⊢ iIndep (fun i => MeasurableSpace.comap (fun x => x ∈ f i) ⊤) κ μ ↔ iIndepSet f κ μ

Tactic:
simp_rw [← generateFrom_singleton, iIndepSet]

Result:
no goals
-- Mathlib/Order/Category/Lat.lean
lemma hom_inv_apply {X Y : Lat} (e : X ≅ Y) (s : Y) : e.hom (e.inv s) = s

Proof state:
X Y : Lat
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
/-- A vector field on a vector space is `C^n` in the manifold sense iff it is `C^n` in the vector
space sense. -/
lemma contMDiff_vectorSpace_iff_contDiff
    {V : Π (x : E), TangentSpace 𝓘(𝕜, E) x} {n : ℕ∞} :
    ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E).tangent n (fun x ↦ (V x : TangentBundle 𝓘(𝕜, E) E)) ↔
      ContDiff 𝕜 n V

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
n : ℕ∞
⊢ (ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E).tangent ↑n fun x => { proj := x, snd := V x }) ↔ ContDiff 𝕜 (↑n) V

Tactic:
simp only [← contMDiffOn_univ, ← contDiffOn_univ, contMDiffOn_vectorSpace_iff_contDiffOn]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean
lemma mem_range_iff_of_surjective {S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) (e : X ⟶ Y)
    [Surjective e] (hge : e ≫ g = f) (s : S) : s ∈ Set.range f.base ↔ s ∈ Set.range g.base

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst✝ : Surjective e
hge : e ≫ g = f
s : ↑↑S.toPresheafedSpace
⊢ s ∈ Set.range ⇑(ConcreteCategory.hom f.base) ↔ s ∈ Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
rw [range_eq_range_of_surjective f g e hge]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackCone.lean
theorem coequalizer_ext (t : PushoutCocone f g) {W : C} {k l : t.pt ⟶ W}
    (h₀ : inl t ≫ k = inl t ≫ l) (h₁ : inr t ≫ k = inr t ≫ l) :
    ∀ j : WalkingSpan, t.ι.app j ≫ k = t.ι.app j ≫ l
  | some WalkingPair.left => h₀
  | some WalkingPair.right => h₁
  | none => by rw [← t.w fst, Category.assoc, Category.assoc, h₀]

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
W : C
k l : t.pt ⟶ W
h₀ : t.inl ≫ k = t.inl ≫ l
h₁ : t.inr ≫ k = t.inr ≫ l
⊢ t.ι.app none ≫ k = t.ι.app none ≫ l

Tactic:
rw [← t.w fst, Category.assoc, Category.assoc, h₀]

Result:
no goals
-- Mathlib/Topology/UnitInterval.lean
theorem symm_lt_symm {i j : I} : σ i < σ j ↔ j < i

Proof state:
i j : ↑I
⊢ σ i < σ j ↔ j < i

Tactic:
simp only [symm, Subtype.mk_lt_mk, sub_lt_sub_iff_left, Subtype.coe_lt_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_alter_eq_isEmpty_erase [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
    (h : m.WF) : (m.alter k f).isEmpty = ((m.erase k).isEmpty && (f (m.get? k)).isNone)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).isEmpty = ((m.erase k).isEmpty && (f (m.get? k)).isNone)

Tactic:
simp_to_raw using Raw₀.isEmpty_alter_eq_isEmpty_erase

Result:
no goals
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem prime_mul_iff {a b : ℕ} : Nat.Prime (a * b) ↔ a.Prime ∧ b = 1 ∨ b.Prime ∧ a = 1

Proof state:
a b : ℕ
⊢ Prime (a * b) ↔ Prime a ∧ b = 1 ∨ Prime b ∧ a = 1

Tactic:
simp only [irreducible_mul_iff, ← irreducible_iff_nat_prime, Nat.isUnit_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_isBilimit {b : BinaryBicone X Y} (h : b.IsBilimit) :
    IsPullback b.fst b.snd (0 : X ⟶ 0) (0 : Y ⟶ 0)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback b.fst b.snd 0 0

Tactic:
convert IsPullback.of_is_product' h.isLimit HasZeroObject.zeroIsTerminal
  <;> subsingleton

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
lemma add_right_inj [IsRightCancelAdd α] (hz : z ≠ ⊥) : x + z = y + z ↔ x = y

Proof state:
case intro
α : Type u
inst✝¹ : Add α
x y : WithBot α
inst✝ : IsRightCancelAdd α
z : α
⊢ x + ↑z = y + ↑z ↔ x = y

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Add α
x y z : WithBot α
inst✝ : IsRightCancelAdd α
hz : z ≠ ⊥
⊢ x + z = y + z ↔ x = y

Tactic:
lift z to α using hz

Result:
case intro
α : Type u
inst✝¹ : Add α
x y : WithBot α
inst✝ : IsRightCancelAdd α
z : α
⊢ x + ↑z = y + ↑z ↔ x = y
-- Mathlib/Order/Bounds/Basic.lean
theorem isLUB_congr (h : upperBounds s = upperBounds t) : IsLUB s a ↔ IsLUB t a

Proof state:
α : Type u
inst✝ : Preorder α
s t : Set α
a : α
h : upperBounds s = upperBounds t
⊢ IsLUB s a ↔ IsLUB t a

Tactic:
rw [IsLUB, IsLUB, h]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
theorem abs_dvd (a b : α) : |a| ∣ b ↔ a ∣ b

Proof state:
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a b : α
⊢ |a| ∣ b ↔ a ∣ b

Tactic:
rcases abs_choice a with h | h <;> simp only [h, neg_dvd]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem inv_mem_nhds_one {S : Set G} (hS : S ∈ (𝓝 1 : Filter G)) : S⁻¹ ∈ 𝓝 (1 : G)

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Set G
hS : S ∈ 𝓝 1
⊢ S⁻¹ ∈ 𝓝 1

Tactic:
rwa [← nhds_one_symm'] at hS

Result:
no goals
-- Mathlib/Algebra/DirectSum/Module.lean
theorem IsInternal.isCompl {A : ι → Submodule R M} {i j : ι} (hij : i ≠ j)
    (h : (Set.univ : Set ι) = {i, j}) (hi : IsInternal A) : IsCompl (A i) (A j) :=
  ⟨hi.submodule_iSupIndep.pairwiseDisjoint hij,
    codisjoint_iff.mpr <| Eq.symm <| hi.submodule_iSup_eq_top.symm.trans <| by
      rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]⟩

Proof state:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
hi : IsInternal A
⊢ iSup A = A i ⊔ A j

Tactic:
rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem comap_dist_right_atTop (c : α) : comap (dist · c) atTop = cobounded α :=
  (atTop_basis.comap _).eq_of_same_basis <| by
    simpa only [compl_def, mem_ball, not_lt] using hasBasis_cobounded_compl_ball c

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
c : α
⊢ (cobounded α).HasBasis (fun x => True) fun i => (fun x => dist x c) ⁻¹' Ici i

Tactic:
simpa only [compl_def, mem_ball, not_lt] using hasBasis_cobounded_compl_ball c

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive nsmul_zero_sub]
lemma one_div_pow (a : α) (n : ℕ) : (1 / a) ^ n = 1 / a ^ n

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ (1 / a) ^ n = 1 / a ^ n

Tactic:
simp only [one_div, inv_pow]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem cthickening_closedBall (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (x : E) :
    cthickening ε (closedBall x δ) = closedBall x (ε + δ)

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : E
⊢ cthickening ε (Metric.closedBall x δ) = Metric.closedBall x (ε + δ)

Tactic:
rw [← cthickening_singleton _ hδ, cthickening_cthickening hε hδ,
    cthickening_singleton _ (add_nonneg hε hδ)]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem norm_cpow_real (x : ℂ) (y : ℝ) : ‖x ^ (y : ℂ)‖ = ‖x‖ ^ y

Proof state:
x : ℂ
y : ℝ
⊢ ‖x ^ ↑y‖ = ‖x‖ ^ y

Tactic:
rw [norm_cpow_of_imp] <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_conj_coe_angle (x : ℂ) : (arg (conj x) : Real.Angle) = -arg x

Proof state:
x : ℂ
⊢ ↑((starRingEnd ℂ) x).arg = -↑x.arg

Tactic:
by_cases h : arg x = π <;> simp [arg_conj, h]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_ofReal_im (x : ℝ) : (cosh x).im = 0

Proof state:
x : ℝ
⊢ (cosh ↑x).im = 0

Tactic:
rw [← ofReal_cosh_ofReal_re, ofReal_im]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem isPredPrelimit_toDual_iff : IsPredPrelimit (toDual a) ↔ IsSuccPrelimit a

Proof state:
α : Type u_1
a : α
inst✝ : LT α
⊢ IsPredPrelimit (toDual a) ↔ IsSuccPrelimit a

Tactic:
simp [IsSuccPrelimit, IsPredPrelimit]

Result:
no goals
-- Mathlib/SetTheory/Lists.lean
theorem to_ofList (l : List (Lists α)) : toList (ofList l) = l

Proof state:
α : Type u_1
l : List (Lists α)
⊢ (ofList l).toList = l

Tactic:
simp [ofList, of']

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isClosed_range_inr : IsClosed (range (inr : Y → X ⊕ Y))

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosed (range inr)

Tactic:
rw [← isOpen_compl_iff, compl_range_inr]

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsOpen (range inl)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsOpen (range inl)

Tactic:
exact isOpen_range_inl

Result:
no goals
-- Mathlib/Tactic/NormNum/Result.lean
theorem IsRat.of_raw (α) [DivisionRing α] (n : ℤ) (d : ℕ)
    (h : (d : α) ≠ 0) : IsRat (Rat.rawCast n d : α) n d :=
  have := invertibleOfNonzero h
  ⟨this, by simp [div_eq_mul_inv]⟩

Proof state:
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : ↑d ≠ 0
this : Invertible ↑d
⊢ Rat.rawCast n d = ↑n * ⅟↑d

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem coe_sumPiEquivProdPi (α : δ ⊕ δ' → Type*) [∀ i, MeasurableSpace (α i)] :
    ⇑(MeasurableEquiv.sumPiEquivProdPi α) = Equiv.sumPiEquivProdPi α

Proof state:
δ : Type u_4
δ' : Type u_5
α : δ ⊕ δ' → Type u_8
inst✝ : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ ⇑(sumPiEquivProdPi α) = ⇑(Equiv.sumPiEquivProdPi α)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_le_sqrt_iff (hy : 0 ≤ y) : √x ≤ √y ↔ x ≤ y

Proof state:
x y : ℝ
hy : 0 ≤ y
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
rw [Real.sqrt, Real.sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt, toNNReal_le_toNNReal_iff hy]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Monoid.lean
theorem image_const_add_Ico : (fun x => a + x) '' Ico b c = Ico (a + b) (a + c)

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c : M
⊢ (fun x => a + x) '' Ico b c = Ico (a + b) (a + c)

Tactic:
simp only [add_comm a, image_add_const_Ico]

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublistsLen_length : ∀ l : List α, sublistsLen l.length l = [l]
  | [] => rfl
  | a :: l => by
    simp only [length, sublistsLen_succ_cons, sublistsLen_length, map,
      sublistsLen_of_length_lt (lt_succ_self _), nil_append]

Proof state:
α : Type u
a : α
l : List α
⊢ sublistsLen (a :: l).length (a :: l) = [a :: l]

Tactic:
simp only [length, sublistsLen_succ_cons, sublistsLen_length, map,
  sublistsLen_of_length_lt (lt_succ_self _), nil_append]

Result:
no goals
-- Mathlib/Tactic/Linarith/Lemmas.lean
theorem eq_of_eq_of_eq {α} [OrderedSemiring α] {a b : α} (ha : a = 0) (hb : b = 0) : a + b = 0

Proof state:
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a = 0
hb : b = 0
⊢ a + b = 0

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Algebra/Category/Semigrp/Basic.lean
@[to_additive]
lemma id_apply (X : Semigrp) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : Semigrp
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_set_ne (v : Vector α n) (i : Nat) (hi : i < n) (x : α) (j : Nat)
    (h : i ≠ j) : (v.set i x hi)[j]? = v[j]?

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
hi : i < n
x : α
j : Nat
h : i ≠ j
⊢ (v.set i x hi)[j]? = v[j]?

Tactic:
simp [getElem?_set, h]

Result:
no goals
-- Mathlib/Logic/Equiv/Option.lean
lemma optionSubtypeNe_symm_of_ne (hba : b ≠ a) : (optionSubtypeNe a).symm b = some ⟨b, hba⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
hba : b ≠ a
⊢ (optionSubtypeNe a).symm b = some ⟨b, hba⟩

Tactic:
simp [hba]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
@[reassoc]
lemma pullback.comp_diagonal (f : X ⟶ Y) (g : Y ⟶ Z) :
    f ≫ pullback.diagonal g = pullback.diagonal (f ≫ g) ≫
      pullback.map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) (by simp) (by simp)

Proof state:
C : Type u_1
inst✝⁵ : Category.{?u.822808, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X ⟶ T
g✝ : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ : HasPullback (diagonal i) (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) ⋯ ⋯)
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g) ≫ 𝟙 Z = f ≫ g

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ diagonal g = diagonal (f ≫ g) ≫ map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Action/Basic.lean
theorem hom_inv_hom {M N : Action V G} (f : M ≅ N) :
    f.hom.hom ≫ f.inv.hom = 𝟙 M.V

Proof state:
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : Type u
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 M.V

Tactic:
rw [← comp_hom, Iso.hom_inv_id, id_hom]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mod_zero (a : Ordinal) : a % 0 = a

Proof state:
a : Ordinal.{u_4}
⊢ a % 0 = a

Tactic:
simp only [mod_def, div_zero, zero_mul, sub_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_iff_exists [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} :
    containsKey a l ↔ ∃ a' ∈ keys l, a == a'

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a : α
⊢ containsKey a l = true ↔ ∃ a', a' ∈ keys l ∧ (a == a') = true

Tactic:
rw [containsKey_eq_keys_contains, List.contains_iff_exists_mem_beq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem back?_attach {xs : Vector α n} :
    xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩

Proof state:
case mk
α : Type u_1
n : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.attach.back? =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.back?.pbind fun a h => some ⟨a, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
⊢ xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, ⋯⟩

Tactic:
cases xs

Result:
case mk
α : Type u_1
n : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.attach.back? =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.back?.pbind fun a h => some ⟨a, ⋯⟩
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma isIso_pOpcycles : IsIso (K.pOpcycles j)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hi : c.prev j = i
h : K.d i j = 0
inst✝ : K.HasHomology j
⊢ IsIso (K.pOpcycles j)

Tactic:
obtain rfl := hi

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
j : ι
inst✝ : K.HasHomology j
h : K.d (c.prev j) j = 0
⊢ IsIso (K.pOpcycles j)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
j : ι
inst✝ : K.HasHomology j
h : K.d (c.prev j) j = 0
⊢ IsIso (K.pOpcycles j)

Tactic:
exact ShortComplex.isIso_pOpcycles _ h

Result:
no goals
-- Mathlib/Data/Fin/Fin2.lean
@[simp] lemma rev_rev {n} (i : Fin2 n) : i.rev.rev = i

Proof state:
n : ℕ
i : Fin2 n
⊢ i.rev.rev = i

Tactic:
induction i <;> simp_all [rev]

Result:
no goals
-- Mathlib/Combinatorics/Additive/Dissociation.lean
@[to_additive (attr := simp)] lemma mulDissociated_empty : MulDissociated (∅ : Set α)

Proof state:
α : Type u_1
inst✝ : CommGroup α
⊢ MulDissociated ∅

Tactic:
simp [MulDissociated, subset_empty_iff]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_add : cosh (x + y) = cosh x * cosh y + sinh x * sinh y

Proof state:
x y : ℂ
⊢ (cexp x + cexp (-x)) * (cexp y + cexp (-y)) + (cexp x - cexp (-x)) * (cexp y - cexp (-y)) =
    2 * (cexp x * cexp y + cexp (-x) * cexp (-y))

Tactic:
exact cosh_add_aux

Result:
no goals

Proof state:
x y : ℂ
⊢ cosh (x + y) = cosh x * cosh y + sinh x * sinh y

Tactic:
rw [← mul_right_inj' (two_ne_zero' ℂ), two_cosh, exp_add, neg_add, exp_add, eq_comm, mul_add, ←
  mul_assoc, two_cosh, ← mul_assoc, two_sinh, ← mul_right_inj' (two_ne_zero' ℂ), mul_add,
  mul_left_comm, two_cosh, mul_left_comm, two_sinh]

Result:
x y : ℂ
⊢ (cexp x + cexp (-x)) * (cexp y + cexp (-y)) + (cexp x - cexp (-x)) * (cexp y - cexp (-y)) =
    2 * (cexp x * cexp y + cexp (-x) * cexp (-y))
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem fieldRange_comp_val : (f.comp L.val).fieldRange = L.map f := toSubalgebra_injective <| by
  rw [toSubalgebra_map, AlgHom.fieldRange_toSubalgebra, AlgHom.range_comp, range_val]

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
L : IntermediateField F E
f : E →ₐ[F] K
⊢ (f.comp L.val).fieldRange.toSubalgebra = (map f L).toSubalgebra

Tactic:
rw [toSubalgebra_map, AlgHom.fieldRange_toSubalgebra, AlgHom.range_comp, range_val]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem snoc_last : snoc p x (last n) = x

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
⊢ snoc p x (last n) = x

Tactic:
simp [snoc]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff (x : L) (i : ℕ) :
    MvPolynomial.eval (b.repr x) ((polyCharpolyAux φ b bₘ).coeff i) =
      (toMatrix bₘ bₘ (φ x)).charpoly.coeff i

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
φ : L →ₗ[R] Module.End R M
inst✝³ : Fintype ι
inst✝² : Fintype ιM
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
x : L
i : ℕ
⊢ (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) = ((toMatrix bₘ bₘ) (φ x)).charpoly.coeff i

Tactic:
simp [← polyCharpolyAux_map_eq_toMatrix_charpoly φ b bₘ x]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem dite_then_true {p : Prop} [Decidable p] {x : ¬ p → Prop} : (if h : p then True else x h) ↔ ∀ h : ¬ p, x h

Proof state:
p : Prop
inst✝ : Decidable p
x : ¬p → Prop
⊢ (if h : p then True else x h) ↔ ∀ (h : ¬p), x h

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem of_mem_support_derivative {p : R[X]} {n : ℕ} (h : n ∈ p.derivative.support) :
    n + 1 ∈ p.support :=
  mem_support_iff.2 fun h1 : p.coeff (n + 1) = 0 =>
    mem_support_iff.1 h <| show p.derivative.coeff n = 0 by rw [coeff_derivative, h1, zero_mul]

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n ∈ (derivative p).support
h1 : p.coeff (n + 1) = 0
⊢ (derivative p).coeff n = 0

Tactic:
rw [coeff_derivative, h1, zero_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem apply_cond (f : α → β) {b : Bool} {a a' : α} :
    f (bif b then a else a') = bif b then f a else f a'

Proof state:
α : Type u_1
β : Type u_2
f : α → β
b : Bool
a a' : α
⊢ f (bif b then a else a') = bif b then f a else f a'

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/RootSystem.lean
lemma chainLength_smul {x} (hx : x ∈ rootSpace H (chainTop α β)) :
    (chainLength α β : K) • x = ⁅coroot α, x⁆

Proof state:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
⊢ ↑(chainLength α β) • x = ⁅coroot α, x⁆

Tactic:
rw [Nat.cast_smul_eq_nsmul, chainLength_nsmul _ _ hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) :
    (Const.modify m k f).isEmpty = m.isEmpty

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : β → β
h : m.WF
⊢ (modify m k f).isEmpty = m.isEmpty

Tactic:
simp_to_raw using Raw₀.Const.isEmpty_modify

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
lemma card_filter (p) [DecidablePred p] (s : Finset ι) :
    #{i ∈ s | p i} = ∑ i ∈ s, ite (p i) 1 0

Proof state:
ι : Type u_1
p : ι → Prop
inst✝ : DecidablePred p
s : Finset ι
⊢ #(filter (fun i => p i) s) = ∑ i ∈ s, if p i then 1 else 0

Tactic:
simp [sum_ite]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_mem_multiset [DecidableEq α] (m : Multiset α) (f : { x // x ∈ m } → β) (g : α → β)
    (hfg : ∀ x, f x = g x) : ∏ x : { x // x ∈ m }, f x = ∏ x ∈ m.toFinset, g x

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
m : Multiset α
f : { x // x ∈ m } → β
g : α → β
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∏ x : { x // x ∈ m }, f x = ∏ x ∈ m.toFinset, g x

Tactic:
refine prod_bij' (fun x _ ↦ x) (fun x hx ↦ ⟨x, Multiset.mem_toFinset.1 hx⟩) ?_ ?_ ?_ ?_ ?_ <;>
  simp [hfg]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem divInt_ofNat (num den) : num /. (den : Nat) = mkRat num den

Proof state:
num : Int
den : Nat
⊢ num /. ↑den = mkRat num den

Tactic:
simp [divInt, normalize_eq_mkRat]

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem orderEmbOfFin_singleton (a : α) (i : Fin 1) :
    orderEmbOfFin {a} (card_singleton a) i = a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a : α
i : Fin 1
⊢ ({a}.orderEmbOfFin ⋯) i = a

Tactic:
rw [Subsingleton.elim i ⟨0, Nat.zero_lt_one⟩, orderEmbOfFin_zero _ Nat.zero_lt_one,
  min'_singleton]

Result:
no goals