harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem uniformEquicontinuousOn_iInf_rng {u : κ → UniformSpace α'} {F : ι → β → α'}
    {S : Set β} : UniformEquicontinuousOn (uα := ⨅ k, u k) F S ↔
      ∀ k, UniformEquicontinuousOn (uα := u k) F S

Proof state:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
S : Set β
⊢ Tendsto (fun x => ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α')) ↔
    ∀ (k : κ), Tendsto (fun x => ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α'))

Tactic:
rw [UniformFun.iInf_eq, iInf_uniformity, tendsto_iInf]

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
S : Set β
⊢ UniformEquicontinuousOn F S ↔ ∀ (k : κ), UniformEquicontinuousOn F S

Tactic:
simp_rw [uniformEquicontinuousOn_iff_uniformContinuousOn (uα := _)]

Result:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
S : Set β
⊢ UniformContinuousOn (⇑ofFun ∘ swap F) S ↔ ∀ (k : κ), UniformContinuousOn (⇑ofFun ∘ swap F) S

Proof state:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
S : Set β
⊢ UniformContinuousOn (⇑ofFun ∘ swap F) S ↔ ∀ (k : κ), UniformContinuousOn (⇑ofFun ∘ swap F) S

Tactic:
unfold UniformContinuousOn

Result:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
S : Set β
⊢ Tendsto (fun x => ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α')) ↔
    ∀ (k : κ), Tendsto (fun x => ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α'))
-- Mathlib/Logic/Relation.lean
theorem tail' (hab : ReflTransGen r a b) (hbc : r b c) : TransGen r a c

Proof state:
case refl
α : Type u_1
r : α → α → Prop
a b c : α
hbc : r a c
⊢ TransGen r a c

Tactic:
exact single hbc

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
a b b✝ c✝ : α
a✝ : ReflTransGen r a b✝
hdb : r b✝ c✝
IH : ∀ {c : α}, r b✝ c → TransGen r a c
c : α
hbc : r c✝ c
⊢ TransGen r a c

Tactic:
exact tail (IH hdb) hbc

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : r b c
⊢ TransGen r a c

Tactic:
induction hab generalizing c with
| refl => exact single hbc
| tail _ hdb IH => exact tail (IH hdb) hbc

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem pred_update (P : ∀ ⦃a⦄, β a → Prop) (f : ∀ a, β a) (a' : α) (v : β a') (a : α) :
    P (update f a' v a) ↔ a = a' ∧ P v ∨ a ≠ a' ∧ P (f a)

Proof state:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
P : ⦃a : α⦄ → β a → Prop
f : (a : α) → β a
a' : α
v : β a'
a : α
⊢ P (update f a' v a) ↔ a = a' ∧ P v ∨ a ≠ a' ∧ P (f a)

Tactic:
rw [apply_update P, update_apply, ite_prop_iff_or]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem prod_le [Nontrivial α] {a b : FactorSet α} : a.prod ≤ b.prod ↔ a ≤ b

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
h : a.prod ≤ b.prod
⊢ a ≤ b

Tactic:
have : a.prod.factors ≤ b.prod.factors := factors_mono h

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
h : a.prod ≤ b.prod
this : a.prod.factors ≤ b.prod.factors
⊢ a ≤ b

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
⊢ a.prod ≤ b.prod ↔ a ≤ b

Tactic:
refine ⟨fun h ↦ ?_, prod_mono⟩

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
h : a.prod ≤ b.prod
⊢ a ≤ b

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
h : a.prod ≤ b.prod
this : a.prod.factors ≤ b.prod.factors
⊢ a ≤ b

Tactic:
rwa [prod_factors, prod_factors] at this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldl_reverse (l : Vector α n) (f : β → α → β) (b) :
    l.reverse.foldl f b = l.foldr (fun x y => f y x) b

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : β → α → β
b : β
⊢ foldl f b l.reverse = foldr (fun x y => f y x) b l

Tactic:
simp [foldl_eq_foldlM, foldr_eq_foldrM]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderiv_comp_sub (a : E) :
    fderiv 𝕜 (fun x ↦ f (x - a)) x = fderiv 𝕜 f (x - a)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x a : E
⊢ fderiv 𝕜 (fun x => f (x - a)) x = fderiv 𝕜 f (x - a)

Tactic:
simp [← fderivWithin_univ, fderivWithin_comp_sub]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem isCycle (h : IsThreeCycle σ) : IsCycle σ

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ σ.IsCycle

Tactic:
rw [← card_cycleType_eq_one, h.cycleType, card_singleton]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem not_dvd_of_natDegree_lt (hp : Monic p) (h0 : q ≠ 0) (hl : natDegree q < natDegree p) :
    ¬p ∣ q

Proof state:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
h0 : p * r ≠ 0
hl : (p * r).natDegree < p.natDegree
⊢ False

Tactic:
rw [hp.natDegree_mul' <| right_ne_zero_of_mul h0] at hl

Result:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
h0 : p * r ≠ 0
hl : p.natDegree + r.natDegree < p.natDegree
⊢ False

Proof state:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
h0 : p * r ≠ 0
hl : p.natDegree + r.natDegree < p.natDegree
⊢ False

Tactic:
exact hl.not_le (Nat.le_add_right _ _)

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
h0 : q ≠ 0
hl : q.natDegree < p.natDegree
⊢ ¬p ∣ q

Tactic:
rintro ⟨r, rfl⟩

Result:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
h0 : p * r ≠ 0
hl : (p * r).natDegree < p.natDegree
⊢ False
-- Mathlib/Algebra/Regular/Basic.lean
@[simp] lemma IsLeftRegular.mul_left_eq_zero_iff (hb : IsLeftRegular b) : b * a = 0 ↔ a = 0

Proof state:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
⊢ b * a = 0 ↔ a = 0

Tactic:
nth_rw 1 [← mul_zero b]

Result:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
⊢ b * a = b * 0 ↔ a = 0

Proof state:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
⊢ b * a = b * 0 ↔ a = 0

Tactic:
exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
ha : a = 0
⊢ b * a = b * 0

Tactic:
rw [ha]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem _root_.Function.update_exp {ι : Type*} {𝔸 : ι → Type*} [Finite ι] [DecidableEq ι]
    [∀ i, NormedRing (𝔸 i)] [∀ i, NormedAlgebra 𝕂 (𝔸 i)] [∀ i, CompleteSpace (𝔸 i)] (x : ∀ i, 𝔸 i)
    (j : ι) (xj : 𝔸 j) :
    Function.update (exp 𝕂 x) j (exp 𝕂 xj) = exp 𝕂 (Function.update x j xj)

Proof state:
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
ι : Type u_4
𝔸 : ι → Type u_5
inst✝⁴ : Finite ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → NormedRing (𝔸 i)
inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)
inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
⊢ Function.update (exp 𝕂 x) j (exp 𝕂 xj) = exp 𝕂 (Function.update x j xj)

Tactic:
ext i

Result:
case h
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
ι : Type u_4
𝔸 : ι → Type u_5
inst✝⁴ : Finite ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → NormedRing (𝔸 i)
inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)
inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
i : ι
⊢ Function.update (exp 𝕂 x) j (exp 𝕂 xj) i = exp 𝕂 (Function.update x j xj) i

Proof state:
case h
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
ι : Type u_4
𝔸 : ι → Type u_5
inst✝⁴ : Finite ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → NormedRing (𝔸 i)
inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)
inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
i : ι
⊢ Function.update (exp 𝕂 x) j (exp 𝕂 xj) i = exp 𝕂 (Function.update x j xj) i

Tactic:
simp_rw [Pi.exp_def]

Result:
case h
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
ι : Type u_4
𝔸 : ι → Type u_5
inst✝⁴ : Finite ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → NormedRing (𝔸 i)
inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)
inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
i : ι
⊢ Function.update (fun i => exp 𝕂 (x i)) j (exp 𝕂 xj) i = exp 𝕂 (Function.update x j xj i)

Proof state:
case h
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
ι : Type u_4
𝔸 : ι → Type u_5
inst✝⁴ : Finite ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → NormedRing (𝔸 i)
inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)
inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
i : ι
⊢ Function.update (fun i => exp 𝕂 (x i)) j (exp 𝕂 xj) i = exp 𝕂 (Function.update x j xj i)

Tactic:
exact (Function.apply_update (fun i => exp 𝕂) x j xj i).symm

Result:
no goals
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem isEquivalent_zero_iff_eventually_zero : u ~[l] 0 ↔ u =ᶠ[l] 0

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ u ~[l] 0 ↔ u =ᶠ[l] 0

Tactic:
rw [IsEquivalent, sub_zero]

Result:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ u =o[l] 0 ↔ u =ᶠ[l] 0

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ u =o[l] 0 ↔ u =ᶠ[l] 0

Tactic:
exact isLittleO_zero_right_iff

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
lemma neg_mulVec_neg [Fintype n] (v : n → α) (A : Matrix m n α) : (-A) *ᵥ (-v) = A *ᵥ v

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
⊢ -A *ᵥ -v = A *ᵥ v

Tactic:
rw [mulVec_neg, neg_mulVec, neg_neg]

Result:
no goals
-- Mathlib/Data/List/ToFinsupp.lean
theorem toFinsupp_eq_sum_mapIdx_single {R : Type*} [AddMonoid R] (l : List R)
    [DecidablePred (getD l · 0 ≠ 0)] :
    toFinsupp l = (l.mapIdx fun n r => Finsupp.single n r).sum

Proof state:
R : Type u_2
inst✝¹ : AddMonoid R
l : List R
inst✝ : DecidablePred fun x => l.getD x 0 ≠ 0
⊢ l.toFinsupp = (mapIdx (fun n r => Finsupp.single n r) l).sum

Tactic:
revert l

Result:
R : Type u_2
inst✝ : AddMonoid R
⊢ ∀ (l : List R) [inst : DecidablePred fun x => l.getD x 0 ≠ 0],
    l.toFinsupp = (mapIdx (fun n r => Finsupp.single n r) l).sum

Proof state:
case nil
R : Type u_2
inst✝ : AddMonoid R
⊢ ∀ [inst : DecidablePred fun x => [].getD x 0 ≠ 0], [].toFinsupp = (mapIdx (fun n r => Finsupp.single n r) []).sum

Tactic:
exact toFinsupp_nil

Result:
no goals

Proof state:
case append_singleton
R : Type u_2
inst✝ : AddMonoid R
x : List R
xs : R
ih : ∀ [inst : DecidablePred fun x_1 => x.getD x_1 0 ≠ 0], x.toFinsupp = (mapIdx (fun n r => Finsupp.single n r) x).sum
⊢ ∀ [inst : DecidablePred fun x_1 => (x ++ [xs]).getD x_1 0 ≠ 0],
    (x ++ [xs]).toFinsupp = (mapIdx (fun n r => Finsupp.single n r) (x ++ [xs])).sum

Tactic:
simp [toFinsupp_concat_eq_toFinsupp_add_single, ih]

Result:
no goals

Proof state:
case append_singleton
R : Type u_2
inst✝ : AddMonoid R
x : List R
xs : R
ih : ∀ [inst : DecidablePred fun x_1 => x.getD x_1 0 ≠ 0], x.toFinsupp = (mapIdx (fun n r => Finsupp.single n r) x).sum
⊢ ∀ [inst : DecidablePred fun x_1 => (x ++ [xs]).getD x_1 0 ≠ 0],
    (x ++ [xs]).toFinsupp = (mapIdx (fun n r => Finsupp.single n r) (x ++ [xs])).sum

Tactic:
classical simp [toFinsupp_concat_eq_toFinsupp_add_single, ih]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : AddMonoid R
l : List R
⊢ ∀ [inst : DecidablePred fun x => l.getD x 0 ≠ 0], l.toFinsupp = (mapIdx (fun n r => Finsupp.single n r) l).sum

Tactic:
induction l using List.reverseRecOn with
| nil => exact toFinsupp_nil
| append_singleton x xs ih =>
  classical simp [toFinsupp_concat_eq_toFinsupp_add_single, ih]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : AddMonoid R
⊢ ∀ (l : List R) [inst : DecidablePred fun x => l.getD x 0 ≠ 0],
    l.toFinsupp = (mapIdx (fun n r => Finsupp.single n r) l).sum

Tactic:
intro l

Result:
R : Type u_2
inst✝ : AddMonoid R
l : List R
⊢ ∀ [inst : DecidablePred fun x => l.getD x 0 ≠ 0], l.toFinsupp = (mapIdx (fun n r => Finsupp.single n r) l).sum
-- Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean
theorem foldr_prod_map_ι (l : List M) (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) :
    foldr Q f hf n (l.map <| ι Q).prod = List.foldr (fun m n => f m n) n l

Proof state:
case nil
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldr Q f hf) n) (List.map ⇑(ι Q) []).prod = List.foldr (fun m n => (f m) n) n []

