harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/AbsoluteValue.lean
theorem det_le {A : Matrix n n R} {abv : AbsoluteValue R S} {x : S} (hx : ∀ i j, abv (A i j) ≤ x) :
    abv A.det ≤ Nat.factorial (Fintype.card n) • x ^ Fintype.card n :=
  calc
    abv A.det = abv (∑ σ : Perm n, Perm.sign σ • ∏ i, A (σ i) i) := congr_arg abv (det_apply _)
    _ ≤ ∑ σ : Perm n, abv (Perm.sign σ • ∏ i, A (σ i) i) := abv.sum_le _ _
    _ = ∑ σ : Perm n, ∏ i, abv (A (σ i) i) :=
      (sum_congr rfl fun σ _ => by rw [abv.map_units_int_smul, abv.map_prod])
    _ ≤ ∑ _σ : Perm n, ∏ _i : n, x :=
      (sum_le_sum fun _ _ => prod_le_prod (fun _ _ => abv.nonneg _) fun _ _ => hx _ _)
    _ = ∑ _σ : Perm n, x ^ Fintype.card n :=
      (sum_congr rfl fun _ _ => by rw [prod_const, Finset.card_univ])
    _ = Nat.factorial (Fintype.card n) • x ^ Fintype.card n

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), abv (A i j) ≤ x
⊢ ∑ _σ : Perm n, x ^ Fintype.card n = (Fintype.card n).factorial • x ^ Fintype.card n

Tactic:
rw [sum_const, Finset.card_univ, Fintype.card_perm]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), abv (A i j) ≤ x
x✝¹ : Perm n
x✝ : x✝¹ ∈ univ
⊢ ∏ _i : n, x = x ^ Fintype.card n

Tactic:
rw [prod_const, Finset.card_univ]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), abv (A i j) ≤ x
σ : Perm n
x✝ : σ ∈ univ
⊢ abv (Perm.sign σ • ∏ i : n, A (σ i) i) = ∏ i : n, abv (A (σ i) i)

Tactic:
rw [abv.map_units_int_smul, abv.map_prod]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem eval₂Hom_comp_bind₂ (f : S →+* T) (g : σ → T) (h : R →+* MvPolynomial σ S) :
    (eval₂Hom f g).comp (bind₂ h) = eval₂Hom ((eval₂Hom f g).comp h) g

Proof state:
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
⊢ (eval₂Hom f g).comp (bind₂ h) = eval₂Hom ((eval₂Hom f g).comp h) g

Tactic:
ext : 2 <;> simp

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem IsPreconnected.union (x : α) {s t : Set α} (H1 : x ∈ s) (H2 : x ∈ t) (H3 : IsPreconnected s)
    (H4 : IsPreconnected t) : IsPreconnected (s ∪ t) :=
  sUnion_pair s t ▸ isPreconnected_sUnion x {s, t} (by rintro r (rfl | rfl | h) <;> assumption)
    (by rintro r (rfl | rfl | h) <;> assumption)

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ ∀ s_1 ∈ {s, t}, x ∈ s_1

Tactic:
rintro r (rfl | rfl | h) <;> assumption

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ ∀ s_1 ∈ {s, t}, IsPreconnected s_1

Tactic:
rintro r (rfl | rfl | h) <;> assumption

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem inv_whiskerRight {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) [IsIso η] :
    inv (η ▷ h) = inv η ▷ h

Proof state:
B : Type u
inst✝¹ : Bicategory B
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst✝ : IsIso η
⊢ inv (η ▷ h) = inv η ▷ h

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Result:
case hom_inv_id
B : Type u
inst✝¹ : Bicategory B
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst✝ : IsIso η
⊢ η ▷ h ≫ inv η ▷ h = 𝟙 (f ≫ h)

Proof state:
case hom_inv_id
B : Type u
inst✝¹ : Bicategory B
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst✝ : IsIso η
⊢ η ▷ h ≫ inv η ▷ h = 𝟙 (f ≫ h)

Tactic:
simp only [← comp_whiskerRight, id_whiskerRight, IsIso.hom_inv_id]

