harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/CoverLifting.lean
lemma fac' (j : StructuredArrow (op X) G.op) :
    lift hF hR s ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s j.hom.unop

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
j : StructuredArrow (op X) G.op
⊢ lift hF hR s ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s j.hom.unop

Tactic:
apply IsLimit.fac

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem castPred_inj {i j : Fin (n + 1)} {hi : i ≠ last n} {hj : j ≠ last n} :
    castPred i hi = castPred j hj ↔ i = j

Proof state:
n : ℕ
i j : Fin (n + 1)
hi : i ≠ last n
hj : j ≠ last n
⊢ i.castPred hi = j.castPred hj ↔ i = j

Tactic:
simp_rw [Fin.ext_iff, le_antisymm_iff, ← le_def, castPred_le_castPred_iff]

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem mk_mem_row_iff {μ : YoungDiagram} {i j : ℕ} : (i, j) ∈ μ.row i ↔ (i, j) ∈ μ

Proof state:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ.row i ↔ (i, j) ∈ μ

Tactic:
simp [row]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem IsCompact.closedBall_mul (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) :
    closedBall x δ * s = x • cthickening δ s

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ closedBall x δ * s = x • cthickening δ s

Tactic:
rw [mul_comm, hs.mul_closedBall hδ]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Invariant.lean
@[simp]
protected lemma top_mem : ⊤ ∈ f.invtSubmodule

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
⊢ ⊤ ∈ f.invtSubmodule

Tactic:
simp [invtSubmodule]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma isUnramified_iff_card_stabilizer_eq_one [IsGalois k K] :
    IsUnramified k w ↔ Nat.card (Stab w) = 1

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ IsUnramified k w ↔ Nat.card ↥(Stab w) = 1

