harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem findSomeRevM?_toArray [Monad m] (f : α → m (Option β)) (v : Vector α n) :
    v.toArray.findSomeRevM? f = v.findSomeRevM? f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝ : Monad m
f : α → m (Option β)
v : Vector α n
⊢ Array.findSomeRevM? f v.toArray = findSomeRevM? f v

Tactic:
rcases v with ⟨v, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → m (Option β)
v : Array α
⊢ Array.findSomeRevM? f { toArray := v, size_toArray := ⋯ }.toArray =
    findSomeRevM? f { toArray := v, size_toArray := ⋯ }

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → m (Option β)
v : Array α
⊢ Array.findSomeRevM? f { toArray := v, size_toArray := ⋯ }.toArray =
    findSomeRevM? f { toArray := v, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_sub_right_of_add_lt {a b c : Int} (h : a + b < c) : a < c - b

Proof state:
a b c : Int
h✝ : a + b < c
h : a + b + -b < c + -b
⊢ a < c - b

Tactic:
rwa [Int.add_neg_cancel_right] at h

Result:
no goals

Proof state:
a b c : Int
h : a + b < c
⊢ a < c - b

Tactic:
have h := Int.add_lt_add_right h (-b)

Result:
a b c : Int
h✝ : a + b < c
h : a + b + -b < c + -b
⊢ a < c - b
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem ite_else_self {p q : Prop} [h : Decidable p] : (if p then q else p) ↔ (p ∧ q)

Proof state:
case isTrue
p q : Prop
h✝ : p
⊢ (if p then q else p) ↔ p ∧ q

Tactic:
rename_i g

Result:
case isTrue
p q : Prop
g : p
⊢ (if p then q else p) ↔ p ∧ q

Proof state:
p q : Prop
h : Decidable p
⊢ (if p then q else p) ↔ p ∧ q

Tactic:
cases h <;> (rename_i g; simp [g])

Result:
no goals

Proof state:
case isTrue
p q : Prop
g : p
⊢ (if p then q else p) ↔ p ∧ q

Tactic:
simp [g]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem torsion_smul_mem_of_mem (hx : x ∈ fundamentalCone K) {ζ : (𝓞 K)ˣ} (hζ : ζ ∈ torsion K) :
    ζ • x ∈ fundamentalCone K

Proof state:
case left
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ logMap x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
exact hx.1

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ζ • x ∈ fundamentalCone K

Tactic:
constructor

Result:
case left
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ζ • x ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

case right
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ζ • x ∉ {x | mixedEmbedding.norm x = 0}

Proof state:
case right
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ¬mixedEmbedding.norm x = 0

Tactic:
exact hx.2

Result:
no goals

Proof state:
case left
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ζ • x ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
rw [Set.mem_preimage, logMap_torsion_smul _ hζ]

Result:
case left
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ logMap x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Proof state:
case right
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ζ • x ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
rw [Set.mem_setOf_eq, unitSMul_smul, map_mul, norm_unit, one_mul]

Result:
case right
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ¬mixedEmbedding.norm x = 0
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem _root_.Nat.sum_divisors {n : ℕ} (hn : n ≠ 0) :
    ∑ d ∈ n.divisors, d = ∏ p ∈ n.primeFactors, ∑ k ∈ .range (n.factorization p + 1), p ^ k

Proof state:
n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k => (σ 1) (p ^ k)) = ∏ p ∈ n.primeFactors, ∑ k ∈ range (n.factorization p + 1), p ^ k

Tactic:
exact Finset.prod_congr n.support_factorization fun _ h =>
  sigma_one_apply_prime_pow <| Nat.prime_of_mem_primeFactors h

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
⊢ ∑ d ∈ n.divisors, d = ∏ p ∈ n.primeFactors, ∑ k ∈ range (n.factorization p + 1), p ^ k

Tactic:
rw [← sigma_one_apply, isMultiplicative_sigma.multiplicative_factorization _ hn]

Result:
n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k => (σ 1) (p ^ k)) = ∏ p ∈ n.primeFactors, ∑ k ∈ range (n.factorization p + 1), p ^ k
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma disjointSigma_isBase_iff {h B} :
    (Matroid.disjointSigma M h).IsBase B ↔
      (∀ i, (M i).IsBase (B ∩ (M i).E)) ∧ B ⊆ ⋃ i, (M i).E

Proof state:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i => (M i).E)
B : Set α
⊢ (Matroid.disjointSigma M h).IsBase B ↔ (∀ (i : ι), (M i).IsBase (B ∩ (M i).E)) ∧ B ⊆ ⋃ i, (M i).E

