harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/UpperLower/Basic.lean
theorem compl_iSup (f : ι → LowerSet α) : (⨆ i, f i).compl = ⨆ i, (f i).compl :=
  UpperSet.ext <| by simp only [coe_compl, coe_iSup, compl_iUnion, UpperSet.coe_iSup]

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
f : ι → LowerSet α
⊢ ↑(⨆ i, f i).compl = ↑(⨆ i, (f i).compl)

Tactic:
simp only [coe_compl, coe_iSup, compl_iUnion, UpperSet.coe_iSup]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem prod_eq_tprod_mulIndicator (f : β → α) (s : Finset β) :
    ∏ x ∈ s, f x = ∏' x, Set.mulIndicator (↑s) f x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
s : Finset β
⊢ ∏ x ∈ s, f x = ∏' (x : β), (↑s).mulIndicator f x

Tactic:
rw [tprod_eq_prod' (Set.mulSupport_mulIndicator_subset),
    Finset.prod_mulIndicator_subset _ Finset.Subset.rfl]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Completion.lean
theorem LipschitzWith.completion_extension [MetricSpace β] [CompleteSpace β] {f : α → β}
    {K : ℝ≥0} (h : LipschitzWith K f) : LipschitzWith K (Completion.extension f) :=
  LipschitzWith.of_dist_le_mul fun x y => induction_on₂ x y
    (isClosed_le (by fun_prop) (by fun_prop)) <| by
      simpa only [extension_coe h.uniformContinuous, Completion.dist_eq] using h.dist_le_mul

Proof state:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ Continuous fun x => dist (Completion.extension f x.1) (Completion.extension f x.2)

Tactic:
fun_prop

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ ∀ (a b : α), dist (Completion.extension f ↑a) (Completion.extension f ↑b) ≤ ↑K * dist ↑a ↑b

Tactic:
simpa only [extension_coe h.uniformContinuous, Completion.dist_eq] using h.dist_le_mul

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ Continuous fun x => ↑K * dist x.1 x.2

Tactic:
fun_prop

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem map_ext {N} {f g : AdicCompletion I M → N}
    (h : ∀ (a : AdicCauchySequence I M),
      f (AdicCompletion.mk I M a) = g (AdicCompletion.mk I M a)) :
    f = g

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Sort u_6
f g : AdicCompletion I M → N
h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)
⊢ f = g

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Sort u_6
f g : AdicCompletion I M → N
h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)
x : AdicCompletion I M
⊢ f x = g x

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Sort u_6
f g : AdicCompletion I M → N
h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)
x : AdicCompletion I M
⊢ f x = g x

Tactic:
apply induction_on I M x h

Result:
no goals
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem coe_sumSq : sumSq T = {s : T | IsSumSq s}

Proof state:
case h
T : Type u_2
inst✝ : CommSemiring T
x✝ : T
⊢ x✝ ∈ ↑(sumSq T) ↔ x✝ ∈ {s | IsSumSq s}

Tactic:
simp

Result:
no goals

Proof state:
T : Type u_2
inst✝ : CommSemiring T
⊢ ↑(sumSq T) = {s | IsSumSq s}

Tactic:
ext

Result:
case h
T : Type u_2
inst✝ : CommSemiring T
x✝ : T
⊢ x✝ ∈ ↑(sumSq T) ↔ x✝ ∈ {s | IsSumSq s}
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_up : -up = down

Proof state:
⊢ -up = down

Tactic:
simp [up, down]

Result:
no goals
-- Mathlib/RingTheory/ClassGroup.lean
theorem coe_toPrincipalIdeal (x : Kˣ) :
    (toPrincipalIdeal R K x : FractionalIdeal R⁰ K) = spanSingleton _ (x : K)

Proof state:
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : Kˣ
⊢ ↑({ toFun := fun x => { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ },
          map_one' := ⋯, map_mul' := ⋯ }
        x) =
    spanSingleton R⁰ ↑x

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : Kˣ
⊢ ↑((toPrincipalIdeal R K) x) = spanSingleton R⁰ ↑x

Tactic:
simp only [toPrincipalIdeal]

Result:
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : Kˣ
⊢ ↑({ toFun := fun x => { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ },
          map_one' := ⋯, map_mul' := ⋯ }
        x) =
    spanSingleton R⁰ ↑x
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem lt_aleph0_of_finite {ι : Type w}
    [Module.Finite R M] {v : ι → M} (h : LinearIndependent R v) : #ι < ℵ₀

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ #ι < ℵ₀

Tactic:
apply Cardinal.lift_lt.1

Result:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ lift.{?u.115417, w} #ι < lift.{?u.115417, w} ℵ₀

Proof state:
case hbc
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ ↑(finrank R M) < ℵ₀

