harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Lattice/Union.lean
theorem sup_eq_biUnion {α β} [DecidableEq β] (s : Finset α) (t : α → Finset β) :
    s.sup t = s.biUnion t

Proof state:
case h
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
a✝ : β
⊢ a✝ ∈ s.sup t ↔ a✝ ∈ s.biUnion t

Tactic:
rw [mem_sup, mem_biUnion]

Result:
no goals

Proof state:
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
⊢ s.sup t = s.biUnion t

Tactic:
ext

Result:
case h
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
a✝ : β
⊢ a✝ ∈ s.sup t ↔ a✝ ∈ s.biUnion t
-- Mathlib/Data/Fin/Basic.lean
theorem range_castSucc {n : ℕ} : Set.range (castSucc : Fin n → Fin n.succ) =
    ({ i | (i : ℕ) < n } : Set (Fin n.succ)) := range_castLE (by omega)

Proof state:
n : ℕ
⊢ n ≤ n + 1

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem toArray_appendList (l₁ l₂ : List α) :
    l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray

Proof state:
case h
α : Type u_1
l₁ l₂ : List α
⊢ (l₁.toArray ++ l₂).toList = (l₁ ++ l₂).toArray.toList

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
⊢ l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
l₁ l₂ : List α
⊢ (l₁.toArray ++ l₂).toList = (l₁ ++ l₂).toArray.toList
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem reverse_concat {u v w : V} (p : G.Walk u v) (h : G.Adj v w) :
    (p.concat h).reverse = cons (G.symm h) p.reverse

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).reverse = cons ⋯ p.reverse

Tactic:
simp [concat_eq_append]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_div_add (hc : c ≠ 0) (d) :
    (∫ x in a..b, f (x / c + d)) = c • ∫ x in a / c + d..b / c + d, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (x / c + d) = c • ∫ (x : ℝ) in a / c + d..b / c + d, f x

Tactic:
simpa only [div_eq_inv_mul, inv_inv] using integral_comp_mul_add f (inv_ne_zero hc) d

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem repr_ofNat (n : ℕ) : repr (ofNat n) = n

Proof state:
n : ℕ
⊢ (↑n).repr = ↑n

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_smul_smul {c : ℝ} (hc : c ≠ 0) (x y : V) : angle (c • x) (c • y) = angle x y

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
⊢ angle (c • x) (c • y) = angle x y

Tactic:
rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, Real.norm_eq_abs,
  mul_mul_mul_comm _ ‖x‖, abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
⊢ angle (c • x) (c • y) = angle x y

Tactic:
have : c * c ≠ 0 := mul_ne_zero hc hc

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
⊢ angle (c • x) (c • y) = angle x y
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem superpolynomialDecay_iff_superpolynomialDecay_abs :
    SuperpolynomialDecay l k f ↔ SuperpolynomialDecay l (fun a => |k a|) fun a => |f a| :=
  (superpolynomialDecay_iff_abs_tendsto_zero l k f).trans
    (by simp_rw [SuperpolynomialDecay, abs_mul, abs_pow])

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
⊢ (∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)) ↔ SuperpolynomialDecay l (fun a => |k a|) fun a => |f a|

