harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem _root_.MeasurableEmbedding.integrableOn_iff_comap [MeasurableSpace β] {e : α → β}
    (he : MeasurableEmbedding e) {f : β → E} {μ : Measure β} {s : Set β} (hs : s ⊆ range e) :
    IntegrableOn f s μ ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) (μ.comap e)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
μ : Measure β
s : Set β
hs : s ⊆ range e
⊢ IntegrableOn f s μ ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) (Measure.comap e μ)

Tactic:
simp_rw [← he.integrableOn_map_iff, he.map_comap, IntegrableOn,
  Measure.restrict_restrict_of_subset hs]

Result:
no goals
-- Mathlib/Dynamics/BirkhoffSum/Basic.lean
theorem birkhoffSum_add (f : α → α) (g : α → M) (m n : ℕ) (x : α) :
    birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x)

Proof state:
α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
g : α → M
m n : ℕ
x : α
⊢ birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x)

Tactic:
simp_rw [birkhoffSum, sum_range_add, add_comm m, iterate_add_apply]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem single_zero_mul_apply [AddZeroClass G] (f : k[G]) (r : k) (x : G) :
    (single (0 : G) r * f) x = r * f x :=
  f.single_mul_apply_aux r _ _ _ fun a _ => by rw [zero_add]

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddZeroClass G
f : k[G]
r : k
x a : G
x✝ : a ∈ f.support
⊢ 0 + a = x ↔ a = x

Tactic:
rw [zero_add]

Result:
no goals
-- Mathlib/Data/Bool/Count.lean
theorem length_div_two_le_count_bool (hl : Chain' (· ≠ ·) l) (b : Bool) :
    length l / 2 ≤ count b l

Proof state:
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
b : Bool
⊢ l.length - (2 - 1) ≤ 2 * count b l

Tactic:
exact length_sub_one_le_two_mul_count_bool hl b

Result:
no goals

Proof state:
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
b : Bool
⊢ l.length / 2 ≤ count b l

Tactic:
rw [Nat.div_le_iff_le_mul_add_pred two_pos, ← tsub_le_iff_right]

Result:
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
b : Bool
⊢ l.length - (2 - 1) ≤ 2 * count b l
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma odd_abs [LinearOrder α] [Ring α] {a : α} : Odd (abs a) ↔ Odd a

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Ring α
a : α
⊢ Odd |a| ↔ Odd a

Tactic:
rcases abs_choice a with h | h <;> simp only [h, odd_neg]

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem chain_append_singleton_iff_forall₂ :
    Chain R a (l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b])

Proof state:
α : Type u
R : α → α → Prop
l : List α
a b : α
⊢ Chain R a (l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b])

Tactic:
simp [chain_iff_forall₂]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem remainingBytes_le : ∀ {it}, Valid it → it.remainingBytes ≤ utf8ByteSize it.s
  | _, h => let ⟨l, r, h⟩ := h.validFor; by simp [h.remainingBytes, h.toString, Nat.le_add_left]

Proof state:
x✝ : Iterator
h✝ : x✝.Valid
l r : List Char
h : ValidFor l r x✝
⊢ x✝.remainingBytes ≤ x✝.s.utf8ByteSize

Tactic:
simp [h.remainingBytes, h.toString, Nat.le_add_left]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem Finset.coe_einfsep [DecidableEq α] {s : Finset α} :
    (s : Set α).einfsep = s.offDiag.inf (uncurry edist)

Proof state:
α : Type u_1
inst✝¹ : EDist α
inst✝ : DecidableEq α
s : Finset α
⊢ (↑s).einfsep = s.offDiag.inf (uncurry edist)