Tactic:
apply Cardinal.nat_lt_aleph0

Result:
no goals

Proof state:
case hbc
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ lift.{w, v} (Module.rank R M) < lift.{v, w} ℵ₀

Tactic:
rw [← finrank_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_natCast]

Result:
case hbc
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ ↑(finrank R M) < ℵ₀

Proof state:
case hab
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ lift.{?u.115417, w} #ι ≤ ?b

Tactic:
apply h.cardinal_lift_le_rank

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ lift.{?u.115417, w} #ι < lift.{?u.115417, w} ℵ₀

Tactic:
apply lt_of_le_of_lt

Result:
case hab
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ lift.{?u.115417, w} #ι ≤ ?b

case hbc
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ ?b < lift.{?u.115417, w} ℵ₀

case b
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ Cardinal.{max w ?u.115417}
-- Mathlib/Logic/Equiv/Basic.lean
theorem Perm.extendDomain_apply_image (a : α') : e.extendDomain f (f a) = f (e a)

Proof state:
α' : Type u_9
β' : Type u_10
e : Perm α'
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
a : α'
⊢ (e.extendDomain f) ↑(f a) = ↑(f (e a))

Tactic:
simp [Perm.extendDomain]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Slope.lean
theorem slope_comm (f : k → PE) (a b : k) : slope f a b = slope f b a

Proof state:
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ slope f a b = slope f b a

Tactic:
rw [slope, slope, ← neg_vsub_eq_vsub_rev, smul_neg, ← neg_smul, neg_inv, neg_sub]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem apply_ne_zero_iff [MulZeroOneClass α] [Nontrivial α] (h : IsAdjMatrix A) (i j : V) :
    ¬A i j = 0 ↔ A i j = 1

Proof state:
V : Type u_1
α : Type u_2
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
i j : V
⊢ ¬A i j = 0 ↔ A i j = 1

Tactic:
rw [← apply_ne_one_iff h, Classical.not_not]

Result:
no goals
-- Mathlib/Data/Multiset/DershowitzManna.lean
/-- `TransGen OneStep` and `IsDershowitzMannaLT` are equivalent. -/
private lemma transGen_oneStep_eq_isDershowitzMannaLT :
    (TransGen OneStep : Multiset α → Multiset α → Prop) = IsDershowitzMannaLT

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ TransGen Multiset.OneStep = IsDershowitzMannaLT

Tactic:
ext M N

Result:
case h.h.a
α : Type u_1
inst✝ : Preorder α
M N : Multiset α
⊢ TransGen Multiset.OneStep M N ↔ M.IsDershowitzMannaLT N

Proof state:
case h.h.a
α : Type u_1
inst✝ : Preorder α
M N : Multiset α
⊢ TransGen Multiset.OneStep M N ↔ M.IsDershowitzMannaLT N

Tactic:
exact ⟨isDershowitzMannaLT_of_transGen_oneStep, transGen_oneStep_of_isDershowitzMannaLT⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/BasicAux.lean
theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a < sizeOf as

Proof state:
case head
α : Type u_1
a : α
inst✝ : SizeOf α
as as✝ : List α
⊢ sizeOf a < sizeOf (a :: as✝)

Tactic:
simp_arith

Result:
no goals

Proof state:
case tail
α : Type u_1
a : α
inst✝ : SizeOf α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : sizeOf a < sizeOf as✝
⊢ sizeOf a < sizeOf (b✝ :: as✝)

Tactic:
exact Nat.lt_trans ih (by simp_arith)

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : SizeOf α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : sizeOf a < sizeOf as✝
⊢ sizeOf as✝ < sizeOf (b✝ :: as✝)

Tactic:
simp_arith

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : SizeOf α
as : List α
h : a ∈ as
⊢ sizeOf a < sizeOf as

Tactic:
induction h with
| head => simp_arith
| tail _ _ ih => exact Nat.lt_trans ih (by simp_arith)

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eval_basisDivisor_left_of_ne (hxy : x ≠ y) : eval x (basisDivisor x y) = 1

Proof state:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ * (x - y) = 1

Tactic:
exact inv_mul_cancel₀ (sub_ne_zero_of_ne hxy)

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ eval x (basisDivisor x y) = 1

Tactic:
simp only [basisDivisor, eval_mul, eval_C, eval_sub, eval_X]

Result:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ * (x - y) = 1
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma CWComplex.closed (C : Set X) [CWComplex C] [T2Space X] (A : Set X) (asubc : A ⊆ C) :
    IsClosed A ↔ ∀ n (j : cell C n), IsClosed (A ∩ closedCell n j)

Proof state:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : CWComplex C
inst✝ : T2Space X
A : Set X
asubc : A ⊆ C
this : IsClosed A ↔ (∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ closedCell n j)) ∧ IsClosed (A ∩ ∅)
⊢ IsClosed A ↔ ∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ closedCell n j)

