harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem Function.false_comp {f : α → β} : ((fun _ => false) ∘ f) = fun _ => false

Proof state:
α : Sort u_1
β : Sort u_2
f : α → β
⊢ (fun x => false) ∘ f = fun x => false

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_Icc {a b : ℝ} : volume (Icc a b) = ofReal (b - a)

Proof state:
a b : ℝ
⊢ volume (Icc a b) = ofReal (b - a)

Tactic:
simp [volume_val]

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive (attr := simp) negPart_pos] lemma one_lt_ltOnePart (ha : a < 1) : 1 < a⁻ᵐ

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
ha : a < 1
⊢ 1 < a⁻ᵐ

Tactic:
rwa [leOnePart_eq_inv.2 ha.le, one_lt_inv']

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
theorem ContMDiff.comp {g : M' → M''} (hg : ContMDiff I' I'' n g) (hf : ContMDiff I I' n f) :
    ContMDiff I I'' n (g ∘ f)

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
E'' : Type u_8
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝³ : TopologicalSpace M''
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
n : WithTop ℕ∞
g : M' → M''
hg : ContMDiff I' I'' n g
hf : ContMDiff I I' n f
⊢ ContMDiff I I'' n (g ∘ f)

Tactic:
rw [← contMDiffOn_univ] at hf hg ⊢

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
E'' : Type u_8
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝³ : TopologicalSpace M''
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
n : WithTop ℕ∞
g : M' → M''
hg : ContMDiffOn I' I'' n g univ
hf : ContMDiffOn I I' n f univ
⊢ ContMDiffOn I I'' n (g ∘ f) univ

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
E'' : Type u_8
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝³ : TopologicalSpace M''
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
n : WithTop ℕ∞
g : M' → M''
hg : ContMDiffOn I' I'' n g univ
hf : ContMDiffOn I I' n f univ
⊢ ContMDiffOn I I'' n (g ∘ f) univ

Tactic:
exact hg.comp hf subset_preimage_univ

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem compl_sdiff_compl : xᶜ \ yᶜ = y \ x

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ xᶜ \ yᶜ = y \ x

Tactic:
rw [sdiff_compl, sdiff_eq, inf_comm]

Result:
no goals
-- Mathlib/Control/Traversable/Equiv.lean
theorem id_map {α : Type u} (x : t' α) : Equiv.map eqv id x = x

Proof state:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
α : Type u
x : t' α
⊢ Equiv.map eqv id x = x

Tactic:
simp [Equiv.map, id_map]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem le_opNorm_mul_pow_of_le {n : ℕ} {Ei : Fin n → Type*} [∀ i, SeminormedAddCommGroup (Ei i)]
    [∀ i, NormedSpace 𝕜 (Ei i)] (f : ContinuousMultilinearMap 𝕜 Ei G) {m : ∀ i, Ei i} {b : ℝ}
    (hm : ‖m‖ ≤ b) : ‖f m‖ ≤ ‖f‖ * b ^ n

Proof state:
𝕜 : Type u
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
n : ℕ
Ei : Fin n → Type u_1
inst✝¹ : (i : Fin n) → SeminormedAddCommGroup (Ei i)
inst✝ : (i : Fin n) → NormedSpace 𝕜 (Ei i)
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n) → Ei i
b : ℝ
hm : ‖m‖ ≤ b
⊢ ‖f m‖ ≤ ‖f‖ * b ^ n

Tactic:
simpa only [Fintype.card_fin] using f.le_opNorm_mul_pow_card_of_le hm

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma supClosed_empty : SupClosed (∅ : Set α)

Proof state:
α : Type u_3
inst✝ : SemilatticeSup α
⊢ SupClosed ∅

Tactic:
simp [SupClosed]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem mul_le_mul_of_mul_div_le (h : a * (b / c) ≤ d) (hc : 0 < c) : b * a ≤ d * c

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b c d : α
h : a * b / c ≤ d
hc : 0 < c
⊢ b * a ≤ d * c

Tactic:
rwa [mul_comm b, ← div_le_iff₀ hc]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b c d : α
h : a * (b / c) ≤ d
hc : 0 < c
⊢ b * a ≤ d * c

Tactic:
rw [← mul_div_assoc] at h

Result:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b c d : α
h : a * b / c ≤ d
hc : 0 < c
⊢ b * a ≤ d * c
-- Mathlib/Topology/Homeomorph.lean
theorem map_nhds_eq (h : X ≃ₜ Y) (x : X) : map h (𝓝 x) = 𝓝 (h x) :=
  h.isEmbedding.map_nhds_of_mem _ (by simp)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ range ⇑h ∈ 𝓝 (h x)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
lemma IsUpperSet.erase (hs : IsUpperSet s) (has : ∀ b ∈ s, b ≤ a → b = a) : IsUpperSet (s \ {a}) :=
  hs.sdiff <| by simpa using has

Proof state:
α : Type u_1
inst✝ : LE α
s : Set α
a : α
hs : IsUpperSet s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ ∀ b ∈ s, ∀ c ∈ {a}, b ≤ c → b ∈ {a}

Tactic:
simpa using has

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt (hf : FiniteMultiplicity a b) {m : ℕ}
    (hm : multiplicity a b < m) : ¬a ^ m ∣ b

Proof state:
case hm
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ ↑(multiplicity a b) < ↑m

Tactic:
norm_cast

Result:
no goals

Proof state:
case hm
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ emultiplicity a b < ↑m

Tactic:
rw [hf.emultiplicity_eq_multiplicity]

Result:
case hm
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ ↑(multiplicity a b) < ↑m

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ ¬a ^ m ∣ b

Tactic:
apply not_pow_dvd_of_emultiplicity_lt

Result:
case hm
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ emultiplicity a b < ↑m
-- Mathlib/Data/Set/Pairwise/Lattice.lean
theorem pairwise_sUnion {r : α → α → Prop} {s : Set (Set α)} (h : DirectedOn (· ⊆ ·) s) :
    (⋃₀ s).Pairwise r ↔ ∀ a ∈ s, Set.Pairwise a r

Proof state:
α : Type u_1
r : α → α → Prop
s : Set (Set α)
h : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
⊢ (⋃₀ s).Pairwise r ↔ ∀ a ∈ s, a.Pairwise r

Tactic:
rw [sUnion_eq_iUnion, pairwise_iUnion h.directed_val, SetCoe.forall]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem sum_taylor_eq {R} [CommRing R] (f : R[X]) (r : R) :
    ((taylor r f).sum fun i a => C a * (X - C r) ^ i) = f

Proof state:
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
⊢ (((taylor r) f).sum fun i a => C a * (X - C r) ^ i) = f

Tactic:
rw [← comp_eq_sum_left, sub_eq_add_neg, ← C_neg, ← taylor_apply, taylor_taylor, neg_add_cancel,
  taylor_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : k == a) :
    getEntry? a (⟨k, v⟩ :: l) = some ⟨k, v⟩

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : (k == a) = true
⊢ getEntry? a (⟨k, v⟩ :: l) = some ⟨k, v⟩

Tactic:
simp [getEntry?, h]

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem mk_add {f g : CauSeq ℚ abs} : mk (f + g) = mk f + mk g

Proof state:
f g : CauSeq ℚ abs
⊢ mk (f + g) = mk f + mk g

Tactic:
simp [mk, ← ofCauchy_add]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_monomial (m n : ℕ) (a : R) : coeff R m (monomial R n a) = if m = n then a else 0 :=
  calc
    coeff R m (monomial R n a) = _ := MvPowerSeries.coeff_monomial _ _ _
    _ = if m = n then a else 0

Proof state:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
a : R
⊢ (if single () m = single () n then a else 0) = if m = n then a else 0

Tactic:
simp only [Finsupp.unique_single_eq_iff]

Result:
no goals
-- Mathlib/Order/Circular.lean
theorem sbtw_iff_not_btw {a b c : α} : sbtw a b c ↔ ¬btw c b a

Proof state:
α : Type u_1
inst✝ : CircularOrder α
a b c : α
⊢ sbtw a b c ↔ ¬btw c b a

Tactic:
rw [sbtw_iff_btw_not_btw]

Result:
α : Type u_1
inst✝ : CircularOrder α
a b c : α
⊢ btw a b c ∧ ¬btw c b a ↔ ¬btw c b a

Proof state:
α : Type u_1
inst✝ : CircularOrder α
a b c : α
⊢ btw a b c ∧ ¬btw c b a ↔ ¬btw c b a

Tactic:
exact and_iff_right_of_imp (btw_total _ _ _).resolve_left

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_of_sub_nonpos {a b : Int} (h : a - b ≤ 0) : a ≤ b

Proof state:
a b : Int
h : a - b ≤ 0
⊢ a ≤ b

Tactic:
have h := Int.add_le_add_right h b

Result:
a b : Int
h✝ : a - b ≤ 0
h : a - b + b ≤ 0 + b
⊢ a ≤ b

Proof state:
a b : Int
h✝ : a - b ≤ 0
h : a - b + b ≤ 0 + b
⊢ a ≤ b

Tactic:
rwa [Int.sub_add_cancel, Int.zero_add] at h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_C : (C a).eval₂ f x = f a

Proof state:
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (C a) = f a

Tactic:
simp [eval₂_eq_sum]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem not_bddAbove_principal (op : Ordinal → Ordinal → Ordinal) :
    ¬ BddAbove { o | Principal op o }

Proof state:
case intro
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
ha : a ∈ upperBounds {o | Principal op o}
⊢ False

Tactic:
exact ((le_nfp _ _).trans (ha (principal_nfp_iSup op (succ a)))).not_lt (lt_succ a)

Result:
no goals

Proof state:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
⊢ ¬BddAbove {o | Principal op o}

Tactic:
rintro ⟨a, ha⟩

Result:
case intro
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
ha : a ∈ upperBounds {o | Principal op o}
⊢ False
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem interior_Ioc [NoMaxOrder α] {a b : α} : interior (Ioc a b) = Ioo a b

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
⊢ interior (Ioc a b) = Ioo a b

Tactic:
rw [← Ioi_inter_Iic, interior_inter, interior_Ioi, interior_Iic, Ioi_inter_Iio]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem smul_mem_lifts {p : S[X]} (r : R) (hp : p ∈ lifts (algebraMap R S)) :
    r • p ∈ lifts (algebraMap R S)

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : S[X]
r : R
hp : p ∈ lifts (algebraMap R S)
⊢ r • p ∈ lifts (algebraMap R S)

Tactic:
rw [mem_lifts_iff_mem_alg] at hp ⊢

Result:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : S[X]
r : R
hp : p ∈ (mapAlg R S).range
⊢ r • p ∈ (mapAlg R S).range

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : S[X]
r : R
hp : p ∈ (mapAlg R S).range
⊢ r • p ∈ (mapAlg R S).range

Tactic:
exact Subalgebra.smul_mem (mapAlg R S).range hp r

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)} :
    (insertMany m l).isEmpty = (m.isEmpty && l.isEmpty)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
