harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integrableOn_iUnion_of_summable_integral_norm {f : X → E} {s : ι → Set X}
    (hs : ∀ i : ι, MeasurableSet (s i)) (hi : ∀ i : ι, IntegrableOn f (s i) μ)
    (h : Summable fun i : ι => ∫ x : X in s i, ‖f x‖ ∂μ) : IntegrableOn f (iUnion s) μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
S' : Summable fun i => ⟨∫ (x : X) in s i, ↑‖f x‖₊ ∂μ, ⋯⟩
⊢ ∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f a‖₊ ∂μ) < ⊤

Tactic:
have S'' := ENNReal.tsum_coe_eq S'.hasSum

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
S' : Summable fun i => ⟨∫ (x : X) in s i, ↑‖f x‖₊ ∂μ, ⋯⟩
S'' : ∑' (a : ι), ↑⟨∫ (x : X) in s a, ↑‖f x‖₊ ∂μ, ⋯⟩ = ↑(∑' (b : ι), ⟨∫ (x : X) in s b, ↑‖f x‖₊ ∂μ, ⋯⟩)
⊢ ∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f a‖₊ ∂μ) < ⊤

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
⊢ Summable fun a => ↑⟨∫ (x : X) in s a, ↑‖f x‖₊ ∂μ, ⋯⟩

Tactic:
exact h

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
/-- A nonempty set is scaled by zero to the singleton set containing zero. -/
@[simp] lemma zero_smul_finset {s : Finset β} (h : s.Nonempty) : (0 : α) • s = (0 : Finset β) :=
  coe_injective <| by simpa using @Set.zero_smul_set α _ _ _ _ _ h

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
s : Finset β
h : s.Nonempty
⊢ ↑(0 • s) = ↑0

Tactic:
simpa using @Set.zero_smul_set α _ _ _ _ _ h

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem range_comp_subset_range (f : α → β) (g : β → γ) : range (g ∘ f) ⊆ range g

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ range (g ∘ f) ⊆ range g

Tactic:
rw [range_comp]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ g '' range f ⊆ range g

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ g '' range f ⊆ range g

Tactic:
apply image_subset_range

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem reverse_flatMap {β} (l : Array α) (f : α → Array β) :
    (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f)

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → Array β
⊢ (flatMap f l).reverse = flatMap (reverse ∘ f) l.reverse

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
toList✝ : List α
⊢ (flatMap f { toList := toList✝ }).reverse = flatMap (reverse ∘ f) { toList := toList✝ }.reverse

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
toList✝ : List α
⊢ (flatMap f { toList := toList✝ }).reverse = flatMap (reverse ∘ f) { toList := toList✝ }.reverse

Tactic:
simp [List.reverse_flatMap, Function.comp_def]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/IndicatorFunction.lean
theorem enorm_indicator_le_of_subset (h : s ⊆ t) (f : α → E) (a : α) :
    ‖indicator s f a‖ₑ ≤ ‖indicator t f a‖ₑ

Proof state:
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s t : Set α
h : s ⊆ t
f : α → E
a : α
⊢ s.indicator (fun a => ‖f a‖ₑ) a ≤ t.indicator (fun a => ‖f a‖ₑ) a

Tactic:
apply indicator_le_indicator_of_subset ‹_› (zero_le _)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s t : Set α
h : s ⊆ t
f : α → E
a : α
⊢ ‖s.indicator f a‖ₑ ≤ ‖t.indicator f a‖ₑ

Tactic:
simp only [enorm_indicator_eq_indicator_enorm]

Result:
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s t : Set α
h : s ⊆ t
f : α → E
a : α
⊢ s.indicator (fun a => ‖f a‖ₑ) a ≤ t.indicator (fun a => ‖f a‖ₑ) a
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem Δ_of_isCharThreeJNeZeroNF_of_char_three : W.Δ = -W.a₂ ^ 3 * W.a₆

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ -64 * W.a₂ ^ 3 * W.a₆ - 432 * W.a₆ ^ 2 = -W.a₂ ^ 3 * W.a₆

