harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Icc_succ_left : Icc a.succ b = Ioc a b

Proof state:
case h
a b x : ℕ
⊢ x ∈ Icc a.succ b ↔ x ∈ Ioc a b

Tactic:
rw [mem_Icc, mem_Ioc, succ_le_iff]

Result:
no goals

Proof state:
a b : ℕ
⊢ Icc a.succ b = Ioc a b

Tactic:
ext x

Result:
case h
a b x : ℕ
⊢ x ∈ Icc a.succ b ↔ x ∈ Ioc a b
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem eval_intCast_map {R S : Type*} [Ring R] [Ring S] (f : R →+* S) (p : R[X]) (i : ℤ) :
    (p.map f).eval (i : S) = f (p.eval i)

Proof state:
case h_monomial
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
i : ℤ
n : ℕ
r : R
⊢ eval (↑i) (map f ((monomial n) r)) = f (eval (↑i) ((monomial n) r))

Tactic:
simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]

Result:
no goals

Proof state:
case h_add
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
i : ℤ
p q : R[X]
hp : eval (↑i) (map f p) = f (eval (↑i) p)
hq : eval (↑i) (map f q) = f (eval (↑i) q)
⊢ eval (↑i) (map f (p + q)) = f (eval (↑i) (p + q))

Tactic:
simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
p : R[X]
i : ℤ
⊢ eval (↑i) (map f p) = f (eval (↑i) p)

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q hp hq =>
  simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
| h_monomial n r =>
  simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_union_add_inter (s : Set α) (ht : MeasurableSet t) :
    μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
ht : MeasurableSet t
⊢ μ t + μ (s \ t) + μ (s ∩ t) = μ (s ∩ t) + μ (s \ t) + μ t

Tactic:
ac_rfl

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
ht : MeasurableSet t
⊢ μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

Tactic:
rw [← measure_inter_add_diff (s ∪ t) ht, Set.union_inter_cancel_right, union_diff_right, ←
  measure_inter_add_diff s ht]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
ht : MeasurableSet t
⊢ μ t + μ (s \ t) + μ (s ∩ t) = μ (s ∩ t) + μ (s \ t) + μ t
-- Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
lemma _root_.RootSystem.rootForm_anisotropic (P : RootSystem ι R M N) :
    P.RootForm.toQuadraticMap.Anisotropic :=
  fun x ↦ P.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero <| by
    simpa only [rootSpan, P.span_root_eq_top] using Submodule.mem_top

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : LinearOrderedCommRing R
inst✝¹ : Module R M
inst✝ : Module R N
P : RootSystem ι R M N
x : M
⊢ x ∈ P.rootSpan

Tactic:
simpa only [rootSpan, P.span_root_eq_top] using Submodule.mem_top

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_mul_dvd (x y : RatFunc K) : num (x * y) ∣ num x * num y

Proof state:
case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : x = 0
⊢ (x * y).num ∣ x.num * y.num

Tactic:
simp [hx]

Result:
no goals

Proof state:
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).num ∣ x.num * y.num

Tactic:
rw [num_dvd (mul_ne_zero (num_ne_zero hx) (num_ne_zero hy))]

Result:
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : ¬y = 0
⊢ ∃ q, q ≠ 0 ∧ x * y = (algebraMap K[X] (RatFunc K)) (x.num * y.num) / (algebraMap K[X] (RatFunc K)) q

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ (x * y).num ∣ x.num * y.num

Tactic:
by_cases hx : x = 0

Result:
case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : x = 0
⊢ (x * y).num ∣ x.num * y.num

case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
⊢ (x * y).num ∣ x.num * y.num

Proof state:
case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : y = 0
⊢ (x * y).num ∣ x.num * y.num

Tactic:
simp [hy]

Result:
no goals

Proof state:
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
⊢ (x * y).num ∣ x.num * y.num

Tactic:
by_cases hy : y = 0

Result:
case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : y = 0
⊢ (x * y).num ∣ x.num * y.num

case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).num ∣ x.num * y.num

Proof state:
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : ¬y = 0
⊢ x * y = (algebraMap K[X] (RatFunc K)) (x.num * y.num) / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)

Tactic:
rw [RingHom.map_mul, RingHom.map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]

Result:
no goals

Proof state:
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : ¬y = 0
⊢ ∃ q, q ≠ 0 ∧ x * y = (algebraMap K[X] (RatFunc K)) (x.num * y.num) / (algebraMap K[X] (RatFunc K)) q

