harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem sameCycle_zpow_left {n : ℤ} : SameCycle f ((f ^ n) x) y ↔ SameCycle f x y :=
  (Equiv.addRight (n : ℤ)).exists_congr_left.trans <| by simp [SameCycle, zpow_add]

Proof state:
α : Type u_2
f : Perm α
x y : α
n : ℤ
⊢ (∃ b, (f ^ (Equiv.symm (Equiv.addRight n)) b) ((f ^ n) x) = y) ↔ f.SameCycle x y

Tactic:
simp [SameCycle, zpow_add]

Result:
no goals
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
lemma specializes_iff_le {a b : α} : a ⤳ b ↔ b ≤ a

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
a b : α
⊢ a ⤳ b ↔ b ≤ a

Tactic:
simp only [specializes_iff_closure_subset, closure_singleton, Iic_subset_Iic]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem tail_attachWith {P : α → Prop} {xs : List α}
    {H : ∀ (a : α), a ∈ xs → P a} :
    (xs.attachWith P H).tail = xs.tail.attachWith P (fun a h => H a (mem_of_mem_tail h))

Proof state:
α : Type u_1
P : α → Prop
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ (xs.attachWith P H).tail = xs.tail.attachWith P ⋯

Tactic:
cases xs <;> simp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem smul_closedBall' {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) :
    c • closedBall x r = closedBall (c • x) (‖c‖ * r)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)

Tactic:
simp only [← ball_union_sphere, Set.smul_set_union, _root_.smul_ball hc, smul_sphere' hc]

Result:
no goals
-- Mathlib/Order/Filter/Pointwise.lean
theorem map_one [FunLike F α β] [OneHomClass F α β] (φ : F) : map φ 1 = 1

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : One α
inst✝² : One β
inst✝¹ : FunLike F α β
inst✝ : OneHomClass F α β
φ : F
⊢ map (⇑φ) 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem LipschitzWith.norm_div_le_of_le {f : E → F} {C : ℝ≥0} (h : LipschitzWith C f)
    (hr : ‖a / b‖ ≤ r) : ‖f a / f b‖ ≤ C * r :=
  (h.norm_div_le _ _).trans <| by gcongr

Proof state:
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
a b : E
r : ℝ
f : E → F
C : ℝ≥0
h : LipschitzWith C f
hr : ‖a / b‖ ≤ r
⊢ ↑C * ‖a / b‖ ≤ ↑C * r

Tactic:
gcongr

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
lemma Measurable.div' [MeasurableDiv₂ G] {f g : α → β → G} {h : α → β} (hf : Measurable ↿f)
    (hg : Measurable ↿g) (hh : Measurable h) : Measurable fun a ↦ (f a / g a) (h a)

Proof state:
G : Type u_2
α : Type u_3
β : Type u_4
inst✝² : MeasurableSpace G
inst✝¹ : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableDiv₂ G
f g : α → β → G
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable fun a => (f a / g a) (h a)

Tactic:
simp

Result:
G : Type u_2
α : Type u_3
β : Type u_4
inst✝² : MeasurableSpace G
inst✝¹ : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableDiv₂ G
f g : α → β → G
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable fun a => f a (h a) / g a (h a)

Proof state:
G : Type u_2
α : Type u_3
β : Type u_4
inst✝² : MeasurableSpace G
inst✝¹ : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableDiv₂ G
f g : α → β → G
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable fun a => f a (h a) / g a (h a)

Tactic:
fun_prop

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem quotientMap_surjective {J : Ideal R} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided]
    {f : R →+* S} {H : J ≤ I.comap f}
    (hf : Function.Surjective f) : Function.Surjective (quotientMap I f H) := fun x =>
  let ⟨x, hx⟩ := Quotient.mk_surjective x
  let ⟨y, hy⟩ := hf x
  ⟨(Quotient.mk J) y, by simp [hx, hy]⟩

Proof state:
R : Type u
inst✝³ : Ring R
S : Type v
inst✝² : Ring S
J : Ideal R
I : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
hf : Surjective ⇑f
x✝ : S ⧸ I
x : S
hx : (Quotient.mk I) x = x✝
y : R
hy : f y = x
⊢ (quotientMap I f H) ((Quotient.mk J) y) = x✝

Tactic:
simp [hx, hy]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem le_castSucc_pred_iff {a b : Fin (n + 1)} (ha : a ≠ 0) :
    b ≤ castSucc (a.pred ha) ↔ b < a

Proof state:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
⊢ b ≤ (a.pred ha).castSucc ↔ b < a

