harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : List β₁) (init : α) :
    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init

Proof state:
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
inst✝ : Monad m
f : β₁ → β₂
g : α → β₂ → m α
l : List β₁
init : α
⊢ List.foldlM g init (map f l) = List.foldlM (fun x y => g x (f y)) init l

Tactic:
induction l generalizing g init <;> simp [*]

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem lookup_insert {a} {b : β a} (s : AList β) : lookup a (insert a b s) = some b

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ lookup a (insert a b s) = some b

Tactic:
simp only [lookup, insert, dlookup_kinsert]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem hasProd_nat_add_iff' {f : ℕ → G} (k : ℕ) :
    HasProd (fun n ↦ f (n + k)) (g / ∏ i ∈ range k, f i) ↔ HasProd f g

Proof state:
G : Type u_2
inst✝² : CommGroup G
g : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ HasProd (fun n => f (n + k)) (g / ∏ i ∈ range k, f i) ↔ HasProd f g

Tactic:
simp [hasProd_nat_add_iff]

Result:
no goals
-- Mathlib/GroupTheory/CommutingProbability.lean
lemma reciprocalFactors_odd {n : ℕ} (h1 : n ≠ 1) (h2 : Odd n) :
    reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1)

Proof state:
n : ℕ
h1 : n ≠ 1
h2 : Odd n
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
h1 : 0 ≠ 1
h2 : Odd 0
⊢ False

Proof state:
n : ℕ
h1 : n ≠ 1
h2 : Odd n
⊢ reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1)

Tactic:
have h0 : n ≠ 0 := by
  rintro rfl
  norm_num [← Nat.not_even_iff_odd] at h2

Result:
n : ℕ
h1 : n ≠ 1
h2 : Odd n
h0 : n ≠ 0
⊢ reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1)

Proof state:
n : ℕ
h1 : n ≠ 1
h2 : Odd n
h0 : n ≠ 0
⊢ reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1)

Tactic:
rw [reciprocalFactors, dif_neg h0, dif_neg h1, if_neg (Nat.not_even_iff_odd.2 h2)]

Result:
no goals

Proof state:
h1 : 0 ≠ 1
h2 : Odd 0
⊢ False

Tactic:
norm_num [← Nat.not_even_iff_odd] at h2

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux {X : TopCat}
    (F : X.Presheaf CommRingCat) {U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens X} {n₁ n₂ : ℕ}
    {y₁ : F.obj (op U₁)} {y₂ : F.obj (op U₂)} {f : F.obj (op <| U₁ ⊔ U₂)}
    {x : F.obj (op U₃)} (h₄₁ : U₄ ≤ U₁) (h₄₂ : U₄ ≤ U₂) (h₅₁ : U₅ ≤ U₁) (h₅₃ : U₅ ≤ U₃)
    (h₆₂ : U₆ ≤ U₂) (h₆₃ : U₆ ≤ U₃) (h₇₄ : U₇ ≤ U₄) (h₇₅ : U₇ ≤ U₅) (h₇₆ : U₇ ≤ U₆)
    (e₁ : y₁ |_ U₅ = (f |_ U₁ |_ U₅) ^ n₁ * x |_ U₅)
    (e₂ : y₂ |_ U₆ = (f |_ U₂ |_ U₆) ^ n₂ * x |_ U₆) :
    (((f |_ U₁) ^ n₂ * y₁) |_ U₄) |_ U₇ = (((f |_ U₂) ^ n₁ * y₂) |_ U₄) |_ U₇

Proof state:
X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op U₃))
h₄₁ : U₄ ≤ U₁
h₄₂ : U₄ ≤ U₂
h₅₁ : U₅ ≤ U₁
h₅₃ : U₅ ≤ U₃
h₆₂ : U₆ ≤ U₂
h₆₃ : U₆ ≤ U₃
h₇₄ : U₇ ≤ U₄
h₇₅ : U₇ ≤ U₅
h₇₆ : U₇ ≤ U₆
e₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
e₂ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂

