harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem dist_one_right (a : E) : dist a 1 = ‖a‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ dist a 1 = ‖a‖

Tactic:
rw [dist_eq_norm_div, div_one]

Result:
no goals
-- Mathlib/Data/Multiset/NatAntidiagonal.lean
theorem antidiagonal_succ' {n : ℕ} :
    antidiagonal (n + 1) = (n + 1, 0) ::ₘ (antidiagonal n).map (Prod.map id Nat.succ)

Proof state:
n : ℕ
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)

Tactic:
rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
  map_coe, coe_add, List.singleton_append, cons_coe]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₆_of_isCharThreeJNeZeroNF_of_char_three : W.b₆ = W.a₆

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ W.b₆ = W.a₆

Tactic:
rw [b₆_of_isCharThreeJNeZeroNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ 4 * W.a₆ = W.a₆

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ 4 * W.a₆ = W.a₆

Tactic:
linear_combination W.a₆ * CharP.cast_eq_zero R 3

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FintypeCat.lean
@[simp]
lemma productEquiv_apply {ι : Type*} [Finite ι] (X : ι → FintypeCat.{u})
    (x : (∏ᶜ X : FintypeCat)) (i : ι) : productEquiv X x i = Pi.π X i x

Proof state:
ι : Type u_1
inst✝ : Finite ι
X : ι → FintypeCat
x : (∏ᶜ X).carrier
i : ι
⊢ (productEquiv X) x i = Pi.π X i x

Tactic:
simpa [productEquiv] using (elementwise_of% piComparison_comp_π FintypeCat.incl X i) x

Result:
no goals
-- Mathlib/Topology/SeparatedMap.lean
theorem IsSeparatedMap.isClosed_eqLocus (sep : IsSeparatedMap f) (he : f ∘ g₁ = f ∘ g₂) :
    IsClosed {a | g₁ a = g₂ a} :=
  let g : A → f.Pullback f := fun a ↦ ⟨⟨g₁ a, g₂ a⟩, congr_fun he a⟩
  (isSeparatedMap_iff_isClosed_diagonal.mp sep).preimage (by fun_prop : Continuous g)

Proof state:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
g₁ g₂ : A → X
h₁ : Continuous g₁
h₂ : Continuous g₂
sep : IsSeparatedMap f
he : f ∘ g₁ = f ∘ g₂
g : A → Function.Pullback f f := fun a => ⟨(g₁ a, g₂ a), ⋯⟩
⊢ Continuous g

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc]
lemma d_fst_v (i j k : ℤ) (hij : i + 1 = j) (hjk : j + 1 = k) :
    (mappingCone φ).d i j ≫ (fst φ).1.v j k hjk =
      -(fst φ).1.v i j hij ≫ F.d j k

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j k : ℤ
hij : i + 1 = j
hjk : j + 1 = k
⊢ (mappingCone φ).d i j ≫ (↑(fst φ)).v j k hjk = -(↑(fst φ)).v i j hij ≫ F.d j k

Tactic:
apply homotopyCofiber.d_fstX

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Semiconj.lean
theorem zero_left [MulZeroClass G₀] (x y : G₀) : SemiconjBy 0 x y

Proof state:
G₀ : Type u_1
inst✝ : MulZeroClass G₀
x y : G₀
⊢ SemiconjBy 0 x y

Tactic:
simp only [SemiconjBy, mul_zero, zero_mul]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem le_einfsep_image_iff {d} {f : β → α} {s : Set β} : d ≤ einfsep (f '' s)
    ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : EDist α
d : ℝ≥0∞
f : β → α
s : Set β
⊢ d ≤ (f '' s).einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)

Tactic:
simp_rw [le_einfsep_iff, forall_mem_image]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem differentiableAt_comp_add_left (a : E) :
    DifferentiableAt 𝕜 (fun x ↦ f (a + x)) x ↔ DifferentiableAt 𝕜 f (a + x)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x a : E
⊢ DifferentiableAt 𝕜 (fun x => f (a + x)) x ↔ DifferentiableAt 𝕜 f (a + x)

