harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem exists_lt_norm (r : ℝ) : ∃ x : α, r < ‖x‖ :=
  let ⟨w, hw⟩ := exists_one_lt_norm α
  let ⟨n, hn⟩ := pow_unbounded_of_one_lt r hw
  ⟨w ^ n, by rwa [norm_pow]⟩

Proof state:
α : Type u_2
inst✝ : NontriviallyNormedField α
r : ℝ
w : α
hw : 1 < ‖w‖
n : ℕ
hn : r < ‖w‖ ^ n
⊢ r < ‖w ^ n‖

Tactic:
rwa [norm_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_of_forall {l : List α} (H : ∀ x y, R x y) : Pairwise R l

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
H : ∀ (x y : α), R x y
⊢ Pairwise R l

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Topology/Instances/Int.lean
theorem closedBall_eq_Icc (x : ℤ) (r : ℝ) : closedBall x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋

Proof state:
x : ℤ
r : ℝ
⊢ closedBall x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋

Tactic:
rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp)]
lemma inv_inter (s t : Finset α) : (s ∩ t)⁻¹ = s⁻¹ ∩ t⁻¹ := coe_injective <| by simp

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : InvolutiveInv α
s t : Finset α
⊢ ↑(s ∩ t)⁻¹ = ↑(s⁻¹ ∩ t⁻¹)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem vectorSpan_pair (p₁ p₂ : P) : vectorSpan k ({p₁, p₂} : Set P) = k ∙ p₁ -ᵥ p₂

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
⊢ vectorSpan k {p₁, p₂} = Submodule.span k {p₁ -ᵥ p₂}

Tactic:
simp_rw [vectorSpan_eq_span_vsub_set_left k (mem_insert p₁ _), image_pair, vsub_self,
  Submodule.span_insert_zero]

Result:
no goals
-- Mathlib/Analysis/Polynomial/CauchyBound.lean
@[simp]
lemma one_le_cauchyBound (p : K[X]) : 1 ≤ cauchyBound p

Proof state:
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
⊢ 1 ≤ p.cauchyBound

Tactic:
simp [cauchyBound]

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem card_singleton (a : α) : card ({a} : Multiset α) = 1

Proof state:
α : Type u_1
a : α
⊢ {a}.card = 1

Tactic:
simp only [← cons_zero, card_zero, eq_self_iff_true, card_cons]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem smul_integral_comp_mul_left (c) :
    (c • ∫ x in a..b, f (c * x)) = ∫ x in c * a..c * b, f x

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

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

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem toReal_rpow (x : ℝ≥0∞) (z : ℝ) : x.toReal ^ z = (x ^ z).toReal

Proof state:
x : ℝ≥0∞
z : ℝ
⊢ x.toReal ^ z = (x ^ z).toReal

