harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem le_inv_of_neg (ha : a < 0) (hb : b < 0) : a ≤ b⁻¹ ↔ b ≤ a⁻¹

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
ha : a < 0
hb : b < 0
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹

Tactic:
rw [← inv_le_inv_of_neg (inv_lt_zero.2 hb) ha, inv_inv]

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
lemma filter_sups_le [DecidableRel (α := α) (· ≤ ·)] (s t : Finset α) (a : α) :
    {b ∈ s ⊻ t | b ≤ a} = {b ∈ s | b ≤ a} ⊻ {b ∈ t | b ≤ a}

Proof state:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : SemilatticeSup α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
s t : Finset α
a : α
⊢ filter (fun b => b ≤ a) (s ⊻ t) = filter (fun b => b ≤ a) s ⊻ filter (fun b => b ≤ a) t

Tactic:
simp only [← coe_inj, coe_filter, coe_sups, ← mem_coe, Set.sep_sups_le]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iInf_inf [Nonempty ι] {f : ι → α} {a : α} : (⨅ x, f x) ⊓ a = ⨅ x, f x ⊓ a

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ (⨅ x, f x) ⊓ a = ⨅ x, f x ⊓ a

Tactic:
rw [iInf_inf_eq, iInf_const]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderEmbedding.lean
theorem preimage_uIcc [Lattice β] (e : α ↪o β) (x y : α) :
    e ⁻¹' (uIcc (e x) (e y)) = uIcc x y

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' uIcc (e x) (e y) = uIcc x y

Tactic:
cases le_total x y <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_of_le_neg_one {x : ℝ} (hx : x ≤ -1) : arcsin x = -(π / 2)

Proof state:
x : ℝ
hx : x ≤ -1
⊢ arcsin x = -(π / 2)

Tactic:
rw [← arcsin_projIcc, projIcc_of_le_left _ hx, Subtype.coe_mk, arcsin_neg_one]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Basic.lean
theorem mem_pretrivializationAt_source (b : B) (x : E b) :
    ⟨b, x⟩ ∈ (a.pretrivializationAt b).source

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
x : E b
⊢ { proj := b, snd := x } ∈ (a.pretrivializationAt b).source

Tactic:
simp only [(a.pretrivializationAt b).source_eq, mem_preimage, TotalSpace.proj]

Result:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
x : E b
⊢ b ∈ (a.pretrivializationAt b).baseSet

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
x : E b
⊢ b ∈ (a.pretrivializationAt b).baseSet

Tactic:
exact a.mem_base_pretrivializationAt b

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem symm_toLinearEquiv (e : M₁ ≃SL[σ₁₂] M₂) : e.symm.toLinearEquiv = e.toLinearEquiv.symm

Proof state:
case h
R₁ : Type u_3
R₂ : Type u_4
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_6
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_7
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x✝ : M₂
⊢ e.symm.toLinearEquiv x✝ = e.symm x✝

Tactic:
rfl

Result:
no goals

Proof state:
R₁ : Type u_3
R₂ : Type u_4
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_6
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_7
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ e.symm.toLinearEquiv = e.symm

Tactic:
ext

Result:
case h
R₁ : Type u_3
R₂ : Type u_4
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_6
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_7
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x✝ : M₂
⊢ e.symm.toLinearEquiv x✝ = e.symm x✝
-- Mathlib/Data/Num/Lemmas.lean
theorem mod_to_nat : ∀ n d, ((n % d : Num) : ℕ) = n % d
  | 0, 0 => by simp
  | 0, pos _ => (Nat.zero_mod _).symm
  | pos _, 0 => (Nat.mod_zero _).symm
  | pos _, pos _ => PosNum.mod'_to_nat _ _

