harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/ByteArray.lean
theorem size_ofFn (f : Fin n → UInt8) : (ofFn f).size = n

Proof state:
n : Nat
f : Fin n → UInt8
⊢ (ofFn f).size = n

Tactic:
simp [size]

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonAssocRing_injective :
    Function.Injective (@toNonAssocRing R)

Proof state:
R : Type u
⊢ Function.Injective (@toNonAssocRing R)

Tactic:
intro _ _ _

Result:
R : Type u
a₁✝ a₂✝ : Ring R
a✝ : toNonAssocRing = toNonAssocRing
⊢ a₁✝ = a₂✝

Proof state:
R : Type u
a₁✝ a₂✝ : Ring R
a✝ : toNonAssocRing = toNonAssocRing
⊢ a₁✝ = a₂✝

Tactic:
ext <;> congr

Result:
no goals
-- Mathlib/Order/Heyting/Boundary.lean
theorem boundary_le_boundary_sup_sup_boundary_inf_right : ∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)

Tactic:
rw [sup_comm a, inf_comm]

Result:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (b ⊓ a)

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (b ⊓ a)

Tactic:
exact boundary_le_boundary_sup_sup_boundary_inf_left

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
@[simp] lemma valuation_one : valuation (1 : ℤ_[p]) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation 1 = 0

Tactic:
simp [valuation]

Result:
no goals
-- Mathlib/Topology/Sequences.lean
theorem mem_closure_iff_seq_limit [FrechetUrysohnSpace X] {s : Set X} {a : X} :
    a ∈ closure s ↔ ∃ x : ℕ → X, (∀ n : ℕ, x n ∈ s) ∧ Tendsto x atTop (𝓝 a)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FrechetUrysohnSpace X
s : Set X
a : X
⊢ a ∈ seqClosure s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FrechetUrysohnSpace X
s : Set X
a : X
⊢ a ∈ closure s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)

Tactic:
rw [← seqClosure_eq_closure]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FrechetUrysohnSpace X
s : Set X
a : X
⊢ a ∈ seqClosure s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_const {m : MeasurableSpace α} (μ : Measure α) (y : F) :
    (const α y).integral μ = (μ univ).toReal • y

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
y : F
⊢ integral μ (const α y) = (μ Set.univ).toReal • y

