harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem append_zero_width (x : BitVec w) (y : BitVec 0) : x ++ y = x

Proof state:
case pred
w : Nat
x : BitVec w
y : BitVec 0
i✝ : Nat
a✝ : i✝ < w + 0
⊢ (if i✝ < 0 then y.getLsbD i✝ else x.getLsbD (i✝ - 0)) = x.getLsbD i✝

Tactic:
simp

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
y : BitVec 0
i✝ : Nat
a✝ : i✝ < w + 0
⊢ (x ++ y).getLsbD i✝ = x.getLsbD i✝

Tactic:
rw [getLsbD_append]

Result:
case pred
w : Nat
x : BitVec w
y : BitVec 0
i✝ : Nat
a✝ : i✝ < w + 0
⊢ (if i✝ < 0 then y.getLsbD i✝ else x.getLsbD (i✝ - 0)) = x.getLsbD i✝

Proof state:
w : Nat
x : BitVec w
y : BitVec 0
⊢ x ++ y = x

Tactic:
ext

Result:
case pred
w : Nat
x : BitVec w
y : BitVec 0
i✝ : Nat
a✝ : i✝ < w + 0
⊢ (x ++ y).getLsbD i✝ = x.getLsbD i✝
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem measure_mono_ae (H : s ≤ᵐ[μ] t) : μ s ≤ μ t :=
  calc
    μ s ≤ μ (s ∪ t) := measure_mono subset_union_left
    _ = μ (t ∪ s \ t)

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
H : s ≤ᶠ[ae μ] t
⊢ μ t + μ (s \ t) = μ t

Tactic:
rw [ae_le_set.1 H, add_zero]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
H : s ≤ᶠ[ae μ] t
⊢ μ (s ∪ t) = μ (t ∪ s \ t)

Tactic:
rw [union_diff_self, Set.union_comm]

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Ring.lean
theorem inv_def {r : R} {s : R⁰} :
    (r /ₒ s)⁻¹ =
      if hr : r = (0 : R) then (0 : R[R⁰⁻¹])
      else s /ₒ ⟨r, fun _ => eq_zero_of_ne_zero_of_mul_right_eq_zero hr⟩

Proof state:
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
⊢ (r /ₒ s)⁻¹ = if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩

Tactic:
with_unfolding_all rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
⊢ (r /ₒ s)⁻¹ = if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
theorem aeval_sumIDeriv_of_pos [Nontrivial A] [NoZeroDivisors A] (p : R[X]) {q : ℕ} (hq : 0 < q)
    (inj_amap : Function.Injective (algebraMap R A)) :
    ∃ gp : R[X], gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A) {p' : A[X]},
        p.map (algebraMap R A) = (X - C r) ^ (q - 1) * p' →
        aeval r (sumIDeriv p) = (q - 1)! • p'.eval r + q ! • aeval r gp

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k => if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
⊢ q ≤ p.natDegree + 1

Tactic:
rw [← tsub_le_iff_right]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k => if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
⊢ q - 1 ≤ p.natDegree
-- Mathlib/Topology/EMetricSpace/Basic.lean
theorem tendstoUniformly_iff {ι : Type*} {F : ι → β → α} {f : β → α} {p : Filter ι} :
    TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x, edist (f x) (F n x) < ε

Proof state:
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), edist (f x) (F n x) < ε

Tactic:
simp only [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff, mem_univ, forall_const]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem ite_eq_true_distrib (p : Prop) [h : Decidable p] (t f : Bool) :
    (ite p t f = true) = ite p (t = true) (f = true)

Proof state:
case isTrue
p✝ : Prop
t f : Bool
p : p✝
⊢ ((if p✝ then t else f) = true) = if p✝ then t = true else f = true

Tactic:
simp [p]

Result:
no goals

Proof state:
p : Prop
h : Decidable p
t f : Bool
⊢ ((if p then t else f) = true) = if p then t = true else f = true

Tactic:
cases h with | _ p => simp [p]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem Finset.emultiplicity_prod {β : Type*} {p : α} (hp : Prime p) (s : Finset β) (f : β → α) :
    emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
β : Type u_3
p : α
hp : Prime p
s : Finset β
f : β → α
⊢ emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)

Tactic:
induction' s using Finset.induction with a s has ih h

Result:
case empty
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
⊢ emultiplicity p (∏ x ∈ ∅, f x) = ∑ x ∈ ∅, emultiplicity p (f x)

