harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/SeparatedMap.lean
theorem IsLocallyInjective.isOpen_eqLocus (inj : IsLocallyInjective f) (he : f ∘ g₁ = f ∘ g₂) :
    IsOpen {a | g₁ a = g₂ a} :=
  let g : A → f.Pullback f := fun a ↦ ⟨⟨g₁ a, g₂ a⟩, congr_fun he a⟩
  (isLocallyInjective_iff_isOpen_diagonal.mp inj).preimage (by fun_prop : Continuous g)

Proof state:
X : Type u_1
Y : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
g₁ g₂ : A → X
h₁ : Continuous g₁
h₂ : Continuous g₂
inj : IsLocallyInjective f
he : f ∘ g₁ = f ∘ g₂
g : A → Function.Pullback f f := fun a => ⟨(g₁ a, g₂ a), ⋯⟩
⊢ Continuous g

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_eq_diagonal [DecidableEq n] [AddMonoid α] [StarAddMonoid α]
    {M : Matrix n n α} {v : n → α} :
    Mᴴ = diagonal v ↔ M = diagonal (star v) :=
  (Function.Involutive.eq_iff conjTranspose_conjTranspose).trans <|
    by rw [diagonal_conjTranspose]

Proof state:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : Matrix n n α
v : n → α
⊢ M = (diagonal v)ᴴ ↔ M = diagonal (star v)

Tactic:
rw [diagonal_conjTranspose]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem val_pos_iff [NeZero n] {a : Fin n} : 0 < a.val ↔ 0 < a

Proof state:
n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ 0 < ↑a ↔ 0 < a

Tactic:
rw [← val_fin_lt, val_zero]

Result:
no goals
-- Mathlib/Topology/Compactness/LocallyCompact.lean
theorem IsLocallyClosed.locallyCompactSpace [LocallyCompactSpace X] {s : Set X}
    (hs : IsLocallyClosed s) : LocallyCompactSpace s :=
  IsEmbedding.subtypeVal.locallyCompactSpace <| by rwa [Subtype.range_val]

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
s : Set X
hs : IsLocallyClosed s
⊢ IsLocallyClosed (range Subtype.val)

Tactic:
rwa [Subtype.range_val]

Result:
no goals
-- Mathlib/Order/BoundedOrder/Lattice.lean
theorem min_eq_bot [OrderBot α] {a b : α} : min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥

Proof state:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a b : α
⊢ a ⊓ b = ⊥ ↔ a = ⊥ ∨ b = ⊥

