harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Seq/Computation.lean
theorem map_think (f : α → β) : ∀ s, map f (think s) = think (map f s)
  | ⟨s, al⟩ => by apply Subtype.eq; dsimp [think, map]; rw [Stream'.map_cons]

Proof state:
case a
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ Stream'.map (fun o => Option.rec none (fun val => some (f val)) o) (Stream'.cons none s) =
    Stream'.cons none (Stream'.map (fun o => Option.rec none (fun val => some (f val)) o) s)

Tactic:
rw [Stream'.map_cons]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ map f (think ⟨s, al⟩) = (map f ⟨s, al⟩).think

Tactic:
apply Subtype.eq

Result:
case a
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ ↑(map f (think ⟨s, al⟩)) = ↑(map f ⟨s, al⟩).think

Proof state:
case a
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ ↑(map f (think ⟨s, al⟩)) = ↑(map f ⟨s, al⟩).think

Tactic:
dsimp [think, map]

Result:
case a
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ Stream'.map (fun o => Option.rec none (fun val => some (f val)) o) (Stream'.cons none s) =
    Stream'.cons none (Stream'.map (fun o => Option.rec none (fun val => some (f val)) o) s)
-- Mathlib/Analysis/Convex/Deriv.lean
/-- If `f : ℝ → ℝ` is convex on `S` and right-differentiable at `x ∈ S`, then the slope of any
secant line with left endpoint at `x` is bounded below by the right derivative of `f` at `x`. -/
lemma le_slope_of_hasDerivWithinAt_Ioi (hfc : ConvexOn ℝ S f)
    (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Ioi x) x) :
    f' ≤ slope f x y

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝 x, x_1 ∈ Ioi x → (f x_1 - f x) / (x_1 - x) ≤ (f y - f x) / (y - x)

Tactic:
filter_upwards [eventually_lt_nhds hxy] with t ht (ht' : x < t)

Result:
case h
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
t : ℝ
ht : t < y
ht' : x < t
⊢ (f t - f x) / (t - x) ≤ (f y - f x) / (y - x)

Proof state:
case h
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
t : ℝ
ht : t < y
ht' : x < t
⊢ t ∈ S

Tactic:
exact hfc.1.ordConnected.out hx hy ⟨ht'.le, ht.le⟩

Result:
no goals

Proof state:
case h
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
t : ℝ
ht : t < y
ht' : x < t
⊢ (f t - f x) / (t - x) ≤ (f y - f x) / (y - x)

Tactic:
refine hfc.secant_mono hx (?_ : t ∈ S) hy ht'.ne' hxy.ne' ht.le

Result:
case h
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
t : ℝ
ht : t < y
ht' : x < t
⊢ t ∈ S

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] x, slope f x c ≤ slope f x y

Tactic:
simp_rw [eventually_nhdsWithin_iff, slope_def_field]

Result:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝 x, x_1 ∈ Ioi x → (f x_1 - f x) / (x_1 - x) ≤ (f y - f x) / (y - x)

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ f' ≤ slope f x y