Tactic:
calc
  (const α y).integral μ = ∑ z ∈ {y}, (μ (const α y ⁻¹' {z})).toReal • z :=
    integral_eq_sum_of_subset <| (filter_subset _ _).trans (range_const_subset _ _)
  _ = (μ univ).toReal • y := by simp [Set.preimage]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
y : F
⊢ ∑ z ∈ {y}, (μ (⇑(const α y) ⁻¹' {z})).toReal • z = (μ Set.univ).toReal • y

Tactic:
simp [Set.preimage]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
y : F
⊢ integral μ (const α y) = (μ Set.univ).toReal • y

Tactic:
classical
calc
  (const α y).integral μ = ∑ z ∈ {y}, (μ (const α y ⁻¹' {z})).toReal • z :=
    integral_eq_sum_of_subset <| (filter_subset _ _).trans (range_const_subset _ _)
  _ = (μ univ).toReal • y := by simp [Set.preimage]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma WithTop.le_toDual_iff {x : WithBot αᵒᵈ} {y : WithTop α} :
    x ≤ WithTop.toDual y ↔ y ≤ WithBot.ofDual x

Proof state:
α : Type u_1
inst✝ : LE α
x : WithBot αᵒᵈ
y : WithTop α
⊢ x ≤ WithTop.toDual y ↔ y ≤ WithBot.ofDual x

Tactic:
cases x <;> cases y <;> simp [le_toDual]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_eq_of_forall_col_eq_smul_add_pred {n : ℕ} {A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R}
    (c : Fin n → R) (A_zero : ∀ i, A i 0 = B i 0)
    (A_succ : ∀ (i) (j : Fin n), A i j.succ = B i j.succ + c j * A i (Fin.castSucc j)) :
    det A = det B

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc
⊢ A.det = B.det

Tactic:
rw [← det_transpose A, ← det_transpose B]

Result:
R : Type v
inst✝ : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc
⊢ Aᵀ.det = Bᵀ.det

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc
⊢ Aᵀ.det = Bᵀ.det

Tactic:
exact det_eq_of_forall_row_eq_smul_add_pred c A_zero fun i j => A_succ j i

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem repr_self [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) :
    b.repr (b i) = EuclideanSpace.single i (1 : 𝕜)

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ b.repr (b i) = EuclideanSpace.single i 1

Tactic:
rw [← b.repr_symm_single i, LinearIsometryEquiv.apply_symm_apply]

Result:
no goals
-- Mathlib/GroupTheory/PGroup.lean
theorem powEquiv_symm_apply {n : ℕ} (hn : p.Coprime n) (g : G) :
    (hG.powEquiv hn).symm g = g ^ (orderOf g).gcdB n

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : p.Coprime n
g : G
⊢ (hG.powEquiv hn).symm g = g ^ (Nat.card ↥(Subgroup.zpowers g)).gcdB n

Tactic:
rfl

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : p.Coprime n
g : G
⊢ (hG.powEquiv hn).symm g = g ^ (orderOf g).gcdB n

Tactic:
rw [← Nat.card_zpowers]

Result:
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : p.Coprime n
g : G
⊢ (hG.powEquiv hn).symm g = g ^ (Nat.card ↥(Subgroup.zpowers g)).gcdB n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_set {f : α → β} {l : List α} {i : Nat} {a : α} :
    (l.set i a).map f = (l.map f).set i (f a)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
i : Nat
a : α
⊢ map f (l.set i a) = (map f l).set i (f a)

Tactic:
induction l generalizing i with
| nil => simp
| cons b l ih => cases i <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
a : α
i : Nat
⊢ map f ([].set i a) = (map f []).set i (f a)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
a b : α
l : List α
ih : ∀ {i : Nat}, map f (l.set i a) = (map f l).set i (f a)
i : Nat
⊢ map f ((b :: l).set i a) = (map f (b :: l)).set i (f a)

Tactic:
cases i <;> simp_all

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem div_isBoundedUnder_of_isBigO {α : Type*} {l : Filter α} {f g : α → 𝕜} (h : f =O[l] g) :
    IsBoundedUnder (· ≤ ·) l fun x => ‖f x / g x‖

Proof state:
case intro.intro
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
c : ℝ
h₀ : c ≥ 0
hc : IsBigOWith c l f g
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ (fun x1 x2 => x1 ≤ x2) ‖f x / g x‖ c

Tactic:
rw [norm_div]

Result:
case intro.intro
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
c : ℝ
h₀ : c ≥ 0
hc : IsBigOWith c l f g
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ (fun x1 x2 => x1 ≤ x2) (‖f x‖ / ‖g x‖) c

Proof state:
case intro.intro
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
c : ℝ
h₀ : c ≥ 0
hc : IsBigOWith c l f g
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f x / g x‖

Tactic:
refine ⟨c, eventually_map.2 (hc.bound.mono fun x hx => ?_)⟩

Result:
case intro.intro
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
c : ℝ
h₀ : c ≥ 0
hc : IsBigOWith c l f g
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ (fun x1 x2 => x1 ≤ x2) ‖f x / g x‖ c

Proof state:
case intro.intro
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
c : ℝ
h₀ : c ≥ 0
hc : IsBigOWith c l f g
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ (fun x1 x2 => x1 ≤ x2) (‖f x‖ / ‖g x‖) c

Tactic:
exact div_le_of_le_mul₀ (norm_nonneg _) h₀ hx

Result:
no goals

Proof state:
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f x / g x‖

Tactic:
obtain ⟨c, h₀, hc⟩ := h.exists_nonneg

Result:
case intro.intro
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
c : ℝ
h₀ : c ≥ 0
hc : IsBigOWith c l f g
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f x / g x‖
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem mem_box_iff' [NeZero n] {ν : ι → ℤ} {x : ι → ℝ} :
    x ∈ box n ν ↔ ∀ i, ν i < n * x i ∧ n * x i ≤ ν i + 1

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x : ι → ℝ
h : 0 < ↑n
⊢ x ∈ box n ν ↔ ∀ (i : ι), ↑(ν i) < ↑n * x i ∧ ↑n * x i ≤ ↑(ν i) + 1

Tactic:
simp_rw [mem_box_iff, ← _root_.le_div_iff₀' h, ← div_lt_iff₀' h]

Result:
no goals

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x : ι → ℝ
⊢ x ∈ box n ν ↔ ∀ (i : ι), ↑(ν i) < ↑n * x i ∧ ↑n * x i ≤ ↑(ν i) + 1

Tactic:
have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero

Result:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x : ι → ℝ
h : 0 < ↑n
⊢ x ∈ box n ν ↔ ∀ (i : ι), ↑(ν i) < ↑n * x i ∧ ↑n * x i ≤ ↑(ν i) + 1
-- Mathlib/Data/List/Rotate.lean
theorem rotate_replicate (a : α) (n : ℕ) (k : ℕ) : (replicate n a).rotate k = replicate n a :=
  eq_replicate_iff.2 ⟨by rw [length_rotate, length_replicate], fun b hb =>
    eq_of_mem_replicate <| mem_rotate.1 hb⟩

Proof state:
α : Type u
a : α
n k : ℕ
⊢ ((replicate n a).rotate k).length = n

Tactic:
rw [length_rotate, length_replicate]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.mul_left (H1 : IsCoprime x z) (H2 : IsCoprime y z) : IsCoprime (x * y) z :=
  let ⟨a, b, h1⟩ := H1
  let ⟨c, d, h2⟩ := H2
  ⟨a * c, a * x * d + b * c * y + b * d * z,
    calc a * c * (x * y) + (a * x * d + b * c * y + b * d * z) * z
      _ = (a * x + b * z) * (c * y + d * z)

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : IsCoprime y z
a b : R
h1 : a * x + b * z = 1
c d : R
h2 : c * y + d * z = 1
⊢ a * c * (x * y) + (a * x * d + b * c * y + b * d * z) * z = (a * x + b * z) * (c * y + d * z)

Tactic:
ring

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : IsCoprime y z
a b : R
h1 : a * x + b * z = 1
c d : R
h2 : c * y + d * z = 1
⊢ (a * x + b * z) * (c * y + d * z) = 1

Tactic:
rw [h1, h2, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_insertEntry_self [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)}
    {k : α} {v : β k} : getKey! k (insertEntry k v l) = k

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
l : List ((a : α) × β a)
k : α
v : β k
⊢ getKey! k (insertEntry k v l) = k

Tactic:
rw [getKey!_insertEntry, if_pos BEq.refl]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
theorem MonoidHom.cancel_left [MulOneClass M] [MulOneClass N] [MulOneClass P]
    {g : N →* P} {f₁ f₂ : M →* N} (hg : Function.Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => MonoidHom.ext fun x => hg <| by rw [← MonoidHom.comp_apply, h, MonoidHom.comp_apply],
    fun h => h ▸ rfl⟩

Proof state:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
g : N →* P
f₁ f₂ : M →* N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ g (f₁ x) = g (f₂ x)

Tactic:
rw [← MonoidHom.comp_apply, h, MonoidHom.comp_apply]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Hom.lean
theorem id_comp (f : R →ₑ+*[φ] S) : (MulSemiringActionHom.id N).comp f = f :=
  ext fun x => by rw [comp_apply, id_apply]

Proof state:
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
R : Type u_10
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_12
inst✝¹ : Semiring S
inst✝ : MulSemiringAction N S
f : R →ₑ+*[φ] S
x : R
⊢ ((MulSemiringActionHom.id N).comp f) x = f x

Tactic:
rw [comp_apply, id_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mkVector_succ : mkVector (n + 1) a = (mkVector n a).push a

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ mkVector (n + 1) a = (mkVector n a).push a

Tactic:
simp [mkVector, Array.mkArray_succ]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem aemeasurable_inv_iff₀ {G₀ : Type*} [GroupWithZero G₀] [MeasurableSpace G₀]
    [MeasurableInv G₀] {f : α → G₀} : AEMeasurable (fun x => (f x)⁻¹) μ ↔ AEMeasurable f μ :=
  ⟨fun h => by simpa only [inv_inv] using h.inv, fun h => h.inv⟩

Proof state:
α : Type u_3
m : MeasurableSpace α
μ : Measure α
G₀ : Type u_4
inst✝² : GroupWithZero G₀
inst✝¹ : MeasurableSpace G₀
inst✝ : MeasurableInv G₀
f : α → G₀
h : AEMeasurable (fun x => (f x)⁻¹) μ
⊢ AEMeasurable f μ

Tactic:
simpa only [inv_inv] using h.inv

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem supDegree_zero : (0 : R[A]).supDegree D = ⊥

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : SemilatticeSup B
inst✝¹ : OrderBot B
D : A → B
inst✝ : AddZeroClass A
⊢ supDegree D 0 = ⊥

Tactic:
simp [supDegree]

Result:
no goals
-- Mathlib/Data/Multiset/Basic.lean
theorem toList_eq_singleton_iff {a : α} {m : Multiset α} : m.toList = [a] ↔ m = {a}

Proof state:
α : Type u_1
a : α
m : Multiset α
⊢ m.toList = [a] ↔ m = {a}

Tactic:
rw [← perm_singleton, ← coe_eq_coe, coe_toList, coe_singleton]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_single (c : R) (a : α) :
    linearCombination R v (single a c) = c • v a

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
c : R
a : α
⊢ (linearCombination R v) (single a c) = c • v a

Tactic:
simp [linearCombination_apply, sum_single_index]

Result:
no goals
-- Mathlib/Data/Finset/SMulAntidiagonal.lean
theorem IsPWO.smul [PartialOrder G] [PartialOrder P] [SMul G P] [IsOrderedCancelSMul G P]
    {s : Set G} {t : Set P} (hs : s.IsPWO) (ht : t.IsPWO) : IsPWO (s • t)

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
⊢ (s • t).IsPWO

Tactic:
rw [← @image_smul_prod]

Result:
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
⊢ ((fun x => x.1 • x.2) '' s ×ˢ t).IsPWO

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
⊢ ((fun x => x.1 • x.2) '' s ×ˢ t).IsPWO

Tactic:
exact (hs.prod ht).image_of_monotone (monotone_fst.smul monotone_snd)

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[reassoc (attr := simp)]
lemma ι_D₁ (i₁₂ i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂) (h : ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = i₁₂) :
    K.ιTotal c₁₂ i₁ i₂ i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂' =
      K.d₁ c₁₂ i₁ i₂ i₁₂'

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.ιTotal c₁₂ i₁ i₂ i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂' = K.d₁ c₁₂ i₁ i₂ i₁₂'

Tactic:
apply totalAux.ιMapObj_D₁

Result:
no goals
-- Mathlib/Deprecated/Cardinal/Finite.lean
theorem card_sum (α β : Type*) :
    PartENat.card (α ⊕ β) = PartENat.card α + PartENat.card β

Proof state:
α : Type u_1
β : Type u_2
⊢ card (α ⊕ β) = card α + card β

Tactic:
simp only [PartENat.card, Cardinal.mk_sum, map_add, Cardinal.toPartENat_lift]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive of_forall_le_norm]
lemma DiscreteTopology.of_forall_le_norm' (hpos : 0 < r) (hr : ∀ x : E, x ≠ 1 → r ≤ ‖x‖) :
    DiscreteTopology E :=
  .of_forall_le_dist hpos fun x y hne ↦ by
    simp only [dist_eq_norm_div]
    exact hr _ (div_ne_one.2 hne)

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
r : ℝ
hpos : 0 < r
hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖
x y : E
hne : x ≠ y
⊢ r ≤ ‖x / y‖

Tactic:
exact hr _ (div_ne_one.2 hne)

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
r : ℝ
hpos : 0 < r
hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖
x y : E
hne : x ≠ y
⊢ (fun x1 x2 => r ≤ dist x1 x2) x y

Tactic:
simp only [dist_eq_norm_div]

Result:
E : Type u_5
inst✝ : SeminormedGroup E
r : ℝ
hpos : 0 < r
hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖
x y : E
hne : x ≠ y
⊢ r ≤ ‖x / y‖
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem int_mul_iff (hm : m ≠ 0) : LiouvilleWith p (m * x) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
m : ℤ
hm : m ≠ 0
⊢ LiouvilleWith p (↑m * x) ↔ LiouvilleWith p x

Tactic:
rw [mul_comm, mul_int_iff hm]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem foldl_op_eq_op_foldr_assoc :
    ∀ {l : List α} {a₁ a₂}, ((l <*> a₁) ⋆ a₂) = a₁ ⋆ l.foldr (· ⋆ ·) a₂
  | [], _, _ => rfl
  | a :: l, a₁, a₂ => by
    simp only [foldl_cons, foldr_cons, foldl_assoc, ha.assoc]; rw [foldl_op_eq_op_foldr_assoc]

Proof state:
α : Type u
op : α → α → α
ha : Std.Associative op
a : α
l : List α
a₁ a₂ : α
⊢ op ((a :: l) <*> a₁) a₂ = op a₁ (foldr (fun x1 x2 => op x1 x2) a₂ (a :: l))

Tactic:
simp only [foldl_cons, foldr_cons, foldl_assoc, ha.assoc]

Result:
α : Type u
op : α → α → α
ha : Std.Associative op
a : α
l : List α
a₁ a₂ : α
⊢ op a₁ (op (l <*> a) a₂) = op a₁ (op a (foldr (fun x1 x2 => op x1 x2) a₂ l))

Proof state:
α : Type u
op : α → α → α
ha : Std.Associative op
a : α
l : List α
a₁ a₂ : α
⊢ op a₁ (op (l <*> a) a₂) = op a₁ (op a (foldr (fun x1 x2 => op x1 x2) a₂ l))

Tactic:
rw [foldl_op_eq_op_foldr_assoc]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem continuous_inf_rng {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β} :
    Continuous[t₁, t₂ ⊓ t₃] f ↔ Continuous[t₁, t₂] f ∧ Continuous[t₁, t₃] f

Proof state:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
⊢ Continuous f ↔ Continuous f ∧ Continuous f

Tactic:
simp only [continuous_iff_coinduced_le, le_inf_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem mul_inv_le_iff_le_mul : a * b⁻¹ ≤ c ↔ a ≤ c * b :=
  (mul_le_mul_iff_right b).symm.trans <| by rw [inv_mul_cancel_right]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a * b⁻¹ * b ≤ c * b ↔ a ≤ c * b

Tactic:
rw [inv_mul_cancel_right]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem mul_eq_right₀ (hb : b ≠ 0) : a * b = b ↔ a = 1

Proof state:
M₀ : Type u_1
inst✝ : CancelMonoidWithZero M₀
a b : M₀
hb : b ≠ 0
⊢ a * b = b ↔ a = 1

Tactic:
rw [Iff.comm, ← mul_left_inj' hb, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zip_map_left (f : α → γ) (l₁ : Array α) (l₂ : Array β) :
    zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id)

Proof state:
α : Type u_1
γ : Type u_2
β : Type u_3
f : α → γ
l₁ : Array α
l₂ : Array β
⊢ (map f l₁).zip l₂ = map (Prod.map f id) (l₁.zip l₂)

Tactic:
rw [← zip_map, map_id]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_list_le_max (α : Type u) : #(List α) ≤ max ℵ₀ #α

Proof state:
case inl
α : Type u
h✝ : Finite α
⊢ #(List α) ≤ ℵ₀ ⊔ #α

Tactic:
exact mk_le_aleph0.trans (le_max_left _ _)

Result:
no goals

Proof state:
case inr
α : Type u
h✝ : Infinite α
⊢ #α ≤ ℵ₀ ⊔ #α

Tactic:
apply le_max_right

Result:
no goals

Proof state:
case inr
α : Type u
h✝ : Infinite α
⊢ #(List α) ≤ ℵ₀ ⊔ #α

Tactic:
rw [mk_list_eq_mk]

Result:
case inr
α : Type u
h✝ : Infinite α
⊢ #α ≤ ℵ₀ ⊔ #α

Proof state:
α : Type u
⊢ #(List α) ≤ ℵ₀ ⊔ #α

Tactic:
cases finite_or_infinite α

Result:
case inl
α : Type u
h✝ : Finite α
⊢ #(List α) ≤ ℵ₀ ⊔ #α

case inr
α : Type u
h✝ : Infinite α
⊢ #(List α) ≤ ℵ₀ ⊔ #α
-- Mathlib/Analysis/Normed/Group/Continuity.lean
theorem continuous_norm' : Continuous fun a : E => ‖a‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ Continuous fun a => ‖a‖

Tactic:
simpa using continuous_id.dist (continuous_const : Continuous fun _a => (1 : E))

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk_eq_mk_iff' : mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = a₂ * b₁

Proof state:
α : Type u_1
inst✝ : CancelCommMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
⊢ mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁

Tactic:
simp_rw [mk_eq_mk_iff, r_iff_exists, mul_left_cancel_iff, exists_const]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
theorem map_le_lineMap_iff_slope_le_slope_left (h : 0 < r * (b - a)) :
    f c ≤ lineMap (f a) (f b) r ↔ slope f a c ≤ slope f a b

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f ((lineMap a b) r) ≤ (lineMap (f a) (f b)) r ↔ slope f a ((lineMap a b) r) ≤ slope f a b

Tactic:
rw [lineMap_apply, lineMap_apply, slope, slope, vsub_eq_sub, vsub_eq_sub, vsub_eq_sub,
  vadd_eq_add, vadd_eq_add, smul_eq_mul, add_sub_cancel_right, smul_sub, smul_sub, smul_sub,
  sub_le_iff_le_add, mul_inv_rev, mul_smul, mul_smul, ← smul_sub, ← smul_sub, ← smul_add,
  smul_smul, ← mul_inv_rev, inv_smul_le_iff_of_pos h, smul_smul,
  mul_inv_cancel_right₀ (right_ne_zero_of_mul h.ne'), smul_add,
  smul_inv_smul₀ (left_ne_zero_of_mul h.ne')]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem lift'_mk [T0Space β] {f : α → β} (h : UniformContinuous f) (a : α) :
    lift' f (mk a) = f a

Proof state:
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
h : UniformContinuous f
a : α
⊢ lift' f (mk a) = f a

Tactic:
rw [lift', dif_pos h, lift_mk]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem dist_map_zero_lt_of_semiconj {f g₁ g₂ : CircleDeg1Lift} (h : Function.Semiconj f g₁ g₂) :
    dist (g₁ 0) (g₂ 0) < 2 :=
  calc
    dist (g₁ 0) (g₂ 0) ≤ dist (g₁ 0) (f (g₁ 0) - f 0) + dist _ (g₂ 0) := dist_triangle _ _ _
    _ = dist (f 0 + g₁ 0) (f (g₁ 0)) + dist (g₂ 0 + f 0) (g₂ (f 0))

Proof state:
f g₁ g₂ : CircleDeg1Lift
h : Semiconj ⇑f ⇑g₁ ⇑g₂
⊢ dist (g₁ 0) (f (g₁ 0) - f 0) + dist (f (g₁ 0) - f 0) (g₂ 0) =
    dist (f 0 + g₁ 0) (f (g₁ 0)) + dist (g₂ 0 + f 0) (g₂ (f 0))

Tactic:
simp only [h.eq, Real.dist_eq, sub_sub, add_comm (f 0), sub_sub_eq_add_sub,
  abs_sub_comm (g₂ (f 0))]

Result:
no goals