harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Seminorm.lean
theorem ball_sup (p : Seminorm 𝕜 E) (q : Seminorm 𝕜 E) (e : E) (r : ℝ) :
    ball (p ⊔ q) e r = ball p e r ∩ ball q e r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ (p ⊔ q).ball e r = p.ball e r ∩ q.ball e r

Tactic:
simp_rw [ball, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_lt_iff]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem filter_eq_self_iff : f.filter p = f ↔ ∀ x, f x ≠ 0 → p x

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
⊢ filter p f = f ↔ ∀ (x : α), f x ≠ 0 → p x

Tactic:
simp only [DFunLike.ext_iff, filter_eq_indicator, Set.indicator_apply_eq_self, Set.mem_setOf_eq,
  not_imp_comm]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem closedComplemented_bot : ClosedComplemented (⊥ : Submodule R M) :=
  ⟨0, fun x => by simp only [zero_apply, eq_zero_of_bot_submodule x]⟩

Proof state:
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↥⊥
⊢ 0 ↑x = x

Tactic:
simp only [zero_apply, eq_zero_of_bot_submodule x]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem not_eq_key {a} {l : List (Sigma β)} : a ∉ l.keys ↔ ∀ s : Sigma β, s ∈ l → a ≠ s.1 :=
  Iff.intro (fun h₁ s h₂ e => absurd (mem_keys_of_mem h₂) (by rwa [e] at h₁)) fun f h₁ =>
    let ⟨_, h₂⟩ := exists_of_mem_keys h₁
    f _ h₂ rfl

Proof state:
α : Type u
β : α → Type v
a : α
l : List (Sigma β)
h₁ : a ∉ l.keys
s : Sigma β
h₂ : s ∈ l
e : a = s.fst
⊢ s.fst ∉ l.keys

Tactic:
rwa [e] at h₁

Result:
no goals
-- Mathlib/GroupTheory/DoubleCoset.lean
theorem eq (H K : Subgroup G) (a b : G) :
    mk H K a = mk H K b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
⊢ mk H K a = mk H K b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Tactic:
rw [Quotient.eq'']

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
⊢ (setoid ↑H ↑K) a b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
⊢ (setoid ↑H ↑K) a b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Tactic:
apply rel_iff

Result:
no goals
-- Mathlib/Analysis/Convex/Hull.lean
theorem convexHull_nonempty_iff : (convexHull 𝕜 s).Nonempty ↔ s.Nonempty

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ ¬(convexHull 𝕜) s = ∅ ↔ ¬s = ∅

Tactic:
exact not_congr convexHull_empty_iff

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ ((convexHull 𝕜) s).Nonempty ↔ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty, nonempty_iff_ne_empty, Ne, Ne]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ ¬(convexHull 𝕜) s = ∅ ↔ ¬s = ∅
-- Mathlib/GroupTheory/Perm/Support.lean
theorem disjoint_conj (h : Perm α) : Disjoint (h * f * h⁻¹) (h * g * h⁻¹) ↔ Disjoint f g :=
  (h⁻¹).forall_congr fun {_} ↦ by simp only [mul_apply, eq_inv_iff_eq]

Proof state:
α : Type u_1
f g h : Perm α
x✝ : α
⊢ (h * f * h⁻¹) x✝ = x✝ ∨ (h * g * h⁻¹) x✝ = x✝ ↔ f (h⁻¹ x✝) = h⁻¹ x✝ ∨ g (h⁻¹ x✝) = h⁻¹ x✝

Tactic:
simp only [mul_apply, eq_inv_iff_eq]

Result:
no goals
-- Mathlib/Data/Fintype/Defs.lean
theorem nodup_map_univ_iff_injective [Fintype α] {f : α → β} :
    (Multiset.map f univ.val).Nodup ↔ Function.Injective f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
f : α → β
⊢ (Multiset.map f univ.val).Nodup ↔ Injective f

Tactic:
rw [nodup_map_iff_injOn, coe_univ, Set.injective_iff_injOn_univ]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem gcd_eq_zero_iff (a : ℤ√d) : Int.gcd a.re a.im = 0 ↔ a = 0

