harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_length_le (l : List (Option α)) : l.reduceOption.length ≤ l.length

Proof state:
α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length ≤ l.reduceOption.length + (filter Option.isNone l).length

Tactic:
apply Nat.le_add_right

Result:
no goals

Proof state:
α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length ≤ l.length

Tactic:
rw [length_eq_reduceOption_length_add_filter_none]

Result:
α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length ≤ l.reduceOption.length + (filter Option.isNone l).length
-- Mathlib/Algebra/Group/Pi/Basic.lean
theorem extend_inv [Inv γ] (f : α → β) (g : α → γ) (e : β → γ) :
    Function.extend f g⁻¹ e⁻¹ = (Function.extend f g e)⁻¹

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
x : β
⊢ extend f g⁻¹ e⁻¹ x = (extend f g e)⁻¹ x

Tactic:
simp only [not_exists, extend_def, Pi.inv_apply, apply_dite Inv.inv]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
⊢ extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹

Tactic:
funext x

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
x : β
⊢ extend f g⁻¹ e⁻¹ x = (extend f g e)⁻¹ x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
⊢ extend f g⁻¹ e⁻¹ = (extend f g e)⁻¹

Tactic:
classical
funext x
simp only [not_exists, extend_def, Pi.inv_apply, apply_dite Inv.inv]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasStrictDerivAt.clm_comp (hc : HasStrictDerivAt c c' x) (hd : HasStrictDerivAt d d' x) :
    HasStrictDerivAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
⊢ HasStrictDerivAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x

Tactic:
have := (hc.hasStrictFDerivAt.clm_comp hd.hasStrictFDerivAt).hasStrictDerivAt

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
this :
  HasStrictDerivAt (fun y => (c y).comp (d y))
    ((((compL 𝕜 E F G) (c x)).comp (smulRight 1 d') + ((compL 𝕜 E F G).flip (d x)).comp (smulRight 1 c')) 1) x
⊢ HasStrictDerivAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
this :
  HasStrictDerivAt (fun y => (c y).comp (d y))
    ((((compL 𝕜 E F G) (c x)).comp (smulRight 1 d') + ((compL 𝕜 E F G).flip (d x)).comp (smulRight 1 c')) 1) x
⊢ HasStrictDerivAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x

Tactic:
rwa [add_apply, comp_apply, comp_apply, smulRight_apply, smulRight_apply, one_apply, one_smul,
  one_smul, add_comm] at this

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem add_coeff_zero (x y : 𝕎 R) : (x + y).coeff 0 = x.coeff 0 + y.coeff 0

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ (x + y).coeff 0 = x.coeff 0 + y.coeff 0

Tactic:
simp [add_coeff, peval, Function.uncurry]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
@[simp] lemma image2_mk_eq_prod : image2 Prod.mk s t = s ×ˢ t := ext <| by simp

Proof state:
α : Type u_1
β : Type u_3
s : Set α
t : Set β
⊢ ∀ (x : α × β), x ∈ image2 Prod.mk s t ↔ x ∈ s ×ˢ t

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem take_concat_get (l : List α) (i : Nat) (h : i < l.length) :
    (l.take i).concat l[i] = l.take (i+1) :=
  Eq.symm <| (append_left_inj _).1 <| (take_append_drop (i+1) l).trans <| by
    rw [concat_eq_append, append_assoc, singleton_append, getElem_cons_drop_succ_eq_drop, take_append_drop]

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.length
⊢ l = (take i l).concat l[i] ++ drop (i + 1) l

Tactic:
rw [concat_eq_append, append_assoc, singleton_append, getElem_cons_drop_succ_eq_drop, take_append_drop]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_lt_inv_mul₀ (ha : 0 < a) : 1 < a⁻¹ * b ↔ a < b

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
⊢ 1 < a⁻¹ * b ↔ a < b

