harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Int/Range.lean
theorem mem_range_iff {m n r : ℤ} : r ∈ range m n ↔ m ≤ r ∧ r < n

Proof state:
m n r : ℤ
h : m ≤ r ∧ r < n
⊢ m + ↑(r - m).toNat < n ∧ m + ↑(r - m).toNat = r

Tactic:
simp [toNat_of_nonneg (sub_nonneg.2 h.1), h.2]

Result:
no goals

Proof state:
m n r : ℤ
⊢ (∃ a, m + ↑a < n ∧ m + ↑a = r) ↔ m ≤ r ∧ r < n

Tactic:
exact ⟨fun ⟨a, ha⟩ => ha.2 ▸ ⟨le_add_of_nonneg_right (Int.natCast_nonneg _), ha.1⟩,
  fun h => ⟨toNat (r - m), by simp [toNat_of_nonneg (sub_nonneg.2 h.1), h.2] ⟩⟩

Result:
no goals

Proof state:
m n r : ℤ
⊢ r ∈ m.range n ↔ m ≤ r ∧ r < n

Tactic:
simp only [range, List.mem_map, List.mem_range, lt_toNat, lt_sub_iff_add_lt, add_comm]

Result:
m n r : ℤ
⊢ (∃ a, m + ↑a < n ∧ m + ↑a = r) ↔ m ≤ r ∧ r < n
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_toNNReal_iff' {f : α → ℝ≥0∞} {u : Filter α} {a : ℝ≥0} (hf : ∀ x, f x ≠ ∞) :
    Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a) ↔ Tendsto f u (𝓝 a)

Proof state:
α : Type u_1
f : α → ℝ≥0∞
u : Filter α
a : ℝ≥0
hf : ∀ (x : α), f x ≠ ⊤
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a) ↔ Tendsto f u (𝓝 ↑a)

Tactic:
rw [← toNNReal_coe a]

Result:
α : Type u_1
f : α → ℝ≥0∞
u : Filter α
a : ℝ≥0
hf : ∀ (x : α), f x ≠ ⊤
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 (↑a).toNNReal) ↔ Tendsto f u (𝓝 ↑(↑a).toNNReal)

Proof state:
α : Type u_1
f : α → ℝ≥0∞
u : Filter α
a : ℝ≥0
hf : ∀ (x : α), f x ≠ ⊤
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 (↑a).toNNReal) ↔ Tendsto f u (𝓝 ↑(↑a).toNNReal)

Tactic:
exact tendsto_toNNReal_iff coe_ne_top hf

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem zero_descFactorial_succ (k : ℕ) : (0 : ℕ).descFactorial (k + 1) = 0

Proof state:
k : ℕ
⊢ descFactorial 0 (k + 1) = 0

Tactic:
rw [descFactorial_succ, Nat.zero_sub, Nat.zero_mul]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_sub_right (x y : V) : (o.oangle x (y - x)).sign = (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.oangle x (y - x)).sign = (o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_sub_smul_right x y 1, one_smul]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem lt_ciSup_iff' {f : ι → α} (h : BddAbove (range f)) : a < iSup f ↔ ∃ i, a < f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
a : α
f : ι → α
h : BddAbove (range f)
⊢ a < iSup f ↔ ∃ i, a < f i

Tactic:
simpa only [not_le, not_forall] using (ciSup_le_iff' h).not

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_apply_left (a : α) : toIcoDiv hp a a = 0 :=
  toIcoDiv_eq_of_sub_zsmul_mem_Ico hp <| by simp [hp]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a - 0 • p ∈ Set.Ico a (a + p)

Tactic:
simp [hp]

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem range_eq_map (f : R →+* S) : f.range = Subring.map f ⊤

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ f.range = Subring.map f ⊤

Tactic:
ext

Result:
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
x✝ : S
⊢ x✝ ∈ f.range ↔ x✝ ∈ Subring.map f ⊤

Proof state:
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
x✝ : S
⊢ x✝ ∈ f.range ↔ x✝ ∈ Subring.map f ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem sup_sdiff_symmDiff : (a ⊔ b) \ a ∆ b = a ⊓ b :=
  sdiff_eq_symm inf_le_sup (by rw [symmDiff_eq_sup_sdiff_inf])

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ (a ⊔ b) \ (a ⊓ b) = a ∆ b

Tactic:
rw [symmDiff_eq_sup_sdiff_inf]

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem le_max_of_le {l : List α} {a x : α} (hx : x ∈ l) (h : a ≤ x) : a ≤ l.foldr max ⊥

Proof state:
case cons.head
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ foldr max ⊥ (x :: l)

Tactic:
simp only [foldr, foldr_cons]

Result:
case cons.head
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ x ⊔ foldr max ⊥ l

Proof state:
case cons.tail
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)

