harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/Augment.lean
theorem cochainComplex_d_succ_succ_zero (C : CochainComplex V ℕ) (i : ℕ) : C.d 0 (i + 2) = 0

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ C.d 0 (i + 2) = 0

Tactic:
rw [C.shape]

Result:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ¬(ComplexShape.up ℕ).Rel 0 (i + 2)

Proof state:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ¬1 = i + 2

Tactic:
exact (Nat.one_lt_succ_succ _).ne

Result:
no goals

Proof state:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ¬(ComplexShape.up ℕ).Rel 0 (i + 2)

Tactic:
simp only [ComplexShape.up_Rel, zero_add]

Result:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ¬1 = i + 2
-- Mathlib/Order/Filter/EventuallyConst.lean
theorem mulIndicator_const_iff :
    EventuallyConst (s.mulIndicator fun _ ↦ c) l ↔ c = 1 ∨ EventuallyConst s l

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
inst✝ : One β
s : Set α
c : β
⊢ EventuallyConst (s.mulIndicator fun x => c) l ↔ c = 1 ∨ EventuallyConst s l

Tactic:
rcases eq_or_ne c 1 with rfl | hc <;> simp [mulIndicator_const_iff_of_ne, *]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem disjoint_cylinder_iff [Nonempty (∀ i, α i)] {s t : Finset ι} {S : Set (∀ i : s, α i)}
    {T : Set (∀ i : t, α i)} [DecidableEq ι] :
    Disjoint (cylinder s S) (cylinder t T) ↔
      Disjoint
        (Finset.restrict₂ Finset.subset_union_left ⁻¹' S)
        (Finset.restrict₂ Finset.subset_union_right ⁻¹' T)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Nonempty ((i : ι) → α i)
s t : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
T : Set ((i : { x // x ∈ t }) → α ↑i)
inst✝ : DecidableEq ι
⊢ Disjoint (cylinder s S) (cylinder t T) ↔ Disjoint (Finset.restrict₂ ⋯ ⁻¹' S) (Finset.restrict₂ ⋯ ⁻¹' T)

Tactic:
simp_rw [Set.disjoint_iff, subset_empty_iff, inter_cylinder, cylinder_eq_empty_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_ediv_mul_of_pos_left
    (a : Int) {b : Int} (c : Int) (H : 0 < b) : (a * b) / (c * b) = a / c

Proof state:
a b c : Int
H : 0 < b
⊢ a * b / (c * b) = a / c

Tactic:
rw [Int.mul_comm, Int.mul_comm c, mul_ediv_mul_of_pos _ _ H]

Result:
no goals
-- Mathlib/Dynamics/Newton.lean
theorem isFixedPt_newtonMap_of_aeval_eq_zero (h : aeval x P = 0) :
    IsFixedPt P.newtonMap x

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : (aeval x) P = 0
⊢ IsFixedPt P.newtonMap x

Tactic:
rw [IsFixedPt, newtonMap_apply, h, mul_zero, sub_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RelabelNat.lean
theorem relabelNat_size_eq_size {aig : AIG α} : aig.relabelNat.decls.size = aig.decls.size

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
⊢ aig.relabelNat.decls.size = aig.decls.size

Tactic:
simp [relabelNat, relabelNat']

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma baseChange_ψ₂ : (W.baseChange B).ψ₂ = (W.baseChange A).ψ₂.map (mapRingHom f)

Proof state:
R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W.baseChange B).ψ₂ = Polynomial.map (mapRingHom ↑f) (W.baseChange A).ψ₂

Tactic:
rw [← map_ψ₂, map_baseChange]

Result:
no goals
-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem nnnorm_changeOriginSeries_le_tsum (k l : ℕ) :
    ‖p.changeOriginSeries k l‖₊ ≤
      ∑' _ : { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + l)‖₊ :=
  (nnnorm_sum_le _ (fun t => changeOriginSeriesTerm p k l (Subtype.val t) t.prop)).trans_eq <| by
    simp_rw [tsum_fintype, nnnorm_changeOriginSeriesTerm (p := p) (k := k) (l := l)]

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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
⊢ ∑ a : { s // s.card = l }, ‖p.changeOriginSeriesTerm k l ↑a ⋯‖₊ = ∑' (x : { s // s.card = l }), ‖p (k + l)‖₊

Tactic:
simp_rw [tsum_fintype, nnnorm_changeOriginSeriesTerm (p := p) (k := k) (l := l)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_of_add_le_add_right {a b c : Int} (h : a + b ≤ c + b) : a ≤ c :=
  Int.le_of_add_le_add_left (a := b) <| by rwa [Int.add_comm b a, Int.add_comm b c]

Proof state:
a b c : Int
h : a + b ≤ c + b
⊢ b + a ≤ b + c

Tactic:
rwa [Int.add_comm b a, Int.add_comm b c]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HolderNorm.lean
lemma eHolderNorm_nsmul [Module ℝ Y] [BoundedSMul ℝ Y] (n : ℕ) :
    eHolderNorm r (n • f) = n • eHolderNorm r f

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : MetricSpace X
inst✝² : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
inst✝¹ : Module ℝ Y
inst✝ : BoundedSMul ℝ Y
n : ℕ
⊢ eHolderNorm r (n • f) = n • eHolderNorm r f

Tactic:
simp [← Nat.cast_smul_eq_nsmul (R := ℝ), eHolderNorm_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem map_add_self (x : M) : Q (x + x) = 4 • Q x

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ Q (x + x) = 4 • Q x

Tactic:
rw [← two_smul R x, map_smul, ← Nat.cast_smul_eq_nsmul R]

Result:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ (2 * 2) • Q x = ↑4 • Q x

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ (2 * 2) • Q x = ↑4 • Q x

Tactic:
norm_num

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
theorem pentagon_inv_inv_hom (W X Y Z : C) :
    (α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ 𝟙 Z) ≫ (α_ (W ⊗ X) Y Z).hom =
      (𝟙 W ⊗ (α_ X Y Z).hom) ≫ (α_ W X (Y ⊗ Z)).inv

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ 𝟙 Z) ≫ (α_ (W ⊗ X) Y Z).hom = (𝟙 W ⊗ (α_ X Y Z).hom) ≫ (α_ W X (Y ⊗ Z)).inv

Tactic:
monoidal_coherence

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem normSq_ratCast (q : ℚ) : normSq (q : ℍ[R]) = (q : ℍ[R]) ^ 2

Proof state:
R : Type u_1
inst✝ : LinearOrderedField R
q : ℚ
⊢ ↑(normSq ↑q) = ↑q ^ 2

Tactic:
rw [← coe_ratCast, normSq_coe, coe_pow]

Result:
no goals
-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem changeOriginSeries_summable_aux₂ (hr : (r : ℝ≥0∞) < p.radius) (k : ℕ) :
    Summable fun s : Σl : ℕ, { s : Finset (Fin (k + l)) // s.card = l } =>
      ‖p (k + s.1)‖₊ * r ^ s.1

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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : ↑r < p.radius
k : ℕ
⊢ Summable fun s => ‖p (k + s.fst)‖₊ * r ^ s.fst

Tactic:
rcases ENNReal.lt_iff_exists_add_pos_lt.1 hr with ⟨r', h0, hr'⟩

Result:
case intro.intro
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : ↑r < p.radius
k : ℕ
r' : ℝ≥0
h0 : 0 < r'
hr' : ↑r + ↑r' < p.radius
⊢ Summable fun s => ‖p (k + s.fst)‖₊ * r ^ s.fst

Proof state:
case intro.intro
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : ↑r < p.radius
k : ℕ
r' : ℝ≥0
h0 : 0 < r'
hr' : ↑r + ↑r' < p.radius
⊢ Summable fun s => ‖p (k + s.fst)‖₊ * r ^ s.fst

Tactic:
simpa only [mul_inv_cancel_right₀ (pow_pos h0 _).ne'] using
  ((NNReal.summable_sigma.1 (p.changeOriginSeries_summable_aux₁ hr')).1 k).mul_right (r' ^ k)⁻¹

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma truncatedInf_union_right (hs : a ∉ upperClosure s) (ht : a ∈ upperClosure t) :
    truncatedInf (s ∪ t) a = truncatedInf t a

Proof state:
α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∉ upperClosure ↑s
ht : a ∈ upperClosure ↑t
⊢ (s ∪ t).truncatedInf a = t.truncatedInf a

Tactic:
rw [union_comm, truncatedInf_union_left ht hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem pbind_eq_none_iff {o : Option α} {f : (a : α) → a ∈ o → Option β} :
    o.pbind f = none ↔ o = none ∨ ∃ a h, f a h = none

Proof state:
case some.mpr
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ (∃ a_1 h, f a_1 ⋯ = none) → f a ⋯ = none

Tactic:
rintro ⟨a, rfl, h⟩

Result:
case some.mpr.intro.intro
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
h : f a ⋯ = none
⊢ f a ⋯ = none

Proof state:
case some
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ f a ⋯ = none ↔ ∃ a_1 h, f a_1 ⋯ = none

Tactic:
constructor

Result:
case some.mp
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ f a ⋯ = none → ∃ a_2 h, f a_2 ⋯ = none

case some.mpr
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ (∃ a_1 h, f a_1 ⋯ = none) → f a ⋯ = none

Proof state:
case some.mpr.intro.intro
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
h : f a ⋯ = none
⊢ f a ⋯ = none

Tactic:
exact h

Result:
no goals

Proof state:
case some.mp
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ f a ⋯ = none → ∃ a_2 h, f a_2 ⋯ = none

Tactic:
intro h

Result:
case some.mp
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
h : f a ⋯ = none
⊢ ∃ a_1 h, f a_1 ⋯ = none

Proof state:
case some
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ (some a).pbind f = none ↔ some a = none ∨ ∃ a_1 h, f a_1 h = none

Tactic:
simp only [pbind_some, reduceCtorEq, mem_def, some.injEq, false_or]

Result:
case some
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ f a ⋯ = none ↔ ∃ a_1 h, f a_1 ⋯ = none

Proof state:
case some.mp
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
h : f a ⋯ = none
⊢ ∃ a_1 h, f a_1 ⋯ = none

Tactic:
exact ⟨a, rfl, h⟩

Result:
no goals

Proof state:
case none
α : Type u_1
β : Type u_2
f : (a : α) → a ∈ none → Option β
⊢ none.pbind f = none ↔ none = none ∨ ∃ a h, f a h = none

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.const_inv_smul [AddMonoid α] [Group γ] [DistribMulAction γ α] (h : Periodic f c)
    (a : γ) : Periodic (fun x => f (a⁻¹ • x)) (a • c)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddMonoid α
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Periodic f c
a : γ
⊢ Periodic (fun x => f (a⁻¹ • x)) (a • c)

Tactic:
simpa only [inv_inv] using h.const_smul a⁻¹

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp] lemma cast_le_ofNat : (p : K) ≤ ofNat(n) ↔ p ≤ OfNat.ofNat n

Proof state:
K : Type u_5
inst✝¹ : LinearOrderedSemifield K
p : ℚ≥0
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑p ≤ OfNat.ofNat n ↔ p ≤ OfNat.ofNat n

Tactic:
simp [← cast_le (K := K)]

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem existsUnique_mul_zpow_mem_Ico {a : α} (ha : 1 < a) (b c : α) :
    ∃! m : ℤ, b * a ^ m ∈ Set.Ico c (c * a) :=
  (Equiv.neg ℤ).bijective.existsUnique_iff.2 <| by
    simpa only [Equiv.neg_apply, mem_Ico, zpow_neg, ← div_eq_mul_inv, le_div_iff_mul_le, one_mul,
      mul_comm c, div_lt_iff_lt_mul, mul_assoc] using existsUnique_zpow_near_of_one_lt' ha (b / c)

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedCommGroup α
inst✝ : MulArchimedean α
a : α
ha : 1 < a
b c : α
⊢ ∃! x, b * a ^ (Equiv.neg ℤ) x ∈ Ico c (c * a)

Tactic:
simpa only [Equiv.neg_apply, mem_Ico, zpow_neg, ← div_eq_mul_inv, le_div_iff_mul_le, one_mul,
  mul_comm c, div_lt_iff_lt_mul, mul_assoc] using existsUnique_zpow_near_of_one_lt' ha (b / c)

Result:
no goals
-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem trinomial_monic (hkm : k < m) (hmn : m < n) : (trinomial k m n u v 1).Monic

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v : R
hkm : k < m
hmn : m < n
a✝ : Nontrivial R
⊢ (trinomial k m n u v 1).Monic

Tactic:
exact trinomial_leadingCoeff hkm hmn one_ne_zero

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v : R
hkm : k < m
hmn : m < n
⊢ (trinomial k m n u v 1).Monic

Tactic:
nontriviality R

Result:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v : R
hkm : k < m
hmn : m < n
a✝ : Nontrivial R
⊢ (trinomial k m n u v 1).Monic
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma id_apply (R : CommRingCat) (r : R) :
    (𝟙 R : R ⟶ R) r = r

Proof state:
R : CommRingCat
r : ↑R
⊢ (ConcreteCategory.hom (𝟙 R)) r = r

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem ghostFun_pow (m : ℕ) : ghostFun (x ^ m) = ghostFun x ^ m

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
m : ℕ
⊢ WittVector.ghostFun (x ^ m) = WittVector.ghostFun x ^ m

Tactic:
ghost_fun_tac X 0 ^ m, ![x.coeff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem one_cpow (x : ℂ) : (1 : ℂ) ^ x = 1

Proof state:
x : ℂ
⊢ 1 ^ x = 1

Tactic:
rw [cpow_def]

Result:
x : ℂ
⊢ (if 1 = 0 then if x = 0 then 1 else 0 else cexp (log 1 * x)) = 1

Proof state:
x : ℂ
⊢ (if 1 = 0 then if x = 0 then 1 else 0 else cexp (log 1 * x)) = 1

Tactic:
split_ifs <;> simp_all [one_ne_zero]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem mem_support_pure_iff : a' ∈ (pure a).support ↔ a' = a

Proof state:
α : Type u_1
a a' : α
⊢ a' ∈ (pure a).support ↔ a' = a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem Associated.of_mul_left [CancelCommMonoidWithZero M] {a b c d : M} (h : a * b ~ᵤ c * d)
    (h₁ : a ~ᵤ c) (ha : a ≠ 0) : b ~ᵤ d :=
  let ⟨u, hu⟩ := h
  let ⟨v, hv⟩ := Associated.symm h₁
  ⟨u * (v : Mˣ),
    mul_left_cancel₀ ha
      (by
        rw [← hv, mul_assoc c (v : M) d, mul_left_comm c, ← hu]
        simp [hv.symm, mul_assoc, mul_comm, mul_left_comm])⟩

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
a b c d : M
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : Mˣ
hu : a * b * ↑u = c * d
v : Mˣ
hv : c * ↑v = a
⊢ a * (b * ↑(u * v)) = a * d

Tactic:
rw [← hv, mul_assoc c (v : M) d, mul_left_comm c, ← hu]

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
a b c d : M
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : Mˣ
hu : a * b * ↑u = c * d
v : Mˣ
hv : c * ↑v = a
⊢ c * ↑v * (b * ↑(u * v)) = ↑v * (a * b * ↑u)

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
a b c d : M
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : Mˣ
hu : a * b * ↑u = c * d
v : Mˣ
hv : c * ↑v = a
⊢ c * ↑v * (b * ↑(u * v)) = ↑v * (a * b * ↑u)

Tactic:
simp [hv.symm, mul_assoc, mul_comm, mul_left_comm]

Result:
no goals
-- Mathlib/Algebra/CharP/Two.lean
theorem add_eq_iff_eq_add {a b c : R} : a + b = c ↔ a = c + b

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
a b c : R
⊢ a + b = c ↔ a = c + b

Tactic:
rw [← sub_eq_iff_eq_add, sub_eq_add]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem quasiMeasurePreserving_smul {r : ℝ} (hr : r ≠ 0) :
    QuasiMeasurePreserving (r • ·) μ μ

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
⊢ ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ ≪ μ

Tactic:
exact smul_absolutelyContinuous

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
⊢ QuasiMeasurePreserving (fun x => r • x) μ μ

Tactic:
refine ⟨measurable_const_smul r, ?_⟩

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
⊢ map (fun x => r • x) μ ≪ μ

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
⊢ map (fun x => r • x) μ ≪ μ

Tactic:
rw [map_addHaar_smul μ hr]

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
⊢ ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ ≪ μ
-- Mathlib/Data/Int/Init.lean
lemma emod_two_eq_zero_or_one (n : ℤ) : n % 2 = 0 ∨ n % 2 = 1

Proof state:
n : ℤ
⊢ n % 2 = 0 ∨ n % 2 = 1

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mk_zip_mk (a : Array α) (b : Array β) (ha : a.size = n) (hb : b.size = n) :
    zip (Vector.mk a ha) (Vector.mk b hb) = Vector.mk (Array.zip a b) (by simp [ha, hb]) := rfl

Proof state:
α : Type ?u.18261
β : Type ?u.18264
n : Nat
a : Array α
b : Array β
ha : a.size = n
hb : b.size = n
⊢ (a.zip b).size = n

Tactic:
simp [ha, hb]

Result:
no goals
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.map_zero_mem_openCell [RelCWComplex C D] (n : ℕ) (i : cell C n) :
    map n i 0 ∈ openCell n i

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ ↑(map n i) 0 ∈ openCell n i

Tactic:
apply mem_image_of_mem

Result:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ 0 ∈ ball 0 1

Proof state:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ 0 ∈ ball 0 1

Tactic:
simp only [mem_ball, dist_self, zero_lt_one]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_empty : hausdorffDist s ∅ = 0

Proof state:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
h : s = ∅
⊢ hausdorffDist s ∅ = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ hausdorffDist s ∅ = 0

Tactic:
rcases s.eq_empty_or_nonempty with h | h

Result:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
h : s = ∅
⊢ hausdorffDist s ∅ = 0

case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
h : s.Nonempty
⊢ hausdorffDist s ∅ = 0

Proof state:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
h : s.Nonempty
⊢ hausdorffDist s ∅ = 0

Tactic:
simp [hausdorffDist, hausdorffEdist_empty h]

Result:
no goals
-- Mathlib/RingTheory/Bialgebra/TensorProduct.lean
theorem rid_toAlgEquiv :
    (Bialgebra.TensorProduct.rid R A : A ⊗[R] R ≃ₐ[R] A) = Algebra.TensorProduct.rid R R A

Proof state:
R A : Type u
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Bialgebra R A
⊢ ↑(TensorProduct.rid R A) = Algebra.TensorProduct.rid R R A

Tactic:
ext x

Result:
case h
R A : Type u
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Bialgebra R A
x : A ⊗[R] R
⊢ ↑(TensorProduct.rid R A) x = (Algebra.TensorProduct.rid R R A) x

Proof state:
case h
R A : Type u
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Bialgebra R A
x : A ⊗[R] R
⊢ ↑(TensorProduct.rid R A) x = (Algebra.TensorProduct.rid R R A) x

Tactic:
exact coalgebra_rid_eq_algebra_rid_apply x

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
lemma semilength_insidePart_add_semilength_outsidePart_add_one :
    p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength

Proof state:
p : DyckWord
h : p ≠ 0
⊢ p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength

Tactic:
rw [← congrArg semilength (nest_insidePart_add_outsidePart h), semilength_add, semilength_nest,
  add_right_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
@[simp] lemma qaryEntropy_one (q : ℕ) : qaryEntropy q 1 = log (q - 1 : ℤ)

Proof state:
q : ℕ
⊢ qaryEntropy q 1 = log ↑(↑q - 1)

Tactic:
simp [qaryEntropy]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_comp_smul_deriv'' {f f' : ℝ → ℝ} {g : ℝ → G} (hf : ContinuousOn f [[a, b]])
    (hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x)
    (hf' : ContinuousOn f' [[a, b]]) (hg : ContinuousOn g (f '' [[a, b]])) :
    (∫ x in a..b, f' x • (g ∘ f) x) = ∫ u in f a..f b, g u

Proof state:
a b : ℝ
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f f' : ℝ → ℝ
g : ℝ → G
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g (f '' [[a, b]])
⊢ ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
refine
  integral_comp_smul_deriv''' hf hff' (hg.mono <| image_subset _ Ioo_subset_Icc_self) ?_
    (hf'.smul (hg.comp hf <| subset_preimage_image f _)).integrableOn_Icc

Result:
a b : ℝ
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f f' : ℝ → ℝ
g : ℝ → G
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g (f '' [[a, b]])
⊢ IntegrableOn g (f '' [[a, b]]) volume

Proof state:
a b : ℝ
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f f' : ℝ → ℝ
g : ℝ → G
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
⊢ IntegrableOn g [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]] volume

Tactic:
exact hg.integrableOn_Icc

Result:
no goals

Proof state:
a b : ℝ
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f f' : ℝ → ℝ
g : ℝ → G
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g (f '' [[a, b]])
⊢ IntegrableOn g (f '' [[a, b]]) volume

Tactic:
rw [hf.image_uIcc] at hg ⊢

Result:
a b : ℝ
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f f' : ℝ → ℝ
g : ℝ → G
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
⊢ IntegrableOn g [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]] volume