harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_sum_of_countable [Countable ι] (μ : ι → Measure α) (s : Set α) :
    (sum μ).restrict s = sum fun i => (μ i).restrict s

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst✝ : Countable ι
μ : ι → Measure α
s : Set α
⊢ (sum μ).restrict s = sum fun i => (μ i).restrict s

Tactic:
ext t ht

Result:
case h
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst✝ : Countable ι
μ : ι → Measure α
s t : Set α
ht : MeasurableSet t
⊢ ((sum μ).restrict s) t = (sum fun i => (μ i).restrict s) t

Proof state:
case h
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst✝ : Countable ι
μ : ι → Measure α
s t : Set α
ht : MeasurableSet t
⊢ ((sum μ).restrict s) t = (sum fun i => (μ i).restrict s) t

Tactic:
simp_rw [sum_apply _ ht, restrict_apply ht, sum_apply_of_countable]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem sOppSide_pointReflection {s : AffineSubspace R P} {x y : P} (hx : x ∈ s) (hy : y ∉ s) :
    s.SOppSide y (pointReflection R x y)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
hy : y ∉ s
⊢ s.SOppSide y ((pointReflection R x) y)

Tactic:
refine (sbtw_pointReflection_of_ne R fun h => hy ?_).sOppSide_of_not_mem_of_mem hy hx

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
hy : y ∉ s
h : x = y
⊢ y ∈ s

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
hy : y ∉ s
h : x = y
⊢ y ∈ s

Tactic:
rwa [← h]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem map_reverse_inits (l : List α) : map reverse l.inits = (reverse <| tails <| reverse l)

Proof state:
α : Type u_1
l : List α
⊢ map reverse l.inits = l.reverse.tails.reverse

Tactic:
rw [inits_eq_tails l]

Result:
α : Type u_1
l : List α
⊢ map reverse (map reverse l.reverse.tails).reverse = l.reverse.tails.reverse

Proof state:
α : Type u_1
l : List α
⊢ map reverse (map reverse l.reverse.tails).reverse = l.reverse.tails.reverse

Tactic:
simp [reverse_involutive.comp_self, ← map_reverse]

Result:
no goals
-- Mathlib/FieldTheory/SplittingField/IsSplittingField.lean
theorem IntermediateField.splits_of_splits (h : p.Splits (algebraMap K L))
    (hF : ∀ x ∈ p.rootSet L, x ∈ F) : p.Splits (algebraMap K F)

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ x ∈ p.aroots L, x ∈ F.val.fieldRange
⊢ Splits (algebraMap K ↥F) p

Tactic:
exact splits_of_comp _ F.val.toRingHom h hF

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ x ∈ p.rootSet L, x ∈ F
⊢ Splits (algebraMap K ↥F) p

Tactic:
classical
simp_rw [← F.fieldRange_val, rootSet_def, Finset.mem_coe, Multiset.mem_toFinset] at hF
exact splits_of_comp _ F.val.toRingHom h hF

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ x ∈ p.rootSet L, x ∈ F
⊢ Splits (algebraMap K ↥F) p

Tactic:
simp_rw [← F.fieldRange_val, rootSet_def, Finset.mem_coe, Multiset.mem_toFinset] at hF

Result:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ x ∈ p.aroots L, x ∈ F.val.fieldRange
⊢ Splits (algebraMap K ↥F) p
-- Mathlib/Algebra/Module/Presentation/Basic.lean
/-- The sequence `(relations.R →₀ A) → (relations.G →₀ A) → M → 0` is exact. -/
lemma exact : Function.Exact relations.map solution.π

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentation
⊢ Function.Exact ⇑relations.map ⇑solution.π

Tactic:
rw [LinearMap.exact_iff, range_map, ← solution.injective_fromQuotient_iff_ker_π_eq_span]

Result:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentation
⊢ Function.Injective ⇑solution.fromQuotient

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentation
⊢ Function.Injective ⇑solution.fromQuotient

Tactic:
exact h.bijective.1

