harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_replace {l : List α} : (l.replace a b).length = l.length

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
a b x : α
l : List α
ih : (l.replace a b).length = l.length
⊢ ((x :: l).replace a b).length = (x :: l).length

Tactic:
simp only [replace_cons]

Result:
case cons
α : Type u_1
inst✝ : BEq α
a b x : α
l : List α
ih : (l.replace a b).length = l.length
⊢ (match a == x with
      | true => b :: l
      | false => x :: l.replace a b).length =
    (x :: l).length

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
a b x : α
l : List α
ih : (l.replace a b).length = l.length
⊢ (match a == x with
      | true => b :: l
      | false => x :: l.replace a b).length =
    (x :: l).length

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
l : List α
⊢ (l.replace a b).length = l.length

Tactic:
induction l with
| nil => simp
| cons x l ih =>
  simp only [replace_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : BEq α
a b : α
⊢ ([].replace a b).length = [].length

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/WithLp.lean
theorem hasFDerivWithinAt_piLp :
    HasFDerivWithinAt f f' t y ↔
      ∀ i, HasFDerivWithinAt (fun x => f x i) (PiLp.proj _ _ i ∘L f') t y

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
t : Set H
y : H
⊢ HasFDerivWithinAt f f' t y ↔ ∀ (i : ι), HasFDerivWithinAt (fun x => f x i) ((PiLp.proj p E i).comp f') t y

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_hasFDerivWithinAt_iff, hasFDerivWithinAt_pi']

Result:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
t : Set H
y : H
⊢ (∀ (i : ι),
      HasFDerivWithinAt (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i)
        ((proj i).comp ((↑(PiLp.continuousLinearEquiv p 𝕜 E)).comp f')) t y) ↔
    ∀ (i : ι), HasFDerivWithinAt (fun x => f x i) ((PiLp.proj p E i).comp f') t y

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
t : Set H
y : H
⊢ (∀ (i : ι),
      HasFDerivWithinAt (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i)
        ((proj i).comp ((↑(PiLp.continuousLinearEquiv p 𝕜 E)).comp f')) t y) ↔
    ∀ (i : ι), HasFDerivWithinAt (fun x => f x i) ((PiLp.proj p E i).comp f') t y

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
@[reassoc]
lemma uncurry_pre_app (f : Y ⟶ A ⟶[C] X) (g : B ⟶ A) :
    uncurry (f ≫ (pre g).app X) = g ▷ _ ≫ uncurry f :=
  curry_injective (by
    rw [curry_uncurry, ← curry_pre_app, curry_uncurry])

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X Y : C
inst✝¹ : Closed A
inst✝ : Closed B
f : Y ⟶ (ihom A).obj X
g : B ⟶ A
⊢ curry (uncurry (f ≫ (pre g).app X)) = curry (g ▷ Y ≫ uncurry f)

Tactic:
rw [curry_uncurry, ← curry_pre_app, curry_uncurry]

Result:
no goals
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem ramificationIdx_of_not_le (h : ¬map f p ≤ P) : ramificationIdx f p P = 0 :=
  ramificationIdx_spec (by simp) (by simpa using h)

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
h : ¬map f p ≤ P
⊢ map f p ≤ P ^ 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
h : ¬map f p ≤ P
⊢ ¬map f p ≤ P ^ (0 + 1)

Tactic:
simpa using h

Result:
no goals
-- Mathlib/RingTheory/Artinian/Module.lean
lemma eventually_iInf_range_pow_eq (f : Module.End R M) :
    ∀ᶠ n in atTop, ⨅ m, LinearMap.range (f ^ m) = LinearMap.range (f ^ n)

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
l : ℕ
hl : l ≥ n
m : ℕ
⊢ range (f ^ l) ≤ range (f ^ m)

Tactic:
rcases le_or_lt l m with h | h

Result:
case intro.inl
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
l : ℕ
hl : l ≥ n
m : ℕ
h : l ≤ m
⊢ range (f ^ l) ≤ range (f ^ m)

case intro.inr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
l : ℕ
hl : l ≥ n
m : ℕ
h : m < l
⊢ range (f ^ l) ≤ range (f ^ m)

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
⊢ ∀ᶠ (n : ℕ) in atTop, ⨅ m, range (f ^ m) = range (f ^ n)

Tactic:
refine eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩

Result:
case intro
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
l : ℕ
hl : l ≥ n
m : ℕ
⊢ range (f ^ l) ≤ range (f ^ m)

Proof state:
case intro.inr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
l : ℕ
hl : l ≥ n
m : ℕ
h : m < l
⊢ range (f ^ l) ≤ range (f ^ m)

Tactic:
exact f.iterateRange.monotone h.le

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
⊢ ∀ᶠ (n : ℕ) in atTop, ⨅ m, range (f ^ m) = range (f ^ n)

Tactic:
obtain ⟨n, hn : ∀ m, n ≤ m → LinearMap.range (f ^ n) = LinearMap.range (f ^ m)⟩ :=
  IsArtinian.monotone_stabilizes f.iterateRange

Result:
case intro
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
⊢ ∀ᶠ (n : ℕ) in atTop, ⨅ m, range (f ^ m) = range (f ^ n)

Proof state:
case intro.inl
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
l : ℕ
hl : l ≥ n
m : ℕ
h : l ≤ m
⊢ range (f ^ l) ≤ range (f ^ m)

Tactic:
rw [← hn _ (hl.trans h), hn _ hl]

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem contDiffOn_of_differentiableOn_deriv {n : ℕ∞}
    (h : ∀ m : ℕ, (m : ℕ∞) ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) :
    ContDiffOn 𝕜 n f s

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞
h : ∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
⊢ ContDiffOn 𝕜 (↑n) f s

Tactic:
apply contDiffOn_of_differentiableOn

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞
h : ∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
⊢ ∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞
h : ∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
⊢ ∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s

Tactic:
simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableOn_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_int : (Int.fract : ℤ → ℤ) = 0 :=
  funext fun x => by simp [fract]

Proof state:
x : ℤ
⊢ fract x = 0 x

Tactic:
simp [fract]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Holder.lean
theorem uniformContinuousOn (hf : HolderOnWith C r f s) (h0 : 0 < r) :
    UniformContinuousOn f s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
⊢ ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε

Tactic:
rcases ENNReal.nhds_zero_basis.mem_iff.1 (this (gt_mem_nhds εpos)) with ⟨δ, δ0, H⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : Iio δ ⊆ (fun d => ↑C * d ^ ↑r) ⁻¹' {x | (fun x => x < ε) x}
⊢ ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
⊢ UniformContinuousOn f s

Tactic:
refine EMetric.uniformContinuousOn_iff.2 fun ε εpos => ?_

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε

Tactic:
have : Tendsto (fun d : ℝ≥0∞ => (C : ℝ≥0∞) * d ^ (r : ℝ)) (𝓝 0) (𝓝 0) :=
  ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos ENNReal.coe_ne_top h0

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
⊢ ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : Iio δ ⊆ (fun d => ↑C * d ^ ↑r) ⁻¹' {x | (fun x => x < ε) x}
⊢ ∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε

Tactic:
exact ⟨δ, δ0, fun hx y hy h => (hf.edist_le hx hy).trans_lt (H h)⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem Fin.circulant_mul [Semiring α] :
    ∀ {n} (v w : Fin n → α), circulant v * circulant w = circulant (circulant v *ᵥ w)
  | 0 => by simp [Injective, eq_iff_true_of_subsingleton]
  | _ + 1 => Matrix.circulant_mul

Proof state:
α : Type u_1
inst✝ : Semiring α
⊢ ∀ (v w : Fin 0 → α), circulant v * circulant w = circulant (circulant v *ᵥ w)

Tactic:
simp [Injective, eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem Icc_add_Icc (f : α → E) {s : Set α} {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) (hb : b ∈ s) :
    eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hb : b ∈ s
⊢ eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)

Tactic:
have A : IsGreatest (s ∩ Icc a b) b :=
  ⟨⟨hb, hab, le_rfl⟩, inter_subset_right.trans Icc_subset_Iic_self⟩

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hb : b ∈ s
A : IsGreatest (s ∩ Icc a b) b
⊢ eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hb : b ∈ s
A : IsGreatest (s ∩ Icc a b) b
B : IsLeast (s ∩ Icc b c) b
⊢ eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)

Tactic:
rw [← eVariationOn.union f A B, ← inter_union_distrib_left, Icc_union_Icc_eq_Icc hab hbc]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hb : b ∈ s
A : IsGreatest (s ∩ Icc a b) b
⊢ eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)

Tactic:
have B : IsLeast (s ∩ Icc b c) b :=
  ⟨⟨hb, le_rfl, hbc⟩, inter_subset_right.trans Icc_subset_Ici_self⟩

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hb : b ∈ s
A : IsGreatest (s ∩ Icc a b) b
B : IsLeast (s ∩ Icc b c) b
⊢ eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)
-- Mathlib/Algebra/Group/Prod.lean
theorem coprod_comp_inl : (f.coprod g).comp (inl M N) = f :=
  ext fun x => by simp [coprod_apply]

Proof state:
M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f : M →* P
g : N →* P
x : M
⊢ ((f.coprod g).comp (inl M N)) x = f x

Tactic:
simp [coprod_apply]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem comap_comm (H : ψ ∘ φ = ρ ∘ θ) (G : Filter δ) :
    comap φ (comap ψ G) = comap θ (comap ρ G)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
G : Filter δ
⊢ comap φ (comap ψ G) = comap θ (comap ρ G)

Tactic:
rw [Filter.comap_comap, H, ← Filter.comap_comap]

Result:
no goals
-- Mathlib/GroupTheory/Perm/ClosureSwap.lean
theorem SubmonoidClass.swap_mem_trans {a b c : α} {C} [SetLike C (Perm α)]
    [SubmonoidClass C (Perm α)] (M : C) (hab : swap a b ∈ M) (hbc : swap b c ∈ M) :
    swap a c ∈ M

Proof state:
case inr.inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
hab' : a ≠ b
hac : a ≠ c
⊢ swap a c ∈ M

Tactic:
rw [swap_comm, ← swap_mul_swap_mul_swap hab' hac]

Result:
case inr.inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
hab' : a ≠ b
hac : a ≠ c
⊢ swap b c * swap a b * swap b c ∈ M

Proof state:
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
⊢ swap a c ∈ M

Tactic:
obtain rfl | hab' := eq_or_ne a b

Result:
case inl
α : Type u_2
inst✝² : DecidableEq α
a c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a a ∈ M
hbc : swap a c ∈ M
⊢ swap a c ∈ M

case inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
hab' : a ≠ b
⊢ swap a c ∈ M

Proof state:
case inl
α : Type u_2
inst✝² : DecidableEq α
a c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a a ∈ M
hbc : swap a c ∈ M
⊢ swap a c ∈ M

Tactic:
exact hbc

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
hab' : a ≠ b
⊢ swap a c ∈ M

Tactic:
obtain rfl | hac := eq_or_ne a c

Result:
case inr.inl
α : Type u_2
inst✝² : DecidableEq α
a b : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hab' : a ≠ b
hbc : swap b a ∈ M
⊢ swap a a ∈ M

case inr.inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
hab' : a ≠ b
hac : a ≠ c
⊢ swap a c ∈ M

Proof state:
case inr.inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
hab' : a ≠ b
hac : a ≠ c
⊢ swap b c * swap a b * swap b c ∈ M

Tactic:
exact mul_mem (mul_mem hbc hab) hbc

Result:
no goals

Proof state:
case inr.inl
α : Type u_2
inst✝² : DecidableEq α
a b : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hab' : a ≠ b
hbc : swap b a ∈ M
⊢ swap a a ∈ M

Tactic:
exact swap_self a ▸ one_mem M

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma natDegree_preΨ₄_pos (h : (2 : R) ≠ 0) : 0 < W.preΨ₄.natDegree

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 2 ≠ 0
⊢ 0 < W.preΨ₄.natDegree

Tactic:
linarith only [W.natDegree_preΨ₄ h]

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonUnitalNonAssocSemiring_injective :
    Function.Injective (@toNonUnitalNonAssocSemiring R)

Proof state:
case mk.mk
R : Type u
toNonUnitalNonAssocSemiring✝¹ : NonUnitalNonAssocSemiring R
mul_assoc✝¹ : ∀ (a b c : R), a * b * c = a * (b * c)
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
mul_assoc✝ : ∀ (a b c : R), a * b * c = a * (b * c)
a✝ : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
⊢ mk mul_assoc✝¹ = mk mul_assoc✝

Tactic:
congr

Result:
no goals

Proof state:
R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocSemiring R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Result:
case mk.mk
R : Type u
toNonUnitalNonAssocSemiring✝¹ : NonUnitalNonAssocSemiring R
mul_assoc✝¹ : ∀ (a b c : R), a * b * c = a * (b * c)
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
mul_assoc✝ : ∀ (a b c : R), a * b * c = a * (b * c)
a✝ : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
⊢ mk mul_assoc✝¹ = mk mul_assoc✝
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem ennrealToMeasure_apply {m : MeasurableSpace α} {v : VectorMeasure α ℝ≥0∞} {s : Set α}
    (hs : MeasurableSet s) : ennrealToMeasure v s = v s

Proof state:
α : Type u_1
m : MeasurableSpace α
v : VectorMeasure α ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ v.ennrealToMeasure s = ↑v s

Tactic:
rw [ennrealToMeasure, ofMeasurable_apply _ hs]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem mem_one' {x : A} : x ∈ (1 : SubMulAction R A) ↔ ∃ y, algebraMap R A y = x :=
  exists_congr fun r => by rw [algebraMap_eq_smul_one]

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
⊢ (fun r => r • 1) r = x ↔ (algebraMap R A) r = x

Tactic:
rw [algebraMap_eq_smul_one]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
lemma ciSup_neg {p : Prop} {f : p → α} (hp : ¬ p) :
    ⨆ (h : p), f h = sSup (∅ : Set α)

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : p → α
hp : ¬p
⊢ sSup (range fun h => f h) = sSup ∅

Tactic:
congr

Result:
case e_a
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : p → α
hp : ¬p
⊢ (range fun h => f h) = ∅

Proof state:
case e_a
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : p → α
hp : ¬p
⊢ (range fun h => f h) = ∅

Tactic:
rwa [range_eq_empty_iff, isEmpty_Prop]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : p → α
hp : ¬p
⊢ ⨆ (h : p), f h = sSup ∅

Tactic:
rw [iSup]

Result:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : p → α
hp : ¬p
⊢ sSup (range fun h => f h) = sSup ∅
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
lemma le_nnreal_iff [Algebra ℝ A] {a : A}
    (ha : SpectrumRestricts a ContinuousMap.realToNNReal) {r : ℝ≥0} :
    (∀ x ∈ spectrum ℝ≥0 a, x ≤ r) ↔ ∀ x ∈ spectrum ℝ a, x ≤ r

Proof state:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
r : ℝ≥0
⊢ (∀ x ∈ spectrum ℝ≥0 a, x ≤ r) ↔ ∀ x ∈ spectrum ℝ a, x ≤ ↑r

Tactic:
simp [← ha.algebraMap_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem dropLast_eq_take (l : List α) : l.dropLast = l.take (l.length - 1)

Proof state:
α : Type u_1
l : List α
⊢ l.dropLast = take (l.length - 1) l

Tactic:
cases l with
| nil => simp [dropLast]
| cons x l =>
  induction l generalizing x <;> simp_all [dropLast]

Result:
no goals

Proof state:
case cons
α : Type u_1
x : α
l : List α
⊢ (x :: l).dropLast = take ((x :: l).length - 1) (x :: l)

Tactic:
induction l generalizing x <;> simp_all [dropLast]

Result:
no goals

Proof state:
case nil
α : Type u_1
⊢ [].dropLast = take ([].length - 1) []

Tactic:
simp [dropLast]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem antilipschitzWith_lineMap {p₁ p₂ : Q} (h : p₁ ≠ p₂) :
    AntilipschitzWith (nndist p₁ p₂)⁻¹ (lineMap p₁ p₂ : 𝕜 → Q) :=
  AntilipschitzWith.of_le_mul_dist fun c₁ c₂ => by
    rw [dist_lineMap_lineMap, NNReal.coe_inv, ← dist_nndist, mul_left_comm,
      inv_mul_cancel₀ (dist_ne_zero.2 h), mul_one]

Proof state:
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : Q
h : p₁ ≠ p₂
c₁ c₂ : 𝕜
⊢ dist c₁ c₂ ≤ ↑(nndist p₁ p₂)⁻¹ * dist ((lineMap p₁ p₂) c₁) ((lineMap p₁ p₂) c₂)

Tactic:
rw [dist_lineMap_lineMap, NNReal.coe_inv, ← dist_nndist, mul_left_comm,
  inv_mul_cancel₀ (dist_ne_zero.2 h), mul_one]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Ab.lean
@[simp]
lemma ab_zero_apply (x : S.X₁) : S.g (S.f x) = 0

Proof state:
S : ShortComplex Ab
x : ↑S.X₁
⊢ (ConcreteCategory.hom S.g) ((ConcreteCategory.hom S.f) x) = 0

Tactic:
rw [← ConcreteCategory.comp_apply, S.zero]

Result:
S : ShortComplex Ab
x : ↑S.X₁
⊢ (ConcreteCategory.hom 0) x = 0

Proof state:
S : ShortComplex Ab
x : ↑S.X₁
⊢ (ConcreteCategory.hom 0) x = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem support_transfer (hp) : (p.transfer H hp).support = p.support

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ (p.transfer H hp).support = p.support

Tactic:
induction p <;> simp [*]

Result:
no goals