Tactic:
simp_rw [einfsep_of_fintype, ← Finset.coe_offDiag, Finset.toFinset_coe]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_compl_preimage {f : α → β} {s : Set β} : f '' (f ⁻¹' s)ᶜ = range f \ s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' (f ⁻¹' s)ᶜ = range f \ s

Tactic:
rw [compl_eq_univ_diff, image_diff_preimage, image_univ]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_swap₁₃_sign (p₁ p₂ p₃ : P) : -(∡ p₁ p₂ p₃).sign = (∡ p₃ p₂ p₁).sign

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ -(∡ p₁ p₂ p₃).sign = (∡ p₃ p₂ p₁).sign

Tactic:
rw [oangle_rev, Real.Angle.sign_neg, neg_neg]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem optionToList : Primrec (Option.toList : Option α → List α) :=
  (option_casesOn Primrec.id (const [])
    ((list_cons.comp Primrec.id (const [])).comp₂ Primrec₂.right)).of_eq
  (fun o => by rcases o <;> simp)

Proof state:
α : Type u_1
inst✝ : Primcodable α
o : Option α
⊢ (Option.casesOn (id o) [] fun b => [id b]) = o.toList

Tactic:
rcases o <;> simp

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem t0Space_iff_exists_isOpen_xor'_mem (X : Type u) [TopologicalSpace X] :
    T0Space X ↔ Pairwise fun x y => ∃ U : Set X, IsOpen U ∧ Xor' (x ∈ U) (y ∈ U)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ T0Space X ↔ Pairwise fun x y => ∃ U, IsOpen U ∧ Xor' (x ∈ U) (y ∈ U)

Tactic:
simp only [t0Space_iff_not_inseparable, xor_iff_not_iff, not_forall, exists_prop,
  inseparable_iff_forall_isOpen, Pairwise]

Result:
no goals
-- Mathlib/Data/Sign.lean
private lemma mul_comm : ∀ (a b : SignType), a * b = b * a

Proof state:
⊢ ∀ (a b : SignType), a * b = b * a

Tactic:
rintro ⟨⟩ ⟨⟩ <;> rfl

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_erase_left (a b : α) : (Ico a b).erase a = Ioo a b

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Ico a b).erase a = Ioo a b

Tactic:
simp [← coe_inj]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_nat_add (n : ℕ) (a : α) : ⌊↑n + a⌋ = n + ⌊a⌋

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
n : ℕ
a : α
⊢ ⌊↑n + a⌋ = ↑n + ⌊a⌋

Tactic:
rw [← Int.cast_natCast, floor_int_add]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem bit1_of_bit1 (n : PosNum) : (n + n) + 1 = bit1 n :=
  show (n + n) + 1 = bit1 n by rw [add_one, bit0_of_bit0, succ]

Proof state:
n : PosNum
⊢ n + n + 1 = n.bit1

Tactic:
rw [add_one, bit0_of_bit0, succ]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Basic.lean
theorem union_inter_cancel_left {s t : Finset α} : (s ∪ t) ∩ s = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∪ t) ∩ s = s

