harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_mono_left (h : ∀ x ∈ l, p x → q x) : countP p l ≤ countP q l

Proof state:
α : Type u_1
p q : α → Bool
toList✝ : List α
h : ∀ (x : α), x ∈ { toList := toList✝ } → p x = true → q x = true
⊢ ∀ (x : α), x ∈ toList✝ → p x = true → q x = true

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
p q : α → Bool
l : Array α
h : ∀ (x : α), x ∈ l → p x = true → q x = true
⊢ countP p l ≤ countP q l

Tactic:
cases l

Result:
case mk
α : Type u_1
p q : α → Bool
toList✝ : List α
h : ∀ (x : α), x ∈ { toList := toList✝ } → p x = true → q x = true
⊢ countP p { toList := toList✝ } ≤ countP q { toList := toList✝ }

Proof state:
case mk
α : Type u_1
p q : α → Bool
toList✝ : List α
h : ∀ (x : α), x ∈ { toList := toList✝ } → p x = true → q x = true
⊢ countP p { toList := toList✝ } ≤ countP q { toList := toList✝ }

Tactic:
simpa using List.countP_mono_left (by simpa using h)

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropWithinAt_of_liftPropAt (mono : ∀ ⦃s x t⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x)
    (h : LiftPropAt P g x) : LiftPropWithinAt P g s x

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropAt P g x
⊢ LiftPropWithinAt P g s x

Tactic:
rw [← liftPropWithinAt_univ] at h

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g univ x
⊢ LiftPropWithinAt P g s x

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g univ x
⊢ LiftPropWithinAt P g s x

Tactic:
exact liftPropWithinAt_mono mono h (subset_univ _)

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem one_sub_self_mul_hsum_powers : (1 - x) * (powers x hx).hsum = 1

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
⊢ (1 - x) * (powers x hx).hsum = 1

Tactic:
rw [← hsum_smul, sub_smul 1 x (powers x hx), one_smul, hsum_sub, ←
  hsum_embDomain (x • powers x hx) ⟨Nat.succ, Nat.succ_injective⟩, embDomain_succ_smul_powers]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