Tactic:
rw [isUnramified_iff_stabilizer_eq_bot, Subgroup.card_eq_one]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean
theorem prod_ext_iff {f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)} :
    f = g ↔ (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap f =
      (ContinuousLinearMap.fst _ _ _).compContinuousMultilinearMap g ∧
      (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap f =
      (ContinuousLinearMap.snd _ _ _).compContinuousMultilinearMap g

Proof state:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst✝⁹ : Semiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : (i : ι) → TopologicalSpace (M₁ i)
inst✝¹ : TopologicalSpace M₂
inst✝ : TopologicalSpace M₃
f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)
⊢ f = g ↔
    (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap f =
        (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap g ∧
      (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap f =
        (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap g

Tactic:
rw [← Prod.mk.inj_iff, ← prodEquiv_symm_apply, ← prodEquiv_symm_apply, Equiv.apply_eq_iff_eq]

Result:
no goals
-- Mathlib/Analysis/Complex/Circle.lean
@[simp] lemma normSq_coe (z : Circle) : normSq z = 1

Proof state:
z : Circle
⊢ normSq ↑z = 1

Tactic:
simp [normSq_eq_norm_sq]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma odd_mul : Odd (m * n) ↔ Odd m ∧ Odd n

Proof state:
m n : ℕ
⊢ Odd (m * n) ↔ Odd m ∧ Odd n

Tactic:
simp [not_or, even_mul, ← not_even_iff_odd]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem prod_mem_nhds_iff {s : Set X} {t : Set Y} {x : X} {y : Y} :
    s ×ˢ t ∈ 𝓝 (x, y) ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
x : X
y : Y
⊢ s ×ˢ t ∈ 𝓝 (x, y) ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y

Tactic:
rw [nhds_prod_eq, prod_mem_prod_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
@[simp]
lemma basis_one : CoordinateRing.basis W 1 = mk W Y

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
⊢ (CoordinateRing.basis W) 1 = (mk W) Y

Tactic:
simpa only [basis_apply] using pow_one _

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sin_ne_zero_iff {θ : Angle} : sin θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ π

Proof state:
θ : Angle
⊢ θ.sin ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
rw [← not_or, ← sin_eq_zero_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Classes/SatisfiesM.lean
theorem of_true [Applicative m] [LawfulApplicative m] {x : m α}
    (h : ∀ a, p a) : SatisfiesM p x :=
  ⟨(fun a => ⟨a, h a⟩) <$> x, by simp [← comp_map, Function.comp_def]⟩

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
x : m α
h : ∀ (a : α), p a
⊢ Subtype.val <$> (fun a => ⟨a, ⋯⟩) <$> x = x

Tactic:
simp [← comp_map, Function.comp_def]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem isClosed_coinduced {t : TopologicalSpace α} {s : Set β} {f : α → β} :
    IsClosed[t.coinduced f] s ↔ IsClosed (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
s : Set β
f : α → β
⊢ IsClosed s ↔ IsClosed (f ⁻¹' s)

Tactic:
simp only [← isOpen_compl_iff, isOpen_coinduced (f := f), preimage_compl]

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma map_zero_succ_succ (j : ℕ) (hj : j + 2 < n + 1 + 1) :
    map F f 0 ⟨j + 2, hj⟩ (by simp) = f ≫ F.map' 0 (j+1) := rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.86957, u_1} C
n m : ℕ
F G : ComposableArrows C n
X : C
f : X ⟶ F.left
j : ℕ
hj : j + 2 < n + 1 + 1
⊢ 0 ≤ ⟨j + 2, hj⟩

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem false_eq (b : Bool) : (false = b) = (b = false)

Proof state:
b : Bool
⊢ (false = b) = (b = false)

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/Computability/Language.lean
theorem mem_one (x : List α) : x ∈ (1 : Language α) ↔ x = []

Proof state:
α : Type u_1
x : List α
⊢ x ∈ 1 ↔ x = []

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem sub_mul (M M' : Matrix m n α) (N : Matrix n o α) :
    (M - M') * N = M * N - M' * N

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M M' : Matrix m n α
N : Matrix n o α
⊢ (M - M') * N = M * N - M' * N

Tactic:
rw [sub_eq_add_neg, Matrix.add_mul, Matrix.neg_mul, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem le_toNNReal_iff_coe_le {r : ℝ≥0} {p : ℝ} (hp : 0 ≤ p) : r ≤ Real.toNNReal p ↔ ↑r ≤ p

Proof state:
r : ℝ≥0
p : ℝ
hp : 0 ≤ p
⊢ r ≤ p.toNNReal ↔ ↑r ≤ p

Tactic:
rw [← NNReal.coe_le_coe, Real.coe_toNNReal p hp]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem map_whiskerRight {X Y : C} (f : X ⟶ Y) (Z : C) :
    F.map (f ▷ Z) = δ F X Z ≫ F.map f ▷ F.obj Z ≫ μ F Y Z

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
f : X ⟶ Y
Z : C
⊢ F.map (f ▷ Z) = δ F X Z ≫ F.map f ▷ F.obj Z ≫ μ F Y Z

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalAverage.lean
theorem interval_average_symm (f : ℝ → E) (a b : ℝ) : (⨍ x in a..b, f x) = ⨍ x in b..a, f x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
⊢ ⨍ (x : ℝ) in a..b, f x = ⨍ (x : ℝ) in b..a, f x

Tactic:
rw [setAverage_eq, setAverage_eq, uIoc_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem Basis.det_reindex {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M) (v : ι' → M)
    (e : ι ≃ ι') : (b.reindex e).det v = b.det (v ∘ e)

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 ι
ι' : Type u_6
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ (b.reindex e).det v = b.det (v ∘ ⇑e)

Tactic:
rw [Basis.det_apply, Basis.toMatrix_reindex', det_reindexAlgEquiv, Basis.det_apply]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Set/Basic.lean
lemma Nonempty.zero_mul (hs : s.Nonempty) : 0 * s = 0 :=
  s.zero_mul_subset.antisymm <| by simpa [mem_mul] using hs

Proof state:
α : Type u_1
inst✝ : MulZeroClass α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ 0 * s

Tactic:
simpa [mem_mul] using hs

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extChartAt_preimage_mem_nhdsWithin' {x x' : M} (h : x' ∈ (extChartAt I x).source)
    (ht : t ∈ 𝓝[s] x') :
    (extChartAt I x).symm ⁻¹' t ∈ 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x'

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s t : Set M
inst✝ : ChartedSpace H M
x x' : M
h : x' ∈ (extChartAt I x).source
ht : t ∈ 𝓝[s] x'
⊢ ↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x'

Tactic:
rwa [← map_extChartAt_symm_nhdsWithin' h, mem_map] at ht

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc]
lemma opcyclesOpIso_inv_naturality (φ : S₁ ⟶ S₂)
    [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    (cyclesMap φ).op ≫ (S₁.opcyclesOpIso).inv =
      S₂.opcyclesOpIso.inv ≫ opcyclesMap (opMap φ)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ (cyclesMap φ).op ≫ S₁.opcyclesOpIso.inv = S₂.opcyclesOpIso.inv ≫ opcyclesMap (opMap φ)

Tactic:
rw [← cancel_epi (S₂.opcyclesOpIso.hom), Iso.hom_inv_id_assoc,
  ← opcyclesOpIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited β]
    (h : m.WF) {a : α} :
    m.contains a = false → get! m a = default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
a : α
⊢ m.contains a = false → get! m a = default

Tactic:
simp_to_raw using Raw₀.Const.get!_eq_default

Result:
no goals
-- Mathlib/Algebra/Lie/Free.lean
theorem Rel.neg {a b : lib R X} (h : Rel R X a b) : Rel R X (-a) (-b)

Proof state:
R : Type u
X : Type v
inst✝ : CommRing R
a b : lib R X
h : Rel R X a b
⊢ Rel R X (-a) (-b)

Tactic:
simpa only [neg_one_smul] using h.smul (-1)

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
@[simp]
lemma antivaryOn_inv_right₀ (hg : ∀ i ∈ s, 0 < g i) : AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s :=
  forall₂_swap.trans <| forall₄_congr fun i hi j hj ↦ by simp [inv_lt_inv₀ (hg _ hj) (hg _ hi)]

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrderedSemifield α
inst✝ : LinearOrderedSemifield β
s : Set ι
f : ι → α
g : ι → β
hg : ∀ i ∈ s, 0 < g i
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
⊢ g⁻¹ j < g⁻¹ i → f i ≤ f j ↔ g i < g j → f i ≤ f j

Tactic:
simp [inv_lt_inv₀ (hg _ hj) (hg _ hi)]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
lemma image_compl_eq_range_diff_image {f : α → β} (hf : Injective f) (s : Set α) :
    f '' sᶜ = range f \ f '' s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ f '' sᶜ = range f \ f '' s

Tactic:
rw [← image_univ, ← image_diff hf, compl_eq_univ_diff]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/BigOperators.lean
theorem prod_factorial_pos : 0 < ∏ i ∈ s, (f i)!

Proof state:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ 0 < ∏ i ∈ s, (f i)!

Tactic:
positivity

Result:
no goals
-- Mathlib/RingTheory/Perfection.lean
theorem coeff_iterate_frobenius (f : Ring.Perfection R p) (n m : ℕ) :
    coeff R p (n + m) ((frobenius _ p)^[m] f) = coeff R p n f :=
  Nat.recOn m rfl fun m ih => by erw [Function.iterate_succ_apply', coeff_frobenius, ih]

Proof state:
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Ring.Perfection R p
n m✝ m : ℕ
ih : (coeff R p (n + m)) ((⇑(frobenius (Ring.Perfection R p) p))^[m] f) = (coeff R p n) f
⊢ (coeff R p (n + m.succ)) ((⇑(frobenius (Ring.Perfection R p) p))^[m.succ] f) = (coeff R p n) f

Tactic:
erw [Function.iterate_succ_apply', coeff_frobenius, ih]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem infEdist_inv_inv (x : E) (s : Set E) : infEdist x⁻¹ s⁻¹ = infEdist x s

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
x : E
s : Set E
⊢ infEdist x⁻¹ s⁻¹ = infEdist x s

Tactic:
rw [← image_inv_eq_inv, infEdist_image isometry_inv]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
theorem mlieBracketWithin_of_mem_nhds (h : s ∈ 𝓝 x) :
    mlieBracketWithin I V W s x = mlieBracket I V W x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
h : s ∈ 𝓝 x
⊢ mlieBracketWithin I V W s x = mlieBracket I V W x

Tactic:
rw [← mlieBracketWithin_univ, ← univ_inter s, mlieBracketWithin_inter h]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_cancel (a : M) (b c : S) :
    f.mk' (a * c) (b * c) = f.mk' a b :=
  mk'_eq_of_eq' f (by rw [Submonoid.coe_mul, mul_comm (b : M), mul_assoc])

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a : M
b c : ↥S
⊢ a * ↑(b * c) = a * ↑c * ↑b

Tactic:
rw [Submonoid.coe_mul, mul_comm (b : M), mul_assoc]

Result:
no goals
-- Mathlib/Data/PNat/Interval.lean
theorem card_uIcc : #(uIcc a b) = (b - a : ℤ).natAbs + 1

Proof state:
a b : ℕ+
⊢ #(uIcc a b) = (↑↑b - ↑↑a).natAbs + 1

Tactic:
rw [← Nat.card_uIcc, ← map_subtype_embedding_uIcc, card_map]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Ideal.lean
@[simp]
lemma mem_matricesOver (I : TwoSidedIdeal R) (M : Matrix n n R) :
    M ∈ I.matricesOver n ↔ ∀ i j, M i j ∈ I

Proof state:
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
I : TwoSidedIdeal R
M : Matrix n n R
⊢ M ∈ matricesOver n I ↔ ∀ (i j : n), M i j ∈ I

Tactic:
simp [matricesOver]

Result:
no goals
-- Mathlib/Analysis/Quaternion.lean
theorem coeComplex_mul (z w : ℂ) : ↑(z * w) = (z * w : ℍ)

Proof state:
z w : ℂ
⊢ ↑(z * w) = ↑z * ↑w

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem succ_lt_succ_iff_of_not_isMax (ha : ¬IsMax a) (hb : ¬IsMax b) :
    succ a < succ b ↔ a < b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ succ a < succ b ↔ a < b

Tactic:
rw [lt_succ_iff_of_not_isMax hb, succ_le_iff_of_not_isMax ha]

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_add_int [AddGroupWithOne G] [AddGroupWithOne H] [AddConstMapClass F G H 1 1]
    (f : F) (x : G) (n : ℤ) : f (x + n) = f x + n

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroupWithOne H
inst✝ : AddConstMapClass F G H 1 1
f : F
x : G
n : ℤ
⊢ f (x + ↑n) = f x + ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
theorem mul_self_sub_mul_self_eq [NonUnitalNonAssocRing R] {a b : R} (h : Commute a b) :
    a * a - b * b = (a + b) * (a - b)

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = (a + b) * (a - b)

Tactic:
rw [add_mul, mul_sub, mul_sub, h.eq, sub_add_sub_cancel]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem map_eq (s : Stream' α) : map f s = f (head s)::map f (tail s)

Proof state:
α : Type u
β : Type v
f : α → β
s : Stream' α
⊢ map f s = f s.head :: map f s.tail

Tactic:
rw [← Stream'.eta (map f s), tail_map, head_map]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem finrank_eq_rank [Module.Finite R M] : ↑(finrank R M) = Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ ↑(finrank R M) = Module.rank R M

Tactic:
rw [Module.finrank, cast_toNat_of_lt_aleph0 (rank_lt_aleph0 R M)]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem deleteVerts_le : G'.deleteVerts s ≤ G'

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ G'.deleteVerts s ≤ G'

Tactic:
constructor <;> simp [Set.diff_subset]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
@[simp]
lemma leadingCoeff_preΨ {n : ℤ} (h : (n : R) ≠ 0) :
    (W.preΨ n).leadingCoeff = if Even n then n / 2 else n

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
h : ↑n ≠ 0
⊢ (W.preΨ n).leadingCoeff = ↑(if Even n then n / 2 else n)

Tactic:
rw [leadingCoeff, W.natDegree_preΨ h, coeff_preΨ]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem map_powers {N : Type*} {F : Type*} [Monoid N] [FunLike F M N] [MonoidHomClass F M N]
    (f : F) (m : M) :
    (powers m).map f = powers (f m)

Proof state:
M : Type u_1
inst✝³ : Monoid M
N : Type u_4
F : Type u_5
inst✝² : Monoid N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
m : M
⊢ map f (powers m) = powers (f m)

Tactic:
simp only [powers_eq_closure, map_mclosure f, Set.image_singleton]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isDetector_op_iff (G : C) : IsDetector (op G) ↔ IsCodetector G

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ IsDetector (op G) ↔ IsCodetector G

Tactic:
rw [IsDetector, IsCodetector, ← isDetecting_op_iff, Set.singleton_op]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tanh_neg : tanh (-x) = -tanh x

Proof state:
x : ℝ
⊢ tanh (-x) = -tanh x

Tactic:
simp [tanh, neg_div]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem IsPrimitive.mul {p q : R[X]} (hp : p.IsPrimitive) (hq : q.IsPrimitive) :
    (p * q).IsPrimitive

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ (p * q).IsPrimitive

Tactic:
rw [isPrimitive_iff_content_eq_one, content_mul, hp.content_eq_one, hq.content_eq_one, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l H₁ H₂) :
    pmap f (pmap g l H₁) H₂ =
      pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
        (fun a _ => H₁ a a.2)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
q : β → Prop
g : (a : α) → p a → β
f : (b : β) → q b → γ
l : List α
H₁ : ∀ (a : α), a ∈ l → p a
H₂ : ∀ (a : β), a ∈ pmap g l H₁ → q a
⊢ pmap f (pmap g l H₁) H₂ = pmap (fun a h => f (g a.val h) ⋯) l.attach ⋯

Tactic:
simp [pmap_eq_map_attach, attach_map]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_neg_id (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
a : A
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => -x) a = -a

Tactic:
rw [cfc_neg _ a, cfc_id' R a]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Raw.lean
theorem WF.filter [BEq α] [Hashable α] {m : Raw α β} {f : (a : α) → β a → Bool} (h : m.WF) :
    (m.filter f).WF

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
f : (a : α) → β a → Bool
h : m.WF
⊢ (Raw.filter f m).WF

Tactic:
simpa [Raw.filter, h.size_buckets_pos] using .filter₀ h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem WalkingParallelPairHom.assoc {X Y Z W : WalkingParallelPair}
    (f : WalkingParallelPairHom X Y) (g : WalkingParallelPairHom Y Z)
    (h : WalkingParallelPairHom Z W) : comp (comp f g) h = comp f (comp g h)

Proof state:
X Y Z W : WalkingParallelPair
f : WalkingParallelPairHom X Y
g : WalkingParallelPairHom Y Z
h : WalkingParallelPairHom Z W
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
cases f <;> cases g <;> cases h <;> rfl

Result:
no goals
-- Mathlib/Tactic/Abel.lean
theorem term_atom_pfg {α} [AddCommGroup α] (x x' : α) (h : x = x') : x = termg 1 x' 0

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
x x' : α
h : x = x'
⊢ x = termg 1 x' 0

Tactic:
simp [termg, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_toList_iff (a : α) (l : Array α) : a ∈ l.toList ↔ a ∈ l

Proof state:
α : Type u_1
a : α
l : Array α
⊢ a ∈ l.toList ↔ a ∈ l

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
    (h : m.WF) : Const.get? (Const.alter m k f) k = f (Const.get? m k)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
h : m.WF
⊢ get? (alter m k f) k = f (get? m k)

Tactic:
simp [get?_alter h]

Result:
no goals
-- Mathlib/Order/RelClasses.lean
theorem not_unbounded_iff {r : α → α → Prop} (s : Set α) : ¬Unbounded r s ↔ Bounded r s

Proof state:
α : Type u
r : α → α → Prop
s : Set α
⊢ ¬Unbounded r s ↔ Bounded r s

Tactic:
rw [not_iff_comm, not_bounded_iff]

Result:
no goals
-- Mathlib/Algebra/Order/AddGroupWithTop.lean
theorem top_sub {a : WithTop α} : (⊤ : WithTop α) - a = ⊤

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : WithTop α
⊢ ⊤ - a = ⊤

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem tensorLeftHomEquiv_tensor {X X' Y Y' Z Z' : C} [ExactPairing Y Y'] (f : X ⟶ Y ⊗ Z)
    (g : X' ⟶ Z') :
    (tensorLeftHomEquiv (X ⊗ X') Y Y' (Z ⊗ Z')).symm ((f ⊗ g) ≫ (α_ _ _ _).hom) =
      (α_ _ _ _).inv ≫ ((tensorLeftHomEquiv X Y Y' Z).symm f ⊗ g)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y Y' Z Z' : C
inst✝ : ExactPairing Y Y'
f : X ⟶ Y ⊗ Z
g : X' ⟶ Z'
⊢ (tensorLeftHomEquiv (X ⊗ X') Y Y' (Z ⊗ Z')).symm ((f ⊗ g) ≫ (α_ Y Z Z').hom) =
    (α_ Y' X X').inv ≫ ((tensorLeftHomEquiv X Y Y' Z).symm f ⊗ g)

Tactic:
simp [tensorLeftHomEquiv, tensorHom_def']

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem zero_div {a : R} : 0 / a = 0 :=
  by_cases (fun a0 : a = 0 => a0.symm ▸ div_zero 0) fun a0 => by
    simpa only [zero_mul] using mul_div_cancel_right₀ 0 a0

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a : R
a0 : ¬a = 0
⊢ 0 / a = 0

Tactic:
simpa only [zero_mul] using mul_div_cancel_right₀ 0 a0

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/VectorSpace.lean
theorem range_ofSpan (hs : ⊤ ≤ span K s) :
    range (ofSpan hs) = (linearIndepOn_empty K id).extend (empty_subset s)

Proof state:
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
hs : ⊤ ≤ span K s
⊢ range ⇑(ofSpan hs) = ⋯.extend ⋯

Tactic:
rw [coe_ofSpan, Subtype.range_coe_subtype, setOf_mem_eq]

Result:
no goals