harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_zero_iff_eq_of_closed (hs : IsClosed s) (ht : IsClosed t) :
    hausdorffEdist s t = 0 ↔ s = t

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsClosed s
ht : IsClosed t
⊢ hausdorffEdist s t = 0 ↔ s = t

Tactic:
rw [hausdorffEdist_zero_iff_closure_eq_closure, hs.closure_eq, ht.closure_eq]

Result:
no goals
-- Mathlib/GroupTheory/PushoutI.lean
theorem prod_base_smul (h : H) (w : NormalWord d) :
    (h • w).prod = base φ h * w.prod

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
h : H
w : NormalWord d
⊢ (h • w).prod = (base φ) h * w.prod

Tactic:
simp only [base_smul_def', prod, map_mul, mul_assoc]

Result:
no goals
-- Mathlib/Logic/Denumerable.lean
theorem prod_ofNat_val (n : ℕ) :
    ofNat (α × β) n = (ofNat α (unpair n).1, ofNat β (unpair n).2)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ofNat (α × β) n = (ofNat α (unpair n).1, ofNat β (unpair n).2)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Basic.lean
lemma MapsTo.perm_pow : MapsTo f s s → ∀ n : ℕ, MapsTo (f ^ n) s s

Proof state:
α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (⇑f) s s → ∀ (n : ℕ), MapsTo (⇑(f ^ n)) s s

Tactic:
simp_rw [Equiv.Perm.coe_pow]

Result:
α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (⇑f) s s → ∀ (n : ℕ), MapsTo (⇑f)^[n] s s

Proof state:
α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (⇑f) s s → ∀ (n : ℕ), MapsTo (⇑f)^[n] s s

Tactic:
exact MapsTo.iterate

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasFDerivAtFilter_id (x : E) (L : Filter E) : HasFDerivAtFilter id (id 𝕜 E) x L :=
  .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left <| by simp

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
L : Filter E
⊢ ∀ (x_1 : E), 0 x_1 = _root_.id x_1 - _root_.id x - (ContinuousLinearMap.id 𝕜 E) (x_1 - x)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Free.lean
theorem rank_mul_rank (A : Type v) [AddCommGroup A]
    [Module K A] [Module F A] [IsScalarTower F K A] [Module.Free K A] :
    Module.rank F K * Module.rank K A = Module.rank F A

Proof state:
F : Type u
K : Type v
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : Module F K
inst✝⁷ : StrongRankCondition F
inst✝⁶ : StrongRankCondition K
inst✝⁵ : Free F K
A : Type v
inst✝⁴ : AddCommGroup A
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : Free K A
⊢ Module.rank F K * Module.rank K A = Module.rank F A

Tactic:
convert lift_rank_mul_lift_rank F K A <;> rw [lift_id]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem isSt_iff_tendsto {x : ℝ*} {r : ℝ} : IsSt x r ↔ x.Tendsto (𝓝 r)

Proof state:
x : ℝ*
r : ℝ
⊢ x.IsSt r ↔ Germ.Tendsto x (𝓝 r)

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩

Result:
case intro
r : ℝ
f : ℕ → ℝ
⊢ (ofSeq f).IsSt r ↔ Germ.Tendsto (ofSeq f) (𝓝 r)

Proof state:
case intro
r : ℝ
f : ℕ → ℝ
⊢ (ofSeq f).IsSt r ↔ Germ.Tendsto (ofSeq f) (𝓝 r)

Tactic:
exact isSt_ofSeq_iff_tendsto

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem exists_eq_left' : (∃ a, a' = a ∧ p a) ↔ p a'

