harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_of_contains_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List α} {k : α} (h₂ : l.contains k = false) :
    (insertManyIfNewUnit m l).1.contains k → m.contains k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
k : α
h₂ : l.contains k = false
⊢ (insertManyIfNewUnit m l).val.contains k = true → m.contains k = true

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.containsKey_of_containsKey_insertListIfNewUnit

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Finite.lean
/-- If we preserve limits of some arbitrary size, then we preserve all finite limits. -/
lemma PreservesLimitsOfSize.preservesFiniteLimits (F : C ⥤ D)
    [PreservesLimitsOfSize.{w, w₂} F] : PreservesFiniteLimits F where
  preservesFiniteLimits J (sJ : SmallCategory J) fJ

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesLimitsOfShape J F

Tactic:
exact preservesLimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesLimitsOfShape J F

Tactic:
haveI := preservesSmallestLimits_of_preservesLimits F

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesLimitsOfShape J F
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem num_zero_eq (h_inj : Function.Injective (algebraMap R P)) :
    num (0 : FractionalIdeal S P) = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
h_inj : Function.Injective ⇑(algebraMap R P)
⊢ num 0 = 0

Tactic:
simpa [num, LinearMap.ker_eq_bot] using h_inj

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem orbit.pairwiseDisjoint :
    (Set.range fun x : X => orbit G x).PairwiseDisjoint id

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
x y : X
h : (fun x => orbit G x) x ≠ (fun x => orbit G x) y
⊢ Function.onFun Disjoint id ((fun x => orbit G x) x) ((fun x => orbit G x) y)

Tactic:
contrapose! h

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
x y : X
h : ¬Function.onFun Disjoint id (orbit G x) (orbit G y)
⊢ orbit G x = orbit G y

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
x y : X
h : ¬Function.onFun Disjoint id (orbit G x) (orbit G y)
⊢ orbit G x = orbit G y

Tactic:
exact (orbit.eq_or_disjoint x y).resolve_right h

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ (range fun x => orbit G x).PairwiseDisjoint id

Tactic:
rintro s ⟨x, rfl⟩ t ⟨y, rfl⟩ h

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
x y : X
h : (fun x => orbit G x) x ≠ (fun x => orbit G x) y
⊢ Function.onFun Disjoint id ((fun x => orbit G x) x) ((fun x => orbit G x) y)
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem mem_sumSq {s : T} : s ∈ sumSq T ↔ IsSumSq s

Proof state:
T : Type u_2
inst✝ : CommSemiring T
s : T
⊢ s ∈ sumSq T ↔ IsSumSq s