Tactic:
rw [lt_inv_mul_iff₀ ha, mul_one]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem _root_.NumberField.mixedEmbedding_injective [NumberField K] :
    Function.Injective (NumberField.mixedEmbedding K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Injective ⇑(mixedEmbedding K)

Tactic:
exact RingHom.injective _

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_induction {p : α → Prop} (hb : p ⊥) (hp : ∀ a₁, p a₁ → ∀ a₂, p a₂ → p (a₁ ⊔ a₂))
    (hs : ∀ b ∈ s, p (f b)) : p (s.sup f)

Proof state:
case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : (∀ b ∈ s✝, p (f b)) → p (s✝.sup f)
hs : p (f a✝) ∧ ∀ x ∈ s✝, p (f x)
⊢ p (f a✝ ⊔ s✝.sup f)

Tactic:
exact hp _ hs.1 _ (ih hs.2)

Result:
no goals

Proof state:
case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : (∀ b ∈ s✝, p (f b)) → p (s✝.sup f)
hs : ∀ b ∈ cons a✝ s✝ h✝, p (f b)
⊢ p ((cons a✝ s✝ h✝).sup f)

Tactic:
simp only [sup_cons, forall_mem_cons] at hs ⊢

Result:
case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : (∀ b ∈ s✝, p (f b)) → p (s✝.sup f)
hs : p (f a✝) ∧ ∀ x ∈ s✝, p (f x)
⊢ p (f a✝ ⊔ s✝.sup f)

Proof state:
case empty
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ ∅, p (f b)
⊢ p (∅.sup f)

Tactic:
exact hb

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
⊢ p (s.sup f)

Tactic:
induction s using Finset.cons_induction with
| empty => exact hb
| cons _ _ _ ih =>
  simp only [sup_cons, forall_mem_cons] at hs ⊢
  exact hp _ hs.1 _ (ih hs.2)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_filter (q) (l : Array α) :
    filter p (filter q l) = filter (fun a => p a && q a) l

Proof state:
α : Type u_1
p q : α → Bool
l : Array α
⊢ filter p (filter q l) = filter (fun a => p a && q a) l

Tactic:
apply ext'

Result:
case h
α : Type u_1
p q : α → Bool
l : Array α
⊢ (filter p (filter q l)).toList = (filter (fun a => p a && q a) l).toList

Proof state:
case h
α : Type u_1
p q : α → Bool
l : Array α
⊢ (filter p (filter q l)).toList = (filter (fun a => p a && q a) l).toList

Tactic:
simp only [toList_filter, List.filter_filter]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive sub_nsmul]
lemma pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ :=
  eq_mul_inv_of_mul_eq <| by rw [← pow_add, Nat.sub_add_cancel h]

Proof state:
G : Type u_3
inst✝ : Group G
a : G
m n : ℕ
h : n ≤ m
⊢ a ^ (m - n) * a ^ n = a ^ m