Tactic:
rw [castSucc_pred_eq_pred_castSucc, le_pred_castSucc_iff]

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
@[simp]
lemma add_inv_add_mul_eq_zero (u : (PreQuasiregular R)ˣ) :
    u.val.val + u⁻¹.val.val + u⁻¹.val.val * u.val.val = 0

Proof state:
R : Type u_1
inst✝ : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ (↑u).val + (↑u⁻¹).val + (↑u⁻¹).val * (↑u).val = 0

Tactic:
simpa [-Units.inv_mul] using congr($(u.inv_mul).val)

Result:
no goals
-- Mathlib/CategoryTheory/Dialectica/Monoidal.lean
theorem tensor_id (X₁ X₂ : Dial C) : (𝟙 X₁ ⊗ 𝟙 X₂ : _ ⟶ _) = 𝟙 (X₁ ⊗ X₂ : Dial C)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ : Dial C
⊢ 𝟙 X₁ ⊗ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem natAbs_norm_eq (x : ℤ[i]) :
    x.norm.natAbs = x.re.natAbs * x.re.natAbs + x.im.natAbs * x.im.natAbs :=
  Int.ofNat.inj <| by simp; simp [Zsqrtd.norm]

Proof state:
x : ℤ[i]
⊢ norm x = x.re * x.re + x.im * x.im

Tactic:
simp [Zsqrtd.norm]

Result:
no goals

Proof state:
x : ℤ[i]
⊢ Int.ofNat (norm x).natAbs = Int.ofNat (x.re.natAbs * x.re.natAbs + x.im.natAbs * x.im.natAbs)

Tactic:
simp

Result:
x : ℤ[i]
⊢ norm x = x.re * x.re + x.im * x.im
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_singleton (a : α) (f : α → β) :
    noncommProd ({a} : Finset α) f
        (by
          norm_cast
          exact Set.pairwise_singleton _ _) =
      f a := mul_one _

Proof state:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
a : α
f : α → β
⊢ {a}.Pairwise (Commute on f)

Tactic:
exact Set.pairwise_singleton _ _

Result:
no goals

Proof state:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
a : α
f : α → β
⊢ (↑{a}).Pairwise (Commute on f)

Tactic:
norm_cast

Result:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
a : α
f : α → β
⊢ {a}.Pairwise (Commute on f)
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_umax_eq {a : Cardinal.{u}} {b : Cardinal.{v}} :
    lift.{max v w} a = lift.{max u w} b ↔ lift.{v} a = lift.{u} b

Proof state:
a : Cardinal.{u}
b : Cardinal.{v}
⊢ lift.{max v w, u} a = lift.{max u w, v} b ↔ lift.{v, u} a = lift.{u, v} b

Tactic:
rw [← lift_lift.{v, w, u}, ← lift_lift.{u, w, v}, lift_inj]

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Hom.lean
@[to_additive existing AddMonoidHom.apply_nat]
lemma MonoidHom.apply_mnat (f : Multiplicative ℕ →* M) (n : Multiplicative ℕ) :
    f n = f (Multiplicative.ofAdd 1) ^ n.toAdd

Proof state:
M : Type u_2
inst✝ : Monoid M
f : Multiplicative ℕ →* M
n : Multiplicative ℕ
⊢ f n = f (ofAdd 1) ^ toAdd n

