harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem inv (q : ℚ) : padicValRat p q⁻¹ = -padicValRat p q

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q

Tactic:
rw [eq_neg_iff_add_eq_zero, ← padicValRat.mul (inv_ne_zero hq) hq, inv_mul_cancel₀ hq,
  padicValRat.one]

Result:
no goals

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q

Tactic:
simp [hq]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ padicValRat p q⁻¹ = -padicValRat p q

Tactic:
by_cases hq : q = 0

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q

case neg
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q
-- Mathlib/Deprecated/Cardinal/Finite.lean
theorem _root_.Cardinal.natCast_eq_toPartENat_iff {n : ℕ} {c : Cardinal} :
    ↑n = toPartENat c ↔ ↑n = c

Proof state:
n : ℕ
c : Cardinal.{u_1}
⊢ ↑n = toPartENat c ↔ ↑n = c

Tactic:
rw [le_antisymm_iff, le_antisymm_iff, Cardinal.toPartENat_le_natCast_iff,
  Cardinal.natCast_le_toPartENat_iff]

Result:
no goals
-- Mathlib/Data/List/GetD.lean
theorem getD_replicate {y i n} (h : i < n) :
    getD (replicate n x) i y = x

Proof state:
α : Type u
x y : α
i n : ℕ
h : i < n
⊢ (replicate n x).getD i y = x

Tactic:
rw [getD_eq_getElem,  getElem_replicate]

Result:
case h
α : Type u
x y : α
i n : ℕ
h : i < n
⊢ i < (replicate n x).length

Proof state:
case h
α : Type u
x y : α
i n : ℕ
h : i < n
⊢ i < (replicate n x).length

Tactic:
rwa [length_replicate]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem IsSt.unique {x : ℝ*} {r s : ℝ} (hr : IsSt x r) (hs : IsSt x s) : r = s

Proof state:
case intro
r s : ℝ
f : ℕ → ℝ
hr : (ofSeq f).IsSt r
hs : (ofSeq f).IsSt s
⊢ r = s

Tactic:
rw [isSt_ofSeq_iff_tendsto] at hr hs

Result:
case intro
r s : ℝ
f : ℕ → ℝ
hr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
hs : Tendsto f (↑(hyperfilter ℕ)) (𝓝 s)
⊢ r = s

Proof state:
case intro
r s : ℝ
f : ℕ → ℝ
hr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
hs : Tendsto f (↑(hyperfilter ℕ)) (𝓝 s)
⊢ r = s

Tactic:
exact tendsto_nhds_unique hr hs

Result:
no goals

Proof state:
x : ℝ*
r s : ℝ
hr : x.IsSt r
hs : x.IsSt s
⊢ r = s

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩

Result:
case intro
r s : ℝ
f : ℕ → ℝ
hr : (ofSeq f).IsSt r
hs : (ofSeq f).IsSt s
⊢ r = s
-- Mathlib/Data/Nat/Factors.lean
theorem dvd_of_primeFactorsList_subperm {a b : ℕ} (ha : a ≠ 0)
    (h : a.primeFactorsList <+~ b.primeFactorsList) : a ∣ b

Proof state:
case inl
a : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ primeFactorsList 0
⊢ a ∣ 0

Tactic:
exact dvd_zero _

Result:
no goals

Proof state:
case inr
a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
hb : b > 0
⊢ a ∣ b

Tactic:
rcases a with (_ | _ | a)

Result:
case inr.zero
b : ℕ
hb : b > 0
ha : 0 ≠ 0
h : primeFactorsList 0 <+~ b.primeFactorsList
⊢ 0 ∣ b