Tactic:
exact le_max_of_le_right (IH (by assumption))

Result:
no goals

Proof state:
case cons.head
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ x ⊔ foldr max ⊥ l

Tactic:
exact le_max_of_le_left h

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
hx : x ∈ y :: l
⊢ a ≤ foldr max ⊥ (y :: l)

Tactic:
obtain hl | hl := hx

Result:
case cons.head
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ foldr max ⊥ (x :: l)

case cons.tail
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)

Proof state:
case nil
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
hx : x ∈ []
⊢ a ≤ foldr max ⊥ []

Tactic:
exact absurd hx (not_mem_nil _)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
a x : α
hx : x ∈ l
h : a ≤ x
⊢ a ≤ foldr max ⊥ l

Tactic:
induction' l with y l IH

Result:
case nil
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
hx : x ∈ []
⊢ a ≤ foldr max ⊥ []

case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
hx : x ∈ y :: l
⊢ a ≤ foldr max ⊥ (y :: l)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ x ∈ l

Tactic:
assumption

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
    m.isEmpty = true → get! m a = default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
a : α
⊢ m.isEmpty = true → get! m a = default

Tactic:
simp_to_raw using Raw₀.Const.get!_of_isEmpty ⟨m, _⟩

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem coe_mk (hon : Orthonormal 𝕜 v) (hsp : ⊤ ≤ Submodule.span 𝕜 (Set.range v)) :
    ⇑(OrthonormalBasis.mk hon hsp) = v

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : ⊤ ≤ span 𝕜 (range v)
⊢ ⇑(OrthonormalBasis.mk hon hsp) = v

Tactic:
classical rw [OrthonormalBasis.mk, _root_.Basis.coe_toOrthonormalBasis, Basis.coe_mk]

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : ⊤ ≤ span 𝕜 (range v)
⊢ ⇑(OrthonormalBasis.mk hon hsp) = v

Tactic:
rw [OrthonormalBasis.mk, _root_.Basis.coe_toOrthonormalBasis, Basis.coe_mk]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Block.lean
lemma BlockTriangular.map {S F} [FunLike F R S] [Zero R] [Zero S] [ZeroHomClass F R S] (f : F)
    (h : BlockTriangular M b) : BlockTriangular (M.map f) b :=
  fun i j lt ↦ by simp [h lt]

Proof state:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : LT α
S : Type u_8
F : Type u_9
inst✝³ : FunLike F R S
inst✝² : Zero R
inst✝¹ : Zero S
inst✝ : ZeroHomClass F R S
f : F
h : M.BlockTriangular b
i j : m
lt : b j < b i
⊢ M.map (⇑f) i j = 0

Tactic:
simp [h lt]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_sdiff : a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)

Tactic:
rw [symmDiff, sup_sdiff_distrib, sdiff_sdiff_left, sdiff_sdiff_left]

Result:
no goals
-- Mathlib/Data/Set/Countable.lean
theorem countable_union {s t : Set α} : (s ∪ t).Countable ↔ s.Countable ∧ t.Countable

Proof state:
α : Type u
s t : Set α
⊢ (s ∪ t).Countable ↔ s.Countable ∧ t.Countable

Tactic:
simp [union_eq_iUnion, and_comm]

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem exists_pos_variant (h₀ : 0 < d) (a : Solution₁ d) :
    ∃ b : Solution₁ d, 0 < b.x ∧ 0 ≤ b.y ∧ a ∈ ({b, b⁻¹, -b, -b⁻¹} : Set (Solution₁ d))

