harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Digits.lean
theorem lt_base_pow_length_digits {b m : ℕ} (hb : 1 < b) : m < b ^ (digits b m).length

Proof state:
case succ.succ
m b : ℕ
hb : 1 < b + 1 + 1
⊢ m < (b + 1 + 1) ^ ((b + 1 + 1).digits m).length

Tactic:
simp_all

Result:
case succ.succ
m b : ℕ
⊢ m < (b + 1 + 1) ^ ((b + 1 + 1).digits m).length

Proof state:
b m : ℕ
hb : 1 < b
⊢ m < b ^ (b.digits m).length

Tactic:
rcases b with (_ | _ | b) <;> try simp_all

Result:
case succ.succ
m b : ℕ
⊢ m < (b + 1 + 1) ^ ((b + 1 + 1).digits m).length

Proof state:
case succ.succ
m b : ℕ
⊢ m < (b + 1 + 1) ^ ((b + 1 + 1).digits m).length

Tactic:
exact lt_base_pow_length_digits'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem getKey_eq [BEq α] [Hashable α] {m : Raw α β} {a : α} {h : a ∈ m} :
    m.getKey a h = Raw₀.getKey ⟨m, by change dite .. = true at h; split at h <;> simp_all⟩ a
      (by change dite .. = true at h; split at h <;> simp_all) := rfl

Proof state:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
a : α
h : (if h : 0 < m.buckets.size then Raw₀.contains ⟨m, h⟩ a else false) = true
⊢ 0 < m.buckets.size

Tactic:
split at h <;> simp_all

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
a : α
h : a ∈ m
⊢ Raw₀.contains ⟨m, ⋯⟩ a = true

Tactic:
change dite .. = true at h

Result:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
a : α
h : (if h : 0 < m.buckets.size then Raw₀.contains ⟨m, h⟩ a else false) = true
⊢ Raw₀.contains ⟨m, ⋯⟩ a = true

Proof state:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
a : α
h : (if h : 0 < m.buckets.size then Raw₀.contains ⟨m, h⟩ a else false) = true
⊢ Raw₀.contains ⟨m, ⋯⟩ a = true

Tactic:
split at h <;> simp_all

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
a : α
h : a ∈ m
⊢ 0 < m.buckets.size

Tactic:
change dite .. = true at h

Result:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
a : α
h : (if h : 0 < m.buckets.size then Raw₀.contains ⟨m, h⟩ a else false) = true
⊢ 0 < m.buckets.size
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem neLocus_self_sub_right : neLocus f (f - g) = g.support

Proof state:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ f.neLocus (f - g) = g.support

Tactic:
rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]

Result:
no goals
-- Mathlib/CategoryTheory/NatIso.lean
theorem isIso_map_iff {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) {X Y : C} (f : X ⟶ Y) :
    IsIso (F₁.map f) ↔ IsIso (F₂.map f)

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ (e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X) ≫ F₂.map f = 𝟙 (F₂.obj Y)

Tactic:
simp only [assoc, ← e.hom.naturality, IsIso.inv_hom_id_assoc, Iso.inv_hom_id_app]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ IsIso (F₂.map f)

Tactic:
refine IsIso.mk ⟨e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X, ?_, ?_⟩

Result:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ F₂.map f ≫ e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X = 𝟙 (F₂.obj X)

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ (e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X) ≫ F₂.map f = 𝟙 (F₂.obj Y)

Proof state:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ F₂.map f ≫ e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X = 𝟙 (F₂.obj X)

Tactic:
simp only [NatTrans.naturality_assoc, IsIso.hom_inv_id_assoc, Iso.inv_hom_id_app]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
this : ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → IsIso (F₁.map f) → IsIso (F₂.map f)
⊢ ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → (IsIso (F₁.map f) ↔ IsIso (F₂.map f))

Tactic:
exact fun F₁ F₂ e => ⟨this e, this e.symm⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → IsIso (F₁.map f) → IsIso (F₂.map f)