⊢ (insertMany m l).isEmpty = (m.isEmpty && l.isEmpty)

Tactic:
simp_to_raw using Raw₀.Const.isEmpty_insertMany_list

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem edist_dist (f g : Lp E p μ) : edist f g = .ofReal (dist f g)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
rw [edist_def, dist_def, ← eLpNorm_congr_ae (coeFn_sub _ _),
  ENNReal.ofReal_toReal (eLpNorm_ne_top (f - g))]

Result:
no goals
-- Mathlib/Data/PEquiv.lean
theorem symm_trans_self (f : α ≃. β) : f.symm.trans f = ofSet { b | (f.symm b).isSome } :=
  symm_injective <| by simp [symm_trans_rev, self_trans_symm, -symm_symm]

Proof state:
α : Type u
β : Type v
f : α ≃. β
⊢ (f.symm.trans f).symm = (ofSet {b | (f.symm b).isSome = true}).symm

Tactic:
simp [symm_trans_rev, self_trans_symm, -symm_symm]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem trailingDegree_monomial (ha : a ≠ 0) : trailingDegree (monomial n a) = n

Proof state:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
ha : a ≠ 0
⊢ ((monomial n) a).trailingDegree = ↑n

Tactic:
rw [trailingDegree, support_monomial n ha, min_singleton]