Result:
no goals
-- Mathlib/Topology/List.lean
theorem List.tendsto_cons {a : α} {l : List α} :
    Tendsto (fun p : α × List α => List.cons p.1 p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a::l))

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ (Filter.map (fun a b => (a, b).1 :: (a, b).2) (𝓝 a)).seq (𝓝 l) ≤ cons <$> 𝓝 a <*> 𝓝 l

Tactic:
exact le_rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun p => p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: l))

Tactic:
rw [nhds_cons, Tendsto, Filter.map_prod]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ (Filter.map (fun a b => (a, b).1 :: (a, b).2) (𝓝 a)).seq (𝓝 l) ≤ cons <$> 𝓝 a <*> 𝓝 l
-- Mathlib/Analysis/Calculus/Deriv/Shift.lean
/-- Translation in the domain does not change the derivative. -/
lemma HasDerivAt.comp_const_sub (a x : 𝕜) (hf : HasDerivAt f f' (a - x)) :
    HasDerivAt (fun x ↦ f (a - x)) (-f') x

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
a x : 𝕜
hf : HasDerivAt f f' (a - x)
⊢ HasDerivAt (fun x => f (a - x)) (-f') x

Tactic:
simpa [Function.comp_def] using HasDerivAt.scomp (𝕜 := 𝕜) x hf <| hasDerivAt_id' x |>.const_sub a

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem mul_div_cancel' {n m : Nat} (H : n ∣ m) : n * (m / n) = m

Proof state:
n m : Nat
H : n ∣ m
this : m % n + n * (m / n) = m
⊢ n * (m / n) = m

Tactic:
rwa [mod_eq_zero_of_dvd H, Nat.zero_add] at this

Result:
no goals

Proof state:
n m : Nat
H : n ∣ m
⊢ n * (m / n) = m

Tactic:
have := mod_add_div m n

Result:
n m : Nat
H : n ∣ m
this : m % n + n * (m / n) = m
⊢ n * (m / n) = m
-- Mathlib/Algebra/Homology/ImageToKernel.lean
theorem imageToKernel_epi_comp {Z : V} (h : Z ⟶ A) [Epi h] (w) :
    imageToKernel (h ≫ f) g w =
      Subobject.ofLE _ _ (imageSubobject_comp_le h f) ≫
        imageToKernel f g ((cancel_epi h).mp (by simpa using w : h ≫ f ≫ g = h ≫ 0))

Proof state:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
Z : V
h : Z ⟶ A
inst✝ : Epi h
w : (h ≫ f) ≫ g = 0
⊢ imageToKernel (h ≫ f) g w = (imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯ ≫ imageToKernel f g ⋯

Tactic:
ext

Result:
case h
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
Z : V
h : Z ⟶ A
inst✝ : Epi h
w : (h ≫ f) ≫ g = 0
⊢ imageToKernel (h ≫ f) g w ≫ (kernelSubobject g).arrow =
    ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯ ≫ imageToKernel f g ⋯) ≫ (kernelSubobject g).arrow

Proof state:
case h
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
Z : V
h : Z ⟶ A
inst✝ : Epi h
w : (h ≫ f) ≫ g = 0
⊢ imageToKernel (h ≫ f) g w ≫ (kernelSubobject g).arrow =
    ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯ ≫ imageToKernel f g ⋯) ≫ (kernelSubobject g).arrow

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
Z : V
h : Z ⟶ A
inst✝ : Epi h
w : (h ≫ f) ≫ g = 0
⊢ h ≫ f ≫ g = h ≫ 0

Tactic:
simpa using w

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem min_add_right {a b : Nat} : min a (a + b) = a

Proof state:
a b : Nat
⊢ min a (a + b) = a

Tactic:
rw [Nat.min_def]

Result:
a b : Nat
⊢ (if a ≤ a + b then a else a + b) = a

Proof state:
a b : Nat
⊢ (if a ≤ a + b then a else a + b) = a

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_top :
    s.einfsep = ∞ ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep = ⊤ ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ⊤

Tactic:
simp_rw [einfsep, iInf_eq_top]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem lineMap_apply_one_sub (p₀ p₁ : P1) (c : k) : lineMap p₀ p₁ (1 - c) = lineMap p₁ p₀ c

Proof state:
case h.e_6.h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c : k
⊢ (lineMap 1 0) (1 - c) = c

Tactic:
simp [lineMap_apply]

Result:
no goals

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c : k
⊢ (lineMap p₁ p₀) ((lineMap 1 0) (1 - c)) = (lineMap p₁ p₀) c

Tactic:
congr

Result:
case h.e_6.h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c : k
⊢ (lineMap 1 0) (1 - c) = c

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c : k
⊢ (lineMap p₀ p₁) (1 - c) = (lineMap p₁ p₀) c

Tactic:
rw [lineMap_symm p₀, comp_apply]

Result:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c : k
⊢ (lineMap p₁ p₀) ((lineMap 1 0) (1 - c)) = (lineMap p₁ p₀) c
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem monomial_mem_lifts {s : S} (n : ℕ) (h : s ∈ Set.range f) : monomial n s ∈ lifts f

Proof state:
case intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
r : R
h : f r ∈ Set.range ⇑f
⊢ (monomial n) (f r) ∈ lifts f

Tactic:
use monomial n r

Result:
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
r : R
h : f r ∈ Set.range ⇑f
⊢ (mapRingHom f) ((monomial n) r) = (monomial n) (f r)

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
h : s ∈ Set.range ⇑f
⊢ (monomial n) s ∈ lifts f

Tactic:
obtain ⟨r, rfl⟩ := Set.mem_range.1 h

Result:
case intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
r : R
h : f r ∈ Set.range ⇑f
⊢ (monomial n) (f r) ∈ lifts f

Proof state:
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
r : R
h : f r ∈ Set.range ⇑f
⊢ (mapRingHom f) ((monomial n) r) = (monomial n) (f r)

Tactic:
simp only [coe_mapRingHom, Set.mem_univ, map_monomial, Subsemiring.coe_top, eq_self_iff_true,
  and_self_iff]

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_eq_zero_iff : Ico a b = 0 ↔ ¬a < b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ico a b = 0 ↔ ¬a < b

Tactic:
rw [Ico, Finset.val_eq_zero, Finset.Ico_eq_empty_iff]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem l_ciSup_set (gc : GaloisConnection l u) {s : Set γ} {f : γ → α} (hf : BddAbove (f '' s))
    (hne : s.Nonempty) : l (⨆ i : s, f i) = ⨆ i : s, l (f i)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : s.Nonempty
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)

Tactic:
haveI := hne.to_subtype

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : s.Nonempty
this : Nonempty ↑s
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (range fun x => f ↑x)
hne : s.Nonempty
this : Nonempty ↑s
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)