case inr.succ.zero
b : ℕ
hb : b > 0
ha : 0 + 1 ≠ 0
h : (0 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ 0 + 1 ∣ b

case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ a + 1 + 1 ∣ b

Proof state:
case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ a + 1 + 1 ∣ b

Tactic:
use (@List.diff _ instBEqOfDecidableEq b.primeFactorsList a.succ.succ.primeFactorsList).prod

Result:
case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = (a + 1 + 1) * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod

Proof state:
case inr.zero
b : ℕ
hb : b > 0
ha : 0 ≠ 0
h : primeFactorsList 0 <+~ b.primeFactorsList
⊢ 0 ∣ b

Tactic:
exact (ha rfl).elim

Result:
no goals

Proof state:
case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = (a + 1 + 1).primeFactorsList.prod * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod

Tactic:
rw [← List.prod_append,
  List.Perm.prod_eq <| List.subperm_append_diff_self_of_count_le <| List.subperm_ext_iff.mp h,
  Nat.prod_primeFactorsList hb.ne']

Result:
no goals

Proof state:
case inr.succ.zero
b : ℕ
hb : b > 0
ha : 0 + 1 ≠ 0
h : (0 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ 0 + 1 ∣ b

Tactic:
exact one_dvd _

Result:
no goals

Proof state:
a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
⊢ a ∣ b

Tactic:
rcases b.eq_zero_or_pos with (rfl | hb)

Result:
case inl
a : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ primeFactorsList 0
⊢ a ∣ 0

case inr
a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
hb : b > 0
⊢ a ∣ b

Proof state:
case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = (a + 1 + 1) * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod

Tactic:
nth_rw 1 [← Nat.prod_primeFactorsList ha]

Result:
case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = (a + 1 + 1).primeFactorsList.prod * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
-- Mathlib/Order/SupClosed.lean
lemma infClosed_range [FunLike F α β] [InfHomClass F α β] (f : F) : InfClosed (Set.range f)

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeInf α
inst✝² : SemilatticeInf β
inst✝¹ : FunLike F α β
inst✝ : InfHomClass F α β
f : F
⊢ InfClosed (range ⇑f)

Tactic:
simpa using infClosed_univ.image f

Result:
no goals
-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
/-- We can express `ArithmeticFunction.vonMangoldt.residueClass` as a linear combination
of twists of the von Mangoldt function by Dirichlet characters. -/
lemma residueClass_apply (ha : IsUnit a) (n : ℕ) :
    residueClass a n =
      (q.totient : ℂ)⁻¹ * ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * χ n * vonMangoldt n

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
n : ℕ
⊢ ↑(residueClass a n) = (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * χ ↑n * ↑(Λ n)

Tactic:
rw [eq_inv_mul_iff_mul_eq₀ <| mod_cast (Nat.totient_pos.mpr q.pos_of_neZero).ne']

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
n : ℕ
⊢ ↑q.totient * ↑(residueClass a n) = ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * χ ↑n * ↑(Λ n)

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
n : ℕ
⊢ ↑q.totient * ↑(residueClass a n) = ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * χ ↑n * ↑(Λ n)

Tactic:
simp +contextual only [residueClass, Set.indicator_apply, Set.mem_setOf_eq, apply_ite,
  ofReal_zero, mul_zero, ← Finset.sum_mul, sum_char_inv_mul_char_eq ℂ ha n, eq_comm (a := a),
  ite_mul, zero_mul, ↓reduceIte, ite_self]

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_filter_lt_of_le_left [DecidablePred (· < c)] (hca : c ≤ a) :
    ((Ico a b).filter fun x => x < c) = ∅

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hca : c ≤ a
⊢ filter (fun x => x < c) (Ico a b) = ∅

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_left hca]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hca : c ≤ a
⊢ ∅.val = ∅

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hca : c ≤ a
⊢ ∅.val = ∅

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/Map2.lean
theorem zipLeft'_nil_right : zipLeft' as ([] : List β) = (as.map fun a => (a, none), [])

Proof state:
α : Type u
β : Type v
as : List α
⊢ as.zipLeft' [] = (map (fun a => (a, none)) as, [])

Tactic:
cases as <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/ByteArray.lean
theorem data_extract (a : ByteArray) (start stop) :
    (a.extract start stop).data = a.data.extract start stop

Proof state:
a : ByteArray
start stop : Nat
h : stop ≤ start
⊢ a.data.extract start (start + (stop - start)) = a.data.extract start stop

Tactic:
simp [h, Nat.sub_eq_zero_of_le, Array.extract_empty_of_stop_le_start]

Result:
no goals

Proof state:
a : ByteArray
start stop : Nat
⊢ a.data.extract start (start + (stop - start)) = a.data.extract start stop

Tactic:
match Nat.le_total start stop with
| .inl h => simp [h, Nat.add_sub_cancel']
| .inr h => simp [h, Nat.sub_eq_zero_of_le, Array.extract_empty_of_stop_le_start]

Result:
no goals

Proof state:
a : ByteArray
start stop : Nat
h : start ≤ stop
⊢ a.data.extract start (start + (stop - start)) = a.data.extract start stop

Tactic:
simp [h, Nat.add_sub_cancel']

Result:
no goals

Proof state:
a : ByteArray
start stop : Nat
⊢ (a.extract start stop).data = a.data.extract start stop

Tactic:
simp [extract]

Result:
a : ByteArray
start stop : Nat
⊢ a.data.extract start (start + (stop - start)) = a.data.extract start stop
-- Mathlib/Order/Filter/FilterProduct.lean
theorem max_def [LinearOrder β] (x y : β*) : max x y = map₂ max x y :=
  inductionOn₂ x y fun a b => by
    rcases le_total (a : β*) b with h | h
    · rw [max_eq_right h, map₂_coe, coe_eq]
      exact h.mono fun i hi => (max_eq_right hi).symm
    · rw [max_eq_left h, map₂_coe, coe_eq]
      exact h.mono fun i hi => (max_eq_left hi).symm

Proof state:
case inr
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑b ≤ ↑a
⊢ ↑a ⊔ ↑b = map₂ max ↑a ↑b

Tactic:
rw [max_eq_left h, map₂_coe, coe_eq]

Result:
case inr
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑b ≤ ↑a
⊢ a =ᶠ[↑φ] fun x => a x ⊔ b x

Proof state:
case inr
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑b ≤ ↑a
⊢ a =ᶠ[↑φ] fun x => a x ⊔ b x

Tactic:
exact h.mono fun i hi => (max_eq_left hi).symm

Result:
no goals

Proof state:
case inl
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ b =ᶠ[↑φ] fun x => a x ⊔ b x

Tactic:
exact h.mono fun i hi => (max_eq_right hi).symm

Result:
no goals

Proof state:
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
⊢ ↑a ⊔ ↑b = map₂ max ↑a ↑b

Tactic:
rcases le_total (a : β*) b with h | h

Result:
case inl
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ ↑a ⊔ ↑b = map₂ max ↑a ↑b

case inr
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑b ≤ ↑a
⊢ ↑a ⊔ ↑b = map₂ max ↑a ↑b

Proof state:
case inl
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ ↑a ⊔ ↑b = map₂ max ↑a ↑b

Tactic:
rw [max_eq_right h, map₂_coe, coe_eq]

Result:
case inl
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ b =ᶠ[↑φ] fun x => a x ⊔ b x
-- Mathlib/Data/ZMod/Basic.lean
lemma ZModModule.neg_eq_self (x : G) : -x = x

Proof state:
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x : G
⊢ -x = x

Tactic:
simp [add_self, eq_comm, ← sub_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma inv_hom_apply {R S : SemiRingCat} (e : R ≅ S) (r : R) : e.inv (e.hom r) = r

Proof state:
R S : SemiRingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/CoversTop.lean
lemma sections_ext (F : Sheaf J (Type _)) {x y : F.1.sections}
    (h : ∀ (i : I), x.1 (Opposite.op (Y i)) = y.1 (Opposite.op (Y i))) :
    x = y

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : ↑F.val.sections
h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))
⊢ x = y

Tactic:
ext W

Result:
case a.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : ↑F.val.sections
h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))
W : Cᵒᵖ
⊢ ↑x W = ↑y W

Proof state:
case a.h.intro.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : ↑F.val.sections
h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))
W : Cᵒᵖ
T : C
a : T ⟶ Opposite.unop W
i : I
b : T ⟶ Y i
⊢ F.val.map a.op (↑x W) = F.val.map a.op (↑y W)

Tactic:
simpa using congr_arg (F.1.map b.op) (h i)

Result:
no goals

Proof state:
case a.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : ↑F.val.sections
h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))
W : Cᵒᵖ
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Opposite.unop W⦄,
    (Sieve.ofObjects Y (Opposite.unop W)).arrows f → F.val.map f.op (↑x W) = F.val.map f.op (↑y W)

