harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Analytic/Basic.lean
theorem ContinuousLinearMap.comp_hasFPowerSeriesOnBall (g : F →L[𝕜] G)
    (h : HasFPowerSeriesOnBall f p x r) :
    HasFPowerSeriesOnBall (g ∘ f) (g.compFormalMultilinearSeries p) x r

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
g : F →L[𝕜] G
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (⇑g ∘ f) (g.compFormalMultilinearSeries p) x r

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at h ⊢

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
g : F →L[𝕜] G
h : HasFPowerSeriesWithinOnBall f p univ x r
⊢ HasFPowerSeriesWithinOnBall (⇑g ∘ f) (g.compFormalMultilinearSeries p) univ x r

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
g : F →L[𝕜] G
h : HasFPowerSeriesWithinOnBall f p univ x r
⊢ HasFPowerSeriesWithinOnBall (⇑g ∘ f) (g.compFormalMultilinearSeries p) univ x r

Tactic:
exact g.comp_hasFPowerSeriesWithinOnBall h

Result:
no goals
-- Mathlib/CategoryTheory/Types.lean
theorem types_ext {α β : Type u} (f g : α ⟶ β) (h : ∀ a : α, f a = g a) : f = g

Proof state:
α β : Type u
f g : α ⟶ β
h : ∀ (a : α), f a = g a
⊢ f = g

Tactic:
funext x

Result:
case h
α β : Type u
f g : α ⟶ β
h : ∀ (a : α), f a = g a
x : α
⊢ f x = g x

Proof state:
case h
α β : Type u
f g : α ⟶ β
h : ∀ (a : α), f a = g a
x : α
⊢ f x = g x

Tactic:
exact h x

Result:
no goals
-- Mathlib/Data/Nat/Pairing.lean
theorem unpair_left_le : ∀ n : ℕ, (unpair n).1 ≤ n
  | 0 => by simp
  | _ + 1 => le_of_lt (unpair_lt (Nat.succ_pos _))

Proof state:
⊢ (unpair 0).1 ≤ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem pi_eq_empty_iff' : s.pi t = ∅ ↔ ∃ i ∈ s, t i = ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ s.pi t = ∅ ↔ ∃ i ∈ s, t i = ∅

Tactic:
simp [pi_eq_empty_iff]