Tactic:
apply le_of_tendsto <| (hasDerivWithinAt_iff_tendsto_slope' not_mem_Ioi_self).mp hf'

Result:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] x, slope f x c ≤ slope f x y
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem basisSets_neg (U) (hU' : U ∈ p.basisSets) :
    ∃ V ∈ p.basisSets, V ⊆ (fun x : E => -x) ⁻¹' U

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU' : U ∈ p.basisSets
⊢ ∃ V ∈ p.basisSets, V ⊆ (fun x => -x) ⁻¹' U

Tactic:
rcases p.basisSets_iff.mp hU' with ⟨s, r, _, hU⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU' : U ∈ p.basisSets
s : Finset ι
r : ℝ
left✝ : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ p.basisSets, V ⊆ (fun x => -x) ⁻¹' U

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU' : U ∈ p.basisSets
s : Finset ι
r : ℝ
left✝ : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ p.basisSets, V ⊆ (fun x => -x) ⁻¹' U

Tactic:
rw [hU, neg_preimage, neg_ball (s.sup p), neg_zero]

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU' : U ∈ p.basisSets
s : Finset ι
r : ℝ
left✝ : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ p.basisSets, V ⊆ (s.sup p).ball 0 r

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU' : U ∈ p.basisSets
s : Finset ι
r : ℝ
left✝ : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ p.basisSets, V ⊆ (s.sup p).ball 0 r

Tactic:
exact ⟨U, hU', Eq.subset hU⟩

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem preimage_coe_Ioc : (some : α → WithBot α) ⁻¹' Ioc a b = Ioc a b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Ioc ↑a ↑b = Ioc a b

Tactic:
simp [← Ioi_inter_Iic]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
@[simp] lemma num_nonneg : 0 ≤ q.num ↔ 0 ≤ q

Proof state:
q : ℚ
⊢ 0 ≤ q.num ↔ 0 ≤ q

Tactic:
simp [Int.le_iff_lt_or_eq, instLE, Rat.blt, Int.not_lt]

Result:
q : ℚ
⊢ 0 < q.num ∨ 0 = q.num → ¬q = 0 → q.num < 0 ∨ q = 0 → 0 < q.num ∨ 0 = q.num

Proof state:
q : ℚ
⊢ 0 < q.num ∨ 0 = q.num → ¬q = 0 → q.num < 0 ∨ q = 0 → 0 < q.num ∨ 0 = q.num

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
lemma mulShift_unit_eq_one_iff (ψ : AddChar R M) {u : R} (hu : IsUnit u) :
    ψ.mulShift u = 1 ↔ ψ = 1

Proof state:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
u : R
hu : IsUnit u
⊢ mulShift 1 u = 1

Tactic:
ext1 y

Result:
case refine_2.h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
u : R
hu : IsUnit u
y : R
⊢ (mulShift 1 u) y = 1 y

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
y : R
⊢ y = u * (↑hu.unit⁻¹ * y)

Tactic:
rw [← mul_assoc, IsUnit.mul_val_inv, one_mul]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
⊢ ψ.mulShift u = 1 ↔ ψ = 1

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Result:
case refine_1
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
⊢ ψ = 1

case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
⊢ ψ = 1 → ψ.mulShift u = 1

Proof state:
case refine_1.h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
y : R
⊢ ψ (u * (↑hu.unit⁻¹ * y)) = 1 (u * (↑hu.unit⁻¹ * y))

Tactic:
simpa only [mulShift_apply] using DFunLike.ext_iff.mp h (hu.unit⁻¹ * y)

Result:
no goals

Proof state:
case refine_2.h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
u : R
hu : IsUnit u
y : R
⊢ (mulShift 1 u) y = 1 y

Tactic:
rw [mulShift_apply, one_apply, one_apply]

Result:
no goals

Proof state:
case refine_1.h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
y : R
⊢ ψ y = 1 y

Tactic:
rw [show y = u * (hu.unit⁻¹ * y) by rw [← mul_assoc, IsUnit.mul_val_inv, one_mul]]

Result:
case refine_1.h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
y : R
⊢ ψ (u * (↑hu.unit⁻¹ * y)) = 1 (u * (↑hu.unit⁻¹ * y))

Proof state:
case refine_1
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
⊢ ψ = 1

Tactic:
ext1 y

Result:
case refine_1.h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
y : R
⊢ ψ y = 1 y

Proof state:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
⊢ ψ = 1 → ψ.mulShift u = 1

Tactic:
rintro rfl

Result:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
u : R
hu : IsUnit u
⊢ mulShift 1 u = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_mkVector (a : α) (n i : Nat) : (mkVector n a)[i]? = if i < n then some a else none

Proof state:
α : Type u_1
a : α
n i : Nat
⊢ (mkVector n a)[i]? = if i < n then some a else none

Tactic:
simp [getElem?_def]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
/-- To show a property of all powers of `g` it suffices to show it is closed under multiplication
by `g` and `g⁻¹` on the left. For subgroups generated by more than one element, see
`Subgroup.closure_induction_left`. -/
@[to_additive "To show a property of all multiples of `g` it suffices to show it is closed under
addition by `g` and `-g` on the left. For additive subgroups generated by more than one element, see
`AddSubgroup.closure_induction_left`."]
lemma zpow_induction_left {g : G} {P : G → Prop} (h_one : P (1 : G))
    (h_mul : ∀ a, P a → P (g * a)) (h_inv : ∀ a, P a → P (g⁻¹ * a)) (n : ℤ) : P (g ^ n)

Proof state:
case hn
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n - 1))

