harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
protected lemma Filter.HasBasis.isUniformInducing_iff {ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'}
    (h : (𝓤 α).HasBasis p s) (h' : (𝓤 β).HasBasis p' s') {f : α → β} :
    IsUniformInducing f ↔
      (∀ i, p' i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
        (∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j)

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : (𝓤 α).HasBasis p s
h' : (𝓤 β).HasBasis p' s'
f : α → β
⊢ IsUniformInducing f ↔
    (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
      ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j

Tactic:
simp [isUniformInducing_iff', h.uniformContinuous_iff h', (h'.comap _).le_basis_iff h, subset_def]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma restrictSubtype_inter_indep_iff :
    (M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep (X ∩ I)

Proof state:
α : Type u_1
X I : Set α
M : Matroid α
⊢ (M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep (X ∩ I)

Tactic:
simp [restrictSubtype, Subtype.val_injective.injOn]

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
lemma klDiv_of_ac_of_integrable (h1 : μ ≪ ν) (h2 : Integrable (llr μ ν) μ) :
    klDiv μ ν = ENNReal.ofReal (∫ x, llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
h2 : Integrable (llr μ ν) μ
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal)
    else ⊤) =
    ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal)

Tactic:
exact if_pos ⟨h1, h2⟩

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
h2 : Integrable (llr μ ν) μ
⊢ klDiv μ ν = ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal)

Tactic:
rw [klDiv_def]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
h2 : Integrable (llr μ ν) μ
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal)
    else ⊤) =
    ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal)
-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
lemma shiftIso_add_hom_app (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
    (F.shiftIso (m + n) a a'' (by rw [add_assoc, ha', ha''])).hom.app X =
      (shift F a).map ((shiftFunctorAdd C m n).hom.app X) ≫
        (shiftIso F n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫
          (shiftIso F m a' a'' ha'').hom.app X

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_6, u_1} C
inst✝³ : Category.{u_5, u_2} A
F : C ⥤ A
M : Type u_3
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso (m + n) a a'' ⋯).hom.app X =
    (F.shift a).map ((shiftFunctorAdd C m n).hom.app X) ≫
      (F.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X

Tactic:
simp [F.shiftIso_add n m a a' a'' ha' ha'']

Result:
no goals

Proof state:
C : Type u_1
A : Type u_2
inst✝⁶ : Category.{?u.44380, u_1} C
inst✝⁵ : Category.{?u.44384, u_2} A
F : C ⥤ A
M : Type u_3
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
G : Type u_4
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ m + n + a = a''

Tactic:
rw [add_assoc, ha', ha'']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem add_comm (x y : BitVec n) : x + y = y + x

Proof state:
n : Nat
x y : BitVec n
⊢ x + y = y + x

Tactic:
simp [add_def, Nat.add_comm]

Result:
no goals
-- Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
lemma minimalPrimes_eq_minimals : minimalPrimes R = {x | Minimal Ideal.IsPrime x} :=
  congr_arg Minimal (by simp)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ (fun q => q.IsPrime ∧ ⊥ ≤ q) = Ideal.IsPrime

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem mem_roots_map_of_injective [Semiring S] {p : S[X]} {f : S →+* R}
    (hf : Function.Injective f) {x : R} (hp : p ≠ 0) : x ∈ (p.map f).roots ↔ p.eval₂ f x = 0

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Semiring S
p : S[X]
f : S →+* R
hf : Function.Injective ⇑f
x : R
hp : p ≠ 0
⊢ x ∈ (map f p).roots ↔ eval₂ f x p = 0

Tactic:
rw [mem_roots ((Polynomial.map_ne_zero_iff hf).mpr hp), IsRoot, eval_map]

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValExtension.lean
theorem val_map_lt_iff (x y : R) : vA (algebraMap R A x) < vA (algebraMap R A y) ↔ vR x < vR y

Proof state:
R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : LinearOrderedCommMonoidWithZero ΓR
inst✝² : LinearOrderedCommMonoidWithZero ΓA
inst✝¹ : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : IsValExtension vR vA
x y : R
⊢ vA ((algebraMap R A) x) < vA ((algebraMap R A) y) ↔ vR x < vR y

Tactic:
simpa only [not_le] using ((val_map_le_iff vR vA _ _).not)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem tan_eq_zero_iff' {θ : ℂ} (hθ : cos θ ≠ 0) : tan θ = 0 ↔ ∃ k : ℤ, k * π = θ

Proof state:
θ : ℂ
hθ : cos θ ≠ 0
⊢ tan θ = 0 ↔ ∃ k, ↑k * ↑π = θ

Tactic:
simp only [tan, hθ, div_eq_zero_iff, sin_eq_zero_iff]

Result:
θ : ℂ
hθ : cos θ ≠ 0
⊢ (∃ k, θ = ↑k * ↑π) ∨ False ↔ ∃ k, ↑k * ↑π = θ

Proof state:
θ : ℂ
hθ : cos θ ≠ 0
⊢ (∃ k, θ = ↑k * ↑π) ∨ False ↔ ∃ k, ↑k * ↑π = θ

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem pi_inf_principal_pi_neBot [∀ i, NeBot (f i)] {I : Set ι} :
    NeBot (pi f ⊓ 𝓟 (I.pi s)) ↔ ∀ i ∈ I, NeBot (f i ⊓ 𝓟 (s i))

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ (pi f ⊓ 𝓟 (I.pi s)).NeBot ↔ ∀ i ∈ I, (f i ⊓ 𝓟 (s i)).NeBot

Tactic:
simp [neBot_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem unit_app_inverse (e : C ≌ D) (Y : D) :
    e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ 𝟙 (e.inverse.obj Y) = 𝟙 (e.inverse.obj ((𝟭 D).obj Y))

Tactic:
dsimp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)

Tactic:
erw [← Iso.comp_hom_eq_id (e.inverse.mapIso (e.counitIso.app Y)), unit_inverse_comp]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ 𝟙 (e.inverse.obj Y) = 𝟙 (e.inverse.obj ((𝟭 D).obj Y))
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem complete_graph_degree [DecidableEq V] (v : V) :
    (⊤ : SimpleGraph V).degree v = Fintype.card V - 1

Proof state:
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v : V
⊢ ⊤.degree v = Fintype.card V - 1

Tactic:
erw [degree, neighborFinset_eq_filter, filter_ne, card_erase_of_mem (mem_univ v), card_univ]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem average_const (μ : Measure α) [IsFiniteMeasure μ] [h : NeZero μ] (c : E) :
    ⨍ _x, c ∂μ = c

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
h : NeZero μ
c : E
⊢ ⨍ (_x : α), c ∂μ = c

Tactic:
rw [average, integral_const, measure_univ, ENNReal.one_toReal, one_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem unattach_mkArray {p : α → Prop} {n : Nat} {x : { x // p x }} :
    (Array.mkArray n x).unattach = Array.mkArray n x.1

Proof state:
α : Type u_1
p : α → Prop
n : Nat
x : { x // p x }
⊢ (mkArray n x).unattach = mkArray n x.val

Tactic:
simp [unattach]

Result:
no goals
-- Mathlib/Algebra/Order/Group/DenselyOrdered.lean
@[to_additive]
private lemma exists_lt_mul_right [CommGroup α] [LT α] [DenselyOrdered α]
    [CovariantClass α α (· * ·) (· < ·)] {a b c : α} (hc : c < a * b) :
    ∃ b' < b, c < a * b'

Proof state:
case intro.intro
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 < x2
a b c : α
hc : c < a * b
a' : α
hc' : c / a < a'
ha' : a' < b
⊢ ∃ b', b' < b ∧ c < a * b'

Tactic:
exact ⟨a', ha', div_lt_iff_lt_mul'.1 hc'⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 < x2
a b c : α
hc : c < a * b
⊢ ∃ b', b' < b ∧ c < a * b'

Tactic:
obtain ⟨a', hc', ha'⟩ := exists_between (div_lt_iff_lt_mul'.2 hc)

Result:
case intro.intro
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 < x2
a b c : α
hc : c < a * b
a' : α
hc' : c / a < a'
ha' : a' < b
⊢ ∃ b', b' < b ∧ c < a * b'
-- Mathlib/Analysis/NormedSpace/Real.lean
theorem frontier_ball (x : E) {r : ℝ} (hr : r ≠ 0) :
    frontier (ball x r) = sphere x r

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (ball x r) = sphere x r

Tactic:
rw [frontier, closure_ball x hr, isOpen_ball.interior_eq, closedBall_diff_ball]

Result:
no goals
-- Mathlib/Logic/Function/Conjugate.lean
theorem trans (hab : Semiconj fab ga gb) (hbc : Semiconj fbc gb gc) :
    Semiconj (fbc ∘ fab) ga gc := fun x ↦ by
  simp only [comp_apply, hab.eq, hbc.eq]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
fab : α → β
fbc : β → γ
ga : α → α
gb : β → β
gc : γ → γ
hab : Semiconj fab ga gb
hbc : Semiconj fbc gb gc
x : α
⊢ (fbc ∘ fab) (ga x) = gc ((fbc ∘ fab) x)

Tactic:
simp only [comp_apply, hab.eq, hbc.eq]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem LipschitzOnWith.dimH_image_le (h : LipschitzOnWith K f s) : dimH (f '' s) ≤ dimH s

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
K : ℝ≥0
f : X → Y
s : Set X
h : LipschitzOnWith K f s
⊢ dimH (f '' s) ≤ dimH s

Tactic:
simpa using h.holderOnWith.dimH_image_le zero_lt_one

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem castLE_zero {n m : Nat} (h : n.succ ≤ m.succ) : castLE h 0 = 0

Proof state:
n m : Nat
h : n.succ ≤ m.succ
⊢ castLE h 0 = 0

Tactic:
simp [Fin.ext_iff]

Result:
no goals
-- Mathlib/GroupTheory/Abelianization.lean
theorem Subgroup.map_subtype_commutator (H : Subgroup G) :
    (_root_.commutator H).map H.subtype = ⁅H, H⁆

Proof state:
G : Type u
inst✝ : Group G
H : Subgroup G
⊢ map H.subtype (_root_.commutator ↥H) = ⁅H, H⁆

Tactic:
rw [_root_.commutator_def, map_commutator, ← MonoidHom.range_eq_map, H.range_subtype]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem right_unitality_inv (X : C) :
    (ρ_ (F.obj X)).inv ≫ F.obj X ◁ ε F ≫ μ F X (𝟙_ C) = F.map (ρ_ X).inv

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
⊢ (ρ_ (F.obj X)).inv ≫ F.obj X ◁ ε F ≫ μ F X (𝟙_ C) = F.map (ρ_ X).inv

Tactic:
rw [Iso.inv_comp_eq, right_unitality, Category.assoc, Category.assoc, ← F.map_comp,
  Iso.hom_inv_id, F.map_id, comp_id]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma WithBot.toDual_le_iff {x : WithBot α} {y : WithTop αᵒᵈ} :
    x.toDual ≤ y ↔ WithTop.ofDual y ≤ x

Proof state:
α : Type u_1
inst✝ : LE α
x : WithBot α
y : WithTop αᵒᵈ
⊢ WithBot.toDual x ≤ y ↔ WithTop.ofDual y ≤ x

Tactic:
cases x <;> cases y <;> simp [toDual_le]

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

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

Tactic:
simp [natDegree]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
lemma resLE_eq_morphismRestrict : f.resLE U (f ⁻¹ᵁ U) le_rfl = f ∣_ U

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ resLE f U (f ⁻¹ᵁ U) ⋯ = f ∣_ U

Tactic:
simp [resLE]

Result:
no goals
-- Mathlib/LinearAlgebra/CrossProduct.lean
theorem cross_self (v : Fin 3 → R) : v ×₃ v = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
v : Fin 3 → R
⊢ (crossProduct v) v = 0

Tactic:
simp [cross_apply, mul_comm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem cycleGraph_neighborFinset {n : ℕ} {v : Fin (n + 2)} :
    (cycleGraph (n + 2)).neighborFinset v = {v - 1, v + 1}

Proof state:
n : ℕ
v : Fin (n + 2)
⊢ (cycleGraph (n + 2)).neighborFinset v = {v - 1, v + 1}

Tactic:
simp [neighborFinset, cycleGraph_neighborSet]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem eq_zero_of_epi_kernel [Epi (kernel.ι f)] : f = 0 :=
  (cancel_epi (kernel.ι f)).1 (by simp)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : Epi (kernel.ι f)
⊢ kernel.ι f ≫ f = kernel.ι f ≫ 0

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_add_measure {m : MeasurableSpace α} (μ ν : Measure α) (f : α → ℝ≥0∞) :
    (μ + ν).withDensity f = μ.withDensity f + ν.withDensity f

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ (μ + ν).withDensity f = μ.withDensity f + ν.withDensity f

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ((μ + ν).withDensity f) s = (μ.withDensity f + ν.withDensity f) s

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ((μ + ν).withDensity f) s = (μ.withDensity f + ν.withDensity f) s

Tactic:
simp only [withDensity_apply f hs, restrict_add, lintegral_add_measure, Measure.add_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modify_eq_nil_iff {f : α → α} {n} {l : List α} :
    l.modify f n = [] ↔ l = []

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
⊢ modify f n l = [] ↔ l = []

Tactic:
cases l <;> cases n <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem concat_append (a : α) (l₁ l₂ : List α) : concat l₁ a ++ l₂ = l₁ ++ a :: l₂

Proof state:
α : Type u_1
a : α
l₁ l₂ : List α
⊢ l₁.concat a ++ l₂ = l₁ ++ a :: l₂

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue!_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
    {l : List ((_ : α) × β)} {k a : α} {v : β} : getValue! a (insertEntryIfNew k v l) =
      if k == a ∧ containsKey k l = false then v else getValue! a l

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : PartialEquivBEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
k a : α
v : β
⊢ getValue! a (insertEntryIfNew k v l) = if (k == a) = true ∧ containsKey k l = false then v else getValue! a l

Tactic:
simp [getValue!_eq_getValue?, getValue?_insertEntryIfNew, apply_ite Option.get!]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobjectCompIso_hom_arrow (f : X ⟶ Y) [HasImage f] {Y' : C} (h : Y ⟶ Y') [IsIso h] :
    (imageSubobjectCompIso f h).hom ≫ (imageSubobject f).arrow =
      (imageSubobject (f ≫ h)).arrow ≫ inv h

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : HasImage f
Y' : C
h : Y ⟶ Y'
inst✝ : IsIso h
⊢ (imageSubobjectCompIso f h).hom ≫ (imageSubobject f).arrow = (imageSubobject (f ≫ h)).arrow ≫ inv h

Tactic:
simp [imageSubobjectCompIso]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem map_subtype_le (p' : Submodule R p) : map p.subtype p' ≤ p

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
p' : Submodule R ↥p
⊢ map p.subtype p' ≤ p

Tactic:
simpa using (map_le_range : map p.subtype p' ≤ range p.subtype)

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem perm_union {s₁ s₂ s₃ s₄ : AList β} (p₁₂ : s₁.entries ~ s₂.entries)
    (p₃₄ : s₃.entries ~ s₄.entries) : (s₁ ∪ s₃).entries ~ (s₂ ∪ s₄).entries

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ s₄ : AList β
p₁₂ : s₁.entries ~ s₂.entries
p₃₄ : s₃.entries ~ s₄.entries
⊢ (s₁ ∪ s₃).entries ~ (s₂ ∪ s₄).entries

Tactic:
simp [p₁₂.kunion s₃.nodupKeys p₃₄]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem fastGrowing_limit (o) {f} (h : fundamentalSequence o = Sum.inr f) :
    fastGrowing o = fun i => fastGrowing (f i) i

Proof state:
o : ONote
f : ℕ → ONote
h : o.fundamentalSequence = Sum.inr f
⊢ o.fastGrowing = fun i => (f i).fastGrowing i

Tactic:
rw [fastGrowing_def h]

Result:
no goals
-- Mathlib/Topology/DiscreteQuotient.lean
theorem ofLE_ofLE (h₁ : A ≤ B) (h₂ : B ≤ C) (x : A) :
    ofLE h₂ (ofLE h₁ x) = ofLE (h₁.trans h₂) x

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
⊢ ofLE h₂ (ofLE h₁ x) = ofLE ⋯ x

Tactic:
rcases x with ⟨⟩

Result:
case mk
X : Type u_2
inst✝ : TopologicalSpace X
A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
a✝ : X
⊢ ofLE h₂ (ofLE h₁ (Quot.mk (⇑A.toSetoid) a✝)) = ofLE ⋯ (Quot.mk (⇑A.toSetoid) a✝)

Proof state:
case mk
X : Type u_2
inst✝ : TopologicalSpace X
A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
a✝ : X
⊢ ofLE h₂ (ofLE h₁ (Quot.mk (⇑A.toSetoid) a✝)) = ofLE ⋯ (Quot.mk (⇑A.toSetoid) a✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_eq_dif {p : Prop} [Decidable p] (a : p → α) :
    ⨆ h : p, a h = if h : p then a h else ⊥

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
p : Prop
inst✝ : Decidable p
a : p → α
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥

Tactic:
by_cases h : p <;> simp [h]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
protected lemma zero : PosSemidef (0 : Matrix n n R) :=
  ⟨isHermitian_zero, by simp⟩

Proof state:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
⊢ ∀ (x : n → R), 0 ≤ star x ⬝ᵥ 0 *ᵥ x

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem iInf_apply' {ι} (m : ι → OuterMeasure α) {s : Set α} (hs : s.Nonempty) :
    (⨅ i, m i) s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' n, ⨅ i, m i (t n)

Proof state:
α : Type u_1
ι : Sort u_2
m : ι → OuterMeasure α
s : Set α
hs : s.Nonempty
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ range fun i => m i, μ (t n) =
    ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)

Tactic:
simp only [iInf_range]

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_2
m : ι → OuterMeasure α
s : Set α
hs : s.Nonempty
⊢ (⨅ i, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)

Tactic:
rw [iInf, sInf_apply' hs]

Result:
α : Type u_1
ι : Sort u_2
m : ι → OuterMeasure α
s : Set α
hs : s.Nonempty
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ range fun i => m i, μ (t n) =
    ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)
-- Mathlib/Order/Sublattice.lean
@[simp] lemma prod_eq_bot {M : Sublattice β} : L.prod M = ⊥ ↔ L = ⊥ ∨ M = ⊥

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L : Sublattice α
M : Sublattice β
⊢ L.prod M = ⊥ ↔ L = ⊥ ∨ M = ⊥

Tactic:
simpa only [← coe_inj] using Set.prod_eq_empty_iff

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem map_comap_eq_self
    {f : A →ₐ[R] B} {S : Subalgebra R B} (h : S ≤ f.range) : (S.comap f).map f = S

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R B
h : S ≤ f.range
⊢ map f (comap f S) = S

Tactic:
simpa only [inf_of_le_left h] using map_comap_eq f S

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addX_of_X_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2) : W.addX P Q = addU P Q ^ 2

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addX P Q = addU P Q ^ 2

Tactic:
rw [addU, neg_sq, div_pow, ← addX_of_X_eq' hP hQ hx,
  mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]

Result:
no goals
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
theorem sub_le (a b c : R) : abv (a - c) ≤ abv (a - b) + abv (b - c)

Proof state:
R : Type u_5
S : Type u_6
inst✝¹ : Ring R
inst✝ : OrderedSemiring S
abv : AbsoluteValue R S
a b c : R
⊢ abv (a - c) ≤ abv (a - b) + abv (b - c)

Tactic:
simpa [sub_eq_add_neg, add_assoc] using abv.add_le (a - b) (b - c)

Result:
no goals
-- Mathlib/CategoryTheory/Sums/Basic.lean
theorem hom_inl_inr_false {X : C} {Y : D} (f : Sum.inl X ⟶ Sum.inr Y) : False

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
X : C
Y : D
f : inl X ⟶ inr Y
⊢ False

Tactic:
cases f

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
theorem symm {φ ψ : L.BoundedFormula α n}
    (h : φ ⇔[T] ψ) : ψ ⇔[T] φ := fun M v xs => by
  rw [BoundedFormula.realize_iff, Iff.comm, ← BoundedFormula.realize_iff]
  exact h M v xs

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (ψ ⇔ φ).Realize v xs

Tactic:
rw [BoundedFormula.realize_iff, Iff.comm, ← BoundedFormula.realize_iff]

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⇔ ψ).Realize v xs

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⇔ ψ).Realize v xs

Tactic:
exact h M v xs

Result:
no goals
-- Mathlib/Data/Multiset/Fintype.lean
theorem map_univ_coe (m : Multiset α) :
    (Finset.univ : Finset m).val.map (fun x : m ↦ (x : α)) = m

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
this : map Prod.fst (Finset.map m.coeEmbedding Finset.univ).val = m
⊢ map (fun x => x.fst) Finset.univ.val = m

Tactic:
simpa only [Finset.map_val, Multiset.coeEmbedding_apply, Multiset.map_map,
  Function.comp_apply] using this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ map (fun x => x.fst) Finset.univ.val = m

Tactic:
have := m.map_toEnumFinset_fst

Result:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
this : map Prod.fst m.toEnumFinset.val = m
⊢ map (fun x => x.fst) Finset.univ.val = m

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
this : map Prod.fst m.toEnumFinset.val = m
⊢ map (fun x => x.fst) Finset.univ.val = m

Tactic:
rw [← m.map_univ_coeEmbedding] at this

Result:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
this : map Prod.fst (Finset.map m.coeEmbedding Finset.univ).val = m
⊢ map (fun x => x.fst) Finset.univ.val = m