Proof state:
⊢ ↑(0 % 0) = ↑0 % ↑0

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem dist_self : dist G v v = 0

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
⊢ G.dist v v = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α}
    {f : Option β → Option β} (h : m.WF) (he : (k == k') = false) :
    (Const.alter m k f).contains k' = m.contains k'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
h : m.WF
he : (k == k') = false
⊢ (alter m k f).contains k' = m.contains k'

Tactic:
simp only [contains_alter h, he, Bool.false_eq_true, reduceIte]

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem toStalk_stalkSpecializes {R : Type*} [CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) :
    toStalk R y ≫ (structureSheaf R).presheaf.stalkSpecializes h = toStalk R x

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (toOpen R ⊤ ≫ (structureSheaf R).presheaf.germ ⊤ y True.intro) ≫ (structureSheaf R).presheaf.stalkSpecializes h =
    toOpen R ⊤ ≫ (structureSheaf R).presheaf.germ ⊤ x True.intro

Tactic:
simp [-toOpen_germ]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ toStalk R y ≫ (structureSheaf R).presheaf.stalkSpecializes h = toStalk R x

Tactic:
dsimp [toStalk]

Result:
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (toOpen R ⊤ ≫ (structureSheaf R).presheaf.germ ⊤ y True.intro) ≫ (structureSheaf R).presheaf.stalkSpecializes h =
    toOpen R ⊤ ≫ (structureSheaf R).presheaf.germ ⊤ x True.intro
-- Mathlib/CategoryTheory/NatIso.lean
theorem naturality_2' (α : F ⟶ G) (f : X ⟶ Y) {_ : IsIso (α.app Y)} :
    α.app X ≫ G.map f ≫ inv (α.app Y) = F.map f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
α : F ⟶ G
f : X ⟶ Y
x✝ : IsIso (α.app Y)
⊢ α.app X ≫ G.map f ≫ inv (α.app Y) = F.map f

Tactic:
rw [← Category.assoc, ← naturality, Category.assoc, IsIso.hom_inv_id, Category.comp_id]

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
lemma univ_map_subtype [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype {a // p a}] :
    univ.map (Function.Embedding.subtype p) = univ.filter p

Proof state:
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ map (Embedding.subtype p) univ = filter p univ

Tactic:
rw [← subtype_map, subtype_univ]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem coeff_zero_X (i : σ) : coeff 0 (X i : MvPolynomial σ R) = 0 :=
  single_eq_of_ne fun h => by cases Finsupp.single_eq_zero.1 h

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
h : Finsupp.single i 1 = 0
⊢ False

Tactic:
cases Finsupp.single_eq_zero.1 h

Result:
no goals
-- Mathlib/Algebra/Module/CharacterModule.lean
theorem _root_.rTensor_injective_iff_lcomp_surjective {f : A →ₗ[R] A'} :
    Function.Injective (f.rTensor B) ↔ Function.Surjective (f.lcomp R <| CharacterModule B)

Proof state:
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
f : A →ₗ[R] A'
⊢ Function.Injective ⇑(LinearMap.rTensor B f) ↔ Function.Surjective ⇑(LinearMap.lcomp R (CharacterModule B) f)

Tactic:
simp [← dual_rTensor_conj_homEquiv, dual_surjective_iff_injective]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/EpiMono.lean
theorem reflectsEpimorphisms.of_iso {F G : C ⥤ D} [ReflectsEpimorphisms F] (α : F ≅ G) :
    ReflectsEpimorphisms G :=
  { reflects := fun {X} {Y} f h => by
      apply F.epi_of_epi_map
      suffices F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv from this ▸ epi_comp _ _
      rw [← Category.assoc, Iso.eq_comp_inv, Iso.app_hom, Iso.app_hom, NatTrans.naturality] }

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.ReflectsEpimorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
⊢ Epi f

Tactic:
apply F.epi_of_epi_map

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.ReflectsEpimorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
⊢ Epi (F.map f)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.ReflectsEpimorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
⊢ Epi (F.map f)

Tactic:
suffices F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv from this ▸ epi_comp _ _

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.ReflectsEpimorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
⊢ F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.ReflectsEpimorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
⊢ F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv

Tactic:
rw [← Category.assoc, Iso.eq_comp_inv, Iso.app_hom, Iso.app_hom, NatTrans.naturality]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Icc_iff_integrableOn_Ioo :
    IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [integrableOn_Icc_iff_integrableOn_Ioc, integrableOn_Ioc_iff_integrableOn_Ioo]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem measure_prod_null {s : Set (α × β)} (hs : MeasurableSet s) :
    μ.prod ν s = 0 ↔ (fun x => ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.prod ν) s = 0 ↔ (fun x => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0

Tactic:
rw [prod_apply hs, lintegral_eq_zero_iff (measurable_measure_prod_mk_left hs)]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Pi.lean
@[simp]
lemma piRight_apply (x : N ⊗[R] (∀ i, M i)) :
    piRight R S N M x = piRightHom R S N M x

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N ⊗[R] ((i : ι) → M i)
⊢ (piRight R S N M) x = (piRightHom R S N M) x

Tactic:
rfl

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem equivOfEq_rfl (S : IntermediateField F E) : equivOfEq (rfl : S = S) = AlgEquiv.refl

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : IntermediateField F E
⊢ equivOfEq ⋯ = AlgEquiv.refl

Tactic:
ext

Result:
case h.a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : IntermediateField F E
a✝ : ↥S
⊢ ↑((equivOfEq ⋯) a✝) = ↑(AlgEquiv.refl a✝)

Proof state:
case h.a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : IntermediateField F E
a✝ : ↥S
⊢ ↑((equivOfEq ⋯) a✝) = ↑(AlgEquiv.refl a✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem pi_empty_univ {α : Type*} [Fintype α] [IsEmpty α] {β : α → Type*}
    {m : ∀ α, MeasurableSpace (β α)} (μ : ∀ a : α, Measure (β a)) :
    Measure.pi μ (Set.univ) = 1

Proof state:
α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (α : α) → MeasurableSpace (β α)
μ : (a : α) → Measure (β a)
⊢ (Measure.pi μ) univ = 1

Tactic:
rw [pi_of_empty, measure_univ]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem mem_box_iff_index {x : ι → ℝ} {ν : ι → ℤ} :
    x ∈ box n ν ↔ index n x = ν

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
x : ι → ℝ
ν : ι → ℤ
⊢ x ∈ box n ν ↔ index n x = ν

Tactic:
simp_rw [mem_box_iff', funext_iff, index_apply, sub_eq_iff_eq_add, Int.ceil_eq_iff,
  Int.cast_add, Int.cast_one, add_sub_cancel_right]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean
theorem of_convergence [TopologicalSpace K] [OrderTopology K] :
    Filter.Tendsto (of v).convs Filter.atTop <| 𝓝 v

Proof state:
K : Type u_1
v : K
inst✝⁴ : LinearOrderedField K
inst✝³ : FloorRing K
inst✝² : Archimedean K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
⊢ Filter.Tendsto (of v).convs Filter.atTop (𝓝 v)

Tactic:
simpa [LinearOrderedAddCommGroup.tendsto_nhds, abs_sub_comm] using of_convergence_epsilon v

Result:
no goals
-- Mathlib/CategoryTheory/DiscreteCategory.lean
theorem natIso_app {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i)
    (i : Discrete I) : (Discrete.natIso f).app i = f i

Proof state:
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
i : Discrete I
⊢ (natIso f).app i = f i

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem hasStrictFDerivAt_iff_hasStrictDerivAt {f' : 𝕜 →L[𝕜] F} :
    HasStrictFDerivAt f f' x ↔ HasStrictDerivAt f (f' 1) x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
inst✝ : ContinuousSMul 𝕜 F
f' : 𝕜 →L[𝕜] F
⊢ HasStrictFDerivAt f f' x ↔ HasStrictDerivAt f (f' 1) x

Tactic:
simp [HasStrictDerivAt, HasStrictFDerivAt]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem expSeries_eq_expSeries (n : ℕ) (x : 𝔸) :
    (expSeries 𝕂 𝔸 n fun _ => x) = expSeries 𝕂' 𝔸 n fun _ => x

Proof state:
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
n : ℕ
x : 𝔸
⊢ ((expSeries 𝕂 𝔸 n) fun x_1 => x) = (expSeries 𝕂' 𝔸 n) fun x_1 => x

Tactic:
rw [expSeries_apply_eq, expSeries_apply_eq, inv_natCast_smul_eq 𝕂 𝕂']

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
@[simp]
lemma pushout.desc_inl_inr {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] :
    desc (inl f g) (inr f g) condition = 𝟙 (pushout f g)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ desc (inl f g) (inr f g) ⋯ = 𝟙 (pushout f g)

Tactic:
apply hom_ext <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean
theorem Module.finrank_linearMap_self : finrank S (M →ₗ[R] S) = finrank R M

Proof state:
R : Type u
S : Type u'
M : Type v
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : StrongRankCondition R
inst✝² : StrongRankCondition S
inst✝¹ : Module R S
inst✝ : SMulCommClass R S S
⊢ finrank S (M →ₗ[R] S) = finrank R M

Tactic:
rw [finrank_linearMap, finrank_self, mul_one]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem truncateFun_sub (x y : 𝕎 R) :
    truncateFun n (x - y) = truncateFun n x - truncateFun n y

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ truncateFun n (x - y) = truncateFun n x - truncateFun n y

Tactic:
witt_truncateFun_tac

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem measure_eq_tsum_of_ac (h : IsFundamentalDomain G s μ) (hν : ν ≪ μ) (t : Set α) :
    ν t = ∑' g : G, ν (t ∩ g • s)

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
t : Set α
⊢ ν t = ∑' (g : G), ν (t ∩ g • s)

Tactic:
have H : ν.restrict t ≪ μ := Measure.restrict_le_self.absolutelyContinuous.trans hν

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
t : Set α
H : ν.restrict t ≪ μ
⊢ ν t = ∑' (g : G), ν (t ∩ g • s)

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

Tactic:
simpa only [setLIntegral_one, Pi.one_def,
  Measure.restrict_apply₀ ((h.nullMeasurableSet_smul _).mono_ac H), inter_comm] using
  h.lintegral_eq_tsum_of_ac H 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/GetElem.lean
theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
    [Inhabited elem] (c : cont) (i : idx) (h : dom c i) :
    c[i]! = c[i]'h

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
inst✝ : Inhabited elem
c : cont
i : idx
h : dom c i
this : Decidable (dom c i)
⊢ getElem! c i = getElem c i h

Tactic:
simp [getElem!_def, getElem?_def, h]

Result:
no goals

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
inst✝ : Inhabited elem
c : cont
i : idx
h : dom c i
⊢ getElem! c i = getElem c i h

Tactic:
have : Decidable (dom c i) := .isTrue h

Result:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
inst✝ : Inhabited elem
c : cont
i : idx
h : dom c i
this : Decidable (dom c i)
⊢ getElem! c i = getElem c i h
-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/-- The function `mahler k` extends `n ↦ n.choose k` on `ℕ`. -/
lemma mahler_natCast_eq (k n : ℕ) : mahler k (n : ℤ_[p]) = n.choose k

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
⊢ (mahler k) ↑n = ↑(n.choose k)

Tactic:
simp only [mahler_apply, Ring.choose_natCast, PadicInt.coe_natCast]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
@[to_additive]
lemma LocallyLipschitz.div (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :
    LocallyLipschitz fun x ↦ f x / g x

Proof state:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz fun x => f x / g x

Tactic:
simpa only [div_eq_mul_inv] using hf.mul hg.inv

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem separable_X : (X : R[X]).Separable

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ IsCoprime X 1

Tactic:
exact isCoprime_one_right

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ X.Separable

Tactic:
rw [separable_def, derivative_X]

Result:
R : Type u
inst✝ : CommSemiring R
⊢ IsCoprime X 1
-- Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
theorem geometric_hahn_banach_point_point [T1Space E] (hxy : x ≠ y) :
    ∃ f : E →L[𝕜] 𝕜, re (f x) < re (f y)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
x y : E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
f : E →L[𝕜] 𝕜
s t : ℝ
hs : ∀ a ∈ {x}, re (f a) < s
st : s < t
ht : ∀ b ∈ {y}, t < re (f b)
⊢ re (f x) < re (f y)

Tactic:
linarith [hs x rfl, ht y rfl]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
x y : E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
⊢ ∃ f, re (f x) < re (f y)

Tactic:
obtain ⟨f, s, t, hs, st, ht⟩ :=
  geometric_hahn_banach_compact_closed (𝕜 := 𝕜) (convex_singleton x) isCompact_singleton
    (convex_singleton y) isClosed_singleton (disjoint_singleton.2 hxy)

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
x y : E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
f : E →L[𝕜] 𝕜
s t : ℝ
hs : ∀ a ∈ {x}, re (f a) < s
st : s < t
ht : ∀ b ∈ {y}, t < re (f b)
⊢ ∃ f, re (f x) < re (f y)

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
x y : E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
f : E →L[𝕜] 𝕜
s t : ℝ
hs : ∀ a ∈ {x}, re (f a) < s
st : s < t
ht : ∀ b ∈ {y}, t < re (f b)
⊢ ∃ f, re (f x) < re (f y)

Tactic:
exact ⟨f, by linarith [hs x rfl, ht y rfl]⟩

Result:
no goals
-- Mathlib/GroupTheory/HNNExtension.lean
theorem prod_group_smul (g : G) (w : NormalWord d) :
    (g • w).prod φ = of g * (w.prod φ)

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
w : NormalWord d
⊢ ReducedWord.prod φ (g • w).toReducedWord = of g * ReducedWord.prod φ w.toReducedWord

Tactic:
simp [ReducedWord.prod, smul_def, mul_assoc]

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_iUnion_right (s : Set E) (t : ι → Set E) :
    convexJoin 𝕜 s (⋃ i, t i) = ⋃ i, convexJoin 𝕜 s (t i)

Proof state:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
t : ι → Set E
⊢ convexJoin 𝕜 s (⋃ i, t i) = ⋃ i, convexJoin 𝕜 s (t i)

Tactic:
simp_rw [convexJoin_comm s, convexJoin_iUnion_left]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem LinearIndependent.repr_range : LinearMap.range hv.repr = ⊤

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
⊢ LinearMap.range hv.repr = ⊤

Tactic:
rw [LinearIndependent.repr, LinearEquiv.range]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
private lemma sups_aux : a ∈ upperClosure ↑(s ⊻ t) ↔ a ∈ upperClosure s ∧ a ∈ upperClosure t

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ upperClosure ↑(s ⊻ t) ↔ a ∈ upperClosure ↑s ∧ a ∈ upperClosure ↑t

Tactic:
rw [coe_sups, upperClosure_sups, UpperSet.mem_sup_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_or : ∀ (x y : Bool), (!(x || y)) = (!x && !y)

Proof state:
⊢ ∀ (x y : Bool), (!(x || y)) = (!x && !y)

Tactic:
decide

Result:
no goals