Proof state:
d : ℤ
a : ℤ√d
⊢ a.re.gcd a.im = 0 ↔ a = 0

Tactic:
simp only [Int.gcd_eq_zero_iff, Zsqrtd.ext_iff, eq_self_iff_true, zero_im, zero_re]

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem range_eq_top {f : R →+* S} :
    f.range = (⊤ : Subring S) ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_range, coe_top]) Set.range_eq_univ

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ ↑f.range = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
rw [coe_range, coe_top]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProdFun_empty (κ : Kernel α β) (η : Kernel (α × β) γ) (a : α) :
    compProdFun κ η a ∅ = 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
a : α
⊢ κ.compProdFun η a ∅ = 0

Tactic:
simp only [compProdFun, Set.mem_empty_iff_false, Set.setOf_false, measure_empty,
  MeasureTheory.lintegral_const, zero_mul]

Result:
no goals
-- Mathlib/Tactic/NormNum/Basic.lean
theorem isRat_div {α : Type u} [DivisionRing α] : {a b : α} → {cn : ℤ} → {cd : ℕ} →
    IsRat (a * b⁻¹) cn cd → IsRat (a / b) cn cd
  | _, _, _, _, h => by simpa [div_eq_mul_inv] using h

Proof state:
α : Type u
inst✝ : DivisionRing α
x✝³ x✝² : α
x✝¹ : ℤ
x✝ : ℕ
h : IsRat (x✝³ * x✝²⁻¹) x✝¹ x✝
⊢ IsRat (x✝³ / x✝²) x✝¹ x✝

Tactic:
simpa [div_eq_mul_inv] using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
    (f : α → β → m (ForInStep β)) (init : β) (l : Array α) :
    forIn l init f = ForInStep.value <$>
      l.foldlM (fun b a => match b with
        | .yield b => f a b
        | .done b => pure (.done b)) (ForInStep.yield init)

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
init : β
toList✝ : List α
⊢ ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) toList✝ =
    ForInStep.value <$>
      List.foldlM
        (fun x y =>
          match x with
          | ForInStep.yield b => f y b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) toList✝

Tactic:
congr

Result:
no goals

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
init : β
toList✝ : List α
⊢ forIn { toList := toList✝ } init f =
    ForInStep.value <$>
      foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) { toList := toList✝ }

Tactic:
simp only [List.forIn_toArray, List.forIn_eq_foldlM, size_toArray, List.foldlM_toArray']

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
init : β
toList✝ : List α
⊢ ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) toList✝ =
    ForInStep.value <$>
      List.foldlM
        (fun x y =>
          match x with
          | ForInStep.yield b => f y b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) toList✝

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
init : β
l : Array α
⊢ forIn l init f =
    ForInStep.value <$>
      foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