Tactic:
rw [e₁, e₂, mul_left_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_pow_pos : 0 < ∫ x in (0)..π, sin x ^ n

Proof state:
n : ℕ
⊢ 0 < ∫ (x : ℝ) in 0 ..π, sin x ^ n

Tactic:
rcases even_or_odd' n with ⟨k, rfl | rfl⟩ <;>
simp only [integral_sin_pow_even, integral_sin_pow_odd] <;>
refine mul_pos (by norm_num [pi_pos]) (prod_pos fun n _ => div_pos ?_ ?_) <;>
norm_cast <;>
omega

Result:
no goals

Proof state:
k : ℕ
⊢ 0 < 2

Tactic:
norm_num [pi_pos]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/OneHypercover.lean
@[simp]
lemma preOneHypercover_sieve₀ : S.preOneHypercover.sieve₀ = S.1

Proof state:
case h.mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ (↑S).arrows f → S.preOneHypercover.sieve₀.arrows f

Tactic:
intro hf

Result:
case h.mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
hf : (↑S).arrows f
⊢ S.preOneHypercover.sieve₀.arrows f

Proof state:
case h.mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
hf : (↑S).arrows f
⊢ S.preOneHypercover.sieve₀.arrows f

Tactic:
exact Sieve.ofArrows_mk _ _ ({ hf := hf } : S.Arrow)

Result:
no goals

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ S.preOneHypercover.sieve₀.arrows f ↔ (↑S).arrows f

Tactic:
constructor

Result:
case h.mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ S.preOneHypercover.sieve₀.arrows f → (↑S).arrows f

case h.mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ (↑S).arrows f → S.preOneHypercover.sieve₀.arrows f

Proof state:
case h.mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ S.preOneHypercover.sieve₀.arrows f → (↑S).arrows f

Tactic:
rintro ⟨_, _, _, ⟨g⟩, rfl⟩

Result:
case h.mp.intro.intro.intro.intro.mk
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y✝ Y : C
g : S.preOneHypercover.I₀
w✝ : Y✝ ⟶ S.preOneHypercover.X g
⊢ (↑S).arrows (w✝ ≫ S.preOneHypercover.f g)

Proof state:
case h.mp.intro.intro.intro.intro.mk
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y✝ Y : C
g : S.preOneHypercover.I₀
w✝ : Y✝ ⟶ S.preOneHypercover.X g
⊢ (↑S).arrows (w✝ ≫ S.preOneHypercover.f g)

Tactic:
exact S.1.downward_closed g.hf _

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
⊢ S.preOneHypercover.sieve₀ = ↑S

Tactic:
ext Y f

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ S.preOneHypercover.sieve₀.arrows f ↔ (↑S).arrows f
-- Mathlib/Analysis/Normed/Ring/Units.lean
theorem inverse_add_norm (x : Rˣ) : (fun t : R => inverse (↑x + t)) =O[𝓝 0] fun _t => (1 : ℝ)

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
⊢ (fun x_1 => inverse (1 + ↑x⁻¹ * x_1) * ↑x⁻¹) =O[𝓝 0] fun _t => 1 * 1

Tactic:
simp only [← sub_neg_eq_add, ← neg_mul]

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
⊢ (fun x_1 => inverse (1 - -↑x⁻¹ * x_1) * ↑x⁻¹) =O[𝓝 0] fun _t => 1 * 1

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
⊢ (fun t => inverse (↑x + t)) =O[𝓝 0] fun _t => 1

Tactic:
refine EventuallyEq.trans_isBigO (inverse_add x) (one_mul (1 : ℝ) ▸ ?_)

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
⊢ (fun x_1 => inverse (1 + ↑x⁻¹ * x_1) * ↑x⁻¹) =O[𝓝 0] fun _t => 1 * 1

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
⊢ (fun x_1 => inverse (1 - -↑x⁻¹ * x_1) * ↑x⁻¹) =O[𝓝 0] fun _t => 1 * 1

Tactic:
exact (inverse_one_sub_norm.comp_tendsto hzero).mul (isBigO_const_const _ one_ne_zero _)

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem gcd_a_modEq (a b : ℕ) : (a : ℤ) * Nat.gcdA a b ≡ Nat.gcd a b [ZMOD b]

Proof state:
a b : ℕ
⊢ ↑a * a.gcdA b + 0 ≡ ↑a * a.gcdA b + ↑b * a.gcdB b [ZMOD ↑b]

Tactic:
exact (dvd_mul_right _ _).zero_modEq_int.add_left _

Result:
no goals

Proof state:
a b : ℕ
⊢ ↑a * a.gcdA b ≡ ↑(a.gcd b) [ZMOD ↑b]

Tactic:
rw [← add_zero ((a : ℤ) * _), Nat.gcd_eq_gcd_ab]

Result:
a b : ℕ
⊢ ↑a * a.gcdA b + 0 ≡ ↑a * a.gcdA b + ↑b * a.gcdB b [ZMOD ↑b]
-- Mathlib/Data/Finsupp/Multiset.lean
theorem toMultiset_inf [DecidableEq α] (f g : α →₀ ℕ) :
    toMultiset (f ⊓ g) = toMultiset f ∩ toMultiset g

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
f g : α →₀ ℕ
a✝ : α
⊢ Multiset.count a✝ (toMultiset (f ⊓ g)) = Multiset.count a✝ (toMultiset f ∩ toMultiset g)

Tactic:
simp_rw [Multiset.count_inter, Finsupp.count_toMultiset, Finsupp.inf_apply]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f g : α →₀ ℕ
⊢ toMultiset (f ⊓ g) = toMultiset f ∩ toMultiset g

Tactic:
ext

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
f g : α →₀ ℕ
a✝ : α
⊢ Multiset.count a✝ (toMultiset (f ⊓ g)) = Multiset.count a✝ (toMultiset f ∩ toMultiset g)
-- Mathlib/FieldTheory/Galois/Basic.lean
theorem of_fixedField_eq_bot [FiniteDimensional F E]
    (h : IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E)) = ⊥) : IsGalois F E

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : fixedField ⊤ = ⊥
⊢ IsGalois (↥(fixedField ⊤)) E

