harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
    (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega)

Proof state:
α : Type u_1
i : Nat
as bs : Array α
h : i < (as ++ bs).size
⊢ (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]

Tactic:
cases as

Result:
case mk
α : Type u_1
i : Nat
bs : Array α
toList✝ : List α
h : i < ({ toList := toList✝ } ++ bs).size
⊢ ({ toList := toList✝ } ++ bs)[i] =
    if h' : i < { toList := toList✝ }.size then { toList := toList✝ }[i] else bs[i - { toList := toList✝ }.size]

Proof state:
α : Type ?u.228071
i : Nat
as bs : Array α
h' : ¬i < as.size
h : i < as.size + bs.size
⊢ i - as.size < bs.size

Tactic:
omega

Result:
no goals

Proof state:
case mk
α : Type u_1
i : Nat
bs : Array α
toList✝ : List α
h : i < ({ toList := toList✝ } ++ bs).size
⊢ ({ toList := toList✝ } ++ bs)[i] =
    if h' : i < { toList := toList✝ }.size then { toList := toList✝ }[i] else bs[i - { toList := toList✝ }.size]

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
i : Nat
toList✝¹ toList✝ : List α
h : i < ({ toList := toList✝¹ } ++ { toList := toList✝ }).size
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ })[i] =
    if h' : i < { toList := toList✝¹ }.size then { toList := toList✝¹ }[i]
    else { toList := toList✝ }[i - { toList := toList✝¹ }.size]

Proof state:
α : Type ?u.228071
i : Nat
as bs : Array α
h : i < (as ++ bs).size
h' : ¬i < as.size
⊢ i - as.size < bs.size

Tactic:
simp at h

Result:
α : Type ?u.228071
i : Nat
as bs : Array α
h' : ¬i < as.size
h : i < as.size + bs.size
⊢ i - as.size < bs.size

Proof state:
case mk.mk
α : Type u_1
i : Nat
toList✝¹ toList✝ : List α
h : i < ({ toList := toList✝¹ } ++ { toList := toList✝ }).size
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ })[i] =
    if h' : i < { toList := toList✝¹ }.size then { toList := toList✝¹ }[i]
    else { toList := toList✝ }[i - { toList := toList✝¹ }.size]

Tactic:
simp [List.getElem_append]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean
lemma absolutelyContinuous_sum_left {μs : ι → Measure α} (hμs : ∀ i, μs i ≪ ν) :
    Measure.sum μs ≪ ν :=
  AbsolutelyContinuous.mk fun s hs hs0 ↦ by simp [sum_apply _ hs, fun i ↦ hμs i hs0]

Proof state:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
hμs : ∀ (i : ι), μs i ≪ ν
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
⊢ (sum μs) s = 0

Tactic:
simp [sum_apply _ hs, fun i ↦ hμs i hs0]

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
theorem algebraMap_image (h : SpectrumRestricts a f) :
    algebraMap R S '' spectrum R a = spectrum S a

Proof state:
case refine_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : Semifield R
inst✝⁵ : Semifield S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
a : A
f : S → R
inst✝ : IsScalarTower R S A
h : SpectrumRestricts a f
s : S
hs : s ∈ spectrum S a
⊢ f s ∈ spectrum R a ∧ (algebraMap R S) (f s) = s

Tactic:
exact ⟨spectrum.of_algebraMap_mem S ((h.rightInvOn hs).symm ▸ hs), h.rightInvOn hs⟩

Result:
no goals

Proof state:
case refine_1
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : Semifield R
inst✝⁵ : Semifield S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
a : A
f : S → R
inst✝ : IsScalarTower R S A
h : SpectrumRestricts a f
⊢ ⇑(algebraMap R S) '' spectrum R a ⊆ spectrum S a

Tactic:
simpa only [spectrum.preimage_algebraMap] using
  (spectrum S a).image_preimage_subset (algebraMap R S)

Result:
no goals

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : Semifield R
inst✝⁵ : Semifield S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
a : A
f : S → R
inst✝ : IsScalarTower R S A
h : SpectrumRestricts a f
⊢ ⇑(algebraMap R S) '' spectrum R a = spectrum S a

Tactic:
refine Set.eq_of_subset_of_subset ?_ fun s hs => ⟨f s, ?_⟩

Result:
case refine_1
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : Semifield R
inst✝⁵ : Semifield S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
a : A
f : S → R
inst✝ : IsScalarTower R S A
h : SpectrumRestricts a f
⊢ ⇑(algebraMap R S) '' spectrum R a ⊆ spectrum S a

