harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Part.lean
lemma Monotone.partMap (hg : Monotone g) : Monotone fun x ↦ (g x).map f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : β → γ
g : α → Part β
hg : Monotone g
⊢ Monotone fun x => map f (g x)

Tactic:
simpa only [← bind_some_eq_map] using hg.partBind monotone_const

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
@[simp]
lemma scaleRoots_C (r c : R) : (C c).scaleRoots r = C c

Proof state:
R : Type u_1
inst✝ : Semiring R
r c : R
⊢ (C c).scaleRoots r = C c

Tactic:
ext

Result:
case a
R : Type u_1
inst✝ : Semiring R
r c : R
n✝ : ℕ
⊢ ((C c).scaleRoots r).coeff n✝ = (C c).coeff n✝

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
r c : R
n✝ : ℕ
⊢ ((C c).scaleRoots r).coeff n✝ = (C c).coeff n✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem top_prod (s : Submonoid N) : (⊤ : Submonoid M).prod s = s.comap (MonoidHom.snd M N) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_snd]

Proof state:
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid N
x : M × N
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (MonoidHom.snd M N) s

Tactic:
simp [mem_prod, MonoidHom.coe_snd]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineSpace.lean
lemma not_isIntegralHom [Nonempty S] [Nonempty n] : ¬ IsIntegralHom (𝔸(n; S) ↘ S)

Proof state:
n : Type v
S : Scheme
inst✝¹ : Nonempty ↑↑S.toPresheafedSpace
inst✝ : Nonempty n
⊢ ¬IsIntegralHom (𝔸(n; S) ↘ S)

Tactic:
simp [isIntegralHom_over_iff_isEmpty]

Result:
no goals
-- Mathlib/FieldTheory/Galois/Infinite.lean
theorem isOpen_and_normal_iff_finite_and_isGalois (L : IntermediateField k K) [IsGalois k K] :
    IsOpen L.fixingSubgroup.carrier ∧ L.fixingSubgroup.Normal ↔
    FiniteDimensional k L ∧ IsGalois k L

Proof state:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
⊢ IsOpen L.fixingSubgroup.carrier ∧ L.fixingSubgroup.Normal ↔ FiniteDimensional k ↥L ∧ IsGalois k ↥L

