harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem eq_single_iff_length {n : ℕ} (h : 0 < n) {c : Composition n} :
    c = single n h ↔ c.length = 1

Proof state:
case mpr.blocks
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
⊢ c.blocks = (single n h).blocks

Tactic:
have A : c.blocks.length = 1 := H ▸ c.blocks_length

Result:
case mpr.blocks
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
A : c.blocks.length = 1
⊢ c.blocks = (single n h).blocks

Proof state:
case mp
n : ℕ
h : 0 < n
c : Composition n
⊢ c = single n h → c.length = 1

Tactic:
intro H

Result:
case mp
n : ℕ
h : 0 < n
c : Composition n
H : c = single n h
⊢ c.length = 1

Proof state:
case mp
n : ℕ
h : 0 < n
c : Composition n
H : c = single n h
⊢ c.length = 1

Tactic:
rw [H]

Result:
case mp
n : ℕ
h : 0 < n
c : Composition n
H : c = single n h
⊢ (single n h).length = 1

Proof state:
case mpr.blocks
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
A : c.blocks.length = 1
B : c.blocks.sum = n
⊢ c.blocks = (single n h).blocks

Tactic:
rw [eq_cons_of_length_one A] at B ⊢

Result:
case mpr.blocks
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
A : c.blocks.length = 1
B : [c.blocks.get ⟨0, ⋯⟩].sum = n
⊢ [c.blocks.get ⟨0, ⋯⟩] = (single n h).blocks

Proof state:
case mpr
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
⊢ c = single n h

Tactic:
ext1

Result:
case mpr.blocks
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
⊢ c.blocks = (single n h).blocks

Proof state:
case mpr.blocks
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
A : c.blocks.length = 1
⊢ c.blocks = (single n h).blocks

Tactic:
have B : c.blocks.sum = n := c.blocks_sum

Result:
case mpr.blocks
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
A : c.blocks.length = 1
B : c.blocks.sum = n
⊢ c.blocks = (single n h).blocks

Proof state:
case mpr.blocks
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
A : c.blocks.length = 1
B : [c.blocks.get ⟨0, ⋯⟩].sum = n
⊢ [c.blocks.get ⟨0, ⋯⟩] = (single n h).blocks

Tactic:
simpa [single_blocks] using B

Result:
no goals

Proof state:
n : ℕ
h : 0 < n
c : Composition n
⊢ c = single n h ↔ c.length = 1

Tactic:
constructor

Result:
case mp
n : ℕ
h : 0 < n
c : Composition n
⊢ c = single n h → c.length = 1

case mpr
n : ℕ
h : 0 < n
c : Composition n
⊢ c.length = 1 → c = single n h

Proof state:
case mpr
n : ℕ
h : 0 < n
c : Composition n
⊢ c.length = 1 → c = single n h

Tactic:
intro H

Result:
case mpr
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
⊢ c = single n h

Proof state:
case mp
n : ℕ
h : 0 < n
c : Composition n
H : c = single n h
⊢ (single n h).length = 1

Tactic:
exact single_length h

Result:
no goals
-- Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean
lemma support_prod (s : Finset ι) (f : ι → κ → M₀) :
    support (fun j ↦ ∏ i ∈ s, f i j) = ⋂ i ∈ s, support (f i) :=
  Set.ext fun x ↦ by simp [support, prod_eq_zero_iff]

Proof state:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
s : Finset ι
f : ι → κ → M₀
x : κ
⊢ (x ∈ support fun j => ∏ i ∈ s, f i j) ↔ x ∈ ⋂ i ∈ s, support (f i)

Tactic:
simp [support, prod_eq_zero_iff]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem mem_closedBall_iff_norm'' : b ∈ closedBall a r ↔ ‖b / a‖ ≤ r

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖b / a‖ ≤ r

Tactic:
rw [mem_closedBall, dist_eq_norm_div]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zip_map (f : α → γ) (g : β → δ) (l₁ : Array α) (l₂ : Array β) :
    zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)