Tactic:
rw [ENNReal.toReal, ENNReal.toReal, ← NNReal.coe_rpow, ENNReal.toNNReal_rpow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p

Proof state:
p : Prop
h : Decidable p
⊢ ((!decide p) = true) = ¬p

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Bounds.lean
/-- The value at a unit of a Dirichlet character with target a normed field has norm `1`. -/
@[simp] lemma unit_norm_eq_one (a : (ZMod n)ˣ) : ‖χ a‖ = 1

Proof state:
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : (ZMod n)ˣ
⊢ ‖χ ↑a‖ = 1

Tactic:
refine (pow_eq_one_iff_of_nonneg (norm_nonneg _) (Nat.card_pos (α := (ZMod n)ˣ)).ne').mp ?_

Result:
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : (ZMod n)ˣ
⊢ ‖χ ↑a‖ ^ Nat.card (ZMod n)ˣ = 1

Proof state:
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : (ZMod n)ˣ
⊢ ‖χ ↑a‖ ^ Nat.card (ZMod n)ˣ = 1

Tactic:
rw [← norm_pow, ← map_pow, ← Units.val_pow_eq_pow_val, pow_card_eq_one', Units.val_one, map_one,
  norm_one]

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem map_add (n m k : ℕ) : (Ico n m).map (k + ·) = Ico (n + k) (m + k)

Proof state:
n m k : ℕ
⊢ map (fun x => k + x) (Ico n m) = Ico (n + k) (m + k)

Tactic:
rw [Ico, Ico, map_add_range', Nat.add_sub_add_right m k, Nat.add_comm n k]

Result:
no goals
-- Mathlib/Topology/DenseEmbedding.lean
theorem mk' (i : α → β) (c : Continuous i) (dense : ∀ x, x ∈ closure (range i))
    (H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (i a), ∀ b, i b ∈ t → b ∈ s) : IsDenseInducing i where
  toIsInducing := isInducing_iff_nhds.2 fun a =>
      le_antisymm (c.tendsto _).le_comap (by simpa [Filter.le_def] using H a)
  dense := dense

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
c : Continuous i
dense : ∀ (x : β), x ∈ closure (range i)
H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (i a), ∀ (b : α), i b ∈ t → b ∈ s
a : α
⊢ comap i (𝓝 (i a)) ≤ 𝓝 a

Tactic:
simpa [Filter.le_def] using H a

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma _root_.Odd.not_two_dvd_nat (h : Odd n) : ¬(2 ∣ n)

Proof state:
n : ℕ
h : Odd n
⊢ ¬2 ∣ n

Tactic:
rwa [← even_iff_two_dvd, not_even_iff_odd]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
@[simp] lemma bot_lt_iSup : ⊥ < ⨆ i, s i ↔ ∃ i, ⊥ < s i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
s : ι → α
⊢ ⊥ < ⨆ i, s i ↔ ∃ i, ⊥ < s i

Tactic:
simp [bot_lt_iff_ne_bot]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem add_mod_add_of_le_add_mod {a b c : ℕ} (hc : c ≤ a % c + b % c) :
    (a + b) % c + c = a % c + b % c

Proof state:
a b c : ℕ
hc : c ≤ a % c + b % c
⊢ (a + b) % c + c = a % c + b % c

Tactic:
rw [← add_mod_add_ite, if_pos hc]

Result:
no goals
-- Mathlib/Analysis/MellinTransform.lean
theorem mellin_cpow_smul (f : ℝ → E) (s a : ℂ) :
    mellin (fun t => (t : ℂ) ^ a • f t) s = mellin f (s + a)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s a : ℂ
⊢ mellin (fun t => ↑t ^ a • f t) s = mellin f (s + a)

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s a : ℂ
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • (fun t => ↑t ^ a • f t) t = ↑t ^ (s + a - 1) • f t

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s a : ℂ
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • (fun t => ↑t ^ a • f t) t = ↑t ^ (s + a - 1) • f t

Tactic:
simp_rw [← sub_add_eq_add_sub, cpow_add _ _ (ofReal_ne_zero.2 <| ne_of_gt ht), mul_smul]

Result:
no goals
-- Mathlib/Topology/Order/LowerUpperTopology.lean
theorem isOpen_iff_generate_Iic_compl : IsOpen s ↔ GenerateOpen { t | ∃ a, (Iic a)ᶜ = t } s

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsUpper α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {t | ∃ a, (Iic a)ᶜ = t} s

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem closure_singleton_one : closure ({1} : Set G) = ⊥

Proof state:
G : Type u_1
inst✝ : Group G
⊢ closure {1} = ⊥

Tactic:
simp [eq_bot_iff_forall, mem_closure_singleton]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem len_le_of_epi {x y : SimplexCategory} {f : x ⟶ y} : Epi f → y.len ≤ x.len

Proof state:
x y : SimplexCategory
f : x ⟶ y
⊢ Epi f → y.len ≤ x.len

Tactic:
intro hyp_f_epi

Result:
x y : SimplexCategory
f : x ⟶ y
hyp_f_epi : Epi f
⊢ y.len ≤ x.len

Proof state:
x y : SimplexCategory
f : x ⟶ y
hyp_f_epi : Epi f
f_surj : Function.Surjective (Hom.toOrderHom f).toFun
⊢ y.len ≤ x.len

Tactic:
simpa using Fintype.card_le_of_surjective f.toOrderHom.toFun f_surj

Result:
no goals

Proof state:
x y : SimplexCategory
f : x ⟶ y
hyp_f_epi : Epi f
⊢ y.len ≤ x.len

Tactic:
have f_surj : Function.Surjective f.toOrderHom.toFun := epi_iff_surjective.1 hyp_f_epi

Result:
x y : SimplexCategory
f : x ⟶ y
hyp_f_epi : Epi f
f_surj : Function.Surjective (Hom.toOrderHom f).toFun
⊢ y.len ≤ x.len
-- Mathlib/Data/Nat/Nth.lean
theorem nth_zero_of_zero (h : p 0) : nth p 0 = 0

Proof state:
p : ℕ → Prop
h : p 0
⊢ nth p 0 = 0

Tactic:
simp [nth_zero, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lcm.lean
theorem lcm_zero_right (m : Nat) : lcm m 0 = 0

Proof state:
m : Nat
⊢ m.lcm 0 = 0

Tactic:
simp [lcm]

Result:
no goals
-- Mathlib/Algebra/Group/Operations.lean
@[to_additive]
lemma dite_div_dite (a : P → α) (b : ¬ P → α) (c : P → α) (d : ¬ P → α) :
    ((if h : P then a h else b h) / if h : P then c h else d h) =
      if h : P then a h / c h else b h / d h

Proof state:
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
⊢ ((if h : P then a h else b h) / if h : P then c h else d h) = if h : P then a h / c h else b h / d h

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem repeat_eq_append1 {β} {n} (α : TypeVec n) :
    repeatEq (α ::: β) = splitFun (α := (α ⊗ α) ::: _)
    (α' := («repeat» n Prop) ::: _) (repeatEq α) (uncurry Eq)

Proof state:
β : Type u_1
n : ℕ
α : TypeVec.{u_1} n
⊢ (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)

Tactic:
induction n <;> rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem deleteEdges_inter_edgeSet_left_eq :
    G'.deleteEdges (G'.edgeSet ∩ s) = G'.deleteEdges s

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ G'.deleteEdges (G'.edgeSet ∩ s) = G'.deleteEdges s

Tactic:
ext <;> simp +contextual [imp_false]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem or_comm : ∀ (x y : Bool), (x || y) = (y || x)

Proof state:
⊢ ∀ (x y : Bool), (x || y) = (y || x)

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem sum_zero_index {S : Type*} [AddCommMonoid S] {f : G → k → S} :
    (0 : SkewMonoidAlgebra k G).sum f = 0

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : AddCommMonoid S
f : G → k → S
⊢ sum 0 f = 0

Tactic:
simp [sum]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem eq_of_mem_smul_span_of_index_eq_index {x y : ι → ℝ} (hx : x ∈ (n : ℝ)⁻¹ • L)
    (hy : y ∈ (n : ℝ)⁻¹ • L) (h : index n x = index n y) : x = y

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
x y : ι → ℝ
hx : x ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))
hy : y ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))
h : index n x = index n y
⊢ x = y