Tactic:
simp_all

Result:
no goals

Proof state:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : CWComplex C
inst✝ : T2Space X
A : Set X
asubc : A ⊆ C
⊢ IsClosed A ↔ ∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ closedCell n j)

Tactic:
have := RelCWComplex.closed C A asubc

Result:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : CWComplex C
inst✝ : T2Space X
A : Set X
asubc : A ⊆ C
this : IsClosed A ↔ (∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ closedCell n j)) ∧ IsClosed (A ∩ ∅)
⊢ IsClosed A ↔ ∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ closedCell n j)
-- Mathlib/Data/Set/Operations.lean
theorem mem_univ_pi : f ∈ pi univ t ↔ ∀ i, f i ∈ t i

Proof state:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ univ.pi t ↔ ∀ (i : ι), f i ∈ t i

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem getD_val [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α} {fallback : β a} :
    m.val.getD a fallback = m.getD a fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
fallback : β a
⊢ m.val.getD a fallback = m.getD a fallback

Tactic:
simp [Raw.getD, m.2]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_bilinear_hasDerivAt_right_eq_sub [CompleteSpace G]
    (hu : ∀ x, HasDerivAt u (u' x) x) (hv : ∀ x, HasDerivAt v (v' x) x)
    (huv' : Integrable (fun x ↦ L (u x) (v' x))) (hu'v : Integrable (fun x ↦ L (u' x) (v x)))
    (h_bot : Tendsto (fun x ↦ L (u x) (v x)) atBot (𝓝 m))
    (h_top : Tendsto (fun x ↦ L (u x) (v x)) atTop (𝓝 n)) :
    ∫ (x : ℝ), L (u x) (v' x) = n - m - ∫ (x : ℝ), L (u' x) (v x)

Proof state:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
m n : G
inst✝ : CompleteSpace G
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
h_bot : Tendsto (fun x => (L (u x)) (v x)) atBot (𝓝 m)
h_top : Tendsto (fun x => (L (u x)) (v x)) atTop (𝓝 n)
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = n - m - ∫ (x : ℝ), (L (u' x)) (v x)

Tactic:
rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]

Result:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
m n : G
inst✝ : CompleteSpace G
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
h_bot : Tendsto (fun x => (L (u x)) (v x)) atBot (𝓝 m)
h_top : Tendsto (fun x => (L (u x)) (v x)) atTop (𝓝 n)
⊢ ∫ (a : ℝ), (L (u a)) (v' a) + (L (u' a)) (v a) = n - m

Proof state:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
m n : G
inst✝ : CompleteSpace G
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
h_bot : Tendsto (fun x => (L (u x)) (v x)) atBot (𝓝 m)
h_top : Tendsto (fun x => (L (u x)) (v x)) atTop (𝓝 n)
⊢ ∫ (a : ℝ), (L (u a)) (v' a) + (L (u' a)) (v a) = n - m

Tactic:
exact integral_bilinear_hasDerivAt_eq_sub hu hv (huv'.add hu'v) h_bot h_top

Result:
no goals
-- Mathlib/Data/List/TFAE.lean
theorem exists_tfae {α : Type*} (l : List (α → Prop)) (H : ∀ a : α, (l.map (fun p ↦ p a)).TFAE) :
    (l.map (fun p ↦ ∃ a, p a)).TFAE

Proof state:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p => p a) l).TFAE
⊢ (map (fun p => ∃ a, p a) l).TFAE

Tactic:
simp only [TFAE, List.forall_mem_map]

Result:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p => p a) l).TFAE
⊢ ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∃ a, j a) ↔ ∃ a, j_1 a)

Proof state:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p => p a) l).TFAE
⊢ ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∃ a, j a) ↔ ∃ a, j_1 a)

Tactic:
intros p₁ hp₁ p₂ hp₂

Result:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p => p a) l).TFAE
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∃ a, p₁ a) ↔ ∃ a, p₂ a

Proof state:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p => p a) l).TFAE
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∃ a, p₁ a) ↔ ∃ a, p₂ a

Tactic:
exact exists_congr fun a ↦ H a (p₁ a) (mem_map_of_mem (fun p ↦ p a) hp₁)
  (p₂ a) (mem_map_of_mem (fun p ↦ p a) hp₂)

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem comap_liftQ (f : M →ₛₗ[τ₁₂] M₂) (h) : q.comap (p.liftQ f h) = (q.comap f).map (mkQ p) :=
  le_antisymm (by rintro ⟨x⟩ hx; exact ⟨_, hx, rfl⟩)
    (by rw [map_le_iff_le_comap, ← comap_comp, liftQ_mkQ])

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
⊢ comap (p.liftQ f h) q ≤ map p.mkQ (comap f q)