Tactic:
intro F₁ F₂ e hf

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ IsIso (F₂.map f)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → (IsIso (F₁.map f) ↔ IsIso (F₂.map f))

Tactic:
suffices ∀ {F₁ F₂ : C ⥤ D} (_ : F₁ ≅ F₂) (_ : IsIso (F₁.map f)), IsIso (F₂.map f) by
  exact fun F₁ F₂ e => ⟨this e, this e.symm⟩

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → IsIso (F₁.map f) → IsIso (F₂.map f)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
X Y : C
f : X ⟶ Y
⊢ IsIso (F₁.map f) ↔ IsIso (F₂.map f)

Tactic:
revert F₁ F₂

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : C ⥤ D}, (F₁ ≅ F₂) → (IsIso (F₁.map f) ↔ IsIso (F₂.map f))
-- Mathlib/NumberTheory/MulChar/Lemmas.lean
lemma star_apply' (χ : MulChar R ℂ) (a : R) : star (χ a) = χ⁻¹ a

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Finite Rˣ
χ : MulChar R ℂ
a : R
⊢ star (χ a) = χ⁻¹ a

Tactic:
simp only [RCLike.star_def, ← star_eq_inv, star_apply]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem mk_neg [∀ i, AddGroup (β i)] {s : Finset ι} {x : ∀ i : (↑s : Set ι), β i.1} :
    mk s (-x) = -mk s x :=
  ext fun i => by simp only [neg_apply, mk_apply]; split_ifs <;> [rfl; rw [neg_zero]]

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (mk s (-x)) i = (-mk s x) i

Tactic:
simp only [neg_apply, mk_apply]

Result:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (-x) ⟨i, H⟩ else 0) = -if H : i ∈ s then x ⟨i, H⟩ else 0

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (-x) ⟨i, H⟩ else 0) = -if H : i ∈ s then x ⟨i, H⟩ else 0

Tactic:
split_ifs <;> [rfl; rw [neg_zero]]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_mul_eq_mul_div : a / b * c = a * c / b

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b c : α
⊢ a / b * c = a * c / b

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem Finsupp.sum_inner {ι : Type*} (l : ι →₀ 𝕜) (v : ι → E) (x : E) :
    ⟪l.sum fun (i : ι) (a : 𝕜) => a • v i, x⟫ = l.sum fun (i : ι) (a : 𝕜) => conj a • ⟪v i, x⟫

Proof state:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
l : ι →₀ 𝕜
v : ι → E
x : E
⊢ (l.sum fun i a => (starRingEnd 𝕜) a • ⟪v i, x⟫_𝕜) = ∑ i ∈ l.support, ⟪l i • v i, x⟫_𝕜

Tactic:
simp only [inner_smul_left, Finsupp.sum, smul_eq_mul]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
l : ι →₀ 𝕜
v : ι → E
x : E
⊢ ⟪l.sum fun i a => a • v i, x⟫_𝕜 = l.sum fun i a => (starRingEnd 𝕜) a • ⟪v i, x⟫_𝕜

Tactic:
convert sum_inner (𝕜 := 𝕜) l.support (fun a => l a • v a) x