case refine_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : Semifield R
inst✝⁵ : Semifield S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
a : A
f : S → R
inst✝ : IsScalarTower R S A
h : SpectrumRestricts a f
s : S
hs : s ∈ spectrum S a
⊢ f s ∈ spectrum R a ∧ (algebraMap R S) (f s) = s
-- Mathlib/Order/Filter/CardinalInter.lean
theorem cardinalGenerate_isGreatest (hc : 2 < c) :
    IsGreatest { f : Filter α | CardinalInterFilter f c ∧ g ⊆ f.sets } (cardinalGenerate g hc)

Proof state:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
⊢ cardinalGenerate g hc ∈ upperBounds {f | CardinalInterFilter f c ∧ g ⊆ f.sets}

Tactic:
rintro f ⟨fct, hf⟩

Result:
case intro
α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
f : Filter α
fct : CardinalInterFilter f c
hf : g ⊆ f.sets
⊢ f ≤ cardinalGenerate g hc

Proof state:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
⊢ IsGreatest {f | CardinalInterFilter f c ∧ g ⊆ f.sets} (cardinalGenerate g hc)

Tactic:
refine ⟨⟨cardinalInter_ofCardinalGenerate _ _, fun s => CardinalGenerateSets.basic⟩, ?_⟩

Result:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
⊢ cardinalGenerate g hc ∈ upperBounds {f | CardinalInterFilter f c ∧ g ⊆ f.sets}

Proof state:
case intro
α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
f : Filter α
fct : CardinalInterFilter f c
hf : g ⊆ f.sets
⊢ f ≤ cardinalGenerate g hc

Tactic:
rwa [le_cardinalGenerate_iff_of_cardinalInterFilter]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem isLittleO_rpow_exp_pos_mul_atTop (s : ℝ) {b : ℝ} (hb : 0 < b) :
    (fun x : ℝ => x ^ s) =o[atTop] fun x => exp (b * x) :=
  isLittleO_of_tendsto (fun _ h => absurd h (exp_pos _).ne') <| by
    simpa only [div_eq_mul_inv, exp_neg, neg_mul] using
      tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero s b hb

Proof state:
s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x => x ^ s / rexp (b * x)) atTop (𝓝 0)

Tactic:
simpa only [div_eq_mul_inv, exp_neg, neg_mul] using
  tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero s b hb

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem card_compression (a : α) (𝒜 : Finset (Finset α)) : #(𝓓 a 𝒜) = #𝒜

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ ↑(filter (fun a_1 => a_1.erase a ∉ 𝒜) 𝒜)
⊢ s ∈ {s | a ∈ s}

Tactic:
rw [mem_coe, mem_filter] at hs

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜 ∧ s.erase a ∉ 𝒜
⊢ s ∈ {s | a ∈ s}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #(𝓓 a 𝒜) = #𝒜

