harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_add_tsub_cancel (hab : b ≤ a) (hcb : c ≤ b) : a - b + (b - c) = a - c

Proof state:
case h.e'_2.h.e'_5
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b = a - c - (b - c)

Tactic:
rw [tsub_tsub, add_tsub_cancel_of_le hcb]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b + (b - c) = a - c

Tactic:
convert tsub_add_cancel_of_le (tsub_le_tsub_right hab c) using 2

Result:
case h.e'_2.h.e'_5
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b = a - c - (b - c)
-- Mathlib/Order/Heyting/Basic.lean
theorem ne_compl_self [Nontrivial α] : a ≠ aᶜ

Proof state:
α : Type u_2
inst✝¹ : HeytingAlgebra α
a : α
inst✝ : Nontrivial α
⊢ a ≠ aᶜ

Tactic:
intro h

Result:
α : Type u_2
inst✝¹ : HeytingAlgebra α
a : α
inst✝ : Nontrivial α
h : a = aᶜ
⊢ False

Proof state:
case refl
α : Type u_2
inst✝¹ : HeytingAlgebra α
inst✝ : Nontrivial α
h : ⊥ = ⊥ᶜ
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : HeytingAlgebra α
a : α
inst✝ : Nontrivial α
h : a = aᶜ
⊢ False

Tactic:
cases le_compl_self.1 (le_of_eq h)

Result:
case refl
α : Type u_2
inst✝¹ : HeytingAlgebra α
inst✝ : Nontrivial α
h : ⊥ = ⊥ᶜ
⊢ False
-- Mathlib/Data/Complex/Basic.lean
theorem I_mul_re (z : ℂ) : (I * z).re = -z.im

Proof state:
z : ℂ
⊢ (I * z).re = -z.im

Tactic:
simp

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem pow_add_period_smul (n : ℕ) (m : M) (a : α) :
    m ^ (n + period m a) • a = m ^ n • a

Proof state:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ (n + period m a) • a = m ^ n • a

Tactic:
rw [← pow_mod_period_smul, Nat.add_mod_right, pow_mod_period_smul]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_bsup_le {o : Ordinal} {f : ∀ a < o, Ordinal} :
    (∀ i h, f i h < bsup.{u, u} o f) → cof (bsup.{u, u} o f) ≤ o.card

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ o.card

Tactic:
rw [← o.card.lift_id]

Result:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ Cardinal.lift.{u, u} o.card

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ Cardinal.lift.{u, u} o.card

Tactic:
exact cof_bsup_le_lift

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Slope.lean
theorem lineMap_slope_slope_sub_div_sub (f : k → PE) (a b c : k) (h : a ≠ c) :
    lineMap (slope f a b) (slope f b c) ((c - b) / (c - a)) = slope f a c

Proof state:
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
h : a ≠ c
⊢ (lineMap (slope f a b) (slope f b c)) ((c - b) / (c - a)) = slope f a c

Tactic:
field_simp [sub_ne_zero.2 h.symm, ← sub_div_sub_smul_slope_add_sub_div_sub_smul_slope f a b c,
  lineMap_apply_module]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma hurwitzZetaOdd_neg (a : UnitAddCircle) (s : ℂ) :
    hurwitzZetaOdd (-a) s = -hurwitzZetaOdd a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaOdd (-a) s = -hurwitzZetaOdd a s

Tactic:
simp_rw [hurwitzZetaOdd, completedHurwitzZetaOdd_neg, neg_div]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Schur.lean
theorem finrank_hom_simple_simple_eq_zero_iff (X Y : C) [FiniteDimensional 𝕜 (X ⟶ X)]
    [FiniteDimensional 𝕜 (X ⟶ Y)] [Simple X] [Simple Y] :
    finrank 𝕜 (X ⟶ Y) = 0 ↔ IsEmpty (X ≅ Y)

Proof state:
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 0 ↔ IsEmpty (X ≅ Y)

Tactic:
rw [← not_nonempty_iff, ← not_congr (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y)]

Result:
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 0 ↔ ¬finrank 𝕜 (X ⟶ Y) = 1

Proof state:
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
this : finrank 𝕜 (X ⟶ Y) ≤ 1
⊢ finrank 𝕜 (X ⟶ Y) = 0 ↔ ¬finrank 𝕜 (X ⟶ Y) = 1

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 0 ↔ ¬finrank 𝕜 (X ⟶ Y) = 1