Tactic:
simp [← Subsemiring.mem_toNonUnitalSubsemiring]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem mapL_smul [DecidableEq ι] (i : ι) (c : 𝕜) (u : E i →L[𝕜] E' i) :
    mapL (update f i (c • u)) = c • mapL (update f i u)

Proof state:
ι : Type uι
inst✝⁶ : Fintype ι
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
c : 𝕜
u : E i →L[𝕜] E' i
⊢ mapL (update f i (c • u)) = c • mapL (update f i u)

Tactic:
ext x

Result:
case h
ι : Type uι
inst✝⁶ : Fintype ι
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
c : 𝕜
u : E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
⊢ (mapL (update f i (c • u))) x = (c • mapL (update f i u)) x

Proof state:
case h
ι : Type uι
inst✝⁶ : Fintype ι
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
c : 𝕜
u : E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
⊢ (mapL (update f i (c • u))) x = (c • mapL (update f i u)) x

Tactic:
simp only [mapL_apply, mapL_add_smul_aux, ContinuousLinearMap.coe_smul,
  PiTensorProduct.map_update_smul, LinearMap.smul_apply, ContinuousLinearMap.coe_smul',
  Pi.smul_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_or_inj_left : ∀ {m x y : Bool}, (m && x) = (m && y) → (m || x) = (m || y) → x = y

Proof state:
⊢ ∀ {m x y : Bool}, (m && x) = (m && y) → (m || x) = (m || y) → x = y

Tactic:
decide

Result:
no goals
-- Mathlib/Topology/Algebra/GroupWithZero.lean
lemma nhds_inv₀ (hx : x ≠ 0) : 𝓝 x⁻¹ = (𝓝 x)⁻¹

Proof state:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : TopologicalSpace G₀
inst✝ : HasContinuousInv₀ G₀
x : G₀
hx : x ≠ 0
⊢ (𝓝 x⁻¹)⁻¹ ≤ 𝓝 x

Tactic:
simpa only [inv_inv] using tendsto_inv₀ (inv_ne_zero hx)

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : TopologicalSpace G₀
inst✝ : HasContinuousInv₀ G₀
x : G₀
hx : x ≠ 0
⊢ 𝓝 x⁻¹ = (𝓝 x)⁻¹

Tactic:
refine le_antisymm (inv_le_iff_le_inv.1 ?_) (tendsto_inv₀ hx)

Result:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : TopologicalSpace G₀
inst✝ : HasContinuousInv₀ G₀
x : G₀
hx : x ≠ 0
⊢ (𝓝 x⁻¹)⁻¹ ≤ 𝓝 x
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_le_card_height [Fintype m] [StrongRankCondition R] (A : Matrix m n R) :
    A.rank ≤ Fintype.card m

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : StrongRankCondition R
A : Matrix m n R
this : Module.Finite R (m → R)
⊢ A.rank ≤ Fintype.card m

Tactic:
haveI : Module.Free R (m → R) := Module.Free.pi _ _

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : StrongRankCondition R
A : Matrix m n R
this✝ : Module.Finite R (m → R)
this : Free R (m → R)
⊢ A.rank ≤ Fintype.card m

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : StrongRankCondition R
A : Matrix m n R
⊢ A.rank ≤ Fintype.card m

Tactic:
haveI : Module.Finite R (m → R) := Module.Finite.pi

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : StrongRankCondition R
A : Matrix m n R
this : Module.Finite R (m → R)
⊢ A.rank ≤ Fintype.card m

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : StrongRankCondition R
A : Matrix m n R
this✝ : Module.Finite R (m → R)
this : Free R (m → R)
⊢ A.rank ≤ Fintype.card m

Tactic:
exact (Submodule.finrank_le _).trans (finrank_pi R).le

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem dropn_tail (s : Seq α) (n) : drop (tail s) n = drop s (n + 1)

Proof state:
α : Type u
s : Seq α
n : ℕ
⊢ s.drop (1 + n) = s.tail.drop n

Tactic:
apply dropn_add

Result:
no goals

Proof state:
α : Type u
s : Seq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)

Tactic:
symm

Result:
α : Type u
s : Seq α
n : ℕ
⊢ s.drop (1 + n) = s.tail.drop n

Proof state:
α : Type u
s : Seq α
n : ℕ
⊢ s.tail.drop n = s.drop (n + 1)

Tactic:
rw [Nat.add_comm]

Result:
α : Type u
s : Seq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma coeff_preΨ_ne_zero {n : ℤ} (h : (n : R) ≠ 0) :
    (W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) ≠ 0

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
h : ↑n ≠ 0
⊢ (W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) ≠ 0

Tactic:
induction n using Int.negInduction with
| nat n => simpa only [preΨ_ofNat, Int.even_coe_nat]
    using W.coeff_preΨ'_ne_zero <| by exact_mod_cast h
| neg ih n => simpa only [preΨ_neg, coeff_neg, neg_ne_zero, Int.natAbs_neg, even_neg]
      using ih n <| neg_ne_zero.mp <| by exact_mod_cast h

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), ↑↑n ≠ 0 → (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) ≠ 0
n : ℕ
h : ↑(-↑n) ≠ 0
⊢ (W.preΨ (-↑n)).coeff (((-↑n).natAbs ^ 2 - if Even (-↑n) then 4 else 1) / 2) ≠ 0

Tactic:
simpa only [preΨ_neg, coeff_neg, neg_ne_zero, Int.natAbs_neg, even_neg]
using ih n <| neg_ne_zero.mp <| by exact_mod_cast h

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), ↑↑n ≠ 0 → (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) ≠ 0
n : ℕ
h : ↑(-↑n) ≠ 0
⊢ -↑↑n ≠ 0