Proof state:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
⊢ ∃ b, 0 < b.x ∧ 0 ≤ b.y ∧ a ∈ {b, b⁻¹, -b, -b⁻¹}

Tactic:
refine
      (lt_or_gt_of_ne (a.x_ne_zero h₀.le)).elim
        ((le_total 0 a.y).elim (fun hy hx => ⟨-a⁻¹, ?_, ?_, ?_⟩) fun hy hx => ⟨-a, ?_, ?_, ?_⟩)
        ((le_total 0 a.y).elim (fun hy hx => ⟨a, hx, hy, ?_⟩) fun hy hx => ⟨a⁻¹, hx, ?_, ?_⟩) <;>
    simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
      eq_self_iff_true, x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true] <;>
  assumption

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
@[simp]
lemma card_Iic : #(Iic b) = b + 1

Proof state:
b : ℕ
⊢ #(Iic b) = b + 1

Tactic:
rw [Iic_eq_Icc, card_Icc, Nat.bot_eq_zero, Nat.sub_zero]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_sub_right_swap (x y : V) : (o.oangle y (y - x)).sign = (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.oangle y (y - x)).sign = (o.oangle x y).sign

Tactic:
rw [oangle_sign_sub_right_eq_neg, o.oangle_rev y x, Real.Angle.sign_neg]

Result:
no goals
-- Mathlib/CategoryTheory/FintypeCat.lean
theorem incl_mk_nat_card (n : ℕ) : Fintype.card (incl.obj (mk n)) = n

Proof state:
n : ℕ
⊢ Fintype.card (incl.obj (mk n)).carrier = n

Tactic:
convert Finset.card_fin n

Result:
case h.e'_2
n : ℕ
⊢ Fintype.card (incl.obj (mk n)).carrier = Finset.univ.card

Proof state:
case h.e'_2
n : ℕ
⊢ Fintype.card (incl.obj (mk n)).carrier = Finset.univ.card

Tactic:
apply Fintype.ofEquiv_card

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem map_comp_map (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ)
    (hf' : ψ'.comp f₂ = f₃.comp φ') (hg' : ψ'.comp g₂ = g₃.comp φ') :
    (map φ' ψ' hf' hg').comp (map φ ψ hf hg) =
      map (φ'.comp φ) (ψ'.comp ψ) (comm_sq₂ hf hf') (comm_sq₂ hg hg')

Proof state:
case H.a
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
hg' : ψ'.comp g₂ = g₃.comp φ'
x✝ : ↥(f₁.equalizer g₁)
⊢ ↑(((map φ' ψ' hf' hg').comp (map φ ψ hf hg)) x✝) = ↑((map (φ'.comp φ) (ψ'.comp ψ) ⋯ ⋯) x✝)

Tactic:
rfl

Result:
no goals

Proof state:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
hg' : ψ'.comp g₂ = g₃.comp φ'
⊢ (map φ' ψ' hf' hg').comp (map φ ψ hf hg) = map (φ'.comp φ) (ψ'.comp ψ) ⋯ ⋯

Tactic:
ext

Result:
case H.a
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
hg' : ψ'.comp g₂ = g₃.comp φ'
x✝ : ↥(f₁.equalizer g₁)
⊢ ↑(((map φ' ψ' hf' hg').comp (map φ ψ hf hg)) x✝) = ↑((map (φ'.comp φ) (ψ'.comp ψ) ⋯ ⋯) x✝)
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem inv_smul_integral_comp_div_add (c d) :
    (c⁻¹ • ∫ x in a..b, f (x / c + d)) = ∫ x in a / c + d..b / c + d, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
⊢ c⁻¹ • ∫ (x : ℝ) in a..b, f (x / c + d) = ∫ (x : ℝ) in a / c + d..b / c + d, f x

Tactic:
by_cases hc : c = 0 <;> simp [hc, integral_comp_div_add]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem mem_support_cycleOf_iff'_aux (hx : f x ≠ x)
    [DecidableRel f.SameCycle] [DecidableEq α] [Fintype α] :
    y ∈ support (f.cycleOf x) ↔ SameCycle f x y

Proof state:
α : Type u_2
f : Perm α
x y : α
hx : f x ≠ x
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y