⊢ (powers x hx).hsum - (powers x hx - ofFinsupp (Finsupp.single 0 1)).hsum = 1

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
⊢ (powers x hx).hsum - (powers x hx - ofFinsupp (Finsupp.single 0 1)).hsum = 1

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
/-- See `MvPolynomial.IsHomogeneous.funext`
for a version that assumes `Infinite R`. -/
lemma funext_of_le_card (hF : F.IsHomogeneous n) (hG : G.IsHomogeneous n)
    (h : ∀ r : σ → R, eval r F = eval r G) (hnR : n ≤ #R) :
    F = G

Proof state:
R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
hnR : ↑n ≤ #R
⊢ ∀ (r : σ → R), (eval r) (F - G) = 0

Tactic:
simpa [sub_eq_zero] using h

Result:
no goals

Proof state:
R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
hnR : ↑n ≤ #R
⊢ F = G

Tactic:
rw [← sub_eq_zero]

Result:
R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
hnR : ↑n ≤ #R
⊢ F - G = 0

Proof state:
R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
hnR : ↑n ≤ #R
⊢ F - G = 0

Tactic:
apply eq_zero_of_forall_eval_eq_zero_of_le_card (hF.sub hG) _ hnR

Result:
R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
hnR : ↑n ≤ #R
⊢ ∀ (r : σ → R), (eval r) (F - G) = 0
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
lemma sum_range_succ_mul_sum_range_succ (m n : ℕ) (f g : ℕ → α) :
    (∑ i ∈ range (m + 1), f i) * ∑ i ∈ range (n + 1), g i =
      (∑ i ∈ range m, f i) * ∑ i ∈ range n, g i +
        f m * ∑ i ∈ range n, g i + (∑ i ∈ range m, f i) * g n + f m * g n

Proof state:
α : Type u_3
inst✝ : NonUnitalNonAssocSemiring α
m n : ℕ
f g : ℕ → α
⊢ (∑ i ∈ range (m + 1), f i) * ∑ i ∈ range (n + 1), g i =
    (∑ i ∈ range m, f i) * ∑ i ∈ range n, g i + f m * ∑ i ∈ range n, g i + (∑ i ∈ range m, f i) * g n + f m * g n

Tactic:
simp only [add_mul, mul_add, add_assoc, sum_range_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findSome?_mkVector_of_isNone (h : (f a).isNone) :
    findSome? f (mkVector n a) = none

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
h : (f a).isNone = true
⊢ findSome? f (mkVector n a) = none

Tactic:
rw [Option.isNone_iff_eq_none] at h

Result:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
h : f a = none
⊢ findSome? f (mkVector n a) = none

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
h : f a = none
⊢ findSome? f (mkVector n a) = none

Tactic:
simp [findSome?_mkVector, h]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem disjoint_of_erase_right (ha : a ∉ s) (hst : Disjoint s (t.erase a)) : Disjoint s t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
hst : Disjoint s (t.erase a)
⊢ Disjoint s t

Tactic:
rw [← erase_insert ha, disjoint_erase_comm, disjoint_insert_left]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
hst : Disjoint s (t.erase a)
⊢ a ∉ t.erase a ∧ Disjoint s (t.erase a)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
hst : Disjoint s (t.erase a)
⊢ a ∉ t.erase a ∧ Disjoint s (t.erase a)

Tactic:
exact ⟨not_mem_erase _ _, hst⟩

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

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

Tactic:
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Prod.lean
theorem antidiagonal_zero : antidiagonal (0 : A) = {(0, 0)}

Proof state:
A : Type u_1
inst✝² : OrderedAddCommMonoid A
inst✝¹ : CanonicallyOrderedAdd A
inst✝ : HasAntidiagonal A
⊢ antidiagonal 0 = {(0, 0)}

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
A : Type u_1
inst✝² : OrderedAddCommMonoid A
inst✝¹ : CanonicallyOrderedAdd A
inst✝ : HasAntidiagonal A
x y : A
⊢ (x, y) ∈ antidiagonal 0 ↔ (x, y) ∈ {(0, 0)}

Proof state:
case h.mk
A : Type u_1
inst✝² : OrderedAddCommMonoid A
inst✝¹ : CanonicallyOrderedAdd A
inst✝ : HasAntidiagonal A
x y : A
⊢ (x, y) ∈ antidiagonal 0 ↔ (x, y) ∈ {(0, 0)}

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits {k n : ℕ} [hp : Fact p.Prime]
    (h : k ≤ n) : (p - 1) * padicValNat p (choose n k) =
    (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum

Proof state:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n
⊢ (p - 1) * padicValNat p (n.choose k) = (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum

Tactic:
convert @sub_one_mul_padicValNat_choose_eq_sub_sum_digits' _ _ _ ‹_›

Result:
case h.e'_2.h.e'_6.h.e'_2.h.e'_1
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n
⊢ n = n - k + k

case h.e'_3.h.e'_6.h.e'_4.h.e'_2
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n
⊢ n = n - k + k

Proof state:
case h.e'_2.h.e'_6.h.e'_2.h.e'_1
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n
⊢ n = n - k + k

case h.e'_3.h.e'_6.h.e'_4.h.e'_2
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n
⊢ n = n - k + k

Tactic:
all_goals omega

Result:
no goals

Proof state:
case h.e'_3.h.e'_6.h.e'_4.h.e'_2
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n
⊢ n = n - k + k

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem add_congr {a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a + c = b + d

Proof state:
a c d : Int
h₂ : c = d
⊢ a + c = a + d

Tactic:
subst h₂

Result:
a c : Int
⊢ a + c = a + c

Proof state:
a c : Int
⊢ a + c = a + c

Tactic:
rfl

Result:
no goals

Proof state:
a b c d : Int
h₁ : a = b
h₂ : c = d
⊢ a + c = b + d

Tactic:
subst h₁

Result:
a c d : Int
h₂ : c = d
⊢ a + c = a + d
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mkRat_self (a : Rat) : mkRat a.num a.den = a

Proof state:
a : Rat
⊢ mkRat a.num a.den = a

Tactic:
rw [← normalize_eq_mkRat a.den_nz, normalize_self]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_bot : orthogonalProjection (⊥ : Submodule 𝕜 E) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ orthogonalProjection ⊥ = 0

Tactic:
ext

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_set (p : α → Bool) (l : Vector α n) (i : Nat) (a : α) (h : i < n) :
    (l.set i a).countP p = l.countP p - (if p l[i] then 1 else 0) + (if p a then 1 else 0)

Proof state:
case mk
α : Type u_1
n : Nat
p : α → Bool
i : Nat
a : α
h : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ countP p ({ toArray := toArray✝, size_toArray := size_toArray✝ }.set i a h) =
    (countP p { toArray := toArray✝, size_toArray := size_toArray✝ } -
        if p { toArray := toArray✝, size_toArray := size_toArray✝ }[i] = true then 1 else 0) +
      if p a = true then 1 else 0

Tactic:
simp [Array.countP_set, h]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
p : α → Bool
l : Vector α n
i : Nat
a : α
h : i < n
⊢ countP p (l.set i a h) = (countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
p : α → Bool
i : Nat
a : α
h : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ countP p ({ toArray := toArray✝, size_toArray := size_toArray✝ }.set i a h) =
    (countP p { toArray := toArray✝, size_toArray := size_toArray✝ } -
        if p { toArray := toArray✝, size_toArray := size_toArray✝ }[i] = true then 1 else 0) +
      if p a = true then 1 else 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n

Proof state:
a b n : Nat
⊢ (a + b) % n = (a % n + b % n) % n

Tactic:
rw [add_mod_mod, mod_add_mod]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem unit_smul_eq_iff_mul_eq {x y : 𝓞 K} {u : (𝓞 K)ˣ} :
    u • mixedEmbedding K x = mixedEmbedding K y ↔ u * x = y

Proof state:
case I
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ Function.Injective ⇑(mixedEmbedding K)

Tactic:
exact mixedEmbedding_injective K

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ u • (mixedEmbedding K) ↑x = (mixedEmbedding K) ↑y ↔ ↑u * x = y

Tactic:
rw [unitSMul_smul, ← map_mul, Function.Injective.eq_iff, ← RingOfIntegers.coe_eq_algebraMap,
  ← map_mul, ← RingOfIntegers.ext_iff]

Result:
case I
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ Function.Injective ⇑(mixedEmbedding K)
-- Mathlib/Data/Int/Lemmas.lean
theorem le_natCast_sub (m n : ℕ) : (m - n : ℤ) ≤ ↑(m - n : ℕ)

Proof state:
case pos
m n : ℕ
h : m ≥ n
⊢ ↑m - ↑n ≤ ↑(m - n)

Tactic:
exact le_of_eq (Int.ofNat_sub h).symm

Result:
no goals

Proof state:
m n : ℕ
⊢ ↑m - ↑n ≤ ↑(m - n)

Tactic:
by_cases h : m ≥ n

Result:
case pos
m n : ℕ
h : m ≥ n
⊢ ↑m - ↑n ≤ ↑(m - n)

case neg
m n : ℕ
h : ¬m ≥ n
⊢ ↑m - ↑n ≤ ↑(m - n)

Proof state:
case neg
m n : ℕ
h : ¬m ≥ n
⊢ ↑m - ↑n ≤ ↑(m - n)

Tactic:
simp [le_of_not_ge h, ofNat_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem ite_else_decide_not_self (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) :
   (@ite _ p h q (!decide p)) = (!decide p || q)

Proof state:
p : Prop
h w : Decidable p
q : Bool
⊢ (if p then q else !decide p) = (!decide p || q)

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
@[simp, norm_cast] lemma ofReal_natCast (n : ℕ) : ENNReal.ofReal n = n

Proof state:
n : ℕ
⊢ ENNReal.ofReal ↑n = ↑n

Tactic:
simp [ENNReal.ofReal]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem MeasureTheory.AEStronglyMeasurable.prod_swap {γ : Type*} [TopologicalSpace γ]
    [SFinite μ] [SFinite ν] {f : β × α → γ} (hf : AEStronglyMeasurable f (ν.prod μ)) :
    AEStronglyMeasurable (fun z : α × β => f z.swap) (μ.prod ν)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
γ : Type u_4
inst✝² : TopologicalSpace γ
inst✝¹ : SFinite μ
inst✝ : SFinite ν
f : β × α → γ
hf : AEStronglyMeasurable f (ν.prod μ)
⊢ AEStronglyMeasurable (fun z => f z.swap) (μ.prod ν)

Tactic:
rw [← prod_swap] at hf

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
γ : Type u_4
inst✝² : TopologicalSpace γ
inst✝¹ : SFinite μ
inst✝ : SFinite ν
f : β × α → γ
hf : AEStronglyMeasurable f (map Prod.swap (μ.prod ν))
⊢ AEStronglyMeasurable (fun z => f z.swap) (μ.prod ν)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
γ : Type u_4
inst✝² : TopologicalSpace γ
inst✝¹ : SFinite μ
inst✝ : SFinite ν
f : β × α → γ
hf : AEStronglyMeasurable f (map Prod.swap (μ.prod ν))
⊢ AEStronglyMeasurable (fun z => f z.swap) (μ.prod ν)

Tactic:
exact hf.comp_measurable measurable_swap

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem Int.natCast_floor_eq_floor (ha : 0 ≤ a) : (⌊a⌋₊ : ℤ) = ⌊a⌋

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ ↑⌊a⌋₊ = ⌊a⌋

Tactic:
rw [← Int.floor_toNat, Int.toNat_of_nonneg (Int.floor_nonneg.2 ha)]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem mul_pf_left (a₁ : R) (a₂) (_ : a₃ * b = c) :
    (a₁ ^ a₂ * a₃ : R) * b = a₁ ^ a₂ * c

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a₃ b c a₁ : R
a₂ : ℕ
x✝ : a₃ * b = c
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a₃ b a₁ : R
a₂ : ℕ
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a₃ b a₁ : R
a₂ : ℕ
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b)

Tactic:
rw [mul_assoc]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem dist_iterate_succ_le_geometric {f : α → α} (hf : LipschitzWith K f) (x n) :
    dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * (K : ℝ) ^ n

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist (f^[n] x) ((f^[n] ∘ f) x) ≤ ↑K ^ n * dist x (f x)

Tactic:
simpa only [NNReal.coe_pow] using (hf.iterate n).dist_le_mul x (f x)

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * ↑K ^ n

Tactic:
rw [iterate_succ, mul_comm]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist (f^[n] x) ((f^[n] ∘ f) x) ≤ ↑K ^ n * dist x (f x)
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
/-- If `f` is an alternating map from `M` to `N`,
`alternatingMapLinearEquiv f` is the corresponding linear map from `⋀[R]^n M` to `N`,
and if `g` is a linear map from `N` to `N'`, then
the alternating map `g.compAlternatingMap f` from `M` to `N'` corresponds to the linear
map `g.comp (alternatingMapLinearEquiv f)` on `⋀[R]^n M`. -/
lemma alternatingMapLinearEquiv_comp (g : N →ₗ[R] N') (f : M [⋀^Fin n]→ₗ[R] N) :
    alternatingMapLinearEquiv (g.compAlternatingMap f) = g.comp (alternatingMapLinearEquiv f)

Proof state:
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
g : N →ₗ[R] N'
f : M [⋀^Fin n]→ₗ[R] N
⊢ alternatingMapLinearEquiv (g.compAlternatingMap f) = g ∘ₗ alternatingMapLinearEquiv f

Tactic:
ext

Result:
case heq.H
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
g : N →ₗ[R] N'
f : M [⋀^Fin n]→ₗ[R] N
x✝ : Fin n → M
⊢ ((alternatingMapLinearEquiv (g.compAlternatingMap f)).compAlternatingMap (ιMulti R n)) x✝ =
    ((g ∘ₗ alternatingMapLinearEquiv f).compAlternatingMap (ιMulti R n)) x✝

Proof state:
case heq.H
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
g : N →ₗ[R] N'
f : M [⋀^Fin n]→ₗ[R] N
x✝ : Fin n → M
⊢ ((alternatingMapLinearEquiv (g.compAlternatingMap f)).compAlternatingMap (ιMulti R n)) x✝ =
    ((g ∘ₗ alternatingMapLinearEquiv f).compAlternatingMap (ιMulti R n)) x✝

Tactic:
simp only [alternatingMapLinearEquiv_comp_ιMulti, LinearMap.compAlternatingMap_apply,
  LinearMap.coe_comp, comp_apply, alternatingMapLinearEquiv_apply_ιMulti]

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp)]
lemma divConst_inv_right (A B : Finset G) : δₘ[A, B⁻¹] = σₘ[A, B]

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ δₘ[A, B⁻¹] = σₘ[A, B]

Tactic:
rw [mulConst, divConst, div_inv_eq_mul]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
protected lemma Antitone.iInf (hf : ∀ i, Antitone (f i)) : Antitone (⨅ i, f i) :=
  Antitone.sInf (by simpa)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : Preorder α
inst✝ : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), Antitone (f i)
⊢ ∀ f_1 ∈ range fun i => f i, Antitone f_1

Tactic:
simpa

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem vadd_vsub {f : P → P₂} (hf : Isometry f) {p : P} {g : V → V₂}
    (hg : ∀ v, g v = f (v +ᵥ p) -ᵥ f p) : Isometry g

Proof state:
case h.e'_5
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P → P₂
hf : Isometry f
p : P
g : V → V₂
hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p
⊢ g = ⇑(vaddConst 𝕜 (f p)).symm ∘ f ∘ ⇑(vaddConst 𝕜 p)

Tactic:
exact funext hg

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P → P₂
hf : Isometry f
p : P
g : V → V₂
hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p
⊢ Isometry g

Tactic:
convert (vaddConst 𝕜 (f p)).symm.isometry.comp (hf.comp (vaddConst 𝕜 p).isometry)

Result:
case h.e'_5
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P → P₂
hf : Isometry f
p : P
g : V → V₂
hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p
⊢ g = ⇑(vaddConst 𝕜 (f p)).symm ∘ f ∘ ⇑(vaddConst 𝕜 p)
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_sub_linear_isLittleO_of_tendsto_ae [FTCFilter a l l']
    (hfm : StronglyMeasurableAtFilter f l') (hf : Tendsto f (l' ⊓ ae volume) (𝓝 c)) {u v : ι → ℝ}
    (hu : Tendsto u lt l) (hv : Tendsto v lt l) :
    (fun t => (∫ x in u t..v t, f x) - (v t - u t) • c) =o[lt] (v - u)

Proof state:
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
a : ℝ
inst✝ : FTCFilter a l l'
hfm : StronglyMeasurableAtFilter f l' volume
hf : Tendsto f (l' ⊓ ae volume) (𝓝 c)
u v : ι → ℝ
hu : Tendsto u lt l
hv : Tendsto v lt l
⊢ (fun t => (∫ (x : ℝ) in u t..v t, f x) - (v t - u t) • c) =o[lt] (v - u)

Tactic:
simpa [integral_const] using measure_integral_sub_linear_isLittleO_of_tendsto_ae hfm hf hu hv

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem pi_ball [∀ i, MetricSpace (α i)] (x : ∀ i, α i) {r : ℝ} (hr : 0 < r) :
    Measure.pi μ (Metric.ball x r) = ∏ i, μ i (Metric.ball (x i) r)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 < r
⊢ (Measure.pi μ) (Metric.ball x r) = ∏ i : ι, (μ i) (Metric.ball (x i) r)

Tactic:
rw [ball_pi _ hr, pi_pi]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem head_range' (n : Nat) (h) : (range' s n).head h = s

Proof state:
s n : Nat
h : range' s n ≠ []
⊢ (range' s n).head h = s

Tactic:
repeat simp_all [head?_range', head_eq_iff_head?_eq_some]

Result:
no goals

Proof state:
s n : Nat
h : range' s n ≠ []
⊢ ¬n = 0

Tactic:
simp_all [head?_range', head_eq_iff_head?_eq_some]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
@[to_additive]
protected lemma mul_div_mul_left (h : IsUnit c) (a b : α) : c * a / (c * b) = a / b

Proof state:
α : Type u
inst✝ : DivisionCommMonoid α
c : α
h : IsUnit c
a b : α
⊢ c * a / (c * b) = a / b

Tactic:
rw [mul_comm c, mul_comm c, h.mul_div_mul_right]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_sub_zsmul (a b : α) (m : ℤ) : toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - m

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - m

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIcoDiv_add_zsmul, sub_eq_add_neg]

Result:
no goals