harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem ne_zero_iff_weightedOrder_finite :
    f ≠ 0 ↔ (f.weightedOrder w).toNat = f.weightedOrder w

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ↑(weightedOrder w f).toNat = weightedOrder w f

Tactic:
simp only [weightedOrder, ne_eq, coe_toNat_eq_self, dite_eq_left_iff,
  ENat.coe_ne_top, imp_false, not_not]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem bijOn_empty_iff_left : BijOn f s ∅ ↔ s = ∅ :=
  ⟨fun h ↦ by simpa using h.mapsTo, by rintro rfl; exact bijOn_empty f⟩

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f ∅ ∅

Tactic:
exact bijOn_empty f

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : BijOn f s ∅
⊢ s = ∅

Tactic:
simpa using h.mapsTo

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ s = ∅ → BijOn f s ∅

Tactic:
rintro rfl

Result:
α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f ∅ ∅
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractLeft_algebraMap_mul (r : R) (b : CliffordAlgebra Q) :
    d⌋(algebraMap _ _ r * b) = algebraMap _ _ r * (d⌋b)

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
r : R
b : CliffordAlgebra Q
⊢ (contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r * b) =
    (algebraMap R (CliffordAlgebra Q)) r * (contractLeft d) b

Tactic:
rw [← Algebra.smul_def, map_smul, Algebra.smul_def]

Result:
no goals
-- Mathlib/Data/Nat/Pairing.lean
theorem pair_lt_max_add_one_sq (m n : ℕ) : pair m n < (max m n + 1) ^ 2

Proof state:
m n : ℕ
⊢ (if m < n then n * n + m else m * m + (m + n)) < (m ⊔ n) * (m ⊔ n) + (m ⊔ n + (m ⊔ n + 1))

Tactic:
split_ifs <;> simp [Nat.max_eq_left, Nat.max_eq_right, Nat.le_of_lt,  not_lt.1, *] <;> omega

Result:
no goals

Proof state:
m n : ℕ
⊢ pair m n < (m ⊔ n + 1) ^ 2

Tactic:
simp only [pair, Nat.pow_two, Nat.mul_add, Nat.add_mul, Nat.mul_one, Nat.one_mul, Nat.add_assoc]

Result:
m n : ℕ
⊢ (if m < n then n * n + m else m * m + (m + n)) < (m ⊔ n) * (m ⊔ n) + (m ⊔ n + (m ⊔ n + 1))
-- Mathlib/Data/Nat/Count.lean
theorem count_iff_forall_not {n : ℕ} : count p n = 0 ↔ ∀ m < n, ¬p m

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = 0 ↔ ∀ m < n, ¬p m