Tactic:
rw [compression, card_disjUnion, filter_image,
  card_image_of_injOn ((erase_injOn' _).mono fun s hs => _), ← card_union_of_disjoint]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #(filter (fun s => s.erase a ∈ 𝒜) 𝒜 ∪ filter (fun a_1 => a_1.erase a ∉ 𝒜) 𝒜) = #𝒜

α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Disjoint (filter (fun s => s.erase a ∈ 𝒜) 𝒜) (filter (fun a_1 => a_1.erase a ∉ 𝒜) 𝒜)

α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ∀ s ∈ ↑(filter (fun a_1 => a_1.erase a ∉ 𝒜) 𝒜), s ∈ {s | a ∈ s}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Disjoint (filter (fun s => s.erase a ∈ 𝒜) 𝒜) (filter (fun a_1 => a_1.erase a ∉ 𝒜) 𝒜)

Tactic:
exact disjoint_filter_filter_neg 𝒜 𝒜 (fun s => (erase s a ∈ 𝒜))

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜 ∧ s.erase a ∉ 𝒜
⊢ s ∈ {s | a ∈ s}

Tactic:
exact not_imp_comm.1 erase_eq_of_not_mem (ne_of_mem_of_not_mem hs.1 hs.2).symm

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #(filter (fun s => s.erase a ∈ 𝒜) 𝒜 ∪ filter (fun a_1 => a_1.erase a ∉ 𝒜) 𝒜) = #𝒜

Tactic:
conv_rhs => rw [← filter_union_filter_neg_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ∀ s ∈ ↑(filter (fun a_1 => a_1.erase a ∉ 𝒜) 𝒜), s ∈ {s | a ∈ s}

Tactic:
intro s hs

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ ↑(filter (fun a_1 => a_1.erase a ∉ 𝒜) 𝒜)
⊢ s ∈ {s | a ∈ s}
-- Mathlib/Order/SymmDiff.lean
theorem le_symmDiff_sup_right (a b : α) : a ≤ (a ∆ b) ⊔ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a ∆ b ⊔ b

Tactic:
convert symmDiff_triangle a b ⊥ <;> rw [symmDiff_bot]

Result:
no goals
-- Mathlib/Data/Matrix/PEquiv.lean
theorem toMatrix_trans [Fintype m] [DecidableEq m] [DecidableEq n] [Semiring α] (f : l ≃. m)
    (g : m ≃. n) : ((f.trans g).toMatrix : Matrix l n α) = f.toMatrix * g.toMatrix

Proof state:
case a
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ (f.trans g).toMatrix i j = (f.toMatrix * g.toMatrix) i j

Tactic:
rw [toMatrix_mul_apply]

Result:
case a
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ (f.trans g).toMatrix i j = Option.casesOn (f i) 0 fun fi => g.toMatrix fi j

Proof state:
case a
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ (f.trans g).toMatrix i j = Option.casesOn (f i) 0 fun fi => g.toMatrix fi j

Tactic:
dsimp [toMatrix, PEquiv.trans]

Result:
case a
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ (if j ∈ (f i).bind ⇑g then 1 else 0) = Option.rec 0 (fun val => if j ∈ g val then 1 else 0) (f i)

Proof state:
case a
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ (if j ∈ (f i).bind ⇑g then 1 else 0) = Option.rec 0 (fun val => if j ∈ g val then 1 else 0) (f i)

Tactic:
cases f i <;> simp

Result:
no goals

Proof state:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
⊢ (f.trans g).toMatrix = f.toMatrix * g.toMatrix

Tactic:
ext i j

Result:
case a
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ (f.trans g).toMatrix i j = (f.toMatrix * g.toMatrix) i j
-- Mathlib/Analysis/Convex/Strong.lean
@[simp] lemma uniformConvexOn_zero : UniformConvexOn s 0 f ↔ ConvexOn ℝ s f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
f : E → ℝ
⊢ UniformConvexOn s 0 f ↔ ConvexOn ℝ s f

Tactic:
simp [UniformConvexOn, ConvexOn]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem prodMonoidal_rightUnitor_hom_fst (X : C₁ × C₂) :
    ((ρ_ X).hom : X ⊗ 𝟙_ _ ⟶ X).1 = (ρ_ X.1).hom

Proof state:
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (ρ_ X).hom.1 = (ρ_ X.1).hom

Tactic:
cases X

Result:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (ρ_ (fst✝, snd✝)).hom.1 = (ρ_ (fst✝, snd✝).1).hom

Proof state:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (ρ_ (fst✝, snd✝)).hom.1 = (ρ_ (fst✝, snd✝).1).hom

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Fold.lean
theorem fold_min_lt : s.fold min b f < c ↔ b < c ∨ ∃ x ∈ s, f x < c

Proof state:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold min b f s < c ↔ b < c ∨ ∃ x ∈ s, f x < c

Tactic:
show _ > _ ↔ _

Result:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c > fold min b f s ↔ b < c ∨ ∃ x ∈ s, f x < c

Proof state:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x > y ⊓ z ↔ x > y ∨ x > z

Tactic:
intro x y z

Result:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x > y ⊓ z ↔ x > y ∨ x > z

Proof state:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c > fold min b f s ↔ b < c ∨ ∃ x ∈ s, f x < c

Tactic:
apply fold_op_rel_iff_or

Result:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x > y ⊓ z ↔ x > y ∨ x > z

Proof state:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x > y ⊓ z ↔ x > y ∨ x > z

Tactic:
show _ < _ ↔ _

Result:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ y ⊓ z < x ↔ x > y ∨ x > z

Proof state:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ y ⊓ z < x ↔ x > y ∨ x > z

Tactic:
exact min_lt_iff

Result:
no goals
-- Mathlib/Data/Set/MulAntidiagonal.lean
theorem swap_mem_mulAntidiagonal [CommSemigroup α] {s t : Set α} {a : α} {x : α × α} :
    x.swap ∈ Set.mulAntidiagonal s t a ↔ x ∈ Set.mulAntidiagonal t s a

Proof state:
α : Type u_1
inst✝ : CommSemigroup α
s t : Set α
a : α
x : α × α
⊢ x.swap ∈ s.mulAntidiagonal t a ↔ x ∈ t.mulAntidiagonal s a

Tactic:
simp [mul_comm, and_left_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem isUnit_det_transpose (h : IsUnit A.det) : IsUnit Aᵀ.det

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ IsUnit Aᵀ.det

Tactic:
rw [det_transpose]

Result:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ IsUnit A.det

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ IsUnit A.det

Tactic:
exact h

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Defs.lean
lemma IsNilpotent.pow_of_pos {n} {S : Type*} [MonoidWithZero S] {x : S}
    (hx : IsNilpotent x) (hn : n ≠ 0) : IsNilpotent (x ^ n)

Proof state:
case zero
S : Type u_3
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
hn : 0 ≠ 0
⊢ IsNilpotent (x ^ 0)

Tactic:
contradiction

Result:
no goals

Proof state:
case succ
S : Type u_3
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ IsNilpotent (x ^ (n✝ + 1))

Tactic:
exact IsNilpotent.pow_succ _ hx

Result:
no goals

Proof state:
n : ℕ
S : Type u_3
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
hn : n ≠ 0
⊢ IsNilpotent (x ^ n)

Tactic:
cases n with
| zero => contradiction
| succ => exact IsNilpotent.pow_succ _ hx

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Equiv.lean
theorem equivSubtypeMap_symm_apply {p : Submodule R M} {q : Submodule R p} (x : q.map p.subtype) :
    ((p.equivSubtypeMap q).symm x : M) = x

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
q : Submodule R ↥p
x : ↥(map p.subtype q)
⊢ ↑↑((p.equivSubtypeMap q).symm x) = ↑x

Tactic:
cases x

Result:
case mk
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
q : Submodule R ↥p
val✝ : M
property✝ : val✝ ∈ map p.subtype q
⊢ ↑↑((p.equivSubtypeMap q).symm ⟨val✝, property✝⟩) = ↑⟨val✝, property✝⟩

Proof state:
case mk
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
q : Submodule R ↥p
val✝ : M
property✝ : val✝ ∈ map p.subtype q
⊢ ↑↑((p.equivSubtypeMap q).symm ⟨val✝, property✝⟩) = ↑⟨val✝, property✝⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Localization/Finiteness.lean
/--
To check that the kernel of a ring homomorphism is finitely generated,
it suffices to check this after localizing at a spanning set of the source.
-/
lemma RingHom.ker_fg_of_localizationSpan (t : Set R) (ht : Ideal.span t = ⊤)
    (H : ∀ g : t, (RingHom.ker (Localization.awayMap f g.val)).FG) :
    (RingHom.ker f).FG

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
t : Set R
ht : Ideal.span t = ⊤
H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG
⊢ ∀ (g : ↑t), (Ideal.map (algebraMap R (Localization.Away ↑g)) (ker f)).FG

Tactic:
intro g

Result:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
t : Set R
ht : Ideal.span t = ⊤
H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG
g : ↑t
⊢ (Ideal.map (algebraMap R (Localization.Away ↑g)) (ker f)).FG

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
t : Set R
ht : Ideal.span t = ⊤
H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG
g : ↑t
⊢ (ker (IsLocalization.map (Localization.Away (f ↑g)) f ⋯)).FG

Tactic:
exact H g

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
t : Set R
ht : Ideal.span t = ⊤
H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG
⊢ (ker f).FG

Tactic:
apply Ideal.fg_of_localizationSpan t ht

Result:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
t : Set R
ht : Ideal.span t = ⊤
H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG
⊢ ∀ (g : ↑t), (Ideal.map (algebraMap R (Localization.Away ↑g)) (ker f)).FG

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
t : Set R
ht : Ideal.span t = ⊤
H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG
g : ↑t
⊢ (Ideal.map (algebraMap R (Localization.Away ↑g)) (ker f)).FG

Tactic:
rw [← IsLocalization.ker_map (Localization.Away (f g.val)) f (Submonoid.map_powers f g.val)]

Result:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
t : Set R
ht : Ideal.span t = ⊤
H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG
g : ↑t
⊢ (ker (IsLocalization.map (Localization.Away (f ↑g)) f ⋯)).FG
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem rotation_pi_div_two : o.rotation (π / 2 : ℝ) = J

Proof state:
case h
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ (o.rotation ↑(π / 2)) x = o.rightAngleRotation x

Tactic:
simp [rotation]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
⊢ o.rotation ↑(π / 2) = o.rightAngleRotation

Tactic:
ext x

Result:
case h
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ (o.rotation ↑(π / 2)) x = o.rightAngleRotation x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_filter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    {f : (a : α) → β a → Bool} (h : Raw.WFImp m.1) : Raw.WFImp (m.filter f).1

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Bool
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.filterₘ f).val

Tactic:
exact wfImp_filterₘ h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Bool
h : Raw.WFImp m.val
⊢ Raw.WFImp (filter f m).val

Tactic:
rw [filter_eq_filterₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Bool
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.filterₘ f).val
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_eq_zipIdx_map {l : Vector α n} {f : Nat → α → β} :
    l.mapIdx f = l.zipIdx.map fun ⟨a, i⟩ => f i a

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : Nat → α → β
⊢ mapIdx f l =
    map
      (fun x =>
        match x with
        | (a, i) => f i a)
      l.zipIdx

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem values_eq_on_of_interpolate_eq (hvs : Set.InjOn v s)
    (hrr' : interpolate s v r = interpolate s v r') : ∀ i ∈ s, r i = r' i := fun _ hi => by
  rw [← eval_interpolate_at_node r hvs hi, hrr', eval_interpolate_at_node r' hvs hi]

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
hrr' : (interpolate s v) r = (interpolate s v) r'
x✝ : ι
hi : x✝ ∈ s
⊢ r x✝ = r' x✝

Tactic:
rw [← eval_interpolate_at_node r hvs hi, hrr', eval_interpolate_at_node r' hvs hi]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
@[simp]
lemma toBlocks₂₂_diagonal (v : l ⊕ m → α) :
    toBlocks₂₂ (diagonal v) = diagonal (fun i => v (Sum.inr i))

Proof state:
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
⊢ (of fun i j => diagonal v (Sum.inr i) (Sum.inr j)) = diagonal fun i => v (Sum.inr i)

Tactic:
funext i j

Result:
case h.h
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
i j : m
⊢ of (fun i j => diagonal v (Sum.inr i) (Sum.inr j)) i j = diagonal (fun i => v (Sum.inr i)) i j

Proof state:
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
⊢ (diagonal v).toBlocks₂₂ = diagonal fun i => v (Sum.inr i)

Tactic:
unfold toBlocks₂₂

Result:
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
⊢ (of fun i j => diagonal v (Sum.inr i) (Sum.inr j)) = diagonal fun i => v (Sum.inr i)

Proof state:
case h.h
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
i j : m
⊢ of (fun i j => diagonal v (Sum.inr i) (Sum.inr j)) i j = diagonal (fun i => v (Sum.inr i)) i j

Tactic:
simp only [ne_eq, Sum.inr.injEq, of_apply, diagonal_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem integral_image_eq_integral_abs_deriv_smul {s : Set ℝ} {f : ℝ → ℝ} {f' : ℝ → ℝ}
    (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x)
    (hf : InjOn f s) (g : ℝ → F) : ∫ x in f '' s, g x = ∫ x in s, |f' x| • g (f x)

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : InjOn f s
g : ℝ → F
⊢ ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, |f' x| • g (f x)

Tactic:
simpa only [det_one_smulRight] using
  integral_image_eq_integral_abs_det_fderiv_smul volume hs
    (fun x hx => (hf' x hx).hasFDerivWithinAt) hf g

Result:
no goals
-- Mathlib/Deprecated/Cardinal/Finite.lean
theorem card_eq_coe_natCard (α : Type*) [Finite α] : card α = Nat.card α

Proof state:
case a
α : Type u_1
inst✝ : Finite α
⊢ ↑(Nat.card α) = #α

Tactic:
exact Nat.cast_card

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Finite α
⊢ card α = ↑(Nat.card α)

Tactic:
unfold PartENat.card

Result:
α : Type u_1
inst✝ : Finite α
⊢ toPartENat #α = ↑(Nat.card α)

Proof state:
case a
α : Type u_1
inst✝ : Finite α
⊢ ↑(Nat.card α) = toPartENat #α

Tactic:
rw [Cardinal.natCast_eq_toPartENat_iff]

Result:
case a
α : Type u_1
inst✝ : Finite α
⊢ ↑(Nat.card α) = #α

Proof state:
α : Type u_1
inst✝ : Finite α
⊢ toPartENat #α = ↑(Nat.card α)

Tactic:
apply symm

Result:
case a
α : Type u_1
inst✝ : Finite α
⊢ ↑(Nat.card α) = toPartENat #α