harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range'_eq_nil_iff : range' s n step = [] ↔ n = 0

Proof state:
s n step : Nat
⊢ range' s n step = [] ↔ n = 0

Tactic:
rw [← length_eq_zero, length_range']

Result:
no goals
-- Mathlib/Algebra/Group/Even.lean
@[to_additive (attr := simp)] lemma isSquare_inv : IsSquare a⁻¹ ↔ IsSquare a

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
a : α
⊢ IsSquare a⁻¹ ↔ IsSquare a

Tactic:
constructor <;> intro h <;> simpa using (isSquare_op_iff.mpr h).map (MulEquiv.inv' α).symm

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Subspace.lean
theorem DirectSum.IsInternal.collectedBasis_orthonormal [DecidableEq ι] {V : ι → Submodule 𝕜 E}
    (hV : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ)
    (hV_sum : DirectSum.IsInternal fun i => V i) {α : ι → Type*}
    {v_family : ∀ i, Basis (α i) 𝕜 (V i)} (hv_family : ∀ i, Orthonormal 𝕜 (v_family i)) :
    Orthonormal 𝕜 (hV_sum.collectedBasis v_family)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
hV_sum : IsInternal fun i => V i
α : ι → Type u_6
v_family : (i : ι) → Basis (α i) 𝕜 ↥(V i)
hv_family : ∀ (i : ι), Orthonormal 𝕜 ⇑(v_family i)
⊢ Orthonormal 𝕜 ⇑(hV_sum.collectedBasis v_family)

Tactic:
simpa only [hV_sum.collectedBasis_coe] using hV.orthonormal_sigma_orthonormal hv_family

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_eq_pi_div_two_iff {θ : Angle} : θ.toReal = π / 2 ↔ θ = (π / 2 : ℝ)

Proof state:
θ : Angle
⊢ θ.toReal = π / 2 ↔ θ = ↑(π / 2)

Tactic:
rw [← toReal_inj, toReal_pi_div_two]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Comp.lean
@[simp]
lemma comp_discard (κ : Kernel α β) [IsMarkovKernel κ] : discard β ∘ₖ κ = discard α

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a : α
s : Set Unit
hs : MeasurableSet s
⊢ ((discard β ∘ₖ κ) a) s = ((discard α) a) s

Tactic:
simp [comp_apply' _ _ _ hs]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ discard β ∘ₖ κ = discard α

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a : α
s : Set Unit
hs : MeasurableSet s
⊢ ((discard β ∘ₖ κ) a) s = ((discard α) a) s
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNormEssSup_zero : eLpNormEssSup (0 : α → F) μ = 0

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
⊢ eLpNormEssSup 0 μ = 0

Tactic:
simp [eLpNormEssSup, ← bot_eq_zero', essSup_const_bot]

Result:
no goals
-- Mathlib/Data/Quot.lean
theorem Quotient.out_equiv_out {s : Setoid α} {x y : Quotient s} : x.out ≈ y.out ↔ x = y

Proof state:
α : Sort u_1
s : Setoid α
x y : Quotient s
⊢ x.out ≈ y.out ↔ x = y

Tactic:
rw [← Quotient.eq_mk_iff_out, Quotient.out_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
lemma charpoly_map (M : Matrix n n R) (f : R →+* S) :
    (M.map f).charpoly = M.charpoly.map f

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
⊢ (M.map ⇑f).charpoly = Polynomial.map f M.charpoly

Tactic:
rw [charpoly, charmatrix_map, ← Polynomial.coe_mapRingHom, charpoly, RingHom.map_det,
  RingHom.mapMatrix_apply]

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iUnion_Ico_eq_Iio_self_iff {f : ι → α} {a : α} :
    ⋃ i, Ico (f i) a = Iio a ↔ ∀ x < a, ∃ i, f i ≤ x

Proof state:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
a : α
⊢ ⋃ i, Ico (f i) a = Iio a ↔ ∀ x < a, ∃ i, f i ≤ x

Tactic:
simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem replicate_succ' {x : BitVec w} :
    x.replicate (n + 1) =
    (replicate n x ++ x).cast (by rw [Nat.mul_succ])

Proof state:
w n : Nat
x : BitVec w
⊢ w * n + w = w * (n + 1)

Tactic:
rw [Nat.mul_succ]

Result:
no goals

Proof state:
w n : Nat
x : BitVec w
⊢ replicate (n + 1) x = BitVec.cast ⋯ (replicate n x ++ x)

Tactic:
simp [replicate_append_self]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma IsCircuit.isCocircuit_inter_nontrivial (hC : M.IsCircuit C) (hK : M.IsCocircuit K)
    (hCK : (C ∩ K).Nonempty) : (C ∩ K).Nontrivial

Proof state:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
hCK : (C ∩ K).Nonempty
⊢ (C ∩ K).Nontrivial

Tactic:
obtain ⟨e, heCK⟩ := hCK

Result:
case intro
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
e : α
heCK : e ∈ C ∩ K
⊢ (C ∩ K).Nontrivial

Proof state:
case intro
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
e : α
heCK : e ∈ C ∩ K
⊢ (C ∩ K).Nontrivial

Tactic:
rw [nontrivial_iff_ne_singleton heCK]

Result:
case intro
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
e : α
heCK : e ∈ C ∩ K
⊢ C ∩ K ≠ {e}

Proof state:
case intro
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
e : α
heCK : e ∈ C ∩ K
⊢ C ∩ K ≠ {e}

Tactic:
exact hC.inter_isCocircuit_ne_singleton hK

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem exists_grundyValue_moveLeft_of_lt {G : PGame} {o : Nimber} (h : o < grundyValue G) :
    ∃ i, grundyValue (G.moveLeft i) = o

Proof state:
G : PGame
o : Nimber
h : o < sInf (Set.range (grundyValue ∘ G.moveLeft))ᶜ
⊢ ∃ i, (G.moveLeft i).grundyValue = o

Tactic:
by_contra ha

Result:
G : PGame
o : Nimber
h : o < sInf (Set.range (grundyValue ∘ G.moveLeft))ᶜ
ha : ¬∃ i, (G.moveLeft i).grundyValue = o
⊢ False

Proof state:
G : PGame
o : Nimber
h : o < sInf (Set.range (grundyValue ∘ G.moveLeft))ᶜ
ha : ¬∃ i, (G.moveLeft i).grundyValue = o
⊢ False

Tactic:
exact h.not_le (csInf_le' ha)

Result:
no goals

Proof state:
G : PGame
o : Nimber
h : o < G.grundyValue
⊢ ∃ i, (G.moveLeft i).grundyValue = o

Tactic:
rw [grundyValue_eq_sInf_moveLeft] at h

Result:
G : PGame
o : Nimber
h : o < sInf (Set.range (grundyValue ∘ G.moveLeft))ᶜ
⊢ ∃ i, (G.moveLeft i).grundyValue = o
-- Mathlib/Topology/Homotopy/Basic.lean
theorem eq_snd (F : HomotopyRel f₀ f₁ S) (t : I) {x : X} (hx : x ∈ S) : F (t, x) = f₁ x

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
t : ↑I
x : X
hx : x ∈ S
⊢ F (t, x) = f₁ x

Tactic:
rw [F.eq_fst t hx, ← F.eq_fst 1 hx, F.apply_one]

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_empty_right (s : Set E) : convexJoin 𝕜 s ∅ = ∅

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ convexJoin 𝕜 s ∅ = ∅

Tactic:
simp [convexJoin]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma liftCochain_v_snd_v (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂) :
    (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (snd φ).v p₂ p₂ (add_zero p₂) = β.v p₁ p₂ h₁₂

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
p₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (snd φ).v p₂ p₂ ⋯ = β.v p₁ p₂ h₁₂

Tactic:
simpa only [Cochain.comp_v _ _ (add_zero n) p₁ p₂ p₂ h₁₂ (add_zero p₂)]
  using Cochain.congr_v (liftCochain_snd φ α β h) p₁ p₂ (by omega)

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
p₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ p₁ + n = p₂

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_pi_univ_eq [Finite ι] (s : ∀ i, Set (π i)) (x : ∀ i, π i) :
    𝓝[pi univ s] x = ⨅ i, comap (fun x => x i) (𝓝[s i] x i)

Proof state:
ι : Type u_5
π : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : (i : ι) → Set (π i)
x : (i : ι) → π i
⊢ 𝓝[univ.pi s] x = ⨅ i, comap (fun x => x i) (𝓝[s i] x i)

Tactic:
simpa [nhdsWithin] using nhdsWithin_pi_eq finite_univ s x

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma equation_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W'.Equation P ↔ W'.Equation Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.Equation P ↔ W'.Equation Q

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
W' : Projective R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Equation ((fun m => m • Q) u) ↔ W'.Equation Q

Proof state:
case intro
R : Type r
inst✝ : CommRing R
W' : Projective R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Equation ((fun m => m • Q) u) ↔ W'.Equation Q

Tactic:
exact equation_smul Q u.isUnit

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem Fork.app_one_eq_ι_comp_right (s : Fork f g) : s.π.app one = s.ι ≫ g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
⊢ s.π.app one = s.ι ≫ g

Tactic:
rw [← s.app_zero_eq_ι, ← s.w right, parallelPair_map_right]

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_mk_eq_prod (f : Filter α) (g : Filter β) : map₂ Prod.mk f g = f ×ˢ g

Proof state:
α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
⊢ map₂ Prod.mk f g = f ×ˢ g

Tactic:
simp only [← map_prod_eq_map₂, map_id']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_alter [LawfulBEq α] {k k' fallback : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
    (m.alter k f).getKeyD k' fallback =
      if k == k' then
        if (f (m.get? k)).isSome then k else fallback
      else
        m.getKeyD k' fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' fallback : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).getKeyD k' fallback =
    if (k == k') = true then if (f (m.get? k)).isSome = true then k else fallback else m.getKeyD k' fallback

Tactic:
simp_to_raw using Raw₀.getKeyD_alter

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem inv_le_of_le_mul {r p : ℝ≥0} (h : 1 ≤ r * p) : r⁻¹ ≤ p

Proof state:
r p : ℝ≥0
h : 1 ≤ r * p
⊢ r⁻¹ ≤ p

Tactic:
by_cases r = 0 <;> simp [*, inv_le]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_mul_left_Ico {a : α} (h : 0 < a) (b c : α) :
    (a * ·) '' Ico b c = Ico (a * b) (a * c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
h : 0 < a
b c : α
⊢ (fun x => a * x) '' Ico b c = Ico (a * b) (a * c)

Tactic:
convert image_mul_right_Ico b c h using 1 <;> simp only [mul_comm _ a]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma dirac_unit_compProd (κ : Kernel Unit β) [IsSFiniteKernel κ] :
    Measure.dirac () ⊗ₘ κ = (κ ()).map (Prod.mk ())

Proof state:
β : Type u_2
mβ : MeasurableSpace β
κ : Kernel Unit β
inst✝ : IsSFiniteKernel κ
⊢ dirac () ⊗ₘ κ = map (Prod.mk ()) (κ ())

Tactic:
ext s hs

Result:
case h
β : Type u_2
mβ : MeasurableSpace β
κ : Kernel Unit β
inst✝ : IsSFiniteKernel κ
s : Set (Unit × β)
hs : MeasurableSet s
⊢ (dirac () ⊗ₘ κ) s = (map (Prod.mk ()) (κ ())) s

Proof state:
case h
β : Type u_2
mβ : MeasurableSpace β
κ : Kernel Unit β
inst✝ : IsSFiniteKernel κ
s : Set (Unit × β)
hs : MeasurableSet s
⊢ (dirac () ⊗ₘ κ) s = (map (Prod.mk ()) (κ ())) s

Tactic:
rw [dirac_compProd_apply hs, Measure.map_apply measurable_prod_mk_left hs]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Cast.lean
theorem cast_choose_eq_ascPochhammer_div (a b : ℕ) :
    (a.choose b : K) = (ascPochhammer K b).eval ↑(a - (b - 1)) / b !

Proof state:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a.choose b) = Polynomial.eval (↑(a - (b - 1))) (ascPochhammer K b) / ↑b !

Tactic:
rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
  mul_comm, ← descFactorial_eq_factorial_mul_choose, ← cast_descFactorial]

Result:
no goals
-- Mathlib/Tactic/Ring/RingNF.lean
theorem nat_rawCast_1 : (Nat.rawCast 1 : R) = 1

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ Nat.rawCast 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_eq_false_imp : ∀ {x y : Bool}, (x && y) = false ↔ (x = true → y = false)

Proof state:
⊢ ∀ {x y : Bool}, (x && y) = false ↔ x = true → y = false

Tactic:
decide

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Span.lean
theorem iInf_ker_lapply_le_bot : ⨅ a, ker (lapply a : (α →₀ M) →ₗ[R] M) ≤ ⊥

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ ⦃x : α →₀ M⦄, (∀ (i : α), x i = 0) → x = 0

Tactic:
exact fun a h => Finsupp.ext h

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⨅ a, ker (lapply a) ≤ ⊥

Tactic:
simp only [SetLike.le_def, mem_iInf, mem_ker, mem_bot, lapply_apply]

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ ⦃x : α →₀ M⦄, (∀ (i : α), x i = 0) → x = 0
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
@[simp] lemma rpow_inv_rpow (hx : 0 ≤ x) (hy : y ≠ 0) : (x ^ y⁻¹) ^ y = x

Proof state:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
⊢ (x ^ y⁻¹) ^ y = x

Tactic:
rw [← rpow_mul hx, inv_mul_cancel₀ hy, rpow_one]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousOn_iff :
    ContinuousOn f s ↔
      ∀ x ∈ s, ∀ t : Set β, IsOpen t → f x ∈ t → ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' t

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ x ∈ s, ∀ (t : Set β), IsOpen t → f x ∈ t → ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' t

Tactic:
simp only [ContinuousOn, ContinuousWithinAt, tendsto_nhds, mem_nhdsWithin]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem relindex_bot_left : (⊥ : Subgroup G).relindex H = Nat.card H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊥.relindex H = Nat.card ↥H

Tactic:
rw [relindex, bot_subgroupOf, index_bot]

Result:
no goals
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem lift_comp_lift_apply_eq_self [PerfectRing L p] (x : L) :
    lift j i p (lift i j p x) = x

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing K
inst✝⁸ : CommRing L
inst✝⁷ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝⁶ : ExpChar M p
inst✝⁵ : ExpChar K p
inst✝⁴ : PerfectRing M p
inst✝³ : IsPRadical i p
inst✝² : ExpChar L p
inst✝¹ : IsPRadical j p
inst✝ : PerfectRing L p
x : L
⊢ (lift j i p) ((lift i j p) x) = x

Tactic:
rw [lift_comp_lift_apply, lift_self_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma nonsingular_of_Z_eq_zero {P : Fin 3 → R} (hPz : P z = 0) :
    W'.Nonsingular P ↔
      W'.Equation P ∧ (3 * P x ^ 2 ≠ 0 ∨ P y ^ 2 + W'.a₁ * P x * P y - W'.a₂ * P x ^ 2 ≠ 0)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.Nonsingular P ↔ W'.Equation P ∧ (3 * P x ^ 2 ≠ 0 ∨ P y ^ 2 + W'.a₁ * P x * P y - W'.a₂ * P x ^ 2 ≠ 0)

Tactic:
simp only [nonsingular_iff, hPz, add_zero, sub_zero, zero_sub, mul_zero,
  zero_pow <| OfNat.ofNat_ne_zero _, neg_ne_zero, ne_self_iff_false, false_or]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerLeft_eqToHom (X : C) {Y Z : C} (f : Y = Z) :
    X ◁ eqToHom f = eqToHom (congr_arg₂ tensorObj rfl f)

Proof state:
case refl
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ X ◁ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp only [whiskerLeft_id, eqToHom_refl]

Result:
no goals

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
f : Y = Z
⊢ X ◁ eqToHom f = eqToHom ⋯

Tactic:
cases f

Result:
case refl
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ X ◁ eqToHom ⋯ = eqToHom ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁

Proof state:
α✝ : Type u_1
l₁ : List α✝
b : α✝
⊢ (l₁ ++ [b]).dropLast = l₁

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem one_shiftLeft (n : Nat) : 1 <<< n = 2 ^ n

Proof state:
n : Nat
⊢ 1 <<< n = 2 ^ n

Tactic:
rw [shiftLeft_eq, Nat.one_mul]

Result:
no goals
-- Mathlib/Topology/Order/ScottTopology.lean
lemma dirSupInacc_iff_forall_sSup :
    DirSupInacc s ↔ ∀ ⦃d⦄, d.Nonempty → DirectedOn (· ≤ ·) d → sSup d ∈ s → (d ∩ s).Nonempty

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → sSup d ∈ s → (d ∩ s).Nonempty

Tactic:
simp [DirSupInacc, isLUB_iff_sSup_eq]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addMap_of_Y_eq {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) (hy' : P y * Q z = W.negY Q * P z) :
    W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![0, 1, 0]⟧

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z = W.negY Q * P z
hy : P y * Q z = Q y * P z
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![0, 1, 0]⟧

Tactic:
rw [addMap_eq, add_of_Y_eq hP.left hPz hQz hx hy hy',
  smul_eq _ <| isUnit_dblU_of_Y_eq hP hPz hQz hx hy hy']

Result:
no goals

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z = W.negY Q * P z
hy : ¬P y * Q z = Q y * P z
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![0, 1, 0]⟧

Tactic:
rw [addMap_eq, add_of_Y_ne hP.left hQ hPz hQz hx hy,
  smul_eq _ <| isUnit_addU_of_Y_ne hPz hQz hy]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![0, 1, 0]⟧

Tactic:
by_cases hy : P y * Q z = Q y * P z

Result:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z = W.negY Q * P z
hy : P y * Q z = Q y * P z
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![0, 1, 0]⟧

case neg
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z = W.negY Q * P z
hy : ¬P y * Q z = Q y * P z
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![0, 1, 0]⟧
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma ofENat_eq_one {m : ℕ∞} : (m : Cardinal) = 1 ↔ m = 1

Proof state:
m : ℕ∞
⊢ ↑m = 1 ↔ m = 1

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean
theorem exp_blockDiagonal (v : m → Matrix n n 𝔸) :
    exp 𝕂 (blockDiagonal v) = blockDiagonal (exp 𝕂 v)

Proof state:
𝕂 : Type u_1
m : Type u_2
n : Type u_3
𝔸 : Type u_5
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq m
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : TopologicalSpace 𝔸
inst✝² : IsTopologicalRing 𝔸
inst✝¹ : Algebra 𝕂 𝔸
inst✝ : T2Space 𝔸
v : m → Matrix n n 𝔸
⊢ exp 𝕂 (blockDiagonal v) = blockDiagonal (exp 𝕂 v)

Tactic:
simp_rw [exp_eq_tsum, ← blockDiagonal_pow, ← blockDiagonal_smul, ← blockDiagonal_tsum]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem taylor_X : taylor r X = X + C r

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
⊢ (taylor r) X = X + C r

Tactic:
simp only [taylor_apply, X_comp]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_smul_const_vsub_eq_sub_weightedVSubOfPoint (w : ι → k) (p₂ : ι → P) (p₁ b : P) :
    (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i)) = (∑ i ∈ s, w i) • (p₁ -ᵥ b) - s.weightedVSubOfPoint p₂ b w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₂ : ι → P
p₁ b : P
⊢ ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = (∑ i ∈ s, w i) • (p₁ -ᵥ b) - (s.weightedVSubOfPoint p₂ b) w

Tactic:
rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioc_eq_cons_Ioo (h : a < b) : Ioc a b = (Ioo a b).cons b right_not_mem_Ioo

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ioc a b = cons b (Ioo a b) ⋯

Tactic:
rw [cons_eq_insert, Ioo_insert_right h]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ioc a b = cons b (Ioo a b) ⋯

Tactic:
classical rw [cons_eq_insert, Ioo_insert_right h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_alterKey_eq_add_one {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)}
    (h : containsKey k l = false) (h' : (f (getValue? k l)).isSome) :
    (alterKey k f l).length = l.length + 1

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
h : containsKey k l = false
h' : (f (getValue? k l)).isSome = true
⊢ (alterKey k f l).length = l.length + 1

Tactic:
simp [length_alterKey', h, h']

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem collinear_insert_of_mem_affineSpan_pair {p₁ p₂ p₃ : P} (h : p₁ ∈ line[k, p₂, p₃]) :
    Collinear k ({p₁, p₂, p₃} : Set P)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
h : p₁ ∈ affineSpan k {p₂, p₃}
⊢ Collinear k {p₁, p₂, p₃}

Tactic:
rw [collinear_insert_iff_of_mem_affineSpan h]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
h : p₁ ∈ affineSpan k {p₂, p₃}
⊢ Collinear k {p₂, p₃}

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
h : p₁ ∈ affineSpan k {p₂, p₃}
⊢ Collinear k {p₂, p₃}

Tactic:
exact collinear_pair _ _ _

Result:
no goals
-- Mathlib/Combinatorics/HalesJewett.lean
@[simp] lemma toSubspaceUnit_apply (l : Line α ι) (a) : ⇑l.toSubspaceUnit a = l (a ())

Proof state:
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
⊢ ↑l.toSubspaceUnit a = ↑l (a ())

Tactic:
ext i

Result:
case h
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
i : ι
⊢ ↑l.toSubspaceUnit a i = ↑l (a ()) i

Proof state:
case h
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
i : ι
⊢ ↑l.toSubspaceUnit a i = ↑l (a ()) i

Tactic:
cases h : l.idxFun i <;> simp [toSubspaceUnit, h, Subspace.coe_apply]

Result:
no goals