Proof state:
α : Sort u_1
p : α → Prop
a' : α
⊢ (∃ a, a' = a ∧ p a) ↔ p a'

Tactic:
simp [@eq_comm _ a']

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem Continuous.closure_preimage_subset (hf : Continuous f) (t : Set Y) :
    closure (f ⁻¹' t) ⊆ f ⁻¹' closure t

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
t : Set Y
⊢ closure (f ⁻¹' t) ⊆ f ⁻¹' closure t

Tactic:
rw [← (isClosed_closure.preimage hf).closure_eq]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
t : Set Y
⊢ closure (f ⁻¹' t) ⊆ closure (f ⁻¹' closure t)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
t : Set Y
⊢ closure (f ⁻¹' t) ⊆ closure (f ⁻¹' closure t)

Tactic:
exact closure_mono (preimage_mono subset_closure)

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem aevalTower_id : aevalTower (AlgHom.id S S) = aeval

Proof state:
S : Type v
inst✝ : CommSemiring S
⊢ aevalTower (AlgHom.id S S) = aeval

Tactic:
ext s

Result:
case h.hX
S : Type v
inst✝ : CommSemiring S
s : S
⊢ (aevalTower (AlgHom.id S S) s) X = (aeval s) X

Proof state:
case h.hX
S : Type v
inst✝ : CommSemiring S
s : S
⊢ (aevalTower (AlgHom.id S S) s) X = (aeval s) X

Tactic:
simp only [eval_X, aevalTower_X, coe_aeval_eq_eval]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem add_nat_iff : LiouvilleWith p (x + n) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
n : ℕ
⊢ LiouvilleWith p (x + ↑n) ↔ LiouvilleWith p x

Tactic:
rw [← Rat.cast_natCast n, add_rat_iff]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_add_lt_pi_div_two_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0) :
    angle x (x + y) < π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ angle x (x + y) < π / 2

Tactic:
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_lt_pi_div_two,
  norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ 0 < ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ 0 < ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)

Tactic:
exact div_pos (norm_pos_iff.2 h0) (Real.sqrt_pos.2 (Left.add_pos_of_pos_of_nonneg
  (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)))

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigOWith_of_le (hfg : ∀ x, ‖f x‖ ≤ ‖g x‖) : IsBigOWith 1 l f g :=
  isBigOWith_of_le' l fun x => by
    rw [one_mul]
    exact hfg x

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
x : α
⊢ ‖f x‖ ≤ 1 * ‖g x‖

Tactic:
rw [one_mul]

Result:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
x : α
⊢ ‖f x‖ ≤ ‖g x‖

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
x : α
⊢ ‖f x‖ ≤ ‖g x‖

Tactic:
exact hfg x

Result:
no goals
-- Mathlib/RingTheory/Localization/AsSubring.lean
theorem map_isUnit_of_le (hS : S ≤ A⁰) (s : S) : IsUnit (algebraMap A K s)

Proof state:
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
s : ↥S
⊢ IsUnit ((algebraMap A K) ↑s)

Tactic:
apply IsLocalization.map_units K (⟨s.1, hS s.2⟩ : A⁰)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_false_same : ∀(c b : Bool), cond c b c = (c && b)

Proof state:
⊢ ∀ (c b : Bool), (bif c then b else c) = (c && b)

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/FreeCommRing.lean
theorem coe_neg (x : FreeRing α) : ↑(-x) = -(x : FreeCommRing α)

Proof state:
α : Type u
x : FreeRing α
⊢ ↑(-x) = -↑x

Tactic:
rw [castFreeCommRing, map_neg]

Result:
no goals
-- Mathlib/Algebra/Homology/Homotopy.lean
lemma dNext_eq_zero (f : ∀ i j, C.X i ⟶ D.X j) (i : ι) (hi : ¬ c.Rel i (c.next i)) :
    dNext i f = 0

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ C.d i (c.next i) ≫ f (c.next i) i = 0

Tactic:
rw [shape _ _ _ hi, zero_comp]

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (dNext i) f = 0

Tactic:
dsimp [dNext]

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ C.d i (c.next i) ≫ f (c.next i) i = 0
-- Mathlib/Data/Set/Image.lean
theorem preimage_coe_inter_self (s t : Set α) :
    ((↑) : s → α) ⁻¹' (t ∩ s) = ((↑) : s → α) ⁻¹' t

Proof state:
α : Type u_1
s t : Set α
⊢ val ⁻¹' (t ∩ s) = val ⁻¹' t

Tactic:
rw [inter_comm, preimage_coe_self_inter]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
lemma map_filter' {f : α → β} (hf : Injective f) (s : Multiset α)
    [DecidablePred fun b => ∃ a, p a ∧ f a = b] :
    (s.filter p).map f = (s.map f).filter fun b => ∃ a, p a ∧ f a = b

Proof state:
α : Type u_1
β : Type v
p : α → Prop
inst✝¹ : DecidablePred p
f : α → β
hf : Injective f
s : Multiset α
inst✝ : DecidablePred fun b => ∃ a, p a ∧ f a = b
⊢ map f (filter p s) = filter (fun b => ∃ a, p a ∧ f a = b) (map f s)

Tactic:
simp [comp_def, filter_map, hf.eq_iff]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toMeasure_apply_eq_of_inter_support_eq {s t : Set α} (hs : MeasurableSet s)
    (ht : MeasurableSet t) (h : s ∩ p.support = t ∩ p.support) : p.toMeasure s = p.toMeasure t

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
p : PMF α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : s ∩ p.support = t ∩ p.support
⊢ p.toMeasure s = p.toMeasure t

Tactic:
simpa only [p.toMeasure_apply_eq_toOuterMeasure_apply, hs, ht] using
  toOuterMeasure_apply_eq_of_inter_support_eq p h

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Comap.lean
theorem comapₗ_apply {_ : MeasurableSpace α} {_ : MeasurableSpace β} (f : α → β)
    (hfi : Injective f) (hf : ∀ s, MeasurableSet s → MeasurableSet (f '' s)) (μ : Measure β)
    (hs : MeasurableSet s) : comapₗ f μ s = μ (f '' s)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ ((comapₗ f) μ) s = μ (f '' s)

Tactic:
rw [comapₗ, dif_pos, liftLinear_apply _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure]

Result:
case hc
α : Type u_1
β : Type u_2
s : Set α
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)

case hc
α : Type u_1
β : Type u_2
s : Set α
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)

