harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem finMeasSupp_iff : f.FinMeasSupp μ ↔ ∀ y, y ≠ 0 → μ (f ⁻¹' {y}) < ∞

Proof state:
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
⊢ μ (⋃ y ∈ filter (fun y => y ≠ 0) f.range, ⇑f ⁻¹' {y}) < ⊤

Tactic:
exact measure_biUnion_lt_top (finite_toSet _) fun y hy ↦ H y (mem_filter.1 hy).2

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
⊢ f.FinMeasSupp μ

Tactic:
rw [finMeasSupp_iff_support, support_eq]

Result:
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
⊢ μ (⋃ y ∈ filter (fun y => y ≠ 0) f.range, ⇑f ⁻¹' {y}) < ⊤

Proof state:
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
⊢ f.FinMeasSupp μ → ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
refine fun h y hy => lt_of_le_of_lt (measure_mono ?_) h

Result:
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
h : f.FinMeasSupp μ
y : β
hy : y ≠ 0
⊢ ⇑f ⁻¹' {y} ⊆ {x | (fun x => f x = 0 x) x}ᶜ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
⊢ f.FinMeasSupp μ ↔ ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
⊢ f.FinMeasSupp μ → ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤

case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
⊢ (∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤) → f.FinMeasSupp μ

Proof state:
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
h : f.FinMeasSupp μ
y : β
hy : y ≠ 0
⊢ ⇑f ⁻¹' {y} ⊆ {x | (fun x => f x = 0 x) x}ᶜ

Tactic:
exact fun x hx (H : f x = 0) => hy <| H ▸ Eq.symm hx

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
⊢ (∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤) → f.FinMeasSupp μ

Tactic:
intro H

Result:
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
⊢ f.FinMeasSupp μ
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem associated_iff_eq {x y : M} : x ~ᵤ y ↔ x = y

Proof state:
case mp.intro
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x : M
c : Mˣ
⊢ x = x * ↑c

Tactic:
rw [units_eq_one c, Units.val_one, mul_one]

Result:
no goals

Proof state:
case mpr
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x : M
⊢ x ~ᵤ x

Tactic:
rfl

Result:
no goals

Proof state:
case mp
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x y : M
⊢ x ~ᵤ y → x = y

Tactic:
rintro ⟨c, rfl⟩

Result:
case mp.intro
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x : M
c : Mˣ
⊢ x = x * ↑c

Proof state:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x y : M
⊢ x ~ᵤ y ↔ x = y

Tactic:
constructor

Result:
case mp
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x y : M
⊢ x ~ᵤ y → x = y

case mpr
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x y : M
⊢ x = y → x ~ᵤ y

Proof state:
case mpr
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x y : M
⊢ x = y → x ~ᵤ y

Tactic:
rintro rfl

Result:
case mpr
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x : M
⊢ x ~ᵤ x
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
lemma eq_image_iff_symm_image_eq (e : α ≃ᵐ β) (s : Set β) (t : Set α) :
    s = e '' t ↔ e.symm '' s = t

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
t : Set α
⊢ s = ⇑e '' t ↔ ⇑e.symm '' s = t

Tactic:
rw [← coe_toEquiv, Equiv.eq_image_iff_symm_image_eq, coe_toEquiv_symm]

Result:
no goals
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem appr_mono (x : ℤ_[p]) : Monotone x.appr

Proof state:
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
h✝ : ¬x - ↑(x.appr n) = 0
⊢ x.appr n ≤ x.appr n + p ^ n * (toZMod (↑(unitCoeff h✝) * ↑p ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs)).val

Tactic:
apply Nat.le_add_right

Result:
no goals

Proof state:
case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ x.appr n ≤
    if hy : x - ↑(x.appr n) = 0 then x.appr n
    else x.appr n + p ^ n * (toZMod (↑(unitCoeff hy) * ↑p ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs)).val

Tactic:
split_ifs

Result:
case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
h✝ : x - ↑(x.appr n) = 0
⊢ x.appr n ≤ x.appr n

case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
h✝ : ¬x - ↑(x.appr n) = 0
⊢ x.appr n ≤ x.appr n + p ^ n * (toZMod (↑(unitCoeff h✝) * ↑p ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs)).val

Proof state:
case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
h✝ : x - ↑(x.appr n) = 0
⊢ x.appr n ≤ x.appr n

Tactic:
rfl

Result:
no goals

Proof state:
case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ x.appr n ≤ x.appr (n + 1)

Tactic:
dsimp [appr]

Result:
case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ x.appr n ≤
    if hy : x - ↑(x.appr n) = 0 then x.appr n
    else x.appr n + p ^ n * (toZMod (↑(unitCoeff hy) * ↑p ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs)).val

Proof state:
case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ (n : ℕ), x.appr n ≤ x.appr (n + 1)

Tactic:
intro n

Result:
case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ x.appr n ≤ x.appr (n + 1)

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Monotone x.appr

Tactic:
apply monotone_nat_of_le_succ

Result:
case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ (n : ℕ), x.appr n ≤ x.appr (n + 1)
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
@[elab_as_elim]
lemma adjoin_induction {s : Set A} {p : (x : A) → x ∈ adjoin R s → Prop}
    (mem : ∀ (x : A) (hx : x ∈ s), p x (subset_adjoin R s hx))
    (add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem hx hy))
    (zero : p 0 (zero_mem _)) (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
    (smul : ∀ (r : R) x hx, p x hx → p (r • x) (SMulMemClass.smul_mem r hx))
    (star : ∀ x hx, p x hx → p (star x) (star_mem hx))
    {a : A} (ha : a ∈ adjoin R s) : p a ha

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : x ∈ adjoin R s), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯
a : A
ha : a ∈ adjoin R s
x : A
hx✝ : x ∈ s ∪ Star.star s
hx : x ∈ s ∨ Star.star x ∈ s
⊢ p x ⋯

Tactic:
obtain (hx | hx) := hx

Result:
case inl
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : x ∈ adjoin R s), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯
a : A
ha : a ∈ adjoin R s
x : A
hx✝ : x ∈ s ∪ Star.star s
hx : x ∈ s
⊢ p x ⋯

case inr
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : x ∈ adjoin R s), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯
a : A
ha : a ∈ adjoin R s
x : A
hx✝ : x ∈ s ∪ Star.star s
hx : Star.star x ∈ s
⊢ p x ⋯
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
/-- The Riemann Zeta Function does not vanish on the closed half-plane `re s ≥ 1`.
(Note that the value at `s = 1` is a junk value, which happens to be nonzero.) -/
lemma _root_.riemannZeta_ne_zero_of_one_le_re ⦃s : ℂ⦄ (hs : 1 ≤ s.re) :
    riemannZeta s ≠ 0