Tactic:
simp [DifferentiableAt, hasFDerivAt_comp_add_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_reverse (l : List α) : countP p l.reverse = countP p l

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ countP p l.reverse = countP p l

Tactic:
simp [countP_eq_length_filter, filter_reverse]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.le_eq_false_of_lo (u v k : Nat) : isLt 0 k = true → u + k ≤ v → (v ≤ u) = False

Proof state:
u v k : Nat
⊢ 0 < k → u + k ≤ v → u < v

Tactic:
omega

Result:
no goals

Proof state:
u v k : Nat
⊢ isLt 0 k = true → u + k ≤ v → (v ≤ u) = False

Tactic:
simp [isLt]

Result:
u v k : Nat
⊢ 0 < k → u + k ≤ v → u < v
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem nextCoeff_pow (hp : p.Monic) (n : ℕ) : (p ^ n).nextCoeff = n • p.nextCoeff

Proof state:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ (p ^ 0).nextCoeff = 0 • p.nextCoeff

Tactic:
rw [pow_zero, zero_smul, ← map_one (f := C), nextCoeff_C_eq_zero]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
ih : (p ^ n).nextCoeff = n • p.nextCoeff
⊢ (p ^ (n + 1)).nextCoeff = (n + 1) • p.nextCoeff

Tactic:
rw [pow_succ, (hp.pow n).nextCoeff_mul hp, ih, succ_nsmul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ n).nextCoeff = n • p.nextCoeff

Tactic:
induction n with
| zero => rw [pow_zero, zero_smul, ← map_one (f := C), nextCoeff_C_eq_zero]
| succ n ih => rw [pow_succ, (hp.pow n).nextCoeff_mul hp, ih, succ_nsmul]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_iUnion_of_directed {ι : Type*} [Countable ι]
    (f : α → ℝ≥0∞) {s : ι → Set α} (hd : Directed (· ⊆ ·) s) :
    ∫⁻ x in ⋃ i, s i, f x ∂μ = ⨆ i, ∫⁻ x in s i, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst✝ : Countable ι
f : α → ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
⊢ ∫⁻ (x : α) in ⋃ i, s i, f x ∂μ = ⨆ i, ∫⁻ (x : α) in s i, f x ∂μ

Tactic:
simp only [lintegral_def, iSup_comm (ι := ι),
  SimpleFunc.lintegral_restrict_iUnion_of_directed _ hd]

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem insert_insert_of_ne {a a'} {b : β a} {b' : β a'} (s : AList β) (h : a ≠ a') :
    ((s.insert a b).insert a' b').entries ~ ((s.insert a' b').insert a b).entries

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ ⟨a', b'⟩ :: kerase a' (⟨a, b⟩ :: kerase a s.entries) ~ ⟨a, b⟩ :: kerase a (⟨a', b'⟩ :: kerase a' s.entries)

Tactic:
rw [kerase_cons_ne, kerase_cons_ne, kerase_comm] <;>
[apply Perm.swap; exact h; exact h.symm]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ (insert a' b' (insert a b s)).entries ~ (insert a b (insert a' b' s)).entries