Proof state:
case hc
α : Type u_1
β : Type u_2
s : Set α
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)

case hc
α : Type u_1
β : Type u_2
s : Set α
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)

Tactic:
exact ⟨hfi, hf⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem natAbs_eq_iff {a : Int} {n : Nat} : a.natAbs = n ↔ a = n ∨ a = -↑n

Proof state:
a : Int
n : Nat
⊢ a.natAbs = n ↔ a = ↑n ∨ a = -↑n

Tactic:
rw [← Int.natAbs_eq_natAbs_iff, Int.natAbs_ofNat]

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem toSubmodule_injective :
    Function.Injective (toSubmodule : NonUnitalSubalgebra R A → Submodule R A) := fun S T h =>
  ext fun x => by rw [← mem_toSubmodule, ← mem_toSubmodule, h]

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
S T : NonUnitalSubalgebra R A
h : S.toSubmodule = T.toSubmodule
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toSubmodule, ← mem_toSubmodule, h]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem _root_.AffineIsometry.angle_map {V₂ P₂ : Type*} [NormedAddCommGroup V₂]
    [InnerProductSpace ℝ V₂] [MetricSpace P₂] [NormedAddTorsor V₂ P₂]
    (f : P →ᵃⁱ[ℝ] P₂) (p₁ p₂ p₃ : P) : ∠ (f p₁) (f p₂) (f p₃) = ∠ p₁ p₂ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[ℝ] P₂
p₁ p₂ p₃ : P
⊢ ∠ (f p₁) (f p₂) (f p₃) = ∠ p₁ p₂ p₃