Tactic:
rw [List.map_nil, List.prod_nil, List.foldr_nil, foldr_one]

Result:
no goals

Proof state:
case cons
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
hd : M
tl : List M
ih : ((foldr Q f hf) n) (List.map (⇑(ι Q)) tl).prod = List.foldr (fun m n => (f m) n) n tl
⊢ ((foldr Q f hf) n) (List.map (⇑(ι Q)) (hd :: tl)).prod = List.foldr (fun m n => (f m) n) n (hd :: tl)

Tactic:
rw [List.map_cons, List.prod_cons, List.foldr_cons, foldr_mul, foldr_ι, ih]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
l : List M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldr Q f hf) n) (List.map (⇑(ι Q)) l).prod = List.foldr (fun m n => (f m) n) n l

Tactic:
induction l with
| nil => rw [List.map_nil, List.prod_nil, List.foldr_nil, foldr_one]
| cons hd tl ih => rw [List.map_cons, List.prod_cons, List.foldr_cons, foldr_mul, foldr_ι, ih]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem eq_of_testBit_eq {x y : Nat} (pred : ∀i, testBit x i = testBit y i) : x = y

Proof state:
x y : Nat
pred : ∀ (i : Nat), x.testBit i = y.testBit i
h : ¬x = y
i : Nat
eq : x.testBit i ≠ y.testBit i
⊢ x = y

