harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fin/Tuple/Sort.lean
theorem eq_sort_iff' : σ = sort f ↔ StrictMono (σ.trans <| graphEquiv₁ f)

Proof state:
case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))
this : graphEquiv₂ f = StrictMono.orderIsoOfSurjective (⇑(Equiv.trans σ (graphEquiv₁ f))) h ⋯
⊢ σ = sort f

Tactic:
ext1 x

Result:
case mpr.H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))
this : graphEquiv₂ f = StrictMono.orderIsoOfSurjective (⇑(Equiv.trans σ (graphEquiv₁ f))) h ⋯
x : Fin n
⊢ σ x = (sort f) x

Proof state:
case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))
⊢ σ = sort f

Tactic:
have := Subsingleton.elim (graphEquiv₂ f) (h.orderIsoOfSurjective _ <| Equiv.surjective _)

Result:
case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))
this : graphEquiv₂ f = StrictMono.orderIsoOfSurjective (⇑(Equiv.trans σ (graphEquiv₁ f))) h ⋯
⊢ σ = sort f

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ σ = sort f ↔ StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))

Tactic:
constructor <;> intro h

Result:
case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))

case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))
⊢ σ = sort f

Proof state:
case mpr.H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))
this : graphEquiv₂ f = StrictMono.orderIsoOfSurjective (⇑(Equiv.trans σ (graphEquiv₁ f))) h ⋯
x : Fin n
⊢ σ x = (sort f) x

Tactic:
exact (graphEquiv₁ f).apply_eq_iff_eq_symm_apply.1 (DFunLike.congr_fun this x).symm

Result:
no goals

Proof state:
case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono ⇑((graphEquiv₂ f).trans (Equiv.refl { x // x ∈ graph f }))

Tactic:
exact (graphEquiv₂ f).strictMono

Result:
no goals

Proof state:
case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))

Tactic:
rw [h, sort, Equiv.trans_assoc, Equiv.symm_trans_self]

Result:
case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono ⇑((graphEquiv₂ f).trans (Equiv.refl { x // x ∈ graph f }))
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem Module.finrank_eq_zero_iff :
    finrank R M = 0 ↔ ∀ x : M, ∃ a : R, a ≠ 0 ∧ a • x = 0

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ finrank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0

Tactic:
rw [← rank_eq_zero_iff (R := R), ← finrank_eq_rank]

Result:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ finrank R M = 0 ↔ ↑(finrank R M) = 0

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ finrank R M = 0 ↔ ↑(finrank R M) = 0

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasFDerivWithinAt.comp_hasDerivWithinAt_of_eq {t : Set F}
    (hl : HasFDerivWithinAt l l' t y)
    (hf : HasDerivWithinAt f f' s x) (hst : MapsTo f s t) (hy : y = f x) :
    HasDerivWithinAt (l ∘ f) (l' f') s x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
t : Set F
hl : HasFDerivWithinAt l l' t (f x)
hf : HasDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasDerivWithinAt (l ∘ f) (l' f') s x

Tactic:
exact hl.comp_hasDerivWithinAt x hf hst

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
t : Set F
hl : HasFDerivWithinAt l l' t y
hf : HasDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasDerivWithinAt (l ∘ f) (l' f') s x

Tactic:
rw [hy] at hl

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
t : Set F
hl : HasFDerivWithinAt l l' t (f x)
hf : HasDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasDerivWithinAt (l ∘ f) (l' f') s x
-- Mathlib/Data/ZMod/Basic.lean
theorem val_one (n : ℕ) [Fact (1 < n)] : (1 : ZMod n).val = 1

Proof state:
n : ℕ
inst✝ : Fact (1 < n)
⊢ val 1 = 1

Tactic:
rw [val_one_eq_one_mod]

Result:
n : ℕ
inst✝ : Fact (1 < n)
⊢ 1 % n = 1

Proof state:
n : ℕ
inst✝ : Fact (1 < n)
⊢ 1 % n = 1

Tactic:
exact Nat.mod_eq_of_lt Fact.out

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem weightedOrder_le {d : σ →₀ ℕ} (h : coeff R d f ≠ 0) :
    f.weightedOrder w ≤ weight w d

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) f ≠ 0
⊢ weightedOrder w f ≤ ↑((weight w) d)

Tactic:
rw [weightedOrder, dif_neg]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) f ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑((weight w) d)

case hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) f ≠ 0
⊢ ¬f = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) f ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑((weight w) d)

Tactic:
simp only [ne_eq, Nat.cast_le, Nat.find_le_iff]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) f ≠ 0
⊢ ∃ m ≤ (weight w) d, ∃ d, ¬(coeff R d) f = 0 ∧ (weight w) d = m

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) f ≠ 0
⊢ ∃ m ≤ (weight w) d, ∃ d, ¬(coeff R d) f = 0 ∧ (weight w) d = m