Tactic:
rintro ⟨x⟩ hx

Result:
case mk
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
x✝ : M ⧸ p
x : M
hx : Quot.mk (⇑p.quotientRel) x ∈ comap (p.liftQ f h) q
⊢ Quot.mk (⇑p.quotientRel) x ∈ map p.mkQ (comap f q)

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
x✝ : M ⧸ p
x : M
hx : Quot.mk (⇑p.quotientRel) x ∈ comap (p.liftQ f h) q
⊢ Quot.mk (⇑p.quotientRel) x ∈ map p.mkQ (comap f q)

Tactic:
exact ⟨_, hx, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
⊢ map p.mkQ (comap f q) ≤ comap (p.liftQ f h) q

Tactic:
rw [map_le_iff_le_comap, ← comap_comp, liftQ_mkQ]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma mod_add_div' (a b : ℕ) : a % b + a / b * b = a

Proof state:
a b : ℕ
⊢ a % b + a / b * b = a

Tactic:
rw [Nat.mul_comm]

Result:
a b : ℕ
⊢ a % b + b * (a / b) = a

Proof state:
a b : ℕ
⊢ a % b + b * (a / b) = a

Tactic:
exact mod_add_div _ _

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem mul_neg_of_neg_of_pos [MulPosStrictMono α] (ha : a < 0) (hb : 0 < b) : a * b < 0

Proof state:
α : Type u_3
a b : α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
ha : a < 0
hb : 0 < b
⊢ a * b < 0

Tactic:
simpa only [zero_mul] using mul_lt_mul_of_pos_right ha hb

Result:
no goals
-- Mathlib/Data/Finset/Disjoint.lean
theorem disjoint_singleton_left : Disjoint (singleton a) s ↔ a ∉ s

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ Disjoint {a} s ↔ a ∉ s

Tactic:
simp only [disjoint_left, mem_singleton, forall_eq]

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem lift_graph {f : α → β} {a b} : (a, b) ∈ (f : α →. β).graph ↔ f a = b :=
  show (∃ _ : True, f a = b) ↔ f a = b by simp

Proof state:
α : Type u_1
β : Type u_2
f : α → β
a : α
b : β
⊢ (∃ (_ : True), f a = b) ↔ f a = b

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem deriv_circleMap_eq_zero_iff {c : ℂ} {R : ℝ} {θ : ℝ} :
    deriv (circleMap c R) θ = 0 ↔ R = 0

Proof state:
c : ℂ
R θ : ℝ
⊢ deriv (circleMap c R) θ = 0 ↔ R = 0

Tactic:
simp [I_ne_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Basic.lean
theorem imageIsoImage_hom_comp_image_ι : (imageIsoImage f).hom ≫ Limits.image.ι _ = kernel.ι _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (imageIsoImage f).hom ≫ Limits.image.ι f = kernel.ι (cokernel.π f)

Tactic:
simp only [IsImage.isoExt_hom, IsImage.lift_ι, imageStrongEpiMonoFactorisation_m]

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem ldiff_bit (a m b n) : ldiff (bit a m) (bit b n) = bit (a && not b) (ldiff m n)

Proof state:
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ (bit a m).ldiff (bit b n) = bit (a && !b) (m.ldiff n)

Tactic:
rw [← bitwise_diff, bitwise_bit]

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
lemma Filter.EventuallyEq.iteratedDeriv_eq (n : ℕ) {f g : 𝕜 → F} {x : 𝕜} (hfg : f =ᶠ[𝓝 x] g) :
    iteratedDeriv n f x = iteratedDeriv n g x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f g : 𝕜 → F
x : 𝕜
hfg : f =ᶠ[𝓝 x] g
⊢ iteratedDeriv n f x = iteratedDeriv n g x

Tactic:
simp only [← iteratedDerivWithin_univ, iteratedDerivWithin_eq_iteratedFDerivWithin]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f g : 𝕜 → F
x : 𝕜
hfg : f =ᶠ[𝓝 x] g
⊢ ((iteratedFDerivWithin 𝕜 n f Set.univ x) fun x => 1) = (iteratedFDerivWithin 𝕜 n g Set.univ x) fun x => 1

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f g : 𝕜 → F
x : 𝕜
hfg : f =ᶠ[𝓝 x] g
⊢ ((iteratedFDerivWithin 𝕜 n f Set.univ x) fun x => 1) = (iteratedFDerivWithin 𝕜 n g Set.univ x) fun x => 1

Tactic:
rw [(hfg.filter_mono nhdsWithin_le_nhds).iteratedFDerivWithin_eq hfg.eq_of_nhds n]

Result:
no goals