Proof state:
α : Type u_1
γ : Type u_2
β : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
l₁ : Array α
l₂ : Array β
⊢ (map f l₁).zip (map g l₂) = map (Prod.map f g) (l₁.zip l₂)

Tactic:
cases l₁

Result:
case mk
α : Type u_1
γ : Type u_2
β : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
l₂ : Array β
toList✝ : List α
⊢ (map f { toList := toList✝ }).zip (map g l₂) = map (Prod.map f g) ({ toList := toList✝ }.zip l₂)

Proof state:
case mk
α : Type u_1
γ : Type u_2
β : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
l₂ : Array β
toList✝ : List α
⊢ (map f { toList := toList✝ }).zip (map g l₂) = map (Prod.map f g) ({ toList := toList✝ }.zip l₂)

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
γ : Type u_2
β : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
toList✝¹ : List α
toList✝ : List β
⊢ (map f { toList := toList✝¹ }).zip (map g { toList := toList✝ }) =
    map (Prod.map f g) ({ toList := toList✝¹ }.zip { toList := toList✝ })

Proof state:
case mk.mk
α : Type u_1
γ : Type u_2
β : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
toList✝¹ : List α
toList✝ : List β
⊢ (map f { toList := toList✝¹ }).zip (map g { toList := toList✝ }) =
    map (Prod.map f g) ({ toList := toList✝¹ }.zip { toList := toList✝ })

Tactic:
simp [List.zip_map]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem comap_map_eq_self {f : F} {p : Submodule R M} (h : LinearMap.ker f ≤ p) :
    comap f (map f p) = p

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_8
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R M
h : LinearMap.ker f ≤ p
⊢ comap f (map f p) = p

Tactic:
rw [Submodule.comap_map_eq, sup_of_le_left h]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma genEigenspace_le_smul (f : Module.End R M) (μ t : R) (k : ℕ∞) :
    (f.genEigenspace μ k) ≤ (t • f).genEigenspace (t * μ) k

Proof state:
case h.h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), ((f - μ • 1) ^ l) m = 0
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ • 1) ^ l) m = 0
⊢ ((t • f - (t * μ) • 1) ^ l) m = 0

Tactic:
rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hl, smul_zero]

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
⊢ (f.genEigenspace μ) k ≤ ((t • f).genEigenspace (t * μ)) k

Tactic:
intro m hm

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : m ∈ (f.genEigenspace μ) k
⊢ m ∈ ((t • f).genEigenspace (t * μ)) k

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : m ∈ (f.genEigenspace μ) k
⊢ m ∈ ((t • f).genEigenspace (t * μ)) k

Tactic:
simp_rw [mem_genEigenspace, ← exists_prop, LinearMap.mem_ker] at hm ⊢

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), ((f - μ • 1) ^ l) m = 0
⊢ ∃ l, ∃ (_ : ↑l ≤ k), ((t • f - (t * μ) • 1) ^ l) m = 0

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), ((f - μ • 1) ^ l) m = 0
⊢ ∃ l, ∃ (_ : ↑l ≤ k), ((t • f - (t * μ) • 1) ^ l) m = 0

Tactic:
peel hm with l hlk hl

Result:
case h.h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), ((f - μ • 1) ^ l) m = 0
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ • 1) ^ l) m = 0
⊢ ((t • f - (t * μ) • 1) ^ l) m = 0
-- Mathlib/Data/Real/Irrational.lean
theorem mul_rat (h : Irrational x) {q : ℚ} (hq : q ≠ 0) : Irrational (x * q) :=
  of_mul_rat q⁻¹ <| by rwa [mul_assoc, ← cast_mul, mul_inv_cancel₀ hq, cast_one, mul_one]

Proof state:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * ↑q * ↑q⁻¹)