Tactic:
rw [← tag_index_eq_self_of_mem_smul_span n hx, ← tag_index_eq_self_of_mem_smul_span n hy, h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
lemma dvd_comp_neg_X_iff (p q : R[X]) : p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
x✝¹ : Invertible 1 := invertibleOne
x✝ : Invertible (-1) := invertibleNeg 1
⊢ p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q

Tactic:
simpa using dvd_comp_C_mul_X_add_C_iff p q (-1) 0

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
⊢ p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q

Tactic:
let _ := invertibleOne (α := R)

Result:
R : Type u
inst✝ : CommRing R
p q : R[X]
x✝ : Invertible 1 := invertibleOne
⊢ p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
x✝ : Invertible 1 := invertibleOne
⊢ p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q

Tactic:
let _ := invertibleNeg (α := R) 1

Result:
R : Type u
inst✝ : CommRing R
p q : R[X]
x✝¹ : Invertible 1 := invertibleOne
x✝ : Invertible (-1) := invertibleNeg 1
⊢ p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_zero_left_eq_zero : logb 0 = 0

Proof state:
case h
x✝ : ℝ
⊢ logb 0 x✝ = 0 x✝

Tactic:
rw [logb_zero_left, Pi.zero_apply]

Result:
no goals

Proof state:
⊢ logb 0 = 0

Tactic:
ext

Result:
case h
x✝ : ℝ
⊢ logb 0 x✝ = 0 x✝
-- Mathlib/Topology/Maps/Basic.lean
theorem isClosed_iff (hf : IsInducing f) {s : Set X} :
    IsClosed s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsClosed s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s

Tactic:
rw [hf.eq_induced, isClosed_induced_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem mem_eraseIdx_iff_getElem? {x : α} {l : Vector α n} {k} {h} : x ∈ eraseIdx l k h ↔ ∃ i ≠ k, l[i]? = some x

Proof state:
case mk
α : Type u_1
x : α
k : Nat
l : Array α
h : k < l.size
⊢ x ∈ { toArray := l, size_toArray := ⋯ }.eraseIdx k h ↔ ∃ i, i ≠ k ∧ { toArray := l, size_toArray := ⋯ }[i]? = some x

Tactic:
simp [Array.mem_eraseIdx_iff_getElem?, *]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
x : α
l : Vector α n
k : Nat
h : k < n
⊢ x ∈ l.eraseIdx k h ↔ ∃ i, i ≠ k ∧ l[i]? = some x

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
x : α
k : Nat
l : Array α
h : k < l.size
⊢ x ∈ { toArray := l, size_toArray := ⋯ }.eraseIdx k h ↔ ∃ i, i ≠ k ∧ { toArray := l, size_toArray := ⋯ }[i]? = some x
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
theorem ext_ring {f g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) : f = g :=
  ext fun x ↦ by rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]

Proof state:
R : Type u_1
S : Type u_5
M₃ : Type u_11
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M₃
inst✝ : Module S M₃
σ : R →+* S
f g : R →ₛₗ[σ] M₃
h : f 1 = g 1
x : R
⊢ f x = g x

Tactic:
rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.pentagon [HasBinaryProducts C] (W X Y Z : C) :
    prod.map (prod.associator W X Y).hom (𝟙 Z) ≫
        (prod.associator W (X ⨯ Y) Z).hom ≫ prod.map (𝟙 W) (prod.associator X Y Z).hom =
      (prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y ⨯ Z)).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryProducts C
