harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/ModEq.lean
lemma modEq_sub (h : b ≤ a) : a ≡ b [MOD a - b] := (modEq_of_dvd <| by rw [Int.ofNat_sub h]).symm

Proof state:
a b : ℕ
h : b ≤ a
⊢ ↑(a - b) ∣ ↑a - ↑b

Tactic:
rw [Int.ofNat_sub h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.and_assoc (a b c : Bool) : (a && b && c) = (a && (b && c))

Proof state:
a b c : Bool
⊢ (a && b && c) = (a && (b && c))

Tactic:
cases a <;> cases b <;> cases c <;> decide

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem mul_inverse_cancel_right (x y : M₀) (h : IsUnit x) : y * x * inverse x = y

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ y * x * inverse x = y

Tactic:
rw [mul_assoc, mul_inverse_cancel x h, mul_one]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma succAbove_eq_zero_iff [NeZero n] {a : Fin (n + 1)} {b : Fin n} (ha : a ≠ 0) :
    a.succAbove b = 0 ↔ b = 0

Proof state:
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
b : Fin n
ha : a ≠ 0
⊢ a.succAbove b = 0 ↔ b = 0

Tactic:
rw [← succAbove_ne_zero_zero ha, succAbove_right_inj]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
lemma norm_eq_sqrt_sq_add_sq (z : ℂ) : ‖z‖ = (z.re ^ 2 + z.im ^ 2).sqrt

Proof state:
z : ℂ
⊢ ‖z‖ = √(z.re ^ 2 + z.im ^ 2)

Tactic:
rw [norm_def, normSq_apply, sq, sq]

Result:
no goals
-- Mathlib/Order/Fin/Tuple.lean
lemma preimage_insertNth_Icc_of_not_mem {i : Fin (n + 1)} {x : α i} {q₁ q₂ : ∀ j, α j}
    (hx : x ∉ Icc (q₁ i) (q₂ i)) : i.insertNth x ⁻¹' Icc q₁ q₂ = ∅ :=
  Set.ext fun p ↦ by
    simp only [mem_preimage, insertNth_mem_Icc, hx, false_and, mem_empty_iff_false]

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
q₁ q₂ : (j : Fin (n + 1)) → α j
hx : x ∉ Icc (q₁ i) (q₂ i)
p : (j : Fin n) → α (i.succAbove j)
⊢ p ∈ i.insertNth x ⁻¹' Icc q₁ q₂ ↔ p ∈ ∅

Tactic:
simp only [mem_preimage, insertNth_mem_Icc, hx, false_and, mem_empty_iff_false]

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma ext₁ {F G : ComposableArrows C 1}
    (left : F.left = G.left) (right : F.right = G.right)
    (w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom right.symm) : F = G :=
  Functor.ext_of_iso (isoMk₁ (eqToIso left) (eqToIso right) (by simp [map'_eq_hom₁, w]))
    (fun i => by fin_cases i <;> assumption)
    (fun i => by fin_cases i <;> rfl)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
i : Fin (1 + 1)
⊢ F.obj i = G.obj i

Tactic:
fin_cases i <;> assumption

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
i : Fin (1 + 1)
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app i = eqToHom ⋯

Tactic:
fin_cases i <;> rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
⊢ F.map' 0 1 ⋯ ⋯ ≫ (eqToIso right).hom = (eqToIso left).hom ≫ G.map' 0 1 ⋯ ⋯

Tactic:
simp [map'_eq_hom₁, w]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem biUnion_range_preimage_singleton (f : α → β) : ⋃ y ∈ range f, f ⁻¹' {y} = univ

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ ⋃ y ∈ range f, f ⁻¹' {y} = univ

Tactic:
rw [biUnion_preimage_singleton, preimage_range]

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
@[simp]
lemma fromCols_toCols (A : Matrix m (n₁ ⊕ n₂) R) :
    fromCols A.toCols₁ A.toCols₂ = A

Proof state:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
⊢ A.toCols₁.fromCols A.toCols₂ = A

Tactic:
ext i (j | j) <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : k == a) :
    getKey? a (⟨k, v⟩ :: l) = some k

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : (k == a) = true
⊢ getKey? a (⟨k, v⟩ :: l) = some k

Tactic:
simp [h]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem sInf_toSubalgebra (S : Set (IntermediateField F E)) :
    (sInf S).toSubalgebra = sInf (toSubalgebra '' S) :=
  SetLike.coe_injective <| by simp [Set.sUnion_image]

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
⊢ ↑(sInf S).toSubalgebra = ↑(sInf (toSubalgebra '' S))

Tactic:
simp [Set.sUnion_image]

Result:
no goals
-- Mathlib/Order/Filter/Tendsto.lean
theorem tendsto_map'_iff {f : β → γ} {g : α → β} {x : Filter α} {y : Filter γ} :
    Tendsto f (map g x) y ↔ Tendsto (f ∘ g) x y

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
x : Filter α
y : Filter γ
⊢ Tendsto f (map g x) y ↔ Tendsto (f ∘ g) x y

Tactic:
rw [Tendsto, Tendsto, map_map]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Iic_sub_one_eq_Iio_of_not_isMin (hb : ¬ IsMin b) : Iic (b - 1) = Iio b

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
b : α
hb : ¬IsMin b
⊢ Iic (b - 1) = Iio b

Tactic:
simpa [pred_eq_sub_one] using Iic_pred_eq_Iio_of_not_isMin hb

Result:
no goals
-- Mathlib/RingTheory/Smooth/Kaehler.lean
lemma sectionOfRetractionKerToTensorAux_algebraMap (x : P) :
    sectionOfRetractionKerToTensorAux l hl σ hσ hf' (algebraMap P S x) = x - l (1 ⊗ₜ .D _ _ x) :=
  sectionOfRetractionKerToTensorAux_prop l hl _ x (by simp [hσ])

Proof state:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
x : P
⊢ (algebraMap P S) (σ ((algebraMap P S) x)) = (algebraMap P S) x

Tactic:
simp [hσ]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
theorem erase_lt {a : α} {s : Multiset α} : s.erase a < s ↔ a ∈ s :=
  ⟨fun h => not_imp_comm.1 erase_of_not_mem (ne_of_lt h), fun h => by
    simpa [h] using lt_cons_self (s.erase a) a⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ s.erase a < s

Tactic:
simpa [h] using lt_cons_self (s.erase a) a

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.inf_basis_neBot_iff (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
    NeBot (l ⊓ l') ↔ ∀ ⦃i⦄, p i → ∀ ⦃i'⦄, p' i' → (s i ∩ s' i').Nonempty :=
  (hl.inf' hl').neBot_iff.trans <| by simp [@forall_swap _ ι']

Proof state:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ (∀ {i : ι ×' ι'}, p i.fst ∧ p' i.snd → (s i.fst ∩ s' i.snd).Nonempty) ↔
    ∀ ⦃i : ι⦄, p i → ∀ ⦃i' : ι'⦄, p' i' → (s i ∩ s' i').Nonempty

Tactic:
simp [@forall_swap _ ι']

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem sum_restrict_of_ac (h : IsFundamentalDomain G s μ) (hν : ν ≪ μ) :
    (sum fun g : G => ν.restrict (g • s)) = ν

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
⊢ (sum fun g => ν.restrict (g • s)) = ν

Tactic:
rw [← restrict_iUnion_ae (h.aedisjoint.mono fun i j h => hν h) fun g =>
    (h.nullMeasurableSet_smul g).mono_ac hν,
  restrict_congr_set (hν h.iUnion_smul_ae_eq), restrict_univ]

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
/-- Given a tower of scalar actions `M → α → β`, if we use `SMul.comp`
to pull back both of `M`'s actions by a map `g : N → M`, then we obtain a new
tower of scalar actions `N → α → β`.

This cannot be an instance because it can cause infinite loops whenever the `SMul` arguments
are still metavariables. -/
@[to_additive
"Given a tower of additive actions `M → α → β`, if we use `SMul.comp` to pull back both of
`M`'s actions by a map `g : N → M`, then we obtain a new tower of scalar actions `N → α → β`.

This cannot be an instance because it can cause infinite loops whenever the `SMul` arguments
are still metavariables."]
lemma comp.isScalarTower [SMul M β] [SMul α β] [IsScalarTower M α β] (g : N → M) : by
    haveI := comp α g; haveI := comp β g; exact IsScalarTower N α β where
  __ := comp α g
  __ := comp β g
  smul_assoc n := smul_assoc (g n)

Proof state:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
this : SMul N α
⊢ Sort ?u.10024

Tactic:
haveI := comp β g

Result:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
this✝ : SMul N α
this : SMul N β
⊢ Sort ?u.10024

Proof state:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
⊢ Sort ?u.10024

Tactic:
haveI := comp α g

Result:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
this : SMul N α
⊢ Sort ?u.10024

Proof state:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
this✝ : SMul N α
this : SMul N β
⊢ Sort ?u.10024

Tactic:
exact IsScalarTower N α β

Result:
no goals
-- Mathlib/GroupTheory/Exponent.lean
theorem Group.exponent_dvd_sub_iff_zpow_eq_zpow :
    (Monoid.exponent G : ℤ) ∣ n - m ↔ ∀ g : G, g ^ n = g ^ m

Proof state:
G : Type u
inst✝ : Group G
n m : ℤ
⊢ ↑(Monoid.exponent G) ∣ n - m ↔ ∀ (g : G), g ^ n = g ^ m

Tactic:
simp_rw [Group.exponent_dvd_iff_forall_zpow_eq_one, zpow_sub, mul_inv_eq_one]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
lemma im_eq_zero (h : I = (0 : K)) (z : K) : im z = 0

Proof state:
K : Type u_1
inst✝ : RCLike K
h : I = 0
z : K
⊢ im (↑(re z) + ↑(im z) * 0) = 0

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
h : I = 0
z : K
⊢ im z = 0

Tactic:
rw [← re_add_im z, h]

Result:
K : Type u_1
inst✝ : RCLike K
h : I = 0
z : K
⊢ im (↑(re z) + ↑(im z) * 0) = 0
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem subset_negative_null_set (hu : MeasurableSet u) (hv : MeasurableSet v)
    (hw : MeasurableSet w) (hsu : s ≤[u] 0) (hw₁ : s w = 0) (hw₂ : w ⊆ u) (hwt : v ⊆ w) :
    s v = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : ↑s w = 0 → w ⊆ u → v ⊆ w → ↑s v = 0
⊢ ↑s v = 0

Tactic:
exact this hw₁ hw₂ hwt

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : s ≤[u] 0
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ ↑s v = 0

Tactic:
rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ ↑s v = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ ↑s v = 0

Tactic:
have := subset_positive_null_set hu hv hw hsu

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : ↑(-s) w = 0 → w ⊆ u → v ⊆ w → ↑(-s) v = 0
⊢ ↑s v = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : ↑(-s) w = 0 → w ⊆ u → v ⊆ w → ↑(-s) v = 0
⊢ ↑s v = 0

Tactic:
simp only [Pi.neg_apply, neg_eq_zero, coe_neg] at this

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hw₁ : ↑s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : ↑s w = 0 → w ⊆ u → v ⊆ w → ↑s v = 0
⊢ ↑s v = 0
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem C_mul_monomial : C a * monomial s a' = monomial s (a * a')

Proof state:
R : Type u
σ : Type u_1
a a' : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ C a * (monomial s) a' = (monomial s) (a * a')

Tactic:
show AddMonoidAlgebra.single _ _ * AddMonoidAlgebra.single _ _ = AddMonoidAlgebra.single _ _

Result:
R : Type u
σ : Type u_1
a a' : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ AddMonoidAlgebra.single 0 a * AddMonoidAlgebra.single s a' = AddMonoidAlgebra.single s (a * a')

Proof state:
R : Type u
σ : Type u_1
a a' : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ AddMonoidAlgebra.single 0 a * AddMonoidAlgebra.single s a' = AddMonoidAlgebra.single s (a * a')

Tactic:
simp [C_apply, single_mul_single]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/HomEquiv.lean
@[reassoc]
lemma homRestrict_comp_extendMap (ψ : K ⟶ L.extend e) (β : L ⟶ L') :
    e.homRestrict (ψ ≫ extendMap β e) =
      e.homRestrict ψ ≫ β

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L L' : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
β : L ⟶ L'
⊢ e.homRestrict (ψ ≫ extendMap β e) = e.homRestrict ψ ≫ β

Tactic:
ext i

Result:
case h
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L L' : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
β : L ⟶ L'
i : ι
⊢ (e.homRestrict (ψ ≫ extendMap β e)).f i = (e.homRestrict ψ ≫ β).f i

Proof state:
case h
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L L' : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
β : L ⟶ L'
i : ι
⊢ (e.homRestrict (ψ ≫ extendMap β e)).f i = (e.homRestrict ψ ≫ β).f i

Tactic:
simp [homRestrict_f _ _ rfl, extendMap_f β e rfl]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp)]
lemma inv_op_smul_finset_distrib (a : α) (s : Finset α) : (op a • s)⁻¹ = a⁻¹ • s⁻¹

Proof state:
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (op a • s)⁻¹ = a⁻¹ • s⁻¹

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ (op a • s)⁻¹ ↔ a✝ ∈ a⁻¹ • s⁻¹

Proof state:
case h
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ (op a • s)⁻¹ ↔ a✝ ∈ a⁻¹ • s⁻¹

Tactic:
simp [← inv_smul_mem_iff]

Result:
no goals
-- Mathlib/Data/Vector/Mem.lean
theorem not_mem_nil : a ∉ (Vector.nil : Vector α 0).toList

Proof state:
α : Type u_1
a : α
⊢ a ∉ toList ⟨[], ⋯⟩

Tactic:
dsimp

Result:
α : Type u_1
a : α
⊢ a ∉ []

Proof state:
α : Type u_1
a : α
⊢ a ∉ []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
⊢ a ∉ nil.toList

Tactic:
unfold Vector.nil

Result:
α : Type u_1
a : α
⊢ a ∉ toList ⟨[], ⋯⟩
-- Mathlib/Algebra/Homology/Augment.lean
theorem augment_d_succ_succ (C : ChainComplex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫ f = 0)
    (i j : ℕ) : (augment C f w).d (i + 1) (j + 1) = C.d i j

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i j : ℕ
⊢ (C.augment f w).d (i + 1) (j + 1) = C.d i j

Tactic:
cases i <;> rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_zero : log 0 = 0

Proof state:
⊢ log 0 = 0

Tactic:
simp [log]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblU_smul {P : Fin 3 → F} (hPz : P z ≠ 0) {u : F} (hu : u ≠ 0) :
    W.dblU (u • P) = u ^ 4 * W.dblU P

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
u : F
hu : u ≠ 0
⊢ W.dblU (u • P) = u ^ 4 * W.dblU P

Tactic:
field_simp [dblU_eq, smul_fin3_ext]

Result:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
u : F
hu : u ≠ 0
⊢ (W.a₁ * (u * P y) * (u * P z) - (3 * (u * P x) ^ 2 + 2 * W.a₂ * (u * P x) * (u * P z) + W.a₄ * (u * P z) ^ 2)) ^ 3 *
      P z ^ 2 =
    u ^ 4 * (W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2)) ^ 3 * (u * P z) ^ 2

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
u : F
hu : u ≠ 0
⊢ (W.a₁ * (u * P y) * (u * P z) - (3 * (u * P x) ^ 2 + 2 * W.a₂ * (u * P x) * (u * P z) + W.a₄ * (u * P z) ^ 2)) ^ 3 *
      P z ^ 2 =
    u ^ 4 * (W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2)) ^ 3 * (u * P z) ^ 2

Tactic:
ring1

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Iso.lean
@[reassoc (attr := simp)]
lemma pullback_inv_fst_snd_of_right_isIso :
    inv (pullback.fst f g) ≫ pullback.snd f g = f ≫ inv g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ inv (pullback.fst f g) ≫ pullback.snd f g = f ≫ inv g

Tactic:
rw [IsIso.inv_comp_eq, pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem isBounded_iff {s : Set α} :
    IsBounded s ↔ ∃ C : ℝ, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → dist x y ≤ C

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C

Tactic:
rw [isBounded_def, ← Filter.mem_sets, @PseudoMetricSpace.cobounded_sets α, mem_setOf_eq,
  compl_compl]

Result:
no goals
-- Mathlib/Control/Fold.lean
theorem toList_spec (xs : t α) : toList xs = FreeMonoid.toList (foldMap FreeMonoid.of xs) :=
  Eq.symm <|
    calc
      FreeMonoid.toList (foldMap FreeMonoid.of xs) =
          FreeMonoid.toList (foldMap FreeMonoid.of xs).reverse.reverse

Proof state:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (unop ((Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)) []).reverse = toList xs

Tactic:
rw [foldMap_hom_free (Foldl.ofFreeMonoid (flip <| @cons α))]

Result:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (unop (foldMap (⇑(Foldl.ofFreeMonoid (flip cons)) ∘ FreeMonoid.of) xs) []).reverse = toList xs

Proof state:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ FreeMonoid.toList (foldMap FreeMonoid.of xs).reverse.reverse =
    (List.foldr cons [] (FreeMonoid.toList (foldMap FreeMonoid.of xs)).reverse).reverse

Tactic:
simp only [FreeMonoid.reverse_reverse, List.foldr_reverse, List.foldl_flip_cons_eq_append,
  List.append_nil, List.reverse_reverse]

Result:
no goals

Proof state:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (List.foldr cons [] (FreeMonoid.toList (foldMap FreeMonoid.of xs)).reverse).reverse =
    (unop ((Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)) []).reverse

Tactic:
simp [Function.flip_def, List.foldr_reverse, Foldl.ofFreeMonoid, unop_op]

Result:
no goals

Proof state:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (unop (foldMap (⇑(Foldl.ofFreeMonoid (flip cons)) ∘ FreeMonoid.of) xs) []).reverse = toList xs

Tactic:
simp only [toList, foldl, List.reverse_inj, Foldl.get, foldl.ofFreeMonoid_comp_of,
  Function.comp_apply]

Result:
no goals

Proof state:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ FreeMonoid.toList (foldMap FreeMonoid.of xs) = FreeMonoid.toList (foldMap FreeMonoid.of xs).reverse.reverse

Tactic:
simp only [FreeMonoid.reverse_reverse]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem neg_get (xs : IntList) (i : Nat) : (- xs).get i = - xs.get i

Proof state:
xs : IntList
i : Nat
⊢ (Option.map (fun x => -x) xs[i]?).getD 0 = -xs[i]?.getD 0

Tactic:
cases xs[i]? <;> simp

Result:
no goals

Proof state:
xs : IntList
i : Nat
⊢ (-xs).get i = -xs.get i

Tactic:
simp only [get, neg_def, List.get?_eq_getElem?, List.getElem?_map]

Result:
xs : IntList
i : Nat
⊢ (Option.map (fun x => -x) xs[i]?).getD 0 = -xs[i]?.getD 0
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem sum_Ico_Ico_comm {M : Type*} [AddCommMonoid M] (a b : ℕ) (f : ℕ → ℕ → M) :
    (∑ i ∈ Finset.Ico a b, ∑ j ∈ Finset.Ico i b, f i j) =
      ∑ j ∈ Finset.Ico a b, ∑ i ∈ Finset.Ico a (j + 1), f i j

Proof state:
M : Type u_3
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ x ∈ (Ico a b).sigma fun i => Ico i b, f x.fst x.snd = ∑ x ∈ (Ico a b).sigma fun j => Ico a (j + 1), f x.snd x.fst

Tactic:
refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
  (fun _ _ ↦ rfl) <;>
simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma] <;>
rintro a b ⟨⟨h₁, h₂⟩, ⟨h₃, h₄⟩⟩ <;>
omega

Result:
no goals

Proof state:
M : Type u_3
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ i ∈ Ico a b, ∑ j ∈ Ico i b, f i j = ∑ j ∈ Ico a b, ∑ i ∈ Ico a (j + 1), f i j

Tactic:
rw [Finset.sum_sigma', Finset.sum_sigma']

Result:
M : Type u_3
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ x ∈ (Ico a b).sigma fun i => Ico i b, f x.fst x.snd = ∑ x ∈ (Ico a b).sigma fun j => Ico a (j + 1), f x.snd x.fst
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem Context.mergeIdem_head : mergeIdem (x :: x :: xs) = mergeIdem (x :: xs)

Proof state:
x : Nat
xs : List Nat
⊢ mergeIdem (x :: x :: xs) = mergeIdem (x :: xs)

Tactic:
simp [mergeIdem, mergeIdem.loop]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem val_lt_one_iff (v : Valuation K Γ₀) {x : K} (h : x ≠ 0) : v x < 1 ↔ 1 < v x⁻¹

Proof state:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x ≠ 0
⊢ v x < 1 ↔ 1 < v x⁻¹

Tactic:
simp [one_lt_inv₀ (v.pos_iff.2 h)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_ediv_cancel (a : Int) {b : Int} (H : b ≠ 0) : (a * b) / b = a

Proof state:
a b : Int
H : b ≠ 0
⊢ a * b / b = a

Tactic:
have := Int.add_mul_ediv_right 0 a H

Result:
a b : Int
H : b ≠ 0
this : (0 + a * b) / b = 0 / b + a
⊢ a * b / b = a

Proof state:
a b : Int
H : b ≠ 0
this : (0 + a * b) / b = 0 / b + a
⊢ a * b / b = a

Tactic:
rwa [Int.zero_add, Int.zero_ediv, Int.zero_add] at this

Result:
no goals