harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean
theorem fromUnitLift_injective [Fact <| 0 < n] :
    Function.Injective <| @fromUnitLift R _ _ K _ _ _ n _

Proof state:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type v
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
n : ℕ
inst✝ : Fact (0 < n)
⊢ Function.Injective (⇑(QuotientGroup.kerLift fromUnit) ∘ ⇑(QuotientGroup.quotientMulEquivOfEq ⋯).symm)

Tactic:
exact Function.Injective.comp (QuotientGroup.kerLift_injective _) (MulEquiv.injective _)

Result:
no goals

Proof state:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type v
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
n : ℕ
inst✝ : Fact (0 < n)
⊢ Function.Injective ⇑fromUnitLift

Tactic:
dsimp only [fromUnitLift, MonoidHom.coe_comp, MulEquiv.coe_toMonoidHom]

Result:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type v
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
n : ℕ
inst✝ : Fact (0 < n)
⊢ Function.Injective (⇑(QuotientGroup.kerLift fromUnit) ∘ ⇑(QuotientGroup.quotientMulEquivOfEq ⋯).symm)
-- Mathlib/Data/List/Permutation.lean
theorem permutationsAux2_snd_cons (t : α) (ts : List α) (r : List β) (y : α) (ys : List α)
    (f : List α → β) :
    (permutationsAux2 t ts r (y :: ys) f).2 =
      f (t :: y :: ys ++ ts) :: (permutationsAux2 t ts r ys fun x : List α => f (y :: x)).2

Proof state:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
y : α
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r (y :: ys) f).2 = f (t :: y :: ys ++ ts) :: (permutationsAux2 t ts r ys fun x => f (y :: x)).2

Tactic:
simp [permutationsAux2, permutationsAux2_fst t _ _ ys]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp]
lemma leRec_succ {n} {motive : (m : ℕ) → n ≤ m → Sort*}
    (refl : motive n (Nat.le_refl _))
    (le_succ_of_le : ∀ ⦃k⦄ (h : n ≤ k), motive k h → motive (k + 1) (le_succ_of_le h))
    (h1 : n ≤ m) {h2 : n ≤ m + 1} :
    (leRec (motive := motive) refl le_succ_of_le h2) =
      le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)

Proof state:
m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
⊢ leRec refl le_succ_of_le h2 = le_succ_of_le h1 (leRec refl le_succ_of_le h1)

Tactic:
conv =>
  lhs
  rw [leRec, Or.by_cases, dif_pos h1]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_modifyKey_self [BEq α] [LawfulBEq α] {k : α} {f : β k → β k}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
    getKey? k (modifyKey k f l) = if containsKey k l then some k else none

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getKey? k (modifyKey k f l) = if containsKey k l = true then some k else none