Tactic:
rw [Int.sub_eq_add_neg, Int.add_comm, zpow_add, zpow_neg_one]

Result:
case hn
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g⁻¹ * g ^ (-↑n))

Proof state:
case hp
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ ↑n)
⊢ P (g * g ^ ↑n)

Tactic:
exact h_mul _ ih

Result:
no goals

Proof state:
case hz
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
⊢ P (g ^ 0)

Tactic:
rwa [zpow_zero]

Result:
no goals

Proof state:
case hp
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ ↑n)
⊢ P (g ^ (↑n + 1))

Tactic:
rw [Int.add_comm, zpow_add, zpow_one]

Result:
case hp
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ ↑n)
⊢ P (g * g ^ ↑n)

Proof state:
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℤ
⊢ P (g ^ n)

Tactic:
induction n with
| hz => rwa [zpow_zero]
| hp n ih =>
  rw [Int.add_comm, zpow_add, zpow_one]
  exact h_mul _ ih
| hn n ih =>
  rw [Int.sub_eq_add_neg, Int.add_comm, zpow_add, zpow_neg_one]
  exact h_inv _ ih

Result:
no goals

Proof state:
case hn
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g⁻¹ * g ^ (-↑n))

Tactic:
exact h_inv _ ih

Result:
no goals
-- Mathlib/Order/UpperLower/LocallyFinite.lean
theorem Finite.lowerClosure [LocallyFiniteOrderBot α] (hs : s.Finite) :
    (lowerClosure s : Set α).Finite

Proof state:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderBot α
hs : s.Finite
⊢ (⋃ a ∈ s, Iic a).Finite

Tactic:
exact hs.biUnion fun _ _ => finite_Iic _

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderBot α
hs : s.Finite
⊢ (↑(lowerClosure s)).Finite

Tactic:
rw [coe_lowerClosure]

Result:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderBot α
hs : s.Finite
⊢ (⋃ a ∈ s, Iic a).Finite
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_insert_right (h : a ≤ b) : insert b (Ico a b) = Icc a b

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert b (Ico a b) = Icc a b

Tactic:
rw [← coe_inj, coe_insert, coe_Icc, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ico_union_right h]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_mul_of_coprime_of_dvd {a b c : ℕ} (hac : Coprime a c) (b_dvd_c : b ∣ c) :
    gcd (a * b) c = b

Proof state:
case intro
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ (a * b).gcd (d * b) = b

Tactic:
rw [gcd_mul_right]

Result:
case intro
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ a.gcd d * b = b

Proof state:
a b c : ℕ
hac : a.Coprime c
b_dvd_c : b ∣ c
⊢ (a * b).gcd c = b

Tactic:
rcases exists_eq_mul_left_of_dvd b_dvd_c with ⟨d, rfl⟩

Result:
case intro
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ (a * b).gcd (d * b) = b

Proof state:
case intro
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ a.gcd d * b = b

Tactic:
convert one_mul b

Result:
case h.e'_2.h.e'_5
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ a.gcd d = 1

Proof state:
case h.e'_2.h.e'_5
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ a.gcd d = 1

Tactic:
exact Coprime.coprime_mul_right_right hac

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem coe_ndinter (l₁ l₂ : List α) : @ndinter α _ l₁ l₂ = (l₁ ∩ l₂ : List α)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ List.filter (fun b => elem b l₂) l₁ ~ l₁ ∩ l₂

