harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
lemma cotangentComplexAux_apply (P : PreSubmersivePresentation R S) (x : P.ker) (i : P.rels) :
    P.cotangentComplexAux (Cotangent.mk x) i = (aeval P.val) (pderiv (P.map i) x.val)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : PreSubmersivePresentation R S
x : ↥P.ker
i : P.rels
⊢ (Finsupp.linearEquivFunOnFinite S S P.rels)
      ((Finsupp.lcomapDomain P.map ⋯)
        (P.cotangentSpaceBasis.repr (1 ⊗ₜ[P.toExtension.Ring] (KaehlerDifferential.D R P.toExtension.Ring) ↑x)))
      i =
    (aeval P.val) ((pderiv (P.map i)) ↑x)

Tactic:
simp only [Generators.toExtension_Ring, Finsupp.lcomapDomain_apply,
  Finsupp.linearEquivFunOnFinite_apply, Finsupp.comapDomain_apply,
  Generators.cotangentSpaceBasis_repr_tmul, one_mul]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : PreSubmersivePresentation R S
x : ↥P.ker
i : P.rels
⊢ P.cotangentComplexAux (Cotangent.mk x) i = (aeval P.val) ((pderiv (P.map i)) ↑x)

Tactic:
dsimp only [cotangentComplexAux, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
  cotangentComplex_mk]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : PreSubmersivePresentation R S
x : ↥P.ker
i : P.rels
⊢ (Finsupp.linearEquivFunOnFinite S S P.rels)
      ((Finsupp.lcomapDomain P.map ⋯)
        (P.cotangentSpaceBasis.repr (1 ⊗ₜ[P.toExtension.Ring] (KaehlerDifferential.D R P.toExtension.Ring) ↑x)))
      i =
    (aeval P.val) ((pderiv (P.map i)) ↑x)
-- Mathlib/Algebra/CharP/Lemmas.lean
lemma sub_pow_expChar_of_commute (h : Commute x y) : (x - y) ^ p = x ^ p - y ^ p

Proof state:
R : Type u_1
inst✝ : Ring R
x y : R
p : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ p = x ^ p - y ^ p

Tactic:
simp [eq_sub_iff_add_eq, ← add_pow_expChar_of_commute _ (h.sub_left rfl)]

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
/-- The exponential characteristic is a prime number or one.
See also `CharP.char_is_prime_or_zero`. -/
lemma expChar_is_prime_or_one (q : ℕ) [hq : ExpChar R q] : Nat.Prime q ∨ q = 1

Proof state:
case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
q : ℕ
hp : Nat.Prime q
hchar✝ : CharP R q
⊢ Nat.Prime q ∨ q = 1

Tactic:
exact .inl hp

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ Nat.Prime 1 ∨ 1 = 1

Tactic:
exact .inr rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
q : ℕ
hq : ExpChar R q
⊢ Nat.Prime q ∨ q = 1

Tactic:
cases hq with
| zero => exact .inr rfl
| prime hp => exact .inl hp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
theorem ι_desc (j : J) : ι arrows j ≫ desc f fs w = fs _

Proof state:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
j : J
⊢ ι arrows j ≫ desc f fs w = fs j

Tactic:
simp only [colimit.ι_desc, WidePushoutShape.mkCocone_pt, WidePushoutShape.mkCocone_ι_app]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean
@[simp]
lemma opEquiv_symm_add {n : ℤ} (x y : ShiftedHom (Opposite.op Y) (Opposite.op X) n) :
    (opEquiv n).symm (x + y) = (opEquiv n).symm x + (opEquiv n).symm y

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n : ℤ
x y : ShiftedHom (Opposite.op Y) (Opposite.op X) n
⊢ ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C n).map (Quiver.Hom.unop (x + y)) =
    ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C n).map (Quiver.Hom.unop x) +
      ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C n).map (Quiver.Hom.unop y)

Tactic:
rw [← Preadditive.comp_add, ← Functor.map_add]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n : ℤ
x y : ShiftedHom (Opposite.op Y) (Opposite.op X) n
⊢ ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C n).map (Quiver.Hom.unop (x + y)) =
    ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C n).map (Quiver.Hom.unop x + Quiver.Hom.unop y)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n : ℤ
x y : ShiftedHom (Opposite.op Y) (Opposite.op X) n
⊢ ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C n).map (Quiver.Hom.unop (x + y)) =
    ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C n).map (Quiver.Hom.unop x + Quiver.Hom.unop y)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n : ℤ