Tactic:
simp [Matroid.disjointSigma, (Function.Embedding.sigmaSet_preimage h)]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma isComplex_smul_iff : IsComplex (σ • w) ↔ IsComplex w

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : K ≃ₐ[k] K
w : InfinitePlace K
⊢ (σ • w).IsComplex ↔ w.IsComplex

Tactic:
rw [← not_isReal_iff_isComplex, ← not_isReal_iff_isComplex, isReal_smul_iff]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem Ideal.span_singleton_nonZeroDivisors {R : Type*} [CommSemiring R] [NoZeroDivisors R]
    {r : R} : span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰

Proof state:
case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Subsingleton R
⊢ span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰

Tactic:
exact ⟨fun _ _ _ ↦ Subsingleton.eq_zero _, fun _ _ _ ↦ Subsingleton.eq_zero _⟩

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Nontrivial R
⊢ span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰

Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero, mem_nonZeroDivisors_iff_ne_zero, ne_eq, zero_eq_bot,
  span_singleton_eq_bot]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
⊢ span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Subsingleton R
⊢ span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰

case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Nontrivial R
⊢ span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp) subConst_mul_card]
lemma divConst_mul_card (A B : Finset G) : δₘ[A, B] * #A = #(A / B)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ δₘ[A, B] * ↑(#A) = ↑(#(A / B))

Tactic:
obtain rfl | hA := A.eq_empty_or_nonempty