Result:
no goals
-- Mathlib/Analysis/Convex/Strict.lean
theorem StrictConvex.linear_image [Semiring 𝕝] [Module 𝕝 E] [Module 𝕝 F]
    [LinearMap.CompatibleSMul E F 𝕜 𝕝] (hs : StrictConvex 𝕜 s) (f : E →ₗ[𝕝] F) (hf : IsOpenMap f) :
    StrictConvex 𝕜 (f '' s)

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap ⇑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : f x ≠ f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y ∈ interior (⇑f '' s)

Tactic:
refine hf.image_interior_subset _ ⟨a • x + b • y, hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, ?_⟩

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap ⇑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : f x ≠ f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x + b • y) = a • f x + b • f y

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap ⇑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : f x ≠ f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x + b • y) = a • f x + b • f y

Tactic:
rw [map_add, f.map_smul_of_tower a, f.map_smul_of_tower b]

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap ⇑f
⊢ StrictConvex 𝕜 (⇑f '' s)

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ hxy a b ha hb hab

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap ⇑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : f x ≠ f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y ∈ interior (⇑f '' s)
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem coeff_single_of_ne (h : b ≠ a) : (single a r).coeff b = 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a b : Γ
r : R
h : b ≠ a
⊢ ((single a) r).coeff b = 0

Tactic:
classical exact Pi.single_eq_of_ne (f := fun _ => R) h r

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a b : Γ
r : R
h : b ≠ a
⊢ ((single a) r).coeff b = 0

Tactic:
exact Pi.single_eq_of_ne (f := fun _ => R) h r

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Group.lean
theorem tendsto_atTop_add_right_of_le' (C : β) (hf : Tendsto f l atTop) (hg : ∀ᶠ x in l, C ≤ g x) :
    Tendsto (fun x => f x + g x) l atTop :=
  .atTop_of_add_isBoundedUnder_le (g := -g) ⟨-C, by simpa⟩ (by simpa)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : OrderedAddCommGroup β
l : Filter α
f g : α → β
C : β
hf : Tendsto f l atTop
hg : ∀ᶠ (x : α) in l, C ≤ g x
⊢ Tendsto (fun x => f x + g x + (-g) x) l atTop

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : OrderedAddCommGroup β
l : Filter α
f g : α → β
C : β
hf : Tendsto f l atTop
hg : ∀ᶠ (x : α) in l, C ≤ g x
⊢ ∀ᶠ (x : β) in map (-g) l, (fun x1 x2 => x1 ≤ x2) x (-C)

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem normalize_eq_one {a : G₀} (h0 : a ≠ 0) : normalize a = 1

Proof state:
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a : G₀
h0 : a ≠ 0
⊢ normalize a = 1

Tactic:
simp [normalize_apply, h0]

Result:
no goals
-- Mathlib/Algebra/Homology/ExactSequence.lean
@[reassoc]
lemma IsComplex.zero' (hS : S.IsComplex) (i j k : ℕ) (hij : i + 1 = j

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C n
hS : S.IsComplex
i : ℕ
hk : autoParam (i + 1 + 1 ≤ n) _auto✝
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 1 + 1) ⋯ hk = 0

Tactic:
exact hS.zero i hk

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C n
hS : S.IsComplex
i j k : ℕ
hij : autoParam (i + 1 = j) _auto✝
hjk : autoParam (j + 1 = k) _auto✝
hk : autoParam (k ≤ n) _auto✝
⊢ S.map' i j ⋯ ⋯ ≫ S.map' j k ⋯ hk = 0

Tactic:
subst hij hjk

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C n
hS : S.IsComplex
i : ℕ
hk : autoParam (i + 1 + 1 ≤ n) _auto✝
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 1 + 1) ⋯ hk = 0
-- Mathlib/Topology/MetricSpace/HolderNorm.lean
lemma MemHolder.coe_nnHolderNorm_eq_eHolderNorm
    {r : ℝ≥0} {f : X → Y} (hf : MemHolder r f) :
    (nnHolderNorm r f : ℝ≥0∞) = eHolderNorm r f

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
⊢ eHolderNorm r f ≠ ⊤

Tactic:
exact ne_of_lt <| lt_of_le_of_lt hf.holderWith.eHolderNorm_le <| coe_lt_top

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
⊢ ↑(nnHolderNorm r f) = eHolderNorm r f