Tactic:
rintro T a ⟨i, ⟨b⟩⟩

Result:
case a.h.intro.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : ↑F.val.sections
h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))
W : Cᵒᵖ
T : C
a : T ⟶ Opposite.unop W
i : I
b : T ⟶ Y i
⊢ F.val.map a.op (↑x W) = F.val.map a.op (↑y W)

Proof state:
case a.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : ↑F.val.sections
h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))
W : Cᵒᵖ
⊢ ↑x W = ↑y W

Tactic:
apply (Presieve.isSeparated_of_isSheaf J F.1
  ((isSheaf_iff_isSheaf_of_type _ _).1 F.2) _ (hY W.unop)).ext

Result:
case a.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : ↑F.val.sections
h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))
W : Cᵒᵖ
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Opposite.unop W⦄,
    (Sieve.ofObjects Y (Opposite.unop W)).arrows f → F.val.map f.op (↑x W) = F.val.map f.op (↑y W)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem dvd_natAbs {a b : Int} : a ∣ b.natAbs ↔ a ∣ b :=
  match natAbs_eq b with
  | .inl e => by rw [← e]
  | .inr e => by rw [← Int.dvd_neg, ← e]

Proof state:
a b : Int
e : b = ↑b.natAbs
⊢ a ∣ ↑b.natAbs ↔ a ∣ b