Proof state:
case inl
hs : 1 ≤ re 1
⊢ riemannZeta 1 ≠ 0

Tactic:
exact riemannZeta_one_ne_zero

Result:
no goals

Proof state:
case inr
s : ℂ
hs : 1 ≤ s.re
hs₀ : s ≠ 1
⊢ riemannZeta s ≠ 0

Tactic:
exact LFunction_modOne_eq (χ := 1) ▸ LFunction_ne_zero_of_one_le_re _ (.inr hs₀) hs

Result:
no goals

Proof state:
s : ℂ
hs : 1 ≤ s.re
⊢ riemannZeta s ≠ 0

Tactic:
rcases eq_or_ne s 1 with rfl | hs₀

Result:
case inl
hs : 1 ≤ re 1
⊢ riemannZeta 1 ≠ 0

case inr
s : ℂ
hs : 1 ≤ s.re
hs₀ : s ≠ 1
⊢ riemannZeta s ≠ 0
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem contDiffOn_of_continuousOn_differentiableOn_deriv {n : ℕ∞}
    (Hcont : ∀ m : ℕ, (m : ℕ∞) ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s)
    (Hdiff : ∀ m : ℕ, (m : ℕ∞) < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s) :
    ContDiffOn 𝕜 n f s

Proof state:
case Hcont
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s