Tactic:
exact_mod_cast h

Result:
no goals

Proof state:
case nat
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑↑n ≠ 0
⊢ (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) ≠ 0

Tactic:
simpa only [preΨ_ofNat, Int.even_coe_nat]
using W.coeff_preΨ'_ne_zero <| by exact_mod_cast h

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑↑n ≠ 0
⊢ ↑n ≠ 0

Tactic:
exact_mod_cast h

Result:
no goals
-- Mathlib/Topology/MetricSpace/Antilipschitz.lean
theorem antilipschitzWith_iff_le_mul_nndist :
    AntilipschitzWith K f ↔ ∀ x y, nndist x y ≤ K * nndist (f x) (f y)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), ↑(nndist x y) ≤ ↑K * ↑(nndist (f x) (f y))) ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)

Tactic:
norm_cast

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ AntilipschitzWith K f ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)

Tactic:
simp only [AntilipschitzWith, edist_nndist]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), ↑(nndist x y) ≤ ↑K * ↑(nndist (f x) (f y))) ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_neg' (x : Game) : (-x).birthday ≤ x.birthday

Proof state:
x : Game
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ (-x).birthday ≤ x.birthday

Tactic:
rw [← hy₂, ← PGame.birthday_neg y]

Result:
x : Game
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ (-x).birthday ≤ (-y).birthday

Proof state:
x : Game
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ (-x).birthday ≤ (-y).birthday

Tactic:
conv_lhs => rw [← hy₁]

Result:
x : Game
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ (-⟦y⟧).birthday ≤ (-y).birthday

Proof state:
x : Game
⊢ (-x).birthday ≤ x.birthday

Tactic:
let ⟨y, hy₁, hy₂⟩ := birthday_eq_pGameBirthday x

Result:
x : Game
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ (-x).birthday ≤ x.birthday

Proof state:
x : Game
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ (-⟦y⟧).birthday ≤ (-y).birthday

Tactic:
apply birthday_quot_le_pGameBirthday

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.convex_le (hf : ConvexOn 𝕜 s f) (r : β) : Convex 𝕜 ({ x ∈ s | f x ≤ r }) :=
  fun x hx y hy a b ha hb hab =>
  ⟨hf.1 hx.1 hy.1 ha hb hab,
    calc
      f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx.1 hy.1 ha hb hab
      _ ≤ a • r + b • r

Proof state:
case h₁.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x ≤ r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x ≤ r}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f x ≤ r

Tactic:
exact hx.2

Result:
no goals

Proof state:
case h₂.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x ≤ r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x ≤ r}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f y ≤ r

Tactic:
exact hy.2

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x ≤ r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x ≤ r}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • r + b • r

Tactic:
gcongr

Result:
case h₁.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x ≤ r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x ≤ r}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f x ≤ r