Tactic:
rw [← e]

Result:
no goals

Proof state:
a b : Int
e : b = -↑b.natAbs
⊢ a ∣ ↑b.natAbs ↔ a ∣ b

Tactic:
rw [← Int.dvd_neg, ← e]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Plus.lean
theorem diagramNatTrans_zero [Preadditive D] (X : C) (P Q : Cᵒᵖ ⥤ D) :
    J.diagramNatTrans (0 : P ⟶ Q) X = 0

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : Preadditive D
X : C
P Q : Cᵒᵖ ⥤ D
⊢ J.diagramNatTrans 0 X = 0

Tactic:
ext : 2

Result:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : Preadditive D
X : C
P Q : Cᵒᵖ ⥤ D
x✝ : (J.Cover X)ᵒᵖ
⊢ (J.diagramNatTrans 0 X).app x✝ = NatTrans.app 0 x✝

Proof state:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : Preadditive D
X : C
P Q : Cᵒᵖ ⥤ D
x✝ : (J.Cover X)ᵒᵖ
⊢ (J.diagramNatTrans 0 X).app x✝ = NatTrans.app 0 x✝

Tactic:
refine Multiequalizer.hom_ext _ _ _ (fun i => ?_)

Result:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : Preadditive D
X : C
P Q : Cᵒᵖ ⥤ D
x✝ : (J.Cover X)ᵒᵖ
i : (unop x✝).shape.L
⊢ (J.diagramNatTrans 0 X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index Q) i =
    NatTrans.app 0 x✝ ≫ Multiequalizer.ι ((unop x✝).index Q) i

Proof state:
case w.h
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : Preadditive D
X : C
P Q : Cᵒᵖ ⥤ D
x✝ : (J.Cover X)ᵒᵖ
i : (unop x✝).shape.L
⊢ (J.diagramNatTrans 0 X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index Q) i =
    NatTrans.app 0 x✝ ≫ Multiequalizer.ι ((unop x✝).index Q) i

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_eq_one_of_not_module_finite (h : ¬Module.Finite R M) (f : M →ₗ[R] M) : f.det = 1

Proof state:
case hnc
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ¬Module.Finite R M
f : M →ₗ[R] M
⊢ ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)

Tactic:
exact fun ⟨_, ⟨b⟩⟩ ↦ h (Module.Finite.of_basis b)

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ¬Module.Finite R M
f : M →ₗ[R] M
⊢ LinearMap.det f = 1

Tactic:
rw [LinearMap.det, dif_neg, MonoidHom.one_apply]

Result:
case hnc
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ¬Module.Finite R M
f : M →ₗ[R] M
⊢ ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
-- Mathlib/RingTheory/GradedAlgebra/Basic.lean
theorem coe_decompose_mul_of_left_mem (n) [Decidable (i ≤ n)] (a_mem : a ∈ 𝒜 i) :
    (decompose 𝒜 (a * b) n : A) = if i ≤ n then a * decompose 𝒜 b (n - i) else 0

Proof state:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹¹ : Semiring A
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommMonoid ι
inst✝⁸ : PartialOrder ι
inst✝⁷ : CanonicallyOrderedAdd ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a b : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
a_mem : a ∈ 𝒜 i
⊢ ↑(((decompose 𝒜) (a * b)) n) = if i ≤ n then a * ↑(((decompose 𝒜) b) (n - i)) else 0

Tactic:
lift a to 𝒜 i using a_mem

Result:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹¹ : Semiring A
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommMonoid ι
inst✝⁸ : PartialOrder ι
inst✝⁷ : CanonicallyOrderedAdd ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
b : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
a : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (↑a * b)) n) = if i ≤ n then ↑a * ↑(((decompose 𝒜) b) (n - i)) else 0