Result:
no goals
-- Mathlib/Data/List/EditDistance/Defs.lean
theorem suffixLevenshtein_cons₁_aux {α} {x y : { l : List α // 0 < l.length }}
    (w₀ : x.1[0]'x.2 = y.1[0]'y.2) (w : x.1.tail = y.1.tail) : x = y

Proof state:
α : Type u_4
x y : { l // 0 < l.length }
hx : α
tx : List α
property✝¹ : 0 < (hx :: tx).length
hy : α
ty : List α
property✝ : 0 < (hy :: ty).length
w₀ : ⟨hx :: tx, property✝¹⟩.val[0] = ⟨hy :: ty, property✝⟩.val[0]
w : ⟨hx :: tx, property✝¹⟩.val.tail = ⟨hy :: ty, property✝⟩.val.tail
⊢ ⟨hx :: tx, property✝¹⟩ = ⟨hy :: ty, property✝⟩

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_4
x y : { l // 0 < l.length }
w₀ : x.val[0] = y.val[0]
w : x.val.tail = y.val.tail
⊢ x = y

Tactic:
match x, y with
| ⟨hx :: tx, _⟩, ⟨hy :: ty, _⟩ => simp_all

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem uIcc_comm (a b : α) : [[a, b]] = [[b, a]]

Proof state:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ [[a, b]] = [[b, a]]

Tactic:
rw [uIcc, uIcc, inf_comm, sup_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
@[simp]
lemma star_nonpos_iff {x : R} : star x ≤ 0 ↔ x ≤ 0

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
⊢ star x ≤ 0 ↔ x ≤ 0

Tactic:
simpa using star_le_star_iff (x := x) (y := 0)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_lt_pi_iff {z : ℂ} : arg z < π ↔ 0 ≤ z.re ∨ z.im ≠ 0

Proof state:
z : ℂ
⊢ z.arg < π ↔ 0 ≤ z.re ∨ z.im ≠ 0

Tactic:
rw [(arg_le_pi z).lt_iff_ne, not_iff_comm, not_or, not_le, Classical.not_not, arg_eq_pi_iff]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem mul_eq_one : a * b = 1 ↔ a = 1 ∧ b = 1 :=
  ⟨fun h => ⟨eq_one_of_mul_right h, eq_one_of_mul_left h⟩, by
    rintro ⟨rfl, rfl⟩
    exact mul_one _⟩

Proof state:
case intro
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
⊢ 1 * 1 = 1

Tactic:
exact mul_one _

Result:
no goals

Proof state:
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a = 1 ∧ b = 1 → a * b = 1

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case intro
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
⊢ 1 * 1 = 1
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem pow_sup_eq_top {n : ℕ} (h : I ⊔ J = ⊤) : I ^ n ⊔ J = ⊤

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n : ℕ
h : I ⊔ J = ⊤
⊢ (∏ _x ∈ Finset.range n, I) ⊔ J = ⊤

Tactic:
exact prod_sup_eq_top fun _ _ => h

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n : ℕ
h : I ⊔ J = ⊤
⊢ I ^ n ⊔ J = ⊤

Tactic:
rw [← Finset.card_range n, ← Finset.prod_const]

Result:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n : ℕ
h : I ⊔ J = ⊤
⊢ (∏ _x ∈ Finset.range n, I) ⊔ J = ⊤
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem hasGenEigenvalue_of_hasGenEigenvalue_of_le {f : End R M} {μ : R} {k : ℕ}
    {m : ℕ} (hm : k ≤ m) (hk : f.HasGenEigenvalue μ k) :
    f.HasGenEigenvalue μ m :=
  hk.le <| by simpa using hm

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ
hm : k ≤ m
hk : f.HasGenEigenvalue μ k
⊢ ↑k ≤ ↑m

Tactic:
simpa using hm

Result:
no goals
-- Mathlib/Data/Nat/Cast/NeZero.lean
lemma of_neZero_natCast (R) [AddMonoidWithOne R] {n : ℕ} [h : NeZero (n : R)] : NeZero n :=
  ⟨by rintro rfl; exact h.out Nat.cast_zero⟩

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
h : NeZero ↑0
⊢ False

Tactic:
exact h.out Nat.cast_zero

Result:
no goals

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
h : NeZero ↑n
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝ : AddMonoidWithOne R
h : NeZero ↑0
⊢ False
-- Mathlib/Algebra/Ring/Rat.lean
lemma num_div_den (r : ℚ) : (r.num : ℚ) / (r.den : ℚ) = r

Proof state:
r : ℚ
⊢ ↑r.num / ↑r.den = r

Tactic:
rw [← Int.cast_natCast, ← divInt_eq_div, num_divInt_den]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Equiv.lean
@[simp]
lemma codRestrict₂_apply (x : M₁) (y : M₂) :
    i (codRestrict₂ f i hi hf x y) = f x y

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ range i
x : M₁
y : M₂
⊢ i (((f.codRestrict₂ i hi hf) x) y) = (f x) y

Tactic:
simp [codRestrict₂]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem sphere_zero_subset : sphere n d 0 ⊆ 0 := fun x => by simp [sphere, funext_iff]

Proof state:
n d : ℕ
x : Fin n → ℕ
⊢ x ∈ sphere n d 0 → x ∈ 0

Tactic:
simp [sphere, funext_iff]

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem apply_of_row_ne {i i' : m} (hi : i ≠ i') (j j' : n) (a : α) :
    stdBasisMatrix i j a i' j' = 0

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i i' : m
hi : i ≠ i'
j j' : n
a : α
⊢ stdBasisMatrix i j a i' j' = 0

Tactic:
simp [hi]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/FunctorToTypes.lean
@[ext]
lemma prod_ext' (a : C) (z w : (F ⨯ G).obj a)
    (h1 : (Limits.prod.fst (X := F)).app a z = (Limits.prod.fst (X := F)).app a w)
    (h2 : (Limits.prod.snd (X := F)).app a z = (Limits.prod.snd (X := F)).app a w) :
    z = w

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
z w : (F ⨯ G).obj a
h1 : Limits.prod.fst.app a z = Limits.prod.fst.app a w
h2 : Limits.prod.snd.app a z = Limits.prod.snd.app a w
⊢ z = w

Tactic:
apply Equiv.injective (binaryProductEquiv F G a)

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
z w : (F ⨯ G).obj a
h1 : Limits.prod.fst.app a z = Limits.prod.fst.app a w
h2 : Limits.prod.snd.app a z = Limits.prod.snd.app a w
⊢ (binaryProductEquiv F G a) z = (binaryProductEquiv F G a) w

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
z w : (F ⨯ G).obj a
h1 : Limits.prod.fst.app a z = Limits.prod.fst.app a w
h2 : Limits.prod.snd.app a z = Limits.prod.snd.app a w
⊢ (binaryProductEquiv F G a) z = (binaryProductEquiv F G a) w

Tactic:
aesop

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_toLin (b : Basis ι R M) (f : Matrix ι ι R) :
    LinearMap.det (Matrix.toLin b b f) = f.det

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Matrix ι ι R
⊢ LinearMap.det ((toLin b b) f) = f.det

Tactic:
rw [← LinearMap.det_toMatrix b, LinearMap.toMatrix_toLin]

Result:
no goals
-- Mathlib/Data/Fintype/Lattice.lean
lemma mem_inf [DecidableEq α] {s : Finset ι} {f : ι → Finset α} {a : α} :
    a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
⊢ a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i

Tactic:
induction' s using Finset.cons_induction <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem comp_ite {P : Prop} [Decidable P] {X Y Z : C} (f : X ⟶ Y) (g g' : Y ⟶ Z) :
    (f ≫ if P then g else g') = if P then f ≫ g else f ≫ g'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ (f ≫ if P then g else g') = if P then f ≫ g else f ≫ g'

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_false_of_le_false : ∀ {x : Bool}, x ≤ false → x = false

Proof state:
⊢ ∀ {x : Bool}, x ≤ false → x = false

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWith_map {μ} (f : γ → δ → μ) (g : α → γ) (h : β → δ) (l₁ : Array α) (l₂ : Array β) :
    zipWith f (l₁.map g) (l₂.map h) = zipWith (fun a b => f (g a) (h b)) l₁ l₂

Proof state:
case mk
γ : Type u_1
δ : Type u_2
α : Type u_3
β : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h : β → δ
l₂ : Array β
toList✝ : List α
⊢ zipWith f (map g { toList := toList✝ }) (map h l₂) = zipWith (fun a b => f (g a) (h b)) { toList := toList✝ } l₂

Tactic:
cases l₂

Result:
case mk.mk
γ : Type u_1
δ : Type u_2
α : Type u_3
β : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h : β → δ
toList✝¹ : List α
toList✝ : List β
⊢ zipWith f (map g { toList := toList✝¹ }) (map h { toList := toList✝ }) =
    zipWith (fun a b => f (g a) (h b)) { toList := toList✝¹ } { toList := toList✝ }

Proof state:
γ : Type u_1
δ : Type u_2
α : Type u_3
β : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h : β → δ
l₁ : Array α
l₂ : Array β
⊢ zipWith f (map g l₁) (map h l₂) = zipWith (fun a b => f (g a) (h b)) l₁ l₂

Tactic:
cases l₁

Result:
case mk
γ : Type u_1
δ : Type u_2
α : Type u_3
β : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h : β → δ
l₂ : Array β
toList✝ : List α
⊢ zipWith f (map g { toList := toList✝ }) (map h l₂) = zipWith (fun a b => f (g a) (h b)) { toList := toList✝ } l₂

Proof state:
case mk.mk
γ : Type u_1
δ : Type u_2
α : Type u_3
β : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h : β → δ
toList✝¹ : List α
toList✝ : List β
⊢ zipWith f (map g { toList := toList✝¹ }) (map h { toList := toList✝ }) =
    zipWith (fun a b => f (g a) (h b)) { toList := toList✝¹ } { toList := toList✝ }

Tactic:
simp [List.zipWith_map]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem lcm_one_right (i : ℤ) : lcm i 1 = natAbs i

Proof state:
i : ℤ
⊢ i.lcm 1 = i.natAbs

Tactic:
rw [Int.lcm]

Result:
i : ℤ
⊢ i.natAbs.lcm (natAbs 1) = i.natAbs

Proof state:
i : ℤ
⊢ i.natAbs.lcm (natAbs 1) = i.natAbs

Tactic:
apply Nat.lcm_one_right

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem evalWhiskerRight_comp
    {f f' : a ⟶ b} {g : b ⟶ c} {h : c ⟶ d}
    {η : f ⟶ f'} {η₁ : f ≫ g ⟶ f' ≫ g} {η₂ : (f ≫ g) ≫ h ⟶ (f' ≫ g) ≫ h}
    {η₃ : (f ≫ g) ≫ h ⟶ f' ≫ (g ≫ h)} {η₄ : f ≫ (g ≫ h) ⟶ f' ≫ (g ≫ h)}
    (e_η₁ : η ▷ g = η₁) (e_η₂ : η₁ ▷ h = η₂)
    (e_η₃ : η₂ ≫ (α_ _ _ _).hom = η₃) (e_η₄ : (α_ _ _ _).inv ≫ η₃ = η₄) :
    η ▷ (g ≫ h) = η₄

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
f f' : a ⟶ b
g : b ⟶ c
h : c ⟶ d
η : f ⟶ f'
η₁ : f ≫ g ⟶ f' ≫ g
η₂ : (f ≫ g) ≫ h ⟶ (f' ≫ g) ≫ h
η₃ : (f ≫ g) ≫ h ⟶ f' ≫ g ≫ h
η₄ : f ≫ g ≫ h ⟶ f' ≫ g ≫ h
e_η₁ : η ▷ g = η₁
e_η₂ : η₁ ▷ h = η₂
e_η₃ : η₂ ≫ (α_ f' g h).hom = η₃
e_η₄ : (α_ f g h).inv ≫ η₃ = η₄
⊢ η ▷ (g ≫ h) = η₄

Tactic:
simp [e_η₁, e_η₂, e_η₃, e_η₄]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem msymm_zero : msymm σ R (.indiscrete 0) = 1

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ msymm σ R (Nat.Partition.indiscrete 0) = 1

Tactic:
rw [msymm, Fintype.sum_subsingleton _ ⟨(Sym.nil : Sym σ 0), rfl⟩]

Result:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ (Multiset.map X ↑↑⟨Sym.nil, ⋯⟩).prod = 1

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ (Multiset.map X ↑↑⟨Sym.nil, ⋯⟩).prod = 1

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValExtension.lean
theorem val_map_le_one_iff (x : R) : vA (algebraMap R A x) ≤ 1 ↔ vR x ≤ 1

Proof state:
R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : LinearOrderedCommMonoidWithZero ΓR
inst✝² : LinearOrderedCommMonoidWithZero ΓA
inst✝¹ : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : IsValExtension vR vA
x : R
⊢ vA ((algebraMap R A) x) ≤ 1 ↔ vR x ≤ 1

Tactic:
simpa only [_root_.map_one] using val_map_le_iff vR vA x 1

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
theorem cast_intCast (n : ℤ) : ((n : ℚ) : α) = n :=
  (cast_def _).trans <| show (n / (1 : ℕ) : α) = n by rw [Nat.cast_one, div_one]

Proof state:
α : Type u_3
inst✝ : DivisionRing α
n : ℤ
⊢ ↑n / ↑1 = ↑n

Tactic:
rw [Nat.cast_one, div_one]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem dist_le_of_fixedPoint (x) {y} (hy : IsFixedPt f y) : dist x y ≤ dist x (f x) / (1 - K)

Proof state:
α : Type u_1
inst✝ : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hy : IsFixedPt f y
⊢ dist x y ≤ dist x (f x) / (1 - ↑K)

Tactic:
simpa only [hy.eq, dist_self, add_zero] using hf.dist_inequality x y

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
theorem freeGroupoidFunctor_comp (φ : V ⥤q V') (φ' : V' ⥤q V'') :
    freeGroupoidFunctor (φ ⋙q φ') = freeGroupoidFunctor φ ⋙ freeGroupoidFunctor φ'

Proof state:
case hΦ
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ of V ⋙q (lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')).toPrefunctor = φ ⋙q φ' ⋙q of V''

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ lift (φ ⋙q φ' ⋙q of V'') = lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')

Tactic:
symm

Result:
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'') = lift (φ ⋙q φ' ⋙q of V'')

Proof state:
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ freeGroupoidFunctor (φ ⋙q φ') = freeGroupoidFunctor φ ⋙ freeGroupoidFunctor φ'

Tactic:
dsimp only [freeGroupoidFunctor]

Result:
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ lift (φ ⋙q φ' ⋙q of V'') = lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')

Proof state:
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'') = lift (φ ⋙q φ' ⋙q of V'')

Tactic:
apply lift_unique

Result:
case hΦ
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ of V ⋙q (lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')).toPrefunctor = φ ⋙q φ' ⋙q of V''
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem sinh_half_dist (z w : ℍ) :
    sinh (dist z w / 2) = dist (z : ℂ) w / (2 * √(z.im * w.im))

Proof state:
z w : ℍ
⊢ sinh (dist z w / 2) = dist ↑z ↑w / (2 * √(z.im * w.im))

Tactic:
rw [dist_eq, mul_div_cancel_left₀ (arsinh _) two_ne_zero, sinh_arsinh]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem m_pos [Nonempty α] (hPα : #P.parts * 16 ^ #P.parts ≤ card α) : 0 < m

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ 0 < m

Tactic:
sz_positivity

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
@[simp]
lemma eulerChar_prod [BoundedOrder α] [BoundedOrder β] :
    eulerChar 𝕜 (α × β) = eulerChar 𝕜 α * eulerChar 𝕜 β

Proof state:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝¹⁰ : Ring 𝕜
inst✝⁹ : PartialOrder α
inst✝⁸ : PartialOrder β
inst✝⁷ : LocallyFiniteOrder α
inst✝⁶ : LocallyFiniteOrder β
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq β
inst✝³ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
⊢ eulerChar 𝕜 (α × β) = eulerChar 𝕜 α * eulerChar 𝕜 β

Tactic:
simp [eulerChar, ← mu_prod_mu]

Result:
no goals
-- Mathlib/Order/Sublattice.lean
@[simp, norm_cast] lemma coe_iInf (f : ι → Sublattice α) : ⨅ i, f i = ⋂ i, (f i : Set α)

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : Lattice α
f : ι → Sublattice α
⊢ ↑(⨅ i, f i) = ⋂ i, ↑(f i)

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJNe0Or1728_j (j : R) [Fact (IsUnit j)] [Fact (IsUnit (j - 1728))] :
    (ofJNe0Or1728 j).j = j

Proof state:
R : Type u_1
inst✝² : CommRing R
j : R
inst✝¹ : Fact (IsUnit j)
inst✝ : Fact (IsUnit (j - 1728))
⊢ (j * (j - 1728) ^ 3) ^ 3 = j ^ 2 * (j - 1728) ^ 9 * j

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
j : R
inst✝¹ : Fact (IsUnit j)
inst✝ : Fact (IsUnit (j - 1728))
⊢ (ofJNe0Or1728 j).j = j

Tactic:
rw [WeierstrassCurve.j, Units.inv_mul_eq_iff_eq_mul, ofJNe0Or1728_c₄, coe_Δ', ofJNe0Or1728_Δ]

Result:
R : Type u_1
inst✝² : CommRing R
j : R
inst✝¹ : Fact (IsUnit j)
inst✝ : Fact (IsUnit (j - 1728))
⊢ (j * (j - 1728) ^ 3) ^ 3 = j ^ 2 * (j - 1728) ^ 9 * j
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ioi_sub_one_eq_Ici_of_not_isMin (ha : ¬ IsMin a) : Ioi (a - 1) = Ici a

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
⊢ Ioi (a - 1) = Ici a

Tactic:
simpa [pred_eq_sub_one] using Ioi_pred_eq_Ici_of_not_isMin ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
    o₁.attach = o₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩)

Proof state:
α : Type u_1
o₁ o₂ : Option α
h : o₁ = o₂
⊢ o₁.attach = Option.map (fun x => ⟨x.val, ⋯⟩) o₂.attach

Tactic:
subst h

Result:
α : Type u_1
o₁ : Option α
⊢ o₁.attach = Option.map (fun x => ⟨x.val, ⋯⟩) o₁.attach

Proof state:
α : Type u_1
o₁ : Option α
⊢ o₁.attach = Option.map (fun x => ⟨x.val, ⋯⟩) o₁.attach

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblXYZ_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3) :
    W.dblXYZ P = W.dblZ P •
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ W.dblXYZ P =
    W.dblZ P •
      ![(toAffine W).addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        (toAffine W).addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]

Tactic:
have hZ {n : ℕ} : IsUnit <| W.dblZ P ^ n := (isUnit_dblZ_of_Y_ne' hP hQ hPz hx hy).pow n

Result:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
hZ : ∀ {n : ℕ}, IsUnit (W.dblZ P ^ n)
⊢ W.dblXYZ P =
    W.dblZ P •
      ![(toAffine W).addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        (toAffine W).addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
hZ : ∀ {n : ℕ}, IsUnit (W.dblZ P ^ n)
⊢ W.dblXYZ P =
    W.dblZ P •
      ![(toAffine W).addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        (toAffine W).addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]

Tactic:
erw [dblXYZ, smul_fin3, ← dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel,
  ← dblY_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel, mul_one]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_self_nonpos {x : E} : re ⟪x, x⟫ ≤ 0 ↔ x = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ re (inner x x) ≤ 0 ↔ x = 0

Tactic:
rw [← norm_sq_eq_inner, (sq_nonneg _).le_iff_eq, sq_eq_zero_iff, norm_eq_zero]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bsup_eq_blsub_iff_succ {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
    bsup.{_, v} o f = blsub.{_, v} o f ↔ ∀ a < blsub.{_, v} o f, succ a < blsub.{_, v} o f

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ sup (o.familyOfBFamily f) = lsub (o.familyOfBFamily f) ↔
    ∀ a < lsub (o.familyOfBFamily f), succ a < lsub (o.familyOfBFamily f)

Tactic:
apply sup_eq_lsub_iff_succ

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ o.bsup f = o.blsub f ↔ ∀ a < o.blsub f, succ a < o.blsub f

Tactic:
rw [← sup_eq_bsup, ← lsub_eq_blsub]

Result:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ sup (o.familyOfBFamily f) = lsub (o.familyOfBFamily f) ↔
    ∀ a < lsub (o.familyOfBFamily f), succ a < lsub (o.familyOfBFamily f)