harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsLittleO.sub (h₁ : f₁ =o[l] g) (h₂ : f₂ =o[l] g) : (fun x => f₁ x - f₂ x) =o[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =o[l] g
h₂ : f₂ =o[l] g
⊢ (fun x => f₁ x - f₂ x) =o[l] g

Tactic:
simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem end_mem_tail_support_of_ne {u v : V} (h : u ≠ v) (p : G.Walk u v) : v ∈ p.support.tail

Proof state:
V : Type u
G : SimpleGraph V
u v : V
h : u ≠ v
p : G.Walk u v
⊢ v ∈ p.support.tail

Tactic:
obtain ⟨_, _, _, rfl⟩ := exists_eq_cons_of_ne h p

Result:
case intro.intro.intro
V : Type u
G : SimpleGraph V
u v : V
h : u ≠ v
w✝² : V
w✝¹ : G.Adj u w✝²
w✝ : G.Walk w✝² v
⊢ v ∈ (cons w✝¹ w✝).support.tail

Proof state:
case intro.intro.intro
V : Type u
G : SimpleGraph V
u v : V
h : u ≠ v
w✝² : V
w✝¹ : G.Adj u w✝²
w✝ : G.Walk w✝² v
⊢ v ∈ (cons w✝¹ w✝).support.tail

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Sqrt.lean
lemma le_sqrt' : m ≤ sqrt n ↔ m ^ 2 ≤ n

Proof state:
m n : ℕ
⊢ m ≤ n.sqrt ↔ m ^ 2 ≤ n

Tactic:
simpa only [Nat.pow_two] using le_sqrt

Result:
no goals
-- Mathlib/Topology/Exterior.lean
lemma exterior_singleton_eq_ker_nhds (x : X) : exterior {x} = (𝓝 x).ker

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
x : X
⊢ exterior {x} = (𝓝 x).ker

Tactic:
simp [exterior]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
theorem uIoo_subset_uIcc {α : Type*} [LinearOrder α] (a : α) (b : α) : uIoo a b ⊆ uIcc a b

Proof state:
α : Type u_3
inst✝ : LinearOrder α
a b : α
⊢ uIoo a b ⊆ [[a, b]]

Tactic:
simp [uIoo, uIcc, Ioo_subset_Icc_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_pos_of_neg {a : Int} (h : a < 0) : 0 < -a

Proof state:
a : Int
h : a < 0
this : -0 < -a
⊢ 0 < -a

Tactic:
rwa [Int.neg_zero] at this

Result:
no goals

Proof state:
a : Int
h : a < 0
⊢ 0 < -a

Tactic:
have : -0 < -a := Int.neg_lt_neg h

Result:
a : Int
h : a < 0
this : -0 < -a
⊢ 0 < -a
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
theorem sum_pow_mul_eq_add_pow (a b : α) (s : Finset ι) :
    (∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t)) = (a + b) ^ #s

Proof state:
ι : Type u_1
α : Type u_3
inst✝ : CommSemiring α
a b : α
s : Finset ι
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = ∑ t ∈ s.powerset, (∏ i ∈ t, a) * ∏ i ∈ s \ t, b

Tactic:
refine Finset.sum_congr rfl fun t ht => ?_

Result:
ι : Type u_1
α : Type u_3
inst✝ : CommSemiring α
a b : α
s t : Finset ι
ht : t ∈ s.powerset
⊢ a ^ #t * b ^ (#s - #t) = (∏ i ∈ t, a) * ∏ i ∈ s \ t, b

Proof state:
ι : Type u_1
α : Type u_3
inst✝ : CommSemiring α
a b : α
s : Finset ι
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = (a + b) ^ #s

Tactic:
classical
rw [← prod_const, prod_add]
refine Finset.sum_congr rfl fun t ht => ?_
rw [prod_const, prod_const, ← card_sdiff (mem_powerset.1 ht)]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝ : CommSemiring α
a b : α
s : Finset ι
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = (a + b) ^ #s

Tactic:
rw [← prod_const, prod_add]

Result:
ι : Type u_1
α : Type u_3
inst✝ : CommSemiring α
a b : α
s : Finset ι
⊢ ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = ∑ t ∈ s.powerset, (∏ i ∈ t, a) * ∏ i ∈ s \ t, b

Proof state:
ι : Type u_1
α : Type u_3
inst✝ : CommSemiring α
a b : α
s t : Finset ι
ht : t ∈ s.powerset
⊢ a ^ #t * b ^ (#s - #t) = (∏ i ∈ t, a) * ∏ i ∈ s \ t, b

Tactic:
rw [prod_const, prod_const, ← card_sdiff (mem_powerset.1 ht)]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem inv_range {ι : Sort*} {f : ι → α} : (range f)⁻¹ = range fun i => (f i)⁻¹

Proof state:
α : Type u_2
inst✝ : InvolutiveInv α
ι : Sort u_5
f : ι → α
⊢ (range f)⁻¹ = range fun i => (f i)⁻¹

Tactic:
rw [← image_inv_eq_inv]

Result:
α : Type u_2
inst✝ : InvolutiveInv α
ι : Sort u_5
f : ι → α
⊢ (fun x => x⁻¹) '' range f = range fun i => (f i)⁻¹

Proof state:
α : Type u_2
inst✝ : InvolutiveInv α
ι : Sort u_5
f : ι → α
⊢ (fun x => x⁻¹) '' range f = range fun i => (f i)⁻¹

Tactic:
exact (range_comp ..).symm

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma inl_v_fst_v (p q : ℤ) (hpq : q + 1 = p) :
    (inl φ).v p q (by rw [← hpq, add_neg_cancel_right]) ≫
      (fst φ : Cochain (mappingCone φ) F 1).v q p hpq = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.17402, u_1} C
