harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attachWith_map_coe {p : α → Prop} (f : α → β) (l : Vector α n) (H : ∀ a ∈ l, p a) :
    ((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f

Proof state:
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : α → β
l : Vector α n
H : ∀ (a : α), a ∈ l → p a
⊢ map (fun i => f i.val) (l.attachWith p H) = map f l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ map (fun i => f i.val) ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith p H) =
    map f { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ map (fun i => f i.val) ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith p H) =
    map f { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Choose/Central.lean
theorem succ_dvd_centralBinom (n : ℕ) : n + 1 ∣ n.centralBinom

Proof state:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ n + 1 ∣ (2 * n + 1) * n.centralBinom

Tactic:
apply Nat.dvd_of_mul_dvd_mul_left zero_lt_two

Result:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ 2 * (n + 1) ∣ 2 * ((2 * n + 1) * n.centralBinom)

Proof state:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ 2 * (n + 1) ∣ 2 * ((2 * n + 1) * n.centralBinom)

Tactic:
rw [← mul_assoc, ← succ_mul_centralBinom_succ, mul_comm]

Result:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ (n + 1) * 2 ∣ (n + 1) * (n + 1).centralBinom

Proof state:
n : ℕ
⊢ Coprime 1 n

Tactic:
exact coprime_one_left n

Result:
no goals

Proof state:
n : ℕ
⊢ (n + 1).Coprime (2 * n + 1)

Tactic:
rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]

Result:
n : ℕ
⊢ Coprime 1 n

Proof state:
n : ℕ
⊢ n + 1 ∣ n.centralBinom

Tactic:
have h_s : (n + 1).Coprime (2 * n + 1) := by
  rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]
  exact coprime_one_left n

Result:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ n + 1 ∣ n.centralBinom

Proof state:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ (n + 1) * 2 ∣ (n + 1) * (n + 1).centralBinom

Tactic:
exact mul_dvd_mul_left _ (two_dvd_centralBinom_succ n)

Result:
no goals

Proof state:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ n + 1 ∣ n.centralBinom

Tactic:
apply h_s.dvd_of_dvd_mul_left

Result:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ n + 1 ∣ (2 * n + 1) * n.centralBinom
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma predAbove_last_of_ne_last {i : Fin (n + 2)} (hi : i ≠ last (n + 1)) :
    predAbove (last n) i = castPred i hi

Proof state:
case intro
n : ℕ
y : Fin (n + 1)
hi : y.castSucc ≠ last (n + 1)
⊢ (last n).predAbove y.castSucc = y.castSucc.castPred hi

Tactic:
exact predAbove_last_castSucc

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 2)
hi : i ≠ last (n + 1)
⊢ (last n).predAbove i = i.castPred hi

Tactic:
rw [← exists_castSucc_eq] at hi

Result:
n : ℕ
i : Fin (n + 2)
hi✝ : i ≠ last (n + 1)
hi : ∃ j, j.castSucc = i
⊢ (last n).predAbove i = i.castPred hi✝

Proof state:
n : ℕ
i : Fin (n + 2)
hi✝ : i ≠ last (n + 1)
hi : ∃ j, j.castSucc = i
⊢ (last n).predAbove i = i.castPred hi✝

Tactic:
rcases hi with ⟨y, rfl⟩

Result:
case intro
n : ℕ
y : Fin (n + 1)
hi : y.castSucc ≠ last (n + 1)
⊢ (last n).predAbove y.castSucc = y.castSucc.castPred hi
-- Mathlib/FieldTheory/SplittingField/Construction.lean
theorem X_sub_C_mul_removeFactor (f : K[X]) (hf : f.natDegree ≠ 0) :
    (X - C (AdjoinRoot.root f.factor)) * f.removeFactor = map (AdjoinRoot.of f.factor) f

Proof state:
K : Type v
inst✝ : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
⊢ (X - C (AdjoinRoot.root f.factor)) * f.removeFactor = map (AdjoinRoot.of f.factor) f