Tactic:
have := finrank_hom_simple_simple_le_one 𝕜 X Y

Result:
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
this : finrank 𝕜 (X ⟶ Y) ≤ 1
⊢ finrank 𝕜 (X ⟶ Y) = 0 ↔ ¬finrank 𝕜 (X ⟶ Y) = 1
-- Mathlib/Tactic/NormNum/Inv.lean
theorem isRat_inv_zero {α} [DivisionRing α] : {a : α} →
    IsNat a (nat_lit 0) → IsNat a⁻¹ (nat_lit 0)
  | _, ⟨rfl⟩ => ⟨by simp⟩

Proof state:
α : Type u_1
inst✝ : DivisionRing α
⊢ (↑0)⁻¹ = ↑0

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem isPiSystem_image_Iic (s : Set α) : IsPiSystem (Iic '' s)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ IsPiSystem (Iic '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ -

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Iic a ∩ Iic b ∈ Iic '' s

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Iic a ∩ Iic b ∈ Iic '' s

Tactic:
exact ⟨a ⊓ b, inf_ind a b ha hb, Iic_inter_Iic.symm⟩

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_mul_const_le (r : ℝ≥0∞) (f : α → ℝ≥0∞) :
    (∫⁻ a, f a ∂μ) * r ≤ ∫⁻ a, f a * r ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ (∫⁻ (a : α), f a ∂μ) * r ≤ ∫⁻ (a : α), f a * r ∂μ

Tactic:
simp_rw [mul_comm, lintegral_const_mul_le r f]

Result:
no goals
-- Mathlib/RingTheory/Localization/Ideal.lean
lemma algebraMap_mem_map_algebraMap_iff (I : Ideal R) (x : R) :
    algebraMap R S x ∈ I.map (algebraMap R S) ↔
      ∃ m ∈ M, m * x ∈ I

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
x : R
⊢ (algebraMap R S) x ∈ Ideal.map (algebraMap R S) I ↔ ∃ m ∈ M, m * x ∈ I

Tactic:
rw [← IsLocalization.mk'_one (M := M), mk'_mem_map_algebraMap_iff]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem seq_def {s : Set (α → β)} {t : Set α} : seq s t = ⋃ f ∈ s, f '' t

Proof state:
α : Type u_1
β : Type u_2
s : Set (α → β)
t : Set α
⊢ s.seq t = ⋃ f ∈ s, f '' t

Tactic:
rw [seq_eq_image2, iUnion_image_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_mkArray_of_isSome {f : α → Option β} (h : (f a).isSome) :
    (mkArray n a).filterMap f = mkArray n (Option.get _ h)

Proof state:
α : Type u_1
β : Type u_2
a : α
n : Nat
f : α → Option β
h : (f a).isSome = true
⊢ filterMap f (mkArray n a) = mkArray n ((f a).get h)

Tactic:
match w : f a, h with
| some b, _ => simp [filterMap_mkArray, h, w]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
n : Nat
f : α → Option β
h : (f a).isSome = true
b : β
x✝ : (some b).isSome = true
w : f a = some b
⊢ filterMap f (mkArray n a) = mkArray n ((some b).get x✝)

Tactic:
simp [filterMap_mkArray, h, w]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem eq_one_iff_not_exists_prime_dvd {n : ℕ} : n = 1 ↔ ∀ p : ℕ, p.Prime → ¬p ∣ n

Proof state:
n : ℕ
⊢ n = 1 ↔ ∀ (p : ℕ), Prime p → ¬p ∣ n

Tactic:
simpa using not_iff_not.mpr ne_one_iff_exists_prime_dvd

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem geom_sum_eq_zero [IsDomain R] {ζ : R} (hζ : IsPrimitiveRoot ζ k) (hk : 1 < k) :
    ∑ i ∈ range k, ζ ^ i = 0

Proof state:
R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
hζ : IsPrimitiveRoot ζ k
hk : 1 < k
⊢ ∑ i ∈ range k, ζ ^ i = 0

Tactic:
refine eq_zero_of_ne_zero_of_mul_left_eq_zero (sub_ne_zero_of_ne (hζ.ne_one hk).symm) ?_

Result:
R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
hζ : IsPrimitiveRoot ζ k
hk : 1 < k
⊢ (1 - ζ) * ∑ i ∈ range k, ζ ^ i = 0

Proof state:
R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
hζ : IsPrimitiveRoot ζ k
hk : 1 < k
⊢ (1 - ζ) * ∑ i ∈ range k, ζ ^ i = 0

Tactic:
rw [mul_neg_geom_sum, hζ.pow_eq_one, sub_self]

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem isRefl (H : B.IsAlt) : B.IsRefl

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
⊢ B.IsRefl

Tactic:
intro x y h

Result:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x y : M₁
h : (B x) y = 0
⊢ (B y) x = 0

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x y : M₁
h : (B x) y = 0
⊢ (B y) x = 0

Tactic:
rw [← neg H, h, neg_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_re (x : ℂ) : x.log.re = Real.log ‖x‖

Proof state:
x : ℂ
⊢ (log x).re = Real.log ‖x‖

Tactic:
simp [log]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem finset_card_neighborSet_eq_degree {G' : Subgraph G} {v : V} [Fintype (G'.neighborSet v)] :
    (G'.neighborSet v).toFinset.card = G'.degree v

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
⊢ (G'.neighborSet v).toFinset.card = G'.degree v

Tactic:
rw [degree, Set.toFinset_card]

Result:
no goals
-- Mathlib/FieldTheory/Normal/Defs.lean
theorem Normal.tower_top_of_normal [h : Normal F E] : Normal K E :=
  normal_iff.2 fun x => by
    obtain ⟨hx, hhx⟩ := h.out x
    rw [algebraMap_eq F K E] at hhx
    exact
      ⟨hx.tower_top,
        Polynomial.splits_of_splits_of_dvd (algebraMap K E)
          (Polynomial.map_ne_zero (minpoly.ne_zero hx))
          ((Polynomial.splits_map_iff (algebraMap F K) (algebraMap K E)).mpr hhx)
          (minpoly.dvd_map_of_isScalarTower F K x)⟩

Proof state:
case intro
F : Type u_1
K : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : Normal F E
x : E
hx : IsIntegral F x
hhx : Splits ((algebraMap K E).comp (algebraMap F K)) (minpoly F x)
⊢ IsIntegral K x ∧ Splits (algebraMap K E) (minpoly K x)

Tactic:
exact
  ⟨hx.tower_top,
    Polynomial.splits_of_splits_of_dvd (algebraMap K E)
      (Polynomial.map_ne_zero (minpoly.ne_zero hx))
      ((Polynomial.splits_map_iff (algebraMap F K) (algebraMap K E)).mpr hhx)
      (minpoly.dvd_map_of_isScalarTower F K x)⟩

Result:
no goals

Proof state:
case intro
F : Type u_1
K : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : Normal F E
x : E
hx : IsIntegral F x
hhx : Splits (algebraMap F E) (minpoly F x)
⊢ IsIntegral K x ∧ Splits (algebraMap K E) (minpoly K x)

Tactic:
rw [algebraMap_eq F K E] at hhx

Result:
case intro
F : Type u_1
K : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : Normal F E
x : E
hx : IsIntegral F x
hhx : Splits ((algebraMap K E).comp (algebraMap F K)) (minpoly F x)
⊢ IsIntegral K x ∧ Splits (algebraMap K E) (minpoly K x)

Proof state:
F : Type u_1
K : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : Normal F E
x : E
⊢ IsIntegral K x ∧ Splits (algebraMap K E) (minpoly K x)

Tactic:
obtain ⟨hx, hhx⟩ := h.out x

Result:
case intro
F : Type u_1
K : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : Normal F E
x : E
hx : IsIntegral F x
hhx : Splits (algebraMap F E) (minpoly F x)
⊢ IsIntegral K x ∧ Splits (algebraMap K E) (minpoly K x)
-- Mathlib/Data/Fin/Basic.lean
theorem pred_lt_iff {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : pred i hi < j ↔ i < succ j

Proof state:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ i.pred hi < j ↔ i < j.succ

Tactic:
rw [← succ_lt_succ_iff, succ_pred]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_modify (h : m.1.WF) {k k' : α} [hi : Inhabited β] {f : β → β} :
    Const.get! (Const.modify m k f) k' =
      if k == k' then
        Const.get? m k |>.map f |>.get!
      else
        Const.get! m k'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k k' : α
hi : Inhabited β
f : β → β
⊢ get! (modify m k f) k' = if (k == k') = true then (Option.map f (get? m k)).get! else get! m k'

Tactic:
simp_to_model [Const.modify] using List.Const.getValue!_modifyKey

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem edist_one_eq_enorm (x : E) : edist x 1 = ‖x‖ₑ

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ edist x 1 = ‖x‖ₑ

Tactic:
rw [edist_eq_enorm_div, div_one]

Result:
no goals
-- Mathlib/Algebra/Homology/Double.lean
lemma double_d_eq_zero₁ (a b : ι) (hb : b ≠ i₁) :
    (double f hi₀₁).d a b = 0 :=
  dif_neg (by tauto)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
a b : ι
hb : b ≠ i₁
⊢ ¬(a = i₀ ∧ b = i₁ ∧ i₀ ≠ i₁)

Tactic:
tauto

Result:
no goals
-- Mathlib/RingTheory/Filtration.lean
theorem submodule_span_single :
    Submodule.span (reesAlgebra I) (⋃ i, single R i '' (F.N i : Set M)) = F.submodule

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⇑(single R i) '' ↑(F.N i)) = F.submodule

Tactic:
rw [← Submodule.span_closure, submodule_closure_single, Submodule.coe_toAddSubmonoid]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ Submodule.span ↥(reesAlgebra I) ↑F.submodule = F.submodule

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ Submodule.span ↥(reesAlgebra I) ↑F.submodule = F.submodule

Tactic:
exact Submodule.span_eq (Filtration.submodule F)

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem mem_oneCocycles_iff (f : G → A) :
    f ∈ oneCocycles A ↔ ∀ g h : G, f (g * h) = A.ρ g (f h) + f g

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G → ↑A.V
⊢ f ∈ oneCocycles A ↔ ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g

Tactic:
simp_rw [mem_oneCocycles_def, sub_add_eq_add_sub, sub_eq_zero, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_append_of_ne_nil {l : List α} {h₁} (h₂ : l' ≠ []) :
    (l ++ l').getLast h₁ = l'.getLast h₂

Proof state:
α : Type u_1
l' l : List α
h₁ : l ++ l' ≠ []
h₂ : l' ≠ []
⊢ (l ++ l').getLast h₁ = l'.getLast h₂

Tactic:
simp only [getLast_eq_head_reverse, reverse_append]

Result:
α : Type u_1
l' l : List α
h₁ : l ++ l' ≠ []
h₂ : l' ≠ []
⊢ (l'.reverse ++ l.reverse).head ⋯ = l'.reverse.head ⋯

Proof state:
α : Type u_1
l' l : List α
h₁ : l ++ l' ≠ []
h₂ : l' ≠ []
⊢ (l'.reverse ++ l.reverse).head ⋯ = l'.reverse.head ⋯

Tactic:
rw [head_append_of_ne_nil]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.mem_nhdsSet_inf_of_forall {K : Set X} {l : Filter X} {s : Set X}
    (hK : IsCompact K) (hs : ∀ x ∈ K, s ∈ 𝓝 x ⊓ l) : s ∈ (𝓝ˢ K) ⊓ l :=
  (hK.nhdsSet_inf_eq_biSup l).symm ▸ by simpa using hs

Proof state:
X : Type u
inst✝ : TopologicalSpace X
K : Set X
l : Filter X
s : Set X
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ⊓ l
⊢ s ∈ ⨆ x ∈ K, 𝓝 x ⊓ l

Tactic:
simpa using hs

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem circulantGraph_adj_translate {s : Set G} {u v d : G} :
    (circulantGraph s).Adj (u + d) (v + d) ↔ (circulantGraph s).Adj u v

Proof state:
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v d : G
⊢ (circulantGraph s).Adj (u + d) (v + d) ↔ (circulantGraph s).Adj u v

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Archimedean.lean
theorem dense_of_no_min (S : AddSubgroup G) (hbot : S ≠ ⊥)
    (H : ¬∃ a : G, IsLeast { g : G | g ∈ S ∧ 0 < g } a) : Dense (S : Set G)

Proof state:
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
H : ¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
⊢ Dense ↑S

Tactic:
refine S.dense_of_not_isolated_zero fun ε ε0 => ?_

Result:
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
H : ¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
ε : G
ε0 : ε > 0
⊢ ∃ g ∈ S, g ∈ Ioo 0 ε

Proof state:
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
ε : G
ε0 : ε > 0
H : ∀ g ∈ S, g ∉ Ioo 0 ε
⊢ ∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a

Tactic:
exact exists_isLeast_pos hbot ε0 (disjoint_left.2 H)

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
H : ¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
ε : G
ε0 : ε > 0
⊢ ∃ g ∈ S, g ∈ Ioo 0 ε

Tactic:
contrapose! H

Result:
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
ε : G
ε0 : ε > 0
H : ∀ g ∈ S, g ∉ Ioo 0 ε
⊢ ∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
-- Mathlib/Algebra/Star/StarRingHom.lean
theorem mk_coe (f : A →⋆ₙ+* B) (h₁ h₂ h₃ h₄) :
    (⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →⋆ₙ+* B) = f

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Star A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : Star B
f : A →⋆ₙ+* B
h₁ : ∀ (x y : A), f (x * y) = f x * f y
h₂ : { toFun := ⇑f, map_mul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_mul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_mul' := h₁ }.toFun x + { toFun := ⇑f, map_mul' := h₁ }.toFun y
h₄ :
  ∀ (a : A),
    { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (star a) =
      star ({ toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun a)
⊢ { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ } = f

Tactic:
ext

Result:
case h
A : Type u_1
B : Type u_2
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Star A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : Star B
f : A →⋆ₙ+* B
h₁ : ∀ (x y : A), f (x * y) = f x * f y
h₂ : { toFun := ⇑f, map_mul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_mul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_mul' := h₁ }.toFun x + { toFun := ⇑f, map_mul' := h₁ }.toFun y
h₄ :
  ∀ (a : A),
    { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (star a) =
      star ({ toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun a)
x✝ : A
⊢ { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ } x✝ = f x✝

Proof state:
case h
A : Type u_1
B : Type u_2
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Star A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : Star B
f : A →⋆ₙ+* B
h₁ : ∀ (x y : A), f (x * y) = f x * f y
h₂ : { toFun := ⇑f, map_mul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_mul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_mul' := h₁ }.toFun x + { toFun := ⇑f, map_mul' := h₁ }.toFun y
h₄ :
  ∀ (a : A),
    { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (star a) =
      star ({ toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun a)
x✝ : A
⊢ { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ } x✝ = f x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
lemma Finset.centerMass_smul_left {c : R'} [Module R' R] [Module R' E] [SMulCommClass R' R R]
    [IsScalarTower R' R R] [SMulCommClass R R' E] [IsScalarTower R' R E] (hc : c ≠ 0) :
    t.centerMass (c • w) z = t.centerMass w z

Proof state:
R : Type u_1
R' : Type u_2
E : Type u_3
ι : Type u_5
inst✝⁹ : LinearOrderedField R
inst✝⁸ : LinearOrderedField R'
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module R E
t : Finset ι
w : ι → R
z : ι → E
c : R'
inst✝⁵ : Module R' R
inst✝⁴ : Module R' E
inst✝³ : SMulCommClass R' R R
inst✝² : IsScalarTower R' R R
inst✝¹ : SMulCommClass R R' E
inst✝ : IsScalarTower R' R E
hc : c ≠ 0
⊢ t.centerMass (c • w) z = t.centerMass w z

Tactic:
simp [centerMass, -smul_assoc, smul_assoc c, ← smul_sum, smul_inv₀, smul_smul_smul_comm, hc]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologySequence.lean
@[reassoc (attr := simp)]
lemma opcyclesToCycles_naturality :
    opcyclesMap φ i ≫ opcyclesToCycles L i j = opcyclesToCycles K i j ≫ cyclesMap φ j

Proof state:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
i j : ι
inst✝³ : K.HasHomology i
inst✝² : K.HasHomology j
inst✝¹ : L.HasHomology i
inst✝ : L.HasHomology j
⊢ opcyclesMap φ i ≫ L.opcyclesToCycles i j = K.opcyclesToCycles i j ≫ cyclesMap φ j

Tactic:
simp only [← cancel_mono (L.iCycles j), ← cancel_epi (K.pOpcycles i),
  assoc, p_opcyclesMap_assoc, pOpcycles_opcyclesToCycles_iCycles, Hom.comm, cyclesMap_i,
  pOpcycles_opcyclesToCycles_iCycles_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zip_of_prod {l : Array α} {l' : Array β} {lp : Array (α × β)} (hl : lp.map Prod.fst = l)
    (hr : lp.map Prod.snd = l') : lp = l.zip l'

Proof state:
α : Type u_1
β : Type u_2
l : Array α
l' : Array β
lp : Array (α × β)
hl : map Prod.fst lp = l
hr : map Prod.snd lp = l'
⊢ lp = l.zip l'

Tactic:
rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]

Result:
no goals