Tactic:
simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_continuousOn_iff]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s
⊢ ContDiffOn 𝕜 (↑n) f s

Tactic:
apply contDiffOn_of_continuousOn_differentiableOn

Result:
case Hcont
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s

case Hdiff
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s
⊢ ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s

Proof state:
case Hdiff
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s
⊢ ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s

Tactic:
simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableOn_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_le_neg {a b : Int} (h : a ≤ b) : -b ≤ -a

Proof state:
a b : Int
h : a ≤ b
this : 0 ≤ -a + b
⊢ -b ≤ -a

Tactic:
have : 0 + -b ≤ -a + b + -b := Int.add_le_add_right this (-b)

Result:
a b : Int
h : a ≤ b
this✝ : 0 ≤ -a + b
this : 0 + -b ≤ -a + b + -b
⊢ -b ≤ -a

Proof state:
a b : Int
h : a ≤ b
this✝ : 0 ≤ -a + b
this : 0 + -b ≤ -a + b + -b
⊢ -b ≤ -a

Tactic:
rwa [Int.add_neg_cancel_right, Int.zero_add] at this

Result:
no goals

Proof state:
a b : Int
h : a ≤ b
⊢ -b ≤ -a

Tactic:
have : 0 ≤ -a + b := Int.add_left_neg a ▸ Int.add_le_add_left h (-a)

Result:
a b : Int
h : a ≤ b
this : 0 ≤ -a + b
⊢ -b ≤ -a
-- Mathlib/Data/Vector/Basic.lean
theorem get_map₂ (v₁ : Vector α n) (v₂ : Vector β n) (f : α → β → γ) (i : Fin n) :
    get (map₂ f v₁ v₂) i = f (get v₁ i) (get v₂ i)

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
i : Fin n✝.succ
⊢ (map₂ f (a✝ ::ᵥ x✝) (b✝ ::ᵥ y✝)).get i = f ((a✝ ::ᵥ x✝).get i) ((b✝ ::ᵥ y✝).get i)

Tactic:
rw [map₂_cons]

Result:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
i : Fin n✝.succ
⊢ (f a✝ b✝ ::ᵥ map₂ f x✝ y✝).get i = f ((a✝ ::ᵥ x✝).get i) ((b✝ ::ᵥ y✝).get i)

Proof state:
case cons.succ
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
i✝ : Fin n✝
⊢ (f a✝ b✝ ::ᵥ map₂ f x✝ y✝).get i✝.succ = f ((a✝ ::ᵥ x✝).get i✝.succ) ((b✝ ::ᵥ y✝).get i✝.succ)