Tactic:
exact IsGalois.of_fixed_field E (⊤ : Subgroup (E ≃ₐ[F] E))

Result:
no goals

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : fixedField ⊤ = ⊥
⊢ IsGalois F E

Tactic:
rw [← isGalois_iff_isGalois_bot, ← h]

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : fixedField ⊤ = ⊥
⊢ IsGalois (↥(fixedField ⊤)) E

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : fixedField ⊤ = ⊥
⊢ IsGalois (↥(fixedField ⊤)) E

Tactic:
classical exact IsGalois.of_fixed_field E (⊤ : Subgroup (E ≃ₐ[F] E))

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem JoinedIn.symm (h : JoinedIn F x y) : JoinedIn F y x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ JoinedIn F y x

Tactic:
obtain ⟨hx, hy⟩ := h.mem

Result:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F y x

Proof state:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F y x

Tactic:
simp_all only [joinedIn_iff_joined]

Result:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
hx✝ : x ∈ F
hy✝ : y ∈ F
h : Joined ⟨x, hx✝⟩ ⟨y, hy✝⟩
hx : x ∈ F
hy : y ∈ F
⊢ Joined ⟨y, hy✝⟩ ⟨x, hx✝⟩

Proof state:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
hx✝ : x ∈ F
hy✝ : y ∈ F
h : Joined ⟨x, hx✝⟩ ⟨y, hy✝⟩
hx : x ∈ F
hy : y ∈ F
⊢ Joined ⟨y, hy✝⟩ ⟨x, hx✝⟩

