harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Real/Irrational.lean
theorem sub_int (h : Irrational x) (m : ℤ) : Irrational (x - m)

Proof state:
x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (x - ↑m)

Tactic:
simpa only [Rat.cast_intCast] using h.sub_rat m

Result:
no goals
-- Mathlib/Data/Set/Finite/Lattice.lean
theorem Infinite.sUnion {s : Set (Set α)} (hs : s.Infinite) : (⋃₀ s).Infinite

Proof state:
α : Type u
s : Set (Set α)
hs : s.Infinite
⊢ (⋃₀ s).Infinite

Tactic:
rw [sUnion_eq_iUnion]

Result:
α : Type u
s : Set (Set α)
hs : s.Infinite
⊢ (⋃ i, ↑i).Infinite

Proof state:
α : Type u
s : Set (Set α)
hs : s.Infinite
⊢ (⋃ i, ↑i).Infinite

Tactic:
have _ := hs.to_subtype

Result:
α : Type u
s : Set (Set α)
hs : s.Infinite
x✝ : Infinite ↑s
⊢ (⋃ i, ↑i).Infinite

Proof state:
α : Type u
s : Set (Set α)
hs : s.Infinite
x✝ : Infinite ↑s
⊢ (⋃ i, ↑i).Infinite

Tactic:
exact infinite_iUnion Subtype.coe_injective

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_minimal {U : Submodule 𝕜 E} [HasOrthogonalProjection U] (y : E) :
    ‖y - orthogonalProjection U y‖ = ⨅ x : U, ‖y - x‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection U
y : E
⊢ ‖y - ↑((orthogonalProjection U) y)‖ = ⨅ x, ‖y - ↑x‖

Tactic:
rw [norm_eq_iInf_iff_inner_eq_zero _ (Submodule.coe_mem _)]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection U
y : E
⊢ ∀ w ∈ U, ⟪y - ↑((orthogonalProjection U) y), w⟫_𝕜 = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection U
y : E
⊢ ∀ w ∈ U, ⟪y - ↑((orthogonalProjection U) y), w⟫_𝕜 = 0

Tactic:
exact orthogonalProjection_inner_eq_zero _

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem finSepDegree_bot : finSepDegree F (⊥ : IntermediateField F E) = 1

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ finSepDegree F ↥⊥ = 1

Tactic:
rw [finSepDegree_eq_of_equiv _ _ _ (botEquiv F E), finSepDegree_self]

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
lemma UniformConcaveOn.add (hf : UniformConcaveOn s φ f) (hg : UniformConcaveOn s ψ g) :
    UniformConcaveOn s (φ + ψ) (f + g)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConcaveOn s φ f
hg : UniformConcaveOn s ψ g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (f + g) x + b • (f + g) y + a * b * (φ + ψ) ‖x - y‖ ≤ (f + g) (a • x + b • y)

Tactic:
simpa [mul_add, add_add_add_comm] using add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConcaveOn s φ f
hg : UniformConcaveOn s ψ g
⊢ UniformConcaveOn s (φ + ψ) (f + g)

Tactic:
refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConcaveOn s φ f
hg : UniformConcaveOn s ψ g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (f + g) x + b • (f + g) y + a * b * (φ + ψ) ‖x - y‖ ≤ (f + g) (a • x + b • y)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem infix_cons_iff : l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

Proof state:
case mpr.inr
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
hl₁ : l₁ <:+: l₂
⊢ l₁ <:+: a :: l₂

Tactic:
exact infix_cons hl₁

Result:
no goals

Proof state:
case mp.intro.cons.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ t : List α✝
hl₃ : head✝ :: (tail✝ ++ l₁ ++ t) = a :: l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

Tactic:
injection hl₃ with _ hl₄

Result:
case mp.intro.cons.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ t : List α✝
head_eq✝ : head✝ = a
hl₄ : tail✝ ++ l₁ ++ t = l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

Proof state:
case mp.intro.nil.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ t : List α✝
hl₃ : [] ++ l₁ ++ t = a :: l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

Tactic:
exact Or.inl ⟨t, hl₃⟩

Result:
no goals

Proof state:
case mpr.inl
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
h : l₁ <+: a :: l₂
⊢ l₁ <:+: a :: l₂

Tactic:
exact h.isInfix

Result:
no goals

Proof state:
case mp.intro.cons.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ t : List α✝
hl₃ : head✝ :: tail✝ ++ l₁ ++ t = a :: l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