Tactic:
simp only [get_cons_succ, ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
i : Fin n✝.succ
⊢ (f a✝ b✝ ::ᵥ map₂ f x✝ y✝).get i = f ((a✝ ::ᵥ x✝).get i) ((b✝ ::ᵥ y✝).get i)

Tactic:
cases i using Fin.cases

Result:
case cons.zero
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
⊢ (f a✝ b✝ ::ᵥ map₂ f x✝ y✝).get 0 = f ((a✝ ::ᵥ x✝).get 0) ((b✝ ::ᵥ y✝).get 0)

case cons.succ
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
i✝ : Fin n✝
⊢ (f a✝ b✝ ::ᵥ map₂ f x✝ y✝).get i✝.succ = f ((a✝ ::ᵥ x✝).get i✝.succ) ((b✝ ::ᵥ y✝).get i✝.succ)

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
i : Fin 0
⊢ (map₂ f nil nil).get i = f (nil.get i) (nil.get i)

Tactic:
exact Fin.elim0 i

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
⊢ (f a✝ b✝ ::ᵥ map₂ f x✝ y✝).get 0 = f ((a✝ ::ᵥ x✝).get 0) ((b✝ ::ᵥ y✝).get 0)

Tactic:
simp only [get_zero, head_cons]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem getVert_of_length_le {u v} (w : G.Walk u v) {i : ℕ} (hi : w.length ≤ i) :
    w.getVert i = v

Proof state:
case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, p✝.length ≤ i → p✝.getVert i = w✝
n✝ : ℕ
hi : (cons h✝ p✝).length ≤ n✝ + 1
⊢ (cons h✝ p✝).getVert (n✝ + 1) = w✝

Tactic:
exact ih (Nat.succ_le_succ_iff.1 hi)

Result:
no goals

Proof state:
case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, p✝.length ≤ i → p✝.getVert i = w✝
hi : (cons h✝ p✝).length ≤ 0
⊢ (cons h✝ p✝).getVert 0 = w✝

Tactic:
cases hi

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
i : ℕ
hi : nil.length ≤ i
⊢ nil.getVert i = u✝

Tactic:
rfl

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, p✝.length ≤ i → p✝.getVert i = w✝
i : ℕ
hi : (cons h✝ p✝).length ≤ i
⊢ (cons h✝ p✝).getVert i = w✝

Tactic:
cases i

Result:
case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, p✝.length ≤ i → p✝.getVert i = w✝
hi : (cons h✝ p✝).length ≤ 0
⊢ (cons h✝ p✝).getVert 0 = w✝

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, p✝.length ≤ i → p✝.getVert i = w✝
n✝ : ℕ
hi : (cons h✝ p✝).length ≤ n✝ + 1
⊢ (cons h✝ p✝).getVert (n✝ + 1) = w✝
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_rel₁ {R : L.Relations 1} {t : L.Term _} :
    (R.boundedFormula₁ t).Realize v xs ↔ RelMap R ![t.realize (Sum.elim v xs)]

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : L.Term (α ⊕ Fin l)
⊢ (RelMap R fun i => realize (Sum.elim v xs) (![t] i)) = RelMap R ![realize (Sum.elim v xs) t]

Tactic:
refine congr rfl (funext fun _ => ?_)

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : L.Term (α ⊕ Fin l)
x✝ : Fin 1
⊢ realize (Sum.elim v xs) (![t] x✝) = ![realize (Sum.elim v xs) t] x✝

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : L.Term (α ⊕ Fin l)
x✝ : Fin 1
⊢ realize (Sum.elim v xs) (![t] x✝) = ![realize (Sum.elim v xs) t] x✝

Tactic:
simp only [Matrix.cons_val_fin_one]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : L.Term (α ⊕ Fin l)
⊢ (R.boundedFormula₁ t).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t]

Tactic:
rw [Relations.boundedFormula₁, realize_rel, iff_eq_eq]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : L.Term (α ⊕ Fin l)
⊢ (RelMap R fun i => realize (Sum.elim v xs) (![t] i)) = RelMap R ![realize (Sum.elim v xs) t]
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_append_left {a : Vector α n} {b : Vector α m} {i : Nat} (hi : i < n) :
    (a ++ b)[i] = a[i]

Proof state:
α : Type u_1
n m : Nat
a : Vector α n
b : Vector α m
i : Nat
hi : i < n
⊢ (a ++ b)[i] = a[i]

Tactic:
simp [getElem_append, hi]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsSuffix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) : l₁.map f <:+ l₂.map f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ : List α
h : l₁ <:+ l₂
⊢ List.map f l₁ <:+ List.map f l₂

Tactic:
obtain ⟨r, rfl⟩ := h

Result:
case intro
α : Type u_1
β : Type u_2
f : α → β
l₁ r : List α
⊢ List.map f l₁ <:+ List.map f (r ++ l₁)

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → β
l₁ r : List α
⊢ List.map f l₁ <:+ List.map f (r ++ l₁)

Tactic:
rw [map_append]

Result:
case intro
α : Type u_1
β : Type u_2
f : α → β
l₁ r : List α
⊢ List.map f l₁ <:+ List.map f r ++ List.map f l₁

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → β
l₁ r : List α
⊢ List.map f l₁ <:+ List.map f r ++ List.map f l₁

Tactic:
apply suffix_append