Tactic:
simp_rw [SuperpolynomialDecay, abs_mul, abs_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem empty_append_fun : ((#[] : Array α) ++ ·) = id

Proof state:
α : Type u_1
⊢ (fun x => #[] ++ x) = id

Tactic:
funext ⟨l⟩

Result:
case h
α : Type u_1
l : List α
⊢ #[] ++ { toList := l } = id { toList := l }

Proof state:
case h
α : Type u_1
l : List α
⊢ #[] ++ { toList := l } = id { toList := l }

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/HolderNorm.lean
lemma MemHolder.nnHolderNorm_nsmul [Module ℝ Y] [BoundedSMul ℝ Y] (n : ℕ) (hf : MemHolder r f) :
    nnHolderNorm r (n • f) = n • nnHolderNorm r f

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : MetricSpace X
inst✝² : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
inst✝¹ : Module ℝ Y
inst✝ : BoundedSMul ℝ Y
n : ℕ
hf : MemHolder r f
⊢ nnHolderNorm r (n • f) = n • nnHolderNorm r f

Tactic:
simp [← Nat.cast_smul_eq_nsmul (R := ℝ), hf.nnHolderNorm_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem right_inv_eq_left_inv (h : A * B = 1) (g : C * A = 1) : B = C

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : C * A = 1
⊢ B = C

Tactic:
rw [← inv_eq_right_inv h, ← inv_eq_left_inv g]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem tail_cons (a : α) (s) : tail (cons a s) = s

Proof state:
α : Type u
a : α
s : WSeq α
⊢ (cons a s).tail = s

Tactic:
simp [tail]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_inter_Ioc_of_left_le (h : b₁ ≤ b₂) : Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioo (max a₁ a₂) b₁

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₁ ≤ b₂
⊢ Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioo (a₁ ⊔ a₂) b₁

Tactic:
rw [inter_comm, Ioc_inter_Ioo_of_right_le h, max_comm]

Result:
no goals
-- Mathlib/Topology/Homotopy/HomotopyGroup.lean
theorem copy_eq (f : Ω^ N X x) {g : (I^N) → X} (h : g = f) : copy f g h = f

Proof state:
case H
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
f : ↑(Ω^ N X x✝)
g : (N → ↑I) → X
h : g = ⇑f
x : N → ↑I
⊢ (copy f g h) x = f x

Tactic:
exact congr_fun h x

Result:
no goals

Proof state:
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x : X
f : ↑(Ω^ N X x)
g : (N → ↑I) → X
h : g = ⇑f
⊢ copy f g h = f

Tactic:
ext x

Result:
case H
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
f : ↑(Ω^ N X x✝)
g : (N → ↑I) → X
h : g = ⇑f
x : N → ↑I
⊢ (copy f g h) x = f x
-- Mathlib/Order/SymmDiff.lean
theorem le_symmDiff_iff_left : a ≤ a ∆ b ↔ Disjoint a b

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ (a ⊔ b) \ (a ⊓ b)
⊢ Disjoint a b

Tactic:
exact disjoint_iff_inf_le.mpr (le_sdiff_right.1 <| inf_le_of_left_le h).le

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ a ∆ b
⊢ Disjoint a b

Tactic:
rw [symmDiff_eq_sup_sdiff_inf] at h

Result:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ (a ⊔ b) \ (a ⊓ b)
⊢ Disjoint a b

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ≤ a ∆ b ↔ Disjoint a b

Tactic:
refine ⟨fun h => ?_, fun h => h.symmDiff_eq_sup.symm ▸ le_sup_left⟩

Result:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ a ∆ b
⊢ Disjoint a b
-- Mathlib/Topology/Basic.lean
theorem Set.Finite.interior_biInter {ι : Type*} {s : Set ι} (hs : s.Finite) (f : ι → Set X) :
    interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i) :=
  hs.induction_on _ (by simp) <| by intros; simp [*]

Proof state:
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_3
s : Set ι
hs : s.Finite
f : ι → Set X
⊢ ∀ {a : ι} {s : Set ι},
    a ∉ s →
      s.Finite →
        interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i) →
          interior (⋂ i ∈ insert a s, f i) = ⋂ i ∈ insert a s, interior (f i)

Tactic:
intros

Result:
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_3
s : Set ι
hs : s.Finite
f : ι → Set X
a✝² : ι
s✝ : Set ι
a✝¹ : a✝² ∉ s✝
hs✝ : s✝.Finite
a✝ : interior (⋂ i ∈ s✝, f i) = ⋂ i ∈ s✝, interior (f i)
⊢ interior (⋂ i ∈ insert a✝² s✝, f i) = ⋂ i ∈ insert a✝² s✝, interior (f i)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_3
s : Set ι
hs : s.Finite
f : ι → Set X
⊢ interior (⋂ i ∈ ∅, f i) = ⋂ i ∈ ∅, interior (f i)

Tactic:
simp

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_3
s : Set ι
hs : s.Finite
f : ι → Set X
a✝² : ι
s✝ : Set ι
a✝¹ : a✝² ∉ s✝
hs✝ : s✝.Finite
a✝ : interior (⋂ i ∈ s✝, f i) = ⋂ i ∈ s✝, interior (f i)
⊢ interior (⋂ i ∈ insert a✝² s✝, f i) = ⋂ i ∈ insert a✝² s✝, interior (f i)

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
lemma mem_inf_principal {f : Filter α} {s t : Set α} : s ∈ f ⊓ 𝓟 t ↔ { x | x ∈ t → x ∈ s } ∈ f

Proof state:
α : Type u
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t ↔ {x | x ∈ t → x ∈ s} ∈ f

Tactic:
simp only [mem_inf_principal', imp_iff_not_or, setOf_or, compl_def, setOf_mem_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
theorem Basis.addHaar_self (b : Basis ι ℝ E) : b.addHaar (_root_.parallelepiped b) = 1

Proof state:
ι : Type u_1
E : Type u_3
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ (addHaarMeasure b.parallelepiped) (_root_.parallelepiped ⇑b) = 1

Tactic:
exact addHaarMeasure_self

Result:
no goals

Proof state:
ι : Type u_1
E : Type u_3
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ b.addHaar (_root_.parallelepiped ⇑b) = 1

Tactic:
rw [Basis.addHaar]

Result:
ι : Type u_1
E : Type u_3
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ (addHaarMeasure b.parallelepiped) (_root_.parallelepiped ⇑b) = 1
-- Mathlib/Data/Complex/Order.lean
theorem real_le_real {x y : ℝ} : (x : ℂ) ≤ (y : ℂ) ↔ x ≤ y

Proof state:
x y : ℝ
⊢ ↑x ≤ ↑y ↔ x ≤ y

Tactic:
simp [le_def, ofReal]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem volume_negAt_plusPart (hm : MeasurableSet A) :
    volume (negAt s '' (plusPart A)) = volume (plusPart A)

Proof state:
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
⊢ volume (⇑(negAt s) '' plusPart A) = volume (plusPart A)

Tactic:
rw [← negAt_symm, ContinuousLinearEquiv.image_symm_eq_preimage,
  volume_preserving_negAt.measure_preimage (measurableSet_plusPart hm).nullMeasurableSet]

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

Proof state:
n m k : Nat
⊢ n + m + k = n + k + m

Tactic:
rw [Nat.add_assoc, Nat.add_comm m k, ← Nat.add_assoc]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem sign_mul_abs : ∀ x : EReal, (sign x * x.abs : EReal) = x
  | ⊥ => by simp
  | ⊤ => by simp
  | (x : ℝ) => by rw [sign_coe, coe_abs, ← coe_coe_sign, ← coe_mul, sign_mul_abs]

Proof state:
⊢ ↑(sign ⊥) * ↑⊥.abs = ⊥

Tactic:
simp

Result:
no goals

Proof state:
x : ℝ
⊢ ↑(sign ↑x) * ↑(↑x).abs = ↑x

Tactic:
rw [sign_coe, coe_abs, ← coe_coe_sign, ← coe_mul, sign_mul_abs]

Result:
no goals

Proof state:
⊢ ↑(sign ⊤) * ↑⊤.abs = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem blimsup_and_le_inf : (blimsup u f fun x => p x ∧ q x) ≤ blimsup u f p ⊓ blimsup u f q :=
  le_inf (blimsup_mono <| by tauto) (blimsup_mono <| by tauto)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ ∀ (x : β), p x ∧ q x → q x

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ ∀ (x : β), p x ∧ q x → p x

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive]
protected lemma one_div_mul_cancel (h : IsUnit a) : 1 / a * a = 1

Proof state:
α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ 1 / a * a = 1

Tactic:
simp [h]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma jacobiTheta₂''_neg_left (z τ : ℂ) : jacobiTheta₂'' (-z) τ = -jacobiTheta₂'' z τ

Proof state:
z τ : ℂ
⊢ jacobiTheta₂'' (-z) τ = -jacobiTheta₂'' z τ

Tactic:
simp [jacobiTheta₂'', jacobiTheta₂'_neg_left, neg_div, -neg_add_rev, ← neg_add]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem Rel.symm {x y : α × α} : Rel α x y → Rel α y x

Proof state:
α : Type u_1
x y : α × α
⊢ Rel α x y → Rel α y x

Tactic:
aesop (rule_sets := [Sym2])

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
/-- If `a ≠ 0` and `a ≠ ∞`, then right multiplication by `a` maps infimum to infimum.

See `ENNReal.mul_iInf'` for the general case, and `ENNReal.iInf_mul` for another special case that
assumes `Nonempty ι` but does not require `a ≠ 0`, and `ENNReal`. -/
lemma mul_iInf_of_ne (ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * ⨅ i, f i = ⨅ i, a * f i :=
  mul_iInf' (by simp [ha]) (by simp [ha₀])

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0

Tactic:
simp [ha]

Result:
no goals

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a = 0 → Nonempty ι

Tactic:
simp [ha₀]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhds_of_nhdsWithin_of_nhds {s t : Set α} {a : α} (h1 : s ∈ 𝓝 a) (h2 : t ∈ 𝓝[s] a) :
    t ∈ 𝓝 a

Proof state:
case intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
w✝ : Set α
Hw : w✝ ∈ 𝓝 a
hw : w✝ ∩ s ⊆ t
⊢ t ∈ 𝓝 a

Tactic:
exact (𝓝 a).sets_of_superset ((𝓝 a).inter_sets Hw h1) hw

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
⊢ t ∈ 𝓝 a

Tactic:
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.mp h2 with ⟨_, Hw, hw⟩

Result:
case intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
w✝ : Set α
Hw : w✝ ∈ 𝓝 a
hw : w✝ ∩ s ⊆ t
⊢ t ∈ 𝓝 a
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem isometry_iff_dist_eq [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} :
    Isometry f ↔ ∀ x y, dist (f x) (f y) = dist x y

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ Isometry f ↔ ∀ (x y : α), dist (f x) (f y) = dist x y

Tactic:
simp only [isometry_iff_nndist_eq, ← coe_nndist, NNReal.coe_inj]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cot_conj : cot (conj x) = conj (cot x)

Proof state:
x : ℂ
⊢ ((starRingEnd ℂ) x).cot = (starRingEnd ℂ) x.cot

Tactic:
rw [cot, sin_conj, cos_conj, ← map_div₀, cot]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : as.contains a = true

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
toList✝ : List α
h : a ∈ { toList := toList✝ }
⊢ { toList := toList✝ }.contains a = true

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : Array α
h : a ∈ as
⊢ as.contains a = true

Tactic:
cases as

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
toList✝ : List α
h : a ∈ { toList := toList✝ }
⊢ { toList := toList✝ }.contains a = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem unzip_fst : (unzip l).fst = l.map Prod.fst

Proof state:
α✝ : Type u_1
β✝ : Type u_2
n✝ : Nat
l : Vector (α✝ × β✝) n✝
⊢ l.unzip.fst = map Prod.fst l

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Data/Int/CardIntervalMod.lean
theorem Ico_filter_modEq_card (v : ℤ) :
    #{x ∈ Ico a b | x ≡ v [ZMOD r]} = max (⌈(b - v) / (r : ℚ)⌉ - ⌈(a - v) / (r : ℚ)⌉) 0

Proof state:
a b r : ℤ
hr : 0 < r
v : ℤ
⊢ ↑(#(filter (fun x => x ≡ v [ZMOD r]) (Ico a b))) = (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) ⊔ 0

Tactic:
simp [Ico_filter_modEq_eq, Ico_filter_dvd_eq, toNat_eq_max, hr]

Result:
no goals
-- Mathlib/Order/BooleanSubalgebra.lean
/-- An induction principle for closure membership. If `p` holds for `⊥` and all elements of `s`, and
is preserved under suprema and complement, then `p` holds for all elements of the closure of `s`. -/
@[elab_as_elim]
lemma closure_bot_sup_induction {p : ∀ g ∈ closure s, Prop} (mem : ∀ x hx, p x (subset_closure hx))
    (bot : p ⊥ bot_mem)
    (sup : ∀ x hx y hy, p x hx → p y hy → p (x ⊔ y) (supClosed _ hx hy))
    (compl : ∀ x hx, p x hx → p xᶜ (compl_mem hx)) {x} (hx : x ∈ closure s) : p x hx :=
  have inf ⦃x hx y hy⦄ (hx' : p x hx) (hy' : p y hy) : p (x ⊓ y) (infClosed _ hx hy)

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
p : (g : α) → g ∈ closure s → Prop
mem : ∀ (x : α) (hx : x ∈ s), p x ⋯
bot : p ⊥ ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
compl : ∀ (x : α) (hx : x ∈ closure s), p x hx → p xᶜ ⋯
x✝ : α
hx✝ : x✝ ∈ closure s
x : α
hx : x ∈ closure s
y : α
hy : y ∈ closure s
hx' : p x hx
hy' : p y hy
⊢ p (x ⊓ y) ⋯

Tactic:
simpa using compl _ _ <| sup _ _ _ _ (compl _ _ hx') (compl _ _ hy')

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_inter_Ioi : Ioc a b ∩ Ioi c = Ioc (a ⊔ c) b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioc a b ∩ Ioi c = Ioc (a ⊔ c) b

Tactic:
rw [← Ioi_inter_Iic, inter_assoc, inter_comm, inter_assoc, Ioi_inter_Ioi, inter_comm,
  Ioi_inter_Iic, sup_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem sum_mkArray_nat (n : Nat) (a : Nat) : (mkArray n a).sum = n * a

Proof state:
n a : Nat
⊢ (List.replicate n a).sum = n * a

Tactic:
simp

Result:
no goals

Proof state:
n a : Nat
⊢ (mkArray n a).sum = n * a

Tactic:
rw [← List.toArray_replicate, List.sum_toArray]

Result:
n a : Nat
⊢ (List.replicate n a).sum = n * a
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem aleph0_eq_lift {c : Cardinal.{u}} : ℵ₀ = lift.{v} c ↔ ℵ₀ = c

Proof state:
c : Cardinal.{u}
⊢ ℵ₀ = lift.{v, u} c ↔ ℵ₀ = c

Tactic:
simpa using lift_inj (a := ℵ₀)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem fromEdgeSet_empty : fromEdgeSet (∅ : Set (Sym2 V)) = ⊥

Proof state:
V : Type u
⊢ fromEdgeSet ∅ = ⊥

Tactic:
ext v w

Result:
case Adj.h.h.a
V : Type u
v w : V
⊢ (fromEdgeSet ∅).Adj v w ↔ ⊥.Adj v w

Proof state:
case Adj.h.h.a
V : Type u
v w : V
⊢ (fromEdgeSet ∅).Adj v w ↔ ⊥.Adj v w

Tactic:
simp only [fromEdgeSet_adj, Set.mem_empty_iff_false, false_and, bot_adj]

Result:
no goals
-- Mathlib/Data/Set/Finite/Lattice.lean
lemma Set.finite_diff_iUnion_Ioo' (s : Set α) : (s \ ⋃ x : s × s, Ioo x.1 x.2).Finite

Proof state:
α : Type u
inst✝ : LinearOrder α
s : Set α
⊢ (s \ ⋃ x, Ioo ↑x.1 ↑x.2).Finite

Tactic:
simpa only [iUnion, iSup_prod, iSup_subtype] using s.finite_diff_iUnion_Ioo

Result:
no goals
-- Mathlib/Order/Filter/IndicatorFunction.lean
theorem Antitone.mulIndicator_eventuallyEq_iInter {ι} [Preorder ι] [One β] (s : ι → Set α)
    (hs : Antitone s) (f : α → β) (a : α) :
    (fun i => mulIndicator (s i) f a) =ᶠ[atTop] fun _ ↦ mulIndicator (⋂ i, s i) f a

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Antitone s
f : α → β
a : α
⊢ (fun i => (s i).mulIndicator f a) =ᶠ[atTop] fun x => (⋂ i, s i).mulIndicator f a

Tactic:
exact hs.piecewise_eventually_eq_iInter f 1 a

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Antitone s
f : α → β
a : α
⊢ (fun i => (s i).mulIndicator f a) =ᶠ[atTop] fun x => (⋂ i, s i).mulIndicator f a

Tactic:
classical exact hs.piecewise_eventually_eq_iInter f 1 a

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem AnalyticOnNhd.continuous {f : E → F} (fa : AnalyticOnNhd 𝕜 f univ) : Continuous f

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
fa : AnalyticOnNhd 𝕜 f univ
⊢ ContinuousOn f univ

Tactic:
exact fa.continuousOn

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
fa : AnalyticOnNhd 𝕜 f univ
⊢ Continuous f

Tactic:
rw [continuous_iff_continuousOn_univ]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
fa : AnalyticOnNhd 𝕜 f univ
⊢ ContinuousOn f univ
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
lemma yonedaULeftEquiv_symm_map {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : Sheaf J (Type (max v v'))}
    (t : F.val.obj X) : J.yonedaULiftEquiv.symm (F.val.map f t) =
      J.yonedaULift.map f.unop ≫ J.yonedaULiftEquiv.symm t

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
t : F.val.obj X
⊢ J.yonedaULiftEquiv.symm (F.val.map f t) = (yonedaULift.{v', v, u} J).map f.unop ≫ J.yonedaULiftEquiv.symm t

Tactic:
obtain ⟨u, rfl⟩ := J.yonedaULiftEquiv.surjective t

Result:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
u : (yonedaULift.{v', v, u} J).obj (unop X) ⟶ F
⊢ J.yonedaULiftEquiv.symm (F.val.map f (J.yonedaULiftEquiv u)) =
    (yonedaULift.{v', v, u} J).map f.unop ≫ J.yonedaULiftEquiv.symm (J.yonedaULiftEquiv u)

Proof state:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
u : (yonedaULift.{v', v, u} J).obj (unop X) ⟶ F
⊢ J.yonedaULiftEquiv.symm (F.val.map f (J.yonedaULiftEquiv u)) =
    (yonedaULift.{v', v, u} J).map f.unop ≫ J.yonedaULiftEquiv.symm (J.yonedaULiftEquiv u)

Tactic:
rw [yonedaULiftEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]

Result:
no goals
-- Mathlib/ModelTheory/Basic.lean
theorem symm_comp_self_toHom (f : M ≃[L] N) :
    f.symm.toHom.comp f.toHom = Hom.id L M

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ f.symm.toHom.comp f.toHom = Hom.id L M

Tactic:
rw [← comp_toHom, symm_comp_self, refl_toHom]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_le {x y : BitVec n} : ¬ x ≤ y ↔ y < x

Proof state:
n : Nat
x y : BitVec n
⊢ ¬x ≤ y ↔ y < x

Tactic:
simp [le_def, lt_def]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
lemma FractionalIdeal.le_inv_comm {I J : FractionalIdeal A⁰ K} (hI : I ≠ 0) (hJ : J ≠ 0) :
    I ≤ J⁻¹ ↔ J ≤ I⁻¹

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : FractionalIdeal A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
⊢ I ≤ J⁻¹ ↔ J ≤ I⁻¹

Tactic:
rw [inv_eq, inv_eq, le_div_iff_mul_le hI, le_div_iff_mul_le hJ, mul_comm]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
@[fun_prop]
lemma Units.continuousOn_zpow₀_spectrum [ContinuousMul R] (a : Aˣ) (n : ℤ) :
    ContinuousOn (· ^ n) (spectrum R (a : A)) :=
  (continuousOn_zpow₀ n).mono <| by
    simpa only [Set.subset_compl_singleton_iff] using spectrum.zero_not_mem R a.isUnit

Proof state:
R : Type u_3
A : Type u_4
inst✝⁵ : Semifield R
inst✝⁴ : Ring A
inst✝³ : TopologicalSpace R
inst✝² : HasContinuousInv₀ R
inst✝¹ : Algebra R A
inst✝ : ContinuousMul R
a : Aˣ
n : ℤ
⊢ spectrum R ↑a ⊆ {0}ᶜ

Tactic:
simpa only [Set.subset_compl_singleton_iff] using spectrum.zero_not_mem R a.isUnit

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reflect_add (f g : R[X]) (N : ℕ) : reflect N (f + g) = reflect N f + reflect N g

Proof state:
R : Type u_1
inst✝ : Semiring R
f g : R[X]
N : ℕ
⊢ reflect N (f + g) = reflect N f + reflect N g

Tactic:
ext

Result:
case a
R : Type u_1
inst✝ : Semiring R
f g : R[X]
N n✝ : ℕ
⊢ (reflect N (f + g)).coeff n✝ = (reflect N f + reflect N g).coeff n✝

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
f g : R[X]
N n✝ : ℕ
⊢ (reflect N (f + g)).coeff n✝ = (reflect N f + reflect N g).coeff n✝

Tactic:
simp only [coeff_add, coeff_reflect]

Result:
no goals