harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/ChainOfDivisors.lean
theorem mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors {m p : Associates M}
    {n : Associates N} (hn : n ≠ 0) (hp : p ∈ normalizedFactors m) (d : Set.Iic m ≃o Set.Iic n) :
    (d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : Associates N) ∈ normalizedFactors n

Proof state:
case intro.intro
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : Associated (↑(d ⟨p, ⋯⟩)) q
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n

Tactic:
rw [associated_iff_eq] at hq'

Result:
case intro.intro
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : ↑(d ⟨p, ⋯⟩) = q
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n

Proof state:
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n

Tactic:
obtain ⟨q, hq, hq'⟩ :=
  exists_mem_normalizedFactors_of_dvd hn (map_prime_of_factor_orderIso hn hp d).irreducible
    (d ⟨p, dvd_of_mem_normalizedFactors hp⟩).prop

Result:
case intro.intro
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : Associated (↑(d ⟨p, ⋯⟩)) q
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n

Proof state:
case intro.intro
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : ↑(d ⟨p, ⋯⟩) = q
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n

Tactic:
rwa [hq']

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
/-- `EReal.toENNReal` is multiplicative. For the version with the nonnegativity
hypothesis on the second variable, see `EReal.toENNReal_mul'`. -/
lemma toENNReal_mul {x y : EReal} (hx : 0 ≤ x) :
    (x * y).toENNReal = x.toENNReal * y.toENNReal

Proof state:
case h_top.h_real.inl
hx : 0 ≤ ⊤
a : ℝ
ha : a < 0
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

Tactic:
simp_all [le_of_lt, top_mul_of_neg (EReal.coe_neg'.mpr ha)]

Result:
no goals

Proof state:
case h_real.h_top.inl
a✝ : ℝ
hx✝ : 0 ≤ ↑a✝
hx : 0 = ↑a✝
⊢ (↑a✝ * ⊤).toENNReal = (↑a✝).toENNReal * ⊤.toENNReal

Tactic:
simp [← hx]

Result:
no goals

Proof state:
case h_top.h_top
hx : 0 ≤ ⊤
⊢ (⊤ * ⊤).toENNReal = ⊤.toENNReal * ⊤.toENNReal

Tactic:
simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]

Result:
no goals

Proof state:
case h_top.h_real.inr.inr
hx : 0 ≤ ⊤
a : ℝ
ha : 0 < a
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

Tactic:
simp_all [top_mul_of_pos (EReal.coe_pos.mpr ha)]

Result:
no goals

Proof state:
case h_top.h_real
hx : 0 ≤ ⊤
a✝ : ℝ
⊢ (⊤ * ↑a✝).toENNReal = ⊤.toENNReal * (↑a✝).toENNReal

Tactic:
rename_i a

Result:
case h_top.h_real
hx : 0 ≤ ⊤
a : ℝ
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

Proof state:
case h_top.h_real.inr.inl
hx : 0 ≤ ⊤
a : ℝ
ha : a = 0
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

Tactic:
simp [ha]

Result:
no goals

Proof state:
case h_top.h_real
hx : 0 ≤ ⊤
a : ℝ
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

Tactic:
rcases lt_trichotomy a 0 with (ha | ha | ha)

Result:
case h_top.h_real.inl
hx : 0 ≤ ⊤
a : ℝ
ha : a < 0
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

case h_top.h_real.inr.inl
hx : 0 ≤ ⊤
a : ℝ
ha : a = 0
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

case h_top.h_real.inr.inr
hx : 0 ≤ ⊤
a : ℝ
ha : 0 < a
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

Proof state:
case h_real.h_top
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * ⊤).toENNReal = (↑a✝).toENNReal * ⊤.toENNReal

Tactic:
rcases eq_or_lt_of_le hx with (hx | hx)

Result:
case h_real.h_top.inl
a✝ : ℝ
hx✝ : 0 ≤ ↑a✝
hx : 0 = ↑a✝
⊢ (↑a✝ * ⊤).toENNReal = (↑a✝).toENNReal * ⊤.toENNReal

case h_real.h_top.inr
a✝ : ℝ
hx✝ : 0 ≤ ↑a✝
hx : 0 < ↑a✝
⊢ (↑a✝ * ⊤).toENNReal = (↑a✝).toENNReal * ⊤.toENNReal

Proof state:
case h_real.h_top.inr
a✝ : ℝ
hx✝ : 0 ≤ ↑a✝
hx : 0 < ↑a✝
⊢ (↑a✝ * ⊤).toENNReal = (↑a✝).toENNReal * ⊤.toENNReal

Tactic:
simp_all [mul_top_of_pos hx]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem mk_eq_mk_of_basis (v : Basis ι R M) (v' : Basis ι' R M) :
    Cardinal.lift.{w'} #ι = Cardinal.lift.{w} #ι'

Proof state:
case inr.intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Infinite ι
w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
f : ι ↪ ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
haveI : Infinite ι' := Infinite.of_injective f f.2

Result:
case inr.intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this✝ : Nontrivial R
val✝ : Infinite ι
w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
f : ι ↪ ι'
this : Infinite ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Proof state:
case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Infinite ι
w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
rcases Cardinal.lift_mk_le'.mp w₁ with ⟨f⟩

Result:
case inr.intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Infinite ι
w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
f : ι ↪ ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
-- Mathlib/FieldTheory/Separable.lean
theorem X_pow_sub_one_separable_iff {n : ℕ} : (X ^ n - 1 : F[X]).Separable ↔ (n : F) ≠ 0

Proof state:
F : Type u
inst✝ : Field F
n : ℕ
h : IsUnit (X ^ n - 1)
hn' : ↑n = 0
⊢ False

Tactic:
exact not_isUnit_X_pow_sub_one F n h

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
n : ℕ
⊢ (X ^ n - 1).Separable → ↑n ≠ 0

Tactic:
rw [separable_def', derivative_sub, derivative_X_pow, derivative_one, sub_zero]

Result:
F : Type u
inst✝ : Field F
n : ℕ
⊢ (∃ a b, a * (X ^ n - 1) + b * (C ↑n * X ^ (n - 1)) = 1) → ↑n ≠ 0

Proof state:
F : Type u
inst✝ : Field F
n : ℕ
⊢ (∃ a b, a * (X ^ n - 1) + b * (C ↑n * X ^ (n - 1)) = 1) → ↑n ≠ 0

Tactic:
rintro (h : IsCoprime _ _) hn'

Result:
F : Type u
inst✝ : Field F
n : ℕ
h : IsCoprime (X ^ n - 1) (C ↑n * X ^ (n - 1))
hn' : ↑n = 0
⊢ False

Proof state:
F : Type u
inst✝ : Field F
n : ℕ
h : IsCoprime (X ^ n - 1) (C ↑n * X ^ (n - 1))
hn' : ↑n = 0
⊢ False

Tactic:
rw [hn', C_0, zero_mul, isCoprime_zero_right] at h

Result:
F : Type u
inst✝ : Field F
n : ℕ
h : IsUnit (X ^ n - 1)
hn' : ↑n = 0
⊢ False

Proof state:
F : Type u
inst✝ : Field F
n : ℕ
⊢ (X ^ n - 1).Separable ↔ ↑n ≠ 0

Tactic:
refine ⟨?_, fun h => separable_X_pow_sub_C_unit 1 (IsUnit.mk0 _ h)⟩

Result:
F : Type u
inst✝ : Field F
n : ℕ
⊢ (X ^ n - 1).Separable → ↑n ≠ 0
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem Nat.ModEq.pow_totient {x n : ℕ} (h : Nat.Coprime x n) : x ^ φ n ≡ 1 [MOD n]

Proof state:
x n : ℕ
h : x.Coprime n
x' : (ZMod n)ˣ := unitOfCoprime x h
this : x' ^ φ n = 1
⊢ ↑(x ^ φ n) = ↑1

Tactic:
apply_fun ((fun (x : Units (ZMod n)) => (x : ZMod n)) : Units (ZMod n) → ZMod n) at this

Result:
x n : ℕ
h : x.Coprime n
x' : (ZMod n)ˣ := unitOfCoprime x h
this : ↑(x' ^ φ n) = ↑1
⊢ ↑(x ^ φ n) = ↑1

Proof state:
x n : ℕ
h : x.Coprime n
⊢ x ^ φ n ≡ 1 [MOD n]

Tactic:
rw [← ZMod.eq_iff_modEq_nat]

Result:
x n : ℕ
h : x.Coprime n
⊢ ↑(x ^ φ n) = ↑1

Proof state:
x n : ℕ
h : x.Coprime n
⊢ ↑(x ^ φ n) = ↑1

Tactic:
let x' : Units (ZMod n) := ZMod.unitOfCoprime _ h

Result:
x n : ℕ
h : x.Coprime n
x' : (ZMod n)ˣ := unitOfCoprime x h
⊢ ↑(x ^ φ n) = ↑1

Proof state:
x n : ℕ
h : x.Coprime n
x' : (ZMod n)ˣ := unitOfCoprime x h
⊢ ↑(x ^ φ n) = ↑1

Tactic:
have := ZMod.pow_totient x'

Result:
x n : ℕ
h : x.Coprime n
x' : (ZMod n)ˣ := unitOfCoprime x h
this : x' ^ φ n = 1
⊢ ↑(x ^ φ n) = ↑1

Proof state:
x n : ℕ
h : x.Coprime n
x' : (ZMod n)ˣ := unitOfCoprime x h
this : ↑(x' ^ φ n) = ↑1
⊢ ↑(x ^ φ n) = ↑1

Tactic:
simpa only [Nat.succ_eq_add_one, Nat.cast_pow, Units.val_one, Nat.cast_one,
  coe_unitOfCoprime, Units.val_pow_eq_pow_val]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem codisjoint_subgroupOf_sup (H K : Subgroup G) :
    Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))

Tactic:
rw [codisjoint_iff, sup_subgroupOf_eq, subgroupOf_self]

Result:
case hH
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ≤ H ⊔ K

case hK
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ K ≤ H ⊔ K

Proof state:
case hH
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ≤ H ⊔ K

case hK
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ K ≤ H ⊔ K

Tactic:
exacts [le_sup_left, le_sup_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_mkArray (p : α → Bool) (a : α) (n : Nat) :
    countP p (mkArray n a) = if p a then n else 0

Proof state:
α : Type u_1
p : α → Bool
a : α
n : Nat
⊢ countP p (mkArray n a) = if p a = true then n else 0

Tactic:
simp [← List.toArray_replicate, List.countP_replicate]

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem computable_iff {p : α → Prop} :
    ComputablePred p ↔ ∃ f : α → Bool, Computable f ∧ p = fun a => (f a : Prop) :=
  ⟨fun ⟨_, h⟩ => ⟨_, h, funext fun _ => propext (Bool.decide_iff _).symm⟩, by
    rintro ⟨f, h, rfl⟩; exact ⟨by infer_instance, by simpa using h⟩⟩

Proof state:
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
h : Computable f
⊢ Computable fun a => decide ((fun a => f a = true) a)

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
h : Computable f
⊢ DecidablePred fun a => f a = true

Tactic:
infer_instance

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
h : Computable f
⊢ ComputablePred fun a => f a = true

Tactic:
exact ⟨by infer_instance, by simpa using h⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Primcodable α
p : α → Prop
⊢ (∃ f, Computable f ∧ p = fun a => f a = true) → ComputablePred p

Tactic:
rintro ⟨f, h, rfl⟩

Result:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
h : Computable f
⊢ ComputablePred fun a => f a = true
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive (attr := simp) norm_le_zero_iff]
lemma norm_le_zero_iff' : ‖a‖ ≤ 0 ↔ a = 1

Proof state:
E : Type u_5
inst✝ : NormedGroup E
a : E
⊢ ‖a‖ ≤ 0 ↔ a = 1

Tactic:
rw [← dist_one_right, dist_le_zero]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Division.lean
theorem monomial_dvd_monomial {r s : R} {i j : σ →₀ ℕ} :
    monomial i r ∣ monomial j s ↔ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Proof state:
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m ((monomial j) s) = coeff m ((monomial i) r * x)
hi : (if j = i then s else 0) = coeff i ((monomial i) r * x)
hj : s = coeff j ((monomial i) r * x)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Tactic:
simp_rw [coeff_monomial_mul'] at hi hj

Result:
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m ((monomial j) s) = coeff m ((monomial i) r * x)
hi : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hj : s = if i ≤ j then r * coeff (j - i) x else 0
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Proof state:
case mp
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
⊢ (monomial i) r ∣ (monomial j) s → (s = 0 ∨ i ≤ j) ∧ r ∣ s

Tactic:
rintro ⟨x, hx⟩

Result:
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : (monomial j) s = (monomial i) r * x
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Proof state:
case mpr.intro.inr.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r : R
i j : σ →₀ ℕ
hij : i ≤ j
d : R
⊢ (monomial j) (r * d) = (monomial i) r * (monomial (j - i)) d

Tactic:
rw [monomial_mul, add_tsub_cancel_of_le hij]

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem xgcdAux_fst (x y : R) : ∀ s t s' t', (xgcdAux x s t y s' t').1 = gcd x y :=
  GCD.induction x y
    (by
      intros
      rw [xgcd_zero_left, gcd_zero_left])
    fun x y h IH s t s' t' => by
    simp only [xgcdAux_rec h, if_neg h, IH]
    rw [← gcd_val]

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ ∀ (x s t s' t' : R), (xgcdAux 0 s t x s' t').1 = gcd 0 x

Tactic:
intros

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y x✝ s✝ t✝ s'✝ t'✝ : R
⊢ (xgcdAux 0 s✝ t✝ x✝ s'✝ t'✝).1 = gcd 0 x✝

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x✝ y✝ x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').1 = gcd (y % x) x
s t s' t' : R
⊢ (xgcdAux x s t y s' t').1 = gcd x y

Tactic:
simp only [xgcdAux_rec h, if_neg h, IH]

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x✝ y✝ x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').1 = gcd (y % x) x
s t s' t' : R
⊢ gcd (y % x) x = gcd x y

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y x✝ s✝ t✝ s'✝ t'✝ : R
⊢ (xgcdAux 0 s✝ t✝ x✝ s'✝ t'✝).1 = gcd 0 x✝

Tactic:
rw [xgcd_zero_left, gcd_zero_left]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x✝ y✝ x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').1 = gcd (y % x) x
s t s' t' : R
⊢ gcd (y % x) x = gcd x y

Tactic:
rw [← gcd_val]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem length_mapFinIdx_go :
    (mapFinIdx.go as f bs acc h).length = as.length

Proof state:
case nil
α✝¹ : Type u_1
as : List α✝¹
α✝ : Type u_2
f : (i : Nat) → α✝¹ → i < as.length → α✝
acc : Array α✝
h : [].length + acc.size = as.length
⊢ (mapFinIdx.go as f [] acc h).length = as.length

Tactic:
simpa using h

Result:
no goals

Proof state:
α✝¹ : Type u_1
as : List α✝¹
α✝ : Type u_2
f : (i : Nat) → α✝¹ → i < as.length → α✝
bs : List α✝¹
acc : Array α✝
h : bs.length + acc.size = as.length
⊢ (mapFinIdx.go as f bs acc h).length = as.length

Tactic:
induction bs generalizing acc with
| nil => simpa using h
| cons _ _ ih => simp [mapFinIdx.go, ih]

Result:
no goals

Proof state:
case cons
α✝¹ : Type u_1
as : List α✝¹
α✝ : Type u_2
f : (i : Nat) → α✝¹ → i < as.length → α✝
head✝ : α✝¹
tail✝ : List α✝¹
ih : ∀ {acc : Array α✝} {h : tail✝.length + acc.size = as.length}, (mapFinIdx.go as f tail✝ acc h).length = as.length
acc : Array α✝
h : (head✝ :: tail✝).length + acc.size = as.length
⊢ (mapFinIdx.go as f (head✝ :: tail✝) acc h).length = as.length

Tactic:
simp [mapFinIdx.go, ih]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
lemma IsSeparable.of_equiv_equiv {x : B₁} (h : IsSeparable A₁ x) : IsSeparable A₂ (e₂ x) :=
  letI := e₁.toRingHom.toAlgebra
  letI : Algebra A₂ B₁ :=
    { (algebraMap A₁ B₁).comp e₁.symm.toRingHom with
        smul := fun a b ↦ ((algebraMap A₁ B₁).comp e₁.symm.toRingHom a) * b
        commutes' := fun r x ↦ (Algebra.commutes) (e₁.symm.toRingHom r) x
        smul_def' := fun _ _ ↦ rfl }
  haveI : IsScalarTower A₁ A₂ B₁ := IsScalarTower.of_algebraMap_eq <| fun x ↦
      (algebraMap A₁ B₁).congr_arg <| id ((e₁.symm_apply_apply x).symm)
  let e : B₁ ≃ₐ[A₂] B₂ :=
    { e₂ with
      commutes' := fun x ↦ by
        simpa [RingHom.algebraMap_toAlgebra] using DFunLike.congr_fun he.symm (e₁.symm x) }
  (AlgEquiv.isSeparable_iff e).mpr <| IsSeparable.tower_top A₂ h

Proof state:
A₁ : Type u_1
B₁ : Type u_2
A₂ : Type u_3
B₂ : Type u_4
inst✝⁵ : Field A₁
inst✝⁴ : Ring B₁
inst✝³ : Field A₂
inst✝² : Ring B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x✝ : B₁
h : IsSeparable A₁ x✝
this✝¹ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this✝ : Algebra A₂ B₁ :=
  let __src := (algebraMap A₁ B₁).comp e₁.symm.toRingHom;
  Algebra.mk ((algebraMap A₁ B₁).comp e₁.symm.toRingHom) ⋯ ⋯
this : IsScalarTower A₁ A₂ B₁
x : A₂
⊢ e₂.toFun ((algebraMap A₂ B₁) x) = (algebraMap A₂ B₂) x

Tactic:
simpa [RingHom.algebraMap_toAlgebra] using DFunLike.congr_fun he.symm (e₁.symm x)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem Fin.circulant_isSymm_iff : ∀ {n} {v : Fin n → α}, (circulant v).IsSymm ↔ ∀ i, v (-i) = v i
  | 0 => by simp [IsSymm.ext_iff, IsEmpty.forall_iff]
  | _ + 1 => Matrix.circulant_isSymm_iff

Proof state:
α : Type u_1
v✝ : Fin 0 → α
⊢ (circulant v✝).IsSymm ↔ ∀ (i : Fin 0), v✝ (-i) = v✝ i

Tactic:
simp [IsSymm.ext_iff, IsEmpty.forall_iff]

Result:
no goals
-- Mathlib/Topology/TietzeExtension.lean
theorem exists_forall_mem_restrict_eq_of_closed {s : Set Y} (f : s →ᵇ ℝ) (hs : IsClosed s)
    {t : Set ℝ} [OrdConnected t] (hf : ∀ x, f x ∈ t) (hne : t.Nonempty) :
    ∃ g : Y →ᵇ ℝ, (∀ y, g y ∈ t) ∧ g.restrict s = f

Proof state:
case intro.intro
Y : Type u_2
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
s : Set Y
f : ↑s →ᵇ ℝ
hs : IsClosed s
t : Set ℝ
inst✝ : t.OrdConnected
hf : ∀ (x : ↑s), f x ∈ t
hne : t.Nonempty
g : Y →ᵇ ℝ
hg : ∀ (y : Y), g y ∈ t
hgf : ⇑g ∘ Subtype.val = ⇑f
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ g.restrict s = f

Tactic:
exact ⟨g, hg, DFunLike.coe_injective hgf⟩

Result:
no goals

Proof state:
Y : Type u_2
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
s : Set Y
f : ↑s →ᵇ ℝ
hs : IsClosed s
t : Set ℝ
inst✝ : t.OrdConnected
hf : ∀ (x : ↑s), f x ∈ t
hne : t.Nonempty
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ g.restrict s = f

Tactic:
obtain ⟨g, hg, hgf⟩ :=
  exists_extension_forall_mem_of_isClosedEmbedding f hf hne hs.isClosedEmbedding_subtypeVal

Result:
case intro.intro
Y : Type u_2
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
s : Set Y
f : ↑s →ᵇ ℝ
hs : IsClosed s
t : Set ℝ
inst✝ : t.OrdConnected
hf : ∀ (x : ↑s), f x ∈ t
hne : t.Nonempty
g : Y →ᵇ ℝ
hg : ∀ (y : Y), g y ∈ t
hgf : ⇑g ∘ Subtype.val = ⇑f
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ g.restrict s = f
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Products.lean
/-- If `sigma_comparison G f` is an isomorphism, then `G` preserves the colimit of `f`. -/
lemma PreservesCoproduct.of_iso_comparison [i : IsIso (sigmaComparison G f)] :
    PreservesColimit (Discrete.functor f) G

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun j => G.obj (f j)
i : IsIso (sigmaComparison G f)
⊢ IsColimit (Cofan.mk (G.obj (∐ f)) fun j => G.map (Sigma.ι f j))

Tactic:
exact @IsColimit.ofPointIso _ _ _ _ _ _ _
  (colimit.isColimit (Discrete.functor fun j : J => G.obj (f j))) i

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun j => G.obj (f j)
i : IsIso (sigmaComparison G f)
⊢ IsColimit (G.mapCocone (Cofan.mk (∐ f) (Sigma.ι f)))

Tactic:
apply (isColimitMapCoconeCofanMkEquiv _ _ _).symm _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun j => G.obj (f j)
i : IsIso (sigmaComparison G f)
⊢ IsColimit (Cofan.mk (G.obj (∐ f)) fun j => G.map (Sigma.ι f j))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun j => G.obj (f j)
i : IsIso (sigmaComparison G f)
⊢ PreservesColimit (Discrete.functor f) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (coproductIsCoproduct f)

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun j => G.obj (f j)
i : IsIso (sigmaComparison G f)
⊢ IsColimit (G.mapCocone (Cofan.mk (∐ f) (Sigma.ι f)))
-- Mathlib/ModelTheory/DirectLimit.lean
theorem comp_unify {α : Type*} {x : α → Σˣ f} {i j : ι} (ij : i ≤ j)
    (h : i ∈ upperBounds (range (Sigma.fst ∘ x))) :
    f i j ij ∘ unify f x i h = unify f x j
      fun k hk => _root_.trans (mem_upperBounds.1 h k hk) ij

Proof state:
L : Language
ι : Type v
inst✝² : Preorder ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
α : Type u_1
x : α → Σˣ f
i j : ι
ij : i ≤ j
h : i ∈ upperBounds (range (Sigma.fst ∘ x))
⊢ ⇑(f i j ij) ∘ unify f x i h = unify f x j ⋯

Tactic:
ext a

Result:
case h
L : Language
ι : Type v
inst✝² : Preorder ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
α : Type u_1
x : α → Σˣ f
i j : ι
ij : i ≤ j
h : i ∈ upperBounds (range (Sigma.fst ∘ x))
a : α
⊢ (⇑(f i j ij) ∘ unify f x i h) a = unify f x j ⋯ a

Proof state:
case h
L : Language
ι : Type v
inst✝² : Preorder ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
α : Type u_1
x : α → Σˣ f
i j : ι
ij : i ≤ j
h : i ∈ upperBounds (range (Sigma.fst ∘ x))
a : α
⊢ (⇑(f i j ij) ∘ unify f x i h) a = unify f x j ⋯ a

Tactic:
simp [unify, DirectedSystem.map_map]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorComm_symm (i j : A) :
    (shiftFunctorComm C i j).symm = shiftFunctorComm C j i

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ (shiftFunctorComm C i j).symm = shiftFunctorComm C j i

Tactic:
ext1

Result:
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ (shiftFunctorComm C i j).symm.hom = (shiftFunctorComm C j i).hom

Proof state:
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ ((shiftFunctorAdd' C i j (i + j) ⋯).symm ≪≫ shiftFunctorAdd' C j i (i + j) ⋯).inv =
    ((shiftFunctorAdd' C j i (i + j) ⋯).symm ≪≫ shiftFunctorAdd' C i j (i + j) ⋯).hom

Tactic:
rfl

Result:
no goals

Proof state:
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ (shiftFunctorComm C i j).symm.hom = (shiftFunctorComm C j i).hom

Tactic:
dsimp

Result:
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ (shiftFunctorComm C i j).inv = (shiftFunctorComm C j i).hom

Proof state:
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ (shiftFunctorComm C i j).inv = (shiftFunctorComm C j i).hom

Tactic:
rw [shiftFunctorComm_eq C i j (i+j) rfl, shiftFunctorComm_eq C j i (i+j) (add_comm j i)]

Result:
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ ((shiftFunctorAdd' C i j (i + j) ⋯).symm ≪≫ shiftFunctorAdd' C j i (i + j) ⋯).inv =
    ((shiftFunctorAdd' C j i (i + j) ⋯).symm ≪≫ shiftFunctorAdd' C i j (i + j) ⋯).hom