Result:
no goals
-- Mathlib/Data/Finite/Prod.lean
theorem infinite_image2 (hfs : ∀ b ∈ t, InjOn (fun a => f a b) s) (hft : ∀ a ∈ s, InjOn (f a) t) :
    (image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Proof state:
case refine_2.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a => f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
ht : t.Infinite
a : α
ha : a ∈ s
⊢ (image2 f s t).Infinite

Tactic:
exact ht.image2_right ha (hft _ ha)

Result:
no goals

Proof state:
case refine_2.inl.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a => f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
hs : s.Infinite
b : β
hb : b ∈ t
⊢ (image2 f s t).Infinite

Tactic:
exact hs.image2_left hb (hfs _ hb)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a => f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
refine ⟨fun h => Set.infinite_prod.1 ?_, ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a => f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (image2 f s t).Infinite
⊢ (s ×ˢ t).Infinite

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a => f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (image2 f s t).Infinite

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a => f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (uncurry f '' s ×ˢ t).Infinite
⊢ (s ×ˢ t).Infinite

Tactic:
exact h.of_image _

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a => f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (image2 f s t).Infinite
⊢ (s ×ˢ t).Infinite

Tactic:
rw [← image_uncurry_prod] at h

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a => f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (uncurry f '' s ×ˢ t).Infinite
⊢ (s ×ˢ t).Infinite

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a => f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (image2 f s t).Infinite

Tactic:
rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)

Result:
case refine_2.inl.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a => f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
hs : s.Infinite
b : β
hb : b ∈ t
⊢ (image2 f s t).Infinite

case refine_2.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a => f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
ht : t.Infinite
a : α
ha : a ∈ s
⊢ (image2 f s t).Infinite
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive (attr := simp)]
lemma stabilizer_op_subgroup (s : Subgroup G) : stabilizer Gᵐᵒᵖ (s : Set G) = s.op

Proof state:
G : Type u_1
inst✝ : Group G
s : Subgroup G
a : G
h : ∀ (b : G), b * a ∈ s ↔ b ∈ s
⊢ a ∈ s

Tactic:
simpa only [op_smul_eq_mul, SetLike.mem_coe, one_mul] using (h 1).2 s.one_mem

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
s : Subgroup G
⊢ ∀ (x : Gᵐᵒᵖ), (∀ (b : G), x • b ∈ ↑s ↔ b ∈ ↑s) ↔ x ∈ s.op

Tactic:
simp only [smul_eq_mul_unop, SetLike.mem_coe, Subgroup.mem_op, «forall», unop_op]

Result:
G : Type u_1
inst✝ : Group G
s : Subgroup G
⊢ ∀ (a : G), (∀ (b : G), b * a ∈ s ↔ b ∈ s) ↔ a ∈ s

Proof state:
G : Type u_1
inst✝ : Group G
s : Subgroup G
⊢ stabilizer Gᵐᵒᵖ ↑s = s.op

Tactic:
simp_rw [SetLike.ext_iff, mem_stabilizer_set]

Result:
G : Type u_1
inst✝ : Group G
s : Subgroup G
⊢ ∀ (x : Gᵐᵒᵖ), (∀ (b : G), x • b ∈ ↑s ↔ b ∈ ↑s) ↔ x ∈ s.op

Proof state:
G : Type u_1
inst✝ : Group G
s : Subgroup G
⊢ ∀ (a : G), (∀ (b : G), b * a ∈ s ↔ b ∈ s) ↔ a ∈ s

Tactic:
refine fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_right ha⟩

Result:
G : Type u_1
inst✝ : Group G
s : Subgroup G
a : G
h : ∀ (b : G), b * a ∈ s ↔ b ∈ s
⊢ a ∈ s
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem monic_map_iff [Semiring S] [Nontrivial S] {f : R →+* S} {p : R[X]} :
    (p.map f).Monic ↔ p.Monic

Proof state:
R : Type u
S : Type v
inst✝² : DivisionRing R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
⊢ (map f p).Monic ↔ p.Monic

Tactic:
rw [Monic, leadingCoeff_map, ← f.map_one, Function.Injective.eq_iff f.injective, Monic]

Result:
no goals