Tactic:
rwa [mul_assoc, ← cast_mul, mul_inv_cancel₀ hq, cast_one, mul_one]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
lemma indicator_const_mul (s : Set ι) (f : ι → M₀) (a : M₀) (i : ι) :
    s.indicator (a * f ·) i = a * s.indicator f i

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f : ι → M₀
a : M₀
i : ι
⊢ s.indicator (fun x => a * f x) i = a * s.indicator f i

Tactic:
rw [indicator_mul_right]

Result:
no goals
-- Mathlib/Order/KonigLemma.lean
theorem exists_orderEmbedding_covby_of_forall_covby_finite_of_bot [OrderBot α] [Infinite α]
    (hfin : ∀ (a : α), {x | a ⋖ x}.Finite) : ∃ f : ℕ ↪o α, f 0 = ⊥ ∧ ∀ i, f i ⋖ f (i+1) :=
  exists_orderEmbedding_covby_of_forall_covby_finite hfin (by simpa using infinite_univ)

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : IsStronglyAtomic α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
⊢ (Ici ⊥).Infinite

Tactic:
simpa using infinite_univ

Result:
no goals
-- Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean
theorem antidiagonalTuple_two (n : ℕ) :
    antidiagonalTuple 2 n = (antidiagonal n).map fun i => ![i.1, i.2]

Proof state:
n : ℕ
⊢ flatMap (fun ni => [Fin.cons ni.1 ![ni.2]]) (antidiagonal n) = map (fun i => ![i.1, i.2]) (antidiagonal n)

Tactic:
rw [List.map_eq_flatMap]

Result:
n : ℕ
⊢ flatMap (fun ni => [Fin.cons ni.1 ![ni.2]]) (antidiagonal n) = flatMap (fun x => [![x.1, x.2]]) (antidiagonal n)

Proof state:
n : ℕ
⊢ flatMap (fun ni => [Fin.cons ni.1 ![ni.2]]) (antidiagonal n) = flatMap (fun x => [![x.1, x.2]]) (antidiagonal n)

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ antidiagonalTuple 2 n = map (fun i => ![i.1, i.2]) (antidiagonal n)

Tactic:
rw [antidiagonalTuple]

Result:
n : ℕ
⊢ flatMap (fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple 1 ni.2)) (antidiagonal n) =
    map (fun i => ![i.1, i.2]) (antidiagonal n)

Proof state:
n : ℕ
⊢ flatMap (fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple 1 ni.2)) (antidiagonal n) =
    map (fun i => ![i.1, i.2]) (antidiagonal n)

Tactic:
simp_rw [antidiagonalTuple_one, List.map_singleton]

Result:
n : ℕ
⊢ flatMap (fun ni => [Fin.cons ni.1 ![ni.2]]) (antidiagonal n) = map (fun i => ![i.1, i.2]) (antidiagonal n)
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem coeff_sum {s : Finset α} {x : α → HahnSeries Γ R} (g : Γ) :
    (∑ i ∈ s, x i).coeff g = ∑ i ∈ s, (x i).coeff g :=
  cons_induction rfl (fun i s his hsum => by rw [sum_cons, sum_cons, coeff_add, hsum]) s

Proof state:
Γ : Type u_1
R : Type u_3
α : Type u_7
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s✝ : Finset α
x : α → HahnSeries Γ R
g : Γ
i : α
s : Finset α
his : i ∉ s
hsum : (∑ i ∈ s, x i).coeff g = ∑ i ∈ s, (x i).coeff g
⊢ (∑ i ∈ cons i s his, x i).coeff g = ∑ i ∈ cons i s his, (x i).coeff g

