harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/RingQuot.lean
theorem mul_quot {a b} : (⟨Quot.mk _ a⟩ * ⟨Quot.mk _ b⟩ : RingQuot r) = ⟨Quot.mk _ (a * b)⟩

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b : R
⊢ (match { toQuot := Quot.mk (Rel r) a }, { toQuot := Quot.mk (Rel r) b } with
    | { toQuot := a }, { toQuot := b } => { toQuot := Quot.map₂ (fun x1 x2 => x1 * x2) ⋯ ⋯ a b }) =
    { toQuot := Quot.mk (Rel r) (a * b) }

Tactic:
rfl

Result:
no goals

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b : R
⊢ { toQuot := Quot.mk (Rel r) a } * { toQuot := Quot.mk (Rel r) b } = { toQuot := Quot.mk (Rel r) (a * b) }

Tactic:
show mul r _ _ = _

Result:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b : R
⊢ RingQuot.mul r { toQuot := Quot.mk (Rel r) a } { toQuot := Quot.mk (Rel r) b } = { toQuot := Quot.mk (Rel r) (a * b) }

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b : R
⊢ RingQuot.mul r { toQuot := Quot.mk (Rel r) a } { toQuot := Quot.mk (Rel r) b } = { toQuot := Quot.mk (Rel r) (a * b) }

Tactic:
rw [mul_def]

Result:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b : R
⊢ (match { toQuot := Quot.mk (Rel r) a }, { toQuot := Quot.mk (Rel r) b } with
    | { toQuot := a }, { toQuot := b } => { toQuot := Quot.map₂ (fun x1 x2 => x1 * x2) ⋯ ⋯ a b }) =
    { toQuot := Quot.mk (Rel r) (a * b) }
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma disjointSigma_indep_iff {h I} :
    (Matroid.disjointSigma M h).Indep I ↔
      (∀ i, (M i).Indep (I ∩ (M i).E)) ∧ I ⊆ ⋃ i, (M i).E

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

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

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_fuzzy_iff {x y : PGame} : -x ‖ y ↔ x ‖ -y

Proof state:
x y : PGame
⊢ -x ‖ y ↔ x ‖ -y

Tactic:
rw [← neg_neg y, neg_fuzzy_neg_iff, neg_neg]

Result:
no goals
-- Mathlib/Algebra/Ring/CentroidHom.lean
lemma _root_.NonUnitalNonAssocCommSemiring.mem_center_iff (a : α) :
    a ∈ NonUnitalSubsemiring.center α ↔ ∀ b : α, Commute (L b) (L a)

Proof state:
α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ (L a = L a ∧ ∀ g ∈ Set.range ⇑L, g * L a = L a * g) ↔ ∀ (b : α), Commute (L b) (L a)

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α ↔ ∀ (b : α), Commute (L b) (L a)

Tactic:
rw [NonUnitalNonAssocSemiring.mem_center_iff, CentroidHom.centroid_eq_centralizer_mulLeftRight,
  Subsemiring.mem_centralizer_iff, AddMonoid.End.mulRight_eq_mulLeft, Set.union_self]

Result:
α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ (L a = L a ∧ ∀ g ∈ Set.range ⇑L, g * L a = L a * g) ↔ ∀ (b : α), Commute (L b) (L a)
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem Step.cons_cons_iff : ∀ {p : α × Bool}, Step (p :: L₁) (p :: L₂) ↔ Step L₁ L₂

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
⊢ ∀ {p : α × Bool}, Step (p :: L₁) (p :: L₂) ↔ Step L₁ L₂

Tactic:
simp +contextual [Step.cons_left_iff, iff_def, or_imp]

Result:
no goals
-- Mathlib/Algebra/BigOperators/NatAntidiagonal.lean
theorem prod_antidiagonal_swap {n : ℕ} {f : ℕ × ℕ → M} :
    ∏ p ∈ antidiagonal n, f p.swap = ∏ p ∈ antidiagonal n, f p

Proof state:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p ∈ antidiagonal n, f p.swap = ∏ p ∈ antidiagonal n, f p

