harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Additive/SmallTripling.lean
/-- If `A` is symmetric (`A⁻¹ = A`) and has small tripling, then `A` has small powers,
in the sense that `|A ^ m|` is at most `|A|` times a constant exponential in `m`.

See also `Finset.small_alternating_pow_of_small_tripling` for a version with a weaker constant but
which encompasses non-symmetric sets. -/
@[to_additive
"If `A` is symmetric (`-A = A`) and has small tripling, then `A` has small powers,
in the sense that `|m • A|` is at most `|A|` times a constant exponential in `m`.

See also `Finset.small_alternating_nsmul_of_small_tripling` for a version with a weaker constant but
which encompasses non-symmetric sets."]
lemma small_pow_of_small_tripling (hm : 3 ≤ m) (hA : #(A ^ 3) ≤ K * #A) (hAsymm : A⁻¹ = A) :
    #(A ^ m) ≤ K ^ (m - 2) * #A

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ), |ε| = 1 → A ^ ε = A
⊢ Fin m → |1| = 1

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ), |ε| = 1 → A ^ ε = A
⊢ ↑(#(A ^ m)) = ↑(#(List.map (fun i => A ^ 1) (finRange m)).prod)

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ), |ε| = 1 → A ^ ε = A
δ : Fin 3 → ℤ
hδ : ∀ (i : Fin 3), |δ i| = 1
⊢ ↑(#(List.map (fun i => A ^ δ i) (finRange 3)).prod) ≤ K * ↑(#A)

Tactic:
simpa [this _ (hδ _), pow_succ'] using hA

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
ε : ℤ
hε : |ε| = 1
⊢ A ^ ε = A

Tactic:
obtain rfl | rfl := eq_or_eq_neg_of_abs_eq hε <;> simp [hAsymm]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
⊢ ↑(#(A ^ m)) ≤ K ^ (m - 2) * ↑(#A)

Tactic:
have (ε : ℤ) (hε : |ε| = 1) : A ^ ε = A := by
  obtain rfl | rfl := eq_or_eq_neg_of_abs_eq hε <;> simp [hAsymm]

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ), |ε| = 1 → A ^ ε = A
⊢ ↑(#(A ^ m)) ≤ K ^ (m - 2) * ↑(#A)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ), |ε| = 1 → A ^ ε = A
⊢ ↑(#(A ^ m)) ≤ K ^ (m - 2) * ↑(#A)

Tactic:
calc
  (#(A ^ m) : ℝ) = #((finRange m).map fun i ↦ A ^ 1).prod := by simp
  _ ≤ K ^ (m - 2) * #A :=
    inductive_claim_mul hm (fun δ hδ ↦ by simpa [this _ (hδ _), pow_succ'] using hA) _ (by simp)

Result:
no goals
-- Mathlib/Logic/Equiv/Set.lean
theorem sumDiffSubset_symm_apply_of_mem {α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)]
    {x : t} (hx : x.1 ∈ s) : (Equiv.Set.sumDiffSubset h).symm x = Sum.inl ⟨x, hx⟩

Proof state:
case a
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ (Set.sumDiffSubset h) ((Set.sumDiffSubset h).symm x) = (Set.sumDiffSubset h) (Sum.inl ⟨↑x, hx⟩)

Tactic:
simp only [apply_symm_apply, sumDiffSubset_apply_inl, Set.inclusion_mk]

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ (Set.sumDiffSubset h).symm x = Sum.inl ⟨↑x, hx⟩

Tactic:
apply (Equiv.Set.sumDiffSubset h).injective

Result:
case a
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ (Set.sumDiffSubset h) ((Set.sumDiffSubset h).symm x) = (Set.sumDiffSubset h) (Sum.inl ⟨↑x, hx⟩)
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
lemma mor₂_eq_zero_iff_epi₁ : T.mor₂ = 0 ↔ Epi T.mor₁

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.invRotate.mor₃ = 0 ↔ Epi T.invRotate.mor₂
⊢ T.mor₂ = 0 ↔ Epi T.mor₁

Tactic:
dsimp at h

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.mor₂ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.3 = 0 ↔ Epi T.mor₁
⊢ T.mor₂ = 0 ↔ Epi T.mor₁

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.mor₂ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.3 = 0 ↔ Epi T.mor₁
⊢ T.mor₂ = 0 ↔ Epi T.mor₁

Tactic:
rw [← h, IsIso.comp_right_eq_zero]

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.mor₂ = 0 ↔ Epi T.mor₁

Tactic:
have h := mor₃_eq_zero_iff_epi₂ _ (inv_rot_of_distTriang _ hT)

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.invRotate.mor₃ = 0 ↔ Epi T.invRotate.mor₂
⊢ T.mor₂ = 0 ↔ Epi T.mor₁
-- Mathlib/Analysis/Analytic/Composition.lean
theorem comp_removeZero (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) :
    q.comp p.removeZero = q.comp p

Proof state:
case h.H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x✝ : Fin n → E
⊢ (q.comp p.removeZero n) x✝ = (q.comp p n) x✝

Tactic:
simp [FormalMultilinearSeries.comp]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
⊢ q.comp p.removeZero = q.comp p

Tactic:
ext n

Result:
case h.H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x✝ : Fin n → E
⊢ (q.comp p.removeZero n) x✝ = (q.comp p n) x✝
-- Mathlib/Data/Nat/Lattice.lean
theorem sInf_le {s : Set ℕ} {m : ℕ} (hm : m ∈ s) : sInf s ≤ m

Proof state:
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ sInf s ≤ m

Tactic:
classical
rw [Nat.sInf_def ⟨m, hm⟩]
exact Nat.find_min' ⟨m, hm⟩ hm

Result:
no goals

Proof state:
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ sInf s ≤ m

Tactic:
rw [Nat.sInf_def ⟨m, hm⟩]

Result:
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ Nat.find ⋯ ≤ m

Proof state:
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ Nat.find ⋯ ≤ m

Tactic:
exact Nat.find_min' ⟨m, hm⟩ hm

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem nonempty_of_pos_dist (h : 0 < G.dist u v) :
    (Set.univ : Set (G.Walk u v)).Nonempty

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
h : 0 < G.dist u v
⊢ Set.univ.Nonempty

Tactic:
rw [dist_eq_sInf] at h

Result:
V : Type u_1
G : SimpleGraph V
u v : V
h : 0 < sInf (Set.range Walk.length)
⊢ Set.univ.Nonempty

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
h : 0 < sInf (Set.range Walk.length)
⊢ Set.univ.Nonempty

Tactic:
simpa [Set.range_nonempty_iff_nonempty, Set.nonempty_iff_univ_nonempty] using
  Nat.nonempty_of_pos_sInf h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem hasLimitsOfShape_of_equivalence {J' : Type u₂} [Category.{v₂} J'] (e : J ≌ J')
    [HasLimitsOfShape J C] : HasLimitsOfShape J' C

Proof state:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J' C

Tactic:
constructor

Result:
case has_limit
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
⊢ autoParam (∀ (F : J' ⥤ C), HasLimit F) _auto✝

Proof state:
case has_limit
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
F : J' ⥤ C
⊢ HasLimit F

Tactic:
apply hasLimitOfEquivalenceComp e

Result:
no goals

Proof state:
case has_limit
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
⊢ autoParam (∀ (F : J' ⥤ C), HasLimit F) _auto✝

Tactic:
intro F

Result:
case has_limit
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
F : J' ⥤ C
⊢ HasLimit F
-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
theorem Submodule.rank_sup_add_rank_inf_eq (s t : Submodule R M) :
    Module.rank R (s ⊔ t : Submodule R M) + Module.rank R (s ⊓ t : Submodule R M) =
    Module.rank R s + Module.rank R t

Proof state:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
s t : Submodule R M
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥t

Tactic:
conv_rhs => enter [2]; rw [show t = (s ⊔ t) ⊓ t by simp]

Result:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
s t : Submodule R M
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥((s ⊔ t) ⊓ t)

Proof state:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
s t : Submodule R M
⊢ t = (s ⊔ t) ⊓ t

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
s t : Submodule R M
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥((s ⊔ t) ⊓ t)

Tactic:
rw [← rank_quotient_add_rank ((s ⊓ t).comap s.subtype),
  ← rank_quotient_add_rank (t.comap (s ⊔ t).subtype),
  (quotientInfEquivSupQuotient s t).rank_eq,
  (equivSubtypeMap s (comap _ (s ⊓ t))).rank_eq, Submodule.map_comap_subtype,
  (equivSubtypeMap (s ⊔ t) (comap _ t)).rank_eq, Submodule.map_comap_subtype,
  ← inf_assoc, inf_idem, add_right_comm]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Polar.lean
theorem polar_singleton {a : E} : B.polar {a} = { y | ‖B a y‖ ≤ 1 } := le_antisymm
  (fun _ hy => hy _ rfl)
  (fun y hy => (polar_mem_iff _ _ _).mp (fun _ hb => by rw [Set.mem_singleton_iff.mp hb]; exact hy))

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
a : E
y : F
hy : y ∈ {y | ‖(B a) y‖ ≤ 1}
x✝ : E
hb : x✝ ∈ {a}
⊢ ‖(B a) y‖ ≤ 1

Tactic:
exact hy

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
a : E
y : F
hy : y ∈ {y | ‖(B a) y‖ ≤ 1}
x✝ : E
hb : x✝ ∈ {a}
⊢ ‖(B x✝) y‖ ≤ 1

Tactic:
rw [Set.mem_singleton_iff.mp hb]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
a : E
y : F
hy : y ∈ {y | ‖(B a) y‖ ≤ 1}
x✝ : E
hb : x✝ ∈ {a}
⊢ ‖(B a) y‖ ≤ 1
-- Mathlib/Data/List/EditDistance/Bounds.lean
theorem suffixLevenshtein_minimum_le_levenshtein_append (xs ys₁ ys₂) :
    (suffixLevenshtein C xs ys₂).1.minimum ≤ levenshtein C xs (ys₁ ++ ys₂)

Proof state:
case cons
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
ys₂ : List β
y : β
ys₁ : List β
⊢ (↑(suffixLevenshtein C xs ys₂)).minimum ≤ ↑(levenshtein C xs (y :: ys₁ ++ ys₂))

Tactic:
exact (le_suffixLevenshtein_append_minimum _ _ _).trans
  (suffixLevenshtein_minimum_le_levenshtein_cons _ _ _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
ys₁ ys₂ : List β
⊢ (↑(suffixLevenshtein C xs ys₂)).minimum ≤ ↑(levenshtein C xs (ys₁ ++ ys₂))

Tactic:
cases ys₁ with
| nil => exact List.minimum_le_of_mem' (List.getElem_mem _)
| cons y ys₁ =>
    exact (le_suffixLevenshtein_append_minimum _ _ _).trans
      (suffixLevenshtein_minimum_le_levenshtein_cons _ _ _)

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
ys₂ : List β
⊢ (↑(suffixLevenshtein C xs ys₂)).minimum ≤ ↑(levenshtein C xs ([] ++ ys₂))

Tactic:
exact List.minimum_le_of_mem' (List.getElem_mem _)

Result:
no goals
-- Mathlib/Order/Filter/Pointwise.lean
theorem inv_mem_inv (hs : s ∈ f) : s⁻¹ ∈ f⁻¹

Proof state:
α : Type u_2
inst✝ : InvolutiveInv α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s⁻¹ ∈ f⁻¹

Tactic:
rwa [mem_inv, inv_preimage, inv_inv]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Presheaf/EpiMono.lean
lemma surjective_of_epi [Epi f] (X : Cᵒᵖ) :
    Function.Surjective (f.app X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Epi f
X : Cᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app X))

Tactic:
rw [← ModuleCat.epi_iff_surjective]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Epi f
X : Cᵒᵖ
⊢ Epi (f.app X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Epi f
X : Cᵒᵖ
⊢ Epi (f.app X)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Even.lean
lemma even_mul_succ_self (n : ℕ) : Even (n * (n + 1))

Proof state:
n : ℕ
⊢ Even n ∨ ¬Even n

Tactic:
exact em _

Result:
no goals

Proof state:
n : ℕ
⊢ Even (n * (n + 1))

Tactic:
rw [even_mul, even_add_one]

Result:
n : ℕ
⊢ Even n ∨ ¬Even n
-- Mathlib/LinearAlgebra/BilinearForm/Basic.lean
lemma smul_right_of_tower (r : S) (x y : M) : B x (r • y) = r • B x y

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
B : BilinForm R M
r : S
x y : M
⊢ (B x) (r • y) = r • (B x) y

Tactic:
rw [← IsScalarTower.algebraMap_smul R r, smul_right, Algebra.smul_def]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
lemma countableOrCountablyGenerated_left_of_prod_left_of_nonempty [Nonempty β]
    [h : CountableOrCountablyGenerated (α × β) γ] :
    CountableOrCountablyGenerated α γ

Proof state:
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h : CountableOrCountablyGenerated (α × β) γ
⊢ CountableOrCountablyGenerated α γ

Tactic:
rcases h.countableOrCountablyGenerated with (h | h)

Result:
case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated α γ

case inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated α γ

Proof state:
case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
this : Countable α
⊢ CountableOrCountablyGenerated α γ

Tactic:
infer_instance

Result:
no goals

Proof state:
case inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated α γ

Tactic:
infer_instance

Result:
no goals

Proof state:
case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated α γ

Tactic:
have := countable_left_of_prod_of_nonempty h

Result:
case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
this : Countable α
⊢ CountableOrCountablyGenerated α γ
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_X : derivative (X : R[X]) = 1 :=
  (derivative_monomial _ _).trans <| by simp

Proof state:
R : Type u
inst✝ : Semiring R
⊢ (monomial (1 - 1)) (1 * ↑1) = 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem castLE_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) (i : Fin k) :
    Fin.castLE mn (Fin.castLE km i) = Fin.castLE (Nat.le_trans km mn) i :=
  Fin.ext (by simp only [coe_castLE])

Proof state:
k m n : Nat
km : k ≤ m
mn : m ≤ n
i : Fin k
⊢ ↑(castLE mn (castLE km i)) = ↑(castLE ⋯ i)

Tactic:
simp only [coe_castLE]

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma rnDeriv_pos [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (ha : κ a ≪ η a) :
    ∀ᵐ x ∂(κ a), 0 < rnDeriv κ η a x

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
ha : κ a ≪ η a
⊢ ∀ᵐ (x : γ) ∂κ a, 0 < κ.rnDeriv η a x

Tactic:
filter_upwards [ha.ae_le κ.rnDeriv_eq_rnDeriv_measure, Measure.rnDeriv_pos ha]
  with x heq hpos using heq ▸ hpos

Result:
no goals
-- Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean
lemma Sieve.generateSingleton_eq {X Y : C} (f : Y ⟶ X) :
    Sieve.generate (Presieve.singleton f) = Sieve.generateSingleton f

Proof state:
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
⊢ (generate (Presieve.singleton f)).arrows g ↔ (generateSingleton f).arrows g

Tactic:
constructor

Result:
case h.mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
⊢ (generate (Presieve.singleton f)).arrows g → (generateSingleton f).arrows g

case h.mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
⊢ (generateSingleton f).arrows g → (generate (Presieve.singleton f)).arrows g

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
⊢ generate (Presieve.singleton f) = generateSingleton f

Tactic:
ext Z g

Result:
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
⊢ (generate (Presieve.singleton f)).arrows g ↔ (generateSingleton f).arrows g

Proof state:
case h.mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
⊢ (generateSingleton f).arrows g → (generate (Presieve.singleton f)).arrows g

Tactic:
rintro ⟨g,h⟩

Result:
case h.mpr.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
Z : C
g✝ : Z ⟶ X
g : Z ⟶ Y
h : g ≫ f = g✝
⊢ (generate (Presieve.singleton f)).arrows g✝

Proof state:
case h.mpr.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
Z : C
g✝ : Z ⟶ X
g : Z ⟶ Y
h : g ≫ f = g✝
⊢ (generate (Presieve.singleton f)).arrows g✝

Tactic:
exact ⟨Y,g,f,⟨⟩,h⟩

Result:
no goals

Proof state:
case h.mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
⊢ (generate (Presieve.singleton f)).arrows g → (generateSingleton f).arrows g

Tactic:
rintro ⟨W,i,p,⟨⟩,rfl⟩

Result:
case h.mp.intro.intro.intro.intro.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y✝ : C
f : Y✝ ⟶ X
Z Y : C
i : Z ⟶ Y✝
⊢ (generateSingleton f).arrows (i ≫ f)

Proof state:
case h.mp.intro.intro.intro.intro.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y✝ : C
f : Y✝ ⟶ X
Z Y : C
i : Z ⟶ Y✝
⊢ (generateSingleton f).arrows (i ≫ f)

Tactic:
exact ⟨i,rfl⟩

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Vector/Monadic.lean
theorem toArray_mapIdxM [Monad m] [LawfulMonad m] (a : Vector α n) (f : Nat → α → m β) :
    toArray <$> a.mapIdxM f = a.toArray.mapIdxM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Vector α n
f : Nat → α → m β
⊢ toArray <$> mapIdxM f a = Array.mapIdxM f a.toArray

Tactic:
exact toArray_mapFinIdxM _ _

Result:
no goals