harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/SModEq.lean
lemma zsmul (hxy : x ≡ y [SMOD U]) (n : ℤ) : n • x ≡ n • y [SMOD U]

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : x ≡ y [SMOD U]
n : ℤ
⊢ n • x ≡ n • y [SMOD U]

Tactic:
rw [SModEq.def] at hxy ⊢

Result:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : Submodule.Quotient.mk x = Submodule.Quotient.mk y
n : ℤ
⊢ Submodule.Quotient.mk (n • x) = Submodule.Quotient.mk (n • y)

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : Submodule.Quotient.mk x = Submodule.Quotient.mk y
n : ℤ
⊢ Submodule.Quotient.mk (n • x) = Submodule.Quotient.mk (n • y)

Tactic:
simp_rw [Quotient.mk_smul, hxy]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Vector/Monadic.lean
theorem mapFinIdxM_mk [Monad m] [LawfulMonad m] [MonadSatisfying m]
    (a : Array α) (h : a.size = n) (f : (i : Nat) → α → (h : i < n) → m β) :
    (Vector.mk a h).mapFinIdxM f =
      (fun ⟨a, h'⟩ => Vector.mk a (h'.trans h)) <$> satisfying
        (Array.size_mapFinIdxM a (fun i a h' => f i a (h ▸ h')))

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : MonadSatisfying m
a : Array α
h : a.size = n
f : (i : Nat) → α → i < n → m β
⊢ { toArray := a, size_toArray := h }.mapFinIdxM f =
    (fun x =>
        match x with
        | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$>
      satisfying ⋯

Tactic:
rw [← LawfulMonad.map_inj_right Vector.toArray_inj.mp]

Result:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : MonadSatisfying m
a : Array α
h : a.size = n
f : (i : Nat) → α → i < n → m β
⊢ (fun {x} => x.toArray) <$> { toArray := a, size_toArray := h }.mapFinIdxM f =
    (fun {x} => x.toArray) <$>
      (fun x =>
          match x with
          | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$>
        satisfying ⋯

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : MonadSatisfying m
a : Array α
h : a.size = n
f : (i : Nat) → α → i < n → m β
⊢ (fun {x} => x.toArray) <$> { toArray := a, size_toArray := h }.mapFinIdxM f =
    (fun {x} => x.toArray) <$>
      (fun x =>
          match x with
          | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$>
        satisfying ⋯

Tactic:
simp only [Functor.map_map, MonadSatisfying.val_eq, toArray_mapFinIdxM]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean
lemma preservesZeroMorphisms_of_iso {F₁ F₂ : C ⥤ D} [F₁.PreservesZeroMorphisms] (e : F₁ ≅ F₂) :
    F₂.PreservesZeroMorphisms where
  map_zero X Y

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F₁ F₂ : C ⥤ D
inst✝ : F₁.PreservesZeroMorphisms
e : F₁ ≅ F₂
X Y : C
⊢ F₂.map 0 = 0

Tactic:
simp only [← cancel_epi (e.hom.app X), ← e.hom.naturality,
F₁.map_zero, zero_comp, comp_zero]

Result:
no goals
-- Mathlib/Probability/Kernel/CondDistrib.lean
theorem _root_.MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff
    (hY : AEMeasurable Y μ) (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) :
    (∀ᵐ a ∂μ.map X, Integrable (fun ω => f (a, ω)) (condDistrib Y X μ a)) ∧
      Integrable (fun a => ∫ ω, ‖f (a, ω)‖ ∂condDistrib Y X μ a) (μ.map X) ↔
    Integrable f (μ.map fun a => (X a, Y a))

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ (∀ᵐ (a : β) ∂Measure.map X μ, Integrable (fun ω => f (a, ω)) ((condDistrib Y X μ) a)) ∧
      Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂(condDistrib Y X μ) a) (Measure.map X μ) ↔
    Integrable f (Measure.map (fun a => (X a, Y a)) μ)

Tactic:
rw [condDistrib, ← hf.ae_integrable_condKernel_iff, Measure.fst_map_prod_mk₀ hY]

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ico_succ_right_eq_Icc_of_not_isMax (hb : ¬ IsMax b) (a : α) : Ico a (succ b) = Icc a b :=
  coe_injective <| by simpa using Set.Ico_succ_right_eq_Icc_of_not_isMax hb _

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ ↑(Ico a (succ b)) = ↑(Icc a b)

Tactic:
simpa using Set.Ico_succ_right_eq_Icc_of_not_isMax hb _

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem mem_nonunits {z : ℤ_[p]} : z ∈ nonunits ℤ_[p] ↔ ‖z‖ < 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ z ∈ nonunits ℤ_[p] ↔ ‖z‖ < 1

Tactic:
rw [lt_iff_le_and_ne]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ z ∈ nonunits ℤ_[p] ↔ ‖z‖ ≤ 1 ∧ ‖z‖ ≠ 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ z ∈ nonunits ℤ_[p] ↔ ‖z‖ ≤ 1 ∧ ‖z‖ ≠ 1

Tactic:
simp [norm_le_one z, nonunits, isUnit_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldl_add_const (l : List α) (a b : Nat) :
    l.foldl (fun x _ => x + a) b = b + a * l.length

Proof state:
case cons
α : Type u_1
a : Nat
y : α
l : List α
ih : ∀ (b : Nat), foldl (fun x x_1 => x + a) b l = b + a * l.length
b : Nat
⊢ foldl (fun x x_1 => x + a) b (y :: l) = b + a * (y :: l).length

Tactic:
simp only [foldl_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc,
  Nat.add_comm a]

Result:
no goals

Proof state:
α : Type u_1
l : List α
a b : Nat
⊢ foldl (fun x x_1 => x + a) b l = b + a * l.length

Tactic:
induction l generalizing b with
| nil => simp
| cons y l ih =>
  simp only [foldl_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc,
    Nat.add_comm a]

Result:
no goals

Proof state:
case nil
α : Type u_1
a b : Nat
⊢ foldl (fun x x_1 => x + a) b [] = b + a * [].length

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.toMatrix₂_basisFun :
    LinearMap.toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) =
    LinearMap.toMatrix₂' R (N₂ := N₂)

Proof state:
case h.a
R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
B : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂
i✝ : n
j✝ : m
⊢ (toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m)) B i✝ j✝ = (toMatrix₂' R) B i✝ j✝

Tactic:
rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂'_apply, Pi.basisFun_apply, Pi.basisFun_apply]

Result:
no goals

Proof state:
R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
⊢ toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) = toMatrix₂' R

Tactic:
ext B

Result:
case h.a
R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
B : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂
i✝ : n
j✝ : m
⊢ (toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m)) B i✝ j✝ = (toMatrix₂' R) B i✝ j✝
-- Mathlib/Probability/Kernel/Composition/Prod.lean
theorem id_prod_apply' (κ : Kernel α β) [IsSFiniteKernel κ] (a : α) {s : Set (α × β)}
    (hs : MeasurableSet s) : (Kernel.id ×ₖ κ) a s = κ a (Prod.mk a ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a : α
s : Set (α × β)
hs : MeasurableSet s
⊢ ((Kernel.id ×ₖ κ) a) s = (κ a) (Prod.mk a ⁻¹' s)

Tactic:
rw [Kernel.id, deterministic_prod_apply' _ _ _ hs, id_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/AbsoluteValue.lean
theorem det_sum_le {ι : Type*} (s : Finset ι) {A : ι → Matrix n n R} {abv : AbsoluteValue R S}
    {x : S} (hx : ∀ k i j, abv (A k i j) ≤ x) :
    abv (det (∑ k ∈ s, A k)) ≤
      Nat.factorial (Fintype.card n) • (#s• x) ^ Fintype.card n :=
  det_le fun i j =>
    calc
      abv ((∑ k ∈ s, A k) i j) = abv (∑ k ∈ s, A k i j)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
ι : Type u_4
s : Finset ι
A : ι → Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (k : ι) (i j : n), abv (A k i j) ≤ x
i j : n
⊢ abv ((∑ k ∈ s, A k) i j) = abv (∑ k ∈ s, A k i j)

Tactic:
simp only [sum_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_filter [LawfulBEq α] (f : α → Bool) (l : Array α) :
    (filter f l).erase a = filter f (l.erase a)

Proof state:
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
l : Array α
⊢ (filter f l).erase a = filter f (l.erase a)

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
l : List α
⊢ (filter f { toList := l }).erase a = filter f ({ toList := l }.erase a)

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
f : α → Bool
l : List α
⊢ (filter f { toList := l }).erase a = filter f ({ toList := l }.erase a)

Tactic:
simpa using List.erase_filter f l

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₈_of_isCharTwoJNeZeroNF_of_char_two : W.b₈ = W.a₆

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ W.b₈ = W.a₆

Tactic:
rw [b₈_of_isCharTwoJNeZeroNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ W.a₆ + 4 * W.a₂ * W.a₆ = W.a₆

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ W.a₆ + 4 * W.a₂ * W.a₆ = W.a₆

Tactic:
linear_combination 2 * W.a₂ * W.a₆ * CharP.cast_eq_zero R 2

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem nhdsWithin_Ioi_neBot' {a b : α} (H₁ : (Ioi a).Nonempty) (H₂ : a ≤ b) :
    NeBot (𝓝[Ioi a] b) :=
  mem_closure_iff_nhdsWithin_neBot.1 <| by rwa [closure_Ioi' H₁]

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
H₁ : (Ioi a).Nonempty
H₂ : a ≤ b
⊢ b ∈ closure (Ioi a)

Tactic:
rwa [closure_Ioi' H₁]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem group_inseparable_iff {x y : G} : Inseparable x y ↔ x / y ∈ closure (1 : Set G)

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ Inseparable ((Homeomorph.mulRight y⁻¹) x) ((Homeomorph.mulRight y⁻¹) y) ↔ Inseparable (x / y) 1

Tactic:
simp [div_eq_mul_inv]

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ Inseparable x y ↔ x / y ∈ closure 1

Tactic:
rw [← singleton_one, ← specializes_iff_mem_closure, specializes_comm, specializes_iff_inseparable,
  ← (Homeomorph.mulRight y⁻¹).isEmbedding.inseparable_iff]

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ Inseparable ((Homeomorph.mulRight y⁻¹) x) ((Homeomorph.mulRight y⁻¹) y) ↔ Inseparable (x / y) 1
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ioo_succ_right_of_not_isMax (hb : ¬IsMax b) : Ioo a (succ b) = Ioc a b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ioo a (succ b) = Ioc a b

Tactic:
rw [← Ioi_inter_Iio, Iio_succ_of_not_isMax hb, Ioi_inter_Iic]

Result:
no goals
-- Mathlib/Data/W/Cardinal.lean
theorem cardinalMk_eq_sum : #(WType β) = sum (fun a : α => #(WType β) ^ #(β a)) :=
  cardinalMk_eq_sum_lift.trans <| by simp_rw [lift_id]

Proof state:
α : Type u
β : α → Type u
⊢ (sum fun a => #(WType β) ^ lift.{u, u} #(β a)) = sum fun a => #(WType β) ^ #(β a)

Tactic:
simp_rw [lift_id]

Result:
no goals
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem trop_sInf_image [ConditionallyCompleteLinearOrder R] (s : Finset S) (f : S → WithTop R) :
    trop (sInf (f '' s)) = ∑ i ∈ s, trop (f i)

Proof state:
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
⊢ trop (sInf (f '' ↑s)) = ∑ i ∈ s, trop (f i)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | h)

Result:
case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → WithTop R
⊢ trop (sInf (f '' ↑∅)) = ∑ i ∈ ∅, trop (f i)

case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
h : s.Nonempty
⊢ trop (sInf (f '' ↑s)) = ∑ i ∈ s, trop (f i)

Proof state:
case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
h : s.Nonempty
⊢ trop (sInf (f '' ↑s)) = ∑ i ∈ s, trop (f i)

Tactic:
rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, s.trop_inf]

Result:
no goals

Proof state:
case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → WithTop R
⊢ trop (sInf (f '' ↑∅)) = ∑ i ∈ ∅, trop (f i)

Tactic:
simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, trop_top]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem HasFTaylorSeriesUpTo.hasFDerivAt (h : HasFTaylorSeriesUpTo n f p) (hn : 1 ≤ n) (x : E) :
    HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
hn : 1 ≤ n
x : E
⊢ HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) x

Tactic:
rw [← hasFDerivWithinAt_univ]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
hn : 1 ≤ n
x : E
⊢ HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) univ x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
hn : 1 ≤ n
x : E
⊢ HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) univ x

Tactic:
exact (hasFTaylorSeriesUpToOn_univ_iff.2 h).hasFDerivWithinAt hn (mem_univ _)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem parent_link {self} {x y : Fin self.size} (yroot) {i} :
    (link self x y yroot).parent i =
    if x.1 = y then
      self.parent i
    else
      if self.rank y < self.rank x then
        if y = i then x else self.parent i
      else
        if x = i then y else self.parent i

Proof state:
self : UnionFind
x y : Fin self.size
yroot : self.parent ↑y = ↑y
i : Nat
⊢ (self.link x y yroot).parent i =
    if ↑x = ↑y then self.parent i
    else
      if self.arr[↑y].rank < self.arr[↑x].rank then if ↑y = i then ↑x else self.parent i
      else if ↑x = i then ↑y else self.parent i

Tactic:
exact parentD_linkAux

Result:
no goals

Proof state:
self : UnionFind
x y : Fin self.size
yroot : self.parent ↑y = ↑y
i : Nat
⊢ (self.link x y yroot).parent i =
    if ↑x = ↑y then self.parent i
    else
      if self.rank ↑y < self.rank ↑x then if ↑y = i then ↑x else self.parent i else if ↑x = i then ↑y else self.parent i

Tactic:
simp [rankD_eq]

Result:
self : UnionFind
x y : Fin self.size
yroot : self.parent ↑y = ↑y
i : Nat
⊢ (self.link x y yroot).parent i =
    if ↑x = ↑y then self.parent i
    else
      if self.arr[↑y].rank < self.arr[↑x].rank then if ↑y = i then ↑x else self.parent i
      else if ↑x = i then ↑y else self.parent i
-- Mathlib/Algebra/Free.lean
theorem hom_ext {β : Type v} [Mul β] {f g : FreeSemigroup α →ₙ* β} (h : f ∘ of = g ∘ of) : f = g :=
  (DFunLike.ext _ _) fun x ↦
    FreeSemigroup.recOnMul x (congr_fun h) fun x y hx hy ↦ by simp only [map_mul, *]

Proof state:
α : Type u
β : Type v
inst✝ : Mul β
f g : FreeSemigroup α →ₙ* β
h : ⇑f ∘ of = ⇑g ∘ of
x✝ : FreeSemigroup α
x : α
y : FreeSemigroup α
hx : f (of x) = g (of x)
hy : f y = g y
⊢ f (of x * y) = g (of x * y)

Tactic:
simp only [map_mul, *]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_mul_left_add_right (m n k : ℕ) : Coprime m (m * k + n) ↔ Coprime m n

Proof state:
m n k : ℕ
⊢ m.Coprime (m * k + n) ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_mul_left_add_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem getElem_eraseIdx (l : Vector α n) (i : Nat) (h : i < n) (j : Nat) (h' : j < n - 1) :
    (l.eraseIdx i)[j] = if h'' : j < i then l[j] else l[j + 1]

Proof state:
case x
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h' : j < n - 1
⊢ (if j < i then l[j]? else l[j + 1]?) = some (if h'' : j < i then l[j] else l[j + 1])

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h' : j < n - 1
⊢ (l.eraseIdx i h)[j] = if h'' : j < i then l[j] else l[j + 1]

Tactic:
apply Option.some.inj

Result:
case x
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h' : j < n - 1
⊢ some (l.eraseIdx i h)[j] = some (if h'' : j < i then l[j] else l[j + 1])

Proof state:
case x
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h' : j < n - 1
⊢ some (l.eraseIdx i h)[j] = some (if h'' : j < i then l[j] else l[j + 1])

Tactic:
rw [← getElem?_eq_getElem, getElem?_eraseIdx]

Result:
case x
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h' : j < n - 1
⊢ (if j < i then l[j]? else l[j + 1]?) = some (if h'' : j < i then l[j] else l[j + 1])
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.not_neg' (x : BitVec w) : ~~~(x + 1#w) = ~~~x + -1#w

Proof state:
w : Nat
x : BitVec w
⊢ ~~~(~~~~~~x + 1#w) = ~~~~~~~~~x + -1#w

Tactic:
rw [BitVec.not_neg]

Result:
w : Nat
x : BitVec w
⊢ ~~~x + -1#w = ~~~~~~~~~x + -1#w

Proof state:
w : Nat
x : BitVec w
⊢ ~~~(x + 1#w) = ~~~x + -1#w

Tactic:
rw [← BitVec.not_not (b := x)]

Result:
w : Nat
x : BitVec w
⊢ ~~~(~~~~~~x + 1#w) = ~~~~~~~~~x + -1#w

Proof state:
w : Nat
x : BitVec w
⊢ ~~~x + -1#w = ~~~~~~~~~x + -1#w

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_Prop : #Prop = 2

Proof state:
⊢ #Prop = 2

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem log_eq_zero_iff {b n : ℕ} : log b n = 0 ↔ n < b ∨ b ≤ 1

Proof state:
b n : ℕ
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

Tactic:
rw [log, dite_eq_right_iff]

Result:
b n : ℕ
⊢ b ≤ n ∧ 1 < b → log b (n / b) + 1 = 0 ↔ n < b ∨ b ≤ 1

Proof state:
b n : ℕ
⊢ b ≤ n ∧ 1 < b → log b (n / b) + 1 = 0 ↔ n < b ∨ b ≤ 1

Tactic:
simp only [Nat.add_eq_zero_iff, Nat.one_ne_zero, and_false, imp_false, not_and_or, not_le, not_lt]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem divisors_zero : divisors 0 = ∅

Proof state:
⊢ divisors 0 = ∅

Tactic:
ext

Result:
case h
a✝ : ℕ
⊢ a✝ ∈ divisors 0 ↔ a✝ ∈ ∅

Proof state:
case h
a✝ : ℕ
⊢ a✝ ∈ divisors 0 ↔ a✝ ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Units/Basic.lean
theorem NumberField.isUnit_iff_norm [NumberField K] {x : 𝓞 K} :
    IsUnit x ↔ |(RingOfIntegers.norm ℚ x : ℚ)| = 1

Proof state:
case h.e'_2.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
⊢ |↑((RingOfIntegers.norm ℚ) x)| = 1 ↔ IsUnit ((RingOfIntegers.norm ℚ) x)

Tactic:
rw [← abs_one, abs_eq_abs, ← Rat.RingOfIntegers.isUnit_iff]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
⊢ IsUnit x ↔ |↑((RingOfIntegers.norm ℚ) x)| = 1

Tactic:
convert (RingOfIntegers.isUnit_norm ℚ (F := K)).symm

Result:
case h.e'_2.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
⊢ |↑((RingOfIntegers.norm ℚ) x)| = 1 ↔ IsUnit ((RingOfIntegers.norm ℚ) x)
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem norm_pow_le' (a : α) {n : ℕ} (h : 0 < n) : ‖a ^ n‖ ≤ ‖a‖ ^ n

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a : α
n : ℕ
h : 0 < n
⊢ ‖a ^ n‖ ≤ ‖a‖ ^ n

Tactic:
simpa only [NNReal.coe_pow, coe_nnnorm] using NNReal.coe_mono (nnnorm_pow_le' a h)

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean
theorem lift_commutes {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y)
    (Q : ProjectiveResolution Z) : lift f P Q ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f

Proof state:
case hfg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ (lift f P Q ≫ Q.π).f 0 = (P.π ≫ (ChainComplex.single₀ C).map f).f 0

Tactic:
simp [lift, liftFZero, liftFOne]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ lift f P Q ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f

Tactic:
ext

Result:
case hfg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ (lift f P Q ≫ Q.π).f 0 = (P.π ≫ (ChainComplex.single₀ C).map f).f 0
-- Mathlib/Analysis/RCLike/Basic.lean
theorem ofNat_mul_re (n : ℕ) [n.AtLeastTwo] (z : K) :
    re (ofNat(n) * z) = ofNat(n) * re z

Proof state:
K : Type u_1
inst✝¹ : RCLike K
n : ℕ
inst✝ : n.AtLeastTwo
z : K
⊢ re (OfNat.ofNat n * z) = OfNat.ofNat n * re z

Tactic:
rw [← ofReal_ofNat, re_ofReal_mul]

Result:
no goals
-- Mathlib/Tactic/NormNum/Pow.lean
theorem intPow_negOfNat_bit0 {b' c' : ℕ} (h1 : Nat.pow a b' = c')
    (hb : nat_lit 2 * b' = b) (hc : c' * c' = c) :
    Int.pow (Int.negOfNat a) b = Int.ofNat c

Proof state:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' = Int.ofNat (a.pow b' * a.pow b')

Tactic:
simp

Result:
no goals

Proof state:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ (Int.negOfNat a).pow b = Int.ofNat c

Tactic:
rw [← hb, Int.negOfNat_eq, Int.pow_eq, pow_mul, neg_pow_two, ← pow_mul, two_mul, pow_add, ← hc,
  ← h1]

Result:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' = Int.ofNat (a.pow b' * a.pow b')
-- Mathlib/Algebra/Polynomial/Degree/Domain.lean
lemma not_dvd_of_degree_lt (h0 : q ≠ 0) (hl : q.degree < p.degree) : ¬p ∣ q

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.degree < p.degree
hcontra : p ∣ q
⊢ False

Tactic:
exact h0 (eq_zero_of_dvd_of_degree_lt hcontra hl)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.degree < p.degree
⊢ ¬p ∣ q

Tactic:
by_contra hcontra

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.degree < p.degree
hcontra : p ∣ q
⊢ False
-- Mathlib/Data/Matrix/Diagonal.lean
theorem diagonal_neg [NegZeroClass α] (d : n → α) :
    -diagonal d = diagonal fun i => -d i

Proof state:
case a
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : NegZeroClass α
d : n → α
i j : n
⊢ (-diagonal d) i j = diagonal (fun i => -d i) i j

Tactic:
by_cases h : i = j <;>
simp [h]

Result:
no goals

Proof state:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : NegZeroClass α
d : n → α
⊢ -diagonal d = diagonal fun i => -d i

Tactic:
ext i j

Result:
case a
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : NegZeroClass α
d : n → α
i j : n
⊢ (-diagonal d) i j = diagonal (fun i => -d i) i j
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
theorem Bool.neg_to_not (a : Bool) : (¬a) = ((!a) = true)

Proof state:
a : Bool
⊢ (¬a = true) = ((!a) = true)

Tactic:
simp

Result:
no goals