inst✝³ : Category.{?u.17406, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : q + 1 = p
⊢ p + -1 = q

Tactic:
rw [← hpq, add_neg_cancel_right]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : q + 1 = p
⊢ (inl φ).v p q ⋯ ≫ (↑(fst φ)).v q p hpq = 𝟙 (F.X p)

Tactic:
simp [inl, fst]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem mul_add_right_right {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (z * x + y)

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + z * x)

Tactic:
exact h.add_mul_right_right z

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (z * x + y)

Tactic:
rw [add_comm]

Result:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + z * x)
-- Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean
theorem contMDiffOn_extend_symm (he : e ∈ maximalAtlas I n M) :
    ContMDiffOn 𝓘(𝕜, E) I n (e.extend I).symm (I '' e.target)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
e : PartialHomeomorph M H
he : e ∈ maximalAtlas I n M
⊢ ContMDiffOn 𝓘(𝕜, E) I n (↑(e.extend I).symm) (↑I '' e.target)

Tactic:
refine (contMDiffOn_symm_of_mem_maximalAtlas he).comp
  (contMDiffOn_model_symm.mono <| image_subset_range _ _) ?_

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
e : PartialHomeomorph M H
he : e ∈ maximalAtlas I n M
⊢ ↑I '' e.target ⊆ ↑(I.restr e.target).symm ⁻¹' e.target

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
e : PartialHomeomorph M H
he : e ∈ maximalAtlas I n M
⊢ ↑I '' e.target ⊆ ↑(I.restr e.target).symm ⁻¹' e.target

Tactic:
simp_rw [image_subset_iff, PartialEquiv.restr_coe_symm, I.toPartialEquiv_coe_symm,
  preimage_preimage, I.left_inv, preimage_id']

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
e : PartialHomeomorph M H
he : e ∈ maximalAtlas I n M
⊢ e.target ⊆ e.target

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
e : PartialHomeomorph M H
he : e ∈ maximalAtlas I n M
⊢ e.target ⊆ e.target

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem neg_left {M : Type*} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M]
    {v : VectorMeasure α M} {w : VectorMeasure α N} (h : v ≪ᵥ w) : -v ≪ᵥ w

Proof state:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
⊢ -v ≪ᵥ w

Tactic:
intro s hs

Result:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(-v) s = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(-v) s = 0

Tactic:
rw [neg_apply, h hs, neg_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_neg (p : R[X]) : degree (-p) = degree p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).degree = p.degree

Tactic:
unfold degree

Result:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).support.max = p.support.max

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).support.max = p.support.max

Tactic:
rw [support_neg]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma surjOn_id (s : Set α) : SurjOn id s s

Proof state:
α : Type u_1
s : Set α
⊢ SurjOn id s s

Tactic:
simp [SurjOn, subset_rfl]

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Basic.lean
@[simp]
lemma lt_one_iff {n : ℕ} (x : Fin (n + 2)) : x < 1 ↔ x = 0

Proof state:
n : ℕ
x : Fin (n + 2)
⊢ x < 1 ↔ x = 0