Tactic:
apply (mul_divByMonic_eq_iff_isRoot
  (R := AdjoinRoot f.factor) (a := AdjoinRoot.root f.factor)).mpr

Result:
K : Type v
inst✝ : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
⊢ (map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)

Proof state:
K : Type v
inst✝ : Field K
f : K[X]
hf : f.natDegree ≠ 0
⊢ (X - C (AdjoinRoot.root f.factor)) * f.removeFactor = map (AdjoinRoot.of f.factor) f

Tactic:
let ⟨g, hg⟩ := factor_dvd_of_natDegree_ne_zero hf

Result:
K : Type v
inst✝ : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
⊢ (X - C (AdjoinRoot.root f.factor)) * f.removeFactor = map (AdjoinRoot.of f.factor) f

Proof state:
K : Type v
inst✝ : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
⊢ (map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)

Tactic:
rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem descFactorial_mul_descFactorial {k m n : ℕ} (hkm : k ≤ m) :
    (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Proof state:
case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : ¬k ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0

Tactic:
rw [descFactorial_eq_zero_iff_lt.mpr (show n < k by omega), Nat.mul_zero]

Result:
no goals

Proof state:
case pos
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : k ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0

Tactic:
rw [descFactorial_eq_zero_iff_lt.mpr (show n - k < m - k by omega), Nat.zero_mul]

Result:
no goals

Proof state:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ n < m

Tactic:
omega

Result:
no goals

Proof state:
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ n - m = n - k - (m - k)

Tactic:
omega

Result:
no goals

Proof state:
k m n : ℕ
hkm : k ≤ m
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Tactic:
by_cases hmn : m ≤ n

Result:
case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Proof state:
case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Tactic:
apply Nat.mul_left_cancel (n - m).factorial_pos

Result:
case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = (n - m)! * n.descFactorial m

Proof state:
case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0

Tactic:
by_cases hkn : k ≤ n

Result:
case pos
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : k ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0

case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : ¬k ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0

Proof state:
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ m - k ≤ n - k

Tactic:
omega

Result:
no goals

Proof state:
case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Tactic:
rw [descFactorial_eq_zero_iff_lt.mpr (show n < m by omega)]

Result:
case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0

Proof state:
case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = (n - m)! * n.descFactorial m

Tactic:
rw [factorial_mul_descFactorial hmn, show n - m = (n - k) - (m - k) by omega, ← Nat.mul_assoc,
  factorial_mul_descFactorial (show m - k ≤ n - k by omega),
  factorial_mul_descFactorial (le_trans hkm hmn)]

Result:
no goals

Proof state:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : ¬k ≤ n
⊢ n < k

Tactic:
omega

Result:
no goals

Proof state:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : k ≤ n
⊢ n - k < m - k

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_filter {l : List α} (h : p a) : count a (filter p l) = count a l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
a : α
l : List α
h : p a = true
⊢ count a (filter p l) = count a l

Tactic:
rw [count, countP_filter]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
a : α
l : List α
h : p a = true
⊢ countP (fun a_1 => a_1 == a && p a_1) l = countP (fun x => x == a) l

Proof state:
case e_p.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
a : α
l : List α
h : p a = true
b : α
⊢ b = a → p b = true

Tactic:
rintro rfl

Result:
case e_p.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
l : List α
b : α
h : p b = true
⊢ p b = true

Proof state:
case e_p.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
l : List α
b : α
h : p b = true
⊢ p b = true

Tactic:
exact h

Result:
no goals

Proof state:
case e_p
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
a : α
l : List α
h : p a = true
⊢ (fun a_1 => a_1 == a && p a_1) = fun x => x == a

Tactic:
funext b

Result:
case e_p.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
a : α
l : List α
h : p a = true
b : α
⊢ (b == a && p b) = (b == a)

Proof state:
case e_p.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
a : α
l : List α
h : p a = true
b : α
⊢ (b == a && p b) = (b == a)

Tactic:
simp

Result:
case e_p.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
a : α
l : List α
h : p a = true
b : α
⊢ b = a → p b = true

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
a : α
l : List α
h : p a = true
⊢ countP (fun a_1 => a_1 == a && p a_1) l = countP (fun x => x == a) l

Tactic:
congr

Result:
case e_p
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
a : α
l : List α
h : p a = true
⊢ (fun a_1 => a_1 == a && p a_1) = fun x => x == a
-- Mathlib/Analysis/Normed/Affine/Simplex.lean
lemma Regular.equilateral {s : Simplex R P n} (hr : s.Regular) : s.Equilateral

Proof state:
case pos
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
⊢ dist (s.points j) (s.points 1) = dist (s.points 0) (s.points 1)

Tactic:
rcases hr (Equiv.swap 0 j) with ⟨x, hx⟩

Result:
case pos.intro
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.swap 0 j) = ⇑x ∘ s.points
⊢ dist (s.points j) (s.points 1) = dist (s.points 0) (s.points 1)