Tactic:
rw [← coe_inj, coe_inter, coe_union, Set.union_inter_cancel_left]

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem compAlongComposition_norm {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
    (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n) :
    ‖q.compAlongComposition p c‖ ≤ ‖q c.length‖ * ∏ i, ‖p (c.blocksFun i)‖ :=
  ContinuousMultilinearMap.opNorm_le_bound (by positivity) (compAlongComposition_bound _ _ _)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
⊢ 0 ≤ ‖q c.length‖ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖

Tactic:
positivity

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_div_cancel (a) {b : Ordinal} (b0 : b ≠ 0) : b * a / b = a

Proof state:
a b : Ordinal.{u_4}
b0 : b ≠ 0
⊢ b * a / b = a

Tactic:
simpa only [add_zero, zero_div] using mul_add_div a b0 0

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem transvection_zero : transvection i j (0 : R) = 1

Proof state:
n : Type u_1
R : Type u₂
inst✝¹ : DecidableEq n
inst✝ : CommRing R
i j : n
⊢ transvection i j 0 = 1

Tactic:
simp [transvection]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem normalizer_eq_top_iff : H.normalizer = ⊤ ↔ H.Normal :=
  eq_top_iff.trans
    ⟨fun h => ⟨fun a ha b => (h (mem_top b) a).mp ha⟩, fun h a _ha b =>
      ⟨fun hb => h.conj_mem b hb a, fun hb => by rwa [h.mem_comm_iff, inv_mul_cancel_left] at hb⟩⟩

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.Normal
a : G
_ha : a ∈ ⊤
b : G
hb : a * b * a⁻¹ ∈ H
⊢ b ∈ H

Tactic:
rwa [h.mem_comm_iff, inv_mul_cancel_left] at hb

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem _root_.IsCompact.exists_infDist_eq_dist (h : IsCompact s) (hne : s.Nonempty) (x : α) :
    ∃ y ∈ s, infDist x s = dist x y :=
  let ⟨y, hys, hy⟩ := h.exists_infEdist_eq_edist hne x
  ⟨y, hys, by rw [infDist, dist_edist, hy]⟩

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
h : IsCompact s
hne : s.Nonempty
x y : α
hys : y ∈ s
hy : infEdist x s = edist x y
⊢ infDist x s = dist x y

Tactic:
rw [infDist, dist_edist, hy]

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
lemma essSup_eq_ciSup (hμ : ∀ a, μ {a} ≠ 0) (hf : BddAbove (Set.range f)) :
    essSup f μ = ⨆ a, f a

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : ConditionallyCompleteLattice β
f : α → β
inst✝ : Nonempty α
hμ : ∀ (a : α), μ {a} ≠ 0
hf : BddAbove (range f)
⊢ essSup f μ = ⨆ a, f a

Tactic:
rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_ciSup hf]

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean
theorem map_pow_of_nonempty [IsAlgClosed 𝕜] {a : A} (ha : (σ a).Nonempty) (n : ℕ) :
    σ (a ^ n) = (· ^ n) '' σ a

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
ha : (σ a).Nonempty
n : ℕ
⊢ σ (a ^ n) = (fun x => x ^ n) '' σ a

Tactic:
simpa only [aeval_X_pow, eval_pow, eval_X] using map_polynomial_aeval_of_nonempty a (X ^ n) ha

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem coprime_mul_iff_left : Coprime (m * n) k ↔ Coprime m k ∧ Coprime n k :=
  ⟨fun h => ⟨h.coprime_mul_right, h.coprime_mul_left⟩,
   fun ⟨h, _⟩ => by rwa [coprime_iff_gcd_eq_one, h.gcd_mul_left_cancel n]⟩

Proof state:
m n k : Nat
x✝ : m.Coprime k ∧ n.Coprime k
h : m.Coprime k
right✝ : n.Coprime k
⊢ (m * n).Coprime k

Tactic:
rwa [coprime_iff_gcd_eq_one, h.gcd_mul_left_cancel n]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem toLp_congr {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) (hfg : f =ᵐ[μ] g) :
    hf.toLp f = hg.toLp g

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
hfg : f =ᶠ[ae μ] g
⊢ toLp f hf = toLp g hg

Tactic:
simp [toLp, hfg]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Take.lean
theorem take_zero (v : (i : Fin n) → α i) : take 0 n.zero_le v = fun i ↦ elim0 i

Proof state:
case h
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
i : Fin 0
⊢ take 0 ⋯ v i = i.elim0

Tactic:
exact elim0 i

Result:
no goals

Proof state:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
⊢ take 0 ⋯ v = fun i => i.elim0

Tactic:
ext i

Result:
case h
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
i : Fin 0
⊢ take 0 ⋯ v i = i.elim0
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_neg {R : Type*} {R₂ : Type*} {M : Type*} {M₂ : Type*} [Semiring R] [Ring R₂]
    [AddCommMonoid M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂}
    [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) : LinearMap.range (-f) = LinearMap.range f

Proof state:
R : Type u_11
R₂ : Type u_12
M : Type u_13
M₂ : Type u_14
inst✝⁶ : Semiring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ range (-f) = range f