Tactic:
simp only [cons_append] at hl₃

Result:
case mp.intro.cons.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ t : List α✝
hl₃ : head✝ :: (tail✝ ++ l₁ ++ t) = a :: l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

Proof state:
case mp.intro.cons.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ t : List α✝
head_eq✝ : head✝ = a
hl₄ : tail✝ ++ l₁ ++ t = l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

Tactic:
exact Or.inr ⟨_, t, hl₄⟩

Result:
no goals

Proof state:
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

Tactic:
constructor

Result:
case mp
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ <:+: a :: l₂ → l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

case mpr
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂ → l₁ <:+: a :: l₂

Proof state:
case mp
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ <:+: a :: l₂ → l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

Tactic:
rintro ⟨⟨hd, tl⟩, t, hl₃⟩

Result:
case mp.intro.nil.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ t : List α✝
hl₃ : [] ++ l₁ ++ t = a :: l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

case mp.intro.cons.intro
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ t : List α✝
hl₃ : head✝ :: tail✝ ++ l₁ ++ t = a :: l₂
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

Proof state:
case mpr
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂ → l₁ <:+: a :: l₂

Tactic:
rintro (h | hl₁)

Result:
case mpr.inl
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
h : l₁ <+: a :: l₂
⊢ l₁ <:+: a :: l₂

case mpr.inr
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
hl₁ : l₁ <:+: l₂
⊢ l₁ <:+: a :: l₂
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem measure_compl_le_add_of_le_add [IsFiniteMeasure μ] (hs : MeasurableSet s)
    (ht : MeasurableSet t) {ε : ℝ≥0∞} (h : μ s ≤ μ t + ε) : μ tᶜ ≤ μ sᶜ + ε

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ tᶜ ≤ μ sᶜ + ε

Tactic:
rw [measure_compl ht (measure_ne_top μ _), measure_compl hs (measure_ne_top μ _),
  tsub_le_iff_right]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ univ ≤ μ univ - μ s + ε + μ t

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ univ ≤ μ univ - μ s + ε + μ t

Tactic:
calc
  μ univ = μ univ - μ s + μ s := (tsub_add_cancel_of_le <| measure_mono s.subset_univ).symm
  _ ≤ μ univ - μ s + (μ t + ε) := add_le_add_left h _
  _ = _ := by rw [add_right_comm, add_assoc]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ univ - μ s + (μ t + ε) = μ univ - μ s + ε + μ t

Tactic:
rw [add_right_comm, add_assoc]

Result:
no goals
-- Mathlib/Order/JordanHolder.lean
theorem eq_snoc_eraseLast {s : CompositionSeries X} (h : 0 < s.length) :
    s = snoc (eraseLast s) s.last (isMaximal_eraseLast_last h)

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
⊢ s = (eraseLast s).snoc (last s) ⋯

Tactic:
ext x

Result:
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
x : X
⊢ x ∈ s ↔ x ∈ (eraseLast s).snoc (last s) ⋯

Proof state:
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
x : X
⊢ x ∈ s ↔ ¬x = last s ∧ x ∈ s ∨ x = last s

Tactic:
by_cases h : x = s.last <;> simp [*, s.last_mem]

Result:
no goals

Proof state:
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
x : X
⊢ x ∈ s ↔ x ∈ (eraseLast s).snoc (last s) ⋯

Tactic:
simp only [mem_snoc, mem_eraseLast h, ne_eq]

Result:
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
x : X
⊢ x ∈ s ↔ ¬x = last s ∧ x ∈ s ∨ x = last s
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.of_mul_add_left_right (h : IsCoprime x (x * z + y)) : IsCoprime x y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y

Tactic:
exact h.of_add_mul_left_right

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (x * z + y)
⊢ IsCoprime x y