Tactic:
refine ⟨x.denom * y.denom, mul_ne_zero (denom_ne_zero x) (denom_ne_zero y), ?_⟩

Result:
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : ¬y = 0
⊢ x * y = (algebraMap K[X] (RatFunc K)) (x.num * y.num) / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)
-- Mathlib/Algebra/Star/Pointwise.lean
theorem star_inv' [DivisionSemiring α] [StarRing α] (s : Set α) : s⁻¹⋆ = s⋆⁻¹

Proof state:
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : StarRing α
s : Set α
⊢ s⁻¹⋆ = s⋆⁻¹

Tactic:
ext

Result:
case h
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : StarRing α
s : Set α
x✝ : α
⊢ x✝ ∈ s⁻¹⋆ ↔ x✝ ∈ s⋆⁻¹

Proof state:
case h
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : StarRing α
s : Set α
x✝ : α
⊢ x✝ ∈ s⁻¹⋆ ↔ x✝ ∈ s⋆⁻¹

Tactic:
simp only [mem_star, mem_inv, star_inv₀]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean
lemma surjective_eq_topologically :
    @Surjective = topologically Function.Surjective

Proof state:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ Surjective x✝ ↔ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective) x✝

Tactic:
exact surjective_iff _

Result:
no goals

Proof state:
⊢ @Surjective = topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective

Tactic:
ext

Result:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ Surjective x✝ ↔ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective) x✝
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_of_eqOn_one (hf : s.EqOn f 1) : ∏ᶠ i ∈ s, f i = 1

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hf : EqOn f 1 s
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ s), 1

Tactic:
exact finprod_mem_congr rfl hf

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hf : EqOn f 1 s
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = 1

Tactic:
rw [← finprod_mem_one s]

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hf : EqOn f 1 s
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ s), 1
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
/-- For `‖z‖ ≤ 1/2`, the complex logarithm is bounded by `(3/2) * ‖z‖`. -/
lemma norm_log_one_add_half_le_self {z : ℂ} (hz : ‖z‖ ≤ 1/2) : ‖(log (1 + z))‖ ≤ (3/2) * ‖z‖

Proof state:
case hab.h₁
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖z‖ * ‖z‖ ≤ ‖z‖ * (1 / 2)

Tactic:
apply mul_le_mul (by simp only [mul_one, le_refl])
  (by simpa only [one_div] using hz) (norm_nonneg z) (by simp only [mul_one, norm_nonneg])

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hz4 : ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2 * 2 / 2
⊢ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖

Tactic:
simp only [isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
  IsUnit.div_mul_cancel] at hz4

Result:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hz4 : ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2
⊢ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖

Proof state:
case hab.c0
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ 0 ≤ 1 - ‖z‖

Tactic:
linarith

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ ‖log (1 + z)‖ ≤ 3 / 2 * ‖z‖

Tactic:
apply le_trans (norm_log_one_add_le (lt_of_le_of_lt hz one_half_lt_one))

Result:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖

Proof state:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ 1 ≤ 2 * (1 - ‖z‖)

Tactic:
linarith

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hz4 : ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2
⊢ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖

Tactic:
linarith

Result:
no goals

Proof state:
case hab.c0
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ 0 ≤ (1 - ‖z‖)⁻¹

Tactic:
rw [inv_nonneg]

Result:
case hab.c0
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ 0 ≤ 1 - ‖z‖

Proof state:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2 * 2 / 2

Tactic:
gcongr

Result:
case hab.c0
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ 0 ≤ (1 - ‖z‖)⁻¹

case hab.h₁
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖z‖ ^ 2 ≤ ‖z‖ / 2

Proof state:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖z‖ ≤ ‖z‖

Tactic:
simp only [mul_one, le_refl]

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ 0 < 1 - ‖z‖

Tactic:
linarith

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ 0 ≤ ‖z‖

Tactic:
simp only [mul_one, norm_nonneg]

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ (1 - ‖z‖)⁻¹ ≤ 2

Tactic:
rw [inv_eq_one_div, div_le_iff₀]

Result:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ 1 ≤ 2 * (1 - ‖z‖)

z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ 0 < 1 - ‖z‖

Proof state:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖z‖ ≤ 1 / 2

Tactic:
simpa only [one_div] using hz

Result:
no goals

Proof state:
case hab.h₁
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖z‖ ^ 2 ≤ ‖z‖ / 2

Tactic:
rw [sq, div_eq_mul_one_div]

Result:
case hab.h₁
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖z‖ * ‖z‖ ≤ ‖z‖ * (1 / 2)
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem mersenne_coe_X (p : ℕ) : (mersenne p : X (q p)) = 0

