harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem mod_opow_log_lt_self (b : Ordinal) {o : Ordinal} (ho : o ≠ 0) : o % (b ^ log b o) < o

Proof state:
b o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o % b ^ log b o < o

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Result:
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o % 0 ^ log 0 o < o

case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : b ≠ 0
⊢ o % b ^ log b o < o

Proof state:
case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : b ≠ 0
⊢ o % b ^ log b o < o

Tactic:
exact (mod_lt _ <| opow_ne_zero _ hb).trans_le (opow_log_le_self _ ho)

Result:
no goals

Proof state:
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o % 0 ^ log 0 o < o

Tactic:
simpa using Ordinal.pos_iff_ne_zero.2 ho

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem comap_exp_cobounded : comap exp (cobounded ℂ) = comap re atTop :=
  calc
    comap exp (cobounded ℂ) = comap re (comap Real.exp atTop)

Proof state:
⊢ comap re (comap Real.exp atTop) = comap re atTop

Tactic:
rw [Real.comap_exp_atTop]

Result:
no goals

Proof state:
⊢ comap cexp (cobounded ℂ) = comap re (comap Real.exp atTop)

Tactic:
simp only [← comap_norm_atTop, comap_comap, comp_def, norm_exp]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_add_left (d) :
    (∫ x in a..b, f (d + x)) = ∫ x in d + a..d + b, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d + x) = ∫ (x : ℝ) in d + a..d + b, f x

Tactic:
simpa only [add_comm d] using integral_comp_add_right f d

Result:
no goals
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem Multiset.trop_sum [AddCommMonoid R] (s : Multiset R) :
    trop s.sum = Multiset.prod (s.map trop) :=
  Quotient.inductionOn s (by simpa using List.trop_sum)

Proof state:
R : Type u_1
inst✝ : AddCommMonoid R
s : Multiset R
⊢ ∀ (a : List R), trop (sum ⟦a⟧) = (map trop ⟦a⟧).prod

Tactic:
simpa using List.trop_sum

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem range_aleph : range aleph = Set.Ici ℵ₀

Proof state:
⊢ range ⇑ℵ_ = Ici ℵ₀

Tactic:
ext c

Result:
case h
c : Cardinal.{u_1}
⊢ c ∈ range ⇑ℵ_ ↔ c ∈ Ici ℵ₀

Proof state:
case h
c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ ω ≤ preAleph.symm c

Tactic:
rwa [← aleph0_le_preAleph, preAleph.apply_symm_apply]

Result:
no goals

Proof state:
case h
c : Cardinal.{u_1}
⊢ c ∈ range ⇑ℵ_ ↔ c ∈ Ici ℵ₀

Tactic:
refine ⟨fun ⟨o, e⟩ => e ▸ aleph0_le_aleph _, fun hc ↦ ⟨preAleph.symm c - ω, ?_⟩⟩

Result:
case h
c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ ℵ_ (preAleph.symm c - ω) = c

Proof state:
case h
c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ ℵ_ (preAleph.symm c - ω) = c

Tactic:
rw [aleph_eq_preAleph, Ordinal.add_sub_cancel_of_le, preAleph.apply_symm_apply]

Result:
case h
c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ ω ≤ preAleph.symm c
-- Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean
theorem uniqueMDiffOn_iff_uniqueDiffOn : UniqueMDiffOn 𝓘(𝕜, E) s ↔ UniqueDiffOn 𝕜 s

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ UniqueMDiffOn 𝓘(𝕜, E) s ↔ UniqueDiffOn 𝕜 s