Tactic:
simp only [entries_insert]

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ ⟨a', b'⟩ :: kerase a' (⟨a, b⟩ :: kerase a s.entries) ~ ⟨a, b⟩ :: kerase a (⟨a', b'⟩ :: kerase a' s.entries)
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem ker_mkQ : ker p.mkQ = p

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x✝ : M
⊢ x✝ ∈ ker p.mkQ ↔ x✝ ∈ p

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ ker p.mkQ = p

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x✝ : M
⊢ x✝ ∈ ker p.mkQ ↔ x✝ ∈ p
-- Mathlib/LinearAlgebra/Matrix/Diagonal.lean
theorem range_diagonal [DecidableEq m] (w : m → K) :
    LinearMap.range (toLin' (diagonal w)) =
      ⨆ i ∈ { i | w i ≠ 0 }, LinearMap.range (LinearMap.single K (fun _ => K) i)

Proof state:
case e_s.h
m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
i : m
⊢ Submodule.map (toLin' (diagonal w)) (LinearMap.range (single K (fun a => K) i)) =
    ⨆ (_ : w i ≠ 0), LinearMap.range (single K (fun x => K) i)

Tactic:
rw [← LinearMap.range_comp, diagonal_comp_single, ← range_smul']

Result:
no goals

Proof state:
m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ ⨆ i, Submodule.map (toLin' (diagonal w)) (LinearMap.range (single K (fun a => K) i)) =
    ⨆ i, ⨆ (_ : w i ≠ 0), LinearMap.range (single K (fun x => K) i)

Tactic:
congr

Result:
case e_s
m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ (fun i => Submodule.map (toLin' (diagonal w)) (LinearMap.range (single K (fun a => K) i))) = fun i =>
    ⨆ (_ : w i ≠ 0), LinearMap.range (single K (fun x => K) i)

Proof state:
case e_s
m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ (fun i => Submodule.map (toLin' (diagonal w)) (LinearMap.range (single K (fun a => K) i))) = fun i =>
    ⨆ (_ : w i ≠ 0), LinearMap.range (single K (fun x => K) i)

Tactic:
funext i

Result:
case e_s.h
m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
i : m
⊢ Submodule.map (toLin' (diagonal w)) (LinearMap.range (single K (fun a => K) i)) =
    ⨆ (_ : w i ≠ 0), LinearMap.range (single K (fun x => K) i)

Proof state:
m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ LinearMap.range (toLin' (diagonal w)) = ⨆ i, ⨆ (_ : w i ≠ 0), LinearMap.range (single K (fun x => K) i)

Tactic:
rw [← Submodule.map_top, ← iSup_range_single, Submodule.map_iSup]

Result:
m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ ⨆ i, Submodule.map (toLin' (diagonal w)) (LinearMap.range (single K (fun a => K) i)) =
    ⨆ i, ⨆ (_ : w i ≠ 0), LinearMap.range (single K (fun x => K) i)

Proof state:
m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ LinearMap.range (toLin' (diagonal w)) = ⨆ i ∈ {i | w i ≠ 0}, LinearMap.range (single K (fun x => K) i)

Tactic:
dsimp only [mem_setOf_eq]

Result:
m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ LinearMap.range (toLin' (diagonal w)) = ⨆ i, ⨆ (_ : w i ≠ 0), LinearMap.range (single K (fun x => K) i)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_zsmul_neg_pi_div_two : (2 : ℤ) • (↑(-π / 2) : Angle) = π

Proof state:
⊢ 2 • ↑(-π / 2) = ↑π

Tactic:
rw [two_zsmul, ← two_nsmul, two_nsmul_neg_pi_div_two]

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem map_natDegree_eq_sub {S F : Type*} [Semiring S]
    [FunLike F R[X] S[X]] [AddMonoidHomClass F R[X] S[X]] {φ : F}
    {p : R[X]} {k : ℕ} (φ_k : ∀ f : R[X], f.natDegree < k → φ f = 0)
    (φ_mon : ∀ n c, c ≠ 0 → (φ (monomial n c)).natDegree = n - k) :
    (φ p).natDegree = p.natDegree - k :=
  mono_map_natDegree_eq k (fun j => j - k) (by simp_all)
    (@fun _ _ h => (tsub_lt_tsub_iff_right h).mpr)
    (φ_k _) φ_mon

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
φ_k : ∀ (f : R[X]), f.natDegree < k → φ f = 0
φ_mon : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = n - k
⊢ ∀ {n : ℕ}, n ≤ k → (fun j => j - k) n = 0

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.add_right_inj' (a b c : BitVec w) : (c + a == b + c) = (a == b)

Proof state:
w : Nat
a b c : BitVec w
⊢ (c + a == b + c) = (a == b)

Tactic:
rw [BitVec.add_comm b c, add_right_inj]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem preimage_coe_eq_preimage_coe_iff {s t u : Set α} :
    ((↑) : s → α) ⁻¹' t = ((↑) : s → α) ⁻¹' u ↔ s ∩ t = s ∩ u

Proof state:
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t = val ⁻¹' u ↔ s ∩ t = s ∩ u

Tactic:
rw [← image_preimage_coe, ← image_preimage_coe, coe_injective.image_injective.eq_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem tendsto_testAgainstNN_filter_of_le_const {ι : Type*} {L : Filter ι}
    [L.IsCountablyGenerated] {μ : FiniteMeasure Ω} {fs : ι → Ω →ᵇ ℝ≥0} {c : ℝ≥0}
    (fs_le_const : ∀ᶠ i in L, ∀ᵐ ω : Ω ∂(μ : Measure Ω), fs i ω ≤ c) {f : Ω →ᵇ ℝ≥0}
    (fs_lim : ∀ᵐ ω : Ω ∂(μ : Measure Ω), Tendsto (fun i ↦ fs i ω) L (𝓝 (f ω))) :
    Tendsto (fun i ↦ μ.testAgainstNN (fs i)) L (𝓝 (μ.testAgainstNN f))

Proof state:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
μ : FiniteMeasure Ω
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂↑μ, (fs i) ω ≤ c
f : Ω →ᵇ ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂↑μ, Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))
⊢ Tendsto (fun i => μ.testAgainstNN (fs i)) L (𝓝 (μ.testAgainstNN f))

Tactic:
apply (ENNReal.tendsto_toNNReal (f.lintegral_lt_top_of_nnreal (μ : Measure Ω)).ne).comp

Result:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
μ : FiniteMeasure Ω
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂↑μ, (fs i) ω ≤ c
f : Ω →ᵇ ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂↑μ, Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))
⊢ Tendsto (fun i => ∫⁻ (ω : Ω), ↑((fs i) ω) ∂↑μ) L (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))

Proof state:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
μ : FiniteMeasure Ω
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂↑μ, (fs i) ω ≤ c
f : Ω →ᵇ ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂↑μ, Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))
⊢ Tendsto (fun i => ∫⁻ (ω : Ω), ↑((fs i) ω) ∂↑μ) L (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))

Tactic:
exact tendsto_lintegral_nn_filter_of_le_const (Ω := Ω) μ fs_le_const fs_lim

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive (attr := simp)] lemma leOnePart_one : (1 : α)⁻ᵐ = 1

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
⊢ 1⁻ᵐ = 1

Tactic:
simp [leOnePart]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem Equiv.Perm.decomposeFin_symm_of_refl {n : ℕ} (p : Fin (n + 1)) :
    Equiv.Perm.decomposeFin.symm (p, Equiv.refl _) = swap 0 p

Proof state:
n : ℕ
p : Fin (n + 1)
⊢ decomposeFin.symm (p, Equiv.refl (Fin n)) = swap 0 p

Tactic:
simp [Equiv.Perm.decomposeFin, Equiv.permCongr_def]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc (attr := simp)]
lemma whiskerRight_ε_η (T : D) : ε F ▷ T ≫ η F ▷ T = 𝟙 _

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ ε F ▷ T ≫ η F ▷ T = 𝟙 (𝟙_ D ⊗ T)

Tactic:
rw [← MonoidalCategory.comp_whiskerRight, ε_η, id_whiskerRight]

Result:
no goals
-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem ruzsa_triangle_inequality_mulInv_mulInv_mulInv (A B C : Finset G) :
    #(A * C⁻¹) * #B ≤ #(A * B⁻¹) * #(C * B⁻¹)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A * B⁻¹) * #(C * B⁻¹)

Tactic:
simpa [div_eq_mul_inv] using ruzsa_triangle_inequality_div_div_div A B C

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem mem_diff_of_mem {a : α} : ∀ {l₁ l₂ : List α}, a ∈ l₁ → a ∉ l₂ → a ∈ l₁.diff l₂
  | _, [], h₁, _ => h₁
  | l₁, b :: l₂, h₁, h₂ => by
    rw [diff_cons]
    exact mem_diff_of_mem ((mem_erase_of_ne <| ne_of_not_mem_cons h₂).2 h₁) (mt (.tail _) h₂)

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
b : α
l₂ : List α
h₁ : a ∈ l₁
h₂ : ¬a ∈ b :: l₂
⊢ a ∈ (l₁.erase b).diff l₂

Tactic:
exact mem_diff_of_mem ((mem_erase_of_ne <| ne_of_not_mem_cons h₂).2 h₁) (mt (.tail _) h₂)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
b : α
l₂ : List α
h₁ : a ∈ l₁
h₂ : ¬a ∈ b :: l₂
⊢ a ∈ l₁.diff (b :: l₂)

Tactic:
rw [diff_cons]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
b : α
l₂ : List α
h₁ : a ∈ l₁
h₂ : ¬a ∈ b :: l₂
⊢ a ∈ (l₁.erase b).diff l₂
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem linearDisjoint_iff_injective : A.LinearDisjoint B ↔ Function.Injective (A.mulMap B)

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ A.LinearDisjoint B ↔ Function.Injective ⇑(A.mulMap B)

Tactic:
rw [linearDisjoint_iff, Submodule.linearDisjoint_iff]

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ Function.Injective ⇑((toSubmodule A).mulMap (toSubmodule B)) ↔ Function.Injective ⇑(A.mulMap B)

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ Function.Injective ⇑((toSubmodule A).mulMap (toSubmodule B)) ↔ Function.Injective ⇑(A.mulMap B)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem Cauchy.coeff_tendsto {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) (D : ℤ) :
    Tendsto (fun f : K⸨X⸩ ↦ f.coeff D) ℱ (𝓟 {coeff hℱ D}) :=
  let _ : UniformSpace K := ⊥
  le_of_eq <| UniformSpace.DiscreteUnif.eq_const_of_cauchy (by rfl)
    (hℱ.map (uniformContinuous_coeff D)) ▸ (principal_singleton _).symm

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
x✝ : UniformSpace K := ⊥
⊢ x✝ = ⊥

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem symmetrize_mem_uniformity {V : Set (α × α)} (h : V ∈ 𝓤 α) : symmetrizeRel V ∈ 𝓤 α

Proof state:
α : Type ua
inst✝ : UniformSpace α
V : Set (α × α)
h : V ∈ 𝓤 α
⊢ Prod.swap ⁻¹' V ∈ (𝓤 α).sets

Tactic:
rw [← image_swap_eq_preimage_swap, uniformity_eq_symm]

Result:
α : Type ua
inst✝ : UniformSpace α
V : Set (α × α)
h : V ∈ 𝓤 α
⊢ Prod.swap '' V ∈ (Prod.swap <$> 𝓤 α).sets

Proof state:
α : Type ua
inst✝ : UniformSpace α
V : Set (α × α)
h : V ∈ 𝓤 α
⊢ symmetrizeRel V ∈ 𝓤 α

Tactic:
apply (𝓤 α).inter_sets h

Result:
α : Type ua
inst✝ : UniformSpace α
V : Set (α × α)
h : V ∈ 𝓤 α
⊢ Prod.swap ⁻¹' V ∈ (𝓤 α).sets

Proof state:
α : Type ua
inst✝ : UniformSpace α
V : Set (α × α)
h : V ∈ 𝓤 α
⊢ Prod.swap '' V ∈ (Prod.swap <$> 𝓤 α).sets

Tactic:
exact image_mem_map h

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_sq_sub_sinh_sq : cosh x ^ 2 - sinh x ^ 2 = 1

Proof state:
x : ℂ
⊢ cosh x ^ 2 - sinh x ^ 2 = 1

Tactic:
rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_cancel, exp_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem mkPiRing_zero [Fintype ι] : MultilinearMap.mkPiRing R ι (0 : M₂) = 0

Proof state:
case H
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
x✝ : ι → R
⊢ (MultilinearMap.mkPiRing R ι 0) x✝ = 0 x✝

Tactic:
rw [mkPiRing_apply, smul_zero, MultilinearMap.zero_apply]

Result:
no goals

Proof state:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
⊢ MultilinearMap.mkPiRing R ι 0 = 0

Tactic:
ext

Result:
case H
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
x✝ : ι → R
⊢ (MultilinearMap.mkPiRing R ι 0) x✝ = 0 x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_filter {p : α → Bool} {l : Array α} {a : α} :
    a ∈ filter p l ↔ a ∈ l ∧ p a

Proof state:
α : Type u_1
p : α → Bool
l : Array α
a : α
⊢ a ∈ filter p l ↔ a ∈ l ∧ p a = true

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ a ∈ filter p { toList := l } ↔ a ∈ { toList := l } ∧ p a = true

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ a ∈ filter p { toList := l } ↔ a ∈ { toList := l } ∧ p a = true

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Multiset.lean
lemma prod_eq_zero (h : (0 : α) ∈ s) : s.prod = 0

Proof state:
α : Type u_2
inst✝ : CommMonoidWithZero α
s : Multiset α
h : 0 ∈ s
⊢ s.prod = 0

Tactic:
rcases Multiset.exists_cons_of_mem h with ⟨s', hs'⟩

Result:
case intro
α : Type u_2
inst✝ : CommMonoidWithZero α
s : Multiset α
h : 0 ∈ s
s' : Multiset α
hs' : s = 0 ::ₘ s'
⊢ s.prod = 0

Proof state:
case intro
α : Type u_2
inst✝ : CommMonoidWithZero α
s : Multiset α
h : 0 ∈ s
s' : Multiset α
hs' : s = 0 ::ₘ s'
⊢ s.prod = 0

Tactic:
simp [hs', Multiset.prod_cons]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem Fintype.not_linearIndependent_iffₛ [Fintype ι] :
    ¬LinearIndependent R v ↔ ∃ f g : ι → R, ∑ i, f i • v i = ∑ i, g i • v i ∧ ∃ i, f i ≠ g i

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
⊢ ¬LinearIndependent R v ↔ ∃ f g, ∑ i : ι, f i • v i = ∑ i : ι, g i • v i ∧ ∃ i, f i ≠ g i

Tactic:
simpa using not_iff_not.2 Fintype.linearIndependent_iffₛ

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem zpow_add_period_smul (i : ℤ) (g : G) (a : α) :
    g ^ (i + period g a) • a = g ^ i • a

Proof state:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
i : ℤ
g : G
a : α
⊢ g ^ (i + ↑(period g a)) • a = g ^ i • a

Tactic:
rw [← zpow_mod_period_smul, Int.add_emod_self, zpow_mod_period_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Pairwise.lean
theorem map_get_sublist {l : List α} {is : List (Fin l.length)} (h : is.Pairwise (·.val < ·.val)) :
    is.map (get l) <+ l

Proof state:
α : Type u_1
l : List α
is : List (Fin l.length)
h : Pairwise (fun x1 x2 => ↑x1 < ↑x2) is
⊢ map l.get is <+ l

Tactic:
simpa using map_getElem_sublist h

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem left_le_veblen (o a : Ordinal) : o ≤ veblen o a :=
  left_le_veblenWith (isNormal_opow one_lt_omega0) (by simp) o a

Proof state:
o a : Ordinal.{u_1}
⊢ 0 < ω ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem ωSup_total {c : Chain α} {x : α} (h : ∀ i, c i ≤ x ∨ x ≤ c i) : ωSup c ≤ x ∨ x ≤ ωSup c :=
  by_cases
    (fun (this : ∀ i, c i ≤ x) => Or.inl (ωSup_le _ _ this))
    (fun (this : ¬∀ i, c i ≤ x) =>
      have : ∃ i, ¬c i ≤ x

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ∀ (i : ℕ), c i ≤ x ∨ x ≤ c i
this : ∃ x_1, ¬c x_1 ≤ x
⊢ ∃ i, ¬c i ≤ x

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ∀ (i : ℕ), c i ≤ x ∨ x ≤ c i
this : ¬∀ (i : ℕ), c i ≤ x
⊢ ∃ i, ¬c i ≤ x

Tactic:
simp only [not_forall] at this ⊢

Result:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ∀ (i : ℕ), c i ≤ x ∨ x ≤ c i
this : ∃ x_1, ¬c x_1 ≤ x
⊢ ∃ i, ¬c i ≤ x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Basic.lean
theorem size_swap (a : Array α) (i j : Nat) {hi hj} : (a.swap i j hi hj).size = a.size

Proof state:
α : Type u
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ ((a.set i (getElem a j hj) hi).set j (getElem a i hi) ⋯).size = a.size

Tactic:
rw [size_set, size_set]

Result:
no goals

Proof state:
α : Type u
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ (a.swap i j hi hj).size = a.size

Tactic:
show ((a.set i a[j]).set j a[i]
  (Nat.lt_of_lt_of_eq hj (size_set a i a[j] _).symm)).size = a.size

Result:
α : Type u
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ ((a.set i (getElem a j hj) hi).set j (getElem a i hi) ⋯).size = a.size
-- Mathlib/Data/Real/Sqrt.lean
@[simp] lemma one_le_sqrt : 1 ≤ √x ↔ 1 ≤ x

Proof state:
x : ℝ
⊢ 1 ≤ √x ↔ 1 ≤ x

Tactic:
rw [← sqrt_one, sqrt_le_sqrt_iff' zero_lt_one, sqrt_one]

Result:
no goals