Proof state:
case pos
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
⊢ dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)

Tactic:
rw [hi, dist_comm]

Result:
case pos
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
⊢ dist (s.points j) (s.points 1) = dist (s.points 0) (s.points 1)
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
@[simp] lemma prod_zero : μ.prod (0 : FiniteMeasure β) = 0

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
⊢ μ.prod 0 = 0

Tactic:
rw [← mass_zero_iff, mass_prod, zero_mass, mul_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem intervalIntegrable_rpow' {r : ℝ} (h : -1 < r) :
    IntervalIntegrable (fun x => x ^ r) volume a b

Proof state:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c)) volume
⊢ IntegrableOn (fun x => (-x) ^ r) (Ι 0 (-c)) volume

Tactic:
refine m.congr_fun ?_ measurableSet_Ioc

Result:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c)) volume
⊢ EqOn (cos (r * π) • fun x => x ^ r) (fun x => (-x) ^ r) (Ι 0 (-c))

Proof state:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c)) volume
⊢ EqOn (cos (r * π) • fun x => x ^ r) (fun x => (-x) ^ r) (Ι 0 (-c))

Tactic:
intro x hx

Result:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c)) volume
x : ℝ
hx : x ∈ Ι 0 (-c)
⊢ (cos (r * π) • fun x => x ^ r) x = (fun x => (-x) ^ r) x

Proof state:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
a✝ : x ∈ Set.Icc 0 c
⊢ id x ≠ 0 ∨ 0 ≤ r + 1

Tactic:
right

Result:
case h
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Set.Ioo 0 c, HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
a✝ : x ∈ Set.Icc 0 c
⊢ 0 ≤ r + 1

Proof state:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x => x ^ r) volume 0 c

Tactic:
intro c

Result:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c

Proof state:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x