x y : ShiftedHom (Opposite.op Y) (Opposite.op X) n
⊢ (opEquiv n).symm (x + y) = (opEquiv n).symm x + (opEquiv n).symm y

Tactic:
dsimp [opEquiv_symm_apply]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n : ℤ
x y : ShiftedHom (Opposite.op Y) (Opposite.op X) n
⊢ ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C n).map (Quiver.Hom.unop (x + y)) =
    ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C n).map (Quiver.Hom.unop x) +
      ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C n).map (Quiver.Hom.unop y)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_mkArray_of_pos {n : Nat} {a : α} (h : p a) :
    (mkArray n a).eraseP p = mkArray (n - 1) a

Proof state:
α : Type u_1
p : α → Bool
n : Nat
a : α
h : p a = true
⊢ (List.eraseP p (List.replicate n a)).toArray = (List.replicate (n - 1) a).toArray

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
n : Nat
a : α
h : p a = true
⊢ (mkArray n a).eraseP p = mkArray (n - 1) a

Tactic:
simp only [← List.toArray_replicate, List.eraseP_toArray]

Result:
α : Type u_1
p : α → Bool
n : Nat
a : α
h : p a = true
⊢ (List.eraseP p (List.replicate n a)).toArray = (List.replicate (n - 1) a).toArray
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.closure_iInter_eq_biInter_closure_of_forall_subset [Nonempty ι] {Js : ι → Set α}
    (hI : M.Indep I) (hJs : ∀ i, Js i ⊆ I) : M.closure (⋂ i, Js i) = ⋂ i, M.closure (Js i) :=
  closure_iInter_eq_iInter_closure_of_iUnion_indep _ (hI.subset <| by simpa)

Proof state:
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst✝ : Nonempty ι
Js : ι → Set α
hI : M.Indep I
hJs : ∀ (i : ι), Js i ⊆ I
⊢ ⋃ i, Js i ⊆ I

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem support_update_ne_zero (f : Π₀ i, β i) (i : ι) {b : β i} (h : b ≠ 0) :
    support (f.update i b) = insert i f.support

Proof state:
case h.inl
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
⊢ i ∈ (f.update i b).support ↔ i ∈ insert i f.support

Tactic:
simp [h]

Result:
no goals

Proof state:
case h.inr
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
j : ι
hi : i ≠ j
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support

Tactic:
simp [hi.symm]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
⊢ (f.update i b).support = insert i f.support

Tactic:
ext j

Result:
case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
j : ι
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
j : ι
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support

Tactic:
rcases eq_or_ne i j with (rfl | hi)

Result:
case h.inl
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
⊢ i ∈ (f.update i b).support ↔ i ∈ insert i f.support

case h.inr
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
j : ι
hi : i ≠ j
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support
-- Mathlib/MeasureTheory/Group/Pointwise.lean
theorem MeasurableSet.const_smul {G α : Type*} [Group G] [MulAction G α] [MeasurableSpace G]
    [MeasurableSpace α] [MeasurableSMul G α] {s : Set α} (hs : MeasurableSet s) (a : G) :
    MeasurableSet (a • s)

Proof state:
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSMul G α
s : Set α
hs : MeasurableSet s
a : G
⊢ MeasurableSet (a • s)

Tactic:
rw [← preimage_smul_inv]

