harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem pow_dichotomy (hF : ringChar F ≠ 2) {a : F} (ha : a ≠ 0) :
    a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F / 2) * a ^ (Fintype.card F / 2) = 1
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1

Tactic:
exact mul_self_eq_one_iff.mp h₁

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F - 1) = 1
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1

Tactic:
rw [← Nat.two_mul_odd_div_two (FiniteField.odd_card_of_char_ne_two hF), mul_comm, pow_mul,
  pow_two] at h₁

Result:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F / 2) * a ^ (Fintype.card F / 2) = 1
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1

Tactic:
have h₁ := FiniteField.pow_card_sub_one_eq_one a ha

Result:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F - 1) = 1
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
-- Mathlib/Probability/Kernel/Integral.lean
theorem setIntegral_const {μ : Measure β} {s : Set β} :
    ∫ x in s, f x ∂const α μ a = ∫ x in s, f x ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
μ : Measure β
s : Set β
⊢ ∫ (x : β) in s, f x ∂(const α μ) a = ∫ (x : β) in s, f x ∂μ

Tactic:
rw [const_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem pop_push (a : Array α) : (a.push x).pop = a

Proof state:
α : Type u_1
x : α
a : Array α
⊢ (a.push x).pop = a

Tactic:
simp [pop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem map_add_range' (a) (s n step) : map (a + ·) (range' s n step) = range' (a + s) n step

Proof state:
a s n step : Nat
⊢ map (fun x => a + x) (range' s n step) = range' (a + s) n step

Tactic:
ext <;> simp <;> omega

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem ext_iff' : μ₁ = μ₂ ↔ ∀ s, μ₁ s = μ₂ s :=
  ⟨by rintro rfl s; rfl, fun h ↦ Measure.ext (fun s _ ↦ h s)⟩

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
⊢ μ₁ = μ₂ → ∀ (s : Set α), μ₁ s = μ₂ s

Tactic:
rintro rfl s

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ₁ : Measure α
s : Set α
⊢ μ₁ s = μ₁ s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ₁ : Measure α
s : Set α
⊢ μ₁ s = μ₁ s

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Int/AbsoluteValue.lean
theorem AbsoluteValue.map_units_intCast [Nontrivial R] (abv : AbsoluteValue R S) (x : ℤˣ) :
    abv ((x : ℤ) : R) = 1

Proof state:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
x : ℤˣ
⊢ abv ↑↑x = 1

Tactic:
rcases Int.units_eq_one_or x with (rfl | rfl) <;> simp

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem acc_principal_iff_cluster (x : X) (C : Set X) :
    AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))

Tactic:
rw [acc_iff_cluster, inf_principal, inter_comm, diff_eq]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem eq_zero_iff_of_le {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s)
    {a b : α} (ha : a ∈ s) (hb : b ∈ s) (ab : a ≤ b) :
    variationOnFromTo f s a b = 0 ↔
      ∀ ⦃x⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
ab : a ≤ b
⊢ variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Icc a b → ∀ ⦃y : α⦄, y ∈ s ∩ Icc a b → edist (f x) (f y) = 0

Tactic:
rw [variationOnFromTo.eq_of_le _ _ ab, ENNReal.toReal_eq_zero_iff, or_iff_left (hf a b ha hb),
  eVariationOn.eq_zero_iff]

Result:
no goals
-- Mathlib/AlgebraicTopology/ModelCategory/CategoryWithCofibrations.lean
lemma mem_trivialFibrations_iff :
    trivialFibrations C f ↔ Fibration f ∧ WeakEquivalence f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
⊢ trivialFibrations C f ↔ Fibration f ∧ WeakEquivalence f

Tactic:
rw [fibration_iff, weakEquivalence_iff]