Tactic:
rw [sum_cons, sum_cons, coeff_add, hsum]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem mk'_d_1_0 : (mk' X₀ X₁ d₀ succ').d 1 0 = d₀

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ (if 1 = 0 + 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀

Tactic:
rw [if_pos rfl, Category.id_comp]

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ (mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').d 1 0 = d₀

Tactic:
change ite (1 = 0 + 1) (𝟙 X₁ ≫ d₀) 0 = d₀

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ (if 1 = 0 + 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem coeHom_injective : Function.Injective (coeHom E F)

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
⊢ Function.Injective DFunLike.coe

Tactic:
exact DFunLike.coe_injective

Result:
no goals

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
⊢ Function.Injective ⇑(coeHom E F)

Tactic:
rw [coe_coeHom]

Result:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
⊢ Function.Injective DFunLike.coe
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_indicator_one {s : Set α} (hs : MeasurableSet s) :
    μ.withDensity (s.indicator 1) = μ.restrict s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ μ.withDensity (s.indicator 1) = μ.restrict s

Tactic:
rw [withDensity_indicator hs, withDensity_one]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_natCast {n : ℕ} (a : ℕ) : (a : ZMod n).val = a % n

Proof state:
case zero
a : ℕ
⊢ (↑a).val = a

Tactic:
exact Int.natAbs_ofNat a

Result:
no goals

Proof state:
case succ
a n✝ : ℕ
⊢ (↑a).val = a % (n✝ + 1)

Tactic:
apply Fin.val_natCast

Result:
no goals

Proof state:
n a : ℕ
⊢ (↑a).val = a % n

Tactic:
cases n

Result:
case zero
a : ℕ
⊢ (↑a).val = a % 0

case succ
a n✝ : ℕ
⊢ (↑a).val = a % (n✝ + 1)

Proof state:
case zero
a : ℕ
⊢ (↑a).val = a % 0

Tactic:
rw [Nat.mod_zero]

Result:
case zero
a : ℕ
⊢ (↑a).val = a
-- Mathlib/GroupTheory/GroupAction/FixedPoints.lean
theorem set_mem_fixedBy_of_subset_fixedBy {s : Set α} {g : G} (s_ss_fixedBy : s ⊆ fixedBy α g) :
    s ∈ fixedBy (Set α) g

Proof state:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
⊢ x ∈ g⁻¹ • s ↔ x ∈ s

Tactic:
rw [Set.mem_inv_smul_set_iff]

Result:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
⊢ g • x ∈ s ↔ x ∈ s

Proof state:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
⊢ s ∈ fixedBy (Set α) g⁻¹

Tactic:
ext x

Result:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
⊢ x ∈ g⁻¹ • s ↔ x ∈ s

Proof state:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
⊢ g • x ∈ s ↔ x ∈ s

Tactic:
refine ⟨fun gxs => ?xs, fun xs => (s_ss_fixedBy xs).symm ▸ xs⟩

Result:
case xs
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
gxs : g • x ∈ s
⊢ x ∈ s

Proof state:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
⊢ s ∈ fixedBy (Set α) g

Tactic:
rw [← fixedBy_inv]

Result:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
⊢ s ∈ fixedBy (Set α) g⁻¹

Proof state:
case xs
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g⁻¹
x : α
gxs : g • x ∈ s
⊢ x ∈ s

Tactic:
rwa [← s_ss_fixedBy gxs, inv_smul_smul] at gxs

Result:
no goals

Proof state:
case xs
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
gxs : g • x ∈ s
⊢ x ∈ s

Tactic:
rw [← fixedBy_inv] at s_ss_fixedBy

Result:
case xs
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g⁻¹
x : α
gxs : g • x ∈ s
⊢ x ∈ s
-- Mathlib/Data/List/GetD.lean
theorem getD_eq_getElem {n : ℕ} (hn : n < l.length) : l.getD n d = l[n]

Proof state:
case cons
α : Type u
l : List α
d head : α
tail : List α
ih : ∀ {n : ℕ} (hn : n < tail.length), tail.getD n d = tail[n]
n : ℕ
hn : n < (head :: tail).length
⊢ (head :: tail).getD n d = (head :: tail)[n]

Tactic:
cases n

Result:
case cons.zero
α : Type u
l : List α
d head : α
tail : List α
ih : ∀ {n : ℕ} (hn : n < tail.length), tail.getD n d = tail[n]
hn : 0 < (head :: tail).length
⊢ (head :: tail).getD 0 d = (head :: tail)[0]

case cons.succ
α : Type u
l : List α
d head : α
tail : List α
ih : ∀ {n : ℕ} (hn : n < tail.length), tail.getD n d = tail[n]
n✝ : ℕ
hn : n✝ + 1 < (head :: tail).length
⊢ (head :: tail).getD (n✝ + 1) d = (head :: tail)[n✝ + 1]

Proof state:
case cons.zero
α : Type u
l : List α
d head : α
tail : List α
ih : ∀ {n : ℕ} (hn : n < tail.length), tail.getD n d = tail[n]
hn : 0 < (head :: tail).length
⊢ (head :: tail).getD 0 d = (head :: tail)[0]

Tactic:
exact getD_cons_zero

Result:
no goals

Proof state:
case cons.succ
α : Type u
l : List α
d head : α
tail : List α
ih : ∀ {n : ℕ} (hn : n < tail.length), tail.getD n d = tail[n]
n✝ : ℕ
hn : n✝ + 1 < (head :: tail).length
⊢ (head :: tail).getD (n✝ + 1) d = (head :: tail)[n✝ + 1]

Tactic:
exact ih _

Result:
no goals

Proof state:
case nil
α : Type u
l : List α
d : α
n : ℕ
hn : n < [].length
⊢ [].getD n d = [][n]

Tactic:
simp at hn

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem prod_self_eq_iUnion_perm (hf : f.IsCycleOn s) :
    s ×ˢ s = ⋃ n : ℤ, (fun a => (a, (f ^ n) a)) '' s

Proof state:
case h.mk.refine_1.intro
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a : α
n : ℤ
hx : a ∈ s ∧ (f ^ n) a ∈ s
⊢ ∃ i, ∃ x ∈ s, (x, (f ^ i) x) = (a, (f ^ n) a)

Tactic:
exact ⟨_, _, hx.1, rfl⟩

Result:
no goals

Proof state:
case h.mk.refine_2.intro.intro.intro.refl
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a : α
n : ℤ
ha : a ∈ s
⊢ a ∈ s ∧ (f ^ n) a ∈ s

Tactic:
exact ⟨ha, (hf.1.perm_zpow _).mapsTo ha⟩

Result:
no goals

Proof state:
case h.mk.refine_2
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
⊢ (∃ i, ∃ x ∈ s, (x, (f ^ i) x) = (a, b)) → a ∈ s ∧ b ∈ s

Tactic:
rintro ⟨n, a, ha, ⟨⟩⟩

Result:
case h.mk.refine_2.intro.intro.intro.refl
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a : α
n : ℤ
ha : a ∈ s
⊢ a ∈ s ∧ (f ^ n) a ∈ s

Proof state:
case h.mk
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
⊢ a ∈ s ∧ b ∈ s ↔ ∃ i, ∃ x ∈ s, (x, (f ^ i) x) = (a, b)

Tactic:
refine ⟨fun hx => ?_, ?_⟩

Result:
case h.mk.refine_1
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
hx : a ∈ s ∧ b ∈ s
⊢ ∃ i, ∃ x ∈ s, (x, (f ^ i) x) = (a, b)

case h.mk.refine_2
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
⊢ (∃ i, ∃ x ∈ s, (x, (f ^ i) x) = (a, b)) → a ∈ s ∧ b ∈ s

Proof state:
case h.mk.refine_1
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
hx : a ∈ s ∧ b ∈ s
⊢ ∃ i, ∃ x ∈ s, (x, (f ^ i) x) = (a, b)

Tactic:
obtain ⟨n, rfl⟩ := hf.2 hx.1 hx.2

Result:
case h.mk.refine_1.intro
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a : α
n : ℤ
hx : a ∈ s ∧ (f ^ n) a ∈ s
⊢ ∃ i, ∃ x ∈ s, (x, (f ^ i) x) = (a, (f ^ n) a)

Proof state:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
⊢ s ×ˢ s = ⋃ n, (fun a => (a, (f ^ n) a)) '' s

Tactic:
ext ⟨a, b⟩

Result:
case h.mk
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
⊢ (a, b) ∈ s ×ˢ s ↔ (a, b) ∈ ⋃ n, (fun a => (a, (f ^ n) a)) '' s

Proof state:
case h.mk
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
⊢ (a, b) ∈ s ×ˢ s ↔ (a, b) ∈ ⋃ n, (fun a => (a, (f ^ n) a)) '' s

Tactic:
simp only [Set.mem_prod, Set.mem_iUnion, Set.mem_image]

Result:
case h.mk
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
⊢ a ∈ s ∧ b ∈ s ↔ ∃ i, ∃ x ∈ s, (x, (f ^ i) x) = (a, b)
-- Mathlib/CategoryTheory/Monoidal/Cartesian/Comon_.lean
theorem comul_eq_diag (A : Comon_ C) : A.comul = diag A.X

Proof state:
case w₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
A : Comon_ C
⊢ A.comul ≫ prod.snd = diag A.X ≫ prod.snd

Tactic:
simpa using A.counit_comul =≫ prod.snd

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
A : Comon_ C
⊢ A.comul = diag A.X

Tactic:
ext

Result:
case w₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
A : Comon_ C
⊢ A.comul ≫ prod.fst = diag A.X ≫ prod.fst

case w₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
A : Comon_ C
⊢ A.comul ≫ prod.snd = diag A.X ≫ prod.snd

Proof state:
case w₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
A : Comon_ C
⊢ A.comul ≫ prod.fst = diag A.X ≫ prod.fst

Tactic:
simpa using A.comul_counit =≫ prod.fst

Result:
no goals
-- Mathlib/Data/Analysis/Topology.lean
theorem isClosed_iff [TopologicalSpace α] (F : Realizer α) {s : Set α} :
    IsClosed s ↔ ∀ a, (∀ b, a ∈ F.F b → ∃ z, z ∈ F.F b ∩ s) → a ∈ s :=
  isOpen_compl_iff.symm.trans <|
    F.isOpen_iff.trans <|
      forall_congr' fun a ↦
        show (a ∉ s → ∃ b : F.σ, a ∈ F.F b ∧ ∀ z ∈ F.F b, z ∉ s) ↔ _ by
          haveI := Classical.propDecidable; rw [not_imp_comm]
          simp [not_exists, not_and, not_forall, and_comm]

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (¬∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) → a ∈ s ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s

Tactic:
simp [not_exists, not_and, not_forall, and_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (a ∉ s → ∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s

Tactic:
rw [not_imp_comm]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (¬∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) → a ∈ s ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
⊢ (a ∉ s → ∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s

Tactic:
haveI := Classical.propDecidable

Result:
α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (a ∉ s → ∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem domRestrict (p : Submodule R₁ M₁) : (B.domRestrict₁₂ p p).IsRefl :=
  fun _ _ ↦ by
  simp_rw [domRestrict₁₂_apply]
  exact H _ _

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
p : Submodule R₁ M₁
x✝¹ x✝ : ↥p
⊢ ((B.domRestrict₁₂ p p) x✝¹) x✝ = 0 → ((B.domRestrict₁₂ p p) x✝) x✝¹ = 0

Tactic:
simp_rw [domRestrict₁₂_apply]

Result:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
p : Submodule R₁ M₁
x✝¹ x✝ : ↥p
⊢ (B ↑x✝¹) ↑x✝ = 0 → (B ↑x✝) ↑x✝¹ = 0

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
p : Submodule R₁ M₁
x✝¹ x✝ : ↥p
⊢ (B ↑x✝¹) ↑x✝ = 0 → (B ↑x✝) ↑x✝¹ = 0

Tactic:
exact H _ _

Result:
no goals