Tactic:
exact h.symm

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
@[norm_cast] lemma cast_div_of_ne_zero (hp : (p.den : α) ≠ 0) (hq : (q.num : α) ≠ 0) :
    ↑(p / q) = (p / q : α)

Proof state:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(p.num * ↑q.den) / ↑(↑p.den * q.num) = ↑p.num * ↑q.den / (↑p.den * ↑q.num)

Tactic:
push_cast

Result:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑p.num * ↑q.den / (↑p.den * ↑q.num) = ↑p.num * ↑q.den / (↑p.den * ↑q.num)

Proof state:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑p.num * ↑q.den / (↑p.den * ↑q.num) = ↑p.num * ↑q.den / (↑p.den * ↑q.num)

Tactic:
rfl

Result:
no goals

Proof state:
case b0
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑p.den * ↑q.num ≠ 0

Tactic:
exact mul_ne_zero hp hq

Result:
no goals

Proof state:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(p / q) = ↑p / ↑q

Tactic:
rw [div_def', cast_divInt_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _), inv_div,
  (Int.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]

Result:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(p.num * ↑q.den) / ↑(↑p.den * q.num) = ↑p.num * ↑q.den / (↑p.den * ↑q.num)

case b0
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(↑p.den * q.num) ≠ 0

Proof state:
case b0
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(↑p.den * q.num) ≠ 0

Tactic:
push_cast

Result:
case b0
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑p.den * ↑q.num ≠ 0
-- Mathlib/Data/ZMod/ValMinAbs.lean
@[simp]
lemma valMinAbs_natCast_eq_self [NeZero n] : (a : ZMod n).valMinAbs = a ↔ a ≤ n / 2

Proof state:
n a : ℕ
inst✝ : NeZero n
ha : (↑a).valMinAbs = ↑a
⊢ a ≤ n / 2

Tactic:
rw [← Int.natAbs_ofNat a, ← ha]

Result:
n a : ℕ
inst✝ : NeZero n
ha : (↑a).valMinAbs = ↑a
⊢ (↑a).valMinAbs.natAbs ≤ n / 2

Proof state:
n a : ℕ
inst✝ : NeZero n
⊢ (↑a).valMinAbs = ↑a ↔ a ≤ n / 2

Tactic:
refine ⟨fun ha => ?_, valMinAbs_natCast_of_le_half⟩

Result:
n a : ℕ
inst✝ : NeZero n
ha : (↑a).valMinAbs = ↑a
⊢ a ≤ n / 2

Proof state:
n a : ℕ
inst✝ : NeZero n
ha : (↑a).valMinAbs = ↑a
⊢ (↑a).valMinAbs.natAbs ≤ n / 2

Tactic:
exact natAbs_valMinAbs_le (n := n) a

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem snd_lt_add_of_mem_zipIdx {x : α × Nat} {l : Array α} {k : Nat} (h : x ∈ zipIdx l k) :
    x.2 < k + l.size

Proof state:
case intro.intro
α : Type u_1
l : Array α
k i : Nat
h' : i < (l.zipIdx k).size
h : (l.zipIdx k)[i] ∈ l.zipIdx k
⊢ (l.zipIdx k)[i].snd < k + l.size

Tactic:
simpa using h'

Result:
no goals

Proof state:
α : Type u_1
x : α × Nat
l : Array α
k : Nat
h : x ∈ l.zipIdx k
⊢ x.snd < k + l.size

Tactic:
rcases mem_iff_getElem.1 h with ⟨i, h', rfl⟩

Result:
case intro.intro
α : Type u_1
l : Array α
k i : Nat
h' : i < (l.zipIdx k).size
h : (l.zipIdx k)[i] ∈ l.zipIdx k
⊢ (l.zipIdx k)[i].snd < k + l.size
-- Mathlib/Data/List/Basic.lean
theorem eq_cons_of_length_one {l : List α} (h : l.length = 1) : l = [l.get ⟨0, by omega⟩]

Proof state:
α : Type u
l : List α
h : l.length = 1
⊢ l.length = [l.get ⟨0, ⋯⟩].length

Tactic:
convert h

Result:
no goals

Proof state:
α : Type u
l : List α
h : l.length = 1
n : ℕ
h₁ : n < l.length
h₂ : n < [l.get ⟨0, ⋯⟩].length
⊢ l.get ⟨n, h₁⟩ = [l.get ⟨0, ⋯⟩].get ⟨n, h₂⟩

Tactic:
simp

Result:
α : Type u
l : List α
h : l.length = 1
n : ℕ
h₁ : n < l.length
h₂ : n < [l.get ⟨0, ⋯⟩].length
⊢ l[n] = l[0]

Proof state:
α : Type u
l : List α
h : l.length = 1
n : ℕ
h₁ : n < l.length
h₂ : n < [l.get ⟨0, ⋯⟩].length
⊢ l[n] = l[0]

Tactic:
congr

Result:
case e_i
α : Type u
l : List α
h : l.length = 1
n : ℕ
h₁ : n < l.length
h₂ : n < [l.get ⟨0, ⋯⟩].length
⊢ n = 0

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ l : List α
h : l.length = 1
⊢ 0 < l.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
l : List α
h : l.length = 1
⊢ l = [l.get ⟨0, ⋯⟩]

Tactic:
refine ext_get (by convert h) fun n h₁ h₂ => ?_

Result:
α : Type u
l : List α
h : l.length = 1
n : ℕ
h₁ : n < l.length
h₂ : n < [l.get ⟨0, ⋯⟩].length
⊢ l.get ⟨n, h₁⟩ = [l.get ⟨0, ⋯⟩].get ⟨n, h₂⟩

Proof state:
case e_i
α : Type u
l : List α
h : l.length = 1
n : ℕ
h₁ : n < l.length
h₂ : n < [l.get ⟨0, ⋯⟩].length
⊢ n = 0

Tactic:
omega

Result:
no goals
-- Mathlib/Order/Monotone/Defs.lean
theorem injective_of_lt_imp_ne [LinearOrder α] {f : α → β} (h : ∀ x y, x < y → f x ≠ f y) :
    Injective f

Proof state:
α : Type u
β : Type v
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
⊢ Injective f

Tactic:
intro x y hf

Result:
α : Type u
β : Type v
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
⊢ x = y

Proof state:
α : Type u
β : Type v
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
⊢ x = y

Tactic:
rcases lt_trichotomy x y with (hxy | rfl | hxy)

Result:
case inl
α : Type u
β : Type v
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
hxy : x < y
⊢ x = y

case inr.inl
α : Type u
β : Type v
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x : α
hf : f x = f x
⊢ x = x

case inr.inr
α : Type u
β : Type v
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
hxy : y < x
⊢ x = y

Proof state:
case inr.inl
α : Type u
β : Type v
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x : α
hf : f x = f x
⊢ x = x

Tactic:
rfl

Result:
no goals

Proof state:
case inl
α : Type u
β : Type v
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
hxy : x < y
⊢ x = y

Tactic:
exact absurd hf <| h _ _ hxy

Result:
no goals

Proof state:
case inr.inr
α : Type u
β : Type v
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
hxy : y < x
⊢ x = y

Tactic:
exact absurd hf.symm <| h _ _ hxy

Result:
no goals
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem Submonoid.square_subsemiringClosure {T : Type*} [CommSemiring T] :
    (Submonoid.square T).subsemiringClosure = .closure {x : T | IsSquare x}

Proof state:
T : Type u_2
inst✝ : CommSemiring T
⊢ (square T).subsemiringClosure = Subsemiring.closure {x | IsSquare x}

Tactic:
simp [Submonoid.subsemiringClosure_eq_closure]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem findIdxs_cons_aux (p : α → Bool) :
    foldrIdx (fun i a is => if p a = true then (i + 1) :: is else is) [] xs s =
      map (· + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs s)

Proof state:
α : Type u_1
xs : List α
s : Nat
p : α → Bool
⊢ foldrIdx (fun i a is => if p a = true then (i + 1) :: is else is) [] xs s =
    map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs s)