Tactic:
rw [add_comm] at h

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false [BEq α] [EquivBEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α} {k fallback : α}
    (contains_eq_false : containsKey k l = false) (contains_eq_false' : toInsert.contains k = false) :
    getKeyD k (insertListIfNewUnit l toInsert) fallback = fallback

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k fallback : α
contains_eq_false : containsKey k l = false
contains_eq_false' : toInsert.contains k = false
⊢ none.getD fallback = fallback

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k fallback : α
contains_eq_false : containsKey k l = false
contains_eq_false' : toInsert.contains k = false
⊢ getKeyD k (insertListIfNewUnit l toInsert) fallback = fallback

Tactic:
rw [getKeyD_eq_getKey?, getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false
  contains_eq_false contains_eq_false']

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k fallback : α
contains_eq_false : containsKey k l = false
contains_eq_false' : toInsert.contains k = false
⊢ none.getD fallback = fallback
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma toRight_disjSum : (s.disjSum t).toRight = t

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s.disjSum t).toRight = t

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : β
⊢ x ∈ (s.disjSum t).toRight ↔ x ∈ t

Proof state:
case h
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : β
⊢ x ∈ (s.disjSum t).toRight ↔ x ∈ t

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_natCast {n : ℕ} : derivative (n : R[X]) = 0

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative (C ↑n) = 0

Tactic:
exact derivative_C

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative ↑n = 0

Tactic:
rw [← map_natCast C n]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative (C ↑n) = 0
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_eq_iff' (hn : n ≠ 0) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
⊢ ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1

Tactic:
rw [← le_floor_iff' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n),
  Nat.lt_add_one_iff, le_antisymm_iff, and_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem splitInTwo_snd_sorted (l : { l : List α // l.length = n }) (h : Pairwise le l.1) : Pairwise le (splitInTwo l).2.1

Proof state:
α : Type u_1
n : Nat
le : α → α → Prop
l : { l // l.length = n }
h : Pairwise le l.val
⊢ Pairwise le (splitInTwo l).snd.val

Tactic:
rw [splitInTwo_snd]

Result:
α : Type u_1
n : Nat
le : α → α → Prop
l : { l // l.length = n }
h : Pairwise le l.val
⊢ Pairwise le ⟨drop ((n + 1) / 2) l.val, ⋯⟩.val

Proof state:
α : Type u_1
n : Nat
le : α → α → Prop
l : { l // l.length = n }
h : Pairwise le l.val
⊢ Pairwise le ⟨drop ((n + 1) / 2) l.val, ⋯⟩.val

Tactic:
exact h.drop

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
@[gcongr]
lemma arccos_lt_arccos {x y : ℝ} (hx : -1 ≤ x) (hlt : x < y) (hy : y ≤ 1) :
    arccos y < arccos x

Proof state:
x y : ℝ
hx : -1 ≤ x
hlt : x < y
hy : y ≤ 1
⊢ π / 2 - arcsin y < π / 2 - arcsin x

Tactic:
gcongr <;> assumption

Result:
no goals

Proof state:
x y : ℝ
hx : -1 ≤ x
hlt : x < y
hy : y ≤ 1
⊢ arccos y < arccos x

Tactic:
unfold arccos

Result:
x y : ℝ
hx : -1 ≤ x
hlt : x < y
hy : y ≤ 1
⊢ π / 2 - arcsin y < π / 2 - arcsin x
-- Mathlib/Order/TransfiniteIteration.lean
@[simp]
lemma transfiniteIterate_bot [OrderBot J] (i₀ : I) :
    transfiniteIterate φ (⊥ : J) i₀ = i₀

Proof state:
I : Type u
inst✝⁴ : SupSet I
φ : I → I
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : OrderBot J
i₀ : I
⊢ transfiniteIterate φ ⊥ i₀ = i₀

Tactic:
dsimp [transfiniteIterate]

Result:
I : Type u
inst✝⁴ : SupSet I
φ : I → I
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : OrderBot J
i₀ : I
⊢ SuccOrder.limitRecOn ⊥ (fun x x => id) (fun x x g => φ ∘ g) (fun y x h => ⨆ x, h ↑x ⋯) i₀ = i₀

Proof state:
I : Type u
inst✝⁴ : SupSet I
φ : I → I
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : OrderBot J
i₀ : I
⊢ SuccOrder.limitRecOn ⊥ (fun x x => id) (fun x x g => φ ∘ g) (fun y x h => ⨆ x, h ↑x ⋯) i₀ = i₀

Tactic:
simp only [isMin_iff_eq_bot, SuccOrder.limitRecOn_isMin, id_eq]

Result:
no goals
-- Mathlib/Topology/Homotopy/Path.lean
theorem eval_one (F : Homotopy p₀ p₁) : F.eval 1 = p₁

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
⊢ F.eval 1 = p₁

Tactic:
ext t

Result:
case a.h
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : ↑I
⊢ (F.eval 1) t = p₁ t

Proof state:
case a.h
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : ↑I
⊢ (F.eval 1) t = p₁ t

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Option.lean
theorem Equiv.optionCongr_swap {α : Type*} [DecidableEq α] (x y : α) :
    optionCongr (swap x y) = swap (some x) (some y)

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
⊢ a✝ ∈ (optionCongr (swap x y)) (some i) ↔ a✝ ∈ (swap (some x) (some y)) (some i)

Tactic:
by_cases hy : i = y <;> simp [hx, hy, swap_apply_of_ne_of_ne]

Result:
no goals

Proof state:
case H.some.a
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
⊢ a✝ ∈ (optionCongr (swap x y)) (some i) ↔ a✝ ∈ (swap (some x) (some y)) (some i)

Tactic:
by_cases hx : i = x

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : i = x
⊢ a✝ ∈ (optionCongr (swap x y)) (some i) ↔ a✝ ∈ (swap (some x) (some y)) (some i)

case neg
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
⊢ a✝ ∈ (optionCongr (swap x y)) (some i) ↔ a✝ ∈ (swap (some x) (some y)) (some i)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ optionCongr (swap x y) = swap (some x) (some y)

Tactic:
ext (_ | i)

Result:
case H.none.a
α : Type u_1
inst✝ : DecidableEq α
x y a✝ : α
⊢ a✝ ∈ (optionCongr (swap x y)) none ↔ a✝ ∈ (swap (some x) (some y)) none

case H.some.a
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
⊢ a✝ ∈ (optionCongr (swap x y)) (some i) ↔ a✝ ∈ (swap (some x) (some y)) (some i)

Proof state:
case H.none.a
α : Type u_1
inst✝ : DecidableEq α
x y a✝ : α
⊢ a✝ ∈ (optionCongr (swap x y)) none ↔ a✝ ∈ (swap (some x) (some y)) none

Tactic:
simp [swap_apply_of_ne_of_ne]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : i = x
⊢ a✝ ∈ (optionCongr (swap x y)) (some i) ↔ a✝ ∈ (swap (some x) (some y)) (some i)

Tactic:
simp only [hx, optionCongr_apply, Option.map_some', swap_apply_left, Option.mem_def,
       Option.some.injEq]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem coeFn_comp (g : β → γ) (hg : Continuous g) (f : α →ₘ[μ] β) : comp g hg f =ᵐ[μ] g ∘ f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
hg : Continuous g
f : α →ₘ[μ] β
⊢ ↑(comp g hg f) =ᶠ[ae μ] g ∘ ↑f

Tactic:
rw [comp_eq_mk]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
hg : Continuous g
f : α →ₘ[μ] β
⊢ ↑(mk (g ∘ ↑f) ⋯) =ᶠ[ae μ] g ∘ ↑f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
hg : Continuous g
f : α →ₘ[μ] β
⊢ ↑(mk (g ∘ ↑f) ⋯) =ᶠ[ae μ] g ∘ ↑f

Tactic:
apply coeFn_mk

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem le_le_succ_iff : a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ b = a ∨ b = succ a → a ≤ b ∧ b ≤ succ a

Tactic:
rintro (rfl | rfl)

Result:
case inl
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b : α
⊢ b ≤ b ∧ b ≤ succ b

case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
⊢ a ≤ succ a ∧ succ a ≤ succ a

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a

Tactic:
refine
  ⟨fun h =>
    or_iff_not_imp_left.2 fun hba : b ≠ a =>
      h.2.antisymm (succ_le_of_lt <| h.1.lt_of_ne <| hba.symm),
    ?_⟩

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ b = a ∨ b = succ a → a ≤ b ∧ b ≤ succ a

Proof state:
case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
⊢ a ≤ succ a ∧ succ a ≤ succ a

Tactic:
exact ⟨le_succ a, le_rfl⟩

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b : α
⊢ b ≤ b ∧ b ≤ succ b

Tactic:
exact ⟨le_rfl, le_succ b⟩

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem nonempty_Ioc : (Ioc a b).Nonempty ↔ a < b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ (Ioc a b).Nonempty ↔ a < b

Tactic:
rw [← coe_nonempty, coe_Ioc, Set.nonempty_Ioc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) (i : Nat)
    (hi : i < n) : (zipWith f a b)[i] = f a[i] b[i]

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β → γ
i : Nat
hi : i < n
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array β
size_toArray✝ : toArray✝.size = n
⊢ (zipWith f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }
        { toArray := toArray✝, size_toArray := size_toArray✝ })[i] =
    f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }[i]
      { toArray := toArray✝, size_toArray := size_toArray✝ }[i]

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β → γ
b : Vector β n
i : Nat
hi : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (zipWith f { toArray := toArray✝, size_toArray := size_toArray✝ } b)[i] =
    f { toArray := toArray✝, size_toArray := size_toArray✝ }[i] b[i]

Tactic:
cases b

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β → γ
i : Nat
hi : i < n
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array β
size_toArray✝ : toArray✝.size = n
⊢ (zipWith f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }
        { toArray := toArray✝, size_toArray := size_toArray✝ })[i] =
    f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }[i]
      { toArray := toArray✝, size_toArray := size_toArray✝ }[i]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β → γ
a : Vector α n
b : Vector β n
i : Nat
hi : i < n
⊢ (zipWith f a b)[i] = f a[i] b[i]

Tactic:
cases a

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β → γ
b : Vector β n
i : Nat
hi : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (zipWith f { toArray := toArray✝, size_toArray := size_toArray✝ } b)[i] =
    f { toArray := toArray✝, size_toArray := size_toArray✝ }[i] b[i]
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma ΨSq_one : W.ΨSq 1 = 1

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.ΨSq 1 = 1

Tactic:
rw [← Nat.cast_one, ΨSq_ofNat, preΨ'_one, one_pow, one_mul, if_neg Nat.not_even_one]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem sum_apply {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) (b : M₁) :
    (∑ d ∈ t, f d) b = ∑ d ∈ t, f d b

Proof state:
R₁ : Type u_1
R₂ : Type u_2
inst✝⁸ : Semiring R₁
inst✝⁷ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : ContinuousAdd M₂
ι : Type u_9
t : Finset ι
f : ι → M₁ →SL[σ₁₂] M₂
b : M₁
⊢ (∑ d ∈ t, f d) b = ∑ d ∈ t, (f d) b

Tactic:
simp only [coe_sum', Finset.sum_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_prod_real : (μH[2] : Measure (ℝ × ℝ)) = volume

Proof state:
⊢ μH[2] = volume

Tactic:
rw [← (volume_preserving_piFinTwo fun _ => ℝ).map_eq,
  ← (hausdorffMeasure_measurePreserving_piFinTwo (fun _ => ℝ) _).map_eq,
  ← hausdorffMeasure_pi_real, Fintype.card_fin, Nat.cast_two]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_eq_true {l : List α} : l.all p = true ↔ ∀ x, x ∈ l → p x

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ l.all p = true ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
simp only [all_eq, decide_eq_true_eq]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem multiplicity_eq_of_emultiplicity_eq {c d : β}
    (h : emultiplicity a b = emultiplicity c d) : multiplicity a b = multiplicity c d

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : emultiplicity a b = emultiplicity c d
⊢ WithTop.untopD 1 (emultiplicity a b) = WithTop.untopD 1 (emultiplicity c d)

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : emultiplicity a b = emultiplicity c d
⊢ multiplicity a b = multiplicity c d

Tactic:
unfold multiplicity

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : emultiplicity a b = emultiplicity c d
⊢ WithTop.untopD 1 (emultiplicity a b) = WithTop.untopD 1 (emultiplicity c d)
-- Mathlib/Order/BoundedOrder/Monotone.lean
theorem StrictMono.maximal_preimage_top [LinearOrder α] [Preorder β] [OrderTop β] {f : α → β}
    (H : StrictMono f) {a} (h_top : f a = ⊤) (x : α) : x ≤ a :=
  H.maximal_of_maximal_image
    (fun p => by
      rw [h_top]
      exact le_top)
    x

Proof state:
α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : Preorder β
inst✝ : OrderTop β
f : α → β
H : StrictMono f
a : α
h_top : f a = ⊤
x : α
p : β
⊢ p ≤ f a

Tactic:
rw [h_top]

Result:
α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : Preorder β
inst✝ : OrderTop β
f : α → β
H : StrictMono f
a : α
h_top : f a = ⊤
x : α
p : β
⊢ p ≤ ⊤

Proof state:
α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : Preorder β
inst✝ : OrderTop β
f : α → β
H : StrictMono f
a : α
h_top : f a = ⊤
x : α
p : β
⊢ p ≤ ⊤

Tactic:
exact le_top

Result:
no goals