Result:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑n = ↑n

Proof state:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑n = ↑n

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_antiperiodic : Function.Antiperiodic cos π

Proof state:
⊢ Function.Antiperiodic cos ↑π

Tactic:
simp [cos_add]

Result:
no goals
-- Mathlib/Tactic/NormNum/BigOperators.lean
lemma Multiset.range_zero' {n : ℕ} (pn : NormNum.IsNat n 0) :
    Multiset.range n = 0

Proof state:
n : ℕ
pn : NormNum.IsNat n 0
⊢ Multiset.range n = 0

Tactic:
rw [pn.out, Nat.cast_zero, Multiset.range_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean
@[simp]
lemma toProd_one_tmul_ι (m₂ : M₂) : toProd Q₁ Q₂ (1 ᵍ⊗ₜ ι _ m₂) = ι _ (0, m₂)

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₂ : M₂
⊢ (toProd Q₁ Q₂) (1 ᵍ⊗ₜ[R] (ι Q₂) m₂) = (ι (QuadraticMap.prod Q₁ Q₂)) (0, m₂)

Tactic:
rw [toProd, GradedTensorProduct.lift_tmul, map_one, one_mul, map_apply_ι,
  QuadraticMap.Isometry.inr_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem all_eq_false {p : α → Bool} {xs : Vector α n} :
    xs.all p = false ↔ ∃ (i : Nat) (_ : i < n), ¬p xs[i]

Proof state:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ xs.all p = false ↔ ∃ i x, ¬p xs[i] = true

Tactic:
rw [Bool.eq_false_iff, Ne, all_eq_true]

Result:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ (¬∀ (i : Nat) (x : i < n), p xs[i] = true) ↔ ∃ i x, ¬p xs[i] = true

Proof state:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ (¬∀ (i : Nat) (x : i < n), p xs[i] = true) ↔ ∃ i x, ¬p xs[i] = true

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem mem_transpose {μ : YoungDiagram} {c : ℕ × ℕ} : c ∈ μ.transpose ↔ c.swap ∈ μ

Proof state:
μ : YoungDiagram
c : ℕ × ℕ
⊢ c ∈ μ.transpose ↔ c.swap ∈ μ

Tactic:
simp [transpose]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_congr_mono (hs : s ⊆ t) (h : μ.restrict t = ν.restrict t) :
    μ.restrict s = ν.restrict s

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : s ⊆ t
h : μ.restrict t = ν.restrict t
⊢ μ.restrict s = ν.restrict s

Tactic:
rw [← restrict_restrict_of_subset hs, h, restrict_restrict_of_subset hs]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma nnrpow_inv_nnrpow (a : A) {x : ℝ≥0} (hx : x ≠ 0) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
hx : x ≠ 0
ha : autoParam (0 ≤ a) _auto✝
⊢ (a ^ x⁻¹) ^ x = a

Tactic:
simp [inv_mul_cancel₀ hx, nnrpow_one _ ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y

Proof state:
ε : Type u_1
m : Type u_1 → Type u_2
α : Type u_1
x y : ExceptT ε m α
h : x.run = y.run
⊢ x = y

Tactic:
simp [run] at h

Result:
ε : Type u_1
m : Type u_1 → Type u_2
α : Type u_1
x y : ExceptT ε m α
h : x = y
⊢ x = y

Proof state:
ε : Type u_1
m : Type u_1 → Type u_2
α : Type u_1
x y : ExceptT ε m α
h : x = y
⊢ x = y

Tactic:
assumption

Result:
no goals
-- Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean
theorem NoZeroSMulDivisors.int_of_charZero
    (R) (M) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] :
    NoZeroSMulDivisors ℤ M :=
  ⟨fun {z x} h ↦ by simpa [← smul_one_smul R z x] using h⟩

Proof state:
R : Type u_3
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
z : ℤ
x : M
h : z • x = 0
⊢ z = 0 ∨ x = 0

Tactic:
simpa [← smul_one_smul R z x] using h

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/FixedPoints.lean
theorem smul_inv_mem_fixedBy_iff_mem_fixedBy {a : α} {g : G} :
    g⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α g

Proof state:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ g⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α g

Tactic:
rw [← fixedBy_inv, smul_mem_fixedBy_iff_mem_fixedBy, fixedBy_inv]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem inv_mul_cancel_right₀ (h : b ≠ 0) (a : G₀) : a * b⁻¹ * b = a :=
  calc
    a * b⁻¹ * b = a * (b⁻¹ * b) := mul_assoc _ _ _
    _ = a

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
b : G₀
h : b ≠ 0
a : G₀
⊢ a * (b⁻¹ * b) = a

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/Sheaves/Stalks.lean
theorem germ_res_apply (F : X.Presheaf C)
    {U V : Opens X} (i : U ⟶ V) (x : X) (hx : x ∈ U) [ConcreteCategory C FC] (s) :
    F.germ U x hx (F.map i.op s) = F.germ V x (i.le hx) s

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
U V : Opens ↑X
i : U ⟶ V
x : ↑X
hx : x ∈ U
inst✝ : ConcreteCategory C FC
s : CC (F.obj (op V))
⊢ (ConcreteCategory.hom (F.germ U x hx)) ((ConcreteCategory.hom (F.map i.op)) s) =
    (ConcreteCategory.hom (F.germ V x ⋯)) s

Tactic:
rw [← ConcreteCategory.comp_apply, germ_res]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sub_eq_self {x : BitVec 1} : -x = x

Proof state:
x : BitVec 1
ha : x = 0 ∨ x = 1
⊢ -x = x

Tactic:
rcases ha with h | h <;> simp [h]

Result:
no goals

Proof state:
x : BitVec 1
⊢ -x = x

Tactic:
have ha : x = 0 ∨ x = 1 := eq_zero_or_eq_one _

Result:
x : BitVec 1
ha : x = 0 ∨ x = 1
⊢ -x = x
-- Mathlib/Algebra/Category/Semigrp/Basic.lean
@[to_additive]
lemma id_apply (M : MagmaCat) (x : M) :
    (𝟙 M : M ⟶ M) x = x

Proof state:
M : MagmaCat
x : ↑M
⊢ (ConcreteCategory.hom (𝟙 M)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem eval_const : ∀ n m, eval (Code.const n) m = Part.some n
  | 0, _ => rfl
  | n + 1, m => by simp! [eval_const n m]

Proof state:
n m : ℕ
⊢ (Code.const (n + 1)).eval m = Part.some (n + 1)

Tactic:
simp! [eval_const n m]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem lift_lift'_assoc {g : Set α → Set β} {h : Set β → Filter γ} (hg : Monotone g)
    (hh : Monotone h) : (f.lift' g).lift h = f.lift fun s => h (g s) :=
  calc
    (f.lift' g).lift h = f.lift fun s => (𝓟 (g s)).lift h := lift_assoc (monotone_principal.comp hg)
    _ = f.lift fun s => h (g s)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Set β
h : Set β → Filter γ
hg : Monotone g
hh : Monotone h
⊢ (f.lift fun s => (𝓟 (g s)).lift h) = f.lift fun s => h (g s)

Tactic:
simp only [lift_principal, hh, eq_self_iff_true]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_add_right' (a b : α) : toIcoMod hp (a + p) b = toIcoMod hp a b + p

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

Tactic:
simpa only [one_zsmul] using toIcoMod_add_zsmul' hp a b 1

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Trim.lean
lemma trim_add {ν : Measure α} (hm : m ≤ m0) : (μ + ν).trim hm = μ.trim hm + ν.trim hm :=
  @Measure.ext _ m _ _ (fun s hs ↦ by simp [trim_measurableSet_eq hm hs])

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
⊢ ((μ + ν).trim hm) s = (μ.trim hm + ν.trim hm) s

Tactic:
simp [trim_measurableSet_eq hm hs]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem nat_eq_lift_iff {n : ℕ} {a : Cardinal.{u}} :
    (n : Cardinal) = lift.{v} a ↔ (n : Cardinal) = a

Proof state:
n : ℕ
a : Cardinal.{u}
⊢ ↑n = lift.{v, u} a ↔ ↑n = a

Tactic:
rw [← lift_natCast.{v,u} n, lift_inj]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem ringEquivOfRingEquiv_mk' {j : R ≃+* P} (H : M.map j.toMonoidHom = T) (x : R) (y : M) :
    ringEquivOfRingEquiv S Q j H (mk' S x y) =
      mk' Q (j x) ⟨j y, show j y ∈ T from H ▸ Set.mem_image_of_mem j y.2⟩

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
j : R ≃+* P
H : Submonoid.map j.toMonoidHom M = T
x : R
y : ↥M
⊢ (ringEquivOfRingEquiv S Q j H) (mk' S x y) = mk' Q (j x) ⟨j ↑y, ⋯⟩

Tactic:
simp [map_mk']

Result:
no goals
-- Mathlib/Data/Sum/Interval.lean
lemma Ioo_inl_inl :
    Ioo (inlₗ a₁ : α ⊕ₗ β) (inlₗ a₂) = (Ioo a₁ a₂).map (Embedding.inl.trans toLex.toEmbedding)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Ioo (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioo a₁ a₂))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Ioo (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Ioo a₁ a₂)

Tactic:
rw [← Finset.map_map]

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Ioo (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioo a₁ a₂))
-- Mathlib/Data/Finite/Card.lean
theorem card_option [Finite α] : Nat.card (Option α) = Nat.card α + 1

Proof state:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (Option α) = Nat.card α + 1

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_option]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Finite α
⊢ Nat.card (Option α) = Nat.card α + 1

Tactic:
haveI := Fintype.ofFinite α

Result:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (Option α) = Nat.card α + 1