Tactic:
simp [getKey?_modifyKey, hl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.eq_of_le_of_le (u v : Nat) : u ≤ v → v ≤ u → u = v

Proof state:
u v : Nat
⊢ u ≤ v → v ≤ u → u = v

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Vector/Snoc.lean
theorem reverse_snoc : reverse (xs.snoc x) = x ::ᵥ (reverse xs)

Proof state:
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : val✝.length = n
⊢ (snoc ⟨val✝, property✝⟩ x).reverse = x ::ᵥ reverse ⟨val✝, property✝⟩

Tactic:
simp only [reverse, snoc, cons, toList_mk]

Result:
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : val✝.length = n
⊢ ⟨(append ⟨val✝, property✝⟩ ⟨[x], ⋯⟩).toList.reverse, ⋯⟩ = ⟨x :: val✝.reverse, ⋯⟩

Proof state:
case mk.e_val
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : val✝.length = n
⊢ (append ⟨val✝, property✝⟩ ⟨[x], ⋯⟩).toList.reverse = x :: val✝.reverse

Tactic:
simp [toList, Vector.append, Append.append]

Result:
no goals

Proof state:
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : val✝.length = n
⊢ ⟨(append ⟨val✝, property✝⟩ ⟨[x], ⋯⟩).toList.reverse, ⋯⟩ = ⟨x :: val✝.reverse, ⋯⟩

Tactic:
congr

Result:
case mk.e_val
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : val✝.length = n
⊢ (append ⟨val✝, property✝⟩ ⟨[x], ⋯⟩).toList.reverse = x :: val✝.reverse

Proof state:
α : Type u_1
n : ℕ
x : α
xs : Vector α n
⊢ (xs.snoc x).reverse = x ::ᵥ xs.reverse

Tactic:
cases xs

Result:
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : val✝.length = n
⊢ (snoc ⟨val✝, property✝⟩ x).reverse = x ::ᵥ reverse ⟨val✝, property✝⟩
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_le_iff_one_le_mul : a⁻¹ ≤ b ↔ 1 ≤ b * a :=
  (mul_le_mul_iff_right a).symm.trans <| by rw [inv_mul_cancel]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a⁻¹ * a ≤ b * a ↔ 1 ≤ b * a

Tactic:
rw [inv_mul_cancel]

Result:
no goals
-- Mathlib/Data/Int/Order/Units.lean
theorem units_coe_mul_self (u : ℤˣ) : (u * u : ℤ) = 1

Proof state:
u : ℤˣ
⊢ ↑u * ↑u = 1

Tactic:
rw [← Units.val_mul, units_mul_self, Units.val_one]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem hasBasis_iSup {ι : Sort*} {ι' : ι → Type*} {l : ι → Filter α} {p : ∀ i, ι' i → Prop}
    {s : ∀ i, ι' i → Set α} (hl : ∀ i, (l i).HasBasis (p i) (s i)) :
    (⨆ i, l i).HasBasis (fun f : ∀ i, ι' i => ∀ i, p i (f i)) fun f : ∀ i, ι' i => ⋃ i, s i (f i) :=
  hasBasis_iff.mpr fun t => by
    simp only [hasBasis_iff, (hl _).mem_iff, Classical.skolem, forall_and, iUnion_subset_iff,
      mem_iSup]

Proof state:
α : Type u_1
ι : Sort u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ t ∈ ⨆ i, l i ↔ ∃ i, (∀ (i_1 : ι), p i_1 (i i_1)) ∧ ⋃ i_1, s i_1 (i i_1) ⊆ t

Tactic:
simp only [hasBasis_iff, (hl _).mem_iff, Classical.skolem, forall_and, iUnion_subset_iff,
  mem_iSup]

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Ioo : (some : α → WithBot α) '' Ioo a b = Ioo (a : WithBot α) b

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

Tactic:
rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Ioi_self <| Ioi_subset_Ioi bot_le)]

Result:
no goals
-- Mathlib/RingTheory/Perfection.lean
theorem map_eq_map (φ : R →+* S) : map p (of p R) (of p S) φ = Perfection.map p φ :=
  hom_ext _ (of p S) fun f => by rw [map_map, Perfection.coeff_map]

Proof state:
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
R : Type u₁
inst✝³ : CommSemiring R
inst✝² : CharP R p
S : Type u₂
inst✝¹ : CommSemiring S
inst✝ : CharP S p
φ : R →+* S
f : Ring.Perfection R p
⊢ (Perfection.coeff S p 0) ((map p ⋯ ⋯ φ) f) = (Perfection.coeff S p 0) ((Perfection.map p φ) f)

Tactic:
rw [map_map, Perfection.coeff_map]

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem zero_quot : (⟨Quot.mk _ 0⟩ : RingQuot r) = 0 :=
  show _ = zero r by rw [zero_def]

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
⊢ { toQuot := Quot.mk (Rel r) 0 } = RingQuot.zero r

Tactic:
rw [zero_def]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem totallyBounded_of_forall_symm {s : Set α}
    (h : ∀ V ∈ 𝓤 α, SymmetricRel V → ∃ t : Set α, Set.Finite t ∧ s ⊆ ⋃ y ∈ t, ball y V) :
    TotallyBounded s :=
  UniformSpace.hasBasis_symmetric.totallyBounded_iff.2 fun V hV => by
    simpa only [ball_eq_of_symmetry hV.2] using h V hV.1 hV.2

Proof state:
α : Type u
uniformSpace : UniformSpace α
s : Set α
h : ∀ V ∈ 𝓤 α, SymmetricRel V → ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y V
V : Set (α × α)
hV : V ∈ 𝓤 α ∧ SymmetricRel V
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ id V}