Tactic:
have p := pred i

Result:
x y : Nat
pred : ∀ (i : Nat), x.testBit i = y.testBit i
h : ¬x = y
i : Nat
eq : x.testBit i ≠ y.testBit i
p : x.testBit i = y.testBit i
⊢ x = y

Proof state:
x y : Nat
pred : ∀ (i : Nat), x.testBit i = y.testBit i
h : ¬x = y
⊢ x = y

Tactic:
let ⟨i,eq⟩ := ne_implies_bit_diff h

Result:
x y : Nat
pred : ∀ (i : Nat), x.testBit i = y.testBit i
h : ¬x = y
i : Nat
eq : x.testBit i ≠ y.testBit i
⊢ x = y

Proof state:
x y : Nat
pred : ∀ (i : Nat), x.testBit i = y.testBit i
h : x = y
⊢ x = y

Tactic:
exact h

Result:
no goals

Proof state:
x y : Nat
pred : ∀ (i : Nat), x.testBit i = y.testBit i
⊢ x = y

Tactic:
if h : x = y then
  exact h
else
  let ⟨i,eq⟩ := ne_implies_bit_diff h
  have p := pred i
  contradiction

Result:
no goals

Proof state:
x y : Nat
pred : ∀ (i : Nat), x.testBit i = y.testBit i
h : ¬x = y
i : Nat
eq : x.testBit i ≠ y.testBit i
p : x.testBit i = y.testBit i
⊢ x = y