Tactic:
convert (Real.hasDerivAt_rpow_const (p := r + 1) (Or.inl hx.1.ne')).div_const (r + 1) using 1

Result:
case h.e'_9
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ x ^ r = (r + 1) * x ^ (r + 1 - 1) / (r + 1)

Proof state:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), IntervalIntegrable (fun x => x ^ r) volume 0 c
⊢ IntervalIntegrable (fun x => x ^ r) volume a b

Tactic:
exact IntervalIntegrable.trans (this a).symm (this b)

Result:
no goals

Proof state:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c

Tactic:
rw [intervalIntegrable_iff, uIoc_of_le hc]

Result:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (fun x => x ^ r) (Set.Ioc 0 c) volume

Proof state:
case inl
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c

Tactic:
exact this c hc

Result:
no goals
-- Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean
theorem comp {f : X → Y} {g : Y → Z} (x : X) (hg : ConformalAt g (f x)) (hf : ConformalAt f x) :
    ConformalAt (g ∘ f) x

Proof state:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
f' : X →L[ℝ] Y
hf₁ : HasFDerivAt f f' x
cf : IsConformalMap f'
g' : Y →L[ℝ] Z
hg₁ : HasFDerivAt g g' (f x)
cg : IsConformalMap g'
⊢ ConformalAt (g ∘ f) x

Tactic:
exact ⟨g'.comp f', hg₁.comp x hf₁, cg.comp cf⟩

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
hg : ConformalAt g (f x)
f' : X →L[ℝ] Y
hf₁ : HasFDerivAt f f' x
cf : IsConformalMap f'
⊢ ConformalAt (g ∘ f) x

Tactic:
rcases hg with ⟨g', hg₁, cg⟩

Result:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
f' : X →L[ℝ] Y
hf₁ : HasFDerivAt f f' x
cf : IsConformalMap f'
g' : Y →L[ℝ] Z
hg₁ : HasFDerivAt g g' (f x)
cg : IsConformalMap g'
⊢ ConformalAt (g ∘ f) x

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
hg : ConformalAt g (f x)
hf : ConformalAt f x
⊢ ConformalAt (g ∘ f) x

Tactic:
rcases hf with ⟨f', hf₁, cf⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
hg : ConformalAt g (f x)
f' : X →L[ℝ] Y
hf₁ : HasFDerivAt f f' x
cf : IsConformalMap f'
⊢ ConformalAt (g ∘ f) x
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma summable_jacobiTheta₂_term_fderiv_iff (z τ : ℂ) :
    Summable (jacobiTheta₂_term_fderiv · z τ) ↔ 0 < im τ

Proof state:
case mp
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term_fderiv x z τ
this : Summable fun x => ‖jacobiTheta₂_term_fderiv x z τ‖
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ ‖jacobiTheta₂_term_fderiv i z τ‖

Tactic:
have : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0 :=
  Int.cofinite_eq ▸ (mem_sup.mpr ⟨eventually_ne_atBot 0, eventually_ne_atTop 0⟩)

Result:
case mp
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term_fderiv x z τ
this✝ : Summable fun x => ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ ‖jacobiTheta₂_term_fderiv i z τ‖

Proof state:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term_fderiv x z τ
this✝ : Summable fun x => ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ π * ↑|n| ^ 2

Tactic:
refine one_le_pi_div_two.trans (mul_le_mul_of_nonneg_left ?_ pi_pos.le)

Result:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term_fderiv x z τ
this✝ : Summable fun x => ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 2⁻¹ ≤ ↑|n| ^ 2
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem perm_ext_iff_of_nodup {l₁ l₂ : List α} (d₁ : Nodup l₁) (d₂ : Nodup l₂) :
    l₁ ~ l₂ ↔ ∀ a, a ∈ l₁ ↔ a ∈ l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
d₁ : l₁.Nodup
d₂ : l₂.Nodup
⊢ l₁ ~ l₂ ↔ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂

Tactic:
refine ⟨fun p _ => p.mem_iff, fun H => ?_⟩

Result:
α : Type u_1
l₁ l₂ : List α
d₁ : l₁.Nodup
d₂ : l₂.Nodup
H : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
⊢ l₁ ~ l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
d₁ : l₁.Nodup
d₂ : l₂.Nodup
H : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
⊢ l₁ ~ l₂

Tactic:
exact (subperm_of_subset d₁ fun a => (H a).1).antisymm <| subperm_of_subset d₂ fun a => (H a).2

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem zero_ascFactorial : ∀ (k : ℕ), (0 : ℕ).ascFactorial k.succ = 0
  | 0 => by
    rw [ascFactorial_succ, ascFactorial_zero, Nat.zero_add, Nat.zero_mul]
  | (k+1) => by
    rw [ascFactorial_succ, zero_ascFactorial k, Nat.mul_zero]

Proof state:
k : ℕ
⊢ ascFactorial 0 (k + 1).succ = 0

Tactic:
rw [ascFactorial_succ, zero_ascFactorial k, Nat.mul_zero]

Result:
no goals

Proof state:
⊢ ascFactorial 0 (succ 0) = 0

Tactic:
rw [ascFactorial_succ, ascFactorial_zero, Nat.zero_add, Nat.zero_mul]

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropAt_chart_symm [HasGroupoid M G] (hG : G.LocalInvariantProp G Q)
    (hQ : ∀ y, Q id univ y) : LiftPropAt Q (chartAt (H := H) x).symm ((chartAt H x) x) :=
  hG.liftPropAt_symm_of_mem_maximalAtlas hQ (chart_mem_maximalAtlas G x) (by simp)

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
x : M
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
⊢ ↑(chartAt H x) x ∈ (chartAt H x).target

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_eq_one [DecidableEq n] [Semiring α] [StarRing α] {M : Matrix n n α} :
    Mᴴ = 1 ↔ M = 1 :=
  (Function.Involutive.eq_iff conjTranspose_conjTranspose).trans <|
    by rw [conjTranspose_one]

Proof state:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Semiring α
inst✝ : StarRing α
M : Matrix n n α
⊢ M = 1ᴴ ↔ M = 1

Tactic:
rw [conjTranspose_one]

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma isIso_of_yoneda_map_bijective {X Y : C} (f : X ⟶ Y)
    (hf : ∀ (T : C), Function.Bijective (fun (x : T ⟶ X) => x ≫ f)) :
    IsIso f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x => x ≫ f
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
⊢ (fun x => x ≫ f) (f ≫ g) = (fun x => x ≫ f) (𝟙 X)

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x => x ≫ f
⊢ IsIso f

Tactic:
obtain ⟨g, hg : g ≫ f = 𝟙 Y⟩ := (hf Y).2 (𝟙 Y)

Result:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x => x ≫ f
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
⊢ IsIso f

Proof state:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x => x ≫ f
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
⊢ IsIso f

Tactic:
exact ⟨g, (hf _).1 (by aesop_cat), hg⟩

Result:
no goals
-- Mathlib/Computability/Reduce.lean
theorem le_trans {d₁ d₂ d₃ : ManyOneDegree} : d₁ ≤ d₂ → d₂ ≤ d₃ → d₁ ≤ d₃

Proof state:
case h
d₂ d₃ : ManyOneDegree
p✝ : Set ℕ
⊢ of p✝ ≤ d₂ → d₂ ≤ d₃ → of p✝ ≤ d₃

Tactic:
induction d₂ using ManyOneDegree.ind_on

Result:
case h.h
d₃ : ManyOneDegree
p✝¹ p✝ : Set ℕ
⊢ of p✝¹ ≤ of p✝ → of p✝ ≤ d₃ → of p✝¹ ≤ d₃

Proof state:
case h.h.h
p✝² p✝¹ p✝ : Set ℕ
⊢ of p✝² ≤ of p✝¹ → of p✝¹ ≤ of p✝ → of p✝² ≤ of p✝

Tactic:
apply ManyOneReducible.trans

Result:
no goals

Proof state:
case h.h
d₃ : ManyOneDegree
p✝¹ p✝ : Set ℕ
⊢ of p✝¹ ≤ of p✝ → of p✝ ≤ d₃ → of p✝¹ ≤ d₃

Tactic:
induction d₃ using ManyOneDegree.ind_on

Result:
case h.h.h
p✝² p✝¹ p✝ : Set ℕ
⊢ of p✝² ≤ of p✝¹ → of p✝¹ ≤ of p✝ → of p✝² ≤ of p✝

Proof state:
d₁ d₂ d₃ : ManyOneDegree
⊢ d₁ ≤ d₂ → d₂ ≤ d₃ → d₁ ≤ d₃

Tactic:
induction d₁ using ManyOneDegree.ind_on

Result:
case h
d₂ d₃ : ManyOneDegree
p✝ : Set ℕ
⊢ of p✝ ≤ d₂ → d₂ ≤ d₃ → of p✝ ≤ d₃