case h₂.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x ≤ r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x ≤ r}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f y ≤ r
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem blsub_comp {o o' : Ordinal.{max u v}} {f : ∀ a < o, Ordinal.{max u v w}}
    (hf : ∀ {i j} (hi) (hj), i ≤ j → f i hi ≤ f j hj) {g : ∀ a < o', Ordinal.{max u v}}
    (hg : blsub.{_, u} o' g = o) :
    (blsub.{_, w} o' fun a ha => f (g a ha) (by rw [← hg]; apply lt_blsub)) = blsub.{_, w} o f :=
  @bsup_comp.{u, v, w} o _ (fun a ha => succ (f a ha))
    (fun {_ _} _ _ h => succ_le_succ_iff.2 (hf _ _ h)) g hg

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
a : Ordinal.{max u v}
ha : a < o'
⊢ g a ha < o

Tactic:
rw [← hg]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
a : Ordinal.{max u v}
ha : a < o'
⊢ g a ha < o'.blsub g

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
a : Ordinal.{max u v}
ha : a < o'
⊢ g a ha < o'.blsub g

Tactic:
apply lt_blsub

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem mem_insertIdx {a b : α} :
    ∀ {n : Nat} {l : List α} (_ : n ≤ l.length), a ∈ l.insertIdx n b ↔ a = b ∨ a ∈ l
  | 0, as, _ => by simp
  | _ + 1, [], h => (Nat.not_succ_le_zero _ h).elim
  | n + 1, a' :: as, h => by
    rw [List.insertIdx_succ_cons, mem_cons, mem_insertIdx (Nat.le_of_succ_le_succ h),
      ← or_assoc, @or_comm (a = a'), or_assoc, mem_cons]

Proof state:
α : Type u
a b : α
n : Nat
a' : α
as : List α
h : n + 1 ≤ (a' :: as).length
⊢ a ∈ insertIdx (n + 1) b (a' :: as) ↔ a = b ∨ a ∈ a' :: as

Tactic:
rw [List.insertIdx_succ_cons, mem_cons, mem_insertIdx (Nat.le_of_succ_le_succ h),
  ← or_assoc, @or_comm (a = a'), or_assoc, mem_cons]

Result:
no goals

Proof state:
α : Type u
a b : α
as : List α
x✝ : 0 ≤ as.length
⊢ a ∈ insertIdx 0 b as ↔ a = b ∨ a ∈ as

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.add_const [AddCommSemigroup α] (h : Periodic f c) (a : α) :
    Periodic (fun x => f (x + a)) c := fun x => by
  simpa only [add_right_comm] using h (x + a)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommSemigroup α
h : Periodic f c
a x : α
⊢ (fun x => f (x + a)) (x + c) = (fun x => f (x + a)) x

Tactic:
simpa only [add_right_comm] using h (x + a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem shiftLeft_congr (m n : Nat) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m)
    (rhs' : BitVec n) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    lhs <<< rhs = lhs' <<< rhs'

Proof state:
m n : Nat
lhs : BitVec m
rhs : BitVec n
lhs' : BitVec m
rhs' : BitVec n
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs <<< rhs = lhs' <<< rhs'

Tactic:
simp[*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/UInt/Basic.lean
theorem le_usize_size : 4294967296 ≤ USize.size

Proof state:
⊢ 4294967296 ≤ USize.size

Tactic:
cases usize_size_eq <;> next h => rw [h]; decide

Result:
no goals

Proof state:
h : USize.size = 18446744073709551616
⊢ 4294967296 ≤ USize.size

Tactic:
rw [h]

Result:
h : USize.size = 18446744073709551616
⊢ 4294967296 ≤ 18446744073709551616

Proof state:
h : USize.size = 18446744073709551616
⊢ 4294967296 ≤ 18446744073709551616

Tactic:
decide

Result:
no goals
-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
lemma equivHeightOneSpectrum_symm_apply (v : HeightOneSpectrum (𝓞 K)) (x : K) :
    (equivHeightOneSpectrum.symm v) x = ‖embedding v x‖

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : K
this : v = (equivHeightOneSpectrum.symm v).maximalIdeal
⊢ (equivHeightOneSpectrum.symm v) x = ‖(embedding v) x‖

Tactic:
convert (norm_embedding_eq (equivHeightOneSpectrum.symm v) x).symm

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : K
⊢ (equivHeightOneSpectrum.symm v) x = ‖(embedding v) x‖

Tactic:
have : v = (equivHeightOneSpectrum.symm v).maximalIdeal := by
  show v = equivHeightOneSpectrum (equivHeightOneSpectrum.symm v)
  exact (Equiv.apply_symm_apply _ v).symm

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : K
this : v = (equivHeightOneSpectrum.symm v).maximalIdeal
⊢ (equivHeightOneSpectrum.symm v) x = ‖(embedding v) x‖

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : K
⊢ v = (equivHeightOneSpectrum.symm v).maximalIdeal

Tactic:
show v = equivHeightOneSpectrum (equivHeightOneSpectrum.symm v)

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : K
⊢ v = equivHeightOneSpectrum (equivHeightOneSpectrum.symm v)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : K
⊢ v = equivHeightOneSpectrum (equivHeightOneSpectrum.symm v)

Tactic:
exact (Equiv.apply_symm_apply _ v).symm

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc (attr := simp)]
lemma associativity (X Y Z : C) :
    μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
        (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z)

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.LaxMonoidal
X Y Z : C
⊢ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z)

Tactic:
apply associativity'

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem zero_shiftLeft : ∀ n : ℤ, 0 <<< n = 0
  | (n : ℕ) => congr_arg ((↑) : ℕ → ℤ) (by simp)
  | -[_+1] => congr_arg ((↑) : ℕ → ℤ) (by simp)

Proof state:
a✝ : ℕ
⊢ 0 >>> a✝.succ = 0

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ Nat.shiftLeft' false 0 n = 0

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Over.lean
lemma overEquiv_iff {X : C} {Y : Over X} (S : Sieve Y) {Z : C} (f : Z ⟶ Y.left) :
    overEquiv Y S f ↔ S (Over.homMk f : Over.mk (f ≫ Y.hom) ⟶ Y)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y
Z : C
f : Z ⟶ Y.left
⊢ ((overEquiv Y) S).arrows f ↔ S.arrows (Over.homMk f ⋯)

Tactic:
obtain ⟨S, rfl⟩ := (overEquiv Y).symm.surjective S

Result:
case intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
Z : C
f : Z ⟶ Y.left
S : Sieve Y.left
⊢ ((overEquiv Y) ((overEquiv Y).symm S)).arrows f ↔ ((overEquiv Y).symm S).arrows (Over.homMk f ⋯)

Proof state:
case intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
Z : C
f : Z ⟶ Y.left
S : Sieve Y.left
⊢ ((overEquiv Y) ((overEquiv Y).symm S)).arrows f ↔ ((overEquiv Y).symm S).arrows (Over.homMk f ⋯)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Semiconj/Basic.lean
@[to_additive (attr := simp)] lemma inv_symm_left_iff : SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y

Proof state:
G : Type u_1
inst✝ : Group G
a x y : G
⊢ SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y

Tactic:
simp_rw [SemiconjBy, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul, eq_comm]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Pi.lean
theorem generateFrom_eq_pi [h : ∀ i, MeasurableSpace (α i)] {C : ∀ i, Set (Set (α i))}
    (hC : ∀ i, generateFrom (C i) = h i) (h2C : ∀ i, IsCountablySpanning (C i)) :
    generateFrom (pi univ '' pi univ C) = MeasurableSpace.pi

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
h : (i : ι) → MeasurableSpace (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = h i
h2C : ∀ (i : ι), IsCountablySpanning (C i)
⊢ generateFrom (univ.pi '' univ.pi C) = MeasurableSpace.pi

Tactic:
simp only [← funext hC, generateFrom_pi_eq h2C]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean
lemma absolutelyContinuous_smul {c : ℝ≥0∞} (hc : c ≠ 0) : μ ≪ c • μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
hc : c ≠ 0
⊢ μ ≪ c • μ

Tactic:
simp [AbsolutelyContinuous, hc]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem clusterPt_iff_forall_mem_closure {F : Filter X} :
    ClusterPt x F ↔ ∀ s ∈ F, x ∈ closure s

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
⊢ ClusterPt x F ↔ ∀ s ∈ F, x ∈ closure s

Tactic:
simp_rw [ClusterPt, inf_neBot_iff, mem_closure_iff_nhds]

Result:
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
⊢ (∀ ⦃s : Set X⦄, s ∈ 𝓝 x → ∀ ⦃s' : Set X⦄, s' ∈ F → (s ∩ s').Nonempty) ↔ ∀ s ∈ F, ∀ t ∈ 𝓝 x, (t ∩ s).Nonempty

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
⊢ (∀ ⦃s : Set X⦄, s ∈ 𝓝 x → ∀ ⦃s' : Set X⦄, s' ∈ F → (s ∩ s').Nonempty) ↔ ∀ s ∈ F, ∀ t ∈ 𝓝 x, (t ∩ s).Nonempty

Tactic:
rw [forall₂_swap]

Result:
no goals