Tactic:
induction xs generalizing s with
| nil => rfl
| cons x xs ih =>
  simp only [foldrIdx]
  split <;> simp [ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
s : Nat
⊢ foldrIdx (fun i a is => if p a = true then (i + 1) :: is else is) [] [] s =
    map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] [] s)

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  ∀ {s : Nat},
    foldrIdx (fun i a is => if p a = true then (i + 1) :: is else is) [] xs s =
      map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs s)
s : Nat
⊢ (if p x = true then (s + 1) :: foldrIdx (fun i a is => if p a = true then (i + 1) :: is else is) [] xs (s + 1)
    else foldrIdx (fun i a is => if p a = true then (i + 1) :: is else is) [] xs (s + 1)) =
    map (fun x => x + 1)
      (if p x = true then s :: foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs (s + 1)
      else foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs (s + 1))

Tactic:
split <;> simp [ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  ∀ {s : Nat},
    foldrIdx (fun i a is => if p a = true then (i + 1) :: is else is) [] xs s =
      map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs s)
s : Nat
⊢ foldrIdx (fun i a is => if p a = true then (i + 1) :: is else is) [] (x :: xs) s =
    map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] (x :: xs) s)

Tactic:
simp only [foldrIdx]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  ∀ {s : Nat},
    foldrIdx (fun i a is => if p a = true then (i + 1) :: is else is) [] xs s =
      map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs s)