Tactic:
exact gc.l_ciSup hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : s.Nonempty
this : Nonempty ↑s
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)

Tactic:
rw [image_eq_range] at hf

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (range fun x => f ↑x)
hne : s.Nonempty
this : Nonempty ↑s
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)
-- Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
theorem lTensorOne'_one_tmul (n : N) : N.lTensorOne' (1 ⊗ₜ[R] n) = n

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
n : ↥N
⊢ N.lTensorOne' (1 ⊗ₜ[R] n) = n

Tactic:
simpa using lTensorOne'_tmul 1 n

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gaugeSeminorm_ball_one (hs : IsOpen s) : (gaugeSeminorm hs₀ hs₁ hs₂).ball 0 1 = s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
hs₀ : Balanced 𝕜 s
hs₁ : Convex ℝ s
hs₂ : Absorbent ℝ s
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : IsOpen s
⊢ (gaugeSeminorm hs₀ hs₁ hs₂).ball 0 1 = s

Tactic:
rw [Seminorm.ball_zero_eq]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
hs₀ : Balanced 𝕜 s
hs₁ : Convex ℝ s
hs₂ : Absorbent ℝ s
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : IsOpen s
⊢ {y | (gaugeSeminorm hs₀ hs₁ hs₂) y < 1} = s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
hs₀ : Balanced 𝕜 s
hs₁ : Convex ℝ s
hs₂ : Absorbent ℝ s
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : IsOpen s
⊢ {y | (gaugeSeminorm hs₀ hs₁ hs₂) y < 1} = s