Tactic:
simpa only [ball_eq_of_symmetry hV.2] using h V hV.1 hV.2

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_div (hx : x ≠ 0) (hy : y ≠ 0) : logb b (x / y) = logb b x - logb b y

Proof state:
b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ logb b (x / y) = logb b x - logb b y

Tactic:
simp_rw [logb, log_div hx hy, sub_div]

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem mk'_algebraMap [Algebra R A] [IsScalarTower R A B] (x : R)
    (h : IsIntegral R (algebraMap R B x) := isIntegral_algebraMap) :
    IsIntegralClosure.mk' A (algebraMap R B x) h = algebraMap R A x :=
  algebraMap_injective A R B <| by rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply]

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsIntegralClosure A R B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : R
h : optParam (IsIntegral R ((algebraMap R B) x)) ⋯
⊢ (algebraMap A B) (mk' A ((algebraMap R B) x) h) = (algebraMap A B) ((algebraMap R A) x)

Tactic:
rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply]

Result:
no goals
-- Mathlib/Order/Filter/Cocardinal.lean
theorem mem_cocountable {s : Set α} :
    s ∈ cocountable ↔ (sᶜ : Set α).Countable

Proof state:
α : Type u
s : Set α
⊢ s ∈ cocountable ↔ sᶜ.Countable

Tactic:
rw [Cardinal.countable_iff_lt_aleph_one, mem_cocardinal]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.iff_congr_left {P Q R : Prop} [Decidable P] [Decidable Q] [Decidable R] :
    ((P ↔ R) ↔ (Q ↔ R)) ↔ (P ↔ Q) :=
  if h : R then by simp_all [Decidable.not_iff_not] else by simp_all [Decidable.not_iff_not]

Proof state:
P Q R : Prop
inst✝² : Decidable P
inst✝¹ : Decidable Q
inst✝ : Decidable R
h : R
⊢ ((P ↔ R) ↔ (Q ↔ R)) ↔ (P ↔ Q)

Tactic:
simp_all [Decidable.not_iff_not]

Result:
no goals

Proof state:
P Q R : Prop
inst✝² : Decidable P
inst✝¹ : Decidable Q
inst✝ : Decidable R
h : ¬R
⊢ ((P ↔ R) ↔ (Q ↔ R)) ↔ (P ↔ Q)

Tactic:
simp_all [Decidable.not_iff_not]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem length_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : (pmap f l H).length = l.length

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {H : ∀ (a : α), a ∈ tail✝ → p a}, (pmap f tail✝ H).length = tail✝.length
H : ∀ (a : α), a ∈ head✝ :: tail✝ → p a
⊢ (pmap f (head✝ :: tail✝) H).length = (head✝ :: tail✝).length

Tactic:
simp only [*, pmap, length]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a : α), a ∈ [] → p a
⊢ (pmap f [] H).length = [].length

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
⊢ (pmap f l H).length = l.length

Tactic:
induction l

Result:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a : α), a ∈ [] → p a
⊢ (pmap f [] H).length = [].length

case cons
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {H : ∀ (a : α), a ∈ tail✝ → p a}, (pmap f tail✝ H).length = tail✝.length
H : ∀ (a : α), a ∈ head✝ :: tail✝ → p a
⊢ (pmap f (head✝ :: tail✝) H).length = (head✝ :: tail✝).length
-- Mathlib/Data/Finset/Basic.lean
theorem sdiff_singleton_eq_erase (a : α) (s : Finset α) : s \ {a} = erase s a

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ s \ {a} ↔ a✝ ∈ s.erase a