Tactic:
change range ((-LinearMap.id : M₂ →ₗ[R₂] M₂).comp f) = _

Result:
R : Type u_11
R₂ : Type u_12
M : Type u_13
M₂ : Type u_14
inst✝⁶ : Semiring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ range ((-id).comp f) = range f

Proof state:
R : Type u_11
R₂ : Type u_12
M : Type u_13
M₂ : Type u_14
inst✝⁶ : Semiring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ range ((-id).comp f) = range f

Tactic:
rw [range_comp, Submodule.map_neg, Submodule.map_id]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean
@[reassoc (attr := simp)]
lemma lift_commutes_zero {Y Z : C} (f : Y ⟶ Z)
    (P : ProjectiveResolution Y) (Q : ProjectiveResolution Z) :
    (lift f P Q).f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f :=
  (HomologicalComplex.congr_hom (lift_commutes f P Q) 0).trans (by simp)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ (P.π ≫ (ChainComplex.single₀ C).map f).f 0 = P.π.f 0 ≫ f

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem dvd_mod_iff {k m n : Nat} (h: k ∣ n) : k ∣ m % n ↔ k ∣ m

Proof state:
k m n : Nat
h : k ∣ n
⊢ k ∣ m % n ↔ k ∣ m

Tactic:
have := Nat.dvd_add_iff_left (m := m % n) <| Nat.dvd_trans h <| Nat.dvd_mul_right n (m / n)

Result:
k m n : Nat
h : k ∣ n
this : k ∣ m % n ↔ k ∣ m % n + n * (m / n)
⊢ k ∣ m % n ↔ k ∣ m

Proof state:
k m n : Nat
h : k ∣ n
this : k ∣ m % n ↔ k ∣ m % n + n * (m / n)
⊢ k ∣ m % n ↔ k ∣ m