Proof state:
case h₁
p : ℕ
⊢ (2 ^ p - 1).minFac ∣ 2 ^ p - 1

Tactic:
apply Nat.minFac_dvd

Result:
no goals

Proof state:
p : ℕ
⊢ ↑(mersenne p) = 0

Tactic:
ext <;> simp [mersenne, q, ZMod.natCast_zmod_eq_zero_iff_dvd, -pow_pos]

Result:
case h₁
p : ℕ
⊢ (2 ^ p - 1).minFac ∣ 2 ^ p - 1
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
theorem IsPerfectMatching.even_card [Fintype V] (h : M.IsPerfectMatching) :
    Even (Fintype.card V)

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype V
h : M.IsPerfectMatching
⊢ Even (Fintype.card V)

Tactic:
simpa only [h.2.card_verts] using IsMatching.even_card h.1

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype V
h : M.IsPerfectMatching
⊢ Even (Fintype.card V)

Tactic:
classical
simpa only [h.2.card_verts] using IsMatching.even_card h.1

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem prod_pow_pos_of_zero_not_mem_support {f : ℕ →₀ ℕ} (nhf : 0 ∉ f.support) :
    0 < f.prod (· ^ ·) :=
  Nat.pos_iff_ne_zero.mpr <| Finset.prod_ne_zero_iff.mpr fun _ hf =>
    pow_ne_zero _ fun H => by subst H; exact nhf hf

Proof state:
f : ℕ →₀ ℕ
nhf : 0 ∉ f.support
hf : 0 ∈ f.support
⊢ False

Tactic:
exact nhf hf

Result:
no goals

Proof state:
f : ℕ →₀ ℕ
nhf : 0 ∉ f.support
x✝ : ℕ
hf : x✝ ∈ f.support
H : x✝ = 0
⊢ False

Tactic:
subst H

Result:
f : ℕ →₀ ℕ
nhf : 0 ∉ f.support
hf : 0 ∈ f.support
⊢ False
-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem has_fpower_series_iterate_dslope_fslope (n : ℕ) (hp : HasFPowerSeriesAt f p z₀) :
    HasFPowerSeriesAt ((swap dslope z₀)^[n] f) (fslope^[n] p) z₀

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
z₀ : 𝕜
n : ℕ
ih :
  ∀ {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E},
    HasFPowerSeriesAt f p z₀ → HasFPowerSeriesAt ((swap dslope z₀)^[n] f) (fslope^[n] p) z₀
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
hp : HasFPowerSeriesAt f p z₀
⊢ HasFPowerSeriesAt ((swap dslope z₀)^[n + 1] f) (fslope^[n + 1] p) z₀

Tactic:
simpa using ih (has_fpower_series_dslope_fslope hp)

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
hp : HasFPowerSeriesAt f p z₀
⊢ HasFPowerSeriesAt ((swap dslope z₀)^[0] f) (fslope^[0] p) z₀

Tactic:
exact hp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
hp : HasFPowerSeriesAt f p z₀
⊢ HasFPowerSeriesAt ((swap dslope z₀)^[n] f) (fslope^[n] p) z₀

Tactic:
induction n generalizing f p with
| zero => exact hp
| succ n ih => simpa using ih (has_fpower_series_dslope_fslope hp)

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_pow_le {m n : ℕ} [Fact (1 < n)] {a : ZMod n} : (a ^ m).val ≤ a.val ^ m

Proof state:
m n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
⊢ (a ^ m).val ≤ a.val ^ m

Tactic:
induction m with
| zero => simp [ZMod.val_one]
| succ m ih =>
  rw [pow_succ, pow_succ]
  apply le_trans (ZMod.val_mul_le _ _)
  apply Nat.mul_le_mul_right _ ih

Result:
no goals

Proof state:
case zero
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
⊢ (a ^ 0).val ≤ a.val ^ 0

Tactic:
simp [ZMod.val_one]

Result:
no goals

Proof state:
case succ
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ m).val * a.val ≤ a.val ^ m * a.val

Tactic:
apply Nat.mul_le_mul_right _ ih

Result:
no goals

Proof state:
case succ
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ m * a).val ≤ a.val ^ m * a.val

Tactic:
apply le_trans (ZMod.val_mul_le _ _)

Result:
case succ
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ m).val * a.val ≤ a.val ^ m * a.val

Proof state:
case succ
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ (m + 1)).val ≤ a.val ^ (m + 1)

Tactic:
rw [pow_succ, pow_succ]