init : β
toList✝ : List α
⊢ forIn { toList := toList✝ } init f =
    ForInStep.value <$>
      foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) { toList := toList✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem forall_mem_append {p : α → Prop} {l₁ l₂ : List α} :
    (∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x)

Proof state:
α : Type u_1
p : α → Prop
l₁ l₂ : List α
⊢ (∀ (x : α), x ∈ l₁ ++ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x

Tactic:
simp only [mem_append, or_imp, forall_and]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_image_le (h : LipschitzOnWith K f s) {d : ℝ} (hd : 0 ≤ d) :
    μH[d] (f '' s) ≤ (K : ℝ≥0∞) ^ d * μH[d] s

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
K : ℝ≥0
f : X → Y
s : Set X
h : LipschitzOnWith K f s
d : ℝ
hd : 0 ≤ d
⊢ μH[d] (f '' s) ≤ ↑K ^ d * μH[d] s

Tactic:
simpa only [NNReal.coe_one, one_mul] using h.holderOnWith.hausdorffMeasure_image_le zero_lt_one hd

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem mem_finset_inf {ι} {s : Finset ι} {p : ι → Submodule R M} {x : M} :
    x ∈ s.inf p ↔ ∀ i ∈ s, x ∈ p i

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
x : M
⊢ x ∈ s.inf p ↔ ∀ i ∈ s, x ∈ p i

Tactic:
simp only [← SetLike.mem_coe, finset_inf_coe, Set.mem_iInter]

Result:
no goals
-- Mathlib/Control/EquivFunctor.lean
theorem mapEquiv.injective (f : Type u₀ → Type u₁)
    [Applicative f] [LawfulApplicative f] {α β : Type u₀}
    (h : ∀ γ, Function.Injective (pure : γ → f γ)) :
      Function.Injective (@EquivFunctor.mapEquiv f _ α β) :=
  fun e₁ e₂ H =>
    Equiv.ext fun x => h β (by simpa [EquivFunctor.map] using Equiv.congr_fun H (pure x))

Proof state:
f : Type u₀ → Type u₁
inst✝¹ : Applicative f
inst✝ : LawfulApplicative f
α β : Type u₀
h : ∀ (γ : Type u₀), Injective pure
e₁ e₂ : α ≃ β
H : mapEquiv f e₁ = mapEquiv f e₂
x : α
⊢ pure (e₁ x) = pure (e₂ x)

Tactic:
simpa [EquivFunctor.map] using Equiv.congr_fun H (pure x)

Result:
no goals
-- Mathlib/Analysis/Calculus/Implicit.lean
theorem mem_implicitToPartialHomeomorphOfComplemented_target (hf : HasStrictFDerivAt f f' a)
    (hf' : range f' = ⊤) (hker : (ker f').ClosedComplemented) :
    (f a, (0 : ker f')) ∈ (hf.implicitToPartialHomeomorphOfComplemented f f' hf' hker).target

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : (LinearMap.ker f').ClosedComplemented
⊢ (f a, 0) ∈ (implicitToPartialHomeomorphOfComplemented f f' hf hf' hker).target

Tactic:
simpa only [implicitToPartialHomeomorphOfComplemented_self] using
  (hf.implicitToPartialHomeomorphOfComplemented f f' hf' hker).map_source <|
    hf.mem_implicitToPartialHomeomorphOfComplemented_source hf' hker

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma baseChange_addX : (W'.baseChange B).toAffine.addX (f x₁) (f x₂) (f ℓ) =
    f ((W'.baseChange A).toAffine.addX x₁ x₂ ℓ)

Proof state:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
x₁ x₂ ℓ : A
⊢ (baseChange W' B).toAffine.addX (f x₁) (f x₂) (f ℓ) = f ((baseChange W' A).toAffine.addX x₁ x₂ ℓ)

Tactic:
rw [← RingHom.coe_coe, ← map_addX, map_baseChange]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List α} {k : α} :
    get? (insertManyIfNewUnit m l).1 k =
    if m.contains k ∨ l.contains k then some () else none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
k : α
⊢ get? (insertManyIfNewUnit m l).val k = if m.contains k = true ∨ l.contains k = true then some () else none

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.getValue?_insertListIfNewUnit

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem normSq_intCast (z : ℤ) : normSq (z : ℍ[R]) = (z : R) ^ 2

Proof state:
R : Type u_3
inst✝ : CommRing R
z : ℤ
⊢ normSq ↑z = ↑z ^ 2

Tactic:
rw [← coe_intCast, normSq_coe]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullback.diagonal_comp (f : X ⟶ Y) (g : Y ⟶ Z) :
    diagonal (f ≫ g) = diagonal f ≫ (pullbackDiagonalMapIdIso f f g).inv ≫ pullback.snd _ _

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
⊢ diagonal (f ≫ g) =
    diagonal f ≫ (pullbackDiagonalMapIdIso f f g).inv ≫ snd (diagonal g) (map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Degree.lean
theorem natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree {x : RatFunc K}
    (hx : x ≠ 0) {s : K[X]} (hs : s ≠ 0) :
    ((x.num * s).natDegree : ℤ) - (s * x.denom).natDegree = x.intDegree

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
⊢ x.num * s * x.denom = x.num * (s * x.denom)

Tactic:
rw [mul_assoc]

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
⊢ ↑(x.num * s).natDegree - ↑(s * x.denom).natDegree = x.intDegree

Tactic:
apply natDegree_sub_eq_of_prod_eq (mul_ne_zero (num_ne_zero hx) hs)
  (mul_ne_zero hs x.denom_ne_zero) (num_ne_zero hx) x.denom_ne_zero

Result:
K : Type u
inst✝ : Field K
x : RatFunc K
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
⊢ x.num * s * x.denom = x.num * (s * x.denom)
-- Mathlib/Data/Finset/Option.lean
theorem eraseNone_insertNone (s : Finset α) : eraseNone (insertNone s) = s

Proof state:
case h
α : Type u_1
s : Finset α
a✝ : α
⊢ a✝ ∈ eraseNone (insertNone s) ↔ a✝ ∈ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
⊢ eraseNone (insertNone s) = s

Tactic:
ext

Result:
case h
α : Type u_1
s : Finset α
a✝ : α
⊢ a✝ ∈ eraseNone (insertNone s) ↔ a✝ ∈ s
-- Mathlib/FieldTheory/Relrank.lean
theorem lift_relrank_map_map (f : E →ₐ[F] L) :
    Cardinal.lift.{v} (relrank (A.map f) (B.map f)) = Cardinal.lift.{w} (relrank A B)

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : Type w
inst✝¹ : Field L
inst✝ : Algebra F L
A B : IntermediateField F E
f : E →ₐ[F] L
⊢ Cardinal.lift.{v, w} ((map f A).relrank (map f B)) = Cardinal.lift.{w, v} (A.relrank B)

Tactic:
rw [← lift_relrank_comap, comap_map]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem max?_reverse (t : RBNode α) : t.reverse.max? = t.min?

Proof state:
α : Type u_1
t : RBNode α
⊢ t.reverse.max? = t.min?

Tactic:
rw [← min?_reverse, reverse_reverse]

Result:
no goals
-- Mathlib/ModelTheory/Basic.lean
theorem toHom_injective : @Function.Injective (M ↪[L] N) (M →[L] N) (·.toHom)

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f f' : M ↪[L] N
h : (fun x => x.toHom) f = (fun x => x.toHom) f'
⊢ f = f'

Tactic:
ext

Result:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f f' : M ↪[L] N
h : (fun x => x.toHom) f = (fun x => x.toHom) f'
x✝ : M
⊢ f x✝ = f' x✝

Proof state:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f f' : M ↪[L] N
h : (fun x => x.toHom) f = (fun x => x.toHom) f'
x✝ : M
⊢ f x✝ = f' x✝

Tactic:
exact congr_fun (congr_arg (↑) h) _

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ Function.Injective fun x => x.toHom

Tactic:
intro f f' h

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f f' : M ↪[L] N
h : (fun x => x.toHom) f = (fun x => x.toHom) f'
⊢ f = f'
-- Mathlib/Order/Filter/Basic.lean
theorem biInter_mem' {β : Type v} {s : β → Set α} {is : Set β} (hf : is.Subsingleton) :
    (⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f

Proof state:
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Subsingleton
⊢ ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f

Tactic:
apply Subsingleton.induction_on hf <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem ext {g h : M ⊗ N →ₗ[R] P} (H : (mk R M N).compr₂ g = (mk R M N).compr₂ h) : g = h

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
g h : M ⊗[R] N →ₗ[R] P
H : (mk R M N).compr₂ g = (mk R M N).compr₂ h
⊢ g = h

Tactic:
rw [← lift_mk_compr₂ g, H, lift_mk_compr₂]

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
lemma sub_sq (a b : R) : (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
a b : R
⊢ (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2

Tactic:
rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem isEmpty_replicate : (replicate n a).isEmpty = decide (n = 0)

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ (replicate n a).isEmpty = decide (n = 0)

Tactic:
cases n <;> simp [replicate_succ]

Result:
no goals
-- Mathlib/Algebra/Star/Basic.lean
theorem commute_star_comm {x y : R} : Commute (star x) y ↔ Commute x (star y)

Proof state:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ Commute (star x) y ↔ Commute x (star y)

Tactic:
rw [← commute_star_star, star_star]

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem exists_Ico_subset_of_mem_nhds' [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝 a) {u : α}
    (hu : a < u) : ∃ u' ∈ Ioc a u, Ico a u' ⊆ s

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
u : α
hu : a < u
⊢ ∃ u' ∈ Ioc a u, Ico a u' ⊆ s

Tactic:
simpa only [OrderDual.exists, exists_prop, dual_Ico, dual_Ioc] using
  exists_Ioc_subset_of_mem_nhds' (show ofDual ⁻¹' s ∈ 𝓝 (toDual a) from hs) hu.dual

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem inf_arrow_factors_left {B : C} (X Y : Subobject B) : X.Factors (X ⊓ Y).arrow :=
  (factors_iff _ _).mpr ⟨ofLE (X ⊓ Y) X (inf_le_left X Y), by simp⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
B : C
X Y : Subobject B
⊢ (X ⊓ Y).ofLE X ⋯ ≫ (representative.obj X).arrow = (X ⊓ Y).arrow

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_inv_one_add_sq : (∫ x : ℝ in a..b, (↑1 + x ^ 2)⁻¹) = arctan b - arctan a

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, (1 + x ^ 2)⁻¹ = arctan b - arctan a

Tactic:
simp only [← one_div, integral_one_div_one_add_sq]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_update_ne (p : R[X]) {n : ℕ} (a : R) {i : ℕ} (h : i ≠ n) :
    (p.update n a).coeff i = p.coeff i

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
i : ℕ
h : i ≠ n
⊢ (p.update n a).coeff i = p.coeff i

Tactic:
rw [p.coeff_update_apply, if_neg h]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toNNReal_strict_mono (hb : b ≠ ∞) (h : a < b) : a.toNNReal < b.toNNReal

Proof state:
a b : ℝ≥0∞
hb : b ≠ ⊤
h : a < b
⊢ a.toNNReal < b.toNNReal

Tactic:
simpa [← ENNReal.coe_lt_coe, hb, h.ne_top]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem seminormFromBounded_ker (f_nonneg : 0 ≤ f)
    (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) :
    seminormFromBounded' f ⁻¹' {0} = f ⁻¹' {0}

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
⊢ x ∈ seminormFromBounded' f ⁻¹' {0} ↔ x ∈ f ⁻¹' {0}

Tactic:
exact seminormFromBounded_eq_zero_iff f_nonneg f_mul x

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ seminormFromBounded' f ⁻¹' {0} = f ⁻¹' {0}

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
⊢ x ∈ seminormFromBounded' f ⁻¹' {0} ↔ x ∈ f ⁻¹' {0}
-- Mathlib/Algebra/Lie/Weights/Basic.lean
theorem mem_genWeightSpaceOf (χ : R) (x : L) (m : M) :
    m ∈ genWeightSpaceOf M χ x ↔ ∃ k : ℕ, ((toEnd R L M x - χ • ↑1) ^ k) m = 0

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : R
x : L
m : M
⊢ m ∈ genWeightSpaceOf M χ x ↔ ∃ k, (((toEnd R L M) x - χ • 1) ^ k) m = 0

Tactic:
simp [genWeightSpaceOf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_modify_self (h : m.1.WF) {k : α} {f : β k → β k} :
    (m.modify k f).getKey? k = if m.contains k then some k else none

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : β k → β k
⊢ (m.modify k f).getKey? k = if m.contains k = true then some k else none

Tactic:
simp_to_model [modify] using List.getKey?_modifyKey_self

Result:
no goals
-- Mathlib/Data/Finset/Sigma.lean
theorem sigmaLift_eq_empty : sigmaLift f a b = ∅ ↔ ∀ h : a.1 = b.1, f (h ▸ a.2) b.2 = ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) = ∅ ↔
    ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

Tactic:
split_ifs with h

Result:
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ ∅ = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

Proof state:
case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ ∅ = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

Tactic:
simp [h, forall_prop_of_false h]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ sigmaLift f a b = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

Tactic:
simp_rw [sigmaLift]

Result:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) = ∅ ↔
    ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

Proof state:
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

Tactic:
simp [h, forall_prop_of_true h]

Result:
no goals