case insert
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
a : β
s : Finset β
has : a ∉ s
ih : emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)
⊢ emultiplicity p (∏ x ∈ insert a s, f x) = ∑ x ∈ insert a s, emultiplicity p (f x)

Proof state:
case empty
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
⊢ emultiplicity p (∏ x ∈ ∅, f x) = ∑ x ∈ ∅, emultiplicity p (f x)

Tactic:
simp only [Finset.sum_empty, Finset.prod_empty]

Result:
case empty
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
⊢ emultiplicity p 1 = 0

Proof state:
case empty
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
⊢ emultiplicity p 1 = 0

Tactic:
exact emultiplicity_of_one_right hp.not_unit

Result:
no goals

Proof state:
case insert
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
a : β
s : Finset β
has : a ∉ s
ih : emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)
⊢ emultiplicity p (∏ x ∈ insert a s, f x) = ∑ x ∈ insert a s, emultiplicity p (f x)

Tactic:
simpa [has, ← ih] using emultiplicity_mul hp

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem odd_of_mod_four_eq_one {n : ℕ} : n % 4 = 1 → n % 2 = 1

Proof state:
n : ℕ
⊢ n % 4 = 1 → n % 2 = 1

Tactic:
simpa [ModEq] using @ModEq.of_mul_left 2 n 1 2

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem one_smul' (b : ArithmeticFunction M) : (1 : ArithmeticFunction R) • b = b

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
y : ℕ × ℕ
ymem : y ∈ x.divisorsAntidiagonal
ynmem : y ∉ {(1, x)}
⊢ y.1 ≠ 1

Tactic:
intro con

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
y : ℕ × ℕ
ymem : y ∈ x.divisorsAntidiagonal
ynmem : y ∉ {(1, x)}
con : y.1 = 1
⊢ False

Proof state:
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
⊢ ∀ x_1 ∈ x.divisorsAntidiagonal, x_1 ∉ {(1, x)} → 1 x_1.1 • b x_1.2 = 0

Tactic:
intro y ymem ynmem

Result:
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
y : ℕ × ℕ
ymem : y ∈ x.divisorsAntidiagonal
ynmem : y ∉ {(1, x)}
⊢ 1 y.1 • b y.2 = 0

Proof state:
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
⊢ ∑ x ∈ x.divisorsAntidiagonal, 1 x.1 • b x.2 = b x

Tactic:
have h : {(1, x)} ⊆ divisorsAntidiagonal x := by simp [x0]

Result:
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
⊢ ∑ x ∈ x.divisorsAntidiagonal, 1 x.1 • b x.2 = b x
-- Mathlib/Algebra/Vertex/HVertexOperator.lean
theorem coeff_smul (A : HVertexOperator Γ R V W) (r : R) : (r • A).coeff = r • (A.coeff)

Proof state:
case h.h
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
r : R
x✝¹ : Γ
x✝ : V
⊢ ((r • A).coeff x✝¹) x✝ = ((r • A.coeff) x✝¹) x✝

Tactic:
simp

Result:
no goals

Proof state:
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
r : R
⊢ (r • A).coeff = r • A.coeff

Tactic:
ext

Result:
case h.h
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
r : R
x✝¹ : Γ
x✝ : V
⊢ ((r • A).coeff x✝¹) x✝ = ((r • A.coeff) x✝¹) x✝
-- Mathlib/Topology/UniformSpace/Ascoli.lean
theorem EquicontinuousOn.isClosed_range_uniformOnFun_iff_pi
    {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (𝔖_covers : ⋃₀ 𝔖 = univ)
    (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) :
    IsClosed (range <| UniformOnFun.ofFun 𝔖 ∘ F) ↔
    IsClosed (range F)

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ⋃₀ 𝔖 = univ
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) ↔ IsClosed (range F)

Tactic:
simp_rw [isClosed_iff_clusterPt, ← Filter.map_top, ← mapClusterPt_def,
  mapClusterPt_iff_ultrafilter, range_comp, (UniformOnFun.ofFun 𝔖).surjective.forall,
  ← EquicontinuousOn.tendsto_uniformOnFun_iff_pi 𝔖_compact 𝔖_covers F_eqcont,
  (UniformOnFun.ofFun 𝔖).injective.mem_set_image]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem bind_mono {f₁ f₂ : Filter α} {g₁ g₂ : α → Filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ᶠ[f₁] g₂) :
    bind f₁ g₁ ≤ bind f₂ g₂

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
⊢ f₁.bind g₁ ≤ f₂.bind g₂