Tactic:
simp_rw [angle, ← AffineIsometry.map_vsub, LinearIsometry.angle_map]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem getElem_insertIdx_lt (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
    (k) (h' : k < (as.insertIdx i v).size) (h : k < i) :
    (as.insertIdx i v)[k] = as[k]

Proof state:
α : Type u_1
as : Array α
i : Nat
h✝ : i ≤ as.size
v : α
k : Nat
h' : k < (as.insertIdx i v h✝).size
h : k < i
⊢ (as.insertIdx i v h✝)[k] = as[k]

Tactic:
simp [getElem_insertIdx, h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem exists_measurable_superset_forall_eq [Countable ι] (μ : ι → Measure α) (s : Set α) :
    ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ i, μ i t = μ i s

Proof state:
α : Type u_1
ι : Sort u_5
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
μ : ι → Measure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i) s

Tactic:
simpa only [← measure_eq_trim] using
  OuterMeasure.exists_measurable_superset_forall_eq_trim (fun i => (μ i).toOuterMeasure) s

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem toMeasure_map_apply (hf : Measurable f)
    (hs : MeasurableSet s) : (p.map f).toMeasure s = p.toMeasure (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
mα : MeasurableSpace α
mβ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ (map f p).toMeasure s = p.toMeasure (f ⁻¹' s)

Tactic:
rw [toMeasure_apply_eq_toOuterMeasure_apply _ s hs,
  toMeasure_apply_eq_toOuterMeasure_apply _ (f ⁻¹' s) (measurableSet_preimage hf hs)]

Result:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
mα : MeasurableSpace α
mβ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ (map f p).toOuterMeasure s = p.toOuterMeasure (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
mα : MeasurableSpace α
mβ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ (map f p).toOuterMeasure s = p.toOuterMeasure (f ⁻¹' s)

Tactic:
exact toOuterMeasure_map_apply f p s

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_image_source_inter :
    f.extend I '' (f.source ∩ f'.source) = ((f.extend I).symm ≫ f'.extend I).source

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ↑(f.extend I) '' (f.source ∩ f'.source) = ((f.extend I).symm ≫ f'.extend I).source

Tactic:
simp_rw [f.extend_coord_change_source, f.extend_coe, image_comp I f, trans_source'', symm_symm,
  symm_target]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_mono : Monotone (@card α)

Proof state:
α : Type u_1
⊢ Monotone card

Tactic:
apply card_le_card

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
@[simp]
lemma natAbs_odd : Odd n.natAbs ↔ Odd n

Proof state:
n : ℤ
⊢ Odd n.natAbs ↔ Odd n

Tactic:
rw [← not_even_iff_odd, ← Nat.not_even_iff_odd, natAbs_even]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range_eq_range' (n : Nat) : range n = range' 0 n

Proof state:
n : Nat
⊢ range n = range' 0 n

Tactic:
simp [range, range']

Result:
no goals
-- Mathlib/Data/Finset/NatAntidiagonal.lean
lemma antidiagonal_eq_image (n : ℕ) :
    antidiagonal n = (range (n + 1)).image fun i ↦ (i, n - i)

Proof state:
n : ℕ
⊢ antidiagonal n = image (fun i => (i, n - i)) (range (n + 1))

Tactic:
simp only [antidiagonal_eq_map, map_eq_image, Function.Embedding.coeFn_mk]

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
lemma cast_eq_mod (p : ℕ) [CharP R p] (k : ℕ) : (k : R) = (k % p : ℕ) :=
  calc
    (k : R) = ↑(k % p + p * (k / p))

Proof state:
R : Type u_1
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ ↑(k % p + p * (k / p)) = ↑(k % p)

Tactic:
simp [cast_eq_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ ↑k = ↑(k % p + p * (k / p))

Tactic:
rw [Nat.mod_add_div]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem interior_compl : interior sᶜ = (closure s)ᶜ

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ interior sᶜ = (closure s)ᶜ

Tactic:
simp [closure_eq_compl_interior_compl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_cons_tail {a b : α} {l : List α} (h : ¬(b == a)) :
    (b :: l).erase a = b :: l.erase a

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
l : List α
h : ¬(b == a) = true
⊢ (b :: l).erase a = b :: l.erase a

Tactic:
simp only [erase_cons, if_neg h]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.rotate_iff [NoZeroSMulDivisors R V] {x y z : P} (h : Wbtw R x y z) :
    Wbtw R z x y ↔ x = y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y z : P
h : Wbtw R x y z
⊢ Wbtw R z x y ↔ x = y

Tactic:
rw [← wbtw_rotate_iff R x, and_iff_right h]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem U_add_one (n : ℤ) : U R (n + 1) = 2 * X * U R n - U R (n - 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R (n + 1) = 2 * X * U R n - U R (n - 1)

Tactic:
linear_combination (norm := ring_nf) U_add_two R (n - 1)

Result:
no goals
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem projIcc_of_mem (hx : x ∈ Icc a b) : projIcc a b h x = ⟨x, hx⟩

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ projIcc a b h x = ⟨x, hx⟩

Tactic:
simp [projIcc, hx.1, hx.2]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_ofList [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} {k : α} :
    (ofList l).contains k = (l.map Sigma.fst).contains k

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k : α
⊢ (ofList l).contains k = (List.map Sigma.fst l).contains k

Tactic:
simp_to_raw using Raw₀.contains_insertMany_empty_list

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem mem_support_nil_iff {u v : V} : u ∈ (nil : G.Walk v v).support ↔ u = v

Proof state:
V : Type u
G : SimpleGraph V
u v : V
⊢ u ∈ nil.support ↔ u = v

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
theorem LSeriesSummable_zero {s : ℂ} : LSeriesSummable 0 s

Proof state:
s : ℂ
⊢ LSeriesSummable 0 s

Tactic:
simp [LSeriesSummable, funext (term_def 0 s), summable_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem map₂_eq_range_lift_comp_mapIncl (f : P →ₗ[R] Q →ₗ[R] M)
    (p : Submodule R P) (q : Submodule R Q) :
    Submodule.map₂ f p q = LinearMap.range (lift f ∘ₗ mapIncl p q)

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
P : Type u_7
Q : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R M
inst✝¹ : Module R Q
inst✝ : Module R P
f : P →ₗ[R] Q →ₗ[R] M
p : Submodule R P
q : Submodule R Q
⊢ Submodule.map₂ f p q = range (lift f ∘ₗ mapIncl p q)

Tactic:
simp_rw [LinearMap.range_comp, range_mapIncl, Submodule.map_span,
  Set.image_image2, Submodule.map₂_eq_span_image2, lift.tmul]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean
lemma fromFreeYoneda_app_apply (m : M.Elements) :
    m.fromFreeYoneda.app m.1 (ModuleCat.freeMk (𝟙 _)) = m.2

Proof state:
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ (ConcreteCategory.hom (m.fromFreeYoneda.app m.fst)) (ModuleCat.freeMk (𝟙 (Opposite.unop m.fst))) = m.snd

Tactic:
apply freeYonedaEquiv_symm_app

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem length_leftInvSeq (ω : List B) : (lis ω).length = ω.length

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ (cs.leftInvSeq ω).length = ω.length

Tactic:
simp [leftInvSeq_eq_reverse_rightInvSeq_reverse]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.sameRay_vsub_right {x y z : P} (h : Wbtw R x y z) : SameRay R (z -ᵥ x) (z -ᵥ y)

Proof state:
case intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
left✝ : 0 ≤ t
ht1 : t ≤ 1
⊢ SameRay R (z -ᵥ x) (z -ᵥ (lineMap x z) t)

Tactic:
simpa [lineMap_apply, vsub_vadd_eq_vsub_sub, sub_smul] using
  SameRay.sameRay_nonneg_smul_right (z -ᵥ x) (sub_nonneg.2 ht1)

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ SameRay R (z -ᵥ x) (z -ᵥ y)

Tactic:
rcases h with ⟨t, ⟨_, ht1⟩, rfl⟩

Result:
case intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
left✝ : 0 ≤ t
ht1 : t ≤ 1
⊢ SameRay R (z -ᵥ x) (z -ᵥ (lineMap x z) t)
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem Set.Finite.multipliable {s : Set β} (hs : s.Finite) (f : β → α) :
    Multipliable (f ∘ (↑) : s → α)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
hs : s.Finite
f : β → α
this : Multipliable (f ∘ Subtype.val)
⊢ Multipliable (f ∘ Subtype.val)

Tactic:
rwa [hs.coe_toFinset] at this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
hs : s.Finite
f : β → α
⊢ Multipliable (f ∘ Subtype.val)

Tactic:
have := hs.toFinset.multipliable f

Result:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
hs : s.Finite
f : β → α
this : Multipliable (f ∘ Subtype.val)
⊢ Multipliable (f ∘ Subtype.val)
-- Mathlib/CategoryTheory/Monoidal/Braided/Opposite.lean
@[simp] lemma unop_tensorμ {C : Type*} [Category C] [MonoidalCategory C]
    [BraidedCategory C] (X Y W Z : Cᵒᵖ) :
    (tensorμ X W Y Z).unop = tensorμ X.unop Y.unop W.unop Z.unop

Proof state:
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y W Z : Cᵒᵖ
⊢ (tensorμ X W Y Z).unop = tensorμ (unop X) (unop Y) (unop W) (unop Z)

Tactic:
simp only [unop_tensorObj, tensorμ, unop_comp, unop_inv_associator, unop_whiskerLeft,
  unop_hom_associator, unop_whiskerRight, unop_hom_braiding, Category.assoc]

Result:
no goals
-- Mathlib/Data/Nat/Pairing.lean
theorem iSup_unpair {α} [CompleteLattice α] (f : ℕ → ℕ → α) :
    ⨆ n : ℕ, f n.unpair.1 n.unpair.2 = ⨆ (i : ℕ) (j : ℕ), f i j

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → ℕ → α
⊢ ⨆ n, f (unpair n).1 (unpair n).2 = ⨆ i, ⨆ j, f i j

Tactic:
rw [← (iSup_prod : ⨆ i : ℕ × ℕ, f i.1 i.2 = _), ← Nat.surjective_unpair.iSup_comp]

Result:
no goals