W X Y Z : C
⊢ map (associator W X Y).hom (𝟙 Z) ≫ (associator W (X ⨯ Y) Z).hom ≫ map (𝟙 W) (associator X Y Z).hom =
    (associator (W ⨯ X) Y Z).hom ≫ (associator W X (Y ⨯ Z)).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
theorem map_smul : X (r • f) = r • X f

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
r : 𝕜
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ X (r • f) = r • X f

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Setoid/Partition.lean
theorem rel_iff_exists_classes (r : Setoid α) {x y} : r x y ↔ ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c :=
  ⟨fun h => ⟨_, r.mem_classes y, h, r.refl' y⟩, fun ⟨c, ⟨z, hz⟩, hx, hy⟩ => by
    subst c
    exact r.trans' hx (r.symm' hy)⟩

Proof state:
α : Type u_1
r : Setoid α
x y : α
x✝ : ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c
c : Set α
z : α
hz : c = {x | r x z}
hx : x ∈ c
hy : y ∈ c
⊢ r x y

Tactic:
subst c

Result:
α : Type u_1
r : Setoid α
x y : α
x✝ : ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c
z : α
hx : x ∈ {x | r x z}
hy : y ∈ {x | r x z}
⊢ r x y

Proof state:
α : Type u_1
r : Setoid α
x y : α
x✝ : ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c
z : α
hx : x ∈ {x | r x z}
hy : y ∈ {x | r x z}
⊢ r x y

Tactic:
exact r.trans' hx (r.symm' hy)

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Properties.lean
theorem dualBasis_repr_apply
    (B : BilinForm K V) (hB : B.Nondegenerate) (b : Basis ι K V) (x i) :
    (B.dualBasis hB b).repr x i = B x (b i)

Proof state:
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
x : V
i : ι
⊢ ((B.dualBasis hB b).repr x) i = (B x) (b i)

Tactic:
rw [dualBasis, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
  Basis.dualBasis_repr, @toDual_def]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem id_compRel {r : Set (α × α)} : idRel ○ r = r :=
  Set.ext fun ⟨a, b⟩ => by simp

Proof state:
α : Type ua
r : Set (α × α)
x✝ : α × α
a b : α
⊢ (a, b) ∈ idRel ○ r ↔ (a, b) ∈ r