Tactic:
conv_lhs => rw [← map_swap_antidiagonal, Finset.prod_map]

Result:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ x ∈ antidiagonal n, f ({ toFun := Prod.swap, inj' := ⋯ } x).swap = ∏ p ∈ antidiagonal n, f p

Proof state:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ x ∈ antidiagonal n, f ({ toFun := Prod.swap, inj' := ⋯ } x).swap = ∏ p ∈ antidiagonal n, f p

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Part.lean
theorem some_sdiff_some [SDiff α] (a b : α) : some a \ some b = some (a \ b)

Proof state:
α : Type u_1
inst✝ : SDiff α
a b : α
⊢ some a \ some b = some (a \ b)

Tactic:
simp [sdiff_def]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem principal_singleton (a : α) : 𝓟 {a} = pure a :=
  Filter.ext fun s => by simp only [mem_pure, mem_principal, singleton_subset_iff]

Proof state:
α : Type u_1
a : α
s : Set α
⊢ s ∈ 𝓟 {a} ↔ s ∈ pure a

Tactic:
simp only [mem_pure, mem_principal, singleton_subset_iff]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem get?_terminates_le {s : WSeq α} {m n} (h : m ≤ n) :
    Terminates (get? s n) → Terminates (get? s m)

Proof state:
α : Type u
s : WSeq α
m n : ℕ
h : m ≤ n
⊢ (s.get? n).Terminates → (s.get? m).Terminates

Tactic:
induction' h with m' _ IH

Result:
case refl
α : Type u
s : WSeq α
m n : ℕ
⊢ (s.get? m).Terminates → (s.get? m).Terminates

case step
α : Type u
s : WSeq α
m n m' : ℕ
a✝ : m.le m'
IH : (s.get? m').Terminates → (s.get? m).Terminates
⊢ (s.get? m'.succ).Terminates → (s.get? m).Terminates

Proof state:
case refl
α : Type u
s : WSeq α
m n : ℕ
⊢ (s.get? m).Terminates → (s.get? m).Terminates

case step
α : Type u
s : WSeq α
m n m' : ℕ
a✝ : m.le m'
IH : (s.get? m').Terminates → (s.get? m).Terminates
⊢ (s.get? m'.succ).Terminates → (s.get? m).Terminates

Tactic:
exacts [id, fun T => IH (@head_terminates_of_head_tail_terminates _ _ T)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range'_succ_left : range' (s + 1) n step = (range' s n step).map (· + 1)

Proof state:
s n step : Nat
⊢ range' (s + 1) n step = map (fun x => x + 1) (range' s n step)

Tactic:
ext <;> simp <;> omega

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem top_rpow_of_pos {y : ℝ} (h : 0 < y) : (⊤ : ℝ≥0∞) ^ y = ⊤

Proof state:
y : ℝ
h : 0 < y
⊢ ⊤ ^ y = ⊤

Tactic:
simp [top_rpow_def, h]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem index_inf_le : (H ⊓ K).index ≤ H.index * K.index

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H ⊓ K).index ≤ H.index * K.index

Tactic:
simp_rw [← relindex_top_right, relindex_inf_le]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iInf₂_comm {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*}
    (f : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → α) :
    ⨅ (i₁) (j₁) (i₂) (j₂), f i₁ j₁ i₂ j₂ = ⨅ (i₂) (j₂) (i₁) (j₁), f i₁ j₁ i₂ j₂

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
ι₁ : Sort u_8
ι₂ : Sort u_9
κ₁ : ι₁ → Sort u_10
κ₂ : ι₂ → Sort u_11
f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α
⊢ ⨅ i₁, ⨅ j₁, ⨅ i₂, ⨅ j₂, f i₁ j₁ i₂ j₂ = ⨅ i₂, ⨅ j₂, ⨅ i₁, ⨅ j₁, f i₁ j₁ i₂ j₂

Tactic:
simp only [@iInf_comm _ (κ₁ _), @iInf_comm _ ι₁]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_const_add_Iic : (fun x => a + x) '' Iic b = Iic (a + b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => a + x) '' Iic b = Iic (a + b)

Tactic:
simp [add_comm]

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

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
x x' : α
h : x = x'
⊢ x = term 1 x' 0

Tactic:
simp [term, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem sub_min_sub_left (a b c : Nat) : min (a - b) (a - c) = a - max b c

Proof state:
a b c : Nat
⊢ min (a - b) (a - c) = a - max b c

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem card_image_of_inj_on {s : Set α} [Fintype s] {f : α → β} [Fintype (f '' s)]
    (H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) : Fintype.card (f '' s) = Fintype.card s :=
  haveI := Classical.propDecidable
  calc
    Fintype.card (f '' s) = (s.toFinset.image f).card := Fintype.card_of_finset' _ (by simp)
    _ = s.toFinset.card :=
      Finset.card_image_of_injOn fun x hx y hy hxy =>
        H x (mem_toFinset.1 hx) y (mem_toFinset.1 hy) hxy
    _ = Fintype.card s := (Fintype.card_of_finset' _ fun _ => mem_toFinset).symm

Proof state:
α : Type u
β : Type v
s : Set α
inst✝¹ : Fintype ↑s
f : α → β
inst✝ : Fintype ↑(f '' s)
H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
this : (a : Prop) → Decidable a
⊢ ∀ (x : β), x ∈ Finset.image f s.toFinset ↔ x ∈ f '' s

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem finset_card_le_finrank [Module.Finite R M]
    {b : Finset M} (h : LinearIndependent R (fun x => x : b → M)) :
    b.card ≤ finrank R M

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
b : Finset M
h : LinearIndependent R fun x => ↑x
⊢ b.card ≤ finrank R M

Tactic:
rw [← Fintype.card_coe]

Result:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
b : Finset M
h : LinearIndependent R fun x => ↑x
⊢ Fintype.card { x // x ∈ b } ≤ finrank R M

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
b : Finset M
h : LinearIndependent R fun x => ↑x
⊢ Fintype.card { x // x ∈ b } ≤ finrank R M

Tactic:
exact h.fintype_card_le_finrank

Result:
no goals
-- Mathlib/Algebra/DirectSum/Ring.lean
theorem of_intCast (n : ℤ) : of A 0 n = n

Proof state:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommGroup (A i)
inst✝¹ : AddMonoid ι
inst✝ : GRing A
n : ℤ
⊢ (of A 0) ↑n = ↑n

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivAt.const_mul (c : 𝔸) (hd : HasDerivAt d d' x) :
    HasDerivAt (fun y => c * d y) (c * d') x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (fun y => c * d y) (c * d') univ x

Tactic:
exact hd.const_mul c

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivAt d d' x
⊢ HasDerivAt (fun y => c * d y) (c * d') x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (fun y => c * d y) (c * d') univ x
-- Mathlib/Algebra/Group/Basic.lean
theorem div_div_div_eq : a / b / (c / d) = a * d / (b * c)

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b / (c / d) = a * d / (b * c)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/WithZero.lean
lemma unzero_mul {x y : WithZero α} (hxy : x * y ≠ 0) :
    unzero hxy = unzero (left_ne_zero_of_mul hxy) * unzero (right_ne_zero_of_mul hxy)

Proof state:
α : Type u_1
inst✝ : Mul α
x y : WithZero α
hxy : x * y ≠ 0
⊢ unzero hxy = unzero ⋯ * unzero ⋯

Tactic:
simp only [← coe_inj, coe_mul, coe_unzero]

Result:
no goals
-- Mathlib/Data/Rat/Floor.lean
theorem Int.mod_nat_eq_sub_mul_floor_rat_div {n : ℤ} {d : ℕ} : n % d = n - d * ⌊(n : ℚ) / d⌋

Proof state:
n : ℤ
d : ℕ
⊢ n % ↑d = n - ↑d * ⌊↑n / ↑d⌋

Tactic:
rw [eq_sub_of_add_eq <| Int.emod_add_ediv n d, Rat.floor_intCast_div_natCast]

Result:
no goals
-- Mathlib/Tactic/NormNum/Pow.lean
theorem isInt_zpow_neg {α : Type*} [DivisionRing α] {a : α} {b : ℤ} {nb ne : ℕ}
    (pb : IsInt b (Int.negOfNat nb)) (pe' : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)) :
    IsInt (a ^ b) (Int.negOfNat ne)

Proof state:
α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)
⊢ IsInt (a ^ b) (Int.negOfNat ne)

Tactic:
rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addXYZ_of_Z_eq_zero_right [NoZeroDivisors R] {P Q : Fin 3 → R} (hQ : W'.Equation Q)
    (hQz : Q z = 0) : W'.addXYZ P Q = -(Q y ^ 2 * P z) • P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.addXYZ P Q = -(Q y ^ 2 * P z) • P

Tactic:
rw [addXYZ, addX_of_Z_eq_zero_right hQ hQz, addY_of_Z_eq_zero_right hQ hQz,
  addZ_of_Z_eq_zero_right hQ hQz, smul_fin3]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_inj {v w : Vector α n} : v.toList = w.toList ↔ v = w

Proof state:
case mk.mk
α : Type u_1
n : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.toList =
      { toArray := toArray✝, size_toArray := size_toArray✝ }.toList ↔
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp [Array.toList_inj]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v w : Vector α n
⊢ v.toList = w.toList ↔ v = w

Tactic:
cases v

Result:
case mk
α : Type u_1
n : Nat
w : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toList = w.toList ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } = w

Proof state:
case mk
α : Type u_1
n : Nat
w : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toList = w.toList ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } = w

Tactic:
cases w

Result:
case mk.mk
α : Type u_1
n : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.toList =
      { toArray := toArray✝, size_toArray := size_toArray✝ }.toList ↔
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem Function.comp_const {f : β → γ} {b : β} :
    (f ∘ Function.const α b) = Function.const α (f b)

Proof state:
β : Sort u_1
γ : Sort u_2
α : Sort u_3
f : β → γ
b : β
⊢ f ∘ const α b = const α (f b)

Tactic:
rfl

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem equivAdjoinSimple_symm_aeval (pb : PowerBasis K L) (f : K[X]) :
    pb.equivAdjoinSimple.symm (aeval pb.gen f) = aeval (AdjoinSimple.gen K pb.gen) f

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
pb : PowerBasis K L
f : K[X]
⊢ pb.equivAdjoinSimple.symm ((aeval pb.gen) f) = (aeval (AdjoinSimple.gen K pb.gen)) f

Tactic:
rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_aeval, adjoin.powerBasis_gen]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem isCauSeq_im (f : CauSeq K norm) : IsCauSeq abs fun n => im (f n) := fun _ ε0 =>
  (f.cauchy ε0).imp fun i H j ij =>
    lt_of_le_of_lt (by simpa only [map_sub] using abs_im_le_norm (f j - f i)) (H _ ij)

Proof state:
K : Type u_1
inst✝ : RCLike K
f : CauSeq K norm
x✝ : ℝ
ε0 : x✝ > 0
i : ℕ
H : ∀ j ≥ i, ‖↑f j - ↑f i‖ < x✝
j : ℕ
ij : j ≥ i
⊢ |(fun n => im (↑f n)) j - (fun n => im (↑f n)) i| ≤ ‖↑f j - ↑f i‖

Tactic:
simpa only [map_sub] using abs_im_le_norm (f j - f i)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
lemma integral_pos (hab : a < b)
    (hfc : ContinuousOn f (Icc a b)) (hle : ∀ x ∈ Ioc a b, 0 ≤ f x) (hlt : ∃ c ∈ Icc a b, 0 < f c) :
    0 < ∫ x in a..b, f x :=
  (integral_lt_integral_of_continuousOn_of_le_of_exists_lt hab
    continuousOn_const hfc hle hlt).trans_eq' (by simp)

Proof state:
f : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hle : ∀ x ∈ Ioc a b, 0 ≤ f x
hlt : ∃ c ∈ Icc a b, 0 < f c
⊢ 0 = ∫ (x : ℝ) in a..b, 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Holder.lean
lemma one_div_add_one_div : 1 / p + 1 / q = 1 / r

Proof state:
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
⊢ 1 / p + 1 / q = 1 / r

Tactic:
simpa using inv_add_inv'

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem inverse_unit (u : M₀ˣ) : inverse (u : M₀) = (u⁻¹ : M₀ˣ)

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ inverse ↑u = ↑u⁻¹

Tactic:
rw [inverse, dif_pos u.isUnit, IsUnit.unit_of_val_units]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_inv_lt_iff_of_neg (h : a < 0) : b₁ < a⁻¹ • b₂ ↔ b₂ < a • b₁

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedField α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
a : α
b₁ b₂ : β
inst✝ : PosSMulStrictMono α β
h : a < 0
⊢ b₁ < a⁻¹ • b₂ ↔ b₂ < a • b₁

Tactic:
rw [← smul_lt_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem insert_idem (a : α) (s : Finset α) : insert a (insert a s) = insert a s :=
  ext fun x => by simp only [mem_insert, ← or_assoc, or_self_iff]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
⊢ x ∈ insert a (insert a s) ↔ x ∈ insert a s

Tactic:
simp only [mem_insert, ← or_assoc, or_self_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem unzip_zipIdx_eq_prod (l : List α) {n : Nat} :
    (l.zipIdx n).unzip = (l, range' n l.length)

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ (l.zipIdx n).unzip = (l, range' n l.length)

Tactic:
simp only [zipIdx_eq_zip_range', unzip_zip, length_range']

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem bodd_subNatNat (m n : ℕ) : bodd (subNatNat m n) = xor m.bodd n.bodd

Proof state:
m n : ℕ
⊢ (subNatNat m n).bodd = (m.bodd ^^ n.bodd)

Tactic:
apply subNatNat_elim m n fun m n i => bodd i = xor m.bodd n.bodd <;>
intros i j <;>
simp only [Int.bodd, Int.bodd_coe, Nat.bodd_add] <;>
cases Nat.bodd i <;> simp

Result:
no goals
-- Mathlib/NumberTheory/Multiplicity.lean
theorem dvd_geom_sum₂_iff_of_dvd_sub {x y p : R} (h : p ∣ x - y) :
    (p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) ↔ p ∣ n * y ^ (n - 1)

Proof state:
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : p ∣ x - y
⊢ p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1)

Tactic:
rw [← mem_span_singleton, ← Ideal.Quotient.eq] at h

Result:
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : (Ideal.Quotient.mk (span {p})) x = (Ideal.Quotient.mk (span {p})) y
⊢ p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1)

Proof state:
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : (Ideal.Quotient.mk (span {p})) x = (Ideal.Quotient.mk (span {p})) y
⊢ p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1)

Tactic:
simp only [← mem_span_singleton, ← eq_zero_iff_mem, RingHom.map_geom_sum₂, h, geom_sum₂_self,
  _root_.map_mul, map_pow, map_natCast]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_congr_meas (hs : MeasurableSet s) :
    μ.restrict s = ν.restrict s ↔ ∀ t ⊆ s, MeasurableSet t → μ t = ν t :=
  ⟨fun H t hts ht => by
    rw [← inter_eq_self_of_subset_left hts, ← restrict_apply ht, H, restrict_apply ht], fun H =>
    ext fun t ht => by
      rw [restrict_apply ht, restrict_apply ht, H _ inter_subset_right (ht.inter hs)]⟩

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
H : μ.restrict s = ν.restrict s
t : Set α
hts : t ⊆ s
ht : MeasurableSet t
⊢ μ t = ν t

Tactic:
rw [← inter_eq_self_of_subset_left hts, ← restrict_apply ht, H, restrict_apply ht]

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
H : ∀ t ⊆ s, MeasurableSet t → μ t = ν t
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict s) t = (ν.restrict s) t

Tactic:
rw [restrict_apply ht, restrict_apply ht, H _ inter_subset_right (ht.inter hs)]

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomial.lean
theorem HasFiniteFPowerSeriesOnBall.sub (hf : HasFiniteFPowerSeriesOnBall f pf x n r)
    (hg : HasFiniteFPowerSeriesOnBall g pg x m r) :
    HasFiniteFPowerSeriesOnBall (f - g) (pf - pg) x (max n m) r

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n m : ℕ
hf : HasFiniteFPowerSeriesOnBall f pf x n r
hg : HasFiniteFPowerSeriesOnBall g pg x m r
⊢ HasFiniteFPowerSeriesOnBall (f - g) (pf - pg) x (n ⊔ m) r

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.isOpen_iff_mem_balls (hp : WithSeminorms p) (U : Set E) :
    IsOpen U ↔ ∀ x ∈ U, ∃ s : Finset ι, ∃ r > 0, (s.sup p).ball x r ⊆ U

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
U : Set E
⊢ IsOpen U ↔ ∀ x ∈ U, ∃ s, ∃ r > 0, (s.sup p).ball x r ⊆ U

Tactic:
simp_rw [← WithSeminorms.mem_nhds_iff hp _ U, isOpen_iff_mem_nhds]

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

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

Tactic:
rw [← castSucc_lt_castSucc_iff, castSucc_castPred]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiffAt_iff_target {x : M} :
    ContMDiffAt I I' n f x ↔
      ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n (extChartAt I' (f x) ∘ 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'
n : WithTop ℕ∞
x : M
⊢ ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n (↑(extChartAt I' (f x)) ∘ f) x

Tactic:
rw [ContMDiffAt, ContMDiffAt, contMDiffWithinAt_iff_target, continuousWithinAt_univ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem degree_pos_of_ne_zero_of_nonunit (hp0 : p ≠ 0) (hp : ¬IsUnit p) : 0 < degree p :=
  lt_of_not_ge fun h => by
    rw [eq_C_of_degree_le_zero h] at hp0 hp
    exact hp (IsUnit.map C (IsUnit.mk0 (coeff p 0) (mt C_inj.2 (by simpa using hp0))))

Proof state:
R : Type u
inst✝ : DivisionRing R
p : R[X]
hp0 : p ≠ 0
hp : ¬IsUnit p
h : 0 ≥ p.degree
⊢ False

Tactic:
rw [eq_C_of_degree_le_zero h] at hp0 hp

Result:
R : Type u
inst✝ : DivisionRing R
p : R[X]
hp0 : C (p.coeff 0) ≠ 0
hp : ¬IsUnit (C (p.coeff 0))
h : 0 ≥ p.degree
⊢ False

Proof state:
R : Type u
inst✝ : DivisionRing R
p : R[X]
hp0 : C (p.coeff 0) ≠ 0
hp : ¬IsUnit (C (p.coeff 0))
h : 0 ≥ p.degree
⊢ ¬C (p.coeff 0) = C 0

Tactic:
simpa using hp0

Result:
no goals

Proof state:
R : Type u
inst✝ : DivisionRing R
p : R[X]
hp0 : C (p.coeff 0) ≠ 0
hp : ¬IsUnit (C (p.coeff 0))
h : 0 ≥ p.degree
⊢ False

Tactic:
exact hp (IsUnit.map C (IsUnit.mk0 (coeff p 0) (mt C_inj.2 (by simpa using hp0))))

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem norm_eq_of_L1 (x : PiLp 1 β) : ‖x‖ = ∑ i : ι, ‖x i‖

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 1 β
⊢ ‖x‖ = ∑ i : ι, ‖x i‖

Tactic:
simp [norm_eq_sum]

Result:
no goals
-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem addVal_uniformizer {ϖ : R} (hϖ : Irreducible ϖ) : addVal R ϖ = 1

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
⊢ (addVal R) ϖ = 1

Tactic:
simpa only [one_mul, eq_self_iff_true, Units.val_one, pow_one, forall_true_left, Nat.cast_one]
  using addVal_def ϖ 1 hϖ 1

Result:
no goals