Tactic:
simp [UniqueMDiffOn, UniqueDiffOn, uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem List.nnnorm_prod_le' {l : List α} (hl : l ≠ []) : ‖l.prod‖₊ ≤ (l.map nnnorm).prod :=
  (List.norm_prod_le' hl).trans_eq <| by simp [NNReal.coe_list_prod, List.map_map]

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
l : List α
hl : l ≠ []
⊢ (map norm l).prod = (fun a => ↑a) (map nnnorm l).prod

Tactic:
simp [NNReal.coe_list_prod, List.map_map]

Result:
no goals
-- Mathlib/Data/Matrix/PEquiv.lean
theorem toMatrix_refl [DecidableEq n] [Zero α] [One α] :
    ((PEquiv.refl n).toMatrix : Matrix n n α) = 1

Proof state:
case a
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i✝ j✝ : n
⊢ (PEquiv.refl n).toMatrix i✝ j✝ = 1 i✝ j✝

Tactic:
simp [toMatrix_apply, one_apply]

Result:
no goals

Proof state:
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
⊢ (PEquiv.refl n).toMatrix = 1

Tactic:
ext

Result:
case a
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i✝ j✝ : n
⊢ (PEquiv.refl n).toMatrix i✝ j✝ = 1 i✝ j✝
-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJ_0_of_three_ne_zero (h3 : (3 : F) ≠ 0) : ofJ 0 = ofJ0 F

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h3 : 3 ≠ 0
⊢ ofJ 0 = ofJ0 F

Tactic:
rw [ofJ, if_pos rfl, if_neg h3]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem measureUnivNNReal_eq_zero [IsFiniteMeasure μ] : measureUnivNNReal μ = 0 ↔ μ = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ measureUnivNNReal μ = 0 ↔ ↑(measureUnivNNReal μ) = 0

Tactic:
norm_cast

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ measureUnivNNReal μ = 0 ↔ μ = 0

Tactic:
rw [← MeasureTheory.Measure.measure_univ_eq_zero, ← coe_measureUnivNNReal]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ measureUnivNNReal μ = 0 ↔ ↑(measureUnivNNReal μ) = 0
-- Mathlib/Topology/PartialHomeomorph.lean
theorem ofSet_trans {s : Set X} (hs : IsOpen s) : (ofSet s hs).trans e = e.restr s :=
  PartialHomeomorph.ext _ _ (fun _ => rfl) (fun _ => rfl) <| by simp [hs.interior_eq, inter_comm]

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
hs : IsOpen s
⊢ ((ofSet s hs).trans e).source = (e.restr s).source

Tactic:
simp [hs.interior_eq, inter_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_dirac' {a : α} {f : α → ℝ≥0∞} (hf : Measurable f) {s : Set α}
    (hs : MeasurableSet s) [Decidable (a ∈ s)] :
    ∫⁻ x in s, f x ∂Measure.dirac a = if a ∈ s then f a else 0

Proof state:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∉ s
⊢ ∫⁻ (x : α), f x ∂0 = 0

Tactic:
exact lintegral_zero_measure _

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0

Tactic:
split_ifs

Result:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∈ s
⊢ ∫⁻ (x : α), f x ∂dirac a = f a

case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∉ s
⊢ ∫⁻ (x : α), f x ∂0 = 0

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ ∫⁻ (x : α) in s, f x ∂dirac a = if a ∈ s then f a else 0

Tactic:
rw [restrict_dirac' hs]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0

Proof state:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∈ s
⊢ ∫⁻ (x : α), f x ∂dirac a = f a

Tactic:
exact lintegral_dirac' _ hf

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma IsAntichain.le_infSum (h𝒜 : IsAntichain (· ⊆ ·) (𝒜 : Set (Finset α))) (h𝒜₀ : ∅ ∉ 𝒜) :
    ∑ s ∈ 𝒜, ((card α).choose #s : ℚ)⁻¹ ≤ infSum 𝒜

Proof state:
case ha
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
h𝒜₀ : ∅ ∉ 𝒜
s : Finset α
hs : s ∈ 𝒜
⊢ ↑(#s) ≠ 0

Tactic:
have := (nonempty_iff_ne_empty.2 <| ne_of_mem_of_not_mem hs h𝒜₀).card_pos

Result:
case ha
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
h𝒜₀ : ∅ ∉ 𝒜
s : Finset α
hs : s ∈ 𝒜
this : 0 < #s
⊢ ↑(#s) ≠ 0

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
h𝒜₀ : ∅ ∉ 𝒜
⊢ ∑ s ∈ 𝒜, (↑((card α).choose #s))⁻¹ ≤ infSum 𝒜

Tactic:
calc
  _ = ∑ s ∈ 𝒜, #(truncatedInf 𝒜 s) / (#s * (card α).choose #s : ℚ) := ?_
  _ ≤ _ := sum_le_univ_sum_of_nonneg fun s ↦ by positivity

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
h𝒜₀ : ∅ ∉ 𝒜
⊢ ∑ s ∈ 𝒜, (↑((card α).choose #s))⁻¹ = ∑ s ∈ 𝒜, ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
h𝒜₀ : ∅ ∉ 𝒜
s : Finset α
⊢ 0 ≤ ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
h𝒜₀ : ∅ ∉ 𝒜
s : Finset α
hs : s ∈ 𝒜
⊢ (↑((card α).choose #s))⁻¹ = ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))

Tactic:
rw [truncatedInf_of_isAntichain h𝒜 hs, div_mul_cancel_left₀]

Result:
case ha
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
h𝒜₀ : ∅ ∉ 𝒜
s : Finset α
hs : s ∈ 𝒜
⊢ ↑(#s) ≠ 0

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
h𝒜₀ : ∅ ∉ 𝒜
⊢ ∑ s ∈ 𝒜, (↑((card α).choose #s))⁻¹ = ∑ s ∈ 𝒜, ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))

Tactic:
refine sum_congr rfl fun s hs ↦ ?_

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
h𝒜₀ : ∅ ∉ 𝒜
s : Finset α
hs : s ∈ 𝒜
⊢ (↑((card α).choose #s))⁻¹ = ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))

Proof state:
case ha
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
h𝒜₀ : ∅ ∉ 𝒜
s : Finset α
hs : s ∈ 𝒜
this : 0 < #s
⊢ ↑(#s) ≠ 0

Tactic:
positivity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mkVector_succ' : mkVector (n + 1) a = (#v[a] ++ mkVector n a).cast (by omega)

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ mkVector (n + 1) a = Vector.cast ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ mkVector n a)

Tactic:
rw [← toArray_inj]

Result:
n : Nat
α✝ : Type u_1
a : α✝
⊢ (mkVector (n + 1) a).toArray = (Vector.cast ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ mkVector n a)).toArray

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ (mkVector (n + 1) a).toArray = (Vector.cast ⋯ ({ toArray := #[a], size_toArray := ⋯ } ++ mkVector n a)).toArray

Tactic:
simp [Array.mkArray_succ']

Result:
no goals

Proof state:
n : Nat
a : ?m.339173
⊢ 1 + n = n + 1

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
    a ∈ m → m.getKey? a = some (m.getKeyD a fallback)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a fallback : α
⊢ a ∈ m → m.getKey? a = some (m.getKeyD a fallback)

Tactic:
simpa [mem_iff_contains] using getKey?_eq_some_getKeyD_of_contains h

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem Convex.lipschitzWith_gauge {r : ℝ≥0} (hc : Convex ℝ s) (hr : 0 < r)
    (hs : Metric.ball (0 : E) r ⊆ s) : LipschitzWith r⁻¹ (gauge s) :=
  have : Absorbent ℝ (Metric.ball (0 : E) r) := absorbent_ball_zero hr
  LipschitzWith.of_le_add_mul _ fun x y =>
    calc
      gauge s x = gauge s (y + (x - y))

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : ball 0 ↑r ⊆ s
this : Absorbent ℝ (ball 0 ↑r)
x y : E
⊢ gauge s x = gauge s (y + (x - y))

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : ball 0 ↑r ⊆ s
this : Absorbent ℝ (ball 0 ↑r)
x y : E
⊢ gauge s y + ‖x - y‖ / ↑r = gauge s y + ↑r⁻¹ * dist x y

Tactic:
rw [dist_eq_norm, div_eq_inv_mul, NNReal.coe_inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem PUnit.subsingleton (a b : PUnit) : a = b

Proof state:
case unit
b : PUnit
⊢ unit = b

Tactic:
cases b

Result:
case unit.unit

⊢ unit = unit

Proof state:
case unit.unit

⊢ unit = unit

Tactic:
exact rfl

Result:
no goals

Proof state:
a b : PUnit
⊢ a = b

Tactic:
cases a

Result:
case unit
b : PUnit
⊢ unit = b
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma Nontrivial.pow (hs : s.Nontrivial) : ∀ {n}, n ≠ 0 → (s ^ n).Nontrivial
  | 1, _ => by simpa
  | n + 2, _ => by simpa [pow_succ] using (hs.pow n.succ_ne_zero).mul hs

Proof state:
α : Type u_2
inst✝ : CancelMonoid α
s : Set α
hs : s.Nontrivial
x✝ : 1 ≠ 0
⊢ (s ^ 1).Nontrivial

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CancelMonoid α
s : Set α
hs : s.Nontrivial
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (s ^ (n + 2)).Nontrivial

Tactic:
simpa [pow_succ] using (hs.pow n.succ_ne_zero).mul hs

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem ball_add_ball (hε : 0 < ε) (hδ : 0 < δ) (a b : E) :
    ball a ε + ball b δ = ball (a + b) (ε + δ)

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
a b : E
⊢ Metric.ball a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)

Tactic:
rw [ball_add, thickening_ball hε hδ b, Metric.vadd_ball, vadd_eq_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem map_snd_zip :
    ∀ (l₁ : List α) (l₂ : List β), l₂.length ≤ l₁.length → map Prod.snd (zip l₁ l₂) = l₂
  | _, [], _ => by
    rw [zip_nil_right]
    rfl
  | [], b :: bs, h => by simp at h
  | a :: as, b :: bs, h => by
    simp [Nat.succ_le_succ_iff] at h
    show _ :: map Prod.snd (zip as bs) = _ :: bs
    rw [map_snd_zip as bs h]

Proof state:
α : Type u_1
β : Type u_2
b : β
bs : List β
h : (b :: bs).length ≤ [].length
⊢ map Prod.snd ([].zip (b :: bs)) = b :: bs

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
as : List α
b : β
bs : List β
h : bs.length ≤ as.length
⊢ (a, b).snd :: map Prod.snd (as.zip bs) = b :: bs

Tactic:
rw [map_snd_zip as bs h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
x✝¹ : List α
x✝ : [].length ≤ x✝¹.length
⊢ map Prod.snd [] = []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
as : List α
b : β
bs : List β
h : bs.length ≤ as.length
⊢ map Prod.snd ((a :: as).zip (b :: bs)) = b :: bs

Tactic:
show _ :: map Prod.snd (zip as bs) = _ :: bs

Result:
α : Type u_1
β : Type u_2
a : α
as : List α
b : β
bs : List β
h : bs.length ≤ as.length
⊢ (a, b).snd :: map Prod.snd (as.zip bs) = b :: bs

Proof state:
α : Type u_1
β : Type u_2
x✝¹ : List α
x✝ : [].length ≤ x✝¹.length
⊢ map Prod.snd (x✝¹.zip []) = []

Tactic:
rw [zip_nil_right]

Result:
α : Type u_1
β : Type u_2
x✝¹ : List α
x✝ : [].length ≤ x✝¹.length
⊢ map Prod.snd [] = []

Proof state:
α : Type u_1
β : Type u_2
a : α
as : List α
b : β
bs : List β
h : (b :: bs).length ≤ (a :: as).length
⊢ map Prod.snd ((a :: as).zip (b :: bs)) = b :: bs

Tactic:
simp [Nat.succ_le_succ_iff] at h

Result:
α : Type u_1
β : Type u_2
a : α
as : List α
b : β
bs : List β
h : bs.length ≤ as.length
⊢ map Prod.snd ((a :: as).zip (b :: bs)) = b :: bs
-- Mathlib/Algebra/Ring/Subsemiring/Defs.lean
theorem natCast_mem [AddSubmonoidWithOneClass S R] (n : ℕ) : (n : R) ∈ s

Proof state:
S : Type u_1
R : Type u_2
inst✝² : AddMonoidWithOne R
inst✝¹ : SetLike S R
s : S
inst✝ : AddSubmonoidWithOneClass S R
n : ℕ
⊢ ↑n ∈ s

Tactic:
induction n <;> simp [zero_mem, add_mem, one_mem, *]

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem map_noncommProd [MonoidHomClass F α β] (s : Multiset α) (comm) (f : F) :
    f (s.noncommProd comm) = (s.map f).noncommProd (Multiset.map_noncommProd_aux s comm f)

Proof state:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
⊢ f (s.noncommProd comm) = (map (⇑f) s).noncommProd ⋯

Tactic:
induction s using Quotient.inductionOn

Result:
case h
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
⊢ f (noncommProd ⟦a✝⟧ comm) = (map ⇑f ⟦a✝⟧).noncommProd ⋯

Proof state:
case h
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
⊢ f (noncommProd ⟦a✝⟧ comm) = (map ⇑f ⟦a✝⟧).noncommProd ⋯

Tactic:
simpa using map_list_prod f _

Result:
no goals
-- Mathlib/RingTheory/Localization/NumDen.lean
theorem mk'_num_den' (x : K) : algebraMap A K (num A x) / algebraMap A K (den A x) = x

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
⊢ (algebraMap A K) (num A x) / (algebraMap A K) ↑(den A x) = x

Tactic:
rw [← mk'_eq_div]

Result:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
⊢ mk' K (num A x) (den A x) = x

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
⊢ mk' K (num A x) (den A x) = x

Tactic:
apply mk'_num_den

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Properties.lean
theorem isSymm_iff_flip : B.IsSymm ↔ flipHom B = B :=
  (forall₂_congr fun _ _ => by exact eq_comm).trans BilinForm.ext_iff.symm

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
x✝¹ x✝ : M
⊢ (RingHom.id R) ((B x✝¹) x✝) = (B x✝) x✝¹ ↔ ((flipHom B) x✝¹) x✝ = (B x✝¹) x✝

Tactic:
exact eq_comm

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem isSheafFor_arrows_iff_pullbacks : (ofArrows X π).IsSheafFor P ↔
    (∀ (x : (i : I) → P.obj (op (X i))), Arrows.PullbackCompatible P π x →
    ∃! t, ∀ i, P.map (π i).op t = x i)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).hasPullbacks
⊢ IsSheafFor P (ofArrows X π) ↔
    ∀ (x : (i : I) → P.obj (op (X i))), Arrows.PullbackCompatible P π x → ∃! t, ∀ (i : I), P.map (π i).op t = x i

Tactic:
simp_rw [← Arrows.pullbackCompatible_iff, isSheafFor_arrows_iff]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma sinKernel_undef (a : UnitAddCircle) {x : ℝ} (hx : x ≤ 0) : sinKernel a x = 0

Proof state:
x : ℝ
hx : x ≤ 0
a : ℝ
⊢ (I * ↑x).im ≤ 0

Tactic:
simpa

Result:
no goals

Proof state:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ sinKernel a x = 0

Tactic:
induction a using QuotientAddGroup.induction_on with
| H a => rw [← ofReal_eq_zero, sinKernel_def, jacobiTheta₂'_undef _ (by simpa), zero_div]

Result:
no goals

Proof state:
case H
x : ℝ
hx : x ≤ 0
a : ℝ
⊢ sinKernel (↑a) x = 0

Tactic:
rw [← ofReal_eq_zero, sinKernel_def, jacobiTheta₂'_undef _ (by simpa), zero_div]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma comp_mk₀_id (α : Ext X Y n) :
    α.comp (mk₀ (𝟙 Y)) (add_zero n) = α

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (α.comp (mk₀ (𝟙 Y)) ⋯).hom = α.hom

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp (mk₀ (𝟙 Y)) ⋯ = α

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (α.comp (mk₀ (𝟙 Y)) ⋯).hom = α.hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
⊢ α.comp (mk₀ (𝟙 Y)) ⋯ = α

Tactic:
letI := HasDerivedCategory.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp (mk₀ (𝟙 Y)) ⋯ = α
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
lemma add'_comm (f₁ f₂ : L.obj X ⟶ L.obj Y) :
    add' W f₁ f₂ = add' W f₂ f₁

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : L.obj X ⟶ L.obj Y
⊢ add' W f₁ f₂ = add' W f₂ f₁

Tactic:
obtain ⟨α, h₁, h₂⟩ := exists_leftFraction₂ L W f₁ f₂

Result:
case intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
⊢ add' W f₁ f₂ = add' W f₂ f₁

Proof state:
case intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
⊢ add' W f₁ f₂ = add' W f₂ f₁

Tactic:
rw [add'_eq W f₁ f₂ α h₁ h₂, add'_eq W f₂ f₁ α.symm h₂ h₁, α.symm_add]

Result:
no goals
-- Mathlib/GroupTheory/Coset/Card.lean
@[to_additive]
lemma card_mul_eq_card_subgroup_mul_card_quotient (s : Subgroup α) (t : Set α) :
    Nat.card (t * s : Set α) = Nat.card s * Nat.card (t.image (↑) : Set (α ⧸ s))

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ Nat.card ↑(t * ↑s) = Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' t)

Tactic:
rw [← Nat.card_prod, Nat.card_congr]

Result:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ↑(t * ↑s) ≃ ↥s × ↑(QuotientGroup.mk '' t)

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ↑(t * ↑s) ≃ ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' t))

Tactic:
rw [QuotientGroup.preimage_image_mk]

Result:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ↑(t * ↑s) ≃ ↑(⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t)

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ↑(t * ↑s) ≃ ↑(⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t)

Tactic:
convert Equiv.refl ↑(t * s)

Result:
case h.e'_2.h.e'_2
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t = t * ↑s

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ↑(t * ↑s) ≃ ↥s × ↑(QuotientGroup.mk '' t)

Tactic:
apply Equiv.trans _ (QuotientGroup.preimageMkEquivSubgroupProdSet _ _)

Result:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ↑(t * ↑s) ≃ ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' t))

Proof state:
case h.e'_2.h.e'_2
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t = t * ↑s

Tactic:
aesop (add simp [Set.mem_mul])

Result:
no goals