harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem insertNth_binop (op : ∀ j, α j → α j → α j) (i : Fin (n + 1)) (x y : α i)
    (p q : ∀ j, α (i.succAbove j)) :
    (i.insertNth (op i x y) fun j ↦ op _ (p j) (q j)) = fun j ↦
      op j (i.insertNth x p j) (i.insertNth y q j) :=
  insertNth_eq_iff.2 <| by unfold removeNth; simp

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
op : (j : Fin (n + 1)) → α j → α j → α j
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (i.succAbove j)
⊢ op i x y = op i (i.insertNth x p i) (i.insertNth y q i) ∧
    (fun j => op (i.succAbove j) (p j) (q j)) = i.removeNth fun j => op j (i.insertNth x p j) (i.insertNth y q j)

Tactic:
unfold removeNth

Result:
n : ℕ
α : Fin (n + 1) → Sort u_1
op : (j : Fin (n + 1)) → α j → α j → α j
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (i.succAbove j)
⊢ op i x y = op i (i.insertNth x p i) (i.insertNth y q i) ∧
    (fun j => op (i.succAbove j) (p j) (q j)) = fun i_1 =>
      (fun j => op j (i.insertNth x p j) (i.insertNth y q j)) (i.succAbove i_1)

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
op : (j : Fin (n + 1)) → α j → α j → α j
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (i.succAbove j)
⊢ op i x y = op i (i.insertNth x p i) (i.insertNth y q i) ∧
    (fun j => op (i.succAbove j) (p j) (q j)) = fun i_1 =>
      (fun j => op j (i.insertNth x p j) (i.insertNth y q j)) (i.succAbove i_1)

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma ofENat_eq_lift {x : Cardinal.{v}} {m : ℕ∞} : m = lift.{u} x ↔ m = x

Proof state:
x : Cardinal.{v}
m : ℕ∞
⊢ ↑m = lift.{u, v} x ↔ ↑m = x

Tactic:
rw [← lift_ofENat.{u, v}, lift_inj]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
@[simp]
lemma zero_pow_eq_zero [Nontrivial M₀] : (0 : M₀) ^ n = 0 ↔ n ≠ 0 :=
  ⟨by rintro h rfl; simp at h, zero_pow⟩

Proof state:
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
n : ℕ
inst✝ : Nontrivial M₀
⊢ 0 ^ n = 0 → n ≠ 0

Tactic:
rintro h rfl

Result:
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
h : 0 ^ 0 = 0
⊢ False

Proof state:
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
h : 0 ^ 0 = 0
⊢ False

Tactic:
simp at h

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean
theorem Monics.map_eq_prod {f : Monics k} :
    f.1.map (algebraMap k (AlgebraicClosure k)) =
      ∏ i, map (Ideal.Quotient.mk <| maxIdeal k) (X - C (MvPolynomial.X ⟨f, i⟩))

Proof state:
k : Type u
inst✝ : Field k
f : Monics k
⊢ map (algebraMap k (AlgebraicClosure k)) ↑f =
    ∏ i : Fin (↑f).natDegree, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨f, i⟩))

Tactic:
ext

Result:
case a
k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (map (algebraMap k (AlgebraicClosure k)) ↑f).coeff n✝ =
    (∏ i : Fin (↑f).natDegree, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨f, i⟩))).coeff n✝

Proof state:
case a
k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (map (algebraMap k (MvPolynomial (Vars k) k ⧸ maxIdeal k)) ↑f).coeff n✝ =
    (∏ i : Fin (↑f).natDegree, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨f, i⟩))).coeff n✝

Tactic:
rw [← Ideal.Quotient.mk_comp_algebraMap, ← map_map, ← Polynomial.map_prod, ← sub_eq_zero,
  ← coeff_sub, ← Polynomial.map_sub, ← subProdXSubC, coeff_map, Ideal.Quotient.eq_zero_iff_mem]

Result:
case a
k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (subProdXSubC f).coeff n✝ ∈ maxIdeal k

Proof state:
case a
k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (map (algebraMap k (AlgebraicClosure k)) ↑f).coeff n✝ =
    (∏ i : Fin (↑f).natDegree, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨f, i⟩))).coeff n✝

Tactic:
dsimp [AlgebraicClosure]

Result:
case a
k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (map (algebraMap k (MvPolynomial (Vars k) k ⧸ maxIdeal k)) ↑f).coeff n✝ =
    (∏ i : Fin (↑f).natDegree, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨f, i⟩))).coeff n✝

Proof state:
case a
k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (subProdXSubC f).coeff n✝ ∈ maxIdeal k