Tactic:
linear_combination (-21 * W.a₂ ^ 3 * W.a₆ - 144 * W.a₆ ^ 2) * CharP.cast_eq_zero R 3

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ W.Δ = -W.a₂ ^ 3 * W.a₆

Tactic:
rw [Δ_of_isCharThreeJNeZeroNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ -64 * W.a₂ ^ 3 * W.a₆ - 432 * W.a₆ ^ 2 = -W.a₂ ^ 3 * W.a₆
-- Mathlib/LinearAlgebra/Matrix/Trace.lean
theorem trace_mul_cycle' [NonUnitalCommSemiring R] (A : Matrix m n R) (B : Matrix n p R)
    (C : Matrix p m R) : trace (A * (B * C)) = trace (C * (A * B))

Proof state:
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
⊢ (A * (B * C)).trace = (C * (A * B)).trace

Tactic:
rw [← Matrix.mul_assoc, trace_mul_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma equation_zero : W'.Equation ![0, 1, 0]

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ W'.Equation ![0, 1, 0]

Tactic:
simp only [equation_of_Z_eq_zero, fin3_def_ext, zero_pow three_ne_zero]

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma changeLevel_one {d : ℕ} (h : d ∣ n) :
    changeLevel h (1 : DirichletCharacter R d) = 1

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n d : ℕ
h : d ∣ n
⊢ (changeLevel h) 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/BorelCantelli.lean
theorem iIndepFun.indep_comap_natural_of_lt (hf : ∀ i, StronglyMeasurable (f i))
    (hfi : iIndepFun (fun _ => mβ) f μ) (hij : i < j) :
    Indep (MeasurableSpace.comap (f j) mβ) (Filtration.natural f hf i) μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (fun x => mβ) f μ
hij : i < j
⊢ Indep (⨆ k ∈ {j}, MeasurableSpace.comap (f k) mβ) (⨆ k ∈ {k | k ≤ i}, MeasurableSpace.comap (f k) mβ) μ

Tactic:
exact indep_iSup_of_disjoint (fun k => (hf k).measurable.comap_le) hfi (by simpa)

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (fun x => mβ) f μ
hij : i < j
⊢ Disjoint {j} {k | k ≤ i}

Tactic:
simpa

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (fun x => mβ) f μ
hij : i < j
⊢ Indep (MeasurableSpace.comap (f j) mβ) (↑(Filtration.natural f hf) i) μ

Tactic:
suffices Indep (⨆ k ∈ ({j} : Set ι), MeasurableSpace.comap (f k) mβ)
    (⨆ k ∈ {k | k ≤ i}, MeasurableSpace.comap (f k) mβ) μ by rwa [iSup_singleton] at this

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (fun x => mβ) f μ
hij : i < j
⊢ Indep (⨆ k ∈ {j}, MeasurableSpace.comap (f k) mβ) (⨆ k ∈ {k | k ≤ i}, MeasurableSpace.comap (f k) mβ) μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun (fun x => mβ) f μ
hij : i < j
this : Indep (⨆ k ∈ {j}, MeasurableSpace.comap (f k) mβ) (⨆ k ∈ {k | k ≤ i}, MeasurableSpace.comap (f k) mβ) μ
⊢ Indep (MeasurableSpace.comap (f j) mβ) (↑(Filtration.natural f hf) i) μ

Tactic:
rwa [iSup_singleton] at this

Result:
no goals
-- Mathlib/Order/Radical.lean
theorem OrderIso.map_radical (f : α ≃o β) : f (Order.radical α) = Order.radical β

Proof state:
case e
α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ α ≃ β

Tactic:
exact f.toEquiv

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ f (Order.radical α) = Order.radical β

Tactic:
unfold Order.radical

Result:
α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ f (⨅ a ∈ {H | IsCoatom H}, a) = ⨅ a ∈ {H | IsCoatom H}, a

Proof state:
case h
α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ ∀ (x : α), ⨅ (_ : f.toEquiv x ∈ {H | IsCoatom H}), f.toEquiv x = ⨅ (_ : x ∈ {H | IsCoatom H}), f x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ ⨅ i ∈ {H | IsCoatom H}, f i = ⨅ a ∈ {H | IsCoatom H}, a

Tactic:
fapply Equiv.iInf_congr

Result:
case e
α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ α ≃ β

case h
α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ ∀ (x : α), ⨅ (_ : ?e x ∈ {H | IsCoatom H}), ?e x = ⨅ (_ : x ∈ {H | IsCoatom H}), f x

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ f (⨅ a ∈ {H | IsCoatom H}, a) = ⨅ a ∈ {H | IsCoatom H}, a

Tactic:
simp only [OrderIso.map_iInf]

Result:
α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ ⨅ i ∈ {H | IsCoatom H}, f i = ⨅ a ∈ {H | IsCoatom H}, a
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_negY (P : Fin 3 → R) : (W'.map f).toJacobian.negY (f ∘ P) = f (W'.negY P)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ -(⇑f ∘ P) y - (map W' f).toJacobian.a₁ * (⇑f ∘ P) x * (⇑f ∘ P) z - (map W' f).toJacobian.a₃ * (⇑f ∘ P) z ^ 3 =
    f (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)

Tactic:
map_simp

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (map W' f).toJacobian.negY (⇑f ∘ P) = f (W'.negY P)

Tactic:
simp only [negY]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ -(⇑f ∘ P) y - (map W' f).toJacobian.a₁ * (⇑f ∘ P) x * (⇑f ∘ P) z - (map W' f).toJacobian.a₃ * (⇑f ∘ P) z ^ 3 =
    f (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)
-- Mathlib/Data/Finsupp/Single.lean
theorem mem_support_single (a a' : α) (b : M) : a ∈ (single a' b).support ↔ a = a' ∧ b ≠ 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
⊢ a ∈ (single a' b).support ↔ a = a' ∧ b ≠ 0

Tactic:
simp [single_apply_eq_zero, not_or]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_spec (x) (y : S) : f.mk' x y * f.toMap y = f.toMap x :=
  show _ * _ * _ = _ by rw [mul_assoc, mul_comm _ (f.toMap y), ← mul_assoc, mul_inv_left, mul_comm]

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ f.toMap x * ↑((IsUnit.liftRight (f.toMap.restrict S) ⋯) y)⁻¹ * f.toMap ↑y = f.toMap x

Tactic:
rw [mul_assoc, mul_comm _ (f.toMap y), ← mul_assoc, mul_inv_left, mul_comm]

Result:
no goals
-- Mathlib/Control/Traversable/Instances.lean
theorem traverse_append :
    ∀ as bs : List α', traverse f (as ++ bs) = (· ++ ·) <$> traverse f as <*> traverse f bs
  | [], bs => by simp [functor_norm]
  | a :: as, bs => by simp [traverse_append as bs, functor_norm]; congr

Proof state:
F : Type u → Type u
inst✝¹ : Applicative F
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ traverse f (a :: as ++ bs) = (fun x1 x2 => x1 ++ x2) <$> traverse f (a :: as) <*> traverse f bs

Tactic:
simp [traverse_append as bs, functor_norm]

Result:
F : Type u → Type u
inst✝¹ : Applicative F
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ (fun a => (Function.comp fun x2 => a :: x2) ∘ fun x1 x2 => x1 ++ x2) <$> f a <*> traverse f as <*> traverse f bs =
    (fun a => (fun x1 x2 => x1 ++ x2) ∘ fun x2 => a :: x2) <$> f a <*> traverse f as <*> traverse f bs

Proof state:
F : Type u → Type u
inst✝¹ : Applicative F
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
bs : List α'
⊢ traverse f ([] ++ bs) = (fun x1 x2 => x1 ++ x2) <$> traverse f [] <*> traverse f bs

Tactic:
simp [functor_norm]

Result:
no goals

Proof state:
F : Type u → Type u
inst✝¹ : Applicative F
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ (fun a => (Function.comp fun x2 => a :: x2) ∘ fun x1 x2 => x1 ++ x2) <$> f a <*> traverse f as <*> traverse f bs =
    (fun a => (fun x1 x2 => x1 ++ x2) ∘ fun x2 => a :: x2) <$> f a <*> traverse f as <*> traverse f bs

Tactic:
congr

Result:
no goals
-- Mathlib/Algebra/FreeMonoid/Count.lean
lemma countP_of (x : α) : (of x).countP p =
    if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (if decide (p x) = true then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0) =
    if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0

Tactic:
simp only [decide_eq_true_eq]

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (countP p) (of x) = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0

Tactic:
rw [countP_apply, toList_of, List.countP_singleton, apply_ite (Multiplicative.ofAdd)]

Result:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (if decide (p x) = true then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0) =
    if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_append (f : α → β) (l₁ l₂ : Array α) :
    map f (l₁ ++ l₂) = map f l₁ ++ map f l₂

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : α → β
toList✝¹ toList✝ : List α
⊢ map f ({ toList := toList✝¹ } ++ { toList := toList✝ }) = map f { toList := toList✝¹ } ++ map f { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ : Array α
⊢ map f (l₁ ++ l₂) = map f l₁ ++ map f l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
l₂ : Array α
toList✝ : List α
⊢ map f ({ toList := toList✝ } ++ l₂) = map f { toList := toList✝ } ++ map f l₂

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
l₂ : Array α
toList✝ : List α
⊢ map f ({ toList := toList✝ } ++ l₂) = map f { toList := toList✝ } ++ map f l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : α → β
toList✝¹ toList✝ : List α
⊢ map f ({ toList := toList✝¹ } ++ { toList := toList✝ }) = map f { toList := toList✝¹ } ++ map f { toList := toList✝ }
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lTensor_comp_map (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    (g'.lTensor _).comp (map f g) = map f (g'.comp g)

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R Q
inst✝¹ : Module R S
inst✝ : Module R P
g' : Q →ₗ[R] S
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ lTensor P g' ∘ₗ map f g = map f (g' ∘ₗ g)

Tactic:
simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem conj_eq_iff_re {z : ℂ} : conj z = z ↔ (z.re : ℂ) = z :=
  conj_eq_iff_real.trans ⟨by rintro ⟨r, rfl⟩; simp [ofReal], fun h => ⟨_, h.symm⟩⟩

Proof state:
z : ℂ
⊢ (∃ r, z = ↑r) → ↑z.re = z

Tactic:
rintro ⟨r, rfl⟩

Result:
case intro
r : ℝ
⊢ ↑(↑r).re = ↑r

Proof state:
case intro
r : ℝ
⊢ ↑(↑r).re = ↑r

Tactic:
simp [ofReal]

Result:
no goals
-- Mathlib/Topology/StoneCech.lean
theorem stoneCech_hom_ext {g₁ g₂ : StoneCech α → β} (h₁ : Continuous g₁) (h₂ : Continuous g₂)
    (h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit) : g₁ = g₂

Proof state:
α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : StoneCech α → β
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
⊢ g₁ = g₂

Tactic:
apply h₁.ext_on denseRange_stoneCechUnit h₂

Result:
α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : StoneCech α → β
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
⊢ EqOn g₁ g₂ (range stoneCechUnit)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : StoneCech α → β
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
⊢ EqOn g₁ g₂ (range stoneCechUnit)

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case intro
α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : StoneCech α → β
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
x : α
⊢ g₁ (stoneCechUnit x) = g₂ (stoneCechUnit x)

Proof state:
case intro
α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : StoneCech α → β
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
x : α
⊢ g₁ (stoneCechUnit x) = g₂ (stoneCechUnit x)

Tactic:
exact congr_fun h x

Result:
no goals
-- Mathlib/Algebra/Prime/Lemmas.lean
theorem pow_injective_of_not_isUnit [CancelCommMonoidWithZero M] {q : M} (hq : ¬IsUnit q)
    (hq' : q ≠ 0) : Function.Injective fun n : ℕ => q ^ n

Proof state:
case refine_2
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ q ^ m = q ^ n * q ^ (m - n)

Tactic:
exact (pow_mul_pow_sub q h.le).symm

Result:
no goals

Proof state:
case refine_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ ¬IsUnit (q ^ (m - n))

Tactic:
exact not_isUnit_of_not_isUnit_dvd hq (dvd_pow (dvd_refl _) (Nat.sub_pos_of_lt h).ne')

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
⊢ Function.Injective fun n => q ^ n

Tactic:
refine injective_of_lt_imp_ne fun n m h => DvdNotUnit.ne ⟨pow_ne_zero n hq', q ^ (m - n), ?_, ?_⟩

Result:
case refine_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ ¬IsUnit (q ^ (m - n))

case refine_2
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ q ^ m = q ^ n * q ^ (m - n)
-- Mathlib/Order/Iterate.lean
theorem id_le_iterate_of_id_le (h : id ≤ f) (n : ℕ) : id ≤ f^[n]

Proof state:
α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
⊢ id ≤ f^[n]

Tactic:
simpa only [iterate_id] using monotone_id.iterate_le_of_le h n

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem _root_.is_const_of_deriv_eq_zero (hf : Differentiable 𝕜 f) (hf' : ∀ x, deriv f x = 0)
    (x y : 𝕜) : f x = f y :=
  is_const_of_fderiv_eq_zero hf (fun z => by ext; simp [← deriv_fderiv, hf']) _ _

Proof state:
case h
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : 𝕜 → G
hf : Differentiable 𝕜 f
hf' : ∀ (x : 𝕜), deriv f x = 0
x y z : 𝕜
⊢ (fderiv 𝕜 f z) 1 = 0 1

Tactic:
simp [← deriv_fderiv, hf']

Result:
no goals

Proof state:
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : 𝕜 → G
hf : Differentiable 𝕜 f
hf' : ∀ (x : 𝕜), deriv f x = 0
x y z : 𝕜
⊢ fderiv 𝕜 f z = 0

Tactic:
ext

Result:
case h
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : 𝕜 → G
hf : Differentiable 𝕜 f
hf' : ∀ (x : 𝕜), deriv f x = 0
x y z : 𝕜
⊢ (fderiv 𝕜 f z) 1 = 0 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_set (p : α → Bool) (l : Array α) (i : Nat) (a : α) (h : i < l.size) :
    (l.set i a).countP p = l.countP p - (if p l[i] then 1 else 0) + (if p a then 1 else 0)

Proof state:
case mk
α : Type u_1
p : α → Bool
i : Nat
a : α
toList✝ : List α
h : i < { toList := toList✝ }.size
⊢ countP p ({ toList := toList✝ }.set i a h) =
    (countP p { toList := toList✝ } - if p { toList := toList✝ }[i] = true then 1 else 0) + if p a = true then 1 else 0

Tactic:
simp [List.countP_set, h]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : Array α
i : Nat
a : α
h : i < l.size
⊢ countP p (l.set i a h) = (countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Bool
i : Nat
a : α
toList✝ : List α
h : i < { toList := toList✝ }.size
⊢ countP p ({ toList := toList✝ }.set i a h) =
    (countP p { toList := toList✝ } - if p { toList := toList✝ }[i] = true then 1 else 0) + if p a = true then 1 else 0