Tactic:
rw [nnHolderNorm, coe_toNNReal]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
⊢ eHolderNorm r f ≠ ⊤
-- Mathlib/Data/Fin/Basic.lean
theorem castPred_le_iff {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ last n) :
    castPred i hi ≤ j ↔ i ≤ castSucc j

Proof state:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ i.castPred hi ≤ j ↔ i ≤ j.castSucc

Tactic:
rw [← castSucc_le_castSucc_iff, castSucc_castPred]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem sign_subtypeCongr {p : α → Prop} [DecidablePred p] (ep : Perm { a // p a })
    (en : Perm { a // ¬p a }) : sign (ep.subtypeCongr en) = sign ep * sign en

Proof state:
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
⊢ sign (ep.subtypeCongr en) = sign ep * sign en

Tactic:
simp [subtypeCongr]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem map_Iio (f : α ≃o β) (a : α) : map f (Iio a) = Iio (f a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
⊢ (map f) (Iio a) = Iio (f a)

Tactic:
ext

Result:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑((map f) (Iio a)) ↔ x✝ ∈ ↑(Iio (f a))

Proof state:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑((map f) (Iio a)) ↔ x✝ ∈ ↑(Iio (f a))

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive nsmul_add_sub_nsmul]
lemma pow_mul_pow_sub (a : M) (h : m ≤ n) : a ^ m * a ^ (n - m) = a ^ n

Proof state:
M : Type u_4
inst✝ : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ m * a ^ (n - m) = a ^ n

Tactic:
rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_eq_zero_iff {x : ℝ} : arcsin x = 0 ↔ x = 0

Proof state:
x : ℝ
⊢ arcsin x = 0 ↔ x = 0

Tactic:
simp [le_antisymm_iff]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem balanceR_eq_balance' {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Sized l)
    (sr : Sized r)
    (H : (∃ l', Raised (size l) l' ∧ BalancedSz l' (size r)) ∨
        ∃ r', Raised r' (size r) ∧ BalancedSz (size l) r') :
    @balanceR α l x r = balance' l x r

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ l.balanceR x r = l.balance' x r

Tactic:
rw [← dual_dual (balanceR l x r), dual_balanceR,
  balanceL_eq_balance' hr.dual hl.dual sr.dual sl.dual (balance_sz_dual H), ← dual_balance',
  dual_dual]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem cast_append_left (h : w + v = w' + v) (x : BitVec w) (y : BitVec v) :
    (x ++ y).cast h = x.cast (by omega) ++ y

Proof state:
w v w' : Nat
h : w + v = w' + v
x : BitVec w
y : BitVec v
⊢ BitVec.cast h (x ++ y) = BitVec.cast ⋯ x ++ y

Tactic:
ext

Result:
case pred
w v w' : Nat
h : w + v = w' + v
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w' + v
⊢ (BitVec.cast h (x ++ y)).getLsbD i✝ = (BitVec.cast ⋯ x ++ y).getLsbD i✝

Proof state:
w v w' : Nat
h : w + v = w' + v
x : BitVec w
y : BitVec v
⊢ w = w'

Tactic:
omega

Result:
no goals

Proof state:
case pred
w v w' : Nat
h : w + v = w' + v
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w' + v
⊢ (BitVec.cast h (x ++ y)).getLsbD i✝ = (BitVec.cast ⋯ x ++ y).getLsbD i✝

Tactic:
simp [getLsbD_append]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem isNormal_mul_right {a : Ordinal} (h : 0 < a) : IsNormal (a * ·) :=
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/12129): additional beta reduction needed
  ⟨fun b => by
      beta_reduce
      rw [mul_succ]
      simpa only [add_zero] using (add_lt_add_iff_left (a * b)).2 h,
    fun _ l _ => mul_le_of_limit l⟩

Proof state:
a : Ordinal.{u_4}
h : 0 < a
b : Ordinal.{u_4}
⊢ a * b < a * b + a

Tactic:
simpa only [add_zero] using (add_lt_add_iff_left (a * b)).2 h

Result:
no goals

Proof state:
a : Ordinal.{u_4}
h : 0 < a
b : Ordinal.{u_4}
⊢ a * b < a * succ b

Tactic:
rw [mul_succ]

Result:
a : Ordinal.{u_4}
h : 0 < a
b : Ordinal.{u_4}
⊢ a * b < a * b + a

Proof state:
a : Ordinal.{u_4}
h : 0 < a
b : Ordinal.{u_4}
⊢ (fun x => a * x) b < (fun x => a * x) (succ b)

Tactic:
beta_reduce

Result:
a : Ordinal.{u_4}
h : 0 < a
b : Ordinal.{u_4}
⊢ a * b < a * succ b
-- Mathlib/Order/WithBot.lean
lemma WithTop.le_ofDual_iff {x : WithBot α} {y : WithTop αᵒᵈ} :
    x ≤ WithTop.ofDual y ↔ y ≤ x.toDual

Proof state:
α : Type u_1
inst✝ : LE α
x : WithBot α
y : WithTop αᵒᵈ
⊢ x ≤ WithTop.ofDual y ↔ y ≤ WithBot.toDual x

Tactic:
cases x <;> cases y <;> simp [le_toDual]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem Filter.HasBasis.uniformEquicontinuous_iff_left {p : κ → Prop}
    {s : κ → Set (β × β)} {F : ι → β → α} (hβ : (𝓤 β).HasBasis p s) :
    UniformEquicontinuous F ↔
      ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x y, (x, y) ∈ s k → ∀ i, (F i x, F i y) ∈ U

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : (𝓤 β).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α, ∃ ia, p ia ∧ ∀ x ∈ s ia, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
simp only [Prod.forall]

Result:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : (𝓤 β).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α,
      ∃ ia, p ia ∧ ∀ (a b : β), (a, b) ∈ s ia → ((⇑ofFun ∘ swap F) a, (⇑ofFun ∘ swap F) b) ∈ UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : (𝓤 β).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α,
      ∃ ia, p ia ∧ ∀ (a b : β), (a, b) ∈ s ia → ((⇑ofFun ∘ swap F) a, (⇑ofFun ∘ swap F) b) ∈ UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : (𝓤 β).HasBasis p s
⊢ UniformEquicontinuous F ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
  hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)]

Result:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : (𝓤 β).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α, ∃ ia, p ia ∧ ∀ x ∈ s ia, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem le_mul_iff_one_le_left' [MulRightMono α]
    [MulRightReflectLE α] (a : α) {b : α} :
    a ≤ b * a ↔ 1 ≤ b :=
  Iff.trans (by rw [one_mul]) (mul_le_mul_iff_right a)

Proof state:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulRightMono α
inst✝ : MulRightReflectLE α
a b : α
⊢ a ≤ b * a ↔ 1 * a ≤ b * a

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_p_zpow (n : ℤ) : ‖(p : ℚ_[p]) ^ n‖ = (p : ℝ) ^ (-n)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
⊢ ‖↑p ^ n‖ = ↑p ^ (-n)

Tactic:
rw [norm_zpow, norm_p, zpow_neg, inv_zpow]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem ULift.isOpen_iff [TopologicalSpace X] {s : Set (ULift.{v} X)} :
    IsOpen s ↔ IsOpen (ULift.up ⁻¹' s)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set (ULift.{v, u} X)
⊢ IsOpen s ↔ IsOpen (up ⁻¹' s)

Tactic:
rw [ULift.topologicalSpace, ← Equiv.ulift_apply, ← Equiv.ulift.coinduced_symm, ← isOpen_coinduced]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem subtypeDomain_eq_iff_forall {f g : α →₀ M} :
    f.subtypeDomain p = g.subtypeDomain p ↔ ∀ x, p x → f x = g x

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
f g : α →₀ M
⊢ subtypeDomain p f = subtypeDomain p g ↔ ∀ (x : α), p x → f x = g x

Tactic:
simp_rw [DFunLike.ext_iff, subtypeDomain_apply, Subtype.forall]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma isUnit_prime_iff_not_dvd {n p : ℕ} (hp : p.Prime) : IsUnit (p : ZMod n) ↔ ¬p ∣ n

Proof state:
n p : ℕ
hp : Nat.Prime p
⊢ IsUnit ↑p ↔ ¬p ∣ n

Tactic:
rw [isUnit_iff_coprime, Nat.Prime.coprime_iff_not_dvd hp]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem bind₁_X_left : bind₁ (X : σ → MvPolynomial σ R) = AlgHom.id R _

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
⊢ bind₁ X = AlgHom.id R (MvPolynomial σ R)

Tactic:
ext1 i

Result:
case hf
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (bind₁ X) (X i) = (AlgHom.id R (MvPolynomial σ R)) (X i)

Proof state:
case hf
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (bind₁ X) (X i) = (AlgHom.id R (MvPolynomial σ R)) (X i)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_self_left  : ∀ (a b : Bool), (a && (a && b)) = (a && b)

Proof state:
⊢ ∀ (a b : Bool), (a && (a && b)) = (a && b)

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty

Proof state:
α : Type u_1
l : List α
⊢ l.toArray.isEmpty = l.isEmpty

Tactic:
cases l <;> simp [Array.isEmpty]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem sub_mem_closedBall (p : Seminorm 𝕜 E) (x₁ x₂ y : E) (r : ℝ) :
    x₁ - x₂ ∈ p.closedBall y r ↔ x₁ ∈ p.closedBall (x₂ + y) r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x₁ x₂ y : E
r : ℝ
⊢ x₁ - x₂ ∈ p.closedBall y r ↔ x₁ ∈ p.closedBall (x₂ + y) r

Tactic:
simp_rw [mem_closedBall, sub_sub]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem isIdempotentElem_apply_one_iff {f : Module.End R R} :
    IsIdempotentElem (f 1) ↔ IsIdempotentElem f

Proof state:
R : Type u_1
inst✝ : Semiring R
f : Module.End R R
h : f (f 1) = f 1
r : R
⊢ f (f r) = f r

Tactic:
rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ f (f 1) = f 1 ↔ ∀ (x : R), (f * f) x = f x

Tactic:
simp_rw [mul_apply]

Result:
R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ f (f 1) = f 1 ↔ ∀ (x : R), f (f x) = f x

Proof state:
R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ IsIdempotentElem (f 1) ↔ IsIdempotentElem f

Tactic:
rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, IsIdempotentElem,
  LinearMap.ext_iff]

Result:
R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ f (f 1) = f 1 ↔ ∀ (x : R), (f * f) x = f x
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma baseChange_polynomialX : (W'.baseChange B).toAffine.polynomialX =
    (W'.baseChange A).toAffine.polynomialX.map (mapRingHom f)

Proof state:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (baseChange W' B).toAffine.polynomialX = Polynomial.map (mapRingHom ↑f) (baseChange W' A).toAffine.polynomialX

Tactic:
rw [← map_polynomialX, map_baseChange]

Result:
no goals
-- Mathlib/Order/MinMax.lean
theorem min_lt_min_right_iff : min a b < min a c ↔ b < c ∧ b < a

Proof state:
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ a ⊓ b < a ⊓ c ↔ b < c ∧ b < a

Tactic:
simp_rw [min_comm a, min_lt_min_left_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Int.lean
theorem testBit_ofBits (f : Fin n → Bool) :
    (ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else decide (ofBits f < 0)

Proof state:
n i : Nat
f : Fin n → Bool
⊢ (ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else decide (ofBits f < 0)

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem tensor_id_comp_id_tensor (f : W ⟶ X) (g : Y ⟶ Z) : (g ⊗ 𝟙 W) ≫ (𝟙 Z ⊗ f) = g ⊗ f

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ (g ⊗ 𝟙 W) ≫ (𝟙 Z ⊗ f) = g ⊗ f

Tactic:
rw [← tensor_comp]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ g ≫ 𝟙 Z ⊗ 𝟙 W ≫ f = g ⊗ f

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ g ≫ 𝟙 Z ⊗ 𝟙 W ≫ f = g ⊗ f

Tactic:
simp

Result:
no goals