Tactic:
contradiction

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_lineMap_iff [NoZeroSMulDivisors R V] {x y : P} {r : R} :
    Wbtw R x (lineMap x y r) y ↔ x = y ∨ r ∈ Set.Icc (0 : R) 1

Proof state:
case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : ¬x = y
⊢ Wbtw R x ((lineMap x y) r) y ↔ x = y ∨ r ∈ Set.Icc 0 1

Tactic:
rw [or_iff_right hxy, Wbtw, affineSegment, (lineMap_injective R hxy).mem_set_image]

Result:
no goals

Proof state:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : x = y
⊢ Wbtw R y y y ↔ y = y ∨ r ∈ Set.Icc 0 1

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
⊢ Wbtw R x ((lineMap x y) r) y ↔ x = y ∨ r ∈ Set.Icc 0 1

Tactic:
by_cases hxy : x = y

Result:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : x = y
⊢ Wbtw R x ((lineMap x y) r) y ↔ x = y ∨ r ∈ Set.Icc 0 1

case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : ¬x = y
⊢ Wbtw R x ((lineMap x y) r) y ↔ x = y ∨ r ∈ Set.Icc 0 1

Proof state:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : x = y
⊢ Wbtw R x ((lineMap x y) r) y ↔ x = y ∨ r ∈ Set.Icc 0 1