Tactic:
exact ⟨weight w d, le_rfl, d, h, rfl⟩

Result:
no goals

Proof state:
case hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) f ≠ 0
⊢ ¬f = 0

Tactic:
exact (f.ne_zero_iff_exists_coeff_ne_zero_and_weight w).mpr ⟨weight w d, d, h, rfl⟩

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_pow (φ : MvPolynomial σ R) (n : ℕ) : (φ ^ n).vars ⊆ φ.vars

Proof state:
case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
⊢ φ.vars ∪ (φ ^ n).vars ⊆ φ.vars

Tactic:
exact Finset.union_subset (Finset.Subset.refl _) ih

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
⊢ (φ ^ n).vars ⊆ φ.vars

Tactic:
classical
induction n with
| zero => simp
| succ n ih =>
  rw [pow_succ']
  apply Finset.Subset.trans (vars_mul _ _)
  exact Finset.union_subset (Finset.Subset.refl _) ih

Result:
no goals

Proof state:
case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
⊢ (φ * φ ^ n).vars ⊆ φ.vars

Tactic:
apply Finset.Subset.trans (vars_mul _ _)

Result:
case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
⊢ φ.vars ∪ (φ ^ n).vars ⊆ φ.vars

Proof state:
case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ (φ ^ 0).vars ⊆ φ.vars

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
⊢ (φ ^ n).vars ⊆ φ.vars

Tactic:
induction n with
| zero => simp
| succ n ih =>
  rw [pow_succ']
  apply Finset.Subset.trans (vars_mul _ _)
  exact Finset.union_subset (Finset.Subset.refl _) ih

Result:
no goals

Proof state:
case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
⊢ (φ ^ (n + 1)).vars ⊆ φ.vars

Tactic:
rw [pow_succ']

Result:
case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
⊢ (φ * φ ^ n).vars ⊆ φ.vars
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem _root_.Directed.measure_iUnion [Countable ι] {s : ι → Set α} (hd : Directed (· ⊆ ·) s) :
    μ (⋃ i, s i) = ⨆ i, μ (s i)

Proof state:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
T : ℕ → Set α := fun n => toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
hm : ∀ (n : ℕ), MeasurableSet (Td n)
I : Finset ℕ
N : ℕ
hN : ∀ i ∈ I, t i ⊆ t N
⊢ ∑ n ∈ I, μ (Td n) ≤ ⨆ n, μ (t n)

Tactic:
calc
  (∑ n ∈ I, μ (Td n)) = μ (⋃ n ∈ I, Td n) :=
    (measure_biUnion_finset ((disjoint_disjointed T).set_pairwise I) fun n _ => hm n).symm
  _ ≤ μ (⋃ n ∈ I, T n) := measure_mono (iUnion₂_mono fun n _hn => disjointed_subset _ _)
  _ = μ (⋃ n ∈ I, t n) := measure_biUnion_toMeasurable I.countable_toSet _
  _ ≤ μ (t N) := measure_mono (iUnion₂_subset hN)
  _ ≤ ⨆ n, μ (t n) := le_iSup (μ ∘ t) N

Result:
no goals
-- Mathlib/Data/Finset/SMulAntidiagonal.lean
theorem mem_smulAntidiagonal :
    x ∈ SMulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
a : P
x : G × P
⊢ x ∈ s.smulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a

Tactic:
exact Set.mem_sep_iff

Result:
no goals

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
a : P
x : G × P
⊢ x ∈ SMulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a

Tactic:
simp only [SMulAntidiagonal, Set.Finite.mem_toFinset]

Result:
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
a : P
x : G × P
⊢ x ∈ s.smulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
lemma mkPrecomp_comp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') :
    mkPrecomp f (g' ≫ g) = eqToHom (by simp) ≫ mkPrecomp (S.map g ≫ f) g' ≫ mkPrecomp f g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
Y Y' Y'' : C
S : C ⥤ D
f : S.obj Y ⟶ T
g : Y' ⟶ Y
g' : Y'' ⟶ Y'
⊢ mkPrecomp f (g' ≫ g) = eqToHom ⋯ ≫ mkPrecomp (S.map g ≫ f) g' ≫ mkPrecomp f g

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f : S.obj Y ⟶ T
g : Y' ⟶ Y
g' : Y'' ⟶ Y'
⊢ mk (S.map (g' ≫ g) ≫ f) = mk (S.map g' ≫ S.map g ≫ f)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/Double.lean
lemma isZero_double_X (k : ι) (h₀ : k ≠ i₀) (h₁ : k ≠ i₁) :
    IsZero ((double f hi₀₁).X k)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
⊢ IsZero ((double f hi₀₁).X k)

Tactic:
dsimp [double]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
⊢ IsZero (if k = i₀ then X₀ else if k = i₁ then X₁ else 0)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
⊢ IsZero (if k = i₀ then X₀ else if k = i₁ then X₁ else 0)

Tactic:
rw [if_neg h₀, if_neg h₁]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
⊢ IsZero 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
⊢ IsZero 0

Tactic:
exact Limits.isZero_zero C

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_of_back? {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs

Proof state:
case mk
α : Type u_1
a : α
toList✝ : List α
h : { toList := toList✝ }.back? = some a
⊢ a ∈ { toList := toList✝ }

Tactic:
simpa using List.mem_of_getLast? (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
a : α
h : xs.back? = some a
⊢ a ∈ xs

Tactic:
cases xs

Result:
case mk
α : Type u_1
a : α
toList✝ : List α
h : { toList := toList✝ }.back? = some a
⊢ a ∈ { toList := toList✝ }

Proof state:
α : Type u_1
a : α
toList✝ : List α
h : { toList := toList✝ }.back? = some a
⊢ toList✝.getLast? = some a

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/Matrix/Kronecker.lean
theorem kroneckerMap_diagonal_right [Zero β] [Zero γ] [DecidableEq n] (f : α → β → γ)
    (hf : ∀ a, f a 0 = 0) (A : Matrix l m α) (b : n → β) :
    kroneckerMap f A (diagonal b) = blockDiagonal fun i => A.map fun a => f a (b i)

Proof state:
case a.mk.mk
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : DecidableEq n
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
b : n → β
i₁ : l
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f A (diagonal b) (i₁, i₂) (j₁, j₂) = blockDiagonal (fun i => A.map fun a => f a (b i)) (i₁, i₂) (j₁, j₂)

Tactic:
simp [diagonal, blockDiagonal, apply_ite (f (A i₁ j₁)), hf]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : DecidableEq n
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
b : n → β
⊢ kroneckerMap f A (diagonal b) = blockDiagonal fun i => A.map fun a => f a (b i)

Tactic:
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩

Result:
case a.mk.mk
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : DecidableEq n
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
b : n → β
i₁ : l
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f A (diagonal b) (i₁, i₂) (j₁, j₂) = blockDiagonal (fun i => A.map fun a => f a (b i)) (i₁, i₂) (j₁, j₂)
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem left_inv (x : H) : I.symm (I x) = x

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x : H
⊢ ↑I.symm (↑I x) = x

Tactic:
refine I.left_inv' ?_

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x : H
⊢ x ∈ I.source

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x : H
⊢ x ∈ I.source

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
@[simp] lemma mem_Iio : x ∈ Iio b ↔ x < b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Iio b ↔ x < b

Tactic:
rw [Iio, ← Finset.mem_def, Finset.mem_Iio]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem adjoin.range_algebraMap_subset : Set.range (algebraMap F E) ⊆ adjoin F S

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ Set.range ⇑(algebraMap F E)
⊢ x ∈ ↑(adjoin F S)

Tactic:
obtain ⟨f, hf⟩ := hx

Result:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
f : F
hf : (algebraMap F E) f = x
⊢ x ∈ ↑(adjoin F S)

Proof state:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
f : F
hf : (algebraMap F E) f = x
⊢ x ∈ ↑(adjoin F S)

Tactic:
rw [← hf]

Result:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
f : F
hf : (algebraMap F E) f = x
⊢ (algebraMap F E) f ∈ ↑(adjoin F S)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
⊢ Set.range ⇑(algebraMap F E) ⊆ ↑(adjoin F S)

Tactic:
intro x hx

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ Set.range ⇑(algebraMap F E)
⊢ x ∈ ↑(adjoin F S)

Proof state:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
f : F
hf : (algebraMap F E) f = x
⊢ (algebraMap F E) f ∈ ↑(adjoin F S)

Tactic:
exact adjoin.algebraMap_mem F S f

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem toFinsupp_monomial (n : ℕ) (r : R) : (monomial n r).toFinsupp = Finsupp.single n r

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ ((monomial n) r).toFinsupp = Finsupp.single n r

Tactic:
simp [monomial]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coverage.lean
lemma eq_top_pullback {X Y : C} {S T : Sieve X} (h : S ≤ T) (f : Y ⟶ X) (hf : S f) :
    T.pullback f = ⊤

Proof state:
case h
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ T.arrows (g ≫ f)

Tactic:
apply h

Result:
case h.a
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ S.arrows (g ≫ f)

Proof state:
case h.a.x
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ S.arrows f

Tactic:
exact hf

Result:
no goals

Proof state:
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f T = ⊤

Tactic:
ext Z g

Result:
case h
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f T).arrows g ↔ ⊤.arrows g

Proof state:
case h.a
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ S.arrows (g ≫ f)

Tactic:
apply S.downward_closed

Result:
case h.a.x
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ S.arrows f

Proof state:
case h
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f T).arrows g ↔ ⊤.arrows g

Tactic:
simp only [Sieve.pullback_apply, Sieve.top_apply, iff_true]

Result:
case h
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ T.arrows (g ≫ f)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_sign : ∀ a b, a / sign b = a * sign b
  | _, succ _ => by simp [sign, Int.mul_one]
  | _, 0 => by simp [sign, Int.mul_zero]
  | _, -[_+1] => by simp [sign, Int.mul_neg, Int.mul_one]

Proof state:
x✝ : Int
a✝ : Nat
⊢ x✝ / -[a✝+1].sign = x✝ * -[a✝+1].sign

Tactic:
simp [sign, Int.mul_neg, Int.mul_one]

Result:
no goals

Proof state:
x✝ : Int
n✝ : Nat
⊢ x✝ / (↑n✝.succ).sign = x✝ * (↑n✝.succ).sign

Tactic:
simp [sign, Int.mul_one]

Result:
no goals

Proof state:
x✝ : Int
⊢ x✝ / sign 0 = x✝ * sign 0

Tactic:
simp [sign, Int.mul_zero]

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
lemma isConjExponent_iff_eq_conjExponent (h : 1 < p) : p.IsConjExponent q ↔ q = p / (p - 1)

Proof state:
p q : ℝ≥0
h : 1 < p
⊢ p.IsConjExponent q ↔ q = p / (p - 1)

Tactic:
rw [← isConjExponent_coe, Real.isConjExponent_iff_eq_conjExponent (mod_cast h), ← coe_inj,
  NNReal.coe_div, NNReal.coe_sub h.le, coe_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem bucket_updateBucket [Hashable α] (self : Array (AssocList α β)) (h : 0 < self.size) (k : α)
    (f : AssocList α β → AssocList α β) :
    bucket (updateBucket self h k f) (by simpa using h) k = f (bucket self h k)

Proof state:
α : Type u
β : α → Type v
inst✝ : Hashable α
self : Array (AssocList α β)
h : 0 < self.size
k : α
f : AssocList α β → AssocList α β
⊢ bucket (updateBucket self h k f) ⋯ k = f (bucket self h k)

Tactic:
unfold bucket updateBucket mkIdx

Result:
α : Type u
β : α → Type v
inst✝ : Hashable α
self : Array (AssocList α β)
h : 0 < self.size
k : α
f : AssocList α β → AssocList α β
⊢ (match
      ⟨(scrambleHash (hash k)).toUSize &&&
          (match ⟨(scrambleHash (hash k)).toUSize &&& self.size.toUSize - 1, ⋯⟩ with
                | ⟨i, h⟩ => self.uset i (f self[i]) h).size.toUSize -
            1,
        ⋯⟩ with
    | ⟨i, h_1⟩ =>
      (match ⟨(scrambleHash (hash k)).toUSize &&& self.size.toUSize - 1, ⋯⟩ with
        | ⟨i, h⟩ => self.uset i (f self[i]) h)[i]) =
    f
      (match ⟨(scrambleHash (hash k)).toUSize &&& self.size.toUSize - 1, ⋯⟩ with
      | ⟨i, h⟩ => self[i])

Proof state:
α : Type u
β : α → Type v
inst✝ : Hashable α
self : Array (AssocList α β)
h : 0 < self.size
k : α
f : AssocList α β → AssocList α β
⊢ (match
      ⟨(scrambleHash (hash k)).toUSize &&&
          (match ⟨(scrambleHash (hash k)).toUSize &&& self.size.toUSize - 1, ⋯⟩ with
                | ⟨i, h⟩ => self.uset i (f self[i]) h).size.toUSize -
            1,
        ⋯⟩ with
    | ⟨i, h_1⟩ =>
      (match ⟨(scrambleHash (hash k)).toUSize &&& self.size.toUSize - 1, ⋯⟩ with
        | ⟨i, h⟩ => self.uset i (f self[i]) h)[i]) =
    f
      (match ⟨(scrambleHash (hash k)).toUSize &&& self.size.toUSize - 1, ⋯⟩ with
      | ⟨i, h⟩ => self[i])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝ : Hashable α
self : Array (AssocList α β)
h : 0 < self.size
k : α
f : AssocList α β → AssocList α β
⊢ 0 < (updateBucket self h k f).size

Tactic:
simpa using h

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.sub' {f g : α → β} (hf : Integrable f μ) (hg : Integrable g μ) :
    Integrable (fun a ↦ f a - g a) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (fun a => f a - g a) μ

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
theorem one_le_evenOdd_zero : 1 ≤ evenOdd Q 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ 1 ≤ LinearMap.range (ι Q) ^ ↑⟨0, ⋯⟩

Tactic:
exact (pow_zero _).ge

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ 1 ≤ evenOdd Q 0

Tactic:
refine le_trans ?_ (le_iSup _ ⟨0, Nat.cast_zero⟩)

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ 1 ≤ LinearMap.range (ι Q) ^ ↑⟨0, ⋯⟩