harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/TMToPartrec.lean
theorem supports_singleton {S q} : Supports {q} S ↔ TM2.SupportsStmt S (tr q)

Proof state:
S : Finset Λ'
q : Λ'
⊢ Supports {q} S ↔ TM2.SupportsStmt S (tr q)

Tactic:
simp [Supports]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem norm_fderivWithin_iteratedFDerivWithin {n : ℕ} :
    ‖fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x‖ =
      ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ
⊢ ‖fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x‖ = ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖

Tactic:
rw [iteratedFDerivWithin_succ_eq_comp_left, comp_apply, LinearIsometryEquiv.norm_map]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
@[simp] lemma truncatedInf_singleton (b a : α) : truncatedInf {b} a = if b ≤ a then b else ⊥

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
b a : α
⊢ {b}.truncatedInf a = if b ≤ a then b else ⊥

Tactic:
simp only [truncatedInf, coe_singleton, upperClosure_singleton, UpperSet.mem_Ici_iff,
  filter_congr_decidable, id_eq]

Result:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
b a : α
⊢ (if h : b ≤ a then (filter (fun b => b ≤ a) {b}).inf' ⋯ fun x => x else ⊥) = if b ≤ a then b else ⊥

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
b a : α
⊢ (if h : b ≤ a then (filter (fun b => b ≤ a) {b}).inf' ⋯ fun x => x else ⊥) = if b ≤ a then b else ⊥

Tactic:
split_ifs <;> simp [Finset.filter_true_of_mem, *]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem nonnegg_comm {c d : ℕ} {x y : ℤ} : Nonnegg c d x y = Nonnegg d c y x

Proof state:
c d : ℕ
x y : ℤ
⊢ Nonnegg c d x y = Nonnegg d c y x

Tactic:
cases x <;> cases y <;> rfl

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
@[simp, norm_cast]
lemma ofReal_nonpos {x : ℝ} : (x : K) ≤ 0 ↔ x ≤ 0

Proof state:
K : Type u_1
inst✝ : RCLike K
x : ℝ
⊢ ↑x ≤ 0 ↔ x ≤ 0

Tactic:
rw [← ofReal_zero, ofReal_le_ofReal]

Result:
no goals
-- Mathlib/Analysis/Complex/Periodic.lean
theorem norm_qParam (z : ℂ) : ‖𝕢 h z‖ = Real.exp (-2 * π * im z / h)

Proof state:
h : ℝ
z : ℂ
⊢ ‖𝕢 h z‖ = rexp (-2 * π * z.im / h)

Tactic:
simp only [qParam, norm_exp, div_ofReal_re, mul_re, re_ofNat, ofReal_re, im_ofNat, ofReal_im,
  mul_zero, sub_zero, I_re, mul_im, zero_mul, add_zero, I_im, mul_one, sub_self, zero_sub,
  neg_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem zipIdx_succ (l : Array α) (n : Nat) :
    l.zipIdx (n + 1) = (l.zipIdx n).map (fun ⟨a, i⟩ => (a, i + 1))

Proof state:
case mk
α : Type u_1
n : Nat
toList✝ : List α
⊢ { toList := toList✝ }.zipIdx (n + 1) =
    map
      (fun x =>
        match x with
        | (a, i) => (a, i + 1))
      ({ toList := toList✝ }.zipIdx n)

Tactic:
simp [List.zipIdx_succ]

Result:
no goals

Proof state:
α : Type u_1
l : Array α
n : Nat
⊢ l.zipIdx (n + 1) =
    map
      (fun x =>
        match x with
        | (a, i) => (a, i + 1))
      (l.zipIdx n)

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
toList✝ : List α
⊢ { toList := toList✝ }.zipIdx (n + 1) =
    map
      (fun x =>
        match x with
        | (a, i) => (a, i + 1))
      ({ toList := toList✝ }.zipIdx n)
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem lintegral_coe_le_coe_iff_integral_le {f : α → ℝ≥0} (hfi : Integrable (fun x => (f x : ℝ)) μ)
    {b : ℝ≥0} : ∫⁻ a, f a ∂μ ≤ b ↔ ∫ a, (f a : ℝ) ∂μ ≤ b

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (fun x => ↑(f x)) μ
b : ℝ≥0
⊢ ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b ↔ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b

Tactic:
rw [lintegral_coe_eq_integral f hfi, ENNReal.ofReal, ENNReal.coe_le_coe,
  Real.toNNReal_le_iff_le_coe]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem _root_.Wbtw.oangle_sign_eq_of_ne_right {p₁ p₂ p₃ : P} (p₄ : P) (h : Wbtw ℝ p₁ p₂ p₃)
    (hne : p₂ ≠ p₃) : (∡ p₂ p₄ p₃).sign = (∡ p₁ p₄ p₃).sign

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Wbtw ℝ p₁ p₂ p₃
hne : p₂ ≠ p₃
⊢ (∡ p₂ p₄ p₃).sign = (∡ p₁ p₄ p₃).sign

Tactic:
simp_rw [oangle_rev p₃, Real.Angle.sign_neg, h.symm.oangle_sign_eq_of_ne_left _ hne.symm]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem coe_sumPiEquivProdPi_symm (α : δ ⊕ δ' → Type*) [∀ i, MeasurableSpace (α i)] :
    ⇑(MeasurableEquiv.sumPiEquivProdPi α).symm = (Equiv.sumPiEquivProdPi α).symm

Proof state:
δ : Type u_4
δ' : Type u_5
α : δ ⊕ δ' → Type u_8
inst✝ : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ ⇑(sumPiEquivProdPi α).symm = ⇑(Equiv.sumPiEquivProdPi α).symm

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem val_add_eq_of_add_lt {n : ℕ} {a b : Fin n} (huv : a.val + b.val < n) :
    (a + b).val = a.val + b.val

Proof state:
n : ℕ
a b : Fin n
huv : ↑a + ↑b < n
⊢ ↑(a + b) = ↑a + ↑b

Tactic:
rw [val_add]

Result:
n : ℕ
a b : Fin n
huv : ↑a + ↑b < n
⊢ (↑a + ↑b) % n = ↑a + ↑b

Proof state:
n : ℕ
a b : Fin n
huv : ↑a + ↑b < n
⊢ (↑a + ↑b) % n = ↑a + ↑b

Tactic:
simp [Nat.mod_eq_of_lt huv]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem glued_cover_cocycle (x y z : 𝒰.J) :
    gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y = 𝟙 _

Proof state:
case h₁
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) =
    pullback.snd (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z))

Tactic:
apply glued_cover_cocycle_snd

Result:
no goals

Proof state:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y =
    𝟙 (pullback (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)))

Tactic:
apply pullback.hom_ext <;> simp_rw [Category.id_comp, Category.assoc]

Result:
case h₀
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) =
    pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z))