Tactic:
rw [isOpen_iff_finite, normal_iff_isGalois]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
theorem log_pos_real {x : ℝ≥0∞} (h : x ≠ 0) (h' : x ≠ ⊤) :
    log x = Real.log (ENNReal.toReal x)

Proof state:
x : ℝ≥0∞
h : x ≠ 0
h' : x ≠ ⊤
⊢ x.log = ↑(Real.log x.toReal)

Tactic:
simp [log, h, h']

Result:
no goals
-- Mathlib/CategoryTheory/CommSq.lean
theorem op (p : CommSq f g h i) : CommSq i.op h.op g.op f.op :=
  ⟨by simp only [← op_comp, p.w]⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ i.op ≫ g.op = h.op ≫ f.op

Tactic:
simp only [← op_comp, p.w]

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem iInf_ne_top [CompleteLattice α] (f : ℝ≥0∞ → α) :
    ⨅ (x) (_ : x ≠ ∞), f x = ⨅ x : ℝ≥0, f x

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
f : ℝ≥0∞ → α
⊢ ⨅ x, ⨅ (_ : x ≠ ⊤), f x = ⨅ x, f ↑x

Tactic:
rw [iInf_subtype', cinfi_ne_top]

Result:
no goals
-- Mathlib/Algebra/Ring/InjSurj.lean
theorem leftDistribClass [Mul α] [Add α] [LeftDistribClass α] (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) : LeftDistribClass β where
  left_distrib x y z := hf <| by simp only [*, left_distrib]

Proof state:
α : Type u_1
β : Type u_2
f : β → α
hf : Injective f
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
x y z : β
⊢ f (x * (y + z)) = f (x * y + x * z)

Tactic:
simp only [*, left_distrib]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mod_self (a : Ordinal) : a % a = 0 :=
  if a0 : a = 0 then by simp only [a0, zero_mod]
  else by simp only [mod_def, div_self a0, mul_one, sub_self]

Proof state:
a : Ordinal.{u_4}
a0 : a = 0
⊢ a % a = 0

Tactic:
simp only [a0, zero_mod]

Result:
no goals

Proof state:
a : Ordinal.{u_4}
a0 : ¬a = 0
⊢ a % a = 0

Tactic:
simp only [mod_def, div_self a0, mul_one, sub_self]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Icc_add_one_left_eq_Ioc (a b : α) : Icc (a + 1) b = Ioc a b

Proof state:
α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Icc (a + 1) b = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Icc_succ_left_eq_Ioc a b

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem false_of_mem_take_findIdx {xs : List α} {p : α → Bool} (h : x ∈ xs.take (xs.findIdx p)) :
    p x = false

Proof state:
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < min (findIdx p xs) xs.length
⊢ i < findIdx p xs

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
x : α
xs : List α
p : α → Bool
h : ∃ i hm, xs[i] = x
⊢ p x = false

Tactic:
obtain ⟨i, h, rfl⟩ := h

Result:
case intro.intro
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < min (findIdx p xs) xs.length
⊢ p xs[i] = false

Proof state:
α : Type u_1
x : α
xs : List α
p : α → Bool
h : x ∈ take (findIdx p xs) xs
⊢ p x = false

Tactic:
simp only [mem_take_iff_getElem, forall_exists_index] at h

Result:
α : Type u_1
x : α
xs : List α
p : α → Bool
h : ∃ i hm, xs[i] = x
⊢ p x = false

Proof state:
case intro.intro
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < min (findIdx p xs) xs.length
⊢ p xs[i] = false

Tactic:
exact not_of_lt_findIdx (by omega)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_take (a : Vector α n) (m) : (a.take m).toList = a.toList.take m

Proof state:
α : Type u_1
n : Nat
a : Vector α n
m : Nat
⊢ (a.take m).toList = List.take m a.toList

Tactic:
simp [List.take_of_length_le]

Result:
no goals
-- Mathlib/GroupTheory/PushoutI.lean
theorem prod_summand_smul {i : ι} (g : G i) (w : NormalWord d) :
    (g • w).prod = of i g * w.prod

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
⊢ (g • w).prod = (of i) g * w.prod

Tactic:
simp only [prod, summand_smul_def', equivPair, rcons, Word.equivPair_symm,
  Equiv.coe_fn_mk, Equiv.coe_fn_symm_mk, Word.equivPair_smul_same,
  Word.equivPair_tail_eq_inv_smul, Word.rcons_eq_smul, ← of_apply_eq_base φ i,
  MonoidHom.apply_ofInjective_symm, equiv_fst_eq_mul_inv, mul_assoc, map_mul, map_inv,
  Word.prod_smul, ofCoprodI_of, inv_mul_cancel_left, mul_inv_cancel_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zip_append :
    ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
      zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
  | [], r₁, l₂, r₂, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
  | l₁, r₁, [], r₂, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
  | a :: l₁, r₁, b :: l₂, r₂, h => by
    simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]

Proof state:
α : Type u_1
β : Type u_2
a : α
l₁ r₁ : List α
b : β
l₂ r₂ : List β
h : (a :: l₁).length = (b :: l₂).length
⊢ (a :: l₁ ++ r₁).zip (b :: l₂ ++ r₂) = (a :: l₁).zip (b :: l₂) ++ r₁.zip r₂

Tactic:
simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l₁ r₁ : List α
r₂ : List β
h : l₁.length = [].length
⊢ (l₁ ++ r₁).zip ([] ++ r₂) = l₁.zip [] ++ r₁.zip r₂

Tactic:
simp only [eq_nil_of_length_eq_zero h]

Result:
α : Type u_1
β : Type u_2
l₁ r₁ : List α
r₂ : List β
h : l₁.length = [].length
⊢ ([] ++ r₁).zip ([] ++ r₂) = [].zip [] ++ r₁.zip r₂

Proof state:
α : Type u_1
β : Type u_2
l₁ r₁ : List α
r₂ : List β
h : l₁.length = [].length
⊢ ([] ++ r₁).zip ([] ++ r₂) = [].zip [] ++ r₁.zip r₂

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r₁ : List α
l₂ r₂ : List β
h : [].length = l₂.length
⊢ ([] ++ r₁).zip ([] ++ r₂) = [].zip [] ++ r₁.zip r₂

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r₁ : List α
l₂ r₂ : List β
h : [].length = l₂.length
⊢ ([] ++ r₁).zip (l₂ ++ r₂) = [].zip l₂ ++ r₁.zip r₂

Tactic:
simp only [eq_nil_of_length_eq_zero h.symm]

Result:
α : Type u_1
β : Type u_2
r₁ : List α
l₂ r₂ : List β
h : [].length = l₂.length
⊢ ([] ++ r₁).zip ([] ++ r₂) = [].zip [] ++ r₁.zip r₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem log2_zero : Nat.log2 0 = 0

Proof state:
⊢ log2 0 = 0

Tactic:
simp [Nat.log2]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem trailingDegree_eq_iff_natTrailingDegree_eq {p : R[X]} {n : ℕ} (hp : p ≠ 0) :
    p.trailingDegree = n ↔ p.natTrailingDegree = n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.trailingDegree = ↑n ↔ p.natTrailingDegree = n

Tactic:
rw [trailingDegree_eq_natTrailingDegree hp, Nat.cast_inj]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
@[reassoc (attr := simp)]
lemma commShiftIso_inv_app_counit_app [adj.CommShift A] (a : A) (Y : D) :
    ((G ⋙ F).commShiftIso a).inv.app Y ≫ adj.counit.app (Y⟦a⟧) = (adj.counit.app Y)⟦a⟧'

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
inst✝ : adj.CommShift A
a : A
Y : D
⊢ ((G ⋙ F).commShiftIso a).inv.app Y ≫ adj.counit.app ((shiftFunctor D a).obj Y) =
    (shiftFunctor D a).map (adj.counit.app Y)

Tactic:
simp [← cancel_epi (((G ⋙ F).commShiftIso _).hom.app _)]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem single_one_dotProduct [DecidableEq n] (i : n) (v : n → α) :
    dotProduct (Pi.single i 1) v = v i

Proof state:
n : Type u_3
α : Type v
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
i : n
v : n → α
⊢ Pi.single i 1 ⬝ᵥ v = v i

Tactic:
rw [single_dotProduct, one_mul]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_zpow_isUnit (a : E) {n : ℤ} (hn : IsUnit n) : ‖a ^ n‖ = ‖a‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
hn : IsUnit n
⊢ ‖a ^ n‖ = ‖a‖

Tactic:
rw [← norm_pow_natAbs, Int.isUnit_iff_natAbs_eq.mp hn, pow_one]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Real.lean
lemma dist_le_of_mem_pi_Icc (hx : x ∈ Icc x' y') (hy : y ∈ Icc x' y') : dist x y ≤ dist x' y'

Proof state:
ι : Type u_1
inst✝ : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
⊢ dist x y ≤ dist x' y'

Tactic:
refine (dist_pi_le_iff dist_nonneg).2 fun b =>
  (Real.dist_le_of_mem_uIcc ?_ ?_).trans (dist_le_pi_dist x' y' b) <;> refine Icc_subset_uIcc ?_

Result:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ x b ∈ Icc (x' b) (y' b)

case refine_2
ι : Type u_1
inst✝ : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ y b ∈ Icc (x' b) (y' b)

Proof state:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ x b ∈ Icc (x' b) (y' b)

case refine_2
ι : Type u_1
inst✝ : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ y b ∈ Icc (x' b) (y' b)

Tactic:
exacts [⟨hx.1 _, hx.2 _⟩, ⟨hy.1 _, hy.2 _⟩]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem IsUniformInducing.prod {α' : Type*} {β' : Type*} [UniformSpace α'] [UniformSpace β']
    {e₁ : α → α'} {e₂ : β → β'} (h₁ : IsUniformInducing e₁) (h₂ : IsUniformInducing e₂) :
    IsUniformInducing fun p : α × β => (e₁ p.1, e₂ p.2) :=
  ⟨by simp [Function.comp_def, uniformity_prod, ← h₁.1, ← h₂.1, comap_inf, comap_comap]⟩

Proof state:
α : Type u
β : Type v
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
α' : Type u_1
β' : Type u_2
inst✝¹ : UniformSpace α'
inst✝ : UniformSpace β'
e₁ : α → α'
e₂ : β → β'
h₁ : IsUniformInducing e₁
h₂ : IsUniformInducing e₂
⊢ comap (fun x => ((e₁ x.1.1, e₂ x.1.2), e₁ x.2.1, e₂ x.2.2)) (𝓤 (α' × β')) = 𝓤 (α × β)

Tactic:
simp [Function.comp_def, uniformity_prod, ← h₁.1, ← h₂.1, comap_inf, comap_comap]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem HasFPowerSeriesAt.sub (hf : HasFPowerSeriesAt f pf x) (hg : HasFPowerSeriesAt g pg x) :
    HasFPowerSeriesAt (f - g) (pf - pg) x

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f pf x
hg : HasFPowerSeriesAt g pg x
⊢ HasFPowerSeriesAt (f - g) (pf - pg) x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/MinMax.lean
@[to_additive]
lemma fn_min_mul_fn_max (f : α → β) (a b : α) : f (min a b) * f (max a b) = f a * f b

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommSemigroup β
f : α → β
a b : α
⊢ f (a ⊓ b) * f (a ⊔ b) = f a * f b

Tactic:
obtain h | h := le_total a b <;> simp [h, mul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
lemma mem_distinguishedTriangles_iff (T : Triangle Cᵒᵖ) :
    T ∈ distinguishedTriangles C ↔
      ((triangleOpEquivalence C).inverse.obj T).unop ∈ distTriang C

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ T ∈ distinguishedTriangles C ↔
    Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_coe_pi : (π : Angle).sign = 0

Proof state:
⊢ (↑π).sign = 0

Tactic:
rw [sign, sin_coe_pi, _root_.sign_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem le_total (x y : BitVec n) : x ≤ y ∨ y ≤ x

Proof state:
n : Nat
x y : BitVec n
⊢ x.toNat ≤ y.toNat ∨ y.toNat ≤ x.toNat

Tactic:
apply Nat.le_total

Result:
no goals

Proof state:
n : Nat
x y : BitVec n
⊢ x ≤ y ∨ y ≤ x

Tactic:
simp only [le_def]

Result:
n : Nat
x y : BitVec n
⊢ x.toNat ≤ y.toNat ∨ y.toNat ≤ x.toNat
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
lemma exp_two_pi_mul_int (n : ℤ) : exp (2 * π * n) = 1

Proof state:
n : ℤ
⊢ exp (2 * π * ↑n) = 1

Tactic:
simpa only [mul_comm] using exp_int_mul_two_pi n

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem injective_iff_bijective {f : α → α} : Injective f ↔ Bijective f

Proof state:
α : Type u_1
inst✝ : Finite α
f : α → α
⊢ Injective f ↔ Bijective f

Tactic:
simp [Bijective, injective_iff_surjective]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem mem_iSup {x : Set α} {f : ι → Filter α} : x ∈ iSup f ↔ ∀ i, x ∈ f i

Proof state:
α : Type u
ι : Sort x
x : Set α
f : ι → Filter α
⊢ x ∈ iSup f ↔ ∀ (i : ι), x ∈ f i

Tactic:
simp only [← Filter.mem_sets, iSup_sets_eq, mem_iInter]

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
@[norm_cast] lemma num_coe (q : ℚ≥0) : (q : ℚ).num = q.num

Proof state:
q : ℚ≥0
⊢ (↑q).num = ↑q.num

Tactic:
simp only [num, Int.natCast_natAbs, Rat.num_nonneg, coe_nonneg, abs_of_nonneg]

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem LinearMap.eq_of_localization_maximal (g g' : M →ₗ[R] M₁)
    (h : ∀ (P : Ideal R) [P.IsMaximal],
      IsLocalizedModule.map P.primeCompl (f P) (f₁ P) g =
      IsLocalizedModule.map P.primeCompl (f P) (f₁ P) g') :
    g = g' :=
  ext fun x ↦ Module.eq_of_localization_maximal _ f₁ _ _ fun P _ ↦ by
    simpa only [IsLocalizedModule.map_apply] using DFunLike.congr_fun (h P) (f P x)

Proof state:
R : Type u_1
M : Type u_2
M₁ : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
M₁ₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_6
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (M₁ₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (M₁ₚ P)
f₁ : (P : Ideal R) → [inst : P.IsMaximal] → M₁ →ₗ[R] M₁ₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f₁ P)
g g' : M →ₗ[R] M₁
h :
  ∀ (P : Ideal R) [inst : P.IsMaximal],
    (IsLocalizedModule.map P.primeCompl (f P) (f₁ P)) g = (IsLocalizedModule.map P.primeCompl (f P) (f₁ P)) g'
x : M
P : Ideal R
x✝ : P.IsMaximal
⊢ (f₁ P) (g x) = (f₁ P) (g' x)

Tactic:
simpa only [IsLocalizedModule.map_apply] using DFunLike.congr_fun (h P) (f P x)

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem zero_vecMul [Fintype m] (A : Matrix m n α) : 0 ᵥ* A = 0

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
⊢ 0 ᵥ* A = 0

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x✝ : n
⊢ (0 ᵥ* A) x✝ = 0 x✝

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x✝ : n
⊢ (0 ᵥ* A) x✝ = 0 x✝

Tactic:
simp [vecMul]

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem length_gather (a : Composition n) (b : Composition a.length) :
    length (a.gather b) = b.length :=
  show (map List.sum (a.blocks.splitWrtComposition b)).length = b.blocks.length by
    rw [length_map, length_splitWrtComposition]

Proof state:
n : ℕ
a : Composition n
b : Composition a.length
⊢ (List.map sum (a.blocks.splitWrtComposition b)).length = b.blocks.length

Tactic:
rw [length_map, length_splitWrtComposition]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_zero (a) : a ⨳ 0 = 0

Proof state:
a : Ordinal.{u_1}
⊢ a ⨳ 0 = 0

Tactic:
rw [← Ordinal.le_zero, nmul_le_iff]

Result:
a : Ordinal.{u_1}
⊢ ∀ a' < a, ∀ b' < 0, a' ⨳ 0 ♯ a ⨳ b' < 0 ♯ a' ⨳ b'

Proof state:
a : Ordinal.{u_1}
⊢ ∀ a' < a, ∀ b' < 0, a' ⨳ 0 ♯ a ⨳ b' < 0 ♯ a' ⨳ b'

Tactic:
exact fun _ _ a ha => (Ordinal.not_lt_zero a ha).elim

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
lemma functor_obj (i : J) (hi : i < j) {k : J} (iter' : Φ.Iteration k) (hk : i ≤ k) :
    (functor hj iter).obj ⟨i, hi.le⟩ = iter'.F.obj ⟨i, hk⟩

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (ofCocone (colimit.cocone (inductiveSystem iter))).obj ⟨i, ⋯⟩ = iter'.F.obj ⟨i, hk⟩

Tactic:
rw [ofCocone_obj_eq _ _ hi]

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (inductiveSystem iter).obj ⟨i, hi⟩ = iter'.F.obj ⟨i, hk⟩

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (inductiveSystem iter).obj ⟨i, hi⟩ = iter'.F.obj ⟨i, hk⟩

Tactic:
apply congr_obj

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (functor hj iter).obj ⟨i, ⋯⟩ = iter'.F.obj ⟨i, hk⟩

Tactic:
dsimp only [functor]

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (ofCocone (colimit.cocone (inductiveSystem iter))).obj ⟨i, ⋯⟩ = iter'.F.obj ⟨i, hk⟩
-- Mathlib/Data/Fin/SuccPred.lean
@[simp]
lemma orderSucc_castSucc {n : ℕ} (i : Fin n) :
    Order.succ i.castSucc = i.succ

Proof state:
n : ℕ
i : Fin n
⊢ Order.succ i.castSucc = i.succ

Tactic:
simp [orderSucc_apply]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem preimage_frontier_subset_frontier_preimage (hf : IsOpenMap f) {s : Set Y} :
    f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)

Tactic:
simpa only [frontier_eq_closure_inter_closure, preimage_inter] using
  inter_subset_inter hf.preimage_closure_subset_closure_preimage
    hf.preimage_closure_subset_closure_preimage

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem mk_coeff (x : TruncatedWittVector p n R) : (mk p fun i => x.coeff i) = x

Proof state:
p n : ℕ
R : Type u_1
x : TruncatedWittVector p n R
⊢ (mk p fun i => coeff i x) = x

Tactic:
ext i

Result:
case h
p n : ℕ
R : Type u_1
x : TruncatedWittVector p n R
i : Fin n
⊢ coeff i (mk p fun i => coeff i x) = coeff i x

Proof state:
case h
p n : ℕ
R : Type u_1
x : TruncatedWittVector p n R
i : Fin n
⊢ coeff i (mk p fun i => coeff i x) = coeff i x

Tactic:
rw [coeff_mk]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem sInter_empty : ⋂₀ (∅ : Class.{u}) = univ

Proof state:
⊢ ⋂₀ ∅ = univ

Tactic:
rw [sInter, classToCong_empty, Set.sInter_empty, univ]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Invariant.lean
protected lemma codisjoint_iff {p q : f.invtSubmodule} :
    Codisjoint p q ↔ Codisjoint (p : Submodule R M) (q : Submodule R M)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : ↥f.invtSubmodule
⊢ Codisjoint p q ↔ Codisjoint ↑p ↑q

Tactic:
obtain ⟨p, hp⟩ := p

Result:
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
q : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ Codisjoint ⟨p, hp⟩ q ↔ Codisjoint ↑⟨p, hp⟩ ↑q

Proof state:
case mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ Codisjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Codisjoint ↑⟨p, hp⟩ ↑⟨q, hq⟩

Tactic:
simp

Result:
no goals

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
q : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ Codisjoint ⟨p, hp⟩ q ↔ Codisjoint ↑⟨p, hp⟩ ↑q

Tactic:
obtain ⟨q, hq⟩ := q

Result:
case mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ Codisjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Codisjoint ↑⟨p, hp⟩ ↑⟨q, hq⟩
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ioc_pred_pred_eq_Ico_of_not_isMin (ha : ¬ IsMin a) (b : α) :
    Ioc (pred a) (pred b) = Ico a b :=
  coe_injective <| by simpa using Set.Ioc_pred_pred_eq_Ico_of_not_isMin ha _

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ ↑(Ioc (pred a) (pred b)) = ↑(Ico a b)

Tactic:
simpa using Set.Ioc_pred_pred_eq_Ico_of_not_isMin ha _

Result:
no goals