Tactic:
rw [← pow_add, Nat.sub_add_cancel h]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean
theorem upper_sub_lower_splitCenterBox (I : Box ι) (s : Set ι) (i : ι) :
    (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2

Proof state:
ι : Type u_1
I : Box ι
s : Set ι
i : ι
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2

Tactic:
by_cases i ∈ s <;> field_simp [splitCenterBox] <;> field_simp [mul_two, two_mul]

Result:
no goals
-- Mathlib/Data/ENat/Lattice.lean
lemma iSup_add_iSup_of_monotone {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f g : ι → ℕ∞}
    (hf : Monotone f) (hg : Monotone g) : iSup f + iSup g = ⨆ a, f a + g a :=
  iSup_add_iSup fun i j ↦ (exists_ge_ge i j).imp fun _k ⟨hi, hj⟩ ↦ by gcongr <;> apply_rules

Proof state:
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ f i + g j ≤ f _k + g _k

Tactic:
gcongr <;> apply_rules

Result:
no goals
-- Mathlib/Algebra/Group/EvenFunction.lean
lemma Even.smul_odd [Monoid β] [AddGroup γ] [DistribMulAction β γ] (hf : f.Even) (hg : g.Odd) :
    (f • g).Odd

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Monoid β
inst✝¹ : AddGroup γ
inst✝ : DistribMulAction β γ
hf : Function.Even f
hg : Function.Odd g
⊢ Function.Odd (f • g)

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Monoid β
inst✝¹ : AddGroup γ
inst✝ : DistribMulAction β γ
hf : Function.Even f
hg : Function.Odd g
a : α
⊢ (f • g) (-a) = -(f • g) a

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Monoid β
inst✝¹ : AddGroup γ
inst✝ : DistribMulAction β γ
hf : Function.Even f
hg : Function.Odd g
a : α
⊢ (f • g) (-a) = -(f • g) a

Tactic:
simp only [Pi.smul_apply', hf a, hg a, smul_neg]

Result:
no goals
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem projIic_of_mem (hx : x ∈ Iic b) : projIic b x = ⟨x, hx⟩

Proof state:
α : Type u_1
inst✝ : LinearOrder α
b x : α
hx : x ∈ Iic b
⊢ projIic b x = ⟨x, hx⟩

Tactic:
simpa [projIic]

Result:
no goals
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
theorem start_path : f x₀ = g x₂

Proof state:
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ f x₀ = g x₂

Tactic:
convert hfg 0 <;> simp only [Path.source]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma ideal_ext_iff {I J : Ideal Γ(X, U)} :
    I = J ↔ ∀ (x : X) (h : x ∈ U),
      I.map (X.presheaf.germ U x h).hom = J.map (X.presheaf.germ U x h).hom

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
I J : Ideal ↑Γ(X, U)
⊢ I = J ↔
    ∀ (x : ↑↑X.toPresheafedSpace) (h : x ∈ U),
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I =
        Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J

Tactic:
simp_rw [le_antisymm_iff, hU.ideal_le_iff, forall_and]

Result:
no goals
-- Mathlib/NumberTheory/EulerProduct/Basic.lean
/-- A version of `EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric`
in terms of the value of the series. -/
lemma prod_filter_prime_geometric_eq_tsum_factoredNumbers {f : ℕ →* F} (hsum : Summable f)
    (s : Finset ℕ) :
    ∏ p ∈ s with p.Prime, (1 - f p)⁻¹ = ∑' m : factoredNumbers s, f m

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
s : Finset ℕ
⊢ ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1

Tactic:
exact fun {_} hp ↦ hsum.norm_lt_one hp.one_lt

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
s : Finset ℕ
⊢ ∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹ = ∑' (m : ↑(factoredNumbers s)), f ↑m

Tactic:
refine (summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric ?_ s).2.tsum_eq.symm

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
s : Finset ℕ
⊢ ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_congr_set_coe (f : β → α) {s t : Set β} (h : s = t) :
    ∏' x : s, f x = ∏' x : t, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
s t : Set β
h : s = t
⊢ ∏' (x : ↑s), f ↑x = ∏' (x : ↑t), f ↑x

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivAt.finset_prod [DecidableEq ι] {x : E}
    (hg : ∀ i ∈ u, HasFDerivAt (g i) (g' i) x) :
    HasFDerivAt (∏ i ∈ u, g i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasFDerivAt (g i) (g' i) x
⊢ (∑ i ∈ u.attach, (∏ j ∈ u.attach.erase i, g (↑j) x) • proj i).comp (pi fun i => g' ↑i) =
    ∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasFDerivAt (g i) (g' i) x
x✝ : E
⊢ ((∑ i ∈ u.attach, (∏ j ∈ u.attach.erase i, g (↑j) x) • proj i).comp (pi fun i => g' ↑i)) x✝ =
    (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x✝
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem tendsto_log_nhdsWithin_zero : Tendsto log (𝓝[≠] 0) atBot

Proof state:
⊢ Tendsto log (𝓝[>] 0) atBot

Tactic:
simpa [← tendsto_comp_exp_atBot] using tendsto_id

Result:
no goals

Proof state:
⊢ Tendsto (fun x => log |x|) (𝓝[≠] 0) atBot

Tactic:
refine Tendsto.comp (g := log) ?_ tendsto_abs_nhdsWithin_zero

Result:
⊢ Tendsto log (𝓝[>] 0) atBot

Proof state:
⊢ Tendsto log (𝓝[≠] 0) atBot

Tactic:
rw [← show _ = log from funext log_abs]

Result:
⊢ Tendsto (fun x => log |x|) (𝓝[≠] 0) atBot
-- Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
theorem associator_inv_fst_fst (X Y Z : C) :
    (α_ X Y Z).inv ≫ prod.fst ≫ prod.fst = prod.fst

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ prod.fst ≫ prod.fst = prod.fst

Tactic:
simp [associator_inv]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma lt_iff_add_one_le : m < n ↔ m + 1 ≤ n

Proof state:
m n : ℕ
⊢ m < n ↔ m + 1 ≤ n

Tactic:
rw [succ_le_iff]

Result:
no goals
-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem nsmul_pow_two_powHalf (n : ℕ) : 2 ^ n * powHalf n = 1

Proof state:
n : ℕ
⊢ 2 ^ n * powHalf n = 1

Tactic:
induction' n with n hn

Result:
case zero

⊢ 2 ^ 0 * powHalf 0 = 1

case succ
n : ℕ
hn : 2 ^ n * powHalf n = 1
⊢ 2 ^ (n + 1) * powHalf (n + 1) = 1

Proof state:
case succ
n : ℕ
hn : 2 ^ n * powHalf n = 1
⊢ 2 ^ (n + 1) * powHalf (n + 1) = 1

Tactic:
rw [← hn, ← double_powHalf_succ_eq_powHalf n, ← mul_assoc (2 ^ n) 2 (powHalf (n + 1)),
  pow_succ', mul_comm 2 (2 ^ n)]

Result:
no goals

Proof state:
case zero

⊢ 2 ^ 0 * powHalf 0 = 1

Tactic:
simp only [pow_zero, powHalf_zero, mul_one]

Result:
no goals
-- Mathlib/Data/PNat/Prime.lean
theorem Coprime.factor_eq_gcd_left {a b m n : ℕ+} (cop : m.Coprime n) (am : a ∣ m) (bn : b ∣ n) :
    a = (a * b).gcd m

Proof state:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (a * b).gcd m

Tactic:
rw [gcd_eq_left_iff_dvd] at am

Result:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ a = (a * b).gcd m

Proof state:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ (a * b).gcd m = a.gcd m

Tactic:
apply Coprime.gcd_mul_right_cancel a

Result:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ b.Coprime m

Proof state:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ a.gcd m = (a * b).gcd m

Tactic:
rw [eq_comm]

Result:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ (a * b).gcd m = a.gcd m

Proof state:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ a = (a * b).gcd m

Tactic:
conv_lhs => rw [← am]

Result:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ a.gcd m = (a * b).gcd m

Proof state:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ b.Coprime m

Tactic:
apply Coprime.coprime_dvd_left bn cop.symm

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/UV.lean
theorem card_compression (u v : α) (s : Finset α) : #(𝓒 u v s) = #s

Proof state:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u v : α
s : Finset α
⊢ #(𝓒 u v s) = #s

Tactic:
rw [compression, card_union_of_disjoint compress_disjoint, filter_image,
  card_image_of_injOn compress_injOn, ← card_union_of_disjoint (disjoint_filter_filter_neg s _ _),
  filter_union_filter_neg_eq]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_add_cyc3_neg_right {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
    o.oangle x (-y) + o.oangle y (-z) + o.oangle z (-x) = π

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle x (-y) + o.oangle y (-z) + o.oangle z (-x) = ↑π

Tactic:
simp_rw [← oangle_neg_left_eq_neg_right, o.oangle_add_cyc3_neg_left hx hy hz]

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

Proof state:
p : Prop
h : Decidable p
t : Bool
⊢ (if p then t else false) = (decide p && t)

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

Result:
no goals

Proof state:
case isTrue
p✝ : Prop
t : Bool
p : p✝
⊢ (if p✝ then t else false) = (decide p✝ && t)

Tactic:
simp [p]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Basic.lean
theorem isOpenEmbedding_iff_isIso_comp' {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] :
    IsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding g

Proof state:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f)) ↔ IsOpenEmbedding ⇑(ConcreteCategory.hom g)

Tactic:
exact isOpenEmbedding_iff_isIso_comp f g

Result:
no goals
-- Mathlib/NumberTheory/EulerProduct/Basic.lean
/-- A version of `EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric`
in terms of the value of the series. -/
lemma prod_primesBelow_geometric_eq_tsum_smoothNumbers {f : ℕ →* F} (hsum : Summable f) (N : ℕ) :
    ∏ p ∈ N.primesBelow, (1 - f p)⁻¹ = ∑' m : N.smoothNumbers, f m

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
N : ℕ
⊢ ∏ p ∈ N.primesBelow, (1 - f p)⁻¹ = ∑' (m : ↑N.smoothNumbers), f ↑m

Tactic:
rw [smoothNumbers_eq_factoredNumbers, primesBelow]

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
N : ℕ
⊢ ∏ p ∈ filter (fun p => Nat.Prime p) (range N), (1 - f p)⁻¹ = ∑' (m : ↑(factoredNumbers (range N))), f ↑m

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
N : ℕ
⊢ ∏ p ∈ filter (fun p => Nat.Prime p) (range N), (1 - f p)⁻¹ = ∑' (m : ↑(factoredNumbers (range N))), f ↑m

Tactic:
exact prod_filter_prime_geometric_eq_tsum_factoredNumbers hsum _

Result:
no goals
-- Mathlib/Order/PartialSups.lean
theorem partialSups_eq_sup_range [OrderBot α] (f : ℕ → α) (n : ℕ) :
    partialSups f n = (Finset.range (n + 1)).sup f :=
  eq_of_forall_ge_iff fun _ ↦ by simp [Nat.lt_succ_iff]

Proof state:
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
n : ℕ
x✝ : α
⊢ (partialSups f) n ≤ x✝ ↔ (range (n + 1)).sup f ≤ x✝

Tactic:
simp [Nat.lt_succ_iff]

Result:
no goals
-- Mathlib/Data/Int/Interval.lean
theorem card_fintype_Ioo : Fintype.card (Set.Ioo a b) = (b - a - 1).toNat

Proof state:
a b : ℤ
⊢ Fintype.card ↑(Set.Ioo a b) = (b - a - 1).toNat

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/WithAbs.lean
theorem pseudoMetricSpace_induced_of_comp (h : ∀ x, ‖f x‖ = v x) :
    PseudoMetricSpace.induced f inferInstance = (normedField v).toPseudoMetricSpace

Proof state:
case h.dist.h.h
K : Type u_3
inst✝¹ : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝ : NormedField L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x✝¹ x✝ : WithAbs v
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
exact isometry_of_comp h |>.dist_eq _ _

Result:
no goals

Proof state:
K : Type u_3
inst✝¹ : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝ : NormedField L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
⊢ PseudoMetricSpace.induced (⇑f) inferInstance = MetricSpace.toPseudoMetricSpace

Tactic:
ext

Result:
case h.dist.h.h
K : Type u_3
inst✝¹ : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝ : NormedField L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
x✝¹ x✝ : WithAbs v
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
-- Mathlib/NumberTheory/Divisors.lean
theorem mem_divisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) {x : ℕ} :
    x ∈ divisors (p ^ k) ↔ ∃ j ≤ k, x = p ^ j

Proof state:
p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∈ (p ^ k).divisors ↔ ∃ j ≤ k, x = p ^ j

Tactic:
rw [mem_divisors, Nat.dvd_prime_pow pp, and_iff_left (ne_of_gt (pow_pos pp.pos k))]

Result:
no goals
-- Mathlib/CategoryTheory/Opposites.lean
theorem isIso_unop_iff {X Y : Cᵒᵖ} (f : X ⟶ Y) : IsIso f.unop ↔ IsIso f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ IsIso f.unop ↔ IsIso f

Tactic:
rw [← isIso_op_iff f.unop, Quiver.Hom.op_unop]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ofLE_comp_ofLEMk {B A : C} (X Y : Subobject B) (f : A ⟶ B) [Mono f] (h₁ : X ≤ Y)
    (h₂ : Y ≤ mk f) : ofLE X Y h₁ ≫ ofLEMk Y f h₂ = ofLEMk X f (h₁.trans h₂)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
X Y : Subobject B
f : A ⟶ B
inst✝ : Mono f
h₁ : X ≤ Y
h₂ : Y ≤ mk f
⊢ underlying.map (h₁.hom ≫ h₂.hom) ≫ (underlyingIso f).hom = underlying.map ⋯.hom ≫ (underlyingIso f).hom

Tactic:
congr 1

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
X Y : Subobject B
f : A ⟶ B
inst✝ : Mono f
h₁ : X ≤ Y
h₂ : Y ≤ mk f
⊢ X.ofLE Y h₁ ≫ Y.ofLEMk f h₂ = X.ofLEMk f ⋯

Tactic:
simp only [ofMkLE, ofLEMk, ofLE, ← Functor.map_comp_assoc underlying]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
X Y : Subobject B
f : A ⟶ B
inst✝ : Mono f
h₁ : X ≤ Y
h₂ : Y ≤ mk f
⊢ underlying.map (h₁.hom ≫ h₂.hom) ≫ (underlyingIso f).hom = underlying.map ⋯.hom ≫ (underlyingIso f).hom
-- Mathlib/Computability/ContextFreeGrammar.lean
@[simp] lemma produces_reverse_comm : g.reverse.Produces u v ↔ g.Produces u.reverse v.reverse :=
  (Equiv.ofBijective _ ContextFreeRule.reverse_bijective).exists_congr
    (by simp [ContextFreeRule.reverse_involutive.eq_iff])

Proof state:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ ∀ (a : ContextFreeRule T g.reverse.NT),
    a ∈ g.reverse.rules ∧ a.Rewrites u v ↔
      (Equiv.ofBijective ContextFreeRule.reverse ⋯) a ∈ g.rules ∧
        ((Equiv.ofBijective ContextFreeRule.reverse ⋯) a).Rewrites u.reverse v.reverse

Tactic:
simp [ContextFreeRule.reverse_involutive.eq_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_id (l : Array α) : map (id : α → α) l = l

Proof state:
α : Type u_1
l : Array α
⊢ map id l = l

Tactic:
cases l <;> simp_all

Result:
no goals