Tactic:
rw [← powersHom_symm_apply, ← powersHom_apply, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem balance_sz_dual {l r}
    (H : (∃ l', Raised (@size α l) l' ∧ BalancedSz l' (@size α r)) ∨
        ∃ r', Raised r' (size r) ∧ BalancedSz (size l) r') :
    (∃ l', Raised l' (size (dual r)) ∧ BalancedSz l' (size (dual l))) ∨
      ∃ r', Raised (size (dual l)) r' ∧ BalancedSz (size (dual r)) r'

Proof state:
α : Type u_1
l r : Ordnode α
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ (∃ l', Raised l' r.size ∧ BalancedSz l' l.size) ∨ ∃ r', Raised l.size r' ∧ BalancedSz r.size r'

Tactic:
exact
  H.symm.imp (Exists.imp fun _ => And.imp_right BalancedSz.symm)
    (Exists.imp fun _ => And.imp_right BalancedSz.symm)

Result:
no goals

Proof state:
α : Type u_1
l r : Ordnode α
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ (∃ l', Raised l' r.dual.size ∧ BalancedSz l' l.dual.size) ∨ ∃ r', Raised l.dual.size r' ∧ BalancedSz r.dual.size r'

Tactic:
rw [size_dual, size_dual]

Result:
α : Type u_1
l r : Ordnode α
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ (∃ l', Raised l' r.size ∧ BalancedSz l' l.size) ∨ ∃ r', Raised l.size r' ∧ BalancedSz r.size r'
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_inv_natCast_smul [DivisionSemiring R] [AddCommMonoid α] [StarAddMonoid α]
    [Module R α] (c : ℕ) (M : Matrix m n α) : ((c : R)⁻¹ • M)ᴴ = (c : R)⁻¹ • Mᴴ :=
  Matrix.ext <| by simp

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommMonoid α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℕ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), ((↑c)⁻¹ • M)ᴴ i j = ((↑c)⁻¹ • Mᴴ) i j

Tactic:
simp

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem map_fract_sub_fract_eq (x : ℝ) : f (fract x) - fract x = f x - x

Proof state:
f : CircleDeg1Lift
x : ℝ
⊢ f (fract x) - fract x = f x - x

Tactic:
rw [Int.fract, f.map_sub_int, sub_sub_sub_cancel_right]

Result:
no goals
-- Mathlib/RingTheory/Radical.lean
theorem radical_pow_of_prime {a : M} (ha : Prime a) {n : ℕ} (hn : 0 < n) :
    radical (a ^ n) = normalize a

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : Prime a
n : ℕ
hn : 0 < n
⊢ radical (a ^ n) = normalize a

Tactic:
rw [radical_pow a hn]

Result:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : Prime a
n : ℕ
hn : 0 < n
⊢ radical a = normalize a

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : Prime a
n : ℕ
hn : 0 < n
⊢ radical a = normalize a

Tactic:
exact radical_of_prime ha

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
lemma condition (G : ReflexiveCofork F) : F.map left ≫ G.π = F.map right ≫ G.π

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ F.map left ≫ G.π = F.map right ≫ G.π

Tactic:
rw [Cocone.w G left, Cocone.w G right]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Inductions.lean
theorem divX_add : divX (p + q) = divX p + divX q :=
  ext <| by simp

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (n : ℕ), (p + q).divX.coeff n = (p.divX + q.divX).coeff n

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedDerivWithin_eq_equiv_comp : iteratedDerivWithin n f s =
    (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDerivWithin 𝕜 n f s

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
⊢ iteratedDerivWithin n f s = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDerivWithin 𝕜 n f s

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin n f s x =
    (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDerivWithin 𝕜 n f s) x

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin n f s x =
    (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDerivWithin 𝕜 n f s) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/UnitInterval.lean
@[simp]
lemma symm_eq_one {i : I} : σ i = 1 ↔ i = 0

Proof state:
i : ↑I
⊢ σ i = 1 ↔ i = 0

Tactic:
rw [← symm_zero, symm_inj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem self_eq_append_left {x y : List α} : y = x ++ y ↔ x = []

Proof state:
α : Type u_1
x y : List α
⊢ y = x ++ y ↔ x = []

Tactic:
rw [eq_comm, append_left_eq_self]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem frontier_compl (s : Set X) : frontier sᶜ = frontier s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier sᶜ = frontier s

Tactic:
simp only [frontier_eq_closure_inter_closure, compl_compl, inter_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
    {k fallback : α} (hl : DistinctKeys l) : getKeyD k (eraseKey k l) fallback = fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k fallback : α
hl : DistinctKeys l
⊢ getKeyD k (eraseKey k l) fallback = fallback

Tactic:
simp [getKeyD_eq_getKey?, getKey?_eraseKey_self hl]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Basic.lean
theorem map_neg (x : R) : f (-x) = f x

Proof state:
M : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : MulLeftMono M
f : R →* M
x : R
⊢ f (-x) = f x

Tactic:
rw [← neg_one_mul, map_mul, map_neg_one, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem mk' : ValidFor l r ⟨⟨l.reverse ++ r⟩, ⟨utf8Len l.reverse⟩⟩

Proof state:
l r : List Char
⊢ ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }

Tactic:
simpa [List.reverseAux_eq] using mk

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem lookup_replicate_self {a : α} :
    (replicate n (a, b)).lookup a = if n = 0 then none else some b

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
α✝ : Type u_1
b : α✝
a : α
⊢ lookup a (replicate n (a, b)) = if n = 0 then none else some b

Tactic:
simp [lookup_replicate]

Result:
no goals
-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem pluennecke_ruzsa_inequality_pow_div (hA : A.Nonempty) (B : Finset G) (n : ℕ) :
    #(B ^ n) ≤ (#(A / B) / #A : ℚ≥0) ^ n * #A

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
n : ℕ
⊢ ↑(#(B ^ n)) ≤ (↑(#(A / B)) / ↑(#A)) ^ n * ↑(#A)

Tactic:
simpa only [_root_.pow_zero, div_one] using pluennecke_ruzsa_inequality_pow_div_pow_div hA _ _ 0

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem forall_mem_append {p : α → Prop} {l₁ l₂ : Array α} :
    (∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x)

Proof state:
α : Type u_1
p : α → Prop
l₁ l₂ : Array α
⊢ (∀ (x : α), x ∈ l₁ ++ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x

Tactic:
simp only [mem_append, or_imp, forall_and]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_le_div_iff_right (c : α) : a / c ≤ b / c ↔ a ≤ b

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a / c ≤ b / c ↔ a ≤ b

Tactic:
simpa only [div_eq_mul_inv] using mul_le_mul_iff_right _

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

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

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma disjointSigma_isBasis_iff {h I X} :
    (Matroid.disjointSigma M h).IsBasis I X ↔
      (∀ i, (M i).IsBasis (I ∩ (M i).E) (X ∩ (M i).E)) ∧ I ⊆ X ∧ X ⊆ ⋃ i, (M i).E

Proof state:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise (Disjoint on fun i => (M i).E)
I X : Set α
⊢ (Matroid.disjointSigma M h).IsBasis I X ↔
    (∀ (i : ι), (M i).IsBasis (I ∩ (M i).E) (X ∩ (M i).E)) ∧ I ⊆ X ∧ X ⊆ ⋃ i, (M i).E

Tactic:
simp [Matroid.disjointSigma, Function.Embedding.sigmaSet_preimage h]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem mk_eq_mk_of_comm {B A₁ A₂ : C} (f : A₁ ⟶ B) (g : A₂ ⟶ B) [Mono f] [Mono g] (i : A₁ ≅ A₂)
    (w : i.hom ≫ g = f) : mk f = mk g :=
  eq_mk_of_comm _ ((underlyingIso f).trans i) <| by simp [w]

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst✝¹ : Mono f
inst✝ : Mono g
i : A₁ ≅ A₂
w : i.hom ≫ g = f
⊢ (underlyingIso f ≪≫ i).hom ≫ g = (mk f).arrow

Tactic:
simp [w]

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem lookup_insert {a} {b : β a} (s : Finmap β) : lookup a (insert a b s) = some b :=
  induction_on s fun s => by simp only [insert_toFinmap, lookup_toFinmap, AList.lookup_insert]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
⊢ lookup a (insert a b ⟦s⟧) = some b

Tactic:
simp only [insert_toFinmap, lookup_toFinmap, AList.lookup_insert]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem range_diag : (range fun x => (x, x)) = diagonal α

Proof state:
case h.mk
α : Type u_1
x y : α
⊢ ((x, y) ∈ range fun x => (x, x)) ↔ (x, y) ∈ diagonal α

Tactic:
simp [diagonal, eq_comm]

Result:
no goals

Proof state:
α : Type u_1
⊢ (range fun x => (x, x)) = diagonal α

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
x y : α
⊢ ((x, y) ∈ range fun x => (x, x)) ↔ (x, y) ∈ diagonal α
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableAt_iff_target_of_mem_source
    [IsManifold I' 1 M'] {x : M} {y : M'} (hy : f x ∈ (chartAt H' y).source) :
    MDifferentiableAt I I' f x ↔
      ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') (extChartAt I' y ∘ f) x

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
f : M → M'
inst✝ : IsManifold I' 1 M'
x : M
y : M'
hy : f x ∈ (chartAt H' y).source
⊢ MDifferentiableAt I I' f x ↔ ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') (↑(extChartAt I' y) ∘ f) x

Tactic:
rw [← mdifferentiableWithinAt_univ, mdifferentiableWithinAt_iff_target_of_mem_source hy,
  continuousWithinAt_univ, ← mdifferentiableWithinAt_univ]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem or_inr {a b : Bool} (H : b) : a || b

Proof state:
a b : Bool
H : b = true
⊢ (a || b) = true

Tactic:
cases a <;> simp [H]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive] lemma eq_or_eq_inv_of_mabs_eq (h : |a|ₘ = b) : a = b ∨ a = b⁻¹

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
h : mabs a = b
⊢ a = b ∨ a = b⁻¹

Tactic:
simpa only [← h, eq_comm (a := |a|ₘ), inv_eq_iff_eq_inv] using mabs_choice a

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_zero_mul_X (φ : R⟦X⟧) : coeff R 0 (φ * X) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (coeff R 0) (φ * X) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem compactSpace_of_finite_subfamily_closed
    (h : ∀ {ι : Type u} (t : ι → Set X), (∀ i, IsClosed (t i)) → ⋂ i, t i = ∅ →
      ∃ u : Finset ι, ⋂ i ∈ u, t i = ∅) :
    CompactSpace X where
  isCompact_univ := isCompact_of_finite_subfamily_closed fun t => by simpa using h t

Proof state:
X : Type u
inst✝ : TopologicalSpace X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → ⋂ i, t i = ∅ → ∃ u, ⋂ i ∈ u, t i = ∅
ι✝ : Type u
t : ι✝ → Set X
⊢ (∀ (i : ι✝), IsClosed (t i)) → univ ∩ ⋂ i, t i = ∅ → ∃ u, univ ∩ ⋂ i ∈ u, t i = ∅

Tactic:
simpa using h t

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem IsIntegral.map_of_comp_eq {R S T U : Type*} [CommRing R] [Ring S]
    [CommRing T] [Ring U] [Algebra R S] [Algebra T U] (φ : R →+* T) (ψ : S →+* U)
    (h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)) {a : S} (ha : IsIntegral R a) :
    IsIntegral T (ψ a) :=
  let ⟨p, hp⟩ := ha
  ⟨p.map φ, hp.1.map _, by
    rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.2, ψ.map_zero]⟩

Proof state:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : CommRing T
inst✝² : Ring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
⊢ eval₂ (algebraMap T U) (ψ a) (Polynomial.map φ p) = 0

Tactic:
rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.2, ψ.map_zero]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem of_equiv_iff {β} (e : β ≃ α) {f : σ → β} :
    haveI := Primcodable.ofEquiv α e
    (Primrec fun a => e (f a)) ↔ Primrec f :=
  letI := Primcodable.ofEquiv α e
  ⟨fun h => (of_equiv_symm.comp h).of_eq fun a => by simp, of_equiv.comp⟩

Proof state:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
β : Type u_4
e : β ≃ α
f : σ → β
this : Primcodable β := Primcodable.ofEquiv α e
h : Primrec fun a => e (f a)
a : σ
⊢ e.symm (e (f a)) = f a

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma ΨSq_four : W.ΨSq 4 = W.preΨ₄ ^ 2 * W.Ψ₂Sq

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ Even 4

Tactic:
decide

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.ΨSq 4 = W.preΨ₄ ^ 2 * W.Ψ₂Sq

Tactic:
rw [← Nat.cast_four, ΨSq_ofNat, preΨ'_four, if_pos <| by decide]

Result:
no goals
-- Mathlib/Algebra/Group/Action/Equidecomp.lean
theorem source_restr (f : Equidecomp X G) {A : Set X} (hA : A ⊆ f.source) :
    (f.restr A).source = A

Proof state:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
f : Equidecomp X G
A : Set X
hA : A ⊆ f.source
⊢ (f.restr A).source = A

Tactic:
rw [restr_source, inter_eq_self_of_subset_right hA]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Comma.lean
theorem unop_left_comp_underlyingIso_hom_unop {A : CostructuredArrow S T}
    {P : (CostructuredArrow S T)ᵒᵖ} (f : P ⟶ op A) [Mono f.unop.left.op] :
    f.unop.left ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop =
      (Subobject.mk f.unop.left.op).arrow.unop

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst✝ : Mono f.unop.left.op
⊢ f.unop.left ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop = (Subobject.mk f.unop.left.op).arrow.unop

Tactic:
conv_lhs =>
  congr
  rw [← Quiver.Hom.unop_op f.unop.left]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst✝ : Mono f.unop.left.op
⊢ f.unop.left.op.unop ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop = (Subobject.mk f.unop.left.op).arrow.unop

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst✝ : Mono f.unop.left.op
⊢ f.unop.left.op.unop ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop = (Subobject.mk f.unop.left.op).arrow.unop

Tactic:
rw [← unop_comp, Subobject.underlyingIso_hom_comp_eq_mk]

Result:
no goals
-- Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean
theorem comul_T (n : ℤ) :
    Coalgebra.comul (R := R) (T n : A[T;T⁻¹]) = T n ⊗ₜ[R] T n

Proof state:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
n : ℤ
⊢ CoalgebraStruct.comul (T n) = T n ⊗ₜ[R] T n

Tactic:
simp [T, -single_eq_C_mul_T, Algebra.TensorProduct.one_def]

Result:
no goals