harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem ndunion_le {s t u : Multiset α} : ndunion s t ≤ u ↔ s ⊆ u ∧ t ≤ u :=
  Multiset.induction_on s (by simp [zero_ndunion])
    (fun _ _ h =>
      by simp only [cons_ndunion, mem_ndunion, ndinsert_le, and_comm, cons_subset, and_left_comm, h,
        and_assoc])

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
x✝¹ : α
x✝ : Multiset α
h : x✝.ndunion t ≤ u ↔ x✝ ⊆ u ∧ t ≤ u
⊢ (x✝¹ ::ₘ x✝).ndunion t ≤ u ↔ x✝¹ ::ₘ x✝ ⊆ u ∧ t ≤ u

Tactic:
simp only [cons_ndunion, mem_ndunion, ndinsert_le, and_comm, cons_subset, and_left_comm, h,
and_assoc]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ ndunion 0 t ≤ u ↔ 0 ⊆ u ∧ t ≤ u

Tactic:
simp [zero_ndunion]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive natCast_sub_natCast_zsmul]
lemma zpow_natCast_sub_natCast (a : G) (m n : ℕ) : a ^ (m - n : ℤ) = a ^ m / a ^ n

Proof state:
G : Type u_3
inst✝ : Group G
a : G
m n : ℕ
⊢ a ^ (↑m - ↑n) = a ^ m / a ^ n

