harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Perfect.lean
theorem roots_expand_image_frobenius_subset [DecidableEq R] :
    (expand R p f).roots.toFinset.image (frobenius R p) ⊆ f.roots.toFinset

Proof state:
case h.e'_3.h.e'_5.h.e'_3.h.e'_4.h.e'_5.h.e'_3
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : DecidableEq R
⊢ p ^ 1 = p

Tactic:
apply pow_one

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : DecidableEq R
⊢ Finset.image (⇑(frobenius R p)) ((expand R p) f).roots.toFinset ⊆ f.roots.toFinset

Tactic:
rw [← iterateFrobenius_one]

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : DecidableEq R
⊢ Finset.image (⇑(iterateFrobenius R p 1)) ((expand R p) f).roots.toFinset ⊆ f.roots.toFinset

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : DecidableEq R
⊢ Finset.image (⇑(iterateFrobenius R p 1)) ((expand R p) f).roots.toFinset ⊆ f.roots.toFinset

Tactic:
convert ← roots_expand_pow_image_iterateFrobenius_subset p 1 f

Result:
case h.e'_3.h.e'_5.h.e'_3.h.e'_4.h.e'_5.h.e'_3
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : DecidableEq R
⊢ p ^ 1 = p
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem eq_comp_δ_of_not_surjective {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ mk (n + 1))
    (hθ : ¬Function.Surjective θ.toOrderHom) :
    ∃ (i : Fin (n + 2)) (θ' : Δ ⟶ mk n), θ = θ' ≫ δ i

Proof state:
case h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ : ¬Function.Surjective ⇑(Hom.toOrderHom θ)
i : Fin (⦋n + 1⦌.len + 1)
hi : ¬∃ a, (Hom.toOrderHom θ) a = i
⊢ ∃ θ', θ = θ' ≫ δ i

Tactic:
exact eq_comp_δ_of_not_surjective' θ i (not_exists.mp hi)

Result:
no goals

Proof state:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ : ¬Function.Surjective ⇑(Hom.toOrderHom θ)
⊢ ∃ i θ', θ = θ' ≫ δ i

Tactic:
obtain ⟨i, hi⟩ := not_forall.mp hθ

Result:
case intro
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ : ¬Function.Surjective ⇑(Hom.toOrderHom θ)
i : Fin (⦋n + 1⦌.len + 1)
hi : ¬∃ a, (Hom.toOrderHom θ) a = i
⊢ ∃ i θ', θ = θ' ≫ δ i

Proof state:
case intro
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ : ¬Function.Surjective ⇑(Hom.toOrderHom θ)
i : Fin (⦋n + 1⦌.len + 1)
hi : ¬∃ a, (Hom.toOrderHom θ) a = i
⊢ ∃ i θ', θ = θ' ≫ δ i

Tactic:
use i

Result:
case h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ : ¬Function.Surjective ⇑(Hom.toOrderHom θ)
i : Fin (⦋n + 1⦌.len + 1)
hi : ¬∃ a, (Hom.toOrderHom θ) a = i
⊢ ∃ θ', θ = θ' ≫ δ i
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem _root_.Polynomial.ker_mapRingHom (f : R →+* S) :
    RingHom.ker (Polynomial.mapRingHom f) = f.ker.map (C : R →+* R[X])

Proof state:
case h
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R[X]
⊢ x✝ ∈ RingHom.ker (mapRingHom f) ↔ x✝ ∈ map C (RingHom.ker f)

Tactic:
simp only [RingHom.mem_ker, coe_mapRingHom]

Result:
case h
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R[X]
⊢ Polynomial.map f x✝ = 0 ↔ x✝ ∈ map C (RingHom.ker f)

Proof state:
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
⊢ RingHom.ker (mapRingHom f) = map C (RingHom.ker f)

Tactic:
ext

Result:
case h
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R[X]
⊢ x✝ ∈ RingHom.ker (mapRingHom f) ↔ x✝ ∈ map C (RingHom.ker f)

Proof state:
case h
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R[X]
⊢ (∀ (n : ℕ), (Polynomial.map f x✝).coeff n = coeff 0 n) ↔ ∀ (n : ℕ), x✝.coeff n ∈ RingHom.ker f

Tactic:
simp [RingHom.mem_ker]

Result:
no goals

Proof state:
case h
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R[X]
⊢ Polynomial.map f x✝ = 0 ↔ x✝ ∈ map C (RingHom.ker f)

Tactic:
rw [mem_map_C_iff, Polynomial.ext_iff]

Result:
case h
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R[X]
⊢ (∀ (n : ℕ), (Polynomial.map f x✝).coeff n = coeff 0 n) ↔ ∀ (n : ℕ), x✝.coeff n ∈ RingHom.ker f
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem ZLattice.module_free [IsZLattice K L] : Module.Free ℤ L

Proof state:
K : Type u_1
inst✝⁸ : NormedLinearOrderedField K
inst✝⁷ : HasSolidNorm K
inst✝⁶ : FloorRing K
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
inst✝³ : FiniteDimensional K E
inst✝² : ProperSpace E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
⊢ Free ℤ ↥L

Tactic:
have : Module.Finite ℤ L := module_finite K L

Result:
K : Type u_1
inst✝⁸ : NormedLinearOrderedField K
inst✝⁷ : HasSolidNorm K
inst✝⁶ : FloorRing K
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
inst✝³ : FiniteDimensional K E
inst✝² : ProperSpace E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
this : Module.Finite ℤ ↥L
⊢ Free ℤ ↥L

Proof state:
K : Type u_1
inst✝⁸ : NormedLinearOrderedField K
inst✝⁷ : HasSolidNorm K
inst✝⁶ : FloorRing K
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
inst✝³ : FiniteDimensional K E
inst✝² : ProperSpace E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
this✝ : Module.Finite ℤ ↥L
this : Module ℚ E
⊢ Free ℤ ↥L

Tactic:
infer_instance

Result:
no goals

Proof state:
K : Type u_1
inst✝⁸ : NormedLinearOrderedField K
inst✝⁷ : HasSolidNorm K
inst✝⁶ : FloorRing K
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
inst✝³ : FiniteDimensional K E
inst✝² : ProperSpace E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
this : Module.Finite ℤ ↥L
⊢ Free ℤ ↥L

Tactic:
have : Module ℚ E := Module.compHom E (algebraMap ℚ K)

Result:
K : Type u_1
inst✝⁸ : NormedLinearOrderedField K
inst✝⁷ : HasSolidNorm K
inst✝⁶ : FloorRing K
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
inst✝³ : FiniteDimensional K E
inst✝² : ProperSpace E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
this✝ : Module.Finite ℤ ↥L
this : Module ℚ E
⊢ Free ℤ ↥L
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- The cosine zeta function is differentiable everywhere, except at `s = 1` if `a = 0`. -/
lemma differentiableAt_cosZeta (a : UnitAddCircle) {s : ℂ} (hs' : s ≠ 1 ∨ a ≠ 0) :
    DifferentiableAt ℂ (cosZeta a) s

Proof state:
case inr
a : UnitAddCircle
hs' : 1 ≠ 1 ∨ a ≠ 0
⊢ cosZeta a =ᶠ[𝓝 1] fun y => completedCosZeta a y * y.Gammaℝ⁻¹

Tactic:
filter_upwards [isOpen_compl_singleton.mem_nhds one_ne_zero] with x hx

Result:
case h
a : UnitAddCircle
hs' : 1 ≠ 1 ∨ a ≠ 0
x : ℂ
hx : x ∈ {0}ᶜ
⊢ cosZeta a x = completedCosZeta a x * x.Gammaℝ⁻¹

Proof state:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (cosZeta a) s

Tactic:
rcases ne_or_eq s 1 with hs' | rfl

Result:
case inl
a : UnitAddCircle
s : ℂ
hs'✝ : s ≠ 1 ∨ a ≠ 0
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (cosZeta a) s

case inr
a : UnitAddCircle
hs' : 1 ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (cosZeta a) 1

Proof state:
case h
a : UnitAddCircle
hs' : 1 ≠ 1 ∨ a ≠ 0
x : ℂ
hx : x ∈ {0}ᶜ
⊢ cosZeta a x = completedCosZeta a x * x.Gammaℝ⁻¹

Tactic:
rw [cosZeta, Function.update_of_ne hx, div_eq_mul_inv]

Result:
no goals

Proof state:
case inr
a : UnitAddCircle
hs' : 1 ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (cosZeta a) 1

Tactic:
apply ((differentiableAt_completedCosZeta a one_ne_zero hs').mul
  (differentiable_Gammaℝ_inv.differentiableAt)).congr_of_eventuallyEq

Result:
case inr
a : UnitAddCircle
hs' : 1 ≠ 1 ∨ a ≠ 0
⊢ cosZeta a =ᶠ[𝓝 1] fun y => completedCosZeta a y * y.Gammaℝ⁻¹

Proof state:
case inl
a : UnitAddCircle
s : ℂ
hs'✝ : s ≠ 1 ∨ a ≠ 0
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (cosZeta a) s

Tactic:
exact differentiableAt_update_of_residue (fun _ ht ht' ↦
  differentiableAt_completedCosZeta a ht (Or.inl ht')) (completedCosZeta_residue_zero a) s hs'

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem cast_mul (h : m ∣ n) (a b : ZMod n) : (cast (a * b : ZMod n) : R) = cast a * cast b

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ n
a b : ZMod n
⊢ (a * b).cast = a.cast * b.cast

Tactic:
cases n

Result:
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
a b : ZMod 0
⊢ (a * b).cast = a.cast * b.cast

case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ (a * b).cast = a.cast * b.cast

Proof state:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ a.cast * b.cast = (a * b).cast

Tactic:
dsimp [ZMod, ZMod.cast, ZMod.val]

Result:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ ↑↑a * ↑↑b = ↑↑(a * b)

Proof state:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ ↑↑a * ↑↑b = ↑↑(a * b)

Tactic:
rw [← Nat.cast_mul, Fin.val_mul, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _),
  @CharP.cast_eq_zero_iff R _ m]

Result:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ m ∣ ↑a * ↑b - ↑a * ↑b % (n✝ + 1)

Proof state:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ m ∣ ↑a * ↑b - ↑a * ↑b % (n✝ + 1)

Tactic:
exact h.trans (Nat.dvd_sub_mod _)

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ (a * b).cast = a.cast * b.cast

Tactic:
symm

Result:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ a.cast * b.cast = (a * b).cast

Proof state:
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
a b : ZMod 0
⊢ (a * b).cast = a.cast * b.cast

Tactic:
apply Int.cast_mul

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem of_mono {X Y : C} (f : X ⟶ Y) [Mono f] (i : IsZero Y) : IsZero X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
i : IsZero Y
⊢ IsZero X

Tactic:
have hf := i.eq_zero_of_tgt f

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
i : IsZero Y
hf : f = 0
⊢ IsZero X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
i : IsZero Y
hf : f = 0
⊢ IsZero X

Tactic:
subst hf

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
i : IsZero Y
inst✝ : Mono 0
⊢ IsZero X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
i : IsZero Y
inst✝ : Mono 0
⊢ IsZero X

Tactic:
exact IsZero.of_mono_zero X Y

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean
theorem T_complex_cosh (n : ℤ) : (T ℂ n).eval (cosh θ) = cosh (n * θ) := calc
  (T ℂ n).eval (cosh θ)
  _ = (T ℂ n).eval (cos (θ * I))

Proof state:
θ : ℂ
n : ℤ
⊢ cos (↑n * (θ * I)) = cos (↑n * θ * I)

Tactic:
rw [mul_assoc]

Result:
no goals

Proof state:
θ : ℂ
n : ℤ
⊢ eval (cosh θ) (T ℂ n) = eval (cos (θ * I)) (T ℂ n)

Tactic:
rw [cos_mul_I]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
lemma d_none_eq_zero' (i j : Option ι) (hj : j = none) :
    d K i j = 0

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i : Option ι
⊢ d K i none = 0

Tactic:
cases i <;> rfl

Result:
no goals

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i j : Option ι
hj : j = none
⊢ d K i j = 0

Tactic:
subst hj

Result:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i : Option ι
⊢ d K i none = 0
-- Mathlib/Data/Int/GCD.lean
theorem gcd_least_linear {a b : ℤ} (ha : a ≠ 0) :
    IsLeast { n : ℕ | 0 < n ∧ ∃ x y : ℤ, ↑n = a * x + b * y } (a.gcd b)

Proof state:
case right
a b : ℤ
ha : a ≠ 0
⊢ ∀ ⦃a_1 : ℕ⦄, 0 < a_1 → a.gcd b ∣ a_1 → a.gcd b ≤ a_1

Tactic:
exact fun n hn_pos hn => Nat.le_of_dvd hn_pos hn

Result:
no goals

Proof state:
case right
a b : ℤ
ha : a ≠ 0
⊢ a.gcd b ∈ lowerBounds {n | 0 < n ∧ a.gcd b ∣ n}

Tactic:
simp only [lowerBounds, and_imp, Set.mem_setOf_eq]

Result:
case right
a b : ℤ
ha : a ≠ 0
⊢ ∀ ⦃a_1 : ℕ⦄, 0 < a_1 → a.gcd b ∣ a_1 → a.gcd b ≤ a_1

Proof state:
a b : ℤ
ha : a ≠ 0
⊢ IsLeast {n | 0 < n ∧ a.gcd b ∣ n} (a.gcd b)

Tactic:
constructor

Result:
case left
a b : ℤ
ha : a ≠ 0
⊢ a.gcd b ∈ {n | 0 < n ∧ a.gcd b ∣ n}

case right
a b : ℤ
ha : a ≠ 0
⊢ a.gcd b ∈ lowerBounds {n | 0 < n ∧ a.gcd b ∣ n}

Proof state:
case left
a b : ℤ
ha : a ≠ 0
⊢ a.gcd b ∈ {n | 0 < n ∧ a.gcd b ∣ n}

Tactic:
simpa [and_true, dvd_refl, Set.mem_setOf_eq] using gcd_pos_of_ne_zero_left b ha

Result:
no goals

Proof state:
a b : ℤ
ha : a ≠ 0
⊢ IsLeast {n | 0 < n ∧ ∃ x y, ↑n = a * x + b * y} (a.gcd b)

Tactic:
simp_rw [← gcd_dvd_iff]

Result:
a b : ℤ
ha : a ≠ 0
⊢ IsLeast {n | 0 < n ∧ a.gcd b ∣ n} (a.gcd b)
-- Mathlib/AlgebraicGeometry/Restrict.lean
@[simp]
lemma morphismRestrict_id {X : Scheme.{u}} (U : X.Opens) : 𝟙 X ∣_ U = 𝟙 _

Proof state:
X : Scheme
U : X.Opens
⊢ 𝟙 X ∣_ U = 𝟙 ↑(𝟙 X ⁻¹ᵁ U)

Tactic:
rw [← cancel_mono U.ι, morphismRestrict_ι, Category.comp_id, Category.id_comp]

Result:
X : Scheme
U : X.Opens
⊢ (𝟙 X ⁻¹ᵁ U).ι = U.ι

Proof state:
X : Scheme
U : X.Opens
⊢ (𝟙 X ⁻¹ᵁ U).ι = U.ι

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean
/-- If a functor `G : J ⥤ C` to a concrete category has a limit and that `forget C`
is corepresentable, then `(G ⋙ forget C).sections` is small. -/
lemma small_sections_of_hasLimit
    {C : Type u} [Category.{v} C] [HasForget.{v} C]
    [(forget C).IsCorepresentable] {J : Type w} [Category.{t} J] (G : J ⥤ C) [HasLimit G] :
    Small.{v} (G ⋙ forget C).sections

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasForget C
inst✝² : (forget C).IsCorepresentable
J : Type w
inst✝¹ : Category.{t, w} J
G : J ⥤ C
inst✝ : HasLimit G
⊢ Small.{v, max v w} ↑(G ⋙ forget C).sections

Tactic:
rw [← Types.hasLimit_iff_small_sections]

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasForget C
inst✝² : (forget C).IsCorepresentable
J : Type w
inst✝¹ : Category.{t, w} J
G : J ⥤ C
inst✝ : HasLimit G
⊢ HasLimit (G ⋙ forget C)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasForget C
inst✝² : (forget C).IsCorepresentable
J : Type w
inst✝¹ : Category.{t, w} J
G : J ⥤ C
inst✝ : HasLimit G
⊢ HasLimit (G ⋙ forget C)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Nat/WithBot.lean
theorem add_eq_one_iff {n m : WithBot ℕ} : n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0

Proof state:
case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 1 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 0

Tactic:
simp [← WithBot.coe_add, Nat.add_eq_one_iff]

Result:
no goals

Proof state:
case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 1 ↔ ↑a✝ = 0 ∧ m = 1 ∨ ↑a✝ = 1 ∧ m = 0

Tactic:
cases m

Result:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 1 ↔ ↑a✝ = 0 ∧ ⊥ = 1 ∨ ↑a✝ = 1 ∧ ⊥ = 0

case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 1 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 0

Proof state:
case bot
m : WithBot ℕ
⊢ ⊥ + m = 1 ↔ ⊥ = 0 ∧ m = 1 ∨ ⊥ = 1 ∧ m = 0

Tactic:
simp only [WithBot.bot_add, WithBot.bot_ne_one, WithBot.bot_ne_zero, false_and, or_self]

Result:
no goals

Proof state:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 1 ↔ ↑a✝ = 0 ∧ ⊥ = 1 ∨ ↑a✝ = 1 ∧ ⊥ = 0

Tactic:
simp [WithBot.add_bot]

Result:
no goals

Proof state:
n m : WithBot ℕ
⊢ n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0

Tactic:
cases n

Result:
case bot
m : WithBot ℕ
⊢ ⊥ + m = 1 ↔ ⊥ = 0 ∧ m = 1 ∨ ⊥ = 1 ∧ m = 0

case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 1 ↔ ↑a✝ = 0 ∧ m = 1 ∨ ↑a✝ = 1 ∧ m = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Perm.lean
theorem Perm.symm {l₁ l₂ : Array α} (h : l₁ ~ l₂) : l₂ ~ l₁

Proof state:
α : Type u_1
l₁ l₂ : Array α
h : l₁ ~ l₂
⊢ l₂ ~ l₁

Tactic:
cases l₁

Result:
case mk
α : Type u_1
l₂ : Array α
toList✝ : List α
h : { toList := toList✝ } ~ l₂
⊢ l₂ ~ { toList := toList✝ }

Proof state:
case mk
α : Type u_1
l₂ : Array α
toList✝ : List α
h : { toList := toList✝ } ~ l₂
⊢ l₂ ~ { toList := toList✝ }

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
h : { toList := toList✝¹ } ~ { toList := toList✝ }
⊢ { toList := toList✝ } ~ { toList := toList✝¹ }

Proof state:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
h : toList✝¹ ~ toList✝
⊢ { toList := toList✝ } ~ { toList := toList✝¹ }

Tactic:
simpa using h.symm

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
h : { toList := toList✝¹ } ~ { toList := toList✝ }
⊢ { toList := toList✝ } ~ { toList := toList✝¹ }

Tactic:
simp only [perm_toArray] at h

Result:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
h : toList✝¹ ~ toList✝
⊢ { toList := toList✝ } ~ { toList := toList✝¹ }
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_preimage_linearEquiv (f : E ≃ₗ[ℝ] E) (s : Set E) :
    μ (f ⁻¹' s) = ENNReal.ofReal |LinearMap.det (f.symm : E →ₗ[ℝ] E)| * μ s

Proof state:
case h.e'_3.h.e'_5.h.e'_1.h.e'_4
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E ≃ₗ[ℝ] E
s : Set E
A : LinearMap.det ↑f ≠ 0
⊢ LinearMap.det ↑f.symm = (LinearMap.det ↑f)⁻¹

Tactic:
simp only [LinearEquiv.det_coe_symm]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E ≃ₗ[ℝ] E
s : Set E
⊢ μ (⇑f ⁻¹' s) = ENNReal.ofReal |LinearMap.det ↑f.symm| * μ s

Tactic:
have A : LinearMap.det (f : E →ₗ[ℝ] E) ≠ 0 := (LinearEquiv.isUnit_det' f).ne_zero

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E ≃ₗ[ℝ] E
s : Set E
A : LinearMap.det ↑f ≠ 0
⊢ μ (⇑f ⁻¹' s) = ENNReal.ofReal |LinearMap.det ↑f.symm| * μ s

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E ≃ₗ[ℝ] E
s : Set E
A : LinearMap.det ↑f ≠ 0
⊢ μ (⇑f ⁻¹' s) = ENNReal.ofReal |LinearMap.det ↑f.symm| * μ s

Tactic:
convert addHaar_preimage_linearMap μ A s

Result:
case h.e'_3.h.e'_5.h.e'_1.h.e'_4
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E ≃ₗ[ℝ] E
s : Set E
A : LinearMap.det ↑f ≠ 0
⊢ LinearMap.det ↑f.symm = (LinearMap.det ↑f)⁻¹
-- Mathlib/Algebra/Group/Action/Hom.lean
/-- If an action is transitive, then composing this action with a surjective homomorphism gives
again a transitive action. -/
@[to_additive]
lemma isPretransitive_compHom {E F G : Type*} [Monoid E] [Monoid F] [MulAction F G]
    [IsPretransitive F G] {f : E →* F} (hf : Surjective f) :
    letI : MulAction E G := MulAction.compHom _ f
    IsPretransitive E G

Proof state:
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
x y : G
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨m, rfl⟩ : ∃ m : F, m • x = y := exists_smul_eq F x y

Result:
case intro
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
x : G
m : F
⊢ ∃ g, g • x = m • x

Proof state:
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
⊢ IsPretransitive E G

Tactic:
refine ⟨fun x y ↦ ?_⟩

Result:
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
x y : G
⊢ ∃ g, g • x = y

Proof state:
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
⊢ IsPretransitive E G

Tactic:
let _ : MulAction E G := MulAction.compHom _ f

Result:
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
⊢ IsPretransitive E G

Proof state:
case intro.intro
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
x : G
e : E
⊢ ∃ g, g • x = f e • x

Tactic:
exact ⟨e, rfl⟩

Result:
no goals

Proof state:
case intro
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
x : G
m : F
⊢ ∃ g, g • x = m • x

Tactic:
obtain ⟨e, rfl⟩ : ∃ e, f e = m := hf m

Result:
case intro.intro
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
x : G
e : E
⊢ ∃ g, g • x = f e • x
-- Mathlib/Algebra/Lie/Derivation/AdjointAction.lean
lemma lie_ad (x : L) (D : LieDerivation R L L) : ⁅ad R L x, D⁆ = ⁅x, D⁆

Proof state:
case H
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
a✝ : L
⊢ ⁅(ad R L) x, D⁆ a✝ = ⁅x, D⁆ a✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
⊢ ⁅(ad R L) x, D⁆ = ⁅x, D⁆

Tactic:
ext

Result:
case H
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
a✝ : L
⊢ ⁅(ad R L) x, D⁆ a✝ = ⁅x, D⁆ a✝
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToL1_congr_left' (T T' : Set α → E →L[ℝ] F) {C C' : ℝ}
    (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C')
    (h : ∀ s, MeasurableSet s → μ s < ∞ → T s = T' s) (f : α →₁[μ] E) :
    setToL1 hT f = setToL1 hT' f

Proof state:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s
f✝ : ↥(Lp E 1 μ)
f : ↥(simpleFunc E 1 μ)
⊢ (setToL1 hT') ↑f = (setToL1SCLM α E μ hT) f

Tactic:
rw [setToL1_eq_setToL1SCLM]

Result:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s
f✝ : ↥(Lp E 1 μ)
f : ↥(simpleFunc E 1 μ)
⊢ (setToL1SCLM α E μ hT') f = (setToL1SCLM α E μ hT) f
-- Mathlib/Data/Nat/Nth.lean
theorem count_nth_zero : count p (nth p 0) = 0

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ ∀ ⦃x : ℕ⦄, x ∈ range (sInf (setOf p)) → ¬p x

Tactic:
exact fun n h₁ h₂ => (mem_range.1 h₁).not_le (Nat.sInf_le h₂)

Result:
no goals

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p (nth p 0) = 0

Tactic:
rw [count_eq_card_filter_range, card_eq_zero, filter_eq_empty_iff, nth_zero]

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ ∀ ⦃x : ℕ⦄, x ∈ range (sInf (setOf p)) → ¬p x