harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma twoTorsionPolynomial_of_char_three : W.twoTorsionPolynomial = ⟨1, W.b₂, -W.b₄, W.b₆⟩

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ } = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }

Tactic:
ext <;> dsimp

Result:
case a
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ 4 = 1

case c
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ 2 * W.b₄ = -W.b₄

Proof state:
case a
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ 4 = 1

Tactic:
linear_combination CharP.cast_eq_zero R 3

Result:
no goals

Proof state:
case c
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ 2 * W.b₄ = -W.b₄

Tactic:
linear_combination W.b₄ * CharP.cast_eq_zero R 3

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.twoTorsionPolynomial = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }

Tactic:
rw [twoTorsionPolynomial]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ } = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }
-- Mathlib/Data/PNat/Basic.lean
theorem sub_add_of_lt {a b : ℕ+} (h : b < a) : a - b + b = a

Proof state:
a b : ℕ+
h : b < a
⊢ a - b + b = a

Tactic:
rw [add_comm, add_sub_of_lt h]

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Real.lean
lemma IccLeftChart_extend_bot : (IccLeftChart x y).extend (𝓡∂ 1) ⊥ = 0

Proof state:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑(𝓡∂ 1) ⟨fun x => 0, ⋯⟩ = 0

Tactic:
congr

Result:
no goals

Proof state:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑((IccLeftChart x y).extend (𝓡∂ 1)) ⊥ = 0

Tactic:
norm_num [IccLeftChart, modelWithCornersEuclideanHalfSpace_zero]

Result:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑(𝓡∂ 1) ⟨fun x => 0, ⋯⟩ = 0
-- Mathlib/Tactic/Ring/Basic.lean
theorem pow_bit0 {k : ℕ} (_ : (a : R) ^ k = b) (_ : b * b = c) :
    a ^ (Nat.mul (nat_lit 2) k) = c

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ Nat.mul 2 k = a ^ k * a ^ k