Tactic:
simpa [count_eq_card_filter_range, mem_range] using
  card_filter_eq_zero_iff (p := p) (s := range n)

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem IsOpenMap.continuousOn_range_of_leftInverse {f : α → β} (hf : IsOpenMap f) {finv : β → α}
    (hleft : Function.LeftInverse finv f) : ContinuousOn finv (range f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (f '' univ)

Tactic:
exact (hf.restrict isOpen_univ).continuousOn_image_of_leftInvOn fun x _ => hleft x

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (range f)

Tactic:
rw [← image_univ]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (f '' univ)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem back!_filterMap [Inhabited β] (f : α → Option β) (l : Array α) :
    (l.filterMap f).back! = (l.findSomeRev? f).getD default

Proof state:
β : Type u_1
α : Type u_2
inst✝ : Inhabited β
f : α → Option β
l : Array α
⊢ (filterMap f l).back! = (findSomeRev? f l).getD default

Tactic:
cases l

Result:
case mk
β : Type u_1
α : Type u_2
inst✝ : Inhabited β
f : α → Option β
toList✝ : List α
⊢ (filterMap f { toList := toList✝ }).back! = (findSomeRev? f { toList := toList✝ }).getD default

Proof state:
case mk
β : Type u_1
α : Type u_2
inst✝ : Inhabited β
f : α → Option β
toList✝ : List α
⊢ (filterMap f { toList := toList✝ }).back! = (findSomeRev? f { toList := toList✝ }).getD default

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Order.lean
theorem real_lt_real {x y : ℝ} : (x : ℂ) < (y : ℂ) ↔ x < y

Proof state:
x y : ℝ
⊢ ↑x < ↑y ↔ x < y

Tactic:
simp [lt_def, ofReal]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Semiconj.lean
theorem inv_symm_left_iff₀ : SemiconjBy a⁻¹ x y ↔ SemiconjBy a y x :=
  Classical.by_cases (fun ha : a = 0 => by simp only [ha, inv_zero, SemiconjBy.zero_left]) fun ha =>
    @units_inv_symm_left_iff _ _ (Units.mk0 a ha) _ _

Proof state:
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
ha : a = 0
⊢ SemiconjBy a⁻¹ x y ↔ SemiconjBy a y x

Tactic:
simp only [ha, inv_zero, SemiconjBy.zero_left]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
/-- If `F ⋙ G` preserves limits for `K`, and `G` reflects limits for `K ⋙ F`,
then `F` preserves limits for `K`. -/
lemma preservesLimit_of_reflects_of_preserves [PreservesLimit K (F ⋙ G)] [ReflectsLimit (K ⋙ F) G] :
    PreservesLimit K F :=
  ⟨fun h => ⟨by
    apply isLimitOfReflects G
    apply isLimitOfPreserves (F ⋙ G) h⟩⟩

Proof state:
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesLimit K (F ⋙ G)
inst✝ : ReflectsLimit (K ⋙ F) G
c✝ : Cone K
h : IsLimit c✝
⊢ IsLimit (G.mapCone (F.mapCone c✝))

Tactic:
apply isLimitOfPreserves (F ⋙ G) h

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesLimit K (F ⋙ G)
inst✝ : ReflectsLimit (K ⋙ F) G
c✝ : Cone K
h : IsLimit c✝
⊢ IsLimit (F.mapCone c✝)

Tactic:
apply isLimitOfReflects G

Result:
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesLimit K (F ⋙ G)
inst✝ : ReflectsLimit (K ⋙ F) G
c✝ : Cone K
h : IsLimit c✝
⊢ IsLimit (G.mapCone (F.mapCone c✝))
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem mul_card_image_le_card_of_maps_to {f : α → β} {s : Finset α} {t : Finset β}
    (Hf : ∀ a ∈ s, f a ∈ t) (n : ℕ) (hn : ∀ b ∈ t, n ≤ #{a ∈ s | f a = b}) :
    n * #t ≤ #s :=
  calc
    n * #t = ∑ _a ∈ t, n

Proof state:
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ a ∈ s, f a ∈ t
n : ℕ
hn : ∀ b ∈ t, n ≤ #(filter (fun a => f a = b) s)
⊢ ∑ b ∈ t, #(filter (fun a => f a = b) s) = #s

Tactic:
rw [← card_eq_sum_card_fiberwise Hf]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ a ∈ s, f a ∈ t
n : ℕ
hn : ∀ b ∈ t, n ≤ #(filter (fun a => f a = b) s)
⊢ n * #t = ∑ _a ∈ t, n

Tactic:
simp [mul_comm]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
@[simp] lemma zero_apply (x : E) : (0 : E →WOT[𝕜] F) x = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
x : E
⊢ (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm 0)).toFun x = 0

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
x : E
⊢ 0 x = 0

Tactic:
simp only [DFunLike.coe]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
x : E
⊢ (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm 0)).toFun x = 0
-- Mathlib/Order/LatticeIntervals.lean
protected lemma isCompl_iff [Lattice α] [BoundedOrder α] {x y : Iic a} :
    IsCompl x y ↔ Disjoint (x : α) (y : α) ∧ (x : α) ⊔ (y : α) = a

Proof state:
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
x y : ↑(Iic a)
⊢ IsCompl x y ↔ Disjoint ↑x ↑y ∧ ↑x ⊔ ↑y = a