Proof state:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹¹ : Semiring A
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommMonoid ι
inst✝⁸ : PartialOrder ι
inst✝⁷ : CanonicallyOrderedAdd ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
b : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
a : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (↑a * b)) n) = if i ≤ n then ↑a * ↑(((decompose 𝒜) b) (n - i)) else 0

Tactic:
rw [decompose_mul, decompose_coe, coe_of_mul_apply]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem strictMonoOn_logb_of_base_lt_one : StrictMonoOn (logb b) (Set.Iio 0)

Proof state:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ StrictMonoOn (logb b) (Iio 0)

Tactic:
rintro x (hx : x < 0) y (hy : y < 0) hxy

Result:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b x < logb b y

Proof state:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ |y| < |x|

Tactic:
rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]

Result:
no goals

Proof state:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b |x| < logb b |y|

Tactic:
refine logb_lt_logb_of_base_lt_one b_pos b_lt_one (abs_pos.2 hy.ne) ?_

Result:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ |y| < |x|

Proof state:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b x < logb b y

Tactic:
rw [← logb_abs y, ← logb_abs x]

Result:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b |x| < logb b |y|
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_eq_some_getElem_iff (a : Vector α n) (i : Nat) (h : i < n) :
    (a[i]? = some a[i]) ↔ True

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
h : i < n
⊢ a[i]? = some a[i] ↔ True

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem dist_triangle_nonarch (x y z : ∀ n, E n) : dist x z ≤ max (dist x y) (dist y z)

Proof state:
case inl
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ dist x x ≤ dist x y ⊔ dist y x

Tactic:
simp [PiNat.dist_self x, PiNat.dist_nonneg]

Result:
no goals

Proof state:
case inr.inl
E : ℕ → Type u_1
x z : (n : ℕ) → E n
hxz : x ≠ z
⊢ dist x z ≤ dist x x ⊔ dist x z

Tactic:
simp

Result:
no goals

Proof state:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
⊢ dist x z ≤ dist x y ⊔ dist y z

Tactic:
rcases eq_or_ne x z with (rfl | hxz)

Result:
case inl
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ dist x x ≤ dist x y ⊔ dist y x

case inr
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
⊢ dist x z ≤ dist x y ⊔ dist y z

Proof state:
case inr.inr.inl
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy hxz : x ≠ y
⊢ dist x y ≤ dist x y ⊔ dist y y

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
hxy : x ≠ y
⊢ dist x z ≤ dist x y ⊔ dist y z

Tactic:
rcases eq_or_ne y z with (rfl | hyz)

Result:
case inr.inr.inl
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy hxz : x ≠ y
⊢ dist x y ≤ dist x y ⊔ dist y y

case inr.inr.inr
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
hxy : x ≠ y
hyz : y ≠ z
⊢ dist x z ≤ dist x y ⊔ dist y z

Proof state:
case inr.inr.inr
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
hxy : x ≠ y
hyz : y ≠ z
⊢ dist x z ≤ dist x y ⊔ dist y z

Tactic:
simp only [dist_eq_of_ne, hxz, hxy, hyz, inv_le_inv₀, one_div, inv_pow, zero_lt_two, Ne,
  not_false_iff, le_max_iff, pow_le_pow_iff_right₀, one_lt_two, pow_pos,
  min_le_iff.1 (min_firstDiff_le x y z hxz)]

Result:
no goals

Proof state:
case inr
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
⊢ dist x z ≤ dist x y ⊔ dist y z

Tactic:
rcases eq_or_ne x y with (rfl | hxy)

Result:
case inr.inl
E : ℕ → Type u_1
x z : (n : ℕ) → E n
hxz : x ≠ z
⊢ dist x z ≤ dist x x ⊔ dist x z

case inr.inr
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
hxy : x ≠ y
⊢ dist x z ≤ dist x y ⊔ dist y z
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem inverse_range : LinearMap.range (inverse f).toFun = f.domain

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
⊢ LinearMap.range f.inverse.toFun = f.domain

Tactic:
rw [inverse, Submodule.toLinearPMap_range _ (mem_inverse_graph_snd_eq_zero hf),
  ← graph_map_fst_eq_domain, ← LinearEquiv.snd_comp_prodComm, Submodule.map_comp]

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
⊢ Submodule.map (LinearMap.snd R F E) (Submodule.map (LinearEquiv.prodComm R E F) f.graph) =
    Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph)

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
⊢ Submodule.map (LinearMap.snd R F E) (Submodule.map (LinearEquiv.prodComm R E F) f.graph) =
    Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph)

Tactic:
rfl

Result:
no goals