Tactic:
simp [lt_iff_val_lt_val]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem gcd_mul_right [NormalizedGCDMonoid α] (a b c : α) :
    gcd (b * a) (c * a) = gcd b c * normalize a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b c : α
⊢ gcd (b * a) (c * a) = gcd b c * normalize a

Tactic:
simp only [mul_comm, gcd_mul_left]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
/-- An exterior point of a subset `E` (i.e., a point outside the closure of `E`) is not in the
closed `δ`-thickening of `E` for small enough positive `δ`. -/
lemma eventually_not_mem_cthickening_of_infEdist_pos {E : Set α} {x : α} (h : x ∉ closure E) :
    ∀ᶠ δ in 𝓝 (0 : ℝ), x ∉ Metric.cthickening δ E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ cthickening δ E

Tactic:
obtain ⟨ε, ⟨ε_pos, ε_lt⟩⟩ := exists_real_pos_lt_infEdist_of_not_mem_closure h

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ cthickening δ E

Proof state:
case h
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δ : ℝ
hδ : δ < ε
⊢ ENNReal.ofReal δ < infEdist x E

Tactic:
exact ((ofReal_lt_ofReal_iff ε_pos).mpr hδ).trans ε_lt

Result:
no goals

Proof state:
case h
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δ : ℝ
hδ : δ < ε
⊢ x ∉ cthickening δ E

Tactic:
simp only [cthickening, mem_setOf_eq, not_le]

Result:
case h
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δ : ℝ
hδ : δ < ε
⊢ ENNReal.ofReal δ < infEdist x E

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ cthickening δ E

Tactic:
filter_upwards [eventually_lt_nhds ε_pos] with δ hδ

Result:
case h
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δ : ℝ
hδ : δ < ε
⊢ x ∉ cthickening δ E
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem Basis.parallelepiped_basisFun (ι : Type*) [Fintype ι] :
    (Pi.basisFun ℝ ι).parallelepiped = TopologicalSpace.PositiveCompacts.piIcc01 ι :=
  SetLike.coe_injective <| by
    refine Eq.trans ?_ ((uIcc_of_le ?_).trans (Set.pi_univ_Icc _ _).symm)
    · classical convert parallelepiped_single (ι := ι) 1
    · exact zero_le_one

Proof state:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
⊢ (fun i => 0) ≤ fun i => 1

Tactic:
exact zero_le_one

Result:
no goals

Proof state:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
⊢ ↑(Pi.basisFun ℝ ι).parallelepiped = uIcc (fun i => 0) fun i => 1

Tactic:
convert parallelepiped_single (ι := ι) 1

Result:
no goals

Proof state:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
⊢ ↑(Pi.basisFun ℝ ι).parallelepiped = uIcc (fun i => 0) fun i => 1

Tactic:
classical convert parallelepiped_single (ι := ι) 1

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
⊢ ↑(Pi.basisFun ℝ ι).parallelepiped = ↑(PositiveCompacts.piIcc01 ι)

Tactic:
refine Eq.trans ?_ ((uIcc_of_le ?_).trans (Set.pi_univ_Icc _ _).symm)

Result:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
⊢ ↑(Pi.basisFun ℝ ι).parallelepiped = uIcc (fun i => 0) fun i => 1

case refine_2
ι : Type u_1
inst✝ : Fintype ι
⊢ (fun i => 0) ≤ fun i => 1
-- Mathlib/Order/Monotone/Basic.lean
theorem monotoneOn_dual_iff : MonotoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ MonotoneOn f s

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ MonotoneOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ MonotoneOn f s