s : Nat
⊢ (if p x = true then (s + 1) :: foldrIdx (fun i a is => if p a = true then (i + 1) :: is else is) [] xs (s + 1)
    else foldrIdx (fun i a is => if p a = true then (i + 1) :: is else is) [] xs (s + 1)) =
    map (fun x => x + 1)
      (if p x = true then s :: foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs (s + 1)
      else foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs (s + 1))
-- Mathlib/GroupTheory/Complement.lean
@[to_additive (attr := deprecated exists_isComplement_left (since := "2024-12-18"))]
lemma exists_left_transversal (H : Subgroup G) (g : G) :
    ∃ S ∈ leftTransversals (H : Set G), g ∈ S

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ ↑(update Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
refine (Function.update_of_ne ?_ g Quotient.out) ▸ q.out_eq'

Result:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ q ≠ Quotient.mk'' g

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ ↑(update Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
by_cases hq : q = Quotient.mk'' g

Result:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : q = Quotient.mk'' g
⊢ ↑(update Quotient.out (Quotient.mk'' g) g q) = q

case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ ↑(update Quotient.out (Quotient.mk'' g) g q) = q

Proof state:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : q = Quotient.mk'' g
⊢ ↑(update Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
exact hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ q ≠ Quotient.mk'' g

Tactic:
exact hq

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ ∃ S ∈ leftTransversals ↑H, g ∈ S

Tactic:
refine
  ⟨Set.range (Function.update Quotient.out _ g), range_mem_leftTransversals fun q => ?_,
    Quotient.mk'' g, Function.update_self (Quotient.mk'' g) g Quotient.out⟩

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ ↑(update Quotient.out (Quotient.mk'' g) g q) = q
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
theorem PreservesPullback.iso_inv_snd :
    (PreservesPullback.iso G f g).inv ≫ G.map (pullback.snd f g) = pullback.snd _ _

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).inv ≫ G.map (pullback.snd f g) = pullback.snd (G.map f) (G.map g)

Tactic:
simp [PreservesPullback.iso, Iso.inv_comp_eq]

Result:
no goals