Tactic:
rw [hxy, lineMap_same_apply]

Result:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y : P
r : R
hxy : x = y
⊢ Wbtw R y y y ↔ y = y ∨ r ∈ Set.Icc 0 1
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem coe_preimage_infty : ((↑) : X → OnePoint X) ⁻¹' {∞} = ∅

Proof state:
case h
X : Type u_1
x✝ : X
⊢ x✝ ∈ some ⁻¹' {∞} ↔ x✝ ∈ ∅

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
⊢ some ⁻¹' {∞} = ∅

Tactic:
ext

Result:
case h
X : Type u_1
x✝ : X
⊢ x✝ ∈ some ⁻¹' {∞} ↔ x✝ ∈ ∅
-- Mathlib/Algebra/Ring/Divisibility/Lemmas.lean
lemma dvd_smul_of_dvd {M : Type*} [SMul M R] [Semigroup R] [SMulCommClass M R R] {x y : R}
    (m : M) (h : x ∣ y) : x ∣ m • y :=
  let ⟨k, hk⟩ := h; ⟨m • k, by rw [mul_smul_comm, ← hk]⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : SMul M R
inst✝¹ : Semigroup R
inst✝ : SMulCommClass M R R
x y : R
m : M
h : x ∣ y
k : R
hk : y = x * k
⊢ m • y = x * m • k

Tactic:
rw [mul_smul_comm, ← hk]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem derivativeFun_smul (r : R) (f : R⟦X⟧) : derivativeFun (r • f) = r • derivativeFun f

Proof state:
R : Type u_1
inst✝ : CommSemiring R
r : R
f : R⟦X⟧
⊢ (r • f).derivativeFun = r • f.derivativeFun

Tactic:
rw [smul_eq_C_mul, smul_eq_C_mul, derivativeFun_mul, derivativeFun_C, smul_zero, add_zero,
  smul_eq_mul]

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
lemma preNormEDS_even_ofNat (m : ℕ) : preNormEDS b c d (2 * (m + 3)) =
    preNormEDS b c d (m + 2) ^ 2 * preNormEDS b c d (m + 3) * preNormEDS b c d (m + 5) -
      preNormEDS b c d (m + 1) * preNormEDS b c d (m + 3) * preNormEDS b c d (m + 4) ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * (↑m + 3)) =
    preNormEDS b c d (↑m + 2) ^ 2 * preNormEDS b c d (↑m + 3) * preNormEDS b c d (↑m + 5) -
      preNormEDS b c d (↑m + 1) * preNormEDS b c d (↑m + 3) * preNormEDS b c d (↑m + 4) ^ 2