Tactic:
rw [monotoneOn_toDual_comp_iff, antitoneOn_comp_ofDual_iff]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem cycleOf_formPerm (hl : Nodup l) (hn : 2 ≤ l.length) (x) :
    cycleOf l.attach.formPerm x = l.attach.formPerm :=
  have hn : 2 ≤ l.attach.length

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
hn✝ : 2 ≤ l.length
x : { x // x ∈ l }
hn : 2 ≤ l.attach.length
⊢ l.attach.Nodup

Tactic:
rwa [← nodup_attach] at hl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.length
x : { x // x ∈ l }
⊢ 2 ≤ l.attach.length

Tactic:
rwa [← length_attach] at hn

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem Set.Iic.isCoatom_iff {a : Set.Iic b} : IsCoatom a ↔ ↑a ⋖ b

Proof state:
α : Type u_2
inst✝ : PartialOrder α
b : α
a : ↑(Iic b)
⊢ (range ⇑(OrderEmbedding.subtype fun c => c ≤ b)).OrdConnected

Tactic:
simpa only [OrderEmbedding.coe_subtype, Subtype.range_coe_subtype] using Set.ordConnected_Iic

Result:
no goals

Proof state:
α : Type u_2
inst✝ : PartialOrder α
b : α
a : ↑(Iic b)
⊢ a ⋖ ⊤ ↔ ↑a ⋖ b

Tactic:
refine (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => c ≤ b) ?_).symm

Result:
α : Type u_2
inst✝ : PartialOrder α
b : α
a : ↑(Iic b)
⊢ (range ⇑(OrderEmbedding.subtype fun c => c ≤ b)).OrdConnected

Proof state:
α : Type u_2
inst✝ : PartialOrder α
b : α
a : ↑(Iic b)
⊢ IsCoatom a ↔ ↑a ⋖ b

Tactic:
rw [← covBy_top_iff]

Result:
α : Type u_2
inst✝ : PartialOrder α
b : α
a : ↑(Iic b)
⊢ a ⋖ ⊤ ↔ ↑a ⋖ b
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem logMap_unit_smul (u : (𝓞 K)ˣ) (hx : mixedEmbedding.norm x ≠ 0) :
    logMap (u • x) = logEmbedding K (Additive.ofMul u) + logMap x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ logMap (u • x) = (logEmbedding K) (Additive.ofMul u) + logMap x

Tactic:
rw [unitSMul_smul, logMap_mul (by rw [norm_unit]; norm_num) hx, logMap_eq_logEmbedding]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) ≠ 0

Tactic:
rw [norm_unit]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ 1 ≠ 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ 1 ≠ 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem mem_range_preOmega_iff {x : Ordinal} : x ∈ range preOmega ↔ IsInitial x

Proof state:
x : Ordinal.{u_1}
⊢ x ∈ range ⇑preOmega ↔ x.IsInitial

Tactic:
rw [range_preOmega, mem_setOf]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem self (hp : 1 < p) : padicValNat p p = 1

Proof state:
p : ℕ
hp : 1 < p
⊢ padicValNat p p = 1