Tactic:
rw [_root_.isCompl_iff, Iic.disjoint_iff, Iic.codisjoint_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem circulant_isSymm_iff [AddGroup n] {v : n → α} :
    (circulant v).IsSymm ↔ ∀ i, v (-i) = v i

Proof state:
α : Type u_1
n : Type u_3
inst✝ : AddGroup n
v : n → α
⊢ (circulant v).IsSymm ↔ ∀ (i : n), v (-i) = v i

Tactic:
rw [IsSymm, transpose_circulant, circulant_inj, funext_iff]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem mulVec_one [Fintype n] (A : Matrix m n α) : A *ᵥ 1 = ∑ j, Aᵀ j

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
⊢ A *ᵥ 1 = ∑ j : n, Aᵀ j

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x✝ : m
⊢ (A *ᵥ 1) x✝ = (∑ j : n, Aᵀ j) x✝

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x✝ : m
⊢ (A *ᵥ 1) x✝ = (∑ j : n, Aᵀ j) x✝

Tactic:
simp [mulVec, dotProduct]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem iso_symm_comp : (iso S f).symm.toLinearMap.comp f = LocalizedModule.mkLinearMap S M

Proof state:
case h.eq1
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
⊢ 1 • f m = f m

Tactic:
exact one_smul _ _

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
⊢ ↑(iso S f).symm ∘ₗ f = LocalizedModule.mkLinearMap S M

Tactic:
ext m

Result:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
⊢ (↑(iso S f).symm ∘ₗ f) m = (LocalizedModule.mkLinearMap S M) m

Proof state:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
⊢ (↑(iso S f).symm ∘ₗ f) m = (LocalizedModule.mkLinearMap S M) m

Tactic:
rw [LinearMap.comp_apply, LocalizedModule.mkLinearMap_apply, LinearEquiv.coe_coe, iso_symm_apply']

Result:
case h.eq1
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
⊢ 1 • f m = f m
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
lemma singleFunctor_map_comp_hom [HasDerivedCategory.{w'} C]
    {X Y Z : C} (f : X ⟶ Y) {n : ℕ} (x : Ext Y Z n) :
    (DerivedCategory.singleFunctor C 0).map f ≫ x.hom =
      ((mk₀ f).comp x (zero_add n)).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : HasDerivedCategory C
X Y Z : C
f : X ⟶ Y
n : ℕ
x : Ext Y Z n
⊢ (singleFunctor C 0).map f ≫ x.hom = ((mk₀ f).comp x ⋯).hom

Tactic:
simp only [comp_hom, mk₀_hom, ShiftedHom.mk₀_comp]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
theorem add_singleton_eq_iff {s t : Multiset α} {a : α} : s + {a} = t ↔ a ∈ t ∧ s = t.erase a

Proof state:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
h : a ∈ t
⊢ a ::ₘ t.erase a = t

Tactic:
exact cons_erase h

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ t ∧ s = t.erase a → a ::ₘ s = t

Tactic:
rintro ⟨h, rfl⟩

Result:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
h : a ∈ t
⊢ a ::ₘ t.erase a = t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ s + {a} = t ↔ a ∈ t ∧ s = t.erase a

Tactic:
rw [Multiset.add_comm, singleton_add]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ::ₘ s = t ↔ a ∈ t ∧ s = t.erase a

Proof state:
case mp
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ a ∈ a ::ₘ s ∧ s = (a ::ₘ s).erase a

Tactic:
exact ⟨s.mem_cons_self a, (s.erase_cons_head a).symm⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ::ₘ s = t → a ∈ t ∧ s = t.erase a

Tactic:
rintro rfl

Result:
case mp
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ a ∈ a ::ₘ s ∧ s = (a ::ₘ s).erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ::ₘ s = t ↔ a ∈ t ∧ s = t.erase a

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ::ₘ s = t → a ∈ t ∧ s = t.erase a

case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ t ∧ s = t.erase a → a ::ₘ s = t
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_of_containsKey_insertListConst [BEq α] [PartialEquivBEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
    (h₁ : containsKey k (insertListConst l toInsert))
    (h₂ : (toInsert.map Prod.fst).contains k = false) : containsKey k l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
h₁ : containsKey k (insertList l (List.map Prod.toSigma toInsert)) = true
h₂ : (List.map Prod.fst toInsert).contains k = false
⊢ containsKey k l = true

Tactic:
apply containsKey_of_containsKey_insertList h₁

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
h₁ : containsKey k (insertList l (List.map Prod.toSigma toInsert)) = true
h₂ : (List.map Prod.fst toInsert).contains k = false
⊢ (List.map Sigma.fst (List.map Prod.toSigma toInsert)).contains k = false

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
h₁ : containsKey k (insertList l (List.map Prod.toSigma toInsert)) = true
h₂ : (List.map Prod.fst toInsert).contains k = false
⊢ (List.map Sigma.fst (List.map Prod.toSigma toInsert)).contains k = false

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
h₁ : containsKey k (insertListConst l toInsert) = true
h₂ : (List.map Prod.fst toInsert).contains k = false
⊢ containsKey k l = true

Tactic:
unfold insertListConst at h₁

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
h₁ : containsKey k (insertList l (List.map Prod.toSigma toInsert)) = true
h₂ : (List.map Prod.fst toInsert).contains k = false
⊢ containsKey k l = true
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
    (h : (k == a) = false) : getKey? a (⟨k, v⟩ :: l) = getKey? a l

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

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem singleton_mul_closedBall : {x} * closedBall y δ = closedBall (x * y) δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} * closedBall y δ = closedBall (x * y) δ

Tactic:
simp_rw [singleton_mul, ← smul_eq_mul, image_smul, smul_closedBall]

Result:
no goals
-- Mathlib/Tactic/Ring/RingNF.lean
theorem nat_rawCast_0 : (Nat.rawCast 0 : R) = 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ Nat.rawCast 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem degree_restriction {p : R[X]} : (restriction p).degree = p.degree

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.restriction.degree = p.degree

Tactic:
simp [degree]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Monoid.lean
@[to_additive]
protected lemma strictMono_symm : StrictMono f.symm :=
  strictMono_of_le_iff_le <| fun a b ↦ by
    rw [← map_le_map_iff f]
    convert Iff.rfl <;>
    exact f.toEquiv.apply_symm_apply _

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ a ≤ b ↔ f (f.symm a) ≤ f (f.symm b)

Tactic:
convert Iff.rfl <;>
exact f.toEquiv.apply_symm_apply _

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ a ≤ b ↔ f.symm a ≤ f.symm b

Tactic:
rw [← map_le_map_iff f]

Result:
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ a ≤ b ↔ f (f.symm a) ≤ f (f.symm b)
-- Mathlib/Algebra/Prime/Lemmas.lean
theorem DvdNotUnit.isUnit_of_irreducible_right [CommMonoidWithZero M] {p q : M}
    (h : DvdNotUnit p q) (hq : Irreducible q) : IsUnit p

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : DvdNotUnit p q
hq : Irreducible q
⊢ IsUnit p

Tactic:
obtain ⟨_, x, hx, hx'⟩ := h

Result:
case intro.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
hq : Irreducible q
left✝ : p ≠ 0
x : M
hx : ¬IsUnit x
hx' : q = p * x
⊢ IsUnit p

Proof state:
case intro.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
hq : Irreducible q
left✝ : p ≠ 0
x : M
hx : ¬IsUnit x
hx' : q = p * x
⊢ IsUnit p

Tactic:
exact Or.resolve_right ((irreducible_iff.1 hq).right p x hx') hx

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Grading.lean
theorem mem_gradeBy_iff (f : M → ι) (i : ι) (a : R[M]) :
    a ∈ gradeBy R f i ↔ (a.support : Set M) ⊆ f ⁻¹' {i}

Proof state:
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : M → ι
i : ι
a : R[M]
⊢ a ∈ gradeBy R f i ↔ ↑a.support ⊆ f ⁻¹' {i}

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
lemma counitForward_val_fst (s : CostructuredArrow yoneda A) (x : F.obj (op s)) :
    (counitForward F s x).val.fst = s.hom

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
x : F.obj (op s)
⊢ YonedaCollection.fst (counitForward F s x).val = s.hom

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem erase_apply [DecidableEq α] {a a' : α} {f : α →₀ M} :
    f.erase a a' = if a' = a then 0 else f a'

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a a' : α
f : α →₀ M
⊢ (if a' = a then 0 else f a') = if a' = a then 0 else f a'

Tactic:
convert rfl

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a a' : α
f : α →₀ M
⊢ (erase a f) a' = if a' = a then 0 else f a'

Tactic:
rw [erase, coe_mk]

Result:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a a' : α
f : α →₀ M
⊢ (if a' = a then 0 else f a') = if a' = a then 0 else f a'
-- Mathlib/Algebra/Polynomial/Monic.lean
lemma Monic.comp_X_sub_C {p : R[X]} (hp : p.Monic) (r : R) : (p.comp (X - C r)).Monic

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
hp : p.Monic
r : R
⊢ (p.comp (X - C r)).Monic

Tactic:
simpa using hp.comp_X_add_C (-r)

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma isStrictlyLE_of_le (p q : ℤ) (hpq : p ≤ q) [K.IsStrictlyLE p] :
    K.IsStrictlyLE q

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyLE p
⊢ K.IsStrictlyLE q

Tactic:
rw [isStrictlyLE_iff]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyLE p
⊢ ∀ (i : ℤ), q < i → IsZero (K.X i)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyLE p
⊢ ∀ (i : ℤ), q < i → IsZero (K.X i)

Tactic:
intro i hi

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyLE p
i : ℤ
hi : q < i
⊢ IsZero (K.X i)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyLE p
i : ℤ
hi : q < i
⊢ IsZero (K.X i)

Tactic:
apply K.isZero_of_isStrictlyLE p

Result:
case hi
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyLE p
i : ℤ
hi : q < i
⊢ p < i

Proof state:
case hi
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyLE p
i : ℤ
hi : q < i
⊢ p < i

Tactic:
omega

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem sameCycle_one : SameCycle 1 x y ↔ x = y

Proof state:
α : Type u_2
x y : α
⊢ SameCycle 1 x y ↔ x = y

Tactic:
simp [SameCycle]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem interior_eq_empty_iff_dense_compl : interior s = ∅ ↔ Dense sᶜ

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ interior s = ∅ ↔ Dense sᶜ

Tactic:
rw [dense_iff_closure_eq, closure_compl, compl_univ_iff]

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem PythagoreanTriple.zero : PythagoreanTriple 0 0 0

Proof state:
⊢ PythagoreanTriple 0 0 0

Tactic:
simp only [PythagoreanTriple, zero_mul, zero_add]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive (attr := simp)] lemma inv_mul_cancel_comm_assoc (a b : G) : a⁻¹ * (b * a) = b

Proof state:
G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a⁻¹ * (b * a) = b

Tactic:
rw [mul_comm, mul_inv_cancel_right]

Result:
no goals
-- Mathlib/Topology/Algebra/ConstMulAction.lean
theorem continuous_const_smul_iff (c : G) : (Continuous fun x => c • f x) ↔ Continuous f

Proof state:
α : Type u_2
β : Type u_3
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
inst✝ : TopologicalSpace β
f : β → α
c : G
⊢ (Continuous fun x => c • f x) ↔ Continuous f

Tactic:
simp only [continuous_iff_continuousAt, continuousAt_const_smul_iff]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
theorem limsup_eq_bot : f.limsup u = ⊥ ↔ u =ᶠ[f] ⊥ :=
  ⟨fun h =>
    (EventuallyLE.trans eventually_le_limsup <| Eventually.of_forall fun _ => h.le).mono fun _ hx =>
      le_antisymm hx bot_le,
    fun h => by
    rw [limsup_congr h]
    exact limsup_const_bot⟩

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : CompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : FirstCountableTopology α
inst✝¹ : OrderTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
h : u =ᶠ[f] ⊥
⊢ limsup ⊥ f = ⊥

Tactic:
exact limsup_const_bot

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : CompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : FirstCountableTopology α
inst✝¹ : OrderTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
h : u =ᶠ[f] ⊥
⊢ limsup u f = ⊥

Tactic:
rw [limsup_congr h]

Result:
α : Type u_2
β : Type u_3
inst✝⁴ : CompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : FirstCountableTopology α
inst✝¹ : OrderTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
h : u =ᶠ[f] ⊥
⊢ limsup ⊥ f = ⊥