Tactic:
rw [mem_support_cycleOf_iff_aux, and_iff_left (mem_support.2 hx)]

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_lt_one_eq_self_of_isOpen (hs₁ : Convex ℝ s) (hs₀ : (0 : E) ∈ s) (hs₂ : IsOpen s) :
    { x | gauge s x < 1 } = s

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : IsOpen s
⊢ {x | gauge s x < 1} = s

Tactic:
refine (gauge_lt_one_subset_self hs₁ ‹_› <| absorbent_nhds_zero <| hs₂.mem_nhds hs₀).antisymm ?_

Result:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : IsOpen s
⊢ s ⊆ {x | gauge s x < 1}

Proof state:
case h.e'_3
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : IsOpen s
⊢ s = interior s

Tactic:
exact hs₂.interior_eq.symm

Result:
no goals

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : IsOpen s
⊢ s ⊆ {x | gauge s x < 1}

Tactic:
convert interior_subset_gauge_lt_one s

Result:
case h.e'_3
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : IsOpen s
⊢ s = interior s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_lt_mul_of_neg_right {a b c : Int} (h : b < a) (hc : c < 0) : a * c < b * c :=
  have : -c > 0 := Int.neg_pos_of_neg hc
  have : b * -c < a * -c := Int.mul_lt_mul_of_pos_right h this
  have : -(b * c) < -(a * c)

Proof state:
a b c : Int
h : b < a
hc : c < 0
this✝ : -c > 0
this : b * -c < a * -c
⊢ -(b * c) < -(a * c)

Tactic:
rwa [← Int.neg_mul_eq_mul_neg, ← Int.neg_mul_eq_mul_neg] at this

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem frontier_setOf_im_le (a : ℝ) : frontier { z : ℂ | z.im ≤ a } = { z | z.im = a }

Proof state:
a : ℝ
⊢ frontier {z | z.im ≤ a} = {z | z.im = a}

Tactic:
simpa only [frontier_Iic] using frontier_preimage_im (Iic a)

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem C_mul_X_eq_monomial {s : σ} {a : R} : C a * X s = monomial (Finsupp.single s 1) a

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
⊢ C a * X s = (monomial (Finsupp.single s 1)) a

Tactic:
rw [← C_mul_X_pow_eq_monomial, pow_one]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem eq_of_prime_pow_eq (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₁ : 0 < k₁)
    (h : p₁ ^ k₁ = p₂ ^ k₂) : p₁ = p₂

Proof state:
R : Type u_2
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂

Tactic:
apply h.of_pow_associated_of_prime hp₁ hp₂ hk₁

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ = p₂ ^ k₂
⊢ p₁ = p₂

Tactic:
rw [← associated_iff_eq] at h ⊢

Result:
R : Type u_2
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_eq_mapFinIdx_iff {l : Vector α n} {f g : (i : Nat) → α → (h : i < n) → β} :
    l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < n), f i l[i] h = g i l[i] h

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f g : (i : Nat) → α → i < n → β
⊢ l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < n), f i l[i] h = g i l[i] h

Tactic:
rw [eq_comm, mapFinIdx_eq_iff]