Tactic:
simp_rw [← le_bot_iff, inf_le_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem eq_C_coeff_zero_iff_natDegree_eq_zero : p = C (p.coeff 0) ↔ p.natDegree = 0 :=
  ⟨fun h ↦ by rw [h, natDegree_C], eq_C_of_natDegree_eq_zero⟩

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p = C (p.coeff 0)
⊢ p.natDegree = 0

Tactic:
rw [h, natDegree_C]

Result:
no goals
-- Mathlib/Topology/Algebra/Support.lean
theorem LocallyFinite.smul_left [Zero R] [Zero M] [SMulWithZero R M]
    {s : ι → X → R} (h : LocallyFinite fun i ↦ support <| s i) (f : ι → X → M) :
    LocallyFinite fun i ↦ support <| s i • f i :=
  h.subset fun i x ↦ mt <| fun h ↦ by rw [Pi.smul_apply', h, zero_smul]

Proof state:
X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : ι → X → R
h✝ : LocallyFinite fun i => support (s i)
f : ι → X → M
i : ι
x : X
h : s i x = 0
⊢ (s i • f i) x = 0

Tactic:
rw [Pi.smul_apply', h, zero_smul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
lemma revAt_eq_self_of_lt {N i : ℕ} (h : N < i) : revAt N i = i

Proof state:
N i : ℕ
h : N < i
⊢ (revAt N) i = i

Tactic:
simp [revAt, Nat.not_le.mpr h]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem eventually_atBot_prod_self [Nonempty α] [Preorder α] [IsDirected α (· ≥ ·)]
    {p : α × α → Prop} : (∀ᶠ x in atBot, p x) ↔ ∃ a, ∀ k l, k ≤ a → l ≤ a → p (k, l)

Proof state:
α : Type u_3
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≥ x2
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ a, ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)

Tactic:
simp [← prod_atBot_atBot_eq, (@atBot_basis α _ _).prod_self.eventually_iff]

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
theorem coe_add_period (x : 𝕜) : ((x + p : 𝕜) : AddCircle p) = x

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedAddCommGroup 𝕜
p x : 𝕜
⊢ ↑(x + p) = ↑x

Tactic:
rw [coe_add, ← eq_sub_iff_add_eq', sub_self, coe_period]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
lemma mulSupport_one_sub' [AddGroup R] (f : ι → R) : mulSupport (1 - f) = support f

Proof state:
ι : Type u_1
R : Type u_5
inst✝¹ : One R
inst✝ : AddGroup R
f : ι → R
⊢ mulSupport (1 - f) = support f

Tactic:
rw [sub_eq_add_neg, mulSupport_one_add', support_neg']

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_fin_fun (n : ℕ) : Module.rank R (Fin n → R) = n

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
n : ℕ
⊢ Module.rank R (Fin n → R) = ↑n

Tactic:
simp [rank_fun']

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem Filter.HasBasis.mapClusterPt_iff_frequently {ι : Sort*} {p : ι → Prop} {s : ι → Set X}
    (hx : (𝓝 x).HasBasis p s) : MapClusterPt x F u ↔ ∀ i, p i → ∃ᶠ a in F, u a ∈ s i

Proof state:
X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
F : Filter α
u : α → X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
hx : (𝓝 x).HasBasis p s
⊢ MapClusterPt x F u ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i

Tactic:
simp_rw [MapClusterPt, hx.clusterPt_iff_frequently, frequently_map]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem nhds_translation_mul_inv (x : G) : comap (· * x⁻¹) (𝓝 1) = 𝓝 x :=
  ((Homeomorph.mulRight x⁻¹).comap_nhds_eq 1).trans <| show 𝓝 (1 * x⁻¹⁻¹) = 𝓝 x by simp

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x : G
⊢ 𝓝 (1 * x⁻¹⁻¹) = 𝓝 x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem Iic_iInf₂ (f : ∀ i, κ i → α) : Iic (⨅ (i) (j), f i j) = ⋂ (i) (j), Iic (f i j)

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Iic (⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, Iic (f i j)

Tactic:
simp_rw [Iic_iInf]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem comp₂Measurable_toGerm [PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β]
    [PseudoMetrizableSpace γ] [SecondCountableTopologyEither β γ]
    [MeasurableSpace γ] [BorelSpace γ] [PseudoMetrizableSpace δ] [SecondCountableTopology δ]
    [MeasurableSpace δ] [OpensMeasurableSpace δ] (g : β → γ → δ) (hg : Measurable (uncurry g))
    (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :
    (comp₂Measurable g hg f₁ f₂).toGerm = f₁.toGerm.map₂ g f₂.toGerm :=
  induction_on₂ f₁ f₂ fun f₁ _ f₂ _ => by simp

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹⁴ : MeasurableSpace α
μ : Measure α
inst✝¹³ : TopologicalSpace δ
inst✝¹² : TopologicalSpace β
inst✝¹¹ : TopologicalSpace γ
inst✝¹⁰ : PseudoMetrizableSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : PseudoMetrizableSpace γ
inst✝⁶ : SecondCountableTopologyEither β γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : PseudoMetrizableSpace δ
inst✝² : SecondCountableTopology δ
inst✝¹ : MeasurableSpace δ
inst✝ : OpensMeasurableSpace δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁✝ : α →ₘ[μ] β
f₂✝ : α →ₘ[μ] γ
f₁ : α → β
x✝¹ : AEStronglyMeasurable f₁ μ
f₂ : α → γ
x✝ : AEStronglyMeasurable f₂ μ
⊢ (comp₂Measurable g hg (mk f₁ x✝¹) (mk f₂ x✝)).toGerm = Germ.map₂ g (mk f₁ x✝¹).toGerm (mk f₂ x✝).toGerm

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Adhesive.lean
theorem IsPushout.IsVanKampen.mono_of_mono_right [Mono g] {H : IsPushout f g h i}
    (H' : H.IsVanKampen) : Mono h :=
  IsKernelPair.mono_of_isIso_fst
    ((H' f (𝟙 _) (𝟙 _) f (𝟙 _) (𝟙 _) g h (IsPullback.of_vert_isIso ⟨by simp⟩)
        (IsKernelPair.id_of_mono g) ⟨rfl⟩ H.1 ⟨by simp⟩).mp
      (IsPushout.of_vert_isIso ⟨by simp⟩)).1

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono g
H : IsPushout f g h i
H' : H.IsVanKampen
⊢ f ≫ 𝟙 X = 𝟙 W ≫ f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma zero_smul_subset (t : Finset β) : (0 : Finset α) • t ⊆ 0

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
t : Finset β
⊢ 0 • t ⊆ 0

Tactic:
simp [subset_iff, mem_smul]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
lemma mem_ofObjects_iff {I : Type*} (Y : I → C) {Z X : C} (g : Z ⟶ X) :
    ofObjects Y X g ↔ ∃ (i : I), Nonempty (Z ⟶ Y i)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
Z X : C
g : Z ⟶ X
⊢ (ofObjects Y X).arrows g ↔ ∃ i, Nonempty (Z ⟶ Y i)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_eq_fallback [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
    ¬a ∈ m → m.getD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
a : α
fallback : β a
⊢ ¬a ∈ m → m.getD a fallback = fallback

Tactic:
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_neg : (-p).smeval x = - p.smeval x

Proof state:
R : Type u_1
inst✝³ : Ring R
S : Type u_2
inst✝² : AddCommGroup S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
p : R[X]
x : S
⊢ (-p).smeval x = -p.smeval x

Tactic:
rw [← add_eq_zero_iff_eq_neg, ← smeval_add, neg_add_cancel, smeval_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_linear_comp (f : M →ₗ[R] M') :
    linearCombination R (f ∘ v) = f ∘ₗ linearCombination R v

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v : α → M
f : M →ₗ[R] M'
⊢ linearCombination R (⇑f ∘ v) = f ∘ₗ linearCombination R v

Tactic:
ext

Result:
case h.h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v : α → M
f : M →ₗ[R] M'
a✝ : α
⊢ (linearCombination R (⇑f ∘ v) ∘ₗ lsingle a✝) 1 = ((f ∘ₗ linearCombination R v) ∘ₗ lsingle a✝) 1

Proof state:
case h.h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v : α → M
f : M →ₗ[R] M'
a✝ : α
⊢ (linearCombination R (⇑f ∘ v) ∘ₗ lsingle a✝) 1 = ((f ∘ₗ linearCombination R v) ∘ₗ lsingle a✝) 1

Tactic:
simp [linearCombination_apply]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/End.lean
theorem pow_map_zero_of_le {f : Module.End R M} {m : M} {k l : ℕ} (hk : k ≤ l)
    (hm : (f ^ k) m = 0) : (f ^ l) m = 0

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : Module.End R M
m : M
k l : ℕ
hk : k ≤ l
hm : (f ^ k) m = 0
⊢ (f ^ l) m = 0

Tactic:
rw [← Nat.sub_add_cancel hk, pow_add, mul_apply, hm, map_zero]

Result:
no goals
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_univ [Fintype Ω] {s : Set Ω} :
    uniformOn Set.univ s = Measure.count s / Fintype.card Ω

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ (uniformOn Set.univ) s = Measure.count s / ↑(Fintype.card Ω)

Tactic:
simp [uniformOn, cond_apply, ← ENNReal.div_eq_inv_mul]

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem testBit_land (m n k) : testBit (land m n) k = (testBit m k && testBit n k)

Proof state:
m n : ℤ
k : ℕ
⊢ (m.land n).testBit k = (m.testBit k && n.testBit k)

Tactic:
rw [← bitwise_and, testBit_bitwise]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderIso.lean
theorem image_Ico (e : α ≃o β) (a b : α) : e '' Ico a b = Ico (e a) (e b)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ ⇑e '' Ico a b = Ico (e a) (e b)

Tactic:
rw [e.image_eq_preimage, e.symm.preimage_Ico, e.symm_symm]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_zsmul_add (a b : α) (m : ℤ) : toIocMod hp a (m • p + b) = toIocMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp a (m • p + b) = toIocMod hp a b

Tactic:
rw [add_comm, toIocMod_add_zsmul]

Result:
no goals
-- Mathlib/Control/Traversable/Lemmas.lean
theorem id_sequence (x : t α) : sequence (f := Id) (pure <$> x) = pure x

Proof state:
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
x : t α
⊢ sequence (pure <$> x) = pure x

Tactic:
simp [sequence, traverse_map, id_traverse]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
protected lemma continuous_rng_iff {X : Type*} [TopologicalSpace X] {f : X → (α →ᵤ[𝔖] β)} :
    Continuous f ↔ ∀ s ∈ 𝔖,
      Continuous (UniformFun.ofFun ∘ s.restrict ∘ UniformOnFun.toFun 𝔖 ∘ f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
X : Type u_5
inst✝ : TopologicalSpace X
f : X → α →ᵤ[𝔖] β
⊢ Continuous f ↔ ∀ s ∈ 𝔖, Continuous (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖) ∘ f)

Tactic:
simp only [continuous_iff_continuousAt, ContinuousAt,
  UniformOnFun.tendsto_iff_tendstoUniformlyOn, UniformFun.tendsto_iff_tendstoUniformly,
  tendstoUniformlyOn_iff_tendstoUniformly_comp_coe, @forall_swap X, Function.comp_apply,
  Function.comp_def, restrict_eq, UniformFun.toFun_ofFun]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem all_iff (s : String) (p : Char → Bool) : all s p ↔ ∀ c ∈ s.1, p c

Proof state:
s : String
p : Char → Bool
⊢ s.all p = true ↔ ∀ (c : Char), c ∈ s.data → p c = true

Tactic:
simp [all_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
@[reassoc]
lemma associator_naturality₁ {X₁ X₂ X₃ Y₁ : LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) :
    ((f₁ ▷ X₂) ▷ X₃) ≫ (α_ Y₁ X₂ X₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ▷ (X₂ ⊗ X₃))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₁ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
⊢ f₁ ▷ X₂ ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom = (α_ X₁ X₂ X₃).hom ≫ f₁ ▷ (X₂ ⊗ X₃)

Tactic:
simp only [← tensorHom_id, associator_naturality, Iso.cancel_iso_hom_left, tensor_id]

Result:
no goals
-- Mathlib/Logic/Equiv/Fintype.lean
theorem Equiv.Perm.viaFintypeEmbedding_sign [DecidableEq α] [Fintype β] :
    Equiv.Perm.sign (e.viaFintypeEmbedding f) = Equiv.Perm.sign e

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : DecidableEq β
e : Perm α
f : α ↪ β
inst✝¹ : DecidableEq α
inst✝ : Fintype β
⊢ sign (e.viaFintypeEmbedding f) = sign e

Tactic:
simp [Equiv.Perm.viaFintypeEmbedding]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem triangle_assoc_comp_left_inv (X Y : C) :
    (X ◁ (λ_ Y).inv) ≫ (α_ X (𝟙_ C) Y).inv = (ρ_ X).inv ▷ Y

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ X ◁ (λ_ Y).inv ≫ (α_ X (𝟙_ C) Y).inv = (ρ_ X).inv ▷ Y

Tactic:
simp [← cancel_mono ((ρ_ X).hom ▷ Y)]

Result:
no goals
-- Mathlib/CategoryTheory/Dialectica/Monoidal.lean
theorem triangle (X Y : Dial C) :
    (associator X (𝟙_ (Dial C)) Y).hom ≫ tensorHom (𝟙 X) (leftUnitor Y).hom =
    tensorHom (rightUnitor X).hom (𝟙 Y)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
⊢ (X.associator (𝟙_ (Dial C)) Y).hom ≫ tensorHom (𝟙 X) Y.leftUnitor.hom = tensorHom X.rightUnitor.hom (𝟙 Y)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_eq_some_iff {a : Vector α n} : a[i]? = some b ↔ ∃ h : i < n, a[i] = b

Proof state:
α : Type u_1
n i : Nat
b : α
a : Vector α n
⊢ a[i]? = some b ↔ ∃ h, a[i] = b

Tactic:
simp [getElem?_def]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[simp]
lemma negPart_neg (a : A) : (-a)⁻ = a⁺

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
a : A
⊢ (-a)⁻ = a⁺

Tactic:
rw [← eq_comm, ← sub_eq_zero, ← posPart_neg, neg_neg, sub_self]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma lt_last_iff_ne_last {a : Fin (n + 1)} : a < last n ↔ a ≠ last n

Proof state:
n : ℕ
a : Fin (n + 1)
⊢ a < last n ↔ a ≠ last n

Tactic:
simp [Fin.lt_iff_le_and_ne, le_last]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/FullyFaithful.lean
theorem preimage_map (f : X ⟶ Y) : F.preimage (F.map f) = f :=
  F.map_injective (by simp)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
inst✝¹ : F.Full
inst✝ : F.Faithful
f : X ⟶ Y
⊢ F.map (F.preimage (F.map f)) = F.map f

Tactic:
simp

Result:
no goals
-- Mathlib/ModelTheory/DirectLimit.lean
theorem relMap_unify_equiv {n : ℕ} (R : L.Relations n) (x : Fin n → Σˣ f) (i j : ι)
    (hi : i ∈ upperBounds (range (Sigma.fst ∘ x))) (hj : j ∈ upperBounds (range (Sigma.fst ∘ x))) :
    RelMap R (unify f x i hi) = RelMap R (unify f x j hj)

Proof state:
case intro.intro
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
n : ℕ
R : L.Relations n
x : Fin n → Σˣ f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst ∘ x))
k : ι
ik : i ≤ k
jk : j ≤ k
⊢ RelMap R (unify f x i hi) = RelMap R (unify f x j hj)

Tactic:
rw [← (f i k ik).map_rel, comp_unify, ← (f j k jk).map_rel, comp_unify]

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Ioc : (some : α → WithTop α) '' Ioc a b = Ioc (a : WithTop α) b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Ioc a b = Ioc ↑a ↑b

Tactic:
rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left
    (Subset.trans Ioc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblZ_of_Z_eq_zero {P : Fin 3 → R} (hPz : P z = 0) : W'.dblZ P = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.dblZ P = 0

Tactic:
rw [dblZ, hPz, zero_mul]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
@[reassoc (attr := simp)]
lemma pullbackAwayιIso_hom_SpecMap_awayMap_left :
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) = Limits.pullback.fst _ _

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) =
    Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')

Tactic:
rw [← cancel_mono (awayι 𝒜 f f_deg hm), ← pullbackAwayιIso_hom_awayι,
  Category.assoc, SpecMap_awayMap_awayι]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma CompleteOrthogonalIdempotents.unique_iff [Unique I] :
    CompleteOrthogonalIdempotents e ↔ e default = 1

Proof state:
R : Type u_1
inst✝² : Semiring R
I : Type u_3
e : I → R
inst✝¹ : Fintype I
inst✝ : Unique I
⊢ CompleteOrthogonalIdempotents e ↔ e default = 1

Tactic:
rw [completeOrthogonalIdempotents_iff, OrthogonalIdempotents.unique, Fintype.sum_unique,
  and_iff_right_iff_imp]

Result:
R : Type u_1
inst✝² : Semiring R
I : Type u_3
e : I → R
inst✝¹ : Fintype I
inst✝ : Unique I
⊢ e default = 1 → IsIdempotentElem (e default)
-- Mathlib/Analysis/Complex/Basic.lean
theorem ringHom_eq_ofReal_of_continuous {f : ℝ →+* ℂ} (h : Continuous f) : f = ofRealHom

Proof state:
f : ℝ →+* ℂ
h : Continuous ⇑f
⊢ f = ofRealHom

Tactic:
convert congr_arg AlgHom.toRingHom <| Subsingleton.elim (AlgHom.mk' f <| map_real_smul f h)
  (Algebra.ofId ℝ ℂ)

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
/-- A union of a finite family of sets is totally bounded
if and only if each set of the family is totally bounded. -/
lemma totallyBounded_sUnion {S : Set (Set α)} (hS : S.Finite) :
    TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s

Proof state:
α : Type u
uniformSpace : UniformSpace α
S : Set (Set α)
hS : S.Finite
⊢ TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s

Tactic:
rw [sUnion_eq_biUnion, totallyBounded_biUnion hS]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem t'_snd_snd (i j k : 𝒰.J) :
    t' 𝒰 f g i j k ≫ pullback.snd _ _ ≫ pullback.snd _ _ =
      pullback.fst _ _ ≫ pullback.fst _ _ ≫ pullback.fst _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ t' 𝒰 f g i j k ≫
      pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫ pullback.snd (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
      pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.fst (𝒰.map i ≫ f) g

Tactic:
simp only [t', Category.assoc, pullbackSymmetry_hom_comp_snd_assoc,
  pullbackRightPullbackFstIso_inv_fst_assoc, pullback.lift_fst_assoc, t_snd,
  pullbackRightPullbackFstIso_hom_fst_assoc]

Result:
no goals
-- Mathlib/Order/Monotone/Basic.lean
theorem strictAnti_dual_iff : StrictAnti (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictAnti f

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictAnti (⇑toDual ∘ f ∘ ⇑ofDual) ↔ StrictAnti f

Tactic:
rw [strictAnti_toDual_comp_iff, strictMono_comp_ofDual_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
@[reassoc (attr := simp)]
lemma hom_right_inv_right {f g : Under X} (e : f ≅ g) :
    e.hom.right ≫ e.inv.right = 𝟙 f.right

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f g : Under X
e : f ≅ g
⊢ e.hom.right ≫ e.inv.right = 𝟙 f.right

Tactic:
simp [← Under.comp_right]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
lemma mu_apply (a b : α) : mu 𝕜 a b = if a = b then 1 else -∑ x ∈ Ico a b, mu 𝕜 a x

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (mu 𝕜) a b = if a = b then 1 else -∑ x ∈ Ico a b, (mu 𝕜) a x

Tactic:
rw [mu, coe_mk, muFun_apply, sum_attach]

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
private lemma logC_of_left_le_one {b m : ℕ} (hb : b ≤ 1) : logC b m = 0

Proof state:
b m : ℕ
hb : b ≤ 1
⊢ logC b m = 0

Tactic:
rw [logC, dif_neg hb.not_lt]

Result:
no goals
-- Mathlib/FieldTheory/Extension.lean
theorem exists_lift_of_splits (x : Lifts F E K) {s : E} (h1 : IsIntegral F s)
    (h2 : (minpoly F s).Splits (algebraMap F K)) : ∃ y, x ≤ y ∧ s ∈ y.carrier :=
  exists_lift_of_splits' x h1.tower_top <| h1.minpoly_splits_tower_top' <| by
    rwa [← x.emb.comp_algebraMap] at h2

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
⊢ Splits (x.emb.comp (algebraMap F ↥x.carrier)) (minpoly F s)

Tactic:
rwa [← x.emb.comp_algebraMap] at h2

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Cardinal.lean
theorem cardinalMk_eq_max_lift [Nonempty σ] [Nontrivial R] :
    #(MvPolynomial σ R) = max (max (Cardinal.lift.{u} #R) <| Cardinal.lift.{v} #σ) ℵ₀ :=
  (mk_finsupp_lift_of_infinite _ R).trans <| by
    rw [mk_finsupp_nat, max_assoc, lift_max, lift_aleph0, max_comm]

Proof state:
σ : Type u
R : Type v
inst✝² : CommSemiring R
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ lift.{v, u} #(σ →₀ ℕ) ⊔ lift.{u, v} #R = lift.{u, v} #R ⊔ lift.{v, u} #σ ⊔ ℵ₀

Tactic:
rw [mk_finsupp_nat, max_assoc, lift_max, lift_aleph0, max_comm]

Result:
no goals