Result:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
l : ι →₀ 𝕜
v : ι → E
x : E
⊢ (l.sum fun i a => (starRingEnd 𝕜) a • ⟪v i, x⟫_𝕜) = ∑ i ∈ l.support, ⟪l i • v i, x⟫_𝕜
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zipWith_comm_of_comm (f : α → α → β) (comm : ∀ x y : α, f x y = f y x) (l l' : Vector α n) :
    zipWith f l l' = zipWith f l' l

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → α → β
comm : ∀ (x y : α), f x y = f y x
l l' : Vector α n
⊢ zipWith (fun b a => f a b) l' l = zipWith f l' l

Tactic:
simp only [comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → α → β
comm : ∀ (x y : α), f x y = f y x
l l' : Vector α n
⊢ zipWith f l l' = zipWith f l' l

Tactic:
rw [zipWith_comm]

Result:
α : Type u_1
β : Type u_2
n : Nat
f : α → α → β
comm : ∀ (x y : α), f x y = f y x
l l' : Vector α n
⊢ zipWith (fun b a => f a b) l' l = zipWith f l' l
-- Mathlib/Data/Set/Function.lean
theorem piecewise_le {δ : α → Type*} [∀ i, Preorder (δ i)] {s : Set α} [∀ j, Decidable (j ∈ s)]
    {f₁ f₂ g : ∀ i, δ i} (h₁ : ∀ i ∈ s, f₁ i ≤ g i) (h₂ : ∀ i ∉ s, f₂ i ≤ g i) :
    s.piecewise f₁ f₂ ≤ g := fun i => if h : i ∈ s then by simp [*] else by simp [*]

Proof state:
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g : (i : α) → δ i
h₁ : ∀ i ∈ s, f₁ i ≤ g i
h₂ : ∀ i ∉ s, f₂ i ≤ g i
i : α
h : i ∈ s
⊢ s.piecewise f₁ f₂ i ≤ g i

Tactic:
simp [*]

Result:
no goals

Proof state:
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g : (i : α) → δ i
h₁ : ∀ i ∈ s, f₁ i ≤ g i
h₂ : ∀ i ∉ s, f₂ i ≤ g i
i : α
h : i ∉ s
⊢ s.piecewise f₁ f₂ i ≤ g i

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma preimage_coe_Ioo (x y : ℝ) : Real.toEReal ⁻¹' Ioo x y = Ioo x y

Proof state:
x y : ℝ
⊢ Real.toEReal ⁻¹' Ioo ↑x ↑y = Ioo x y

Tactic:
simp_rw [← Ioi_inter_Iio]

Result:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ↑x ∩ Iio ↑y) = Ioi x ∩ Iio y

Proof state:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ↑x ∩ Iio ↑y) = Ioi x ∩ Iio y