Tactic:
simp [padicValNat_def', zero_lt_one.trans hp, hp.ne']

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[reassoc]
lemma mapCyclesIso_inv_naturality [S₁.HasLeftHomology] [S₂.HasLeftHomology]
    [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
    F.map (cyclesMap φ) ≫ (S₂.mapCyclesIso F).inv =
      (S₁.mapCyclesIso F).inv ≫ cyclesMap (F.mapShortComplex.map φ)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Category.{u_4, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ F.map (cyclesMap φ) ≫ (S₂.mapCyclesIso F).inv = (S₁.mapCyclesIso F).inv ≫ cyclesMap (F.mapShortComplex.map φ)

Tactic:
rw [← cancel_epi (S₁.mapCyclesIso F).hom, ← mapCyclesIso_hom_naturality_assoc,
  Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.translate_preimage_right (hs : Convex 𝕜 s) (z : E) :
    Convex 𝕜 ((fun x => z + x) ⁻¹' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : a • (fun x => z + x) x + b • (fun x => z + x) y ∈ s
⊢ a • x + b • y ∈ (fun x => z + x) ⁻¹' s

Tactic:
rwa [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] at h

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 ((fun x => z + x) ⁻¹' s)

Tactic:
intro x hx y hy a b ha hb hab

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ (fun x => z + x) ⁻¹' s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ (fun x => z + x) ⁻¹' s

Tactic:
have h := hs hx hy ha hb hab

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : a • (fun x => z + x) x + b • (fun x => z + x) y ∈ s
⊢ a • x + b • y ∈ (fun x => z + x) ⁻¹' s
-- Mathlib/Data/List/Count.lean
theorem countP_lt_length_iff {l : List α} {p : α → Bool} :
    l.countP p < l.length ↔ ∃ a ∈ l, p a = false

Proof state:
α : Type u_1
l : List α
p : α → Bool
⊢ countP p l < l.length ↔ ∃ a, a ∈ l ∧ p a = false

Tactic:
simp [Nat.lt_iff_le_and_ne, countP_le_length]

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem min_of_mem {s : Finset α} {a : α} (h : a ∈ s) : ∃ b : α, s.min = b

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
a : α
h : a ∈ s
⊢ ∃ b, s.min = ↑b

Tactic:
obtain ⟨b, h, _⟩ := inf_le (α := WithTop α) h _ rfl

Result:
case intro.intro
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
a : α
h✝ : a ∈ s
b : α
h : s.inf WithTop.some = ↑b
right✝ : b ≤ a
⊢ ∃ b, s.min = ↑b

Proof state:
case intro.intro
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
a : α
h✝ : a ∈ s
b : α
h : s.inf WithTop.some = ↑b
right✝ : b ≤ a
⊢ ∃ b, s.min = ↑b

Tactic:
exact ⟨b, h⟩

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem congrArg_mpr_hom_left {X Y Z : C} (p : X = Y) (q : Y ⟶ Z) :
    (congrArg (fun W : C => W ⟶ Z) p).mpr q = eqToHom p ≫ q

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y ⟶ Z
⊢ ⋯.mpr q = eqToHom p ≫ q

Tactic:
cases p

Result:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
q : X ⟶ Z
⊢ ⋯.mpr q = eqToHom ⋯ ≫ q

Proof state:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
q : X ⟶ Z
⊢ ⋯.mpr q = eqToHom ⋯ ≫ q

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
@[simp] lemma left_mem_uIoc : a ∈ Ι a b ↔ b < a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a ∈ Ι a b ↔ b < a

Tactic:
simp [mem_uIoc]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp] lemma sectR_zero (a : α) : sectR (0 : Kernel (α × β) γ) a = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
a : α
⊢ sectR 0 a = 0

Tactic:
simp [sectR]

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma univ_sups_univ [Fintype α] : (univ : Finset α) ⊻ univ = univ

Proof state:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : SemilatticeSup α
inst✝ : Fintype α
⊢ univ ⊻ univ = univ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem neg_add {a b : Int} : -(a + b) = -a + -b

Proof state:
a b : Int
⊢ -(a + b) = -a + -b

Tactic:
apply Int.add_left_cancel (a := a + b)

Result:
a b : Int
⊢ a + b + -(a + b) = a + b + (-a + -b)

Proof state:
a b : Int
⊢ a + b + -(a + b) = a + b + (-a + -b)

Tactic:
rw [Int.add_right_neg, Int.add_comm a, ← Int.add_assoc, Int.add_assoc b,
  Int.add_right_neg, Int.add_zero, Int.add_right_neg]

Result:
no goals
-- Mathlib/Data/Matrix/Kronecker.lean
theorem natCast_kronecker_natCast [NonAssocSemiring α] [DecidableEq m] [DecidableEq n] (a b : ℕ) :
    (a : Matrix m m α) ⊗ₖ (b : Matrix n n α) = ↑(a * b) :=
  (diagonal_kronecker_diagonal _ _).trans <| by simp_rw [← Nat.cast_mul]; rfl

Proof state:
α : Type u_2
m : Type u_9
n : Type u_10
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
a b : ℕ
⊢ (diagonal fun mn => ↑(a * b)) = ↑(a * b)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
m : Type u_9
n : Type u_10
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
a b : ℕ
⊢ (diagonal fun mn => ↑a * ↑b) = ↑(a * b)

Tactic:
simp_rw [← Nat.cast_mul]

Result:
α : Type u_2
m : Type u_9
n : Type u_10
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
a b : ℕ
⊢ (diagonal fun mn => ↑(a * b)) = ↑(a * b)
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem aleph0_lt_lift {c : Cardinal.{u}} : ℵ₀ < lift.{v} c ↔ ℵ₀ < c

Proof state:
c : Cardinal.{u}
⊢ ℵ₀ < lift.{v, u} c ↔ ℵ₀ < c

Tactic:
simpa using lift_lt (a := ℵ₀)

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerLeft_rightUnitor (X Y : C) :
    X ◁ (ρ_ Y).hom = (α_ X Y (𝟙_ C)).inv ≫ (ρ_ (X ⊗ Y)).hom

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ X ◁ (ρ_ Y).hom = (α_ X Y (𝟙_ C)).inv ≫ (ρ_ (X ⊗ Y)).hom

Tactic:
rw [← whiskerRight_iff, comp_whiskerRight, ← cancel_epi (α_ _ _ _).inv, ←
    cancel_epi (X ◁ (α_ _ _ _).inv), pentagon_inv_assoc, triangle_assoc_comp_right, ←
    associator_inv_naturality_middle, ← whiskerLeft_comp_assoc, triangle_assoc_comp_right,
    associator_inv_naturality_right]

Result:
no goals