harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_sup {p : α → Prop} {f g : Filter α} :
    (∃ᶠ x in f ⊔ g, p x) ↔ (∃ᶠ x in f, p x) ∨ ∃ᶠ x in g, p x

Proof state:
α : Type u
p : α → Prop
f g : Filter α
⊢ (∃ᶠ (x : α) in f ⊔ g, p x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in g, p x

Tactic:
simp only [Filter.Frequently, eventually_sup, not_and_or]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem IsUniformInducing.equicontinuousOn_iff {F : ι → X → α} {S : Set X} {u : α → β}
    (hu : IsUniformInducing u) : EquicontinuousOn F S ↔ EquicontinuousOn ((u ∘ ·) ∘ F) S

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
u : α → β
hu : IsUniformInducing u
⊢ EquicontinuousOn F S ↔ EquicontinuousOn ((fun x => u ∘ x) ∘ F) S

Tactic:
congrm ∀ x ∈ S, ?_

Result:
case a
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
u : α → β
hu : IsUniformInducing u
x : X
⊢ EquicontinuousWithinAt F S x ↔ EquicontinuousWithinAt ((fun x => u ∘ x) ∘ F) S x

Proof state:
case a
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
u : α → β
hu : IsUniformInducing u
x : X
⊢ EquicontinuousWithinAt F S x ↔ EquicontinuousWithinAt ((fun x => u ∘ x) ∘ F) S x

Tactic:
rw [hu.equicontinuousWithinAt_iff]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
@[simp]
lemma exists_subset_image_iff {p : Set β → Prop} : (∃ t ⊆ f '' s, p t) ↔ ∃ t ⊆ s, p (f '' t)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ t ⊆ f '' s, p t) ↔ ∃ t ⊆ s, p (f '' t)

Tactic:
simp [subset_image_iff]

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem orderEmbOfCardLe_mem (s : Finset α) {k : ℕ} (h : k ≤ s.card) (a) :
    orderEmbOfCardLe s h a ∈ s

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : k ≤ #s
a : Fin k
⊢ (s.orderEmbOfCardLe h) a ∈ s

Tactic:
simp only [orderEmbOfCardLe, RelEmbedding.coe_trans, Finset.orderEmbOfFin_mem,
  Function.comp_apply]