Tactic:
refine le_maxIdeal _ (Ideal.subset_span ⟨⟨f, _⟩, rfl⟩)

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem coe_sSup_of_directedOn {S : Set (NonUnitalSubsemiring R)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set R) = ⋃ s ∈ S, ↑s :=
  Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
S : Set (NonUnitalSubsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s

Tactic:
simp [mem_sSup_of_directedOn Sne hS]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
@[to_additive addProjection_respects_measure_apply]
lemma IsFundamentalDomain.projection_respects_measure_apply {ν : Measure α}
    (μ : Measure (Quotient α_mod_G)) [i : QuotientMeasureEqMeasurePreimage ν μ] {t : Set α}
    (fund_dom_t : IsFundamentalDomain G t ν) {U : Set (Quotient α_mod_G)}
    (meas_U : MeasurableSet U) : μ U = ν (π ⁻¹' U ∩ t)

Proof state:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
ν : Measure α
μ : Measure (Quotient α_mod_G)
i : QuotientMeasureEqMeasurePreimage ν μ
t : Set α
fund_dom_t : IsFundamentalDomain G t ν
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ μ U = ν (Quotient.mk α_mod_G ⁻¹' U ∩ t)

Tactic:
rw [fund_dom_t.projection_respects_measure (μ := μ), measure_map_restrict_apply ν t meas_U]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean
theorem zero_of_nonpos {x : ℝ} (hx : x ≤ 0) : expNegInvGlue x = 0

Proof state:
x : ℝ
hx : x ≤ 0
⊢ expNegInvGlue x = 0

Tactic:
simp [expNegInvGlue, hx]

Result:
no goals
-- Mathlib/Topology/Order/Lattice.lean
lemma ContinuousWithinAt.finset_inf' (hne : s.Nonempty)
    (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) : ContinuousWithinAt (s.inf' hne f) t x

Proof state:
L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeInf L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.inf' hne f) t x

Tactic:
simpa only [← Finset.inf'_apply] using finset_inf'_apply hne hs

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Algebra.lean
theorem evalₐ_mk (n : ℕ) (x : AdicCauchySequence I R) :
    evalₐ I n (mk I R x) = Ideal.Quotient.mk (I ^ n) (x.val n)

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x : AdicCauchySequence I R
⊢ (evalₐ I n) ((mk I R) x) = (Ideal.Quotient.mk (I ^ n)) (↑x n)

Tactic:
simp [evalₐ]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem frontier_lt_subset_eq (hf : Continuous f) (hg : Continuous g) :
    frontier { b | f b < g b } ⊆ { b | f b = g b }

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
⊢ frontier {b | f b < g b} ⊆ {b | f b = g b}

Tactic:
simpa only [← not_lt, ← compl_setOf, frontier_compl, eq_comm] using frontier_le_subset_eq hg hf

Result:
no goals
-- Mathlib/Algebra/Category/Semigrp/Basic.lean
@[to_additive]
lemma inv_hom_apply {X Y : Semigrp} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x

Proof state:
X Y : Semigrp
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Monoid.lean
theorem image_const_add_Icc : (fun x => a + x) '' Icc b c = Icc (a + b) (a + c)

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c : M
⊢ (fun x => a + x) '' Icc b c = Icc (a + b) (a + c)

Tactic:
simp only [add_comm a, image_add_const_Icc]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_zero_X_mul (φ : R⟦X⟧) : coeff R 0 (X * φ) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (coeff R 0) (X * φ) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Mod.lean
theorem lt_of_mul_lt_mul_left {a b c : Nat} (h : a * b < a * c) : b < c

Proof state:
a b c : Nat
h : a * b < a * c
⊢ b < c

Tactic:
cases a <;> simp_all

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem IsCoprime.pow_left (H : IsCoprime x y) : IsCoprime (x ^ m) y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y : R
m : ℕ
H : IsCoprime x y
⊢ IsCoprime (∏ _x ∈ range m, x) y

Tactic:
exact IsCoprime.prod_left fun _ _ ↦ H

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x y : R
m : ℕ
H : IsCoprime x y
⊢ IsCoprime (x ^ m) y

Tactic:
rw [← Finset.card_range m, ← Finset.prod_const]

Result:
R : Type u
inst✝ : CommSemiring R
x y : R
m : ℕ
H : IsCoprime x y
⊢ IsCoprime (∏ _x ∈ range m, x) y
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem zero_limZero : LimZero (0 : CauSeq β abv)
  | ε, ε0 => ⟨0, fun j _ => by simpa [abv_zero abv] using ε0⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε : α
ε0 : ε > 0
j : ℕ
x✝ : j ≥ 0
⊢ abv (↑0 j) < ε

Tactic:
simpa [abv_zero abv] using ε0

Result:
no goals
-- Mathlib/Data/Finset/Range.lean
theorem exists_nat_subset_range (s : Finset ℕ) : ∃ n : ℕ, s ⊆ range n :=
  s.induction_on (by simp)
    fun a _ _ ⟨n, hn⟩ => ⟨max (a + 1) n, insert_subset (by simp) (hn.trans (by simp))⟩

Proof state:
s : Finset ℕ
a : ℕ
x✝² : Finset ℕ
x✝¹ : a ∉ x✝²
x✝ : ∃ n, x✝² ⊆ range n
n : ℕ
hn : x✝² ⊆ range n
⊢ range n ⊆ range ((a + 1) ⊔ n)

Tactic:
simp

Result:
no goals

Proof state:
s : Finset ℕ
⊢ ∃ n, ∅ ⊆ range n

Tactic:
simp

Result:
no goals

Proof state:
s : Finset ℕ
a : ℕ
x✝² : Finset ℕ
x✝¹ : a ∉ x✝²
x✝ : ∃ n, x✝² ⊆ range n
n : ℕ
hn : x✝² ⊆ range n
⊢ a ∈ range ((a + 1) ⊔ n)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldrM_append [Monad m] [LawfulMonad m] (f : α → β → m β) (b) (l l' : List α) :
    (l ++ l').foldrM f b = l'.foldrM f b >>= l.foldrM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l l' : List α
⊢ foldrM f b (l ++ l') = do
    let init ← foldrM f b l'
    foldrM f init l

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem pentagon_hom_inv_inv_inv_hom :
    (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv =
      (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z

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

Tactic:
simp

Result:
no goals

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

Tactic:
rw [← cancel_epi (α_ W X (Y ⊗ Z)).inv, ← cancel_mono ((α_ W X Y).inv ▷ Z)]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ ((α_ W X (Y ⊗ Z)).inv ≫ (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv) ≫ (α_ W X Y).inv ▷ Z =
    ((α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z) ≫ (α_ W X Y).inv ▷ Z
-- Mathlib/CategoryTheory/Sites/Grothendieck.lean
theorem arrow_max (f : Y ⟶ X) (S : Sieve X) (hf : S f) : J.Covers S f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
hf : S.arrows f
⊢ J.Covers S f

Tactic:
rw [Covers, (Sieve.mem_iff_pullback_eq_top f).1 hf]

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
hf : S.arrows f
⊢ ⊤ ∈ J Y

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
hf : S.arrows f
⊢ ⊤ ∈ J Y

Tactic:
apply J.top_mem

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem liftOrGet_choice {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b = b) :
    ∀ o₁ o₂, liftOrGet f o₁ o₂ = o₁ ∨ liftOrGet f o₁ o₂ = o₂
  | none, none => Or.inl rfl
  | some _, none => Or.inl rfl
  | none, some _ => Or.inr rfl
  | some a, some b => by simpa [liftOrGet] using h a b

Proof state:
α : Type u_1
f : α → α → α
h : ∀ (a b : α), f a b = a ∨ f a b = b
a b : α
⊢ liftOrGet f (some a) (some b) = some a ∨ liftOrGet f (some a) (some b) = some b

Tactic:
simpa [liftOrGet] using h a b

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@[reassoc (attr := simp)]
lemma lift_φ₂ {A : C} (a : A ⟶ S.L₁.X₂) (b : A ⟶ S.L₀.X₃) (h : a ≫ S.L₁.g = b ≫ S.v₀₁.τ₃) :
    pullback.lift a b h ≫ S.φ₂ = a ≫ S.v₁₂.τ₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
a : A ⟶ S.L₁.X₂
b : A ⟶ S.L₀.X₃
h : a ≫ S.L₁.g = b ≫ S.v₀₁.τ₃
⊢ pullback.lift a b h ≫ S.φ₂ = a ≫ S.v₁₂.τ₂

Tactic:
simp [φ₂]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma homology_π_ι :
    S.homologyπ ≫ S.homologyι = S.iCycles ≫ S.pOpcycles

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ (S.leftHomologyπ ≫ S.leftHomologyIso.hom) ≫ S.rightHomologyIso.inv ≫ S.rightHomologyι = S.iCycles ≫ S.pOpcycles

Tactic:
simpa only [assoc, S.leftRightHomologyComparison_fac] using S.π_leftRightHomologyComparison_ι

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.homologyπ ≫ S.homologyι = S.iCycles ≫ S.pOpcycles

Tactic:
dsimp only [homologyπ, homologyι]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ (S.leftHomologyπ ≫ S.leftHomologyIso.hom) ≫ S.rightHomologyIso.inv ≫ S.rightHomologyι = S.iCycles ≫ S.pOpcycles
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem lt_log2_self : n < 2 ^ (n.log2 + 1) :=
  match n with
  | 0 => by simp
  | n+1 => (log2_lt n.succ_ne_zero).1 (Nat.le_refl _)

Proof state:
n : Nat
⊢ 0 < 2 ^ (log2 0 + 1)

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem range_subset_closure_interior : range I ⊆ closure (interior (range I))

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ I.target ⊆ closure (interior I.target)

Tactic:
exact I.target_subset_closure_interior

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ range ↑I ⊆ closure (interior (range ↑I))

Tactic:
rw [← I.target_eq]

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ I.target ⊆ closure (interior I.target)
-- Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean
theorem IsLowerSet.nonMemberSubfamily (h : IsLowerSet (𝒜 : Set (Finset α))) :
    IsLowerSet (𝒜.nonMemberSubfamily a : Set (Finset α)) := fun s t hts => by
  simp_rw [mem_coe, mem_nonMemberSubfamily]
  exact And.imp (h hts) (mt <| @hts _)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ≤ s
⊢ s ∈ 𝒜 ∧ a ∉ s → t ∈ 𝒜 ∧ a ∉ t

Tactic:
exact And.imp (h hts) (mt <| @hts _)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ≤ s
⊢ s ∈ ↑(Finset.nonMemberSubfamily a 𝒜) → t ∈ ↑(Finset.nonMemberSubfamily a 𝒜)

Tactic:
simp_rw [mem_coe, mem_nonMemberSubfamily]

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ≤ s
⊢ s ∈ 𝒜 ∧ a ∉ s → t ∈ 𝒜 ∧ a ∉ t
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem logMap_real (c : ℝ) :
    logMap (c • (1 : mixedSpace K)) = 0

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w ≠ w₀ }
⊢ logMap (c • 1) x✝ = 0 x✝

Tactic:
rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
  mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
  mul_one, sub_self, mul_zero, Pi.zero_apply]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
⊢ logMap (c • 1) = 0

Tactic:
ext

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w ≠ w₀ }
⊢ logMap (c • 1) x✝ = 0 x✝
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem ord_one : ord 1 = 1

Proof state:
⊢ ord 1 = 1

Tactic:
simpa using ord_nat 1

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasStrictFDerivAt.multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E}
    (h : ∀ i ∈ u, HasStrictFDerivAt (g i ·) (g' i) x) :
    HasStrictFDerivAt (fun x ↦ (u.map (g · x)).prod)
      (u.map fun i ↦ ((u.erase i).map (g · x)).prod • g' i).sum x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasStrictFDerivAt (fun x => g i x) (g' i) x
⊢ (Multiset.map (fun i => (Multiset.map (fun i => g (↑i) x) (u.attach.erase i)).prod • proj i) u.attach).sum.comp
      (pi fun i => g' ↑i) =
    (Multiset.map
        ((fun x_1 =>
            (Multiset.map (fun x_2 => g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod • g' x_1) ∘
          Subtype.val)
        u.attach).sum

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasStrictFDerivAt (fun x => g i x) (g' i) x
x✝ : E
⊢ ((Multiset.map (fun i => (Multiset.map (fun i => g (↑i) x) (u.attach.erase i)).prod • proj i) u.attach).sum.comp
        (pi fun i => g' ↑i))
      x✝ =
    (Multiset.map
          ((fun x_1 =>
              (Multiset.map (fun x_2 => g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod • g' x_1) ∘
            Subtype.val)
          u.attach).sum
      x✝

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasStrictFDerivAt (fun x => g i x) (g' i) x
⊢ HasStrictFDerivAt (fun x => (Multiset.map (fun x_1 => g x_1 x) u).prod)
    (Multiset.map (fun i => (Multiset.map (fun x_1 => g x_1 x) (u.erase i)).prod • g' i) u).sum x

Tactic:
simp only [← Multiset.attach_map_val u, Multiset.map_map]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasStrictFDerivAt (fun x => g i x) (g' i) x
⊢ HasStrictFDerivAt (fun x => (Multiset.map ((fun x_1 => g x_1 x) ∘ Subtype.val) u.attach).prod)
    (Multiset.map
        ((fun x_1 =>
            (Multiset.map (fun x_2 => g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod • g' x_1) ∘
          Subtype.val)
        u.attach).sum
    x
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem isBigO_one_exp_comp {f : α → ℝ} :
    ((fun _ => 1 : α → ℝ) =O[l] fun x => exp (f x)) ↔ IsBoundedUnder (· ≥ ·) l f

Proof state:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ ((fun x => 1) =O[l] fun x => rexp (f x)) ↔ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) l f

Tactic:
simp only [← exp_zero, isBigO_exp_comp_exp_comp, Pi.sub_def, zero_sub, isBoundedUnder_le_neg]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem legendreSym.at_neg_one (hp : p ≠ 2) : legendreSym p (-1) = χ₄ p

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ legendreSym p (-1) = χ₄ ↑p

Tactic:
simp only [legendreSym, card p, quadraticChar_neg_one ((ringChar_zmod_n p).substr hp),
  Int.cast_neg, Int.cast_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem HasImage.uniq (F' : MonoFactorisation f) (l : image f ⟶ F'.I) (w : l ≫ F'.m = image.ι f) :
    l = image.lift F' :=
  (cancel_mono F'.m).1 (by simp [w])

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
F' : MonoFactorisation f
l : image f ⟶ F'.I
w : l ≫ F'.m = image.ι f
⊢ l ≫ F'.m = image.lift F' ≫ F'.m

Tactic:
simp [w]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_le_self (ha : 0 ≤ a) (hb : 1 ≤ b) : a / b ≤ a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
ha : 0 ≤ a
hb : 1 ≤ b
⊢ a / b ≤ a

Tactic:
simpa only [div_one] using div_le_div_of_nonneg_left ha zero_lt_one hb

Result:
no goals
-- Mathlib/Data/List/Iterate.lean
theorem get?_iterate (f : α → α) (a : α) (n i : ℕ) (h : i < n) :
    get? (iterate f a n) i = f^[i] a

Proof state:
α : Type u_1
f : α → α
a : α
n i : ℕ
h : i < n
⊢ (iterate f a n).get? i = some (f^[i] a)

Tactic:
simp only [get?_eq_getElem?, getElem?_iterate, h]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_pos' [SMulPosStrictMono α β] (ha : 0 < a) (hb : 0 < b) : 0 < a • b

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosStrictMono α β
ha : 0 < a
hb : 0 < b
⊢ 0 < a • b

Tactic:
simpa only [zero_smul] using smul_lt_smul_of_pos_right ha hb

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- Expression for `hurwitzZetaEven a 1` as a limit. (Mathematically `hurwitzZetaEven a 1` is
undefined, but our construction assigns some value to it; this lemma is mostly of interest for
determining what that value is). -/
lemma tendsto_hurwitzZetaEven_sub_one_div_nhds_one (a : UnitAddCircle) :
    Tendsto (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / Gammaℝ s) (𝓝 1)
    (𝓝 (hurwitzZetaEven a 1))

Proof state:
a : UnitAddCircle
⊢ Tendsto (fun s => hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) (𝓝 1) (𝓝 (hurwitzZetaEven a 1))

Tactic:
simpa using (differentiableAt_hurwitzZetaEven_sub_one_div a).continuousAt.tendsto

Result:
no goals
-- Mathlib/Algebra/Lie/Killing.lean
/-- Given an equivalence `e` of Lie algebras from `L` to `L'`, and elements `x y : L`, the
respective Killing forms of `L` and `L'` satisfy `κ'(e x, e y) = κ(x, y)`. -/
@[simp] lemma killingForm_of_equiv_apply (e : L ≃ₗ⁅R⁆ L') (x y : L) :
    killingForm R L' (e x) (e y) = killingForm R L x y

Proof state:
R : Type u_1
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L' : Type u_4
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
x y : L
⊢ ((killingForm R L') (e x)) (e y) = ((killingForm R L) x) y

Tactic:
simp_rw [killingForm_apply_apply, ← LieAlgebra.conj_ad_apply, ← LinearEquiv.conj_comp,
  LinearMap.trace_conj']

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_comap {L : Type v} [Field L] (f : L →+* E)
    (B : Subfield L) : relrank (A.comap f) B = relrank A (B.map f)

Proof state:
E : Type v
inst✝¹ : Field E
A : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
B : Subfield L
⊢ (comap f A).relrank B = A.relrank (map f B)

Tactic:
simpa only [lift_id] using A.lift_relrank_comap f B

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem head!_mem_head? [Inhabited α] : ∀ {l : List α}, l ≠ [] → head! l ∈ head? l
  | [], h => by contradiction
  | _ :: _, _ => rfl

Proof state:
α : Type u
inst✝ : Inhabited α
h : [] ≠ []
⊢ [].head! ∈ [].head?

Tactic:
contradiction

Result:
no goals