harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem uniformEquicontinuousOn_finite [Finite ι] {F : ι → β → α} {S : Set β} :
    UniformEquicontinuousOn F S ↔ ∀ i, UniformContinuousOn (F i) S

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst✝ : Finite ι
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S ↔ ∀ (i : ι), UniformContinuousOn (F i) S

Tactic:
simp only [UniformEquicontinuousOn, eventually_all, @forall_swap _ ι]

Result:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst✝ : Finite ι
F : ι → β → α
S : Set β
⊢ (∀ (y : ι), ∀ x ∈ 𝓤 α, ∀ᶠ (x_2 : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), (F y x_2.1, F y x_2.2) ∈ x) ↔
    ∀ (i : ι), UniformContinuousOn (F i) S

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst✝ : Finite ι
F : ι → β → α
S : Set β
⊢ (∀ (y : ι), ∀ x ∈ 𝓤 α, ∀ᶠ (x_2 : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), (F y x_2.1, F y x_2.2) ∈ x) ↔
    ∀ (i : ι), UniformContinuousOn (F i) S

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/CharP/Two.lean
theorem add_self_eq_zero (x : R) : x + x = 0

Proof state:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
x : R
⊢ x + x = 0

Tactic:
rw [← two_smul R x, two_eq_zero, zero_smul]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem zero : padicValRat p 0 = 0

Proof state:
p : ℕ
⊢ padicValRat p 0 = 0

Tactic:
simp [padicValRat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_alter [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} :
    k' ∈ m.alter k f ↔ if k == k' then (f (m.get? k)).isSome = true else k' ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
⊢ k' ∈ m.alter k f ↔ if (k == k') = true then (f (m.get? k)).isSome = true else k' ∈ m

Tactic:
simp only [mem_iff_contains, contains_alter, beq_iff_eq, Bool.ite_eq_true_distrib]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem _root_.Nat.mem_range_succ (i : ℕ) : i ∈ range Nat.succ ↔ 0 < i :=
  ⟨by
    rintro ⟨n, rfl⟩
    exact Nat.succ_pos n, fun h => ⟨_, Nat.succ_pred_eq_of_pos h⟩⟩

Proof state:
case intro
n : ℕ
⊢ 0 < n.succ

Tactic:
exact Nat.succ_pos n

Result:
no goals

Proof state:
i : ℕ
⊢ i ∈ range Nat.succ → 0 < i

Tactic:
rintro ⟨n, rfl⟩

Result:
case intro
n : ℕ
⊢ 0 < n.succ
-- Mathlib/Data/ENNReal/Order.lean
theorem not_lt_top {x : ℝ≥0∞} : ¬x < ∞ ↔ x = ∞

Proof state:
x : ℝ≥0∞
⊢ ¬x < ⊤ ↔ x = ⊤

Tactic:
rw [lt_top_iff_ne_top, Classical.not_not]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
theorem row_ne_zero [Nontrivial R] (g : SpecialLinearGroup n R) (i : n) : g i ≠ 0 := fun h =>
  g.det_ne_zero <| det_eq_zero_of_row_eq_zero i <| by simp [h]

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
i : n
h : ↑g i = 0
⊢ ∀ (j : n), ↑g i j = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem norm_one : norm (1 : ℤ√d) = 1

Proof state:
d : ℤ
⊢ norm 1 = 1

Tactic:
simp [norm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem edist_eq_zero_iff :
    G.edist u v = 0 ↔ u = v

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = 0 ↔ u = v

Tactic:
apply Iff.intro <;> simp [edist, ENat.iInf_eq_zero]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem freeOn_indep_iff : (freeOn E).Indep I ↔ I ⊆ E

Proof state:
α : Type u_1
E I : Set α
⊢ (freeOn E).Indep I ↔ I ⊆ E

Tactic:
simp [indep_iff]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma toENNReal_add_le {x y : EReal} : (x + y).toENNReal ≤ x.toENNReal + y.toENNReal

Proof state:
case h_real.h_real
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).toENNReal ≤ (↑a✝¹).toENNReal + (↑a✝).toENNReal