Tactic:
rw [mem_erase, mem_sdiff, mem_singleton, and_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ s \ {a} = s.erase a

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ s \ {a} ↔ a✝ ∈ s.erase a
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem add_tsub_le_assoc : a + b - c ≤ a + (b - c)

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b - c ≤ a + (b - c)

Tactic:
rw [tsub_le_iff_left, add_left_comm]

Result:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a + (c + (b - c))

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a + (c + (b - c))

Tactic:
exact add_le_add_left le_add_tsub a

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Ray.lean
theorem sameRay_iff_inv_norm_smul_eq_of_ne (hx : x ≠ 0) (hy : y ≠ 0) :
    SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Tactic:
rw [inv_smul_eq_iff₀, smul_comm, eq_comm, inv_smul_eq_iff₀, sameRay_iff_norm_smul_eq] <;>
  rwa [norm_ne_zero_iff]

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalHom.lean
theorem to_distribMulActionHom_injective {f g : A →ₛₙₐ[φ] B}
    (h : (f : A →ₑ+[φ] B) = (g : A →ₑ+[φ] B)) : f = g

Proof state:
case h
R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : ↑f = ↑g
a : A
⊢ f a = g a

Tactic:
exact DistribMulActionHom.congr_fun h a

Result:
no goals

Proof state:
R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : ↑f = ↑g
⊢ f = g

Tactic:
ext a

Result:
case h
R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : ↑f = ↑g
a : A
⊢ f a = g a
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem isAdjMatrix_compl [Zero α] [One α] (h : A.IsSymm) : IsAdjMatrix A.compl :=
  { symm

Proof state:
V : Type u_1
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsSymm
⊢ A.compl.IsSymm

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
lemma ofQuotient_isPresentation : (ofQuotient relations).IsPresentation where
  bijective

Proof state:
A : Type u
inst✝ : Ring A
relations : Relations A
⊢ Function.Bijective ⇑(ofQuotient relations).fromQuotient

Tactic:
simpa only [ofQuotient_fromQuotient, LinearMap.id_coe] using Function.bijective_id

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `inv_lt_iff_one_lt_mul₀` for a version with multiplication on the other side. -/
lemma inv_lt_iff_one_lt_mul₀' (ha : 0 < a) : a⁻¹ < b ↔ 1 < a * b

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
⊢ a⁻¹ < b ↔ 1 < a * b

Tactic:
rw [← inv_mul_lt_iff₀ ha, mul_one]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean
theorem image_symm_eq_preimage (e : P₁ ≃ᵃL[k] P₂) (s : Set P₂) :
    e.symm '' s = e ⁻¹' s

Proof state:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
e : P₁ ≃ᵃL[k] P₂
s : Set P₂
⊢ ⇑e.symm '' s = ⇑e ⁻¹' s

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

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem succ_mono : CategoryTheory.Mono (ModuleCat.ofHom (πs C o))

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Mono (ModuleCat.ofHom (πs C o))

Tactic:
rw [ModuleCat.mono_iff_injective]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Function.Injective ⇑(ConcreteCategory.hom (ModuleCat.ofHom (πs C o)))

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Function.Injective ⇑(ConcreteCategory.hom (ModuleCat.ofHom (πs C o)))

Tactic:
exact injective_πs _ _

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_symm_half (m : ℕ) : choose (2 * m + 1) (m + 1) = choose (2 * m + 1) m

Proof state:
m : ℕ
⊢ (2 * m + 1).choose (m + 1) = (2 * m + 1).choose m

Tactic:
apply choose_symm_of_eq_add

Result:
case h
m : ℕ
⊢ 2 * m + 1 = m + 1 + m

Proof state:
case h
m : ℕ
⊢ 2 * m + 1 = m + 1 + m

Tactic:
rw [Nat.add_comm m 1, Nat.add_assoc 1 m m, Nat.add_comm (2 * m) 1, Nat.two_mul m]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_swap₂₃_sign (p₁ p₂ p₃ : P) : -(∡ p₁ p₂ p₃).sign = (∡ p₁ p₃ p₂).sign

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ -(∡ p₁ p₂ p₃).sign = (∡ p₁ p₃ p₂).sign

Tactic:
rw [oangle_swap₁₃_sign, ← oangle_swap₁₂_sign, oangle_swap₁₃_sign]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_eq_zero_iff (s : ℝ) : Gamma s = 0 ↔ ∃ m : ℕ, s = -m :=
  ⟨by contrapose!; exact Gamma_ne_zero, by rintro ⟨m, rfl⟩; exact Gamma_neg_nat_eq_zero m⟩

Proof state:
s : ℝ
⊢ (∀ (m : ℕ), s ≠ -↑m) → Gamma s ≠ 0

Tactic:
exact Gamma_ne_zero

Result:
no goals

Proof state:
case intro
m : ℕ
⊢ Gamma (-↑m) = 0

Tactic:
exact Gamma_neg_nat_eq_zero m

Result:
no goals

Proof state:
s : ℝ
⊢ (∃ m, s = -↑m) → Gamma s = 0

Tactic:
rintro ⟨m, rfl⟩

Result:
case intro
m : ℕ
⊢ Gamma (-↑m) = 0

Proof state:
s : ℝ
⊢ Gamma s = 0 → ∃ m, s = -↑m

Tactic:
contrapose!

Result:
s : ℝ
⊢ (∀ (m : ℕ), s ≠ -↑m) → Gamma s ≠ 0
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContinuousLinearEquiv.contDiffOn_comp_iff (e : G ≃L[𝕜] E) :
    ContDiffOn 𝕜 n (f ∘ e) (e ⁻¹' s) ↔ ContDiffOn 𝕜 n f s :=
  ⟨fun H => by simpa [Function.comp_def] using H.comp_continuousLinearMap (e.symm : E →L[𝕜] G),
    fun H => H.comp_continuousLinearMap (e : G →L[𝕜] E)⟩

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
n : WithTop ℕ∞
e : G ≃L[𝕜] E
H : ContDiffOn 𝕜 n (f ∘ ⇑e) (⇑e ⁻¹' s)
⊢ ContDiffOn 𝕜 n f s

Tactic:
simpa [Function.comp_def] using H.comp_continuousLinearMap (e.symm : E →L[𝕜] G)

Result:
no goals
-- Mathlib/RingTheory/Trace/Basic.lean
theorem traceMatrix_of_matrix_mulVec [Fintype κ] (b : κ → B) (P : Matrix κ κ A) :
    traceMatrix A (P.map (algebraMap A B) *ᵥ b) = P * traceMatrix A b * Pᵀ

Proof state:
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
⊢ (transposeAddEquiv κ κ A) (traceMatrix A (P.map ⇑(algebraMap A B) *ᵥ b)) =
    (transposeAddEquiv κ κ A) (P * traceMatrix A b * Pᵀ)

Tactic:
rw [transposeAddEquiv_apply, transposeAddEquiv_apply, ← vecMul_transpose, ← transpose_map,
  traceMatrix_of_matrix_vecMul, transpose_transpose]

Result:
no goals

Proof state:
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
⊢ traceMatrix A (P.map ⇑(algebraMap A B) *ᵥ b) = P * traceMatrix A b * Pᵀ

Tactic:
refine AddEquiv.injective (transposeAddEquiv κ κ A) ?_

Result:
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
⊢ (transposeAddEquiv κ κ A) (traceMatrix A (P.map ⇑(algebraMap A B) *ᵥ b)) =
    (transposeAddEquiv κ κ A) (P * traceMatrix A b * Pᵀ)
-- Mathlib/Analysis/Normed/Ring/Units.lean
theorem subset_compl_ball : nonunits R ⊆ (Metric.ball (1 : R) 1)ᶜ := fun x hx h₁ ↦ hx <|
  sub_sub_self 1 x ▸ (Units.oneSub (1 - x) (by rwa [mem_ball_iff_norm'] at h₁)).isUnit

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
hx : x ∈ nonunits R
h₁ : x ∈ Metric.ball 1 1
⊢ ‖1 - x‖ < 1

Tactic:
rwa [mem_ball_iff_norm'] at h₁

Result:
no goals
-- Mathlib/LinearAlgebra/FreeModule/Int.lean
lemma addSubgroup_index_ne_zero_iff {H : AddSubgroup (ι → ℤ)} :
    H.index ≠ 0 ↔ Nonempty (H ≃+ (ι → ℤ))

Proof state:
case h.e'_2.a
ι : Type u_1
inst✝ : Finite ι
H : AddSubgroup (ι → ℤ)
⊢ Nonempty (↥H ≃+ (ι → ℤ)) ↔ Nonempty (↥(AddSubgroup.toIntSubmodule H) ≃ₗ[ℤ] ι → ℤ)

Tactic:
exact ⟨fun ⟨e⟩ ↦ ⟨e.toIntLinearEquiv⟩, fun ⟨e⟩ ↦ ⟨e.toAddEquiv⟩⟩

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Finite ι
H : AddSubgroup (ι → ℤ)
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃+ (ι → ℤ))

Tactic:
convert submodule_toAddSubgroup_index_ne_zero_iff (N := AddSubgroup.toIntSubmodule H) using 1

Result:
case h.e'_2.a
ι : Type u_1
inst✝ : Finite ι
H : AddSubgroup (ι → ℤ)
⊢ Nonempty (↥H ≃+ (ι → ℤ)) ↔ Nonempty (↥(AddSubgroup.toIntSubmodule H) ≃ₗ[ℤ] ι → ℤ)
-- Mathlib/CategoryTheory/Limits/Creates.lean
lemma liftedLimitMapsToOriginal_inv_map_π
    {K : J ⥤ C} {F : C ⥤ D} [CreatesLimit K F] {c : Cone (K ⋙ F)} (t : IsLimit c) (j : J) :
      (liftedLimitMapsToOriginal t).inv.hom ≫ F.map ((liftLimit t).π.app j) = c.π.app j

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ F.map ((liftLimit t).π.app j) = (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app j

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ (liftedLimitMapsToOriginal t).inv.hom ≫ F.map ((liftLimit t).π.app j) = c.π.app j

Tactic:
rw [show F.map ((liftLimit t).π.app j) = (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app j
  from (by simp), ← Category.assoc, ← Cone.category_comp_hom]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ ((liftedLimitMapsToOriginal t).inv ≫ (liftedLimitMapsToOriginal t).hom).hom ≫ c.π.app j = c.π.app j

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ ((liftedLimitMapsToOriginal t).inv ≫ (liftedLimitMapsToOriginal t).hom).hom ≫ c.π.app j = c.π.app j

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma Even.toUnitHom_eval_neg_one (hψ : ψ.Even) : ψ.toUnitHom (-1) = 1

Proof state:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Even
⊢ ψ ↑(-1) = ↑1

Tactic:
exact hψ

Result:
no goals

Proof state:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Even
⊢ (toUnitHom ψ) (-1) = 1

Tactic:
rw [← Units.eq_iff, MulChar.coe_toUnitHom]

Result:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Even
⊢ ψ ↑(-1) = ↑1
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive (attr := simp) ofReal_norm]
lemma ofReal_norm' (x : E) : .ofReal ‖x‖ = ‖x‖ₑ

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ ENNReal.ofReal ‖x‖ = ‖x‖ₑ

Tactic:
simp [enorm, ENNReal.ofReal, Real.toNNReal, nnnorm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ l[n]?.isSome = true ↔ n < l.length

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean
lemma smul_ne_zero_iff_right (hc : c ≠ 0) : c • x ≠ 0 ↔ x ≠ 0

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
hc : c ≠ 0
⊢ c • x ≠ 0 ↔ x ≠ 0

Tactic:
simp [hc]

Result:
no goals