Tactic:
apply Perm.refl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (↑l₁).ndinter ↑l₂ = ↑(l₁ ∩ l₂)

Tactic:
simp only [ndinter, mem_coe, filter_coe, coe_eq_coe, ← elem_eq_mem]

Result:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ List.filter (fun b => elem b l₂) l₁ ~ l₁ ∩ l₂
-- Mathlib/CategoryTheory/Localization/Resolution.lean
lemma isIso_iff_of_hasLeftResolutions [Φ.HasLeftResolutions] {F G : D₂ ⥤ H} (α : F ⟶ G) :
    IsIso α ↔ ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))

Proof state:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ (∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))) → IsIso α

Tactic:
intro hα

Result:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
⊢ IsIso α
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/DecidableEq.lean
theorem isEqv_self_beq [BEq α] [ReflBEq α] (a : Vector α n) : Vector.isEqv a a (· == ·) = true

Proof state:
α : Type u_1
n : Nat
inst✝¹ : BEq α
inst✝ : ReflBEq α
a : Vector α n
⊢ (a.isEqv a fun x1 x2 => x1 == x2) = true

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : ReflBEq α
a : Array α
⊢ ({ toArray := a, size_toArray := ⋯ }.isEqv { toArray := a, size_toArray := ⋯ } fun x1 x2 => x1 == x2) = true

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : ReflBEq α
a : Array α
⊢ ({ toArray := a, size_toArray := ⋯ }.isEqv { toArray := a, size_toArray := ⋯ } fun x1 x2 => x1 == x2) = true

Tactic:
simp [Array.isEqv_self_beq]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_add_toIocMod_zero (a b : α) :
    toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - a) = p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - a) = p

Tactic:
rw [toIcoMod_zero_sub_comm, sub_add_cancel]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem mapDomain_apply {f : α → β} (hf : Function.Injective f) (x : α →₀ M) (a : α) :
    mapDomain f x (f a) = x a

Proof state:
case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a b : α
a✝ : x b ≠ 0
hba : b ≠ a
⊢ (single (f b) (x b)) (f a) = 0

Tactic:
exact single_eq_of_ne (hf.ne hba)

Result:
no goals

Proof state:
case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ x a = 0 → (single (f a) 0) (f a) = 0

Tactic:
intro _

Result:
case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
a✝ : x a = 0
⊢ (single (f a) 0) (f a) = 0

Proof state:
case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ ∀ (b : α), x b ≠ 0 → b ≠ a → (single (f b) (x b)) (f a) = 0

Tactic:
intro b _ hba

Result:
case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a b : α
a✝ : x b ≠ 0
hba : b ≠ a
⊢ (single (f b) (x b)) (f a) = 0

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ (mapDomain f x) (f a) = x a

Tactic:
rw [mapDomain, sum_apply, sum_eq_single a, single_eq_same]

Result:
case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ ∀ (b : α), x b ≠ 0 → b ≠ a → (single (f b) (x b)) (f a) = 0

case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ x a = 0 → (single (f a) 0) (f a) = 0

Proof state:
case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
a✝ : x a = 0
⊢ (single (f a) 0) (f a) = 0

Tactic:
rw [single_zero, coe_zero, Pi.zero_apply]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem Finite.eq_insert_of_subset_of_encard_eq_succ (hs : s.Finite) (h : s ⊆ t)
    (hst : t.encard = s.encard + 1) : ∃ a, t = insert a s

Proof state:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
hst : ∃ x, t \ s = {x}
⊢ ∃ a, t = insert a s

Tactic:
obtain ⟨x, hx⟩ := hst

Result:
case intro
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ ∃ a, t = insert a s

Proof state:
case h
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ t = insert x s

Tactic:
rw [← diff_union_of_subset h, hx, singleton_union]

Result:
no goals

Proof state:
case intro
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ ∃ a, t = insert a s

Tactic:
use x

Result:
case h
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ t = insert x s