Tactic:
exact ENNReal.ofReal_add_le

Result:
no goals

Proof state:
case h_top.h_top

⊢ (⊤ + ⊤).toENNReal ≤ ⊤.toENNReal + ⊤.toENNReal

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_eq_prime (hg : x ^ p = 1) (hg1 : x ≠ 1) : orderOf x = p :=
  minimalPeriod_eq_prime ((isPeriodicPt_mul_iff_pow_eq_one _).mpr hg)
    (by rwa [IsFixedPt, mul_one])

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
hg : x ^ p = 1
hg1 : x ≠ 1
⊢ ¬IsFixedPt (fun x_1 => x * x_1) 1

Tactic:
rwa [IsFixedPt, mul_one]

Result:
no goals
-- Mathlib/Data/Finset/Preimage.lean
theorem image_preimage [DecidableEq β] (f : α → β) (s : Finset β) [∀ x, Decidable (x ∈ Set.range f)]
    (hf : Set.InjOn f (f ⁻¹' ↑s)) : image f (preimage s f hf) = s.filter fun x => x ∈ Set.range f :=
  Finset.coe_inj.1 <| by
    simp only [coe_image, coe_preimage, coe_filter, Set.image_preimage_eq_inter_range,
      ← Set.sep_mem_eq]; rfl

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ ↑(image f (s.preimage f hf)) = ↑(filter (fun x => x ∈ Set.range f) s)

Tactic:
simp only [coe_image, coe_preimage, coe_filter, Set.image_preimage_eq_inter_range,
  ← Set.sep_mem_eq]

Result:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ {x | x ∈ ↑s ∧ x ∈ Set.range f} = {x | x ∈ s ∧ x ∈ Set.range f}

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ {x | x ∈ ↑s ∧ x ∈ Set.range f} = {x | x ∈ s ∧ x ∈ Set.range f}

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem closedBall_normSeminorm : (normSeminorm 𝕜 E).closedBall = Metric.closedBall

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ (normSeminorm 𝕜 E).closedBall = Metric.closedBall

Tactic:
ext x r y

Result:
case h.h.h
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ (normSeminorm 𝕜 E).closedBall x r ↔ y ∈ Metric.closedBall x r

Proof state:
case h.h.h
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ (normSeminorm 𝕜 E).closedBall x r ↔ y ∈ Metric.closedBall x r

Tactic:
simp only [Seminorm.mem_closedBall, Metric.mem_closedBall, coe_normSeminorm, dist_eq_norm]

Result:
no goals
-- Mathlib/Order/Ideal.lean
theorem toLowerSet_injective : Injective (toLowerSet : Ideal P → LowerSet P) := fun s t _ ↦ by
  cases s
  cases t
  congr

Proof state:
case mk
P : Type u_1
inst✝ : LE P
t : Ideal P
toLowerSet✝ : LowerSet P
nonempty'✝ : toLowerSet✝.carrier.Nonempty
directed'✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet✝.carrier
x✝ : { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet = t.toLowerSet
⊢ { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ } = t

Tactic:
cases t

Result:
case mk.mk
P : Type u_1
inst✝ : LE P
toLowerSet✝¹ : LowerSet P
nonempty'✝¹ : toLowerSet✝¹.carrier.Nonempty
directed'✝¹ : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet✝¹.carrier
toLowerSet✝ : LowerSet P
nonempty'✝ : toLowerSet✝.carrier.Nonempty
directed'✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet✝.carrier
x✝ :
  { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ }.toLowerSet =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet
⊢ { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ } =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }

Proof state:
P : Type u_1
inst✝ : LE P
s t : Ideal P
x✝ : s.toLowerSet = t.toLowerSet
⊢ s = t

Tactic:
cases s

Result:
case mk
P : Type u_1
inst✝ : LE P
t : Ideal P
toLowerSet✝ : LowerSet P
nonempty'✝ : toLowerSet✝.carrier.Nonempty
directed'✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet✝.carrier
x✝ : { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet = t.toLowerSet
⊢ { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ } = t

Proof state:
case mk.mk
P : Type u_1
inst✝ : LE P
toLowerSet✝¹ : LowerSet P
nonempty'✝¹ : toLowerSet✝¹.carrier.Nonempty
directed'✝¹ : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet✝¹.carrier
toLowerSet✝ : LowerSet P
nonempty'✝ : toLowerSet✝.carrier.Nonempty
directed'✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet✝.carrier
x✝ :
  { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ }.toLowerSet =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet
⊢ { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ } =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
/-- `0` has infinite radius of convergence -/
@[simp] lemma zero_radius : (0 : FormalMultilinearSeries 𝕜 E F).radius = ∞

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ radius 0 = ⊤

Tactic:
rw [← constFormalMultilinearSeries_zero]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ (constFormalMultilinearSeries 𝕜 E 0).radius = ⊤

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ (constFormalMultilinearSeries 𝕜 E 0).radius = ⊤

Tactic:
exact constFormalMultilinearSeries_radius

Result:
no goals
-- Mathlib/Data/Finsupp/SMulWithZero.lean
theorem mapRange_smul {_ : Monoid R} [AddMonoid M] [DistribMulAction R M] [AddMonoid N]
    [DistribMulAction R N] {f : M → N} {hf : f 0 = 0} (c : R) (v : α →₀ M)
    (hsmul : ∀ x, f (c • x) = c • f x) : mapRange f hf (c • v) = c • mapRange f hf v

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
x✝ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
f : M → N
hf : f 0 = 0
c : R
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = c • f x
this : (f ∘ fun x => c • x) = (fun x => c • x) ∘ f
⊢ mapRange (f ∘ fun x => c • x) ?h v = c • mapRange f hf v

Tactic:
simp_rw [this]

Result:
α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
x✝ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
f : M → N
hf : f 0 = 0
c : R
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = c • f x
this : (f ∘ fun x => c • x) = (fun x => c • x) ∘ f
⊢ mapRange ((fun x => c • x) ∘ f) ⋯ v = c • mapRange f hf v

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
x✝ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
f : M → N
hf : f 0 = 0
c : R
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = c • f x
⊢ mapRange f hf (c • v) = c • mapRange f hf v

Tactic:
erw [← mapRange_comp]

Result:
α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
x✝ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
f : M → N
hf : f 0 = 0
c : R
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = c • f x
⊢ mapRange (f ∘ fun x => c • x) ?h v = c • mapRange f hf v

case h
α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
x✝ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
f : M → N
hf : f 0 = 0
c : R
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = c • f x
⊢ (f ∘ fun x => c • x) 0 = 0

Proof state:
case h
α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
x✝ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
f : M → N
hf : f 0 = 0
c : R
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = c • f x
⊢ (f ∘ fun x => c • x) 0 = 0

Tactic:
simp only [Function.comp_apply, smul_zero, hf]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
x✝ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
f : M → N
hf : f 0 = 0
c : R
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = c • f x
this : (f ∘ fun x => c • x) = (fun x => c • x) ∘ f
⊢ mapRange ((fun x => c • x) ∘ f) ⋯ v = c • mapRange f hf v

Tactic:
apply mapRange_comp

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Defs.lean
theorem mk_eq_div' (p q : K[X]) :
    RatFunc.mk p q = ofFractionRing (algebraMap _ _ p / algebraMap _ _ q)

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q : K[X]
⊢ RatFunc.mk p q =
    { toFractionRing := (algebraMap K[X] (FractionRing K[X])) p / (algebraMap K[X] (FractionRing K[X])) q }

Tactic:
rw [RatFunc.mk]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp, nolint simpNF] protected lemma add_eq_zero : m + n = 0 ↔ m = 0 ∧ n = 0

Proof state:
m n : ℕ
⊢ m + n = 0 ↔ m = 0 ∧ n = 0

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
lemma strongConvexOn_iff_convex :
    StrongConvexOn s m f ↔ ConvexOn ℝ s fun x ↦ f x - m / (2 : ℝ) * ‖x‖ ^ 2

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
x✝² : Convex ℝ s
x : E
x✝¹ : x ∈ s
y : E
x✝ : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • f x + b • f y - a * b * (fun r => m / 2 * r ^ 2) ‖x - y‖ ↔
    (fun x => f x - m / 2 * ‖x‖ ^ 2) (a • x + b • y) ≤
      a • (fun x => f x - m / 2 * ‖x‖ ^ 2) x + b • (fun x => f x - m / 2 * ‖x‖ ^ 2) y

Tactic:
simp_rw [sub_le_iff_le_add, smul_eq_mul, aux_sub ha hb hab, mul_assoc, mul_left_comm]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
⊢ StrongConvexOn s m f ↔ ConvexOn ℝ s fun x => f x - m / 2 * ‖x‖ ^ 2

Tactic:
refine and_congr_right fun _ ↦ forall₄_congr fun x _ y _ ↦ forall₅_congr fun a b ha hb hab ↦ ?_

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
x✝² : Convex ℝ s
x : E
x✝¹ : x ∈ s
y : E
x✝ : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • f x + b • f y - a * b * (fun r => m / 2 * r ^ 2) ‖x - y‖ ↔
    (fun x => f x - m / 2 * ‖x‖ ^ 2) (a • x + b • y) ≤
      a • (fun x => f x - m / 2 * ‖x‖ ^ 2) x + b • (fun x => f x - m / 2 * ‖x‖ ^ 2) y
-- Mathlib/Analysis/Convex/Combination.lean
lemma Finset.centerMass_of_sum_add_sum_eq_zero {s t : Finset ι}
    (hw : ∑ i ∈ s, w i + ∑ i ∈ t, w i = 0) (hz : ∑ i ∈ s, w i • z i + ∑ i ∈ t, w i • z i = 0) :
    s.centerMass w z = t.centerMass w z

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
w : ι → R
z : ι → E
s t : Finset ι
hw : ∑ i ∈ s, w i + ∑ i ∈ t, w i = 0
hz : ∑ i ∈ s, w i • z i + ∑ i ∈ t, w i • z i = 0
⊢ s.centerMass w z = t.centerMass w z

Tactic:
simp [centerMass, eq_neg_of_add_eq_zero_right hw, eq_neg_of_add_eq_zero_left hz, ← neg_inv]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem normSq_le_normSq_of_re_le_of_im_le {x y : ℂ} (hre : |x.re| ≤ |y.re|)
    (him : |x.im| ≤ |y.im|) : Complex.normSq x ≤ Complex.normSq y

Proof state:
x y : ℂ
hre : |x.re| ≤ |y.re|
him : |x.im| ≤ |y.im|
⊢ normSq x ≤ normSq y

Tactic:
rw [normSq_apply, normSq_apply, ← _root_.abs_mul_self, _root_.abs_mul, ←
    _root_.abs_mul_self y.re, _root_.abs_mul y.re, ← _root_.abs_mul_self x.im,
    _root_.abs_mul x.im, ← _root_.abs_mul_self y.im, _root_.abs_mul y.im]

Result:
x y : ℂ
hre : |x.re| ≤ |y.re|
him : |x.im| ≤ |y.im|
⊢ |x.re| * |x.re| + |x.im| * |x.im| ≤ |y.re| * |y.re| + |y.im| * |y.im|

Proof state:
x y : ℂ
hre : |x.re| ≤ |y.re|
him : |x.im| ≤ |y.im|
⊢ |x.re| * |x.re| + |x.im| * |x.im| ≤ |y.re| * |y.re| + |y.im| * |y.im|

Tactic:
exact
    add_le_add (mul_self_le_mul_self (abs_nonneg _) hre) (mul_self_le_mul_self (abs_nonneg _) him)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
    (h : m.WF) {l : List α}
    {k k' : α} (k_beq : k == k') {h'} :
    ¬ k ∈ m → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
      getKey (insertManyIfNewUnit m l) k' h' = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k k' : α
k_beq : (k == k') = true
h' : k' ∈ insertManyIfNewUnit m l
⊢ ¬k ∈ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKey k' h' = k

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k k' : α
k_beq : (k == k') = true
h' : k' ∈ insertManyIfNewUnit m l
⊢ m.contains k = false →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKey k' h' = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k k' : α
k_beq : (k == k') = true
h' : k' ∈ insertManyIfNewUnit m l
⊢ m.contains k = false →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKey k' h' = k

Tactic:
simp_to_raw using Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem union_pi : (s₁ ∪ s₂).pi t = s₁.pi t ∩ s₂.pi t

Proof state:
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t : (i : ι) → Set (α i)
⊢ (s₁ ∪ s₂).pi t = s₁.pi t ∩ s₂.pi t

Tactic:
simp [pi, or_imp, forall_and, setOf_and]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem finite_toSet_toFinset (s : Finset α) : s.finite_toSet.toFinset = s

Proof state:
α : Type u
s : Finset α
⊢ ⋯.toFinset = s

Tactic:
rw [toFinite_toFinset, toFinset_coe]

Result:
no goals
-- Mathlib/Tactic/NormNum/Result.lean
theorem IsRat.nonneg_to_eq {α} [DivisionRing α] {n d} :
    {a n' d' : α} → IsRat a (.ofNat n) d → n = n' → d = d' → a = n' / d'
  | _, _, _, ⟨_, rfl⟩, rfl, rfl => by simp [div_eq_mul_inv]

Proof state:
α : Type u_1
inst✝ : DivisionRing α
n d : ℕ
inv✝ : Invertible ↑d
⊢ ↑(Int.ofNat n) * ⅟↑d = ↑n / ↑d

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem int_cyclotomic_unique {n : ℕ} {P : ℤ[X]} (h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ) :
    P = cyclotomic n ℤ

Proof state:
case a
n : ℕ
P : ℤ[X]
h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ
⊢ map (Int.castRingHom ℂ) P = map (Int.castRingHom ℂ) (cyclotomic n ℤ)

Tactic:
rw [h, (int_cyclotomic_spec n).1]

Result:
no goals

Proof state:
n : ℕ
P : ℤ[X]
h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ
⊢ P = cyclotomic n ℤ

Tactic:
apply map_injective (Int.castRingHom ℂ) Int.cast_injective

Result:
case a
n : ℕ
P : ℤ[X]
h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ
⊢ map (Int.castRingHom ℂ) P = map (Int.castRingHom ℂ) (cyclotomic n ℤ)
-- Mathlib/Data/Multiset/Sum.lean
theorem card_disjSum : Multiset.card (s.disjSum t) = Multiset.card s + Multiset.card t

Proof state:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ (s.disjSum t).card = s.card + t.card

Tactic:
rw [disjSum, card_add, card_map, card_map]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem padicNorm_p_lt_one (hp : 1 < p) : padicNorm p p < 1

Proof state:
p : ℕ
hp : 1 < p
⊢ ↑p ≤ 0 ∨ 1 < ↑p

Tactic:
exact mod_cast Or.inr hp

Result:
no goals

Proof state:
p : ℕ
hp : 1 < p
⊢ padicNorm p ↑p < 1

Tactic:
rw [padicNorm_p hp, inv_lt_one_iff₀]

Result:
p : ℕ
hp : 1 < p
⊢ ↑p ≤ 0 ∨ 1 < ↑p
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma odd_add' : Odd (m + n) ↔ (Odd n ↔ Even m)

Proof state:
m n : ℤ
⊢ Odd (m + n) ↔ (Odd n ↔ Even m)

Tactic:
rw [add_comm, odd_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mod_mod (a n : Nat) : (a % n) % n = a % n :=
  match eq_zero_or_pos n with
  | .inl n0 => by simp [n0, mod_zero]
  | .inr npos => Nat.mod_eq_of_lt (mod_lt _ npos)

Proof state:
a n : Nat
n0 : n = 0
⊢ a % n % n = a % n

Tactic:
simp [n0, mod_zero]

Result:
no goals
-- Mathlib/Tactic/NormNum/GCD.lean
theorem int_lcm_helper {x y : ℤ} {x' y' d : ℕ}
    (hx : x.natAbs = x') (hy : y.natAbs = y') (h : Nat.lcm x' y' = d) :
    Int.lcm x y = d

Proof state:
x y : ℤ
⊢ x.lcm y = x.natAbs.lcm y.natAbs

Tactic:
rw [Int.lcm_def]

Result:
no goals

Proof state:
x y : ℤ
x' y' d : ℕ
hx : x.natAbs = x'
hy : y.natAbs = y'
h : x'.lcm y' = d
⊢ x.lcm y = d

Tactic:
subst_vars

Result:
x y : ℤ
⊢ x.lcm y = x.natAbs.lcm y.natAbs
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_shiftConcat_succ {x : BitVec w} {b : Bool} (h : i + 1 < w) :
    (x.shiftConcat b)[i+1] = x[i]

Proof state:
w i : Nat
x : BitVec w
b : Bool
h : i + 1 < w
⊢ (x.shiftConcat b)[i + 1] = x[i]

Tactic:
simp [getElem_shiftConcat]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_top : Ioc a ⊤ = Ioi a

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ Ioc a ⊤ = Ioi a

Tactic:
simp [← Ioi_inter_Iic]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem isometry_mk (i : ι) : Isometry (Sigma.mk i : E i → Σk, E k) :=
  Isometry.of_dist_eq fun x y => by simp

Proof state:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x y : E i
⊢ dist ⟨i, x⟩ ⟨i, y⟩ = dist x y

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem inr_isoPushout_hom (h : IsPushout f g inl inr) [HasPushout f g] :
    inr ≫ h.isoPushout.hom = pushout.inr _ _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ inr ≫ h.isoPushout.hom = pushout.inr f g

Tactic:
simp [← Iso.eq_comp_inv]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem mul_right_cancel' {a b c m : ℕ} (hc : c ≠ 0) :
    a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m]

Proof state:
a b c m : ℕ
hc : c ≠ 0
⊢ a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m]

Tactic:
simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.sub_mul]

Result:
a b c m : ℕ
hc : c ≠ 0
⊢ ↑m * ↑c ∣ (↑b - ↑a) * ↑c → ↑m ∣ ↑b - ↑a

Proof state:
a b c m : ℕ
hc : c ≠ 0
⊢ ↑m * ↑c ∣ (↑b - ↑a) * ↑c → ↑m ∣ ↑b - ↑a

Tactic:
exact fun h => (Int.dvd_of_mul_dvd_mul_right (Int.ofNat_ne_zero.mpr hc) h)

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem le_one_iff {p : Associates M} : p ≤ 1 ↔ p = 1

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
⊢ p ≤ 1 ↔ p = 1

Tactic:
rw [← Associates.bot_eq_one, le_bot_iff]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mex_le_of_ne {ι} {f : ι → Ordinal} {a} (ha : ∀ i, f i ≠ a) : mex f ≤ a :=
  csInf_le' (by simp [ha])

Proof state:
ι : Type u_4
f : ι → Ordinal.{max u_5 u_4}
a : Ordinal.{max u_5 u_4}
ha : ∀ (i : ι), f i ≠ a
⊢ a ∈ (range f)ᶜ

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem tsub_eq_of_eq_add (hb : AddLECancellable b) (h : a = c + b) : a - b = c :=
  le_antisymm (tsub_le_iff_right.mpr h.le) <| by
    rw [h]
    exact hb.le_add_tsub

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a = c + b
⊢ c ≤ c + b - b

Tactic:
exact hb.le_add_tsub

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a = c + b
⊢ c ≤ a - b

Tactic:
rw [h]

Result:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a = c + b
⊢ c ≤ c + b - b