Result:
no goals
-- Mathlib/Algebra/Homology/ExactSequence.lean
theorem ShortComplex.mapToComposableArrows_id {S₁ : ShortComplex C} :
    (ShortComplex.mapToComposableArrows (𝟙 S₁)) = 𝟙 S₁.toComposableArrows

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ : ShortComplex C
⊢ mapToComposableArrows (𝟙 S₁) = 𝟙 S₁.toComposableArrows

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.mul_toMatrix₂'_mul (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (M : Matrix n' n R)
    (N : Matrix m m' R) :
    M * toMatrix₂' R B * N = toMatrix₂' R (B.compl₁₂ (toLin' Mᵀ) (toLin' N))

Proof state:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
M : Matrix n' n R
N : Matrix m m' R
⊢ M * (toMatrix₂' R) B * N = (toMatrix₂' R) (B.compl₁₂ (toLin' Mᵀ) (toLin' N))

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem ratCast_im (q : ℚ) : im (q : K) = 0

Proof state:
K : Type u_1
inst✝ : RCLike K
q : ℚ
⊢ im ↑q = 0

Tactic:
rw [← ofReal_ratCast, ofReal_im]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_sub_const_uIcc : (fun x => x - a) ⁻¹' [[b, c]] = [[b + a, c + a]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' [[b, c]] = [[b + a, c + a]]

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem isUpperSet_iff_forall_lt : IsUpperSet s ↔ ∀ ⦃a b : α⦄, a < b → a ∈ s → b ∈ s :=
  forall_congr' fun a => by simp [le_iff_eq_or_lt, or_imp, forall_and]

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
a : α
⊢ (∀ ⦃b : α⦄, a ≤ b → a ∈ s → b ∈ s) ↔ ∀ ⦃b : α⦄, a < b → a ∈ s → b ∈ s

Tactic:
simp [le_iff_eq_or_lt, or_imp, forall_and]

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem contSupp_fix (f k) : contSupp (Cont'.fix f k) = codeSupp f (Cont'.fix f k)

Proof state:
f : Code
k : Cont'
⊢ contSupp (Cont'.fix f k) = codeSupp f (Cont'.fix f k)

Tactic:
simp +contextual [codeSupp, codeSupp', contSupp, Finset.union_assoc,
  Finset.subset_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_mul' (A : M) (h : IsUnit A.det) (m n : ℤ) : A ^ (m * n) = (A ^ n) ^ m

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℤ
⊢ A ^ (m * n) = (A ^ n) ^ m

Tactic:
rw [mul_comm, zpow_mul _ h]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem comp_whiskerLeft_symm (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') :
    f ◁ g ◁ η = (α_ f g h).inv ≫ (f ≫ g) ◁ η ≫ (α_ f g h').hom

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ f ◁ g ◁ η = (α_ f g h).inv ≫ (f ≫ g) ◁ η ≫ (α_ f g h').hom

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldl_filterMap (f : α → Option β) (g : γ → β → γ) (l : Vector α n) (init : γ) :
    (l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
init : γ
l : Array α
⊢ Array.foldl g init (Array.filterMap f { toArray := l, size_toArray := ⋯ }.toArray) =
    foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.foldl_filterMap']

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
init : γ
l : Array α
⊢ Array.foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init l =
    Array.foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init l

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
init : γ
l : Array α
⊢ Array.foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init l =
    Array.foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init l

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → Option β
g : γ → β → γ
l : Vector α n
init : γ
⊢ Array.foldl g init (Array.filterMap f l.toArray) =
    foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : γ → β → γ
init : γ
l : Array α
⊢ Array.foldl g init (Array.filterMap f { toArray := l, size_toArray := ⋯ }.toArray) =
    foldl
      (fun x y =>
        match f y with
        | some b => g x b
        | none => x)
      init { toArray := l, size_toArray := ⋯ }
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma fst_map_id_prod (κ : Kernel α β) {f : β → γ} (hf : Measurable f) :
    fst (map κ (fun a ↦ (a, f a))) = κ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
f : β → γ
hf : Measurable f
⊢ (κ.map fun a => (a, f a)).fst = κ

Tactic:
rw [fst_map_prod _ hf, Kernel.map_id']

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem contract_one {f : R[X]} : contract 1 f = f :=
  ext fun n ↦ by rw [coeff_contract one_ne_zero, mul_one]

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
⊢ (contract 1 f).coeff n = f.coeff n

Tactic:
rw [coeff_contract one_ne_zero, mul_one]

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
@[simp] lemma mem_Ioo : x ∈ Ioo a b ↔ a < x ∧ x < b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioo a b ↔ a < x ∧ x < b

Tactic:
rw [Ioo, ← Finset.mem_def, Finset.mem_Ioo]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_equiv_of_eq (eq : #α = #β) : #(α ≃ β) = 2 ^ #α

Proof state:
α β : Type u
inst✝ : Infinite α
eq : #α = #β
⊢ #(α ≃ β) = 2 ^ #α

Tactic:
rw [mk_equiv_of_lift_eq (lift_inj.mpr eq), lift_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insertMany_list_of_contains_eq_false [LawfulBEq α] (h : m.1.WF)
    {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)]
    (h' : (l.map Sigma.fst).contains k = false) :
    (m.insertMany l).1.get! k = m.get! k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k : α
inst✝ : Inhabited (β k)
h' : (List.map Sigma.fst l).contains k = false
⊢ (m.insertMany l).val.get! k = m.get! k

Tactic:
simp_to_model [insertMany] using List.getValueCast!_insertList_of_contains_eq_false

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
lemma differentiableAt_iff_comp_const_add {a b : 𝕜} :
    DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x ↦ f (b + x)) (-b + a)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x => f (b + x)) (-b + a)

Tactic:
simp [differentiableAt_comp_const_add]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_balanceR (l : Ordnode α) (x : α) (r : Ordnode α) :
    dual (balanceR l x r) = balanceL (dual r) x (dual l)

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.balanceR x r).dual = r.dual.balanceL x l.dual

Tactic:
rw [← dual_dual (balanceL _ _ _), dual_balanceL, dual_dual, dual_dual]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem discr_smul (a : R) : (a • Q).discr = a ^ Fintype.card n * Q.discr

Proof state:
R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Invertible 2
Q : QuadraticMap R (n → R) R
a : R
⊢ (a • Q).discr = a ^ Fintype.card n * Q.discr

Tactic:
simp only [discr, toMatrix'_smul, Matrix.det_smul]

Result:
no goals
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem Filter.Tendsto.atTop_add {C : α} (hf : Tendsto f l atTop) (hg : Tendsto g l (𝓝 C)) :
    Tendsto (fun x => f x + g x) l atTop

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => f x + g x) l atTop

Tactic:
conv in _ + _ => rw [add_comm]

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => g x + f x) l atTop

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => g x + f x) l atTop

Tactic:
exact hg.add_atTop hf

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Basic.lean
theorem UniformCauchySeqOn.mul (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) :
    UniformCauchySeqOn (f * f') l s := fun u hu => by
  simpa using (uniformContinuous_mul.comp_uniformCauchySeqOn (hf.prod' hf')) u hu

Proof state:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Type u_3
l : Filter ι
f f' : ι → β → α
s : Set β
hf : UniformCauchySeqOn f l s
hf' : UniformCauchySeqOn f' l s
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (m : ι × ι) in l ×ˢ l, ∀ x ∈ s, ((f * f') m.1 x, (f * f') m.2 x) ∈ u

Tactic:
simpa using (uniformContinuous_mul.comp_uniformCauchySeqOn (hf.prod' hf')) u hu

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem Normal.comap {H : Subgroup N} (hH : H.Normal) (f : G →* N) : (H.comap f).Normal :=
  ⟨fun _ => by simp +contextual [Subgroup.mem_comap, hH.conj_mem]⟩

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
hH : H.Normal
f : G →* N
x✝ : G
⊢ x✝ ∈ Subgroup.comap f H → ∀ (g : G), g * x✝ * g⁻¹ ∈ Subgroup.comap f H

Tactic:
simp +contextual [Subgroup.mem_comap, hH.conj_mem]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma add_of_Z_eq_zero {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q)
    (hPz : P z = 0) (hQz : Q z = 0) : W.add P Q = P y ^ 4 • ![0, 1, 0]

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ W.add P Q = P y ^ 4 • ![0, 1, 0]

Tactic:
rw [add, if_pos <| equiv_of_Z_eq_zero hP hQ hPz hQz, dblXYZ_of_Z_eq_zero hP.left hPz]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_empty_right : image₂ f s ∅ = ∅ :=
  coe_injective <| by simp

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
⊢ ↑(image₂ f s ∅) = ↑∅

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Multiset.lean
lemma prod_map_sum {s : Multiset (Multiset α)} :
    prod (s.map sum) = sum ((Sections s).map prod) :=
  Multiset.induction_on s (by simp) fun a s ih ↦ by
    simp [ih, map_bind, sum_map_mul_left, sum_map_mul_right]

Proof state:
α : Type u_2
inst✝ : CommSemiring α
s : Multiset (Multiset α)
⊢ (map sum 0).prod = (map prod (Sections 0)).sum

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CommSemiring α
s✝ : Multiset (Multiset α)
a : Multiset α
s : Multiset (Multiset α)
ih : (map sum s).prod = (map prod s.Sections).sum
⊢ (map sum (a ::ₘ s)).prod = (map prod (a ::ₘ s).Sections).sum

Tactic:
simp [ih, map_bind, sum_map_mul_left, sum_map_mul_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem join_ne_none : x.join ≠ none ↔ ∃ z, x = some (some z)

Proof state:
α✝ : Type u_1
x : Option (Option α✝)
⊢ x.join ≠ none ↔ ∃ z, x = some (some z)

Tactic:
simp only [ne_none_iff_exists', join_eq_some, iff_self]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem data_takeWhile (p : Char → Bool) (s : String) :
    (s.takeWhile p).1 = s.1.takeWhile p

Proof state:
p : Char → Bool
s : String
⊢ (s.takeWhile p).data = List.takeWhile p s.data

Tactic:
rw [takeWhile_eq]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
lemma tendsto_nat_ceil_atTop {α : Type*} [LinearOrderedSemiring α] [FloorSemiring α] :
    Tendsto (fun x : α ↦ ⌈x⌉₊) atTop atTop

Proof state:
α : Type u_4
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
x : ℕ
⊢ x ≤ ⌈↑x⌉₊

Tactic:
simp only [Nat.ceil_natCast, le_refl]

Result:
no goals

Proof state:
α : Type u_4
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
⊢ Tendsto (fun x => ⌈x⌉₊) atTop atTop

Tactic:
refine Nat.ceil_mono.tendsto_atTop_atTop (fun x ↦ ⟨x, ?_⟩)

Result:
α : Type u_4
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
x : ℕ
⊢ x ≤ ⌈↑x⌉₊
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_le_ker_iff {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} :
    range f ≤ ker g ↔ (g.comp f : M →ₛₗ[τ₁₃] M₃) = 0 :=
  ⟨fun h => ker_eq_top.1 <| eq_top_iff'.2 fun _ => h <| ⟨_, rfl⟩, fun h x hx =>
    mem_ker.2 <| Exists.elim hx fun y hy => by rw [← hy, ← comp_apply, h, zero_apply]⟩

Proof state:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
h : g.comp f = 0
x : M₂
hx : x ∈ range f
y : M
hy : f y = x
⊢ g x = 0

Tactic:
rw [← hy, ← comp_apply, h, zero_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_eq_true {l : List α} : l.any p = true ↔ ∃ x, x ∈ l ∧ p x

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ l.any p = true ↔ ∃ x, x ∈ l ∧ p x = true

Tactic:
simp only [any_eq, decide_eq_true_eq]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma IsBase.fundCircuit_isCircuit {B : Set α} (hB : M.IsBase B) (hxE : x ∈ M.E) (hxB : x ∉ B) :
    M.IsCircuit (M.fundCircuit x B) :=
  hB.indep.fundCircuit_isCircuit (by rwa [hB.closure_eq]) hxB

Proof state:
α : Type u_1
M : Matroid α
x : α
B : Set α
hB : M.IsBase B
hxE : x ∈ M.E
hxB : x ∉ B
⊢ x ∈ M.closure B

Tactic:
rwa [hB.closure_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_eq_pi {x} : arccos x = π ↔ x ≤ -1

Proof state:
x : ℝ
⊢ arccos x = π ↔ x ≤ -1

Tactic:
rw [arccos, sub_eq_iff_eq_add, ← sub_eq_iff_eq_add', div_two_sub_self, neg_pi_div_two_eq_arcsin]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
lemma ae_iff_of_countable [Countable α] {p : α → Prop} : (∀ᵐ x ∂μ, p x) ↔ ∀ x, μ {x} ≠ 0 → p x

Proof state:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable α
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ, p x) ↔ ∀ (x : α), μ {x} ≠ 0 → p x

Tactic:
rw [ae_iff, measure_null_iff_singleton]

Result:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable α
p : α → Prop
⊢ (∀ x ∈ {a | ¬p a}, μ {x} = 0) ↔ ∀ (x : α), μ {x} ≠ 0 → p x

α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable α
p : α → Prop
⊢ {a | ¬p a}.Countable

Proof state:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable α
p : α → Prop
⊢ (∀ x ∈ {a | ¬p a}, μ {x} = 0) ↔ ∀ (x : α), μ {x} ≠ 0 → p x

α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable α
p : α → Prop
⊢ {a | ¬p a}.Countable

Tactic:
exacts [forall_congr' fun _ ↦ not_imp_comm, Set.to_countable _]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma toAffine_of_Z_ne_zero {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P z ≠ 0) :
    toAffine W P = .some ((nonsingular_of_Z_ne_zero hPz).mp hP)

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z ≠ 0
⊢ toAffine W P = Affine.Point.some ⋯

Tactic:
rw [toAffine, dif_pos ⟨hP, hPz⟩]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem setBlack_toList {t : RBNode α} : t.setBlack.toList = t.toList

Proof state:
α : Type u_1
t : RBNode α
⊢ t.setBlack.toList = t.toList

Tactic:
cases t <;> simp [setBlack]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_eq_singleton_iff {l : List α} {n : ℕ} {x : α} : l.rotate n = [x] ↔ l = [x]

Proof state:
α : Type u
l : List α
n : ℕ
x : α
⊢ l.rotate n = [x] ↔ l = [x]

Tactic:
rw [rotate_eq_iff, rotate_singleton]

Result:
no goals
-- Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
lemma iff_flat_and_ideal_smul_eq_top :
    FaithfullyFlat R M ↔
    (Flat R M ∧ ∀ (I : Ideal R), I • (⊤ : Submodule R M) = ⊤ → I = ⊤) :=
  iff_flat_and_proper_ideal R M |>.trans <| and_congr_right_iff.2 fun _ => iff_of_eq <|
    forall_congr fun I => eq_iff_iff.2 <| by tauto

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : Flat R M
I : Ideal R
⊢ I ≠ ⊤ → I • ⊤ ≠ ⊤ ↔ I • ⊤ = ⊤ → I = ⊤

Tactic:
tauto

Result:
no goals
-- Mathlib/Data/Nat/WithBot.lean
theorem lt_one_iff_le_zero {x : WithBot ℕ} : x < 1 ↔ x ≤ 0 :=
  not_iff_not.mp (by simpa using one_le_iff_zero_lt)

Proof state:
x : WithBot ℕ
⊢ ¬x < 1 ↔ ¬x ≤ 0

Tactic:
simpa using one_le_iff_zero_lt

Result:
no goals
-- Mathlib/Algebra/Lie/Abelian.lean
lemma commute_toEnd_of_mem_center_left :
    Commute (toEnd R L M x) (toEnd R L M y)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : L
hx : x ∈ LieAlgebra.center R L
y : L
⊢ Commute ((toEnd R L M) x) ((toEnd R L M) y)

Tactic:
rw [Commute.symm_iff, commute_iff_lie_eq, ← LieHom.map_lie, hx y, LieHom.map_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem ae_iff_measure_eq [IsFiniteMeasure μ] {p : α → Prop}
    (hp : NullMeasurableSet { a | p a } μ) : (∀ᵐ a ∂μ, p a) ↔ μ { a | p a } = μ univ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
p : α → Prop
hp : NullMeasurableSet {a | p a} μ
⊢ (∀ᵐ (a : α) ∂μ, p a) ↔ μ {a | p a} = μ univ

Tactic:
rw [← ae_eq_univ_iff_measure_eq hp, eventuallyEq_univ, eventually_iff]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem mul_inv_of_unit {n : ℕ} (a : ZMod n) (h : IsUnit a) : a * a⁻¹ = 1

Proof state:
case intro
n : ℕ
u : (ZMod n)ˣ
⊢ ↑u * (↑u)⁻¹ = 1

Tactic:
rw [inv_coe_unit, u.mul_inv]

Result:
no goals

Proof state:
n : ℕ
a : ZMod n
h : IsUnit a
⊢ a * a⁻¹ = 1

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
n : ℕ
u : (ZMod n)ˣ
⊢ ↑u * (↑u)⁻¹ = 1
-- Mathlib/NumberTheory/Harmonic/GammaDeriv.lean
lemma hasDerivAt_Gamma_one : HasDerivAt Gamma (-γ) 1

Proof state:
⊢ HasDerivAt Gamma (-γ) 1

Tactic:
simpa only [factorial_zero, cast_one, harmonic_zero, Rat.cast_zero, add_zero, mul_neg, one_mul,
  cast_zero, zero_add] using hasDerivAt_Gamma_nat 0

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem cond_congr (discr lhs rhs discr' lhs' rhs' : Bool) (h1 : discr' = discr) (h2 : lhs' = lhs)
    (h3 : rhs' = rhs) :
    (bif discr' then lhs' else rhs') = (bif discr then lhs else rhs)

Proof state:
discr lhs rhs discr' lhs' rhs' : Bool
h1 : discr' = discr
h2 : lhs' = lhs
h3 : rhs' = rhs
⊢ (bif discr' then lhs' else rhs') = bif discr then lhs else rhs

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem range_eq_top {N} [Group N] {f : G →* N} :
    f.range = (⊤ : Subgroup N) ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_range, coe_top]) Set.range_eq_univ

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_7
inst✝ : Group N
f : G →* N
⊢ ↑f.range = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
rw [coe_range, coe_top]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem digitsAux_zero (b : ℕ) (h : 2 ≤ b) : digitsAux b h 0 = []

Proof state:
b : ℕ
h : 2 ≤ b
⊢ b.digitsAux h 0 = []

Tactic:
rw [digitsAux]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insertMany_empty_list_of_mem [LawfulBEq α]
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} [Inhabited β]
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    get! (insertMany (empty : Raw₀ α (fun _ => β)) l) k' = v

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : LawfulBEq α
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
inst✝ : Inhabited β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
⊢ get! (insertMany empty l).val k' = v

Tactic:
rw [get!_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem lineMap_vadd_apply (p : P1) (v : V1) (c : k) : lineMap p (v +ᵥ p) c = c • v +ᵥ p

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p : P1
v : V1
c : k
⊢ (lineMap p (v +ᵥ p)) c = c • v +ᵥ p

Tactic:
rw [lineMap_apply, vadd_vsub]

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

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

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

Result:
no goals