Tactic:
simp

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_const [Nonempty ι] : ⨆ _ : ι, a = a

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
a : α
inst✝ : Nonempty ι
⊢ ⨆ x, a = a

Tactic:
rw [iSup, range_const, sSup_singleton]

Result:
no goals
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem lsum_single [Semiring S] [Module S N] [SMulCommClass R S N] (F : ∀ i, M i →ₗ[R] N) (i)
    (x : M i) : lsum S (M := M) F (single i x) = F i x

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : ι → Type u_4
N : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
i : ι
x : M i
⊢ ((lsum S) F) (single i x) = (F i) x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem submatrix_mul_transpose_submatrix [Fintype m] [Fintype n] [AddCommMonoid α] [Mul α]
    (e : m ≃ n) (M : Matrix m n α) : M.submatrix id e * Mᵀ.submatrix e id = M * Mᵀ

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
e : m ≃ n
M : Matrix m n α
⊢ M.submatrix id ⇑e * Mᵀ.submatrix (⇑e) id = M * Mᵀ

Tactic:
rw [submatrix_mul_equiv, submatrix_id_id]

Result:
no goals
-- Mathlib/Algebra/Ring/Rat.lean
@[simp] lemma divInt_pow (num : ℕ) (den : ℤ) (n : ℕ) : (num /. den) ^ n = num ^ n /. den ^ n

Proof state:
num : ℕ
den : ℤ
n : ℕ
⊢ (↑num /. den) ^ n = ↑num ^ n /. den ^ n

Tactic:
simp [divInt_eq_div, div_pow, Int.natCast_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem Nodup.not_mem_erase [LawfulBEq α] {a : α} (h : Nodup l) : a ∉ l.erase a := fun H => by
  simpa using ((Nodup.mem_erase_iff h).mp H).left

Proof state:
α : Type u_1
inst✝¹ : BEq α
l : List α
inst✝ : LawfulBEq α
a : α
h : l.Nodup
H : a ∈ l.erase a
⊢ False

Tactic:
simpa using ((Nodup.mem_erase_iff h).mp H).left

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma fst_injOn_graph : (s.graphOn f).InjOn Prod.fst

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ InjOn Prod.fst (graphOn f s)

Tactic:
aesop (add simp InjOn)

Result:
no goals
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem MemLp.integral_indicator_norm_ge_nonneg_le_of_meas (hf : MemLp f 1 μ)
    (hmeas : StronglyMeasurable f) {ε : ℝ} (hε : 0 < ε) :
    ∃ M : ℝ, 0 ≤ M ∧ (∫⁻ x, ‖{ x | M ≤ ‖f x‖₊ }.indicator f x‖ₑ ∂μ) ≤ ENNReal.ofReal ε :=
  let ⟨M, hM⟩ := hf.integral_indicator_norm_ge_le hmeas hε
  ⟨max M 0, le_max_right _ _, by simpa⟩

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
⊢ ∫⁻ (x : α), ‖{x | M ⊔ 0 ≤ ↑‖f x‖₊}.indicator f x‖ₑ ∂μ ≤ ENNReal.ofReal ε

Tactic:
simpa

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma limitRightOpIsoOpColimit_hom_comp_ι (F : Jᵒᵖ ⥤ C) [HasColimit F] (j : Jᵒᵖ) :
    (limitRightOpIsoOpColimit F).hom ≫ (colimit.ι F j).op = limit.π F.rightOp j.unop

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
inst✝ : HasColimit F
j : Jᵒᵖ
⊢ (limitRightOpIsoOpColimit F).hom ≫ (colimit.ι F j).op = limit.π F.rightOp (unop j)

Tactic:
simp [← Iso.eq_inv_comp]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tan_neg : tan (-x) = -tan x

Proof state:
x : ℝ
⊢ tan (-x) = -tan x

Tactic:
simp [tan, neg_div]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem cons_dotProduct_cons (x : α) (v : Fin n → α) (y : α) (w : Fin n → α) :
    dotProduct (vecCons x v) (vecCons y w) = x * y + dotProduct v w

Proof state:
α : Type u
n : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v ⬝ᵥ vecCons y w = x * y + v ⬝ᵥ w

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Algebra/Tower.lean
theorem of_algebraMap_smul [SMul R M] (h : ∀ (r : R) (x : M), algebraMap R A r • x = r • x) :
    IsScalarTower R A M where
  smul_assoc r a x

Proof state:
R : Type u
A : Type w
M : Type v₁
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : MulAction A M
inst✝ : SMul R M
h : ∀ (r : R) (x : M), (algebraMap R A) r • x = r • x
r : R
a : A
x : M
⊢ (r • a) • x = r • a • x

Tactic:
rw [Algebra.smul_def, mul_smul, h]

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.monotone (h : ωScottContinuous f) : Monotone f :=
  ScottContinuousOn.monotone _ (fun a b hab => by
    use pair a b hab; exact range_pair a b hab) h

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
h : ωScottContinuous f
a b : α
hab : a ≤ b
⊢ {a, b} ∈ Set.range fun c => Set.range ⇑c

Tactic:
use pair a b hab

Result:
case h
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
h : ωScottContinuous f
a b : α
hab : a ≤ b
⊢ (fun c => Set.range ⇑c) (pair a b hab) = {a, b}

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
h : ωScottContinuous f
a b : α
hab : a ≤ b
⊢ (fun c => Set.range ⇑c) (pair a b hab) = {a, b}

Tactic:
exact range_pair a b hab

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
theorem dvd_abs (a b : α) : a ∣ |b| ↔ a ∣ b

Proof state:
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a b : α
⊢ a ∣ |b| ↔ a ∣ b

Tactic:
rcases abs_choice b with h | h <;> simp only [h, dvd_neg]

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem lt_cauchy {f g} : (⟨⟦f⟧⟩ : ℝ) < ⟨⟦g⟧⟩ ↔ f < g :=
  show lt _ _ ↔ _ by rw [lt_def]; rfl

Proof state:
f g : CauSeq ℚ abs
⊢ Real.lt { cauchy := ⟦f⟧ } { cauchy := ⟦g⟧ } ↔ f < g

Tactic:
rw [lt_def]

Result:
f g : CauSeq ℚ abs
⊢ (match { cauchy := ⟦f⟧ }, { cauchy := ⟦g⟧ } with
    | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x1 x2 => x1 < x2) Real.definition.proof_1✝) ↔
    f < g