Proof state:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
hst : t.encard = s.encard + 1
⊢ ∃ a, t = insert a s

Tactic:
rw [← encard_diff_add_encard_of_subset h, add_comm, WithTop.add_left_inj hs.encard_lt_top.ne,
  encard_eq_one] at hst

Result:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
hst : ∃ x, t \ s = {x}
⊢ ∃ a, t = insert a s
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem isUnit_ring_inverse {a : M₀} : IsUnit (Ring.inverse a) ↔ IsUnit a :=
  ⟨fun h => by
    cases subsingleton_or_nontrivial M₀
    · convert h
    · contrapose h
      rw [Ring.inverse_non_unit _ h]
      exact not_isUnit_zero
      ,
    IsUnit.ring_inverse⟩

Proof state:
case inl
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit (Ring.inverse a)
h✝ : Subsingleton M₀
⊢ IsUnit a

Tactic:
convert h

Result:
no goals

Proof state:
case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit (Ring.inverse a)

Tactic:
rw [Ring.inverse_non_unit _ h]

Result:
case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit 0

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit (Ring.inverse a)
⊢ IsUnit a

Tactic:
cases subsingleton_or_nontrivial M₀

Result:
case inl
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit (Ring.inverse a)
h✝ : Subsingleton M₀
⊢ IsUnit a

case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit (Ring.inverse a)
h✝ : Nontrivial M₀
⊢ IsUnit a

Proof state:
case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit (Ring.inverse a)
h✝ : Nontrivial M₀
⊢ IsUnit a

Tactic:
contrapose h

Result:
case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit (Ring.inverse a)

Proof state:
case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit 0

Tactic:
exact not_isUnit_zero

Result:
no goals
-- Mathlib/Logic/Unique.lean
theorem heq_const_of_unique [Unique α] {β : α → Sort v} (f : ∀ a, β a) :
    HEq f (Function.const α (f default)) :=
  (Function.hfunext rfl) fun i _ _ ↦ by rw [Subsingleton.elim i default]; rfl

Proof state:
α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : HEq i x✝¹
⊢ HEq (f default) (Function.const α (f default) x✝¹)

Tactic:
rfl

Result:
no goals

Proof state:
α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : HEq i x✝¹
⊢ HEq (f i) (Function.const α (f default) x✝¹)

Tactic:
rw [Subsingleton.elim i default]

Result:
α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : HEq i x✝¹
⊢ HEq (f default) (Function.const α (f default) x✝¹)
-- Mathlib/NumberTheory/LSeries/ZMod.lean
/-- If `Φ` is a periodic function, then the L-series of `Φ` converges for `1 < re s`. -/
lemma LSeriesSummable_of_one_lt_re (Φ : ZMod N → ℂ) {s : ℂ} (hs : 1 < re s) :
    LSeriesSummable (Φ ·) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
c : ℝ := (Finset.image (norm ∘ Φ) Finset.univ).max' ⋯
n : ℕ
x✝ : n ≠ 0
⊢ ‖Φ ↑n‖ ∈ Finset.image (norm ∘ Φ) Finset.univ

Tactic:
exact mem_image_of_mem _ (mem_univ _)

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (fun x => Φ ↑x) s

Tactic:
let c := max' _ <| univ_nonempty.image (norm ∘ Φ)

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
c : ℝ := (Finset.image (norm ∘ Φ) Finset.univ).max' ⋯
⊢ LSeriesSummable (fun x => Φ ↑x) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
c : ℝ := (Finset.image (norm ∘ Φ) Finset.univ).max' ⋯
⊢ LSeriesSummable (fun x => Φ ↑x) s

Tactic:
refine LSeriesSummable_of_bounded_of_one_lt_re (fun n _ ↦ le_max' _ _ ?_) (m := c) hs

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
c : ℝ := (Finset.image (norm ∘ Φ) Finset.univ).max' ⋯
n : ℕ
x✝ : n ≠ 0
⊢ ‖Φ ↑n‖ ∈ Finset.image (norm ∘ Φ) Finset.univ