Result:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
⊢ trivialFibrations C f ↔ fibrations C f ∧ weakEquivalences C f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
⊢ trivialFibrations C f ↔ fibrations C f ∧ weakEquivalences C f

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_singleton_le_iff_mem (m : M) (p : Submodule R M) : (R ∙ m) ≤ p ↔ m ∈ p

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
p : Submodule R M
⊢ span R {m} ≤ p ↔ m ∈ p

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

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem disjoint_ker {f : F} {p : Submodule R M} :
    Disjoint p (ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0

Proof state:
R : Type u_1
R₂ : Type u_2
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₂
F : Type u_11
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R M
⊢ Disjoint p (ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0

Tactic:
simp [disjoint_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_mod_mod (m n k : Nat) : (m + n % k) % k = (m + n) % k

Proof state:
m n k : Nat
⊢ (m + n % k) % k = (m + n) % k

Tactic:
rw [Nat.add_comm, mod_add_mod, Nat.add_comm]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
/-- See also `Finset.prod_dite_eq'`. -/
@[to_additive "See also `Finset.sum_dite_eq'`."] lemma prod_dite_eq' (i : ι) (f : ∀ j, j = i → α) :
    ∏ j, (if h : j = i then f j h else 1) = f i rfl

Proof state:
ι : Type u_6
α : Type u_8
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → α
⊢ (∏ j : ι, if h : j = i then f j h else 1) = f i ⋯

Tactic:
rw [Finset.prod_dite_eq', if_pos (mem_univ _)]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_Ioi_succ {M : Type*} [CommMonoid M] {n : ℕ} (i : Fin n) (v : Fin n.succ → M) :
    ∏ j ∈ Ioi i.succ, v j = ∏ j ∈ Ioi i, v j.succ

Proof state:
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
i : Fin n
v : Fin n.succ → M
⊢ ∏ j ∈ Ioi i.succ, v j = ∏ j ∈ Ioi i, v j.succ

Tactic:
rw [Ioi_succ, Finset.prod_map, val_succEmb]

Result:
no goals
-- Mathlib/Topology/Algebra/NonUnitalAlgebra.lean
theorem le_of_mem {x : A} {s : NonUnitalSubalgebra R A} (hs : IsClosed (s : Set A)) (hx : x ∈ s) :
    elemental R x ≤ s :=
  topologicalClosure_minimal _ (adjoin_le <| by simpa using hx) hs

Proof state:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalSemiring A
inst✝ : ContinuousConstSMul R A
x : A
s : NonUnitalSubalgebra R A
hs : IsClosed ↑s
hx : x ∈ s
⊢ {x} ⊆ ↑s

Tactic:
simpa using hx

Result:
no goals
-- Mathlib/Topology/MetricSpace/MetricSeparated.lean
theorem finite_iUnion_right_iff {ι : Type*} {I : Set ι} (hI : I.Finite) {s : Set X}
    {t : ι → Set X} : AreSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, AreSeparated s (t i)

Proof state:
X : Type u_1
inst✝ : EMetricSpace X
ι : Type u_2
I : Set ι
hI : I.Finite
s : Set X
t : ι → Set X
⊢ AreSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, AreSeparated s (t i)

Tactic:
simpa only [@comm _ _ s] using finite_iUnion_left_iff hI

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem mul_X_add_natCast_comp {n : ℕ} :
    (p * (X + (n : R[X]))).comp q = p.comp q * (q + n)

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (p * (X + ↑n)).comp q = p.comp q * (q + ↑n)

Tactic:
rw [mul_add, add_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_add]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/WeakDual.lean
theorem WeakSpace.isOpen_of_isOpen (V : Set E)
    (hV : IsOpen ((toWeakSpaceCLM 𝕜 E) '' V : Set (WeakSpace 𝕜 E))) : IsOpen V

Proof state:
𝕜 : Type u_2
E : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
V : Set E
hV : IsOpen (⇑(toWeakSpaceCLM 𝕜 E) '' V)
⊢ IsOpen V

Tactic:
simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsPrefix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
    filterMap f l₁ <+: filterMap f l₂

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
h : l₁ <+: l₂
⊢ List.filterMap f l₁ <+: List.filterMap f l₂

Tactic:
obtain ⟨xs, rfl⟩ := h

Result:
case intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ xs : List α
⊢ List.filterMap f l₁ <+: List.filterMap f (l₁ ++ xs)

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ xs : List α
⊢ List.filterMap f l₁ <+: List.filterMap f l₁ ++ List.filterMap f xs

Tactic:
apply prefix_append

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ xs : List α
⊢ List.filterMap f l₁ <+: List.filterMap f (l₁ ++ xs)

Tactic:
rw [filterMap_append]

Result:
case intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ xs : List α
⊢ List.filterMap f l₁ <+: List.filterMap f l₁ ++ List.filterMap f xs
-- Mathlib/Order/Heyting/Basic.lean
theorem hnot_sdiff (a : α) : ￢a \ a = ￢a

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢a \ a = ￢a

Tactic:
rw [← top_sdiff', sdiff_sdiff, sup_idem]

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem partiallyWellOrderedOn_bUnion (s : Finset ι) {f : ι → Set α} :
    (⋃ i ∈ s, f i).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r

Proof state:
ι : Type u_1
α : Type u_2
r : α → α → Prop
s : Finset ι
f : ι → Set α
⊢ (⋃ i ∈ s, f i).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r

Tactic:
simpa only [Finset.sup_eq_iSup] using s.partiallyWellOrderedOn_sup

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem diagonalObjPullbackFstIso_inv_fst_snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
    (diagonalObjPullbackFstIso f g).inv ≫ pullback.fst _ _ ≫ pullback.snd _ _ =
      pullback.fst _ _ ≫ pullback.fst _ _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g (fst f g) ≪≫
          congrHom ⋯ ⋯ ≪≫ pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom ⋯ ⋯).inv ≫
      fst (fst f g) (fst f g) ≫ snd f g =
    fst (snd g g ≫ g) f ≫ fst g g

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).inv ≫ fst (fst f g) (fst f g) ≫ snd f g = fst (snd g g ≫ g) f ≫ fst g g

Tactic:
delta diagonalObjPullbackFstIso

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g (fst f g) ≪≫
          congrHom ⋯ ⋯ ≪≫ pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom ⋯ ⋯).inv ≫
      fst (fst f g) (fst f g) ≫ snd f g =
    fst (snd g g ≫ g) f ≫ fst g g
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem sum_pow_mul_eq_add_pow {n : ℕ} {R : Type*} [CommSemiring R] (a b : R) :
    (∑ s : Finset (Fin n), a ^ s.card * b ^ (n - s.card)) = (a + b) ^ n

Proof state:
n : ℕ
R : Type u_3
inst✝ : CommSemiring R
a b : R
⊢ ∑ s : Finset (Fin n), a ^ #s * b ^ (n - #s) = (a + b) ^ n

Tactic:
simpa using Fintype.sum_pow_mul_eq_add_pow (Fin n) a b

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem le_compl_iff_disjoint_right : a ≤ bᶜ ↔ Disjoint a b

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ≤ bᶜ ↔ Disjoint a b

Tactic:
rw [← himp_bot, le_himp_iff, disjoint_iff_inf_le]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
theorem withDensityᵥ_rnDeriv_smul (hμν : μ ≪ ν) (hf : Integrable f μ) :
    ν.withDensityᵥ (fun x ↦ (rnDeriv μ ν x).toReal • f x) = μ.withDensityᵥ f

Proof state:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
hf : Integrable f μ
⊢ (ν.withDensityᵥ fun x => (μ.rnDeriv ν x).toReal • f x) = μ.withDensityᵥ f

Tactic:
rw [withDensityᵥ_smul_eq_withDensityᵥ_withDensity' (measurable_rnDeriv μ ν).aemeasurable
  (rnDeriv_lt_top μ ν) ((integrable_rnDeriv_smul_iff hμν).mpr hf), withDensity_rnDeriv_eq μ ν hμν]

Result:
no goals
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem compLinearMap_zero [Nonempty ι] (f : M [⋀^ι]→ₗ[R] N) :
    f.compLinearMap (0 : M₂ →ₗ[R] M) = 0

Proof state:
case H
R : Type u_1
inst✝⁷ : Semiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
N : Type u_3
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
x✝ : ι → M₂
⊢ (f.compLinearMap 0) x✝ = 0 x✝

Tactic:
simp_rw [compLinearMap_apply, LinearMap.zero_apply, ← Pi.zero_def, map_zero, zero_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁷ : Semiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
N : Type u_3
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
⊢ f.compLinearMap 0 = 0

Tactic:
ext

Result:
case H
R : Type u_1
inst✝⁷ : Semiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
N : Type u_3
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
x✝ : ι → M₂
⊢ (f.compLinearMap 0) x✝ = 0 x✝
-- Mathlib/MeasureTheory/Group/LIntegral.lean
theorem lintegral_div_right_eq_self [IsMulRightInvariant μ] (f : G → ℝ≥0∞) (g : G) :
    (∫⁻ x, f (x / g) ∂μ) = ∫⁻ x, f x ∂μ

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x / g) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
simp_rw [div_eq_mul_inv, lintegral_mul_right_eq_self f g⁻¹]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Division.lean
theorem coeff_modMonomial_of_not_le {s' s : σ →₀ ℕ} (x : MvPolynomial σ R) (h : ¬s ≤ s') :
    coeff s' (x %ᵐᵒⁿᵒᵐⁱᵃˡ s) = coeff s' x :=
  x.modOf_apply_of_not_exists_add s s'
    (by
      rintro ⟨d, rfl⟩
      exact h le_self_add)

Proof state:
case intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
x : MvPolynomial σ R
d : σ →₀ ℕ
h : ¬s ≤ s + d
⊢ False

Tactic:
exact h le_self_add

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s' s : σ →₀ ℕ
x : MvPolynomial σ R
h : ¬s ≤ s'
⊢ ¬∃ d, s' = s + d

Tactic:
rintro ⟨d, rfl⟩

Result:
case intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
x : MvPolynomial σ R
d : σ →₀ ℕ
h : ¬s ≤ s + d
⊢ False
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toMeasure_apply_inter_support (hs : MeasurableSet s) (hp : MeasurableSet p.support) :
    p.toMeasure (s ∩ p.support) = p.toMeasure s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
p : PMF α
s : Set α
hs : MeasurableSet s
hp : MeasurableSet p.support
⊢ p.toMeasure (s ∩ p.support) = p.toMeasure s

Tactic:
simp [p.toMeasure_apply_eq_toOuterMeasure_apply s hs,
  p.toMeasure_apply_eq_toOuterMeasure_apply _ (hs.inter hp)]

Result:
no goals
-- Mathlib/SetTheory/Game/Impartial.lean
theorem impartial_def {G : PGame} :
    G.Impartial ↔ G ≈ -G ∧ (∀ i, Impartial (G.moveLeft i)) ∧ ∀ j, Impartial (G.moveRight j)

Proof state:
G : PGame
⊢ SetTheory.PGame.ImpartialAux G ↔
    G ≈ -G ∧
      (∀ (i : G.LeftMoves), SetTheory.PGame.ImpartialAux (G.moveLeft i)) ∧
        ∀ (j : G.RightMoves), SetTheory.PGame.ImpartialAux (G.moveRight j)

Tactic:
rw [ImpartialAux]

Result:
no goals

Proof state:
G : PGame
⊢ G.Impartial ↔
    G ≈ -G ∧ (∀ (i : G.LeftMoves), (G.moveLeft i).Impartial) ∧ ∀ (j : G.RightMoves), (G.moveRight j).Impartial

Tactic:
simp_rw [impartial_iff_aux]

Result:
G : PGame
⊢ SetTheory.PGame.ImpartialAux G ↔
    G ≈ -G ∧
      (∀ (i : G.LeftMoves), SetTheory.PGame.ImpartialAux (G.moveLeft i)) ∧
        ∀ (j : G.RightMoves), SetTheory.PGame.ImpartialAux (G.moveRight j)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertManyIfNewUnit_list_singleton {k : α} :
    insertManyIfNewUnit m [k] = m.insertIfNew k ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => Unit
k : α
⊢ (insertManyIfNewUnit m [k]).val = m.insertIfNew k ()

Tactic:
simp [insertManyIfNewUnit, Id.run]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_finsupp' (ι : Type v) : Module.rank R (ι →₀ M) = #ι * Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
ι : Type v
⊢ Module.rank R (ι →₀ M) = #ι * Module.rank R M

Tactic:
simp [rank_finsupp]

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
lemma toAddCircle_intCast (j : ℤ) :
    toAddCircle (j : ZMod N) = ↑(j / N : ℝ)

Proof state:
N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ toAddCircle ↑j = ↑(↑j / ↑N)

Tactic:
simp [toAddCircle]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem blsub_lt_ord {o : Ordinal} {f : ∀ a < o, Ordinal} {c : Ordinal} (ho : o.card < c.cof)
    (hf : ∀ i hi, f i hi < c) : blsub.{u, u} o f < c :=
  blsub_lt_ord_lift (by rwa [o.card.lift_id]) hf

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
⊢ Cardinal.lift.{u, u} o.card < c.cof

Tactic:
rwa [o.card.lift_id]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem map_injective_of_ker_le {H K : Subgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K)
    (hf : map f H = map f K) : H = K

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : map f H = map f K
⊢ H = K

Tactic:
apply_fun comap f at hf

Result:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : comap f (map f H) = comap f (map f K)
⊢ H = K

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : comap f (map f H) = comap f (map f K)
⊢ H = K

Tactic:
rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem pdf_of_not_aemeasurable {_ : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E}
    {X : Ω → E} (hX : ¬AEMeasurable X ℙ) : pdf X ℙ μ =ᵐ[μ] 0

Proof state:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : ¬AEMeasurable X ℙ
⊢ rnDeriv 0 μ =ᶠ[ae μ] 0

Tactic:
exact rnDeriv_zero μ

Result:
no goals

Proof state:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : ¬AEMeasurable X ℙ
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
rw [pdf_def, map_of_not_aemeasurable hX]

Result:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : ¬AEMeasurable X ℙ
⊢ rnDeriv 0 μ =ᶠ[ae μ] 0
-- Mathlib/Topology/Inseparable.lean
theorem not_inseparable_iff_exists_open :
    ¬(x ~ᵢ y) ↔ ∃ s : Set X, IsOpen s ∧ Xor' (x ∈ s) (y ∈ s)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ¬(x ~ᵢ y) ↔ ∃ s, IsOpen s ∧ Xor' (x ∈ s) (y ∈ s)

Tactic:
simp [inseparable_iff_forall_isOpen, ← xor_iff_not_iff]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem lowerClosure_singleton (a : α) : lowerClosure ({a} : Set α) = LowerSet.Iic a

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
a x✝ : α
⊢ x✝ ∈ ↑(lowerClosure {a}) ↔ x✝ ∈ ↑(LowerSet.Iic a)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ lowerClosure {a} = LowerSet.Iic a

Tactic:
ext

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
a x✝ : α
⊢ x✝ ∈ ↑(lowerClosure {a}) ↔ x✝ ∈ ↑(LowerSet.Iic a)
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem evalWhiskerRight_id
    {η : f ⟶ g} {η₁ : f ⟶ g ≫ 𝟙 b} {η₂ : f ≫ 𝟙 b ⟶ g ≫ 𝟙 b}
    (e_η₁ : η ≫ (ρ_ _).inv = η₁) (e_η₂ : (ρ_ _).hom ≫ η₁ = η₂) :
    η ▷ 𝟙 b = η₂

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
η₁ : f ⟶ g ≫ 𝟙 b
η₂ : f ≫ 𝟙 b ⟶ g ≫ 𝟙 b
e_η₁ : η ≫ (ρ_ g).inv = η₁
e_η₂ : (ρ_ f).hom ≫ η₁ = η₂
⊢ η ▷ 𝟙 b = η₂

Tactic:
simp [e_η₁, e_η₂]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem card_bind : card (s.bind f) = (s.map (card ∘ f)).sum

Proof state:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
⊢ (s.bind f).card = (map (card ∘ f) s).sum

Tactic:
simp [bind]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
lemma Ico_map_sectR : (Ico a b).map (.sectR c _) = Ico (c, a) (c, b)

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

Tactic:
aesop (add safe forward [le_antisymm, le_of_lt])

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean
theorem uniqueMDiffWithinAt_iff_uniqueDiffWithinAt :
    UniqueMDiffWithinAt 𝓘(𝕜, E) s x ↔ UniqueDiffWithinAt 𝕜 s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
⊢ UniqueMDiffWithinAt 𝓘(𝕜, E) s x ↔ UniqueDiffWithinAt 𝕜 s x

Tactic:
simp only [UniqueMDiffWithinAt, mfld_simps]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem toContinuousLinearMap_norm [NormOneClass A] (φ : A →ₐ[𝕜] 𝕜) :
    ‖φ.toContinuousLinearMap‖ = 1 :=
  ContinuousLinearMap.opNorm_eq_of_bounds zero_le_one
    (fun a => (one_mul ‖a‖).symm ▸ spectrum.norm_le_norm_of_mem (apply_mem_spectrum φ _))
    fun _ _ h => by simpa only [coe_toContinuousLinearMap, map_one, norm_one, mul_one] using h 1

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : NormOneClass A
φ : A →ₐ[𝕜] 𝕜
x✝¹ : ℝ
x✝ : x✝¹ ≥ 0
h : ∀ (x : A), ‖φ.toContinuousLinearMap x‖ ≤ x✝¹ * ‖x‖
⊢ 1 ≤ x✝¹

Tactic:
simpa only [coe_toContinuousLinearMap, map_one, norm_one, mul_one] using h 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem enumFrom_eq_nil {n : Nat} {l : List α} : List.enumFrom n l = [] ↔ l = []

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ enumFrom n l = [] ↔ l = []

Tactic:
cases l <;> simp

Result:
no goals