Proof state:
f g : CauSeq ℚ abs
⊢ (match { cauchy := ⟦f⟧ }, { cauchy := ⟦g⟧ } with
    | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x1 x2 => x1 < x2) Real.definition.proof_1✝) ↔
    f < g

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_liminf {s : ℕ → Set α} (hs : ∀ n, MeasurableSet <| s n) :
    MeasurableSet <| Filter.liminf s Filter.atTop

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ MeasurableSet (liminf s atTop)

Tactic:
simpa only [← bliminf_true] using measurableSet_bliminf fun n _ => hs n

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_sum (k : ℕ) (s : Finset ι) (f : ι → R[X]) :
    derivative^[k] (∑ b ∈ s, f b) = ∑ b ∈ s, derivative^[k] (f b)

Proof state:
R : Type u
ι : Type y
inst✝ : Semiring R
k : ℕ
s : Finset ι
f : ι → R[X]
⊢ (⇑derivative)^[k] (∑ b ∈ s, f b) = ∑ b ∈ s, (⇑derivative)^[k] (f b)

Tactic:
simp_rw [← LinearMap.pow_apply, map_sum]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem isSheafFor_subsieve (P : Cᵒᵖ ⥤ Type w) {S : Sieve X} {R : Presieve X}
    (h : (S : Presieve X) ≤ R) (trans : ∀ ⦃Y⦄ (f : Y ⟶ X),
      IsSheafFor P (S.pullback f : Presieve Y)) :
    IsSheafFor P R :=
  isSheafFor_subsieve_aux P h (by simpa using trans (𝟙 _)) fun _ f _ => (trans f).isSeparatedFor

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
trans : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f S).arrows
⊢ IsSheafFor P S.arrows

Tactic:
simpa using trans (𝟙 _)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem add_sub_add_cancel (a b c : Ordinal) : a + b - (a + c) = b - c

Proof state:
a b c : Ordinal.{u_4}
⊢ a + b - (a + c) = b - c

Tactic:
rw [← sub_sub, add_sub_cancel]

Result:
no goals