Tactic:
simp

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
lemma limsup_piecewise {s : Set β} [DecidablePred (· ∈ s)] {v} :
    limsup (s.piecewise u v) f = blimsup u f (· ∈ s) ⊔ blimsup v f (· ∉ s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
v : β → α
a✝ : β
h : a✝ ∉ s
⊢ s.piecewise u v a✝ = v a✝

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
v : β → α
⊢ ((blimsup (s.piecewise u v) f fun x => x ∈ s) ⊔ blimsup (s.piecewise u v) f fun x => x ∉ s) =
    (blimsup u f fun x => x ∈ s) ⊔ blimsup v f fun x => x ∉ s

Tactic:
refine congr_arg₂ _ (blimsup_congr ?_) (blimsup_congr ?_) <;>
  filter_upwards with _ h using by simp [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem range_cos_infinite : (range Real.cos).Infinite

Proof state:
⊢ (Icc (-1) 1).Infinite

Tactic:
exact Icc_infinite (by norm_num)

Result:
no goals

Proof state:
⊢ -1 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ (range cos).Infinite

Tactic:
rw [Real.range_cos]

Result:
⊢ (Icc (-1) 1).Infinite
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma isoHomologyι₀_inv_naturality [L.HasHomology 0] :
    K.isoHomologyι₀.inv ≫ HomologicalComplex.homologyMap φ 0 =
      HomologicalComplex.opcyclesMap φ 0 ≫ L.isoHomologyι₀.inv

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
K L : ChainComplex C ℕ
φ : K ⟶ L
inst✝¹ : HomologicalComplex.HasHomology K 0
inst✝ : HomologicalComplex.HasHomology L 0
⊢ K.isoHomologyι₀.inv ≫ HomologicalComplex.homologyMap φ 0 = HomologicalComplex.opcyclesMap φ 0 ≫ L.isoHomologyι₀.inv

Tactic:
simp only [assoc, ← cancel_mono (L.homologyι 0),
  HomologicalComplex.homologyι_naturality, HomologicalComplex.isoHomologyι_inv_hom_id_assoc,
  HomologicalComplex.isoHomologyι_inv_hom_id, comp_id]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem exists_square_le [MulLeftStrictMono α] (a : α) : ∃ b : α, b * b ≤ a

Proof state:
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
⊢ ∃ b, b * b ≤ a

Tactic:
by_cases h : a < 1

Result:
case pos
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
⊢ ∃ b, b * b ≤ a

case neg
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : ¬a < 1
⊢ ∃ b, b * b ≤ a

Proof state:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
⊢ a * a ≤ a

Tactic:
have : a * a < a * 1 := mul_lt_mul_left' h a

Result:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
this : a * a < a * 1
⊢ a * a ≤ a

Proof state:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : ¬a < 1
⊢ 1 * 1 ≤ a

Tactic:
push_neg at h

Result:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : 1 ≤ a
⊢ 1 * 1 ≤ a

Proof state:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
this : a * a < a
⊢ a * a ≤ a

Tactic:
exact le_of_lt this

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : ¬a < 1
⊢ ∃ b, b * b ≤ a

Tactic:
use 1

Result:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : ¬a < 1
⊢ 1 * 1 ≤ a

Proof state:
case pos
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
⊢ ∃ b, b * b ≤ a

Tactic:
use a

Result:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
⊢ a * a ≤ a

Proof state:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
this : a * a < a * 1
⊢ a * a ≤ a

Tactic:
rw [mul_one] at this

Result:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
this : a * a < a
⊢ a * a ≤ a

Proof state:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : 1 ≤ a
⊢ 1 * 1 ≤ a

Tactic:
rwa [mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem reverse_take {l : List α} {n : Nat} :
    (l.take n).reverse = l.reverse.drop (l.length - n)

Proof state:
case pos
α : Type u_1
l : List α
n : Nat
h : n ≤ l.length
⊢ (take n l).reverse = drop (l.length - n) l.reverse

Tactic:
rw [drop_reverse]

Result:
case pos
α : Type u_1
l : List α
n : Nat
h : n ≤ l.length
⊢ (take n l).reverse = (take (l.length - (l.length - n)) l).reverse

Proof state:
case pos
α : Type u_1
l : List α
n : Nat
h : n ≤ l.length
⊢ (take n l).reverse = (take (l.length - (l.length - n)) l).reverse

Tactic:
congr

Result:
case pos.e_as.e_a
α : Type u_1
l : List α
n : Nat
h : n ≤ l.length
⊢ n = l.length - (l.length - n)

Proof state:
α : Type u_1
l : List α
n : Nat
h : ¬n ≤ l.length
⊢ l.length - n = 0

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ (take n l).reverse = drop (l.length - n) l.reverse

Tactic:
by_cases h : n ≤ l.length

Result:
case pos
α : Type u_1
l : List α
n : Nat
h : n ≤ l.length
⊢ (take n l).reverse = drop (l.length - n) l.reverse

case neg
α : Type u_1
l : List α
n : Nat
h : ¬n ≤ l.length
⊢ (take n l).reverse = drop (l.length - n) l.reverse

Proof state:
case neg
α : Type u_1
l : List α
n : Nat
h : ¬n ≤ l.length
⊢ (take n l).reverse = drop (l.length - n) l.reverse

Tactic:
have w : l.length - n = 0 := by omega

Result:
case neg
α : Type u_1
l : List α
n : Nat
h : ¬n ≤ l.length
w : l.length - n = 0
⊢ (take n l).reverse = drop (l.length - n) l.reverse

Proof state:
case pos.e_as.e_a
α : Type u_1
l : List α
n : Nat
h : n ≤ l.length
⊢ n = l.length - (l.length - n)

Tactic:
omega

Result:
no goals

Proof state:
case neg
α : Type u_1
l : List α
n : Nat
h : ¬n ≤ l.length
w : l.length - n = 0
⊢ (take n l).reverse = drop (l.length - n) l.reverse

Tactic:
rw [w, drop_zero, take_of_length_le]

Result:
case neg
α : Type u_1
l : List α
n : Nat
h : ¬n ≤ l.length
w : l.length - n = 0
⊢ l.length ≤ n

Proof state:
case neg
α : Type u_1
l : List α
n : Nat
h : ¬n ≤ l.length
w : l.length - n = 0
⊢ l.length ≤ n

Tactic:
omega

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_sInter {x y : ZFSet} (h : x.Nonempty) : y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z

Proof state:
x y : ZFSet.{u_1}
h : x.Nonempty
mem : ∀ z ∈ x, y ∈ z
⊢ y ∈ ⋃₀ x

Tactic:
apply mem_sUnion.mpr

Result:
x y : ZFSet.{u_1}
h : x.Nonempty
mem : ∀ z ∈ x, y ∈ z
⊢ ∃ z ∈ x, y ∈ z

Proof state:
x y : ZFSet.{u_1}
mem : ∀ z ∈ x, y ∈ z
s : ZFSet.{u_1}
h : s ∈ x.toSet
⊢ ∃ z ∈ x, y ∈ z

Tactic:
exact ⟨_, h, mem _ h⟩

Result:
no goals

Proof state:
x y : ZFSet.{u_1}
h : x.Nonempty
⊢ y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z

Tactic:
unfold sInter

Result:
x y : ZFSet.{u_1}
h : x.Nonempty
⊢ y ∈ ZFSet.sep (fun y => ∀ z ∈ x, y ∈ z) (⋃₀ x) ↔ ∀ z ∈ x, y ∈ z

Proof state:
x y : ZFSet.{u_1}
h : x.Nonempty
⊢ (∀ z ∈ x, y ∈ z) → y ∈ ⋃₀ x

Tactic:
intro mem

Result:
x y : ZFSet.{u_1}
h : x.Nonempty
mem : ∀ z ∈ x, y ∈ z
⊢ y ∈ ⋃₀ x

Proof state:
x y : ZFSet.{u_1}
h : x.Nonempty
⊢ y ∈ ZFSet.sep (fun y => ∀ z ∈ x, y ∈ z) (⋃₀ x) ↔ ∀ z ∈ x, y ∈ z

Tactic:
simp only [and_iff_right_iff_imp, mem_sep]

Result:
x y : ZFSet.{u_1}
h : x.Nonempty
⊢ (∀ z ∈ x, y ∈ z) → y ∈ ⋃₀ x

Proof state:
x y : ZFSet.{u_1}
h : x.Nonempty
mem : ∀ z ∈ x, y ∈ z
⊢ ∃ z ∈ x, y ∈ z

Tactic:
replace ⟨s, h⟩ := h

Result:
x y : ZFSet.{u_1}
mem : ∀ z ∈ x, y ∈ z
s : ZFSet.{u_1}
h : s ∈ x.toSet
⊢ ∃ z ∈ x, y ∈ z
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem recF_eq_of_Wequiv {α : Type u} (u : F α → α) (x y : q.P.W) :
    Wequiv x y → recF u x = recF u y

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
h : Wequiv x y
⊢ recF u x = recF u y

Tactic:
induction h with
| ind a f f' _ ih => simp only [recF_eq', PFunctor.map_eq, Function.comp_def, ih]
| abs a f a' f' h => simp only [recF_eq', abs_map, h]
| trans x y z _ _ ih₁ ih₂ => exact Eq.trans ih₁ ih₂

Result:
no goals

Proof state:
case ind
F : Type u → Type u
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
a : (P F).A
f f' : (P F).B a → (P F).W
a✝ : ∀ (x : (P F).B a), Wequiv (f x) (f' x)
ih : ∀ (x : (P F).B a), recF u (f x) = recF u (f' x)
⊢ recF u (WType.mk a f) = recF u (WType.mk a f')

Tactic:
simp only [recF_eq', PFunctor.map_eq, Function.comp_def, ih]

Result:
no goals

Proof state:
case trans
F : Type u → Type u
q : QPF F
α : Type u
u : F α → α
x✝ y✝ x y z : (P F).W
a✝¹ : Wequiv x y
a✝ : Wequiv y z
ih₁ : recF u x = recF u y
ih₂ : recF u y = recF u z
⊢ recF u x = recF u z

Tactic:
exact Eq.trans ih₁ ih₂

Result:
no goals

Proof state:
case abs
F : Type u → Type u
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
a : (P F).A
f : (P F).B a → (P F).W
a' : (P F).A
f' : (P F).B a' → (P F).W
h : abs ⟨a, f⟩ = abs ⟨a', f'⟩
⊢ recF u (WType.mk a f) = recF u (WType.mk a' f')

Tactic:
simp only [recF_eq', abs_map, h]

Result:
no goals

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
⊢ Wequiv x y → recF u x = recF u y

Tactic:
intro h

Result:
F : Type u → Type u
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
h : Wequiv x y
⊢ recF u x = recF u y
-- Mathlib/RingTheory/Idempotents.lean
lemma OrthogonalIdempotents.prod_one_sub {I : Type*} {e : I → R}
    (he : OrthogonalIdempotents e) (s : Finset I) :
    ∏ i ∈ s, (1 - e i) = 1 - ∑ i ∈ s, e i

Proof state:
case cons
R : Type u_1
inst✝ : CommRing R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
a : I
s : Finset I
has : a ∉ s
ih : ∏ i ∈ s, (1 - e i) = 1 - ∑ i ∈ s, e i
⊢ ∏ i ∈ Finset.cons a s has, (1 - e i) = 1 - ∑ i ∈ Finset.cons a s has, e i

Tactic:
simp [ih, sub_mul, mul_sub, he.mul_sum_of_not_mem has, sub_sub]

Result:
no goals

Proof state:
case empty
R : Type u_1
inst✝ : CommRing R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
⊢ ∏ i ∈ ∅, (1 - e i) = 1 - ∑ i ∈ ∅, e i

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
s : Finset I
⊢ ∏ i ∈ s, (1 - e i) = 1 - ∑ i ∈ s, e i

Tactic:
induction s using Finset.cons_induction with
| empty => simp
| cons a s has ih =>
  simp [ih, sub_mul, mul_sub, he.mul_sum_of_not_mem has, sub_sub]

Result:
no goals
-- Mathlib/Data/Finite/Card.lean
theorem card_le_of_surjective [Finite α] (f : α → β) (hf : Function.Surjective f) :
    Nat.card β ≤ Nat.card α

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
this✝ : Fintype α
this : Fintype β
⊢ Nat.card β ≤ Nat.card α

Tactic:
simpa only [Nat.card_eq_fintype_card] using Fintype.card_le_of_surjective f hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
this : Fintype α
⊢ Nat.card β ≤ Nat.card α

Tactic:
haveI := Fintype.ofSurjective f hf

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
this✝ : Fintype α
this : Fintype β
⊢ Nat.card β ≤ Nat.card α

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
⊢ Nat.card β ≤ Nat.card α

Tactic:
haveI := Fintype.ofFinite α

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
this : Fintype α
⊢ Nat.card β ≤ Nat.card α

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
⊢ Nat.card β ≤ Nat.card α

Tactic:
classical
haveI := Fintype.ofFinite α
haveI := Fintype.ofSurjective f hf
simpa only [Nat.card_eq_fintype_card] using Fintype.card_le_of_surjective f hf

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean
theorem unitization_range :
    (unitization s).range = subalgebraOfSubring (.closure s)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : SetLike S R
hSR : NonUnitalSubringClass S R
s : S
this : SMulMemClass S ℤ R
⊢ (unitization s).range = subalgebraOfSubring (Subring.closure ↑s)

Tactic:
rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_int]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : SetLike S R
hSR : NonUnitalSubringClass S R
s : S
⊢ (unitization s).range = subalgebraOfSubring (Subring.closure ↑s)

Tactic:
have := AddSubgroupClass.zsmulMemClass (S := S)

Result:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : SetLike S R
hSR : NonUnitalSubringClass S R
s : S
this : SMulMemClass S ℤ R
⊢ (unitization s).range = subalgebraOfSubring (Subring.closure ↑s)