harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem comap_bracket_le {J₁ J₂ : LieIdeal R L'} : ⁅comap f J₁, comap f J₂⁆ ≤ comap f ⁅J₁, J₂⁆

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
⊢ ⁅comap f J₁, comap f J₂⁆ ≤ comap f ⁅J₁, J₂⁆

Tactic:
rw [← map_le_iff_le_comap]

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
⊢ map f ⁅comap f J₁, comap f J₂⁆ ≤ ⁅J₁, J₂⁆

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
⊢ map f ⁅comap f J₁, comap f J₂⁆ ≤ ⁅J₁, J₂⁆

Tactic:
exact le_trans (map_bracket_le f) (LieSubmodule.mono_lie map_comap_le map_comap_le)

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_surjective : Function.Surjective (Function.uncurry <| mk' f : M × S → M')

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
⊢ Function.Surjective (Function.uncurry (mk' f))

Tactic:
intro x

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : M'
⊢ ∃ a, Function.uncurry (mk' f) a = x

Proof state:
case intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : M'
m : M
s : ↥S
e : s • x = f m
⊢ ∃ a, Function.uncurry (mk' f) a = x

Tactic:
exact ⟨⟨m, s⟩, mk'_eq_iff.mpr e.symm⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : M'
⊢ ∃ a, Function.uncurry (mk' f) a = x

Tactic:
obtain ⟨⟨m, s⟩, e : s • x = f m⟩ := IsLocalizedModule.surj S f x

Result:
case intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : M'
m : M
s : ↥S
e : s • x = f m
⊢ ∃ a, Function.uncurry (mk' f) a = x
-- Mathlib/Algebra/FreeAlgebra/Cardinality.lean
theorem cardinalMk_eq_max_lift [Nonempty X] [Nontrivial R] :
    #(FreeAlgebra R X) = Cardinal.lift.{v} #R ⊔ Cardinal.lift.{u} #X ⊔ ℵ₀

Proof state:
R : Type u
inst✝² : CommSemiring R
X : Type v
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
hX : #(FreeMonoid X) = #X ⊔ ℵ₀
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R ⊔ Cardinal.lift.{u, v} #X ⊔ ℵ₀

Tactic:
haveI : Infinite (FreeMonoid X) := infinite_iff.2 (by simp [hX])

Result:
R : Type u
inst✝² : CommSemiring R
X : Type v
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
hX : #(FreeMonoid X) = #X ⊔ ℵ₀
this : Infinite (FreeMonoid X)
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R ⊔ Cardinal.lift.{u, v} #X ⊔ ℵ₀

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

Tactic:
have hX := mk_freeMonoid X

Result:
R : Type u
inst✝² : CommSemiring R
X : Type v
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
hX : #(FreeMonoid X) = #X ⊔ ℵ₀
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R ⊔ Cardinal.lift.{u, v} #X ⊔ ℵ₀

Proof state:
R : Type u
inst✝² : CommSemiring R
X : Type v
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
hX : #(FreeMonoid X) = #X ⊔ ℵ₀
⊢ ℵ₀ ≤ #(FreeMonoid X)

Tactic:
simp [hX]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
X : Type v
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
hX : #(FreeMonoid X) = #X ⊔ ℵ₀
this : Infinite (FreeMonoid X)
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R ⊔ Cardinal.lift.{u, v} #X ⊔ ℵ₀

Tactic:
rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra,
  mk_finsupp_lift_of_infinite, hX, lift_max, lift_aleph0, sup_comm, ← sup_assoc]

Result:
no goals
-- Mathlib/ModelTheory/Syntax.lean
theorem sumElim_comp_relabelAux {m : ℕ} {g : α → β ⊕ (Fin n)} {v : β → M}
    {xs : Fin (n + m) → M} : Sum.elim v xs ∘ relabelAux g m =
    Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n)

Proof state:
case h.inl
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
⊢ (Sum.elim v xs ∘ relabelAux g m) (Sum.inl x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inl x)

Tactic:
simp only [BoundedFormula.relabelAux, Function.comp_apply, Sum.map_inl, Sum.elim_inl]

Result:
case h.inl
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
⊢ Sum.elim v xs (Sum.map id (⇑finSumFinEquiv) ((Equiv.sumAssoc β (Fin n) (Fin m)) (Sum.inl (g x)))) =
    Sum.elim v (xs ∘ castAdd m) (g x)

Proof state:
case h.inl
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
⊢ Sum.elim v xs (Sum.map id (⇑finSumFinEquiv) ((Equiv.sumAssoc β (Fin n) (Fin m)) (Sum.inl (g x)))) =
    Sum.elim v (xs ∘ castAdd m) (g x)

Tactic:
rcases g x with l | r <;> simp

Result:
no goals

Proof state:
case h.inr
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : Fin m
⊢ (Sum.elim v xs ∘ relabelAux g m) (Sum.inr x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inr x)

Tactic:
simp [BoundedFormula.relabelAux]

Result:
no goals

Proof state:
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
⊢ Sum.elim v xs ∘ relabelAux g m = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n)

Tactic:
ext x

Result:
case h
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α ⊕ Fin m
⊢ (Sum.elim v xs ∘ relabelAux g m) x = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) x

Proof state:
case h
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α ⊕ Fin m
⊢ (Sum.elim v xs ∘ relabelAux g m) x = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) x

Tactic:
rcases x with x | x

Result:
case h.inl
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
⊢ (Sum.elim v xs ∘ relabelAux g m) (Sum.inl x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inl x)

case h.inr
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : Fin m
⊢ (Sum.elim v xs ∘ relabelAux g m) (Sum.inr x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inr x)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem denote_projected_entry' {entry : Entrypoint α} :
    ⟦entry.aig, ⟨entry.ref.gate, entry.ref.hgate⟩, assign⟧ = ⟦entry, assign⟧

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig✝ : AIG α
ref✝ : aig✝.Ref
⊢ ⟦assign,
      { aig := { aig := aig✝, ref := ref✝ }.aig,
        ref := { gate := { aig := aig✝, ref := ref✝ }.ref.gate, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig✝, ref := ref✝ }⟧

Tactic:
simp

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
⊢ ⟦assign, { aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ = ⟦assign, entry⟧

Tactic:
cases entry

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig✝ : AIG α
ref✝ : aig✝.Ref
⊢ ⟦assign,
      { aig := { aig := aig✝, ref := ref✝ }.aig,
        ref := { gate := { aig := aig✝, ref := ref✝ }.ref.gate, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig✝, ref := ref✝ }⟧
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem Monic.ne_zero [Nontrivial R] {f : MvPolynomial σ R} (hf : m.Monic f) :
    f ≠ 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
f : MvPolynomial σ R
hf : m.Monic f
⊢ f ≠ 0

Tactic:
rintro rfl

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : m.Monic 0
⊢ False

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : m.Monic 0
⊢ False

Tactic:
simp [Monic, leadingCoeff_zero] at hf

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem exists_gcf_pair_rat_eq_nth_conts :
    ∃ conts : Pair ℚ, (of v).conts n = (conts.map (↑) : Pair K)

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ conts, (of v).contsAux (n + 1) = Pair.map Rat.cast conts

Tactic:
exact exists_gcf_pair_rat_eq_of_nth_contsAux v <| n + 1

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ conts, (of v).conts n = Pair.map Rat.cast conts

Tactic:
rw [nth_cont_eq_succ_nth_contAux]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ conts, (of v).contsAux (n + 1) = Pair.map Rat.cast conts
-- Mathlib/Logic/Relation.lean
theorem to_reflTransGen {a b} (h : TransGen r a b) : ReflTransGen r a b

Proof state:
case single
α : Type u_1
r : α → α → Prop
a b b✝ : α
h : r a b✝
⊢ ReflTransGen r a b✝

Tactic:
exact ReflTransGen.single h

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
a b b✝ c✝ : α
a✝ : TransGen r a b✝
bc : r b✝ c✝
ab : ReflTransGen r a b✝
⊢ ReflTransGen r a c✝

Tactic:
exact ReflTransGen.tail ab bc

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
h : TransGen r a b
⊢ ReflTransGen r a b

Tactic:
induction h with
| single h => exact ReflTransGen.single h
| tail _ bc ab => exact ReflTransGen.tail ab bc

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem pow_eq_one_iff_modEq : x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]

Tactic:
rw [modEq_zero_iff_dvd, orderOf_dvd_iff_pow_eq_one]

Result:
no goals
-- Mathlib/Control/EquivFunctor.lean
theorem mapEquiv_trans {γ : Type u₀} (ab : α ≃ β) (bc : β ≃ γ) :
    (mapEquiv f ab).trans (mapEquiv f bc) = mapEquiv f (ab.trans bc) :=
  Equiv.ext fun x => by simp [mapEquiv, map_trans']

Proof state:
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β γ : Type u₀
ab : α ≃ β
bc : β ≃ γ
x : f α
⊢ ((mapEquiv f ab).trans (mapEquiv f bc)) x = (mapEquiv f (ab.trans bc)) x

Tactic:
simp [mapEquiv, map_trans']

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.of_mul_left_left (H : IsCoprime (x * y) z) : IsCoprime x z :=
  let ⟨a, b, h⟩ := H
  ⟨a * y, b, by rwa [mul_right_comm, mul_assoc]⟩

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime (x * y) z
a b : R
h : a * (x * y) + b * z = 1
⊢ a * y * x + b * z = 1

Tactic:
rwa [mul_right_comm, mul_assoc]

Result:
no goals
-- Mathlib/RepresentationTheory/Invariants.lean
theorem averageMap_id (v : V) (hv : v ∈ invariants ρ) : averageMap ρ v = v

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
hv : v ∈ ρ.invariants
⊢ ρ.averageMap v = v

Tactic:
rw [mem_invariants] at hv

Result:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
hv : ∀ (g : G), (ρ g) v = v
⊢ ρ.averageMap v = v

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
hv : ∀ (g : G), (ρ g) v = v
⊢ ρ.averageMap v = v

Tactic:
simp [average, map_sum, hv, Finset.card_univ, ← Nat.cast_smul_eq_nsmul k _ v, smul_smul]

Result:
no goals
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem neLocus_comm : f.neLocus g = g.neLocus f

Proof state:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
⊢ f.neLocus g = g.neLocus f

Tactic:
simp_rw [neLocus, Finset.union_comm, ne_comm]

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem not_irreducible_expand (R p) [CommSemiring R] [Fact p.Prime] [CharP R p] [PerfectRing R p]
    (f : R[X]) : ¬ Irreducible (expand R p f)

Proof state:
R : Type u_2
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
⊢ ¬Irreducible ((expand R p) f)

Tactic:
rw [polynomial_expand_eq]

Result:
R : Type u_2
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
⊢ ¬Irreducible (map (↑(frobeniusEquiv R p).symm) f ^ p)

Proof state:
R : Type u_2
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
⊢ ¬Irreducible (map (↑(frobeniusEquiv R p).symm) f ^ p)

Tactic:
exact not_irreducible_pow (Fact.out : p.Prime).ne_one

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
/-- `t` is in the upper shadow of `𝒜` iff `t` is exactly one element more than something from `𝒜`.

See also `Finset.mem_upShadow_iff_exists_mem_card_add_one`. -/
lemma mem_upShadow_iff_exists_sdiff : t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = 1

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = 1

Tactic:
simp_rw [mem_upShadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]

Result:
no goals
-- Mathlib/Order/SuccPred/Archimedean.lean
theorem exists_succ_iterate_iff_le : (∃ n, succ^[n] a = b) ↔ a ≤ b

Proof state:
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a : α
n : ℕ
⊢ a ≤ succ^[n] a

Tactic:
exact id_le_iterate_of_id_le le_succ n a

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (∃ n, succ^[n] a = b) ↔ a ≤ b

Tactic:
refine ⟨?_, exists_succ_iterate_of_le⟩

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (∃ n, succ^[n] a = b) → a ≤ b

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (∃ n, succ^[n] a = b) → a ≤ b

Tactic:
rintro ⟨n, rfl⟩

Result:
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a : α
n : ℕ
⊢ a ≤ succ^[n] a
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
theorem colimit_map_colimitObjIsoColimitCompEvaluation_hom [HasColimitsOfShape J C] (F : J ⥤ K ⥤ C)
    {i j : K} (f : i ⟶ j) :
    (colimit F).map f ≫ (colimitObjIsoColimitCompEvaluation _ _).hom =
      (colimitObjIsoColimitCompEvaluation _ _).hom ≫
        colimMap (whiskerLeft _ ((evaluation _ _).map f))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
i j : K
f : i ⟶ j
⊢ (colimit F).map f ≫ (colimitObjIsoColimitCompEvaluation F j).hom =
    (colimitObjIsoColimitCompEvaluation F i).hom ≫ colimMap (whiskerLeft F ((evaluation K C).map f))

Tactic:
rw [← Iso.inv_comp_eq, ← Category.assoc, ← Iso.eq_comp_inv,
  colimitObjIsoColimitCompEvaluation_inv_colimit_map]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem prehaar_pos (K₀ : PositiveCompacts G) {U : Set G} (hU : (interior U).Nonempty) {K : Set G}
    (h1K : IsCompact K) (h2K : (interior K).Nonempty) : 0 < prehaar (K₀ : Set G) U ⟨K, h1K⟩

Proof state:
case ha
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
⊢ 0 < index (↑{ carrier := K, isCompact' := h1K }) U

Tactic:
apply index_pos ⟨⟨K, h1K⟩, h2K⟩ hU

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
⊢ 0 < prehaar (↑K₀) U { carrier := K, isCompact' := h1K }

Tactic:
apply div_pos <;> norm_cast

Result:
case ha
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
⊢ 0 < index (↑{ carrier := K, isCompact' := h1K }) U

case hb
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
⊢ 0 < index (↑K₀) U

Proof state:
case hb
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
⊢ 0 < index (↑K₀) U

Tactic:
exact index_pos K₀ hU

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem getElem?_mapIdx (f : Nat → α → β) (a : Vector α n) (i : Nat) :
    (a.mapIdx f)[i]? = a[i]?.map (f i)

Proof state:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
i : Nat
a : Array α
⊢ (mapIdx f { toArray := a, size_toArray := ⋯ })[i]? = Option.map (f i) { toArray := a, size_toArray := ⋯ }[i]?

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : Nat → α → β
a : Vector α n
i : Nat
⊢ (mapIdx f a)[i]? = Option.map (f i) a[i]?

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
i : Nat
a : Array α
⊢ (mapIdx f { toArray := a, size_toArray := ⋯ })[i]? = Option.map (f i) { toArray := a, size_toArray := ⋯ }[i]?
-- Mathlib/Order/Minimal.lean
theorem Set.exists_insert_of_not_maximal (hP : ∀ ⦃s t⦄, P t → s ⊆ t → P s) (hs : P s)
    (h : ¬ Maximal P s) : ∃ x ∉ s, P (insert x s)

Proof state:
α : Type u_1
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
hs : P s
h : ¬Maximal P s
⊢ ∃ x ∉ s, P (insert x s)

Tactic:
simpa [Set.maximal_iff_forall_insert hP, hs] using h

Result:
no goals
-- Mathlib/Computability/RegularExpressions.lean
theorem one_rmatch_iff (x : List α) : rmatch 1 x ↔ x = []

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ rmatch 1 x = true ↔ x = []

Tactic:
induction x <;> simp [rmatch, matchEpsilon, *]

Result:
no goals
-- Mathlib/Topology/Algebra/GroupWithZero.lean
theorem Continuous.div (hf : Continuous f) (hg : Continuous g) (h₀ : ∀ x, g x ≠ 0) :
    Continuous (f / g)

Proof state:
α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
f g : α → G₀
inst✝ : TopologicalSpace α
hf : Continuous f
hg : Continuous g
h₀ : ∀ (x : α), g x ≠ 0
⊢ Continuous (f / g)

Tactic:
simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
@[reassoc (attr := simp)]
lemma map_hom_ofInv_id (s : Y ⟶ X) (hs : W s) (L : C ⥤ D) (hL : W.IsInvertedBy L) :
    L.map s ≫ (ofInv s hs).map L hL = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
s : Y ⟶ X
hs : W s
L : C ⥤ D
hL : W.IsInvertedBy L
this : IsIso (L.map s) := hL s hs
⊢ L.map s ≫ (ofInv s hs).map L hL = 𝟙 (L.obj Y)

Tactic:
simp [map]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
s : Y ⟶ X
hs : W s
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ L.map s ≫ (ofInv s hs).map L hL = 𝟙 (L.obj Y)

Tactic:
letI := hL _ hs

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
s : Y ⟶ X
hs : W s
L : C ⥤ D
hL : W.IsInvertedBy L
this : IsIso (L.map s) := hL s hs
⊢ L.map s ≫ (ofInv s hs).map L hL = 𝟙 (L.obj Y)
-- Mathlib/Topology/Basic.lean
theorem interior_eq_nhds : interior s = { x | 𝓝 x ≤ 𝓟 s } :=
  interior_eq_nhds'.trans <| by simp only [le_principal_iff]

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ {x | s ∈ 𝓝 x} = {x | 𝓝 x ≤ 𝓟 s}

Tactic:
simp only [le_principal_iff]

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem isPurelyInseparable_adjoin_simple_iff_natSepDegree_eq_one {x : E} :
    IsPurelyInseparable F F⟮x⟯ ↔ (minpoly F x).natSepDegree = 1

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ IsPurelyInseparable F ↥F⟮x⟯ ↔ (minpoly F x).natSepDegree = 1

Tactic:
rw [← le_perfectClosure_iff, adjoin_simple_le_iff, mem_perfectClosure_iff_natSepDegree_eq_one]

Result:
no goals
-- Mathlib/ModelTheory/ElementaryMaps.lean
theorem injective (φ : M ↪ₑ[L] N) : Function.Injective φ

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
x y : M
h : φ x = φ (if 2 = 1 then x else y) ↔ x = if 2 = 1 then x else y
⊢ φ x = φ y → x = y

Tactic:
exact h.1

Result:
no goals

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
x y : M
h :
  Term.realize (⇑φ ∘ fun i => if i = 0 then x else y) (var 0) =
      Term.realize (⇑φ ∘ fun i => if i = 0 then x else y) (var 1) ↔
    Term.realize (fun i => if i = 0 then x else y) (var 0) = Term.realize (fun i => if i = 0 then x else y) (var 1)
⊢ φ x = φ y → x = y

Tactic:
simp only [Nat.one_ne_zero, Term.realize, Fin.one_eq_zero_iff, if_true, eq_self_iff_true,
  Function.comp_apply, if_false] at h

Result:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
x y : M
h : φ x = φ (if 2 = 1 then x else y) ↔ x = if 2 = 1 then x else y
⊢ φ x = φ y → x = y

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
⊢ Function.Injective ⇑φ

Tactic:
intro x y

Result:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
x y : M
⊢ φ x = φ y → x = y

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
x y : M
h :
  ((var 0).equal (var 1)).Realize (⇑φ ∘ fun i => if i = 0 then x else y) ↔
    ((var 0).equal (var 1)).Realize fun i => if i = 0 then x else y
⊢ φ x = φ y → x = y

Tactic:
rw [Formula.realize_equal, Formula.realize_equal] at h

Result:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
x y : M
h :
  Term.realize (⇑φ ∘ fun i => if i = 0 then x else y) (var 0) =
      Term.realize (⇑φ ∘ fun i => if i = 0 then x else y) (var 1) ↔
    Term.realize (fun i => if i = 0 then x else y) (var 0) = Term.realize (fun i => if i = 0 then x else y) (var 1)
⊢ φ x = φ y → x = y

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
x y : M
⊢ φ x = φ y → x = y

Tactic:
have h :=
  φ.map_formula ((var 0).equal (var 1) : L.Formula (Fin 2)) fun i => if i = 0 then x else y

Result:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
x y : M
h :
  ((var 0).equal (var 1)).Realize (⇑φ ∘ fun i => if i = 0 then x else y) ↔
    ((var 0).equal (var 1)).Realize fun i => if i = 0 then x else y
⊢ φ x = φ y → x = y
-- Mathlib/Algebra/Ring/CharZero.lean
theorem nat_mul_inj' {n : ℕ} {a b : R} (h : (n : R) * a = (n : R) * b) (w : n ≠ 0) : a = b

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n * a = ↑n * b
w : n ≠ 0
⊢ a = b

Tactic:
simpa [w] using nat_mul_inj h

Result:
no goals