Result:
case succ
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ m * a).val ≤ a.val ^ m * a.val
-- Mathlib/Data/Set/Lattice.lean
theorem image2_iInter_subset_right (s : Set α) (t : ι → Set β) :
    image2 f s (⋂ i, t i) ⊆ ⋂ i, image2 f s (t i)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ ∀ x ∈ s, ∀ (y : β), (∀ (i : ι), y ∈ t i) → ∀ (i : ι), f x y ∈ image2 f s (t i)

Tactic:
exact fun x hx y hy i => mem_image2_of_mem hx (hy _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ image2 f s (⋂ i, t i) ⊆ ⋂ i, image2 f s (t i)

Tactic:
simp_rw [image2_subset_iff, mem_iInter]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ ∀ x ∈ s, ∀ (y : β), (∀ (i : ι), y ∈ t i) → ∀ (i : ι), f x y ∈ image2 f s (t i)
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
lemma _root_.MeasurableEmbedding.sigmaFinite_map {f : α → β} (hf : MeasurableEmbedding f)
    [SigmaFinite μ] :
    SigmaFinite (μ.map f)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
⊢ ⋃ i, (fun n => f '' spanningSets μ n ∪ (range f)ᶜ) i = univ

Tactic:
rw [← Set.iUnion_union, ← Set.image_iUnion, iUnion_spanningSets,
  Set.image_univ, Set.union_compl_self]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
⊢ ∀ (i : ℕ), (fun n => f '' spanningSets μ n ∪ (range f)ᶜ) i ∈ univ

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
n : ℕ
⊢ μ (f ⁻¹' (f '' spanningSets μ n) ∪ f ⁻¹' (range f)ᶜ) < ⊤

Tactic:
simp only [Set.preimage_compl, Set.preimage_range, Set.compl_univ, Set.union_empty,
  Set.preimage_image_eq _ hf.injective]

Result:
case refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
n : ℕ
⊢ μ (spanningSets μ n) < ⊤

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
n : ℕ
⊢ (Measure.map f μ) ((fun n => f '' spanningSets μ n ∪ (range f)ᶜ) n) < ⊤

Tactic:
rw [hf.map_apply, Set.preimage_union]

Result:
case refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
n : ℕ
⊢ μ (f ⁻¹' (f '' spanningSets μ n) ∪ f ⁻¹' (range f)ᶜ) < ⊤

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
n : ℕ
⊢ μ (spanningSets μ n) < ⊤

Tactic:
exact measure_spanningSets_lt_top μ n

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
⊢ SigmaFinite (Measure.map f μ)

Tactic:
refine ⟨fun n ↦ f '' (spanningSets μ n) ∪ (Set.range f)ᶜ, by simp, fun n ↦ ?_, ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
n : ℕ
⊢ (Measure.map f μ) ((fun n => f '' spanningSets μ n ∪ (range f)ᶜ) n) < ⊤

case refine_2
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
⊢ ⋃ i, (fun n => f '' spanningSets μ n ∪ (range f)ᶜ) i = univ
-- Mathlib/Order/WithBot.lean
theorem _root_.IsMin.withTop (h : IsMin a) : IsMin (a : WithTop α) :=
  fun x ↦ by cases x <;> simp; simpa using @h _

Proof state:
α : Type u_1
a : α
inst✝ : LE α
h : IsMin a
x : WithTop α
⊢ x ≤ ↑a → ↑a ≤ x

Tactic:
cases x <;> simp

Result:
case coe
α : Type u_1
a : α
inst✝ : LE α
h : IsMin a
a✝ : α
⊢ a✝ ≤ a → a ≤ a✝

Proof state:
case coe
α : Type u_1
a : α
inst✝ : LE α
h : IsMin a
a✝ : α
⊢ a✝ ≤ a → a ≤ a✝

Tactic:
simpa using @h _

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem mem_congr [@TransCmp α cmp] {t : RBNode α} (h : cmp x y = .eq) :
    Mem cmp x t ↔ Mem cmp y t

Proof state:
α : Type u_1
cmp : α → α → Ordering
x y : α
inst✝ : TransCmp cmp
t : RBNode α
h : cmp x y = Ordering.eq
⊢ Mem cmp x t ↔ Mem cmp y t

Tactic:
simp [Mem, TransCmp.cmp_congr_left' h]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_zero_right (x : V) : o.oangle x 0 = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ o.oangle x 0 = 0

Tactic:
simp [oangle]

Result:
no goals
-- Mathlib/Data/Finsupp/AList.lean
theorem toAList_keys_toFinset [DecidableEq α] (f : α →₀ M) :
    f.toAList.keys.toFinset = f.support

Proof state:
case h
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a✝ : α
⊢ a✝ ∈ f.toAList.keys.toFinset ↔ a✝ ∈ f.support

Tactic:
simp [toAList, AList.mem_keys, AList.keys, List.keys]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ f.toAList.keys.toFinset = f.support

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a✝ : α
⊢ a✝ ∈ f.toAList.keys.toFinset ↔ a✝ ∈ f.support
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem mem_range'_1 : m ∈ range' s n ↔ s ≤ m ∧ m < s + n

Proof state:
s n m : Nat
⊢ m ∈ range' s n ↔ s ≤ m ∧ m < s + n

Tactic:
simp [mem_range']

Result:
s n m : Nat
⊢ (∃ i, i < n ∧ m = s + i) ↔ s ≤ m ∧ m < s + n

Proof state:
s n m : Nat
⊢ (∃ i, i < n ∧ m = s + i) ↔ s ≤ m ∧ m < s + n

Tactic:
exact ⟨
fun ⟨i, h, e⟩ => e ▸ ⟨Nat.le_add_right .., Nat.add_lt_add_left h _⟩,
fun ⟨h₁, h₂⟩ => ⟨m - s, Nat.sub_lt_left_of_lt_add h₁ h₂, (Nat.add_sub_cancel' h₁).symm⟩⟩

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem sum_eq : (∑ i : Fin n, d * (2 * d + 1) ^ (i : ℕ)) = ((2 * d + 1) ^ n - 1) / 2

Proof state:
n d : ℕ
⊢ (2 * d + 1) ^ n - 1 = (∑ i : Fin n, d * (2 * d + 1) ^ ↑i) * 2

Tactic:
rw [← sum_range fun i => d * (2 * d + 1) ^ (i : ℕ), ← mul_sum, mul_right_comm, mul_comm d, ←
  geom_sum_mul_add, add_tsub_cancel_right, mul_comm]

Result:
no goals

Proof state:
n d : ℕ
⊢ ∑ i : Fin n, d * (2 * d + 1) ^ ↑i = ((2 * d + 1) ^ n - 1) / 2

Tactic:
refine (Nat.div_eq_of_eq_mul_left zero_lt_two ?_).symm

Result:
n d : ℕ
⊢ (2 * d + 1) ^ n - 1 = (∑ i : Fin n, d * (2 * d + 1) ^ ↑i) * 2
-- Mathlib/Order/Interval/Set/OrderIso.lean
theorem image_Ioo (e : α ≃o β) (a b : α) : e '' Ioo a b = Ioo (e a) (e b)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ ⇑e '' Ioo a b = Ioo (e a) (e b)

Tactic:
rw [e.image_eq_preimage, e.symm.preimage_Ioo, e.symm_symm]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
lemma not_boundaryGE_next [e.IsRelIff] {j k : ι} (hk : c.Rel j k) :
    ¬ e.BoundaryGE k

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hk : c.Rel j k
⊢ c'.Rel (c'.prev (e.f k)) (e.f k) → ∃ x, c'.Rel (e.f x) (e.f k)

Tactic:
intro

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hk : c.Rel j k
a✝ : c'.Rel (c'.prev (e.f k)) (e.f k)
⊢ ∃ x, c'.Rel (e.f x) (e.f k)

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hk : c.Rel j k
a✝ : c'.Rel (c'.prev (e.f k)) (e.f k)
⊢ ∃ x, c'.Rel (e.f x) (e.f k)

Tactic:
exact ⟨j, by simpa only [e.rel_iff] using hk⟩

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hk : c.Rel j k
a✝ : c'.Rel (c'.prev (e.f k)) (e.f k)
⊢ c'.Rel (e.f j) (e.f k)

Tactic:
simpa only [e.rel_iff] using hk

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hk : c.Rel j k
⊢ ¬(c'.Rel (c'.prev (e.f k)) (e.f k) ∧ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f k))

Tactic:
simp only [not_and, not_forall, not_not]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hk : c.Rel j k
⊢ c'.Rel (c'.prev (e.f k)) (e.f k) → ∃ x, c'.Rel (e.f x) (e.f k)

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hk : c.Rel j k
⊢ ¬e.BoundaryGE k

Tactic:
dsimp [BoundaryGE]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hk : c.Rel j k
⊢ ¬(c'.Rel (c'.prev (e.f k)) (e.f k) ∧ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f k))