Tactic:
exact gauge_lt_one_eq_self_of_isOpen hs₁ hs₂.zero_mem hs

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem Subsequent.moveLeft_mk_left {xR : xr → PGame} {i : xl} (xL : xl → PGame) (j) :
    Subsequent ((xL i).moveLeft j) (mk xl xr xL xR)

Proof state:
xl xr : Type u
xR : xr → PGame
i : xl
xL : xl → PGame
j : (xL i).LeftMoves
⊢ ((xL i).moveLeft j).Subsequent (mk xl xr xL xR)

Tactic:
pgame_wf_tac

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
lemma sum_neg_one_pow (R : Type*) [Ring R] (m : ℕ) :
    (∑ n : Fin m, (-1) ^ n.1 : R) = if Even m then 0 else 1

Proof state:
case succ
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1 : Fin n, (-1) ^ ↑n_1 = if Even n then 0 else 1
⊢ (if Even n then 0 else 1) + (-1) ^ n = if Even n then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1 : Fin n, (-1) ^ ↑n_1 = if Even n then 0 else 1
h : Even n
⊢ 0 + (-1) ^ n = 1

case neg
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1 : Fin n, (-1) ^ ↑n_1 = if Even n then 0 else 1
h : ¬Even n
⊢ 1 + (-1) ^ n = 0

Proof state:
case succ
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1 : Fin n, (-1) ^ ↑n_1 = if Even n then 0 else 1
⊢ ∑ n_1 : Fin (n + 1), (-1) ^ ↑n_1 = if Even (n + 1) then 0 else 1

Tactic:
simp only [Fin.sum_univ_castSucc, Fin.coe_castSucc, IH, Fin.val_last,
  Nat.even_add_one, ← Nat.not_even_iff_odd, ite_not]

Result:
case succ
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1 : Fin n, (-1) ^ ↑n_1 = if Even n then 0 else 1
⊢ (if Even n then 0 else 1) + (-1) ^ n = if Even n then 1 else 0

Proof state:
case neg
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1 : Fin n, (-1) ^ ↑n_1 = if Even n then 0 else 1
h : ¬Even n
⊢ 1 + (-1) ^ n = 0

Tactic:
simp [(Nat.not_even_iff_odd.mp h).neg_pow]

Result:
no goals

Proof state:
case zero
R : Type u_3
inst✝ : Ring R
⊢ ∑ n : Fin 0, (-1) ^ ↑n = if Even 0 then 0 else 1

Tactic:
simp

Result:
no goals

Proof state:
case pos
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1 : Fin n, (-1) ^ ↑n_1 = if Even n then 0 else 1
h : Even n
⊢ 0 + (-1) ^ n = 1

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Pi.lean
theorem hasFDerivAt_update (x : ∀ i, E i) {i : ι} (y : E i) :
    HasFDerivAt (Function.update x i) (.pi (Pi.single i (.id 𝕜 (E i)))) y

Proof state:
case neg
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
t : E i
j : ι
hji : ¬j = i
⊢ x j = x j + 0 (t - x i)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_12.h.h
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
update_eq : Function.update x i = (fun x_1 => x) + ⇑l ∘ fun x_1 => x_1 - x i
e_8✝ : Pi.addCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : Pi.module ι E 𝕜 = NormedSpace.toModule
e_10✝ : Pi.topologicalSpace = UniformSpace.toTopologicalSpace
⊢ l = 0 + l.comp (ContinuousLinearMap.id 𝕜 (E i))

Tactic:
rw [zero_add, ContinuousLinearMap.comp_id]

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
theorem scheme_toScheme {X Y : Scheme.{u}} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] :
    toScheme Y f.toPshHom = X

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : AlgebraicGeometry.IsOpenImmersion f
⊢ toScheme Y f.toPshHom = X