Tactic:
repeat erw [preNormEDS_ofNat]

Result:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS' b c d (2 * (m + 3)) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS' b c d (2 * (m + 3)) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS b c d (↑m + 4) ^ 2

Tactic:
erw [preNormEDS_ofNat]

Result:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS' b c d (2 * (m + 3)) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS' b c d (2 * (m + 3)) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2

Tactic:
exact preNormEDS'_even ..

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem mem_dite_none_left {x : α} [Decidable p] {l : ¬ p → Option α} :
    (x ∈ if h : p then none else l h) ↔ ∃ h : ¬ p, x ∈ l h

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : ¬p → Option α
⊢ (x ∈ if h : p then none else l h) ↔ ∃ h, x ∈ l h

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem map_volume_mul_left {a : ℝ} (h : a ≠ 0) :
    Measure.map (a * ·) volume = ENNReal.ofReal |a⁻¹| • volume

Proof state:
a : ℝ
h : a ≠ 0
⊢ Measure.map (fun x => a * x) volume = ofReal |a⁻¹| • volume

Tactic:
conv_rhs =>
  rw [← Real.smul_map_volume_mul_left h, smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ←
    abs_mul, inv_mul_cancel₀ h, abs_one, ENNReal.ofReal_one, one_smul]

Result:
no goals
-- Mathlib/Topology/List.lean
theorem tendsto_insertIdx {n : ℕ} {i : Fin (n + 1)} {a : α} :
    ∀ {l : List.Vector α n},
      Tendsto (fun p : α × List.Vector α n => Vector.insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l)
        (𝓝 (Vector.insertIdx a i l))
  | ⟨l, hl⟩ => by
    rw [Vector.insertIdx, tendsto_subtype_rng]
    simp only [Vector.insertIdx_val]
    exact List.tendsto_insertIdx tendsto_fst (Tendsto.comp continuousAt_subtype_val tendsto_snd : _)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun x => insertIdx (↑i) x.1 ↑x.2) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 (insertIdx (↑i) a l))

Tactic:
exact List.tendsto_insertIdx tendsto_fst (Tendsto.comp continuousAt_subtype_val tendsto_snd : _)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun p => Vector.insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 (Vector.insertIdx a i ⟨l, hl⟩))

Tactic:
rw [Vector.insertIdx, tendsto_subtype_rng]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun x => ↑(Vector.insertIdx x.1 i x.2)) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 ↑⟨insertIdx (↑i) a ↑⟨l, hl⟩, ⋯⟩)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun x => ↑(Vector.insertIdx x.1 i x.2)) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 ↑⟨insertIdx (↑i) a ↑⟨l, hl⟩, ⋯⟩)

Tactic:
simp only [Vector.insertIdx_val]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun x => insertIdx (↑i) x.1 ↑x.2) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 (insertIdx (↑i) a l))
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive mod_addOrderOf_zsmul]
lemma zpow_mod_orderOf (x : G) (z : ℤ) : x ^ (z % (orderOf x : ℤ)) = x ^ z :=
  calc
    x ^ (z % (orderOf x : ℤ)) = x ^ (z % orderOf x + orderOf x * (z / orderOf x) : ℤ)

Proof state:
G : Type u_1
inst✝ : Group G
x : G
z : ℤ
⊢ x ^ (z % ↑(orderOf x)) = x ^ (z % ↑(orderOf x) + ↑(orderOf x) * (z / ↑(orderOf x)))

Tactic:
simp [zpow_add, zpow_mul, pow_orderOf_eq_one]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
x : G
z : ℤ
⊢ x ^ (z % ↑(orderOf x) + ↑(orderOf x) * (z / ↑(orderOf x))) = x ^ z

Tactic:
rw [Int.emod_add_ediv]

Result:
no goals