case h₁
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) =
    pullback.snd (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z))

Proof state:
case h₀
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) =
    pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z))

Tactic:
apply glued_cover_cocycle_fst

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem Submodule.IsPrincipal.map (f : M →ₗ[R] N) {S : Submodule R M}
    (hI : IsPrincipal S) : IsPrincipal (map f S) :=
  ⟨⟨f (IsPrincipal.generator S), by
      rw [← Set.image_singleton, ← map_span, span_singleton_generator]⟩⟩

Proof state:
R : Type u
M : Type v
N : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
S : Submodule R M
hI : S.IsPrincipal
⊢ Submodule.map f S = span R {f (generator S)}

Tactic:
rw [← Set.image_singleton, ← map_span, span_singleton_generator]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem exists_mul_le_one_eqOn_ge (f : C(X, ℝ≥0)) {c : ℝ≥0} (hc : 0 < c) :
    ∃ g : C(X, ℝ≥0), (∀ x : X, (g * f) x ≤ 1) ∧ {x : X | c ≤ f x}.EqOn (g * f) 1 :=
  ⟨{  toFun := (f ⊔ const X c)⁻¹
      continuous_toFun :=
        ((map_continuous f).sup <| map_continuous _).inv₀ fun _ => (hc.trans_le le_sup_right).ne' },
    fun x =>
    (inv_mul_le_iff₀ (hc.trans_le le_sup_right)).mpr ((mul_one (f x ⊔ c)).symm ▸ le_sup_left),
    fun x hx => by
    simpa only [coe_const, mul_apply, coe_mk, Pi.inv_apply, Pi.sup_apply,
      Function.const_apply, sup_eq_left.mpr (Set.mem_setOf.mp hx), ne_eq, Pi.one_apply]
      using inv_mul_cancel₀ (hc.trans_le hx).ne' ⟩

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
f : C(X, ℝ≥0)
c : ℝ≥0
hc : 0 < c
x : X
hx : x ∈ {x | c ≤ f x}
⊢ ({ toFun := (⇑f ⊔ ⇑(const X c))⁻¹, continuous_toFun := ⋯ } * f) x = 1 x

Tactic:
simpa only [coe_const, mul_apply, coe_mk, Pi.inv_apply, Pi.sup_apply,
  Function.const_apply, sup_eq_left.mpr (Set.mem_setOf.mp hx), ne_eq, Pi.one_apply]
  using inv_mul_cancel₀ (hc.trans_le hx).ne'

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_mul (s : Set α) (f g : α → M) :
    (mulIndicator s fun a => f a * g a) = fun a => mulIndicator s f a * mulIndicator s g a

Proof state:
case h
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
⊢ s.mulIndicator (fun a => f a * g a) x✝ = s.mulIndicator f x✝ * s.mulIndicator g x✝

Tactic:
simp only [mulIndicator]

Result:
case h
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
⊢ (if x✝ ∈ s then f x✝ * g x✝ else 1) = (if x✝ ∈ s then f x✝ else 1) * if x✝ ∈ s then g x✝ else 1

Proof state:
case h
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
⊢ (if x✝ ∈ s then f x✝ * g x✝ else 1) = (if x✝ ∈ s then f x✝ else 1) * if x✝ ∈ s then g x✝ else 1

Tactic:
split_ifs

Result:
case pos
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
h✝ : x✝ ∈ s
⊢ f x✝ * g x✝ = f x✝ * g x✝

case neg
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
h✝ : x✝ ∉ s
⊢ 1 = 1 * 1

Proof state:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
s : Set α
f g : α → M
⊢ (s.mulIndicator fun a => f a * g a) = fun a => s.mulIndicator f a * s.mulIndicator g a

Tactic:
funext

Result:
case h
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
⊢ s.mulIndicator (fun a => f a * g a) x✝ = s.mulIndicator f x✝ * s.mulIndicator g x✝

Proof state:
case neg
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
h✝ : x✝ ∉ s
⊢ 1 = 1 * 1

Tactic:
rw [mul_one]

Result:
no goals

Proof state:
case pos
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
h✝ : x✝ ∈ s
⊢ f x✝ * g x✝ = f x✝ * g x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem digits_of_lt (b x : ℕ) (hx : x ≠ 0) (hxb : x < b) : digits b x = [x]

Proof state:
b x : ℕ
hx : x ≠ 0
hxb : x < b
⊢ b.digits x = [x]

Tactic:
rcases exists_eq_succ_of_ne_zero hx with ⟨x, rfl⟩

Result:
case intro
b x : ℕ
hx : x.succ ≠ 0
hxb : x.succ < b
⊢ b.digits x.succ = [x.succ]

Proof state:
case intro.intro
x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
⊢ (b + succ 1).digits x.succ = [x.succ]

Tactic:
rw [digits_add_two_add_one, div_eq_of_lt hxb, digits_zero, mod_eq_of_lt hxb]

Result:
no goals

Proof state:
case intro
b x : ℕ
hx : x.succ ≠ 0
hxb : x.succ < b
⊢ b.digits x.succ = [x.succ]

Tactic:
rcases Nat.exists_eq_add_of_le' ((Nat.le_add_left 1 x).trans_lt hxb) with ⟨b, rfl⟩

Result:
case intro.intro
x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
⊢ (b + succ 1).digits x.succ = [x.succ]
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem disjoint_cylinder_of_longestPrefix_lt {s : Set (∀ n, E n)} (hs : IsClosed s) {x : ∀ n, E n}
    (hx : x ∉ s) {n : ℕ} (hn : longestPrefix x s < n) : Disjoint s (cylinder x n)

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : ¬Disjoint s (cylinder x n)
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder x n
⊢ x ∈ cylinder y n

Tactic:
rwa [mem_cylinder_comm]

Result:
no goals

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : ¬Disjoint s (cylinder x n)
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder x n
⊢ n ≤ firstDiff x y

Tactic:
apply (mem_cylinder_iff_le_firstDiff (ne_of_mem_of_not_mem ys hx).symm _).1

Result:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : ¬Disjoint s (cylinder x n)
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder x n
⊢ x ∈ cylinder y n

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : longestPrefix x s < n
⊢ Disjoint s (cylinder x n)

Tactic:
contrapose! hn

Result:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : ¬Disjoint s (cylinder x n)
⊢ n ≤ longestPrefix x s

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : ¬Disjoint s (cylinder x n)
⊢ n ≤ longestPrefix x s

Tactic:
rcases not_disjoint_iff_nonempty_inter.1 hn with ⟨y, ys, hy⟩

Result:
case intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : ¬Disjoint s (cylinder x n)
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder x n
⊢ n ≤ longestPrefix x s

Proof state:
case intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : ¬Disjoint s (cylinder x n)
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder x n
⊢ n ≤ longestPrefix x s

Tactic:
apply le_trans _ (firstDiff_le_longestPrefix hs hx ys)

Result:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : ¬Disjoint s (cylinder x n)
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder x n
⊢ n ≤ firstDiff x y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tmod_self {a : Int} : a.tmod a = 0

Proof state:
a : Int
⊢ a.tmod a = 0

Tactic:
have := mul_tmod_left 1 a

Result:
a : Int
this : (1 * a).tmod a = 0
⊢ a.tmod a = 0

Proof state:
a : Int
this : (1 * a).tmod a = 0
⊢ a.tmod a = 0

Tactic:
rwa [Int.one_mul] at this

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem sep_eq_empty_iff_mem_false : { x ∈ s | p x } = ∅ ↔ ∀ x ∈ s, ¬p x

Proof state:
α : Type u
s : Set α
p : α → Prop
⊢ {x | x ∈ s ∧ p x} = ∅ ↔ ∀ x ∈ s, ¬p x

Tactic:
simp_rw [Set.ext_iff, mem_sep_iff, mem_empty_iff_false, iff_false, not_and]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem _root_.Finset.nullMeasurableSet (s : Finset α) : NullMeasurableSet (↑s) μ

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass (NullMeasurableSpace α μ)
s : Finset α
⊢ NullMeasurableSet (↑s) μ

Tactic:
apply Finset.measurableSet

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem isUnit_of_mul_eq_one_right [CommMonoid M] (a b : M) (h : a * b = 1) : IsUnit b

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a b : M
h : a * b = 1
⊢ IsUnit b

Tactic:
rw [mul_comm] at h

Result:
M : Type u_1
inst✝ : CommMonoid M
a b : M
h : b * a = 1
⊢ IsUnit b

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a b : M
h : b * a = 1
⊢ IsUnit b

Tactic:
exact isUnit_of_mul_eq_one b a h

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
lemma map_injective_of_injective (hf : Function.Injective f) :
    Function.Injective (map f) := fun {N N'} h ↦
  SetLike.coe_injective <| hf.image_injective <| by simp only [← coe_map, h]

Proof state:
R : Type u
L : Type v
M : Type w
M' : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
hf : Function.Injective ⇑f
N N' : LieSubmodule R L M
h : map f N = map f N'
⊢ ⇑f '' ↑N = ⇑f '' ↑N'

Tactic:
simp only [← coe_map, h]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Unitor.lean
lemma r_zero (i₁ : I₁) (i₃ : I₃) : r ⟨i₁, 0, i₃⟩ = π ⟨i₁, i₃⟩

Proof state:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
J : Type u_4
inst✝ : Zero I₂
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
i₁ : I₁
i₃ : I₃
⊢ r (i₁, 0, i₃) = π (i₁, i₃)

Tactic:
rw [← τ.hp₂₃, τ.h₃ i₃]

Result:
no goals
-- Mathlib/Data/List/Perm/Basic.lean
theorem eq_map_comp_perm (f : α → β) : (· = map f ·) ∘r (· ~ ·) = (· ~ map f ·)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ ((fun x1 x2 => x1 = map f x2) ∘r fun x1 x2 => x1 ~ x2) = Perm ∘r fun x1 x2 => x1 = map f x2

Tactic:
simp only [← forall₂_eq_eq_eq, forall₂_map_right_iff, forall₂_comp_perm_eq_perm_comp_forall₂]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ ((fun x1 x2 => x1 = map f x2) ∘r fun x1 x2 => x1 ~ x2) = fun x1 x2 => x1 ~ map f x2

Tactic:
conv_rhs => rw [← Relation.comp_eq_fun (map f)]

Result:
α : Type u_1
β : Type u_2
f : α → β
⊢ ((fun x1 x2 => x1 = map f x2) ∘r fun x1 x2 => x1 ~ x2) = Perm ∘r fun x1 x2 => x1 = map f x2
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_range [DecidableEq α] [Fintype β] (f : β → α) (h : (range f).Finite) :
    h.toFinset = Finset.univ.image f

Proof state:
case h
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype β
f : β → α
h : (range f).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ Finset.image f Finset.univ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype β
f : β → α
h : (range f).Finite
⊢ h.toFinset = Finset.image f Finset.univ

Tactic:
ext

Result:
case h
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype β
f : β → α
h : (range f).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ Finset.image f Finset.univ
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_cpow {p : ℂ × ℂ} (hp_fst : p.fst ∈ slitPlane) :
    ContinuousAt (fun x : ℂ × ℂ => x.1 ^ x.2) p

Proof state:
p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
⊢ ContinuousAt (fun x => Complex.log x.1 * x.2) p

Tactic:
exact
  ContinuousAt.mul
    (ContinuousAt.comp (continuousAt_clog hp_fst) continuous_fst.continuousAt)
    continuous_snd.continuousAt

Result:
no goals

Proof state:
p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
⊢ ContinuousAt (fun x => x.1 ^ x.2) p

Tactic:
rw [continuousAt_congr (cpow_eq_nhds' <| slitPlane_ne_zero hp_fst)]

Result:
p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
⊢ ContinuousAt (fun x => cexp (Complex.log x.1 * x.2)) p

Proof state:
p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
⊢ ContinuousAt (fun x => cexp (Complex.log x.1 * x.2)) p

Tactic:
refine continuous_exp.continuousAt.comp ?_

Result:
p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
⊢ ContinuousAt (fun x => Complex.log x.1 * x.2) p
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tendsto_tan_neg_pi_div_two : Tendsto tan (𝓝[>] (-(π / 2))) atBot

Proof state:
⊢ -1 < 0

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ Tendsto tan (𝓝[>] (-(π / 2))) atBot

Tactic:
convert tendsto_cos_neg_pi_div_two.inv_tendsto_nhdsGT_zero.atTop_mul_neg (by norm_num)
    tendsto_sin_neg_pi_div_two using 1

Result:
case h.e'_3

⊢ tan = fun x => cos⁻¹ x * sin x

Proof state:
case h.e'_3

⊢ tan = fun x => cos⁻¹ x * sin x

Tactic:
simp only [Pi.inv_apply, ← div_eq_inv_mul, ← tan_eq_sin_div_cos]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem valid_endPos : Valid s (endPos s) := ⟨s.1, [], by simp, rfl⟩

Proof state:
s : String
⊢ s.data ++ [] = s.data

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `div_le_iff₀'` for a version with multiplication on the other side. -/
lemma div_le_iff₀ (hc : 0 < c) : b / c ≤ a ↔ b ≤ a * c

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hc : 0 < c
⊢ b / c ≤ a ↔ b ≤ a * c

Tactic:
rw [div_eq_mul_inv, mul_inv_le_iff₀ hc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma ΨSq_three : W.ΨSq 3 = W.Ψ₃ ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ ¬Even 3

Tactic:
decide

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.ΨSq 3 = W.Ψ₃ ^ 2

Tactic:
rw [← Nat.cast_three, ΨSq_ofNat, preΨ'_three, if_neg <| by decide, mul_one]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalHorizontalComp_cons_cons {f f' g g' h h' i i' : C}
    {α : f ≅ g} {η : g ⟶ h} {ηs : h ⟶ i}
    {β : f' ≅ g'} {θ : g' ⟶ h'} {θs : h' ⟶ i'}
    {ηθ : g ⊗ g' ⟶ h ⊗ h'} {ηθs : h ⊗ h' ⟶ i ⊗ i'}
    {ηθ₁ : g ⊗ g' ⟶ i ⊗ i'} {ηθ₂ : f ⊗ f' ⟶ i ⊗ i'}
    (e_ηθ : η ⊗ θ = ηθ) (e_ηθs : ηs ⊗ θs = ηθs)
    (e_ηθ₁ : ηθ ≫ ηθs = ηθ₁) (e_ηθ₂ : (α ⊗ β).hom ≫ ηθ₁ = ηθ₂) :
    (α.hom ≫ η ≫ ηs) ⊗ (β.hom ≫ θ ≫ θs) = ηθ₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h h' i i' : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
β : f' ≅ g'
θ : g' ⟶ h'
θs : h' ⟶ i'
ηθ : g ⊗ g' ⟶ h ⊗ h'
ηθs : h ⊗ h' ⟶ i ⊗ i'
ηθ₁ : g ⊗ g' ⟶ i ⊗ i'
ηθ₂ : f ⊗ f' ⟶ i ⊗ i'
e_ηθ : η ⊗ θ = ηθ
e_ηθs : ηs ⊗ θs = ηθs
e_ηθ₁ : ηθ ≫ ηθs = ηθ₁
e_ηθ₂ : (α ⊗ β).hom ≫ ηθ₁ = ηθ₂
⊢ α.hom ≫ η ≫ ηs ⊗ β.hom ≫ θ ≫ θs = ηθ₂

Tactic:
simp [← e_ηθ , ← e_ηθs , ← e_ηθ₁, ← e_ηθ₂]

Result:
no goals
-- Mathlib/Order/Filter/Pointwise.lean
theorem inv_le_iff_le_inv : f⁻¹ ≤ g ↔ f ≤ g⁻¹

Proof state:
α : Type u_2
inst✝ : InvolutiveInv α
f g : Filter α
⊢ f⁻¹ ≤ g ↔ f ≤ g⁻¹

Tactic:
rw [← Filter.inv_le_inv_iff, inv_inv]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem norm_exp_ofReal_mul_I (x : ℝ) : ‖exp (x * I)‖ = 1

Proof state:
x : ℝ
⊢ ‖cexp (↑x * I)‖ = 1

Tactic:
rw [exp_mul_I, norm_cos_add_sin_mul_I]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem le_mul_right {a b : Cardinal} (h : b ≠ 0) : a ≤ a * b

Proof state:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ b * a

Tactic:
exact le_mul_left h

Result:
no goals

Proof state:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ a * b

Tactic:
rw [mul_comm]

Result:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ b * a
-- Mathlib/RingTheory/AdicCompletion/Algebra.lean
theorem evalₐ_mkₐ (n : ℕ) (x : AdicCauchySequence I R) :
    evalₐ I n (mkₐ I x) = Ideal.Quotient.mk (I ^ n) (x.val n)

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x : AdicCauchySequence I R
⊢ (evalₐ I n) ((mkₐ I) x) = (Ideal.Quotient.mk (I ^ n)) (↑x n)

Tactic:
simp [mkₐ]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Sphere.lean
theorem oangle_eq_pi_sub_two_zsmul_oangle_center_left {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s)
    (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) : ∡ p₁ s.center p₂ = π - (2 : ℤ) • ∡ s.center p₂ p₁

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ∡ p₁ s.center p₂ = ↑π - 2 • ∡ s.center p₂ p₁

Tactic:
rw [oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq h.symm
    (dist_center_eq_dist_center_of_mem_sphere' hp₂ hp₁)]

Result:
no goals