Result:
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSMul G α
s : Set α
hs : MeasurableSet s
a : G
⊢ MeasurableSet ((fun x => a⁻¹ • x) ⁻¹' s)

Proof state:
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSMul G α
s : Set α
hs : MeasurableSet s
a : G
⊢ MeasurableSet ((fun x => a⁻¹ • x) ⁻¹' s)

Tactic:
exact measurable_const_smul _ hs

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean
lemma exists_leftFraction₂ {X Y : C} (f f' : L.obj X ⟶ L.obj Y) :
    ∃ (φ : W.LeftFraction₂ X Y), f = φ.fst.map L (inverts L W) ∧
      f' = φ.snd.map L (inverts L W)

Proof state:
case intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map L ⋯
α : W.LeftFraction φ.Y' φ'.Y'
hα : (RightFraction.mk φ.s ⋯ φ'.s).f ≫ α.s = (RightFraction.mk φ.s ⋯ φ'.s).s ≫ α.f
ψ : W.LeftFraction₂ X Y := LeftFraction₂.mk (φ.f ≫ α.f) (φ'.f ≫ α.s) (φ'.s ≫ α.s) ⋯
⊢ ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯

Tactic:
have := inverts L W _ φ'.hs

Result:
case intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map L ⋯
α : W.LeftFraction φ.Y' φ'.Y'
hα : (RightFraction.mk φ.s ⋯ φ'.s).f ≫ α.s = (RightFraction.mk φ.s ⋯ φ'.s).s ≫ α.f
ψ : W.LeftFraction₂ X Y := LeftFraction₂.mk (φ.f ≫ α.f) (φ'.f ≫ α.s) (φ'.s ≫ α.s) ⋯
this : IsIso (L.map φ'.s)
⊢ ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma isUnramifiedIn_comap [IsGalois k K] {w : InfinitePlace K} :
    (w.comap (algebraMap k K)).IsUnramifiedIn K ↔ w.IsUnramified k

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
H : IsUnramified k w
v : InfinitePlace K
hv : v.comap (algebraMap k K) = w.comap (algebraMap k K)
⊢ IsUnramified k v

Tactic:
obtain ⟨σ, rfl⟩ := exists_smul_eq_of_comap_eq hv

Result:
case intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
v : InfinitePlace K
σ : K ≃ₐ[k] K
H : IsUnramified k (σ • v)
hv : v.comap (algebraMap k K) = (σ • v).comap (algebraMap k K)
⊢ IsUnramified k v

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
⊢ IsUnramifiedIn K (w.comap (algebraMap k K)) ↔ IsUnramified k w

Tactic:
refine ⟨fun H ↦ H _ rfl, fun H v hv ↦ ?_⟩

Result:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
H : IsUnramified k w
v : InfinitePlace K
hv : v.comap (algebraMap k K) = w.comap (algebraMap k K)
⊢ IsUnramified k v

Proof state:
case intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
v : InfinitePlace K
σ : K ≃ₐ[k] K
H : IsUnramified k (σ • v)
hv : v.comap (algebraMap k K) = (σ • v).comap (algebraMap k K)
⊢ IsUnramified k v

Tactic:
rwa [isUnramified_smul_iff] at H

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
lemma exp_mul_le_cosh_add_mul_sinh {t : ℝ} (ht : |t| ≤ 1) (x : ℝ) :
    exp (t * x) ≤ cosh x + t * sinh x

Proof state:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ 0 ≤ (1 - t) / 2

Tactic:
linarith

Result:
no goals

Proof state:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ 0 ≤ (1 + t) / 2

Tactic:
linarith

Result:
no goals

Proof state:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ (1 + t) / 2 * rexp x + (1 - t) / 2 * rexp (-x) = (rexp x + rexp (-x)) / 2 + t * ((rexp x - rexp (-x)) / 2)

Tactic:
ring

Result:
no goals

Proof state:
t : ℝ
ht : |t| ≤ 1
x : ℝ
⊢ rexp (t * x) ≤ cosh x + t * sinh x

Tactic:
rw [abs_le] at ht

Result:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ rexp (t * x) ≤ cosh x + t * sinh x

Proof state:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ rexp (t * x) ≤ cosh x + t * sinh x

Tactic:
calc
  _ = exp ((1 + t) / 2 * x + (1 - t) / 2 * (-x)) := by ring_nf
  _ ≤ (1 + t) / 2 * exp x + (1 - t) / 2 * exp (-x) :=
      convexOn_exp.2 (Set.mem_univ _) (Set.mem_univ _) (by linarith) (by linarith) <| by ring
  _ = _ := by rw [cosh_eq, sinh_eq]; ring

Result:
no goals

Proof state:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ rexp (t * x) = rexp ((1 + t) / 2 * x + (1 - t) / 2 * -x)

Tactic:
ring_nf

Result:
no goals

Proof state:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ (1 + t) / 2 + (1 - t) / 2 = 1

Tactic:
ring

Result:
no goals

Proof state:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ (1 + t) / 2 * rexp x + (1 - t) / 2 * rexp (-x) = cosh x + t * sinh x

Tactic:
rw [cosh_eq, sinh_eq]

Result:
t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ (1 + t) / 2 * rexp x + (1 - t) / 2 * rexp (-x) = (rexp x + rexp (-x)) / 2 + t * ((rexp x - rexp (-x)) / 2)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_setIfInBounds {f : α → β} {l : Vector α n} {i : Nat} {a : α} :
    (l.setIfInBounds i a).map f = (l.map f).setIfInBounds i (f a)

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β
l : Vector α n
i : Nat
a : α
⊢ map f (l.setIfInBounds i a) = (map f l).setIfInBounds i (f a)

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
i : Nat
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map f ({ toArray := toArray✝, size_toArray := size_toArray✝ }.setIfInBounds i a) =
    (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).setIfInBounds i (f a)

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
i : Nat
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map f ({ toArray := toArray✝, size_toArray := size_toArray✝ }.setIfInBounds i a) =
    (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).setIfInBounds i (f a)

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem support_ofFinset : (ofFinset f s h h').support = ↑s ∩ Function.support f :=
  Set.ext fun a => by simpa [mem_support_iff] using mt (h' a)

Proof state:
α : Type u_1
f : α → ℝ≥0∞
s : Finset α
h : ∑ a ∈ s, f a = 1
h' : ∀ a ∉ s, f a = 0
a : α
⊢ a ∈ (ofFinset f s h h').support ↔ a ∈ ↑s ∩ Function.support f

Tactic:
simpa [mem_support_iff] using mt (h' a)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem eq_prod_range_div {M : Type*} [CommGroup M] (f : ℕ → M) (n : ℕ) :
    f n = f 0 * ∏ i ∈ range n, f (i + 1) / f i

Proof state:
M : Type u_6
inst✝ : CommGroup M
f : ℕ → M
n : ℕ
⊢ f n = f 0 * ∏ i ∈ range n, f (i + 1) / f i

Tactic:
rw [prod_range_div, mul_div_cancel]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
lemma reflect_map {S : Type*} [Semiring S] (f : R →+* S) (p : R[X]) (n : ℕ) :
    (p.map f).reflect n = (p.reflect n).map f

Proof state:
case a
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
p : R[X]
n n✝ : ℕ
⊢ (reflect n (map f p)).coeff n✝ = (map f (reflect n p)).coeff n✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ reflect n (map f p) = map f (reflect n p)

Tactic:
ext

Result:
case a
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
p : R[X]
n n✝ : ℕ
⊢ (reflect n (map f p)).coeff n✝ = (map f (reflect n p)).coeff n✝
-- Mathlib/LinearAlgebra/Charpoly/Basic.lean
theorem aeval_self_charpoly : aeval f f.charpoly = 0

Proof state:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ (algEquivMatrix (chooseBasis R M)).toLinearEquiv ((aeval f) f.charpoly) = 0

Tactic:
rw [AlgEquiv.toLinearEquiv_apply, ← AlgEquiv.coe_algHom, ← Polynomial.aeval_algHom_apply _ _ _,
  charpoly_def]

Result:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ (aeval (↑(algEquivMatrix (chooseBasis R M)) f)) ((toMatrix (chooseBasis R M) (chooseBasis R M)) f).charpoly = 0

Proof state:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ (aeval f) f.charpoly = 0

Tactic:
apply (LinearEquiv.map_eq_zero_iff (algEquivMatrix (chooseBasis R M)).toLinearEquiv).1

Result:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ (algEquivMatrix (chooseBasis R M)).toLinearEquiv ((aeval f) f.charpoly) = 0

Proof state:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ (aeval (↑(algEquivMatrix (chooseBasis R M)) f)) ((toMatrix (chooseBasis R M) (chooseBasis R M)) f).charpoly = 0

Tactic:
exact Matrix.aeval_self_charpoly _

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem right_mem_Icc : b ∈ Icc a b ↔ a ≤ b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ b ∈ Icc a b ↔ a ≤ b

Tactic:
simp only [mem_Icc, and_true, le_rfl]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem conj_eq_one_iff : a * b * a⁻¹ = 1 ↔ b = 1

Proof state:
G : Type u_3
inst✝ : Group G
a b : G
⊢ a * b * a⁻¹ = 1 ↔ b = 1

Tactic:
rw [mul_inv_eq_one, mul_right_eq_self]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Prod.lean
theorem boxProd_neighborSet (x : α × β) :
    (G □ H).neighborSet x = G.neighborSet x.1 ×ˢ {x.2} ∪ {x.1} ×ˢ H.neighborSet x.2

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
⊢ (G □ H).neighborSet x = G.neighborSet x.1 ×ˢ {x.2} ∪ {x.1} ×ˢ H.neighborSet x.2

Tactic:
ext ⟨a', b'⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
a' : α
b' : β
⊢ (a', b') ∈ (G □ H).neighborSet x ↔ (a', b') ∈ G.neighborSet x.1 ×ˢ {x.2} ∪ {x.1} ×ˢ H.neighborSet x.2

Proof state:
case h.mk
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
a' : α
b' : β
⊢ G.Adj x.1 a' ∧ x.2 = b' ∨ H.Adj x.2 b' ∧ x.1 = a' ↔ G.Adj x.1 a' ∧ b' = x.2 ∨ a' = x.1 ∧ H.Adj x.2 b'

Tactic:
simp only [eq_comm, and_comm]

Result:
no goals

Proof state:
case h.mk
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
a' : α
b' : β
⊢ (a', b') ∈ (G □ H).neighborSet x ↔ (a', b') ∈ G.neighborSet x.1 ×ˢ {x.2} ∪ {x.1} ×ˢ H.neighborSet x.2

Tactic:
simp only [mem_neighborSet, Set.mem_union, boxProd_adj, Set.mem_prod, Set.mem_singleton_iff]

Result:
case h.mk
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
a' : α
b' : β
⊢ G.Adj x.1 a' ∧ x.2 = b' ∨ H.Adj x.2 b' ∧ x.1 = a' ↔ G.Adj x.1 a' ∧ b' = x.2 ∨ a' = x.1 ∧ H.Adj x.2 b'
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem degreeOf_coeff_finSuccEquiv (p : MvPolynomial (Fin (n + 1)) R) (j : Fin n) (i : ℕ) :
    degreeOf j (Polynomial.coeff (finSuccEquiv R n p) i) ≤ degreeOf j.succ p

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ (((finSuccEquiv R n) p).coeff i).support
⊢ (cons i m) j.succ ≤ p.support.sup fun m => m j.succ

Tactic:
exact Finset.le_sup
  (f := fun (g : Fin (Nat.succ n) →₀ ℕ) => g (Fin.succ j))
  (support_coeff_finSuccEquiv.1 hm)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ (((finSuccEquiv R n) p).coeff i).support
⊢ m j ≤ p.support.sup fun m => m j.succ

Tactic:
rw [← Finsupp.cons_succ j i m]

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ (((finSuccEquiv R n) p).coeff i).support
⊢ (cons i m) j.succ ≤ p.support.sup fun m => m j.succ

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ degreeOf j (((finSuccEquiv R n) p).coeff i) ≤ degreeOf j.succ p

Tactic:
rw [degreeOf_eq_sup, degreeOf_eq_sup, Finset.sup_le_iff]

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ ∀ b ∈ (((finSuccEquiv R n) p).coeff i).support, b j ≤ p.support.sup fun m => m j.succ

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ ∀ b ∈ (((finSuccEquiv R n) p).coeff i).support, b j ≤ p.support.sup fun m => m j.succ

Tactic:
intro m hm

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ (((finSuccEquiv R n) p).coeff i).support
⊢ m j ≤ p.support.sup fun m => m j.succ
-- Mathlib/Algebra/Ring/InjSurj.lean
theorem rightDistribClass [Mul α] [Add α] [RightDistribClass α] (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) : RightDistribClass β where
  right_distrib x y z := hf <| by simp only [*, right_distrib]

Proof state:
α : Type u_1
β : Type u_2
f : β → α
hf : Injective f
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
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 * z + y * z)

Tactic:
simp only [*, right_distrib]

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem invFunIdAssoc_hom_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
    (invFunIdAssoc e F).hom.app X = F.map (e.counit.app X)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : D ⥤ E
X : D
⊢ (e.invFunIdAssoc F).hom.app X = F.map (e.counit.app X)

Tactic:
dsimp [invFunIdAssoc]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : D ⥤ E
X : D
⊢ 𝟙 (F.obj (e.functor.obj (e.inverse.obj X))) ≫ F.map (e.counitIso.hom.app X) ≫ 𝟙 (F.obj X) = F.map (e.counit.app X)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : D ⥤ E
X : D
⊢ 𝟙 (F.obj (e.functor.obj (e.inverse.obj X))) ≫ F.map (e.counitIso.hom.app X) ≫ 𝟙 (F.obj X) = F.map (e.counit.app X)

Tactic:
simp

Result:
no goals