Tactic:
refine le_trans (fun s hs => ?_) (join_mono <| map_mono hf)

Result:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : s ∈ (map g₂ f₁).join
⊢ s ∈ f₁.bind g₁

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : s ∈ (map g₂ f₁).join
⊢ s ∈ f₁.bind g₁

Tactic:
simp only [mem_join, mem_bind', mem_map] at hs ⊢

Result:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : g₂ ⁻¹' {t | s ∈ t} ∈ f₁
⊢ {a | s ∈ g₁ a} ∈ f₁

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : g₂ ⁻¹' {t | s ∈ t} ∈ f₁
⊢ {a | s ∈ g₁ a} ∈ f₁

Tactic:
filter_upwards [hg, hs] with _ hx hs using hx hs

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean
@[reassoc]
lemma w : f ≫ p = c.ι.app ⊥ ≫ g

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : LinearOrder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
⊢ f ≫ p = c.ι.app ⊥ ≫ g

Tactic:
rw [← sq'.w₁, assoc, sq'.w₂, Cocone.w_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_append [BEq α] {l l' : List ((a : α) × β a)} {a : α} :
    containsKey a (l ++ l') = (containsKey a l || containsKey a l')

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
a : α
⊢ containsKey a (l ++ l') = (containsKey a l || containsKey a l')

Tactic:
simp [containsKey_eq_isSome_getEntry?]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem tendstoUniformlyOnFilter_iff {F : ι → β → α} {f : β → α} {p : Filter ι} {p' : Filter β} :
    TendstoUniformlyOnFilter F f p p' ↔
      ∀ ε > 0, ∀ᶠ n : ι × β in p ×ˢ p', dist (f n.snd) (F n.fst n.snd) < ε

Proof state:
α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
p' : Filter β
H : ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u

Tactic:
rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩

Result:
case intro.intro
α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
p' : Filter β
H : ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u

Proof state:
α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
p' : Filter β
⊢ TendstoUniformlyOnFilter F f p p' ↔ ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε

Tactic:
refine ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu => ?_⟩

Result:
α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
p' : Filter β
H : ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u

Proof state:
case intro.intro
α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
p' : Filter β
H : ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u

Tactic:
exact (H ε εpos).mono fun n hn => hε hn

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Basic.lean
lemma Triangle.isIso_of_isIsos {A B : Triangle C} (f : A ⟶ B)
    (h₁ : IsIso f.hom₁) (h₂ : IsIso f.hom₂) (h₃ : IsIso f.hom₃) : IsIso f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ A.mor₂ ≫ (asIso f.hom₃).hom = (asIso f.hom₂).hom ≫ B.mor₂

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ A.mor₁ ≫ (asIso f.hom₂).hom = (asIso f.hom₁).hom ≫ B.mor₁

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ A.mor₃ ≫ (shiftFunctor C 1).map (asIso f.hom₁).hom = (asIso f.hom₃).hom ≫ B.mor₃

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
e : A ≅ B := A.isoMk B (asIso f.hom₁) (asIso f.hom₂) (asIso f.hom₃) ⋯ ⋯ ⋯
⊢ IsIso f

Tactic:
exact (inferInstance : IsIso e.hom)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ IsIso f

Tactic:
let e := Triangle.isoMk A B (asIso f.hom₁) (asIso f.hom₂) (asIso f.hom₃)
  (by simp) (by simp) (by simp)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
e : A ≅ B := A.isoMk B (asIso f.hom₁) (asIso f.hom₂) (asIso f.hom₃) ⋯ ⋯ ⋯
⊢ IsIso f
-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem one_leftUnitor {M : Mon_ C} :
    ((λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ M.one)) ≫ (λ_ M.X).hom = M.one

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ M.one)) ≫ (λ_ M.X).hom = M.one

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem GoodProducts.linearIndependent_iff_union_smaller :
    LinearIndependent ℤ (GoodProducts.eval C) ↔
      LinearIndependent ℤ (fun (p : ⋃ (e : {o' // o' < o}), (smaller C e.val)) ↦ p.1)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
⊢ LinearIndependent (ι := ↑(range C)) ℤ ((fun p => ↑p) ∘ (range_equiv C ho hsC).toFun) ↔
    LinearIndependent ℤ fun (p : ↑(⋃ e, smaller C ↑e)) => ↑p

Tactic:
exact linearIndependent_equiv (range_equiv C ho hsC)

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
⊢ LinearIndependent ℤ (eval C) ↔ LinearIndependent ℤ fun (p : ↑(⋃ e, smaller C ↑e)) => ↑p

Tactic:
rw [GoodProducts.linearIndependent_iff_range, ← range_equiv_factorization C ho hsC]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
⊢ LinearIndependent (ι := ↑(range C)) ℤ ((fun p => ↑p) ∘ (range_equiv C ho hsC).toFun) ↔
    LinearIndependent ℤ fun (p : ↑(⋃ e, smaller C ↑e)) => ↑p
-- Mathlib/Data/Nat/ChineseRemainder.lean
theorem chineseRemainderOfFinset_lt_prod {t : Finset ι}
    (hs : ∀ i ∈ t, s i ≠ 0) (pp : Set.Pairwise t (Coprime on s)) :
    chineseRemainderOfFinset a s t hs pp < ∏ i ∈ t, s i

Proof state:
ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ {x | x ∈ t.val}.Pairwise (Coprime on s)

Tactic:
simpa using pp

Result:
no goals

Proof state:
ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ ∀ i ∈ t.val, s i ≠ 0

Tactic:
simpa using hs

Result:
no goals

Proof state:
ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ ↑(chineseRemainderOfFinset a s t hs pp) < ∏ i ∈ t, s i

Tactic:
simpa [chineseRemainderOfFinset] using
  chineseRemainderOfMultiset_lt_prod a s t.nodup (by simpa using hs) (by simpa using pp)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem utf8Len_append (cs₁ cs₂) : utf8Len (cs₁ ++ cs₂) = utf8Len cs₁ + utf8Len cs₂

Proof state:
cs₁ cs₂ : List Char
⊢ utf8Len (cs₁ ++ cs₂) = utf8Len cs₁ + utf8Len cs₂

Tactic:
induction cs₁ <;> simp [*, Nat.add_right_comm]

Result:
no goals
-- Mathlib/Order/SuccPred/CompleteLinearOrder.lean
theorem sSup_Iio_eq_self_iff_isSuccPrelimit : sSup (Iio x) = x ↔ IsSuccPrelimit x

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
hx : ¬IsSuccPrelimit (sSup (Iio x))
⊢ False

Tactic:
simpa [h] using csSup_mem_of_not_isSuccPrelimit' bddAbove_Iio hx

Result:
no goals

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
hx : ¬IsSuccPrelimit x
⊢ False

Tactic:
rw [← h] at hx

Result:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
hx : ¬IsSuccPrelimit (sSup (Iio x))
⊢ False

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
⊢ sSup (Iio x) = x ↔ IsSuccPrelimit x

Tactic:
refine ⟨fun h ↦ ?_, IsSuccPrelimit.sSup_Iio⟩

Result:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
⊢ IsSuccPrelimit x

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
⊢ IsSuccPrelimit x

Tactic:
by_contra hx

Result:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
hx : ¬IsSuccPrelimit x
⊢ False
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
lemma disjoint_edge {u v : V} : Disjoint G (edge u v) ↔ ¬G.Adj u v

Proof state:
case pos
V : Type u_1
G : SimpleGraph V
u : V
⊢ Disjoint G (edge u u) ↔ ¬G.Adj u u

Tactic:
simp [edge_self_eq_bot]

Result:
no goals

Proof state:
case pos
V : Type u_1
G : SimpleGraph V
u v : V
h : u = v
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v

Tactic:
subst h

Result:
case pos
V : Type u_1
G : SimpleGraph V
u : V
⊢ Disjoint G (edge u u) ↔ ¬G.Adj u u

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬u = v
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v

Tactic:
simp [← disjoint_edgeSet, edge_edgeSet_of_ne h]

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v

Tactic:
by_cases h : u = v

Result:
case pos
V : Type u_1
G : SimpleGraph V
u v : V
h : u = v
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v

case neg
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬u = v
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v
-- Mathlib/RingTheory/Localization/Basic.lean
theorem isLocalization_of_algEquiv [Algebra R P] [IsLocalization M S] (h : S ≃ₐ[R] P) :
    IsLocalization M P

Proof state:
case surj'.intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e :
  (let_fun this := ⇑h;
      this)
      (h.symm y * (algebraMap R S) ↑(x, s).2) =
    (let_fun this := ⇑h;
      this)
      ((algebraMap R S) (x, s).1)
⊢ ∃ x, y * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1

Tactic:
simp only [map_mul, h.apply_symm_apply, h.commutes] at e

Result:
case surj'.intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e : y * (algebraMap R P) ↑s = (algebraMap R P) x
⊢ ∃ x, y * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1