Tactic:
simpa [div_eq_mul_inv] using zpow_sub a m n

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma isGreatest_nnnorm_spectrum [Nontrivial A] (a : A) (ha : p a

Proof state:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
a : A
ha : autoParam (p a) _auto✝
⊢ IsGreatest ((fun x => ‖x‖₊) '' σ 𝕜 a) ‖a‖₊

Tactic:
simpa only [cfc_id 𝕜 a] using IsGreatest.nnnorm_cfc (id : 𝕜 → 𝕜) a

Result:
no goals
-- Mathlib/Order/Filter/CountablyGenerated.lean
theorem HasAntitoneBasis.mem_iff [Preorder ι] {l : Filter α} {s : ι → Set α}
    (hs : l.HasAntitoneBasis s) {t : Set α} : t ∈ l ↔ ∃ i, s i ⊆ t :=
  hs.toHasBasis.mem_iff.trans <| by simp only [exists_prop, true_and]

Proof state:
α : Type u_1
ι : Type u_4
inst✝ : Preorder ι
l : Filter α
s : ι → Set α
hs : l.HasAntitoneBasis s
t : Set α
⊢ (∃ i, True ∧ s i ⊆ t) ↔ ∃ i, s i ⊆ t

Tactic:
simp only [exists_prop, true_and]

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Basic.lean
@[simp]
lemma iInf_obj {ι : Type*} (S : ι → Subpresheaf F) (U : Cᵒᵖ) :
    (⨅ i, S i).obj U = ⋂ i, (S i).obj U

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
ι : Type u_1
S : ι → Subpresheaf F
U : Cᵒᵖ
⊢ (⨅ i, S i).obj U = ⋂ i, (S i).obj U

Tactic:
simp [iInf, sInf_obj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_alter [LawfulBEq α] (h : m.1.WF) {k k' : α} {f : Option (β k) → Option (β k)} :
    (m.alter k f).contains k' = if k == k' then (f (m.get? k)).isSome else m.contains k'

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k k' : α
f : Option (β k) → Option (β k)
⊢ (m.alter k f).contains k' = if (k == k') = true then (f (m.get? k)).isSome else m.contains k'

Tactic:
simp_to_model [alter] using List.containsKey_alterKey

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_left_identity {f : α → γ → γ} {a : α} (h : ∀ b, f a b = b) (t : Finset γ) :
    image₂ f {a} t = t :=
  coe_injective <| by rw [coe_image₂, coe_singleton, Set.image2_left_identity h]

Proof state:
α : Type u_1
γ : Type u_5
inst✝ : DecidableEq γ
f : α → γ → γ
a : α
h : ∀ (b : γ), f a b = b
t : Finset γ
⊢ ↑(image₂ f {a} t) = ↑t

Tactic:
rw [coe_image₂, coe_singleton, Set.image2_left_identity h]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem equalizerSubobject_arrow :
    (equalizerSubobjectIso f g).hom ≫ equalizer.ι f g = (equalizerSubobject f g).arrow

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
⊢ (equalizerSubobjectIso f g).hom ≫ equalizer.ι f g = (equalizerSubobject f g).arrow

Tactic:
simp [equalizerSubobjectIso]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sub_add_bmod_cancel {x y : BitVec w} :
    ((((2 ^ w : Nat) - y.toNat) : Int) + x.toNat).bmod (2 ^ w) =
      ((x.toNat : Int) - y.toNat).bmod (2 ^ w)

Proof state:
w : Nat
x y : BitVec w
⊢ (↑(2 ^ w) - ↑y.toNat + ↑x.toNat).bmod (2 ^ w) = (↑x.toNat - ↑y.toNat).bmod (2 ^ w)

Tactic:
rw [Int.sub_eq_add_neg, Int.add_assoc, Int.add_comm, Int.bmod_add_cancel, Int.add_comm,
  Int.sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mem_zipIdx_iff_le_and_getElem?_sub {x : α × Nat} {l : Vector α n} {k : Nat} :
    x ∈ zipIdx l k ↔ k ≤ x.2 ∧ l[x.2 - k]? = some x.1

Proof state:
α : Type u_1
n : Nat
x : α × Nat
l : Vector α n
k : Nat
⊢ x ∈ l.zipIdx k ↔ k ≤ x.snd ∧ l[x.snd - k]? = some x.fst

Tactic:
cases x

Result:
case mk
α : Type u_1
n : Nat
l : Vector α n
k : Nat
fst✝ : α
snd✝ : Nat
⊢ (fst✝, snd✝) ∈ l.zipIdx k ↔ k ≤ (fst✝, snd✝).snd ∧ l[(fst✝, snd✝).snd - k]? = some (fst✝, snd✝).fst

Proof state:
case mk
α : Type u_1
n : Nat
l : Vector α n
k : Nat
fst✝ : α
snd✝ : Nat
⊢ (fst✝, snd✝) ∈ l.zipIdx k ↔ k ≤ (fst✝, snd✝).snd ∧ l[(fst✝, snd✝).snd - k]? = some (fst✝, snd✝).fst

Tactic:
simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
    m.1.size ≤ (m.insert k v).1.size

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
v : β k
⊢ m.val.size ≤ (m.insert k v).val.size

Tactic:
simp_to_model [insert] using List.length_le_length_insertEntry

Result:
no goals
-- Mathlib/Topology/Constructions.lean
lemma Topology.isOpenEmbedding_sigmaMap {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)} (h : Injective f₁) :
    IsOpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ i, IsOpenEmbedding (f₂ i)

Proof state:
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h : Injective f₁
⊢ IsOpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsOpenEmbedding (f₂ i)

Tactic:
simp only [isOpenEmbedding_iff_isEmbedding_isOpenMap, isOpenMap_sigma_map, isEmbedding_sigmaMap h,
  forall_and]

Result:
no goals
-- Mathlib/Computability/DFA.lean
theorem evalFrom_append_singleton (s : σ) (x : List α) (a : α) :
    M.evalFrom s (x ++ [a]) = M.step (M.evalFrom s x) a

Proof state:
α : Type u
σ : Type v
M : DFA α σ
s : σ
x : List α
a : α
⊢ M.evalFrom s (x ++ [a]) = M.step (M.evalFrom s x) a

Tactic:
simp only [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem sup_span : p ⊔ span R s = span R (p ∪ s)

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
⊢ p ⊔ span R s = span R (↑p ∪ s)

Tactic:
rw [Submodule.span_union, p.span_eq]

Result:
no goals
-- Mathlib/Algebra/Quandle.lean
/--
The associativity of a unital shelf comes for free.
-/
lemma assoc (x y z : S) : (x ◃ y) ◃ z = x ◃ y ◃ z

Proof state:
S : Type u_1
inst✝ : UnitalShelf S
x y z : S
⊢ (x ◃ y) ◃ z = x ◃ y ◃ z

Tactic:
rw [self_distrib, self_distrib, act_act_self_eq, act_self_act_eq]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@[to_additive (attr := simp)]
lemma encard_smul_set (a : G) (s : Set α) : (a • s).encard = s.encard

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
⊢ (a • s).encard = s.encard

Tactic:
simp [ENat.card, ← toENat_cardinalMk]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
@[simp] lemma graphOn_inj {g : α → β} : s.graphOn f = s.graphOn g ↔ s.EqOn f g

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f g : α → β
⊢ graphOn f s = graphOn g s ↔ EqOn f g s

Tactic:
simp [Set.ext_iff, funext_iff, forall_swap, EqOn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_ofList [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} {k : α} :
    k ∈ ofList l ↔ (l.map Sigma.fst).contains k

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k : α
⊢ k ∈ ofList l ↔ (List.map Sigma.fst l).contains k = true

Tactic:
simp [mem_iff_contains]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
lemma natCast_add_one_le_iff {n : ℕ} {c : Cardinal} : n + 1 ≤ c ↔ n < c

Proof state:
n : ℕ
c : Cardinal.{u_1}
⊢ ↑n + 1 ≤ c ↔ ↑n < c

Tactic:
rw [← Order.succ_le_iff, Cardinal.succ_natCast]

Result:
no goals
-- Mathlib/Data/Finset/Dedup.lean
theorem toFinset_eq (n : Nodup l) : @Finset.mk α l n = l.toFinset :=
  Multiset.toFinset_eq <| by rwa [Multiset.coe_nodup]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
n : l.Nodup
⊢ (↑l).Nodup

Tactic:
rwa [Multiset.coe_nodup]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem Basis.sum_equivFun [Fintype ι] (b : Basis ι R M) (u : M) :
    ∑ i, b.equivFun u i • b i = u

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
u : M
⊢ ∑ i : ι, b.equivFun u i • b i = u

Tactic:
rw [← b.equivFun_symm_apply, b.equivFun.symm_apply_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_neg_left (x y : M) : polar Q (-x) y = -polar Q x y

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x y : M
⊢ polar (⇑Q) (-x) y = -polar (⇑Q) x y

Tactic:
rw [← neg_one_smul R x, polar_smul_left, neg_one_smul]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem torusMap_eq_center_iff {c : ℂⁿ} {R : ℝⁿ} {θ : ℝⁿ} : torusMap c R θ = c ↔ R = 0

Proof state:
n : ℕ
c : Fin n → ℂ
R θ : Fin n → ℝ
⊢ torusMap c R θ = c ↔ R = 0

Tactic:
simp [funext_iff, torusMap, exp_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem allOnes_or {x : BitVec w} : allOnes w ||| x = allOnes w

Proof state:
w : Nat
x : BitVec w
⊢ allOnes w ||| x = allOnes w

Tactic:
ext i h

Result:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (allOnes w ||| x).getLsbD i = (allOnes w).getLsbD i

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (allOnes w ||| x).getLsbD i = (allOnes w).getLsbD i

Tactic:
simp [h]

Result:
no goals
-- Mathlib/RingTheory/Lasker.lean
lemma IsLasker.minimal [DecidableEq (Ideal R)] (h : IsLasker R) (I : Ideal R) :
    ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧
      ((t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical)) ∧
      (∀ ⦃J⦄, J ∈ t → ¬ (t.erase J).inf id ≤ J)

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
h : IsLasker R
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
⊢ ∃ t,
    t.inf id = I ∧
      (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧
        (↑t).Pairwise ((fun x1 x2 => x1 ≠ x2) on radical) ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
exact exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition hs hs'

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
h : IsLasker R
I : Ideal R
⊢ ∃ t,
    t.inf id = I ∧
      (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧
        (↑t).Pairwise ((fun x1 x2 => x1 ≠ x2) on radical) ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
obtain ⟨s, hs, hs'⟩ := h I

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
h : IsLasker R
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
⊢ ∃ t,
    t.inf id = I ∧
      (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧
        (↑t).Pairwise ((fun x1 x2 => x1 ≠ x2) on radical) ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem coeff_X (i : σ) : coeff (Finsupp.single i 1) (X i : MvPolynomial σ R) = 1

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
⊢ coeff (Finsupp.single i 1) (X i) = 1

Tactic:
rw [coeff_X', if_pos rfl]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
⊢ coeff (Finsupp.single i 1) (X i) = 1

Tactic:
classical rw [coeff_X', if_pos rfl]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_sign_eq_zero_iff_collinear {p₁ p₂ p₃ : P} :
    (∡ p₁ p₂ p₃).sign = 0 ↔ Collinear ℝ ({p₁, p₂, p₃} : Set P)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ (∡ p₁ p₂ p₃).sign = 0 ↔ Collinear ℝ {p₁, p₂, p₃}

Tactic:
rw [Real.Angle.sign_eq_zero_iff, oangle_eq_zero_or_eq_pi_iff_collinear]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)}
    {k k' fallback : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Sigma.fst) :
    (ofList l).getKeyD k' fallback = k

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k k' fallback : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Sigma.fst l
⊢ (ofList l).getKeyD k' fallback = k

Tactic:
simp_to_raw using Raw₀.getKeyD_insertMany_empty_list_of_mem

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma image_compl [DecidableEq α] : s.image compl = sᶜˢ

Proof state:
α : Type u_2
inst✝¹ : BooleanAlgebra α
s : Finset α
inst✝ : DecidableEq α
⊢ image compl s = sᶜˢ

Tactic:
simp [compls, map_eq_image]

Result:
no goals
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem zipWith_neLocus_eq_left [∀ a, DecidableEq (N a)] [∀ a, DecidableEq (P a)]
    {F : ∀ a, M a → N a → P a} (F0 : ∀ a, F a 0 0 = 0) (f : Π₀ a, M a) (g₁ g₂ : Π₀ a, N a)
    (hF : ∀ a f, Function.Injective fun g ↦ F a f g) :
    (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) = g₁.neLocus g₂

Proof state:
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f : Π₀ (a : α), M a
g₁ g₂ : Π₀ (a : α), N a
hF : ∀ (a : α) (f : M a), Function.Injective fun g => F a f g
⊢ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) = g₁.neLocus g₂

Tactic:
ext a

Result:
case h
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f : Π₀ (a : α), M a
g₁ g₂ : Π₀ (a : α), N a
hF : ∀ (a : α) (f : M a), Function.Injective fun g => F a f g
a : α
⊢ a ∈ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) ↔ a ∈ g₁.neLocus g₂

Proof state:
case h
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f : Π₀ (a : α), M a
g₁ g₂ : Π₀ (a : α), N a
hF : ∀ (a : α) (f : M a), Function.Injective fun g => F a f g
a : α
⊢ a ∈ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) ↔ a ∈ g₁.neLocus g₂

Tactic:
simpa only [mem_neLocus] using (hF a _).ne_iff

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem le_one_iff {a : Ordinal} : a ≤ 1 ↔ a = 0 ∨ a = 1

Proof state:
a : Ordinal.{u_1}
⊢ a ≤ 1 ↔ a = 0 ∨ a = 1

Tactic:
simpa using @le_succ_bot_iff _ _ _ a _

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem map_extChartAt_symm_nhdsWithin_range' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    map (extChartAt I x).symm (𝓝[range I] extChartAt I x y) = 𝓝 y :=
  map_extend_symm_nhdsWithin_range _ <| by rwa [← extChartAt_source I]

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ y ∈ (chartAt H x).source

Tactic:
rwa [← extChartAt_source I]

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
@[simp] lemma subtype_eq_univ {p : α → Prop} [DecidablePred p] [Fintype {a // p a}] :
    s.subtype p = univ ↔ ∀ ⦃a⦄, p a → a ∈ s

Proof state:
α : Type u_1
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Finset.subtype p s = univ ↔ ∀ ⦃a : α⦄, p a → a ∈ s

Tactic:
simp [Finset.ext_iff]

Result:
no goals
-- Mathlib/Data/Int/Log.lean
theorem neg_clog_inv_eq_log (b : ℕ) (r : R) : -clog b r⁻¹ = log b r

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ -clog b r⁻¹ = log b r

Tactic:
rw [clog_inv, neg_neg]

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

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

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
    m.contains a = false → get? m a = none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
⊢ m.contains a = false → get? m a = none

Tactic:
simp_to_model using List.getValue?_eq_none.2

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
theorem continuousAt_equivIco (hx : x ≠ a) : ContinuousAt (equivIco p a) x

Proof state:
case H
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ Filter.map (⇑(equivIco p a) ∘ QuotientAddGroup.mk) (𝓝 z✝) ≤ 𝓝 ((equivIco p a) ↑z✝)

Tactic:
exact (continuousAt_toIcoMod hp.out a hx).codRestrict _

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
hx : x ≠ ↑a
⊢ ContinuousAt (⇑(equivIco p a)) x

Tactic:
induction x using QuotientAddGroup.induction_on

Result:
case H
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ ContinuousAt ⇑(equivIco p a) ↑z✝

Proof state:
case H
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ ContinuousAt ⇑(equivIco p a) ↑z✝

Tactic:
rw [ContinuousAt, Filter.Tendsto, QuotientAddGroup.nhds_eq, Filter.map_map]

Result:
case H
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ Filter.map (⇑(equivIco p a) ∘ QuotientAddGroup.mk) (𝓝 z✝) ≤ 𝓝 ((equivIco p a) ↑z✝)
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem apply_lineMap (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) (c : k) :
    f (lineMap p₀ p₁ c) = lineMap (f p₀) (f p₁) c

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
p₀ p₁ : P1
c : k
⊢ f ((lineMap p₀ p₁) c) = (lineMap (f p₀) (f p₁)) c

Tactic:
simp [lineMap_apply]

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem star_add_self (x : R) : IsSelfAdjoint (star x + x)

Proof state:
R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : StarAddMonoid R
x : R
⊢ IsSelfAdjoint (star x + x)

Tactic:
simp only [isSelfAdjoint_iff, add_comm, star_add, star_star]

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_X_sub_C (x : F) : (X - C x).natSepDegree = 1

Proof state:
F : Type u
inst✝ : Field F
x : F
⊢ (X - C x).natSepDegree = 1

Tactic:
simp only [natSepDegree, aroots_X_sub_C, Multiset.toFinset_singleton, Finset.card_singleton]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
theorem _root_.NumberField.mixedEmbedding.covolume_integerLattice :
    ZLattice.covolume (mixedEmbedding.integerLattice K) =
      (2 ⁻¹) ^ nrComplexPlaces K * √|discr K|

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ZLattice.covolume (mixedEmbedding.integerLattice K) volume = 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|

Tactic:
rw [ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_integerLattice K),
  volume_fundamentalDomain_latticeBasis, ENNReal.toReal_mul, ENNReal.toReal_pow,
  ENNReal.toReal_inv, toReal_ofNat, ENNReal.coe_toReal, Real.coe_sqrt, coe_nnnorm,
  Int.norm_eq_abs]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
/-- Binary strict **rearrangement inequality**. -/
lemma smul_add_smul_lt_smul_add_smul' (ha : a₂ < a₁) (hb : b₂ < b₁) :
    a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ < a₁
hb : b₂ < b₁
⊢ a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂

Tactic:
simp_rw [add_comm (a₁ • _)]

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ < a₁
hb : b₂ < b₁
⊢ a₂ • b₁ + a₁ • b₂ < a₂ • b₂ + a₁ • b₁

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ < a₁
hb : b₂ < b₁
⊢ a₂ • b₁ + a₁ • b₂ < a₂ • b₂ + a₁ • b₁

Tactic:
exact smul_add_smul_lt_smul_add_smul ha hb

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
@[simp] lemma sdiff_eq_sdiff_iff : a \ b = b \ a ↔ a = b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ b = b \ a ↔ a = b

Tactic:
simp [le_antisymm_iff]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_congr' {M : Type*} [CommMonoid M] {a b : ℕ} (f : Fin b → M) (h : a = b) :
    (∏ i : Fin a, f (i.cast h)) = ∏ i : Fin b, f i

Proof state:
M : Type u_3
inst✝ : CommMonoid M
a : ℕ
f : Fin a → M
⊢ ∏ i : Fin a, f (Fin.cast ⋯ i) = ∏ i : Fin a, f i

Tactic:
congr

Result:
no goals

Proof state:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin b → M
h : a = b
⊢ ∏ i : Fin a, f (Fin.cast h i) = ∏ i : Fin b, f i

Tactic:
subst h

Result:
M : Type u_3
inst✝ : CommMonoid M
a : ℕ
f : Fin a → M
⊢ ∏ i : Fin a, f (Fin.cast ⋯ i) = ∏ i : Fin a, f i
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem associator_conjugation {X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') :
    (f ⊗ g) ⊗ h = (α_ X Y Z).hom ≫ (f ⊗ g ⊗ h) ≫ (α_ X' Y' Z').inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ (f ⊗ g) ⊗ h = (α_ X Y Z).hom ≫ (f ⊗ g ⊗ h) ≫ (α_ X' Y' Z').inv

Tactic:
rw [associator_inv_naturality, hom_inv_id_assoc]

Result:
no goals