Result:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f g : (i : Nat) → α → i < n → β
⊢ (∀ (i : Nat) (h : i < n), (l.mapFinIdx f)[i] = g i l[i] h) ↔ ∀ (i : Nat) (h : i < n), f i l[i] h = g i l[i] h

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f g : (i : Nat) → α → i < n → β
⊢ (∀ (i : Nat) (h : i < n), (l.mapFinIdx f)[i] = g i l[i] h) ↔ ∀ (i : Nat) (h : i < n), f i l[i] h = g i l[i] h

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List ((a : α) × β a)}
    {k k' fallback : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Sigma.fst) :
    (m.insertMany l).1.getKeyD k' fallback = k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List ((a : α) × β a)
k k' fallback : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Sigma.fst l
⊢ (m.insertMany l).val.getKeyD k' fallback = k

Tactic:
simp_to_model [insertMany] using List.getKeyD_insertList_of_mem

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
theorem quasispectrumRestricts_iff_spectrumRestricts {R S A : Type*} [Semifield R] [Semifield S]
    [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} :
    QuasispectrumRestricts a f ↔ SpectrumRestricts a f

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
⊢ QuasispectrumRestricts a f ↔ SpectrumRestricts a f

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
theorem strictConcaveOn_of_deriv2_neg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
    (hf : ContinuousOn f D) (hf'' : ∀ x ∈ interior D, deriv^[2] f x < 0) :
    StrictConcaveOn ℝ D f :=
  ((strictAntiOn_of_deriv_neg hD.interior fun z hz =>
          (differentiableAt_of_deriv_ne_zero
                (hf'' z hz).ne).differentiableWithinAt.continuousWithinAt) <|
        by rwa [interior_interior]).strictConcaveOn_of_deriv
    hD hf

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf'' : ∀ x ∈ interior D, deriv^[2] f x < 0
⊢ ∀ x ∈ interior (interior D), deriv (deriv f) x < 0

Tactic:
rwa [interior_interior]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_add_self_right {m n : ℕ} : Coprime m (n + m) ↔ Coprime m n

Proof state:
m n : ℕ
⊢ m.Coprime (n + m) ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_add_self_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.extract_toArray (l : List α) (start stop : Nat) :
    l.toArray.extract start stop = (l.extract start stop).toArray

Proof state:
α : Type u_1
l : List α
start stop : Nat
⊢ l.toArray.extract start stop = (l.extract start stop).toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
l : List α
start stop : Nat
⊢ (l.toArray.extract start stop).toList = (l.extract start stop).toArray.toList

Proof state:
case h
α : Type u_1
l : List α
start stop : Nat
⊢ (l.toArray.extract start stop).toList = (l.extract start stop).toArray.toList

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem mul_one (a : Int) : a * 1 = a

Proof state:
a : Int
⊢ a * 1 = a

Tactic:
rw [Int.mul_comm, Int.one_mul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem edges_map : (p.map f).edges = p.edges.map (Sym2.map f)

Proof state:
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ : V
⊢ (Walk.map f nil).edges = List.map (Sym2.map ⇑f) nil.edges

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
⊢ (Walk.map f p).edges = List.map (Sym2.map ⇑f) p.edges

Tactic:
induction p with
| nil => rfl
| cons _ _ ih =>
  simp only [Walk.map_cons, edges_cons, List.map_cons, Sym2.map_pair_eq, List.cons.injEq,
    true_and, ih]

Result:
no goals

Proof state:
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (Walk.map f p✝).edges = List.map (Sym2.map ⇑f) p✝.edges
⊢ (Walk.map f (cons h✝ p✝)).edges = List.map (Sym2.map ⇑f) (cons h✝ p✝).edges

Tactic:
simp only [Walk.map_cons, edges_cons, List.map_cons, Sym2.map_pair_eq, List.cons.injEq,
  true_and, ih]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem inv_hom_whiskerRight' {X Y : C} (f : X ⟶ Y) [IsIso f] (Z : C) :
    inv f ▷ Z ≫ f ▷ Z = 𝟙 (Y ⊗ Z)

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

Tactic:
rw [← comp_whiskerRight, IsIso.inv_hom_id, id_whiskerRight]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem lcm_union [DecidableEq β] : (s₁ ∪ s₂).lcm f = GCDMonoid.lcm (s₁.lcm f) (s₂.lcm f) :=
  Finset.induction_on s₁ (by rw [empty_union, lcm_empty, lcm_one_left, normalize_lcm])
    fun a s _ ih ↦ by rw [insert_union, lcm_insert, lcm_insert, ih, lcm_assoc]

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ (∅ ∪ s₂).lcm f = GCDMonoid.lcm (∅.lcm f) (s₂.lcm f)

Tactic:
rw [empty_union, lcm_empty, lcm_one_left, normalize_lcm]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : a ∉ s
ih : (s ∪ s₂).lcm f = GCDMonoid.lcm (s.lcm f) (s₂.lcm f)
⊢ (insert a s ∪ s₂).lcm f = GCDMonoid.lcm ((insert a s).lcm f) (s₂.lcm f)

Tactic:
rw [insert_union, lcm_insert, lcm_insert, ih, lcm_assoc]

Result:
no goals