Tactic:
apply scheme_eq_of_locallyRingedSpace_eq

Result:
case H
X Y : Scheme
f : X ⟶ Y
inst✝ : AlgebraicGeometry.IsOpenImmersion f
⊢ (toScheme Y f.toPshHom).toLocallyRingedSpace = X.toLocallyRingedSpace

Proof state:
case H
X Y : Scheme
f : X ⟶ Y
inst✝ : AlgebraicGeometry.IsOpenImmersion f
⊢ (toScheme Y f.toPshHom).toLocallyRingedSpace = X.toLocallyRingedSpace

Tactic:
exact locallyRingedSpace_toLocallyRingedSpace f.toLRSHom

Result:
no goals
-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem tsupport_subset_symm_image_closedBall :
    tsupport f ⊆ (extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I)

Proof state:
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
⊢ closure (↑(extChartAt I c).symm '' (ball (↑(extChartAt I c) c) f.rOut ∩ range ↑I)) ⊆
    ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)

Tactic:
exact closure_minimal (image_subset _ <| inter_subset_inter_left _ ball_subset_closedBall)
  f.isClosed_symm_image_closedBall

Result:
no goals

Proof state:
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
⊢ tsupport ↑f ⊆ ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)

Tactic:
rw [tsupport, support_eq_symm_image]

Result:
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
⊢ closure (↑(extChartAt I c).symm '' (ball (↑(extChartAt I c) c) f.rOut ∩ range ↑I)) ⊆
    ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem takeD_succ (l) (a : α) :
    takeD (n+1) l a = l.head?.getD a :: takeD n l.tail a

Proof state:
α : Type u_1
n : Nat
l : List α
a : α
⊢ takeD (n + 1) l a = l.head?.getD a :: takeD n l.tail a

Tactic:
simp [takeD]

Result:
no goals
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem projIci_coe (x : Ici a) : projIci a x = x

Proof state:
case mk
α : Type u_1
inst✝ : LinearOrder α
a val✝ : α
property✝ : val✝ ∈ Ici a
⊢ projIci a ↑⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Tactic:
apply projIci_of_mem

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a : α
x : ↑(Ici a)
⊢ projIci a ↑x = x

Tactic:
cases x

Result:
case mk
α : Type u_1
inst✝ : LinearOrder α
a val✝ : α
property✝ : val✝ ∈ Ici a
⊢ projIci a ↑⟨val✝, property✝⟩ = ⟨val✝, property✝⟩
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivAt.mul (hc : HasDerivAt c c' x) (hd : HasDerivAt d d' x) :
    HasDerivAt (fun y => c y * d y) (c' * d x + c x * d') x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (fun y => c y * d y) (c' * d x + c x * d') univ x

Tactic:
exact hc.mul hd

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasDerivAt c c' x
hd : HasDerivAt d d' x
⊢ HasDerivAt (fun y => c y * d y) (c' * d x + c x * d') x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (fun y => c y * d y) (c' * d x + c x * d') univ x
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
lemma rightHomology_ext_iff {A : C} (f₁ f₂ : A ⟶ S.rightHomology) :
    f₁ = f₂ ↔ f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
A : C
f₁ f₂ : A ⟶ S.rightHomology
⊢ f₁ = f₂ ↔ f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι

Tactic:
rw [cancel_mono]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
@[simp] protected lemma inv_eq_one : a⁻¹ = 1 ↔ a = 1

Proof state:
a : ℝ≥0∞
⊢ a⁻¹ = 1 ↔ a = 1

Tactic:
rw [← inv_inj, inv_inv, inv_one]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem repr_zero_mem_span (h : IsAdjoinRoot S f) : h.repr 0 ∈ Ideal.span ({f} : Set R[X])

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRoot S f
⊢ h.repr 0 ∈ Ideal.span {f}

Tactic:
rw [← h.ker_map, RingHom.mem_ker, h.map_repr]

Result:
no goals