harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem dist_eq_zero_of_not_reachable (h : ¬G.Reachable u v) : G.dist u v = 0

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬G.Reachable u v
⊢ G.dist u v = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem pow_prod_atom (a : R) (b) : a ^ b = (a + 0) ^ b * (nat_lit 1).rawCast

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
b : ℕ
⊢ a ^ b = (a + 0) ^ b * Nat.rawCast 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_affine_Ioc {a : α} (h : 0 < a) (b c d : α) :
    (a * · + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
h : 0 < a
b c d : α
this : (fun x => x + b) '' ((fun x => a * x) '' Ioc c d) = Ioc (a * c + b) (a * d + b)
⊢ (fun x => a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)

Tactic:
rwa [Set.image_image] at this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
h : 0 < a
b c d : α
⊢ (fun x => x + b) '' ((fun x => a * x) '' Ioc c d) = Ioc (a * c + b) (a * d + b)

Tactic:
rw [image_mul_left_Ioc h, image_add_const_Ioc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_mkVector_of_pos (h : p a) :
    find? p (mkVector n a) = if n = 0 then none else some a

Proof state:
α✝ : Type
p : α✝ → Bool
n : Nat
a : α✝
h : p a = true
⊢ find? p (mkVector n a) = if n = 0 then none else some a

Tactic:
simp [find?_mkVector, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem or_eq_decide (p q : Prop) [dpq : Decidable (p ∨ q)] [dp : Decidable p] [dq : Decidable q] :
    (p || q) = decide (p ∨ q)

Proof state:
p q : Prop
dpq : Decidable (p ∨ q)
dp : Decidable p
dq : Decidable q
⊢ (decide p || decide q) = decide (p ∨ q)

Tactic:
cases dp with | _ p => simp [p]

Result:
no goals

Proof state:
case isTrue
p✝ q : Prop
dpq : Decidable (p✝ ∨ q)
dq : Decidable q
p : p✝
⊢ (decide p✝ || decide q) = decide (p✝ ∨ q)

Tactic:
simp [p]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem uniformEquicontinuous_iff_uniformContinuous {F : ι → β → α} :
    UniformEquicontinuous F ↔ UniformContinuous (ofFun ∘ Function.swap F : β → ι →ᵤ α)

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
⊢ UniformEquicontinuous F ↔ UniformContinuous (⇑ofFun ∘ swap F)

Tactic:
rw [UniformContinuous, (UniformFun.hasBasis_uniformity ι α).tendsto_right_iff]

Result:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
⊢ UniformEquicontinuous F ↔
    ∀ i ∈ 𝓤 α, ∀ᶠ (x : β × β) in 𝓤 β, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ UniformFun.gen ι α i

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
⊢ UniformEquicontinuous F ↔
    ∀ i ∈ 𝓤 α, ∀ᶠ (x : β × β) in 𝓤 β, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ UniformFun.gen ι α i

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem or_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a ∨ b) = True

Proof state:
a b : Prop
h : b = True
⊢ (a ∨ b) = True

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Pi.lean
lemma Pi.uniformSpace_eq :
    Pi.uniformSpace α = ⨅ i, UniformSpace.comap (eval i) (U i)

Proof state:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
⊢ uniformSpace α = ⨅ i, UniformSpace.comap (eval i) (U i)

Tactic:
ext : 1

Result:
case h
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
⊢ 𝓤 ((i : ι) → α i) = 𝓤 ((i : ι) → α i)

Proof state:
case h
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
⊢ 𝓤 ((i : ι) → α i) = 𝓤 ((i : ι) → α i)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
/-- Self-adjoint elements commute if and only if their product is self-adjoint. -/
lemma commute_iff {R : Type*} [Mul R] [StarMul R] {x y : R}
    (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : Commute x y ↔ IsSelfAdjoint (x * y)

Proof state:
case refine_1
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : Commute x y
⊢ IsSelfAdjoint (x * y)

Tactic:
rw [isSelfAdjoint_iff, star_mul, hx.star_eq, hy.star_eq, h.eq]

Result:
no goals

Proof state:
case refine_2
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : IsSelfAdjoint (x * y)
⊢ Commute x y

Tactic:
simpa only [star_mul, hx.star_eq, hy.star_eq] using h.symm

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ Commute x y ↔ IsSelfAdjoint (x * y)

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

Result:
case refine_1
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : Commute x y
⊢ IsSelfAdjoint (x * y)

case refine_2
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : IsSelfAdjoint (x * y)
⊢ Commute x y
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem natCast_mul_eq_nsmul (x : ℝ) (n : ℕ) : ↑((n : ℝ) * x) = n • (↑x : Angle)

Proof state:
x : ℝ
n : ℕ
⊢ ↑(↑n * x) = n • ↑x

Tactic:
simpa only [nsmul_eq_mul] using coeHom.map_nsmul x n

Result:
no goals
-- Mathlib/FieldTheory/Normal/Closure.lean
lemma normal_iff_forall_map_le : Normal F K ↔ ∀ σ : L →ₐ[F] L, K.map σ ≤ K

Proof state:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
⊢ Normal F ↥K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K

Tactic:
rw [normal_iff_normalClosure_le, normalClosure_def', iSup_le_iff]

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
lemma mul_eq_add : p * q = p + q

Proof state:
p q : ℝ≥0
h : p.IsConjExponent q
⊢ p * q = p + q

Tactic:
simpa only [← NNReal.coe_mul, ← NNReal.coe_add, NNReal.coe_inj] using h.coe.mul_eq_add

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem hasPrev : ∀ {it}, ValidFor l r it → (it.hasPrev ↔ l ≠ [])
  | it, h => by simp [Iterator.hasPrev, h.pos, Nat.pos_iff_ne_zero]

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ it.hasPrev = true ↔ l ≠ []

Tactic:
simp [Iterator.hasPrev, h.pos, Nat.pos_iff_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem snd_lt_of_mem_zipIdx {x : α × Nat} {l : Vector α n} {k : Nat} (h : x ∈ l.zipIdx k) :
    x.2 < n + k

Proof state:
α : Type u_1
n : Nat
x : α × Nat
l : Vector α n
k : Nat
h : x ∈ l.zipIdx k
⊢ x.snd < n + k

Tactic:
simpa [Nat.add_comm] using snd_lt_add_of_mem_zipIdx h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem toFinsupp_C_mul_X (a : R) : Polynomial.toFinsupp (C a * X) = Finsupp.single 1 a

Proof state:
R : Type u
inst✝ : Semiring R
a : R
⊢ (C a * X).toFinsupp = Finsupp.single 1 a

Tactic:
rw [C_mul_X_eq_monomial, toFinsupp_monomial]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem reverse_cons {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
    (cons h p).reverse = p.reverse.append (cons (G.symm h) nil)

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).reverse = p.reverse.append (cons ⋯ nil)

Tactic:
simp [reverse]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
@[to_additive] lemma monovaryOn_inv : MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedCommGroup α
inst✝ : OrderedCommGroup β
s : Set ι
f : ι → α
g : ι → β
⊢ MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousWithinAt_update_same [DecidableEq α] {y : β} :
    ContinuousWithinAt (update f x y) s x ↔ Tendsto f (𝓝[s \ {x}] x) (𝓝 y) :=
  calc
    ContinuousWithinAt (update f x y) s x ↔ Tendsto (update f x y) (𝓝[s \ {x}] x) (𝓝 y)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
x : α
inst✝ : DecidableEq α
y : β
⊢ ContinuousWithinAt (update f x y) s x ↔ Tendsto (update f x y) (𝓝[s \ {x}] x) (𝓝 y)

Tactic:
rw [← continuousWithinAt_diff_self, ContinuousWithinAt, update_self]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem erase_eq_empty_iff (s : Finset α) (a : α) : s.erase a = ∅ ↔ s = ∅ ∨ s = {a}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s.erase a = ∅ ↔ s = ∅ ∨ s = {a}

Tactic:
rw [← sdiff_singleton_eq_erase, sdiff_eq_empty_iff_subset, subset_singleton_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
lemma dist_top [DecidableEq V] : (⊤ : SimpleGraph V).dist u v = (if u = v then 0 else 1)

Proof state:
V : Type u_1
u v : V
inst✝ : DecidableEq V
⊢ ⊤.dist u v = if u = v then 0 else 1

Tactic:
by_cases h : u = v <;> simp [h]

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem Lp_add_le_of_nonneg (hp : 1 ≤ p) (hf : ∀ i ∈ s, 0 ≤ f i) (hg : ∀ i ∈ s, 0 ≤ g i) :
    (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤
      (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
convert Lp_add_le s f g hp using 2 <;> [skip;congr 1;congr 1] <;> apply sum_congr rfl <;>
    intro i hi <;>
  simp only [abs_of_nonneg, hf i hi, hg i hi, add_nonneg]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get?_set_eq_of_lt (a : α) {n} {l : List α} (h : n < length l) :
    (set l n a).get? n = some a

Proof state:
α : Type u_1
a : α
n : Nat
l : List α
h : n < l.length
⊢ Function.const α a <$> some l[n] = some a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
a : α
n : Nat
l : List α
h : n < l.length
⊢ (l.set n a).get? n = some a

Tactic:
rw [get?_eq_getElem?, getElem?_set_self', getElem?_eq_getElem h]

Result:
α : Type u_1
a : α
n : Nat
l : List α
h : n < l.length
⊢ Function.const α a <$> some l[n] = some a
-- Mathlib/Data/Rat/Floor.lean
theorem round_cast (x : ℚ) : round (x : α) = round x

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
⊢ ↑(x + 1 / 2) = ↑x + 1 / 2

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
this : ↑(x + 1 / 2) = ↑x + 1 / 2
⊢ round ↑x = round x

Tactic:
rw [round_eq, round_eq, ← this, floor_cast]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
⊢ round ↑x = round x

Tactic:
have : ((x + 1 / 2 : ℚ) : α) = x + 1 / 2 := by simp

Result:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
this : ↑(x + 1 / 2) = ↑x + 1 / 2
⊢ round ↑x = round x
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.nonempty_support {g : Perm α} (hg : g.IsCycle) :
    g.support.Nonempty

Proof state:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
⊢ g.support.Nonempty

Tactic:
rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty_iff]

Result:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
⊢ ¬g = 1

Proof state:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
⊢ ¬g = 1

Tactic:
exact IsCycle.ne_one hg

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem sum_le_iSup_lift {ι : Type u}
    (f : ι → Cardinal.{max u v}) : sum f ≤ Cardinal.lift #ι * iSup f

Proof state:
ι : Type u
f : ι → Cardinal.{max u v}
⊢ sum f ≤ lift.{v, u} #ι * iSup f

Tactic:
rw [← (iSup f).lift_id, ← lift_umax, lift_umax.{max u v, u}, ← sum_const]

Result:
ι : Type u
f : ι → Cardinal.{max u v}
⊢ sum f ≤ sum fun x => iSup f

Proof state:
ι : Type u
f : ι → Cardinal.{max u v}
⊢ sum f ≤ sum fun x => iSup f

Tactic:
exact sum_le_sum _ _ (le_ciSup <| bddAbove_of_small _)

Result:
no goals
-- Mathlib/Data/Int/CharZero.lean
theorem cast_div_ofNat_charZero {k : Type*} [DivisionRing k] [CharZero k] {m n : ℕ}
    (n_dvd : n ∣ m) : (((m : ℤ) / (n : ℤ) : ℤ) : k) = m / n

Proof state:
k : Type u_3
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℕ
n_dvd : n ∣ m
⊢ ↑(↑m / ↑n) = ↑m / ↑n

Tactic:
rw [cast_div_charZero (Int.ofNat_dvd.mpr n_dvd), cast_natCast, cast_natCast]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem add_comm' (x y : LocalizedModule S M) : x + y = y + x :=
  LocalizedModule.induction_on₂ (fun m m' s s' => by rw [mk_add_mk, mk_add_mk, add_comm, mul_comm])
    x y

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : LocalizedModule S M
m m' : M
s s' : ↥S
⊢ mk m s + mk m' s' = mk m' s' + mk m s

Tactic:
rw [mk_add_mk, mk_add_mk, add_comm, mul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[ext]
lemma hom_ext₁ {F G : ComposableArrows C 1} {φ φ' : F ⟶ G}
    (h₀ : app' φ 0 = app' φ' 0) (h₁ : app' φ 1 = app' φ' 1) :
    φ = φ'

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : ComposableArrows C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 ⋯ = app' φ' 0 ⋯
h₁ : app' φ 1 ⋯ = app' φ' 1 ⋯
i : Fin (1 + 1)
⊢ φ.app 0 = φ'.app 0

Tactic:
exact h₀

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : ComposableArrows C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 ⋯ = app' φ' 0 ⋯
h₁ : app' φ 1 ⋯ = app' φ' 1 ⋯
⊢ φ = φ'

Tactic:
ext i

Result:
case w.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : ComposableArrows C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 ⋯ = app' φ' 0 ⋯
h₁ : app' φ 1 ⋯ = app' φ' 1 ⋯
i : Fin (1 + 1)
⊢ φ.app i = φ'.app i

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : ComposableArrows C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 ⋯ = app' φ' 0 ⋯
h₁ : app' φ 1 ⋯ = app' φ' 1 ⋯
i : Fin (1 + 1)
⊢ φ.app 1 = φ'.app 1

Tactic:
exact h₁

Result:
no goals

Proof state:
case w.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : ComposableArrows C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 ⋯ = app' φ' 0 ⋯
h₁ : app' φ 1 ⋯ = app' φ' 1 ⋯
i : Fin (1 + 1)
⊢ φ.app i = φ'.app i

Tactic:
match i with
  | 0 => exact h₀
  | 1 => exact h₁

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
lemma le_induce_union_left : G'.induce s ≤ G'.induce (s ∪ s')

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ G'.induce s ≤ G'.induce (s ∪ s')

Tactic:
exact (sup_le_iff.mp le_induce_union).1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem lex_eq_true_iff_lex [DecidableEq α] (lt : α → α → Bool) :
    lex l₁ l₂ lt = true ↔ Lex (fun x y => lt x y) l₁ l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
lt : α → α → Bool
⊢ l₁.lex l₂ lt = true ↔ Lex (fun x y => lt x y = true) l₁ l₂

Tactic:
simp [lex_eq_decide_lex]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_ofList_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! (ofList 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! (ofList l) k' = v

Tactic:
simp_to_raw using Raw₀.Const.get!_insertMany_empty_list_of_mem

Result:
no goals
-- Mathlib/Algebra/Order/Round.lean
theorem abs_sub_round_div_natCast_eq {m n : ℕ} :
    |(m : α) / n - round ((m : α) / n)| = ↑(min (m % n) (n - m % n)) / n

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
⊢ |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(m % n ⊓ (n - m % n)) / ↑n

Tactic:
have hn' : 0 < (n : α) := by
  norm_cast

Result:
case inr
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(m % n ⊓ (n - m % n)) / ↑n

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
⊢ 0 < ↑n

Tactic:
norm_cast

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m : ℕ
⊢ |↑m / ↑0 - ↑(round (↑m / ↑0))| = ↑(m % 0 ⊓ (0 - m % 0)) / ↑0

Tactic:
simp

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(m % n ⊓ (n - m % n)) / ↑n

Tactic:
rw [abs_sub_round_eq_min, Nat.cast_min, ← min_div_div_right hn'.le,
  fract_div_natCast_eq_div_natCast_mod, Nat.cast_sub (m.mod_lt hn).le, sub_div, div_self hn'.ne']

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m n : ℕ
⊢ |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(m % n ⊓ (n - m % n)) / ↑n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m : ℕ
⊢ |↑m / ↑0 - ↑(round (↑m / ↑0))| = ↑(m % 0 ⊓ (0 - m % 0)) / ↑0

case inr
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
⊢ |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(m % n ⊓ (n - m % n)) / ↑n
-- Mathlib/Data/Nat/Lattice.lean
theorem sInf_mem {s : Set ℕ} (h : s.Nonempty) : sInf s ∈ s

Proof state:
s : Set ℕ
h : s.Nonempty
⊢ sInf s ∈ s

Tactic:
rw [Nat.sInf_def h]

Result:
s : Set ℕ
h : s.Nonempty
⊢ Nat.find h ∈ s

Proof state:
s : Set ℕ
h : s.Nonempty
⊢ sInf s ∈ s

Tactic:
classical
rw [Nat.sInf_def h]
exact Nat.find_spec h

Result:
no goals

Proof state:
s : Set ℕ
h : s.Nonempty
⊢ Nat.find h ∈ s

Tactic:
exact Nat.find_spec h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
lemma nextCoeff_eq_zero :
    p.nextCoeff = 0 ↔ p.natDegree = 0 ∨ 0 < p.natDegree ∧ p.coeff (p.natDegree - 1) = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬p.natDegree = 0 → p.coeff (p.natDegree - 1) = 0 ↔ ¬p.natDegree = 0 → ¬p.natDegree = 0 ∧ p.coeff (p.natDegree - 1) = 0

Tactic:
aesop

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.nextCoeff = 0 ↔ p.natDegree = 0 ∨ 0 < p.natDegree ∧ p.coeff (p.natDegree - 1) = 0

Tactic:
simp [nextCoeff, or_iff_not_imp_left, pos_iff_ne_zero]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬p.natDegree = 0 → p.coeff (p.natDegree - 1) = 0 ↔ ¬p.natDegree = 0 → ¬p.natDegree = 0 ∧ p.coeff (p.natDegree - 1) = 0
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Iic_iff_integrableOn_Iio :
    IntegrableOn f (Iic b) μ ↔ IntegrableOn f (Iio b) μ :=
  integrableOn_Iic_iff_integrableOn_Iio' (by rw [measure_singleton]; exact ENNReal.zero_ne_top)

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤

Tactic:
exact ENNReal.zero_ne_top

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
b : α
inst✝ : NoAtoms μ
⊢ μ {b} ≠ ⊤

Tactic:
rw [measure_singleton]

Result:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem repeat_one (a : Fin n → α) : Fin.repeat 1 a = a ∘ Fin.cast (Nat.one_mul _)

Proof state:
case h
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
i : Fin n
⊢ «repeat» 1 a (Fin.cast ⋯ i) = (a ∘ Fin.cast h) (Fin.cast ⋯ i)

Tactic:
simp [modNat, Nat.mod_eq_of_lt i.is_lt]

Result:
no goals

Proof state:
case h
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
⊢ ∀ (x : Fin (1 * n)), «repeat» 1 a x = (a ∘ Fin.cast h) x

Tactic:
rw [(Fin.rightInverse_cast h.symm).surjective.forall]

Result:
case h
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
⊢ ∀ (x : Fin n), «repeat» 1 a (Fin.cast ⋯ x) = (a ∘ Fin.cast h) (Fin.cast ⋯ x)

Proof state:
case h
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
⊢ ∀ (x : Fin n), «repeat» 1 a (Fin.cast ⋯ x) = (a ∘ Fin.cast h) (Fin.cast ⋯ x)

Tactic:
intro i

Result:
case h
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
i : Fin n
⊢ «repeat» 1 a (Fin.cast ⋯ i) = (a ∘ Fin.cast h) (Fin.cast ⋯ i)

Proof state:
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
⊢ «repeat» 1 a = a ∘ Fin.cast h

Tactic:
apply funext

Result:
case h
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
⊢ ∀ (x : Fin (1 * n)), «repeat» 1 a x = (a ∘ Fin.cast h) x

Proof state:
n : ℕ
α : Sort u_1
a : Fin n → α
⊢ «repeat» 1 a = a ∘ Fin.cast ⋯

Tactic:
generalize_proofs h

Result:
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
⊢ «repeat» 1 a = a ∘ Fin.cast h
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma map_comp_right (κ : Kernel α β) {f : β → γ} (hf : Measurable f) {g : γ → δ}
    (hg : Measurable g) : κ.map (g ∘ f) = (κ.map f).map g

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
hf : Measurable f
g : γ → δ
hg : Measurable g
x : α
⊢ (κ.map (g ∘ f)) x = ((κ.map f).map g) x

Tactic:
rw [map_apply _ hg, map_apply _ hf, Measure.map_map hg hf, ← map_apply _ (hg.comp hf)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
hf : Measurable f
g : γ → δ
hg : Measurable g
⊢ κ.map (g ∘ f) = (κ.map f).map g

Tactic:
ext1 x

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
hf : Measurable f
g : γ → δ
hg : Measurable g
x : α
⊢ (κ.map (g ∘ f)) x = ((κ.map f).map g) x
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
private lemma continuousAt_mul_coe_coe (a b : ℝ) :
    ContinuousAt (fun p : EReal × EReal ↦ p.1 * p.2) (a, b)

Proof state:
a b : ℝ
⊢ ContinuousAt (fun p => p.1 * p.2) (↑a, ↑b)

Tactic:
simp [ContinuousAt, EReal.nhds_coe_coe, ← EReal.coe_mul, Filter.tendsto_map'_iff,
  Function.comp_def, EReal.tendsto_coe, tendsto_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem unit_conjugateEquiv_symm (α : R₁ ⟶ R₂) (c : C) :
    adj₁.unit.app _ ≫ α.app _ =
      adj₂.unit.app c ≫ R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app _)

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
c : C
⊢ adj₁.unit.app c ≫ α.app (L₁.obj c) = adj₂.unit.app c ≫ R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app c)

Tactic:
conv_lhs => rw [← (conjugateEquiv adj₁ adj₂).right_inv α]

Result:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
c : C
⊢ adj₁.unit.app c ≫ ((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c) =
    adj₂.unit.app c ≫ R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app c)

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
c : C
⊢ adj₁.unit.app c ≫ ((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c) =
    adj₂.unit.app c ≫ R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app c)

Tactic:
exact (unit_conjugateEquiv adj₁ adj₂ ((conjugateEquiv adj₁ adj₂).symm α) c)

Result:
no goals