Result:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
B : Finset G
⊢ δₘ[∅, B] * ↑(#∅) = ↑(#(∅ / B))

case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
⊢ δₘ[A, B] * ↑(#A) = ↑(#(A / B))

Proof state:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
⊢ δₘ[A, B] * ↑(#A) = ↑(#(A / B))

Tactic:
exact div_mul_cancel₀ _ (by positivity)

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
⊢ ↑(#A) ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
B : Finset G
⊢ δₘ[∅, B] * ↑(#∅) = ↑(#(∅ / B))

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem singleton_mem_nhdsWithin_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X}
    (hx : x ∈ s) : {x} ∈ 𝓝[s] x

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
this : {⟨x, hx⟩} ∈ 𝓝 ⟨x, hx⟩
⊢ {x} ∈ 𝓝[s] x

Tactic:
simpa only [nhdsWithin_eq_map_subtype_coe hx, image_singleton] using
  @image_mem_map _ _ _ ((↑) : s → X) _ this

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
⊢ {x} ∈ 𝓝[s] x

Tactic:
have : ({⟨x, hx⟩} : Set s) ∈ 𝓝 (⟨x, hx⟩ : s) := by simp [nhds_discrete]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
this : {⟨x, hx⟩} ∈ 𝓝 ⟨x, hx⟩
⊢ {x} ∈ 𝓝[s] x

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
⊢ {⟨x, hx⟩} ∈ 𝓝 ⟨x, hx⟩

Tactic:
simp [nhds_discrete]

Result:
no goals
-- Mathlib/AlgebraicTopology/ExtraDegeneracy.lean
theorem ExtraDegeneracy.s_comp_base (n : ℕ) :
    ExtraDegeneracy.s f S n ≫ WidePullback.base _ = WidePullback.base _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
⊢ (s f S n ≫ WidePullback.base fun x => f.hom) = WidePullback.base fun x => f.hom

Tactic:
apply WidePullback.lift_base

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
/-- Any game without left or right moves is identical to 0. -/
lemma identical_zero (x : PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] : x ≡ 0 :=
  x.identical_zero_iff.mpr ⟨by infer_instance, by infer_instance⟩

Proof state:
x : PGame
inst✝¹ : IsEmpty x.LeftMoves
inst✝ : IsEmpty x.RightMoves
⊢ IsEmpty x.LeftMoves

Tactic:
infer_instance

Result:
no goals

Proof state:
x : PGame
inst✝¹ : IsEmpty x.LeftMoves
inst✝ : IsEmpty x.RightMoves
⊢ IsEmpty x.RightMoves

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatMap_eq_foldl (f : α → List β) (l : List α) :
    l.flatMap f = l.foldl (fun acc a => acc ++ f a) []

Proof state:
α : Type u_1
β : Type u_2
f : α → List β
l : List α
this : ∀ (l' : List β), l' ++ flatMap f l = foldl (fun acc a => acc ++ f a) l' l
⊢ flatMap f l = foldl (fun acc a => acc ++ f a) [] l

Tactic:
simpa using this []

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → List β
l : List α
⊢ ∀ (l' : List β), l' ++ flatMap f l = foldl (fun acc a => acc ++ f a) l' l

Tactic:
intro l'

Result:
α : Type u_1
β : Type u_2
f : α → List β
l : List α
l' : List β
⊢ l' ++ flatMap f l = foldl (fun acc a => acc ++ f a) l' l

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → List β
l' : List β
⊢ l' ++ flatMap f [] = foldl (fun acc a => acc ++ f a) l' []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → List β
head✝ : α
tail✝ : List α
ih : ∀ (l' : List β), l' ++ flatMap f tail✝ = foldl (fun acc a => acc ++ f a) l' tail✝
l' : List β
⊢ l' ++ flatMap f (head✝ :: tail✝) = foldl (fun acc a => acc ++ f a) l' (head✝ :: tail✝)

Tactic:
rw [flatMap_cons, ← append_assoc, ih, foldl_cons]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → List β
l : List α
l' : List β
⊢ l' ++ flatMap f l = foldl (fun acc a => acc ++ f a) l' l

Tactic:
induction l generalizing l'

Result:
case nil
α : Type u_1
β : Type u_2
f : α → List β
l' : List β
⊢ l' ++ flatMap f [] = foldl (fun acc a => acc ++ f a) l' []

case cons
α : Type u_1
β : Type u_2
f : α → List β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l' : List β), l' ++ flatMap f tail✝ = foldl (fun acc a => acc ++ f a) l' tail✝
l' : List β
⊢ l' ++ flatMap f (head✝ :: tail✝) = foldl (fun acc a => acc ++ f a) l' (head✝ :: tail✝)

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → List β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l' : List β), l' ++ flatMap f tail✝ = foldl (fun acc a => acc ++ f a) l' tail✝
l' : List β
⊢ l' ++ flatMap f (head✝ :: tail✝) = foldl (fun acc a => acc ++ f a) l' (head✝ :: tail✝)

Tactic:
next ih => rw [flatMap_cons, ← append_assoc, ih, foldl_cons]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → List β
l : List α
⊢ flatMap f l = foldl (fun acc a => acc ++ f a) [] l

Tactic:
suffices ∀ l', l' ++ l.flatMap f = l.foldl (fun acc a => acc ++ f a) l' by simpa using this []

Result:
α : Type u_1
β : Type u_2
f : α → List β
l : List α
⊢ ∀ (l' : List β), l' ++ flatMap f l = foldl (fun acc a => acc ++ f a) l' l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_rotateRight {x : BitVec w} {r i : Nat} :
    (x.rotateRight r).getLsbD i =
      cond (i < w - (r % w))
      (x.getLsbD ((r % w) + i))
      (decide (i < w) && x.getLsbD (i - (w - (r % w))))

Proof state:
case succ
r i n✝ : Nat
x : BitVec (n✝ + 1)
⊢ (x.rotateRight r).getLsbD i =
    bif decide (i < n✝ + 1 - r % (n✝ + 1)) then x.getLsbD (r % (n✝ + 1) + i)
    else decide (i < n✝ + 1) && x.getLsbD (i - (n✝ + 1 - r % (n✝ + 1)))

Tactic:
rw [← rotateRight_mod_eq_rotateRight, getLsbD_rotateRight_of_lt (Nat.mod_lt _ (by omega))]

Result:
no goals

Proof state:
r i n✝ : Nat
x : BitVec (n✝ + 1)
⊢ n✝ + 1 > 0

Tactic:
omega

Result:
no goals

Proof state:
case zero
r i : Nat
x : BitVec 0
⊢ (x.rotateRight r).getLsbD i =
    bif decide (i < 0 - r % 0) then x.getLsbD (r % 0 + i) else decide (i < 0) && x.getLsbD (i - (0 - r % 0))

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
⊢ (x.rotateRight r).getLsbD i =
    bif decide (i < w - r % w) then x.getLsbD (r % w + i) else decide (i < w) && x.getLsbD (i - (w - r % w))

Tactic:
rcases w with ⟨rfl, w⟩

Result:
case zero
r i : Nat
x : BitVec 0
⊢ (x.rotateRight r).getLsbD i =
    bif decide (i < 0 - r % 0) then x.getLsbD (r % 0 + i) else decide (i < 0) && x.getLsbD (i - (0 - r % 0))

case succ
r i n✝ : Nat
x : BitVec (n✝ + 1)
⊢ (x.rotateRight r).getLsbD i =
    bif decide (i < n✝ + 1 - r % (n✝ + 1)) then x.getLsbD (r % (n✝ + 1) + i)
    else decide (i < n✝ + 1) && x.getLsbD (i - (n✝ + 1 - r % (n✝ + 1)))
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem lift_comp_kernelIsoOfEq_hom {Z} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g)
    (e : Z ⟶ X) (he) :
    kernel.lift _ e he ≫ (kernelIsoOfEq h).hom = kernel.lift _ e (by simp [← h, he])

Proof state:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasKernel f
e : Z ⟶ X
he : e ≫ f = 0
inst✝ : HasKernel f
⊢ kernel.lift f e he ≫ (kernelIsoOfEq ⋯).hom = kernel.lift f e ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
Z : C
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
e : Z ⟶ X
he : e ≫ f = 0
⊢ e ≫ g = 0

Tactic:
simp [← h, he]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
e : Z ⟶ X
he : e ≫ f = 0
⊢ kernel.lift f e he ≫ (kernelIsoOfEq h).hom = kernel.lift g e ⋯

Tactic:
cases h

Result:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasKernel f
e : Z ⟶ X
he : e ≫ f = 0
inst✝ : HasKernel f
⊢ kernel.lift f e he ≫ (kernelIsoOfEq ⋯).hom = kernel.lift f e ⋯
-- Mathlib/Order/Filter/Tendsto.lean
theorem map_inf_principal_preimage {f : α → β} {s : Set β} {l : Filter α} :
    map f (l ⊓ 𝓟 (f ⁻¹' s)) = map f l ⊓ 𝓟 s :=
  Filter.ext fun t => by simp only [mem_map', mem_inf_principal, mem_setOf_eq, mem_preimage]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
l : Filter α
t : Set β
⊢ t ∈ map f (l ⊓ 𝓟 (f ⁻¹' s)) ↔ t ∈ map f l ⊓ 𝓟 s

Tactic:
simp only [mem_map', mem_inf_principal, mem_setOf_eq, mem_preimage]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem units_semiconj_of_translationNumber_eq {f₁ f₂ : CircleDeg1Liftˣ} (h : τ f₁ = τ f₂) :
    ∃ F : CircleDeg1Lift, Semiconj F f₁ f₂ :=
  have : ∀ n : Multiplicative ℤ,
      τ ((Units.coeHom _).comp (zpowersHom _ f₁) n) =
        τ ((Units.coeHom _).comp (zpowersHom _ f₂) n) := fun n ↦ by
    simp [h]
  (semiconj_of_group_action_of_forall_translationNumber_eq _ _ this).imp fun F hF => by
    simpa using hF (Multiplicative.ofAdd 1)

Proof state:
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
this :
  ∀ (n : Multiplicative ℤ),
    τ (((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₁)) n) =
      τ (((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₂)) n)
F : CircleDeg1Lift
hF :
  ∀ (g : Multiplicative ℤ),
    Semiconj ⇑F ⇑(((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₁)) g)
      ⇑(((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₂)) g)
⊢ Semiconj ⇑F ⇑↑f₁ ⇑↑f₂

Tactic:
simpa using hF (Multiplicative.ofAdd 1)

Result:
no goals

Proof state:
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
n : Multiplicative ℤ
⊢ τ (((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₁)) n) =
    τ (((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₂)) n)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean
@[to_additive]
lemma csSup_div (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
    sSup (s / t) = sSup s / sInf t

Proof state:
M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddBelow t
⊢ sSup (s / t) = sSup s / sInf t

Tactic:
rw [div_eq_mul_inv, csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, csSup_inv ht₀ ht₁, div_eq_mul_inv]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Real.lean
theorem equivalent_one_neg_one_weighted_sum_squared {M : Type*} [AddCommGroup M] [Module ℝ M]
    [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) (hQ : (associated (R := ℝ) Q).SeparatingLeft) :
    ∃ w : Fin (Module.finrank ℝ M) → ℝ,
      (∀ i, w i = -1 ∨ w i = 1) ∧ Equivalent Q (weightedSumSquares ℝ w) :=
  let ⟨w, hw₀, hw⟩ := Q.equivalent_sign_ne_zero_weighted_sum_squared hQ
  ⟨(w ·), fun i ↦ by cases hi : w i <;> simp_all, hw⟩

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module ℝ M
inst✝ : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
hQ : LinearMap.SeparatingLeft (associated Q)
w : Fin (Module.finrank ℝ M) → SignType
hw₀ : ∀ (i : Fin (Module.finrank ℝ M)), w i ≠ 0
hw : Equivalent Q (weightedSumSquares ℝ fun i => ↑(w i))
i : Fin (Module.finrank ℝ M)
⊢ (fun x => ↑(w x)) i = -1 ∨ (fun x => ↑(w x)) i = 1

Tactic:
cases hi : w i <;> simp_all

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem IsSt.infinitesimal_sub {x : ℝ*} {r : ℝ} (hxr : IsSt x r) : Infinitesimal (x - ↑r)

Proof state:
x : ℝ*
r : ℝ
hxr : x.IsSt r
⊢ (x - ↑r).Infinitesimal

Tactic:
simpa only [sub_self] using hxr.sub (isSt_refl_real r)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
theorem hasStrictDerivAt_log (hx : x ≠ 0) : HasStrictDerivAt log x⁻¹ x

Proof state:
x : ℝ
hx : x ≠ 0
⊢ HasStrictDerivAt log x⁻¹ x

Tactic:
rcases hx.lt_or_lt with hx | hx

Result:
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt log x⁻¹ x

case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt log x⁻¹ x

Proof state:
case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt log x⁻¹ x

Tactic:
exact hasStrictDerivAt_log_of_pos hx

Result:
no goals

Proof state:
case h.e'_8.h
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
y : ℝ
⊢ log y = (log ∘ Neg.neg) y

Tactic:
exact (log_neg_eq_log y).symm

Result:
no goals

Proof state:
case h.e'_8
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ log = log ∘ Neg.neg

Tactic:
ext y

Result:
case h.e'_8.h
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
y : ℝ
⊢ log y = (log ∘ Neg.neg) y

Proof state:
case h.e'_9
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ x⁻¹ = (-x)⁻¹ * -1

Tactic:
field_simp [hx.ne]

Result:
no goals

Proof state:
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt log x⁻¹ x

Tactic:
convert (hasStrictDerivAt_log_of_pos (neg_pos.mpr hx)).comp x (hasStrictDerivAt_neg x) using 1

Result:
case h.e'_8
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ log = log ∘ Neg.neg

case h.e'_9
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ x⁻¹ = (-x)⁻¹ * -1
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.of_add_mul_right_left (h : IsCoprime (x + z * y) y) : IsCoprime x y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + z * y) y
⊢ IsCoprime x y

Tactic:
rw [mul_comm] at h

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
⊢ IsCoprime x y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
⊢ IsCoprime x y

Tactic:
exact h.of_add_mul_left_left

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem preimage_mul_right_one : preimage 1 (· * b) (mul_left_injective _).injOn = {b⁻¹}

Proof state:
α : Type u_2
inst✝ : Group α
b : α
⊢ preimage 1 (fun x => x * b) ⋯ = {b⁻¹}

Tactic:
rw [← image_mul_right', image_one, one_mul]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Group α
b : α
⊢ preimage 1 (fun x => x * b) ⋯ = {b⁻¹}

Tactic:
classical rw [← image_mul_right', image_one, one_mul]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nadd_le_nadd_left (h : b ≤ c) (a) : a ♯ b ≤ a ♯ c

Proof state:
case inr
b a : Ordinal.{u}
h : b ≤ b
⊢ a ♯ b ≤ a ♯ b

Tactic:
exact le_rfl

Result:
no goals

Proof state:
b c : Ordinal.{u}
h : b ≤ c
a : Ordinal.{u}
⊢ a ♯ b ≤ a ♯ c

Tactic:
rcases lt_or_eq_of_le h with (h | rfl)

Result:
case inl
b c : Ordinal.{u}
h✝ : b ≤ c
a : Ordinal.{u}
h : b < c
⊢ a ♯ b ≤ a ♯ c

case inr
b a : Ordinal.{u}
h : b ≤ b
⊢ a ♯ b ≤ a ♯ b

Proof state:
case inl
b c : Ordinal.{u}
h✝ : b ≤ c
a : Ordinal.{u}
h : b < c
⊢ a ♯ b ≤ a ♯ c

Tactic:
exact (nadd_lt_nadd_left h a).le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem idxOf?_toArray [BEq α] (a : α) (l : List α) :
    l.toArray.idxOf? a = l.idxOf? a

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ l.toArray.idxOf? a = idxOf? a l

Tactic:
rw [Array.idxOf?, idxOf?]

Result:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ Option.map (fun x => ↑x) (l.toArray.finIdxOf? a) = findIdx? (fun x => x == a) l

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ Option.map (fun x => ↑x) (l.toArray.finIdxOf? a) = findIdx? (fun x => x == a) l

Tactic:
simp [finIdxOf?, findIdx?_eq_map_findFinIdx?_val]

Result:
no goals