Tactic:
simp [Nat.succ_mul, pow_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a b c : R
k : ℕ
x✝¹ : a ^ k = b
x✝ : b * b = c
⊢ a ^ Nat.mul 2 k = c

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ Nat.mul 2 k = a ^ k * a ^ k
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem getKeyD_eq [BEq α] {l : AssocList α β} {a fallback : α} :
    l.getKeyD a fallback = List.getKeyD a l.toList fallback

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
a fallback key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : getKeyD a fallback tail✝ = List.getKeyD a tail✝.toList fallback
⊢ getKeyD a fallback (cons key✝ value✝ tail✝) = List.getKeyD a (cons key✝ value✝ tail✝).toList fallback

Tactic:
simp_all [getKeyD, List.getKeyD, Bool.apply_cond (fun x => Option.getD x fallback)]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a fallback : α
⊢ getKeyD a fallback nil = List.getKeyD a nil.toList fallback

Tactic:
simp [getKeyD, List.getKeyD]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : AssocList α β
a fallback : α
⊢ getKeyD a fallback l = List.getKeyD a l.toList fallback

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a fallback : α
⊢ getKeyD a fallback nil = List.getKeyD a nil.toList fallback

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
a fallback key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : getKeyD a fallback tail✝ = List.getKeyD a tail✝.toList fallback
⊢ getKeyD a fallback (cons key✝ value✝ tail✝) = List.getKeyD a (cons key✝ value✝ tail✝).toList fallback
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
lemma IsEquipartition.card_interedges_sparsePairs_le' (hP : P.IsEquipartition)
    (hε : 0 ≤ ε) :
    #((P.sparsePairs G ε).biUnion fun (U, V) ↦ G.interedges U V) ≤ ε * (#A + #P.parts) ^ 2

Proof state:
case calc_1.h.mk
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
U V : Finset α
hUV : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V ∧ ↑(#(G.interedges U V)) / (↑(#U) * ↑(#V)) < ε
⊢ 0 < ↑(#U) * ↑(#V)

Tactic:
exact mul_pos (Nat.cast_pos.2 (P.nonempty_of_mem_parts hUV.1).card_pos)
  (Nat.cast_pos.2 (P.nonempty_of_mem_parts hUV.2.1).card_pos)

Result:
no goals

Proof state:
case calc_1.h
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
UV : Finset α × Finset α
hUV : UV ∈ P.sparsePairs G ε
⊢ ↑(#(G.interedges UV.1 UV.2)) ≤ ε * (↑(#UV.1) * ↑(#UV.2))

Tactic:
obtain ⟨U, V⟩ := UV

Result:
case calc_1.h.mk
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
U V : Finset α
hUV : (U, V) ∈ P.sparsePairs G ε
⊢ ↑(#(G.interedges (U, V).1 (U, V).2)) ≤ ε * (↑(#(U, V).1) * ↑(#(U, V).2))

Proof state:
case calc_2.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ (#P.parts * (#A / #P.parts) + #P.parts) ^ 2 - #P.parts * (#A / #P.parts + 1) ^ 2 ≤
    (#P.parts * (#A / #P.parts) + #P.parts) ^ 2

Tactic:
exact Nat.sub_le _ _

Result:
no goals

Proof state:
case calc_1
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ∑ UV ∈ P.sparsePairs G ε, ↑(#(G.interedges UV.1 UV.2)) ≤ ∑ UV ∈ P.sparsePairs G ε, ε * (↑(#UV.1) * ↑(#UV.2))

Tactic:
gcongr with UV hUV

Result:
case calc_1.h
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
UV : Finset α × Finset α
hUV : UV ∈ P.sparsePairs G ε
⊢ ↑(#(G.interedges UV.1 UV.2)) ≤ ε * (↑(#UV.1) * ↑(#UV.2))
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma mem_stabilizer_set_iff_smul_set_subset {s : Set α} (hs : s.Finite) :
    a ∈ stabilizer G s ↔ a • s ⊆ s

Proof state:
case intro
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ a ∈ stabilizer G ↑s ↔ a • ↑s ⊆ ↑s

Tactic:
classical
rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_smul_finset_subset, ← Finset.coe_smul_finset,
  Finset.coe_subset]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
hs : s.Finite
⊢ a ∈ stabilizer G s ↔ a • s ⊆ s

Tactic:
lift s to Finset α using hs

Result:
case intro
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ a ∈ stabilizer G ↑s ↔ a • ↑s ⊆ ↑s

Proof state:
case intro
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ a ∈ stabilizer G ↑s ↔ a • ↑s ⊆ ↑s

Tactic:
rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_smul_finset_subset, ← Finset.coe_smul_finset,
  Finset.coe_subset]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem FactorSet.coe_add {a b : Multiset { a : Associates α // Irreducible a }} :
    (↑(a + b) : FactorSet α) = a + b

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ ↑(a + b) = ↑a + ↑b

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Geometry/Euclidean/Inversion/Basic.lean
theorem dist_inversion_inversion (hx : x ≠ c) (hy : y ≠ c) (R : ℝ) :
    dist (inversion c R x) (inversion c R y) = R ^ 2 / (dist x c * dist y c) * dist x y

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist ((R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c) ((R / dist y c) ^ 2 • (y -ᵥ c) +ᵥ c) =
    R ^ 2 / (dist x c * dist y c) * dist x y

Tactic:
simp_rw [dist_vadd_cancel_right, dist_eq_norm_vsub V _ c]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist ((R / ‖x -ᵥ c‖) ^ 2 • (x -ᵥ c)) ((R / ‖y -ᵥ c‖) ^ 2 • (y -ᵥ c)) = R ^ 2 / (‖x -ᵥ c‖ * ‖y -ᵥ c‖) * dist x y

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist ((R / ‖x -ᵥ c‖) ^ 2 • (x -ᵥ c)) ((R / ‖y -ᵥ c‖) ^ 2 • (y -ᵥ c)) = R ^ 2 / (‖x -ᵥ c‖ * ‖y -ᵥ c‖) * dist x y

Tactic:
simpa only [dist_vsub_cancel_right] using
  dist_div_norm_sq_smul (vsub_ne_zero.2 hx) (vsub_ne_zero.2 hy) R

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist (inversion c R x) (inversion c R y) = R ^ 2 / (dist x c * dist y c) * dist x y

Tactic:
dsimp only [inversion]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist ((R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c) ((R / dist y c) ^ 2 • (y -ᵥ c) +ᵥ c) =
    R ^ 2 / (dist x c * dist y c) * dist x y
-- Mathlib/ModelTheory/Definability.lean
theorem empty_definable_iff :
    (∅ : Set M).Definable L s ↔ ∃ φ : L.Formula α, s = setOf φ.Realize

Proof state:
M : Type w
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ φ, s = setOf φ.Realize) ↔ ∃ b, s = setOf ((LEquiv.addEmptyConstants L ↑∅).onFormula.symm b).Realize

Tactic:
simp

Result:
no goals

Proof state:
M : Type w
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ ∅.Definable L s ↔ ∃ φ, s = setOf φ.Realize

Tactic:
rw [Definable, Equiv.exists_congr_left (LEquiv.addEmptyConstants L (∅ : Set M)).onFormula]

Result:
M : Type w
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ φ, s = setOf φ.Realize) ↔ ∃ b, s = setOf ((LEquiv.addEmptyConstants L ↑∅).onFormula.symm b).Realize
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem sFinite_of_absolutelyContinuous {ν : Measure α} [SFinite ν] (hμν : μ ≪ ν) :
    SFinite μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
⊢ SFinite (μ.restrict (μ.sigmaFiniteSetWRT ν) + ⊤ • ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ)

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
⊢ SFinite μ

Tactic:
rw [← Measure.restrict_add_restrict_compl (μ := μ) measurableSet_sigmaFiniteSetWRT,
  restrict_compl_sigmaFiniteSetWRT hμν]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
⊢ SFinite (μ.restrict (μ.sigmaFiniteSetWRT ν) + ⊤ • ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ)
-- Mathlib/Probability/Kernel/WithDensity.lean
nonrec lemma withDensity_absolutelyContinuous [IsSFiniteKernel κ]
    (f : α → β → ℝ≥0∞) (a : α) :
    Kernel.withDensity κ f a ≪ κ a

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : Measurable (Function.uncurry f)
⊢ (κ a).withDensity (f a) ≪ κ a

Tactic:
exact withDensity_absolutelyContinuous _ _

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : ¬Measurable (Function.uncurry f)
⊢ (κ.withDensity f) a ≪ κ a

Tactic:
rw [withDensity_of_not_measurable _ hf]

Result:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : ¬Measurable (Function.uncurry f)
⊢ 0 a ≪ κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
⊢ (κ.withDensity f) a ≪ κ a

Tactic:
by_cases hf : Measurable (Function.uncurry f)

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : Measurable (Function.uncurry f)
⊢ (κ.withDensity f) a ≪ κ a

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : ¬Measurable (Function.uncurry f)
⊢ (κ.withDensity f) a ≪ κ a

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : Measurable (Function.uncurry f)
⊢ (κ.withDensity f) a ≪ κ a

Tactic:
rw [Kernel.withDensity_apply _ hf]

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : Measurable (Function.uncurry f)
⊢ (κ a).withDensity (f a) ≪ κ a

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : ¬Measurable (Function.uncurry f)
⊢ 0 a ≪ κ a

Tactic:
simp [Measure.AbsolutelyContinuous.zero]

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem FG.sup {N₁ N₂ : Submodule R M} (hN₁ : N₁.FG) (hN₂ : N₂.FG) : (N₁ ⊔ N₂).FG :=
  let ⟨t₁, ht₁⟩ := fg_def.1 hN₁
  let ⟨t₂, ht₂⟩ := fg_def.1 hN₂
  fg_def.2 ⟨t₁ ∪ t₂, ht₁.1.union ht₂.1, by rw [span_union, ht₁.2, ht₂.2]⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N₁ N₂ : Submodule R M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite ∧ span R t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite ∧ span R t₂ = N₂
⊢ span R (t₁ ∪ t₂) = N₁ ⊔ N₂

Tactic:
rw [span_union, ht₁.2, ht₂.2]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
lemma nil_iff_support_eq {p : G.Walk v w} : p.Nil ↔ p.support = [v]

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.Nil ↔ p.support = [v]

Tactic:
cases p <;> simp

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem jacobson_pi_le : jacobson R (Π i, M i) ≤ Submodule.pi Set.univ (jacobson R <| M ·)

Proof state:
R : Type u_1
inst✝² : Ring R
ι : Type u_7
M : ι → Type u_6
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ ∀ (i : ι) (i_1 : ↑{m | IsCoatom m}), ⨅ a, ↑a ≤ comap (LinearMap.proj i) ↑i_1

Tactic:
intro i m

Result:
R : Type u_1
inst✝² : Ring R
ι : Type u_7
M : ι → Type u_6
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
m : ↑{m | IsCoatom m}
⊢ ⨅ a, ↑a ≤ comap (LinearMap.proj i) ↑m

Proof state:
R : Type u_1
inst✝² : Ring R
ι : Type u_7
M : ι → Type u_6
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
m : ↑{m | IsCoatom m}
⊢ ⨅ a, ↑a ≤ comap (LinearMap.proj i) ↑m

Tactic:
exact iInf_le_of_le ⟨_, (isCoatom_comap_iff <| LinearMap.proj_surjective i).mpr m.2⟩ le_rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Ring R
ι : Type u_7
M : ι → Type u_6
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ jacobson R ((i : ι) → M i) ≤ pi Set.univ fun x => jacobson R (M x)

Tactic:
simp_rw [← iInf_comap_proj, jacobson, sInf_eq_iInf', comap_iInf, le_iInf_iff]

Result:
R : Type u_1
inst✝² : Ring R
ι : Type u_7
M : ι → Type u_6
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ ∀ (i : ι) (i_1 : ↑{m | IsCoatom m}), ⨅ a, ↑a ≤ comap (LinearMap.proj i) ↑i_1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1) = - x.sign

Proof state:
case H.h
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 0 ≤ ↑x / 2

case H
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ≠ 0

case H
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ∣ ↑1 + 1

t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ≠ 0

t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ∣ 1 + 1

Tactic:
exact Int.le.intro_sub _ rfl

Result:
case H
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ≠ 0

case H
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ∣ ↑1 + 1

t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ≠ 0

t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x✝¹ : Nat
w : 1 < -[x✝¹+1].natAbs
x : Nat
x✝ : 1 < -[x + 1+1].natAbs
⊢ 2 ∣ 1 + 1

Proof state:
x : Int
w : 1 < x.natAbs
⊢ x.bmod (x.natAbs + 1) = -x.sign

Tactic:
have t₁ : ∀ (x : Nat), x % (x + 2) = x :=
  fun x => Nat.mod_eq_of_lt (Nat.lt_succ_of_lt (Nat.lt.base x))

Result:
x : Int
w : 1 < x.natAbs
t₁ : ∀ (x : Nat), x % (x + 2) = x
⊢ x.bmod (x.natAbs + 1) = -x.sign

Proof state:
case negSucc.a
t₁ : ∀ (x : Nat), x % (x + 2) = x
t₂ : ∀ (x : Int), 0 ≤ x → x % (x + 2) = x
x : Nat
w : 1 < -[x+1].natAbs
⊢ 0 ≤ ↑x

Tactic:
exact ofNat_nonneg x

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma counitForward_naturality₁ {G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (η : F ⟶ G)
    (s : (CostructuredArrow yoneda A)ᵒᵖ) (x : F.obj s) : counitForward G s.unop (η.app s x) =
      OverArrows.map₁ (counitForward F s.unop x) (yonedaCollectionPresheafMap₁ η) (by aesop_cat) :=
  OverArrows.ext <| YonedaCollection.ext (by simp) (by simp)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
s : (CostructuredArrow yoneda A)ᵒᵖ
x : F.obj s
⊢ YonedaCollection.fst (counitForward G (unop s) (η.app s x)).val =
    YonedaCollection.fst ((counitForward F (unop s) x).map₁ (yonedaCollectionPresheafMap₁ η) ⋯).val

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
s : (CostructuredArrow yoneda A)ᵒᵖ
x : F.obj s
⊢ yonedaCollectionPresheafMap₁ η ≫ yonedaCollectionPresheafToA G = yonedaCollectionPresheafToA F

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
s : (CostructuredArrow yoneda A)ᵒᵖ
x : F.obj s
⊢ G.map (eqToHom ⋯) (YonedaCollection.snd ((counitForward F (unop s) x).map₁ (yonedaCollectionPresheafMap₁ η) ⋯).val) =
    YonedaCollection.snd (counitForward G (unop s) (η.app s x)).val

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Take.lean
theorem take_take {m n' : ℕ} (h : m ≤ n') (h' : n' ≤ n) (v : (i : Fin n) → α i) :
    take m h (take n' h' v) = take m (Nat.le_trans h h') v

Proof state:
case h
n : ℕ
α : Fin n → Sort u_1
m n' : ℕ
h : m ≤ n'
h' : n' ≤ n
v : (i : Fin n) → α i
i : Fin m
⊢ take m h (take n' h' v) i = take m ⋯ v i

Tactic:
simp only [take]

Result:
case h
n : ℕ
α : Fin n → Sort u_1
m n' : ℕ
h : m ≤ n'
h' : n' ≤ n
v : (i : Fin n) → α i
i : Fin m
⊢ v (castLE h' (castLE h i)) = v (castLE ⋯ i)

Proof state:
n : ℕ
α : Fin n → Sort u_1
m n' : ℕ
h : m ≤ n'
h' : n' ≤ n
v : (i : Fin n) → α i
⊢ take m h (take n' h' v) = take m ⋯ v

Tactic:
ext i

Result:
case h
n : ℕ
α : Fin n → Sort u_1
m n' : ℕ
h : m ≤ n'
h' : n' ≤ n
v : (i : Fin n) → α i
i : Fin m
⊢ take m h (take n' h' v) i = take m ⋯ v i

Proof state:
case h
n : ℕ
α : Fin n → Sort u_1
m n' : ℕ
h : m ≤ n'
h' : n' ≤ n
v : (i : Fin n) → α i
i : Fin m
⊢ v (castLE h' (castLE h i)) = v (castLE ⋯ i)

Tactic:
congr

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem inf_subgroupOf_left (H K : Subgroup G) : (K ⊓ H).subgroupOf K = H.subgroupOf K

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (K ⊓ H).subgroupOf K = H.subgroupOf K

Tactic:
rw [inf_comm, inf_subgroupOf_right]

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
theorem BddBelow.bddAbove_image2_of_bddAbove :
    BddBelow s → BddAbove t → BddAbove (Set.image2 f s t)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddBelow s → BddAbove t → BddAbove (image2 f s t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Result:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (image2 f s t)

Proof state:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (image2 f s t)

Tactic:
exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha hb⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_C_mul_X (x : R) (n : ℕ) : coeff (C x * X : R[X]) n = if n = 1 then x else 0

Proof state:
R : Type u
inst✝ : Semiring R
x : R
n : ℕ
⊢ (C x * X).coeff n = if n = 1 then x else 0

Tactic:
rw [← pow_one X, coeff_C_mul_X_pow]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Covering.lean
theorem Prefunctor.IsCovering.of_comp_left (hφ : φ.IsCovering) (hφψ : (φ ⋙q ψ).IsCovering)
    (φsur : Surjective φ.obj) : ψ.IsCovering

Proof state:
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
⊢ ψ.IsCovering

Tactic:
refine ⟨fun v => ?_, fun v => ?_⟩ <;> obtain ⟨u, rfl⟩ := φsur v

Result:
case refine_1.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
u : U
⊢ Bijective (ψ.star (φ.obj u))

case refine_2.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
u : U
⊢ Bijective (ψ.costar (φ.obj u))

Proof state:
case refine_1.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
u : U
⊢ Bijective (ψ.star (φ.obj u))

case refine_2.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
u : U
⊢ Bijective (ψ.costar (φ.obj u))

Tactic:
exacts [(Bijective.of_comp_iff _ (hφ.star_bijective u)).mp (hφψ.star_bijective u),
  (Bijective.of_comp_iff _ (hφ.costar_bijective u)).mp (hφψ.costar_bijective u)]

Result:
no goals