Tactic:
rwa [mod_add_div] at this

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma baseChange_polynomialY : (W'.baseChange B).toAffine.polynomialY =
    (W'.baseChange A).toAffine.polynomialY.map (mapRingHom f)

Proof state:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (baseChange W' B).toAffine.polynomialY = Polynomial.map (mapRingHom ↑f) (baseChange W' A).toAffine.polynomialY

Tactic:
rw [← map_polynomialY, map_baseChange]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SeminormFromConst.lean
theorem seminormFromConst_seq_one (n : ℕ) (hn : 1 ≤ n) : seminormFromConst_seq c f 1 n = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hc : f c ≠ 0
hpm : IsPowMul ⇑f
n : ℕ
hn : 1 ≤ n
⊢ seminormFromConst_seq c f 1 n = 1

Tactic:
simp only [seminormFromConst_seq]

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hc : f c ≠ 0
hpm : IsPowMul ⇑f
n : ℕ
hn : 1 ≤ n
⊢ f (1 * c ^ n) / f c ^ n = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hc : f c ≠ 0
hpm : IsPowMul ⇑f
n : ℕ
hn : 1 ≤ n
⊢ f (1 * c ^ n) / f c ^ n = 1

Tactic:
rw [one_mul, hpm _ hn, div_self (pow_ne_zero n hc)]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
theorem toQuaternion_comp_ofQuaternion :
    toQuaternion.comp ofQuaternion = AlgHom.id R ℍ[R,c₁,0,c₂]

Proof state:
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ toQuaternion.comp ofQuaternion = AlgHom.id R ℍ[R,c₁,c₂]

Tactic:
ext : 1 <;> simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem zsmul (z : ℤ) (x : WittVector p R) : mapFun f (z • x) = z • mapFun f x

Proof state:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
z : ℤ
x : 𝕎 R
⊢ mapFun (⇑f) (z • x) = z • mapFun (⇑f) x

Tactic:
map_fun_tac

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_sub_self_left (a b : Nat) : (a + b) - a = b

Proof state:
case succ
b a : Nat
ih : a + b - a = b
⊢ a + b - a = b

Tactic:
apply ih

Result:
no goals

Proof state:
case succ
b a : Nat
ih : a + b - a = b
⊢ a + 1 + b - (a + 1) = b

Tactic:
rw [Nat.succ_add, Nat.succ_sub_succ]

Result:
case succ
b a : Nat
ih : a + b - a = b
⊢ a + b - a = b

Proof state:
a b : Nat
⊢ a + b - a = b

Tactic:
induction a with
| zero => simp
| succ a ih =>
  rw [Nat.succ_add, Nat.succ_sub_succ]
  apply ih

Result:
no goals

Proof state:
case zero
b : Nat
⊢ 0 + b - 0 = b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
theorem inv_eq_one_div (x : G) : x⁻¹ = 1 / x

Proof state:
G : Type u_1
inst✝ : DivInvMonoid G
x : G
⊢ x⁻¹ = 1 / x

Tactic:
rw [div_eq_mul_inv, one_mul]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem le_div_self_iff (a : α) {b : α} : a ≤ a / b ↔ b ≤ 1

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ a ≤ a / b ↔ b ≤ 1

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem swap_comp_apply {a b x : α} (π : Perm α) :
    π.trans (swap a b) x = if π x = a then b else if π x = b then a else π x

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
π : Perm α
⊢ (Equiv.trans π (swap a b)) x = if π x = a then b else if π x = b then a else π x

Tactic:
cases π

Result:
case mk
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
toFun✝ invFun✝ : α → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
⊢ ({ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.trans (swap a b)) x =
    if { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x = a then b
    else
      if { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x = b then a
      else { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x

Proof state:
case mk
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
toFun✝ invFun✝ : α → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
⊢ ({ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.trans (swap a b)) x =
    if { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x = a then b
    else
      if { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x = b then a
      else { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.eq [AddZeroClass α] [Neg β] (h : Antiperiodic f c) : f c = -f 0

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddZeroClass α
inst✝ : Neg β
h : Antiperiodic f c
⊢ f c = -f 0

Tactic:
simpa only [zero_add] using h 0

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem dual_rank_eq [CommRing K] [AddCommGroup V] [Module K V] [Finite ι] (b : Basis ι K V) :
    Cardinal.lift.{uK,uV} (Module.rank K V) = Module.rank K (Dual K V)

Proof state:
K : Type uK
V : Type uV
ι : Type uι
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Finite ι
b : Basis ι K V
⊢ lift.{uK, uV} (Module.rank K V) = Module.rank K (Dual K V)

Tactic:
classical rw [← lift_umax.{uV,uK}, b.toDualEquiv.lift_rank_eq, lift_id'.{uV,uK}]

Result:
no goals

Proof state:
K : Type uK
V : Type uV
ι : Type uι
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Finite ι
b : Basis ι K V
⊢ lift.{uK, uV} (Module.rank K V) = Module.rank K (Dual K V)

Tactic:
rw [← lift_umax.{uV,uK}, b.toDualEquiv.lift_rank_eq, lift_id'.{uV,uK}]

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem isWF_univ_iff : IsWF (univ : Set α) ↔ WellFounded ((· < ·) : α → α → Prop)

Proof state:
α : Type u_2
inst✝ : LT α
⊢ univ.IsWF ↔ WellFounded fun x1 x2 => x1 < x2

Tactic:
simp [IsWF, wellFoundedOn_iff]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem smul_unitClosedBall (c : 𝕜) : c • closedBall (0 : E) (1 : ℝ) = closedBall (0 : E) ‖c‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
⊢ c • closedBall 0 1 = closedBall 0 ‖c‖

Tactic:
rw [_root_.smul_closedBall _ _ zero_le_one, smul_zero, mul_one]

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem ofCauchy_inv {f} : (⟨f⁻¹⟩ : ℝ) = ⟨f⟩⁻¹ :=
  show _ = inv' _ by rw [inv']

Proof state:
f : Cauchy abs
⊢ { cauchy := f⁻¹ } = Real.inv' { cauchy := f }

Tactic:
rw [inv']

Result:
no goals
-- Mathlib/MeasureTheory/Covering/VitaliFamily.lean
theorem frequently_filterAt_iff {x : X} {P : Set X → Prop} :
    (∃ᶠ t in v.filterAt x, P t) ↔ ∀ ε > (0 : ℝ), ∃ t ∈ v.setsAt x, t ⊆ closedBall x ε ∧ P t

Proof state:
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
P : Set X → Prop
⊢ (∃ᶠ (t : Set X) in v.filterAt x, P t) ↔ ∀ ε > 0, ∃ t ∈ v.setsAt x, t ⊆ closedBall x ε ∧ P t

Tactic:
simp only [(v.filterAt_basis_closedBall x).frequently_iff, ← and_assoc, subset_def, mem_setOf]

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem map_eq_setLIntegral_pdf {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω)
    (μ : Measure E

Proof state:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
hX : HasPDF X ℙ μ
s : Set E
hs : MeasurableSet s
⊢ (map X ℙ) s = ∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ

Tactic:
rw [← withDensity_apply _ hs, map_eq_withDensity_pdf X ℙ μ]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem Injective.of_comp_right {g : γ → α} (I : Injective (f ∘ g)) (hg : Surjective g) :
    Injective f := fun x y h ↦ by
  obtain ⟨x, rfl⟩ := hg x
  obtain ⟨y, rfl⟩ := hg y
  exact congr_arg g (I h)

Proof state:
case intro
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
y : α
x : γ
h : f (g x) = f y
⊢ g x = y

Tactic:
obtain ⟨y, rfl⟩ := hg y

Result:
case intro.intro
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
x y : γ
h : f (g x) = f (g y)
⊢ g x = g y

Proof state:
case intro.intro
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
x y : γ
h : f (g x) = f (g y)
⊢ g x = g y

Tactic:
exact congr_arg g (I h)

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
x y : α
h : f x = f y
⊢ x = y

Tactic:
obtain ⟨x, rfl⟩ := hg x

Result:
case intro
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
y : α
x : γ
h : f (g x) = f y
⊢ g x = y
-- Mathlib/Computability/Primrec.lean
theorem list_casesOn' {f : α → List β} {g : α → σ} {h : α → β × List β → σ}
    (hf : haveI := prim H; Primrec f) (hg : Primrec g) (hh : haveI := prim H; Primrec₂ h) :
    @Primrec _ σ _ _ fun a => List.casesOn (f a) (g a) fun b l => h a (b, l) :=
  letI := prim H
  have :
    @Primrec _ (Option σ) _ _ fun a =>
      (@decode (Option (β × List β)) _ (encode (f a))).map fun o => Option.casesOn o (g a) (h a) :=
    ((@map_decode_iff _ (Option (β × List β)) _ _ _ _ _).2 <|
      to₂ <|
        option_casesOn snd (hg.comp fst) (hh.comp₂ (fst.comp₂ Primrec₂.left) Primrec₂.right)).comp
      .id (encode_iff.2 hf)
  option_some_iff.1 <| this.of_eq fun a => by rcases f a with - | ⟨b, l⟩ <;> simp [encodek]

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a => Option.map (fun o => Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
⊢ Option.map (fun o => Option.casesOn o (g a) (h a)) (decode (encode (f a))) =
    some (List.casesOn (f a) (g a) fun b l => h a (b, l))

Tactic:
rcases f a with - | ⟨b, l⟩ <;> simp [encodek]

Result:
no goals
-- Mathlib/LinearAlgebra/SymplecticGroup.lean
theorem mem_iff' : A ∈ symplecticGroup l R ↔ Aᵀ * J l R * A = J l R

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
⊢ A ∈ symplecticGroup l R ↔ Aᵀ * J l R * A = J l R

Tactic:
rw [← transpose_mem_iff, mem_iff, transpose_transpose]

Result:
no goals